%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PUZ054-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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 02:00:23 PM UTC 2026
% Result : Satisfiable 0.15s 0.38s
% Output : Saturation 0.15s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C] : ifeq(A,A,B,C) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0)))))))))) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] : ifeq(p(s(s(X)),Y),true,p(X,s(Y)),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] : ifeq(p(X,s(s(Y))),true,p(X,s(Y)),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y] : ifeq(p(s(X),s(Y)),true,p(s(X),Y),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,negated_conjecture,
p(s(n0),n0) != true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,plain,
! [X0,X1,X2] : ifeq(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f8,plain,
p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(s(n0)))))))))) = true,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f9,plain,
! [X0,X1] : ifeq(p(s(s(X0)),X1),true,p(X0,s(X1)),true) = true,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f10,plain,
! [X0,X1] : ifeq(p(X0,s(s(X1))),true,p(X0,s(X1)),true) = true,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f11,plain,
! [X0,X1] : ifeq(p(s(X0),s(X1)),true,p(s(X0),X1),true) = true,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f12,plain,
p(s(n0),n0) != true,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f13,definition,
sF1_fnc = s(n0),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f14,definition,
sF0_fnc = p(sF1_fnc,n0),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f15,plain,
sF0_fnc != true,
inference(definition_folding,[],[f12,f14,f13]) ).
fof(f16,plain,
p(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(s(sF1_fnc))))))))) = true,
inference(backward_demodulation,[status(thm)],[f13,f8]) ).
fof(f17,plain,
p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),s(s(s(s(s(s(s(s(sF1_fnc))))))))) = true,
inference(forward_demodulation,[status(thm)],[f13,f16]) ).
fof(f18,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))),true) = true,
inference(paramodulation,[status(thm)],[f17,f9]) ).
fof(f19,plain,
! [X0] : ifeq(p(s(sF1_fnc),X0),true,p(n0,s(X0)),true) = true,
inference(paramodulation,[status(thm)],[f13,f9]) ).
fof(f20,plain,
ifeq(p(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))),s(s(s(s(s(s(s(sF1_fnc)))))))),true,true,true) = true,
inference(paramodulation,[status(thm)],[f17,f9]) ).
fof(f21,plain,
! [X0] : ifeq(p(s(s(X0)),n0),true,p(X0,sF1_fnc),true) = true,
inference(paramodulation,[status(thm)],[f13,f9]) ).
fof(f22,plain,
p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f18]) ).
fof(f23,plain,
ifeq(true,true,p(s(s(s(s(s(sF1_fnc))))),s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))),true) = true,
inference(paramodulation,[status(thm)],[f22,f9]) ).
fof(f25,plain,
p(s(s(s(s(s(sF1_fnc))))),s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f23]) ).
fof(f29,plain,
ifeq(true,true,p(s(s(s(sF1_fnc))),s(s(s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))))),true) = true,
inference(paramodulation,[status(thm)],[f25,f9]) ).
fof(f31,plain,
p(s(s(s(sF1_fnc))),s(s(s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f29]) ).
fof(f33,plain,
ifeq(true,true,p(s(sF1_fnc),s(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))))),true) = true,
inference(paramodulation,[status(thm)],[f31,f9]) ).
fof(f35,plain,
p(s(sF1_fnc),s(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f33]) ).
fof(f37,plain,
ifeq(true,true,p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))))))),true) = true,
inference(paramodulation,[status(thm)],[f35,f19]) ).
fof(f39,plain,
p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f37]) ).
fof(f46,plain,
ifeq(true,true,p(s(sF1_fnc),s(s(s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))))),true) = true,
inference(paramodulation,[status(thm)],[f35,f11]) ).
fof(f47,plain,
ifeq(true,true,p(s(s(s(sF1_fnc))),s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))),true) = true,
inference(paramodulation,[status(thm)],[f31,f11]) ).
fof(f48,plain,
ifeq(true,true,p(s(s(s(s(s(sF1_fnc))))),s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))),true) = true,
inference(paramodulation,[status(thm)],[f25,f11]) ).
fof(f49,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(s(s(s(s(s(s(sF1_fnc))))))))),true) = true,
inference(paramodulation,[status(thm)],[f22,f11]) ).
fof(f50,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),s(s(s(s(s(s(s(sF1_fnc)))))))),true) = true,
inference(paramodulation,[status(thm)],[f17,f11]) ).
fof(f51,plain,
! [X0] : ifeq(p(sF1_fnc,s(X0)),true,p(s(n0),X0),true) = true,
inference(paramodulation,[status(thm)],[f13,f11]) ).
fof(f52,plain,
! [X0] : ifeq(p(s(X0),sF1_fnc),true,p(s(X0),n0),true) = true,
inference(paramodulation,[status(thm)],[f13,f11]) ).
fof(f53,plain,
ifeq(p(s(sF1_fnc),s(s(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))))))),true,true,true) = true,
inference(paramodulation,[status(thm)],[f35,f11]) ).
fof(f54,plain,
ifeq(p(s(s(s(sF1_fnc))),s(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))))),true,true,true) = true,
inference(paramodulation,[status(thm)],[f31,f11]) ).
fof(f55,plain,
ifeq(p(s(s(s(s(s(sF1_fnc))))),s(s(s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))))),true,true,true) = true,
inference(paramodulation,[status(thm)],[f25,f11]) ).
fof(f56,plain,
ifeq(p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))),true,true,true) = true,
inference(paramodulation,[status(thm)],[f22,f11]) ).
fof(f57,plain,
ifeq(p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))),true,true,true) = true,
inference(paramodulation,[status(thm)],[f17,f11]) ).
fof(f59,plain,
p(s(sF1_fnc),s(s(s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f46]) ).
fof(f60,plain,
p(s(s(s(sF1_fnc))),s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f47]) ).
fof(f61,plain,
p(s(s(s(s(s(sF1_fnc))))),s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f48]) ).
fof(f62,plain,
p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(s(s(s(s(s(s(sF1_fnc))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f49]) ).
fof(f63,plain,
p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),s(s(s(s(s(s(s(sF1_fnc)))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f50]) ).
fof(f64,plain,
! [X0] : ifeq(p(sF1_fnc,s(X0)),true,p(sF1_fnc,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f51]) ).
fof(f66,plain,
ifeq(p(sF1_fnc,sF1_fnc),true,p(sF1_fnc,n0),true) = true,
inference(paramodulation,[status(thm)],[f13,f64]) ).
fof(f68,plain,
ifeq(p(sF1_fnc,sF1_fnc),true,sF0_fnc,true) = true,
inference(forward_demodulation,[status(thm)],[f14,f66]) ).
fof(f77,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),s(s(s(s(s(s(sF1_fnc))))))),true) = true,
inference(paramodulation,[status(thm)],[f63,f11]) ).
fof(f79,plain,
ifeq(p(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))),s(s(s(s(s(s(sF1_fnc))))))),true,true,true) = true,
inference(paramodulation,[status(thm)],[f63,f9]) ).
fof(f81,plain,
p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),s(s(s(s(s(s(sF1_fnc))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f77]) ).
fof(f85,plain,
ifeq(true,true,p(n0,s(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))))),true) = true,
inference(paramodulation,[status(thm)],[f39,f10]) ).
fof(f92,plain,
! [X0] : ifeq(p(X0,s(sF1_fnc)),true,p(X0,s(n0)),true) = true,
inference(paramodulation,[status(thm)],[f13,f10]) ).
fof(f93,plain,
ifeq(p(n0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))))))),true,true,true) = true,
inference(paramodulation,[status(thm)],[f39,f10]) ).
fof(f103,plain,
p(n0,s(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f85]) ).
fof(f110,plain,
! [X0] : ifeq(p(X0,s(sF1_fnc)),true,p(X0,sF1_fnc),true) = true,
inference(forward_demodulation,[status(thm)],[f13,f92]) ).
fof(f118,plain,
ifeq(true,true,p(n0,s(s(s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))))),true) = true,
inference(paramodulation,[status(thm)],[f103,f10]) ).
fof(f122,plain,
p(n0,s(s(s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f118]) ).
fof(f127,plain,
ifeq(true,true,p(n0,s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))),true) = true,
inference(paramodulation,[status(thm)],[f122,f10]) ).
fof(f130,plain,
p(n0,s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f127]) ).
fof(f134,plain,
ifeq(true,true,p(n0,s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))),true) = true,
inference(paramodulation,[status(thm)],[f130,f10]) ).
fof(f137,plain,
p(n0,s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f134]) ).
fof(f141,plain,
ifeq(true,true,p(n0,s(s(s(s(s(s(s(s(sF1_fnc))))))))),true) = true,
inference(paramodulation,[status(thm)],[f137,f10]) ).
fof(f144,plain,
p(n0,s(s(s(s(s(s(s(s(sF1_fnc))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f141]) ).
fof(f148,plain,
ifeq(true,true,p(n0,s(s(s(s(s(s(s(sF1_fnc)))))))),true) = true,
inference(paramodulation,[status(thm)],[f144,f10]) ).
fof(f151,plain,
p(n0,s(s(s(s(s(s(s(sF1_fnc)))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f148]) ).
fof(f155,plain,
ifeq(true,true,p(n0,s(s(s(s(s(s(sF1_fnc))))))),true) = true,
inference(paramodulation,[status(thm)],[f151,f10]) ).
fof(f158,plain,
p(n0,s(s(s(s(s(s(sF1_fnc))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f155]) ).
fof(f162,plain,
ifeq(true,true,p(n0,s(s(s(s(s(sF1_fnc)))))),true) = true,
inference(paramodulation,[status(thm)],[f158,f10]) ).
fof(f165,plain,
p(n0,s(s(s(s(s(sF1_fnc)))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f162]) ).
fof(f169,plain,
ifeq(true,true,p(n0,s(s(s(s(sF1_fnc))))),true) = true,
inference(paramodulation,[status(thm)],[f165,f10]) ).
fof(f172,plain,
p(n0,s(s(s(s(sF1_fnc))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f169]) ).
fof(f176,plain,
ifeq(true,true,p(n0,s(s(s(sF1_fnc)))),true) = true,
inference(paramodulation,[status(thm)],[f172,f10]) ).
fof(f179,plain,
p(n0,s(s(s(sF1_fnc)))) = true,
inference(forward_demodulation,[status(thm)],[f7,f176]) ).
fof(f183,plain,
ifeq(true,true,p(n0,s(s(sF1_fnc))),true) = true,
inference(paramodulation,[status(thm)],[f179,f10]) ).
fof(f186,plain,
p(n0,s(s(sF1_fnc))) = true,
inference(forward_demodulation,[status(thm)],[f7,f183]) ).
fof(f190,plain,
ifeq(true,true,p(n0,s(sF1_fnc)),true) = true,
inference(paramodulation,[status(thm)],[f186,f10]) ).
fof(f193,plain,
p(n0,s(sF1_fnc)) = true,
inference(forward_demodulation,[status(thm)],[f7,f190]) ).
fof(f197,plain,
ifeq(true,true,p(n0,sF1_fnc),true) = true,
inference(paramodulation,[status(thm)],[f193,f110]) ).
fof(f201,plain,
p(n0,sF1_fnc) = true,
inference(forward_demodulation,[status(thm)],[f7,f197]) ).
fof(f209,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(s(s(s(s(s(sF1_fnc)))))))),true) = true,
inference(paramodulation,[status(thm)],[f62,f11]) ).
fof(f215,plain,
p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(s(s(s(s(s(sF1_fnc)))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f209]) ).
fof(f221,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),s(s(s(s(s(sF1_fnc)))))),true) = true,
inference(paramodulation,[status(thm)],[f81,f11]) ).
fof(f225,plain,
ifeq(p(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))),s(s(s(s(s(sF1_fnc)))))),true,true,true) = true,
inference(paramodulation,[status(thm)],[f81,f9]) ).
fof(f227,plain,
p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),s(s(s(s(s(sF1_fnc)))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f221]) ).
fof(f232,plain,
ifeq(true,true,p(s(sF1_fnc),s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))),true) = true,
inference(paramodulation,[status(thm)],[f59,f11]) ).
fof(f239,plain,
p(s(sF1_fnc),s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f232]) ).
fof(f245,plain,
ifeq(true,true,p(s(sF1_fnc),s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))),true) = true,
inference(paramodulation,[status(thm)],[f239,f11]) ).
fof(f252,plain,
p(s(sF1_fnc),s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f245]) ).
fof(f257,plain,
ifeq(true,true,p(s(sF1_fnc),s(s(s(s(s(s(s(s(sF1_fnc))))))))),true) = true,
inference(paramodulation,[status(thm)],[f252,f11]) ).
fof(f264,plain,
p(s(sF1_fnc),s(s(s(s(s(s(s(s(sF1_fnc))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f257]) ).
fof(f269,plain,
ifeq(true,true,p(s(sF1_fnc),s(s(s(s(s(s(s(sF1_fnc)))))))),true) = true,
inference(paramodulation,[status(thm)],[f264,f11]) ).
fof(f276,plain,
p(s(sF1_fnc),s(s(s(s(s(s(s(sF1_fnc)))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f269]) ).
fof(f281,plain,
ifeq(true,true,p(s(sF1_fnc),s(s(s(s(s(s(sF1_fnc))))))),true) = true,
inference(paramodulation,[status(thm)],[f276,f11]) ).
fof(f288,plain,
p(s(sF1_fnc),s(s(s(s(s(s(sF1_fnc))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f281]) ).
fof(f293,plain,
ifeq(true,true,p(s(sF1_fnc),s(s(s(s(s(sF1_fnc)))))),true) = true,
inference(paramodulation,[status(thm)],[f288,f11]) ).
fof(f300,plain,
p(s(sF1_fnc),s(s(s(s(s(sF1_fnc)))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f293]) ).
fof(f305,plain,
ifeq(true,true,p(s(sF1_fnc),s(s(s(s(sF1_fnc))))),true) = true,
inference(paramodulation,[status(thm)],[f300,f11]) ).
fof(f312,plain,
p(s(sF1_fnc),s(s(s(s(sF1_fnc))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f305]) ).
fof(f317,plain,
ifeq(true,true,p(s(sF1_fnc),s(s(s(sF1_fnc)))),true) = true,
inference(paramodulation,[status(thm)],[f312,f11]) ).
fof(f324,plain,
p(s(sF1_fnc),s(s(s(sF1_fnc)))) = true,
inference(forward_demodulation,[status(thm)],[f7,f317]) ).
fof(f329,plain,
ifeq(true,true,p(s(sF1_fnc),s(s(sF1_fnc))),true) = true,
inference(paramodulation,[status(thm)],[f324,f11]) ).
fof(f336,plain,
p(s(sF1_fnc),s(s(sF1_fnc))) = true,
inference(forward_demodulation,[status(thm)],[f7,f329]) ).
fof(f341,plain,
ifeq(true,true,p(s(sF1_fnc),s(sF1_fnc)),true) = true,
inference(paramodulation,[status(thm)],[f336,f11]) ).
fof(f348,plain,
p(s(sF1_fnc),s(sF1_fnc)) = true,
inference(forward_demodulation,[status(thm)],[f7,f341]) ).
fof(f353,plain,
ifeq(true,true,p(s(sF1_fnc),sF1_fnc),true) = true,
inference(paramodulation,[status(thm)],[f348,f11]) ).
fof(f360,plain,
p(s(sF1_fnc),sF1_fnc) = true,
inference(forward_demodulation,[status(thm)],[f7,f353]) ).
fof(f365,plain,
ifeq(true,true,p(s(sF1_fnc),n0),true) = true,
inference(paramodulation,[status(thm)],[f360,f52]) ).
fof(f371,plain,
p(s(sF1_fnc),n0) = true,
inference(forward_demodulation,[status(thm)],[f7,f365]) ).
fof(f375,plain,
ifeq(true,true,p(s(s(s(s(s(sF1_fnc))))),s(s(s(s(s(s(s(s(sF1_fnc))))))))),true) = true,
inference(paramodulation,[status(thm)],[f61,f11]) ).
fof(f381,plain,
p(s(s(s(s(s(sF1_fnc))))),s(s(s(s(s(s(s(s(sF1_fnc))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f375]) ).
fof(f395,plain,
ifeq(true,true,p(s(s(s(sF1_fnc))),s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))),true) = true,
inference(paramodulation,[status(thm)],[f60,f11]) ).
fof(f402,plain,
p(s(s(s(sF1_fnc))),s(s(s(s(s(s(s(s(s(sF1_fnc)))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f395]) ).
fof(f408,plain,
ifeq(true,true,p(s(s(s(sF1_fnc))),s(s(s(s(s(s(s(s(sF1_fnc))))))))),true) = true,
inference(paramodulation,[status(thm)],[f402,f11]) ).
fof(f415,plain,
p(s(s(s(sF1_fnc))),s(s(s(s(s(s(s(s(sF1_fnc))))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f408]) ).
fof(f421,plain,
ifeq(true,true,p(s(s(s(sF1_fnc))),s(s(s(s(s(s(s(sF1_fnc)))))))),true) = true,
inference(paramodulation,[status(thm)],[f415,f11]) ).
fof(f428,plain,
p(s(s(s(sF1_fnc))),s(s(s(s(s(s(s(sF1_fnc)))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f421]) ).
fof(f433,plain,
ifeq(true,true,p(s(s(s(sF1_fnc))),s(s(s(s(s(s(sF1_fnc))))))),true) = true,
inference(paramodulation,[status(thm)],[f428,f11]) ).
fof(f440,plain,
p(s(s(s(sF1_fnc))),s(s(s(s(s(s(sF1_fnc))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f433]) ).
fof(f445,plain,
ifeq(true,true,p(s(s(s(sF1_fnc))),s(s(s(s(s(sF1_fnc)))))),true) = true,
inference(paramodulation,[status(thm)],[f440,f11]) ).
fof(f452,plain,
p(s(s(s(sF1_fnc))),s(s(s(s(s(sF1_fnc)))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f445]) ).
fof(f457,plain,
ifeq(true,true,p(s(s(s(sF1_fnc))),s(s(s(s(sF1_fnc))))),true) = true,
inference(paramodulation,[status(thm)],[f452,f11]) ).
fof(f464,plain,
p(s(s(s(sF1_fnc))),s(s(s(s(sF1_fnc))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f457]) ).
fof(f469,plain,
ifeq(true,true,p(s(s(s(sF1_fnc))),s(s(s(sF1_fnc)))),true) = true,
inference(paramodulation,[status(thm)],[f464,f11]) ).
fof(f476,plain,
p(s(s(s(sF1_fnc))),s(s(s(sF1_fnc)))) = true,
inference(forward_demodulation,[status(thm)],[f7,f469]) ).
fof(f481,plain,
ifeq(true,true,p(s(s(s(sF1_fnc))),s(s(sF1_fnc))),true) = true,
inference(paramodulation,[status(thm)],[f476,f11]) ).
fof(f488,plain,
p(s(s(s(sF1_fnc))),s(s(sF1_fnc))) = true,
inference(forward_demodulation,[status(thm)],[f7,f481]) ).
fof(f493,plain,
ifeq(true,true,p(s(s(s(sF1_fnc))),s(sF1_fnc)),true) = true,
inference(paramodulation,[status(thm)],[f488,f11]) ).
fof(f500,plain,
p(s(s(s(sF1_fnc))),s(sF1_fnc)) = true,
inference(forward_demodulation,[status(thm)],[f7,f493]) ).
fof(f505,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(s(s(s(s(sF1_fnc))))))),true) = true,
inference(paramodulation,[status(thm)],[f215,f11]) ).
fof(f511,plain,
p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(s(s(s(s(sF1_fnc))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f505]) ).
fof(f517,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),s(s(s(s(sF1_fnc))))),true) = true,
inference(paramodulation,[status(thm)],[f227,f11]) ).
fof(f521,plain,
ifeq(p(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))),s(s(s(s(sF1_fnc))))),true,true,true) = true,
inference(paramodulation,[status(thm)],[f227,f9]) ).
fof(f523,plain,
p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),s(s(s(s(sF1_fnc))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f517]) ).
fof(f528,plain,
ifeq(true,true,p(s(s(s(sF1_fnc))),sF1_fnc),true) = true,
inference(paramodulation,[status(thm)],[f500,f11]) ).
fof(f535,plain,
p(s(s(s(sF1_fnc))),sF1_fnc) = true,
inference(forward_demodulation,[status(thm)],[f7,f528]) ).
fof(f540,plain,
ifeq(true,true,p(s(s(s(sF1_fnc))),n0),true) = true,
inference(paramodulation,[status(thm)],[f535,f52]) ).
fof(f546,plain,
p(s(s(s(sF1_fnc))),n0) = true,
inference(forward_demodulation,[status(thm)],[f7,f540]) ).
fof(f560,plain,
ifeq(true,true,p(s(s(s(s(s(sF1_fnc))))),s(s(s(s(s(s(s(sF1_fnc)))))))),true) = true,
inference(paramodulation,[status(thm)],[f381,f11]) ).
fof(f567,plain,
p(s(s(s(s(s(sF1_fnc))))),s(s(s(s(s(s(s(sF1_fnc)))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f560]) ).
fof(f573,plain,
ifeq(true,true,p(s(s(s(s(s(sF1_fnc))))),s(s(s(s(s(s(sF1_fnc))))))),true) = true,
inference(paramodulation,[status(thm)],[f567,f11]) ).
fof(f580,plain,
p(s(s(s(s(s(sF1_fnc))))),s(s(s(s(s(s(sF1_fnc))))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f573]) ).
fof(f586,plain,
ifeq(true,true,p(s(s(s(s(s(sF1_fnc))))),s(s(s(s(s(sF1_fnc)))))),true) = true,
inference(paramodulation,[status(thm)],[f580,f11]) ).
fof(f593,plain,
p(s(s(s(s(s(sF1_fnc))))),s(s(s(s(s(sF1_fnc)))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f586]) ).
fof(f598,plain,
ifeq(true,true,p(s(s(s(s(s(sF1_fnc))))),s(s(s(s(sF1_fnc))))),true) = true,
inference(paramodulation,[status(thm)],[f593,f11]) ).
fof(f605,plain,
p(s(s(s(s(s(sF1_fnc))))),s(s(s(s(sF1_fnc))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f598]) ).
fof(f610,plain,
ifeq(true,true,p(s(s(s(s(s(sF1_fnc))))),s(s(s(sF1_fnc)))),true) = true,
inference(paramodulation,[status(thm)],[f605,f11]) ).
fof(f617,plain,
p(s(s(s(s(s(sF1_fnc))))),s(s(s(sF1_fnc)))) = true,
inference(forward_demodulation,[status(thm)],[f7,f610]) ).
fof(f622,plain,
ifeq(true,true,p(s(s(s(s(s(sF1_fnc))))),s(s(sF1_fnc))),true) = true,
inference(paramodulation,[status(thm)],[f617,f11]) ).
fof(f629,plain,
p(s(s(s(s(s(sF1_fnc))))),s(s(sF1_fnc))) = true,
inference(forward_demodulation,[status(thm)],[f7,f622]) ).
fof(f634,plain,
ifeq(true,true,p(s(s(s(s(s(sF1_fnc))))),s(sF1_fnc)),true) = true,
inference(paramodulation,[status(thm)],[f629,f11]) ).
fof(f641,plain,
p(s(s(s(s(s(sF1_fnc))))),s(sF1_fnc)) = true,
inference(forward_demodulation,[status(thm)],[f7,f634]) ).
fof(f646,plain,
ifeq(true,true,p(s(s(s(s(s(sF1_fnc))))),sF1_fnc),true) = true,
inference(paramodulation,[status(thm)],[f641,f11]) ).
fof(f653,plain,
p(s(s(s(s(s(sF1_fnc))))),sF1_fnc) = true,
inference(forward_demodulation,[status(thm)],[f7,f646]) ).
fof(f658,plain,
ifeq(true,true,p(s(s(s(s(s(sF1_fnc))))),n0),true) = true,
inference(paramodulation,[status(thm)],[f653,f52]) ).
fof(f664,plain,
p(s(s(s(s(s(sF1_fnc))))),n0) = true,
inference(forward_demodulation,[status(thm)],[f7,f658]) ).
fof(f668,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(s(s(s(sF1_fnc)))))),true) = true,
inference(paramodulation,[status(thm)],[f511,f11]) ).
fof(f675,plain,
p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(s(s(s(sF1_fnc)))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f668]) ).
fof(f681,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),s(s(s(sF1_fnc)))),true) = true,
inference(paramodulation,[status(thm)],[f523,f11]) ).
fof(f685,plain,
ifeq(p(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))),s(s(s(sF1_fnc)))),true,true,true) = true,
inference(paramodulation,[status(thm)],[f523,f9]) ).
fof(f687,plain,
p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),s(s(s(sF1_fnc)))) = true,
inference(forward_demodulation,[status(thm)],[f7,f681]) ).
fof(f702,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(s(s(sF1_fnc))))),true) = true,
inference(paramodulation,[status(thm)],[f675,f11]) ).
fof(f709,plain,
p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(s(s(sF1_fnc))))) = true,
inference(forward_demodulation,[status(thm)],[f7,f702]) ).
fof(f715,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(s(sF1_fnc)))),true) = true,
inference(paramodulation,[status(thm)],[f709,f11]) ).
fof(f722,plain,
p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(s(sF1_fnc)))) = true,
inference(forward_demodulation,[status(thm)],[f7,f715]) ).
fof(f728,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(sF1_fnc))),true) = true,
inference(paramodulation,[status(thm)],[f722,f11]) ).
fof(f735,plain,
p(s(s(s(s(s(s(s(sF1_fnc))))))),s(s(sF1_fnc))) = true,
inference(forward_demodulation,[status(thm)],[f7,f728]) ).
fof(f740,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(sF1_fnc))))))),s(sF1_fnc)),true) = true,
inference(paramodulation,[status(thm)],[f735,f11]) ).
fof(f747,plain,
p(s(s(s(s(s(s(s(sF1_fnc))))))),s(sF1_fnc)) = true,
inference(forward_demodulation,[status(thm)],[f7,f740]) ).
fof(f752,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(sF1_fnc))))))),sF1_fnc),true) = true,
inference(paramodulation,[status(thm)],[f747,f11]) ).
fof(f759,plain,
p(s(s(s(s(s(s(s(sF1_fnc))))))),sF1_fnc) = true,
inference(forward_demodulation,[status(thm)],[f7,f752]) ).
fof(f764,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(sF1_fnc))))))),n0),true) = true,
inference(paramodulation,[status(thm)],[f759,f52]) ).
fof(f770,plain,
p(s(s(s(s(s(s(s(sF1_fnc))))))),n0) = true,
inference(forward_demodulation,[status(thm)],[f7,f764]) ).
fof(f784,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),s(s(sF1_fnc))),true) = true,
inference(paramodulation,[status(thm)],[f687,f11]) ).
fof(f788,plain,
ifeq(p(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))),s(s(sF1_fnc))),true,true,true) = true,
inference(paramodulation,[status(thm)],[f687,f9]) ).
fof(f791,plain,
p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),s(s(sF1_fnc))) = true,
inference(forward_demodulation,[status(thm)],[f7,f784]) ).
fof(f796,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),s(sF1_fnc)),true) = true,
inference(paramodulation,[status(thm)],[f791,f11]) ).
fof(f800,plain,
ifeq(p(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))),s(sF1_fnc)),true,true,true) = true,
inference(paramodulation,[status(thm)],[f791,f9]) ).
fof(f803,plain,
p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),s(sF1_fnc)) = true,
inference(forward_demodulation,[status(thm)],[f7,f796]) ).
fof(f808,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),sF1_fnc),true) = true,
inference(paramodulation,[status(thm)],[f803,f11]) ).
fof(f812,plain,
ifeq(p(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))),sF1_fnc),true,true,true) = true,
inference(paramodulation,[status(thm)],[f803,f9]) ).
fof(f815,plain,
p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),sF1_fnc) = true,
inference(forward_demodulation,[status(thm)],[f7,f808]) ).
fof(f820,plain,
ifeq(true,true,p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),n0),true) = true,
inference(paramodulation,[status(thm)],[f815,f52]) ).
fof(f823,plain,
ifeq(p(s(s(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))))),n0),true,true,true) = true,
inference(paramodulation,[status(thm)],[f815,f21]) ).
fof(f826,plain,
p(s(s(s(s(s(s(s(s(s(sF1_fnc))))))))),n0) = true,
inference(forward_demodulation,[status(thm)],[f7,f820]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ054-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n011.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 03:47:10 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.15/0.37 % Drodi V4.1.1
% 0.15/0.38 % SZS status Satisfiable for theBenchmark: Theory is satisfiable
% 0.15/0.38 % SZS output start Saturation for theBenchmark
% See solution above
% 0.15/0.41 % Elapsed time: 0.035241 seconds
% 0.15/0.41 % CPU time: 0.076967 seconds
% 0.15/0.41 % Total memory used: 4.551 MB
% 0.15/0.41 % Net memory used: 4.531 MB
%------------------------------------------------------------------------------