%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC344+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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 : Tue Sep 29 01:05:38 PM UTC 2026
% Result : Theorem 4.39s 0.91s
% Output : Refutation 4.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 50
% Syntax : Number of formulae : 588 ( 56 unt; 49 def)
% Number of atoms : 2638 ( 523 equ)
% Maximal formula atoms : 46 ( 4 avg)
% Number of connectives : 3524 (1474 ~;1883 |; 90 &)
% ( 49 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 56 ( 54 usr; 50 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-3 aty)
% Number of variables : 468 ( 0 sgn 420 !; 48 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f96,conjecture,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ( X1 != X3
| X0 != X2
| ! [X4] :
( ssList(X4)
=> ! [X5] :
( ssList(X5)
=> ( app(app(X4,X2),X5) != X3
| ~ strictorderedP(X2)
| ? [X6] :
( ssItem(X6)
& ? [X7] :
( ssList(X7)
& app(X7,cons(X6,nil)) = X4
& ? [X8] :
( ssItem(X8)
& ? [X9] :
( ssList(X9)
& app(cons(X8,nil),X9) = X2
& lt(X6,X8) ) ) ) )
| ? [X10] :
( ssItem(X10)
& ? [X11] :
( ssList(X11)
& app(cons(X10,nil),X11) = X5
& ? [X12] :
( ssItem(X12)
& ? [X13] :
( ssList(X13)
& app(X13,cons(X12,nil)) = X2
& lt(X12,X10) ) ) ) ) ) ) )
| ( nil != X3
& nil = X2 )
| ( ? [X14] :
( ssList(X14)
& ? [X15] :
( ssList(X15)
& app(app(X14,X0),X15) = X1
& ! [X16] :
( ssItem(X16)
=> ! [X17] :
( ssList(X17)
=> ( app(X17,cons(X16,nil)) != X14
| ! [X18] :
( ssItem(X18)
=> ! [X19] :
( ssList(X19)
=> ( app(cons(X18,nil),X19) != X0
| ~ lt(X16,X18) ) ) ) ) ) )
& ! [X20] :
( ssItem(X20)
=> ! [X21] :
( ssList(X21)
=> ( app(cons(X20,nil),X21) != X15
| ! [X22] :
( ssItem(X22)
=> ! [X23] :
( ssList(X23)
=> ( app(X23,cons(X22,nil)) != X0
| ~ lt(X22,X20) ) ) ) ) ) )
& strictorderedP(X0) ) )
& ( nil != X0
| nil = X1 ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f97,negated_conjecture,
~ ! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ( X1 != X3
| X0 != X2
| ! [X4] :
( ssList(X4)
=> ! [X5] :
( ssList(X5)
=> ( app(app(X4,X2),X5) != X3
| ~ strictorderedP(X2)
| ? [X6] :
( ssItem(X6)
& ? [X7] :
( ssList(X7)
& app(X7,cons(X6,nil)) = X4
& ? [X8] :
( ssItem(X8)
& ? [X9] :
( ssList(X9)
& app(cons(X8,nil),X9) = X2
& lt(X6,X8) ) ) ) )
| ? [X10] :
( ssItem(X10)
& ? [X11] :
( ssList(X11)
& app(cons(X10,nil),X11) = X5
& ? [X12] :
( ssItem(X12)
& ? [X13] :
( ssList(X13)
& app(X13,cons(X12,nil)) = X2
& lt(X12,X10) ) ) ) ) ) ) )
| ( nil != X3
& nil = X2 )
| ( ? [X14] :
( ssList(X14)
& ? [X15] :
( ssList(X15)
& app(app(X14,X0),X15) = X1
& ! [X16] :
( ssItem(X16)
=> ! [X17] :
( ssList(X17)
=> ( app(X17,cons(X16,nil)) != X14
| ! [X18] :
( ssItem(X18)
=> ! [X19] :
( ssList(X19)
=> ( app(cons(X18,nil),X19) != X0
| ~ lt(X16,X18) ) ) ) ) ) )
& ! [X20] :
( ssItem(X20)
=> ! [X21] :
( ssList(X21)
=> ( app(cons(X20,nil),X21) != X15
| ! [X22] :
( ssItem(X22)
=> ! [X23] :
( ssList(X23)
=> ( app(X23,cons(X22,nil)) != X0
| ~ lt(X22,X20) ) ) ) ) ) )
& strictorderedP(X0) ) )
& ( nil != X0
| nil = X1 ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f221,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( X1 = X3
& X0 = X2
& ? [X4] :
( ? [X5] :
( app(app(X4,X2),X5) = X3
& strictorderedP(X2)
& ! [X6] :
( ~ ssItem(X6)
| ! [X7] :
( ~ ssList(X7)
| app(X7,cons(X6,nil)) != X4
| ! [X8] :
( ~ ssItem(X8)
| ! [X9] :
( ~ ssList(X9)
| app(cons(X8,nil),X9) != X2
| ~ lt(X6,X8) ) ) ) )
& ! [X10] :
( ~ ssItem(X10)
| ! [X11] :
( ~ ssList(X11)
| app(cons(X10,nil),X11) != X5
| ! [X12] :
( ~ ssItem(X12)
| ! [X13] :
( ~ ssList(X13)
| app(X13,cons(X12,nil)) != X2
| ~ lt(X12,X10) ) ) ) )
& ssList(X5) )
& ssList(X4) )
& ( nil = X3
| nil != X2 )
& ( ! [X14] :
( ~ ssList(X14)
| ! [X15] :
( ~ ssList(X15)
| app(app(X14,X0),X15) != X1
| ? [X16] :
( ? [X17] :
( app(X17,cons(X16,nil)) = X14
& ? [X18] :
( ? [X19] :
( app(cons(X18,nil),X19) = X0
& lt(X16,X18)
& ssList(X19) )
& ssItem(X18) )
& ssList(X17) )
& ssItem(X16) )
| ? [X20] :
( ? [X21] :
( app(cons(X20,nil),X21) = X15
& ? [X22] :
( ? [X23] :
( app(X23,cons(X22,nil)) = X0
& lt(X22,X20)
& ssList(X23) )
& ssItem(X22) )
& ssList(X21) )
& ssItem(X20) )
| ~ strictorderedP(X0) ) )
| ( nil = X0
& nil != X1 ) )
& ssList(X3) )
& ssList(X2) )
& ssList(X1) )
& ssList(X0) ),
inference(ennf_transformation,[],[f97]) ).
fof(f222,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( X1 = X3
& X0 = X2
& ? [X4] :
( ? [X5] :
( app(app(X4,X2),X5) = X3
& strictorderedP(X2)
& ! [X6] :
( ~ ssItem(X6)
| ! [X7] :
( ~ ssList(X7)
| app(X7,cons(X6,nil)) != X4
| ! [X8] :
( ~ ssItem(X8)
| ! [X9] :
( ~ ssList(X9)
| app(cons(X8,nil),X9) != X2
| ~ lt(X6,X8) ) ) ) )
& ! [X10] :
( ~ ssItem(X10)
| ! [X11] :
( ~ ssList(X11)
| app(cons(X10,nil),X11) != X5
| ! [X12] :
( ~ ssItem(X12)
| ! [X13] :
( ~ ssList(X13)
| app(X13,cons(X12,nil)) != X2
| ~ lt(X12,X10) ) ) ) )
& ssList(X5) )
& ssList(X4) )
& ( nil = X3
| nil != X2 )
& ( ! [X14] :
( ~ ssList(X14)
| ! [X15] :
( ~ ssList(X15)
| app(app(X14,X0),X15) != X1
| ? [X16] :
( ? [X17] :
( app(X17,cons(X16,nil)) = X14
& ? [X18] :
( ? [X19] :
( app(cons(X18,nil),X19) = X0
& lt(X16,X18)
& ssList(X19) )
& ssItem(X18) )
& ssList(X17) )
& ssItem(X16) )
| ? [X20] :
( ? [X21] :
( app(cons(X20,nil),X21) = X15
& ? [X22] :
( ? [X23] :
( app(X23,cons(X22,nil)) = X0
& lt(X22,X20)
& ssList(X23) )
& ssItem(X22) )
& ssList(X21) )
& ssItem(X20) )
| ~ strictorderedP(X0) ) )
| ( nil = X0
& nil != X1 ) )
& ssList(X3) )
& ssList(X2) )
& ssList(X1) )
& ssList(X0) ),
inference(flattening,[],[f221]) ).
fof(f411,plain,
! [X0,X18,X16] :
( ssList(sK61(X0,X16,X18))
| ~ sP59(X18,X16,X0) ),
inference(cnf_transformation,[],[f222]) ).
fof(f412,plain,
! [X0,X18,X16] :
( ~ sP59(X18,X16,X0)
| lt(X16,X18) ),
inference(cnf_transformation,[],[f222]) ).
fof(f413,plain,
! [X0,X18,X16] :
( ~ sP59(X18,X16,X0)
| app(cons(X18,nil),sK61(X0,X16,X18)) = X0 ),
inference(cnf_transformation,[],[f222]) ).
fof(f414,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| ssList(sK60(X15))
| ssList(sK56(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f415,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| lt(sK57(X15),sK53(X15))
| ssList(sK56(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f416,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| sK47 = app(sK60(X15),cons(sK57(X15),nil))
| ssList(sK56(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f417,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| ssList(sK60(X15))
| sP59(sK58(X14),sK54(X14),sK47)
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f418,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| lt(sK57(X15),sK53(X15))
| sP59(sK58(X14),sK54(X14),sK47)
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f419,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| sK47 = app(sK60(X15),cons(sK57(X15),nil))
| sP59(sK58(X14),sK54(X14),sK47)
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f420,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| ssList(sK60(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f421,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| lt(sK57(X15),sK53(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f422,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| sK47 = app(sK60(X15),cons(sK57(X15),nil))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f423,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| ssList(sK60(X15))
| ssList(sK56(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f424,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| lt(sK57(X15),sK53(X15))
| ssList(sK56(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f425,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| sK47 = app(sK60(X15),cons(sK57(X15),nil))
| ssList(sK56(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f426,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| ssList(sK60(X15))
| sP59(sK58(X14),sK54(X14),sK47)
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f427,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| lt(sK57(X15),sK53(X15))
| sP59(sK58(X14),sK54(X14),sK47)
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f428,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| sK47 = app(sK60(X15),cons(sK57(X15),nil))
| sP59(sK58(X14),sK54(X14),sK47)
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f429,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| ssList(sK60(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f430,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| lt(sK57(X15),sK53(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f431,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| sK47 = app(sK60(X15),cons(sK57(X15),nil))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f432,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| ssList(sK60(X15))
| ssItem(sK54(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f433,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| lt(sK57(X15),sK53(X15))
| ssItem(sK54(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f434,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| sK47 = app(sK60(X15),cons(sK57(X15),nil))
| ssItem(sK54(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f435,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| ssList(sK60(X15))
| ssItem(sK54(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f436,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| lt(sK57(X15),sK53(X15))
| ssItem(sK54(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f437,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| sK47 = app(sK60(X15),cons(sK57(X15),nil))
| ssItem(sK54(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f438,plain,
! [X8,X6,X9,X7] :
( app(cons(X8,nil),X9) != sK49
| ~ lt(X6,X8)
| ~ ssList(X9)
| ~ ssItem(X8)
| app(X7,cons(X6,nil)) != sK51
| ~ ssList(X7)
| ~ ssItem(X6) ),
inference(cnf_transformation,[],[f222]) ).
fof(f439,plain,
! [X10,X11,X12,X13] :
( app(cons(X10,nil),X11) != sK52
| app(X13,cons(X12,nil)) != sK49
| ~ ssList(X13)
| ~ ssItem(X12)
| ~ lt(X12,X10)
| ~ ssList(X11)
| ~ ssItem(X10) ),
inference(cnf_transformation,[],[f222]) ).
fof(f440,plain,
! [X0,X18,X16] :
( ~ sP59(X18,X16,X0)
| ssItem(X18) ),
inference(cnf_transformation,[],[f222]) ).
fof(f441,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| ssItem(sK57(X15))
| ssItem(sK54(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f442,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| ssItem(sK57(X15))
| ssItem(sK54(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f443,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| ssItem(sK57(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f444,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| ssItem(sK57(X15))
| sP59(sK58(X14),sK54(X14),sK47)
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f445,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| ssItem(sK57(X15))
| ssList(sK56(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f446,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| ssItem(sK57(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f447,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| ssItem(sK57(X15))
| sP59(sK58(X14),sK54(X14),sK47)
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f448,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| ssItem(sK57(X15))
| ssList(sK56(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f449,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| ssItem(sK53(X15))
| ssList(sK56(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f450,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| ssItem(sK53(X15))
| sP59(sK58(X14),sK54(X14),sK47)
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f451,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| ssItem(sK53(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f452,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| ssItem(sK53(X15))
| ssList(sK56(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f453,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| ssItem(sK53(X15))
| sP59(sK58(X14),sK54(X14),sK47)
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f454,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| ssItem(sK53(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f455,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| app(cons(sK53(X15),nil),sK55(X15)) = X15
| ssList(sK56(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f456,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| app(cons(sK53(X15),nil),sK55(X15)) = X15
| sP59(sK58(X14),sK54(X14),sK47)
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f457,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| app(cons(sK53(X15),nil),sK55(X15)) = X15
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f458,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| ssList(sK55(X15))
| ssList(sK56(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f459,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| ssList(sK55(X15))
| sP59(sK58(X14),sK54(X14),sK47)
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f460,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| ssList(sK55(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f461,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| app(cons(sK53(X15),nil),sK55(X15)) = X15
| ssList(sK56(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f462,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| app(cons(sK53(X15),nil),sK55(X15)) = X15
| sP59(sK58(X14),sK54(X14),sK47)
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f463,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| app(cons(sK53(X15),nil),sK55(X15)) = X15
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f464,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| ssList(sK55(X15))
| ssList(sK56(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f465,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| ssList(sK55(X15))
| sP59(sK58(X14),sK54(X14),sK47)
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f466,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| ssList(sK55(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f467,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| ssList(sK55(X15))
| ssItem(sK54(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f468,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| app(cons(sK53(X15),nil),sK55(X15)) = X15
| ssItem(sK54(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f469,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| ssList(sK55(X15))
| ssItem(sK54(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f470,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| app(cons(sK53(X15),nil),sK55(X15)) = X15
| ssItem(sK54(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f471,plain,
! [X14,X15] :
( nil != sK48
| ~ strictorderedP(sK47)
| ssItem(sK53(X15))
| ssItem(sK54(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f472,plain,
! [X14,X15] :
( nil = sK47
| ~ strictorderedP(sK47)
| ssItem(sK53(X15))
| ssItem(sK54(X14))
| sK48 != app(app(X14,sK47),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(cnf_transformation,[],[f222]) ).
fof(f473,plain,
ssList(sK52),
inference(cnf_transformation,[],[f222]) ).
fof(f474,plain,
strictorderedP(sK49),
inference(cnf_transformation,[],[f222]) ).
fof(f475,plain,
sK50 = app(app(sK51,sK49),sK52),
inference(cnf_transformation,[],[f222]) ).
fof(f476,plain,
ssList(sK51),
inference(cnf_transformation,[],[f222]) ).
fof(f477,plain,
( nil != sK49
| nil = sK50 ),
inference(cnf_transformation,[],[f222]) ).
fof(f479,plain,
sK47 = sK49,
inference(cnf_transformation,[],[f222]) ).
fof(f480,plain,
sK48 = sK50,
inference(cnf_transformation,[],[f222]) ).
fof(f486,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| ssItem(sK53(X15))
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f472,f479,f479,f480,f479]) ).
fof(f487,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| ssItem(sK53(X15))
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f471,f480,f479,f480,f479]) ).
fof(f488,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| app(cons(sK53(X15),nil),sK55(X15)) = X15
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f470,f480,f479,f480,f479]) ).
fof(f489,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| ssList(sK55(X15))
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f469,f480,f479,f480,f479]) ).
fof(f490,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| app(cons(sK53(X15),nil),sK55(X15)) = X15
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f468,f479,f479,f480,f479]) ).
fof(f491,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| ssList(sK55(X15))
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f467,f479,f479,f480,f479]) ).
fof(f492,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| ssList(sK55(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f466,f479,f479,f480,f479]) ).
fof(f493,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| ssList(sK55(X15))
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f465,f479,f479,f479,f480,f479]) ).
fof(f494,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| ssList(sK55(X15))
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f464,f479,f479,f480,f479]) ).
fof(f495,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| app(cons(sK53(X15),nil),sK55(X15)) = X15
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f463,f479,f479,f480,f479]) ).
fof(f496,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| app(cons(sK53(X15),nil),sK55(X15)) = X15
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f462,f479,f479,f479,f480,f479]) ).
fof(f497,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| app(cons(sK53(X15),nil),sK55(X15)) = X15
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f461,f479,f479,f480,f479]) ).
fof(f498,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| ssList(sK55(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f460,f480,f479,f480,f479]) ).
fof(f499,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| ssList(sK55(X15))
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f459,f480,f479,f479,f480,f479]) ).
fof(f500,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| ssList(sK55(X15))
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f458,f480,f479,f480,f479]) ).
fof(f501,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| app(cons(sK53(X15),nil),sK55(X15)) = X15
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f457,f480,f479,f480,f479]) ).
fof(f502,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| app(cons(sK53(X15),nil),sK55(X15)) = X15
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f456,f480,f479,f479,f480,f479]) ).
fof(f503,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| app(cons(sK53(X15),nil),sK55(X15)) = X15
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f455,f480,f479,f480,f479]) ).
fof(f504,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| ssItem(sK53(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f454,f480,f479,f480,f479]) ).
fof(f505,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| ssItem(sK53(X15))
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f453,f480,f479,f479,f480,f479]) ).
fof(f506,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| ssItem(sK53(X15))
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f452,f480,f479,f480,f479]) ).
fof(f507,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| ssItem(sK53(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f451,f479,f479,f480,f479]) ).
fof(f508,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| ssItem(sK53(X15))
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f450,f479,f479,f479,f480,f479]) ).
fof(f509,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| ssItem(sK53(X15))
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f449,f479,f479,f480,f479]) ).
fof(f510,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| ssItem(sK57(X15))
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f448,f480,f479,f480,f479]) ).
fof(f511,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| ssItem(sK57(X15))
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f447,f480,f479,f479,f480,f479]) ).
fof(f512,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| ssItem(sK57(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f446,f480,f479,f480,f479]) ).
fof(f513,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| ssItem(sK57(X15))
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f445,f479,f479,f480,f479]) ).
fof(f514,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| ssItem(sK57(X15))
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f444,f479,f479,f479,f480,f479]) ).
fof(f515,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| ssItem(sK57(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f443,f479,f479,f480,f479]) ).
fof(f516,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| ssItem(sK57(X15))
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f442,f479,f479,f480,f479]) ).
fof(f517,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| ssItem(sK57(X15))
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f441,f480,f479,f480,f479]) ).
fof(f518,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| sK49 = app(sK60(X15),cons(sK57(X15),nil))
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f437,f480,f479,f479,f480,f479]) ).
fof(f519,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| lt(sK57(X15),sK53(X15))
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f436,f480,f479,f480,f479]) ).
fof(f520,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| ssList(sK60(X15))
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f435,f480,f479,f480,f479]) ).
fof(f521,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| sK49 = app(sK60(X15),cons(sK57(X15),nil))
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f434,f479,f479,f479,f480,f479]) ).
fof(f522,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| lt(sK57(X15),sK53(X15))
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f433,f479,f479,f480,f479]) ).
fof(f523,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| ssList(sK60(X15))
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f432,f479,f479,f480,f479]) ).
fof(f524,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| sK49 = app(sK60(X15),cons(sK57(X15),nil))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f431,f479,f479,f479,f480,f479]) ).
fof(f525,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| lt(sK57(X15),sK53(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f430,f479,f479,f480,f479]) ).
fof(f526,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| ssList(sK60(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f429,f479,f479,f480,f479]) ).
fof(f527,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| sK49 = app(sK60(X15),cons(sK57(X15),nil))
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f428,f479,f479,f479,f479,f480,f479]) ).
fof(f528,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| lt(sK57(X15),sK53(X15))
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f427,f479,f479,f479,f480,f479]) ).
fof(f529,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| ssList(sK60(X15))
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f426,f479,f479,f479,f480,f479]) ).
fof(f530,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| sK49 = app(sK60(X15),cons(sK57(X15),nil))
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f425,f479,f479,f479,f480,f479]) ).
fof(f531,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| lt(sK57(X15),sK53(X15))
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f424,f479,f479,f480,f479]) ).
fof(f532,plain,
! [X14,X15] :
( nil = sK49
| ~ strictorderedP(sK49)
| ssList(sK60(X15))
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f423,f479,f479,f480,f479]) ).
fof(f533,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| sK49 = app(sK60(X15),cons(sK57(X15),nil))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f422,f480,f479,f479,f480,f479]) ).
fof(f534,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| lt(sK57(X15),sK53(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f421,f480,f479,f480,f479]) ).
fof(f535,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| ssList(sK60(X15))
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f420,f480,f479,f480,f479]) ).
fof(f536,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| sK49 = app(sK60(X15),cons(sK57(X15),nil))
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f419,f480,f479,f479,f479,f480,f479]) ).
fof(f537,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| lt(sK57(X15),sK53(X15))
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f418,f480,f479,f479,f480,f479]) ).
fof(f538,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| ssList(sK60(X15))
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f417,f480,f479,f479,f480,f479]) ).
fof(f539,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| sK49 = app(sK60(X15),cons(sK57(X15),nil))
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f416,f480,f479,f479,f480,f479]) ).
fof(f540,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| lt(sK57(X15),sK53(X15))
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f415,f480,f479,f480,f479]) ).
fof(f541,plain,
! [X14,X15] :
( nil != sK50
| ~ strictorderedP(sK49)
| ssList(sK60(X15))
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15)
| ~ ssList(X15)
| ~ ssList(X14) ),
inference(definition_unfolding,[],[f414,f480,f479,f480,f479]) ).
fof(f599,definition,
( spl62_9
<=> ! [X14,X15] :
( ssList(sK60(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_9])],[avatar_definition]) ).
fof(f600,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| ssList(sK56(X14))
| ssList(sK60(X15)) )
| ~ spl62_9 ),
inference(avatar_component_clause,[],[f599]) ).
fof(f602,definition,
( spl62_10
<=> strictorderedP(sK49) ),
introduced(definition,[new_symbols(definition,[spl62_10])],[avatar_definition]) ).
fof(f604,plain,
( ~ strictorderedP(sK49)
| spl62_10 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f606,definition,
( spl62_11
<=> nil = sK50 ),
introduced(definition,[new_symbols(definition,[spl62_11])],[avatar_definition]) ).
fof(f609,plain,
( spl62_9
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f541,f606,f602,f599]) ).
fof(f614,definition,
( spl62_13
<=> ! [X14,X15] :
( lt(sK57(X15),sK53(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_13])],[avatar_definition]) ).
fof(f615,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| ssList(sK56(X14))
| lt(sK57(X15),sK53(X15)) )
| ~ spl62_13 ),
inference(avatar_component_clause,[],[f614]) ).
fof(f616,plain,
( spl62_13
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f540,f606,f602,f614]) ).
fof(f621,definition,
( spl62_15
<=> ! [X14,X15] :
( sK49 = app(sK60(X15),cons(sK57(X15),nil))
| ~ ssList(X14)
| ~ ssList(X15)
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_15])],[avatar_definition]) ).
fof(f622,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| ssList(sK56(X14))
| sK49 = app(sK60(X15),cons(sK57(X15),nil)) )
| ~ spl62_15 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f623,plain,
( spl62_15
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f539,f606,f602,f621]) ).
fof(f628,definition,
( spl62_17
<=> ! [X14,X15] :
( ssList(sK60(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_17])],[avatar_definition]) ).
fof(f629,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| sP59(sK58(X14),sK54(X14),sK49)
| ssList(sK60(X15)) )
| ~ spl62_17 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f630,plain,
( spl62_17
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f538,f606,f602,f628]) ).
fof(f632,definition,
( spl62_18
<=> ! [X14,X15] :
( lt(sK57(X15),sK53(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_18])],[avatar_definition]) ).
fof(f633,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| sP59(sK58(X14),sK54(X14),sK49)
| lt(sK57(X15),sK53(X15)) )
| ~ spl62_18 ),
inference(avatar_component_clause,[],[f632]) ).
fof(f634,plain,
( spl62_18
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f537,f606,f602,f632]) ).
fof(f636,definition,
( spl62_19
<=> ! [X14,X15] :
( sK49 = app(sK60(X15),cons(sK57(X15),nil))
| ~ ssList(X14)
| ~ ssList(X15)
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_19])],[avatar_definition]) ).
fof(f637,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| sP59(sK58(X14),sK54(X14),sK49)
| sK49 = app(sK60(X15),cons(sK57(X15),nil)) )
| ~ spl62_19 ),
inference(avatar_component_clause,[],[f636]) ).
fof(f638,plain,
( spl62_19
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f536,f606,f602,f636]) ).
fof(f643,definition,
( spl62_21
<=> ! [X14,X15] :
( ssList(sK60(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_21])],[avatar_definition]) ).
fof(f644,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| ssList(sK60(X15)) )
| ~ spl62_21 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f645,plain,
( spl62_21
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f535,f606,f602,f643]) ).
fof(f647,definition,
( spl62_22
<=> ! [X14,X15] :
( lt(sK57(X15),sK53(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_22])],[avatar_definition]) ).
fof(f648,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| lt(sK57(X15),sK53(X15)) )
| ~ spl62_22 ),
inference(avatar_component_clause,[],[f647]) ).
fof(f649,plain,
( spl62_22
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f534,f606,f602,f647]) ).
fof(f651,definition,
( spl62_23
<=> ! [X14,X15] :
( sK49 = app(sK60(X15),cons(sK57(X15),nil))
| ~ ssList(X14)
| ~ ssList(X15)
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_23])],[avatar_definition]) ).
fof(f652,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK49 = app(sK60(X15),cons(sK57(X15),nil)) )
| ~ spl62_23 ),
inference(avatar_component_clause,[],[f651]) ).
fof(f653,plain,
( spl62_23
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f533,f606,f602,f651]) ).
fof(f655,definition,
( spl62_24
<=> nil = sK49 ),
introduced(definition,[new_symbols(definition,[spl62_24])],[avatar_definition]) ).
fof(f658,plain,
( spl62_9
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f532,f655,f602,f599]) ).
fof(f659,plain,
( spl62_13
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f531,f655,f602,f614]) ).
fof(f660,plain,
( spl62_15
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f530,f655,f602,f621]) ).
fof(f661,plain,
( spl62_17
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f529,f655,f602,f628]) ).
fof(f662,plain,
( spl62_18
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f528,f655,f602,f632]) ).
fof(f663,plain,
( spl62_19
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f527,f655,f602,f636]) ).
fof(f664,plain,
( spl62_21
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f526,f655,f602,f643]) ).
fof(f665,plain,
( spl62_22
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f525,f655,f602,f647]) ).
fof(f666,plain,
( spl62_23
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f524,f655,f602,f651]) ).
fof(f671,definition,
( spl62_26
<=> ! [X14,X15] :
( ssList(sK60(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_26])],[avatar_definition]) ).
fof(f672,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| ssItem(sK54(X14))
| ssList(sK60(X15)) )
| ~ spl62_26 ),
inference(avatar_component_clause,[],[f671]) ).
fof(f673,plain,
( spl62_26
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f523,f655,f602,f671]) ).
fof(f675,definition,
( spl62_27
<=> ! [X14,X15] :
( lt(sK57(X15),sK53(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_27])],[avatar_definition]) ).
fof(f676,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| ssItem(sK54(X14))
| lt(sK57(X15),sK53(X15)) )
| ~ spl62_27 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f677,plain,
( spl62_27
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f522,f655,f602,f675]) ).
fof(f679,definition,
( spl62_28
<=> ! [X14,X15] :
( sK49 = app(sK60(X15),cons(sK57(X15),nil))
| ~ ssList(X14)
| ~ ssList(X15)
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_28])],[avatar_definition]) ).
fof(f680,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| ssItem(sK54(X14))
| sK49 = app(sK60(X15),cons(sK57(X15),nil)) )
| ~ spl62_28 ),
inference(avatar_component_clause,[],[f679]) ).
fof(f681,plain,
( spl62_28
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f521,f655,f602,f679]) ).
fof(f682,plain,
( spl62_26
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f520,f606,f602,f671]) ).
fof(f683,plain,
( spl62_27
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f519,f606,f602,f675]) ).
fof(f684,plain,
( spl62_28
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f518,f606,f602,f679]) ).
fof(f710,definition,
( spl62_37
<=> ! [X14,X15] :
( ssItem(sK57(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_37])],[avatar_definition]) ).
fof(f711,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| ssItem(sK54(X14))
| ssItem(sK57(X15)) )
| ~ spl62_37 ),
inference(avatar_component_clause,[],[f710]) ).
fof(f712,plain,
( spl62_37
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f517,f606,f602,f710]) ).
fof(f713,plain,
( spl62_37
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f516,f655,f602,f710]) ).
fof(f715,definition,
( spl62_38
<=> ! [X14,X15] :
( ssItem(sK57(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_38])],[avatar_definition]) ).
fof(f716,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| ssItem(sK57(X15)) )
| ~ spl62_38 ),
inference(avatar_component_clause,[],[f715]) ).
fof(f717,plain,
( spl62_38
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f515,f655,f602,f715]) ).
fof(f719,definition,
( spl62_39
<=> ! [X14,X15] :
( ssItem(sK57(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_39])],[avatar_definition]) ).
fof(f720,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| sP59(sK58(X14),sK54(X14),sK49)
| ssItem(sK57(X15)) )
| ~ spl62_39 ),
inference(avatar_component_clause,[],[f719]) ).
fof(f721,plain,
( spl62_39
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f514,f655,f602,f719]) ).
fof(f723,definition,
( spl62_40
<=> ! [X14,X15] :
( ssItem(sK57(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_40])],[avatar_definition]) ).
fof(f724,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| ssList(sK56(X14))
| ssItem(sK57(X15)) )
| ~ spl62_40 ),
inference(avatar_component_clause,[],[f723]) ).
fof(f725,plain,
( spl62_40
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f513,f655,f602,f723]) ).
fof(f726,plain,
( spl62_38
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f512,f606,f602,f715]) ).
fof(f727,plain,
( spl62_39
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f511,f606,f602,f719]) ).
fof(f728,plain,
( spl62_40
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f510,f606,f602,f723]) ).
fof(f733,definition,
( spl62_42
<=> ! [X14,X15] :
( ssItem(sK53(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_42])],[avatar_definition]) ).
fof(f734,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| ssList(sK56(X14))
| ssItem(sK53(X15)) )
| ~ spl62_42 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f735,plain,
( spl62_42
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f509,f655,f602,f733]) ).
fof(f737,definition,
( spl62_43
<=> ! [X14,X15] :
( ssItem(sK53(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_43])],[avatar_definition]) ).
fof(f738,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| sP59(sK58(X14),sK54(X14),sK49)
| ssItem(sK53(X15)) )
| ~ spl62_43 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f739,plain,
( spl62_43
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f508,f655,f602,f737]) ).
fof(f741,definition,
( spl62_44
<=> ! [X14,X15] :
( ssItem(sK53(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_44])],[avatar_definition]) ).
fof(f742,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| ssItem(sK53(X15)) )
| ~ spl62_44 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f743,plain,
( spl62_44
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f507,f655,f602,f741]) ).
fof(f744,plain,
( spl62_42
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f506,f606,f602,f733]) ).
fof(f745,plain,
( spl62_43
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f505,f606,f602,f737]) ).
fof(f746,plain,
( spl62_44
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f504,f606,f602,f741]) ).
fof(f751,definition,
( spl62_46
<=> ! [X14,X15] :
( app(cons(sK53(X15),nil),sK55(X15)) = X15
| ~ ssList(X14)
| ~ ssList(X15)
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_46])],[avatar_definition]) ).
fof(f752,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| ssList(sK56(X14))
| app(cons(sK53(X15),nil),sK55(X15)) = X15 )
| ~ spl62_46 ),
inference(avatar_component_clause,[],[f751]) ).
fof(f753,plain,
( spl62_46
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f503,f606,f602,f751]) ).
fof(f755,definition,
( spl62_47
<=> ! [X14,X15] :
( app(cons(sK53(X15),nil),sK55(X15)) = X15
| ~ ssList(X14)
| ~ ssList(X15)
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_47])],[avatar_definition]) ).
fof(f756,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| sP59(sK58(X14),sK54(X14),sK49)
| app(cons(sK53(X15),nil),sK55(X15)) = X15 )
| ~ spl62_47 ),
inference(avatar_component_clause,[],[f755]) ).
fof(f757,plain,
( spl62_47
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f502,f606,f602,f755]) ).
fof(f759,definition,
( spl62_48
<=> ! [X14,X15] :
( app(cons(sK53(X15),nil),sK55(X15)) = X15
| ~ ssList(X14)
| ~ ssList(X15)
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_48])],[avatar_definition]) ).
fof(f760,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| app(cons(sK53(X15),nil),sK55(X15)) = X15 )
| ~ spl62_48 ),
inference(avatar_component_clause,[],[f759]) ).
fof(f761,plain,
( spl62_48
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f501,f606,f602,f759]) ).
fof(f766,definition,
( spl62_50
<=> ! [X14,X15] :
( ssList(sK55(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| ssList(sK56(X14))
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_50])],[avatar_definition]) ).
fof(f767,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| ssList(sK56(X14))
| ssList(sK55(X15)) )
| ~ spl62_50 ),
inference(avatar_component_clause,[],[f766]) ).
fof(f768,plain,
( spl62_50
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f500,f606,f602,f766]) ).
fof(f770,definition,
( spl62_51
<=> ! [X14,X15] :
( ssList(sK55(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| sP59(sK58(X14),sK54(X14),sK49)
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_51])],[avatar_definition]) ).
fof(f771,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| sP59(sK58(X14),sK54(X14),sK49)
| ssList(sK55(X15)) )
| ~ spl62_51 ),
inference(avatar_component_clause,[],[f770]) ).
fof(f772,plain,
( spl62_51
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f499,f606,f602,f770]) ).
fof(f774,definition,
( spl62_52
<=> ! [X14,X15] :
( ssList(sK55(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_52])],[avatar_definition]) ).
fof(f775,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| app(sK56(X14),cons(sK54(X14),nil)) = X14
| ssList(sK55(X15)) )
| ~ spl62_52 ),
inference(avatar_component_clause,[],[f774]) ).
fof(f776,plain,
( spl62_52
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f498,f606,f602,f774]) ).
fof(f777,plain,
( spl62_46
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f497,f655,f602,f751]) ).
fof(f778,plain,
( spl62_47
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f496,f655,f602,f755]) ).
fof(f779,plain,
( spl62_48
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f495,f655,f602,f759]) ).
fof(f780,plain,
( spl62_50
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f494,f655,f602,f766]) ).
fof(f781,plain,
( spl62_51
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f493,f655,f602,f770]) ).
fof(f782,plain,
( spl62_52
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f492,f655,f602,f774]) ).
fof(f784,definition,
( spl62_53
<=> ! [X14,X15] :
( ssList(sK55(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_53])],[avatar_definition]) ).
fof(f785,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| ssItem(sK54(X14))
| ssList(sK55(X15)) )
| ~ spl62_53 ),
inference(avatar_component_clause,[],[f784]) ).
fof(f786,plain,
( spl62_53
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f491,f655,f602,f784]) ).
fof(f788,definition,
( spl62_54
<=> ! [X14,X15] :
( app(cons(sK53(X15),nil),sK55(X15)) = X15
| ~ ssList(X14)
| ~ ssList(X15)
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_54])],[avatar_definition]) ).
fof(f789,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| ssItem(sK54(X14))
| app(cons(sK53(X15),nil),sK55(X15)) = X15 )
| ~ spl62_54 ),
inference(avatar_component_clause,[],[f788]) ).
fof(f790,plain,
( spl62_54
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f490,f655,f602,f788]) ).
fof(f791,plain,
( spl62_53
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f489,f606,f602,f784]) ).
fof(f792,plain,
( spl62_54
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f488,f606,f602,f788]) ).
fof(f794,definition,
( spl62_55
<=> ! [X14,X15] :
( ssItem(sK53(X15))
| ~ ssList(X14)
| ~ ssList(X15)
| ssItem(sK54(X14))
| sK50 != app(app(X14,sK49),X15) ) ),
introduced(definition,[new_symbols(definition,[spl62_55])],[avatar_definition]) ).
fof(f795,plain,
( ! [X14,X15] :
( sK50 != app(app(X14,sK49),X15)
| ~ ssList(X14)
| ~ ssList(X15)
| ssItem(sK54(X14))
| ssItem(sK53(X15)) )
| ~ spl62_55 ),
inference(avatar_component_clause,[],[f794]) ).
fof(f796,plain,
( spl62_55
| ~ spl62_10
| ~ spl62_11 ),
inference(avatar_split_clause,[],[f487,f606,f602,f794]) ).
fof(f797,plain,
( spl62_55
| ~ spl62_10
| spl62_24 ),
inference(avatar_split_clause,[],[f486,f655,f602,f794]) ).
fof(f798,plain,
( spl62_11
| ~ spl62_24 ),
inference(avatar_split_clause,[],[f477,f655,f606]) ).
fof(f1370,plain,
( $false
| spl62_10 ),
inference(resolution,[],[f604,f474]) ).
fof(f1371,plain,
spl62_10,
inference(avatar_contradiction_clause,[],[f1370]) ).
fof(f1408,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| sP59(sK58(sK51),sK54(sK51),sK49)
| lt(sK57(sK52),sK53(sK52))
| ~ spl62_18 ),
inference(superposition,[],[f633,f475]) ).
fof(f1409,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| sP59(sK58(sK51),sK54(sK51),sK49)
| lt(sK57(sK52),sK53(sK52))
| ~ spl62_18 ),
inference(trivial_inequality_removal,[],[f1408]) ).
fof(f1411,definition,
( spl62_240
<=> lt(sK57(sK52),sK53(sK52)) ),
introduced(definition,[new_symbols(definition,[spl62_240])],[avatar_definition]) ).
fof(f1415,definition,
( spl62_241
<=> sP59(sK58(sK51),sK54(sK51),sK49) ),
introduced(definition,[new_symbols(definition,[spl62_241])],[avatar_definition]) ).
fof(f1417,plain,
( sP59(sK58(sK51),sK54(sK51),sK49)
| ~ spl62_241 ),
inference(avatar_component_clause,[],[f1415]) ).
fof(f1419,definition,
( spl62_242
<=> ssList(sK52) ),
introduced(definition,[new_symbols(definition,[spl62_242])],[avatar_definition]) ).
fof(f1421,plain,
( ~ ssList(sK52)
| spl62_242 ),
inference(avatar_component_clause,[],[f1419]) ).
fof(f1423,definition,
( spl62_243
<=> ssList(sK51) ),
introduced(definition,[new_symbols(definition,[spl62_243])],[avatar_definition]) ).
fof(f1425,plain,
( ~ ssList(sK51)
| spl62_243 ),
inference(avatar_component_clause,[],[f1423]) ).
fof(f1426,plain,
( spl62_240
| spl62_241
| ~ spl62_242
| ~ spl62_243
| ~ spl62_18 ),
inference(avatar_split_clause,[],[f1409,f632,f1423,f1419,f1415,f1411]) ).
fof(f1427,plain,
( $false
| spl62_242 ),
inference(resolution,[],[f1421,f473]) ).
fof(f1428,plain,
spl62_242,
inference(avatar_contradiction_clause,[],[f1427]) ).
fof(f1429,plain,
( $false
| spl62_243 ),
inference(resolution,[],[f1425,f476]) ).
fof(f1430,plain,
spl62_243,
inference(avatar_contradiction_clause,[],[f1429]) ).
fof(f1433,plain,
( lt(sK54(sK51),sK58(sK51))
| ~ spl62_241 ),
inference(resolution,[],[f412,f1417]) ).
fof(f1449,definition,
( spl62_246
<=> ssItem(sK58(sK51)) ),
introduced(definition,[new_symbols(definition,[spl62_246])],[avatar_definition]) ).
fof(f1451,plain,
( ~ ssItem(sK58(sK51))
| spl62_246 ),
inference(avatar_component_clause,[],[f1449]) ).
fof(f1453,definition,
( spl62_247
<=> ssList(sK61(sK49,sK54(sK51),sK58(sK51))) ),
introduced(definition,[new_symbols(definition,[spl62_247])],[avatar_definition]) ).
fof(f1455,plain,
( ~ ssList(sK61(sK49,sK54(sK51),sK58(sK51)))
| spl62_247 ),
inference(avatar_component_clause,[],[f1453]) ).
fof(f1480,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| sK51 = app(sK56(sK51),cons(sK54(sK51),nil))
| lt(sK57(sK52),sK53(sK52))
| ~ spl62_22 ),
inference(superposition,[],[f648,f475]) ).
fof(f1481,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| sK51 = app(sK56(sK51),cons(sK54(sK51),nil))
| lt(sK57(sK52),sK53(sK52))
| ~ spl62_22 ),
inference(trivial_inequality_removal,[],[f1480]) ).
fof(f1482,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| sP59(sK58(sK51),sK54(sK51),sK49)
| sK52 = app(cons(sK53(sK52),nil),sK55(sK52))
| ~ spl62_47 ),
inference(superposition,[],[f756,f475]) ).
fof(f1483,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| sP59(sK58(sK51),sK54(sK51),sK49)
| sK52 = app(cons(sK53(sK52),nil),sK55(sK52))
| ~ spl62_47 ),
inference(trivial_inequality_removal,[],[f1482]) ).
fof(f1485,definition,
( spl62_251
<=> sK52 = app(cons(sK53(sK52),nil),sK55(sK52)) ),
introduced(definition,[new_symbols(definition,[spl62_251])],[avatar_definition]) ).
fof(f1487,plain,
( sK52 = app(cons(sK53(sK52),nil),sK55(sK52))
| ~ spl62_251 ),
inference(avatar_component_clause,[],[f1485]) ).
fof(f1488,plain,
( spl62_251
| spl62_241
| ~ spl62_242
| ~ spl62_243
| ~ spl62_47 ),
inference(avatar_split_clause,[],[f1483,f755,f1423,f1419,f1415,f1485]) ).
fof(f1492,definition,
( spl62_252
<=> ssItem(sK53(sK52)) ),
introduced(definition,[new_symbols(definition,[spl62_252])],[avatar_definition]) ).
fof(f1496,definition,
( spl62_253
<=> ssList(sK55(sK52)) ),
introduced(definition,[new_symbols(definition,[spl62_253])],[avatar_definition]) ).
fof(f1503,definition,
( spl62_255
<=> ! [X0,X1] :
( sK49 != app(X0,cons(X1,nil))
| ~ lt(X1,sK53(sK52))
| ~ ssItem(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl62_255])],[avatar_definition]) ).
fof(f1504,plain,
( ! [X0,X1] :
( sK49 != app(X0,cons(X1,nil))
| ~ lt(X1,sK53(sK52))
| ~ ssItem(X1)
| ~ ssList(X0) )
| ~ spl62_255 ),
inference(avatar_component_clause,[],[f1503]) ).
fof(f1512,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| ssItem(sK54(sK51))
| ssItem(sK57(sK52))
| ~ spl62_37 ),
inference(superposition,[],[f711,f475]) ).
fof(f1513,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| ssItem(sK54(sK51))
| ssItem(sK57(sK52))
| ~ spl62_37 ),
inference(trivial_inequality_removal,[],[f1512]) ).
fof(f1515,definition,
( spl62_256
<=> ssItem(sK57(sK52)) ),
introduced(definition,[new_symbols(definition,[spl62_256])],[avatar_definition]) ).
fof(f1519,definition,
( spl62_257
<=> ssItem(sK54(sK51)) ),
introduced(definition,[new_symbols(definition,[spl62_257])],[avatar_definition]) ).
fof(f1522,plain,
( spl62_256
| spl62_257
| ~ spl62_242
| ~ spl62_243
| ~ spl62_37 ),
inference(avatar_split_clause,[],[f1513,f710,f1423,f1419,f1519,f1515]) ).
fof(f1523,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| ssItem(sK54(sK51))
| ssList(sK55(sK52))
| ~ spl62_53 ),
inference(superposition,[],[f785,f475]) ).
fof(f1524,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| ssItem(sK54(sK51))
| ssList(sK55(sK52))
| ~ spl62_53 ),
inference(trivial_inequality_removal,[],[f1523]) ).
fof(f1528,definition,
( spl62_258
<=> sK51 = app(sK56(sK51),cons(sK54(sK51),nil)) ),
introduced(definition,[new_symbols(definition,[spl62_258])],[avatar_definition]) ).
fof(f1530,plain,
( sK51 = app(sK56(sK51),cons(sK54(sK51),nil))
| ~ spl62_258 ),
inference(avatar_component_clause,[],[f1528]) ).
fof(f1531,plain,
( spl62_240
| spl62_258
| ~ spl62_242
| ~ spl62_243
| ~ spl62_22 ),
inference(avatar_split_clause,[],[f1481,f647,f1423,f1419,f1528,f1411]) ).
fof(f1532,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| ssItem(sK54(sK51))
| lt(sK57(sK52),sK53(sK52))
| ~ spl62_27 ),
inference(superposition,[],[f676,f475]) ).
fof(f1533,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| ssItem(sK54(sK51))
| lt(sK57(sK52),sK53(sK52))
| ~ spl62_27 ),
inference(trivial_inequality_removal,[],[f1532]) ).
fof(f1538,plain,
( ssItem(sK58(sK51))
| ~ spl62_241 ),
inference(resolution,[],[f440,f1417]) ).
fof(f1539,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| sP59(sK58(sK51),sK54(sK51),sK49)
| ssItem(sK57(sK52))
| ~ spl62_39 ),
inference(superposition,[],[f720,f475]) ).
fof(f1540,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| sP59(sK58(sK51),sK54(sK51),sK49)
| ssItem(sK57(sK52))
| ~ spl62_39 ),
inference(trivial_inequality_removal,[],[f1539]) ).
fof(f1545,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| sP59(sK58(sK51),sK54(sK51),sK49)
| ssList(sK55(sK52))
| ~ spl62_51 ),
inference(superposition,[],[f771,f475]) ).
fof(f1546,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| sP59(sK58(sK51),sK54(sK51),sK49)
| ssList(sK55(sK52))
| ~ spl62_51 ),
inference(trivial_inequality_removal,[],[f1545]) ).
fof(f1547,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| sK51 = app(sK56(sK51),cons(sK54(sK51),nil))
| ssList(sK55(sK52))
| ~ spl62_52 ),
inference(superposition,[],[f775,f475]) ).
fof(f1548,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| sK51 = app(sK56(sK51),cons(sK54(sK51),nil))
| ssList(sK55(sK52))
| ~ spl62_52 ),
inference(trivial_inequality_removal,[],[f1547]) ).
fof(f1556,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| sP59(sK58(sK51),sK54(sK51),sK49)
| sK49 = app(sK60(sK52),cons(sK57(sK52),nil))
| ~ spl62_19 ),
inference(superposition,[],[f637,f475]) ).
fof(f1557,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| sP59(sK58(sK51),sK54(sK51),sK49)
| sK49 = app(sK60(sK52),cons(sK57(sK52),nil))
| ~ spl62_19 ),
inference(trivial_inequality_removal,[],[f1556]) ).
fof(f1558,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| sK51 = app(sK56(sK51),cons(sK54(sK51),nil))
| sK49 = app(sK60(sK52),cons(sK57(sK52),nil))
| ~ spl62_23 ),
inference(superposition,[],[f652,f475]) ).
fof(f1559,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| sK51 = app(sK56(sK51),cons(sK54(sK51),nil))
| sK49 = app(sK60(sK52),cons(sK57(sK52),nil))
| ~ spl62_23 ),
inference(trivial_inequality_removal,[],[f1558]) ).
fof(f1563,definition,
( spl62_260
<=> ssList(sK56(sK51)) ),
introduced(definition,[new_symbols(definition,[spl62_260])],[avatar_definition]) ).
fof(f1579,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| ssList(sK56(sK51))
| ssItem(sK57(sK52))
| ~ spl62_40 ),
inference(superposition,[],[f724,f475]) ).
fof(f1580,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| ssList(sK56(sK51))
| ssItem(sK57(sK52))
| ~ spl62_40 ),
inference(trivial_inequality_removal,[],[f1579]) ).
fof(f1581,plain,
( spl62_256
| spl62_260
| ~ spl62_242
| ~ spl62_243
| ~ spl62_40 ),
inference(avatar_split_clause,[],[f1580,f723,f1423,f1419,f1563,f1515]) ).
fof(f1582,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| ssList(sK56(sK51))
| ssItem(sK53(sK52))
| ~ spl62_42 ),
inference(superposition,[],[f734,f475]) ).
fof(f1583,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| ssList(sK56(sK51))
| ssItem(sK53(sK52))
| ~ spl62_42 ),
inference(trivial_inequality_removal,[],[f1582]) ).
fof(f1584,plain,
( spl62_252
| spl62_260
| ~ spl62_242
| ~ spl62_243
| ~ spl62_42 ),
inference(avatar_split_clause,[],[f1583,f733,f1423,f1419,f1563,f1492]) ).
fof(f1585,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| ssList(sK56(sK51))
| ssList(sK55(sK52))
| ~ spl62_50 ),
inference(superposition,[],[f767,f475]) ).
fof(f1586,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| ssList(sK56(sK51))
| ssList(sK55(sK52))
| ~ spl62_50 ),
inference(trivial_inequality_removal,[],[f1585]) ).
fof(f1587,plain,
( spl62_253
| spl62_260
| ~ spl62_242
| ~ spl62_243
| ~ spl62_50 ),
inference(avatar_split_clause,[],[f1586,f766,f1423,f1419,f1563,f1496]) ).
fof(f1588,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| ssItem(sK54(sK51))
| ssItem(sK53(sK52))
| ~ spl62_55 ),
inference(superposition,[],[f795,f475]) ).
fof(f1589,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| ssItem(sK54(sK51))
| ssItem(sK53(sK52))
| ~ spl62_55 ),
inference(trivial_inequality_removal,[],[f1588]) ).
fof(f1593,definition,
( spl62_263
<=> sK49 = app(sK60(sK52),cons(sK57(sK52),nil)) ),
introduced(definition,[new_symbols(definition,[spl62_263])],[avatar_definition]) ).
fof(f1595,plain,
( sK49 = app(sK60(sK52),cons(sK57(sK52),nil))
| ~ spl62_263 ),
inference(avatar_component_clause,[],[f1593]) ).
fof(f1596,plain,
( spl62_263
| spl62_241
| ~ spl62_242
| ~ spl62_243
| ~ spl62_19 ),
inference(avatar_split_clause,[],[f1557,f636,f1423,f1419,f1415,f1593]) ).
fof(f1597,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| ssList(sK56(sK51))
| lt(sK57(sK52),sK53(sK52))
| ~ spl62_13 ),
inference(superposition,[],[f615,f475]) ).
fof(f1598,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| ssList(sK56(sK51))
| lt(sK57(sK52),sK53(sK52))
| ~ spl62_13 ),
inference(trivial_inequality_removal,[],[f1597]) ).
fof(f1599,plain,
( spl62_240
| spl62_260
| ~ spl62_242
| ~ spl62_243
| ~ spl62_13 ),
inference(avatar_split_clause,[],[f1598,f614,f1423,f1419,f1563,f1411]) ).
fof(f1600,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| sP59(sK58(sK51),sK54(sK51),sK49)
| ssItem(sK53(sK52))
| ~ spl62_43 ),
inference(superposition,[],[f738,f475]) ).
fof(f1601,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| sP59(sK58(sK51),sK54(sK51),sK49)
| ssItem(sK53(sK52))
| ~ spl62_43 ),
inference(trivial_inequality_removal,[],[f1600]) ).
fof(f1611,definition,
( spl62_264
<=> ssList(sK60(sK52)) ),
introduced(definition,[new_symbols(definition,[spl62_264])],[avatar_definition]) ).
fof(f1629,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| ssList(sK56(sK51))
| ssList(sK60(sK52))
| ~ spl62_9 ),
inference(superposition,[],[f600,f475]) ).
fof(f1630,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| ssList(sK56(sK51))
| ssList(sK60(sK52))
| ~ spl62_9 ),
inference(trivial_inequality_removal,[],[f1629]) ).
fof(f1631,plain,
( spl62_264
| spl62_260
| ~ spl62_242
| ~ spl62_243
| ~ spl62_9 ),
inference(avatar_split_clause,[],[f1630,f599,f1423,f1419,f1563,f1611]) ).
fof(f1632,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| ssItem(sK54(sK51))
| ssList(sK60(sK52))
| ~ spl62_26 ),
inference(superposition,[],[f672,f475]) ).
fof(f1633,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| ssItem(sK54(sK51))
| ssList(sK60(sK52))
| ~ spl62_26 ),
inference(trivial_inequality_removal,[],[f1632]) ).
fof(f1634,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| sP59(sK58(sK51),sK54(sK51),sK49)
| ssList(sK60(sK52))
| ~ spl62_17 ),
inference(superposition,[],[f629,f475]) ).
fof(f1635,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| sP59(sK58(sK51),sK54(sK51),sK49)
| ssList(sK60(sK52))
| ~ spl62_17 ),
inference(trivial_inequality_removal,[],[f1634]) ).
fof(f1636,plain,
( spl62_264
| spl62_241
| ~ spl62_242
| ~ spl62_243
| ~ spl62_17 ),
inference(avatar_split_clause,[],[f1635,f628,f1423,f1419,f1415,f1611]) ).
fof(f1637,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| ssList(sK56(sK51))
| sK49 = app(sK60(sK52),cons(sK57(sK52),nil))
| ~ spl62_15 ),
inference(superposition,[],[f622,f475]) ).
fof(f1638,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| ssList(sK56(sK51))
| sK49 = app(sK60(sK52),cons(sK57(sK52),nil))
| ~ spl62_15 ),
inference(trivial_inequality_removal,[],[f1637]) ).
fof(f1641,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| sK51 = app(sK56(sK51),cons(sK54(sK51),nil))
| ssList(sK60(sK52))
| ~ spl62_21 ),
inference(superposition,[],[f644,f475]) ).
fof(f1642,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| sK51 = app(sK56(sK51),cons(sK54(sK51),nil))
| ssList(sK60(sK52))
| ~ spl62_21 ),
inference(trivial_inequality_removal,[],[f1641]) ).
fof(f1643,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| ssItem(sK54(sK51))
| sK49 = app(sK60(sK52),cons(sK57(sK52),nil))
| ~ spl62_28 ),
inference(superposition,[],[f680,f475]) ).
fof(f1644,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| ssItem(sK54(sK51))
| sK49 = app(sK60(sK52),cons(sK57(sK52),nil))
| ~ spl62_28 ),
inference(trivial_inequality_removal,[],[f1643]) ).
fof(f1648,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| sK51 = app(sK56(sK51),cons(sK54(sK51),nil))
| ssItem(sK57(sK52))
| ~ spl62_38 ),
inference(superposition,[],[f716,f475]) ).
fof(f1649,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| sK51 = app(sK56(sK51),cons(sK54(sK51),nil))
| ssItem(sK57(sK52))
| ~ spl62_38 ),
inference(trivial_inequality_removal,[],[f1648]) ).
fof(f1654,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| sK51 = app(sK56(sK51),cons(sK54(sK51),nil))
| ssItem(sK53(sK52))
| ~ spl62_44 ),
inference(superposition,[],[f742,f475]) ).
fof(f1655,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| sK51 = app(sK56(sK51),cons(sK54(sK51),nil))
| ssItem(sK53(sK52))
| ~ spl62_44 ),
inference(trivial_inequality_removal,[],[f1654]) ).
fof(f1657,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| ssList(sK56(sK51))
| sK52 = app(cons(sK53(sK52),nil),sK55(sK52))
| ~ spl62_46 ),
inference(superposition,[],[f752,f475]) ).
fof(f1658,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| ssList(sK56(sK51))
| sK52 = app(cons(sK53(sK52),nil),sK55(sK52))
| ~ spl62_46 ),
inference(trivial_inequality_removal,[],[f1657]) ).
fof(f1661,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| ssItem(sK54(sK51))
| sK52 = app(cons(sK53(sK52),nil),sK55(sK52))
| ~ spl62_54 ),
inference(superposition,[],[f789,f475]) ).
fof(f1662,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| ssItem(sK54(sK51))
| sK52 = app(cons(sK53(sK52),nil),sK55(sK52))
| ~ spl62_54 ),
inference(trivial_inequality_removal,[],[f1661]) ).
fof(f1667,plain,
( sK50 != sK50
| ~ ssList(sK51)
| ~ ssList(sK52)
| sK51 = app(sK56(sK51),cons(sK54(sK51),nil))
| sK52 = app(cons(sK53(sK52),nil),sK55(sK52))
| ~ spl62_48 ),
inference(superposition,[],[f760,f475]) ).
fof(f1668,plain,
( ~ ssList(sK51)
| ~ ssList(sK52)
| sK51 = app(sK56(sK51),cons(sK54(sK51),nil))
| sK52 = app(cons(sK53(sK52),nil),sK55(sK52))
| ~ spl62_48 ),
inference(trivial_inequality_removal,[],[f1667]) ).
fof(f1673,definition,
( spl62_270
<=> lt(sK54(sK51),sK58(sK51)) ),
introduced(definition,[new_symbols(definition,[spl62_270])],[avatar_definition]) ).
fof(f1675,plain,
( ~ lt(sK54(sK51),sK58(sK51))
| spl62_270 ),
inference(avatar_component_clause,[],[f1673]) ).
fof(f1677,plain,
( $false
| ~ spl62_241
| spl62_246 ),
inference(resolution,[],[f1451,f1538]) ).
fof(f1678,plain,
( ~ spl62_241
| spl62_246 ),
inference(avatar_contradiction_clause,[],[f1677]) ).
fof(f1681,plain,
( $false
| ~ spl62_241
| spl62_270 ),
inference(resolution,[],[f1675,f1433]) ).
fof(f1682,plain,
( ~ spl62_241
| spl62_270 ),
inference(avatar_contradiction_clause,[],[f1681]) ).
fof(f1687,definition,
( spl62_271
<=> ! [X0,X1] :
( ~ lt(X0,sK58(sK51))
| ~ ssItem(X0)
| ~ ssList(X1)
| sK51 != app(X1,cons(X0,nil)) ) ),
introduced(definition,[new_symbols(definition,[spl62_271])],[avatar_definition]) ).
fof(f1688,plain,
( ! [X0,X1] :
( sK51 != app(X1,cons(X0,nil))
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ lt(X0,sK58(sK51)) )
| ~ spl62_271 ),
inference(avatar_component_clause,[],[f1687]) ).
fof(f1690,plain,
( ~ sP59(sK58(sK51),sK54(sK51),sK49)
| spl62_247 ),
inference(resolution,[],[f1455,f411]) ).
fof(f1693,plain,
( $false
| ~ spl62_241
| spl62_247 ),
inference(resolution,[],[f1690,f1417]) ).
fof(f1694,plain,
( ~ spl62_241
| spl62_247 ),
inference(avatar_contradiction_clause,[],[f1693]) ).
fof(f2410,plain,
( spl62_251
| spl62_258
| ~ spl62_242
| ~ spl62_243
| ~ spl62_48 ),
inference(avatar_split_clause,[],[f1668,f759,f1423,f1419,f1528,f1485]) ).
fof(f2464,plain,
( sK49 != sK49
| ~ lt(sK57(sK52),sK53(sK52))
| ~ ssItem(sK57(sK52))
| ~ ssList(sK60(sK52))
| ~ spl62_255
| ~ spl62_263 ),
inference(superposition,[],[f1504,f1595]) ).
fof(f2469,plain,
( spl62_252
| spl62_241
| ~ spl62_242
| ~ spl62_243
| ~ spl62_43 ),
inference(avatar_split_clause,[],[f1601,f737,f1423,f1419,f1415,f1492]) ).
fof(f2470,plain,
( spl62_252
| spl62_258
| ~ spl62_242
| ~ spl62_243
| ~ spl62_44 ),
inference(avatar_split_clause,[],[f1655,f741,f1423,f1419,f1528,f1492]) ).
fof(f2471,plain,
( spl62_253
| spl62_241
| ~ spl62_242
| ~ spl62_243
| ~ spl62_51 ),
inference(avatar_split_clause,[],[f1546,f770,f1423,f1419,f1415,f1496]) ).
fof(f2472,plain,
( spl62_253
| spl62_258
| ~ spl62_242
| ~ spl62_243
| ~ spl62_52 ),
inference(avatar_split_clause,[],[f1548,f774,f1423,f1419,f1528,f1496]) ).
fof(f2473,plain,
( ~ lt(sK57(sK52),sK53(sK52))
| ~ ssItem(sK57(sK52))
| ~ ssList(sK60(sK52))
| ~ spl62_255
| ~ spl62_263 ),
inference(trivial_inequality_removal,[],[f2464]) ).
fof(f2478,plain,
( spl62_256
| spl62_241
| ~ spl62_242
| ~ spl62_243
| ~ spl62_39 ),
inference(avatar_split_clause,[],[f1540,f719,f1423,f1419,f1415,f1515]) ).
fof(f2479,plain,
( spl62_256
| spl62_258
| ~ spl62_242
| ~ spl62_243
| ~ spl62_38 ),
inference(avatar_split_clause,[],[f1649,f715,f1423,f1419,f1528,f1515]) ).
fof(f2508,plain,
( sK49 = app(cons(sK58(sK51),nil),sK61(sK49,sK54(sK51),sK58(sK51)))
| ~ spl62_241 ),
inference(resolution,[],[f1417,f413]) ).
fof(f2549,plain,
( spl62_252
| spl62_257
| ~ spl62_242
| ~ spl62_243
| ~ spl62_55 ),
inference(avatar_split_clause,[],[f1589,f794,f1423,f1419,f1519,f1492]) ).
fof(f2550,plain,
( spl62_253
| spl62_257
| ~ spl62_242
| ~ spl62_243
| ~ spl62_53 ),
inference(avatar_split_clause,[],[f1524,f784,f1423,f1419,f1519,f1496]) ).
fof(f2570,plain,
( spl62_264
| spl62_257
| ~ spl62_242
| ~ spl62_243
| ~ spl62_26 ),
inference(avatar_split_clause,[],[f1633,f671,f1423,f1419,f1519,f1611]) ).
fof(f2587,plain,
( spl62_240
| spl62_257
| ~ spl62_242
| ~ spl62_243
| ~ spl62_27 ),
inference(avatar_split_clause,[],[f1533,f675,f1423,f1419,f1519,f1411]) ).
fof(f2613,plain,
( spl62_251
| spl62_260
| ~ spl62_242
| ~ spl62_243
| ~ spl62_46 ),
inference(avatar_split_clause,[],[f1658,f751,f1423,f1419,f1563,f1485]) ).
fof(f2614,plain,
( spl62_251
| spl62_257
| ~ spl62_242
| ~ spl62_243
| ~ spl62_54 ),
inference(avatar_split_clause,[],[f1662,f788,f1423,f1419,f1519,f1485]) ).
fof(f2615,plain,
( spl62_263
| spl62_258
| ~ spl62_242
| ~ spl62_243
| ~ spl62_23 ),
inference(avatar_split_clause,[],[f1559,f651,f1423,f1419,f1528,f1593]) ).
fof(f2616,plain,
( spl62_263
| spl62_257
| ~ spl62_242
| ~ spl62_243
| ~ spl62_28 ),
inference(avatar_split_clause,[],[f1644,f679,f1423,f1419,f1519,f1593]) ).
fof(f2617,plain,
( spl62_263
| spl62_260
| ~ spl62_242
| ~ spl62_243
| ~ spl62_15 ),
inference(avatar_split_clause,[],[f1638,f621,f1423,f1419,f1563,f1593]) ).
fof(f2619,plain,
( ! [X0,X1] :
( sK52 != sK52
| sK49 != app(X0,cons(X1,nil))
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ lt(X1,sK53(sK52))
| ~ ssList(sK55(sK52))
| ~ ssItem(sK53(sK52)) )
| ~ spl62_251 ),
inference(superposition,[],[f439,f1487]) ).
fof(f2620,plain,
( ! [X0,X1] :
( sK49 != app(X0,cons(X1,nil))
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ lt(X1,sK53(sK52))
| ~ ssList(sK55(sK52))
| ~ ssItem(sK53(sK52)) )
| ~ spl62_251 ),
inference(trivial_inequality_removal,[],[f2619]) ).
fof(f2621,plain,
( ~ spl62_252
| ~ spl62_253
| spl62_255
| ~ spl62_251 ),
inference(avatar_split_clause,[],[f2620,f1485,f1503,f1496,f1492]) ).
fof(f2626,plain,
( ! [X0,X1] :
( sK49 != sK49
| ~ lt(X0,sK58(sK51))
| ~ ssList(sK61(sK49,sK54(sK51),sK58(sK51)))
| ~ ssItem(sK58(sK51))
| sK51 != app(X1,cons(X0,nil))
| ~ ssList(X1)
| ~ ssItem(X0) )
| ~ spl62_241 ),
inference(superposition,[],[f438,f2508]) ).
fof(f2628,plain,
( ! [X0,X1] :
( ~ lt(X0,sK58(sK51))
| ~ ssList(sK61(sK49,sK54(sK51),sK58(sK51)))
| ~ ssItem(sK58(sK51))
| sK51 != app(X1,cons(X0,nil))
| ~ ssList(X1)
| ~ ssItem(X0) )
| ~ spl62_241 ),
inference(trivial_inequality_removal,[],[f2626]) ).
fof(f2629,plain,
( ~ spl62_246
| ~ spl62_247
| spl62_271
| ~ spl62_241 ),
inference(avatar_split_clause,[],[f2628,f1415,f1687,f1453,f1449]) ).
fof(f2642,plain,
( sK51 != sK51
| ~ ssItem(sK54(sK51))
| ~ ssList(sK56(sK51))
| ~ lt(sK54(sK51),sK58(sK51))
| ~ spl62_258
| ~ spl62_271 ),
inference(superposition,[],[f1688,f1530]) ).
fof(f2643,plain,
( ~ ssItem(sK54(sK51))
| ~ ssList(sK56(sK51))
| ~ lt(sK54(sK51),sK58(sK51))
| ~ spl62_258
| ~ spl62_271 ),
inference(trivial_inequality_removal,[],[f2642]) ).
fof(f2644,plain,
( ~ spl62_270
| ~ spl62_260
| ~ spl62_257
| ~ spl62_258
| ~ spl62_271 ),
inference(avatar_split_clause,[],[f2643,f1687,f1528,f1519,f1563,f1673]) ).
fof(f2649,plain,
( ~ spl62_264
| ~ spl62_256
| ~ spl62_240
| ~ spl62_255
| ~ spl62_263 ),
inference(avatar_split_clause,[],[f2473,f1593,f1503,f1411,f1515,f1611]) ).
fof(f2650,plain,
( spl62_264
| spl62_258
| ~ spl62_242
| ~ spl62_243
| ~ spl62_21 ),
inference(avatar_split_clause,[],[f1642,f643,f1423,f1419,f1528,f1611]) ).
cnf(s1,plain,
( spl62_9
| ~ spl62_10
| ~ spl62_11 ),
inference(sat_conversion,[],[f609]) ).
cnf(s2,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_13 ),
inference(sat_conversion,[],[f616]) ).
cnf(s3,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_15 ),
inference(sat_conversion,[],[f623]) ).
cnf(s4,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_17 ),
inference(sat_conversion,[],[f630]) ).
cnf(s5,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_18 ),
inference(sat_conversion,[],[f634]) ).
cnf(s6,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_19 ),
inference(sat_conversion,[],[f638]) ).
cnf(s7,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_21 ),
inference(sat_conversion,[],[f645]) ).
cnf(s8,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_22 ),
inference(sat_conversion,[],[f649]) ).
cnf(s9,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_23 ),
inference(sat_conversion,[],[f653]) ).
cnf(s10,plain,
( spl62_9
| ~ spl62_10
| spl62_24 ),
inference(sat_conversion,[],[f658]) ).
cnf(s11,plain,
( ~ spl62_10
| spl62_13
| spl62_24 ),
inference(sat_conversion,[],[f659]) ).
cnf(s12,plain,
( ~ spl62_10
| spl62_15
| spl62_24 ),
inference(sat_conversion,[],[f660]) ).
cnf(s13,plain,
( ~ spl62_10
| spl62_17
| spl62_24 ),
inference(sat_conversion,[],[f661]) ).
cnf(s14,plain,
( ~ spl62_10
| spl62_18
| spl62_24 ),
inference(sat_conversion,[],[f662]) ).
cnf(s15,plain,
( ~ spl62_10
| spl62_19
| spl62_24 ),
inference(sat_conversion,[],[f663]) ).
cnf(s16,plain,
( ~ spl62_10
| spl62_21
| spl62_24 ),
inference(sat_conversion,[],[f664]) ).
cnf(s17,plain,
( ~ spl62_10
| spl62_22
| spl62_24 ),
inference(sat_conversion,[],[f665]) ).
cnf(s18,plain,
( ~ spl62_10
| spl62_23
| spl62_24 ),
inference(sat_conversion,[],[f666]) ).
cnf(s19,plain,
( ~ spl62_10
| spl62_24
| spl62_26 ),
inference(sat_conversion,[],[f673]) ).
cnf(s20,plain,
( ~ spl62_10
| spl62_24
| spl62_27 ),
inference(sat_conversion,[],[f677]) ).
cnf(s21,plain,
( ~ spl62_10
| spl62_24
| spl62_28 ),
inference(sat_conversion,[],[f681]) ).
cnf(s22,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_26 ),
inference(sat_conversion,[],[f682]) ).
cnf(s23,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_27 ),
inference(sat_conversion,[],[f683]) ).
cnf(s24,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_28 ),
inference(sat_conversion,[],[f684]) ).
cnf(s25,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_37 ),
inference(sat_conversion,[],[f712]) ).
cnf(s26,plain,
( ~ spl62_10
| spl62_24
| spl62_37 ),
inference(sat_conversion,[],[f713]) ).
cnf(s27,plain,
( ~ spl62_10
| spl62_24
| spl62_38 ),
inference(sat_conversion,[],[f717]) ).
cnf(s28,plain,
( ~ spl62_10
| spl62_24
| spl62_39 ),
inference(sat_conversion,[],[f721]) ).
cnf(s29,plain,
( ~ spl62_10
| spl62_24
| spl62_40 ),
inference(sat_conversion,[],[f725]) ).
cnf(s30,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_38 ),
inference(sat_conversion,[],[f726]) ).
cnf(s31,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_39 ),
inference(sat_conversion,[],[f727]) ).
cnf(s32,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_40 ),
inference(sat_conversion,[],[f728]) ).
cnf(s33,plain,
( ~ spl62_10
| spl62_24
| spl62_42 ),
inference(sat_conversion,[],[f735]) ).
cnf(s34,plain,
( ~ spl62_10
| spl62_24
| spl62_43 ),
inference(sat_conversion,[],[f739]) ).
cnf(s35,plain,
( ~ spl62_10
| spl62_24
| spl62_44 ),
inference(sat_conversion,[],[f743]) ).
cnf(s36,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_42 ),
inference(sat_conversion,[],[f744]) ).
cnf(s37,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_43 ),
inference(sat_conversion,[],[f745]) ).
cnf(s38,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_44 ),
inference(sat_conversion,[],[f746]) ).
cnf(s39,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_46 ),
inference(sat_conversion,[],[f753]) ).
cnf(s40,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_47 ),
inference(sat_conversion,[],[f757]) ).
cnf(s41,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_48 ),
inference(sat_conversion,[],[f761]) ).
cnf(s42,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_50 ),
inference(sat_conversion,[],[f768]) ).
cnf(s43,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_51 ),
inference(sat_conversion,[],[f772]) ).
cnf(s44,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_52 ),
inference(sat_conversion,[],[f776]) ).
cnf(s45,plain,
( ~ spl62_10
| spl62_24
| spl62_46 ),
inference(sat_conversion,[],[f777]) ).
cnf(s46,plain,
( ~ spl62_10
| spl62_24
| spl62_47 ),
inference(sat_conversion,[],[f778]) ).
cnf(s47,plain,
( ~ spl62_10
| spl62_24
| spl62_48 ),
inference(sat_conversion,[],[f779]) ).
cnf(s48,plain,
( ~ spl62_10
| spl62_24
| spl62_50 ),
inference(sat_conversion,[],[f780]) ).
cnf(s49,plain,
( ~ spl62_10
| spl62_24
| spl62_51 ),
inference(sat_conversion,[],[f781]) ).
cnf(s50,plain,
( ~ spl62_10
| spl62_24
| spl62_52 ),
inference(sat_conversion,[],[f782]) ).
cnf(s51,plain,
( ~ spl62_10
| spl62_24
| spl62_53 ),
inference(sat_conversion,[],[f786]) ).
cnf(s52,plain,
( ~ spl62_10
| spl62_24
| spl62_54 ),
inference(sat_conversion,[],[f790]) ).
cnf(s53,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_53 ),
inference(sat_conversion,[],[f791]) ).
cnf(s54,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_54 ),
inference(sat_conversion,[],[f792]) ).
cnf(s55,plain,
( ~ spl62_10
| ~ spl62_11
| spl62_55 ),
inference(sat_conversion,[],[f796]) ).
cnf(s56,plain,
( ~ spl62_10
| spl62_24
| spl62_55 ),
inference(sat_conversion,[],[f797]) ).
cnf(s57,plain,
( spl62_11
| ~ spl62_24 ),
inference(sat_conversion,[],[f798]) ).
cnf(s68,plain,
spl62_10,
inference(sat_conversion,[],[f1371]) ).
cnf(s83,plain,
( ~ spl62_18
| spl62_240
| spl62_241
| ~ spl62_242
| ~ spl62_243 ),
inference(sat_conversion,[],[f1426]) ).
cnf(s84,plain,
spl62_242,
inference(sat_conversion,[],[f1428]) ).
cnf(s85,plain,
spl62_243,
inference(sat_conversion,[],[f1430]) ).
cnf(s96,plain,
( ~ spl62_47
| spl62_241
| ~ spl62_242
| ~ spl62_243
| spl62_251 ),
inference(sat_conversion,[],[f1488]) ).
cnf(s101,plain,
( ~ spl62_37
| ~ spl62_242
| ~ spl62_243
| spl62_256
| spl62_257 ),
inference(sat_conversion,[],[f1522]) ).
cnf(s103,plain,
( ~ spl62_22
| spl62_240
| ~ spl62_242
| ~ spl62_243
| spl62_258 ),
inference(sat_conversion,[],[f1531]) ).
cnf(s111,plain,
( ~ spl62_40
| ~ spl62_242
| ~ spl62_243
| spl62_256
| spl62_260 ),
inference(sat_conversion,[],[f1581]) ).
cnf(s112,plain,
( ~ spl62_42
| ~ spl62_242
| ~ spl62_243
| spl62_252
| spl62_260 ),
inference(sat_conversion,[],[f1584]) ).
cnf(s113,plain,
( ~ spl62_50
| ~ spl62_242
| ~ spl62_243
| spl62_253
| spl62_260 ),
inference(sat_conversion,[],[f1587]) ).
cnf(s115,plain,
( ~ spl62_19
| spl62_241
| ~ spl62_242
| ~ spl62_243
| spl62_263 ),
inference(sat_conversion,[],[f1596]) ).
cnf(s116,plain,
( ~ spl62_13
| spl62_240
| ~ spl62_242
| ~ spl62_243
| spl62_260 ),
inference(sat_conversion,[],[f1599]) ).
cnf(s122,plain,
( ~ spl62_9
| ~ spl62_242
| ~ spl62_243
| spl62_260
| spl62_264 ),
inference(sat_conversion,[],[f1631]) ).
cnf(s123,plain,
( ~ spl62_17
| spl62_241
| ~ spl62_242
| ~ spl62_243
| spl62_264 ),
inference(sat_conversion,[],[f1636]) ).
cnf(s128,plain,
( ~ spl62_241
| spl62_246 ),
inference(sat_conversion,[],[f1678]) ).
cnf(s130,plain,
( ~ spl62_241
| spl62_270 ),
inference(sat_conversion,[],[f1682]) ).
cnf(s133,plain,
( ~ spl62_241
| spl62_247 ),
inference(sat_conversion,[],[f1694]) ).
cnf(s220,plain,
( ~ spl62_48
| ~ spl62_242
| ~ spl62_243
| spl62_251
| spl62_258 ),
inference(sat_conversion,[],[f2410]) ).
cnf(s239,plain,
( ~ spl62_43
| spl62_241
| ~ spl62_242
| ~ spl62_243
| spl62_252 ),
inference(sat_conversion,[],[f2469]) ).
cnf(s240,plain,
( ~ spl62_44
| ~ spl62_242
| ~ spl62_243
| spl62_252
| spl62_258 ),
inference(sat_conversion,[],[f2470]) ).
cnf(s241,plain,
( ~ spl62_51
| spl62_241
| ~ spl62_242
| ~ spl62_243
| spl62_253 ),
inference(sat_conversion,[],[f2471]) ).
cnf(s242,plain,
( ~ spl62_52
| ~ spl62_242
| ~ spl62_243
| spl62_253
| spl62_258 ),
inference(sat_conversion,[],[f2472]) ).
cnf(s246,plain,
( ~ spl62_39
| spl62_241
| ~ spl62_242
| ~ spl62_243
| spl62_256 ),
inference(sat_conversion,[],[f2478]) ).
cnf(s247,plain,
( ~ spl62_38
| ~ spl62_242
| ~ spl62_243
| spl62_256
| spl62_258 ),
inference(sat_conversion,[],[f2479]) ).
cnf(s257,plain,
( ~ spl62_55
| ~ spl62_242
| ~ spl62_243
| spl62_252
| spl62_257 ),
inference(sat_conversion,[],[f2549]) ).
cnf(s258,plain,
( ~ spl62_53
| ~ spl62_242
| ~ spl62_243
| spl62_253
| spl62_257 ),
inference(sat_conversion,[],[f2550]) ).
cnf(s265,plain,
( ~ spl62_26
| ~ spl62_242
| ~ spl62_243
| spl62_257
| spl62_264 ),
inference(sat_conversion,[],[f2570]) ).
cnf(s271,plain,
( ~ spl62_27
| spl62_240
| ~ spl62_242
| ~ spl62_243
| spl62_257 ),
inference(sat_conversion,[],[f2587]) ).
cnf(s280,plain,
( ~ spl62_46
| ~ spl62_242
| ~ spl62_243
| spl62_251
| spl62_260 ),
inference(sat_conversion,[],[f2613]) ).
cnf(s281,plain,
( ~ spl62_54
| ~ spl62_242
| ~ spl62_243
| spl62_251
| spl62_257 ),
inference(sat_conversion,[],[f2614]) ).
cnf(s282,plain,
( ~ spl62_23
| ~ spl62_242
| ~ spl62_243
| spl62_258
| spl62_263 ),
inference(sat_conversion,[],[f2615]) ).
cnf(s283,plain,
( ~ spl62_28
| ~ spl62_242
| ~ spl62_243
| spl62_257
| spl62_263 ),
inference(sat_conversion,[],[f2616]) ).
cnf(s284,plain,
( ~ spl62_15
| ~ spl62_242
| ~ spl62_243
| spl62_260
| spl62_263 ),
inference(sat_conversion,[],[f2617]) ).
cnf(s285,plain,
( ~ spl62_251
| ~ spl62_252
| ~ spl62_253
| spl62_255 ),
inference(sat_conversion,[],[f2621]) ).
cnf(s288,plain,
( ~ spl62_241
| ~ spl62_246
| ~ spl62_247
| spl62_271 ),
inference(sat_conversion,[],[f2629]) ).
cnf(s293,plain,
( ~ spl62_257
| ~ spl62_258
| ~ spl62_260
| ~ spl62_270
| ~ spl62_271 ),
inference(sat_conversion,[],[f2644]) ).
cnf(s297,plain,
( ~ spl62_240
| ~ spl62_255
| ~ spl62_256
| ~ spl62_263
| ~ spl62_264 ),
inference(sat_conversion,[],[f2649]) ).
cnf(s298,plain,
( ~ spl62_21
| ~ spl62_242
| ~ spl62_243
| spl62_258
| spl62_264 ),
inference(sat_conversion,[],[f2650]) ).
cnf(s299,plain,
( ~ spl62_18
| spl62_240
| spl62_241 ),
inference(rat,[],[s83,s85,s84]) ).
cnf(s312,plain,
( spl62_24
| spl62_55 ),
inference(rat,[],[s56,s68]) ).
cnf(s313,plain,
( ~ spl62_11
| spl62_55 ),
inference(rat,[],[s55,s68]) ).
cnf(s314,plain,
( ~ spl62_11
| spl62_54 ),
inference(rat,[],[s54,s68]) ).
cnf(s315,plain,
( ~ spl62_11
| spl62_53 ),
inference(rat,[],[s53,s68]) ).
cnf(s316,plain,
( spl62_24
| spl62_54 ),
inference(rat,[],[s52,s68]) ).
cnf(s317,plain,
( spl62_24
| spl62_53 ),
inference(rat,[],[s51,s68]) ).
cnf(s318,plain,
( spl62_24
| spl62_52 ),
inference(rat,[],[s50,s68]) ).
cnf(s319,plain,
( spl62_24
| spl62_51 ),
inference(rat,[],[s49,s68]) ).
cnf(s320,plain,
( spl62_24
| spl62_50 ),
inference(rat,[],[s48,s68]) ).
cnf(s321,plain,
( spl62_24
| spl62_48 ),
inference(rat,[],[s47,s68]) ).
cnf(s322,plain,
( spl62_24
| spl62_47 ),
inference(rat,[],[s46,s68]) ).
cnf(s323,plain,
( spl62_24
| spl62_46 ),
inference(rat,[],[s45,s68]) ).
cnf(s324,plain,
( ~ spl62_11
| spl62_52 ),
inference(rat,[],[s44,s68]) ).
cnf(s325,plain,
( ~ spl62_11
| spl62_51 ),
inference(rat,[],[s43,s68]) ).
cnf(s326,plain,
( ~ spl62_11
| spl62_50 ),
inference(rat,[],[s42,s68]) ).
cnf(s327,plain,
( ~ spl62_11
| spl62_48 ),
inference(rat,[],[s41,s68]) ).
cnf(s328,plain,
( ~ spl62_11
| spl62_47 ),
inference(rat,[],[s40,s68]) ).
cnf(s329,plain,
( ~ spl62_11
| spl62_46 ),
inference(rat,[],[s39,s68]) ).
cnf(s330,plain,
( ~ spl62_11
| spl62_44 ),
inference(rat,[],[s38,s68]) ).
cnf(s331,plain,
( ~ spl62_11
| spl62_43 ),
inference(rat,[],[s37,s68]) ).
cnf(s332,plain,
( ~ spl62_11
| spl62_42 ),
inference(rat,[],[s36,s68]) ).
cnf(s333,plain,
( spl62_24
| spl62_44 ),
inference(rat,[],[s35,s68]) ).
cnf(s334,plain,
( spl62_24
| spl62_43 ),
inference(rat,[],[s34,s68]) ).
cnf(s335,plain,
( spl62_24
| spl62_42 ),
inference(rat,[],[s33,s68]) ).
cnf(s336,plain,
( ~ spl62_11
| spl62_40 ),
inference(rat,[],[s32,s68]) ).
cnf(s337,plain,
( ~ spl62_11
| spl62_39 ),
inference(rat,[],[s31,s68]) ).
cnf(s338,plain,
( ~ spl62_11
| spl62_38 ),
inference(rat,[],[s30,s68]) ).
cnf(s339,plain,
( spl62_24
| spl62_40 ),
inference(rat,[],[s29,s68]) ).
cnf(s340,plain,
( spl62_24
| spl62_39 ),
inference(rat,[],[s28,s68]) ).
cnf(s341,plain,
( spl62_24
| spl62_38 ),
inference(rat,[],[s27,s68]) ).
cnf(s342,plain,
( spl62_24
| spl62_37 ),
inference(rat,[],[s26,s68]) ).
cnf(s343,plain,
( ~ spl62_11
| spl62_37 ),
inference(rat,[],[s25,s68]) ).
cnf(s344,plain,
( ~ spl62_11
| spl62_28 ),
inference(rat,[],[s24,s68]) ).
cnf(s345,plain,
( ~ spl62_11
| spl62_27 ),
inference(rat,[],[s23,s68]) ).
cnf(s346,plain,
( ~ spl62_11
| spl62_26 ),
inference(rat,[],[s22,s68]) ).
cnf(s347,plain,
( spl62_24
| spl62_28 ),
inference(rat,[],[s21,s68]) ).
cnf(s348,plain,
( spl62_24
| spl62_27 ),
inference(rat,[],[s20,s68]) ).
cnf(s349,plain,
( spl62_24
| spl62_26 ),
inference(rat,[],[s19,s68]) ).
cnf(s350,plain,
( spl62_23
| spl62_24 ),
inference(rat,[],[s18,s68]) ).
cnf(s351,plain,
( spl62_22
| spl62_24 ),
inference(rat,[],[s17,s68]) ).
cnf(s352,plain,
( spl62_21
| spl62_24 ),
inference(rat,[],[s16,s68]) ).
cnf(s353,plain,
( spl62_19
| spl62_24 ),
inference(rat,[],[s15,s68]) ).
cnf(s354,plain,
( spl62_18
| spl62_24 ),
inference(rat,[],[s14,s68]) ).
cnf(s355,plain,
( spl62_17
| spl62_24 ),
inference(rat,[],[s13,s68]) ).
cnf(s356,plain,
( spl62_15
| spl62_24 ),
inference(rat,[],[s12,s68]) ).
cnf(s357,plain,
( spl62_13
| spl62_24 ),
inference(rat,[],[s11,s68]) ).
cnf(s358,plain,
( spl62_9
| spl62_24 ),
inference(rat,[],[s10,s68]) ).
cnf(s359,plain,
( ~ spl62_11
| spl62_23 ),
inference(rat,[],[s9,s68]) ).
cnf(s360,plain,
( ~ spl62_11
| spl62_22 ),
inference(rat,[],[s8,s68]) ).
cnf(s361,plain,
( ~ spl62_11
| spl62_21 ),
inference(rat,[],[s7,s68]) ).
cnf(s362,plain,
( ~ spl62_11
| spl62_19 ),
inference(rat,[],[s6,s68]) ).
cnf(s363,plain,
( ~ spl62_11
| spl62_18 ),
inference(rat,[],[s5,s68]) ).
cnf(s364,plain,
( ~ spl62_11
| spl62_17 ),
inference(rat,[],[s4,s68]) ).
cnf(s365,plain,
( ~ spl62_11
| spl62_15 ),
inference(rat,[],[s3,s68]) ).
cnf(s366,plain,
( ~ spl62_11
| spl62_13 ),
inference(rat,[],[s2,s68]) ).
cnf(s367,plain,
( spl62_9
| ~ spl62_11 ),
inference(rat,[],[s1,s68]) ).
cnf(s368,plain,
spl62_9,
inference(rat,[],[s57,s367,s358]) ).
cnf(s369,plain,
( spl62_240
| spl62_24 ),
inference(rat,[],[s288,s293,s128,s130,s133,s299,s103,s116,s271,s348,s351,s354,s357,s84,s85]) ).
cnf(s370,plain,
( spl62_260
| spl62_24 ),
inference(rat,[],[s297,s285,s111,s112,s280,s113,s122,s284,s320,s323,s335,s339,s356,s369,s85,s84,s368]) ).
cnf(s371,plain,
( spl62_258
| spl62_24 ),
inference(rat,[],[s297,s285,s247,s240,s220,s242,s282,s298,s318,s321,s333,s341,s350,s352,s369,s85,s84]) ).
cnf(s372,plain,
( spl62_257
| spl62_24 ),
inference(rat,[],[s297,s285,s101,s258,s281,s257,s265,s283,s312,s316,s317,s342,s347,s349,s369,s85,s84]) ).
cnf(s373,plain,
( ~ spl62_241
| spl62_24 ),
inference(rat,[],[s288,s293,s128,s130,s133,s370,s371,s372]) ).
cnf(s374,plain,
spl62_24,
inference(rat,[],[s297,s285,s123,s115,s246,s239,s96,s241,s373,s369,s355,s353,s340,s334,s322,s319,s84,s85]) ).
cnf(s375,plain,
spl62_11,
inference(rat,[],[s57,s374]) ).
cnf(s376,plain,
spl62_55,
inference(rat,[],[s313,s375]) ).
cnf(s377,plain,
spl62_54,
inference(rat,[],[s314,s375]) ).
cnf(s378,plain,
spl62_53,
inference(rat,[],[s315,s375]) ).
cnf(s379,plain,
spl62_52,
inference(rat,[],[s324,s375]) ).
cnf(s380,plain,
spl62_51,
inference(rat,[],[s325,s375]) ).
cnf(s381,plain,
spl62_50,
inference(rat,[],[s326,s375]) ).
cnf(s382,plain,
spl62_48,
inference(rat,[],[s327,s375]) ).
cnf(s383,plain,
spl62_47,
inference(rat,[],[s328,s375]) ).
cnf(s384,plain,
spl62_46,
inference(rat,[],[s329,s375]) ).
cnf(s385,plain,
spl62_44,
inference(rat,[],[s330,s375]) ).
cnf(s386,plain,
spl62_43,
inference(rat,[],[s331,s375]) ).
cnf(s387,plain,
spl62_42,
inference(rat,[],[s332,s375]) ).
cnf(s388,plain,
spl62_40,
inference(rat,[],[s336,s375]) ).
cnf(s389,plain,
spl62_39,
inference(rat,[],[s337,s375]) ).
cnf(s390,plain,
spl62_38,
inference(rat,[],[s338,s375]) ).
cnf(s391,plain,
spl62_37,
inference(rat,[],[s343,s375]) ).
cnf(s392,plain,
spl62_28,
inference(rat,[],[s344,s375]) ).
cnf(s393,plain,
spl62_27,
inference(rat,[],[s345,s375]) ).
cnf(s394,plain,
spl62_26,
inference(rat,[],[s346,s375]) ).
cnf(s395,plain,
spl62_23,
inference(rat,[],[s359,s375]) ).
cnf(s396,plain,
spl62_22,
inference(rat,[],[s360,s375]) ).
cnf(s397,plain,
spl62_21,
inference(rat,[],[s361,s375]) ).
cnf(s398,plain,
spl62_19,
inference(rat,[],[s362,s375]) ).
cnf(s399,plain,
spl62_18,
inference(rat,[],[s363,s375]) ).
cnf(s400,plain,
spl62_17,
inference(rat,[],[s364,s375]) ).
cnf(s401,plain,
spl62_15,
inference(rat,[],[s365,s375]) ).
cnf(s402,plain,
spl62_13,
inference(rat,[],[s366,s375]) ).
cnf(s403,plain,
spl62_260,
inference(rat,[],[s297,s285,s116,s111,s112,s280,s113,s122,s284,s84,s85,s402,s388,s387,s384,s381,s368,s401]) ).
cnf(s404,plain,
spl62_258,
inference(rat,[],[s297,s285,s247,s103,s240,s220,s242,s282,s298,s85,s84,s390,s396,s385,s382,s379,s395,s397]) ).
cnf(s409,plain,
spl62_257,
inference(rat,[],[s297,s285,s101,s271,s258,s281,s257,s265,s283,s85,s84,s391,s393,s378,s377,s376,s394,s392]) ).
cnf(s411,plain,
~ spl62_241,
inference(rat,[],[s288,s293,s128,s130,s133,s404,s409,s403]) ).
cnf(s412,plain,
spl62_253,
inference(rat,[],[s241,s380,s85,s84,s411]) ).
cnf(s413,plain,
spl62_251,
inference(rat,[],[s96,s383,s85,s84,s411]) ).
cnf(s414,plain,
spl62_252,
inference(rat,[],[s239,s386,s85,s84,s411]) ).
cnf(s415,plain,
spl62_256,
inference(rat,[],[s246,s389,s85,s84,s411]) ).
cnf(s416,plain,
spl62_263,
inference(rat,[],[s115,s398,s85,s84,s411]) ).
cnf(s417,plain,
spl62_240,
inference(rat,[],[s299,s399,s411]) ).
cnf(s418,plain,
spl62_264,
inference(rat,[],[s123,s400,s85,s84,s411]) ).
cnf(s422,plain,
spl62_255,
inference(rat,[],[s285,s413,s412,s414]) ).
cnf(s423,plain,
$false,
inference(rat,[],[s297,s418,s416,s417,s415,s422]) ).
fof(f2651,plain,
$false,
inference(avatar_sat_refutation,[],[s423]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC344+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.18 % Computer : n010.cluster.edu
% 0.10/0.18 % Model : x86_64 x86_64
% 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.18 % Memory : 8046.5625MB
% 0.10/0.18 % OS : Linux 6.8.0-71-generic
% 0.10/0.18 % CPULimit : 300
% 0.10/0.18 % WCLimit : 300
% 0.10/0.18 % DateTime : Mon Sep 28 09:12:02 UTC 2026
% 0.10/0.18 % CPUTime :
% 0.10/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.21 Running first-order model finding
% 0.10/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.39/0.91 % (1791590)Will run a generic schedule for satisfiability detection.
% 4.39/0.91 % (1791599)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1399882688:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.39/0.91 % (1791596)% WARNING: option uhcvi not known.
% 4.39/0.91 % (1791595)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3192986744_2999 on theBenchmark for (2999ds/0Mi)
% 4.39/0.91 % (1791596)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=10449930:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.39/0.91 % (1791597)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3448996474:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.39/0.91 % (1791598)dis+10_1_sil=32000:sp=arity:random_seed=184414100:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.39/0.91 % (1791600)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4219171001:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.39/0.91 % (1791601)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4267173857:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.39/0.91 % TRYING [1]
% 4.39/0.91 % TRYING [2]
% 4.39/0.91 % TRYING [3]
% 4.39/0.91 % (1791599)Instruction limit reached!
% 4.39/0.91 % (1791599)------------------------------
% 4.39/0.91 % (1791599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.39/0.91 % (1791599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.39/0.91 % (1791599)CaDiCaL version: 2.1.3
% 4.39/0.91 % (1791599)Termination reason: Instruction limit
% 4.39/0.91 % (1791599)Termination phase: Saturation
% 4.39/0.91 % (1791599)Time elapsed: 0.033 s
% 4.39/0.91 % (1791599)Peak memory usage: 13 MB
% 4.39/0.91 % (1791599)Instructions burned: 119 (million)
% 4.39/0.91 % (1791609)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4116751628:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.39/0.91 % TRYING [4]
% 4.39/0.91 % TRYING [1]
% 4.39/0.91 % TRYING [2]
% 4.39/0.91 % TRYING [3]
% 4.39/0.91 % (1791598)Instruction limit reached!
% 4.39/0.91 % (1791598)------------------------------
% 4.39/0.91 % (1791598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.39/0.91 % (1791598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.39/0.91 % (1791598)CaDiCaL version: 2.1.3
% 4.39/0.91 % (1791598)Termination reason: Instruction limit
% 4.39/0.91 % (1791598)Termination phase: Saturation
% 4.39/0.91 % (1791598)Time elapsed: 0.058 s
% 4.39/0.91 % (1791598)Peak memory usage: 13 MB
% 4.39/0.91 % (1791598)Instructions burned: 103 (million)
% 4.39/0.91 % TRYING [4]
% 4.39/0.91 % (1791600)Instruction limit reached!
% 4.39/0.91 % (1791600)------------------------------
% 4.39/0.91 % (1791600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.39/0.91 % (1791600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.39/0.91 % (1791600)CaDiCaL version: 2.1.3
% 4.39/0.91 % (1791600)Termination reason: Instruction limit
% 4.39/0.91 % (1791600)Termination phase: Saturation
% 4.39/0.91 % (1791600)Time elapsed: 0.076 s
% 4.39/0.91 % (1791600)Peak memory usage: 13 MB
% 4.39/0.91 % (1791600)Instructions burned: 131 (million)
% 4.39/0.91 % (1791611)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1337409348:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.39/0.91 % (1791601)Instruction limit reached!
% 4.39/0.91 % (1791601)------------------------------
% 4.39/0.91 % (1791601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.39/0.91 % (1791601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.39/0.91 % (1791601)CaDiCaL version: 2.1.3
% 4.39/0.91 % (1791601)Termination reason: Instruction limit
% 4.39/0.91 % (1791601)Termination phase: Saturation
% 4.39/0.91 % (1791601)Time elapsed: 0.084 s
% 4.39/0.91 % (1791601)Peak memory usage: 14 MB
% 4.39/0.91 % (1791601)Instructions burned: 160 (million)
% 4.39/0.91 % TRYING [5]
% 4.39/0.91 % (1791612)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2473801715:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 4.39/0.91 % TRYING [5]
% 4.39/0.91 % (1791614)ott-21_1_sil=16000:fs=off:random_seed=4019653152:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.39/0.91 % (1791611)Instruction limit reached!
% 4.39/0.91 % (1791611)------------------------------
% 4.39/0.91 % (1791611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.39/0.91 % (1791611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.39/0.91 % (1791611)CaDiCaL version: 2.1.3
% 4.39/0.91 % (1791611)Termination reason: Instruction limit
% 4.39/0.91 % (1791611)Termination phase: Saturation
% 4.39/0.91 % (1791611)Time elapsed: 0.073 s
% 4.39/0.91 % (1791611)Peak memory usage: 13 MB
% 4.39/0.91 % (1791611)Instructions burned: 131 (million)
% 4.39/0.91 % (1791617)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1553362433:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 4.39/0.91 % (1791614)Instruction limit reached!
% 4.39/0.91 % (1791614)------------------------------
% 4.39/0.91 % (1791614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.39/0.91 % (1791614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.39/0.91 % (1791614)CaDiCaL version: 2.1.3
% 4.39/0.91 % (1791614)Termination reason: Instruction limit
% 4.39/0.91 % (1791614)Termination phase: Saturation
% 4.39/0.91 % (1791614)Time elapsed: 0.088 s
% 4.39/0.91 % (1791614)Peak memory usage: 14 MB
% 4.39/0.91 % (1791614)Instructions burned: 181 (million)
% 4.39/0.91 % TRYING [6]
% 4.39/0.91 % (1791609)Instruction limit reached!
% 4.39/0.91 % (1791609)------------------------------
% 4.39/0.91 % (1791609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.39/0.91 % (1791609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.39/0.91 % (1791609)CaDiCaL version: 2.1.3
% 4.39/0.91 % (1791609)Termination reason: Instruction limit
% 4.39/0.91 % (1791609)Termination phase: Finite model building constraint generation
% 4.39/0.91 % (1791609)Time elapsed: 0.165 s
% 4.39/0.91 % (1791609)Peak memory usage: 31 MB
% 4.39/0.91 % (1791609)Instructions burned: 715 (million)
% 4.39/0.91 % (1791619)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1795276159:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 4.39/0.91 % (1791620)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4134323220:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 4.39/0.91 % TRYING [1]
% 4.39/0.91 % TRYING [2]
% 4.39/0.91 % TRYING [3]
% 4.39/0.91 % TRYING [6]
% 4.39/0.91 % TRYING [4]
% 4.39/0.91 % TRYING [5]
% 4.39/0.91 % (1791612)Instruction limit reached!
% 4.39/0.91 % (1791612)------------------------------
% 4.39/0.91 % (1791612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.39/0.91 % (1791612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.39/0.91 % (1791612)CaDiCaL version: 2.1.3
% 4.39/0.91 % (1791612)Termination reason: Instruction limit
% 4.39/0.91 % (1791612)Termination phase: Saturation
% 4.39/0.91 % (1791612)Time elapsed: 0.361 s
% 4.39/0.91 % (1791612)Peak memory usage: 21 MB
% 4.39/0.91 % (1791612)Instructions burned: 685 (million)
% 4.39/0.91 % (1791623)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3972964980:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 4.39/0.91 % (1791617)Instruction limit reached!
% 4.39/0.91 % (1791617)------------------------------
% 4.39/0.91 % (1791617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.39/0.91 % (1791617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.39/0.91 % (1791617)CaDiCaL version: 2.1.3
% 4.39/0.91 % (1791617)Termination reason: Instruction limit
% 4.39/0.91 % (1791617)Termination phase: Saturation
% 4.39/0.91 % (1791617)Time elapsed: 0.314 s
% 4.39/0.91 % (1791617)Peak memory usage: 14 MB
% 4.39/0.91 % (1791617)Instructions burned: 477 (million)
% 4.39/0.91 % (1791625)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3611915492:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 4.39/0.91 % (1791619)Instruction limit reached!
% 4.39/0.91 % (1791619)------------------------------
% 4.39/0.91 % (1791619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.39/0.91 % (1791619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.39/0.91 % (1791619)CaDiCaL version: 2.1.3
% 4.39/0.91 % (1791619)Termination reason: Instruction limit
% 4.39/0.91 % (1791619)Termination phase: Finite model building SAT solving
% 4.39/0.91 % (1791619)Time elapsed: 0.351 s
% 4.39/0.91 % (1791619)Peak memory usage: 23 MB
% 4.39/0.91 % (1791619)Instructions burned: 865 (million)
% 4.39/0.91 % TRYING [7]
% 4.39/0.91 % (1791627)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1169857936:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 4.39/0.91 % TRYING [14]
% 4.39/0.91 % (1791620)Instruction limit reached!
% 4.39/0.91 % (1791620)------------------------------
% 4.39/0.91 % (1791620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.39/0.91 % (1791620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.39/0.91 % (1791620)CaDiCaL version: 2.1.3
% 4.39/0.91 % (1791620)Termination reason: Instruction limit
% 4.39/0.91 % (1791620)Termination phase: Saturation
% 4.39/0.91 % (1791620)Time elapsed: 0.386 s
% 4.39/0.91 % (1791620)Peak memory usage: 26 MB
% 4.39/0.91 % (1791620)Instructions burned: 1182 (million)
% 4.39/0.91 % (1791629)fmb+10_1_sil=64000:random_seed=1485409759:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 4.39/0.91 % TRYING [1]
% 4.39/0.91 % (1791627) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1791590-1791627"...
% 4.39/0.91 % TRYING [2]
% 4.39/0.91 % (1791627)...printing done.
% 4.39/0.91 % TRYING [3]
% 4.39/0.91 % (1791627)Refutation found. Thanks to Tanya!
% 4.39/0.91 % SZS status Theorem for theBenchmark
% 4.39/0.91 % SZS output start Proof for theBenchmark
% See solution above
% 4.39/0.92 % (1791627)------------------------------
% 4.39/0.92 % (1791627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.39/0.92 % (1791627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.39/0.92 % (1791627)CaDiCaL version: 2.1.3
% 4.39/0.92 % (1791627)Termination reason: Refutation
% 4.39/0.92 % (1791627)Time elapsed: 0.052 s
% 4.39/0.92 % (1791627)Peak memory usage: 13 MB
% 4.39/0.92 % (1791627)Instructions burned: 93 (million)
% 4.39/0.92 % (1791590)Success in time 0.691 s
% 4.39/0.92 % Vampire exiting
%------------------------------------------------------------------------------