%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PUZ030-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n016.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 7.25s 6.58s
% Output : Proof 7.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 93
% Number of leaves : 39
% Syntax : Number of formulae : 315 ( 7 unt; 0 def)
% Number of atoms : 1146 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 1196 ( 365 ~; 831 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 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 :
%------------------------------------------------------------------------------
cnf(f48,hypothesis,
( ~ salt_dix
| ~ mustard_dix
| ~ salt_cole
| ~ mustard_cole
| ~ mustard_mill ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c49) ).
fof(f48_nnf,plain,
( ~ salt_dix
| ~ mustard_dix
| ~ salt_cole
| ~ mustard_cole
| ~ mustard_mill ),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
( ~ salt_dix
| ~ mustard_dix
| ~ salt_cole
| ~ mustard_cole
| ~ mustard_mill ),
inference(skolemisation,[status(esa)],[f48_nnf]) ).
cnf(c48,plain,
( ~ salt_dix
| ~ mustard_dix
| ~ salt_cole
| ~ mustard_cole
| ~ mustard_mill ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(f55,hypothesis,
( mustard_lang
| mustard_mill
| salt_mill ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c56) ).
fof(f55_nnf,plain,
( mustard_lang
| mustard_mill
| salt_mill ),
inference(nnf_transformation,[status(thm)],[f55]) ).
fof(f55_sk,plain,
( mustard_lang
| mustard_mill
| salt_mill ),
inference(skolemisation,[status(esa)],[f55_nnf]) ).
cnf(c55,plain,
( mustard_lang
| mustard_mill
| salt_mill ),
inference(cnf_transformation,[status(esa)],[f55_sk]) ).
cnf(p83,plain,
( mustard_lang
| salt_mill
| ~ salt_dix
| ~ mustard_dix
| ~ salt_cole
| ~ mustard_cole ),
inference(resolution,[status(thm)],[c48,c55]) ).
cnf(f56,hypothesis,
( mustard_lang
| mustard_cole
| salt_cole ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c57) ).
fof(f56_nnf,plain,
( mustard_lang
| mustard_cole
| salt_cole ),
inference(nnf_transformation,[status(thm)],[f56]) ).
fof(f56_sk,plain,
( mustard_lang
| mustard_cole
| salt_cole ),
inference(skolemisation,[status(esa)],[f56_nnf]) ).
cnf(c56,plain,
( mustard_lang
| mustard_cole
| salt_cole ),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(f43,hypothesis,
( salt_barry
| mustard_cole
| ~ salt_cole ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c44) ).
fof(f43_nnf,plain,
( salt_barry
| mustard_cole
| ~ salt_cole ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
( salt_barry
| mustard_cole
| ~ salt_cole ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c43,plain,
( salt_barry
| mustard_cole
| ~ salt_cole ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p64,plain,
( salt_barry
| mustard_cole
| mustard_lang
| mustard_cole ),
inference(resolution,[status(thm)],[c56,c43]) ).
cnf(p82,plain,
( salt_barry
| mustard_lang
| mustard_cole ),
inference(factoring,[status(thm)],[p64]) ).
cnf(p129,plain,
( salt_barry
| mustard_lang
| mustard_lang
| salt_mill
| ~ salt_dix
| ~ mustard_dix
| ~ salt_cole ),
inference(resolution,[status(thm)],[p83,p82]) ).
cnf(p149,plain,
( salt_barry
| mustard_lang
| salt_mill
| ~ salt_dix
| ~ mustard_dix
| ~ salt_cole ),
inference(factoring,[status(thm)],[p129]) ).
cnf(f42,hypothesis,
( salt_barry
| ~ mustard_cole
| salt_cole ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c43) ).
fof(f42_nnf,plain,
( salt_barry
| ~ mustard_cole
| salt_cole ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
( salt_barry
| ~ mustard_cole
| salt_cole ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c42,plain,
( salt_barry
| ~ mustard_cole
| salt_cole ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p88,plain,
( salt_barry
| salt_cole
| salt_barry
| mustard_lang ),
inference(resolution,[status(thm)],[p82,c42]) ).
cnf(p120,plain,
( salt_cole
| salt_barry
| mustard_lang ),
inference(factoring,[status(thm)],[p88]) ).
cnf(p172,plain,
( salt_barry
| mustard_lang
| salt_barry
| mustard_lang
| salt_mill
| ~ salt_dix
| ~ mustard_dix ),
inference(resolution,[status(thm)],[p149,p120]) ).
cnf(p184,plain,
( salt_barry
| salt_barry
| mustard_lang
| salt_mill
| ~ salt_dix
| ~ mustard_dix ),
inference(factoring,[status(thm)],[p172]) ).
cnf(p193,plain,
( salt_barry
| mustard_lang
| salt_mill
| ~ salt_dix
| ~ mustard_dix ),
inference(factoring,[status(thm)],[p184]) ).
cnf(f16,hypothesis,
( mustard_lang
| mustard_dix
| ~ mustard_cole ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c17) ).
fof(f16_nnf,plain,
( mustard_lang
| mustard_dix
| ~ mustard_cole ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
( mustard_lang
| mustard_dix
| ~ mustard_cole ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( mustard_lang
| mustard_dix
| ~ mustard_cole ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p84,plain,
( mustard_lang
| mustard_dix
| salt_barry
| mustard_lang ),
inference(resolution,[status(thm)],[p82,c16]) ).
cnf(p117,plain,
( mustard_dix
| salt_barry
| mustard_lang ),
inference(factoring,[status(thm)],[p84]) ).
cnf(p195,plain,
( salt_barry
| mustard_lang
| salt_barry
| mustard_lang
| salt_mill
| ~ salt_dix ),
inference(resolution,[status(thm)],[p193,p117]) ).
cnf(p206,plain,
( salt_barry
| salt_barry
| mustard_lang
| salt_mill
| ~ salt_dix ),
inference(factoring,[status(thm)],[p195]) ).
cnf(p208,plain,
( salt_barry
| mustard_lang
| salt_mill
| ~ salt_dix ),
inference(factoring,[status(thm)],[p206]) ).
cnf(f18,hypothesis,
( mustard_lang
| salt_dix
| ~ mustard_cole ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c19) ).
fof(f18_nnf,plain,
( mustard_lang
| salt_dix
| ~ mustard_cole ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
( mustard_lang
| salt_dix
| ~ mustard_cole ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( mustard_lang
| salt_dix
| ~ mustard_cole ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p85,plain,
( mustard_lang
| salt_dix
| salt_barry
| mustard_lang ),
inference(resolution,[status(thm)],[p82,c18]) ).
cnf(p119,plain,
( salt_dix
| salt_barry
| mustard_lang ),
inference(factoring,[status(thm)],[p85]) ).
cnf(p210,plain,
( salt_barry
| mustard_lang
| salt_barry
| mustard_lang
| salt_mill ),
inference(resolution,[status(thm)],[p208,p119]) ).
cnf(p219,plain,
( salt_barry
| salt_barry
| mustard_lang
| salt_mill ),
inference(factoring,[status(thm)],[p210]) ).
cnf(p221,plain,
( salt_barry
| mustard_lang
| salt_mill ),
inference(factoring,[status(thm)],[p219]) ).
cnf(f54,hypothesis,
( mustard_lang
| salt_lang
| ~ salt_cole
| ~ mustard_cole
| ~ salt_barry ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c55) ).
fof(f54_nnf,plain,
( mustard_lang
| salt_lang
| ~ salt_cole
| ~ mustard_cole
| ~ salt_barry ),
inference(nnf_transformation,[status(thm)],[f54]) ).
fof(f54_sk,plain,
( mustard_lang
| salt_lang
| ~ salt_cole
| ~ mustard_cole
| ~ salt_barry ),
inference(skolemisation,[status(esa)],[f54_nnf]) ).
cnf(c54,plain,
( mustard_lang
| salt_lang
| ~ salt_cole
| ~ mustard_cole
| ~ salt_barry ),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(p223,plain,
( mustard_lang
| salt_lang
| ~ salt_cole
| ~ mustard_cole
| mustard_lang
| salt_mill ),
inference(resolution,[status(thm)],[p221,c54]) ).
cnf(p233,plain,
( salt_lang
| ~ salt_cole
| ~ mustard_cole
| mustard_lang
| salt_mill ),
inference(factoring,[status(thm)],[p223]) ).
cnf(f58,hypothesis,
( mustard_dix
| mustard_lang
| salt_lang ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c59) ).
fof(f58_nnf,plain,
( mustard_dix
| mustard_lang
| salt_lang ),
inference(nnf_transformation,[status(thm)],[f58]) ).
fof(f58_sk,plain,
( mustard_dix
| mustard_lang
| salt_lang ),
inference(skolemisation,[status(esa)],[f58_nnf]) ).
cnf(c58,plain,
( mustard_dix
| mustard_lang
| salt_lang ),
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
cnf(f30,hypothesis,
( salt_lang
| ~ mustard_dix
| salt_dix ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c31) ).
fof(f30_nnf,plain,
( salt_lang
| ~ mustard_dix
| salt_dix ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
( salt_lang
| ~ mustard_dix
| salt_dix ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( salt_lang
| ~ mustard_dix
| salt_dix ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p68,plain,
( salt_lang
| salt_dix
| mustard_lang
| salt_lang ),
inference(resolution,[status(thm)],[c58,c30]) ).
cnf(p95,plain,
( salt_dix
| mustard_lang
| salt_lang ),
inference(factoring,[status(thm)],[p68]) ).
cnf(f36,hypothesis,
( mustard_cole
| ~ mustard_dix
| ~ salt_dix ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c37) ).
fof(f36_nnf,plain,
( mustard_cole
| ~ mustard_dix
| ~ salt_dix ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
( mustard_cole
| ~ mustard_dix
| ~ salt_dix ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
( mustard_cole
| ~ mustard_dix
| ~ salt_dix ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p100,plain,
( mustard_cole
| ~ mustard_dix
| mustard_lang
| salt_lang ),
inference(resolution,[status(thm)],[p95,c36]) ).
cnf(p122,plain,
( mustard_lang
| salt_lang
| mustard_cole
| mustard_lang
| salt_lang ),
inference(resolution,[status(thm)],[p100,c58]) ).
cnf(p141,plain,
( mustard_lang
| mustard_cole
| mustard_lang
| salt_lang ),
inference(factoring,[status(thm)],[p122]) ).
cnf(p143,plain,
( mustard_cole
| mustard_lang
| salt_lang ),
inference(factoring,[status(thm)],[p141]) ).
cnf(p234,plain,
( mustard_lang
| salt_lang
| salt_lang
| ~ salt_cole
| mustard_lang
| salt_mill ),
inference(resolution,[status(thm)],[p233,p143]) ).
cnf(p248,plain,
( salt_lang
| salt_lang
| ~ salt_cole
| mustard_lang
| salt_mill ),
inference(factoring,[status(thm)],[p234]) ).
cnf(p253,plain,
( salt_lang
| ~ salt_cole
| mustard_lang
| salt_mill ),
inference(factoring,[status(thm)],[p248]) ).
cnf(f15,hypothesis,
( salt_cole
| ~ salt_barry
| ~ salt_dix ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c16) ).
fof(f15_nnf,plain,
( salt_cole
| ~ salt_barry
| ~ salt_dix ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
( salt_cole
| ~ salt_barry
| ~ salt_dix ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( salt_cole
| ~ salt_barry
| ~ salt_dix ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p99,plain,
( salt_cole
| ~ salt_barry
| mustard_lang
| salt_lang ),
inference(resolution,[status(thm)],[p95,c15]) ).
cnf(p224,plain,
( salt_cole
| mustard_lang
| salt_lang
| mustard_lang
| salt_mill ),
inference(resolution,[status(thm)],[p221,p99]) ).
cnf(p228,plain,
( salt_cole
| salt_lang
| mustard_lang
| salt_mill ),
inference(factoring,[status(thm)],[p224]) ).
cnf(p254,plain,
( salt_lang
| mustard_lang
| salt_mill
| salt_lang
| mustard_lang
| salt_mill ),
inference(resolution,[status(thm)],[p253,p228]) ).
cnf(p272,plain,
( salt_lang
| mustard_lang
| salt_lang
| mustard_lang
| salt_mill ),
inference(factoring,[status(thm)],[p254]) ).
cnf(p275,plain,
( salt_lang
| salt_lang
| mustard_lang
| salt_mill ),
inference(factoring,[status(thm)],[p272]) ).
cnf(p277,plain,
( salt_lang
| mustard_lang
| salt_mill ),
inference(factoring,[status(thm)],[p275]) ).
cnf(f46,hypothesis,
( ~ mustard_mill
| mustard_barry
| salt_barry
| ~ salt_cole ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c47) ).
fof(f46_nnf,plain,
( ~ mustard_mill
| mustard_barry
| salt_barry
| ~ salt_cole ),
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
( ~ mustard_mill
| mustard_barry
| salt_barry
| ~ salt_cole ),
inference(skolemisation,[status(esa)],[f46_nnf]) ).
cnf(c46,plain,
( ~ mustard_mill
| mustard_barry
| salt_barry
| ~ salt_cole ),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(p121,plain,
( ~ mustard_mill
| mustard_barry
| salt_barry
| salt_barry
| mustard_lang ),
inference(resolution,[status(thm)],[p120,c46]) ).
cnf(p139,plain,
( ~ mustard_mill
| mustard_barry
| salt_barry
| mustard_lang ),
inference(factoring,[status(thm)],[p121]) ).
cnf(p140,plain,
( mustard_lang
| salt_mill
| mustard_barry
| salt_barry
| mustard_lang ),
inference(resolution,[status(thm)],[p139,c55]) ).
cnf(p163,plain,
( salt_mill
| mustard_barry
| salt_barry
| mustard_lang ),
inference(factoring,[status(thm)],[p140]) ).
cnf(f61,hypothesis,
( mustard_barry
| mustard_dix
| salt_dix ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c62) ).
fof(f61_nnf,plain,
( mustard_barry
| mustard_dix
| salt_dix ),
inference(nnf_transformation,[status(thm)],[f61]) ).
fof(f61_sk,plain,
( mustard_barry
| mustard_dix
| salt_dix ),
inference(skolemisation,[status(esa)],[f61_nnf]) ).
cnf(c61,plain,
( mustard_barry
| mustard_dix
| salt_dix ),
inference(cnf_transformation,[status(esa)],[f61_sk]) ).
cnf(f14,hypothesis,
( mustard_cole
| ~ salt_barry
| ~ salt_dix ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c15) ).
fof(f14_nnf,plain,
( mustard_cole
| ~ salt_barry
| ~ salt_dix ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
( mustard_cole
| ~ salt_barry
| ~ salt_dix ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( mustard_cole
| ~ salt_barry
| ~ salt_dix ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p76,plain,
( mustard_cole
| ~ salt_barry
| mustard_barry
| mustard_dix ),
inference(resolution,[status(thm)],[c61,c14]) ).
cnf(p167,plain,
( mustard_cole
| mustard_barry
| mustard_dix
| salt_mill
| mustard_barry
| mustard_lang ),
inference(resolution,[status(thm)],[p163,p76]) ).
cnf(p182,plain,
( mustard_cole
| mustard_dix
| salt_mill
| mustard_barry
| mustard_lang ),
inference(factoring,[status(thm)],[p167]) ).
cnf(f10,hypothesis,
( ~ mustard_mill
| ~ salt_lang
| ~ mustard_dix ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c11) ).
fof(f10_nnf,plain,
( ~ mustard_mill
| ~ salt_lang
| ~ mustard_dix ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
( ~ mustard_mill
| ~ salt_lang
| ~ mustard_dix ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( ~ mustard_mill
| ~ salt_lang
| ~ mustard_dix ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p183,plain,
( ~ mustard_mill
| ~ salt_lang
| mustard_cole
| salt_mill
| mustard_barry
| mustard_lang ),
inference(resolution,[status(thm)],[p182,c10]) ).
cnf(f33,hypothesis,
( salt_lang
| mustard_barry
| ~ salt_barry ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c34) ).
fof(f33_nnf,plain,
( salt_lang
| mustard_barry
| ~ salt_barry ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
( salt_lang
| mustard_barry
| ~ salt_barry ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
( salt_lang
| mustard_barry
| ~ salt_barry ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p165,plain,
( salt_lang
| mustard_barry
| salt_mill
| mustard_barry
| mustard_lang ),
inference(resolution,[status(thm)],[p163,c33]) ).
cnf(p170,plain,
( salt_lang
| salt_mill
| mustard_barry
| mustard_lang ),
inference(factoring,[status(thm)],[p165]) ).
cnf(p192,plain,
( salt_mill
| mustard_barry
| mustard_lang
| ~ mustard_mill
| mustard_cole
| salt_mill
| mustard_barry
| mustard_lang ),
inference(resolution,[status(thm)],[p183,p170]) ).
cnf(p203,plain,
( salt_mill
| mustard_barry
| ~ mustard_mill
| mustard_cole
| salt_mill
| mustard_barry
| mustard_lang ),
inference(factoring,[status(thm)],[p192]) ).
cnf(p225,plain,
( salt_mill
| ~ mustard_mill
| mustard_cole
| salt_mill
| mustard_barry
| mustard_lang ),
inference(factoring,[status(thm)],[p203]) ).
cnf(p235,plain,
( ~ mustard_mill
| mustard_cole
| salt_mill
| mustard_barry
| mustard_lang ),
inference(factoring,[status(thm)],[p225]) ).
cnf(p236,plain,
( mustard_lang
| salt_mill
| mustard_cole
| salt_mill
| mustard_barry
| mustard_lang ),
inference(resolution,[status(thm)],[p235,c55]) ).
cnf(p256,plain,
( salt_mill
| mustard_cole
| salt_mill
| mustard_barry
| mustard_lang ),
inference(factoring,[status(thm)],[p236]) ).
cnf(p262,plain,
( mustard_cole
| salt_mill
| mustard_barry
| mustard_lang ),
inference(factoring,[status(thm)],[p256]) ).
cnf(p263,plain,
( mustard_lang
| mustard_dix
| salt_mill
| mustard_barry
| mustard_lang ),
inference(resolution,[status(thm)],[p262,c16]) ).
cnf(p266,plain,
( mustard_dix
| salt_mill
| mustard_barry
| mustard_lang ),
inference(factoring,[status(thm)],[p263]) ).
cnf(p269,plain,
( ~ mustard_mill
| ~ salt_lang
| salt_mill
| mustard_barry
| mustard_lang ),
inference(resolution,[status(thm)],[p266,c10]) ).
cnf(p278,plain,
( ~ mustard_mill
| salt_mill
| mustard_barry
| mustard_lang
| mustard_lang
| salt_mill ),
inference(resolution,[status(thm)],[p277,p269]) ).
cnf(p279,plain,
( ~ mustard_mill
| mustard_barry
| mustard_lang
| mustard_lang
| salt_mill ),
inference(factoring,[status(thm)],[p278]) ).
cnf(p283,plain,
( ~ mustard_mill
| mustard_barry
| mustard_lang
| salt_mill ),
inference(factoring,[status(thm)],[p279]) ).
cnf(p284,plain,
( mustard_lang
| salt_mill
| mustard_barry
| mustard_lang
| salt_mill ),
inference(resolution,[status(thm)],[p283,c55]) ).
cnf(p285,plain,
( mustard_lang
| mustard_barry
| mustard_lang
| salt_mill ),
inference(factoring,[status(thm)],[p284]) ).
cnf(p287,plain,
( mustard_barry
| mustard_lang
| salt_mill ),
inference(factoring,[status(thm)],[p285]) ).
cnf(f40,hypothesis,
( salt_barry
| ~ mustard_lang
| salt_lang ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c41) ).
fof(f40_nnf,plain,
( salt_barry
| ~ mustard_lang
| salt_lang ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
( salt_barry
| ~ mustard_lang
| salt_lang ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,plain,
( salt_barry
| ~ mustard_lang
| salt_lang ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p290,plain,
( salt_barry
| salt_lang
| mustard_barry
| salt_mill ),
inference(resolution,[status(thm)],[p287,c40]) ).
cnf(p292,plain,
( salt_lang
| mustard_barry
| salt_lang
| mustard_barry
| salt_mill ),
inference(resolution,[status(thm)],[p290,c33]) ).
cnf(p295,plain,
( salt_lang
| salt_lang
| mustard_barry
| salt_mill ),
inference(factoring,[status(thm)],[p292]) ).
cnf(p297,plain,
( salt_lang
| mustard_barry
| salt_mill ),
inference(factoring,[status(thm)],[p295]) ).
cnf(f28,hypothesis,
( salt_mill
| ~ mustard_lang
| ~ salt_lang ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c29) ).
fof(f28_nnf,plain,
( salt_mill
| ~ mustard_lang
| ~ salt_lang ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
( salt_mill
| ~ mustard_lang
| ~ salt_lang ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( salt_mill
| ~ mustard_lang
| ~ salt_lang ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(p298,plain,
( salt_mill
| ~ mustard_lang
| mustard_barry
| salt_mill ),
inference(resolution,[status(thm)],[p297,c28]) ).
cnf(p301,plain,
( ~ mustard_lang
| mustard_barry
| salt_mill ),
inference(factoring,[status(thm)],[p298]) ).
cnf(p303,plain,
( mustard_barry
| salt_mill
| mustard_barry
| salt_mill ),
inference(resolution,[status(thm)],[p301,p287]) ).
cnf(p304,plain,
( mustard_barry
| mustard_barry
| salt_mill ),
inference(factoring,[status(thm)],[p303]) ).
cnf(p306,plain,
( mustard_barry
| salt_mill ),
inference(factoring,[status(thm)],[p304]) ).
cnf(f32,hypothesis,
( salt_lang
| ~ mustard_barry
| salt_barry ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c33) ).
fof(f32_nnf,plain,
( salt_lang
| ~ mustard_barry
| salt_barry ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
( salt_lang
| ~ mustard_barry
| salt_barry ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c32,plain,
( salt_lang
| ~ mustard_barry
| salt_barry ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p311,plain,
( salt_lang
| salt_barry
| salt_mill ),
inference(resolution,[status(thm)],[p306,c32]) ).
cnf(f29,hypothesis,
( salt_mill
| ~ mustard_barry
| ~ salt_barry ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c30) ).
fof(f29_nnf,plain,
( salt_mill
| ~ mustard_barry
| ~ salt_barry ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
( salt_mill
| ~ mustard_barry
| ~ salt_barry ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( salt_mill
| ~ mustard_barry
| ~ salt_barry ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(p320,plain,
( salt_mill
| ~ mustard_barry
| salt_lang
| salt_mill ),
inference(resolution,[status(thm)],[p311,c29]) ).
cnf(p330,plain,
( ~ mustard_barry
| salt_lang
| salt_mill ),
inference(factoring,[status(thm)],[p320]) ).
cnf(p331,plain,
( salt_mill
| salt_lang
| salt_mill ),
inference(resolution,[status(thm)],[p330,p306]) ).
cnf(p332,plain,
( salt_lang
| salt_mill ),
inference(factoring,[status(thm)],[p331]) ).
cnf(p333,plain,
( salt_mill
| ~ mustard_lang
| salt_mill ),
inference(resolution,[status(thm)],[p332,c28]) ).
cnf(p335,plain,
( ~ mustard_lang
| salt_mill ),
inference(factoring,[status(thm)],[p333]) ).
cnf(p222,plain,
( salt_mill
| ~ mustard_barry
| mustard_lang
| salt_mill ),
inference(resolution,[status(thm)],[p221,c29]) ).
cnf(p227,plain,
( ~ mustard_barry
| mustard_lang
| salt_mill ),
inference(factoring,[status(thm)],[p222]) ).
cnf(p315,plain,
( mustard_lang
| salt_mill
| salt_mill ),
inference(resolution,[status(thm)],[p306,p227]) ).
cnf(p323,plain,
( mustard_lang
| salt_mill ),
inference(factoring,[status(thm)],[p315]) ).
cnf(p336,plain,
( salt_mill
| salt_mill ),
inference(resolution,[status(thm)],[p335,p323]) ).
cnf(p337,plain,
salt_mill,
inference(factoring,[status(thm)],[p336]) ).
cnf(f39,hypothesis,
( mustard_barry
| ~ mustard_mill
| ~ salt_mill ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c40) ).
fof(f39_nnf,plain,
( mustard_barry
| ~ mustard_mill
| ~ salt_mill ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
( mustard_barry
| ~ mustard_mill
| ~ salt_mill ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( mustard_barry
| ~ mustard_mill
| ~ salt_mill ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p342,plain,
( mustard_barry
| ~ mustard_mill ),
inference(resolution,[status(thm)],[p337,c39]) ).
cnf(f25,hypothesis,
( mustard_mill
| mustard_dix
| ~ salt_dix ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c26) ).
fof(f25_nnf,plain,
( mustard_mill
| mustard_dix
| ~ salt_dix ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
( mustard_mill
| mustard_dix
| ~ salt_dix ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
( mustard_mill
| mustard_dix
| ~ salt_dix ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p77,plain,
( mustard_mill
| mustard_dix
| mustard_barry
| mustard_dix ),
inference(resolution,[status(thm)],[c61,c25]) ).
cnf(p107,plain,
( mustard_mill
| mustard_barry
| mustard_dix ),
inference(factoring,[status(thm)],[p77]) ).
cnf(f24,hypothesis,
( mustard_mill
| ~ mustard_dix
| salt_dix ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c25) ).
fof(f24_nnf,plain,
( mustard_mill
| ~ mustard_dix
| salt_dix ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
( mustard_mill
| ~ mustard_dix
| salt_dix ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( mustard_mill
| ~ mustard_dix
| salt_dix ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p110,plain,
( mustard_mill
| salt_dix
| mustard_mill
| mustard_barry ),
inference(resolution,[status(thm)],[p107,c24]) ).
cnf(p124,plain,
( salt_dix
| mustard_mill
| mustard_barry ),
inference(factoring,[status(thm)],[p110]) ).
cnf(p126,plain,
( mustard_cole
| ~ mustard_dix
| mustard_mill
| mustard_barry ),
inference(resolution,[status(thm)],[p124,c36]) ).
cnf(p130,plain,
( mustard_mill
| mustard_barry
| mustard_cole
| mustard_mill
| mustard_barry ),
inference(resolution,[status(thm)],[p126,p107]) ).
cnf(p147,plain,
( mustard_mill
| mustard_cole
| mustard_mill
| mustard_barry ),
inference(factoring,[status(thm)],[p130]) ).
cnf(p150,plain,
( mustard_cole
| mustard_mill
| mustard_barry ),
inference(factoring,[status(thm)],[p147]) ).
cnf(p352,plain,
( mustard_cole
| mustard_barry
| mustard_barry ),
inference(resolution,[status(thm)],[p342,p150]) ).
cnf(p353,plain,
( mustard_cole
| mustard_barry ),
inference(factoring,[status(thm)],[p352]) ).
cnf(f0,hypothesis,
( mustard_lang
| mustard_barry
| ~ salt_mill ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c1) ).
fof(f0_nnf,plain,
( mustard_lang
| mustard_barry
| ~ salt_mill ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
( mustard_lang
| mustard_barry
| ~ salt_mill ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( mustard_lang
| mustard_barry
| ~ salt_mill ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p338,plain,
( mustard_lang
| mustard_barry ),
inference(resolution,[status(thm)],[p337,c0]) ).
cnf(f5,hypothesis,
( ~ salt_mill
| ~ mustard_cole
| ~ mustard_lang ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c6) ).
fof(f5_nnf,plain,
( ~ salt_mill
| ~ mustard_cole
| ~ mustard_lang ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
( ~ salt_mill
| ~ mustard_cole
| ~ mustard_lang ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( ~ salt_mill
| ~ mustard_cole
| ~ mustard_lang ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p343,plain,
( ~ salt_mill
| ~ mustard_cole
| mustard_barry ),
inference(resolution,[status(thm)],[p338,c5]) ).
cnf(p356,plain,
( ~ salt_mill
| mustard_barry
| mustard_barry ),
inference(resolution,[status(thm)],[p353,p343]) ).
cnf(p358,plain,
( ~ salt_mill
| mustard_barry ),
inference(factoring,[status(thm)],[p356]) ).
cnf(p359,plain,
mustard_barry,
inference(resolution,[status(thm)],[p358,p337]) ).
cnf(f45,hypothesis,
( ~ salt_mill
| ~ salt_barry
| ~ mustard_barry
| ~ salt_cole ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c46) ).
fof(f45_nnf,plain,
( ~ salt_mill
| ~ salt_barry
| ~ mustard_barry
| ~ salt_cole ),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
( ~ salt_mill
| ~ salt_barry
| ~ mustard_barry
| ~ salt_cole ),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c45,plain,
( ~ salt_mill
| ~ salt_barry
| ~ mustard_barry
| ~ salt_cole ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p79,plain,
( mustard_lang
| mustard_cole
| ~ salt_mill
| ~ salt_barry
| ~ mustard_barry ),
inference(resolution,[status(thm)],[c45,c56]) ).
cnf(p366,plain,
( mustard_lang
| mustard_cole
| ~ salt_mill
| ~ salt_barry ),
inference(resolution,[status(thm)],[p359,p79]) ).
cnf(f2,hypothesis,
( mustard_lang
| salt_barry
| ~ salt_mill ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c3) ).
fof(f2_nnf,plain,
( mustard_lang
| salt_barry
| ~ salt_mill ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
( mustard_lang
| salt_barry
| ~ salt_mill ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( mustard_lang
| salt_barry
| ~ salt_mill ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p340,plain,
( mustard_lang
| salt_barry ),
inference(resolution,[status(thm)],[p337,c2]) ).
cnf(p381,plain,
( mustard_lang
| mustard_lang
| mustard_cole
| ~ salt_mill ),
inference(resolution,[status(thm)],[p366,p340]) ).
cnf(p389,plain,
( mustard_lang
| mustard_cole
| ~ salt_mill ),
inference(factoring,[status(thm)],[p381]) ).
cnf(p390,plain,
( mustard_lang
| mustard_cole ),
inference(resolution,[status(thm)],[p389,p337]) ).
cnf(p348,plain,
( mustard_lang
| salt_lang
| ~ salt_cole
| ~ mustard_cole
| mustard_lang ),
inference(resolution,[status(thm)],[p340,c54]) ).
cnf(p368,plain,
( salt_lang
| ~ salt_cole
| ~ mustard_cole
| mustard_lang ),
inference(factoring,[status(thm)],[p348]) ).
cnf(p395,plain,
( salt_lang
| ~ salt_cole
| mustard_lang
| mustard_lang ),
inference(resolution,[status(thm)],[p390,p368]) ).
cnf(p412,plain,
( salt_lang
| ~ salt_cole
| mustard_lang ),
inference(factoring,[status(thm)],[p395]) ).
cnf(p393,plain,
( mustard_lang
| salt_dix
| mustard_lang ),
inference(resolution,[status(thm)],[p390,c18]) ).
cnf(p402,plain,
( salt_dix
| mustard_lang ),
inference(factoring,[status(thm)],[p393]) ).
cnf(f13,hypothesis,
( salt_cole
| ~ mustard_barry
| ~ salt_dix ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c14) ).
fof(f13_nnf,plain,
( salt_cole
| ~ mustard_barry
| ~ salt_dix ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
( salt_cole
| ~ mustard_barry
| ~ salt_dix ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( salt_cole
| ~ mustard_barry
| ~ salt_dix ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p403,plain,
( salt_cole
| ~ mustard_barry
| mustard_lang ),
inference(resolution,[status(thm)],[p402,c13]) ).
cnf(p407,plain,
( salt_cole
| mustard_lang ),
inference(resolution,[status(thm)],[p403,p359]) ).
cnf(p414,plain,
( mustard_lang
| salt_lang
| mustard_lang ),
inference(resolution,[status(thm)],[p412,p407]) ).
cnf(p415,plain,
( salt_lang
| mustard_lang ),
inference(factoring,[status(thm)],[p414]) ).
cnf(p392,plain,
( mustard_lang
| mustard_dix
| mustard_lang ),
inference(resolution,[status(thm)],[p390,c16]) ).
cnf(p396,plain,
( mustard_dix
| mustard_lang ),
inference(factoring,[status(thm)],[p392]) ).
cnf(p397,plain,
( ~ mustard_mill
| ~ salt_lang
| mustard_lang ),
inference(resolution,[status(thm)],[p396,c10]) ).
cnf(p417,plain,
( ~ mustard_mill
| mustard_lang
| mustard_lang ),
inference(resolution,[status(thm)],[p415,p397]) ).
cnf(p419,plain,
( ~ mustard_mill
| mustard_lang ),
inference(factoring,[status(thm)],[p417]) ).
cnf(f20,hypothesis,
( mustard_mill
| ~ mustard_dix
| ~ mustard_barry ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c21) ).
fof(f20_nnf,plain,
( mustard_mill
| ~ mustard_dix
| ~ mustard_barry ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
( mustard_mill
| ~ mustard_dix
| ~ mustard_barry ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( mustard_mill
| ~ mustard_dix
| ~ mustard_barry ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p361,plain,
( mustard_mill
| ~ mustard_dix ),
inference(resolution,[status(thm)],[p359,c20]) ).
cnf(p399,plain,
( mustard_mill
| mustard_lang ),
inference(resolution,[status(thm)],[p396,p361]) ).
cnf(p421,plain,
( mustard_lang
| mustard_lang ),
inference(resolution,[status(thm)],[p419,p399]) ).
cnf(p422,plain,
mustard_lang,
inference(factoring,[status(thm)],[p421]) ).
cnf(f62,negated_conjecture,
( mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_lang
| ~ salt_mill
| ~ salt_barry
| ~ mustard_barry
| salt_lang ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_who_takes_what) ).
fof(f62_nnf,plain,
( mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_lang
| ~ salt_mill
| ~ salt_barry
| ~ mustard_barry
| salt_lang ),
inference(nnf_transformation,[status(thm)],[f62]) ).
fof(f62_sk,plain,
( mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_lang
| ~ salt_mill
| ~ salt_barry
| ~ mustard_barry
| salt_lang ),
inference(skolemisation,[status(esa)],[f62_nnf]) ).
cnf(c62,plain,
( mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_lang
| ~ salt_mill
| ~ salt_barry
| ~ mustard_barry
| salt_lang ),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(p360,plain,
( mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_lang
| ~ salt_mill
| ~ salt_barry
| salt_lang ),
inference(resolution,[status(thm)],[p359,c62]) ).
cnf(f3,hypothesis,
( salt_lang
| salt_barry
| ~ salt_mill ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c4) ).
fof(f3_nnf,plain,
( salt_lang
| salt_barry
| ~ salt_mill ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
( salt_lang
| salt_barry
| ~ salt_mill ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( salt_lang
| salt_barry
| ~ salt_mill ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p341,plain,
( salt_lang
| salt_barry ),
inference(resolution,[status(thm)],[p337,c3]) ).
cnf(p369,plain,
( salt_lang
| mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_lang
| ~ salt_mill
| salt_lang ),
inference(resolution,[status(thm)],[p360,p341]) ).
cnf(p370,plain,
( mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_lang
| ~ salt_mill
| salt_lang ),
inference(factoring,[status(thm)],[p369]) ).
cnf(p371,plain,
( mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_lang
| salt_lang ),
inference(resolution,[status(thm)],[p370,p337]) ).
cnf(p427,plain,
( mustard_mill
| mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| salt_lang ),
inference(resolution,[status(thm)],[p422,p371]) ).
cnf(f22,hypothesis,
( mustard_mill
| ~ salt_dix
| ~ mustard_barry ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c23) ).
fof(f22_nnf,plain,
( mustard_mill
| ~ salt_dix
| ~ mustard_barry ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
( mustard_mill
| ~ salt_dix
| ~ mustard_barry ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( mustard_mill
| ~ salt_dix
| ~ mustard_barry ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(p362,plain,
( mustard_mill
| ~ salt_dix ),
inference(resolution,[status(thm)],[p359,c22]) ).
cnf(p433,plain,
( mustard_mill
| mustard_mill
| mustard_dix
| mustard_cole
| salt_cole
| salt_lang ),
inference(resolution,[status(thm)],[p427,p362]) ).
cnf(p435,plain,
( mustard_mill
| mustard_dix
| mustard_cole
| salt_cole
| salt_lang ),
inference(factoring,[status(thm)],[p433]) ).
cnf(p438,plain,
( mustard_mill
| mustard_mill
| mustard_cole
| salt_cole
| salt_lang ),
inference(resolution,[status(thm)],[p435,p361]) ).
cnf(p439,plain,
( mustard_mill
| mustard_cole
| salt_cole
| salt_lang ),
inference(factoring,[status(thm)],[p438]) ).
cnf(f27,hypothesis,
( mustard_mill
| mustard_cole
| ~ salt_cole ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c28) ).
fof(f27_nnf,plain,
( mustard_mill
| mustard_cole
| ~ salt_cole ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
( mustard_mill
| mustard_cole
| ~ salt_cole ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
( mustard_mill
| mustard_cole
| ~ salt_cole ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p440,plain,
( mustard_mill
| mustard_cole
| mustard_mill
| mustard_cole
| salt_lang ),
inference(resolution,[status(thm)],[p439,c27]) ).
cnf(p442,plain,
( mustard_mill
| mustard_mill
| mustard_cole
| salt_lang ),
inference(factoring,[status(thm)],[p440]) ).
cnf(p444,plain,
( mustard_mill
| mustard_cole
| salt_lang ),
inference(factoring,[status(thm)],[p442]) ).
cnf(f49,hypothesis,
( mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_mill ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c50) ).
fof(f49_nnf,plain,
( mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_mill ),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
( mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_mill ),
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c49,plain,
( mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| ~ mustard_mill ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(p445,plain,
( mustard_dix
| salt_dix
| mustard_cole
| salt_cole
| mustard_cole
| salt_lang ),
inference(resolution,[status(thm)],[p444,c49]) ).
cnf(p446,plain,
( mustard_dix
| salt_dix
| salt_cole
| mustard_cole
| salt_lang ),
inference(factoring,[status(thm)],[p445]) ).
cnf(f12,hypothesis,
( mustard_cole
| ~ mustard_barry
| ~ salt_dix ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c13) ).
fof(f12_nnf,plain,
( mustard_cole
| ~ mustard_barry
| ~ salt_dix ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
( mustard_cole
| ~ mustard_barry
| ~ salt_dix ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( mustard_cole
| ~ mustard_barry
| ~ salt_dix ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p448,plain,
( mustard_cole
| ~ mustard_barry
| mustard_dix
| salt_cole
| mustard_cole
| salt_lang ),
inference(resolution,[status(thm)],[p446,c12]) ).
cnf(p453,plain,
( ~ mustard_barry
| mustard_dix
| salt_cole
| mustard_cole
| salt_lang ),
inference(factoring,[status(thm)],[p448]) ).
cnf(p454,plain,
( mustard_dix
| salt_cole
| mustard_cole
| salt_lang ),
inference(resolution,[status(thm)],[p453,p359]) ).
cnf(f9,hypothesis,
( ~ salt_mill
| ~ mustard_lang
| ~ mustard_dix ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c10) ).
fof(f9_nnf,plain,
( ~ salt_mill
| ~ mustard_lang
| ~ mustard_dix ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
( ~ salt_mill
| ~ mustard_lang
| ~ mustard_dix ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( ~ salt_mill
| ~ mustard_lang
| ~ mustard_dix ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p456,plain,
( ~ salt_mill
| ~ mustard_lang
| salt_cole
| mustard_cole
| salt_lang ),
inference(resolution,[status(thm)],[p454,c9]) ).
cnf(p460,plain,
( ~ salt_mill
| salt_cole
| mustard_cole
| salt_lang ),
inference(resolution,[status(thm)],[p456,p422]) ).
cnf(p461,plain,
( salt_cole
| mustard_cole
| salt_lang ),
inference(resolution,[status(thm)],[p460,p337]) ).
cnf(f7,hypothesis,
( ~ salt_mill
| ~ salt_cole
| ~ mustard_lang ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c8) ).
fof(f7_nnf,plain,
( ~ salt_mill
| ~ salt_cole
| ~ mustard_lang ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
( ~ salt_mill
| ~ salt_cole
| ~ mustard_lang ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( ~ salt_mill
| ~ salt_cole
| ~ mustard_lang ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p426,plain,
( ~ salt_mill
| ~ salt_cole ),
inference(resolution,[status(thm)],[p422,c7]) ).
cnf(p463,plain,
( ~ salt_mill
| mustard_cole
| salt_lang ),
inference(resolution,[status(thm)],[p461,p426]) ).
cnf(p465,plain,
( mustard_cole
| salt_lang ),
inference(resolution,[status(thm)],[p463,p337]) ).
cnf(p424,plain,
( ~ salt_mill
| ~ mustard_cole ),
inference(resolution,[status(thm)],[p422,c5]) ).
cnf(p470,plain,
( ~ salt_mill
| salt_lang ),
inference(resolution,[status(thm)],[p465,p424]) ).
cnf(p472,plain,
salt_lang,
inference(resolution,[status(thm)],[p470,p337]) ).
cnf(f35,hypothesis,
( mustard_cole
| ~ mustard_lang
| ~ salt_lang ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c36) ).
fof(f35_nnf,plain,
( mustard_cole
| ~ mustard_lang
| ~ salt_lang ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
( mustard_cole
| ~ mustard_lang
| ~ salt_lang ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
( mustard_cole
| ~ mustard_lang
| ~ salt_lang ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p473,plain,
( mustard_cole
| ~ mustard_lang ),
inference(resolution,[status(thm)],[p472,c35]) ).
cnf(p476,plain,
mustard_cole,
inference(resolution,[status(thm)],[p473,p422]) ).
cnf(p480,plain,
~ salt_mill,
inference(resolution,[status(thm)],[p476,p424]) ).
cnf(p482,plain,
$false,
inference(resolution,[status(thm)],[p480,p337]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ030-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/5.39 % Computer : n016.cluster.edu
% 0.12/5.39 % Model : x86_64 x86_64
% 0.12/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.39 % Memory : 8046.5625MB
% 0.12/5.39 % OS : Linux 6.8.0-71-generic
% 0.12/5.39 % CPULimit : 300
% 0.12/5.39 % WCLimit : 300
% 0.12/5.39 % DateTime : Thu Sep 24 06:47:18 UTC 2026
% 0.12/5.39 % CPUTime :
% 0.12/5.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.25/6.58 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.25/6.58 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------