%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN703-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n009.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:31 PM UTC 2026
% Result : Unsatisfiable 7.22s 1.44s
% Output : Proof 7.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 12
% Syntax : Number of formulae : 65 ( 45 unt; 0 def)
% Number of atoms : 97 ( 21 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 76 ( 44 ~; 32 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 13 con; 0-4 aty)
% Number of variables : 166 ( 33 sgn 62 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f59,negated_conjecture,
( ~ p3(X119,X121)
| ~ p2(X118,X120)
| p4(f5(X118,X119),f5(X120,X121)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p4_60) ).
fof(f59_nnf,plain,
! [X118,X119,X120,X121] :
( ~ p3(X119,X121)
| ~ p2(X118,X120)
| p4(f5(X118,X119),f5(X120,X121)) ),
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_sk,plain,
! [X118,X119,X120,X121] :
( ~ p3(X119,X121)
| ~ p2(X118,X120)
| p4(f5(X118,X119),f5(X120,X121)) ),
inference(skolemisation,[status(esa)],[f59_nnf]) ).
cnf(c59,plain,
( ~ p3(X1,X3)
| ~ p2(X0,X2)
| p4(f5(X0,X1),f5(X2,X3)) ),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
cnf(hi57,negated_conjecture,
ifeq(p2(X0,X1),true,ifeq(p3(X2,X3),true,p4(f5(X0,X2),f5(X1,X3)),true),true) = true,
inference(equality_encoding,[status(esa)],[c59]) ).
cnf(f7,negated_conjecture,
p2(X30,X30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2_8) ).
fof(f7_nnf,plain,
! [X30] : p2(X30,X30),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X30] : p2(X30,X30),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
p2(X0,X0),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(hi7,negated_conjecture,
p2(X0,X0) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(f79,negated_conjecture,
p3(f16(f18(c54,f8(f11(f13(c49,X57),X58),X59)),X60),f8(f11(f13(c49,f20(f22(f24(f26(c56,X57),X58),X59),X60)),f30(f32(f34(f36(c57,X57),X58),X59),X60)),f40(f42(f44(f46(c58,X57),X58),X59),X60))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p3_80) ).
fof(f79_nnf,plain,
! [X57,X58,X59,X60] : p3(f16(f18(c54,f8(f11(f13(c49,X57),X58),X59)),X60),f8(f11(f13(c49,f20(f22(f24(f26(c56,X57),X58),X59),X60)),f30(f32(f34(f36(c57,X57),X58),X59),X60)),f40(f42(f44(f46(c58,X57),X58),X59),X60))),
inference(nnf_transformation,[status(thm)],[f79]) ).
fof(f79_sk,plain,
! [X57,X58,X59,X60] : p3(f16(f18(c54,f8(f11(f13(c49,X57),X58),X59)),X60),f8(f11(f13(c49,f20(f22(f24(f26(c56,X57),X58),X59),X60)),f30(f32(f34(f36(c57,X57),X58),X59),X60)),f40(f42(f44(f46(c58,X57),X58),X59),X60))),
inference(skolemisation,[status(esa)],[f79_nnf]) ).
cnf(c79,plain,
p3(f16(f18(c54,f8(f11(f13(c49,X0),X1),X2)),X3),f8(f11(f13(c49,f20(f22(f24(f26(c56,X0),X1),X2),X3)),f30(f32(f34(f36(c57,X0),X1),X2),X3)),f40(f42(f44(f46(c58,X0),X1),X2),X3))),
inference(cnf_transformation,[status(esa)],[f79_sk]) ).
cnf(hi77,negated_conjecture,
p3(f16(f18(c54,f8(f11(f13(c49,X0),X1),X2)),X3),f8(f11(f13(c49,f20(f22(f24(f26(c56,X0),X1),X2),X3)),f30(f32(f34(f36(c57,X0),X1),X2),X3)),f40(f42(f44(f46(c58,X0),X1),X2),X3))) = true,
inference(equality_encoding,[status(esa)],[c79]) ).
cnf(h22,plain,
p4(f5(V0,f16(f18(c54,f8(f11(f13(c49,V1),V2),V3)),V4)),f5(V0,f8(f11(f13(c49,f20(f22(f24(f26(c56,V1),V2),V3),V4)),f30(f32(f34(f36(c57,V1),V2),V3),V4)),f40(f42(f44(f46(c58,V1),V2),V3),V4)))) = true,
inference(hyper_resolution,[status(thm)],[hi57,hi7,hi77]) ).
cnf(f52,negated_conjecture,
( ~ p15(X145,X144)
| ~ p47(X146,X145)
| ~ p4(X146,X143)
| p47(X143,X144) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p47_53) ).
fof(f52_nnf,plain,
! [X143,X144,X146,X145] :
( ~ p15(X145,X144)
| ~ p47(X146,X145)
| ~ p4(X146,X143)
| p47(X143,X144) ),
inference(nnf_transformation,[status(thm)],[f52]) ).
fof(f52_sk,plain,
! [X143,X144,X146,X145] :
( ~ p15(X145,X144)
| ~ p47(X146,X145)
| ~ p4(X146,X143)
| p47(X143,X144) ),
inference(skolemisation,[status(esa)],[f52_nnf]) ).
cnf(c52,plain,
( ~ p15(X3,X1)
| ~ p47(X2,X3)
| ~ p4(X2,X0)
| p47(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(hi50,negated_conjecture,
ifeq(p4(X0,X1),true,ifeq(p47(X0,X2),true,ifeq(p15(X2,X3),true,p47(X1,X3),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c52]) ).
cnf(f76,negated_conjecture,
p47(f5(c48,f16(f18(c54,f8(f11(f13(c49,c50),c51),c52)),c55)),c53),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p47_77) ).
fof(f76_nnf,plain,
p47(f5(c48,f16(f18(c54,f8(f11(f13(c49,c50),c51),c52)),c55)),c53),
inference(nnf_transformation,[status(thm)],[f76]) ).
cnf(c76,plain,
p47(f5(c48,f16(f18(c54,f8(f11(f13(c49,c50),c51),c52)),c55)),c53),
inference(cnf_transformation,[status(esa)],[f76_nnf]) ).
cnf(hi74,negated_conjecture,
p47(f5(c48,f16(f18(c54,f8(f11(f13(c49,c50),c51),c52)),c55)),c53) = true,
inference(equality_encoding,[status(esa)],[c76]) ).
cnf(f4,negated_conjecture,
p15(X17,X17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p15_5) ).
fof(f4_nnf,plain,
! [X17] : p15(X17,X17),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X17] : p15(X17,X17),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
p15(X0,X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(hi4,negated_conjecture,
p15(X0,X0) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(h77,plain,
p47(f5(c48,f8(f11(f13(c49,f20(f22(f24(f26(c56,c50),c51),c52),c55)),f30(f32(f34(f36(c57,c50),c51),c52),c55)),f40(f42(f44(f46(c58,c50),c51),c52),c55))),c53) = true,
inference(hyper_resolution,[status(thm)],[hi50,h22,hi74,hi4]) ).
cnf(f73,negated_conjecture,
( ~ p47(f5(c48,f8(f11(f13(c49,X139),X141),X142)),X140)
| p47(X139,X140) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p47_74) ).
fof(f73_nnf,plain,
! [X139,X140,X141,X142] :
( ~ p47(f5(c48,f8(f11(f13(c49,X139),X141),X142)),X140)
| p47(X139,X140) ),
inference(nnf_transformation,[status(thm)],[f73]) ).
fof(f73_sk,plain,
! [X139,X140,X141,X142] :
( ~ p47(f5(c48,f8(f11(f13(c49,X139),X141),X142)),X140)
| p47(X139,X140) ),
inference(skolemisation,[status(esa)],[f73_nnf]) ).
cnf(c73,plain,
( ~ p47(f5(c48,f8(f11(f13(c49,X0),X2),X3)),X1)
| p47(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f73_sk]) ).
cnf(hi71,negated_conjecture,
ifeq(p47(f5(c48,f8(f11(f13(c49,X0),X1),X2)),X3),true,p47(X0,X3),true) = true,
inference(equality_encoding,[status(esa)],[c73]) ).
cnf(h225,plain,
p47(f20(f22(f24(f26(c56,c50),c51),c52),c55),c53) = true,
inference(hyper_resolution,[status(thm)],[hi71,h77]) ).
cnf(f74,negated_conjecture,
( ~ p47(f20(f22(f24(f26(c56,X57),X58),X59),X60),X61)
| p47(X57,X61) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p47_75) ).
fof(f74_nnf,plain,
! [X57,X61,X58,X59,X60] :
( ~ p47(f20(f22(f24(f26(c56,X57),X58),X59),X60),X61)
| p47(X57,X61) ),
inference(nnf_transformation,[status(thm)],[f74]) ).
fof(f74_sk,plain,
! [X57,X61,X58,X59,X60] :
( ~ p47(f20(f22(f24(f26(c56,X57),X58),X59),X60),X61)
| p47(X57,X61) ),
inference(skolemisation,[status(esa)],[f74_nnf]) ).
cnf(c74,plain,
( ~ p47(f20(f22(f24(f26(c56,X0),X2),X3),X4),X1)
| p47(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f74_sk]) ).
cnf(hi72,negated_conjecture,
ifeq(p47(f20(f22(f24(f26(c56,X0),X1),X2),X3),X4),true,p47(X0,X4),true) = true,
inference(equality_encoding,[status(esa)],[c74]) ).
cnf(h229,plain,
p47(c50,c53) = true,
inference(hyper_resolution,[status(thm)],[hi72,h225]) ).
cnf(f75,negated_conjecture,
( ~ p47(X139,X140)
| p47(f5(c48,f8(f11(f13(c49,X139),X141),X142)),X140) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p47_76) ).
fof(f75_nnf,plain,
! [X139,X141,X142,X140] :
( ~ p47(X139,X140)
| p47(f5(c48,f8(f11(f13(c49,X139),X141),X142)),X140) ),
inference(nnf_transformation,[status(thm)],[f75]) ).
fof(f75_sk,plain,
! [X139,X141,X142,X140] :
( ~ p47(X139,X140)
| p47(f5(c48,f8(f11(f13(c49,X139),X141),X142)),X140) ),
inference(skolemisation,[status(esa)],[f75_nnf]) ).
cnf(c75,plain,
( ~ p47(X0,X3)
| p47(f5(c48,f8(f11(f13(c49,X0),X1),X2)),X3) ),
inference(cnf_transformation,[status(esa)],[f75_sk]) ).
cnf(hi73,negated_conjecture,
ifeq(p47(X0,X1),true,p47(f5(c48,f8(f11(f13(c49,X0),X2),X3)),X1),true) = true,
inference(equality_encoding,[status(esa)],[c75]) ).
cnf(t78,plain,
p47(f5(c48,f8(f11(f13(c49,c50),X1),X2)),c53) = true,
inference(hyper_resolution,[status(thm)],[hi73,h229]) ).
cnf(t357,plain,
p47(f5(c48,f8(f11(f13(c49,c50),X1),X2)),c53) = true,
inference(orient,[status(thm)],[t78]) ).
cnf(t27,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t27]) ).
cnf(f50,negated_conjecture,
~ p47(f5(c48,f8(f11(f13(c49,c50),c51),c52)),c53),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_p47_51) ).
fof(f50_nnf,plain,
~ p47(f5(c48,f8(f11(f13(c49,c50),c51),c52)),c53),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
~ p47(f5(c48,f8(f11(f13(c49,c50),c51),c52)),c53),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c50,plain,
~ p47(f5(c48,f8(f11(f13(c49,c50),c51),c52)),c53),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(f51,negated_conjecture,
~ p47(f20(f22(f24(f26(c56,X57),X58),X59),X60),X60),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_p47_52) ).
fof(f51_nnf,plain,
! [X57,X58,X59,X60] : ~ p47(f20(f22(f24(f26(c56,X57),X58),X59),X60),X60),
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
! [X57,X58,X59,X60] : ~ p47(f20(f22(f24(f26(c56,X57),X58),X59),X60),X60),
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c51,plain,
~ p47(f20(f22(f24(f26(c56,X0),X1),X2),X3),X3),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c50,c51]) ).
cnf(g0_0,plain,
true != ifeq(p47(f5(c48,f8(f11(f13(c49,c50),c51),c52)),c53),true,false,true),
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
true != ifeq(true,true,false,true),
inference(rw,[status(thm)],[g0_0,t357]) ).
cnf(g0_2,plain,
true != false,
inference(rw,[status(thm)],[g0_1,t256]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN703-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/0.34 % Computer : n009.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Fri Sep 25 02:07:58 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.34 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 7.22/1.44 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.22/1.44 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------