%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWC344+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:06:03 PM UTC 2026
% Result : Theorem 231.88s 35.18s
% Output : Proof 231.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 187
% Number of leaves : 1
% Syntax : Number of formulae : 943 ( 27 unt; 0 def)
% Number of atoms : 4355 (1862 equ)
% Maximal formula atoms : 46 ( 4 avg)
% Number of connectives : 5514 (2102 ~;3294 |; 90 &)
% ( 0 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 35 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-2 aty)
% Number of variables : 608 ( 0 sgn 48 !; 34 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f95,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( ( nil = V
| nil != U )
& ? [X9] :
( ? [X10] :
( strictorderedP(U)
& ! [X15] :
( ssItem(X15)
=> ! [X16] :
( ssList(X16)
=> ( ! [X17] :
( ssItem(X17)
=> ! [X18] :
( ssList(X18)
=> ( ~ lt(X17,X15)
| app(X18,cons(X17,nil)) != U ) ) )
| app(cons(X15,nil),X16) != X10 ) ) )
& ! [X11] :
( ssItem(X11)
=> ! [X12] :
( ssList(X12)
=> ( ! [X13] :
( ssItem(X13)
=> ! [X14] :
( ssList(X14)
=> ( ~ lt(X11,X13)
| app(cons(X13,nil),X14) != U ) ) )
| app(X12,cons(X11,nil)) != X9 ) ) )
& app(app(X9,U),X10) = V
& ssList(X10) )
& ssList(X9) ) )
| ( nil = W
& nil != X )
| ! [Y] :
( ssList(Y)
=> ! [Z] :
( ssList(Z)
=> ( ? [X5] :
( ? [X6] :
( ? [X7] :
( ? [X8] :
( lt(X7,X5)
& app(X8,cons(X7,nil)) = W
& ssList(X8) )
& ssItem(X7) )
& app(cons(X5,nil),X6) = Z
& ssList(X6) )
& ssItem(X5) )
| ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( lt(X1,X3)
& app(cons(X3,nil),X4) = W
& ssList(X4) )
& ssItem(X3) )
& app(X2,cons(X1,nil)) = Y
& ssList(X2) )
& ssItem(X1) )
| ~ strictorderedP(W)
| app(app(Y,W),Z) != X ) ) )
| U != W
| V != X ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f95_neg,negated_conjecture,
~ ! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( ( nil = V
| nil != U )
& ? [X9] :
( ? [X10] :
( strictorderedP(U)
& ! [X15] :
( ssItem(X15)
=> ! [X16] :
( ssList(X16)
=> ( ! [X17] :
( ssItem(X17)
=> ! [X18] :
( ssList(X18)
=> ( ~ lt(X17,X15)
| app(X18,cons(X17,nil)) != U ) ) )
| app(cons(X15,nil),X16) != X10 ) ) )
& ! [X11] :
( ssItem(X11)
=> ! [X12] :
( ssList(X12)
=> ( ! [X13] :
( ssItem(X13)
=> ! [X14] :
( ssList(X14)
=> ( ~ lt(X11,X13)
| app(cons(X13,nil),X14) != U ) ) )
| app(X12,cons(X11,nil)) != X9 ) ) )
& app(app(X9,U),X10) = V
& ssList(X10) )
& ssList(X9) ) )
| ( nil = W
& nil != X )
| ! [Y] :
( ssList(Y)
=> ! [Z] :
( ssList(Z)
=> ( ? [X5] :
( ? [X6] :
( ? [X7] :
( ? [X8] :
( lt(X7,X5)
& app(X8,cons(X7,nil)) = W
& ssList(X8) )
& ssItem(X7) )
& app(cons(X5,nil),X6) = Z
& ssList(X6) )
& ssItem(X5) )
| ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( lt(X1,X3)
& app(cons(X3,nil),X4) = W
& ssList(X4) )
& ssItem(X3) )
& app(X2,cons(X1,nil)) = Y
& ssList(X2) )
& ssItem(X1) )
| ~ strictorderedP(W)
| app(app(Y,W),Z) != X ) ) )
| U != W
| V != X ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f95_nnf,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ( nil != V
& nil = U )
| ! [X9] :
( ! [X10] :
( ~ strictorderedP(U)
| ? [X15] :
( ? [X16] :
( ? [X17] :
( ? [X18] :
( lt(X17,X15)
& app(X18,cons(X17,nil)) = U
& ssList(X18) )
& ssItem(X17) )
& app(cons(X15,nil),X16) = X10
& ssList(X16) )
& ssItem(X15) )
| ? [X11] :
( ? [X12] :
( ? [X13] :
( ? [X14] :
( lt(X11,X13)
& app(cons(X13,nil),X14) = U
& ssList(X14) )
& ssItem(X13) )
& app(X12,cons(X11,nil)) = X9
& ssList(X12) )
& ssItem(X11) )
| app(app(X9,U),X10) != V
| ~ ssList(X10) )
| ~ ssList(X9) ) )
& ( nil != W
| nil = X )
& ? [Y] :
( ? [Z] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ~ lt(X7,X5)
| app(X8,cons(X7,nil)) != W
| ~ ssList(X8) )
| ~ ssItem(X7) )
| app(cons(X5,nil),X6) != Z
| ~ ssList(X6) )
| ~ ssItem(X5) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ~ lt(X1,X3)
| app(cons(X3,nil),X4) != W
| ~ ssList(X4) )
| ~ ssItem(X3) )
| app(X2,cons(X1,nil)) != Y
| ~ ssList(X2) )
| ~ ssItem(X1) )
& strictorderedP(W)
& app(app(Y,W),Z) = X
& ssList(Z) )
& ssList(Y) )
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(nnf_transformation,[status(thm)],[f95_neg]) ).
fof(f95_sk,plain,
! [X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( ( ( nil != sk48
& nil = sk47 )
| ~ strictorderedP(sk47)
| ( lt(sk59(X9,X10),sk57(X9,X10))
& app(sk60(X9,X10),cons(sk59(X9,X10),nil)) = sk47
& ssList(sk60(X9,X10))
& ssItem(sk59(X9,X10))
& app(cons(sk57(X9,X10),nil),sk58(X9,X10)) = X10
& ssList(sk58(X9,X10))
& ssItem(sk57(X9,X10)) )
| ( lt(sk53(X9,X10),sk55(X9,X10))
& app(cons(sk55(X9,X10),nil),sk56(X9,X10)) = sk47
& ssList(sk56(X9,X10))
& ssItem(sk55(X9,X10))
& app(sk54(X9,X10),cons(sk53(X9,X10),nil)) = X9
& ssList(sk54(X9,X10))
& ssItem(sk53(X9,X10)) )
| app(app(X9,sk47),X10) != sk48
| ~ ssList(X10)
| ~ ssList(X9) )
& ( nil != sk49
| nil = sk50 )
& ( ~ lt(X7,X5)
| app(X8,cons(X7,nil)) != sk49
| ~ ssList(X8)
| ~ ssItem(X7)
| app(cons(X5,nil),X6) != sk52
| ~ ssList(X6)
| ~ ssItem(X5) )
& ( ~ lt(X1,X3)
| app(cons(X3,nil),X4) != sk49
| ~ ssList(X4)
| ~ ssItem(X3)
| app(X2,cons(X1,nil)) != sk51
| ~ ssList(X2)
| ~ ssItem(X1) )
& strictorderedP(sk49)
& app(app(sk51,sk49),sk52) = sk50
& ssList(sk52)
& ssList(sk51)
& sk47 = sk49
& sk48 = sk50
& ssList(sk50)
& ssList(sk49)
& ssList(sk48)
& ssList(sk47) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk47,sk48,sk49,sk50,sk51,sk52,sk53,sk54,sk55,sk56,sk57,sk58,sk59,sk60])],[f95_nnf]) ).
cnf(c195,plain,
sk47 = sk49,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c201,plain,
( ~ lt(X12,X10)
| app(X13,cons(X12,nil)) != sk49
| ~ ssList(X13)
| ~ ssItem(X12)
| app(cons(X10,nil),X11) != sk52
| ~ ssList(X11)
| ~ ssItem(X10) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c245,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(X14,X15))
| ssItem(sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c196,plain,
ssList(sk51),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p1687,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,X0))
| ssItem(sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c245,c196]) ).
cnf(c197,plain,
ssList(sk52),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p1748,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p1687,c197]) ).
cnf(p1755,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p1748]) ).
cnf(c199,plain,
strictorderedP(sk49),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p312,plain,
strictorderedP(sk47),
inference(superposition,[status(thm)],[c195,c199]) ).
cnf(p1756,plain,
( nil = sk47
| ssItem(sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p1755,p312]) ).
cnf(p4415,plain,
( nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(X1,sk57(sk51,sk52))
| app(X2,cons(X1,nil)) != sk49
| ~ ssList(X2)
| ~ ssItem(X1)
| app(cons(sk57(sk51,sk52),nil),X0) != sk52
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c201,p1756]) ).
cnf(c247,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(X14,X15))
| ssItem(sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p1859,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,X0))
| ssItem(sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c247,c196]) ).
cnf(p1920,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| ssItem(sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p1859,c197]) ).
cnf(p1927,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p1920]) ).
cnf(p1928,plain,
( nil = sk47
| ssList(sk58(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p1927,p312]) ).
cnf(p13182,plain,
( nil = sk47
| ssItem(sk55(sk51,sk52))
| nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52 ),
inference(resolution,[status(thm)],[p4415,p1928]) ).
cnf(p20430,plain,
( nil = sk47
| nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52 ),
inference(factoring,[status(thm)],[p13182]) ).
cnf(p20432,plain,
( nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52 ),
inference(factoring,[status(thm)],[p20430]) ).
cnf(c249,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(X14,X15),nil),sk58(X14,X15)) = X15
| ssItem(sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p8774,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,X0),nil),sk58(sk51,X0)) = X0
| ssItem(sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c249,c196]) ).
cnf(p8868,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssItem(sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p8774,c197]) ).
cnf(p8881,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p8868]) ).
cnf(p8882,plain,
( nil = sk47
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p8881,p312]) ).
cnf(p20433,plain,
( nil = sk47
| ssItem(sk55(sk51,sk52))
| nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[p20432,p8882]) ).
cnf(p20438,plain,
( nil = sk47
| nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(factoring,[status(thm)],[p20433]) ).
cnf(p20440,plain,
( nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(factoring,[status(thm)],[p20438]) ).
cnf(c251,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(X14,X15))
| ssItem(sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p2171,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,X0))
| ssItem(sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c251,c196]) ).
cnf(p2237,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| ssItem(sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p2171,c197]) ).
cnf(p2245,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p2237]) ).
cnf(p2246,plain,
( nil = sk47
| ssItem(sk59(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p2245,p312]) ).
cnf(p20442,plain,
( nil = sk47
| ssItem(sk55(sk51,sk52))
| nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p20440,p2246]) ).
cnf(p20490,plain,
( nil = sk47
| nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0) ),
inference(factoring,[status(thm)],[p20442]) ).
cnf(p20492,plain,
( nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0) ),
inference(factoring,[status(thm)],[p20490]) ).
cnf(c253,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(X14,X15))
| ssItem(sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p2357,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,X0))
| ssItem(sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c253,c196]) ).
cnf(p2423,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| ssItem(sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p2357,c197]) ).
cnf(p2431,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p2423]) ).
cnf(p2432,plain,
( nil = sk47
| ssList(sk60(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p2431,p312]) ).
cnf(p20498,plain,
( nil = sk47
| ssItem(sk55(sk51,sk52))
| nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49 ),
inference(resolution,[status(thm)],[p20492,p2432]) ).
cnf(p20506,plain,
( nil = sk47
| nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49 ),
inference(factoring,[status(thm)],[p20498]) ).
cnf(p20508,plain,
( nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49 ),
inference(factoring,[status(thm)],[p20506]) ).
cnf(p20509,plain,
( nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk47 ),
inference(superposition,[status(thm)],[c195,p20508]) ).
cnf(c255,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(X14,X15),cons(sk59(X14,X15),nil)) = sk47
| ssItem(sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p9033,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,X0),cons(sk59(sk51,X0),nil)) = sk47
| ssItem(sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c255,c196]) ).
cnf(p9124,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssItem(sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p9033,c197]) ).
cnf(p9137,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p9124]) ).
cnf(p9138,plain,
( nil = sk47
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p9137,p312]) ).
cnf(p20514,plain,
( nil = sk47
| ssItem(sk55(sk51,sk52))
| nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52)) ),
inference(resolution,[status(thm)],[p20509,p9138]) ).
cnf(p20518,plain,
( nil = sk47
| nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52)) ),
inference(factoring,[status(thm)],[p20514]) ).
cnf(p20520,plain,
( nil = sk47
| ssItem(sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52)) ),
inference(factoring,[status(thm)],[p20518]) ).
cnf(c257,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(X14,X15),sk57(X14,X15))
| ssItem(sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p4937,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,X0),sk57(sk51,X0))
| ssItem(sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c257,c196]) ).
cnf(p5028,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p4937,c197]) ).
cnf(p5041,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p5028]) ).
cnf(p5042,plain,
( nil = sk47
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p5041,p312]) ).
cnf(p20521,plain,
( nil = sk47
| ssItem(sk55(sk51,sk52))
| nil = sk47
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p20520,p5042]) ).
cnf(p20524,plain,
( nil = sk47
| nil = sk47
| ssItem(sk55(sk51,sk52)) ),
inference(factoring,[status(thm)],[p20521]) ).
cnf(p20526,plain,
( nil = sk47
| ssItem(sk55(sk51,sk52)) ),
inference(factoring,[status(thm)],[p20524]) ).
cnf(c203,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(X14,X15))
| ssItem(sk53(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p310,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,X0))
| ssItem(sk53(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c203,c196]) ).
cnf(p342,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p310,c197]) ).
cnf(p343,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p342]) ).
cnf(p344,plain,
( nil = sk47
| ssItem(sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p343,p312]) ).
cnf(p4413,plain,
( nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(X1,sk57(sk51,sk52))
| app(X2,cons(X1,nil)) != sk49
| ~ ssList(X2)
| ~ ssItem(X1)
| app(cons(sk57(sk51,sk52),nil),X0) != sk52
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c201,p344]) ).
cnf(c205,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(X14,X15))
| ssItem(sk53(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p399,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,X0))
| ssItem(sk53(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c205,c196]) ).
cnf(p430,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| ssItem(sk53(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p399,c197]) ).
cnf(p431,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p430]) ).
cnf(p432,plain,
( nil = sk47
| ssList(sk58(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p431,p312]) ).
cnf(p13154,plain,
( nil = sk47
| ssItem(sk53(sk51,sk52))
| nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52 ),
inference(resolution,[status(thm)],[p4413,p432]) ).
cnf(p18768,plain,
( nil = sk47
| nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52 ),
inference(factoring,[status(thm)],[p13154]) ).
cnf(p18770,plain,
( nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52 ),
inference(factoring,[status(thm)],[p18768]) ).
cnf(c207,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(X14,X15),nil),sk58(X14,X15)) = X15
| ssItem(sk53(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p6729,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,X0),nil),sk58(sk51,X0)) = X0
| ssItem(sk53(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c207,c196]) ).
cnf(p6820,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssItem(sk53(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p6729,c197]) ).
cnf(p6833,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p6820]) ).
cnf(p6834,plain,
( nil = sk47
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p6833,p312]) ).
cnf(p18771,plain,
( nil = sk47
| ssItem(sk53(sk51,sk52))
| nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[p18770,p6834]) ).
cnf(p18778,plain,
( nil = sk47
| nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(factoring,[status(thm)],[p18771]) ).
cnf(p18780,plain,
( nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(factoring,[status(thm)],[p18778]) ).
cnf(c209,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(X14,X15))
| ssItem(sk53(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p503,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,X0))
| ssItem(sk53(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c209,c196]) ).
cnf(p551,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| ssItem(sk53(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p503,c197]) ).
cnf(p553,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p551]) ).
cnf(p554,plain,
( nil = sk47
| ssItem(sk59(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p553,p312]) ).
cnf(p18782,plain,
( nil = sk47
| ssItem(sk53(sk51,sk52))
| nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p18780,p554]) ).
cnf(p18806,plain,
( nil = sk47
| nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0) ),
inference(factoring,[status(thm)],[p18782]) ).
cnf(p18808,plain,
( nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0) ),
inference(factoring,[status(thm)],[p18806]) ).
cnf(c211,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(X14,X15))
| ssItem(sk53(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p617,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,X0))
| ssItem(sk53(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c211,c196]) ).
cnf(p653,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| ssItem(sk53(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p617,c197]) ).
cnf(p655,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p653]) ).
cnf(p656,plain,
( nil = sk47
| ssList(sk60(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p655,p312]) ).
cnf(p18814,plain,
( nil = sk47
| ssItem(sk53(sk51,sk52))
| nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49 ),
inference(resolution,[status(thm)],[p18808,p656]) ).
cnf(p18823,plain,
( nil = sk47
| nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49 ),
inference(factoring,[status(thm)],[p18814]) ).
cnf(p18825,plain,
( nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49 ),
inference(factoring,[status(thm)],[p18823]) ).
cnf(p18826,plain,
( nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk47 ),
inference(superposition,[status(thm)],[c195,p18825]) ).
cnf(c213,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(X14,X15),cons(sk59(X14,X15),nil)) = sk47
| ssItem(sk53(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p6985,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,X0),cons(sk59(sk51,X0),nil)) = sk47
| ssItem(sk53(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c213,c196]) ).
cnf(p7076,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssItem(sk53(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p6985,c197]) ).
cnf(p7089,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p7076]) ).
cnf(p7090,plain,
( nil = sk47
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p7089,p312]) ).
cnf(p18833,plain,
( nil = sk47
| ssItem(sk53(sk51,sk52))
| nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52)) ),
inference(resolution,[status(thm)],[p18826,p7090]) ).
cnf(p18839,plain,
( nil = sk47
| nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52)) ),
inference(factoring,[status(thm)],[p18833]) ).
cnf(p18841,plain,
( nil = sk47
| ssItem(sk53(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52)) ),
inference(factoring,[status(thm)],[p18839]) ).
cnf(c215,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(X14,X15),sk57(X14,X15))
| ssItem(sk53(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p4425,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,X0),sk57(sk51,X0))
| ssItem(sk53(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c215,c196]) ).
cnf(p4516,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p4425,c197]) ).
cnf(p4529,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p4516]) ).
cnf(p4530,plain,
( nil = sk47
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p4529,p312]) ).
cnf(p18842,plain,
( nil = sk47
| ssItem(sk53(sk51,sk52))
| nil = sk47
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p18841,p4530]) ).
cnf(p18847,plain,
( nil = sk47
| nil = sk47
| ssItem(sk53(sk51,sk52)) ),
inference(factoring,[status(thm)],[p18842]) ).
cnf(p18849,plain,
( nil = sk47
| ssItem(sk53(sk51,sk52)) ),
inference(factoring,[status(thm)],[p18847]) ).
cnf(c200,plain,
( ~ lt(X6,X8)
| app(cons(X8,nil),X9) != sk49
| ~ ssList(X9)
| ~ ssItem(X8)
| app(X7,cons(X6,nil)) != sk51
| ~ ssList(X7)
| ~ ssItem(X6) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p18850,plain,
( ~ lt(sk53(sk51,sk52),X1)
| app(cons(X1,nil),X2) != sk49
| ~ ssList(X2)
| ~ ssItem(X1)
| app(X0,cons(sk53(sk51,sk52),nil)) != sk51
| ~ ssList(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p18849,c200]) ).
cnf(c217,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(X14,X15))
| ssList(sk54(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p775,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,X0))
| ssList(sk54(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c217,c196]) ).
cnf(p816,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| ssList(sk54(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p775,c197]) ).
cnf(p819,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p816]) ).
cnf(p820,plain,
( nil = sk47
| ssItem(sk57(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(resolution,[status(thm)],[p819,p312]) ).
cnf(p18894,plain,
( nil = sk47
| ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) != sk51
| nil = sk47 ),
inference(resolution,[status(thm)],[p18850,p820]) ).
cnf(p18962,plain,
( ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) != sk51
| nil = sk47 ),
inference(factoring,[status(thm)],[p18894]) ).
cnf(c231,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(X14,X15))
| app(sk54(X14,X15),cons(sk53(X14,X15),nil)) = X14
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p7415,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,X0))
| app(sk54(sk51,X0),cons(sk53(sk51,X0),nil)) = sk51
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c231,c196]) ).
cnf(p7985,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p7415,c197]) ).
cnf(p7998,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p7985]) ).
cnf(p7999,plain,
( nil = sk47
| ssItem(sk57(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(resolution,[status(thm)],[p7998,p312]) ).
cnf(p18963,plain,
( nil = sk47
| ssItem(sk57(sk51,sk52))
| ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p18962,p7999]) ).
cnf(p18969,plain,
( nil = sk47
| ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p18963]) ).
cnf(p18970,plain,
( ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p18969]) ).
cnf(p20533,plain,
( ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0)
| nil = sk47
| nil = sk47 ),
inference(resolution,[status(thm)],[p20526,p18970]) ).
cnf(p20567,plain,
( ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p20533]) ).
cnf(c259,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(X14,X15))
| ssList(sk56(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p2711,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,X0))
| ssList(sk56(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c259,c196]) ).
cnf(p2782,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| ssList(sk56(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p2711,c197]) ).
cnf(p2791,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p2782]) ).
cnf(p2792,plain,
( nil = sk47
| ssItem(sk57(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(resolution,[status(thm)],[p2791,p312]) ).
cnf(p20573,plain,
( nil = sk47
| ssItem(sk57(sk51,sk52))
| ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49
| nil = sk47 ),
inference(resolution,[status(thm)],[p20567,p2792]) ).
cnf(p20619,plain,
( nil = sk47
| ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p20573]) ).
cnf(p20620,plain,
( ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p20619]) ).
cnf(p20621,plain,
( ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk47
| nil = sk47 ),
inference(superposition,[status(thm)],[c195,p20620]) ).
cnf(c273,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(X14,X15))
| app(cons(sk55(X14,X15),nil),sk56(X14,X15)) = sk47
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p9801,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,X0))
| app(cons(sk55(sk51,X0),nil),sk56(sk51,X0)) = sk47
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c273,c196]) ).
cnf(p9892,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p9801,c197]) ).
cnf(p9905,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(equality_resolution,[status(thm)],[p9892]) ).
cnf(p9906,plain,
( nil = sk47
| ssItem(sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(resolution,[status(thm)],[p9905,p312]) ).
cnf(p20628,plain,
( nil = sk47
| ssItem(sk57(sk51,sk52))
| ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p20621,p9906]) ).
cnf(p20635,plain,
( nil = sk47
| ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p20628]) ).
cnf(p20636,plain,
( ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p20635]) ).
cnf(c287,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(X14,X15))
| lt(sk53(X14,X15),sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p5449,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,X0))
| lt(sk53(sk51,X0),sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c287,c196]) ).
cnf(p5540,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p5449,c197]) ).
cnf(p5553,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p5540]) ).
cnf(p5554,plain,
( nil = sk47
| ssItem(sk57(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p5553,p312]) ).
cnf(p20637,plain,
( nil = sk47
| ssItem(sk57(sk51,sk52))
| ssItem(sk57(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p20636,p5554]) ).
cnf(p20642,plain,
( nil = sk47
| ssItem(sk57(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p20637]) ).
cnf(p20643,plain,
( ssItem(sk57(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p20642]) ).
cnf(p20646,plain,
( ~ lt(X1,sk57(sk51,sk52))
| app(X2,cons(X1,nil)) != sk49
| ~ ssList(X2)
| ~ ssItem(X1)
| app(cons(sk57(sk51,sk52),nil),X0) != sk52
| ~ ssList(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p20643,c201]) ).
cnf(c261,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(X14,X15))
| ssList(sk56(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p3093,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,X0))
| ssList(sk56(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c261,c196]) ).
cnf(p3169,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| ssList(sk56(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p3093,c197]) ).
cnf(p3179,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p3169]) ).
cnf(p3180,plain,
( nil = sk47
| ssList(sk58(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(resolution,[status(thm)],[p3179,p312]) ).
cnf(p20707,plain,
( nil = sk47
| ssList(sk56(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52
| nil = sk47 ),
inference(resolution,[status(thm)],[p20646,p3180]) ).
cnf(p23121,plain,
( ssList(sk56(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52
| nil = sk47 ),
inference(factoring,[status(thm)],[p20707]) ).
cnf(c263,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(X14,X15),nil),sk58(X14,X15)) = X15
| ssList(sk56(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p9289,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,X0),nil),sk58(sk51,X0)) = X0
| ssList(sk56(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c263,c196]) ).
cnf(p9380,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssList(sk56(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p9289,c197]) ).
cnf(p9393,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p9380]) ).
cnf(p9394,plain,
( nil = sk47
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssList(sk56(sk51,sk52)) ),
inference(resolution,[status(thm)],[p9393,p312]) ).
cnf(p23122,plain,
( nil = sk47
| ssList(sk56(sk51,sk52))
| ssList(sk56(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p23121,p9394]) ).
cnf(p23127,plain,
( nil = sk47
| ssList(sk56(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p23122]) ).
cnf(p23128,plain,
( ssList(sk56(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p23127]) ).
cnf(c223,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(X14,X15))
| ssList(sk54(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p1175,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,X0))
| ssList(sk54(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c223,c196]) ).
cnf(p1226,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| ssList(sk54(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p1175,c197]) ).
cnf(p1231,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p1226]) ).
cnf(p1232,plain,
( nil = sk47
| ssItem(sk59(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(resolution,[status(thm)],[p1231,p312]) ).
cnf(p18896,plain,
( nil = sk47
| ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) != sk51
| nil = sk47 ),
inference(resolution,[status(thm)],[p18850,p1232]) ).
cnf(p18990,plain,
( ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) != sk51
| nil = sk47 ),
inference(factoring,[status(thm)],[p18896]) ).
cnf(c237,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(X14,X15))
| app(sk54(X14,X15),cons(sk53(X14,X15),nil)) = X14
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p8262,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,X0))
| app(sk54(sk51,X0),cons(sk53(sk51,X0),nil)) = sk51
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c237,c196]) ).
cnf(p8353,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p8262,c197]) ).
cnf(p8366,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p8353]) ).
cnf(p8367,plain,
( nil = sk47
| ssItem(sk59(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(resolution,[status(thm)],[p8366,p312]) ).
cnf(p18992,plain,
( nil = sk47
| ssItem(sk59(sk51,sk52))
| ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p18990,p8367]) ).
cnf(p18998,plain,
( nil = sk47
| ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p18992]) ).
cnf(p18999,plain,
( ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p18998]) ).
cnf(p20534,plain,
( ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0)
| nil = sk47
| nil = sk47 ),
inference(resolution,[status(thm)],[p20526,p18999]) ).
cnf(p20580,plain,
( ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p20534]) ).
cnf(c265,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(X14,X15))
| ssList(sk56(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p3503,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,X0))
| ssList(sk56(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c265,c196]) ).
cnf(p3584,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| ssList(sk56(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p3503,c197]) ).
cnf(p3595,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p3584]) ).
cnf(p3596,plain,
( nil = sk47
| ssItem(sk59(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(resolution,[status(thm)],[p3595,p312]) ).
cnf(p20586,plain,
( nil = sk47
| ssItem(sk59(sk51,sk52))
| ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49
| nil = sk47 ),
inference(resolution,[status(thm)],[p20580,p3596]) ).
cnf(p20711,plain,
( nil = sk47
| ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p20586]) ).
cnf(p20712,plain,
( ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p20711]) ).
cnf(p20713,plain,
( ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk47
| nil = sk47 ),
inference(superposition,[status(thm)],[c195,p20712]) ).
cnf(c279,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(X14,X15))
| app(cons(sk55(X14,X15),nil),sk56(X14,X15)) = sk47
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p10313,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,X0))
| app(cons(sk55(sk51,X0),nil),sk56(sk51,X0)) = sk47
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c279,c196]) ).
cnf(p10404,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p10313,c197]) ).
cnf(p10417,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(equality_resolution,[status(thm)],[p10404]) ).
cnf(p10418,plain,
( nil = sk47
| ssItem(sk59(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(resolution,[status(thm)],[p10417,p312]) ).
cnf(p20720,plain,
( nil = sk47
| ssItem(sk59(sk51,sk52))
| ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p20713,p10418]) ).
cnf(p21479,plain,
( nil = sk47
| ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p20720]) ).
cnf(p21480,plain,
( ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p21479]) ).
cnf(c293,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(X14,X15))
| lt(sk53(X14,X15),sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p5961,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,X0))
| lt(sk53(sk51,X0),sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c293,c196]) ).
cnf(p6052,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p5961,c197]) ).
cnf(p6065,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p6052]) ).
cnf(p6066,plain,
( nil = sk47
| ssItem(sk59(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p6065,p312]) ).
cnf(p21481,plain,
( nil = sk47
| ssItem(sk59(sk51,sk52))
| ssItem(sk59(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p21480,p6066]) ).
cnf(p21484,plain,
( nil = sk47
| ssItem(sk59(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p21481]) ).
cnf(p21485,plain,
( ssItem(sk59(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p21484]) ).
cnf(p23132,plain,
( nil = sk47
| ssList(sk56(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p23128,p21485]) ).
cnf(p23178,plain,
( ssList(sk56(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p23132]) ).
cnf(c267,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(X14,X15))
| ssList(sk56(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p3941,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,X0))
| ssList(sk56(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c267,c196]) ).
cnf(p4027,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| ssList(sk56(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p3941,c197]) ).
cnf(p4039,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p4027]) ).
cnf(p4040,plain,
( nil = sk47
| ssList(sk60(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(resolution,[status(thm)],[p4039,p312]) ).
cnf(p23184,plain,
( nil = sk47
| ssList(sk56(sk51,sk52))
| ssList(sk56(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49
| nil = sk47 ),
inference(resolution,[status(thm)],[p23178,p4040]) ).
cnf(p23206,plain,
( nil = sk47
| ssList(sk56(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p23184]) ).
cnf(p23207,plain,
( ssList(sk56(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p23206]) ).
cnf(p23208,plain,
( ssList(sk56(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk47
| nil = sk47 ),
inference(superposition,[status(thm)],[c195,p23207]) ).
cnf(c269,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(X14,X15),cons(sk59(X14,X15),nil)) = sk47
| ssList(sk56(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p9545,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,X0),cons(sk59(sk51,X0),nil)) = sk47
| ssList(sk56(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c269,c196]) ).
cnf(p9636,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssList(sk56(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p9545,c197]) ).
cnf(p9649,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p9636]) ).
cnf(p9650,plain,
( nil = sk47
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssList(sk56(sk51,sk52)) ),
inference(resolution,[status(thm)],[p9649,p312]) ).
cnf(p23212,plain,
( nil = sk47
| ssList(sk56(sk51,sk52))
| ssList(sk56(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p23208,p9650]) ).
cnf(p23216,plain,
( nil = sk47
| ssList(sk56(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p23212]) ).
cnf(p23217,plain,
( ssList(sk56(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p23216]) ).
cnf(c271,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(X14,X15),sk57(X14,X15))
| ssList(sk56(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p5193,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,X0),sk57(sk51,X0))
| ssList(sk56(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c271,c196]) ).
cnf(p5284,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk56(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p5193,c197]) ).
cnf(p5297,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p5284]) ).
cnf(p5298,plain,
( nil = sk47
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(resolution,[status(thm)],[p5297,p312]) ).
cnf(p23218,plain,
( nil = sk47
| ssList(sk56(sk51,sk52))
| ssList(sk56(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p23217,p5298]) ).
cnf(p23221,plain,
( nil = sk47
| ssList(sk56(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p23218]) ).
cnf(p23222,plain,
( ssList(sk56(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p23221]) ).
cnf(c219,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(X14,X15))
| ssList(sk54(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p961,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,X0))
| ssList(sk54(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c219,c196]) ).
cnf(p1007,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| ssList(sk54(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p961,c197]) ).
cnf(p1011,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p1007]) ).
cnf(p1012,plain,
( nil = sk47
| ssList(sk58(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(resolution,[status(thm)],[p1011,p312]) ).
cnf(p20704,plain,
( nil = sk47
| ssList(sk54(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52
| nil = sk47 ),
inference(resolution,[status(thm)],[p20646,p1012]) ).
cnf(p21616,plain,
( ssList(sk54(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52
| nil = sk47 ),
inference(factoring,[status(thm)],[p20704]) ).
cnf(c221,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(X14,X15),nil),sk58(X14,X15)) = X15
| ssList(sk54(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p7241,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,X0),nil),sk58(sk51,X0)) = X0
| ssList(sk54(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c221,c196]) ).
cnf(p7326,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssList(sk54(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p7241,c197]) ).
cnf(p7339,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p7326]) ).
cnf(p7340,plain,
( nil = sk47
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssList(sk54(sk51,sk52)) ),
inference(resolution,[status(thm)],[p7339,p312]) ).
cnf(p21617,plain,
( nil = sk47
| ssList(sk54(sk51,sk52))
| ssList(sk54(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p21616,p7340]) ).
cnf(p21623,plain,
( nil = sk47
| ssList(sk54(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p21617]) ).
cnf(p21624,plain,
( ssList(sk54(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p21623]) ).
cnf(p21628,plain,
( nil = sk47
| ssList(sk54(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p21624,p21485]) ).
cnf(p21668,plain,
( ssList(sk54(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p21628]) ).
cnf(c225,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(X14,X15))
| ssList(sk54(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p1417,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,X0))
| ssList(sk54(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c225,c196]) ).
cnf(p1473,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| ssList(sk54(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p1417,c197]) ).
cnf(p1479,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p1473]) ).
cnf(p1480,plain,
( nil = sk47
| ssList(sk60(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(resolution,[status(thm)],[p1479,p312]) ).
cnf(p21674,plain,
( nil = sk47
| ssList(sk54(sk51,sk52))
| ssList(sk54(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49
| nil = sk47 ),
inference(resolution,[status(thm)],[p21668,p1480]) ).
cnf(p21694,plain,
( nil = sk47
| ssList(sk54(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p21674]) ).
cnf(p21695,plain,
( ssList(sk54(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p21694]) ).
cnf(p21696,plain,
( ssList(sk54(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk47
| nil = sk47 ),
inference(superposition,[status(thm)],[c195,p21695]) ).
cnf(c227,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(X14,X15),cons(sk59(X14,X15),nil)) = sk47
| ssList(sk54(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p7379,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,X0),cons(sk59(sk51,X0),nil)) = sk47
| ssList(sk54(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c227,c196]) ).
cnf(p7765,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssList(sk54(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p7379,c197]) ).
cnf(p7778,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p7765]) ).
cnf(p7779,plain,
( nil = sk47
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssList(sk54(sk51,sk52)) ),
inference(resolution,[status(thm)],[p7778,p312]) ).
cnf(p21701,plain,
( nil = sk47
| ssList(sk54(sk51,sk52))
| ssList(sk54(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p21696,p7779]) ).
cnf(p21706,plain,
( nil = sk47
| ssList(sk54(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p21701]) ).
cnf(p21707,plain,
( ssList(sk54(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p21706]) ).
cnf(c229,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(X14,X15),sk57(X14,X15))
| ssList(sk54(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p4681,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,X0),sk57(sk51,X0))
| ssList(sk54(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c229,c196]) ).
cnf(p4772,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk54(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p4681,c197]) ).
cnf(p4785,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p4772]) ).
cnf(p4786,plain,
( nil = sk47
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(resolution,[status(thm)],[p4785,p312]) ).
cnf(p21708,plain,
( nil = sk47
| ssList(sk54(sk51,sk52))
| ssList(sk54(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p21707,p4786]) ).
cnf(p21712,plain,
( nil = sk47
| ssList(sk54(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p21708]) ).
cnf(p21713,plain,
( ssList(sk54(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p21712]) ).
cnf(p22450,plain,
( ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) != sk51
| nil = sk47
| nil = sk47 ),
inference(resolution,[status(thm)],[p21713,p18850]) ).
cnf(p22802,plain,
( ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) != sk51
| nil = sk47 ),
inference(factoring,[status(thm)],[p22450]) ).
cnf(c233,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(X14,X15))
| app(sk54(X14,X15),cons(sk53(X14,X15),nil)) = X14
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p7451,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,X0))
| app(sk54(sk51,X0),cons(sk53(sk51,X0),nil)) = sk51
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c233,c196]) ).
cnf(p8205,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p7451,c197]) ).
cnf(p8218,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p8205]) ).
cnf(p8219,plain,
( nil = sk47
| ssList(sk58(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(resolution,[status(thm)],[p8218,p312]) ).
cnf(p22803,plain,
( nil = sk47
| ssList(sk58(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p22802,p8219]) ).
cnf(p22806,plain,
( ssList(sk58(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p22803]) ).
cnf(p22808,plain,
( nil = sk47
| ssList(sk58(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p22806,p20526]) ).
cnf(p22827,plain,
( ssList(sk58(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p22808]) ).
cnf(p23942,plain,
( ssList(sk58(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49
| nil = sk47
| nil = sk47 ),
inference(resolution,[status(thm)],[p23222,p22827]) ).
cnf(p23963,plain,
( ssList(sk58(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p23942]) ).
cnf(p23964,plain,
( ssList(sk58(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk47
| nil = sk47 ),
inference(superposition,[status(thm)],[c195,p23963]) ).
cnf(c275,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(X14,X15))
| app(cons(sk55(X14,X15),nil),sk56(X14,X15)) = sk47
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p10057,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,X0))
| app(cons(sk55(sk51,X0),nil),sk56(sk51,X0)) = sk47
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c275,c196]) ).
cnf(p10148,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p10057,c197]) ).
cnf(p10161,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(equality_resolution,[status(thm)],[p10148]) ).
cnf(p10162,plain,
( nil = sk47
| ssList(sk58(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(resolution,[status(thm)],[p10161,p312]) ).
cnf(p23969,plain,
( nil = sk47
| ssList(sk58(sk51,sk52))
| ssList(sk58(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p23964,p10162]) ).
cnf(p23974,plain,
( nil = sk47
| ssList(sk58(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p23969]) ).
cnf(p23975,plain,
( ssList(sk58(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p23974]) ).
cnf(c289,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(X14,X15))
| lt(sk53(X14,X15),sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p5705,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,X0))
| lt(sk53(sk51,X0),sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c289,c196]) ).
cnf(p5796,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p5705,c197]) ).
cnf(p5809,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p5796]) ).
cnf(p5810,plain,
( nil = sk47
| ssList(sk58(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p5809,p312]) ).
cnf(p23976,plain,
( nil = sk47
| ssList(sk58(sk51,sk52))
| ssList(sk58(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p23975,p5810]) ).
cnf(p23979,plain,
( nil = sk47
| ssList(sk58(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p23976]) ).
cnf(p23980,plain,
( ssList(sk58(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p23979]) ).
cnf(p24678,plain,
( ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52
| nil = sk47
| nil = sk47 ),
inference(resolution,[status(thm)],[p23980,p20646]) ).
cnf(p26424,plain,
( ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52
| nil = sk47 ),
inference(factoring,[status(thm)],[p24678]) ).
cnf(c235,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(X14,X15),nil),sk58(X14,X15)) = X15
| app(sk54(X14,X15),cons(sk53(X14,X15),nil)) = X14
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p14961,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,X0),nil),sk58(sk51,X0)) = X0
| app(sk54(sk51,X0),cons(sk53(sk51,X0),nil)) = sk51
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c235,c196]) ).
cnf(p15052,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p14961,c197]) ).
cnf(p15065,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p15052]) ).
cnf(p15066,plain,
( nil = sk47
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(resolution,[status(thm)],[p15065,p312]) ).
cnf(p26426,plain,
( nil = sk47
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p26424,p15066]) ).
cnf(p26601,plain,
( app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p26426]) ).
cnf(p26605,plain,
( nil = sk47
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p26601,p21485]) ).
cnf(p26911,plain,
( app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p26605]) ).
cnf(c239,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(X14,X15))
| app(sk54(X14,X15),cons(sk53(X14,X15),nil)) = X14
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p8518,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,X0))
| app(sk54(sk51,X0),cons(sk53(sk51,X0),nil)) = sk51
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c239,c196]) ).
cnf(p8609,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p8518,c197]) ).
cnf(p8622,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p8609]) ).
cnf(p8623,plain,
( nil = sk47
| ssList(sk60(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(resolution,[status(thm)],[p8622,p312]) ).
cnf(p22804,plain,
( nil = sk47
| ssList(sk60(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p22802,p8623]) ).
cnf(p22811,plain,
( ssList(sk60(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p22804]) ).
cnf(p22813,plain,
( nil = sk47
| ssList(sk60(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p22811,p20526]) ).
cnf(p22871,plain,
( ssList(sk60(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p22813]) ).
cnf(p23946,plain,
( ssList(sk60(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49
| nil = sk47
| nil = sk47 ),
inference(resolution,[status(thm)],[p23222,p22871]) ).
cnf(p24717,plain,
( ssList(sk60(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p23946]) ).
cnf(p24718,plain,
( ssList(sk60(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk47
| nil = sk47 ),
inference(superposition,[status(thm)],[c195,p24717]) ).
cnf(c281,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(X14,X15))
| app(cons(sk55(X14,X15),nil),sk56(X14,X15)) = sk47
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p10569,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,X0))
| app(cons(sk55(sk51,X0),nil),sk56(sk51,X0)) = sk47
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c281,c196]) ).
cnf(p10660,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p10569,c197]) ).
cnf(p10673,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(equality_resolution,[status(thm)],[p10660]) ).
cnf(p10674,plain,
( nil = sk47
| ssList(sk60(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(resolution,[status(thm)],[p10673,p312]) ).
cnf(p24722,plain,
( nil = sk47
| ssList(sk60(sk51,sk52))
| ssList(sk60(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p24718,p10674]) ).
cnf(p24726,plain,
( nil = sk47
| ssList(sk60(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p24722]) ).
cnf(p24727,plain,
( ssList(sk60(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p24726]) ).
cnf(c295,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(X14,X15))
| lt(sk53(X14,X15),sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p6217,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,X0))
| lt(sk53(sk51,X0),sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c295,c196]) ).
cnf(p6308,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p6217,c197]) ).
cnf(p6321,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p6308]) ).
cnf(p6322,plain,
( nil = sk47
| ssList(sk60(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p6321,p312]) ).
cnf(p24728,plain,
( nil = sk47
| ssList(sk60(sk51,sk52))
| ssList(sk60(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p24727,p6322]) ).
cnf(p24730,plain,
( nil = sk47
| ssList(sk60(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p24728]) ).
cnf(p24731,plain,
( ssList(sk60(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p24730]) ).
cnf(p26919,plain,
( nil = sk47
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49
| nil = sk47 ),
inference(resolution,[status(thm)],[p26911,p24731]) ).
cnf(p26929,plain,
( app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p26919]) ).
cnf(p26930,plain,
( app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk47
| nil = sk47 ),
inference(superposition,[status(thm)],[c195,p26929]) ).
cnf(c241,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(X14,X15),cons(sk59(X14,X15),nil)) = sk47
| app(sk54(X14,X15),cons(sk53(X14,X15),nil)) = X14
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p15217,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,X0),cons(sk59(sk51,X0),nil)) = sk47
| app(sk54(sk51,X0),cons(sk53(sk51,X0),nil)) = sk51
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c241,c196]) ).
cnf(p15308,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p15217,c197]) ).
cnf(p15321,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p15308]) ).
cnf(p15322,plain,
( nil = sk47
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(resolution,[status(thm)],[p15321,p312]) ).
cnf(p26932,plain,
( nil = sk47
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p26930,p15322]) ).
cnf(p26934,plain,
( nil = sk47
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p26932]) ).
cnf(p26935,plain,
( app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p26934]) ).
cnf(c291,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(X14,X15),nil),sk58(X14,X15)) = X15
| lt(sk53(X14,X15),sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p12593,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,X0),nil),sk58(sk51,X0)) = X0
| lt(sk53(sk51,X0),sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c291,c196]) ).
cnf(p12684,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p12593,c197]) ).
cnf(p12697,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p12684]) ).
cnf(p12698,plain,
( nil = sk47
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p12697,p312]) ).
cnf(p26425,plain,
( nil = sk47
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p26424,p12698]) ).
cnf(p26428,plain,
( lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p26425]) ).
cnf(p26432,plain,
( nil = sk47
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p26428,p21485]) ).
cnf(p26493,plain,
( lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p26432]) ).
cnf(p26501,plain,
( nil = sk47
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49
| nil = sk47 ),
inference(resolution,[status(thm)],[p26493,p24731]) ).
cnf(p26511,plain,
( lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p26501]) ).
cnf(p26512,plain,
( lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk47
| nil = sk47 ),
inference(superposition,[status(thm)],[c195,p26511]) ).
cnf(c297,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(X14,X15),cons(sk59(X14,X15),nil)) = sk47
| lt(sk53(X14,X15),sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p12849,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,X0),cons(sk59(sk51,X0),nil)) = sk47
| lt(sk53(sk51,X0),sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c297,c196]) ).
cnf(p12940,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p12849,c197]) ).
cnf(p12953,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p12940]) ).
cnf(p12954,plain,
( nil = sk47
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p12953,p312]) ).
cnf(p26515,plain,
( nil = sk47
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p26512,p12954]) ).
cnf(p26518,plain,
( nil = sk47
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p26515]) ).
cnf(p26519,plain,
( lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p26518]) ).
cnf(c299,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(X14,X15),sk57(X14,X15))
| lt(sk53(X14,X15),sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p6473,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,X0),sk57(sk51,X0))
| lt(sk53(sk51,X0),sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c299,c196]) ).
cnf(p6564,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p6473,c197]) ).
cnf(p6577,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p6564]) ).
cnf(p6578,plain,
( nil = sk47
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p6577,p312]) ).
cnf(p26520,plain,
( nil = sk47
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p26519,p6578]) ).
cnf(p26522,plain,
( nil = sk47
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p26520]) ).
cnf(p26523,plain,
( lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p26522]) ).
cnf(c243,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(X14,X15),sk57(X14,X15))
| app(sk54(X14,X15),cons(sk53(X14,X15),nil)) = X14
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p12081,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,X0),sk57(sk51,X0))
| app(sk54(sk51,X0),cons(sk53(sk51,X0),nil)) = sk51
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c243,c196]) ).
cnf(p12172,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p12081,c197]) ).
cnf(p12185,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p12172]) ).
cnf(p12186,plain,
( nil = sk47
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(resolution,[status(thm)],[p12185,p312]) ).
cnf(p22805,plain,
( nil = sk47
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p22802,p12186]) ).
cnf(p22904,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p22805]) ).
cnf(p22906,plain,
( nil = sk47
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p22904,p20526]) ).
cnf(p22920,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p22906]) ).
cnf(p23950,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49
| nil = sk47
| nil = sk47 ),
inference(resolution,[status(thm)],[p23222,p22920]) ).
cnf(p25752,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p23950]) ).
cnf(p25753,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk47
| nil = sk47 ),
inference(superposition,[status(thm)],[c195,p25752]) ).
cnf(c285,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(X14,X15),sk57(X14,X15))
| app(cons(sk55(X14,X15),nil),sk56(X14,X15)) = sk47
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p12337,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,X0),sk57(sk51,X0))
| app(cons(sk55(sk51,X0),nil),sk56(sk51,X0)) = sk47
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c285,c196]) ).
cnf(p12428,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p12337,c197]) ).
cnf(p12441,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(equality_resolution,[status(thm)],[p12428]) ).
cnf(p12442,plain,
( nil = sk47
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(resolution,[status(thm)],[p12441,p312]) ).
cnf(p25756,plain,
( nil = sk47
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p25753,p12442]) ).
cnf(p25759,plain,
( nil = sk47
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p25756]) ).
cnf(p25760,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p25759]) ).
cnf(p26524,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil = sk47
| nil = sk47 ),
inference(resolution,[status(thm)],[p26523,p25760]) ).
cnf(p26525,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p26524]) ).
cnf(p26936,plain,
( nil = sk47
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| nil = sk47 ),
inference(resolution,[status(thm)],[p26935,p26525]) ).
cnf(p26937,plain,
( app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| nil = sk47 ),
inference(factoring,[status(thm)],[p26936]) ).
cnf(p26939,plain,
( ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47
| nil = sk47 ),
inference(resolution,[status(thm)],[p26937,p22802]) ).
cnf(p26945,plain,
( ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p26939]) ).
cnf(p26947,plain,
( nil = sk47
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p26945,p20526]) ).
cnf(p26978,plain,
( ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p26947]) ).
cnf(p26984,plain,
( nil = sk47
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49
| nil = sk47 ),
inference(resolution,[status(thm)],[p26978,p23222]) ).
cnf(p26992,plain,
( ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p26984]) ).
cnf(p26993,plain,
( ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk47
| nil = sk47 ),
inference(superposition,[status(thm)],[c195,p26992]) ).
cnf(c283,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(X14,X15),cons(sk59(X14,X15),nil)) = sk47
| app(cons(sk55(X14,X15),nil),sk56(X14,X15)) = sk47
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p15729,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,X0),cons(sk59(sk51,X0),nil)) = sk47
| app(cons(sk55(sk51,X0),nil),sk56(sk51,X0)) = sk47
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c283,c196]) ).
cnf(p15820,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p15729,c197]) ).
cnf(p15833,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(equality_resolution,[status(thm)],[p15820]) ).
cnf(p15834,plain,
( nil = sk47
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(resolution,[status(thm)],[p15833,p312]) ).
cnf(p26995,plain,
( nil = sk47
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p26993,p15834]) ).
cnf(p27000,plain,
( app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p26995]) ).
cnf(p27001,plain,
( nil = sk47
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| nil = sk47 ),
inference(resolution,[status(thm)],[p27000,p26523]) ).
cnf(p27002,plain,
( app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| nil = sk47 ),
inference(factoring,[status(thm)],[p27001]) ).
cnf(c277,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(X14,X15),nil),sk58(X14,X15)) = X15
| app(cons(sk55(X14,X15),nil),sk56(X14,X15)) = sk47
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p15473,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,X0),nil),sk58(sk51,X0)) = X0
| app(cons(sk55(sk51,X0),nil),sk56(sk51,X0)) = sk47
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c277,c196]) ).
cnf(p15564,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p15473,c197]) ).
cnf(p15577,plain,
( nil = sk47
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(equality_resolution,[status(thm)],[p15564]) ).
cnf(p15578,plain,
( nil = sk47
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(resolution,[status(thm)],[p15577,p312]) ).
cnf(p26427,plain,
( nil = sk47
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p26424,p15578]) ).
cnf(p26606,plain,
( app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p26427]) ).
cnf(p26610,plain,
( nil = sk47
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(resolution,[status(thm)],[p26606,p21485]) ).
cnf(p27114,plain,
( app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0)
| nil = sk47 ),
inference(factoring,[status(thm)],[p26610]) ).
cnf(p27122,plain,
( nil = sk47
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49
| nil = sk47 ),
inference(resolution,[status(thm)],[p27114,p24731]) ).
cnf(p27132,plain,
( app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p27122]) ).
cnf(p27134,plain,
( app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| sk47 != sk49
| nil = sk47
| nil = sk47 ),
inference(superposition,[status(thm)],[p27002,p27132]) ).
cnf(p27135,plain,
( app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| sk47 != sk49
| nil = sk47 ),
inference(factoring,[status(thm)],[p27134]) ).
cnf(p27136,plain,
( app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil = sk47 ),
inference(resolution,[status(thm)],[p27135,c195]) ).
cnf(p27137,plain,
( nil = sk47
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| nil = sk47 ),
inference(resolution,[status(thm)],[p27136,p26525]) ).
cnf(p27138,plain,
( app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| nil = sk47 ),
inference(factoring,[status(thm)],[p27137]) ).
cnf(p27142,plain,
( ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47
| nil = sk47 ),
inference(resolution,[status(thm)],[p27138,p26993]) ).
cnf(p27143,plain,
( ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil = sk47 ),
inference(factoring,[status(thm)],[p27142]) ).
cnf(p27144,plain,
( nil = sk47
| nil = sk47 ),
inference(resolution,[status(thm)],[p27143,p26523]) ).
cnf(p27145,plain,
nil = sk47,
inference(factoring,[status(thm)],[p27144]) ).
cnf(c194,plain,
sk48 = sk50,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(c198,plain,
app(app(sk51,sk49),sk52) = sk50,
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p301,plain,
sk50 = sk48,
inference(superposition,[status(thm)],[c194,c198]) ).
cnf(c202,plain,
( nil != sk49
| nil = sk50 ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p303,plain,
( nil != sk49
| nil = sk48 ),
inference(demodulation,[status(thm)],[p301,c202]) ).
cnf(p305,plain,
( nil != sk47
| nil = sk48 ),
inference(superposition,[status(thm)],[c195,p303]) ).
cnf(p27148,plain,
nil = sk48,
inference(resolution,[status(thm)],[p27145,p305]) ).
cnf(p32112,plain,
sk48 = nil,
inference(superposition,[status(thm)],[p27148,p301]) ).
cnf(p27146,plain,
nil = sk49,
inference(superposition,[status(thm)],[p27145,c195]) ).
cnf(p30040,plain,
sk47 = nil,
inference(superposition,[status(thm)],[p27146,c195]) ).
cnf(c276,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(X14,X15))
| app(cons(sk55(X14,X15),nil),sk56(X14,X15)) = sk47
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p10185,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,X0))
| app(cons(sk55(sk51,X0),nil),sk56(sk51,X0)) = sk47
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c276,c196]) ).
cnf(p10276,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p10185,c197]) ).
cnf(p10289,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(equality_resolution,[status(thm)],[p10276]) ).
cnf(p10290,plain,
( nil != sk48
| ssList(sk58(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(resolution,[status(thm)],[p10289,p312]) ).
cnf(p31688,plain,
( nil != sk48
| ssList(sk58(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(demodulation,[status(thm)],[p30040,p10290]) ).
cnf(p33332,plain,
( nil != nil
| ssList(sk58(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(demodulation,[status(thm)],[p32112,p31688]) ).
cnf(p33689,plain,
( ssList(sk58(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(equality_resolution,[status(thm)],[p33332]) ).
cnf(c270,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(X14,X15),cons(sk59(X14,X15),nil)) = sk47
| ssList(sk56(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p9673,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,X0),cons(sk59(sk51,X0),nil)) = sk47
| ssList(sk56(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c270,c196]) ).
cnf(p9764,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssList(sk56(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p9673,c197]) ).
cnf(p9777,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p9764]) ).
cnf(p9778,plain,
( nil != sk48
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssList(sk56(sk51,sk52)) ),
inference(resolution,[status(thm)],[p9777,p312]) ).
cnf(p31604,plain,
( nil != sk48
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| ssList(sk56(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p30040,p9778]) ).
cnf(p33272,plain,
( nil != nil
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| ssList(sk56(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p31604]) ).
cnf(p33687,plain,
( app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p33272]) ).
cnf(c274,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(X14,X15))
| app(cons(sk55(X14,X15),nil),sk56(X14,X15)) = sk47
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p9929,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,X0))
| app(cons(sk55(sk51,X0),nil),sk56(sk51,X0)) = sk47
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c274,c196]) ).
cnf(p10020,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p9929,c197]) ).
cnf(p10033,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(equality_resolution,[status(thm)],[p10020]) ).
cnf(p10034,plain,
( nil != sk48
| ssItem(sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(resolution,[status(thm)],[p10033,p312]) ).
cnf(p31646,plain,
( nil != sk48
| ssItem(sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(demodulation,[status(thm)],[p30040,p10034]) ).
cnf(p33302,plain,
( nil != nil
| ssItem(sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(demodulation,[status(thm)],[p32112,p31646]) ).
cnf(p33688,plain,
( ssItem(sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(equality_resolution,[status(thm)],[p33302]) ).
cnf(c256,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(X14,X15),cons(sk59(X14,X15),nil)) = sk47
| ssItem(sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p9161,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,X0),cons(sk59(sk51,X0),nil)) = sk47
| ssItem(sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c256,c196]) ).
cnf(p9252,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssItem(sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p9161,c197]) ).
cnf(p9265,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p9252]) ).
cnf(p9266,plain,
( nil != sk48
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p9265,p312]) ).
cnf(p31521,plain,
( nil != sk48
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| ssItem(sk55(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p30040,p9266]) ).
cnf(p33213,plain,
( nil != nil
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| ssItem(sk55(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p31521]) ).
cnf(p33686,plain,
( app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p33213]) ).
cnf(c246,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(X14,X15))
| ssItem(sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p1773,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,X0))
| ssItem(sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c246,c196]) ).
cnf(p1834,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p1773,c197]) ).
cnf(p1841,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p1834]) ).
cnf(p1842,plain,
( nil != sk48
| ssItem(sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p1841,p312]) ).
cnf(p32123,plain,
( nil != nil
| ssItem(sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p1842]) ).
cnf(p33651,plain,
( ssItem(sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32123]) ).
cnf(p33654,plain,
( ~ lt(X1,sk57(sk51,sk52))
| app(X2,cons(X1,nil)) != sk49
| ~ ssList(X2)
| ~ ssItem(X1)
| app(cons(sk57(sk51,sk52),nil),X0) != sk52
| ~ ssList(X0)
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p33651,c201]) ).
cnf(c248,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(X14,X15))
| ssItem(sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p2078,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,X0))
| ssItem(sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c248,c196]) ).
cnf(p2144,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| ssItem(sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p2078,c197]) ).
cnf(p2152,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p2144]) ).
cnf(p2153,plain,
( nil != sk48
| ssList(sk58(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p2152,p312]) ).
cnf(p32124,plain,
( nil != nil
| ssList(sk58(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p2153]) ).
cnf(p33656,plain,
( ssList(sk58(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32124]) ).
cnf(p39861,plain,
( ssItem(sk55(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p33654,p33656]) ).
cnf(p41988,plain,
( ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52
| ssItem(sk55(sk51,sk52)) ),
inference(factoring,[status(thm)],[p39861]) ).
cnf(c250,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(X14,X15),nil),sk58(X14,X15)) = X15
| ssItem(sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p8905,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,X0),nil),sk58(sk51,X0)) = X0
| ssItem(sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c250,c196]) ).
cnf(p8996,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssItem(sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p8905,c197]) ).
cnf(p9009,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p8996]) ).
cnf(p9010,plain,
( nil != sk48
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p9009,p312]) ).
cnf(p32146,plain,
( nil != nil
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssItem(sk55(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p9010]) ).
cnf(p33682,plain,
( app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32146]) ).
cnf(p41989,plain,
( ssItem(sk55(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p41988,p33682]) ).
cnf(p41994,plain,
( ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| ssItem(sk55(sk51,sk52)) ),
inference(factoring,[status(thm)],[p41989]) ).
cnf(c252,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(X14,X15))
| ssItem(sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p2264,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,X0))
| ssItem(sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c252,c196]) ).
cnf(p2330,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| ssItem(sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p2264,c197]) ).
cnf(p2338,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p2330]) ).
cnf(p2339,plain,
( nil != sk48
| ssItem(sk59(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p2338,p312]) ).
cnf(p32125,plain,
( nil != nil
| ssItem(sk59(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p2339]) ).
cnf(p33657,plain,
( ssItem(sk59(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32125]) ).
cnf(p41996,plain,
( ssItem(sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0)
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p41994,p33657]) ).
cnf(p42029,plain,
( ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0)
| ssItem(sk55(sk51,sk52)) ),
inference(factoring,[status(thm)],[p41996]) ).
cnf(c254,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(X14,X15))
| ssItem(sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p2611,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,X0))
| ssItem(sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c254,c196]) ).
cnf(p2682,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| ssItem(sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p2611,c197]) ).
cnf(p2691,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p2682]) ).
cnf(p2692,plain,
( nil != sk48
| ssList(sk60(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p2691,p312]) ).
cnf(p32126,plain,
( nil != nil
| ssList(sk60(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p2692]) ).
cnf(p33662,plain,
( ssList(sk60(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32126]) ).
cnf(p42033,plain,
( ssItem(sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p42029,p33662]) ).
cnf(p42041,plain,
( ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49
| ssItem(sk55(sk51,sk52)) ),
inference(factoring,[status(thm)],[p42033]) ).
cnf(p42043,plain,
( ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil != sk49
| ssItem(sk55(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(superposition,[status(thm)],[p33686,p42041]) ).
cnf(p42047,plain,
( ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil != sk49
| ssItem(sk55(sk51,sk52)) ),
inference(factoring,[status(thm)],[p42043]) ).
cnf(p42048,plain,
( ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p42047,p27146]) ).
cnf(c258,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(X14,X15),sk57(X14,X15))
| ssItem(sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p5065,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,X0),sk57(sk51,X0))
| ssItem(sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c258,c196]) ).
cnf(p5156,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p5065,c197]) ).
cnf(p5169,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p5156]) ).
cnf(p5170,plain,
( nil != sk48
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p5169,p312]) ).
cnf(p32133,plain,
( nil != nil
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p5170]) ).
cnf(p33669,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32133]) ).
cnf(p42049,plain,
( ssItem(sk55(sk51,sk52))
| ssItem(sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p42048,p33669]) ).
cnf(p42052,plain,
ssItem(sk55(sk51,sk52)),
inference(factoring,[status(thm)],[p42049]) ).
cnf(c214,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(X14,X15),cons(sk59(X14,X15),nil)) = sk47
| ssItem(sk53(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p7113,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,X0),cons(sk59(sk51,X0),nil)) = sk47
| ssItem(sk53(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c214,c196]) ).
cnf(p7204,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssItem(sk53(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p7113,c197]) ).
cnf(p7217,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p7204]) ).
cnf(p7218,plain,
( nil != sk48
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p7217,p312]) ).
cnf(p31191,plain,
( nil != sk48
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| ssItem(sk53(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p30040,p7218]) ).
cnf(p32979,plain,
( nil != nil
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| ssItem(sk53(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p31191]) ).
cnf(p33684,plain,
( app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32979]) ).
cnf(c204,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(X14,X15))
| ssItem(sk53(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p355,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,X0))
| ssItem(sk53(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c204,c196]) ).
cnf(p386,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p355,c197]) ).
cnf(p387,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p386]) ).
cnf(p388,plain,
( nil != sk48
| ssItem(sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p387,p312]) ).
cnf(p32115,plain,
( nil != nil
| ssItem(sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p388]) ).
cnf(p33635,plain,
( ssItem(sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32115]) ).
cnf(p33638,plain,
( ~ lt(X1,sk57(sk51,sk52))
| app(X2,cons(X1,nil)) != sk49
| ~ ssList(X2)
| ~ ssItem(X1)
| app(cons(sk57(sk51,sk52),nil),X0) != sk52
| ~ ssList(X0)
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p33635,c201]) ).
cnf(c206,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(X14,X15))
| ssItem(sk53(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p464,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,X0))
| ssItem(sk53(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c206,c196]) ).
cnf(p492,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| ssItem(sk53(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p464,c197]) ).
cnf(p506,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p492]) ).
cnf(p507,plain,
( nil != sk48
| ssList(sk58(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p506,p312]) ).
cnf(p32116,plain,
( nil != nil
| ssList(sk58(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p507]) ).
cnf(p33640,plain,
( ssList(sk58(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32116]) ).
cnf(p39813,plain,
( ssItem(sk53(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p33638,p33640]) ).
cnf(p41119,plain,
( ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52
| ssItem(sk53(sk51,sk52)) ),
inference(factoring,[status(thm)],[p39813]) ).
cnf(c208,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(X14,X15),nil),sk58(X14,X15)) = X15
| ssItem(sk53(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p6857,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,X0),nil),sk58(sk51,X0)) = X0
| ssItem(sk53(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c208,c196]) ).
cnf(p6948,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssItem(sk53(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p6857,c197]) ).
cnf(p6961,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p6948]) ).
cnf(p6962,plain,
( nil != sk48
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p6961,p312]) ).
cnf(p32140,plain,
( nil != nil
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssItem(sk53(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p6962]) ).
cnf(p33676,plain,
( app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32140]) ).
cnf(p41120,plain,
( ssItem(sk53(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p41119,p33676]) ).
cnf(p41127,plain,
( ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| ssItem(sk53(sk51,sk52)) ),
inference(factoring,[status(thm)],[p41120]) ).
cnf(c210,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(X14,X15))
| ssItem(sk53(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p566,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,X0))
| ssItem(sk53(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c210,c196]) ).
cnf(p602,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| ssItem(sk53(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p566,c197]) ).
cnf(p604,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p602]) ).
cnf(p605,plain,
( nil != sk48
| ssItem(sk59(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p604,p312]) ).
cnf(p32117,plain,
( nil != nil
| ssItem(sk59(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p605]) ).
cnf(p33641,plain,
( ssItem(sk59(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32117]) ).
cnf(p41129,plain,
( ssItem(sk53(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0)
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p41127,p33641]) ).
cnf(p41147,plain,
( ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0)
| ssItem(sk53(sk51,sk52)) ),
inference(factoring,[status(thm)],[p41129]) ).
cnf(c212,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(X14,X15))
| ssItem(sk53(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p717,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,X0))
| ssItem(sk53(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c212,c196]) ).
cnf(p758,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| ssItem(sk53(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p717,c197]) ).
cnf(p761,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p758]) ).
cnf(p762,plain,
( nil != sk48
| ssList(sk60(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p761,p312]) ).
cnf(p32118,plain,
( nil != nil
| ssList(sk60(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p762]) ).
cnf(p33646,plain,
( ssList(sk60(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32118]) ).
cnf(p41151,plain,
( ssItem(sk53(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p41147,p33646]) ).
cnf(p41160,plain,
( ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49
| ssItem(sk53(sk51,sk52)) ),
inference(factoring,[status(thm)],[p41151]) ).
cnf(p41162,plain,
( ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil != sk49
| ssItem(sk53(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(superposition,[status(thm)],[p33684,p41160]) ).
cnf(p41168,plain,
( ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil != sk49
| ssItem(sk53(sk51,sk52)) ),
inference(factoring,[status(thm)],[p41162]) ).
cnf(p41169,plain,
( ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p41168,p27146]) ).
cnf(c216,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(X14,X15),sk57(X14,X15))
| ssItem(sk53(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p4553,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,X0),sk57(sk51,X0))
| ssItem(sk53(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c216,c196]) ).
cnf(p4644,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p4553,c197]) ).
cnf(p4657,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p4644]) ).
cnf(p4658,plain,
( nil != sk48
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p4657,p312]) ).
cnf(p32131,plain,
( nil != nil
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p4658]) ).
cnf(p33667,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32131]) ).
cnf(p41170,plain,
( ssItem(sk53(sk51,sk52))
| ssItem(sk53(sk51,sk52)) ),
inference(resolution,[status(thm)],[p41169,p33667]) ).
cnf(p41175,plain,
ssItem(sk53(sk51,sk52)),
inference(factoring,[status(thm)],[p41170]) ).
cnf(p41176,plain,
( ~ lt(sk53(sk51,sk52),X1)
| app(cons(X1,nil),X2) != sk49
| ~ ssList(X2)
| ~ ssItem(X1)
| app(X0,cons(sk53(sk51,sk52),nil)) != sk51
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p41175,c200]) ).
cnf(c218,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(X14,X15))
| ssList(sk54(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p896,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,X0))
| ssList(sk54(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c218,c196]) ).
cnf(p942,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| ssList(sk54(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p896,c197]) ).
cnf(p946,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p942]) ).
cnf(p947,plain,
( nil != sk48
| ssItem(sk57(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(resolution,[status(thm)],[p946,p312]) ).
cnf(p32119,plain,
( nil != nil
| ssItem(sk57(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p947]) ).
cnf(p33647,plain,
( ssItem(sk57(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32119]) ).
cnf(p41213,plain,
( ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) != sk51 ),
inference(resolution,[status(thm)],[p41176,p33647]) ).
cnf(c232,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(X14,X15))
| app(sk54(X14,X15),cons(sk53(X14,X15),nil)) = X14
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p7433,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,X0))
| app(sk54(sk51,X0),cons(sk53(sk51,X0),nil)) = sk51
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c232,c196]) ).
cnf(p8095,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p7433,c197]) ).
cnf(p8108,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p8095]) ).
cnf(p8109,plain,
( nil != sk48
| ssItem(sk57(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(resolution,[status(thm)],[p8108,p312]) ).
cnf(p32143,plain,
( nil != nil
| ssItem(sk57(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(demodulation,[status(thm)],[p32112,p8109]) ).
cnf(p33679,plain,
( ssItem(sk57(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p32143]) ).
cnf(p41256,plain,
( ssItem(sk57(sk51,sk52))
| ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[p41213,p33679]) ).
cnf(p41261,plain,
( ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(factoring,[status(thm)],[p41256]) ).
cnf(p42059,plain,
( ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p42052,p41261]) ).
cnf(c260,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(X14,X15))
| ssList(sk56(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p2986,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,X0))
| ssList(sk56(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c260,c196]) ).
cnf(p3062,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| ssList(sk56(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p2986,c197]) ).
cnf(p3072,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p3062]) ).
cnf(p3073,plain,
( nil != sk48
| ssItem(sk57(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(resolution,[status(thm)],[p3072,p312]) ).
cnf(p32127,plain,
( nil != nil
| ssItem(sk57(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p3073]) ).
cnf(p33663,plain,
( ssItem(sk57(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32127]) ).
cnf(p42066,plain,
( ssItem(sk57(sk51,sk52))
| ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49 ),
inference(resolution,[status(thm)],[p42059,p33663]) ).
cnf(p42106,plain,
( ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49 ),
inference(factoring,[status(thm)],[p42066]) ).
cnf(p42108,plain,
( ssItem(sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil != sk49
| ssItem(sk57(sk51,sk52)) ),
inference(superposition,[status(thm)],[p33688,p42106]) ).
cnf(p42114,plain,
( ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil != sk49
| ssItem(sk57(sk51,sk52)) ),
inference(factoring,[status(thm)],[p42108]) ).
cnf(p42115,plain,
( ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ssItem(sk57(sk51,sk52)) ),
inference(resolution,[status(thm)],[p42114,p27146]) ).
cnf(c288,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(X14,X15))
| lt(sk53(X14,X15),sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p5577,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,X0))
| lt(sk53(sk51,X0),sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c288,c196]) ).
cnf(p5668,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p5577,c197]) ).
cnf(p5681,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk57(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p5668]) ).
cnf(p5682,plain,
( nil != sk48
| ssItem(sk57(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p5681,p312]) ).
cnf(p32135,plain,
( nil != nil
| ssItem(sk57(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p5682]) ).
cnf(p33671,plain,
( ssItem(sk57(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32135]) ).
cnf(p42116,plain,
( ssItem(sk57(sk51,sk52))
| ssItem(sk57(sk51,sk52)) ),
inference(resolution,[status(thm)],[p42115,p33671]) ).
cnf(p42120,plain,
ssItem(sk57(sk51,sk52)),
inference(factoring,[status(thm)],[p42116]) ).
cnf(p42123,plain,
( ~ lt(X1,sk57(sk51,sk52))
| app(X2,cons(X1,nil)) != sk49
| ~ ssList(X2)
| ~ ssItem(X1)
| app(cons(sk57(sk51,sk52),nil),X0) != sk52
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p42120,c201]) ).
cnf(c262,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(X14,X15))
| ssList(sk56(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p3389,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,X0))
| ssList(sk56(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c262,c196]) ).
cnf(p3470,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| ssList(sk56(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p3389,c197]) ).
cnf(p3481,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p3470]) ).
cnf(p3482,plain,
( nil != sk48
| ssList(sk58(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(resolution,[status(thm)],[p3481,p312]) ).
cnf(p32128,plain,
( nil != nil
| ssList(sk58(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p3482]) ).
cnf(p33664,plain,
( ssList(sk58(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32128]) ).
cnf(p42565,plain,
( ssList(sk56(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52 ),
inference(resolution,[status(thm)],[p42123,p33664]) ).
cnf(c264,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(X14,X15),nil),sk58(X14,X15)) = X15
| ssList(sk56(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p9417,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,X0),nil),sk58(sk51,X0)) = X0
| ssList(sk56(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c264,c196]) ).
cnf(p9508,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssList(sk56(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p9417,c197]) ).
cnf(p9521,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p9508]) ).
cnf(p9522,plain,
( nil != sk48
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssList(sk56(sk51,sk52)) ),
inference(resolution,[status(thm)],[p9521,p312]) ).
cnf(p32147,plain,
( nil != nil
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssList(sk56(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p9522]) ).
cnf(p33683,plain,
( app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32147]) ).
cnf(p43360,plain,
( ssList(sk56(sk51,sk52))
| ssList(sk56(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[p42565,p33683]) ).
cnf(p43364,plain,
( ssList(sk56(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(factoring,[status(thm)],[p43360]) ).
cnf(c280,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(X14,X15))
| app(cons(sk55(X14,X15),nil),sk56(X14,X15)) = sk47
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p10441,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,X0))
| app(cons(sk55(sk51,X0),nil),sk56(sk51,X0)) = sk47
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c280,c196]) ).
cnf(p10532,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p10441,c197]) ).
cnf(p10545,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(equality_resolution,[status(thm)],[p10532]) ).
cnf(p10546,plain,
( nil != sk48
| ssItem(sk59(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(resolution,[status(thm)],[p10545,p312]) ).
cnf(p31730,plain,
( nil != sk48
| ssItem(sk59(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(demodulation,[status(thm)],[p30040,p10546]) ).
cnf(p33362,plain,
( nil != nil
| ssItem(sk59(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(demodulation,[status(thm)],[p32112,p31730]) ).
cnf(p33690,plain,
( ssItem(sk59(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(equality_resolution,[status(thm)],[p33362]) ).
cnf(c224,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(X14,X15))
| ssList(sk54(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p1338,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,X0))
| ssList(sk54(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c224,c196]) ).
cnf(p1394,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| ssList(sk54(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p1338,c197]) ).
cnf(p1400,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p1394]) ).
cnf(p1401,plain,
( nil != sk48
| ssItem(sk59(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(resolution,[status(thm)],[p1400,p312]) ).
cnf(p32121,plain,
( nil != nil
| ssItem(sk59(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p1401]) ).
cnf(p33649,plain,
( ssItem(sk59(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32121]) ).
cnf(p41215,plain,
( ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) != sk51 ),
inference(resolution,[status(thm)],[p41176,p33649]) ).
cnf(c238,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(X14,X15))
| app(sk54(X14,X15),cons(sk53(X14,X15),nil)) = X14
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p8390,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,X0))
| app(sk54(sk51,X0),cons(sk53(sk51,X0),nil)) = sk51
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c238,c196]) ).
cnf(p8481,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p8390,c197]) ).
cnf(p8494,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p8481]) ).
cnf(p8495,plain,
( nil != sk48
| ssItem(sk59(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(resolution,[status(thm)],[p8494,p312]) ).
cnf(p32144,plain,
( nil != nil
| ssItem(sk59(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(demodulation,[status(thm)],[p32112,p8495]) ).
cnf(p33680,plain,
( ssItem(sk59(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p32144]) ).
cnf(p41276,plain,
( ssItem(sk59(sk51,sk52))
| ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[p41215,p33680]) ).
cnf(p41280,plain,
( ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(factoring,[status(thm)],[p41276]) ).
cnf(p42060,plain,
( ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p42052,p41280]) ).
cnf(c266,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(X14,X15))
| ssList(sk56(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p3820,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,X0))
| ssList(sk56(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c266,c196]) ).
cnf(p3906,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| ssList(sk56(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p3820,c197]) ).
cnf(p3918,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p3906]) ).
cnf(p3919,plain,
( nil != sk48
| ssItem(sk59(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(resolution,[status(thm)],[p3918,p312]) ).
cnf(p32129,plain,
( nil != nil
| ssItem(sk59(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p3919]) ).
cnf(p33665,plain,
( ssItem(sk59(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32129]) ).
cnf(p42076,plain,
( ssItem(sk59(sk51,sk52))
| ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49 ),
inference(resolution,[status(thm)],[p42060,p33665]) ).
cnf(p42137,plain,
( ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49 ),
inference(factoring,[status(thm)],[p42076]) ).
cnf(p42140,plain,
( ssItem(sk59(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil != sk49
| ssItem(sk59(sk51,sk52)) ),
inference(superposition,[status(thm)],[p33690,p42137]) ).
cnf(p42495,plain,
( ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil != sk49
| ssItem(sk59(sk51,sk52)) ),
inference(factoring,[status(thm)],[p42140]) ).
cnf(p42496,plain,
( ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ssItem(sk59(sk51,sk52)) ),
inference(resolution,[status(thm)],[p42495,p27146]) ).
cnf(c294,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(X14,X15))
| lt(sk53(X14,X15),sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p6089,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,X0))
| lt(sk53(sk51,X0),sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c294,c196]) ).
cnf(p6180,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p6089,c197]) ).
cnf(p6193,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssItem(sk59(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p6180]) ).
cnf(p6194,plain,
( nil != sk48
| ssItem(sk59(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p6193,p312]) ).
cnf(p32137,plain,
( nil != nil
| ssItem(sk59(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p6194]) ).
cnf(p33673,plain,
( ssItem(sk59(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32137]) ).
cnf(p42497,plain,
( ssItem(sk59(sk51,sk52))
| ssItem(sk59(sk51,sk52)) ),
inference(resolution,[status(thm)],[p42496,p33673]) ).
cnf(p42499,plain,
ssItem(sk59(sk51,sk52)),
inference(factoring,[status(thm)],[p42497]) ).
cnf(p43368,plain,
( ssList(sk56(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p43364,p42499]) ).
cnf(c268,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(X14,X15))
| ssList(sk56(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p4279,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,X0))
| ssList(sk56(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c268,c196]) ).
cnf(p4370,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| ssList(sk56(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p4279,c197]) ).
cnf(p4383,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p4370]) ).
cnf(p4384,plain,
( nil != sk48
| ssList(sk60(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(resolution,[status(thm)],[p4383,p312]) ).
cnf(p32130,plain,
( nil != nil
| ssList(sk60(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p4384]) ).
cnf(p33666,plain,
( ssList(sk60(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32130]) ).
cnf(p43405,plain,
( ssList(sk56(sk51,sk52))
| ssList(sk56(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49 ),
inference(resolution,[status(thm)],[p43368,p33666]) ).
cnf(p43419,plain,
( ssList(sk56(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49 ),
inference(factoring,[status(thm)],[p43405]) ).
cnf(p43421,plain,
( ssList(sk56(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil != sk49
| ssList(sk56(sk51,sk52)) ),
inference(superposition,[status(thm)],[p33687,p43419]) ).
cnf(p43424,plain,
( ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil != sk49
| ssList(sk56(sk51,sk52)) ),
inference(factoring,[status(thm)],[p43421]) ).
cnf(p43425,plain,
( ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(resolution,[status(thm)],[p43424,p27146]) ).
cnf(c272,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(X14,X15),sk57(X14,X15))
| ssList(sk56(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p5321,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,X0),sk57(sk51,X0))
| ssList(sk56(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c272,c196]) ).
cnf(p5412,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk56(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p5321,c197]) ).
cnf(p5425,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p5412]) ).
cnf(p5426,plain,
( nil != sk48
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(resolution,[status(thm)],[p5425,p312]) ).
cnf(p32134,plain,
( nil != nil
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p5426]) ).
cnf(p33670,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32134]) ).
cnf(p43426,plain,
( ssList(sk56(sk51,sk52))
| ssList(sk56(sk51,sk52)) ),
inference(resolution,[status(thm)],[p43425,p33670]) ).
cnf(p43428,plain,
ssList(sk56(sk51,sk52)),
inference(factoring,[status(thm)],[p43426]) ).
cnf(c228,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(X14,X15),cons(sk59(X14,X15),nil)) = sk47
| ssList(sk54(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p7397,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,X0),cons(sk59(sk51,X0),nil)) = sk47
| ssList(sk54(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c228,c196]) ).
cnf(p7875,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssList(sk54(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p7397,c197]) ).
cnf(p7888,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p7875]) ).
cnf(p7889,plain,
( nil != sk48
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| ssList(sk54(sk51,sk52)) ),
inference(resolution,[status(thm)],[p7888,p312]) ).
cnf(p31313,plain,
( nil != sk48
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| ssList(sk54(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p30040,p7889]) ).
cnf(p33065,plain,
( nil != nil
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| ssList(sk54(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p31313]) ).
cnf(p33685,plain,
( app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p33065]) ).
cnf(c220,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(X14,X15))
| ssList(sk54(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p1103,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,X0))
| ssList(sk54(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c220,c196]) ).
cnf(p1154,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| ssList(sk54(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p1103,c197]) ).
cnf(p1159,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p1154]) ).
cnf(p1160,plain,
( nil != sk48
| ssList(sk58(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(resolution,[status(thm)],[p1159,p312]) ).
cnf(p32120,plain,
( nil != nil
| ssList(sk58(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p1160]) ).
cnf(p33648,plain,
( ssList(sk58(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32120]) ).
cnf(p42563,plain,
( ssList(sk54(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52 ),
inference(resolution,[status(thm)],[p42123,p33648]) ).
cnf(c222,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(X14,X15),nil),sk58(X14,X15)) = X15
| ssList(sk54(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p7361,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,X0),nil),sk58(sk51,X0)) = X0
| ssList(sk54(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c222,c196]) ).
cnf(p7655,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssList(sk54(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p7361,c197]) ).
cnf(p7668,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p7655]) ).
cnf(p7669,plain,
( nil != sk48
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssList(sk54(sk51,sk52)) ),
inference(resolution,[status(thm)],[p7668,p312]) ).
cnf(p32142,plain,
( nil != nil
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssList(sk54(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p7669]) ).
cnf(p33678,plain,
( app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32142]) ).
cnf(p42620,plain,
( ssList(sk54(sk51,sk52))
| ssList(sk54(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[p42563,p33678]) ).
cnf(p42625,plain,
( ssList(sk54(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(factoring,[status(thm)],[p42620]) ).
cnf(p42629,plain,
( ssList(sk54(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p42625,p42499]) ).
cnf(c226,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(X14,X15))
| ssList(sk54(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p1601,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,X0))
| ssList(sk54(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c226,c196]) ).
cnf(p1662,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| ssList(sk54(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p1601,c197]) ).
cnf(p1669,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p1662]) ).
cnf(p1670,plain,
( nil != sk48
| ssList(sk60(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(resolution,[status(thm)],[p1669,p312]) ).
cnf(p32122,plain,
( nil != nil
| ssList(sk60(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p1670]) ).
cnf(p33650,plain,
( ssList(sk60(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32122]) ).
cnf(p42663,plain,
( ssList(sk54(sk51,sk52))
| ssList(sk54(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49 ),
inference(resolution,[status(thm)],[p42629,p33650]) ).
cnf(p42676,plain,
( ssList(sk54(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49 ),
inference(factoring,[status(thm)],[p42663]) ).
cnf(p42678,plain,
( ssList(sk54(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil != sk49
| ssList(sk54(sk51,sk52)) ),
inference(superposition,[status(thm)],[p33685,p42676]) ).
cnf(p42682,plain,
( ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil != sk49
| ssList(sk54(sk51,sk52)) ),
inference(factoring,[status(thm)],[p42678]) ).
cnf(p42683,plain,
( ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(resolution,[status(thm)],[p42682,p27146]) ).
cnf(c230,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(X14,X15),sk57(X14,X15))
| ssList(sk54(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p4809,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,X0),sk57(sk51,X0))
| ssList(sk54(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c230,c196]) ).
cnf(p4900,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk54(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p4809,c197]) ).
cnf(p4913,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p4900]) ).
cnf(p4914,plain,
( nil != sk48
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(resolution,[status(thm)],[p4913,p312]) ).
cnf(p32132,plain,
( nil != nil
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p4914]) ).
cnf(p33668,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32132]) ).
cnf(p42684,plain,
( ssList(sk54(sk51,sk52))
| ssList(sk54(sk51,sk52)) ),
inference(resolution,[status(thm)],[p42683,p33668]) ).
cnf(p42687,plain,
ssList(sk54(sk51,sk52)),
inference(factoring,[status(thm)],[p42684]) ).
cnf(p43028,plain,
( ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) != sk51 ),
inference(resolution,[status(thm)],[p42687,p41176]) ).
cnf(c234,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(X14,X15))
| app(sk54(X14,X15),cons(sk53(X14,X15),nil)) = X14
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p7469,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,X0))
| app(sk54(sk51,X0),cons(sk53(sk51,X0),nil)) = sk51
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c234,c196]) ).
cnf(p7551,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p7469,c197]) ).
cnf(p7564,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p7551]) ).
cnf(p7565,plain,
( nil != sk48
| ssList(sk58(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(resolution,[status(thm)],[p7564,p312]) ).
cnf(p32141,plain,
( nil != nil
| ssList(sk58(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(demodulation,[status(thm)],[p32112,p7565]) ).
cnf(p33677,plain,
( ssList(sk58(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p32141]) ).
cnf(p43189,plain,
( ssList(sk58(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[p43028,p33677]) ).
cnf(p43193,plain,
( ssList(sk58(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p43189,p42052]) ).
cnf(p43752,plain,
( ssList(sk58(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49 ),
inference(resolution,[status(thm)],[p43428,p43193]) ).
cnf(p43773,plain,
( ssList(sk58(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil != sk49
| ssList(sk58(sk51,sk52)) ),
inference(superposition,[status(thm)],[p33689,p43752]) ).
cnf(p43777,plain,
( ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil != sk49
| ssList(sk58(sk51,sk52)) ),
inference(factoring,[status(thm)],[p43773]) ).
cnf(p43778,plain,
( ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ssList(sk58(sk51,sk52)) ),
inference(resolution,[status(thm)],[p43777,p27146]) ).
cnf(c290,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(X14,X15))
| lt(sk53(X14,X15),sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p5833,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,X0))
| lt(sk53(sk51,X0),sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c290,c196]) ).
cnf(p5924,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p5833,c197]) ).
cnf(p5937,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk58(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p5924]) ).
cnf(p5938,plain,
( nil != sk48
| ssList(sk58(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p5937,p312]) ).
cnf(p32136,plain,
( nil != nil
| ssList(sk58(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p5938]) ).
cnf(p33672,plain,
( ssList(sk58(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32136]) ).
cnf(p43779,plain,
( ssList(sk58(sk51,sk52))
| ssList(sk58(sk51,sk52)) ),
inference(resolution,[status(thm)],[p43778,p33672]) ).
cnf(p43781,plain,
ssList(sk58(sk51,sk52)),
inference(factoring,[status(thm)],[p43779]) ).
cnf(p44085,plain,
( ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) != sk52 ),
inference(resolution,[status(thm)],[p43781,p42123]) ).
cnf(c278,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(X14,X15),nil),sk58(X14,X15)) = X15
| app(cons(sk55(X14,X15),nil),sk56(X14,X15)) = sk47
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p15601,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,X0),nil),sk58(sk51,X0)) = X0
| app(cons(sk55(sk51,X0),nil),sk56(sk51,X0)) = sk47
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c278,c196]) ).
cnf(p15692,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p15601,c197]) ).
cnf(p15705,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(equality_resolution,[status(thm)],[p15692]) ).
cnf(p15706,plain,
( nil != sk48
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(resolution,[status(thm)],[p15705,p312]) ).
cnf(p32063,plain,
( nil != sk48
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(demodulation,[status(thm)],[p30040,p15706]) ).
cnf(p33599,plain,
( nil != nil
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(demodulation,[status(thm)],[p32112,p32063]) ).
cnf(p35314,plain,
( app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(equality_resolution,[status(thm)],[p33599]) ).
cnf(p44907,plain,
( app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[p44085,p35314]) ).
cnf(p45000,plain,
( app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p44907,p42499]) ).
cnf(c282,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(X14,X15))
| app(cons(sk55(X14,X15),nil),sk56(X14,X15)) = sk47
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p10697,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,X0))
| app(cons(sk55(sk51,X0),nil),sk56(sk51,X0)) = sk47
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c282,c196]) ).
cnf(p10788,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p10697,c197]) ).
cnf(p10801,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(equality_resolution,[status(thm)],[p10788]) ).
cnf(p10802,plain,
( nil != sk48
| ssList(sk60(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(resolution,[status(thm)],[p10801,p312]) ).
cnf(p31772,plain,
( nil != sk48
| ssList(sk60(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(demodulation,[status(thm)],[p30040,p10802]) ).
cnf(p33392,plain,
( nil != nil
| ssList(sk60(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(demodulation,[status(thm)],[p32112,p31772]) ).
cnf(p33691,plain,
( ssList(sk60(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(equality_resolution,[status(thm)],[p33392]) ).
cnf(c240,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(X14,X15))
| app(sk54(X14,X15),cons(sk53(X14,X15),nil)) = X14
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p8646,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,X0))
| app(sk54(sk51,X0),cons(sk53(sk51,X0),nil)) = sk51
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c240,c196]) ).
cnf(p8737,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p8646,c197]) ).
cnf(p8750,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p8737]) ).
cnf(p8751,plain,
( nil != sk48
| ssList(sk60(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(resolution,[status(thm)],[p8750,p312]) ).
cnf(p32145,plain,
( nil != nil
| ssList(sk60(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(demodulation,[status(thm)],[p32112,p8751]) ).
cnf(p33681,plain,
( ssList(sk60(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p32145]) ).
cnf(p43190,plain,
( ssList(sk60(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[p43028,p33681]) ).
cnf(p43197,plain,
( ssList(sk60(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p43190,p42052]) ).
cnf(p43756,plain,
( ssList(sk60(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49 ),
inference(resolution,[status(thm)],[p43428,p43197]) ).
cnf(p44122,plain,
( ssList(sk60(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil != sk49
| ssList(sk60(sk51,sk52)) ),
inference(superposition,[status(thm)],[p33691,p43756]) ).
cnf(p44125,plain,
( ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil != sk49
| ssList(sk60(sk51,sk52)) ),
inference(factoring,[status(thm)],[p44122]) ).
cnf(p44126,plain,
( ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ssList(sk60(sk51,sk52)) ),
inference(resolution,[status(thm)],[p44125,p27146]) ).
cnf(c296,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(X14,X15))
| lt(sk53(X14,X15),sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p6345,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,X0))
| lt(sk53(sk51,X0),sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c296,c196]) ).
cnf(p6436,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p6345,c197]) ).
cnf(p6449,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| ssList(sk60(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p6436]) ).
cnf(p6450,plain,
( nil != sk48
| ssList(sk60(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p6449,p312]) ).
cnf(p32138,plain,
( nil != nil
| ssList(sk60(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p6450]) ).
cnf(p33674,plain,
( ssList(sk60(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32138]) ).
cnf(p44127,plain,
( ssList(sk60(sk51,sk52))
| ssList(sk60(sk51,sk52)) ),
inference(resolution,[status(thm)],[p44126,p33674]) ).
cnf(p44128,plain,
ssList(sk60(sk51,sk52)),
inference(factoring,[status(thm)],[p44127]) ).
cnf(p45187,plain,
( app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| nil != sk49 ),
inference(resolution,[status(thm)],[p45000,p44128]) ).
cnf(p45188,plain,
( app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52)) ),
inference(resolution,[status(thm)],[p45187,p27146]) ).
cnf(c292,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(X14,X15),nil),sk58(X14,X15)) = X15
| lt(sk53(X14,X15),sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p12721,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,X0),nil),sk58(sk51,X0)) = X0
| lt(sk53(sk51,X0),sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c292,c196]) ).
cnf(p12812,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p12721,c197]) ).
cnf(p12825,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p12812]) ).
cnf(p12826,plain,
( nil != sk48
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p12825,p312]) ).
cnf(p32149,plain,
( nil != nil
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p12826]) ).
cnf(p33693,plain,
( app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32149]) ).
cnf(p44905,plain,
( lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[p44085,p33693]) ).
cnf(p44911,plain,
( lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p44905,p42499]) ).
cnf(p44959,plain,
( lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49 ),
inference(resolution,[status(thm)],[p44911,p44128]) ).
cnf(p44967,plain,
( lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != nil ),
inference(superposition,[status(thm)],[p27146,p44959]) ).
cnf(c298,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(X14,X15),cons(sk59(X14,X15),nil)) = sk47
| lt(sk53(X14,X15),sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p12977,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,X0),cons(sk59(sk51,X0),nil)) = sk47
| lt(sk53(sk51,X0),sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c298,c196]) ).
cnf(p13068,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p12977,c197]) ).
cnf(p13081,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p13068]) ).
cnf(p13082,plain,
( nil != sk48
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p13081,p312]) ).
cnf(p31938,plain,
( nil != sk48
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p30040,p13082]) ).
cnf(p33510,plain,
( nil != nil
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p31938]) ).
cnf(p33695,plain,
( app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p33510]) ).
cnf(p44970,plain,
( lt(sk53(sk51,sk52),sk55(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52)) ),
inference(resolution,[status(thm)],[p44967,p33695]) ).
cnf(p44972,plain,
( lt(sk53(sk51,sk52),sk55(sk51,sk52))
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52)) ),
inference(factoring,[status(thm)],[p44970]) ).
cnf(c300,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(X14,X15),sk57(X14,X15))
| lt(sk53(X14,X15),sk55(X14,X15))
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p6601,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,X0),sk57(sk51,X0))
| lt(sk53(sk51,X0),sk55(sk51,X0))
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c300,c196]) ).
cnf(p6692,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52))
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p6601,c197]) ).
cnf(p6705,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p6692]) ).
cnf(p6706,plain,
( nil != sk48
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p6705,p312]) ).
cnf(p32139,plain,
( nil != nil
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(demodulation,[status(thm)],[p32112,p6706]) ).
cnf(p33675,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(equality_resolution,[status(thm)],[p32139]) ).
cnf(p44973,plain,
( lt(sk53(sk51,sk52),sk55(sk51,sk52))
| lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p44972,p33675]) ).
cnf(p44974,plain,
lt(sk53(sk51,sk52),sk55(sk51,sk52)),
inference(factoring,[status(thm)],[p44973]) ).
cnf(c244,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(X14,X15),sk57(X14,X15))
| app(sk54(X14,X15),cons(sk53(X14,X15),nil)) = X14
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p12209,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,X0),sk57(sk51,X0))
| app(sk54(sk51,X0),cons(sk53(sk51,X0),nil)) = sk51
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c244,c196]) ).
cnf(p12300,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p12209,c197]) ).
cnf(p12313,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p12300]) ).
cnf(p12314,plain,
( nil != sk48
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(resolution,[status(thm)],[p12313,p312]) ).
cnf(p32148,plain,
( nil != nil
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(demodulation,[status(thm)],[p32112,p12314]) ).
cnf(p33692,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p32148]) ).
cnf(p43191,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[p43028,p33692]) ).
cnf(p43265,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p43191,p42052]) ).
cnf(p43760,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49 ),
inference(resolution,[status(thm)],[p43428,p43265]) ).
cnf(p44512,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != nil ),
inference(superposition,[status(thm)],[p27146,p43760]) ).
cnf(c286,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(X14,X15),sk57(X14,X15))
| app(cons(sk55(X14,X15),nil),sk56(X14,X15)) = sk47
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p12465,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,X0),sk57(sk51,X0))
| app(cons(sk55(sk51,X0),nil),sk56(sk51,X0)) = sk47
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c286,c196]) ).
cnf(p12556,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p12465,c197]) ).
cnf(p12569,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(equality_resolution,[status(thm)],[p12556]) ).
cnf(p12570,plain,
( nil != sk48
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = sk47 ),
inference(resolution,[status(thm)],[p12569,p312]) ).
cnf(p31855,plain,
( nil != sk48
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(demodulation,[status(thm)],[p30040,p12570]) ).
cnf(p33451,plain,
( nil != nil
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(demodulation,[status(thm)],[p32112,p31855]) ).
cnf(p33694,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil ),
inference(equality_resolution,[status(thm)],[p33451]) ).
cnf(p44525,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(resolution,[status(thm)],[p44512,p33694]) ).
cnf(p44527,plain,
( lt(sk59(sk51,sk52),sk57(sk51,sk52))
| ~ lt(sk53(sk51,sk52),sk55(sk51,sk52)) ),
inference(factoring,[status(thm)],[p44525]) ).
cnf(p44975,plain,
lt(sk59(sk51,sk52),sk57(sk51,sk52)),
inference(resolution,[status(thm)],[p44974,p44527]) ).
cnf(p45189,plain,
app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) = nil,
inference(resolution,[status(thm)],[p45188,p44975]) ).
cnf(c236,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(X14,X15),nil),sk58(X14,X15)) = X15
| app(sk54(X14,X15),cons(sk53(X14,X15),nil)) = X14
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p15089,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,X0),nil),sk58(sk51,X0)) = X0
| app(sk54(sk51,X0),cons(sk53(sk51,X0),nil)) = sk51
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c236,c196]) ).
cnf(p15180,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p15089,c197]) ).
cnf(p15193,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p15180]) ).
cnf(p15194,plain,
( nil != sk48
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(resolution,[status(thm)],[p15193,p312]) ).
cnf(p32150,plain,
( nil != nil
| app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(demodulation,[status(thm)],[p32112,p15194]) ).
cnf(p34080,plain,
( app(cons(sk57(sk51,sk52),nil),sk58(sk51,sk52)) = sk52
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p32150]) ).
cnf(p44906,plain,
( app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| ~ lt(X0,sk57(sk51,sk52))
| app(X1,cons(X0,nil)) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[p44085,p34080]) ).
cnf(p44996,plain,
( app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(X0,cons(sk59(sk51,sk52),nil)) != sk49
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p44906,p42499]) ).
cnf(p45048,plain,
( app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != sk49 ),
inference(resolution,[status(thm)],[p44996,p44128]) ).
cnf(p45056,plain,
( app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52))
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) != nil ),
inference(superposition,[status(thm)],[p27146,p45048]) ).
cnf(c242,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(X14,X15),cons(sk59(X14,X15),nil)) = sk47
| app(sk54(X14,X15),cons(sk53(X14,X15),nil)) = X14
| app(app(X14,sk47),X15) != sk48
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p15345,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,X0),cons(sk59(sk51,X0),nil)) = sk47
| app(sk54(sk51,X0),cons(sk53(sk51,X0),nil)) = sk51
| app(app(sk51,sk47),X0) != sk48
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[c242,c196]) ).
cnf(p15436,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| sk48 != sk48 ),
inference(resolution,[status(thm)],[p15345,c197]) ).
cnf(p15449,plain,
( nil != sk48
| ~ strictorderedP(sk47)
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p15436]) ).
cnf(p15450,plain,
( nil != sk48
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = sk47
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(resolution,[status(thm)],[p15449,p312]) ).
cnf(p32021,plain,
( nil != sk48
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(demodulation,[status(thm)],[p30040,p15450]) ).
cnf(p33569,plain,
( nil != nil
| app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(demodulation,[status(thm)],[p32112,p32021]) ).
cnf(p35313,plain,
( app(sk60(sk51,sk52),cons(sk59(sk51,sk52),nil)) = nil
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51 ),
inference(equality_resolution,[status(thm)],[p33569]) ).
cnf(p45058,plain,
( app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52)) ),
inference(resolution,[status(thm)],[p45056,p35313]) ).
cnf(p45059,plain,
( app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51
| ~ lt(sk59(sk51,sk52),sk57(sk51,sk52)) ),
inference(factoring,[status(thm)],[p45058]) ).
cnf(p45060,plain,
app(sk54(sk51,sk52),cons(sk53(sk51,sk52),nil)) = sk51,
inference(resolution,[status(thm)],[p45059,p44975]) ).
cnf(p45062,plain,
( ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0)
| sk51 != sk51 ),
inference(demodulation,[status(thm)],[p45060,p43028]) ).
cnf(p45072,plain,
( ~ lt(sk53(sk51,sk52),X0)
| app(cons(X0,nil),X1) != sk49
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(equality_resolution,[status(thm)],[p45062]) ).
cnf(p45074,plain,
( ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),X0) != sk49
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[p45072,p42052]) ).
cnf(p45094,plain,
( ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| app(cons(sk55(sk51,sk52),nil),sk56(sk51,sk52)) != sk49 ),
inference(resolution,[status(thm)],[p45074,p43428]) ).
cnf(p45192,plain,
( ~ lt(sk53(sk51,sk52),sk55(sk51,sk52))
| nil != sk49 ),
inference(demodulation,[status(thm)],[p45189,p45094]) ).
cnf(p45194,plain,
~ lt(sk53(sk51,sk52),sk55(sk51,sk52)),
inference(resolution,[status(thm)],[p45192,p27146]) ).
cnf(p45195,plain,
$false,
inference(resolution,[status(thm)],[p45194,p44974]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC344+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n002.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.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 17:47:19 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 231.88/35.18 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 231.88/35.18 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------