%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : PUZ030-1 : TPTP v9.3.1. Released v1.0.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 : 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 08:54:20 AM UTC 2026
% Result : Unsatisfiable 0.23s 0.48s
% Output : Proof 0.23s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(both1,axiom,
( salt(X)
| ~ both(X) ),
file('theBenchmark.p',both1) ).
cnf(both2,axiom,
( mustard(X)
| ~ both(X) ),
file('theBenchmark.p',both2) ).
cnf(both3,axiom,
( both(X)
| ~ mustard(X)
| ~ salt(X) ),
file('theBenchmark.p',both3) ).
cnf(oneof1,axiom,
( mustard(X)
| salt(X)
| ~ oneof(X) ),
file('theBenchmark.p',oneof1) ).
cnf(oneof2,axiom,
( ~ both(X)
| ~ oneof(X) ),
file('theBenchmark.p',oneof2) ).
cnf(oneof3,axiom,
( ~ neither(X)
| ~ oneof(X) ),
file('theBenchmark.p',oneof3) ).
cnf(one_condition_holds1,axiom,
( oneof(X)
| neither(X)
| both(X) ),
file('theBenchmark.p',one_condition_holds1) ).
cnf(oneof4,axiom,
( ~ mustard(X)
| ~ salt(X)
| ~ oneof(X) ),
file('theBenchmark.p',oneof4) ).
cnf(neither1,axiom,
( ~ neither(X)
| ~ both(X) ),
file('theBenchmark.p',neither1) ).
cnf(neither2,axiom,
( ~ salt(X)
| ~ neither(X) ),
file('theBenchmark.p',neither2) ).
cnf(neither3,axiom,
( ~ mustard(X)
| ~ neither(X) ),
file('theBenchmark.p',neither3) ).
cnf(neither4,axiom,
( neither(X)
| mustard(X)
| salt(X) ),
file('theBenchmark.p',neither4) ).
cnf(rule1_1,hypothesis,
( oneof(lang)
| oneof(cole)
| ~ salt(barry) ),
file('theBenchmark.p',rule1_1) ).
cnf(rule1_2,hypothesis,
( salt(barry)
| ~ oneof(cole) ),
file('theBenchmark.p',rule1_2) ).
cnf(rule1_3,hypothesis,
( salt(barry)
| ~ oneof(lang) ),
file('theBenchmark.p',rule1_3) ).
cnf(rule2_1,hypothesis,
( both(mill)
| neither(dix)
| ~ mustard(barry) ),
file('theBenchmark.p',rule2_1) ).
cnf(rule2_2,hypothesis,
( mustard(barry)
| ~ neither(dix) ),
file('theBenchmark.p',rule2_2) ).
cnf(rule2_3,hypothesis,
( mustard(barry)
| ~ both(mill) ),
file('theBenchmark.p',rule2_3) ).
cnf(rule3_1,hypothesis,
( neither(mill)
| oneof(barry)
| ~ salt(cole) ),
file('theBenchmark.p',rule3_1) ).
cnf(rule3_2,hypothesis,
( salt(cole)
| ~ oneof(barry) ),
file('theBenchmark.p',rule3_2) ).
cnf(rule3_3,hypothesis,
( salt(cole)
| ~ neither(mill) ),
file('theBenchmark.p',rule3_3) ).
cnf(rule4_1,hypothesis,
( both(lang)
| both(dix)
| ~ mustard(cole) ),
file('theBenchmark.p',rule4_1) ).
cnf(rule4_2,hypothesis,
( mustard(cole)
| ~ both(dix) ),
file('theBenchmark.p',rule4_2) ).
cnf(rule4_3,hypothesis,
( mustard(cole)
| ~ both(lang) ),
file('theBenchmark.p',rule4_3) ).
cnf(rule5_1,hypothesis,
( both(cole)
| neither(barry)
| ~ salt(dix) ),
file('theBenchmark.p',rule5_1) ).
cnf(rule5_2,hypothesis,
( salt(dix)
| ~ neither(barry) ),
file('theBenchmark.p',rule5_2) ).
cnf(rule5_3,hypothesis,
( salt(dix)
| ~ both(cole) ),
file('theBenchmark.p',rule5_3) ).
cnf(rule6_1,hypothesis,
( neither(mill)
| neither(lang)
| ~ mustard(dix) ),
file('theBenchmark.p',rule6_1) ).
cnf(rule6_2,hypothesis,
( mustard(dix)
| ~ neither(lang) ),
file('theBenchmark.p',rule6_2) ).
cnf(rule6_3,hypothesis,
( mustard(dix)
| ~ neither(mill) ),
file('theBenchmark.p',rule6_3) ).
cnf(rule7_1,hypothesis,
( oneof(dix)
| oneof(barry)
| ~ salt(lang) ),
file('theBenchmark.p',rule7_1) ).
cnf(rule7_2,hypothesis,
( salt(lang)
| ~ oneof(barry) ),
file('theBenchmark.p',rule7_2) ).
cnf(rule7_3,hypothesis,
( salt(lang)
| ~ oneof(dix) ),
file('theBenchmark.p',rule7_3) ).
cnf(rule8_1,hypothesis,
( neither(mill)
| neither(cole)
| ~ mustard(lang) ),
file('theBenchmark.p',rule8_1) ).
cnf(rule8_2,hypothesis,
( mustard(lang)
| ~ neither(cole) ),
file('theBenchmark.p',rule8_2) ).
cnf(rule8_3,hypothesis,
( mustard(lang)
| ~ neither(mill) ),
file('theBenchmark.p',rule8_3) ).
cnf(rule9_1,hypothesis,
( both(lang)
| both(barry)
| ~ salt(mill) ),
file('theBenchmark.p',rule9_1) ).
cnf(rule9_2,hypothesis,
( salt(mill)
| ~ both(barry) ),
file('theBenchmark.p',rule9_2) ).
cnf(rule9_3,hypothesis,
( mustard(mill)
| ~ both(lang) ),
file('theBenchmark.p',rule9_3) ).
cnf(rule10_1,hypothesis,
( oneof(dix)
| oneof(cole)
| ~ mustard(mill) ),
file('theBenchmark.p',rule10_1) ).
cnf(rule10_2,hypothesis,
( mustard(mill)
| ~ oneof(cole) ),
file('theBenchmark.p',rule10_2) ).
cnf(rule10_3,hypothesis,
( mustard(mill)
| ~ oneof(dix) ),
file('theBenchmark.p',rule10_3) ).
cnf(prove_who_takes_what,negated_conjecture,
( ~ oneof(mill)
| ~ mustard(lang)
| ~ salt(mill)
| ~ oneof(lang)
| ~ both(barry)
| ~ neither(dix)
| ~ neither(cole) ),
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-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 This is a CNF_UNS_EPR_NEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n011.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Sat Sep 19 19:57:40 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.23/0.48 % SZS status Unsatisfiable for theBenchmark
% 0.23/0.48 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------