Fixed that - proof is 2 steps shorter; but takes longer to find - odd.
Step 1
? (all a (all x ((eq (+ a x) e) => (eq a (inv x)))))
> revsk
=============================
Step 2
? ((~ (eq (+ c26534 c26533) e)) v (eq c26534 (inv c26533)))
> supp
=============================
Step 3
? (eq c26534 (inv c26533))
1. (eq (+ c26534 c26533) e)
> paramodulate
=============================
|Step 4
|
|? (eq Var109 c26534)
|
|1. (~ (eq c26534 (inv c26533)))
|2. (eq (+ c26534 c26533) e)
|
|> paramodulate
|=============================
||Step 5
||
||? (eq Var118 c26534)
||
||1. (~ (eq Var117 c26534))
||2. (~ (eq c26534 (inv c26533)))
||3. (eq (+ c26534 c26533) e)
||
||> ((eq (+ X e) X) <--)
||=============================
|Step 6
|
|? (eq Var117 (+ c26534 e))
|
|1. (~ (eq Var117 c26534))
|2. (~ (eq c26534 (inv c26533)))
|3. (eq (+ c26534 c26533) e)
|
|> paramodulate
|=============================
||Step 7
||
||? (eq Var138 e)
||
||1. (~ (eq Var131 (+ c26534 e)))
||2. (~ (eq Var131 c26534))
||3. (~ (eq c26534 (inv c26533)))
||4. (eq (+ c26534 c26533) e)
||
||> ((eq (+ X (inv X)) e) <--)
||=============================
|Step 8
|
|? (eq Var131 (+ c26534 (+ Var145 (inv Var145))))
|
|1. (~ (eq Var131 (+ c26534 e)))
|2. (~ (eq Var131 c26534))
|3. (~ (eq c26534 (inv c26533)))
|4. (eq (+ c26534 c26533) e)
|
|> ((eq X X) <--)
|=============================
Step 9
? (eq (+ c26534 (+ Var145 (inv Var145))) (inv c26533))
1. (~ (eq c26534 (inv c26533)))
2. (eq (+ c26534 c26533) e)
> paramodulate
=============================
|Step 10
|
|? (eq Var158 (inv c26533))
|
|1. (~ (eq (+ c26534 (+ Var145 (inv Var145))) (inv c26533)))
|2. (~ (eq c26534 (inv c26533)))
|3. (eq (+ c26534 c26533) e)
|
|> ((eq (+ e X) X) <--)
|=============================
Step 11
? (eq (+ c26534 (+ Var145 (inv Var145))) (+ e (inv c26533)))
1. (~ (eq (+ c26534 (+ Var145 (inv Var145))) (inv c26533)))
2. (~ (eq c26534 (inv c26533)))
3. (eq (+ c26534 c26533) e)
> paramodulate
=============================
|Step 12
|
|? (eq Var176 e)
|
|1. (~ (eq (+ c26534 (+ Var145 (inv Var145))) (+ e (inv c26533))))
|2. (~ (eq (+ c26534 (+ Var145 (inv Var145))) (inv c26533)))
|3. (~ (eq c26534 (inv c26533)))
|4. (eq (+ c26534 c26533) e)
|
|> hyp
|=============================
Step 13
? (eq (+ c26534 (+ Var145 (inv Var145))) (+ (+ c26534 c26533) (inv c26533)))
1. (~ (eq (+ c26534 (+ Var145 (inv Var145))) (+ e (inv c26533))))
2. (~ (eq (+ c26534 (+ Var145 (inv Var145))) (inv c26533)))
3. (~ (eq c26534 (inv c26533)))
4. (eq (+ c26534 c26533) e)
> ((eq (+ X (+ Y Z)) (+ (+ X Y) Z)) <--)
=============================
M.