%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWC344-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 : n011.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:23 PM UTC 2026
% Result : Unsatisfiable 23.98s 4.27s
% Output : CNFRefutation 23.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 108
% Syntax : Number of formulae : 745 ( 27 unt; 0 def)
% Number of atoms : 4266 (1440 equ)
% Maximal formula atoms : 10 ( 5 avg)
% Number of connectives : 6199 (2678 ~;3521 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 8 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-2 aty)
% Number of variables : 1216 ( 0 sgn1216 !; 0 ?; 610 :)
% Comments :
%------------------------------------------------------------------------------
fof(f72,axiom,
! [X0,X1] :
( ssItem(X1)
| duplicatefreeP(X0)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f204,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_5) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
ssList(sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
ssList(sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
app(app(sk5,sk3),sk6) = sk4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_9) ).
fof(f209,plain,
sk4 = app(app(sk5,sk3),sk6),
inference(reorient_equations,[],[f208]) ).
fof(f210,negated_conjecture,
strictorderedP(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_10) ).
fof(f211,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ lt(X0,X2)
| app(cons(X2,nil),X3) != sk3
| ~ ssList(X3)
| ~ ssItem(X2)
| app(X1,cons(X0,nil)) != sk5
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).
fof(f212,plain,
! [X2,X3,X0,X1] :
( ~ lt(X0,X2)
| sk3 != app(cons(X2,nil),X3)
| ~ ssList(X3)
| ~ ssItem(X2)
| sk5 != app(X1,cons(X0,nil))
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(reorient_equations,[],[f211]) ).
fof(f213,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ lt(X2,X0)
| app(X3,cons(X2,nil)) != sk3
| ~ ssList(X3)
| ~ ssItem(X2)
| app(cons(X0,nil),X1) != sk6
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_12) ).
fof(f214,plain,
! [X2,X3,X0,X1] :
( ~ lt(X2,X0)
| sk3 != app(X3,cons(X2,nil))
| ~ ssList(X3)
| ~ ssItem(X2)
| app(cons(X0,nil),X1) != sk6
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(reorient_equations,[],[f213]) ).
fof(f215,negated_conjecture,
( nil != sk3
| nil = sk4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_13) ).
fof(f216,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| ssItem(sk7(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_14) ).
fof(f217,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| ssItem(sk7(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f216]) ).
fof(f218,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| ssItem(sk7(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_15) ).
fof(f219,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| ssItem(sk7(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f218]) ).
fof(f220,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| ssItem(sk7(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_16) ).
fof(f221,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| ssItem(sk7(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f220]) ).
fof(f222,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssItem(sk7(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_17) ).
fof(f223,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssItem(sk7(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f222]) ).
fof(f224,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| ssItem(sk7(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_18) ).
fof(f225,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| ssItem(sk7(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f224]) ).
fof(f226,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| ssItem(sk7(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_19) ).
fof(f227,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| ssItem(sk7(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f226]) ).
fof(f228,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk1
| ssItem(sk7(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_20) ).
fof(f229,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| sk1 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| ssItem(sk7(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f228]) ).
fof(f230,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssItem(sk7(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_21) ).
fof(f231,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssItem(sk7(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f230]) ).
fof(f232,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| ssList(sk8(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_22) ).
fof(f233,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| ssList(sk8(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f232]) ).
fof(f234,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_23) ).
fof(f235,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f234]) ).
fof(f236,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| ssItem(sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_24) ).
fof(f237,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| ssItem(sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f236]) ).
fof(f238,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| ssList(sk10(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_25) ).
fof(f239,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| ssList(sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f238]) ).
fof(f240,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk1
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_26) ).
fof(f241,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| sk1 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f240]) ).
fof(f242,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_27) ).
fof(f243,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f242]) ).
fof(f244,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| ssList(sk8(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_28) ).
fof(f245,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| ssList(sk8(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f244]) ).
fof(f246,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssList(sk8(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_29) ).
fof(f247,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssList(sk8(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f246]) ).
fof(f248,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| ssList(sk8(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_30) ).
fof(f249,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| ssList(sk8(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f248]) ).
fof(f250,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| ssList(sk8(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_31) ).
fof(f251,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| ssList(sk8(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f250]) ).
fof(f252,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk1
| ssList(sk8(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_32) ).
fof(f253,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| sk1 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| ssList(sk8(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f252]) ).
fof(f254,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssList(sk8(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_33) ).
fof(f255,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssList(sk8(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f254]) ).
fof(f256,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_34) ).
fof(f257,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f256]) ).
fof(f258,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| ssItem(sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_35) ).
fof(f259,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| ssItem(sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f258]) ).
fof(f260,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| ssList(sk10(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_36) ).
fof(f261,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| ssList(sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f260]) ).
fof(f262,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk1
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_37) ).
fof(f263,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| sk1 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f262]) ).
fof(f264,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_38) ).
fof(f265,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f264]) ).
fof(f266,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_39) ).
fof(f267,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f266]) ).
fof(f268,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_40) ).
fof(f269,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f268]) ).
fof(f270,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_41) ).
fof(f271,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f270]) ).
fof(f272,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk1
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_42) ).
fof(f273,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| sk1 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f272]) ).
fof(f274,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_43) ).
fof(f275,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f274]) ).
fof(f276,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssItem(sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_44) ).
fof(f277,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssItem(sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f276]) ).
fof(f278,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssList(sk10(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_45) ).
fof(f279,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssList(sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f278]) ).
fof(f280,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk1
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_46) ).
fof(f281,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| sk1 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f280]) ).
fof(f282,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| lt(sk7(X1,X0),sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_47) ).
fof(f283,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| lt(sk7(X1,X0),sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f282]) ).
fof(f284,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| ssItem(sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_48) ).
fof(f285,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| ssItem(sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f284]) ).
fof(f286,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| ssItem(sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_49) ).
fof(f287,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| ssItem(sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f286]) ).
fof(f288,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk1
| ssItem(sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_50) ).
fof(f289,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| sk1 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| ssItem(sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f288]) ).
fof(f290,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssItem(sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_51) ).
fof(f291,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssItem(sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f290]) ).
fof(f292,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| ssList(sk10(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_52) ).
fof(f293,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| ssList(sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f292]) ).
fof(f294,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk1
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_53) ).
fof(f295,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| sk1 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f294]) ).
fof(f296,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_54) ).
fof(f297,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f296]) ).
fof(f298,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| ssList(sk10(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_55) ).
fof(f299,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| ssList(sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f298]) ).
fof(f300,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk1
| ssList(sk10(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_56) ).
fof(f301,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| sk1 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| ssList(sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f300]) ).
fof(f302,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssList(sk10(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_57) ).
fof(f303,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssList(sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f302]) ).
fof(f304,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk1
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_58) ).
fof(f305,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| sk1 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f304]) ).
fof(f306,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_59) ).
fof(f307,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f306]) ).
fof(f308,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk1
| app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk1
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_60) ).
fof(f309,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| sk1 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| sk1 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f308]) ).
fof(f310,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk1
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_61) ).
fof(f311,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| sk1 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f310]) ).
fof(f312,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk1
| lt(sk7(X1,X0),sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_62) ).
fof(f313,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| sk1 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f312]) ).
fof(f314,negated_conjecture,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_63) ).
fof(f315,plain,
! [X0,X1] :
( nil = sk1
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f314]) ).
fof(f316,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| ssItem(sk7(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_64) ).
fof(f317,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| ssItem(sk7(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f316]) ).
fof(f318,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssItem(sk7(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_65) ).
fof(f319,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssItem(sk7(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f318]) ).
fof(f320,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| ssItem(sk7(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_66) ).
fof(f321,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| ssItem(sk7(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f320]) ).
fof(f322,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| ssItem(sk7(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_67) ).
fof(f323,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| ssItem(sk7(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f322]) ).
fof(f324,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk1
| ssItem(sk7(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_68) ).
fof(f325,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| sk1 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| ssItem(sk7(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f324]) ).
fof(f326,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssItem(sk7(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_69) ).
fof(f327,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssItem(sk7(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f326]) ).
fof(f328,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| ssList(sk8(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_70) ).
fof(f329,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| ssList(sk8(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f328]) ).
fof(f330,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_71) ).
fof(f331,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f330]) ).
fof(f332,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| ssItem(sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_72) ).
fof(f333,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| ssItem(sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f332]) ).
fof(f334,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| ssList(sk10(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_73) ).
fof(f335,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| ssList(sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f334]) ).
fof(f336,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk1
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_74) ).
fof(f337,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| sk1 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f336]) ).
fof(f338,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_75) ).
fof(f339,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f338]) ).
fof(f340,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| ssList(sk8(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_76) ).
fof(f341,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| ssList(sk8(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f340]) ).
fof(f342,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssList(sk8(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_77) ).
fof(f343,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssList(sk8(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f342]) ).
fof(f344,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| ssList(sk8(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_78) ).
fof(f345,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| ssList(sk8(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f344]) ).
fof(f346,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| ssList(sk8(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_79) ).
fof(f347,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| ssList(sk8(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f346]) ).
fof(f348,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk1
| ssList(sk8(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_80) ).
fof(f349,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| sk1 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| ssList(sk8(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f348]) ).
fof(f350,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssList(sk8(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_81) ).
fof(f351,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssList(sk8(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f350]) ).
fof(f352,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_82) ).
fof(f353,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f352]) ).
fof(f354,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| ssItem(sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_83) ).
fof(f355,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| ssItem(sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f354]) ).
fof(f356,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| ssList(sk10(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_84) ).
fof(f357,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| ssList(sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f356]) ).
fof(f358,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk1
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_85) ).
fof(f359,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| sk1 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f358]) ).
fof(f360,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_86) ).
fof(f361,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk12(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f360]) ).
fof(f362,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_87) ).
fof(f363,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f362]) ).
fof(f364,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_88) ).
fof(f365,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f364]) ).
fof(f366,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_89) ).
fof(f367,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f366]) ).
fof(f368,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk1
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_90) ).
fof(f369,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| sk1 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f368]) ).
fof(f370,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_91) ).
fof(f371,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f370]) ).
fof(f372,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssItem(sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_92) ).
fof(f373,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssItem(sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f372]) ).
fof(f374,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssList(sk10(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_93) ).
fof(f375,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssList(sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f374]) ).
fof(f376,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk1
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_94) ).
fof(f377,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| sk1 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f376]) ).
fof(f378,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| lt(sk7(X1,X0),sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_95) ).
fof(f379,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| lt(sk7(X1,X0),sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f378]) ).
fof(f380,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| ssItem(sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_96) ).
fof(f381,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| ssItem(sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f380]) ).
fof(f382,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| ssItem(sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_97) ).
fof(f383,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| ssItem(sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f382]) ).
fof(f384,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk1
| ssItem(sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_98) ).
fof(f385,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| sk1 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| ssItem(sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f384]) ).
fof(f386,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssItem(sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_99) ).
fof(f387,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssItem(sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f386]) ).
fof(f388,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| ssList(sk10(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_100) ).
fof(f389,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| ssList(sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f388]) ).
fof(f390,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk1
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_101) ).
fof(f391,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| sk1 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f390]) ).
fof(f392,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_102) ).
fof(f393,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssItem(sk13(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f392]) ).
fof(f394,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| ssList(sk10(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_103) ).
fof(f395,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| ssList(sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f394]) ).
fof(f396,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk1
| ssList(sk10(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_104) ).
fof(f397,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| sk1 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| ssList(sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f396]) ).
fof(f398,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssList(sk10(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_105) ).
fof(f399,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssList(sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f398]) ).
fof(f400,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk1
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_106) ).
fof(f401,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| sk1 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f400]) ).
fof(f402,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_107) ).
fof(f403,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| ssList(sk14(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f402]) ).
fof(f404,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk1
| app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk1
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_108) ).
fof(f405,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| sk1 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| sk1 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f404]) ).
fof(f406,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk1
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_109) ).
fof(f407,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| sk1 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f406]) ).
fof(f408,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk1
| lt(sk7(X1,X0),sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_110) ).
fof(f409,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| sk1 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f408]) ).
fof(f410,negated_conjecture,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| app(app(X0,sk1),X1) != sk2
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_111) ).
fof(f411,plain,
! [X0,X1] :
( nil != sk2
| ~ strictorderedP(sk1)
| lt(sk13(X1,X0),sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk2 != app(app(X0,sk1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(reorient_equations,[],[f410]) ).
fof(f414,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssItem(sk11(X1,X0))
| ssItem(sk7(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f217,f204,f205,f205,f205]) ).
fof(f415,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssItem(sk11(X1,X0))
| ssItem(sk7(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f219,f204,f205,f205,f204]) ).
fof(f416,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssList(sk12(X1,X0))
| ssItem(sk7(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f221,f204,f205,f205,f205]) ).
fof(f417,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssItem(sk7(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f223,f204,f205,f205,f205]) ).
fof(f418,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssItem(sk13(X1,X0))
| ssItem(sk7(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f225,f204,f205,f205,f205]) ).
fof(f419,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssList(sk14(X1,X0))
| ssItem(sk7(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f227,f204,f205,f205,f205]) ).
fof(f420,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| sk3 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| ssItem(sk7(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f229,f204,f205,f205,f205,f205]) ).
fof(f421,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssItem(sk7(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f231,f204,f205,f205,f205]) ).
fof(f422,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssItem(sk11(X1,X0))
| ssList(sk8(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f233,f204,f205,f205,f205]) ).
fof(f423,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssItem(sk11(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f235,f204,f205,f205,f205]) ).
fof(f424,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssItem(sk11(X1,X0))
| ssItem(sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f237,f204,f205,f205,f205]) ).
fof(f425,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssItem(sk11(X1,X0))
| ssList(sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f239,f204,f205,f205,f205]) ).
fof(f426,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssItem(sk11(X1,X0))
| sk3 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f241,f204,f205,f205,f205,f205]) ).
fof(f427,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssItem(sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f243,f204,f205,f205,f205]) ).
fof(f428,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssList(sk12(X1,X0))
| ssList(sk8(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f245,f204,f205,f205,f205]) ).
fof(f429,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssList(sk8(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f247,f204,f205,f205,f205]) ).
fof(f430,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssItem(sk13(X1,X0))
| ssList(sk8(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f249,f204,f205,f205,f205]) ).
fof(f431,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssList(sk14(X1,X0))
| ssList(sk8(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f251,f204,f205,f205,f205]) ).
fof(f432,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| sk3 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| ssList(sk8(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f253,f204,f205,f205,f205,f205]) ).
fof(f433,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssList(sk8(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f255,f204,f205,f205,f205]) ).
fof(f434,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssList(sk12(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f257,f204,f205,f205,f205]) ).
fof(f435,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssList(sk12(X1,X0))
| ssItem(sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f259,f204,f205,f205,f205]) ).
fof(f436,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssList(sk12(X1,X0))
| ssList(sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f261,f204,f205,f205,f205]) ).
fof(f437,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssList(sk12(X1,X0))
| sk3 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f263,f204,f205,f205,f205,f205]) ).
fof(f438,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssList(sk12(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f265,f204,f205,f205,f205]) ).
fof(f439,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f267,f204,f205,f205,f205]) ).
fof(f440,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssItem(sk13(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f269,f204,f205,f205,f205]) ).
fof(f441,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssList(sk14(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f271,f204,f205,f205,f205]) ).
fof(f442,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| sk3 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f273,f204,f205,f205,f205,f205]) ).
fof(f443,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| lt(sk13(X1,X0),sk11(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f275,f204,f205,f205,f205]) ).
fof(f444,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssItem(sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f277,f204,f205,f205,f205]) ).
fof(f445,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssList(sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f279,f204,f205,f205,f205]) ).
fof(f446,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| sk3 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f281,f204,f205,f205,f205,f205]) ).
fof(f447,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| lt(sk7(X1,X0),sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f283,f204,f205,f205,f205]) ).
fof(f448,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssItem(sk13(X1,X0))
| ssItem(sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f285,f204,f205,f205,f205]) ).
fof(f449,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssList(sk14(X1,X0))
| ssItem(sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f287,f204,f205,f205,f205]) ).
fof(f450,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| sk3 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| ssItem(sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f289,f204,f205,f205,f205,f205]) ).
fof(f451,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssItem(sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f291,f204,f205,f205,f205]) ).
fof(f452,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssItem(sk13(X1,X0))
| ssList(sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f293,f204,f205,f205,f205]) ).
fof(f453,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssItem(sk13(X1,X0))
| sk3 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f295,f204,f205,f205,f205,f205]) ).
fof(f454,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssItem(sk13(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f297,f204,f205,f205,f205]) ).
fof(f455,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssList(sk14(X1,X0))
| ssList(sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f299,f204,f205,f205,f205]) ).
fof(f456,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| sk3 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| ssList(sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f301,f204,f205,f205,f205,f205]) ).
fof(f457,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssList(sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f303,f204,f205,f205,f205]) ).
fof(f458,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssList(sk14(X1,X0))
| sk3 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f305,f204,f205,f205,f205,f205]) ).
fof(f459,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| ssList(sk14(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f307,f204,f205,f205,f205]) ).
fof(f460,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| sk3 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| sk3 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f309,f204,f205,f205,f205,f205,f205]) ).
fof(f461,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| lt(sk13(X1,X0),sk11(X1,X0))
| sk3 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f311,f204,f205,f205,f205,f205]) ).
fof(f462,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| sk3 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f313,f204,f205,f205,f205,f205]) ).
fof(f463,plain,
! [X0,X1] :
( nil = sk3
| ~ strictorderedP(sk3)
| lt(sk13(X1,X0),sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f315,f204,f205,f205,f205]) ).
fof(f464,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssList(sk12(X1,X0))
| ssItem(sk7(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f317,f204,f205,f205,f204]) ).
fof(f465,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssItem(sk7(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f319,f204,f205,f205,f204]) ).
fof(f466,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssItem(sk13(X1,X0))
| ssItem(sk7(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f321,f204,f205,f205,f204]) ).
fof(f467,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssList(sk14(X1,X0))
| ssItem(sk7(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f323,f204,f205,f205,f204]) ).
fof(f468,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| sk3 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| ssItem(sk7(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f325,f204,f205,f205,f205,f204]) ).
fof(f469,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssItem(sk7(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f327,f204,f205,f205,f204]) ).
fof(f470,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssItem(sk11(X1,X0))
| ssList(sk8(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f329,f204,f205,f205,f204]) ).
fof(f471,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssItem(sk11(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f331,f204,f205,f205,f204]) ).
fof(f472,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssItem(sk11(X1,X0))
| ssItem(sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f333,f204,f205,f205,f204]) ).
fof(f473,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssItem(sk11(X1,X0))
| ssList(sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f335,f204,f205,f205,f204]) ).
fof(f474,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssItem(sk11(X1,X0))
| sk3 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f337,f204,f205,f205,f205,f204]) ).
fof(f475,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssItem(sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f339,f204,f205,f205,f204]) ).
fof(f476,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssList(sk12(X1,X0))
| ssList(sk8(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f341,f204,f205,f205,f204]) ).
fof(f477,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssList(sk8(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f343,f204,f205,f205,f204]) ).
fof(f478,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssItem(sk13(X1,X0))
| ssList(sk8(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f345,f204,f205,f205,f204]) ).
fof(f479,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssList(sk14(X1,X0))
| ssList(sk8(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f347,f204,f205,f205,f204]) ).
fof(f480,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| sk3 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| ssList(sk8(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f349,f204,f205,f205,f205,f204]) ).
fof(f481,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssList(sk8(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f351,f204,f205,f205,f204]) ).
fof(f482,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssList(sk12(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f353,f204,f205,f205,f204]) ).
fof(f483,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssList(sk12(X1,X0))
| ssItem(sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f355,f204,f205,f205,f204]) ).
fof(f484,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssList(sk12(X1,X0))
| ssList(sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f357,f204,f205,f205,f204]) ).
fof(f485,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssList(sk12(X1,X0))
| sk3 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f359,f204,f205,f205,f205,f204]) ).
fof(f486,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssList(sk12(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f361,f204,f205,f205,f204]) ).
fof(f487,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f363,f204,f205,f205,f204]) ).
fof(f488,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssItem(sk13(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f365,f204,f205,f205,f204]) ).
fof(f489,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssList(sk14(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f367,f204,f205,f205,f204]) ).
fof(f490,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| sk3 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f369,f204,f205,f205,f205,f204]) ).
fof(f491,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| lt(sk13(X1,X0),sk11(X1,X0))
| app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f371,f204,f205,f205,f204]) ).
fof(f492,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssItem(sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f373,f204,f205,f205,f204]) ).
fof(f493,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| ssList(sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f375,f204,f205,f205,f204]) ).
fof(f494,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| sk3 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f377,f204,f205,f205,f205,f204]) ).
fof(f495,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1
| lt(sk7(X1,X0),sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f379,f204,f205,f205,f204]) ).
fof(f496,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssItem(sk13(X1,X0))
| ssItem(sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f381,f204,f205,f205,f204]) ).
fof(f497,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssList(sk14(X1,X0))
| ssItem(sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f383,f204,f205,f205,f204]) ).
fof(f498,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| sk3 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| ssItem(sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f385,f204,f205,f205,f205,f204]) ).
fof(f499,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssItem(sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f387,f204,f205,f205,f204]) ).
fof(f500,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssItem(sk13(X1,X0))
| ssList(sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f389,f204,f205,f205,f204]) ).
fof(f501,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssItem(sk13(X1,X0))
| sk3 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f391,f204,f205,f205,f205,f204]) ).
fof(f502,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssItem(sk13(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f393,f204,f205,f205,f204]) ).
fof(f503,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssList(sk14(X1,X0))
| ssList(sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f395,f204,f205,f205,f204]) ).
fof(f504,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| sk3 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| ssList(sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f397,f204,f205,f205,f205,f204]) ).
fof(f505,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| lt(sk13(X1,X0),sk11(X1,X0))
| ssList(sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f399,f204,f205,f205,f204]) ).
fof(f506,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssList(sk14(X1,X0))
| sk3 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f401,f204,f205,f205,f205,f204]) ).
fof(f507,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| ssList(sk14(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f403,f204,f205,f205,f204]) ).
fof(f508,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| sk3 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| sk3 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f405,f204,f205,f205,f205,f205,f204]) ).
fof(f509,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| lt(sk13(X1,X0),sk11(X1,X0))
| sk3 = app(cons(sk9(X1,X0),nil),sk10(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f407,f204,f205,f205,f205,f204]) ).
fof(f510,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| sk3 = app(sk14(X1,X0),cons(sk13(X1,X0),nil))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f409,f204,f205,f205,f205,f204]) ).
fof(f511,plain,
! [X0,X1] :
( nil != sk4
| ~ strictorderedP(sk3)
| lt(sk13(X1,X0),sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| sk4 != app(app(X0,sk3),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(definition_unfolding,[],[f411,f204,f205,f205,f204]) ).
tcf(c_416,plain,
! [X0: $i,X1: $i] :
( duplicatefreeP(X0)
| ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_534,negated_conjecture,
ssList(sk5),
inference(cnf_transformation,[],[f206]) ).
tcf(c_535,negated_conjecture,
ssList(sk6),
inference(cnf_transformation,[],[f207]) ).
tcf(c_536,negated_conjecture,
app(app(sk5,sk3),sk6) = sk4,
inference(cnf_transformation,[],[f209]) ).
tcf(c_537,negated_conjecture,
strictorderedP(sk3),
inference(cnf_transformation,[],[f210]) ).
tcf(c_538,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ssItem(X3)
| ~ ssItem(X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ lt(X3,X0)
| ( app(X2,cons(X3,nil)) != sk5 )
| ( app(cons(X0,nil),X1) != sk3 ) ),
inference(cnf_transformation,[],[f212]) ).
tcf(c_539,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ssItem(X3)
| ~ ssItem(X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ lt(X3,X0)
| ( app(X2,cons(X3,nil)) != sk3 )
| ( app(cons(X0,nil),X1) != sk6 ) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_540,negated_conjecture,
( ( sk4 = nil )
| ( sk3 != nil ) ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_541,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ssItem(sk7(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f414]) ).
tcf(c_542,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ssItem(sk7(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f415]) ).
tcf(c_543,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ssList(sk12(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f416]) ).
tcf(c_544,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ( sk3 = nil )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f417]) ).
tcf(c_545,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ssItem(sk7(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f418]) ).
tcf(c_546,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ssList(sk14(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f419]) ).
tcf(c_547,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ( sk3 = nil )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f420]) ).
tcf(c_548,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f421]) ).
tcf(c_549,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ssList(sk8(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f422]) ).
tcf(c_550,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ( sk3 = nil )
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f423]) ).
tcf(c_551,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ssItem(sk11(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f424]) ).
tcf(c_552,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ssList(sk10(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f425]) ).
tcf(c_553,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ( sk3 = nil )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f426]) ).
tcf(c_554,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f427]) ).
tcf(c_555,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ssList(sk12(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f428]) ).
tcf(c_556,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ( sk3 = nil )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f429]) ).
tcf(c_557,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ssList(sk8(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f430]) ).
tcf(c_558,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ssList(sk14(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f431]) ).
tcf(c_559,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ( sk3 = nil )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f432]) ).
tcf(c_560,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f433]) ).
tcf(c_561,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| ( sk3 = nil )
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f434]) ).
tcf(c_562,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ssList(sk12(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f435]) ).
tcf(c_563,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ssList(sk12(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f436]) ).
tcf(c_564,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| ( sk3 = nil )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f437]) ).
tcf(c_565,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f438]) ).
tcf(c_566,negated_conjecture,
! [X0: $i,X1: $i] :
( ( sk3 = nil )
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f439]) ).
tcf(c_567,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ( sk3 = nil )
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f440]) ).
tcf(c_568,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| ( sk3 = nil )
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f441]) ).
tcf(c_569,negated_conjecture,
! [X0: $i,X1: $i] :
( ( sk3 = nil )
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f442]) ).
tcf(c_570,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| ( sk3 = nil )
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f443]) ).
tcf(c_571,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ( sk3 = nil )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f444]) ).
tcf(c_572,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ( sk3 = nil )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f445]) ).
tcf(c_573,negated_conjecture,
! [X0: $i,X1: $i] :
( ( sk3 = nil )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f446]) ).
tcf(c_574,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk7(X1,X0),sk9(X1,X0))
| ( sk3 = nil )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f447]) ).
tcf(c_575,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ssItem(sk13(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f448]) ).
tcf(c_576,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ssList(sk14(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f449]) ).
tcf(c_577,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ( sk3 = nil )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f450]) ).
tcf(c_578,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f451]) ).
tcf(c_579,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ssList(sk10(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f452]) ).
tcf(c_580,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ( sk3 = nil )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f453]) ).
tcf(c_581,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f454]) ).
tcf(c_582,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ssList(sk14(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f455]) ).
tcf(c_583,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ( sk3 = nil )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f456]) ).
tcf(c_584,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f457]) ).
tcf(c_585,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| ( sk3 = nil )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f458]) ).
tcf(c_586,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f459]) ).
tcf(c_587,negated_conjecture,
! [X0: $i,X1: $i] :
( ( sk3 = nil )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f460]) ).
tcf(c_588,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| ( sk3 = nil )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f461]) ).
tcf(c_589,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk7(X1,X0),sk9(X1,X0))
| ( sk3 = nil )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f462]) ).
tcf(c_590,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ( sk3 = nil )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f463]) ).
tcf(c_591,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ssList(sk12(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f464]) ).
tcf(c_592,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f465]) ).
tcf(c_593,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ssItem(sk7(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f466]) ).
tcf(c_594,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ssList(sk14(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f467]) ).
tcf(c_595,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f468]) ).
tcf(c_596,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f469]) ).
tcf(c_597,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ssList(sk8(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f470]) ).
tcf(c_598,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f471]) ).
tcf(c_599,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ssItem(sk11(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f472]) ).
tcf(c_600,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ssList(sk10(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f473]) ).
tcf(c_601,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f474]) ).
tcf(c_602,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f475]) ).
tcf(c_603,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ssList(sk12(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f476]) ).
tcf(c_604,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f477]) ).
tcf(c_605,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ssList(sk8(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f478]) ).
tcf(c_606,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ssList(sk14(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f479]) ).
tcf(c_607,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f480]) ).
tcf(c_608,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f481]) ).
tcf(c_609,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f482]) ).
tcf(c_610,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ssList(sk12(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f483]) ).
tcf(c_611,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ssList(sk12(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f484]) ).
tcf(c_612,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f485]) ).
tcf(c_613,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f486]) ).
tcf(c_614,negated_conjecture,
! [X0: $i,X1: $i] :
( ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f487]) ).
tcf(c_615,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f488]) ).
tcf(c_616,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f489]) ).
tcf(c_617,negated_conjecture,
! [X0: $i,X1: $i] :
( ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f490]) ).
tcf(c_618,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f491]) ).
tcf(c_619,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f492]) ).
tcf(c_620,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f493]) ).
tcf(c_621,negated_conjecture,
! [X0: $i,X1: $i] :
( ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f494]) ).
tcf(c_622,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk7(X1,X0),sk9(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f495]) ).
tcf(c_623,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ssItem(sk13(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f496]) ).
tcf(c_624,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ssList(sk14(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f497]) ).
tcf(c_625,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f498]) ).
tcf(c_626,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f499]) ).
tcf(c_627,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ssList(sk10(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f500]) ).
tcf(c_628,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f501]) ).
tcf(c_629,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f502]) ).
tcf(c_630,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ssList(sk14(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f503]) ).
tcf(c_631,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f504]) ).
tcf(c_632,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f505]) ).
tcf(c_633,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f506]) ).
tcf(c_634,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f507]) ).
tcf(c_635,negated_conjecture,
! [X0: $i,X1: $i] :
( ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f508]) ).
tcf(c_636,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f509]) ).
tcf(c_637,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk7(X1,X0),sk9(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f510]) ).
tcf(c_638,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ~ strictorderedP(sk3)
| ~ ssList(X1)
| ~ ssList(X0)
| ( sk4 != nil )
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(cnf_transformation,[],[f511]) ).
tcf(c_856,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ssList(sk14(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_582,c_537,c_540,c_582,c_630]) ).
tcf(c_859,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ssList(sk10(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_579,c_537,c_540,c_579,c_627]) ).
tcf(c_862,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ssList(sk14(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_576,c_537,c_540,c_576,c_624]) ).
tcf(c_865,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ssItem(sk13(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_575,c_537,c_540,c_575,c_623]) ).
tcf(c_868,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ssList(sk12(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_563,c_537,c_540,c_563,c_611]) ).
tcf(c_871,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ssList(sk12(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_562,c_537,c_540,c_562,c_610]) ).
tcf(c_874,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ssList(sk14(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_558,c_537,c_540,c_558,c_606]) ).
tcf(c_877,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ssList(sk8(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_557,c_537,c_540,c_557,c_605]) ).
tcf(c_880,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ssList(sk12(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_555,c_537,c_540,c_555,c_603]) ).
tcf(c_883,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ssList(sk10(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_552,c_537,c_540,c_552,c_600]) ).
tcf(c_886,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ssItem(sk11(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_551,c_537,c_540,c_551,c_599]) ).
tcf(c_889,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ssList(sk8(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_549,c_537,c_540,c_549,c_597]) ).
tcf(c_892,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ssList(sk14(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_546,c_537,c_540,c_546,c_594]) ).
tcf(c_895,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ssItem(sk7(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_545,c_537,c_540,c_545,c_593]) ).
tcf(c_898,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ssList(sk12(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_543,c_537,c_540,c_543,c_591]) ).
tcf(c_901,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ssItem(sk7(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_541,c_537,c_540,c_541,c_542]) ).
tcf(c_916,plain,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ssList(sk14(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_606,c_874]) ).
tcf(c_917,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ssList(sk14(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_916]) ).
tcf(c_918,plain,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ssList(sk8(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_605,c_877]) ).
tcf(c_919,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ssList(sk8(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_918]) ).
tcf(c_920,plain,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ssList(sk12(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_603,c_880]) ).
tcf(c_921,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ssList(sk12(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_920]) ).
tcf(c_922,plain,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ssList(sk10(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_600,c_883]) ).
tcf(c_923,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ssList(sk10(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_922]) ).
tcf(c_924,plain,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ssItem(sk11(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_599,c_886]) ).
tcf(c_925,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ssItem(sk11(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_924]) ).
tcf(c_926,plain,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ssList(sk8(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_597,c_889]) ).
tcf(c_927,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ssList(sk8(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_926]) ).
tcf(c_928,plain,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ssList(sk14(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_594,c_892]) ).
tcf(c_929,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ssList(sk14(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_928]) ).
tcf(c_930,plain,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ssItem(sk7(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_593,c_895]) ).
tcf(c_931,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ssItem(sk7(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_930]) ).
tcf(c_932,plain,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ssList(sk12(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_591,c_898]) ).
tcf(c_933,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ssList(sk12(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_932]) ).
tcf(c_934,plain,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ssItem(sk7(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_542,c_901]) ).
tcf(c_935,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ssItem(sk7(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_934]) ).
tcf(c_936,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_586,c_537,c_540,c_586,c_634]) ).
tcf(c_939,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_584,c_537,c_540,c_584,c_632]) ).
tcf(c_942,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_581,c_537,c_540,c_581,c_629]) ).
tcf(c_945,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_578,c_537,c_540,c_578,c_626]) ).
tcf(c_948,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_565,c_537,c_540,c_565,c_613]) ).
tcf(c_951,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_560,c_537,c_540,c_560,c_608]) ).
tcf(c_954,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_554,c_537,c_540,c_554,c_602]) ).
tcf(c_957,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_548,c_537,c_540,c_548,c_596]) ).
tcf(c_960,plain,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_634,c_936]) ).
tcf(c_961,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_960]) ).
tcf(c_962,plain,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_632,c_939]) ).
tcf(c_963,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_962]) ).
tcf(c_964,plain,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_629,c_942]) ).
tcf(c_965,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_964]) ).
tcf(c_966,plain,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_626,c_945]) ).
tcf(c_967,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_966]) ).
tcf(c_968,plain,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_613,c_948]) ).
tcf(c_969,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_968]) ).
tcf(c_970,plain,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_608,c_951]) ).
tcf(c_971,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_970]) ).
tcf(c_972,plain,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_602,c_954]) ).
tcf(c_973,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_972]) ).
tcf(c_974,plain,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_596,c_957]) ).
tcf(c_975,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| lt(sk13(X1,X0),sk11(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_974]) ).
tcf(c_976,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_590,c_537,c_540,c_590,c_638]) ).
tcf(c_979,plain,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_638,c_976]) ).
tcf(c_980,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| lt(sk7(X1,X0),sk9(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_979]) ).
tcf(c_981,plain,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_585,c_537,c_540,c_585,c_633]) ).
tcf(c_982,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_981]) ).
tcf(c_984,plain,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_583,c_537,c_540,c_583,c_631]) ).
tcf(c_985,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_984]) ).
tcf(c_987,plain,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_580,c_537,c_540,c_580,c_628]) ).
tcf(c_988,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_987]) ).
tcf(c_990,plain,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_577,c_537,c_540,c_577,c_625]) ).
tcf(c_991,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_990]) ).
tcf(c_993,plain,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 ) ),
inference(global_subsumption_just,[status(thm)],[c_572,c_537,c_540,c_572,c_620]) ).
tcf(c_994,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_993]) ).
tcf(c_996,plain,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 ) ),
inference(global_subsumption_just,[status(thm)],[c_571,c_537,c_540,c_571,c_619]) ).
tcf(c_997,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_996]) ).
tcf(c_999,plain,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_568,c_537,c_540,c_568,c_616]) ).
tcf(c_1000,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_999]) ).
tcf(c_1002,plain,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_567,c_537,c_540,c_567,c_615]) ).
tcf(c_1003,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1002]) ).
tcf(c_1005,plain,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_564,c_537,c_540,c_564,c_612]) ).
tcf(c_1006,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1005]) ).
tcf(c_1008,plain,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_561,c_537,c_540,c_561,c_609]) ).
tcf(c_1009,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1008]) ).
tcf(c_1011,plain,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_559,c_537,c_540,c_559,c_607]) ).
tcf(c_1012,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1011]) ).
tcf(c_1014,plain,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 ) ),
inference(global_subsumption_just,[status(thm)],[c_556,c_537,c_540,c_556,c_604]) ).
tcf(c_1015,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1014]) ).
tcf(c_1017,plain,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_553,c_537,c_540,c_553,c_601]) ).
tcf(c_1018,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1017]) ).
tcf(c_1020,plain,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_550,c_537,c_540,c_550,c_598]) ).
tcf(c_1021,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1020]) ).
tcf(c_1023,plain,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_547,c_537,c_540,c_547,c_595]) ).
tcf(c_1024,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1023]) ).
tcf(c_1026,plain,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 ) ),
inference(global_subsumption_just,[status(thm)],[c_544,c_537,c_540,c_544,c_592]) ).
tcf(c_1027,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1026]) ).
tcf(c_1029,plain,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_633,c_982]) ).
tcf(c_1030,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1029]) ).
tcf(c_1031,plain,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_631,c_985]) ).
tcf(c_1032,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1031]) ).
tcf(c_1033,plain,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_628,c_988]) ).
tcf(c_1034,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1033]) ).
tcf(c_1035,plain,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_625,c_991]) ).
tcf(c_1036,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1035]) ).
tcf(c_1037,plain,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_620,c_994]) ).
tcf(c_1038,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk10(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1037]) ).
tcf(c_1039,plain,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_619,c_997]) ).
tcf(c_1040,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk9(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1039]) ).
tcf(c_1041,plain,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_616,c_1000]) ).
tcf(c_1042,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk14(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1041]) ).
tcf(c_1043,plain,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_615,c_1003]) ).
tcf(c_1044,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk13(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1043]) ).
tcf(c_1045,plain,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_612,c_1006]) ).
tcf(c_1046,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1045]) ).
tcf(c_1047,plain,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_609,c_1009]) ).
tcf(c_1048,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk12(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1047]) ).
tcf(c_1049,plain,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_607,c_1012]) ).
tcf(c_1050,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1049]) ).
tcf(c_1051,plain,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_604,c_1015]) ).
tcf(c_1052,negated_conjecture,
! [X0: $i,X1: $i] :
( ssList(sk8(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1051]) ).
tcf(c_1053,plain,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_601,c_1018]) ).
tcf(c_1054,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1053]) ).
tcf(c_1055,plain,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_598,c_1021]) ).
tcf(c_1056,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk11(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1055]) ).
tcf(c_1057,plain,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_595,c_1024]) ).
tcf(c_1058,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1057]) ).
tcf(c_1059,plain,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_592,c_1027]) ).
tcf(c_1060,negated_conjecture,
! [X0: $i,X1: $i] :
( ssItem(sk7(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1059]) ).
tcf(c_1061,plain,
! [X0: $i,X1: $i] :
( lt(sk7(X1,X0),sk9(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_589,c_537,c_540,c_589,c_637]) ).
tcf(c_1062,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk7(X1,X0),sk9(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1061]) ).
tcf(c_1064,plain,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_588,c_537,c_540,c_588,c_636]) ).
tcf(c_1065,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1064]) ).
tcf(c_1067,plain,
! [X0: $i,X1: $i] :
( lt(sk7(X1,X0),sk9(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 ) ),
inference(global_subsumption_just,[status(thm)],[c_574,c_537,c_540,c_574,c_622]) ).
tcf(c_1068,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk7(X1,X0),sk9(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1067]) ).
tcf(c_1070,plain,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_570,c_537,c_540,c_570,c_618]) ).
tcf(c_1071,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1070]) ).
tcf(c_1073,plain,
! [X0: $i,X1: $i] :
( lt(sk7(X1,X0),sk9(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_637,c_1062]) ).
tcf(c_1074,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk7(X1,X0),sk9(X1,X0))
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1073]) ).
tcf(c_1075,plain,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_636,c_1065]) ).
tcf(c_1076,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1075]) ).
tcf(c_1077,plain,
! [X0: $i,X1: $i] :
( lt(sk7(X1,X0),sk9(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_622,c_1068]) ).
tcf(c_1078,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk7(X1,X0),sk9(X1,X0))
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1077]) ).
tcf(c_1079,plain,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_618,c_1071]) ).
tcf(c_1080,negated_conjecture,
! [X0: $i,X1: $i] :
( lt(sk13(X1,X0),sk11(X1,X0))
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1079]) ).
tcf(c_1081,plain,
! [X0: $i,X1: $i] :
( ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_587,c_537,c_540,c_587,c_635]) ).
tcf(c_1082,negated_conjecture,
! [X0: $i,X1: $i] :
( ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1081]) ).
tcf(c_1084,plain,
! [X0: $i,X1: $i] :
( ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_573,c_537,c_540,c_573,c_621]) ).
tcf(c_1085,negated_conjecture,
! [X0: $i,X1: $i] :
( ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1084]) ).
tcf(c_1087,plain,
! [X0: $i,X1: $i] :
( ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_569,c_537,c_540,c_569,c_617]) ).
tcf(c_1088,negated_conjecture,
! [X0: $i,X1: $i] :
( ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1087]) ).
tcf(c_1090,plain,
! [X0: $i,X1: $i] :
( ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_566,c_537,c_540,c_566,c_614]) ).
tcf(c_1091,negated_conjecture,
! [X0: $i,X1: $i] :
( ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1090]) ).
tcf(c_1093,plain,
! [X0: $i,X1: $i] :
( ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_635,c_1082]) ).
tcf(c_1094,negated_conjecture,
! [X0: $i,X1: $i] :
( ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1093]) ).
tcf(c_1095,plain,
! [X0: $i,X1: $i] :
( ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_621,c_1085]) ).
tcf(c_1096,negated_conjecture,
! [X0: $i,X1: $i] :
( ( app(cons(sk9(X1,X0),nil),sk10(X1,X0)) = sk3 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1095]) ).
tcf(c_1097,plain,
! [X0: $i,X1: $i] :
( ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_617,c_1088]) ).
tcf(c_1098,negated_conjecture,
! [X0: $i,X1: $i] :
( ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ( app(sk14(X1,X0),cons(sk13(X1,X0),nil)) = sk3 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1097]) ).
tcf(c_1099,plain,
! [X0: $i,X1: $i] :
( ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ( app(app(X0,sk3),X1) != sk4 )
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(global_subsumption_just,[status(thm)],[c_614,c_1091]) ).
tcf(c_1100,negated_conjecture,
! [X0: $i,X1: $i] :
( ( app(sk8(X1,X0),cons(sk7(X1,X0),nil)) = X0 )
| ( app(cons(sk11(X1,X0),nil),sk12(X1,X0)) = X1 )
| ~ ssList(X1)
| ~ ssList(X0)
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(renaming,[status(thm)],[c_1099]) ).
tcf(c_1518,plain,
( ssList(sk8(sk6,sk5))
| ssList(sk14(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_917]) ).
tcf(c_1519,plain,
( ssItem(sk13(sk6,sk5))
| ssList(sk8(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_919]) ).
tcf(c_1541,plain,
( ssList(sk8(sk6,sk5))
| ssList(sk12(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_921]) ).
tcf(c_1542,plain,
( ssItem(sk11(sk6,sk5))
| ssList(sk10(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_923]) ).
tcf(c_1543,plain,
( ssItem(sk9(sk6,sk5))
| ssItem(sk11(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_925]) ).
tcf(c_1544,plain,
( ssItem(sk11(sk6,sk5))
| ssList(sk8(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_927]) ).
tcf(c_1545,plain,
( ssItem(sk7(sk6,sk5))
| ssList(sk14(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_929]) ).
tcf(c_1546,plain,
( ssItem(sk13(sk6,sk5))
| ssItem(sk7(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_931]) ).
tcf(c_1547,plain,
( ssItem(sk7(sk6,sk5))
| ssList(sk12(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_933]) ).
tcf(c_1569,plain,
( ssItem(sk11(sk6,sk5))
| ssItem(sk7(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_935]) ).
tcf(c_1570,plain,
( ssList(sk14(sk6,sk5))
| lt(sk7(sk6,sk5),sk9(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_961]) ).
tcf(c_1571,plain,
( ssList(sk10(sk6,sk5))
| lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_963]) ).
tcf(c_1572,plain,
( ssItem(sk13(sk6,sk5))
| lt(sk7(sk6,sk5),sk9(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_965]) ).
tcf(c_1573,plain,
( ssItem(sk9(sk6,sk5))
| lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_967]) ).
tcf(c_1574,plain,
( ssList(sk12(sk6,sk5))
| lt(sk7(sk6,sk5),sk9(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_969]) ).
tcf(c_1575,plain,
( ssList(sk8(sk6,sk5))
| lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_971]) ).
tcf(c_1576,plain,
( ssItem(sk11(sk6,sk5))
| lt(sk7(sk6,sk5),sk9(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_973]) ).
tcf(c_1577,plain,
( ssItem(sk7(sk6,sk5))
| lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_975]) ).
tcf(c_1599,plain,
( lt(sk13(sk6,sk5),sk11(sk6,sk5))
| lt(sk7(sk6,sk5),sk9(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_980]) ).
tcf(c_1601,plain,
( ssList(sk10(sk6,sk5))
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1032]) ).
tcf(c_1603,plain,
( ssItem(sk9(sk6,sk5))
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1036]) ).
tcf(c_1604,plain,
( ssList(sk10(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1038]) ).
tcf(c_1605,plain,
( ssItem(sk9(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1040]) ).
tcf(c_1631,plain,
( ssList(sk8(sk6,sk5))
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1050]) ).
tcf(c_1632,plain,
( ssList(sk8(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1052]) ).
tcf(c_1633,plain,
( ssItem(sk11(sk6,sk5))
| ( app(cons(sk9(sk6,sk5),nil),sk10(sk6,sk5)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1054]) ).
tcf(c_1634,plain,
( ssItem(sk11(sk6,sk5))
| ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1056]) ).
tcf(c_1656,plain,
( ssItem(sk7(sk6,sk5))
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1058]) ).
tcf(c_1657,plain,
( ssItem(sk7(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1060]) ).
tcf(c_1658,plain,
( lt(sk7(sk6,sk5),sk9(sk6,sk5))
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1074]) ).
tcf(c_1659,plain,
( lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ( app(cons(sk9(sk6,sk5),nil),sk10(sk6,sk5)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1076]) ).
tcf(c_1660,plain,
( lt(sk7(sk6,sk5),sk9(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1078]) ).
tcf(c_1661,plain,
( lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1080]) ).
tcf(c_1662,plain,
( ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ( app(cons(sk9(sk6,sk5),nil),sk10(sk6,sk5)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1094]) ).
tcf(c_1663,plain,
( ( app(cons(sk9(sk6,sk5),nil),sk10(sk6,sk5)) = sk3 )
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1096]) ).
tcf(c_1664,plain,
( ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 )
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1098]) ).
tcf(c_1686,plain,
( ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 )
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1100]) ).
tcf(c_2448,plain,
( ssList(sk8(sk6,sk5))
| ssList(sk14(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_1518,c_535,c_534,c_1518]) ).
tcf(c_2454,plain,
( ssItem(sk13(sk6,sk5))
| ssList(sk8(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_1519,c_535,c_534,c_1519]) ).
tcf(c_2456,plain,
( ssList(sk8(sk6,sk5))
| ssList(sk12(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_1541,c_535,c_534,c_1541]) ).
tcf(c_2501,plain,
( ssItem(sk11(sk6,sk5))
| ssList(sk10(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_1542,c_535,c_534,c_1542]) ).
tcf(c_2503,plain,
( ssItem(sk9(sk6,sk5))
| ssItem(sk11(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_1543,c_535,c_534,c_1543]) ).
tcf(c_2507,plain,
( ssItem(sk7(sk6,sk5))
| ssList(sk14(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_1545,c_535,c_534,c_1545]) ).
tcf(c_2509,plain,
( ssItem(sk13(sk6,sk5))
| ssItem(sk7(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_1546,c_535,c_534,c_1546]) ).
tcf(c_2520,plain,
( ssItem(sk7(sk6,sk5))
| ssList(sk12(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_1547,c_535,c_534,c_1547]) ).
tcf(c_2524,plain,
( ssList(sk14(sk6,sk5))
| lt(sk7(sk6,sk5),sk9(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_1570,c_535,c_534,c_1570]) ).
tcf(c_2527,plain,
( ssList(sk10(sk6,sk5))
| lt(sk13(sk6,sk5),sk11(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_1571,c_535,c_534,c_1571]) ).
tcf(c_2530,plain,
( ssItem(sk13(sk6,sk5))
| lt(sk7(sk6,sk5),sk9(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_1572,c_535,c_534,c_1572]) ).
tcf(c_2535,plain,
( ssItem(sk9(sk6,sk5))
| lt(sk13(sk6,sk5),sk11(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_1573,c_535,c_534,c_1573]) ).
tcf(c_2592,plain,
( ssList(sk12(sk6,sk5))
| lt(sk7(sk6,sk5),sk9(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_969]) ).
tcf(c_2598,plain,
( ssList(sk10(sk6,sk5))
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1032]) ).
tcf(c_2600,plain,
( ssItem(sk9(sk6,sk5))
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1036]) ).
tcf(c_2601,plain,
( ssList(sk10(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1038]) ).
tcf(c_2607,plain,
( ssList(sk8(sk6,sk5))
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1050]) ).
tcf(c_2608,plain,
( ssList(sk8(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1052]) ).
tcf(c_2609,plain,
( ssItem(sk11(sk6,sk5))
| ( app(cons(sk9(sk6,sk5),nil),sk10(sk6,sk5)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1054]) ).
tcf(c_2610,plain,
( ssItem(sk11(sk6,sk5))
| ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1056]) ).
tcf(c_2611,plain,
( ssItem(sk7(sk6,sk5))
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1058]) ).
tcf(c_2612,plain,
( ssItem(sk7(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1060]) ).
tcf(c_2665,plain,
( ssList(sk12(sk6,sk5))
| lt(sk7(sk6,sk5),sk9(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_2592,c_535,c_534,c_1574]) ).
tcf(c_2682,plain,
( ssList(sk10(sk6,sk5))
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_2598,c_535,c_534,c_1601]) ).
tcf(c_2686,plain,
( ssItem(sk9(sk6,sk5))
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_2600,c_535,c_534,c_1603]) ).
tcf(c_2688,plain,
( ssList(sk10(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 ) ),
inference(global_subsumption_just,[status(thm)],[c_2601,c_535,c_534,c_1604]) ).
tcf(c_2700,plain,
( ssList(sk8(sk6,sk5))
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_2607,c_535,c_534,c_1631]) ).
tcf(c_2702,plain,
( ssList(sk8(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 ) ),
inference(global_subsumption_just,[status(thm)],[c_2608,c_535,c_534,c_1632]) ).
tcf(c_2704,plain,
( ssItem(sk11(sk6,sk5))
| ( app(cons(sk9(sk6,sk5),nil),sk10(sk6,sk5)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_2609,c_535,c_534,c_1633]) ).
tcf(c_2706,plain,
( ssItem(sk11(sk6,sk5))
| ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 ) ),
inference(global_subsumption_just,[status(thm)],[c_2610,c_535,c_534,c_1634]) ).
tcf(c_3168,plain,
( ssItem(sk7(sk6,sk5))
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_2611,c_535,c_534,c_1656]) ).
tcf(c_3174,plain,
( ssItem(sk7(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 ) ),
inference(global_subsumption_just,[status(thm)],[c_2612,c_535,c_534,c_1657]) ).
tcf(c_4702,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssList(sk14(X2,sk5))
| ~ ssList(sk5)
| ~ ssItem(X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(sk7(X2,sk5))
| ~ ssList(sk8(X2,sk5))
| ~ lt(sk7(X2,sk5),X0)
| ( app(app(sk5,sk3),X2) != sk4 )
| ( app(cons(X0,nil),X1) != sk3 ) ),
inference(resolution,[status(thm)],[c_538,c_1042]) ).
tcf(c_4703,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssItem(sk13(X2,sk5))
| ~ ssList(sk5)
| ~ ssItem(X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(sk7(X2,sk5))
| ~ ssList(sk8(X2,sk5))
| ~ lt(sk7(X2,sk5),X0)
| ( app(app(sk5,sk3),X2) != sk4 )
| ( app(cons(X0,nil),X1) != sk3 ) ),
inference(resolution,[status(thm)],[c_538,c_1044]) ).
tcf(c_4704,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssList(sk12(X2,sk5))
| ~ ssList(sk5)
| ~ ssItem(X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(sk7(X2,sk5))
| ~ ssList(sk8(X2,sk5))
| ~ lt(sk7(X2,sk5),X0)
| ( app(app(sk5,sk3),X2) != sk4 )
| ( app(cons(X0,nil),X1) != sk3 ) ),
inference(resolution,[status(thm)],[c_538,c_1048]) ).
tcf(c_6121,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssList(sk14(X2,sk5))
| ( app(cons(X0,nil),X1) != sk3 )
| ( app(app(sk5,sk3),X2) != sk4 )
| ~ lt(sk7(X2,sk5),X0)
| ~ ssList(sk8(X2,sk5))
| ~ ssItem(sk7(X2,sk5))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssItem(X0) ),
inference(global_subsumption_just,[status(thm)],[c_4702,c_534,c_4702]) ).
tcf(c_6122,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssList(sk14(X2,sk5))
| ~ ssItem(X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(sk7(X2,sk5))
| ~ ssList(sk8(X2,sk5))
| ~ lt(sk7(X2,sk5),X0)
| ( app(app(sk5,sk3),X2) != sk4 )
| ( app(cons(X0,nil),X1) != sk3 ) ),
inference(renaming,[status(thm)],[c_6121]) ).
tcf(c_6202,plain,
! [X0: $i,X1: $i] :
( ssList(sk14(sk6,sk5))
| ~ ssList(sk6)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ ssItem(sk7(sk6,sk5))
| ~ ssList(sk8(sk6,sk5))
| ~ lt(sk7(sk6,sk5),X0)
| ( app(cons(X0,nil),X1) != sk3 ) ),
inference(resolution,[status(thm)],[c_6122,c_536]) ).
tcf(c_6204,plain,
! [X0: $i,X1: $i] :
( ssList(sk14(sk6,sk5))
| ( app(cons(X0,nil),X1) != sk3 )
| ~ lt(sk7(sk6,sk5),X0)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(global_subsumption_just,[status(thm)],[c_6202,c_535,c_2448,c_2507,c_6202]) ).
tcf(c_6205,plain,
! [X0: $i,X1: $i] :
( ssList(sk14(sk6,sk5))
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ lt(sk7(sk6,sk5),X0)
| ( app(cons(X0,nil),X1) != sk3 ) ),
inference(renaming,[status(thm)],[c_6204]) ).
tcf(c_6241,plain,
! [X0: $i,X1: $i] :
( ssList(sk14(sk6,sk5))
| ssList(sk14(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(sk9(X1,X0))
| ~ ssList(sk10(X1,X0))
| ~ lt(sk7(sk6,sk5),sk9(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(resolution,[status(thm)],[c_6205,c_1030]) ).
tcf(c_6452,plain,
! [X0: $i,X1: $i] :
( ssList(sk14(sk6,sk5))
| ssList(sk14(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ lt(sk7(sk6,sk5),sk9(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_6241,c_856,c_862,c_6241]) ).
tcf(c_6479,plain,
( ssList(sk14(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5)
| ~ lt(sk7(sk6,sk5),sk9(sk6,sk5)) ),
inference(resolution,[status(thm)],[c_6452,c_536]) ).
tcf(c_6480,plain,
ssList(sk14(sk6,sk5)),
inference(global_subsumption_just,[status(thm)],[c_6479,c_535,c_534,c_2524,c_6479]) ).
tcf(c_6496,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssItem(sk13(X2,sk5))
| ( app(cons(X0,nil),X1) != sk3 )
| ( app(app(sk5,sk3),X2) != sk4 )
| ~ lt(sk7(X2,sk5),X0)
| ~ ssList(sk8(X2,sk5))
| ~ ssItem(sk7(X2,sk5))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssItem(X0) ),
inference(global_subsumption_just,[status(thm)],[c_4703,c_534,c_4703]) ).
tcf(c_6497,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssItem(sk13(X2,sk5))
| ~ ssItem(X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(sk7(X2,sk5))
| ~ ssList(sk8(X2,sk5))
| ~ lt(sk7(X2,sk5),X0)
| ( app(app(sk5,sk3),X2) != sk4 )
| ( app(cons(X0,nil),X1) != sk3 ) ),
inference(renaming,[status(thm)],[c_6496]) ).
tcf(c_6535,plain,
! [X0: $i,X1: $i] :
( ssItem(sk13(sk6,sk5))
| ~ ssList(sk6)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ ssItem(sk7(sk6,sk5))
| ~ ssList(sk8(sk6,sk5))
| ~ lt(sk7(sk6,sk5),X0)
| ( app(cons(X0,nil),X1) != sk3 ) ),
inference(resolution,[status(thm)],[c_6497,c_536]) ).
tcf(c_6537,plain,
! [X0: $i,X1: $i] :
( ssItem(sk13(sk6,sk5))
| ( app(cons(X0,nil),X1) != sk3 )
| ~ lt(sk7(sk6,sk5),X0)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(global_subsumption_just,[status(thm)],[c_6535,c_535,c_2454,c_2509,c_6535]) ).
tcf(c_6538,plain,
! [X0: $i,X1: $i] :
( ssItem(sk13(sk6,sk5))
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ lt(sk7(sk6,sk5),X0)
| ( app(cons(X0,nil),X1) != sk3 ) ),
inference(renaming,[status(thm)],[c_6537]) ).
tcf(c_6575,plain,
! [X0: $i,X1: $i] :
( ssItem(sk13(sk6,sk5))
| ssItem(sk13(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(sk9(X1,X0))
| ~ ssList(sk10(X1,X0))
| ~ lt(sk7(sk6,sk5),sk9(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(resolution,[status(thm)],[c_6538,c_1034]) ).
tcf(c_6828,plain,
! [X0: $i,X1: $i] :
( ssItem(sk13(sk6,sk5))
| ssItem(sk13(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ lt(sk7(sk6,sk5),sk9(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_6575,c_859,c_865,c_6575]) ).
tcf(c_6855,plain,
( ssItem(sk13(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5)
| ~ lt(sk7(sk6,sk5),sk9(sk6,sk5)) ),
inference(resolution,[status(thm)],[c_6828,c_536]) ).
tcf(c_6856,plain,
ssItem(sk13(sk6,sk5)),
inference(global_subsumption_just,[status(thm)],[c_6855,c_535,c_534,c_2530,c_6855]) ).
tcf(c_6882,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssList(sk12(X2,sk5))
| ( app(cons(X0,nil),X1) != sk3 )
| ( app(app(sk5,sk3),X2) != sk4 )
| ~ lt(sk7(X2,sk5),X0)
| ~ ssList(sk8(X2,sk5))
| ~ ssItem(sk7(X2,sk5))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssItem(X0) ),
inference(global_subsumption_just,[status(thm)],[c_4704,c_534,c_4704]) ).
tcf(c_6883,plain,
! [X0: $i,X1: $i,X2: $i] :
( ssList(sk12(X2,sk5))
| ~ ssItem(X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(sk7(X2,sk5))
| ~ ssList(sk8(X2,sk5))
| ~ lt(sk7(X2,sk5),X0)
| ( app(app(sk5,sk3),X2) != sk4 )
| ( app(cons(X0,nil),X1) != sk3 ) ),
inference(renaming,[status(thm)],[c_6882]) ).
tcf(c_6921,plain,
! [X0: $i,X1: $i] :
( ssList(sk12(sk6,sk5))
| ~ ssList(sk6)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ ssItem(sk7(sk6,sk5))
| ~ ssList(sk8(sk6,sk5))
| ~ lt(sk7(sk6,sk5),X0)
| ( app(cons(X0,nil),X1) != sk3 ) ),
inference(resolution,[status(thm)],[c_6883,c_536]) ).
tcf(c_6923,plain,
! [X0: $i,X1: $i] :
( ssList(sk12(sk6,sk5))
| ( app(cons(X0,nil),X1) != sk3 )
| ~ lt(sk7(sk6,sk5),X0)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(global_subsumption_just,[status(thm)],[c_6921,c_535,c_2456,c_2520,c_6921]) ).
tcf(c_6924,plain,
! [X0: $i,X1: $i] :
( ssList(sk12(sk6,sk5))
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ lt(sk7(sk6,sk5),X0)
| ( app(cons(X0,nil),X1) != sk3 ) ),
inference(renaming,[status(thm)],[c_6923]) ).
tcf(c_6962,plain,
! [X0: $i,X1: $i] :
( ssList(sk12(sk6,sk5))
| ssList(sk12(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(sk9(X1,X0))
| ~ ssList(sk10(X1,X0))
| ~ lt(sk7(sk6,sk5),sk9(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(resolution,[status(thm)],[c_6924,c_1046]) ).
tcf(c_7172,plain,
! [X0: $i,X1: $i] :
( ssList(sk12(sk6,sk5))
| ssList(sk12(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ lt(sk7(sk6,sk5),sk9(X1,X0))
| ( app(app(X0,sk3),X1) != sk4 ) ),
inference(global_subsumption_just,[status(thm)],[c_6962,c_868,c_871,c_6962]) ).
tcf(c_7199,plain,
( ssList(sk12(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5)
| ~ lt(sk7(sk6,sk5),sk9(sk6,sk5)) ),
inference(resolution,[status(thm)],[c_7172,c_536]) ).
tcf(c_7200,plain,
ssList(sk12(sk6,sk5)),
inference(global_subsumption_just,[status(thm)],[c_7199,c_535,c_534,c_2665,c_7199]) ).
tcf(c_10205,plain,
( ssList(sk10(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1038]) ).
tcf(c_10229,plain,
( lt(sk7(sk6,sk5),sk9(sk6,sk5))
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1074]) ).
tcf(c_10230,plain,
( lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ( app(cons(sk9(sk6,sk5),nil),sk10(sk6,sk5)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1076]) ).
tcf(c_10231,plain,
( lt(sk7(sk6,sk5),sk9(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1078]) ).
tcf(c_10240,plain,
( lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1080]) ).
tcf(c_10241,plain,
( ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ( app(cons(sk9(sk6,sk5),nil),sk10(sk6,sk5)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1094]) ).
tcf(c_10242,plain,
( ( app(cons(sk9(sk6,sk5),nil),sk10(sk6,sk5)) = sk3 )
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1096]) ).
tcf(c_10243,plain,
( ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 )
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1098]) ).
tcf(c_10244,plain,
( ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 )
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1100]) ).
tcf(c_10289,plain,
( ssList(sk10(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 ) ),
inference(global_subsumption_just,[status(thm)],[c_10205,c_2688]) ).
tcf(c_10319,plain,
( lt(sk7(sk6,sk5),sk9(sk6,sk5))
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_10229,c_535,c_534,c_1658]) ).
tcf(c_10322,plain,
( lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ( app(cons(sk9(sk6,sk5),nil),sk10(sk6,sk5)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_10230,c_535,c_534,c_1659]) ).
tcf(c_10325,plain,
( lt(sk7(sk6,sk5),sk9(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 ) ),
inference(global_subsumption_just,[status(thm)],[c_10231,c_535,c_534,c_1660]) ).
tcf(c_10328,plain,
( lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 ) ),
inference(global_subsumption_just,[status(thm)],[c_10240,c_535,c_534,c_1661]) ).
tcf(c_10333,plain,
( ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ( app(cons(sk9(sk6,sk5),nil),sk10(sk6,sk5)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_10241,c_535,c_534,c_1662]) ).
tcf(c_10335,plain,
! [X0: $i,X1: $i] :
( ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssItem(sk9(sk6,sk5))
| ~ ssList(sk10(sk6,sk5))
| ~ lt(X1,sk9(sk6,sk5))
| ( sk3 != sk6 )
| ( app(X0,cons(X1,nil)) != sk3 ) ),
inference(superposition,[status(thm)],[c_10333,c_539]) ).
tcf(c_10336,plain,
! [X0: $i,X1: $i] :
( ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssItem(sk9(sk6,sk5))
| ~ ssList(sk10(sk6,sk5))
| ~ lt(X1,sk9(sk6,sk5))
| ( app(X0,cons(X1,nil)) != sk5 ) ),
inference(superposition,[status(thm)],[c_10333,c_538]) ).
tcf(c_10339,plain,
( ( app(cons(sk9(sk6,sk5),nil),sk10(sk6,sk5)) = sk3 )
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 ) ),
inference(global_subsumption_just,[status(thm)],[c_10242,c_535,c_534,c_1663]) ).
tcf(c_10342,plain,
! [X0: $i,X1: $i] :
( ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssItem(sk9(sk6,sk5))
| ~ ssList(sk10(sk6,sk5))
| ~ lt(X1,sk9(sk6,sk5))
| ( app(X0,cons(X1,nil)) != sk5 ) ),
inference(superposition,[status(thm)],[c_10339,c_538]) ).
tcf(c_10345,plain,
( ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 )
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_10243,c_535,c_534,c_1664]) ).
tcf(c_10351,plain,
( ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 )
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 ) ),
inference(global_subsumption_just,[status(thm)],[c_10244,c_535,c_534,c_1686]) ).
tcf(c_10353,plain,
! [X0: $i,X1: $i] :
( ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 )
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssItem(sk11(sk6,sk5))
| ~ ssList(sk12(sk6,sk5))
| ~ lt(X1,sk11(sk6,sk5))
| ( app(X0,cons(X1,nil)) != sk3 ) ),
inference(superposition,[status(thm)],[c_10351,c_539]) ).
tcf(c_10354,plain,
! [X0: $i,X1: $i] :
( ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 )
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssItem(sk11(sk6,sk5))
| ~ ssList(sk12(sk6,sk5))
| ~ lt(X1,sk11(sk6,sk5))
| ( sk3 != sk6 )
| ( app(X0,cons(X1,nil)) != sk5 ) ),
inference(superposition,[status(thm)],[c_10351,c_538]) ).
tcf(c_10365,plain,
! [X0: $i,X1: $i] :
( ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ lt(X1,sk9(sk6,sk5))
| ( app(X0,cons(X1,nil)) != sk5 ) ),
inference(global_subsumption_just,[status(thm)],[c_10336,c_2682,c_2686,c_10336]) ).
tcf(c_10368,plain,
( ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssItem(sk7(sk6,sk5))
| ~ ssList(sk8(sk6,sk5))
| ~ lt(sk7(sk6,sk5),sk9(sk6,sk5)) ),
inference(superposition,[status(thm)],[c_10345,c_10365]) ).
tcf(c_10369,plain,
! [X0: $i,X1: $i] :
( ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ lt(X1,sk9(sk6,sk5))
| ( app(X0,cons(X1,nil)) != sk5 ) ),
inference(global_subsumption_just,[status(thm)],[c_10342,c_535,c_534,c_1604,c_1605,c_10342]) ).
tcf(c_10373,plain,
! [X0: $i,X1: $i] :
( ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 )
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ lt(X1,sk11(sk6,sk5))
| ( app(X0,cons(X1,nil)) != sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_10353,c_2706,c_7200,c_10353]) ).
tcf(c_10377,plain,
app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3,
inference(global_subsumption_just,[status(thm)],[c_10335,c_2700,c_3168,c_10319,c_10368]) ).
tcf(c_10381,plain,
( ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 )
| ~ ssItem(sk13(sk6,sk5))
| ~ ssList(sk14(sk6,sk5))
| ~ lt(sk13(sk6,sk5),sk11(sk6,sk5)) ),
inference(superposition,[status(thm)],[c_10377,c_10373]) ).
tcf(c_10395,plain,
app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5,
inference(global_subsumption_just,[status(thm)],[c_10354,c_6480,c_6856,c_10328,c_10381]) ).
tcf(c_10401,plain,
( ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssItem(sk7(sk6,sk5))
| ~ ssList(sk8(sk6,sk5))
| ~ lt(sk7(sk6,sk5),sk9(sk6,sk5)) ),
inference(superposition,[status(thm)],[c_10395,c_10369]) ).
tcf(c_10451,plain,
! [X0: $i] :
( ssItem(X0)
| duplicatefreeP(sk10(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 ) ),
inference(superposition,[status(thm)],[c_10289,c_416]) ).
tcf(c_10456,plain,
app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6,
inference(global_subsumption_just,[status(thm)],[c_10451,c_2702,c_3174,c_10325,c_10401]) ).
tcf(c_10458,plain,
! [X0: $i,X1: $i] :
( ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssItem(sk11(sk6,sk5))
| ~ ssList(sk12(sk6,sk5))
| ~ lt(X1,sk11(sk6,sk5))
| ( app(X0,cons(X1,nil)) != sk3 ) ),
inference(superposition,[status(thm)],[c_10456,c_539]) ).
tcf(c_19657,plain,
( ssList(sk10(sk6,sk5))
| lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_963]) ).
tcf(c_19659,plain,
( ssItem(sk9(sk6,sk5))
| lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_967]) ).
tcf(c_19661,plain,
( ssList(sk8(sk6,sk5))
| lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_971]) ).
tcf(c_19671,plain,
( ssItem(sk7(sk6,sk5))
| lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_975]) ).
tcf(c_19672,plain,
( lt(sk13(sk6,sk5),sk11(sk6,sk5))
| lt(sk7(sk6,sk5),sk9(sk6,sk5))
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_980]) ).
tcf(c_19674,plain,
( ssList(sk10(sk6,sk5))
| ( app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1032]) ).
tcf(c_19677,plain,
( ssList(sk10(sk6,sk5))
| ( app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1038]) ).
tcf(c_19694,plain,
( ssItem(sk11(sk6,sk5))
| ( app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1056]) ).
tcf(c_19706,plain,
( lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ( app(cons(sk9(sk6,sk5),nil),sk10(sk6,sk5)) = sk3 )
| ~ ssList(sk6)
| ~ ssList(sk5) ),
inference(superposition,[status(thm)],[c_536,c_1076]) ).
tcf(c_19723,plain,
( ssList(sk10(sk6,sk5))
| lt(sk13(sk6,sk5),sk11(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_19657,c_2527]) ).
tcf(c_19728,plain,
( ssItem(sk9(sk6,sk5))
| lt(sk13(sk6,sk5),sk11(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_19659,c_2535]) ).
tcf(c_19733,plain,
( ssList(sk8(sk6,sk5))
| lt(sk13(sk6,sk5),sk11(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_19661,c_535,c_534,c_1575]) ).
tcf(c_19739,plain,
( ssItem(sk7(sk6,sk5))
| lt(sk13(sk6,sk5),sk11(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_19671,c_535,c_534,c_1577]) ).
tcf(c_19742,plain,
( lt(sk13(sk6,sk5),sk11(sk6,sk5))
| lt(sk7(sk6,sk5),sk9(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_19672,c_535,c_534,c_1599]) ).
tcf(c_19745,plain,
app(sk14(sk6,sk5),cons(sk13(sk6,sk5),nil)) = sk3,
inference(global_subsumption_just,[status(thm)],[c_19674,c_2700,c_3168,c_10319,c_10368]) ).
tcf(c_19751,plain,
app(cons(sk11(sk6,sk5),nil),sk12(sk6,sk5)) = sk6,
inference(global_subsumption_just,[status(thm)],[c_19677,c_10456]) ).
tcf(c_19753,plain,
! [X0: $i,X1: $i] :
( ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssItem(sk11(sk6,sk5))
| ~ ssList(sk12(sk6,sk5))
| ~ lt(X1,sk11(sk6,sk5))
| ( app(X0,cons(X1,nil)) != sk3 ) ),
inference(superposition,[status(thm)],[c_19751,c_539]) ).
tcf(c_19763,plain,
app(sk8(sk6,sk5),cons(sk7(sk6,sk5),nil)) = sk5,
inference(global_subsumption_just,[status(thm)],[c_19694,c_10395]) ).
tcf(c_19783,plain,
( lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ( app(cons(sk9(sk6,sk5),nil),sk10(sk6,sk5)) = sk3 ) ),
inference(global_subsumption_just,[status(thm)],[c_19706,c_10322]) ).
tcf(c_19802,plain,
! [X0: $i,X1: $i] :
( ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssItem(sk11(sk6,sk5))
| ( app(X0,cons(X1,nil)) != sk3 )
| ~ lt(X1,sk11(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_19753,c_535,c_534,c_2665,c_7199,c_10458]) ).
tcf(c_19803,plain,
! [X0: $i,X1: $i] :
( ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssItem(sk11(sk6,sk5))
| ~ lt(X1,sk11(sk6,sk5))
| ( app(X0,cons(X1,nil)) != sk3 ) ),
inference(renaming,[status(thm)],[c_19802]) ).
tcf(c_19805,plain,
( ~ ssItem(sk13(sk6,sk5))
| ~ ssItem(sk11(sk6,sk5))
| ~ ssList(sk14(sk6,sk5))
| ~ lt(sk13(sk6,sk5),sk11(sk6,sk5)) ),
inference(superposition,[status(thm)],[c_19745,c_19803]) ).
tcf(c_19834,plain,
( ~ lt(sk13(sk6,sk5),sk11(sk6,sk5))
| ~ ssItem(sk11(sk6,sk5)) ),
inference(global_subsumption_just,[status(thm)],[c_19805,c_535,c_534,c_2524,c_2530,c_6479,c_6855,c_19805]) ).
tcf(c_19835,plain,
( ~ ssItem(sk11(sk6,sk5))
| ~ lt(sk13(sk6,sk5),sk11(sk6,sk5)) ),
inference(renaming,[status(thm)],[c_19834]) ).
tcf(c_19836,plain,
( ( app(cons(sk9(sk6,sk5),nil),sk10(sk6,sk5)) = sk3 )
| ~ ssItem(sk11(sk6,sk5)) ),
inference(superposition,[status(thm)],[c_19783,c_19835]) ).
tcf(c_19837,plain,
( lt(sk7(sk6,sk5),sk9(sk6,sk5))
| ~ ssItem(sk11(sk6,sk5)) ),
inference(superposition,[status(thm)],[c_19742,c_19835]) ).
tcf(c_19838,plain,
( ssItem(sk7(sk6,sk5))
| ~ ssItem(sk11(sk6,sk5)) ),
inference(superposition,[status(thm)],[c_19739,c_19835]) ).
tcf(c_19839,plain,
( ssList(sk8(sk6,sk5))
| ~ ssItem(sk11(sk6,sk5)) ),
inference(superposition,[status(thm)],[c_19733,c_19835]) ).
tcf(c_19840,plain,
( ssItem(sk9(sk6,sk5))
| ~ ssItem(sk11(sk6,sk5)) ),
inference(superposition,[status(thm)],[c_19728,c_19835]) ).
tcf(c_19841,plain,
( ssList(sk10(sk6,sk5))
| ~ ssItem(sk11(sk6,sk5)) ),
inference(superposition,[status(thm)],[c_19723,c_19835]) ).
tcf(c_19842,plain,
ssItem(sk7(sk6,sk5)),
inference(global_subsumption_just,[status(thm)],[c_19838,c_535,c_534,c_1569,c_19838]) ).
tcf(c_19844,plain,
ssList(sk8(sk6,sk5)),
inference(global_subsumption_just,[status(thm)],[c_19839,c_535,c_534,c_1544,c_19839]) ).
tcf(c_19846,plain,
ssItem(sk9(sk6,sk5)),
inference(global_subsumption_just,[status(thm)],[c_19840,c_2503,c_19840]) ).
tcf(c_19848,plain,
ssList(sk10(sk6,sk5)),
inference(global_subsumption_just,[status(thm)],[c_19841,c_2501,c_19841]) ).
tcf(c_19850,plain,
lt(sk7(sk6,sk5),sk9(sk6,sk5)),
inference(global_subsumption_just,[status(thm)],[c_19837,c_535,c_534,c_1576,c_19837]) ).
tcf(c_19855,plain,
app(cons(sk9(sk6,sk5),nil),sk10(sk6,sk5)) = sk3,
inference(global_subsumption_just,[status(thm)],[c_19836,c_2704,c_19836]) ).
tcf(c_19858,plain,
! [X0: $i,X1: $i] :
( ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssItem(sk9(sk6,sk5))
| ~ ssList(sk10(sk6,sk5))
| ~ lt(X1,sk9(sk6,sk5))
| ( app(X0,cons(X1,nil)) != sk5 ) ),
inference(superposition,[status(thm)],[c_19855,c_538]) ).
tcf(c_19861,plain,
! [X0: $i,X1: $i] :
( ~ ssItem(X1)
| ~ ssList(X0)
| ~ lt(X1,sk9(sk6,sk5))
| ( app(X0,cons(X1,nil)) != sk5 ) ),
inference(global_subsumption_just,[status(thm)],[c_19858,c_19846,c_19848,c_19858]) ).
tcf(c_19865,plain,
( ~ ssItem(sk7(sk6,sk5))
| ~ ssList(sk8(sk6,sk5))
| ~ lt(sk7(sk6,sk5),sk9(sk6,sk5)) ),
inference(superposition,[status(thm)],[c_19763,c_19861]) ).
tcf(c_19866,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_19865,c_19850,c_19844,c_19842]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC344-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 : n011.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 17:44:42 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.39 Running first-order theorem proving
% 0.13/0.39 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.40
% 0.13/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.40
% 0.13/0.40 % Detected problem language: tptp
% 0.13/0.41 % Proving...
% 23.98/4.27 % SZS status Started for theBenchmark.p
% 23.98/4.27 % SZS status Unsatisfiable for theBenchmark.p
% 23.98/4.27
% 23.98/4.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 23.98/4.27
% 23.98/4.27 % ------ iProver source info
% 23.98/4.27
% 23.98/4.27 % git: date: 2026-07-19 20:42:38 +0200
% 23.98/4.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 23.98/4.27 % git: non_committed_changes: false
% 23.98/4.27
% 23.98/4.27 % ------ Parsing...% successful
% 23.98/4.27
% 23.98/4.27
% 23.98/4.27 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 23.98/4.27
% 23.98/4.27 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e sup_sim: 0 sf_s rm: 1 0s sf_e %
% 23.98/4.27
% 23.98/4.27 % ------ Preprocessing...%
% 23.98/4.27
% 23.98/4.27 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 23.98/4.27 % ------ Proving...
% 23.98/4.27 % ------ Problem Properties
% 23.98/4.27
% 23.98/4.27 %
% 23.98/4.27 % clauses 237
% 23.98/4.27 % conjectures 70
% 23.98/4.27 % EPR 60
% 23.98/4.27 % Horn 158
% 23.98/4.27 % unary 64
% 23.98/4.27 % binary 22
% 23.98/4.27 % lits 818
% 23.98/4.27 % lits eq 155
% 23.98/4.27 % fd_pure 0
% 23.98/4.27 % fd_pseudo 0
% 23.98/4.27 % fd_cond 15
% 23.98/4.27 % fd_pseudo_cond 16
% 23.98/4.27 % AC symbols 0
% 23.98/4.27
% 23.98/4.27 % ------ Input Options Time Limit: Unbounded
% 23.98/4.27
% 23.98/4.27
% 23.98/4.27 % ------
% 23.98/4.27 % Current options:
% 23.98/4.27 % ------
% 23.98/4.27
% 23.98/4.27
% 23.98/4.27 %
% 23.98/4.27
% 23.98/4.27 % ------ Proving...
% 23.98/4.27 %
% 23.98/4.27
% 23.98/4.27 % SZS status Unsatisfiable for theBenchmark.p
% 23.98/4.27
% 23.98/4.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 23.98/4.29
% 23.98/4.29
%------------------------------------------------------------------------------