%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : SYO604+1 : TPTP v8.1.0. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n009.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 : 600s
% DateTime : Thu Jul 21 15:30:35 EDT 2022
% Result : Theorem 99.24s 13.32s
% Output : CNFRefutation 99.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 32
% Syntax : Number of clauses : 239 ( 8 unt; 206 nHn; 125 RR)
% Number of literals : 1304 ( 0 equ; 289 neg)
% Maximal clause size : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 1 con; 0-2 aty)
% Number of variables : 434 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_126,negated_conjecture,
( ~ g_false_only(X1,esk1_0)
| ~ g_false_only(X1,esk2_1(X1)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_126) ).
cnf(i_0_137,plain,
( g_true_only(X1,X2)
| g_both(X1,X2)
| g_false_only(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_137) ).
cnf(i_0_125,negated_conjecture,
( ~ g_false_only(X1,esk1_0)
| ~ g_false_only(esk2_1(X1),X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_125) ).
cnf(i_0_141,plain,
( epred1_2(X1,X2)
| ~ g_true_only(X3,X1)
| ~ g_true_only(X1,X2)
| ~ g_true_only(X1,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_141) ).
cnf(i_0_127,negated_conjecture,
~ epred1_2(X1,esk1_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_127) ).
cnf(i_0_122,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_true_only(X2,esk3_1(X2))
| ~ g_both(X1,X2)
| ~ g_false_only(X2,esk1_0) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_122) ).
cnf(i_0_121,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_true_only(esk3_1(X2),X2)
| ~ g_both(X1,X2)
| ~ g_false_only(X2,esk1_0) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_121) ).
cnf(i_0_124,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_true_only(X2,esk3_1(X2))
| ~ g_both(X2,X1)
| ~ g_false_only(X2,esk1_0) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_124) ).
cnf(i_0_123,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_true_only(esk3_1(X2),X2)
| ~ g_both(X2,X1)
| ~ g_false_only(X2,esk1_0) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_123) ).
cnf(i_0_130,plain,
( g_true(X1,X2)
| ~ g_true_only(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_130) ).
cnf(i_0_133,plain,
( g_true(X1,X2)
| ~ g_both(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_133) ).
cnf(i_0_116,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(X4,esk9_1(X4))
| g_false_only(esk6_1(X5),X5)
| epred1_2(esk5_1(X5),X5)
| g_true_only(X2,esk4_2(X5,X2))
| ~ g_both(X2,X1)
| ~ g_both(X2,X5) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_116) ).
cnf(i_0_135,plain,
( ~ g_false_only(X1,X2)
| ~ g_true(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_135) ).
cnf(i_0_86,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(X4,esk9_1(X4))
| g_false_only(esk6_1(X5),X5)
| epred1_2(esk5_1(X5),X5)
| g_true_only(esk4_2(X5,X2),X2)
| ~ g_both(X2,X1)
| ~ g_both(X2,X5) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_86) ).
cnf(i_0_85,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(esk9_1(X4),X4)
| g_false_only(esk6_1(X5),X5)
| epred1_2(esk5_1(X5),X5)
| g_true_only(esk4_2(X5,X2),X2)
| ~ g_both(X2,X1)
| ~ g_both(X2,X5) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_85) ).
cnf(i_0_129,plain,
( ~ g_true_only(X1,X2)
| ~ g_false(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_129) ).
cnf(i_0_136,plain,
( g_false(X1,X2)
| ~ g_false_only(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_136) ).
cnf(i_0_132,plain,
( g_false(X1,X2)
| ~ g_both(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_132) ).
cnf(i_0_115,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(esk9_1(X4),X4)
| g_false_only(esk6_1(X5),X5)
| epred1_2(esk5_1(X5),X5)
| g_true_only(X2,esk4_2(X5,X2))
| ~ g_both(X2,X1)
| ~ g_both(X2,X5) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_115) ).
cnf(i_0_68,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(X4,esk9_1(X4))
| g_false_only(X5,esk6_1(X6))
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(esk4_2(X6,X2),X2)
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_false_only(esk7_1(X6),esk6_1(X6)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_68) ).
cnf(i_0_74,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(X4,esk9_1(X4))
| g_false_only(X5,esk6_1(X6))
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(esk4_2(X6,X2),X2)
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_false_only(esk6_1(X6),esk7_1(X6)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_74) ).
cnf(i_0_98,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(X4,esk9_1(X4))
| g_false_only(X5,esk6_1(X6))
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(X2,esk4_2(X6,X2))
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_false_only(esk7_1(X6),esk6_1(X6)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_98) ).
cnf(i_0_104,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(X4,esk9_1(X4))
| g_false_only(X5,esk6_1(X6))
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(X2,esk4_2(X6,X2))
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_false_only(esk6_1(X6),esk7_1(X6)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_104) ).
cnf(i_0_67,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_false_only(X5,esk6_1(X6))
| g_true_only(esk9_1(X4),X4)
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(esk4_2(X6,X2),X2)
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_false_only(esk7_1(X6),esk6_1(X6)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_67) ).
cnf(i_0_73,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_false_only(X5,esk6_1(X6))
| g_true_only(esk9_1(X4),X4)
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(esk4_2(X6,X2),X2)
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_false_only(esk6_1(X6),esk7_1(X6)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_73) ).
cnf(i_0_97,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_false_only(X5,esk6_1(X6))
| g_true_only(esk9_1(X4),X4)
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(X2,esk4_2(X6,X2))
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_false_only(esk7_1(X6),esk6_1(X6)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_97) ).
cnf(i_0_103,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_false_only(X5,esk6_1(X6))
| g_true_only(esk9_1(X4),X4)
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(X2,esk4_2(X6,X2))
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_false_only(esk6_1(X6),esk7_1(X6)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_103) ).
cnf(i_0_62,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(X4,esk9_1(X4))
| g_false_only(X5,esk6_1(X6))
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(esk4_2(X6,X2),X2)
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_true_only(X7,esk6_1(X6))
| ~ g_true_only(esk6_1(X6),X7) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_62) ).
cnf(i_0_92,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(X4,esk9_1(X4))
| g_false_only(X5,esk6_1(X6))
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(X2,esk4_2(X6,X2))
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_true_only(X7,esk6_1(X6))
| ~ g_true_only(esk6_1(X6),X7) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_92) ).
cnf(i_0_61,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_false_only(X5,esk6_1(X6))
| g_true_only(esk9_1(X4),X4)
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(esk4_2(X6,X2),X2)
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_true_only(X7,esk6_1(X6))
| ~ g_true_only(esk6_1(X6),X7) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_61) ).
cnf(i_0_91,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_false_only(X5,esk6_1(X6))
| g_true_only(esk9_1(X4),X4)
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(X2,esk4_2(X6,X2))
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_true_only(X7,esk6_1(X6))
| ~ g_true_only(esk6_1(X6),X7) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_91) ).
cnf(i_0_138,plain,
( epred1_2(X1,X2)
| ~ g_true_only(X3,X1)
| ~ g_true_only(X1,X3)
| ~ g_both(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-uxppgzm_/lgb.p',i_0_138) ).
cnf(c_0_174,negated_conjecture,
( ~ g_false_only(X1,esk1_0)
| ~ g_false_only(X1,esk2_1(X1)) ),
i_0_126 ).
cnf(c_0_175,plain,
( g_true_only(X1,X2)
| g_both(X1,X2)
| g_false_only(X1,X2) ),
i_0_137 ).
cnf(c_0_176,negated_conjecture,
( g_true_only(X1,esk1_0)
| g_both(X1,esk1_0)
| ~ g_false_only(X1,esk2_1(X1)) ),
inference(spm,[status(thm)],[c_0_174,c_0_175]) ).
cnf(c_0_177,negated_conjecture,
( ~ g_false_only(X1,esk1_0)
| ~ g_false_only(esk2_1(X1),X1) ),
i_0_125 ).
cnf(c_0_178,plain,
( epred1_2(X1,X2)
| ~ g_true_only(X3,X1)
| ~ g_true_only(X1,X2)
| ~ g_true_only(X1,X3) ),
i_0_141 ).
cnf(c_0_179,plain,
( g_true_only(X1,esk2_1(X1))
| g_true_only(X1,esk1_0)
| g_both(X1,esk2_1(X1))
| g_both(X1,esk1_0) ),
inference(spm,[status(thm)],[c_0_176,c_0_175]) ).
cnf(c_0_180,negated_conjecture,
( g_true_only(X1,esk1_0)
| g_both(X1,esk1_0)
| ~ g_false_only(esk2_1(X1),X1) ),
inference(spm,[status(thm)],[c_0_177,c_0_175]) ).
cnf(c_0_181,plain,
( epred1_2(esk2_1(X1),X2)
| g_true_only(X1,esk1_0)
| g_both(X1,esk2_1(X1))
| g_both(X1,esk1_0)
| ~ g_true_only(esk2_1(X1),X1)
| ~ g_true_only(esk2_1(X1),X2) ),
inference(spm,[status(thm)],[c_0_178,c_0_179]) ).
cnf(c_0_182,plain,
( g_true_only(esk2_1(X1),X1)
| g_true_only(X1,esk1_0)
| g_both(esk2_1(X1),X1)
| g_both(X1,esk1_0) ),
inference(spm,[status(thm)],[c_0_180,c_0_175]) ).
cnf(c_0_183,plain,
( epred1_2(esk2_1(X1),X2)
| g_true_only(X1,esk1_0)
| g_both(esk2_1(X1),X1)
| g_both(X1,esk2_1(X1))
| g_both(X1,esk1_0)
| ~ g_true_only(esk2_1(X1),X2) ),
inference(spm,[status(thm)],[c_0_181,c_0_182]) ).
cnf(c_0_184,negated_conjecture,
~ epred1_2(X1,esk1_0),
i_0_127 ).
cnf(c_0_185,plain,
( epred1_2(esk2_1(X1),X1)
| g_true_only(X1,esk1_0)
| g_both(X1,esk2_1(X1))
| g_both(esk2_1(X1),X1)
| g_both(X1,esk1_0) ),
inference(spm,[status(thm)],[c_0_183,c_0_182]) ).
cnf(c_0_186,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_true_only(X2,esk3_1(X2))
| ~ g_both(X1,X2)
| ~ g_false_only(X2,esk1_0) ),
i_0_122 ).
cnf(c_0_187,negated_conjecture,
( g_true_only(esk1_0,esk1_0)
| g_both(esk2_1(esk1_0),esk1_0)
| g_both(esk1_0,esk2_1(esk1_0))
| g_both(esk1_0,esk1_0) ),
inference(spm,[status(thm)],[c_0_184,c_0_185]) ).
cnf(c_0_188,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_true_only(esk3_1(X2),X2)
| ~ g_both(X1,X2)
| ~ g_false_only(X2,esk1_0) ),
i_0_121 ).
cnf(c_0_189,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_true_only(X2,esk3_1(X2))
| ~ g_both(X2,X1)
| ~ g_false_only(X2,esk1_0) ),
i_0_124 ).
cnf(c_0_190,negated_conjecture,
( g_true_only(esk1_0,esk3_1(esk1_0))
| g_true_only(esk1_0,esk1_0)
| g_both(esk1_0,esk2_1(esk1_0))
| g_both(esk1_0,esk1_0) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_186,c_0_187]),c_0_175]),c_0_180]),c_0_176]) ).
cnf(c_0_191,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_true_only(esk3_1(X2),X2)
| ~ g_both(X2,X1)
| ~ g_false_only(X2,esk1_0) ),
i_0_123 ).
cnf(c_0_192,negated_conjecture,
( g_true_only(esk3_1(esk1_0),esk1_0)
| g_true_only(esk1_0,esk1_0)
| g_both(esk1_0,esk2_1(esk1_0))
| g_both(esk1_0,esk1_0) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_188,c_0_187]),c_0_175]),c_0_180]),c_0_176]) ).
cnf(c_0_193,negated_conjecture,
( g_true_only(esk1_0,esk3_1(esk1_0))
| g_true_only(esk1_0,esk1_0)
| g_both(esk1_0,esk1_0) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_189,c_0_190]),c_0_175]),c_0_180]),c_0_176]) ).
cnf(c_0_194,negated_conjecture,
( g_true_only(esk3_1(esk1_0),esk1_0)
| g_true_only(esk1_0,esk1_0)
| g_both(esk1_0,esk1_0) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_191,c_0_192]),c_0_175]),c_0_180]),c_0_176]) ).
cnf(c_0_195,plain,
( epred1_2(esk3_1(esk1_0),X1)
| g_true_only(esk1_0,esk1_0)
| g_both(esk1_0,esk1_0)
| ~ g_true_only(esk3_1(esk1_0),X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_178,c_0_193]),c_0_194]) ).
cnf(c_0_196,negated_conjecture,
( g_true_only(esk1_0,esk1_0)
| g_both(esk1_0,esk1_0) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_195,c_0_194]),c_0_184]) ).
cnf(c_0_197,plain,
( epred1_2(esk1_0,X1)
| g_both(esk1_0,esk1_0)
| ~ g_true_only(esk1_0,X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_178,c_0_196]),c_0_196]) ).
cnf(c_0_198,plain,
( g_true(X1,X2)
| ~ g_true_only(X1,X2) ),
i_0_130 ).
cnf(c_0_199,plain,
( g_true(X1,X2)
| ~ g_both(X1,X2) ),
i_0_133 ).
cnf(c_0_200,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(X4,esk9_1(X4))
| g_false_only(esk6_1(X5),X5)
| epred1_2(esk5_1(X5),X5)
| g_true_only(X2,esk4_2(X5,X2))
| ~ g_both(X2,X1)
| ~ g_both(X2,X5) ),
i_0_116 ).
cnf(c_0_201,negated_conjecture,
g_both(esk1_0,esk1_0),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_197,c_0_196]),c_0_184]) ).
cnf(c_0_202,plain,
( ~ g_false_only(X1,X2)
| ~ g_true(X1,X2) ),
i_0_135 ).
cnf(c_0_203,plain,
g_true(esk1_0,esk1_0),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_198,c_0_196]),c_0_199]) ).
cnf(c_0_204,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(X4,esk9_1(X4))
| g_false_only(esk6_1(X5),X5)
| epred1_2(esk5_1(X5),X5)
| g_true_only(esk4_2(X5,X2),X2)
| ~ g_both(X2,X1)
| ~ g_both(X2,X5) ),
i_0_86 ).
cnf(c_0_205,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(X1,esk9_1(X1))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X2,esk1_0)
| g_false_only(esk1_0,X2)
| g_false_only(X3,X1)
| g_false_only(X1,X3)
| ~ g_both(esk1_0,X2) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_200,c_0_201]),c_0_184]) ).
cnf(c_0_206,plain,
~ g_false_only(esk1_0,esk1_0),
inference(spm,[status(thm)],[c_0_202,c_0_203]) ).
cnf(c_0_207,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(X1,esk9_1(X1))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X2,esk1_0)
| g_false_only(esk1_0,X2)
| g_false_only(X3,X1)
| g_false_only(X1,X3)
| ~ g_both(esk1_0,X2) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_204,c_0_201]),c_0_184]) ).
cnf(c_0_208,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(esk9_1(X4),X4)
| g_false_only(esk6_1(X5),X5)
| epred1_2(esk5_1(X5),X5)
| g_true_only(esk4_2(X5,X2),X2)
| ~ g_both(X2,X1)
| ~ g_both(X2,X5) ),
i_0_85 ).
cnf(c_0_209,plain,
( ~ g_true_only(X1,X2)
| ~ g_false(X1,X2) ),
i_0_129 ).
cnf(c_0_210,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(X1,esk9_1(X1))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X1,X2)
| g_false_only(X2,X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_205,c_0_201]),c_0_206]) ).
cnf(c_0_211,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(X1,esk9_1(X1))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X1,X2)
| g_false_only(X2,X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_207,c_0_201]),c_0_206]) ).
cnf(c_0_212,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(X1),X1)
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X2,esk1_0)
| g_false_only(esk1_0,X2)
| g_false_only(X3,X1)
| g_false_only(X1,X3)
| ~ g_both(esk1_0,X2) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_208,c_0_201]),c_0_184]) ).
cnf(c_0_213,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X1,X2)
| g_false_only(X2,X1)
| ~ g_false(X2,esk9_1(X2)) ),
inference(spm,[status(thm)],[c_0_209,c_0_210]) ).
cnf(c_0_214,plain,
( g_false(X1,X2)
| ~ g_false_only(X1,X2) ),
i_0_136 ).
cnf(c_0_215,plain,
( g_false(X1,X2)
| ~ g_both(X1,X2) ),
i_0_132 ).
cnf(c_0_216,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(esk1_0,X1)
| ~ g_false_only(esk2_1(X1),X1) ),
inference(spm,[status(thm)],[c_0_177,c_0_210]) ).
cnf(c_0_217,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(esk1_0,X1)
| ~ g_false_only(X1,esk2_1(X1)) ),
inference(spm,[status(thm)],[c_0_174,c_0_210]) ).
cnf(c_0_218,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(esk9_1(X4),X4)
| g_false_only(esk6_1(X5),X5)
| epred1_2(esk5_1(X5),X5)
| g_true_only(X2,esk4_2(X5,X2))
| ~ g_both(X2,X1)
| ~ g_both(X2,X5) ),
i_0_115 ).
cnf(c_0_219,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(esk1_0,X1)
| ~ g_false_only(esk2_1(X1),X1) ),
inference(spm,[status(thm)],[c_0_177,c_0_211]) ).
cnf(c_0_220,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(esk1_0,X1)
| ~ g_false_only(X1,esk2_1(X1)) ),
inference(spm,[status(thm)],[c_0_174,c_0_211]) ).
cnf(c_0_221,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(X1),X1)
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X1,X2)
| g_false_only(X2,X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_212,c_0_201]),c_0_206]) ).
cnf(c_0_222,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X1,X1)
| ~ g_false(X1,esk9_1(X1)) ),
inference(ef,[status(thm)],[c_0_213]) ).
cnf(c_0_223,plain,
( g_true_only(X1,X2)
| g_false(X1,X2) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_214,c_0_175]),c_0_215]) ).
cnf(c_0_224,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_true_only(X1,esk9_1(X1))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(esk1_0,X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_216,c_0_210]),c_0_217]) ).
cnf(c_0_225,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(X1),X1)
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X2,esk1_0)
| g_false_only(esk1_0,X2)
| g_false_only(X3,X1)
| g_false_only(X1,X3)
| ~ g_both(esk1_0,X2) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_218,c_0_201]),c_0_184]) ).
cnf(c_0_226,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_true_only(X1,esk9_1(X1))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(esk1_0,X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_219,c_0_211]),c_0_220]) ).
cnf(c_0_227,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X1,X2)
| g_false_only(X2,X1)
| ~ g_false(esk9_1(X2),X2) ),
inference(spm,[status(thm)],[c_0_209,c_0_221]) ).
cnf(c_0_228,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(X1,esk9_1(X1))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X1,X1) ),
inference(spm,[status(thm)],[c_0_222,c_0_223]) ).
cnf(c_0_229,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_false_only(esk6_1(esk1_0),esk1_0) ),
inference(sr,[status(thm)],[inference(ef,[status(thm)],[c_0_224]),c_0_206]) ).
cnf(c_0_230,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(X1),X1)
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X1,X2)
| g_false_only(X2,X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_225,c_0_201]),c_0_206]) ).
cnf(c_0_231,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_false_only(esk6_1(esk1_0),esk1_0) ),
inference(sr,[status(thm)],[inference(ef,[status(thm)],[c_0_226]),c_0_206]) ).
cnf(c_0_232,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X1,X1)
| ~ g_false(esk9_1(X1),X1) ),
inference(ef,[status(thm)],[c_0_227]) ).
cnf(c_0_233,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(X4,esk9_1(X4))
| g_false_only(X5,esk6_1(X6))
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(esk4_2(X6,X2),X2)
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_false_only(esk7_1(X6),esk6_1(X6)) ),
i_0_68 ).
cnf(c_0_234,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(X4,esk9_1(X4))
| g_false_only(X5,esk6_1(X6))
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(esk4_2(X6,X2),X2)
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_false_only(esk6_1(X6),esk7_1(X6)) ),
i_0_74 ).
cnf(c_0_235,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true(X1,esk9_1(X1))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X1,X1) ),
inference(spm,[status(thm)],[c_0_198,c_0_228]) ).
cnf(c_0_236,plain,
( epred1_2(esk9_1(esk1_0),X1)
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_false_only(esk6_1(esk1_0),esk1_0)
| ~ g_true_only(esk9_1(esk1_0),esk1_0)
| ~ g_true_only(esk9_1(esk1_0),X1) ),
inference(spm,[status(thm)],[c_0_178,c_0_229]) ).
cnf(c_0_237,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(X1),X1)
| g_false(X2,X1)
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X1,X2) ),
inference(spm,[status(thm)],[c_0_214,c_0_230]) ).
cnf(c_0_238,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(X4,esk9_1(X4))
| g_false_only(X5,esk6_1(X6))
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(X2,esk4_2(X6,X2))
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_false_only(esk7_1(X6),esk6_1(X6)) ),
i_0_98 ).
cnf(c_0_239,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(X4,esk9_1(X4))
| g_false_only(X5,esk6_1(X6))
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(X2,esk4_2(X6,X2))
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_false_only(esk6_1(X6),esk7_1(X6)) ),
i_0_104 ).
cnf(c_0_240,plain,
( epred1_2(esk9_1(esk1_0),X1)
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_false_only(esk6_1(esk1_0),esk1_0)
| ~ g_true_only(esk9_1(esk1_0),esk1_0)
| ~ g_true_only(esk9_1(esk1_0),X1) ),
inference(spm,[status(thm)],[c_0_178,c_0_231]) ).
cnf(c_0_241,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(X1),X1)
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X1,X1) ),
inference(spm,[status(thm)],[c_0_232,c_0_223]) ).
cnf(c_0_242,negated_conjecture,
( epred1_2(esk5_1(X1),X1)
| g_true_only(esk4_2(X1,X2),X2)
| g_true_only(X3,esk9_1(X3))
| g_false_only(esk6_1(X1),X4)
| g_false_only(X4,esk6_1(X1))
| g_false_only(X3,X2)
| g_false_only(X2,X3)
| ~ g_both(X2,X1)
| ~ g_both(X2,X3)
| ~ g_false_only(esk7_1(X1),esk6_1(X1)) ),
inference(ef,[status(thm)],[c_0_233]) ).
cnf(c_0_243,negated_conjecture,
( epred1_2(esk5_1(X1),X1)
| g_true_only(esk4_2(X1,X2),X2)
| g_true_only(X3,esk9_1(X3))
| g_false_only(esk6_1(X1),X4)
| g_false_only(X4,esk6_1(X1))
| g_false_only(X3,X2)
| g_false_only(X2,X3)
| ~ g_both(X2,X1)
| ~ g_both(X2,X3)
| ~ g_false_only(esk6_1(X1),esk7_1(X1)) ),
inference(ef,[status(thm)],[c_0_234]) ).
cnf(c_0_244,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_false_only(X5,esk6_1(X6))
| g_true_only(esk9_1(X4),X4)
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(esk4_2(X6,X2),X2)
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_false_only(esk7_1(X6),esk6_1(X6)) ),
i_0_67 ).
cnf(c_0_245,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_false_only(X5,esk6_1(X6))
| g_true_only(esk9_1(X4),X4)
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(esk4_2(X6,X2),X2)
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_false_only(esk6_1(X6),esk7_1(X6)) ),
i_0_73 ).
cnf(c_0_246,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X1,X2)
| g_false_only(X2,X1)
| ~ g_false(esk9_1(X2),X2) ),
inference(spm,[status(thm)],[c_0_209,c_0_230]) ).
cnf(c_0_247,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X1,X1)
| ~ g_false_only(X1,esk9_1(X1)) ),
inference(spm,[status(thm)],[c_0_202,c_0_235]) ).
cnf(c_0_248,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_false(X1,esk1_0)
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(esk1_0,X1) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_236,c_0_237]),c_0_184]),c_0_237]) ).
cnf(c_0_249,negated_conjecture,
( epred1_2(esk5_1(X1),X1)
| g_true_only(X2,esk4_2(X1,X2))
| g_true_only(X3,esk9_1(X3))
| g_false_only(esk6_1(X1),X4)
| g_false_only(X4,esk6_1(X1))
| g_false_only(X3,X2)
| g_false_only(X2,X3)
| ~ g_both(X2,X1)
| ~ g_both(X2,X3)
| ~ g_false_only(esk7_1(X1),esk6_1(X1)) ),
inference(ef,[status(thm)],[c_0_238]) ).
cnf(c_0_250,negated_conjecture,
( epred1_2(esk5_1(X1),X1)
| g_true_only(X2,esk4_2(X1,X2))
| g_true_only(X3,esk9_1(X3))
| g_false_only(esk6_1(X1),X4)
| g_false_only(X4,esk6_1(X1))
| g_false_only(X3,X2)
| g_false_only(X2,X3)
| ~ g_both(X2,X1)
| ~ g_both(X2,X3)
| ~ g_false_only(esk6_1(X1),esk7_1(X1)) ),
inference(ef,[status(thm)],[c_0_239]) ).
cnf(c_0_251,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_false_only(X5,esk6_1(X6))
| g_true_only(esk9_1(X4),X4)
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(X2,esk4_2(X6,X2))
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_false_only(esk7_1(X6),esk6_1(X6)) ),
i_0_97 ).
cnf(c_0_252,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_false_only(X5,esk6_1(X6))
| g_true_only(esk9_1(X4),X4)
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(X2,esk4_2(X6,X2))
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_false_only(esk6_1(X6),esk7_1(X6)) ),
i_0_103 ).
cnf(c_0_253,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_false_only(esk6_1(esk1_0),esk1_0)
| ~ g_true_only(esk9_1(esk1_0),esk1_0) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_240,c_0_241]),c_0_184]),c_0_206]) ).
cnf(c_0_254,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(X1,esk9_1(X1))
| g_false_only(X2,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X2)
| g_false_only(esk1_0,X1)
| g_false_only(X1,esk1_0)
| ~ g_both(esk1_0,X1)
| ~ g_false_only(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_242,c_0_201]),c_0_184]) ).
cnf(c_0_255,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(X4,esk9_1(X4))
| g_false_only(X5,esk6_1(X6))
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(esk4_2(X6,X2),X2)
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_true_only(X7,esk6_1(X6))
| ~ g_true_only(esk6_1(X6),X7) ),
i_0_62 ).
cnf(c_0_256,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(X1,esk9_1(X1))
| g_false_only(X2,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X2)
| g_false_only(esk1_0,X1)
| g_false_only(X1,esk1_0)
| ~ g_both(esk1_0,X1)
| ~ g_false_only(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_243,c_0_201]),c_0_184]) ).
cnf(c_0_257,negated_conjecture,
( epred1_2(esk5_1(X1),X1)
| g_true_only(esk4_2(X1,X2),X2)
| g_true_only(esk9_1(X3),X3)
| g_false_only(esk6_1(X1),X4)
| g_false_only(X4,esk6_1(X1))
| g_false_only(X3,X2)
| g_false_only(X2,X3)
| ~ g_both(X2,X1)
| ~ g_both(X2,X3)
| ~ g_false_only(esk7_1(X1),esk6_1(X1)) ),
inference(ef,[status(thm)],[c_0_244]) ).
cnf(c_0_258,negated_conjecture,
( epred1_2(esk5_1(X1),X1)
| g_true_only(esk4_2(X1,X2),X2)
| g_true_only(esk9_1(X3),X3)
| g_false_only(esk6_1(X1),X4)
| g_false_only(X4,esk6_1(X1))
| g_false_only(X3,X2)
| g_false_only(X2,X3)
| ~ g_both(X2,X1)
| ~ g_both(X2,X3)
| ~ g_false_only(esk6_1(X1),esk7_1(X1)) ),
inference(ef,[status(thm)],[c_0_245]) ).
cnf(c_0_259,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_false_only(esk6_1(esk1_0),esk1_0)
| g_false_only(X1,X1)
| ~ g_false(esk9_1(X1),X1) ),
inference(ef,[status(thm)],[c_0_246]) ).
cnf(c_0_260,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_false(esk9_1(esk1_0),esk1_0)
| g_false_only(esk6_1(esk1_0),esk1_0) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_247,c_0_248]),c_0_206]) ).
cnf(c_0_261,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(X1,esk9_1(X1))
| g_false_only(X2,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X2)
| g_false_only(esk1_0,X1)
| g_false_only(X1,esk1_0)
| ~ g_both(esk1_0,X1)
| ~ g_false_only(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_249,c_0_201]),c_0_184]) ).
cnf(c_0_262,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_true_only(X4,esk9_1(X4))
| g_false_only(X5,esk6_1(X6))
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(X2,esk4_2(X6,X2))
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_true_only(X7,esk6_1(X6))
| ~ g_true_only(esk6_1(X6),X7) ),
i_0_92 ).
cnf(c_0_263,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(X1,esk9_1(X1))
| g_false_only(X2,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X2)
| g_false_only(esk1_0,X1)
| g_false_only(X1,esk1_0)
| ~ g_both(esk1_0,X1)
| ~ g_false_only(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_250,c_0_201]),c_0_184]) ).
cnf(c_0_264,negated_conjecture,
( epred1_2(esk5_1(X1),X1)
| g_true_only(X2,esk4_2(X1,X2))
| g_true_only(esk9_1(X3),X3)
| g_false_only(esk6_1(X1),X4)
| g_false_only(X4,esk6_1(X1))
| g_false_only(X3,X2)
| g_false_only(X2,X3)
| ~ g_both(X2,X1)
| ~ g_both(X2,X3)
| ~ g_false_only(esk7_1(X1),esk6_1(X1)) ),
inference(ef,[status(thm)],[c_0_251]) ).
cnf(c_0_265,negated_conjecture,
( epred1_2(esk5_1(X1),X1)
| g_true_only(X2,esk4_2(X1,X2))
| g_true_only(esk9_1(X3),X3)
| g_false_only(esk6_1(X1),X4)
| g_false_only(X4,esk6_1(X1))
| g_false_only(X3,X2)
| g_false_only(X2,X3)
| ~ g_both(X2,X1)
| ~ g_both(X2,X3)
| ~ g_false_only(esk6_1(X1),esk7_1(X1)) ),
inference(ef,[status(thm)],[c_0_252]) ).
cnf(c_0_266,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_false_only(esk6_1(esk1_0),esk1_0) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_253,c_0_241]),c_0_206]) ).
cnf(c_0_267,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0))
| ~ g_false_only(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_254,c_0_201]),c_0_206]) ).
cnf(c_0_268,negated_conjecture,
( epred1_2(esk5_1(X1),X1)
| g_true_only(esk4_2(X1,X2),X2)
| g_true_only(X3,esk9_1(X3))
| g_false_only(esk6_1(X1),X4)
| g_false_only(X4,esk6_1(X1))
| g_false_only(X3,X2)
| g_false_only(X2,X3)
| ~ g_true_only(X5,esk6_1(X1))
| ~ g_true_only(esk6_1(X1),X5)
| ~ g_both(X2,X1)
| ~ g_both(X2,X3) ),
inference(ef,[status(thm)],[c_0_255]) ).
cnf(c_0_269,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0))
| ~ g_false_only(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_256,c_0_201]),c_0_206]) ).
cnf(c_0_270,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(X1),X1)
| g_false_only(X2,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X2)
| g_false_only(esk1_0,X1)
| g_false_only(X1,esk1_0)
| ~ g_both(esk1_0,X1)
| ~ g_false_only(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_257,c_0_201]),c_0_184]) ).
cnf(c_0_271,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_false_only(X5,esk6_1(X6))
| g_true_only(esk9_1(X4),X4)
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(esk4_2(X6,X2),X2)
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_true_only(X7,esk6_1(X6))
| ~ g_true_only(esk6_1(X6),X7) ),
i_0_61 ).
cnf(c_0_272,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(X1),X1)
| g_false_only(X2,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X2)
| g_false_only(esk1_0,X1)
| g_false_only(X1,esk1_0)
| ~ g_both(esk1_0,X1)
| ~ g_false_only(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_258,c_0_201]),c_0_184]) ).
cnf(c_0_273,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_false_only(esk6_1(esk1_0),esk1_0) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_259,c_0_260]),c_0_206]) ).
cnf(c_0_274,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0))
| ~ g_false_only(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_261,c_0_201]),c_0_206]) ).
cnf(c_0_275,negated_conjecture,
( epred1_2(esk5_1(X1),X1)
| g_true_only(X2,esk4_2(X1,X2))
| g_true_only(X3,esk9_1(X3))
| g_false_only(esk6_1(X1),X4)
| g_false_only(X4,esk6_1(X1))
| g_false_only(X3,X2)
| g_false_only(X2,X3)
| ~ g_true_only(X5,esk6_1(X1))
| ~ g_true_only(esk6_1(X1),X5)
| ~ g_both(X2,X1)
| ~ g_both(X2,X3) ),
inference(ef,[status(thm)],[c_0_262]) ).
cnf(c_0_276,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0))
| ~ g_false_only(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_263,c_0_201]),c_0_206]) ).
cnf(c_0_277,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(X1),X1)
| g_false_only(X2,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X2)
| g_false_only(esk1_0,X1)
| g_false_only(X1,esk1_0)
| ~ g_both(esk1_0,X1)
| ~ g_false_only(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_264,c_0_201]),c_0_184]) ).
cnf(c_0_278,negated_conjecture,
( g_false_only(X1,X2)
| g_false_only(X2,X1)
| g_false_only(X3,X4)
| g_false_only(X4,X3)
| g_false_only(X5,esk6_1(X6))
| g_true_only(esk9_1(X4),X4)
| g_false_only(esk6_1(X6),X5)
| epred1_2(esk5_1(X6),X6)
| g_true_only(X2,esk4_2(X6,X2))
| ~ g_both(X2,X1)
| ~ g_both(X2,X6)
| ~ g_true_only(X7,esk6_1(X6))
| ~ g_true_only(esk6_1(X6),X7) ),
i_0_91 ).
cnf(c_0_279,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(X1),X1)
| g_false_only(X2,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X2)
| g_false_only(esk1_0,X1)
| g_false_only(X1,esk1_0)
| ~ g_both(esk1_0,X1)
| ~ g_false_only(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_265,c_0_201]),c_0_184]) ).
cnf(c_0_280,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| ~ g_false_only(esk2_1(esk6_1(esk1_0)),esk6_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_177,c_0_266]) ).
cnf(c_0_281,plain,
( g_true_only(esk7_1(esk1_0),esk6_1(esk1_0))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk7_1(esk1_0),esk6_1(esk1_0))
| g_false_only(X1,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1) ),
inference(spm,[status(thm)],[c_0_267,c_0_175]) ).
cnf(c_0_282,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| ~ g_false_only(esk6_1(esk1_0),esk2_1(esk6_1(esk1_0))) ),
inference(spm,[status(thm)],[c_0_174,c_0_266]) ).
cnf(c_0_283,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(X1,esk9_1(X1))
| g_false_only(X2,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X2)
| g_false_only(esk1_0,X1)
| g_false_only(X1,esk1_0)
| ~ g_true_only(X3,esk6_1(esk1_0))
| ~ g_true_only(esk6_1(esk1_0),X3)
| ~ g_both(esk1_0,X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_268,c_0_201]),c_0_184]) ).
cnf(c_0_284,plain,
( g_true_only(esk6_1(esk1_0),esk7_1(esk1_0))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk6_1(esk1_0),esk7_1(esk1_0))
| g_false_only(X1,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1) ),
inference(spm,[status(thm)],[c_0_269,c_0_175]) ).
cnf(c_0_285,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0))
| ~ g_false_only(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_270,c_0_201]),c_0_206]) ).
cnf(c_0_286,negated_conjecture,
( epred1_2(esk5_1(X1),X1)
| g_true_only(esk4_2(X1,X2),X2)
| g_true_only(esk9_1(X3),X3)
| g_false_only(esk6_1(X1),X4)
| g_false_only(X4,esk6_1(X1))
| g_false_only(X3,X2)
| g_false_only(X2,X3)
| ~ g_true_only(X5,esk6_1(X1))
| ~ g_true_only(esk6_1(X1),X5)
| ~ g_both(X2,X1)
| ~ g_both(X2,X3) ),
inference(ef,[status(thm)],[c_0_271]) ).
cnf(c_0_287,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0))
| ~ g_false_only(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_272,c_0_201]),c_0_206]) ).
cnf(c_0_288,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| ~ g_false_only(esk2_1(esk6_1(esk1_0)),esk6_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_177,c_0_273]) ).
cnf(c_0_289,plain,
( g_true_only(esk7_1(esk1_0),esk6_1(esk1_0))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk7_1(esk1_0),esk6_1(esk1_0))
| g_false_only(X1,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1) ),
inference(spm,[status(thm)],[c_0_274,c_0_175]) ).
cnf(c_0_290,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| ~ g_false_only(esk6_1(esk1_0),esk2_1(esk6_1(esk1_0))) ),
inference(spm,[status(thm)],[c_0_174,c_0_273]) ).
cnf(c_0_291,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(X1,esk9_1(X1))
| g_false_only(X2,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X2)
| g_false_only(esk1_0,X1)
| g_false_only(X1,esk1_0)
| ~ g_true_only(X3,esk6_1(esk1_0))
| ~ g_true_only(esk6_1(esk1_0),X3)
| ~ g_both(esk1_0,X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_275,c_0_201]),c_0_184]) ).
cnf(c_0_292,plain,
( g_true_only(esk6_1(esk1_0),esk7_1(esk1_0))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk6_1(esk1_0),esk7_1(esk1_0))
| g_false_only(X1,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1) ),
inference(spm,[status(thm)],[c_0_276,c_0_175]) ).
cnf(c_0_293,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0))
| ~ g_false_only(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_277,c_0_201]),c_0_206]) ).
cnf(c_0_294,negated_conjecture,
( epred1_2(esk5_1(X1),X1)
| g_true_only(X2,esk4_2(X1,X2))
| g_true_only(esk9_1(X3),X3)
| g_false_only(esk6_1(X1),X4)
| g_false_only(X4,esk6_1(X1))
| g_false_only(X3,X2)
| g_false_only(X2,X3)
| ~ g_true_only(X5,esk6_1(X1))
| ~ g_true_only(esk6_1(X1),X5)
| ~ g_both(X2,X1)
| ~ g_both(X2,X3) ),
inference(ef,[status(thm)],[c_0_278]) ).
cnf(c_0_295,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0))
| ~ g_false_only(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_279,c_0_201]),c_0_206]) ).
cnf(c_0_296,negated_conjecture,
( g_true_only(esk7_1(esk1_0),esk6_1(esk1_0))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_280,c_0_281]),c_0_282]) ).
cnf(c_0_297,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0))
| ~ g_true_only(X2,esk6_1(esk1_0))
| ~ g_true_only(esk6_1(esk1_0),X2) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_283,c_0_201]),c_0_206]) ).
cnf(c_0_298,negated_conjecture,
( g_true_only(esk6_1(esk1_0),esk7_1(esk1_0))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_280,c_0_284]),c_0_282]) ).
cnf(c_0_299,plain,
( g_true_only(esk7_1(esk1_0),esk6_1(esk1_0))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk7_1(esk1_0),esk6_1(esk1_0))
| g_false_only(X1,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1) ),
inference(spm,[status(thm)],[c_0_285,c_0_175]) ).
cnf(c_0_300,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(X1),X1)
| g_false_only(X2,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X2)
| g_false_only(esk1_0,X1)
| g_false_only(X1,esk1_0)
| ~ g_true_only(X3,esk6_1(esk1_0))
| ~ g_true_only(esk6_1(esk1_0),X3)
| ~ g_both(esk1_0,X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_286,c_0_201]),c_0_184]) ).
cnf(c_0_301,plain,
( g_true_only(esk6_1(esk1_0),esk7_1(esk1_0))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk6_1(esk1_0),esk7_1(esk1_0))
| g_false_only(X1,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1) ),
inference(spm,[status(thm)],[c_0_287,c_0_175]) ).
cnf(c_0_302,negated_conjecture,
( g_true_only(esk7_1(esk1_0),esk6_1(esk1_0))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_288,c_0_289]),c_0_290]) ).
cnf(c_0_303,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0))
| ~ g_true_only(X2,esk6_1(esk1_0))
| ~ g_true_only(esk6_1(esk1_0),X2) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_291,c_0_201]),c_0_206]) ).
cnf(c_0_304,negated_conjecture,
( g_true_only(esk6_1(esk1_0),esk7_1(esk1_0))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_288,c_0_292]),c_0_290]) ).
cnf(c_0_305,plain,
( g_true_only(esk7_1(esk1_0),esk6_1(esk1_0))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk7_1(esk1_0),esk6_1(esk1_0))
| g_false_only(X1,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1) ),
inference(spm,[status(thm)],[c_0_293,c_0_175]) ).
cnf(c_0_306,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(X1),X1)
| g_false_only(X2,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X2)
| g_false_only(esk1_0,X1)
| g_false_only(X1,esk1_0)
| ~ g_true_only(X3,esk6_1(esk1_0))
| ~ g_true_only(esk6_1(esk1_0),X3)
| ~ g_both(esk1_0,X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_294,c_0_201]),c_0_184]) ).
cnf(c_0_307,plain,
( g_true_only(esk6_1(esk1_0),esk7_1(esk1_0))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk6_1(esk1_0),esk7_1(esk1_0))
| g_false_only(X1,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1) ),
inference(spm,[status(thm)],[c_0_295,c_0_175]) ).
cnf(c_0_308,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_true(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_198,c_0_296]),c_0_199]) ).
cnf(c_0_309,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk7_1(esk1_0),esk6_1(esk1_0))
| g_false_only(X1,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1)
| ~ g_true_only(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_297,c_0_296]) ).
cnf(c_0_310,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_true(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_198,c_0_298]),c_0_199]) ).
cnf(c_0_311,negated_conjecture,
( g_true_only(esk7_1(esk1_0),esk6_1(esk1_0))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_280,c_0_299]),c_0_282]) ).
cnf(c_0_312,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0))
| ~ g_true_only(X2,esk6_1(esk1_0))
| ~ g_true_only(esk6_1(esk1_0),X2) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_300,c_0_201]),c_0_206]) ).
cnf(c_0_313,negated_conjecture,
( g_true_only(esk6_1(esk1_0),esk7_1(esk1_0))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_280,c_0_301]),c_0_282]) ).
cnf(c_0_314,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_true(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_198,c_0_302]),c_0_199]) ).
cnf(c_0_315,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk7_1(esk1_0),esk6_1(esk1_0))
| g_false_only(X1,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1)
| ~ g_true_only(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_303,c_0_302]) ).
cnf(c_0_316,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_true(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_198,c_0_304]),c_0_199]) ).
cnf(c_0_317,negated_conjecture,
( g_true_only(esk7_1(esk1_0),esk6_1(esk1_0))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_288,c_0_305]),c_0_290]) ).
cnf(c_0_318,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0))
| ~ g_true_only(X2,esk6_1(esk1_0))
| ~ g_true_only(esk6_1(esk1_0),X2) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_306,c_0_201]),c_0_206]) ).
cnf(c_0_319,negated_conjecture,
( g_true_only(esk6_1(esk1_0),esk7_1(esk1_0))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_288,c_0_307]),c_0_290]) ).
cnf(c_0_320,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| ~ g_false_only(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_202,c_0_308]) ).
cnf(c_0_321,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk6_1(esk1_0),esk7_1(esk1_0))
| g_both(esk7_1(esk1_0),esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_309,c_0_298]) ).
cnf(c_0_322,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| ~ g_false_only(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_202,c_0_310]) ).
cnf(c_0_323,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_true(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_198,c_0_311]),c_0_199]) ).
cnf(c_0_324,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk7_1(esk1_0),esk6_1(esk1_0))
| g_false_only(X1,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1)
| ~ g_true_only(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_312,c_0_311]) ).
cnf(c_0_325,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_true(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_198,c_0_313]),c_0_199]) ).
cnf(c_0_326,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| ~ g_false_only(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_202,c_0_314]) ).
cnf(c_0_327,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk6_1(esk1_0),esk7_1(esk1_0))
| g_both(esk7_1(esk1_0),esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_315,c_0_304]) ).
cnf(c_0_328,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| ~ g_false_only(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_202,c_0_316]) ).
cnf(c_0_329,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_true(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_198,c_0_317]),c_0_199]) ).
cnf(c_0_330,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk7_1(esk1_0),esk6_1(esk1_0))
| g_false_only(X1,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1)
| ~ g_true_only(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_318,c_0_317]) ).
cnf(c_0_331,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_true(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_198,c_0_319]),c_0_199]) ).
cnf(c_0_332,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk7_1(esk1_0),esk6_1(esk1_0))
| g_both(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_320,c_0_321]),c_0_322]) ).
cnf(c_0_333,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| ~ g_false_only(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_202,c_0_323]) ).
cnf(c_0_334,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk6_1(esk1_0),esk7_1(esk1_0))
| g_both(esk7_1(esk1_0),esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_324,c_0_313]) ).
cnf(c_0_335,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| ~ g_false_only(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_202,c_0_325]) ).
cnf(c_0_336,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk7_1(esk1_0),esk6_1(esk1_0))
| g_both(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_326,c_0_327]),c_0_328]) ).
cnf(c_0_337,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| ~ g_false_only(esk7_1(esk1_0),esk6_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_202,c_0_329]) ).
cnf(c_0_338,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk6_1(esk1_0),esk7_1(esk1_0))
| g_both(esk7_1(esk1_0),esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_330,c_0_319]) ).
cnf(c_0_339,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| ~ g_false_only(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_202,c_0_331]) ).
cnf(c_0_340,negated_conjecture,
( g_true_only(esk3_1(esk6_1(esk1_0)),esk6_1(esk1_0))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_188,c_0_332]),c_0_266]),c_0_320]),c_0_322]) ).
cnf(c_0_341,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk7_1(esk1_0),esk6_1(esk1_0))
| g_both(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_333,c_0_334]),c_0_335]) ).
cnf(c_0_342,negated_conjecture,
( g_true_only(esk3_1(esk6_1(esk1_0)),esk6_1(esk1_0))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_188,c_0_336]),c_0_273]),c_0_326]),c_0_328]) ).
cnf(c_0_343,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk7_1(esk1_0),esk6_1(esk1_0))
| g_both(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_337,c_0_338]),c_0_339]) ).
cnf(c_0_344,negated_conjecture,
( g_true_only(esk3_1(esk6_1(esk1_0)),esk6_1(esk1_0))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_191,c_0_340]),c_0_266]),c_0_320]),c_0_322]) ).
cnf(c_0_345,negated_conjecture,
( g_true_only(esk3_1(esk6_1(esk1_0)),esk6_1(esk1_0))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_188,c_0_341]),c_0_266]),c_0_333]),c_0_335]) ).
cnf(c_0_346,negated_conjecture,
( g_true_only(esk3_1(esk6_1(esk1_0)),esk6_1(esk1_0))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_191,c_0_342]),c_0_273]),c_0_326]),c_0_328]) ).
cnf(c_0_347,negated_conjecture,
( g_true_only(esk3_1(esk6_1(esk1_0)),esk6_1(esk1_0))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_188,c_0_343]),c_0_273]),c_0_337]),c_0_339]) ).
cnf(c_0_348,plain,
( epred1_2(esk9_1(esk1_0),X1)
| g_true_only(esk3_1(esk6_1(esk1_0)),esk6_1(esk1_0))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| ~ g_true_only(esk9_1(esk1_0),esk1_0)
| ~ g_true_only(esk9_1(esk1_0),X1) ),
inference(spm,[status(thm)],[c_0_178,c_0_344]) ).
cnf(c_0_349,negated_conjecture,
( g_true_only(esk3_1(esk6_1(esk1_0)),esk6_1(esk1_0))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_191,c_0_345]),c_0_266]),c_0_333]),c_0_335]) ).
cnf(c_0_350,negated_conjecture,
( g_true_only(esk6_1(esk1_0),esk3_1(esk6_1(esk1_0)))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_186,c_0_332]),c_0_266]),c_0_320]),c_0_322]) ).
cnf(c_0_351,plain,
( epred1_2(esk9_1(esk1_0),X1)
| g_true_only(esk3_1(esk6_1(esk1_0)),esk6_1(esk1_0))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| ~ g_true_only(esk9_1(esk1_0),esk1_0)
| ~ g_true_only(esk9_1(esk1_0),X1) ),
inference(spm,[status(thm)],[c_0_178,c_0_346]) ).
cnf(c_0_352,negated_conjecture,
( g_true_only(esk3_1(esk6_1(esk1_0)),esk6_1(esk1_0))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_191,c_0_347]),c_0_273]),c_0_337]),c_0_339]) ).
cnf(c_0_353,negated_conjecture,
( g_true_only(esk6_1(esk1_0),esk3_1(esk6_1(esk1_0)))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_both(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_186,c_0_336]),c_0_273]),c_0_326]),c_0_328]) ).
cnf(c_0_354,plain,
( g_true_only(esk3_1(esk6_1(esk1_0)),esk6_1(esk1_0))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_348,c_0_349]),c_0_184]),c_0_349]) ).
cnf(c_0_355,negated_conjecture,
( g_true_only(esk6_1(esk1_0),esk3_1(esk6_1(esk1_0)))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_189,c_0_350]),c_0_266]),c_0_320]),c_0_322]) ).
cnf(c_0_356,plain,
( g_true_only(esk3_1(esk6_1(esk1_0)),esk6_1(esk1_0))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0)) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_351,c_0_352]),c_0_184]),c_0_352]) ).
cnf(c_0_357,negated_conjecture,
( g_true_only(esk6_1(esk1_0),esk3_1(esk6_1(esk1_0)))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_189,c_0_353]),c_0_273]),c_0_326]),c_0_328]) ).
cnf(c_0_358,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_false_only(X1,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_297,c_0_354]),c_0_355]) ).
cnf(c_0_359,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0))
| g_false_only(X1,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_303,c_0_356]),c_0_357]) ).
cnf(c_0_360,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk1_0,esk9_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_320,c_0_358]),c_0_322]) ).
cnf(c_0_361,negated_conjecture,
( g_true_only(esk6_1(esk1_0),esk3_1(esk6_1(esk1_0)))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_186,c_0_341]),c_0_266]),c_0_333]),c_0_335]) ).
cnf(c_0_362,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk1_0,esk9_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_326,c_0_359]),c_0_328]) ).
cnf(c_0_363,negated_conjecture,
( g_true_only(esk6_1(esk1_0),esk3_1(esk6_1(esk1_0)))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_both(esk6_1(esk1_0),esk7_1(esk1_0)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_186,c_0_343]),c_0_273]),c_0_337]),c_0_339]) ).
cnf(c_0_364,plain,
( epred1_2(esk9_1(esk1_0),X1)
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| ~ g_true_only(esk9_1(esk1_0),esk1_0)
| ~ g_true_only(esk9_1(esk1_0),X1) ),
inference(spm,[status(thm)],[c_0_178,c_0_360]) ).
cnf(c_0_365,negated_conjecture,
( g_true_only(esk6_1(esk1_0),esk3_1(esk6_1(esk1_0)))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_189,c_0_361]),c_0_266]),c_0_333]),c_0_335]) ).
cnf(c_0_366,plain,
( epred1_2(esk9_1(esk1_0),X1)
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| ~ g_true_only(esk9_1(esk1_0),esk1_0)
| ~ g_true_only(esk9_1(esk1_0),X1) ),
inference(spm,[status(thm)],[c_0_178,c_0_362]) ).
cnf(c_0_367,negated_conjecture,
( g_true_only(esk6_1(esk1_0),esk3_1(esk6_1(esk1_0)))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_189,c_0_363]),c_0_273]),c_0_337]),c_0_339]) ).
cnf(c_0_368,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_false_only(X1,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1)
| ~ g_true_only(esk6_1(esk1_0),esk3_1(esk6_1(esk1_0))) ),
inference(spm,[status(thm)],[c_0_312,c_0_354]) ).
cnf(c_0_369,plain,
( g_true_only(esk6_1(esk1_0),esk3_1(esk6_1(esk1_0)))
| g_true_only(esk4_2(esk1_0,esk1_0),esk1_0) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_364,c_0_365]),c_0_184]),c_0_365]) ).
cnf(c_0_370,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_false_only(X1,esk6_1(esk1_0))
| g_false_only(esk6_1(esk1_0),X1)
| ~ g_true_only(esk6_1(esk1_0),esk3_1(esk6_1(esk1_0))) ),
inference(spm,[status(thm)],[c_0_318,c_0_356]) ).
cnf(c_0_371,plain,
( g_true_only(esk6_1(esk1_0),esk3_1(esk6_1(esk1_0)))
| g_true_only(esk1_0,esk4_2(esk1_0,esk1_0)) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_366,c_0_367]),c_0_184]),c_0_367]) ).
cnf(c_0_372,negated_conjecture,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_368,c_0_369]) ).
cnf(c_0_373,negated_conjecture,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0)
| g_false_only(esk6_1(esk1_0),X1)
| g_false_only(X1,esk6_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_370,c_0_371]) ).
cnf(c_0_374,plain,
( g_true_only(esk4_2(esk1_0,esk1_0),esk1_0)
| g_true_only(esk9_1(esk1_0),esk1_0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_333,c_0_372]),c_0_335]) ).
cnf(c_0_375,plain,
( g_true_only(esk1_0,esk4_2(esk1_0,esk1_0))
| g_true_only(esk9_1(esk1_0),esk1_0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_337,c_0_373]),c_0_339]) ).
cnf(c_0_376,plain,
( epred1_2(X1,X2)
| ~ g_true_only(X3,X1)
| ~ g_true_only(X1,X3)
| ~ g_both(X1,X2) ),
i_0_138 ).
cnf(c_0_377,plain,
g_true_only(esk4_2(esk1_0,esk1_0),esk1_0),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_364,c_0_374]),c_0_184]),c_0_374]) ).
cnf(c_0_378,plain,
g_true_only(esk1_0,esk4_2(esk1_0,esk1_0)),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_366,c_0_375]),c_0_184]),c_0_375]) ).
cnf(c_0_379,plain,
( epred1_2(esk1_0,X1)
| ~ g_both(esk1_0,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_376,c_0_377]),c_0_378])]) ).
cnf(c_0_380,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_379,c_0_201]),c_0_184]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SYO604+1 : TPTP v8.1.0. Released v7.0.0.
% 0.06/0.13 % Command : enigmatic-eprover.py %s %d 1
% 0.12/0.34 % Computer : n009.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Sat Jul 9 12:35:09 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.18/0.45 # ENIGMATIC: Selected complete mode:
% 99.24/13.32 # ENIGMATIC: Solved by autoschedule-lgb:
% 99.24/13.32 # No SInE strategy applied
% 99.24/13.32 # Trying AutoSched0 for 150 seconds
% 99.24/13.32 # AutoSched0-Mode selected heuristic G_E___208_B00_00_F1_SE_CS_SP_PS_S5PRR_S00EN
% 99.24/13.32 # and selection function PSelectSmallestOrientable.
% 99.24/13.32 #
% 99.24/13.32 # Preprocessing time : 0.044 s
% 99.24/13.32 # Presaturation interreduction done
% 99.24/13.32
% 99.24/13.32 # Proof found!
% 99.24/13.32 # SZS status Theorem
% 99.24/13.32 # SZS output start CNFRefutation
% See solution above
% 99.24/13.32 # Training examples: 0 positive, 0 negative
% 99.24/13.32
% 99.24/13.32 # -------------------------------------------------
% 99.24/13.32 # User time : 10.697 s
% 99.24/13.32 # System time : 0.238 s
% 99.24/13.32 # Total time : 10.935 s
% 99.24/13.32 # Maximum resident set size: 7124 pages
% 99.24/13.32
%------------------------------------------------------------------------------