%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : PUZ030-2 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:02:42 PM UTC 2026
% Result : Unsatisfiable 0.58s 1.61s
% Output : CNFRefutation 0.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 63
% Syntax : Number of clauses : 549 ( 66 unt; 229 nHn; 549 RR)
% Number of literals : 1471 ( 0 equ; 738 neg)
% Maximal clause size : 10 ( 2 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)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_who_takes_what,negated_conjecture,
( salt_lang
| salt_cole
| mustard_cole
| salt_dix
| mustard_dix
| mustard_mill
| ~ mustard_barry
| ~ salt_barry
| ~ salt_mill
| ~ mustard_lang ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_who_takes_what) ).
cnf(c49,hypothesis,
( ~ mustard_mill
| ~ mustard_cole
| ~ salt_cole
| ~ mustard_dix
| ~ salt_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c49) ).
cnf(c54,hypothesis,
( ~ salt_barry
| ~ mustard_cole
| ~ salt_cole
| ~ mustard_lang
| ~ salt_lang ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c54) ).
cnf(c51,hypothesis,
( ~ salt_lang
| ~ mustard_barry
| ~ salt_barry
| ~ mustard_dix
| ~ salt_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c51) ).
cnf(c52,hypothesis,
( salt_dix
| mustard_dix
| ~ salt_lang
| ~ mustard_barry
| ~ salt_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c52) ).
cnf(c55,hypothesis,
( salt_lang
| mustard_lang
| ~ salt_barry
| ~ mustard_cole
| ~ salt_cole ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c55) ).
cnf(c53,hypothesis,
( salt_barry
| mustard_barry
| ~ salt_lang
| ~ mustard_dix
| ~ salt_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c53) ).
cnf(c45,hypothesis,
( ~ salt_cole
| ~ mustard_barry
| ~ salt_barry
| ~ mustard_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c45) ).
cnf(c46,hypothesis,
( ~ salt_cole
| ~ mustard_barry
| ~ salt_barry
| ~ salt_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c46) ).
cnf(c50,hypothesis,
( salt_cole
| mustard_cole
| salt_dix
| mustard_dix
| ~ mustard_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c50) ).
cnf(c47,hypothesis,
( salt_barry
| mustard_barry
| ~ salt_cole
| ~ mustard_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c47) ).
cnf(c48,hypothesis,
( salt_barry
| mustard_barry
| ~ salt_cole
| ~ salt_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c48) ).
cnf(c11,hypothesis,
( ~ mustard_dix
| ~ salt_lang
| ~ mustard_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c11) ).
cnf(c9,hypothesis,
( ~ mustard_dix
| ~ mustard_lang
| ~ mustard_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c9) ).
cnf(c7,hypothesis,
( ~ mustard_lang
| ~ salt_cole
| ~ mustard_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c7) ).
cnf(c5,hypothesis,
( ~ mustard_lang
| ~ mustard_cole
| ~ mustard_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c5) ).
cnf(c12,hypothesis,
( ~ mustard_dix
| ~ salt_lang
| ~ salt_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c12) ).
cnf(c10,hypothesis,
( ~ mustard_dix
| ~ mustard_lang
| ~ salt_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c10) ).
cnf(c8,hypothesis,
( ~ mustard_lang
| ~ salt_cole
| ~ salt_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c8) ).
cnf(c6,hypothesis,
( ~ mustard_lang
| ~ mustard_cole
| ~ salt_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c6) ).
cnf(c35,hypothesis,
( salt_dix
| ~ salt_cole
| ~ mustard_cole ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c35) ).
cnf(c16,hypothesis,
( salt_cole
| ~ salt_dix
| ~ salt_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c16) ).
cnf(c14,hypothesis,
( salt_cole
| ~ salt_dix
| ~ mustard_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c14) ).
cnf(c23,hypothesis,
( mustard_mill
| ~ mustard_barry
| ~ salt_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c23) ).
cnf(c21,hypothesis,
( mustard_mill
| ~ mustard_barry
| ~ mustard_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c21) ).
cnf(c37,hypothesis,
( mustard_cole
| ~ salt_dix
| ~ mustard_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c37) ).
cnf(c15,hypothesis,
( mustard_cole
| ~ salt_dix
| ~ salt_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c15) ).
cnf(c36,hypothesis,
( mustard_cole
| ~ salt_lang
| ~ mustard_lang ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c36) ).
cnf(c13,hypothesis,
( mustard_cole
| ~ salt_dix
| ~ mustard_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c13) ).
cnf(c40,hypothesis,
( mustard_barry
| ~ salt_mill
| ~ mustard_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c40) ).
cnf(c29,hypothesis,
( salt_mill
| ~ salt_lang
| ~ mustard_lang ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c29) ).
cnf(c24,hypothesis,
( salt_mill
| ~ mustard_barry
| ~ salt_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c24) ).
cnf(c22,hypothesis,
( salt_mill
| ~ mustard_barry
| ~ mustard_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c22) ).
cnf(c30,hypothesis,
( salt_mill
| ~ salt_barry
| ~ mustard_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c30) ).
cnf(c25,hypothesis,
( salt_dix
| mustard_mill
| ~ mustard_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c25) ).
cnf(c26,hypothesis,
( mustard_dix
| mustard_mill
| ~ salt_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c26) ).
cnf(c27,hypothesis,
( salt_cole
| mustard_mill
| ~ mustard_cole ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c27) ).
cnf(c28,hypothesis,
( mustard_cole
| mustard_mill
| ~ salt_cole ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c28) ).
cnf(c43,hypothesis,
( salt_cole
| salt_barry
| ~ mustard_cole ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c43) ).
cnf(c38,hypothesis,
( salt_barry
| salt_cole
| ~ mustard_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c38) ).
cnf(c44,hypothesis,
( mustard_cole
| salt_barry
| ~ salt_cole ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c44) ).
cnf(c31,hypothesis,
( salt_dix
| salt_lang
| ~ mustard_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c31) ).
cnf(c20,hypothesis,
( salt_dix
| salt_lang
| ~ mustard_cole ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c20) ).
cnf(c32,hypothesis,
( mustard_dix
| salt_lang
| ~ salt_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c32) ).
cnf(c18,hypothesis,
( mustard_dix
| salt_lang
| ~ mustard_cole ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c18) ).
cnf(c41,hypothesis,
( salt_lang
| salt_barry
| ~ mustard_lang ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c41) ).
cnf(c33,hypothesis,
( salt_barry
| salt_lang
| ~ mustard_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c33) ).
cnf(c4,hypothesis,
( salt_barry
| salt_lang
| ~ salt_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c4) ).
cnf(c19,hypothesis,
( salt_dix
| mustard_lang
| ~ mustard_cole ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c19) ).
cnf(c17,hypothesis,
( mustard_dix
| mustard_lang
| ~ mustard_cole ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c17) ).
cnf(c42,hypothesis,
( mustard_lang
| salt_barry
| ~ salt_lang ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c42) ).
cnf(c3,hypothesis,
( salt_barry
| mustard_lang
| ~ salt_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c3) ).
cnf(c39,hypothesis,
( mustard_barry
| salt_cole
| ~ salt_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c39) ).
cnf(c34,hypothesis,
( mustard_barry
| salt_lang
| ~ salt_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c34) ).
cnf(c2,hypothesis,
( mustard_barry
| salt_lang
| ~ salt_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c2) ).
cnf(c1,hypothesis,
( mustard_barry
| mustard_lang
| ~ salt_mill ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c1) ).
cnf(c57,hypothesis,
( salt_cole
| mustard_cole
| mustard_lang ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c57) ).
cnf(c59,hypothesis,
( salt_lang
| mustard_lang
| mustard_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c59) ).
cnf(c62,hypothesis,
( salt_dix
| mustard_dix
| mustard_barry ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c62) ).
cnf(c60,hypothesis,
( salt_barry
| mustard_barry
| salt_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c60) ).
cnf(c58,hypothesis,
( salt_mill
| mustard_mill
| mustard_dix ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c58) ).
cnf(c61,hypothesis,
( salt_mill
| mustard_mill
| salt_cole ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c61) ).
cnf(c56,hypothesis,
( salt_mill
| mustard_mill
| mustard_lang ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c56) ).
cnf(i_0_63,negated_conjecture,
( salt_lang
| salt_cole
| mustard_cole
| salt_dix
| mustard_dix
| mustard_mill
| ~ mustard_barry
| ~ salt_barry
| ~ salt_mill
| ~ mustard_lang ),
prove_who_takes_what,
[final] ).
cnf(i_0_64,hypothesis,
( ~ mustard_mill
| ~ mustard_cole
| ~ salt_cole
| ~ mustard_dix
| ~ salt_dix ),
c49,
[final] ).
cnf(i_0_65,hypothesis,
( ~ salt_barry
| ~ mustard_cole
| ~ salt_cole
| ~ mustard_lang
| ~ salt_lang ),
c54,
[final] ).
cnf(i_0_66,hypothesis,
( ~ salt_lang
| ~ mustard_barry
| ~ salt_barry
| ~ mustard_dix
| ~ salt_dix ),
c51,
[final] ).
cnf(i_0_67,hypothesis,
( salt_dix
| mustard_dix
| ~ salt_lang
| ~ mustard_barry
| ~ salt_barry ),
c52,
[final] ).
cnf(i_0_68,hypothesis,
( salt_lang
| mustard_lang
| ~ salt_barry
| ~ mustard_cole
| ~ salt_cole ),
c55,
[final] ).
cnf(i_0_69,hypothesis,
( salt_barry
| mustard_barry
| ~ salt_lang
| ~ mustard_dix
| ~ salt_dix ),
c53,
[final] ).
cnf(i_0_70,hypothesis,
( ~ salt_cole
| ~ mustard_barry
| ~ salt_barry
| ~ mustard_mill ),
c45,
[final] ).
cnf(i_0_71,hypothesis,
( ~ salt_cole
| ~ mustard_barry
| ~ salt_barry
| ~ salt_mill ),
c46,
[final] ).
cnf(i_0_72,hypothesis,
( salt_cole
| mustard_cole
| salt_dix
| mustard_dix
| ~ mustard_mill ),
c50,
[final] ).
cnf(i_0_73,hypothesis,
( salt_barry
| mustard_barry
| ~ salt_cole
| ~ mustard_mill ),
c47,
[final] ).
cnf(i_0_74,hypothesis,
( salt_barry
| mustard_barry
| ~ salt_cole
| ~ salt_mill ),
c48,
[final] ).
cnf(i_0_75,hypothesis,
( ~ mustard_dix
| ~ salt_lang
| ~ mustard_mill ),
c11,
[final] ).
cnf(i_0_76,hypothesis,
( ~ mustard_dix
| ~ mustard_lang
| ~ mustard_mill ),
c9,
[final] ).
cnf(i_0_77,hypothesis,
( ~ mustard_lang
| ~ salt_cole
| ~ mustard_mill ),
c7,
[final] ).
cnf(i_0_78,hypothesis,
( ~ mustard_lang
| ~ mustard_cole
| ~ mustard_mill ),
c5,
[final] ).
cnf(i_0_79,hypothesis,
( ~ mustard_dix
| ~ salt_lang
| ~ salt_mill ),
c12,
[final] ).
cnf(i_0_80,hypothesis,
( ~ mustard_dix
| ~ mustard_lang
| ~ salt_mill ),
c10,
[final] ).
cnf(i_0_81,hypothesis,
( ~ mustard_lang
| ~ salt_cole
| ~ salt_mill ),
c8,
[final] ).
cnf(i_0_82,hypothesis,
( ~ mustard_lang
| ~ mustard_cole
| ~ salt_mill ),
c6,
[final] ).
cnf(i_0_83,hypothesis,
( salt_dix
| ~ salt_cole
| ~ mustard_cole ),
c35,
[final] ).
cnf(i_0_84,hypothesis,
( salt_cole
| ~ salt_dix
| ~ salt_barry ),
c16,
[final] ).
cnf(i_0_85,hypothesis,
( salt_cole
| ~ salt_dix
| ~ mustard_barry ),
c14,
[final] ).
cnf(i_0_86,hypothesis,
( mustard_mill
| ~ mustard_barry
| ~ salt_dix ),
c23,
[final] ).
cnf(i_0_87,hypothesis,
( mustard_mill
| ~ mustard_barry
| ~ mustard_dix ),
c21,
[final] ).
cnf(i_0_88,hypothesis,
( mustard_cole
| ~ salt_dix
| ~ mustard_dix ),
c37,
[final] ).
cnf(i_0_89,hypothesis,
( mustard_cole
| ~ salt_dix
| ~ salt_barry ),
c15,
[final] ).
cnf(i_0_90,hypothesis,
( mustard_cole
| ~ salt_lang
| ~ mustard_lang ),
c36,
[final] ).
cnf(i_0_91,hypothesis,
( mustard_cole
| ~ salt_dix
| ~ mustard_barry ),
c13,
[final] ).
cnf(i_0_92,hypothesis,
( mustard_barry
| ~ salt_mill
| ~ mustard_mill ),
c40,
[final] ).
cnf(i_0_93,hypothesis,
( salt_mill
| ~ salt_lang
| ~ mustard_lang ),
c29,
[final] ).
cnf(i_0_94,hypothesis,
( salt_mill
| ~ mustard_barry
| ~ salt_dix ),
c24,
[final] ).
cnf(i_0_95,hypothesis,
( salt_mill
| ~ mustard_barry
| ~ mustard_dix ),
c22,
[final] ).
cnf(i_0_96,hypothesis,
( salt_mill
| ~ salt_barry
| ~ mustard_barry ),
c30,
[final] ).
cnf(i_0_97,hypothesis,
( salt_dix
| mustard_mill
| ~ mustard_dix ),
c25,
[final] ).
cnf(i_0_98,hypothesis,
( mustard_dix
| mustard_mill
| ~ salt_dix ),
c26,
[final] ).
cnf(i_0_99,hypothesis,
( salt_cole
| mustard_mill
| ~ mustard_cole ),
c27,
[final] ).
cnf(i_0_100,hypothesis,
( mustard_cole
| mustard_mill
| ~ salt_cole ),
c28,
[final] ).
cnf(i_0_101,hypothesis,
( salt_cole
| salt_barry
| ~ mustard_cole ),
c43,
[final] ).
cnf(i_0_102,hypothesis,
( salt_barry
| salt_cole
| ~ mustard_barry ),
c38,
[final] ).
cnf(i_0_103,hypothesis,
( mustard_cole
| salt_barry
| ~ salt_cole ),
c44,
[final] ).
cnf(i_0_104,hypothesis,
( salt_dix
| salt_lang
| ~ mustard_dix ),
c31,
[final] ).
cnf(i_0_105,hypothesis,
( salt_dix
| salt_lang
| ~ mustard_cole ),
c20,
[final] ).
cnf(i_0_106,hypothesis,
( mustard_dix
| salt_lang
| ~ salt_dix ),
c32,
[final] ).
cnf(i_0_107,hypothesis,
( mustard_dix
| salt_lang
| ~ mustard_cole ),
c18,
[final] ).
cnf(i_0_108,hypothesis,
( salt_lang
| salt_barry
| ~ mustard_lang ),
c41,
[final] ).
cnf(i_0_109,hypothesis,
( salt_barry
| salt_lang
| ~ mustard_barry ),
c33,
[final] ).
cnf(i_0_110,hypothesis,
( salt_barry
| salt_lang
| ~ salt_mill ),
c4,
[final] ).
cnf(i_0_111,hypothesis,
( salt_dix
| mustard_lang
| ~ mustard_cole ),
c19,
[final] ).
cnf(i_0_112,hypothesis,
( mustard_dix
| mustard_lang
| ~ mustard_cole ),
c17,
[final] ).
cnf(i_0_113,hypothesis,
( mustard_lang
| salt_barry
| ~ salt_lang ),
c42,
[final] ).
cnf(i_0_114,hypothesis,
( salt_barry
| mustard_lang
| ~ salt_mill ),
c3,
[final] ).
cnf(i_0_115,hypothesis,
( mustard_barry
| salt_cole
| ~ salt_barry ),
c39,
[final] ).
cnf(i_0_116,hypothesis,
( mustard_barry
| salt_lang
| ~ salt_barry ),
c34,
[final] ).
cnf(i_0_117,hypothesis,
( mustard_barry
| salt_lang
| ~ salt_mill ),
c2,
[final] ).
cnf(i_0_118,hypothesis,
( mustard_barry
| mustard_lang
| ~ salt_mill ),
c1,
[final] ).
cnf(i_0_119,hypothesis,
( salt_cole
| mustard_cole
| mustard_lang ),
c57,
[final] ).
cnf(i_0_120,hypothesis,
( salt_lang
| mustard_lang
| mustard_dix ),
c59,
[final] ).
cnf(i_0_121,hypothesis,
( salt_dix
| mustard_dix
| mustard_barry ),
c62,
[final] ).
cnf(i_0_122,hypothesis,
( salt_barry
| mustard_barry
| salt_dix ),
c60,
[final] ).
cnf(i_0_123,hypothesis,
( salt_mill
| mustard_mill
| mustard_dix ),
c58,
[final] ).
cnf(i_0_124,hypothesis,
( salt_mill
| mustard_mill
| salt_cole ),
c61,
[final] ).
cnf(i_0_125,hypothesis,
( salt_mill
| mustard_mill
| mustard_lang ),
c56,
[final] ).
cnf(i_0_126,plain,
( ~ mustard_mill
| salt_dix
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_78,i_0_111]) ).
cnf(i_0_127,plain,
( ~ mustard_dix
| ~ salt_lang
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_79,i_0_93]) ).
cnf(i_0_128,plain,
( ~ mustard_dix
| salt_barry
| ~ salt_mill ),
inference(scs_inference,[],[i_0_80,i_0_114]) ).
cnf(i_0_129,plain,
( ~ salt_cole
| mustard_barry
| ~ salt_mill ),
inference(scs_inference,[],[i_0_81,i_0_118]) ).
cnf(i_0_130,plain,
( ~ salt_mill
| salt_dix
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_82,i_0_111]) ).
cnf(i_0_131,plain,
( ~ salt_dix
| salt_cole
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_84,i_0_101]) ).
cnf(i_0_132,plain,
( ~ mustard_barry
| ~ mustard_dix
| ~ salt_lang ),
inference(scs_inference,[],[i_0_87,i_0_75]) ).
cnf(i_0_133,plain,
( ~ mustard_dix
| ~ salt_dix
| salt_cole ),
inference(scs_inference,[],[i_0_88,i_0_131]) ).
cnf(i_0_134,plain,
( ~ salt_dix
| mustard_cole
| ~ salt_cole ),
inference(scs_inference,[],[i_0_89,i_0_103]) ).
cnf(i_0_135,plain,
( ~ salt_lang
| ~ mustard_lang
| ~ mustard_mill ),
inference(scs_inference,[],[i_0_90,i_0_78]) ).
cnf(i_0_136,plain,
( ~ mustard_barry
| ~ mustard_dix
| salt_barry ),
inference(scs_inference,[],[i_0_95,i_0_128]) ).
cnf(i_0_137,plain,
( ~ salt_cole
| ~ mustard_barry
| ~ salt_barry ),
inference(scs_inference,[],[i_0_96,i_0_71]) ).
cnf(i_0_138,plain,
( ~ mustard_dix
| mustard_dix
| mustard_mill ),
inference(scs_inference,[],[i_0_97,i_0_98]) ).
cnf(i_0_139,plain,
( mustard_mill
| salt_dix
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_99,i_0_83]) ).
cnf(i_0_140,plain,
( ~ salt_cole
| mustard_mill
| salt_dix ),
inference(scs_inference,[],[i_0_100,i_0_139]) ).
cnf(i_0_141,plain,
( ~ mustard_barry
| mustard_barry
| salt_cole ),
inference(scs_inference,[],[i_0_102,i_0_115]) ).
cnf(i_0_142,plain,
( salt_lang
| mustard_cole
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_104,i_0_88]) ).
cnf(i_0_143,plain,
( salt_lang
| ~ mustard_cole
| salt_cole ),
inference(scs_inference,[],[i_0_105,i_0_131]) ).
cnf(i_0_144,plain,
( salt_lang
| ~ salt_dix
| salt_cole ),
inference(scs_inference,[],[i_0_106,i_0_133]) ).
cnf(i_0_145,plain,
( ~ mustard_cole
| salt_lang
| mustard_cole ),
inference(scs_inference,[],[i_0_107,i_0_142]) ).
cnf(i_0_146,plain,
( salt_barry
| mustard_cole
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_108,i_0_90]) ).
cnf(i_0_147,plain,
( ~ mustard_barry
| mustard_barry
| salt_lang ),
inference(scs_inference,[],[i_0_109,i_0_116]) ).
cnf(i_0_148,plain,
( salt_barry
| ~ salt_lang
| mustard_cole ),
inference(scs_inference,[],[i_0_113,i_0_90]) ).
cnf(i_0_149,plain,
( mustard_barry
| ~ mustard_dix
| ~ salt_mill ),
inference(scs_inference,[],[i_0_117,i_0_79]) ).
cnf(i_0_150,plain,
( mustard_lang
| mustard_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_119,i_0_100]) ).
cnf(i_0_151,plain,
( mustard_dix
| mustard_lang
| salt_barry ),
inference(scs_inference,[],[i_0_120,i_0_113]) ).
cnf(i_0_152,plain,
( mustard_barry
| mustard_dix
| mustard_mill ),
inference(scs_inference,[],[i_0_121,i_0_98]) ).
cnf(i_0_153,plain,
( salt_dix
| mustard_barry
| salt_cole ),
inference(scs_inference,[],[i_0_122,i_0_115]) ).
cnf(i_0_154,plain,
( salt_mill
| mustard_mill
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_123,i_0_87]) ).
cnf(i_0_155,plain,
( salt_mill
| mustard_mill
| salt_dix ),
inference(scs_inference,[],[i_0_124,i_0_140]) ).
cnf(i_0_156,plain,
( mustard_mill
| mustard_lang
| salt_barry ),
inference(scs_inference,[],[i_0_125,i_0_114]) ).
cnf(i_0_157,plain,
( ~ mustard_cole
| salt_dix
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_126,i_0_97]) ).
cnf(i_0_158,plain,
( ~ mustard_dix
| ~ salt_lang
| salt_barry ),
inference(scs_inference,[],[i_0_127,i_0_113]) ).
cnf(i_0_159,plain,
( ~ salt_mill
| salt_dix
| mustard_barry ),
inference(scs_inference,[],[i_0_129,i_0_153]) ).
cnf(i_0_160,plain,
( ~ salt_dix
| ~ salt_cole
| salt_dix ),
inference(scs_inference,[],[i_0_134,i_0_83]) ).
cnf(i_0_161,plain,
( ~ mustard_mill
| salt_barry
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_135,i_0_108]) ).
cnf(i_0_162,plain,
( ~ mustard_dix
| salt_barry
| salt_dix ),
inference(scs_inference,[],[i_0_136,i_0_122]) ).
cnf(i_0_163,plain,
( ~ salt_barry
| salt_barry
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_137,i_0_102]) ).
cnf(i_0_164,plain,
( salt_lang
| ~ salt_dix
| mustard_cole ),
inference(scs_inference,[],[i_0_144,i_0_134]) ).
cnf(i_0_165,plain,
( ~ mustard_lang
| mustard_cole
| ~ salt_dix ),
inference(scs_inference,[],[i_0_146,i_0_89]) ).
cnf(i_0_166,plain,
( ~ salt_lang
| mustard_cole
| ~ salt_dix ),
inference(scs_inference,[],[i_0_148,i_0_89]) ).
cnf(i_0_167,plain,
( ~ salt_mill
| ~ mustard_dix
| mustard_mill ),
inference(scs_inference,[],[i_0_149,i_0_87]) ).
cnf(i_0_168,plain,
( mustard_mill
| ~ salt_lang
| mustard_cole ),
inference(scs_inference,[],[i_0_150,i_0_90]) ).
cnf(i_0_169,plain,
( mustard_lang
| ~ mustard_barry
| salt_barry ),
inference(scs_inference,[],[i_0_151,i_0_136]) ).
cnf(i_0_170,plain,
( mustard_barry
| mustard_mill
| salt_dix ),
inference(scs_inference,[],[i_0_152,i_0_97]) ).
cnf(i_0_171,plain,
( salt_mill
| salt_dix
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_155,i_0_126]) ).
cnf(i_0_172,plain,
( mustard_lang
| salt_barry
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_156,i_0_161]) ).
cnf(i_0_173,plain,
( ~ mustard_cole
| mustard_cole
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_157,i_0_88]) ).
cnf(i_0_174,plain,
( mustard_barry
| salt_dix
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_159,i_0_171]) ).
cnf(i_0_175,plain,
( salt_dix
| mustard_lang
| salt_barry ),
inference(scs_inference,[],[i_0_162,i_0_151]) ).
cnf(i_0_176,plain,
( ~ salt_dix
| salt_barry
| mustard_cole ),
inference(scs_inference,[],[i_0_164,i_0_148]) ).
cnf(i_0_177,plain,
( ~ salt_dix
| salt_cole
| mustard_cole ),
inference(scs_inference,[],[i_0_165,i_0_119]) ).
cnf(i_0_178,plain,
( mustard_cole
| mustard_dix
| ~ salt_dix ),
inference(scs_inference,[],[i_0_166,i_0_106]) ).
cnf(i_0_179,plain,
( ~ mustard_dix
| mustard_mill
| salt_cole ),
inference(scs_inference,[],[i_0_167,i_0_124]) ).
cnf(i_0_180,plain,
( ~ salt_lang
| salt_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_168,i_0_99]) ).
cnf(i_0_181,plain,
( ~ mustard_barry
| salt_barry
| mustard_cole ),
inference(scs_inference,[],[i_0_169,i_0_146]) ).
cnf(i_0_182,plain,
( salt_dix
| mustard_mill
| ~ salt_dix ),
inference(scs_inference,[],[i_0_170,i_0_86]) ).
cnf(i_0_183,plain,
( mustard_barry
| ~ mustard_cole
| salt_cole ),
inference(scs_inference,[],[i_0_174,i_0_131]) ).
cnf(i_0_184,plain,
( mustard_lang
| salt_barry
| mustard_cole ),
inference(scs_inference,[],[i_0_175,i_0_176]) ).
cnf(i_0_185,plain,
( mustard_cole
| salt_cole
| mustard_barry ),
inference(scs_inference,[],[i_0_177,i_0_153]) ).
cnf(i_0_186,plain,
( ~ salt_dix
| mustard_dix
| mustard_lang ),
inference(scs_inference,[],[i_0_178,i_0_112]) ).
cnf(i_0_187,plain,
( salt_cole
| mustard_barry
| mustard_mill ),
inference(scs_inference,[],[i_0_179,i_0_152]) ).
cnf(i_0_188,plain,
( mustard_mill
| ~ salt_dix
| salt_cole ),
inference(scs_inference,[],[i_0_180,i_0_144]) ).
cnf(i_0_189,plain,
( mustard_cole
| salt_barry
| salt_dix ),
inference(scs_inference,[],[i_0_181,i_0_122]) ).
cnf(i_0_190,plain,
( salt_cole
| mustard_barry ),
inference(scs_inference,[],[i_0_183,i_0_185]) ).
cnf(i_0_191,plain,
( mustard_barry
| ~ mustard_lang
| ~ mustard_mill ),
inference(scs_inference,[],[i_0_190,i_0_77]) ).
cnf(i_0_192,plain,
( mustard_cole
| salt_lang
| salt_barry ),
inference(scs_inference,[],[i_0_184,i_0_108]) ).
cnf(i_0_193,plain,
( mustard_lang
| ~ salt_dix
| mustard_cole ),
inference(scs_inference,[],[i_0_186,i_0_88]) ).
cnf(i_0_194,plain,
( ~ salt_dix
| mustard_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_188,i_0_100]) ).
cnf(i_0_195,plain,
( salt_barry
| ~ salt_cole
| salt_dix ),
inference(scs_inference,[],[i_0_189,i_0_83]) ).
cnf(i_0_196,plain,
( salt_lang
| salt_barry
| salt_cole ),
inference(scs_inference,[],[i_0_192,i_0_101]) ).
cnf(i_0_197,plain,
( mustard_cole
| ~ salt_dix ),
inference(scs_inference,[],[i_0_193,i_0_165]) ).
cnf(i_0_198,plain,
( ~ salt_dix
| ~ mustard_lang
| ~ mustard_mill ),
inference(scs_inference,[],[i_0_197,i_0_78]) ).
cnf(i_0_199,plain,
( salt_dix
| ~ salt_cole
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_195,i_0_137]) ).
cnf(i_0_200,plain,
( salt_cole
| mustard_lang
| salt_barry ),
inference(scs_inference,[],[i_0_196,i_0_113]) ).
cnf(i_0_201,plain,
( ~ mustard_mill
| ~ salt_dix
| mustard_dix ),
inference(scs_inference,[],[i_0_198,i_0_186]) ).
cnf(i_0_202,plain,
( ~ salt_cole
| salt_cole
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_199,i_0_85]) ).
cnf(i_0_203,plain,
( salt_cole
| salt_barry
| mustard_cole ),
inference(scs_inference,[],[i_0_200,i_0_146]) ).
cnf(i_0_204,plain,
( ~ salt_dix
| mustard_dix ),
inference(scs_inference,[],[i_0_201,i_0_98]) ).
cnf(i_0_205,plain,
( mustard_dix
| ~ mustard_dix
| salt_barry ),
inference(scs_inference,[],[i_0_204,i_0_162]) ).
cnf(i_0_206,plain,
( salt_barry
| mustard_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_203,i_0_100]) ).
cnf(i_0_207,plain,
( salt_barry
| salt_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_206,i_0_99]) ).
cnf(i_0_208,plain,
( salt_barry
| mustard_mill
| salt_dix ),
inference(scs_inference,[],[i_0_207,i_0_140]) ).
cnf(i_0_209,plain,
( salt_barry
| salt_dix
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_208,i_0_126]) ).
cnf(i_0_210,plain,
( salt_barry
| ~ mustard_cole
| mustard_cole ),
inference(scs_inference,[],[i_0_209,i_0_197]) ).
cnf(i_0_211,plain,
( ~ salt_dix
| salt_cole ),
inference(scs_inference,[],[i_0_190,i_0_85]) ).
cnf(i_0_212,plain,
( salt_cole
| ~ mustard_dix
| salt_barry ),
inference(scs_inference,[],[i_0_211,i_0_162]) ).
cnf(i_0_213,plain,
( ~ mustard_dix
| salt_barry
| mustard_cole ),
inference(scs_inference,[],[i_0_212,i_0_103]) ).
cnf(i_0_214,plain,
( salt_cole
| salt_mill
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_190,i_0_95]) ).
cnf(i_0_215,plain,
( mustard_barry
| ~ mustard_lang
| ~ salt_mill ),
inference(scs_inference,[],[i_0_190,i_0_81]) ).
cnf(i_0_216,plain,
( mustard_barry
| ~ salt_mill
| salt_barry ),
inference(scs_inference,[],[i_0_215,i_0_114]) ).
cnf(i_0_217,plain,
( ~ salt_mill
| salt_cole
| salt_barry ),
inference(scs_inference,[],[i_0_216,i_0_102]) ).
cnf(i_0_218,plain,
( ~ salt_mill
| salt_barry
| mustard_cole ),
inference(scs_inference,[],[i_0_217,i_0_103]) ).
cnf(i_0_219,plain,
( salt_barry
| ~ mustard_lang
| ~ salt_mill ),
inference(scs_inference,[],[i_0_218,i_0_82]) ).
cnf(i_0_220,plain,
( ~ salt_mill
| ~ salt_lang
| salt_barry ),
inference(scs_inference,[],[i_0_219,i_0_113]) ).
cnf(i_0_221,plain,
( salt_barry
| ~ salt_lang
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_220,i_0_93]) ).
cnf(i_0_222,plain,
( ~ mustard_lang
| salt_barry ),
inference(scs_inference,[],[i_0_221,i_0_108]) ).
cnf(i_0_223,plain,
( salt_barry
| ~ mustard_cole
| mustard_dix ),
inference(scs_inference,[],[i_0_222,i_0_112]) ).
cnf(i_0_224,plain,
( ~ mustard_cole
| ~ salt_mill
| salt_barry ),
inference(scs_inference,[],[i_0_223,i_0_128]) ).
cnf(i_0_225,plain,
( ~ salt_mill
| ~ mustard_barry
| salt_barry ),
inference(scs_inference,[],[i_0_224,i_0_181]) ).
cnf(i_0_226,plain,
( salt_barry
| mustard_mill
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_225,i_0_154]) ).
cnf(i_0_227,plain,
( mustard_mill
| ~ salt_cole
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_226,i_0_137]) ).
cnf(i_0_228,plain,
( ~ mustard_barry
| ~ salt_cole
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_227,i_0_77]) ).
cnf(i_0_229,plain,
( ~ mustard_barry
| ~ mustard_lang
| ~ salt_dix ),
inference(scs_inference,[],[i_0_228,i_0_211]) ).
cnf(i_0_230,plain,
( ~ salt_dix
| ~ mustard_lang
| ~ salt_mill ),
inference(scs_inference,[],[i_0_229,i_0_215]) ).
cnf(i_0_231,plain,
( ~ salt_dix
| mustard_barry
| ~ salt_mill ),
inference(scs_inference,[],[i_0_230,i_0_118]) ).
cnf(i_0_232,plain,
( ~ salt_mill
| mustard_dix
| mustard_barry ),
inference(scs_inference,[],[i_0_231,i_0_121]) ).
cnf(i_0_233,plain,
( mustard_barry
| ~ salt_mill ),
inference(scs_inference,[],[i_0_232,i_0_149]) ).
cnf(i_0_234,plain,
( ~ salt_mill
| mustard_mill
| ~ salt_dix ),
inference(scs_inference,[],[i_0_233,i_0_86]) ).
cnf(i_0_235,plain,
( mustard_barry
| mustard_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_190,i_0_100]) ).
cnf(i_0_236,plain,
( mustard_cole
| salt_mill
| mustard_mill ),
inference(scs_inference,[],[i_0_235,i_0_154]) ).
cnf(i_0_237,plain,
( salt_cole
| salt_mill
| ~ salt_barry ),
inference(scs_inference,[],[i_0_190,i_0_96]) ).
cnf(i_0_238,plain,
( salt_cole
| salt_mill
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_237,i_0_222]) ).
cnf(i_0_239,plain,
( salt_mill
| ~ mustard_barry
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_238,i_0_228]) ).
cnf(i_0_240,plain,
( ~ mustard_barry
| ~ mustard_dix
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_239,i_0_80]) ).
cnf(i_0_241,plain,
( salt_cole
| salt_barry ),
inference(scs_inference,[],[i_0_190,i_0_102]) ).
cnf(i_0_242,plain,
( salt_barry
| mustard_cole ),
inference(scs_inference,[],[i_0_241,i_0_103]) ).
cnf(i_0_243,plain,
( mustard_cole
| ~ mustard_barry
| salt_mill ),
inference(scs_inference,[],[i_0_242,i_0_96]) ).
cnf(i_0_244,plain,
( ~ mustard_barry
| salt_mill
| salt_dix ),
inference(scs_inference,[],[i_0_243,i_0_171]) ).
cnf(i_0_245,plain,
( salt_mill
| salt_dix
| mustard_dix ),
inference(scs_inference,[],[i_0_244,i_0_121]) ).
cnf(i_0_246,plain,
( mustard_dix
| salt_dix
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_245,i_0_130]) ).
cnf(i_0_247,plain,
( ~ mustard_cole
| salt_dix ),
inference(scs_inference,[],[i_0_246,i_0_157]) ).
cnf(i_0_248,plain,
( salt_dix
| ~ salt_dix ),
inference(scs_inference,[],[i_0_247,i_0_197]) ).
cnf(i_0_249,plain,
( mustard_barry
| ~ salt_barry
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_190,i_0_137]) ).
cnf(i_0_250,plain,
( mustard_barry
| salt_dix
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_190,i_0_199]) ).
cnf(i_0_251,plain,
( salt_cole
| ~ mustard_dix
| ~ salt_lang ),
inference(scs_inference,[],[i_0_190,i_0_132]) ).
cnf(i_0_252,plain,
( salt_cole
| ~ salt_barry
| ~ salt_cole ),
inference(scs_inference,[],[i_0_190,i_0_137]) ).
cnf(i_0_253,plain,
( mustard_barry
| mustard_mill
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_190,i_0_227]) ).
cnf(i_0_254,plain,
( mustard_barry
| ~ mustard_barry
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_190,i_0_228]) ).
cnf(i_0_255,plain,
( salt_cole
| ~ salt_cole
| salt_dix ),
inference(scs_inference,[],[i_0_190,i_0_199]) ).
cnf(i_0_256,plain,
( salt_cole
| ~ salt_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_190,i_0_227]) ).
cnf(i_0_257,plain,
( salt_barry
| mustard_barry
| ~ mustard_mill ),
inference(scs_inference,[],[i_0_190,i_0_73]) ).
cnf(i_0_258,plain,
( ~ mustard_mill
| mustard_barry
| salt_lang ),
inference(scs_inference,[],[i_0_257,i_0_116]) ).
cnf(i_0_259,plain,
( salt_lang
| mustard_dix
| mustard_barry ),
inference(scs_inference,[],[i_0_258,i_0_152]) ).
cnf(i_0_260,plain,
( mustard_barry
| salt_dix
| salt_lang ),
inference(scs_inference,[],[i_0_259,i_0_104]) ).
cnf(i_0_261,plain,
( salt_dix
| salt_barry
| salt_lang ),
inference(scs_inference,[],[i_0_260,i_0_109]) ).
cnf(i_0_262,plain,
( salt_barry
| salt_lang
| mustard_dix ),
inference(scs_inference,[],[i_0_261,i_0_204]) ).
cnf(i_0_263,plain,
( mustard_dix
| ~ salt_mill
| salt_barry ),
inference(scs_inference,[],[i_0_262,i_0_220]) ).
cnf(i_0_264,plain,
( ~ salt_mill
| salt_barry ),
inference(scs_inference,[],[i_0_263,i_0_128]) ).
cnf(i_0_265,plain,
( salt_barry
| ~ mustard_barry
| ~ salt_dix ),
inference(scs_inference,[],[i_0_264,i_0_94]) ).
cnf(i_0_266,plain,
( ~ salt_dix
| ~ salt_cole
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_265,i_0_137]) ).
cnf(i_0_267,plain,
( ~ mustard_barry
| salt_barry
| ~ salt_cole ),
inference(scs_inference,[],[i_0_266,i_0_195]) ).
cnf(i_0_268,plain,
( ~ salt_cole
| salt_barry
| ~ mustard_mill ),
inference(scs_inference,[],[i_0_267,i_0_257]) ).
cnf(i_0_269,plain,
( salt_barry
| ~ mustard_mill
| ~ salt_dix ),
inference(scs_inference,[],[i_0_268,i_0_211]) ).
cnf(i_0_270,plain,
( mustard_barry
| ~ salt_dix
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_190,i_0_266]) ).
cnf(i_0_271,plain,
( mustard_barry
| ~ mustard_barry
| salt_barry ),
inference(scs_inference,[],[i_0_190,i_0_267]) ).
cnf(i_0_272,plain,
( mustard_cole
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_197,i_0_247]) ).
cnf(i_0_273,plain,
( mustard_cole
| mustard_mill
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_197,i_0_97]) ).
cnf(i_0_274,plain,
( mustard_cole
| mustard_barry
| mustard_dix ),
inference(scs_inference,[],[i_0_197,i_0_121]) ).
cnf(i_0_275,plain,
( mustard_barry
| salt_barry
| mustard_dix ),
inference(scs_inference,[],[i_0_274,i_0_223]) ).
cnf(i_0_276,plain,
( mustard_dix
| salt_barry
| mustard_mill ),
inference(scs_inference,[],[i_0_275,i_0_226]) ).
cnf(i_0_277,plain,
( mustard_mill
| ~ salt_lang
| salt_barry ),
inference(scs_inference,[],[i_0_276,i_0_158]) ).
cnf(i_0_278,plain,
( ~ salt_lang
| mustard_barry
| salt_barry ),
inference(scs_inference,[],[i_0_277,i_0_257]) ).
cnf(i_0_279,plain,
( mustard_cole
| ~ salt_cole
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_197,i_0_199]) ).
cnf(i_0_280,plain,
( mustard_cole
| ~ mustard_barry
| mustard_barry ),
inference(scs_inference,[],[i_0_279,i_0_190]) ).
cnf(i_0_281,plain,
( mustard_cole
| salt_mill
| mustard_dix ),
inference(scs_inference,[],[i_0_197,i_0_245]) ).
cnf(i_0_282,plain,
( salt_mill
| mustard_dix
| salt_lang ),
inference(scs_inference,[],[i_0_281,i_0_107]) ).
cnf(i_0_283,plain,
( salt_lang
| ~ mustard_barry
| salt_mill ),
inference(scs_inference,[],[i_0_282,i_0_95]) ).
cnf(i_0_284,plain,
( salt_lang
| salt_mill
| salt_cole ),
inference(scs_inference,[],[i_0_283,i_0_190]) ).
cnf(i_0_285,plain,
( mustard_cole
| mustard_barry
| salt_lang ),
inference(scs_inference,[],[i_0_197,i_0_260]) ).
cnf(i_0_286,plain,
( mustard_barry
| ~ mustard_lang
| mustard_cole ),
inference(scs_inference,[],[i_0_285,i_0_90]) ).
cnf(i_0_287,plain,
( mustard_cole
| ~ salt_cole
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_286,i_0_228]) ).
cnf(i_0_288,plain,
( ~ mustard_lang
| ~ salt_cole
| salt_dix ),
inference(scs_inference,[],[i_0_287,i_0_247]) ).
cnf(i_0_289,plain,
( ~ mustard_lang
| salt_dix
| mustard_barry ),
inference(scs_inference,[],[i_0_288,i_0_190]) ).
cnf(i_0_290,plain,
( ~ salt_dix
| ~ mustard_mill
| ~ salt_lang ),
inference(scs_inference,[],[i_0_204,i_0_75]) ).
cnf(i_0_291,plain,
( ~ salt_lang
| ~ mustard_mill
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_290,i_0_247]) ).
cnf(i_0_292,plain,
( ~ mustard_mill
| ~ mustard_cole
| mustard_dix ),
inference(scs_inference,[],[i_0_291,i_0_107]) ).
cnf(i_0_293,plain,
( mustard_dix
| ~ mustard_cole
| salt_cole ),
inference(scs_inference,[],[i_0_292,i_0_99]) ).
cnf(i_0_294,plain,
( ~ mustard_cole
| salt_cole
| ~ salt_lang ),
inference(scs_inference,[],[i_0_293,i_0_251]) ).
cnf(i_0_295,plain,
( ~ salt_lang
| mustard_lang
| salt_cole ),
inference(scs_inference,[],[i_0_294,i_0_119]) ).
cnf(i_0_296,plain,
( salt_cole
| mustard_lang
| mustard_dix ),
inference(scs_inference,[],[i_0_295,i_0_120]) ).
cnf(i_0_297,plain,
( mustard_dix
| salt_cole
| salt_mill ),
inference(scs_inference,[],[i_0_296,i_0_238]) ).
cnf(i_0_298,plain,
( salt_cole
| ~ mustard_barry
| salt_mill ),
inference(scs_inference,[],[i_0_297,i_0_95]) ).
cnf(i_0_299,plain,
( salt_mill
| salt_cole ),
inference(scs_inference,[],[i_0_298,i_0_190]) ).
cnf(i_0_300,plain,
( salt_cole
| ~ mustard_dix
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_299,i_0_80]) ).
cnf(i_0_301,plain,
( ~ mustard_dix
| mustard_cole
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_300,i_0_287]) ).
cnf(i_0_302,plain,
( ~ mustard_lang
| mustard_cole
| salt_mill ),
inference(scs_inference,[],[i_0_301,i_0_281]) ).
cnf(i_0_303,plain,
( ~ salt_dix
| ~ salt_lang
| ~ salt_mill ),
inference(scs_inference,[],[i_0_204,i_0_79]) ).
cnf(i_0_304,plain,
( ~ salt_lang
| ~ salt_mill
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_303,i_0_247]) ).
cnf(i_0_305,plain,
( ~ salt_mill
| ~ mustard_cole
| mustard_dix ),
inference(scs_inference,[],[i_0_304,i_0_107]) ).
cnf(i_0_306,plain,
( ~ mustard_cole
| mustard_mill
| mustard_dix ),
inference(scs_inference,[],[i_0_305,i_0_123]) ).
cnf(i_0_307,plain,
( mustard_dix
| ~ salt_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_306,i_0_100]) ).
cnf(i_0_308,plain,
( ~ salt_cole
| ~ salt_mill
| mustard_mill ),
inference(scs_inference,[],[i_0_307,i_0_167]) ).
cnf(i_0_309,plain,
( ~ salt_mill
| ~ salt_lang
| mustard_mill ),
inference(scs_inference,[],[i_0_308,i_0_180]) ).
cnf(i_0_310,plain,
( ~ salt_lang
| mustard_mill
| mustard_lang ),
inference(scs_inference,[],[i_0_309,i_0_125]) ).
cnf(i_0_311,plain,
( mustard_mill
| mustard_lang
| mustard_dix ),
inference(scs_inference,[],[i_0_310,i_0_120]) ).
cnf(i_0_312,plain,
( mustard_lang
| ~ mustard_barry
| mustard_mill ),
inference(scs_inference,[],[i_0_311,i_0_87]) ).
cnf(i_0_313,plain,
( mustard_dix
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_204,i_0_247]) ).
cnf(i_0_314,plain,
( ~ mustard_cole
| ~ mustard_barry
| mustard_mill ),
inference(scs_inference,[],[i_0_313,i_0_87]) ).
cnf(i_0_315,plain,
( mustard_dix
| ~ mustard_dix
| salt_lang ),
inference(scs_inference,[],[i_0_204,i_0_104]) ).
cnf(i_0_316,plain,
( ~ salt_dix
| ~ salt_lang
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_204,i_0_127]) ).
cnf(i_0_317,plain,
( ~ salt_lang
| ~ mustard_lang
| ~ salt_cole ),
inference(scs_inference,[],[i_0_316,i_0_288]) ).
cnf(i_0_318,plain,
( ~ salt_cole
| ~ salt_lang
| salt_cole ),
inference(scs_inference,[],[i_0_317,i_0_295]) ).
cnf(i_0_319,plain,
( ~ salt_dix
| ~ mustard_barry
| ~ salt_lang ),
inference(scs_inference,[],[i_0_204,i_0_132]) ).
cnf(i_0_320,plain,
( ~ salt_lang
| ~ salt_cole
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_319,i_0_199]) ).
cnf(i_0_321,plain,
( ~ salt_cole
| ~ mustard_barry
| salt_mill ),
inference(scs_inference,[],[i_0_320,i_0_283]) ).
cnf(i_0_322,plain,
( salt_mill
| ~ mustard_barry
| mustard_barry ),
inference(scs_inference,[],[i_0_321,i_0_190]) ).
cnf(i_0_323,plain,
( ~ mustard_barry
| mustard_barry ),
inference(scs_inference,[],[i_0_322,i_0_233]) ).
cnf(i_0_324,plain,
( mustard_barry
| mustard_dix ),
inference(scs_inference,[],[i_0_204,i_0_121]) ).
cnf(i_0_325,plain,
( mustard_dix
| ~ mustard_dix
| salt_mill ),
inference(scs_inference,[],[i_0_324,i_0_95]) ).
cnf(i_0_326,plain,
( mustard_dix
| salt_barry
| ~ salt_cole ),
inference(scs_inference,[],[i_0_204,i_0_195]) ).
cnf(i_0_327,plain,
( ~ salt_cole
| ~ salt_lang
| salt_barry ),
inference(scs_inference,[],[i_0_326,i_0_158]) ).
cnf(i_0_328,plain,
( salt_barry
| ~ mustard_cole
| ~ salt_lang ),
inference(scs_inference,[],[i_0_327,i_0_294]) ).
cnf(i_0_329,plain,
( ~ salt_lang
| salt_barry ),
inference(scs_inference,[],[i_0_328,i_0_242]) ).
cnf(i_0_330,plain,
( ~ mustard_barry
| salt_barry ),
inference(scs_inference,[],[i_0_329,i_0_109]) ).
cnf(i_0_331,plain,
( salt_barry
| mustard_dix ),
inference(scs_inference,[],[i_0_330,i_0_324]) ).
cnf(i_0_332,plain,
( mustard_dix
| ~ mustard_barry
| salt_mill ),
inference(scs_inference,[],[i_0_331,i_0_96]) ).
cnf(i_0_333,plain,
( salt_mill
| ~ mustard_barry
| ~ salt_lang ),
inference(scs_inference,[],[i_0_332,i_0_132]) ).
cnf(i_0_334,plain,
( ~ mustard_barry
| ~ salt_lang
| mustard_mill ),
inference(scs_inference,[],[i_0_333,i_0_309]) ).
cnf(i_0_335,plain,
( ~ salt_lang
| mustard_mill
| salt_dix ),
inference(scs_inference,[],[i_0_334,i_0_170]) ).
cnf(i_0_336,plain,
( salt_dix
| ~ salt_lang
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_335,i_0_135]) ).
cnf(i_0_337,plain,
( ~ mustard_lang
| ~ salt_lang
| ~ salt_mill ),
inference(scs_inference,[],[i_0_336,i_0_303]) ).
cnf(i_0_338,plain,
( ~ salt_mill
| ~ salt_lang
| salt_cole ),
inference(scs_inference,[],[i_0_337,i_0_295]) ).
cnf(i_0_339,plain,
( salt_cole
| ~ mustard_barry
| ~ salt_lang ),
inference(scs_inference,[],[i_0_338,i_0_333]) ).
cnf(i_0_340,plain,
( ~ salt_lang
| ~ salt_barry
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_339,i_0_137]) ).
cnf(i_0_341,plain,
( ~ salt_lang
| ~ mustard_barry
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_340,i_0_222]) ).
cnf(i_0_342,plain,
( mustard_dix
| ~ salt_cole
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_204,i_0_199]) ).
cnf(i_0_343,plain,
( ~ mustard_barry
| mustard_lang
| mustard_dix ),
inference(scs_inference,[],[i_0_342,i_0_296]) ).
cnf(i_0_344,plain,
( mustard_lang
| mustard_dix
| ~ salt_mill ),
inference(scs_inference,[],[i_0_343,i_0_233]) ).
cnf(i_0_345,plain,
( mustard_dix
| ~ salt_mill
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_344,i_0_80]) ).
cnf(i_0_346,plain,
( mustard_dix
| ~ mustard_lang
| ~ salt_cole ),
inference(scs_inference,[],[i_0_204,i_0_288]) ).
cnf(i_0_347,plain,
( ~ salt_cole
| salt_cole
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_346,i_0_300]) ).
cnf(i_0_348,plain,
( mustard_dix
| ~ salt_lang
| mustard_mill ),
inference(scs_inference,[],[i_0_204,i_0_335]) ).
cnf(i_0_349,plain,
( mustard_mill
| ~ salt_lang
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_348,i_0_127]) ).
cnf(i_0_350,plain,
( ~ mustard_lang
| ~ salt_lang
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_349,i_0_291]) ).
cnf(i_0_351,plain,
( ~ mustard_cole
| ~ salt_lang
| mustard_mill ),
inference(scs_inference,[],[i_0_350,i_0_310]) ).
cnf(i_0_352,plain,
( ~ salt_lang
| mustard_mill
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_351,i_0_273]) ).
cnf(i_0_353,plain,
( ~ mustard_dix
| ~ salt_dix
| ~ salt_lang ),
inference(scs_inference,[],[i_0_352,i_0_290]) ).
cnf(i_0_354,plain,
( ~ salt_dix
| ~ salt_lang
| mustard_mill ),
inference(scs_inference,[],[i_0_353,i_0_348]) ).
cnf(i_0_355,plain,
( ~ salt_lang
| ~ salt_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_354,i_0_140]) ).
cnf(i_0_356,plain,
( ~ salt_cole
| ~ salt_dix
| ~ salt_lang ),
inference(scs_inference,[],[i_0_355,i_0_290]) ).
cnf(i_0_357,plain,
( ~ salt_dix
| ~ salt_lang ),
inference(scs_inference,[],[i_0_204,i_0_353]) ).
cnf(i_0_358,plain,
( ~ salt_lang
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_357,i_0_247]) ).
cnf(i_0_359,plain,
( ~ mustard_cole
| ~ salt_barry
| mustard_barry ),
inference(scs_inference,[],[i_0_358,i_0_116]) ).
cnf(i_0_360,plain,
( ~ salt_barry
| mustard_barry
| mustard_mill ),
inference(scs_inference,[],[i_0_359,i_0_235]) ).
cnf(i_0_361,plain,
( mustard_mill
| mustard_barry
| ~ mustard_mill ),
inference(scs_inference,[],[i_0_360,i_0_257]) ).
cnf(i_0_362,plain,
( mustard_dix
| ~ salt_lang
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_204,i_0_336]) ).
cnf(i_0_363,plain,
( ~ salt_lang
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_362,i_0_127]) ).
cnf(i_0_364,plain,
( ~ mustard_lang
| ~ mustard_dix
| salt_dix ),
inference(scs_inference,[],[i_0_363,i_0_104]) ).
cnf(i_0_365,plain,
( mustard_dix
| ~ mustard_lang
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_204,i_0_364]) ).
cnf(i_0_366,plain,
( salt_cole
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_211,i_0_247]) ).
cnf(i_0_367,plain,
( ~ mustard_cole
| ~ mustard_barry
| salt_mill ),
inference(scs_inference,[],[i_0_366,i_0_321]) ).
cnf(i_0_368,plain,
( salt_mill
| ~ mustard_cole
| ~ salt_barry ),
inference(scs_inference,[],[i_0_367,i_0_359]) ).
cnf(i_0_369,plain,
( ~ salt_barry
| ~ mustard_cole
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_368,i_0_82]) ).
cnf(i_0_370,plain,
( ~ mustard_cole
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_369,i_0_222]) ).
cnf(i_0_371,plain,
( ~ mustard_lang
| ~ salt_dix ),
inference(scs_inference,[],[i_0_370,i_0_197]) ).
cnf(i_0_372,plain,
( ~ salt_dix
| salt_mill
| mustard_mill ),
inference(scs_inference,[],[i_0_371,i_0_125]) ).
cnf(i_0_373,plain,
( salt_mill
| ~ salt_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_372,i_0_140]) ).
cnf(i_0_374,plain,
( mustard_mill
| ~ salt_cole
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_373,i_0_81]) ).
cnf(i_0_375,plain,
( ~ salt_cole
| ~ mustard_dix
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_374,i_0_76]) ).
cnf(i_0_376,plain,
( ~ mustard_lang
| ~ mustard_dix
| mustard_mill ),
inference(scs_inference,[],[i_0_375,i_0_179]) ).
cnf(i_0_377,plain,
( ~ mustard_dix
| salt_mill
| mustard_mill ),
inference(scs_inference,[],[i_0_376,i_0_125]) ).
cnf(i_0_378,plain,
( salt_mill
| mustard_mill ),
inference(scs_inference,[],[i_0_377,i_0_123]) ).
cnf(i_0_379,plain,
( mustard_mill
| mustard_barry ),
inference(scs_inference,[],[i_0_378,i_0_233]) ).
cnf(i_0_380,plain,
( mustard_barry
| ~ mustard_dix
| ~ salt_lang ),
inference(scs_inference,[],[i_0_379,i_0_75]) ).
cnf(i_0_381,plain,
( ~ salt_lang
| ~ mustard_dix
| salt_mill ),
inference(scs_inference,[],[i_0_380,i_0_95]) ).
cnf(i_0_382,plain,
( salt_mill
| ~ mustard_dix
| mustard_cole ),
inference(scs_inference,[],[i_0_381,i_0_142]) ).
cnf(i_0_383,plain,
( ~ mustard_dix
| mustard_cole
| mustard_barry ),
inference(scs_inference,[],[i_0_382,i_0_233]) ).
cnf(i_0_384,plain,
( mustard_barry
| mustard_cole
| salt_mill ),
inference(scs_inference,[],[i_0_383,i_0_281]) ).
cnf(i_0_385,plain,
( mustard_cole
| salt_mill ),
inference(scs_inference,[],[i_0_384,i_0_243]) ).
cnf(i_0_386,plain,
( salt_mill
| mustard_dix ),
inference(scs_inference,[],[i_0_385,i_0_313]) ).
cnf(i_0_387,plain,
( mustard_dix
| ~ salt_lang
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_386,i_0_79]) ).
cnf(i_0_388,plain,
( salt_cole
| ~ mustard_dix
| salt_lang ),
inference(scs_inference,[],[i_0_211,i_0_104]) ).
cnf(i_0_389,plain,
( salt_lang
| ~ mustard_dix
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_388,i_0_375]) ).
cnf(i_0_390,plain,
( ~ mustard_lang
| mustard_barry
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_389,i_0_380]) ).
cnf(i_0_391,plain,
( ~ mustard_dix
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_390,i_0_240]) ).
cnf(i_0_392,plain,
( ~ mustard_lang
| mustard_barry ),
inference(scs_inference,[],[i_0_391,i_0_324]) ).
cnf(i_0_393,plain,
( ~ mustard_lang
| ~ salt_barry
| salt_mill ),
inference(scs_inference,[],[i_0_392,i_0_96]) ).
cnf(i_0_394,plain,
( salt_mill
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_393,i_0_222]) ).
cnf(i_0_395,plain,
( ~ salt_cole
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_394,i_0_81]) ).
cnf(i_0_396,plain,
( ~ salt_cole
| mustard_cole
| salt_cole ),
inference(scs_inference,[],[i_0_395,i_0_119]) ).
cnf(i_0_397,plain,
( mustard_mill
| salt_barry ),
inference(scs_inference,[],[i_0_222,i_0_156]) ).
cnf(i_0_398,plain,
( mustard_barry
| salt_barry ),
inference(scs_inference,[],[i_0_397,i_0_257]) ).
cnf(i_0_399,plain,
salt_barry,
inference(scs_inference,[],[i_0_398,i_0_330]) ).
cnf(i_0_400,plain,
( salt_lang
| salt_cole
| mustard_cole
| salt_dix
| mustard_dix
| mustard_mill
| ~ mustard_barry
| ~ salt_mill
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_399,i_0_63]) ).
cnf(i_0_401,plain,
( salt_lang
| mustard_lang
| ~ mustard_cole
| ~ salt_cole ),
inference(scs_inference,[],[i_0_399,i_0_68]) ).
cnf(i_0_402,plain,
( ~ mustard_barry
| salt_mill ),
inference(scs_inference,[],[i_0_399,i_0_96]) ).
cnf(i_0_403,plain,
( salt_lang
| mustard_barry ),
inference(scs_inference,[],[i_0_399,i_0_116]) ).
cnf(i_0_404,plain,
( ~ salt_cole
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_399,i_0_137]) ).
cnf(i_0_405,plain,
( salt_cole
| ~ salt_cole ),
inference(scs_inference,[],[i_0_399,i_0_252]) ).
cnf(i_0_406,plain,
( ~ salt_lang
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_399,i_0_340]) ).
cnf(i_0_407,plain,
( mustard_barry
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_399,i_0_359]) ).
cnf(i_0_408,plain,
( salt_mill
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_399,i_0_368]) ).
cnf(i_0_409,plain,
( salt_mill
| ~ salt_mill ),
inference(scs_inference,[],[i_0_402,i_0_233]) ).
cnf(i_0_410,plain,
( mustard_barry
| ~ salt_dix ),
inference(scs_inference,[],[i_0_403,i_0_357]) ).
cnf(i_0_411,plain,
( ~ mustard_barry
| ~ salt_dix ),
inference(scs_inference,[],[i_0_404,i_0_211]) ).
cnf(i_0_412,plain,
( ~ mustard_barry
| salt_dix
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_406,i_0_104]) ).
cnf(i_0_413,plain,
( ~ mustard_cole
| ~ salt_cole ),
inference(scs_inference,[],[i_0_407,i_0_404]) ).
cnf(i_0_414,plain,
( ~ mustard_cole
| ~ mustard_dix
| mustard_mill ),
inference(scs_inference,[],[i_0_408,i_0_167]) ).
cnf(i_0_415,plain,
( ~ salt_dix
| salt_mill ),
inference(scs_inference,[],[i_0_410,i_0_402]) ).
cnf(i_0_416,plain,
( ~ salt_dix
| ~ salt_mill ),
inference(scs_inference,[],[i_0_411,i_0_233]) ).
cnf(i_0_417,plain,
( ~ salt_cole
| ~ salt_dix ),
inference(scs_inference,[],[i_0_413,i_0_197]) ).
cnf(i_0_418,plain,
( salt_mill
| salt_lang
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_415,i_0_104]) ).
cnf(i_0_419,plain,
( ~ salt_mill
| ~ mustard_cole ),
inference(scs_inference,[],[i_0_416,i_0_247]) ).
cnf(i_0_420,plain,
~ salt_dix,
inference(scs_inference,[],[i_0_417,i_0_211]) ).
cnf(i_0_421,plain,
( salt_cole
| mustard_cole
| mustard_dix
| ~ mustard_mill ),
inference(scs_inference,[],[i_0_420,i_0_72]) ).
cnf(i_0_422,plain,
( mustard_mill
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_420,i_0_97]) ).
cnf(i_0_423,plain,
( salt_lang
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_420,i_0_104]) ).
cnf(i_0_424,plain,
( ~ salt_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_420,i_0_140]) ).
cnf(i_0_425,plain,
( ~ salt_cole
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_420,i_0_199]) ).
cnf(i_0_426,plain,
( ~ mustard_barry
| salt_mill ),
inference(scs_inference,[],[i_0_420,i_0_244]) ).
cnf(i_0_427,plain,
~ mustard_cole,
inference(scs_inference,[],[i_0_420,i_0_247]) ).
cnf(i_0_428,plain,
( salt_cole
| ~ salt_cole ),
inference(scs_inference,[],[i_0_420,i_0_255]) ).
cnf(i_0_429,plain,
( mustard_barry
| salt_lang ),
inference(scs_inference,[],[i_0_420,i_0_260]) ).
cnf(i_0_430,plain,
( ~ salt_lang
| mustard_mill ),
inference(scs_inference,[],[i_0_420,i_0_335]) ).
cnf(i_0_431,plain,
( salt_lang
| salt_cole
| mustard_cole
| mustard_dix
| mustard_mill
| ~ mustard_barry
| ~ salt_mill
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_420,i_0_400]) ).
cnf(i_0_432,plain,
( ~ mustard_barry
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_420,i_0_412]) ).
cnf(i_0_433,plain,
( ~ salt_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_427,i_0_100]) ).
cnf(i_0_434,plain,
( mustard_lang
| salt_cole ),
inference(scs_inference,[],[i_0_427,i_0_119]) ).
cnf(i_0_435,plain,
( ~ mustard_dix
| salt_lang ),
inference(scs_inference,[],[i_0_427,i_0_142]) ).
cnf(i_0_436,plain,
( mustard_lang
| mustard_mill ),
inference(scs_inference,[],[i_0_427,i_0_150]) ).
cnf(i_0_437,plain,
( mustard_mill
| ~ salt_lang ),
inference(scs_inference,[],[i_0_427,i_0_168]) ).
cnf(i_0_438,plain,
~ mustard_cole,
inference(scs_inference,[],[i_0_427,i_0_272]) ).
cnf(i_0_439,plain,
( mustard_mill
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_427,i_0_273]) ).
cnf(i_0_440,plain,
( ~ salt_cole
| ~ mustard_barry ),
inference(scs_inference,[],[i_0_427,i_0_279]) ).
cnf(i_0_441,plain,
( mustard_barry
| salt_lang ),
inference(scs_inference,[],[i_0_427,i_0_285]) ).
cnf(i_0_442,plain,
( ~ mustard_dix
| mustard_barry ),
inference(scs_inference,[],[i_0_427,i_0_383]) ).
cnf(i_0_443,plain,
salt_mill,
inference(scs_inference,[],[i_0_427,i_0_385]) ).
cnf(i_0_444,plain,
( ~ salt_cole
| salt_cole ),
inference(scs_inference,[],[i_0_427,i_0_396]) ).
cnf(i_0_445,plain,
( ~ salt_lang
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_443,i_0_79]) ).
cnf(i_0_446,plain,
( ~ mustard_dix
| mustard_mill ),
inference(scs_inference,[],[i_0_443,i_0_167]) ).
cnf(i_0_447,plain,
mustard_barry,
inference(scs_inference,[],[i_0_443,i_0_233]) ).
cnf(i_0_448,plain,
( ~ salt_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_443,i_0_308]) ).
cnf(i_0_449,plain,
( ~ salt_lang
| mustard_mill ),
inference(scs_inference,[],[i_0_443,i_0_309]) ).
cnf(i_0_450,plain,
( ~ salt_lang
| salt_cole ),
inference(scs_inference,[],[i_0_443,i_0_338]) ).
cnf(i_0_451,plain,
( mustard_lang
| mustard_dix ),
inference(scs_inference,[],[i_0_443,i_0_344]) ).
cnf(i_0_452,plain,
( mustard_dix
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_443,i_0_345]) ).
cnf(i_0_453,plain,
salt_mill,
inference(scs_inference,[],[i_0_443,i_0_409]) ).
cnf(i_0_454,plain,
~ mustard_cole,
inference(scs_inference,[],[i_0_443,i_0_419]) ).
cnf(i_0_455,plain,
( salt_cole
| mustard_dix
| ~ mustard_mill ),
inference(scs_inference,[],[i_0_427,i_0_421]) ).
cnf(i_0_456,plain,
( salt_lang
| salt_cole
| mustard_dix
| mustard_mill
| ~ mustard_barry
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_427,i_0_443,i_0_431]) ).
cnf(i_0_457,plain,
( ~ mustard_dix
| mustard_mill ),
inference(scs_inference,[],[i_0_447,i_0_87]) ).
cnf(i_0_458,plain,
( ~ mustard_dix
| salt_mill ),
inference(scs_inference,[],[i_0_447,i_0_95]) ).
cnf(i_0_459,plain,
( ~ mustard_dix
| ~ salt_lang ),
inference(scs_inference,[],[i_0_447,i_0_132]) ).
cnf(i_0_460,plain,
( ~ salt_cole
| salt_cole ),
inference(scs_inference,[],[i_0_447,i_0_202]) ).
cnf(i_0_461,plain,
( ~ salt_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_447,i_0_227]) ).
cnf(i_0_462,plain,
( salt_lang
| salt_mill ),
inference(scs_inference,[],[i_0_447,i_0_283]) ).
cnf(i_0_463,plain,
( mustard_lang
| mustard_mill ),
inference(scs_inference,[],[i_0_447,i_0_312]) ).
cnf(i_0_464,plain,
( ~ mustard_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_447,i_0_314]) ).
cnf(i_0_465,plain,
( ~ salt_lang
| ~ salt_cole ),
inference(scs_inference,[],[i_0_447,i_0_320]) ).
cnf(i_0_466,plain,
( ~ salt_cole
| salt_mill ),
inference(scs_inference,[],[i_0_447,i_0_321]) ).
cnf(i_0_467,plain,
mustard_barry,
inference(scs_inference,[],[i_0_447,i_0_323]) ).
cnf(i_0_468,plain,
( salt_mill
| ~ salt_lang ),
inference(scs_inference,[],[i_0_447,i_0_333]) ).
cnf(i_0_469,plain,
( ~ salt_lang
| mustard_mill ),
inference(scs_inference,[],[i_0_447,i_0_334]) ).
cnf(i_0_470,plain,
( salt_cole
| ~ salt_lang ),
inference(scs_inference,[],[i_0_447,i_0_339]) ).
cnf(i_0_471,plain,
( mustard_dix
| ~ salt_cole ),
inference(scs_inference,[],[i_0_447,i_0_342]) ).
cnf(i_0_472,plain,
( mustard_lang
| mustard_dix ),
inference(scs_inference,[],[i_0_447,i_0_343]) ).
cnf(i_0_473,plain,
( ~ mustard_cole
| salt_mill ),
inference(scs_inference,[],[i_0_447,i_0_367]) ).
cnf(i_0_474,plain,
salt_mill,
inference(scs_inference,[],[i_0_447,i_0_402]) ).
cnf(i_0_475,plain,
~ salt_cole,
inference(scs_inference,[],[i_0_447,i_0_404]) ).
cnf(i_0_476,plain,
~ salt_lang,
inference(scs_inference,[],[i_0_447,i_0_406]) ).
cnf(i_0_477,plain,
~ salt_cole,
inference(scs_inference,[],[i_0_447,i_0_425]) ).
cnf(i_0_478,plain,
salt_mill,
inference(scs_inference,[],[i_0_447,i_0_426]) ).
cnf(i_0_479,plain,
~ mustard_dix,
inference(scs_inference,[],[i_0_447,i_0_432]) ).
cnf(i_0_480,plain,
~ salt_cole,
inference(scs_inference,[],[i_0_447,i_0_440]) ).
cnf(i_0_481,plain,
mustard_lang,
inference(scs_inference,[],[i_0_476,i_0_479,i_0_120]) ).
cnf(i_0_482,plain,
( ~ mustard_dix
| mustard_mill ),
inference(scs_inference,[],[i_0_479,i_0_138]) ).
cnf(i_0_483,plain,
( ~ mustard_dix
| mustard_mill ),
inference(scs_inference,[],[i_0_475,i_0_179]) ).
cnf(i_0_484,plain,
( ~ salt_lang
| mustard_mill ),
inference(scs_inference,[],[i_0_475,i_0_180]) ).
cnf(i_0_485,plain,
mustard_barry,
inference(scs_inference,[],[i_0_475,i_0_190]) ).
cnf(i_0_486,plain,
( ~ mustard_dix
| ~ salt_lang ),
inference(scs_inference,[],[i_0_475,i_0_251]) ).
cnf(i_0_487,plain,
( ~ salt_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_475,i_0_256]) ).
cnf(i_0_488,plain,
( ~ mustard_mill
| mustard_barry ),
inference(scs_inference,[],[i_0_476,i_0_258]) ).
cnf(i_0_489,plain,
( mustard_lang
| ~ salt_lang ),
inference(scs_inference,[],[i_0_475,i_0_295]) ).
cnf(i_0_490,plain,
mustard_lang,
inference(scs_inference,[],[i_0_475,i_0_479,i_0_296]) ).
cnf(i_0_491,plain,
salt_mill,
inference(scs_inference,[],[i_0_475,i_0_299]) ).
cnf(i_0_492,plain,
( ~ salt_cole
| mustard_mill ),
inference(scs_inference,[],[i_0_479,i_0_307]) ).
cnf(i_0_493,plain,
( mustard_mill
| mustard_lang ),
inference(scs_inference,[],[i_0_479,i_0_311]) ).
cnf(i_0_494,plain,
~ mustard_cole,
inference(scs_inference,[],[i_0_479,i_0_313]) ).
cnf(i_0_495,plain,
~ mustard_dix,
inference(scs_inference,[],[i_0_479,i_0_476,i_0_315]) ).
cnf(i_0_496,plain,
( ~ salt_cole
| ~ salt_lang ),
inference(scs_inference,[],[i_0_475,i_0_318]) ).
cnf(i_0_497,plain,
mustard_barry,
inference(scs_inference,[],[i_0_479,i_0_324]) ).
cnf(i_0_498,plain,
( ~ salt_lang
| mustard_mill ),
inference(scs_inference,[],[i_0_479,i_0_348]) ).
cnf(i_0_499,plain,
~ mustard_cole,
inference(scs_inference,[],[i_0_475,i_0_366]) ).
cnf(i_0_500,plain,
salt_mill,
inference(scs_inference,[],[i_0_479,i_0_386]) ).
cnf(i_0_501,plain,
( ~ salt_lang
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_479,i_0_387]) ).
cnf(i_0_502,plain,
~ mustard_dix,
inference(scs_inference,[],[i_0_475,i_0_476,i_0_388]) ).
cnf(i_0_503,plain,
mustard_barry,
inference(scs_inference,[],[i_0_476,i_0_403]) ).
cnf(i_0_504,plain,
~ salt_cole,
inference(scs_inference,[],[i_0_475,i_0_405]) ).
cnf(i_0_505,plain,
( salt_mill
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_476,i_0_418]) ).
cnf(i_0_506,plain,
~ mustard_dix,
inference(scs_inference,[],[i_0_476,i_0_423]) ).
cnf(i_0_507,plain,
~ salt_cole,
inference(scs_inference,[],[i_0_475,i_0_428]) ).
cnf(i_0_508,plain,
mustard_barry,
inference(scs_inference,[],[i_0_476,i_0_429]) ).
cnf(i_0_509,plain,
mustard_lang,
inference(scs_inference,[],[i_0_475,i_0_434]) ).
cnf(i_0_510,plain,
~ mustard_dix,
inference(scs_inference,[],[i_0_476,i_0_435]) ).
cnf(i_0_511,plain,
mustard_barry,
inference(scs_inference,[],[i_0_476,i_0_441]) ).
cnf(i_0_512,plain,
~ salt_cole,
inference(scs_inference,[],[i_0_475,i_0_444]) ).
cnf(i_0_513,plain,
~ salt_lang,
inference(scs_inference,[],[i_0_475,i_0_450]) ).
cnf(i_0_514,plain,
mustard_lang,
inference(scs_inference,[],[i_0_479,i_0_451]) ).
cnf(i_0_515,plain,
~ mustard_dix,
inference(scs_inference,[],[i_0_479,i_0_452]) ).
cnf(i_0_516,plain,
~ mustard_mill,
inference(scs_inference,[],[i_0_475,i_0_479,i_0_455]) ).
cnf(i_0_517,plain,
( mustard_mill
| ~ mustard_lang ),
inference(scs_inference,[],[i_0_476,i_0_475,i_0_479,i_0_447,i_0_456]) ).
cnf(i_0_518,plain,
( mustard_lang
| ~ salt_lang ),
inference(scs_inference,[],[i_0_516,i_0_310]) ).
cnf(i_0_519,plain,
( ~ salt_lang
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_516,i_0_352]) ).
cnf(i_0_520,plain,
( ~ salt_lang
| ~ salt_cole ),
inference(scs_inference,[],[i_0_516,i_0_355]) ).
cnf(i_0_521,plain,
~ salt_lang,
inference(scs_inference,[],[i_0_490,i_0_363]) ).
cnf(i_0_522,plain,
~ mustard_cole,
inference(scs_inference,[],[i_0_490,i_0_370]) ).
cnf(i_0_523,plain,
salt_mill,
inference(scs_inference,[],[i_0_516,i_0_378]) ).
cnf(i_0_524,plain,
mustard_barry,
inference(scs_inference,[],[i_0_516,i_0_379]) ).
cnf(i_0_525,plain,
~ mustard_dix,
inference(scs_inference,[],[i_0_490,i_0_391]) ).
cnf(i_0_526,plain,
mustard_barry,
inference(scs_inference,[],[i_0_490,i_0_392]) ).
cnf(i_0_527,plain,
salt_mill,
inference(scs_inference,[],[i_0_490,i_0_394]) ).
cnf(i_0_528,plain,
~ salt_cole,
inference(scs_inference,[],[i_0_490,i_0_395]) ).
cnf(i_0_529,plain,
( ~ mustard_cole
| ~ mustard_dix ),
inference(scs_inference,[],[i_0_516,i_0_414]) ).
cnf(i_0_530,plain,
~ mustard_dix,
inference(scs_inference,[],[i_0_516,i_0_422]) ).
cnf(i_0_531,plain,
~ salt_cole,
inference(scs_inference,[],[i_0_516,i_0_424]) ).
cnf(i_0_532,plain,
~ salt_lang,
inference(scs_inference,[],[i_0_516,i_0_430]) ).
cnf(i_0_533,plain,
~ salt_cole,
inference(scs_inference,[],[i_0_516,i_0_433]) ).
cnf(i_0_534,plain,
mustard_lang,
inference(scs_inference,[],[i_0_516,i_0_436]) ).
cnf(i_0_535,plain,
~ salt_lang,
inference(scs_inference,[],[i_0_516,i_0_437]) ).
cnf(i_0_536,plain,
~ mustard_dix,
inference(scs_inference,[],[i_0_516,i_0_439]) ).
cnf(i_0_537,plain,
~ mustard_dix,
inference(scs_inference,[],[i_0_516,i_0_446]) ).
cnf(i_0_538,plain,
~ salt_cole,
inference(scs_inference,[],[i_0_516,i_0_448]) ).
cnf(i_0_539,plain,
~ salt_lang,
inference(scs_inference,[],[i_0_516,i_0_449]) ).
cnf(i_0_540,plain,
~ mustard_dix,
inference(scs_inference,[],[i_0_516,i_0_457]) ).
cnf(i_0_541,plain,
~ salt_cole,
inference(scs_inference,[],[i_0_477,i_0_460]) ).
cnf(i_0_542,plain,
~ salt_cole,
inference(scs_inference,[],[i_0_516,i_0_461]) ).
cnf(i_0_543,plain,
mustard_lang,
inference(scs_inference,[],[i_0_516,i_0_463]) ).
cnf(i_0_544,plain,
~ salt_lang,
inference(scs_inference,[],[i_0_516,i_0_469]) ).
cnf(i_0_545,plain,
~ salt_lang,
inference(scs_inference,[],[i_0_477,i_0_470]) ).
cnf(i_0_546,plain,
~ salt_cole,
inference(scs_inference,[],[i_0_495,i_0_471]) ).
cnf(i_0_547,plain,
mustard_lang,
inference(scs_inference,[],[i_0_495,i_0_472]) ).
cnf(i_0_548,plain,
$false,
inference(scs_inference,[],[i_0_490,i_0_516,i_0_517]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PUZ030-2 : TPTP v9.2.1. Released v1.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.32 % Computer : n016.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Tue May 5 01:33:36 EDT 2026
% 0.15/0.32 % CPUTime :
% 0.15/0.33 % start to proof: theBenchmark
% 0.58/1.61 % Version : CSE_E---1.7
% 0.58/1.61 % Problem : theBenchmark.p
% 0.58/1.61 % SZS status Unsatisfiable for theBenchmark.p
% 0.58/1.61 % SZS output start CNFRefutation
% See solution above
% 0.90/1.96 % Total time : 1.271s
%------------------------------------------------------------------------------