%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN625-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 : n012.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:44 AM UTC 2026
% Result : Unsatisfiable 0.08s 0.32s
% Output : Proof 0.08s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c21_is_p15_1,negated_conjecture,
p15(c21),
file('theBenchmark.p',c21_is_p15_1) ).
cnf(p10_2,negated_conjecture,
p10(X0,X0),
file('theBenchmark.p',p10_2) ).
cnf(p8_3,negated_conjecture,
p8(X71,X71),
file('theBenchmark.p',p8_3) ).
cnf(p6_4,negated_conjecture,
p6(X68,X68),
file('theBenchmark.p',p6_4) ).
cnf(p5_5,negated_conjecture,
p5(X47,X47),
file('theBenchmark.p',p5_5) ).
cnf(p3_6,negated_conjecture,
p3(X40,X40),
file('theBenchmark.p',p3_6) ).
cnf(p2_7,negated_conjecture,
p2(X33,X33),
file('theBenchmark.p',p2_7) ).
cnf(f4_is_not_p15_8,negated_conjecture,
~ p15(f4(f7(c19,c20),c21)),
file('theBenchmark.p',f4_is_not_p15_8) ).
cnf(p16_9,negated_conjecture,
( ~ p5(X15,X16)
| p16(X14,X15,X16) ),
file('theBenchmark.p',p16_9) ).
cnf(not_p15_10,negated_conjecture,
( ~ p18(f9(X7),X76,X76)
| ~ p15(X7) ),
file('theBenchmark.p',not_p15_10) ).
cnf(p15_11,negated_conjecture,
( ~ p3(X6,X5)
| ~ p15(X6)
| p15(X5) ),
file('theBenchmark.p',p15_11) ).
cnf(p10_12,negated_conjecture,
( ~ p6(X3,X4)
| p10(f11(X3),f11(X4)) ),
file('theBenchmark.p',p10_12) ).
cnf(p8_13,negated_conjecture,
( ~ p3(X74,X75)
| p8(f9(X74),f9(X75)) ),
file('theBenchmark.p',p8_13) ).
cnf(p5_14,negated_conjecture,
( ~ p3(X66,X67)
| p5(f14(X66),f14(X67)) ),
file('theBenchmark.p',p5_14) ).
cnf(p15_15,negated_conjecture,
( p18(f9(X7),f14(X7),f14(X7))
| p15(X7) ),
file('theBenchmark.p',p15_15) ).
cnf(not_p17_16,negated_conjecture,
( ~ p16(f9(c21),X77,c19)
| ~ p17(X77,f11(c20)) ),
file('theBenchmark.p',not_p17_16) ).
cnf(p10_17,negated_conjecture,
( ~ p10(X0,X2)
| ~ p10(X0,X1)
| p10(X1,X2) ),
file('theBenchmark.p',p10_17) ).
cnf(p8_18,negated_conjecture,
( ~ p8(X71,X73)
| ~ p8(X71,X72)
| p8(X72,X73) ),
file('theBenchmark.p',p8_18) ).
cnf(p6_19,negated_conjecture,
( ~ p6(X68,X70)
| ~ p6(X68,X69)
| p6(X69,X70) ),
file('theBenchmark.p',p6_19) ).
cnf(p5_20,negated_conjecture,
( ~ p5(X47,X49)
| ~ p5(X47,X48)
| p5(X48,X49) ),
file('theBenchmark.p',p5_20) ).
cnf(p3_21,negated_conjecture,
( ~ p3(X40,X42)
| ~ p3(X40,X41)
| p3(X41,X42) ),
file('theBenchmark.p',p3_21) ).
cnf(p2_22,negated_conjecture,
( ~ p2(X33,X35)
| ~ p2(X33,X34)
| p2(X34,X35) ),
file('theBenchmark.p',p2_22) ).
cnf(p16_23,negated_conjecture,
( ~ p16(X14,X17,X16)
| ~ p16(X14,X15,X17)
| p16(X14,X15,X16) ),
file('theBenchmark.p',p16_23) ).
cnf(p17_24,negated_conjecture,
( ~ p10(X25,X24)
| ~ p5(X26,X23)
| ~ p17(X26,X25)
| p17(X23,X24) ),
file('theBenchmark.p',p17_24) ).
cnf(p3_25,negated_conjecture,
( ~ p3(X44,X46)
| ~ p2(X43,X45)
| p3(f4(X43,X44),f4(X45,X46)) ),
file('theBenchmark.p',p3_25) ).
cnf(p2_26,negated_conjecture,
( ~ p6(X37,X39)
| ~ p5(X36,X38)
| p2(f7(X36,X37),f7(X38,X39)) ),
file('theBenchmark.p',p2_26) ).
cnf(p5_27,negated_conjecture,
( ~ p16(X14,X15,X16)
| p16(X14,X15,f13(X14,X15,X16))
| p5(X15,X16) ),
file('theBenchmark.p',p5_27) ).
cnf(p5_28,negated_conjecture,
( ~ p16(X14,X15,X16)
| p16(X14,f13(X14,X15,X16),X16)
| p5(X15,X16) ),
file('theBenchmark.p',p5_28) ).
cnf(p16_29,negated_conjecture,
( ~ p16(X11,X12,X13)
| ~ p5(X12,X9)
| ~ p5(X13,X10)
| ~ p8(X11,X8)
| p16(X8,X9,X10) ),
file('theBenchmark.p',p16_29) ).
cnf(p18_30,negated_conjecture,
( ~ p18(X30,X31,X32)
| ~ p5(X31,X28)
| ~ p5(X32,X29)
| ~ p8(X30,X27)
| p18(X27,X28,X29) ),
file('theBenchmark.p',p18_30) ).
cnf(p5_31,negated_conjecture,
( ~ p5(X61,X64)
| ~ p8(X60,X63)
| ~ p5(X62,X65)
| p5(f13(X60,X61,X62),f13(X63,X64,X65)) ),
file('theBenchmark.p',p5_31) ).
cnf(p16_32,negated_conjecture,
( ~ p18(f9(f4(f7(X20,X22),X18)),X19,X21)
| p18(f9(X18),X19,X21)
| p16(f9(X18),X19,X20) ),
file('theBenchmark.p',p16_32) ).
cnf(p18_33,negated_conjecture,
( ~ p18(f9(f4(f7(X20,X22),X18)),X19,X21)
| p17(f12(X18,X20,X22,X19,X21),f11(X22))
| p18(f9(X18),X19,X21) ),
file('theBenchmark.p',p18_33) ).
cnf(p18_34,negated_conjecture,
( ~ p18(f9(f4(f7(X20,X22),X18)),X19,X21)
| p16(f9(X18),f12(X18,X20,X22,X19,X21),X21)
| p18(f9(X18),X19,X21) ),
file('theBenchmark.p',p18_34) ).
cnf(p5_35,negated_conjecture,
( ~ p5(X53,X58)
| ~ p5(X51,X56)
| ~ p3(X50,X55)
| ~ p6(X52,X57)
| ~ p5(X54,X59)
| p5(f12(X50,X51,X52,X53,X54),f12(X55,X56,X57,X58,X59)) ),
file('theBenchmark.p',p5_35) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN625-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.01 This is a CNF_UNS_RFO_NEQ_NHN problem
% 0.00/0.02 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.04/0.29 % Computer : n012.cluster.edu
% 0.04/0.29 % Model : x86_64 x86_64
% 0.04/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.29 % Memory : 8046.5625MB
% 0.04/0.29 % OS : Linux 6.8.0-71-generic
% 0.04/0.29 % CPULimit : 300
% 0.04/0.29 % WCLimit : 300
% 0.04/0.29 % DateTime : Sun Sep 20 07:05:52 UTC 2026
% 0.04/0.29 % CPUTime :
% 0.08/0.32 % SZS status Unsatisfiable for theBenchmark
% 0.08/0.32 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------