%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SYN713-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 : n005.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:24 AM UTC 2026
% Result : Unsatisfiable 20.77s 3.15s
% Output : CNFRefutation 20.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 17
% Syntax : Number of clauses : 52 ( 22 unt; 2 nHn; 40 RR)
% Number of literals : 114 ( 0 equ; 66 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 11 ( 10 usr; 1 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 15 con; 0-2 aty)
% Number of variables : 104 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(p9_2,negated_conjecture,
p9(X0,X0) ).
cnf(p40_14,negated_conjecture,
p40(X0,X0) ).
cnf(p4_15,negated_conjecture,
p4(X0,X0) ).
cnf(p13_33,negated_conjecture,
p13(X0,X0) ).
cnf(p12_34,negated_conjecture,
p12(X0,X0) ).
cnf(p59_35,negated_conjecture,
p59(f38(c72,c77),f35(c73,c68)) ).
cnf(p56_38,negated_conjecture,
p56(f11(c65,f14(f17(c66,c67),c68)),c64) ).
cnf(not_p57_39,negated_conjecture,
~ p57(f26(f28(c71,f41(c78,c64)),c67),c77) ).
cnf(p10_40,negated_conjecture,
( ~ p10(X2,X1)
| ~ p10(X2,X0)
| p10(X0,X1) ) ).
cnf(p4_54,negated_conjecture,
( ~ p4(X2,X1)
| ~ p4(X2,X0)
| p4(X0,X1) ) ).
cnf(p57_74,negated_conjecture,
( ~ p57(f26(X0,X1),X2)
| p57(f26(f28(c71,X0),X1),X2) ) ).
cnf(p56_76,negated_conjecture,
( ~ p4(X3,X0)
| ~ p56(X3,X2)
| ~ p40(X2,X1)
| p56(X0,X1) ) ).
cnf(not_p58_80,negated_conjecture,
~ p58(f31(f33(c75,c76),f23(c69,c77)),f19(f22(c70,c69),c68)) ).
cnf(p10_81,negated_conjecture,
( ~ p13(X1,X3)
| ~ p12(X0,X2)
| p10(f14(X0,X1),f14(X2,X3)) ) ).
cnf(p4_87,negated_conjecture,
( ~ p9(X0,X2)
| ~ p10(X1,X3)
| p4(f11(X0,X1),f11(X2,X3)) ) ).
cnf(p57_101,negated_conjecture,
( ~ p56(f11(c65,f14(f17(c66,X1),f23(c74,X2))),X0)
| p57(f26(f41(c78,X0),X1),X2) ) ).
cnf(p13_105,negated_conjecture,
( ~ p59(f38(c72,X1),f35(c73,X0))
| p58(f31(f33(c75,c76),f23(c69,X1)),f19(f22(c70,c69),X0))
| p13(X0,f23(c74,X1)) ) ).
cnf(c1,plain,
p9(X0,X0),
inference(clausification,[status(esa)],[p9_2]) ).
cnf(c13,plain,
p40(X0,X0),
inference(clausification,[status(esa)],[p40_14]) ).
cnf(c14,plain,
p4(X0,X0),
inference(clausification,[status(esa)],[p4_15]) ).
cnf(c32,plain,
p13(X0,X0),
inference(clausification,[status(esa)],[p13_33]) ).
cnf(c33,plain,
p12(X0,X0),
inference(clausification,[status(esa)],[p12_34]) ).
cnf(c34,plain,
p59(f38(c72,c77),f35(c73,c68)),
inference(clausification,[status(esa)],[p59_35]) ).
cnf(c37,plain,
p56(f11(c65,f14(f17(c66,c67),c68)),c64),
inference(clausification,[status(esa)],[p56_38]) ).
cnf(c38,plain,
~ p57(f26(f28(c71,f41(c78,c64)),c67),c77),
inference(clausification,[status(esa)],[not_p57_39]) ).
cnf(c39,plain,
( ~ p10(X2,X1)
| ~ p10(X2,X0)
| p10(X0,X1) ),
inference(clausification,[status(esa)],[p10_40]) ).
cnf(c53,plain,
( ~ p4(X2,X1)
| ~ p4(X2,X0)
| p4(X0,X1) ),
inference(clausification,[status(esa)],[p4_54]) ).
cnf(c73,plain,
( ~ p57(f26(X0,X1),X2)
| p57(f26(f28(c71,X0),X1),X2) ),
inference(clausification,[status(esa)],[p57_74]) ).
cnf(c75,plain,
( ~ p4(X3,X0)
| ~ p56(X3,X2)
| ~ p40(X2,X1)
| p56(X0,X1) ),
inference(clausification,[status(esa)],[p56_76]) ).
cnf(c79,plain,
~ p58(f31(f33(c75,c76),f23(c69,c77)),f19(f22(c70,c69),c68)),
inference(clausification,[status(esa)],[not_p58_80]) ).
cnf(c80,plain,
( ~ p13(X1,X3)
| ~ p12(X0,X2)
| p10(f14(X0,X1),f14(X2,X3)) ),
inference(clausification,[status(esa)],[p10_81]) ).
cnf(c86,plain,
( ~ p9(X0,X2)
| ~ p10(X1,X3)
| p4(f11(X0,X1),f11(X2,X3)) ),
inference(clausification,[status(esa)],[p4_87]) ).
cnf(c100,plain,
( ~ p56(f11(c65,f14(f17(c66,X1),f23(c74,X2))),X0)
| p57(f26(f41(c78,X0),X1),X2) ),
inference(clausification,[status(esa)],[p57_101]) ).
cnf(c104,plain,
( ~ p59(f38(c72,X1),f35(c73,X0))
| p58(f31(f33(c75,c76),f23(c69,X1)),f19(f22(c70,c69),X0))
| p13(X0,f23(c74,X1)) ),
inference(clausification,[status(esa)],[p13_105]) ).
cnf(d0,plain,
~ p57(f26(f41(c78,c64),c67),c77),
inference(resolution,[status(thm)],[c73,c38]) ).
cnf(d1,plain,
( p56(X1,X0)
| ~ p4(f11(c65,f14(f17(c66,c67),c68)),X1)
| ~ p40(c64,X0) ),
inference(resolution,[status(thm)],[c75,c37]) ).
cnf(d2,plain,
( ~ p4(f11(X2,X0),X4)
| p4(f11(X3,X1),X4)
| ~ p9(X2,X3)
| ~ p10(X0,X1) ),
inference(resolution,[status(thm)],[c86,c53]) ).
cnf(d3,plain,
( p4(f11(X3,X1),f11(X2,X0))
| ~ p9(X2,X3)
| ~ p10(X0,X1) ),
inference(resolution,[status(thm)],[d2,c14]) ).
cnf(d4,plain,
( p56(f11(X1,X0),X2)
| ~ p40(c64,X2)
| ~ p9(X1,c65)
| ~ p10(X0,f14(f17(c66,c67),c68)) ),
inference(resolution,[status(thm)],[d3,d1]) ).
cnf(d5,plain,
( ~ p59(f38(c72,c77),f35(c73,c68))
| p13(c68,f23(c74,c77)) ),
inference(resolution,[status(thm)],[c104,c79]) ).
cnf(d6,plain,
p13(c68,f23(c74,c77)),
inference(resolution,[status(thm)],[c34,d5]) ).
cnf(d7,plain,
( ~ p10(f14(X2,X0),X4)
| p10(f14(X3,X1),X4)
| ~ p12(X2,X3)
| ~ p13(X0,X1) ),
inference(resolution,[status(thm)],[c80,c39]) ).
cnf(d8,plain,
( ~ p12(X5,X2)
| ~ p13(X4,X3)
| ~ p12(X5,X0)
| ~ p13(X4,X1)
| p10(f14(X0,X1),f14(X2,X3)) ),
inference(resolution,[status(thm)],[d7,c80]) ).
cnf(d9,plain,
( ~ p12(X0,X2)
| ~ p13(X4,X1)
| ~ p13(X4,X3)
| p10(f14(X0,X1),f14(X2,X3)) ),
inference(resolution,[status(thm)],[d8,c33]) ).
cnf(d10,plain,
( ~ p13(X3,X1)
| ~ p13(X3,X2)
| p10(f14(X0,X1),f14(X0,X2)) ),
inference(resolution,[status(thm)],[d9,c33]) ).
cnf(d11,plain,
( ~ p13(c68,X1)
| p10(f14(X0,f23(c74,c77)),f14(X0,X1)) ),
inference(resolution,[status(thm)],[d10,d6]) ).
cnf(d12,plain,
( p56(f11(X0,f14(f17(c66,c67),f23(c74,c77))),X1)
| ~ p40(c64,X1)
| ~ p9(X0,c65)
| ~ p13(c68,c68) ),
inference(resolution,[status(thm)],[d11,d4]) ).
cnf(d13,plain,
( p56(f11(X0,f14(f17(c66,c67),f23(c74,c77))),X1)
| ~ p40(c64,X1)
| ~ p9(X0,c65) ),
inference(resolution,[status(thm)],[c32,d12]) ).
cnf(d14,plain,
( p57(f26(f41(c78,X0),c67),c77)
| ~ p40(c64,X0)
| ~ p9(c65,c65) ),
inference(resolution,[status(thm)],[d13,c100]) ).
cnf(d15,plain,
( p57(f26(f41(c78,X0),c67),c77)
| ~ p40(c64,X0) ),
inference(resolution,[status(thm)],[c1,d14]) ).
cnf(d16,plain,
~ p40(c64,c64),
inference(resolution,[status(thm)],[d15,d0]) ).
cnf(d17,plain,
$false,
inference(resolution,[status(thm)],[c13,d16]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN713-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n005.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 : Sat Sep 26 18:21:34 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.77/3.15 % SZS status Unsatisfiable for theBenchmark.p
% 20.77/3.15 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------