%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SYO605+1 : TPTP v7.0.0. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : n106.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.75MB
% OS : Linux 3.10.0-327.36.3.el7.x86_64
% CPULimit : 300s
% DateTime : Fri Jan 20 10:34:46 EST 2017
% Result : Theorem 0.06s
% Output : CNFRefutation 0.06s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO605+1 : TPTP v7.0.0. Released v7.0.0.
% 0.00/0.03 % Command : Source/sine.py -e eprover -t %d %s
% 0.02/0.23 % Computer : n106.star.cs.uiowa.edu
% 0.02/0.23 % Model : x86_64 x86_64
% 0.02/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.02/0.23 % Memory : 32218.75MB
% 0.02/0.23 % OS : Linux 3.10.0-327.36.3.el7.x86_64
% 0.02/0.23 % CPULimit : 300
% 0.02/0.23 % DateTime : Fri Jan 20 05:57:47 CST 2017
% 0.02/0.23 % CPUTime:
% 0.06/0.27 % SZS status Started for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.27 --creating new selector for []
% 0.06/0.44 -running prover on /export/starexec/sandbox2/tmp/tmpjHBug2/sel_theBenchmark.p_1 with time limit 29
% 0.06/0.44 -running prover with command ['/export/starexec/sandbox2/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=29', '/export/starexec/sandbox2/tmp/tmpjHBug2/sel_theBenchmark.p_1']
% 0.06/0.44 -prover status Theorem
% 0.06/0.44 Problem theBenchmark.p solved in phase 0.
% 0.06/0.44 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.44 % SZS status Ended for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.44 Solved 1 out of 1.
% 0.06/0.44 # Problem is unsatisfiable (or provable), constructing proof object
% 0.06/0.44 # SZS status Theorem
% 0.06/0.44 # SZS output start CNFRefutation.
% 0.06/0.44 fof(1, axiom,![X1]:![X2]:(g_false_only(X1,X2)<=>(g_false(X1,X2)&~(g_true(X1,X2)))),file('/export/starexec/sandbox2/tmp/tmpjHBug2/sel_theBenchmark.p_1', false_only_g)).
% 0.06/0.44 fof(2, axiom,![X1]:![X2]:(g_true_only(X1,X2)<=>(g_true(X1,X2)&~(g_false(X1,X2)))),file('/export/starexec/sandbox2/tmp/tmpjHBug2/sel_theBenchmark.p_1', true_only_g)).
% 0.06/0.44 fof(3, axiom,![X1]:![X2]:((g_true_only(X1,X2)|g_both(X1,X2))|g_false_only(X1,X2)),file('/export/starexec/sandbox2/tmp/tmpjHBug2/sel_theBenchmark.p_1', exhaustion_g)).
% 0.06/0.44 fof(4,
% conjecture,((![X3]:?[X4]:(((g_true_only(X4,X3)&(g_both(X4,X4)|g_false_only(X4,X4)))|(g_both(X4,X3)&(g_true_only(X4,X4)|g_false_only(X4,X4))))|(g_false_only(X4,X3)&(g_true_only(X4,X4)|g_both(X4,X4))))|?[X4]:![X3]:?[X5]:(((g_true_only(X5,X3)&(g_both(X5,X4)|g_true_only(X5,X4)))|(g_both(X5,X3)&(g_false_only(X5,X4)|g_true_only(X5,X4))))|(g_false_only(X5,X3)&(g_false_only(X5,X4)|g_both(X5,X4)))))|(((?[X3]:(?[X4]:(g_both(X4,X3)&g_both(X4,X4))&~(?[X4]:(((g_true_only(X4,X3)&(g_both(X4,X4)|g_false_only(X4,X4)))|(g_both(X4,X3)&(g_true_only(X4,X4)|g_false_only(X4,X4))))|(g_false_only(X4,X3)&(g_true_only(X4,X4)|g_both(X4,X4))))))&~(?[X3]:![X4]:((g_true_only(X4,X3)&g_true_only(X4,X4))|(g_false_only(X4,X3)&g_false_only(X4,X4)))))&?[X4]:(?[X3]:(?[X5]:(g_both(X5,X3)&g_both(X5,X4))&~(?[X5]:(((g_true_only(X5,X3)&(g_both(X5,X4)|g_true_only(X5,X4)))|(g_both(X5,X3)&(g_false_only(X5,X4)|g_true_only(X5,X4))))|(g_false_only(X5,X3)&(g_false_only(X5,X4)|g_both(X5,X4))))))&~(?[X3]:![X5]:((g_true_only(X5,X3)&g_false_only(X5,X4))|(g_false
% _only(X5,X3)&g_true_only(X5,X4))))))&~(?[X4]:![X3]:?[X5]:(((g_true_only(X5,X3)&(g_both(X5,X4)|g_true_only(X5,X4)))|(g_both(X5,X3)&(g_false_only(X5,X4)|g_true_only(X5,X4))))|(g_false_only(X5,X3)&(g_false_only(X5,X4)|g_both(X5,X4))))))),file('/export/starexec/sandbox2/tmp/tmpjHBug2/sel_theBenchmark.p_1', nc4)).
% 0.06/0.44 fof(5, axiom,![X1]:![X2]:(g_both(X1,X2)<=>(g_true(X1,X2)&g_false(X1,X2))),file('/export/starexec/sandbox2/tmp/tmpjHBug2/sel_theBenchmark.p_1', both_g)).
% 0.06/0.44 fof(6,
% negated_conjecture,~(((![X3]:?[X4]:(((g_true_only(X4,X3)&(g_both(X4,X4)|g_false_only(X4,X4)))|(g_both(X4,X3)&(g_true_only(X4,X4)|g_false_only(X4,X4))))|(g_false_only(X4,X3)&(g_true_only(X4,X4)|g_both(X4,X4))))|?[X4]:![X3]:?[X5]:(((g_true_only(X5,X3)&(g_both(X5,X4)|g_true_only(X5,X4)))|(g_both(X5,X3)&(g_false_only(X5,X4)|g_true_only(X5,X4))))|(g_false_only(X5,X3)&(g_false_only(X5,X4)|g_both(X5,X4)))))|(((?[X3]:(?[X4]:(g_both(X4,X3)&g_both(X4,X4))&~(?[X4]:(((g_true_only(X4,X3)&(g_both(X4,X4)|g_false_only(X4,X4)))|(g_both(X4,X3)&(g_true_only(X4,X4)|g_false_only(X4,X4))))|(g_false_only(X4,X3)&(g_true_only(X4,X4)|g_both(X4,X4))))))&~(?[X3]:![X4]:((g_true_only(X4,X3)&g_true_only(X4,X4))|(g_false_only(X4,X3)&g_false_only(X4,X4)))))&?[X4]:(?[X3]:(?[X5]:(g_both(X5,X3)&g_both(X5,X4))&~(?[X5]:(((g_true_only(X5,X3)&(g_both(X5,X4)|g_true_only(X5,X4)))|(g_both(X5,X3)&(g_false_only(X5,X4)|g_true_only(X5,X4))))|(g_false_only(X5,X3)&(g_false_only(X5,X4)|g_both(X5,X4))))))&~(?[X3]:![X5]:((g_true_only(X5,X3)&g_false_only(X5,X4)
% )|(g_false_only(X5,X3)&g_true_only(X5,X4))))))&~(?[X4]:![X3]:?[X5]:(((g_true_only(X5,X3)&(g_both(X5,X4)|g_true_only(X5,X4)))|(g_both(X5,X3)&(g_false_only(X5,X4)|g_true_only(X5,X4))))|(g_false_only(X5,X3)&(g_false_only(X5,X4)|g_both(X5,X4)))))))),inference(assume_negation,[status(cth)],[4])).
% 0.06/0.44 fof(7, plain,![X1]:![X2]:(g_false_only(X1,X2)<=>(g_false(X1,X2)&~(g_true(X1,X2)))),inference(fof_simplification,[status(thm)],[1,theory(equality)])).
% 0.06/0.44 fof(8, plain,![X1]:![X2]:(g_true_only(X1,X2)<=>(g_true(X1,X2)&~(g_false(X1,X2)))),inference(fof_simplification,[status(thm)],[2,theory(equality)])).
% 0.06/0.44 fof(9, plain,((?[X3]:(?[X4]:(g_both(X4,X3)&g_both(X4,X4))&~(?[X4]:(((g_true_only(X4,X3)&(g_both(X4,X4)|g_false_only(X4,X4)))|(g_both(X4,X3)&(g_true_only(X4,X4)|g_false_only(X4,X4))))|(g_false_only(X4,X3)&(g_true_only(X4,X4)|g_both(X4,X4))))))&~(?[X3]:![X4]:((g_true_only(X4,X3)&g_true_only(X4,X4))|(g_false_only(X4,X3)&g_false_only(X4,X4)))))=>epred1_0),introduced(definition)).
% 0.06/0.44 fof(10, plain,(?[X4]:(?[X3]:(?[X5]:(g_both(X5,X3)&g_both(X5,X4))&~(?[X5]:(((g_true_only(X5,X3)&(g_both(X5,X4)|g_true_only(X5,X4)))|(g_both(X5,X3)&(g_false_only(X5,X4)|g_true_only(X5,X4))))|(g_false_only(X5,X3)&(g_false_only(X5,X4)|g_both(X5,X4))))))&~(?[X3]:![X5]:((g_true_only(X5,X3)&g_false_only(X5,X4))|(g_false_only(X5,X3)&g_true_only(X5,X4)))))=>epred2_0),introduced(definition)).
% 0.06/0.44 fof(11, negated_conjecture,~(((![X3]:?[X4]:(((g_true_only(X4,X3)&(g_both(X4,X4)|g_false_only(X4,X4)))|(g_both(X4,X3)&(g_true_only(X4,X4)|g_false_only(X4,X4))))|(g_false_only(X4,X3)&(g_true_only(X4,X4)|g_both(X4,X4))))|?[X4]:![X3]:?[X5]:(((g_true_only(X5,X3)&(g_both(X5,X4)|g_true_only(X5,X4)))|(g_both(X5,X3)&(g_false_only(X5,X4)|g_true_only(X5,X4))))|(g_false_only(X5,X3)&(g_false_only(X5,X4)|g_both(X5,X4)))))|((epred1_0&epred2_0)&~(?[X4]:![X3]:?[X5]:(((g_true_only(X5,X3)&(g_both(X5,X4)|g_true_only(X5,X4)))|(g_both(X5,X3)&(g_false_only(X5,X4)|g_true_only(X5,X4))))|(g_false_only(X5,X3)&(g_false_only(X5,X4)|g_both(X5,X4)))))))),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[6,9,theory(equality)]),10,theory(equality)])).
% 0.06/0.44 fof(12, plain,![X1]:![X2]:((~(g_false_only(X1,X2))|(g_false(X1,X2)&~(g_true(X1,X2))))&((~(g_false(X1,X2))|g_true(X1,X2))|g_false_only(X1,X2))),inference(fof_nnf,[status(thm)],[7])).
% 0.06/0.44 fof(13, plain,![X3]:![X4]:((~(g_false_only(X3,X4))|(g_false(X3,X4)&~(g_true(X3,X4))))&((~(g_false(X3,X4))|g_true(X3,X4))|g_false_only(X3,X4))),inference(variable_rename,[status(thm)],[12])).
% 0.06/0.44 fof(14, plain,![X3]:![X4]:(((g_false(X3,X4)|~(g_false_only(X3,X4)))&(~(g_true(X3,X4))|~(g_false_only(X3,X4))))&((~(g_false(X3,X4))|g_true(X3,X4))|g_false_only(X3,X4))),inference(distribute,[status(thm)],[13])).
% 0.06/0.44 cnf(16,plain,(~g_false_only(X1,X2)|~g_true(X1,X2)),inference(split_conjunct,[status(thm)],[14])).
% 0.06/0.44 fof(18, plain,![X1]:![X2]:((~(g_true_only(X1,X2))|(g_true(X1,X2)&~(g_false(X1,X2))))&((~(g_true(X1,X2))|g_false(X1,X2))|g_true_only(X1,X2))),inference(fof_nnf,[status(thm)],[8])).
% 0.06/0.44 fof(19, plain,![X3]:![X4]:((~(g_true_only(X3,X4))|(g_true(X3,X4)&~(g_false(X3,X4))))&((~(g_true(X3,X4))|g_false(X3,X4))|g_true_only(X3,X4))),inference(variable_rename,[status(thm)],[18])).
% 0.06/0.44 fof(20, plain,![X3]:![X4]:(((g_true(X3,X4)|~(g_true_only(X3,X4)))&(~(g_false(X3,X4))|~(g_true_only(X3,X4))))&((~(g_true(X3,X4))|g_false(X3,X4))|g_true_only(X3,X4))),inference(distribute,[status(thm)],[19])).
% 0.06/0.44 cnf(22,plain,(~g_true_only(X1,X2)|~g_false(X1,X2)),inference(split_conjunct,[status(thm)],[20])).
% 0.06/0.44 cnf(23,plain,(g_true(X1,X2)|~g_true_only(X1,X2)),inference(split_conjunct,[status(thm)],[20])).
% 0.06/0.44 fof(24, plain,![X3]:![X4]:((g_true_only(X3,X4)|g_both(X3,X4))|g_false_only(X3,X4)),inference(variable_rename,[status(thm)],[3])).
% 0.06/0.44 cnf(25,plain,(g_false_only(X1,X2)|g_both(X1,X2)|g_true_only(X1,X2)),inference(split_conjunct,[status(thm)],[24])).
% 0.06/0.44 fof(26, negated_conjecture,((?[X3]:![X4]:(((~(g_true_only(X4,X3))|(~(g_both(X4,X4))&~(g_false_only(X4,X4))))&(~(g_both(X4,X3))|(~(g_true_only(X4,X4))&~(g_false_only(X4,X4)))))&(~(g_false_only(X4,X3))|(~(g_true_only(X4,X4))&~(g_both(X4,X4)))))&![X4]:?[X3]:![X5]:(((~(g_true_only(X5,X3))|(~(g_both(X5,X4))&~(g_true_only(X5,X4))))&(~(g_both(X5,X3))|(~(g_false_only(X5,X4))&~(g_true_only(X5,X4)))))&(~(g_false_only(X5,X3))|(~(g_false_only(X5,X4))&~(g_both(X5,X4))))))&((~(epred1_0)|~(epred2_0))|?[X4]:![X3]:?[X5]:(((g_true_only(X5,X3)&(g_both(X5,X4)|g_true_only(X5,X4)))|(g_both(X5,X3)&(g_false_only(X5,X4)|g_true_only(X5,X4))))|(g_false_only(X5,X3)&(g_false_only(X5,X4)|g_both(X5,X4)))))),inference(fof_nnf,[status(thm)],[11])).
% 0.06/0.44 fof(27, negated_conjecture,((?[X6]:![X7]:(((~(g_true_only(X7,X6))|(~(g_both(X7,X7))&~(g_false_only(X7,X7))))&(~(g_both(X7,X6))|(~(g_true_only(X7,X7))&~(g_false_only(X7,X7)))))&(~(g_false_only(X7,X6))|(~(g_true_only(X7,X7))&~(g_both(X7,X7)))))&![X8]:?[X9]:![X10]:(((~(g_true_only(X10,X9))|(~(g_both(X10,X8))&~(g_true_only(X10,X8))))&(~(g_both(X10,X9))|(~(g_false_only(X10,X8))&~(g_true_only(X10,X8)))))&(~(g_false_only(X10,X9))|(~(g_false_only(X10,X8))&~(g_both(X10,X8))))))&((~(epred1_0)|~(epred2_0))|?[X11]:![X12]:?[X13]:(((g_true_only(X13,X12)&(g_both(X13,X11)|g_true_only(X13,X11)))|(g_both(X13,X12)&(g_false_only(X13,X11)|g_true_only(X13,X11))))|(g_false_only(X13,X12)&(g_false_only(X13,X11)|g_both(X13,X11)))))),inference(variable_rename,[status(thm)],[26])).
% 0.06/0.44 fof(28, negated_conjecture,((![X7]:(((~(g_true_only(X7,esk1_0))|(~(g_both(X7,X7))&~(g_false_only(X7,X7))))&(~(g_both(X7,esk1_0))|(~(g_true_only(X7,X7))&~(g_false_only(X7,X7)))))&(~(g_false_only(X7,esk1_0))|(~(g_true_only(X7,X7))&~(g_both(X7,X7)))))&![X8]:![X10]:(((~(g_true_only(X10,esk2_1(X8)))|(~(g_both(X10,X8))&~(g_true_only(X10,X8))))&(~(g_both(X10,esk2_1(X8)))|(~(g_false_only(X10,X8))&~(g_true_only(X10,X8)))))&(~(g_false_only(X10,esk2_1(X8)))|(~(g_false_only(X10,X8))&~(g_both(X10,X8))))))&((~(epred1_0)|~(epred2_0))|![X12]:(((g_true_only(esk4_1(X12),X12)&(g_both(esk4_1(X12),esk3_0)|g_true_only(esk4_1(X12),esk3_0)))|(g_both(esk4_1(X12),X12)&(g_false_only(esk4_1(X12),esk3_0)|g_true_only(esk4_1(X12),esk3_0))))|(g_false_only(esk4_1(X12),X12)&(g_false_only(esk4_1(X12),esk3_0)|g_both(esk4_1(X12),esk3_0)))))),inference(skolemize,[status(esa)],[27])).
% 0.06/0.44 fof(29, negated_conjecture,![X7]:![X8]:![X10]:![X12]:(((((g_true_only(esk4_1(X12),X12)&(g_both(esk4_1(X12),esk3_0)|g_true_only(esk4_1(X12),esk3_0)))|(g_both(esk4_1(X12),X12)&(g_false_only(esk4_1(X12),esk3_0)|g_true_only(esk4_1(X12),esk3_0))))|(g_false_only(esk4_1(X12),X12)&(g_false_only(esk4_1(X12),esk3_0)|g_both(esk4_1(X12),esk3_0))))|(~(epred1_0)|~(epred2_0)))&((((~(g_true_only(X10,esk2_1(X8)))|(~(g_both(X10,X8))&~(g_true_only(X10,X8))))&(~(g_both(X10,esk2_1(X8)))|(~(g_false_only(X10,X8))&~(g_true_only(X10,X8)))))&(~(g_false_only(X10,esk2_1(X8)))|(~(g_false_only(X10,X8))&~(g_both(X10,X8)))))&(((~(g_true_only(X7,esk1_0))|(~(g_both(X7,X7))&~(g_false_only(X7,X7))))&(~(g_both(X7,esk1_0))|(~(g_true_only(X7,X7))&~(g_false_only(X7,X7)))))&(~(g_false_only(X7,esk1_0))|(~(g_true_only(X7,X7))&~(g_both(X7,X7))))))),inference(shift_quantors,[status(thm)],[28])).
% 0.06/0.44 fof(30,
% negated_conjecture,![X7]:![X8]:![X10]:![X12]:((((((g_false_only(esk4_1(X12),X12)|(g_both(esk4_1(X12),X12)|g_true_only(esk4_1(X12),X12)))|(~(epred1_0)|~(epred2_0)))&(((g_false_only(esk4_1(X12),esk3_0)|g_both(esk4_1(X12),esk3_0))|(g_both(esk4_1(X12),X12)|g_true_only(esk4_1(X12),X12)))|(~(epred1_0)|~(epred2_0))))&(((g_false_only(esk4_1(X12),X12)|((g_false_only(esk4_1(X12),esk3_0)|g_true_only(esk4_1(X12),esk3_0))|g_true_only(esk4_1(X12),X12)))|(~(epred1_0)|~(epred2_0)))&(((g_false_only(esk4_1(X12),esk3_0)|g_both(esk4_1(X12),esk3_0))|((g_false_only(esk4_1(X12),esk3_0)|g_true_only(esk4_1(X12),esk3_0))|g_true_only(esk4_1(X12),X12)))|(~(epred1_0)|~(epred2_0)))))&((((g_false_only(esk4_1(X12),X12)|(g_both(esk4_1(X12),X12)|(g_both(esk4_1(X12),esk3_0)|g_true_only(esk4_1(X12),esk3_0))))|(~(epred1_0)|~(epred2_0)))&(((g_false_only(esk4_1(X12),esk3_0)|g_both(esk4_1(X12),esk3_0))|(g_both(esk4_1(X12),X12)|(g_both(esk4_1(X12),esk3_0)|g_true_only(esk4_1(X12),esk3_0))))|(~(epred1_0)|~(epred2_0))))&(((g_false_only(esk4_1(X12),X12)
% |((g_false_only(esk4_1(X12),esk3_0)|g_true_only(esk4_1(X12),esk3_0))|(g_both(esk4_1(X12),esk3_0)|g_true_only(esk4_1(X12),esk3_0))))|(~(epred1_0)|~(epred2_0)))&(((g_false_only(esk4_1(X12),esk3_0)|g_both(esk4_1(X12),esk3_0))|((g_false_only(esk4_1(X12),esk3_0)|g_true_only(esk4_1(X12),esk3_0))|(g_both(esk4_1(X12),esk3_0)|g_true_only(esk4_1(X12),esk3_0))))|(~(epred1_0)|~(epred2_0))))))&(((((~(g_both(X10,X8))|~(g_true_only(X10,esk2_1(X8))))&(~(g_true_only(X10,X8))|~(g_true_only(X10,esk2_1(X8)))))&((~(g_false_only(X10,X8))|~(g_both(X10,esk2_1(X8))))&(~(g_true_only(X10,X8))|~(g_both(X10,esk2_1(X8))))))&((~(g_false_only(X10,X8))|~(g_false_only(X10,esk2_1(X8))))&(~(g_both(X10,X8))|~(g_false_only(X10,esk2_1(X8))))))&((((~(g_both(X7,X7))|~(g_true_only(X7,esk1_0)))&(~(g_false_only(X7,X7))|~(g_true_only(X7,esk1_0))))&((~(g_true_only(X7,X7))|~(g_both(X7,esk1_0)))&(~(g_false_only(X7,X7))|~(g_both(X7,esk1_0)))))&((~(g_true_only(X7,X7))|~(g_false_only(X7,esk1_0)))&(~(g_both(X7,X7))|~(g_false_only(X7,esk1_0))))))),inference(dis
% tribute,[status(thm)],[29])).
% 0.06/0.44 cnf(31,negated_conjecture,(~g_false_only(X1,esk1_0)|~g_both(X1,X1)),inference(split_conjunct,[status(thm)],[30])).
% 0.06/0.44 cnf(32,negated_conjecture,(~g_false_only(X1,esk1_0)|~g_true_only(X1,X1)),inference(split_conjunct,[status(thm)],[30])).
% 0.06/0.44 cnf(33,negated_conjecture,(~g_both(X1,esk1_0)|~g_false_only(X1,X1)),inference(split_conjunct,[status(thm)],[30])).
% 0.06/0.44 cnf(34,negated_conjecture,(~g_both(X1,esk1_0)|~g_true_only(X1,X1)),inference(split_conjunct,[status(thm)],[30])).
% 0.06/0.44 cnf(35,negated_conjecture,(~g_true_only(X1,esk1_0)|~g_false_only(X1,X1)),inference(split_conjunct,[status(thm)],[30])).
% 0.06/0.44 cnf(36,negated_conjecture,(~g_true_only(X1,esk1_0)|~g_both(X1,X1)),inference(split_conjunct,[status(thm)],[30])).
% 0.06/0.44 cnf(37,negated_conjecture,(~g_false_only(X1,esk2_1(X2))|~g_both(X1,X2)),inference(split_conjunct,[status(thm)],[30])).
% 0.06/0.44 cnf(38,negated_conjecture,(~g_false_only(X1,esk2_1(X2))|~g_false_only(X1,X2)),inference(split_conjunct,[status(thm)],[30])).
% 0.06/0.44 cnf(39,negated_conjecture,(~g_both(X1,esk2_1(X2))|~g_true_only(X1,X2)),inference(split_conjunct,[status(thm)],[30])).
% 0.06/0.44 cnf(40,negated_conjecture,(~g_both(X1,esk2_1(X2))|~g_false_only(X1,X2)),inference(split_conjunct,[status(thm)],[30])).
% 0.06/0.44 cnf(41,negated_conjecture,(~g_true_only(X1,esk2_1(X2))|~g_true_only(X1,X2)),inference(split_conjunct,[status(thm)],[30])).
% 0.06/0.44 cnf(42,negated_conjecture,(~g_true_only(X1,esk2_1(X2))|~g_both(X1,X2)),inference(split_conjunct,[status(thm)],[30])).
% 0.06/0.44 cnf(46,negated_conjecture,(g_true_only(esk4_1(X1),esk3_0)|g_both(esk4_1(X1),esk3_0)|g_both(esk4_1(X1),X1)|g_false_only(esk4_1(X1),X1)|~epred2_0|~epred1_0),inference(split_conjunct,[status(thm)],[30])).
% 0.06/0.44 cnf(48,negated_conjecture,(g_true_only(esk4_1(X1),X1)|g_true_only(esk4_1(X1),esk3_0)|g_false_only(esk4_1(X1),esk3_0)|g_false_only(esk4_1(X1),X1)|~epred2_0|~epred1_0),inference(split_conjunct,[status(thm)],[30])).
% 0.06/0.44 cnf(49,negated_conjecture,(g_true_only(esk4_1(X1),X1)|g_both(esk4_1(X1),X1)|g_both(esk4_1(X1),esk3_0)|g_false_only(esk4_1(X1),esk3_0)|~epred2_0|~epred1_0),inference(split_conjunct,[status(thm)],[30])).
% 0.06/0.44 fof(51, plain,![X1]:![X2]:((~(g_both(X1,X2))|(g_true(X1,X2)&g_false(X1,X2)))&((~(g_true(X1,X2))|~(g_false(X1,X2)))|g_both(X1,X2))),inference(fof_nnf,[status(thm)],[5])).
% 0.06/0.44 fof(52, plain,![X3]:![X4]:((~(g_both(X3,X4))|(g_true(X3,X4)&g_false(X3,X4)))&((~(g_true(X3,X4))|~(g_false(X3,X4)))|g_both(X3,X4))),inference(variable_rename,[status(thm)],[51])).
% 0.06/0.44 fof(53, plain,![X3]:![X4]:(((g_true(X3,X4)|~(g_both(X3,X4)))&(g_false(X3,X4)|~(g_both(X3,X4))))&((~(g_true(X3,X4))|~(g_false(X3,X4)))|g_both(X3,X4))),inference(distribute,[status(thm)],[52])).
% 0.06/0.44 cnf(55,plain,(g_false(X1,X2)|~g_both(X1,X2)),inference(split_conjunct,[status(thm)],[53])).
% 0.06/0.44 cnf(56,plain,(g_true(X1,X2)|~g_both(X1,X2)),inference(split_conjunct,[status(thm)],[53])).
% 0.06/0.44 fof(57, plain,((![X3]:(![X4]:(~(g_both(X4,X3))|~(g_both(X4,X4)))|?[X4]:(((g_true_only(X4,X3)&(g_both(X4,X4)|g_false_only(X4,X4)))|(g_both(X4,X3)&(g_true_only(X4,X4)|g_false_only(X4,X4))))|(g_false_only(X4,X3)&(g_true_only(X4,X4)|g_both(X4,X4)))))|?[X3]:![X4]:((g_true_only(X4,X3)&g_true_only(X4,X4))|(g_false_only(X4,X3)&g_false_only(X4,X4))))|epred1_0),inference(fof_nnf,[status(thm)],[9])).
% 0.06/0.44 fof(58, plain,((![X5]:(![X6]:(~(g_both(X6,X5))|~(g_both(X6,X6)))|?[X7]:(((g_true_only(X7,X5)&(g_both(X7,X7)|g_false_only(X7,X7)))|(g_both(X7,X5)&(g_true_only(X7,X7)|g_false_only(X7,X7))))|(g_false_only(X7,X5)&(g_true_only(X7,X7)|g_both(X7,X7)))))|?[X8]:![X9]:((g_true_only(X9,X8)&g_true_only(X9,X9))|(g_false_only(X9,X8)&g_false_only(X9,X9))))|epred1_0),inference(variable_rename,[status(thm)],[57])).
% 0.06/0.44 fof(59, plain,((![X5]:(![X6]:(~(g_both(X6,X5))|~(g_both(X6,X6)))|(((g_true_only(esk5_1(X5),X5)&(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5))))|(g_both(esk5_1(X5),X5)&(g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))))|(g_false_only(esk5_1(X5),X5)&(g_true_only(esk5_1(X5),esk5_1(X5))|g_both(esk5_1(X5),esk5_1(X5))))))|![X9]:((g_true_only(X9,esk6_0)&g_true_only(X9,X9))|(g_false_only(X9,esk6_0)&g_false_only(X9,X9))))|epred1_0),inference(skolemize,[status(esa)],[58])).
% 0.06/0.44 fof(60, plain,![X5]:![X6]:![X9]:((((g_true_only(X9,esk6_0)&g_true_only(X9,X9))|(g_false_only(X9,esk6_0)&g_false_only(X9,X9)))|((~(g_both(X6,X5))|~(g_both(X6,X6)))|(((g_true_only(esk5_1(X5),X5)&(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5))))|(g_both(esk5_1(X5),X5)&(g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))))|(g_false_only(esk5_1(X5),X5)&(g_true_only(esk5_1(X5),esk5_1(X5))|g_both(esk5_1(X5),esk5_1(X5)))))))|epred1_0),inference(shift_quantors,[status(thm)],[59])).
% 0.06/0.44 fof(61,
% plain,![X5]:![X6]:![X9]:(((((((((g_false_only(esk5_1(X5),X5)|(g_both(esk5_1(X5),X5)|g_true_only(esk5_1(X5),X5)))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,esk6_0)|g_true_only(X9,esk6_0)))|epred1_0)&(((((g_true_only(esk5_1(X5),esk5_1(X5))|g_both(esk5_1(X5),esk5_1(X5)))|(g_both(esk5_1(X5),X5)|g_true_only(esk5_1(X5),X5)))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,esk6_0)|g_true_only(X9,esk6_0)))|epred1_0))&(((((g_false_only(esk5_1(X5),X5)|((g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))|g_true_only(esk5_1(X5),X5)))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,esk6_0)|g_true_only(X9,esk6_0)))|epred1_0)&(((((g_true_only(esk5_1(X5),esk5_1(X5))|g_both(esk5_1(X5),esk5_1(X5)))|((g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))|g_true_only(esk5_1(X5),X5)))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,esk6_0)|g_true_only(X9,esk6_0)))|epred1_0)))&((((((g_false_only(esk5_1(X5),X5)|(g_both(esk5_1(X5),X5)|(g_both(esk5_1(X5),esk5_1(X5))
% |g_false_only(esk5_1(X5),esk5_1(X5)))))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,esk6_0)|g_true_only(X9,esk6_0)))|epred1_0)&(((((g_true_only(esk5_1(X5),esk5_1(X5))|g_both(esk5_1(X5),esk5_1(X5)))|(g_both(esk5_1(X5),X5)|(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,esk6_0)|g_true_only(X9,esk6_0)))|epred1_0))&(((((g_false_only(esk5_1(X5),X5)|((g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))|(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,esk6_0)|g_true_only(X9,esk6_0)))|epred1_0)&(((((g_true_only(esk5_1(X5),esk5_1(X5))|g_both(esk5_1(X5),esk5_1(X5)))|((g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))|(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,esk6_0)|g_true_only(X9,esk6_0)))|epred1_0))))&(((((((g_false_only(esk5_1(X5),X5)|(
% g_both(esk5_1(X5),X5)|g_true_only(esk5_1(X5),X5)))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,X9)|g_true_only(X9,esk6_0)))|epred1_0)&(((((g_true_only(esk5_1(X5),esk5_1(X5))|g_both(esk5_1(X5),esk5_1(X5)))|(g_both(esk5_1(X5),X5)|g_true_only(esk5_1(X5),X5)))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,X9)|g_true_only(X9,esk6_0)))|epred1_0))&(((((g_false_only(esk5_1(X5),X5)|((g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))|g_true_only(esk5_1(X5),X5)))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,X9)|g_true_only(X9,esk6_0)))|epred1_0)&(((((g_true_only(esk5_1(X5),esk5_1(X5))|g_both(esk5_1(X5),esk5_1(X5)))|((g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))|g_true_only(esk5_1(X5),X5)))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,X9)|g_true_only(X9,esk6_0)))|epred1_0)))&((((((g_false_only(esk5_1(X5),X5)|(g_both(esk5_1(X5),X5)|(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(
% g_false_only(X9,X9)|g_true_only(X9,esk6_0)))|epred1_0)&(((((g_true_only(esk5_1(X5),esk5_1(X5))|g_both(esk5_1(X5),esk5_1(X5)))|(g_both(esk5_1(X5),X5)|(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,X9)|g_true_only(X9,esk6_0)))|epred1_0))&(((((g_false_only(esk5_1(X5),X5)|((g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))|(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,X9)|g_true_only(X9,esk6_0)))|epred1_0)&(((((g_true_only(esk5_1(X5),esk5_1(X5))|g_both(esk5_1(X5),esk5_1(X5)))|((g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))|(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,X9)|g_true_only(X9,esk6_0)))|epred1_0)))))&((((((((g_false_only(esk5_1(X5),X5)|(g_both(esk5_1(X5),X5)|g_true_only(esk5_1(X5),X5)))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_f
% alse_only(X9,esk6_0)|g_true_only(X9,X9)))|epred1_0)&(((((g_true_only(esk5_1(X5),esk5_1(X5))|g_both(esk5_1(X5),esk5_1(X5)))|(g_both(esk5_1(X5),X5)|g_true_only(esk5_1(X5),X5)))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,esk6_0)|g_true_only(X9,X9)))|epred1_0))&(((((g_false_only(esk5_1(X5),X5)|((g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))|g_true_only(esk5_1(X5),X5)))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,esk6_0)|g_true_only(X9,X9)))|epred1_0)&(((((g_true_only(esk5_1(X5),esk5_1(X5))|g_both(esk5_1(X5),esk5_1(X5)))|((g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))|g_true_only(esk5_1(X5),X5)))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,esk6_0)|g_true_only(X9,X9)))|epred1_0)))&((((((g_false_only(esk5_1(X5),X5)|(g_both(esk5_1(X5),X5)|(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,esk6_0)|g_true_only(X9,X9)))|epred1_0)&(((((g_true_only(esk5_1(X5),esk5_1(X5
% ))|g_both(esk5_1(X5),esk5_1(X5)))|(g_both(esk5_1(X5),X5)|(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,esk6_0)|g_true_only(X9,X9)))|epred1_0))&(((((g_false_only(esk5_1(X5),X5)|((g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))|(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,esk6_0)|g_true_only(X9,X9)))|epred1_0)&(((((g_true_only(esk5_1(X5),esk5_1(X5))|g_both(esk5_1(X5),esk5_1(X5)))|((g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))|(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,esk6_0)|g_true_only(X9,X9)))|epred1_0))))&(((((((g_false_only(esk5_1(X5),X5)|(g_both(esk5_1(X5),X5)|g_true_only(esk5_1(X5),X5)))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,X9)|g_true_only(X9,X9)))|epred1_0)&(((((g_true_only(esk5_1(X5),esk5_1(X5))|g_both
% (esk5_1(X5),esk5_1(X5)))|(g_both(esk5_1(X5),X5)|g_true_only(esk5_1(X5),X5)))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,X9)|g_true_only(X9,X9)))|epred1_0))&(((((g_false_only(esk5_1(X5),X5)|((g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))|g_true_only(esk5_1(X5),X5)))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,X9)|g_true_only(X9,X9)))|epred1_0)&(((((g_true_only(esk5_1(X5),esk5_1(X5))|g_both(esk5_1(X5),esk5_1(X5)))|((g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))|g_true_only(esk5_1(X5),X5)))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,X9)|g_true_only(X9,X9)))|epred1_0)))&((((((g_false_only(esk5_1(X5),X5)|(g_both(esk5_1(X5),X5)|(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,X9)|g_true_only(X9,X9)))|epred1_0)&(((((g_true_only(esk5_1(X5),esk5_1(X5))|g_both(esk5_1(X5),esk5_1(X5)))|(g_both(esk5_1(X5),X5)|(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),es
% k5_1(X5)))))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,X9)|g_true_only(X9,X9)))|epred1_0))&(((((g_false_only(esk5_1(X5),X5)|((g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))|(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,X9)|g_true_only(X9,X9)))|epred1_0)&(((((g_true_only(esk5_1(X5),esk5_1(X5))|g_both(esk5_1(X5),esk5_1(X5)))|((g_true_only(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))|(g_both(esk5_1(X5),esk5_1(X5))|g_false_only(esk5_1(X5),esk5_1(X5)))))|(~(g_both(X6,X5))|~(g_both(X6,X6))))|(g_false_only(X9,X9)|g_true_only(X9,X9)))|epred1_0)))))),inference(distribute,[status(thm)],[60])).
% 0.06/0.44 cnf(67,plain,(epred1_0|g_true_only(X1,X1)|g_false_only(X1,X1)|g_true_only(esk5_1(X3),X3)|g_false_only(esk5_1(X3),esk5_1(X3))|g_true_only(esk5_1(X3),esk5_1(X3))|g_false_only(esk5_1(X3),X3)|~g_both(X2,X2)|~g_both(X2,X3)),inference(split_conjunct,[status(thm)],[61])).
% 0.06/0.44 cnf(68,plain,(epred1_0|g_true_only(X1,X1)|g_false_only(X1,X1)|g_true_only(esk5_1(X3),X3)|g_both(esk5_1(X3),X3)|g_both(esk5_1(X3),esk5_1(X3))|g_true_only(esk5_1(X3),esk5_1(X3))|~g_both(X2,X2)|~g_both(X2,X3)),inference(split_conjunct,[status(thm)],[61])).
% 0.06/0.44 cnf(73,plain,(epred1_0|g_true_only(X1,X1)|g_false_only(X1,esk6_0)|g_false_only(esk5_1(X3),esk5_1(X3))|g_both(esk5_1(X3),esk5_1(X3))|g_both(esk5_1(X3),X3)|g_false_only(esk5_1(X3),X3)|~g_both(X2,X2)|~g_both(X2,X3)),inference(split_conjunct,[status(thm)],[61])).
% 0.06/0.44 cnf(81,plain,(epred1_0|g_true_only(X1,esk6_0)|g_false_only(X1,X1)|g_false_only(esk5_1(X3),esk5_1(X3))|g_both(esk5_1(X3),esk5_1(X3))|g_both(esk5_1(X3),X3)|g_false_only(esk5_1(X3),X3)|~g_both(X2,X2)|~g_both(X2,X3)),inference(split_conjunct,[status(thm)],[61])).
% 0.06/0.44 fof(94, plain,(![X4]:(![X3]:(![X5]:(~(g_both(X5,X3))|~(g_both(X5,X4)))|?[X5]:(((g_true_only(X5,X3)&(g_both(X5,X4)|g_true_only(X5,X4)))|(g_both(X5,X3)&(g_false_only(X5,X4)|g_true_only(X5,X4))))|(g_false_only(X5,X3)&(g_false_only(X5,X4)|g_both(X5,X4)))))|?[X3]:![X5]:((g_true_only(X5,X3)&g_false_only(X5,X4))|(g_false_only(X5,X3)&g_true_only(X5,X4))))|epred2_0),inference(fof_nnf,[status(thm)],[10])).
% 0.06/0.44 fof(95, plain,(![X6]:(![X7]:(![X8]:(~(g_both(X8,X7))|~(g_both(X8,X6)))|?[X9]:(((g_true_only(X9,X7)&(g_both(X9,X6)|g_true_only(X9,X6)))|(g_both(X9,X7)&(g_false_only(X9,X6)|g_true_only(X9,X6))))|(g_false_only(X9,X7)&(g_false_only(X9,X6)|g_both(X9,X6)))))|?[X10]:![X11]:((g_true_only(X11,X10)&g_false_only(X11,X6))|(g_false_only(X11,X10)&g_true_only(X11,X6))))|epred2_0),inference(variable_rename,[status(thm)],[94])).
% 0.06/0.44 fof(96, plain,(![X6]:(![X7]:(![X8]:(~(g_both(X8,X7))|~(g_both(X8,X6)))|(((g_true_only(esk7_2(X6,X7),X7)&(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6)))|(g_both(esk7_2(X6,X7),X7)&(g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(g_false_only(esk7_2(X6,X7),X7)&(g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6)))))|![X11]:((g_true_only(X11,esk8_1(X6))&g_false_only(X11,X6))|(g_false_only(X11,esk8_1(X6))&g_true_only(X11,X6))))|epred2_0),inference(skolemize,[status(esa)],[95])).
% 0.06/0.44 fof(97, plain,![X6]:![X7]:![X8]:![X11]:((((g_true_only(X11,esk8_1(X6))&g_false_only(X11,X6))|(g_false_only(X11,esk8_1(X6))&g_true_only(X11,X6)))|((~(g_both(X8,X7))|~(g_both(X8,X6)))|(((g_true_only(esk7_2(X6,X7),X7)&(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6)))|(g_both(esk7_2(X6,X7),X7)&(g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(g_false_only(esk7_2(X6,X7),X7)&(g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))))))|epred2_0),inference(shift_quantors,[status(thm)],[96])).
% 0.06/0.44 fof(98,
% plain,![X6]:![X7]:![X8]:![X11]:(((((((((g_false_only(esk7_2(X6,X7),X7)|(g_both(esk7_2(X6,X7),X7)|g_true_only(esk7_2(X6,X7),X7)))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_false_only(X11,esk8_1(X6))|g_true_only(X11,esk8_1(X6))))|epred2_0)&(((((g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))|(g_both(esk7_2(X6,X7),X7)|g_true_only(esk7_2(X6,X7),X7)))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_false_only(X11,esk8_1(X6))|g_true_only(X11,esk8_1(X6))))|epred2_0))&(((((g_false_only(esk7_2(X6,X7),X7)|((g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))|g_true_only(esk7_2(X6,X7),X7)))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_false_only(X11,esk8_1(X6))|g_true_only(X11,esk8_1(X6))))|epred2_0)&(((((g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))|((g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))|g_true_only(esk7_2(X6,X7),X7)))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_false_only(X11,esk8_1(X6))|g_true_only(X11,esk8_1(X6))))|epred2_0)))&((((((g_false_only(esk7_2(X6,X7),X7)|(g_both(esk7_2(X6
% ,X7),X7)|(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_false_only(X11,esk8_1(X6))|g_true_only(X11,esk8_1(X6))))|epred2_0)&(((((g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))|(g_both(esk7_2(X6,X7),X7)|(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_false_only(X11,esk8_1(X6))|g_true_only(X11,esk8_1(X6))))|epred2_0))&(((((g_false_only(esk7_2(X6,X7),X7)|((g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))|(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_false_only(X11,esk8_1(X6))|g_true_only(X11,esk8_1(X6))))|epred2_0)&(((((g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))|((g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))|(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_false_only(X11,esk8_1(X6))|g_true_only(X11,esk8_1(X6))))|epred2_0))))&(((((((g_false_only(esk7_2(X6,X7)
% ,X7)|(g_both(esk7_2(X6,X7),X7)|g_true_only(esk7_2(X6,X7),X7)))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_true_only(X11,X6)|g_true_only(X11,esk8_1(X6))))|epred2_0)&(((((g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))|(g_both(esk7_2(X6,X7),X7)|g_true_only(esk7_2(X6,X7),X7)))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_true_only(X11,X6)|g_true_only(X11,esk8_1(X6))))|epred2_0))&(((((g_false_only(esk7_2(X6,X7),X7)|((g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))|g_true_only(esk7_2(X6,X7),X7)))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_true_only(X11,X6)|g_true_only(X11,esk8_1(X6))))|epred2_0)&(((((g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))|((g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))|g_true_only(esk7_2(X6,X7),X7)))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_true_only(X11,X6)|g_true_only(X11,esk8_1(X6))))|epred2_0)))&((((((g_false_only(esk7_2(X6,X7),X7)|(g_both(esk7_2(X6,X7),X7)|(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(~(g_both(X8,X7))|~(g_both(X8,X6))
% ))|(g_true_only(X11,X6)|g_true_only(X11,esk8_1(X6))))|epred2_0)&(((((g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))|(g_both(esk7_2(X6,X7),X7)|(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_true_only(X11,X6)|g_true_only(X11,esk8_1(X6))))|epred2_0))&(((((g_false_only(esk7_2(X6,X7),X7)|((g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))|(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_true_only(X11,X6)|g_true_only(X11,esk8_1(X6))))|epred2_0)&(((((g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))|((g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))|(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_true_only(X11,X6)|g_true_only(X11,esk8_1(X6))))|epred2_0)))))&((((((((g_false_only(esk7_2(X6,X7),X7)|(g_both(esk7_2(X6,X7),X7)|g_true_only(esk7_2(X6,X7),X7)))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_false_only(X11,esk8_1(X6))|g_fals
% e_only(X11,X6)))|epred2_0)&(((((g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))|(g_both(esk7_2(X6,X7),X7)|g_true_only(esk7_2(X6,X7),X7)))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_false_only(X11,esk8_1(X6))|g_false_only(X11,X6)))|epred2_0))&(((((g_false_only(esk7_2(X6,X7),X7)|((g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))|g_true_only(esk7_2(X6,X7),X7)))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_false_only(X11,esk8_1(X6))|g_false_only(X11,X6)))|epred2_0)&(((((g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))|((g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))|g_true_only(esk7_2(X6,X7),X7)))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_false_only(X11,esk8_1(X6))|g_false_only(X11,X6)))|epred2_0)))&((((((g_false_only(esk7_2(X6,X7),X7)|(g_both(esk7_2(X6,X7),X7)|(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_false_only(X11,esk8_1(X6))|g_false_only(X11,X6)))|epred2_0)&(((((g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))|
% (g_both(esk7_2(X6,X7),X7)|(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_false_only(X11,esk8_1(X6))|g_false_only(X11,X6)))|epred2_0))&(((((g_false_only(esk7_2(X6,X7),X7)|((g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))|(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_false_only(X11,esk8_1(X6))|g_false_only(X11,X6)))|epred2_0)&(((((g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))|((g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))|(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_false_only(X11,esk8_1(X6))|g_false_only(X11,X6)))|epred2_0))))&(((((((g_false_only(esk7_2(X6,X7),X7)|(g_both(esk7_2(X6,X7),X7)|g_true_only(esk7_2(X6,X7),X7)))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_true_only(X11,X6)|g_false_only(X11,X6)))|epred2_0)&(((((g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))|(g_both(esk7_2(X6,X7),X7)|g_true_only(esk7
% _2(X6,X7),X7)))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_true_only(X11,X6)|g_false_only(X11,X6)))|epred2_0))&(((((g_false_only(esk7_2(X6,X7),X7)|((g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))|g_true_only(esk7_2(X6,X7),X7)))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_true_only(X11,X6)|g_false_only(X11,X6)))|epred2_0)&(((((g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))|((g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))|g_true_only(esk7_2(X6,X7),X7)))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_true_only(X11,X6)|g_false_only(X11,X6)))|epred2_0)))&((((((g_false_only(esk7_2(X6,X7),X7)|(g_both(esk7_2(X6,X7),X7)|(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_true_only(X11,X6)|g_false_only(X11,X6)))|epred2_0)&(((((g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))|(g_both(esk7_2(X6,X7),X7)|(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_true_only(X11,X6)|g_false_only(X11,X6)))|e
% pred2_0))&(((((g_false_only(esk7_2(X6,X7),X7)|((g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))|(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_true_only(X11,X6)|g_false_only(X11,X6)))|epred2_0)&(((((g_false_only(esk7_2(X6,X7),X6)|g_both(esk7_2(X6,X7),X6))|((g_false_only(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))|(g_both(esk7_2(X6,X7),X6)|g_true_only(esk7_2(X6,X7),X6))))|(~(g_both(X8,X7))|~(g_both(X8,X6))))|(g_true_only(X11,X6)|g_false_only(X11,X6)))|epred2_0)))))),inference(distribute,[status(thm)],[97])).
% 0.06/0.44 cnf(102,plain,(epred2_0|g_false_only(X1,X2)|g_true_only(X1,X2)|g_true_only(esk7_2(X2,X4),X2)|g_both(esk7_2(X2,X4),X2)|g_both(esk7_2(X2,X4),X4)|g_false_only(esk7_2(X2,X4),X4)|~g_both(X3,X2)|~g_both(X3,X4)),inference(split_conjunct,[status(thm)],[98])).
% 0.06/0.44 cnf(104,plain,(epred2_0|g_false_only(X1,X2)|g_true_only(X1,X2)|g_true_only(esk7_2(X2,X4),X4)|g_true_only(esk7_2(X2,X4),X2)|g_false_only(esk7_2(X2,X4),X2)|g_false_only(esk7_2(X2,X4),X4)|~g_both(X3,X2)|~g_both(X3,X4)),inference(split_conjunct,[status(thm)],[98])).
% 0.06/0.44 cnf(105,plain,(epred2_0|g_false_only(X1,X2)|g_true_only(X1,X2)|g_true_only(esk7_2(X2,X4),X4)|g_both(esk7_2(X2,X4),X4)|g_both(esk7_2(X2,X4),X2)|g_false_only(esk7_2(X2,X4),X2)|~g_both(X3,X2)|~g_both(X3,X4)),inference(split_conjunct,[status(thm)],[98])).
% 0.06/0.44 cnf(131,negated_conjecture,(g_both(X1,X1)|g_true_only(X1,X1)|~g_true_only(X1,esk1_0)),inference(spm,[status(thm)],[35,25,theory(equality)])).
% 0.06/0.44 cnf(132,negated_conjecture,(g_both(X1,X1)|g_true_only(X1,X1)|~g_both(X1,esk1_0)),inference(spm,[status(thm)],[33,25,theory(equality)])).
% 0.06/0.44 cnf(133,negated_conjecture,(g_both(X1,esk1_0)|g_true_only(X1,esk1_0)|~g_true_only(X1,X1)),inference(spm,[status(thm)],[32,25,theory(equality)])).
% 0.06/0.44 cnf(135,negated_conjecture,(g_both(X1,esk2_1(X2))|g_true_only(X1,esk2_1(X2))|~g_false_only(X1,X2)),inference(spm,[status(thm)],[38,25,theory(equality)])).
% 0.06/0.44 cnf(140,plain,(~g_false_only(X1,X2)|~g_true_only(X1,X2)),inference(spm,[status(thm)],[16,23,theory(equality)])).
% 0.06/0.44 cnf(141,plain,(~g_false_only(X1,X2)|~g_both(X1,X2)),inference(spm,[status(thm)],[16,56,theory(equality)])).
% 0.06/0.44 cnf(143,plain,(~g_true_only(X1,X2)|~g_both(X1,X2)),inference(spm,[status(thm)],[22,55,theory(equality)])).
% 0.06/0.44 cnf(144,negated_conjecture,(g_both(X1,esk2_1(X2))|g_true_only(X1,esk2_1(X2))|~g_both(X1,X2)),inference(spm,[status(thm)],[37,25,theory(equality)])).
% 0.06/0.44 cnf(163,negated_conjecture,(g_both(esk4_1(esk2_1(X1)),esk3_0)|g_both(esk4_1(esk2_1(X1)),esk2_1(X1))|g_true_only(esk4_1(esk2_1(X1)),esk3_0)|~g_false_only(esk4_1(esk2_1(X1)),X1)|~epred2_0|~epred1_0),inference(spm,[status(thm)],[38,46,theory(equality)])).
% 0.06/0.44 cnf(389,negated_conjecture,(g_both(X1,X1)|~g_both(X1,esk1_0)),inference(csr,[status(thm)],[132,34])).
% 0.06/0.44 cnf(390,negated_conjecture,(g_true_only(X1,esk1_0)|~g_true_only(X1,X1)),inference(csr,[status(thm)],[133,34])).
% 0.06/0.44 cnf(394,negated_conjecture,(g_true_only(X1,X1)|~g_true_only(X1,esk1_0)),inference(csr,[status(thm)],[131,36])).
% 0.06/0.44 cnf(397,negated_conjecture,(g_true_only(X1,esk2_1(X2))|~g_false_only(X1,X2)),inference(csr,[status(thm)],[135,40])).
% 0.06/0.44 cnf(401,negated_conjecture,(g_true_only(esk2_1(X1),esk1_0)|~g_false_only(esk2_1(X1),X1)),inference(spm,[status(thm)],[390,397,theory(equality)])).
% 0.06/0.44 cnf(403,negated_conjecture,(g_true_only(esk2_1(X1),esk1_0)|g_both(esk2_1(X1),X1)|g_true_only(esk2_1(X1),X1)),inference(spm,[status(thm)],[401,25,theory(equality)])).
% 0.06/0.44 cnf(404,negated_conjecture,(g_both(esk2_1(esk1_0),esk1_0)|g_true_only(esk2_1(esk1_0),esk1_0)),inference(ef,[status(thm)],[403,theory(equality)])).
% 0.06/0.44 cnf(407,negated_conjecture,(g_both(esk2_1(esk2_1(X1)),esk2_1(X1))|g_true_only(esk2_1(esk2_1(X1)),esk1_0)|~g_true_only(esk2_1(esk2_1(X1)),X1)),inference(spm,[status(thm)],[41,403,theory(equality)])).
% 0.06/0.44 cnf(413,negated_conjecture,(g_true_only(esk2_1(esk1_0),esk2_1(esk1_0))|g_both(esk2_1(esk1_0),esk1_0)),inference(spm,[status(thm)],[394,404,theory(equality)])).
% 0.06/0.44 cnf(415,negated_conjecture,(g_both(X1,esk2_1(X2))|~g_both(X1,X2)),inference(csr,[status(thm)],[144,42])).
% 0.06/0.44 cnf(444,negated_conjecture,(g_both(esk2_1(esk1_0),esk1_0)|~g_true_only(esk2_1(esk1_0),esk1_0)),inference(spm,[status(thm)],[41,413,theory(equality)])).
% 0.06/0.44 cnf(450,negated_conjecture,(g_both(esk2_1(esk1_0),esk1_0)),inference(csr,[status(thm)],[444,404])).
% 0.06/0.44 cnf(452,negated_conjecture,(epred1_0|g_true_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_true_only(esk5_1(esk1_0),esk1_0)|g_true_only(X1,X1)|g_false_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,X1)|~g_both(esk2_1(esk1_0),esk2_1(esk1_0))),inference(spm,[status(thm)],[67,450,theory(equality)])).
% 0.06/0.44 cnf(457,negated_conjecture,(epred1_0|g_both(esk5_1(esk1_0),esk5_1(esk1_0))|g_both(esk5_1(esk1_0),esk1_0)|g_true_only(X1,esk6_0)|g_false_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,X1)|~g_both(esk2_1(esk1_0),esk2_1(esk1_0))),inference(spm,[status(thm)],[81,450,theory(equality)])).
% 0.06/0.44 cnf(459,negated_conjecture,(epred1_0|g_both(esk5_1(esk1_0),esk5_1(esk1_0))|g_both(esk5_1(esk1_0),esk1_0)|g_true_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_true_only(esk5_1(esk1_0),esk1_0)|g_true_only(X1,X1)|g_false_only(X1,X1)|~g_both(esk2_1(esk1_0),esk2_1(esk1_0))),inference(spm,[status(thm)],[68,450,theory(equality)])).
% 0.06/0.44 cnf(463,negated_conjecture,(epred1_0|g_both(esk5_1(esk1_0),esk5_1(esk1_0))|g_both(esk5_1(esk1_0),esk1_0)|g_true_only(X1,X1)|g_false_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,esk6_0)|~g_both(esk2_1(esk1_0),esk2_1(esk1_0))),inference(spm,[status(thm)],[73,450,theory(equality)])).
% 0.06/0.44 cnf(475,negated_conjecture,(g_both(esk2_1(esk1_0),esk2_1(esk1_0))),inference(spm,[status(thm)],[389,450,theory(equality)])).
% 0.06/0.44 cnf(489,negated_conjecture,(epred2_0|g_true_only(esk7_2(X1,esk2_1(esk1_0)),X1)|g_true_only(esk7_2(X1,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(X2,X1)|g_false_only(esk7_2(X1,esk2_1(esk1_0)),X1)|g_false_only(esk7_2(X1,esk2_1(esk1_0)),esk2_1(esk1_0))|g_false_only(X2,X1)|~g_both(esk2_1(esk1_0),X1)),inference(spm,[status(thm)],[104,475,theory(equality)])).
% 0.06/0.44 cnf(490,negated_conjecture,(epred2_0|g_both(esk7_2(X1,esk2_1(esk1_0)),X1)|g_both(esk7_2(X1,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(esk7_2(X1,esk2_1(esk1_0)),X1)|g_true_only(X2,X1)|g_false_only(esk7_2(X1,esk2_1(esk1_0)),esk2_1(esk1_0))|g_false_only(X2,X1)|~g_both(esk2_1(esk1_0),X1)),inference(spm,[status(thm)],[102,475,theory(equality)])).
% 0.06/0.44 cnf(494,negated_conjecture,(epred2_0|g_both(esk7_2(X1,esk2_1(esk1_0)),X1)|g_both(esk7_2(X1,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(esk7_2(X1,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(X2,X1)|g_false_only(esk7_2(X1,esk2_1(esk1_0)),X1)|g_false_only(X2,X1)|~g_both(esk2_1(esk1_0),X1)),inference(spm,[status(thm)],[105,475,theory(equality)])).
% 0.06/0.44 cnf(570,negated_conjecture,(g_both(esk4_1(esk2_1(X1)),esk3_0)|g_true_only(esk4_1(esk2_1(X1)),esk3_0)|~epred2_0|~epred1_0|~g_false_only(esk4_1(esk2_1(X1)),X1)),inference(csr,[status(thm)],[163,40])).
% 0.06/0.44 cnf(571,negated_conjecture,(g_both(esk4_1(esk2_1(X1)),esk3_0)|g_true_only(esk4_1(esk2_1(X1)),esk3_0)|g_both(esk4_1(esk2_1(X1)),X1)|g_true_only(esk4_1(esk2_1(X1)),X1)|~epred2_0|~epred1_0),inference(spm,[status(thm)],[570,25,theory(equality)])).
% 0.06/0.44 cnf(573,negated_conjecture,(g_true_only(esk2_1(esk2_1(X1)),esk1_0)|~g_true_only(esk2_1(esk2_1(X1)),X1)),inference(csr,[status(thm)],[407,39])).
% 0.06/0.44 cnf(574,negated_conjecture,(g_true_only(esk2_1(esk2_1(esk2_1(X1))),esk1_0)|~g_false_only(esk2_1(esk2_1(esk2_1(X1))),X1)),inference(spm,[status(thm)],[573,397,theory(equality)])).
% 0.06/0.44 cnf(575,negated_conjecture,(g_true_only(esk2_1(esk2_1(esk2_1(X1))),esk1_0)|g_both(esk2_1(esk2_1(esk2_1(X1))),X1)|g_true_only(esk2_1(esk2_1(esk2_1(X1))),X1)),inference(spm,[status(thm)],[574,25,theory(equality)])).
% 0.06/0.44 cnf(576,negated_conjecture,(g_both(esk2_1(esk2_1(esk2_1(esk1_0))),esk1_0)|g_true_only(esk2_1(esk2_1(esk2_1(esk1_0))),esk1_0)),inference(ef,[status(thm)],[575,theory(equality)])).
% 0.06/0.44 cnf(585,negated_conjecture,(g_true_only(esk2_1(esk2_1(esk2_1(esk1_0))),esk2_1(esk2_1(esk2_1(esk1_0))))|g_both(esk2_1(esk2_1(esk2_1(esk1_0))),esk1_0)),inference(spm,[status(thm)],[394,576,theory(equality)])).
% 0.06/0.44 cnf(588,negated_conjecture,(g_both(esk2_1(esk2_1(esk2_1(esk1_0))),esk1_0)|~g_true_only(esk2_1(esk2_1(esk2_1(esk1_0))),esk2_1(esk2_1(esk1_0)))),inference(spm,[status(thm)],[41,585,theory(equality)])).
% 0.06/0.44 cnf(596,negated_conjecture,(g_both(esk2_1(esk2_1(esk2_1(esk1_0))),esk1_0)|~g_false_only(esk2_1(esk2_1(esk2_1(esk1_0))),esk2_1(esk1_0))),inference(spm,[status(thm)],[588,397,theory(equality)])).
% 0.06/0.44 cnf(599,negated_conjecture,(~g_false_only(esk2_1(esk2_1(esk2_1(esk1_0))),esk2_1(esk1_0))),inference(csr,[status(thm)],[596,37])).
% 0.06/0.44 cnf(600,negated_conjecture,(g_both(esk2_1(esk2_1(esk2_1(esk1_0))),esk2_1(esk1_0))|g_true_only(esk2_1(esk2_1(esk2_1(esk1_0))),esk2_1(esk1_0))),inference(spm,[status(thm)],[599,25,theory(equality)])).
% 0.06/0.44 cnf(601,negated_conjecture,(g_both(esk2_1(esk2_1(esk2_1(esk1_0))),esk2_1(esk1_0))|~g_true_only(esk2_1(esk2_1(esk2_1(esk1_0))),esk1_0)),inference(spm,[status(thm)],[41,600,theory(equality)])).
% 0.06/0.44 cnf(604,negated_conjecture,(g_true_only(esk2_1(esk2_1(esk2_1(esk1_0))),esk1_0)|g_both(esk2_1(esk2_1(esk2_1(esk1_0))),esk2_1(esk1_0))),inference(spm,[status(thm)],[573,600,theory(equality)])).
% 0.06/0.44 cnf(605,negated_conjecture,(g_true_only(esk2_1(esk2_1(esk2_1(esk1_0))),esk1_0)|~g_false_only(esk2_1(esk2_1(esk2_1(esk1_0))),esk1_0)),inference(spm,[status(thm)],[40,604,theory(equality)])).
% 0.06/0.44 cnf(632,negated_conjecture,(~g_false_only(esk2_1(esk2_1(esk2_1(esk1_0))),esk1_0)),inference(csr,[status(thm)],[605,140])).
% 0.06/0.44 cnf(634,negated_conjecture,(g_both(esk2_1(esk2_1(esk2_1(esk1_0))),esk2_1(esk1_0))),inference(csr,[status(thm)],[601,604])).
% 0.06/0.44 cnf(636,negated_conjecture,(~g_true_only(esk2_1(esk2_1(esk2_1(esk1_0))),esk1_0)),inference(spm,[status(thm)],[39,634,theory(equality)])).
% 0.06/0.44 cnf(2503,negated_conjecture,(epred1_0|g_true_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_true_only(esk5_1(esk1_0),esk1_0)|g_true_only(X1,X1)|g_false_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,X1)|$false),inference(rw,[status(thm)],[452,475,theory(equality)])).
% 0.06/0.44 cnf(2504,negated_conjecture,(epred1_0|g_true_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_true_only(esk5_1(esk1_0),esk1_0)|g_true_only(X1,X1)|g_false_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,X1)),inference(cn,[status(thm)],[2503,theory(equality)])).
% 0.06/0.44 cnf(2505,negated_conjecture,(epred1_0|g_true_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_true_only(X1,X1)|g_false_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,X1)),inference(csr,[status(thm)],[2504,394])).
% 0.06/0.44 cnf(2506,negated_conjecture,(epred1_0|g_true_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(esk5_1(esk1_0),esk5_1(esk1_0))),inference(ef,[status(thm)],[2505,theory(equality)])).
% 0.06/0.44 cnf(2546,negated_conjecture,(epred1_0|g_true_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_false_only(esk5_1(esk1_0),esk1_0)|~g_both(esk5_1(esk1_0),esk5_1(esk1_0))),inference(spm,[status(thm)],[141,2506,theory(equality)])).
% 0.06/0.44 cnf(2551,negated_conjecture,(epred1_0|g_true_only(esk5_1(esk1_0),esk5_1(esk1_0))|~g_both(esk5_1(esk1_0),esk5_1(esk1_0))),inference(csr,[status(thm)],[2546,31])).
% 0.06/0.44 cnf(2552,negated_conjecture,(epred1_0|~g_both(esk5_1(esk1_0),esk5_1(esk1_0))),inference(csr,[status(thm)],[2551,143])).
% 0.06/0.44 cnf(2675,negated_conjecture,(epred1_0|g_both(esk5_1(esk1_0),esk5_1(esk1_0))|g_both(esk5_1(esk1_0),esk1_0)|g_true_only(X1,esk6_0)|g_false_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,X1)|$false),inference(rw,[status(thm)],[457,475,theory(equality)])).
% 0.06/0.44 cnf(2676,negated_conjecture,(epred1_0|g_both(esk5_1(esk1_0),esk5_1(esk1_0))|g_both(esk5_1(esk1_0),esk1_0)|g_true_only(X1,esk6_0)|g_false_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,X1)),inference(cn,[status(thm)],[2675,theory(equality)])).
% 0.06/0.44 cnf(2677,negated_conjecture,(epred1_0|g_both(esk5_1(esk1_0),esk5_1(esk1_0))|g_true_only(X1,esk6_0)|g_false_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,X1)),inference(csr,[status(thm)],[2676,389])).
% 0.06/0.44 cnf(2678,negated_conjecture,(epred1_0|g_true_only(X1,esk6_0)|g_false_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,X1)),inference(csr,[status(thm)],[2677,2552])).
% 0.06/0.44 cnf(2681,negated_conjecture,(epred1_0|g_true_only(X1,esk6_0)|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,X1)|~g_true_only(esk5_1(esk1_0),esk1_0)),inference(spm,[status(thm)],[35,2678,theory(equality)])).
% 0.06/0.44 cnf(2763,negated_conjecture,(epred1_0|g_both(esk5_1(esk1_0),esk5_1(esk1_0))|g_both(esk5_1(esk1_0),esk1_0)|g_true_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_true_only(esk5_1(esk1_0),esk1_0)|g_true_only(X1,X1)|g_false_only(X1,X1)|$false),inference(rw,[status(thm)],[459,475,theory(equality)])).
% 0.06/0.44 cnf(2764,negated_conjecture,(epred1_0|g_both(esk5_1(esk1_0),esk5_1(esk1_0))|g_both(esk5_1(esk1_0),esk1_0)|g_true_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_true_only(esk5_1(esk1_0),esk1_0)|g_true_only(X1,X1)|g_false_only(X1,X1)),inference(cn,[status(thm)],[2763,theory(equality)])).
% 0.06/0.44 cnf(2765,negated_conjecture,(epred1_0|g_both(esk5_1(esk1_0),esk5_1(esk1_0))|g_both(esk5_1(esk1_0),esk1_0)|g_true_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_true_only(X1,X1)|g_false_only(X1,X1)),inference(csr,[status(thm)],[2764,394])).
% 0.06/0.44 cnf(2766,negated_conjecture,(epred1_0|g_both(esk5_1(esk1_0),esk5_1(esk1_0))|g_true_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_true_only(X1,X1)|g_false_only(X1,X1)),inference(csr,[status(thm)],[2765,389])).
% 0.06/0.44 cnf(2767,negated_conjecture,(epred1_0|g_true_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_true_only(X1,X1)|g_false_only(X1,X1)),inference(csr,[status(thm)],[2766,2552])).
% 0.06/0.44 cnf(2773,negated_conjecture,(g_true_only(esk5_1(esk1_0),esk1_0)|epred1_0|g_true_only(X1,X1)|g_false_only(X1,X1)),inference(spm,[status(thm)],[390,2767,theory(equality)])).
% 0.06/0.44 cnf(2780,negated_conjecture,(epred1_0|g_true_only(esk5_1(esk1_0),esk1_0)|g_true_only(X1,X1)|~g_both(X1,esk1_0)),inference(spm,[status(thm)],[33,2773,theory(equality)])).
% 0.06/0.44 cnf(2803,negated_conjecture,(epred1_0|g_true_only(esk5_1(esk1_0),esk1_0)|~g_both(X1,esk1_0)),inference(csr,[status(thm)],[2780,34])).
% 0.06/0.44 cnf(2804,negated_conjecture,(epred1_0|g_true_only(esk5_1(esk1_0),esk1_0)),inference(spm,[status(thm)],[2803,450,theory(equality)])).
% 0.06/0.44 cnf(2881,negated_conjecture,(epred1_0|g_true_only(X1,esk6_0)|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,X1)),inference(csr,[status(thm)],[2681,2804])).
% 0.06/0.44 cnf(2888,negated_conjecture,(epred1_0|g_true_only(X1,esk6_0)|g_false_only(X1,X1)|~g_true_only(esk5_1(esk1_0),esk1_0)),inference(spm,[status(thm)],[140,2881,theory(equality)])).
% 0.06/0.44 cnf(2923,negated_conjecture,(epred1_0|g_both(esk5_1(esk1_0),esk5_1(esk1_0))|g_both(esk5_1(esk1_0),esk1_0)|g_true_only(X1,X1)|g_false_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,esk6_0)|$false),inference(rw,[status(thm)],[463,475,theory(equality)])).
% 0.06/0.44 cnf(2924,negated_conjecture,(epred1_0|g_both(esk5_1(esk1_0),esk5_1(esk1_0))|g_both(esk5_1(esk1_0),esk1_0)|g_true_only(X1,X1)|g_false_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,esk6_0)),inference(cn,[status(thm)],[2923,theory(equality)])).
% 0.06/0.44 cnf(2925,negated_conjecture,(epred1_0|g_both(esk5_1(esk1_0),esk5_1(esk1_0))|g_true_only(X1,X1)|g_false_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,esk6_0)),inference(csr,[status(thm)],[2924,389])).
% 0.06/0.44 cnf(2926,negated_conjecture,(epred1_0|g_true_only(X1,X1)|g_false_only(esk5_1(esk1_0),esk5_1(esk1_0))|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,esk6_0)),inference(csr,[status(thm)],[2925,2552])).
% 0.06/0.44 cnf(2927,negated_conjecture,(epred1_0|g_true_only(X1,X1)|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,esk6_0)|~g_true_only(esk5_1(esk1_0),esk1_0)),inference(spm,[status(thm)],[35,2926,theory(equality)])).
% 0.06/0.44 cnf(2940,negated_conjecture,(epred1_0|g_true_only(X1,esk6_0)|g_false_only(X1,X1)),inference(csr,[status(thm)],[2888,2804])).
% 0.06/0.44 cnf(2948,negated_conjecture,(epred1_0|g_true_only(X1,esk6_0)|~g_both(X1,X1)),inference(spm,[status(thm)],[141,2940,theory(equality)])).
% 0.06/0.44 cnf(3009,negated_conjecture,(epred1_0|g_true_only(esk2_1(esk1_0),esk6_0)),inference(spm,[status(thm)],[2948,475,theory(equality)])).
% 0.06/0.44 cnf(3146,negated_conjecture,(epred1_0|g_true_only(X1,X1)|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,esk6_0)),inference(csr,[status(thm)],[2927,2804])).
% 0.06/0.44 cnf(3148,negated_conjecture,(epred1_0|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(X1,esk6_0)|~g_both(X1,esk1_0)),inference(spm,[status(thm)],[34,3146,theory(equality)])).
% 0.06/0.44 cnf(3160,negated_conjecture,(epred1_0|g_false_only(esk5_1(esk1_0),esk1_0)|g_false_only(esk2_1(esk1_0),esk6_0)),inference(spm,[status(thm)],[3148,450,theory(equality)])).
% 0.06/0.44 cnf(3164,negated_conjecture,(epred1_0|g_false_only(esk5_1(esk1_0),esk1_0)|~g_true_only(esk2_1(esk1_0),esk6_0)),inference(spm,[status(thm)],[140,3160,theory(equality)])).
% 0.06/0.44 cnf(3168,negated_conjecture,(epred1_0|g_false_only(esk5_1(esk1_0),esk1_0)),inference(csr,[status(thm)],[3164,3009])).
% 0.06/0.44 cnf(3171,negated_conjecture,(epred1_0|~g_true_only(esk5_1(esk1_0),esk1_0)),inference(spm,[status(thm)],[140,3168,theory(equality)])).
% 0.06/0.44 cnf(3185,negated_conjecture,(epred1_0),inference(csr,[status(thm)],[3171,2804])).
% 0.06/0.44 cnf(3225,negated_conjecture,(g_both(esk4_1(esk2_1(X1)),esk3_0)|g_both(esk4_1(esk2_1(X1)),X1)|g_true_only(esk4_1(esk2_1(X1)),esk3_0)|g_true_only(esk4_1(esk2_1(X1)),X1)|~epred2_0|$false),inference(rw,[status(thm)],[571,3185,theory(equality)])).
% 0.06/0.44 cnf(3226,negated_conjecture,(g_both(esk4_1(esk2_1(X1)),esk3_0)|g_both(esk4_1(esk2_1(X1)),X1)|g_true_only(esk4_1(esk2_1(X1)),esk3_0)|g_true_only(esk4_1(esk2_1(X1)),X1)|~epred2_0),inference(cn,[status(thm)],[3225,theory(equality)])).
% 0.06/0.44 cnf(3241,negated_conjecture,(g_both(esk4_1(X1),esk3_0)|g_both(esk4_1(X1),X1)|g_true_only(esk4_1(X1),X1)|g_false_only(esk4_1(X1),esk3_0)|~epred2_0|$false),inference(rw,[status(thm)],[49,3185,theory(equality)])).
% 0.06/0.44 cnf(3242,negated_conjecture,(g_both(esk4_1(X1),esk3_0)|g_both(esk4_1(X1),X1)|g_true_only(esk4_1(X1),X1)|g_false_only(esk4_1(X1),esk3_0)|~epred2_0),inference(cn,[status(thm)],[3241,theory(equality)])).
% 0.06/0.44 cnf(3245,negated_conjecture,(g_true_only(esk4_1(X1),esk3_0)|g_true_only(esk4_1(X1),X1)|g_false_only(esk4_1(X1),esk3_0)|g_false_only(esk4_1(X1),X1)|~epred2_0|$false),inference(rw,[status(thm)],[48,3185,theory(equality)])).
% 0.06/0.44 cnf(3246,negated_conjecture,(g_true_only(esk4_1(X1),esk3_0)|g_true_only(esk4_1(X1),X1)|g_false_only(esk4_1(X1),esk3_0)|g_false_only(esk4_1(X1),X1)|~epred2_0),inference(cn,[status(thm)],[3245,theory(equality)])).
% 0.06/0.44 cnf(3269,negated_conjecture,(epred2_0|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|g_true_only(X1,esk1_0)|g_false_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_false_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|g_false_only(X1,esk1_0)),inference(spm,[status(thm)],[489,450,theory(equality)])).
% 0.06/0.44 cnf(3319,negated_conjecture,(epred2_0|g_both(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_both(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|g_true_only(X1,esk1_0)|g_false_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_false_only(X1,esk1_0)),inference(spm,[status(thm)],[490,450,theory(equality)])).
% 0.06/0.44 cnf(3335,negated_conjecture,(epred2_0|g_both(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_both(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(X1,esk1_0)|g_false_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|g_false_only(X1,esk1_0)),inference(spm,[status(thm)],[494,450,theory(equality)])).
% 0.06/0.44 cnf(3361,negated_conjecture,(epred2_0|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|g_true_only(X1,esk1_0)|g_false_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_false_only(X1,esk1_0)),inference(csr,[status(thm)],[3269,397])).
% 0.06/0.44 cnf(3362,negated_conjecture,(epred2_0|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|g_true_only(esk2_1(esk2_1(esk2_1(esk1_0))),esk1_0)|g_false_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))),inference(spm,[status(thm)],[632,3361,theory(equality)])).
% 0.06/0.44 cnf(3379,negated_conjecture,(epred2_0|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|g_false_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))),inference(sr,[status(thm)],[3362,636,theory(equality)])).
% 0.06/0.44 cnf(3395,negated_conjecture,(epred2_0|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|~g_both(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)),inference(spm,[status(thm)],[37,3379,theory(equality)])).
% 0.06/0.44 cnf(3397,negated_conjecture,(epred2_0|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|~g_both(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))),inference(spm,[status(thm)],[141,3379,theory(equality)])).
% 0.06/0.44 cnf(3400,negated_conjecture,(epred2_0|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|~g_both(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)),inference(csr,[status(thm)],[3395,143])).
% 0.06/0.44 cnf(3401,negated_conjecture,(epred2_0|~g_both(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)),inference(csr,[status(thm)],[3400,42])).
% 0.06/0.44 cnf(3402,negated_conjecture,(epred2_0|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|~g_both(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))),inference(csr,[status(thm)],[3397,39])).
% 0.06/0.44 cnf(3403,negated_conjecture,(epred2_0|~g_both(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))),inference(csr,[status(thm)],[3402,143])).
% 0.06/0.44 cnf(3408,negated_conjecture,(epred2_0|g_both(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|g_true_only(X1,esk1_0)|g_false_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_false_only(X1,esk1_0)),inference(csr,[status(thm)],[3319,415])).
% 0.06/0.44 cnf(3409,negated_conjecture,(epred2_0|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|g_true_only(X1,esk1_0)|g_false_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_false_only(X1,esk1_0)),inference(csr,[status(thm)],[3408,3403])).
% 0.06/0.44 cnf(3410,negated_conjecture,(epred2_0|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|g_true_only(esk2_1(esk2_1(esk2_1(esk1_0))),esk1_0)|g_false_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))),inference(spm,[status(thm)],[632,3409,theory(equality)])).
% 0.06/0.44 cnf(3427,negated_conjecture,(epred2_0|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|g_false_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))),inference(sr,[status(thm)],[3410,636,theory(equality)])).
% 0.06/0.44 cnf(3442,negated_conjecture,(epred2_0|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|~g_false_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)),inference(spm,[status(thm)],[38,3427,theory(equality)])).
% 0.06/0.44 cnf(3446,negated_conjecture,(epred2_0|~g_false_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)),inference(csr,[status(thm)],[3442,140])).
% 0.06/0.44 cnf(3447,negated_conjecture,(epred2_0|g_both(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)),inference(spm,[status(thm)],[3446,25,theory(equality)])).
% 0.06/0.44 cnf(3448,negated_conjecture,(epred2_0|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)),inference(csr,[status(thm)],[3447,3401])).
% 0.06/0.44 cnf(3458,negated_conjecture,(epred2_0|g_both(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_both(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(X1,esk1_0)|g_false_only(X1,esk1_0)),inference(csr,[status(thm)],[3335,397])).
% 0.06/0.44 cnf(3459,negated_conjecture,(epred2_0|g_both(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(X1,esk1_0)|g_false_only(X1,esk1_0)),inference(csr,[status(thm)],[3458,415])).
% 0.06/0.44 cnf(3460,negated_conjecture,(epred2_0|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(X1,esk1_0)|g_false_only(X1,esk1_0)),inference(csr,[status(thm)],[3459,3403])).
% 0.06/0.44 cnf(3461,negated_conjecture,(epred2_0|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))|g_true_only(esk2_1(esk2_1(esk2_1(esk1_0))),esk1_0)),inference(spm,[status(thm)],[632,3460,theory(equality)])).
% 0.06/0.44 cnf(3477,negated_conjecture,(epred2_0|g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk2_1(esk1_0))),inference(sr,[status(thm)],[3461,636,theory(equality)])).
% 0.06/0.44 cnf(3492,negated_conjecture,(epred2_0|~g_true_only(esk7_2(esk1_0,esk2_1(esk1_0)),esk1_0)),inference(spm,[status(thm)],[41,3477,theory(equality)])).
% 0.06/0.44 cnf(3495,negated_conjecture,(epred2_0),inference(csr,[status(thm)],[3492,3448])).
% 0.06/0.44 cnf(3512,negated_conjecture,(g_true_only(esk4_1(X1),esk3_0)|g_true_only(esk4_1(X1),X1)|g_false_only(esk4_1(X1),esk3_0)|g_false_only(esk4_1(X1),X1)|$false),inference(rw,[status(thm)],[3246,3495,theory(equality)])).
% 0.06/0.44 cnf(3513,negated_conjecture,(g_true_only(esk4_1(X1),esk3_0)|g_true_only(esk4_1(X1),X1)|g_false_only(esk4_1(X1),esk3_0)|g_false_only(esk4_1(X1),X1)),inference(cn,[status(thm)],[3512,theory(equality)])).
% 0.06/0.44 cnf(3514,negated_conjecture,(g_both(esk4_1(esk2_1(X1)),esk3_0)|g_both(esk4_1(esk2_1(X1)),X1)|g_true_only(esk4_1(esk2_1(X1)),esk3_0)|g_true_only(esk4_1(esk2_1(X1)),X1)|$false),inference(rw,[status(thm)],[3226,3495,theory(equality)])).
% 0.06/0.44 cnf(3515,negated_conjecture,(g_both(esk4_1(esk2_1(X1)),esk3_0)|g_both(esk4_1(esk2_1(X1)),X1)|g_true_only(esk4_1(esk2_1(X1)),esk3_0)|g_true_only(esk4_1(esk2_1(X1)),X1)),inference(cn,[status(thm)],[3514,theory(equality)])).
% 0.06/0.44 cnf(3516,negated_conjecture,(g_both(esk4_1(X1),esk3_0)|g_both(esk4_1(X1),X1)|g_true_only(esk4_1(X1),X1)|g_false_only(esk4_1(X1),esk3_0)|$false),inference(rw,[status(thm)],[3242,3495,theory(equality)])).
% 0.06/0.44 cnf(3517,negated_conjecture,(g_both(esk4_1(X1),esk3_0)|g_both(esk4_1(X1),X1)|g_true_only(esk4_1(X1),X1)|g_false_only(esk4_1(X1),esk3_0)),inference(cn,[status(thm)],[3516,theory(equality)])).
% 0.06/0.44 cnf(3574,negated_conjecture,(g_true_only(esk4_1(X1),esk3_0)|g_true_only(esk4_1(X1),X1)|g_false_only(esk4_1(X1),X1)|~g_both(esk4_1(X1),esk3_0)),inference(spm,[status(thm)],[141,3513,theory(equality)])).
% 0.06/0.44 cnf(3581,negated_conjecture,(g_both(esk4_1(X1),esk3_0)|g_both(esk4_1(X1),X1)|g_true_only(esk4_1(X1),X1)|~g_true_only(esk4_1(X1),esk3_0)),inference(spm,[status(thm)],[140,3517,theory(equality)])).
% 0.06/0.44 cnf(3595,negated_conjecture,(g_both(esk4_1(esk2_1(esk3_0)),esk3_0)|g_true_only(esk4_1(esk2_1(esk3_0)),esk3_0)),inference(ef,[status(thm)],[3515,theory(equality)])).
% 0.06/0.44 cnf(3604,negated_conjecture,(g_true_only(esk4_1(X1),X1)|g_false_only(esk4_1(X1),X1)|~g_both(esk4_1(X1),esk3_0)),inference(csr,[status(thm)],[3574,143])).
% 0.06/0.44 cnf(3610,negated_conjecture,(g_true_only(esk4_1(X1),X1)|~g_both(esk4_1(X1),X1)|~g_both(esk4_1(X1),esk3_0)),inference(spm,[status(thm)],[141,3604,theory(equality)])).
% 0.06/0.44 cnf(3611,negated_conjecture,(~g_both(esk4_1(X1),esk3_0)|~g_both(esk4_1(X1),X1)),inference(csr,[status(thm)],[3610,143])).
% 0.06/0.44 cnf(3623,negated_conjecture,(g_both(esk4_1(X1),X1)|g_true_only(esk4_1(X1),X1)|~g_true_only(esk4_1(X1),esk3_0)),inference(csr,[status(thm)],[3581,143])).
% 0.06/0.44 cnf(3625,negated_conjecture,(g_both(esk4_1(esk2_1(esk3_0)),esk2_1(esk3_0))|g_true_only(esk4_1(esk2_1(esk3_0)),esk2_1(esk3_0))|g_both(esk4_1(esk2_1(esk3_0)),esk3_0)),inference(spm,[status(thm)],[3623,3595,theory(equality)])).
% 0.06/0.44 cnf(3626,negated_conjecture,(g_both(esk4_1(esk2_1(esk3_0)),esk2_1(esk3_0))|g_true_only(esk4_1(esk2_1(esk3_0)),esk2_1(esk3_0))),inference(csr,[status(thm)],[3625,415])).
% 0.06/0.44 cnf(3627,negated_conjecture,(g_both(esk4_1(esk2_1(esk3_0)),esk2_1(esk3_0))|~g_true_only(esk4_1(esk2_1(esk3_0)),esk3_0)),inference(spm,[status(thm)],[41,3626,theory(equality)])).
% 0.06/0.44 cnf(3631,negated_conjecture,(~g_true_only(esk4_1(esk2_1(esk3_0)),esk3_0)),inference(csr,[status(thm)],[3627,39])).
% 0.06/0.44 cnf(3632,negated_conjecture,(g_both(esk4_1(esk2_1(esk3_0)),esk3_0)),inference(sr,[status(thm)],[3595,3631,theory(equality)])).
% 0.06/0.44 cnf(3633,negated_conjecture,(~g_both(esk4_1(esk2_1(esk3_0)),esk2_1(esk3_0))),inference(spm,[status(thm)],[3611,3632,theory(equality)])).
% 0.06/0.44 cnf(3634,negated_conjecture,(~g_both(esk4_1(esk2_1(esk3_0)),esk3_0)),inference(spm,[status(thm)],[3633,415,theory(equality)])).
% 0.06/0.44 cnf(3636,negated_conjecture,($false),inference(rw,[status(thm)],[3634,3632,theory(equality)])).
% 0.06/0.44 cnf(3637,negated_conjecture,($false),inference(cn,[status(thm)],[3636,theory(equality)])).
% 0.06/0.44 cnf(3638,negated_conjecture,($false),3637,['proof']).
% 0.06/0.44 # SZS output end CNFRefutation
%------------------------------------------------------------------------------