Step 1

? (((tpp a b) & (tpp b c)) => ((tpp a c) v (ntpp a c)))


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

? (((~ (tpp a b)) v (~ (tpp b c))) v ((tpp a c) v (ntpp a c)))


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

? ((~ (tpp a b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c))))


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

? (((~ (pp a b)) v ((~ (ec c185732 a)) v (~ (ec c185732 b)))) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c))))


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

? ((~ (pp a b)) v (((~ (ec c185732 a)) v (~ (ec c185732 b))) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))


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

? (((~ (p a b)) v (p b a)) v (((~ (ec c185732 a)) v (~ (ec c185732 b))) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))


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

? ((~ (p a b)) v ((p b a) v (((~ (ec c185732 a)) v (~ (ec c185732 b))) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c))))))


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

? (exists x185733 (((c x185733 a) v ((p b a) v (((~ (ec c185732 a)) v (~ (ec c185732 b))) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))) & ((~ (c x185733 b)) v ((p b a) v (((~ (ec c185732 a)) v (~ (ec c185732 b))) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c))))))))


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

? (((c Var227 a) v ((p b a) v (((~ (ec c185732 a)) v (~ (ec c185732 b))) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))) & ((~ (c Var227 b)) v ((p b a) v (((~ (ec c185732 a)) v (~ (ec c185732 b))) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))))


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

? ((~ (c Var253 b)) v ((p b a) v (((~ (ec c185732 a)) v (~ (ec c185732 b))) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c))))))


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

? ((p b a) v (((~ (ec c185732 a)) v (~ (ec c185732 b))) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))

1. (all x185737 (c x185737 b))

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

? (((~ (c c185739 b)) v (c c185739 a)) v (((~ (ec c185732 a)) v (~ (ec c185732 b))) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))

1. (all x185737 (c x185737 b))

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

? ((~ (c c185739 b)) v ((c c185739 a) v (((~ (ec c185732 a)) v (~ (ec c185732 b))) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c))))))

1. (all x185737 (c x185737 b))

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

? ((c c185739 a) v (((~ (ec c185732 a)) v (~ (ec c185732 b))) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))

1. (c c185739 b)
2. (all x185737 (c x185737 b))

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

? (((~ (ec c185732 a)) v (~ (ec c185732 b))) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c))))

1. (~ (c c185739 a))
2. (c c185739 b)
3. (all x185737 (c x185737 b))

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

? ((~ (ec c185732 a)) v ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))

1. (~ (c c185739 a))
2. (c c185739 b)
3. (all x185737 (c x185737 b))

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

? (((~ (c c185732 a)) v (o c185732 a)) v ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))

1. (~ (c c185739 a))
2. (c c185739 b)
3. (all x185737 (c x185737 b))

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

? ((~ (c c185732 a)) v ((o c185732 a) v ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c))))))

1. (~ (c c185739 a))
2. (c c185739 b)
3. (all x185737 (c x185737 b))

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

? ((o c185732 a) v ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))

1. (c c185732 a)
2. (~ (c c185739 a))
3. (c c185739 b)
4. (all x185737 (c x185737 b))

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

? (exists x185740 (((p x185740 c185732) v ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c))))) & ((p x185740 a) v ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))))

1. (c c185732 a)
2. (~ (c c185739 a))
3. (c c185739 b)
4. (all x185737 (c x185737 b))

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

? (((p Var424 c185732) v ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c))))) & ((p Var424 a) v ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c))))))

1. (c c185732 a)
2. (~ (c c185739 a))
3. (c c185739 b)
4. (all x185737 (c x185737 b))

> &r
=============================
|Step 32
|
|? ((p Var424 c185732) v ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))
|
|1. (c c185732 a)
|2. (~ (c c185739 a))
|3. (c c185739 b)
|4. (all x185737 (c x185737 b))
|
|> demodulate+revsk
|=============================
|Step 33
|
|? (((~ (c c185742 Var424)) v (c c185742 c185732)) v ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))
|
|1. (c c185732 a)
|2. (~ (c c185739 a))
|3. (c c185739 b)
|4. (all x185737 (c x185737 b))
|
|> assocv
|=============================
|Step 34
|
|? ((~ (c c185742 Var424)) v ((c c185742 c185732) v ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c))))))
|
|1. (c c185732 a)
|2. (~ (c c185739 a))
|3. (c c185739 b)
|4. (all x185737 (c x185737 b))
|
|> supp-
|=============================
|Step 35
|
|? ((c c185742 c185732) v ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))
|
|1. (all x185743 (c c185742 x185743))
|2. (c c185732 a)
|3. (~ (c c185739 a))
|4. (c c185739 b)
|5. (all x185737 (c x185737 b))
|
|> supp+
|=============================
|Step 36
|
|? ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c))))
|
|1. (~ (c c185742 c185732))
|2. (all x185743 (c c185742 x185743))
|3. (c c185732 a)
|4. (~ (c c185739 a))
|5. (c c185739 b)
|6. (all x185737 (c x185737 b))
|
|> contradiction
|=============================
Step 37

? ((p Var459 a) v ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))

1. (c c185732 a)
2. (~ (c c185739 a))
3. (c c185739 b)
4. (all x185737 (c x185737 b))

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

? (((~ (c c185745 Var459)) v (c c185745 a)) v ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))

1. (c c185732 a)
2. (~ (c c185739 a))
3. (c c185739 b)
4. (all x185737 (c x185737 b))

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

? ((~ (c c185745 Var459)) v ((c c185745 a) v ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c))))))

1. (c c185732 a)
2. (~ (c c185739 a))
3. (c c185739 b)
4. (all x185737 (c x185737 b))

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

? ((c c185745 a) v ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c)))))

1. (all x185746 (c c185745 x185746))
2. (c c185732 a)
3. (~ (c c185739 a))
4. (c c185739 b)
5. (all x185737 (c x185737 b))

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

? ((~ (ec c185732 b)) v ((~ (tpp b c)) v ((tpp a c) v (ntpp a c))))

1. (~ (c c185745 a))
2. (all x185746 (c c185745 x185746))
3. (c c185732 a)
4. (~ (c c185739 a))
5. (c c185739 b)
6. (all x185737 (c x185737 b))

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