Step 1

? (all a (all x ((eq (+ a x) e) => (eq a (inv x)))))


> ftp.revsk
=============================
Step 2

? ((~ (eq (+ c47815 c47814) e)) v (eq c47815 (inv c47814)))


> supp-
=============================
Step 3

? (eq c47815 (inv c47814))

1. (eq (+ c47815 c47814) e)

> paramodulate
=============================
|Step 4
|
|? (eq c47815 (inv c47814))
|
|1. (~ (eq c47815 (inv c47814)))
|2. (eq (+ c47815 c47814) e)
|
|> paramodulate right
|=============================
|Step 5
|
|? (eq c47815 Var96)
|
|1. (~ (eq c47815 (inv c47814)))
|2. (eq (+ c47815 c47814) e)
|
|> paramodulate
|=============================
||Step 6
||
||? (eq c47815 Var96)
||
||1. (~ (eq c47815 Var96))
||2. (~ (eq c47815 (inv c47814)))
||3. (eq (+ c47815 c47814) e)
||
||> paramodulate left
||=============================
||Step 7
||
||? (eq Var108 c47815)
||
||1. (~ (eq c47815 Var109))
||2. (~ (eq c47815 (inv c47814)))
||3. (eq (+ c47815 c47814) e)
||
||> ((eq (+ e X) X) <--)
||=============================
|Step 8
|
|? (eq (+ e c47815) Var109)
|
|1. (~ (eq c47815 Var109))
|2. (~ (eq c47815 (inv c47814)))
|3. (eq (+ c47815 c47814) e)
|
|> paramodulate
|=============================
||Step 9
||
||? (eq (+ e c47815) Var109)
||
||1. (~ (eq (+ e c47815) Var109))
||2. (~ (eq c47815 Var109))
||3. (~ (eq c47815 (inv c47814)))
||4. (eq (+ c47815 c47814) e)
||
||> zeroing on term ...
||=============================
||Step 10
||
||? (eq (+ e c47815) Var127)
||
||1. (~ (eq (+ e c47815) Var127))
||2. (~ (eq c47815 Var127))
||3. (~ (eq c47815 (inv c47814)))
||4. (eq (+ c47815 c47814) e)
||
||> zeroing on terms ...
||=============================
||Step 11
||
||? (eq (+ e c47815) Var127)
||
||1. (~ (eq (+ e c47815) Var127))
||2. (~ (eq c47815 Var127))
||3. (~ (eq c47815 (inv c47814)))
||4. (eq (+ c47815 c47814) e)
||
||> paramodulate left
||=============================
||Step 12
||
||? (eq Var145 c47815)
||
||1. (~ (eq (+ e c47815) Var127))
||2. (~ (eq c47815 Var127))
||3. (~ (eq c47815 (inv c47814)))
||4. (eq (+ c47815 c47814) e)
||
||> ((eq (+ X e) X) <--)
||=============================
|Step 13
|
|? (eq (+ e (+ c47815 e)) Var127)
|
|1. (~ (eq (+ e c47815) Var127))
|2. (~ (eq c47815 Var127))
|3. (~ (eq c47815 (inv c47814)))
|4. (eq (+ c47815 c47814) e)
|
|> ((eq (+ e X) X) <--)
|=============================
Step 14

? (eq (+ c47815 e) (inv c47814))

1. (~ (eq c47815 (inv c47814)))
2. (eq (+ c47815 c47814) e)

