%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWC285-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 : n002.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:09 PM UTC 2026
% Result : Unsatisfiable 111.09s 28.48s
% Output : CNFRefutation 111.09s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f248ERROR: Could not build tree for root c_312615ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f16,axiom,
! [X0] : ssItem(skaf79(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause16) ).
fof(f47,axiom,
! [X0] : ssItem(skaf44(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause47) ).
fof(f50,axiom,
! [X0,X1] : ssList(skaf46(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause50) ).
fof(f62,axiom,
! [X0] :
( leq(X0,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause62) ).
fof(f71,axiom,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause71) ).
fof(f72,axiom,
! [X0,X1] :
( ssItem(X1)
| duplicatefreeP(X0)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f79,axiom,
! [X0] :
( segmentP(nil,X0)
| ~ ssList(X0)
| nil != X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause79) ).
fof(f80,axiom,
! [X0] :
( nil = X0
| ~ ssList(X0)
| ~ segmentP(nil,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause80) ).
fof(f85,axiom,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause86) ).
fof(f97,axiom,
! [X0,X1] :
( hd(cons(X0,X1)) = X0
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause97) ).
fof(f98,axiom,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != nil ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause98) ).
fof(f99,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| nil != cons(X0,X1) ),
inference(reorient_equations,[],[f98]) ).
fof(f101,axiom,
! [X0,X1] :
( X1 = X0
| neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause100) ).
fof(f102,plain,
! [X0,X1] :
( X0 = X1
| neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f101]) ).
fof(f103,axiom,
! [X0] :
( cons(skaf44(X0),nil) = X0
| ~ ssList(X0)
| ~ singletonP(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause101) ).
fof(f119,axiom,
! [X0,X1] :
( singletonP(X1)
| ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,nil) != X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause116) ).
fof(f121,axiom,
! [X0,X1] :
( nil = X0
| ~ ssList(X0)
| ~ ssList(X1)
| app(X0,X1) != nil ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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(f142,axiom,
! [X0,X1] :
( app(skaf46(X0,X1),X1) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ rearsegP(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause131) ).
fof(f151,axiom,
! [X2,X0,X1] :
( memberP(app(X0,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ memberP(X0,X1) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SWC001-0.ax',clause143) ).
fof(f163,axiom,
! [X2,X0,X1] :
( X0 = X2
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) != app(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause151) ).
fof(f164,axiom,
! [X2,X0,X1] :
( segmentP(X0,X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(X1,X2)
| ~ segmentP(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause152) ).
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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(f202,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_3) ).
fof(f203,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_4) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
segmentP(sk4,sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
ssList(sk6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_10) ).
fof(f210,negated_conjecture,
app(app(sk6,cons(sk5,nil)),sk7) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_11) ).
fof(f211,plain,
sk1 = app(app(sk6,cons(sk5,nil)),sk7),
inference(reorient_equations,[],[f210]) ).
fof(f212,negated_conjecture,
ssItem(sk8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_12) ).
fof(f213,negated_conjecture,
( memberP(sk7,sk8)
| memberP(sk6,sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_13) ).
fof(f216,negated_conjecture,
( ~ leq(sk5,sk8)
| ~ leq(sk8,sk5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_16) ).
fof(f217,negated_conjecture,
( ~ neq(sk4,nil)
| singletonP(sk3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_17) ).
fof(f220,plain,
sk3 = app(app(sk6,cons(sk5,nil)),sk7),
inference(definition_unfolding,[],[f211,f205]) ).
fof(f221,plain,
( segmentP(nil,nil)
| ~ ssList(nil) ),
inference(equality_resolution,[],[f79]) ).
fof(f228,plain,
! [X0] :
( singletonP(cons(X0,nil))
| ~ ssList(cons(X0,nil))
| ~ ssItem(X0) ),
inference(equality_resolution,[],[f119]) ).
fof(f231,plain,
! [X0,X1] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(equality_resolution,[],[f154]) ).
fof(f238,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_258,plain,
ssList(nil),
inference(cnf_transformation,[],[f8]) ).
tcf(c_266,plain,
! [X0: $i] : ssItem(skaf79(X0)),
inference(cnf_transformation,[],[f16]) ).
tcf(c_297,plain,
! [X0: $i] : ssItem(skaf44(X0)),
inference(cnf_transformation,[],[f47]) ).
tcf(c_300,plain,
! [X0: $i,X1: $i] : ssList(skaf46(X0,X1)),
inference(cnf_transformation,[],[f50]) ).
tcf(c_312,plain,
! [X0: $i] :
( leq(X0,X0)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_321,plain,
! [X0: $i] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_322,plain,
! [X0: $i,X1: $i] :
( duplicatefreeP(X0)
| ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_329,plain,
( segmentP(nil,nil)
| ~ ssList(nil) ),
inference(cnf_transformation,[],[f221]) ).
tcf(c_330,plain,
! [X0: $i] :
( ( X0 = nil )
| ~ ssList(X0)
| ~ segmentP(nil,X0) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_335,plain,
! [X0: $i,X1: $i] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_336,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_347,plain,
! [X0: $i,X1: $i] :
( ( hd(cons(X1,X0)) = X1 )
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_348,plain,
! [X0: $i,X1: $i] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ( cons(X0,X1) != nil ) ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_350,plain,
! [X0: $i,X1: $i] :
( neq(X1,X0)
| ( X0 = X1 )
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_351,plain,
! [X0: $i] :
( ( cons(skaf44(X0),nil) = X0 )
| ~ singletonP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_366,plain,
! [X0: $i] :
( singletonP(cons(X0,nil))
| ~ ssItem(X0)
| ~ ssList(cons(X0,nil)) ),
inference(cnf_transformation,[],[f228]) ).
tcf(c_368,plain,
! [X0: $i,X1: $i] :
( ( X0 = nil )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(X0,X1) != nil ) ),
inference(cnf_transformation,[],[f122]) ).
tcf(c_369,plain,
! [X0: $i,X1: $i] :
( ( X1 = nil )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(X0,X1) != nil ) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_370,plain,
! [X0: $i,X1: $i] :
( ( app(cons(X1,nil),X0) = cons(X1,X0) )
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_381,plain,
! [X0: $i,X1: $i] :
( ( app(skaf46(X0,X1),X1) = X0 )
| ~ ssList(X1)
| ~ ssList(X0)
| ~ rearsegP(X0,X1) ),
inference(cnf_transformation,[],[f142]) ).
tcf(c_388,plain,
! [X0: $i,X1: $i] :
( memberP(cons(X1,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f248]) ).
tcf(c_390,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_391,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_393,plain,
! [X0: $i,X1: $i] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1)) ),
inference(cnf_transformation,[],[f231]) ).
tcf(c_401,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = X2 )
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(X0,X1) != app(X2,X1) ) ),
inference(cnf_transformation,[],[f163]) ).
tcf(c_402,plain,
! [X0: $i,X1: $i,X2: $i] :
( segmentP(X0,X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ segmentP(X1,X2)
| ~ segmentP(X0,X1) ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_408,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_411,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_420,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_429,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,[],[f238]) ).
tcf(c_438,negated_conjecture,
ssList(sk3),
inference(cnf_transformation,[],[f202]) ).
tcf(c_439,negated_conjecture,
ssList(sk4),
inference(cnf_transformation,[],[f203]) ).
tcf(c_440,negated_conjecture,
segmentP(sk4,sk3),
inference(cnf_transformation,[],[f206]) ).
tcf(c_441,negated_conjecture,
ssItem(sk5),
inference(cnf_transformation,[],[f207]) ).
tcf(c_442,negated_conjecture,
ssList(sk6),
inference(cnf_transformation,[],[f208]) ).
tcf(c_443,negated_conjecture,
ssList(sk7),
inference(cnf_transformation,[],[f209]) ).
tcf(c_444,negated_conjecture,
app(app(sk6,cons(sk5,nil)),sk7) = sk3,
inference(cnf_transformation,[],[f220]) ).
tcf(c_445,negated_conjecture,
ssItem(sk8),
inference(cnf_transformation,[],[f212]) ).
tcf(c_446,negated_conjecture,
( memberP(sk7,sk8)
| memberP(sk6,sk8) ),
inference(cnf_transformation,[],[f213]) ).
tcf(c_449,negated_conjecture,
( ~ leq(sk8,sk5)
| ~ leq(sk5,sk8) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_450,negated_conjecture,
( singletonP(sk3)
| ~ neq(sk4,nil) ),
inference(cnf_transformation,[],[f217]) ).
tcf(c_831,plain,
! [X0: $i,X1: $i] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_393,c_335]) ).
tcf(c_2796,plain,
! [X0: $i,X1: $i] :
( singletonP(sk3)
| ( X0 = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( X1 != nil )
| ( X0 != sk4 ) ),
inference(resolution_lifted,[status(thm)],[c_450,c_350]) ).
tcf(c_2797,plain,
( singletonP(sk3)
| ( sk4 = nil )
| ~ ssList(nil)
| ~ ssList(sk4) ),
inference(unflattening,[status(thm)],[c_2796]) ).
tcf(c_2798,plain,
( singletonP(sk3)
| ( sk4 = nil ) ),
inference(global_subsumption_just,[status(thm)],[c_2797,c_439,c_258,c_2797]) ).
tcf(c_6644,plain,
! [X0: $i] :
( ~ iPr_def_10
| ssItem(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_322]) ).
tcf(c_6645,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ ssList(X0)
| duplicatefreeP(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_322]) ).
tcf(c_6646,plain,
( iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_322]) ).
tcf(c_6647,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_6649,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_6651,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( segmentP(X0,X2)
| ~ segmentP(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_6655,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( memberP(X0,X2)
| ~ memberP(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_6656,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( leq(X0,X2)
| ~ leq(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_9197,plain,
! [X0: $i] :
( ( cons(skaf44(cons(X0,nil)),nil) = cons(X0,nil) )
| ~ singletonP(cons(X0,nil))
| ~ ssList(cons(X0,nil)) ),
inference(instantiation,[status(thm)],[c_351]) ).
tcf(c_9273,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( memberP(X0,X3)
| ~ memberP(cons(X1,X2),X4)
| ( X3 != X4 )
| ( X0 != cons(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_6655]) ).
tcf(c_9311,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssList(app(X2,cons(X0,X1)))
| ~ ssList(X2)
| ~ ssList(cons(X0,X1)) ),
inference(instantiation,[status(thm)],[c_335]) ).
tcf(c_9346,plain,
! [X0: $i,X1: $i] :
( leq(sk5,sk8)
| ~ leq(X0,X1)
| ( sk8 != X1 )
| ( sk5 != X0 ) ),
inference(instantiation,[status(thm)],[c_6656]) ).
tcf(c_9524,plain,
! [X0: $i,X1: $i] :
( ( sk8 = X0 )
| ( sk8 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_6649]) ).
tcf(c_9528,plain,
sk8 = sk8,
inference(instantiation,[status(thm)],[c_6647]) ).
tcf(c_10139,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(cons(X1,X3))
| ~ ssList(app(X0,cons(X1,X2))) ),
inference(instantiation,[status(thm)],[c_9311]) ).
tcf(c_10562,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( memberP(app(cons(X0,X1),nil),X2)
| ~ memberP(cons(X0,X1),X3)
| ( X2 != X3 )
| ( app(cons(X0,X1),nil) != cons(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_9273]) ).
tcf(c_10987,plain,
( rearsegP(sk3,sk7)
| ~ ssList(sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(superposition,[status(thm)],[c_444,c_831]) ).
tcf(c_11045,plain,
( rearsegP(sk3,sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10987,c_443]) ).
tcf(c_11250,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( memberP(X2,X3)
| memberP(cons(X0,X1),X3)
| ~ ssItem(X3)
| ~ ssList(X2)
| ~ ssList(cons(X0,X1))
| ~ memberP(app(cons(X0,X1),X2),X3) ),
inference(instantiation,[status(thm)],[c_408]) ).
tcf(c_11310,plain,
( rearsegP(sk3,sk7)
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil)) ),
inference(superposition,[status(thm)],[c_335,c_11045]) ).
tcf(c_11311,plain,
( rearsegP(sk3,sk7)
| ~ ssList(cons(sk5,nil)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11310,c_442]) ).
tcf(c_11314,plain,
( rearsegP(sk3,sk7)
| ~ ssItem(sk5)
| ~ ssList(nil) ),
inference(superposition,[status(thm)],[c_336,c_11311]) ).
tcf(c_11315,plain,
rearsegP(sk3,sk7),
inference(forward_subsumption_resolution,[status(thm)],[c_11314,c_441,c_258]) ).
tcf(c_11882,plain,
! [X0: $i] :
( ( hd(cons(sk8,X0)) = sk8 )
| ~ ssItem(sk8)
| ~ ssList(X0) ),
inference(instantiation,[status(thm)],[c_347]) ).
tcf(c_11884,plain,
( ( hd(cons(sk8,nil)) = sk8 )
| ~ ssItem(sk8)
| ~ ssList(nil) ),
inference(instantiation,[status(thm)],[c_11882]) ).
tcf(c_12082,plain,
! [X0: $i] :
( leq(sk5,sk8)
| ~ leq(X0,sk8)
| ( sk8 != sk8 )
| ( sk5 != X0 ) ),
inference(instantiation,[status(thm)],[c_9346]) ).
tcf(c_12165,plain,
( leq(sk8,sk8)
| ~ ssItem(sk8) ),
inference(instantiation,[status(thm)],[c_312]) ).
tcf(c_12305,plain,
! [X0: $i] :
( ( sk8 = X0 )
| ( sk8 != sk8 )
| ( X0 != sk8 ) ),
inference(instantiation,[status(thm)],[c_9524]) ).
tcf(c_13282,plain,
! [X0: $i] :
( ssList(cons(sk5,X0))
| ~ ssItem(sk5)
| ~ ssList(X0) ),
inference(instantiation,[status(thm)],[c_336]) ).
tcf(c_13283,plain,
( ssList(cons(sk5,nil))
| ~ ssItem(sk5)
| ~ ssList(nil) ),
inference(instantiation,[status(thm)],[c_13282]) ).
tcf(c_13284,plain,
! [X0: $i] :
( ssList(cons(sk8,X0))
| ~ ssItem(sk8)
| ~ ssList(X0) ),
inference(instantiation,[status(thm)],[c_336]) ).
tcf(c_13285,plain,
( ssList(cons(sk8,nil))
| ~ ssItem(sk8)
| ~ ssList(nil) ),
inference(instantiation,[status(thm)],[c_13284]) ).
tcf(c_15535,plain,
( rearsegP(sk3,sk7)
| ~ ssList(sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(superposition,[status(thm)],[c_444,c_831]) ).
tcf(c_15553,plain,
( rearsegP(sk3,sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15535,c_443]) ).
tcf(c_15646,plain,
rearsegP(sk3,sk7),
inference(global_subsumption_just,[status(thm)],[c_15553,c_11315]) ).
tcf(c_16267,plain,
( ( app(skaf46(sk3,sk7),sk7) = sk3 )
| ~ ssList(sk7)
| ~ ssList(sk3) ),
inference(superposition,[status(thm)],[c_15646,c_381]) ).
tcf(c_16285,plain,
app(skaf46(sk3,sk7),sk7) = sk3,
inference(forward_subsumption_resolution,[status(thm)],[c_16267,c_443,c_438]) ).
tcf(c_16886,plain,
( ( skaf46(sk3,sk7) = nil )
| ~ ssList(sk7)
| ~ ssList(skaf46(sk3,sk7))
| ( sk3 != nil ) ),
inference(superposition,[status(thm)],[c_16285,c_368]) ).
tcf(c_16897,plain,
( ( skaf46(sk3,sk7) = nil )
| ( sk3 != nil ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_16886,c_443,c_300]) ).
tcf(c_19599,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(X1,X2)
| memberP(cons(sk5,X0),X2)
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(cons(sk5,X0))
| ~ memberP(app(cons(sk5,X0),X1),X2) ),
inference(instantiation,[status(thm)],[c_11250]) ).
tcf(c_19615,plain,
! [X0: $i,X1: $i] :
( ssList(app(X1,cons(sk5,X0)))
| ~ ssList(X1)
| ~ ssList(cons(sk5,X0)) ),
inference(instantiation,[status(thm)],[c_9311]) ).
tcf(c_19624,plain,
( ssList(app(nil,cons(sk5,nil)))
| ~ ssList(nil)
| ~ ssList(cons(sk5,nil)) ),
inference(instantiation,[status(thm)],[c_19615]) ).
tcf(c_19649,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssList(app(app(X0,cons(sk5,X1)),cons(sk5,X2)))
| ~ ssList(cons(sk5,X2))
| ~ ssList(app(X0,cons(sk5,X1))) ),
inference(instantiation,[status(thm)],[c_10139]) ).
tcf(c_19650,plain,
( ssList(app(app(nil,cons(sk5,nil)),cons(sk5,nil)))
| ~ ssList(cons(sk5,nil))
| ~ ssList(app(nil,cons(sk5,nil))) ),
inference(instantiation,[status(thm)],[c_19649]) ).
tcf(c_19807,plain,
! [X0: $i,X1: $i] :
( singletonP(sk3)
| segmentP(X0,sk4)
| ~ segmentP(X1,nil)
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_6651,c_2798]) ).
tcf(c_20663,plain,
! [X0: $i] :
( singletonP(sk3)
| segmentP(X0,sk4)
| ~ segmentP(X0,nil) ),
inference(resolution,[status(thm)],[c_19807,c_6647]) ).
tcf(c_20664,plain,
( singletonP(sk3)
| segmentP(nil,sk4)
| ~ segmentP(nil,nil) ),
inference(instantiation,[status(thm)],[c_20663]) ).
tcf(c_27183,plain,
( leq(sk5,sk8)
| ~ leq(sk8,sk8)
| ( sk8 != sk8 )
| ( sk5 != sk8 ) ),
inference(instantiation,[status(thm)],[c_12082]) ).
tcf(c_27247,plain,
! [X0: $i] :
( ( sk8 = hd(cons(sk8,X0)) )
| ( sk8 != sk8 )
| ( hd(cons(sk8,X0)) != sk8 ) ),
inference(instantiation,[status(thm)],[c_12305]) ).
tcf(c_27248,plain,
( ( sk8 = hd(cons(sk8,nil)) )
| ( sk8 != sk8 )
| ( hd(cons(sk8,nil)) != sk8 ) ),
inference(instantiation,[status(thm)],[c_27247]) ).
tcf(c_28341,plain,
( ~ ssItem(sk8)
| ~ memberP(nil,sk8) ),
inference(instantiation,[status(thm)],[c_321]) ).
tcf(c_30414,plain,
! [X0: $i,X1: $i] :
( memberP(X1,sk8)
| memberP(cons(sk5,X0),sk8)
| ~ ssItem(sk8)
| ~ ssList(X1)
| ~ ssList(cons(sk5,X0))
| ~ memberP(app(cons(sk5,X0),X1),sk8) ),
inference(instantiation,[status(thm)],[c_19599]) ).
tcf(c_30415,plain,
( memberP(nil,sk8)
| memberP(cons(sk5,nil),sk8)
| ~ ssItem(sk8)
| ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| ~ memberP(app(cons(sk5,nil),nil),sk8) ),
inference(instantiation,[status(thm)],[c_30414]) ).
tcf(c_33508,plain,
! [X0: $i,X1: $i] :
( memberP(app(cons(sk5,X0),nil),sk8)
| ~ memberP(cons(sk5,X0),X1)
| ( sk8 != X1 )
| ( app(cons(sk5,X0),nil) != cons(sk5,X0) ) ),
inference(instantiation,[status(thm)],[c_10562]) ).
tcf(c_41410,plain,
! [X0: $i,X1: $i] :
( duplicatefreeP(app(X1,X0))
| ~ iPr_def_11
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(superposition,[status(thm)],[c_335,c_6645]) ).
tcf(c_41517,plain,
( rearsegP(sk3,sk7)
| ~ ssList(sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(superposition,[status(thm)],[c_444,c_831]) ).
tcf(c_41535,plain,
( rearsegP(sk3,sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_41517,c_443]) ).
tcf(c_41637,plain,
rearsegP(sk3,sk7),
inference(global_subsumption_just,[status(thm)],[c_41535,c_11315]) ).
tcf(c_41852,plain,
! [X0: $i] :
( ( app(cons(X0,nil),sk3) = cons(X0,sk3) )
| ~ ssItem(X0) ),
inference(superposition,[status(thm)],[c_438,c_370]) ).
tcf(c_42303,plain,
( ( app(skaf46(sk3,sk7),sk7) = sk3 )
| ~ ssList(sk7)
| ~ ssList(sk3) ),
inference(superposition,[status(thm)],[c_41637,c_381]) ).
tcf(c_42321,plain,
app(skaf46(sk3,sk7),sk7) = sk3,
inference(forward_subsumption_resolution,[status(thm)],[c_42303,c_443,c_438]) ).
tcf(c_42661,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ ssList(sk7)
| ~ ssItem(X0)
| ~ memberP(sk7,X0)
| ~ ssList(skaf46(sk3,sk7)) ),
inference(superposition,[status(thm)],[c_42321,c_391]) ).
tcf(c_42668,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk7,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_42661,c_443,c_300]) ).
tcf(c_43473,plain,
! [X0: $i] :
( ( skaf46(sk3,sk7) = X0 )
| ~ ssList(sk7)
| ~ ssList(X0)
| ~ ssList(skaf46(sk3,sk7))
| ( app(X0,sk7) != sk3 ) ),
inference(superposition,[status(thm)],[c_42321,c_401]) ).
tcf(c_43515,plain,
! [X0: $i] :
( ( skaf46(sk3,sk7) = X0 )
| ~ ssList(X0)
| ( app(X0,sk7) != sk3 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_43473,c_443,c_300]) ).
tcf(c_44744,plain,
! [X0: $i] : app(cons(skaf79(X0),nil),sk3) = cons(skaf79(X0),sk3),
inference(superposition,[status(thm)],[c_266,c_41852]) ).
tcf(c_49762,plain,
! [X0: $i] :
( ~ ssItem(sk5)
| ~ ssList(X0)
| ( cons(sk5,X0) != nil ) ),
inference(instantiation,[status(thm)],[c_348]) ).
tcf(c_49763,plain,
( ~ ssItem(sk5)
| ~ ssList(nil)
| ( cons(sk5,nil) != nil ) ),
inference(instantiation,[status(thm)],[c_49762]) ).
tcf(c_50782,plain,
( ( app(cons(sk5,nil),nil) = cons(sk5,nil) )
| ~ ssItem(sk5)
| ~ ssList(nil) ),
inference(instantiation,[status(thm)],[c_370]) ).
tcf(c_51003,plain,
! [X0: $i] :
( memberP(app(cons(sk5,nil),nil),sk8)
| ~ memberP(cons(sk5,nil),X0)
| ( sk8 != X0 )
| ( app(cons(sk5,nil),nil) != cons(sk5,nil) ) ),
inference(instantiation,[status(thm)],[c_33508]) ).
tcf(c_51348,plain,
( ( cons(skaf44(cons(sk8,nil)),nil) = cons(sk8,nil) )
| ~ singletonP(cons(sk8,nil))
| ~ ssList(cons(sk8,nil)) ),
inference(instantiation,[status(thm)],[c_9197]) ).
tcf(c_54826,plain,
! [X0: $i] :
( segmentP(X0,sk3)
| ~ ssList(sk4)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ segmentP(X0,sk4) ),
inference(resolution,[status(thm)],[c_402,c_440]) ).
tcf(c_56618,plain,
! [X0: $i] :
( segmentP(X0,sk3)
| ~ ssList(X0)
| ~ segmentP(X0,sk4) ),
inference(global_subsumption_just,[status(thm)],[c_54826,c_439,c_438,c_54826]) ).
tcf(c_56620,plain,
( segmentP(nil,sk3)
| ~ ssList(nil)
| ~ segmentP(nil,sk4) ),
inference(instantiation,[status(thm)],[c_56618]) ).
tcf(c_60785,plain,
( singletonP(cons(sk8,nil))
| ~ ssItem(sk8)
| ~ ssList(cons(sk8,nil)) ),
inference(instantiation,[status(thm)],[c_366]) ).
tcf(c_75898,plain,
! [X0: $i,X1: $i] :
( leq(sk8,sk5)
| ~ leq(X1,X0)
| ( sk8 != X1 )
| ( sk5 != X0 ) ),
inference(instantiation,[status(thm)],[c_6656]) ).
tcf(c_76019,plain,
! [X0: $i,X1: $i,X2: $i] :
( leq(sk8,X0)
| ~ leq(X2,X1)
| ( sk8 != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_6656]) ).
tcf(c_76043,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = sk8 )
| ~ ssItem(sk8)
| ~ ssItem(X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ( cons(X0,X1) != cons(sk8,X2) ) ),
inference(instantiation,[status(thm)],[c_420]) ).
tcf(c_76044,plain,
! [X0: $i,X1: $i] :
( memberP(X1,sk8)
| ( X0 = sk8 )
| ~ ssItem(sk8)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),sk8) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_76074,plain,
! [X0: $i,X1: $i] :
( ( sk8 = X0 )
| ( sk8 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_6649]) ).
tcf(c_77132,plain,
! [X0: $i] :
( ( sk8 = X0 )
| ( sk8 != sk8 )
| ( X0 != sk8 ) ),
inference(instantiation,[status(thm)],[c_76074]) ).
tcf(c_77292,plain,
! [X0: $i,X1: $i] :
( leq(sk8,X0)
| ~ leq(sk8,X1)
| ( sk8 != sk8 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_76019]) ).
tcf(c_77364,plain,
( ( skaf44(cons(sk8,nil)) = sk8 )
| ~ ssItem(sk8)
| ~ ssList(nil)
| ~ ssItem(skaf44(cons(sk8,nil)))
| ( cons(skaf44(cons(sk8,nil)),nil) != cons(sk8,nil) ) ),
inference(instantiation,[status(thm)],[c_76043]) ).
tcf(c_81623,plain,
ssItem(skaf44(cons(sk8,nil))),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_81801,plain,
( ( sk3 = nil )
| ~ ssList(sk3)
| ~ segmentP(nil,sk3) ),
inference(instantiation,[status(thm)],[c_330]) ).
tcf(c_82082,plain,
! [X0: $i] :
( leq(sk8,X0)
| ~ leq(sk8,sk8)
| ( sk8 != sk8 )
| ( X0 != sk8 ) ),
inference(instantiation,[status(thm)],[c_77292]) ).
tcf(c_87125,plain,
! [X0: $i,X1: $i] :
( leq(sk8,sk5)
| ~ leq(hd(cons(sk8,X1)),X0)
| ( sk8 != hd(cons(sk8,X1)) )
| ( sk5 != X0 ) ),
inference(instantiation,[status(thm)],[c_75898]) ).
tcf(c_89904,plain,
( ( sk8 = skaf44(cons(sk8,nil)) )
| ( sk8 != sk8 )
| ( skaf44(cons(sk8,nil)) != sk8 ) ),
inference(instantiation,[status(thm)],[c_77132]) ).
tcf(c_90625,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( leq(hd(cons(sk8,X0)),X2)
| ~ leq(X1,X3)
| ( X2 != X3 )
| ( hd(cons(sk8,X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_6656]) ).
tcf(c_90630,plain,
! [X0: $i] :
( leq(sk8,sk5)
| ~ leq(hd(cons(sk8,X0)),sk8)
| ( sk8 != hd(cons(sk8,X0)) )
| ( sk5 != sk8 ) ),
inference(instantiation,[status(thm)],[c_87125]) ).
tcf(c_90632,plain,
( leq(sk8,sk5)
| ~ leq(hd(cons(sk8,nil)),sk8)
| ( sk8 != hd(cons(sk8,nil)) )
| ( sk5 != sk8 ) ),
inference(instantiation,[status(thm)],[c_90630]) ).
tcf(c_94836,plain,
! [X0: $i] :
( ( sk8 = X0 )
| ( sk8 != skaf44(cons(sk8,nil)) )
| ( X0 != skaf44(cons(sk8,nil)) ) ),
inference(instantiation,[status(thm)],[c_76074]) ).
tcf(c_95181,plain,
( leq(sk8,skaf44(cons(sk8,nil)))
| ~ leq(sk8,sk8)
| ( sk8 != sk8 )
| ( skaf44(cons(sk8,nil)) != sk8 ) ),
inference(instantiation,[status(thm)],[c_82082]) ).
tcf(c_99823,plain,
! [X0: $i] :
( ( sk8 = hd(cons(skaf44(cons(sk8,nil)),X0)) )
| ( sk8 != skaf44(cons(sk8,nil)) )
| ( hd(cons(skaf44(cons(sk8,nil)),X0)) != skaf44(cons(sk8,nil)) ) ),
inference(instantiation,[status(thm)],[c_94836]) ).
tcf(c_99824,plain,
! [X0: $i] :
( ( hd(cons(skaf44(cons(sk8,nil)),X0)) = skaf44(cons(sk8,nil)) )
| ~ ssList(X0)
| ~ ssItem(skaf44(cons(sk8,nil))) ),
inference(instantiation,[status(thm)],[c_347]) ).
tcf(c_99825,plain,
( ( sk8 = hd(cons(skaf44(cons(sk8,nil)),nil)) )
| ( sk8 != skaf44(cons(sk8,nil)) )
| ( hd(cons(skaf44(cons(sk8,nil)),nil)) != skaf44(cons(sk8,nil)) ) ),
inference(instantiation,[status(thm)],[c_99823]) ).
tcf(c_99826,plain,
( ( hd(cons(skaf44(cons(sk8,nil)),nil)) = skaf44(cons(sk8,nil)) )
| ~ ssList(nil)
| ~ ssItem(skaf44(cons(sk8,nil))) ),
inference(instantiation,[status(thm)],[c_99824]) ).
tcf(c_101060,plain,
! [X0: $i,X1: $i,X2: $i] :
( leq(hd(cons(sk8,X0)),X1)
| ~ leq(sk8,X2)
| ( X1 != X2 )
| ( hd(cons(sk8,X0)) != sk8 ) ),
inference(instantiation,[status(thm)],[c_90625]) ).
tcf(c_102239,plain,
! [X0: $i] :
( leq(sk8,X0)
| ~ leq(sk8,skaf44(cons(sk8,nil)))
| ( sk8 != sk8 )
| ( X0 != skaf44(cons(sk8,nil)) ) ),
inference(instantiation,[status(thm)],[c_77292]) ).
tcf(c_109626,plain,
! [X0: $i] :
( leq(sk8,hd(cons(skaf44(cons(sk8,nil)),X0)))
| ~ leq(sk8,skaf44(cons(sk8,nil)))
| ( sk8 != sk8 )
| ( hd(cons(skaf44(cons(sk8,nil)),X0)) != skaf44(cons(sk8,nil)) ) ),
inference(instantiation,[status(thm)],[c_102239]) ).
tcf(c_109627,plain,
( leq(sk8,hd(cons(skaf44(cons(sk8,nil)),nil)))
| ~ leq(sk8,skaf44(cons(sk8,nil)))
| ( sk8 != sk8 )
| ( hd(cons(skaf44(cons(sk8,nil)),nil)) != skaf44(cons(sk8,nil)) ) ),
inference(instantiation,[status(thm)],[c_109626]) ).
tcf(c_115260,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ssItem(sk5)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ duplicatefreeP(app(app(X0,cons(sk5,X1)),cons(sk5,X2)))
| ~ ssList(app(app(X0,cons(sk5,X1)),cons(sk5,X2))) ),
inference(instantiation,[status(thm)],[c_429]) ).
tcf(c_115261,plain,
( ~ ssItem(sk5)
| ~ ssList(nil)
| ~ duplicatefreeP(app(app(nil,cons(sk5,nil)),cons(sk5,nil)))
| ~ ssList(app(app(nil,cons(sk5,nil)),cons(sk5,nil))) ),
inference(instantiation,[status(thm)],[c_115260]) ).
tcf(c_117597,plain,
! [X0: $i] :
( duplicatefreeP(cons(skaf79(X0),sk3))
| ~ iPr_def_11
| ~ ssList(sk3)
| ~ ssList(cons(skaf79(X0),nil)) ),
inference(superposition,[status(thm)],[c_44744,c_41410]) ).
tcf(c_117617,plain,
! [X0: $i] :
( duplicatefreeP(cons(skaf79(X0),sk3))
| ~ iPr_def_11
| ~ ssList(cons(skaf79(X0),nil)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_117597,c_438]) ).
tcf(c_119229,plain,
! [X0: $i,X1: $i,X2: $i] :
( duplicatefreeP(app(app(X0,cons(sk5,X1)),cons(sk5,X2)))
| ~ iPr_def_11
| ~ ssList(app(app(X0,cons(sk5,X1)),cons(sk5,X2))) ),
inference(instantiation,[status(thm)],[c_6645]) ).
tcf(c_119232,plain,
( duplicatefreeP(app(app(nil,cons(sk5,nil)),cons(sk5,nil)))
| ~ iPr_def_11
| ~ ssList(app(app(nil,cons(sk5,nil)),cons(sk5,nil))) ),
inference(instantiation,[status(thm)],[c_119229]) ).
tcf(c_121260,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_117617,c_441,c_258,c_13283,c_19624,c_19650,c_115261,c_119232]) ).
tcf(c_121262,plain,
iPr_def_10,
inference(backward_subsumption_resolution,[status(thm)],[c_6646,c_121260]) ).
tcf(c_121325,plain,
! [X0: $i] : ssItem(X0),
inference(backward_subsumption_resolution,[status(thm)],[c_6644,c_121262]) ).
tcf(c_122156,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ memberP(sk7,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_42668,c_121325]) ).
tcf(c_124367,plain,
( ( app(sk6,cons(sk5,nil)) = skaf46(sk3,sk7) )
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(superposition,[status(thm)],[c_444,c_43515]) ).
tcf(c_126097,plain,
( ( app(sk6,cons(sk5,nil)) = skaf46(sk3,sk7) )
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil)) ),
inference(superposition,[status(thm)],[c_335,c_124367]) ).
tcf(c_126098,plain,
( ( app(sk6,cons(sk5,nil)) = skaf46(sk3,sk7) )
| ~ ssList(cons(sk5,nil)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_126097,c_442]) ).
tcf(c_126099,plain,
app(sk6,cons(sk5,nil)) = skaf46(sk3,sk7),
inference(global_subsumption_just,[status(thm)],[c_126098,c_441,c_258,c_13283,c_126098]) ).
tcf(c_126108,plain,
( ( cons(sk5,nil) = nil )
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ( skaf46(sk3,sk7) != nil ) ),
inference(superposition,[status(thm)],[c_126099,c_369]) ).
tcf(c_126125,plain,
( ( cons(sk5,nil) = nil )
| ~ ssList(cons(sk5,nil))
| ( skaf46(sk3,sk7) != nil ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_126108,c_442]) ).
tcf(c_138287,plain,
! [X0: $i] :
( memberP(X0,sk8)
| ( sk5 = sk8 )
| ~ ssItem(sk8)
| ~ ssItem(sk5)
| ~ ssList(X0)
| ~ memberP(cons(sk5,X0),sk8) ),
inference(instantiation,[status(thm)],[c_76044]) ).
tcf(c_138289,plain,
( memberP(nil,sk8)
| ( sk5 = sk8 )
| ~ ssItem(sk8)
| ~ ssItem(sk5)
| ~ ssList(nil)
| ~ memberP(cons(sk5,nil),sk8) ),
inference(instantiation,[status(thm)],[c_138287]) ).
tcf(c_139932,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_411,c_121325]) ).
tcf(c_139942,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_391,c_121325]) ).
tcf(c_139943,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_390,c_121325]) ).
tcf(c_139962,plain,
! [X0: $i,X1: $i] :
( ( hd(cons(X1,X0)) = X1 )
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_347,c_121325]) ).
tcf(c_139965,plain,
! [X0: $i] : ~ memberP(nil,X0),
inference(backward_subsumption_resolution,[status(thm)],[c_321,c_121325]) ).
tcf(c_139982,plain,
singletonP(sk3),
inference(global_subsumption_just,[status(thm)],[c_2798,c_441,c_438,c_258,c_329,c_13283,c_16897,c_20664,c_49763,c_56620,c_81801,c_126125]) ).
tcf(c_140016,plain,
! [X0: $i] : hd(cons(X0,nil)) = X0,
inference(superposition,[status(thm)],[c_258,c_139962]) ).
tcf(c_140138,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ ssList(sk7)
| ~ memberP(sk7,X0)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(superposition,[status(thm)],[c_444,c_139942]) ).
tcf(c_140147,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ memberP(sk7,X0)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_140138,c_443]) ).
tcf(c_140164,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ memberP(sk7,X0) ),
inference(global_subsumption_just,[status(thm)],[c_140147,c_122156]) ).
tcf(c_140168,plain,
( memberP(sk6,sk8)
| memberP(sk3,sk8) ),
inference(superposition,[status(thm)],[c_446,c_140164]) ).
tcf(c_140184,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ ssList(sk7)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ memberP(app(sk6,cons(sk5,nil)),X0) ),
inference(superposition,[status(thm)],[c_444,c_139943]) ).
tcf(c_140193,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ memberP(app(sk6,cons(sk5,nil)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_140184,c_443]) ).
tcf(c_140229,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ ssList(sk6)
| ~ memberP(sk6,X0)
| ~ ssList(cons(sk5,nil))
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(superposition,[status(thm)],[c_139943,c_140193]) ).
tcf(c_140230,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(superposition,[status(thm)],[c_139942,c_140193]) ).
tcf(c_140231,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ memberP(sk6,X0)
| ~ ssList(cons(sk5,nil))
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_140229,c_442]) ).
tcf(c_140232,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_140230,c_442]) ).
tcf(c_140235,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ memberP(sk6,X0)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(global_subsumption_just,[status(thm)],[c_140231,c_441,c_258,c_13283,c_140231]) ).
tcf(c_140241,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ memberP(cons(sk5,nil),X0) ),
inference(global_subsumption_just,[status(thm)],[c_140232,c_441,c_258,c_13283,c_140232]) ).
tcf(c_140242,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ memberP(cons(sk5,nil),X0)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(renaming,[status(thm)],[c_140241]) ).
tcf(c_141132,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0) ),
inference(superposition,[status(thm)],[c_335,c_140242]) ).
tcf(c_141133,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ ssList(sk6)
| ~ memberP(sk6,X0)
| ~ ssList(cons(sk5,nil)) ),
inference(superposition,[status(thm)],[c_335,c_140235]) ).
tcf(c_141154,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ memberP(sk6,X0)
| ~ ssList(cons(sk5,nil)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_141133,c_442]) ).
tcf(c_141155,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_141132,c_442]) ).
tcf(c_141429,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ memberP(sk6,X0) ),
inference(global_subsumption_just,[status(thm)],[c_141154,c_441,c_258,c_13283,c_141154]) ).
tcf(c_141434,plain,
memberP(sk3,sk8),
inference(superposition,[status(thm)],[c_140168,c_141429]) ).
tcf(c_141435,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ memberP(cons(sk5,nil),X0) ),
inference(global_subsumption_just,[status(thm)],[c_141155,c_441,c_258,c_13283,c_141155]) ).
tcf(c_141626,plain,
( ( cons(skaf44(sk3),nil) = sk3 )
| ~ ssList(sk3) ),
inference(superposition,[status(thm)],[c_139982,c_351]) ).
tcf(c_141628,plain,
cons(skaf44(sk3),nil) = sk3,
inference(forward_subsumption_resolution,[status(thm)],[c_141626,c_438]) ).
tcf(c_141812,plain,
skaf44(sk3) = hd(sk3),
inference(superposition,[status(thm)],[c_141628,c_140016]) ).
tcf(c_141825,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( skaf44(sk3) = X0 )
| ~ ssList(nil)
| ~ memberP(sk3,X0) ),
inference(superposition,[status(thm)],[c_141628,c_139932]) ).
tcf(c_141854,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( hd(sk3) = X0 )
| ~ ssList(nil)
| ~ memberP(sk3,X0) ),
inference(light_normalisation,[status(thm)],[c_141825,c_141812]) ).
tcf(c_141855,plain,
! [X0: $i] :
( ( hd(sk3) = X0 )
| ~ memberP(sk3,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_141854,c_139965,c_258]) ).
tcf(c_166605,plain,
! [X0: $i,X1: $i,X2: $i] :
( leq(hd(cons(sk8,X0)),X1)
| ~ leq(sk8,hd(cons(skaf44(cons(sk8,nil)),X2)))
| ( X1 != hd(cons(skaf44(cons(sk8,nil)),X2)) )
| ( hd(cons(sk8,X0)) != sk8 ) ),
inference(instantiation,[status(thm)],[c_101060]) ).
tcf(c_221857,plain,
! [X0: $i,X1: $i] :
( leq(hd(cons(sk8,X0)),sk8)
| ~ leq(sk8,hd(cons(skaf44(cons(sk8,nil)),X1)))
| ( sk8 != hd(cons(skaf44(cons(sk8,nil)),X1)) )
| ( hd(cons(sk8,X0)) != sk8 ) ),
inference(instantiation,[status(thm)],[c_166605]) ).
tcf(c_221858,plain,
( leq(hd(cons(sk8,nil)),sk8)
| ~ leq(sk8,hd(cons(skaf44(cons(sk8,nil)),nil)))
| ( sk8 != hd(cons(skaf44(cons(sk8,nil)),nil)) )
| ( hd(cons(sk8,nil)) != sk8 ) ),
inference(instantiation,[status(thm)],[c_221857]) ).
tcf(c_238968,plain,
( ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil)) ),
inference(instantiation,[status(thm)],[c_335]) ).
tcf(c_301209,plain,
! [X0: $i,X1: $i] :
( memberP(cons(X1,X0),X1)
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_388,c_121325]) ).
tcf(c_301216,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_411,c_121325]) ).
tcf(c_301226,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_391,c_121325]) ).
tcf(c_301227,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_390,c_121325]) ).
tcf(c_301236,plain,
! [X0: $i,X1: $i] :
( ( app(cons(X1,nil),X0) = cons(X1,X0) )
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_370,c_121325]) ).
tcf(c_301246,plain,
! [X0: $i,X1: $i] :
( ( hd(cons(X1,X0)) = X1 )
| ~ ssList(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_347,c_121325]) ).
tcf(c_301265,plain,
singletonP(sk3),
inference(global_subsumption_just,[status(thm)],[c_2798,c_441,c_438,c_258,c_329,c_13283,c_16897,c_20664,c_49763,c_56620,c_81801,c_126125]) ).
tcf(c_301311,plain,
! [X0: $i] : hd(cons(X0,nil)) = X0,
inference(superposition,[status(thm)],[c_258,c_301246]) ).
tcf(c_301388,plain,
! [X0: $i] : app(cons(X0,nil),sk6) = cons(X0,sk6),
inference(superposition,[status(thm)],[c_442,c_301236]) ).
tcf(c_301430,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ ssList(sk7)
| ~ memberP(sk7,X0)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(superposition,[status(thm)],[c_444,c_301226]) ).
tcf(c_301439,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ memberP(sk7,X0)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_301430,c_443]) ).
tcf(c_301461,plain,
! [X0: $i] :
( memberP(sk3,X0)
| ~ memberP(sk7,X0) ),
inference(global_subsumption_just,[status(thm)],[c_301439,c_122156]) ).
tcf(c_301465,plain,
( memberP(sk6,sk8)
| memberP(sk3,sk8) ),
inference(superposition,[status(thm)],[c_446,c_301461]) ).
tcf(c_301466,plain,
memberP(sk3,sk8),
inference(global_subsumption_just,[status(thm)],[c_301465,c_141434]) ).
tcf(c_301475,plain,
! [X0: $i,X1: $i] :
( memberP(cons(X0,sk6),X1)
| ~ ssList(sk6)
| ~ ssList(cons(X0,nil))
| ~ memberP(cons(X0,nil),X1) ),
inference(superposition,[status(thm)],[c_301388,c_301227]) ).
tcf(c_301478,plain,
! [X0: $i,X1: $i] :
( memberP(cons(X0,sk6),X1)
| ~ ssList(cons(X0,nil))
| ~ memberP(cons(X0,nil),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_301475,c_442]) ).
tcf(c_302431,plain,
( ( cons(skaf44(sk3),nil) = sk3 )
| ~ ssList(sk3) ),
inference(superposition,[status(thm)],[c_301265,c_351]) ).
tcf(c_302433,plain,
cons(skaf44(sk3),nil) = sk3,
inference(forward_subsumption_resolution,[status(thm)],[c_302431,c_438]) ).
tcf(c_302434,plain,
skaf44(sk3) = hd(sk3),
inference(superposition,[status(thm)],[c_302433,c_301311]) ).
tcf(c_302445,plain,
! [X0: $i] :
( memberP(cons(skaf44(sk3),sk6),X0)
| ~ memberP(sk3,X0)
| ~ ssList(cons(skaf44(sk3),nil)) ),
inference(superposition,[status(thm)],[c_302433,c_301478]) ).
tcf(c_302448,plain,
cons(skaf44(sk3),sk6) = app(sk3,sk6),
inference(superposition,[status(thm)],[c_302433,c_301388]) ).
tcf(c_302465,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( skaf44(sk3) = X0 )
| ~ ssList(nil)
| ~ memberP(sk3,X0) ),
inference(superposition,[status(thm)],[c_302433,c_301216]) ).
tcf(c_302506,plain,
cons(hd(sk3),sk6) = app(sk3,sk6),
inference(light_normalisation,[status(thm)],[c_302448,c_302434]) ).
tcf(c_302517,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( hd(sk3) = X0 )
| ~ ssList(nil)
| ~ memberP(sk3,X0) ),
inference(light_normalisation,[status(thm)],[c_302465,c_302434]) ).
tcf(c_302518,plain,
! [X0: $i] :
( ( hd(sk3) = X0 )
| ~ memberP(sk3,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_302517,c_139965,c_258]) ).
tcf(c_302526,plain,
! [X0: $i] :
( memberP(app(sk3,sk6),X0)
| ~ ssList(sk3)
| ~ memberP(sk3,X0) ),
inference(light_normalisation,[status(thm)],[c_302445,c_302433,c_302434,c_302506]) ).
tcf(c_302527,plain,
! [X0: $i] :
( memberP(app(sk3,sk6),X0)
| ~ memberP(sk3,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_302526,c_438]) ).
tcf(c_303329,plain,
( rearsegP(sk3,sk7)
| ~ ssList(sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(superposition,[status(thm)],[c_444,c_831]) ).
tcf(c_303363,plain,
( rearsegP(sk3,sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_303329,c_443]) ).
tcf(c_303575,plain,
! [X0: $i] :
( memberP(sk6,X0)
| ( hd(sk3) = X0 )
| ~ ssList(sk6)
| ~ memberP(app(sk3,sk6),X0) ),
inference(superposition,[status(thm)],[c_302506,c_301216]) ).
tcf(c_303640,plain,
! [X0: $i] :
( memberP(sk6,X0)
| ( hd(sk3) = X0 )
| ~ memberP(app(sk3,sk6),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_303575,c_442]) ).
tcf(c_304118,plain,
rearsegP(sk3,sk7),
inference(global_subsumption_just,[status(thm)],[c_303363,c_11315]) ).
tcf(c_304362,plain,
hd(sk3) = sk8,
inference(superposition,[status(thm)],[c_301466,c_302518]) ).
tcf(c_304736,plain,
( ( app(skaf46(sk3,sk7),sk7) = sk3 )
| ~ ssList(sk7)
| ~ ssList(sk3) ),
inference(superposition,[status(thm)],[c_304118,c_381]) ).
tcf(c_304758,plain,
app(skaf46(sk3,sk7),sk7) = sk3,
inference(forward_subsumption_resolution,[status(thm)],[c_304736,c_443,c_438]) ).
tcf(c_305863,plain,
! [X0: $i] :
( ( skaf46(sk3,sk7) = X0 )
| ~ ssList(sk7)
| ~ ssList(X0)
| ~ ssList(skaf46(sk3,sk7))
| ( app(X0,sk7) != sk3 ) ),
inference(superposition,[status(thm)],[c_304758,c_401]) ).
tcf(c_305919,plain,
! [X0: $i] :
( ( skaf46(sk3,sk7) = X0 )
| ~ ssList(X0)
| ( app(X0,sk7) != sk3 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_305863,c_443,c_300]) ).
tcf(c_307579,plain,
! [X0: $i] :
( ~ memberP(app(sk3,sk6),X0)
| ( hd(sk3) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_303640,c_442,c_441,c_258,c_13283,c_140235,c_141855,c_238968,c_303640]) ).
tcf(c_307580,plain,
! [X0: $i] :
( ( hd(sk3) = X0 )
| ~ memberP(app(sk3,sk6),X0) ),
inference(renaming,[status(thm)],[c_307579]) ).
tcf(c_307582,plain,
! [X0: $i] :
( ( X0 = sk8 )
| ~ memberP(app(sk3,sk6),X0) ),
inference(light_normalisation,[status(thm)],[c_307580,c_304362]) ).
tcf(c_307590,plain,
! [X0: $i] :
( ( X0 = sk8 )
| ~ memberP(sk3,X0) ),
inference(superposition,[status(thm)],[c_302527,c_307582]) ).
tcf(c_310262,plain,
( ( app(sk6,cons(sk5,nil)) = skaf46(sk3,sk7) )
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(superposition,[status(thm)],[c_444,c_305919]) ).
tcf(c_312284,plain,
app(sk6,cons(sk5,nil)) = skaf46(sk3,sk7),
inference(global_subsumption_just,[status(thm)],[c_310262,c_441,c_258,c_13283,c_126098]) ).
tcf(c_312300,plain,
! [X0: $i] :
( memberP(skaf46(sk3,sk7),X0)
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0) ),
inference(superposition,[status(thm)],[c_312284,c_301226]) ).
tcf(c_312322,plain,
! [X0: $i] :
( memberP(skaf46(sk3,sk7),X0)
| ~ ssList(cons(sk5,nil))
| ~ memberP(cons(sk5,nil),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_312300,c_442]) ).
tcf(c_312599,plain,
! [X0: $i] : ~ memberP(cons(sk5,nil),X0),
inference(global_subsumption_just,[status(thm)],[c_312322,c_445,c_441,c_258,c_449,c_9528,c_11884,c_12165,c_12305,c_13283,c_13285,c_27183,c_27248,c_28341,c_30415,c_50782,c_51003,c_51348,c_60785,c_77364,c_81623,c_89904,c_90632,c_95181,c_99825,c_99826,c_109627,c_138289,c_141435,c_221858,c_307590]) ).
tcf(c_312610,plain,
~ ssList(nil),
inference(superposition,[status(thm)],[c_301209,c_312599]) ).
tcf(c_312615,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_312610,c_258]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC285-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.37 % Computer : n002.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Thu Sep 24 17:27:49 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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.12/0.42
% 0.12/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.42
% 0.12/0.42 % Detected problem language: tptp
% 0.12/0.43 % Proving...
% 111.09/28.48 % SZS status Started for theBenchmark.p
% 111.09/28.48 % SZS status Unsatisfiable for theBenchmark.p
% 111.09/28.48
% 111.09/28.48 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 111.09/28.48
% 111.09/28.48 % ------ iProver source info
% 111.09/28.48
% 111.09/28.48 % git: date: 2026-07-19 20:42:38 +0200
% 111.09/28.48 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 111.09/28.48 % git: non_committed_changes: false
% 111.09/28.48
% 111.09/28.48 % ------ Parsing...% successful
% 111.09/28.48
% 111.09/28.48
% 111.09/28.48 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 111.09/28.48
% 111.09/28.48 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe_e sup_sim: 0 sf_s rm: 2 0s sf_e pe_s pe_e %
% 111.09/28.48
% 111.09/28.48 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 111.09/28.48
% 111.09/28.48 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 111.09/28.48 % ------ Proving...
% 111.09/28.48 % ------ Problem Properties
% 111.09/28.48
% 111.09/28.48 %
% 111.09/28.48 % clauses 190
% 111.09/28.48 % conjectures 12
% 111.09/28.48 % EPR 64
% 111.09/28.48 % Horn 160
% 111.09/28.48 % unary 66
% 111.09/28.48 % binary 26
% 111.09/28.48 % lits 559
% 111.09/28.48 % lits eq 71
% 111.09/28.48 % fd_pure 0
% 111.09/28.48 % fd_pseudo 0
% 111.09/28.48 % fd_cond 15
% 111.09/28.48 % fd_pseudo_cond 14
% 111.09/28.48 % AC symbols 0
% 111.09/28.48
% 111.09/28.48 % ------ Input Options Time Limit: Unbounded
% 111.09/28.48
% 111.09/28.48
% 111.09/28.48 % ------
% 111.09/28.48 % Current options:
% 111.09/28.48 % ------
% 111.09/28.48
% 111.09/28.48
% 111.09/28.48 %
% 111.09/28.48
% 111.09/28.48 % ------ Proving...
% 111.09/28.48 %
% 111.09/28.48
% 111.09/28.48 % SZS status Unsatisfiable for theBenchmark.p
% 111.09/28.48
% 111.09/28.48 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 111.09/28.49
% 111.09/28.49
%------------------------------------------------------------------------------