%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWC152-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n013.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:08:06 PM UTC 2026
% Result : Unsatisfiable 85.37s 14.40s
% Output : CNFRefutation 76.40s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f257ERROR: Could not build tree for root c_211751ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f50,axiom,
! [X0,X1] : ssList(skaf46(X0,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause50) ).
fof(f51,axiom,
! [X0,X1] : ssList(skaf45(X0,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause51) ).
fof(f55,axiom,
! [X0] :
( geq(X0,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause55) ).
fof(f58,axiom,
! [X0] :
( rearsegP(X0,nil)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause58) ).
fof(f62,axiom,
! [X0] :
( leq(X0,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause62) ).
fof(f71,axiom,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause71) ).
fof(f72,axiom,
! [X0,X1] :
( ssItem(X1)
| duplicatefreeP(X0)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f73,axiom,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause73) ).
fof(f83,axiom,
! [X0] :
( frontsegP(nil,X0)
| ~ ssList(X0)
| nil != X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause83) ).
fof(f84,axiom,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause84) ).
fof(f85,axiom,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause86) ).
fof(f98,axiom,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != nil ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause98) ).
fof(f99,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| nil != cons(X0,X1) ),
inference(reorient_equations,[],[f98]) ).
fof(f110,axiom,
! [X0,X1] :
( leq(X1,X0)
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ geq(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause107) ).
fof(f121,axiom,
! [X0,X1] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause118) ).
fof(f122,plain,
! [X0,X1] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(X1)
| nil != app(X0,X1) ),
inference(reorient_equations,[],[f121]) ).
fof(f123,axiom,
! [X0,X1] :
( nil = X1
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause119) ).
fof(f124,plain,
! [X0,X1] :
( nil = X1
| ~ ssList(X0)
| ~ ssList(X1)
| nil != app(X0,X1) ),
inference(reorient_equations,[],[f123]) ).
fof(f125,axiom,
! [X0,X1] :
( app(cons(X0,nil),X1) = cons(X0,X1)
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause120) ).
fof(f126,plain,
! [X0,X1] :
( cons(X0,X1) = app(cons(X0,nil),X1)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(reorient_equations,[],[f125]) ).
fof(f132,axiom,
! [X0,X1] :
( X1 = X0
| ~ ssItem(X1)
| ~ ssItem(X0)
| ~ geq(X1,X0)
| ~ geq(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause126) ).
fof(f133,plain,
! [X0,X1] :
( X0 = X1
| ~ ssItem(X1)
| ~ ssItem(X0)
| ~ geq(X1,X0)
| ~ geq(X0,X1) ),
inference(reorient_equations,[],[f132]) ).
fof(f136,axiom,
! [X0,X1] :
( X1 = X0
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X1,X0)
| ~ rearsegP(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause128) ).
fof(f137,plain,
! [X0,X1] :
( X0 = X1
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X1,X0)
| ~ rearsegP(X0,X1) ),
inference(reorient_equations,[],[f136]) ).
fof(f140,axiom,
! [X0,X1] :
( X1 = X0
| ~ ssItem(X1)
| ~ ssItem(X0)
| ~ leq(X1,X0)
| ~ leq(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause130) ).
fof(f141,plain,
! [X0,X1] :
( X0 = X1
| ~ ssItem(X1)
| ~ ssItem(X0)
| ~ leq(X1,X0)
| ~ leq(X0,X1) ),
inference(reorient_equations,[],[f140]) ).
fof(f142,axiom,
! [X0,X1] :
( app(skaf46(X0,X1),X1) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause131) ).
fof(f143,axiom,
! [X0,X1] :
( app(X1,skaf45(X0,X1)) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause132) ).
fof(f148,axiom,
! [X2,X0,X1] :
( frontsegP(app(X0,X2),X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause137) ).
fof(f151,axiom,
! [X2,X0,X1] :
( memberP(app(X0,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ memberP(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause140) ).
fof(f152,axiom,
! [X2,X0,X1] :
( memberP(app(X2,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause141) ).
fof(f154,axiom,
! [X2,X0,X1] :
( rearsegP(X2,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause143) ).
fof(f155,axiom,
! [X2,X0,X1] :
( frontsegP(X2,X0)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause144) ).
fof(f168,axiom,
! [X2,X0,X1] :
( leq(X0,X2)
| ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssItem(X2)
| ~ leq(X1,X2)
| ~ leq(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause156) ).
fof(f170,axiom,
! [X2,X0,X1] :
( memberP(X0,X2)
| memberP(X1,X2)
| ~ ssItem(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ memberP(app(X0,X1),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause158) ).
fof(f173,axiom,
! [X2,X0,X1] :
( X2 = X0
| memberP(X1,X2)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause161) ).
fof(f174,plain,
! [X2,X0,X1] :
( X0 = X2
| memberP(X1,X2)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
inference(reorient_equations,[],[f173]) ).
fof(f183,axiom,
! [X2,X3,X0,X1] :
( X0 = X2
| ~ ssList(X1)
| ~ ssList(X3)
| ~ ssItem(X0)
| ~ ssItem(X2)
| cons(X0,X1) != cons(X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause170) ).
fof(f193,axiom,
! [X2,X3,X0,X1,X4] :
( ~ ssList(X4)
| ~ duplicatefreeP(X4)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(X3)
| app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(f202,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_3) ).
fof(f203,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_4) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
ssItem(sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
ssList(sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_10) ).
fof(f210,negated_conjecture,
ssList(sk9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).
fof(f211,negated_conjecture,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_12) ).
fof(f212,plain,
sk1 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(reorient_equations,[],[f211]) ).
fof(f213,negated_conjecture,
leq(sk6,sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_13) ).
fof(f215,negated_conjecture,
( ~ leq(sk5,sk6)
| memberP(sk8,sk10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_15) ).
fof(f216,negated_conjecture,
( ~ leq(sk5,sk6)
| ~ leq(sk10,sk6)
| ~ leq(sk5,sk10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_16) ).
fof(f218,negated_conjecture,
( nil = sk3
| ssItem(sk11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_18) ).
fof(f219,negated_conjecture,
( nil = sk4
| cons(sk11,nil) = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_19) ).
fof(f220,plain,
( nil = sk4
| sk3 = cons(sk11,nil) ),
inference(reorient_equations,[],[f219]) ).
fof(f223,negated_conjecture,
( nil = sk3
| cons(sk11,nil) = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_22) ).
fof(f224,plain,
( nil = sk3
| sk3 = cons(sk11,nil) ),
inference(reorient_equations,[],[f223]) ).
fof(f225,negated_conjecture,
( nil = sk3
| memberP(sk4,sk11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_23) ).
fof(f226,negated_conjecture,
! [X0] :
( nil = sk3
| ~ leq(sk11,X0)
| ~ memberP(sk4,X0)
| sk11 = X0
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_24) ).
fof(f229,plain,
sk3 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(definition_unfolding,[],[f212,f205]) ).
fof(f232,plain,
( frontsegP(nil,nil)
| ~ ssList(nil) ),
inference(equality_resolution,[],[f83]) ).
fof(f240,plain,
! [X0,X1] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(equality_resolution,[],[f154]) ).
fof(f241,plain,
! [X0,X1] :
( frontsegP(app(X0,X1),X0)
| ~ ssList(app(X0,X1))
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(equality_resolution,[],[f155]) ).
fof(f247,plain,
! [X2,X3,X0,X1] :
( ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssList(X3) ),
inference(equality_resolution,[],[f193]) ).
tcf(c_265,plain,
ssList(nil),
inference(cnf_transformation,[],[f8]) ).
tcf(c_307,plain,
! [X0: $i,X1: $i] : ssList(skaf46(X0,X1)),
inference(cnf_transformation,[],[f50]) ).
tcf(c_308,plain,
! [X0: $i,X1: $i] : ssList(skaf45(X0,X1)),
inference(cnf_transformation,[],[f51]) ).
tcf(c_312,plain,
! [X0: $i] :
( geq(X0,X0)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_315,plain,
! [X0: $i] :
( rearsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_319,plain,
! [X0: $i] :
( leq(X0,X0)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_328,plain,
! [X0: $i] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_329,plain,
! [X0: $i,X1: $i] :
( duplicatefreeP(X0)
| ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_330,plain,
! [X0: $i] :
( ( app(X0,nil) = X0 )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_340,plain,
( frontsegP(nil,nil)
| ~ ssList(nil) ),
inference(cnf_transformation,[],[f232]) ).
tcf(c_341,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(X0)
| ~ frontsegP(nil,X0) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_342,plain,
! [X0: $i,X1: $i] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_343,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_355,plain,
! [X0: $i,X1: $i] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ( cons(X0,X1) != nil ) ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_364,plain,
! [X0: $i,X1: $i] :
( leq(X1,X0)
| ~ ssItem(X1)
| ~ ssItem(X0)
| ~ geq(X0,X1) ),
inference(cnf_transformation,[],[f110]) ).
tcf(c_375,plain,
! [X0: $i,X1: $i] :
( ( X0 = nil )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(X0,X1) != nil ) ),
inference(cnf_transformation,[],[f122]) ).
tcf(c_376,plain,
! [X0: $i,X1: $i] :
( ( X1 = nil )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(X0,X1) != nil ) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_377,plain,
! [X0: $i,X1: $i] :
( ( app(cons(X1,nil),X0) = cons(X1,X0) )
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_383,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ ssItem(X1)
| ~ ssItem(X0)
| ~ geq(X1,X0)
| ~ geq(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
tcf(c_385,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X1,X0)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[],[f137]) ).
tcf(c_387,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ ssItem(X1)
| ~ ssItem(X0)
| ~ leq(X1,X0)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[],[f141]) ).
tcf(c_388,plain,
! [X0: $i,X1: $i] :
( ( app(skaf46(X0,X1),X1) = X0 )
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[],[f142]) ).
tcf(c_389,plain,
! [X0: $i,X1: $i] :
( ( app(X1,skaf45(X0,X1)) = X0 )
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[],[f143]) ).
tcf(c_394,plain,
! [X0: $i,X1: $i,X2: $i] :
( frontsegP(app(X0,X2),X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[],[f148]) ).
tcf(c_395,plain,
! [X0: $i,X1: $i] :
( memberP(cons(X1,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f257]) ).
tcf(c_397,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X0,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[],[f151]) ).
tcf(c_398,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X2,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[],[f152]) ).
tcf(c_400,plain,
! [X0: $i,X1: $i] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1)) ),
inference(cnf_transformation,[],[f240]) ).
tcf(c_401,plain,
! [X0: $i,X1: $i] :
( frontsegP(app(X0,X1),X0)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1)) ),
inference(cnf_transformation,[],[f241]) ).
tcf(c_413,plain,
! [X0: $i,X1: $i,X2: $i] :
( leq(X0,X2)
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ ssItem(X0)
| ~ leq(X1,X2)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[],[f168]) ).
tcf(c_415,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(X1,X2)
| memberP(X0,X2)
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ memberP(app(X0,X1),X2) ),
inference(cnf_transformation,[],[f170]) ).
tcf(c_418,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(X1,X2)
| ( X0 = X2 )
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
inference(cnf_transformation,[],[f174]) ).
tcf(c_427,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X0 = X2 )
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X3)
| ~ ssList(X1)
| ( cons(X0,X1) != cons(X2,X3) ) ),
inference(cnf_transformation,[],[f183]) ).
tcf(c_436,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ssItem(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(cnf_transformation,[],[f247]) ).
tcf(c_445,negated_conjecture,
ssList(sk3),
inference(cnf_transformation,[],[f202]) ).
tcf(c_446,negated_conjecture,
ssList(sk4),
inference(cnf_transformation,[],[f203]) ).
tcf(c_447,negated_conjecture,
ssItem(sk5),
inference(cnf_transformation,[],[f206]) ).
tcf(c_448,negated_conjecture,
ssItem(sk6),
inference(cnf_transformation,[],[f207]) ).
tcf(c_449,negated_conjecture,
ssList(sk7),
inference(cnf_transformation,[],[f208]) ).
tcf(c_450,negated_conjecture,
ssList(sk8),
inference(cnf_transformation,[],[f209]) ).
tcf(c_451,negated_conjecture,
ssList(sk9),
inference(cnf_transformation,[],[f210]) ).
tcf(c_452,negated_conjecture,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk3,
inference(cnf_transformation,[],[f229]) ).
tcf(c_453,negated_conjecture,
leq(sk6,sk5),
inference(cnf_transformation,[],[f213]) ).
tcf(c_455,negated_conjecture,
( memberP(sk8,sk10)
| ~ leq(sk5,sk6) ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_456,negated_conjecture,
( ~ leq(sk10,sk6)
| ~ leq(sk5,sk10)
| ~ leq(sk5,sk6) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_458,negated_conjecture,
( ssItem(sk11)
| ( sk3 = nil ) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_459,negated_conjecture,
( ( sk4 = nil )
| ( cons(sk11,nil) = sk3 ) ),
inference(cnf_transformation,[],[f220]) ).
tcf(c_462,negated_conjecture,
( ( sk3 = nil )
| ( cons(sk11,nil) = sk3 ) ),
inference(cnf_transformation,[],[f224]) ).
tcf(c_463,negated_conjecture,
( memberP(sk4,sk11)
| ( sk3 = nil ) ),
inference(cnf_transformation,[],[f225]) ).
tcf(c_464,negated_conjecture,
! [X0: $i] :
( ( sk3 = nil )
| ( X0 = sk11 )
| ~ ssItem(X0)
| ~ memberP(sk4,X0)
| ~ leq(sk11,X0) ),
inference(cnf_transformation,[],[f226]) ).
tcf(c_525,plain,
( ( nil = nil )
| ~ ssList(nil)
| ~ frontsegP(nil,nil) ),
inference(instantiation,[status(thm)],[c_341]) ).
tcf(c_860,plain,
! [X0: $i,X1: $i] :
( frontsegP(app(X0,X1),X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_401,c_342]) ).
tcf(c_861,plain,
! [X0: $i,X1: $i] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_400,c_342]) ).
tcf(c_6699,plain,
! [X0: $i] :
( ~ iPr_def_10
| ssItem(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_329]) ).
tcf(c_6700,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ ssList(X0)
| duplicatefreeP(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_329]) ).
tcf(c_6701,plain,
( iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_329]) ).
tcf(c_6702,definition,
iPr_def_12 = cons(sk5,nil),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_6703,definition,
iPr_def_13 = app(sk7,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_6704,definition,
iPr_def_14 = app(iPr_def_13,sk8),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_6705,definition,
iPr_def_15 = cons(sk6,nil),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_6706,definition,
iPr_def_16 = app(iPr_def_14,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_6707,definition,
iPr_def_17 = app(iPr_def_16,sk9),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_6708,definition,
iPr_def_18 = cons(sk11,nil),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_6709,negated_conjecture,
iPr_def_17 = sk3,
inference(demodulation,[status(thm)],[c_452,c_6705,c_6702,c_6703,c_6704,c_6706,c_6707]) ).
tcf(c_6710,negated_conjecture,
! [X0: $i] :
( ( sk3 = nil )
| ( X0 = sk11 )
| ~ ssItem(X0)
| ~ memberP(sk4,X0)
| ~ leq(sk11,X0) ),
inference(demodulation,[status(thm)],[c_464]) ).
tcf(c_6711,negated_conjecture,
( memberP(sk4,sk11)
| ( sk3 = nil ) ),
inference(demodulation,[status(thm)],[c_463]) ).
tcf(c_6712,negated_conjecture,
( ( iPr_def_18 = sk3 )
| ( sk3 = nil ) ),
inference(demodulation,[status(thm)],[c_462,c_6708]) ).
tcf(c_6715,negated_conjecture,
( ( iPr_def_18 = sk3 )
| ( sk4 = nil ) ),
inference(demodulation,[status(thm)],[c_459]) ).
tcf(c_6716,negated_conjecture,
( ssItem(sk11)
| ( sk3 = nil ) ),
inference(demodulation,[status(thm)],[c_458]) ).
tcf(c_6718,negated_conjecture,
( ~ leq(sk10,sk6)
| ~ leq(sk5,sk10)
| ~ leq(sk5,sk6) ),
inference(demodulation,[status(thm)],[c_456]) ).
tcf(c_6719,negated_conjecture,
( memberP(sk8,sk10)
| ~ leq(sk5,sk6) ),
inference(demodulation,[status(thm)],[c_455]) ).
tcf(c_6721,negated_conjecture,
leq(sk6,sk5),
inference(demodulation,[status(thm)],[c_453]) ).
tcf(c_6722,negated_conjecture,
ssList(sk9),
inference(demodulation,[status(thm)],[c_451]) ).
tcf(c_6723,negated_conjecture,
ssList(sk8),
inference(demodulation,[status(thm)],[c_450]) ).
tcf(c_6724,negated_conjecture,
ssList(sk7),
inference(demodulation,[status(thm)],[c_449]) ).
tcf(c_6725,negated_conjecture,
ssItem(sk6),
inference(demodulation,[status(thm)],[c_448]) ).
tcf(c_6726,negated_conjecture,
ssItem(sk5),
inference(demodulation,[status(thm)],[c_447]) ).
tcf(c_6727,negated_conjecture,
ssList(sk4),
inference(demodulation,[status(thm)],[c_446]) ).
tcf(c_6728,negated_conjecture,
ssList(sk3),
inference(demodulation,[status(thm)],[c_445]) ).
tcf(c_6729,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_6731,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_6736,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( leq(X0,X2)
| ~ leq(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_6737,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( memberP(X0,X2)
| ~ memberP(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_9377,plain,
ssList(iPr_def_17),
inference(light_normalisation,[status(thm)],[c_6728,c_6709]) ).
tcf(c_9378,plain,
( ssItem(sk11)
| ( nil = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_6716,c_6709]) ).
tcf(c_9389,plain,
( memberP(sk4,sk11)
| ( nil = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_6711,c_6709]) ).
tcf(c_9404,plain,
( ( iPr_def_17 = iPr_def_18 )
| ( nil = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_6712,c_6709]) ).
tcf(c_9446,plain,
( ( iPr_def_17 = iPr_def_18 )
| ( sk4 = nil ) ),
inference(light_normalisation,[status(thm)],[c_6715,c_6709]) ).
tcf(c_9462,plain,
! [X0: $i] :
( ( nil = iPr_def_17 )
| ( X0 = sk11 )
| ~ ssItem(X0)
| ~ memberP(sk4,X0)
| ~ leq(sk11,X0) ),
inference(light_normalisation,[status(thm)],[c_6710,c_6709]) ).
tcf(c_9596,plain,
! [X0: $i] :
( rearsegP(X0,iPr_def_17)
| ( iPr_def_17 = iPr_def_18 )
| ~ ssList(X0) ),
inference(superposition,[status(thm)],[c_9404,c_315]) ).
tcf(c_9733,plain,
app(sk4,nil) = sk4,
inference(superposition,[status(thm)],[c_6727,c_330]) ).
tcf(c_9765,plain,
app(iPr_def_17,nil) = iPr_def_17,
inference(superposition,[status(thm)],[c_9377,c_330]) ).
tcf(c_9858,plain,
( ( iPr_def_17 = iPr_def_18 )
| ( app(sk4,iPr_def_17) = sk4 ) ),
inference(superposition,[status(thm)],[c_9404,c_9733]) ).
tcf(c_10039,plain,
( ssList(iPr_def_13)
| ~ ssList(iPr_def_12)
| ~ ssList(sk7) ),
inference(superposition,[status(thm)],[c_6703,c_342]) ).
tcf(c_10040,plain,
( ssList(iPr_def_14)
| ~ ssList(iPr_def_13)
| ~ ssList(sk8) ),
inference(superposition,[status(thm)],[c_6704,c_342]) ).
tcf(c_10041,plain,
( ssList(iPr_def_16)
| ~ ssList(iPr_def_15)
| ~ ssList(iPr_def_14) ),
inference(superposition,[status(thm)],[c_6706,c_342]) ).
tcf(c_10061,plain,
( ssList(iPr_def_14)
| ~ ssList(iPr_def_13) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10040,c_6723]) ).
tcf(c_10064,plain,
( ssList(iPr_def_13)
| ~ ssList(iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10039,c_6724]) ).
tcf(c_10081,plain,
( ssList(iPr_def_12)
| ~ ssItem(sk5)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6702,c_343]) ).
tcf(c_10082,plain,
( ssList(iPr_def_15)
| ~ ssItem(sk6)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6705,c_343]) ).
tcf(c_10092,plain,
ssList(iPr_def_15),
inference(forward_subsumption_resolution,[status(thm)],[c_10082,c_6725,c_265]) ).
tcf(c_10093,plain,
ssList(iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_10081,c_6726,c_265]) ).
tcf(c_10132,plain,
ssList(iPr_def_14),
inference(global_subsumption_just,[status(thm)],[c_10061,c_10064,c_10061,c_10093]) ).
tcf(c_10136,plain,
ssList(iPr_def_13),
inference(global_subsumption_just,[status(thm)],[c_10064,c_10064,c_10093]) ).
tcf(c_10429,plain,
( frontsegP(iPr_def_16,iPr_def_14)
| ~ ssList(iPr_def_15)
| ~ ssList(iPr_def_14) ),
inference(superposition,[status(thm)],[c_6706,c_860]) ).
tcf(c_10477,plain,
frontsegP(iPr_def_16,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_10429,c_10092,c_10132]) ).
tcf(c_10594,plain,
( rearsegP(iPr_def_17,sk9)
| ~ ssList(iPr_def_16)
| ~ ssList(sk9) ),
inference(superposition,[status(thm)],[c_6707,c_861]) ).
tcf(c_10606,plain,
( rearsegP(iPr_def_17,nil)
| ~ ssList(iPr_def_17)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_9765,c_861]) ).
tcf(c_10607,plain,
( rearsegP(sk4,iPr_def_17)
| ( iPr_def_17 = iPr_def_18 )
| ~ ssList(iPr_def_17)
| ~ ssList(sk4) ),
inference(superposition,[status(thm)],[c_9858,c_861]) ).
tcf(c_10634,plain,
rearsegP(iPr_def_17,nil),
inference(forward_subsumption_resolution,[status(thm)],[c_10606,c_9377,c_265]) ).
tcf(c_10639,plain,
( rearsegP(iPr_def_17,sk9)
| ~ ssList(iPr_def_16) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10594,c_6722]) ).
tcf(c_10651,plain,
( rearsegP(sk4,iPr_def_17)
| ( iPr_def_17 = iPr_def_18 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10607,c_9377,c_6727]) ).
tcf(c_11004,plain,
( ~ ssItem(sk5)
| ~ ssList(nil)
| ( nil != iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_6702,c_355]) ).
tcf(c_11014,plain,
nil != iPr_def_12,
inference(forward_subsumption_resolution,[status(thm)],[c_11004,c_6726,c_265]) ).
tcf(c_11072,plain,
rearsegP(iPr_def_17,sk9),
inference(global_subsumption_just,[status(thm)],[c_10639,c_10064,c_10061,c_10041,c_10093,c_10092,c_10639]) ).
tcf(c_11128,plain,
( rearsegP(nil,iPr_def_17)
| ( iPr_def_17 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_9446,c_10651]) ).
tcf(c_12018,plain,
! [X0: $i,X1: $i] :
( ( app(cons(X1,nil),X0) = cons(X1,X0) )
| ~ iPr_def_10
| ~ ssList(X0) ),
inference(superposition,[status(thm)],[c_6699,c_377]) ).
tcf(c_12143,plain,
( ( nil = iPr_def_13 )
| ~ ssList(iPr_def_13)
| ~ ssList(sk8)
| ( nil != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_6704,c_375]) ).
tcf(c_12144,plain,
( ( nil = iPr_def_14 )
| ~ ssList(iPr_def_15)
| ~ ssList(iPr_def_14)
| ( nil != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_6706,c_375]) ).
tcf(c_12145,plain,
( ( nil = iPr_def_16 )
| ~ ssList(iPr_def_16)
| ~ ssList(sk9)
| ( nil != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_6707,c_375]) ).
tcf(c_12176,plain,
( ( nil = iPr_def_16 )
| ~ ssList(iPr_def_16)
| ( nil != iPr_def_17 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12145,c_6722]) ).
tcf(c_12180,plain,
( ( nil = iPr_def_14 )
| ( nil != iPr_def_16 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12144,c_10092,c_10132]) ).
tcf(c_12183,plain,
( ( nil = iPr_def_13 )
| ( nil != iPr_def_14 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12143,c_10136,c_6723]) ).
tcf(c_12198,plain,
( ( nil = iPr_def_12 )
| ~ ssList(iPr_def_12)
| ~ ssList(sk7)
| ( nil != iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_6703,c_376]) ).
tcf(c_12240,plain,
nil != iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_12198,c_11014,c_10093,c_6724]) ).
tcf(c_12884,plain,
( ( nil = iPr_def_17 )
| ~ ssList(iPr_def_17)
| ~ ssList(nil)
| ~ rearsegP(nil,iPr_def_17) ),
inference(superposition,[status(thm)],[c_10634,c_385]) ).
tcf(c_12888,plain,
( ( sk9 = iPr_def_17 )
| ~ ssList(iPr_def_17)
| ~ ssList(sk9)
| ~ rearsegP(sk9,iPr_def_17) ),
inference(superposition,[status(thm)],[c_11072,c_385]) ).
tcf(c_12926,plain,
( ( sk9 = iPr_def_17 )
| ~ rearsegP(sk9,iPr_def_17) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12888,c_9377,c_6722]) ).
tcf(c_12939,plain,
( ( nil = iPr_def_17 )
| ~ rearsegP(nil,iPr_def_17) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12884,c_9377,c_265]) ).
tcf(c_13335,plain,
( ( iPr_def_17 = iPr_def_18 )
| ( sk9 = iPr_def_17 )
| ~ ssList(sk9) ),
inference(superposition,[status(thm)],[c_9596,c_12926]) ).
tcf(c_13336,plain,
( ( iPr_def_17 = iPr_def_18 )
| ( sk9 = iPr_def_17 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13335,c_6722]) ).
tcf(c_13370,plain,
( ( sk5 = sk6 )
| ~ ssItem(sk6)
| ~ ssItem(sk5)
| ~ leq(sk5,sk6) ),
inference(superposition,[status(thm)],[c_6721,c_387]) ).
tcf(c_13374,plain,
( ( sk5 = sk6 )
| ~ leq(sk5,sk6) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13370,c_6725,c_6726]) ).
tcf(c_13405,plain,
( ( app(skaf46(iPr_def_17,sk9),sk9) = iPr_def_17 )
| ~ ssList(iPr_def_17)
| ~ ssList(sk9) ),
inference(superposition,[status(thm)],[c_11072,c_388]) ).
tcf(c_13451,plain,
app(skaf46(iPr_def_17,sk9),sk9) = iPr_def_17,
inference(forward_subsumption_resolution,[status(thm)],[c_13405,c_9377,c_6722]) ).
tcf(c_13493,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ssItem(sk6)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ duplicatefreeP(app(app(X0,cons(sk6,X1)),cons(sk6,X2)))
| ~ ssList(app(app(X0,cons(sk6,X1)),cons(sk6,X2))) ),
inference(instantiation,[status(thm)],[c_436]) ).
tcf(c_13494,plain,
( ~ ssItem(sk6)
| ~ ssList(nil)
| ~ duplicatefreeP(app(app(nil,cons(sk6,nil)),cons(sk6,nil)))
| ~ ssList(app(app(nil,cons(sk6,nil)),cons(sk6,nil))) ),
inference(instantiation,[status(thm)],[c_13493]) ).
tcf(c_14004,plain,
iPr_def_17 = iPr_def_18,
inference(global_subsumption_just,[status(thm)],[c_13336,c_10064,c_10061,c_10041,c_10093,c_10092,c_11128,c_12183,c_12180,c_12176,c_12240,c_12939]) ).
tcf(c_14041,plain,
cons(sk11,nil) = iPr_def_17,
inference(demodulation,[status(thm)],[c_6708,c_14004]) ).
tcf(c_14155,plain,
! [X0: $i] :
( frontsegP(iPr_def_17,X0)
| ~ ssList(iPr_def_16)
| ~ ssList(sk9)
| ~ ssList(X0)
| ~ frontsegP(iPr_def_16,X0) ),
inference(superposition,[status(thm)],[c_6707,c_394]) ).
tcf(c_14227,plain,
! [X0: $i] :
( frontsegP(iPr_def_17,X0)
| ~ ssList(iPr_def_16)
| ~ ssList(X0)
| ~ frontsegP(iPr_def_16,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14155,c_6722]) ).
tcf(c_14287,plain,
! [X0: $i] :
( memberP(iPr_def_14,X0)
| ~ ssList(iPr_def_13)
| ~ ssList(sk8)
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_6704,c_397]) ).
tcf(c_14289,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ ssList(iPr_def_16)
| ~ ssList(sk9)
| ~ ssItem(X0)
| ~ memberP(iPr_def_16,X0) ),
inference(superposition,[status(thm)],[c_6707,c_397]) ).
tcf(c_14323,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ ssList(iPr_def_16)
| ~ ssItem(X0)
| ~ memberP(iPr_def_16,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14289,c_6722]) ).
tcf(c_14332,plain,
! [X0: $i] :
( memberP(iPr_def_14,X0)
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14287,c_10136,c_6723]) ).
tcf(c_14360,plain,
! [X0: $i] :
( memberP(iPr_def_13,X0)
| ~ ssList(iPr_def_12)
| ~ ssList(sk7)
| ~ ssItem(X0)
| ~ memberP(iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_6703,c_398]) ).
tcf(c_14361,plain,
! [X0: $i] :
( memberP(iPr_def_14,X0)
| ~ ssList(iPr_def_13)
| ~ ssList(sk8)
| ~ ssItem(X0)
| ~ memberP(sk8,X0) ),
inference(superposition,[status(thm)],[c_6704,c_398]) ).
tcf(c_14406,plain,
! [X0: $i] :
( memberP(iPr_def_14,X0)
| ~ ssItem(X0)
| ~ memberP(sk8,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14361,c_10136,c_6723]) ).
tcf(c_14410,plain,
! [X0: $i] :
( memberP(iPr_def_13,X0)
| ~ ssItem(X0)
| ~ memberP(iPr_def_12,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14360,c_10093,c_6724]) ).
tcf(c_15083,plain,
( ( sk9 = nil )
| ~ ssList(sk9)
| ~ ssList(skaf46(iPr_def_17,sk9))
| ( nil != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_13451,c_376]) ).
tcf(c_15092,plain,
( ( sk9 = nil )
| ( nil != iPr_def_17 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15083,c_6722,c_307]) ).
tcf(c_15868,plain,
! [X0: $i] :
( ( X0 = sk6 )
| ~ ssItem(sk6)
| ~ ssItem(X0)
| ~ geq(sk6,X0)
| ~ geq(X0,sk6) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_15905,plain,
nil != iPr_def_17,
inference(global_subsumption_just,[status(thm)],[c_15092,c_10064,c_10061,c_10041,c_10093,c_10092,c_12183,c_12180,c_12176,c_12240]) ).
tcf(c_15907,plain,
! [X0: $i] :
( ( X0 = sk11 )
| ~ ssItem(X0)
| ~ memberP(sk4,X0)
| ~ leq(sk11,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_9462,c_15905]) ).
tcf(c_15908,plain,
memberP(sk4,sk11),
inference(backward_subsumption_resolution,[status(thm)],[c_9389,c_15905]) ).
tcf(c_15909,plain,
ssItem(sk11),
inference(backward_subsumption_resolution,[status(thm)],[c_9378,c_15905]) ).
tcf(c_16262,plain,
( ssList(iPr_def_13)
| ~ ssList(iPr_def_12)
| ~ ssList(sk7) ),
inference(superposition,[status(thm)],[c_6703,c_342]) ).
tcf(c_16281,plain,
( ssList(iPr_def_13)
| ~ ssList(iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_16262,c_6724]) ).
tcf(c_16544,plain,
ssList(iPr_def_13),
inference(global_subsumption_just,[status(thm)],[c_16281,c_10064,c_10093]) ).
tcf(c_17304,plain,
! [X0: $i,X1: $i] :
( duplicatefreeP(skaf46(X0,X1))
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_307,c_6700]) ).
tcf(c_19163,plain,
sk5 = sk5,
inference(instantiation,[status(thm)],[c_6729]) ).
tcf(c_21177,plain,
! [X0: $i,X1: $i] :
( ssList(app(X1,cons(sk6,X0)))
| ~ ssList(X1)
| ~ ssList(cons(sk6,X0)) ),
inference(instantiation,[status(thm)],[c_342]) ).
tcf(c_21178,plain,
( ssList(app(nil,cons(sk6,nil)))
| ~ ssList(nil)
| ~ ssList(cons(sk6,nil)) ),
inference(instantiation,[status(thm)],[c_21177]) ).
tcf(c_22251,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk6 )
| ~ ssItem(sk6)
| ~ ssList(nil)
| ~ ssItem(X0)
| ~ ssList(X1)
| ( cons(X0,X1) != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_6705,c_427]) ).
tcf(c_22258,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk6 )
| ~ ssItem(X0)
| ~ ssList(X1)
| ( cons(X0,X1) != iPr_def_15 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_22251,c_6725,c_265]) ).
tcf(c_26596,plain,
! [X0: $i] :
( frontsegP(iPr_def_17,X0)
| ~ frontsegP(iPr_def_16,X0)
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_14227,c_10064,c_10061,c_10041,c_10093,c_10092,c_14227]) ).
tcf(c_26597,plain,
! [X0: $i] :
( frontsegP(iPr_def_17,X0)
| ~ ssList(X0)
| ~ frontsegP(iPr_def_16,X0) ),
inference(renaming,[status(thm)],[c_26596]) ).
tcf(c_26606,plain,
( frontsegP(iPr_def_17,iPr_def_14)
| ~ ssList(iPr_def_14) ),
inference(superposition,[status(thm)],[c_10477,c_26597]) ).
tcf(c_26607,plain,
frontsegP(iPr_def_17,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_26606,c_10132]) ).
tcf(c_26881,plain,
( ( app(iPr_def_14,skaf45(iPr_def_17,iPr_def_14)) = iPr_def_17 )
| ~ ssList(iPr_def_17)
| ~ ssList(iPr_def_14) ),
inference(superposition,[status(thm)],[c_26607,c_389]) ).
tcf(c_26888,plain,
app(iPr_def_14,skaf45(iPr_def_17,iPr_def_14)) = iPr_def_17,
inference(forward_subsumption_resolution,[status(thm)],[c_26881,c_9377,c_10132]) ).
tcf(c_31771,plain,
( leq(sk6,sk6)
| ~ ssItem(sk6) ),
inference(instantiation,[status(thm)],[c_319]) ).
tcf(c_33546,plain,
! [X0: $i,X1: $i,X2: $i] :
( leq(sk5,X0)
| ~ leq(X2,X1)
| ( sk5 != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_6736]) ).
tcf(c_33745,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ssList(app(app(X0,cons(sk6,X1)),cons(X2,X3)))
| ~ ssList(cons(X2,X3))
| ~ ssList(app(X0,cons(sk6,X1))) ),
inference(instantiation,[status(thm)],[c_342]) ).
tcf(c_34191,plain,
! [X0: $i] :
( ssList(cons(sk6,X0))
| ~ ssItem(sk6)
| ~ ssList(X0) ),
inference(instantiation,[status(thm)],[c_343]) ).
tcf(c_34192,plain,
( ssList(cons(sk6,nil))
| ~ ssItem(sk6)
| ~ ssList(nil) ),
inference(instantiation,[status(thm)],[c_34191]) ).
tcf(c_35901,plain,
( ( sk6 = sk6 )
| ~ ssItem(sk6)
| ~ geq(sk6,sk6) ),
inference(instantiation,[status(thm)],[c_15868]) ).
tcf(c_35902,plain,
( geq(sk6,sk6)
| ~ ssItem(sk6) ),
inference(instantiation,[status(thm)],[c_312]) ).
tcf(c_36073,plain,
! [X0: $i,X1: $i] :
( ( sk6 = X0 )
| ( sk6 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_6731]) ).
tcf(c_42773,plain,
( ( sk6 = sk11 )
| ~ ssItem(sk11)
| ~ ssList(nil)
| ( iPr_def_15 != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_14041,c_22258]) ).
tcf(c_42783,plain,
( ( sk6 = sk11 )
| ( iPr_def_15 != iPr_def_17 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_42773,c_15909,c_265]) ).
tcf(c_44924,plain,
! [X0: $i] :
( memberP(iPr_def_14,X0)
| ~ ssList(iPr_def_13)
| ~ ssList(sk8)
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_6704,c_397]) ).
tcf(c_44926,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ ssList(iPr_def_16)
| ~ ssList(sk9)
| ~ ssItem(X0)
| ~ memberP(iPr_def_16,X0) ),
inference(superposition,[status(thm)],[c_6707,c_397]) ).
tcf(c_44962,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ ssList(iPr_def_16)
| ~ ssItem(X0)
| ~ memberP(iPr_def_16,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_44926,c_6722]) ).
tcf(c_44971,plain,
! [X0: $i] :
( memberP(iPr_def_14,X0)
| ~ ssItem(X0)
| ~ memberP(iPr_def_13,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_44924,c_16544,c_6723]) ).
tcf(c_52213,plain,
! [X0: $i,X1: $i] :
( leq(sk5,X0)
| ~ leq(sk5,X1)
| ( sk5 != sk5 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_33546]) ).
tcf(c_52214,plain,
! [X0: $i,X1: $i] :
( leq(sk5,X0)
| ~ leq(sk6,X1)
| ( sk5 != sk6 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_33546]) ).
tcf(c_55516,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ ssList(iPr_def_14)
| ~ ssItem(X0)
| ~ memberP(iPr_def_14,X0)
| ~ ssList(skaf45(iPr_def_17,iPr_def_14)) ),
inference(superposition,[status(thm)],[c_26888,c_397]) ).
tcf(c_55535,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ ssItem(X0)
| ~ memberP(iPr_def_14,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_55516,c_10132,c_308]) ).
tcf(c_60389,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssList(app(app(X0,cons(sk6,X1)),cons(sk6,X2)))
| ~ ssList(cons(sk6,X2))
| ~ ssList(app(X0,cons(sk6,X1))) ),
inference(instantiation,[status(thm)],[c_33745]) ).
tcf(c_60392,plain,
( ssList(app(app(nil,cons(sk6,nil)),cons(sk6,nil)))
| ~ ssList(cons(sk6,nil))
| ~ ssList(app(nil,cons(sk6,nil))) ),
inference(instantiation,[status(thm)],[c_60389]) ).
tcf(c_61236,plain,
! [X0: $i,X1: $i,X2: $i] :
( duplicatefreeP(app(app(X0,cons(sk6,X1)),cons(sk6,X2)))
| ~ iPr_def_11
| ~ ssList(app(app(X0,cons(sk6,X1)),cons(sk6,X2))) ),
inference(instantiation,[status(thm)],[c_6700]) ).
tcf(c_61237,plain,
( duplicatefreeP(app(app(nil,cons(sk6,nil)),cons(sk6,nil)))
| ~ iPr_def_11
| ~ ssList(app(app(nil,cons(sk6,nil)),cons(sk6,nil))) ),
inference(instantiation,[status(thm)],[c_61236]) ).
tcf(c_61279,plain,
! [X0: $i] :
( memberP(iPr_def_14,X0)
| ~ memberP(iPr_def_13,X0) ),
inference(global_subsumption_just,[status(thm)],[c_44971,c_448,c_265,c_6699,c_6701,c_13494,c_14332,c_21178,c_34192,c_60392,c_61237]) ).
tcf(c_76103,plain,
! [X0: $i] :
( ( sk6 = X0 )
| ( sk6 != sk6 )
| ( X0 != sk6 ) ),
inference(instantiation,[status(thm)],[c_36073]) ).
tcf(c_76378,plain,
! [X0: $i] :
( leq(sk5,sk10)
| ~ leq(sk5,X0)
| ( sk10 != X0 )
| ( sk5 != sk5 ) ),
inference(instantiation,[status(thm)],[c_52213]) ).
tcf(c_77611,plain,
( ssItem(sk10)
| ~ iPr_def_10 ),
inference(instantiation,[status(thm)],[c_6699]) ).
tcf(c_93532,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_17304,c_448,c_265,c_13494,c_21178,c_34192,c_60392,c_61237]) ).
tcf(c_93534,plain,
iPr_def_10,
inference(backward_subsumption_resolution,[status(thm)],[c_6701,c_93532]) ).
tcf(c_93535,plain,
! [X0: $i] : ssItem(X0),
inference(backward_subsumption_resolution,[status(thm)],[c_6699,c_93534]) ).
tcf(c_93551,plain,
! [X0: $i,X1: $i] :
( memberP(cons(X1,X0),X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_395,c_93535]) ).
tcf(c_93552,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(X1,X2)
| ( X0 = X2 )
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
inference(backward_subsumption_resolution,[status(thm)],[c_418,c_93535]) ).
tcf(c_93555,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(X1,X2)
| memberP(X0,X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ memberP(app(X0,X1),X2) ),
inference(backward_subsumption_resolution,[status(thm)],[c_415,c_93535]) ).
tcf(c_93557,plain,
! [X0: $i,X1: $i,X2: $i] :
( leq(X0,X2)
| ~ leq(X1,X2)
| ~ leq(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_413,c_93535]) ).
tcf(c_93562,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X2,X0),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_398,c_93535]) ).
tcf(c_93563,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X0,X2),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_397,c_93535]) ).
tcf(c_93584,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X1,X0))
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_343,c_93535]) ).
tcf(c_97656,plain,
! [X0: $i] :
( leq(sk5,X0)
| ~ leq(sk6,sk6)
| ( sk5 != sk6 )
| ( X0 != sk6 ) ),
inference(instantiation,[status(thm)],[c_52214]) ).
tcf(c_98966,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ memberP(iPr_def_16,X0) ),
inference(global_subsumption_just,[status(thm)],[c_44962,c_448,c_265,c_6699,c_6701,c_10064,c_10061,c_10041,c_10093,c_10092,c_13494,c_14323,c_21178,c_34192,c_60392,c_61237]) ).
tcf(c_99295,plain,
! [X0: $i,X1: $i] :
( leq(sk5,sk6)
| ~ leq(X0,X1)
| ( sk6 != X1 )
| ( sk5 != X0 ) ),
inference(instantiation,[status(thm)],[c_6736]) ).
tcf(c_99296,plain,
! [X0: $i,X1: $i] :
( memberP(X0,X1)
| ~ memberP(sk4,sk11)
| ( X1 != sk11 )
| ( X0 != sk4 ) ),
inference(instantiation,[status(thm)],[c_6737]) ).
tcf(c_99400,plain,
! [X0: $i] :
( leq(sk5,sk6)
| ~ leq(sk5,X0)
| ( sk6 != X0 )
| ( sk5 != sk5 ) ),
inference(instantiation,[status(thm)],[c_99295]) ).
tcf(c_99453,plain,
! [X0: $i] :
( memberP(sk4,X0)
| ~ memberP(sk4,sk11)
| ( sk4 != sk4 )
| ( X0 != sk11 ) ),
inference(instantiation,[status(thm)],[c_99296]) ).
tcf(c_99454,plain,
sk4 = sk4,
inference(instantiation,[status(thm)],[c_6729]) ).
tcf(c_99456,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk4 )
| ( sk4 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_6731]) ).
tcf(c_99457,plain,
( ( nil = sk4 )
| ( nil != nil )
| ( sk4 != nil ) ),
inference(instantiation,[status(thm)],[c_99456]) ).
tcf(c_100461,plain,
! [X0: $i] :
( memberP(X0,sk11)
| ~ memberP(sk4,sk11)
| ( sk11 != sk11 )
| ( X0 != sk4 ) ),
inference(instantiation,[status(thm)],[c_99296]) ).
tcf(c_100462,plain,
sk11 = sk11,
inference(instantiation,[status(thm)],[c_6729]) ).
tcf(c_100463,plain,
( memberP(nil,sk11)
| ~ memberP(sk4,sk11)
| ( sk11 != sk11 )
| ( nil != sk4 ) ),
inference(instantiation,[status(thm)],[c_100461]) ).
tcf(c_100866,plain,
! [X0: $i] :
( leq(sk11,X0)
| ~ ssItem(sk11)
| ~ ssItem(X0)
| ~ geq(X0,sk11) ),
inference(instantiation,[status(thm)],[c_364]) ).
tcf(c_104368,plain,
( leq(sk11,sk11)
| ~ ssItem(sk11)
| ~ geq(sk11,sk11) ),
inference(instantiation,[status(thm)],[c_100866]) ).
tcf(c_104369,plain,
( geq(sk11,sk11)
| ~ ssItem(sk11) ),
inference(instantiation,[status(thm)],[c_312]) ).
tcf(c_104731,plain,
! [X0: $i,X1: $i,X2: $i] :
( leq(X0,sk11)
| ~ leq(X1,X2)
| ( sk11 != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_6736]) ).
tcf(c_110886,plain,
( ~ ssItem(sk11)
| ~ memberP(nil,sk11) ),
inference(instantiation,[status(thm)],[c_328]) ).
tcf(c_114203,plain,
! [X0: $i,X1: $i] :
( leq(X0,sk11)
| ~ leq(X1,sk11)
| ( sk11 != sk11 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_104731]) ).
tcf(c_120568,plain,
! [X0: $i] :
( leq(X0,sk11)
| ~ leq(sk11,sk11)
| ( sk11 != sk11 )
| ( X0 != sk11 ) ),
inference(instantiation,[status(thm)],[c_114203]) ).
tcf(c_124735,plain,
( leq(sk5,sk11)
| ~ leq(sk11,sk11)
| ( sk11 != sk11 )
| ( sk5 != sk11 ) ),
inference(instantiation,[status(thm)],[c_120568]) ).
tcf(c_124739,plain,
( leq(sk5,sk6)
| ~ leq(sk5,sk11)
| ( sk6 != sk11 )
| ( sk5 != sk5 ) ),
inference(instantiation,[status(thm)],[c_99400]) ).
tcf(c_134771,plain,
! [X0: $i] : ~ memberP(nil,X0),
inference(global_subsumption_just,[status(thm)],[c_328,c_448,c_265,c_328,c_6699,c_6701,c_13494,c_21178,c_34192,c_60392,c_61237]) ).
tcf(c_134785,negated_conjecture,
iPr_def_18 = sk3,
inference(global_subsumption_just,[status(thm)],[c_6712,c_265,c_340,c_525,c_6715,c_15909,c_15908,c_99457,c_100463,c_100462,c_110886]) ).
tcf(c_134787,plain,
iPr_def_17 = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_134785,c_6709]) ).
tcf(c_134912,plain,
cons(sk11,nil) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_6708,c_134787]) ).
tcf(c_138813,plain,
! [X0: $i,X1: $i,X2: $i] :
( leq(X0,X2)
| ~ leq(X0,X1)
| ~ leq(X1,X2) ),
inference(global_subsumption_just,[status(thm)],[c_413,c_93557]) ).
tcf(c_138814,plain,
! [X0: $i,X1: $i,X2: $i] :
( leq(X0,X2)
| ~ leq(X1,X2)
| ~ leq(X0,X1) ),
inference(renaming,[status(thm)],[c_138813]) ).
tcf(c_138821,plain,
( ~ leq(sk10,sk6)
| ~ leq(sk5,sk10) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6718,c_138814]) ).
tcf(c_140672,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(X1,X2)
| ( X0 = X2 )
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
inference(global_subsumption_just,[status(thm)],[c_418,c_93552]) ).
tcf(c_140685,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( X0 = sk6 )
| ~ ssList(nil)
| ~ memberP(iPr_def_15,X0) ),
inference(superposition,[status(thm)],[c_6705,c_140672]) ).
tcf(c_140686,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( X0 = sk11 )
| ~ ssList(nil)
| ~ memberP(iPr_def_17,X0) ),
inference(superposition,[status(thm)],[c_134912,c_140672]) ).
tcf(c_140697,plain,
! [X0: $i] :
( ( X0 = sk11 )
| ~ memberP(iPr_def_17,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_140686,c_134771,c_265]) ).
tcf(c_140700,plain,
! [X0: $i] :
( ( X0 = sk6 )
| ~ memberP(iPr_def_15,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_140685,c_134771,c_265]) ).
tcf(c_166107,plain,
ssList(iPr_def_17),
inference(light_normalisation,[status(thm)],[c_6728,c_6709]) ).
tcf(c_166133,plain,
! [X0: $i] :
( ~ memberP(sk4,X0)
| ~ leq(sk11,X0)
| ( X0 = sk11 ) ),
inference(global_subsumption_just,[status(thm)],[c_6710,c_448,c_265,c_6699,c_6701,c_13494,c_15907,c_21178,c_34192,c_60392,c_61237]) ).
tcf(c_166134,negated_conjecture,
! [X0: $i] :
( ( X0 = sk11 )
| ~ memberP(sk4,X0)
| ~ leq(sk11,X0) ),
inference(renaming,[status(thm)],[c_166133]) ).
tcf(c_166172,plain,
cons(sk11,nil) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_6708,c_14004]) ).
tcf(c_166306,plain,
( ssList(iPr_def_14)
| ~ ssList(iPr_def_13)
| ~ ssList(sk8) ),
inference(superposition,[status(thm)],[c_6704,c_342]) ).
tcf(c_166320,plain,
( ssList(iPr_def_14)
| ~ ssList(iPr_def_13) ),
inference(forward_subsumption_resolution,[status(thm)],[c_166306,c_6723]) ).
tcf(c_166332,plain,
ssList(iPr_def_14),
inference(global_subsumption_just,[status(thm)],[c_166320,c_10064,c_10061,c_10093]) ).
tcf(c_166347,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X1,X0))
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_343,c_93584]) ).
tcf(c_166353,plain,
( ssList(iPr_def_12)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6702,c_166347]) ).
tcf(c_166354,plain,
( ssList(iPr_def_15)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6705,c_166347]) ).
tcf(c_166358,plain,
ssList(iPr_def_15),
inference(forward_subsumption_resolution,[status(thm)],[c_166354,c_265]) ).
tcf(c_166359,plain,
ssList(iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_166353,c_265]) ).
tcf(c_166480,plain,
! [X0: $i,X1: $i] :
( memberP(cons(X1,X0),X1)
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_395,c_93551]) ).
tcf(c_166487,plain,
( memberP(iPr_def_15,sk6)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_6705,c_166480]) ).
tcf(c_166490,plain,
memberP(iPr_def_15,sk6),
inference(forward_subsumption_resolution,[status(thm)],[c_166487,c_265]) ).
tcf(c_166905,plain,
! [X0: $i,X1: $i] :
( leq(sk10,sk6)
| ~ leq(X1,X0)
| ( sk10 != X1 )
| ( sk6 != X0 ) ),
inference(instantiation,[status(thm)],[c_6736]) ).
tcf(c_167360,plain,
! [X0: $i,X1: $i] :
( ( app(cons(X1,nil),X0) = cons(X1,X0) )
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_377,c_448,c_265,c_6701,c_12018,c_13494,c_21178,c_34192,c_60392,c_61237]) ).
tcf(c_167366,plain,
! [X0: $i] : app(cons(X0,nil),sk4) = cons(X0,sk4),
inference(superposition,[status(thm)],[c_6727,c_167360]) ).
tcf(c_167368,plain,
! [X0: $i] : app(cons(X0,nil),sk8) = cons(X0,sk8),
inference(superposition,[status(thm)],[c_6723,c_167360]) ).
tcf(c_167426,plain,
! [X0: $i,X1: $i,X2: $i] :
( leq(sk10,X0)
| ~ leq(X2,X1)
| ( sk10 != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_6736]) ).
tcf(c_167455,plain,
cons(sk5,sk4) = app(iPr_def_12,sk4),
inference(superposition,[status(thm)],[c_6702,c_167366]) ).
tcf(c_167504,plain,
! [X0: $i] :
( leq(sk10,sk6)
| ~ leq(sk10,X0)
| ( sk10 != sk10 )
| ( sk6 != X0 ) ),
inference(instantiation,[status(thm)],[c_166905]) ).
tcf(c_167505,plain,
sk10 = sk10,
inference(instantiation,[status(thm)],[c_6729]) ).
tcf(c_167507,plain,
! [X0: $i,X1: $i] :
( ( sk10 = X0 )
| ( sk10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_6731]) ).
tcf(c_167543,plain,
cons(sk11,sk8) = app(iPr_def_17,sk8),
inference(superposition,[status(thm)],[c_166172,c_167368]) ).
tcf(c_169706,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X0,X2),X1)
| ~ memberP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X2) ),
inference(global_subsumption_just,[status(thm)],[c_397,c_93563]) ).
tcf(c_169707,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X0,X2),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(renaming,[status(thm)],[c_169706]) ).
tcf(c_169720,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ ssList(iPr_def_16)
| ~ ssList(sk9)
| ~ memberP(iPr_def_16,X0) ),
inference(superposition,[status(thm)],[c_6707,c_169707]) ).
tcf(c_169784,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ ssList(iPr_def_16)
| ~ memberP(iPr_def_16,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_169720,c_6722]) ).
tcf(c_169820,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X2,X0),X1)
| ~ memberP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X2) ),
inference(global_subsumption_just,[status(thm)],[c_398,c_93562]) ).
tcf(c_169821,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X2,X0),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(renaming,[status(thm)],[c_169820]) ).
tcf(c_169833,plain,
! [X0: $i] :
( memberP(iPr_def_16,X0)
| ~ ssList(iPr_def_15)
| ~ ssList(iPr_def_14)
| ~ memberP(iPr_def_15,X0) ),
inference(superposition,[status(thm)],[c_6706,c_169821]) ).
tcf(c_169902,plain,
! [X0: $i] :
( memberP(iPr_def_16,X0)
| ~ memberP(iPr_def_15,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_169833,c_166358,c_166332]) ).
tcf(c_172411,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(X1,X2)
| memberP(X0,X2)
| ~ memberP(app(X0,X1),X2)
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_415,c_93555]) ).
tcf(c_172412,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(X1,X2)
| memberP(X0,X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ memberP(app(X0,X1),X2) ),
inference(renaming,[status(thm)],[c_172411]) ).
tcf(c_174221,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(X1,X2)
| ( X0 = X2 )
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
inference(global_subsumption_just,[status(thm)],[c_418,c_93552]) ).
tcf(c_174235,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( X0 = sk11 )
| ~ ssList(nil)
| ~ memberP(iPr_def_17,X0) ),
inference(superposition,[status(thm)],[c_166172,c_174221]) ).
tcf(c_174243,plain,
! [X0: $i] :
( ( X0 = sk11 )
| ~ memberP(iPr_def_17,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_174235,c_134771,c_265]) ).
tcf(c_174457,plain,
( leq(sk10,sk10)
| ~ ssItem(sk10) ),
inference(instantiation,[status(thm)],[c_319]) ).
tcf(c_175163,plain,
! [X0: $i] :
( ( sk10 = X0 )
| ( sk10 != sk10 )
| ( X0 != sk10 ) ),
inference(instantiation,[status(thm)],[c_167507]) ).
tcf(c_176085,plain,
! [X0: $i,X1: $i] :
( leq(sk10,X0)
| ~ leq(sk10,X1)
| ( sk10 != sk10 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_167426]) ).
tcf(c_177681,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ memberP(iPr_def_16,X0) ),
inference(global_subsumption_just,[status(thm)],[c_169784,c_98966]) ).
tcf(c_190169,plain,
memberP(iPr_def_16,sk6),
inference(superposition,[status(thm)],[c_166490,c_169902]) ).
tcf(c_190486,plain,
memberP(iPr_def_17,sk6),
inference(superposition,[status(thm)],[c_190169,c_177681]) ).
tcf(c_193691,plain,
! [X0: $i] :
( memberP(iPr_def_12,X0)
| memberP(sk4,X0)
| ~ ssList(iPr_def_12)
| ~ ssList(sk4)
| ~ memberP(cons(sk5,sk4),X0) ),
inference(superposition,[status(thm)],[c_167455,c_172412]) ).
tcf(c_193720,plain,
! [X0: $i] :
( memberP(iPr_def_12,X0)
| memberP(sk4,X0)
| ~ memberP(cons(sk5,sk4),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_193691,c_166359,c_6727]) ).
tcf(c_193997,plain,
! [X0: $i] :
( ~ memberP(cons(sk5,sk4),X0)
| memberP(sk4,X0) ),
inference(global_subsumption_just,[status(thm)],[c_193720,c_448,c_265,c_6699,c_6701,c_13494,c_14410,c_15908,c_21178,c_34192,c_55535,c_60392,c_61237,c_61279,c_99453,c_99454,c_140697,c_193720]) ).
tcf(c_193998,plain,
! [X0: $i] :
( memberP(sk4,X0)
| ~ memberP(cons(sk5,sk4),X0) ),
inference(renaming,[status(thm)],[c_193997]) ).
tcf(c_194005,plain,
( memberP(sk4,sk5)
| ~ ssList(sk4) ),
inference(superposition,[status(thm)],[c_166480,c_193998]) ).
tcf(c_194009,plain,
memberP(sk4,sk5),
inference(forward_subsumption_resolution,[status(thm)],[c_194005,c_6727]) ).
tcf(c_194039,plain,
( ( sk5 = sk11 )
| ~ leq(sk11,sk5) ),
inference(superposition,[status(thm)],[c_194009,c_166134]) ).
tcf(c_195931,plain,
! [X0: $i] :
( leq(sk10,X0)
| ~ leq(sk10,sk10)
| ( sk10 != sk10 )
| ( X0 != sk10 ) ),
inference(instantiation,[status(thm)],[c_176085]) ).
tcf(c_196818,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| memberP(sk8,X0)
| ~ ssList(iPr_def_17)
| ~ ssList(sk8)
| ~ memberP(cons(sk11,sk8),X0) ),
inference(superposition,[status(thm)],[c_167543,c_172412]) ).
tcf(c_196823,plain,
! [X0: $i] :
( memberP(cons(sk11,sk8),X0)
| ~ ssList(iPr_def_17)
| ~ ssList(sk8)
| ~ memberP(sk8,X0) ),
inference(superposition,[status(thm)],[c_167543,c_169821]) ).
tcf(c_196842,plain,
! [X0: $i] :
( memberP(cons(sk11,sk8),X0)
| ~ memberP(sk8,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_196823,c_166107,c_6723]) ).
tcf(c_196854,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| memberP(sk8,X0)
| ~ memberP(cons(sk11,sk8),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_196818,c_166107,c_6723]) ).
tcf(c_202641,plain,
sk6 = sk11,
inference(superposition,[status(thm)],[c_190486,c_174243]) ).
tcf(c_202708,plain,
cons(sk11,nil) = iPr_def_15,
inference(demodulation,[status(thm)],[c_6705,c_202641]) ).
tcf(c_202711,plain,
leq(sk11,sk5),
inference(demodulation,[status(thm)],[c_6721,c_202641]) ).
tcf(c_202717,plain,
iPr_def_15 = iPr_def_17,
inference(demodulation,[status(thm)],[c_166172,c_202708]) ).
tcf(c_203451,plain,
! [X0: $i] :
( memberP(iPr_def_17,X0)
| ~ memberP(cons(sk11,sk8),X0) ),
inference(global_subsumption_just,[status(thm)],[c_196854,c_448,c_265,c_6699,c_6701,c_13494,c_14406,c_21178,c_34192,c_55535,c_60392,c_61237,c_196854]) ).
tcf(c_203454,plain,
! [X0: $i] :
( memberP(iPr_def_15,X0)
| ~ memberP(cons(sk11,sk8),X0) ),
inference(light_normalisation,[status(thm)],[c_203451,c_202717]) ).
tcf(c_203464,plain,
! [X0: $i] :
( memberP(iPr_def_15,X0)
| ~ memberP(sk8,X0) ),
inference(superposition,[status(thm)],[c_196842,c_203454]) ).
tcf(c_208045,plain,
! [X0: $i,X1: $i] :
( memberP(X0,X1)
| ~ leq(sk5,sk6)
| ( X1 != sk10 )
| ( X0 != sk8 ) ),
inference(resolution,[status(thm)],[c_6737,c_6719]) ).
tcf(c_209994,plain,
! [X0: $i,X1: $i] :
( memberP(X0,X1)
| ( X0 != sk8 )
| ( X1 != sk10 ) ),
inference(global_subsumption_just,[status(thm)],[c_208045,c_15909,c_19163,c_42783,c_100462,c_104368,c_104369,c_124735,c_124739,c_194039,c_202711,c_202717,c_208045]) ).
tcf(c_209995,plain,
! [X0: $i,X1: $i] :
( memberP(X0,X1)
| ( X1 != sk10 )
| ( X0 != sk8 ) ),
inference(renaming,[status(thm)],[c_209994]) ).
tcf(c_210031,plain,
! [X0: $i] :
( memberP(sk8,X0)
| ( X0 != sk10 ) ),
inference(resolution,[status(thm)],[c_209995,c_6729]) ).
tcf(c_211738,plain,
! [X0: $i] : X0 != sk10,
inference(global_subsumption_just,[status(thm)],[c_210031,c_448,c_265,c_6701,c_13374,c_13494,c_15909,c_19163,c_21178,c_31771,c_34192,c_35901,c_35902,c_42783,c_60392,c_61237,c_76103,c_76378,c_77611,c_97656,c_100462,c_104368,c_104369,c_124735,c_124739,c_138821,c_140700,c_167504,c_167505,c_174457,c_175163,c_194039,c_195931,c_202711,c_202717,c_203464,c_210031]) ).
tcf(c_211751,plain,
$false,
inference(resolution,[status(thm)],[c_211738,c_6729]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC152-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n013.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 16:40:21 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.40 Running first-order theorem proving
% 0.13/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.41
% 0.13/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.41
% 0.13/0.41 % Detected problem language: tptp
% 0.13/0.42 % Proving...
% 85.37/14.40 % SZS status Started for theBenchmark.p
% 85.37/14.40 % SZS status Unsatisfiable for theBenchmark.p
% 85.37/14.40
% 85.37/14.40 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 85.37/14.40
% 85.37/14.40 % ------ iProver source info
% 85.37/14.40
% 85.37/14.40 % git: date: 2026-07-19 20:42:38 +0200
% 85.37/14.40 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 85.37/14.40 % git: non_committed_changes: false
% 85.37/14.40
% 85.37/14.40 % ------ Parsing...% successful
% 85.37/14.40
% 85.37/14.40
% 85.37/14.40 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 85.37/14.40
% 85.37/14.40 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 85.37/14.40
% 85.37/14.40 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 85.37/14.40
% 85.37/14.40 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 85.37/14.40 % ------ Proving...
% 85.37/14.40 % ------ Problem Properties
% 85.37/14.40
% 85.37/14.40 %
% 85.37/14.40 % clauses 204
% 85.37/14.40 % conjectures 20
% 85.37/14.40 % EPR 72
% 85.37/14.40 % Horn 168
% 85.37/14.40 % unary 74
% 85.37/14.40 % binary 29
% 85.37/14.40 % lits 586
% 85.37/14.40 % lits eq 89
% 85.37/14.40 % fd_pure 0
% 85.37/14.40 % fd_pseudo 0
% 85.37/14.40 % fd_cond 17
% 85.37/14.40 % fd_pseudo_cond 14
% 85.37/14.40 % AC symbols 0
% 85.37/14.40
% 85.37/14.40 % ------ Schedule dynamic 5 is on
% 85.37/14.40
% 85.37/14.40 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 85.37/14.40
% 85.37/14.40
% 85.37/14.40 % ------
% 85.37/14.40 % Current options:
% 85.37/14.40 % ------
% 85.37/14.40
% 85.37/14.40
% 85.37/14.40 %
% 85.37/14.40
% 85.37/14.40 % ------ Proving...
% 85.37/14.40 % Proof_search_loop: time out after: 8032 full_loop iterations
% 85.37/14.40
% 85.37/14.40 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 85.37/14.40
% 85.37/14.40
% 85.37/14.40 % ------
% 85.37/14.40 % Current options:
% 85.37/14.40 % ------
% 85.37/14.40
% 85.37/14.40
% 85.37/14.40 %
% 85.37/14.40
% 85.37/14.40 % ------ Proving...
% 85.37/14.40 %
% 85.37/14.40
% 85.37/14.40 % SZS status Unsatisfiable for theBenchmark.p
% 85.37/14.40
% 85.37/14.40 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 76.40/14.41
% 76.40/14.41
%------------------------------------------------------------------------------