%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN621-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:43 AM UTC 2026
% Result : Unsatisfiable 0.08s 0.37s
% Output : Proof 0.08s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(p10_1,negated_conjecture,
p10(X0,X0),
file('theBenchmark.p',p10_1) ).
cnf(p8_2,negated_conjecture,
p8(X78,X78),
file('theBenchmark.p',p8_2) ).
cnf(p7_3,negated_conjecture,
p7(X71,X71),
file('theBenchmark.p',p7_3) ).
cnf(p4_4,negated_conjecture,
p4(X38,X38),
file('theBenchmark.p',p4_4) ).
cnf(p2_5,negated_conjecture,
p2(X12,X12),
file('theBenchmark.p',p2_5) ).
cnf(p13_6,negated_conjecture,
p13(X7,X7),
file('theBenchmark.p',p13_6) ).
cnf(not_p2_7,negated_conjecture,
~ p2(c23,f3(c24)),
file('theBenchmark.p',not_p2_7) ).
cnf(p13_8,negated_conjecture,
( ~ p7(X10,X11)
| p13(f14(X10),f14(X11)) ),
file('theBenchmark.p',p13_8) ).
cnf(p4_9,negated_conjecture,
( ~ p4(X59,X60)
| p4(f5(X59),f5(X60)) ),
file('theBenchmark.p',p4_9) ).
cnf(p4_10,negated_conjecture,
( ~ p2(X45,X46)
| p4(f16(X45),f16(X46)) ),
file('theBenchmark.p',p4_10) ).
cnf(p2_11,negated_conjecture,
( ~ p2(X24,X25)
| p2(f3(X24),f3(X25)) ),
file('theBenchmark.p',p2_11) ).
cnf(p2_12,negated_conjecture,
( ~ p2(X22,X23)
| p2(f18(X22),f18(X23)) ),
file('theBenchmark.p',p2_12) ).
cnf(p2_13,negated_conjecture,
( ~ p2(X20,X21)
| p2(f17(X20),f17(X21)) ),
file('theBenchmark.p',p2_13) ).
cnf(p10_14,negated_conjecture,
( ~ p10(X0,X2)
| ~ p10(X0,X1)
| p10(X1,X2) ),
file('theBenchmark.p',p10_14) ).
cnf(p8_15,negated_conjecture,
( ~ p8(X78,X80)
| ~ p8(X78,X79)
| p8(X79,X80) ),
file('theBenchmark.p',p8_15) ).
cnf(p7_16,negated_conjecture,
( ~ p7(X71,X73)
| ~ p7(X71,X72)
| p7(X72,X73) ),
file('theBenchmark.p',p7_16) ).
cnf(p4_17,negated_conjecture,
( ~ p4(X38,X40)
| ~ p4(X38,X39)
| p4(X39,X40) ),
file('theBenchmark.p',p4_17) ).
cnf(p21_18,negated_conjecture,
( ~ p21(X32,X31)
| ~ p21(X30,X32)
| p21(X30,X31) ),
file('theBenchmark.p',p21_18) ).
cnf(p2_19,negated_conjecture,
( ~ p2(X12,X14)
| ~ p2(X12,X13)
| p2(X13,X14) ),
file('theBenchmark.p',p2_19) ).
cnf(p13_20,negated_conjecture,
( ~ p13(X7,X9)
| ~ p13(X7,X8)
| p13(X8,X9) ),
file('theBenchmark.p',p13_20) ).
cnf(p21_21,negated_conjecture,
( ~ p21(X28,X29)
| ~ p4(X29,X27)
| ~ p4(X28,X26)
| p21(X26,X27) ),
file('theBenchmark.p',p21_21) ).
cnf(p22_22,negated_conjecture,
( ~ p13(X36,X35)
| ~ p4(X37,X34)
| ~ p22(X37,X36)
| p22(X34,X35) ),
file('theBenchmark.p',p22_22) ).
cnf(p7_23,negated_conjecture,
( ~ p2(X74,X76)
| ~ p10(X75,X77)
| p7(f11(X74,X75),f11(X76,X77)) ),
file('theBenchmark.p',p7_23) ).
cnf(p10_24,negated_conjecture,
( ~ p2(X4,X6)
| ~ p2(X3,X5)
| p10(f12(X3,X4),f12(X5,X6)) ),
file('theBenchmark.p',p10_24) ).
cnf(p4_25,negated_conjecture,
( ~ p4(X42,X44)
| ~ p4(X41,X43)
| p4(f15(X41,X42),f15(X43,X44)) ),
file('theBenchmark.p',p4_25) ).
cnf(p4_26,negated_conjecture,
( ~ p7(X47,X49)
| ~ p4(X48,X50)
| p4(f19(X47,X48),f19(X49,X50)) ),
file('theBenchmark.p',p4_26) ).
cnf(p4_27,negated_conjecture,
( ~ p4(X62,X64)
| ~ p4(X61,X63)
| p4(f6(X61,X62),f6(X63,X64)) ),
file('theBenchmark.p',p4_27) ).
cnf(p2_28,negated_conjecture,
( p22(f20(X17,X15,X18,X16),f14(f11(X17,f12(X15,X18))))
| p2(X15,f3(c24)) ),
file('theBenchmark.p',p2_28) ).
cnf(p4_29,negated_conjecture,
( ~ p4(X67,X70)
| ~ p8(X66,X69)
| ~ p7(X65,X68)
| p4(f9(X65,X66,X67),f9(X68,X69,X70)) ),
file('theBenchmark.p',p4_29) ).
cnf(p4_30,negated_conjecture,
( ~ p2(X52,X56)
| ~ p2(X51,X55)
| ~ p4(X54,X58)
| ~ p2(X53,X57)
| p4(f20(X51,X52,X53,X54),f20(X55,X56,X57,X58)) ),
file('theBenchmark.p',p4_30) ).
cnf(p21_31,negated_conjecture,
( ~ p22(X33,f14(f11(c25,f12(c23,c26))))
| p21(f5(f6(c27,f9(f11(c25,f12(c23,c26)),c28,c27))),f5(f6(c27,X33))) ),
file('theBenchmark.p',p21_31) ).
cnf(not_p21_32,negated_conjecture,
~ p21(f5(f6(c27,f9(f11(c25,f12(c23,c26)),c28,c27))),f15(f19(f11(c25,f12(c23,c26)),c27),f16(f3(f17(f18(c24)))))),
file('theBenchmark.p',not_p21_32) ).
cnf(p2_33,negated_conjecture,
( ~ p22(X19,f14(f11(X17,f12(X15,X18))))
| p21(f5(f6(X16,f20(X17,X15,X18,X16))),f5(f6(X16,X19)))
| p2(X15,f3(c24)) ),
file('theBenchmark.p',p2_33) ).
cnf(p2_34,negated_conjecture,
( p21(f5(f6(X16,f20(X17,X15,X18,X16))),f15(f19(f11(X17,f12(X15,X18)),X16),f16(f3(f17(f18(c24))))))
| p2(X15,f3(c24)) ),
file('theBenchmark.p',p2_34) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN621-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 This is a CNF_UNS_RFO_NEQ_NHN problem
% 0.00/0.03 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n010.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 07:06:23 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % SZS status Unsatisfiable for theBenchmark
% 0.08/0.37 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------