%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PUZ030-2 : 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 : 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 : Sun Sep 27 08:23:09 AM UTC 2026
% Result : Unsatisfiable 0.12s 0.39s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 61
% Number of leaves : 34
% Syntax : Number of formulae : 208 ( 9 unt; 0 def)
% Number of atoms : 747 ( 0 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 747 ( 208 ~; 539 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of predicates : 11 ( 10 usr; 11 prp; 0-0 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(c4,axiom,
( salt_lang
| salt_barry
| ~ salt_mill ),
file('theBenchmark.p',c4) ).
cnf(c_4,plain,
( salt_lang
| salt_barry
| ~ salt_mill ),
inference(clausify,[status(thm)],[c4]) ).
fof(c5,axiom,
( ~ mustard_mill
| ~ mustard_cole
| ~ mustard_lang ),
file('theBenchmark.p',c5) ).
cnf(c_5,plain,
( ~ mustard_mill
| ~ mustard_cole
| ~ mustard_lang ),
inference(clausify,[status(thm)],[c5]) ).
fof(c6,axiom,
( ~ salt_mill
| ~ mustard_cole
| ~ mustard_lang ),
file('theBenchmark.p',c6) ).
cnf(c_6,plain,
( ~ salt_mill
| ~ mustard_cole
| ~ mustard_lang ),
inference(clausify,[status(thm)],[c6]) ).
fof(c7,axiom,
( ~ mustard_mill
| ~ salt_cole
| ~ mustard_lang ),
file('theBenchmark.p',c7) ).
cnf(c_7,plain,
( ~ mustard_mill
| ~ salt_cole
| ~ mustard_lang ),
inference(clausify,[status(thm)],[c7]) ).
fof(c10,axiom,
( ~ salt_mill
| ~ mustard_lang
| ~ mustard_dix ),
file('theBenchmark.p',c10) ).
cnf(c_10,plain,
( ~ salt_mill
| ~ mustard_lang
| ~ mustard_dix ),
inference(clausify,[status(thm)],[c10]) ).
fof(c11,axiom,
( ~ mustard_mill
| ~ salt_lang
| ~ mustard_dix ),
file('theBenchmark.p',c11) ).
cnf(c_11,plain,
( ~ mustard_mill
| ~ salt_lang
| ~ mustard_dix ),
inference(clausify,[status(thm)],[c11]) ).
fof(c12,axiom,
( ~ salt_mill
| ~ salt_lang
| ~ mustard_dix ),
file('theBenchmark.p',c12) ).
cnf(c_12,plain,
( ~ salt_mill
| ~ salt_lang
| ~ mustard_dix ),
inference(clausify,[status(thm)],[c12]) ).
fof(c15,axiom,
( mustard_cole
| ~ salt_barry
| ~ salt_dix ),
file('theBenchmark.p',c15) ).
cnf(c_15,plain,
( mustard_cole
| ~ salt_barry
| ~ salt_dix ),
inference(clausify,[status(thm)],[c15]) ).
fof(c16,axiom,
( salt_cole
| ~ salt_barry
| ~ salt_dix ),
file('theBenchmark.p',c16) ).
cnf(c_16,plain,
( salt_cole
| ~ salt_barry
| ~ salt_dix ),
inference(clausify,[status(thm)],[c16]) ).
fof(c17,axiom,
( mustard_lang
| mustard_dix
| ~ mustard_cole ),
file('theBenchmark.p',c17) ).
cnf(c_17,plain,
( mustard_lang
| mustard_dix
| ~ mustard_cole ),
inference(clausify,[status(thm)],[c17]) ).
fof(c19,axiom,
( mustard_lang
| salt_dix
| ~ mustard_cole ),
file('theBenchmark.p',c19) ).
cnf(c_19,plain,
( mustard_lang
| salt_dix
| ~ mustard_cole ),
inference(clausify,[status(thm)],[c19]) ).
fof(c25,axiom,
( mustard_mill
| ~ mustard_dix
| salt_dix ),
file('theBenchmark.p',c25) ).
cnf(c_25,plain,
( mustard_mill
| ~ mustard_dix
| salt_dix ),
inference(clausify,[status(thm)],[c25]) ).
fof(c26,axiom,
( mustard_mill
| mustard_dix
| ~ salt_dix ),
file('theBenchmark.p',c26) ).
cnf(c_26,plain,
( mustard_mill
| mustard_dix
| ~ salt_dix ),
inference(clausify,[status(thm)],[c26]) ).
fof(c29,axiom,
( salt_mill
| ~ mustard_lang
| ~ salt_lang ),
file('theBenchmark.p',c29) ).
cnf(c_29,plain,
( salt_mill
| ~ mustard_lang
| ~ salt_lang ),
inference(clausify,[status(thm)],[c29]) ).
fof(c30,axiom,
( salt_mill
| ~ mustard_barry
| ~ salt_barry ),
file('theBenchmark.p',c30) ).
cnf(c_30,plain,
( salt_mill
| ~ mustard_barry
| ~ salt_barry ),
inference(clausify,[status(thm)],[c30]) ).
fof(c31,axiom,
( salt_lang
| ~ mustard_dix
| salt_dix ),
file('theBenchmark.p',c31) ).
cnf(c_31,plain,
( salt_lang
| ~ mustard_dix
| salt_dix ),
inference(clausify,[status(thm)],[c31]) ).
fof(c34,axiom,
( salt_lang
| mustard_barry
| ~ salt_barry ),
file('theBenchmark.p',c34) ).
cnf(c_34,plain,
( salt_lang
| mustard_barry
| ~ salt_barry ),
inference(clausify,[status(thm)],[c34]) ).
fof(c35,axiom,
( salt_dix
| ~ mustard_cole
| ~ salt_cole ),
file('theBenchmark.p',c35) ).
cnf(c_35,plain,
( salt_dix
| ~ mustard_cole
| ~ salt_cole ),
inference(clausify,[status(thm)],[c35]) ).
fof(c36,axiom,
( mustard_cole
| ~ mustard_lang
| ~ salt_lang ),
file('theBenchmark.p',c36) ).
cnf(c_36,plain,
( mustard_cole
| ~ mustard_lang
| ~ salt_lang ),
inference(clausify,[status(thm)],[c36]) ).
fof(c41,axiom,
( salt_barry
| ~ mustard_lang
| salt_lang ),
file('theBenchmark.p',c41) ).
cnf(c_41,plain,
( salt_barry
| ~ mustard_lang
| salt_lang ),
inference(clausify,[status(thm)],[c41]) ).
fof(c42,axiom,
( salt_barry
| mustard_lang
| ~ salt_lang ),
file('theBenchmark.p',c42) ).
cnf(c_42,plain,
( salt_barry
| mustard_lang
| ~ salt_lang ),
inference(clausify,[status(thm)],[c42]) ).
fof(c43,axiom,
( salt_barry
| ~ mustard_cole
| salt_cole ),
file('theBenchmark.p',c43) ).
cnf(c_43,plain,
( salt_barry
| ~ mustard_cole
| salt_cole ),
inference(clausify,[status(thm)],[c43]) ).
fof(c44,axiom,
( salt_barry
| mustard_cole
| ~ salt_cole ),
file('theBenchmark.p',c44) ).
cnf(c_44,plain,
( salt_barry
| mustard_cole
| ~ salt_cole ),
inference(clausify,[status(thm)],[c44]) ).
fof(c46,axiom,
( ~ salt_mill
| ~ salt_barry
| ~ mustard_barry
| ~ salt_cole ),
file('theBenchmark.p',c46) ).
cnf(c_46,plain,
( ~ salt_mill
| ~ salt_barry
| ~ mustard_barry
| ~ salt_cole ),
inference(clausify,[status(thm)],[c46]) ).
fof(c47,axiom,
( ~ mustard_mill
| mustard_barry
| salt_barry
| ~ salt_cole ),
file('theBenchmark.p',c47) ).
cnf(c_47,plain,
( ~ mustard_mill
| mustard_barry
| salt_barry
| ~ salt_cole ),
inference(clausify,[status(thm)],[c47]) ).
fof(c48,axiom,
( ~ salt_mill
| mustard_barry
| salt_barry
| ~ salt_cole ),
file('theBenchmark.p',c48) ).
cnf(c_48,plain,
( ~ salt_mill
| mustard_barry
| salt_barry
| ~ salt_cole ),
inference(clausify,[status(thm)],[c48]) ).
fof(c49,axiom,
( ~ salt_dix
| ~ mustard_dix
| ~ salt_cole
| ~ mustard_cole
| ~ mustard_mill ),
file('theBenchmark.p',c49) ).
cnf(c_49,plain,
( ~ salt_dix
| ~ mustard_dix
| ~ salt_cole
| ~ mustard_cole
| ~ mustard_mill ),
inference(clausify,[status(thm)],[c49]) ).
fof(c50,axiom,
( mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_mill ),
file('theBenchmark.p',c50) ).
cnf(c_50,plain,
( mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_mill ),
inference(clausify,[status(thm)],[c50]) ).
fof(c56,axiom,
( mustard_lang
| mustard_mill
| salt_mill ),
file('theBenchmark.p',c56) ).
cnf(c_56,plain,
( mustard_lang
| mustard_mill
| salt_mill ),
inference(clausify,[status(thm)],[c56]) ).
fof(c57,axiom,
( mustard_lang
| mustard_cole
| salt_cole ),
file('theBenchmark.p',c57) ).
cnf(c_57,plain,
( mustard_lang
| mustard_cole
| salt_cole ),
inference(clausify,[status(thm)],[c57]) ).
fof(c58,axiom,
( mustard_dix
| mustard_mill
| salt_mill ),
file('theBenchmark.p',c58) ).
cnf(c_58,plain,
( mustard_dix
| mustard_mill
| salt_mill ),
inference(clausify,[status(thm)],[c58]) ).
fof(c59,axiom,
( mustard_dix
| mustard_lang
| salt_lang ),
file('theBenchmark.p',c59) ).
cnf(c_59,plain,
( mustard_dix
| mustard_lang
| salt_lang ),
inference(clausify,[status(thm)],[c59]) ).
fof(c62,axiom,
( mustard_barry
| mustard_dix
| salt_dix ),
file('theBenchmark.p',c62) ).
cnf(c_62,plain,
( mustard_barry
| mustard_dix
| salt_dix ),
inference(clausify,[status(thm)],[c62]) ).
fof(prove_who_takes_what,axiom,
( 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(c_63,plain,
( mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_lang
| ~ salt_mill
| ~ salt_barry
| ~ mustard_barry
| salt_lang ),
inference(clausify,[status(thm)],[prove_who_takes_what]) ).
cnf(c_64,plain,
( ~ salt_dix
| ~ mustard_dix
| ~ salt_cole
| ~ mustard_cole
| mustard_lang
| salt_mill ),
inference(resolve,[status(thm)],[c_56,c_49]) ).
cnf(c_65,plain,
( mustard_barry
| salt_barry
| ~ salt_cole
| mustard_lang
| salt_mill ),
inference(resolve,[status(thm)],[c_56,c_47]) ).
cnf(c_66,plain,
( ~ salt_lang
| ~ mustard_dix
| mustard_lang
| salt_mill ),
inference(resolve,[status(thm)],[c_56,c_11]) ).
cnf(c_67,plain,
( salt_barry
| salt_lang
| mustard_cole
| salt_cole ),
inference(resolve,[status(thm)],[c_57,c_41]) ).
cnf(c_235,plain,
( mustard_cole
| ~ salt_lang
| mustard_cole
| salt_cole ),
inference(resolve,[status(thm)],[c_57,c_36]) ).
cnf(c_68,plain,
( ~ salt_lang
| mustard_cole
| salt_cole ),
inference(copy,[status(thm)],[c_235]) ).
cnf(c_236,plain,
( mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| mustard_dix
| salt_mill ),
inference(resolve,[status(thm)],[c_58,c_50]) ).
cnf(c_70,plain,
( salt_dix
| mustard_cole
| salt_cole
| mustard_dix
| salt_mill ),
inference(copy,[status(thm)],[c_236]) ).
cnf(c_237,plain,
( salt_lang
| salt_dix
| mustard_barry
| salt_dix ),
inference(resolve,[status(thm)],[c_62,c_31]) ).
cnf(c_80,plain,
( salt_lang
| mustard_barry
| salt_dix ),
inference(copy,[status(thm)],[c_237]) ).
cnf(c_238,plain,
( mustard_mill
| salt_dix
| mustard_barry
| salt_dix ),
inference(resolve,[status(thm)],[c_62,c_25]) ).
cnf(c_81,plain,
( mustard_mill
| mustard_barry
| salt_dix ),
inference(copy,[status(thm)],[c_238]) ).
cnf(c_239,plain,
( mustard_dix
| salt_lang
| mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ salt_mill
| ~ salt_barry
| ~ mustard_barry
| salt_lang ),
inference(resolve,[status(thm)],[c_63,c_59]) ).
cnf(c_240,plain,
( mustard_dix
| mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ salt_mill
| ~ salt_barry
| ~ mustard_barry
| salt_lang ),
inference(copy,[status(thm)],[c_239]) ).
cnf(c_82,plain,
( mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ salt_mill
| ~ salt_barry
| ~ mustard_barry
| salt_lang ),
inference(copy,[status(thm)],[c_240]) ).
cnf(c_87,plain,
( ~ salt_lang
| ~ mustard_dix
| mustard_barry
| salt_dix ),
inference(resolve,[status(thm)],[c_81,c_11]) ).
cnf(c_241,plain,
( salt_barry
| mustard_cole
| salt_barry
| salt_lang
| mustard_cole ),
inference(resolve,[status(thm)],[c_67,c_44]) ).
cnf(c_242,plain,
( salt_barry
| salt_barry
| salt_lang
| mustard_cole ),
inference(copy,[status(thm)],[c_241]) ).
cnf(c_100,plain,
( salt_barry
| salt_lang
| mustard_cole ),
inference(copy,[status(thm)],[c_242]) ).
cnf(c_243,plain,
( mustard_cole
| salt_cole
| salt_barry
| mustard_cole ),
inference(resolve,[status(thm)],[c_100,c_68]) ).
cnf(c_101,plain,
( salt_cole
| salt_barry
| mustard_cole ),
inference(copy,[status(thm)],[c_243]) ).
cnf(c_244,plain,
( salt_barry
| mustard_cole
| salt_barry
| mustard_cole ),
inference(resolve,[status(thm)],[c_101,c_44]) ).
cnf(c_245,plain,
( salt_barry
| salt_barry
| mustard_cole ),
inference(copy,[status(thm)],[c_244]) ).
cnf(c_103,plain,
( salt_barry
| mustard_cole ),
inference(copy,[status(thm)],[c_245]) ).
cnf(c_246,plain,
( salt_barry
| salt_cole
| salt_barry ),
inference(resolve,[status(thm)],[c_103,c_43]) ).
cnf(c_104,plain,
( salt_cole
| salt_barry ),
inference(copy,[status(thm)],[c_246]) ).
cnf(c_105,plain,
( mustard_lang
| mustard_dix
| salt_barry ),
inference(resolve,[status(thm)],[c_103,c_17]) ).
cnf(c_247,plain,
( mustard_barry
| salt_barry
| mustard_lang
| salt_mill
| salt_barry ),
inference(resolve,[status(thm)],[c_104,c_65]) ).
cnf(c_106,plain,
( mustard_barry
| mustard_lang
| salt_mill
| salt_barry ),
inference(copy,[status(thm)],[c_247]) ).
cnf(c_107,plain,
( ~ salt_dix
| ~ mustard_dix
| ~ mustard_cole
| mustard_lang
| salt_mill
| salt_barry ),
inference(resolve,[status(thm)],[c_104,c_64]) ).
cnf(c_108,plain,
( salt_dix
| ~ mustard_cole
| salt_barry ),
inference(resolve,[status(thm)],[c_104,c_35]) ).
cnf(c_248,plain,
( salt_barry
| salt_dix
| salt_barry ),
inference(resolve,[status(thm)],[c_108,c_103]) ).
cnf(c_112,plain,
( salt_dix
| salt_barry ),
inference(copy,[status(thm)],[c_248]) ).
cnf(c_113,plain,
( mustard_mill
| mustard_dix
| salt_barry ),
inference(resolve,[status(thm)],[c_112,c_26]) ).
cnf(c_118,plain,
( ~ salt_cole
| ~ mustard_lang
| mustard_dix
| salt_barry ),
inference(resolve,[status(thm)],[c_113,c_7]) ).
cnf(c_249,plain,
( salt_dix
| mustard_cole
| salt_cole
| mustard_dix
| mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ salt_barry
| ~ mustard_barry
| salt_lang ),
inference(resolve,[status(thm)],[c_82,c_70]) ).
cnf(c_250,plain,
( salt_dix
| mustard_cole
| salt_cole
| mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ salt_barry
| ~ mustard_barry
| salt_lang ),
inference(copy,[status(thm)],[c_249]) ).
cnf(c_251,plain,
( salt_dix
| mustard_cole
| mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ salt_barry
| ~ mustard_barry
| salt_lang ),
inference(copy,[status(thm)],[c_250]) ).
cnf(c_252,plain,
( salt_dix
| mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ salt_barry
| ~ mustard_barry
| salt_lang ),
inference(copy,[status(thm)],[c_251]) ).
cnf(c_125,plain,
( mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ salt_barry
| ~ mustard_barry
| salt_lang ),
inference(copy,[status(thm)],[c_252]) ).
cnf(c_253,plain,
( mustard_barry
| salt_dix
| ~ salt_lang
| mustard_barry
| salt_dix ),
inference(resolve,[status(thm)],[c_87,c_62]) ).
cnf(c_254,plain,
( mustard_barry
| ~ salt_lang
| mustard_barry
| salt_dix ),
inference(copy,[status(thm)],[c_253]) ).
cnf(c_126,plain,
( ~ salt_lang
| mustard_barry
| salt_dix ),
inference(copy,[status(thm)],[c_254]) ).
cnf(c_255,plain,
( mustard_barry
| salt_dix
| mustard_barry
| salt_dix ),
inference(resolve,[status(thm)],[c_126,c_80]) ).
cnf(c_256,plain,
( mustard_barry
| mustard_barry
| salt_dix ),
inference(copy,[status(thm)],[c_255]) ).
cnf(c_127,plain,
( mustard_barry
| salt_dix ),
inference(copy,[status(thm)],[c_256]) ).
cnf(c_129,plain,
( mustard_mill
| mustard_dix
| mustard_barry ),
inference(resolve,[status(thm)],[c_127,c_26]) ).
cnf(c_130,plain,
( mustard_cole
| ~ salt_barry
| mustard_barry ),
inference(resolve,[status(thm)],[c_127,c_15]) ).
cnf(c_257,plain,
( salt_barry
| salt_lang
| mustard_barry
| salt_mill
| salt_barry ),
inference(resolve,[status(thm)],[c_106,c_41]) ).
cnf(c_132,plain,
( salt_lang
| mustard_barry
| salt_mill
| salt_barry ),
inference(copy,[status(thm)],[c_257]) ).
cnf(c_258,plain,
( salt_mill
| ~ salt_lang
| mustard_barry
| salt_mill
| salt_barry ),
inference(resolve,[status(thm)],[c_106,c_29]) ).
cnf(c_133,plain,
( ~ salt_lang
| mustard_barry
| salt_mill
| salt_barry ),
inference(copy,[status(thm)],[c_258]) ).
cnf(c_136,plain,
( ~ mustard_cole
| ~ mustard_lang
| mustard_dix
| mustard_barry ),
inference(resolve,[status(thm)],[c_129,c_5]) ).
cnf(c_259,plain,
( mustard_dix
| salt_barry
| ~ salt_cole
| mustard_dix
| salt_barry ),
inference(resolve,[status(thm)],[c_118,c_105]) ).
cnf(c_260,plain,
( mustard_dix
| ~ salt_cole
| mustard_dix
| salt_barry ),
inference(copy,[status(thm)],[c_259]) ).
cnf(c_140,plain,
( ~ salt_cole
| mustard_dix
| salt_barry ),
inference(copy,[status(thm)],[c_260]) ).
cnf(c_261,plain,
( salt_barry
| mustard_dix
| salt_barry ),
inference(resolve,[status(thm)],[c_140,c_104]) ).
cnf(c_141,plain,
( mustard_dix
| salt_barry ),
inference(copy,[status(thm)],[c_261]) ).
cnf(c_262,plain,
( ~ salt_dix
| ~ mustard_cole
| mustard_lang
| salt_mill
| salt_barry
| salt_barry ),
inference(resolve,[status(thm)],[c_141,c_107]) ).
cnf(c_142,plain,
( ~ salt_dix
| ~ mustard_cole
| mustard_lang
| salt_mill
| salt_barry ),
inference(copy,[status(thm)],[c_262]) ).
cnf(c_263,plain,
( salt_lang
| salt_barry
| salt_lang
| mustard_barry
| salt_barry ),
inference(resolve,[status(thm)],[c_132,c_4]) ).
cnf(c_264,plain,
( salt_lang
| salt_lang
| mustard_barry
| salt_barry ),
inference(copy,[status(thm)],[c_263]) ).
cnf(c_152,plain,
( salt_lang
| mustard_barry
| salt_barry ),
inference(copy,[status(thm)],[c_264]) ).
cnf(c_265,plain,
( mustard_barry
| salt_barry
| mustard_barry
| salt_mill
| salt_barry ),
inference(resolve,[status(thm)],[c_133,c_152]) ).
cnf(c_266,plain,
( mustard_barry
| mustard_barry
| salt_mill
| salt_barry ),
inference(copy,[status(thm)],[c_265]) ).
cnf(c_156,plain,
( mustard_barry
| salt_mill
| salt_barry ),
inference(copy,[status(thm)],[c_266]) ).
cnf(c_267,plain,
( mustard_barry
| salt_barry
| ~ salt_cole
| mustard_barry
| salt_barry ),
inference(resolve,[status(thm)],[c_156,c_48]) ).
cnf(c_268,plain,
( mustard_barry
| ~ salt_cole
| mustard_barry
| salt_barry ),
inference(copy,[status(thm)],[c_267]) ).
cnf(c_157,plain,
( ~ salt_cole
| mustard_barry
| salt_barry ),
inference(copy,[status(thm)],[c_268]) ).
cnf(c_269,plain,
( salt_barry
| mustard_barry
| salt_barry ),
inference(resolve,[status(thm)],[c_157,c_104]) ).
cnf(c_159,plain,
( mustard_barry
| salt_barry ),
inference(copy,[status(thm)],[c_269]) ).
cnf(c_270,plain,
( mustard_cole
| mustard_barry
| mustard_barry ),
inference(resolve,[status(thm)],[c_159,c_130]) ).
cnf(c_160,plain,
( mustard_cole
| mustard_barry ),
inference(copy,[status(thm)],[c_270]) ).
cnf(c_271,plain,
( salt_lang
| mustard_barry
| mustard_barry ),
inference(resolve,[status(thm)],[c_159,c_34]) ).
cnf(c_162,plain,
( salt_lang
| mustard_barry ),
inference(copy,[status(thm)],[c_271]) ).
cnf(c_163,plain,
( mustard_lang
| mustard_dix
| mustard_barry ),
inference(resolve,[status(thm)],[c_160,c_17]) ).
cnf(c_272,plain,
( ~ mustard_cole
| mustard_dix
| mustard_barry
| mustard_dix
| mustard_barry ),
inference(resolve,[status(thm)],[c_163,c_136]) ).
cnf(c_273,plain,
( ~ mustard_cole
| mustard_dix
| mustard_dix
| mustard_barry ),
inference(copy,[status(thm)],[c_272]) ).
cnf(c_165,plain,
( ~ mustard_cole
| mustard_dix
| mustard_barry ),
inference(copy,[status(thm)],[c_273]) ).
cnf(c_274,plain,
( mustard_barry
| mustard_dix
| mustard_barry ),
inference(resolve,[status(thm)],[c_165,c_160]) ).
cnf(c_168,plain,
( mustard_dix
| mustard_barry ),
inference(copy,[status(thm)],[c_274]) ).
cnf(c_275,plain,
( salt_barry
| ~ salt_dix
| mustard_lang
| salt_mill
| salt_barry ),
inference(resolve,[status(thm)],[c_142,c_103]) ).
cnf(c_169,plain,
( ~ salt_dix
| mustard_lang
| salt_mill
| salt_barry ),
inference(copy,[status(thm)],[c_275]) ).
cnf(c_170,plain,
( ~ salt_lang
| mustard_lang
| salt_mill
| mustard_barry ),
inference(resolve,[status(thm)],[c_168,c_66]) ).
cnf(c_276,plain,
( salt_barry
| mustard_lang
| salt_mill
| salt_barry ),
inference(resolve,[status(thm)],[c_169,c_112]) ).
cnf(c_171,plain,
( mustard_lang
| salt_mill
| salt_barry ),
inference(copy,[status(thm)],[c_276]) ).
cnf(c_277,plain,
( salt_barry
| salt_lang
| salt_mill
| salt_barry ),
inference(resolve,[status(thm)],[c_171,c_41]) ).
cnf(c_172,plain,
( salt_lang
| salt_mill
| salt_barry ),
inference(copy,[status(thm)],[c_277]) ).
cnf(c_278,plain,
( salt_mill
| ~ salt_lang
| salt_mill
| salt_barry ),
inference(resolve,[status(thm)],[c_171,c_29]) ).
cnf(c_173,plain,
( ~ salt_lang
| salt_mill
| salt_barry ),
inference(copy,[status(thm)],[c_278]) ).
cnf(c_279,plain,
( salt_lang
| salt_barry
| salt_lang
| salt_barry ),
inference(resolve,[status(thm)],[c_172,c_4]) ).
cnf(c_280,plain,
( salt_lang
| salt_lang
| salt_barry ),
inference(copy,[status(thm)],[c_279]) ).
cnf(c_174,plain,
( salt_lang
| salt_barry ),
inference(copy,[status(thm)],[c_280]) ).
cnf(c_281,plain,
( salt_barry
| mustard_lang
| salt_barry ),
inference(resolve,[status(thm)],[c_174,c_42]) ).
cnf(c_176,plain,
( mustard_lang
| salt_barry ),
inference(copy,[status(thm)],[c_281]) ).
cnf(c_177,plain,
( ~ salt_mill
| ~ mustard_dix
| salt_barry ),
inference(resolve,[status(thm)],[c_176,c_10]) ).
cnf(c_282,plain,
( salt_barry
| salt_mill
| salt_barry ),
inference(resolve,[status(thm)],[c_173,c_174]) ).
cnf(c_180,plain,
( salt_mill
| salt_barry ),
inference(copy,[status(thm)],[c_282]) ).
cnf(c_283,plain,
( mustard_barry
| mustard_lang
| salt_mill
| mustard_barry ),
inference(resolve,[status(thm)],[c_170,c_162]) ).
cnf(c_182,plain,
( mustard_lang
| salt_mill
| mustard_barry ),
inference(copy,[status(thm)],[c_283]) ).
cnf(c_284,plain,
( salt_barry
| ~ mustard_dix
| salt_barry ),
inference(resolve,[status(thm)],[c_177,c_180]) ).
cnf(c_183,plain,
( ~ mustard_dix
| salt_barry ),
inference(copy,[status(thm)],[c_284]) ).
cnf(c_285,plain,
( salt_barry
| salt_barry ),
inference(resolve,[status(thm)],[c_183,c_141]) ).
cnf(c_184,plain,
salt_barry,
inference(copy,[status(thm)],[c_285]) ).
cnf(c_185,plain,
( mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_barry
| salt_lang ),
inference(resolve,[status(thm)],[c_184,c_125]) ).
cnf(c_190,plain,
( ~ salt_mill
| ~ mustard_barry
| ~ salt_cole ),
inference(resolve,[status(thm)],[c_184,c_46]) ).
cnf(c_192,plain,
( salt_mill
| ~ mustard_barry ),
inference(resolve,[status(thm)],[c_184,c_30]) ).
cnf(c_193,plain,
( salt_cole
| ~ salt_dix ),
inference(resolve,[status(thm)],[c_184,c_16]) ).
cnf(c_286,plain,
( salt_mill
| ~ salt_lang
| salt_mill
| mustard_barry ),
inference(resolve,[status(thm)],[c_182,c_29]) ).
cnf(c_195,plain,
( ~ salt_lang
| salt_mill
| mustard_barry ),
inference(copy,[status(thm)],[c_286]) ).
cnf(c_287,plain,
( mustard_barry
| salt_mill
| mustard_barry ),
inference(resolve,[status(thm)],[c_195,c_162]) ).
cnf(c_196,plain,
( salt_mill
| mustard_barry ),
inference(copy,[status(thm)],[c_287]) ).
cnf(c_197,plain,
( ~ salt_lang
| ~ mustard_dix
| mustard_barry ),
inference(resolve,[status(thm)],[c_196,c_12]) ).
cnf(c_288,plain,
( mustard_barry
| ~ salt_lang
| mustard_barry ),
inference(resolve,[status(thm)],[c_197,c_168]) ).
cnf(c_203,plain,
( ~ salt_lang
| mustard_barry ),
inference(copy,[status(thm)],[c_288]) ).
cnf(c_289,plain,
( mustard_barry
| mustard_barry ),
inference(resolve,[status(thm)],[c_203,c_162]) ).
cnf(c_204,plain,
mustard_barry,
inference(copy,[status(thm)],[c_289]) ).
cnf(c_205,plain,
salt_mill,
inference(resolve,[status(thm)],[c_204,c_192]) ).
cnf(c_290,plain,
( ~ salt_mill
| ~ salt_cole ),
inference(resolve,[status(thm)],[c_204,c_190]) ).
cnf(c_207,plain,
~ salt_cole,
inference(resolve,[status(thm)],[c_205,c_290]) ).
cnf(c_291,plain,
( mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| salt_lang ),
inference(resolve,[status(thm)],[c_204,c_185]) ).
cnf(c_210,plain,
( mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_lang ),
inference(resolve,[status(thm)],[c_207,c_291]) ).
cnf(c_216,plain,
( ~ mustard_cole
| ~ mustard_lang ),
inference(resolve,[status(thm)],[c_205,c_6]) ).
cnf(c_217,plain,
~ salt_dix,
inference(resolve,[status(thm)],[c_207,c_193]) ).
cnf(c_218,plain,
( ~ salt_lang
| mustard_cole ),
inference(resolve,[status(thm)],[c_207,c_68]) ).
cnf(c_292,plain,
( mustard_dix
| salt_dix
| mustard_cole
| ~ mustard_mill ),
inference(resolve,[status(thm)],[c_207,c_50]) ).
cnf(c_220,plain,
( mustard_dix
| mustard_cole
| ~ mustard_mill ),
inference(resolve,[status(thm)],[c_217,c_292]) ).
cnf(c_222,plain,
( mustard_mill
| mustard_dix
| mustard_cole
| salt_lang ),
inference(resolve,[status(thm)],[c_217,c_210]) ).
cnf(c_224,plain,
( salt_lang
| ~ mustard_dix ),
inference(resolve,[status(thm)],[c_217,c_31]) ).
cnf(c_226,plain,
( mustard_lang
| ~ mustard_cole ),
inference(resolve,[status(thm)],[c_217,c_19]) ).
cnf(c_293,plain,
( mustard_dix
| mustard_cole
| mustard_dix
| mustard_cole
| salt_lang ),
inference(resolve,[status(thm)],[c_222,c_220]) ).
cnf(c_294,plain,
( mustard_dix
| mustard_dix
| mustard_cole
| salt_lang ),
inference(copy,[status(thm)],[c_293]) ).
cnf(c_227,plain,
( mustard_dix
| mustard_cole
| salt_lang ),
inference(copy,[status(thm)],[c_294]) ).
cnf(c_295,plain,
( salt_lang
| mustard_cole
| salt_lang ),
inference(resolve,[status(thm)],[c_227,c_224]) ).
cnf(c_228,plain,
( mustard_cole
| salt_lang ),
inference(copy,[status(thm)],[c_295]) ).
cnf(c_296,plain,
( mustard_cole
| mustard_cole ),
inference(resolve,[status(thm)],[c_228,c_218]) ).
cnf(c_230,plain,
mustard_cole,
inference(copy,[status(thm)],[c_296]) ).
cnf(c_231,plain,
mustard_lang,
inference(resolve,[status(thm)],[c_230,c_226]) ).
cnf(c_297,plain,
~ mustard_cole,
inference(resolve,[status(thm)],[c_231,c_216]) ).
cnf(c_234,plain,
$false,
inference(resolve,[status(thm)],[c_230,c_297]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ030-2 : 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.35 % Computer : n018.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sat Sep 26 05:08:21 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 3781135 was started by sandbox2 on n018,
% 0.10/0.36 % Sat Sep 26 05:08:21 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.36
% 0.12/0.36 % From the command line: assign(max_seconds, 300).
% 0.12/0.39
% 0.12/0.39 % SZS status Unsatisfiable for theBenchmark
% 0.12/0.39
% 0.12/0.39 % Proof 1 at 0.01 (+ 0.00) seconds.
% 0.12/0.39 % Length of proof is 111.
% 0.12/0.39 % Level of proof is 31.
% 0.12/0.39 % Maximum clause weight is 10.000.
% 0.12/0.39 % Given clauses 181.
% 0.12/0.39
% 0.12/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------