%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KLE091+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:58:19 PM UTC 2026
% Result : Theorem 37.69s 5.29s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE091+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n017.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sun Sep 20 22:37:57 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.44 % Drodi V4.1.1
% 37.69/5.29 % Refutation found
% 37.69/5.29 % SZS status Theorem for theBenchmark: Theorem is valid
% 37.69/5.29 % SZS output start CNFRefutation for theBenchmark
% 37.69/5.29 fof(f1,axiom,(
% 37.69/5.29 (! [A,B] : addition(A,B) = addition(B,A) )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f2,axiom,(
% 37.69/5.29 (! [C,B,A] : addition(A,addition(B,C)) = addition(addition(A,B),C) )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f3,axiom,(
% 37.69/5.29 (! [A] : addition(A,zero) = A )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f4,axiom,(
% 37.69/5.29 (! [A] : addition(A,A) = A )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f5,axiom,(
% 37.69/5.29 (! [A,B,C] : multiplication(A,multiplication(B,C)) = multiplication(multiplication(A,B),C) )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f6,axiom,(
% 37.69/5.29 (! [A] : multiplication(A,one) = A )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f7,axiom,(
% 37.69/5.29 (! [A] : multiplication(one,A) = A )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f8,axiom,(
% 37.69/5.29 (! [A,B,C] : multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)) )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f9,axiom,(
% 37.69/5.29 (! [A,B,C] : multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)) )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f13,axiom,(
% 37.69/5.29 (! [X0] : multiplication(antidomain(X0),X0) = zero )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f14,axiom,(
% 37.69/5.29 (! [X0,X1] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))) )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f15,axiom,(
% 37.69/5.29 (! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f16,axiom,(
% 37.69/5.29 (! [X0] : domain(X0) = antidomain(antidomain(X0)) )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f17,axiom,(
% 37.69/5.29 (! [X0] : multiplication(X0,coantidomain(X0)) = zero )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f18,axiom,(
% 37.69/5.29 (! [X0,X1] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)) )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f19,axiom,(
% 37.69/5.29 (! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f20,axiom,(
% 37.69/5.29 (! [X0] : codomain(X0) = coantidomain(coantidomain(X0)) )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f21,conjecture,(
% 37.69/5.29 (! [X0] : domain(codomain(X0)) = codomain(X0) )),
% 37.69/5.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 37.69/5.29 fof(f22,negated_conjecture,(
% 37.69/5.29 ~((! [X0] : domain(codomain(X0)) = codomain(X0) ))),
% 37.69/5.29 inference(negated_conjecture,[status(cth)],[f21])).
% 37.69/5.29 fof(f23,plain,(
% 37.69/5.29 ![X0,X1]: (addition(X0,X1)=addition(X1,X0))),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f1])).
% 37.69/5.29 fof(f24,plain,(
% 37.69/5.29 ![X0,X1,X2]: (addition(X0,addition(X1,X2))=addition(addition(X0,X1),X2))),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f2])).
% 37.69/5.29 fof(f25,plain,(
% 37.69/5.29 ![X0]: (addition(X0,zero)=X0)),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f3])).
% 37.69/5.29 fof(f26,plain,(
% 37.69/5.29 ![X0]: (addition(X0,X0)=X0)),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f4])).
% 37.69/5.29 fof(f27,plain,(
% 37.69/5.29 ![X0,X1,X2]: (multiplication(X0,multiplication(X1,X2))=multiplication(multiplication(X0,X1),X2))),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f5])).
% 37.69/5.29 fof(f28,plain,(
% 37.69/5.29 ![X0]: (multiplication(X0,one)=X0)),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f6])).
% 37.69/5.29 fof(f29,plain,(
% 37.69/5.29 ![X0]: (multiplication(one,X0)=X0)),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f7])).
% 37.69/5.29 fof(f30,plain,(
% 37.69/5.29 ![X0,X1,X2]: (multiplication(X0,addition(X1,X2))=addition(multiplication(X0,X1),multiplication(X0,X2)))),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f8])).
% 37.69/5.29 fof(f31,plain,(
% 37.69/5.29 ![X0,X1,X2]: (multiplication(addition(X0,X1),X2)=addition(multiplication(X0,X2),multiplication(X1,X2)))),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f9])).
% 37.69/5.29 fof(f38,plain,(
% 37.69/5.29 ![X0]: (multiplication(antidomain(X0),X0)=zero)),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f13])).
% 37.69/5.29 fof(f39,plain,(
% 37.69/5.29 ![X0,X1]: (addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1)))))=antidomain(multiplication(X0,antidomain(antidomain(X1)))))),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f14])).
% 37.69/5.29 fof(f40,plain,(
% 37.69/5.29 ![X0]: (addition(antidomain(antidomain(X0)),antidomain(X0))=one)),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f15])).
% 37.69/5.29 fof(f41,plain,(
% 37.69/5.29 ![X0]: (domain(X0)=antidomain(antidomain(X0)))),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f16])).
% 37.69/5.29 fof(f42,plain,(
% 37.69/5.29 ![X0]: (multiplication(X0,coantidomain(X0))=zero)),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f17])).
% 37.69/5.29 fof(f43,plain,(
% 37.69/5.29 ![X0,X1]: (addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)))=coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)))),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f18])).
% 37.69/5.29 fof(f44,plain,(
% 37.69/5.29 ![X0]: (addition(coantidomain(coantidomain(X0)),coantidomain(X0))=one)),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f19])).
% 37.69/5.29 fof(f45,plain,(
% 37.69/5.29 ![X0]: (codomain(X0)=coantidomain(coantidomain(X0)))),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f20])).
% 37.69/5.29 fof(f46,plain,(
% 37.69/5.29 (?[X0]: ~domain(codomain(X0))=codomain(X0))),
% 37.69/5.29 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 37.69/5.29 fof(f47,plain,(
% 37.69/5.29 ~domain(codomain(sK0_skl))=codomain(sK0_skl)),
% 37.69/5.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X0,sK0_skl)],[f46])).
% 37.69/5.29 fof(f48,plain,(
% 37.69/5.29 ~domain(codomain(sK0_skl))=codomain(sK0_skl)),
% 37.69/5.29 inference(cnf_transformation,[status(thm)],[f47])).
% 37.69/5.29 fof(f49,plain,(
% 37.69/5.29 ![X0]: (addition(domain(X0),antidomain(X0))=one)),
% 37.69/5.29 inference(backward_demodulation,[status(thm)],[f41,f40])).
% 37.69/5.29 fof(f50,plain,(
% 37.69/5.29 ![X0,X1]: (addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1)))))=antidomain(multiplication(X0,domain(X1))))),
% 37.69/5.29 inference(backward_demodulation,[status(thm)],[f41,f39])).
% 37.69/5.29 fof(f51,plain,(
% 37.69/5.29 ![X0]: (addition(codomain(X0),coantidomain(X0))=one)),
% 37.69/5.29 inference(backward_demodulation,[status(thm)],[f45,f44])).
% 37.69/5.29 fof(f52,plain,(
% 37.69/5.29 ![X0,X1]: (addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)))=coantidomain(multiplication(codomain(X0),X1)))),
% 37.69/5.29 inference(backward_demodulation,[status(thm)],[f45,f43])).
% 37.69/5.29 fof(f53,plain,(
% 37.69/5.29 ![X0,X1]: (addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,domain(X1))))=antidomain(multiplication(X0,domain(X1))))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f41,f50])).
% 37.69/5.29 fof(f54,plain,(
% 37.69/5.29 ![X0,X1]: (addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(codomain(X0),X1)))=coantidomain(multiplication(codomain(X0),X1)))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f45,f52])).
% 37.69/5.29 fof(f59,plain,(
% 37.69/5.29 ![X0]: (X0=addition(zero,X0))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f25,f23])).
% 37.69/5.29 fof(f82,plain,(
% 37.69/5.29 antidomain(one)=zero),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f28,f38])).
% 37.69/5.29 fof(f86,plain,(
% 37.69/5.29 ![X0,X1,X2]: (addition(X0,addition(X1,X2))=addition(X2,addition(X0,X1)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f23,f24])).
% 37.69/5.29 fof(f94,plain,(
% 37.69/5.29 ![X0,X1]: (addition(X0,addition(X0,X1))=addition(X0,X1))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f26,f24])).
% 37.69/5.29 fof(f102,plain,(
% 37.69/5.29 ![X0]: (domain(antidomain(X0))=antidomain(domain(X0)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f41,f41])).
% 37.69/5.29 fof(f103,plain,(
% 37.69/5.29 domain(one)=antidomain(zero)),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f82,f41])).
% 37.69/5.29 fof(f104,plain,(
% 37.69/5.29 ![X0]: (multiplication(domain(X0),antidomain(X0))=zero)),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f41,f38])).
% 37.69/5.29 fof(f106,plain,(
% 37.69/5.29 coantidomain(one)=zero),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f29,f42])).
% 37.69/5.29 fof(f110,plain,(
% 37.69/5.29 ![X0,X1]: (multiplication(X0,multiplication(X1,coantidomain(multiplication(X0,X1))))=zero)),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f42,f27])).
% 37.69/5.29 fof(f132,plain,(
% 37.69/5.29 ![X0]: (codomain(coantidomain(X0))=coantidomain(codomain(X0)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f45,f45])).
% 37.69/5.29 fof(f133,plain,(
% 37.69/5.29 codomain(one)=coantidomain(zero)),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f106,f45])).
% 37.69/5.29 fof(f141,plain,(
% 37.69/5.29 ![X0,X1,X2]: (multiplication(X0,addition(X1,X2))=addition(multiplication(X0,X2),multiplication(X0,X1)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f23,f30])).
% 37.69/5.29 fof(f145,plain,(
% 37.69/5.29 ![X0,X1]: (multiplication(antidomain(X0),addition(X0,X1))=addition(zero,multiplication(antidomain(X0),X1)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f38,f30])).
% 37.69/5.29 fof(f148,plain,(
% 37.69/5.29 ![X0,X1]: (multiplication(X0,addition(coantidomain(X0),X1))=addition(zero,multiplication(X0,X1)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f42,f30])).
% 37.69/5.29 fof(f165,plain,(
% 37.69/5.29 ![X0,X1]: (multiplication(antidomain(X0),addition(X0,X1))=multiplication(antidomain(X0),X1))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f59,f145])).
% 37.69/5.29 fof(f169,plain,(
% 37.69/5.29 ![X0,X1]: (multiplication(X0,addition(coantidomain(X0),X1))=multiplication(X0,X1))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f59,f148])).
% 37.69/5.29 fof(f183,plain,(
% 37.69/5.29 addition(domain(one),zero)=one),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f82,f49])).
% 37.69/5.29 fof(f184,plain,(
% 37.69/5.29 ![X0,X1]: (addition(domain(X0),addition(antidomain(X0),X1))=addition(one,X1))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f49,f24])).
% 37.69/5.29 fof(f185,plain,(
% 37.69/5.29 one=antidomain(zero)),
% 37.69/5.29 inference(backward_demodulation,[status(thm)],[f187,f103])).
% 37.69/5.29 fof(f187,plain,(
% 37.69/5.29 domain(one)=one),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f25,f183])).
% 37.69/5.29 fof(f195,plain,(
% 37.69/5.29 ![X0,X1]: (multiplication(addition(antidomain(X0),X1),X0)=addition(zero,multiplication(X1,X0)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f38,f31])).
% 37.69/5.29 fof(f198,plain,(
% 37.69/5.29 ![X0,X1]: (multiplication(addition(X0,X1),coantidomain(X0))=addition(zero,multiplication(X1,coantidomain(X0))))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f42,f31])).
% 37.69/5.29 fof(f204,plain,(
% 37.69/5.29 ![X0,X1]: (multiplication(addition(X0,one),X1)=addition(multiplication(X0,X1),X1))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f29,f31])).
% 37.69/5.29 fof(f214,plain,(
% 37.69/5.29 ![X0,X1]: (multiplication(addition(antidomain(X0),X1),X0)=multiplication(X1,X0))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f59,f195])).
% 37.69/5.29 fof(f216,plain,(
% 37.69/5.29 ![X0,X1]: (multiplication(addition(X0,X1),coantidomain(X0))=multiplication(X1,coantidomain(X0)))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f59,f198])).
% 37.69/5.29 fof(f236,plain,(
% 37.69/5.29 addition(codomain(one),zero)=one),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f106,f51])).
% 37.69/5.29 fof(f238,plain,(
% 37.69/5.29 one=coantidomain(zero)),
% 37.69/5.29 inference(backward_demodulation,[status(thm)],[f240,f133])).
% 37.69/5.29 fof(f240,plain,(
% 37.69/5.29 codomain(one)=one),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f25,f236])).
% 37.69/5.29 fof(f247,plain,(
% 37.69/5.29 ![X0]: (addition(antidomain(zero),antidomain(multiplication(X0,domain(coantidomain(X0)))))=antidomain(multiplication(X0,domain(coantidomain(X0)))))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f42,f53])).
% 37.69/5.29 fof(f269,plain,(
% 37.69/5.29 ![X0]: (addition(one,antidomain(multiplication(X0,domain(coantidomain(X0)))))=antidomain(multiplication(X0,domain(coantidomain(X0)))))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f185,f247])).
% 37.69/5.29 fof(f328,plain,(
% 37.69/5.29 ![X0,X1]: (multiplication(addition(domain(X0),X1),antidomain(X0))=addition(zero,multiplication(X1,antidomain(X0))))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f104,f31])).
% 37.69/5.29 fof(f336,plain,(
% 37.69/5.29 ![X0,X1]: (multiplication(addition(domain(X0),X1),antidomain(X0))=multiplication(X1,antidomain(X0)))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f59,f328])).
% 37.69/5.29 fof(f342,plain,(
% 37.69/5.29 ![X0]: (addition(coantidomain(zero),coantidomain(multiplication(codomain(antidomain(X0)),X0)))=coantidomain(multiplication(codomain(antidomain(X0)),X0)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f38,f54])).
% 37.69/5.29 fof(f347,plain,(
% 37.69/5.29 ![X0]: (addition(coantidomain(X0),coantidomain(multiplication(codomain(X0),one)))=coantidomain(multiplication(codomain(X0),one)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f28,f54])).
% 37.69/5.29 fof(f355,plain,(
% 37.69/5.29 ![X0]: (addition(one,coantidomain(multiplication(codomain(antidomain(X0)),X0)))=coantidomain(multiplication(codomain(antidomain(X0)),X0)))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f238,f342])).
% 37.69/5.29 fof(f373,plain,(
% 37.69/5.29 ![X0]: (addition(coantidomain(X0),coantidomain(codomain(X0)))=coantidomain(multiplication(codomain(X0),one)))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f28,f347])).
% 37.69/5.29 fof(f374,plain,(
% 37.69/5.29 ![X0]: (addition(coantidomain(X0),codomain(coantidomain(X0)))=coantidomain(multiplication(codomain(X0),one)))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f132,f373])).
% 37.69/5.29 fof(f375,plain,(
% 37.69/5.29 ![X0]: (addition(coantidomain(X0),codomain(coantidomain(X0)))=coantidomain(codomain(X0)))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f28,f374])).
% 37.69/5.29 fof(f376,plain,(
% 37.69/5.29 ![X0]: (addition(coantidomain(X0),codomain(coantidomain(X0)))=codomain(coantidomain(X0)))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f132,f375])).
% 37.69/5.29 fof(f433,plain,(
% 37.69/5.29 ![X0]: (addition(codomain(X0),one)=addition(codomain(X0),coantidomain(X0)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f51,f94])).
% 37.69/5.29 fof(f441,plain,(
% 37.69/5.29 ![X0,X1]: (addition(X0,addition(X1,X0))=addition(X0,X1))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f23,f94])).
% 37.69/5.29 fof(f449,plain,(
% 37.69/5.29 ![X0]: (addition(codomain(X0),one)=one)),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f51,f433])).
% 37.69/5.29 fof(f463,plain,(
% 37.69/5.29 ![X0]: (addition(one,codomain(X0))=one)),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f23,f449])).
% 37.69/5.29 fof(f478,plain,(
% 37.69/5.29 ![X0,X1]: (addition(X0,X1)=addition(X1,addition(addition(X0,X1),X0)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f26,f86])).
% 37.69/5.29 fof(f538,plain,(
% 37.69/5.29 ![X0,X1]: (addition(X0,X1)=addition(X1,addition(X0,addition(X1,X0))))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f24,f478])).
% 37.69/5.29 fof(f539,plain,(
% 37.69/5.29 ![X0,X1]: (addition(X0,X1)=addition(X1,addition(X0,X1)))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f441,f538])).
% 37.69/5.29 fof(f750,plain,(
% 37.69/5.29 ![X0]: (addition(coantidomain(X0),one)=addition(coantidomain(X0),codomain(X0)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f51,f441])).
% 37.69/5.29 fof(f752,plain,(
% 37.69/5.29 ![X0]: (addition(antidomain(X0),one)=addition(antidomain(X0),domain(X0)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f49,f441])).
% 37.69/5.29 fof(f833,plain,(
% 37.69/5.29 ![X0]: (addition(codomain(X0),coantidomain(X0))=addition(coantidomain(X0),one))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f51,f539])).
% 37.69/5.29 fof(f835,plain,(
% 37.69/5.29 ![X0]: (addition(domain(X0),antidomain(X0))=addition(antidomain(X0),one))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f49,f539])).
% 37.69/5.29 fof(f872,plain,(
% 37.69/5.29 ![X0]: (one=addition(coantidomain(X0),codomain(X0)))),
% 37.69/5.29 inference(backward_demodulation,[status(thm)],[f873,f750])).
% 37.69/5.29 fof(f873,plain,(
% 37.69/5.29 ![X0]: (one=addition(coantidomain(X0),one))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f51,f833])).
% 37.69/5.29 fof(f876,plain,(
% 37.69/5.29 ![X0]: (one=addition(antidomain(X0),domain(X0)))),
% 37.69/5.29 inference(backward_demodulation,[status(thm)],[f877,f752])).
% 37.69/5.29 fof(f877,plain,(
% 37.69/5.29 ![X0]: (one=addition(antidomain(X0),one))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f49,f835])).
% 37.69/5.29 fof(f914,plain,(
% 37.69/5.29 ![X0]: (one=addition(one,coantidomain(X0)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f23,f873])).
% 37.69/5.29 fof(f931,plain,(
% 37.69/5.29 ![X0]: (one=coantidomain(multiplication(codomain(antidomain(X0)),X0)))),
% 37.69/5.29 inference(backward_demodulation,[status(thm)],[f914,f355])).
% 37.69/5.29 fof(f996,plain,(
% 37.69/5.29 ![X0]: (one=addition(one,antidomain(X0)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f23,f877])).
% 37.69/5.29 fof(f1017,plain,(
% 37.69/5.29 ![X0]: (one=antidomain(multiplication(X0,domain(coantidomain(X0)))))),
% 37.69/5.29 inference(backward_demodulation,[status(thm)],[f996,f269])).
% 37.69/5.29 fof(f1360,plain,(
% 37.69/5.29 ![X0]: (multiplication(antidomain(coantidomain(X0)),one)=multiplication(antidomain(coantidomain(X0)),codomain(X0)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f872,f165])).
% 37.69/5.29 fof(f1370,plain,(
% 37.69/5.29 ![X0]: (multiplication(antidomain(domain(X0)),one)=multiplication(antidomain(domain(X0)),antidomain(X0)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f49,f165])).
% 37.69/5.29 fof(f1413,plain,(
% 37.69/5.29 ![X0]: (antidomain(coantidomain(X0))=multiplication(antidomain(coantidomain(X0)),codomain(X0)))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f28,f1360])).
% 37.69/5.29 fof(f1424,plain,(
% 37.69/5.29 ![X0]: (antidomain(domain(X0))=multiplication(antidomain(domain(X0)),antidomain(X0)))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f28,f1370])).
% 37.69/5.29 fof(f1425,plain,(
% 37.69/5.29 ![X0]: (domain(antidomain(X0))=multiplication(antidomain(domain(X0)),antidomain(X0)))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f102,f1424])).
% 37.69/5.29 fof(f1426,plain,(
% 37.69/5.29 ![X0]: (domain(antidomain(X0))=multiplication(domain(antidomain(X0)),antidomain(X0)))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f102,f1425])).
% 37.69/5.29 fof(f1556,plain,(
% 37.69/5.29 ![X0]: (multiplication(codomain(antidomain(X0)),multiplication(X0,one))=zero)),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f931,f110])).
% 37.69/5.29 fof(f1577,plain,(
% 37.69/5.29 ![X0]: (multiplication(codomain(antidomain(X0)),X0)=zero)),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f28,f1556])).
% 37.69/5.29 fof(f1594,plain,(
% 37.69/5.29 ![X0]: (multiplication(X0,one)=multiplication(X0,codomain(X0)))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f872,f169])).
% 37.69/5.29 fof(f1629,plain,(
% 37.69/5.29 ![X0]: (X0=multiplication(X0,codomain(X0)))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f28,f1594])).
% 37.69/5.29 fof(f1663,plain,(
% 37.69/5.29 ![X0]: (addition(coantidomain(X0),coantidomain(multiplication(codomain(X0),codomain(X0))))=coantidomain(multiplication(codomain(X0),codomain(X0))))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f1629,f54])).
% 37.69/5.29 fof(f2008,plain,(
% 37.69/5.29 ![X0]: (multiplication(codomain(one),multiplication(X0,domain(coantidomain(X0))))=zero)),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f1017,f1577])).
% 37.69/5.29 fof(f2030,plain,(
% 37.69/5.29 ![X0]: (multiplication(one,multiplication(X0,domain(coantidomain(X0))))=zero)),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f240,f2008])).
% 37.69/5.29 fof(f2033,plain,(
% 37.69/5.29 ![X0]: (multiplication(X0,domain(coantidomain(X0)))=zero)),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f29,f2030])).
% 37.69/5.29 fof(f2062,plain,(
% 37.69/5.29 ![X0,X1]: (multiplication(X0,addition(domain(coantidomain(X0)),X1))=addition(multiplication(X0,X1),zero))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f2033,f141])).
% 37.69/5.29 fof(f2089,plain,(
% 37.69/5.29 ![X0,X1]: (multiplication(X0,addition(domain(coantidomain(X0)),X1))=multiplication(X0,X1))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f25,f2062])).
% 37.69/5.29 fof(f3640,plain,(
% 37.69/5.29 ![X0]: (multiplication(one,X0)=multiplication(domain(X0),X0))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f876,f214])).
% 37.69/5.29 fof(f3682,plain,(
% 37.69/5.29 ![X0]: (domain(antidomain(X0))=antidomain(X0))),
% 37.69/5.29 inference(backward_demodulation,[status(thm)],[f3684,f1426])).
% 37.69/5.29 fof(f3684,plain,(
% 37.69/5.29 ![X0]: (X0=multiplication(domain(X0),X0))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f29,f3640])).
% 37.69/5.29 fof(f5466,plain,(
% 37.69/5.29 ![X0]: (multiplication(one,coantidomain(coantidomain(X0)))=multiplication(codomain(X0),coantidomain(coantidomain(X0))))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f872,f216])).
% 37.69/5.29 fof(f5474,plain,(
% 37.69/5.29 ![X0]: (multiplication(one,coantidomain(codomain(X0)))=multiplication(coantidomain(X0),coantidomain(codomain(X0))))),
% 37.69/5.29 inference(paramodulation,[status(thm)],[f51,f216])).
% 37.69/5.29 fof(f5539,plain,(
% 37.69/5.29 ![X0]: (coantidomain(coantidomain(X0))=multiplication(codomain(X0),coantidomain(coantidomain(X0))))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f29,f5466])).
% 37.69/5.29 fof(f5540,plain,(
% 37.69/5.29 ![X0]: (codomain(X0)=multiplication(codomain(X0),coantidomain(coantidomain(X0))))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f45,f5539])).
% 37.69/5.29 fof(f5541,plain,(
% 37.69/5.29 ![X0]: (addition(coantidomain(X0),coantidomain(multiplication(codomain(X0),codomain(X0))))=coantidomain(codomain(X0)))),
% 37.69/5.29 inference(backward_demodulation,[status(thm)],[f5542,f1663])).
% 37.69/5.29 fof(f5542,plain,(
% 37.69/5.29 ![X0]: (codomain(X0)=multiplication(codomain(X0),codomain(X0)))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f45,f5540])).
% 37.69/5.29 fof(f5602,plain,(
% 37.69/5.29 ![X0]: (coantidomain(codomain(X0))=multiplication(coantidomain(X0),coantidomain(codomain(X0))))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f29,f5474])).
% 37.69/5.29 fof(f5603,plain,(
% 37.69/5.29 ![X0]: (codomain(coantidomain(X0))=multiplication(coantidomain(X0),coantidomain(codomain(X0))))),
% 37.69/5.29 inference(forward_demodulation,[status(thm)],[f132,f5602])).
% 37.69/5.29 fof(f5604,plain,(
% 37.69/5.29 ![X0]: (codomain(coantidomain(X0))=multiplication(coantidomain(X0),codomain(coantidomain(X0))))),
% 38.55/5.36 inference(forward_demodulation,[status(thm)],[f132,f5603])).
% 38.55/5.36 fof(f5650,plain,(
% 38.55/5.36 ![X0]: (codomain(coantidomain(X0))=coantidomain(X0))),
% 38.55/5.36 inference(forward_demodulation,[status(thm)],[f1629,f5604])).
% 38.55/5.36 fof(f5706,plain,(
% 38.55/5.36 ![X0]: (addition(coantidomain(X0),coantidomain(codomain(X0)))=coantidomain(codomain(X0)))),
% 38.55/5.36 inference(forward_demodulation,[status(thm)],[f5542,f5541])).
% 38.55/5.36 fof(f5707,plain,(
% 38.55/5.36 ![X0]: (addition(coantidomain(X0),codomain(coantidomain(X0)))=coantidomain(codomain(X0)))),
% 38.55/5.36 inference(forward_demodulation,[status(thm)],[f132,f5706])).
% 38.55/5.36 fof(f5708,plain,(
% 38.55/5.36 ![X0]: (codomain(coantidomain(X0))=coantidomain(codomain(X0)))),
% 38.55/5.36 inference(forward_demodulation,[status(thm)],[f376,f5707])).
% 38.55/5.36 fof(f5709,plain,(
% 38.55/5.36 ![X0]: (coantidomain(X0)=coantidomain(codomain(X0)))),
% 38.55/5.36 inference(forward_demodulation,[status(thm)],[f5650,f5708])).
% 38.55/5.36 fof(f24913,plain,(
% 38.55/5.36 ![X0]: (multiplication(addition(antidomain(coantidomain(X0)),one),codomain(X0))=addition(antidomain(coantidomain(X0)),codomain(X0)))),
% 38.55/5.36 inference(paramodulation,[status(thm)],[f1413,f204])).
% 38.55/5.36 fof(f24997,plain,(
% 38.55/5.36 ![X0]: (multiplication(one,codomain(X0))=addition(antidomain(coantidomain(X0)),codomain(X0)))),
% 38.55/5.36 inference(forward_demodulation,[status(thm)],[f877,f24913])).
% 38.55/5.36 fof(f24998,plain,(
% 38.55/5.36 ![X0]: (codomain(X0)=addition(antidomain(coantidomain(X0)),codomain(X0)))),
% 38.55/5.36 inference(forward_demodulation,[status(thm)],[f29,f24997])).
% 38.55/5.36 fof(f25038,plain,(
% 38.55/5.36 ![X0]: (addition(domain(coantidomain(X0)),codomain(X0))=addition(one,codomain(X0)))),
% 38.55/5.36 inference(paramodulation,[status(thm)],[f24998,f184])).
% 38.55/5.36 fof(f25112,plain,(
% 38.55/5.36 ![X0]: (addition(domain(coantidomain(X0)),codomain(X0))=one)),
% 38.55/5.36 inference(forward_demodulation,[status(thm)],[f463,f25038])).
% 38.55/5.36 fof(f26507,plain,(
% 38.55/5.36 ![X0]: (multiplication(one,antidomain(coantidomain(X0)))=multiplication(codomain(X0),antidomain(coantidomain(X0))))),
% 38.55/5.36 inference(paramodulation,[status(thm)],[f25112,f336])).
% 38.55/5.36 fof(f26573,plain,(
% 38.55/5.36 ![X0]: (antidomain(coantidomain(X0))=multiplication(codomain(X0),antidomain(coantidomain(X0))))),
% 38.55/5.36 inference(forward_demodulation,[status(thm)],[f29,f26507])).
% 38.55/5.36 fof(f33891,plain,(
% 38.55/5.36 ![X0]: (multiplication(X0,one)=multiplication(X0,antidomain(coantidomain(X0))))),
% 38.55/5.36 inference(paramodulation,[status(thm)],[f49,f2089])).
% 38.55/5.36 fof(f34000,plain,(
% 38.55/5.36 ![X0]: (X0=multiplication(X0,antidomain(coantidomain(X0))))),
% 38.55/5.36 inference(forward_demodulation,[status(thm)],[f28,f33891])).
% 38.55/5.36 fof(f35400,plain,(
% 38.55/5.36 ![X0]: (codomain(X0)=multiplication(codomain(X0),antidomain(coantidomain(X0))))),
% 38.55/5.36 inference(paramodulation,[status(thm)],[f5709,f34000])).
% 38.55/5.36 fof(f35472,plain,(
% 38.55/5.36 ![X0]: (antidomain(coantidomain(X0))=codomain(X0))),
% 38.55/5.36 inference(backward_demodulation,[status(thm)],[f35400,f26573])).
% 38.55/5.36 fof(f36013,plain,(
% 38.55/5.36 ![X0]: (domain(codomain(X0))=antidomain(coantidomain(X0)))),
% 38.55/5.36 inference(paramodulation,[status(thm)],[f35472,f3682])).
% 38.55/5.36 fof(f36198,plain,(
% 38.55/5.36 ~codomain(sK0_skl)=codomain(sK0_skl)),
% 38.55/5.36 inference(backward_demodulation,[status(thm)],[f36262,f48])).
% 38.55/5.36 fof(f36262,plain,(
% 38.55/5.36 ![X0]: (domain(codomain(X0))=codomain(X0))),
% 38.55/5.36 inference(forward_demodulation,[status(thm)],[f35472,f36013])).
% 38.55/5.36 fof(f36392,plain,(
% 38.55/5.36 $false),
% 38.55/5.36 inference(trivial_equality_resolution,[status(thm)],[f36198])).
% 38.55/5.36 % SZS output end CNFRefutation for theBenchmark.p
% 38.55/5.37 % Elapsed time: 4.925751 seconds
% 38.55/5.37 % CPU time: 38.824667 seconds
% 38.55/5.37 % Total memory used: 417.567 MB
% 38.55/5.37 % Net memory used: 404.547 MB
%------------------------------------------------------------------------------