WATCH: 0.00 CPU 0.01 WC WATCH: 5.11 CPU 3.02 WC WATCH: 10.70 CPU 6.03 WC WATCH: 16.23 CPU 9.04 WC # Garbage collection reclaimed 113 unused term cells. # Garbage collection reclaimed 74 unused term cells. # Garbage collection reclaimed 73 unused term cells. # Garbage collection reclaimed 47 unused term cells. # Auto-Ordering is analysing problem. # Problem is type HUSMGFFMF21MD # Auto-mode selected ordering type KBO6 # Auto-mode selected ordering precedence scheme # Auto-mode selected weight ordering scheme # # Auto-Heuristic is analysing problem. # Problem is type HUSMGFFMF21MD # Auto-Mode selected heuristic G_E___100_C18_F1_PI_AE_Q4_CS_SP_PS_S0Y # and selection function SelectMaxLComplexAvoidPosPred. # # Initializing proof state # Scanning for AC axioms # multiplication is associative # addition is AC # AC handling enabled # Presaturation interreduction done # Proof found! # SZS status Theorem # Parsed axioms : 27 # Removed by relevancy pruning : 0 # Initial clauses : 29 # Removed in clause preprocessing : 8 # Initial clauses in saturation : 21 # Processed clauses : 10901 # ...of these trivial : 5959 # ...subsumed : 3437 # ...remaining for further processing : 1505 # Other redundant clauses eliminated : 0 # Clauses deleted for lack of memory : 0 # Backward-subsumed : 0 # Backward-rewritten : 283 # Generated clauses : 709233 # ...of the previous two non-trivial : 282965 # Contextual simplify-reflections : 0 # Paramodulations : 709233 # Factorizations : 0 # Equation resolutions : 0 # Current number of processed clauses : 1201 # Positive orientable unit clauses : 1182 # Positive unorientable unit clauses: 16 # Negative unit clauses : 1 # Non-unit-clauses : 2 # Current number of unprocessed clauses: 237018 # ...number of literals in the above : 237018 # Clause-clause subsumption calls (NU) : 0 # Rec. Clause-clause subsumption calls : 0 # Unit Clause-clause subsumption calls : 120 # Rewrite failures with RHS unbound : 0 # Indexed BW rewrite attempts : 16755 # Indexed BW rewrite successes : 384 # Backwards rewriting index : 630 leaves, 4.29+/-6.597 terms/leaf # Paramod-from index : 355 leaves, 3.41+/-4.945 terms/leaf # Paramod-into index : 612 leaves, 4.17+/-6.325 terms/leaf # SZS output start CNFRefutation. fof(1, axiom,![X1]:![X2]:![X3]:multiplication(X1,multiplication(X2,X3))=multiplication(multiplication(X1,X2),X3),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+0.ax', multiplicative_associativity)). fof(2, axiom,![X1]:X1=addition(X1,zero),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+0.ax', additive_identity)). fof(3, axiom,![X3]:![X2]:![X1]:addition(X1,addition(X2,X3))=addition(addition(X1,X2),X3),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+0.ax', additive_associativity)). fof(4, axiom,![X1]:addition(X1,X1)=X1,file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+0.ax', additive_idempotence)). fof(5, axiom,![X1]:multiplication(zero,X1)=zero,file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+0.ax', left_annihilation)). fof(6, axiom,![X1]:multiplication(X1,zero)=zero,file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+0.ax', right_annihilation)). fof(7, axiom,![X1]:![X2]:![X3]:multiplication(addition(X1,X2),X3)=addition(multiplication(X1,X3),multiplication(X2,X3)),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+0.ax', left_distributivity)). fof(8, axiom,![X1]:X1=multiplication(one,X1),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+0.ax', multiplicative_left_identity)). fof(9, axiom,![X1]:![X2]:![X3]:addition(multiplication(X1,X2),multiplication(X1,X3))=multiplication(X1,addition(X2,X3)),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+0.ax', right_distributivity)). fof(11, axiom,![X1]:X1=multiplication(X1,one),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+0.ax', multiplicative_right_identity)). fof(12, axiom,![X1]:![X2]:addition(X1,X2)=addition(X2,X1),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+0.ax', additive_commutativity)). fof(13, axiom,![X4]:one=addition(antidomain(antidomain(X4)),antidomain(X4)),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+4.ax', domain3)). fof(14, axiom,![X4]:codomain(X4)=coantidomain(coantidomain(X4)),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+4.ax', codomain4)). fof(15, axiom,![X4]:one=addition(coantidomain(coantidomain(X4)),coantidomain(X4)),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+4.ax', codomain3)). fof(16, axiom,![X4]:domain(X4)=antidomain(antidomain(X4)),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+4.ax', domain4)). fof(17, axiom,![X4]:![X5]:addition(coantidomain(multiplication(X4,X5)),coantidomain(multiplication(coantidomain(coantidomain(X4)),X5)))=coantidomain(multiplication(coantidomain(coantidomain(X4)),X5)),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+4.ax', codomain2)). fof(18, axiom,![X4]:![X5]:antidomain(multiplication(X4,antidomain(antidomain(X5))))=addition(antidomain(multiplication(X4,X5)),antidomain(multiplication(X4,antidomain(antidomain(X5))))),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+4.ax', domain2)). fof(19, axiom,![X4]:multiplication(antidomain(X4),X4)=zero,file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+4.ax', domain1)). fof(20, axiom,![X4]:multiplication(X4,coantidomain(X4))=zero,file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+4.ax', codomain1)). fof(21, axiom,![X4]:![X5]:backward_diamond(X4,X5)=codomain(multiplication(codomain(X5),X4)),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+6.ax', backward_diamond)). fof(22, axiom,![X4]:antidomain(domain(X4))=c(X4),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+6.ax', complement)). fof(23, axiom,![X4]:![X5]:forward_diamond(X4,X5)=domain(multiplication(X4,domain(X5))),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+6.ax', forward_diamond)). fof(25, axiom,![X4]:![X5]:backward_box(X4,X5)=c(backward_diamond(X4,c(X5))),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+6.ax', backward_box)). fof(26, axiom,![X4]:![X5]:c(forward_diamond(X4,c(X5)))=forward_box(X4,X5),file('/CW/home-0/sutcliff/TPTP/Axioms/KLE001+6.ax', forward_box)). fof(27, conjecture,![X4]:![X5]:![X6]:(addition(domain(X5),backward_box(X4,domain(X6)))=one=>addition(forward_box(X4,domain(X5)),domain(X6))=one),file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p', goals)). fof(28, negated_conjecture,~(![X4]:![X5]:![X6]:(addition(domain(X5),backward_box(X4,domain(X6)))=one=>addition(forward_box(X4,domain(X5)),domain(X6))=one)),inference(assume_negation,[status(cth)],[27])). fof(29, plain,![X4]:![X5]:![X6]:multiplication(X4,multiplication(X5,X6))=multiplication(multiplication(X4,X5),X6),inference(variable_rename,[status(thm)],[1])). cnf(30,plain,(multiplication(X1,multiplication(X2,X3))=multiplication(multiplication(X1,X2),X3)),inference(split_conjunct,[status(thm)],[29])). fof(31, plain,![X2]:X2=addition(X2,zero),inference(variable_rename,[status(thm)],[2])). cnf(32,plain,(X1=addition(X1,zero)),inference(split_conjunct,[status(thm)],[31])). fof(33, plain,![X4]:![X5]:![X6]:addition(X6,addition(X5,X4))=addition(addition(X6,X5),X4),inference(variable_rename,[status(thm)],[3])). cnf(34,plain,(addition(X1,addition(X2,X3))=addition(addition(X1,X2),X3)),inference(split_conjunct,[status(thm)],[33])). fof(35, plain,![X2]:addition(X2,X2)=X2,inference(variable_rename,[status(thm)],[4])). cnf(36,plain,(addition(X1,X1)=X1),inference(split_conjunct,[status(thm)],[35])). fof(37, plain,![X2]:multiplication(zero,X2)=zero,inference(variable_rename,[status(thm)],[5])). cnf(38,plain,(multiplication(zero,X1)=zero),inference(split_conjunct,[status(thm)],[37])). fof(39, plain,![X2]:multiplication(X2,zero)=zero,inference(variable_rename,[status(thm)],[6])). cnf(40,plain,(multiplication(X1,zero)=zero),inference(split_conjunct,[status(thm)],[39])). fof(41, plain,![X4]:![X5]:![X6]:multiplication(addition(X4,X5),X6)=addition(multiplication(X4,X6),multiplication(X5,X6)),inference(variable_rename,[status(thm)],[7])). cnf(42,plain,(multiplication(addition(X1,X2),X3)=addition(multiplication(X1,X3),multiplication(X2,X3))),inference(split_conjunct,[status(thm)],[41])). fof(43, plain,![X2]:X2=multiplication(one,X2),inference(variable_rename,[status(thm)],[8])). cnf(44,plain,(X1=multiplication(one,X1)),inference(split_conjunct,[status(thm)],[43])). fof(45, plain,![X4]:![X5]:![X6]:addition(multiplication(X4,X5),multiplication(X4,X6))=multiplication(X4,addition(X5,X6)),inference(variable_rename,[status(thm)],[9])). cnf(46,plain,(addition(multiplication(X1,X2),multiplication(X1,X3))=multiplication(X1,addition(X2,X3))),inference(split_conjunct,[status(thm)],[45])). fof(51, plain,![X2]:X2=multiplication(X2,one),inference(variable_rename,[status(thm)],[11])). cnf(52,plain,(X1=multiplication(X1,one)),inference(split_conjunct,[status(thm)],[51])). fof(53, plain,![X3]:![X4]:addition(X3,X4)=addition(X4,X3),inference(variable_rename,[status(thm)],[12])). cnf(54,plain,(addition(X1,X2)=addition(X2,X1)),inference(split_conjunct,[status(thm)],[53])). fof(55, plain,![X5]:one=addition(antidomain(antidomain(X5)),antidomain(X5)),inference(variable_rename,[status(thm)],[13])). cnf(56,plain,(one=addition(antidomain(antidomain(X1)),antidomain(X1))),inference(split_conjunct,[status(thm)],[55])). fof(57, plain,![X5]:codomain(X5)=coantidomain(coantidomain(X5)),inference(variable_rename,[status(thm)],[14])). cnf(58,plain,(codomain(X1)=coantidomain(coantidomain(X1))),inference(split_conjunct,[status(thm)],[57])). fof(59, plain,![X5]:one=addition(coantidomain(coantidomain(X5)),coantidomain(X5)),inference(variable_rename,[status(thm)],[15])). cnf(60,plain,(one=addition(coantidomain(coantidomain(X1)),coantidomain(X1))),inference(split_conjunct,[status(thm)],[59])). fof(61, plain,![X5]:domain(X5)=antidomain(antidomain(X5)),inference(variable_rename,[status(thm)],[16])). cnf(62,plain,(domain(X1)=antidomain(antidomain(X1))),inference(split_conjunct,[status(thm)],[61])). fof(63, plain,![X6]:![X7]:addition(coantidomain(multiplication(X6,X7)),coantidomain(multiplication(coantidomain(coantidomain(X6)),X7)))=coantidomain(multiplication(coantidomain(coantidomain(X6)),X7)),inference(variable_rename,[status(thm)],[17])). cnf(64,plain,(addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)))=coantidomain(multiplication(coantidomain(coantidomain(X1)),X2))),inference(split_conjunct,[status(thm)],[63])). fof(65, plain,![X6]:![X7]:antidomain(multiplication(X6,antidomain(antidomain(X7))))=addition(antidomain(multiplication(X6,X7)),antidomain(multiplication(X6,antidomain(antidomain(X7))))),inference(variable_rename,[status(thm)],[18])). cnf(66,plain,(antidomain(multiplication(X1,antidomain(antidomain(X2))))=addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,antidomain(antidomain(X2)))))),inference(split_conjunct,[status(thm)],[65])). fof(67, plain,![X5]:multiplication(antidomain(X5),X5)=zero,inference(variable_rename,[status(thm)],[19])). cnf(68,plain,(multiplication(antidomain(X1),X1)=zero),inference(split_conjunct,[status(thm)],[67])). fof(69, plain,![X5]:multiplication(X5,coantidomain(X5))=zero,inference(variable_rename,[status(thm)],[20])). cnf(70,plain,(multiplication(X1,coantidomain(X1))=zero),inference(split_conjunct,[status(thm)],[69])). fof(71, plain,![X6]:![X7]:backward_diamond(X6,X7)=codomain(multiplication(codomain(X7),X6)),inference(variable_rename,[status(thm)],[21])). cnf(72,plain,(backward_diamond(X1,X2)=codomain(multiplication(codomain(X2),X1))),inference(split_conjunct,[status(thm)],[71])). fof(73, plain,![X5]:antidomain(domain(X5))=c(X5),inference(variable_rename,[status(thm)],[22])). cnf(74,plain,(antidomain(domain(X1))=c(X1)),inference(split_conjunct,[status(thm)],[73])). fof(75, plain,![X6]:![X7]:forward_diamond(X6,X7)=domain(multiplication(X6,domain(X7))),inference(variable_rename,[status(thm)],[23])). cnf(76,plain,(forward_diamond(X1,X2)=domain(multiplication(X1,domain(X2)))),inference(split_conjunct,[status(thm)],[75])). fof(79, plain,![X6]:![X7]:backward_box(X6,X7)=c(backward_diamond(X6,c(X7))),inference(variable_rename,[status(thm)],[25])). cnf(80,plain,(backward_box(X1,X2)=c(backward_diamond(X1,c(X2)))),inference(split_conjunct,[status(thm)],[79])). fof(81, plain,![X6]:![X7]:c(forward_diamond(X6,c(X7)))=forward_box(X6,X7),inference(variable_rename,[status(thm)],[26])). cnf(82,plain,(c(forward_diamond(X1,c(X2)))=forward_box(X1,X2)),inference(split_conjunct,[status(thm)],[81])). fof(83, negated_conjecture,?[X4]:?[X5]:?[X6]:(addition(domain(X5),backward_box(X4,domain(X6)))=one&~(addition(forward_box(X4,domain(X5)),domain(X6))=one)),inference(fof_nnf,[status(thm)],[28])). fof(84, negated_conjecture,?[X7]:?[X8]:?[X9]:(addition(domain(X8),backward_box(X7,domain(X9)))=one&~(addition(forward_box(X7,domain(X8)),domain(X9))=one)),inference(variable_rename,[status(thm)],[83])). fof(85, negated_conjecture,(addition(domain(esk2_0),backward_box(esk1_0,domain(esk3_0)))=one&~(addition(forward_box(esk1_0,domain(esk2_0)),domain(esk3_0))=one)),inference(skolemize,[status(esa)],[84])). cnf(86,negated_conjecture,(addition(forward_box(esk1_0,domain(esk2_0)),domain(esk3_0))!=one),inference(split_conjunct,[status(thm)],[85])). cnf(87,negated_conjecture,(addition(domain(esk2_0),backward_box(esk1_0,domain(esk3_0)))=one),inference(split_conjunct,[status(thm)],[85])). cnf(88,plain,(antidomain(antidomain(antidomain(X1)))=c(X1)),inference(rw,[status(thm)],[74,62,theory(equality)]),['unfolding']). cnf(89,plain,(antidomain(antidomain(multiplication(X1,antidomain(antidomain(X2)))))=forward_diamond(X1,X2)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[76,62,theory(equality)]),62,theory(equality)]),['unfolding']). cnf(91,negated_conjecture,(addition(antidomain(antidomain(esk2_0)),backward_box(esk1_0,antidomain(antidomain(esk3_0))))=one),inference(rw,[status(thm)],[inference(rw,[status(thm)],[87,62,theory(equality)]),62,theory(equality)]),['unfolding']). cnf(92,negated_conjecture,(addition(forward_box(esk1_0,antidomain(antidomain(esk2_0))),antidomain(antidomain(esk3_0)))!=one),inference(rw,[status(thm)],[inference(rw,[status(thm)],[86,62,theory(equality)]),62,theory(equality)]),['unfolding']). cnf(93,plain,(antidomain(antidomain(antidomain(backward_diamond(X1,antidomain(antidomain(antidomain(X2)))))))=backward_box(X1,X2)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[80,88,theory(equality)]),88,theory(equality)]),['unfolding']). cnf(94,plain,(antidomain(antidomain(antidomain(forward_diamond(X1,antidomain(antidomain(antidomain(X2)))))))=forward_box(X1,X2)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[82,88,theory(equality)]),88,theory(equality)]),['unfolding']). cnf(95,plain,(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(X2)),X1)))=backward_diamond(X1,X2)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[72,58,theory(equality)]),58,theory(equality)]),['unfolding']). cnf(96,plain,(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(X1,antidomain(antidomain(antidomain(antidomain(antidomain(X2)))))))))))=forward_box(X1,X2)),inference(rw,[status(thm)],[94,89,theory(equality)]),['unfolding']). cnf(97,negated_conjecture,(addition(antidomain(antidomain(esk2_0)),antidomain(antidomain(antidomain(backward_diamond(esk1_0,antidomain(antidomain(antidomain(antidomain(antidomain(esk3_0))))))))))=one),inference(rw,[status(thm)],[91,93,theory(equality)]),['unfolding']). cnf(98,negated_conjecture,(addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(esk1_0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(esk2_0))))))))))))),antidomain(antidomain(esk3_0)))!=one),inference(rw,[status(thm)],[92,96,theory(equality)]),['unfolding']). cnf(99,negated_conjecture,(addition(antidomain(antidomain(esk2_0)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(esk3_0))))))),esk1_0)))))))=one),inference(rw,[status(thm)],[97,95,theory(equality)]),['unfolding']). cnf(100,plain,(addition(antidomain(X1),antidomain(antidomain(X1)))=one),inference(rw,[status(thm)],[56,54,theory(equality)])). cnf(101,plain,(addition(coantidomain(X1),coantidomain(coantidomain(X1)))=one),inference(rw,[status(thm)],[60,54,theory(equality)])). cnf(102,negated_conjecture,(addition(antidomain(antidomain(esk3_0)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(esk1_0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(esk2_0))))))))))))))!=one),inference(rw,[status(thm)],[98,54,theory(equality)])). cnf(103,plain,(zero=coantidomain(one)),inference(spm,[status(thm)],[44,70,theory(equality)])). cnf(104,plain,(zero=antidomain(one)),inference(spm,[status(thm)],[52,68,theory(equality)])). cnf(105,plain,(addition(zero,X1)=X1),inference(spm,[status(thm)],[32,54,theory(equality)])). cnf(116,plain,(multiplication(zero,X2)=multiplication(antidomain(X1),multiplication(X1,X2))),inference(spm,[status(thm)],[30,68,theory(equality)])). cnf(119,plain,(multiplication(zero,X2)=multiplication(X1,multiplication(coantidomain(X1),X2))),inference(spm,[status(thm)],[30,70,theory(equality)])). cnf(126,plain,(zero=multiplication(antidomain(X1),multiplication(X1,X2))),inference(rw,[status(thm)],[116,38,theory(equality)])). cnf(130,plain,(zero=multiplication(X1,multiplication(coantidomain(X1),X2))),inference(rw,[status(thm)],[119,38,theory(equality)])). cnf(139,plain,(addition(one,X2)=addition(antidomain(X1),addition(antidomain(antidomain(X1)),X2))),inference(spm,[status(thm)],[34,100,theory(equality)])). cnf(141,plain,(addition(X1,X2)=addition(X1,addition(X1,X2))),inference(spm,[status(thm)],[34,36,theory(equality)])). cnf(153,plain,(addition(multiplication(antidomain(X1),X2),zero)=multiplication(antidomain(X1),addition(X2,X1))),inference(spm,[status(thm)],[46,68,theory(equality)])). cnf(157,plain,(addition(multiplication(X1,X2),zero)=multiplication(X1,addition(X2,coantidomain(X1)))),inference(spm,[status(thm)],[46,70,theory(equality)])). cnf(158,plain,(addition(multiplication(X1,X2),X1)=multiplication(X1,addition(X2,one))),inference(spm,[status(thm)],[46,52,theory(equality)])). cnf(170,plain,(multiplication(antidomain(X1),X2)=multiplication(antidomain(X1),addition(X2,X1))),inference(rw,[status(thm)],[153,32,theory(equality)])). cnf(177,plain,(multiplication(X1,X2)=multiplication(X1,addition(X2,coantidomain(X1)))),inference(rw,[status(thm)],[157,32,theory(equality)])). cnf(191,plain,(addition(multiplication(X1,X2),zero)=multiplication(addition(X1,antidomain(X2)),X2)),inference(spm,[status(thm)],[42,68,theory(equality)])). cnf(192,plain,(addition(multiplication(X1,X2),X2)=multiplication(addition(X1,one),X2)),inference(spm,[status(thm)],[42,44,theory(equality)])). cnf(195,plain,(addition(multiplication(X1,coantidomain(X2)),zero)=multiplication(addition(X1,X2),coantidomain(X2))),inference(spm,[status(thm)],[42,70,theory(equality)])). cnf(210,plain,(multiplication(X1,X2)=multiplication(addition(X1,antidomain(X2)),X2)),inference(rw,[status(thm)],[191,32,theory(equality)])). cnf(213,plain,(multiplication(X1,coantidomain(X2))=multiplication(addition(X1,X2),coantidomain(X2))),inference(rw,[status(thm)],[195,32,theory(equality)])). cnf(263,plain,(addition(zero,coantidomain(zero))=one),inference(spm,[status(thm)],[101,103,theory(equality)])). cnf(268,plain,(addition(zero,antidomain(zero))=one),inference(spm,[status(thm)],[100,104,theory(equality)])). cnf(283,plain,(addition(coantidomain(X1),one)=one),inference(spm,[status(thm)],[141,101,theory(equality)])). cnf(286,plain,(addition(antidomain(X1),one)=one),inference(spm,[status(thm)],[141,100,theory(equality)])). cnf(293,plain,(addition(X1,addition(X2,X1))=addition(X2,X1)),inference(spm,[status(thm)],[141,54,theory(equality)])). cnf(308,plain,(addition(one,coantidomain(X1))=one),inference(rw,[status(thm)],[283,54,theory(equality)])). cnf(314,plain,(addition(one,antidomain(X1))=one),inference(rw,[status(thm)],[286,54,theory(equality)])). cnf(360,plain,(coantidomain(zero)=one),inference(rw,[status(thm)],[263,105,theory(equality)])). cnf(370,plain,(antidomain(zero)=one),inference(rw,[status(thm)],[268,105,theory(equality)])). cnf(421,plain,(addition(antidomain(zero),antidomain(multiplication(X1,antidomain(antidomain(multiplication(coantidomain(X1),X2))))))=antidomain(multiplication(X1,antidomain(antidomain(multiplication(coantidomain(X1),X2)))))),inference(spm,[status(thm)],[66,130,theory(equality)])). cnf(439,plain,(one=antidomain(multiplication(X1,antidomain(antidomain(multiplication(coantidomain(X1),X2)))))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[421,370,theory(equality)]),314,theory(equality)])). cnf(521,plain,(multiplication(X1,addition(coantidomain(X1),X2))=multiplication(X1,X2)),inference(spm,[status(thm)],[177,54,theory(equality)])). cnf(583,plain,(multiplication(addition(antidomain(X2),X1),X2)=multiplication(X1,X2)),inference(spm,[status(thm)],[210,54,theory(equality)])). cnf(687,plain,(multiplication(X1,one)=multiplication(X1,coantidomain(coantidomain(X1)))),inference(spm,[status(thm)],[521,101,theory(equality)])). cnf(706,plain,(X1=multiplication(X1,coantidomain(coantidomain(X1)))),inference(rw,[status(thm)],[687,52,theory(equality)])). cnf(711,plain,(multiplication(X1,X2)=multiplication(X1,multiplication(coantidomain(coantidomain(X1)),X2))),inference(spm,[status(thm)],[30,706,theory(equality)])). cnf(748,plain,(multiplication(one,X1)=multiplication(antidomain(antidomain(X1)),X1)),inference(spm,[status(thm)],[583,100,theory(equality)])). cnf(765,plain,(X1=multiplication(antidomain(antidomain(X1)),X1)),inference(rw,[status(thm)],[748,44,theory(equality)])). cnf(774,plain,(multiplication(antidomain(antidomain(antidomain(X1))),X1)=zero),inference(spm,[status(thm)],[126,765,theory(equality)])). cnf(791,plain,(addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(X1))))),X1)))=coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(X1))))),X1))),inference(spm,[status(thm)],[64,774,theory(equality)])). cnf(806,plain,(one=coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(X1))))),X1))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[791,360,theory(equality)]),308,theory(equality)])). cnf(1160,plain,(addition(X1,multiplication(X1,X2))=multiplication(X1,addition(X2,one))),inference(rw,[status(thm)],[158,54,theory(equality)])). cnf(1609,plain,(multiplication(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(X1))))),X1),one)=zero),inference(spm,[status(thm)],[70,806,theory(equality)])). cnf(1632,plain,(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(X1))))),X1)=zero),inference(rw,[status(thm)],[inference(rw,[status(thm)],[1609,30,theory(equality)]),52,theory(equality)])). cnf(2027,plain,(addition(X2,multiplication(X1,X2))=multiplication(addition(X1,one),X2)),inference(rw,[status(thm)],[192,54,theory(equality)])). cnf(2069,plain,(addition(addition(X1,coantidomain(X2)),multiplication(X2,X1))=multiplication(addition(X2,one),addition(X1,coantidomain(X2)))),inference(spm,[status(thm)],[2027,177,theory(equality)])). cnf(2116,plain,(addition(X1,addition(coantidomain(X2),multiplication(X2,X1)))=multiplication(addition(X2,one),addition(X1,coantidomain(X2)))),inference(rw,[status(thm)],[2069,34,theory(equality)])). cnf(2879,plain,(multiplication(antidomain(antidomain(antidomain(X1))),one)=multiplication(antidomain(antidomain(antidomain(X1))),antidomain(X1))),inference(spm,[status(thm)],[170,100,theory(equality)])). cnf(2893,plain,(multiplication(antidomain(addition(X1,X2)),addition(X1,X2))=multiplication(antidomain(addition(X1,X2)),X1)),inference(spm,[status(thm)],[170,141,theory(equality)])). cnf(2898,plain,(multiplication(antidomain(X1),addition(X1,X2))=multiplication(antidomain(X1),X2)),inference(spm,[status(thm)],[170,54,theory(equality)])). cnf(2930,plain,(antidomain(antidomain(antidomain(X1)))=multiplication(antidomain(antidomain(antidomain(X1))),antidomain(X1))),inference(rw,[status(thm)],[2879,52,theory(equality)])). cnf(2931,plain,(antidomain(antidomain(antidomain(X1)))=antidomain(X1)),inference(rw,[status(thm)],[2930,765,theory(equality)])). cnf(2938,plain,(zero=multiplication(antidomain(addition(X1,X2)),X1)),inference(rw,[status(thm)],[2893,68,theory(equality)])). cnf(2981,plain,(multiplication(coantidomain(coantidomain(antidomain(X1))),X1)=zero),inference(rw,[status(thm)],[1632,2931,theory(equality)])). cnf(2984,negated_conjecture,(addition(antidomain(antidomain(esk3_0)),antidomain(multiplication(esk1_0,antidomain(esk2_0))))!=one),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[102,2931,theory(equality)]),2931,theory(equality)]),2931,theory(equality)]),2931,theory(equality)]),2931,theory(equality)])). cnf(2985,negated_conjecture,(addition(antidomain(antidomain(esk2_0)),antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(esk3_0))),esk1_0)))))=one),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[99,2931,theory(equality)]),2931,theory(equality)]),2931,theory(equality)])). cnf(3010,plain,(addition(zero,multiplication(X3,X1))=multiplication(addition(antidomain(addition(X1,X2)),X3),X1)),inference(spm,[status(thm)],[42,2938,theory(equality)])). cnf(3059,plain,(multiplication(X3,X1)=multiplication(addition(antidomain(addition(X1,X2)),X3),X1)),inference(rw,[status(thm)],[3010,105,theory(equality)])). cnf(3179,plain,(addition(zero,multiplication(X2,X1))=multiplication(addition(coantidomain(coantidomain(antidomain(X1))),X2),X1)),inference(spm,[status(thm)],[42,2981,theory(equality)])). cnf(3206,plain,(multiplication(X2,X1)=multiplication(addition(coantidomain(coantidomain(antidomain(X1))),X2),X1)),inference(rw,[status(thm)],[3179,105,theory(equality)])). cnf(3311,negated_conjecture,(multiplication(one,antidomain(esk2_0))=multiplication(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(esk3_0))),esk1_0)))),antidomain(esk2_0))),inference(spm,[status(thm)],[583,2985,theory(equality)])). cnf(3322,negated_conjecture,(antidomain(esk2_0)=multiplication(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(esk3_0))),esk1_0)))),antidomain(esk2_0))),inference(rw,[status(thm)],[3311,44,theory(equality)])). cnf(3348,plain,(multiplication(one,coantidomain(coantidomain(coantidomain(X1))))=multiplication(coantidomain(X1),coantidomain(coantidomain(coantidomain(X1))))),inference(spm,[status(thm)],[213,101,theory(equality)])). cnf(3370,plain,(multiplication(addition(X2,X1),coantidomain(X2))=multiplication(X1,coantidomain(X2))),inference(spm,[status(thm)],[213,54,theory(equality)])). cnf(3401,plain,(coantidomain(coantidomain(coantidomain(X1)))=multiplication(coantidomain(X1),coantidomain(coantidomain(coantidomain(X1))))),inference(rw,[status(thm)],[3348,44,theory(equality)])). cnf(3402,plain,(coantidomain(coantidomain(coantidomain(X1)))=coantidomain(X1)),inference(rw,[status(thm)],[3401,706,theory(equality)])). cnf(3421,plain,(multiplication(coantidomain(coantidomain(X1)),coantidomain(X1))=zero),inference(spm,[status(thm)],[70,3402,theory(equality)])). cnf(3655,plain,(addition(antidomain(zero),antidomain(multiplication(coantidomain(coantidomain(X1)),antidomain(antidomain(coantidomain(X1))))))=antidomain(multiplication(coantidomain(coantidomain(X1)),antidomain(antidomain(coantidomain(X1)))))),inference(spm,[status(thm)],[66,3421,theory(equality)])). cnf(3687,plain,(one=antidomain(multiplication(coantidomain(coantidomain(X1)),antidomain(antidomain(coantidomain(X1)))))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[3655,370,theory(equality)]),314,theory(equality)])). cnf(3737,plain,(multiplication(antidomain(coantidomain(X1)),one)=multiplication(antidomain(coantidomain(X1)),coantidomain(coantidomain(X1)))),inference(spm,[status(thm)],[2898,101,theory(equality)])). cnf(3786,plain,(antidomain(coantidomain(X1))=multiplication(antidomain(coantidomain(X1)),coantidomain(coantidomain(X1)))),inference(rw,[status(thm)],[3737,52,theory(equality)])). cnf(4038,plain,(multiplication(one,coantidomain(antidomain(X1)))=multiplication(antidomain(antidomain(X1)),coantidomain(antidomain(X1)))),inference(spm,[status(thm)],[3370,100,theory(equality)])). cnf(4088,plain,(coantidomain(antidomain(X1))=multiplication(antidomain(antidomain(X1)),coantidomain(antidomain(X1)))),inference(rw,[status(thm)],[4038,44,theory(equality)])). cnf(4451,plain,(multiplication(one,multiplication(coantidomain(coantidomain(X1)),antidomain(antidomain(coantidomain(X1)))))=zero),inference(spm,[status(thm)],[68,3687,theory(equality)])). cnf(4488,plain,(multiplication(coantidomain(coantidomain(X1)),antidomain(antidomain(coantidomain(X1))))=zero),inference(rw,[status(thm)],[4451,44,theory(equality)])). cnf(4928,plain,(multiplication(X1,zero)=multiplication(X1,antidomain(antidomain(coantidomain(X1))))),inference(spm,[status(thm)],[711,4488,theory(equality)])). cnf(4973,plain,(zero=multiplication(X1,antidomain(antidomain(coantidomain(X1))))),inference(rw,[status(thm)],[4928,40,theory(equality)])). cnf(4999,plain,(addition(zero,multiplication(X1,X2))=multiplication(X1,addition(antidomain(antidomain(coantidomain(X1))),X2))),inference(spm,[status(thm)],[46,4973,theory(equality)])). cnf(5031,plain,(multiplication(X1,X2)=multiplication(X1,addition(antidomain(antidomain(coantidomain(X1))),X2))),inference(rw,[status(thm)],[4999,105,theory(equality)])). cnf(11040,plain,(multiplication(one,multiplication(X1,antidomain(antidomain(multiplication(coantidomain(X1),X2)))))=zero),inference(spm,[status(thm)],[68,439,theory(equality)])). cnf(11122,plain,(multiplication(X1,antidomain(antidomain(multiplication(coantidomain(X1),X2))))=zero),inference(rw,[status(thm)],[11040,44,theory(equality)])). cnf(11322,plain,(addition(zero,multiplication(X1,X3))=multiplication(X1,addition(antidomain(antidomain(multiplication(coantidomain(X1),X2))),X3))),inference(spm,[status(thm)],[46,11122,theory(equality)])). cnf(11415,plain,(multiplication(X1,X3)=multiplication(X1,addition(antidomain(antidomain(multiplication(coantidomain(X1),X2))),X3))),inference(rw,[status(thm)],[11322,105,theory(equality)])). cnf(17983,plain,(multiplication(one,X1)=multiplication(antidomain(antidomain(addition(X1,X2))),X1)),inference(spm,[status(thm)],[3059,100,theory(equality)])). cnf(18061,plain,(X1=multiplication(antidomain(antidomain(addition(X1,X2))),X1)),inference(rw,[status(thm)],[17983,44,theory(equality)])). cnf(18138,plain,(multiplication(antidomain(antidomain(addition(X2,X1))),X1)=X1),inference(spm,[status(thm)],[18061,293,theory(equality)])). cnf(22715,plain,(multiplication(one,X1)=multiplication(coantidomain(coantidomain(coantidomain(antidomain(X1)))),X1)),inference(spm,[status(thm)],[3206,101,theory(equality)])). cnf(22789,plain,(X1=multiplication(coantidomain(coantidomain(coantidomain(antidomain(X1)))),X1)),inference(rw,[status(thm)],[22715,44,theory(equality)])). cnf(22790,plain,(X1=multiplication(coantidomain(antidomain(X1)),X1)),inference(rw,[status(thm)],[22789,3402,theory(equality)])). cnf(22847,plain,(multiplication(coantidomain(antidomain(X1)),antidomain(antidomain(X1)))=antidomain(antidomain(X1))),inference(spm,[status(thm)],[22790,2931,theory(equality)])). cnf(24051,plain,(addition(coantidomain(antidomain(X1)),antidomain(antidomain(X1)))=multiplication(coantidomain(antidomain(X1)),addition(antidomain(antidomain(X1)),one))),inference(spm,[status(thm)],[1160,22847,theory(equality)])). cnf(24121,plain,(addition(coantidomain(antidomain(X1)),antidomain(antidomain(X1)))=coantidomain(antidomain(X1))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[24051,54,theory(equality)]),314,theory(equality)]),52,theory(equality)])). cnf(24195,plain,(addition(antidomain(antidomain(X1)),coantidomain(antidomain(X1)))=coantidomain(antidomain(X1))),inference(rw,[status(thm)],[24121,54,theory(equality)])). cnf(24239,plain,(addition(antidomain(X1),coantidomain(antidomain(X1)))=addition(one,coantidomain(antidomain(X1)))),inference(spm,[status(thm)],[139,24195,theory(equality)])). cnf(24294,plain,(addition(antidomain(X1),coantidomain(antidomain(X1)))=one),inference(rw,[status(thm)],[24239,308,theory(equality)])). cnf(24359,plain,(multiplication(antidomain(antidomain(X1)),one)=multiplication(antidomain(antidomain(X1)),coantidomain(antidomain(X1)))),inference(spm,[status(thm)],[2898,24294,theory(equality)])). cnf(24436,plain,(antidomain(antidomain(X1))=multiplication(antidomain(antidomain(X1)),coantidomain(antidomain(X1)))),inference(rw,[status(thm)],[24359,52,theory(equality)])). cnf(24437,plain,(antidomain(antidomain(X1))=coantidomain(antidomain(X1))),inference(rw,[status(thm)],[24436,4088,theory(equality)])). cnf(24590,negated_conjecture,(multiplication(antidomain(coantidomain(coantidomain(multiplication(antidomain(esk3_0),esk1_0)))),antidomain(esk2_0))=antidomain(esk2_0)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[3322,24437,theory(equality)]),24437,theory(equality)]),2931,theory(equality)])). cnf(25066,negated_conjecture,(multiplication(antidomain(antidomain(coantidomain(coantidomain(multiplication(antidomain(esk3_0),esk1_0))))),antidomain(esk2_0))=zero),inference(spm,[status(thm)],[126,24590,theory(equality)])). cnf(29002,plain,(multiplication(X1,one)=multiplication(X1,antidomain(antidomain(antidomain(coantidomain(X1)))))),inference(spm,[status(thm)],[5031,100,theory(equality)])). cnf(29099,plain,(X1=multiplication(X1,antidomain(antidomain(antidomain(coantidomain(X1)))))),inference(rw,[status(thm)],[29002,52,theory(equality)])). cnf(29100,plain,(X1=multiplication(X1,antidomain(coantidomain(X1)))),inference(rw,[status(thm)],[29099,2931,theory(equality)])). cnf(29129,plain,(multiplication(X1,X2)=multiplication(X1,multiplication(antidomain(coantidomain(X1)),X2))),inference(spm,[status(thm)],[30,29100,theory(equality)])). cnf(29160,plain,(multiplication(coantidomain(coantidomain(X1)),antidomain(coantidomain(X1)))=coantidomain(coantidomain(X1))),inference(spm,[status(thm)],[29100,3402,theory(equality)])). cnf(29563,plain,(addition(antidomain(coantidomain(X1)),coantidomain(coantidomain(X1)))=multiplication(addition(coantidomain(coantidomain(X1)),one),antidomain(coantidomain(X1)))),inference(spm,[status(thm)],[2027,29160,theory(equality)])). cnf(29628,plain,(addition(antidomain(coantidomain(X1)),coantidomain(coantidomain(X1)))=antidomain(coantidomain(X1))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[29563,54,theory(equality)]),308,theory(equality)]),44,theory(equality)])). cnf(29718,plain,(multiplication(antidomain(antidomain(antidomain(coantidomain(X1)))),coantidomain(coantidomain(X1)))=coantidomain(coantidomain(X1))),inference(spm,[status(thm)],[18138,29628,theory(equality)])). cnf(29793,plain,(antidomain(coantidomain(X1))=coantidomain(coantidomain(X1))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[29718,2931,theory(equality)]),3786,theory(equality)])). cnf(29929,negated_conjecture,(multiplication(antidomain(coantidomain(multiplication(antidomain(esk3_0),esk1_0))),antidomain(esk2_0))=zero),inference(rw,[status(thm)],[inference(rw,[status(thm)],[25066,29793,theory(equality)]),2931,theory(equality)])). cnf(30930,negated_conjecture,(multiplication(multiplication(antidomain(esk3_0),esk1_0),zero)=multiplication(multiplication(antidomain(esk3_0),esk1_0),antidomain(esk2_0))),inference(spm,[status(thm)],[29129,29929,theory(equality)])). cnf(30963,negated_conjecture,(zero=multiplication(multiplication(antidomain(esk3_0),esk1_0),antidomain(esk2_0))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[30930,30,theory(equality)]),40,theory(equality)]),40,theory(equality)])). cnf(30964,negated_conjecture,(zero=multiplication(antidomain(esk3_0),multiplication(esk1_0,antidomain(esk2_0)))),inference(rw,[status(thm)],[30963,30,theory(equality)])). cnf(30967,negated_conjecture,(addition(zero,multiplication(X1,multiplication(esk1_0,antidomain(esk2_0))))=multiplication(addition(antidomain(esk3_0),X1),multiplication(esk1_0,antidomain(esk2_0)))),inference(spm,[status(thm)],[42,30964,theory(equality)])). cnf(30998,negated_conjecture,(multiplication(X1,multiplication(esk1_0,antidomain(esk2_0)))=multiplication(addition(antidomain(esk3_0),X1),multiplication(esk1_0,antidomain(esk2_0)))),inference(rw,[status(thm)],[30967,105,theory(equality)])). cnf(1342246,negated_conjecture,(multiplication(one,multiplication(esk1_0,antidomain(esk2_0)))=multiplication(antidomain(antidomain(esk3_0)),multiplication(esk1_0,antidomain(esk2_0)))),inference(spm,[status(thm)],[30998,100,theory(equality)])). cnf(1342631,negated_conjecture,(multiplication(esk1_0,antidomain(esk2_0))=multiplication(antidomain(antidomain(esk3_0)),multiplication(esk1_0,antidomain(esk2_0)))),inference(rw,[status(thm)],[1342246,44,theory(equality)])). cnf(1413947,plain,(multiplication(X1,one)=multiplication(X1,antidomain(antidomain(antidomain(multiplication(coantidomain(X1),X2)))))),inference(spm,[status(thm)],[11415,100,theory(equality)])). cnf(1415146,plain,(X1=multiplication(X1,antidomain(antidomain(antidomain(multiplication(coantidomain(X1),X2)))))),inference(rw,[status(thm)],[1413947,52,theory(equality)])). cnf(1415147,plain,(X1=multiplication(X1,antidomain(multiplication(coantidomain(X1),X2)))),inference(rw,[status(thm)],[1415146,2931,theory(equality)])). cnf(1415716,plain,(multiplication(antidomain(X1),antidomain(multiplication(antidomain(antidomain(X1)),X2)))=antidomain(X1)),inference(spm,[status(thm)],[1415147,24437,theory(equality)])). cnf(1424807,negated_conjecture,(multiplication(antidomain(esk3_0),antidomain(multiplication(esk1_0,antidomain(esk2_0))))=antidomain(esk3_0)),inference(spm,[status(thm)],[1415716,1342631,theory(equality)])). cnf(1428484,negated_conjecture,(addition(antidomain(multiplication(esk1_0,antidomain(esk2_0))),addition(coantidomain(antidomain(esk3_0)),antidomain(esk3_0)))=multiplication(addition(antidomain(esk3_0),one),addition(antidomain(multiplication(esk1_0,antidomain(esk2_0))),coantidomain(antidomain(esk3_0))))),inference(spm,[status(thm)],[2116,1424807,theory(equality)])). cnf(1428750,negated_conjecture,(one=multiplication(addition(antidomain(esk3_0),one),addition(antidomain(multiplication(esk1_0,antidomain(esk2_0))),coantidomain(antidomain(esk3_0))))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[1428484,24437,theory(equality)]),54,theory(equality)]),100,theory(equality)]),54,theory(equality)]),314,theory(equality)])). cnf(1428751,negated_conjecture,(one=addition(antidomain(antidomain(esk3_0)),antidomain(multiplication(esk1_0,antidomain(esk2_0))))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[1428750,54,theory(equality)]),314,theory(equality)]),24437,theory(equality)]),54,theory(equality)]),44,theory(equality)])). cnf(1428752,negated_conjecture,($false),inference(sr,[status(thm)],[1428751,2984,theory(equality)])). cnf(1428753,negated_conjecture,($false),1428752,['proof']). # SZS output end CNFRefutation WATCH: 20.14 CPU 11.20 WC FINAL WATCH: 20.14 CPU 11.20 WC