%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LCL640+1.001 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art03.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 14:30:11 EST 2010
% Result : Theorem 1.73s
% Output : Solution 1.73s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP27123/LCL640+1.001.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP27123/LCL640+1.001.tptp
% SZS output start Solution for /tmp/SystemOnTPTP27123/LCL640+1.001.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 27219
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.014 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, conjecture,~(?[X1]:~((~(![X2]:(~(r1(X1,X2))|((((((![X1]:(~(r1(X2,X1))|p1(X1))|~(p1(X2)))|![X1]:(~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))|~(![X1]:(((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2)))|~(p1(X1)))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2)))|~(p1(X1))))|~((![X1]:(~(r1(X2,X1))|p1(X1))|~(p1(X2)))))))))&((p1(X2)|![X1]:(~(r1(X2,X1))|~(![X2]:(~(r1(X1,X2))|p1(X2)))))|~(![X1]:((~(r1(X2,X1))|p1(X1))|~(![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))))&![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1))))|~(![X2]:(~(r1(X1,X2))|p1(X2)))))&(![X1]:(~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))|~(![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2)))|~(p1(X1))))))|~(![X1]:((~(r1(X2,X1))|p1(X1))|~(![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))))))|~(~(![X2]:(((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|![X1]:(~(r1(X2,X1))|~(![X2]:(~(r1(X1,X2))|p1(X2)))))|~(![X1]:((~(r1(X2,X1))|p1(X1))|~(![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2)))))))))))),file('/tmp/SRASS.s.p', main)).
% fof(2, negated_conjecture,~(~(?[X1]:~((~(![X2]:(~(r1(X1,X2))|((((((![X1]:(~(r1(X2,X1))|p1(X1))|~(p1(X2)))|![X1]:(~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))|~(![X1]:(((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2)))|~(p1(X1)))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2)))|~(p1(X1))))|~((![X1]:(~(r1(X2,X1))|p1(X1))|~(p1(X2)))))))))&((p1(X2)|![X1]:(~(r1(X2,X1))|~(![X2]:(~(r1(X1,X2))|p1(X2)))))|~(![X1]:((~(r1(X2,X1))|p1(X1))|~(![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))))&![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1))))|~(![X2]:(~(r1(X1,X2))|p1(X2)))))&(![X1]:(~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))|~(![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2)))|~(p1(X1))))))|~(![X1]:((~(r1(X2,X1))|p1(X1))|~(![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))))))|~(~(![X2]:(((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|![X1]:(~(r1(X2,X1))|~(![X2]:(~(r1(X1,X2))|p1(X2)))))|~(![X1]:((~(r1(X2,X1))|p1(X1))|~(![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))))))))),inference(assume_negation,[status(cth)],[1])).
% fof(3, negated_conjecture,~(~(?[X1]:~((~(![X2]:(~(r1(X1,X2))|((((((![X1]:(~(r1(X2,X1))|p1(X1))|~(p1(X2)))|![X1]:(~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))|~(![X1]:(((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2)))|~(p1(X1)))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2)))|~(p1(X1))))|~((![X1]:(~(r1(X2,X1))|p1(X1))|~(p1(X2)))))))))&((p1(X2)|![X1]:(~(r1(X2,X1))|~(![X2]:(~(r1(X1,X2))|p1(X2)))))|~(![X1]:((~(r1(X2,X1))|p1(X1))|~(![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))))&![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1))))|~(![X2]:(~(r1(X1,X2))|p1(X2)))))&(![X1]:(~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))|~(![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2)))|~(p1(X1))))))|~(![X1]:((~(r1(X2,X1))|p1(X1))|~(![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))))))|~(~(![X2]:(((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|![X1]:(~(r1(X2,X1))|~(![X2]:(~(r1(X1,X2))|p1(X2)))))|~(![X1]:((~(r1(X2,X1))|p1(X1))|~(![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))))))))),inference(fof_simplification,[status(thm)],[2,theory(equality)])).
% fof(4, plain,![X2]:(epred1_1(X2)=>((((((![X1]:(~(r1(X2,X1))|p1(X1))|~(p1(X2)))|![X1]:(~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))|~(![X1]:(((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2)))|~(p1(X1)))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2)))|~(p1(X1))))|~((![X1]:(~(r1(X2,X1))|p1(X1))|~(p1(X2)))))))))&((p1(X2)|![X1]:(~(r1(X2,X1))|~(![X2]:(~(r1(X1,X2))|p1(X2)))))|~(![X1]:((~(r1(X2,X1))|p1(X1))|~(![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))))&![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1))))|~(![X2]:(~(r1(X1,X2))|p1(X2)))))&(![X1]:(~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))|~(![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2)))|~(p1(X1))))))|~(![X1]:((~(r1(X2,X1))|p1(X1))|~(![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))))),introduced(definition)).
% fof(5, negated_conjecture,~(~(?[X1]:~((~(![X2]:(~(r1(X1,X2))|epred1_1(X2)))|~(~(![X2]:(((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|![X1]:(~(r1(X2,X1))|~(![X2]:(~(r1(X1,X2))|p1(X2)))))|~(![X1]:((~(r1(X2,X1))|p1(X1))|~(![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))))))))),inference(apply_def,[status(esa)],[3,4,theory(equality)])).
% fof(6, negated_conjecture,?[X1]:(![X2]:(~(r1(X1,X2))|epred1_1(X2))&?[X2]:(((r1(X1,X2)&?[X1]:(r1(X2,X1)&~(p1(X1))))&?[X1]:(r1(X2,X1)&![X2]:(~(r1(X1,X2))|p1(X2))))&![X1]:((~(r1(X2,X1))|p1(X1))|?[X2]:((r1(X1,X2)&?[X1]:(r1(X2,X1)&~(p1(X1))))&p1(X2))))),inference(fof_nnf,[status(thm)],[5])).
% fof(7, negated_conjecture,?[X3]:(![X4]:(~(r1(X3,X4))|epred1_1(X4))&?[X5]:(((r1(X3,X5)&?[X6]:(r1(X5,X6)&~(p1(X6))))&?[X7]:(r1(X5,X7)&![X8]:(~(r1(X7,X8))|p1(X8))))&![X9]:((~(r1(X5,X9))|p1(X9))|?[X10]:((r1(X9,X10)&?[X11]:(r1(X10,X11)&~(p1(X11))))&p1(X10))))),inference(variable_rename,[status(thm)],[6])).
% fof(8, negated_conjecture,(![X4]:(~(r1(esk1_0,X4))|epred1_1(X4))&(((r1(esk1_0,esk2_0)&(r1(esk2_0,esk3_0)&~(p1(esk3_0))))&(r1(esk2_0,esk4_0)&![X8]:(~(r1(esk4_0,X8))|p1(X8))))&![X9]:((~(r1(esk2_0,X9))|p1(X9))|((r1(X9,esk5_1(X9))&(r1(esk5_1(X9),esk6_1(X9))&~(p1(esk6_1(X9)))))&p1(esk5_1(X9)))))),inference(skolemize,[status(esa)],[7])).
% fof(9, negated_conjecture,![X4]:![X8]:![X9]:((((~(r1(esk2_0,X9))|p1(X9))|((r1(X9,esk5_1(X9))&(r1(esk5_1(X9),esk6_1(X9))&~(p1(esk6_1(X9)))))&p1(esk5_1(X9))))&(((~(r1(esk4_0,X8))|p1(X8))&r1(esk2_0,esk4_0))&(r1(esk1_0,esk2_0)&(r1(esk2_0,esk3_0)&~(p1(esk3_0))))))&(~(r1(esk1_0,X4))|epred1_1(X4))),inference(shift_quantors,[status(thm)],[8])).
% fof(10, negated_conjecture,![X4]:![X8]:![X9]:(((((r1(X9,esk5_1(X9))|(~(r1(esk2_0,X9))|p1(X9)))&((r1(esk5_1(X9),esk6_1(X9))|(~(r1(esk2_0,X9))|p1(X9)))&(~(p1(esk6_1(X9)))|(~(r1(esk2_0,X9))|p1(X9)))))&(p1(esk5_1(X9))|(~(r1(esk2_0,X9))|p1(X9))))&(((~(r1(esk4_0,X8))|p1(X8))&r1(esk2_0,esk4_0))&(r1(esk1_0,esk2_0)&(r1(esk2_0,esk3_0)&~(p1(esk3_0))))))&(~(r1(esk1_0,X4))|epred1_1(X4))),inference(distribute,[status(thm)],[9])).
% cnf(11,negated_conjecture,(epred1_1(X1)|~r1(esk1_0,X1)),inference(split_conjunct,[status(thm)],[10])).
% cnf(12,negated_conjecture,(~p1(esk3_0)),inference(split_conjunct,[status(thm)],[10])).
% cnf(13,negated_conjecture,(r1(esk2_0,esk3_0)),inference(split_conjunct,[status(thm)],[10])).
% cnf(14,negated_conjecture,(r1(esk1_0,esk2_0)),inference(split_conjunct,[status(thm)],[10])).
% cnf(15,negated_conjecture,(r1(esk2_0,esk4_0)),inference(split_conjunct,[status(thm)],[10])).
% cnf(16,negated_conjecture,(p1(X1)|~r1(esk4_0,X1)),inference(split_conjunct,[status(thm)],[10])).
% cnf(17,negated_conjecture,(p1(X1)|p1(esk5_1(X1))|~r1(esk2_0,X1)),inference(split_conjunct,[status(thm)],[10])).
% cnf(18,negated_conjecture,(p1(X1)|~r1(esk2_0,X1)|~p1(esk6_1(X1))),inference(split_conjunct,[status(thm)],[10])).
% cnf(19,negated_conjecture,(p1(X1)|r1(esk5_1(X1),esk6_1(X1))|~r1(esk2_0,X1)),inference(split_conjunct,[status(thm)],[10])).
% cnf(20,negated_conjecture,(p1(X1)|r1(X1,esk5_1(X1))|~r1(esk2_0,X1)),inference(split_conjunct,[status(thm)],[10])).
% fof(21, plain,![X2]:(~(epred1_1(X2))|((((((![X1]:(~(r1(X2,X1))|p1(X1))|~(p1(X2)))|![X1]:(~(r1(X2,X1))|?[X2]:((r1(X1,X2)&?[X1]:(r1(X2,X1)&~(p1(X1))))&p1(X2))))|?[X1]:(((r1(X2,X1)&?[X2]:(r1(X1,X2)&~(p1(X2))))&p1(X1))&![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2)))|~(p1(X1))))|(?[X1]:(r1(X2,X1)&~(p1(X1)))&p1(X2)))))&((p1(X2)|![X1]:(~(r1(X2,X1))|?[X2]:(r1(X1,X2)&~(p1(X2)))))|?[X1]:((r1(X2,X1)&~(p1(X1)))&![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))&![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1))))|?[X2]:(r1(X1,X2)&~(p1(X2)))))&(![X1]:(~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))|?[X1]:((r1(X2,X1)&?[X2]:(r1(X1,X2)&~(p1(X2))))&p1(X1))))|?[X1]:((r1(X2,X1)&~(p1(X1)))&![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1)))|~(p1(X2))))))),inference(fof_nnf,[status(thm)],[4])).
% fof(22, plain,![X3]:(~(epred1_1(X3))|((((((![X4]:(~(r1(X3,X4))|p1(X4))|~(p1(X3)))|![X5]:(~(r1(X3,X5))|?[X6]:((r1(X5,X6)&?[X7]:(r1(X6,X7)&~(p1(X7))))&p1(X6))))|?[X8]:(((r1(X3,X8)&?[X9]:(r1(X8,X9)&~(p1(X9))))&p1(X8))&![X10]:((~(r1(X8,X10))|![X11]:((~(r1(X10,X11))|![X12]:(~(r1(X11,X12))|p1(X12)))|~(p1(X11))))|(?[X13]:(r1(X10,X13)&~(p1(X13)))&p1(X10)))))&((p1(X3)|![X14]:(~(r1(X3,X14))|?[X15]:(r1(X14,X15)&~(p1(X15)))))|?[X16]:((r1(X3,X16)&~(p1(X16)))&![X17]:((~(r1(X16,X17))|![X18]:(~(r1(X17,X18))|p1(X18)))|~(p1(X17))))))&![X19]:((~(r1(X3,X19))|![X20]:(~(r1(X19,X20))|![X21]:(~(r1(X20,X21))|p1(X21))))|?[X22]:(r1(X19,X22)&~(p1(X22)))))&(![X23]:(~(r1(X3,X23))|![X24]:((~(r1(X23,X24))|p1(X24))|?[X25]:((r1(X24,X25)&?[X26]:(r1(X25,X26)&~(p1(X26))))&p1(X25))))|?[X27]:((r1(X3,X27)&~(p1(X27)))&![X28]:((~(r1(X27,X28))|![X29]:(~(r1(X28,X29))|p1(X29)))|~(p1(X28))))))),inference(variable_rename,[status(thm)],[21])).
% fof(23, plain,![X3]:(~(epred1_1(X3))|((((((![X4]:(~(r1(X3,X4))|p1(X4))|~(p1(X3)))|![X5]:(~(r1(X3,X5))|((r1(X5,esk7_2(X3,X5))&(r1(esk7_2(X3,X5),esk8_2(X3,X5))&~(p1(esk8_2(X3,X5)))))&p1(esk7_2(X3,X5)))))|(((r1(X3,esk9_1(X3))&(r1(esk9_1(X3),esk10_1(X3))&~(p1(esk10_1(X3)))))&p1(esk9_1(X3)))&![X10]:((~(r1(esk9_1(X3),X10))|![X11]:((~(r1(X10,X11))|![X12]:(~(r1(X11,X12))|p1(X12)))|~(p1(X11))))|((r1(X10,esk11_2(X3,X10))&~(p1(esk11_2(X3,X10))))&p1(X10)))))&((p1(X3)|![X14]:(~(r1(X3,X14))|(r1(X14,esk12_2(X3,X14))&~(p1(esk12_2(X3,X14))))))|((r1(X3,esk13_1(X3))&~(p1(esk13_1(X3))))&![X17]:((~(r1(esk13_1(X3),X17))|![X18]:(~(r1(X17,X18))|p1(X18)))|~(p1(X17))))))&![X19]:((~(r1(X3,X19))|![X20]:(~(r1(X19,X20))|![X21]:(~(r1(X20,X21))|p1(X21))))|(r1(X19,esk14_2(X3,X19))&~(p1(esk14_2(X3,X19))))))&(![X23]:(~(r1(X3,X23))|![X24]:((~(r1(X23,X24))|p1(X24))|((r1(X24,esk15_3(X3,X23,X24))&(r1(esk15_3(X3,X23,X24),esk16_3(X3,X23,X24))&~(p1(esk16_3(X3,X23,X24)))))&p1(esk15_3(X3,X23,X24)))))|((r1(X3,esk17_1(X3))&~(p1(esk17_1(X3))))&![X28]:((~(r1(esk17_1(X3),X28))|![X29]:(~(r1(X28,X29))|p1(X29)))|~(p1(X28))))))),inference(skolemize,[status(esa)],[22])).
% fof(24, plain,![X3]:![X4]:![X5]:![X10]:![X11]:![X12]:![X14]:![X17]:![X18]:![X19]:![X20]:![X21]:![X23]:![X24]:![X28]:![X29]:(((((((~(r1(X28,X29))|p1(X29))|~(r1(esk17_1(X3),X28)))|~(p1(X28)))&(r1(X3,esk17_1(X3))&~(p1(esk17_1(X3)))))|(((~(r1(X23,X24))|p1(X24))|((r1(X24,esk15_3(X3,X23,X24))&(r1(esk15_3(X3,X23,X24),esk16_3(X3,X23,X24))&~(p1(esk16_3(X3,X23,X24)))))&p1(esk15_3(X3,X23,X24))))|~(r1(X3,X23))))&(((((~(r1(X20,X21))|p1(X21))|~(r1(X19,X20)))|~(r1(X3,X19)))|(r1(X19,esk14_2(X3,X19))&~(p1(esk14_2(X3,X19)))))&((((((~(r1(X17,X18))|p1(X18))|~(r1(esk13_1(X3),X17)))|~(p1(X17)))&(r1(X3,esk13_1(X3))&~(p1(esk13_1(X3)))))|((~(r1(X3,X14))|(r1(X14,esk12_2(X3,X14))&~(p1(esk12_2(X3,X14)))))|p1(X3)))&(((((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk9_1(X3),X10)))|((r1(X10,esk11_2(X3,X10))&~(p1(esk11_2(X3,X10))))&p1(X10)))&((r1(X3,esk9_1(X3))&(r1(esk9_1(X3),esk10_1(X3))&~(p1(esk10_1(X3)))))&p1(esk9_1(X3))))|((~(r1(X3,X5))|((r1(X5,esk7_2(X3,X5))&(r1(esk7_2(X3,X5),esk8_2(X3,X5))&~(p1(esk8_2(X3,X5)))))&p1(esk7_2(X3,X5))))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))))))|~(epred1_1(X3))),inference(shift_quantors,[status(thm)],[23])).
% fof(25, plain,![X3]:![X4]:![X5]:![X10]:![X11]:![X12]:![X14]:![X17]:![X18]:![X19]:![X20]:![X21]:![X23]:![X24]:![X28]:![X29]:((((((((r1(X24,esk15_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|(((~(r1(X28,X29))|p1(X29))|~(r1(esk17_1(X3),X28)))|~(p1(X28))))|~(epred1_1(X3)))&(((((r1(esk15_3(X3,X23,X24),esk16_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|(((~(r1(X28,X29))|p1(X29))|~(r1(esk17_1(X3),X28)))|~(p1(X28))))|~(epred1_1(X3)))&((((~(p1(esk16_3(X3,X23,X24)))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|(((~(r1(X28,X29))|p1(X29))|~(r1(esk17_1(X3),X28)))|~(p1(X28))))|~(epred1_1(X3)))))&((((p1(esk15_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|(((~(r1(X28,X29))|p1(X29))|~(r1(esk17_1(X3),X28)))|~(p1(X28))))|~(epred1_1(X3))))&(((((((r1(X24,esk15_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|r1(X3,esk17_1(X3)))|~(epred1_1(X3)))&(((((r1(esk15_3(X3,X23,X24),esk16_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|r1(X3,esk17_1(X3)))|~(epred1_1(X3)))&((((~(p1(esk16_3(X3,X23,X24)))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|r1(X3,esk17_1(X3)))|~(epred1_1(X3)))))&((((p1(esk15_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|r1(X3,esk17_1(X3)))|~(epred1_1(X3))))&((((((r1(X24,esk15_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|~(p1(esk17_1(X3))))|~(epred1_1(X3)))&(((((r1(esk15_3(X3,X23,X24),esk16_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|~(p1(esk17_1(X3))))|~(epred1_1(X3)))&((((~(p1(esk16_3(X3,X23,X24)))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|~(p1(esk17_1(X3))))|~(epred1_1(X3)))))&((((p1(esk15_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|~(p1(esk17_1(X3))))|~(epred1_1(X3))))))&((((r1(X19,esk14_2(X3,X19))|(((~(r1(X20,X21))|p1(X21))|~(r1(X19,X20)))|~(r1(X3,X19))))|~(epred1_1(X3)))&((~(p1(esk14_2(X3,X19)))|(((~(r1(X20,X21))|p1(X21))|~(r1(X19,X20)))|~(r1(X3,X19))))|~(epred1_1(X3))))&(((((((r1(X14,esk12_2(X3,X14))|~(r1(X3,X14)))|p1(X3))|(((~(r1(X17,X18))|p1(X18))|~(r1(esk13_1(X3),X17)))|~(p1(X17))))|~(epred1_1(X3)))&((((~(p1(esk12_2(X3,X14)))|~(r1(X3,X14)))|p1(X3))|(((~(r1(X17,X18))|p1(X18))|~(r1(esk13_1(X3),X17)))|~(p1(X17))))|~(epred1_1(X3))))&((((((r1(X14,esk12_2(X3,X14))|~(r1(X3,X14)))|p1(X3))|r1(X3,esk13_1(X3)))|~(epred1_1(X3)))&((((~(p1(esk12_2(X3,X14)))|~(r1(X3,X14)))|p1(X3))|r1(X3,esk13_1(X3)))|~(epred1_1(X3))))&(((((r1(X14,esk12_2(X3,X14))|~(r1(X3,X14)))|p1(X3))|~(p1(esk13_1(X3))))|~(epred1_1(X3)))&((((~(p1(esk12_2(X3,X14)))|~(r1(X3,X14)))|p1(X3))|~(p1(esk13_1(X3))))|~(epred1_1(X3))))))&(((((((((r1(X5,esk7_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(r1(X10,esk11_2(X3,X10))|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk9_1(X3),X10)))))|~(epred1_1(X3)))&(((((r1(esk7_2(X3,X5),esk8_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(r1(X10,esk11_2(X3,X10))|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk9_1(X3),X10)))))|~(epred1_1(X3)))&((((~(p1(esk8_2(X3,X5)))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(r1(X10,esk11_2(X3,X10))|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk9_1(X3),X10)))))|~(epred1_1(X3)))))&((((p1(esk7_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(r1(X10,esk11_2(X3,X10))|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk9_1(X3),X10)))))|~(epred1_1(X3))))&((((((r1(X5,esk7_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(~(p1(esk11_2(X3,X10)))|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk9_1(X3),X10)))))|~(epred1_1(X3)))&(((((r1(esk7_2(X3,X5),esk8_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(~(p1(esk11_2(X3,X10)))|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk9_1(X3),X10)))))|~(epred1_1(X3)))&((((~(p1(esk8_2(X3,X5)))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(~(p1(esk11_2(X3,X10)))|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk9_1(X3),X10)))))|~(epred1_1(X3)))))&((((p1(esk7_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(~(p1(esk11_2(X3,X10)))|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk9_1(X3),X10)))))|~(epred1_1(X3)))))&((((((r1(X5,esk7_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(p1(X10)|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk9_1(X3),X10)))))|~(epred1_1(X3)))&(((((r1(esk7_2(X3,X5),esk8_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(p1(X10)|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk9_1(X3),X10)))))|~(epred1_1(X3)))&((((~(p1(esk8_2(X3,X5)))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(p1(X10)|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk9_1(X3),X10)))))|~(epred1_1(X3)))))&((((p1(esk7_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(p1(X10)|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk9_1(X3),X10)))))|~(epred1_1(X3)))))&((((((((r1(X5,esk7_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|r1(X3,esk9_1(X3)))|~(epred1_1(X3)))&(((((r1(esk7_2(X3,X5),esk8_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|r1(X3,esk9_1(X3)))|~(epred1_1(X3)))&((((~(p1(esk8_2(X3,X5)))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|r1(X3,esk9_1(X3)))|~(epred1_1(X3)))))&((((p1(esk7_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|r1(X3,esk9_1(X3)))|~(epred1_1(X3))))&(((((((r1(X5,esk7_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|r1(esk9_1(X3),esk10_1(X3)))|~(epred1_1(X3)))&(((((r1(esk7_2(X3,X5),esk8_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|r1(esk9_1(X3),esk10_1(X3)))|~(epred1_1(X3)))&((((~(p1(esk8_2(X3,X5)))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|r1(esk9_1(X3),esk10_1(X3)))|~(epred1_1(X3)))))&((((p1(esk7_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|r1(esk9_1(X3),esk10_1(X3)))|~(epred1_1(X3))))&((((((r1(X5,esk7_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|~(p1(esk10_1(X3))))|~(epred1_1(X3)))&(((((r1(esk7_2(X3,X5),esk8_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|~(p1(esk10_1(X3))))|~(epred1_1(X3)))&((((~(p1(esk8_2(X3,X5)))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|~(p1(esk10_1(X3))))|~(epred1_1(X3)))))&((((p1(esk7_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|~(p1(esk10_1(X3))))|~(epred1_1(X3))))))&((((((r1(X5,esk7_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|p1(esk9_1(X3)))|~(epred1_1(X3)))&(((((r1(esk7_2(X3,X5),esk8_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|p1(esk9_1(X3)))|~(epred1_1(X3)))&((((~(p1(esk8_2(X3,X5)))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|p1(esk9_1(X3)))|~(epred1_1(X3)))))&((((p1(esk7_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|p1(esk9_1(X3)))|~(epred1_1(X3))))))))),inference(distribute,[status(thm)],[24])).
% cnf(31,plain,(p1(X2)|~epred1_1(X1)|~p1(esk10_1(X1))|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)|~p1(esk8_2(X1,X3))),inference(split_conjunct,[status(thm)],[25])).
% cnf(32,plain,(p1(X2)|r1(esk7_2(X1,X3),esk8_2(X1,X3))|~epred1_1(X1)|~p1(esk10_1(X1))|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)),inference(split_conjunct,[status(thm)],[25])).
% cnf(33,plain,(p1(X2)|r1(X3,esk7_2(X1,X3))|~epred1_1(X1)|~p1(esk10_1(X1))|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)),inference(split_conjunct,[status(thm)],[25])).
% cnf(35,plain,(r1(esk9_1(X1),esk10_1(X1))|p1(X2)|~epred1_1(X1)|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)|~p1(esk8_2(X1,X3))),inference(split_conjunct,[status(thm)],[25])).
% cnf(36,plain,(r1(esk9_1(X1),esk10_1(X1))|p1(X2)|r1(esk7_2(X1,X3),esk8_2(X1,X3))|~epred1_1(X1)|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)),inference(split_conjunct,[status(thm)],[25])).
% cnf(37,plain,(r1(esk9_1(X1),esk10_1(X1))|p1(X2)|r1(X3,esk7_2(X1,X3))|~epred1_1(X1)|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)),inference(split_conjunct,[status(thm)],[25])).
% cnf(39,plain,(r1(X1,esk9_1(X1))|p1(X2)|~epred1_1(X1)|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)|~p1(esk8_2(X1,X3))),inference(split_conjunct,[status(thm)],[25])).
% cnf(40,plain,(r1(X1,esk9_1(X1))|p1(X2)|r1(esk7_2(X1,X3),esk8_2(X1,X3))|~epred1_1(X1)|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)),inference(split_conjunct,[status(thm)],[25])).
% cnf(41,plain,(r1(X1,esk9_1(X1))|p1(X2)|r1(X3,esk7_2(X1,X3))|~epred1_1(X1)|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)),inference(split_conjunct,[status(thm)],[25])).
% cnf(43,plain,(p1(X4)|p1(X2)|p1(X5)|~epred1_1(X1)|~r1(esk9_1(X1),X2)|~p1(X3)|~r1(X2,X3)|~r1(X3,X4)|~p1(X1)|~r1(X1,X5)|~r1(X1,X6)|~p1(esk8_2(X1,X6))),inference(split_conjunct,[status(thm)],[25])).
% cnf(44,plain,(p1(X4)|p1(X2)|p1(X5)|r1(esk7_2(X1,X6),esk8_2(X1,X6))|~epred1_1(X1)|~r1(esk9_1(X1),X2)|~p1(X3)|~r1(X2,X3)|~r1(X3,X4)|~p1(X1)|~r1(X1,X5)|~r1(X1,X6)),inference(split_conjunct,[status(thm)],[25])).
% cnf(45,plain,(p1(X4)|p1(X2)|p1(X5)|r1(X6,esk7_2(X1,X6))|~epred1_1(X1)|~r1(esk9_1(X1),X2)|~p1(X3)|~r1(X2,X3)|~r1(X3,X4)|~p1(X1)|~r1(X1,X5)|~r1(X1,X6)),inference(split_conjunct,[status(thm)],[25])).
% cnf(54,plain,(p1(X1)|~epred1_1(X1)|~p1(esk13_1(X1))|~r1(X1,X2)|~p1(esk12_2(X1,X2))),inference(split_conjunct,[status(thm)],[25])).
% cnf(55,plain,(p1(X1)|r1(X2,esk12_2(X1,X2))|~epred1_1(X1)|~p1(esk13_1(X1))|~r1(X1,X2)),inference(split_conjunct,[status(thm)],[25])).
% cnf(56,plain,(r1(X1,esk13_1(X1))|p1(X1)|~epred1_1(X1)|~r1(X1,X2)|~p1(esk12_2(X1,X2))),inference(split_conjunct,[status(thm)],[25])).
% cnf(57,plain,(r1(X1,esk13_1(X1))|p1(X1)|r1(X2,esk12_2(X1,X2))|~epred1_1(X1)|~r1(X1,X2)),inference(split_conjunct,[status(thm)],[25])).
% cnf(58,plain,(p1(X3)|p1(X1)|~epred1_1(X1)|~p1(X2)|~r1(esk13_1(X1),X2)|~r1(X2,X3)|~r1(X1,X4)|~p1(esk12_2(X1,X4))),inference(split_conjunct,[status(thm)],[25])).
% cnf(59,plain,(p1(X3)|p1(X1)|r1(X4,esk12_2(X1,X4))|~epred1_1(X1)|~p1(X2)|~r1(esk13_1(X1),X2)|~r1(X2,X3)|~r1(X1,X4)),inference(split_conjunct,[status(thm)],[25])).
% cnf(60,plain,(p1(X4)|~epred1_1(X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~p1(esk14_2(X1,X2))),inference(split_conjunct,[status(thm)],[25])).
% cnf(61,plain,(p1(X4)|r1(X2,esk14_2(X1,X2))|~epred1_1(X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)),inference(split_conjunct,[status(thm)],[25])).
% cnf(62,plain,(p1(X3)|p1(esk15_3(X1,X2,X3))|~epred1_1(X1)|~p1(esk17_1(X1))|~r1(X1,X2)|~r1(X2,X3)),inference(split_conjunct,[status(thm)],[25])).
% cnf(63,plain,(p1(X3)|~epred1_1(X1)|~p1(esk17_1(X1))|~r1(X1,X2)|~r1(X2,X3)|~p1(esk16_3(X1,X2,X3))),inference(split_conjunct,[status(thm)],[25])).
% cnf(64,plain,(p1(X3)|r1(esk15_3(X1,X2,X3),esk16_3(X1,X2,X3))|~epred1_1(X1)|~p1(esk17_1(X1))|~r1(X1,X2)|~r1(X2,X3)),inference(split_conjunct,[status(thm)],[25])).
% cnf(65,plain,(p1(X3)|r1(X3,esk15_3(X1,X2,X3))|~epred1_1(X1)|~p1(esk17_1(X1))|~r1(X1,X2)|~r1(X2,X3)),inference(split_conjunct,[status(thm)],[25])).
% cnf(66,plain,(r1(X1,esk17_1(X1))|p1(X3)|p1(esk15_3(X1,X2,X3))|~epred1_1(X1)|~r1(X1,X2)|~r1(X2,X3)),inference(split_conjunct,[status(thm)],[25])).
% cnf(67,plain,(r1(X1,esk17_1(X1))|p1(X3)|~epred1_1(X1)|~r1(X1,X2)|~r1(X2,X3)|~p1(esk16_3(X1,X2,X3))),inference(split_conjunct,[status(thm)],[25])).
% cnf(68,plain,(r1(X1,esk17_1(X1))|p1(X3)|r1(esk15_3(X1,X2,X3),esk16_3(X1,X2,X3))|~epred1_1(X1)|~r1(X1,X2)|~r1(X2,X3)),inference(split_conjunct,[status(thm)],[25])).
% cnf(69,plain,(r1(X1,esk17_1(X1))|p1(X3)|r1(X3,esk15_3(X1,X2,X3))|~epred1_1(X1)|~r1(X1,X2)|~r1(X2,X3)),inference(split_conjunct,[status(thm)],[25])).
% cnf(70,plain,(p1(X3)|p1(X5)|p1(esk15_3(X1,X4,X5))|~epred1_1(X1)|~p1(X2)|~r1(esk17_1(X1),X2)|~r1(X2,X3)|~r1(X1,X4)|~r1(X4,X5)),inference(split_conjunct,[status(thm)],[25])).
% cnf(71,plain,(p1(X3)|p1(X5)|~epred1_1(X1)|~p1(X2)|~r1(esk17_1(X1),X2)|~r1(X2,X3)|~r1(X1,X4)|~r1(X4,X5)|~p1(esk16_3(X1,X4,X5))),inference(split_conjunct,[status(thm)],[25])).
% cnf(72,plain,(p1(X3)|p1(X5)|r1(esk15_3(X1,X4,X5),esk16_3(X1,X4,X5))|~epred1_1(X1)|~p1(X2)|~r1(esk17_1(X1),X2)|~r1(X2,X3)|~r1(X1,X4)|~r1(X4,X5)),inference(split_conjunct,[status(thm)],[25])).
% cnf(73,plain,(p1(X3)|p1(X5)|r1(X5,esk15_3(X1,X4,X5))|~epred1_1(X1)|~p1(X2)|~r1(esk17_1(X1),X2)|~r1(X2,X3)|~r1(X1,X4)|~r1(X4,X5)),inference(split_conjunct,[status(thm)],[25])).
% cnf(74,negated_conjecture,(epred1_1(esk2_0)),inference(spm,[status(thm)],[11,14,theory(equality)])).
% cnf(87,negated_conjecture,(p1(esk2_0)|r1(esk4_0,esk12_2(esk2_0,esk4_0))|r1(esk2_0,esk13_1(esk2_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[57,15,theory(equality)])).
% cnf(111,negated_conjecture,(p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk2_0)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[41,15,theory(equality)])).
% cnf(124,negated_conjecture,(p1(X1)|r1(esk9_1(esk2_0),esk10_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~p1(esk2_0)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[37,15,theory(equality)])).
% cnf(127,negated_conjecture,(p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk2_0)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[40,15,theory(equality)])).
% cnf(130,negated_conjecture,(p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk2_0)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[36,15,theory(equality)])).
% cnf(238,negated_conjecture,(p1(esk2_0)|r1(esk4_0,esk12_2(esk2_0,esk4_0))|r1(esk2_0,esk13_1(esk2_0))|$false),inference(rw,[status(thm)],[87,74,theory(equality)])).
% cnf(239,negated_conjecture,(p1(esk2_0)|r1(esk4_0,esk12_2(esk2_0,esk4_0))|r1(esk2_0,esk13_1(esk2_0))),inference(cn,[status(thm)],[238,theory(equality)])).
% cnf(254,negated_conjecture,(p1(esk12_2(esk2_0,esk4_0))|p1(esk2_0)|r1(esk2_0,esk13_1(esk2_0))),inference(spm,[status(thm)],[16,239,theory(equality)])).
% cnf(255,plain,(p1(esk2_0)|r1(esk2_0,esk13_1(esk2_0))|~epred1_1(esk2_0)|~r1(esk2_0,esk4_0)),inference(spm,[status(thm)],[56,254,theory(equality)])).
% cnf(256,plain,(p1(esk2_0)|r1(esk2_0,esk13_1(esk2_0))|$false|~r1(esk2_0,esk4_0)),inference(rw,[status(thm)],[255,74,theory(equality)])).
% cnf(257,plain,(p1(esk2_0)|r1(esk2_0,esk13_1(esk2_0))|$false|$false),inference(rw,[status(thm)],[256,15,theory(equality)])).
% cnf(258,plain,(p1(esk2_0)|r1(esk2_0,esk13_1(esk2_0))),inference(cn,[status(thm)],[257,theory(equality)])).
% cnf(292,negated_conjecture,(p1(esk5_1(esk13_1(esk2_0)))|p1(esk13_1(esk2_0))|p1(esk2_0)),inference(spm,[status(thm)],[17,258,theory(equality)])).
% cnf(293,negated_conjecture,(p1(esk13_1(esk2_0))|p1(esk2_0)|~p1(esk6_1(esk13_1(esk2_0)))),inference(spm,[status(thm)],[18,258,theory(equality)])).
% cnf(294,negated_conjecture,(p1(esk13_1(esk2_0))|r1(esk13_1(esk2_0),esk5_1(esk13_1(esk2_0)))|p1(esk2_0)),inference(spm,[status(thm)],[20,258,theory(equality)])).
% cnf(295,negated_conjecture,(p1(esk13_1(esk2_0))|r1(esk5_1(esk13_1(esk2_0)),esk6_1(esk13_1(esk2_0)))|p1(esk2_0)),inference(spm,[status(thm)],[19,258,theory(equality)])).
% cnf(330,plain,(p1(X1)|p1(esk2_0)|r1(X2,esk12_2(esk2_0,X2))|p1(esk13_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk5_1(esk13_1(esk2_0)))|~r1(esk5_1(esk13_1(esk2_0)),X1)|~r1(esk2_0,X2)),inference(spm,[status(thm)],[59,294,theory(equality)])).
% cnf(331,plain,(p1(X1)|p1(esk2_0)|p1(esk13_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk12_2(esk2_0,X2))|~p1(esk5_1(esk13_1(esk2_0)))|~r1(esk5_1(esk13_1(esk2_0)),X1)|~r1(esk2_0,X2)),inference(spm,[status(thm)],[58,294,theory(equality)])).
% cnf(332,plain,(p1(X1)|p1(esk2_0)|r1(X2,esk12_2(esk2_0,X2))|p1(esk13_1(esk2_0))|$false|~p1(esk5_1(esk13_1(esk2_0)))|~r1(esk5_1(esk13_1(esk2_0)),X1)|~r1(esk2_0,X2)),inference(rw,[status(thm)],[330,74,theory(equality)])).
% cnf(333,plain,(p1(X1)|p1(esk2_0)|r1(X2,esk12_2(esk2_0,X2))|p1(esk13_1(esk2_0))|~p1(esk5_1(esk13_1(esk2_0)))|~r1(esk5_1(esk13_1(esk2_0)),X1)|~r1(esk2_0,X2)),inference(cn,[status(thm)],[332,theory(equality)])).
% cnf(334,plain,(p1(X1)|p1(esk2_0)|p1(esk13_1(esk2_0))|$false|~p1(esk12_2(esk2_0,X2))|~p1(esk5_1(esk13_1(esk2_0)))|~r1(esk5_1(esk13_1(esk2_0)),X1)|~r1(esk2_0,X2)),inference(rw,[status(thm)],[331,74,theory(equality)])).
% cnf(335,plain,(p1(X1)|p1(esk2_0)|p1(esk13_1(esk2_0))|~p1(esk12_2(esk2_0,X2))|~p1(esk5_1(esk13_1(esk2_0)))|~r1(esk5_1(esk13_1(esk2_0)),X1)|~r1(esk2_0,X2)),inference(cn,[status(thm)],[334,theory(equality)])).
% cnf(371,negated_conjecture,(p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|$false|~p1(esk2_0)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[111,74,theory(equality)])).
% cnf(372,negated_conjecture,(p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|~p1(esk2_0)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[371,theory(equality)])).
% cnf(441,negated_conjecture,(p1(X1)|r1(esk9_1(esk2_0),esk10_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|~p1(esk2_0)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[124,74,theory(equality)])).
% cnf(442,negated_conjecture,(p1(X1)|r1(esk9_1(esk2_0),esk10_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(esk2_0)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[441,theory(equality)])).
% cnf(462,negated_conjecture,(p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|$false|~p1(esk2_0)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[127,74,theory(equality)])).
% cnf(463,negated_conjecture,(p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|~p1(esk2_0)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[462,theory(equality)])).
% cnf(466,negated_conjecture,(p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))|$false|~p1(esk2_0)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[130,74,theory(equality)])).
% cnf(467,negated_conjecture,(p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))|~p1(esk2_0)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[466,theory(equality)])).
% cnf(495,plain,(p1(esk13_1(esk2_0))|p1(esk2_0)|p1(X1)|~p1(esk12_2(esk2_0,X2))|~r1(esk5_1(esk13_1(esk2_0)),X1)|~r1(esk2_0,X2)),inference(csr,[status(thm)],[335,292])).
% cnf(497,negated_conjecture,(p1(esk13_1(esk2_0))|p1(esk2_0)|p1(X1)|~p1(esk12_2(esk2_0,esk4_0))|~r1(esk5_1(esk13_1(esk2_0)),X1)),inference(spm,[status(thm)],[495,15,theory(equality)])).
% cnf(513,plain,(p1(esk13_1(esk2_0))|p1(esk2_0)|p1(X1)|r1(X2,esk12_2(esk2_0,X2))|~r1(esk5_1(esk13_1(esk2_0)),X1)|~r1(esk2_0,X2)),inference(csr,[status(thm)],[333,292])).
% cnf(515,negated_conjecture,(p1(esk13_1(esk2_0))|p1(esk2_0)|p1(X1)|r1(esk4_0,esk12_2(esk2_0,esk4_0))|~r1(esk5_1(esk13_1(esk2_0)),X1)),inference(spm,[status(thm)],[513,15,theory(equality)])).
% cnf(517,negated_conjecture,(p1(esk13_1(esk2_0))|p1(esk2_0)|p1(esk6_1(esk13_1(esk2_0)))|r1(esk4_0,esk12_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[515,295,theory(equality)])).
% cnf(524,negated_conjecture,(p1(esk13_1(esk2_0))|p1(esk2_0)|r1(esk4_0,esk12_2(esk2_0,esk4_0))),inference(csr,[status(thm)],[517,293])).
% cnf(539,negated_conjecture,(p1(esk12_2(esk2_0,esk4_0))|p1(esk13_1(esk2_0))|p1(esk2_0)),inference(spm,[status(thm)],[16,524,theory(equality)])).
% cnf(560,negated_conjecture,(p1(esk13_1(esk2_0))|p1(esk2_0)|p1(X1)|~r1(esk5_1(esk13_1(esk2_0)),X1)),inference(spm,[status(thm)],[497,539,theory(equality)])).
% cnf(565,negated_conjecture,(p1(esk13_1(esk2_0))|p1(esk2_0)|p1(esk6_1(esk13_1(esk2_0)))),inference(spm,[status(thm)],[560,295,theory(equality)])).
% cnf(576,negated_conjecture,(p1(esk13_1(esk2_0))|p1(esk2_0)),inference(csr,[status(thm)],[565,293])).
% cnf(577,plain,(p1(esk2_0)|r1(X1,esk12_2(esk2_0,X1))|~epred1_1(esk2_0)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[55,576,theory(equality)])).
% cnf(578,plain,(p1(esk2_0)|~epred1_1(esk2_0)|~p1(esk12_2(esk2_0,X1))|~r1(esk2_0,X1)),inference(spm,[status(thm)],[54,576,theory(equality)])).
% cnf(579,plain,(p1(esk2_0)|r1(X1,esk12_2(esk2_0,X1))|$false|~r1(esk2_0,X1)),inference(rw,[status(thm)],[577,74,theory(equality)])).
% cnf(580,plain,(p1(esk2_0)|r1(X1,esk12_2(esk2_0,X1))|~r1(esk2_0,X1)),inference(cn,[status(thm)],[579,theory(equality)])).
% cnf(581,plain,(p1(esk2_0)|$false|~p1(esk12_2(esk2_0,X1))|~r1(esk2_0,X1)),inference(rw,[status(thm)],[578,74,theory(equality)])).
% cnf(582,plain,(p1(esk2_0)|~p1(esk12_2(esk2_0,X1))|~r1(esk2_0,X1)),inference(cn,[status(thm)],[581,theory(equality)])).
% cnf(584,negated_conjecture,(p1(esk2_0)|~p1(esk12_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[582,15,theory(equality)])).
% cnf(591,negated_conjecture,(p1(esk2_0)|r1(esk4_0,esk12_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[580,15,theory(equality)])).
% cnf(607,negated_conjecture,(p1(esk12_2(esk2_0,esk4_0))|p1(esk2_0)),inference(spm,[status(thm)],[16,591,theory(equality)])).
% cnf(627,negated_conjecture,(p1(esk2_0)),inference(csr,[status(thm)],[607,584])).
% cnf(638,negated_conjecture,(p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))|$false|~r1(esk2_0,X1)),inference(rw,[status(thm)],[467,627,theory(equality)])).
% cnf(639,negated_conjecture,(p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))|~r1(esk2_0,X1)),inference(cn,[status(thm)],[638,theory(equality)])).
% cnf(642,negated_conjecture,(p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|$false|~r1(esk2_0,X1)),inference(rw,[status(thm)],[463,627,theory(equality)])).
% cnf(643,negated_conjecture,(p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|~r1(esk2_0,X1)),inference(cn,[status(thm)],[642,theory(equality)])).
% cnf(646,negated_conjecture,(p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))|$false|~r1(esk2_0,X1)),inference(rw,[status(thm)],[442,627,theory(equality)])).
% cnf(647,negated_conjecture,(p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))|~r1(esk2_0,X1)),inference(cn,[status(thm)],[646,theory(equality)])).
% cnf(659,negated_conjecture,(p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|$false|~r1(esk2_0,X1)),inference(rw,[status(thm)],[372,627,theory(equality)])).
% cnf(660,negated_conjecture,(p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|~r1(esk2_0,X1)),inference(cn,[status(thm)],[659,theory(equality)])).
% cnf(707,negated_conjecture,(p1(esk3_0)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))),inference(spm,[status(thm)],[639,13,theory(equality)])).
% cnf(709,negated_conjecture,(r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))),inference(sr,[status(thm)],[707,12,theory(equality)])).
% cnf(720,plain,(p1(esk8_2(esk2_0,esk4_0))|r1(X1,esk14_2(X2,X1))|r1(esk9_1(esk2_0),esk10_1(esk2_0))|~epred1_1(X2)|~r1(X1,esk7_2(esk2_0,esk4_0))|~r1(X2,X1)),inference(spm,[status(thm)],[61,709,theory(equality)])).
% cnf(828,negated_conjecture,(p1(esk3_0)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))),inference(spm,[status(thm)],[660,13,theory(equality)])).
% cnf(830,negated_conjecture,(r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))),inference(sr,[status(thm)],[828,12,theory(equality)])).
% cnf(836,negated_conjecture,(p1(esk3_0)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))),inference(spm,[status(thm)],[643,13,theory(equality)])).
% cnf(838,negated_conjecture,(r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))),inference(sr,[status(thm)],[836,12,theory(equality)])).
% cnf(946,plain,(p1(esk8_2(esk2_0,esk4_0))|r1(X1,esk14_2(X2,X1))|r1(esk2_0,esk9_1(esk2_0))|~epred1_1(X2)|~r1(X1,esk7_2(esk2_0,esk4_0))|~r1(X2,X1)),inference(spm,[status(thm)],[61,838,theory(equality)])).
% cnf(1021,negated_conjecture,(p1(esk3_0)|r1(esk9_1(esk2_0),esk10_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[647,13,theory(equality)])).
% cnf(1023,negated_conjecture,(r1(esk9_1(esk2_0),esk10_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(sr,[status(thm)],[1021,12,theory(equality)])).
% cnf(1099,plain,(p1(esk15_3(X1,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk10_1(esk2_0))|r1(X1,esk17_1(X1))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~epred1_1(X1)|~r1(X1,esk9_1(esk2_0))),inference(spm,[status(thm)],[66,1023,theory(equality)])).
% cnf(1102,plain,(p1(esk10_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(X1,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(X1,esk17_1(X1))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~epred1_1(X1)|~r1(X1,esk9_1(esk2_0))),inference(spm,[status(thm)],[69,1023,theory(equality)])).
% cnf(1103,plain,(p1(esk10_1(esk2_0))|r1(esk15_3(X1,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(X1,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(X1,esk17_1(X1))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~epred1_1(X1)|~r1(X1,esk9_1(esk2_0))),inference(spm,[status(thm)],[68,1023,theory(equality)])).
% cnf(1115,plain,(p1(X1)|p1(X2)|p1(esk10_1(esk2_0))|r1(X3,esk7_2(esk2_0,X3))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~p1(X4)|~p1(esk2_0)|~r1(X4,X2)|~r1(esk10_1(esk2_0),X4)|~r1(esk2_0,X3)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[45,1023,theory(equality)])).
% cnf(1149,plain,(p1(X1)|p1(X2)|p1(esk10_1(esk2_0))|r1(X3,esk7_2(esk2_0,X3))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|~p1(X4)|~p1(esk2_0)|~r1(X4,X2)|~r1(esk10_1(esk2_0),X4)|~r1(esk2_0,X3)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[1115,74,theory(equality)])).
% cnf(1150,plain,(p1(X1)|p1(X2)|p1(esk10_1(esk2_0))|r1(X3,esk7_2(esk2_0,X3))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|~p1(X4)|$false|~r1(X4,X2)|~r1(esk10_1(esk2_0),X4)|~r1(esk2_0,X3)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[1149,627,theory(equality)])).
% cnf(1151,plain,(p1(X1)|p1(X2)|p1(esk10_1(esk2_0))|r1(X3,esk7_2(esk2_0,X3))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(X4)|~r1(X4,X2)|~r1(esk10_1(esk2_0),X4)|~r1(esk2_0,X3)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[1150,theory(equality)])).
% cnf(1502,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|r1(esk4_0,esk14_2(X1,esk4_0))|~epred1_1(X1)|~r1(X1,esk4_0)),inference(spm,[status(thm)],[946,830,theory(equality)])).
% cnf(1503,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[1502,15,theory(equality)])).
% cnf(1504,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|$false),inference(rw,[status(thm)],[1503,74,theory(equality)])).
% cnf(1505,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))),inference(cn,[status(thm)],[1504,theory(equality)])).
% cnf(1520,negated_conjecture,(p1(esk14_2(esk2_0,esk4_0))|p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))),inference(spm,[status(thm)],[16,1505,theory(equality)])).
% cnf(1540,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|~epred1_1(esk2_0)|~r1(X2,X1)|~r1(esk4_0,X2)|~r1(esk2_0,esk4_0)),inference(spm,[status(thm)],[60,1520,theory(equality)])).
% cnf(1541,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|$false|~r1(X2,X1)|~r1(esk4_0,X2)|~r1(esk2_0,esk4_0)),inference(rw,[status(thm)],[1540,74,theory(equality)])).
% cnf(1542,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|$false|~r1(X2,X1)|~r1(esk4_0,X2)|$false),inference(rw,[status(thm)],[1541,15,theory(equality)])).
% cnf(1543,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))|~r1(X2,X1)|~r1(esk4_0,X2)),inference(cn,[status(thm)],[1542,theory(equality)])).
% cnf(1545,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(X1)|r1(esk2_0,esk9_1(esk2_0))|~r1(esk7_2(esk2_0,esk4_0),X1)),inference(spm,[status(thm)],[1543,830,theory(equality)])).
% cnf(1547,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk9_1(esk2_0))),inference(spm,[status(thm)],[1545,838,theory(equality)])).
% cnf(1550,plain,(p1(X1)|r1(esk2_0,esk9_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk2_0)|~r1(esk2_0,esk4_0)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[39,1547,theory(equality)])).
% cnf(1557,plain,(p1(X1)|r1(esk2_0,esk9_1(esk2_0))|$false|~p1(esk2_0)|~r1(esk2_0,esk4_0)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[1550,74,theory(equality)])).
% cnf(1558,plain,(p1(X1)|r1(esk2_0,esk9_1(esk2_0))|$false|$false|~r1(esk2_0,esk4_0)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[1557,627,theory(equality)])).
% cnf(1559,plain,(p1(X1)|r1(esk2_0,esk9_1(esk2_0))|$false|$false|$false|~r1(esk2_0,X1)),inference(rw,[status(thm)],[1558,15,theory(equality)])).
% cnf(1560,plain,(p1(X1)|r1(esk2_0,esk9_1(esk2_0))|~r1(esk2_0,X1)),inference(cn,[status(thm)],[1559,theory(equality)])).
% cnf(1566,negated_conjecture,(p1(esk3_0)|r1(esk2_0,esk9_1(esk2_0))),inference(spm,[status(thm)],[1560,13,theory(equality)])).
% cnf(1568,negated_conjecture,(r1(esk2_0,esk9_1(esk2_0))),inference(sr,[status(thm)],[1566,12,theory(equality)])).
% cnf(1957,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk10_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[1099,1568,theory(equality)])).
% cnf(1958,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk10_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|$false),inference(rw,[status(thm)],[1957,74,theory(equality)])).
% cnf(1959,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk10_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))),inference(cn,[status(thm)],[1958,theory(equality)])).
% cnf(2104,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[1102,1568,theory(equality)])).
% cnf(2105,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|$false),inference(rw,[status(thm)],[2104,74,theory(equality)])).
% cnf(2106,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))),inference(cn,[status(thm)],[2105,theory(equality)])).
% cnf(2167,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|p1(X2)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(X3)|~r1(esk10_1(esk2_0),X3)|~r1(esk2_0,X2)|~r1(X3,X1)),inference(spm,[status(thm)],[1151,15,theory(equality)])).
% cnf(2171,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk3_0)|p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(X2)|~r1(esk10_1(esk2_0),X2)|~r1(X2,X1)),inference(spm,[status(thm)],[2167,13,theory(equality)])).
% cnf(2174,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(X2)|~r1(esk10_1(esk2_0),X2)|~r1(X2,X1)),inference(sr,[status(thm)],[2171,12,theory(equality)])).
% cnf(2176,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(spm,[status(thm)],[2174,2106,theory(equality)])).
% cnf(2216,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(csr,[status(thm)],[2176,1959])).
% cnf(3548,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[1103,1568,theory(equality)])).
% cnf(3549,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|$false),inference(rw,[status(thm)],[3548,74,theory(equality)])).
% cnf(3550,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))),inference(cn,[status(thm)],[3549,theory(equality)])).
% cnf(3566,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))),inference(spm,[status(thm)],[2216,3550,theory(equality)])).
% cnf(3569,plain,(p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~r1(esk9_1(esk2_0),esk10_1(esk2_0))|~r1(esk2_0,esk9_1(esk2_0))),inference(spm,[status(thm)],[67,3566,theory(equality)])).
% cnf(3573,plain,(p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|~r1(esk9_1(esk2_0),esk10_1(esk2_0))|~r1(esk2_0,esk9_1(esk2_0))),inference(rw,[status(thm)],[3569,74,theory(equality)])).
% cnf(3574,plain,(p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|~r1(esk9_1(esk2_0),esk10_1(esk2_0))|$false),inference(rw,[status(thm)],[3573,1568,theory(equality)])).
% cnf(3575,plain,(p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk9_1(esk2_0),esk10_1(esk2_0))),inference(cn,[status(thm)],[3574,theory(equality)])).
% cnf(3576,plain,(p1(esk10_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))),inference(csr,[status(thm)],[3575,1023])).
% cnf(3580,plain,(p1(X1)|r1(X2,esk7_2(esk2_0,X2))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[33,3576,theory(equality)])).
% cnf(3590,plain,(p1(X1)|r1(X2,esk7_2(esk2_0,X2))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|$false|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[3580,74,theory(equality)])).
% cnf(3591,plain,(p1(X1)|r1(X2,esk7_2(esk2_0,X2))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|$false|$false|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[3590,627,theory(equality)])).
% cnf(3592,plain,(p1(X1)|r1(X2,esk7_2(esk2_0,X2))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[3591,theory(equality)])).
% cnf(3630,negated_conjecture,(p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~r1(esk2_0,X1)),inference(spm,[status(thm)],[3592,15,theory(equality)])).
% cnf(3637,negated_conjecture,(p1(esk3_0)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))),inference(spm,[status(thm)],[3630,13,theory(equality)])).
% cnf(3640,negated_conjecture,(r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))),inference(sr,[status(thm)],[3637,12,theory(equality)])).
% cnf(3661,negated_conjecture,(p1(esk5_1(esk17_1(esk2_0)))|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[17,3640,theory(equality)])).
% cnf(3662,negated_conjecture,(p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(esk6_1(esk17_1(esk2_0)))),inference(spm,[status(thm)],[18,3640,theory(equality)])).
% cnf(3663,negated_conjecture,(p1(esk17_1(esk2_0))|r1(esk17_1(esk2_0),esk5_1(esk17_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[20,3640,theory(equality)])).
% cnf(3664,negated_conjecture,(p1(esk17_1(esk2_0))|r1(esk5_1(esk17_1(esk2_0)),esk6_1(esk17_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[19,3640,theory(equality)])).
% cnf(3742,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(X2)|p1(X3)|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X1,X2)|~r1(esk5_1(esk17_1(esk2_0)),X3)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[70,3663,theory(equality)])).
% cnf(3743,plain,(p1(X1)|p1(X2)|r1(X1,esk15_3(esk2_0,X3,X1))|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(spm,[status(thm)],[73,3663,theory(equality)])).
% cnf(3744,plain,(p1(X1)|p1(X2)|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~p1(esk16_3(esk2_0,X3,X1))|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(spm,[status(thm)],[71,3663,theory(equality)])).
% cnf(3745,plain,(p1(X1)|p1(X2)|r1(esk15_3(esk2_0,X3,X1),esk16_3(esk2_0,X3,X1))|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(spm,[status(thm)],[72,3663,theory(equality)])).
% cnf(3754,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(X2)|p1(X3)|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X1,X2)|~r1(esk5_1(esk17_1(esk2_0)),X3)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[3742,74,theory(equality)])).
% cnf(3755,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(X2)|p1(X3)|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X1,X2)|~r1(esk5_1(esk17_1(esk2_0)),X3)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[3754,theory(equality)])).
% cnf(3756,plain,(p1(X1)|p1(X2)|r1(X1,esk15_3(esk2_0,X3,X1))|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(rw,[status(thm)],[3743,74,theory(equality)])).
% cnf(3757,plain,(p1(X1)|p1(X2)|r1(X1,esk15_3(esk2_0,X3,X1))|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(cn,[status(thm)],[3756,theory(equality)])).
% cnf(3758,plain,(p1(X1)|p1(X2)|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|~p1(esk16_3(esk2_0,X3,X1))|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(rw,[status(thm)],[3744,74,theory(equality)])).
% cnf(3759,plain,(p1(X1)|p1(X2)|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(esk16_3(esk2_0,X3,X1))|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(cn,[status(thm)],[3758,theory(equality)])).
% cnf(3760,plain,(p1(X1)|p1(X2)|r1(esk15_3(esk2_0,X3,X1),esk16_3(esk2_0,X3,X1))|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(rw,[status(thm)],[3745,74,theory(equality)])).
% cnf(3761,plain,(p1(X1)|p1(X2)|r1(esk15_3(esk2_0,X3,X1),esk16_3(esk2_0,X3,X1))|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(cn,[status(thm)],[3760,theory(equality)])).
% cnf(3899,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(esk17_1(esk2_0))|p1(X2)|p1(X3)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk5_1(esk17_1(esk2_0)),X3)|~r1(esk2_0,X1)|~r1(X1,X2)),inference(csr,[status(thm)],[3755,3661])).
% cnf(3904,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),X1))|p1(esk17_1(esk2_0))|p1(X2)|p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk9_1(esk2_0),X1)),inference(spm,[status(thm)],[3899,1568,theory(equality)])).
% cnf(3961,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk5_1(esk17_1(esk2_0)),X1)),inference(spm,[status(thm)],[3904,1023,theory(equality)])).
% cnf(3966,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|p1(esk6_1(esk17_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[3961,3664,theory(equality)])).
% cnf(3967,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(csr,[status(thm)],[3966,3662])).
% cnf(3985,plain,(p1(esk17_1(esk2_0))|p1(X1)|p1(X2)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(esk16_3(esk2_0,X3,X1))|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)|~r1(X3,X1)),inference(csr,[status(thm)],[3759,3661])).
% cnf(3990,negated_conjecture,(p1(esk17_1(esk2_0))|p1(X1)|p1(X2)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(esk16_3(esk2_0,esk9_1(esk2_0),X2))|~r1(esk5_1(esk17_1(esk2_0)),X1)|~r1(esk9_1(esk2_0),X2)),inference(spm,[status(thm)],[3985,1568,theory(equality)])).
% cnf(4021,negated_conjecture,(p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|~r1(esk5_1(esk17_1(esk2_0)),X1)),inference(spm,[status(thm)],[3990,1023,theory(equality)])).
% cnf(4159,plain,(p1(esk17_1(esk2_0))|p1(X1)|p1(X2)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(X1,esk15_3(esk2_0,X3,X1))|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)|~r1(X3,X1)),inference(csr,[status(thm)],[3757,3661])).
% cnf(4164,negated_conjecture,(p1(esk17_1(esk2_0))|p1(X1)|p1(X2)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(X2,esk15_3(esk2_0,esk9_1(esk2_0),X2))|~r1(esk5_1(esk17_1(esk2_0)),X1)|~r1(esk9_1(esk2_0),X2)),inference(spm,[status(thm)],[4159,1568,theory(equality)])).
% cnf(4188,negated_conjecture,(p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(X1)|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk5_1(esk17_1(esk2_0)),X1)),inference(spm,[status(thm)],[4164,1023,theory(equality)])).
% cnf(4216,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|p1(esk6_1(esk17_1(esk2_0)))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[4188,3664,theory(equality)])).
% cnf(4217,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(csr,[status(thm)],[4216,3662])).
% cnf(4236,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|~p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(spm,[status(thm)],[2174,4217,theory(equality)])).
% cnf(4275,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(csr,[status(thm)],[4236,3967])).
% cnf(4603,plain,(p1(esk17_1(esk2_0))|p1(X1)|p1(X2)|r1(esk15_3(esk2_0,X3,X1),esk16_3(esk2_0,X3,X1))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)|~r1(X3,X1)),inference(csr,[status(thm)],[3761,3661])).
% cnf(4608,negated_conjecture,(p1(esk17_1(esk2_0))|p1(X1)|p1(X2)|r1(esk15_3(esk2_0,esk9_1(esk2_0),X2),esk16_3(esk2_0,esk9_1(esk2_0),X2))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk5_1(esk17_1(esk2_0)),X1)|~r1(esk9_1(esk2_0),X2)),inference(spm,[status(thm)],[4603,1568,theory(equality)])).
% cnf(5498,negated_conjecture,(p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(X1)|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk5_1(esk17_1(esk2_0)),X1)),inference(spm,[status(thm)],[4608,1023,theory(equality)])).
% cnf(5994,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|p1(esk6_1(esk17_1(esk2_0)))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[5498,3664,theory(equality)])).
% cnf(5999,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(csr,[status(thm)],[5994,3662])).
% cnf(6014,negated_conjecture,(p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[4275,5999,theory(equality)])).
% cnf(6016,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk5_1(esk17_1(esk2_0)),X1)),inference(spm,[status(thm)],[4021,6014,theory(equality)])).
% cnf(6020,negated_conjecture,(p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(esk6_1(esk17_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[6016,3664,theory(equality)])).
% cnf(6021,negated_conjecture,(p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(csr,[status(thm)],[6020,3662])).
% cnf(6025,plain,(p1(X1)|r1(X2,esk7_2(esk2_0,X2))|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[33,6021,theory(equality)])).
% cnf(6035,plain,(p1(X1)|r1(X2,esk7_2(esk2_0,X2))|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[6025,74,theory(equality)])).
% cnf(6036,plain,(p1(X1)|r1(X2,esk7_2(esk2_0,X2))|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|$false|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[6035,627,theory(equality)])).
% cnf(6037,plain,(p1(X1)|r1(X2,esk7_2(esk2_0,X2))|p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[6036,theory(equality)])).
% cnf(6068,negated_conjecture,(p1(esk17_1(esk2_0))|p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk2_0,X1)),inference(spm,[status(thm)],[6037,15,theory(equality)])).
% cnf(6071,negated_conjecture,(p1(esk17_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[6068,3640,theory(equality)])).
% cnf(6083,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(X2)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~r1(X1,X2)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[62,6071,theory(equality)])).
% cnf(6084,plain,(p1(X1)|r1(X1,esk15_3(esk2_0,X2,X1))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~r1(X2,X1)|~r1(esk2_0,X2)),inference(spm,[status(thm)],[65,6071,theory(equality)])).
% cnf(6085,plain,(p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~p1(esk16_3(esk2_0,X2,X1))|~r1(X2,X1)|~r1(esk2_0,X2)),inference(spm,[status(thm)],[63,6071,theory(equality)])).
% cnf(6086,plain,(p1(X1)|r1(esk15_3(esk2_0,X2,X1),esk16_3(esk2_0,X2,X1))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~r1(X2,X1)|~r1(esk2_0,X2)),inference(spm,[status(thm)],[64,6071,theory(equality)])).
% cnf(6087,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(X2)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|~r1(X1,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[6083,74,theory(equality)])).
% cnf(6088,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(X2)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(X1,X2)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[6087,theory(equality)])).
% cnf(6089,plain,(p1(X1)|r1(X1,esk15_3(esk2_0,X2,X1))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|~r1(X2,X1)|~r1(esk2_0,X2)),inference(rw,[status(thm)],[6084,74,theory(equality)])).
% cnf(6090,plain,(p1(X1)|r1(X1,esk15_3(esk2_0,X2,X1))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(X2,X1)|~r1(esk2_0,X2)),inference(cn,[status(thm)],[6089,theory(equality)])).
% cnf(6091,plain,(p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|~p1(esk16_3(esk2_0,X2,X1))|~r1(X2,X1)|~r1(esk2_0,X2)),inference(rw,[status(thm)],[6085,74,theory(equality)])).
% cnf(6092,plain,(p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(esk16_3(esk2_0,X2,X1))|~r1(X2,X1)|~r1(esk2_0,X2)),inference(cn,[status(thm)],[6091,theory(equality)])).
% cnf(6093,plain,(p1(X1)|r1(esk15_3(esk2_0,X2,X1),esk16_3(esk2_0,X2,X1))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|~r1(X2,X1)|~r1(esk2_0,X2)),inference(rw,[status(thm)],[6086,74,theory(equality)])).
% cnf(6094,plain,(p1(X1)|r1(esk15_3(esk2_0,X2,X1),esk16_3(esk2_0,X2,X1))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(X2,X1)|~r1(esk2_0,X2)),inference(cn,[status(thm)],[6093,theory(equality)])).
% cnf(6096,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),X1))|p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk9_1(esk2_0),X1)),inference(spm,[status(thm)],[6088,1568,theory(equality)])).
% cnf(6107,negated_conjecture,(p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(esk16_3(esk2_0,esk9_1(esk2_0),X1))|~r1(esk9_1(esk2_0),X1)),inference(spm,[status(thm)],[6092,1568,theory(equality)])).
% cnf(6119,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk10_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[6096,1023,theory(equality)])).
% cnf(6122,negated_conjecture,(p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|r1(X1,esk15_3(esk2_0,esk9_1(esk2_0),X1))|~r1(esk9_1(esk2_0),X1)),inference(spm,[status(thm)],[6090,1568,theory(equality)])).
% cnf(6157,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(spm,[status(thm)],[6107,1023,theory(equality)])).
% cnf(6162,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[6122,1023,theory(equality)])).
% cnf(6179,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(spm,[status(thm)],[2174,6162,theory(equality)])).
% cnf(6193,negated_conjecture,(p1(X1)|r1(esk15_3(esk2_0,esk9_1(esk2_0),X1),esk16_3(esk2_0,esk9_1(esk2_0),X1))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk9_1(esk2_0),X1)),inference(spm,[status(thm)],[6094,1568,theory(equality)])).
% cnf(6221,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[6193,1023,theory(equality)])).
% cnf(6252,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(csr,[status(thm)],[6179,6119])).
% cnf(6253,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[6252,6221,theory(equality)])).
% cnf(6254,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(csr,[status(thm)],[6253,6157])).
% cnf(6258,plain,(p1(X1)|r1(X2,esk7_2(esk2_0,X2))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[33,6254,theory(equality)])).
% cnf(6268,plain,(p1(X1)|r1(X2,esk7_2(esk2_0,X2))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[6258,74,theory(equality)])).
% cnf(6269,plain,(p1(X1)|r1(X2,esk7_2(esk2_0,X2))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|$false|$false|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[6268,627,theory(equality)])).
% cnf(6270,plain,(p1(X1)|r1(X2,esk7_2(esk2_0,X2))|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[6269,theory(equality)])).
% cnf(6299,negated_conjecture,(p1(X1)|r1(esk4_0,esk7_2(esk2_0,esk4_0))|~r1(esk2_0,X1)),inference(spm,[status(thm)],[6270,15,theory(equality)])).
% cnf(6305,negated_conjecture,(p1(esk3_0)|r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[6299,13,theory(equality)])).
% cnf(6308,negated_conjecture,(r1(esk4_0,esk7_2(esk2_0,esk4_0))),inference(sr,[status(thm)],[6305,12,theory(equality)])).
% cnf(6324,plain,(p1(esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))|r1(esk4_0,esk14_2(X1,esk4_0))|~epred1_1(X1)|~r1(X1,esk4_0)),inference(spm,[status(thm)],[720,6308,theory(equality)])).
% cnf(6395,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[6324,15,theory(equality)])).
% cnf(6396,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|$false),inference(rw,[status(thm)],[6395,74,theory(equality)])).
% cnf(6397,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))),inference(cn,[status(thm)],[6396,theory(equality)])).
% cnf(6412,negated_conjecture,(p1(esk14_2(esk2_0,esk4_0))|p1(esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))),inference(spm,[status(thm)],[16,6397,theory(equality)])).
% cnf(6439,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))|~epred1_1(esk2_0)|~r1(X2,X1)|~r1(esk4_0,X2)|~r1(esk2_0,esk4_0)),inference(spm,[status(thm)],[60,6412,theory(equality)])).
% cnf(6440,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))|$false|~r1(X2,X1)|~r1(esk4_0,X2)|~r1(esk2_0,esk4_0)),inference(rw,[status(thm)],[6439,74,theory(equality)])).
% cnf(6441,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))|$false|~r1(X2,X1)|~r1(esk4_0,X2)|$false),inference(rw,[status(thm)],[6440,15,theory(equality)])).
% cnf(6442,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))|~r1(X2,X1)|~r1(esk4_0,X2)),inference(cn,[status(thm)],[6441,theory(equality)])).
% cnf(6447,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(X1)|r1(esk9_1(esk2_0),esk10_1(esk2_0))|~r1(esk7_2(esk2_0,esk4_0),X1)),inference(spm,[status(thm)],[6442,6308,theory(equality)])).
% cnf(6448,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk9_1(esk2_0),esk10_1(esk2_0))),inference(spm,[status(thm)],[6447,709,theory(equality)])).
% cnf(6458,plain,(p1(esk15_3(X1,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk10_1(esk2_0))|r1(X1,esk17_1(X1))|p1(esk8_2(esk2_0,esk4_0))|~epred1_1(X1)|~r1(X1,esk9_1(esk2_0))),inference(spm,[status(thm)],[66,6448,theory(equality)])).
% cnf(6461,plain,(p1(esk10_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(X1,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(X1,esk17_1(X1))|p1(esk8_2(esk2_0,esk4_0))|~epred1_1(X1)|~r1(X1,esk9_1(esk2_0))),inference(spm,[status(thm)],[69,6448,theory(equality)])).
% cnf(6462,plain,(p1(esk10_1(esk2_0))|r1(esk15_3(X1,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(X1,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(X1,esk17_1(X1))|p1(esk8_2(esk2_0,esk4_0))|~epred1_1(X1)|~r1(X1,esk9_1(esk2_0))),inference(spm,[status(thm)],[68,6448,theory(equality)])).
% cnf(6470,plain,(p1(X1)|p1(X2)|p1(esk10_1(esk2_0))|r1(esk7_2(esk2_0,X3),esk8_2(esk2_0,X3))|p1(esk8_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~p1(X4)|~p1(esk2_0)|~r1(X4,X2)|~r1(esk10_1(esk2_0),X4)|~r1(esk2_0,X3)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[44,6448,theory(equality)])).
% cnf(6515,plain,(p1(X1)|p1(X2)|p1(esk10_1(esk2_0))|r1(esk7_2(esk2_0,X3),esk8_2(esk2_0,X3))|p1(esk8_2(esk2_0,esk4_0))|$false|~p1(X4)|~p1(esk2_0)|~r1(X4,X2)|~r1(esk10_1(esk2_0),X4)|~r1(esk2_0,X3)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[6470,74,theory(equality)])).
% cnf(6516,plain,(p1(X1)|p1(X2)|p1(esk10_1(esk2_0))|r1(esk7_2(esk2_0,X3),esk8_2(esk2_0,X3))|p1(esk8_2(esk2_0,esk4_0))|$false|~p1(X4)|$false|~r1(X4,X2)|~r1(esk10_1(esk2_0),X4)|~r1(esk2_0,X3)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[6515,627,theory(equality)])).
% cnf(6517,plain,(p1(X1)|p1(X2)|p1(esk10_1(esk2_0))|r1(esk7_2(esk2_0,X3),esk8_2(esk2_0,X3))|p1(esk8_2(esk2_0,esk4_0))|~p1(X4)|~r1(X4,X2)|~r1(esk10_1(esk2_0),X4)|~r1(esk2_0,X3)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[6516,theory(equality)])).
% cnf(6564,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[6458,1568,theory(equality)])).
% cnf(6565,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|$false),inference(rw,[status(thm)],[6564,74,theory(equality)])).
% cnf(6566,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))),inference(cn,[status(thm)],[6565,theory(equality)])).
% cnf(6578,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[6461,1568,theory(equality)])).
% cnf(6579,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk2_0,esk17_1(esk2_0))|$false),inference(rw,[status(thm)],[6578,74,theory(equality)])).
% cnf(6580,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk2_0,esk17_1(esk2_0))),inference(cn,[status(thm)],[6579,theory(equality)])).
% cnf(6620,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[6462,1568,theory(equality)])).
% cnf(6621,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk2_0,esk17_1(esk2_0))|$false),inference(rw,[status(thm)],[6620,74,theory(equality)])).
% cnf(6622,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk2_0,esk17_1(esk2_0))),inference(cn,[status(thm)],[6621,theory(equality)])).
% cnf(6638,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(X1)|p1(X2)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|~p1(X3)|~r1(esk10_1(esk2_0),X3)|~r1(esk2_0,X2)|~r1(X3,X1)),inference(spm,[status(thm)],[6517,15,theory(equality)])).
% cnf(6642,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk3_0)|p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|~p1(X2)|~r1(esk10_1(esk2_0),X2)|~r1(X2,X1)),inference(spm,[status(thm)],[6638,13,theory(equality)])).
% cnf(6645,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|~p1(X2)|~r1(esk10_1(esk2_0),X2)|~r1(X2,X1)),inference(sr,[status(thm)],[6642,12,theory(equality)])).
% cnf(6646,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(spm,[status(thm)],[6645,6580,theory(equality)])).
% cnf(6685,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(csr,[status(thm)],[6646,6566])).
% cnf(6686,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))),inference(spm,[status(thm)],[6685,6622,theory(equality)])).
% cnf(6687,plain,(p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|p1(esk8_2(esk2_0,esk4_0))|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~r1(esk9_1(esk2_0),esk10_1(esk2_0))|~r1(esk2_0,esk9_1(esk2_0))),inference(spm,[status(thm)],[67,6686,theory(equality)])).
% cnf(6688,plain,(p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|p1(esk8_2(esk2_0,esk4_0))|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|$false|~r1(esk9_1(esk2_0),esk10_1(esk2_0))|~r1(esk2_0,esk9_1(esk2_0))),inference(rw,[status(thm)],[6687,74,theory(equality)])).
% cnf(6689,plain,(p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|p1(esk8_2(esk2_0,esk4_0))|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|$false|~r1(esk9_1(esk2_0),esk10_1(esk2_0))|$false),inference(rw,[status(thm)],[6688,1568,theory(equality)])).
% cnf(6690,plain,(p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|p1(esk8_2(esk2_0,esk4_0))|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|~r1(esk9_1(esk2_0),esk10_1(esk2_0))),inference(cn,[status(thm)],[6689,theory(equality)])).
% cnf(6691,plain,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))),inference(csr,[status(thm)],[6690,6448])).
% cnf(6702,plain,(p1(esk8_2(esk2_0,esk4_0))|r1(X1,esk14_2(X2,X1))|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(X2)|~r1(X1,esk7_2(esk2_0,esk4_0))|~r1(X2,X1)),inference(spm,[status(thm)],[61,6691,theory(equality)])).
% cnf(6725,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|r1(esk4_0,esk14_2(X1,esk4_0))|~epred1_1(X1)|~r1(X1,esk4_0)),inference(spm,[status(thm)],[6702,6308,theory(equality)])).
% cnf(6726,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[6725,15,theory(equality)])).
% cnf(6727,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|$false),inference(rw,[status(thm)],[6726,74,theory(equality)])).
% cnf(6728,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))),inference(cn,[status(thm)],[6727,theory(equality)])).
% cnf(6743,negated_conjecture,(p1(esk14_2(esk2_0,esk4_0))|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))),inference(spm,[status(thm)],[16,6728,theory(equality)])).
% cnf(6771,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)|~r1(X2,X1)|~r1(esk4_0,X2)|~r1(esk2_0,esk4_0)),inference(spm,[status(thm)],[60,6743,theory(equality)])).
% cnf(6772,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|$false|~r1(X2,X1)|~r1(esk4_0,X2)|~r1(esk2_0,esk4_0)),inference(rw,[status(thm)],[6771,74,theory(equality)])).
% cnf(6773,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|$false|~r1(X2,X1)|~r1(esk4_0,X2)|$false),inference(rw,[status(thm)],[6772,15,theory(equality)])).
% cnf(6774,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|~r1(X2,X1)|~r1(esk4_0,X2)),inference(cn,[status(thm)],[6773,theory(equality)])).
% cnf(6776,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(X1)|r1(esk2_0,esk17_1(esk2_0))|~r1(esk7_2(esk2_0,esk4_0),X1)),inference(spm,[status(thm)],[6774,6308,theory(equality)])).
% cnf(6778,plain,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))),inference(spm,[status(thm)],[6776,6691,theory(equality)])).
% cnf(6781,plain,(p1(X1)|r1(esk7_2(esk2_0,X2),esk8_2(esk2_0,X2))|p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[32,6778,theory(equality)])).
% cnf(6789,plain,(p1(X1)|r1(esk7_2(esk2_0,X2),esk8_2(esk2_0,X2))|p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|$false|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[6781,74,theory(equality)])).
% cnf(6790,plain,(p1(X1)|r1(esk7_2(esk2_0,X2),esk8_2(esk2_0,X2))|p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|$false|$false|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[6789,627,theory(equality)])).
% cnf(6791,plain,(p1(X1)|r1(esk7_2(esk2_0,X2),esk8_2(esk2_0,X2))|p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[6790,theory(equality)])).
% cnf(6914,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~r1(esk2_0,X1)),inference(spm,[status(thm)],[6791,15,theory(equality)])).
% cnf(6918,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk3_0)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))),inference(spm,[status(thm)],[6914,13,theory(equality)])).
% cnf(6921,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))),inference(sr,[status(thm)],[6918,12,theory(equality)])).
% cnf(6940,plain,(p1(esk8_2(esk2_0,esk4_0))|r1(X1,esk14_2(X2,X1))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(X2)|~r1(X1,esk7_2(esk2_0,esk4_0))|~r1(X2,X1)),inference(spm,[status(thm)],[61,6921,theory(equality)])).
% cnf(7002,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|r1(esk4_0,esk14_2(X1,esk4_0))|~epred1_1(X1)|~r1(X1,esk4_0)),inference(spm,[status(thm)],[6940,6308,theory(equality)])).
% cnf(7003,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[7002,15,theory(equality)])).
% cnf(7004,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|$false),inference(rw,[status(thm)],[7003,74,theory(equality)])).
% cnf(7005,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))),inference(cn,[status(thm)],[7004,theory(equality)])).
% cnf(7020,negated_conjecture,(p1(esk14_2(esk2_0,esk4_0))|p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))),inference(spm,[status(thm)],[16,7005,theory(equality)])).
% cnf(7040,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)|~r1(X2,X1)|~r1(esk4_0,X2)|~r1(esk2_0,esk4_0)),inference(spm,[status(thm)],[60,7020,theory(equality)])).
% cnf(7041,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|$false|~r1(X2,X1)|~r1(esk4_0,X2)|~r1(esk2_0,esk4_0)),inference(rw,[status(thm)],[7040,74,theory(equality)])).
% cnf(7042,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|$false|~r1(X2,X1)|~r1(esk4_0,X2)|$false),inference(rw,[status(thm)],[7041,15,theory(equality)])).
% cnf(7043,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))|~r1(X2,X1)|~r1(esk4_0,X2)),inference(cn,[status(thm)],[7042,theory(equality)])).
% cnf(7045,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(X1)|r1(esk2_0,esk17_1(esk2_0))|~r1(esk7_2(esk2_0,esk4_0),X1)),inference(spm,[status(thm)],[7043,6308,theory(equality)])).
% cnf(7055,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk2_0,esk17_1(esk2_0))),inference(spm,[status(thm)],[7045,6921,theory(equality)])).
% cnf(7058,plain,(p1(X1)|r1(esk9_1(esk2_0),esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk2_0)|~r1(esk2_0,esk4_0)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[35,7055,theory(equality)])).
% cnf(7069,plain,(p1(X1)|r1(esk9_1(esk2_0),esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|$false|~p1(esk2_0)|~r1(esk2_0,esk4_0)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[7058,74,theory(equality)])).
% cnf(7070,plain,(p1(X1)|r1(esk9_1(esk2_0),esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|$false|$false|~r1(esk2_0,esk4_0)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[7069,627,theory(equality)])).
% cnf(7071,plain,(p1(X1)|r1(esk9_1(esk2_0),esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|$false|$false|$false|~r1(esk2_0,X1)),inference(rw,[status(thm)],[7070,15,theory(equality)])).
% cnf(7072,plain,(p1(X1)|r1(esk9_1(esk2_0),esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|~r1(esk2_0,X1)),inference(cn,[status(thm)],[7071,theory(equality)])).
% cnf(7075,negated_conjecture,(p1(esk3_0)|r1(esk9_1(esk2_0),esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))),inference(spm,[status(thm)],[7072,13,theory(equality)])).
% cnf(7078,negated_conjecture,(r1(esk9_1(esk2_0),esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))),inference(sr,[status(thm)],[7075,12,theory(equality)])).
% cnf(7088,plain,(p1(esk15_3(X1,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk10_1(esk2_0))|r1(X1,esk17_1(X1))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(X1)|~r1(X1,esk9_1(esk2_0))),inference(spm,[status(thm)],[66,7078,theory(equality)])).
% cnf(7091,plain,(p1(esk10_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(X1,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(X1,esk17_1(X1))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(X1)|~r1(X1,esk9_1(esk2_0))),inference(spm,[status(thm)],[69,7078,theory(equality)])).
% cnf(7092,plain,(p1(esk10_1(esk2_0))|r1(esk15_3(X1,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(X1,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(X1,esk17_1(X1))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(X1)|~r1(X1,esk9_1(esk2_0))),inference(spm,[status(thm)],[68,7078,theory(equality)])).
% cnf(7099,plain,(p1(X1)|p1(X2)|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk8_2(esk2_0,X3))|~p1(X4)|~p1(esk2_0)|~r1(X4,X2)|~r1(esk10_1(esk2_0),X4)|~r1(esk2_0,X3)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[43,7078,theory(equality)])).
% cnf(7142,plain,(p1(X1)|p1(X2)|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|$false|~p1(esk8_2(esk2_0,X3))|~p1(X4)|~p1(esk2_0)|~r1(X4,X2)|~r1(esk10_1(esk2_0),X4)|~r1(esk2_0,X3)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[7099,74,theory(equality)])).
% cnf(7143,plain,(p1(X1)|p1(X2)|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|$false|~p1(esk8_2(esk2_0,X3))|~p1(X4)|$false|~r1(X4,X2)|~r1(esk10_1(esk2_0),X4)|~r1(esk2_0,X3)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[7142,627,theory(equality)])).
% cnf(7144,plain,(p1(X1)|p1(X2)|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|~p1(esk8_2(esk2_0,X3))|~p1(X4)|~r1(X4,X2)|~r1(esk10_1(esk2_0),X4)|~r1(esk2_0,X3)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[7143,theory(equality)])).
% cnf(7169,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[7088,1568,theory(equality)])).
% cnf(7170,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|$false),inference(rw,[status(thm)],[7169,74,theory(equality)])).
% cnf(7171,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))),inference(cn,[status(thm)],[7170,theory(equality)])).
% cnf(7184,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|p1(X2)|r1(esk2_0,esk17_1(esk2_0))|~p1(esk8_2(esk2_0,esk4_0))|~p1(X3)|~r1(esk10_1(esk2_0),X3)|~r1(esk2_0,X2)|~r1(X3,X1)),inference(spm,[status(thm)],[7144,15,theory(equality)])).
% cnf(7193,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|p1(X2)|r1(esk2_0,esk17_1(esk2_0))|~p1(X3)|~r1(esk10_1(esk2_0),X3)|~r1(esk2_0,X2)|~r1(X3,X1)),inference(csr,[status(thm)],[7184,7055])).
% cnf(7196,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk3_0)|p1(X1)|r1(esk2_0,esk17_1(esk2_0))|~p1(X2)|~r1(esk10_1(esk2_0),X2)|~r1(X2,X1)),inference(spm,[status(thm)],[7193,13,theory(equality)])).
% cnf(7199,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|r1(esk2_0,esk17_1(esk2_0))|~p1(X2)|~r1(esk10_1(esk2_0),X2)|~r1(X2,X1)),inference(sr,[status(thm)],[7196,12,theory(equality)])).
% cnf(7200,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[7091,1568,theory(equality)])).
% cnf(7201,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk2_0,esk17_1(esk2_0))|$false),inference(rw,[status(thm)],[7200,74,theory(equality)])).
% cnf(7202,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk2_0,esk17_1(esk2_0))),inference(cn,[status(thm)],[7201,theory(equality)])).
% cnf(7217,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|r1(esk2_0,esk17_1(esk2_0))|~p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(spm,[status(thm)],[7199,7202,theory(equality)])).
% cnf(7228,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|r1(esk2_0,esk17_1(esk2_0))|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(csr,[status(thm)],[7217,7171])).
% cnf(7243,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[7092,1568,theory(equality)])).
% cnf(7244,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk2_0,esk17_1(esk2_0))|$false),inference(rw,[status(thm)],[7243,74,theory(equality)])).
% cnf(7245,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk2_0,esk17_1(esk2_0))),inference(cn,[status(thm)],[7244,theory(equality)])).
% cnf(7260,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk2_0,esk17_1(esk2_0))),inference(spm,[status(thm)],[7228,7245,theory(equality)])).
% cnf(7261,plain,(p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)|~r1(esk9_1(esk2_0),esk10_1(esk2_0))|~r1(esk2_0,esk9_1(esk2_0))),inference(spm,[status(thm)],[67,7260,theory(equality)])).
% cnf(7262,plain,(p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|$false|~r1(esk9_1(esk2_0),esk10_1(esk2_0))|~r1(esk2_0,esk9_1(esk2_0))),inference(rw,[status(thm)],[7261,74,theory(equality)])).
% cnf(7263,plain,(p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|$false|~r1(esk9_1(esk2_0),esk10_1(esk2_0))|$false),inference(rw,[status(thm)],[7262,1568,theory(equality)])).
% cnf(7264,plain,(p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))|~r1(esk9_1(esk2_0),esk10_1(esk2_0))),inference(cn,[status(thm)],[7263,theory(equality)])).
% cnf(7265,plain,(p1(esk10_1(esk2_0))|r1(esk2_0,esk17_1(esk2_0))),inference(csr,[status(thm)],[7264,7078])).
% cnf(7267,plain,(p1(X1)|r1(esk2_0,esk17_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk8_2(esk2_0,X2))|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[31,7265,theory(equality)])).
% cnf(7273,plain,(p1(X1)|r1(esk2_0,esk17_1(esk2_0))|$false|~p1(esk8_2(esk2_0,X2))|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[7267,74,theory(equality)])).
% cnf(7274,plain,(p1(X1)|r1(esk2_0,esk17_1(esk2_0))|$false|~p1(esk8_2(esk2_0,X2))|$false|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[7273,627,theory(equality)])).
% cnf(7275,plain,(p1(X1)|r1(esk2_0,esk17_1(esk2_0))|~p1(esk8_2(esk2_0,X2))|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[7274,theory(equality)])).
% cnf(7283,negated_conjecture,(p1(X1)|r1(esk2_0,esk17_1(esk2_0))|~p1(esk8_2(esk2_0,esk4_0))|~r1(esk2_0,X1)),inference(spm,[status(thm)],[7275,15,theory(equality)])).
% cnf(7285,negated_conjecture,(p1(X1)|r1(esk2_0,esk17_1(esk2_0))|~r1(esk2_0,X1)),inference(csr,[status(thm)],[7283,7055])).
% cnf(7288,negated_conjecture,(p1(esk3_0)|r1(esk2_0,esk17_1(esk2_0))),inference(spm,[status(thm)],[7285,13,theory(equality)])).
% cnf(7291,negated_conjecture,(r1(esk2_0,esk17_1(esk2_0))),inference(sr,[status(thm)],[7288,12,theory(equality)])).
% cnf(7306,negated_conjecture,(p1(esk5_1(esk17_1(esk2_0)))|p1(esk17_1(esk2_0))),inference(spm,[status(thm)],[17,7291,theory(equality)])).
% cnf(7307,negated_conjecture,(p1(esk17_1(esk2_0))|~p1(esk6_1(esk17_1(esk2_0)))),inference(spm,[status(thm)],[18,7291,theory(equality)])).
% cnf(7308,negated_conjecture,(p1(esk17_1(esk2_0))|r1(esk17_1(esk2_0),esk5_1(esk17_1(esk2_0)))),inference(spm,[status(thm)],[20,7291,theory(equality)])).
% cnf(7309,negated_conjecture,(p1(esk17_1(esk2_0))|r1(esk5_1(esk17_1(esk2_0)),esk6_1(esk17_1(esk2_0)))),inference(spm,[status(thm)],[19,7291,theory(equality)])).
% cnf(7407,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(X2)|p1(X3)|p1(esk17_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X1,X2)|~r1(esk5_1(esk17_1(esk2_0)),X3)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[70,7308,theory(equality)])).
% cnf(7408,plain,(p1(X1)|p1(X2)|r1(X1,esk15_3(esk2_0,X3,X1))|p1(esk17_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(spm,[status(thm)],[73,7308,theory(equality)])).
% cnf(7409,plain,(p1(X1)|p1(X2)|p1(esk17_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk16_3(esk2_0,X3,X1))|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(spm,[status(thm)],[71,7308,theory(equality)])).
% cnf(7410,plain,(p1(X1)|p1(X2)|r1(esk15_3(esk2_0,X3,X1),esk16_3(esk2_0,X3,X1))|p1(esk17_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(spm,[status(thm)],[72,7308,theory(equality)])).
% cnf(7411,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(X2)|p1(X3)|p1(esk17_1(esk2_0))|$false|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X1,X2)|~r1(esk5_1(esk17_1(esk2_0)),X3)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[7407,74,theory(equality)])).
% cnf(7412,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(X2)|p1(X3)|p1(esk17_1(esk2_0))|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X1,X2)|~r1(esk5_1(esk17_1(esk2_0)),X3)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[7411,theory(equality)])).
% cnf(7413,plain,(p1(X1)|p1(X2)|r1(X1,esk15_3(esk2_0,X3,X1))|p1(esk17_1(esk2_0))|$false|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(rw,[status(thm)],[7408,74,theory(equality)])).
% cnf(7414,plain,(p1(X1)|p1(X2)|r1(X1,esk15_3(esk2_0,X3,X1))|p1(esk17_1(esk2_0))|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(cn,[status(thm)],[7413,theory(equality)])).
% cnf(7415,plain,(p1(X1)|p1(X2)|p1(esk17_1(esk2_0))|$false|~p1(esk16_3(esk2_0,X3,X1))|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(rw,[status(thm)],[7409,74,theory(equality)])).
% cnf(7416,plain,(p1(X1)|p1(X2)|p1(esk17_1(esk2_0))|~p1(esk16_3(esk2_0,X3,X1))|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(cn,[status(thm)],[7415,theory(equality)])).
% cnf(7417,plain,(p1(X1)|p1(X2)|r1(esk15_3(esk2_0,X3,X1),esk16_3(esk2_0,X3,X1))|p1(esk17_1(esk2_0))|$false|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(rw,[status(thm)],[7410,74,theory(equality)])).
% cnf(7418,plain,(p1(X1)|p1(X2)|r1(esk15_3(esk2_0,X3,X1),esk16_3(esk2_0,X3,X1))|p1(esk17_1(esk2_0))|~p1(esk5_1(esk17_1(esk2_0)))|~r1(X3,X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)),inference(cn,[status(thm)],[7417,theory(equality)])).
% cnf(7545,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(esk17_1(esk2_0))|p1(X2)|p1(X3)|~r1(esk5_1(esk17_1(esk2_0)),X3)|~r1(esk2_0,X1)|~r1(X1,X2)),inference(csr,[status(thm)],[7412,7306])).
% cnf(7547,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),X1))|p1(esk17_1(esk2_0))|p1(X2)|p1(X1)|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk9_1(esk2_0),X1)),inference(spm,[status(thm)],[7545,1568,theory(equality)])).
% cnf(7573,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(X1)|p1(esk8_2(esk2_0,esk4_0))|~r1(esk5_1(esk17_1(esk2_0)),X1)),inference(spm,[status(thm)],[7547,6448,theory(equality)])).
% cnf(7578,plain,(p1(esk17_1(esk2_0))|p1(X1)|p1(X2)|~p1(esk16_3(esk2_0,X3,X1))|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)|~r1(X3,X1)),inference(csr,[status(thm)],[7416,7306])).
% cnf(7580,negated_conjecture,(p1(esk17_1(esk2_0))|p1(X1)|p1(X2)|~p1(esk16_3(esk2_0,esk9_1(esk2_0),X2))|~r1(esk5_1(esk17_1(esk2_0)),X1)|~r1(esk9_1(esk2_0),X2)),inference(spm,[status(thm)],[7578,1568,theory(equality)])).
% cnf(7604,negated_conjecture,(p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(X1)|p1(esk8_2(esk2_0,esk4_0))|~p1(esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|~r1(esk5_1(esk17_1(esk2_0)),X1)),inference(spm,[status(thm)],[7580,6448,theory(equality)])).
% cnf(7609,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|p1(esk6_1(esk17_1(esk2_0)))),inference(spm,[status(thm)],[7573,7309,theory(equality)])).
% cnf(7610,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))),inference(csr,[status(thm)],[7609,7307])).
% cnf(7644,plain,(p1(esk17_1(esk2_0))|p1(X1)|p1(X2)|r1(X1,esk15_3(esk2_0,X3,X1))|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)|~r1(X3,X1)),inference(csr,[status(thm)],[7414,7306])).
% cnf(7646,negated_conjecture,(p1(esk17_1(esk2_0))|p1(X1)|p1(X2)|r1(X2,esk15_3(esk2_0,esk9_1(esk2_0),X2))|~r1(esk5_1(esk17_1(esk2_0)),X1)|~r1(esk9_1(esk2_0),X2)),inference(spm,[status(thm)],[7644,1568,theory(equality)])).
% cnf(7671,negated_conjecture,(p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(X1)|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk8_2(esk2_0,esk4_0))|~r1(esk5_1(esk17_1(esk2_0)),X1)),inference(spm,[status(thm)],[7646,6448,theory(equality)])).
% cnf(7716,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|p1(esk6_1(esk17_1(esk2_0)))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(spm,[status(thm)],[7671,7309,theory(equality)])).
% cnf(7717,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(csr,[status(thm)],[7716,7307])).
% cnf(7736,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|~p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(spm,[status(thm)],[6645,7717,theory(equality)])).
% cnf(7741,plain,(p1(esk17_1(esk2_0))|p1(X1)|p1(X2)|r1(esk15_3(esk2_0,X3,X1),esk16_3(esk2_0,X3,X1))|~r1(esk5_1(esk17_1(esk2_0)),X2)|~r1(esk2_0,X3)|~r1(X3,X1)),inference(csr,[status(thm)],[7418,7306])).
% cnf(7743,negated_conjecture,(p1(esk17_1(esk2_0))|p1(X1)|p1(X2)|r1(esk15_3(esk2_0,esk9_1(esk2_0),X2),esk16_3(esk2_0,esk9_1(esk2_0),X2))|~r1(esk5_1(esk17_1(esk2_0)),X1)|~r1(esk9_1(esk2_0),X2)),inference(spm,[status(thm)],[7741,1568,theory(equality)])).
% cnf(7802,negated_conjecture,(p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(X1)|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk8_2(esk2_0,esk4_0))|~r1(esk5_1(esk17_1(esk2_0)),X1)),inference(spm,[status(thm)],[7743,6448,theory(equality)])).
% cnf(8054,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|p1(esk6_1(esk17_1(esk2_0)))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(spm,[status(thm)],[7802,7309,theory(equality)])).
% cnf(8055,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(csr,[status(thm)],[8054,7307])).
% cnf(8174,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(csr,[status(thm)],[7736,7610])).
% cnf(8175,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[8174,8055,theory(equality)])).
% cnf(8177,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|~r1(esk5_1(esk17_1(esk2_0)),X1)),inference(spm,[status(thm)],[7604,8175,theory(equality)])).
% cnf(8184,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(esk6_1(esk17_1(esk2_0)))|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[8177,7309,theory(equality)])).
% cnf(8185,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))),inference(csr,[status(thm)],[8184,7307])).
% cnf(8196,plain,(p1(esk8_2(esk2_0,esk4_0))|r1(X1,esk14_2(X2,X1))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|~epred1_1(X2)|~r1(X1,esk7_2(esk2_0,esk4_0))|~r1(X2,X1)),inference(spm,[status(thm)],[61,8185,theory(equality)])).
% cnf(8219,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|r1(esk4_0,esk14_2(X1,esk4_0))|~epred1_1(X1)|~r1(X1,esk4_0)),inference(spm,[status(thm)],[8196,6308,theory(equality)])).
% cnf(8220,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[8219,15,theory(equality)])).
% cnf(8221,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|$false),inference(rw,[status(thm)],[8220,74,theory(equality)])).
% cnf(8222,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))),inference(cn,[status(thm)],[8221,theory(equality)])).
% cnf(8237,negated_conjecture,(p1(esk14_2(esk2_0,esk4_0))|p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))),inference(spm,[status(thm)],[16,8222,theory(equality)])).
% cnf(8257,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|~epred1_1(esk2_0)|~r1(X2,X1)|~r1(esk4_0,X2)|~r1(esk2_0,esk4_0)),inference(spm,[status(thm)],[60,8237,theory(equality)])).
% cnf(8258,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|$false|~r1(X2,X1)|~r1(esk4_0,X2)|~r1(esk2_0,esk4_0)),inference(rw,[status(thm)],[8257,74,theory(equality)])).
% cnf(8259,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|$false|~r1(X2,X1)|~r1(esk4_0,X2)|$false),inference(rw,[status(thm)],[8258,15,theory(equality)])).
% cnf(8260,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|~r1(X2,X1)|~r1(esk4_0,X2)),inference(cn,[status(thm)],[8259,theory(equality)])).
% cnf(8262,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(X1)|~r1(esk7_2(esk2_0,esk4_0),X1)),inference(spm,[status(thm)],[8260,6308,theory(equality)])).
% cnf(8264,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))),inference(spm,[status(thm)],[8262,8185,theory(equality)])).
% cnf(8267,plain,(p1(X1)|r1(esk7_2(esk2_0,X2),esk8_2(esk2_0,X2))|p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[32,8264,theory(equality)])).
% cnf(8275,plain,(p1(X1)|r1(esk7_2(esk2_0,X2),esk8_2(esk2_0,X2))|p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|$false|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[8267,74,theory(equality)])).
% cnf(8276,plain,(p1(X1)|r1(esk7_2(esk2_0,X2),esk8_2(esk2_0,X2))|p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|$false|$false|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[8275,627,theory(equality)])).
% cnf(8277,plain,(p1(X1)|r1(esk7_2(esk2_0,X2),esk8_2(esk2_0,X2))|p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[8276,theory(equality)])).
% cnf(8455,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|~r1(esk2_0,X1)),inference(spm,[status(thm)],[8277,15,theory(equality)])).
% cnf(8457,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[8455,7291,theory(equality)])).
% cnf(8474,plain,(p1(esk8_2(esk2_0,esk4_0))|r1(X1,esk14_2(X2,X1))|p1(esk17_1(esk2_0))|~epred1_1(X2)|~r1(X1,esk7_2(esk2_0,esk4_0))|~r1(X2,X1)),inference(spm,[status(thm)],[61,8457,theory(equality)])).
% cnf(8537,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|r1(esk4_0,esk14_2(X1,esk4_0))|~epred1_1(X1)|~r1(X1,esk4_0)),inference(spm,[status(thm)],[8474,6308,theory(equality)])).
% cnf(8538,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[8537,15,theory(equality)])).
% cnf(8539,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|$false),inference(rw,[status(thm)],[8538,74,theory(equality)])).
% cnf(8540,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))),inference(cn,[status(thm)],[8539,theory(equality)])).
% cnf(8555,negated_conjecture,(p1(esk14_2(esk2_0,esk4_0))|p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))),inference(spm,[status(thm)],[16,8540,theory(equality)])).
% cnf(8575,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|~epred1_1(esk2_0)|~r1(X2,X1)|~r1(esk4_0,X2)|~r1(esk2_0,esk4_0)),inference(spm,[status(thm)],[60,8555,theory(equality)])).
% cnf(8576,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|$false|~r1(X2,X1)|~r1(esk4_0,X2)|~r1(esk2_0,esk4_0)),inference(rw,[status(thm)],[8575,74,theory(equality)])).
% cnf(8577,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|$false|~r1(X2,X1)|~r1(esk4_0,X2)|$false),inference(rw,[status(thm)],[8576,15,theory(equality)])).
% cnf(8578,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|~r1(X2,X1)|~r1(esk4_0,X2)),inference(cn,[status(thm)],[8577,theory(equality)])).
% cnf(8580,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))|p1(X1)|~r1(esk7_2(esk2_0,esk4_0),X1)),inference(spm,[status(thm)],[8578,6308,theory(equality)])).
% cnf(8582,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk17_1(esk2_0))),inference(spm,[status(thm)],[8580,8457,theory(equality)])).
% cnf(8583,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(X2)|p1(esk8_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~r1(X1,X2)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[62,8582,theory(equality)])).
% cnf(8584,plain,(p1(X1)|r1(X1,esk15_3(esk2_0,X2,X1))|p1(esk8_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~r1(X2,X1)|~r1(esk2_0,X2)),inference(spm,[status(thm)],[65,8582,theory(equality)])).
% cnf(8585,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~p1(esk16_3(esk2_0,X2,X1))|~r1(X2,X1)|~r1(esk2_0,X2)),inference(spm,[status(thm)],[63,8582,theory(equality)])).
% cnf(8586,plain,(p1(X1)|r1(esk15_3(esk2_0,X2,X1),esk16_3(esk2_0,X2,X1))|p1(esk8_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~r1(X2,X1)|~r1(esk2_0,X2)),inference(spm,[status(thm)],[64,8582,theory(equality)])).
% cnf(8587,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(X2)|p1(esk8_2(esk2_0,esk4_0))|$false|~r1(X1,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[8583,74,theory(equality)])).
% cnf(8588,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(X2)|p1(esk8_2(esk2_0,esk4_0))|~r1(X1,X2)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[8587,theory(equality)])).
% cnf(8589,plain,(p1(X1)|r1(X1,esk15_3(esk2_0,X2,X1))|p1(esk8_2(esk2_0,esk4_0))|$false|~r1(X2,X1)|~r1(esk2_0,X2)),inference(rw,[status(thm)],[8584,74,theory(equality)])).
% cnf(8590,plain,(p1(X1)|r1(X1,esk15_3(esk2_0,X2,X1))|p1(esk8_2(esk2_0,esk4_0))|~r1(X2,X1)|~r1(esk2_0,X2)),inference(cn,[status(thm)],[8589,theory(equality)])).
% cnf(8591,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|$false|~p1(esk16_3(esk2_0,X2,X1))|~r1(X2,X1)|~r1(esk2_0,X2)),inference(rw,[status(thm)],[8585,74,theory(equality)])).
% cnf(8592,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|~p1(esk16_3(esk2_0,X2,X1))|~r1(X2,X1)|~r1(esk2_0,X2)),inference(cn,[status(thm)],[8591,theory(equality)])).
% cnf(8593,plain,(p1(X1)|r1(esk15_3(esk2_0,X2,X1),esk16_3(esk2_0,X2,X1))|p1(esk8_2(esk2_0,esk4_0))|$false|~r1(X2,X1)|~r1(esk2_0,X2)),inference(rw,[status(thm)],[8586,74,theory(equality)])).
% cnf(8594,plain,(p1(X1)|r1(esk15_3(esk2_0,X2,X1),esk16_3(esk2_0,X2,X1))|p1(esk8_2(esk2_0,esk4_0))|~r1(X2,X1)|~r1(esk2_0,X2)),inference(cn,[status(thm)],[8593,theory(equality)])).
% cnf(8596,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk15_3(esk2_0,esk9_1(esk2_0),X1))|p1(X1)|~r1(esk9_1(esk2_0),X1)),inference(spm,[status(thm)],[8588,1568,theory(equality)])).
% cnf(8607,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(X1)|~p1(esk16_3(esk2_0,esk9_1(esk2_0),X1))|~r1(esk9_1(esk2_0),X1)),inference(spm,[status(thm)],[8592,1568,theory(equality)])).
% cnf(8618,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(X1)|r1(X1,esk15_3(esk2_0,esk9_1(esk2_0),X1))|~r1(esk9_1(esk2_0),X1)),inference(spm,[status(thm)],[8590,1568,theory(equality)])).
% cnf(8649,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))),inference(spm,[status(thm)],[8596,6448,theory(equality)])).
% cnf(8659,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|~p1(esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(spm,[status(thm)],[8607,6448,theory(equality)])).
% cnf(8672,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(spm,[status(thm)],[8618,6448,theory(equality)])).
% cnf(8699,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|~p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(spm,[status(thm)],[6645,8672,theory(equality)])).
% cnf(8716,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(X1)|r1(esk15_3(esk2_0,esk9_1(esk2_0),X1),esk16_3(esk2_0,esk9_1(esk2_0),X1))|~r1(esk9_1(esk2_0),X1)),inference(spm,[status(thm)],[8594,1568,theory(equality)])).
% cnf(8760,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(spm,[status(thm)],[8716,6448,theory(equality)])).
% cnf(8852,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(csr,[status(thm)],[8699,8649])).
% cnf(8853,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[8852,8760,theory(equality)])).
% cnf(8854,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))),inference(csr,[status(thm)],[8853,8659])).
% cnf(8865,plain,(p1(esk8_2(esk2_0,esk4_0))|r1(X1,esk14_2(X2,X1))|p1(esk10_1(esk2_0))|~epred1_1(X2)|~r1(X1,esk7_2(esk2_0,esk4_0))|~r1(X2,X1)),inference(spm,[status(thm)],[61,8854,theory(equality)])).
% cnf(8888,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk4_0,esk14_2(X1,esk4_0))|~epred1_1(X1)|~r1(X1,esk4_0)),inference(spm,[status(thm)],[8865,6308,theory(equality)])).
% cnf(8889,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[8888,15,theory(equality)])).
% cnf(8890,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|$false),inference(rw,[status(thm)],[8889,74,theory(equality)])).
% cnf(8891,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))),inference(cn,[status(thm)],[8890,theory(equality)])).
% cnf(8906,negated_conjecture,(p1(esk14_2(esk2_0,esk4_0))|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))),inference(spm,[status(thm)],[16,8891,theory(equality)])).
% cnf(8926,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|~epred1_1(esk2_0)|~r1(X2,X1)|~r1(esk4_0,X2)|~r1(esk2_0,esk4_0)),inference(spm,[status(thm)],[60,8906,theory(equality)])).
% cnf(8927,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|$false|~r1(X2,X1)|~r1(esk4_0,X2)|~r1(esk2_0,esk4_0)),inference(rw,[status(thm)],[8926,74,theory(equality)])).
% cnf(8928,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|$false|~r1(X2,X1)|~r1(esk4_0,X2)|$false),inference(rw,[status(thm)],[8927,15,theory(equality)])).
% cnf(8929,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|~r1(X2,X1)|~r1(esk4_0,X2)),inference(cn,[status(thm)],[8928,theory(equality)])).
% cnf(8931,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))|p1(X1)|~r1(esk7_2(esk2_0,esk4_0),X1)),inference(spm,[status(thm)],[8929,6308,theory(equality)])).
% cnf(8934,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk10_1(esk2_0))),inference(spm,[status(thm)],[8931,8854,theory(equality)])).
% cnf(8937,plain,(p1(X1)|r1(esk7_2(esk2_0,X2),esk8_2(esk2_0,X2))|p1(esk8_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[32,8934,theory(equality)])).
% cnf(8945,plain,(p1(X1)|r1(esk7_2(esk2_0,X2),esk8_2(esk2_0,X2))|p1(esk8_2(esk2_0,esk4_0))|$false|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[8937,74,theory(equality)])).
% cnf(8946,plain,(p1(X1)|r1(esk7_2(esk2_0,X2),esk8_2(esk2_0,X2))|p1(esk8_2(esk2_0,esk4_0))|$false|$false|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[8945,627,theory(equality)])).
% cnf(8947,plain,(p1(X1)|r1(esk7_2(esk2_0,X2),esk8_2(esk2_0,X2))|p1(esk8_2(esk2_0,esk4_0))|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[8946,theory(equality)])).
% cnf(9137,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(X1)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))|~r1(esk2_0,X1)),inference(spm,[status(thm)],[8947,15,theory(equality)])).
% cnf(9142,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(esk3_0)|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[9137,13,theory(equality)])).
% cnf(9145,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk7_2(esk2_0,esk4_0),esk8_2(esk2_0,esk4_0))),inference(sr,[status(thm)],[9142,12,theory(equality)])).
% cnf(9156,plain,(p1(esk8_2(esk2_0,esk4_0))|r1(X1,esk14_2(X2,X1))|~epred1_1(X2)|~r1(X1,esk7_2(esk2_0,esk4_0))|~r1(X2,X1)),inference(spm,[status(thm)],[61,9145,theory(equality)])).
% cnf(9220,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk4_0,esk14_2(X1,esk4_0))|~epred1_1(X1)|~r1(X1,esk4_0)),inference(spm,[status(thm)],[9156,6308,theory(equality)])).
% cnf(9221,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|~epred1_1(esk2_0)),inference(spm,[status(thm)],[9220,15,theory(equality)])).
% cnf(9222,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))|$false),inference(rw,[status(thm)],[9221,74,theory(equality)])).
% cnf(9223,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|r1(esk4_0,esk14_2(esk2_0,esk4_0))),inference(cn,[status(thm)],[9222,theory(equality)])).
% cnf(9238,negated_conjecture,(p1(esk14_2(esk2_0,esk4_0))|p1(esk8_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[16,9223,theory(equality)])).
% cnf(9258,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|~epred1_1(esk2_0)|~r1(X2,X1)|~r1(esk4_0,X2)|~r1(esk2_0,esk4_0)),inference(spm,[status(thm)],[60,9238,theory(equality)])).
% cnf(9259,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|$false|~r1(X2,X1)|~r1(esk4_0,X2)|~r1(esk2_0,esk4_0)),inference(rw,[status(thm)],[9258,74,theory(equality)])).
% cnf(9260,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|$false|~r1(X2,X1)|~r1(esk4_0,X2)|$false),inference(rw,[status(thm)],[9259,15,theory(equality)])).
% cnf(9261,plain,(p1(X1)|p1(esk8_2(esk2_0,esk4_0))|~r1(X2,X1)|~r1(esk4_0,X2)),inference(cn,[status(thm)],[9260,theory(equality)])).
% cnf(9263,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))|p1(X1)|~r1(esk7_2(esk2_0,esk4_0),X1)),inference(spm,[status(thm)],[9261,6308,theory(equality)])).
% cnf(9265,negated_conjecture,(p1(esk8_2(esk2_0,esk4_0))),inference(spm,[status(thm)],[9263,9145,theory(equality)])).
% cnf(9268,plain,(p1(X1)|r1(esk9_1(esk2_0),esk10_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk2_0)|~r1(esk2_0,esk4_0)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[35,9265,theory(equality)])).
% cnf(9336,plain,(p1(X1)|r1(esk9_1(esk2_0),esk10_1(esk2_0))|$false|~p1(esk2_0)|~r1(esk2_0,esk4_0)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[9268,74,theory(equality)])).
% cnf(9337,plain,(p1(X1)|r1(esk9_1(esk2_0),esk10_1(esk2_0))|$false|$false|~r1(esk2_0,esk4_0)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[9336,627,theory(equality)])).
% cnf(9338,plain,(p1(X1)|r1(esk9_1(esk2_0),esk10_1(esk2_0))|$false|$false|$false|~r1(esk2_0,X1)),inference(rw,[status(thm)],[9337,15,theory(equality)])).
% cnf(9339,plain,(p1(X1)|r1(esk9_1(esk2_0),esk10_1(esk2_0))|~r1(esk2_0,X1)),inference(cn,[status(thm)],[9338,theory(equality)])).
% cnf(9344,negated_conjecture,(p1(esk3_0)|r1(esk9_1(esk2_0),esk10_1(esk2_0))),inference(spm,[status(thm)],[9339,13,theory(equality)])).
% cnf(9347,negated_conjecture,(r1(esk9_1(esk2_0),esk10_1(esk2_0))),inference(sr,[status(thm)],[9344,12,theory(equality)])).
% cnf(9368,plain,(p1(X1)|p1(X2)|p1(esk10_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk8_2(esk2_0,X3))|~p1(X4)|~p1(esk2_0)|~r1(X4,X2)|~r1(esk10_1(esk2_0),X4)|~r1(esk2_0,X3)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[43,9347,theory(equality)])).
% cnf(9374,negated_conjecture,(p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(X1)|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|~r1(esk5_1(esk17_1(esk2_0)),X1)),inference(spm,[status(thm)],[7743,9347,theory(equality)])).
% cnf(9375,negated_conjecture,(p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(X1)|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|~r1(esk5_1(esk17_1(esk2_0)),X1)),inference(spm,[status(thm)],[7646,9347,theory(equality)])).
% cnf(9376,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(X1)|~r1(esk5_1(esk17_1(esk2_0)),X1)),inference(spm,[status(thm)],[7547,9347,theory(equality)])).
% cnf(9377,negated_conjecture,(p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(X1)|~p1(esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|~r1(esk5_1(esk17_1(esk2_0)),X1)),inference(spm,[status(thm)],[7580,9347,theory(equality)])).
% cnf(9548,plain,(p1(X1)|p1(X2)|p1(esk10_1(esk2_0))|$false|~p1(esk8_2(esk2_0,X3))|~p1(X4)|~p1(esk2_0)|~r1(X4,X2)|~r1(esk10_1(esk2_0),X4)|~r1(esk2_0,X3)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[9368,74,theory(equality)])).
% cnf(9549,plain,(p1(X1)|p1(X2)|p1(esk10_1(esk2_0))|$false|~p1(esk8_2(esk2_0,X3))|~p1(X4)|$false|~r1(X4,X2)|~r1(esk10_1(esk2_0),X4)|~r1(esk2_0,X3)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[9548,627,theory(equality)])).
% cnf(9550,plain,(p1(X1)|p1(X2)|p1(esk10_1(esk2_0))|~p1(esk8_2(esk2_0,X3))|~p1(X4)|~r1(X4,X2)|~r1(esk10_1(esk2_0),X4)|~r1(esk2_0,X3)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[9549,theory(equality)])).
% cnf(9568,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|p1(esk6_1(esk17_1(esk2_0)))),inference(spm,[status(thm)],[9376,7309,theory(equality)])).
% cnf(9569,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))),inference(csr,[status(thm)],[9568,7307])).
% cnf(9591,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|p1(esk6_1(esk17_1(esk2_0)))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(spm,[status(thm)],[9375,7309,theory(equality)])).
% cnf(9592,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(csr,[status(thm)],[9591,7307])).
% cnf(9618,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|p1(X2)|~p1(esk8_2(esk2_0,esk4_0))|~p1(X3)|~r1(esk10_1(esk2_0),X3)|~r1(esk2_0,X2)|~r1(X3,X1)),inference(spm,[status(thm)],[9550,15,theory(equality)])).
% cnf(9620,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|p1(X2)|$false|~p1(X3)|~r1(esk10_1(esk2_0),X3)|~r1(esk2_0,X2)|~r1(X3,X1)),inference(rw,[status(thm)],[9618,9265,theory(equality)])).
% cnf(9621,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|p1(X2)|~p1(X3)|~r1(esk10_1(esk2_0),X3)|~r1(esk2_0,X2)|~r1(X3,X1)),inference(cn,[status(thm)],[9620,theory(equality)])).
% cnf(9625,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk3_0)|p1(X1)|~p1(X2)|~r1(esk10_1(esk2_0),X2)|~r1(X2,X1)),inference(spm,[status(thm)],[9621,13,theory(equality)])).
% cnf(9628,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|~p1(X2)|~r1(esk10_1(esk2_0),X2)|~r1(X2,X1)),inference(sr,[status(thm)],[9625,12,theory(equality)])).
% cnf(9629,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|p1(esk17_1(esk2_0))|~p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(spm,[status(thm)],[9628,9592,theory(equality)])).
% cnf(9634,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|p1(X1)|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(csr,[status(thm)],[9629,9569])).
% cnf(9655,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|p1(esk6_1(esk17_1(esk2_0)))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(spm,[status(thm)],[9374,7309,theory(equality)])).
% cnf(9656,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(csr,[status(thm)],[9655,7307])).
% cnf(9671,negated_conjecture,(p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(spm,[status(thm)],[9634,9656,theory(equality)])).
% cnf(9673,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk17_1(esk2_0))|p1(X1)|~r1(esk5_1(esk17_1(esk2_0)),X1)),inference(spm,[status(thm)],[9377,9671,theory(equality)])).
% cnf(9679,negated_conjecture,(p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))|p1(esk6_1(esk17_1(esk2_0)))),inference(spm,[status(thm)],[9673,7309,theory(equality)])).
% cnf(9680,negated_conjecture,(p1(esk17_1(esk2_0))|p1(esk10_1(esk2_0))),inference(csr,[status(thm)],[9679,7307])).
% cnf(9682,plain,(p1(X1)|p1(esk17_1(esk2_0))|~epred1_1(esk2_0)|~p1(esk8_2(esk2_0,X2))|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[31,9680,theory(equality)])).
% cnf(9688,plain,(p1(X1)|p1(esk17_1(esk2_0))|$false|~p1(esk8_2(esk2_0,X2))|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[9682,74,theory(equality)])).
% cnf(9689,plain,(p1(X1)|p1(esk17_1(esk2_0))|$false|~p1(esk8_2(esk2_0,X2))|$false|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[9688,627,theory(equality)])).
% cnf(9690,plain,(p1(X1)|p1(esk17_1(esk2_0))|~p1(esk8_2(esk2_0,X2))|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[9689,theory(equality)])).
% cnf(9723,negated_conjecture,(p1(esk17_1(esk2_0))|p1(X1)|~p1(esk8_2(esk2_0,esk4_0))|~r1(esk2_0,X1)),inference(spm,[status(thm)],[9690,15,theory(equality)])).
% cnf(9725,negated_conjecture,(p1(esk17_1(esk2_0))|p1(X1)|$false|~r1(esk2_0,X1)),inference(rw,[status(thm)],[9723,9265,theory(equality)])).
% cnf(9726,negated_conjecture,(p1(esk17_1(esk2_0))|p1(X1)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[9725,theory(equality)])).
% cnf(9727,negated_conjecture,(p1(esk17_1(esk2_0))),inference(spm,[status(thm)],[9726,7291,theory(equality)])).
% cnf(9734,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(X2)|~epred1_1(esk2_0)|~r1(X1,X2)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[62,9727,theory(equality)])).
% cnf(9735,plain,(p1(X1)|r1(X1,esk15_3(esk2_0,X2,X1))|~epred1_1(esk2_0)|~r1(X2,X1)|~r1(esk2_0,X2)),inference(spm,[status(thm)],[65,9727,theory(equality)])).
% cnf(9736,plain,(p1(X1)|~epred1_1(esk2_0)|~p1(esk16_3(esk2_0,X2,X1))|~r1(X2,X1)|~r1(esk2_0,X2)),inference(spm,[status(thm)],[63,9727,theory(equality)])).
% cnf(9737,plain,(p1(X1)|r1(esk15_3(esk2_0,X2,X1),esk16_3(esk2_0,X2,X1))|~epred1_1(esk2_0)|~r1(X2,X1)|~r1(esk2_0,X2)),inference(spm,[status(thm)],[64,9727,theory(equality)])).
% cnf(9808,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(X2)|$false|~r1(X1,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[9734,74,theory(equality)])).
% cnf(9809,plain,(p1(esk15_3(esk2_0,X1,X2))|p1(X2)|~r1(X1,X2)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[9808,theory(equality)])).
% cnf(9810,plain,(p1(X1)|r1(X1,esk15_3(esk2_0,X2,X1))|$false|~r1(X2,X1)|~r1(esk2_0,X2)),inference(rw,[status(thm)],[9735,74,theory(equality)])).
% cnf(9811,plain,(p1(X1)|r1(X1,esk15_3(esk2_0,X2,X1))|~r1(X2,X1)|~r1(esk2_0,X2)),inference(cn,[status(thm)],[9810,theory(equality)])).
% cnf(9812,plain,(p1(X1)|$false|~p1(esk16_3(esk2_0,X2,X1))|~r1(X2,X1)|~r1(esk2_0,X2)),inference(rw,[status(thm)],[9736,74,theory(equality)])).
% cnf(9813,plain,(p1(X1)|~p1(esk16_3(esk2_0,X2,X1))|~r1(X2,X1)|~r1(esk2_0,X2)),inference(cn,[status(thm)],[9812,theory(equality)])).
% cnf(9814,plain,(p1(X1)|r1(esk15_3(esk2_0,X2,X1),esk16_3(esk2_0,X2,X1))|$false|~r1(X2,X1)|~r1(esk2_0,X2)),inference(rw,[status(thm)],[9737,74,theory(equality)])).
% cnf(9815,plain,(p1(X1)|r1(esk15_3(esk2_0,X2,X1),esk16_3(esk2_0,X2,X1))|~r1(X2,X1)|~r1(esk2_0,X2)),inference(cn,[status(thm)],[9814,theory(equality)])).
% cnf(9817,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),X1))|p1(X1)|~r1(esk9_1(esk2_0),X1)),inference(spm,[status(thm)],[9809,1568,theory(equality)])).
% cnf(9827,negated_conjecture,(p1(X1)|~p1(esk16_3(esk2_0,esk9_1(esk2_0),X1))|~r1(esk9_1(esk2_0),X1)),inference(spm,[status(thm)],[9813,1568,theory(equality)])).
% cnf(9837,negated_conjecture,(p1(X1)|r1(X1,esk15_3(esk2_0,esk9_1(esk2_0),X1))|~r1(esk9_1(esk2_0),X1)),inference(spm,[status(thm)],[9811,1568,theory(equality)])).
% cnf(9860,negated_conjecture,(p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|p1(esk10_1(esk2_0))),inference(spm,[status(thm)],[9817,9347,theory(equality)])).
% cnf(9861,negated_conjecture,(p1(esk10_1(esk2_0))|~p1(esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(spm,[status(thm)],[9827,9347,theory(equality)])).
% cnf(9868,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk10_1(esk2_0),esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(spm,[status(thm)],[9837,9347,theory(equality)])).
% cnf(9884,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|~p1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(spm,[status(thm)],[9628,9868,theory(equality)])).
% cnf(9886,negated_conjecture,(p1(X1)|r1(esk15_3(esk2_0,esk9_1(esk2_0),X1),esk16_3(esk2_0,esk9_1(esk2_0),X1))|~r1(esk9_1(esk2_0),X1)),inference(spm,[status(thm)],[9815,1568,theory(equality)])).
% cnf(9913,negated_conjecture,(p1(esk10_1(esk2_0))|r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(spm,[status(thm)],[9886,9347,theory(equality)])).
% cnf(9928,negated_conjecture,(p1(esk10_1(esk2_0))|p1(X1)|~r1(esk15_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)),X1)),inference(csr,[status(thm)],[9884,9860])).
% cnf(9929,negated_conjecture,(p1(esk10_1(esk2_0))|p1(esk16_3(esk2_0,esk9_1(esk2_0),esk10_1(esk2_0)))),inference(spm,[status(thm)],[9928,9913,theory(equality)])).
% cnf(9930,negated_conjecture,(p1(esk10_1(esk2_0))),inference(csr,[status(thm)],[9929,9861])).
% cnf(9932,plain,(p1(X1)|~epred1_1(esk2_0)|~p1(esk8_2(esk2_0,X2))|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(spm,[status(thm)],[31,9930,theory(equality)])).
% cnf(9950,plain,(p1(X1)|$false|~p1(esk8_2(esk2_0,X2))|~p1(esk2_0)|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[9932,74,theory(equality)])).
% cnf(9951,plain,(p1(X1)|$false|~p1(esk8_2(esk2_0,X2))|$false|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(rw,[status(thm)],[9950,627,theory(equality)])).
% cnf(9952,plain,(p1(X1)|~p1(esk8_2(esk2_0,X2))|~r1(esk2_0,X2)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[9951,theory(equality)])).
% cnf(9967,negated_conjecture,(p1(X1)|~p1(esk8_2(esk2_0,esk4_0))|~r1(esk2_0,X1)),inference(spm,[status(thm)],[9952,15,theory(equality)])).
% cnf(9969,negated_conjecture,(p1(X1)|$false|~r1(esk2_0,X1)),inference(rw,[status(thm)],[9967,9265,theory(equality)])).
% cnf(9970,negated_conjecture,(p1(X1)|~r1(esk2_0,X1)),inference(cn,[status(thm)],[9969,theory(equality)])).
% cnf(9974,negated_conjecture,(p1(esk3_0)),inference(spm,[status(thm)],[9970,13,theory(equality)])).
% cnf(9978,negated_conjecture,($false),inference(sr,[status(thm)],[9974,12,theory(equality)])).
% cnf(9979,negated_conjecture,($false),9978,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 2122
% # ...of these trivial : 6
% # ...subsumed : 583
% # ...remaining for further processing: 1533
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 812
% # Backward-rewritten : 515
% # Generated clauses : 5032
% # ...of the previous two non-trivial : 4170
% # Contextual simplify-reflections : 1666
% # Paramodulations : 5032
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 148
% # Positive orientable unit clauses: 21
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 2
% # Non-unit-clauses : 125
% # Current number of unprocessed clauses: 25
% # ...number of literals in the above : 164
% # Clause-clause subsumption calls (NU) : 20091
% # Rec. Clause-clause subsumption calls : 4102
% # Unit Clause-clause subsumption calls : 399
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 13
% # Indexed BW rewrite successes : 13
% # Backwards rewriting index: 202 leaves, 1.47+/-1.535 terms/leaf
% # Paramod-from index: 24 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-into index: 76 leaves, 1.32+/-0.892 terms/leaf
% # -------------------------------------------------
% # User time : 0.669 s
% # System time : 0.014 s
% # Total time : 0.683 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.89 CPU 1.03 WC
% FINAL PrfWatch: 0.89 CPU 1.03 WC
% SZS output end Solution for /tmp/SystemOnTPTP27123/LCL640+1.001.tptp
%
%------------------------------------------------------------------------------