%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN719-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:33 PM UTC 2026
% Result : Unsatisfiable 3.73s 1.02s
% Output : Proof 3.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 9
% Syntax : Number of formulae : 49 ( 37 unt; 0 def)
% Number of atoms : 77 ( 14 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 62 ( 34 ~; 28 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 2 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 16 con; 0-4 aty)
% Number of variables : 68 ( 8 sgn 26 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f51,negated_conjecture,
( ~ p70(X230,X229)
| p69(f36(c86,X229),X230) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p69_52) ).
fof(f51_nnf,plain,
! [X229,X230] :
( ~ p70(X230,X229)
| p69(f36(c86,X229),X230) ),
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
! [X229,X230] :
( ~ p70(X230,X229)
| p69(f36(c86,X229),X230) ),
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c51,plain,
( ~ p70(X1,X0)
| p69(f36(c86,X0),X1) ),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(hi50,negated_conjecture,
ifeq(p70(X0,X1),true,p69(f36(c86,X1),X0),true) = true,
inference(equality_encoding,[status(esa)],[c51]) ).
cnf(f42,negated_conjecture,
p70(f30(c88,X242),f38(c85,X243)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p70_43) ).
fof(f42_nnf,plain,
! [X242,X243] : p70(f30(c88,X242),f38(c85,X243)),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [X242,X243] : p70(f30(c88,X242),f38(c85,X243)),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c42,plain,
p70(f30(c88,X0),f38(c85,X1)),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(hi42,negated_conjecture,
p70(f30(c88,X0),f38(c85,X1)) = true,
inference(equality_encoding,[status(esa)],[c42]) ).
cnf(h24,plain,
p69(f36(c86,f38(c85,V0)),f30(c88,V1)) = true,
inference(hyper_resolution,[status(thm)],[hi50,hi42]) ).
cnf(f89,negated_conjecture,
( ~ p14(X13,X15)
| ~ p14(X13,X14)
| p14(X14,X15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p14_90) ).
fof(f89_nnf,plain,
! [X14,X15,X13] :
( ~ p14(X13,X15)
| ~ p14(X13,X14)
| p14(X14,X15) ),
inference(nnf_transformation,[status(thm)],[f89]) ).
fof(f89_sk,plain,
! [X14,X15,X13] :
( ~ p14(X13,X15)
| ~ p14(X13,X14)
| p14(X14,X15) ),
inference(skolemisation,[status(esa)],[f89_nnf]) ).
cnf(c89,plain,
( ~ p14(X2,X1)
| ~ p14(X2,X0)
| p14(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f89_sk]) ).
cnf(hi88,negated_conjecture,
ifeq(p14(X0,X1),true,ifeq(p14(X0,X2),true,p14(X1,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c89]) ).
cnf(f44,negated_conjecture,
p14(f23(f26(c84,c85),X20),X20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p14_45) ).
fof(f44_nnf,plain,
! [X20] : p14(f23(f26(c84,c85),X20),X20),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [X20] : p14(f23(f26(c84,c85),X20),X20),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c44,plain,
p14(f23(f26(c84,c85),X0),X0),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(hi44,negated_conjecture,
p14(f23(f26(c84,c85),X0),X0) = true,
inference(equality_encoding,[status(esa)],[c44]) ).
cnf(f37,negated_conjecture,
p14(X13,X13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p14_38) ).
fof(f37_nnf,plain,
! [X13] : p14(X13,X13),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [X13] : p14(X13,X13),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
p14(X0,X0),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(hi37,negated_conjecture,
p14(X0,X0) = true,
inference(equality_encoding,[status(esa)],[c37]) ).
cnf(h29,plain,
p14(V0,f23(f26(c84,c85),V0)) = true,
inference(hyper_resolution,[status(thm)],[hi88,hi44,hi37]) ).
cnf(f125,negated_conjecture,
( ~ p69(f36(c86,f38(X223,f40(f42(f44(f46(c87,X221),X222),X223),X224))),f30(c88,f32(c89,f8(c75,c76))))
| ~ p14(X222,f23(f26(c84,X223),X224))
| ~ p66(f12(c78,c77),X221)
| ~ p67(f16(c80,X224),c82)
| p68(f19(f21(c83,c77),X221),X222) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p68_126) ).
fof(f125_nnf,plain,
! [X221,X222,X224,X223] :
( ~ p69(f36(c86,f38(X223,f40(f42(f44(f46(c87,X221),X222),X223),X224))),f30(c88,f32(c89,f8(c75,c76))))
| ~ p14(X222,f23(f26(c84,X223),X224))
| ~ p66(f12(c78,c77),X221)
| ~ p67(f16(c80,X224),c82)
| p68(f19(f21(c83,c77),X221),X222) ),
inference(nnf_transformation,[status(thm)],[f125]) ).
fof(f125_sk,plain,
! [X221,X222,X224,X223] :
( ~ p69(f36(c86,f38(X223,f40(f42(f44(f46(c87,X221),X222),X223),X224))),f30(c88,f32(c89,f8(c75,c76))))
| ~ p14(X222,f23(f26(c84,X223),X224))
| ~ p66(f12(c78,c77),X221)
| ~ p67(f16(c80,X224),c82)
| p68(f19(f21(c83,c77),X221),X222) ),
inference(skolemisation,[status(esa)],[f125_nnf]) ).
cnf(c125,plain,
( ~ p69(f36(c86,f38(X3,f40(f42(f44(f46(c87,X0),X1),X3),X2))),f30(c88,f32(c89,f8(c75,c76))))
| ~ p14(X1,f23(f26(c84,X3),X2))
| ~ p66(f12(c78,c77),X0)
| ~ p67(f16(c80,X2),c82)
| p68(f19(f21(c83,c77),X0),X1) ),
inference(cnf_transformation,[status(esa)],[f125_sk]) ).
cnf(hi124,negated_conjecture,
ifeq(p67(f16(c80,X0),c82),true,ifeq(p66(f12(c78,c77),X1),true,ifeq(p14(X2,f23(f26(c84,X3),X0)),true,ifeq(p69(f36(c86,f38(X3,f40(f42(f44(f46(c87,X1),X2),X3),X0))),f30(c88,f32(c89,f8(c75,c76)))),true,p68(f19(f21(c83,c77),X1),X2),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c125]) ).
cnf(f41,negated_conjecture,
p67(f16(c80,c81),c82),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p67_42) ).
fof(f41_nnf,plain,
p67(f16(c80,c81),c82),
inference(nnf_transformation,[status(thm)],[f41]) ).
cnf(c41,plain,
p67(f16(c80,c81),c82),
inference(cnf_transformation,[status(esa)],[f41_nnf]) ).
cnf(hi41,negated_conjecture,
p67(f16(c80,c81),c82) = true,
inference(equality_encoding,[status(esa)],[c41]) ).
cnf(f40,negated_conjecture,
p66(f12(c78,c77),c79),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p66_41) ).
fof(f40_nnf,plain,
p66(f12(c78,c77),c79),
inference(nnf_transformation,[status(thm)],[f40]) ).
cnf(c40,plain,
p66(f12(c78,c77),c79),
inference(cnf_transformation,[status(esa)],[f40_nnf]) ).
cnf(hi40,negated_conjecture,
p66(f12(c78,c77),c79) = true,
inference(equality_encoding,[status(esa)],[c40]) ).
cnf(t69,plain,
p68(f19(f21(c83,c77),c79),c81) = true,
inference(hyper_resolution,[status(thm)],[hi124,hi41,hi40,h29,h24]) ).
cnf(t662,plain,
p68(f19(f21(c83,c77),c79),c81) = true,
inference(orient,[status(thm)],[t69]) ).
cnf(f45,negated_conjecture,
~ p68(f19(f21(c83,c77),c79),c81),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_p68_46) ).
fof(f45_nnf,plain,
~ p68(f19(f21(c83,c77),c79),c81),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
~ p68(f19(f21(c83,c77),c79),c81),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c45,plain,
~ p68(f19(f21(c83,c77),c79),c81),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(goal_0,negated_conjecture,
p68(f19(f21(c83,c77),c79),c81) != true,
inference(equality_encoding,[status(esa)],[c45]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t662]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN719-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n009.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Fri Sep 25 02:10:15 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 3.73/1.02 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.73/1.02 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------