%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LCL658+1.005 : 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:51:59 EST 2010
% Result : Theorem 85.48s
% Output : Solution 87.52s
% 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/SystemOnTPTP439/LCL658+1.005.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% not found
% Adding ~C to TBU ... ~main:
% ---- Iteration 1 (0 axioms selected)
% Looking for TBU SAT ...
% no
% Looking for TBU UNS ...
% yes - theorem proved
% ---- Selection completed
% Selected axioms are ... (0)
% Unselected axioms are ... :reflexivity (1)
% SZS status THM for /tmp/SystemOnTPTP439/LCL658+1.005.tptp
% Looking for THM ...
% found
% SZS output start Solution for /tmp/SystemOnTPTP439/LCL658+1.005.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=600 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 600s
% TreeLimitedRun: WC time limit is 1200s
% TreeLimitedRun: PID is 1014
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.017 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))|![X2]:(~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1))))|~(![X2]:(~(r1(X1,X2))|p1(X2))))))))|~(![X2]:(~(r1(X1,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))|![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))|![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))))))))))&![X2]:(~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1))))|~(![X2]:(~(r1(X1,X2))|p1(X2))))))&![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2))))|~(![X1]:(~(r1(X2,X1))|p1(X1))))))))),file('/tmp/SRASS.s.p', main)).
% fof(2, negated_conjecture,~(~(?[X1]:~(((~(![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1))))|~(![X2]:(~(r1(X1,X2))|p1(X2))))))))|~(![X2]:(~(r1(X1,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))|![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))|![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))))))))))&![X2]:(~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1))))|~(![X2]:(~(r1(X1,X2))|p1(X2))))))&![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2))))|~(![X1]:(~(r1(X2,X1))|p1(X1)))))))))),inference(assume_negation,[status(cth)],[1])).
% fof(3, negated_conjecture,~(~(?[X1]:~(((~(![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1))))|~(![X2]:(~(r1(X1,X2))|p1(X2))))))))|~(![X2]:(~(r1(X1,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))|![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))|![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))))))))))&![X2]:(~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1))))|~(![X2]:(~(r1(X1,X2))|p1(X2))))))&![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2))))|~(![X1]:(~(r1(X2,X1))|p1(X1)))))))))),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))|![X1]:(~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1))))|~(![X2]:(~(r1(X1,X2))|p1(X2))))))))|~(![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|epred1_1(X2))))))|~(((~(![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|![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))))))))))&![X2]:(~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1))))|~(![X2]:(~(r1(X1,X2))|p1(X2))))))&![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2))))|~(![X1]:(~(r1(X2,X1))|p1(X1)))))))))),inference(apply_def,[status(esa)],[3,4,theory(equality)])).
% fof(6, negated_conjecture,?[X1]:((![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1))))|?[X2]:(r1(X1,X2)&~(p1(X2)))))))&![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|epred1_1(X2)))))&((?[X2]:(r1(X1,X2)&?[X1]:(r1(X2,X1)&?[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))))))&![X2]:(~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|p1(X1))))|?[X2]:(r1(X1,X2)&~(p1(X2))))))&![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|![X2]:(~(r1(X1,X2))|p1(X2))))|?[X1]:(r1(X2,X1)&~(p1(X1)))))),inference(fof_nnf,[status(thm)],[5])).
% fof(7, negated_conjecture,?[X3]:((![X4]:(~(r1(X3,X4))|![X5]:(~(r1(X4,X5))|![X6]:(~(r1(X5,X6))|![X7]:((~(r1(X6,X7))|![X8]:(~(r1(X7,X8))|![X9]:(~(r1(X8,X9))|p1(X9))))|?[X10]:(r1(X7,X10)&~(p1(X10)))))))&![X11]:(~(r1(X3,X11))|![X12]:(~(r1(X11,X12))|![X13]:(~(r1(X12,X13))|epred1_1(X13)))))&((?[X14]:(r1(X3,X14)&?[X15]:(r1(X14,X15)&?[X16]:(((r1(X15,X16)&?[X17]:(r1(X16,X17)&~(p1(X17))))&?[X18]:(r1(X16,X18)&![X19]:(~(r1(X18,X19))|p1(X19))))&![X20]:((~(r1(X16,X20))|p1(X20))|?[X21]:((r1(X20,X21)&?[X22]:(r1(X21,X22)&~(p1(X22))))&p1(X21))))))&![X23]:(~(r1(X3,X23))|![X24]:((~(r1(X23,X24))|![X25]:(~(r1(X24,X25))|![X26]:(~(r1(X25,X26))|p1(X26))))|?[X27]:(r1(X24,X27)&~(p1(X27))))))&![X28]:((~(r1(X3,X28))|![X29]:(~(r1(X28,X29))|![X30]:(~(r1(X29,X30))|p1(X30))))|?[X31]:(r1(X28,X31)&~(p1(X31)))))),inference(variable_rename,[status(thm)],[6])).
% fof(8, negated_conjecture,((![X4]:(~(r1(esk1_0,X4))|![X5]:(~(r1(X4,X5))|![X6]:(~(r1(X5,X6))|![X7]:((~(r1(X6,X7))|![X8]:(~(r1(X7,X8))|![X9]:(~(r1(X8,X9))|p1(X9))))|(r1(X7,esk2_4(X4,X5,X6,X7))&~(p1(esk2_4(X4,X5,X6,X7))))))))&![X11]:(~(r1(esk1_0,X11))|![X12]:(~(r1(X11,X12))|![X13]:(~(r1(X12,X13))|epred1_1(X13)))))&(((r1(esk1_0,esk3_0)&(r1(esk3_0,esk4_0)&(((r1(esk4_0,esk5_0)&(r1(esk5_0,esk6_0)&~(p1(esk6_0))))&(r1(esk5_0,esk7_0)&![X19]:(~(r1(esk7_0,X19))|p1(X19))))&![X20]:((~(r1(esk5_0,X20))|p1(X20))|((r1(X20,esk8_1(X20))&(r1(esk8_1(X20),esk9_1(X20))&~(p1(esk9_1(X20)))))&p1(esk8_1(X20)))))))&![X23]:(~(r1(esk1_0,X23))|![X24]:((~(r1(X23,X24))|![X25]:(~(r1(X24,X25))|![X26]:(~(r1(X25,X26))|p1(X26))))|(r1(X24,esk10_2(X23,X24))&~(p1(esk10_2(X23,X24)))))))&![X28]:((~(r1(esk1_0,X28))|![X29]:(~(r1(X28,X29))|![X30]:(~(r1(X29,X30))|p1(X30))))|(r1(X28,esk11_1(X28))&~(p1(esk11_1(X28))))))),inference(skolemize,[status(esa)],[7])).
% fof(9, negated_conjecture,![X4]:![X5]:![X6]:![X7]:![X8]:![X9]:![X11]:![X12]:![X13]:![X19]:![X20]:![X23]:![X24]:![X25]:![X26]:![X28]:![X29]:![X30]:((((((~(r1(X29,X30))|p1(X30))|~(r1(X28,X29)))|~(r1(esk1_0,X28)))|(r1(X28,esk11_1(X28))&~(p1(esk11_1(X28)))))&((((((~(r1(X25,X26))|p1(X26))|~(r1(X24,X25)))|~(r1(X23,X24)))|(r1(X24,esk10_2(X23,X24))&~(p1(esk10_2(X23,X24)))))|~(r1(esk1_0,X23)))&(((((~(r1(esk5_0,X20))|p1(X20))|((r1(X20,esk8_1(X20))&(r1(esk8_1(X20),esk9_1(X20))&~(p1(esk9_1(X20)))))&p1(esk8_1(X20))))&(((~(r1(esk7_0,X19))|p1(X19))&r1(esk5_0,esk7_0))&(r1(esk4_0,esk5_0)&(r1(esk5_0,esk6_0)&~(p1(esk6_0))))))&r1(esk3_0,esk4_0))&r1(esk1_0,esk3_0))))&((((~(r1(X12,X13))|epred1_1(X13))|~(r1(X11,X12)))|~(r1(esk1_0,X11)))&(((((((~(r1(X8,X9))|p1(X9))|~(r1(X7,X8)))|~(r1(X6,X7)))|(r1(X7,esk2_4(X4,X5,X6,X7))&~(p1(esk2_4(X4,X5,X6,X7)))))|~(r1(X5,X6)))|~(r1(X4,X5)))|~(r1(esk1_0,X4))))),inference(shift_quantors,[status(thm)],[8])).
% fof(10, negated_conjecture,![X4]:![X5]:![X6]:![X7]:![X8]:![X9]:![X11]:![X12]:![X13]:![X19]:![X20]:![X23]:![X24]:![X25]:![X26]:![X28]:![X29]:![X30]:((((r1(X28,esk11_1(X28))|(((~(r1(X29,X30))|p1(X30))|~(r1(X28,X29)))|~(r1(esk1_0,X28))))&(~(p1(esk11_1(X28)))|(((~(r1(X29,X30))|p1(X30))|~(r1(X28,X29)))|~(r1(esk1_0,X28)))))&((((r1(X24,esk10_2(X23,X24))|(((~(r1(X25,X26))|p1(X26))|~(r1(X24,X25)))|~(r1(X23,X24))))|~(r1(esk1_0,X23)))&((~(p1(esk10_2(X23,X24)))|(((~(r1(X25,X26))|p1(X26))|~(r1(X24,X25)))|~(r1(X23,X24))))|~(r1(esk1_0,X23))))&((((((r1(X20,esk8_1(X20))|(~(r1(esk5_0,X20))|p1(X20)))&((r1(esk8_1(X20),esk9_1(X20))|(~(r1(esk5_0,X20))|p1(X20)))&(~(p1(esk9_1(X20)))|(~(r1(esk5_0,X20))|p1(X20)))))&(p1(esk8_1(X20))|(~(r1(esk5_0,X20))|p1(X20))))&(((~(r1(esk7_0,X19))|p1(X19))&r1(esk5_0,esk7_0))&(r1(esk4_0,esk5_0)&(r1(esk5_0,esk6_0)&~(p1(esk6_0))))))&r1(esk3_0,esk4_0))&r1(esk1_0,esk3_0))))&((((~(r1(X12,X13))|epred1_1(X13))|~(r1(X11,X12)))|~(r1(esk1_0,X11)))&(((((r1(X7,esk2_4(X4,X5,X6,X7))|(((~(r1(X8,X9))|p1(X9))|~(r1(X7,X8)))|~(r1(X6,X7))))|~(r1(X5,X6)))|~(r1(X4,X5)))|~(r1(esk1_0,X4)))&((((~(p1(esk2_4(X4,X5,X6,X7)))|(((~(r1(X8,X9))|p1(X9))|~(r1(X7,X8)))|~(r1(X6,X7))))|~(r1(X5,X6)))|~(r1(X4,X5)))|~(r1(esk1_0,X4)))))),inference(distribute,[status(thm)],[9])).
% cnf(11,negated_conjecture,(p1(X6)|~r1(esk1_0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~p1(esk2_4(X1,X2,X3,X4))),inference(split_conjunct,[status(thm)],[10])).
% cnf(12,negated_conjecture,(p1(X6)|r1(X4,esk2_4(X1,X2,X3,X4))|~r1(esk1_0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)),inference(split_conjunct,[status(thm)],[10])).
% cnf(13,negated_conjecture,(epred1_1(X3)|~r1(esk1_0,X1)|~r1(X1,X2)|~r1(X2,X3)),inference(split_conjunct,[status(thm)],[10])).
% cnf(14,negated_conjecture,(r1(esk1_0,esk3_0)),inference(split_conjunct,[status(thm)],[10])).
% cnf(15,negated_conjecture,(r1(esk3_0,esk4_0)),inference(split_conjunct,[status(thm)],[10])).
% cnf(16,negated_conjecture,(~p1(esk6_0)),inference(split_conjunct,[status(thm)],[10])).
% cnf(17,negated_conjecture,(r1(esk5_0,esk6_0)),inference(split_conjunct,[status(thm)],[10])).
% cnf(18,negated_conjecture,(r1(esk4_0,esk5_0)),inference(split_conjunct,[status(thm)],[10])).
% cnf(19,negated_conjecture,(r1(esk5_0,esk7_0)),inference(split_conjunct,[status(thm)],[10])).
% cnf(20,negated_conjecture,(p1(X1)|~r1(esk7_0,X1)),inference(split_conjunct,[status(thm)],[10])).
% cnf(21,negated_conjecture,(p1(X1)|p1(esk8_1(X1))|~r1(esk5_0,X1)),inference(split_conjunct,[status(thm)],[10])).
% cnf(22,negated_conjecture,(p1(X1)|~r1(esk5_0,X1)|~p1(esk9_1(X1))),inference(split_conjunct,[status(thm)],[10])).
% cnf(23,negated_conjecture,(p1(X1)|r1(esk8_1(X1),esk9_1(X1))|~r1(esk5_0,X1)),inference(split_conjunct,[status(thm)],[10])).
% cnf(24,negated_conjecture,(p1(X1)|r1(X1,esk8_1(X1))|~r1(esk5_0,X1)),inference(split_conjunct,[status(thm)],[10])).
% fof(29, 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(30, 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)],[29])).
% fof(31, plain,![X3]:(~(epred1_1(X3))|((((((![X4]:(~(r1(X3,X4))|p1(X4))|~(p1(X3)))|![X5]:(~(r1(X3,X5))|((r1(X5,esk12_2(X3,X5))&(r1(esk12_2(X3,X5),esk13_2(X3,X5))&~(p1(esk13_2(X3,X5)))))&p1(esk12_2(X3,X5)))))|(((r1(X3,esk14_1(X3))&(r1(esk14_1(X3),esk15_1(X3))&~(p1(esk15_1(X3)))))&p1(esk14_1(X3)))&![X10]:((~(r1(esk14_1(X3),X10))|![X11]:((~(r1(X10,X11))|![X12]:(~(r1(X11,X12))|p1(X12)))|~(p1(X11))))|((r1(X10,esk16_2(X3,X10))&~(p1(esk16_2(X3,X10))))&p1(X10)))))&((p1(X3)|![X14]:(~(r1(X3,X14))|(r1(X14,esk17_2(X3,X14))&~(p1(esk17_2(X3,X14))))))|((r1(X3,esk18_1(X3))&~(p1(esk18_1(X3))))&![X17]:((~(r1(esk18_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,esk19_2(X3,X19))&~(p1(esk19_2(X3,X19))))))&(![X23]:(~(r1(X3,X23))|![X24]:((~(r1(X23,X24))|p1(X24))|((r1(X24,esk20_3(X3,X23,X24))&(r1(esk20_3(X3,X23,X24),esk21_3(X3,X23,X24))&~(p1(esk21_3(X3,X23,X24)))))&p1(esk20_3(X3,X23,X24)))))|((r1(X3,esk22_1(X3))&~(p1(esk22_1(X3))))&![X28]:((~(r1(esk22_1(X3),X28))|![X29]:(~(r1(X28,X29))|p1(X29)))|~(p1(X28))))))),inference(skolemize,[status(esa)],[30])).
% fof(32, plain,![X3]:![X4]:![X5]:![X10]:![X11]:![X12]:![X14]:![X17]:![X18]:![X19]:![X20]:![X21]:![X23]:![X24]:![X28]:![X29]:(((((((~(r1(X28,X29))|p1(X29))|~(r1(esk22_1(X3),X28)))|~(p1(X28)))&(r1(X3,esk22_1(X3))&~(p1(esk22_1(X3)))))|(((~(r1(X23,X24))|p1(X24))|((r1(X24,esk20_3(X3,X23,X24))&(r1(esk20_3(X3,X23,X24),esk21_3(X3,X23,X24))&~(p1(esk21_3(X3,X23,X24)))))&p1(esk20_3(X3,X23,X24))))|~(r1(X3,X23))))&(((((~(r1(X20,X21))|p1(X21))|~(r1(X19,X20)))|~(r1(X3,X19)))|(r1(X19,esk19_2(X3,X19))&~(p1(esk19_2(X3,X19)))))&((((((~(r1(X17,X18))|p1(X18))|~(r1(esk18_1(X3),X17)))|~(p1(X17)))&(r1(X3,esk18_1(X3))&~(p1(esk18_1(X3)))))|((~(r1(X3,X14))|(r1(X14,esk17_2(X3,X14))&~(p1(esk17_2(X3,X14)))))|p1(X3)))&(((((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk14_1(X3),X10)))|((r1(X10,esk16_2(X3,X10))&~(p1(esk16_2(X3,X10))))&p1(X10)))&((r1(X3,esk14_1(X3))&(r1(esk14_1(X3),esk15_1(X3))&~(p1(esk15_1(X3)))))&p1(esk14_1(X3))))|((~(r1(X3,X5))|((r1(X5,esk12_2(X3,X5))&(r1(esk12_2(X3,X5),esk13_2(X3,X5))&~(p1(esk13_2(X3,X5)))))&p1(esk12_2(X3,X5))))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))))))|~(epred1_1(X3))),inference(shift_quantors,[status(thm)],[31])).
% fof(33, plain,![X3]:![X4]:![X5]:![X10]:![X11]:![X12]:![X14]:![X17]:![X18]:![X19]:![X20]:![X21]:![X23]:![X24]:![X28]:![X29]:((((((((r1(X24,esk20_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|(((~(r1(X28,X29))|p1(X29))|~(r1(esk22_1(X3),X28)))|~(p1(X28))))|~(epred1_1(X3)))&(((((r1(esk20_3(X3,X23,X24),esk21_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|(((~(r1(X28,X29))|p1(X29))|~(r1(esk22_1(X3),X28)))|~(p1(X28))))|~(epred1_1(X3)))&((((~(p1(esk21_3(X3,X23,X24)))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|(((~(r1(X28,X29))|p1(X29))|~(r1(esk22_1(X3),X28)))|~(p1(X28))))|~(epred1_1(X3)))))&((((p1(esk20_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|(((~(r1(X28,X29))|p1(X29))|~(r1(esk22_1(X3),X28)))|~(p1(X28))))|~(epred1_1(X3))))&(((((((r1(X24,esk20_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|r1(X3,esk22_1(X3)))|~(epred1_1(X3)))&(((((r1(esk20_3(X3,X23,X24),esk21_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|r1(X3,esk22_1(X3)))|~(epred1_1(X3)))&((((~(p1(esk21_3(X3,X23,X24)))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|r1(X3,esk22_1(X3)))|~(epred1_1(X3)))))&((((p1(esk20_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|r1(X3,esk22_1(X3)))|~(epred1_1(X3))))&((((((r1(X24,esk20_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|~(p1(esk22_1(X3))))|~(epred1_1(X3)))&(((((r1(esk20_3(X3,X23,X24),esk21_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|~(p1(esk22_1(X3))))|~(epred1_1(X3)))&((((~(p1(esk21_3(X3,X23,X24)))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|~(p1(esk22_1(X3))))|~(epred1_1(X3)))))&((((p1(esk20_3(X3,X23,X24))|(~(r1(X23,X24))|p1(X24)))|~(r1(X3,X23)))|~(p1(esk22_1(X3))))|~(epred1_1(X3))))))&((((r1(X19,esk19_2(X3,X19))|(((~(r1(X20,X21))|p1(X21))|~(r1(X19,X20)))|~(r1(X3,X19))))|~(epred1_1(X3)))&((~(p1(esk19_2(X3,X19)))|(((~(r1(X20,X21))|p1(X21))|~(r1(X19,X20)))|~(r1(X3,X19))))|~(epred1_1(X3))))&(((((((r1(X14,esk17_2(X3,X14))|~(r1(X3,X14)))|p1(X3))|(((~(r1(X17,X18))|p1(X18))|~(r1(esk18_1(X3),X17)))|~(p1(X17))))|~(epred1_1(X3)))&((((~(p1(esk17_2(X3,X14)))|~(r1(X3,X14)))|p1(X3))|(((~(r1(X17,X18))|p1(X18))|~(r1(esk18_1(X3),X17)))|~(p1(X17))))|~(epred1_1(X3))))&((((((r1(X14,esk17_2(X3,X14))|~(r1(X3,X14)))|p1(X3))|r1(X3,esk18_1(X3)))|~(epred1_1(X3)))&((((~(p1(esk17_2(X3,X14)))|~(r1(X3,X14)))|p1(X3))|r1(X3,esk18_1(X3)))|~(epred1_1(X3))))&(((((r1(X14,esk17_2(X3,X14))|~(r1(X3,X14)))|p1(X3))|~(p1(esk18_1(X3))))|~(epred1_1(X3)))&((((~(p1(esk17_2(X3,X14)))|~(r1(X3,X14)))|p1(X3))|~(p1(esk18_1(X3))))|~(epred1_1(X3))))))&(((((((((r1(X5,esk12_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(r1(X10,esk16_2(X3,X10))|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk14_1(X3),X10)))))|~(epred1_1(X3)))&(((((r1(esk12_2(X3,X5),esk13_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(r1(X10,esk16_2(X3,X10))|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk14_1(X3),X10)))))|~(epred1_1(X3)))&((((~(p1(esk13_2(X3,X5)))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(r1(X10,esk16_2(X3,X10))|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk14_1(X3),X10)))))|~(epred1_1(X3)))))&((((p1(esk12_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(r1(X10,esk16_2(X3,X10))|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk14_1(X3),X10)))))|~(epred1_1(X3))))&((((((r1(X5,esk12_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(~(p1(esk16_2(X3,X10)))|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk14_1(X3),X10)))))|~(epred1_1(X3)))&(((((r1(esk12_2(X3,X5),esk13_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(~(p1(esk16_2(X3,X10)))|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk14_1(X3),X10)))))|~(epred1_1(X3)))&((((~(p1(esk13_2(X3,X5)))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(~(p1(esk16_2(X3,X10)))|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk14_1(X3),X10)))))|~(epred1_1(X3)))))&((((p1(esk12_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|(~(p1(esk16_2(X3,X10)))|((((~(r1(X11,X12))|p1(X12))|~(r1(X10,X11)))|~(p1(X11)))|~(r1(esk14_1(X3),X10)))))|~(epred1_1(X3)))))&((((((r1(X5,esk12_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(esk14_1(X3),X10)))))|~(epred1_1(X3)))&(((((r1(esk12_2(X3,X5),esk13_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(esk14_1(X3),X10)))))|~(epred1_1(X3)))&((((~(p1(esk13_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(esk14_1(X3),X10)))))|~(epred1_1(X3)))))&((((p1(esk12_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(esk14_1(X3),X10)))))|~(epred1_1(X3)))))&((((((((r1(X5,esk12_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|r1(X3,esk14_1(X3)))|~(epred1_1(X3)))&(((((r1(esk12_2(X3,X5),esk13_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|r1(X3,esk14_1(X3)))|~(epred1_1(X3)))&((((~(p1(esk13_2(X3,X5)))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|r1(X3,esk14_1(X3)))|~(epred1_1(X3)))))&((((p1(esk12_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|r1(X3,esk14_1(X3)))|~(epred1_1(X3))))&(((((((r1(X5,esk12_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|r1(esk14_1(X3),esk15_1(X3)))|~(epred1_1(X3)))&(((((r1(esk12_2(X3,X5),esk13_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|r1(esk14_1(X3),esk15_1(X3)))|~(epred1_1(X3)))&((((~(p1(esk13_2(X3,X5)))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|r1(esk14_1(X3),esk15_1(X3)))|~(epred1_1(X3)))))&((((p1(esk12_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|r1(esk14_1(X3),esk15_1(X3)))|~(epred1_1(X3))))&((((((r1(X5,esk12_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|~(p1(esk15_1(X3))))|~(epred1_1(X3)))&(((((r1(esk12_2(X3,X5),esk13_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|~(p1(esk15_1(X3))))|~(epred1_1(X3)))&((((~(p1(esk13_2(X3,X5)))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|~(p1(esk15_1(X3))))|~(epred1_1(X3)))))&((((p1(esk12_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|~(p1(esk15_1(X3))))|~(epred1_1(X3))))))&((((((r1(X5,esk12_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|p1(esk14_1(X3)))|~(epred1_1(X3)))&(((((r1(esk12_2(X3,X5),esk13_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|p1(esk14_1(X3)))|~(epred1_1(X3)))&((((~(p1(esk13_2(X3,X5)))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|p1(esk14_1(X3)))|~(epred1_1(X3)))))&((((p1(esk12_2(X3,X5))|~(r1(X3,X5)))|((~(r1(X3,X4))|p1(X4))|~(p1(X3))))|p1(esk14_1(X3)))|~(epred1_1(X3))))))))),inference(distribute,[status(thm)],[32])).
% cnf(39,plain,(p1(X2)|~epred1_1(X1)|~p1(esk15_1(X1))|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)|~p1(esk13_2(X1,X3))),inference(split_conjunct,[status(thm)],[33])).
% cnf(40,plain,(p1(X2)|r1(esk12_2(X1,X3),esk13_2(X1,X3))|~epred1_1(X1)|~p1(esk15_1(X1))|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)),inference(split_conjunct,[status(thm)],[33])).
% cnf(41,plain,(p1(X2)|r1(X3,esk12_2(X1,X3))|~epred1_1(X1)|~p1(esk15_1(X1))|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)),inference(split_conjunct,[status(thm)],[33])).
% cnf(43,plain,(r1(esk14_1(X1),esk15_1(X1))|p1(X2)|~epred1_1(X1)|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)|~p1(esk13_2(X1,X3))),inference(split_conjunct,[status(thm)],[33])).
% cnf(44,plain,(r1(esk14_1(X1),esk15_1(X1))|p1(X2)|r1(esk12_2(X1,X3),esk13_2(X1,X3))|~epred1_1(X1)|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)),inference(split_conjunct,[status(thm)],[33])).
% cnf(45,plain,(r1(esk14_1(X1),esk15_1(X1))|p1(X2)|r1(X3,esk12_2(X1,X3))|~epred1_1(X1)|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)),inference(split_conjunct,[status(thm)],[33])).
% cnf(47,plain,(r1(X1,esk14_1(X1))|p1(X2)|~epred1_1(X1)|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)|~p1(esk13_2(X1,X3))),inference(split_conjunct,[status(thm)],[33])).
% cnf(48,plain,(r1(X1,esk14_1(X1))|p1(X2)|r1(esk12_2(X1,X3),esk13_2(X1,X3))|~epred1_1(X1)|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)),inference(split_conjunct,[status(thm)],[33])).
% cnf(49,plain,(r1(X1,esk14_1(X1))|p1(X2)|r1(X3,esk12_2(X1,X3))|~epred1_1(X1)|~p1(X1)|~r1(X1,X2)|~r1(X1,X3)),inference(split_conjunct,[status(thm)],[33])).
% cnf(51,plain,(p1(X4)|p1(X2)|p1(X5)|~epred1_1(X1)|~r1(esk14_1(X1),X2)|~p1(X3)|~r1(X2,X3)|~r1(X3,X4)|~p1(X1)|~r1(X1,X5)|~r1(X1,X6)|~p1(esk13_2(X1,X6))),inference(split_conjunct,[status(thm)],[33])).
% cnf(52,plain,(p1(X4)|p1(X2)|p1(X5)|r1(esk12_2(X1,X6),esk13_2(X1,X6))|~epred1_1(X1)|~r1(esk14_1(X1),X2)|~p1(X3)|~r1(X2,X3)|~r1(X3,X4)|~p1(X1)|~r1(X1,X5)|~r1(X1,X6)),inference(split_conjunct,[status(thm)],[33])).
% cnf(53,plain,(p1(X4)|p1(X2)|p1(X5)|r1(X6,esk12_2(X1,X6))|~epred1_1(X1)|~r1(esk14_1(X1),X2)|~p1(X3)|~r1(X2,X3)|~r1(X3,X4)|~p1(X1)|~r1(X1,X5)|~r1(X1,X6)),inference(split_conjunct,[status(thm)],[33])).
% cnf(62,plain,(p1(X1)|~epred1_1(X1)|~p1(esk18_1(X1))|~r1(X1,X2)|~p1(esk17_2(X1,X2))),inference(split_conjunct,[status(thm)],[33])).
% cnf(63,plain,(p1(X1)|r1(X2,esk17_2(X1,X2))|~epred1_1(X1)|~p1(esk18_1(X1))|~r1(X1,X2)),inference(split_conjunct,[status(thm)],[33])).
% cnf(64,plain,(r1(X1,esk18_1(X1))|p1(X1)|~epred1_1(X1)|~r1(X1,X2)|~p1(esk17_2(X1,X2))),inference(split_conjunct,[status(thm)],[33])).
% cnf(65,plain,(r1(X1,esk18_1(X1))|p1(X1)|r1(X2,esk17_2(X1,X2))|~epred1_1(X1)|~r1(X1,X2)),inference(split_conjunct,[status(thm)],[33])).
% cnf(66,plain,(p1(X3)|p1(X1)|~epred1_1(X1)|~p1(X2)|~r1(esk18_1(X1),X2)|~r1(X2,X3)|~r1(X1,X4)|~p1(esk17_2(X1,X4))),inference(split_conjunct,[status(thm)],[33])).
% cnf(67,plain,(p1(X3)|p1(X1)|r1(X4,esk17_2(X1,X4))|~epred1_1(X1)|~p1(X2)|~r1(esk18_1(X1),X2)|~r1(X2,X3)|~r1(X1,X4)),inference(split_conjunct,[status(thm)],[33])).
% cnf(70,plain,(p1(X3)|p1(esk20_3(X1,X2,X3))|~epred1_1(X1)|~p1(esk22_1(X1))|~r1(X1,X2)|~r1(X2,X3)),inference(split_conjunct,[status(thm)],[33])).
% cnf(71,plain,(p1(X3)|~epred1_1(X1)|~p1(esk22_1(X1))|~r1(X1,X2)|~r1(X2,X3)|~p1(esk21_3(X1,X2,X3))),inference(split_conjunct,[status(thm)],[33])).
% cnf(72,plain,(p1(X3)|r1(esk20_3(X1,X2,X3),esk21_3(X1,X2,X3))|~epred1_1(X1)|~p1(esk22_1(X1))|~r1(X1,X2)|~r1(X2,X3)),inference(split_conjunct,[status(thm)],[33])).
% cnf(73,plain,(p1(X3)|r1(X3,esk20_3(X1,X2,X3))|~epred1_1(X1)|~p1(esk22_1(X1))|~r1(X1,X2)|~r1(X2,X3)),inference(split_conjunct,[status(thm)],[33])).
% cnf(74,plain,(r1(X1,esk22_1(X1))|p1(X3)|p1(esk20_3(X1,X2,X3))|~epred1_1(X1)|~r1(X1,X2)|~r1(X2,X3)),inference(split_conjunct,[status(thm)],[33])).
% cnf(75,plain,(r1(X1,esk22_1(X1))|p1(X3)|~epred1_1(X1)|~r1(X1,X2)|~r1(X2,X3)|~p1(esk21_3(X1,X2,X3))),inference(split_conjunct,[status(thm)],[33])).
% cnf(76,plain,(r1(X1,esk22_1(X1))|p1(X3)|r1(esk20_3(X1,X2,X3),esk21_3(X1,X2,X3))|~epred1_1(X1)|~r1(X1,X2)|~r1(X2,X3)),inference(split_conjunct,[status(thm)],[33])).
% cnf(77,plain,(r1(X1,esk22_1(X1))|p1(X3)|r1(X3,esk20_3(X1,X2,X3))|~epred1_1(X1)|~r1(X1,X2)|~r1(X2,X3)),inference(split_conjunct,[status(thm)],[33])).
% cnf(78,plain,(p1(X3)|p1(X5)|p1(esk20_3(X1,X4,X5))|~epred1_1(X1)|~p1(X2)|~r1(esk22_1(X1),X2)|~r1(X2,X3)|~r1(X1,X4)|~r1(X4,X5)),inference(split_conjunct,[status(thm)],[33])).
% cnf(79,plain,(p1(X3)|p1(X5)|~epred1_1(X1)|~p1(X2)|~r1(esk22_1(X1),X2)|~r1(X2,X3)|~r1(X1,X4)|~r1(X4,X5)|~p1(esk21_3(X1,X4,X5))),inference(split_conjunct,[status(thm)],[33])).
% cnf(80,plain,(p1(X3)|p1(X5)|r1(esk20_3(X1,X4,X5),esk21_3(X1,X4,X5))|~epred1_1(X1)|~p1(X2)|~r1(esk22_1(X1),X2)|~r1(X2,X3)|~r1(X1,X4)|~r1(X4,X5)),inference(split_conjunct,[status(thm)],[33])).
% cnf(81,plain,(p1(X3)|p1(X5)|r1(X5,esk20_3(X1,X4,X5))|~epred1_1(X1)|~p1(X2)|~r1(esk22_1(X1),X2)|~r1(X2,X3)|~r1(X1,X4)|~r1(X4,X5)),inference(split_conjunct,[status(thm)],[33])).
% cnf(94,negated_conjecture,(epred1_1(X1)|~r1(X2,X1)|~r1(esk3_0,X2)),inference(spm,[status(thm)],[13,14,theory(equality)])).
% cnf(99,negated_conjecture,(p1(esk5_0)|r1(esk7_0,esk17_2(esk5_0,esk7_0))|r1(esk5_0,esk18_1(esk5_0))|~epred1_1(esk5_0)),inference(spm,[status(thm)],[65,19,theory(equality)])).
% cnf(137,negated_conjecture,(p1(X1)|~p1(esk2_4(esk3_0,X2,X3,X4))|~r1(X5,X1)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)|~r1(esk3_0,X2)),inference(spm,[status(thm)],[11,14,theory(equality)])).
% cnf(138,negated_conjecture,(p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk5_0)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[49,19,theory(equality)])).
% cnf(159,negated_conjecture,(p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk5_0)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[48,19,theory(equality)])).
% cnf(164,negated_conjecture,(p1(X1)|r1(X2,esk2_4(esk3_0,X3,X4,X2))|~r1(X5,X1)|~r1(X2,X5)|~r1(X4,X2)|~r1(X3,X4)|~r1(esk3_0,X3)),inference(spm,[status(thm)],[12,14,theory(equality)])).
% cnf(165,negated_conjecture,(p1(X1)|r1(esk14_1(esk5_0),esk15_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~p1(esk5_0)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[45,19,theory(equality)])).
% cnf(170,negated_conjecture,(p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk14_1(esk5_0),esk15_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk5_0)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[44,19,theory(equality)])).
% cnf(261,negated_conjecture,(epred1_1(X1)|~r1(esk4_0,X1)),inference(spm,[status(thm)],[94,15,theory(equality)])).
% cnf(265,negated_conjecture,(epred1_1(esk5_0)),inference(spm,[status(thm)],[261,18,theory(equality)])).
% cnf(308,negated_conjecture,(p1(esk5_0)|r1(esk7_0,esk17_2(esk5_0,esk7_0))|r1(esk5_0,esk18_1(esk5_0))|$false),inference(rw,[status(thm)],[99,265,theory(equality)])).
% cnf(309,negated_conjecture,(p1(esk5_0)|r1(esk7_0,esk17_2(esk5_0,esk7_0))|r1(esk5_0,esk18_1(esk5_0))),inference(cn,[status(thm)],[308,theory(equality)])).
% cnf(324,negated_conjecture,(p1(esk17_2(esk5_0,esk7_0))|p1(esk5_0)|r1(esk5_0,esk18_1(esk5_0))),inference(spm,[status(thm)],[20,309,theory(equality)])).
% cnf(325,plain,(p1(esk5_0)|r1(esk5_0,esk18_1(esk5_0))|~epred1_1(esk5_0)|~r1(esk5_0,esk7_0)),inference(spm,[status(thm)],[64,324,theory(equality)])).
% cnf(326,plain,(p1(esk5_0)|r1(esk5_0,esk18_1(esk5_0))|$false|~r1(esk5_0,esk7_0)),inference(rw,[status(thm)],[325,265,theory(equality)])).
% cnf(327,plain,(p1(esk5_0)|r1(esk5_0,esk18_1(esk5_0))|$false|$false),inference(rw,[status(thm)],[326,19,theory(equality)])).
% cnf(328,plain,(p1(esk5_0)|r1(esk5_0,esk18_1(esk5_0))),inference(cn,[status(thm)],[327,theory(equality)])).
% cnf(347,negated_conjecture,(p1(esk8_1(esk18_1(esk5_0)))|p1(esk18_1(esk5_0))|p1(esk5_0)),inference(spm,[status(thm)],[21,328,theory(equality)])).
% cnf(348,negated_conjecture,(p1(esk18_1(esk5_0))|p1(esk5_0)|~p1(esk9_1(esk18_1(esk5_0)))),inference(spm,[status(thm)],[22,328,theory(equality)])).
% cnf(349,negated_conjecture,(p1(esk18_1(esk5_0))|r1(esk18_1(esk5_0),esk8_1(esk18_1(esk5_0)))|p1(esk5_0)),inference(spm,[status(thm)],[24,328,theory(equality)])).
% cnf(350,negated_conjecture,(p1(esk18_1(esk5_0))|r1(esk8_1(esk18_1(esk5_0)),esk9_1(esk18_1(esk5_0)))|p1(esk5_0)),inference(spm,[status(thm)],[23,328,theory(equality)])).
% cnf(389,plain,(p1(X1)|p1(esk5_0)|r1(X2,esk17_2(esk5_0,X2))|p1(esk18_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk8_1(esk18_1(esk5_0)))|~r1(esk8_1(esk18_1(esk5_0)),X1)|~r1(esk5_0,X2)),inference(spm,[status(thm)],[67,349,theory(equality)])).
% cnf(390,plain,(p1(X1)|p1(esk5_0)|p1(esk18_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk17_2(esk5_0,X2))|~p1(esk8_1(esk18_1(esk5_0)))|~r1(esk8_1(esk18_1(esk5_0)),X1)|~r1(esk5_0,X2)),inference(spm,[status(thm)],[66,349,theory(equality)])).
% cnf(391,plain,(p1(X1)|p1(esk5_0)|r1(X2,esk17_2(esk5_0,X2))|p1(esk18_1(esk5_0))|$false|~p1(esk8_1(esk18_1(esk5_0)))|~r1(esk8_1(esk18_1(esk5_0)),X1)|~r1(esk5_0,X2)),inference(rw,[status(thm)],[389,265,theory(equality)])).
% cnf(392,plain,(p1(X1)|p1(esk5_0)|r1(X2,esk17_2(esk5_0,X2))|p1(esk18_1(esk5_0))|~p1(esk8_1(esk18_1(esk5_0)))|~r1(esk8_1(esk18_1(esk5_0)),X1)|~r1(esk5_0,X2)),inference(cn,[status(thm)],[391,theory(equality)])).
% cnf(393,plain,(p1(X1)|p1(esk5_0)|p1(esk18_1(esk5_0))|$false|~p1(esk17_2(esk5_0,X2))|~p1(esk8_1(esk18_1(esk5_0)))|~r1(esk8_1(esk18_1(esk5_0)),X1)|~r1(esk5_0,X2)),inference(rw,[status(thm)],[390,265,theory(equality)])).
% cnf(394,plain,(p1(X1)|p1(esk5_0)|p1(esk18_1(esk5_0))|~p1(esk17_2(esk5_0,X2))|~p1(esk8_1(esk18_1(esk5_0)))|~r1(esk8_1(esk18_1(esk5_0)),X1)|~r1(esk5_0,X2)),inference(cn,[status(thm)],[393,theory(equality)])).
% cnf(490,negated_conjecture,(p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))|$false|~p1(esk5_0)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[138,265,theory(equality)])).
% cnf(491,negated_conjecture,(p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))|~p1(esk5_0)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[490,theory(equality)])).
% cnf(496,negated_conjecture,(p1(X1)|~p1(esk2_4(esk3_0,esk4_0,X2,X3))|~r1(X4,X1)|~r1(X3,X4)|~r1(X2,X3)|~r1(esk4_0,X2)),inference(spm,[status(thm)],[137,15,theory(equality)])).
% cnf(559,negated_conjecture,(p1(X1)|r1(esk14_1(esk5_0),esk15_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|~p1(esk5_0)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[165,265,theory(equality)])).
% cnf(560,negated_conjecture,(p1(X1)|r1(esk14_1(esk5_0),esk15_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(esk5_0)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[559,theory(equality)])).
% cnf(571,negated_conjecture,(p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))|$false|~p1(esk5_0)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[159,265,theory(equality)])).
% cnf(572,negated_conjecture,(p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))|~p1(esk5_0)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[571,theory(equality)])).
% cnf(596,negated_conjecture,(p1(X1)|~p1(esk2_4(esk3_0,esk4_0,esk5_0,X2))|~r1(X3,X1)|~r1(X2,X3)|~r1(esk5_0,X2)),inference(spm,[status(thm)],[496,18,theory(equality)])).
% cnf(598,negated_conjecture,(p1(X1)|~p1(esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|~r1(X2,X1)|~r1(esk7_0,X2)),inference(spm,[status(thm)],[596,19,theory(equality)])).
% cnf(601,negated_conjecture,(p1(X1)|r1(X2,esk2_4(esk3_0,esk4_0,X3,X2))|~r1(X4,X1)|~r1(X2,X4)|~r1(X3,X2)|~r1(esk4_0,X3)),inference(spm,[status(thm)],[164,15,theory(equality)])).
% cnf(621,negated_conjecture,(p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk14_1(esk5_0),esk15_1(esk5_0))|$false|~p1(esk5_0)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[170,265,theory(equality)])).
% cnf(622,negated_conjecture,(p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk14_1(esk5_0),esk15_1(esk5_0))|~p1(esk5_0)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[621,theory(equality)])).
% cnf(626,negated_conjecture,(p1(X1)|r1(X2,esk2_4(esk3_0,esk4_0,esk5_0,X2))|~r1(X3,X1)|~r1(X2,X3)|~r1(esk5_0,X2)),inference(spm,[status(thm)],[601,18,theory(equality)])).
% cnf(628,negated_conjecture,(p1(X1)|r1(esk7_0,esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|~r1(X2,X1)|~r1(esk7_0,X2)),inference(spm,[status(thm)],[626,19,theory(equality)])).
% cnf(706,plain,(p1(esk18_1(esk5_0))|p1(esk5_0)|p1(X1)|~p1(esk17_2(esk5_0,X2))|~r1(esk8_1(esk18_1(esk5_0)),X1)|~r1(esk5_0,X2)),inference(csr,[status(thm)],[394,347])).
% cnf(708,negated_conjecture,(p1(esk18_1(esk5_0))|p1(esk5_0)|p1(X1)|~p1(esk17_2(esk5_0,esk7_0))|~r1(esk8_1(esk18_1(esk5_0)),X1)),inference(spm,[status(thm)],[706,19,theory(equality)])).
% cnf(747,plain,(p1(esk18_1(esk5_0))|p1(esk5_0)|p1(X1)|r1(X2,esk17_2(esk5_0,X2))|~r1(esk8_1(esk18_1(esk5_0)),X1)|~r1(esk5_0,X2)),inference(csr,[status(thm)],[392,347])).
% cnf(749,negated_conjecture,(p1(esk18_1(esk5_0))|p1(esk5_0)|p1(X1)|r1(esk7_0,esk17_2(esk5_0,esk7_0))|~r1(esk8_1(esk18_1(esk5_0)),X1)),inference(spm,[status(thm)],[747,19,theory(equality)])).
% cnf(751,negated_conjecture,(p1(esk18_1(esk5_0))|p1(esk5_0)|p1(esk9_1(esk18_1(esk5_0)))|r1(esk7_0,esk17_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[749,350,theory(equality)])).
% cnf(752,negated_conjecture,(p1(esk18_1(esk5_0))|p1(esk5_0)|r1(esk7_0,esk17_2(esk5_0,esk7_0))),inference(csr,[status(thm)],[751,348])).
% cnf(767,negated_conjecture,(p1(esk17_2(esk5_0,esk7_0))|p1(esk18_1(esk5_0))|p1(esk5_0)),inference(spm,[status(thm)],[20,752,theory(equality)])).
% cnf(789,negated_conjecture,(p1(esk18_1(esk5_0))|p1(esk5_0)|p1(X1)|~r1(esk8_1(esk18_1(esk5_0)),X1)),inference(spm,[status(thm)],[708,767,theory(equality)])).
% cnf(803,negated_conjecture,(p1(esk18_1(esk5_0))|p1(esk5_0)|p1(esk9_1(esk18_1(esk5_0)))),inference(spm,[status(thm)],[789,350,theory(equality)])).
% cnf(804,negated_conjecture,(p1(esk18_1(esk5_0))|p1(esk5_0)),inference(csr,[status(thm)],[803,348])).
% cnf(805,plain,(p1(esk5_0)|r1(X1,esk17_2(esk5_0,X1))|~epred1_1(esk5_0)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[63,804,theory(equality)])).
% cnf(806,plain,(p1(esk5_0)|~epred1_1(esk5_0)|~p1(esk17_2(esk5_0,X1))|~r1(esk5_0,X1)),inference(spm,[status(thm)],[62,804,theory(equality)])).
% cnf(807,plain,(p1(esk5_0)|r1(X1,esk17_2(esk5_0,X1))|$false|~r1(esk5_0,X1)),inference(rw,[status(thm)],[805,265,theory(equality)])).
% cnf(808,plain,(p1(esk5_0)|r1(X1,esk17_2(esk5_0,X1))|~r1(esk5_0,X1)),inference(cn,[status(thm)],[807,theory(equality)])).
% cnf(809,plain,(p1(esk5_0)|$false|~p1(esk17_2(esk5_0,X1))|~r1(esk5_0,X1)),inference(rw,[status(thm)],[806,265,theory(equality)])).
% cnf(810,plain,(p1(esk5_0)|~p1(esk17_2(esk5_0,X1))|~r1(esk5_0,X1)),inference(cn,[status(thm)],[809,theory(equality)])).
% cnf(812,negated_conjecture,(p1(esk5_0)|~p1(esk17_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[810,19,theory(equality)])).
% cnf(828,negated_conjecture,(p1(esk5_0)|r1(esk7_0,esk17_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[808,19,theory(equality)])).
% cnf(850,negated_conjecture,(p1(esk17_2(esk5_0,esk7_0))|p1(esk5_0)),inference(spm,[status(thm)],[20,828,theory(equality)])).
% cnf(871,negated_conjecture,(p1(esk5_0)),inference(csr,[status(thm)],[850,812])).
% cnf(888,negated_conjecture,(p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk14_1(esk5_0),esk15_1(esk5_0))|$false|~r1(esk5_0,X1)),inference(rw,[status(thm)],[622,871,theory(equality)])).
% cnf(889,negated_conjecture,(p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk14_1(esk5_0),esk15_1(esk5_0))|~r1(esk5_0,X1)),inference(cn,[status(thm)],[888,theory(equality)])).
% cnf(892,negated_conjecture,(p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk14_1(esk5_0),esk15_1(esk5_0))|$false|~r1(esk5_0,X1)),inference(rw,[status(thm)],[560,871,theory(equality)])).
% cnf(893,negated_conjecture,(p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk14_1(esk5_0),esk15_1(esk5_0))|~r1(esk5_0,X1)),inference(cn,[status(thm)],[892,theory(equality)])).
% cnf(896,negated_conjecture,(p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))|$false|~r1(esk5_0,X1)),inference(rw,[status(thm)],[572,871,theory(equality)])).
% cnf(897,negated_conjecture,(p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))|~r1(esk5_0,X1)),inference(cn,[status(thm)],[896,theory(equality)])).
% cnf(910,negated_conjecture,(p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))|$false|~r1(esk5_0,X1)),inference(rw,[status(thm)],[491,871,theory(equality)])).
% cnf(911,negated_conjecture,(p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))|~r1(esk5_0,X1)),inference(cn,[status(thm)],[910,theory(equality)])).
% cnf(966,negated_conjecture,(p1(esk6_0)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk14_1(esk5_0),esk15_1(esk5_0))),inference(spm,[status(thm)],[889,17,theory(equality)])).
% cnf(968,negated_conjecture,(r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk14_1(esk5_0),esk15_1(esk5_0))),inference(sr,[status(thm)],[966,16,theory(equality)])).
% cnf(1231,negated_conjecture,(p1(esk6_0)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))),inference(spm,[status(thm)],[911,17,theory(equality)])).
% cnf(1233,negated_conjecture,(r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))),inference(sr,[status(thm)],[1231,16,theory(equality)])).
% cnf(1239,negated_conjecture,(p1(esk6_0)|r1(esk14_1(esk5_0),esk15_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[893,17,theory(equality)])).
% cnf(1241,negated_conjecture,(r1(esk14_1(esk5_0),esk15_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(sr,[status(thm)],[1239,16,theory(equality)])).
% cnf(1257,negated_conjecture,(p1(X1)|r1(esk7_0,esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))|~r1(esk12_2(esk5_0,esk7_0),X1)),inference(spm,[status(thm)],[628,1233,theory(equality)])).
% cnf(1342,plain,(p1(esk20_3(X1,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk15_1(esk5_0))|r1(X1,esk22_1(X1))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~epred1_1(X1)|~r1(X1,esk14_1(esk5_0))),inference(spm,[status(thm)],[74,1241,theory(equality)])).
% cnf(1349,plain,(p1(esk15_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(X1,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(X1,esk22_1(X1))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~epred1_1(X1)|~r1(X1,esk14_1(esk5_0))),inference(spm,[status(thm)],[77,1241,theory(equality)])).
% cnf(1350,plain,(p1(esk15_1(esk5_0))|r1(esk20_3(X1,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(X1,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(X1,esk22_1(X1))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~epred1_1(X1)|~r1(X1,esk14_1(esk5_0))),inference(spm,[status(thm)],[76,1241,theory(equality)])).
% cnf(1364,plain,(p1(X1)|p1(X2)|p1(esk15_1(esk5_0))|r1(X3,esk12_2(esk5_0,X3))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~p1(X4)|~p1(esk5_0)|~r1(X4,X2)|~r1(esk15_1(esk5_0),X4)|~r1(esk5_0,X3)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[53,1241,theory(equality)])).
% cnf(1398,plain,(p1(X1)|p1(X2)|p1(esk15_1(esk5_0))|r1(X3,esk12_2(esk5_0,X3))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|~p1(X4)|~p1(esk5_0)|~r1(X4,X2)|~r1(esk15_1(esk5_0),X4)|~r1(esk5_0,X3)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[1364,265,theory(equality)])).
% cnf(1399,plain,(p1(X1)|p1(X2)|p1(esk15_1(esk5_0))|r1(X3,esk12_2(esk5_0,X3))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|~p1(X4)|$false|~r1(X4,X2)|~r1(esk15_1(esk5_0),X4)|~r1(esk5_0,X3)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[1398,871,theory(equality)])).
% cnf(1400,plain,(p1(X1)|p1(X2)|p1(esk15_1(esk5_0))|r1(X3,esk12_2(esk5_0,X3))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(X4)|~r1(X4,X2)|~r1(esk15_1(esk5_0),X4)|~r1(esk5_0,X3)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[1399,theory(equality)])).
% cnf(1499,negated_conjecture,(p1(esk6_0)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))),inference(spm,[status(thm)],[897,17,theory(equality)])).
% cnf(1501,negated_conjecture,(r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))),inference(sr,[status(thm)],[1499,16,theory(equality)])).
% cnf(1546,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|r1(esk7_0,esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))),inference(spm,[status(thm)],[1257,1501,theory(equality)])).
% cnf(1561,negated_conjecture,(p1(esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|p1(esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))),inference(spm,[status(thm)],[20,1546,theory(equality)])).
% cnf(1582,negated_conjecture,(p1(X1)|p1(esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))|~r1(esk7_0,X2)|~r1(X2,X1)),inference(spm,[status(thm)],[598,1561,theory(equality)])).
% cnf(1583,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(X1)|r1(esk5_0,esk14_1(esk5_0))|~r1(esk12_2(esk5_0,esk7_0),X1)),inference(spm,[status(thm)],[1582,1233,theory(equality)])).
% cnf(1588,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk14_1(esk5_0))),inference(spm,[status(thm)],[1583,1501,theory(equality)])).
% cnf(1590,plain,(p1(X1)|r1(esk5_0,esk14_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk5_0)|~r1(esk5_0,esk7_0)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[47,1588,theory(equality)])).
% cnf(1597,plain,(p1(X1)|r1(esk5_0,esk14_1(esk5_0))|$false|~p1(esk5_0)|~r1(esk5_0,esk7_0)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[1590,265,theory(equality)])).
% cnf(1598,plain,(p1(X1)|r1(esk5_0,esk14_1(esk5_0))|$false|$false|~r1(esk5_0,esk7_0)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[1597,871,theory(equality)])).
% cnf(1599,plain,(p1(X1)|r1(esk5_0,esk14_1(esk5_0))|$false|$false|$false|~r1(esk5_0,X1)),inference(rw,[status(thm)],[1598,19,theory(equality)])).
% cnf(1600,plain,(p1(X1)|r1(esk5_0,esk14_1(esk5_0))|~r1(esk5_0,X1)),inference(cn,[status(thm)],[1599,theory(equality)])).
% cnf(1606,negated_conjecture,(p1(esk6_0)|r1(esk5_0,esk14_1(esk5_0))),inference(spm,[status(thm)],[1600,17,theory(equality)])).
% cnf(1608,negated_conjecture,(r1(esk5_0,esk14_1(esk5_0))),inference(sr,[status(thm)],[1606,16,theory(equality)])).
% cnf(2105,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk15_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(esk5_0)),inference(spm,[status(thm)],[1342,1608,theory(equality)])).
% cnf(2106,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk15_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|$false),inference(rw,[status(thm)],[2105,265,theory(equality)])).
% cnf(2107,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk15_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))),inference(cn,[status(thm)],[2106,theory(equality)])).
% cnf(2275,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(esk5_0)),inference(spm,[status(thm)],[1349,1608,theory(equality)])).
% cnf(2276,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|$false),inference(rw,[status(thm)],[2275,265,theory(equality)])).
% cnf(2277,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))),inference(cn,[status(thm)],[2276,theory(equality)])).
% cnf(2394,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|p1(X2)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(X3)|~r1(esk15_1(esk5_0),X3)|~r1(esk5_0,X2)|~r1(X3,X1)),inference(spm,[status(thm)],[1400,19,theory(equality)])).
% cnf(2398,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk6_0)|p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(X2)|~r1(esk15_1(esk5_0),X2)|~r1(X2,X1)),inference(spm,[status(thm)],[2394,17,theory(equality)])).
% cnf(2401,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(X2)|~r1(esk15_1(esk5_0),X2)|~r1(X2,X1)),inference(sr,[status(thm)],[2398,16,theory(equality)])).
% cnf(2405,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|~p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(spm,[status(thm)],[2401,2277,theory(equality)])).
% cnf(2430,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(csr,[status(thm)],[2405,2107])).
% cnf(4290,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(esk5_0)),inference(spm,[status(thm)],[1350,1608,theory(equality)])).
% cnf(4291,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|$false),inference(rw,[status(thm)],[4290,265,theory(equality)])).
% cnf(4292,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))),inference(cn,[status(thm)],[4291,theory(equality)])).
% cnf(4309,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))),inference(spm,[status(thm)],[2430,4292,theory(equality)])).
% cnf(4314,plain,(p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~r1(esk14_1(esk5_0),esk15_1(esk5_0))|~r1(esk5_0,esk14_1(esk5_0))),inference(spm,[status(thm)],[75,4309,theory(equality)])).
% cnf(4318,plain,(p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|~r1(esk14_1(esk5_0),esk15_1(esk5_0))|~r1(esk5_0,esk14_1(esk5_0))),inference(rw,[status(thm)],[4314,265,theory(equality)])).
% cnf(4319,plain,(p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|~r1(esk14_1(esk5_0),esk15_1(esk5_0))|$false),inference(rw,[status(thm)],[4318,1608,theory(equality)])).
% cnf(4320,plain,(p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk14_1(esk5_0),esk15_1(esk5_0))),inference(cn,[status(thm)],[4319,theory(equality)])).
% cnf(4321,plain,(p1(esk15_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))),inference(csr,[status(thm)],[4320,1241])).
% cnf(4325,plain,(p1(X1)|r1(X2,esk12_2(esk5_0,X2))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[41,4321,theory(equality)])).
% cnf(4335,plain,(p1(X1)|r1(X2,esk12_2(esk5_0,X2))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|$false|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[4325,265,theory(equality)])).
% cnf(4336,plain,(p1(X1)|r1(X2,esk12_2(esk5_0,X2))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|$false|$false|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[4335,871,theory(equality)])).
% cnf(4337,plain,(p1(X1)|r1(X2,esk12_2(esk5_0,X2))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[4336,theory(equality)])).
% cnf(4371,negated_conjecture,(p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|~r1(esk5_0,X1)),inference(spm,[status(thm)],[4337,19,theory(equality)])).
% cnf(4378,negated_conjecture,(p1(esk6_0)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))),inference(spm,[status(thm)],[4371,17,theory(equality)])).
% cnf(4381,negated_conjecture,(r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))),inference(sr,[status(thm)],[4378,16,theory(equality)])).
% cnf(4405,negated_conjecture,(p1(esk8_1(esk22_1(esk5_0)))|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[21,4381,theory(equality)])).
% cnf(4406,negated_conjecture,(p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(esk9_1(esk22_1(esk5_0)))),inference(spm,[status(thm)],[22,4381,theory(equality)])).
% cnf(4407,negated_conjecture,(p1(esk22_1(esk5_0))|r1(esk22_1(esk5_0),esk8_1(esk22_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[24,4381,theory(equality)])).
% cnf(4408,negated_conjecture,(p1(esk22_1(esk5_0))|r1(esk8_1(esk22_1(esk5_0)),esk9_1(esk22_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[23,4381,theory(equality)])).
% cnf(4488,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(X2)|p1(X3)|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X1,X2)|~r1(esk8_1(esk22_1(esk5_0)),X3)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[78,4407,theory(equality)])).
% cnf(4489,plain,(p1(X1)|p1(X2)|r1(X1,esk20_3(esk5_0,X3,X1))|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(spm,[status(thm)],[81,4407,theory(equality)])).
% cnf(4490,plain,(p1(X1)|p1(X2)|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~p1(esk21_3(esk5_0,X3,X1))|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(spm,[status(thm)],[79,4407,theory(equality)])).
% cnf(4491,plain,(p1(X1)|p1(X2)|r1(esk20_3(esk5_0,X3,X1),esk21_3(esk5_0,X3,X1))|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(spm,[status(thm)],[80,4407,theory(equality)])).
% cnf(4504,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(X2)|p1(X3)|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X1,X2)|~r1(esk8_1(esk22_1(esk5_0)),X3)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[4488,265,theory(equality)])).
% cnf(4505,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(X2)|p1(X3)|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X1,X2)|~r1(esk8_1(esk22_1(esk5_0)),X3)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[4504,theory(equality)])).
% cnf(4506,plain,(p1(X1)|p1(X2)|r1(X1,esk20_3(esk5_0,X3,X1))|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(rw,[status(thm)],[4489,265,theory(equality)])).
% cnf(4507,plain,(p1(X1)|p1(X2)|r1(X1,esk20_3(esk5_0,X3,X1))|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(cn,[status(thm)],[4506,theory(equality)])).
% cnf(4508,plain,(p1(X1)|p1(X2)|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|~p1(esk21_3(esk5_0,X3,X1))|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(rw,[status(thm)],[4490,265,theory(equality)])).
% cnf(4509,plain,(p1(X1)|p1(X2)|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(esk21_3(esk5_0,X3,X1))|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(cn,[status(thm)],[4508,theory(equality)])).
% cnf(4510,plain,(p1(X1)|p1(X2)|r1(esk20_3(esk5_0,X3,X1),esk21_3(esk5_0,X3,X1))|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(rw,[status(thm)],[4491,265,theory(equality)])).
% cnf(4511,plain,(p1(X1)|p1(X2)|r1(esk20_3(esk5_0,X3,X1),esk21_3(esk5_0,X3,X1))|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(cn,[status(thm)],[4510,theory(equality)])).
% cnf(4811,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(esk22_1(esk5_0))|p1(X2)|p1(X3)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk8_1(esk22_1(esk5_0)),X3)|~r1(esk5_0,X1)|~r1(X1,X2)),inference(csr,[status(thm)],[4505,4405])).
% cnf(4816,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),X1))|p1(esk22_1(esk5_0))|p1(X2)|p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk14_1(esk5_0),X1)),inference(spm,[status(thm)],[4811,1608,theory(equality)])).
% cnf(4855,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk8_1(esk22_1(esk5_0)),X1)),inference(spm,[status(thm)],[4816,1241,theory(equality)])).
% cnf(4861,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|p1(esk9_1(esk22_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[4855,4408,theory(equality)])).
% cnf(4862,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(csr,[status(thm)],[4861,4406])).
% cnf(4878,plain,(p1(esk22_1(esk5_0))|p1(X1)|p1(X2)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(esk21_3(esk5_0,X3,X1))|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)|~r1(X3,X1)),inference(csr,[status(thm)],[4509,4405])).
% cnf(4883,negated_conjecture,(p1(esk22_1(esk5_0))|p1(X1)|p1(X2)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(esk21_3(esk5_0,esk14_1(esk5_0),X2))|~r1(esk8_1(esk22_1(esk5_0)),X1)|~r1(esk14_1(esk5_0),X2)),inference(spm,[status(thm)],[4878,1608,theory(equality)])).
% cnf(4919,negated_conjecture,(p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|~r1(esk8_1(esk22_1(esk5_0)),X1)),inference(spm,[status(thm)],[4883,1241,theory(equality)])).
% cnf(4973,plain,(p1(esk22_1(esk5_0))|p1(X1)|p1(X2)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(X1,esk20_3(esk5_0,X3,X1))|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)|~r1(X3,X1)),inference(csr,[status(thm)],[4507,4405])).
% cnf(4978,negated_conjecture,(p1(esk22_1(esk5_0))|p1(X1)|p1(X2)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(X2,esk20_3(esk5_0,esk14_1(esk5_0),X2))|~r1(esk8_1(esk22_1(esk5_0)),X1)|~r1(esk14_1(esk5_0),X2)),inference(spm,[status(thm)],[4973,1608,theory(equality)])).
% cnf(5011,negated_conjecture,(p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(X1)|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk8_1(esk22_1(esk5_0)),X1)),inference(spm,[status(thm)],[4978,1241,theory(equality)])).
% cnf(5040,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|p1(esk9_1(esk22_1(esk5_0)))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[5011,4408,theory(equality)])).
% cnf(5041,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(csr,[status(thm)],[5040,4406])).
% cnf(5067,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))|~p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(spm,[status(thm)],[2401,5041,theory(equality)])).
% cnf(5074,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(csr,[status(thm)],[5067,4862])).
% cnf(5557,plain,(p1(esk22_1(esk5_0))|p1(X1)|p1(X2)|r1(esk20_3(esk5_0,X3,X1),esk21_3(esk5_0,X3,X1))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)|~r1(X3,X1)),inference(csr,[status(thm)],[4511,4405])).
% cnf(5562,negated_conjecture,(p1(esk22_1(esk5_0))|p1(X1)|p1(X2)|r1(esk20_3(esk5_0,esk14_1(esk5_0),X2),esk21_3(esk5_0,esk14_1(esk5_0),X2))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk8_1(esk22_1(esk5_0)),X1)|~r1(esk14_1(esk5_0),X2)),inference(spm,[status(thm)],[5557,1608,theory(equality)])).
% cnf(6190,negated_conjecture,(p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(X1)|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk8_1(esk22_1(esk5_0)),X1)),inference(spm,[status(thm)],[5562,1241,theory(equality)])).
% cnf(7216,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|p1(esk9_1(esk22_1(esk5_0)))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[6190,4408,theory(equality)])).
% cnf(7222,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(csr,[status(thm)],[7216,4406])).
% cnf(7237,negated_conjecture,(p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[5074,7222,theory(equality)])).
% cnf(7239,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk8_1(esk22_1(esk5_0)),X1)),inference(spm,[status(thm)],[4919,7237,theory(equality)])).
% cnf(7243,negated_conjecture,(p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(esk9_1(esk22_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[7239,4408,theory(equality)])).
% cnf(7244,negated_conjecture,(p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(csr,[status(thm)],[7243,4406])).
% cnf(7248,plain,(p1(X1)|r1(X2,esk12_2(esk5_0,X2))|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[41,7244,theory(equality)])).
% cnf(7258,plain,(p1(X1)|r1(X2,esk12_2(esk5_0,X2))|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[7248,265,theory(equality)])).
% cnf(7259,plain,(p1(X1)|r1(X2,esk12_2(esk5_0,X2))|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|$false|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[7258,871,theory(equality)])).
% cnf(7260,plain,(p1(X1)|r1(X2,esk12_2(esk5_0,X2))|p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[7259,theory(equality)])).
% cnf(7287,negated_conjecture,(p1(esk22_1(esk5_0))|p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk5_0,X1)),inference(spm,[status(thm)],[7260,19,theory(equality)])).
% cnf(7290,negated_conjecture,(p1(esk22_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[7287,4381,theory(equality)])).
% cnf(7297,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(X2)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~r1(X1,X2)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[70,7290,theory(equality)])).
% cnf(7298,plain,(p1(X1)|r1(X1,esk20_3(esk5_0,X2,X1))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~r1(X2,X1)|~r1(esk5_0,X2)),inference(spm,[status(thm)],[73,7290,theory(equality)])).
% cnf(7299,plain,(p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~p1(esk21_3(esk5_0,X2,X1))|~r1(X2,X1)|~r1(esk5_0,X2)),inference(spm,[status(thm)],[71,7290,theory(equality)])).
% cnf(7300,plain,(p1(X1)|r1(esk20_3(esk5_0,X2,X1),esk21_3(esk5_0,X2,X1))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~r1(X2,X1)|~r1(esk5_0,X2)),inference(spm,[status(thm)],[72,7290,theory(equality)])).
% cnf(7301,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(X2)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|~r1(X1,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[7297,265,theory(equality)])).
% cnf(7302,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(X2)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(X1,X2)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[7301,theory(equality)])).
% cnf(7303,plain,(p1(X1)|r1(X1,esk20_3(esk5_0,X2,X1))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|~r1(X2,X1)|~r1(esk5_0,X2)),inference(rw,[status(thm)],[7298,265,theory(equality)])).
% cnf(7304,plain,(p1(X1)|r1(X1,esk20_3(esk5_0,X2,X1))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(X2,X1)|~r1(esk5_0,X2)),inference(cn,[status(thm)],[7303,theory(equality)])).
% cnf(7305,plain,(p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|~p1(esk21_3(esk5_0,X2,X1))|~r1(X2,X1)|~r1(esk5_0,X2)),inference(rw,[status(thm)],[7299,265,theory(equality)])).
% cnf(7306,plain,(p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(esk21_3(esk5_0,X2,X1))|~r1(X2,X1)|~r1(esk5_0,X2)),inference(cn,[status(thm)],[7305,theory(equality)])).
% cnf(7307,plain,(p1(X1)|r1(esk20_3(esk5_0,X2,X1),esk21_3(esk5_0,X2,X1))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|~r1(X2,X1)|~r1(esk5_0,X2)),inference(rw,[status(thm)],[7300,265,theory(equality)])).
% cnf(7308,plain,(p1(X1)|r1(esk20_3(esk5_0,X2,X1),esk21_3(esk5_0,X2,X1))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(X2,X1)|~r1(esk5_0,X2)),inference(cn,[status(thm)],[7307,theory(equality)])).
% cnf(7310,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),X1))|p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk14_1(esk5_0),X1)),inference(spm,[status(thm)],[7302,1608,theory(equality)])).
% cnf(7322,negated_conjecture,(p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(esk21_3(esk5_0,esk14_1(esk5_0),X1))|~r1(esk14_1(esk5_0),X1)),inference(spm,[status(thm)],[7306,1608,theory(equality)])).
% cnf(7334,negated_conjecture,(p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|r1(X1,esk20_3(esk5_0,esk14_1(esk5_0),X1))|~r1(esk14_1(esk5_0),X1)),inference(spm,[status(thm)],[7304,1608,theory(equality)])).
% cnf(7347,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk15_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[7310,1241,theory(equality)])).
% cnf(7388,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(spm,[status(thm)],[7322,1241,theory(equality)])).
% cnf(7397,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[7334,1241,theory(equality)])).
% cnf(7418,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(spm,[status(thm)],[2401,7397,theory(equality)])).
% cnf(7423,negated_conjecture,(p1(X1)|r1(esk20_3(esk5_0,esk14_1(esk5_0),X1),esk21_3(esk5_0,esk14_1(esk5_0),X1))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk14_1(esk5_0),X1)),inference(spm,[status(thm)],[7308,1608,theory(equality)])).
% cnf(7469,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[7423,1241,theory(equality)])).
% cnf(7501,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(csr,[status(thm)],[7418,7347])).
% cnf(7502,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[7501,7469,theory(equality)])).
% cnf(7503,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(csr,[status(thm)],[7502,7388])).
% cnf(7507,plain,(p1(X1)|r1(X2,esk12_2(esk5_0,X2))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[41,7503,theory(equality)])).
% cnf(7517,plain,(p1(X1)|r1(X2,esk12_2(esk5_0,X2))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[7507,265,theory(equality)])).
% cnf(7518,plain,(p1(X1)|r1(X2,esk12_2(esk5_0,X2))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|$false|$false|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[7517,871,theory(equality)])).
% cnf(7519,plain,(p1(X1)|r1(X2,esk12_2(esk5_0,X2))|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[7518,theory(equality)])).
% cnf(7546,negated_conjecture,(p1(X1)|r1(esk7_0,esk12_2(esk5_0,esk7_0))|~r1(esk5_0,X1)),inference(spm,[status(thm)],[7519,19,theory(equality)])).
% cnf(7552,negated_conjecture,(p1(esk6_0)|r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[7546,17,theory(equality)])).
% cnf(7555,negated_conjecture,(r1(esk7_0,esk12_2(esk5_0,esk7_0))),inference(sr,[status(thm)],[7552,16,theory(equality)])).
% cnf(7575,negated_conjecture,(p1(X1)|r1(esk7_0,esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|~r1(esk12_2(esk5_0,esk7_0),X1)),inference(spm,[status(thm)],[628,7555,theory(equality)])).
% cnf(7644,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|r1(esk7_0,esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|r1(esk14_1(esk5_0),esk15_1(esk5_0))),inference(spm,[status(thm)],[7575,968,theory(equality)])).
% cnf(7659,negated_conjecture,(p1(esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|p1(esk13_2(esk5_0,esk7_0))|r1(esk14_1(esk5_0),esk15_1(esk5_0))),inference(spm,[status(thm)],[20,7644,theory(equality)])).
% cnf(7680,negated_conjecture,(p1(X1)|p1(esk13_2(esk5_0,esk7_0))|r1(esk14_1(esk5_0),esk15_1(esk5_0))|~r1(esk7_0,X2)|~r1(X2,X1)),inference(spm,[status(thm)],[598,7659,theory(equality)])).
% cnf(7738,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(X1)|r1(esk14_1(esk5_0),esk15_1(esk5_0))|~r1(esk12_2(esk5_0,esk7_0),X1)),inference(spm,[status(thm)],[7680,7555,theory(equality)])).
% cnf(7743,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|r1(esk14_1(esk5_0),esk15_1(esk5_0))),inference(spm,[status(thm)],[7738,968,theory(equality)])).
% cnf(7747,plain,(p1(esk20_3(X1,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk15_1(esk5_0))|r1(X1,esk22_1(X1))|p1(esk13_2(esk5_0,esk7_0))|~epred1_1(X1)|~r1(X1,esk14_1(esk5_0))),inference(spm,[status(thm)],[74,7743,theory(equality)])).
% cnf(7754,plain,(p1(esk15_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(X1,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(X1,esk22_1(X1))|p1(esk13_2(esk5_0,esk7_0))|~epred1_1(X1)|~r1(X1,esk14_1(esk5_0))),inference(spm,[status(thm)],[77,7743,theory(equality)])).
% cnf(7755,plain,(p1(esk15_1(esk5_0))|r1(esk20_3(X1,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(X1,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(X1,esk22_1(X1))|p1(esk13_2(esk5_0,esk7_0))|~epred1_1(X1)|~r1(X1,esk14_1(esk5_0))),inference(spm,[status(thm)],[76,7743,theory(equality)])).
% cnf(7767,plain,(p1(X1)|p1(X2)|p1(esk15_1(esk5_0))|r1(esk12_2(esk5_0,X3),esk13_2(esk5_0,X3))|p1(esk13_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~p1(X4)|~p1(esk5_0)|~r1(X4,X2)|~r1(esk15_1(esk5_0),X4)|~r1(esk5_0,X3)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[52,7743,theory(equality)])).
% cnf(7817,plain,(p1(X1)|p1(X2)|p1(esk15_1(esk5_0))|r1(esk12_2(esk5_0,X3),esk13_2(esk5_0,X3))|p1(esk13_2(esk5_0,esk7_0))|$false|~p1(X4)|~p1(esk5_0)|~r1(X4,X2)|~r1(esk15_1(esk5_0),X4)|~r1(esk5_0,X3)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[7767,265,theory(equality)])).
% cnf(7818,plain,(p1(X1)|p1(X2)|p1(esk15_1(esk5_0))|r1(esk12_2(esk5_0,X3),esk13_2(esk5_0,X3))|p1(esk13_2(esk5_0,esk7_0))|$false|~p1(X4)|$false|~r1(X4,X2)|~r1(esk15_1(esk5_0),X4)|~r1(esk5_0,X3)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[7817,871,theory(equality)])).
% cnf(7819,plain,(p1(X1)|p1(X2)|p1(esk15_1(esk5_0))|r1(esk12_2(esk5_0,X3),esk13_2(esk5_0,X3))|p1(esk13_2(esk5_0,esk7_0))|~p1(X4)|~r1(X4,X2)|~r1(esk15_1(esk5_0),X4)|~r1(esk5_0,X3)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[7818,theory(equality)])).
% cnf(7846,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(esk5_0)),inference(spm,[status(thm)],[7747,1608,theory(equality)])).
% cnf(7847,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|$false),inference(rw,[status(thm)],[7846,265,theory(equality)])).
% cnf(7848,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))),inference(cn,[status(thm)],[7847,theory(equality)])).
% cnf(7854,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(esk5_0)),inference(spm,[status(thm)],[7754,1608,theory(equality)])).
% cnf(7855,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk5_0,esk22_1(esk5_0))|$false),inference(rw,[status(thm)],[7854,265,theory(equality)])).
% cnf(7856,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk5_0,esk22_1(esk5_0))),inference(cn,[status(thm)],[7855,theory(equality)])).
% cnf(7926,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(X1)|p1(X2)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|~p1(X3)|~r1(esk15_1(esk5_0),X3)|~r1(esk5_0,X2)|~r1(X3,X1)),inference(spm,[status(thm)],[7819,19,theory(equality)])).
% cnf(7930,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(esk6_0)|p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|~p1(X2)|~r1(esk15_1(esk5_0),X2)|~r1(X2,X1)),inference(spm,[status(thm)],[7926,17,theory(equality)])).
% cnf(7933,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|~p1(X2)|~r1(esk15_1(esk5_0),X2)|~r1(X2,X1)),inference(sr,[status(thm)],[7930,16,theory(equality)])).
% cnf(7934,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|~p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(spm,[status(thm)],[7933,7856,theory(equality)])).
% cnf(7966,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(esk5_0)),inference(spm,[status(thm)],[7755,1608,theory(equality)])).
% cnf(7967,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk5_0,esk22_1(esk5_0))|$false),inference(rw,[status(thm)],[7966,265,theory(equality)])).
% cnf(7968,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk5_0,esk22_1(esk5_0))),inference(cn,[status(thm)],[7967,theory(equality)])).
% cnf(7998,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(csr,[status(thm)],[7934,7848])).
% cnf(7999,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))),inference(spm,[status(thm)],[7998,7968,theory(equality)])).
% cnf(8000,plain,(p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|p1(esk13_2(esk5_0,esk7_0))|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~r1(esk14_1(esk5_0),esk15_1(esk5_0))|~r1(esk5_0,esk14_1(esk5_0))),inference(spm,[status(thm)],[75,7999,theory(equality)])).
% cnf(8001,plain,(p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|p1(esk13_2(esk5_0,esk7_0))|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|$false|~r1(esk14_1(esk5_0),esk15_1(esk5_0))|~r1(esk5_0,esk14_1(esk5_0))),inference(rw,[status(thm)],[8000,265,theory(equality)])).
% cnf(8002,plain,(p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|p1(esk13_2(esk5_0,esk7_0))|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|$false|~r1(esk14_1(esk5_0),esk15_1(esk5_0))|$false),inference(rw,[status(thm)],[8001,1608,theory(equality)])).
% cnf(8003,plain,(p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|p1(esk13_2(esk5_0,esk7_0))|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|~r1(esk14_1(esk5_0),esk15_1(esk5_0))),inference(cn,[status(thm)],[8002,theory(equality)])).
% cnf(8004,plain,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))),inference(csr,[status(thm)],[8003,7743])).
% cnf(8019,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|r1(esk7_0,esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))),inference(spm,[status(thm)],[7575,8004,theory(equality)])).
% cnf(8053,negated_conjecture,(p1(esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))),inference(spm,[status(thm)],[20,8019,theory(equality)])).
% cnf(8074,negated_conjecture,(p1(X1)|p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|~r1(esk7_0,X2)|~r1(X2,X1)),inference(spm,[status(thm)],[598,8053,theory(equality)])).
% cnf(8075,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(X1)|r1(esk5_0,esk22_1(esk5_0))|~r1(esk12_2(esk5_0,esk7_0),X1)),inference(spm,[status(thm)],[8074,7555,theory(equality)])).
% cnf(8083,plain,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))),inference(spm,[status(thm)],[8075,8004,theory(equality)])).
% cnf(8086,plain,(p1(X1)|r1(esk12_2(esk5_0,X2),esk13_2(esk5_0,X2))|p1(esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[40,8083,theory(equality)])).
% cnf(8094,plain,(p1(X1)|r1(esk12_2(esk5_0,X2),esk13_2(esk5_0,X2))|p1(esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|$false|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[8086,265,theory(equality)])).
% cnf(8095,plain,(p1(X1)|r1(esk12_2(esk5_0,X2),esk13_2(esk5_0,X2))|p1(esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|$false|$false|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[8094,871,theory(equality)])).
% cnf(8096,plain,(p1(X1)|r1(esk12_2(esk5_0,X2),esk13_2(esk5_0,X2))|p1(esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[8095,theory(equality)])).
% cnf(8212,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|~r1(esk5_0,X1)),inference(spm,[status(thm)],[8096,19,theory(equality)])).
% cnf(8216,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk6_0)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))),inference(spm,[status(thm)],[8212,17,theory(equality)])).
% cnf(8219,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))),inference(sr,[status(thm)],[8216,16,theory(equality)])).
% cnf(8234,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|r1(esk7_0,esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))),inference(spm,[status(thm)],[7575,8219,theory(equality)])).
% cnf(8268,negated_conjecture,(p1(esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|p1(esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))),inference(spm,[status(thm)],[20,8234,theory(equality)])).
% cnf(8292,negated_conjecture,(p1(X1)|p1(esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))|~r1(esk7_0,X2)|~r1(X2,X1)),inference(spm,[status(thm)],[598,8268,theory(equality)])).
% cnf(8293,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(X1)|r1(esk5_0,esk22_1(esk5_0))|~r1(esk12_2(esk5_0,esk7_0),X1)),inference(spm,[status(thm)],[8292,7555,theory(equality)])).
% cnf(8296,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|r1(esk5_0,esk22_1(esk5_0))),inference(spm,[status(thm)],[8293,8219,theory(equality)])).
% cnf(8299,plain,(p1(X1)|r1(esk14_1(esk5_0),esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk5_0)|~r1(esk5_0,esk7_0)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[43,8296,theory(equality)])).
% cnf(8310,plain,(p1(X1)|r1(esk14_1(esk5_0),esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|$false|~p1(esk5_0)|~r1(esk5_0,esk7_0)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[8299,265,theory(equality)])).
% cnf(8311,plain,(p1(X1)|r1(esk14_1(esk5_0),esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|$false|$false|~r1(esk5_0,esk7_0)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[8310,871,theory(equality)])).
% cnf(8312,plain,(p1(X1)|r1(esk14_1(esk5_0),esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|$false|$false|$false|~r1(esk5_0,X1)),inference(rw,[status(thm)],[8311,19,theory(equality)])).
% cnf(8313,plain,(p1(X1)|r1(esk14_1(esk5_0),esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|~r1(esk5_0,X1)),inference(cn,[status(thm)],[8312,theory(equality)])).
% cnf(8316,negated_conjecture,(p1(esk6_0)|r1(esk14_1(esk5_0),esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))),inference(spm,[status(thm)],[8313,17,theory(equality)])).
% cnf(8319,negated_conjecture,(r1(esk14_1(esk5_0),esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))),inference(sr,[status(thm)],[8316,16,theory(equality)])).
% cnf(8323,plain,(p1(esk20_3(X1,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk15_1(esk5_0))|r1(X1,esk22_1(X1))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(X1)|~r1(X1,esk14_1(esk5_0))),inference(spm,[status(thm)],[74,8319,theory(equality)])).
% cnf(8330,plain,(p1(esk15_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(X1,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(X1,esk22_1(X1))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(X1)|~r1(X1,esk14_1(esk5_0))),inference(spm,[status(thm)],[77,8319,theory(equality)])).
% cnf(8331,plain,(p1(esk15_1(esk5_0))|r1(esk20_3(X1,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(X1,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(X1,esk22_1(X1))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(X1)|~r1(X1,esk14_1(esk5_0))),inference(spm,[status(thm)],[76,8319,theory(equality)])).
% cnf(8342,plain,(p1(X1)|p1(X2)|p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk13_2(esk5_0,X3))|~p1(X4)|~p1(esk5_0)|~r1(X4,X2)|~r1(esk15_1(esk5_0),X4)|~r1(esk5_0,X3)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[51,8319,theory(equality)])).
% cnf(8390,plain,(p1(X1)|p1(X2)|p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|$false|~p1(esk13_2(esk5_0,X3))|~p1(X4)|~p1(esk5_0)|~r1(X4,X2)|~r1(esk15_1(esk5_0),X4)|~r1(esk5_0,X3)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[8342,265,theory(equality)])).
% cnf(8391,plain,(p1(X1)|p1(X2)|p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|$false|~p1(esk13_2(esk5_0,X3))|~p1(X4)|$false|~r1(X4,X2)|~r1(esk15_1(esk5_0),X4)|~r1(esk5_0,X3)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[8390,871,theory(equality)])).
% cnf(8392,plain,(p1(X1)|p1(X2)|p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|~p1(esk13_2(esk5_0,X3))|~p1(X4)|~r1(X4,X2)|~r1(esk15_1(esk5_0),X4)|~r1(esk5_0,X3)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[8391,theory(equality)])).
% cnf(8419,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|p1(X2)|r1(esk5_0,esk22_1(esk5_0))|~p1(esk13_2(esk5_0,esk7_0))|~p1(X3)|~r1(esk15_1(esk5_0),X3)|~r1(esk5_0,X2)|~r1(X3,X1)),inference(spm,[status(thm)],[8392,19,theory(equality)])).
% cnf(8421,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(esk5_0)),inference(spm,[status(thm)],[8323,1608,theory(equality)])).
% cnf(8422,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|$false),inference(rw,[status(thm)],[8421,265,theory(equality)])).
% cnf(8423,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))),inference(cn,[status(thm)],[8422,theory(equality)])).
% cnf(8427,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|p1(X2)|r1(esk5_0,esk22_1(esk5_0))|~p1(X3)|~r1(esk15_1(esk5_0),X3)|~r1(esk5_0,X2)|~r1(X3,X1)),inference(csr,[status(thm)],[8419,8296])).
% cnf(8430,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk6_0)|p1(X1)|r1(esk5_0,esk22_1(esk5_0))|~p1(X2)|~r1(esk15_1(esk5_0),X2)|~r1(X2,X1)),inference(spm,[status(thm)],[8427,17,theory(equality)])).
% cnf(8433,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|r1(esk5_0,esk22_1(esk5_0))|~p1(X2)|~r1(esk15_1(esk5_0),X2)|~r1(X2,X1)),inference(sr,[status(thm)],[8430,16,theory(equality)])).
% cnf(8443,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(esk5_0)),inference(spm,[status(thm)],[8330,1608,theory(equality)])).
% cnf(8444,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk5_0,esk22_1(esk5_0))|$false),inference(rw,[status(thm)],[8443,265,theory(equality)])).
% cnf(8445,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk5_0,esk22_1(esk5_0))),inference(cn,[status(thm)],[8444,theory(equality)])).
% cnf(8463,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|r1(esk5_0,esk22_1(esk5_0))|~p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(spm,[status(thm)],[8433,8445,theory(equality)])).
% cnf(8476,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|r1(esk5_0,esk22_1(esk5_0))|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(csr,[status(thm)],[8463,8423])).
% cnf(8484,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(esk5_0)),inference(spm,[status(thm)],[8331,1608,theory(equality)])).
% cnf(8485,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk5_0,esk22_1(esk5_0))|$false),inference(rw,[status(thm)],[8484,265,theory(equality)])).
% cnf(8486,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk5_0,esk22_1(esk5_0))),inference(cn,[status(thm)],[8485,theory(equality)])).
% cnf(8501,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk5_0,esk22_1(esk5_0))),inference(spm,[status(thm)],[8476,8486,theory(equality)])).
% cnf(8502,plain,(p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(esk5_0)|~r1(esk14_1(esk5_0),esk15_1(esk5_0))|~r1(esk5_0,esk14_1(esk5_0))),inference(spm,[status(thm)],[75,8501,theory(equality)])).
% cnf(8503,plain,(p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|$false|~r1(esk14_1(esk5_0),esk15_1(esk5_0))|~r1(esk5_0,esk14_1(esk5_0))),inference(rw,[status(thm)],[8502,265,theory(equality)])).
% cnf(8504,plain,(p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|$false|~r1(esk14_1(esk5_0),esk15_1(esk5_0))|$false),inference(rw,[status(thm)],[8503,1608,theory(equality)])).
% cnf(8505,plain,(p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))|~r1(esk14_1(esk5_0),esk15_1(esk5_0))),inference(cn,[status(thm)],[8504,theory(equality)])).
% cnf(8506,plain,(p1(esk15_1(esk5_0))|r1(esk5_0,esk22_1(esk5_0))),inference(csr,[status(thm)],[8505,8319])).
% cnf(8508,plain,(p1(X1)|r1(esk5_0,esk22_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk13_2(esk5_0,X2))|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[39,8506,theory(equality)])).
% cnf(8514,plain,(p1(X1)|r1(esk5_0,esk22_1(esk5_0))|$false|~p1(esk13_2(esk5_0,X2))|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[8508,265,theory(equality)])).
% cnf(8515,plain,(p1(X1)|r1(esk5_0,esk22_1(esk5_0))|$false|~p1(esk13_2(esk5_0,X2))|$false|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[8514,871,theory(equality)])).
% cnf(8516,plain,(p1(X1)|r1(esk5_0,esk22_1(esk5_0))|~p1(esk13_2(esk5_0,X2))|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[8515,theory(equality)])).
% cnf(8524,negated_conjecture,(p1(X1)|r1(esk5_0,esk22_1(esk5_0))|~p1(esk13_2(esk5_0,esk7_0))|~r1(esk5_0,X1)),inference(spm,[status(thm)],[8516,19,theory(equality)])).
% cnf(8526,negated_conjecture,(p1(X1)|r1(esk5_0,esk22_1(esk5_0))|~r1(esk5_0,X1)),inference(csr,[status(thm)],[8524,8296])).
% cnf(8529,negated_conjecture,(p1(esk6_0)|r1(esk5_0,esk22_1(esk5_0))),inference(spm,[status(thm)],[8526,17,theory(equality)])).
% cnf(8532,negated_conjecture,(r1(esk5_0,esk22_1(esk5_0))),inference(sr,[status(thm)],[8529,16,theory(equality)])).
% cnf(8554,negated_conjecture,(p1(esk8_1(esk22_1(esk5_0)))|p1(esk22_1(esk5_0))),inference(spm,[status(thm)],[21,8532,theory(equality)])).
% cnf(8555,negated_conjecture,(p1(esk22_1(esk5_0))|~p1(esk9_1(esk22_1(esk5_0)))),inference(spm,[status(thm)],[22,8532,theory(equality)])).
% cnf(8556,negated_conjecture,(p1(esk22_1(esk5_0))|r1(esk22_1(esk5_0),esk8_1(esk22_1(esk5_0)))),inference(spm,[status(thm)],[24,8532,theory(equality)])).
% cnf(8557,negated_conjecture,(p1(esk22_1(esk5_0))|r1(esk8_1(esk22_1(esk5_0)),esk9_1(esk22_1(esk5_0)))),inference(spm,[status(thm)],[23,8532,theory(equality)])).
% cnf(8691,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(X2)|p1(X3)|p1(esk22_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X1,X2)|~r1(esk8_1(esk22_1(esk5_0)),X3)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[78,8556,theory(equality)])).
% cnf(8692,plain,(p1(X1)|p1(X2)|r1(X1,esk20_3(esk5_0,X3,X1))|p1(esk22_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(spm,[status(thm)],[81,8556,theory(equality)])).
% cnf(8693,plain,(p1(X1)|p1(X2)|p1(esk22_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk21_3(esk5_0,X3,X1))|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(spm,[status(thm)],[79,8556,theory(equality)])).
% cnf(8694,plain,(p1(X1)|p1(X2)|r1(esk20_3(esk5_0,X3,X1),esk21_3(esk5_0,X3,X1))|p1(esk22_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(spm,[status(thm)],[80,8556,theory(equality)])).
% cnf(8695,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(X2)|p1(X3)|p1(esk22_1(esk5_0))|$false|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X1,X2)|~r1(esk8_1(esk22_1(esk5_0)),X3)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[8691,265,theory(equality)])).
% cnf(8696,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(X2)|p1(X3)|p1(esk22_1(esk5_0))|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X1,X2)|~r1(esk8_1(esk22_1(esk5_0)),X3)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[8695,theory(equality)])).
% cnf(8697,plain,(p1(X1)|p1(X2)|r1(X1,esk20_3(esk5_0,X3,X1))|p1(esk22_1(esk5_0))|$false|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(rw,[status(thm)],[8692,265,theory(equality)])).
% cnf(8698,plain,(p1(X1)|p1(X2)|r1(X1,esk20_3(esk5_0,X3,X1))|p1(esk22_1(esk5_0))|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(cn,[status(thm)],[8697,theory(equality)])).
% cnf(8699,plain,(p1(X1)|p1(X2)|p1(esk22_1(esk5_0))|$false|~p1(esk21_3(esk5_0,X3,X1))|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(rw,[status(thm)],[8693,265,theory(equality)])).
% cnf(8700,plain,(p1(X1)|p1(X2)|p1(esk22_1(esk5_0))|~p1(esk21_3(esk5_0,X3,X1))|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(cn,[status(thm)],[8699,theory(equality)])).
% cnf(8701,plain,(p1(X1)|p1(X2)|r1(esk20_3(esk5_0,X3,X1),esk21_3(esk5_0,X3,X1))|p1(esk22_1(esk5_0))|$false|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(rw,[status(thm)],[8694,265,theory(equality)])).
% cnf(8702,plain,(p1(X1)|p1(X2)|r1(esk20_3(esk5_0,X3,X1),esk21_3(esk5_0,X3,X1))|p1(esk22_1(esk5_0))|~p1(esk8_1(esk22_1(esk5_0)))|~r1(X3,X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)),inference(cn,[status(thm)],[8701,theory(equality)])).
% cnf(8905,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(esk22_1(esk5_0))|p1(X2)|p1(X3)|~r1(esk8_1(esk22_1(esk5_0)),X3)|~r1(esk5_0,X1)|~r1(X1,X2)),inference(csr,[status(thm)],[8696,8554])).
% cnf(8907,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),X1))|p1(esk22_1(esk5_0))|p1(X2)|p1(X1)|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk14_1(esk5_0),X1)),inference(spm,[status(thm)],[8905,1608,theory(equality)])).
% cnf(8938,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(X1)|p1(esk13_2(esk5_0,esk7_0))|~r1(esk8_1(esk22_1(esk5_0)),X1)),inference(spm,[status(thm)],[8907,7743,theory(equality)])).
% cnf(8951,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|p1(esk9_1(esk22_1(esk5_0)))),inference(spm,[status(thm)],[8938,8557,theory(equality)])).
% cnf(8952,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))),inference(csr,[status(thm)],[8951,8555])).
% cnf(8953,plain,(p1(esk22_1(esk5_0))|p1(X1)|p1(X2)|~p1(esk21_3(esk5_0,X3,X1))|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)|~r1(X3,X1)),inference(csr,[status(thm)],[8700,8554])).
% cnf(8955,negated_conjecture,(p1(esk22_1(esk5_0))|p1(X1)|p1(X2)|~p1(esk21_3(esk5_0,esk14_1(esk5_0),X2))|~r1(esk8_1(esk22_1(esk5_0)),X1)|~r1(esk14_1(esk5_0),X2)),inference(spm,[status(thm)],[8953,1608,theory(equality)])).
% cnf(8976,negated_conjecture,(p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(X1)|p1(esk13_2(esk5_0,esk7_0))|~p1(esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|~r1(esk8_1(esk22_1(esk5_0)),X1)),inference(spm,[status(thm)],[8955,7743,theory(equality)])).
% cnf(9015,plain,(p1(esk22_1(esk5_0))|p1(X1)|p1(X2)|r1(X1,esk20_3(esk5_0,X3,X1))|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)|~r1(X3,X1)),inference(csr,[status(thm)],[8698,8554])).
% cnf(9017,negated_conjecture,(p1(esk22_1(esk5_0))|p1(X1)|p1(X2)|r1(X2,esk20_3(esk5_0,esk14_1(esk5_0),X2))|~r1(esk8_1(esk22_1(esk5_0)),X1)|~r1(esk14_1(esk5_0),X2)),inference(spm,[status(thm)],[9015,1608,theory(equality)])).
% cnf(9039,negated_conjecture,(p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(X1)|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk13_2(esk5_0,esk7_0))|~r1(esk8_1(esk22_1(esk5_0)),X1)),inference(spm,[status(thm)],[9017,7743,theory(equality)])).
% cnf(9106,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|p1(esk9_1(esk22_1(esk5_0)))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(spm,[status(thm)],[9039,8557,theory(equality)])).
% cnf(9107,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(csr,[status(thm)],[9106,8555])).
% cnf(9126,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))|~p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(spm,[status(thm)],[7933,9107,theory(equality)])).
% cnf(9146,plain,(p1(esk22_1(esk5_0))|p1(X1)|p1(X2)|r1(esk20_3(esk5_0,X3,X1),esk21_3(esk5_0,X3,X1))|~r1(esk8_1(esk22_1(esk5_0)),X2)|~r1(esk5_0,X3)|~r1(X3,X1)),inference(csr,[status(thm)],[8702,8554])).
% cnf(9148,negated_conjecture,(p1(esk22_1(esk5_0))|p1(X1)|p1(X2)|r1(esk20_3(esk5_0,esk14_1(esk5_0),X2),esk21_3(esk5_0,esk14_1(esk5_0),X2))|~r1(esk8_1(esk22_1(esk5_0)),X1)|~r1(esk14_1(esk5_0),X2)),inference(spm,[status(thm)],[9146,1608,theory(equality)])).
% cnf(9225,negated_conjecture,(p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(X1)|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk13_2(esk5_0,esk7_0))|~r1(esk8_1(esk22_1(esk5_0)),X1)),inference(spm,[status(thm)],[9148,7743,theory(equality)])).
% cnf(9632,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|p1(esk9_1(esk22_1(esk5_0)))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(spm,[status(thm)],[9225,8557,theory(equality)])).
% cnf(9633,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(csr,[status(thm)],[9632,8555])).
% cnf(9882,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(csr,[status(thm)],[9126,8952])).
% cnf(9883,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[9882,9633,theory(equality)])).
% cnf(9885,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|~r1(esk8_1(esk22_1(esk5_0)),X1)),inference(spm,[status(thm)],[8976,9883,theory(equality)])).
% cnf(9890,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(esk9_1(esk22_1(esk5_0)))|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[9885,8557,theory(equality)])).
% cnf(9891,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))),inference(csr,[status(thm)],[9890,8555])).
% cnf(9906,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|r1(esk7_0,esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))),inference(spm,[status(thm)],[7575,9891,theory(equality)])).
% cnf(9940,negated_conjecture,(p1(esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|p1(esk13_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))),inference(spm,[status(thm)],[20,9906,theory(equality)])).
% cnf(9961,negated_conjecture,(p1(X1)|p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|~r1(esk7_0,X2)|~r1(X2,X1)),inference(spm,[status(thm)],[598,9940,theory(equality)])).
% cnf(9963,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(X1)|~r1(esk12_2(esk5_0,esk7_0),X1)),inference(spm,[status(thm)],[9961,7555,theory(equality)])).
% cnf(9966,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))),inference(spm,[status(thm)],[9963,9891,theory(equality)])).
% cnf(9969,plain,(p1(X1)|r1(esk12_2(esk5_0,X2),esk13_2(esk5_0,X2))|p1(esk13_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[40,9966,theory(equality)])).
% cnf(9977,plain,(p1(X1)|r1(esk12_2(esk5_0,X2),esk13_2(esk5_0,X2))|p1(esk13_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))|$false|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[9969,265,theory(equality)])).
% cnf(9978,plain,(p1(X1)|r1(esk12_2(esk5_0,X2),esk13_2(esk5_0,X2))|p1(esk13_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))|$false|$false|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[9977,871,theory(equality)])).
% cnf(9979,plain,(p1(X1)|r1(esk12_2(esk5_0,X2),esk13_2(esk5_0,X2))|p1(esk13_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[9978,theory(equality)])).
% cnf(10161,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))|p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|~r1(esk5_0,X1)),inference(spm,[status(thm)],[9979,19,theory(equality)])).
% cnf(10163,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[10161,8532,theory(equality)])).
% cnf(10184,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|r1(esk7_0,esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|p1(esk22_1(esk5_0))),inference(spm,[status(thm)],[7575,10163,theory(equality)])).
% cnf(10218,negated_conjecture,(p1(esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|p1(esk13_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))),inference(spm,[status(thm)],[20,10184,theory(equality)])).
% cnf(10239,negated_conjecture,(p1(X1)|p1(esk13_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))|~r1(esk7_0,X2)|~r1(X2,X1)),inference(spm,[status(thm)],[598,10218,theory(equality)])).
% cnf(10240,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))|p1(X1)|~r1(esk12_2(esk5_0,esk7_0),X1)),inference(spm,[status(thm)],[10239,7555,theory(equality)])).
% cnf(10245,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk22_1(esk5_0))),inference(spm,[status(thm)],[10240,10163,theory(equality)])).
% cnf(10246,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(X2)|p1(esk13_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~r1(X1,X2)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[70,10245,theory(equality)])).
% cnf(10247,plain,(p1(X1)|r1(X1,esk20_3(esk5_0,X2,X1))|p1(esk13_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~r1(X2,X1)|~r1(esk5_0,X2)),inference(spm,[status(thm)],[73,10245,theory(equality)])).
% cnf(10248,plain,(p1(X1)|p1(esk13_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~p1(esk21_3(esk5_0,X2,X1))|~r1(X2,X1)|~r1(esk5_0,X2)),inference(spm,[status(thm)],[71,10245,theory(equality)])).
% cnf(10249,plain,(p1(X1)|r1(esk20_3(esk5_0,X2,X1),esk21_3(esk5_0,X2,X1))|p1(esk13_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~r1(X2,X1)|~r1(esk5_0,X2)),inference(spm,[status(thm)],[72,10245,theory(equality)])).
% cnf(10250,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(X2)|p1(esk13_2(esk5_0,esk7_0))|$false|~r1(X1,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[10246,265,theory(equality)])).
% cnf(10251,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(X2)|p1(esk13_2(esk5_0,esk7_0))|~r1(X1,X2)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[10250,theory(equality)])).
% cnf(10252,plain,(p1(X1)|r1(X1,esk20_3(esk5_0,X2,X1))|p1(esk13_2(esk5_0,esk7_0))|$false|~r1(X2,X1)|~r1(esk5_0,X2)),inference(rw,[status(thm)],[10247,265,theory(equality)])).
% cnf(10253,plain,(p1(X1)|r1(X1,esk20_3(esk5_0,X2,X1))|p1(esk13_2(esk5_0,esk7_0))|~r1(X2,X1)|~r1(esk5_0,X2)),inference(cn,[status(thm)],[10252,theory(equality)])).
% cnf(10254,plain,(p1(X1)|p1(esk13_2(esk5_0,esk7_0))|$false|~p1(esk21_3(esk5_0,X2,X1))|~r1(X2,X1)|~r1(esk5_0,X2)),inference(rw,[status(thm)],[10248,265,theory(equality)])).
% cnf(10255,plain,(p1(X1)|p1(esk13_2(esk5_0,esk7_0))|~p1(esk21_3(esk5_0,X2,X1))|~r1(X2,X1)|~r1(esk5_0,X2)),inference(cn,[status(thm)],[10254,theory(equality)])).
% cnf(10256,plain,(p1(X1)|r1(esk20_3(esk5_0,X2,X1),esk21_3(esk5_0,X2,X1))|p1(esk13_2(esk5_0,esk7_0))|$false|~r1(X2,X1)|~r1(esk5_0,X2)),inference(rw,[status(thm)],[10249,265,theory(equality)])).
% cnf(10257,plain,(p1(X1)|r1(esk20_3(esk5_0,X2,X1),esk21_3(esk5_0,X2,X1))|p1(esk13_2(esk5_0,esk7_0))|~r1(X2,X1)|~r1(esk5_0,X2)),inference(cn,[status(thm)],[10256,theory(equality)])).
% cnf(10259,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk20_3(esk5_0,esk14_1(esk5_0),X1))|p1(X1)|~r1(esk14_1(esk5_0),X1)),inference(spm,[status(thm)],[10251,1608,theory(equality)])).
% cnf(10272,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(X1)|~p1(esk21_3(esk5_0,esk14_1(esk5_0),X1))|~r1(esk14_1(esk5_0),X1)),inference(spm,[status(thm)],[10255,1608,theory(equality)])).
% cnf(10284,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(X1)|r1(X1,esk20_3(esk5_0,esk14_1(esk5_0),X1))|~r1(esk14_1(esk5_0),X1)),inference(spm,[status(thm)],[10253,1608,theory(equality)])).
% cnf(10333,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))),inference(spm,[status(thm)],[10259,7743,theory(equality)])).
% cnf(10346,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|~p1(esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(spm,[status(thm)],[10272,7743,theory(equality)])).
% cnf(10358,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(spm,[status(thm)],[10284,7743,theory(equality)])).
% cnf(10380,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|~p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(spm,[status(thm)],[7933,10358,theory(equality)])).
% cnf(10404,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(X1)|r1(esk20_3(esk5_0,esk14_1(esk5_0),X1),esk21_3(esk5_0,esk14_1(esk5_0),X1))|~r1(esk14_1(esk5_0),X1)),inference(spm,[status(thm)],[10257,1608,theory(equality)])).
% cnf(10472,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(spm,[status(thm)],[10404,7743,theory(equality)])).
% cnf(10624,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(csr,[status(thm)],[10380,10333])).
% cnf(10625,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[10624,10472,theory(equality)])).
% cnf(10626,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))),inference(csr,[status(thm)],[10625,10346])).
% cnf(10641,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|r1(esk7_0,esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|p1(esk15_1(esk5_0))),inference(spm,[status(thm)],[7575,10626,theory(equality)])).
% cnf(10675,negated_conjecture,(p1(esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))),inference(spm,[status(thm)],[20,10641,theory(equality)])).
% cnf(10696,negated_conjecture,(p1(X1)|p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|~r1(esk7_0,X2)|~r1(X2,X1)),inference(spm,[status(thm)],[598,10675,theory(equality)])).
% cnf(10697,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))|p1(X1)|~r1(esk12_2(esk5_0,esk7_0),X1)),inference(spm,[status(thm)],[10696,7555,theory(equality)])).
% cnf(10700,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk15_1(esk5_0))),inference(spm,[status(thm)],[10697,10626,theory(equality)])).
% cnf(10704,plain,(p1(X1)|r1(esk12_2(esk5_0,X2),esk13_2(esk5_0,X2))|p1(esk13_2(esk5_0,esk7_0))|~epred1_1(esk5_0)|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[40,10700,theory(equality)])).
% cnf(10712,plain,(p1(X1)|r1(esk12_2(esk5_0,X2),esk13_2(esk5_0,X2))|p1(esk13_2(esk5_0,esk7_0))|$false|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[10704,265,theory(equality)])).
% cnf(10713,plain,(p1(X1)|r1(esk12_2(esk5_0,X2),esk13_2(esk5_0,X2))|p1(esk13_2(esk5_0,esk7_0))|$false|$false|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[10712,871,theory(equality)])).
% cnf(10714,plain,(p1(X1)|r1(esk12_2(esk5_0,X2),esk13_2(esk5_0,X2))|p1(esk13_2(esk5_0,esk7_0))|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[10713,theory(equality)])).
% cnf(10909,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(X1)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))|~r1(esk5_0,X1)),inference(spm,[status(thm)],[10714,19,theory(equality)])).
% cnf(10914,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(esk6_0)|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[10909,17,theory(equality)])).
% cnf(10917,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|r1(esk12_2(esk5_0,esk7_0),esk13_2(esk5_0,esk7_0))),inference(sr,[status(thm)],[10914,16,theory(equality)])).
% cnf(10932,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|r1(esk7_0,esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))),inference(spm,[status(thm)],[7575,10917,theory(equality)])).
% cnf(10966,negated_conjecture,(p1(esk2_4(esk3_0,esk4_0,esk5_0,esk7_0))|p1(esk13_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[20,10932,theory(equality)])).
% cnf(10987,negated_conjecture,(p1(X1)|p1(esk13_2(esk5_0,esk7_0))|~r1(esk7_0,X2)|~r1(X2,X1)),inference(spm,[status(thm)],[598,10966,theory(equality)])).
% cnf(10988,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))|p1(X1)|~r1(esk12_2(esk5_0,esk7_0),X1)),inference(spm,[status(thm)],[10987,7555,theory(equality)])).
% cnf(10991,negated_conjecture,(p1(esk13_2(esk5_0,esk7_0))),inference(spm,[status(thm)],[10988,10917,theory(equality)])).
% cnf(10995,plain,(p1(X1)|r1(esk14_1(esk5_0),esk15_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk5_0)|~r1(esk5_0,esk7_0)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[43,10991,theory(equality)])).
% cnf(11068,plain,(p1(X1)|r1(esk14_1(esk5_0),esk15_1(esk5_0))|$false|~p1(esk5_0)|~r1(esk5_0,esk7_0)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[10995,265,theory(equality)])).
% cnf(11069,plain,(p1(X1)|r1(esk14_1(esk5_0),esk15_1(esk5_0))|$false|$false|~r1(esk5_0,esk7_0)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[11068,871,theory(equality)])).
% cnf(11070,plain,(p1(X1)|r1(esk14_1(esk5_0),esk15_1(esk5_0))|$false|$false|$false|~r1(esk5_0,X1)),inference(rw,[status(thm)],[11069,19,theory(equality)])).
% cnf(11071,plain,(p1(X1)|r1(esk14_1(esk5_0),esk15_1(esk5_0))|~r1(esk5_0,X1)),inference(cn,[status(thm)],[11070,theory(equality)])).
% cnf(11075,negated_conjecture,(p1(esk6_0)|r1(esk14_1(esk5_0),esk15_1(esk5_0))),inference(spm,[status(thm)],[11071,17,theory(equality)])).
% cnf(11078,negated_conjecture,(r1(esk14_1(esk5_0),esk15_1(esk5_0))),inference(sr,[status(thm)],[11075,16,theory(equality)])).
% cnf(11101,plain,(p1(X1)|p1(X2)|p1(esk15_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk13_2(esk5_0,X3))|~p1(X4)|~p1(esk5_0)|~r1(X4,X2)|~r1(esk15_1(esk5_0),X4)|~r1(esk5_0,X3)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[51,11078,theory(equality)])).
% cnf(11105,negated_conjecture,(p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(X1)|~p1(esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|~r1(esk8_1(esk22_1(esk5_0)),X1)),inference(spm,[status(thm)],[8955,11078,theory(equality)])).
% cnf(11106,negated_conjecture,(p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(X1)|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|~r1(esk8_1(esk22_1(esk5_0)),X1)),inference(spm,[status(thm)],[9017,11078,theory(equality)])).
% cnf(11107,negated_conjecture,(p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(X1)|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|~r1(esk8_1(esk22_1(esk5_0)),X1)),inference(spm,[status(thm)],[9148,11078,theory(equality)])).
% cnf(11108,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(X1)|~r1(esk8_1(esk22_1(esk5_0)),X1)),inference(spm,[status(thm)],[8907,11078,theory(equality)])).
% cnf(11320,plain,(p1(X1)|p1(X2)|p1(esk15_1(esk5_0))|$false|~p1(esk13_2(esk5_0,X3))|~p1(X4)|~p1(esk5_0)|~r1(X4,X2)|~r1(esk15_1(esk5_0),X4)|~r1(esk5_0,X3)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[11101,265,theory(equality)])).
% cnf(11321,plain,(p1(X1)|p1(X2)|p1(esk15_1(esk5_0))|$false|~p1(esk13_2(esk5_0,X3))|~p1(X4)|$false|~r1(X4,X2)|~r1(esk15_1(esk5_0),X4)|~r1(esk5_0,X3)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[11320,871,theory(equality)])).
% cnf(11322,plain,(p1(X1)|p1(X2)|p1(esk15_1(esk5_0))|~p1(esk13_2(esk5_0,X3))|~p1(X4)|~r1(X4,X2)|~r1(esk15_1(esk5_0),X4)|~r1(esk5_0,X3)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[11321,theory(equality)])).
% cnf(11338,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|p1(esk9_1(esk22_1(esk5_0)))),inference(spm,[status(thm)],[11108,8557,theory(equality)])).
% cnf(11339,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))),inference(csr,[status(thm)],[11338,8555])).
% cnf(11361,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|p1(esk9_1(esk22_1(esk5_0)))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(spm,[status(thm)],[11106,8557,theory(equality)])).
% cnf(11362,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(csr,[status(thm)],[11361,8555])).
% cnf(11386,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|p1(X2)|~p1(esk13_2(esk5_0,esk7_0))|~p1(X3)|~r1(esk15_1(esk5_0),X3)|~r1(esk5_0,X2)|~r1(X3,X1)),inference(spm,[status(thm)],[11322,19,theory(equality)])).
% cnf(11388,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|p1(X2)|$false|~p1(X3)|~r1(esk15_1(esk5_0),X3)|~r1(esk5_0,X2)|~r1(X3,X1)),inference(rw,[status(thm)],[11386,10991,theory(equality)])).
% cnf(11389,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|p1(X2)|~p1(X3)|~r1(esk15_1(esk5_0),X3)|~r1(esk5_0,X2)|~r1(X3,X1)),inference(cn,[status(thm)],[11388,theory(equality)])).
% cnf(11393,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk6_0)|p1(X1)|~p1(X2)|~r1(esk15_1(esk5_0),X2)|~r1(X2,X1)),inference(spm,[status(thm)],[11389,17,theory(equality)])).
% cnf(11396,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|~p1(X2)|~r1(esk15_1(esk5_0),X2)|~r1(X2,X1)),inference(sr,[status(thm)],[11393,16,theory(equality)])).
% cnf(11397,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|p1(esk22_1(esk5_0))|~p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(spm,[status(thm)],[11396,11362,theory(equality)])).
% cnf(11402,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|p1(X1)|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(csr,[status(thm)],[11397,11339])).
% cnf(11443,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|p1(esk9_1(esk22_1(esk5_0)))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(spm,[status(thm)],[11107,8557,theory(equality)])).
% cnf(11444,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(csr,[status(thm)],[11443,8555])).
% cnf(11459,negated_conjecture,(p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(spm,[status(thm)],[11402,11444,theory(equality)])).
% cnf(11461,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk22_1(esk5_0))|p1(X1)|~r1(esk8_1(esk22_1(esk5_0)),X1)),inference(spm,[status(thm)],[11105,11459,theory(equality)])).
% cnf(11467,negated_conjecture,(p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))|p1(esk9_1(esk22_1(esk5_0)))),inference(spm,[status(thm)],[11461,8557,theory(equality)])).
% cnf(11468,negated_conjecture,(p1(esk22_1(esk5_0))|p1(esk15_1(esk5_0))),inference(csr,[status(thm)],[11467,8555])).
% cnf(11470,plain,(p1(X1)|p1(esk22_1(esk5_0))|~epred1_1(esk5_0)|~p1(esk13_2(esk5_0,X2))|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[39,11468,theory(equality)])).
% cnf(11476,plain,(p1(X1)|p1(esk22_1(esk5_0))|$false|~p1(esk13_2(esk5_0,X2))|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[11470,265,theory(equality)])).
% cnf(11477,plain,(p1(X1)|p1(esk22_1(esk5_0))|$false|~p1(esk13_2(esk5_0,X2))|$false|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[11476,871,theory(equality)])).
% cnf(11478,plain,(p1(X1)|p1(esk22_1(esk5_0))|~p1(esk13_2(esk5_0,X2))|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[11477,theory(equality)])).
% cnf(11511,negated_conjecture,(p1(esk22_1(esk5_0))|p1(X1)|~p1(esk13_2(esk5_0,esk7_0))|~r1(esk5_0,X1)),inference(spm,[status(thm)],[11478,19,theory(equality)])).
% cnf(11513,negated_conjecture,(p1(esk22_1(esk5_0))|p1(X1)|$false|~r1(esk5_0,X1)),inference(rw,[status(thm)],[11511,10991,theory(equality)])).
% cnf(11514,negated_conjecture,(p1(esk22_1(esk5_0))|p1(X1)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[11513,theory(equality)])).
% cnf(11515,negated_conjecture,(p1(esk22_1(esk5_0))),inference(spm,[status(thm)],[11514,8532,theory(equality)])).
% cnf(11522,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(X2)|~epred1_1(esk5_0)|~r1(X1,X2)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[70,11515,theory(equality)])).
% cnf(11523,plain,(p1(X1)|r1(X1,esk20_3(esk5_0,X2,X1))|~epred1_1(esk5_0)|~r1(X2,X1)|~r1(esk5_0,X2)),inference(spm,[status(thm)],[73,11515,theory(equality)])).
% cnf(11524,plain,(p1(X1)|~epred1_1(esk5_0)|~p1(esk21_3(esk5_0,X2,X1))|~r1(X2,X1)|~r1(esk5_0,X2)),inference(spm,[status(thm)],[71,11515,theory(equality)])).
% cnf(11525,plain,(p1(X1)|r1(esk20_3(esk5_0,X2,X1),esk21_3(esk5_0,X2,X1))|~epred1_1(esk5_0)|~r1(X2,X1)|~r1(esk5_0,X2)),inference(spm,[status(thm)],[72,11515,theory(equality)])).
% cnf(11621,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(X2)|$false|~r1(X1,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[11522,265,theory(equality)])).
% cnf(11622,plain,(p1(esk20_3(esk5_0,X1,X2))|p1(X2)|~r1(X1,X2)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[11621,theory(equality)])).
% cnf(11623,plain,(p1(X1)|r1(X1,esk20_3(esk5_0,X2,X1))|$false|~r1(X2,X1)|~r1(esk5_0,X2)),inference(rw,[status(thm)],[11523,265,theory(equality)])).
% cnf(11624,plain,(p1(X1)|r1(X1,esk20_3(esk5_0,X2,X1))|~r1(X2,X1)|~r1(esk5_0,X2)),inference(cn,[status(thm)],[11623,theory(equality)])).
% cnf(11625,plain,(p1(X1)|$false|~p1(esk21_3(esk5_0,X2,X1))|~r1(X2,X1)|~r1(esk5_0,X2)),inference(rw,[status(thm)],[11524,265,theory(equality)])).
% cnf(11626,plain,(p1(X1)|~p1(esk21_3(esk5_0,X2,X1))|~r1(X2,X1)|~r1(esk5_0,X2)),inference(cn,[status(thm)],[11625,theory(equality)])).
% cnf(11627,plain,(p1(X1)|r1(esk20_3(esk5_0,X2,X1),esk21_3(esk5_0,X2,X1))|$false|~r1(X2,X1)|~r1(esk5_0,X2)),inference(rw,[status(thm)],[11525,265,theory(equality)])).
% cnf(11628,plain,(p1(X1)|r1(esk20_3(esk5_0,X2,X1),esk21_3(esk5_0,X2,X1))|~r1(X2,X1)|~r1(esk5_0,X2)),inference(cn,[status(thm)],[11627,theory(equality)])).
% cnf(11630,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),X1))|p1(X1)|~r1(esk14_1(esk5_0),X1)),inference(spm,[status(thm)],[11622,1608,theory(equality)])).
% cnf(11641,negated_conjecture,(p1(X1)|~p1(esk21_3(esk5_0,esk14_1(esk5_0),X1))|~r1(esk14_1(esk5_0),X1)),inference(spm,[status(thm)],[11626,1608,theory(equality)])).
% cnf(11651,negated_conjecture,(p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|p1(esk15_1(esk5_0))),inference(spm,[status(thm)],[11630,11078,theory(equality)])).
% cnf(11653,negated_conjecture,(p1(X1)|r1(X1,esk20_3(esk5_0,esk14_1(esk5_0),X1))|~r1(esk14_1(esk5_0),X1)),inference(spm,[status(thm)],[11624,1608,theory(equality)])).
% cnf(11663,negated_conjecture,(p1(esk15_1(esk5_0))|~p1(esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(spm,[status(thm)],[11641,11078,theory(equality)])).
% cnf(11696,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk15_1(esk5_0),esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(spm,[status(thm)],[11653,11078,theory(equality)])).
% cnf(11714,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|~p1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(spm,[status(thm)],[11396,11696,theory(equality)])).
% cnf(11717,negated_conjecture,(p1(X1)|r1(esk20_3(esk5_0,esk14_1(esk5_0),X1),esk21_3(esk5_0,esk14_1(esk5_0),X1))|~r1(esk14_1(esk5_0),X1)),inference(spm,[status(thm)],[11628,1608,theory(equality)])).
% cnf(11755,negated_conjecture,(p1(esk15_1(esk5_0))|r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(spm,[status(thm)],[11717,11078,theory(equality)])).
% cnf(11770,negated_conjecture,(p1(esk15_1(esk5_0))|p1(X1)|~r1(esk20_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)),X1)),inference(csr,[status(thm)],[11714,11651])).
% cnf(11771,negated_conjecture,(p1(esk15_1(esk5_0))|p1(esk21_3(esk5_0,esk14_1(esk5_0),esk15_1(esk5_0)))),inference(spm,[status(thm)],[11770,11755,theory(equality)])).
% cnf(11778,negated_conjecture,(p1(esk15_1(esk5_0))),inference(csr,[status(thm)],[11771,11663])).
% cnf(11780,plain,(p1(X1)|~epred1_1(esk5_0)|~p1(esk13_2(esk5_0,X2))|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(spm,[status(thm)],[39,11778,theory(equality)])).
% cnf(11798,plain,(p1(X1)|$false|~p1(esk13_2(esk5_0,X2))|~p1(esk5_0)|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[11780,265,theory(equality)])).
% cnf(11799,plain,(p1(X1)|$false|~p1(esk13_2(esk5_0,X2))|$false|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(rw,[status(thm)],[11798,871,theory(equality)])).
% cnf(11800,plain,(p1(X1)|~p1(esk13_2(esk5_0,X2))|~r1(esk5_0,X2)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[11799,theory(equality)])).
% cnf(11825,negated_conjecture,(p1(X1)|~p1(esk13_2(esk5_0,esk7_0))|~r1(esk5_0,X1)),inference(spm,[status(thm)],[11800,19,theory(equality)])).
% cnf(11827,negated_conjecture,(p1(X1)|$false|~r1(esk5_0,X1)),inference(rw,[status(thm)],[11825,10991,theory(equality)])).
% cnf(11828,negated_conjecture,(p1(X1)|~r1(esk5_0,X1)),inference(cn,[status(thm)],[11827,theory(equality)])).
% cnf(11832,negated_conjecture,(p1(esk6_0)),inference(spm,[status(thm)],[11828,17,theory(equality)])).
% cnf(11836,negated_conjecture,($false),inference(sr,[status(thm)],[11832,16,theory(equality)])).
% cnf(11837,negated_conjecture,($false),11836,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 2661
% # ...of these trivial : 11
% # ...subsumed : 773
% # ...remaining for further processing: 1877
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 897
% # Backward-rewritten : 644
% # Generated clauses : 6256
% # ...of the previous two non-trivial : 5191
% # Contextual simplify-reflections : 2164
% # Paramodulations : 6256
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 270
% # Positive orientable unit clauses: 28
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 2
% # Non-unit-clauses : 240
% # Current number of unprocessed clauses: 41
% # ...number of literals in the above : 257
% # Clause-clause subsumption calls (NU) : 27788
% # Rec. Clause-clause subsumption calls : 5141
% # Unit Clause-clause subsumption calls : 462
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 17
% # Indexed BW rewrite successes : 17
% # Backwards rewriting index: 339 leaves, 1.43+/-1.487 terms/leaf
% # Paramod-from index: 32 leaves, 1.06+/-0.242 terms/leaf
% # Paramod-into index: 104 leaves, 1.43+/-0.907 terms/leaf
% # -------------------------------------------------
% # User time : 0.983 s
% # System time : 0.022 s
% # Total time : 1.005 s
% # Maximum resident set size: 0 pages
% PrfWatch: 1.25 CPU 1.37 WC
% FINAL PrfWatch: 1.25 CPU 1.37 WC
% SZS output end Solution for /tmp/SystemOnTPTP439/LCL658+1.005.tptp
%
%------------------------------------------------------------------------------