%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN598-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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 03:16:53 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.61s
% Output : CNFRefutation 1.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 30
% Syntax : Number of formulae : 93 ( 93 unt; 20 def)
% Number of atoms : 93 ( 92 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 39 ( 39 usr; 24 con; 0-4 aty)
% Number of variables : 82 ( 82 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C] : ifeq(A,A,B,C) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,negated_conjecture,
p18(c21) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,negated_conjecture,
! [X34] : p7(X34,X34) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,negated_conjecture,
p3(f4(f6(c21)),c22) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
! [X34,X36,X35] : ifeq(p7(X34,X36),true,ifeq(p7(X34,X35),true,p7(X35,X36),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
! [X6,X7,X5,X4] : ifeq(p19(X6,X7),true,ifeq(p7(X7,X5),true,ifeq(p7(X6,X4),true,p19(X4,X5),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,negated_conjecture,
! [X42,X44,X41,X43] : ifeq(p3(X42,X44),true,ifeq(p7(X41,X43),true,p7(f11(X41,X42),f11(X43,X44)),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,negated_conjecture,
! [X38,X40,X37,X39] : ifeq(p7(X38,X40),true,ifeq(p7(X37,X39),true,p7(f10(X37,X38),f10(X39,X40)),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,negated_conjecture,
p19(f10(f11(f14(f12(f15(f13(c23)))),c22),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(c21))) != true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,negated_conjecture,
! [X8] : ifeq(p18(X8),true,p19(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(X8))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(X8))),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,plain,
! [X0,X1,X2] : ifeq(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f33,plain,
p18(c21) = true,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f34,plain,
! [X0] : p7(X0,X0) = true,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f38,plain,
p3(f4(f6(c21)),c22) = true,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f51,plain,
! [X0,X1,X2] : ifeq(p7(X0,X1),true,ifeq(p7(X0,X2),true,p7(X2,X1),true),true) = true,
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f54,plain,
! [X0,X1,X2,X3] : ifeq(p19(X0,X1),true,ifeq(p7(X1,X2),true,ifeq(p7(X0,X3),true,p19(X3,X2),true),true),true) = true,
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f56,plain,
! [X0,X1,X2,X3] : ifeq(p3(X0,X1),true,ifeq(p7(X2,X3),true,p7(f11(X2,X0),f11(X3,X1)),true),true) = true,
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f57,plain,
! [X0,X1,X2,X3] : ifeq(p7(X0,X1),true,ifeq(p7(X2,X3),true,p7(f10(X2,X0),f10(X3,X1)),true),true) = true,
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f58,plain,
p19(f10(f11(f14(f12(f15(f13(c23)))),c22),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(c21))) != true,
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f59,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(f14(f12(f15(f13(c23)))),f4(f6(X0))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(X0))),true) = true,
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f61,definition,
sF6_fnc = f13(c23),
introduced(definition,[new_symbols(definition,[sF6_fnc])],[function_definition]) ).
fof(f62,definition,
sF5_fnc = f15(sF6_fnc),
introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition]) ).
fof(f63,definition,
sF4_fnc = f12(sF5_fnc),
introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition]) ).
fof(f64,definition,
sF3_fnc = f14(sF4_fnc),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f65,definition,
sF2_fnc = f11(sF3_fnc,c22),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f66,definition,
sF10_fnc = f15(sF6_fnc),
introduced(definition,[new_symbols(definition,[sF10_fnc])],[function_definition]) ).
fof(f67,definition,
sF9_fnc = f12(sF10_fnc),
introduced(definition,[new_symbols(definition,[sF9_fnc])],[function_definition]) ).
fof(f68,definition,
sF8_fnc = f14(sF9_fnc),
introduced(definition,[new_symbols(definition,[sF8_fnc])],[function_definition]) ).
fof(f69,definition,
sF17_fnc = f13(sF6_fnc),
introduced(definition,[new_symbols(definition,[sF17_fnc])],[function_definition]) ).
fof(f70,definition,
sF16_fnc = f13(sF17_fnc),
introduced(definition,[new_symbols(definition,[sF16_fnc])],[function_definition]) ).
fof(f71,definition,
sF15_fnc = f13(sF16_fnc),
introduced(definition,[new_symbols(definition,[sF15_fnc])],[function_definition]) ).
fof(f72,definition,
sF14_fnc = f13(sF15_fnc),
introduced(definition,[new_symbols(definition,[sF14_fnc])],[function_definition]) ).
fof(f73,definition,
sF13_fnc = f13(sF14_fnc),
introduced(definition,[new_symbols(definition,[sF13_fnc])],[function_definition]) ).
fof(f74,definition,
sF12_fnc = f13(sF13_fnc),
introduced(definition,[new_symbols(definition,[sF12_fnc])],[function_definition]) ).
fof(f75,definition,
sF11_fnc = f12(sF12_fnc),
introduced(definition,[new_symbols(definition,[sF11_fnc])],[function_definition]) ).
fof(f76,definition,
sF7_fnc = f11(sF8_fnc,sF11_fnc),
introduced(definition,[new_symbols(definition,[sF7_fnc])],[function_definition]) ).
fof(f77,definition,
sF1_fnc = f10(sF2_fnc,sF7_fnc),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f78,definition,
sF19_fnc = f9(c21),
introduced(definition,[new_symbols(definition,[sF19_fnc])],[function_definition]) ).
fof(f79,definition,
sF18_fnc = f8(sF19_fnc),
introduced(definition,[new_symbols(definition,[sF18_fnc])],[function_definition]) ).
fof(f80,definition,
sF0_fnc = p19(sF1_fnc,sF18_fnc),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f81,plain,
sF0_fnc != true,
inference(definition_folding,[],[f58,f80,f79,f78,f77,f76,f75,f74,f73,f72,f71,f70,f69,f68,f67,f66,f65,f64,f63,f62,f61]) ).
fof(f82,plain,
sF4_fnc = f12(sF10_fnc),
inference(backward_demodulation,[status(thm)],[f84,f63]) ).
fof(f83,plain,
sF10_fnc = f15(sF6_fnc),
inference(backward_demodulation,[status(thm)],[f84,f62]) ).
fof(f84,plain,
sF10_fnc = sF5_fnc,
inference(forward_demodulation,[status(thm)],[f62,f66]) ).
fof(f85,plain,
sF3_fnc = f14(sF9_fnc),
inference(backward_demodulation,[status(thm)],[f86,f64]) ).
fof(f86,plain,
sF4_fnc = sF9_fnc,
inference(forward_demodulation,[status(thm)],[f67,f82]) ).
fof(f87,plain,
sF3_fnc = sF8_fnc,
inference(forward_demodulation,[status(thm)],[f68,f85]) ).
fof(f104,plain,
sF2_fnc = f11(sF8_fnc,c22),
inference(forward_demodulation,[status(thm)],[f87,f65]) ).
fof(f282,plain,
! [X0,X1] : ifeq(true,true,ifeq(p7(X0,X1),true,p7(X1,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f34,f51]) ).
fof(f289,plain,
! [X0,X1] : ifeq(p7(X0,X1),true,p7(X1,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f31,f282]) ).
fof(f523,plain,
! [X0,X1,X2] : ifeq(p19(X0,X1),true,ifeq(true,true,ifeq(p7(X0,X2),true,p19(X2,X1),true),true),true) = true,
inference(paramodulation,[status(thm)],[f34,f54]) ).
fof(f530,plain,
! [X0,X1,X2] : ifeq(p19(X0,X1),true,ifeq(p7(X0,X2),true,p19(X2,X1),true),true) = true,
inference(forward_demodulation,[status(thm)],[f31,f523]) ).
fof(f620,plain,
! [X0,X1] : ifeq(true,true,ifeq(p7(X0,X1),true,p7(f11(X0,f4(f6(c21))),f11(X1,c22)),true),true) = true,
inference(paramodulation,[status(thm)],[f38,f56]) ).
fof(f639,plain,
! [X0,X1] : ifeq(p7(X0,X1),true,p7(f11(X0,f4(f6(c21))),f11(X1,c22)),true) = true,
inference(forward_demodulation,[status(thm)],[f31,f620]) ).
fof(f649,plain,
! [X0,X1,X2] : ifeq(true,true,ifeq(p7(X0,X1),true,p7(f10(X0,X2),f10(X1,X2)),true),true) = true,
inference(paramodulation,[status(thm)],[f34,f57]) ).
fof(f658,plain,
! [X0,X1,X2] : ifeq(p7(X0,X1),true,p7(f10(X0,X2),f10(X1,X2)),true) = true,
inference(forward_demodulation,[status(thm)],[f31,f649]) ).
fof(f665,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(f14(f12(f15(sF6_fnc))),f4(f6(X0))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f61,f59]) ).
fof(f666,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(f14(f12(sF10_fnc)),f4(f6(X0))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f83,f665]) ).
fof(f667,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(f14(sF9_fnc),f4(f6(X0))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f67,f666]) ).
fof(f668,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(sF8_fnc,f4(f6(X0))),f11(f14(f12(f15(f13(c23)))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f68,f667]) ).
fof(f669,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(sF8_fnc,f4(f6(X0))),f11(f14(f12(f15(sF6_fnc))),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f61,f668]) ).
fof(f670,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(sF8_fnc,f4(f6(X0))),f11(f14(f12(sF10_fnc)),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f83,f669]) ).
fof(f671,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(sF8_fnc,f4(f6(X0))),f11(f14(sF9_fnc),f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f67,f670]) ).
fof(f672,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(sF8_fnc,f4(f6(X0))),f11(sF8_fnc,f12(f13(f13(f13(f13(f13(f13(f13(c23)))))))))),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f68,f671]) ).
fof(f673,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(sF8_fnc,f4(f6(X0))),f11(sF8_fnc,f12(f13(f13(f13(f13(f13(f13(sF6_fnc))))))))),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f61,f672]) ).
fof(f674,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(sF8_fnc,f4(f6(X0))),f11(sF8_fnc,f12(f13(f13(f13(f13(f13(sF17_fnc)))))))),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f69,f673]) ).
fof(f675,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(sF8_fnc,f4(f6(X0))),f11(sF8_fnc,f12(f13(f13(f13(f13(sF16_fnc))))))),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f70,f674]) ).
fof(f676,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(sF8_fnc,f4(f6(X0))),f11(sF8_fnc,f12(f13(f13(f13(sF15_fnc)))))),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f71,f675]) ).
fof(f677,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(sF8_fnc,f4(f6(X0))),f11(sF8_fnc,f12(f13(f13(sF14_fnc))))),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f72,f676]) ).
fof(f678,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(sF8_fnc,f4(f6(X0))),f11(sF8_fnc,f12(f13(sF13_fnc)))),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f73,f677]) ).
fof(f679,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(sF8_fnc,f4(f6(X0))),f11(sF8_fnc,f12(sF12_fnc))),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f74,f678]) ).
fof(f680,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(sF8_fnc,f4(f6(X0))),f11(sF8_fnc,sF11_fnc)),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f75,f679]) ).
fof(f681,plain,
! [X0] : ifeq(p18(X0),true,p19(f10(f11(sF8_fnc,f4(f6(X0))),sF7_fnc),f8(f9(X0))),true) = true,
inference(forward_demodulation,[status(thm)],[f76,f680]) ).
fof(f682,plain,
ifeq(true,true,p19(f10(f11(sF8_fnc,f4(f6(c21))),sF7_fnc),f8(f9(c21))),true) = true,
inference(paramodulation,[status(thm)],[f33,f681]) ).
fof(f684,plain,
p19(f10(f11(sF8_fnc,f4(f6(c21))),sF7_fnc),f8(f9(c21))) = true,
inference(forward_demodulation,[status(thm)],[f31,f682]) ).
fof(f685,plain,
p19(f10(f11(sF8_fnc,f4(f6(c21))),sF7_fnc),f8(sF19_fnc)) = true,
inference(forward_demodulation,[status(thm)],[f78,f684]) ).
fof(f686,plain,
p19(f10(f11(sF8_fnc,f4(f6(c21))),sF7_fnc),sF18_fnc) = true,
inference(forward_demodulation,[status(thm)],[f79,f685]) ).
fof(f2531,plain,
! [X0] : ifeq(p19(X0,sF18_fnc),true,ifeq(p7(X0,sF1_fnc),true,sF0_fnc,true),true) = true,
inference(paramodulation,[status(thm)],[f80,f530]) ).
fof(f2676,plain,
! [X0] : ifeq(true,true,p7(f11(X0,f4(f6(c21))),f11(X0,c22)),true) = true,
inference(paramodulation,[status(thm)],[f34,f639]) ).
fof(f2692,plain,
! [X0] : p7(f11(X0,f4(f6(c21))),f11(X0,c22)) = true,
inference(forward_demodulation,[status(thm)],[f31,f2676]) ).
fof(f2729,plain,
p7(f11(sF8_fnc,f4(f6(c21))),sF2_fnc) = true,
inference(paramodulation,[status(thm)],[f104,f2692]) ).
fof(f2800,plain,
ifeq(true,true,p7(sF2_fnc,f11(sF8_fnc,f4(f6(c21)))),true) = true,
inference(paramodulation,[status(thm)],[f2729,f289]) ).
fof(f2824,plain,
p7(sF2_fnc,f11(sF8_fnc,f4(f6(c21)))) = true,
inference(forward_demodulation,[status(thm)],[f31,f2800]) ).
fof(f3086,plain,
! [X0] : ifeq(true,true,p7(f10(sF2_fnc,X0),f10(f11(sF8_fnc,f4(f6(c21))),X0)),true) = true,
inference(paramodulation,[status(thm)],[f2824,f658]) ).
fof(f3108,plain,
! [X0] : p7(f10(sF2_fnc,X0),f10(f11(sF8_fnc,f4(f6(c21))),X0)) = true,
inference(forward_demodulation,[status(thm)],[f31,f3086]) ).
fof(f4508,plain,
p7(sF1_fnc,f10(f11(sF8_fnc,f4(f6(c21))),sF7_fnc)) = true,
inference(paramodulation,[status(thm)],[f77,f3108]) ).
fof(f4593,plain,
ifeq(true,true,p7(f10(f11(sF8_fnc,f4(f6(c21))),sF7_fnc),sF1_fnc),true) = true,
inference(paramodulation,[status(thm)],[f4508,f289]) ).
fof(f4625,plain,
p7(f10(f11(sF8_fnc,f4(f6(c21))),sF7_fnc),sF1_fnc) = true,
inference(forward_demodulation,[status(thm)],[f31,f4593]) ).
fof(f7025,plain,
ifeq(true,true,ifeq(p7(f10(f11(sF8_fnc,f4(f6(c21))),sF7_fnc),sF1_fnc),true,sF0_fnc,true),true) = true,
inference(paramodulation,[status(thm)],[f686,f2531]) ).
fof(f7029,plain,
ifeq(p7(f10(f11(sF8_fnc,f4(f6(c21))),sF7_fnc),sF1_fnc),true,sF0_fnc,true) = true,
inference(forward_demodulation,[status(thm)],[f31,f7025]) ).
fof(f7030,plain,
ifeq(true,true,sF0_fnc,true) = true,
inference(forward_demodulation,[status(thm)],[f4625,f7029]) ).
fof(f7031,plain,
sF0_fnc = true,
inference(forward_demodulation,[status(thm)],[f31,f7030]) ).
fof(f7032,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f7031,f81]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN598-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n018.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 : Mon Sep 21 11:11:29 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.13/0.61 % Refutation found
% 0.13/0.61 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.61 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 81.10/16.85 % Elapsed time: 16.493300 seconds
% 81.10/16.85 % CPU time: 99.122743 seconds
% 81.10/16.85 % Total memory used: 44.928 GB
% 81.10/16.85 % Net memory used: 44.928 GB
%------------------------------------------------------------------------------