Step 1

? (((tpp a b) & (ec b c)) => ((dc a c) v (ec a c)))


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

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


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

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


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

? (((~ (pp a b)) v ((~ (ec c6888 a)) v (~ (ec c6888 b)))) v ((~ (ec b c)) v ((dc a c) v (ec a c))))


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

? ((~ (pp a b)) v (((~ (ec c6888 a)) v (~ (ec c6888 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))


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

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


> assocv
=============================
Step 7

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


> demodulate+revsk
=============================
Step 8

? (exists x6889 (((c x6889 a) v ((p b a) v (((~ (ec c6888 a)) v (~ (ec c6888 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))) & ((~ (c x6889 b)) v ((p b a) v (((~ (ec c6888 a)) v (~ (ec c6888 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c))))))))


> eR
=============================
Step 9

? (((c Var227 a) v ((p b a) v (((~ (ec c6888 a)) v (~ (ec c6888 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))) & ((~ (c Var227 b)) v ((p b a) v (((~ (ec c6888 a)) v (~ (ec c6888 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))))


> &r
=============================
|Step 10
|
|? ((c Var227 a) v ((p b a) v (((~ (ec c6888 a)) v (~ (ec c6888 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c))))))
|
|
|> supp+
|=============================
|Step 11
|
|? ((p b a) v (((~ (ec c6888 a)) v (~ (ec c6888 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))
|
|1. (all x6890 (~ (c x6890 a)))
|
|> demodulate+revsk
|=============================
|Step 12
|
|? (((~ (c c6892 b)) v (c c6892 a)) v (((~ (ec c6888 a)) v (~ (ec c6888 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))
|
|1. (all x6890 (~ (c x6890 a)))
|
|> assocv
|=============================
|Step 13
|
|? ((~ (c c6892 b)) v ((c c6892 a) v (((~ (ec c6888 a)) v (~ (ec c6888 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c))))))
|
|1. (all x6890 (~ (c x6890 a)))
|
|> supp-
|=============================
|Step 14
|
|? ((c c6892 a) v (((~ (ec c6888 a)) v (~ (ec c6888 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))
|
|1. (c c6892 b)
|2. (all x6890 (~ (c x6890 a)))
|
|> supp+
|=============================
|Step 15
|
|? (((~ (ec c6888 a)) v (~ (ec c6888 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c))))
|
|1. (~ (c c6892 a))
|2. (c c6892 b)
|3. (all x6890 (~ (c x6890 a)))
|
|> assocv
|=============================
|Step 16
|
|? ((~ (ec c6888 a)) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))
|
|1. (~ (c c6892 a))
|2. (c c6892 b)
|3. (all x6890 (~ (c x6890 a)))
|
|> demodulate+revsk
|=============================
|Step 17
|
|? (((~ (c c6888 a)) v (o c6888 a)) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))
|
|1. (~ (c c6892 a))
|2. (c c6892 b)
|3. (all x6890 (~ (c x6890 a)))
|
|> assocv
|=============================
|Step 18
|
|? ((~ (c c6888 a)) v ((o c6888 a) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c))))))
|
|1. (~ (c c6892 a))
|2. (c c6892 b)
|3. (all x6890 (~ (c x6890 a)))
|
|> supp-
|=============================
|Step 19
|
|? ((o c6888 a) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))
|
|1. (c c6888 a)
|2. (~ (c c6892 a))
|3. (c c6892 b)
|4. (all x6890 (~ (c x6890 a)))
|
|> contradiction
|=============================
Step 20

? ((~ (c Var253 b)) v ((p b a) v (((~ (ec c6888 a)) v (~ (ec c6888 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c))))))


> supp-
=============================
Step 21

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

1. (all x6893 (c x6893 b))

> demodulate+revsk
=============================
Step 22

? (((~ (c c6895 b)) v (c c6895 a)) v (((~ (ec c6888 a)) v (~ (ec c6888 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))

1. (all x6893 (c x6893 b))

> assocv
=============================
Step 23

? ((~ (c c6895 b)) v ((c c6895 a) v (((~ (ec c6888 a)) v (~ (ec c6888 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c))))))

1. (all x6893 (c x6893 b))

> supp-
=============================
Step 24

? ((c c6895 a) v (((~ (ec c6888 a)) v (~ (ec c6888 b))) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))

1. (c c6895 b)
2. (all x6893 (c x6893 b))

> supp+
=============================
Step 25

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

1. (~ (c c6895 a))
2. (c c6895 b)
3. (all x6893 (c x6893 b))

> assocv
=============================
Step 26

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

1. (~ (c c6895 a))
2. (c c6895 b)
3. (all x6893 (c x6893 b))

> demodulate+revsk
=============================
Step 27

? (((~ (c c6888 a)) v (o c6888 a)) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))

1. (~ (c c6895 a))
2. (c c6895 b)
3. (all x6893 (c x6893 b))

> assocv
=============================
Step 28

? ((~ (c c6888 a)) v ((o c6888 a) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c))))))

1. (~ (c c6895 a))
2. (c c6895 b)
3. (all x6893 (c x6893 b))

> supp-
=============================
Step 29

? ((o c6888 a) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))

1. (c c6888 a)
2. (~ (c c6895 a))
3. (c c6895 b)
4. (all x6893 (c x6893 b))

> demodulate+revsk
=============================
Step 30

? (exists x6896 (((p x6896 c6888) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c))))) & ((p x6896 a) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))))

1. (c c6888 a)
2. (~ (c c6895 a))
3. (c c6895 b)
4. (all x6893 (c x6893 b))

> eR
=============================
Step 31

? (((p Var424 c6888) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c))))) & ((p Var424 a) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c))))))

