%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : PUZ008-2 : TPTP v9.3.1. Released v1.0.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 : 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 08:54:17 AM UTC 2026
% Result : Unsatisfiable 0.05s 0.31s
% Output : Proof 0.05s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(bccc_mmm_to_cc_bmmmc,axiom,
( banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)
| ~ banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest) ),
file('theBenchmark.p',bccc_mmm_to_cc_bmmmc) ).
cnf(bmmmcc_c_to_mmmc_cc,axiom,
( banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatoneast)
| ~ banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest) ),
file('theBenchmark.p',bmmmcc_c_to_mmmc_cc) ).
cnf(bcc_mmmc_to_c_mmmcc,axiom,
( banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)
| ~ banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatonwest) ),
file('theBenchmark.p',bcc_mmmc_to_c_mmmcc) ).
cnf(bmmmc_cc_to_mmm_ccc,axiom,
( banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)
| ~ banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest) ),
file('theBenchmark.p',bmmmc_cc_to_mmm_ccc) ).
cnf(bc_mmmcc_to_x_bmmmccc,axiom,
( banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast)
| ~ banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatonwest) ),
file('theBenchmark.p',bc_mmmcc_to_x_bmmmccc) ).
cnf(bmmmccc_x_to_mmmc_bcc,axiom,
( banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatoneast)
| ~ banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest) ),
file('theBenchmark.p',bmmmccc_x_to_mmmc_bcc) ).
cnf(bccc_mmm_to_c_bmmmcc,axiom,
( banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)
| ~ banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest) ),
file('theBenchmark.p',bccc_mmm_to_c_bmmmcc) ).
cnf(bmmmcc_c_to_mmm_bccc,axiom,
( banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)
| ~ banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest) ),
file('theBenchmark.p',bmmmcc_c_to_mmm_bccc) ).
cnf(bcc_mmmc_to_x_bmmmccc,axiom,
( banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast)
| ~ banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatonwest) ),
file('theBenchmark.p',bcc_mmmc_to_x_bmmmccc) ).
cnf(cc_bmmmc_to_bccc_mmm,axiom,
( banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)
| ~ banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast) ),
file('theBenchmark.p',cc_bmmmc_to_bccc_mmm) ).
cnf(c_bmmmcc_to_bcc_mmmc,axiom,
( banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatonwest)
| ~ banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast) ),
file('theBenchmark.p',c_bmmmcc_to_bcc_mmmc) ).
cnf(mmm_bccc_to_bmmmc_cc,axiom,
( banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)
| ~ banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast) ),
file('theBenchmark.p',mmm_bccc_to_bmmmc_cc) ).
cnf(mmmcc_bc_to_bmmmccc_x,axiom,
( banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)
| ~ banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatoneast) ),
file('theBenchmark.p',mmmcc_bc_to_bmmmccc_x) ).
cnf(mmmc_bcc_to_bmmmcc_c,axiom,
( banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)
| ~ banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatoneast) ),
file('theBenchmark.p',mmmc_bcc_to_bmmmcc_c) ).
cnf(c_bmmmcc_to_bccc_mmm,axiom,
( banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)
| ~ banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast) ),
file('theBenchmark.p',c_bmmmcc_to_bccc_mmm) ).
cnf(mmmc_bcc_to_bmmmccc_x,axiom,
( banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)
| ~ banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatoneast) ),
file('theBenchmark.p',mmmc_bcc_to_bmmmccc_x) ).
cnf(mmm_bccc_to_bmmmcc_c,axiom,
( banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)
| ~ banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast) ),
file('theBenchmark.p',mmm_bccc_to_bmmmcc_c) ).
cnf(bmmmcc_c_to_mmcc_bmc,axiom,
( banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)
| ~ banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest) ),
file('theBenchmark.p',bmmmcc_c_to_mmcc_bmc) ).
cnf(bmc_mmcc_to_c_bmmmcc,axiom,
( banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)
| ~ banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest) ),
file('theBenchmark.p',bmc_mmcc_to_c_bmmmcc) ).
cnf(bmmmc_cc_to_mc_bmmcc,axiom,
( banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)
| ~ banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest) ),
file('theBenchmark.p',bmmmc_cc_to_mc_bmmcc) ).
cnf(bmmcc_mc_to_cc_bmmmc,axiom,
( banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)
| ~ banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest) ),
file('theBenchmark.p',bmmcc_mc_to_cc_bmmmc) ).
cnf(c_bmmmcc_to_bmc_mmcc,axiom,
( banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)
| ~ banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast) ),
file('theBenchmark.p',c_bmmmcc_to_bmc_mmcc) ).
cnf(mmcc_bmc_to_bmmmcc_c,axiom,
( banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)
| ~ banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast) ),
file('theBenchmark.p',mmcc_bmc_to_bmmmcc_c) ).
cnf(cc_bmmmc_to_bmmcc_mc,axiom,
( banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)
| ~ banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast) ),
file('theBenchmark.p',cc_bmmmc_to_bmmcc_mc) ).
cnf(mc_bmmcc_to_bmmmc_cc,axiom,
( banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)
| ~ banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast) ),
file('theBenchmark.p',mc_bmmcc_to_bmmmc_cc) ).
cnf(bmmmccc_x_to_mmcc_bmc,axiom,
( banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)
| ~ banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest) ),
file('theBenchmark.p',bmmmccc_x_to_mmcc_bmc) ).
cnf(bmmcc_mc_to_mc_bmmcc,axiom,
( banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)
| ~ banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest) ),
file('theBenchmark.p',bmmcc_mc_to_mc_bmmcc) ).
cnf(bmc_mmcc_to_x_bmmmccc,axiom,
( banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast)
| ~ banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest) ),
file('theBenchmark.p',bmc_mmcc_to_x_bmmmccc) ).
cnf(mc_bmmcc_to_bmmcc_mc,axiom,
( banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)
| ~ banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast) ),
file('theBenchmark.p',mc_bmmcc_to_bmmcc_mc) ).
cnf(mmcc_bmc_to_bmmmccc_x,axiom,
( banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)
| ~ banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast) ),
file('theBenchmark.p',mmcc_bmc_to_bmmmccc_x) ).
cnf(starting_configuration,hypothesis,
banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest),
file('theBenchmark.p',starting_configuration) ).
cnf(prove_can_get_across,negated_conjecture,
~ banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast),
file('theBenchmark.p',prove_can_get_across) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : PUZ008-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.01 This is a CNF_UNS_EPR_NEQ_HRN problem
% 0.00/0.02 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.05/0.30 % Computer : n012.cluster.edu
% 0.05/0.30 % Model : x86_64 x86_64
% 0.05/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.30 % Memory : 8046.5625MB
% 0.05/0.30 % OS : Linux 6.8.0-71-generic
% 0.05/0.30 % CPULimit : 300
% 0.05/0.30 % WCLimit : 300
% 0.05/0.30 % DateTime : Sat Sep 19 19:54:53 UTC 2026
% 0.05/0.30 % CPUTime :
% 0.05/0.31 % SZS status Unsatisfiable for theBenchmark
% 0.05/0.31 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------