%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN617-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 : 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 : Fri Sep 25 03:35:20 PM UTC 2026
% Result : Unsatisfiable 6.11s 1.27s
% Output : Proof 6.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 10
% Syntax : Number of formulae : 63 ( 51 unt; 0 def)
% Number of atoms : 83 ( 23 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 46 ( 26 ~; 20 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-4 aty)
% Number of variables : 80 ( 3 sgn 32 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f23,negated_conjecture,
( ~ p13(X11,X13)
| ~ p13(X11,X12)
| p13(X12,X13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p13_24) ).
fof(f23_nnf,plain,
! [X12,X13,X11] :
( ~ p13(X11,X13)
| ~ p13(X11,X12)
| p13(X12,X13) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [X12,X13,X11] :
( ~ p13(X11,X13)
| ~ p13(X11,X12)
| p13(X12,X13) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( ~ p13(X2,X1)
| ~ p13(X2,X0)
| p13(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(hi23,negated_conjecture,
ifeq(p13(X0,X1),true,ifeq(p13(X0,X2),true,p13(X1,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(f18,negated_conjecture,
p13(f15(f3(X18),X19),f15(X18,f12(X19))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p13_19) ).
fof(f18_nnf,plain,
! [X18,X19] : p13(f15(f3(X18),X19),f15(X18,f12(X19))),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [X18,X19] : p13(f15(f3(X18),X19),f15(X18,f12(X19))),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
p13(f15(f3(X0),X1),f15(X0,f12(X1))),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(hi18,negated_conjecture,
p13(f15(f3(X0),X1),f15(X0,f12(X1))) = true,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(f4,negated_conjecture,
p13(X11,X11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p13_5) ).
fof(f4_nnf,plain,
! [X11] : p13(X11,X11),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X11] : p13(X11,X11),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
p13(X0,X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(hi4,negated_conjecture,
p13(X0,X0) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(h7,plain,
p13(f15(f4(f4(c22,f5(f6(c20))),c21),f12(f14(c23,c24))),f15(f3(f4(f4(c22,f5(f6(c20))),c21)),f14(c23,c24))) = true,
inference(hyper_resolution,[status(thm)],[hi23,hi18,hi4]) ).
cnf(f3,negated_conjecture,
p2(X27,X27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_4) ).
fof(f3_nnf,plain,
! [X27] : p2(X27,X27),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X27] : p2(X27,X27),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
p2(X0,X0),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(hi3,negated_conjecture,
p2(X0,X0) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(h1,plain,
p2(f4(f4(c22,f5(f6(c20))),c21),f4(f4(c22,f5(f6(c20))),c21)) = true,
inference(hyper_resolution,[status(thm)],[hi3]) ).
cnf(f6,negated_conjecture,
p11(f12(f14(X5,X6)),X6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p11_7) ).
fof(f6_nnf,plain,
! [X5,X6] : p11(f12(f14(X5,X6)),X6),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X5,X6] : p11(f12(f14(X5,X6)),X6),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
p11(f12(f14(X0,X1)),X1),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(hi6,negated_conjecture,
p11(f12(f14(X0,X1)),X1) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(h2,plain,
p11(f12(f14(c23,c24)),c24) = true,
inference(hyper_resolution,[status(thm)],[hi6]) ).
cnf(f27,negated_conjecture,
( ~ p2(X14,X16)
| ~ p11(X15,X17)
| p13(f15(X14,X15),f15(X16,X17)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p13_28) ).
fof(f27_nnf,plain,
! [X14,X15,X16,X17] :
( ~ p2(X14,X16)
| ~ p11(X15,X17)
| p13(f15(X14,X15),f15(X16,X17)) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [X14,X15,X16,X17] :
( ~ p2(X14,X16)
| ~ p11(X15,X17)
| p13(f15(X14,X15),f15(X16,X17)) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
( ~ p2(X0,X2)
| ~ p11(X1,X3)
| p13(f15(X0,X1),f15(X2,X3)) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(hi27,negated_conjecture,
ifeq(p11(X0,X1),true,ifeq(p2(X2,X3),true,p13(f15(X2,X0),f15(X3,X1)),true),true) = true,
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(h6,plain,
p13(f15(f4(f4(c22,f5(f6(c20))),c21),f12(f14(c23,c24))),f15(f4(f4(c22,f5(f6(c20))),c21),c24)) = true,
inference(hyper_resolution,[status(thm)],[hi27,h2,h1]) ).
cnf(h8,plain,
p13(f15(f4(f4(c22,f5(f6(c20))),c21),c24),f15(f3(f4(f4(c22,f5(f6(c20))),c21)),f14(c23,c24))) = true,
inference(hyper_resolution,[status(thm)],[hi23,h6,h7]) ).
cnf(h9,plain,
p13(f15(f3(f4(f4(c22,f5(f6(c20))),c21)),f14(c23,c24)),f15(f4(f4(c22,f5(f6(c20))),c21),c24)) = true,
inference(hyper_resolution,[status(thm)],[hi23,h8,hi4]) ).
cnf(f5,negated_conjecture,
p19(c21,c22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p19_6) ).
fof(f5_nnf,plain,
p19(c21,c22),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
p19(c21,c22),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(hi5,negated_conjecture,
p19(c21,c22) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(h0,plain,
p19(c21,c22) = true,
inference(hyper_resolution,[status(thm)],[hi5]) ).
cnf(f30,negated_conjecture,
( ~ p19(X37,X36)
| p2(f4(f4(f3(X36),f5(f6(c20))),X37),f3(f4(f4(X36,f5(f6(c20))),X37))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_31) ).
fof(f30_nnf,plain,
! [X36,X37] :
( ~ p19(X37,X36)
| p2(f4(f4(f3(X36),f5(f6(c20))),X37),f3(f4(f4(X36,f5(f6(c20))),X37))) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [X36,X37] :
( ~ p19(X37,X36)
| p2(f4(f4(f3(X36),f5(f6(c20))),X37),f3(f4(f4(X36,f5(f6(c20))),X37))) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( ~ p19(X1,X0)
| p2(f4(f4(f3(X0),f5(f6(c20))),X1),f3(f4(f4(X0,f5(f6(c20))),X1))) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(hi30,negated_conjecture,
ifeq(p19(X0,X1),true,p2(f4(f4(f3(X1),f5(f6(c20))),X0),f3(f4(f4(X1,f5(f6(c20))),X0))),true) = true,
inference(equality_encoding,[status(esa)],[c30]) ).
cnf(h3,plain,
p2(f4(f4(f3(c22),f5(f6(c20))),c21),f3(f4(f4(c22,f5(f6(c20))),c21))) = true,
inference(hyper_resolution,[status(thm)],[hi30,h0]) ).
cnf(f0,negated_conjecture,
p11(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p11_1) ).
fof(f0_nnf,plain,
! [X0] : p11(X0,X0),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X0] : p11(X0,X0),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
p11(X0,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,negated_conjecture,
p11(X0,X0) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(h4,plain,
p13(f15(f4(f4(f3(c22),f5(f6(c20))),c21),f14(c23,c24)),f15(f3(f4(f4(c22,f5(f6(c20))),c21)),f14(c23,c24))) = true,
inference(hyper_resolution,[status(thm)],[hi27,hi0,h3]) ).
cnf(h5,plain,
p13(f15(f3(f4(f4(c22,f5(f6(c20))),c21)),f14(c23,c24)),f15(f4(f4(f3(c22),f5(f6(c20))),c21),f14(c23,c24))) = true,
inference(hyper_resolution,[status(thm)],[hi23,h4,hi4]) ).
cnf(t31,plain,
p13(f15(f4(f4(f3(c22),f5(f6(c20))),c21),f14(c23,c24)),f15(f4(f4(c22,f5(f6(c20))),c21),c24)) = true,
inference(hyper_resolution,[status(thm)],[hi23,h5,h9]) ).
cnf(t102,plain,
p13(f15(f4(f4(f3(c22),f5(f6(c20))),c21),f14(c23,c24)),f15(f4(f4(c22,f5(f6(c20))),c21),c24)) = true,
inference(orient,[status(thm)],[t31]) ).
cnf(f31,negated_conjecture,
~ p13(f15(f4(f4(f3(c22),f5(f6(c20))),c21),f14(c23,c24)),f15(f4(f4(c22,f5(f6(c20))),c21),c24)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p13_32) ).
fof(f31_nnf,plain,
~ p13(f15(f4(f4(f3(c22),f5(f6(c20))),c21),f14(c23,c24)),f15(f4(f4(c22,f5(f6(c20))),c21),c24)),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
~ p13(f15(f4(f4(f3(c22),f5(f6(c20))),c21),f14(c23,c24)),f15(f4(f4(c22,f5(f6(c20))),c21),c24)),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
~ p13(f15(f4(f4(f3(c22),f5(f6(c20))),c21),f14(c23,c24)),f15(f4(f4(c22,f5(f6(c20))),c21),c24)),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(goal_0,negated_conjecture,
p13(f15(f4(f4(f3(c22),f5(f6(c20))),c21),f14(c23,c24)),f15(f4(f4(c22,f5(f6(c20))),c21),c24)) != true,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t102]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN617-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 01:54:13 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.11/1.27 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.11/1.27 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------