%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PUZ030-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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 : Sun Sep 27 08:23:09 AM UTC 2026
% Result : Unsatisfiable 0.14s 0.43s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 31
% Syntax : Number of formulae : 224 ( 11 unt; 0 def)
% Number of atoms : 750 ( 0 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 747 ( 221 ~; 526 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-1 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 24 ( 0 sgn 10 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(both3,axiom,
! [VAR_0] :
( both(VAR_0)
| ~ mustard(VAR_0)
| ~ salt(VAR_0) ),
file('theBenchmark.p',both3) ).
cnf(c_1,plain,
( both(A)
| ~ mustard(A)
| ~ salt(A) ),
inference(clausify,[status(thm)],[both3]) ).
fof(both1,axiom,
! [VAR_0] :
( salt(VAR_0)
| ~ both(VAR_0) ),
file('theBenchmark.p',both1) ).
cnf(c_2,plain,
( salt(A)
| ~ both(A) ),
inference(clausify,[status(thm)],[both1]) ).
fof(oneof1,axiom,
! [VAR_0] :
( mustard(VAR_0)
| salt(VAR_0)
| ~ oneof(VAR_0) ),
file('theBenchmark.p',oneof1) ).
cnf(c_3,plain,
( mustard(A)
| salt(A)
| ~ oneof(A) ),
inference(clausify,[status(thm)],[oneof1]) ).
fof(oneof4,axiom,
! [VAR_0] :
( ~ mustard(VAR_0)
| ~ salt(VAR_0)
| ~ oneof(VAR_0) ),
file('theBenchmark.p',oneof4) ).
cnf(c_4,plain,
( ~ mustard(A)
| ~ salt(A)
| ~ oneof(A) ),
inference(clausify,[status(thm)],[oneof4]) ).
fof(neither2,axiom,
! [VAR_0] :
( ~ salt(VAR_0)
| ~ neither(VAR_0) ),
file('theBenchmark.p',neither2) ).
cnf(c_5,plain,
( ~ salt(A)
| ~ neither(A) ),
inference(clausify,[status(thm)],[neither2]) ).
fof(neither4,axiom,
! [VAR_0] :
( neither(VAR_0)
| mustard(VAR_0)
| salt(VAR_0) ),
file('theBenchmark.p',neither4) ).
cnf(c_6,plain,
( neither(A)
| mustard(A)
| salt(A) ),
inference(clausify,[status(thm)],[neither4]) ).
fof(rule1_1,axiom,
( oneof(lang)
| oneof(cole)
| ~ salt(barry) ),
file('theBenchmark.p',rule1_1) ).
cnf(c_7,plain,
( oneof(lang)
| oneof(cole)
| ~ salt(barry) ),
inference(clausify,[status(thm)],[rule1_1]) ).
fof(rule1_2,axiom,
( salt(barry)
| ~ oneof(cole) ),
file('theBenchmark.p',rule1_2) ).
cnf(c_8,plain,
( salt(barry)
| ~ oneof(cole) ),
inference(clausify,[status(thm)],[rule1_2]) ).
fof(rule1_3,axiom,
( salt(barry)
| ~ oneof(lang) ),
file('theBenchmark.p',rule1_3) ).
cnf(c_9,plain,
( salt(barry)
| ~ oneof(lang) ),
inference(clausify,[status(thm)],[rule1_3]) ).
fof(rule3_1,axiom,
( neither(mill)
| oneof(barry)
| ~ salt(cole) ),
file('theBenchmark.p',rule3_1) ).
cnf(c_10,plain,
( neither(mill)
| oneof(barry)
| ~ salt(cole) ),
inference(clausify,[status(thm)],[rule3_1]) ).
fof(rule3_3,axiom,
( salt(cole)
| ~ neither(mill) ),
file('theBenchmark.p',rule3_3) ).
cnf(c_12,plain,
( salt(cole)
| ~ neither(mill) ),
inference(clausify,[status(thm)],[rule3_3]) ).
fof(rule5_1,axiom,
( both(cole)
| neither(barry)
| ~ salt(dix) ),
file('theBenchmark.p',rule5_1) ).
cnf(c_13,plain,
( both(cole)
| neither(barry)
| ~ salt(dix) ),
inference(clausify,[status(thm)],[rule5_1]) ).
fof(rule7_2,axiom,
( salt(lang)
| ~ oneof(barry) ),
file('theBenchmark.p',rule7_2) ).
cnf(c_17,plain,
( salt(lang)
| ~ oneof(barry) ),
inference(clausify,[status(thm)],[rule7_2]) ).
fof(rule7_3,axiom,
( salt(lang)
| ~ oneof(dix) ),
file('theBenchmark.p',rule7_3) ).
cnf(c_18,plain,
( salt(lang)
| ~ oneof(dix) ),
inference(clausify,[status(thm)],[rule7_3]) ).
fof(rule9_1,axiom,
( both(lang)
| both(barry)
| ~ salt(mill) ),
file('theBenchmark.p',rule9_1) ).
cnf(c_19,plain,
( both(lang)
| both(barry)
| ~ salt(mill) ),
inference(clausify,[status(thm)],[rule9_1]) ).
fof(rule9_2,axiom,
( salt(mill)
| ~ both(barry) ),
file('theBenchmark.p',rule9_2) ).
cnf(c_20,plain,
( salt(mill)
| ~ both(barry) ),
inference(clausify,[status(thm)],[rule9_2]) ).
fof(prove_who_takes_what,axiom,
( ~ oneof(mill)
| ~ mustard(lang)
| ~ salt(mill)
| ~ oneof(lang)
| ~ both(barry)
| ~ neither(dix)
| ~ neither(cole) ),
file('theBenchmark.p',prove_who_takes_what) ).
cnf(c_21,plain,
( ~ oneof(mill)
| ~ mustard(lang)
| ~ salt(mill)
| ~ oneof(lang)
| ~ both(barry)
| ~ neither(dix)
| ~ neither(cole) ),
inference(clausify,[status(thm)],[prove_who_takes_what]) ).
cnf(c_24,plain,
( both(mill)
| ~ mustard(mill)
| ~ both(barry) ),
inference(resolve,[status(thm)],[c_20,c_1]) ).
cnf(c_25,plain,
( ~ both(barry)
| ~ oneof(mill)
| ~ mustard(lang)
| ~ oneof(lang)
| ~ both(barry)
| ~ neither(dix)
| ~ neither(cole) ),
inference(resolve,[status(thm)],[c_21,c_20]) ).
cnf(c_26,plain,
( neither(mill)
| mustard(mill)
| both(lang)
| both(barry) ),
inference(resolve,[status(thm)],[c_19,c_6]) ).
cnf(c_27,plain,
( both(lang)
| ~ mustard(lang)
| ~ oneof(dix) ),
inference(resolve,[status(thm)],[c_18,c_1]) ).
cnf(c_29,plain,
( both(lang)
| ~ mustard(lang)
| ~ oneof(barry) ),
inference(resolve,[status(thm)],[c_17,c_1]) ).
cnf(c_38,plain,
( neither(dix)
| mustard(dix)
| both(cole)
| neither(barry) ),
inference(resolve,[status(thm)],[c_13,c_6]) ).
cnf(c_43,plain,
( mustard(cole)
| ~ oneof(cole)
| neither(mill)
| oneof(barry) ),
inference(resolve,[status(thm)],[c_10,c_3]) ).
cnf(c_44,plain,
( neither(cole)
| mustard(cole)
| neither(mill)
| oneof(barry) ),
inference(resolve,[status(thm)],[c_10,c_6]) ).
cnf(c_45,plain,
( both(barry)
| ~ mustard(barry)
| ~ oneof(lang) ),
inference(resolve,[status(thm)],[c_9,c_1]) ).
cnf(c_52,plain,
( ~ both(A)
| ~ mustard(A)
| ~ oneof(A) ),
inference(resolve,[status(thm)],[c_4,c_2]) ).
fof(rule10_2,axiom,
( mustard(mill)
| ~ oneof(cole) ),
file('theBenchmark.p',rule10_2) ).
cnf(c_54,plain,
( mustard(mill)
| ~ oneof(cole) ),
inference(clausify,[status(thm)],[rule10_2]) ).
fof(rule10_1,axiom,
( oneof(dix)
| oneof(cole)
| ~ mustard(mill) ),
file('theBenchmark.p',rule10_1) ).
cnf(c_55,plain,
( oneof(dix)
| oneof(cole)
| ~ mustard(mill) ),
inference(clausify,[status(thm)],[rule10_1]) ).
fof(rule9_3,axiom,
( mustard(mill)
| ~ both(lang) ),
file('theBenchmark.p',rule9_3) ).
cnf(c_56,plain,
( mustard(mill)
| ~ both(lang) ),
inference(clausify,[status(thm)],[rule9_3]) ).
fof(rule8_3,axiom,
( mustard(lang)
| ~ neither(mill) ),
file('theBenchmark.p',rule8_3) ).
cnf(c_57,plain,
( mustard(lang)
| ~ neither(mill) ),
inference(clausify,[status(thm)],[rule8_3]) ).
fof(rule8_2,axiom,
( mustard(lang)
| ~ neither(cole) ),
file('theBenchmark.p',rule8_2) ).
cnf(c_58,plain,
( mustard(lang)
| ~ neither(cole) ),
inference(clausify,[status(thm)],[rule8_2]) ).
fof(rule8_1,axiom,
( neither(mill)
| neither(cole)
| ~ mustard(lang) ),
file('theBenchmark.p',rule8_1) ).
cnf(c_59,plain,
( neither(mill)
| neither(cole)
| ~ mustard(lang) ),
inference(clausify,[status(thm)],[rule8_1]) ).
fof(rule6_1,axiom,
( neither(mill)
| neither(lang)
| ~ mustard(dix) ),
file('theBenchmark.p',rule6_1) ).
cnf(c_62,plain,
( neither(mill)
| neither(lang)
| ~ mustard(dix) ),
inference(clausify,[status(thm)],[rule6_1]) ).
fof(rule4_3,axiom,
( mustard(cole)
| ~ both(lang) ),
file('theBenchmark.p',rule4_3) ).
cnf(c_63,plain,
( mustard(cole)
| ~ both(lang) ),
inference(clausify,[status(thm)],[rule4_3]) ).
fof(rule4_1,axiom,
( both(lang)
| both(dix)
| ~ mustard(cole) ),
file('theBenchmark.p',rule4_1) ).
cnf(c_65,plain,
( both(lang)
| both(dix)
| ~ mustard(cole) ),
inference(clausify,[status(thm)],[rule4_1]) ).
fof(rule2_2,axiom,
( mustard(barry)
| ~ neither(dix) ),
file('theBenchmark.p',rule2_2) ).
cnf(c_67,plain,
( mustard(barry)
| ~ neither(dix) ),
inference(clausify,[status(thm)],[rule2_2]) ).
fof(neither3,axiom,
! [VAR_0] :
( ~ mustard(VAR_0)
| ~ neither(VAR_0) ),
file('theBenchmark.p',neither3) ).
cnf(c_69,plain,
( ~ mustard(A)
| ~ neither(A) ),
inference(clausify,[status(thm)],[neither3]) ).
fof(both2,axiom,
! [VAR_0] :
( mustard(VAR_0)
| ~ both(VAR_0) ),
file('theBenchmark.p',both2) ).
cnf(c_70,plain,
( mustard(A)
| ~ both(A) ),
inference(clausify,[status(thm)],[both2]) ).
cnf(c_71,plain,
( ~ both(A)
| ~ oneof(A)
| ~ both(A) ),
inference(resolve,[status(thm)],[c_70,c_52]) ).
cnf(c_72,plain,
( ~ oneof(A)
| ~ both(A) ),
inference(copy,[status(thm)],[c_71]) ).
cnf(c_73,plain,
( oneof(dix)
| oneof(cole)
| ~ both(mill) ),
inference(resolve,[status(thm)],[c_70,c_55]) ).
cnf(c_74,plain,
( neither(mill)
| neither(cole)
| ~ both(lang) ),
inference(resolve,[status(thm)],[c_70,c_59]) ).
cnf(c_75,plain,
( neither(mill)
| neither(lang)
| ~ both(dix) ),
inference(resolve,[status(thm)],[c_70,c_62]) ).
cnf(c_76,plain,
( both(lang)
| both(dix)
| ~ both(cole) ),
inference(resolve,[status(thm)],[c_70,c_65]) ).
cnf(c_78,plain,
( ~ neither(A)
| ~ both(A) ),
inference(resolve,[status(thm)],[c_70,c_69]) ).
cnf(c_81,plain,
( ~ both(lang)
| ~ neither(mill) ),
inference(resolve,[status(thm)],[c_69,c_56]) ).
cnf(c_82,plain,
( ~ neither(mill)
| ~ neither(lang) ),
inference(resolve,[status(thm)],[c_69,c_57]) ).
cnf(c_83,plain,
( ~ neither(cole)
| ~ neither(lang) ),
inference(resolve,[status(thm)],[c_69,c_58]) ).
cnf(c_86,plain,
( ~ both(lang)
| ~ neither(cole) ),
inference(resolve,[status(thm)],[c_69,c_63]) ).
cnf(c_92,plain,
( both(barry)
| ~ oneof(lang)
| ~ neither(dix) ),
inference(resolve,[status(thm)],[c_67,c_45]) ).
cnf(c_100,plain,
( ~ oneof(cole)
| neither(mill)
| oneof(barry)
| both(lang)
| both(dix) ),
inference(resolve,[status(thm)],[c_65,c_43]) ).
cnf(c_101,plain,
( neither(cole)
| neither(mill)
| oneof(barry)
| both(lang)
| both(dix) ),
inference(resolve,[status(thm)],[c_65,c_44]) ).
cnf(c_108,plain,
( neither(dix)
| both(cole)
| neither(barry)
| neither(mill)
| neither(lang) ),
inference(resolve,[status(thm)],[c_62,c_38]) ).
cnf(c_117,plain,
( ~ both(barry)
| ~ oneof(mill)
| ~ oneof(lang)
| ~ both(barry)
| ~ neither(dix)
| ~ neither(cole)
| ~ neither(cole) ),
inference(resolve,[status(thm)],[c_58,c_25]) ).
cnf(c_550,plain,
( ~ both(barry)
| ~ oneof(mill)
| ~ oneof(lang)
| ~ both(barry)
| ~ neither(dix)
| ~ neither(cole) ),
inference(copy,[status(thm)],[c_117]) ).
cnf(c_118,plain,
( ~ oneof(mill)
| ~ oneof(lang)
| ~ both(barry)
| ~ neither(dix)
| ~ neither(cole) ),
inference(copy,[status(thm)],[c_550]) ).
cnf(c_119,plain,
( both(lang)
| ~ oneof(dix)
| ~ neither(cole) ),
inference(resolve,[status(thm)],[c_58,c_27]) ).
cnf(c_123,plain,
( both(lang)
| ~ oneof(barry)
| ~ neither(mill) ),
inference(resolve,[status(thm)],[c_57,c_29]) ).
cnf(c_129,plain,
( neither(mill)
| both(lang)
| both(barry)
| oneof(dix)
| oneof(cole) ),
inference(resolve,[status(thm)],[c_55,c_26]) ).
cnf(c_130,plain,
( both(mill)
| ~ both(barry)
| ~ oneof(cole) ),
inference(resolve,[status(thm)],[c_54,c_24]) ).
fof(oneof3,axiom,
! [VAR_0] :
( ~ neither(VAR_0)
| ~ oneof(VAR_0) ),
file('theBenchmark.p',oneof3) ).
cnf(c_135,plain,
( ~ neither(A)
| ~ oneof(A) ),
inference(clausify,[status(thm)],[oneof3]) ).
fof(one_condition_holds1,axiom,
! [VAR_0] :
( oneof(VAR_0)
| neither(VAR_0)
| both(VAR_0) ),
file('theBenchmark.p',one_condition_holds1) ).
cnf(c_136,plain,
( oneof(A)
| neither(A)
| both(A) ),
inference(clausify,[status(thm)],[one_condition_holds1]) ).
cnf(c_137,plain,
( ~ both(barry)
| oneof(lang)
| oneof(cole) ),
inference(resolve,[status(thm)],[c_7,c_2]) ).
cnf(c_138,plain,
( ~ neither(barry)
| ~ oneof(cole) ),
inference(resolve,[status(thm)],[c_8,c_5]) ).
cnf(c_139,plain,
( ~ neither(barry)
| ~ oneof(lang) ),
inference(resolve,[status(thm)],[c_9,c_5]) ).
cnf(c_140,plain,
( ~ both(cole)
| neither(mill)
| oneof(barry) ),
inference(resolve,[status(thm)],[c_10,c_2]) ).
cnf(c_142,plain,
( ~ neither(cole)
| ~ neither(mill) ),
inference(resolve,[status(thm)],[c_12,c_5]) ).
cnf(c_143,plain,
( ~ both(dix)
| both(cole)
| neither(barry) ),
inference(resolve,[status(thm)],[c_13,c_2]) ).
cnf(c_146,plain,
( ~ neither(lang)
| ~ oneof(barry) ),
inference(resolve,[status(thm)],[c_17,c_5]) ).
cnf(c_147,plain,
( ~ neither(lang)
| ~ oneof(dix) ),
inference(resolve,[status(thm)],[c_18,c_5]) ).
cnf(c_149,plain,
( ~ neither(mill)
| ~ both(barry) ),
inference(resolve,[status(thm)],[c_20,c_5]) ).
cnf(c_169,plain,
( neither(dix)
| both(cole)
| neither(barry)
| neither(lang)
| both(lang)
| ~ oneof(barry) ),
inference(resolve,[status(thm)],[c_123,c_108]) ).
cnf(c_551,plain,
( both(lang)
| ~ oneof(barry)
| both(lang)
| both(barry)
| oneof(dix)
| oneof(cole) ),
inference(resolve,[status(thm)],[c_129,c_123]) ).
cnf(c_172,plain,
( ~ oneof(barry)
| both(lang)
| both(barry)
| oneof(dix)
| oneof(cole) ),
inference(copy,[status(thm)],[c_551]) ).
cnf(c_186,plain,
( ~ oneof(mill)
| ~ oneof(lang)
| ~ both(barry)
| ~ neither(dix)
| oneof(cole)
| both(cole) ),
inference(resolve,[status(thm)],[c_136,c_118]) ).
cnf(c_206,plain,
( ~ neither(lang)
| oneof(cole)
| both(cole) ),
inference(resolve,[status(thm)],[c_136,c_83]) ).
cnf(c_209,plain,
( ~ neither(mill)
| oneof(lang)
| both(lang) ),
inference(resolve,[status(thm)],[c_136,c_82]) ).
cnf(c_213,plain,
( oneof(barry)
| both(barry)
| ~ oneof(cole) ),
inference(resolve,[status(thm)],[c_138,c_136]) ).
cnf(c_214,plain,
( oneof(barry)
| both(barry)
| ~ oneof(lang) ),
inference(resolve,[status(thm)],[c_139,c_136]) ).
cnf(c_216,plain,
( oneof(mill)
| both(mill)
| ~ neither(cole) ),
inference(resolve,[status(thm)],[c_142,c_136]) ).
cnf(c_219,plain,
( oneof(cole)
| both(cole)
| ~ neither(mill) ),
inference(resolve,[status(thm)],[c_142,c_136]) ).
cnf(c_222,plain,
( oneof(lang)
| both(lang)
| ~ oneof(barry) ),
inference(resolve,[status(thm)],[c_146,c_136]) ).
cnf(c_223,plain,
( oneof(lang)
| both(lang)
| ~ oneof(dix) ),
inference(resolve,[status(thm)],[c_147,c_136]) ).
cnf(c_227,plain,
( neither(cole)
| oneof(barry)
| both(lang)
| both(dix)
| ~ both(barry) ),
inference(resolve,[status(thm)],[c_149,c_101]) ).
cnf(c_237,plain,
( oneof(lang)
| both(lang)
| oneof(cole)
| both(cole) ),
inference(resolve,[status(thm)],[c_206,c_136]) ).
cnf(c_552,plain,
( both(lang)
| both(barry)
| oneof(dix)
| oneof(cole)
| oneof(lang)
| both(lang) ),
inference(resolve,[status(thm)],[c_209,c_129]) ).
cnf(c_239,plain,
( both(barry)
| oneof(dix)
| oneof(cole)
| oneof(lang)
| both(lang) ),
inference(copy,[status(thm)],[c_552]) ).
cnf(c_241,plain,
( oneof(cole)
| both(cole)
| oneof(mill)
| both(mill) ),
inference(resolve,[status(thm)],[c_216,c_136]) ).
cnf(c_553,plain,
( neither(dix)
| both(cole)
| neither(barry)
| neither(lang)
| oneof(cole)
| both(cole) ),
inference(resolve,[status(thm)],[c_219,c_108]) ).
cnf(c_243,plain,
( neither(dix)
| neither(barry)
| neither(lang)
| oneof(cole)
| both(cole) ),
inference(copy,[status(thm)],[c_553]) ).
cnf(c_253,plain,
( oneof(barry)
| both(barry)
| oneof(lang)
| both(lang)
| both(cole) ),
inference(resolve,[status(thm)],[c_237,c_213]) ).
cnf(c_554,plain,
( oneof(barry)
| both(barry)
| both(barry)
| oneof(dix)
| oneof(lang)
| both(lang) ),
inference(resolve,[status(thm)],[c_239,c_213]) ).
cnf(c_284,plain,
( oneof(barry)
| both(barry)
| oneof(dix)
| oneof(lang)
| both(lang) ),
inference(copy,[status(thm)],[c_554]) ).
cnf(c_555,plain,
( oneof(cole)
| both(cole)
| both(mill)
| ~ oneof(lang)
| ~ both(barry)
| ~ neither(dix)
| oneof(cole)
| both(cole) ),
inference(resolve,[status(thm)],[c_186,c_241]) ).
cnf(c_556,plain,
( oneof(cole)
| both(mill)
| ~ oneof(lang)
| ~ both(barry)
| ~ neither(dix)
| oneof(cole)
| both(cole) ),
inference(copy,[status(thm)],[c_555]) ).
cnf(c_301,plain,
( both(mill)
| ~ oneof(lang)
| ~ both(barry)
| ~ neither(dix)
| oneof(cole)
| both(cole) ),
inference(copy,[status(thm)],[c_556]) ).
cnf(c_557,plain,
( oneof(cole)
| both(cole)
| neither(dix)
| neither(barry)
| oneof(cole)
| both(cole) ),
inference(resolve,[status(thm)],[c_243,c_206]) ).
cnf(c_558,plain,
( oneof(cole)
| neither(dix)
| neither(barry)
| oneof(cole)
| both(cole) ),
inference(copy,[status(thm)],[c_557]) ).
cnf(c_303,plain,
( neither(dix)
| neither(barry)
| oneof(cole)
| both(cole) ),
inference(copy,[status(thm)],[c_558]) ).
cnf(c_559,plain,
( oneof(barry)
| both(barry)
| oneof(barry)
| both(barry)
| both(lang)
| both(cole) ),
inference(resolve,[status(thm)],[c_253,c_214]) ).
cnf(c_560,plain,
( oneof(barry)
| oneof(barry)
| both(barry)
| both(lang)
| both(cole) ),
inference(copy,[status(thm)],[c_559]) ).
cnf(c_307,plain,
( oneof(barry)
| both(barry)
| both(lang)
| both(cole) ),
inference(copy,[status(thm)],[c_560]) ).
cnf(c_561,plain,
( neither(dix)
| both(cole)
| neither(barry)
| neither(lang)
| both(lang)
| both(barry)
| both(lang)
| both(cole) ),
inference(resolve,[status(thm)],[c_307,c_169]) ).
cnf(c_562,plain,
( neither(dix)
| both(cole)
| neither(barry)
| neither(lang)
| both(barry)
| both(lang)
| both(cole) ),
inference(copy,[status(thm)],[c_561]) ).
cnf(c_312,plain,
( neither(dix)
| neither(barry)
| neither(lang)
| both(barry)
| both(lang)
| both(cole) ),
inference(copy,[status(thm)],[c_562]) ).
cnf(c_563,plain,
( oneof(barry)
| both(barry)
| oneof(barry)
| both(barry)
| oneof(dix)
| both(lang) ),
inference(resolve,[status(thm)],[c_284,c_214]) ).
cnf(c_564,plain,
( oneof(barry)
| oneof(barry)
| both(barry)
| oneof(dix)
| both(lang) ),
inference(copy,[status(thm)],[c_563]) ).
cnf(c_326,plain,
( oneof(barry)
| both(barry)
| oneof(dix)
| both(lang) ),
inference(copy,[status(thm)],[c_564]) ).
cnf(c_565,plain,
( oneof(lang)
| both(lang)
| oneof(barry)
| both(barry)
| both(lang) ),
inference(resolve,[status(thm)],[c_326,c_223]) ).
cnf(c_327,plain,
( oneof(lang)
| oneof(barry)
| both(barry)
| both(lang) ),
inference(copy,[status(thm)],[c_565]) ).
cnf(c_566,plain,
( oneof(barry)
| both(barry)
| oneof(barry)
| both(barry)
| both(lang) ),
inference(resolve,[status(thm)],[c_327,c_214]) ).
cnf(c_567,plain,
( oneof(barry)
| oneof(barry)
| both(barry)
| both(lang) ),
inference(copy,[status(thm)],[c_566]) ).
cnf(c_333,plain,
( oneof(barry)
| both(barry)
| both(lang) ),
inference(copy,[status(thm)],[c_567]) ).
cnf(c_568,plain,
( oneof(lang)
| both(lang)
| both(barry)
| both(lang) ),
inference(resolve,[status(thm)],[c_333,c_222]) ).
cnf(c_337,plain,
( oneof(lang)
| both(barry)
| both(lang) ),
inference(copy,[status(thm)],[c_568]) ).
cnf(c_569,plain,
( both(lang)
| both(barry)
| oneof(dix)
| oneof(cole)
| both(barry)
| both(lang) ),
inference(resolve,[status(thm)],[c_333,c_172]) ).
cnf(c_570,plain,
( both(lang)
| oneof(dix)
| oneof(cole)
| both(barry)
| both(lang) ),
inference(copy,[status(thm)],[c_569]) ).
cnf(c_339,plain,
( oneof(dix)
| oneof(cole)
| both(barry)
| both(lang) ),
inference(copy,[status(thm)],[c_570]) ).
cnf(c_340,plain,
( ~ neither(lang)
| both(barry)
| both(lang) ),
inference(resolve,[status(thm)],[c_333,c_146]) ).
cnf(c_342,plain,
( ~ neither(barry)
| both(barry)
| both(lang) ),
inference(resolve,[status(thm)],[c_333,c_135]) ).
cnf(c_571,plain,
( both(barry)
| ~ neither(dix)
| both(barry)
| both(lang) ),
inference(resolve,[status(thm)],[c_337,c_92]) ).
cnf(c_347,plain,
( ~ neither(dix)
| both(barry)
| both(lang) ),
inference(copy,[status(thm)],[c_571]) ).
cnf(c_351,plain,
( ~ both(cole)
| oneof(dix)
| both(barry)
| both(lang) ),
inference(resolve,[status(thm)],[c_339,c_72]) ).
cnf(c_572,plain,
( neither(barry)
| oneof(cole)
| both(cole)
| both(mill)
| ~ oneof(lang)
| ~ both(barry)
| oneof(cole)
| both(cole) ),
inference(resolve,[status(thm)],[c_301,c_303]) ).
cnf(c_573,plain,
( neither(barry)
| oneof(cole)
| both(mill)
| ~ oneof(lang)
| ~ both(barry)
| oneof(cole)
| both(cole) ),
inference(copy,[status(thm)],[c_572]) ).
cnf(c_357,plain,
( neither(barry)
| both(mill)
| ~ oneof(lang)
| ~ both(barry)
| oneof(cole)
| both(cole) ),
inference(copy,[status(thm)],[c_573]) ).
cnf(c_574,plain,
( both(barry)
| both(lang)
| neither(dix)
| neither(barry)
| both(barry)
| both(lang)
| both(cole) ),
inference(resolve,[status(thm)],[c_312,c_340]) ).
cnf(c_575,plain,
( both(barry)
| neither(dix)
| neither(barry)
| both(barry)
| both(lang)
| both(cole) ),
inference(copy,[status(thm)],[c_574]) ).
cnf(c_362,plain,
( neither(dix)
| neither(barry)
| both(barry)
| both(lang)
| both(cole) ),
inference(copy,[status(thm)],[c_575]) ).
cnf(c_576,plain,
( both(barry)
| both(lang)
| neither(barry)
| both(barry)
| both(lang)
| both(cole) ),
inference(resolve,[status(thm)],[c_362,c_347]) ).
cnf(c_577,plain,
( both(barry)
| neither(barry)
| both(barry)
| both(lang)
| both(cole) ),
inference(copy,[status(thm)],[c_576]) ).
cnf(c_363,plain,
( neither(barry)
| both(barry)
| both(lang)
| both(cole) ),
inference(copy,[status(thm)],[c_577]) ).
cnf(c_578,plain,
( both(barry)
| both(lang)
| both(barry)
| both(lang)
| both(cole) ),
inference(resolve,[status(thm)],[c_363,c_342]) ).
cnf(c_579,plain,
( both(barry)
| both(barry)
| both(lang)
| both(cole) ),
inference(copy,[status(thm)],[c_578]) ).
cnf(c_364,plain,
( both(barry)
| both(lang)
| both(cole) ),
inference(copy,[status(thm)],[c_579]) ).
cnf(c_580,plain,
( oneof(dix)
| both(barry)
| both(lang)
| both(barry)
| both(lang) ),
inference(resolve,[status(thm)],[c_364,c_351]) ).
cnf(c_581,plain,
( oneof(dix)
| both(barry)
| both(barry)
| both(lang) ),
inference(copy,[status(thm)],[c_580]) ).
cnf(c_365,plain,
( oneof(dix)
| both(barry)
| both(lang) ),
inference(copy,[status(thm)],[c_581]) ).
cnf(c_582,plain,
( both(lang)
| both(dix)
| both(barry)
| both(lang) ),
inference(resolve,[status(thm)],[c_364,c_76]) ).
cnf(c_366,plain,
( both(dix)
| both(barry)
| both(lang) ),
inference(copy,[status(thm)],[c_582]) ).
cnf(c_368,plain,
( ~ both(dix)
| both(barry)
| both(lang) ),
inference(resolve,[status(thm)],[c_365,c_72]) ).
cnf(c_375,plain,
( ~ neither(cole)
| both(dix)
| both(barry) ),
inference(resolve,[status(thm)],[c_366,c_86]) ).
cnf(c_376,plain,
( ~ neither(mill)
| both(dix)
| both(barry) ),
inference(resolve,[status(thm)],[c_366,c_81]) ).
cnf(c_378,plain,
( neither(mill)
| neither(cole)
| both(dix)
| both(barry) ),
inference(resolve,[status(thm)],[c_366,c_74]) ).
cnf(c_583,plain,
( both(dix)
| both(barry)
| neither(cole)
| both(dix)
| both(barry) ),
inference(resolve,[status(thm)],[c_378,c_376]) ).
cnf(c_584,plain,
( both(dix)
| neither(cole)
| both(dix)
| both(barry) ),
inference(copy,[status(thm)],[c_583]) ).
cnf(c_391,plain,
( neither(cole)
| both(dix)
| both(barry) ),
inference(copy,[status(thm)],[c_584]) ).
cnf(c_585,plain,
( both(dix)
| both(barry)
| both(dix)
| both(barry) ),
inference(resolve,[status(thm)],[c_391,c_375]) ).
cnf(c_586,plain,
( both(dix)
| both(dix)
| both(barry) ),
inference(copy,[status(thm)],[c_585]) ).
cnf(c_392,plain,
( both(dix)
| both(barry) ),
inference(copy,[status(thm)],[c_586]) ).
cnf(c_587,plain,
( both(barry)
| both(lang)
| both(barry) ),
inference(resolve,[status(thm)],[c_392,c_368]) ).
cnf(c_393,plain,
( both(lang)
| both(barry) ),
inference(copy,[status(thm)],[c_587]) ).
cnf(c_404,plain,
( neither(mill)
| neither(lang)
| both(barry) ),
inference(resolve,[status(thm)],[c_392,c_75]) ).
cnf(c_409,plain,
( ~ neither(mill)
| both(barry) ),
inference(resolve,[status(thm)],[c_393,c_81]) ).
cnf(c_410,plain,
( ~ neither(lang)
| both(barry) ),
inference(resolve,[status(thm)],[c_393,c_78]) ).
cnf(c_588,plain,
( both(barry)
| neither(lang)
| both(barry) ),
inference(resolve,[status(thm)],[c_404,c_409]) ).
cnf(c_418,plain,
( neither(lang)
| both(barry) ),
inference(copy,[status(thm)],[c_588]) ).
cnf(c_589,plain,
( both(barry)
| both(barry) ),
inference(resolve,[status(thm)],[c_418,c_410]) ).
cnf(c_419,plain,
both(barry),
inference(copy,[status(thm)],[c_589]) ).
cnf(c_424,plain,
( neither(barry)
| both(mill)
| ~ oneof(lang)
| oneof(cole)
| both(cole) ),
inference(resolve,[status(thm)],[c_419,c_357]) ).
cnf(c_441,plain,
( neither(cole)
| oneof(barry)
| both(lang)
| both(dix) ),
inference(resolve,[status(thm)],[c_419,c_227]) ).
cnf(c_447,plain,
~ neither(mill),
inference(resolve,[status(thm)],[c_419,c_149]) ).
cnf(c_448,plain,
( oneof(lang)
| oneof(cole) ),
inference(resolve,[status(thm)],[c_419,c_137]) ).
cnf(c_452,plain,
( both(mill)
| ~ oneof(cole) ),
inference(resolve,[status(thm)],[c_419,c_130]) ).
cnf(c_457,plain,
( ~ both(cole)
| oneof(barry) ),
inference(resolve,[status(thm)],[c_447,c_140]) ).
cnf(c_460,plain,
( ~ oneof(cole)
| oneof(barry)
| both(lang)
| both(dix) ),
inference(resolve,[status(thm)],[c_447,c_100]) ).
cnf(c_462,plain,
( neither(cole)
| ~ both(lang) ),
inference(resolve,[status(thm)],[c_447,c_74]) ).
cnf(c_463,plain,
~ neither(barry),
inference(resolve,[status(thm)],[c_419,c_78]) ).
cnf(c_464,plain,
~ oneof(barry),
inference(resolve,[status(thm)],[c_419,c_72]) ).
cnf(c_468,plain,
( both(mill)
| ~ oneof(lang)
| oneof(cole)
| both(cole) ),
inference(resolve,[status(thm)],[c_463,c_424]) ).
cnf(c_472,plain,
( ~ both(dix)
| both(cole) ),
inference(resolve,[status(thm)],[c_463,c_143]) ).
cnf(c_473,plain,
( ~ oneof(cole)
| both(lang)
| both(dix) ),
inference(resolve,[status(thm)],[c_464,c_460]) ).
cnf(c_475,plain,
~ both(cole),
inference(resolve,[status(thm)],[c_464,c_457]) ).
cnf(c_477,plain,
( neither(cole)
| both(lang)
| both(dix) ),
inference(resolve,[status(thm)],[c_464,c_441]) ).
cnf(c_489,plain,
~ both(dix),
inference(resolve,[status(thm)],[c_475,c_472]) ).
cnf(c_493,plain,
( both(mill)
| ~ oneof(lang)
| oneof(cole) ),
inference(resolve,[status(thm)],[c_475,c_468]) ).
cnf(c_511,plain,
( neither(cole)
| both(lang) ),
inference(resolve,[status(thm)],[c_489,c_477]) ).
cnf(c_512,plain,
( ~ oneof(cole)
| both(lang) ),
inference(resolve,[status(thm)],[c_489,c_473]) ).
cnf(c_517,plain,
( oneof(lang)
| both(mill) ),
inference(resolve,[status(thm)],[c_452,c_448]) ).
cnf(c_590,plain,
( both(lang)
| ~ oneof(dix)
| both(lang) ),
inference(resolve,[status(thm)],[c_511,c_119]) ).
cnf(c_529,plain,
( ~ oneof(dix)
| both(lang) ),
inference(copy,[status(thm)],[c_590]) ).
cnf(c_591,plain,
( both(mill)
| both(mill)
| oneof(cole) ),
inference(resolve,[status(thm)],[c_493,c_517]) ).
cnf(c_536,plain,
( both(mill)
| oneof(cole) ),
inference(copy,[status(thm)],[c_591]) ).
cnf(c_592,plain,
( both(mill)
| both(mill) ),
inference(resolve,[status(thm)],[c_536,c_452]) ).
cnf(c_538,plain,
both(mill),
inference(copy,[status(thm)],[c_592]) ).
cnf(c_539,plain,
( oneof(dix)
| oneof(cole) ),
inference(resolve,[status(thm)],[c_538,c_73]) ).
cnf(c_541,plain,
( both(lang)
| oneof(dix) ),
inference(resolve,[status(thm)],[c_539,c_512]) ).
cnf(c_593,plain,
( both(lang)
| both(lang) ),
inference(resolve,[status(thm)],[c_541,c_529]) ).
cnf(c_544,plain,
both(lang),
inference(copy,[status(thm)],[c_593]) ).
cnf(c_548,plain,
neither(cole),
inference(resolve,[status(thm)],[c_544,c_462]) ).
cnf(c_594,plain,
~ both(lang),
inference(resolve,[status(thm)],[c_548,c_86]) ).
cnf(c_549,plain,
$false,
inference(resolve,[status(thm)],[c_544,c_594]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ030-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n019.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 05:06:03 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 445487 was started by sandbox2 on n019,
% 0.10/0.37 % Sat Sep 26 05:06:03 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 0.14/0.43
% 0.14/0.43 % SZS status Unsatisfiable for theBenchmark
% 0.14/0.43
% 0.14/0.43 % Proof 1 at 0.03 (+ 0.01) seconds.
% 0.14/0.43 % Length of proof is 148.
% 0.14/0.43 % Level of proof is 30.
% 0.14/0.43 % Maximum clause weight is 17.000.
% 0.14/0.43 % Given clauses 311.
% 0.14/0.43
% 0.14/0.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------