1. (c c6888 a)
2. (~ (c c6895 a))
3. (c c6895 b)
4. (all x6893 (c x6893 b))

> &r
=============================
|Step 32
|
|? ((p Var424 c6888) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))
|
|1. (c c6888 a)
|2. (~ (c c6895 a))
|3. (c c6895 b)
|4. (all x6893 (c x6893 b))
|
|> demodulate+revsk
|=============================
|Step 33
|
|? (((~ (c c6898 Var424)) v (c c6898 c6888)) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))
|
|1. (c c6888 a)
|2. (~ (c c6895 a))
|3. (c c6895 b)
|4. (all x6893 (c x6893 b))
|
|> assocv
|=============================
|Step 34
|
|? ((~ (c c6898 Var424)) v ((c c6898 c6888) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c))))))
|
|1. (c c6888 a)
|2. (~ (c c6895 a))
|3. (c c6895 b)
|4. (all x6893 (c x6893 b))
|
|> supp-
|=============================
|Step 35
|
|? ((c c6898 c6888) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))
|
|1. (all x6899 (c c6898 x6899))
|2. (c c6888 a)
|3. (~ (c c6895 a))
|4. (c c6895 b)
|5. (all x6893 (c x6893 b))
|
|> supp+
|=============================
|Step 36
|
|? ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c))))
|
|1. (~ (c c6898 c6888))
|2. (all x6899 (c c6898 x6899))
|3. (c c6888 a)
|4. (~ (c c6895 a))
|5. (c c6895 b)
|6. (all x6893 (c x6893 b))
|
|> contradiction
|=============================
Step 37

? ((p Var459 a) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))

1. (c c6888 a)
2. (~ (c c6895 a))
3. (c c6895 b)
4. (all x6893 (c x6893 b))

> demodulate+revsk
=============================
Step 38

? (((~ (c c6901 Var459)) v (c c6901 a)) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))

1. (c c6888 a)
2. (~ (c c6895 a))
3. (c c6895 b)
4. (all x6893 (c x6893 b))

> assocv
=============================
Step 39

? ((~ (c c6901 Var459)) v ((c c6901 a) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c))))))

1. (c c6888 a)
2. (~ (c c6895 a))
3. (c c6895 b)
4. (all x6893 (c x6893 b))

> supp-
=============================
Step 40

? ((c c6901 a) v ((~ (ec c6888 b)) v ((~ (ec b c)) v ((dc a c) v (ec a c)))))

1. (all x6902 (c c6901 x6902))
2. (c c6888 a)
3. (~ (c c6895 a))
4. (c c6895 b)
5. (all x6893 (c x6893 b))

> supp+
=============================
Step 41

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

1. (~ (c c6901 a))
2. (all x6902 (c c6901 x6902))
3. (c c6888 a)
4. (~ (c c6895 a))
5. (c c6895 b)
6. (all x6893 (c x6893 b))

> contradiction
=============================
