%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SWC155+1 : TPTP v5.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art05.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 : Thu Dec 30 07:11:45 EST 2010
% Result : Theorem 6.10s
% Output : Solution 6.10s
% 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/SystemOnTPTP27883/SWC155+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP27883/SWC155+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP27883/SWC155+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 27979
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% PrfWatch: 1.93 CPU 2.01 WC
% # Preprocessing time : 0.032 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 3.55 CPU 4.02 WC
% # SZS output start CNFRefutation.
% fof(3, axiom,![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>ssList(cons(X2,X1)))),file('/tmp/SRASS.s.p', ax16)).
% fof(4, axiom,ssList(nil),file('/tmp/SRASS.s.p', ax17)).
% fof(9, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>ssList(app(X1,X2)))),file('/tmp/SRASS.s.p', ax26)).
% fof(10, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssItem(X3)=>cons(X3,app(X2,X1))=app(cons(X3,X2),X1)))),file('/tmp/SRASS.s.p', ax27)).
% fof(11, axiom,![X1]:(ssList(X1)=>app(nil,X1)=X1),file('/tmp/SRASS.s.p', ax28)).
% fof(12, axiom,![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>((leq(X1,X2)&leq(X2,X1))=>X1=X2))),file('/tmp/SRASS.s.p', ax29)).
% fof(15, axiom,![X1]:(ssItem(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(memberP(app(X2,X3),X1)<=>(memberP(X2,X1)|memberP(X3,X1)))))),file('/tmp/SRASS.s.p', ax36)).
% fof(16, axiom,![X1]:(ssItem(X1)=>![X2]:(ssItem(X2)=>![X3]:(ssList(X3)=>(memberP(cons(X2,X3),X1)<=>(X1=X2|memberP(X3,X1)))))),file('/tmp/SRASS.s.p', ax37)).
% fof(18, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(app(X3,X2)=app(X1,X2)=>X3=X1)))),file('/tmp/SRASS.s.p', ax79)).
% fof(19, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(app(X2,X3)=app(X2,X1)=>X3=X1)))),file('/tmp/SRASS.s.p', ax80)).
% fof(20, axiom,![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>cons(X2,X1)=app(cons(X2,nil),X1))),file('/tmp/SRASS.s.p', ax81)).
% fof(21, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>app(app(X1,X2),X3)=app(X1,app(X2,X3))))),file('/tmp/SRASS.s.p', ax82)).
% fof(48, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(rearsegP(X1,X2)<=>?[X3]:(ssList(X3)&app(X3,X2)=X1)))),file('/tmp/SRASS.s.p', ax6)).
% fof(96, conjecture,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>![X4]:(ssList(X4)=>(((~(X2=X4)|~(X1=X3))|?[X5]:(ssItem(X5)&?[X6]:(ssList(X6)&?[X7]:((ssList(X7)&app(app(X6,cons(X5,nil)),X7)=X3)&?[X8]:(ssItem(X8)&((~(leq(X5,X8))&memberP(X7,X8))|(~(leq(X8,X5))&memberP(X6,X8))))))))|![X9]:(ssItem(X9)=>![X10]:(ssItem(X10)=>![X11]:(ssList(X11)=>![X12]:(ssList(X12)=>![X13]:(ssList(X13)=>((~(app(app(app(app(X11,cons(X9,nil)),X12),cons(X10,nil)),X13)=X1)|~(leq(X10,X9)))|(![X14]:(ssItem(X14)=>(~(memberP(X12,X14))|(leq(X9,X14)&leq(X14,X10))))&leq(X9,X10))))))))))))),file('/tmp/SRASS.s.p', co1)).
% fof(97, negated_conjecture,~(![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>![X4]:(ssList(X4)=>(((~(X2=X4)|~(X1=X3))|?[X5]:(ssItem(X5)&?[X6]:(ssList(X6)&?[X7]:((ssList(X7)&app(app(X6,cons(X5,nil)),X7)=X3)&?[X8]:(ssItem(X8)&((~(leq(X5,X8))&memberP(X7,X8))|(~(leq(X8,X5))&memberP(X6,X8))))))))|![X9]:(ssItem(X9)=>![X10]:(ssItem(X10)=>![X11]:(ssList(X11)=>![X12]:(ssList(X12)=>![X13]:(ssList(X13)=>((~(app(app(app(app(X11,cons(X9,nil)),X12),cons(X10,nil)),X13)=X1)|~(leq(X10,X9)))|(![X14]:(ssItem(X14)=>(~(memberP(X12,X14))|(leq(X9,X14)&leq(X14,X10))))&leq(X9,X10)))))))))))))),inference(assume_negation,[status(cth)],[96])).
% fof(103, negated_conjecture,~(![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>![X4]:(ssList(X4)=>(((~(X2=X4)|~(X1=X3))|?[X5]:(ssItem(X5)&?[X6]:(ssList(X6)&?[X7]:((ssList(X7)&app(app(X6,cons(X5,nil)),X7)=X3)&?[X8]:(ssItem(X8)&((~(leq(X5,X8))&memberP(X7,X8))|(~(leq(X8,X5))&memberP(X6,X8))))))))|![X9]:(ssItem(X9)=>![X10]:(ssItem(X10)=>![X11]:(ssList(X11)=>![X12]:(ssList(X12)=>![X13]:(ssList(X13)=>((~(app(app(app(app(X11,cons(X9,nil)),X12),cons(X10,nil)),X13)=X1)|~(leq(X10,X9)))|(![X14]:(ssItem(X14)=>(~(memberP(X12,X14))|(leq(X9,X14)&leq(X14,X10))))&leq(X9,X10)))))))))))))),inference(fof_simplification,[status(thm)],[97,theory(equality)])).
% fof(118, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssItem(X2))|ssList(cons(X2,X1)))),inference(fof_nnf,[status(thm)],[3])).
% fof(119, plain,![X3]:(~(ssList(X3))|![X4]:(~(ssItem(X4))|ssList(cons(X4,X3)))),inference(variable_rename,[status(thm)],[118])).
% fof(120, plain,![X3]:![X4]:((~(ssItem(X4))|ssList(cons(X4,X3)))|~(ssList(X3))),inference(shift_quantors,[status(thm)],[119])).
% cnf(121,plain,(ssList(cons(X2,X1))|~ssList(X1)|~ssItem(X2)),inference(split_conjunct,[status(thm)],[120])).
% cnf(122,plain,(ssList(nil)),inference(split_conjunct,[status(thm)],[4])).
% fof(144, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|ssList(app(X1,X2)))),inference(fof_nnf,[status(thm)],[9])).
% fof(145, plain,![X3]:(~(ssList(X3))|![X4]:(~(ssList(X4))|ssList(app(X3,X4)))),inference(variable_rename,[status(thm)],[144])).
% fof(146, plain,![X3]:![X4]:((~(ssList(X4))|ssList(app(X3,X4)))|~(ssList(X3))),inference(shift_quantors,[status(thm)],[145])).
% cnf(147,plain,(ssList(app(X1,X2))|~ssList(X1)|~ssList(X2)),inference(split_conjunct,[status(thm)],[146])).
% fof(148, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|![X3]:(~(ssItem(X3))|cons(X3,app(X2,X1))=app(cons(X3,X2),X1)))),inference(fof_nnf,[status(thm)],[10])).
% fof(149, plain,![X4]:(~(ssList(X4))|![X5]:(~(ssList(X5))|![X6]:(~(ssItem(X6))|cons(X6,app(X5,X4))=app(cons(X6,X5),X4)))),inference(variable_rename,[status(thm)],[148])).
% fof(150, plain,![X4]:![X5]:![X6]:(((~(ssItem(X6))|cons(X6,app(X5,X4))=app(cons(X6,X5),X4))|~(ssList(X5)))|~(ssList(X4))),inference(shift_quantors,[status(thm)],[149])).
% cnf(151,plain,(cons(X3,app(X2,X1))=app(cons(X3,X2),X1)|~ssList(X1)|~ssList(X2)|~ssItem(X3)),inference(split_conjunct,[status(thm)],[150])).
% fof(152, plain,![X1]:(~(ssList(X1))|app(nil,X1)=X1),inference(fof_nnf,[status(thm)],[11])).
% fof(153, plain,![X2]:(~(ssList(X2))|app(nil,X2)=X2),inference(variable_rename,[status(thm)],[152])).
% cnf(154,plain,(app(nil,X1)=X1|~ssList(X1)),inference(split_conjunct,[status(thm)],[153])).
% fof(155, plain,![X1]:(~(ssItem(X1))|![X2]:(~(ssItem(X2))|((~(leq(X1,X2))|~(leq(X2,X1)))|X1=X2))),inference(fof_nnf,[status(thm)],[12])).
% fof(156, plain,![X3]:(~(ssItem(X3))|![X4]:(~(ssItem(X4))|((~(leq(X3,X4))|~(leq(X4,X3)))|X3=X4))),inference(variable_rename,[status(thm)],[155])).
% fof(157, plain,![X3]:![X4]:((~(ssItem(X4))|((~(leq(X3,X4))|~(leq(X4,X3)))|X3=X4))|~(ssItem(X3))),inference(shift_quantors,[status(thm)],[156])).
% cnf(158,plain,(X1=X2|~ssItem(X1)|~leq(X2,X1)|~leq(X1,X2)|~ssItem(X2)),inference(split_conjunct,[status(thm)],[157])).
% fof(166, plain,![X1]:(~(ssItem(X1))|![X2]:(~(ssList(X2))|![X3]:(~(ssList(X3))|((~(memberP(app(X2,X3),X1))|(memberP(X2,X1)|memberP(X3,X1)))&((~(memberP(X2,X1))&~(memberP(X3,X1)))|memberP(app(X2,X3),X1)))))),inference(fof_nnf,[status(thm)],[15])).
% fof(167, plain,![X4]:(~(ssItem(X4))|![X5]:(~(ssList(X5))|![X6]:(~(ssList(X6))|((~(memberP(app(X5,X6),X4))|(memberP(X5,X4)|memberP(X6,X4)))&((~(memberP(X5,X4))&~(memberP(X6,X4)))|memberP(app(X5,X6),X4)))))),inference(variable_rename,[status(thm)],[166])).
% fof(168, plain,![X4]:![X5]:![X6]:(((~(ssList(X6))|((~(memberP(app(X5,X6),X4))|(memberP(X5,X4)|memberP(X6,X4)))&((~(memberP(X5,X4))&~(memberP(X6,X4)))|memberP(app(X5,X6),X4))))|~(ssList(X5)))|~(ssItem(X4))),inference(shift_quantors,[status(thm)],[167])).
% fof(169, plain,![X4]:![X5]:![X6]:(((((~(memberP(app(X5,X6),X4))|(memberP(X5,X4)|memberP(X6,X4)))|~(ssList(X6)))|~(ssList(X5)))|~(ssItem(X4)))&(((((~(memberP(X5,X4))|memberP(app(X5,X6),X4))|~(ssList(X6)))|~(ssList(X5)))|~(ssItem(X4)))&((((~(memberP(X6,X4))|memberP(app(X5,X6),X4))|~(ssList(X6)))|~(ssList(X5)))|~(ssItem(X4))))),inference(distribute,[status(thm)],[168])).
% cnf(170,plain,(memberP(app(X2,X3),X1)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|~memberP(X3,X1)),inference(split_conjunct,[status(thm)],[169])).
% cnf(171,plain,(memberP(app(X2,X3),X1)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|~memberP(X2,X1)),inference(split_conjunct,[status(thm)],[169])).
% fof(173, plain,![X1]:(~(ssItem(X1))|![X2]:(~(ssItem(X2))|![X3]:(~(ssList(X3))|((~(memberP(cons(X2,X3),X1))|(X1=X2|memberP(X3,X1)))&((~(X1=X2)&~(memberP(X3,X1)))|memberP(cons(X2,X3),X1)))))),inference(fof_nnf,[status(thm)],[16])).
% fof(174, plain,![X4]:(~(ssItem(X4))|![X5]:(~(ssItem(X5))|![X6]:(~(ssList(X6))|((~(memberP(cons(X5,X6),X4))|(X4=X5|memberP(X6,X4)))&((~(X4=X5)&~(memberP(X6,X4)))|memberP(cons(X5,X6),X4)))))),inference(variable_rename,[status(thm)],[173])).
% fof(175, plain,![X4]:![X5]:![X6]:(((~(ssList(X6))|((~(memberP(cons(X5,X6),X4))|(X4=X5|memberP(X6,X4)))&((~(X4=X5)&~(memberP(X6,X4)))|memberP(cons(X5,X6),X4))))|~(ssItem(X5)))|~(ssItem(X4))),inference(shift_quantors,[status(thm)],[174])).
% fof(176, plain,![X4]:![X5]:![X6]:(((((~(memberP(cons(X5,X6),X4))|(X4=X5|memberP(X6,X4)))|~(ssList(X6)))|~(ssItem(X5)))|~(ssItem(X4)))&(((((~(X4=X5)|memberP(cons(X5,X6),X4))|~(ssList(X6)))|~(ssItem(X5)))|~(ssItem(X4)))&((((~(memberP(X6,X4))|memberP(cons(X5,X6),X4))|~(ssList(X6)))|~(ssItem(X5)))|~(ssItem(X4))))),inference(distribute,[status(thm)],[175])).
% cnf(178,plain,(memberP(cons(X2,X3),X1)|~ssItem(X1)|~ssItem(X2)|~ssList(X3)|X1!=X2),inference(split_conjunct,[status(thm)],[176])).
% fof(183, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|![X3]:(~(ssList(X3))|(~(app(X3,X2)=app(X1,X2))|X3=X1)))),inference(fof_nnf,[status(thm)],[18])).
% fof(184, plain,![X4]:(~(ssList(X4))|![X5]:(~(ssList(X5))|![X6]:(~(ssList(X6))|(~(app(X6,X5)=app(X4,X5))|X6=X4)))),inference(variable_rename,[status(thm)],[183])).
% fof(185, plain,![X4]:![X5]:![X6]:(((~(ssList(X6))|(~(app(X6,X5)=app(X4,X5))|X6=X4))|~(ssList(X5)))|~(ssList(X4))),inference(shift_quantors,[status(thm)],[184])).
% cnf(186,plain,(X3=X1|~ssList(X1)|~ssList(X2)|app(X3,X2)!=app(X1,X2)|~ssList(X3)),inference(split_conjunct,[status(thm)],[185])).
% fof(187, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|![X3]:(~(ssList(X3))|(~(app(X2,X3)=app(X2,X1))|X3=X1)))),inference(fof_nnf,[status(thm)],[19])).
% fof(188, plain,![X4]:(~(ssList(X4))|![X5]:(~(ssList(X5))|![X6]:(~(ssList(X6))|(~(app(X5,X6)=app(X5,X4))|X6=X4)))),inference(variable_rename,[status(thm)],[187])).
% fof(189, plain,![X4]:![X5]:![X6]:(((~(ssList(X6))|(~(app(X5,X6)=app(X5,X4))|X6=X4))|~(ssList(X5)))|~(ssList(X4))),inference(shift_quantors,[status(thm)],[188])).
% cnf(190,plain,(X3=X1|~ssList(X1)|~ssList(X2)|app(X2,X3)!=app(X2,X1)|~ssList(X3)),inference(split_conjunct,[status(thm)],[189])).
% fof(191, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssItem(X2))|cons(X2,X1)=app(cons(X2,nil),X1))),inference(fof_nnf,[status(thm)],[20])).
% fof(192, plain,![X3]:(~(ssList(X3))|![X4]:(~(ssItem(X4))|cons(X4,X3)=app(cons(X4,nil),X3))),inference(variable_rename,[status(thm)],[191])).
% fof(193, plain,![X3]:![X4]:((~(ssItem(X4))|cons(X4,X3)=app(cons(X4,nil),X3))|~(ssList(X3))),inference(shift_quantors,[status(thm)],[192])).
% cnf(194,plain,(cons(X2,X1)=app(cons(X2,nil),X1)|~ssList(X1)|~ssItem(X2)),inference(split_conjunct,[status(thm)],[193])).
% fof(195, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|![X3]:(~(ssList(X3))|app(app(X1,X2),X3)=app(X1,app(X2,X3))))),inference(fof_nnf,[status(thm)],[21])).
% fof(196, plain,![X4]:(~(ssList(X4))|![X5]:(~(ssList(X5))|![X6]:(~(ssList(X6))|app(app(X4,X5),X6)=app(X4,app(X5,X6))))),inference(variable_rename,[status(thm)],[195])).
% fof(197, plain,![X4]:![X5]:![X6]:(((~(ssList(X6))|app(app(X4,X5),X6)=app(X4,app(X5,X6)))|~(ssList(X5)))|~(ssList(X4))),inference(shift_quantors,[status(thm)],[196])).
% cnf(198,plain,(app(app(X1,X2),X3)=app(X1,app(X2,X3))|~ssList(X1)|~ssList(X2)|~ssList(X3)),inference(split_conjunct,[status(thm)],[197])).
% fof(364, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|((~(rearsegP(X1,X2))|?[X3]:(ssList(X3)&app(X3,X2)=X1))&(![X3]:(~(ssList(X3))|~(app(X3,X2)=X1))|rearsegP(X1,X2))))),inference(fof_nnf,[status(thm)],[48])).
% fof(365, plain,![X4]:(~(ssList(X4))|![X5]:(~(ssList(X5))|((~(rearsegP(X4,X5))|?[X6]:(ssList(X6)&app(X6,X5)=X4))&(![X7]:(~(ssList(X7))|~(app(X7,X5)=X4))|rearsegP(X4,X5))))),inference(variable_rename,[status(thm)],[364])).
% fof(366, plain,![X4]:(~(ssList(X4))|![X5]:(~(ssList(X5))|((~(rearsegP(X4,X5))|(ssList(esk34_2(X4,X5))&app(esk34_2(X4,X5),X5)=X4))&(![X7]:(~(ssList(X7))|~(app(X7,X5)=X4))|rearsegP(X4,X5))))),inference(skolemize,[status(esa)],[365])).
% fof(367, plain,![X4]:![X5]:![X7]:(((((~(ssList(X7))|~(app(X7,X5)=X4))|rearsegP(X4,X5))&(~(rearsegP(X4,X5))|(ssList(esk34_2(X4,X5))&app(esk34_2(X4,X5),X5)=X4)))|~(ssList(X5)))|~(ssList(X4))),inference(shift_quantors,[status(thm)],[366])).
% fof(368, plain,![X4]:![X5]:![X7]:(((((~(ssList(X7))|~(app(X7,X5)=X4))|rearsegP(X4,X5))|~(ssList(X5)))|~(ssList(X4)))&((((ssList(esk34_2(X4,X5))|~(rearsegP(X4,X5)))|~(ssList(X5)))|~(ssList(X4)))&(((app(esk34_2(X4,X5),X5)=X4|~(rearsegP(X4,X5)))|~(ssList(X5)))|~(ssList(X4))))),inference(distribute,[status(thm)],[367])).
% cnf(369,plain,(app(esk34_2(X1,X2),X2)=X1|~ssList(X1)|~ssList(X2)|~rearsegP(X1,X2)),inference(split_conjunct,[status(thm)],[368])).
% cnf(370,plain,(ssList(esk34_2(X1,X2))|~ssList(X1)|~ssList(X2)|~rearsegP(X1,X2)),inference(split_conjunct,[status(thm)],[368])).
% cnf(371,plain,(rearsegP(X1,X2)|~ssList(X1)|~ssList(X2)|app(X3,X2)!=X1|~ssList(X3)),inference(split_conjunct,[status(thm)],[368])).
% fof(568, negated_conjecture,?[X1]:(ssList(X1)&?[X2]:(ssList(X2)&?[X3]:(ssList(X3)&?[X4]:(ssList(X4)&(((X2=X4&X1=X3)&![X5]:(~(ssItem(X5))|![X6]:(~(ssList(X6))|![X7]:((~(ssList(X7))|~(app(app(X6,cons(X5,nil)),X7)=X3))|![X8]:(~(ssItem(X8))|((leq(X5,X8)|~(memberP(X7,X8)))&(leq(X8,X5)|~(memberP(X6,X8)))))))))&?[X9]:(ssItem(X9)&?[X10]:(ssItem(X10)&?[X11]:(ssList(X11)&?[X12]:(ssList(X12)&?[X13]:(ssList(X13)&((app(app(app(app(X11,cons(X9,nil)),X12),cons(X10,nil)),X13)=X1&leq(X10,X9))&(?[X14]:(ssItem(X14)&(memberP(X12,X14)&(~(leq(X9,X14))|~(leq(X14,X10)))))|~(leq(X9,X10)))))))))))))),inference(fof_nnf,[status(thm)],[103])).
% fof(569, negated_conjecture,?[X15]:(ssList(X15)&?[X16]:(ssList(X16)&?[X17]:(ssList(X17)&?[X18]:(ssList(X18)&(((X16=X18&X15=X17)&![X19]:(~(ssItem(X19))|![X20]:(~(ssList(X20))|![X21]:((~(ssList(X21))|~(app(app(X20,cons(X19,nil)),X21)=X17))|![X22]:(~(ssItem(X22))|((leq(X19,X22)|~(memberP(X21,X22)))&(leq(X22,X19)|~(memberP(X20,X22)))))))))&?[X23]:(ssItem(X23)&?[X24]:(ssItem(X24)&?[X25]:(ssList(X25)&?[X26]:(ssList(X26)&?[X27]:(ssList(X27)&((app(app(app(app(X25,cons(X23,nil)),X26),cons(X24,nil)),X27)=X15&leq(X24,X23))&(?[X28]:(ssItem(X28)&(memberP(X26,X28)&(~(leq(X23,X28))|~(leq(X28,X24)))))|~(leq(X23,X24)))))))))))))),inference(variable_rename,[status(thm)],[568])).
% fof(570, negated_conjecture,(ssList(esk48_0)&(ssList(esk49_0)&(ssList(esk50_0)&(ssList(esk51_0)&(((esk49_0=esk51_0&esk48_0=esk50_0)&![X19]:(~(ssItem(X19))|![X20]:(~(ssList(X20))|![X21]:((~(ssList(X21))|~(app(app(X20,cons(X19,nil)),X21)=esk50_0))|![X22]:(~(ssItem(X22))|((leq(X19,X22)|~(memberP(X21,X22)))&(leq(X22,X19)|~(memberP(X20,X22)))))))))&(ssItem(esk52_0)&(ssItem(esk53_0)&(ssList(esk54_0)&(ssList(esk55_0)&(ssList(esk56_0)&((app(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),cons(esk53_0,nil)),esk56_0)=esk48_0&leq(esk53_0,esk52_0))&((ssItem(esk57_0)&(memberP(esk55_0,esk57_0)&(~(leq(esk52_0,esk57_0))|~(leq(esk57_0,esk53_0)))))|~(leq(esk52_0,esk53_0)))))))))))))),inference(skolemize,[status(esa)],[569])).
% fof(571, negated_conjecture,![X19]:![X20]:![X21]:![X22]:((((((((((~(ssItem(X22))|((leq(X19,X22)|~(memberP(X21,X22)))&(leq(X22,X19)|~(memberP(X20,X22)))))|(~(ssList(X21))|~(app(app(X20,cons(X19,nil)),X21)=esk50_0)))|~(ssList(X20)))|~(ssItem(X19)))&(esk49_0=esk51_0&esk48_0=esk50_0))&(ssItem(esk52_0)&(ssItem(esk53_0)&(ssList(esk54_0)&(ssList(esk55_0)&(ssList(esk56_0)&((app(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),cons(esk53_0,nil)),esk56_0)=esk48_0&leq(esk53_0,esk52_0))&((ssItem(esk57_0)&(memberP(esk55_0,esk57_0)&(~(leq(esk52_0,esk57_0))|~(leq(esk57_0,esk53_0)))))|~(leq(esk52_0,esk53_0))))))))))&ssList(esk51_0))&ssList(esk50_0))&ssList(esk49_0))&ssList(esk48_0)),inference(shift_quantors,[status(thm)],[570])).
% fof(572, negated_conjecture,![X19]:![X20]:![X21]:![X22]:((((((((((((leq(X19,X22)|~(memberP(X21,X22)))|~(ssItem(X22)))|(~(ssList(X21))|~(app(app(X20,cons(X19,nil)),X21)=esk50_0)))|~(ssList(X20)))|~(ssItem(X19)))&(((((leq(X22,X19)|~(memberP(X20,X22)))|~(ssItem(X22)))|(~(ssList(X21))|~(app(app(X20,cons(X19,nil)),X21)=esk50_0)))|~(ssList(X20)))|~(ssItem(X19))))&(esk49_0=esk51_0&esk48_0=esk50_0))&(ssItem(esk52_0)&(ssItem(esk53_0)&(ssList(esk54_0)&(ssList(esk55_0)&(ssList(esk56_0)&((app(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),cons(esk53_0,nil)),esk56_0)=esk48_0&leq(esk53_0,esk52_0))&((ssItem(esk57_0)|~(leq(esk52_0,esk53_0)))&((memberP(esk55_0,esk57_0)|~(leq(esk52_0,esk53_0)))&((~(leq(esk52_0,esk57_0))|~(leq(esk57_0,esk53_0)))|~(leq(esk52_0,esk53_0))))))))))))&ssList(esk51_0))&ssList(esk50_0))&ssList(esk49_0))&ssList(esk48_0)),inference(distribute,[status(thm)],[571])).
% cnf(577,negated_conjecture,(~leq(esk52_0,esk53_0)|~leq(esk57_0,esk53_0)|~leq(esk52_0,esk57_0)),inference(split_conjunct,[status(thm)],[572])).
% cnf(578,negated_conjecture,(memberP(esk55_0,esk57_0)|~leq(esk52_0,esk53_0)),inference(split_conjunct,[status(thm)],[572])).
% cnf(579,negated_conjecture,(ssItem(esk57_0)|~leq(esk52_0,esk53_0)),inference(split_conjunct,[status(thm)],[572])).
% cnf(580,negated_conjecture,(leq(esk53_0,esk52_0)),inference(split_conjunct,[status(thm)],[572])).
% cnf(581,negated_conjecture,(app(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),cons(esk53_0,nil)),esk56_0)=esk48_0),inference(split_conjunct,[status(thm)],[572])).
% cnf(582,negated_conjecture,(ssList(esk56_0)),inference(split_conjunct,[status(thm)],[572])).
% cnf(583,negated_conjecture,(ssList(esk55_0)),inference(split_conjunct,[status(thm)],[572])).
% cnf(584,negated_conjecture,(ssList(esk54_0)),inference(split_conjunct,[status(thm)],[572])).
% cnf(585,negated_conjecture,(ssItem(esk53_0)),inference(split_conjunct,[status(thm)],[572])).
% cnf(586,negated_conjecture,(ssItem(esk52_0)),inference(split_conjunct,[status(thm)],[572])).
% cnf(587,negated_conjecture,(esk48_0=esk50_0),inference(split_conjunct,[status(thm)],[572])).
% cnf(589,negated_conjecture,(leq(X4,X1)|~ssItem(X1)|~ssList(X2)|app(app(X2,cons(X1,nil)),X3)!=esk50_0|~ssList(X3)|~ssItem(X4)|~memberP(X2,X4)),inference(split_conjunct,[status(thm)],[572])).
% cnf(590,negated_conjecture,(leq(X1,X4)|~ssItem(X1)|~ssList(X2)|app(app(X2,cons(X1,nil)),X3)!=esk50_0|~ssList(X3)|~ssItem(X4)|~memberP(X3,X4)),inference(split_conjunct,[status(thm)],[572])).
% cnf(595,negated_conjecture,(app(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),cons(esk53_0,nil)),esk56_0)=esk50_0),inference(rw,[status(thm)],[581,587,theory(equality)])).
% cnf(679,negated_conjecture,(esk52_0=esk53_0|~leq(esk52_0,esk53_0)|~ssItem(esk53_0)|~ssItem(esk52_0)),inference(spm,[status(thm)],[158,580,theory(equality)])).
% cnf(680,negated_conjecture,(esk52_0=esk53_0|~leq(esk52_0,esk53_0)|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[679,585,theory(equality)])).
% cnf(681,negated_conjecture,(esk52_0=esk53_0|~leq(esk52_0,esk53_0)|$false|$false),inference(rw,[status(thm)],[680,586,theory(equality)])).
% cnf(682,negated_conjecture,(esk52_0=esk53_0|~leq(esk52_0,esk53_0)),inference(cn,[status(thm)],[681,theory(equality)])).
% cnf(713,plain,(memberP(cons(X1,X2),X1)|~ssList(X2)|~ssItem(X1)),inference(er,[status(thm)],[178,theory(equality)])).
% cnf(780,plain,(rearsegP(app(X1,X2),X2)|~ssList(X1)|~ssList(X2)|~ssList(app(X1,X2))),inference(er,[status(thm)],[371,theory(equality)])).
% cnf(921,plain,(X1=X2|app(app(X3,X4),X1)!=app(X3,app(X4,X2))|~ssList(X2)|~ssList(app(X3,X4))|~ssList(X1)|~ssList(X4)|~ssList(X3)),inference(spm,[status(thm)],[190,198,theory(equality)])).
% cnf(925,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(esk56_0)|~ssList(cons(esk53_0,nil))|~ssList(app(app(esk54_0,cons(esk52_0,nil)),esk55_0))),inference(spm,[status(thm)],[595,198,theory(equality)])).
% cnf(926,negated_conjecture,(app(app(app(esk54_0,app(cons(esk52_0,nil),esk55_0)),cons(esk53_0,nil)),esk56_0)=esk50_0|~ssList(esk55_0)|~ssList(cons(esk52_0,nil))|~ssList(esk54_0)),inference(spm,[status(thm)],[595,198,theory(equality)])).
% cnf(935,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0|$false|~ssList(cons(esk53_0,nil))|~ssList(app(app(esk54_0,cons(esk52_0,nil)),esk55_0))),inference(rw,[status(thm)],[925,582,theory(equality)])).
% cnf(936,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(cons(esk53_0,nil))|~ssList(app(app(esk54_0,cons(esk52_0,nil)),esk55_0))),inference(cn,[status(thm)],[935,theory(equality)])).
% cnf(937,negated_conjecture,(app(app(app(esk54_0,app(cons(esk52_0,nil),esk55_0)),cons(esk53_0,nil)),esk56_0)=esk50_0|$false|~ssList(cons(esk52_0,nil))|~ssList(esk54_0)),inference(rw,[status(thm)],[926,583,theory(equality)])).
% cnf(938,negated_conjecture,(app(app(app(esk54_0,app(cons(esk52_0,nil),esk55_0)),cons(esk53_0,nil)),esk56_0)=esk50_0|$false|~ssList(cons(esk52_0,nil))|$false),inference(rw,[status(thm)],[937,584,theory(equality)])).
% cnf(939,negated_conjecture,(app(app(app(esk54_0,app(cons(esk52_0,nil),esk55_0)),cons(esk53_0,nil)),esk56_0)=esk50_0|~ssList(cons(esk52_0,nil))),inference(cn,[status(thm)],[938,theory(equality)])).
% cnf(1004,negated_conjecture,(leq(X1,esk53_0)|~memberP(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),X1)|~ssList(esk56_0)|~ssList(app(app(esk54_0,cons(esk52_0,nil)),esk55_0))|~ssItem(X1)|~ssItem(esk53_0)),inference(spm,[status(thm)],[589,595,theory(equality)])).
% cnf(1010,negated_conjecture,(leq(X1,esk53_0)|~memberP(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),X1)|$false|~ssList(app(app(esk54_0,cons(esk52_0,nil)),esk55_0))|~ssItem(X1)|~ssItem(esk53_0)),inference(rw,[status(thm)],[1004,582,theory(equality)])).
% cnf(1011,negated_conjecture,(leq(X1,esk53_0)|~memberP(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),X1)|$false|~ssList(app(app(esk54_0,cons(esk52_0,nil)),esk55_0))|~ssItem(X1)|$false),inference(rw,[status(thm)],[1010,585,theory(equality)])).
% cnf(1012,negated_conjecture,(leq(X1,esk53_0)|~memberP(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),X1)|~ssList(app(app(esk54_0,cons(esk52_0,nil)),esk55_0))|~ssItem(X1)),inference(cn,[status(thm)],[1011,theory(equality)])).
% cnf(1629,negated_conjecture,(app(app(app(esk54_0,app(cons(esk52_0,nil),esk55_0)),cons(esk53_0,nil)),esk56_0)=esk50_0|~ssList(nil)|~ssItem(esk52_0)),inference(spm,[status(thm)],[939,121,theory(equality)])).
% cnf(1630,negated_conjecture,(app(app(app(esk54_0,app(cons(esk52_0,nil),esk55_0)),cons(esk53_0,nil)),esk56_0)=esk50_0|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[1629,122,theory(equality)])).
% cnf(1631,negated_conjecture,(app(app(app(esk54_0,app(cons(esk52_0,nil),esk55_0)),cons(esk53_0,nil)),esk56_0)=esk50_0|$false|$false),inference(rw,[status(thm)],[1630,586,theory(equality)])).
% cnf(1632,negated_conjecture,(app(app(app(esk54_0,app(cons(esk52_0,nil),esk55_0)),cons(esk53_0,nil)),esk56_0)=esk50_0),inference(cn,[status(thm)],[1631,theory(equality)])).
% cnf(1652,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,esk55_0)),cons(esk53_0,nil)),esk56_0)=esk50_0|~ssList(esk55_0)|~ssItem(esk52_0)),inference(spm,[status(thm)],[1632,194,theory(equality)])).
% cnf(1698,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,esk55_0)),cons(esk53_0,nil)),esk56_0)=esk50_0|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[1652,583,theory(equality)])).
% cnf(1699,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,esk55_0)),cons(esk53_0,nil)),esk56_0)=esk50_0|$false|$false),inference(rw,[status(thm)],[1698,586,theory(equality)])).
% cnf(1700,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,esk55_0)),cons(esk53_0,nil)),esk56_0)=esk50_0),inference(cn,[status(thm)],[1699,theory(equality)])).
% cnf(1717,negated_conjecture,(esk50_0=app(app(esk54_0,cons(esk52_0,esk55_0)),app(cons(esk53_0,nil),esk56_0))|~ssList(esk56_0)|~ssList(cons(esk53_0,nil))|~ssList(app(esk54_0,cons(esk52_0,esk55_0)))),inference(spm,[status(thm)],[198,1700,theory(equality)])).
% cnf(1721,negated_conjecture,(app(app(esk54_0,app(cons(esk52_0,esk55_0),cons(esk53_0,nil))),esk56_0)=esk50_0|~ssList(cons(esk53_0,nil))|~ssList(cons(esk52_0,esk55_0))|~ssList(esk54_0)),inference(spm,[status(thm)],[1700,198,theory(equality)])).
% cnf(1751,negated_conjecture,(esk50_0=app(app(esk54_0,cons(esk52_0,esk55_0)),app(cons(esk53_0,nil),esk56_0))|$false|~ssList(cons(esk53_0,nil))|~ssList(app(esk54_0,cons(esk52_0,esk55_0)))),inference(rw,[status(thm)],[1717,582,theory(equality)])).
% cnf(1752,negated_conjecture,(esk50_0=app(app(esk54_0,cons(esk52_0,esk55_0)),app(cons(esk53_0,nil),esk56_0))|~ssList(cons(esk53_0,nil))|~ssList(app(esk54_0,cons(esk52_0,esk55_0)))),inference(cn,[status(thm)],[1751,theory(equality)])).
% cnf(1761,negated_conjecture,(app(app(esk54_0,app(cons(esk52_0,esk55_0),cons(esk53_0,nil))),esk56_0)=esk50_0|~ssList(cons(esk53_0,nil))|~ssList(cons(esk52_0,esk55_0))|$false),inference(rw,[status(thm)],[1721,584,theory(equality)])).
% cnf(1762,negated_conjecture,(app(app(esk54_0,app(cons(esk52_0,esk55_0),cons(esk53_0,nil))),esk56_0)=esk50_0|~ssList(cons(esk53_0,nil))|~ssList(cons(esk52_0,esk55_0))),inference(cn,[status(thm)],[1761,theory(equality)])).
% cnf(1827,negated_conjecture,(app(app(esk54_0,app(cons(esk52_0,esk55_0),cons(esk53_0,nil))),esk56_0)=esk50_0|~ssList(cons(esk52_0,esk55_0))|~ssList(nil)|~ssItem(esk53_0)),inference(spm,[status(thm)],[1762,121,theory(equality)])).
% cnf(1828,negated_conjecture,(app(app(esk54_0,app(cons(esk52_0,esk55_0),cons(esk53_0,nil))),esk56_0)=esk50_0|~ssList(cons(esk52_0,esk55_0))|$false|~ssItem(esk53_0)),inference(rw,[status(thm)],[1827,122,theory(equality)])).
% cnf(1829,negated_conjecture,(app(app(esk54_0,app(cons(esk52_0,esk55_0),cons(esk53_0,nil))),esk56_0)=esk50_0|~ssList(cons(esk52_0,esk55_0))|$false|$false),inference(rw,[status(thm)],[1828,585,theory(equality)])).
% cnf(1830,negated_conjecture,(app(app(esk54_0,app(cons(esk52_0,esk55_0),cons(esk53_0,nil))),esk56_0)=esk50_0|~ssList(cons(esk52_0,esk55_0))),inference(cn,[status(thm)],[1829,theory(equality)])).
% cnf(1831,negated_conjecture,(app(app(esk54_0,app(cons(esk52_0,esk55_0),cons(esk53_0,nil))),esk56_0)=esk50_0|~ssList(esk55_0)|~ssItem(esk52_0)),inference(spm,[status(thm)],[1830,121,theory(equality)])).
% cnf(1832,negated_conjecture,(app(app(esk54_0,app(cons(esk52_0,esk55_0),cons(esk53_0,nil))),esk56_0)=esk50_0|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[1831,583,theory(equality)])).
% cnf(1833,negated_conjecture,(app(app(esk54_0,app(cons(esk52_0,esk55_0),cons(esk53_0,nil))),esk56_0)=esk50_0|$false|$false),inference(rw,[status(thm)],[1832,586,theory(equality)])).
% cnf(1834,negated_conjecture,(app(app(esk54_0,app(cons(esk52_0,esk55_0),cons(esk53_0,nil))),esk56_0)=esk50_0),inference(cn,[status(thm)],[1833,theory(equality)])).
% cnf(1849,negated_conjecture,(esk50_0=app(esk54_0,app(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)),esk56_0))|~ssList(esk56_0)|~ssList(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)))|~ssList(esk54_0)),inference(spm,[status(thm)],[198,1834,theory(equality)])).
% cnf(1882,negated_conjecture,(esk50_0=app(esk54_0,app(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)),esk56_0))|$false|~ssList(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)))|~ssList(esk54_0)),inference(rw,[status(thm)],[1849,582,theory(equality)])).
% cnf(1883,negated_conjecture,(esk50_0=app(esk54_0,app(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)),esk56_0))|$false|~ssList(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)))|$false),inference(rw,[status(thm)],[1882,584,theory(equality)])).
% cnf(1884,negated_conjecture,(esk50_0=app(esk54_0,app(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)),esk56_0))|~ssList(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)))),inference(cn,[status(thm)],[1883,theory(equality)])).
% cnf(1948,negated_conjecture,(app(esk54_0,app(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)),esk56_0))=esk50_0|~ssList(cons(esk53_0,nil))|~ssList(cons(esk52_0,esk55_0))),inference(spm,[status(thm)],[1884,147,theory(equality)])).
% cnf(2311,negated_conjecture,(app(esk54_0,app(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)),esk56_0))=esk50_0|~ssList(cons(esk52_0,esk55_0))|~ssList(nil)|~ssItem(esk53_0)),inference(spm,[status(thm)],[1948,121,theory(equality)])).
% cnf(2312,negated_conjecture,(app(esk54_0,app(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)),esk56_0))=esk50_0|~ssList(cons(esk52_0,esk55_0))|$false|~ssItem(esk53_0)),inference(rw,[status(thm)],[2311,122,theory(equality)])).
% cnf(2313,negated_conjecture,(app(esk54_0,app(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)),esk56_0))=esk50_0|~ssList(cons(esk52_0,esk55_0))|$false|$false),inference(rw,[status(thm)],[2312,585,theory(equality)])).
% cnf(2314,negated_conjecture,(app(esk54_0,app(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)),esk56_0))=esk50_0|~ssList(cons(esk52_0,esk55_0))),inference(cn,[status(thm)],[2313,theory(equality)])).
% cnf(2315,negated_conjecture,(app(esk54_0,app(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)),esk56_0))=esk50_0|~ssList(esk55_0)|~ssItem(esk52_0)),inference(spm,[status(thm)],[2314,121,theory(equality)])).
% cnf(2316,negated_conjecture,(app(esk54_0,app(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)),esk56_0))=esk50_0|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[2315,583,theory(equality)])).
% cnf(2317,negated_conjecture,(app(esk54_0,app(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)),esk56_0))=esk50_0|$false|$false),inference(rw,[status(thm)],[2316,586,theory(equality)])).
% cnf(2318,negated_conjecture,(app(esk54_0,app(app(cons(esk52_0,esk55_0),cons(esk53_0,nil)),esk56_0))=esk50_0),inference(cn,[status(thm)],[2317,theory(equality)])).
% cnf(2334,negated_conjecture,(app(esk54_0,app(cons(esk52_0,esk55_0),app(cons(esk53_0,nil),esk56_0)))=esk50_0|~ssList(esk56_0)|~ssList(cons(esk53_0,nil))|~ssList(cons(esk52_0,esk55_0))),inference(spm,[status(thm)],[2318,198,theory(equality)])).
% cnf(2370,negated_conjecture,(app(esk54_0,app(cons(esk52_0,esk55_0),app(cons(esk53_0,nil),esk56_0)))=esk50_0|$false|~ssList(cons(esk53_0,nil))|~ssList(cons(esk52_0,esk55_0))),inference(rw,[status(thm)],[2334,582,theory(equality)])).
% cnf(2371,negated_conjecture,(app(esk54_0,app(cons(esk52_0,esk55_0),app(cons(esk53_0,nil),esk56_0)))=esk50_0|~ssList(cons(esk53_0,nil))|~ssList(cons(esk52_0,esk55_0))),inference(cn,[status(thm)],[2370,theory(equality)])).
% cnf(2372,negated_conjecture,(app(esk54_0,app(cons(esk52_0,esk55_0),app(cons(esk53_0,nil),esk56_0)))=esk50_0|~ssList(cons(esk52_0,esk55_0))|~ssList(nil)|~ssItem(esk53_0)),inference(spm,[status(thm)],[2371,121,theory(equality)])).
% cnf(2373,negated_conjecture,(app(esk54_0,app(cons(esk52_0,esk55_0),app(cons(esk53_0,nil),esk56_0)))=esk50_0|~ssList(cons(esk52_0,esk55_0))|$false|~ssItem(esk53_0)),inference(rw,[status(thm)],[2372,122,theory(equality)])).
% cnf(2374,negated_conjecture,(app(esk54_0,app(cons(esk52_0,esk55_0),app(cons(esk53_0,nil),esk56_0)))=esk50_0|~ssList(cons(esk52_0,esk55_0))|$false|$false),inference(rw,[status(thm)],[2373,585,theory(equality)])).
% cnf(2375,negated_conjecture,(app(esk54_0,app(cons(esk52_0,esk55_0),app(cons(esk53_0,nil),esk56_0)))=esk50_0|~ssList(cons(esk52_0,esk55_0))),inference(cn,[status(thm)],[2374,theory(equality)])).
% cnf(2376,negated_conjecture,(app(esk54_0,app(cons(esk52_0,esk55_0),app(cons(esk53_0,nil),esk56_0)))=esk50_0|~ssList(esk55_0)|~ssItem(esk52_0)),inference(spm,[status(thm)],[2375,121,theory(equality)])).
% cnf(2377,negated_conjecture,(app(esk54_0,app(cons(esk52_0,esk55_0),app(cons(esk53_0,nil),esk56_0)))=esk50_0|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[2376,583,theory(equality)])).
% cnf(2378,negated_conjecture,(app(esk54_0,app(cons(esk52_0,esk55_0),app(cons(esk53_0,nil),esk56_0)))=esk50_0|$false|$false),inference(rw,[status(thm)],[2377,586,theory(equality)])).
% cnf(2379,negated_conjecture,(app(esk54_0,app(cons(esk52_0,esk55_0),app(cons(esk53_0,nil),esk56_0)))=esk50_0),inference(cn,[status(thm)],[2378,theory(equality)])).
% cnf(2395,negated_conjecture,(app(esk54_0,app(cons(esk52_0,esk55_0),cons(esk53_0,esk56_0)))=esk50_0|~ssList(esk56_0)|~ssItem(esk53_0)),inference(spm,[status(thm)],[2379,194,theory(equality)])).
% cnf(2431,negated_conjecture,(app(esk54_0,app(cons(esk52_0,esk55_0),cons(esk53_0,esk56_0)))=esk50_0|$false|~ssItem(esk53_0)),inference(rw,[status(thm)],[2395,582,theory(equality)])).
% cnf(2432,negated_conjecture,(app(esk54_0,app(cons(esk52_0,esk55_0),cons(esk53_0,esk56_0)))=esk50_0|$false|$false),inference(rw,[status(thm)],[2431,585,theory(equality)])).
% cnf(2433,negated_conjecture,(app(esk54_0,app(cons(esk52_0,esk55_0),cons(esk53_0,esk56_0)))=esk50_0),inference(cn,[status(thm)],[2432,theory(equality)])).
% cnf(2538,negated_conjecture,(app(app(esk54_0,cons(esk52_0,esk55_0)),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(app(esk54_0,cons(esk52_0,esk55_0)))|~ssList(nil)|~ssItem(esk53_0)),inference(spm,[status(thm)],[1752,121,theory(equality)])).
% cnf(2539,negated_conjecture,(app(app(esk54_0,cons(esk52_0,esk55_0)),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(app(esk54_0,cons(esk52_0,esk55_0)))|$false|~ssItem(esk53_0)),inference(rw,[status(thm)],[2538,122,theory(equality)])).
% cnf(2540,negated_conjecture,(app(app(esk54_0,cons(esk52_0,esk55_0)),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(app(esk54_0,cons(esk52_0,esk55_0)))|$false|$false),inference(rw,[status(thm)],[2539,585,theory(equality)])).
% cnf(2541,negated_conjecture,(app(app(esk54_0,cons(esk52_0,esk55_0)),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(app(esk54_0,cons(esk52_0,esk55_0)))),inference(cn,[status(thm)],[2540,theory(equality)])).
% cnf(2542,negated_conjecture,(app(app(esk54_0,cons(esk52_0,esk55_0)),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(cons(esk52_0,esk55_0))|~ssList(esk54_0)),inference(spm,[status(thm)],[2541,147,theory(equality)])).
% cnf(2543,negated_conjecture,(app(app(esk54_0,cons(esk52_0,esk55_0)),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(cons(esk52_0,esk55_0))|$false),inference(rw,[status(thm)],[2542,584,theory(equality)])).
% cnf(2544,negated_conjecture,(app(app(esk54_0,cons(esk52_0,esk55_0)),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(cons(esk52_0,esk55_0))),inference(cn,[status(thm)],[2543,theory(equality)])).
% cnf(2545,negated_conjecture,(app(app(esk54_0,cons(esk52_0,esk55_0)),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(esk55_0)|~ssItem(esk52_0)),inference(spm,[status(thm)],[2544,121,theory(equality)])).
% cnf(2546,negated_conjecture,(app(app(esk54_0,cons(esk52_0,esk55_0)),app(cons(esk53_0,nil),esk56_0))=esk50_0|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[2545,583,theory(equality)])).
% cnf(2547,negated_conjecture,(app(app(esk54_0,cons(esk52_0,esk55_0)),app(cons(esk53_0,nil),esk56_0))=esk50_0|$false|$false),inference(rw,[status(thm)],[2546,586,theory(equality)])).
% cnf(2548,negated_conjecture,(app(app(esk54_0,cons(esk52_0,esk55_0)),app(cons(esk53_0,nil),esk56_0))=esk50_0),inference(cn,[status(thm)],[2547,theory(equality)])).
% cnf(5145,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(app(app(esk54_0,cons(esk52_0,nil)),esk55_0))|~ssList(nil)|~ssItem(esk53_0)),inference(spm,[status(thm)],[936,121,theory(equality)])).
% cnf(5146,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(app(app(esk54_0,cons(esk52_0,nil)),esk55_0))|$false|~ssItem(esk53_0)),inference(rw,[status(thm)],[5145,122,theory(equality)])).
% cnf(5147,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(app(app(esk54_0,cons(esk52_0,nil)),esk55_0))|$false|$false),inference(rw,[status(thm)],[5146,585,theory(equality)])).
% cnf(5148,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(app(app(esk54_0,cons(esk52_0,nil)),esk55_0))),inference(cn,[status(thm)],[5147,theory(equality)])).
% cnf(5150,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(esk55_0)|~ssList(app(esk54_0,cons(esk52_0,nil)))),inference(spm,[status(thm)],[5148,147,theory(equality)])).
% cnf(5154,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0|$false|~ssList(app(esk54_0,cons(esk52_0,nil)))),inference(rw,[status(thm)],[5150,583,theory(equality)])).
% cnf(5155,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(app(esk54_0,cons(esk52_0,nil)))),inference(cn,[status(thm)],[5154,theory(equality)])).
% cnf(5156,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(cons(esk52_0,nil))|~ssList(esk54_0)),inference(spm,[status(thm)],[5155,147,theory(equality)])).
% cnf(5157,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(cons(esk52_0,nil))|$false),inference(rw,[status(thm)],[5156,584,theory(equality)])).
% cnf(5158,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(cons(esk52_0,nil))),inference(cn,[status(thm)],[5157,theory(equality)])).
% cnf(5159,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0|~ssList(nil)|~ssItem(esk52_0)),inference(spm,[status(thm)],[5158,121,theory(equality)])).
% cnf(5160,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[5159,122,theory(equality)])).
% cnf(5161,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0|$false|$false),inference(rw,[status(thm)],[5160,586,theory(equality)])).
% cnf(5162,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),app(cons(esk53_0,nil),esk56_0))=esk50_0),inference(cn,[status(thm)],[5161,theory(equality)])).
% cnf(5180,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),cons(esk53_0,esk56_0))=esk50_0|~ssList(esk56_0)|~ssItem(esk53_0)),inference(spm,[status(thm)],[5162,194,theory(equality)])).
% cnf(5194,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),cons(esk53_0,esk56_0))=esk50_0|$false|~ssItem(esk53_0)),inference(rw,[status(thm)],[5180,582,theory(equality)])).
% cnf(5195,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),cons(esk53_0,esk56_0))=esk50_0|$false|$false),inference(rw,[status(thm)],[5194,585,theory(equality)])).
% cnf(5196,negated_conjecture,(app(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),cons(esk53_0,esk56_0))=esk50_0),inference(cn,[status(thm)],[5195,theory(equality)])).
% cnf(5220,negated_conjecture,(esk50_0=app(app(esk54_0,cons(esk52_0,nil)),app(esk55_0,cons(esk53_0,esk56_0)))|~ssList(cons(esk53_0,esk56_0))|~ssList(esk55_0)|~ssList(app(esk54_0,cons(esk52_0,nil)))),inference(spm,[status(thm)],[198,5196,theory(equality)])).
% cnf(5242,negated_conjecture,(esk50_0=app(app(esk54_0,cons(esk52_0,nil)),app(esk55_0,cons(esk53_0,esk56_0)))|~ssList(cons(esk53_0,esk56_0))|$false|~ssList(app(esk54_0,cons(esk52_0,nil)))),inference(rw,[status(thm)],[5220,583,theory(equality)])).
% cnf(5243,negated_conjecture,(esk50_0=app(app(esk54_0,cons(esk52_0,nil)),app(esk55_0,cons(esk53_0,esk56_0)))|~ssList(cons(esk53_0,esk56_0))|~ssList(app(esk54_0,cons(esk52_0,nil)))),inference(cn,[status(thm)],[5242,theory(equality)])).
% cnf(5729,negated_conjecture,(app(app(esk54_0,cons(esk52_0,nil)),app(esk55_0,cons(esk53_0,esk56_0)))=esk50_0|~ssList(app(esk54_0,cons(esk52_0,nil)))|~ssList(esk56_0)|~ssItem(esk53_0)),inference(spm,[status(thm)],[5243,121,theory(equality)])).
% cnf(5730,negated_conjecture,(app(app(esk54_0,cons(esk52_0,nil)),app(esk55_0,cons(esk53_0,esk56_0)))=esk50_0|~ssList(app(esk54_0,cons(esk52_0,nil)))|$false|~ssItem(esk53_0)),inference(rw,[status(thm)],[5729,582,theory(equality)])).
% cnf(5731,negated_conjecture,(app(app(esk54_0,cons(esk52_0,nil)),app(esk55_0,cons(esk53_0,esk56_0)))=esk50_0|~ssList(app(esk54_0,cons(esk52_0,nil)))|$false|$false),inference(rw,[status(thm)],[5730,585,theory(equality)])).
% cnf(5732,negated_conjecture,(app(app(esk54_0,cons(esk52_0,nil)),app(esk55_0,cons(esk53_0,esk56_0)))=esk50_0|~ssList(app(esk54_0,cons(esk52_0,nil)))),inference(cn,[status(thm)],[5731,theory(equality)])).
% cnf(5733,negated_conjecture,(app(app(esk54_0,cons(esk52_0,nil)),app(esk55_0,cons(esk53_0,esk56_0)))=esk50_0|~ssList(cons(esk52_0,nil))|~ssList(esk54_0)),inference(spm,[status(thm)],[5732,147,theory(equality)])).
% cnf(5734,negated_conjecture,(app(app(esk54_0,cons(esk52_0,nil)),app(esk55_0,cons(esk53_0,esk56_0)))=esk50_0|~ssList(cons(esk52_0,nil))|$false),inference(rw,[status(thm)],[5733,584,theory(equality)])).
% cnf(5735,negated_conjecture,(app(app(esk54_0,cons(esk52_0,nil)),app(esk55_0,cons(esk53_0,esk56_0)))=esk50_0|~ssList(cons(esk52_0,nil))),inference(cn,[status(thm)],[5734,theory(equality)])).
% cnf(5736,negated_conjecture,(app(app(esk54_0,cons(esk52_0,nil)),app(esk55_0,cons(esk53_0,esk56_0)))=esk50_0|~ssList(nil)|~ssItem(esk52_0)),inference(spm,[status(thm)],[5735,121,theory(equality)])).
% cnf(5737,negated_conjecture,(app(app(esk54_0,cons(esk52_0,nil)),app(esk55_0,cons(esk53_0,esk56_0)))=esk50_0|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[5736,122,theory(equality)])).
% cnf(5738,negated_conjecture,(app(app(esk54_0,cons(esk52_0,nil)),app(esk55_0,cons(esk53_0,esk56_0)))=esk50_0|$false|$false),inference(rw,[status(thm)],[5737,586,theory(equality)])).
% cnf(5739,negated_conjecture,(app(app(esk54_0,cons(esk52_0,nil)),app(esk55_0,cons(esk53_0,esk56_0)))=esk50_0),inference(cn,[status(thm)],[5738,theory(equality)])).
% cnf(5757,negated_conjecture,(leq(esk52_0,X1)|~memberP(app(esk55_0,cons(esk53_0,esk56_0)),X1)|~ssList(app(esk55_0,cons(esk53_0,esk56_0)))|~ssList(esk54_0)|~ssItem(X1)|~ssItem(esk52_0)),inference(spm,[status(thm)],[590,5739,theory(equality)])).
% cnf(5769,negated_conjecture,(leq(esk52_0,X1)|~memberP(app(esk55_0,cons(esk53_0,esk56_0)),X1)|~ssList(app(esk55_0,cons(esk53_0,esk56_0)))|$false|~ssItem(X1)|~ssItem(esk52_0)),inference(rw,[status(thm)],[5757,584,theory(equality)])).
% cnf(5770,negated_conjecture,(leq(esk52_0,X1)|~memberP(app(esk55_0,cons(esk53_0,esk56_0)),X1)|~ssList(app(esk55_0,cons(esk53_0,esk56_0)))|$false|~ssItem(X1)|$false),inference(rw,[status(thm)],[5769,586,theory(equality)])).
% cnf(5771,negated_conjecture,(leq(esk52_0,X1)|~memberP(app(esk55_0,cons(esk53_0,esk56_0)),X1)|~ssList(app(esk55_0,cons(esk53_0,esk56_0)))|~ssItem(X1)),inference(cn,[status(thm)],[5770,theory(equality)])).
% cnf(7247,negated_conjecture,(leq(esk52_0,X1)|~memberP(app(esk55_0,cons(esk53_0,esk56_0)),X1)|~ssItem(X1)|~ssList(cons(esk53_0,esk56_0))|~ssList(esk55_0)),inference(spm,[status(thm)],[5771,147,theory(equality)])).
% cnf(7248,negated_conjecture,(leq(esk52_0,X1)|~memberP(app(esk55_0,cons(esk53_0,esk56_0)),X1)|~ssItem(X1)|~ssList(cons(esk53_0,esk56_0))|$false),inference(rw,[status(thm)],[7247,583,theory(equality)])).
% cnf(7249,negated_conjecture,(leq(esk52_0,X1)|~memberP(app(esk55_0,cons(esk53_0,esk56_0)),X1)|~ssItem(X1)|~ssList(cons(esk53_0,esk56_0))),inference(cn,[status(thm)],[7248,theory(equality)])).
% cnf(7250,negated_conjecture,(leq(esk52_0,X1)|~memberP(app(esk55_0,cons(esk53_0,esk56_0)),X1)|~ssItem(X1)|~ssList(esk56_0)|~ssItem(esk53_0)),inference(spm,[status(thm)],[7249,121,theory(equality)])).
% cnf(7251,negated_conjecture,(leq(esk52_0,X1)|~memberP(app(esk55_0,cons(esk53_0,esk56_0)),X1)|~ssItem(X1)|$false|~ssItem(esk53_0)),inference(rw,[status(thm)],[7250,582,theory(equality)])).
% cnf(7252,negated_conjecture,(leq(esk52_0,X1)|~memberP(app(esk55_0,cons(esk53_0,esk56_0)),X1)|~ssItem(X1)|$false|$false),inference(rw,[status(thm)],[7251,585,theory(equality)])).
% cnf(7253,negated_conjecture,(leq(esk52_0,X1)|~memberP(app(esk55_0,cons(esk53_0,esk56_0)),X1)|~ssItem(X1)),inference(cn,[status(thm)],[7252,theory(equality)])).
% cnf(7460,negated_conjecture,(leq(X1,esk53_0)|~memberP(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),X1)|~ssItem(X1)|~ssList(esk55_0)|~ssList(app(esk54_0,cons(esk52_0,nil)))),inference(spm,[status(thm)],[1012,147,theory(equality)])).
% cnf(7464,negated_conjecture,(leq(X1,esk53_0)|~memberP(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),X1)|~ssItem(X1)|$false|~ssList(app(esk54_0,cons(esk52_0,nil)))),inference(rw,[status(thm)],[7460,583,theory(equality)])).
% cnf(7465,negated_conjecture,(leq(X1,esk53_0)|~memberP(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),X1)|~ssItem(X1)|~ssList(app(esk54_0,cons(esk52_0,nil)))),inference(cn,[status(thm)],[7464,theory(equality)])).
% cnf(7466,negated_conjecture,(leq(X1,esk53_0)|~memberP(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),X1)|~ssItem(X1)|~ssList(cons(esk52_0,nil))|~ssList(esk54_0)),inference(spm,[status(thm)],[7465,147,theory(equality)])).
% cnf(7467,negated_conjecture,(leq(X1,esk53_0)|~memberP(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),X1)|~ssItem(X1)|~ssList(cons(esk52_0,nil))|$false),inference(rw,[status(thm)],[7466,584,theory(equality)])).
% cnf(7468,negated_conjecture,(leq(X1,esk53_0)|~memberP(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),X1)|~ssItem(X1)|~ssList(cons(esk52_0,nil))),inference(cn,[status(thm)],[7467,theory(equality)])).
% cnf(7469,negated_conjecture,(leq(X1,esk53_0)|~memberP(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),X1)|~ssItem(X1)|~ssList(nil)|~ssItem(esk52_0)),inference(spm,[status(thm)],[7468,121,theory(equality)])).
% cnf(7470,negated_conjecture,(leq(X1,esk53_0)|~memberP(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),X1)|~ssItem(X1)|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[7469,122,theory(equality)])).
% cnf(7471,negated_conjecture,(leq(X1,esk53_0)|~memberP(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),X1)|~ssItem(X1)|$false|$false),inference(rw,[status(thm)],[7470,586,theory(equality)])).
% cnf(7472,negated_conjecture,(leq(X1,esk53_0)|~memberP(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),X1)|~ssItem(X1)),inference(cn,[status(thm)],[7471,theory(equality)])).
% cnf(8880,plain,(rearsegP(app(X1,X2),X2)|~ssList(X1)|~ssList(X2)),inference(csr,[status(thm)],[780,147])).
% cnf(21118,plain,(X1=X2|app(app(X3,X4),X1)!=app(X3,app(X4,X2))|~ssList(X1)|~ssList(X4)|~ssList(X3)|~ssList(X2)),inference(csr,[status(thm)],[921,147])).
% cnf(21201,negated_conjecture,(X1=cons(esk53_0,esk56_0)|app(app(esk54_0,cons(esk52_0,esk55_0)),X1)!=esk50_0|~ssList(cons(esk53_0,esk56_0))|~ssList(X1)|~ssList(cons(esk52_0,esk55_0))|~ssList(esk54_0)),inference(spm,[status(thm)],[21118,2433,theory(equality)])).
% cnf(21452,negated_conjecture,(X1=cons(esk53_0,esk56_0)|app(app(esk54_0,cons(esk52_0,esk55_0)),X1)!=esk50_0|~ssList(cons(esk53_0,esk56_0))|~ssList(X1)|~ssList(cons(esk52_0,esk55_0))|$false),inference(rw,[status(thm)],[21201,584,theory(equality)])).
% cnf(21453,negated_conjecture,(X1=cons(esk53_0,esk56_0)|app(app(esk54_0,cons(esk52_0,esk55_0)),X1)!=esk50_0|~ssList(cons(esk53_0,esk56_0))|~ssList(X1)|~ssList(cons(esk52_0,esk55_0))),inference(cn,[status(thm)],[21452,theory(equality)])).
% cnf(52251,negated_conjecture,(X1=cons(esk53_0,esk56_0)|app(app(esk54_0,cons(esk52_0,esk55_0)),X1)!=esk50_0|~ssList(cons(esk52_0,esk55_0))|~ssList(X1)|~ssList(esk56_0)|~ssItem(esk53_0)),inference(spm,[status(thm)],[21453,121,theory(equality)])).
% cnf(52252,negated_conjecture,(X1=cons(esk53_0,esk56_0)|app(app(esk54_0,cons(esk52_0,esk55_0)),X1)!=esk50_0|~ssList(cons(esk52_0,esk55_0))|~ssList(X1)|$false|~ssItem(esk53_0)),inference(rw,[status(thm)],[52251,582,theory(equality)])).
% cnf(52253,negated_conjecture,(X1=cons(esk53_0,esk56_0)|app(app(esk54_0,cons(esk52_0,esk55_0)),X1)!=esk50_0|~ssList(cons(esk52_0,esk55_0))|~ssList(X1)|$false|$false),inference(rw,[status(thm)],[52252,585,theory(equality)])).
% cnf(52254,negated_conjecture,(X1=cons(esk53_0,esk56_0)|app(app(esk54_0,cons(esk52_0,esk55_0)),X1)!=esk50_0|~ssList(cons(esk52_0,esk55_0))|~ssList(X1)),inference(cn,[status(thm)],[52253,theory(equality)])).
% cnf(52255,negated_conjecture,(X1=cons(esk53_0,esk56_0)|app(app(esk54_0,cons(esk52_0,esk55_0)),X1)!=esk50_0|~ssList(X1)|~ssList(esk55_0)|~ssItem(esk52_0)),inference(spm,[status(thm)],[52254,121,theory(equality)])).
% cnf(52256,negated_conjecture,(X1=cons(esk53_0,esk56_0)|app(app(esk54_0,cons(esk52_0,esk55_0)),X1)!=esk50_0|~ssList(X1)|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[52255,583,theory(equality)])).
% cnf(52257,negated_conjecture,(X1=cons(esk53_0,esk56_0)|app(app(esk54_0,cons(esk52_0,esk55_0)),X1)!=esk50_0|~ssList(X1)|$false|$false),inference(rw,[status(thm)],[52256,586,theory(equality)])).
% cnf(52258,negated_conjecture,(X1=cons(esk53_0,esk56_0)|app(app(esk54_0,cons(esk52_0,esk55_0)),X1)!=esk50_0|~ssList(X1)),inference(cn,[status(thm)],[52257,theory(equality)])).
% cnf(52264,negated_conjecture,(app(cons(esk53_0,nil),esk56_0)=cons(esk53_0,esk56_0)|~ssList(app(cons(esk53_0,nil),esk56_0))),inference(spm,[status(thm)],[52258,2548,theory(equality)])).
% cnf(52274,negated_conjecture,(app(cons(esk53_0,nil),esk56_0)=cons(esk53_0,esk56_0)|~ssList(esk56_0)|~ssList(cons(esk53_0,nil))),inference(spm,[status(thm)],[52264,147,theory(equality)])).
% cnf(52279,negated_conjecture,(app(cons(esk53_0,nil),esk56_0)=cons(esk53_0,esk56_0)|$false|~ssList(cons(esk53_0,nil))),inference(rw,[status(thm)],[52274,582,theory(equality)])).
% cnf(52280,negated_conjecture,(app(cons(esk53_0,nil),esk56_0)=cons(esk53_0,esk56_0)|~ssList(cons(esk53_0,nil))),inference(cn,[status(thm)],[52279,theory(equality)])).
% cnf(52281,negated_conjecture,(app(cons(esk53_0,nil),esk56_0)=cons(esk53_0,esk56_0)|~ssList(nil)|~ssItem(esk53_0)),inference(spm,[status(thm)],[52280,121,theory(equality)])).
% cnf(52283,negated_conjecture,(app(cons(esk53_0,nil),esk56_0)=cons(esk53_0,esk56_0)|$false|~ssItem(esk53_0)),inference(rw,[status(thm)],[52281,122,theory(equality)])).
% cnf(52284,negated_conjecture,(app(cons(esk53_0,nil),esk56_0)=cons(esk53_0,esk56_0)|$false|$false),inference(rw,[status(thm)],[52283,585,theory(equality)])).
% cnf(52285,negated_conjecture,(app(cons(esk53_0,nil),esk56_0)=cons(esk53_0,esk56_0)),inference(cn,[status(thm)],[52284,theory(equality)])).
% cnf(52289,negated_conjecture,(ssList(cons(esk53_0,esk56_0))|~ssList(esk56_0)|~ssList(cons(esk53_0,nil))),inference(spm,[status(thm)],[147,52285,theory(equality)])).
% cnf(52295,negated_conjecture,(rearsegP(cons(esk53_0,esk56_0),esk56_0)|~ssList(cons(esk53_0,nil))|~ssList(esk56_0)),inference(spm,[status(thm)],[8880,52285,theory(equality)])).
% cnf(52356,negated_conjecture,(cons(esk53_0,esk56_0)=cons(esk53_0,app(nil,esk56_0))|~ssList(nil)|~ssList(esk56_0)|~ssItem(esk53_0)),inference(spm,[status(thm)],[151,52285,theory(equality)])).
% cnf(52488,negated_conjecture,(ssList(cons(esk53_0,esk56_0))|$false|~ssList(cons(esk53_0,nil))),inference(rw,[status(thm)],[52289,582,theory(equality)])).
% cnf(52489,negated_conjecture,(ssList(cons(esk53_0,esk56_0))|~ssList(cons(esk53_0,nil))),inference(cn,[status(thm)],[52488,theory(equality)])).
% cnf(52500,negated_conjecture,(rearsegP(cons(esk53_0,esk56_0),esk56_0)|~ssList(cons(esk53_0,nil))|$false),inference(rw,[status(thm)],[52295,582,theory(equality)])).
% cnf(52501,negated_conjecture,(rearsegP(cons(esk53_0,esk56_0),esk56_0)|~ssList(cons(esk53_0,nil))),inference(cn,[status(thm)],[52500,theory(equality)])).
% cnf(52622,negated_conjecture,(cons(esk53_0,esk56_0)=cons(esk53_0,app(nil,esk56_0))|$false|~ssList(esk56_0)|~ssItem(esk53_0)),inference(rw,[status(thm)],[52356,122,theory(equality)])).
% cnf(52623,negated_conjecture,(cons(esk53_0,esk56_0)=cons(esk53_0,app(nil,esk56_0))|$false|$false|~ssItem(esk53_0)),inference(rw,[status(thm)],[52622,582,theory(equality)])).
% cnf(52624,negated_conjecture,(cons(esk53_0,esk56_0)=cons(esk53_0,app(nil,esk56_0))|$false|$false|$false),inference(rw,[status(thm)],[52623,585,theory(equality)])).
% cnf(52625,negated_conjecture,(cons(esk53_0,esk56_0)=cons(esk53_0,app(nil,esk56_0))),inference(cn,[status(thm)],[52624,theory(equality)])).
% cnf(52650,negated_conjecture,(ssList(cons(esk53_0,esk56_0))|~ssList(nil)|~ssItem(esk53_0)),inference(spm,[status(thm)],[52489,121,theory(equality)])).
% cnf(52652,negated_conjecture,(ssList(cons(esk53_0,esk56_0))|$false|~ssItem(esk53_0)),inference(rw,[status(thm)],[52650,122,theory(equality)])).
% cnf(52653,negated_conjecture,(ssList(cons(esk53_0,esk56_0))|$false|$false),inference(rw,[status(thm)],[52652,585,theory(equality)])).
% cnf(52654,negated_conjecture,(ssList(cons(esk53_0,esk56_0))),inference(cn,[status(thm)],[52653,theory(equality)])).
% cnf(52695,negated_conjecture,(memberP(cons(esk53_0,esk56_0),esk53_0)|~ssList(app(nil,esk56_0))|~ssItem(esk53_0)),inference(spm,[status(thm)],[713,52625,theory(equality)])).
% cnf(52979,negated_conjecture,(memberP(cons(esk53_0,esk56_0),esk53_0)|~ssList(app(nil,esk56_0))|$false),inference(rw,[status(thm)],[52695,585,theory(equality)])).
% cnf(52980,negated_conjecture,(memberP(cons(esk53_0,esk56_0),esk53_0)|~ssList(app(nil,esk56_0))),inference(cn,[status(thm)],[52979,theory(equality)])).
% cnf(53268,negated_conjecture,(memberP(cons(esk53_0,esk56_0),esk53_0)|~ssList(esk56_0)),inference(spm,[status(thm)],[52980,154,theory(equality)])).
% cnf(53271,negated_conjecture,(memberP(cons(esk53_0,esk56_0),esk53_0)|$false),inference(rw,[status(thm)],[53268,582,theory(equality)])).
% cnf(53272,negated_conjecture,(memberP(cons(esk53_0,esk56_0),esk53_0)),inference(cn,[status(thm)],[53271,theory(equality)])).
% cnf(53285,negated_conjecture,(memberP(app(X1,cons(esk53_0,esk56_0)),esk53_0)|~ssList(cons(esk53_0,esk56_0))|~ssList(X1)|~ssItem(esk53_0)),inference(spm,[status(thm)],[170,53272,theory(equality)])).
% cnf(53313,negated_conjecture,(memberP(app(X1,cons(esk53_0,esk56_0)),esk53_0)|$false|~ssList(X1)|~ssItem(esk53_0)),inference(rw,[status(thm)],[53285,52654,theory(equality)])).
% cnf(53314,negated_conjecture,(memberP(app(X1,cons(esk53_0,esk56_0)),esk53_0)|$false|~ssList(X1)|$false),inference(rw,[status(thm)],[53313,585,theory(equality)])).
% cnf(53315,negated_conjecture,(memberP(app(X1,cons(esk53_0,esk56_0)),esk53_0)|~ssList(X1)),inference(cn,[status(thm)],[53314,theory(equality)])).
% cnf(59594,negated_conjecture,(rearsegP(cons(esk53_0,esk56_0),esk56_0)|~ssList(nil)|~ssItem(esk53_0)),inference(spm,[status(thm)],[52501,121,theory(equality)])).
% cnf(59596,negated_conjecture,(rearsegP(cons(esk53_0,esk56_0),esk56_0)|$false|~ssItem(esk53_0)),inference(rw,[status(thm)],[59594,122,theory(equality)])).
% cnf(59597,negated_conjecture,(rearsegP(cons(esk53_0,esk56_0),esk56_0)|$false|$false),inference(rw,[status(thm)],[59596,585,theory(equality)])).
% cnf(59598,negated_conjecture,(rearsegP(cons(esk53_0,esk56_0),esk56_0)),inference(cn,[status(thm)],[59597,theory(equality)])).
% cnf(64150,negated_conjecture,(leq(esk52_0,esk53_0)|~ssItem(esk53_0)|~ssList(esk55_0)),inference(spm,[status(thm)],[7253,53315,theory(equality)])).
% cnf(64184,negated_conjecture,(leq(esk52_0,esk53_0)|$false|~ssList(esk55_0)),inference(rw,[status(thm)],[64150,585,theory(equality)])).
% cnf(64185,negated_conjecture,(leq(esk52_0,esk53_0)|$false|$false),inference(rw,[status(thm)],[64184,583,theory(equality)])).
% cnf(64186,negated_conjecture,(leq(esk52_0,esk53_0)),inference(cn,[status(thm)],[64185,theory(equality)])).
% cnf(64234,negated_conjecture,(esk53_0=esk52_0|$false),inference(rw,[status(thm)],[682,64186,theory(equality)])).
% cnf(64235,negated_conjecture,(esk53_0=esk52_0),inference(cn,[status(thm)],[64234,theory(equality)])).
% cnf(64236,negated_conjecture,($false|~leq(esk52_0,esk57_0)|~leq(esk57_0,esk53_0)),inference(rw,[status(thm)],[577,64186,theory(equality)])).
% cnf(64237,negated_conjecture,(~leq(esk52_0,esk57_0)|~leq(esk57_0,esk53_0)),inference(cn,[status(thm)],[64236,theory(equality)])).
% cnf(64238,negated_conjecture,(memberP(esk55_0,esk57_0)|$false),inference(rw,[status(thm)],[578,64186,theory(equality)])).
% cnf(64239,negated_conjecture,(memberP(esk55_0,esk57_0)),inference(cn,[status(thm)],[64238,theory(equality)])).
% cnf(64240,negated_conjecture,(ssItem(esk57_0)|$false),inference(rw,[status(thm)],[579,64186,theory(equality)])).
% cnf(64241,negated_conjecture,(ssItem(esk57_0)),inference(cn,[status(thm)],[64240,theory(equality)])).
% cnf(64260,negated_conjecture,(app(cons(esk52_0,nil),esk56_0)=cons(esk53_0,esk56_0)),inference(rw,[status(thm)],[52285,64235,theory(equality)])).
% cnf(64261,negated_conjecture,(app(cons(esk52_0,nil),esk56_0)=cons(esk52_0,esk56_0)),inference(rw,[status(thm)],[64260,64235,theory(equality)])).
% cnf(64311,negated_conjecture,(rearsegP(cons(esk52_0,esk56_0),esk56_0)),inference(rw,[status(thm)],[59598,64235,theory(equality)])).
% cnf(64344,negated_conjecture,(ssList(cons(esk52_0,esk56_0))),inference(rw,[status(thm)],[52654,64235,theory(equality)])).
% cnf(64703,negated_conjecture,(leq(X1,esk52_0)|~memberP(app(app(esk54_0,cons(esk52_0,nil)),esk55_0),X1)|~ssItem(X1)),inference(rw,[status(thm)],[7472,64235,theory(equality)])).
% cnf(64706,negated_conjecture,(leq(esk52_0,X1)|~memberP(app(esk55_0,cons(esk52_0,esk56_0)),X1)|~ssItem(X1)),inference(rw,[status(thm)],[7253,64235,theory(equality)])).
% cnf(64942,negated_conjecture,(memberP(app(X1,esk55_0),esk57_0)|~ssList(esk55_0)|~ssList(X1)|~ssItem(esk57_0)),inference(spm,[status(thm)],[170,64239,theory(equality)])).
% cnf(64943,negated_conjecture,(memberP(app(esk55_0,X1),esk57_0)|~ssList(X1)|~ssList(esk55_0)|~ssItem(esk57_0)),inference(spm,[status(thm)],[171,64239,theory(equality)])).
% cnf(64965,negated_conjecture,(memberP(app(X1,esk55_0),esk57_0)|$false|~ssList(X1)|~ssItem(esk57_0)),inference(rw,[status(thm)],[64942,583,theory(equality)])).
% cnf(64966,negated_conjecture,(memberP(app(X1,esk55_0),esk57_0)|$false|~ssList(X1)|$false),inference(rw,[status(thm)],[64965,64241,theory(equality)])).
% cnf(64967,negated_conjecture,(memberP(app(X1,esk55_0),esk57_0)|~ssList(X1)),inference(cn,[status(thm)],[64966,theory(equality)])).
% cnf(64968,negated_conjecture,(memberP(app(esk55_0,X1),esk57_0)|~ssList(X1)|$false|~ssItem(esk57_0)),inference(rw,[status(thm)],[64943,583,theory(equality)])).
% cnf(64969,negated_conjecture,(memberP(app(esk55_0,X1),esk57_0)|~ssList(X1)|$false|$false),inference(rw,[status(thm)],[64968,64241,theory(equality)])).
% cnf(64970,negated_conjecture,(memberP(app(esk55_0,X1),esk57_0)|~ssList(X1)),inference(cn,[status(thm)],[64969,theory(equality)])).
% cnf(64981,negated_conjecture,(~leq(esk52_0,esk57_0)|~leq(esk57_0,esk52_0)),inference(rw,[status(thm)],[64237,64235,theory(equality)])).
% cnf(65151,negated_conjecture,(X1=cons(esk52_0,nil)|app(X1,esk56_0)!=cons(esk52_0,esk56_0)|~ssList(cons(esk52_0,nil))|~ssList(esk56_0)|~ssList(X1)),inference(spm,[status(thm)],[186,64261,theory(equality)])).
% cnf(65248,negated_conjecture,(X1=cons(esk52_0,nil)|app(X1,esk56_0)!=cons(esk52_0,esk56_0)|~ssList(cons(esk52_0,nil))|$false|~ssList(X1)),inference(rw,[status(thm)],[65151,582,theory(equality)])).
% cnf(65249,negated_conjecture,(X1=cons(esk52_0,nil)|app(X1,esk56_0)!=cons(esk52_0,esk56_0)|~ssList(cons(esk52_0,nil))|~ssList(X1)),inference(cn,[status(thm)],[65248,theory(equality)])).
% cnf(79823,negated_conjecture,(ssList(esk34_2(cons(esk52_0,esk56_0),esk56_0))|~ssList(esk56_0)|~ssList(cons(esk52_0,esk56_0))),inference(spm,[status(thm)],[370,64311,theory(equality)])).
% cnf(79824,negated_conjecture,(app(esk34_2(cons(esk52_0,esk56_0),esk56_0),esk56_0)=cons(esk52_0,esk56_0)|~ssList(esk56_0)|~ssList(cons(esk52_0,esk56_0))),inference(spm,[status(thm)],[369,64311,theory(equality)])).
% cnf(79828,negated_conjecture,(ssList(esk34_2(cons(esk52_0,esk56_0),esk56_0))|$false|~ssList(cons(esk52_0,esk56_0))),inference(rw,[status(thm)],[79823,582,theory(equality)])).
% cnf(79829,negated_conjecture,(ssList(esk34_2(cons(esk52_0,esk56_0),esk56_0))|$false|$false),inference(rw,[status(thm)],[79828,64344,theory(equality)])).
% cnf(79830,negated_conjecture,(ssList(esk34_2(cons(esk52_0,esk56_0),esk56_0))),inference(cn,[status(thm)],[79829,theory(equality)])).
% cnf(79831,negated_conjecture,(app(esk34_2(cons(esk52_0,esk56_0),esk56_0),esk56_0)=cons(esk52_0,esk56_0)|$false|~ssList(cons(esk52_0,esk56_0))),inference(rw,[status(thm)],[79824,582,theory(equality)])).
% cnf(79832,negated_conjecture,(app(esk34_2(cons(esk52_0,esk56_0),esk56_0),esk56_0)=cons(esk52_0,esk56_0)|$false|$false),inference(rw,[status(thm)],[79831,64344,theory(equality)])).
% cnf(79833,negated_conjecture,(app(esk34_2(cons(esk52_0,esk56_0),esk56_0),esk56_0)=cons(esk52_0,esk56_0)),inference(cn,[status(thm)],[79832,theory(equality)])).
% cnf(106348,negated_conjecture,(leq(esk52_0,esk57_0)|~ssItem(esk57_0)|~ssList(cons(esk52_0,esk56_0))),inference(spm,[status(thm)],[64706,64970,theory(equality)])).
% cnf(106350,negated_conjecture,(leq(esk52_0,esk57_0)|$false|~ssList(cons(esk52_0,esk56_0))),inference(rw,[status(thm)],[106348,64241,theory(equality)])).
% cnf(106351,negated_conjecture,(leq(esk52_0,esk57_0)|$false|$false),inference(rw,[status(thm)],[106350,64344,theory(equality)])).
% cnf(106352,negated_conjecture,(leq(esk52_0,esk57_0)),inference(cn,[status(thm)],[106351,theory(equality)])).
% cnf(106362,negated_conjecture,($false|~leq(esk57_0,esk52_0)),inference(rw,[status(thm)],[64981,106352,theory(equality)])).
% cnf(106363,negated_conjecture,(~leq(esk57_0,esk52_0)),inference(cn,[status(thm)],[106362,theory(equality)])).
% cnf(108905,negated_conjecture,(X1=cons(esk52_0,nil)|app(X1,esk56_0)!=cons(esk52_0,esk56_0)|~ssList(X1)|~ssList(nil)|~ssItem(esk52_0)),inference(spm,[status(thm)],[65249,121,theory(equality)])).
% cnf(108908,negated_conjecture,(X1=cons(esk52_0,nil)|app(X1,esk56_0)!=cons(esk52_0,esk56_0)|~ssList(X1)|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[108905,122,theory(equality)])).
% cnf(108909,negated_conjecture,(X1=cons(esk52_0,nil)|app(X1,esk56_0)!=cons(esk52_0,esk56_0)|~ssList(X1)|$false|$false),inference(rw,[status(thm)],[108908,586,theory(equality)])).
% cnf(108910,negated_conjecture,(X1=cons(esk52_0,nil)|app(X1,esk56_0)!=cons(esk52_0,esk56_0)|~ssList(X1)),inference(cn,[status(thm)],[108909,theory(equality)])).
% cnf(108915,negated_conjecture,(esk34_2(cons(esk52_0,esk56_0),esk56_0)=cons(esk52_0,nil)|~ssList(esk34_2(cons(esk52_0,esk56_0),esk56_0))),inference(spm,[status(thm)],[108910,79833,theory(equality)])).
% cnf(108938,negated_conjecture,(esk34_2(cons(esk52_0,esk56_0),esk56_0)=cons(esk52_0,nil)|$false),inference(rw,[status(thm)],[108915,79830,theory(equality)])).
% cnf(108939,negated_conjecture,(esk34_2(cons(esk52_0,esk56_0),esk56_0)=cons(esk52_0,nil)),inference(cn,[status(thm)],[108938,theory(equality)])).
% cnf(109381,negated_conjecture,(ssList(cons(esk52_0,nil))),inference(rw,[status(thm)],[79830,108939,theory(equality)])).
% cnf(114041,negated_conjecture,(leq(esk57_0,esk52_0)|~ssItem(esk57_0)|~ssList(app(esk54_0,cons(esk52_0,nil)))),inference(spm,[status(thm)],[64703,64967,theory(equality)])).
% cnf(114046,negated_conjecture,(leq(esk57_0,esk52_0)|$false|~ssList(app(esk54_0,cons(esk52_0,nil)))),inference(rw,[status(thm)],[114041,64241,theory(equality)])).
% cnf(114047,negated_conjecture,(leq(esk57_0,esk52_0)|~ssList(app(esk54_0,cons(esk52_0,nil)))),inference(cn,[status(thm)],[114046,theory(equality)])).
% cnf(114048,negated_conjecture,(~ssList(app(esk54_0,cons(esk52_0,nil)))),inference(sr,[status(thm)],[114047,106363,theory(equality)])).
% cnf(114049,negated_conjecture,(~ssList(cons(esk52_0,nil))|~ssList(esk54_0)),inference(spm,[status(thm)],[114048,147,theory(equality)])).
% cnf(114050,negated_conjecture,($false|~ssList(esk54_0)),inference(rw,[status(thm)],[114049,109381,theory(equality)])).
% cnf(114051,negated_conjecture,($false|$false),inference(rw,[status(thm)],[114050,584,theory(equality)])).
% cnf(114052,negated_conjecture,($false),inference(cn,[status(thm)],[114051,theory(equality)])).
% cnf(114053,negated_conjecture,($false),114052,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 5959
% # ...of these trivial : 496
% # ...subsumed : 2394
% # ...remaining for further processing: 3069
% # Other redundant clauses eliminated : 769
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 573
% # Backward-rewritten : 1057
% # Generated clauses : 39816
% # ...of the previous two non-trivial : 36898
% # Contextual simplify-reflections : 2017
% # Paramodulations : 38850
% # Factorizations : 0
% # Equation resolutions : 954
% # Current number of processed clauses: 1421
% # Positive orientable unit clauses: 286
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 26
% # Non-unit-clauses : 1109
% # Current number of unprocessed clauses: 20115
% # ...number of literals in the above : 150158
% # Clause-clause subsumption calls (NU) : 312259
% # Rec. Clause-clause subsumption calls : 238790
% # Unit Clause-clause subsumption calls : 10634
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 986
% # Indexed BW rewrite successes : 210
% # Backwards rewriting index: 1134 leaves, 1.44+/-1.215 terms/leaf
% # Paramod-from index: 462 leaves, 1.14+/-0.668 terms/leaf
% # Paramod-into index: 881 leaves, 1.34+/-1.086 terms/leaf
% # -------------------------------------------------
% # User time : 3.039 s
% # System time : 0.100 s
% # Total time : 3.139 s
% # Maximum resident set size: 0 pages
% PrfWatch: 4.95 CPU 5.80 WC
% FINAL PrfWatch: 4.95 CPU 5.80 WC
% SZS output end Solution for /tmp/SystemOnTPTP27883/SWC155+1.tptp
%
%------------------------------------------------------------------------------