%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN672-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n002.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 : Fri Sep 25 03:35:27 PM UTC 2026
% Result : Unsatisfiable 40.18s 5.54s
% Output : Proof 40.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 12
% Syntax : Number of formulae : 90 ( 74 unt; 0 def)
% Number of atoms : 122 ( 50 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 70 ( 38 ~; 32 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 11 con; 0-4 aty)
% Number of variables : 143 ( 2 sgn 32 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f38,negated_conjecture,
( ~ p3(X84,X83)
| ~ p9(X85,X82)
| ~ p30(X85,X84)
| p30(X82,X83) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p30_39) ).
fof(f38_nnf,plain,
! [X82,X83,X85,X84] :
( ~ p3(X84,X83)
| ~ p9(X85,X82)
| ~ p30(X85,X84)
| p30(X82,X83) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [X82,X83,X85,X84] :
( ~ p3(X84,X83)
| ~ p9(X85,X82)
| ~ p30(X85,X84)
| p30(X82,X83) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c38,plain,
( ~ p3(X3,X1)
| ~ p9(X2,X0)
| ~ p30(X2,X3)
| p30(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(t57,plain,
ifeq(p30(X1,X2),true,ifeq(p9(X1,X3),true,ifeq(p3(X2,X4),true,p30(X3,X4),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c38]) ).
cnf(t77,plain,
ifeq(p30(X1,X2),true,ifeq(p9(X1,X3),true,ifeq(p3(X2,X4),true,p30(X3,X4),true),true),true) = true,
inference(orient,[status(thm)],[t57]) ).
cnf(f5,negated_conjecture,
p3(X62,X62),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_6) ).
fof(f5_nnf,plain,
! [X62] : p3(X62,X62),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X62] : p3(X62,X62),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
p3(X0,X0),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t16,plain,
p3(X1,X1) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t98,plain,
p3(X1,X1) = true,
inference(orient,[status(thm)],[t16]) ).
cnf(t105,plain,
true = ifeq(p30(X1,X2),true,ifeq(p9(X1,X3),true,ifeq(true,true,p30(X3,X2),true),true),true),
inference(cp,[status(thm)],[t77,t98]) ).
cnf(t21,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t61,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t21]) ).
cnf(t814,plain,
true = ifeq(p30(X1,X2),true,ifeq(p9(X1,X3),true,p30(X3,X2),true),true),
inference(step,[status(thm)],[t105,t61]) ).
cnf(t353,plain,
ifeq(p30(X1,X2),true,ifeq(p9(X1,X3),true,p30(X3,X2),true),true) = true,
inference(orient,[status(thm)],[t814]) ).
cnf(f41,negated_conjecture,
( ~ p8(X108,X110)
| ~ p3(X109,X111)
| p9(f10(X108,X109),f10(X110,X111)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p9_42) ).
fof(f41_nnf,plain,
! [X108,X109,X110,X111] :
( ~ p8(X108,X110)
| ~ p3(X109,X111)
| p9(f10(X108,X109),f10(X110,X111)) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [X108,X109,X110,X111] :
( ~ p8(X108,X110)
| ~ p3(X109,X111)
| p9(f10(X108,X109),f10(X110,X111)) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c41,plain,
( ~ p8(X0,X2)
| ~ p3(X1,X3)
| p9(f10(X0,X1),f10(X2,X3)) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(t54,plain,
ifeq(p3(X1,X2),true,ifeq(p8(X3,X4),true,p9(f10(X3,X1),f10(X4,X2)),true),true) = true,
inference(equality_encoding,[status(esa)],[c41]) ).
cnf(t65,plain,
ifeq(p3(X1,X2),true,ifeq(p8(X3,X4),true,p9(f10(X3,X1),f10(X4,X2)),true),true) = true,
inference(orient,[status(thm)],[t54]) ).
cnf(f2,negated_conjecture,
p8(X98,X98),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p8_3) ).
fof(f2_nnf,plain,
! [X98] : p8(X98,X98),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X98] : p8(X98,X98),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
p8(X0,X0),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t19,plain,
p8(X1,X1) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t148,plain,
p8(X1,X1) = true,
inference(orient,[status(thm)],[t19]) ).
cnf(t152,plain,
true = ifeq(p3(X1,X2),true,ifeq(true,true,p9(f10(X3,X1),f10(X3,X2)),true),true),
inference(cp,[status(thm)],[t65,t148]) ).
cnf(t802,plain,
true = ifeq(p3(X1,X2),true,p9(f10(X3,X1),f10(X3,X2)),true),
inference(step,[status(thm)],[t152,t61]) ).
cnf(t318,plain,
ifeq(p3(X1,X2),true,p9(f10(X3,X1),f10(X3,X2)),true) = true,
inference(orient,[status(thm)],[t802]) ).
cnf(f36,negated_conjecture,
p3(f4(f7(c34,X77),f14(c38,X78)),f14(X77,X78)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_37) ).
fof(f36_nnf,plain,
! [X77,X78] : p3(f4(f7(c34,X77),f14(c38,X78)),f14(X77,X78)),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [X77,X78] : p3(f4(f7(c34,X77),f14(c38,X78)),f14(X77,X78)),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
p3(f4(f7(c34,X0),f14(c38,X1)),f14(X0,X1)),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(t25,plain,
p3(f4(f7(c34,X1),f14(c38,X2)),f14(X1,X2)) = true,
inference(equality_encoding,[status(esa)],[c36]) ).
cnf(t110,plain,
p3(f4(f7(c34,X1),f14(c38,X2)),f14(X1,X2)) = true,
inference(orient,[status(thm)],[t25]) ).
cnf(t321,plain,
true = ifeq(true,true,p9(f10(X1,f4(f7(c34,X2),f14(c38,X3))),f10(X1,f14(X2,X3))),true),
inference(cp,[status(thm)],[t318,t110]) ).
cnf(t827,plain,
true = p9(f10(X1,f4(f7(c34,X2),f14(c38,X3))),f10(X1,f14(X2,X3))),
inference(step,[status(thm)],[t321,t61]) ).
cnf(t422,plain,
p9(f10(X1,f4(f7(c34,X2),f14(c38,X3))),f10(X1,f14(X2,X3))) = true,
inference(orient,[status(thm)],[t827]) ).
cnf(t423,plain,
true = ifeq(p30(f10(X1,f4(f7(c34,X2),f14(c38,X3))),X4),true,ifeq(true,true,p30(f10(X1,f14(X2,X3)),X4),true),true),
inference(cp,[status(thm)],[t353,t422]) ).
cnf(t881,plain,
true = ifeq(p30(f10(X1,f4(f7(c34,X2),f14(c38,X3))),X4),true,p30(f10(X1,f14(X2,X3)),X4),true),
inference(step,[status(thm)],[t423,t61]) ).
cnf(t724,plain,
ifeq(p30(f10(X1,f4(f7(c34,X2),f14(c38,X3))),X4),true,p30(f10(X1,f14(X2,X3)),X4),true) = true,
inference(orient,[status(thm)],[t881]) ).
cnf(f53,negated_conjecture,
( ~ p30(f10(f12(c32,c33),X86),X87)
| p30(f10(f12(c32,c33),f4(f7(c34,c35),X86)),f4(f7(c34,c35),X87)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p30_54) ).
fof(f53_nnf,plain,
! [X86,X87] :
( ~ p30(f10(f12(c32,c33),X86),X87)
| p30(f10(f12(c32,c33),f4(f7(c34,c35),X86)),f4(f7(c34,c35),X87)) ),
inference(nnf_transformation,[status(thm)],[f53]) ).
fof(f53_sk,plain,
! [X86,X87] :
( ~ p30(f10(f12(c32,c33),X86),X87)
| p30(f10(f12(c32,c33),f4(f7(c34,c35),X86)),f4(f7(c34,c35),X87)) ),
inference(skolemisation,[status(esa)],[f53_nnf]) ).
cnf(c53,plain,
( ~ p30(f10(f12(c32,c33),X0),X1)
| p30(f10(f12(c32,c33),f4(f7(c34,c35),X0)),f4(f7(c34,c35),X1)) ),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
cnf(t59,plain,
ifeq(p30(f10(f12(c32,c33),X1),X2),true,p30(f10(f12(c32,c33),f4(f7(c34,c35),X1)),f4(f7(c34,c35),X2)),true) = true,
inference(equality_encoding,[status(esa)],[c53]) ).
cnf(t78,plain,
ifeq(p30(f10(f12(c32,c33),X1),X2),true,p30(f10(f12(c32,c33),f4(f7(c34,c35),X1)),f4(f7(c34,c35),X2)),true) = true,
inference(orient,[status(thm)],[t59]) ).
cnf(f52,negated_conjecture,
( ~ p31(f20(c36,X61),f17(c37,X60))
| p30(f10(f12(c32,c33),f14(c38,X61)),X60)
| p3(X60,f14(c38,X61)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_53) ).
fof(f52_nnf,plain,
! [X60,X61] :
( ~ p31(f20(c36,X61),f17(c37,X60))
| p30(f10(f12(c32,c33),f14(c38,X61)),X60)
| p3(X60,f14(c38,X61)) ),
inference(nnf_transformation,[status(thm)],[f52]) ).
fof(f52_sk,plain,
! [X60,X61] :
( ~ p31(f20(c36,X61),f17(c37,X60))
| p30(f10(f12(c32,c33),f14(c38,X61)),X60)
| p3(X60,f14(c38,X61)) ),
inference(skolemisation,[status(esa)],[f52_nnf]) ).
cnf(c52,plain,
( ~ p31(f20(c36,X1),f17(c37,X0))
| p30(f10(f12(c32,c33),f14(c38,X1)),X0)
| p3(X0,f14(c38,X1)) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(t60,plain,
ifeq(p31(f20(c36,X1),f17(c37,X2)),true,or(p3(X2,f14(c38,X1)),p30(f10(f12(c32,c33),f14(c38,X1)),X2)),true) = true,
inference(equality_encoding,[status(esa)],[c52]) ).
cnf(t97,plain,
ifeq(p31(f20(c36,X1),f17(c37,X2)),true,or(p3(X2,f14(c38,X1)),p30(f10(f12(c32,c33),f14(c38,X1)),X2)),true) = true,
inference(orient,[status(thm)],[t60]) ).
cnf(f17,negated_conjecture,
~ p3(c40,f14(c38,c39)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p3_18) ).
fof(f17_nnf,plain,
~ p3(c40,f14(c38,c39)),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
~ p3(c40,f14(c38,c39)),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
~ p3(c40,f14(c38,c39)),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(t22,plain,
p3(c40,f14(c38,c39)) = false,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t226,plain,
p3(c40,f14(c38,c39)) = false,
inference(orient,[status(thm)],[t22]) ).
cnf(t234,plain,
true = ifeq(p31(f20(c36,c39),f17(c37,c40)),true,or(false,p30(f10(f12(c32,c33),f14(c38,c39)),c40)),true),
inference(cp,[status(thm)],[t97,t226]) ).
cnf(f18,negated_conjecture,
p31(f20(c36,c39),f17(c37,c40)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p31_19) ).
fof(f18_nnf,plain,
p31(f20(c36,c39),f17(c37,c40)),
inference(nnf_transformation,[status(thm)],[f18]) ).
cnf(c18,plain,
p31(f20(c36,c39),f17(c37,c40)),
inference(cnf_transformation,[status(esa)],[f18_nnf]) ).
cnf(t23,plain,
p31(f20(c36,c39),f17(c37,c40)) = true,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t222,plain,
p31(f20(c36,c39),f17(c37,c40)) = true,
inference(orient,[status(thm)],[t23]) ).
cnf(t787,plain,
true = ifeq(true,true,or(false,p30(f10(f12(c32,c33),f14(c38,c39)),c40)),true),
inference(step,[status(thm)],[t234,t222]) ).
cnf(t788,plain,
true = or(false,p30(f10(f12(c32,c33),f14(c38,c39)),c40)),
inference(step,[status(thm)],[t787,t61]) ).
cnf(t2,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t63,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t789,plain,
true = p30(f10(f12(c32,c33),f14(c38,c39)),c40),
inference(step,[status(thm)],[t788,t63]) ).
cnf(t282,plain,
p30(f10(f12(c32,c33),f14(c38,c39)),c40) = true,
inference(orient,[status(thm)],[t789]) ).
cnf(t285,plain,
true = ifeq(true,true,p30(f10(f12(c32,c33),f4(f7(c34,c35),f14(c38,c39))),f4(f7(c34,c35),c40)),true),
inference(cp,[status(thm)],[t78,t282]) ).
cnf(t837,plain,
true = p30(f10(f12(c32,c33),f4(f7(c34,c35),f14(c38,c39))),f4(f7(c34,c35),c40)),
inference(step,[status(thm)],[t285,t61]) ).
cnf(t492,plain,
p30(f10(f12(c32,c33),f4(f7(c34,c35),f14(c38,c39))),f4(f7(c34,c35),c40)) = true,
inference(orient,[status(thm)],[t837]) ).
cnf(t725,plain,
true = ifeq(true,true,p30(f10(f12(c32,c33),f14(c35,c39)),f4(f7(c34,c35),c40)),true),
inference(cp,[status(thm)],[t724,t492]) ).
cnf(t882,plain,
true = p30(f10(f12(c32,c33),f14(c35,c39)),f4(f7(c34,c35),c40)),
inference(step,[status(thm)],[t725,t61]) ).
cnf(f39,negated_conjecture,
~ p30(f10(f12(c32,c33),f14(c35,c39)),f4(f7(c34,c35),c40)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p30_40) ).
fof(f39_nnf,plain,
~ p30(f10(f12(c32,c33),f14(c35,c39)),f4(f7(c34,c35),c40)),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
~ p30(f10(f12(c32,c33),f14(c35,c39)),f4(f7(c34,c35),c40)),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
~ p30(f10(f12(c32,c33),f14(c35,c39)),f4(f7(c34,c35),c40)),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(t26,plain,
p30(f10(f12(c32,c33),f14(c35,c39)),f4(f7(c34,c35),c40)) = false,
inference(equality_encoding,[status(esa)],[c39]) ).
cnf(t236,plain,
p30(f10(f12(c32,c33),f14(c35,c39)),f4(f7(c34,c35),c40)) = false,
inference(orient,[status(thm)],[t26]) ).
cnf(t883,plain,
true = false,
inference(step,[status(thm)],[t882,t236]) ).
cnf(t727,plain,
false = true,
inference(orient,[status(thm)],[t883]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c17,c39]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t727]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN672-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.35 % Computer : n002.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 02:05:04 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 40.18/5.54 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 40.18/5.54 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------