%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KLE092+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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 38.95s 5.34s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KLE092+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n005.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 22:42:48 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 38.95/5.34 % Refutation found
% 38.95/5.34 % SZS status Theorem for theBenchmark: Theorem is valid
% 38.95/5.34 % SZS output start CNFRefutation for theBenchmark
% 38.95/5.34 fof(f1,axiom,(
% 38.95/5.34 (! [A,B] : addition(A,B) = addition(B,A) )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f2,axiom,(
% 38.95/5.34 (! [C,B,A] : addition(A,addition(B,C)) = addition(addition(A,B),C) )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f3,axiom,(
% 38.95/5.34 (! [A] : addition(A,zero) = A )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f4,axiom,(
% 38.95/5.34 (! [A] : addition(A,A) = A )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f5,axiom,(
% 38.95/5.34 (! [A,B,C] : multiplication(A,multiplication(B,C)) = multiplication(multiplication(A,B),C) )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f6,axiom,(
% 38.95/5.34 (! [A] : multiplication(A,one) = A )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f7,axiom,(
% 38.95/5.34 (! [A] : multiplication(one,A) = A )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f8,axiom,(
% 38.95/5.34 (! [A,B,C] : multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)) )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f9,axiom,(
% 38.95/5.34 (! [A,B,C] : multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)) )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f13,axiom,(
% 38.95/5.34 (! [X0] : multiplication(antidomain(X0),X0) = zero )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f14,axiom,(
% 38.95/5.34 (! [X0,X1] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))) )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f15,axiom,(
% 38.95/5.34 (! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f16,axiom,(
% 38.95/5.34 (! [X0] : domain(X0) = antidomain(antidomain(X0)) )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f17,axiom,(
% 38.95/5.34 (! [X0] : multiplication(X0,coantidomain(X0)) = zero )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f18,axiom,(
% 38.95/5.34 (! [X0,X1] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)) )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f19,axiom,(
% 38.95/5.34 (! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f20,axiom,(
% 38.95/5.34 (! [X0] : codomain(X0) = coantidomain(coantidomain(X0)) )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f21,conjecture,(
% 38.95/5.34 (! [X0] : domain(coantidomain(X0)) = coantidomain(X0) )),
% 38.95/5.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.95/5.34 fof(f22,negated_conjecture,(
% 38.95/5.34 ~((! [X0] : domain(coantidomain(X0)) = coantidomain(X0) ))),
% 38.95/5.34 inference(negated_conjecture,[status(cth)],[f21])).
% 38.95/5.34 fof(f23,plain,(
% 38.95/5.34 ![X0,X1]: (addition(X0,X1)=addition(X1,X0))),
% 38.95/5.34 inference(cnf_transformation,[status(thm)],[f1])).
% 38.95/5.34 fof(f24,plain,(
% 38.95/5.34 ![X0,X1,X2]: (addition(X0,addition(X1,X2))=addition(addition(X0,X1),X2))),
% 38.95/5.34 inference(cnf_transformation,[status(thm)],[f2])).
% 38.95/5.34 fof(f25,plain,(
% 38.95/5.34 ![X0]: (addition(X0,zero)=X0)),
% 38.95/5.34 inference(cnf_transformation,[status(thm)],[f3])).
% 38.95/5.34 fof(f26,plain,(
% 38.95/5.34 ![X0]: (addition(X0,X0)=X0)),
% 38.95/5.34 inference(cnf_transformation,[status(thm)],[f4])).
% 38.95/5.34 fof(f27,plain,(
% 38.95/5.34 ![X0,X1,X2]: (multiplication(X0,multiplication(X1,X2))=multiplication(multiplication(X0,X1),X2))),
% 38.95/5.34 inference(cnf_transformation,[status(thm)],[f5])).
% 38.95/5.34 fof(f28,plain,(
% 38.95/5.34 ![X0]: (multiplication(X0,one)=X0)),
% 38.95/5.34 inference(cnf_transformation,[status(thm)],[f6])).
% 38.95/5.34 fof(f29,plain,(
% 38.95/5.34 ![X0]: (multiplication(one,X0)=X0)),
% 38.95/5.34 inference(cnf_transformation,[status(thm)],[f7])).
% 38.95/5.34 fof(f30,plain,(
% 38.95/5.34 ![X0,X1,X2]: (multiplication(X0,addition(X1,X2))=addition(multiplication(X0,X1),multiplication(X0,X2)))),
% 38.95/5.34 inference(cnf_transformation,[status(thm)],[f8])).
% 38.95/5.35 fof(f31,plain,(
% 38.95/5.35 ![X0,X1,X2]: (multiplication(addition(X0,X1),X2)=addition(multiplication(X0,X2),multiplication(X1,X2)))),
% 38.95/5.35 inference(cnf_transformation,[status(thm)],[f9])).
% 38.95/5.35 fof(f38,plain,(
% 38.95/5.35 ![X0]: (multiplication(antidomain(X0),X0)=zero)),
% 38.95/5.35 inference(cnf_transformation,[status(thm)],[f13])).
% 38.95/5.35 fof(f39,plain,(
% 38.95/5.35 ![X0,X1]: (addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1)))))=antidomain(multiplication(X0,antidomain(antidomain(X1)))))),
% 38.95/5.35 inference(cnf_transformation,[status(thm)],[f14])).
% 38.95/5.35 fof(f40,plain,(
% 38.95/5.35 ![X0]: (addition(antidomain(antidomain(X0)),antidomain(X0))=one)),
% 38.95/5.35 inference(cnf_transformation,[status(thm)],[f15])).
% 38.95/5.35 fof(f41,plain,(
% 38.95/5.35 ![X0]: (domain(X0)=antidomain(antidomain(X0)))),
% 38.95/5.35 inference(cnf_transformation,[status(thm)],[f16])).
% 38.95/5.35 fof(f42,plain,(
% 38.95/5.35 ![X0]: (multiplication(X0,coantidomain(X0))=zero)),
% 38.95/5.35 inference(cnf_transformation,[status(thm)],[f17])).
% 38.95/5.35 fof(f43,plain,(
% 38.95/5.35 ![X0,X1]: (addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)))=coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)))),
% 38.95/5.35 inference(cnf_transformation,[status(thm)],[f18])).
% 38.95/5.35 fof(f44,plain,(
% 38.95/5.35 ![X0]: (addition(coantidomain(coantidomain(X0)),coantidomain(X0))=one)),
% 38.95/5.35 inference(cnf_transformation,[status(thm)],[f19])).
% 38.95/5.35 fof(f45,plain,(
% 38.95/5.35 ![X0]: (codomain(X0)=coantidomain(coantidomain(X0)))),
% 38.95/5.35 inference(cnf_transformation,[status(thm)],[f20])).
% 38.95/5.35 fof(f46,plain,(
% 38.95/5.35 (?[X0]: ~domain(coantidomain(X0))=coantidomain(X0))),
% 38.95/5.35 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 38.95/5.35 fof(f47,plain,(
% 38.95/5.35 ~domain(coantidomain(sK0_skl))=coantidomain(sK0_skl)),
% 38.95/5.35 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X0,sK0_skl)],[f46])).
% 38.95/5.35 fof(f48,plain,(
% 38.95/5.35 ~domain(coantidomain(sK0_skl))=coantidomain(sK0_skl)),
% 38.95/5.35 inference(cnf_transformation,[status(thm)],[f47])).
% 38.95/5.35 fof(f49,plain,(
% 38.95/5.35 ![X0]: (addition(domain(X0),antidomain(X0))=one)),
% 38.95/5.35 inference(backward_demodulation,[status(thm)],[f41,f40])).
% 38.95/5.35 fof(f50,plain,(
% 38.95/5.35 ![X0,X1]: (addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1)))))=antidomain(multiplication(X0,domain(X1))))),
% 38.95/5.35 inference(backward_demodulation,[status(thm)],[f41,f39])).
% 38.95/5.35 fof(f51,plain,(
% 38.95/5.35 ![X0]: (addition(codomain(X0),coantidomain(X0))=one)),
% 38.95/5.35 inference(backward_demodulation,[status(thm)],[f45,f44])).
% 38.95/5.35 fof(f52,plain,(
% 38.95/5.35 ![X0,X1]: (addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)))=coantidomain(multiplication(codomain(X0),X1)))),
% 38.95/5.35 inference(backward_demodulation,[status(thm)],[f45,f43])).
% 38.95/5.35 fof(f53,plain,(
% 38.95/5.35 ![X0,X1]: (addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,domain(X1))))=antidomain(multiplication(X0,domain(X1))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f41,f50])).
% 38.95/5.35 fof(f54,plain,(
% 38.95/5.35 ![X0,X1]: (addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(codomain(X0),X1)))=coantidomain(multiplication(codomain(X0),X1)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f45,f52])).
% 38.95/5.35 fof(f59,plain,(
% 38.95/5.35 ![X0]: (X0=addition(zero,X0))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f25,f23])).
% 38.95/5.35 fof(f82,plain,(
% 38.95/5.35 antidomain(one)=zero),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f28,f38])).
% 38.95/5.35 fof(f86,plain,(
% 38.95/5.35 ![X0,X1,X2]: (addition(X0,addition(X1,X2))=addition(X2,addition(X0,X1)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f23,f24])).
% 38.95/5.35 fof(f94,plain,(
% 38.95/5.35 ![X0,X1]: (addition(X0,addition(X0,X1))=addition(X0,X1))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f26,f24])).
% 38.95/5.35 fof(f102,plain,(
% 38.95/5.35 ![X0]: (domain(antidomain(X0))=antidomain(domain(X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f41,f41])).
% 38.95/5.35 fof(f103,plain,(
% 38.95/5.35 domain(one)=antidomain(zero)),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f82,f41])).
% 38.95/5.35 fof(f104,plain,(
% 38.95/5.35 ![X0]: (multiplication(domain(X0),antidomain(X0))=zero)),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f41,f38])).
% 38.95/5.35 fof(f106,plain,(
% 38.95/5.35 coantidomain(one)=zero),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f29,f42])).
% 38.95/5.35 fof(f110,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(X0,multiplication(X1,coantidomain(multiplication(X0,X1))))=zero)),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f42,f27])).
% 38.95/5.35 fof(f132,plain,(
% 38.95/5.35 ![X0]: (codomain(coantidomain(X0))=coantidomain(codomain(X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f45,f45])).
% 38.95/5.35 fof(f133,plain,(
% 38.95/5.35 codomain(one)=coantidomain(zero)),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f106,f45])).
% 38.95/5.35 fof(f134,plain,(
% 38.95/5.35 ![X0]: (multiplication(coantidomain(X0),codomain(X0))=zero)),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f45,f42])).
% 38.95/5.35 fof(f141,plain,(
% 38.95/5.35 ![X0,X1,X2]: (multiplication(X0,addition(X1,X2))=addition(multiplication(X0,X2),multiplication(X0,X1)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f23,f30])).
% 38.95/5.35 fof(f145,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(antidomain(X0),addition(X0,X1))=addition(zero,multiplication(antidomain(X0),X1)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f38,f30])).
% 38.95/5.35 fof(f148,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(X0,addition(coantidomain(X0),X1))=addition(zero,multiplication(X0,X1)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f42,f30])).
% 38.95/5.35 fof(f165,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(antidomain(X0),addition(X0,X1))=multiplication(antidomain(X0),X1))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f59,f145])).
% 38.95/5.35 fof(f169,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(X0,addition(coantidomain(X0),X1))=multiplication(X0,X1))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f59,f148])).
% 38.95/5.35 fof(f182,plain,(
% 38.95/5.35 ![X0]: (addition(domain(antidomain(X0)),domain(X0))=one)),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f41,f49])).
% 38.95/5.35 fof(f183,plain,(
% 38.95/5.35 addition(domain(one),zero)=one),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f82,f49])).
% 38.95/5.35 fof(f184,plain,(
% 38.95/5.35 ![X0,X1]: (addition(domain(X0),addition(antidomain(X0),X1))=addition(one,X1))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f49,f24])).
% 38.95/5.35 fof(f185,plain,(
% 38.95/5.35 one=antidomain(zero)),
% 38.95/5.35 inference(backward_demodulation,[status(thm)],[f187,f103])).
% 38.95/5.35 fof(f187,plain,(
% 38.95/5.35 domain(one)=one),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f25,f183])).
% 38.95/5.35 fof(f195,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(addition(antidomain(X0),X1),X0)=addition(zero,multiplication(X1,X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f38,f31])).
% 38.95/5.35 fof(f198,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(addition(X0,X1),coantidomain(X0))=addition(zero,multiplication(X1,coantidomain(X0))))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f42,f31])).
% 38.95/5.35 fof(f204,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(addition(X0,one),X1)=addition(multiplication(X0,X1),X1))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f29,f31])).
% 38.95/5.35 fof(f214,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(addition(antidomain(X0),X1),X0)=multiplication(X1,X0))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f59,f195])).
% 38.95/5.35 fof(f216,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(addition(X0,X1),coantidomain(X0))=multiplication(X1,coantidomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f59,f198])).
% 38.95/5.35 fof(f236,plain,(
% 38.95/5.35 addition(codomain(one),zero)=one),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f106,f51])).
% 38.95/5.35 fof(f238,plain,(
% 38.95/5.35 one=coantidomain(zero)),
% 38.95/5.35 inference(backward_demodulation,[status(thm)],[f240,f133])).
% 38.95/5.35 fof(f240,plain,(
% 38.95/5.35 codomain(one)=one),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f25,f236])).
% 38.95/5.35 fof(f246,plain,(
% 38.95/5.35 ![X0]: (addition(antidomain(X0),antidomain(multiplication(one,domain(X0))))=antidomain(multiplication(one,domain(X0))))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f29,f53])).
% 38.95/5.35 fof(f247,plain,(
% 38.95/5.35 ![X0]: (addition(antidomain(zero),antidomain(multiplication(X0,domain(coantidomain(X0)))))=antidomain(multiplication(X0,domain(coantidomain(X0)))))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f42,f53])).
% 38.95/5.35 fof(f265,plain,(
% 38.95/5.35 ![X0]: (addition(antidomain(X0),antidomain(domain(X0)))=antidomain(multiplication(one,domain(X0))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f29,f246])).
% 38.95/5.35 fof(f266,plain,(
% 38.95/5.35 ![X0]: (addition(antidomain(X0),domain(antidomain(X0)))=antidomain(multiplication(one,domain(X0))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f102,f265])).
% 38.95/5.35 fof(f267,plain,(
% 38.95/5.35 ![X0]: (addition(antidomain(X0),domain(antidomain(X0)))=antidomain(domain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f29,f266])).
% 38.95/5.35 fof(f268,plain,(
% 38.95/5.35 ![X0]: (addition(antidomain(X0),domain(antidomain(X0)))=domain(antidomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f102,f267])).
% 38.95/5.35 fof(f269,plain,(
% 38.95/5.35 ![X0]: (addition(one,antidomain(multiplication(X0,domain(coantidomain(X0)))))=antidomain(multiplication(X0,domain(coantidomain(X0)))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f185,f247])).
% 38.95/5.35 fof(f328,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(addition(domain(X0),X1),antidomain(X0))=addition(zero,multiplication(X1,antidomain(X0))))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f104,f31])).
% 38.95/5.35 fof(f336,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(addition(domain(X0),X1),antidomain(X0))=multiplication(X1,antidomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f59,f328])).
% 38.95/5.35 fof(f342,plain,(
% 38.95/5.35 ![X0]: (addition(coantidomain(zero),coantidomain(multiplication(codomain(antidomain(X0)),X0)))=coantidomain(multiplication(codomain(antidomain(X0)),X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f38,f54])).
% 38.95/5.35 fof(f347,plain,(
% 38.95/5.35 ![X0]: (addition(coantidomain(X0),coantidomain(multiplication(codomain(X0),one)))=coantidomain(multiplication(codomain(X0),one)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f28,f54])).
% 38.95/5.35 fof(f355,plain,(
% 38.95/5.35 ![X0]: (addition(one,coantidomain(multiplication(codomain(antidomain(X0)),X0)))=coantidomain(multiplication(codomain(antidomain(X0)),X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f238,f342])).
% 38.95/5.35 fof(f373,plain,(
% 38.95/5.35 ![X0]: (addition(coantidomain(X0),coantidomain(codomain(X0)))=coantidomain(multiplication(codomain(X0),one)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f28,f347])).
% 38.95/5.35 fof(f374,plain,(
% 38.95/5.35 ![X0]: (addition(coantidomain(X0),codomain(coantidomain(X0)))=coantidomain(multiplication(codomain(X0),one)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f132,f373])).
% 38.95/5.35 fof(f375,plain,(
% 38.95/5.35 ![X0]: (addition(coantidomain(X0),codomain(coantidomain(X0)))=coantidomain(codomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f28,f374])).
% 38.95/5.35 fof(f376,plain,(
% 38.95/5.35 ![X0]: (addition(coantidomain(X0),codomain(coantidomain(X0)))=codomain(coantidomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f132,f375])).
% 38.95/5.35 fof(f417,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(coantidomain(X0),addition(X1,codomain(X0)))=addition(multiplication(coantidomain(X0),X1),zero))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f134,f30])).
% 38.95/5.35 fof(f426,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(coantidomain(X0),addition(X1,codomain(X0)))=multiplication(coantidomain(X0),X1))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f25,f417])).
% 38.95/5.35 fof(f433,plain,(
% 38.95/5.35 ![X0]: (addition(codomain(X0),one)=addition(codomain(X0),coantidomain(X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f51,f94])).
% 38.95/5.35 fof(f441,plain,(
% 38.95/5.35 ![X0,X1]: (addition(X0,addition(X1,X0))=addition(X0,X1))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f23,f94])).
% 38.95/5.35 fof(f449,plain,(
% 38.95/5.35 ![X0]: (addition(codomain(X0),one)=one)),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f51,f433])).
% 38.95/5.35 fof(f463,plain,(
% 38.95/5.35 ![X0]: (addition(one,codomain(X0))=one)),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f23,f449])).
% 38.95/5.35 fof(f478,plain,(
% 38.95/5.35 ![X0,X1]: (addition(X0,X1)=addition(X1,addition(addition(X0,X1),X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f26,f86])).
% 38.95/5.35 fof(f538,plain,(
% 38.95/5.35 ![X0,X1]: (addition(X0,X1)=addition(X1,addition(X0,addition(X1,X0))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f24,f478])).
% 38.95/5.35 fof(f539,plain,(
% 38.95/5.35 ![X0,X1]: (addition(X0,X1)=addition(X1,addition(X0,X1)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f441,f538])).
% 38.95/5.35 fof(f750,plain,(
% 38.95/5.35 ![X0]: (addition(coantidomain(X0),one)=addition(coantidomain(X0),codomain(X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f51,f441])).
% 38.95/5.35 fof(f752,plain,(
% 38.95/5.35 ![X0]: (addition(antidomain(X0),one)=addition(antidomain(X0),domain(X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f49,f441])).
% 38.95/5.35 fof(f833,plain,(
% 38.95/5.35 ![X0]: (addition(codomain(X0),coantidomain(X0))=addition(coantidomain(X0),one))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f51,f539])).
% 38.95/5.35 fof(f835,plain,(
% 38.95/5.35 ![X0]: (addition(domain(X0),antidomain(X0))=addition(antidomain(X0),one))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f49,f539])).
% 38.95/5.35 fof(f872,plain,(
% 38.95/5.35 ![X0]: (one=addition(coantidomain(X0),codomain(X0)))),
% 38.95/5.35 inference(backward_demodulation,[status(thm)],[f873,f750])).
% 38.95/5.35 fof(f873,plain,(
% 38.95/5.35 ![X0]: (one=addition(coantidomain(X0),one))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f51,f833])).
% 38.95/5.35 fof(f876,plain,(
% 38.95/5.35 ![X0]: (one=addition(antidomain(X0),domain(X0)))),
% 38.95/5.35 inference(backward_demodulation,[status(thm)],[f877,f752])).
% 38.95/5.35 fof(f877,plain,(
% 38.95/5.35 ![X0]: (one=addition(antidomain(X0),one))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f49,f835])).
% 38.95/5.35 fof(f914,plain,(
% 38.95/5.35 ![X0]: (one=addition(one,coantidomain(X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f23,f873])).
% 38.95/5.35 fof(f931,plain,(
% 38.95/5.35 ![X0]: (one=coantidomain(multiplication(codomain(antidomain(X0)),X0)))),
% 38.95/5.35 inference(backward_demodulation,[status(thm)],[f914,f355])).
% 38.95/5.35 fof(f996,plain,(
% 38.95/5.35 ![X0]: (one=addition(one,antidomain(X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f23,f877])).
% 38.95/5.35 fof(f1017,plain,(
% 38.95/5.35 ![X0]: (one=antidomain(multiplication(X0,domain(coantidomain(X0)))))),
% 38.95/5.35 inference(backward_demodulation,[status(thm)],[f996,f269])).
% 38.95/5.35 fof(f1360,plain,(
% 38.95/5.35 ![X0]: (multiplication(antidomain(coantidomain(X0)),one)=multiplication(antidomain(coantidomain(X0)),codomain(X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f872,f165])).
% 38.95/5.35 fof(f1363,plain,(
% 38.95/5.35 ![X0]: (multiplication(antidomain(antidomain(X0)),one)=multiplication(antidomain(antidomain(X0)),domain(X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f876,f165])).
% 38.95/5.35 fof(f1368,plain,(
% 38.95/5.35 ![X0]: (multiplication(antidomain(domain(antidomain(X0))),one)=multiplication(antidomain(domain(antidomain(X0))),domain(X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f182,f165])).
% 38.95/5.35 fof(f1370,plain,(
% 38.95/5.35 ![X0]: (multiplication(antidomain(domain(X0)),one)=multiplication(antidomain(domain(X0)),antidomain(X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f49,f165])).
% 38.95/5.35 fof(f1413,plain,(
% 38.95/5.35 ![X0]: (antidomain(coantidomain(X0))=multiplication(antidomain(coantidomain(X0)),codomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f28,f1360])).
% 38.95/5.35 fof(f1414,plain,(
% 38.95/5.35 ![X0]: (antidomain(antidomain(X0))=multiplication(antidomain(antidomain(X0)),domain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f28,f1363])).
% 38.95/5.35 fof(f1415,plain,(
% 38.95/5.35 ![X0]: (domain(X0)=multiplication(antidomain(antidomain(X0)),domain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f41,f1414])).
% 38.95/5.35 fof(f1416,plain,(
% 38.95/5.35 ![X0]: (domain(X0)=multiplication(domain(X0),domain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f41,f1415])).
% 38.95/5.35 fof(f1419,plain,(
% 38.95/5.35 ![X0]: (antidomain(domain(antidomain(X0)))=multiplication(antidomain(domain(antidomain(X0))),domain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f28,f1368])).
% 38.95/5.35 fof(f1420,plain,(
% 38.95/5.35 ![X0]: (domain(antidomain(antidomain(X0)))=multiplication(antidomain(domain(antidomain(X0))),domain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f102,f1419])).
% 38.95/5.35 fof(f1421,plain,(
% 38.95/5.35 ![X0]: (domain(domain(X0))=multiplication(antidomain(domain(antidomain(X0))),domain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f41,f1420])).
% 38.95/5.35 fof(f1422,plain,(
% 38.95/5.35 ![X0]: (domain(domain(X0))=multiplication(domain(antidomain(antidomain(X0))),domain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f102,f1421])).
% 38.95/5.35 fof(f1423,plain,(
% 38.95/5.35 ![X0]: (domain(domain(X0))=multiplication(domain(domain(X0)),domain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f41,f1422])).
% 38.95/5.35 fof(f1424,plain,(
% 38.95/5.35 ![X0]: (antidomain(domain(X0))=multiplication(antidomain(domain(X0)),antidomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f28,f1370])).
% 38.95/5.35 fof(f1425,plain,(
% 38.95/5.35 ![X0]: (domain(antidomain(X0))=multiplication(antidomain(domain(X0)),antidomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f102,f1424])).
% 38.95/5.35 fof(f1426,plain,(
% 38.95/5.35 ![X0]: (domain(antidomain(X0))=multiplication(domain(antidomain(X0)),antidomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f102,f1425])).
% 38.95/5.35 fof(f1450,plain,(
% 38.95/5.35 ![X0]: (addition(antidomain(domain(X0)),antidomain(multiplication(domain(X0),domain(domain(X0)))))=antidomain(multiplication(domain(X0),domain(domain(X0)))))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f1416,f53])).
% 38.95/5.35 fof(f1468,plain,(
% 38.95/5.35 ![X0]: (addition(domain(antidomain(X0)),antidomain(multiplication(domain(X0),domain(domain(X0)))))=antidomain(multiplication(domain(X0),domain(domain(X0)))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f102,f1450])).
% 38.95/5.35 fof(f1556,plain,(
% 38.95/5.35 ![X0]: (multiplication(codomain(antidomain(X0)),multiplication(X0,one))=zero)),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f931,f110])).
% 38.95/5.35 fof(f1577,plain,(
% 38.95/5.35 ![X0]: (multiplication(codomain(antidomain(X0)),X0)=zero)),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f28,f1556])).
% 38.95/5.35 fof(f1594,plain,(
% 38.95/5.35 ![X0]: (multiplication(X0,one)=multiplication(X0,codomain(X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f872,f169])).
% 38.95/5.35 fof(f1629,plain,(
% 38.95/5.35 ![X0]: (X0=multiplication(X0,codomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f28,f1594])).
% 38.95/5.35 fof(f1663,plain,(
% 38.95/5.35 ![X0]: (addition(coantidomain(X0),coantidomain(multiplication(codomain(X0),codomain(X0))))=coantidomain(multiplication(codomain(X0),codomain(X0))))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f1629,f54])).
% 38.95/5.35 fof(f1694,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(addition(X0,codomain(antidomain(X1))),X1)=addition(multiplication(X0,X1),zero))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f1577,f31])).
% 38.95/5.35 fof(f1719,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(addition(X0,codomain(antidomain(X1))),X1)=multiplication(X0,X1))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f25,f1694])).
% 38.95/5.35 fof(f2008,plain,(
% 38.95/5.35 ![X0]: (multiplication(codomain(one),multiplication(X0,domain(coantidomain(X0))))=zero)),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f1017,f1577])).
% 38.95/5.35 fof(f2030,plain,(
% 38.95/5.35 ![X0]: (multiplication(one,multiplication(X0,domain(coantidomain(X0))))=zero)),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f240,f2008])).
% 38.95/5.35 fof(f2033,plain,(
% 38.95/5.35 ![X0]: (multiplication(X0,domain(coantidomain(X0)))=zero)),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f29,f2030])).
% 38.95/5.35 fof(f2062,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(X0,addition(domain(coantidomain(X0)),X1))=addition(multiplication(X0,X1),zero))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f2033,f141])).
% 38.95/5.35 fof(f2089,plain,(
% 38.95/5.35 ![X0,X1]: (multiplication(X0,addition(domain(coantidomain(X0)),X1))=multiplication(X0,X1))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f25,f2062])).
% 38.95/5.35 fof(f3640,plain,(
% 38.95/5.35 ![X0]: (multiplication(one,X0)=multiplication(domain(X0),X0))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f876,f214])).
% 38.95/5.35 fof(f3681,plain,(
% 38.95/5.35 ![X0]: (domain(domain(X0))=domain(X0))),
% 38.95/5.35 inference(backward_demodulation,[status(thm)],[f3684,f1423])).
% 38.95/5.35 fof(f3682,plain,(
% 38.95/5.35 ![X0]: (domain(antidomain(X0))=antidomain(X0))),
% 38.95/5.35 inference(backward_demodulation,[status(thm)],[f3684,f1426])).
% 38.95/5.35 fof(f3684,plain,(
% 38.95/5.35 ![X0]: (X0=multiplication(domain(X0),X0))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f29,f3640])).
% 38.95/5.35 fof(f3716,plain,(
% 38.95/5.35 ![X0]: (addition(domain(antidomain(X0)),antidomain(multiplication(domain(X0),domain(domain(X0)))))=antidomain(multiplication(domain(X0),domain(X0))))),
% 38.95/5.35 inference(backward_demodulation,[status(thm)],[f3681,f1468])).
% 38.95/5.35 fof(f3764,plain,(
% 38.95/5.35 ![X0]: (addition(antidomain(X0),antidomain(multiplication(domain(X0),domain(domain(X0)))))=antidomain(multiplication(domain(X0),domain(X0))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f3682,f3716])).
% 38.95/5.35 fof(f3765,plain,(
% 38.95/5.35 ![X0]: (addition(antidomain(X0),antidomain(multiplication(domain(X0),domain(X0))))=antidomain(multiplication(domain(X0),domain(X0))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f3681,f3764])).
% 38.95/5.35 fof(f3766,plain,(
% 38.95/5.35 ![X0]: (addition(antidomain(X0),antidomain(domain(X0)))=antidomain(multiplication(domain(X0),domain(X0))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f1416,f3765])).
% 38.95/5.35 fof(f3767,plain,(
% 38.95/5.35 ![X0]: (addition(antidomain(X0),domain(antidomain(X0)))=antidomain(multiplication(domain(X0),domain(X0))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f102,f3766])).
% 38.95/5.35 fof(f3768,plain,(
% 38.95/5.35 ![X0]: (domain(antidomain(X0))=antidomain(multiplication(domain(X0),domain(X0))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f268,f3767])).
% 38.95/5.35 fof(f3769,plain,(
% 38.95/5.35 ![X0]: (antidomain(X0)=antidomain(multiplication(domain(X0),domain(X0))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f3682,f3768])).
% 38.95/5.35 fof(f3770,plain,(
% 38.95/5.35 ![X0]: (antidomain(X0)=antidomain(domain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f1416,f3769])).
% 38.95/5.35 fof(f5466,plain,(
% 38.95/5.35 ![X0]: (multiplication(one,coantidomain(coantidomain(X0)))=multiplication(codomain(X0),coantidomain(coantidomain(X0))))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f872,f216])).
% 38.95/5.35 fof(f5474,plain,(
% 38.95/5.35 ![X0]: (multiplication(one,coantidomain(codomain(X0)))=multiplication(coantidomain(X0),coantidomain(codomain(X0))))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f51,f216])).
% 38.95/5.35 fof(f5539,plain,(
% 38.95/5.35 ![X0]: (coantidomain(coantidomain(X0))=multiplication(codomain(X0),coantidomain(coantidomain(X0))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f29,f5466])).
% 38.95/5.35 fof(f5540,plain,(
% 38.95/5.35 ![X0]: (codomain(X0)=multiplication(codomain(X0),coantidomain(coantidomain(X0))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f45,f5539])).
% 38.95/5.35 fof(f5541,plain,(
% 38.95/5.35 ![X0]: (addition(coantidomain(X0),coantidomain(multiplication(codomain(X0),codomain(X0))))=coantidomain(codomain(X0)))),
% 38.95/5.35 inference(backward_demodulation,[status(thm)],[f5542,f1663])).
% 38.95/5.35 fof(f5542,plain,(
% 38.95/5.35 ![X0]: (codomain(X0)=multiplication(codomain(X0),codomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f45,f5540])).
% 38.95/5.35 fof(f5602,plain,(
% 38.95/5.35 ![X0]: (coantidomain(codomain(X0))=multiplication(coantidomain(X0),coantidomain(codomain(X0))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f29,f5474])).
% 38.95/5.35 fof(f5603,plain,(
% 38.95/5.35 ![X0]: (codomain(coantidomain(X0))=multiplication(coantidomain(X0),coantidomain(codomain(X0))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f132,f5602])).
% 38.95/5.35 fof(f5604,plain,(
% 38.95/5.35 ![X0]: (codomain(coantidomain(X0))=multiplication(coantidomain(X0),codomain(coantidomain(X0))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f132,f5603])).
% 38.95/5.35 fof(f5650,plain,(
% 38.95/5.35 ![X0]: (codomain(coantidomain(X0))=coantidomain(X0))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f1629,f5604])).
% 38.95/5.35 fof(f5706,plain,(
% 38.95/5.35 ![X0]: (addition(coantidomain(X0),coantidomain(codomain(X0)))=coantidomain(codomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f5542,f5541])).
% 38.95/5.35 fof(f5707,plain,(
% 38.95/5.35 ![X0]: (addition(coantidomain(X0),codomain(coantidomain(X0)))=coantidomain(codomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f132,f5706])).
% 38.95/5.35 fof(f5708,plain,(
% 38.95/5.35 ![X0]: (codomain(coantidomain(X0))=coantidomain(codomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f376,f5707])).
% 38.95/5.35 fof(f5709,plain,(
% 38.95/5.35 ![X0]: (coantidomain(X0)=coantidomain(codomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f5650,f5708])).
% 38.95/5.35 fof(f24913,plain,(
% 38.95/5.35 ![X0]: (multiplication(addition(antidomain(coantidomain(X0)),one),codomain(X0))=addition(antidomain(coantidomain(X0)),codomain(X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f1413,f204])).
% 38.95/5.35 fof(f24997,plain,(
% 38.95/5.35 ![X0]: (multiplication(one,codomain(X0))=addition(antidomain(coantidomain(X0)),codomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f877,f24913])).
% 38.95/5.35 fof(f24998,plain,(
% 38.95/5.35 ![X0]: (codomain(X0)=addition(antidomain(coantidomain(X0)),codomain(X0)))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f29,f24997])).
% 38.95/5.35 fof(f25038,plain,(
% 38.95/5.35 ![X0]: (addition(domain(coantidomain(X0)),codomain(X0))=addition(one,codomain(X0)))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f24998,f184])).
% 38.95/5.35 fof(f25112,plain,(
% 38.95/5.35 ![X0]: (addition(domain(coantidomain(X0)),codomain(X0))=one)),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f463,f25038])).
% 38.95/5.35 fof(f26507,plain,(
% 38.95/5.35 ![X0]: (multiplication(one,antidomain(coantidomain(X0)))=multiplication(codomain(X0),antidomain(coantidomain(X0))))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f25112,f336])).
% 38.95/5.35 fof(f26509,plain,(
% 38.95/5.35 ![X0]: (multiplication(coantidomain(X0),one)=multiplication(coantidomain(X0),domain(coantidomain(X0))))),
% 38.95/5.35 inference(paramodulation,[status(thm)],[f25112,f426])).
% 38.95/5.35 fof(f26573,plain,(
% 38.95/5.35 ![X0]: (antidomain(coantidomain(X0))=multiplication(codomain(X0),antidomain(coantidomain(X0))))),
% 38.95/5.35 inference(forward_demodulation,[status(thm)],[f29,f26507])).
% 38.95/5.35 fof(f26578,plain,(
% 38.95/5.35 ![X0]: (coantidomain(X0)=multiplication(coantidomain(X0),domain(coantidomain(X0))))),
% 38.95/5.40 inference(forward_demodulation,[status(thm)],[f28,f26509])).
% 38.95/5.40 fof(f30760,plain,(
% 38.95/5.40 ![X0]: (multiplication(one,X0)=multiplication(coantidomain(antidomain(X0)),X0))),
% 38.95/5.40 inference(paramodulation,[status(thm)],[f872,f1719])).
% 38.95/5.40 fof(f30848,plain,(
% 38.95/5.40 ![X0]: (X0=multiplication(coantidomain(antidomain(X0)),X0))),
% 38.95/5.40 inference(forward_demodulation,[status(thm)],[f29,f30760])).
% 38.95/5.40 fof(f30929,plain,(
% 38.95/5.40 ![X0]: (domain(X0)=multiplication(coantidomain(antidomain(X0)),domain(X0)))),
% 38.95/5.40 inference(paramodulation,[status(thm)],[f3770,f30848])).
% 38.95/5.40 fof(f33891,plain,(
% 38.95/5.40 ![X0]: (multiplication(X0,one)=multiplication(X0,antidomain(coantidomain(X0))))),
% 38.95/5.40 inference(paramodulation,[status(thm)],[f49,f2089])).
% 38.95/5.40 fof(f34000,plain,(
% 38.95/5.40 ![X0]: (X0=multiplication(X0,antidomain(coantidomain(X0))))),
% 38.95/5.40 inference(forward_demodulation,[status(thm)],[f28,f33891])).
% 38.95/5.40 fof(f35400,plain,(
% 38.95/5.40 ![X0]: (codomain(X0)=multiplication(codomain(X0),antidomain(coantidomain(X0))))),
% 38.95/5.40 inference(paramodulation,[status(thm)],[f5709,f34000])).
% 38.95/5.40 fof(f35472,plain,(
% 38.95/5.40 ![X0]: (antidomain(coantidomain(X0))=codomain(X0))),
% 38.95/5.40 inference(backward_demodulation,[status(thm)],[f35400,f26573])).
% 38.95/5.40 fof(f35990,plain,(
% 38.95/5.40 ![X0]: (domain(coantidomain(X0))=multiplication(coantidomain(codomain(X0)),domain(coantidomain(X0))))),
% 38.95/5.40 inference(paramodulation,[status(thm)],[f35472,f30929])).
% 38.95/5.40 fof(f36039,plain,(
% 38.95/5.40 ![X0]: (domain(coantidomain(X0))=multiplication(coantidomain(X0),domain(coantidomain(X0))))),
% 38.95/5.40 inference(forward_demodulation,[status(thm)],[f5709,f35990])).
% 38.95/5.40 fof(f36041,plain,(
% 38.95/5.40 ~coantidomain(sK0_skl)=coantidomain(sK0_skl)),
% 38.95/5.40 inference(backward_demodulation,[status(thm)],[f36176,f48])).
% 38.95/5.40 fof(f36176,plain,(
% 38.95/5.40 ![X0]: (domain(coantidomain(X0))=coantidomain(X0))),
% 38.95/5.40 inference(forward_demodulation,[status(thm)],[f26578,f36039])).
% 38.95/5.40 fof(f36274,plain,(
% 38.95/5.40 $false),
% 38.95/5.40 inference(trivial_equality_resolution,[status(thm)],[f36041])).
% 38.95/5.40 % SZS output end CNFRefutation for theBenchmark.p
% 5.24/5.42 % Elapsed time: 5.054058 seconds
% 5.24/5.42 % CPU time: 39.743977 seconds
% 5.24/5.42 % Total memory used: 385.254 MB
% 5.24/5.42 % Net memory used: 374.717 MB
%------------------------------------------------------------------------------