%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PUZ030-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n017.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 : Fri Sep 25 02:31:54 PM UTC 2026
% Result : Unsatisfiable 4.59s 6.18s
% Output : Proof 4.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 108
% Number of leaves : 36
% Syntax : Number of formulae : 302 ( 13 unt; 0 def)
% Number of atoms : 916 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 857 ( 243 ~; 614 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 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 : 46 ( 0 sgn 22 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f35,hypothesis,
( mustard(lang)
| ~ neither(mill) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule8_3) ).
fof(f35_nnf,plain,
( mustard(lang)
| ~ neither(mill) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
( mustard(lang)
| ~ neither(mill) ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
( mustard(lang)
| ~ neither(mill) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(f11,axiom,
( neither(X)
| mustard(X)
| salt(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neither4) ).
fof(f11_nnf,plain,
! [X] :
( neither(X)
| mustard(X)
| salt(X) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X] :
( neither(X)
| mustard(X)
| salt(X) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( neither(X0)
| mustard(X0)
| salt(X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p64,plain,
( mustard(mill)
| salt(mill)
| mustard(lang) ),
inference(resolution,[status(thm)],[c35,c11]) ).
cnf(f39,hypothesis,
( oneof(dix)
| oneof(cole)
| ~ mustard(mill) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule10_1) ).
fof(f39_nnf,plain,
( oneof(dix)
| oneof(cole)
| ~ mustard(mill) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
( oneof(dix)
| oneof(cole)
| ~ mustard(mill) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( oneof(dix)
| oneof(cole)
| ~ mustard(mill) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p78,plain,
( oneof(dix)
| oneof(cole)
| salt(mill)
| mustard(lang) ),
inference(resolution,[status(thm)],[p64,c39]) ).
cnf(f32,hypothesis,
( salt(lang)
| ~ oneof(dix) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule7_3) ).
fof(f32_nnf,plain,
( salt(lang)
| ~ oneof(dix) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
( salt(lang)
| ~ oneof(dix) ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c32,plain,
( salt(lang)
| ~ oneof(dix) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p114,plain,
( salt(lang)
| oneof(cole)
| salt(mill)
| mustard(lang) ),
inference(resolution,[status(thm)],[p78,c32]) ).
cnf(f13,hypothesis,
( salt(barry)
| ~ oneof(cole) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule1_2) ).
fof(f13_nnf,plain,
( salt(barry)
| ~ oneof(cole) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
( salt(barry)
| ~ oneof(cole) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( salt(barry)
| ~ oneof(cole) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p174,plain,
( salt(barry)
| salt(lang)
| salt(mill)
| mustard(lang) ),
inference(resolution,[status(thm)],[p114,c13]) ).
cnf(f6,axiom,
( oneof(X)
| neither(X)
| both(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',one_condition_holds1) ).
fof(f6_nnf,plain,
! [X] :
( oneof(X)
| neither(X)
| both(X) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X] :
( oneof(X)
| neither(X)
| both(X) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( oneof(X0)
| neither(X0)
| both(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(f10,axiom,
( ~ mustard(X)
| ~ neither(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neither3) ).
fof(f10_nnf,plain,
! [X] :
( ~ mustard(X)
| ~ neither(X) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X] :
( ~ mustard(X)
| ~ neither(X) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( ~ mustard(X0)
| ~ neither(X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p45,plain,
( ~ mustard(X0)
| oneof(X0)
| both(X0) ),
inference(resolution,[status(thm)],[c6,c10]) ).
cnf(p225,plain,
( oneof(lang)
| both(lang)
| salt(barry)
| salt(lang)
| salt(mill) ),
inference(resolution,[status(thm)],[p174,p45]) ).
cnf(f14,hypothesis,
( salt(barry)
| ~ oneof(lang) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule1_3) ).
fof(f14_nnf,plain,
( salt(barry)
| ~ oneof(lang) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
( salt(barry)
| ~ oneof(lang) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( salt(barry)
| ~ oneof(lang) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p335,plain,
( salt(barry)
| both(lang)
| salt(barry)
| salt(lang)
| salt(mill) ),
inference(resolution,[status(thm)],[p225,c14]) ).
cnf(p384,plain,
( both(lang)
| salt(barry)
| salt(lang)
| salt(mill) ),
inference(factoring,[status(thm)],[p335]) ).
cnf(f36,hypothesis,
( both(lang)
| both(barry)
| ~ salt(mill) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule9_1) ).
fof(f36_nnf,plain,
( both(lang)
| both(barry)
| ~ salt(mill) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
( both(lang)
| both(barry)
| ~ salt(mill) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
( both(lang)
| both(barry)
| ~ salt(mill) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p386,plain,
( both(lang)
| both(barry)
| both(lang)
| salt(barry)
| salt(lang) ),
inference(resolution,[status(thm)],[p384,c36]) ).
cnf(p420,plain,
( both(barry)
| both(lang)
| salt(barry)
| salt(lang) ),
inference(factoring,[status(thm)],[p386]) ).
cnf(f9,axiom,
( ~ salt(X)
| ~ neither(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neither2) ).
fof(f9_nnf,plain,
! [X] :
( ~ salt(X)
| ~ neither(X) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X] :
( ~ salt(X)
| ~ neither(X) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( ~ salt(X0)
| ~ neither(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p44,plain,
( ~ salt(X0)
| oneof(X0)
| both(X0) ),
inference(resolution,[status(thm)],[c6,c9]) ).
cnf(p427,plain,
( oneof(lang)
| both(lang)
| both(barry)
| both(lang)
| salt(barry) ),
inference(resolution,[status(thm)],[p420,p44]) ).
cnf(p464,plain,
( oneof(lang)
| both(barry)
| both(lang)
| salt(barry) ),
inference(factoring,[status(thm)],[p427]) ).
cnf(p466,plain,
( salt(barry)
| both(barry)
| both(lang)
| salt(barry) ),
inference(resolution,[status(thm)],[p464,c14]) ).
cnf(p468,plain,
( both(barry)
| both(lang)
| salt(barry) ),
inference(factoring,[status(thm)],[p466]) ).
cnf(p471,plain,
( oneof(barry)
| both(barry)
| both(barry)
| both(lang) ),
inference(resolution,[status(thm)],[p468,p44]) ).
cnf(p477,plain,
( oneof(barry)
| both(barry)
| both(lang) ),
inference(factoring,[status(thm)],[p471]) ).
cnf(f31,hypothesis,
( salt(lang)
| ~ oneof(barry) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule7_2) ).
fof(f31_nnf,plain,
( salt(lang)
| ~ oneof(barry) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
( salt(lang)
| ~ oneof(barry) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
( salt(lang)
| ~ oneof(barry) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p480,plain,
( salt(lang)
| both(barry)
| both(lang) ),
inference(resolution,[status(thm)],[p477,c31]) ).
cnf(f16,hypothesis,
( mustard(barry)
| ~ neither(dix) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule2_2) ).
fof(f16_nnf,plain,
( mustard(barry)
| ~ neither(dix) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
( mustard(barry)
| ~ neither(dix) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( mustard(barry)
| ~ neither(dix) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p51,plain,
( mustard(barry)
| mustard(dix)
| salt(dix) ),
inference(resolution,[status(thm)],[c11,c16]) ).
cnf(f27,hypothesis,
( neither(mill)
| neither(lang)
| ~ mustard(dix) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule6_1) ).
fof(f27_nnf,plain,
( neither(mill)
| neither(lang)
| ~ mustard(dix) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
( neither(mill)
| neither(lang)
| ~ mustard(dix) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
( neither(mill)
| neither(lang)
| ~ mustard(dix) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p69,plain,
( neither(mill)
| neither(lang)
| mustard(barry)
| salt(dix) ),
inference(resolution,[status(thm)],[p51,c27]) ).
cnf(p91,plain,
( mustard(lang)
| neither(lang)
| mustard(barry)
| salt(dix) ),
inference(resolution,[status(thm)],[p69,c35]) ).
cnf(p136,plain,
( ~ salt(lang)
| mustard(lang)
| mustard(barry)
| salt(dix) ),
inference(resolution,[status(thm)],[p91,c9]) ).
cnf(p485,plain,
( mustard(lang)
| mustard(barry)
| salt(dix)
| both(barry)
| both(lang) ),
inference(resolution,[status(thm)],[p480,p136]) ).
cnf(f2,axiom,
( both(X)
| ~ mustard(X)
| ~ salt(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',both3) ).
fof(f2_nnf,plain,
! [X] :
( both(X)
| ~ mustard(X)
| ~ salt(X) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X] :
( both(X)
| ~ mustard(X)
| ~ salt(X) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( both(X0)
| ~ mustard(X0)
| ~ salt(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p483,plain,
( both(lang)
| ~ mustard(lang)
| both(barry)
| both(lang) ),
inference(resolution,[status(thm)],[p480,c2]) ).
cnf(p492,plain,
( ~ mustard(lang)
| both(barry)
| both(lang) ),
inference(factoring,[status(thm)],[p483]) ).
cnf(p530,plain,
( both(barry)
| both(lang)
| mustard(barry)
| salt(dix)
| both(barry)
| both(lang) ),
inference(resolution,[status(thm)],[p485,p492]) ).
cnf(p565,plain,
( both(barry)
| mustard(barry)
| salt(dix)
| both(barry)
| both(lang) ),
inference(factoring,[status(thm)],[p530]) ).
cnf(p567,plain,
( mustard(barry)
| salt(dix)
| both(barry)
| both(lang) ),
inference(factoring,[status(thm)],[p565]) ).
cnf(p469,plain,
( both(barry)
| ~ mustard(barry)
| both(barry)
| both(lang) ),
inference(resolution,[status(thm)],[p468,c2]) ).
cnf(p472,plain,
( ~ mustard(barry)
| both(barry)
| both(lang) ),
inference(factoring,[status(thm)],[p469]) ).
cnf(p569,plain,
( both(barry)
| both(lang)
| salt(dix)
| both(barry)
| both(lang) ),
inference(resolution,[status(thm)],[p567,p472]) ).
cnf(p573,plain,
( both(barry)
| salt(dix)
| both(barry)
| both(lang) ),
inference(factoring,[status(thm)],[p569]) ).
cnf(p575,plain,
( salt(dix)
| both(barry)
| both(lang) ),
inference(factoring,[status(thm)],[p573]) ).
cnf(f24,hypothesis,
( both(cole)
| neither(barry)
| ~ salt(dix) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule5_1) ).
fof(f24_nnf,plain,
( both(cole)
| neither(barry)
| ~ salt(dix) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
( both(cole)
| neither(barry)
| ~ salt(dix) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( both(cole)
| neither(barry)
| ~ salt(dix) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p576,plain,
( both(cole)
| neither(barry)
| both(barry)
| both(lang) ),
inference(resolution,[status(thm)],[p575,c24]) ).
cnf(f5,axiom,
( ~ neither(X)
| ~ oneof(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',oneof3) ).
fof(f5_nnf,plain,
! [X] :
( ~ neither(X)
| ~ oneof(X) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X] :
( ~ neither(X)
| ~ oneof(X) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( ~ neither(X0)
| ~ oneof(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p478,plain,
( ~ neither(barry)
| both(barry)
| both(lang) ),
inference(resolution,[status(thm)],[p477,c5]) ).
cnf(p579,plain,
( both(barry)
| both(lang)
| both(cole)
| both(barry)
| both(lang) ),
inference(resolution,[status(thm)],[p576,p478]) ).
cnf(p583,plain,
( both(barry)
| both(cole)
| both(barry)
| both(lang) ),
inference(factoring,[status(thm)],[p579]) ).
cnf(p585,plain,
( both(cole)
| both(barry)
| both(lang) ),
inference(factoring,[status(thm)],[p583]) ).
cnf(f23,hypothesis,
( mustard(cole)
| ~ both(lang) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule4_3) ).
fof(f23_nnf,plain,
( mustard(cole)
| ~ both(lang) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
( mustard(cole)
| ~ both(lang) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( mustard(cole)
| ~ both(lang) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p589,plain,
( mustard(cole)
| both(cole)
| both(barry) ),
inference(resolution,[status(thm)],[p585,c23]) ).
cnf(p595,plain,
( oneof(cole)
| both(cole)
| both(cole)
| both(barry) ),
inference(resolution,[status(thm)],[p589,p45]) ).
cnf(p614,plain,
( oneof(cole)
| both(cole)
| both(barry) ),
inference(factoring,[status(thm)],[p595]) ).
cnf(p617,plain,
( salt(barry)
| both(cole)
| both(barry) ),
inference(resolution,[status(thm)],[p614,c13]) ).
cnf(p619,plain,
( oneof(barry)
| both(barry)
| both(cole)
| both(barry) ),
inference(resolution,[status(thm)],[p617,p44]) ).
cnf(p635,plain,
( oneof(barry)
| both(cole)
| both(barry) ),
inference(factoring,[status(thm)],[p619]) ).
cnf(f19,hypothesis,
( salt(cole)
| ~ oneof(barry) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule3_2) ).
fof(f19_nnf,plain,
( salt(cole)
| ~ oneof(barry) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
( salt(cole)
| ~ oneof(barry) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
( salt(cole)
| ~ oneof(barry) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p637,plain,
( salt(cole)
| both(cole)
| both(barry) ),
inference(resolution,[status(thm)],[p635,c19]) ).
cnf(p638,plain,
( both(cole)
| ~ mustard(cole)
| both(cole)
| both(barry) ),
inference(resolution,[status(thm)],[p637,c2]) ).
cnf(p641,plain,
( ~ mustard(cole)
| both(cole)
| both(barry) ),
inference(factoring,[status(thm)],[p638]) ).
cnf(p642,plain,
( both(cole)
| both(barry)
| both(cole)
| both(barry) ),
inference(resolution,[status(thm)],[p641,p589]) ).
cnf(p643,plain,
( both(cole)
| both(cole)
| both(barry) ),
inference(factoring,[status(thm)],[p642]) ).
cnf(p645,plain,
( both(cole)
| both(barry) ),
inference(factoring,[status(thm)],[p643]) ).
cnf(f1,axiom,
( mustard(X)
| ~ both(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',both2) ).
fof(f1_nnf,plain,
! [X] :
( mustard(X)
| ~ both(X) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X] :
( mustard(X)
| ~ both(X) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( mustard(X0)
| ~ both(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p647,plain,
( mustard(cole)
| both(barry) ),
inference(resolution,[status(thm)],[p645,c1]) ).
cnf(f21,hypothesis,
( both(lang)
| both(dix)
| ~ mustard(cole) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule4_1) ).
fof(f21_nnf,plain,
( both(lang)
| both(dix)
| ~ mustard(cole) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
( both(lang)
| both(dix)
| ~ mustard(cole) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( both(lang)
| both(dix)
| ~ mustard(cole) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p653,plain,
( both(lang)
| both(dix)
| both(barry) ),
inference(resolution,[status(thm)],[p647,c21]) ).
cnf(p663,plain,
( mustard(dix)
| both(lang)
| both(barry) ),
inference(resolution,[status(thm)],[p653,c1]) ).
cnf(p680,plain,
( neither(mill)
| neither(lang)
| both(lang)
| both(barry) ),
inference(resolution,[status(thm)],[p663,c27]) ).
cnf(p692,plain,
( mustard(lang)
| neither(lang)
| both(lang)
| both(barry) ),
inference(resolution,[status(thm)],[p680,c35]) ).
cnf(p484,plain,
( oneof(lang)
| both(lang)
| both(barry)
| both(lang) ),
inference(resolution,[status(thm)],[p480,p44]) ).
cnf(p495,plain,
( oneof(lang)
| both(barry)
| both(lang) ),
inference(factoring,[status(thm)],[p484]) ).
cnf(p496,plain,
( ~ neither(lang)
| both(barry)
| both(lang) ),
inference(resolution,[status(thm)],[p495,c5]) ).
cnf(p703,plain,
( both(barry)
| both(lang)
| mustard(lang)
| both(lang)
| both(barry) ),
inference(resolution,[status(thm)],[p692,p496]) ).
cnf(p716,plain,
( both(lang)
| mustard(lang)
| both(lang)
| both(barry) ),
inference(factoring,[status(thm)],[p703]) ).
cnf(p718,plain,
( mustard(lang)
| both(lang)
| both(barry) ),
inference(factoring,[status(thm)],[p716]) ).
cnf(p720,plain,
( both(barry)
| both(lang)
| both(lang)
| both(barry) ),
inference(resolution,[status(thm)],[p718,p492]) ).
cnf(p722,plain,
( both(lang)
| both(lang)
| both(barry) ),
inference(factoring,[status(thm)],[p720]) ).
cnf(p725,plain,
( both(lang)
| both(barry) ),
inference(factoring,[status(thm)],[p722]) ).
cnf(p727,plain,
( mustard(lang)
| both(barry) ),
inference(resolution,[status(thm)],[p725,c1]) ).
cnf(f33,hypothesis,
( neither(mill)
| neither(cole)
| ~ mustard(lang) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule8_1) ).
fof(f33_nnf,plain,
( neither(mill)
| neither(cole)
| ~ mustard(lang) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
( neither(mill)
| neither(cole)
| ~ mustard(lang) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
( neither(mill)
| neither(cole)
| ~ mustard(lang) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p731,plain,
( neither(mill)
| neither(cole)
| both(barry) ),
inference(resolution,[status(thm)],[p727,c33]) ).
cnf(p739,plain,
( ~ mustard(mill)
| neither(cole)
| both(barry) ),
inference(resolution,[status(thm)],[p731,c10]) ).
cnf(f38,hypothesis,
( mustard(mill)
| ~ both(lang) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule9_3) ).
fof(f38_nnf,plain,
( mustard(mill)
| ~ both(lang) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
( mustard(mill)
| ~ both(lang) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c38,plain,
( mustard(mill)
| ~ both(lang) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(p729,plain,
( mustard(mill)
| both(barry) ),
inference(resolution,[status(thm)],[p725,c38]) ).
cnf(p754,plain,
( both(barry)
| neither(cole)
| both(barry) ),
inference(resolution,[status(thm)],[p739,p729]) ).
cnf(p764,plain,
( neither(cole)
| both(barry) ),
inference(factoring,[status(thm)],[p754]) ).
cnf(f8,axiom,
( ~ neither(X)
| ~ both(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',neither1) ).
fof(f8_nnf,plain,
! [X] :
( ~ neither(X)
| ~ both(X) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X] :
( ~ neither(X)
| ~ both(X) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( ~ neither(X0)
| ~ both(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p648,plain,
( ~ neither(cole)
| both(barry) ),
inference(resolution,[status(thm)],[p645,c8]) ).
cnf(p767,plain,
( both(barry)
| both(barry) ),
inference(resolution,[status(thm)],[p764,p648]) ).
cnf(p769,plain,
both(barry),
inference(factoring,[status(thm)],[p767]) ).
cnf(f37,hypothesis,
( salt(mill)
| ~ both(barry) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule9_2) ).
fof(f37_nnf,plain,
( salt(mill)
| ~ both(barry) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
( salt(mill)
| ~ both(barry) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
( salt(mill)
| ~ both(barry) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p777,plain,
salt(mill),
inference(resolution,[status(thm)],[p769,c37]) ).
cnf(p821,plain,
( oneof(mill)
| both(mill) ),
inference(resolution,[status(thm)],[p777,p44]) ).
cnf(f0,axiom,
( salt(X)
| ~ both(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',both1) ).
fof(f0_nnf,plain,
! [X] :
( salt(X)
| ~ both(X) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X] :
( salt(X)
| ~ both(X) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( salt(X0)
| ~ both(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p770,plain,
salt(barry),
inference(resolution,[status(thm)],[p769,c0]) ).
cnf(f12,hypothesis,
( oneof(lang)
| oneof(cole)
| ~ salt(barry) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule1_1) ).
fof(f12_nnf,plain,
( oneof(lang)
| oneof(cole)
| ~ salt(barry) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
( oneof(lang)
| oneof(cole)
| ~ salt(barry) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( oneof(lang)
| oneof(cole)
| ~ salt(barry) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p810,plain,
( oneof(lang)
| oneof(cole) ),
inference(resolution,[status(thm)],[p770,c12]) ).
cnf(f28,hypothesis,
( mustard(dix)
| ~ neither(lang) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule6_2) ).
fof(f28_nnf,plain,
( mustard(dix)
| ~ neither(lang) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
( mustard(dix)
| ~ neither(lang) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( mustard(dix)
| ~ neither(lang) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(p58,plain,
( mustard(lang)
| salt(lang)
| mustard(dix) ),
inference(resolution,[status(thm)],[c28,c11]) ).
cnf(p73,plain,
( oneof(dix)
| both(dix)
| mustard(lang)
| salt(lang) ),
inference(resolution,[status(thm)],[p58,p45]) ).
cnf(p103,plain,
( salt(lang)
| both(dix)
| mustard(lang)
| salt(lang) ),
inference(resolution,[status(thm)],[p73,c32]) ).
cnf(p156,plain,
( both(dix)
| mustard(lang)
| salt(lang) ),
inference(factoring,[status(thm)],[p103]) ).
cnf(p160,plain,
( neither(mill)
| neither(cole)
| both(dix)
| salt(lang) ),
inference(resolution,[status(thm)],[p156,c33]) ).
cnf(f29,hypothesis,
( mustard(dix)
| ~ neither(mill) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule6_3) ).
fof(f29_nnf,plain,
( mustard(dix)
| ~ neither(mill) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
( mustard(dix)
| ~ neither(mill) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( mustard(dix)
| ~ neither(mill) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(p217,plain,
( mustard(dix)
| neither(cole)
| both(dix)
| salt(lang) ),
inference(resolution,[status(thm)],[p160,c29]) ).
cnf(p60,plain,
( mustard(mill)
| salt(mill)
| mustard(dix) ),
inference(resolution,[status(thm)],[c29,c11]) ).
cnf(p74,plain,
( oneof(dix)
| oneof(cole)
| salt(mill)
| mustard(dix) ),
inference(resolution,[status(thm)],[p60,c39]) ).
cnf(p107,plain,
( salt(lang)
| oneof(cole)
| salt(mill)
| mustard(dix) ),
inference(resolution,[status(thm)],[p74,c32]) ).
cnf(p164,plain,
( ~ neither(cole)
| salt(lang)
| salt(mill)
| mustard(dix) ),
inference(resolution,[status(thm)],[p107,c5]) ).
cnf(p264,plain,
( salt(lang)
| salt(mill)
| mustard(dix)
| mustard(dix)
| both(dix)
| salt(lang) ),
inference(resolution,[status(thm)],[p217,p164]) ).
cnf(p367,plain,
( salt(mill)
| mustard(dix)
| mustard(dix)
| both(dix)
| salt(lang) ),
inference(factoring,[status(thm)],[p264]) ).
cnf(p409,plain,
( salt(mill)
| mustard(dix)
| both(dix)
| salt(lang) ),
inference(factoring,[status(thm)],[p367]) ).
cnf(p411,plain,
( oneof(dix)
| both(dix)
| salt(mill)
| both(dix)
| salt(lang) ),
inference(resolution,[status(thm)],[p409,p45]) ).
cnf(p439,plain,
( oneof(dix)
| salt(mill)
| both(dix)
| salt(lang) ),
inference(factoring,[status(thm)],[p411]) ).
cnf(p441,plain,
( salt(lang)
| salt(mill)
| both(dix)
| salt(lang) ),
inference(resolution,[status(thm)],[p439,c32]) ).
cnf(p445,plain,
( salt(mill)
| both(dix)
| salt(lang) ),
inference(factoring,[status(thm)],[p441]) ).
cnf(p214,plain,
( ~ salt(mill)
| neither(cole)
| both(dix)
| salt(lang) ),
inference(resolution,[status(thm)],[p160,c9]) ).
cnf(p449,plain,
( neither(cole)
| both(dix)
| salt(lang)
| both(dix)
| salt(lang) ),
inference(resolution,[status(thm)],[p445,p214]) ).
cnf(p502,plain,
( neither(cole)
| both(dix)
| both(dix)
| salt(lang) ),
inference(factoring,[status(thm)],[p449]) ).
cnf(p504,plain,
( neither(cole)
| both(dix)
| salt(lang) ),
inference(factoring,[status(thm)],[p502]) ).
cnf(f42,negated_conjecture,
( ~ oneof(mill)
| ~ mustard(lang)
| ~ salt(mill)
| ~ oneof(lang)
| ~ both(barry)
| ~ neither(dix)
| ~ neither(cole) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_who_takes_what) ).
fof(f42_nnf,plain,
( ~ oneof(mill)
| ~ mustard(lang)
| ~ salt(mill)
| ~ oneof(lang)
| ~ both(barry)
| ~ neither(dix)
| ~ neither(cole) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
( ~ oneof(mill)
| ~ mustard(lang)
| ~ salt(mill)
| ~ oneof(lang)
| ~ both(barry)
| ~ neither(dix)
| ~ neither(cole) ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c42,plain,
( ~ oneof(mill)
| ~ mustard(lang)
| ~ salt(mill)
| ~ oneof(lang)
| ~ both(barry)
| ~ neither(dix)
| ~ neither(cole) ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p507,plain,
( ~ oneof(mill)
| ~ mustard(lang)
| ~ salt(mill)
| ~ oneof(lang)
| ~ both(barry)
| ~ neither(dix)
| both(dix)
| salt(lang) ),
inference(resolution,[status(thm)],[p504,c42]) ).
cnf(p46,plain,
( mustard(barry)
| oneof(dix)
| both(dix) ),
inference(resolution,[status(thm)],[c6,c16]) ).
cnf(p65,plain,
( salt(lang)
| mustard(barry)
| both(dix) ),
inference(resolution,[status(thm)],[p46,c32]) ).
cnf(f15,hypothesis,
( both(mill)
| neither(dix)
| ~ mustard(barry) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule2_1) ).
fof(f15_nnf,plain,
( both(mill)
| neither(dix)
| ~ mustard(barry) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
( both(mill)
| neither(dix)
| ~ mustard(barry) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( both(mill)
| neither(dix)
| ~ mustard(barry) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p79,plain,
( both(mill)
| neither(dix)
| salt(lang)
| both(dix) ),
inference(resolution,[status(thm)],[p65,c15]) ).
cnf(p511,plain,
( both(mill)
| salt(lang)
| both(dix)
| ~ oneof(mill)
| ~ mustard(lang)
| ~ salt(mill)
| ~ oneof(lang)
| ~ both(barry)
| both(dix)
| salt(lang) ),
inference(resolution,[status(thm)],[p507,p79]) ).
cnf(p514,plain,
( both(mill)
| both(dix)
| ~ oneof(mill)
| ~ mustard(lang)
| ~ salt(mill)
| ~ oneof(lang)
| ~ both(barry)
| both(dix)
| salt(lang) ),
inference(factoring,[status(thm)],[p511]) ).
cnf(p516,plain,
( both(mill)
| ~ oneof(mill)
| ~ mustard(lang)
| ~ salt(mill)
| ~ oneof(lang)
| ~ both(barry)
| both(dix)
| salt(lang) ),
inference(factoring,[status(thm)],[p514]) ).
cnf(p782,plain,
( both(mill)
| ~ oneof(mill)
| ~ mustard(lang)
| ~ salt(mill)
| ~ oneof(lang)
| both(dix)
| salt(lang) ),
inference(resolution,[status(thm)],[p769,p516]) ).
cnf(p878,plain,
( both(mill)
| ~ oneof(mill)
| ~ mustard(lang)
| ~ salt(mill)
| both(dix)
| salt(lang)
| oneof(cole) ),
inference(resolution,[status(thm)],[p810,p782]) ).
cnf(p889,plain,
( both(mill)
| ~ oneof(mill)
| ~ mustard(lang)
| both(dix)
| salt(lang)
| oneof(cole) ),
inference(resolution,[status(thm)],[p878,p777]) ).
cnf(p891,plain,
( both(dix)
| salt(lang)
| both(mill)
| ~ oneof(mill)
| both(dix)
| salt(lang)
| oneof(cole) ),
inference(resolution,[status(thm)],[p889,p156]) ).
cnf(p900,plain,
( both(dix)
| both(mill)
| ~ oneof(mill)
| both(dix)
| salt(lang)
| oneof(cole) ),
inference(factoring,[status(thm)],[p891]) ).
cnf(p902,plain,
( both(mill)
| ~ oneof(mill)
| both(dix)
| salt(lang)
| oneof(cole) ),
inference(factoring,[status(thm)],[p900]) ).
cnf(p910,plain,
( both(mill)
| both(dix)
| salt(lang)
| oneof(cole)
| both(mill) ),
inference(resolution,[status(thm)],[p821,p902]) ).
cnf(p925,plain,
( both(dix)
| salt(lang)
| oneof(cole)
| both(mill) ),
inference(factoring,[status(thm)],[p910]) ).
cnf(f40,hypothesis,
( mustard(mill)
| ~ oneof(cole) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule10_2) ).
fof(f40_nnf,plain,
( mustard(mill)
| ~ oneof(cole) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
( mustard(mill)
| ~ oneof(cole) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,plain,
( mustard(mill)
| ~ oneof(cole) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p929,plain,
( mustard(mill)
| both(dix)
| salt(lang)
| both(mill) ),
inference(resolution,[status(thm)],[p925,c40]) ).
cnf(p820,plain,
( both(mill)
| ~ mustard(mill) ),
inference(resolution,[status(thm)],[p777,c2]) ).
cnf(p934,plain,
( both(mill)
| both(dix)
| salt(lang)
| both(mill) ),
inference(resolution,[status(thm)],[p929,p820]) ).
cnf(p935,plain,
( both(dix)
| salt(lang)
| both(mill) ),
inference(factoring,[status(thm)],[p934]) ).
cnf(f30,hypothesis,
( oneof(dix)
| oneof(barry)
| ~ salt(lang) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule7_1) ).
fof(f30_nnf,plain,
( oneof(dix)
| oneof(barry)
| ~ salt(lang) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
( oneof(dix)
| oneof(barry)
| ~ salt(lang) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( oneof(dix)
| oneof(barry)
| ~ salt(lang) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p937,plain,
( oneof(dix)
| oneof(barry)
| both(dix)
| both(mill) ),
inference(resolution,[status(thm)],[p935,c30]) ).
cnf(p943,plain,
( ~ neither(dix)
| oneof(barry)
| both(dix)
| both(mill) ),
inference(resolution,[status(thm)],[p937,c5]) ).
cnf(p771,plain,
mustard(barry),
inference(resolution,[status(thm)],[p769,c1]) ).
cnf(p813,plain,
( both(mill)
| neither(dix) ),
inference(resolution,[status(thm)],[p771,c15]) ).
cnf(p947,plain,
( both(mill)
| oneof(barry)
| both(dix)
| both(mill) ),
inference(resolution,[status(thm)],[p943,p813]) ).
cnf(p953,plain,
( oneof(barry)
| both(dix)
| both(mill) ),
inference(factoring,[status(thm)],[p947]) ).
cnf(f4,axiom,
( ~ both(X)
| ~ oneof(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',oneof2) ).
fof(f4_nnf,plain,
! [X] :
( ~ both(X)
| ~ oneof(X) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X] :
( ~ both(X)
| ~ oneof(X) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( ~ both(X0)
| ~ oneof(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p954,plain,
( ~ both(barry)
| both(dix)
| both(mill) ),
inference(resolution,[status(thm)],[p953,c4]) ).
cnf(p957,plain,
( both(dix)
| both(mill) ),
inference(resolution,[status(thm)],[p954,p769]) ).
cnf(p959,plain,
( mustard(mill)
| both(dix) ),
inference(resolution,[status(thm)],[p957,c1]) ).
cnf(p961,plain,
( oneof(dix)
| oneof(cole)
| both(dix) ),
inference(resolution,[status(thm)],[p959,c39]) ).
cnf(p964,plain,
( salt(lang)
| oneof(cole)
| both(dix) ),
inference(resolution,[status(thm)],[p961,c32]) ).
cnf(p967,plain,
( ~ neither(cole)
| salt(lang)
| both(dix) ),
inference(resolution,[status(thm)],[p964,c5]) ).
cnf(p969,plain,
( both(dix)
| salt(lang)
| salt(lang)
| both(dix) ),
inference(resolution,[status(thm)],[p967,p504]) ).
cnf(p974,plain,
( salt(lang)
| salt(lang)
| both(dix) ),
inference(factoring,[status(thm)],[p969]) ).
cnf(p976,plain,
( salt(lang)
| both(dix) ),
inference(factoring,[status(thm)],[p974]) ).
cnf(p978,plain,
( oneof(dix)
| oneof(barry)
| both(dix) ),
inference(resolution,[status(thm)],[p976,c30]) ).
cnf(f3,axiom,
( mustard(X)
| salt(X)
| ~ oneof(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',oneof1) ).
fof(f3_nnf,plain,
! [X] :
( mustard(X)
| salt(X)
| ~ oneof(X) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X] :
( mustard(X)
| salt(X)
| ~ oneof(X) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( mustard(X0)
| salt(X0)
| ~ oneof(X0) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p982,plain,
( mustard(dix)
| salt(dix)
| oneof(barry)
| both(dix) ),
inference(resolution,[status(thm)],[p978,c3]) ).
cnf(p991,plain,
( ~ both(barry)
| mustard(dix)
| salt(dix)
| both(dix) ),
inference(resolution,[status(thm)],[p982,c4]) ).
cnf(p996,plain,
( mustard(dix)
| salt(dix)
| both(dix) ),
inference(resolution,[status(thm)],[p991,p769]) ).
cnf(p998,plain,
( neither(mill)
| neither(lang)
| salt(dix)
| both(dix) ),
inference(resolution,[status(thm)],[p996,c27]) ).
cnf(p1000,plain,
( ~ salt(mill)
| neither(lang)
| salt(dix)
| both(dix) ),
inference(resolution,[status(thm)],[p998,c9]) ).
cnf(p1008,plain,
( neither(lang)
| salt(dix)
| both(dix) ),
inference(resolution,[status(thm)],[p1000,p777]) ).
cnf(p1009,plain,
( ~ salt(lang)
| salt(dix)
| both(dix) ),
inference(resolution,[status(thm)],[p1008,c9]) ).
cnf(p1013,plain,
( both(dix)
| salt(dix)
| both(dix) ),
inference(resolution,[status(thm)],[p1009,p976]) ).
cnf(p1017,plain,
( salt(dix)
| both(dix) ),
inference(factoring,[status(thm)],[p1013]) ).
cnf(p1020,plain,
( both(cole)
| neither(barry)
| both(dix) ),
inference(resolution,[status(thm)],[p1017,c24]) ).
cnf(p772,plain,
~ neither(barry),
inference(resolution,[status(thm)],[p769,c8]) ).
cnf(p1025,plain,
( both(cole)
| both(dix) ),
inference(resolution,[status(thm)],[p1020,p772]) ).
cnf(p1027,plain,
( salt(dix)
| both(cole) ),
inference(resolution,[status(thm)],[p1025,c0]) ).
cnf(p1031,plain,
( both(cole)
| neither(barry)
| both(cole) ),
inference(resolution,[status(thm)],[p1027,c24]) ).
cnf(p1041,plain,
( neither(barry)
| both(cole) ),
inference(factoring,[status(thm)],[p1031]) ).
cnf(p1046,plain,
both(cole),
inference(resolution,[status(thm)],[p1041,p772]) ).
cnf(f26,hypothesis,
( salt(dix)
| ~ both(cole) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule5_3) ).
fof(f26_nnf,plain,
( salt(dix)
| ~ both(cole) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
( salt(dix)
| ~ both(cole) ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
( salt(dix)
| ~ both(cole) ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p1050,plain,
salt(dix),
inference(resolution,[status(thm)],[p1046,c26]) ).
cnf(p892,plain,
( ~ salt(dix)
| both(mill) ),
inference(resolution,[status(thm)],[p813,c9]) ).
cnf(p1054,plain,
both(mill),
inference(resolution,[status(thm)],[p1050,p892]) ).
cnf(p1056,plain,
~ neither(mill),
inference(resolution,[status(thm)],[p1054,c8]) ).
cnf(p1047,plain,
salt(cole),
inference(resolution,[status(thm)],[p1046,c0]) ).
cnf(f18,hypothesis,
( neither(mill)
| oneof(barry)
| ~ salt(cole) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule3_1) ).
fof(f18_nnf,plain,
( neither(mill)
| oneof(barry)
| ~ salt(cole) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
( neither(mill)
| oneof(barry)
| ~ salt(cole) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( neither(mill)
| oneof(barry)
| ~ salt(cole) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p1051,plain,
( neither(mill)
| oneof(barry) ),
inference(resolution,[status(thm)],[p1047,c18]) ).
cnf(p1060,plain,
oneof(barry),
inference(resolution,[status(thm)],[p1056,p1051]) ).
cnf(p1061,plain,
~ both(barry),
inference(resolution,[status(thm)],[p1060,c4]) ).
cnf(p1064,plain,
$false,
inference(resolution,[status(thm)],[p1061,p769]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ030-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/5.39 % Computer : n017.cluster.edu
% 0.11/5.39 % Model : x86_64 x86_64
% 0.11/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.39 % Memory : 8046.5625MB
% 0.11/5.39 % OS : Linux 6.8.0-71-generic
% 0.11/5.39 % CPULimit : 300
% 0.11/5.39 % WCLimit : 300
% 0.11/5.39 % DateTime : Thu Sep 24 06:37:51 UTC 2026
% 0.15/5.40 % CPUTime :
% 0.15/5.40 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 4.59/6.18 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.59/6.18 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------