Step 1

? (((e a b) & (dc b c)) => (dc a c))


> revsk
=============================
Step 2

? (((~ (e a b)) v (~ (dc b c))) v (dc a c))


> assocv
=============================
Step 3

? ((~ (e a b)) v ((~ (dc b c)) v (dc a c)))


> demodulate+revsk
=============================
Step 4

? (((~ (p a b)) v (~ (p b a))) v ((~ (dc b c)) v (dc a c)))


> assocv
=============================
Step 5

? ((~ (p a b)) v ((~ (p b a)) v ((~ (dc b c)) v (dc a c))))


> demodulate+revsk
=============================
Step 6

? (exists x185706 (((c x185706 a) v ((~ (p b a)) v ((~ (dc b c)) v (dc a c)))) & ((~ (c x185706 b)) v ((~ (p b a)) v ((~ (dc b c)) v (dc a c))))))


> eR
=============================
Step 7

? (((c Var186 a) v ((~ (p b a)) v ((~ (dc b c)) v (dc a c)))) & ((~ (c Var186 b)) v ((~ (p b a)) v ((~ (dc b c)) v (dc a c)))))


> &r
=============================
|Step 8
|
|? ((c Var186 a) v ((~ (p b a)) v ((~ (dc b c)) v (dc a c))))
|
|
|> supp+
|=============================
|Step 9
|
|? ((~ (p b a)) v ((~ (dc b c)) v (dc a c)))
|
|1. (all x185707 (~ (c x185707 a)))
|
|> demodulate+revsk
|=============================
|Step 10
|
|? (exists x185708 (((c x185708 b) v ((~ (dc b c)) v (dc a c))) & ((~ (c x185708 a)) v ((~ (dc b c)) v (dc a c)))))
|
|1. (all x185707 (~ (c x185707 a)))
|
|> eR
|=============================
|Step 11
|
|? (((c Var221 b) v ((~ (dc b c)) v (dc a c))) & ((~ (c Var221 a)) v ((~ (dc b c)) v (dc a c))))
|
|1. (all x185707 (~ (c x185707 a)))
|
|> &r
|=============================
||Step 12
||
||? ((c Var221 b) v ((~ (dc b c)) v (dc a c)))
||
||1. (all x185707 (~ (c x185707 a)))
||
||> supp+
||=============================
||Step 13
||
||? ((~ (dc b c)) v (dc a c))
||
||1. (all x185709 (~ (c x185709 b)))
||2. (all x185707 (~ (c x185707 a)))
||
||> demodulate+revsk
||=============================
||Step 14
||
||? ((c b c) v (dc a c))
||
||1. (all x185709 (~ (c x185709 b)))
||2. (all x185707 (~ (c x185707 a)))
||
||> supp+
||=============================
||Step 15
||
||? (dc a c)
||
||1. (~ (c b c))
||2. (all x185709 (~ (c x185709 b)))
||3. (all x185707 (~ (c x185707 a)))
||
||> demodulate+revsk
||=============================
||Step 16
||
||? (~ (c a c))
||
||1. (~ (c b c))
||2. (all x185709 (~ (c x185709 b)))
||3. (all x185707 (~ (c x185707 a)))
||
||> background
||=============================
||Step 17
||
||? (~ (c a c))
||
||1. (~ (c b c))
||2. (all x185709 (~ (c x185709 b)))
||3. (all x185707 (~ (c x185707 a)))
||
||> ((~ (c Y X)) <-- (~ (c X Y)))
||=============================
||Step 18
||
||? (~ (c c a))
||
||1. (c a c)
||2. (~ (c b c))
||3. (all x185709 (~ (c x185709 b)))
||4. (all x185707 (~ (c x185707 a)))
||
||> hyp
||=============================
|Step 19
|
|? ((~ (c Var247 a)) v ((~ (dc b c)) v (dc a c)))
|
|1. (all x185707 (~ (c x185707 a)))
|
|> supp-
|=============================
|Step 20
|
|? ((~ (dc b c)) v (dc a c))
|
|1. (all x185710 (c x185710 a))
|2. (all x185707 (~ (c x185707 a)))
|
|> contradiction
|=============================
Step 21

? ((~ (c Var212 b)) v ((~ (p b a)) v ((~ (dc b c)) v (dc a c))))


> supp-
=============================
Step 22

? ((~ (p b a)) v ((~ (dc b c)) v (dc a c)))

1. (all x185711 (c x185711 b))

> demodulate+revsk
=============================
Step 23

? (exists x185712 (((c x185712 b) v ((~ (dc b c)) v (dc a c))) & ((~ (c x185712 a)) v ((~ (dc b c)) v (dc a c)))))

1. (all x185711 (c x185711 b))

> eR
=============================
Step 24

? (((c Var340 b) v ((~ (dc b c)) v (dc a c))) & ((~ (c Var340 a)) v ((~ (dc b c)) v (dc a c))))

1. (all x185711 (c x185711 b))

> &r
=============================
|Step 25
|
|? ((c Var340 b) v ((~ (dc b c)) v (dc a c)))
|
|1. (all x185711 (c x185711 b))
|
|> supp+
|=============================
|Step 26
|
|? ((~ (dc b c)) v (dc a c))
|
|1. (all x185713 (~ (c x185713 b)))
|2. (all x185711 (c x185711 b))
|
|> contradiction
|=============================
Step 27

? ((~ (c Var366 a)) v ((~ (dc b c)) v (dc a c)))

1. (all x185711 (c x185711 b))

> supp-
=============================
Step 28

? ((~ (dc b c)) v (dc a c))

1. (all x185714 (c x185714 a))
2. (all x185711 (c x185711 b))

> demodulate+revsk
=============================
Step 29

? ((c b c) v (dc a c))

1. (all x185714 (c x185714 a))
2. (all x185711 (c x185711 b))

> supp+
=============================
Step 30

? (dc a c)

1. (~ (c b c))
2. (all x185714 (c x185714 a))
3. (all x185711 (c x185711 b))

> demodulate+revsk
=============================
Step 31

? (~ (c a c))

1. (~ (c b c))
2. (all x185714 (c x185714 a))
3. (all x185711 (c x185711 b))

> relative-consistency
=============================
Step 32

? (c b c)

1. (all x185714 (c x185714 a))
2. (all x185711 (c x185711 b))

> background
=============================
Step 33

? (c b c)

1. (all x185714 (c x185714 a))
2. (all x185711 (c x185711 b))

> ((c Y X) <-- (c X Y))
=============================
Step 34

? (c c b)

1. (~ (c b c))
2. (all x185714 (c x185714 a))
3. (all x185711 (c x185711 b))

> hyp
=============================
