%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWC299+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:09:13 PM UTC 2026
% Result : Theorem 37.71s 12.06s
% Output : CNFRefutation 37.71s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f559ERROR: Could not build tree for root c_159345ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> ( memberP(X0,X1)
<=> ? [X2] :
( ? [X3] :
( app(X2,cons(X1,X3)) = X0
& ssList(X3) )
& ssList(X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax3) ).
fof(f5,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( frontsegP(X0,X1)
<=> ? [X2] :
( app(X1,X2) = X0
& ssList(X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax5) ).
fof(f16,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> ssList(cons(X1,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax16) ).
fof(f17,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax17) ).
fof(f18,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> cons(X1,X0) != X0 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax18) ).
fof(f26,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ssList(app(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax26) ).
fof(f28,axiom,
! [X0] :
( ssList(X0)
=> app(nil,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax28) ).
fof(f36,axiom,
! [X0] :
( ssItem(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ( memberP(app(X1,X2),X0)
<=> ( memberP(X2,X0)
| memberP(X1,X0) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax36) ).
fof(f37,axiom,
! [X0] :
( ssItem(X0)
=> ! [X1] :
( ssItem(X1)
=> ! [X2] :
( ssList(X2)
=> ( memberP(cons(X1,X2),X0)
<=> ( memberP(X2,X0)
| X0 = X1 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax37) ).
fof(f38,axiom,
! [X0] :
( ssItem(X0)
=> ~ memberP(nil,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax38) ).
fof(f41,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( ( frontsegP(X1,X0)
& frontsegP(X0,X1) )
=> X0 = X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax41) ).
fof(f81,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> cons(X1,X0) = app(cons(X1,nil),X0) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax81) ).
fof(f83,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( nil = app(X0,X1)
<=> ( nil = X0
& nil = X1 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax',ax83) ).
fof(f96,conjecture,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ( ( ( nil != X2
| nil != X3 )
& ! [X9] :
( ssItem(X9)
=> ! [X10] :
( ssList(X10)
=> ! [X11] :
( ssList(X11)
=> ( ? [X13] :
( lt(X13,X9)
& memberP(X11,X13)
& ssItem(X13) )
| ? [X12] :
( lt(X9,X12)
& memberP(X10,X12)
& ssItem(X12) )
| app(app(X10,X2),X11) != X3
| cons(X9,nil) != X2 ) ) ) ) )
| ! [X4] :
( ssItem(X4)
=> ! [X5] :
( ssItem(X5)
=> ! [X6] :
( ssList(X6)
=> ! [X7] :
( ssList(X7)
=> ! [X8] :
( ssList(X8)
=> ( ~ lt(X5,X4)
| app(app(app(app(X6,cons(X4,nil)),X7),cons(X5,nil)),X8) != X0 ) ) ) ) ) )
| X0 != X2
| X1 != X3 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f97,negated_conjecture,
~ ! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ( ( ( nil != X2
| nil != X3 )
& ! [X9] :
( ssItem(X9)
=> ! [X10] :
( ssList(X10)
=> ! [X11] :
( ssList(X11)
=> ( ? [X13] :
( lt(X13,X9)
& memberP(X11,X13)
& ssItem(X13) )
| ? [X12] :
( lt(X9,X12)
& memberP(X10,X12)
& ssItem(X12) )
| app(app(X10,X2),X11) != X3
| cons(X9,nil) != X2 ) ) ) ) )
| ! [X4] :
( ssItem(X4)
=> ! [X5] :
( ssItem(X5)
=> ! [X6] :
( ssList(X6)
=> ! [X7] :
( ssList(X7)
=> ! [X8] :
( ssList(X8)
=> ( ~ lt(X5,X4)
| app(app(app(app(X6,cons(X4,nil)),X7),cons(X5,nil)),X8) != X0 ) ) ) ) ) )
| X0 != X2
| X1 != X3 ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f99,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssItem(X1)
| ( memberP(X0,X1)
<=> ? [X2] :
( ? [X3] :
( app(X2,cons(X1,X3)) = X0
& ssList(X3) )
& ssList(X2) ) ) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f101,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssList(X1)
| ( frontsegP(X0,X1)
<=> ? [X2] :
( app(X1,X2) = X0
& ssList(X2) ) ) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f119,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssItem(X1)
| ssList(cons(X1,X0)) ) ),
inference(ennf_transformation,[],[f16]) ).
fof(f120,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssItem(X1)
| cons(X1,X0) != X0 ) ),
inference(ennf_transformation,[],[f18]) ).
fof(f132,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssList(X1)
| ssList(app(X0,X1)) ) ),
inference(ennf_transformation,[],[f26]) ).
fof(f134,plain,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
inference(ennf_transformation,[],[f28]) ).
fof(f146,plain,
! [X0] :
( ~ ssItem(X0)
| ! [X1] :
( ~ ssList(X1)
| ! [X2] :
( ~ ssList(X2)
| ( memberP(app(X1,X2),X0)
<=> ( memberP(X2,X0)
| memberP(X1,X0) ) ) ) ) ),
inference(ennf_transformation,[],[f36]) ).
fof(f147,plain,
! [X0] :
( ~ ssItem(X0)
| ! [X1] :
( ~ ssItem(X1)
| ! [X2] :
( ~ ssList(X2)
| ( memberP(cons(X1,X2),X0)
<=> ( memberP(X2,X0)
| X0 = X1 ) ) ) ) ),
inference(ennf_transformation,[],[f37]) ).
fof(f148,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(ennf_transformation,[],[f38]) ).
fof(f151,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssList(X1)
| ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1)
| X0 = X1 ) ),
inference(ennf_transformation,[],[f41]) ).
fof(f152,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssList(X1)
| ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1)
| X0 = X1 ) ),
inference(flattening,[],[f151]) ).
fof(f198,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssItem(X1)
| cons(X1,X0) = app(cons(X1,nil),X0) ) ),
inference(ennf_transformation,[],[f81]) ).
fof(f200,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssList(X1)
| ( nil = app(X0,X1)
<=> ( nil = X0
& nil = X1 ) ) ) ),
inference(ennf_transformation,[],[f83]) ).
fof(f221,plain,
? [X0] :
( ssList(X0)
& ? [X1] :
( ssList(X1)
& ? [X2] :
( ssList(X2)
& ? [X3] :
( ssList(X3)
& ( ( nil = X2
& nil = X3 )
| ? [X9] :
( ssItem(X9)
& ? [X10] :
( ssList(X10)
& ? [X11] :
( ssList(X11)
& ! [X13] :
( ~ lt(X13,X9)
| ~ memberP(X11,X13)
| ~ ssItem(X13) )
& ! [X12] :
( ~ lt(X9,X12)
| ~ memberP(X10,X12)
| ~ ssItem(X12) )
& app(app(X10,X2),X11) = X3
& cons(X9,nil) = X2 ) ) ) )
& ? [X4] :
( ssItem(X4)
& ? [X5] :
( ssItem(X5)
& ? [X6] :
( ssList(X6)
& ? [X7] :
( ssList(X7)
& ? [X8] :
( ssList(X8)
& lt(X5,X4)
& app(app(app(app(X6,cons(X4,nil)),X7),cons(X5,nil)),X8) = X0 ) ) ) ) )
& X0 = X2
& X1 = X3 ) ) ) ),
inference(ennf_transformation,[],[f97]) ).
fof(f222,plain,
? [X0] :
( ssList(X0)
& ? [X1] :
( ssList(X1)
& ? [X2] :
( ssList(X2)
& ? [X3] :
( ssList(X3)
& ( ( nil = X2
& nil = X3 )
| ? [X9] :
( ssItem(X9)
& ? [X10] :
( ssList(X10)
& ? [X11] :
( ssList(X11)
& ! [X13] :
( ~ lt(X13,X9)
| ~ memberP(X11,X13)
| ~ ssItem(X13) )
& ! [X12] :
( ~ lt(X9,X12)
| ~ memberP(X10,X12)
| ~ ssItem(X12) )
& app(app(X10,X2),X11) = X3
& cons(X9,nil) = X2 ) ) ) )
& ? [X4] :
( ssItem(X4)
& ? [X5] :
( ssItem(X5)
& ? [X6] :
( ssList(X6)
& ? [X7] :
( ssList(X7)
& ? [X8] :
( ssList(X8)
& lt(X5,X4)
& app(app(app(app(X6,cons(X4,nil)),X7),cons(X5,nil)),X8) = X0 ) ) ) ) )
& X0 = X2
& X1 = X3 ) ) ) ),
inference(flattening,[],[f221]) ).
fof(f236,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssItem(X1)
| ( ( ~ memberP(X0,X1)
| ? [X2] :
( ? [X3] :
( app(X2,cons(X1,X3)) = X0
& ssList(X3) )
& ssList(X2) ) )
& ( ! [X2] :
( ! [X3] :
( app(X2,cons(X1,X3)) != X0
| ~ ssList(X3) )
| ~ ssList(X2) )
| memberP(X0,X1) ) ) ) ),
inference(nnf_transformation,[],[f99]) ).
fof(f237,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssItem(X1)
| ( ( ~ memberP(X0,X1)
| ? [X4] :
( ? [X5] :
( app(X4,cons(X1,X5)) = X0
& ssList(X5) )
& ssList(X4) ) )
& ( ! [X2] :
( ! [X3] :
( app(X2,cons(X1,X3)) != X0
| ~ ssList(X3) )
| ~ ssList(X2) )
| memberP(X0,X1) ) ) ) ),
inference(rectify,[],[f236]) ).
fof(f238,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssItem(X1)
| ( ( ~ memberP(X0,X1)
| ( app(sK9(X0,X1),cons(X1,sK10(X0,X1))) = X0
& ssList(sK10(X0,X1))
& ssList(sK9(X0,X1)) ) )
& ( ! [X2] :
( ! [X3] :
( app(X2,cons(X1,X3)) != X0
| ~ ssList(X3) )
| ~ ssList(X2) )
| memberP(X0,X1) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10]),skolemize(X4,sK9(X0,X1)),skolemize(X5,sK10(X0,X1))],[f237]) ).
fof(f242,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssList(X1)
| ( ( ~ frontsegP(X0,X1)
| ? [X2] :
( app(X1,X2) = X0
& ssList(X2) ) )
& ( ! [X2] :
( app(X1,X2) != X0
| ~ ssList(X2) )
| frontsegP(X0,X1) ) ) ) ),
inference(nnf_transformation,[],[f101]) ).
fof(f243,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssList(X1)
| ( ( ~ frontsegP(X0,X1)
| ? [X3] :
( app(X1,X3) = X0
& ssList(X3) ) )
& ( ! [X2] :
( app(X1,X2) != X0
| ~ ssList(X2) )
| frontsegP(X0,X1) ) ) ) ),
inference(rectify,[],[f242]) ).
fof(f244,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssList(X1)
| ( ( ~ frontsegP(X0,X1)
| ( app(X1,sK12(X0,X1)) = X0
& ssList(sK12(X0,X1)) ) )
& ( ! [X2] :
( app(X1,X2) != X0
| ~ ssList(X2) )
| frontsegP(X0,X1) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X3,sK12(X0,X1))],[f243]) ).
fof(f279,plain,
! [X0] :
( ~ ssItem(X0)
| ! [X1] :
( ~ ssList(X1)
| ! [X2] :
( ~ ssList(X2)
| ( ( ~ memberP(app(X1,X2),X0)
| memberP(X2,X0)
| memberP(X1,X0) )
& ( ( ~ memberP(X2,X0)
& ~ memberP(X1,X0) )
| memberP(app(X1,X2),X0) ) ) ) ) ),
inference(nnf_transformation,[],[f146]) ).
fof(f280,plain,
! [X0] :
( ~ ssItem(X0)
| ! [X1] :
( ~ ssList(X1)
| ! [X2] :
( ~ ssList(X2)
| ( ( ~ memberP(app(X1,X2),X0)
| memberP(X2,X0)
| memberP(X1,X0) )
& ( ( ~ memberP(X2,X0)
& ~ memberP(X1,X0) )
| memberP(app(X1,X2),X0) ) ) ) ) ),
inference(flattening,[],[f279]) ).
fof(f281,plain,
! [X0] :
( ~ ssItem(X0)
| ! [X1] :
( ~ ssItem(X1)
| ! [X2] :
( ~ ssList(X2)
| ( ( ~ memberP(cons(X1,X2),X0)
| memberP(X2,X0)
| X0 = X1 )
& ( ( ~ memberP(X2,X0)
& X0 != X1 )
| memberP(cons(X1,X2),X0) ) ) ) ) ),
inference(nnf_transformation,[],[f147]) ).
fof(f282,plain,
! [X0] :
( ~ ssItem(X0)
| ! [X1] :
( ~ ssItem(X1)
| ! [X2] :
( ~ ssList(X2)
| ( ( ~ memberP(cons(X1,X2),X0)
| memberP(X2,X0)
| X0 = X1 )
& ( ( ~ memberP(X2,X0)
& X0 != X1 )
| memberP(cons(X1,X2),X0) ) ) ) ) ),
inference(flattening,[],[f281]) ).
fof(f294,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssList(X1)
| ( ( nil != app(X0,X1)
| ( nil = X0
& nil = X1 ) )
& ( nil != X0
| nil != X1
| nil = app(X0,X1) ) ) ) ),
inference(nnf_transformation,[],[f200]) ).
fof(f295,plain,
! [X0] :
( ~ ssList(X0)
| ! [X1] :
( ~ ssList(X1)
| ( ( nil != app(X0,X1)
| ( nil = X0
& nil = X1 ) )
& ( nil != X0
| nil != X1
| nil = app(X0,X1) ) ) ) ),
inference(flattening,[],[f294]) ).
fof(f301,plain,
( ssList(sK57)
& ssList(sK58)
& ssList(sK59)
& ssList(sK60)
& ( ( nil = sK59
& nil = sK60 )
| sP6(sK59,sK60) )
& ssItem(sK61)
& ssItem(sK62)
& ssList(sK63)
& ssList(sK64)
& ssList(sK65)
& lt(sK62,sK61)
& sK57 = app(app(app(app(sK63,cons(sK61,nil)),sK64),cons(sK62,nil)),sK65)
& sK57 = sK59
& sK58 = sK60 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK57,sK58,sK59,sK60,sK61,sK62,sK63,sK64,sK65]),skolemize(X0,sK57),skolemize(X1,sK58),skolemize(X2,sK59),skolemize(X3,sK60),skolemize(X4,sK61),skolemize(X5,sK62),skolemize(X6,sK63),skolemize(X7,sK64),skolemize(X8,sK65)],[f233]) ).
fof(f310,plain,
! [X2,X3,X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| app(X2,cons(X1,X3)) != X0
| ~ ssList(X3)
| ~ ssList(X2)
| memberP(X0,X1) ),
inference(cnf_transformation,[],[f238]) ).
fof(f316,plain,
! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| app(X1,X2) != X0
| ~ ssList(X2)
| frontsegP(X0,X1) ),
inference(cnf_transformation,[],[f244]) ).
fof(f393,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| ssList(cons(X1,X0)) ),
inference(cnf_transformation,[],[f119]) ).
fof(f394,plain,
ssList(nil),
inference(cnf_transformation,[],[f17]) ).
fof(f395,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| cons(X1,X0) != X0 ),
inference(cnf_transformation,[],[f120]) ).
fof(f406,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ssList(app(X0,X1)) ),
inference(cnf_transformation,[],[f132]) ).
fof(f408,plain,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
inference(cnf_transformation,[],[f134]) ).
fof(f420,plain,
! [X2,X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ memberP(X1,X0)
| memberP(app(X1,X2),X0) ),
inference(cnf_transformation,[],[f280]) ).
fof(f421,plain,
! [X2,X0,X1] :
( ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ memberP(cons(X1,X2),X0)
| memberP(X2,X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f282]) ).
fof(f424,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[],[f148]) ).
fof(f427,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f152]) ).
fof(f482,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| cons(X1,X0) = app(cons(X1,nil),X0) ),
inference(cnf_transformation,[],[f198]) ).
fof(f484,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| nil != app(X0,X1)
| nil = X0 ),
inference(cnf_transformation,[],[f295]) ).
fof(f485,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| nil != app(X0,X1)
| nil = X1 ),
inference(cnf_transformation,[],[f295]) ).
fof(f508,plain,
ssList(sK57),
inference(cnf_transformation,[],[f301]) ).
fof(f509,plain,
ssList(sK58),
inference(cnf_transformation,[],[f301]) ).
fof(f512,plain,
( nil = sK59
| sP6(sK59,sK60) ),
inference(cnf_transformation,[],[f301]) ).
fof(f513,plain,
( nil = sK60
| sP6(sK59,sK60) ),
inference(cnf_transformation,[],[f301]) ).
fof(f514,plain,
ssItem(sK61),
inference(cnf_transformation,[],[f301]) ).
fof(f515,plain,
ssItem(sK62),
inference(cnf_transformation,[],[f301]) ).
fof(f516,plain,
ssList(sK63),
inference(cnf_transformation,[],[f301]) ).
fof(f517,plain,
ssList(sK64),
inference(cnf_transformation,[],[f301]) ).
fof(f518,plain,
ssList(sK65),
inference(cnf_transformation,[],[f301]) ).
fof(f519,plain,
lt(sK62,sK61),
inference(cnf_transformation,[],[f301]) ).
fof(f520,plain,
sK57 = app(app(app(app(sK63,cons(sK61,nil)),sK64),cons(sK62,nil)),sK65),
inference(cnf_transformation,[],[f301]) ).
fof(f521,plain,
sK57 = sK59,
inference(cnf_transformation,[],[f301]) ).
fof(f522,plain,
sK58 = sK60,
inference(cnf_transformation,[],[f301]) ).
fof(f523,plain,
sK59 = app(app(app(app(sK63,cons(sK61,nil)),sK64),cons(sK62,nil)),sK65),
inference(definition_unfolding,[],[f520,f521]) ).
fof(f524,plain,
ssList(sK60),
inference(definition_unfolding,[],[f509,f522]) ).
fof(f525,plain,
ssList(sK59),
inference(definition_unfolding,[],[f508,f521]) ).
fof(f527,plain,
! [X2,X3,X1] :
( ~ ssList(app(X2,cons(X1,X3)))
| ~ ssItem(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| memberP(app(X2,cons(X1,X3)),X1) ),
inference(equality_resolution,[],[f310]) ).
fof(f529,plain,
! [X2,X1] :
( ~ ssList(app(X1,X2))
| ~ ssList(X1)
| ~ ssList(X2)
| frontsegP(app(X1,X2),X1) ),
inference(equality_resolution,[],[f316]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X0,cons(X1,X2)),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(app(X0,cons(X1,X2))) ),
inference(cnf_transformation,[],[f527]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] :
( frontsegP(app(X0,X1),X0)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1)) ),
inference(cnf_transformation,[],[f529]) ).
tcf(c_140,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f393]) ).
tcf(c_141,plain,
ssList(nil),
inference(cnf_transformation,[],[f394]) ).
tcf(c_142,plain,
! [X0: $i,X1: $i] :
( ~ ssList(X1)
| ~ ssItem(X0)
| ( cons(X0,X1) != X1 ) ),
inference(cnf_transformation,[],[f395]) ).
tcf(c_153,plain,
! [X0: $i,X1: $i] :
( ssList(app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f406]) ).
tcf(c_155,plain,
! [X0: $i] :
( ( app(nil,X0) = X0 )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f408]) ).
tcf(c_165,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X0,X2),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[],[f420]) ).
tcf(c_170,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(X1,X2)
| ( X0 = X2 )
| ~ ssList(X1)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ memberP(cons(X0,X1),X2) ),
inference(cnf_transformation,[],[f421]) ).
tcf(c_171,plain,
! [X0: $i] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[],[f424]) ).
tcf(c_174,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[],[f427]) ).
tcf(c_227,plain,
! [X0: $i,X1: $i] :
( ( app(cons(X0,nil),X1) = cons(X0,X1) )
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f482]) ).
tcf(c_230,plain,
! [X0: $i,X1: $i] :
( ( X1 = nil )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(X0,X1) != nil ) ),
inference(cnf_transformation,[],[f485]) ).
tcf(c_231,plain,
! [X0: $i,X1: $i] :
( ( X0 = nil )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(X0,X1) != nil ) ),
inference(cnf_transformation,[],[f484]) ).
tcf(c_242,plain,
! [X0: $i] :
( ~ ssItem(X0)
| ~ lt(X0,X0) ),
inference(cnf_transformation,[],[f559]) ).
tcf(c_253,negated_conjecture,
app(app(app(app(sK63,cons(sK61,nil)),sK64),cons(sK62,nil)),sK65) = sK59,
inference(cnf_transformation,[],[f523]) ).
tcf(c_254,negated_conjecture,
lt(sK62,sK61),
inference(cnf_transformation,[],[f519]) ).
tcf(c_255,negated_conjecture,
ssList(sK65),
inference(cnf_transformation,[],[f518]) ).
tcf(c_256,negated_conjecture,
ssList(sK64),
inference(cnf_transformation,[],[f517]) ).
tcf(c_257,negated_conjecture,
ssList(sK63),
inference(cnf_transformation,[],[f516]) ).
tcf(c_258,negated_conjecture,
ssItem(sK62),
inference(cnf_transformation,[],[f515]) ).
tcf(c_259,negated_conjecture,
ssItem(sK61),
inference(cnf_transformation,[],[f514]) ).
tcf(c_260,negated_conjecture,
( sP6(sK59,sK60)
| ( nil = sK60 ) ),
inference(cnf_transformation,[],[f513]) ).
tcf(c_261,negated_conjecture,
( sP6(sK59,sK60)
| ( nil = sK59 ) ),
inference(cnf_transformation,[],[f512]) ).
tcf(c_264,negated_conjecture,
ssList(sK60),
inference(cnf_transformation,[],[f524]) ).
tcf(c_265,negated_conjecture,
ssList(sK59),
inference(cnf_transformation,[],[f525]) ).
tcf(c_394,plain,
! [X0: $i,X1: $i] :
( frontsegP(app(X0,X1),X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_61,c_153,c_61]) ).
tcf(c_9226,definition,
iPr_def_10 = sK54(sK59,sK60),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_9227,definition,
iPr_def_11 = cons(iPr_def_10,nil),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_9232,definition,
iPr_def_16 = cons(sK61,nil),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_9233,definition,
iPr_def_17 = app(sK63,iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_9234,definition,
iPr_def_18 = app(iPr_def_17,sK64),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_9235,definition,
iPr_def_19 = cons(sK62,nil),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_9236,definition,
iPr_def_20 = app(iPr_def_18,iPr_def_19),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_9237,definition,
iPr_def_21 = app(iPr_def_20,sK65),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_9252,negated_conjecture,
ssList(sK59),
inference(demodulation,[status(thm)],[c_265]) ).
tcf(c_9253,negated_conjecture,
ssList(sK60),
inference(demodulation,[status(thm)],[c_264]) ).
tcf(c_9254,negated_conjecture,
ssItem(sK61),
inference(demodulation,[status(thm)],[c_259]) ).
tcf(c_9255,negated_conjecture,
ssItem(sK62),
inference(demodulation,[status(thm)],[c_258]) ).
tcf(c_9256,negated_conjecture,
ssList(sK63),
inference(demodulation,[status(thm)],[c_257]) ).
tcf(c_9257,negated_conjecture,
ssList(sK64),
inference(demodulation,[status(thm)],[c_256]) ).
tcf(c_9258,negated_conjecture,
ssList(sK65),
inference(demodulation,[status(thm)],[c_255]) ).
tcf(c_9259,negated_conjecture,
lt(sK62,sK61),
inference(demodulation,[status(thm)],[c_254]) ).
tcf(c_9260,negated_conjecture,
iPr_def_21 = sK59,
inference(demodulation,[status(thm)],[c_253,c_9235,c_9232,c_9233,c_9234,c_9236,c_9237]) ).
tcf(c_12306,plain,
ssList(iPr_def_21),
inference(light_normalisation,[status(thm)],[c_9252,c_9260]) ).
tcf(c_12767,plain,
! [X0: $i] :
( memberP(app(X0,iPr_def_16),sK61)
| ~ ssList(nil)
| ~ ssItem(sK61)
| ~ ssList(X0)
| ~ ssList(app(X0,cons(sK61,nil))) ),
inference(superposition,[status(thm)],[c_9232,c_54]) ).
tcf(c_12768,plain,
! [X0: $i] :
( memberP(app(X0,iPr_def_19),sK62)
| ~ ssList(nil)
| ~ ssItem(sK62)
| ~ ssList(X0)
| ~ ssList(app(X0,cons(sK62,nil))) ),
inference(superposition,[status(thm)],[c_9235,c_54]) ).
tcf(c_12779,plain,
! [X0: $i] :
( memberP(app(X0,iPr_def_19),sK62)
| ~ ssList(nil)
| ~ ssItem(sK62)
| ~ ssList(X0)
| ~ ssList(app(X0,iPr_def_19)) ),
inference(light_normalisation,[status(thm)],[c_12768,c_9235]) ).
tcf(c_12780,plain,
! [X0: $i] :
( memberP(app(X0,iPr_def_19),sK62)
| ~ ssList(X0)
| ~ ssList(app(X0,iPr_def_19)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12779,c_141,c_9255]) ).
tcf(c_12784,plain,
! [X0: $i] :
( memberP(app(X0,iPr_def_16),sK61)
| ~ ssList(nil)
| ~ ssItem(sK61)
| ~ ssList(X0)
| ~ ssList(app(X0,iPr_def_16)) ),
inference(light_normalisation,[status(thm)],[c_12767,c_9232]) ).
tcf(c_12785,plain,
! [X0: $i] :
( memberP(app(X0,iPr_def_16),sK61)
| ~ ssList(X0)
| ~ ssList(app(X0,iPr_def_16)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12784,c_141,c_9254]) ).
tcf(c_12881,plain,
( memberP(iPr_def_20,sK62)
| ~ ssList(iPr_def_18)
| ~ ssList(app(iPr_def_18,iPr_def_19)) ),
inference(superposition,[status(thm)],[c_9236,c_12780]) ).
tcf(c_12882,plain,
( memberP(iPr_def_20,sK62)
| ~ ssList(iPr_def_20)
| ~ ssList(iPr_def_18) ),
inference(light_normalisation,[status(thm)],[c_12881,c_9236]) ).
tcf(c_12892,plain,
( memberP(iPr_def_17,sK61)
| ~ ssList(sK63)
| ~ ssList(app(sK63,iPr_def_16)) ),
inference(superposition,[status(thm)],[c_9233,c_12785]) ).
tcf(c_12893,plain,
( memberP(iPr_def_17,sK61)
| ~ ssList(iPr_def_17)
| ~ ssList(sK63) ),
inference(light_normalisation,[status(thm)],[c_12892,c_9233]) ).
tcf(c_12894,plain,
( memberP(iPr_def_17,sK61)
| ~ ssList(iPr_def_17) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12893,c_9256]) ).
tcf(c_13452,plain,
app(nil,sK60) = sK60,
inference(superposition,[status(thm)],[c_9253,c_155]) ).
tcf(c_13457,plain,
app(nil,iPr_def_21) = iPr_def_21,
inference(superposition,[status(thm)],[c_12306,c_155]) ).
tcf(c_13646,plain,
( ssList(iPr_def_16)
| ~ ssList(nil)
| ~ ssItem(sK61) ),
inference(superposition,[status(thm)],[c_9232,c_140]) ).
tcf(c_13647,plain,
( ssList(iPr_def_19)
| ~ ssList(nil)
| ~ ssItem(sK62) ),
inference(superposition,[status(thm)],[c_9235,c_140]) ).
tcf(c_13657,plain,
ssList(iPr_def_19),
inference(forward_subsumption_resolution,[status(thm)],[c_13647,c_141,c_9255]) ).
tcf(c_13658,plain,
ssList(iPr_def_16),
inference(forward_subsumption_resolution,[status(thm)],[c_13646,c_141,c_9254]) ).
tcf(c_13766,plain,
( ssList(iPr_def_17)
| ~ ssList(iPr_def_16)
| ~ ssList(sK63) ),
inference(superposition,[status(thm)],[c_9233,c_153]) ).
tcf(c_13767,plain,
( ssList(iPr_def_18)
| ~ ssList(iPr_def_17)
| ~ ssList(sK64) ),
inference(superposition,[status(thm)],[c_9234,c_153]) ).
tcf(c_13768,plain,
( ssList(iPr_def_20)
| ~ ssList(iPr_def_19)
| ~ ssList(iPr_def_18) ),
inference(superposition,[status(thm)],[c_9236,c_153]) ).
tcf(c_13798,plain,
( ssList(iPr_def_20)
| ~ ssList(iPr_def_18) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13768,c_13657]) ).
tcf(c_13801,plain,
( ssList(iPr_def_18)
| ~ ssList(iPr_def_17) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13767,c_9257]) ).
tcf(c_13804,plain,
ssList(iPr_def_17),
inference(forward_subsumption_resolution,[status(thm)],[c_13766,c_13658,c_9256]) ).
tcf(c_13805,plain,
ssList(iPr_def_18),
inference(backward_subsumption_resolution,[status(thm)],[c_13801,c_13804]) ).
tcf(c_13806,plain,
ssList(iPr_def_20),
inference(backward_subsumption_resolution,[status(thm)],[c_13798,c_13805]) ).
tcf(c_13855,plain,
memberP(iPr_def_17,sK61),
inference(backward_subsumption_resolution,[status(thm)],[c_12894,c_13804]) ).
tcf(c_13860,plain,
( memberP(iPr_def_20,sK62)
| ~ ssList(iPr_def_20) ),
inference(backward_subsumption_resolution,[status(thm)],[c_12882,c_13805]) ).
tcf(c_13865,plain,
memberP(iPr_def_20,sK62),
inference(forward_subsumption_resolution,[status(thm)],[c_13860,c_13806]) ).
tcf(c_13888,plain,
app(nil,iPr_def_20) = iPr_def_20,
inference(superposition,[status(thm)],[c_13806,c_155]) ).
tcf(c_14597,plain,
( frontsegP(iPr_def_21,iPr_def_20)
| ~ ssList(iPr_def_20)
| ~ ssList(sK65) ),
inference(superposition,[status(thm)],[c_9237,c_394]) ).
tcf(c_14610,plain,
( frontsegP(iPr_def_21,nil)
| ~ ssList(iPr_def_21)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_13457,c_394]) ).
tcf(c_14631,plain,
( frontsegP(iPr_def_20,nil)
| ~ ssList(iPr_def_20)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_13888,c_394]) ).
tcf(c_14632,plain,
frontsegP(iPr_def_20,nil),
inference(forward_subsumption_resolution,[status(thm)],[c_14631,c_13806,c_141]) ).
tcf(c_14645,plain,
frontsegP(iPr_def_21,nil),
inference(forward_subsumption_resolution,[status(thm)],[c_14610,c_12306,c_141]) ).
tcf(c_14655,plain,
frontsegP(iPr_def_21,iPr_def_20),
inference(forward_subsumption_resolution,[status(thm)],[c_14597,c_13806,c_9258]) ).
tcf(c_14857,plain,
( ~ ssList(nil)
| ~ ssItem(sK62)
| ( nil != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_9235,c_142]) ).
tcf(c_14865,plain,
nil != iPr_def_19,
inference(forward_subsumption_resolution,[status(thm)],[c_14857,c_141,c_9255]) ).
tcf(c_16818,plain,
ssList(iPr_def_21),
inference(light_normalisation,[status(thm)],[c_9252,c_9260]) ).
tcf(c_18084,plain,
( ( nil = iPr_def_19 )
| ~ ssList(iPr_def_19)
| ~ ssList(iPr_def_18)
| ( nil != iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_9236,c_230]) ).
tcf(c_18133,plain,
nil != iPr_def_20,
inference(forward_subsumption_resolution,[status(thm)],[c_18084,c_14865,c_13657,c_13805]) ).
tcf(c_18507,plain,
( ( nil = iPr_def_20 )
| ~ ssList(iPr_def_20)
| ~ ssList(sK65)
| ( nil != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_9237,c_231]) ).
tcf(c_18553,plain,
( ( nil = iPr_def_20 )
| ( nil != iPr_def_21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18507,c_13806,c_9258]) ).
tcf(c_19507,plain,
! [X0: $i] :
( memberP(iPr_def_18,X0)
| ~ ssList(iPr_def_17)
| ~ ssList(sK64)
| ~ ssItem(X0)
| ~ memberP(iPr_def_17,X0) ),
inference(superposition,[status(thm)],[c_9234,c_165]) ).
tcf(c_19508,plain,
! [X0: $i] :
( memberP(iPr_def_20,X0)
| ~ ssList(iPr_def_19)
| ~ ssList(iPr_def_18)
| ~ ssItem(X0)
| ~ memberP(iPr_def_18,X0) ),
inference(superposition,[status(thm)],[c_9236,c_165]) ).
tcf(c_19509,plain,
! [X0: $i] :
( memberP(iPr_def_21,X0)
| ~ ssList(iPr_def_20)
| ~ ssList(sK65)
| ~ ssItem(X0)
| ~ memberP(iPr_def_20,X0) ),
inference(superposition,[status(thm)],[c_9237,c_165]) ).
tcf(c_19564,plain,
! [X0: $i] :
( memberP(iPr_def_21,X0)
| ~ ssItem(X0)
| ~ memberP(iPr_def_20,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_19509,c_13806,c_9258]) ).
tcf(c_19568,plain,
! [X0: $i] :
( memberP(iPr_def_20,X0)
| ~ ssItem(X0)
| ~ memberP(iPr_def_18,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_19508,c_13657,c_13805]) ).
tcf(c_19572,plain,
! [X0: $i] :
( memberP(iPr_def_18,X0)
| ~ ssItem(X0)
| ~ memberP(iPr_def_17,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_19507,c_13804,c_9257]) ).
tcf(c_20149,plain,
( ( nil = iPr_def_21 )
| ~ ssList(iPr_def_21)
| ~ ssList(nil)
| ~ frontsegP(nil,iPr_def_21) ),
inference(superposition,[status(thm)],[c_14645,c_174]) ).
tcf(c_20176,plain,
( ( nil = iPr_def_20 )
| ~ ssList(iPr_def_20)
| ~ ssList(nil)
| ~ frontsegP(nil,iPr_def_20) ),
inference(superposition,[status(thm)],[c_14632,c_174]) ).
tcf(c_20177,plain,
~ frontsegP(nil,iPr_def_20),
inference(forward_subsumption_resolution,[status(thm)],[c_20176,c_18133,c_13806,c_141]) ).
tcf(c_20210,plain,
( ( nil = iPr_def_21 )
| ~ frontsegP(nil,iPr_def_21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_20149,c_12306,c_141]) ).
tcf(c_22114,plain,
nil != iPr_def_21,
inference(global_subsumption_just,[status(thm)],[c_18553,c_18133,c_18553]) ).
tcf(c_23726,plain,
( ssList(iPr_def_16)
| ~ ssList(nil)
| ~ ssItem(sK61) ),
inference(superposition,[status(thm)],[c_9232,c_140]) ).
tcf(c_23727,plain,
( ssList(iPr_def_19)
| ~ ssList(nil)
| ~ ssItem(sK62) ),
inference(superposition,[status(thm)],[c_9235,c_140]) ).
tcf(c_23738,plain,
ssList(iPr_def_19),
inference(forward_subsumption_resolution,[status(thm)],[c_23727,c_141,c_9255]) ).
tcf(c_23739,plain,
ssList(iPr_def_16),
inference(forward_subsumption_resolution,[status(thm)],[c_23726,c_141,c_9254]) ).
tcf(c_23848,plain,
( memberP(iPr_def_18,sK61)
| ~ ssItem(sK61) ),
inference(superposition,[status(thm)],[c_13855,c_19572]) ).
tcf(c_23849,plain,
memberP(iPr_def_18,sK61),
inference(forward_subsumption_resolution,[status(thm)],[c_23848,c_9254]) ).
tcf(c_25756,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( X0 = iPr_def_10 )
| ~ ssList(nil)
| ~ ssItem(iPr_def_10)
| ~ ssItem(X0)
| ~ memberP(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_9227,c_170]) ).
tcf(c_25757,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( X0 = iPr_def_10 )
| ~ ssItem(iPr_def_10)
| ~ ssItem(X0)
| ~ memberP(iPr_def_11,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_25756,c_141]) ).
tcf(c_26784,plain,
( ssList(iPr_def_17)
| ~ ssList(iPr_def_16)
| ~ ssList(sK63) ),
inference(superposition,[status(thm)],[c_9233,c_153]) ).
tcf(c_26785,plain,
( ssList(iPr_def_18)
| ~ ssList(iPr_def_17)
| ~ ssList(sK64) ),
inference(superposition,[status(thm)],[c_9234,c_153]) ).
tcf(c_26786,plain,
( ssList(iPr_def_20)
| ~ ssList(iPr_def_19)
| ~ ssList(iPr_def_18) ),
inference(superposition,[status(thm)],[c_9236,c_153]) ).
tcf(c_26822,plain,
( ssList(iPr_def_20)
| ~ ssList(iPr_def_18) ),
inference(forward_subsumption_resolution,[status(thm)],[c_26786,c_23738]) ).
tcf(c_26825,plain,
( ssList(iPr_def_18)
| ~ ssList(iPr_def_17) ),
inference(forward_subsumption_resolution,[status(thm)],[c_26785,c_9257]) ).
tcf(c_26828,plain,
ssList(iPr_def_17),
inference(forward_subsumption_resolution,[status(thm)],[c_26784,c_23739,c_9256]) ).
tcf(c_26829,plain,
ssList(iPr_def_18),
inference(backward_subsumption_resolution,[status(thm)],[c_26825,c_26828]) ).
tcf(c_26830,plain,
ssList(iPr_def_20),
inference(backward_subsumption_resolution,[status(thm)],[c_26822,c_26829]) ).
tcf(c_35512,plain,
( ~ ssList(nil)
| ~ ssItem(sK62)
| ( nil != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_9235,c_142]) ).
tcf(c_35520,plain,
nil != iPr_def_19,
inference(forward_subsumption_resolution,[status(thm)],[c_35512,c_141,c_9255]) ).
tcf(c_52945,plain,
( ( nil = iPr_def_19 )
| ~ ssList(iPr_def_19)
| ~ ssList(iPr_def_18)
| ( nil != iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_9236,c_230]) ).
tcf(c_52978,plain,
nil != iPr_def_20,
inference(forward_subsumption_resolution,[status(thm)],[c_52945,c_35520,c_23738,c_26829]) ).
tcf(c_67419,plain,
( memberP(iPr_def_20,sK61)
| ~ ssItem(sK61) ),
inference(superposition,[status(thm)],[c_23849,c_19568]) ).
tcf(c_67420,plain,
memberP(iPr_def_20,sK61),
inference(forward_subsumption_resolution,[status(thm)],[c_67419,c_9254]) ).
fof(f232,definition,
! [X2,X3] :
( ~ sP6(X2,X3)
| ? [X9] :
( ssItem(X9)
& ? [X10] :
( ssList(X10)
& ? [X11] :
( ssList(X11)
& ! [X13] :
( ~ lt(X13,X9)
| ~ memberP(X11,X13)
| ~ ssItem(X13) )
& ! [X12] :
( ~ lt(X9,X12)
| ~ memberP(X10,X12)
| ~ ssItem(X12) )
& app(app(X10,X2),X11) = X3
& cons(X9,nil) = X2 ) ) ) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f233,plain,
? [X0] :
( ssList(X0)
& ? [X1] :
( ssList(X1)
& ? [X2] :
( ssList(X2)
& ? [X3] :
( ssList(X3)
& ( ( nil = X2
& nil = X3 )
| sP6(X2,X3) )
& ? [X4] :
( ssItem(X4)
& ? [X5] :
( ssItem(X5)
& ? [X6] :
( ssList(X6)
& ? [X7] :
( ssList(X7)
& ? [X8] :
( ssList(X8)
& lt(X5,X4)
& app(app(app(app(X6,cons(X4,nil)),X7),cons(X5,nil)),X8) = X0 ) ) ) ) )
& X0 = X2
& X1 = X3 ) ) ) ),
inference(definition_folding,[],[f222,f232]) ).
fof(f298,plain,
! [X2,X3] :
( ~ sP6(X2,X3)
| ? [X9] :
( ssItem(X9)
& ? [X10] :
( ssList(X10)
& ? [X11] :
( ssList(X11)
& ! [X13] :
( ~ lt(X13,X9)
| ~ memberP(X11,X13)
| ~ ssItem(X13) )
& ! [X12] :
( ~ lt(X9,X12)
| ~ memberP(X10,X12)
| ~ ssItem(X12) )
& app(app(X10,X2),X11) = X3
& cons(X9,nil) = X2 ) ) ) ),
inference(nnf_transformation,[],[f232]) ).
fof(f299,plain,
! [X0,X1] :
( ~ sP6(X0,X1)
| ? [X2] :
( ssItem(X2)
& ? [X3] :
( ssList(X3)
& ? [X4] :
( ssList(X4)
& ! [X6] :
( ~ lt(X6,X2)
| ~ memberP(X4,X6)
| ~ ssItem(X6) )
& ! [X5] :
( ~ lt(X2,X5)
| ~ memberP(X3,X5)
| ~ ssItem(X5) )
& app(app(X3,X0),X4) = X1
& cons(X2,nil) = X0 ) ) ) ),
inference(rectify,[],[f298]) ).
fof(f300,plain,
! [X0,X1] :
( ~ sP6(X0,X1)
| ( ssItem(sK54(X0,X1))
& ssList(sK55(X0,X1))
& ssList(sK56(X0,X1))
& ! [X6] :
( ~ lt(X6,sK54(X0,X1))
| ~ memberP(sK56(X0,X1),X6)
| ~ ssItem(X6) )
& ! [X5] :
( ~ lt(sK54(X0,X1),X5)
| ~ memberP(sK55(X0,X1),X5)
| ~ ssItem(X5) )
& app(app(sK55(X0,X1),X0),sK56(X0,X1)) = X1
& cons(sK54(X0,X1),nil) = X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54,sK55,sK56]),skolemize(X2,sK54(X0,X1)),skolemize(X3,sK55(X0,X1)),skolemize(X4,sK56(X0,X1))],[f299]) ).
fof(f501,plain,
! [X0,X1] :
( ~ sP6(X0,X1)
| ssItem(sK54(X0,X1)) ),
inference(cnf_transformation,[],[f300]) ).
fof(f507,plain,
! [X0,X1] :
( ~ sP6(X0,X1)
| cons(sK54(X0,X1),nil) = X0 ),
inference(cnf_transformation,[],[f300]) ).
tcf(c_246,plain,
! [X0: $i,X1: $i] :
( ( cons(sK54(X0,X1),nil) = X0 )
| ~ sP6(X0,X1) ),
inference(cnf_transformation,[],[f507]) ).
tcf(c_252,plain,
! [X0: $i,X1: $i] :
( ssItem(sK54(X0,X1))
| ~ sP6(X0,X1) ),
inference(cnf_transformation,[],[f501]) ).
tcf(c_3314,plain,
! [X0: $i,X1: $i] :
( ssItem(sK54(X0,X1))
| ( nil = sK59 )
| ( X1 != sK60 )
| ( X0 != sK59 ) ),
inference(resolution_lifted,[status(thm)],[c_252,c_261]) ).
tcf(c_3315,plain,
( ssItem(sK54(sK59,sK60))
| ( nil = sK59 ) ),
inference(unflattening,[status(thm)],[c_3314]) ).
tcf(c_3438,plain,
! [X0: $i,X1: $i] :
( ( nil = sK59 )
| ( cons(sK54(X0,X1),nil) = X0 )
| ( X1 != sK60 )
| ( X0 != sK59 ) ),
inference(resolution_lifted,[status(thm)],[c_246,c_261]) ).
tcf(c_3439,plain,
( ( nil = sK59 )
| ( cons(sK54(sK59,sK60),nil) = sK59 ) ),
inference(unflattening,[status(thm)],[c_3438]) ).
tcf(c_3446,plain,
! [X0: $i,X1: $i] :
( ( nil = sK60 )
| ( cons(sK54(X0,X1),nil) = X0 )
| ( X1 != sK60 )
| ( X0 != sK59 ) ),
inference(resolution_lifted,[status(thm)],[c_246,c_260]) ).
tcf(c_3447,plain,
( ( nil = sK60 )
| ( cons(sK54(sK59,sK60),nil) = sK59 ) ),
inference(unflattening,[status(thm)],[c_3446]) ).
tcf(c_9238,plain,
( ( iPr_def_11 = sK59 )
| ( nil = sK60 ) ),
inference(demodulation,[status(thm)],[c_3447,c_9226,c_9227]) ).
tcf(c_9239,plain,
( ( iPr_def_11 = sK59 )
| ( nil = sK59 ) ),
inference(demodulation,[status(thm)],[c_3439]) ).
tcf(c_9251,plain,
( ssItem(iPr_def_10)
| ( nil = sK59 ) ),
inference(demodulation,[status(thm)],[c_3315]) ).
tcf(c_12331,plain,
( ssItem(iPr_def_10)
| ( nil = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_9251,c_9260]) ).
tcf(c_12338,plain,
( ( iPr_def_11 = iPr_def_21 )
| ( nil = sK60 ) ),
inference(light_normalisation,[status(thm)],[c_9238,c_9260]) ).
tcf(c_12354,plain,
( ( iPr_def_11 = iPr_def_21 )
| ( nil = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_9239,c_9260]) ).
tcf(c_13707,plain,
( ( iPr_def_11 = iPr_def_21 )
| ( app(iPr_def_21,sK60) = sK60 ) ),
inference(superposition,[status(thm)],[c_12354,c_13452]) ).
tcf(c_14625,plain,
( frontsegP(sK60,iPr_def_21)
| ( iPr_def_11 = iPr_def_21 )
| ~ ssList(iPr_def_21)
| ~ ssList(sK60) ),
inference(superposition,[status(thm)],[c_13707,c_394]) ).
tcf(c_14662,plain,
( frontsegP(sK60,iPr_def_21)
| ( iPr_def_11 = iPr_def_21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14625,c_12306,c_9253]) ).
tcf(c_15819,plain,
( frontsegP(nil,iPr_def_21)
| ( iPr_def_11 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_12338,c_14662]) ).
tcf(c_16866,plain,
( ( iPr_def_11 = iPr_def_21 )
| ( nil = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_9239,c_9260]) ).
tcf(c_17770,plain,
( ( iPr_def_11 = iPr_def_21 )
| ( cons(sK62,iPr_def_21) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_16866,c_9235]) ).
tcf(c_21132,plain,
( ( iPr_def_11 = iPr_def_21 )
| ~ frontsegP(iPr_def_21,iPr_def_20) ),
inference(superposition,[status(thm)],[c_12354,c_20177]) ).
tcf(c_21133,plain,
iPr_def_11 = iPr_def_21,
inference(forward_subsumption_resolution,[status(thm)],[c_21132,c_14655]) ).
tcf(c_21172,plain,
( ssItem(iPr_def_10)
| ( nil = iPr_def_11 ) ),
inference(demodulation,[status(thm)],[c_12331,c_21133]) ).
tcf(c_21176,plain,
ssList(iPr_def_11),
inference(demodulation,[status(thm)],[c_12306,c_21133]) ).
tcf(c_22116,plain,
nil != iPr_def_11,
inference(light_normalisation,[status(thm)],[c_22114,c_21133]) ).
tcf(c_23828,plain,
! [X0: $i] :
( memberP(iPr_def_11,X0)
| ~ ssItem(X0)
| ~ memberP(iPr_def_20,X0) ),
inference(light_normalisation,[status(thm)],[c_19564,c_21133]) ).
tcf(c_23838,plain,
( memberP(iPr_def_11,sK62)
| ~ ssItem(sK62) ),
inference(superposition,[status(thm)],[c_13865,c_23828]) ).
tcf(c_23839,plain,
memberP(iPr_def_11,sK62),
inference(forward_subsumption_resolution,[status(thm)],[c_23838,c_9255]) ).
tcf(c_28002,plain,
ssItem(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_21172,c_22116]) ).
tcf(c_28005,plain,
! [X0: $i] :
( ( app(cons(iPr_def_10,nil),X0) = cons(iPr_def_10,X0) )
| ~ ssList(X0) ),
inference(superposition,[status(thm)],[c_28002,c_227]) ).
tcf(c_28012,plain,
! [X0: $i] :
( ( cons(iPr_def_10,X0) = app(iPr_def_11,X0) )
| ~ ssList(X0) ),
inference(light_normalisation,[status(thm)],[c_28005,c_9227]) ).
tcf(c_35516,plain,
( ( iPr_def_11 = iPr_def_21 )
| ~ ssList(iPr_def_21)
| ~ ssItem(sK62)
| ( iPr_def_19 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_17770,c_142]) ).
tcf(c_35522,plain,
( ( iPr_def_11 = iPr_def_21 )
| ( iPr_def_19 != iPr_def_21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_35516,c_16818,c_9255]) ).
tcf(c_40272,plain,
iPr_def_11 = iPr_def_21,
inference(global_subsumption_just,[status(thm)],[c_35522,c_15819,c_18133,c_18553,c_20210]) ).
tcf(c_40293,plain,
app(iPr_def_20,sK65) = iPr_def_11,
inference(demodulation,[status(thm)],[c_9237,c_40272]) ).
tcf(c_67498,plain,
( memberP(iPr_def_11,sK61)
| ~ ssItem(sK61) ),
inference(superposition,[status(thm)],[c_67420,c_23828]) ).
tcf(c_67499,plain,
memberP(iPr_def_11,sK61),
inference(forward_subsumption_resolution,[status(thm)],[c_67498,c_9254]) ).
tcf(c_83511,plain,
( ( nil = iPr_def_20 )
| ~ ssList(iPr_def_20)
| ~ ssList(sK65)
| ( nil != iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_40293,c_231]) ).
tcf(c_83523,plain,
nil != iPr_def_11,
inference(forward_subsumption_resolution,[status(thm)],[c_83511,c_52978,c_26830,c_9258]) ).
tcf(c_153088,plain,
cons(iPr_def_10,sK65) = app(iPr_def_11,sK65),
inference(superposition,[status(thm)],[c_9258,c_28012]) ).
tcf(c_154137,plain,
! [X0: $i] :
( memberP(cons(iPr_def_10,sK65),X0)
| ~ ssList(iPr_def_11)
| ~ ssList(sK65)
| ~ ssItem(X0)
| ~ memberP(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_153088,c_165]) ).
tcf(c_154180,plain,
! [X0: $i] :
( memberP(cons(iPr_def_10,sK65),X0)
| ~ ssItem(X0)
| ~ memberP(iPr_def_11,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_154137,c_21176,c_9258]) ).
tcf(c_156552,plain,
! [X0: $i] :
( memberP(sK65,X0)
| ( X0 = iPr_def_10 )
| ~ ssList(sK65)
| ~ ssItem(iPr_def_10)
| ~ ssItem(X0)
| ~ memberP(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_154180,c_170]) ).
tcf(c_156553,plain,
! [X0: $i] :
( memberP(sK65,X0)
| ( X0 = iPr_def_10 )
| ~ ssItem(X0)
| ~ memberP(iPr_def_11,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_156552,c_9258,c_28002]) ).
tcf(c_157618,plain,
! [X0: $i] :
( ~ memberP(iPr_def_11,X0)
| ~ ssItem(X0)
| ( X0 = iPr_def_10 ) ),
inference(global_subsumption_just,[status(thm)],[c_156553,c_171,c_21172,c_25757,c_83523]) ).
tcf(c_157619,plain,
! [X0: $i] :
( ( X0 = iPr_def_10 )
| ~ ssItem(X0)
| ~ memberP(iPr_def_11,X0) ),
inference(renaming,[status(thm)],[c_157618]) ).
tcf(c_157628,plain,
( ( sK62 = iPr_def_10 )
| ~ ssItem(sK62) ),
inference(superposition,[status(thm)],[c_23839,c_157619]) ).
tcf(c_157630,plain,
( ( sK61 = iPr_def_10 )
| ~ ssItem(sK61) ),
inference(superposition,[status(thm)],[c_67499,c_157619]) ).
tcf(c_157633,plain,
sK61 = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_157630,c_9254]) ).
tcf(c_157634,plain,
sK62 = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_157628,c_9255]) ).
tcf(c_157998,plain,
lt(sK62,iPr_def_10),
inference(demodulation,[status(thm)],[c_9259,c_157633]) ).
tcf(c_159339,plain,
lt(iPr_def_10,iPr_def_10),
inference(light_normalisation,[status(thm)],[c_157998,c_157634]) ).
tcf(c_159344,plain,
~ ssItem(iPr_def_10),
inference(superposition,[status(thm)],[c_159339,c_242]) ).
tcf(c_159345,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_159344,c_28002]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWC299+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.03/5.72 % Computer : n012.cluster.edu
% 0.03/5.72 % Model : x86_64 x86_64
% 0.03/5.72 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/5.72 % Memory : 8046.5625MB
% 0.03/5.72 % OS : Linux 6.8.0-71-generic
% 0.03/5.72 % CPULimit : 300
% 0.03/5.72 % WCLimit : 300
% 0.03/5.72 % DateTime : Thu Sep 24 17:29:25 UTC 2026
% 0.03/5.73 % CPUTime :
% 0.03/5.73 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.03/5.75 Running first-order theorem proving
% 0.03/5.75 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/5.75
% 0.03/5.75 % ======== iProver multi-core TPTP/SMT =========
% 0.03/5.75
% 0.03/5.75 % Detected problem language: tptp
% 0.03/5.76 % Proving...
% 37.71/12.06 % SZS status Started for theBenchmark.p
% 37.71/12.06 % SZS status Theorem for theBenchmark.p
% 37.71/12.06
% 37.71/12.06 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 37.71/12.06
% 37.71/12.06 % ------ iProver source info
% 37.71/12.06
% 37.71/12.06 % git: date: 2026-07-19 20:42:38 +0200
% 37.71/12.06 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 37.71/12.06 % git: non_committed_changes: false
% 37.71/12.06
% 37.71/12.06 % ------ Parsing...
% 37.71/12.06 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 37.71/12.06
% 37.71/12.06 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 0 sf_s rm: 5 0s sf_e pe_s pe_e %
% 37.71/12.06
% 37.71/12.06 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 37.71/12.06
% 37.71/12.06 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 37.71/12.06 % ------ Proving...
% 37.71/12.06 % ------ Problem Properties
% 37.71/12.06
% 37.71/12.06 %
% 37.71/12.06 % clauses 215
% 37.71/12.06 % conjectures 9
% 37.71/12.06 % EPR 72
% 37.71/12.06 % Horn 137
% 37.71/12.06 % unary 37
% 37.71/12.06 % binary 50
% 37.71/12.06 % lits 675
% 37.71/12.06 % lits eq 109
% 37.71/12.06 % fd_pure 0
% 37.71/12.06 % fd_pseudo 0
% 37.71/12.06 % fd_cond 21
% 37.71/12.06 % fd_pseudo_cond 14
% 37.71/12.06 % AC symbols 0
% 37.71/12.06
% 37.71/12.06 % ------ Schedule dynamic 5 is on
% 37.71/12.06
% 37.71/12.06 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 37.71/12.06
% 37.71/12.06
% 37.71/12.06 % ------
% 37.71/12.06 % Current options:
% 37.71/12.06 % ------
% 37.71/12.06
% 37.71/12.06
% 37.71/12.06 %
% 37.71/12.06
% 37.71/12.06 % ------ Proving...
% 37.71/12.06 %
% 37.71/12.06
% 37.71/12.06 % SZS status Theorem for theBenchmark.p
% 37.71/12.06
% 37.71/12.06 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 37.71/12.06
% 37.71/12.06
%------------------------------------------------------------------------------