%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SWC119+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 : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Thu Dec 30 07:11:05 EST 2010
% Result : Theorem 48.68s
% Output : Solution 48.68s
% 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/SystemOnTPTP31007/SWC119+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP31007/SWC119+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP31007/SWC119+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 31139
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.95 CPU 2.03 WC
% PrfWatch: 3.95 CPU 4.03 WC
% PrfWatch: 5.94 CPU 6.04 WC
% PrfWatch: 7.94 CPU 8.05 WC
% PrfWatch: 9.93 CPU 10.05 WC
% PrfWatch: 11.93 CPU 12.06 WC
% PrfWatch: 13.92 CPU 14.07 WC
% PrfWatch: 15.90 CPU 16.07 WC
% PrfWatch: 17.90 CPU 18.08 WC
% PrfWatch: 19.89 CPU 20.09 WC
% PrfWatch: 21.88 CPU 22.09 WC
% PrfWatch: 23.86 CPU 24.10 WC
% PrfWatch: 25.83 CPU 26.11 WC
% PrfWatch: 27.82 CPU 28.11 WC
% # Preprocessing time : 0.029 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 29.80 CPU 30.12 WC
% PrfWatch: 31.77 CPU 32.13 WC
% PrfWatch: 33.77 CPU 34.13 WC
% PrfWatch: 35.76 CPU 36.14 WC
% PrfWatch: 37.76 CPU 38.15 WC
% PrfWatch: 39.74 CPU 40.15 WC
% PrfWatch: 41.74 CPU 42.16 WC
% PrfWatch: 43.73 CPU 44.17 WC
% PrfWatch: 45.72 CPU 46.17 WC
% # SZS output start CNFRefutation.
% fof(3, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(neq(X1,X2)<=>~(X1=X2)))),file('/tmp/SRASS.s.p', ax15)).
% fof(4, axiom,![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>ssList(cons(X2,X1)))),file('/tmp/SRASS.s.p', ax16)).
% fof(5, axiom,ssList(nil),file('/tmp/SRASS.s.p', ax17)).
% fof(9, axiom,![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>~(nil=cons(X2,X1)))),file('/tmp/SRASS.s.p', ax21)).
% fof(10, 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(12, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>((segmentP(X1,X2)&segmentP(X2,X3))=>segmentP(X1,X3))))),file('/tmp/SRASS.s.p', ax53)).
% fof(14, axiom,![X1]:(ssList(X1)=>segmentP(X1,X1)),file('/tmp/SRASS.s.p', ax55)).
% fof(17, axiom,![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>(memberP(X1,X2)<=>?[X3]:(ssList(X3)&?[X4]:(ssList(X4)&app(X3,cons(X2,X4))=X1))))),file('/tmp/SRASS.s.p', ax3)).
% fof(18, 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)=>(segmentP(X1,X2)<=>?[X3]:(ssList(X3)&?[X4]:(ssList(X4)&app(app(X3,X2),X4)=X1))))),file('/tmp/SRASS.s.p', ax7)).
% fof(23, axiom,![X1]:(ssList(X1)=>![X2]:(ssItem(X2)=>hd(cons(X2,X1))=X2)),file('/tmp/SRASS.s.p', ax23)).
% fof(28, axiom,![X1]:(ssList(X1)=>app(nil,X1)=X1),file('/tmp/SRASS.s.p', ax28)).
% fof(30, axiom,![X1]:(ssList(X1)=>app(X1,nil)=X1),file('/tmp/SRASS.s.p', ax84)).
% fof(31, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>![X4]:(ssList(X4)=>(segmentP(X1,X2)=>segmentP(app(app(X3,X1),X4),X2)))))),file('/tmp/SRASS.s.p', ax56)).
% fof(39, axiom,![X1]:(ssList(X1)=>(~(nil=X1)=>ssList(tl(X1)))),file('/tmp/SRASS.s.p', ax24)).
% fof(41, axiom,![X1]:(ssList(X1)=>(rearsegP(nil,X1)<=>nil=X1)),file('/tmp/SRASS.s.p', ax52)).
% fof(45, axiom,![X1]:(ssList(X1)=>(~(nil=X1)=>cons(hd(X1),tl(X1))=X1)),file('/tmp/SRASS.s.p', ax78)).
% fof(48, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>ssList(app(X1,X2)))),file('/tmp/SRASS.s.p', ax26)).
% fof(63, 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(70, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>((frontsegP(X1,X2)&frontsegP(X2,X1))=>X1=X2))),file('/tmp/SRASS.s.p', ax41)).
% fof(78, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(frontsegP(X1,X2)<=>?[X3]:(ssList(X3)&app(X2,X3)=X1)))),file('/tmp/SRASS.s.p', ax5)).
% fof(79, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(~(nil=X1)=>hd(app(X1,X2))=hd(X1)))),file('/tmp/SRASS.s.p', ax85)).
% fof(88, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(frontsegP(X1,X2)=>frontsegP(app(X1,X3),X2))))),file('/tmp/SRASS.s.p', ax43)).
% fof(89, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>(rearsegP(X1,X2)=>rearsegP(app(X3,X1),X2))))),file('/tmp/SRASS.s.p', ax50)).
% fof(92, 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))|(~(nil=X3)&nil=X4))|(nil=X2&nil=X1))|(![X5]:(ssItem(X5)=>(~(cons(X5,nil)=X3)|~(memberP(X4,X5))))&neq(X4,nil)))|(neq(X1,nil)&segmentP(X2,X1))))))),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))|(~(nil=X3)&nil=X4))|(nil=X2&nil=X1))|(![X5]:(ssItem(X5)=>(~(cons(X5,nil)=X3)|~(memberP(X4,X5))))&neq(X4,nil)))|(neq(X1,nil)&segmentP(X2,X1)))))))),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))|(~(nil=X3)&nil=X4))|(nil=X2&nil=X1))|(![X5]:(ssItem(X5)=>(~(cons(X5,nil)=X3)|~(memberP(X4,X5))))&neq(X4,nil)))|(neq(X1,nil)&segmentP(X2,X1)))))))),inference(fof_simplification,[status(thm)],[97,theory(equality)])).
% fof(115, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|((~(neq(X1,X2))|~(X1=X2))&(X1=X2|neq(X1,X2))))),inference(fof_nnf,[status(thm)],[3])).
% fof(116, plain,![X3]:(~(ssList(X3))|![X4]:(~(ssList(X4))|((~(neq(X3,X4))|~(X3=X4))&(X3=X4|neq(X3,X4))))),inference(variable_rename,[status(thm)],[115])).
% fof(117, plain,![X3]:![X4]:((~(ssList(X4))|((~(neq(X3,X4))|~(X3=X4))&(X3=X4|neq(X3,X4))))|~(ssList(X3))),inference(shift_quantors,[status(thm)],[116])).
% fof(118, plain,![X3]:![X4]:((((~(neq(X3,X4))|~(X3=X4))|~(ssList(X4)))|~(ssList(X3)))&(((X3=X4|neq(X3,X4))|~(ssList(X4)))|~(ssList(X3)))),inference(distribute,[status(thm)],[117])).
% cnf(119,plain,(neq(X1,X2)|X1=X2|~ssList(X1)|~ssList(X2)),inference(split_conjunct,[status(thm)],[118])).
% fof(121, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssItem(X2))|ssList(cons(X2,X1)))),inference(fof_nnf,[status(thm)],[4])).
% fof(122, plain,![X3]:(~(ssList(X3))|![X4]:(~(ssItem(X4))|ssList(cons(X4,X3)))),inference(variable_rename,[status(thm)],[121])).
% fof(123, plain,![X3]:![X4]:((~(ssItem(X4))|ssList(cons(X4,X3)))|~(ssList(X3))),inference(shift_quantors,[status(thm)],[122])).
% cnf(124,plain,(ssList(cons(X2,X1))|~ssList(X1)|~ssItem(X2)),inference(split_conjunct,[status(thm)],[123])).
% cnf(125,plain,(ssList(nil)),inference(split_conjunct,[status(thm)],[5])).
% fof(143, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssItem(X2))|~(nil=cons(X2,X1)))),inference(fof_nnf,[status(thm)],[9])).
% fof(144, plain,![X3]:(~(ssList(X3))|![X4]:(~(ssItem(X4))|~(nil=cons(X4,X3)))),inference(variable_rename,[status(thm)],[143])).
% fof(145, plain,![X3]:![X4]:((~(ssItem(X4))|~(nil=cons(X4,X3)))|~(ssList(X3))),inference(shift_quantors,[status(thm)],[144])).
% cnf(146,plain,(~ssList(X1)|nil!=cons(X2,X1)|~ssItem(X2)),inference(split_conjunct,[status(thm)],[145])).
% fof(147, 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)],[10])).
% fof(148, 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)],[147])).
% fof(149, 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)],[148])).
% fof(150, 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)],[149])).
% cnf(152,plain,(memberP(cons(X2,X3),X1)|~ssItem(X1)|~ssItem(X2)|~ssList(X3)|X1!=X2),inference(split_conjunct,[status(thm)],[150])).
% fof(157, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|![X3]:(~(ssList(X3))|((~(segmentP(X1,X2))|~(segmentP(X2,X3)))|segmentP(X1,X3))))),inference(fof_nnf,[status(thm)],[12])).
% fof(158, plain,![X4]:(~(ssList(X4))|![X5]:(~(ssList(X5))|![X6]:(~(ssList(X6))|((~(segmentP(X4,X5))|~(segmentP(X5,X6)))|segmentP(X4,X6))))),inference(variable_rename,[status(thm)],[157])).
% fof(159, plain,![X4]:![X5]:![X6]:(((~(ssList(X6))|((~(segmentP(X4,X5))|~(segmentP(X5,X6)))|segmentP(X4,X6)))|~(ssList(X5)))|~(ssList(X4))),inference(shift_quantors,[status(thm)],[158])).
% cnf(160,plain,(segmentP(X1,X3)|~ssList(X1)|~ssList(X2)|~segmentP(X2,X3)|~segmentP(X1,X2)|~ssList(X3)),inference(split_conjunct,[status(thm)],[159])).
% fof(165, plain,![X1]:(~(ssList(X1))|segmentP(X1,X1)),inference(fof_nnf,[status(thm)],[14])).
% fof(166, plain,![X2]:(~(ssList(X2))|segmentP(X2,X2)),inference(variable_rename,[status(thm)],[165])).
% cnf(167,plain,(segmentP(X1,X1)|~ssList(X1)),inference(split_conjunct,[status(thm)],[166])).
% fof(176, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssItem(X2))|((~(memberP(X1,X2))|?[X3]:(ssList(X3)&?[X4]:(ssList(X4)&app(X3,cons(X2,X4))=X1)))&(![X3]:(~(ssList(X3))|![X4]:(~(ssList(X4))|~(app(X3,cons(X2,X4))=X1)))|memberP(X1,X2))))),inference(fof_nnf,[status(thm)],[17])).
% fof(177, plain,![X5]:(~(ssList(X5))|![X6]:(~(ssItem(X6))|((~(memberP(X5,X6))|?[X7]:(ssList(X7)&?[X8]:(ssList(X8)&app(X7,cons(X6,X8))=X5)))&(![X9]:(~(ssList(X9))|![X10]:(~(ssList(X10))|~(app(X9,cons(X6,X10))=X5)))|memberP(X5,X6))))),inference(variable_rename,[status(thm)],[176])).
% fof(178, plain,![X5]:(~(ssList(X5))|![X6]:(~(ssItem(X6))|((~(memberP(X5,X6))|(ssList(esk5_2(X5,X6))&(ssList(esk6_2(X5,X6))&app(esk5_2(X5,X6),cons(X6,esk6_2(X5,X6)))=X5)))&(![X9]:(~(ssList(X9))|![X10]:(~(ssList(X10))|~(app(X9,cons(X6,X10))=X5)))|memberP(X5,X6))))),inference(skolemize,[status(esa)],[177])).
% fof(179, plain,![X5]:![X6]:![X9]:![X10]:((((((~(ssList(X10))|~(app(X9,cons(X6,X10))=X5))|~(ssList(X9)))|memberP(X5,X6))&(~(memberP(X5,X6))|(ssList(esk5_2(X5,X6))&(ssList(esk6_2(X5,X6))&app(esk5_2(X5,X6),cons(X6,esk6_2(X5,X6)))=X5))))|~(ssItem(X6)))|~(ssList(X5))),inference(shift_quantors,[status(thm)],[178])).
% fof(180, plain,![X5]:![X6]:![X9]:![X10]:((((((~(ssList(X10))|~(app(X9,cons(X6,X10))=X5))|~(ssList(X9)))|memberP(X5,X6))|~(ssItem(X6)))|~(ssList(X5)))&((((ssList(esk5_2(X5,X6))|~(memberP(X5,X6)))|~(ssItem(X6)))|~(ssList(X5)))&((((ssList(esk6_2(X5,X6))|~(memberP(X5,X6)))|~(ssItem(X6)))|~(ssList(X5)))&(((app(esk5_2(X5,X6),cons(X6,esk6_2(X5,X6)))=X5|~(memberP(X5,X6)))|~(ssItem(X6)))|~(ssList(X5)))))),inference(distribute,[status(thm)],[179])).
% cnf(181,plain,(app(esk5_2(X1,X2),cons(X2,esk6_2(X1,X2)))=X1|~ssList(X1)|~ssItem(X2)|~memberP(X1,X2)),inference(split_conjunct,[status(thm)],[180])).
% cnf(182,plain,(ssList(esk6_2(X1,X2))|~ssList(X1)|~ssItem(X2)|~memberP(X1,X2)),inference(split_conjunct,[status(thm)],[180])).
% cnf(183,plain,(ssList(esk5_2(X1,X2))|~ssList(X1)|~ssItem(X2)|~memberP(X1,X2)),inference(split_conjunct,[status(thm)],[180])).
% fof(185, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssItem(X2))|cons(X2,X1)=app(cons(X2,nil),X1))),inference(fof_nnf,[status(thm)],[18])).
% fof(186, plain,![X3]:(~(ssList(X3))|![X4]:(~(ssItem(X4))|cons(X4,X3)=app(cons(X4,nil),X3))),inference(variable_rename,[status(thm)],[185])).
% fof(187, plain,![X3]:![X4]:((~(ssItem(X4))|cons(X4,X3)=app(cons(X4,nil),X3))|~(ssList(X3))),inference(shift_quantors,[status(thm)],[186])).
% cnf(188,plain,(cons(X2,X1)=app(cons(X2,nil),X1)|~ssList(X1)|~ssItem(X2)),inference(split_conjunct,[status(thm)],[187])).
% fof(201, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|((~(segmentP(X1,X2))|?[X3]:(ssList(X3)&?[X4]:(ssList(X4)&app(app(X3,X2),X4)=X1)))&(![X3]:(~(ssList(X3))|![X4]:(~(ssList(X4))|~(app(app(X3,X2),X4)=X1)))|segmentP(X1,X2))))),inference(fof_nnf,[status(thm)],[21])).
% fof(202, plain,![X5]:(~(ssList(X5))|![X6]:(~(ssList(X6))|((~(segmentP(X5,X6))|?[X7]:(ssList(X7)&?[X8]:(ssList(X8)&app(app(X7,X6),X8)=X5)))&(![X9]:(~(ssList(X9))|![X10]:(~(ssList(X10))|~(app(app(X9,X6),X10)=X5)))|segmentP(X5,X6))))),inference(variable_rename,[status(thm)],[201])).
% fof(203, plain,![X5]:(~(ssList(X5))|![X6]:(~(ssList(X6))|((~(segmentP(X5,X6))|(ssList(esk8_2(X5,X6))&(ssList(esk9_2(X5,X6))&app(app(esk8_2(X5,X6),X6),esk9_2(X5,X6))=X5)))&(![X9]:(~(ssList(X9))|![X10]:(~(ssList(X10))|~(app(app(X9,X6),X10)=X5)))|segmentP(X5,X6))))),inference(skolemize,[status(esa)],[202])).
% fof(204, plain,![X5]:![X6]:![X9]:![X10]:((((((~(ssList(X10))|~(app(app(X9,X6),X10)=X5))|~(ssList(X9)))|segmentP(X5,X6))&(~(segmentP(X5,X6))|(ssList(esk8_2(X5,X6))&(ssList(esk9_2(X5,X6))&app(app(esk8_2(X5,X6),X6),esk9_2(X5,X6))=X5))))|~(ssList(X6)))|~(ssList(X5))),inference(shift_quantors,[status(thm)],[203])).
% fof(205, plain,![X5]:![X6]:![X9]:![X10]:((((((~(ssList(X10))|~(app(app(X9,X6),X10)=X5))|~(ssList(X9)))|segmentP(X5,X6))|~(ssList(X6)))|~(ssList(X5)))&((((ssList(esk8_2(X5,X6))|~(segmentP(X5,X6)))|~(ssList(X6)))|~(ssList(X5)))&((((ssList(esk9_2(X5,X6))|~(segmentP(X5,X6)))|~(ssList(X6)))|~(ssList(X5)))&(((app(app(esk8_2(X5,X6),X6),esk9_2(X5,X6))=X5|~(segmentP(X5,X6)))|~(ssList(X6)))|~(ssList(X5)))))),inference(distribute,[status(thm)],[204])).
% cnf(209,plain,(segmentP(X1,X2)|~ssList(X1)|~ssList(X2)|~ssList(X3)|app(app(X3,X2),X4)!=X1|~ssList(X4)),inference(split_conjunct,[status(thm)],[205])).
% fof(217, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssItem(X2))|hd(cons(X2,X1))=X2)),inference(fof_nnf,[status(thm)],[23])).
% fof(218, plain,![X3]:(~(ssList(X3))|![X4]:(~(ssItem(X4))|hd(cons(X4,X3))=X4)),inference(variable_rename,[status(thm)],[217])).
% fof(219, plain,![X3]:![X4]:((~(ssItem(X4))|hd(cons(X4,X3))=X4)|~(ssList(X3))),inference(shift_quantors,[status(thm)],[218])).
% cnf(220,plain,(hd(cons(X2,X1))=X2|~ssList(X1)|~ssItem(X2)),inference(split_conjunct,[status(thm)],[219])).
% fof(241, plain,![X1]:(~(ssList(X1))|app(nil,X1)=X1),inference(fof_nnf,[status(thm)],[28])).
% fof(242, plain,![X2]:(~(ssList(X2))|app(nil,X2)=X2),inference(variable_rename,[status(thm)],[241])).
% cnf(243,plain,(app(nil,X1)=X1|~ssList(X1)),inference(split_conjunct,[status(thm)],[242])).
% fof(251, plain,![X1]:(~(ssList(X1))|app(X1,nil)=X1),inference(fof_nnf,[status(thm)],[30])).
% fof(252, plain,![X2]:(~(ssList(X2))|app(X2,nil)=X2),inference(variable_rename,[status(thm)],[251])).
% cnf(253,plain,(app(X1,nil)=X1|~ssList(X1)),inference(split_conjunct,[status(thm)],[252])).
% fof(254, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|![X3]:(~(ssList(X3))|![X4]:(~(ssList(X4))|(~(segmentP(X1,X2))|segmentP(app(app(X3,X1),X4),X2)))))),inference(fof_nnf,[status(thm)],[31])).
% fof(255, plain,![X5]:(~(ssList(X5))|![X6]:(~(ssList(X6))|![X7]:(~(ssList(X7))|![X8]:(~(ssList(X8))|(~(segmentP(X5,X6))|segmentP(app(app(X7,X5),X8),X6)))))),inference(variable_rename,[status(thm)],[254])).
% fof(256, plain,![X5]:![X6]:![X7]:![X8]:((((~(ssList(X8))|(~(segmentP(X5,X6))|segmentP(app(app(X7,X5),X8),X6)))|~(ssList(X7)))|~(ssList(X6)))|~(ssList(X5))),inference(shift_quantors,[status(thm)],[255])).
% cnf(257,plain,(segmentP(app(app(X3,X1),X4),X2)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~segmentP(X1,X2)|~ssList(X4)),inference(split_conjunct,[status(thm)],[256])).
% fof(279, plain,![X1]:(~(ssList(X1))|(nil=X1|ssList(tl(X1)))),inference(fof_nnf,[status(thm)],[39])).
% fof(280, plain,![X2]:(~(ssList(X2))|(nil=X2|ssList(tl(X2)))),inference(variable_rename,[status(thm)],[279])).
% cnf(281,plain,(ssList(tl(X1))|nil=X1|~ssList(X1)),inference(split_conjunct,[status(thm)],[280])).
% fof(287, plain,![X1]:(~(ssList(X1))|((~(rearsegP(nil,X1))|nil=X1)&(~(nil=X1)|rearsegP(nil,X1)))),inference(fof_nnf,[status(thm)],[41])).
% fof(288, plain,![X2]:(~(ssList(X2))|((~(rearsegP(nil,X2))|nil=X2)&(~(nil=X2)|rearsegP(nil,X2)))),inference(variable_rename,[status(thm)],[287])).
% fof(289, plain,![X2]:(((~(rearsegP(nil,X2))|nil=X2)|~(ssList(X2)))&((~(nil=X2)|rearsegP(nil,X2))|~(ssList(X2)))),inference(distribute,[status(thm)],[288])).
% cnf(290,plain,(rearsegP(nil,X1)|~ssList(X1)|nil!=X1),inference(split_conjunct,[status(thm)],[289])).
% fof(323, plain,![X1]:(~(ssList(X1))|(nil=X1|cons(hd(X1),tl(X1))=X1)),inference(fof_nnf,[status(thm)],[45])).
% fof(324, plain,![X2]:(~(ssList(X2))|(nil=X2|cons(hd(X2),tl(X2))=X2)),inference(variable_rename,[status(thm)],[323])).
% cnf(325,plain,(cons(hd(X1),tl(X1))=X1|nil=X1|~ssList(X1)),inference(split_conjunct,[status(thm)],[324])).
% fof(333, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|ssList(app(X1,X2)))),inference(fof_nnf,[status(thm)],[48])).
% fof(334, plain,![X3]:(~(ssList(X3))|![X4]:(~(ssList(X4))|ssList(app(X3,X4)))),inference(variable_rename,[status(thm)],[333])).
% fof(335, plain,![X3]:![X4]:((~(ssList(X4))|ssList(app(X3,X4)))|~(ssList(X3))),inference(shift_quantors,[status(thm)],[334])).
% cnf(336,plain,(ssList(app(X1,X2))|~ssList(X1)|~ssList(X2)),inference(split_conjunct,[status(thm)],[335])).
% fof(366, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|![X3]:(~(ssList(X3))|(~(app(X2,X3)=app(X2,X1))|X3=X1)))),inference(fof_nnf,[status(thm)],[63])).
% fof(367, plain,![X4]:(~(ssList(X4))|![X5]:(~(ssList(X5))|![X6]:(~(ssList(X6))|(~(app(X5,X6)=app(X5,X4))|X6=X4)))),inference(variable_rename,[status(thm)],[366])).
% fof(368, plain,![X4]:![X5]:![X6]:(((~(ssList(X6))|(~(app(X5,X6)=app(X5,X4))|X6=X4))|~(ssList(X5)))|~(ssList(X4))),inference(shift_quantors,[status(thm)],[367])).
% cnf(369,plain,(X3=X1|~ssList(X1)|~ssList(X2)|app(X2,X3)!=app(X2,X1)|~ssList(X3)),inference(split_conjunct,[status(thm)],[368])).
% fof(403, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|((~(frontsegP(X1,X2))|~(frontsegP(X2,X1)))|X1=X2))),inference(fof_nnf,[status(thm)],[70])).
% fof(404, plain,![X3]:(~(ssList(X3))|![X4]:(~(ssList(X4))|((~(frontsegP(X3,X4))|~(frontsegP(X4,X3)))|X3=X4))),inference(variable_rename,[status(thm)],[403])).
% fof(405, plain,![X3]:![X4]:((~(ssList(X4))|((~(frontsegP(X3,X4))|~(frontsegP(X4,X3)))|X3=X4))|~(ssList(X3))),inference(shift_quantors,[status(thm)],[404])).
% cnf(406,plain,(X1=X2|~ssList(X1)|~frontsegP(X2,X1)|~frontsegP(X1,X2)|~ssList(X2)),inference(split_conjunct,[status(thm)],[405])).
% fof(483, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|((~(frontsegP(X1,X2))|?[X3]:(ssList(X3)&app(X2,X3)=X1))&(![X3]:(~(ssList(X3))|~(app(X2,X3)=X1))|frontsegP(X1,X2))))),inference(fof_nnf,[status(thm)],[78])).
% fof(484, plain,![X4]:(~(ssList(X4))|![X5]:(~(ssList(X5))|((~(frontsegP(X4,X5))|?[X6]:(ssList(X6)&app(X5,X6)=X4))&(![X7]:(~(ssList(X7))|~(app(X5,X7)=X4))|frontsegP(X4,X5))))),inference(variable_rename,[status(thm)],[483])).
% fof(485, plain,![X4]:(~(ssList(X4))|![X5]:(~(ssList(X5))|((~(frontsegP(X4,X5))|(ssList(esk46_2(X4,X5))&app(X5,esk46_2(X4,X5))=X4))&(![X7]:(~(ssList(X7))|~(app(X5,X7)=X4))|frontsegP(X4,X5))))),inference(skolemize,[status(esa)],[484])).
% fof(486, plain,![X4]:![X5]:![X7]:(((((~(ssList(X7))|~(app(X5,X7)=X4))|frontsegP(X4,X5))&(~(frontsegP(X4,X5))|(ssList(esk46_2(X4,X5))&app(X5,esk46_2(X4,X5))=X4)))|~(ssList(X5)))|~(ssList(X4))),inference(shift_quantors,[status(thm)],[485])).
% fof(487, plain,![X4]:![X5]:![X7]:(((((~(ssList(X7))|~(app(X5,X7)=X4))|frontsegP(X4,X5))|~(ssList(X5)))|~(ssList(X4)))&((((ssList(esk46_2(X4,X5))|~(frontsegP(X4,X5)))|~(ssList(X5)))|~(ssList(X4)))&(((app(X5,esk46_2(X4,X5))=X4|~(frontsegP(X4,X5)))|~(ssList(X5)))|~(ssList(X4))))),inference(distribute,[status(thm)],[486])).
% cnf(488,plain,(app(X2,esk46_2(X1,X2))=X1|~ssList(X1)|~ssList(X2)|~frontsegP(X1,X2)),inference(split_conjunct,[status(thm)],[487])).
% cnf(489,plain,(ssList(esk46_2(X1,X2))|~ssList(X1)|~ssList(X2)|~frontsegP(X1,X2)),inference(split_conjunct,[status(thm)],[487])).
% cnf(490,plain,(frontsegP(X1,X2)|~ssList(X1)|~ssList(X2)|app(X2,X3)!=X1|~ssList(X3)),inference(split_conjunct,[status(thm)],[487])).
% fof(491, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|(nil=X1|hd(app(X1,X2))=hd(X1)))),inference(fof_nnf,[status(thm)],[79])).
% fof(492, plain,![X3]:(~(ssList(X3))|![X4]:(~(ssList(X4))|(nil=X3|hd(app(X3,X4))=hd(X3)))),inference(variable_rename,[status(thm)],[491])).
% fof(493, plain,![X3]:![X4]:((~(ssList(X4))|(nil=X3|hd(app(X3,X4))=hd(X3)))|~(ssList(X3))),inference(shift_quantors,[status(thm)],[492])).
% cnf(494,plain,(hd(app(X1,X2))=hd(X1)|nil=X1|~ssList(X1)|~ssList(X2)),inference(split_conjunct,[status(thm)],[493])).
% fof(528, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|![X3]:(~(ssList(X3))|(~(frontsegP(X1,X2))|frontsegP(app(X1,X3),X2))))),inference(fof_nnf,[status(thm)],[88])).
% fof(529, plain,![X4]:(~(ssList(X4))|![X5]:(~(ssList(X5))|![X6]:(~(ssList(X6))|(~(frontsegP(X4,X5))|frontsegP(app(X4,X6),X5))))),inference(variable_rename,[status(thm)],[528])).
% fof(530, plain,![X4]:![X5]:![X6]:(((~(ssList(X6))|(~(frontsegP(X4,X5))|frontsegP(app(X4,X6),X5)))|~(ssList(X5)))|~(ssList(X4))),inference(shift_quantors,[status(thm)],[529])).
% cnf(531,plain,(frontsegP(app(X1,X3),X2)|~ssList(X1)|~ssList(X2)|~frontsegP(X1,X2)|~ssList(X3)),inference(split_conjunct,[status(thm)],[530])).
% fof(532, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|![X3]:(~(ssList(X3))|(~(rearsegP(X1,X2))|rearsegP(app(X3,X1),X2))))),inference(fof_nnf,[status(thm)],[89])).
% fof(533, plain,![X4]:(~(ssList(X4))|![X5]:(~(ssList(X5))|![X6]:(~(ssList(X6))|(~(rearsegP(X4,X5))|rearsegP(app(X6,X4),X5))))),inference(variable_rename,[status(thm)],[532])).
% fof(534, plain,![X4]:![X5]:![X6]:(((~(ssList(X6))|(~(rearsegP(X4,X5))|rearsegP(app(X6,X4),X5)))|~(ssList(X5)))|~(ssList(X4))),inference(shift_quantors,[status(thm)],[533])).
% cnf(535,plain,(rearsegP(app(X3,X1),X2)|~ssList(X1)|~ssList(X2)|~rearsegP(X1,X2)|~ssList(X3)),inference(split_conjunct,[status(thm)],[534])).
% fof(544, 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)],[92])).
% fof(545, 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)],[544])).
% fof(546, plain,![X4]:(~(ssList(X4))|![X5]:(~(ssList(X5))|((~(rearsegP(X4,X5))|(ssList(esk47_2(X4,X5))&app(esk47_2(X4,X5),X5)=X4))&(![X7]:(~(ssList(X7))|~(app(X7,X5)=X4))|rearsegP(X4,X5))))),inference(skolemize,[status(esa)],[545])).
% fof(547, plain,![X4]:![X5]:![X7]:(((((~(ssList(X7))|~(app(X7,X5)=X4))|rearsegP(X4,X5))&(~(rearsegP(X4,X5))|(ssList(esk47_2(X4,X5))&app(esk47_2(X4,X5),X5)=X4)))|~(ssList(X5)))|~(ssList(X4))),inference(shift_quantors,[status(thm)],[546])).
% fof(548, plain,![X4]:![X5]:![X7]:(((((~(ssList(X7))|~(app(X7,X5)=X4))|rearsegP(X4,X5))|~(ssList(X5)))|~(ssList(X4)))&((((ssList(esk47_2(X4,X5))|~(rearsegP(X4,X5)))|~(ssList(X5)))|~(ssList(X4)))&(((app(esk47_2(X4,X5),X5)=X4|~(rearsegP(X4,X5)))|~(ssList(X5)))|~(ssList(X4))))),inference(distribute,[status(thm)],[547])).
% cnf(549,plain,(app(esk47_2(X1,X2),X2)=X1|~ssList(X1)|~ssList(X2)|~rearsegP(X1,X2)),inference(split_conjunct,[status(thm)],[548])).
% cnf(550,plain,(ssList(esk47_2(X1,X2))|~ssList(X1)|~ssList(X2)|~rearsegP(X1,X2)),inference(split_conjunct,[status(thm)],[548])).
% cnf(551,plain,(rearsegP(X1,X2)|~ssList(X1)|~ssList(X2)|app(X3,X2)!=X1|~ssList(X3)),inference(split_conjunct,[status(thm)],[548])).
% fof(568, negated_conjecture,?[X1]:(ssList(X1)&?[X2]:(ssList(X2)&?[X3]:(ssList(X3)&?[X4]:(ssList(X4)&(((((X2=X4&X1=X3)&(nil=X3|~(nil=X4)))&(~(nil=X2)|~(nil=X1)))&(?[X5]:(ssItem(X5)&(cons(X5,nil)=X3&memberP(X4,X5)))|~(neq(X4,nil))))&(~(neq(X1,nil))|~(segmentP(X2,X1)))))))),inference(fof_nnf,[status(thm)],[103])).
% fof(569, negated_conjecture,?[X6]:(ssList(X6)&?[X7]:(ssList(X7)&?[X8]:(ssList(X8)&?[X9]:(ssList(X9)&(((((X7=X9&X6=X8)&(nil=X8|~(nil=X9)))&(~(nil=X7)|~(nil=X6)))&(?[X10]:(ssItem(X10)&(cons(X10,nil)=X8&memberP(X9,X10)))|~(neq(X9,nil))))&(~(neq(X6,nil))|~(segmentP(X7,X6)))))))),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)&(nil=esk50_0|~(nil=esk51_0)))&(~(nil=esk49_0)|~(nil=esk48_0)))&((ssItem(esk52_0)&(cons(esk52_0,nil)=esk50_0&memberP(esk51_0,esk52_0)))|~(neq(esk51_0,nil))))&(~(neq(esk48_0,nil))|~(segmentP(esk49_0,esk48_0)))))))),inference(skolemize,[status(esa)],[569])).
% fof(571, negated_conjecture,(ssList(esk48_0)&(ssList(esk49_0)&(ssList(esk50_0)&(ssList(esk51_0)&(((((esk49_0=esk51_0&esk48_0=esk50_0)&(nil=esk50_0|~(nil=esk51_0)))&(~(nil=esk49_0)|~(nil=esk48_0)))&((ssItem(esk52_0)|~(neq(esk51_0,nil)))&((cons(esk52_0,nil)=esk50_0|~(neq(esk51_0,nil)))&(memberP(esk51_0,esk52_0)|~(neq(esk51_0,nil))))))&(~(neq(esk48_0,nil))|~(segmentP(esk49_0,esk48_0)))))))),inference(distribute,[status(thm)],[570])).
% cnf(572,negated_conjecture,(~segmentP(esk49_0,esk48_0)|~neq(esk48_0,nil)),inference(split_conjunct,[status(thm)],[571])).
% cnf(573,negated_conjecture,(memberP(esk51_0,esk52_0)|~neq(esk51_0,nil)),inference(split_conjunct,[status(thm)],[571])).
% cnf(574,negated_conjecture,(cons(esk52_0,nil)=esk50_0|~neq(esk51_0,nil)),inference(split_conjunct,[status(thm)],[571])).
% cnf(575,negated_conjecture,(ssItem(esk52_0)|~neq(esk51_0,nil)),inference(split_conjunct,[status(thm)],[571])).
% cnf(576,negated_conjecture,(nil!=esk48_0|nil!=esk49_0),inference(split_conjunct,[status(thm)],[571])).
% cnf(577,negated_conjecture,(nil=esk50_0|nil!=esk51_0),inference(split_conjunct,[status(thm)],[571])).
% cnf(578,negated_conjecture,(esk48_0=esk50_0),inference(split_conjunct,[status(thm)],[571])).
% cnf(579,negated_conjecture,(esk49_0=esk51_0),inference(split_conjunct,[status(thm)],[571])).
% cnf(582,negated_conjecture,(ssList(esk49_0)),inference(split_conjunct,[status(thm)],[571])).
% cnf(583,negated_conjecture,(ssList(esk48_0)),inference(split_conjunct,[status(thm)],[571])).
% cnf(584,negated_conjecture,(esk48_0!=nil|esk51_0!=nil),inference(rw,[status(thm)],[576,579,theory(equality)])).
% cnf(585,negated_conjecture,(ssList(esk51_0)),inference(rw,[status(thm)],[582,579,theory(equality)])).
% cnf(588,negated_conjecture,(esk48_0=nil|esk51_0!=nil),inference(rw,[status(thm)],[577,578,theory(equality)])).
% cnf(589,negated_conjecture,(esk51_0!=nil),inference(csr,[status(thm)],[588,584])).
% cnf(590,negated_conjecture,(~neq(esk48_0,nil)|~segmentP(esk51_0,esk48_0)),inference(rw,[status(thm)],[572,579,theory(equality)])).
% cnf(591,negated_conjecture,(cons(esk52_0,nil)=esk48_0|~neq(esk51_0,nil)),inference(rw,[status(thm)],[574,578,theory(equality)])).
% cnf(598,plain,(rearsegP(nil,nil)|~ssList(nil)),inference(er,[status(thm)],[290,theory(equality)])).
% cnf(599,plain,(rearsegP(nil,nil)|$false),inference(rw,[status(thm)],[598,125,theory(equality)])).
% cnf(600,plain,(rearsegP(nil,nil)),inference(cn,[status(thm)],[599,theory(equality)])).
% cnf(658,negated_conjecture,(ssItem(esk52_0)|esk51_0=nil|~ssList(nil)|~ssList(esk51_0)),inference(spm,[status(thm)],[575,119,theory(equality)])).
% cnf(659,negated_conjecture,(cons(esk52_0,nil)=esk48_0|esk51_0=nil|~ssList(nil)|~ssList(esk51_0)),inference(spm,[status(thm)],[591,119,theory(equality)])).
% cnf(660,negated_conjecture,(memberP(esk51_0,esk52_0)|esk51_0=nil|~ssList(nil)|~ssList(esk51_0)),inference(spm,[status(thm)],[573,119,theory(equality)])).
% cnf(661,negated_conjecture,(ssItem(esk52_0)|esk51_0=nil|$false|~ssList(esk51_0)),inference(rw,[status(thm)],[658,125,theory(equality)])).
% cnf(662,negated_conjecture,(ssItem(esk52_0)|esk51_0=nil|$false|$false),inference(rw,[status(thm)],[661,585,theory(equality)])).
% cnf(663,negated_conjecture,(ssItem(esk52_0)|esk51_0=nil),inference(cn,[status(thm)],[662,theory(equality)])).
% cnf(664,negated_conjecture,(ssItem(esk52_0)),inference(sr,[status(thm)],[663,589,theory(equality)])).
% cnf(665,negated_conjecture,(cons(esk52_0,nil)=esk48_0|esk51_0=nil|$false|~ssList(esk51_0)),inference(rw,[status(thm)],[659,125,theory(equality)])).
% cnf(666,negated_conjecture,(cons(esk52_0,nil)=esk48_0|esk51_0=nil|$false|$false),inference(rw,[status(thm)],[665,585,theory(equality)])).
% cnf(667,negated_conjecture,(cons(esk52_0,nil)=esk48_0|esk51_0=nil),inference(cn,[status(thm)],[666,theory(equality)])).
% cnf(668,negated_conjecture,(cons(esk52_0,nil)=esk48_0),inference(sr,[status(thm)],[667,589,theory(equality)])).
% cnf(669,negated_conjecture,(memberP(esk51_0,esk52_0)|esk51_0=nil|$false|~ssList(esk51_0)),inference(rw,[status(thm)],[660,125,theory(equality)])).
% cnf(670,negated_conjecture,(memberP(esk51_0,esk52_0)|esk51_0=nil|$false|$false),inference(rw,[status(thm)],[669,585,theory(equality)])).
% cnf(671,negated_conjecture,(memberP(esk51_0,esk52_0)|esk51_0=nil),inference(cn,[status(thm)],[670,theory(equality)])).
% cnf(672,negated_conjecture,(memberP(esk51_0,esk52_0)),inference(sr,[status(thm)],[671,589,theory(equality)])).
% cnf(715,plain,(memberP(cons(X1,X2),X1)|~ssList(X2)|~ssItem(X1)),inference(er,[status(thm)],[152,theory(equality)])).
% cnf(752,plain,(frontsegP(app(X1,X2),X1)|~ssList(X2)|~ssList(X1)|~ssList(app(X1,X2))),inference(er,[status(thm)],[490,theory(equality)])).
% cnf(762,plain,(rearsegP(app(X1,X2),X2)|~ssList(X1)|~ssList(X2)|~ssList(app(X1,X2))),inference(er,[status(thm)],[551,theory(equality)])).
% cnf(845,plain,(segmentP(X1,X2)|app(X3,X2)!=X1|~ssList(nil)|~ssList(X3)|~ssList(X2)|~ssList(X1)|~ssList(app(X3,X2))),inference(spm,[status(thm)],[209,253,theory(equality)])).
% cnf(850,plain,(segmentP(X1,X2)|app(X3,X2)!=X1|$false|~ssList(X3)|~ssList(X2)|~ssList(X1)|~ssList(app(X3,X2))),inference(rw,[status(thm)],[845,125,theory(equality)])).
% cnf(851,plain,(segmentP(X1,X2)|app(X3,X2)!=X1|~ssList(X3)|~ssList(X2)|~ssList(X1)|~ssList(app(X3,X2))),inference(cn,[status(thm)],[850,theory(equality)])).
% cnf(940,plain,(segmentP(app(app(X1,X2),X3),X2)|~ssList(X3)|~ssList(X1)|~ssList(X2)),inference(spm,[status(thm)],[257,167,theory(equality)])).
% cnf(1336,negated_conjecture,(esk48_0!=nil|~ssList(nil)|~ssItem(esk52_0)),inference(spm,[status(thm)],[146,668,theory(equality)])).
% cnf(1339,negated_conjecture,(hd(esk48_0)=esk52_0|~ssList(nil)|~ssItem(esk52_0)),inference(spm,[status(thm)],[220,668,theory(equality)])).
% cnf(1370,negated_conjecture,(app(esk48_0,X1)=cons(esk52_0,X1)|~ssList(X1)|~ssItem(esk52_0)),inference(spm,[status(thm)],[188,668,theory(equality)])).
% cnf(1373,negated_conjecture,(esk48_0!=nil|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[1336,125,theory(equality)])).
% cnf(1374,negated_conjecture,(esk48_0!=nil|$false|$false),inference(rw,[status(thm)],[1373,664,theory(equality)])).
% cnf(1375,negated_conjecture,(esk48_0!=nil),inference(cn,[status(thm)],[1374,theory(equality)])).
% cnf(1383,negated_conjecture,(hd(esk48_0)=esk52_0|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[1339,125,theory(equality)])).
% cnf(1384,negated_conjecture,(hd(esk48_0)=esk52_0|$false|$false),inference(rw,[status(thm)],[1383,664,theory(equality)])).
% cnf(1385,negated_conjecture,(hd(esk48_0)=esk52_0),inference(cn,[status(thm)],[1384,theory(equality)])).
% cnf(1469,negated_conjecture,(app(esk48_0,X1)=cons(esk52_0,X1)|~ssList(X1)|$false),inference(rw,[status(thm)],[1370,664,theory(equality)])).
% cnf(1470,negated_conjecture,(app(esk48_0,X1)=cons(esk52_0,X1)|~ssList(X1)),inference(cn,[status(thm)],[1469,theory(equality)])).
% cnf(1473,negated_conjecture,(ssList(esk5_2(esk51_0,esk52_0))|~ssList(esk51_0)|~ssItem(esk52_0)),inference(spm,[status(thm)],[183,672,theory(equality)])).
% cnf(1474,negated_conjecture,(ssList(esk6_2(esk51_0,esk52_0))|~ssList(esk51_0)|~ssItem(esk52_0)),inference(spm,[status(thm)],[182,672,theory(equality)])).
% cnf(1475,negated_conjecture,(app(esk5_2(esk51_0,esk52_0),cons(esk52_0,esk6_2(esk51_0,esk52_0)))=esk51_0|~ssList(esk51_0)|~ssItem(esk52_0)),inference(spm,[status(thm)],[181,672,theory(equality)])).
% cnf(1480,negated_conjecture,(ssList(esk5_2(esk51_0,esk52_0))|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[1473,585,theory(equality)])).
% cnf(1481,negated_conjecture,(ssList(esk5_2(esk51_0,esk52_0))|$false|$false),inference(rw,[status(thm)],[1480,664,theory(equality)])).
% cnf(1482,negated_conjecture,(ssList(esk5_2(esk51_0,esk52_0))),inference(cn,[status(thm)],[1481,theory(equality)])).
% cnf(1483,negated_conjecture,(ssList(esk6_2(esk51_0,esk52_0))|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[1474,585,theory(equality)])).
% cnf(1484,negated_conjecture,(ssList(esk6_2(esk51_0,esk52_0))|$false|$false),inference(rw,[status(thm)],[1483,664,theory(equality)])).
% cnf(1485,negated_conjecture,(ssList(esk6_2(esk51_0,esk52_0))),inference(cn,[status(thm)],[1484,theory(equality)])).
% cnf(1486,negated_conjecture,(app(esk5_2(esk51_0,esk52_0),cons(esk52_0,esk6_2(esk51_0,esk52_0)))=esk51_0|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[1475,585,theory(equality)])).
% cnf(1487,negated_conjecture,(app(esk5_2(esk51_0,esk52_0),cons(esk52_0,esk6_2(esk51_0,esk52_0)))=esk51_0|$false|$false),inference(rw,[status(thm)],[1486,664,theory(equality)])).
% cnf(1488,negated_conjecture,(app(esk5_2(esk51_0,esk52_0),cons(esk52_0,esk6_2(esk51_0,esk52_0)))=esk51_0),inference(cn,[status(thm)],[1487,theory(equality)])).
% cnf(1512,plain,(rearsegP(app(X1,nil),nil)|~ssList(X1)|~ssList(nil)),inference(spm,[status(thm)],[535,600,theory(equality)])).
% cnf(1518,plain,(rearsegP(app(X1,nil),nil)|~ssList(X1)|$false),inference(rw,[status(thm)],[1512,125,theory(equality)])).
% cnf(1519,plain,(rearsegP(app(X1,nil),nil)|~ssList(X1)),inference(cn,[status(thm)],[1518,theory(equality)])).
% cnf(1995,negated_conjecture,(ssList(cons(esk52_0,X1))|~ssList(X1)|~ssList(esk48_0)),inference(spm,[status(thm)],[336,1470,theory(equality)])).
% cnf(2036,negated_conjecture,(ssList(cons(esk52_0,X1))|~ssList(X1)|$false),inference(rw,[status(thm)],[1995,583,theory(equality)])).
% cnf(2037,negated_conjecture,(ssList(cons(esk52_0,X1))|~ssList(X1)),inference(cn,[status(thm)],[2036,theory(equality)])).
% cnf(2841,negated_conjecture,(rearsegP(cons(esk52_0,nil),nil)|~ssList(esk48_0)|~ssList(nil)),inference(spm,[status(thm)],[1519,1470,theory(equality)])).
% cnf(2858,negated_conjecture,(rearsegP(esk48_0,nil)|~ssList(esk48_0)|~ssList(nil)),inference(rw,[status(thm)],[2841,668,theory(equality)])).
% cnf(2859,negated_conjecture,(rearsegP(esk48_0,nil)|$false|~ssList(nil)),inference(rw,[status(thm)],[2858,583,theory(equality)])).
% cnf(2860,negated_conjecture,(rearsegP(esk48_0,nil)|$false|$false),inference(rw,[status(thm)],[2859,125,theory(equality)])).
% cnf(2861,negated_conjecture,(rearsegP(esk48_0,nil)),inference(cn,[status(thm)],[2860,theory(equality)])).
% cnf(2874,negated_conjecture,(ssList(esk47_2(esk48_0,nil))|~ssList(nil)|~ssList(esk48_0)),inference(spm,[status(thm)],[550,2861,theory(equality)])).
% cnf(2875,negated_conjecture,(app(esk47_2(esk48_0,nil),nil)=esk48_0|~ssList(nil)|~ssList(esk48_0)),inference(spm,[status(thm)],[549,2861,theory(equality)])).
% cnf(2879,negated_conjecture,(ssList(esk47_2(esk48_0,nil))|$false|~ssList(esk48_0)),inference(rw,[status(thm)],[2874,125,theory(equality)])).
% cnf(2880,negated_conjecture,(ssList(esk47_2(esk48_0,nil))|$false|$false),inference(rw,[status(thm)],[2879,583,theory(equality)])).
% cnf(2881,negated_conjecture,(ssList(esk47_2(esk48_0,nil))),inference(cn,[status(thm)],[2880,theory(equality)])).
% cnf(2882,negated_conjecture,(app(esk47_2(esk48_0,nil),nil)=esk48_0|$false|~ssList(esk48_0)),inference(rw,[status(thm)],[2875,125,theory(equality)])).
% cnf(2883,negated_conjecture,(app(esk47_2(esk48_0,nil),nil)=esk48_0|$false|$false),inference(rw,[status(thm)],[2882,583,theory(equality)])).
% cnf(2884,negated_conjecture,(app(esk47_2(esk48_0,nil),nil)=esk48_0),inference(cn,[status(thm)],[2883,theory(equality)])).
% cnf(2914,negated_conjecture,(esk48_0=esk47_2(esk48_0,nil)|~ssList(esk47_2(esk48_0,nil))),inference(spm,[status(thm)],[253,2884,theory(equality)])).
% cnf(2959,negated_conjecture,(esk48_0=esk47_2(esk48_0,nil)|$false),inference(rw,[status(thm)],[2914,2881,theory(equality)])).
% cnf(2960,negated_conjecture,(esk48_0=esk47_2(esk48_0,nil)),inference(cn,[status(thm)],[2959,theory(equality)])).
% cnf(2968,negated_conjecture,(app(esk48_0,nil)=esk48_0),inference(rw,[status(thm)],[2884,2960,theory(equality)])).
% cnf(2976,negated_conjecture,(frontsegP(X1,esk48_0)|esk48_0!=X1|~ssList(nil)|~ssList(esk48_0)|~ssList(X1)),inference(spm,[status(thm)],[490,2968,theory(equality)])).
% cnf(2979,negated_conjecture,(X1=nil|app(esk48_0,X1)!=esk48_0|~ssList(nil)|~ssList(esk48_0)|~ssList(X1)),inference(spm,[status(thm)],[369,2968,theory(equality)])).
% cnf(3002,negated_conjecture,(frontsegP(X1,esk48_0)|esk48_0!=X1|$false|~ssList(esk48_0)|~ssList(X1)),inference(rw,[status(thm)],[2976,125,theory(equality)])).
% cnf(3003,negated_conjecture,(frontsegP(X1,esk48_0)|esk48_0!=X1|$false|$false|~ssList(X1)),inference(rw,[status(thm)],[3002,583,theory(equality)])).
% cnf(3004,negated_conjecture,(frontsegP(X1,esk48_0)|esk48_0!=X1|~ssList(X1)),inference(cn,[status(thm)],[3003,theory(equality)])).
% cnf(3011,negated_conjecture,(X1=nil|app(esk48_0,X1)!=esk48_0|$false|~ssList(esk48_0)|~ssList(X1)),inference(rw,[status(thm)],[2979,125,theory(equality)])).
% cnf(3012,negated_conjecture,(X1=nil|app(esk48_0,X1)!=esk48_0|$false|$false|~ssList(X1)),inference(rw,[status(thm)],[3011,583,theory(equality)])).
% cnf(3013,negated_conjecture,(X1=nil|app(esk48_0,X1)!=esk48_0|~ssList(X1)),inference(cn,[status(thm)],[3012,theory(equality)])).
% cnf(3051,negated_conjecture,(frontsegP(esk48_0,esk48_0)|~ssList(esk48_0)),inference(er,[status(thm)],[3004,theory(equality)])).
% cnf(3052,negated_conjecture,(frontsegP(esk48_0,esk48_0)|$false),inference(rw,[status(thm)],[3051,583,theory(equality)])).
% cnf(3053,negated_conjecture,(frontsegP(esk48_0,esk48_0)),inference(cn,[status(thm)],[3052,theory(equality)])).
% cnf(3063,negated_conjecture,(frontsegP(app(esk48_0,X1),esk48_0)|~ssList(X1)|~ssList(esk48_0)),inference(spm,[status(thm)],[531,3053,theory(equality)])).
% cnf(3069,negated_conjecture,(frontsegP(app(esk48_0,X1),esk48_0)|~ssList(X1)|$false),inference(rw,[status(thm)],[3063,583,theory(equality)])).
% cnf(3070,negated_conjecture,(frontsegP(app(esk48_0,X1),esk48_0)|~ssList(X1)),inference(cn,[status(thm)],[3069,theory(equality)])).
% cnf(3660,negated_conjecture,(frontsegP(cons(esk52_0,X1),esk48_0)|~ssList(X1)),inference(spm,[status(thm)],[3070,1470,theory(equality)])).
% cnf(4498,negated_conjecture,(memberP(esk48_0,esk52_0)|~ssList(nil)|~ssItem(esk52_0)),inference(spm,[status(thm)],[715,668,theory(equality)])).
% cnf(4507,negated_conjecture,(memberP(esk48_0,esk52_0)|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[4498,125,theory(equality)])).
% cnf(4508,negated_conjecture,(memberP(esk48_0,esk52_0)|$false|$false),inference(rw,[status(thm)],[4507,664,theory(equality)])).
% cnf(4509,negated_conjecture,(memberP(esk48_0,esk52_0)),inference(cn,[status(thm)],[4508,theory(equality)])).
% cnf(4512,negated_conjecture,(ssList(esk5_2(esk48_0,esk52_0))|~ssList(esk48_0)|~ssItem(esk52_0)),inference(spm,[status(thm)],[183,4509,theory(equality)])).
% cnf(4513,negated_conjecture,(ssList(esk6_2(esk48_0,esk52_0))|~ssList(esk48_0)|~ssItem(esk52_0)),inference(spm,[status(thm)],[182,4509,theory(equality)])).
% cnf(4514,negated_conjecture,(app(esk5_2(esk48_0,esk52_0),cons(esk52_0,esk6_2(esk48_0,esk52_0)))=esk48_0|~ssList(esk48_0)|~ssItem(esk52_0)),inference(spm,[status(thm)],[181,4509,theory(equality)])).
% cnf(4518,negated_conjecture,(ssList(esk5_2(esk48_0,esk52_0))|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[4512,583,theory(equality)])).
% cnf(4519,negated_conjecture,(ssList(esk5_2(esk48_0,esk52_0))|$false|$false),inference(rw,[status(thm)],[4518,664,theory(equality)])).
% cnf(4520,negated_conjecture,(ssList(esk5_2(esk48_0,esk52_0))),inference(cn,[status(thm)],[4519,theory(equality)])).
% cnf(4521,negated_conjecture,(ssList(esk6_2(esk48_0,esk52_0))|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[4513,583,theory(equality)])).
% cnf(4522,negated_conjecture,(ssList(esk6_2(esk48_0,esk52_0))|$false|$false),inference(rw,[status(thm)],[4521,664,theory(equality)])).
% cnf(4523,negated_conjecture,(ssList(esk6_2(esk48_0,esk52_0))),inference(cn,[status(thm)],[4522,theory(equality)])).
% cnf(4524,negated_conjecture,(app(esk5_2(esk48_0,esk52_0),cons(esk52_0,esk6_2(esk48_0,esk52_0)))=esk48_0|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[4514,583,theory(equality)])).
% cnf(4525,negated_conjecture,(app(esk5_2(esk48_0,esk52_0),cons(esk52_0,esk6_2(esk48_0,esk52_0)))=esk48_0|$false|$false),inference(rw,[status(thm)],[4524,664,theory(equality)])).
% cnf(4526,negated_conjecture,(app(esk5_2(esk48_0,esk52_0),cons(esk52_0,esk6_2(esk48_0,esk52_0)))=esk48_0),inference(cn,[status(thm)],[4525,theory(equality)])).
% cnf(4567,negated_conjecture,(hd(esk48_0)=hd(esk5_2(esk48_0,esk52_0))|nil=esk5_2(esk48_0,esk52_0)|~ssList(cons(esk52_0,esk6_2(esk48_0,esk52_0)))|~ssList(esk5_2(esk48_0,esk52_0))),inference(spm,[status(thm)],[494,4526,theory(equality)])).
% cnf(4590,negated_conjecture,(esk52_0=hd(esk5_2(esk48_0,esk52_0))|nil=esk5_2(esk48_0,esk52_0)|~ssList(cons(esk52_0,esk6_2(esk48_0,esk52_0)))|~ssList(esk5_2(esk48_0,esk52_0))),inference(rw,[status(thm)],[4567,1385,theory(equality)])).
% cnf(4591,negated_conjecture,(esk52_0=hd(esk5_2(esk48_0,esk52_0))|nil=esk5_2(esk48_0,esk52_0)|~ssList(cons(esk52_0,esk6_2(esk48_0,esk52_0)))|$false),inference(rw,[status(thm)],[4590,4520,theory(equality)])).
% cnf(4592,negated_conjecture,(esk52_0=hd(esk5_2(esk48_0,esk52_0))|nil=esk5_2(esk48_0,esk52_0)|~ssList(cons(esk52_0,esk6_2(esk48_0,esk52_0)))),inference(cn,[status(thm)],[4591,theory(equality)])).
% cnf(5139,negated_conjecture,(hd(esk5_2(esk48_0,esk52_0))=esk52_0|esk5_2(esk48_0,esk52_0)=nil|~ssList(esk6_2(esk48_0,esk52_0))|~ssItem(esk52_0)),inference(spm,[status(thm)],[4592,124,theory(equality)])).
% cnf(5141,negated_conjecture,(hd(esk5_2(esk48_0,esk52_0))=esk52_0|esk5_2(esk48_0,esk52_0)=nil|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[5139,4523,theory(equality)])).
% cnf(5142,negated_conjecture,(hd(esk5_2(esk48_0,esk52_0))=esk52_0|esk5_2(esk48_0,esk52_0)=nil|$false|$false),inference(rw,[status(thm)],[5141,664,theory(equality)])).
% cnf(5143,negated_conjecture,(hd(esk5_2(esk48_0,esk52_0))=esk52_0|esk5_2(esk48_0,esk52_0)=nil),inference(cn,[status(thm)],[5142,theory(equality)])).
% cnf(5147,negated_conjecture,(cons(esk52_0,tl(esk5_2(esk48_0,esk52_0)))=esk5_2(esk48_0,esk52_0)|nil=esk5_2(esk48_0,esk52_0)|~ssList(esk5_2(esk48_0,esk52_0))),inference(spm,[status(thm)],[325,5143,theory(equality)])).
% cnf(5155,negated_conjecture,(cons(esk52_0,tl(esk5_2(esk48_0,esk52_0)))=esk5_2(esk48_0,esk52_0)|nil=esk5_2(esk48_0,esk52_0)|$false),inference(rw,[status(thm)],[5147,4520,theory(equality)])).
% cnf(5156,negated_conjecture,(cons(esk52_0,tl(esk5_2(esk48_0,esk52_0)))=esk5_2(esk48_0,esk52_0)|nil=esk5_2(esk48_0,esk52_0)),inference(cn,[status(thm)],[5155,theory(equality)])).
% cnf(5608,negated_conjecture,(frontsegP(esk5_2(esk48_0,esk52_0),esk48_0)|esk5_2(esk48_0,esk52_0)=nil|~ssList(tl(esk5_2(esk48_0,esk52_0)))),inference(spm,[status(thm)],[3660,5156,theory(equality)])).
% cnf(5835,negated_conjecture,(esk5_2(esk48_0,esk52_0)=nil|frontsegP(esk5_2(esk48_0,esk52_0),esk48_0)|~ssList(esk5_2(esk48_0,esk52_0))),inference(spm,[status(thm)],[5608,281,theory(equality)])).
% cnf(5836,negated_conjecture,(esk5_2(esk48_0,esk52_0)=nil|frontsegP(esk5_2(esk48_0,esk52_0),esk48_0)|$false),inference(rw,[status(thm)],[5835,4520,theory(equality)])).
% cnf(5837,negated_conjecture,(esk5_2(esk48_0,esk52_0)=nil|frontsegP(esk5_2(esk48_0,esk52_0),esk48_0)),inference(cn,[status(thm)],[5836,theory(equality)])).
% cnf(5839,negated_conjecture,(esk48_0=esk5_2(esk48_0,esk52_0)|esk5_2(esk48_0,esk52_0)=nil|~frontsegP(esk48_0,esk5_2(esk48_0,esk52_0))|~ssList(esk5_2(esk48_0,esk52_0))|~ssList(esk48_0)),inference(spm,[status(thm)],[406,5837,theory(equality)])).
% cnf(5846,negated_conjecture,(esk48_0=esk5_2(esk48_0,esk52_0)|esk5_2(esk48_0,esk52_0)=nil|~frontsegP(esk48_0,esk5_2(esk48_0,esk52_0))|$false|~ssList(esk48_0)),inference(rw,[status(thm)],[5839,4520,theory(equality)])).
% cnf(5847,negated_conjecture,(esk48_0=esk5_2(esk48_0,esk52_0)|esk5_2(esk48_0,esk52_0)=nil|~frontsegP(esk48_0,esk5_2(esk48_0,esk52_0))|$false|$false),inference(rw,[status(thm)],[5846,583,theory(equality)])).
% cnf(5848,negated_conjecture,(esk48_0=esk5_2(esk48_0,esk52_0)|esk5_2(esk48_0,esk52_0)=nil|~frontsegP(esk48_0,esk5_2(esk48_0,esk52_0))),inference(cn,[status(thm)],[5847,theory(equality)])).
% cnf(6181,plain,(frontsegP(app(X1,X2),X1)|~ssList(X2)|~ssList(X1)),inference(csr,[status(thm)],[752,336])).
% cnf(6192,negated_conjecture,(frontsegP(esk48_0,esk5_2(esk48_0,esk52_0))|~ssList(cons(esk52_0,esk6_2(esk48_0,esk52_0)))|~ssList(esk5_2(esk48_0,esk52_0))),inference(spm,[status(thm)],[6181,4526,theory(equality)])).
% cnf(6219,negated_conjecture,(frontsegP(esk48_0,esk5_2(esk48_0,esk52_0))|~ssList(cons(esk52_0,esk6_2(esk48_0,esk52_0)))|$false),inference(rw,[status(thm)],[6192,4520,theory(equality)])).
% cnf(6220,negated_conjecture,(frontsegP(esk48_0,esk5_2(esk48_0,esk52_0))|~ssList(cons(esk52_0,esk6_2(esk48_0,esk52_0)))),inference(cn,[status(thm)],[6219,theory(equality)])).
% cnf(6352,negated_conjecture,(frontsegP(esk48_0,esk5_2(esk48_0,esk52_0))|~ssList(esk6_2(esk48_0,esk52_0))|~ssItem(esk52_0)),inference(spm,[status(thm)],[6220,124,theory(equality)])).
% cnf(6354,negated_conjecture,(frontsegP(esk48_0,esk5_2(esk48_0,esk52_0))|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[6352,4523,theory(equality)])).
% cnf(6355,negated_conjecture,(frontsegP(esk48_0,esk5_2(esk48_0,esk52_0))|$false|$false),inference(rw,[status(thm)],[6354,664,theory(equality)])).
% cnf(6356,negated_conjecture,(frontsegP(esk48_0,esk5_2(esk48_0,esk52_0))),inference(cn,[status(thm)],[6355,theory(equality)])).
% cnf(6365,negated_conjecture,(esk5_2(esk48_0,esk52_0)=nil|esk5_2(esk48_0,esk52_0)=esk48_0|$false),inference(rw,[status(thm)],[5848,6356,theory(equality)])).
% cnf(6366,negated_conjecture,(esk5_2(esk48_0,esk52_0)=nil|esk5_2(esk48_0,esk52_0)=esk48_0),inference(cn,[status(thm)],[6365,theory(equality)])).
% cnf(6386,negated_conjecture,(app(esk48_0,cons(esk52_0,esk6_2(esk48_0,esk52_0)))=esk48_0|esk5_2(esk48_0,esk52_0)=nil),inference(spm,[status(thm)],[4526,6366,theory(equality)])).
% cnf(6483,plain,(rearsegP(app(X1,X2),X2)|~ssList(X1)|~ssList(X2)),inference(csr,[status(thm)],[762,336])).
% cnf(6495,negated_conjecture,(rearsegP(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0)))|~ssList(esk5_2(esk51_0,esk52_0))|~ssList(cons(esk52_0,esk6_2(esk51_0,esk52_0)))),inference(spm,[status(thm)],[6483,1488,theory(equality)])).
% cnf(6527,negated_conjecture,(rearsegP(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0)))|$false|~ssList(cons(esk52_0,esk6_2(esk51_0,esk52_0)))),inference(rw,[status(thm)],[6495,1482,theory(equality)])).
% cnf(6528,negated_conjecture,(rearsegP(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0)))|~ssList(cons(esk52_0,esk6_2(esk51_0,esk52_0)))),inference(cn,[status(thm)],[6527,theory(equality)])).
% cnf(6547,negated_conjecture,(rearsegP(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0)))|~ssList(esk6_2(esk51_0,esk52_0))|~ssItem(esk52_0)),inference(spm,[status(thm)],[6528,124,theory(equality)])).
% cnf(6549,negated_conjecture,(rearsegP(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0)))|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[6547,1485,theory(equality)])).
% cnf(6550,negated_conjecture,(rearsegP(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0)))|$false|$false),inference(rw,[status(thm)],[6549,664,theory(equality)])).
% cnf(6551,negated_conjecture,(rearsegP(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0)))),inference(cn,[status(thm)],[6550,theory(equality)])).
% cnf(6554,negated_conjecture,(ssList(esk47_2(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0))))|~ssList(cons(esk52_0,esk6_2(esk51_0,esk52_0)))|~ssList(esk51_0)),inference(spm,[status(thm)],[550,6551,theory(equality)])).
% cnf(6555,negated_conjecture,(app(esk47_2(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0))),cons(esk52_0,esk6_2(esk51_0,esk52_0)))=esk51_0|~ssList(cons(esk52_0,esk6_2(esk51_0,esk52_0)))|~ssList(esk51_0)),inference(spm,[status(thm)],[549,6551,theory(equality)])).
% cnf(6560,negated_conjecture,(ssList(esk47_2(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0))))|~ssList(cons(esk52_0,esk6_2(esk51_0,esk52_0)))|$false),inference(rw,[status(thm)],[6554,585,theory(equality)])).
% cnf(6561,negated_conjecture,(ssList(esk47_2(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0))))|~ssList(cons(esk52_0,esk6_2(esk51_0,esk52_0)))),inference(cn,[status(thm)],[6560,theory(equality)])).
% cnf(6562,negated_conjecture,(app(esk47_2(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0))),cons(esk52_0,esk6_2(esk51_0,esk52_0)))=esk51_0|~ssList(cons(esk52_0,esk6_2(esk51_0,esk52_0)))|$false),inference(rw,[status(thm)],[6555,585,theory(equality)])).
% cnf(6563,negated_conjecture,(app(esk47_2(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0))),cons(esk52_0,esk6_2(esk51_0,esk52_0)))=esk51_0|~ssList(cons(esk52_0,esk6_2(esk51_0,esk52_0)))),inference(cn,[status(thm)],[6562,theory(equality)])).
% cnf(6620,negated_conjecture,(ssList(esk47_2(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0))))|~ssList(esk6_2(esk51_0,esk52_0))|~ssItem(esk52_0)),inference(spm,[status(thm)],[6561,124,theory(equality)])).
% cnf(6622,negated_conjecture,(ssList(esk47_2(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0))))|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[6620,1485,theory(equality)])).
% cnf(6623,negated_conjecture,(ssList(esk47_2(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0))))|$false|$false),inference(rw,[status(thm)],[6622,664,theory(equality)])).
% cnf(6624,negated_conjecture,(ssList(esk47_2(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0))))),inference(cn,[status(thm)],[6623,theory(equality)])).
% cnf(6673,negated_conjecture,(cons(esk52_0,esk6_2(esk48_0,esk52_0))=nil|esk5_2(esk48_0,esk52_0)=nil|~ssList(cons(esk52_0,esk6_2(esk48_0,esk52_0)))),inference(spm,[status(thm)],[3013,6386,theory(equality)])).
% cnf(6748,negated_conjecture,(cons(esk52_0,esk6_2(esk48_0,esk52_0))=nil|esk5_2(esk48_0,esk52_0)=nil|~ssList(esk6_2(esk48_0,esk52_0))|~ssItem(esk52_0)),inference(spm,[status(thm)],[6673,124,theory(equality)])).
% cnf(6750,negated_conjecture,(cons(esk52_0,esk6_2(esk48_0,esk52_0))=nil|esk5_2(esk48_0,esk52_0)=nil|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[6748,4523,theory(equality)])).
% cnf(6751,negated_conjecture,(cons(esk52_0,esk6_2(esk48_0,esk52_0))=nil|esk5_2(esk48_0,esk52_0)=nil|$false|$false),inference(rw,[status(thm)],[6750,664,theory(equality)])).
% cnf(6752,negated_conjecture,(cons(esk52_0,esk6_2(esk48_0,esk52_0))=nil|esk5_2(esk48_0,esk52_0)=nil),inference(cn,[status(thm)],[6751,theory(equality)])).
% cnf(6761,negated_conjecture,(esk5_2(esk48_0,esk52_0)=nil|~ssList(esk6_2(esk48_0,esk52_0))|~ssItem(esk52_0)),inference(spm,[status(thm)],[146,6752,theory(equality)])).
% cnf(6844,negated_conjecture,(esk5_2(esk48_0,esk52_0)=nil|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[6761,4523,theory(equality)])).
% cnf(6845,negated_conjecture,(esk5_2(esk48_0,esk52_0)=nil|$false|$false),inference(rw,[status(thm)],[6844,664,theory(equality)])).
% cnf(6846,negated_conjecture,(esk5_2(esk48_0,esk52_0)=nil),inference(cn,[status(thm)],[6845,theory(equality)])).
% cnf(7014,negated_conjecture,(frontsegP(esk48_0,nil)),inference(rw,[status(thm)],[6356,6846,theory(equality)])).
% cnf(7045,negated_conjecture,(ssList(esk46_2(esk48_0,nil))|~ssList(nil)|~ssList(esk48_0)),inference(spm,[status(thm)],[489,7014,theory(equality)])).
% cnf(7047,negated_conjecture,(app(nil,esk46_2(esk48_0,nil))=esk48_0|~ssList(nil)|~ssList(esk48_0)),inference(spm,[status(thm)],[488,7014,theory(equality)])).
% cnf(7050,negated_conjecture,(ssList(esk46_2(esk48_0,nil))|$false|~ssList(esk48_0)),inference(rw,[status(thm)],[7045,125,theory(equality)])).
% cnf(7051,negated_conjecture,(ssList(esk46_2(esk48_0,nil))|$false|$false),inference(rw,[status(thm)],[7050,583,theory(equality)])).
% cnf(7052,negated_conjecture,(ssList(esk46_2(esk48_0,nil))),inference(cn,[status(thm)],[7051,theory(equality)])).
% cnf(7057,negated_conjecture,(app(nil,esk46_2(esk48_0,nil))=esk48_0|$false|~ssList(esk48_0)),inference(rw,[status(thm)],[7047,125,theory(equality)])).
% cnf(7058,negated_conjecture,(app(nil,esk46_2(esk48_0,nil))=esk48_0|$false|$false),inference(rw,[status(thm)],[7057,583,theory(equality)])).
% cnf(7059,negated_conjecture,(app(nil,esk46_2(esk48_0,nil))=esk48_0),inference(cn,[status(thm)],[7058,theory(equality)])).
% cnf(7080,negated_conjecture,(esk48_0=esk46_2(esk48_0,nil)|~ssList(esk46_2(esk48_0,nil))),inference(spm,[status(thm)],[243,7059,theory(equality)])).
% cnf(7127,negated_conjecture,(esk48_0=esk46_2(esk48_0,nil)|$false),inference(rw,[status(thm)],[7080,7052,theory(equality)])).
% cnf(7128,negated_conjecture,(esk48_0=esk46_2(esk48_0,nil)),inference(cn,[status(thm)],[7127,theory(equality)])).
% cnf(7170,negated_conjecture,(app(nil,esk48_0)=esk48_0),inference(rw,[status(thm)],[7059,7128,theory(equality)])).
% cnf(13302,plain,(segmentP(X1,X2)|app(X3,X2)!=X1|~ssList(X3)|~ssList(X2)|~ssList(X1)),inference(csr,[status(thm)],[851,336])).
% cnf(13303,plain,(segmentP(app(X1,X2),X2)|~ssList(X1)|~ssList(X2)|~ssList(app(X1,X2))),inference(er,[status(thm)],[13302,theory(equality)])).
% cnf(20999,negated_conjecture,(segmentP(app(esk48_0,X1),esk48_0)|~ssList(X1)|~ssList(nil)|~ssList(esk48_0)),inference(spm,[status(thm)],[940,7170,theory(equality)])).
% cnf(21067,negated_conjecture,(segmentP(app(esk48_0,X1),esk48_0)|~ssList(X1)|$false|~ssList(esk48_0)),inference(rw,[status(thm)],[20999,125,theory(equality)])).
% cnf(21068,negated_conjecture,(segmentP(app(esk48_0,X1),esk48_0)|~ssList(X1)|$false|$false),inference(rw,[status(thm)],[21067,583,theory(equality)])).
% cnf(21069,negated_conjecture,(segmentP(app(esk48_0,X1),esk48_0)|~ssList(X1)),inference(cn,[status(thm)],[21068,theory(equality)])).
% cnf(21565,negated_conjecture,(segmentP(cons(esk52_0,X1),esk48_0)|~ssList(X1)),inference(spm,[status(thm)],[21069,1470,theory(equality)])).
% cnf(21593,negated_conjecture,(segmentP(X1,esk48_0)|~segmentP(X1,cons(esk52_0,X2))|~ssList(esk48_0)|~ssList(cons(esk52_0,X2))|~ssList(X1)|~ssList(X2)),inference(spm,[status(thm)],[160,21565,theory(equality)])).
% cnf(21615,negated_conjecture,(segmentP(X1,esk48_0)|~segmentP(X1,cons(esk52_0,X2))|$false|~ssList(cons(esk52_0,X2))|~ssList(X1)|~ssList(X2)),inference(rw,[status(thm)],[21593,583,theory(equality)])).
% cnf(21616,negated_conjecture,(segmentP(X1,esk48_0)|~segmentP(X1,cons(esk52_0,X2))|~ssList(cons(esk52_0,X2))|~ssList(X1)|~ssList(X2)),inference(cn,[status(thm)],[21615,theory(equality)])).
% cnf(277421,negated_conjecture,(app(esk47_2(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0))),cons(esk52_0,esk6_2(esk51_0,esk52_0)))=esk51_0|~ssList(esk6_2(esk51_0,esk52_0))|~ssItem(esk52_0)),inference(spm,[status(thm)],[6563,124,theory(equality)])).
% cnf(277423,negated_conjecture,(app(esk47_2(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0))),cons(esk52_0,esk6_2(esk51_0,esk52_0)))=esk51_0|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[277421,1485,theory(equality)])).
% cnf(277424,negated_conjecture,(app(esk47_2(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0))),cons(esk52_0,esk6_2(esk51_0,esk52_0)))=esk51_0|$false|$false),inference(rw,[status(thm)],[277423,664,theory(equality)])).
% cnf(277425,negated_conjecture,(app(esk47_2(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0))),cons(esk52_0,esk6_2(esk51_0,esk52_0)))=esk51_0),inference(cn,[status(thm)],[277424,theory(equality)])).
% cnf(455593,plain,(segmentP(app(X1,X2),X2)|~ssList(X1)|~ssList(X2)),inference(csr,[status(thm)],[13303,336])).
% cnf(455713,negated_conjecture,(segmentP(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0)))|~ssList(esk47_2(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0))))|~ssList(cons(esk52_0,esk6_2(esk51_0,esk52_0)))),inference(spm,[status(thm)],[455593,277425,theory(equality)])).
% cnf(456155,negated_conjecture,(segmentP(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0)))|$false|~ssList(cons(esk52_0,esk6_2(esk51_0,esk52_0)))),inference(rw,[status(thm)],[455713,6624,theory(equality)])).
% cnf(456156,negated_conjecture,(segmentP(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0)))|~ssList(cons(esk52_0,esk6_2(esk51_0,esk52_0)))),inference(cn,[status(thm)],[456155,theory(equality)])).
% cnf(456537,negated_conjecture,(segmentP(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0)))|~ssList(esk6_2(esk51_0,esk52_0))|~ssItem(esk52_0)),inference(spm,[status(thm)],[456156,124,theory(equality)])).
% cnf(456539,negated_conjecture,(segmentP(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0)))|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[456537,1485,theory(equality)])).
% cnf(456540,negated_conjecture,(segmentP(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0)))|$false|$false),inference(rw,[status(thm)],[456539,664,theory(equality)])).
% cnf(456541,negated_conjecture,(segmentP(esk51_0,cons(esk52_0,esk6_2(esk51_0,esk52_0)))),inference(cn,[status(thm)],[456540,theory(equality)])).
% cnf(1261308,negated_conjecture,(segmentP(X1,esk48_0)|~segmentP(X1,cons(esk52_0,X2))|~ssList(X1)|~ssList(X2)),inference(csr,[status(thm)],[21616,2037])).
% cnf(1261334,negated_conjecture,(segmentP(esk51_0,esk48_0)|~ssList(esk51_0)|~ssList(esk6_2(esk51_0,esk52_0))),inference(spm,[status(thm)],[1261308,456541,theory(equality)])).
% cnf(1261512,negated_conjecture,(segmentP(esk51_0,esk48_0)|$false|~ssList(esk6_2(esk51_0,esk52_0))),inference(rw,[status(thm)],[1261334,585,theory(equality)])).
% cnf(1261513,negated_conjecture,(segmentP(esk51_0,esk48_0)|$false|$false),inference(rw,[status(thm)],[1261512,1485,theory(equality)])).
% cnf(1261514,negated_conjecture,(segmentP(esk51_0,esk48_0)),inference(cn,[status(thm)],[1261513,theory(equality)])).
% cnf(1262049,negated_conjecture,($false|~neq(esk48_0,nil)),inference(rw,[status(thm)],[590,1261514,theory(equality)])).
% cnf(1262050,negated_conjecture,(~neq(esk48_0,nil)),inference(cn,[status(thm)],[1262049,theory(equality)])).
% cnf(1262078,negated_conjecture,(esk48_0=nil|~ssList(nil)|~ssList(esk48_0)),inference(spm,[status(thm)],[1262050,119,theory(equality)])).
% cnf(1262080,negated_conjecture,(esk48_0=nil|$false|~ssList(esk48_0)),inference(rw,[status(thm)],[1262078,125,theory(equality)])).
% cnf(1262081,negated_conjecture,(esk48_0=nil|$false|$false),inference(rw,[status(thm)],[1262080,583,theory(equality)])).
% cnf(1262082,negated_conjecture,(esk48_0=nil),inference(cn,[status(thm)],[1262081,theory(equality)])).
% cnf(1262083,negated_conjecture,($false),inference(sr,[status(thm)],[1262082,1375,theory(equality)])).
% cnf(1262084,negated_conjecture,($false),1262083,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 35213
% # ...of these trivial : 684
% # ...subsumed : 23135
% # ...remaining for further processing: 11394
% # Other redundant clauses eliminated : 2282
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 507
% # Backward-rewritten : 1811
% # Generated clauses : 390362
% # ...of the previous two non-trivial : 353317
% # Contextual simplify-reflections : 6841
% # Paramodulations : 387297
% # Factorizations : 1
% # Equation resolutions : 3053
% # Current number of processed clauses: 9061
% # Positive orientable unit clauses: 3160
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 931
% # Non-unit-clauses : 4970
% # Current number of unprocessed clauses: 253659
% # ...number of literals in the above : 1630586
% # Clause-clause subsumption calls (NU) : 1116751
% # Rec. Clause-clause subsumption calls : 590628
% # Unit Clause-clause subsumption calls : 89391
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 88711
% # Indexed BW rewrite successes : 528
% # Backwards rewriting index: 3245 leaves, 3.15+/-9.027 terms/leaf
% # Paramod-from index: 1252 leaves, 3.43+/-11.274 terms/leaf
% # Paramod-into index: 2600 leaves, 3.32+/-9.730 terms/leaf
% # -------------------------------------------------
% # User time : 28.006 s
% # System time : 0.787 s
% # Total time : 28.793 s
% # Maximum resident set size: 0 pages
% PrfWatch: 47.19 CPU 47.67 WC
% FINAL PrfWatch: 47.19 CPU 47.67 WC
% SZS output end Solution for /tmp/SystemOnTPTP31007/SWC119+1.tptp
%
%------------------------------------------------------------------------------