> paramodulate
=============================
|Step 15
|
|? (eq (+ c47815 e) (inv c47814))
|
|1. (~ (eq (+ c47815 e) (inv c47814)))
|2. (~ (eq c47815 (inv c47814)))
|3. (eq (+ c47815 c47814) e)
|
|> paramodulate right
|=============================
|Step 16
|
|? (eq (+ c47815 e) Var163)
|
|1. (~ (eq (+ c47815 e) (inv c47814)))
|2. (~ (eq c47815 (inv c47814)))
|3. (eq (+ c47815 c47814) e)
|
|> paramodulate
|=============================
||Step 17
||
||? (eq (+ c47815 e) Var163)
||
||1. (~ (eq (+ c47815 e) Var163))
||2. (~ (eq (+ c47815 e) (inv c47814)))
||3. (~ (eq c47815 (inv c47814)))
||4. (eq (+ c47815 c47814) e)
||
||> zeroing on term ...
||=============================
||Step 18
||
||? (eq (+ c47815 e) Var176)
||
||1. (~ (eq (+ c47815 e) Var176))
||2. (~ (eq (+ c47815 e) (inv c47814)))
||3. (~ (eq c47815 (inv c47814)))
||4. (eq (+ c47815 c47814) e)
||
||> zeroing on terms ...
||=============================
||Step 19
||
||? (eq (+ c47815 e) Var176)
||
||1. (~ (eq (+ c47815 e) Var176))
||2. (~ (eq (+ c47815 e) (inv c47814)))
||3. (~ (eq c47815 (inv c47814)))
||4. (eq (+ c47815 c47814) e)
||
||> paramodulate left
||=============================
||Step 20
||
||? (eq Var194 e)
||
||1. (~ (eq (+ c47815 e) Var176))
||2. (~ (eq (+ c47815 e) (inv c47814)))
||3. (~ (eq c47815 (inv c47814)))
||4. (eq (+ c47815 c47814) e)
||
||> ((eq (+ X (inv X)) e) <--)
||=============================
|Step 21
|
|? (eq (+ c47815 (+ Var201 (inv Var201))) Var176)
|
|1. (~ (eq (+ c47815 e) Var176))
|2. (~ (eq (+ c47815 e) (inv c47814)))
|3. (~ (eq c47815 (inv c47814)))
|4. (eq (+ c47815 c47814) e)
|
|> ((eq (+ X (+ Y Z)) (+ (+ X Y) Z)) <--)
|=============================
Step 22

? (eq (+ (+ c47815 Var208) (inv Var208)) (inv c47814))

1. (~ (eq (+ c47815 e) (inv c47814)))
2. (~ (eq c47815 (inv c47814)))
3. (eq (+ c47815 c47814) e)

> paramodulate
=============================
|Step 23
|
|? (eq (+ (+ c47815 Var208) (inv Var208)) (inv c47814))
|
|1. (~ (eq (+ (+ c47815 Var208) (inv Var208)) (inv c47814)))
|2. (~ (eq (+ c47815 e) (inv c47814)))
|3. (~ (eq c47815 (inv c47814)))
|4. (eq (+ c47815 c47814) e)
|
|> zeroing on term ...
|=============================
|Step 24
|
|? (eq (+ (+ c47815 Var208) (inv Var208)) (inv c47814))
|
|1. (~ (eq (+ (+ c47815 Var208) (inv Var208)) (inv c47814)))
|2. (~ (eq (+ c47815 e) (inv c47814)))
|3. (~ (eq c47815 (inv c47814)))
|4. (eq (+ c47815 c47814) e)
|
|> paramodulate right
|=============================
|Step 25
|
|? (eq (+ c47815 Var208) Var229)
|
|1. (~ (eq (+ (+ c47815 Var208) (inv Var208)) (inv c47814)))
|2. (~ (eq (+ c47815 e) (inv c47814)))
|3. (~ (eq c47815 (inv c47814)))
|4. (eq (+ c47815 c47814) e)
|
|> hyp
|=============================
Step 26

? (eq (+ e (inv c47814)) (inv c47814))

1. (~ (eq (+ (+ c47815 c47814) (inv c47814)) (inv c47814)))
2. (~ (eq (+ c47815 e) (inv c47814)))
3. (~ (eq c47815 (inv c47814)))
4. (eq (+ c47815 c47814) e)

> ((eq (+ e X) X) <--)
=============================