%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SYN719-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 : Sun Sep 27 09:29:25 AM UTC 2026
% Result : Unsatisfiable 17.62s 2.65s
% Output : CNFRefutation 17.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 12
% Syntax : Number of clauses : 35 ( 20 unt; 0 nHn; 22 RR)
% Number of literals : 68 ( 0 equ; 37 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 15 con; 0-2 aty)
% Number of variables : 58 ( 8 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(p35_22,negated_conjecture,
p35(X0,X0) ).
cnf(p29_27,negated_conjecture,
p29(X0,X0) ).
cnf(p14_38,negated_conjecture,
p14(X0,X0) ).
cnf(p66_41,negated_conjecture,
p66(f12(c78,c77),c79) ).
cnf(p67_42,negated_conjecture,
p67(f16(c80,c81),c82) ).
cnf(p70_43,negated_conjecture,
p70(f30(c88,X0),f38(c85,X1)) ).
cnf(p14_45,negated_conjecture,
p14(f23(f26(c84,c85),X0),X0) ).
cnf(not_p68_46,negated_conjecture,
~ p68(f19(f21(c83,c77),c79),c81) ).
cnf(p69_52,negated_conjecture,
( ~ p70(X1,X0)
| p69(f36(c86,X0),X1) ) ).
cnf(p14_90,negated_conjecture,
( ~ p14(X2,X1)
| ~ p14(X2,X0)
| p14(X0,X1) ) ).
cnf(p69_98,negated_conjecture,
( ~ p29(X3,X1)
| ~ p69(X2,X3)
| ~ p35(X2,X0)
| p69(X0,X1) ) ).
cnf(p68_126,negated_conjecture,
( ~ 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) ) ).
cnf(c21,plain,
p35(X0,X0),
inference(clausification,[status(esa)],[p35_22]) ).
cnf(c26,plain,
p29(X0,X0),
inference(clausification,[status(esa)],[p29_27]) ).
cnf(c37,plain,
p14(X0,X0),
inference(clausification,[status(esa)],[p14_38]) ).
cnf(c40,plain,
p66(f12(c78,c77),c79),
inference(clausification,[status(esa)],[p66_41]) ).
cnf(c41,plain,
p67(f16(c80,c81),c82),
inference(clausification,[status(esa)],[p67_42]) ).
cnf(c42,plain,
p70(f30(c88,X0),f38(c85,X1)),
inference(clausification,[status(esa)],[p70_43]) ).
cnf(c44,plain,
p14(f23(f26(c84,c85),X0),X0),
inference(clausification,[status(esa)],[p14_45]) ).
cnf(c45,plain,
~ p68(f19(f21(c83,c77),c79),c81),
inference(clausification,[status(esa)],[not_p68_46]) ).
cnf(c51,plain,
( ~ p70(X1,X0)
| p69(f36(c86,X0),X1) ),
inference(clausification,[status(esa)],[p69_52]) ).
cnf(c89,plain,
( ~ p14(X2,X1)
| ~ p14(X2,X0)
| p14(X0,X1) ),
inference(clausification,[status(esa)],[p14_90]) ).
cnf(c97,plain,
( ~ p29(X3,X1)
| ~ p69(X2,X3)
| ~ p35(X2,X0)
| p69(X0,X1) ),
inference(clausification,[status(esa)],[p69_98]) ).
cnf(c125,plain,
( p68(f19(f21(c83,c77),X3),X0)
| ~ p69(f36(c86,f38(X1,f40(f42(f44(f46(c87,X3),X0),X1),X2))),f30(c88,f32(c89,f8(c75,c76))))
| ~ p67(f16(c80,X2),c82)
| ~ p66(f12(c78,c77),X3)
| ~ p14(X0,f23(f26(c84,X1),X2)) ),
inference(clausification,[status(esa)],[p68_126]) ).
cnf(d0,plain,
( ~ p14(X1,X0)
| p14(X0,X1) ),
inference(resolution,[status(thm)],[c89,c37]) ).
cnf(d1,plain,
p14(X0,f23(f26(c84,c85),X0)),
inference(resolution,[status(thm)],[d0,c44]) ).
cnf(d2,plain,
( ~ p70(X2,X0)
| p69(X1,X3)
| ~ p29(X2,X3)
| ~ p35(f36(c86,X0),X1) ),
inference(resolution,[status(thm)],[c97,c51]) ).
cnf(d3,plain,
( p69(f36(c86,X2),X1)
| ~ p70(X0,X2)
| ~ p29(X0,X1) ),
inference(resolution,[status(thm)],[d2,c21]) ).
cnf(d4,plain,
( p69(f36(c86,f38(c85,X2)),X1)
| ~ p29(f30(c88,X0),X1) ),
inference(resolution,[status(thm)],[d3,c42]) ).
cnf(d5,plain,
p69(f36(c86,f38(c85,X0)),f30(c88,X1)),
inference(resolution,[status(thm)],[d4,c26]) ).
cnf(d6,plain,
( p68(f19(f21(c83,c77),X2),X0)
| ~ p67(f16(c80,X1),c82)
| ~ p66(f12(c78,c77),X2)
| ~ p14(X0,f23(f26(c84,c85),X1)) ),
inference(resolution,[status(thm)],[d5,c125]) ).
cnf(d7,plain,
( p68(f19(f21(c83,c77),X0),X1)
| ~ p67(f16(c80,X1),c82)
| ~ p66(f12(c78,c77),X0) ),
inference(resolution,[status(thm)],[d6,d1]) ).
cnf(d8,plain,
( ~ p67(f16(c80,c81),c82)
| ~ p66(f12(c78,c77),c79) ),
inference(resolution,[status(thm)],[d7,c45]) ).
cnf(d9,plain,
~ p67(f16(c80,c81),c82),
inference(resolution,[status(thm)],[c40,d8]) ).
cnf(d10,plain,
$false,
inference(resolution,[status(thm)],[c41,d9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN719-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n001.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 18:27:58 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.62/2.65 % SZS status Unsatisfiable for theBenchmark.p
% 17.62/2.65 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------