%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUN135-1.006 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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 01:57:32 PM UTC 2026
% Result : Unsatisfiable 18.21s 2.74s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUN135-1.006 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n004.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 03:28:49 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 18.21/2.74 % Refutation found
% 18.21/2.74 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 18.21/2.74 % SZS output start CNFRefutation for theBenchmark
% 18.21/2.74 fof(f1,axiom,(
% 18.21/2.74 (![X]: (minus(X,zero) = X ))),
% 18.21/2.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/2.74 fof(f2,axiom,(
% 18.21/2.74 (![X,Y]: (minus(s(X),s(Y)) = minus(X,Y) ))),
% 18.21/2.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/2.74 fof(f3,axiom,(
% 18.21/2.74 (![Y]: ('<='(zero,Y) = true ))),
% 18.21/2.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/2.74 fof(f4,axiom,(
% 18.21/2.74 (![X]: ('<='(s(X),zero) = false ))),
% 18.21/2.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/2.74 fof(f5,axiom,(
% 18.21/2.74 (![X,Y]: ('<='(s(X),s(Y)) = '<='(X,Y) ))),
% 18.21/2.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/2.74 fof(f6,axiom,(
% 18.21/2.74 (![X,Y]: (if(true,X,Y) = X ))),
% 18.21/2.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/2.74 fof(f7,axiom,(
% 18.21/2.74 (![X,Y]: (if(false,X,Y) = Y ))),
% 18.21/2.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/2.74 fof(f9,axiom,(
% 18.21/2.74 (![X]: (perfectp(s(X)) = f(X,s(zero),s(X),s(X)) ))),
% 18.21/2.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/2.74 fof(f10,axiom,(
% 18.21/2.74 (![Y,U]: (f(zero,Y,zero,U) = true ))),
% 18.21/2.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/2.74 fof(f12,axiom,(
% 18.21/2.74 (![X,Z,U]: (f(s(X),zero,Z,U) = f(X,U,minus(Z,s(X)),U) ))),
% 18.21/2.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/2.74 fof(f13,axiom,(
% 18.21/2.74 (![X,Y,Z,U]: (f(s(X),s(Y),Z,U) = if('<='(X,Y),f(s(X),minus(Y,X),Z,U),f(X,U,Z,U)) ))),
% 18.21/2.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/2.74 fof(f14,negated_conjecture,(
% 18.21/2.74 (![X]: (perfectp(X) != true ))),
% 18.21/2.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/2.74 fof(f15,plain,(
% 18.21/2.74 ![X0]: (minus(X0,zero)=X0)),
% 18.21/2.74 inference(cnf_transformation,[status(thm)],[f1])).
% 18.21/2.74 fof(f16,plain,(
% 18.21/2.74 ![X0,X1]: (minus(s(X0),s(X1))=minus(X0,X1))),
% 18.21/2.74 inference(cnf_transformation,[status(thm)],[f2])).
% 18.21/2.74 fof(f17,plain,(
% 18.21/2.74 ![X0]: ('<='(zero,X0)=true)),
% 18.21/2.74 inference(cnf_transformation,[status(thm)],[f3])).
% 18.21/2.74 fof(f18,plain,(
% 18.21/2.74 ![X0]: ('<='(s(X0),zero)=false)),
% 18.21/2.74 inference(cnf_transformation,[status(thm)],[f4])).
% 18.21/2.74 fof(f19,plain,(
% 18.21/2.74 ![X0,X1]: ('<='(s(X0),s(X1))='<='(X0,X1))),
% 18.21/2.74 inference(cnf_transformation,[status(thm)],[f5])).
% 18.21/2.74 fof(f20,plain,(
% 18.21/2.74 ![X0,X1]: (if(true,X0,X1)=X0)),
% 18.21/2.74 inference(cnf_transformation,[status(thm)],[f6])).
% 18.21/2.74 fof(f21,plain,(
% 18.21/2.74 ![X0,X1]: (if(false,X0,X1)=X1)),
% 18.21/2.74 inference(cnf_transformation,[status(thm)],[f7])).
% 18.21/2.74 fof(f23,plain,(
% 18.21/2.74 ![X0]: (perfectp(s(X0))=f(X0,s(zero),s(X0),s(X0)))),
% 18.21/2.74 inference(cnf_transformation,[status(thm)],[f9])).
% 18.21/2.74 fof(f24,plain,(
% 18.21/2.74 ![X0,X1]: (f(zero,X0,zero,X1)=true)),
% 18.21/2.74 inference(cnf_transformation,[status(thm)],[f10])).
% 18.21/2.74 fof(f26,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(X0),zero,X1,X2)=f(X0,X2,minus(X1,s(X0)),X2))),
% 18.21/2.74 inference(cnf_transformation,[status(thm)],[f12])).
% 18.21/2.74 fof(f27,plain,(
% 18.21/2.74 ![X0,X1,X2,X3]: (f(s(X0),s(X1),X2,X3)=if('<='(X0,X1),f(s(X0),minus(X1,X0),X2,X3),f(X0,X3,X2,X3)))),
% 18.21/2.74 inference(cnf_transformation,[status(thm)],[f13])).
% 18.21/2.74 fof(f28,plain,(
% 18.21/2.74 ![X0]: (~perfectp(X0)=true)),
% 18.21/2.74 inference(cnf_transformation,[status(thm)],[f14])).
% 18.21/2.74 fof(f33,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(X0),zero,s(X1),X2)=f(X0,X2,minus(X1,X0),X2))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f16,f26])).
% 18.21/2.74 fof(f36,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(X0)),zero,s(s(X1)),X2)=f(s(X0),X2,minus(X1,X0),X2))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f16,f33])).
% 18.21/2.74 fof(f37,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(zero),zero,s(X0),X1)=f(zero,X1,X0,X1))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f15,f33])).
% 18.21/2.74 fof(f41,plain,(
% 18.21/2.74 ![X0]: (f(s(zero),zero,s(zero),X0)=true)),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f24,f37])).
% 18.21/2.74 fof(f62,plain,(
% 18.21/2.74 ![X0,X1,X2,X3]: (f(s(s(X0)),s(s(X1)),X2,X3)=if('<='(X0,X1),f(s(s(X0)),minus(s(X1),s(X0)),X2,X3),f(s(X0),X3,X2,X3)))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f19,f27])).
% 18.21/2.74 fof(f63,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(X0)),s(zero),X1,X2)=if(false,f(s(s(X0)),minus(zero,s(X0)),X1,X2),f(s(X0),X2,X1,X2)))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f18,f27])).
% 18.21/2.74 fof(f64,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(zero),s(X0),X1,X2)=if(true,f(s(zero),minus(X0,zero),X1,X2),f(zero,X2,X1,X2)))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f17,f27])).
% 18.21/2.74 fof(f79,plain,(
% 18.21/2.74 ![X0,X1,X2,X3]: (f(s(s(X0)),s(s(X1)),X2,X3)=if('<='(X0,X1),f(s(s(X0)),minus(X1,X0),X2,X3),f(s(X0),X3,X2,X3)))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f16,f62])).
% 18.21/2.74 fof(f80,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(X0)),s(zero),X1,X2)=f(s(X0),X2,X1,X2))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f21,f63])).
% 18.21/2.74 fof(f81,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(zero),s(X0),X1,X2)=f(s(zero),minus(X0,zero),X1,X2))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f20,f64])).
% 18.21/2.74 fof(f82,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(zero),s(X0),X1,X2)=f(s(zero),X0,X1,X2))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f15,f81])).
% 18.21/2.74 fof(f99,plain,(
% 18.21/2.74 ![X0,X1,X2,X3]: (f(s(s(s(X0))),s(s(s(X1))),X2,X3)=if('<='(X0,X1),f(s(s(s(X0))),minus(s(X1),s(X0)),X2,X3),f(s(s(X0)),X3,X2,X3)))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f19,f79])).
% 18.21/2.74 fof(f100,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(X0))),s(s(zero)),X1,X2)=if(false,f(s(s(s(X0))),minus(zero,s(X0)),X1,X2),f(s(s(X0)),X2,X1,X2)))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f18,f79])).
% 18.21/2.74 fof(f101,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(zero)),s(s(X0)),X1,X2)=if(true,f(s(s(zero)),minus(X0,zero),X1,X2),f(s(zero),X2,X1,X2)))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f17,f79])).
% 18.21/2.74 fof(f112,plain,(
% 18.21/2.74 ![X0,X1,X2,X3]: (f(s(s(s(X0))),s(s(s(X1))),X2,X3)=if('<='(X0,X1),f(s(s(s(X0))),minus(X1,X0),X2,X3),f(s(s(X0)),X3,X2,X3)))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f16,f99])).
% 18.21/2.74 fof(f113,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(X0))),s(s(zero)),X1,X2)=f(s(s(X0)),X2,X1,X2))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f21,f100])).
% 18.21/2.74 fof(f114,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(zero)),s(s(X0)),X1,X2)=f(s(s(zero)),minus(X0,zero),X1,X2))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f20,f101])).
% 18.21/2.74 fof(f115,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(zero)),s(s(X0)),X1,X2)=f(s(s(zero)),X0,X1,X2))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f15,f114])).
% 18.21/2.74 fof(f147,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(zero)),s(zero),X0,s(X1))=f(s(zero),X1,X0,s(X1)))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f80,f82])).
% 18.21/2.74 fof(f163,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(s(zero))),s(zero),X0,s(s(X1)))=f(s(s(zero)),X1,X0,s(s(X1))))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f80,f115])).
% 18.21/2.74 fof(f176,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(zero)),s(zero),X0,s(s(X1)))=f(s(zero),X1,X0,s(s(X1))))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f82,f147])).
% 18.21/2.74 fof(f216,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(X0))),zero,s(s(s(X1))),X2)=f(s(s(X0)),X2,minus(X1,X0),X2))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f16,f36])).
% 18.21/2.74 fof(f217,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(zero)),zero,s(s(X0)),X1)=f(s(zero),X1,X0,X1))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f15,f36])).
% 18.21/2.74 fof(f236,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(zero)),zero,s(s(X0)),X1)=f(s(s(zero)),s(zero),X0,X1))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f80,f217])).
% 18.21/2.74 fof(f265,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(X0))),s(s(zero)),X1,X2)=f(s(s(s(X0))),s(zero),X1,X2))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f80,f113])).
% 18.21/2.74 fof(f505,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(zero)),s(zero),X0,s(s(s(X1))))=f(s(zero),X1,X0,s(s(s(X1)))))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f82,f176])).
% 18.21/2.74 fof(f820,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(s(zero))),s(zero),X0,s(s(s(s(X1)))))=f(s(s(zero)),X1,X0,s(s(s(s(X1))))))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f115,f163])).
% 18.21/2.74 fof(f854,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(zero)),s(zero),X0,s(s(s(s(X1)))))=f(s(zero),X1,X0,s(s(s(s(X1))))))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f82,f505])).
% 18.21/2.74 fof(f979,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(s(X0)))),zero,s(s(s(s(X1)))),X2)=f(s(s(s(X0))),X2,minus(X1,X0),X2))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f16,f216])).
% 18.21/2.74 fof(f980,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(s(zero))),zero,s(s(s(X0))),X1)=f(s(s(zero)),X1,X0,X1))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f15,f216])).
% 18.21/2.74 fof(f1021,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(s(zero))),zero,s(s(s(X0))),X1)=f(s(s(s(zero))),s(zero),X0,X1))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f80,f980])).
% 18.21/2.74 fof(f1103,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(s(X0)))),s(s(s(zero))),X1,X2)=if(false,f(s(s(s(s(X0)))),minus(zero,s(X0)),X1,X2),f(s(s(s(X0))),X2,X1,X2)))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f18,f112])).
% 18.21/2.74 fof(f1104,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(zero))),s(s(s(X0))),X1,X2)=if(true,f(s(s(s(zero))),minus(X0,zero),X1,X2),f(s(s(zero)),X2,X1,X2)))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f17,f112])).
% 18.21/2.74 fof(f1135,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(s(X0)))),s(s(s(zero))),X1,X2)=f(s(s(s(X0))),X2,X1,X2))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f21,f1103])).
% 18.21/2.74 fof(f1136,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(zero))),s(s(s(X0))),X1,X2)=f(s(s(s(zero))),minus(X0,zero),X1,X2))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f20,f1104])).
% 18.21/2.74 fof(f1137,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(zero))),s(s(s(X0))),X1,X2)=f(s(s(s(zero))),X0,X1,X2))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f15,f1136])).
% 18.21/2.74 fof(f1300,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(s(s(zero)))),s(s(zero)),X0,s(s(s(X1))))=f(s(s(s(zero))),X1,X0,s(s(s(X1)))))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f113,f1137])).
% 18.21/2.74 fof(f1306,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(s(zero)))),s(s(s(X0))),X1,s(s(s(X2))))=if('<='(s(zero),X0),f(s(s(s(s(zero)))),minus(X0,s(zero)),X1,s(s(s(X2)))),f(s(s(s(zero))),X2,X1,s(s(s(X2))))))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f1137,f112])).
% 18.21/2.74 fof(f1314,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(s(s(zero)))),s(zero),X0,s(s(s(X1))))=f(s(s(s(zero))),X1,X0,s(s(s(X1)))))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f265,f1300])).
% 18.21/2.74 fof(f1413,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(s(X0)))),s(s(s(zero))),X1,X2)=f(s(s(s(s(X0)))),s(s(zero)),X1,X2))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f113,f1135])).
% 18.21/2.74 fof(f1444,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(s(X0)))),s(s(s(zero))),X1,X2)=f(s(s(s(s(X0)))),s(zero),X1,X2))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f265,f1413])).
% 18.21/2.74 fof(f1721,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(s(s(X0))))),zero,s(s(s(s(s(X1))))),X2)=f(s(s(s(s(X0)))),X2,minus(X1,X0),X2))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f16,f979])).
% 18.21/2.74 fof(f2054,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(zero)),s(zero),X0,s(s(s(s(s(X1))))))=f(s(zero),X1,X0,s(s(s(s(s(X1)))))))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f82,f854])).
% 18.21/2.74 fof(f3098,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(s(zero))),s(zero),X0,s(s(s(s(s(s(X1)))))))=f(s(s(zero)),X1,X0,s(s(s(s(s(s(X1))))))))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f115,f820])).
% 18.21/2.74 fof(f3182,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(s(s(zero)))),s(zero),X0,s(s(s(s(s(s(X1)))))))=f(s(s(s(zero))),X1,X0,s(s(s(s(s(s(X1))))))))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f1137,f1314])).
% 18.21/2.74 fof(f3379,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(zero)),s(zero),X0,s(s(s(s(s(s(X1)))))))=f(s(zero),X1,X0,s(s(s(s(s(s(X1))))))))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f82,f2054])).
% 18.21/2.74 fof(f3809,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(s(s(s(zero))))),zero,s(s(s(s(s(X0))))),X1)=f(s(s(s(s(zero)))),X1,X0,X1))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f15,f1721])).
% 18.21/2.74 fof(f3982,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(s(s(s(zero))))),zero,s(s(s(s(s(X0))))),X1)=f(s(s(s(s(s(zero))))),s(s(s(zero))),X0,X1))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f1135,f3809])).
% 18.21/2.74 fof(f4039,plain,(
% 18.21/2.74 ![X0,X1]: (f(s(s(s(s(s(zero))))),zero,s(s(s(s(s(X0))))),X1)=f(s(s(s(s(s(zero))))),s(zero),X0,X1))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f1444,f3982])).
% 18.21/2.74 fof(f7828,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(s(zero)))),s(s(s(s(X0)))),X1,s(s(s(X2))))=if('<='(zero,X0),f(s(s(s(s(zero)))),minus(s(X0),s(zero)),X1,s(s(s(X2)))),f(s(s(s(zero))),X2,X1,s(s(s(X2))))))),
% 18.21/2.74 inference(paramodulation,[status(thm)],[f19,f1306])).
% 18.21/2.74 fof(f7848,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(s(zero)))),s(s(s(s(X0)))),X1,s(s(s(X2))))=if(true,f(s(s(s(s(zero)))),minus(s(X0),s(zero)),X1,s(s(s(X2)))),f(s(s(s(zero))),X2,X1,s(s(s(X2))))))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f17,f7828])).
% 18.21/2.74 fof(f7849,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(s(zero)))),s(s(s(s(X0)))),X1,s(s(s(X2))))=f(s(s(s(s(zero)))),minus(s(X0),s(zero)),X1,s(s(s(X2)))))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f20,f7848])).
% 18.21/2.74 fof(f7850,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(s(zero)))),s(s(s(s(X0)))),X1,s(s(s(X2))))=f(s(s(s(s(zero)))),minus(X0,zero),X1,s(s(s(X2)))))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f16,f7849])).
% 18.21/2.74 fof(f7851,plain,(
% 18.21/2.74 ![X0,X1,X2]: (f(s(s(s(s(zero)))),s(s(s(s(X0)))),X1,s(s(s(X2))))=f(s(s(s(s(zero)))),X0,X1,s(s(s(X2)))))),
% 18.21/2.74 inference(forward_demodulation,[status(thm)],[f15,f7850])).
% 18.21/2.74 fof(f7869,plain,(
% 18.21/2.79 ![X0,X1]: (f(s(s(s(s(s(zero))))),zero,s(s(s(s(s(X0))))),s(s(s(s(X1)))))=f(s(s(s(s(zero)))),X1,X0,s(s(s(s(X1))))))),
% 18.21/2.79 inference(paramodulation,[status(thm)],[f3809,f7851])).
% 18.21/2.79 fof(f7892,plain,(
% 18.21/2.79 ![X0,X1]: (f(s(s(s(s(s(zero))))),s(zero),X0,s(s(s(s(X1)))))=f(s(s(s(s(zero)))),X1,X0,s(s(s(s(X1))))))),
% 18.21/2.79 inference(forward_demodulation,[status(thm)],[f4039,f7869])).
% 18.21/2.79 fof(f7927,plain,(
% 18.21/2.79 perfectp(s(s(s(s(s(s(zero)))))))=f(s(s(s(s(zero)))),s(s(zero)),s(s(s(s(s(s(zero)))))),s(s(s(s(s(s(zero)))))))),
% 18.21/2.79 inference(paramodulation,[status(thm)],[f23,f7892])).
% 18.21/2.79 fof(f7953,plain,(
% 18.21/2.79 perfectp(s(s(s(s(s(s(zero)))))))=f(s(s(s(s(zero)))),s(zero),s(s(s(s(s(s(zero)))))),s(s(s(s(s(s(zero)))))))),
% 18.21/2.79 inference(forward_demodulation,[status(thm)],[f265,f7927])).
% 18.21/2.79 fof(f14284,plain,(
% 18.21/2.79 perfectp(s(s(s(s(s(s(zero)))))))=f(s(s(s(zero))),zero,s(s(s(s(s(s(zero)))))),s(s(s(s(s(s(zero)))))))),
% 18.21/2.79 inference(paramodulation,[status(thm)],[f3182,f7953])).
% 18.21/2.79 fof(f14289,plain,(
% 18.21/2.79 perfectp(s(s(s(s(s(s(zero)))))))=f(s(s(s(zero))),s(zero),s(s(s(zero))),s(s(s(s(s(s(zero)))))))),
% 18.21/2.79 inference(forward_demodulation,[status(thm)],[f1021,f14284])).
% 18.21/2.79 fof(f14291,plain,(
% 18.21/2.79 perfectp(s(s(s(s(s(s(zero)))))))=f(s(s(zero)),zero,s(s(s(zero))),s(s(s(s(s(s(zero)))))))),
% 18.21/2.79 inference(paramodulation,[status(thm)],[f3098,f14289])).
% 18.21/2.79 fof(f14298,plain,(
% 18.21/2.79 perfectp(s(s(s(s(s(s(zero)))))))=f(s(s(zero)),s(zero),s(zero),s(s(s(s(s(s(zero)))))))),
% 18.21/2.79 inference(forward_demodulation,[status(thm)],[f236,f14291])).
% 18.21/2.79 fof(f14307,plain,(
% 18.21/2.79 perfectp(s(s(s(s(s(s(zero)))))))=f(s(zero),zero,s(zero),s(s(s(s(s(s(zero)))))))),
% 18.21/2.79 inference(paramodulation,[status(thm)],[f3379,f14298])).
% 18.21/2.79 fof(f14315,plain,(
% 18.21/2.79 perfectp(s(s(s(s(s(s(zero)))))))=true),
% 18.21/2.79 inference(forward_demodulation,[status(thm)],[f41,f14307])).
% 18.21/2.79 fof(f14316,plain,(
% 18.21/2.79 $false),
% 18.21/2.79 inference(forward_subsumption_resolution,[status(thm)],[f14315,f28])).
% 18.21/2.79 % SZS output end CNFRefutation for theBenchmark.p
% 10.35/2.82 % Elapsed time: 2.448595 seconds
% 10.35/2.82 % CPU time: 18.960197 seconds
% 10.35/2.82 % Total memory used: 161.224 MB
% 10.35/2.82 % Net memory used: 159.296 MB
%------------------------------------------------------------------------------