THORN 3 paramodulation proof debugged, release imminent

17 views
Skip to first unread message

dr.mt...@gmail.com

unread,
Mar 15, 2023, 4:36:53 AM3/15/23
to Shen
THORN 3 was waffling a bit and is fixed.  I think we are ready for release.
This is a group theory proof in the new system which takes 16M inferences.
(eq x y) is x = y.

M.

Step 1

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

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

? ((~ (eq (+ c22669 c22668) e)) v (eq c22669 (inv c22668)))

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

? (eq c22669 (inv c22668))

1. (eq (+ c22669 c22668) e)

> paramodulate right
=============================
|Step 4
|
|? (eq c22669 Var124)
|
|1. (~ (eq c22669 (inv c22668)))
|2. (eq (+ c22669 c22668) e)
|
|> paramodulate left
|=============================
||Step 5
||
||? (eq Var132 c22669)
||
||1. (~ (eq c22669 Var133))
||2. (~ (eq c22669 (inv c22668)))
||3. (eq (+ c22669 c22668) e)
||
||> ((eq (+ e X) X) <--)
||=============================
|Step 6
|
|? (eq (+ e c22669) Var133)
|
|1. (~ (eq c22669 Var133))
|2. (~ (eq c22669 (inv c22668)))
|3. (eq (+ c22669 c22668) e)
|
|> paramodulate left
|=============================
||Step 7
||
||? (eq Var153 c22669)
||
||1. (~ (eq (+ e c22669) Var147))
||2. (~ (eq c22669 Var147))
||3. (~ (eq c22669 (inv c22668)))
||4. (eq (+ c22669 c22668) e)
||
||> ((eq (+ X e) X) <--)
||=============================
|Step 8
|
|? (eq (+ e (+ c22669 e)) Var147)
|
|1. (~ (eq (+ e c22669) Var147))
|2. (~ (eq c22669 Var147))
|3. (~ (eq c22669 (inv c22668)))
|4. (eq (+ c22669 c22668) e)
|
|> ((eq (+ e X) X) <--)
|=============================
Step 9

? (eq (+ c22669 e) (inv c22668))

1. (~ (eq c22669 (inv c22668)))
2. (eq (+ c22669 c22668) e)

> paramodulate right
=============================
|Step 10
|
|? (eq (+ c22669 e) Var171)
|
|1. (~ (eq (+ c22669 e) (inv c22668)))
|2. (~ (eq c22669 (inv c22668)))
|3. (eq (+ c22669 c22668) e)
|
|> paramodulate left
|=============================
||Step 11
||
||? (eq Var186 e)
||
||1. (~ (eq (+ c22669 e) Var180))
||2. (~ (eq (+ c22669 e) (inv c22668)))
||3. (~ (eq c22669 (inv c22668)))
||4. (eq (+ c22669 c22668) e)
||
||> ((eq (+ X (inv X)) e) <--)
||=============================
|Step 12
|
|? (eq (+ c22669 (+ Var193 (inv Var193))) Var180)
|
|1. (~ (eq (+ c22669 e) Var180))
|2. (~ (eq (+ c22669 e) (inv c22668)))
|3. (~ (eq c22669 (inv c22668)))
|4. (eq (+ c22669 c22668) e)
|
|> ((eq (+ X (+ Y Z)) (+ (+ X Y) Z)) <--)
|=============================
Step 13

? (eq (+ (+ c22669 Var200) (inv Var200)) (inv c22668))

1. (~ (eq (+ c22669 e) (inv c22668)))
2. (~ (eq c22669 (inv c22668)))
3. (eq (+ c22669 c22668) e)

> paramodulate right
=============================
|Step 14
|
|? (eq (+ c22669 Var200) Var213)
|
|1. (~ (eq (+ (+ c22669 Var200) (inv Var200)) (inv c22668)))
|2. (~ (eq (+ c22669 e) (inv c22668)))
|3. (~ (eq c22669 (inv c22668)))
|4. (eq (+ c22669 c22668) e)
|
|> hyp
|=============================
Step 15

? (eq (+ e (inv c22668)) (inv c22668))

1. (~ (eq (+ (+ c22669 c22668) (inv c22668)) (inv c22668)))
2. (~ (eq (+ c22669 e) (inv c22668)))
3. (~ (eq c22669 (inv c22668)))
4. (eq (+ c22669 c22668) e)

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

dr.mt...@gmail.com

unread,
Mar 15, 2023, 5:04:48 AM3/15/23
to Shen
The proof is still too long; however for another time.

M.

dr.mt...@gmail.com

unread,
Mar 15, 2023, 10:43:02 AM3/15/23
to Shen
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.

Reply all
Reply to author
Forward
0 new messages