HR1.11 is loaded. What shall we invent today?
| ?- data(non_assoc)::initialise(mace).
First Model of order: 1 2 e01
all ax1 reflexivity: (ax1=ax1).
all ax1 ax2 ax3 non_associativity: (ax1 * (ax2 * ax3) != (ax1 * ax2) * ax3).
1. *
2. non_assoc
3. element
4. pair
5. triple
6. equal_pair
7. equal_triple
8. trivial_entity
9. trivial_element
10. trivial_pair
11. trivial_triple
12. entity_equal_pair
13. non_number
14. non_entity
15. non_element
16. non_pair
17. non_triple
18. number
* | 0 | 1 |
--+---+---+
0 | 1 | 0 |
--+---+---+
1 | 1 | 0 |
--+---+---+
yes
| ?- set_mode(web_page).
***** Setting mode: web_page *****
yes
| ?- set_mode(exhaustive_web_page),construct(20,minutes),set_mode(random_web_page),construct(20,minutes),set_mode(novelty_web_page),construct(20,minutes),set_mode(bf_web_page),construct(2,hours).
***** Setting mode: exhaustive_web_page *****
1. (exists a b c (a*b=c)). max_proofs 1
2. all a ((exists b c (a*b=c))). max_proofs 1
3. all a b ((exists c (a*b=c))). max_proofs 1
(19) [N,a,b] s.t. (exists c (a*c=b)) " abraham pair 1 "
4. all a ((exists b c (b*a=c))). max_proofs 1
(20) [N,a,b] s.t. (exists c (c*a=b)) " ahlfors pair 1 "
(21) [N,a] s.t. (exists b c (b*c=a)) " akhiezer element 1 "
5. all a (((all ax1 ax2 (ax1 = ax2))) <-> (a*a=a)). max_proofs 4
6. all a b (((exists c (c*a=b))) <-> (a*a=b)).
all a b ( (exists c (c*a=b)) -> a*a=b ). sos
all a b ( a*a=b -> (exists c (c*a=b)) ). max_proofs 0
Mace generating counterexample of order: 1 2 e02
Checking whether conjectures are disproved: 6:yes(New Concept = 22),
(22) [N,a,b] s.t. a*a=b " alkhwarizmi pair 1 "
* | 0 | 1 |
--+---+---+
0 | 1 | 1 |
--+---+---+
1 | 0 | 0 |
--+---+---+
(23) [N,a,b] s.t. a*b=a " arbuthnot pair 1 "
(24) [N,a,b] s.t. a*b=b " archimedes pair 1 "
7. all a b ((a*b=a) <-> ((all c (c*a=b)))).
all a b ( a*b=a -> (all c (c*a=b)) ). sos
all a b ( (all c (c*a=b)) -> a*b=a ). sos
Mace generating counterexample of order: 1 2 3 e03
Checking whether conjectures are disproved: 7:yes(New Concept = 25),
(25) [N,a,b] s.t. (all c (c*a=b)) " archytas pair 1 "
* | 0 | 1 | 2 |
--+---+---+---+
0 | 1 | 0 | 0 |
--+---+---+---+
1 | 1 | 0 | 0 |
--+---+---+---+
2 | 1 | 0 | 0 |
--+---+---+---+
8. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b c (b*c=a)))). max_proofs 3
9. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b c (a*b=c))). max_proofs 2
10. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b c (b*a=c)))). max_proofs 2
11. all a b ((a*b=b) <-> ((all c (a*c=b)))).
all a b ( a*b=b -> (all c (a*c=b)) ). sos
all a b ( (all c (a*c=b)) -> a*b=b ). max_proofs 0
Mace generating counterexample of order: 1 2 3 e04
Checking whether conjectures are disproved: 11:yes(New Concept = 26),
(26) [N,a,b] s.t. (all c (a*c=b)) " aristarchus pair 1 "
* | 0 | 1 | 2 |
--+---+---+---+
0 | 1 | 1 | 2 |
--+---+---+---+
1 | 0 | 0 | 0 |
--+---+---+---+
2 | 0 | 0 | 0 |
--+---+---+---+
12. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b c (a*b=c)))). max_proofs 3
13. all a b (((all ax1 ax2 (ax1 = ax2))) <-> ((all c (a*b=c)))). max_proofs 3
(27) [N,a,b,c] s.t. -(a*b=c)
(28) [N,a] s.t. (exists b (a*b=a)) " abraham element 1 "
(29) [N,a] s.t. (all b ((exists c (b*c=a)))) " abraham element 2 "
(30) [N] s.t. (all a b ((exists c (a*c=b)))) " abraham non_assoc 1 "
(31) [N,a] s.t. (all b ((exists c (a*c=b)))) " abraham element 3 "
(32) [N,a] s.t. (exists b (b*a=a)) " ahlfors element 1 "
(33) [N,a] s.t. (all b ((exists c (c*b=a)))) " ahlfors element 2 "
(34) [N] s.t. (all a b ((exists c (c*a=b)))) " ahlfors non_assoc 1 "
(35) [N,a] s.t. (all b ((exists c (c*a=b)))) " ahlfors element 3 "
(36) [N] s.t. (all a ((exists b c (b*c=a)))) " akhiezer non_assoc 1 "
(37) [N,a] s.t. (exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) " akhiezer element 2 "
(38) [N,a] s.t. (exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) " akhiezer element 3 "
(39) [N,a] s.t. (exists b c (b*c=a)) & (all d ((exists e f (e*f=d)))) " akhiezer element 4 "
14. (exists a b (a*a=b)). max_proofs 1
15. all a ((exists b (a*a=b))). max_proofs 1
(40) [N,a] s.t. (exists b (b*b=a)) " alkhwarizmi element 1 "
16. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b (b*b=a)))). max_proofs 5
17. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b (a*a=b))). max_proofs 2
18. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b (a*a=b)))). max_proofs 3
(41) [N,a,b] s.t. -(a*a=b) " alkhwarizmi pair 2 "
(42) [N] s.t. (exists a b (a*b=a)) " arbuthnot non_assoc 1 "
19. all a (((exists b (a*b=a))) <-> ((exists c (a*c=a)))).
all a ( (exists b (a*b=a)) -> (exists c (a*c=a)) ). max_proofs 0
all a ( (exists b (a*b=a)) -> (exists c (a*c=a)) ). max_proofs 0
(43) [N,a] s.t. (exists b (b*a=b)) " arbuthnot element 1 "
20. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b (b*a=b)))). max_proofs 4
21. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b (a*b=a))). max_proofs 4
22. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b (a*b=a)))). max_proofs 4
(44) [N,a,b] s.t. -(a*b=a) " arbuthnot pair 2 "
(45) [N] s.t. (exists a b (a*b=b)) " archimedes non_assoc 1 "
(46) [N,a] s.t. (exists b (a*b=b)) " archimedes element 1 "
23. all a (((exists b (b*a=a))) <-> ((exists c (c*a=a)))).
all a ( (exists b (b*a=a)) -> (exists c (c*a=a)) ). max_proofs 0
all a ( (exists b (b*a=a)) -> (exists c (c*a=a)) ). max_proofs 0
24. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b (b*a=a)))). max_proofs 4
25. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b (a*b=b))). max_proofs 3
26. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b (a*b=b)))). max_proofs 3
(47) [N,a,b] s.t. -(a*b=b) " archimedes pair 2 "
27. ((exists a b (a*b=a))) <-> ((exists c d ((all e (e*c=d))))).
(exists a b (a*b=a)) -> (exists c d ((all e (e*c=d)))). sos
(exists a b ((all c (c*a=b)))) -> (exists d e (d*e=d)). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 e05
Checking whether conjectures are disproved: 27:yes(New Concept = 48),
(48) [N] s.t. (exists a b ((all c (c*a=b)))) " archytas non_assoc 1 "
* | 0 | 1 | 2 | 3 |
--+---+---+---+---+
0 | 1 | 2 | 1 | 1 |
--+---+---+---+---+
1 | 0 | 0 | 0 | 0 |
--+---+---+---+---+
2 | 0 | 0 | 0 | 0 |
--+---+---+---+---+
3 | 3 | 1 | 0 | 0 |
--+---+---+---+---+
(49) [N,a] s.t. (exists b ((all c (c*a=b)))) " archytas element 1 "
28. all a (((all b ((exists c (b*c=a))))) <-> ((exists d ((all e (e*d=a)))))).
all a ( (all b ((exists c (b*c=a)))) -> (exists d ((all e (e*d=a)))) ). sos
all a ( (exists b ((all c (c*b=a)))) -> (all d ((exists e (d*e=a)))) ). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
29. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b (b*a=a)))). max_proofs 4
30. ((exists a b (a*b=b))) <-> ((exists c d ((all e (c*e=d))))).
(exists a b (a*b=b)) -> (exists c d ((all e (c*e=d)))). sos
(exists a b ((all c (a*c=b)))) -> (exists d e (d*e=e)). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 e06
Checking whether conjectures are disproved: 28:yes(New Concept = 50),30:yes(New Concept = 51),
(50) [N,a] s.t. (exists b ((all c (c*b=a)))) " archytas element 2 "
(51) [N] s.t. (exists a b ((all c (a*c=b)))) " aristarchus non_assoc 1 "
* | 0 | 1 | 2 | 3 |
--+---+---+---+---+
0 | 1 | 0 | 0 | 3 |
--+---+---+---+---+
1 | 2 | 0 | 0 | 1 |
--+---+---+---+---+
2 | 1 | 0 | 0 | 0 |
--+---+---+---+---+
3 | 1 | 0 | 0 | 0 |
--+---+---+---+---+
(52) [N,a] s.t. (exists b ((all c (a*c=b)))) " aristarchus element 1 "
(53) [N,a] s.t. (exists b ((all c (b*c=a)))) " aristarchus element 2 "
31. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b (a*b=a)))). max_proofs 4
32. (exists a b c (-(a*b=c))). max_proofs 1
33. all a ((exists b c (-(a*b=c)))). max_proofs 2
34. all a b ((exists c (-(a*b=c)))). max_proofs 2
(54) [N,a,b] s.t. (exists c (-(a*c=b))) " aryabhata pair 1 "
35. all a ((exists b c (-(b*a=c)))). max_proofs 1
(55) [N,a,b] s.t. (exists c (-(c*a=b))) " bartholin pair 1 "
(56) [N,a] s.t. (exists b c (-(b*c=a))) " bhaskara element 1 "
(57) [N,a,b] s.t. (all c (-(c*a=b))) " bieberbach pair 1 "
(58) [N,a] s.t. (all b c (-(b*c=a))) " birkhoff element 1 "
36. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b c (-(a*b=c)))). max_proofs 2
37. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b c (-(b*a=c))))). max_proofs 2
(59) [N,a,b] s.t. (all c (-(a*c=b))) " bocher pair 1 "
38. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b c (-(a*b=c))))). max_proofs 2
39. all a b (((all ax1 ax2 (ax1 = ax2))) <-> ((all c (-(a*b=c))))). max_proofs 2
40. ((exists a b (a*b=a))) <-> ((exists c ((exists d (c*d=c))))).
(exists a b (a*b=a)) -> (exists c ((exists d (c*d=c)))). max_proofs 0
(exists a ((exists b (a*b=a)))) -> (exists c d (c*d=c)). max_proofs 0
41. ((all a b ((exists c (a*c=b))))) <-> ((all d ((exists e (d*e=d))))).
(all a b ((exists c (a*c=b)))) -> (all d ((exists e (d*e=d)))). max_proofs 0
(all a ((exists b (a*b=a)))) -> (all c d ((exists e (c*e=d)))). sos
Mace generating counterexample of order: 1 2 3 e07
Checking whether conjectures are disproved: 41:yes(New Concept = 60),
(60) [N] s.t. (all a ((exists b (a*b=a)))) " abraham non_assoc 2 "
* | 0 | 1 | 2 |
--+---+---+---+
0 | 1 | 0 | 0 |
--+---+---+---+
1 | 1 | 0 | 0 |
--+---+---+---+
2 | 2 | 0 | 0 |
--+---+---+---+
42. all a (((all b ((exists c (a*c=b))))) <-> ((exists d (a*d=a)) & (all e f ((exists g (e*g=f)))))).
all a ( (all b c ((exists d (b*d=c)))) -> (all e ((exists f (a*f=e)))) ). max_proofs 0
all a ( (exists b (a*b=a)) & (all c d ((exists e (c*e=d)))) -> (all f ((exists g (a*g=f)))) ).
---------------------------------------------
all a ( (all b c ((exists d (b*d=c)))) -> (all e ((exists f (a*f=e)))) ).
all a ( (all b ((exists c (a*c=b)))) -> (exists d (a*d=a)) ). max_proofs 0
all a ( (all b ((exists c (a*c=b)))) -> (all d e ((exists f (d*f=e)))) ). sos
Mace generating counterexample of order: 1 2 3 4 e08
Checking whether conjectures are disproved: 42:yes(New Concept = 61),
(61) [N,a] s.t. (exists b (a*b=a)) & (all c d ((exists e (c*e=d)))) " abraham element 4 "
* | 0 | 1 | 2 | 3 |
--+---+---+---+---+
0 | 1 | 0 | 3 | 2 |
--+---+---+---+---+
1 | 1 | 0 | 3 | 2 |
--+---+---+---+---+
2 | 1 | 0 | 0 | 0 |
--+---+---+---+---+
3 | 1 | 0 | 0 | 0 |
--+---+---+---+---+
43. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b (a*b=a)) & (all c d ((exists e (e*c=d)))))). max_proofs 6
(62) [N,a] s.t. (exists b (a*b=a)) & (all c ((exists d e (d*e=c)))) " abraham element 5 "
44. all a (((exists b (a*b=a))) <-> ((exists c (a*c=a)) & (exists d e (d*e=d)))).
all a ( (exists b (a*b=a)) -> (exists c d (c*d=c)) ). max_proofs 0
(63) [N,a] s.t. (exists b (a*b=a)) & (exists c d (c*d=d)) " abraham element 6 "
(64) [N,a] s.t. (exists b (a*b=a)) & (exists c d ((all e (e*c=d)))) " abraham element 7 "
(65) [N,a] s.t. (exists b (a*b=a)) & (exists c d ((all e (c*e=d)))) " abraham element 8 "
(66) [N,a] s.t. (exists b (a*b=a)) & (all c ((exists d (c*d=c)))) " abraham element 9 "
(67) [N,a] s.t. -((exists b (a*b=a))) " abraham element 10 "
45. ((exists a b ((all c (c*a=b))))) <-> ((exists d ((all e ((exists f (e*f=d))))))).
(exists a b ((all c (c*a=b)))) -> (exists d ((all e ((exists f (e*f=d)))))). max_proofs 0
(exists a ((all b ((exists c (b*c=a)))))) -> (exists d e ((all f (f*d=e)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
46. all a (((exists b c (b*c=a)) & (all d e ((exists f (d*f=e))))) <-> ((all g ((exists h (g*h=a)))) & (all i j ((exists k (i*k=j)))))).
all a ( (all b c ((exists d (b*d=c)))) -> (all e ((exists f (e*f=a)))) ). max_proofs 0
all a ( (exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) -> (all g ((exists h (g*h=a)))) ).
---------------------------------------------
all a ( (all b c ((exists d (b*d=c)))) -> (all e ((exists f (e*f=a)))) ).
all a ( (all b c ((exists d (b*d=c)))) -> (exists e f (e*f=a)) ). max_proofs 0
all a ( (all b ((exists c (b*c=a)))) -> (exists d e (d*e=a)) ). max_proofs 0
all a ( (all b ((exists c (b*c=a)))) & (all d e ((exists f (d*f=e)))) -> (exists g h (g*h=a)) ).
---------------------------------------------
all a ( (all b c ((exists d (b*d=c)))) -> (exists e f (e*f=a)) ).
47. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (b*c=a)))) & (all d e ((exists f (f*d=e)))))). max_proofs 6
(68) [N,a] s.t. (all b ((exists c (b*c=a)))) & (all d ((exists e f (e*f=d)))) " abraham element 11 "
48. all a (((all b ((exists c (b*c=a))))) <-> ((all d ((exists e (d*e=a)))) & (exists f g (f*g=f)))).
all a ( (all b ((exists c (b*c=a)))) -> (exists d e (d*e=d)) ). max_proofs 0
(69) [N,a] s.t. (all b ((exists c (b*c=a)))) & (exists d e (d*e=e)) " abraham element 12 "
49. all a (((all b ((exists c (b*c=a))))) <-> ((all d ((exists e (d*e=a)))) & (exists f g ((all h (h*f=g)))))).
all a ( (all b ((exists c (b*c=a)))) -> (exists d e ((all f (f*d=e)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
50. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (b*c=a)))) & (exists d e ((all f (d*f=e)))))). max_proofs 6
(70) [N,a] s.t. (all b ((exists c (b*c=a)))) & (all d ((exists e (d*e=d)))) " abraham element 13 "
51. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (a*c=b)))) & (all d e ((exists f (f*d=e))))). max_proofs 6
52. ((all a b ((exists c (a*c=b))))) <-> ((all d e ((exists f (d*f=e)))) & (all g ((exists h i (h*i=g))))).
(all a b ((exists c (a*c=b)))) -> (all d ((exists e f (e*f=d)))). max_proofs 0
53. ((all a b ((exists c (a*c=b))))) <-> ((all d e ((exists f (d*f=e)))) & (exists g h (g*h=g))).
(all a b ((exists c (a*c=b)))) -> (exists d e (d*e=d)). max_proofs 0
54. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (a*c=b)))) & (exists d e (d*e=e))). max_proofs 6
55. ((all a b ((exists c (a*c=b))))) <-> ((all d e ((exists f (d*f=e)))) & (exists g h ((all i (i*g=h))))).
(all a b ((exists c (a*c=b)))) -> (exists d e ((all f (f*d=e)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
56. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (a*c=b)))) & (exists d e ((all f (d*f=e))))). max_proofs 6
57. ((all a b ((exists c (a*c=b))))) <-> ((all d e ((exists f (d*f=e)))) & (all g ((exists h (g*h=g))))).
(all a b ((exists c (a*c=b)))) -> (all d ((exists e (d*e=d)))). max_proofs 0
(71) [N] s.t. (exists a ((all b ((exists c (a*c=b)))))) " abraham non_assoc 3 "
58. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (a*c=b)))) & (all d e ((exists f (f*d=e)))))). max_proofs 6
59. all a (((all b ((exists c (a*c=b))))) <-> ((all d ((exists e (a*e=d)))) & (all f ((exists g h (g*h=f)))))).
all a ( (all b ((exists c (a*c=b)))) -> (all d ((exists e f (e*f=d)))) ). max_proofs 0
60. all a (((all b ((exists c (a*c=b))))) <-> ((all d ((exists e (a*e=d)))) & (exists f g (f*g=f)))).
all a ( (all b ((exists c (a*c=b)))) -> (exists d e (d*e=d)) ).
---------------------------------------------
all a ( (all b ((exists c (a*c=b)))) -> (exists d (a*d=a)) ).
all a ( (exists b (a*b=a)) -> (exists c d (c*d=c)) ).
61. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (a*c=b)))) & (exists d e (d*e=e)))). sos
Mace generating counterexample of order: 1 2 3 4 e09
Checking whether conjectures are disproved: 45:no,49:no,55:no,61:yes(New Concept = 72),
(72) [N,a] s.t. (all b ((exists c (a*c=b)))) & (exists d e (d*e=e)) " abraham element 14 "
* | 0 | 1 | 2 | 3 |
--+---+---+---+---+
0 | 1 | 0 | 2 | 3 |
--+---+---+---+---+
1 | 2 | 0 | 3 | 1 |
--+---+---+---+---+
2 | 1 | 0 | 0 | 0 |
--+---+---+---+---+
3 | 1 | 0 | 0 | 0 |
--+---+---+---+---+
62. all a (((all b ((exists c (a*c=b))))) <-> ((all d ((exists e (a*e=d)))) & (exists f g ((all h (h*f=g)))))).
all a ( (all b ((exists c (a*c=b)))) -> (exists d e ((all f (f*d=e)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
63. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (a*c=b)))) & (exists d e ((all f (d*f=e)))))). sos
Mace generating counterexample of order: 1 2 3 4 e10
Checking whether conjectures are disproved: 45:no,49:no,55:no,62:yes(New Concept = 73),63:yes(New Concept = 74),
(73) [N,a] s.t. (all b ((exists c (a*c=b)))) & (exists d e ((all f (f*d=e)))) " abraham element 15 "
(74) [N,a] s.t. (all b ((exists c (a*c=b)))) & (exists d e ((all f (d*f=e)))) " abraham element 16 "
* | 0 | 1 | 2 | 3 |
--+---+---+---+---+
0 | 1 | 2 | 1 | 1 |
--+---+---+---+---+
1 | 0 | 0 | 0 | 0 |
--+---+---+---+---+
2 | 0 | 0 | 0 | 0 |
--+---+---+---+---+
3 | 3 | 1 | 2 | 0 |
--+---+---+---+---+
64. all a (((exists b (a*b=a)) & (all c d ((exists e (c*e=d))))) <-> ((all f ((exists g (a*g=f)))) & (all h ((exists i (h*i=h)))))).
all a ( (all b c ((exists d (b*d=c)))) -> (all e ((exists f (e*f=e)))) ). max_proofs 0
all a ( (exists b (a*b=a)) & (all c d ((exists e (c*e=d)))) -> (all f ((exists g (f*g=f)))) ).
---------------------------------------------
all a ( (all b c ((exists d (b*d=c)))) -> (all e ((exists f (e*f=e)))) ).
all a ( (all b ((exists c (b*c=b)))) -> (exists d (a*d=a)) ). max_proofs 0
all a ( (all b ((exists c (a*c=b)))) & (all d ((exists e (d*e=d)))) -> (exists f (a*f=a)) ).
---------------------------------------------
all a ( (all b ((exists c (a*c=b)))) -> (exists d (a*d=a)) ).
all a ( (all b ((exists c (a*c=b)))) & (all d ((exists e (d*e=d)))) -> (all f g ((exists h (f*h=g)))) ). sos
Mace generating counterexample of order: 1 2 3 4 e11
Checking whether conjectures are disproved: 45:no,49:no,55:no,64:yes(New Concept = 75),
(75) [N,a] s.t. (all b ((exists c (a*c=b)))) & (all d ((exists e (d*e=d)))) " abraham element 17 "
* | 0 | 1 | 2 | 3 |
--+---+---+---+---+
0 | 1 | 0 | 3 | 2 |
--+---+---+---+---+
1 | 1 | 0 | 3 | 2 |
--+---+---+---+---+
2 | 1 | 0 | 0 | 2 |
--+---+---+---+---+
3 | 1 | 0 | 3 | 0 |
--+---+---+---+---+
65. ((exists a b (a*b=b))) <-> ((exists c ((exists d (d*c=c))))).
(exists a b (a*b=b)) -> (exists c ((exists d (d*c=c)))). max_proofs 0
(exists a ((exists b (b*a=a)))) -> (exists c d (c*d=d)). max_proofs 0
(76) [N] s.t. (all a ((exists b (b*a=a)))) " ahlfors non_assoc 2 "
66. all a (((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))) <-> ((exists g (g*a=a)) & (all h i ((exists j (j*h=i)))))).
all a ( (all b c ((exists d (d*b=c)))) -> (exists e (e*a=a)) ). max_proofs 0
all a ( (exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) -> (exists g (g*a=a)) ).
---------------------------------------------
all a ( (all b c ((exists d (d*b=c)))) -> (exists e (e*a=a)) ).
all a ( (all b c ((exists d (d*b=c)))) -> (exists e f (e*f=a)) ). max_proofs 0
all a ( (exists b (b*a=a)) -> (exists c d (c*d=a)) ). max_proofs 0
all a ( (exists b (b*a=a)) & (all c d ((exists e (e*c=d)))) -> (exists f g (f*g=a)) ).
---------------------------------------------
all a ( (all b c ((exists d (d*b=c)))) -> (exists e f (e*f=a)) ).
67. all a (((exists b (b*a=a))) <-> ((exists c (c*a=a)) & (all d ((exists e f (e*f=d)))))).
all a ( (exists b (b*a=a)) -> (all c ((exists d e (d*e=c)))) ). sos
Mace generating counterexample of order: 1 2 3 e12
Checking whether conjectures are disproved: 45:no,49:no,55:no,67:yes(New Concept = 77),
(77) [N,a] s.t. (exists b (b*a=a)) & (all c ((exists d e (d*e=c)))) " ahlfors element 4 "
* | 0 | 1 | 2 |
--+---+---+---+
0 | 1 | 1 | 1 |
--+---+---+---+
1 | 0 | 0 | 0 |
--+---+---+---+
2 | 0 | 0 | 0 |
--+---+---+---+
(78) [N,a] s.t. (exists b (b*a=a)) & (exists c d (c*d=c)) " ahlfors element 5 "
68. all a (((exists b (b*a=a))) <-> ((exists c (c*a=a)) & (exists d e (d*e=e)))).
all a ( (exists b (b*a=a)) -> (exists c d (c*d=d)) ). max_proofs 0
(79) [N,a] s.t. (exists b (b*a=a)) & (exists c d ((all e (e*c=d)))) " ahlfors element 6 "
(80) [N,a] s.t. (exists b (b*a=a)) & (exists c d ((all e (c*e=d)))) " ahlfors element 7 "
69. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b (b*a=a)) & (all c ((exists d (c*d=c)))))). max_proofs 6
(81) [N,a] s.t. (exists b (b*a=a)) & (exists c ((all d ((exists e (c*e=d)))))) " ahlfors element 8 "
(82) [N,a] s.t. (exists b (b*a=a)) & (all c ((exists d (d*c=c)))) " ahlfors element 9 "
(83) [N,a] s.t. -((exists b (b*a=a))) " ahlfors element 10 "
70. ((exists a b ((all c (a*c=b))))) <-> ((exists d ((all e ((exists f (f*e=d))))))).
(exists a b ((all c (a*c=b)))) -> (exists d ((all e ((exists f (f*e=d)))))). max_proofs 0
(exists a ((all b ((exists c (c*b=a)))))) -> (exists d e ((all f (d*f=e)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
71. all a (((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))) <-> ((all g ((exists h (h*g=a)))) & (all i j ((exists k (k*i=j)))))).
all a ( (all b c ((exists d (d*b=c)))) -> (all e ((exists f (f*e=a)))) ). max_proofs 0
all a ( (exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) -> (all g ((exists h (h*g=a)))) ).
---------------------------------------------
all a ( (all b c ((exists d (d*b=c)))) -> (all e ((exists f (f*e=a)))) ).
all a ( (all b ((exists c (c*b=a)))) -> (exists d e (d*e=a)) ). max_proofs 0
all a ( (all b ((exists c (c*b=a)))) & (all d e ((exists f (f*d=e)))) -> (exists g h (g*h=a)) ).
---------------------------------------------
all a ( (all b c ((exists d (d*b=c)))) -> (exists e f (e*f=a)) ).
(84) [N,a] s.t. (all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d)))) " ahlfors element 11 "
(85) [N,a] s.t. (all b ((exists c (c*b=a)))) & (exists d e (d*e=d)) " ahlfors element 12 "
72. all a (((all b ((exists c (c*b=a))))) <-> ((all d ((exists e (e*d=a)))) & (exists f g (f*g=g)))).
all a ( (all b ((exists c (c*b=a)))) -> (exists d e (d*e=e)) ). max_proofs 0
73. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (c*b=a)))) & (exists d e ((all f (f*d=e)))))). max_proofs 6
74. all a (((all b ((exists c (c*b=a))))) <-> ((all d ((exists e (e*d=a)))) & (exists f g ((all h (f*h=g)))))).
all a ( (all b ((exists c (c*b=a)))) -> (exists d e ((all f (d*f=e)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
75. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (c*b=a)))) & (all d ((exists e (d*e=d)))))). max_proofs 6
(86) [N,a] s.t. (all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (d*f=e)))))) " ahlfors element 13 "
(87) [N,a] s.t. (all b ((exists c (c*b=a)))) & (all d ((exists e (e*d=d)))) " ahlfors element 14 "
76. ((all a b ((exists c (c*a=b))))) <-> ((all d e ((exists f (f*d=e)))) & (all g ((exists h i (h*i=g))))).
(all a b ((exists c (c*a=b)))) -> (all d ((exists e f (e*f=d)))). max_proofs 0
77. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (c*a=b)))) & (exists d e (d*e=d))). max_proofs 6
78. ((all a b ((exists c (c*a=b))))) <-> ((all d e ((exists f (f*d=e)))) & (exists g h (g*h=h))).
(all a b ((exists c (c*a=b)))) -> (exists d e (d*e=e)). max_proofs 0
79. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (c*a=b)))) & (exists d e ((all f (f*d=e))))). max_proofs 4
80. ((all a b ((exists c (c*a=b))))) <-> ((all d e ((exists f (f*d=e)))) & (exists g h ((all i (g*i=h))))).
(all a b ((exists c (c*a=b)))) -> (exists d e ((all f (d*f=e)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
81. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (c*a=b)))) & (all d ((exists e (d*e=d))))). max_proofs 6
82. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (d*f=e))))))). max_proofs 6
83. ((all a b ((exists c (c*a=b))))) <-> ((all d e ((exists f (f*d=e)))) & (all g ((exists h (h*g=g))))).
(all a b ((exists c (c*a=b)))) -> (all d ((exists e (e*d=d)))). max_proofs 0
84. ((all a b ((exists c (c*a=b))))) <-> ((exists d ((all e ((exists f (f*d=e))))))).
(all a b ((exists c (c*a=b)))) -> (exists d ((all e ((exists f (f*d=e)))))). max_proofs 0
(exists a ((all b ((exists c (c*a=b)))))) -> (all d e ((exists f (f*d=e)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
85. all a (((all b ((exists c (c*a=b))))) <-> ((all d ((exists e (e*a=d)))) & (all f ((exists g h (g*h=f)))))).
all a ( (all b ((exists c (c*a=b)))) -> (all d ((exists e f (e*f=d)))) ). max_proofs 0
86. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (c*a=b)))) & (exists d e (d*e=d)))). sos
Mace generating counterexample of order: 1 2 3 4 e13
Checking whether conjectures are disproved: 45:no,49:no,55:no,70:no,74:no,80:no,84:yes(New Concept = 88),86:yes(New Concept = 89),
(88) [N] s.t. (exists a ((all b ((exists c (c*a=b)))))) " ahlfors non_assoc 3 "
(89) [N,a] s.t. (all b ((exists c (c*a=b)))) & (exists d e (d*e=d)) " ahlfors element 15 "
* | 0 | 1 | 2 | 3 |
--+---+---+---+---+
0 | 1 | 0 | 0 | 3 |
--+---+---+---+---+
1 | 2 | 0 | 0 | 1 |
--+---+---+---+---+
2 | 1 | 0 | 0 | 2 |
--+---+---+---+---+
3 | 1 | 0 | 0 | 0 |
--+---+---+---+---+
87. all a (((all b ((exists c (c*a=b))))) <-> ((all d ((exists e (e*a=d)))) & (exists f g (f*g=g)))).
all a ( (all b ((exists c (c*a=b)))) -> (exists d e (d*e=e)) ). max_proofs 0
88. all a (((all b ((exists c (c*a=b)))) & (exists d e (d*e=d))) <-> ((all f ((exists g (g*a=f)))) & (exists h i ((all j (j*h=i)))))).
all a ( (all b ((exists c (c*a=b)))) & (exists d e (d*e=d)) -> (exists f g ((all h (h*f=g)))) ). sos
all a ( (exists b c ((all d (d*b=c)))) -> (exists e f (e*f=e)) ). max_proofs 0
all a ( (all b ((exists c (c*a=b)))) & (exists d e ((all f (f*d=e)))) -> (exists g h (g*h=g)) ).
---------------------------------------------
all a ( (exists b c ((all d (d*b=c)))) -> (exists e f (e*f=e)) ).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(90) [N,a] s.t. (all b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e)))) " ahlfors element 16 "
89. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (c*a=b)))) & (all d ((exists e (d*e=d)))))). max_proofs 6
90. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (d*f=e)))))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
91. all a (((all b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e))))) <-> ((all g ((exists h (h*a=g)))) & (all i ((exists j (j*i=i)))))).
all a ( (all b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e)))) -> (all g ((exists h (h*g=g)))) ). sos
all a ( (all b ((exists c (c*a=b)))) & (all d ((exists e (e*d=d)))) -> (exists f g ((all h (f*h=g)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(91) [N] s.t. (all a ((exists b c (b*c=a)))) & (exists d e (d*e=d)) " akhiezer non_assoc 2 "
(92) [N] s.t. (all a ((exists b c (b*c=a)))) & (exists d e (d*e=e)) " akhiezer non_assoc 3 "
(93) [N] s.t. (all a ((exists b c (b*c=a)))) & (exists d e ((all f (f*d=e)))) " akhiezer non_assoc 4 "
(94) [N] s.t. (all a ((exists b c (b*c=a)))) & (exists d e ((all f (d*f=e)))) " akhiezer non_assoc 5 "
92. ((all a ((exists b (a*b=a))))) <-> ((all c ((exists d e (d*e=c)))) & (all f ((exists g (f*g=f))))).
(all a ((exists b (a*b=a)))) -> (all c ((exists d e (d*e=c)))). max_proofs 0
93. ((exists a ((all b ((exists c (a*c=b))))))) <-> ((all d ((exists e f (e*f=d)))) & (exists g ((all h ((exists i (g*i=h))))))).
(exists a ((all b ((exists c (a*c=b)))))) -> (all d ((exists e f (e*f=d)))). max_proofs 0
94. ((all a ((exists b (b*a=a))))) <-> ((all c ((exists d e (d*e=c)))) & (all f ((exists g (g*f=f))))).
(all a ((exists b (b*a=a)))) -> (all c ((exists d e (d*e=c)))). max_proofs 0
***** Setting mode: random_web_page *****
95. ((exists a ((all b ((exists c (c*a=b))))))) <-> ((all d ((exists e f (e*f=d)))) & (exists g ((all h ((exists i (i*g=h))))))).
(exists a ((all b ((exists c (c*a=b)))))) -> (all d ((exists e f (e*f=d)))). max_proofs 0
Top Ten Sorted Concepts: [71,78,24,63,19,34,77,70,56,84]
Top Ten Sorted Conjectures: [89,82,81,75,69,77,73,58,56,54]
Summary for session in non_assoc theory:
---------------------
Number of concepts: 94
Number of Conjectures: 95
Number of Models: 13
Largest Model Size: 4
Number of Categorisations: 60
Number of Theorems: 71
Number of Open Conjectures: 8
Number of Prime Implicants: 47
Average Proof Length: 2.323943661971831
Average Surprisingness: 1.704225352112676
Average P.I. Proof Length: 0.0
Number of Otter Proofs: 47
Number of HR Proofs: 11
----------------------
96. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a ((all b ((exists c (a*c=b)))))) & (exists d ((all e ((exists f (f*d=e))))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
97. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a ((all b ((exists c (a*c=b)))))) & (all d ((exists e (e*d=d))))). max_proofs 6
98. all a (((exists b (b*a=a)) & (exists c d ((all e (e*c=d))))) <-> ((exists f (f*a=a)) & (exists g h (g*h=g)) & (exists i j ((all k (k*i=j)))))).
all a ( (exists b (b*a=a)) & (exists c d ((all e (e*c=d)))) -> (exists f g (f*g=f)) ).
---------------------------------------------
all a ( (exists b c ((all d (d*b=c)))) -> (exists e f (e*f=e)) ).
(95) [N,a] s.t. (exists b (b*a=a)) & (exists c d (c*d=c)) & (exists e f ((all g (e*g=f)))) " ahlfors element 17 "
99. all a (((all b ((exists c (c*a=b)))) & (exists d e (d*e=d))) <-> ((exists f (f*a=a)) & (exists g h (g*h=g)) & (exists i ((all j ((exists k (k*i=j)))))))).
all a ( (exists b (b*a=a)) & (exists c d (c*d=c)) & (exists e ((all f ((exists g (g*e=f)))))) -> (all h ((exists i (i*a=h)))) ). sos
all a ( (all b ((exists c (c*a=b)))) -> (exists d (d*a=a)) ). max_proofs 0
all a ( (all b ((exists c (c*a=b)))) & (exists d e (d*e=d)) -> (exists f (f*a=a)) ).
---------------------------------------------
all a ( (all b ((exists c (c*a=b)))) -> (exists d (d*a=a)) ).
all a ( (all b ((exists c (c*a=b)))) -> (exists d ((all e ((exists f (f*d=e)))))) ). max_proofs 0
all a ( (all b ((exists c (c*a=b)))) & (exists d e (d*e=d)) -> (exists f ((all g ((exists h (h*f=g)))))) ).
---------------------------------------------
all a ( (all b ((exists c (c*a=b)))) -> (exists d ((all e ((exists f (f*d=e)))))) ).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
100. all a (((exists b (b*a=a)) & (exists c d (c*d=c))) <-> ((exists e (e*a=a)) & (exists f g (f*g=f)) & (exists h i (h*i=i)))).
all a ( (exists b (b*a=a)) & (exists c d (c*d=c)) -> (exists e f (e*f=f)) ).
---------------------------------------------
all a ( (exists b (b*a=a)) -> (exists c d (c*d=d)) ).
101. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b (b*a=a)) & (exists c d (c*d=c)) & (all e ((exists f (f*e=e)))))). max_proofs 6
102. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b (b*a=a)) & (exists c d (c*d=c))))). max_proofs 6
(96) [N,a] s.t. -((exists b (b*a=a)) & (exists c d (c*d=c))) " ahlfors element 18 "
(97) [N] s.t. (exists a ((exists b (b*a=a)) & (exists c d (c*d=c)))) " ahlfors non_assoc 4 "
103. all a (((all b ((exists c (a*c=b)))) & (exists d e (d*e=e))) <-> ((exists f (a*f=a)) & (exists g h (g*h=h)) & (exists i ((all j ((exists k (i*k=j)))))))).
all a ( (exists b (a*b=a)) & (exists c d (c*d=d)) & (exists e ((all f ((exists g (e*g=f)))))) -> (all h ((exists i (a*i=h)))) ). sos
all a ( (all b ((exists c (a*c=b)))) & (exists d e (d*e=e)) -> (exists f (a*f=a)) ).
---------------------------------------------
all a ( (all b ((exists c (a*c=b)))) -> (exists d (a*d=a)) ).
all a ( (all b ((exists c (a*c=b)))) -> (exists d ((all e ((exists f (d*f=e)))))) ). max_proofs 0
all a ( (all b ((exists c (a*c=b)))) & (exists d e (d*e=e)) -> (exists f ((all g ((exists h (f*h=g)))))) ).
---------------------------------------------
all a ( (all b ((exists c (a*c=b)))) -> (exists d ((all e ((exists f (d*f=e)))))) ).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
104. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b (a*b=a)) & (exists c d (c*d=d)) & (all e ((exists f (e*f=e)))))). max_proofs 6
(98) [N,a] s.t. (exists b (a*b=a)) & (exists c d (c*d=d)) & (exists e f ((all g (g*e=f)))) " abraham element 18 "
105. all a (((exists b (a*b=a)) & (exists c d ((all e (c*e=d))))) <-> ((exists f (a*f=a)) & (exists g h (g*h=h)) & (exists i j ((all k (i*k=j)))))).
all a ( (exists b c ((all d (b*d=c)))) -> (exists e f (e*f=f)) ). max_proofs 0
all a ( (exists b (a*b=a)) & (exists c d ((all e (c*e=d)))) -> (exists f g (f*g=g)) ).
---------------------------------------------
all a ( (exists b c ((all d (b*d=c)))) -> (exists e f (e*f=f)) ).
106. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b (a*b=a)) & (exists c d (c*d=d))))). max_proofs 6
(99) [N,a] s.t. -((exists b (a*b=a)) & (exists c d (c*d=d))) " abraham element 19 "
Top Ten Sorted Concepts: [33,58,53,54,40,64,20,19,98,27]
Top Ten Sorted Conjectures: [106,102,97,89,82,81,75,69,104,101]
107. all a (((all b ((exists c (c*b=a)))) & (exists d e (d*e=d))) <-> ((all f ((exists g (g*f=a)))) & (exists h ((exists i (i*h=h)) & (exists j k (j*k=j)))))).
all a ( (all b ((exists c (c*b=a)))) & (exists d e (d*e=d)) -> (exists f ((exists g (g*f=f)) & (exists h i (h*i=h)))) ). max_proofs 0
all a ( (exists b ((exists c (c*b=b)) & (exists d e (d*e=d)))) -> (exists f g (f*g=f)) ). max_proofs 0
all a ( (all b ((exists c (c*b=a)))) & (exists d ((exists e (e*d=d)) & (exists f g (f*g=f)))) -> (exists h i (h*i=h)) ).
---------------------------------------------
all a ( (exists b ((exists c (c*b=b)) & (exists d e (d*e=d)))) -> (exists f g (f*g=f)) ).
108. all a (((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))) <-> ((all g ((exists h (h*g=a)))) & (exists i ((all j ((exists k (k*i=j)))))))).
all a ( (all b c ((exists d (d*b=c)))) -> (exists e ((all f ((exists g (g*e=f)))))) ). max_proofs 0
all a ( (exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) -> (exists g ((all h ((exists i (i*g=h)))))) ).
---------------------------------------------
all a ( (all b c ((exists d (d*b=c)))) -> (exists e ((all f ((exists g (g*e=f)))))) ).
all a ( (exists b ((all c ((exists d (d*b=c)))))) -> (exists e f (e*f=a)) ). max_proofs 0
all a ( (all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e)))))) -> (exists g h (g*h=a)) ).
---------------------------------------------
all a ( (all b ((exists c (c*b=a)))) -> (exists d e (d*e=a)) ).
all a ( (all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e)))))) -> (all g h ((exists i (i*g=h)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(100) [N] s.t. (exists a ((all b c (-(b*c=a))))) " birkhoff non_assoc 1 "
109. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b c (-(b*c=a))) & (exists d ((all e ((exists f (d*f=e)))))))). max_proofs 3
110. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b c (-(b*c=a))) & (all d ((exists e (d*e=d)))))). max_proofs 3
111. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b c (-(b*c=a))) & (exists d ((all e ((exists f (f*d=e)))))))). max_proofs 3
112. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b c (-(b*c=a))) & (all d ((exists e (e*d=d)))))). max_proofs 3
113. ((all a b ((exists c (c*a=b))))) <-> ((all d ((exists e ((all f (e*f=d))))))).
(all a b ((exists c (c*a=b)))) -> (all d ((exists e ((all f (e*f=d)))))). sos
(all a ((exists b ((all c (b*c=a)))))) -> (all d e ((exists f (f*d=e)))). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(101) [N,a] s.t. (exists b ((all c (b*c=a)))) & (exists d ((all e ((exists f (d*f=e)))))) " aristarchus element 3 "
114. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b ((all c (b*c=a)))) & (all d ((exists e (d*e=d)))))). max_proofs 9
115. all a (((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))) <-> ((exists g ((all h (g*h=a)))) & (exists i ((all j ((exists k (k*i=j)))))))).
all a ( (exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) -> (exists g ((all h (g*h=a)))) ). sos
all a ( (exists b ((all c (b*c=a)))) -> (exists d e (d*e=a)) ). max_proofs 0
all a ( (exists b ((all c (b*c=a)))) & (exists d ((all e ((exists f (f*d=e)))))) -> (exists g h (g*h=a)) ).
---------------------------------------------
all a ( (exists b ((all c ((exists d (d*b=c)))))) -> (exists e f (e*f=a)) ).
all a ( (exists b ((all c (b*c=a)))) & (exists d ((all e ((exists f (f*d=e)))))) -> (all g h ((exists i (i*g=h)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
116. all a (((all b ((exists c (c*b=a)))) & (all d ((exists e (e*d=d))))) <-> ((exists f ((all g (f*g=a)))) & (all h ((exists i (i*h=h)))))).
all a ( (all b ((exists c (c*b=a)))) & (all d ((exists e (e*d=d)))) -> (exists f ((all g (f*g=a)))) ). sos
all a ( (exists b ((all c (b*c=a)))) -> (all d ((exists e (e*d=a)))) ). max_proofs 0
all a ( (exists b ((all c (b*c=a)))) & (all d ((exists e (e*d=d)))) -> (all f ((exists g (g*f=a)))) ).
---------------------------------------------
all a ( (exists b ((all c (b*c=a)))) -> (all d ((exists e (e*d=a)))) ).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(102) [N,a] s.t. (exists b ((all c (b*c=a)))) & (exists d ((all e f (-(e*f=d))))) " aristarchus element 4 "
117. all a ((exists b (-(a*b=a)))). max_proofs 2
(103) [N,a] s.t. (all b ((exists c (-(b*c=a))))) " aryabhata element 1 "
118. ((exists a b ((all c (c*a=b))))) <-> ((all d e ((exists f (-(d*f=e)))))).
(exists a b ((all c (c*a=b)))) -> (all d e ((exists f (-(d*f=e))))). max_proofs 4
(all a b ((exists c (-(a*c=b))))) -> (exists d e ((all f (f*d=e)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(104) [N,a] s.t. (all b ((exists c (-(a*c=b))))) " aryabhata element 2 "
Top Ten Sorted Concepts: [28,103,84,71,88,93,66,70,37,35]
Top Ten Sorted Conjectures: [114,106,102,97,89,82,81,75,69,104]
(105) [N,a] s.t. (exists b (a*b=a)) & (exists c ((all d ((exists e (c*e=d)))))) " abraham element 20 "
(106) [N,a] s.t. (exists b (a*b=a)) & (exists c ((all d ((exists e (e*c=d)))))) " abraham element 21 "
(107) [N,a] s.t. (exists b (a*b=a)) & (exists c ((all d e (-(d*e=c))))) " abraham element 22 "
119. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b (a*b=a)) & (all c ((exists d (d*c=c)))))). max_proofs 6
(108) [N] s.t. (exists a ((all b ((exists c (-(b*c=a))))))) " aryabhata non_assoc 1 "
(109) [N,a] s.t. -((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d))))) " ahlfors element 19 "
Top Ten Sorted Concepts: [30,52,39,44,68,22,81,43,70,99]
Top Ten Sorted Conjectures: [114,106,102,97,119,89,82,81,75,69]
120. ((all a b ((exists c (a*c=b))))) <-> ((all d e ((exists f (d*f=e)))) & (exists g ((all h ((exists i (g*i=h))))))).
(all a b ((exists c (a*c=b)))) -> (exists d ((all e ((exists f (d*f=e)))))). max_proofs 0
121. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (a*c=b)))) & (all d ((exists e (e*d=d))))). max_proofs 6
122. ((all a b ((exists c (a*c=b))))) <-> ((all d e ((exists f (d*f=e)))) & (exists g ((all h ((exists i (-(h*i=g)))))))).
(all a b ((exists c (a*c=b)))) -> (exists d ((all e ((exists f (-(e*f=d))))))). max_proofs 2
123. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (a*c=b)))) & (exists d ((all e f (-(e*f=d)))))). max_proofs 3
124. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (a*c=b)))) & (exists d ((all e ((exists f (f*d=e))))))). max_proofs 6
(110) [N,a] s.t. (exists b ((all c (a*c=b)))) & (exists d ((all e ((exists f (d*f=e)))))) " aristarchus element 5 "
125. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b ((all c (a*c=b)))) & (all d ((exists e (d*e=d)))))). max_proofs 8
(111) [N,a] s.t. (exists b ((all c (a*c=b)))) & (all d ((exists e (e*d=d)))) " aristarchus element 6 "
(112) [N,a] s.t. (exists b ((all c (a*c=b)))) & (exists d ((all e ((exists f (-(e*f=d))))))) " aristarchus element 7 "
(113) [N,a] s.t. (exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))) " aristarchus element 8 "
126. all a (((all b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e))))) <-> ((exists g ((all h (a*h=g)))) & (exists i ((all j ((exists k (k*i=j)))))))).
all a ( (all b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e)))) -> (exists g ((all h (a*h=g)))) ). sos
all a ( (all b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e)))) -> (exists g ((all h ((exists i (i*g=h)))))) ).
---------------------------------------------
all a ( (all b ((exists c (c*a=b)))) -> (exists d ((all e ((exists f (f*d=e)))))) ).
all a ( (exists b ((all c (a*c=b)))) & (exists d ((all e ((exists f (f*d=e)))))) -> (all g ((exists h (h*a=g)))) ). sos
all a ( (exists b ((all c (a*c=b)))) -> (exists d e ((all f (d*f=e)))) ). max_proofs 0
all a ( (exists b ((all c (a*c=b)))) & (exists d ((all e ((exists f (f*d=e)))))) -> (exists g h ((all i (g*i=h)))) ).
---------------------------------------------
all a ( (exists b ((all c (a*c=b)))) -> (exists d e ((all f (d*f=e)))) ).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(114) [N] s.t. (all a ((exists b ((all c (a*c=b)))))) " aristarchus non_assoc 2 "
Top Ten Sorted Concepts: [63,85,43,44,51,19,34,100,101,25]
Top Ten Sorted Conjectures: [114,125,106,102,97,124,121,119,89,82]
127. ((exists a ((exists b (b*a=a)) & (exists c d (c*d=c))))) <-> ((exists e ((exists f (e*f=e)) & (exists g h (g*h=h))))).
(exists a ((exists b (b*a=a)) & (exists c d (c*d=c)))) -> (exists e ((exists f (e*f=e)) & (exists g h (g*h=h)))). max_proofs 0
(exists a ((exists b (a*b=a)) & (exists c d (c*d=d)))) -> (exists e ((exists f (f*e=e)) & (exists g h (g*h=g)))). max_proofs 0
(115) [N] s.t. (exists a ((all b ((exists c (c*b=a)))) & (exists d e (d*e=d)))) " ahlfors non_assoc 5 "
(116) [N,a] s.t. -((all b ((exists c (c*b=a)))) & (exists d e (d*e=d))) " ahlfors element 20 "
128. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((all b ((exists c (c*b=a)))) & (exists d e (d*e=d))))). max_proofs 6
129. all a (((all b ((exists c (c*b=a)))) & (exists d e (d*e=d))) <-> ((all f ((exists g (g*f=a)))) & (exists h i (h*i=h)) & (exists j k ((all l (j*l=k)))))).
all a ( (all b ((exists c (c*b=a)))) & (exists d e (d*e=d)) -> (exists f g ((all h (f*h=g)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
130. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (c*b=a)))) & (exists d e (d*e=d)) & (exists f ((all g ((exists h (h*f=g)))))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
131. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (c*b=a)))) & (exists d e (d*e=d)) & (exists f g ((all h (h*f=g)))))). max_proofs 6
132. all a (((all b ((exists c (c*b=a)))) & (exists d e (d*e=d))) <-> ((all f ((exists g (g*f=a)))) & (exists h i (h*i=h)) & (exists j k (j*k=k)))).
all a ( (all b ((exists c (c*b=a)))) & (exists d e (d*e=d)) -> (exists f g (f*g=g)) ).
---------------------------------------------
all a ( (all b ((exists c (c*b=a)))) -> (exists d e (d*e=e)) ).
133. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (c*b=a)))) & (exists d e (d*e=d)) & (all f ((exists g (g*f=f)))))). max_proofs 6
(117) [N] s.t. (all a ((exists b (b*a=b)))) " arbuthnot non_assoc 2 "
(118) [N,a] s.t. (exists b (b*a=b)) & (exists c d ((all e (c*e=d)))) " arbuthnot element 2 "
(119) [N,a] s.t. (exists b (b*a=b)) & (exists c ((all d e (-(d*e=c))))) " arbuthnot element 3 "
Top Ten Sorted Concepts: [110,97,95,38,55,115,104,49,21,67]
Top Ten Sorted Conjectures: [114,125,128,106,102,131,133,97,124,121]
134. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b ((all c (a*c=b)))) & (exists d ((all e ((exists f (d*f=e))))))))). max_proofs 8
(120) [N] s.t. (exists a ((exists b ((all c (a*c=b)))) & (exists d ((all e ((exists f (d*f=e)))))))) " aristarchus non_assoc 3 "
(121) [N,a] s.t. -((exists b ((all c (a*c=b)))) & (exists d ((all e ((exists f (d*f=e))))))) " aristarchus element 9 "
135. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b ((all c (a*c=b)))) & (exists d ((all e ((exists f (d*f=e)))))) & (all g ((exists h ((all i (g*i=h)))))))). max_proofs 6
136. ((all a b ((exists c (c*a=b))))) <-> ((all d ((exists e f (e*f=d)) & (all g h ((exists i (i*g=h))))))).
(all a b ((exists c (c*a=b)))) -> (all d ((exists e f (e*f=d)) & (all g h ((exists i (i*g=h)))))). max_proofs 0
(all a ((exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))))) -> (all g h ((exists i (i*g=h)))). max_proofs 0
137. ((all a b ((exists c (c*a=b))))) <-> ((exists d ((exists e f (e*f=d)) & (all g h ((exists i (i*g=h))))))).
(all a b ((exists c (c*a=b)))) -> (exists d ((exists e f (e*f=d)) & (all g h ((exists i (i*g=h)))))). max_proofs 0
(exists a ((exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))))) -> (all g h ((exists i (i*g=h)))). max_proofs 0
(122) [N,a] s.t. -((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))) " akhiezer element 5 "
138. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) & (exists g ((all h ((exists i (g*i=h)))))))). max_proofs 6
139. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) & (all g ((exists h (g*h=g)))))). max_proofs 6
140. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) & (exists g h ((all i (i*g=h)))))). max_proofs 4
141. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) & (exists g ((all h i (-(h*i=g))))))). max_proofs 5
142. all a (((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))) <-> ((exists g h (g*h=a)) & (all i j ((exists k (k*i=j)))) & (all l ((exists m (m*l=l)))))).
all a ( (all b c ((exists d (d*b=c)))) -> (all e ((exists f (f*e=e)))) ). max_proofs 0
all a ( (exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) -> (all g ((exists h (h*g=g)))) ).
---------------------------------------------
all a ( (all b c ((exists d (d*b=c)))) -> (all e ((exists f (f*e=e)))) ).
143. all a (((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))) <-> ((exists g h (g*h=a)) & (all i j ((exists k (k*i=j)))) & (exists l m (l*m=m)))).
all a ( (all b c ((exists d (d*b=c)))) -> (exists e f (e*f=f)) ).
---------------------------------------------
all a ( (all b c ((exists d (d*b=c)))) -> (exists e (e*a=a)) ).
all a ( (exists b (b*a=a)) -> (exists c d (c*d=d)) ).
all a ( (exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) -> (exists g h (g*h=h)) ).
---------------------------------------------
all a ( (all b c ((exists d (d*b=c)))) -> (exists e (e*a=a)) ).
all a ( (exists b (b*a=a)) -> (exists c d (c*d=d)) ).
144. all a (((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))) <-> ((exists g h (g*h=a)) & (all i j ((exists k (k*i=j)))) & (exists l ((all m ((exists n (n*l=m)))))))).
145. all a (((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))) <-> ((exists g h (g*h=a)) & (all i j ((exists k (k*i=j)))) & (all l ((exists m ((all n (l*n=m)))))))).
all a ( (exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) -> (all g ((exists h ((all i (g*i=h)))))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
146. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) & (all g ((exists h (h*g=h)))))). max_proofs 5
147. all a (((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))) <-> ((exists g h (g*h=a)) & (all i j ((exists k (k*i=j)))) & (exists l m ((all n (l*n=m)))))).
all a ( (exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) -> (exists g h ((all i (g*i=h)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
148. all a (((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))) <-> ((exists g h (g*h=a)) & (all i j ((exists k (k*i=j)))) & (all l ((exists m n (m*n=l)))))).
all a ( (all b c ((exists d (d*b=c)))) -> (all e ((exists f g (f*g=e)))) ). max_proofs 0
all a ( (exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) -> (all g ((exists h i (h*i=g)))) ).
---------------------------------------------
all a ( (all b c ((exists d (d*b=c)))) -> (all e ((exists f g (f*g=e)))) ).
149. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) & (exists g h (g*h=g)))). max_proofs 6
(123) [N,a] s.t. (exists b (-(b*a=a))) " bartholin element 1 "
(124) [N,a] s.t. (all b ((exists c (-(c*b=a))))) " bartholin element 2 "
Top Ten Sorted Concepts: [60,19,84,80,97,85,117,72,90,35]
Top Ten Sorted Conjectures: [114,134,125,128,106,102,139,138,131,133]
150. ((all a ((exists b (a*b=a))))) <-> ((all c ((exists d (c*d=c)))) & (all e ((exists f (f*e=f))))).
(all a ((exists b (a*b=a)))) -> (all c ((exists d (d*c=d)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
151. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b (a*b=a)))) & (exists c ((all d ((exists e (e*c=d))))))). max_proofs 6
152. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b (a*b=a)))) & (all c ((exists d ((all e (c*e=d))))))). max_proofs 8
(125) [N] s.t. (all a ((exists b (a*b=a)))) & (exists c ((all d ((exists e (c*e=d)))))) " abraham non_assoc 4 "
153. ((all a ((exists b (a*b=a))))) <-> ((all c ((exists d (c*d=c)))) & (exists e ((all f ((exists g (-(f*g=e)))))))).
(all a ((exists b (a*b=a)))) -> (exists c ((all d ((exists e (-(d*e=c))))))). max_proofs 5
154. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b (a*b=a)))) & (all c ((exists d (d*c=c))))). max_proofs 6
155. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b (a*b=a)))) & (exists c ((all d e (-(d*e=c)))))). max_proofs 3
156. ((all a b ((exists c (c*a=b))))) <-> ((all d ((all e ((exists f (f*e=d)))) & (all g ((exists h i (h*i=g))))))).
(all a b ((exists c (c*a=b)))) -> (all d ((all e ((exists f (f*e=d)))) & (all g ((exists h i (h*i=g)))))). max_proofs 0
(all a ((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d)))))) -> (all g h ((exists i (i*g=h)))). max_proofs 0
157. ((all a ((exists b c (b*c=a)))) & (exists d e ((all f (d*f=e))))) <-> ((exists g ((all h ((exists i (i*h=g)))) & (all j ((exists k l (k*l=j))))))).
(all a ((exists b c (b*c=a)))) & (exists d e ((all f (d*f=e)))) -> (exists g ((all h ((exists i (i*h=g)))) & (all j ((exists k l (k*l=j)))))). max_proofs 0
(exists a ((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d)))))) -> (all g ((exists h i (h*i=g)))). max_proofs 0
(exists a ((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d)))))) -> (exists g h ((all i (g*i=h)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
158. all a (((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d))))) <-> ((all g ((exists h (h*g=a)))) & (all i ((exists j k (j*k=i)))) & (exists l m ((all n (l*n=m)))))).
all a ( (all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d)))) -> (exists g h ((all i (g*i=h)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
159. all a (((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d))))) <-> ((all g ((exists h (h*g=a)))) & (all i ((exists j k (j*k=i)))) & (exists l m (l*m=m)))).
all a ( (all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d)))) -> (exists g h (g*h=h)) ).
---------------------------------------------
all a ( (all b ((exists c (c*b=a)))) -> (exists d e (d*e=e)) ).
160. all a (((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))) <-> ((all g ((exists h (h*g=a)))) & (all i ((exists j k (j*k=i)))) & (exists l ((all m ((exists n (n*l=m)))))))).
all a ( (all b ((exists c d (c*d=b)))) & (exists e ((all f ((exists g (g*e=f)))))) -> (exists h i (h*i=a)) ).
---------------------------------------------
all a ( (exists b ((all c ((exists d (d*b=c)))))) -> (exists e f (e*f=a)) ).
all a ( (all b ((exists c d (c*d=b)))) -> (exists e f (e*f=a)) ). max_proofs 0
all a ( (all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d)))) -> (exists g h (g*h=a)) ).
---------------------------------------------
all a ( (all b ((exists c (c*b=a)))) -> (exists d e (d*e=a)) ).
all a ( (all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d)))) & (exists g ((all h ((exists i (i*g=h)))))) -> (exists j k (j*k=a)) ).
---------------------------------------------
all a ( (all b ((exists c (c*b=a)))) -> (exists d e (d*e=a)) ).
all a ( (all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d)))) & (exists g ((all h ((exists i (i*g=h)))))) -> (all j k ((exists l (l*j=k)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
161. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d)))) & (exists g h ((all i (i*g=h)))))). max_proofs 6
162. all a (((all b ((exists c (c*b=a)))) & (exists d e (d*e=d))) <-> ((all f ((exists g (g*f=a)))) & (all h ((exists i j (i*j=h)))) & (exists k l (k*l=k)))).
all a ( (all b ((exists c (c*b=a)))) & (exists d e (d*e=d)) -> (all f ((exists g h (g*h=f)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
Summary for session in non_assoc theory:
---------------------
Number of concepts: 125
Number of Conjectures: 162
Number of Models: 13
Largest Model Size: 4
Number of Categorisations: 77
Number of Theorems: 120
Number of Open Conjectures: 24
Number of Prime Implicants: 76
Average Proof Length: 2.8916666666666666
Average Surprisingness: 2.4166666666666665
Average P.I. Proof Length: 0.14473684210526316
Number of Otter Proofs: 76
Number of HR Proofs: 34
----------------------
***** Setting mode: novelty_web_page *****
163. all a (((all b ((exists c (c*b=a)))) & (all d ((exists e (e*d=d))))) <-> ((all f ((exists g (g*f=a)))) & (all h ((exists i j (i*j=h)))) & (all k ((exists l (l*k=k)))))).
all a ( (all b ((exists c (c*b=b)))) -> (all d ((exists e f (e*f=d)))) ). max_proofs 0
all a ( (all b ((exists c (c*b=a)))) & (all d ((exists e (e*d=d)))) -> (all f ((exists g h (g*h=f)))) ).
---------------------------------------------
all a ( (all b ((exists c (c*b=b)))) -> (all d ((exists e f (e*f=d)))) ).
Top Ten Sorted Concepts: [124,122,121,117,116,114,112,109,105,104]
Top Ten Sorted Conjectures: [114,134,152,125,128,106,102,161,139,138]
(126) [N] s.t. (exists a ((all b ((exists c (-(c*b=a))))))) " bartholin non_assoc 1 "
164. ((exists a ((all b ((exists c (-(b*c=a)))))))) <-> ((exists d (-((exists e f (e*f=d)) & (all g h ((exists i (i*g=h)))))))).
(exists a ((all b ((exists c (-(b*c=a))))))) -> (exists d (-((exists e f (e*f=d)) & (all g h ((exists i (i*g=h))))))). sos
(exists a (-((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))))) -> (exists g ((all h ((exists i (-(h*i=g))))))). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
165. ((exists a ((all b ((exists c (-(b*c=a)))))))) <-> ((all d (-((exists e f (e*f=d)) & (all g h ((exists i (i*g=h)))))))).
(exists a ((all b ((exists c (-(b*c=a))))))) -> (all d (-((exists e f (e*f=d)) & (all g h ((exists i (i*g=h))))))). sos
(all a (-((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))))) -> (exists g ((all h ((exists i (-(h*i=g))))))). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(127) [N] s.t. (all a ((exists b (b*a=b)))) & (exists c ((all d ((exists e (-(e*d=c))))))) " arbuthnot non_assoc 3 "
166. (exists a (-((all b ((exists c (c*b=a)))) & (exists d e (d*e=d))))). max_proofs 3
(128) [N] s.t. (all a (-((all b ((exists c (c*b=a)))) & (exists d e (d*e=d))))) " ahlfors non_assoc 6 "
167. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b ((all c (a*c=b)))))) & (all d ((exists e (e*d=e))))). max_proofs 6
168. ((all a ((exists b ((all c (a*c=b))))))) <-> ((all d ((exists e ((all f (d*f=e)))))) & (exists g ((all h ((exists i (-(i*h=g)))))))).
(all a ((exists b ((all c (a*c=b)))))) -> (exists d ((all e ((exists f (-(f*e=d))))))). max_proofs 3
169. ((exists a ((all b ((exists c (-(b*c=a)))))))) <-> ((exists d (-((all e ((exists f (f*e=d)))) & (all g ((exists h i (h*i=g)))))))).
(exists a ((all b ((exists c (-(b*c=a))))))) -> (exists d (-((all e ((exists f (f*e=d)))) & (all g ((exists h i (h*i=g))))))). sos
(exists a (-((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d))))))) -> (exists g ((all h ((exists i (-(h*i=g))))))). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(129) [N] s.t. (all a (-((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d))))))) " ahlfors non_assoc 7 "
(130) [N,a] s.t. -((exists b (a*b=a)) & (exists c ((all d ((exists e (c*e=d))))))) " abraham element 23 "
Top Ten Sorted Concepts: [130,127,124,122,121,117,116,114,112,109]
Top Ten Sorted Conjectures: [114,134,152,125,166,128,106,102,161,139]
(131) [N] s.t. (exists a (-((exists b (a*b=a)) & (exists c ((all d ((exists e (c*e=d))))))))) " abraham non_assoc 5 "
(132) [N] s.t. (all a (-((exists b (a*b=a)) & (exists c ((all d ((exists e (c*e=d))))))))) " abraham non_assoc 6 "
170. ((exists a ((all b ((exists c (a*c=b))))))) <-> ((exists d ((exists e (d*e=d)) & (exists f ((all g ((exists h (f*h=g))))))))).
(exists a ((all b ((exists c (a*c=b)))))) -> (exists d ((exists e (d*e=d)) & (exists f ((all g ((exists h (f*h=g)))))))). max_proofs 0
(exists a ((exists b (a*b=a)) & (exists c ((all d ((exists e (c*e=d)))))))) -> (exists f ((all g ((exists h (f*h=g)))))). max_proofs 0
171. ((all a ((exists b (a*b=a)))) & (exists c ((all d ((exists e (c*e=d))))))) <-> ((all f ((exists g (f*g=f)) & (exists h ((all i ((exists j (h*j=i))))))))).
(all a ((exists b (a*b=a)))) & (exists c ((all d ((exists e (c*e=d)))))) -> (all f ((exists g (f*g=f)) & (exists h ((all i ((exists j (h*j=i)))))))). max_proofs 0
(all a ((exists b (a*b=a)) & (exists c ((all d ((exists e (c*e=d)))))))) -> (all f ((exists g (f*g=f)))). max_proofs 0
(all a ((exists b (a*b=a)) & (exists c ((all d ((exists e (c*e=d)))))))) -> (exists f ((all g ((exists h (f*h=g)))))). max_proofs 0
(133) [N] s.t. (exists a ((all b ((exists c (-(a*c=b))))))) " aryabhata non_assoc 2 "
(134) [N,a] s.t. (all b ((exists c (-(a*c=b))))) & (all d ((exists e (e*d=e)))) " aryabhata element 3 "
172. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (-(a*c=b))))) & (all d ((exists e ((all f (d*f=e)))))))). max_proofs 3
(135) [N,a] s.t. (all b ((exists c (-(a*c=b))))) & (exists d ((all e ((exists f (-(f*e=d))))))) " aryabhata element 4 "
Top Ten Sorted Concepts: [135,134,130,127,124,122,121,117,116,112]
Top Ten Sorted Conjectures: [114,134,152,125,166,128,106,102,161,139]
(136) [N,a] s.t. -((all b ((exists c (-(a*c=b))))) & (exists d ((all e ((exists f (-(f*e=d)))))))) " aryabhata element 5 "
(137) [N] s.t. (exists a ((all b ((exists c (-(a*c=b))))) & (exists d ((all e ((exists f (-(f*e=d))))))))) " aryabhata non_assoc 3 "
(138) [N] s.t. (all a ((all b ((exists c (-(a*c=b))))) & (exists d ((all e ((exists f (-(f*e=d))))))))) " aryabhata non_assoc 4 "
(139) [N,a] s.t. (all b ((exists c (-(c*b=a))))) & (exists d ((all e ((exists f (-(d*f=e))))))) " bartholin element 3 "
173. ((all a ((exists b (b*a=b))))) <-> ((all c ((exists d (d*c=d)))) & (exists e ((all f ((exists g (-(e*g=f)))))))).
(all a ((exists b (b*a=b)))) -> (exists c ((all d ((exists e (-(c*e=d))))))). max_proofs 4
174. all a (((all b ((exists c (-(a*c=b)))))) <-> ((all d ((exists e (-(a*e=d))))) & (exists f ((all g ((exists h (-(g*h=f))))))))).
all a ( (all b ((exists c (-(a*c=b))))) -> (exists d ((all e ((exists f (-(e*f=d))))))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
175. (exists a (-((exists b (a*b=a)) & (exists c d (c*d=d))))). max_proofs 3
(140) [N] s.t. (all a (-((exists b (a*b=a)) & (exists c d (c*d=d))))) " abraham non_assoc 7 "
Top Ten Sorted Concepts: [139,138,137,136,135,134,130,127,124,122]
Top Ten Sorted Conjectures: [114,134,152,125,175,166,128,106,102,161]
(141) [N,a] s.t. -((all b ((exists c (-(c*b=a))))) & (exists d ((all e ((exists f (-(d*f=e)))))))) " bartholin element 4 "
176. ((exists a ((all b ((exists c (-(a*c=b))))) & (exists d ((all e ((exists f (-(f*e=d)))))))))) <-> ((exists g ((all h ((exists i (-(i*h=g))))) & (exists j ((all k ((exists l (-(j*l=k)))))))))).
(exists a ((all b ((exists c (-(a*c=b))))) & (exists d ((all e ((exists f (-(f*e=d))))))))) -> (exists g ((all h ((exists i (-(i*h=g))))) & (exists j ((all k ((exists l (-(j*l=k))))))))). max_proofs 1
(exists a ((all b ((exists c (-(c*b=a))))) & (exists d ((all e ((exists f (-(d*f=e))))))))) -> (exists g ((all h ((exists i (-(g*i=h))))) & (exists j ((all k ((exists l (-(l*k=j))))))))). max_proofs 1
(142) [N] s.t. (all a ((all b ((exists c (-(c*b=a))))) & (exists d ((all e ((exists f (-(d*f=e))))))))) " bartholin non_assoc 2 "
177. (exists a (-((exists b (b*a=a)) & (exists c d (c*d=c))))). max_proofs 3
178. ((all a (-((exists b (a*b=a)) & (exists c d (c*d=d)))))) <-> ((all e (-((exists f (f*e=e)) & (exists g h (g*h=g)))))).
(all a (-((exists b (a*b=a)) & (exists c d (c*d=d))))) -> (all e (-((exists f (f*e=e)) & (exists g h (g*h=g))))). max_proofs 0
(all a (-((exists b (b*a=a)) & (exists c d (c*d=c))))) -> (all e (-((exists f (e*f=e)) & (exists g h (g*h=h))))). max_proofs 0
(143) [N,a] s.t. -((exists b (b*a=a)) & (exists c d (c*d=c))) & (exists e ((exists f (f*e=e)) & (exists g h (g*h=g)))) " ahlfors element 21 "
(144) [N] s.t. -((all a ((exists b c (b*c=a)))) & (exists d e ((all f (f*d=e))))) " akhiezer non_assoc 6 "
179. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b c (b*c=a)))) & (exists d e ((all f (f*d=e)))) & (exists g h ((all i (g*i=h))))). max_proofs 6
180. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b c (b*c=a)))) & (exists d e ((all f (f*d=e)))) & -((all g ((exists h i (h*i=g)))) & (exists j k ((all l (l*j=k)))))). max_proofs 5
(145) [N] s.t. -((all a ((exists b c (b*c=a)))) & (exists d e (d*e=e))) " akhiezer non_assoc 7 "
Top Ten Sorted Concepts: [142,141,139,138,137,136,135,134,130,127]
Top Ten Sorted Conjectures: [114,134,152,125,177,175,166,128,106,102]
(146) [N] s.t. -((all a ((exists b c (b*c=a)))) & (exists d e (d*e=d))) " akhiezer non_assoc 8 "
181. ((all a ((exists b (a*b=a))))) <-> ((all c ((exists d e (d*e=c)))) & (exists f g (f*g=f)) & (all h ((exists i (i*h=i))))).
(all a ((exists b c (b*c=a)))) & (exists d e (d*e=d)) & (all f ((exists g (g*f=g)))) -> (all h ((exists i (h*i=h)))). sos
(all a ((exists b (a*b=a)))) -> (exists c d (c*d=c)). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
182. ((exists a ((exists b (b*a=a)) & (exists c d (c*d=c))))) <-> ((all e ((exists f g (f*g=e)))) & (exists h i (h*i=h)) & (exists j k (j*k=k))).
(exists a b (a*b=a)) & (exists c d (c*d=d)) -> (exists e ((exists f (f*e=e)) & (exists g h (g*h=g)))). max_proofs 0
(all a ((exists b c (b*c=a)))) & (exists d e (d*e=d)) & (exists f g (f*g=g)) -> (exists h ((exists i (i*h=h)) & (exists j k (j*k=j)))).
---------------------------------------------
(exists a b (a*b=a)) & (exists c d (c*d=d)) -> (exists e ((exists f (f*e=e)) & (exists g h (g*h=g)))).
(exists a ((exists b (b*a=a)) & (exists c d (c*d=c)))) -> (all e ((exists f g (f*g=e)))). sos
(exists a ((exists b (b*a=a)) & (exists c d (c*d=c)))) -> (exists e f (e*f=e)). max_proofs 0
(exists a ((exists b (b*a=a)) & (exists c d (c*d=c)))) -> (exists e f (e*f=f)). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
183. ((exists a ((all b ((exists c (c*b=a)))) & (exists d e (d*e=d))))) <-> ((all f ((exists g h (g*h=f)))) & (exists i j (i*j=i)) & (exists k l ((all m (k*m=l))))).
(exists a b (a*b=a)) & (exists c d ((all e (c*e=d)))) -> (exists f ((all g ((exists h (h*g=f)))) & (exists i j (i*j=i)))). max_proofs 0
(all a ((exists b c (b*c=a)))) & (exists d e (d*e=d)) & (exists f g ((all h (f*h=g)))) -> (exists i ((all j ((exists k (k*j=i)))) & (exists l m (l*m=l)))).
---------------------------------------------
(exists a b (a*b=a)) & (exists c d ((all e (c*e=d)))) -> (exists f ((all g ((exists h (h*g=f)))) & (exists i j (i*j=i)))).
(exists a ((all b ((exists c (c*b=a)))) & (exists d e (d*e=d)))) -> (all f ((exists g h (g*h=f)))). sos
(exists a ((all b ((exists c (c*b=a)))) & (exists d e (d*e=d)))) -> (exists f g (f*g=f)). max_proofs 0
(exists a ((all b ((exists c (c*b=a)))) & (exists d e (d*e=d)))) -> (exists f g ((all h (f*h=g)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
184. ((all a ((exists b c (b*c=a)))) & (exists d e ((all f (f*d=e))))) <-> ((all g ((exists h i (h*i=g)))) & (exists j k (j*k=j)) & (exists l m ((all n (n*l=m))))).
(exists a b ((all c (c*a=b)))) -> (exists d e (d*e=d)). max_proofs 0
(all a ((exists b c (b*c=a)))) & (exists d e ((all f (f*d=e)))) -> (exists g h (g*h=g)).
---------------------------------------------
(exists a b ((all c (c*a=b)))) -> (exists d e (d*e=d)).
185. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b c (b*c=a)))) & (exists d e (d*e=d)) & -((all f ((exists g h (g*h=f)))) & (exists i j (i*j=i)))). max_proofs 6
186. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a ((all b ((exists c (c*a=b)))))) & (all d ((exists e (e*d=e))))). max_proofs 5
(147) [N] s.t. (exists a ((all b ((exists c (c*a=b)))))) & (exists d ((all e ((exists f (-(d*f=e))))))) " ahlfors non_assoc 8 "
187. ((all a b ((exists c (c*a=b))))) <-> ((exists d ((all e ((exists f (f*d=e)))))) & (all g ((exists h ((all i (g*i=h))))))).
(all a b ((exists c (c*a=b)))) -> (exists d ((all e ((exists f (f*d=e)))))). max_proofs 0
(all a b ((exists c (c*a=b)))) -> (all d ((exists e ((all f (d*f=e)))))). sos
(exists a ((all b ((exists c (c*a=b)))))) & (all d ((exists e ((all f (d*f=e)))))) -> (all g h ((exists i (i*g=h)))). max_proofs 2
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
188. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a ((all b ((exists c (c*a=b)))))) & (exists d ((all e f (-(e*f=d)))))). max_proofs 3
189. ((exists a ((all b ((exists c (c*a=b))))))) <-> ((exists d ((all e ((exists f (f*d=e)))))) & (exists g ((all h ((exists i (-(i*h=g)))))))).
(exists a ((all b ((exists c (c*a=b)))))) -> (exists d ((all e ((exists f (-(f*e=d))))))). max_proofs 2
190. ((exists a ((all b ((exists c (c*a=b)))))) & (exists d ((all e ((exists f (-(d*f=e)))))))) <-> ((exists g ((all h ((exists i (i*g=h)))))) & (exists j ((all k ((exists l (-(k*l=j)))))))).
(exists a ((all b ((exists c (c*a=b)))))) & (exists d ((all e ((exists f (-(e*f=d))))))) -> (exists g ((all h ((exists i (-(g*i=h))))))). max_proofs 2
(exists a ((all b ((exists c (c*a=b)))))) & (exists d ((all e ((exists f (-(d*f=e))))))) -> (exists g ((all h ((exists i (-(h*i=g))))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(148) [N,a] s.t. -((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c)))))) " arbuthnot element 4 "
(149) [N] s.t. (all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c))))))) " arbuthnot non_assoc 4 "
191. ((all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c)))))))) <-> ((exists f ((exists g (g*f=g)) & (exists h ((all i j (-(i*j=h)))))))).
(all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c))))))) -> (exists f ((exists g (g*f=g)) & (exists h ((all i j (-(i*j=h))))))). max_proofs 1
(exists a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c))))))) -> (all f ((exists g (g*f=g)) & (exists h ((all i j (-(i*j=h))))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
192. all a (((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c)))))) <-> ((exists f (f*a=f)) & (exists g ((all h i (-(h*i=g))))) & (all j ((exists k (k*j=k)))))).
all a ( (exists b (b*a=b)) & (exists c ((all d e (-(d*e=c))))) -> (all f ((exists g (g*f=g)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
193. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b ((all c (a*c=b)))))) & (exists d ((all e ((exists f (-(d*f=e)))))))). max_proofs 3
(150) [N,a] s.t. -((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d)))))) " aristarchus element 10 "
Top Ten Sorted Concepts: [150,148,142,141,139,138,137,136,135,134]
Top Ten Sorted Conjectures: [114,134,152,125,177,175,166,128,106,102]
(151) [N] s.t. (all a (-((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d)))))))) " aristarchus non_assoc 4 "
194. ((all a (-((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))))))) <-> ((exists g (-((exists h ((all i (g*i=h)))) & (exists j ((all k l (-(k*l=j))))))))).
(all a (-((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d)))))))) -> (exists g (-((exists h ((all i (g*i=h)))) & (exists j ((all k l (-(k*l=j)))))))). max_proofs 1
(exists a (-((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d)))))))) -> (all g (-((exists h ((all i (g*i=h)))) & (exists j ((all k l (-(k*l=j)))))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(152) [N] s.t. (all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))))) " aristarchus non_assoc 5 "
195. ((all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d)))))))) <-> ((exists g ((exists h ((all i (g*i=h)))) & (exists j ((all k l (-(k*l=j)))))))).
(all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))))) -> (exists g ((exists h ((all i (g*i=h)))) & (exists j ((all k l (-(k*l=j))))))). max_proofs 1
(exists a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))))) -> (all g ((exists h ((all i (g*i=h)))) & (exists j ((all k l (-(k*l=j))))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
196. all a (((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d)))))) <-> ((exists g ((all h (a*h=g)))) & (exists i ((all j k (-(j*k=i))))) & (all l ((exists m ((all n (l*n=m)))))))).
all a ( (exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))) -> (all g ((exists h ((all i (g*i=h)))))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(153) [N,a] s.t. (all b ((exists c (-(b*c=a))))) & (all d ((exists e (e*d=e)))) " aryabhata element 6 "
(154) [N,a] s.t. (all b ((exists c (-(b*c=a))))) & (exists d ((all e ((exists f (-(d*f=e))))))) " aryabhata element 7 "
(155) [N,a] s.t. (all b ((exists c (-(b*c=a))))) & (all d ((exists e ((all f (d*f=e)))))) " aryabhata element 8 "
Top Ten Sorted Concepts: [150,148,142,141,139,138,137,136,135,130]
Top Ten Sorted Conjectures: [114,134,152,125,177,175,166,128,106,102]
(156) [N,a] s.t. -((all b ((exists c (-(b*c=a))))) & (exists d ((all e ((exists f (-(d*f=e)))))))) " aryabhata element 9 "
197. ((exists a b ((all c (c*a=b))))) <-> ((all d ((all e ((exists f (-(e*f=d))))) & (exists g ((all h ((exists i (-(g*i=h)))))))))).
(exists a b ((all c (c*a=b)))) -> (all d ((all e ((exists f (-(e*f=d))))) & (exists g ((all h ((exists i (-(g*i=h))))))))). max_proofs 11
(all a ((all b ((exists c (-(b*c=a))))) & (exists d ((all e ((exists f (-(d*f=e))))))))) -> (exists g h ((all i (i*g=h)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
198. ((exists a ((all b ((exists c (-(a*c=b)))))))) <-> ((exists d ((all e ((exists f (-(e*f=d))))) & (exists g ((all h ((exists i (-(g*i=h)))))))))).
(exists a ((all b ((exists c (-(a*c=b))))))) -> (exists d ((all e ((exists f (-(e*f=d))))) & (exists g ((all h ((exists i (-(g*i=h))))))))). sos
(exists a ((all b ((exists c (-(b*c=a))))) & (exists d ((all e ((exists f (-(d*f=e))))))))) -> (exists g ((all h ((exists i (-(g*i=h))))))). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
Summary for session in non_assoc theory:
---------------------
Number of concepts: 156
Number of Conjectures: 198
Number of Models: 13
Largest Model Size: 4
Number of Categorisations: 89
Number of Theorems: 140
Number of Open Conjectures: 40
Number of Prime Implicants: 107
Average Proof Length: 2.8857142857142857
Average Surprisingness: 2.6785714285714284
Average P.I. Proof Length: 0.37383177570093457
Number of Otter Proofs: 107
Number of HR Proofs: 38
----------------------
***** Setting mode: bf_web_page *****
(157) [N,a] s.t. (all b ((exists c (-(b*c=a))))) & (exists d ((all e ((exists f (-(f*e=d))))))) " aryabhata element 10 "
Top Ten Sorted Concepts: [110,146,99,116,144,93,96,60,100,139]
Top Ten Sorted Conjectures: [197,114,134,152,125,128,106,102,179,161]
199. ((all a ((exists b (a*b=a))))) <-> ((all c ((exists d (c*d=c)))) & (exists e ((all f ((exists g (-(e*g=f)))))))).
(all a ((exists b (a*b=a)))) -> (exists c ((all d ((exists e (-(c*e=d))))))). max_proofs 6
(158) [N] s.t. (all a ((exists b (a*b=a)))) & (exists c ((all d ((exists e (-(e*d=c))))))) " abraham non_assoc 8 "
200. ((all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d)))))))) <-> ((exists g ((all h i (-(h*i=g))))) & (all j ((exists k ((all l (j*l=k))))))).
(exists a ((all b c (-(b*c=a))))) & (all d ((exists e ((all f (d*f=e)))))) -> (all g ((exists h ((all i (g*i=h)))) & (exists j ((all k l (-(k*l=j))))))). max_proofs 1
(all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))))) -> (exists g ((all h i (-(h*i=g))))). max_proofs 0
(all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))))) -> (all g ((exists h ((all i (g*i=h)))))). max_proofs 0
201. ((all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c)))))))) <-> ((exists f ((all g h (-(g*h=f))))) & (all i ((exists j (j*i=j))))).
(exists a ((all b c (-(b*c=a))))) & (all d ((exists e (e*d=e)))) -> (all f ((exists g (g*f=g)) & (exists h ((all i j (-(i*j=h))))))). max_proofs 1
(all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c))))))) -> (exists f ((all g h (-(g*h=f))))). max_proofs 0
(all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c))))))) -> (all f ((exists g (g*f=g)))). max_proofs 0
202. ((all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c)))))))) <-> ((exists f ((all g h (-(g*h=f))))) & (exists i ((all j ((exists k (-(i*k=j)))))))).
(exists a ((all b c (-(b*c=a))))) & (exists d ((all e ((exists f (-(d*f=e))))))) -> (all g ((exists h (h*g=h)) & (exists i ((all j k (-(j*k=i))))))). sos
(all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c))))))) -> (exists f ((all g ((exists h (-(f*h=g))))))).
---------------------------------------------
(all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c))))))) -> (all f ((exists g (g*f=g)))).
(all a ((exists b (b*a=b)))) -> (exists c ((all d ((exists e (-(c*e=d))))))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
203. ((exists a ((all b c (-(b*c=a)))))) <-> ((exists d ((all e f (-(e*f=d))))) & (exists g ((all h ((exists i (-(i*h=g)))))))).
(exists a ((all b c (-(b*c=a))))) -> (exists d ((all e ((exists f (-(f*e=d))))))). max_proofs 0
204. ((exists a ((all b c (-(b*c=a)))))) <-> ((exists d ((all e f (-(e*f=d))))) & (exists g ((all h ((exists i (-(h*i=g)))))))).
(exists a ((all b c (-(b*c=a))))) -> (exists d ((all e ((exists f (-(e*f=d))))))). max_proofs 0
205. all a (((all b ((exists c (-(b*c=a))))) & (all d ((exists e ((all f (d*f=e))))))) <-> ((all g h (-(g*h=a))) & (all i ((exists j ((all k (i*k=j)))))))).
all a ( (all b c (-(b*c=a))) -> (all d ((exists e (-(d*e=a))))) ). max_proofs 0
all a ( (all b c (-(b*c=a))) & (all d ((exists e ((all f (d*f=e)))))) -> (all g ((exists h (-(g*h=a))))) ).
---------------------------------------------
all a ( (all b c (-(b*c=a))) -> (all d ((exists e (-(d*e=a))))) ).
all a ( (all b ((exists c (-(b*c=a))))) & (all d ((exists e ((all f (d*f=e)))))) -> (all g h (-(g*h=a))) ). max_proofs 2
(159) [N,a] s.t. (all b c (-(b*c=a))) & (all d ((exists e (e*d=e)))) " birkhoff element 2 "
206. all a (((all b c (-(b*c=a))) & (all d ((exists e (e*d=e))))) <-> ((all f g (-(f*g=a))) & (exists h ((all i ((exists j (-(h*j=i))))))))).
all a ( (all b ((exists c (c*b=c)))) -> (exists d ((all e ((exists f (-(d*f=e))))))) ). max_proofs 4
all a ( (all b c (-(b*c=a))) & (all d ((exists e (e*d=e)))) -> (exists f ((all g ((exists h (-(f*h=g))))))) ).
---------------------------------------------
all a ( (all b ((exists c (c*b=c)))) -> (exists d ((all e ((exists f (-(d*f=e))))))) ).
all a ( (all b c (-(b*c=a))) & (exists d ((all e ((exists f (-(d*f=e))))))) -> (all g ((exists h (h*g=h)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
207. all a (((all b c (-(b*c=a)))) <-> ((all d e (-(d*e=a))) & (exists f ((all g ((exists h (-(h*g=f))))))))).
all a ( (all b c (-(b*c=a))) -> (exists d ((all e ((exists f (-(f*e=d))))))) ). max_proofs 0
208. all a (((all b c (-(b*c=a)))) <-> ((all d e (-(d*e=a))) & (exists f ((all g ((exists h (-(g*h=f))))))))).
all a ( (all b c (-(b*c=a))) -> (exists d ((all e ((exists f (-(e*f=d))))))) ). max_proofs 0
209. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b (b*a=a)))) & (exists c ((all d e (-(d*e=c)))))). max_proofs 3
210. ((all a b ((exists c (c*a=b))))) <-> ((all d ((exists e (e*d=d)))) & (all f ((exists g ((all h (f*h=g))))))).
(all a ((exists b (b*a=a)))) & (all c ((exists d ((all e (c*e=d)))))) -> (all f g ((exists h (h*f=g)))). max_proofs 2
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
211. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b (b*a=a)))) & (all c ((exists d (d*c=d))))). max_proofs 5
(160) [N] s.t. (all a ((exists b (b*a=a)))) & (exists c ((all d ((exists e (-(c*e=d))))))) " ahlfors non_assoc 9 "
212. ((all a ((exists b (b*a=a))))) <-> ((all c ((exists d (d*c=c)))) & (exists e ((all f ((exists g (-(g*f=e)))))))).
(all a ((exists b (b*a=a)))) -> (exists c ((all d ((exists e (-(e*d=c))))))). max_proofs 4
213. ((all a b ((exists c (c*a=b))))) <-> ((all d ((exists e (e*d=d)))) & (exists f ((all g ((exists h (h*f=g))))))).
(all a ((exists b (b*a=a)))) & (exists c ((all d ((exists e (e*c=d)))))) -> (all f g ((exists h (h*f=g)))). sos
Mace generating counterexample of order: 1 2 3 4 e14
Checking whether conjectures are disproved: 45:no,49:no,55:no,70:no,74:no,80:no,88:no,90:no,91:no,96:no,99:no,103:no,108:yes(New Concept = 161),113:no,115:yes(New Conjecture = 214),116:no,118:no,126:no,129:no,130:no,145:no,147:no,150:no,157:no,158:no,160:yes(New Conjecture = 215),162:no,164:no,165:no,169:no,174:no,181:no,182:no,183:no,187:no,190:no,191:no,192:no,194:no,195:no,196:no,197:no,198:no,202:no,206:no,210:no,213:yes(New Concept = 162),
(161) [N,a] s.t. (all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e)))))) " ahlfors element 22 "
(162) [N] s.t. (all a ((exists b (b*a=a)))) & (exists c ((all d ((exists e (e*c=d)))))) " ahlfors non_assoc 10 "
* | 0 | 1 | 2 | 3 |
--+---+---+---+---+
0 | 1 | 1 | 1 | 1 |
--+---+---+---+---+
1 | 0 | 0 | 0 | 0 |
--+---+---+---+---+
2 | 3 | 3 | 0 | 3 |
--+---+---+---+---+
3 | 2 | 2 | 2 | 0 |
--+---+---+---+---+
214. all a (((all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e))))))) <-> ((exists g ((all h (g*h=a)))) & (exists i ((all j ((exists k (k*i=j)))))))).
all a ( (all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e)))))) -> (exists g ((all h (g*h=a)))) ). sos
all a ( (exists b ((all c (b*c=a)))) & (exists d ((all e ((exists f (f*d=e)))))) -> (all g ((exists h (h*g=a)))) ).
---------------------------------------------
all a ( (exists b ((all c (b*c=a)))) -> (all d ((exists e (e*d=a)))) ).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
215. all a (((all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e))))))) <-> ((all g ((exists h (h*g=a)))) & (all i ((exists j k (j*k=i)))) & (exists l ((all m ((exists n (n*l=m)))))))).
all a ( (exists b ((all c ((exists d (d*b=c)))))) -> (all e ((exists f g (f*g=e)))) ). max_proofs 0
all a ( (all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e)))))) -> (all g ((exists h i (h*i=g)))) ).
---------------------------------------------
all a ( (exists b ((all c ((exists d (d*b=c)))))) -> (all e ((exists f g (f*g=e)))) ).
Top Ten Sorted Concepts: [110,146,99,116,144,60,93,96,139,137]
Top Ten Sorted Conjectures: [197,114,134,152,125,128,106,102,179,161]
216. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b (b*a=a)))) & (exists c ((exists d (d*c=c)) & (exists e f (e*f=e))))). max_proofs 6
217. ((all a ((exists b (b*a=a)))) & (exists c ((all d ((exists e (-(c*e=d)))))))) <-> ((all f ((exists g (g*f=f)))) & (exists h ((all i ((exists j (-(i*j=h)))))))).
(all a ((exists b (b*a=a)))) & (exists c ((all d ((exists e (-(d*e=c))))))) -> (exists f ((all g ((exists h (-(f*h=g))))))). max_proofs 2
(all a ((exists b (b*a=a)))) & (exists c ((all d ((exists e (-(c*e=d))))))) -> (exists f ((all g ((exists h (-(g*h=f))))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
218. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b (b*a=a)) & (exists c d (c*d=c)) & (all e ((exists f (f*e=f)))))). max_proofs 5
(163) [N,a] s.t. (exists b ((all c (a*c=b)))) & (all d ((exists e ((all f (d*f=e)))))) " aristarchus element 11 "
219. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b ((all c (a*c=b)))) & (all d ((exists e (e*d=e)))))). max_proofs 5
(164) [N,a] s.t. (exists b ((all c (a*c=b)))) & (exists d ((all e ((exists f (-(d*f=e))))))) " aristarchus element 12 "
220. all a (((exists b ((all c (a*c=b))))) <-> ((exists d ((all e (a*e=d)))) & (exists f ((all g ((exists h (-(h*g=f))))))))).
all a ( (exists b ((all c (a*c=b)))) -> (exists d ((all e ((exists f (-(f*e=d))))))) ). max_proofs 2
221. ((all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c)))))))) <-> ((exists f g ((all h (h*f=g)))) & -((all i ((exists j k (j*k=i)))) & (exists l m ((all n (n*l=m)))))).
(exists a b ((all c (c*a=b)))) & -((all d ((exists e f (e*f=d)))) & (exists g h ((all i (i*g=h))))) -> (all j ((exists k (k*j=k)) & (exists l ((all m n (-(m*n=l))))))). sos
(all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c))))))) -> (exists f g ((all h (h*f=g)))). sos
(all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c))))))) -> -((all f ((exists g h (g*h=f)))) & (exists i j ((all k (k*i=j))))). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
222. ((all a ((exists b (a*b=a))))) <-> ((exists c d ((all e (e*c=d)))) & (all f ((exists g (f*g=f))))).
(all a ((exists b (a*b=a)))) -> (exists c d ((all e (e*c=d)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
223. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a b ((all c (c*a=b)))) & (all d ((exists e (e*d=d))))). max_proofs 6
224. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a b ((all c (c*a=b)))) & (all d ((exists e ((all f (d*f=e))))))). max_proofs 7
225. ((all a ((exists b (b*a=b))))) <-> ((exists c d ((all e (e*c=d)))) & (all f ((exists g (g*f=g))))).
(all a ((exists b (b*a=b)))) -> (exists c d ((all e (e*c=d)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
226. ((all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c)))))))) <-> ((exists f g ((all h (h*f=g)))) & (exists i ((all j k (-(j*k=i)))))).
(exists a b ((all c (c*a=b)))) & (exists d ((all e f (-(e*f=d))))) -> (all g ((exists h (h*g=h)) & (exists i ((all j k (-(j*k=i))))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
227. ((exists a b ((all c (c*a=b))))) <-> ((exists d e ((all f (f*d=e)))) & (exists g ((all h ((exists i (-(g*i=h)))))))).
(exists a b ((all c (c*a=b)))) -> (exists d ((all e ((exists f (-(d*f=e))))))). max_proofs 5
228. ((all a ((all b ((exists c (-(a*c=b))))) & (exists d ((all e ((exists f (-(f*e=d)))))))))) <-> ((exists g h ((all i (i*g=h)))) & (exists j ((all k ((exists l (-(l*k=j)))))))).
(exists a b ((all c (c*a=b)))) & (exists d ((all e ((exists f (-(f*e=d))))))) -> (all g ((all h ((exists i (-(g*i=h))))) & (exists j ((all k ((exists l (-(l*k=j))))))))). max_proofs 7
(all a ((all b ((exists c (-(a*c=b))))) & (exists d ((all e ((exists f (-(f*e=d))))))))) -> (exists g h ((all i (i*g=h)))). sos
(all a ((all b ((exists c (-(a*c=b))))) & (exists d ((all e ((exists f (-(f*e=d))))))))) -> (exists g ((all h ((exists i (-(i*h=g))))))). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(165) [N] s.t. (exists a b ((all c (c*a=b)))) & (exists d ((all e ((exists f (d*f=e)))))) " archytas non_assoc 2 "
(166) [N] s.t. (exists a b ((all c (c*a=b)))) & (exists d ((all e ((exists f (f*d=e)))))) " archytas non_assoc 3 "
Top Ten Sorted Concepts: [138,110,146,99,116,93,60,96,76,139]
Top Ten Sorted Conjectures: [197,114,134,152,125,224,128,106,102,179]
229. ((exists a ((all b ((exists c (-(a*c=b))))) & (exists d ((all e ((exists f (-(f*e=d)))))))))) <-> ((exists g ((all h ((exists i (-(i*h=g))))))) & (exists j ((all k ((exists l (-(j*l=k)))))))).
(exists a ((all b ((exists c (-(c*b=a))))))) & (exists d ((all e ((exists f (-(d*f=e))))))) -> (exists g ((all h ((exists i (-(g*i=h))))) & (exists j ((all k ((exists l (-(l*k=j))))))))). max_proofs 1
(exists a ((all b ((exists c (-(a*c=b))))) & (exists d ((all e ((exists f (-(f*e=d))))))))) -> (exists g ((all h ((exists i (-(i*h=g))))))). max_proofs 0
(exists a ((all b ((exists c (-(a*c=b))))) & (exists d ((all e ((exists f (-(f*e=d))))))))) -> (exists g ((all h ((exists i (-(g*i=h))))))). max_proofs 0
230. ((exists a b ((all c (c*a=b))))) <-> ((exists d e ((all f (f*d=e)))) & (exists g ((all h ((exists i (-(h*i=g)))))))).
(exists a b ((all c (c*a=b)))) -> (exists d ((all e ((exists f (-(e*f=d))))))). max_proofs 2
231. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a b ((all c (c*a=b)))) & (exists d e ((all f (d*f=e))))). max_proofs 6
232. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a ((all b ((exists c (a*c=b)))))) & (all d ((exists e ((all f (d*f=e))))))). max_proofs 6
233. ((all a ((exists b (a*b=a)))) & (exists c ((all d ((exists e (c*e=d))))))) <-> ((exists f ((all g ((exists h (f*h=g)))))) & (all i ((exists j (j*i=j))))).
(all a ((exists b (a*b=a)))) & (exists c ((all d ((exists e (c*e=d)))))) -> (all f ((exists g (g*f=g)))). sos
(exists a ((all b ((exists c (a*c=b)))))) & (all d ((exists e (e*d=e)))) -> (all f ((exists g (f*g=f)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(167) [N] s.t. (exists a ((all b ((exists c (a*c=b)))))) & (exists d ((all e ((exists f (-(f*e=d))))))) " abraham non_assoc 9 "
234. ((exists a ((all b ((exists c (a*c=b))))))) <-> ((exists d ((all e ((exists f (d*f=e)))))) & (exists g ((all h ((exists i (-(g*i=h)))))))).
(exists a ((all b ((exists c (a*c=b)))))) -> (exists d ((all e ((exists f (-(d*f=e))))))). max_proofs 4
235. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a ((all b ((exists c (a*c=b)))))) & (exists d ((all e f (-(e*f=d)))))). max_proofs 3
236. ((exists a ((all b ((exists c (a*c=b))))))) <-> ((exists d ((all e ((exists f (d*f=e)))))) & (exists g ((all h ((exists i (-(h*i=g)))))))).
(exists a ((all b ((exists c (a*c=b)))))) -> (exists d ((all e ((exists f (-(e*f=d))))))). max_proofs 2
237. ((all a b ((exists c (c*a=b))))) <-> ((all d e ((exists f (f*d=e)))) & (all g ((exists h ((all i (g*i=h))))))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
238. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (c*a=b)))) & (all d ((exists e (e*d=e))))). max_proofs 5
239. ((all a b ((exists c (c*a=b))))) <-> ((all d e ((exists f (f*d=e)))) & (exists g ((all h ((exists i (-(i*h=g)))))))).
(all a b ((exists c (c*a=b)))) -> (exists d ((all e ((exists f (-(f*e=d))))))).
---------------------------------------------
(all a b ((exists c (c*a=b)))) -> (exists d ((all e ((exists f (f*d=e)))))).
(exists a ((all b ((exists c (c*a=b)))))) -> (exists d ((all e ((exists f (-(f*e=d))))))).
240. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (-(d*f=e)))))))). sos
Mace generating counterexample of order: 1 2 3 4 e15
Checking whether conjectures are disproved: 45:no,49:no,55:no,70:yes(New Concept = 168),74:yes(New Concept = 169),80:yes(New Concept = 170),88:no,90:no,91:yes(New Concept = 171),96:no,99:no,103:no,113:yes(New Conjecture = 241),116:yes(New Concept = 172),118:yes(New Concept = 173),126:no,129:no,130:no,145:yes(New Concept = 174),147:yes(New Conjecture = 242),150:no,157:yes(New Concept = 175),158:yes(New Concept = 176),162:no,164:yes(New Concept = 177),165:yes(New Conjecture = 243),169:yes(New Conjecture = 244),174:no,181:no,182:no,183:no,187:yes(New Conjecture = 245),190:no,191:no,192:no,194:no,195:no,196:no,197:yes(New Conjecture = 246),198:no,202:no,206:no,210:yes(New Conjecture = 247),214:yes(New Concept = 178),217:no,221:no,222:no,225:no,226:no,228:yes(New Concept = 179),233:no,237:yes(New Conjecture = 248),240:yes(New Concept = 180),
(168) [N] s.t. (exists a ((all b ((exists c (c*b=a)))))) " ahlfors non_assoc 11 "
(169) [N,a] s.t. (all b ((exists c (c*b=a)))) & (exists d e ((all f (d*f=e)))) " ahlfors element 23 "
(170) [N] s.t. (all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e)))) " ahlfors non_assoc 12 "
(171) [N,a] s.t. (all b ((exists c (c*a=b)))) & (all d ((exists e (e*d=d)))) " ahlfors element 24 "
(172) [N,a] s.t. (exists b ((all c (b*c=a)))) & (all d ((exists e (e*d=d)))) " aristarchus element 13 "
(173) [N] s.t. (all a b ((exists c (-(a*c=b))))) " aryabhata non_assoc 5 "
(174) [N,a] s.t. (exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) & (all g ((exists h ((all i (g*i=h)))))) " akhiezer element 6 "
(175) [N] s.t. (exists a ((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d)))))) " ahlfors non_assoc 13 "
(176) [N,a] s.t. (all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d)))) & (exists g h ((all i (g*i=h)))) " ahlfors element 25 "
(177) [N] s.t. (exists a (-((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))))) " akhiezer non_assoc 9 "
(178) [N,a] s.t. (exists b ((all c (b*c=a)))) & (exists d ((all e ((exists f (f*d=e)))))) " aristarchus element 14 "
(179) [N] s.t. (exists a b ((all c (c*a=b)))) & (exists d ((all e ((exists f (-(f*e=d))))))) " archytas non_assoc 4 "
(180) [N] s.t. (all a b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (-(d*f=e))))))) " ahlfors non_assoc 14 "
* | 0 | 1 | 2 | 3 |
--+---+---+---+---+
0 | 1 | 1 | 1 | 2 |
--+---+---+---+---+
1 | 0 | 0 | 3 | 0 |
--+---+---+---+---+
2 | 3 | 3 | 0 | 3 |
--+---+---+---+---+
3 | 2 | 2 | 2 | 1 |
--+---+---+---+---+
241. ((all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e))))) <-> ((all g ((exists h ((all i (h*i=g))))))).
(all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e)))) -> (all g ((exists h ((all i (h*i=g)))))). sos
(all a ((exists b ((all c (b*c=a)))))) -> (exists d e ((all f (d*f=e)))). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
242. all a (((exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) & (all g ((exists h ((all i (g*i=h))))))) <-> ((exists j k (j*k=a)) & (all l m ((exists n (n*l=m)))) & (exists o p ((all q (o*q=p)))))).
all a ( (exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) & (exists g h ((all i (g*i=h)))) -> (all j ((exists k ((all l (j*l=k)))))) ). sos
all a ( (all b c ((exists d (d*b=c)))) & (all e ((exists f ((all g (e*g=f)))))) -> (exists h i ((all j (h*j=i)))) ). max_proofs 0
all a ( (all b ((exists c ((all d (b*d=c)))))) -> (exists e f ((all g (e*g=f)))) ). max_proofs 0
all a ( (exists b c (b*c=a)) & (all d ((exists e ((all f (d*f=e)))))) -> (exists g h ((all i (g*i=h)))) ).
---------------------------------------------
all a ( (all b ((exists c ((all d (b*d=c)))))) -> (exists e f ((all g (e*g=f)))) ).
all a ( (exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) & (all g ((exists h ((all i (g*i=h)))))) -> (exists j k ((all l (j*l=k)))) ).
---------------------------------------------
all a ( (all b c ((exists d (d*b=c)))) & (all e ((exists f ((all g (e*g=f)))))) -> (exists h i ((all j (h*j=i)))) ).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
243. ((exists a (-((exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))))))) <-> ((all g (-((exists h i (h*i=g)) & (all j k ((exists l (l*j=k)))))))).
(exists a (-((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))))) -> (all g (-((exists h i (h*i=g)) & (all j k ((exists l (l*j=k))))))). max_proofs 0
(all a (-((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))))) -> (exists g (-((exists h i (h*i=g)) & (all j k ((exists l (l*j=k))))))). max_proofs 1
244. ((exists a (-((exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))))))) <-> ((exists g (-((all h ((exists i (i*h=g)))) & (all j ((exists k l (k*l=j)))))))).
(exists a (-((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))))) -> (exists g (-((all h ((exists i (i*h=g)))) & (all j ((exists k l (k*l=j))))))). max_proofs 0
(exists a (-((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d))))))) -> (exists g (-((exists h i (h*i=g)) & (all j k ((exists l (l*j=k))))))). max_proofs 1
245. ((all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e))))) <-> ((exists g ((all h ((exists i (i*g=h)))))) & (all j ((exists k ((all l (j*l=k))))))).
(all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e)))) -> (exists g ((all h ((exists i (i*g=h)))))).
---------------------------------------------
(all a b ((exists c (c*a=b)))) -> (exists d ((all e ((exists f (f*d=e)))))).
(all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e)))) -> (all g ((exists h ((all i (g*i=h)))))). sos
(all a ((exists b ((all c (a*c=b)))))) -> (exists d e ((all f (d*f=e)))). max_proofs 0
(exists a ((all b ((exists c (c*a=b)))))) & (all d ((exists e ((all f (d*f=e)))))) -> (exists g h ((all i (g*i=h)))).
---------------------------------------------
(all a ((exists b ((all c (a*c=b)))))) -> (exists d e ((all f (d*f=e)))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
246. ((all a b ((exists c (-(a*c=b)))))) <-> ((all d ((all e ((exists f (-(e*f=d))))) & (exists g ((all h ((exists i (-(g*i=h)))))))))).
(all a b ((exists c (-(a*c=b))))) -> (all d ((all e ((exists f (-(e*f=d))))) & (exists g ((all h ((exists i (-(g*i=h))))))))). max_proofs 1
(all a ((all b ((exists c (-(b*c=a))))) & (exists d ((all e ((exists f (-(d*f=e))))))))) -> (all g h ((exists i (-(g*i=h))))). max_proofs 0
247. ((all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e))))) <-> ((all g ((exists h (h*g=g)))) & (all i ((exists j ((all k (i*k=j))))))).
(all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e)))) -> (all g ((exists h (h*g=g)))).
---------------------------------------------
(all a b ((exists c (c*a=b)))) -> (all d ((exists e (e*d=d)))).
(all a ((exists b (b*a=a)))) & (all c ((exists d ((all e (c*e=d)))))) -> (exists f g ((all h (f*h=g)))).
---------------------------------------------
(all a ((exists b ((all c (a*c=b)))))) -> (exists d e ((all f (d*f=e)))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
248. ((all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e))))) <-> ((all g h ((exists i (i*g=h)))) & (all j ((exists k ((all l (j*l=k))))))).
(all a b ((exists c (c*a=b)))) & (all d ((exists e ((all f (d*f=e)))))) -> (exists g h ((all i (g*i=h)))).
---------------------------------------------
(all a ((exists b ((all c (a*c=b)))))) -> (exists d e ((all f (d*f=e)))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
Top Ten Sorted Concepts: [138,110,146,99,116,93,96,60,139,76]
Top Ten Sorted Conjectures: [197,114,134,152,125,224,128,106,102,179]
Summary for session in non_assoc theory:
---------------------
Number of concepts: 180
Number of Conjectures: 248
Number of Models: 15
Largest Model Size: 4
Number of Categorisations: 111
Number of Theorems: 171
Number of Open Conjectures: 34
Number of Prime Implicants: 146
Average Proof Length: 2.888888888888889
Average Surprisingness: 2.7309941520467835
Average P.I. Proof Length: 0.6027397260273972
Number of Otter Proofs: 146
Number of HR Proofs: 51
----------------------
(181) [N,a] s.t. -((all b ((exists c (c*b=a)))) & (exists d e (d*e=d))) & (exists f ((all g ((exists h (h*g=f)))))) " ahlfors element 26 "
Top Ten Sorted Concepts: [138,110,146,99,116,93,96,60,139,76]
Top Ten Sorted Conjectures: [197,114,134,152,125,224,128,106,102,179]
249. ((all a ((exists b (a*b=a))))) <-> ((all c ((exists d (c*d=c)))) & (all e f ((exists g (-(e*g=f)))))).
(all a ((exists b (a*b=a)))) -> (all c d ((exists e (-(c*e=d))))). max_proofs 2
Top Ten Sorted Concepts: [138,110,146,99,116,93,96,60,139,76]
Top Ten Sorted Conjectures: [197,114,134,152,125,224,128,106,102,179]
250. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b (a*b=a)))) & (exists c ((all d ((exists e (e*d=c))))))). max_proofs 6
251. ((all a b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (-(d*f=e)))))))) <-> ((all g ((exists h (h*g=g)))) & (all i j ((exists k (-(i*k=j)))))).
(all a b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (-(d*f=e))))))) -> (all g ((exists h (h*g=g)))).
---------------------------------------------
(all a b ((exists c (c*a=b)))) -> (all d ((exists e (e*d=d)))).
(all a b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (-(d*f=e))))))) -> (all g h ((exists i (-(g*i=h))))). sos
(all a ((exists b (b*a=a)))) & (all c d ((exists e (-(c*e=d))))) -> (all f g ((exists h (h*f=g)))). sos
(all a b ((exists c (-(a*c=b))))) -> (exists d ((all e ((exists f (-(d*f=e))))))). max_proofs 0
(all a ((exists b (b*a=a)))) & (all c d ((exists e (-(c*e=d))))) -> (exists f ((all g ((exists h (-(f*h=g))))))).
---------------------------------------------
(all a b ((exists c (-(a*c=b))))) -> (exists d ((all e ((exists f (-(d*f=e))))))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
252. ((all a ((exists b (b*a=a))))) <-> ((all c ((exists d (d*c=c)))) & (exists e ((all f ((exists g (g*f=e))))))).
(all a ((exists b (b*a=a)))) -> (exists c ((all d ((exists e (e*d=c)))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
253. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b ((all c (a*c=b)))))) & (all d e ((exists f (-(d*f=e)))))). max_proofs 3
254. ((all a ((exists b ((all c (a*c=b))))))) <-> ((all d ((exists e ((all f (d*f=e)))))) & (exists g ((all h ((exists i (i*h=g))))))).
(all a ((exists b ((all c (a*c=b)))))) -> (exists d ((all e ((exists f (f*e=d)))))). max_proofs 0
255. ((all a ((exists b (b*a=b))))) <-> ((all c ((exists d (d*c=d)))) & (all e f ((exists g (-(e*g=f)))))).
(all a ((exists b (b*a=b)))) -> (all c d ((exists e (-(c*e=d))))). max_proofs 3
256. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b (b*a=b)))) & (exists c ((all d ((exists e (e*d=c))))))). max_proofs 5
257. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b ((all c (a*c=b)))) & (all d e ((exists f (-(d*f=e))))))). max_proofs 3
258. all a (((exists b ((all c (a*c=b))))) <-> ((exists d ((all e (a*e=d)))) & (exists f ((all g ((exists h (h*g=f)))))))).
all a ( (exists b ((all c (a*c=b)))) -> (exists d ((all e ((exists f (f*e=d)))))) ). max_proofs 0
259. all a (((exists b (b*a=a)) & (exists c d (c*d=c)) & (exists e f ((all g (e*g=f))))) <-> ((exists h (h*a=a)) & (exists i j (i*j=i)) & (exists k ((all l ((exists m (m*l=k)))))))).
all a ( (exists b c (b*c=b)) & (exists d e ((all f (d*f=e)))) -> (exists g ((all h ((exists i (i*h=g)))))) ). max_proofs 0
all a ( (exists b c ((all d (b*d=c)))) -> (exists e ((all f ((exists g (g*f=e)))))) ). max_proofs 0
all a ( (exists b (b*a=a)) & (exists c d ((all e (c*e=d)))) -> (exists f ((all g ((exists h (h*g=f)))))) ).
---------------------------------------------
all a ( (exists b c ((all d (b*d=c)))) -> (exists e ((all f ((exists g (g*f=e)))))) ).
all a ( (exists b (b*a=a)) & (exists c d (c*d=c)) & (exists e f ((all g (e*g=f)))) -> (exists h ((all i ((exists j (j*i=h)))))) ).
---------------------------------------------
all a ( (exists b c (b*c=b)) & (exists d e ((all f (d*f=e)))) -> (exists g ((all h ((exists i (i*h=g)))))) ).
all a ( (exists b (b*a=a)) & (exists c d (c*d=c)) & (exists e ((all f ((exists g (g*f=e)))))) -> (exists h i ((all j (h*j=i)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
260. ((exists a b ((all c (c*a=b))))) <-> ((exists d e ((all f (f*d=e)))) & (all g h ((exists i (-(g*i=h)))))).
(exists a b ((all c (c*a=b)))) -> (all d e ((exists f (-(d*f=e))))).
---------------------------------------------
(exists a b ((all c (c*a=b)))) -> (all d ((all e ((exists f (-(e*f=d))))) & (exists g ((all h ((exists i (-(g*i=h))))))))).
(all a ((all b ((exists c (-(b*c=a))))) & (exists d ((all e ((exists f (-(d*f=e))))))))) -> (all g h ((exists i (-(g*i=h))))).
261. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a b ((all c (c*a=b)))) & (exists d ((all e ((exists f (f*e=d))))))). max_proofs 6
(182) [N,a] s.t. (all b ((exists c (-(b*c=a))))) & (exists d ((all e ((exists f (-(d*f=e))))))) & (all g h ((exists i (-(g*i=h))))) " aryabhata element 11 "
262. ((exists a b ((all c (c*a=b)))) & (exists d ((all e ((exists f (d*f=e))))))) <-> ((exists g ((all h ((exists i (g*i=h)))))) & (all j k ((exists l (-(j*l=k)))))).
(exists a b ((all c (c*a=b)))) & (exists d ((all e ((exists f (d*f=e)))))) -> (all g h ((exists i (-(g*i=h))))).
---------------------------------------------
(exists a b ((all c (c*a=b)))) -> (all d ((all e ((exists f (-(e*f=d))))) & (exists g ((all h ((exists i (-(g*i=h))))))))).
(all a ((all b ((exists c (-(b*c=a))))) & (exists d ((all e ((exists f (-(d*f=e))))))))) -> (all g h ((exists i (-(g*i=h))))).
(exists a ((all b ((exists c (a*c=b)))))) & (all d e ((exists f (-(d*f=e))))) -> (exists g h ((all i (i*g=h)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
263. ((exists a ((exists b ((all c (a*c=b)))) & (exists d ((all e ((exists f (d*f=e))))))))) <-> ((exists g ((all h ((exists i (g*i=h)))))) & (exists j ((all k ((exists l (l*k=j))))))).
(exists a ((all b ((exists c (a*c=b)))))) & (exists d ((all e ((exists f (f*e=d)))))) -> (exists g ((exists h ((all i (g*i=h)))) & (exists j ((all k ((exists l (j*l=k)))))))). sos
(exists a ((exists b ((all c (a*c=b)))) & (exists d ((all e ((exists f (d*f=e)))))))) -> (exists g ((all h ((exists i (g*i=h)))))). max_proofs 0
(exists a ((exists b ((all c (a*c=b)))) & (exists d ((all e ((exists f (d*f=e)))))))) -> (exists g ((all h ((exists i (i*h=g)))))). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
264. ((all a ((all b ((exists c (-(a*c=b))))) & (exists d ((all e ((exists f (-(f*e=d)))))))))) <-> ((exists g ((all h ((exists i (-(i*h=g))))))) & (all j k ((exists l (-(j*l=k)))))).
(exists a ((all b ((exists c (-(c*b=a))))))) & (all d e ((exists f (-(d*f=e))))) -> (all g ((all h ((exists i (-(g*i=h))))) & (exists j ((all k ((exists l (-(l*k=j))))))))). max_proofs 1
(all a ((all b ((exists c (-(a*c=b))))) & (exists d ((all e ((exists f (-(f*e=d))))))))) -> (all g h ((exists i (-(g*i=h))))). max_proofs 0
265. ((exists a ((all b ((exists c (c*b=a))))))) <-> ((exists d ((all e ((exists f (-(f*e=d))))))) & (exists g ((all h ((exists i (i*h=g))))))).
(exists a ((all b ((exists c (c*b=a)))))) -> (exists d ((all e ((exists f (-(f*e=d))))))). max_proofs 4
266. ((all a b ((exists c (-(a*c=b)))))) <-> ((exists d ((all e ((exists f (-(d*f=e))))))) & (all g h ((exists i (-(g*i=h)))))).
267. ((all a ((all b ((exists c (-(c*b=a))))) & (exists d ((all e ((exists f (-(d*f=e)))))))))) <-> ((exists g ((all h ((exists i (-(g*i=h))))))) & (exists j ((all k ((exists l (l*k=j))))))).
(exists a ((all b ((exists c (-(a*c=b))))))) & (exists d ((all e ((exists f (f*e=d)))))) -> (all g ((all h ((exists i (-(i*h=g))))) & (exists j ((all k ((exists l (-(j*l=k))))))))). max_proofs 5
(all a ((all b ((exists c (-(c*b=a))))) & (exists d ((all e ((exists f (-(d*f=e))))))))) -> (exists g ((all h ((exists i (-(g*i=h))))))). max_proofs 0
(all a ((all b ((exists c (-(c*b=a))))) & (exists d ((all e ((exists f (-(d*f=e))))))))) -> (exists g ((all h ((exists i (i*h=g)))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
268. ((all a b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (-(d*f=e)))))))) <-> ((all g h ((exists i (i*g=h)))) & (all j k ((exists l (-(j*l=k)))))).
(all a b ((exists c (c*a=b)))) & (all d e ((exists f (-(d*f=e))))) -> (exists g ((all h ((exists i (-(g*i=h))))))).
---------------------------------------------
(all a b ((exists c (-(a*c=b))))) -> (exists d ((all e ((exists f (-(d*f=e))))))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
269. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (c*a=b)))) & (exists d (-((exists e f (e*f=d)) & (all g h ((exists i (i*g=h)))))))). max_proofs 3
270. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (c*a=b)))) & (exists d ((exists e (e*d=d)) & (exists f g (f*g=f))))). max_proofs 6
271. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (c*a=b)))) & (exists d ((all e f (-(e*f=d)))))). max_proofs 3
272. ((all a b ((exists c (c*a=b))))) <-> ((all d e ((exists f (f*d=e)))) & (exists g ((all h ((exists i (i*g=h))))))).
273. ((all a b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (-(d*f=e)))))))) <-> ((all g h ((exists i (i*g=h)))) & (exists j ((all k ((exists l (-(k*l=j)))))))).
(all a b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (-(e*f=d))))))) -> (exists g ((all h ((exists i (-(g*i=h))))))).
---------------------------------------------
(all a b ((exists c (c*a=b)))) -> (exists d ((all e ((exists f (f*d=e)))))).
(exists a ((all b ((exists c (c*a=b)))))) & (exists d ((all e ((exists f (-(e*f=d))))))) -> (exists g ((all h ((exists i (-(g*i=h))))))).
(all a b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (-(d*f=e))))))) -> (exists g ((all h ((exists i (-(h*i=g))))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
274. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (f*e=d)))) & (exists g h (g*h=g))))). max_proofs 6
275. ((all a b ((exists c (c*a=b))))) <-> ((all d e ((exists f (f*d=e)))) & (exists g ((all h ((exists i (i*h=g)))) & (all j ((exists k l (k*l=j))))))).
(all a b ((exists c (c*a=b)))) -> (exists d ((all e ((exists f (f*e=d)))) & (all g ((exists h i (h*i=g)))))). max_proofs 0
276. ((all a b ((exists c (c*a=b))))) <-> ((all d e ((exists f (f*d=e)))) & (exists g ((all h ((exists i (i*h=g))))))).
(all a b ((exists c (c*a=b)))) -> (exists d ((all e ((exists f (f*e=d)))))). max_proofs 0
277. ((all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c)))))))) <-> ((exists f ((all g h (-(g*h=f))))) & (all i j ((exists k (-(i*k=j)))))).
(exists a ((all b c (-(b*c=a))))) & (all d e ((exists f (-(d*f=e))))) -> (all g ((exists h (h*g=h)) & (exists i ((all j k (-(j*k=i))))))). sos
(all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c))))))) -> (all f g ((exists h (-(f*h=g))))).
---------------------------------------------
(all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c))))))) -> (all f ((exists g (g*f=g)))).
(all a ((exists b (b*a=b)))) -> (all c d ((exists e (-(c*e=d))))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
278. ((all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d)))))))) <-> ((exists g ((all h i (-(h*i=g))))) & (exists j ((all k ((exists l (l*k=j))))))).
(exists a ((all b c (-(b*c=a))))) & (exists d ((all e ((exists f (f*e=d)))))) -> (all g ((exists h ((all i (g*i=h)))) & (exists j ((all k l (-(k*l=j))))))). sos
(all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))))) -> (exists g ((all h ((exists i (i*h=g)))))).
---------------------------------------------
(all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))))) -> (all g ((exists h ((all i (g*i=h)))))).
(all a ((exists b ((all c (a*c=b)))))) -> (exists d ((all e ((exists f (f*e=d)))))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
279. all a (((all b c (-(b*c=a))) & (all d ((exists e (e*d=e))))) <-> ((all f g (-(f*g=a))) & (all h i ((exists j (-(h*j=i))))))).
all a ( (all b ((exists c (c*b=c)))) -> (all d e ((exists f (-(d*f=e))))) ). max_proofs 3
all a ( (all b c (-(b*c=a))) & (all d ((exists e (e*d=e)))) -> (all f g ((exists h (-(f*h=g))))) ).
---------------------------------------------
all a ( (all b ((exists c (c*b=c)))) -> (all d e ((exists f (-(d*f=e))))) ).
all a ( (all b c (-(b*c=a))) & (all d e ((exists f (-(d*f=e))))) -> (all g ((exists h (h*g=h)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
280. all a (((all b ((exists c (-(b*c=a))))) & (all d ((exists e ((all f (d*f=e))))))) <-> ((all g h (-(g*h=a))) & (exists i ((all j ((exists k (k*j=i)))))))).
all a ( (all b c (-(b*c=a))) & (exists d ((all e ((exists f (f*e=d)))))) -> (all g ((exists h (-(g*h=a))))) ).
---------------------------------------------
all a ( (all b c (-(b*c=a))) -> (all d ((exists e (-(d*e=a))))) ).
all a ( (all b c (-(b*c=a))) & (exists d ((all e ((exists f (f*e=d)))))) -> (all g ((exists h ((all i (g*i=h)))))) ). sos
all a ( (all b ((exists c ((all d (b*d=c)))))) -> (exists e ((all f ((exists g (g*f=e)))))) ).
---------------------------------------------
all a ( (all b ((exists c ((all d (b*d=c)))))) -> (exists e f ((all g (e*g=f)))) ).
all a ( (exists b c ((all d (b*d=c)))) -> (exists e ((all f ((exists g (g*f=e)))))) ).
all a ( (all b ((exists c (-(b*c=a))))) & (all d ((exists e ((all f (d*f=e)))))) -> (exists g ((all h ((exists i (i*h=g)))))) ).
---------------------------------------------
all a ( (all b ((exists c ((all d (b*d=c)))))) -> (exists e f ((all g (e*g=f)))) ).
all a ( (exists b c ((all d (b*d=c)))) -> (exists e ((all f ((exists g (g*f=e)))))) ).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(183) [N,a] s.t. (exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) & (all g h ((exists i (-(g*i=h))))) " akhiezer element 7 "
281. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) & (exists g (-((exists h i (h*i=g)) & (all j k ((exists l (l*j=k))))))))). max_proofs 5
282. all a (((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))) <-> ((exists g h (g*h=a)) & (all i j ((exists k (k*i=j)))) & (exists l ((all m ((exists n (n*m=l)))))))).
all a ( (all b c ((exists d (d*b=c)))) -> (exists e ((all f ((exists g (g*f=e)))))) ). max_proofs 0
all a ( (exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) -> (exists g ((all h ((exists i (i*h=g)))))) ).
---------------------------------------------
all a ( (all b c ((exists d (d*b=c)))) -> (exists e ((all f ((exists g (g*f=e)))))) ).
(184) [N,a] s.t. -((exists b (b*a=a)) & (exists c d ((all e (e*c=d))))) " ahlfors element 27 "
283. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b (b*a=a)) & (exists c d ((all e (e*c=d))))))). max_proofs 6
(185) [N] s.t. (exists a ((exists b (b*a=a)) & (exists c d ((all e (e*c=d)))))) " ahlfors non_assoc 15 "
284. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b (b*a=a)) & (exists c d ((all e (e*c=d)))) & (all f ((exists g (g*f=f)))))). max_proofs 6
285. all a (((all b ((exists c (c*a=b)))) & (exists d e (d*e=d))) <-> ((exists f (f*a=a)) & (exists g h ((all i (i*g=h)))) & (exists j ((all k ((exists l (l*j=k)))))))).
all a ( (exists b (b*a=a)) & (exists c d ((all e (e*c=d)))) & (exists f ((all g ((exists h (h*f=g)))))) -> (all i ((exists j (j*a=i)))) ). sos
all a ( (exists b c ((all d (d*b=c)))) & (exists e ((all f ((exists g (g*e=f)))))) -> (exists h i (h*i=h)) ).
---------------------------------------------
all a ( (exists b c ((all d (d*b=c)))) -> (exists e f (e*f=e)) ).
all a ( (exists b (b*a=a)) & (exists c d ((all e (e*c=d)))) & (exists f ((all g ((exists h (h*f=g)))))) -> (exists i j (i*j=i)) ).
---------------------------------------------
all a ( (exists b c ((all d (d*b=c)))) -> (exists e f (e*f=e)) ).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
286. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b (b*a=a)) & (exists c d ((all e (e*c=d)))) & (exists f g ((all h (f*h=g)))))). max_proofs 6
287. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b (b*a=a)) & (exists c d ((all e (e*c=d)))) & (exists f ((all g ((exists h (h*g=f)))))))). max_proofs 6
(186) [N] s.t. (exists a ((all b ((exists c (c*a=b)))))) & (all d e ((exists f (-(d*f=e))))) " ahlfors non_assoc 16 "
Top Ten Sorted Concepts: [110,146,142,79,99,116,138,93,60,96]
Top Ten Sorted Conjectures: [197,114,134,152,125,224,283,128,106,102]
288. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b (b*a=a)))) & (exists c ((exists d (d*c=c)) & (exists e f ((all g (g*e=f))))))). max_proofs 6
289. ((exists a ((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d))))))) <-> ((exists g ((all h ((exists i (i*h=g)))))) & (exists j ((all k ((exists l (l*k=j)))) & (all m ((exists n o (n*o=m))))))).
(exists a ((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d)))))) -> (exists g ((all h ((exists i (i*h=g)))))). max_proofs 0
290. ((all a b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (-(d*f=e)))))))) <-> ((exists g ((all h ((exists i (i*h=g)))))) & (all j k ((exists l (-(j*l=k)))))).
(all a b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (-(d*f=e))))))) -> (exists g ((all h ((exists i (i*h=g)))))).
---------------------------------------------
(all a b ((exists c (c*a=b)))) -> (exists d ((all e ((exists f (f*e=d)))))).
(exists a ((all b ((exists c (c*b=a)))))) & (all d e ((exists f (-(d*f=e))))) -> (all g h ((exists i (i*g=h)))). sos
(exists a ((all b ((exists c (c*b=a)))))) & (all d e ((exists f (-(d*f=e))))) -> (exists g ((all h ((exists i (-(g*i=h))))))).
---------------------------------------------
(all a b ((exists c (-(a*c=b))))) -> (exists d ((all e ((exists f (-(d*f=e))))))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
291. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (c*a=b)))) & (exists d ((exists e (e*d=d)) & (exists f g ((all h (h*f=g))))))). max_proofs 4
292. ((exists a ((all b ((exists c (c*b=a)))) & (exists d e (d*e=d))))) <-> ((exists f ((all g ((exists h (h*g=f)))) & (exists i j (i*j=i)))) & (exists k ((all l ((exists m (m*l=k))))))).
(exists a ((all b ((exists c (c*b=a)))) & (exists d e (d*e=d)))) -> (exists f ((all g ((exists h (h*g=f)))))). max_proofs 0
(187) [N,a] s.t. (exists b (a*b=a)) & (all c ((exists d (d*c=d)))) " abraham element 24 "
293. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b (a*b=a)) & (all c ((exists d ((all e (c*e=d)))))))). max_proofs 6
294. all a (((exists b (a*b=a)) & (exists c d ((all e (c*e=d))))) <-> ((exists f (a*f=a)) & (exists g ((all h ((exists i (i*h=g)))))))).
all a ( (exists b (a*b=a)) & (exists c d ((all e (c*e=d)))) -> (exists f ((all g ((exists h (h*g=f)))))) ).
---------------------------------------------
all a ( (exists b c ((all d (b*d=c)))) -> (exists e ((all f ((exists g (g*f=e)))))) ).
all a ( (exists b (a*b=a)) & (exists c ((all d ((exists e (e*d=c)))))) -> (exists f g ((all h (f*h=g)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(188) [N,a] s.t. (exists b (a*b=a)) & (exists c ((all d ((exists e (-(e*d=c))))))) " abraham element 25 "
295. all a (((exists b (a*b=a))) <-> ((exists c (a*c=a)) & (exists d ((all e ((exists f (-(d*f=e))))))))).
all a ( (exists b (a*b=a)) -> (exists c ((all d ((exists e (-(c*e=d))))))) ). max_proofs 4
296. all a (((exists b (a*b=a)) & (exists c d ((all e (e*c=d))))) <-> ((exists f (a*f=a)) & (all g h ((exists i (-(g*i=h))))))).
all a ( (exists b c ((all d (d*b=c)))) -> (all e f ((exists g (-(e*g=f))))) ). max_proofs 4
all a ( (exists b (a*b=a)) & (exists c d ((all e (e*c=d)))) -> (all f g ((exists h (-(f*h=g))))) ).
---------------------------------------------
all a ( (exists b c ((all d (d*b=c)))) -> (all e f ((exists g (-(e*g=f))))) ).
all a ( (exists b (a*b=a)) & (all c d ((exists e (-(c*e=d))))) -> (exists f g ((all h (h*f=g)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
Summary for session in non_assoc theory:
---------------------
Number of concepts: 188
Number of Conjectures: 296
Number of Models: 15
Largest Model Size: 4
Number of Categorisations: 117
Number of Theorems: 203
Number of Open Conjectures: 50
Number of Prime Implicants: 168
Average Proof Length: 2.9261083743842367
Average Surprisingness: 2.7389162561576357
Average P.I. Proof Length: 0.6785714285714286
Number of Otter Proofs: 168
Number of HR Proofs: 72
----------------------
297. all a (((exists b (a*b=a))) <-> ((exists c (a*c=a)) & (exists d ((all e ((exists f (-(e*f=d))))))))).
all a ( (exists b (a*b=a)) -> (exists c ((all d ((exists e (-(d*e=c))))))) ). max_proofs 2
(189) [N,a] s.t. (exists b (b*a=a)) & (exists c (-((exists d e (d*e=c)) & (all f g ((exists h (h*f=g))))))) " ahlfors element 28 "
298. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b (b*a=a)) & (all c ((exists d (d*c=d)))))). max_proofs 5
(190) [N,a] s.t. (exists b (b*a=a)) & (all c ((exists d ((all e (c*e=d)))))) " ahlfors element 29 "
(191) [N,a] s.t. (exists b (b*a=a)) & (exists c ((all d ((exists e (e*d=c)))))) " ahlfors element 30 "
Top Ten Sorted Concepts: [185,110,146,142,79,138,99,116,93,60]
Top Ten Sorted Conjectures: [197,114,134,152,125,224,283,128,106,102]
(192) [N,a] s.t. (exists b (b*a=a)) & (exists c ((all d ((exists e (-(c*e=d))))))) " ahlfors element 31 "
299. all a (((exists b (b*a=a))) <-> ((exists c (c*a=a)) & (exists d ((all e ((exists f (-(f*e=d))))))))).
all a ( (exists b (b*a=a)) -> (exists c ((all d ((exists e (-(e*d=c))))))) ). max_proofs 2
300. all a (((exists b ((all c (b*c=a)))) & (exists d ((all e f (-(e*f=d)))))) <-> ((exists g (g*a=a)) & (exists h ((all i j (-(i*j=h))))))).
all a ( (exists b (b*a=a)) & (exists c ((all d e (-(d*e=c))))) -> (exists f ((all g (f*g=a)))) ). sos
all a ( (exists b ((all c (b*c=a)))) -> (exists d (d*a=a)) ). max_proofs 0
all a ( (exists b ((all c (b*c=a)))) & (exists d ((all e f (-(e*f=d))))) -> (exists g (g*a=a)) ).
---------------------------------------------
all a ( (exists b ((all c (b*c=a)))) -> (exists d (d*a=a)) ).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(193) [N,a] s.t. (exists b (b*a=a)) & (all c d ((exists e (-(c*e=d))))) " ahlfors element 32 "
(194) [N,a] s.t. (exists b (b*a=a)) & (exists c ((all d ((exists e (e*c=d)))))) " ahlfors element 33 "
(195) [N,a] s.t. (exists b (b*a=a)) & (exists c ((all d ((exists e (-(d*e=c))))))) " ahlfors element 34 "
(196) [N,a] s.t. (exists b (b*a=a)) & (exists c ((all d ((exists e (e*d=c)))) & (all f ((exists g h (g*h=f)))))) " ahlfors element 35 "
Top Ten Sorted Concepts: [185,110,146,142,79,99,138,116,93,60]
Top Ten Sorted Conjectures: [197,114,134,152,125,224,283,128,106,102]
301. all a (((exists b (b*a=a)) & (exists c d (c*d=c)) & (exists e f ((all g (e*g=f))))) <-> ((exists h (h*a=a)) & (exists i ((all j ((exists k (k*j=i)))) & (exists l m (l*m=l)))))).
all a ( (exists b c (b*c=b)) & (exists d e ((all f (d*f=e)))) -> (exists g ((all h ((exists i (i*h=g)))) & (exists j k (j*k=j)))) ). max_proofs 0
all a ( (exists b (b*a=a)) & (exists c d (c*d=c)) & (exists e f ((all g (e*g=f)))) -> (exists h ((all i ((exists j (j*i=h)))) & (exists k l (k*l=k)))) ).
---------------------------------------------
all a ( (exists b c (b*c=b)) & (exists d e ((all f (d*f=e)))) -> (exists g ((all h ((exists i (i*h=g)))) & (exists j k (j*k=j)))) ).
all a ( (exists b ((all c ((exists d (d*c=b)))) & (exists e f (e*f=e)))) -> (exists g h (g*h=g)) ). max_proofs 0
all a ( (exists b (b*a=a)) & (exists c ((all d ((exists e (e*d=c)))) & (exists f g (f*g=f)))) -> (exists h i (h*i=h)) ).
---------------------------------------------
all a ( (exists b ((all c ((exists d (d*c=b)))) & (exists e f (e*f=e)))) -> (exists g h (g*h=g)) ).
all a ( (exists b (b*a=a)) & (exists c ((all d ((exists e (e*d=c)))) & (exists f g (f*g=f)))) -> (exists h i ((all j (h*j=i)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
302. ((all a ((exists b (b*a=a)))) & (exists c ((all d ((exists e (e*c=d))))))) <-> ((exists f ((all g ((exists h (h*f=g)))))) & (exists i ((all j ((exists k (k*j=i))))))).
(all a ((exists b (b*a=a)))) & (exists c ((all d ((exists e (e*c=d)))))) -> (exists f ((all g ((exists h (h*g=f)))))). sos
(exists a ((all b ((exists c (c*a=b)))))) & (exists d ((all e ((exists f (f*e=d)))))) -> (all g ((exists h (h*g=g)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
303. ((all a ((exists b (b*a=b))))) <-> ((exists c ((all d ((exists e (-(d*e=c))))))) & (all f ((exists g (g*f=g))))).
(all a ((exists b (b*a=b)))) -> (exists c ((all d ((exists e (-(d*e=c))))))). max_proofs 2
304. ((all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d)))))))) <-> ((exists g ((all h ((exists i (-(h*i=g))))))) & (all j ((exists k ((all l (j*l=k))))))).
(exists a ((all b ((exists c (-(b*c=a))))))) & (all d ((exists e ((all f (d*f=e)))))) -> (all g ((exists h ((all i (g*i=h)))) & (exists j ((all k l (-(k*l=j))))))). max_proofs 4
(all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))))) -> (exists g ((all h ((exists i (-(h*i=g))))))).
---------------------------------------------
(all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))))) -> (exists g ((all h i (-(h*i=g))))).
(exists a ((all b c (-(b*c=a))))) -> (exists d ((all e ((exists f (-(e*f=d))))))).
305. ((exists a ((all b ((exists c (-(a*c=b)))))))) <-> ((exists d ((all e ((exists f (-(e*f=d))))))) & (exists g ((all h ((exists i (-(g*i=h)))))))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(197) [N] s.t. (exists a ((all b ((exists c (-(b*c=a))))))) & (exists d ((all e ((exists f (-(f*e=d))))))) " aryabhata non_assoc 6 "
(198) [N] s.t. (exists a ((all b ((exists c (-(b*c=a))))))) & (exists d ((all e ((exists f (f*e=d)))))) " aryabhata non_assoc 7 "
306. ((all a b ((exists c (-(a*c=b)))))) <-> ((exists d ((all e ((exists f (-(e*f=d))))))) & (all g h ((exists i (-(g*i=h)))))).
(all a b ((exists c (-(a*c=b))))) -> (exists d ((all e ((exists f (-(e*f=d))))))). max_proofs 0
307. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a b ((all c (a*c=b)))) & (all d ((exists e (d*e=d))))). max_proofs 8
(199) [N] s.t. (exists a b ((all c (a*c=b)))) & (all d ((exists e (e*d=d)))) " aristarchus non_assoc 6 "
308. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a b ((all c (a*c=b)))) & (all d ((exists e (e*d=e))))). max_proofs 5
309. ((all a ((exists b ((all c (a*c=b))))))) <-> ((exists d e ((all f (d*f=e)))) & (all g ((exists h ((all i (g*i=h))))))).
(200) [N] s.t. (exists a b ((all c (a*c=b)))) & (exists d ((all e ((exists f (-(d*f=e))))))) " aristarchus non_assoc 7 "
310. ((exists a b ((all c (a*c=b))))) <-> ((exists d e ((all f (d*f=e)))) & (exists g ((all h ((exists i (-(i*h=g)))))))).
(exists a b ((all c (a*c=b)))) -> (exists d ((all e ((exists f (-(f*e=d))))))). max_proofs 2
311. ((exists a b ((all c (a*c=b))))) <-> ((exists d e ((all f (d*f=e)))) & (exists g ((all h ((exists i (i*h=g))))))).
(exists a b ((all c (a*c=b)))) -> (exists d ((all e ((exists f (f*e=d)))))). max_proofs 0
312. ((exists a ((exists b ((all c (a*c=b)))) & (exists d ((all e ((exists f (d*f=e))))))))) <-> ((exists g h ((all i (g*i=h)))) & (exists j ((all k ((exists l (j*l=k))))))).
(exists a b ((all c (a*c=b)))) & (exists d ((all e ((exists f (d*f=e)))))) -> (exists g ((exists h ((all i (g*i=h)))) & (exists j ((all k ((exists l (j*l=k)))))))). max_proofs 0
(exists a ((exists b ((all c (a*c=b)))) & (exists d ((all e ((exists f (d*f=e)))))))) -> (exists g h ((all i (g*i=h)))). max_proofs 0
313. ((all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d)))))))) <-> ((exists g h ((all i (g*i=h)))) & (exists j ((all k l (-(k*l=j)))))).
(exists a b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))) -> (all g ((exists h ((all i (g*i=h)))) & (exists j ((all k l (-(k*l=j))))))). sos
(all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))))) -> (exists g h ((all i (g*i=h)))).
---------------------------------------------
(all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))))) -> (all g ((exists h ((all i (g*i=h)))))).
(all a ((exists b ((all c (a*c=b)))))) -> (exists d e ((all f (d*f=e)))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
314. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a b ((all c (a*c=b)))) & (all d e ((exists f (-(d*f=e)))))). max_proofs 3
(201) [N] s.t. (exists a b ((all c (a*c=b)))) & (exists d ((all e ((exists f (f*d=e)))))) " aristarchus non_assoc 8 "
Top Ten Sorted Concepts: [185,110,146,142,79,99,138,116,60,93]
Top Ten Sorted Conjectures: [197,114,134,152,307,125,224,283,128,106]
(202) [N] s.t. (exists a b ((all c (a*c=b)))) & (exists d ((all e ((exists f (-(e*f=d))))))) " aristarchus non_assoc 9 "
315. ((all a b ((exists c (a*c=b))))) <-> ((all d e ((exists f (d*f=e)))) & (all g ((exists h (h*g=h))))).
(all a b ((exists c (a*c=b)))) -> (all d ((exists e (e*d=e)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
316. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (a*c=b)))) & (all d ((exists e ((all f (d*f=e))))))). max_proofs 5
317. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (a*c=b)))) & (exists d ((all e ((exists f (-(f*e=d)))))))). sos
Mace generating counterexample of order: 1 2 3 4 e16
Checking whether conjectures are disproved: 45:yes(New Concept = 203),49:yes(New Concept = 204),55:yes(New Concept = 205),88:no,90:no,96:no,99:no,103:no,126:no,129:no,130:no,150:no,162:no,174:no,181:no,182:no,183:no,190:no,191:no,192:no,194:no,195:no,196:no,198:no,202:no,206:no,217:no,221:no,222:yes(New Concept = 206),225:yes(New Concept = 207),226:no,233:no,241:no,242:no,245:no,247:no,248:no,251:no,252:no,259:no,262:yes(New Concept = 208),263:no,267:yes(New Concept = 209),268:no,273:no,277:no,278:no,279:no,280:no,285:no,290:no,294:no,296:yes(New Concept = 210),300:no,301:no,302:no,305:no,313:no,315:no,317:yes(New Concept = 211),
(203) [N] s.t. (exists a ((all b ((exists c (b*c=a)))))) " abraham non_assoc 10 "
(204) [N,a] s.t. (all b ((exists c (b*c=a)))) & (exists d e ((all f (f*d=e)))) " abraham element 26 "
(205) [N] s.t. (all a b ((exists c (a*c=b)))) & (exists d e ((all f (f*d=e)))) " abraham non_assoc 11 "
(206) [N] s.t. (exists a b ((all c (c*a=b)))) & (all d ((exists e (d*e=d)))) " archytas non_assoc 5 "
(207) [N] s.t. (exists a b ((all c (c*a=b)))) & (all d ((exists e (e*d=e)))) " archytas non_assoc 6 "
(208) [N] s.t. (exists a ((all b ((exists c (a*c=b)))))) & (all d e ((exists f (-(d*f=e))))) " abraham non_assoc 12 "
(209) [N] s.t. (exists a ((all b ((exists c (-(a*c=b))))))) & (exists d ((all e ((exists f (f*e=d)))))) " aryabhata non_assoc 8 "
(210) [N,a] s.t. (exists b (a*b=a)) & (all c d ((exists e (-(c*e=d))))) " abraham element 27 "
(211) [N] s.t. (all a b ((exists c (a*c=b)))) & (exists d ((all e ((exists f (-(f*e=d))))))) " abraham non_assoc 13 "
* | 0 | 1 | 2 | 3 |
--+---+---+---+---+
0 | 1 | 0 | 3 | 2 |
--+---+---+---+---+
1 | 1 | 0 | 3 | 2 |
--+---+---+---+---+
2 | 1 | 3 | 0 | 2 |
--+---+---+---+---+
3 | 2 | 0 | 3 | 1 |
--+---+---+---+---+
Top Ten Sorted Concepts: [110,185,146,142,79,99,138,116,60,93]
Top Ten Sorted Conjectures: [197,114,134,152,307,125,224,283,128,106]
318. ((all a ((exists b (a*b=a))))) <-> ((all c ((exists d (c*d=c)))) & (exists e ((all f ((exists g (f*g=e))))))).
(all a ((exists b (a*b=a)))) -> (exists c ((all d ((exists e (d*e=c)))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
Top Ten Sorted Concepts: [110,185,146,142,79,99,138,116,93,60]
Top Ten Sorted Conjectures: [197,114,134,152,307,125,224,283,128,106]
319. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b (b*a=a)))) & (exists c ((all d ((exists e (d*e=c))))))). max_proofs 6
320. ((all a ((exists b (b*a=b))))) <-> ((all c ((exists d (d*c=d)))) & (exists e ((all f ((exists g (f*g=e))))))).
(all a ((exists b (b*a=b)))) -> (exists c ((all d ((exists e (d*e=c)))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
321. all a (((exists b (a*b=a)) & (exists c d (c*d=d)) & (exists e f ((all g (g*e=f))))) <-> ((exists h (a*h=a)) & (exists i j (i*j=j)) & (exists k ((all l ((exists m (l*m=k)))))))).
all a ( (exists b c (b*c=c)) & (exists d e ((all f (f*d=e)))) -> (exists g ((all h ((exists i (h*i=g)))))) ). max_proofs 0
all a ( (exists b c ((all d (d*b=c)))) -> (exists e ((all f ((exists g (f*g=e)))))) ). max_proofs 0
all a ( (exists b (a*b=a)) & (exists c d ((all e (e*c=d)))) -> (exists f ((all g ((exists h (g*h=f)))))) ).
---------------------------------------------
all a ( (exists b c ((all d (d*b=c)))) -> (exists e ((all f ((exists g (f*g=e)))))) ).
all a ( (exists b (a*b=a)) & (exists c d (c*d=d)) & (exists e f ((all g (g*e=f)))) -> (exists h ((all i ((exists j (i*j=h)))))) ).
---------------------------------------------
all a ( (exists b c (b*c=c)) & (exists d e ((all f (f*d=e)))) -> (exists g ((all h ((exists i (h*i=g)))))) ).
all a ( (exists b (a*b=a)) & (exists c d (c*d=d)) & (exists e ((all f ((exists g (f*g=e)))))) -> (exists h i ((all j (j*h=i)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(212) [N] s.t. (exists a ((all b ((exists c (-(c*b=a))))))) & (exists d ((all e ((exists f (e*f=d)))))) " bartholin non_assoc 3 "
322. ((exists a b ((all c (c*a=b))))) <-> ((exists d e ((all f (f*d=e)))) & (exists g ((all h ((exists i (h*i=g))))))).
(exists a b ((all c (c*a=b)))) -> (exists d ((all e ((exists f (e*f=d)))))). max_proofs 0
323. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b ((all c (a*c=b)))))) & (exists d ((all e ((exists f (e*f=d))))))). max_proofs 9
324. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b ((all c (a*c=b)))) & (exists d ((all e ((exists f (e*f=d)))))))). max_proofs 6
325. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (a*c=b)))) & (exists d ((all e ((exists f (f*e=d))))))). max_proofs 6
326. ((all a b ((exists c (a*c=b))))) <-> ((all d e ((exists f (d*f=e)))) & (exists g ((all h ((exists i (-(g*i=h)))))))).
(all a b ((exists c (a*c=b)))) -> (exists d ((all e ((exists f (-(d*f=e))))))).
---------------------------------------------
(all a b ((exists c (a*c=b)))) -> (all d ((exists e (d*e=d)))).
(all a ((exists b (a*b=a)))) -> (exists c ((all d ((exists e (-(c*e=d))))))).
327. ((all a b ((exists c (a*c=b))))) <-> ((all d e ((exists f (d*f=e)))) & (all g h ((exists i (-(g*i=h)))))).
(all a b ((exists c (a*c=b)))) -> (all d e ((exists f (-(d*f=e))))).
---------------------------------------------
(all a b ((exists c (a*c=b)))) -> (all d ((exists e (d*e=d)))).
(all a ((exists b (a*b=a)))) -> (all c d ((exists e (-(c*e=d))))).
328. ((all a b ((exists c (a*c=b))))) <-> ((all d e ((exists f (d*f=e)))) & (exists g ((all h ((exists i (h*i=g))))))).
(all a b ((exists c (a*c=b)))) -> (exists d ((all e ((exists f (e*f=d)))))). max_proofs 0
329. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (e*f=d))))))). max_proofs 6
330. all a (((exists b (a*b=a)) & (all c d ((exists e (-(c*e=d)))))) <-> ((exists f (a*f=a)) & (exists g ((all h ((exists i (h*i=g)))))))).
all a ( (exists b (a*b=a)) & (all c d ((exists e (-(c*e=d))))) -> (exists f ((all g ((exists h (g*h=f)))))) ). sos
all a ( (exists b ((all c ((exists d (c*d=b)))))) -> (all e f ((exists g (-(e*g=f))))) ). max_proofs 4
all a ( (exists b (a*b=a)) & (exists c ((all d ((exists e (d*e=c)))))) -> (all f g ((exists h (-(f*h=g))))) ).
---------------------------------------------
all a ( (exists b ((all c ((exists d (c*d=b)))))) -> (all e f ((exists g (-(e*g=f))))) ).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
331. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a ((all b ((exists c (c*b=a)))))) & (exists d ((all e ((exists f (e*f=d))))))). sos
Mace generating counterexample of order: 1 2 3 4 e17
Checking whether conjectures are disproved: 88:no,90:no,96:no,99:no,103:yes(New Concept = 213),126:no,129:yes(New Concept = 214),130:no,150:no,162:no,174:no,181:no,182:no,183:yes(New Concept = 215),190:no,191:no,192:no,194:no,195:no,196:no,198:no,202:no,206:no,217:no,221:no,226:no,233:no,241:no,242:no,245:no,247:no,248:no,251:no,252:no,259:yes(New Concept = 216),263:yes(New Concept = 217),268:no,273:no,277:no,278:no,279:no,280:no,285:no,290:yes(New Concept = 218),294:yes(New Concept = 219),300:no,301:yes(New Conjecture = 332),302:no,305:no,313:no,315:no,318:no,320:no,321:yes(New Concept = 220),330:no,331:yes(New Concept = 221),
(213) [N,a] s.t. (exists b (a*b=a)) & (exists c d (c*d=d)) & (exists e ((all f ((exists g (e*g=f)))))) " abraham element 28 "
(214) [N,a] s.t. (all b ((exists c (c*b=a)))) & (exists d e (d*e=d)) & (exists f g ((all h (f*h=g)))) " ahlfors element 36 "
(215) [N] s.t. (all a ((exists b c (b*c=a)))) & (exists d e (d*e=d)) & (exists f g ((all h (f*h=g)))) " akhiezer non_assoc 10 "
(216) [N,a] s.t. (exists b (b*a=a)) & (exists c d (c*d=c)) & (exists e ((all f ((exists g (g*f=e)))))) " ahlfors element 37 "
(217) [N] s.t. (exists a ((all b ((exists c (a*c=b)))))) & (exists d ((all e ((exists f (f*e=d)))))) " abraham non_assoc 14 "
(218) [N] s.t. (exists a ((all b ((exists c (c*b=a)))))) & (all d e ((exists f (-(d*f=e))))) " ahlfors non_assoc 17 "
(219) [N,a] s.t. (exists b (a*b=a)) & (exists c ((all d ((exists e (e*d=c)))))) " abraham element 29 "
(220) [N,a] s.t. (exists b (a*b=a)) & (exists c d (c*d=d)) & (exists e ((all f ((exists g (f*g=e)))))) " abraham element 30 "
(221) [N] s.t. (exists a ((all b ((exists c (c*b=a)))))) & (exists d ((all e ((exists f (e*f=d)))))) " ahlfors non_assoc 18 "
* | 0 | 1 | 2 | 3 |
--+---+---+---+---+
0 | 1 | 0 | 3 | 2 |
--+---+---+---+---+
1 | 3 | 0 | 3 | 2 |
--+---+---+---+---+
2 | 2 | 3 | 0 | 3 |
--+---+---+---+---+
3 | 1 | 1 | 0 | 1 |
--+---+---+---+---+
332. all a (((exists b (b*a=a)) & (exists c d (c*d=c)) & (exists e ((all f ((exists g (g*f=e))))))) <-> ((exists h (h*a=a)) & (exists i ((all j ((exists k (k*j=i)))) & (exists l m (l*m=l)))))).
all a ( (exists b c (b*c=b)) & (exists d ((all e ((exists f (f*e=d)))))) -> (exists g ((all h ((exists i (i*h=g)))) & (exists j k (j*k=j)))) ). max_proofs 0
all a ( (exists b (b*a=a)) & (exists c d (c*d=c)) & (exists e ((all f ((exists g (g*f=e)))))) -> (exists h ((all i ((exists j (j*i=h)))) & (exists k l (k*l=k)))) ).
---------------------------------------------
all a ( (exists b c (b*c=b)) & (exists d ((all e ((exists f (f*e=d)))))) -> (exists g ((all h ((exists i (i*h=g)))) & (exists j k (j*k=j)))) ).
all a ( (exists b ((all c ((exists d (d*c=b)))) & (exists e f (e*f=e)))) -> (exists g ((all h ((exists i (i*h=g)))))) ). max_proofs 0
all a ( (exists b (b*a=a)) & (exists c ((all d ((exists e (e*d=c)))) & (exists f g (f*g=f)))) -> (exists h ((all i ((exists j (j*i=h)))))) ).
---------------------------------------------
all a ( (exists b ((all c ((exists d (d*c=b)))) & (exists e f (e*f=e)))) -> (exists g ((all h ((exists i (i*h=g)))))) ).
Top Ten Sorted Concepts: [110,185,146,142,138,79,99,116,93,96]
Top Ten Sorted Conjectures: [197,323,114,134,152,307,125,224,283,128]
333. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (c*b=a)))) & (exists d e (d*e=d)) & (all f ((exists g (g*f=g)))))). max_proofs 5
Top Ten Sorted Concepts: [110,185,146,142,138,79,99,116,93,96]
Top Ten Sorted Conjectures: [197,323,114,134,152,307,125,224,283,128]
334. ((exists a ((all b ((exists c (a*c=b)))))) & (all d e ((exists f (-(d*f=e)))))) <-> ((exists g ((all h ((exists i (g*i=h)))))) & (exists j ((all k ((exists l (k*l=j))))))).
(exists a ((all b ((exists c (a*c=b)))))) & (all d e ((exists f (-(d*f=e))))) -> (exists g ((all h ((exists i (h*i=g)))))). sos
(exists a ((all b ((exists c (b*c=a)))))) -> (all d e ((exists f (-(d*f=e))))). max_proofs 4
(exists a ((all b ((exists c (a*c=b)))))) & (exists d ((all e ((exists f (e*f=d)))))) -> (all g h ((exists i (-(g*i=h))))).
---------------------------------------------
(exists a ((all b ((exists c (b*c=a)))))) -> (all d e ((exists f (-(d*f=e))))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
335. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))) & (exists g ((all h ((exists i (h*i=g)))))))). max_proofs 6
336. ((exists a ((all b ((exists c (b*c=a))))))) <-> ((exists d ((all e ((exists f (-(d*f=e))))))) & (exists g ((all h ((exists i (h*i=g))))))).
(exists a ((all b ((exists c (b*c=a)))))) -> (exists d ((all e ((exists f (-(d*f=e))))))).
---------------------------------------------
(exists a ((all b ((exists c (b*c=a)))))) -> (all d e ((exists f (-(d*f=e))))).
(all a b ((exists c (-(a*c=b))))) -> (exists d ((all e ((exists f (-(d*f=e))))))).
(222) [N,a] s.t. (exists b (b*a=a)) & (exists c ((all d ((exists e (d*e=c)))))) " ahlfors element 38 "
337. all a (((all b c (-(b*c=a))) & (all d ((exists e (e*d=e))))) <-> ((all f g (-(f*g=a))) & (exists h ((all i ((exists j (i*j=h)))))))).
all a ( (all b c (-(b*c=a))) & (all d ((exists e (e*d=e)))) -> (exists f ((all g ((exists h (g*h=f)))))) ). sos
all a ( (all b c (-(b*c=a))) & (exists d ((all e ((exists f (e*f=d)))))) -> (all g ((exists h (h*g=h)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(223) [N,a] s.t. (exists b (a*b=a)) & (exists c ((all d ((exists e (c*e=d)))))) & (exists f ((all g ((exists h (g*h=f)))))) " abraham element 31 "
Summary for session in non_assoc theory:
---------------------
Number of concepts: 223
Number of Conjectures: 337
Number of Models: 17
Largest Model Size: 4
Number of Categorisations: 154
Number of Theorems: 230
Number of Open Conjectures: 45
Number of Prime Implicants: 188
Average Proof Length: 2.9391304347826086
Average Surprisingness: 2.760869565217391
Average P.I. Proof Length: 0.7127659574468085
Number of Otter Proofs: 188
Number of HR Proofs: 86
----------------------
338. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a b ((all c (a*c=b)))) & (exists d ((all e ((exists f (e*f=d))))))). max_proofs 6
339. ((all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c)))))))) <-> ((exists f ((all g h (-(g*h=f))))) & (exists i ((all j ((exists k (j*k=i))))))).
(exists a ((all b c (-(b*c=a))))) & (exists d ((all e ((exists f (e*f=d)))))) -> (all g ((exists h (h*g=h)) & (exists i ((all j k (-(j*k=i))))))). sos
(all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c))))))) -> (exists f ((all g ((exists h (g*h=f)))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
340. ((exists a ((all b ((exists c (b*c=a))))))) <-> ((all d e ((exists f (-(d*f=e))))) & (exists g ((all h ((exists i (h*i=g))))))).
341. ((exists a b ((all c (c*a=b)))) & (exists d ((all e ((exists f (f*d=e))))))) <-> ((exists g ((all h ((exists i (i*g=h)))))) & (exists j ((all k ((exists l (k*l=j))))))).
(exists a b ((all c (c*a=b)))) & (exists d ((all e ((exists f (f*d=e)))))) -> (exists g ((all h ((exists i (h*i=g)))))).
---------------------------------------------
(exists a b ((all c (c*a=b)))) -> (exists d ((all e ((exists f (e*f=d)))))).
(exists a ((all b ((exists c (c*a=b)))))) & (exists d ((all e ((exists f (e*f=d)))))) -> (exists g h ((all i (i*g=h)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
342. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (c*b=a)))) & (exists d ((exists e (e*d=d)) & (exists f g ((all h (h*f=g)))))))). max_proofs 6
(224) [N,a] s.t. (all b ((exists c (c*b=a)))) & (exists d (-((exists e f (e*f=d)) & (all g h ((exists i (i*g=h))))))) " ahlfors element 39 "
343. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (c*b=a)))) & (all d ((exists e (e*d=e)))))). max_proofs 5
344. all a (((exists b (b*a=a)) & (all c ((exists d ((all e (c*e=d))))))) <-> ((all f ((exists g (g*f=a)))) & (all h ((exists i ((all j (h*j=i)))))))).
all a ( (exists b (b*a=a)) & (all c ((exists d ((all e (c*e=d)))))) -> (all f ((exists g (g*f=a)))) ). max_proofs 2
all a ( (all b ((exists c (c*b=a)))) -> (exists d (d*a=a)) ). max_proofs 0
all a ( (all b ((exists c (c*b=a)))) & (all d ((exists e ((all f (d*f=e)))))) -> (exists g (g*a=a)) ).
---------------------------------------------
all a ( (all b ((exists c (c*b=a)))) -> (exists d (d*a=a)) ).
345. all a (((all b ((exists c (c*b=a))))) <-> ((all d ((exists e (e*d=a)))) & (exists f ((all g ((exists h (-(h*g=f))))))))).
all a ( (all b ((exists c (c*b=a)))) -> (exists d ((all e ((exists f (-(f*e=d))))))) ).
---------------------------------------------
all a ( (all b ((exists c (c*b=a)))) -> (exists d (d*a=a)) ).
all a ( (exists b (b*a=a)) -> (exists c ((all d ((exists e (-(e*d=c))))))) ).
(225) [N,a] s.t. (all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (e*f=d)))))) " ahlfors element 40 "
(226) [N,a] s.t. (all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (-(d*f=e))))))) " ahlfors element 41 "
Top Ten Sorted Concepts: [185,110,146,142,138,79,99,116,93,96]
Top Ten Sorted Conjectures: [197,323,114,134,152,307,125,224,283,128]
(227) [N,a] s.t. -((exists b (b*a=a)) & (all c ((exists d ((all e (c*e=d))))))) " ahlfors element 42 "
346. ((all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e))))) <-> ((all g ((exists h (h*g=g)) & (all i ((exists j ((all k (i*k=j))))))))).
(all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e)))) -> (all g ((exists h (h*g=g)) & (all i ((exists j ((all k (i*k=j)))))))). sos
(all a ((exists b (b*a=a)) & (all c ((exists d ((all e (c*e=d)))))))) -> (all f g ((exists h (h*f=g)))). max_proofs 2
(all a ((exists b (b*a=a)) & (all c ((exists d ((all e (c*e=d)))))))) -> (exists f g ((all h (f*h=g)))). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
347. ((all a ((exists b ((all c (a*c=b))))))) <-> ((exists d ((exists e (e*d=d)) & (all f ((exists g ((all h (f*h=g))))))))).
(all a ((exists b ((all c (a*c=b)))))) -> (exists d ((exists e (e*d=d)) & (all f ((exists g ((all h (f*h=g)))))))). max_proofs 0
(exists a ((exists b (b*a=a)) & (all c ((exists d ((all e (c*e=d)))))))) -> (all f ((exists g ((all h (f*h=g)))))). max_proofs 0
(228) [N,a] s.t. (all b ((exists c (c*b=a)))) & (all d e ((exists f (-(d*f=e))))) " ahlfors element 43 "
348. all a (((exists b ((all c (b*c=a)))) & (exists d ((all e f (-(e*f=d)))))) <-> ((all g ((exists h (h*g=a)))) & (exists i ((all j k (-(j*k=i))))))).
all a ( (all b ((exists c (c*b=a)))) & (exists d ((all e f (-(e*f=d))))) -> (exists g ((all h (g*h=a)))) ). sos
all a ( (exists b ((all c (b*c=a)))) & (exists d ((all e f (-(e*f=d))))) -> (all g ((exists h (h*g=a)))) ).
---------------------------------------------
all a ( (exists b ((all c (b*c=a)))) -> (all d ((exists e (e*d=a)))) ).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(229) [N,a] s.t. (all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (-(e*f=d))))))) " ahlfors element 44 "
(230) [N,a] s.t. (all b ((exists c (-(a*c=b))))) & (exists d ((all e ((exists f (e*f=d)))))) " aryabhata element 12 "
(231) [N,a] s.t. (all b ((exists c (-(a*c=b))))) & (exists d ((all e ((exists f (f*e=d)))))) " aryabhata element 13 "
Top Ten Sorted Concepts: [185,110,146,142,138,99,79,116,93,96]
Top Ten Sorted Conjectures: [197,323,114,134,152,307,125,224,283,128]
(232) [N,a] s.t. (all b ((exists c (-(a*c=b))))) & (all d e ((exists f (-(d*f=e))))) " aryabhata element 14 "
349. ((exists a ((all b ((exists c (b*c=a))))))) <-> ((exists d ((all e ((exists f (-(e*f=d))))))) & (exists g ((all h ((exists i (h*i=g))))))).
(exists a ((all b ((exists c (b*c=a)))))) -> (exists d ((all e ((exists f (-(e*f=d))))))).
---------------------------------------------
(exists a ((all b ((exists c (b*c=a)))))) -> (all d e ((exists f (-(d*f=e))))).
(all a b ((exists c (-(a*c=b))))) -> (exists d ((all e ((exists f (-(e*f=d))))))).
(233) [N,a] s.t. -((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d))))) & (exists g ((all h ((exists i (i*h=g)))))) " ahlfors element 45 "
(234) [N,a] s.t. -((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d))))) & (exists g ((all h ((exists i (i*h=g)))) & (all j ((exists k l (k*l=j)))))) " ahlfors element 46 "
350. ((all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c)))))))) <-> ((exists f g (f*g=f)) & -((all h ((exists i j (i*j=h)))) & (exists k l (k*l=k)))).
(exists a b (a*b=a)) & -((all c ((exists d e (d*e=c)))) & (exists f g (f*g=f))) -> (all h ((exists i (i*h=i)) & (exists j ((all k l (-(k*l=j))))))). sos
(all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c))))))) -> (exists f g (f*g=f)). max_proofs 0
(all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c))))))) -> -((all f ((exists g h (g*h=f)))) & (exists i j (i*j=i))). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
351. ((all a ((exists b (a*b=a))))) <-> ((exists c d (c*d=c)) & (all e ((exists f (e*f=e))))).
352. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a b (a*b=a)) & (all c ((exists d (d*c=c))))). max_proofs 6
353. ((all a ((exists b (b*a=b))))) <-> ((exists c d (c*d=c)) & (all e ((exists f (f*e=f))))).
(all a ((exists b (b*a=b)))) -> (exists c d (c*d=c)). max_proofs 0
354. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a b (a*b=a)) & (all c ((exists d ((all e (c*e=d))))))). max_proofs 6
(235) [N] s.t. (exists a b (a*b=a)) & (exists c ((all d ((exists e (-(e*d=c))))))) " arbuthnot non_assoc 5 "
355. ((exists a b ((all c (c*a=b))))) <-> ((exists d e (d*e=d)) & (exists f g ((all h (h*f=g))))).
356. ((exists a ((all b ((exists c (b*c=a))))))) <-> ((exists d e (d*e=d)) & (exists f ((all g ((exists h (g*h=f))))))).
(exists a ((all b ((exists c (b*c=a)))))) -> (exists d e (d*e=d)). max_proofs 0
357. ((exists a ((all b ((exists c (c*b=a)))) & (exists d e (d*e=d))))) <-> ((exists f g (f*g=f)) & (exists h ((all i ((exists j (j*i=h))))))).
(exists a b (a*b=a)) & (exists c ((all d ((exists e (e*d=c)))))) -> (exists f ((all g ((exists h (h*g=f)))) & (exists i j (i*j=i)))). max_proofs 0
358. ((exists a ((all b ((exists c (a*c=b))))))) <-> ((exists d e (d*e=d)) & (exists f ((all g ((exists h (f*h=g))))))).
(exists a ((all b ((exists c (a*c=b)))))) -> (exists d e (d*e=d)). max_proofs 0
359. ((exists a b (a*b=a))) <-> ((exists c d (c*d=c)) & (exists e ((all f ((exists g (-(e*g=f)))))))).
(exists a b (a*b=a)) -> (exists c ((all d ((exists e (-(c*e=d))))))). max_proofs 4
360. ((all a ((exists b c (b*c=a)))) & (exists d e (d*e=d)) & (exists f g ((all h (f*h=g))))) <-> ((exists i j (i*j=i)) & (exists k l ((all m (k*m=l))))).
(exists a b (a*b=a)) & (exists c d ((all e (c*e=d)))) -> (all f ((exists g h (g*h=f)))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
361. ((exists a ((all b ((exists c (b*c=a))))))) <-> ((exists d e (d*e=d)) & (all f g ((exists h (-(f*h=g)))))).
(exists a b (a*b=a)) & (all c d ((exists e (-(c*e=d))))) -> (exists f ((all g ((exists h (g*h=f)))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
362. ((all a ((exists b (b*a=b)) & (exists c ((all d e (-(d*e=c)))))))) <-> ((exists f g (f*g=f)) & (exists h ((all i j (-(i*j=h)))))).
(exists a b (a*b=a)) & (exists c ((all d e (-(d*e=c))))) -> (all f ((exists g (g*f=g)) & (exists h ((all i j (-(i*j=h))))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
363. ((exists a b ((all c (c*a=b)))) & (exists d ((all e ((exists f (f*d=e))))))) <-> ((exists g h (g*h=g)) & (exists i ((all j ((exists k (k*i=j))))))).
(exists a b (a*b=a)) & (exists c ((all d ((exists e (e*c=d)))))) -> (exists f g ((all h (h*f=g)))). sos
(exists a b ((all c (c*a=b)))) & (exists d ((all e ((exists f (f*d=e)))))) -> (exists g h (g*h=g)).
---------------------------------------------
(exists a b ((all c (c*a=b)))) -> (exists d e (d*e=d)).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
364. ((exists a b (a*b=a))) <-> ((exists c d (c*d=c)) & (exists e ((all f ((exists g (-(f*g=e)))))))).
(exists a b (a*b=a)) -> (exists c ((all d ((exists e (-(d*e=c))))))). max_proofs 2
365. ((exists a ((exists b (b*a=a)) & (exists c d (c*d=c))))) <-> ((exists e f (e*f=e)) & (exists g h (g*h=h))).
(236) [N,a] s.t. -((exists b c (b*c=a)) & (all d e ((exists f (d*f=e))))) " akhiezer element 8 "
Top Ten Sorted Concepts: [185,110,142,138,99,116,79,93,96,60]
Top Ten Sorted Conjectures: [197,323,114,134,152,307,125,224,283,128]
366. ((all a b ((exists c (a*c=b))))) <-> ((all d ((exists e f (e*f=d)) & (all g h ((exists i (g*i=h))))))).
(all a b ((exists c (a*c=b)))) -> (all d ((exists e f (e*f=d)) & (all g h ((exists i (g*i=h)))))). max_proofs 0
(all a ((exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))))) -> (all g h ((exists i (g*i=h)))). max_proofs 0
367. ((all a b ((exists c (a*c=b))))) <-> ((exists d ((exists e f (e*f=d)) & (all g h ((exists i (g*i=h))))))).
(all a b ((exists c (a*c=b)))) -> (exists d ((exists e f (e*f=d)) & (all g h ((exists i (g*i=h)))))). max_proofs 0
(exists a ((exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))))) -> (all g h ((exists i (g*i=h)))). max_proofs 0
368. all a (((exists b c (b*c=a)) & (all d e ((exists f (d*f=e))))) <-> ((exists g h (g*h=a)) & (all i j ((exists k (i*k=j)))) & (all l ((exists m (l*m=l)))))).
all a ( (exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) -> (all g ((exists h (g*h=g)))) ).
---------------------------------------------
all a ( (all b c ((exists d (b*d=c)))) -> (all e ((exists f (e*f=e)))) ).
369. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) & (all g ((exists h (h*g=g)))))). max_proofs 6
370. all a (((exists b c (b*c=a)) & (all d e ((exists f (d*f=e))))) <-> ((exists g h (g*h=a)) & (all i j ((exists k (i*k=j)))) & (all l ((exists m (m*l=m)))))).
all a ( (exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) -> (all g ((exists h (h*g=h)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
371. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) & (all g ((exists h ((all i (g*i=h)))))))). max_proofs 9
(237) [N,a] s.t. (exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) & (exists g h ((all i (i*g=h)))) " akhiezer element 9 "
372. all a (((exists b c (b*c=a)) & (all d e ((exists f (d*f=e))))) <-> ((exists g h (g*h=a)) & (all i j ((exists k (i*k=j)))) & (exists l ((all m ((exists n (m*n=l)))))))).
all a ( (all b c ((exists d (b*d=c)))) -> (exists e ((all f ((exists g (f*g=e)))))) ). max_proofs 0
all a ( (exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) -> (exists g ((all h ((exists i (h*i=g)))))) ).
---------------------------------------------
all a ( (all b c ((exists d (b*d=c)))) -> (exists e ((all f ((exists g (f*g=e)))))) ).
373. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) & (all g h ((exists i (i*g=h)))))). max_proofs 6
374. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) & (exists g ((all h ((exists i (i*h=g)))))))). max_proofs 6
375. all a (((exists b c (b*c=a)) & (all d e ((exists f (d*f=e))))) <-> ((exists g h (g*h=a)) & (all i j ((exists k (i*k=j)))) & (exists l ((all m ((exists n (l*n=m)))))))).
all a ( (all b c ((exists d (b*d=c)))) -> (exists e ((all f ((exists g (e*g=f)))))) ).
---------------------------------------------
all a ( (all b c ((exists d (b*d=c)))) -> (all e ((exists f (a*f=e)))) ).
all a ( (all b ((exists c (a*c=b)))) -> (exists d ((all e ((exists f (d*f=e)))))) ).
all a ( (exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) -> (exists g ((all h ((exists i (g*i=h)))))) ).
---------------------------------------------
all a ( (all b c ((exists d (b*d=c)))) -> (all e ((exists f (a*f=e)))) ).
all a ( (all b ((exists c (a*c=b)))) -> (exists d ((all e ((exists f (d*f=e)))))) ).
376. all a (((exists b c (b*c=a)) & (all d e ((exists f (d*f=e))))) <-> ((exists g h (g*h=a)) & (all i j ((exists k (i*k=j)))) & (exists l m (l*m=l)))).
all a ( (all b c ((exists d (b*d=c)))) -> (exists e f (e*f=e)) ).
---------------------------------------------
all a ( (all b c ((exists d (b*d=c)))) -> (all e ((exists f (e*f=a)))) ).
all a ( (all b ((exists c (b*c=a)))) -> (exists d e (d*e=d)) ).
all a ( (exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) -> (exists g h (g*h=g)) ).
---------------------------------------------
all a ( (all b c ((exists d (b*d=c)))) -> (all e ((exists f (e*f=a)))) ).
all a ( (all b ((exists c (b*c=a)))) -> (exists d e (d*e=d)) ).
377. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) & (exists g h ((all i (g*i=h)))))). max_proofs 6
378. all a (((exists b c (b*c=a)) & (all d e ((exists f (d*f=e))))) <-> ((exists g h (g*h=a)) & (all i j ((exists k (i*k=j)))) & (all l m ((exists n (-(l*n=m))))))).
all a ( (all b c ((exists d (b*d=c)))) -> (all e f ((exists g (-(e*g=f))))) ).
---------------------------------------------
all a ( (all b c ((exists d (b*d=c)))) -> (exists e ((all f ((exists g (f*g=e)))))) ).
all a ( (exists b ((all c ((exists d (c*d=b)))))) -> (all e f ((exists g (-(e*g=f))))) ).
all a ( (exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) -> (all g h ((exists i (-(g*i=h))))) ).
---------------------------------------------
all a ( (all b c ((exists d (b*d=c)))) -> (exists e ((all f ((exists g (f*g=e)))))) ).
all a ( (exists b ((all c ((exists d (c*d=b)))))) -> (all e f ((exists g (-(e*g=f))))) ).
379. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) & (exists g ((all h i (-(h*i=g))))))). max_proofs 5
380. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) & (exists g ((all h ((exists i (i*g=h)))))))). max_proofs 6
381. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) & (exists g h (g*h=h)))). max_proofs 6
382. all a (((exists b c (b*c=a)) & (all d e ((exists f (d*f=e))))) <-> ((exists g h (g*h=a)) & (all i j ((exists k (i*k=j)))) & (all l ((exists m n (m*n=l)))))).
all a ( (all b c ((exists d (b*d=c)))) -> (all e ((exists f g (f*g=e)))) ).
---------------------------------------------
all a ( (all b c ((exists d (b*d=c)))) -> (all e ((exists f (a*f=e)))) ).
all a ( (all b ((exists c (a*c=b)))) -> (all d ((exists e f (e*f=d)))) ).
all a ( (exists b c (b*c=a)) & (all d e ((exists f (d*f=e)))) -> (all g ((exists h i (h*i=g)))) ).
---------------------------------------------
all a ( (all b c ((exists d (b*d=c)))) -> (all e ((exists f (a*f=e)))) ).
all a ( (all b ((exists c (a*c=b)))) -> (all d ((exists e f (e*f=d)))) ).
383. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (b*c=a)))) & (all d ((exists e (e*d=d)))))). max_proofs 6
(238) [N,a] s.t. (all b ((exists c (b*c=a)))) & (all d ((exists e (e*d=e)))) " abraham element 32 "
384. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (b*c=a)))) & (all d ((exists e ((all f (d*f=e)))))))). max_proofs 7
(239) [N,a] s.t. (all b ((exists c (b*c=a)))) & (exists d ((all e ((exists f (-(f*e=d))))))) " abraham element 33 "
(240) [N,a] s.t. (all b ((exists c (b*c=a)))) & (exists d ((all e ((exists f (f*e=d)))))) " abraham element 34 "
385. all a (((all b ((exists c (b*c=a))))) <-> ((all d ((exists e (d*e=a)))) & (exists f ((all g ((exists h (-(f*h=g))))))))).
all a ( (all b ((exists c (b*c=a)))) -> (exists d ((all e ((exists f (-(d*f=e))))))) ). max_proofs 5
(241) [N,a] s.t. (all b ((exists c (b*c=a)))) & (exists d ((all e ((exists f (d*f=e)))))) " abraham element 35 "
Top Ten Sorted Concepts: [185,110,142,138,79,99,116,93,96,60]
Top Ten Sorted Conjectures: [197,371,323,114,134,152,307,125,384,224]
386. all a (((all b ((exists c (b*c=a))))) <-> ((all d ((exists e (d*e=a)))) & (all f g ((exists h (-(f*h=g))))))).
all a ( (all b ((exists c (b*c=a)))) -> (all d e ((exists f (-(d*f=e))))) ). max_proofs 4
(242) [N,a] s.t. (all b ((exists c (b*c=a)))) & (exists d ((all e f (-(e*f=d))))) " abraham element 36 "
(243) [N,a] s.t. (all b ((exists c (b*c=a)))) & (exists d ((all e ((exists f (f*d=e)))))) " abraham element 37 "
387. all a (((all b ((exists c (b*c=a))))) <-> ((all d ((exists e (d*e=a)))) & (exists f ((all g ((exists h (-(g*h=f))))))))).
all a ( (all b ((exists c (b*c=a)))) -> (exists d ((all e ((exists f (-(e*f=d))))))) ). max_proofs 2
388. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a b (a*b=b)) & (all c ((exists d (c*d=c))))). max_proofs 6
389. ((all a ((exists b (b*a=a))))) <-> ((exists c d (c*d=d)) & (all e ((exists f (f*e=e))))).
(all a ((exists b (b*a=a)))) -> (exists c d (c*d=d)). max_proofs 0
390. ((all a ((exists b ((all c (a*c=b))))))) <-> ((exists d e (d*e=e)) & (all f ((exists g ((all h (f*h=g))))))).
(all a ((exists b ((all c (a*c=b)))))) -> (exists d e (d*e=e)). max_proofs 0
391. ((all ax1 ax2 (ax1 = ax2))) <-> ((exists a b (a*b=b)) & (all c ((exists d (d*c=d))))). max_proofs 5
392. ((exists a b (a*b=b))) <-> ((exists c d (c*d=d)) & (exists e ((all f ((exists g (-(g*f=e)))))))).
(exists a b (a*b=b)) -> (exists c ((all d ((exists e (-(e*d=c))))))). max_proofs 2
393. ((exists a ((exists b (b*a=a)) & (exists c d ((all e (e*c=d))))))) <-> ((exists f g (f*g=g)) & (exists h i ((all j (j*h=i))))).
(exists a b (a*b=b)) & (exists c d ((all e (e*c=d)))) -> (exists f ((exists g (g*f=f)) & (exists h i ((all j (j*h=i)))))). max_proofs 0
(exists a ((exists b (b*a=a)) & (exists c d ((all e (e*c=d)))))) -> (exists f g (f*g=g)). max_proofs 0
(exists a ((exists b (b*a=a)) & (exists c d ((all e (e*c=d)))))) -> (exists f g ((all h (h*f=g)))). max_proofs 0
(244) [N] s.t. (exists a b (a*b=b)) & (exists c ((all d ((exists e (d*e=c)))))) " archimedes non_assoc 2 "
394. ((exists a ((all b ((exists c (c*b=a))))))) <-> ((exists d e (d*e=e)) & (exists f ((all g ((exists h (h*g=f))))))).
(exists a ((all b ((exists c (c*b=a)))))) -> (exists d e (d*e=e)). max_proofs 0
(245) [N] s.t. (exists a b (a*b=b)) & (exists c ((all d ((exists e (-(c*e=d))))))) " archimedes non_assoc 3 "
395. ((exists a b ((all c (a*c=b))))) <-> ((exists d e (d*e=e)) & (exists f g ((all h (f*h=g))))).
(exists a b ((all c (a*c=b)))) -> (exists d e (d*e=e)).
---------------------------------------------
(exists a b ((all c (a*c=b)))) -> (exists d ((all e ((exists f (f*e=d)))))).
(exists a ((all b ((exists c (c*b=a)))))) -> (exists d e (d*e=e)).
(246) [N] s.t. (exists a b (a*b=b)) & (exists c ((all d ((exists e (c*e=d)))))) " archimedes non_assoc 4 "
Top Ten Sorted Concepts: [110,185,142,138,99,79,116,93,96,60]
Top Ten Sorted Conjectures: [197,371,323,114,134,152,307,125,384,224]
(247) [N] s.t. (exists a b (a*b=b)) & (all c d ((exists e (-(c*e=d))))) " archimedes non_assoc 5 "
396. ((all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d)))))))) <-> ((exists g h (g*h=h)) & (exists i ((all j k (-(j*k=i)))))).
(exists a b (a*b=b)) & (exists c ((all d e (-(d*e=c))))) -> (all f ((exists g ((all h (f*h=g)))) & (exists i ((all j k (-(j*k=i))))))). sos
(all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))))) -> (exists g h (g*h=h)).
---------------------------------------------
(all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))))) -> (all g ((exists h ((all i (g*i=h)))))).
(all a ((exists b ((all c (a*c=b)))))) -> (exists d e (d*e=e)).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(248) [N] s.t. (exists a b (a*b=b)) & (exists c ((all d ((exists e (-(d*e=c))))))) " archimedes non_assoc 6 "
397. ((exists a ((all b ((exists c (c*a=b))))))) <-> ((exists d e (d*e=e)) & (exists f ((all g ((exists h (h*f=g))))))).
(exists a ((all b ((exists c (c*a=b)))))) -> (exists d e (d*e=e)). max_proofs 0
398. ((all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d)))))))) <-> ((exists g h (g*h=h)) & -((all i ((exists j k (j*k=i)))) & (exists l m (l*m=m)))).
(exists a b (a*b=b)) & -((all c ((exists d e (d*e=c)))) & (exists f g (f*g=g))) -> (all h ((exists i ((all j (h*j=i)))) & (exists k ((all l m (-(l*m=k))))))). sos
(all a ((exists b ((all c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))))) -> -((all g ((exists h i (h*i=g)))) & (exists j k (j*k=k))). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
399. ((exists a ((all b ((exists c (-(b*c=a)))))))) <-> (-((all d e ((exists f (f*d=e)))) & (exists g h ((all i (g*i=h)))))).
(exists a ((all b ((exists c (-(b*c=a))))))) -> -((all d e ((exists f (f*d=e)))) & (exists g h ((all i (g*i=h))))). sos
-((all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e))))) -> (exists g ((all h ((exists i (-(h*i=g))))))). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
Summary for session in non_assoc theory:
---------------------
Number of concepts: 248
Number of Conjectures: 399
Number of Models: 17
Largest Model Size: 4
Number of Categorisations: 173
Number of Theorems: 279
Number of Open Conjectures: 58
Number of Prime Implicants: 220
Average Proof Length: 2.881720430107527
Average Surprisingness: 2.738351254480287
Average P.I. Proof Length: 0.7136363636363636
Number of Otter Proofs: 220
Number of HR Proofs: 104
----------------------
400. ((all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e))))) <-> ((all g h ((exists i (i*g=h)))) & (exists j k ((all l (j*l=k)))) & (all m ((exists n (n*m=m))))).
401. ((all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e))))) <-> ((all g h ((exists i (i*g=h)))) & (exists j k ((all l (j*l=k)))) & (all m ((exists n ((all o (m*o=n))))))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
402. ((all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e))))) <-> ((all g h ((exists i (i*g=h)))) & (exists j k ((all l (j*l=k)))) & (exists m ((all n ((exists o (o*n=m))))))).
(all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e)))) -> (exists g ((all h ((exists i (i*h=g)))))).
---------------------------------------------
(all a b ((exists c (c*a=b)))) -> (exists d ((all e ((exists f (f*e=d)))))).
403. ((all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e))))) <-> ((all g h ((exists i (i*g=h)))) & (exists j k ((all l (j*l=k)))) & (exists m ((all n ((exists o (o*m=n))))))).
(249) [N,a] s.t. -((all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e))))))) " ahlfors element 47 "
404. ((all a b ((exists c (c*a=b))))) <-> ((all d ((all e ((exists f (f*e=d)))) & (exists g ((all h ((exists i (i*g=h))))))))).
(all a b ((exists c (c*a=b)))) -> (all d ((all e ((exists f (f*e=d)))) & (exists g ((all h ((exists i (i*g=h)))))))). max_proofs 0
(all a ((all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e)))))))) -> (all g h ((exists i (i*g=h)))). max_proofs 0
405. ((all a ((exists b (b*a=a)))) & (exists c ((all d ((exists e (e*c=d))))))) <-> ((exists f ((all g ((exists h (h*g=f)))) & (exists i ((all j ((exists k (k*i=j))))))))).
(all a ((exists b (b*a=a)))) & (exists c ((all d ((exists e (e*c=d)))))) -> (exists f ((all g ((exists h (h*g=f)))) & (exists i ((all j ((exists k (k*i=j)))))))). sos
(exists a ((all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e)))))))) -> (all g ((exists h (h*g=g)))). sos
(exists a ((all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e)))))))) -> (exists g ((all h ((exists i (i*g=h)))))). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(250) [N,a] s.t. -((all b ((exists c (c*b=a)))) & (all d ((exists e (e*d=d))))) " ahlfors element 48 "
406. ((all a b ((exists c (c*a=b))))) <-> ((all d ((all e ((exists f (f*e=d)))) & (all g ((exists h (h*g=g))))))).
(all a b ((exists c (c*a=b)))) -> (all d ((all e ((exists f (f*e=d)))) & (all g ((exists h (h*g=g)))))). max_proofs 0
(all a ((all b ((exists c (c*b=a)))) & (all d ((exists e (e*d=d)))))) -> (all f g ((exists h (h*f=g)))). max_proofs 0
407. ((all a ((exists b (b*a=a))))) <-> ((exists c ((all d ((exists e (e*d=c)))) & (all f ((exists g (g*f=f))))))).
(all a ((exists b (b*a=a)))) -> (exists c ((all d ((exists e (e*d=c)))) & (all f ((exists g (g*f=f)))))). sos
(exists a ((all b ((exists c (c*b=a)))) & (all d ((exists e (e*d=d)))))) -> (all f ((exists g (g*f=f)))). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
408. all a (((all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e))))))) <-> ((all g ((exists h (h*g=a)))) & (all i ((exists j (j*i=i)))) & (exists k ((all l ((exists m (m*k=l)))))))).
all a ( (all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e)))))) -> (all g ((exists h (h*g=g)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(251) [N,a] s.t. -((exists b (a*b=a)) & (exists c d ((all e (c*e=d))))) " abraham element 38 "
Top Ten Sorted Concepts: [110,185,142,138,99,116,79,93,96,60]
Top Ten Sorted Conjectures: [197,371,323,114,134,152,307,125,384,224]
409. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b (a*b=a)) & (exists c d ((all e (c*e=d))))))). max_proofs 6
410. ((all a ((exists b c (b*c=a)))) & (exists d e (d*e=d)) & (exists f g ((all h (f*h=g))))) <-> ((exists i ((exists j (i*j=i)) & (exists k l ((all m (k*m=l))))))).
(exists a b (a*b=a)) & (exists c d ((all e (c*e=d)))) -> (exists f ((exists g (f*g=f)) & (exists h i ((all j (h*j=i)))))). max_proofs 0
(all a ((exists b c (b*c=a)))) & (exists d e (d*e=d)) & (exists f g ((all h (f*h=g)))) -> (exists i ((exists j (i*j=i)) & (exists k l ((all m (k*m=l)))))).
---------------------------------------------
(exists a b (a*b=a)) & (exists c d ((all e (c*e=d)))) -> (exists f ((exists g (f*g=f)) & (exists h i ((all j (h*j=i)))))).
(exists a ((exists b (a*b=a)) & (exists c d ((all e (c*e=d)))))) -> (all f ((exists g h (g*h=f)))). sos
(exists a ((exists b (a*b=a)) & (exists c d ((all e (c*e=d)))))) -> (exists f g (f*g=f)). max_proofs 0
(exists a ((exists b (a*b=a)) & (exists c d ((all e (c*e=d)))))) -> (exists f g ((all h (f*h=g)))). max_proofs 0
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
411. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b (a*b=a)) & (exists c d ((all e (c*e=d)))) & (all f ((exists g (f*g=f)))))). max_proofs 8
412. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b (a*b=a)) & (exists c d ((all e (c*e=d)))) & (all f ((exists g ((all h (f*h=g)))))))). max_proofs 6
413. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b (a*b=a)) & (exists c d ((all e (c*e=d)))) & (exists f ((all g ((exists h (g*h=f)))))))). max_proofs 6
414. all a (((all b ((exists c (a*c=b)))) & (exists d e ((all f (d*f=e))))) <-> ((exists g (a*g=a)) & (exists h i ((all j (h*j=i)))) & (exists k ((all l ((exists m (k*m=l)))))))).
all a ( (exists b (a*b=a)) & (exists c d ((all e (c*e=d)))) & (exists f ((all g ((exists h (f*h=g)))))) -> (all i ((exists j (a*j=i)))) ). sos
all a ( (all b ((exists c (a*c=b)))) & (exists d e ((all f (d*f=e)))) -> (exists g (a*g=a)) ).
---------------------------------------------
all a ( (all b ((exists c (a*c=b)))) -> (exists d (a*d=a)) ).
all a ( (all b ((exists c (a*c=b)))) & (exists d e ((all f (d*f=e)))) -> (exists g ((all h ((exists i (g*i=h)))))) ).
---------------------------------------------
all a ( (all b ((exists c (a*c=b)))) -> (exists d ((all e ((exists f (d*f=e)))))) ).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
415. all a (((exists b (b*a=a)) & (all c ((exists d ((all e (c*e=d))))))) <-> ((exists f ((all g (f*g=a)))) & (all h ((exists i ((all j (h*j=i)))))))).
all a ( (exists b (b*a=a)) & (all c ((exists d ((all e (c*e=d)))))) -> (exists f ((all g (f*g=a)))) ). max_proofs 2
all a ( (exists b ((all c (b*c=a)))) & (all d ((exists e ((all f (d*f=e)))))) -> (exists g (g*a=a)) ).
---------------------------------------------
all a ( (exists b ((all c (b*c=a)))) -> (exists d (d*a=a)) ).
416. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b ((all c (b*c=a)))) & (all d ((exists e (e*d=e)))))). max_proofs 5
417. all a (((exists b ((all c (b*c=a))))) <-> ((exists d ((all e (d*e=a)))) & (exists f ((all g ((exists h (-(h*g=f))))))))).
all a ( (exists b ((all c (b*c=a)))) -> (exists d ((all e ((exists f (-(f*e=d))))))) ).
---------------------------------------------
all a ( (exists b ((all c (b*c=a)))) -> (exists d (d*a=a)) ).
all a ( (exists b (b*a=a)) -> (exists c ((all d ((exists e (-(e*d=c))))))) ).
418. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b ((all c (b*c=a)))) & (exists d ((all e ((exists f (e*f=d)))))))). max_proofs 9
419. all a (((exists b ((all c (b*c=a))))) <-> ((exists d ((all e (d*e=a)))) & (exists f ((all g ((exists h (h*g=f)))))))).
all a ( (exists b ((all c (b*c=a)))) -> (exists d ((all e ((exists f (f*e=d)))))) ). max_proofs 0
(252) [N,a] s.t. (exists b ((all c (b*c=a)))) & (exists d ((all e ((exists f (-(d*f=e))))))) " aristarchus element 15 "
420. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((exists b ((all c (b*c=a)))) & (all d e ((exists f (-(d*f=e))))))). max_proofs 3
(253) [N,a] s.t. (exists b ((all c (b*c=a)))) & (exists d ((all e ((exists f (-(e*f=d))))))) " aristarchus element 16 "
421. ((exists a (-((exists b (a*b=a)) & (exists c ((all d ((exists e (c*e=d)))))))))) <-> (-((all f ((exists g (f*g=f)))) & (exists h ((all i ((exists j (h*j=i)))))))).
(exists a (-((exists b (a*b=a)) & (exists c ((all d ((exists e (c*e=d))))))))) -> -((all f ((exists g (f*g=f)))) & (exists h ((all i ((exists j (h*j=i))))))). max_proofs 0
-((all a ((exists b (a*b=a)))) & (exists c ((all d ((exists e (c*e=d))))))) -> (exists f (-((exists g (f*g=f)) & (exists h ((all i ((exists j (h*j=i))))))))). max_proofs 0
(254) [N] s.t. -((all a ((exists b (b*a=a)))) & (exists c ((all d ((exists e (e*c=d))))))) " ahlfors non_assoc 19 "
(255) [N,a] s.t. -((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))) & (exists g ((all h ((exists i (i*h=g)))))) " akhiezer element 10 "
(256) [N,a] s.t. -((exists b (a*b=a)) & (all c d ((exists e (-(c*e=d)))))) " abraham element 39 "
Top Ten Sorted Concepts: [110,185,142,138,99,116,79,93,96,60]
Top Ten Sorted Conjectures: [197,371,323,418,114,134,152,307,125,411]
422. ((all a ((exists b (a*b=a))))) <-> ((all c ((exists d (c*d=c)) & (all e f ((exists g (-(e*g=f)))))))).
(all a ((exists b (a*b=a)))) -> (all c ((exists d (c*d=c)) & (all e f ((exists g (-(e*g=f))))))). max_proofs 5
(all a ((exists b (a*b=a)) & (all c d ((exists e (-(c*e=d))))))) -> (all f ((exists g (f*g=f)))). max_proofs 0
423. ((exists a ((all b ((exists c (b*c=a))))))) <-> ((exists d ((exists e (d*e=d)) & (all f g ((exists h (-(f*h=g)))))))).
(exists a ((all b ((exists c (b*c=a)))))) -> (exists d ((exists e (d*e=d)) & (all f g ((exists h (-(f*h=g))))))). max_proofs 5
(exists a ((exists b (a*b=a)) & (all c d ((exists e (-(c*e=d))))))) -> (exists f ((all g ((exists h (g*h=f)))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
424. all a (((all b ((exists c (c*a=b)))) & (exists d e (d*e=d))) <-> ((all f ((exists g (g*a=f)))) & (exists h ((exists i (i*h=h)) & (exists j k ((all l (l*j=k)))))))).
all a ( (all b ((exists c (c*a=b)))) & (exists d e (d*e=d)) -> (exists f ((exists g (g*f=f)) & (exists h i ((all j (j*h=i)))))) ). sos
all a ( (exists b ((exists c (c*b=b)) & (exists d e ((all f (f*d=e)))))) -> (exists g h (g*h=g)) ). max_proofs 0
all a ( (all b ((exists c (c*a=b)))) & (exists d ((exists e (e*d=d)) & (exists f g ((all h (h*f=g)))))) -> (exists i j (i*j=i)) ).
---------------------------------------------
all a ( (exists b ((exists c (c*b=b)) & (exists d e ((all f (f*d=e)))))) -> (exists g h (g*h=g)) ).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(257) [N,a] s.t. (all b ((exists c (c*a=b)))) & (exists d (-((exists e f (e*f=d)) & (all g h ((exists i (i*g=h))))))) " ahlfors element 49 "
(258) [N,a] s.t. (all b ((exists c (c*a=b)))) & (all d ((exists e ((all f (d*f=e)))))) " ahlfors element 50 "
425. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (c*a=b)))) & (all d ((exists e (e*d=e)))))). max_proofs 5
426. all a (((all b ((exists c (c*a=b)))) & (exists d e (d*e=d))) <-> ((all f ((exists g (g*a=f)))) & (exists h ((exists i (i*h=h)) & (exists j k (j*k=j)))))).
all a ( (all b ((exists c (c*a=b)))) & (exists d e (d*e=d)) -> (exists f ((exists g (g*f=f)) & (exists h i (h*i=h)))) ). max_proofs 0
all a ( (all b ((exists c (c*a=b)))) & (exists d ((exists e (e*d=d)) & (exists f g (f*g=f)))) -> (exists h i (h*i=h)) ).
---------------------------------------------
all a ( (exists b ((exists c (c*b=b)) & (exists d e (d*e=d)))) -> (exists f g (f*g=f)) ).
427. all a (((all b ((exists c (c*a=b))))) <-> ((all d ((exists e (e*a=d)))) & (exists f ((all g ((exists h (-(h*g=f))))))))).
all a ( (all b ((exists c (c*a=b)))) -> (exists d ((all e ((exists f (-(f*e=d))))))) ).
---------------------------------------------
all a ( (all b ((exists c (c*a=b)))) -> (exists d (d*a=a)) ).
all a ( (exists b (b*a=a)) -> (exists c ((all d ((exists e (-(e*d=c))))))) ).
428. all a (((all b ((exists c (c*a=b)))) & (exists d e (d*e=d))) <-> ((all f ((exists g (g*a=f)))) & (exists h ((all i ((exists j (i*j=h)))))))).
all a ( (all b ((exists c (c*a=b)))) & (exists d e (d*e=d)) -> (exists f ((all g ((exists h (g*h=f)))))) ). sos
all a ( (exists b ((all c ((exists d (c*d=b)))))) -> (exists e f (e*f=e)) ). max_proofs 0
all a ( (all b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (e*f=d)))))) -> (exists g h (g*h=g)) ).
---------------------------------------------
all a ( (exists b ((all c ((exists d (c*d=b)))))) -> (exists e f (e*f=e)) ).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
429. all a (((all b ((exists c (c*a=b)))) & (all d ((exists e (e*d=d))))) <-> ((all f ((exists g (g*a=f)))) & (exists h ((all i ((exists j (j*i=h)))))))).
all a ( (all b ((exists c (c*a=b)))) & (all d ((exists e (e*d=d)))) -> (exists f ((all g ((exists h (h*g=f)))))) ). sos
all a ( (all b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (f*e=d)))))) -> (all g ((exists h (h*g=g)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(259) [N,a] s.t. (all b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (-(d*f=e))))))) " ahlfors element 51 "
(260) [N,a] s.t. (all b ((exists c (c*a=b)))) & (all d e ((exists f (-(d*f=e))))) " ahlfors element 52 "
430. all a (((all b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (-(d*f=e)))))))) <-> ((all g ((exists h (h*a=g)))) & (exists i ((all j ((exists k (-(j*k=i))))))))).
all a ( (all b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (-(e*f=d))))))) -> (exists g ((all h ((exists i (-(g*i=h))))))) ). max_proofs 2
all a ( (all b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (-(d*f=e))))))) -> (exists g ((all h ((exists i (-(h*i=g))))))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
431. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (c*a=b)))) & (exists d ((all e f (-(e*f=d))))))). max_proofs 3
432. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (f*e=d)))) & (exists g h (g*h=g)))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
433. all a (((all b ((exists c (c*a=b)))) & (all d ((exists e (e*d=d))))) <-> ((all f ((exists g (g*a=f)))) & (exists h ((all i ((exists j (j*i=h)))) & (all k ((exists l m (l*m=k)))))))).
all a ( (all b ((exists c (c*a=b)))) & (all d ((exists e (e*d=d)))) -> (exists f ((all g ((exists h (h*g=f)))) & (all i ((exists j k (j*k=i)))))) ). sos
all a ( (all b ((exists c (c*a=b)))) & (exists d ((all e ((exists f (f*e=d)))) & (all g ((exists h i (h*i=g)))))) -> (all j ((exists k (k*j=j)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(261) [N,a] s.t. -((exists b (a*b=a)) & (exists c d ((all e (e*c=d))))) " abraham element 40 "
Top Ten Sorted Concepts: [110,142,138,99,116,79,93,96,185,60]
Top Ten Sorted Conjectures: [197,371,323,418,114,134,152,307,125,411]
434. all a ((-((all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e)))))))) <-> (-((all g ((exists h (h*a=g)))) & (all i ((exists j (j*i=i))))))).
all a ( -((all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e))))))) -> -((all g ((exists h (h*a=g)))) & (all i ((exists j (j*i=i))))) ). sos
all a ( -((all b ((exists c (c*a=b)))) & (all d ((exists e (e*d=d))))) -> -((all f ((exists g (g*f=a)))) & (exists h ((all i ((exists j (j*h=i))))))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
435. ((all a b ((exists c (c*a=b))))) <-> ((all d ((all e ((exists f (f*d=e)))) & (all g ((exists h (h*g=g))))))).
(all a b ((exists c (c*a=b)))) -> (all d ((all e ((exists f (f*d=e)))) & (all g ((exists h (h*g=g)))))). max_proofs 0
(all a ((all b ((exists c (c*a=b)))) & (all d ((exists e (e*d=d)))))) -> (all f g ((exists h (h*f=g)))). max_proofs 0
436. ((all a ((exists b (b*a=a)))) & (exists c ((all d ((exists e (e*c=d))))))) <-> ((exists f ((all g ((exists h (h*f=g)))) & (all i ((exists j (j*i=i))))))).
(all a ((exists b (b*a=a)))) & (exists c ((all d ((exists e (e*c=d)))))) -> (exists f ((all g ((exists h (h*f=g)))) & (all i ((exists j (j*i=i)))))). max_proofs 0
(exists a ((all b ((exists c (c*a=b)))) & (all d ((exists e (e*d=d)))))) -> (all f ((exists g (g*f=f)))). max_proofs 0
(exists a ((all b ((exists c (c*a=b)))) & (all d ((exists e (e*d=d)))))) -> (exists f ((all g ((exists h (h*f=g)))))). max_proofs 0
437. all a (((all b ((exists c (c*a=b)))) & (all d ((exists e (e*d=d))))) <-> ((all f ((exists g (g*a=f)))) & (all h ((exists i (i*h=h)))) & (exists j ((all k ((exists l (l*k=j)))))))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(262) [N] s.t. (all a ((exists b c (b*c=a)))) & (exists d (-((exists e f (e*f=d)) & (all g h ((exists i (i*g=h))))))) " akhiezer non_assoc 11 "
438. ((all a ((exists b (a*b=a))))) <-> ((all c ((exists d e (d*e=c)))) & (all f ((exists g (g*f=g))))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
439. ((all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e))))) <-> ((all g ((exists h i (h*i=g)))) & (all j ((exists k ((all l (j*l=k))))))).
(all a b ((exists c (c*a=b)))) & (exists d e ((all f (d*f=e)))) -> (all g ((exists h i (h*i=g)))).
---------------------------------------------
(all a b ((exists c (c*a=b)))) -> (all d ((exists e f (e*f=d)))).
(all a ((exists b c (b*c=a)))) & (all d ((exists e ((all f (d*f=e)))))) -> (all g h ((exists i (i*g=h)))). max_proofs 3
(all a ((exists b c (b*c=a)))) & (all d ((exists e ((all f (d*f=e)))))) -> (exists g h ((all i (g*i=h)))).
---------------------------------------------
(all a ((exists b ((all c (a*c=b)))))) -> (exists d e ((all f (d*f=e)))).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
Summary for session in non_assoc theory:
---------------------
Number of concepts: 262
Number of Conjectures: 439
Number of Models: 17
Largest Model Size: 4
Number of Categorisations: 184
Number of Theorems: 302
Number of Open Conjectures: 74
Number of Prime Implicants: 246
Average Proof Length: 2.8543046357615895
Average Surprisingness: 2.76158940397351
Average P.I. Proof Length: 0.7073170731707317
Number of Otter Proofs: 246
Number of HR Proofs: 116
----------------------
(263) [N] s.t. (all a ((exists b c (b*c=a)))) & (exists d ((all e ((exists f (-(f*e=d))))))) " akhiezer non_assoc 12 "
(264) [N] s.t. (all a ((exists b c (b*c=a)))) & (exists d ((all e ((exists f (e*f=d)))))) " akhiezer non_assoc 13 "
440. ((all a ((exists b (b*a=a))))) <-> ((all c ((exists d e (d*e=c)))) & -((all f ((exists g h (g*h=f)))) & (exists i j (i*j=i)))).
(all a ((exists b c (b*c=a)))) & -((all d ((exists e f (e*f=d)))) & (exists g h (g*h=g))) -> (all i ((exists j (j*i=i)))). sos
(all a ((exists b (b*a=a)))) -> -((all c ((exists d e (d*e=c)))) & (exists f g (f*g=f))). max_proofs 3
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(265) [N] s.t. (all a ((exists b c (b*c=a)))) & (exists d ((all e ((exists f (-(d*f=e))))))) " akhiezer non_assoc 14 "
441. ((exists a ((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d))))))) <-> ((all g ((exists h i (h*i=g)))) & (exists j ((all k ((exists l (l*k=j))))))).
(all a ((exists b c (b*c=a)))) & (exists d ((all e ((exists f (f*e=d)))))) -> (exists g ((all h ((exists i (i*h=g)))) & (all j ((exists k l (k*l=j)))))). max_proofs 0
(exists a ((all b ((exists c (c*b=a)))) & (all d ((exists e f (e*f=d)))))) -> (all g ((exists h i (h*i=g)))). max_proofs 0
(266) [N] s.t. (all a ((exists b c (b*c=a)))) & (all d e ((exists f (-(d*f=e))))) " akhiezer non_assoc 15 "
Top Ten Sorted Concepts: [110,142,138,99,116,79,93,96,185,60]
Top Ten Sorted Conjectures: [197,371,323,418,114,134,152,307,125,411]
442. (-((all a ((exists b (b*a=a)))) & (exists c ((all d ((exists e (e*c=d)))))))) <-> ((all f (-((all g ((exists h (h*g=f)))) & (exists i ((all j ((exists k (k*i=j)))))))))).
-((all a ((exists b (b*a=a)))) & (exists c ((all d ((exists e (e*c=d))))))) -> (all f (-((all g ((exists h (h*g=f)))) & (exists i ((all j ((exists k (k*i=j))))))))). sos
(all a (-((all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e))))))))) -> -((all g ((exists h (h*g=g)))) & (exists i ((all j ((exists k (k*i=j))))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
443. ((exists a (-((exists b c (b*c=a)) & (all d e ((exists f (f*d=e)))))))) <-> ((exists g (-((all h ((exists i (i*h=g)))) & (exists j ((all k ((exists l (l*j=k)))))))))).
(exists a (-((exists b c (b*c=a)) & (all d e ((exists f (f*d=e))))))) -> (exists g (-((all h ((exists i (i*h=g)))) & (exists j ((all k ((exists l (l*j=k))))))))). max_proofs 0
(exists a (-((all b ((exists c (c*b=a)))) & (exists d ((all e ((exists f (f*d=e))))))))) -> (exists g (-((exists h i (h*i=g)) & (all j k ((exists l (l*j=k))))))). max_proofs 0
(267) [N] s.t. (all a ((exists b c (b*c=a)))) & -((all d ((exists e f (e*f=d)))) & (exists g h ((all i (i*g=h))))) " akhiezer non_assoc 16 "
444. ((all ax1 ax2 (ax1 = ax2))) <-> ((all a ((exists b c (b*c=a)))) & (exists d ((all e f (-(e*f=d)))))). max_proofs 3
445. ((all a ((exists b c (b*c=a)))) & (exists d ((all e ((exists f (-(d*f=e)))))))) <-> ((all g ((exists h i (h*i=g)))) & (exists j ((all k ((exists l (-(k*l=j)))))))).
(all a ((exists b c (b*c=a)))) & (exists d ((all e ((exists f (-(e*f=d))))))) -> (exists g ((all h ((exists i (-(g*i=h))))))). max_proofs 3
(all a ((exists b c (b*c=a)))) & (exists d ((all e ((exists f (-(d*f=e))))))) -> (exists g ((all h ((exists i (-(h*i=g))))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(268) [N] s.t. (all a ((exists b c (b*c=a)))) & -((all d ((exists e f (e*f=d)))) & (exists g h (g*h=h))) " akhiezer non_assoc 17 "
446. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (a*c=b)))) & (all d ((exists e (e*d=d)))))). max_proofs 6
447. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (a*c=b)))) & (all d ((exists e ((all f (d*f=e)))))))). max_proofs 6
448. all a (((all b ((exists c (a*c=b)))) & (all d ((exists e (d*e=d))))) <-> ((all f ((exists g (a*g=f)))) & (all h ((exists i (i*h=i)))))).
all a ( (all b ((exists c (a*c=b)))) & (all d ((exists e (d*e=d)))) -> (all f ((exists g (g*f=g)))) ). sos
all a ( (all b ((exists c (a*c=b)))) & (all d ((exists e (e*d=e)))) -> (all f ((exists g (f*g=f)))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(269) [N,a] s.t. (all b ((exists c (a*c=b)))) & (exists d ((all e ((exists f (-(f*e=d))))))) " abraham element 41 "
(270) [N,a] s.t. (all b ((exists c (a*c=b)))) & (exists d ((all e ((exists f (e*f=d)))))) " abraham element 42 "
449. all a (((all b ((exists c (a*c=b))))) <-> ((all d ((exists e (a*e=d)))) & (exists f ((all g ((exists h (-(f*h=g))))))))).
all a ( (all b ((exists c (a*c=b)))) -> (exists d ((all e ((exists f (-(d*f=e))))))) ).
---------------------------------------------
all a ( (all b ((exists c (a*c=b)))) -> (exists d (a*d=a)) ).
all a ( (exists b (a*b=a)) -> (exists c ((all d ((exists e (-(c*e=d))))))) ).
(271) [N,a] s.t. (all b ((exists c (a*c=b)))) & (exists d ((all e ((exists f (f*e=d)))))) " abraham element 43 "
Top Ten Sorted Concepts: [110,142,138,99,116,79,93,96,265,185]
Top Ten Sorted Conjectures: [197,371,323,418,114,134,152,307,125,411]
450. all a (((all b ((exists c (a*c=b)))) & (exists d ((all e ((exists f (e*f=d))))))) <-> ((all g ((exists h (a*h=g)))) & (all i j ((exists k (-(i*k=j))))))).
all a ( (all b ((exists c (a*c=b)))) & (all d e ((exists f (-(d*f=e))))) -> (exists g ((all h ((exists i (h*i=g)))))) ). sos
all a ( (all b ((exists c (a*c=b)))) & (exists d ((all e ((exists f (e*f=d)))))) -> (all g h ((exists i (-(g*i=h))))) ).
---------------------------------------------
all a ( (exists b ((all c ((exists d (c*d=b)))))) -> (all e f ((exists g (-(e*g=f))))) ).
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
451. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (a*c=b)))) & (exists d ((all e f (-(e*f=d))))))). max_proofs 3
452. all a (((all b ((exists c (a*c=b))))) <-> ((all d ((exists e (a*e=d)))) & (exists f ((all g ((exists h (-(g*h=f))))))))).
all a ( (all b ((exists c (a*c=b)))) -> (exists d ((all e ((exists f (-(e*f=d))))))) ).
---------------------------------------------
all a ( (all b ((exists c (a*c=b)))) -> (exists d (a*d=a)) ).
all a ( (exists b (a*b=a)) -> (exists c ((all d ((exists e (-(d*e=c))))))) ).
453. all a (((all ax1 ax2 (ax1 = ax2))) <-> ((all b ((exists c (a*c=b)))) & (exists d ((all e ((exists f (f*d=e)))))))). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
(272) [N,a] s.t. -((all b ((exists c (a*c=b)))) & (all d ((exists e (d*e=d))))) " abraham element 44 "
454. ((all a b ((exists c (a*c=b))))) <-> ((all d ((all e ((exists f (d*f=e)))) & (all g ((exists h (g*h=g))))))).
(all a b ((exists c (a*c=b)))) -> (all d ((all e ((exists f (d*f=e)))) & (all g ((exists h (g*h=g)))))). max_proofs 0
(all a ((all b ((exists c (a*c=b)))) & (all d ((exists e (d*e=d)))))) -> (all f g ((exists h (f*h=g)))). max_proofs 0
455. ((all a ((exists b (a*b=a)))) & (exists c ((all d ((exists e (c*e=d))))))) <-> ((exists f ((all g ((exists h (f*h=g)))) & (all i ((exists j (i*j=i))))))).
(all a ((exists b (a*b=a)))) & (exists c ((all d ((exists e (c*e=d)))))) -> (exists f ((all g ((exists h (f*h=g)))) & (all i ((exists j (i*j=i)))))). max_proofs 0
(exists a ((all b ((exists c (a*c=b)))) & (all d ((exists e (d*e=d)))))) -> (all f ((exists g (f*g=f)))). max_proofs 0
(exists a ((all b ((exists c (a*c=b)))) & (all d ((exists e (d*e=d)))))) -> (exists f ((all g ((exists h (f*h=g)))))). max_proofs 0
456. all a (((all b ((exists c (a*c=b)))) & (all d ((exists e (d*e=d))))) <-> ((all f ((exists g (a*g=f)))) & (all h ((exists i (h*i=h)))) & (exists j ((all k ((exists l (k*l=j)))))))).
all a ( (all b ((exists c (a*c=b)))) & (all d ((exists e (d*e=d)))) -> (exists f ((all g ((exists h (g*h=f)))))) ). sos
Mace generating counterexample of order: 1 2 3 4 5 6 7 8
457. ((exists a b ((all c (c*a=b)))) & (all d ((exists e (d*e=d))))) <-> ((all f ((exists g (f*g=f)) & (exists h i ((all j (j*h=i))))))).
(exists a b ((all c (c*a=b)))) & (all d ((exists e (d*e=d)))) -> (all f ((exists g (f*g=f)) & (exists h i ((all j (j*h=i)))))). max_proofs 0
(all a ((exists b (a*b=a)) & (exists c d ((all e (e*c=d)))))) -> (exists f g ((all h (h*f=g)))). max_proofs 0
(all a ((exists b (a*b=a)) & (exists c d ((all e (e*c=d)))))) -> (all f ((exists g (f*g=f)))). max_proofs 0
458. ((exists a b ((all c (c*a=b))))) <-> ((exists d ((exists e (d*e=d)) & (exists f g ((all h (h*f=g))))))).
(exists a b ((all c (c*a=b)))) -> (exists d ((exists e (d*e=d)) & (exists f g ((all h (h*f=g)))))). max_proofs 0
(exists a ((exists b (a*b=a)) & (exists c d ((all e (e*c=d)))))) -> (exists f g ((all h (h*f=g)))). max_proofs 0
yes