%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SWC401+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 : art01.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 08:03:23 EST 2010
% Result : Theorem 4.09s
% Output : Solution 4.09s
% 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/SystemOnTPTP11031/SWC401+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP11031/SWC401+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP11031/SWC401+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 11127
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.030 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 1.93 CPU 2.02 WC
% # SZS output start CNFRefutation.
% fof(9, 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(10, 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(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)=>ssList(cons(X2,X1)))),file('/tmp/SRASS.s.p', ax16)).
% fof(22, 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(24, axiom,ssList(nil),file('/tmp/SRASS.s.p', ax17)).
% fof(25, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>ssList(app(X1,X2)))),file('/tmp/SRASS.s.p', ax26)).
% fof(46, axiom,![X1]:(ssList(X1)=>app(X1,nil)=X1),file('/tmp/SRASS.s.p', ax84)).
% fof(68, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(frontsegP(X1,X2)<=>?[X3]:(ssList(X3)&app(X2,X3)=X1)))),file('/tmp/SRASS.s.p', ax5)).
% fof(69, axiom,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>(rearsegP(X1,X2)<=>?[X3]:(ssList(X3)&app(X3,X2)=X1)))),file('/tmp/SRASS.s.p', ax6)).
% fof(82, 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(84, axiom,![X1]:(ssList(X1)=>rearsegP(X1,nil)),file('/tmp/SRASS.s.p', ax51)).
% fof(96, conjecture,![X1]:(ssList(X1)=>![X2]:(ssList(X2)=>![X3]:(ssList(X3)=>![X4]:(ssList(X4)=>(((((~(X2=X4)|~(X1=X3))|~(segmentP(X4,X3)))|~(totalorderedP(X3)))|?[X5]:((((ssList(X5)&neq(X3,X5))&segmentP(X4,X5))&segmentP(X5,X3))&totalorderedP(X5)))|![X6]:(ssItem(X6)=>(~(memberP(X1,X6))|memberP(X2,X6)))))))),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))|~(segmentP(X4,X3)))|~(totalorderedP(X3)))|?[X5]:((((ssList(X5)&neq(X3,X5))&segmentP(X4,X5))&segmentP(X5,X3))&totalorderedP(X5)))|![X6]:(ssItem(X6)=>(~(memberP(X1,X6))|memberP(X2,X6))))))))),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))|~(segmentP(X4,X3)))|~(totalorderedP(X3)))|?[X5]:((((ssList(X5)&neq(X3,X5))&segmentP(X4,X5))&segmentP(X5,X3))&totalorderedP(X5)))|![X6]:(ssItem(X6)=>(~(memberP(X1,X6))|memberP(X2,X6))))))))),inference(fof_simplification,[status(thm)],[97,theory(equality)])).
% fof(144, 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)],[9])).
% fof(145, 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)],[144])).
% fof(146, plain,![X5]:(~(ssList(X5))|![X6]:(~(ssList(X6))|((~(segmentP(X5,X6))|(ssList(esk3_2(X5,X6))&(ssList(esk4_2(X5,X6))&app(app(esk3_2(X5,X6),X6),esk4_2(X5,X6))=X5)))&(![X9]:(~(ssList(X9))|![X10]:(~(ssList(X10))|~(app(app(X9,X6),X10)=X5)))|segmentP(X5,X6))))),inference(skolemize,[status(esa)],[145])).
% fof(147, plain,![X5]:![X6]:![X9]:![X10]:((((((~(ssList(X10))|~(app(app(X9,X6),X10)=X5))|~(ssList(X9)))|segmentP(X5,X6))&(~(segmentP(X5,X6))|(ssList(esk3_2(X5,X6))&(ssList(esk4_2(X5,X6))&app(app(esk3_2(X5,X6),X6),esk4_2(X5,X6))=X5))))|~(ssList(X6)))|~(ssList(X5))),inference(shift_quantors,[status(thm)],[146])).
% fof(148, plain,![X5]:![X6]:![X9]:![X10]:((((((~(ssList(X10))|~(app(app(X9,X6),X10)=X5))|~(ssList(X9)))|segmentP(X5,X6))|~(ssList(X6)))|~(ssList(X5)))&((((ssList(esk3_2(X5,X6))|~(segmentP(X5,X6)))|~(ssList(X6)))|~(ssList(X5)))&((((ssList(esk4_2(X5,X6))|~(segmentP(X5,X6)))|~(ssList(X6)))|~(ssList(X5)))&(((app(app(esk3_2(X5,X6),X6),esk4_2(X5,X6))=X5|~(segmentP(X5,X6)))|~(ssList(X6)))|~(ssList(X5)))))),inference(distribute,[status(thm)],[147])).
% cnf(149,plain,(app(app(esk3_2(X1,X2),X2),esk4_2(X1,X2))=X1|~ssList(X1)|~ssList(X2)|~segmentP(X1,X2)),inference(split_conjunct,[status(thm)],[148])).
% cnf(150,plain,(ssList(esk4_2(X1,X2))|~ssList(X1)|~ssList(X2)|~segmentP(X1,X2)),inference(split_conjunct,[status(thm)],[148])).
% cnf(151,plain,(ssList(esk3_2(X1,X2))|~ssList(X1)|~ssList(X2)|~segmentP(X1,X2)),inference(split_conjunct,[status(thm)],[148])).
% fof(153, 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)],[10])).
% fof(154, 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)],[153])).
% fof(155, 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)],[154])).
% fof(156, 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)],[155])).
% cnf(157,plain,(memberP(app(X2,X3),X1)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|~memberP(X3,X1)),inference(split_conjunct,[status(thm)],[156])).
% cnf(158,plain,(memberP(app(X2,X3),X1)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|~memberP(X2,X1)),inference(split_conjunct,[status(thm)],[156])).
% fof(181, 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(182, 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)],[181])).
% fof(183, 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)],[182])).
% fof(184, 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)],[183])).
% fof(185, 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)],[184])).
% cnf(186,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)],[185])).
% cnf(187,plain,(ssList(esk6_2(X1,X2))|~ssList(X1)|~ssItem(X2)|~memberP(X1,X2)),inference(split_conjunct,[status(thm)],[185])).
% cnf(188,plain,(ssList(esk5_2(X1,X2))|~ssList(X1)|~ssItem(X2)|~memberP(X1,X2)),inference(split_conjunct,[status(thm)],[185])).
% fof(190, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssItem(X2))|ssList(cons(X2,X1)))),inference(fof_nnf,[status(thm)],[18])).
% fof(191, plain,![X3]:(~(ssList(X3))|![X4]:(~(ssItem(X4))|ssList(cons(X4,X3)))),inference(variable_rename,[status(thm)],[190])).
% fof(192, plain,![X3]:![X4]:((~(ssItem(X4))|ssList(cons(X4,X3)))|~(ssList(X3))),inference(shift_quantors,[status(thm)],[191])).
% cnf(193,plain,(ssList(cons(X2,X1))|~ssList(X1)|~ssItem(X2)),inference(split_conjunct,[status(thm)],[192])).
% fof(205, 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)],[22])).
% fof(206, 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)],[205])).
% fof(207, 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)],[206])).
% cnf(208,plain,(app(app(X1,X2),X3)=app(X1,app(X2,X3))|~ssList(X1)|~ssList(X2)|~ssList(X3)),inference(split_conjunct,[status(thm)],[207])).
% cnf(213,plain,(ssList(nil)),inference(split_conjunct,[status(thm)],[24])).
% fof(214, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|ssList(app(X1,X2)))),inference(fof_nnf,[status(thm)],[25])).
% fof(215, plain,![X3]:(~(ssList(X3))|![X4]:(~(ssList(X4))|ssList(app(X3,X4)))),inference(variable_rename,[status(thm)],[214])).
% fof(216, plain,![X3]:![X4]:((~(ssList(X4))|ssList(app(X3,X4)))|~(ssList(X3))),inference(shift_quantors,[status(thm)],[215])).
% cnf(217,plain,(ssList(app(X1,X2))|~ssList(X1)|~ssList(X2)),inference(split_conjunct,[status(thm)],[216])).
% fof(333, plain,![X1]:(~(ssList(X1))|app(X1,nil)=X1),inference(fof_nnf,[status(thm)],[46])).
% fof(334, plain,![X2]:(~(ssList(X2))|app(X2,nil)=X2),inference(variable_rename,[status(thm)],[333])).
% cnf(335,plain,(app(X1,nil)=X1|~ssList(X1)),inference(split_conjunct,[status(thm)],[334])).
% fof(414, 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)],[68])).
% fof(415, 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)],[414])).
% fof(416, plain,![X4]:(~(ssList(X4))|![X5]:(~(ssList(X5))|((~(frontsegP(X4,X5))|(ssList(esk24_2(X4,X5))&app(X5,esk24_2(X4,X5))=X4))&(![X7]:(~(ssList(X7))|~(app(X5,X7)=X4))|frontsegP(X4,X5))))),inference(skolemize,[status(esa)],[415])).
% fof(417, plain,![X4]:![X5]:![X7]:(((((~(ssList(X7))|~(app(X5,X7)=X4))|frontsegP(X4,X5))&(~(frontsegP(X4,X5))|(ssList(esk24_2(X4,X5))&app(X5,esk24_2(X4,X5))=X4)))|~(ssList(X5)))|~(ssList(X4))),inference(shift_quantors,[status(thm)],[416])).
% fof(418, plain,![X4]:![X5]:![X7]:(((((~(ssList(X7))|~(app(X5,X7)=X4))|frontsegP(X4,X5))|~(ssList(X5)))|~(ssList(X4)))&((((ssList(esk24_2(X4,X5))|~(frontsegP(X4,X5)))|~(ssList(X5)))|~(ssList(X4)))&(((app(X5,esk24_2(X4,X5))=X4|~(frontsegP(X4,X5)))|~(ssList(X5)))|~(ssList(X4))))),inference(distribute,[status(thm)],[417])).
% cnf(419,plain,(app(X2,esk24_2(X1,X2))=X1|~ssList(X1)|~ssList(X2)|~frontsegP(X1,X2)),inference(split_conjunct,[status(thm)],[418])).
% cnf(420,plain,(ssList(esk24_2(X1,X2))|~ssList(X1)|~ssList(X2)|~frontsegP(X1,X2)),inference(split_conjunct,[status(thm)],[418])).
% cnf(421,plain,(frontsegP(X1,X2)|~ssList(X1)|~ssList(X2)|app(X2,X3)!=X1|~ssList(X3)),inference(split_conjunct,[status(thm)],[418])).
% fof(422, 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)],[69])).
% fof(423, 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)],[422])).
% fof(424, plain,![X4]:(~(ssList(X4))|![X5]:(~(ssList(X5))|((~(rearsegP(X4,X5))|(ssList(esk25_2(X4,X5))&app(esk25_2(X4,X5),X5)=X4))&(![X7]:(~(ssList(X7))|~(app(X7,X5)=X4))|rearsegP(X4,X5))))),inference(skolemize,[status(esa)],[423])).
% fof(425, plain,![X4]:![X5]:![X7]:(((((~(ssList(X7))|~(app(X7,X5)=X4))|rearsegP(X4,X5))&(~(rearsegP(X4,X5))|(ssList(esk25_2(X4,X5))&app(esk25_2(X4,X5),X5)=X4)))|~(ssList(X5)))|~(ssList(X4))),inference(shift_quantors,[status(thm)],[424])).
% fof(426, plain,![X4]:![X5]:![X7]:(((((~(ssList(X7))|~(app(X7,X5)=X4))|rearsegP(X4,X5))|~(ssList(X5)))|~(ssList(X4)))&((((ssList(esk25_2(X4,X5))|~(rearsegP(X4,X5)))|~(ssList(X5)))|~(ssList(X4)))&(((app(esk25_2(X4,X5),X5)=X4|~(rearsegP(X4,X5)))|~(ssList(X5)))|~(ssList(X4))))),inference(distribute,[status(thm)],[425])).
% cnf(427,plain,(app(esk25_2(X1,X2),X2)=X1|~ssList(X1)|~ssList(X2)|~rearsegP(X1,X2)),inference(split_conjunct,[status(thm)],[426])).
% cnf(428,plain,(ssList(esk25_2(X1,X2))|~ssList(X1)|~ssList(X2)|~rearsegP(X1,X2)),inference(split_conjunct,[status(thm)],[426])).
% fof(526, plain,![X1]:(~(ssList(X1))|![X2]:(~(ssList(X2))|![X3]:(~(ssList(X3))|(~(rearsegP(X1,X2))|rearsegP(app(X3,X1),X2))))),inference(fof_nnf,[status(thm)],[82])).
% fof(527, plain,![X4]:(~(ssList(X4))|![X5]:(~(ssList(X5))|![X6]:(~(ssList(X6))|(~(rearsegP(X4,X5))|rearsegP(app(X6,X4),X5))))),inference(variable_rename,[status(thm)],[526])).
% fof(528, plain,![X4]:![X5]:![X6]:(((~(ssList(X6))|(~(rearsegP(X4,X5))|rearsegP(app(X6,X4),X5)))|~(ssList(X5)))|~(ssList(X4))),inference(shift_quantors,[status(thm)],[527])).
% cnf(529,plain,(rearsegP(app(X3,X1),X2)|~ssList(X1)|~ssList(X2)|~rearsegP(X1,X2)|~ssList(X3)),inference(split_conjunct,[status(thm)],[528])).
% fof(539, plain,![X1]:(~(ssList(X1))|rearsegP(X1,nil)),inference(fof_nnf,[status(thm)],[84])).
% fof(540, plain,![X2]:(~(ssList(X2))|rearsegP(X2,nil)),inference(variable_rename,[status(thm)],[539])).
% cnf(541,plain,(rearsegP(X1,nil)|~ssList(X1)),inference(split_conjunct,[status(thm)],[540])).
% fof(568, negated_conjecture,?[X1]:(ssList(X1)&?[X2]:(ssList(X2)&?[X3]:(ssList(X3)&?[X4]:(ssList(X4)&(((((X2=X4&X1=X3)&segmentP(X4,X3))&totalorderedP(X3))&![X5]:((((~(ssList(X5))|~(neq(X3,X5)))|~(segmentP(X4,X5)))|~(segmentP(X5,X3)))|~(totalorderedP(X5))))&?[X6]:(ssItem(X6)&(memberP(X1,X6)&~(memberP(X2,X6))))))))),inference(fof_nnf,[status(thm)],[103])).
% fof(569, negated_conjecture,?[X7]:(ssList(X7)&?[X8]:(ssList(X8)&?[X9]:(ssList(X9)&?[X10]:(ssList(X10)&(((((X8=X10&X7=X9)&segmentP(X10,X9))&totalorderedP(X9))&![X11]:((((~(ssList(X11))|~(neq(X9,X11)))|~(segmentP(X10,X11)))|~(segmentP(X11,X9)))|~(totalorderedP(X11))))&?[X12]:(ssItem(X12)&(memberP(X7,X12)&~(memberP(X8,X12))))))))),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)&segmentP(esk51_0,esk50_0))&totalorderedP(esk50_0))&![X11]:((((~(ssList(X11))|~(neq(esk50_0,X11)))|~(segmentP(esk51_0,X11)))|~(segmentP(X11,esk50_0)))|~(totalorderedP(X11))))&(ssItem(esk52_0)&(memberP(esk48_0,esk52_0)&~(memberP(esk49_0,esk52_0))))))))),inference(skolemize,[status(esa)],[569])).
% fof(571, negated_conjecture,![X11]:((((((((((~(ssList(X11))|~(neq(esk50_0,X11)))|~(segmentP(esk51_0,X11)))|~(segmentP(X11,esk50_0)))|~(totalorderedP(X11)))&(((esk49_0=esk51_0&esk48_0=esk50_0)&segmentP(esk51_0,esk50_0))&totalorderedP(esk50_0)))&(ssItem(esk52_0)&(memberP(esk48_0,esk52_0)&~(memberP(esk49_0,esk52_0)))))&ssList(esk51_0))&ssList(esk50_0))&ssList(esk49_0))&ssList(esk48_0)),inference(shift_quantors,[status(thm)],[570])).
% cnf(572,negated_conjecture,(ssList(esk48_0)),inference(split_conjunct,[status(thm)],[571])).
% cnf(573,negated_conjecture,(ssList(esk49_0)),inference(split_conjunct,[status(thm)],[571])).
% cnf(576,negated_conjecture,(~memberP(esk49_0,esk52_0)),inference(split_conjunct,[status(thm)],[571])).
% cnf(577,negated_conjecture,(memberP(esk48_0,esk52_0)),inference(split_conjunct,[status(thm)],[571])).
% cnf(578,negated_conjecture,(ssItem(esk52_0)),inference(split_conjunct,[status(thm)],[571])).
% cnf(580,negated_conjecture,(segmentP(esk51_0,esk50_0)),inference(split_conjunct,[status(thm)],[571])).
% cnf(581,negated_conjecture,(esk48_0=esk50_0),inference(split_conjunct,[status(thm)],[571])).
% cnf(582,negated_conjecture,(esk49_0=esk51_0),inference(split_conjunct,[status(thm)],[571])).
% cnf(584,negated_conjecture,(~memberP(esk51_0,esk52_0)),inference(rw,[status(thm)],[576,582,theory(equality)])).
% cnf(585,negated_conjecture,(ssList(esk50_0)),inference(rw,[status(thm)],[572,581,theory(equality)])).
% cnf(586,negated_conjecture,(ssList(esk51_0)),inference(rw,[status(thm)],[573,582,theory(equality)])).
% cnf(589,negated_conjecture,(memberP(esk50_0,esk52_0)),inference(rw,[status(thm)],[577,581,theory(equality)])).
% cnf(631,negated_conjecture,(ssList(esk3_2(esk51_0,esk50_0))|~ssList(esk50_0)|~ssList(esk51_0)),inference(spm,[status(thm)],[151,580,theory(equality)])).
% cnf(634,negated_conjecture,(ssList(esk3_2(esk51_0,esk50_0))|$false|~ssList(esk51_0)),inference(rw,[status(thm)],[631,585,theory(equality)])).
% cnf(635,negated_conjecture,(ssList(esk3_2(esk51_0,esk50_0))|$false|$false),inference(rw,[status(thm)],[634,586,theory(equality)])).
% cnf(636,negated_conjecture,(ssList(esk3_2(esk51_0,esk50_0))),inference(cn,[status(thm)],[635,theory(equality)])).
% cnf(639,negated_conjecture,(ssList(esk4_2(esk51_0,esk50_0))|~ssList(esk50_0)|~ssList(esk51_0)),inference(spm,[status(thm)],[150,580,theory(equality)])).
% cnf(642,negated_conjecture,(ssList(esk4_2(esk51_0,esk50_0))|$false|~ssList(esk51_0)),inference(rw,[status(thm)],[639,585,theory(equality)])).
% cnf(643,negated_conjecture,(ssList(esk4_2(esk51_0,esk50_0))|$false|$false),inference(rw,[status(thm)],[642,586,theory(equality)])).
% cnf(644,negated_conjecture,(ssList(esk4_2(esk51_0,esk50_0))),inference(cn,[status(thm)],[643,theory(equality)])).
% cnf(647,negated_conjecture,(ssList(esk5_2(esk50_0,esk52_0))|~ssList(esk50_0)|~ssItem(esk52_0)),inference(spm,[status(thm)],[188,589,theory(equality)])).
% cnf(648,negated_conjecture,(ssList(esk5_2(esk50_0,esk52_0))|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[647,585,theory(equality)])).
% cnf(649,negated_conjecture,(ssList(esk5_2(esk50_0,esk52_0))|$false|$false),inference(rw,[status(thm)],[648,578,theory(equality)])).
% cnf(650,negated_conjecture,(ssList(esk5_2(esk50_0,esk52_0))),inference(cn,[status(thm)],[649,theory(equality)])).
% cnf(651,negated_conjecture,(ssList(esk6_2(esk50_0,esk52_0))|~ssList(esk50_0)|~ssItem(esk52_0)),inference(spm,[status(thm)],[187,589,theory(equality)])).
% cnf(652,negated_conjecture,(ssList(esk6_2(esk50_0,esk52_0))|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[651,585,theory(equality)])).
% cnf(653,negated_conjecture,(ssList(esk6_2(esk50_0,esk52_0))|$false|$false),inference(rw,[status(thm)],[652,578,theory(equality)])).
% cnf(654,negated_conjecture,(ssList(esk6_2(esk50_0,esk52_0))),inference(cn,[status(thm)],[653,theory(equality)])).
% cnf(737,negated_conjecture,(memberP(app(X1,esk50_0),esk52_0)|~ssList(esk50_0)|~ssList(X1)|~ssItem(esk52_0)),inference(spm,[status(thm)],[157,589,theory(equality)])).
% cnf(738,negated_conjecture,(memberP(app(X1,esk50_0),esk52_0)|$false|~ssList(X1)|~ssItem(esk52_0)),inference(rw,[status(thm)],[737,585,theory(equality)])).
% cnf(739,negated_conjecture,(memberP(app(X1,esk50_0),esk52_0)|$false|~ssList(X1)|$false),inference(rw,[status(thm)],[738,578,theory(equality)])).
% cnf(740,negated_conjecture,(memberP(app(X1,esk50_0),esk52_0)|~ssList(X1)),inference(cn,[status(thm)],[739,theory(equality)])).
% cnf(754,plain,(frontsegP(app(X1,X2),X1)|~ssList(X2)|~ssList(X1)|~ssList(app(X1,X2))),inference(er,[status(thm)],[421,theory(equality)])).
% cnf(842,plain,(rearsegP(app(X1,X2),nil)|~ssList(X1)|~ssList(nil)|~ssList(X2)),inference(spm,[status(thm)],[529,541,theory(equality)])).
% cnf(844,plain,(rearsegP(app(X1,X2),nil)|~ssList(X1)|$false|~ssList(X2)),inference(rw,[status(thm)],[842,213,theory(equality)])).
% cnf(845,plain,(rearsegP(app(X1,X2),nil)|~ssList(X1)|~ssList(X2)),inference(cn,[status(thm)],[844,theory(equality)])).
% cnf(971,plain,(ssList(app(X1,app(X2,X3)))|~ssList(X3)|~ssList(app(X1,X2))|~ssList(X2)|~ssList(X1)),inference(spm,[status(thm)],[217,208,theory(equality)])).
% cnf(1007,negated_conjecture,(app(esk5_2(esk50_0,esk52_0),cons(esk52_0,esk6_2(esk50_0,esk52_0)))=esk50_0|~ssList(esk50_0)|~ssItem(esk52_0)),inference(spm,[status(thm)],[186,589,theory(equality)])).
% cnf(1008,negated_conjecture,(app(esk5_2(esk50_0,esk52_0),cons(esk52_0,esk6_2(esk50_0,esk52_0)))=esk50_0|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[1007,585,theory(equality)])).
% cnf(1009,negated_conjecture,(app(esk5_2(esk50_0,esk52_0),cons(esk52_0,esk6_2(esk50_0,esk52_0)))=esk50_0|$false|$false),inference(rw,[status(thm)],[1008,578,theory(equality)])).
% cnf(1010,negated_conjecture,(app(esk5_2(esk50_0,esk52_0),cons(esk52_0,esk6_2(esk50_0,esk52_0)))=esk50_0),inference(cn,[status(thm)],[1009,theory(equality)])).
% cnf(1011,negated_conjecture,(app(app(esk3_2(esk51_0,esk50_0),esk50_0),esk4_2(esk51_0,esk50_0))=esk51_0|~ssList(esk50_0)|~ssList(esk51_0)),inference(spm,[status(thm)],[149,580,theory(equality)])).
% cnf(1014,negated_conjecture,(app(app(esk3_2(esk51_0,esk50_0),esk50_0),esk4_2(esk51_0,esk50_0))=esk51_0|$false|~ssList(esk51_0)),inference(rw,[status(thm)],[1011,585,theory(equality)])).
% cnf(1015,negated_conjecture,(app(app(esk3_2(esk51_0,esk50_0),esk50_0),esk4_2(esk51_0,esk50_0))=esk51_0|$false|$false),inference(rw,[status(thm)],[1014,586,theory(equality)])).
% cnf(1016,negated_conjecture,(app(app(esk3_2(esk51_0,esk50_0),esk50_0),esk4_2(esk51_0,esk50_0))=esk51_0),inference(cn,[status(thm)],[1015,theory(equality)])).
% cnf(1424,negated_conjecture,(memberP(app(app(X1,esk50_0),X2),esk52_0)|~ssList(X2)|~ssList(app(X1,esk50_0))|~ssItem(esk52_0)|~ssList(X1)),inference(spm,[status(thm)],[158,740,theory(equality)])).
% cnf(1440,negated_conjecture,(memberP(app(app(X1,esk50_0),X2),esk52_0)|~ssList(X2)|~ssList(app(X1,esk50_0))|$false|~ssList(X1)),inference(rw,[status(thm)],[1424,578,theory(equality)])).
% cnf(1441,negated_conjecture,(memberP(app(app(X1,esk50_0),X2),esk52_0)|~ssList(X2)|~ssList(app(X1,esk50_0))|~ssList(X1)),inference(cn,[status(thm)],[1440,theory(equality)])).
% cnf(3233,plain,(frontsegP(app(X1,X2),X1)|~ssList(X2)|~ssList(X1)),inference(csr,[status(thm)],[754,217])).
% cnf(3243,negated_conjecture,(frontsegP(esk50_0,esk5_2(esk50_0,esk52_0))|~ssList(cons(esk52_0,esk6_2(esk50_0,esk52_0)))|~ssList(esk5_2(esk50_0,esk52_0))),inference(spm,[status(thm)],[3233,1010,theory(equality)])).
% cnf(3269,negated_conjecture,(frontsegP(esk50_0,esk5_2(esk50_0,esk52_0))|~ssList(cons(esk52_0,esk6_2(esk50_0,esk52_0)))|$false),inference(rw,[status(thm)],[3243,650,theory(equality)])).
% cnf(3270,negated_conjecture,(frontsegP(esk50_0,esk5_2(esk50_0,esk52_0))|~ssList(cons(esk52_0,esk6_2(esk50_0,esk52_0)))),inference(cn,[status(thm)],[3269,theory(equality)])).
% cnf(3290,negated_conjecture,(frontsegP(esk50_0,esk5_2(esk50_0,esk52_0))|~ssList(esk6_2(esk50_0,esk52_0))|~ssItem(esk52_0)),inference(spm,[status(thm)],[3270,193,theory(equality)])).
% cnf(3293,negated_conjecture,(frontsegP(esk50_0,esk5_2(esk50_0,esk52_0))|$false|~ssItem(esk52_0)),inference(rw,[status(thm)],[3290,654,theory(equality)])).
% cnf(3294,negated_conjecture,(frontsegP(esk50_0,esk5_2(esk50_0,esk52_0))|$false|$false),inference(rw,[status(thm)],[3293,578,theory(equality)])).
% cnf(3295,negated_conjecture,(frontsegP(esk50_0,esk5_2(esk50_0,esk52_0))),inference(cn,[status(thm)],[3294,theory(equality)])).
% cnf(3296,negated_conjecture,(ssList(esk24_2(esk50_0,esk5_2(esk50_0,esk52_0)))|~ssList(esk5_2(esk50_0,esk52_0))|~ssList(esk50_0)),inference(spm,[status(thm)],[420,3295,theory(equality)])).
% cnf(3298,negated_conjecture,(app(esk5_2(esk50_0,esk52_0),esk24_2(esk50_0,esk5_2(esk50_0,esk52_0)))=esk50_0|~ssList(esk5_2(esk50_0,esk52_0))|~ssList(esk50_0)),inference(spm,[status(thm)],[419,3295,theory(equality)])).
% cnf(3303,negated_conjecture,(ssList(esk24_2(esk50_0,esk5_2(esk50_0,esk52_0)))|$false|~ssList(esk50_0)),inference(rw,[status(thm)],[3296,650,theory(equality)])).
% cnf(3304,negated_conjecture,(ssList(esk24_2(esk50_0,esk5_2(esk50_0,esk52_0)))|$false|$false),inference(rw,[status(thm)],[3303,585,theory(equality)])).
% cnf(3305,negated_conjecture,(ssList(esk24_2(esk50_0,esk5_2(esk50_0,esk52_0)))),inference(cn,[status(thm)],[3304,theory(equality)])).
% cnf(3309,negated_conjecture,(app(esk5_2(esk50_0,esk52_0),esk24_2(esk50_0,esk5_2(esk50_0,esk52_0)))=esk50_0|$false|~ssList(esk50_0)),inference(rw,[status(thm)],[3298,650,theory(equality)])).
% cnf(3310,negated_conjecture,(app(esk5_2(esk50_0,esk52_0),esk24_2(esk50_0,esk5_2(esk50_0,esk52_0)))=esk50_0|$false|$false),inference(rw,[status(thm)],[3309,585,theory(equality)])).
% cnf(3311,negated_conjecture,(app(esk5_2(esk50_0,esk52_0),esk24_2(esk50_0,esk5_2(esk50_0,esk52_0)))=esk50_0),inference(cn,[status(thm)],[3310,theory(equality)])).
% cnf(6315,negated_conjecture,(rearsegP(esk50_0,nil)|~ssList(esk5_2(esk50_0,esk52_0))|~ssList(esk24_2(esk50_0,esk5_2(esk50_0,esk52_0)))),inference(spm,[status(thm)],[845,3311,theory(equality)])).
% cnf(6346,negated_conjecture,(rearsegP(esk50_0,nil)|$false|~ssList(esk24_2(esk50_0,esk5_2(esk50_0,esk52_0)))),inference(rw,[status(thm)],[6315,650,theory(equality)])).
% cnf(6347,negated_conjecture,(rearsegP(esk50_0,nil)|$false|$false),inference(rw,[status(thm)],[6346,3305,theory(equality)])).
% cnf(6348,negated_conjecture,(rearsegP(esk50_0,nil)),inference(cn,[status(thm)],[6347,theory(equality)])).
% cnf(6387,negated_conjecture,(ssList(esk25_2(esk50_0,nil))|~ssList(nil)|~ssList(esk50_0)),inference(spm,[status(thm)],[428,6348,theory(equality)])).
% cnf(6388,negated_conjecture,(app(esk25_2(esk50_0,nil),nil)=esk50_0|~ssList(nil)|~ssList(esk50_0)),inference(spm,[status(thm)],[427,6348,theory(equality)])).
% cnf(6392,negated_conjecture,(ssList(esk25_2(esk50_0,nil))|$false|~ssList(esk50_0)),inference(rw,[status(thm)],[6387,213,theory(equality)])).
% cnf(6393,negated_conjecture,(ssList(esk25_2(esk50_0,nil))|$false|$false),inference(rw,[status(thm)],[6392,585,theory(equality)])).
% cnf(6394,negated_conjecture,(ssList(esk25_2(esk50_0,nil))),inference(cn,[status(thm)],[6393,theory(equality)])).
% cnf(6395,negated_conjecture,(app(esk25_2(esk50_0,nil),nil)=esk50_0|$false|~ssList(esk50_0)),inference(rw,[status(thm)],[6388,213,theory(equality)])).
% cnf(6396,negated_conjecture,(app(esk25_2(esk50_0,nil),nil)=esk50_0|$false|$false),inference(rw,[status(thm)],[6395,585,theory(equality)])).
% cnf(6397,negated_conjecture,(app(esk25_2(esk50_0,nil),nil)=esk50_0),inference(cn,[status(thm)],[6396,theory(equality)])).
% cnf(6899,negated_conjecture,(esk50_0=esk25_2(esk50_0,nil)|~ssList(esk25_2(esk50_0,nil))),inference(spm,[status(thm)],[335,6397,theory(equality)])).
% cnf(6972,negated_conjecture,(esk50_0=esk25_2(esk50_0,nil)|$false),inference(rw,[status(thm)],[6899,6394,theory(equality)])).
% cnf(6973,negated_conjecture,(esk50_0=esk25_2(esk50_0,nil)),inference(cn,[status(thm)],[6972,theory(equality)])).
% cnf(6979,negated_conjecture,(app(esk50_0,nil)=esk50_0),inference(rw,[status(thm)],[6397,6973,theory(equality)])).
% cnf(19058,plain,(ssList(app(X1,app(X2,X3)))|~ssList(X2)|~ssList(X1)|~ssList(X3)),inference(csr,[status(thm)],[971,217])).
% cnf(19060,negated_conjecture,(ssList(app(X1,esk50_0))|~ssList(nil)|~ssList(esk50_0)|~ssList(X1)),inference(spm,[status(thm)],[19058,6979,theory(equality)])).
% cnf(19113,negated_conjecture,(ssList(app(X1,esk50_0))|$false|~ssList(esk50_0)|~ssList(X1)),inference(rw,[status(thm)],[19060,213,theory(equality)])).
% cnf(19114,negated_conjecture,(ssList(app(X1,esk50_0))|$false|$false|~ssList(X1)),inference(rw,[status(thm)],[19113,585,theory(equality)])).
% cnf(19115,negated_conjecture,(ssList(app(X1,esk50_0))|~ssList(X1)),inference(cn,[status(thm)],[19114,theory(equality)])).
% cnf(65718,negated_conjecture,(memberP(app(app(X1,esk50_0),X2),esk52_0)|~ssList(X1)|~ssList(X2)),inference(csr,[status(thm)],[1441,19115])).
% cnf(65744,negated_conjecture,(memberP(esk51_0,esk52_0)|~ssList(esk4_2(esk51_0,esk50_0))|~ssList(esk3_2(esk51_0,esk50_0))),inference(spm,[status(thm)],[65718,1016,theory(equality)])).
% cnf(65793,negated_conjecture,(memberP(esk51_0,esk52_0)|$false|~ssList(esk3_2(esk51_0,esk50_0))),inference(rw,[status(thm)],[65744,644,theory(equality)])).
% cnf(65794,negated_conjecture,(memberP(esk51_0,esk52_0)|$false|$false),inference(rw,[status(thm)],[65793,636,theory(equality)])).
% cnf(65795,negated_conjecture,(memberP(esk51_0,esk52_0)),inference(cn,[status(thm)],[65794,theory(equality)])).
% cnf(65796,negated_conjecture,($false),inference(sr,[status(thm)],[65795,584,theory(equality)])).
% cnf(65797,negated_conjecture,($false),65796,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 4697
% # ...of these trivial : 24
% # ...subsumed : 1922
% # ...remaining for further processing: 2751
% # Other redundant clauses eliminated : 767
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 253
% # Backward-rewritten : 574
% # Generated clauses : 24931
% # ...of the previous two non-trivial : 21930
% # Contextual simplify-reflections : 2251
% # Paramodulations : 23869
% # Factorizations : 0
% # Equation resolutions : 1062
% # Current number of processed clauses: 1918
% # Positive orientable unit clauses: 342
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 4
% # Non-unit-clauses : 1572
% # Current number of unprocessed clauses: 14398
% # ...number of literals in the above : 107690
% # Clause-clause subsumption calls (NU) : 106093
% # Rec. Clause-clause subsumption calls : 55504
% # Unit Clause-clause subsumption calls : 971
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 662
% # Indexed BW rewrite successes : 139
% # Backwards rewriting index: 1744 leaves, 1.31+/-1.078 terms/leaf
% # Paramod-from index: 670 leaves, 1.29+/-1.179 terms/leaf
% # Paramod-into index: 1369 leaves, 1.26+/-1.068 terms/leaf
% # -------------------------------------------------
% # User time : 1.680 s
% # System time : 0.061 s
% # Total time : 1.741 s
% # Maximum resident set size: 0 pages
% PrfWatch: 2.82 CPU 2.92 WC
% FINAL PrfWatch: 2.82 CPU 2.92 WC
% SZS output end Solution for /tmp/SystemOnTPTP11031/SWC401+1.tptp
%
%------------------------------------------------------------------------------