%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KLE011+3 : 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 : n008.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:10 PM UTC 2026
% Result : Theorem 107.26s 13.98s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KLE011+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n008.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:38:53 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 107.26/13.98 % Refutation found
% 107.26/13.98 % SZS status Theorem for theBenchmark: Theorem is valid
% 107.26/13.98 % SZS output start CNFRefutation for theBenchmark
% 107.26/13.98 fof(f1,axiom,(
% 107.26/13.98 (! [A,B] : addition(A,B) = addition(B,A) )),
% 107.26/13.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 107.26/13.98 fof(f3,axiom,(
% 107.26/13.98 (! [A] : addition(A,zero) = A )),
% 107.26/13.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 107.26/13.98 fof(f7,axiom,(
% 107.26/13.98 (! [A] : multiplication(one,A) = A )),
% 107.26/13.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 107.26/13.98 fof(f11,axiom,(
% 107.26/13.98 (! [A] : multiplication(zero,A) = zero )),
% 107.26/13.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 107.26/13.98 fof(f13,axiom,(
% 107.26/13.98 (! [X0] :( test(X0)<=> (? [X1] : complement(X1,X0) )) )),
% 107.26/13.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 107.26/13.98 fof(f14,axiom,(
% 107.26/13.98 (! [X0,X1] :( complement(X1,X0)<=> ( multiplication(X0,X1) = zero& multiplication(X1,X0) = zero& addition(X0,X1) = one ) ) )),
% 107.26/13.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 107.26/13.98 fof(f15,axiom,(
% 107.26/13.98 (! [X0,X1] :( test(X0)=> ( c(X0) = X1<=> complement(X0,X1) ) ) )),
% 107.26/13.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 107.26/13.98 fof(f16,axiom,(
% 107.26/13.98 (! [X0] :( ~ test(X0)=> c(X0) = zero ) )),
% 107.26/13.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 107.26/13.98 fof(f17,axiom,(
% 107.26/13.98 (! [X0,X1] :( ( test(X0)& test(X1) )=> c(addition(X0,X1)) = multiplication(c(X0),c(X1)) ) )),
% 107.26/13.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 107.26/13.98 fof(f18,axiom,(
% 107.26/13.98 (! [X0,X1] :( ( test(X0)& test(X1) )=> c(multiplication(X0,X1)) = addition(c(X0),c(X1)) ) )),
% 107.26/13.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 107.26/13.98 fof(f19,conjecture,(
% 107.26/13.98 (! [X0,X1] :( ( test(X1)& test(X0) )=> one = addition(addition(multiplication(addition(X1,c(X1)),X0),multiplication(addition(X0,c(X0)),X1)),multiplication(c(X0),c(X1))) ) )),
% 107.26/13.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 107.26/13.98 fof(f20,negated_conjecture,(
% 107.26/13.98 ~((! [X0,X1] :( ( test(X1)& test(X0) )=> one = addition(addition(multiplication(addition(X1,c(X1)),X0),multiplication(addition(X0,c(X0)),X1)),multiplication(c(X0),c(X1))) ) ))),
% 107.26/13.98 inference(negated_conjecture,[status(cth)],[f19])).
% 107.26/13.98 fof(f21,plain,(
% 107.26/13.98 ![X0,X1]: (addition(X0,X1)=addition(X1,X0))),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f1])).
% 107.26/13.98 fof(f23,plain,(
% 107.26/13.98 ![X0]: (addition(X0,zero)=X0)),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f3])).
% 107.26/13.98 fof(f27,plain,(
% 107.26/13.98 ![X0]: (multiplication(one,X0)=X0)),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f7])).
% 107.26/13.98 fof(f31,plain,(
% 107.26/13.98 ![X0]: (multiplication(zero,X0)=zero)),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f11])).
% 107.26/13.98 fof(f36,plain,(
% 107.26/13.98 ![X0]: ((~test(X0)|(?[X1]: complement(X1,X0)))&(test(X0)|(![X1]: ~complement(X1,X0))))),
% 107.26/13.98 inference(NNF_transformation,[status(thm)],[f13])).
% 107.26/13.98 fof(f37,plain,(
% 107.26/13.98 (![X0]: (~test(X0)|(?[X1]: complement(X1,X0))))&(![X0]: (test(X0)|(![X1]: ~complement(X1,X0))))),
% 107.26/13.98 inference(miniscoping,[status(thm)],[f36])).
% 107.26/13.98 fof(f38,plain,(
% 107.26/13.98 (![X0]: (~test(X0)|complement(sK0_skl(X0),X0)))&(![X0]: (test(X0)|(![X1]: ~complement(X1,X0))))),
% 107.26/13.98 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X1,sK0_skl(X0))],[f37])).
% 107.26/13.98 fof(f40,plain,(
% 107.26/13.98 ![X0,X1]: (test(X0)|~complement(X1,X0))),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f38])).
% 107.26/13.98 fof(f41,plain,(
% 107.26/13.98 ![X0,X1]: ((~complement(X1,X0)|((multiplication(X0,X1)=zero&multiplication(X1,X0)=zero)&addition(X0,X1)=one))&(complement(X1,X0)|((~multiplication(X0,X1)=zero|~multiplication(X1,X0)=zero)|~addition(X0,X1)=one)))),
% 107.26/13.98 inference(NNF_transformation,[status(thm)],[f14])).
% 107.26/13.98 fof(f42,plain,(
% 107.26/13.98 (![X0,X1]: (~complement(X1,X0)|((multiplication(X0,X1)=zero&multiplication(X1,X0)=zero)&addition(X0,X1)=one)))&(![X0,X1]: (complement(X1,X0)|((~multiplication(X0,X1)=zero|~multiplication(X1,X0)=zero)|~addition(X0,X1)=one)))),
% 107.26/13.98 inference(miniscoping,[status(thm)],[f41])).
% 107.26/13.98 fof(f43,plain,(
% 107.26/13.98 ![X0,X1]: (~complement(X0,X1)|multiplication(X1,X0)=zero)),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f42])).
% 107.26/13.98 fof(f44,plain,(
% 107.26/13.98 ![X0,X1]: (~complement(X0,X1)|multiplication(X0,X1)=zero)),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f42])).
% 107.26/13.98 fof(f45,plain,(
% 107.26/13.98 ![X0,X1]: (~complement(X0,X1)|addition(X1,X0)=one)),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f42])).
% 107.26/13.98 fof(f46,plain,(
% 107.26/13.98 ![X0,X1]: (complement(X0,X1)|~multiplication(X1,X0)=zero|~multiplication(X0,X1)=zero|~addition(X1,X0)=one)),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f42])).
% 107.26/13.98 fof(f47,plain,(
% 107.26/13.98 ![X0,X1]: (~test(X0)|(c(X0)=X1<=>complement(X0,X1)))),
% 107.26/13.98 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 107.26/13.98 fof(f48,plain,(
% 107.26/13.98 ![X0,X1]: (~test(X0)|((~c(X0)=X1|complement(X0,X1))&(c(X0)=X1|~complement(X0,X1))))),
% 107.26/13.98 inference(NNF_transformation,[status(thm)],[f47])).
% 107.26/13.98 fof(f49,plain,(
% 107.26/13.98 ![X0]: (~test(X0)|((![X1]: (~c(X0)=X1|complement(X0,X1)))&(![X1]: (c(X0)=X1|~complement(X0,X1)))))),
% 107.26/13.98 inference(miniscoping,[status(thm)],[f48])).
% 107.26/13.98 fof(f50,plain,(
% 107.26/13.98 ![X0,X1]: (~test(X0)|~c(X0)=X1|complement(X0,X1))),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f49])).
% 107.26/13.98 fof(f51,plain,(
% 107.26/13.98 ![X0,X1]: (~test(X0)|c(X0)=X1|~complement(X0,X1))),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f49])).
% 107.26/13.98 fof(f52,plain,(
% 107.26/13.98 ![X0]: (test(X0)|c(X0)=zero)),
% 107.26/13.98 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 107.26/13.98 fof(f53,plain,(
% 107.26/13.98 ![X0]: (test(X0)|c(X0)=zero)),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f52])).
% 107.26/13.98 fof(f54,plain,(
% 107.26/13.98 ![X0,X1]: ((~test(X0)|~test(X1))|c(addition(X0,X1))=multiplication(c(X0),c(X1)))),
% 107.26/13.98 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 107.26/13.98 fof(f55,plain,(
% 107.26/13.98 ![X0,X1]: (~test(X0)|~test(X1)|c(addition(X0,X1))=multiplication(c(X0),c(X1)))),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f54])).
% 107.26/13.98 fof(f56,plain,(
% 107.26/13.98 ![X0,X1]: ((~test(X0)|~test(X1))|c(multiplication(X0,X1))=addition(c(X0),c(X1)))),
% 107.26/13.98 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 107.26/13.98 fof(f57,plain,(
% 107.26/13.98 ![X0,X1]: (~test(X0)|~test(X1)|c(multiplication(X0,X1))=addition(c(X0),c(X1)))),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f56])).
% 107.26/13.98 fof(f58,plain,(
% 107.26/13.98 (?[X0,X1]: ((test(X1)&test(X0))&~one=addition(addition(multiplication(addition(X1,c(X1)),X0),multiplication(addition(X0,c(X0)),X1)),multiplication(c(X0),c(X1)))))),
% 107.26/13.98 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 107.26/13.98 fof(f59,plain,(
% 107.26/13.98 ((test(sK2_skl)&test(sK1_skl))&~one=addition(addition(multiplication(addition(sK2_skl,c(sK2_skl)),sK1_skl),multiplication(addition(sK1_skl,c(sK1_skl)),sK2_skl)),multiplication(c(sK1_skl),c(sK2_skl))))),
% 107.26/13.98 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(X0,sK1_skl),skolemize(X1,sK2_skl)],[f58])).
% 107.26/13.98 fof(f60,plain,(
% 107.26/13.98 test(sK2_skl)),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f59])).
% 107.26/13.98 fof(f61,plain,(
% 107.26/13.98 test(sK1_skl)),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f59])).
% 107.26/13.98 fof(f62,plain,(
% 107.26/13.98 ~one=addition(addition(multiplication(addition(sK2_skl,c(sK2_skl)),sK1_skl),multiplication(addition(sK1_skl,c(sK1_skl)),sK2_skl)),multiplication(c(sK1_skl),c(sK2_skl)))),
% 107.26/13.98 inference(cnf_transformation,[status(thm)],[f59])).
% 107.26/13.98 fof(f63,plain,(
% 107.26/13.98 ![X0]: (~test(X0)|complement(X0,c(X0)))),
% 107.26/13.98 inference(destructive_equality_resolution,[status(thm)],[f50])).
% 107.26/13.98 fof(f68,plain,(
% 107.26/13.98 ~one=addition(multiplication(c(sK1_skl),c(sK2_skl)),addition(multiplication(addition(sK2_skl,c(sK2_skl)),sK1_skl),multiplication(addition(sK1_skl,c(sK1_skl)),sK2_skl)))),
% 107.26/13.98 inference(paramodulation,[status(thm)],[f21,f62])).
% 107.26/13.98 fof(f186,plain,(
% 107.26/13.98 ![X0]: (addition(zero,X0)=X0)),
% 107.26/13.98 inference(paramodulation,[status(thm)],[f21,f23])).
% 107.26/13.98 fof(f326,plain,(
% 107.26/13.98 complement(one,zero)|~multiplication(zero,one)=zero|~multiplication(one,zero)=zero),
% 107.26/13.98 inference(resolution,[status(thm)],[f46,f186])).
% 107.26/13.98 fof(f327,plain,(
% 107.26/13.98 complement(zero,one)|~multiplication(one,zero)=zero|~multiplication(zero,one)=zero),
% 107.26/13.98 inference(resolution,[status(thm)],[f46,f23])).
% 107.26/13.98 fof(f339,plain,(
% 107.26/13.98 complement(one,zero)|~zero=zero|~multiplication(one,zero)=zero),
% 107.26/13.98 inference(forward_demodulation,[status(thm)],[f31,f326])).
% 107.26/13.98 fof(f340,plain,(
% 107.26/13.98 complement(one,zero)|~zero=zero|~zero=zero),
% 107.26/13.98 inference(forward_demodulation,[status(thm)],[f27,f339])).
% 107.26/13.98 fof(f341,plain,(
% 107.26/13.98 complement(one,zero)|~zero=zero),
% 107.26/13.98 inference(duplicate_literals_removal,[status(thm)],[f340])).
% 107.26/13.98 fof(f342,plain,(
% 107.26/13.98 complement(one,zero)),
% 107.26/13.98 inference(trivial_equality_resolution,[status(thm)],[f341])).
% 107.26/13.98 fof(f343,plain,(
% 107.26/13.98 complement(zero,one)|~zero=zero|~multiplication(zero,one)=zero),
% 107.26/13.98 inference(forward_demodulation,[status(thm)],[f27,f327])).
% 107.26/13.98 fof(f344,plain,(
% 107.26/13.98 complement(zero,one)|~zero=zero|~zero=zero),
% 107.26/13.98 inference(forward_demodulation,[status(thm)],[f31,f343])).
% 107.26/13.98 fof(f345,plain,(
% 107.26/13.98 complement(zero,one)|~zero=zero),
% 107.26/13.98 inference(duplicate_literals_removal,[status(thm)],[f344])).
% 107.26/13.98 fof(f346,plain,(
% 107.26/13.98 complement(zero,one)),
% 107.26/13.98 inference(trivial_equality_resolution,[status(thm)],[f345])).
% 107.26/13.98 fof(f366,plain,(
% 107.26/13.98 ![X0]: (~test(X0)|c(addition(X0,sK1_skl))=multiplication(c(X0),c(sK1_skl)))),
% 107.26/13.98 inference(resolution,[status(thm)],[f55,f61])).
% 107.26/13.98 fof(f367,plain,(
% 107.26/13.98 ![X0]: (~test(X0)|c(addition(X0,sK2_skl))=multiplication(c(X0),c(sK2_skl)))),
% 107.26/13.98 inference(resolution,[status(thm)],[f55,f60])).
% 107.26/13.98 fof(f371,plain,(
% 107.26/13.98 test(zero)),
% 107.26/13.98 inference(resolution,[status(thm)],[f342,f40])).
% 107.26/13.98 fof(f396,plain,(
% 107.26/13.98 complement(sK1_skl,c(sK1_skl))),
% 107.26/13.98 inference(resolution,[status(thm)],[f63,f61])).
% 107.26/13.98 fof(f397,plain,(
% 107.26/13.98 complement(sK2_skl,c(sK2_skl))),
% 107.26/13.98 inference(resolution,[status(thm)],[f63,f60])).
% 107.26/13.98 fof(f398,plain,(
% 107.26/13.98 ![X0]: (complement(X0,c(X0))|c(X0)=zero)),
% 107.26/13.98 inference(resolution,[status(thm)],[f63,f53])).
% 107.26/13.98 fof(f399,plain,(
% 107.26/13.98 ~test(zero)|c(zero)=one),
% 107.26/13.98 inference(resolution,[status(thm)],[f51,f346])).
% 107.26/13.98 fof(f404,plain,(
% 107.26/13.98 c(zero)=one),
% 107.26/13.98 inference(forward_subsumption_resolution,[status(thm)],[f399,f371])).
% 107.26/13.98 fof(f414,plain,(
% 107.26/13.98 multiplication(sK1_skl,c(sK1_skl))=zero),
% 107.26/13.98 inference(resolution,[status(thm)],[f396,f44])).
% 107.26/13.98 fof(f415,plain,(
% 107.26/13.98 multiplication(c(sK1_skl),sK1_skl)=zero),
% 107.26/13.98 inference(resolution,[status(thm)],[f396,f43])).
% 107.26/13.98 fof(f416,plain,(
% 107.26/13.98 test(c(sK1_skl))),
% 107.26/13.98 inference(resolution,[status(thm)],[f396,f40])).
% 107.26/13.98 fof(f417,plain,(
% 107.26/13.98 addition(c(sK1_skl),sK1_skl)=one),
% 107.26/13.98 inference(resolution,[status(thm)],[f396,f45])).
% 107.26/13.98 fof(f418,plain,(
% 107.26/13.98 ![X0]: (~test(X0)|c(multiplication(X0,c(sK1_skl)))=addition(c(X0),c(c(sK1_skl))))),
% 107.26/13.98 inference(resolution,[status(thm)],[f416,f57])).
% 107.26/13.98 fof(f423,plain,(
% 107.26/13.98 multiplication(sK2_skl,c(sK2_skl))=zero),
% 107.26/13.98 inference(resolution,[status(thm)],[f397,f44])).
% 107.26/13.98 fof(f424,plain,(
% 107.26/13.98 multiplication(c(sK2_skl),sK2_skl)=zero),
% 107.26/13.98 inference(resolution,[status(thm)],[f397,f43])).
% 107.26/13.98 fof(f425,plain,(
% 107.26/13.98 test(c(sK2_skl))),
% 107.26/13.98 inference(resolution,[status(thm)],[f397,f40])).
% 107.26/13.98 fof(f426,plain,(
% 107.26/13.98 addition(c(sK2_skl),sK2_skl)=one),
% 107.26/13.98 inference(resolution,[status(thm)],[f397,f45])).
% 107.26/13.98 fof(f965,plain,(
% 107.26/13.98 addition(sK1_skl,c(sK1_skl))=one),
% 107.26/13.98 inference(paramodulation,[status(thm)],[f21,f417])).
% 107.26/13.98 fof(f1112,plain,(
% 107.26/13.98 addition(sK2_skl,c(sK2_skl))=one),
% 107.26/13.98 inference(paramodulation,[status(thm)],[f21,f426])).
% 107.26/13.98 fof(f1566,plain,(
% 107.26/13.98 ~one=addition(multiplication(c(sK1_skl),c(sK2_skl)),addition(multiplication(addition(sK2_skl,c(sK2_skl)),sK1_skl),multiplication(one,sK2_skl)))),
% 107.26/13.98 inference(backward_demodulation,[status(thm)],[f965,f68])).
% 107.26/13.98 fof(f1568,plain,(
% 107.26/13.98 complement(c(sK1_skl),sK1_skl)|~multiplication(sK1_skl,c(sK1_skl))=zero|~multiplication(c(sK1_skl),sK1_skl)=zero),
% 107.26/13.98 inference(resolution,[status(thm)],[f965,f46])).
% 107.26/13.98 fof(f1585,plain,(
% 107.26/13.98 ~one=addition(multiplication(c(sK1_skl),c(sK2_skl)),addition(multiplication(addition(sK2_skl,c(sK2_skl)),sK1_skl),sK2_skl))),
% 107.26/13.98 inference(forward_demodulation,[status(thm)],[f27,f1566])).
% 107.26/13.98 fof(f1587,plain,(
% 107.26/13.98 complement(c(sK1_skl),sK1_skl)|~zero=zero|~multiplication(c(sK1_skl),sK1_skl)=zero),
% 107.26/13.98 inference(forward_demodulation,[status(thm)],[f414,f1568])).
% 107.26/13.98 fof(f1588,plain,(
% 107.26/13.98 complement(c(sK1_skl),sK1_skl)|~zero=zero|~zero=zero),
% 107.26/13.98 inference(forward_demodulation,[status(thm)],[f415,f1587])).
% 107.26/13.98 fof(f1589,plain,(
% 107.26/13.98 complement(c(sK1_skl),sK1_skl)|~zero=zero),
% 107.26/13.98 inference(duplicate_literals_removal,[status(thm)],[f1588])).
% 107.26/13.98 fof(f1590,plain,(
% 107.26/13.98 complement(c(sK1_skl),sK1_skl)),
% 107.26/13.98 inference(trivial_equality_resolution,[status(thm)],[f1589])).
% 107.26/13.98 fof(f1599,plain,(
% 107.26/13.98 ~test(c(sK1_skl))|c(c(sK1_skl))=sK1_skl),
% 107.26/13.98 inference(resolution,[status(thm)],[f1590,f51])).
% 107.26/13.98 fof(f1604,plain,(
% 107.26/13.98 c(c(sK1_skl))=sK1_skl),
% 107.26/13.98 inference(forward_subsumption_resolution,[status(thm)],[f1599,f416])).
% 107.26/13.98 fof(f1640,plain,(
% 107.26/13.98 complement(c(sK2_skl),sK2_skl)|~multiplication(sK2_skl,c(sK2_skl))=zero|~multiplication(c(sK2_skl),sK2_skl)=zero),
% 101.48/14.08 inference(resolution,[status(thm)],[f1112,f46])).
% 101.48/14.08 fof(f1657,plain,(
% 101.48/14.08 complement(c(sK2_skl),sK2_skl)|~zero=zero|~multiplication(c(sK2_skl),sK2_skl)=zero),
% 101.48/14.08 inference(forward_demodulation,[status(thm)],[f423,f1640])).
% 101.48/14.08 fof(f1658,plain,(
% 101.48/14.08 complement(c(sK2_skl),sK2_skl)|~zero=zero|~zero=zero),
% 101.48/14.08 inference(forward_demodulation,[status(thm)],[f424,f1657])).
% 101.48/14.08 fof(f1659,plain,(
% 101.48/14.08 complement(c(sK2_skl),sK2_skl)|~zero=zero),
% 101.48/14.08 inference(duplicate_literals_removal,[status(thm)],[f1658])).
% 101.48/14.08 fof(f1660,plain,(
% 101.48/14.08 complement(c(sK2_skl),sK2_skl)),
% 101.48/14.08 inference(trivial_equality_resolution,[status(thm)],[f1659])).
% 101.48/14.08 fof(f1669,plain,(
% 101.48/14.08 ~test(c(sK2_skl))|c(c(sK2_skl))=sK2_skl),
% 101.48/14.08 inference(resolution,[status(thm)],[f1660,f51])).
% 101.48/14.08 fof(f1674,plain,(
% 101.48/14.08 c(c(sK2_skl))=sK2_skl),
% 101.48/14.08 inference(forward_subsumption_resolution,[status(thm)],[f1669,f425])).
% 101.48/14.08 fof(f2018,plain,(
% 101.48/14.08 c(addition(sK2_skl,sK1_skl))=multiplication(c(sK2_skl),c(sK1_skl))),
% 101.48/14.08 inference(resolution,[status(thm)],[f366,f60])).
% 101.48/14.08 fof(f2475,plain,(
% 101.48/14.08 ![X0]: (c(X0)=zero|addition(c(X0),X0)=one)),
% 101.48/14.08 inference(resolution,[status(thm)],[f398,f45])).
% 101.48/14.08 fof(f2863,plain,(
% 101.48/14.08 c(addition(sK1_skl,sK2_skl))=multiplication(c(sK1_skl),c(sK2_skl))),
% 101.48/14.08 inference(resolution,[status(thm)],[f367,f61])).
% 101.48/14.08 fof(f4532,plain,(
% 101.48/14.08 ~one=addition(multiplication(c(sK1_skl),c(sK2_skl)),addition(multiplication(one,sK1_skl),sK2_skl))),
% 101.48/14.08 inference(forward_demodulation,[status(thm)],[f1112,f1585])).
% 101.48/14.08 fof(f4533,plain,(
% 101.48/14.08 ~one=addition(multiplication(c(sK1_skl),c(sK2_skl)),addition(sK1_skl,sK2_skl))),
% 101.48/14.08 inference(forward_demodulation,[status(thm)],[f27,f4532])).
% 101.48/14.08 fof(f29456,plain,(
% 101.48/14.08 ~one=addition(c(addition(sK1_skl,sK2_skl)),addition(sK1_skl,sK2_skl))),
% 101.48/14.08 inference(backward_demodulation,[status(thm)],[f2863,f4533])).
% 101.48/14.08 fof(f29568,plain,(
% 101.48/14.08 c(addition(sK1_skl,sK2_skl))=zero),
% 101.48/14.08 inference(resolution,[status(thm)],[f29456,f2475])).
% 101.48/14.08 fof(f29587,plain,(
% 101.48/14.08 ~one=addition(zero,addition(sK1_skl,sK2_skl))),
% 101.48/14.08 inference(backward_demodulation,[status(thm)],[f29568,f29456])).
% 101.48/14.08 fof(f29590,plain,(
% 101.48/14.08 c(addition(sK2_skl,sK1_skl))=zero),
% 101.48/14.08 inference(paramodulation,[status(thm)],[f21,f29568])).
% 101.48/14.08 fof(f29600,plain,(
% 101.48/14.08 ~one=addition(sK1_skl,sK2_skl)),
% 101.48/14.08 inference(forward_demodulation,[status(thm)],[f186,f29587])).
% 101.48/14.08 fof(f29605,plain,(
% 101.48/14.08 ~one=addition(sK2_skl,sK1_skl)),
% 101.48/14.08 inference(paramodulation,[status(thm)],[f21,f29600])).
% 101.48/14.08 fof(f29607,plain,(
% 101.48/14.08 zero=multiplication(c(sK2_skl),c(sK1_skl))),
% 101.48/14.08 inference(backward_demodulation,[status(thm)],[f29590,f2018])).
% 101.48/14.08 fof(f152754,plain,(
% 101.48/14.08 ![X0]: (~test(X0)|c(multiplication(X0,c(sK1_skl)))=addition(c(X0),sK1_skl))),
% 101.48/14.08 inference(forward_demodulation,[status(thm)],[f1604,f418])).
% 101.48/14.08 fof(f152755,plain,(
% 101.48/14.08 c(multiplication(c(sK2_skl),c(sK1_skl)))=addition(c(c(sK2_skl)),sK1_skl)),
% 101.48/14.08 inference(resolution,[status(thm)],[f152754,f425])).
% 101.48/14.08 fof(f152763,plain,(
% 101.48/14.08 c(zero)=addition(c(c(sK2_skl)),sK1_skl)),
% 101.48/14.08 inference(forward_demodulation,[status(thm)],[f29607,f152755])).
% 101.48/14.08 fof(f152764,plain,(
% 101.48/14.08 one=addition(c(c(sK2_skl)),sK1_skl)),
% 101.48/14.08 inference(forward_demodulation,[status(thm)],[f404,f152763])).
% 101.48/14.08 fof(f152765,plain,(
% 101.48/14.08 one=addition(sK2_skl,sK1_skl)),
% 101.48/14.08 inference(forward_demodulation,[status(thm)],[f1674,f152764])).
% 101.48/14.08 fof(f152766,plain,(
% 101.48/14.08 $false),
% 101.48/14.08 inference(forward_subsumption_resolution,[status(thm)],[f152765,f29605])).
% 101.48/14.08 % SZS output end CNFRefutation for theBenchmark.p
% 101.48/14.09 % Elapsed time: 13.718465 seconds
% 101.48/14.09 % CPU time: 108.541649 seconds
% 101.48/14.09 % Total memory used: 826.737 MB
% 101.48/14.09 % Net memory used: 800.846 MB
%------------------------------------------------------------------------------