%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SWV418-1.060 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:03:37 AM UTC 2026
% Result : Unsatisfiable 282.29s 282.68s
% Output : Proof 282.39s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(bound1,axiom,
succ(s0,s1),
file('theBenchmark.p',bound1) ).
cnf(bound2,axiom,
succ(s1,s2),
file('theBenchmark.p',bound2) ).
cnf(bound3,axiom,
succ(s2,s3),
file('theBenchmark.p',bound3) ).
cnf(bound4,axiom,
succ(s3,s4),
file('theBenchmark.p',bound4) ).
cnf(bound5,axiom,
succ(s4,s5),
file('theBenchmark.p',bound5) ).
cnf(bound6,axiom,
succ(s5,s6),
file('theBenchmark.p',bound6) ).
cnf(bound7,axiom,
succ(s6,s7),
file('theBenchmark.p',bound7) ).
cnf(bound8,axiom,
succ(s7,s8),
file('theBenchmark.p',bound8) ).
cnf(bound9,axiom,
succ(s8,s9),
file('theBenchmark.p',bound9) ).
cnf(bound10,axiom,
succ(s9,s10),
file('theBenchmark.p',bound10) ).
cnf(bound11,axiom,
succ(s10,s11),
file('theBenchmark.p',bound11) ).
cnf(bound12,axiom,
succ(s11,s12),
file('theBenchmark.p',bound12) ).
cnf(bound13,axiom,
succ(s12,s13),
file('theBenchmark.p',bound13) ).
cnf(bound14,axiom,
succ(s13,s14),
file('theBenchmark.p',bound14) ).
cnf(bound15,axiom,
succ(s14,s15),
file('theBenchmark.p',bound15) ).
cnf(bound16,axiom,
succ(s15,s16),
file('theBenchmark.p',bound16) ).
cnf(bound17,axiom,
succ(s16,s17),
file('theBenchmark.p',bound17) ).
cnf(bound18,axiom,
succ(s17,s18),
file('theBenchmark.p',bound18) ).
cnf(bound19,axiom,
succ(s18,s19),
file('theBenchmark.p',bound19) ).
cnf(bound20,axiom,
succ(s19,s20),
file('theBenchmark.p',bound20) ).
cnf(bound21,axiom,
succ(s20,s21),
file('theBenchmark.p',bound21) ).
cnf(bound22,axiom,
succ(s21,s22),
file('theBenchmark.p',bound22) ).
cnf(bound23,axiom,
succ(s22,s23),
file('theBenchmark.p',bound23) ).
cnf(bound24,axiom,
succ(s23,s24),
file('theBenchmark.p',bound24) ).
cnf(bound25,axiom,
succ(s24,s25),
file('theBenchmark.p',bound25) ).
cnf(bound26,axiom,
succ(s25,s26),
file('theBenchmark.p',bound26) ).
cnf(bound27,axiom,
succ(s26,s27),
file('theBenchmark.p',bound27) ).
cnf(bound28,axiom,
succ(s27,s28),
file('theBenchmark.p',bound28) ).
cnf(bound29,axiom,
succ(s28,s29),
file('theBenchmark.p',bound29) ).
cnf(bound30,axiom,
succ(s29,s30),
file('theBenchmark.p',bound30) ).
cnf(bound31,axiom,
succ(s30,s31),
file('theBenchmark.p',bound31) ).
cnf(bound32,axiom,
succ(s31,s32),
file('theBenchmark.p',bound32) ).
cnf(bound33,axiom,
succ(s32,s33),
file('theBenchmark.p',bound33) ).
cnf(bound34,axiom,
succ(s33,s34),
file('theBenchmark.p',bound34) ).
cnf(bound35,axiom,
succ(s34,s35),
file('theBenchmark.p',bound35) ).
cnf(bound36,axiom,
succ(s35,s36),
file('theBenchmark.p',bound36) ).
cnf(bound37,axiom,
succ(s36,s37),
file('theBenchmark.p',bound37) ).
cnf(bound38,axiom,
succ(s37,s38),
file('theBenchmark.p',bound38) ).
cnf(bound39,axiom,
succ(s38,s39),
file('theBenchmark.p',bound39) ).
cnf(bound40,axiom,
succ(s39,s40),
file('theBenchmark.p',bound40) ).
cnf(bound41,axiom,
succ(s40,s41),
file('theBenchmark.p',bound41) ).
cnf(bound42,axiom,
succ(s41,s42),
file('theBenchmark.p',bound42) ).
cnf(bound43,axiom,
succ(s42,s43),
file('theBenchmark.p',bound43) ).
cnf(bound44,axiom,
succ(s43,s44),
file('theBenchmark.p',bound44) ).
cnf(bound45,axiom,
succ(s44,s45),
file('theBenchmark.p',bound45) ).
cnf(bound46,axiom,
succ(s45,s46),
file('theBenchmark.p',bound46) ).
cnf(bound47,axiom,
succ(s46,s47),
file('theBenchmark.p',bound47) ).
cnf(bound48,axiom,
succ(s47,s48),
file('theBenchmark.p',bound48) ).
cnf(bound49,axiom,
succ(s48,s49),
file('theBenchmark.p',bound49) ).
cnf(bound50,axiom,
succ(s49,s50),
file('theBenchmark.p',bound50) ).
cnf(bound51,axiom,
succ(s50,s51),
file('theBenchmark.p',bound51) ).
cnf(bound52,axiom,
succ(s51,s52),
file('theBenchmark.p',bound52) ).
cnf(bound53,axiom,
succ(s52,s53),
file('theBenchmark.p',bound53) ).
cnf(bound54,axiom,
succ(s53,s54),
file('theBenchmark.p',bound54) ).
cnf(bound55,axiom,
succ(s54,s55),
file('theBenchmark.p',bound55) ).
cnf(bound56,axiom,
succ(s55,s56),
file('theBenchmark.p',bound56) ).
cnf(bound57,axiom,
succ(s56,s57),
file('theBenchmark.p',bound57) ).
cnf(bound58,axiom,
succ(s57,s58),
file('theBenchmark.p',bound58) ).
cnf(bound59,axiom,
succ(s58,s59),
file('theBenchmark.p',bound59) ).
cnf(bound60,axiom,
last(s59),
file('theBenchmark.p',bound60) ).
cnf(bound61,axiom,
( trans(X,Y)
| ~ succ(X,Y) ),
file('theBenchmark.p',bound61) ).
cnf(bound62,axiom,
( trans(s59,s59)
| trans(s59,s58)
| trans(s59,s57)
| trans(s59,s56)
| trans(s59,s55)
| trans(s59,s54)
| trans(s59,s53)
| trans(s59,s52)
| trans(s59,s51)
| trans(s59,s50)
| trans(s59,s49)
| trans(s59,s48)
| trans(s59,s47)
| trans(s59,s46)
| trans(s59,s45)
| trans(s59,s44)
| trans(s59,s43)
| trans(s59,s42)
| trans(s59,s41)
| trans(s59,s40)
| trans(s59,s39)
| trans(s59,s38)
| trans(s59,s37)
| trans(s59,s36)
| trans(s59,s35)
| trans(s59,s34)
| trans(s59,s33)
| trans(s59,s32)
| trans(s59,s31)
| trans(s59,s30)
| trans(s59,s29)
| trans(s59,s28)
| trans(s59,s27)
| trans(s59,s26)
| trans(s59,s25)
| trans(s59,s24)
| trans(s59,s23)
| trans(s59,s22)
| trans(s59,s21)
| trans(s59,s20)
| trans(s59,s19)
| trans(s59,s18)
| trans(s59,s17)
| trans(s59,s16)
| trans(s59,s15)
| trans(s59,s14)
| trans(s59,s13)
| trans(s59,s12)
| trans(s59,s11)
| trans(s59,s10)
| trans(s59,s9)
| trans(s59,s8)
| trans(s59,s7)
| trans(s59,s6)
| trans(s59,s5)
| trans(s59,s4)
| trans(s59,s3)
| trans(s59,s2)
| trans(s59,s1)
| trans(s59,s0)
| ~ loop ),
file('theBenchmark.p',bound62) ).
cnf(m_main_1,axiom,
m_counter_cell_v_carry_in(c_bit0,X),
file('theBenchmark.p',m_main_1) ).
cnf(m_main_2,axiom,
( ~ m_counter_cell_v_carry_out(c_bit0,X)
| m_counter_cell_v_carry_in(c_bit1,X) ),
file('theBenchmark.p',m_main_2) ).
cnf(m_main_3,axiom,
( m_counter_cell_v_carry_out(c_bit0,X)
| ~ m_counter_cell_v_carry_in(c_bit1,X) ),
file('theBenchmark.p',m_main_3) ).
cnf(m_main_4,axiom,
( ~ m_counter_cell_v_carry_out(c_bit1,X)
| m_counter_cell_v_carry_in(c_bit2,X) ),
file('theBenchmark.p',m_main_4) ).
cnf(m_main_5,axiom,
( m_counter_cell_v_carry_out(c_bit1,X)
| ~ m_counter_cell_v_carry_in(c_bit2,X) ),
file('theBenchmark.p',m_main_5) ).
cnf(m_counter_cell_1,axiom,
~ m_counter_cell_v_value(I0,s0),
file('theBenchmark.p',m_counter_cell_1) ).
cnf(m_counter_cell_2,axiom,
( ~ node1(I0,X)
| ~ m_counter_cell_v_carry_in(I0,X)
| m_counter_cell_v_value(I0,X) ),
file('theBenchmark.p',m_counter_cell_2) ).
cnf(m_counter_cell_3,axiom,
( ~ node1(I0,X)
| m_counter_cell_v_carry_in(I0,X)
| ~ m_counter_cell_v_value(I0,X) ),
file('theBenchmark.p',m_counter_cell_3) ).
cnf(m_counter_cell_4,axiom,
( ~ node2(I0,X)
| m_counter_cell_v_carry_in(I0,X)
| m_counter_cell_v_value(I0,X) ),
file('theBenchmark.p',m_counter_cell_4) ).
cnf(m_counter_cell_5,axiom,
( ~ node2(I0,X)
| ~ m_counter_cell_v_carry_in(I0,X)
| ~ m_counter_cell_v_value(I0,X) ),
file('theBenchmark.p',m_counter_cell_5) ).
cnf(m_counter_cell_6,axiom,
( ~ node3(I0,X,Y)
| node1(I0,X)
| m_counter_cell_v_value(I0,Y) ),
file('theBenchmark.p',m_counter_cell_6) ).
cnf(m_counter_cell_7,axiom,
( ~ node3(I0,X,Y)
| node2(I0,X)
| ~ m_counter_cell_v_value(I0,Y) ),
file('theBenchmark.p',m_counter_cell_7) ).
cnf(m_counter_cell_8,axiom,
( node3(I0,X,Y)
| ~ trans(X,Y) ),
file('theBenchmark.p',m_counter_cell_8) ).
cnf(m_counter_cell_9,axiom,
( ~ node4(I0,X)
| m_counter_cell_v_value(I0,X) ),
file('theBenchmark.p',m_counter_cell_9) ).
cnf(m_counter_cell_10,axiom,
( ~ node4(I0,X)
| m_counter_cell_v_carry_in(I0,X) ),
file('theBenchmark.p',m_counter_cell_10) ).
cnf(m_counter_cell_11,axiom,
( ~ m_counter_cell_v_carry_in(I0,X)
| ~ m_counter_cell_v_value(I0,X)
| m_counter_cell_v_carry_out(I0,X) ),
file('theBenchmark.p',m_counter_cell_11) ).
cnf(m_counter_cell_12,axiom,
( node4(I0,X)
| ~ m_counter_cell_v_carry_out(I0,X) ),
file('theBenchmark.p',m_counter_cell_12) ).
cnf(prpty1,negated_conjecture,
( ~ always5(X)
| ~ m_counter_cell_v_carry_out(c_bit2,X) ),
file('theBenchmark.p',prpty1) ).
cnf(prpty2,negated_conjecture,
( ~ always5(X)
| ~ trans(X,Y)
| always5(Y) ),
file('theBenchmark.p',prpty2) ).
cnf(prpty3,negated_conjecture,
( ~ last(X)
| ~ always5(X)
| loop ),
file('theBenchmark.p',prpty3) ).
cnf(prpty4,negated_conjecture,
( ~ until6(X)
| xuntil7(X)
| always5(X) ),
file('theBenchmark.p',prpty4) ).
cnf(prpty5,negated_conjecture,
( ~ xuntil7(X)
| ~ succ(X,Y)
| until6(Y) ),
file('theBenchmark.p',prpty5) ).
cnf(prpty6,negated_conjecture,
( ~ xuntil7(X)
| ~ last(X)
| loop ),
file('theBenchmark.p',prpty6) ).
cnf(prpty7,negated_conjecture,
( ~ xuntil7(X)
| ~ last(X)
| ~ trans(X,Y)
| until2p8(Y) ),
file('theBenchmark.p',prpty7) ).
cnf(prpty8,negated_conjecture,
( ~ until2p8(X)
| xuntil2p9(X)
| always5(X) ),
file('theBenchmark.p',prpty8) ).
cnf(prpty9,negated_conjecture,
( ~ xuntil2p9(X)
| ~ succ(X,Y)
| until2p8(Y) ),
file('theBenchmark.p',prpty9) ).
cnf(prpty10,negated_conjecture,
( ~ xuntil2p9(X)
| ~ last(X) ),
file('theBenchmark.p',prpty10) ).
cnf(prpty11,negated_conjecture,
until6(s0),
file('theBenchmark.p',prpty11) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV418-1.060 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.03 This is a CNF_UNS_EPR_NEQ_NHN problem
% 0.00/0.03 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.42 % Computer : n011.cluster.edu
% 0.08/0.42 % Model : x86_64 x86_64
% 0.08/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.42 % Memory : 8046.5625MB
% 0.08/0.42 % OS : Linux 6.8.0-71-generic
% 0.08/0.42 % CPULimit : 300
% 0.08/0.42 % WCLimit : 300
% 0.08/0.42 % DateTime : Sun Sep 20 03:31:54 UTC 2026
% 0.08/0.42 % CPUTime :
% 282.29/282.68 % SZS status Unsatisfiable for theBenchmark
% 282.29/282.68 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------