%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : PUZ030-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 : n018.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:20 AM UTC 2026
% Result : Unsatisfiable 0.14s 5.42s
% Output : Proof 0.14s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c1,hypothesis,
( mustard_lang
| mustard_barry
| ~ salt_mill ),
file('theBenchmark.p',c1) ).
cnf(c2,hypothesis,
( salt_lang
| mustard_barry
| ~ salt_mill ),
file('theBenchmark.p',c2) ).
cnf(c3,hypothesis,
( mustard_lang
| salt_barry
| ~ salt_mill ),
file('theBenchmark.p',c3) ).
cnf(c4,hypothesis,
( salt_lang
| salt_barry
| ~ salt_mill ),
file('theBenchmark.p',c4) ).
cnf(c5,hypothesis,
( ~ mustard_mill
| ~ mustard_cole
| ~ mustard_lang ),
file('theBenchmark.p',c5) ).
cnf(c6,hypothesis,
( ~ salt_mill
| ~ mustard_cole
| ~ mustard_lang ),
file('theBenchmark.p',c6) ).
cnf(c7,hypothesis,
( ~ mustard_mill
| ~ salt_cole
| ~ mustard_lang ),
file('theBenchmark.p',c7) ).
cnf(c8,hypothesis,
( ~ salt_mill
| ~ salt_cole
| ~ mustard_lang ),
file('theBenchmark.p',c8) ).
cnf(c9,hypothesis,
( ~ mustard_mill
| ~ mustard_lang
| ~ mustard_dix ),
file('theBenchmark.p',c9) ).
cnf(c10,hypothesis,
( ~ salt_mill
| ~ mustard_lang
| ~ mustard_dix ),
file('theBenchmark.p',c10) ).
cnf(c11,hypothesis,
( ~ mustard_mill
| ~ salt_lang
| ~ mustard_dix ),
file('theBenchmark.p',c11) ).
cnf(c12,hypothesis,
( ~ salt_mill
| ~ salt_lang
| ~ mustard_dix ),
file('theBenchmark.p',c12) ).
cnf(c13,hypothesis,
( mustard_cole
| ~ mustard_barry
| ~ salt_dix ),
file('theBenchmark.p',c13) ).
cnf(c14,hypothesis,
( salt_cole
| ~ mustard_barry
| ~ salt_dix ),
file('theBenchmark.p',c14) ).
cnf(c15,hypothesis,
( mustard_cole
| ~ salt_barry
| ~ salt_dix ),
file('theBenchmark.p',c15) ).
cnf(c16,hypothesis,
( salt_cole
| ~ salt_barry
| ~ salt_dix ),
file('theBenchmark.p',c16) ).
cnf(c17,hypothesis,
( mustard_lang
| mustard_dix
| ~ mustard_cole ),
file('theBenchmark.p',c17) ).
cnf(c18,hypothesis,
( salt_lang
| mustard_dix
| ~ mustard_cole ),
file('theBenchmark.p',c18) ).
cnf(c19,hypothesis,
( mustard_lang
| salt_dix
| ~ mustard_cole ),
file('theBenchmark.p',c19) ).
cnf(c20,hypothesis,
( salt_lang
| salt_dix
| ~ mustard_cole ),
file('theBenchmark.p',c20) ).
cnf(c21,hypothesis,
( mustard_mill
| ~ mustard_dix
| ~ mustard_barry ),
file('theBenchmark.p',c21) ).
cnf(c22,hypothesis,
( salt_mill
| ~ mustard_dix
| ~ mustard_barry ),
file('theBenchmark.p',c22) ).
cnf(c23,hypothesis,
( mustard_mill
| ~ salt_dix
| ~ mustard_barry ),
file('theBenchmark.p',c23) ).
cnf(c24,hypothesis,
( salt_mill
| ~ salt_dix
| ~ mustard_barry ),
file('theBenchmark.p',c24) ).
cnf(c25,hypothesis,
( mustard_mill
| ~ mustard_dix
| salt_dix ),
file('theBenchmark.p',c25) ).
cnf(c26,hypothesis,
( mustard_mill
| mustard_dix
| ~ salt_dix ),
file('theBenchmark.p',c26) ).
cnf(c27,hypothesis,
( mustard_mill
| ~ mustard_cole
| salt_cole ),
file('theBenchmark.p',c27) ).
cnf(c28,hypothesis,
( mustard_mill
| mustard_cole
| ~ salt_cole ),
file('theBenchmark.p',c28) ).
cnf(c29,hypothesis,
( salt_mill
| ~ mustard_lang
| ~ salt_lang ),
file('theBenchmark.p',c29) ).
cnf(c30,hypothesis,
( salt_mill
| ~ mustard_barry
| ~ salt_barry ),
file('theBenchmark.p',c30) ).
cnf(c31,hypothesis,
( salt_lang
| ~ mustard_dix
| salt_dix ),
file('theBenchmark.p',c31) ).
cnf(c32,hypothesis,
( salt_lang
| mustard_dix
| ~ salt_dix ),
file('theBenchmark.p',c32) ).
cnf(c33,hypothesis,
( salt_lang
| ~ mustard_barry
| salt_barry ),
file('theBenchmark.p',c33) ).
cnf(c34,hypothesis,
( salt_lang
| mustard_barry
| ~ salt_barry ),
file('theBenchmark.p',c34) ).
cnf(c35,hypothesis,
( salt_dix
| ~ mustard_cole
| ~ salt_cole ),
file('theBenchmark.p',c35) ).
cnf(c36,hypothesis,
( mustard_cole
| ~ mustard_lang
| ~ salt_lang ),
file('theBenchmark.p',c36) ).
cnf(c37,hypothesis,
( mustard_cole
| ~ mustard_dix
| ~ salt_dix ),
file('theBenchmark.p',c37) ).
cnf(c38,hypothesis,
( salt_cole
| ~ mustard_barry
| salt_barry ),
file('theBenchmark.p',c38) ).
cnf(c39,hypothesis,
( salt_cole
| mustard_barry
| ~ salt_barry ),
file('theBenchmark.p',c39) ).
cnf(c40,hypothesis,
( mustard_barry
| ~ mustard_mill
| ~ salt_mill ),
file('theBenchmark.p',c40) ).
cnf(c41,hypothesis,
( salt_barry
| ~ mustard_lang
| salt_lang ),
file('theBenchmark.p',c41) ).
cnf(c42,hypothesis,
( salt_barry
| mustard_lang
| ~ salt_lang ),
file('theBenchmark.p',c42) ).
cnf(c43,hypothesis,
( salt_barry
| ~ mustard_cole
| salt_cole ),
file('theBenchmark.p',c43) ).
cnf(c44,hypothesis,
( salt_barry
| mustard_cole
| ~ salt_cole ),
file('theBenchmark.p',c44) ).
cnf(c45,hypothesis,
( ~ mustard_mill
| ~ salt_barry
| ~ mustard_barry
| ~ salt_cole ),
file('theBenchmark.p',c45) ).
cnf(c46,hypothesis,
( ~ salt_mill
| ~ salt_barry
| ~ mustard_barry
| ~ salt_cole ),
file('theBenchmark.p',c46) ).
cnf(c47,hypothesis,
( ~ mustard_mill
| mustard_barry
| salt_barry
| ~ salt_cole ),
file('theBenchmark.p',c47) ).
cnf(c48,hypothesis,
( ~ salt_mill
| mustard_barry
| salt_barry
| ~ salt_cole ),
file('theBenchmark.p',c48) ).
cnf(c49,hypothesis,
( ~ salt_dix
| ~ mustard_dix
| ~ salt_cole
| ~ mustard_cole
| ~ mustard_mill ),
file('theBenchmark.p',c49) ).
cnf(c50,hypothesis,
( mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_mill ),
file('theBenchmark.p',c50) ).
cnf(c51,hypothesis,
( ~ salt_dix
| ~ mustard_dix
| ~ salt_barry
| ~ mustard_barry
| ~ salt_lang ),
file('theBenchmark.p',c51) ).
cnf(c52,hypothesis,
( mustard_dix
| salt_dix
| ~ salt_barry
| ~ mustard_barry
| ~ salt_lang ),
file('theBenchmark.p',c52) ).
cnf(c53,hypothesis,
( ~ salt_dix
| ~ mustard_dix
| mustard_barry
| salt_barry
| ~ salt_lang ),
file('theBenchmark.p',c53) ).
cnf(c54,hypothesis,
( ~ salt_lang
| ~ mustard_lang
| ~ salt_cole
| ~ mustard_cole
| ~ salt_barry ),
file('theBenchmark.p',c54) ).
cnf(c55,hypothesis,
( mustard_lang
| salt_lang
| ~ salt_cole
| ~ mustard_cole
| ~ salt_barry ),
file('theBenchmark.p',c55) ).
cnf(c56,hypothesis,
( mustard_lang
| mustard_mill
| salt_mill ),
file('theBenchmark.p',c56) ).
cnf(c57,hypothesis,
( mustard_lang
| mustard_cole
| salt_cole ),
file('theBenchmark.p',c57) ).
cnf(c58,hypothesis,
( mustard_dix
| mustard_mill
| salt_mill ),
file('theBenchmark.p',c58) ).
cnf(c59,hypothesis,
( mustard_dix
| mustard_lang
| salt_lang ),
file('theBenchmark.p',c59) ).
cnf(c60,hypothesis,
( salt_dix
| mustard_barry
| salt_barry ),
file('theBenchmark.p',c60) ).
cnf(c61,hypothesis,
( salt_cole
| mustard_mill
| salt_mill ),
file('theBenchmark.p',c61) ).
cnf(c62,hypothesis,
( mustard_barry
| mustard_dix
| salt_dix ),
file('theBenchmark.p',c62) ).
cnf(prove_who_takes_what,negated_conjecture,
( mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_lang
| ~ salt_mill
| ~ salt_barry
| ~ mustard_barry
| salt_lang ),
file('theBenchmark.p',prove_who_takes_what) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ030-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 This is a CNF_UNS_PRP problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.39 % Computer : n018.cluster.edu
% 0.10/5.39 % Model : x86_64 x86_64
% 0.10/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.39 % Memory : 8046.5625MB
% 0.10/5.39 % OS : Linux 6.8.0-71-generic
% 0.10/5.39 % CPULimit : 300
% 0.10/5.39 % WCLimit : 300
% 0.10/5.39 % DateTime : Sat Sep 19 19:59:48 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.14/5.42 % SZS status Unsatisfiable for theBenchmark
% 0.14/5.42 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------