%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN655-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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 : Thu Sep 24 09:10:48 AM UTC 2026
% Result : Unsatisfiable 0.14s 0.99s
% Output : Proof 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 15
% Syntax : Number of clauses : 54 ( 39 unt; 0 nHn; 41 RR)
% Number of literals : 85 ( 0 equ; 33 neg)
% Maximal clause size : 7 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 12 con; 0-8 aty)
% Number of variables : 79 ( 12 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(p10_1,negated_conjecture,
p10(X0,X0),
file('theBenchmark.p',p10_1) ).
cnf(p9_2,negated_conjecture,
p9(X177,X177),
file('theBenchmark.p',p9_2) ).
cnf(p8_3,negated_conjecture,
p8(X158,X158),
file('theBenchmark.p',p8_3) ).
cnf(p7_4,negated_conjecture,
p7(X139,X139),
file('theBenchmark.p',p7_4) ).
cnf(p6_5,negated_conjecture,
p6(X120,X120),
file('theBenchmark.p',p6_5) ).
cnf(p5_6,negated_conjecture,
p5(X101,X101),
file('theBenchmark.p',p5_6) ).
cnf(p3_7,negated_conjecture,
p3(X78,X78),
file('theBenchmark.p',p3_7) ).
cnf(not_p9_10,negated_conjecture,
~ p9(c22,c23),
file('theBenchmark.p',not_p9_10) ).
cnf(p9_17,negated_conjecture,
( ~ p9(X177,X179)
| ~ p9(X177,X178)
| p9(X178,X179) ),
file('theBenchmark.p',p9_17) ).
cnf(p3_22,negated_conjecture,
( ~ p3(X78,X80)
| ~ p3(X78,X79)
| p3(X79,X80) ),
file('theBenchmark.p',p3_22) ).
cnf(p21_27,negated_conjecture,
p21(f11(c24,c25,c26,c27,c22,c28),f11(c29,c30,c31,c32,c23,c33)),
file('theBenchmark.p',p21_27) ).
cnf(p9_30,negated_conjecture,
( ~ p3(f11(X5,X6,X7,X8,X9,X3),f11(X10,X11,X12,X13,X14,X4))
| p9(X9,X14) ),
file('theBenchmark.p',p9_30) ).
cnf(p9_35,negated_conjecture,
( ~ p21(f11(X38,X39,X36,X42,X43,X40),X41)
| p9(X43,f15(X37,X38,X39,X40,X41,X36,X42,X43)) ),
file('theBenchmark.p',p9_35) ).
cnf(p3_40,negated_conjecture,
( ~ p7(X7,X12)
| ~ p6(X6,X11)
| ~ p5(X5,X10)
| ~ p10(X3,X4)
| ~ p9(X9,X14)
| ~ p8(X8,X13)
| p3(f11(X5,X6,X7,X8,X9,X3),f11(X10,X11,X12,X13,X14,X4)) ),
file('theBenchmark.p',p3_40) ).
cnf(p3_48,negated_conjecture,
( ~ p21(f11(X38,X39,X36,X42,X43,X40),X41)
| p3(X41,f11(f19(X37,X38,X39,X40,X41,X36,X42,X43),f18(X37,X38,X39,X40,X41,X36,X42,X43),f17(X37,X38,X39,X40,X41,X36,X42,X43),f16(X37,X38,X39,X40,X41,X36,X42,X43),f15(X37,X38,X39,X40,X41,X36,X42,X43),f14(X37,X38,X39,X40,X41,X36,X42,X43))) ),
file('theBenchmark.p',p3_48) ).
cnf(t1,plain,
~ p9(c22,c23),
inference(start,[status(thm),parent(0:0)],[not_p9_10]) ).
cnf(t2,plain,
( ~ p9(f15(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),c22)
| ~ p9(f15(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),c23)
| p9(c22,c23) ),
inference(extension,[status(thm),parent(t1:1)],[p9_17]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ p3(f11(f19(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f18(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f17(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f16(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f15(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f14(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22)),f11(c29,c30,c31,c32,c23,c33))
| p9(f15(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),c23) ),
inference(extension,[status(thm),parent(t2:2)],[p9_30]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( ~ p3(f11(c29,c30,c31,c32,c23,c33),f11(f19(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f18(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f17(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f16(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f15(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f14(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22)))
| ~ p3(f11(c29,c30,c31,c32,c23,c33),f11(c29,c30,c31,c32,c23,c33))
| p3(f11(f19(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f18(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f17(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f16(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f15(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f14(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22)),f11(c29,c30,c31,c32,c23,c33)) ),
inference(extension,[status(thm),parent(t4:2)],[p3_22]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
( ~ p8(c32,c32)
| ~ p9(c23,c23)
| ~ p10(c33,c33)
| ~ p5(c29,c29)
| ~ p6(c30,c30)
| ~ p7(c31,c31)
| p3(f11(c29,c30,c31,c32,c23,c33),f11(c29,c30,c31,c32,c23,c33)) ),
inference(extension,[status(thm),parent(t6:2)],[p3_40]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
p7(c31,c31),
inference(extension,[status(thm),parent(t8:2)],[p7_4]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
p6(c30,c30),
inference(extension,[status(thm),parent(t8:3)],[p6_5]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t8:3]) ).
cnf(t14,plain,
p5(c29,c29),
inference(extension,[status(thm),parent(t8:4)],[p5_6]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t8:4]) ).
cnf(t16,plain,
p10(c33,c33),
inference(extension,[status(thm),parent(t8:5)],[p10_1]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t8:5]) ).
cnf(t18,plain,
p9(c23,c23),
inference(extension,[status(thm),parent(t8:6)],[p9_2]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t8:6]) ).
cnf(t20,plain,
p8(c32,c32),
inference(extension,[status(thm),parent(t8:7)],[p8_3]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t8:7]) ).
cnf(t22,plain,
( ~ p21(f11(c24,c25,c26,c27,c22,c28),f11(c29,c30,c31,c32,c23,c33))
| p3(f11(c29,c30,c31,c32,c23,c33),f11(f19(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f18(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f17(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f16(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f15(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),f14(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22))) ),
inference(extension,[status(thm),parent(t6:3)],[p3_48]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t6:3]) ).
cnf(t24,plain,
p21(f11(c24,c25,c26,c27,c22,c28),f11(c29,c30,c31,c32,c23,c33)),
inference(extension,[status(thm),parent(t22:2)],[p21_27]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t22:2]) ).
cnf(t26,plain,
( ~ p9(c22,f15(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22))
| ~ p9(c22,c22)
| p9(f15(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22),c22) ),
inference(extension,[status(thm),parent(t2:3)],[p9_17]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t2:3]) ).
cnf(t28,plain,
( ~ p3(f11(U_1691,U_1692,U_1693,U_1694,c22,U_1695),f11(U_1691,U_1692,U_1693,U_1694,c22,U_1695))
| p9(c22,c22) ),
inference(extension,[status(thm),parent(t26:2)],[p9_30]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t26:2]) ).
cnf(t30,plain,
( ~ p3(f11(U_1691,U_1692,U_1693,U_1694,c22,U_1695),f11(U_1691,U_1692,U_1693,U_1694,c22,U_1695))
| ~ p3(f11(U_1691,U_1692,U_1693,U_1694,c22,U_1695),f11(U_1691,U_1692,U_1693,U_1694,c22,U_1695))
| p3(f11(U_1691,U_1692,U_1693,U_1694,c22,U_1695),f11(U_1691,U_1692,U_1693,U_1694,c22,U_1695)) ),
inference(extension,[status(thm),parent(t28:2)],[p3_22]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t28:2]) ).
cnf(t32,plain,
p3(f11(U_1691,U_1692,U_1693,U_1694,c22,U_1695),f11(U_1691,U_1692,U_1693,U_1694,c22,U_1695)),
inference(extension,[status(thm),parent(t30:2)],[p3_7]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t30:2]) ).
cnf(t34,plain,
p3(f11(U_1691,U_1692,U_1693,U_1694,c22,U_1695),f11(U_1691,U_1692,U_1693,U_1694,c22,U_1695)),
inference(extension,[status(thm),parent(t30:3)],[p3_7]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t30:3]) ).
cnf(t36,plain,
( ~ p21(f11(c24,c25,c26,c27,c22,c28),f11(c29,c30,c31,c32,c23,c33))
| p9(c22,f15(U_1702,c24,c25,c28,f11(c29,c30,c31,c32,c23,c33),c26,c27,c22)) ),
inference(extension,[status(thm),parent(t26:3)],[p9_35]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t26:3]) ).
cnf(t38,plain,
p21(f11(c24,c25,c26,c27,c22,c28),f11(c29,c30,c31,c32,c23,c33)),
inference(extension,[status(thm),parent(t36:2)],[p21_27]) ).
cnf(t39,plain,
$false,
inference(connection,[status(thm),parent(t38:1)],[t38:1,t36:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN655-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 This is a CNF_UNS_RFO_NEQ_HRN problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.58 % Computer : n010.cluster.edu
% 0.10/0.58 % Model : x86_64 x86_64
% 0.10/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.58 % Memory : 8046.5625MB
% 0.10/0.58 % OS : Linux 6.8.0-71-generic
% 0.10/0.58 % CPULimit : 300
% 0.10/0.58 % WCLimit : 300
% 0.10/0.58 % DateTime : Sun Sep 20 07:06:58 UTC 2026
% 0.10/0.58 % CPUTime :
% 0.14/0.99 % SZS status Unsatisfiable for theBenchmark
% 0.14/0.99 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------