%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWC283+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:03:16 PM UTC 2026
% Result : Theorem 12.63s 2.43s
% Output : Refutation 13.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 38
% Syntax : Number of formulae : 278 ( 46 unt; 28 def)
% Number of atoms : 1189 ( 100 equ)
% Maximal formula atoms : 27 ( 4 avg)
% Number of connectives : 1663 ( 752 ~; 719 |; 114 &)
% ( 37 <=>; 41 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 36 ( 34 usr; 29 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 10 con; 0-2 aty)
% Number of variables : 281 ( 0 sgn 237 !; 44 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> ( memberP(X0,X1)
<=> ? [X2] :
( ssList(X2)
& ? [X3] :
( ssList(X3)
& app(X2,cons(X1,X3)) = X0 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f12,axiom,
! [X0] :
( ssList(X0)
=> ( strictorderedP(X0)
<=> ! [X1] :
( ssItem(X1)
=> ! [X2] :
( ssItem(X2)
=> ! [X3] :
( ssList(X3)
=> ! [X4] :
( ssList(X4)
=> ! [X5] :
( ssList(X5)
=> ( app(app(X3,cons(X1,X4)),cons(X2,X5)) = X0
=> lt(X1,X2) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f16,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> ssList(cons(X1,X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f26,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ssList(app(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax26) ).
fof(f36,axiom,
! [X0] :
( ssItem(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ( memberP(app(X1,X2),X0)
<=> ( memberP(X1,X0)
| memberP(X2,X0) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax36) ).
fof(f81,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> cons(X1,X0) = app(cons(X1,nil),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax81) ).
fof(f82,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> app(app(X0,X1),X2) = app(X0,app(X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax82) ).
fof(f93,axiom,
! [X0] :
( ssItem(X0)
=> ! [X1] :
( ssItem(X1)
=> ( lt(X0,X1)
<=> ( X0 != X1
& leq(X0,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax93) ).
fof(f96,conjecture,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ( X1 != X3
| X0 != X2
| ! [X4] :
( ssList(X4)
=> ( app(X2,X4) != X3
| ~ strictorderedP(X2)
| ? [X5] :
( ssItem(X5)
& ? [X6] :
( ssList(X6)
& app(cons(X5,nil),X6) = X4
& ? [X7] :
( ssItem(X7)
& ? [X8] :
( ssList(X8)
& app(X8,cons(X7,nil)) = X2
& lt(X7,X5) ) ) ) ) ) )
| ! [X9] :
( ssItem(X9)
=> ! [X10] :
( ssList(X10)
=> ! [X11] :
( ssList(X11)
=> ( app(app(X10,cons(X9,nil)),X11) != X0
| ! [X12] :
( ssItem(X12)
=> ( ( ~ memberP(X10,X12)
| leq(X12,X9) )
& ( ~ memberP(X11,X12)
| leq(X9,X12) ) ) ) ) ) ) )
| ( nil != X3
& nil = X2 ) ) ) ) ) ),
file('/export/starexec/sandbox/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)
=> ( app(X2,X4) != X3
| ~ strictorderedP(X2)
| ? [X5] :
( ssItem(X5)
& ? [X6] :
( ssList(X6)
& app(cons(X5,nil),X6) = X4
& ? [X7] :
( ssItem(X7)
& ? [X8] :
( ssList(X8)
& app(X8,cons(X7,nil)) = X2
& lt(X7,X5) ) ) ) ) ) )
| ! [X9] :
( ssItem(X9)
=> ! [X10] :
( ssList(X10)
=> ! [X11] :
( ssList(X11)
=> ( app(app(X10,cons(X9,nil)),X11) != X0
| ! [X12] :
( ssItem(X12)
=> ( ( ~ memberP(X10,X12)
| leq(X12,X9) )
& ( ~ memberP(X11,X12)
| leq(X9,X12) ) ) ) ) ) ) )
| ( nil != X3
& nil = X2 ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f98,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( X1 = X3
& X0 = X2
& ? [X4] :
( app(X2,X4) = X3
& strictorderedP(X2)
& ! [X5] :
( ~ ssItem(X5)
| ! [X6] :
( ~ ssList(X6)
| app(cons(X5,nil),X6) != X4
| ! [X7] :
( ~ ssItem(X7)
| ! [X8] :
( ~ ssList(X8)
| app(X8,cons(X7,nil)) != X2
| ~ lt(X7,X5) ) ) ) )
& ssList(X4) )
& ? [X9] :
( ? [X10] :
( ? [X11] :
( app(app(X10,cons(X9,nil)),X11) = X0
& ? [X12] :
( ( ( memberP(X10,X12)
& ~ leq(X12,X9) )
| ( memberP(X11,X12)
& ~ leq(X9,X12) ) )
& ssItem(X12) )
& ssList(X11) )
& ssList(X10) )
& ssItem(X9) )
& ( nil = X3
| nil != X2 )
& ssList(X3) )
& ssList(X2) )
& ssList(X1) )
& ssList(X0) ),
inference(ennf_transformation,[],[f97]) ).
fof(f99,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( X1 = X3
& X0 = X2
& ? [X4] :
( app(X2,X4) = X3
& strictorderedP(X2)
& ! [X5] :
( ~ ssItem(X5)
| ! [X6] :
( ~ ssList(X6)
| app(cons(X5,nil),X6) != X4
| ! [X7] :
( ~ ssItem(X7)
| ! [X8] :
( ~ ssList(X8)
| app(X8,cons(X7,nil)) != X2
| ~ lt(X7,X5) ) ) ) )
& ssList(X4) )
& ? [X9] :
( ? [X10] :
( ? [X11] :
( app(app(X10,cons(X9,nil)),X11) = X0
& ? [X12] :
( ( ( memberP(X10,X12)
& ~ leq(X12,X9) )
| ( memberP(X11,X12)
& ~ leq(X9,X12) ) )
& ssItem(X12) )
& ssList(X11) )
& ssList(X10) )
& ssItem(X9) )
& ( nil = X3
| nil != X2 )
& ssList(X3) )
& ssList(X2) )
& ssList(X1) )
& ssList(X0) ),
inference(flattening,[],[f98]) ).
fof(f106,plain,
! [X0] :
( ! [X1] :
( ssList(cons(X1,X0))
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f109,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( app(app(X0,X1),X2) = app(X0,app(X1,X2))
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f82]) ).
fof(f110,plain,
! [X0] :
( ! [X1] :
( cons(X1,X0) = app(cons(X1,nil),X0)
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f81]) ).
fof(f117,plain,
! [X0] :
( ! [X1] :
( ssList(app(X0,X1))
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f120,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( memberP(app(X1,X2),X0)
<=> ( memberP(X1,X0)
| memberP(X2,X0) ) )
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f36]) ).
fof(f121,plain,
! [X0] :
( ! [X1] :
( ( memberP(X0,X1)
<=> ? [X2] :
( ssList(X2)
& ? [X3] :
( ssList(X3)
& app(X2,cons(X1,X3)) = X0 ) ) )
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f127,plain,
! [X0] :
( ! [X1] :
( ( lt(X0,X1)
<=> ( X0 != X1
& leq(X0,X1) ) )
| ~ ssItem(X1) )
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f93]) ).
fof(f139,plain,
! [X0] :
( ( strictorderedP(X0)
<=> ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( lt(X1,X2)
| app(app(X3,cons(X1,X4)),cons(X2,X5)) != X0
| ~ ssList(X5) )
| ~ ssList(X4) )
| ~ ssList(X3) )
| ~ ssItem(X2) )
| ~ ssItem(X1) ) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f140,plain,
! [X0] :
( ( strictorderedP(X0)
<=> ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( lt(X1,X2)
| app(app(X3,cons(X1,X4)),cons(X2,X5)) != X0
| ~ ssList(X5) )
| ~ ssList(X4) )
| ~ ssList(X3) )
| ~ ssItem(X2) )
| ~ ssItem(X1) ) )
| ~ ssList(X0) ),
inference(flattening,[],[f139]) ).
fof(f141,plain,
( sK1 = sK3
& sK0 = sK2
& sK3 = app(sK2,sK4)
& strictorderedP(sK2)
& ! [X5] :
( ~ ssItem(X5)
| ! [X6] :
( ~ ssList(X6)
| app(cons(X5,nil),X6) != sK4
| ! [X7] :
( ~ ssItem(X7)
| ! [X8] :
( ~ ssList(X8)
| app(X8,cons(X7,nil)) != sK2
| ~ lt(X7,X5) ) ) ) )
& ssList(sK4)
& sK0 = app(app(sK6,cons(sK5,nil)),sK7)
& ( ( memberP(sK6,sK8)
& ~ leq(sK8,sK5) )
| ( memberP(sK7,sK8)
& ~ leq(sK5,sK8) ) )
& ssItem(sK8)
& ssList(sK7)
& ssList(sK6)
& ssItem(sK5)
& ( nil = sK3
| nil != sK2 )
& ssList(sK3)
& ssList(sK2)
& ssList(sK1)
& ssList(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X9,sK5),skolemize(X10,sK6),skolemize(X11,sK7),skolemize(X12,sK8)],[f99]) ).
fof(f148,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( memberP(app(X1,X2),X0)
| ( ~ memberP(X1,X0)
& ~ memberP(X2,X0) ) )
& ( memberP(X1,X0)
| memberP(X2,X0)
| ~ memberP(app(X1,X2),X0) ) )
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssItem(X0) ),
inference(nnf_transformation,[],[f120]) ).
fof(f149,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( memberP(app(X1,X2),X0)
| ( ~ memberP(X1,X0)
& ~ memberP(X2,X0) ) )
& ( memberP(X1,X0)
| memberP(X2,X0)
| ~ memberP(app(X1,X2),X0) ) )
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssItem(X0) ),
inference(flattening,[],[f148]) ).
fof(f150,plain,
! [X0] :
( ! [X1] :
( ( ( memberP(X0,X1)
| ! [X2] :
( ~ ssList(X2)
| ! [X3] :
( ~ ssList(X3)
| app(X2,cons(X1,X3)) != X0 ) ) )
& ( ? [X2] :
( ssList(X2)
& ? [X3] :
( ssList(X3)
& app(X2,cons(X1,X3)) = X0 ) )
| ~ memberP(X0,X1) ) )
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(nnf_transformation,[],[f121]) ).
fof(f151,plain,
! [X0] :
( ! [X1] :
( ( ( memberP(X0,X1)
| ! [X2] :
( ~ ssList(X2)
| ! [X3] :
( ~ ssList(X3)
| app(X2,cons(X1,X3)) != X0 ) ) )
& ( ? [X4] :
( ssList(X4)
& ? [X5] :
( ssList(X5)
& app(X4,cons(X1,X5)) = X0 ) )
| ~ memberP(X0,X1) ) )
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(rectify,[],[f150]) ).
fof(f152,plain,
! [X0] :
( ! [X1] :
( ( ( memberP(X0,X1)
| ! [X2] :
( ~ ssList(X2)
| ! [X3] :
( ~ ssList(X3)
| app(X2,cons(X1,X3)) != X0 ) ) )
& ( ( ssList(sK13(X0,X1))
& ssList(sK14(X0,X1))
& app(sK13(X0,X1),cons(X1,sK14(X0,X1))) = X0 )
| ~ memberP(X0,X1) ) )
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14]),skolemize(X4,sK13(X0,X1)),skolemize(X5,sK14(X0,X1))],[f151]) ).
fof(f153,plain,
! [X0] :
( ! [X1] :
( ( ( lt(X0,X1)
| X0 = X1
| ~ leq(X0,X1) )
& ( ( X0 != X1
& leq(X0,X1) )
| ~ lt(X0,X1) ) )
| ~ ssItem(X1) )
| ~ ssItem(X0) ),
inference(nnf_transformation,[],[f127]) ).
fof(f154,plain,
! [X0] :
( ! [X1] :
( ( ( lt(X0,X1)
| X0 = X1
| ~ leq(X0,X1) )
& ( ( X0 != X1
& leq(X0,X1) )
| ~ lt(X0,X1) ) )
| ~ ssItem(X1) )
| ~ ssItem(X0) ),
inference(flattening,[],[f153]) ).
fof(f157,plain,
! [X0] :
( ( ( strictorderedP(X0)
| ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ~ lt(X1,X2)
& app(app(X3,cons(X1,X4)),cons(X2,X5)) = X0
& ssList(X5) )
& ssList(X4) )
& ssList(X3) )
& ssItem(X2) )
& ssItem(X1) ) )
& ( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( lt(X1,X2)
| app(app(X3,cons(X1,X4)),cons(X2,X5)) != X0
| ~ ssList(X5) )
| ~ ssList(X4) )
| ~ ssList(X3) )
| ~ ssItem(X2) )
| ~ ssItem(X1) )
| ~ strictorderedP(X0) ) )
| ~ ssList(X0) ),
inference(nnf_transformation,[],[f140]) ).
fof(f158,plain,
! [X0] :
( ( ( strictorderedP(X0)
| ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ~ lt(X1,X2)
& app(app(X3,cons(X1,X4)),cons(X2,X5)) = X0
& ssList(X5) )
& ssList(X4) )
& ssList(X3) )
& ssItem(X2) )
& ssItem(X1) ) )
& ( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ! [X10] :
( lt(X6,X7)
| app(app(X8,cons(X6,X9)),cons(X7,X10)) != X0
| ~ ssList(X10) )
| ~ ssList(X9) )
| ~ ssList(X8) )
| ~ ssItem(X7) )
| ~ ssItem(X6) )
| ~ strictorderedP(X0) ) )
| ~ ssList(X0) ),
inference(rectify,[],[f157]) ).
fof(f159,plain,
! [X0] :
( ( ( strictorderedP(X0)
| ( ~ lt(sK15(X0),sK16(X0))
& app(app(sK17(X0),cons(sK15(X0),sK18(X0))),cons(sK16(X0),sK19(X0))) = X0
& ssList(sK19(X0))
& ssList(sK18(X0))
& ssList(sK17(X0))
& ssItem(sK16(X0))
& ssItem(sK15(X0)) ) )
& ( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ! [X10] :
( lt(X6,X7)
| app(app(X8,cons(X6,X9)),cons(X7,X10)) != X0
| ~ ssList(X10) )
| ~ ssList(X9) )
| ~ ssList(X8) )
| ~ ssItem(X7) )
| ~ ssItem(X6) )
| ~ strictorderedP(X0) ) )
| ~ ssList(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16,sK17,sK18,sK19]),skolemize(X1,sK15(X0)),skolemize(X2,sK16(X0)),skolemize(X3,sK17(X0)),skolemize(X4,sK18(X0)),skolemize(X5,sK19(X0))],[f158]) ).
fof(f160,plain,
ssList(sK0),
inference(cnf_transformation,[],[f141]) ).
fof(f165,plain,
ssItem(sK5),
inference(cnf_transformation,[],[f141]) ).
fof(f166,plain,
ssList(sK6),
inference(cnf_transformation,[],[f141]) ).
fof(f167,plain,
ssList(sK7),
inference(cnf_transformation,[],[f141]) ).
fof(f168,plain,
ssItem(sK8),
inference(cnf_transformation,[],[f141]) ).
fof(f169,plain,
( ~ leq(sK8,sK5)
| ~ leq(sK5,sK8) ),
inference(cnf_transformation,[],[f141]) ).
fof(f170,plain,
( ~ leq(sK8,sK5)
| memberP(sK7,sK8) ),
inference(cnf_transformation,[],[f141]) ).
fof(f171,plain,
( memberP(sK6,sK8)
| ~ leq(sK5,sK8) ),
inference(cnf_transformation,[],[f141]) ).
fof(f172,plain,
( memberP(sK6,sK8)
| memberP(sK7,sK8) ),
inference(cnf_transformation,[],[f141]) ).
fof(f173,plain,
sK0 = app(app(sK6,cons(sK5,nil)),sK7),
inference(cnf_transformation,[],[f141]) ).
fof(f176,plain,
strictorderedP(sK2),
inference(cnf_transformation,[],[f141]) ).
fof(f178,plain,
sK0 = sK2,
inference(cnf_transformation,[],[f141]) ).
fof(f190,plain,
! [X0,X1] :
( ssList(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f106]) ).
fof(f195,plain,
! [X2,X0,X1] :
( app(app(X0,X1),X2) = app(X0,app(X1,X2))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f109]) ).
fof(f196,plain,
! [X0,X1] :
( cons(X1,X0) = app(cons(X1,nil),X0)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f110]) ).
fof(f201,plain,
! [X0,X1] :
( ssList(app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f202,plain,
ssList(nil),
inference(cnf_transformation,[],[f17]) ).
fof(f209,plain,
! [X2,X0,X1] :
( memberP(app(X1,X2),X0)
| ~ memberP(X1,X0)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f149]) ).
fof(f210,plain,
! [X0,X1] :
( app(sK13(X0,X1),cons(X1,sK14(X0,X1))) = X0
| ~ memberP(X0,X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f211,plain,
! [X0,X1] :
( ssList(sK14(X0,X1))
| ~ memberP(X0,X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f212,plain,
! [X0,X1] :
( ssList(sK13(X0,X1))
| ~ memberP(X0,X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f213,plain,
! [X2,X3,X0,X1] :
( memberP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X3)
| app(X2,cons(X1,X3)) != X0
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f217,plain,
! [X0,X1] :
( leq(X0,X1)
| ~ lt(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f154]) ).
fof(f232,plain,
! [X10,X0,X8,X6,X9,X7] :
( lt(X6,X7)
| app(app(X8,cons(X6,X9)),cons(X7,X10)) != X0
| ~ ssList(X10)
| ~ ssList(X9)
| ~ ssList(X8)
| ~ ssItem(X7)
| ~ ssItem(X6)
| ~ strictorderedP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f159]) ).
fof(f240,plain,
sK2 = app(app(sK6,cons(sK5,nil)),sK7),
inference(definition_unfolding,[],[f173,f178]) ).
fof(f242,plain,
ssList(sK2),
inference(definition_unfolding,[],[f160,f178]) ).
fof(f246,plain,
! [X2,X3,X1] :
( memberP(app(X2,cons(X1,X3)),X1)
| ~ ssList(X2)
| ~ ssList(X3)
| ~ ssItem(X1)
| ~ ssList(app(X2,cons(X1,X3))) ),
inference(equality_resolution,[],[f213]) ).
fof(f250,plain,
! [X10,X8,X6,X9,X7] :
( lt(X6,X7)
| ~ ssList(X10)
| ~ ssList(X9)
| ~ ssList(X8)
| ~ ssItem(X7)
| ~ ssItem(X6)
| ~ strictorderedP(app(app(X8,cons(X6,X9)),cons(X7,X10)))
| ~ ssList(app(app(X8,cons(X6,X9)),cons(X7,X10))) ),
inference(equality_resolution,[],[f232]) ).
fof(f259,definition,
( spl22_1
<=> sK2 = app(app(sK6,cons(sK5,nil)),sK7) ),
introduced(definition,[new_symbols(definition,[spl22_1])],[avatar_definition]) ).
fof(f261,plain,
( sK2 = app(app(sK6,cons(sK5,nil)),sK7)
| ~ spl22_1 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f262,plain,
spl22_1,
inference(avatar_split_clause,[],[f240,f259]) ).
fof(f284,plain,
( sK2 = app(sK6,app(cons(sK5,nil),sK7))
| ~ ssList(sK7)
| ~ ssList(cons(sK5,nil))
| ~ ssList(sK6)
| ~ spl22_1 ),
inference(superposition,[],[f195,f261]) ).
fof(f285,plain,
( sK2 = app(sK6,app(cons(sK5,nil),sK7))
| ~ ssList(cons(sK5,nil))
| ~ ssList(sK6)
| ~ spl22_1 ),
inference(forward_subsumption_resolution,[],[f284,f167]) ).
fof(f298,plain,
( sK2 = app(sK6,app(cons(sK5,nil),sK7))
| ~ ssList(cons(sK5,nil))
| ~ spl22_1 ),
inference(forward_subsumption_resolution,[],[f285,f166]) ).
fof(f301,definition,
( spl22_2
<=> ssItem(sK5) ),
introduced(definition,[new_symbols(definition,[spl22_2])],[avatar_definition]) ).
fof(f303,plain,
( ssItem(sK5)
| ~ spl22_2 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f304,plain,
spl22_2,
inference(avatar_split_clause,[],[f165,f301]) ).
fof(f323,plain,
( ! [X0] :
( ssList(sK14(X0,sK5))
| ~ memberP(X0,sK5)
| ~ ssList(X0) )
| ~ spl22_2 ),
inference(resolution,[],[f303,f211]) ).
fof(f324,plain,
( ! [X0] :
( ssList(sK13(X0,sK5))
| ~ memberP(X0,sK5)
| ~ ssList(X0) )
| ~ spl22_2 ),
inference(resolution,[],[f303,f212]) ).
fof(f352,plain,
( ! [X2,X3,X0,X1] :
( lt(X0,sK5)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(X3)
| ~ ssItem(X0)
| ~ strictorderedP(app(app(X3,cons(X0,X2)),cons(sK5,X1)))
| ~ ssList(app(app(X3,cons(X0,X2)),cons(sK5,X1))) )
| ~ spl22_2 ),
inference(resolution,[],[f303,f250]) ).
fof(f358,definition,
( spl22_3
<=> leq(sK5,sK8) ),
introduced(definition,[new_symbols(definition,[spl22_3])],[avatar_definition]) ).
fof(f360,plain,
( ~ leq(sK5,sK8)
| spl22_3 ),
inference(avatar_component_clause,[],[f358]) ).
fof(f362,definition,
( spl22_4
<=> leq(sK8,sK5) ),
introduced(definition,[new_symbols(definition,[spl22_4])],[avatar_definition]) ).
fof(f364,plain,
( ~ leq(sK8,sK5)
| spl22_4 ),
inference(avatar_component_clause,[],[f362]) ).
fof(f365,plain,
( ~ spl22_3
| ~ spl22_4 ),
inference(avatar_split_clause,[],[f169,f362,f358]) ).
fof(f366,plain,
( ~ lt(sK5,sK8)
| ~ ssItem(sK8)
| ~ ssItem(sK5)
| spl22_3 ),
inference(resolution,[],[f360,f217]) ).
fof(f369,plain,
( ~ lt(sK5,sK8)
| ~ ssItem(sK5)
| spl22_3 ),
inference(forward_subsumption_resolution,[],[f366,f168]) ).
fof(f371,plain,
( ~ lt(sK5,sK8)
| ~ spl22_2
| spl22_3 ),
inference(forward_subsumption_resolution,[],[f369,f303]) ).
fof(f435,definition,
( spl22_6
<=> ssItem(sK8) ),
introduced(definition,[new_symbols(definition,[spl22_6])],[avatar_definition]) ).
fof(f437,plain,
( ssItem(sK8)
| ~ spl22_6 ),
inference(avatar_component_clause,[],[f435]) ).
fof(f438,plain,
spl22_6,
inference(avatar_split_clause,[],[f168,f435]) ).
fof(f461,plain,
( ! [X0] :
( ssList(cons(sK8,X0))
| ~ ssList(X0) )
| ~ spl22_6 ),
inference(resolution,[],[f437,f190]) ).
fof(f508,definition,
( spl22_8
<=> ssList(sK2) ),
introduced(definition,[new_symbols(definition,[spl22_8])],[avatar_definition]) ).
fof(f510,plain,
( ssList(sK2)
| ~ spl22_8 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f511,plain,
spl22_8,
inference(avatar_split_clause,[],[f242,f508]) ).
fof(f610,definition,
( spl22_10
<=> ssList(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_10])],[avatar_definition]) ).
fof(f612,plain,
( ssList(sK7)
| ~ spl22_10 ),
inference(avatar_component_clause,[],[f610]) ).
fof(f613,plain,
spl22_10,
inference(avatar_split_clause,[],[f167,f610]) ).
fof(f672,definition,
( spl22_11
<=> lt(sK5,sK8) ),
introduced(definition,[new_symbols(definition,[spl22_11])],[avatar_definition]) ).
fof(f674,plain,
( ~ lt(sK5,sK8)
| spl22_11 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f675,plain,
( ~ spl22_11
| ~ spl22_2
| spl22_3 ),
inference(avatar_split_clause,[],[f371,f358,f301,f672]) ).
fof(f681,definition,
( spl22_13
<=> memberP(sK6,sK8) ),
introduced(definition,[new_symbols(definition,[spl22_13])],[avatar_definition]) ).
fof(f683,plain,
( memberP(sK6,sK8)
| ~ spl22_13 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f684,plain,
( ~ spl22_3
| spl22_13 ),
inference(avatar_split_clause,[],[f171,f681,f358]) ).
fof(f686,definition,
( spl22_14
<=> ssList(cons(sK5,nil)) ),
introduced(definition,[new_symbols(definition,[spl22_14])],[avatar_definition]) ).
fof(f687,plain,
( ssList(cons(sK5,nil))
| ~ spl22_14 ),
inference(avatar_component_clause,[],[f686]) ).
fof(f688,plain,
( ~ ssList(cons(sK5,nil))
| spl22_14 ),
inference(avatar_component_clause,[],[f686]) ).
fof(f690,definition,
( spl22_15
<=> sK2 = app(sK6,app(cons(sK5,nil),sK7)) ),
introduced(definition,[new_symbols(definition,[spl22_15])],[avatar_definition]) ).
fof(f692,plain,
( sK2 = app(sK6,app(cons(sK5,nil),sK7))
| ~ spl22_15 ),
inference(avatar_component_clause,[],[f690]) ).
fof(f693,plain,
( ~ spl22_14
| spl22_15
| ~ spl22_1 ),
inference(avatar_split_clause,[],[f298,f259,f690,f686]) ).
fof(f694,plain,
( ~ ssItem(sK5)
| ~ ssList(nil)
| spl22_14 ),
inference(resolution,[],[f688,f190]) ).
fof(f711,plain,
( ~ ssList(nil)
| ~ spl22_2
| spl22_14 ),
inference(forward_subsumption_resolution,[],[f694,f303]) ).
fof(f712,plain,
( $false
| ~ spl22_2
| spl22_14 ),
inference(forward_subsumption_resolution,[],[f711,f202]) ).
fof(f713,plain,
( ~ spl22_2
| spl22_14 ),
inference(avatar_contradiction_clause,[],[f712]) ).
fof(f722,plain,
( sK2 = app(sK6,cons(sK5,sK7))
| ~ ssItem(sK5)
| ~ ssList(sK7)
| ~ spl22_15 ),
inference(superposition,[],[f692,f196]) ).
fof(f746,plain,
( sK2 = app(sK6,cons(sK5,sK7))
| ~ ssList(sK7)
| ~ spl22_2
| ~ spl22_15 ),
inference(forward_subsumption_resolution,[],[f722,f303]) ).
fof(f747,plain,
( sK2 = app(sK6,cons(sK5,sK7))
| ~ spl22_2
| ~ spl22_10
| ~ spl22_15 ),
inference(forward_subsumption_resolution,[],[f746,f612]) ).
fof(f749,definition,
( spl22_16
<=> sK2 = app(sK6,cons(sK5,sK7)) ),
introduced(definition,[new_symbols(definition,[spl22_16])],[avatar_definition]) ).
fof(f751,plain,
( sK2 = app(sK6,cons(sK5,sK7))
| ~ spl22_16 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f752,plain,
( spl22_16
| ~ spl22_2
| ~ spl22_10
| ~ spl22_15 ),
inference(avatar_split_clause,[],[f747,f690,f610,f301,f749]) ).
fof(f795,definition,
( spl22_17
<=> strictorderedP(sK2) ),
introduced(definition,[new_symbols(definition,[spl22_17])],[avatar_definition]) ).
fof(f797,plain,
( strictorderedP(sK2)
| ~ spl22_17 ),
inference(avatar_component_clause,[],[f795]) ).
fof(f798,plain,
spl22_17,
inference(avatar_split_clause,[],[f176,f795]) ).
fof(f800,definition,
( spl22_18
<=> ssList(sK6) ),
introduced(definition,[new_symbols(definition,[spl22_18])],[avatar_definition]) ).
fof(f802,plain,
( ssList(sK6)
| ~ spl22_18 ),
inference(avatar_component_clause,[],[f800]) ).
fof(f803,plain,
spl22_18,
inference(avatar_split_clause,[],[f166,f800]) ).
fof(f862,definition,
( spl22_19
<=> memberP(sK7,sK8) ),
introduced(definition,[new_symbols(definition,[spl22_19])],[avatar_definition]) ).
fof(f864,plain,
( memberP(sK7,sK8)
| ~ spl22_19 ),
inference(avatar_component_clause,[],[f862]) ).
fof(f865,plain,
( spl22_19
| ~ spl22_4 ),
inference(avatar_split_clause,[],[f170,f362,f862]) ).
fof(f866,plain,
( ~ lt(sK8,sK5)
| ~ ssItem(sK5)
| ~ ssItem(sK8)
| spl22_4 ),
inference(resolution,[],[f364,f217]) ).
fof(f869,plain,
( ~ lt(sK8,sK5)
| ~ ssItem(sK8)
| ~ spl22_2
| spl22_4 ),
inference(forward_subsumption_resolution,[],[f866,f303]) ).
fof(f871,plain,
( ~ lt(sK8,sK5)
| ~ spl22_2
| spl22_4
| ~ spl22_6 ),
inference(forward_subsumption_resolution,[],[f869,f437]) ).
fof(f873,plain,
( ! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssItem(sK8)
| ~ ssItem(sK5)
| ~ strictorderedP(app(app(X2,cons(sK5,X1)),cons(sK8,X0)))
| ~ ssList(app(app(X2,cons(sK5,X1)),cons(sK8,X0))) )
| spl22_11 ),
inference(resolution,[],[f674,f250]) ).
fof(f880,plain,
( ! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssItem(sK5)
| ~ strictorderedP(app(app(X2,cons(sK5,X1)),cons(sK8,X0)))
| ~ ssList(app(app(X2,cons(sK5,X1)),cons(sK8,X0))) )
| ~ spl22_6
| spl22_11 ),
inference(forward_subsumption_resolution,[],[f873,f437]) ).
fof(f883,plain,
( ! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ strictorderedP(app(app(X2,cons(sK5,X1)),cons(sK8,X0)))
| ~ ssList(app(app(X2,cons(sK5,X1)),cons(sK8,X0))) )
| ~ spl22_2
| ~ spl22_6
| spl22_11 ),
inference(forward_subsumption_resolution,[],[f880,f303]) ).
fof(f885,definition,
( spl22_20
<=> lt(sK8,sK5) ),
introduced(definition,[new_symbols(definition,[spl22_20])],[avatar_definition]) ).
fof(f887,plain,
( ~ lt(sK8,sK5)
| spl22_20 ),
inference(avatar_component_clause,[],[f885]) ).
fof(f888,plain,
( ~ spl22_20
| ~ spl22_2
| spl22_4
| ~ spl22_6 ),
inference(avatar_split_clause,[],[f871,f435,f362,f301,f885]) ).
fof(f989,plain,
( spl22_19
| spl22_13 ),
inference(avatar_split_clause,[],[f172,f681,f862]) ).
fof(f990,plain,
( sK7 = app(sK13(sK7,sK8),cons(sK8,sK14(sK7,sK8)))
| ~ ssItem(sK8)
| ~ ssList(sK7)
| ~ spl22_19 ),
inference(resolution,[],[f864,f210]) ).
fof(f1001,plain,
( sK7 = app(sK13(sK7,sK8),cons(sK8,sK14(sK7,sK8)))
| ~ ssList(sK7)
| ~ spl22_6
| ~ spl22_19 ),
inference(forward_subsumption_resolution,[],[f990,f437]) ).
fof(f1007,plain,
( sK7 = app(sK13(sK7,sK8),cons(sK8,sK14(sK7,sK8)))
| ~ spl22_6
| ~ spl22_10
| ~ spl22_19 ),
inference(forward_subsumption_resolution,[],[f1001,f612]) ).
fof(f1026,definition,
( spl22_24
<=> sK7 = app(sK13(sK7,sK8),cons(sK8,sK14(sK7,sK8))) ),
introduced(definition,[new_symbols(definition,[spl22_24])],[avatar_definition]) ).
fof(f1028,plain,
( sK7 = app(sK13(sK7,sK8),cons(sK8,sK14(sK7,sK8)))
| ~ spl22_24 ),
inference(avatar_component_clause,[],[f1026]) ).
fof(f1029,plain,
( spl22_24
| ~ spl22_6
| ~ spl22_10
| ~ spl22_19 ),
inference(avatar_split_clause,[],[f1007,f862,f610,f435,f1026]) ).
fof(f1030,plain,
( sK6 = app(sK13(sK6,sK8),cons(sK8,sK14(sK6,sK8)))
| ~ ssItem(sK8)
| ~ ssList(sK6)
| ~ spl22_13 ),
inference(resolution,[],[f683,f210]) ).
fof(f1041,plain,
( sK6 = app(sK13(sK6,sK8),cons(sK8,sK14(sK6,sK8)))
| ~ ssList(sK6)
| ~ spl22_6
| ~ spl22_13 ),
inference(forward_subsumption_resolution,[],[f1030,f437]) ).
fof(f1047,plain,
( sK6 = app(sK13(sK6,sK8),cons(sK8,sK14(sK6,sK8)))
| ~ spl22_6
| ~ spl22_13
| ~ spl22_18 ),
inference(forward_subsumption_resolution,[],[f1041,f802]) ).
fof(f1058,definition,
( spl22_25
<=> sK6 = app(sK13(sK6,sK8),cons(sK8,sK14(sK6,sK8))) ),
introduced(definition,[new_symbols(definition,[spl22_25])],[avatar_definition]) ).
fof(f1060,plain,
( sK6 = app(sK13(sK6,sK8),cons(sK8,sK14(sK6,sK8)))
| ~ spl22_25 ),
inference(avatar_component_clause,[],[f1058]) ).
fof(f1061,plain,
( spl22_25
| ~ spl22_6
| ~ spl22_13
| ~ spl22_18 ),
inference(avatar_split_clause,[],[f1047,f800,f681,f435,f1058]) ).
fof(f1167,definition,
( spl22_27
<=> ! [X0,X3,X2,X1] :
( lt(X0,sK5)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(X3)
| ~ ssItem(X0)
| ~ strictorderedP(app(app(X3,cons(X0,X2)),cons(sK5,X1)))
| ~ ssList(app(app(X3,cons(X0,X2)),cons(sK5,X1))) ) ),
introduced(definition,[new_symbols(definition,[spl22_27])],[avatar_definition]) ).
fof(f1168,plain,
( ! [X2,X3,X0,X1] :
( ~ strictorderedP(app(app(X3,cons(X0,X2)),cons(sK5,X1)))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(X3)
| ~ ssItem(X0)
| lt(X0,sK5)
| ~ ssList(app(app(X3,cons(X0,X2)),cons(sK5,X1))) )
| ~ spl22_27 ),
inference(avatar_component_clause,[],[f1167]) ).
fof(f1169,plain,
( spl22_27
| ~ spl22_2 ),
inference(avatar_split_clause,[],[f352,f301,f1167]) ).
fof(f1239,plain,
( ssList(sK14(sK6,sK8))
| ~ ssItem(sK8)
| ~ ssList(sK6)
| ~ spl22_13 ),
inference(resolution,[],[f683,f211]) ).
fof(f1240,plain,
( ssList(sK13(sK6,sK8))
| ~ ssItem(sK8)
| ~ ssList(sK6)
| ~ spl22_13 ),
inference(resolution,[],[f683,f212]) ).
fof(f1247,plain,
( ssList(sK13(sK6,sK8))
| ~ ssList(sK6)
| ~ spl22_6
| ~ spl22_13 ),
inference(forward_subsumption_resolution,[],[f1240,f437]) ).
fof(f1248,plain,
( ssList(sK14(sK6,sK8))
| ~ ssList(sK6)
| ~ spl22_6
| ~ spl22_13 ),
inference(forward_subsumption_resolution,[],[f1239,f437]) ).
fof(f1252,plain,
( ssList(sK13(sK6,sK8))
| ~ spl22_6
| ~ spl22_13
| ~ spl22_18 ),
inference(forward_subsumption_resolution,[],[f1247,f802]) ).
fof(f1253,plain,
( ssList(sK14(sK6,sK8))
| ~ spl22_6
| ~ spl22_13
| ~ spl22_18 ),
inference(forward_subsumption_resolution,[],[f1248,f802]) ).
fof(f1255,plain,
( ! [X0] :
( ~ strictorderedP(app(sK6,cons(sK5,X0)))
| ~ ssList(X0)
| ~ ssList(sK14(sK6,sK8))
| ~ ssList(sK13(sK6,sK8))
| ~ ssItem(sK8)
| lt(sK8,sK5)
| ~ ssList(app(sK6,cons(sK5,X0))) )
| ~ spl22_25
| ~ spl22_27 ),
inference(superposition,[],[f1168,f1060]) ).
fof(f1285,plain,
( ! [X0] :
( ~ strictorderedP(app(sK6,cons(sK5,X0)))
| ~ ssList(X0)
| ~ ssList(sK13(sK6,sK8))
| ~ ssItem(sK8)
| lt(sK8,sK5)
| ~ ssList(app(sK6,cons(sK5,X0))) )
| ~ spl22_6
| ~ spl22_13
| ~ spl22_18
| ~ spl22_25
| ~ spl22_27 ),
inference(forward_subsumption_resolution,[],[f1255,f1253]) ).
fof(f1289,plain,
( ! [X0] :
( ~ strictorderedP(app(sK6,cons(sK5,X0)))
| ~ ssList(X0)
| ~ ssItem(sK8)
| lt(sK8,sK5)
| ~ ssList(app(sK6,cons(sK5,X0))) )
| ~ spl22_6
| ~ spl22_13
| ~ spl22_18
| ~ spl22_25
| ~ spl22_27 ),
inference(forward_subsumption_resolution,[],[f1285,f1252]) ).
fof(f1293,plain,
( ! [X0] :
( ~ strictorderedP(app(sK6,cons(sK5,X0)))
| ~ ssList(X0)
| lt(sK8,sK5)
| ~ ssList(app(sK6,cons(sK5,X0))) )
| ~ spl22_6
| ~ spl22_13
| ~ spl22_18
| ~ spl22_25
| ~ spl22_27 ),
inference(forward_subsumption_resolution,[],[f1289,f437]) ).
fof(f1294,plain,
( ! [X0] :
( ~ strictorderedP(app(sK6,cons(sK5,X0)))
| ~ ssList(X0)
| ~ ssList(app(sK6,cons(sK5,X0))) )
| ~ spl22_6
| ~ spl22_13
| ~ spl22_18
| spl22_20
| ~ spl22_25
| ~ spl22_27 ),
inference(forward_subsumption_resolution,[],[f1293,f887]) ).
fof(f1296,definition,
( spl22_30
<=> ! [X0] :
( ~ strictorderedP(app(sK6,cons(sK5,X0)))
| ~ ssList(X0)
| ~ ssList(app(sK6,cons(sK5,X0))) ) ),
introduced(definition,[new_symbols(definition,[spl22_30])],[avatar_definition]) ).
fof(f1297,plain,
( ! [X0] :
( ~ strictorderedP(app(sK6,cons(sK5,X0)))
| ~ ssList(X0)
| ~ ssList(app(sK6,cons(sK5,X0))) )
| ~ spl22_30 ),
inference(avatar_component_clause,[],[f1296]) ).
fof(f1298,plain,
( spl22_30
| ~ spl22_6
| ~ spl22_13
| ~ spl22_18
| spl22_20
| ~ spl22_25
| ~ spl22_27 ),
inference(avatar_split_clause,[],[f1294,f1167,f1058,f885,f800,f681,f435,f1296]) ).
fof(f1308,plain,
( ~ strictorderedP(sK2)
| ~ ssList(sK7)
| ~ ssList(sK2)
| ~ spl22_16
| ~ spl22_30 ),
inference(superposition,[],[f1297,f751]) ).
fof(f1317,plain,
( ~ ssList(sK7)
| ~ ssList(sK2)
| ~ spl22_16
| ~ spl22_17
| ~ spl22_30 ),
inference(forward_subsumption_resolution,[],[f1308,f797]) ).
fof(f1319,plain,
( ~ ssList(sK2)
| ~ spl22_10
| ~ spl22_16
| ~ spl22_17
| ~ spl22_30 ),
inference(forward_subsumption_resolution,[],[f1317,f612]) ).
fof(f1321,plain,
( $false
| ~ spl22_8
| ~ spl22_10
| ~ spl22_16
| ~ spl22_17
| ~ spl22_30 ),
inference(forward_subsumption_resolution,[],[f1319,f510]) ).
fof(f1322,plain,
( ~ spl22_8
| ~ spl22_10
| ~ spl22_16
| ~ spl22_17
| ~ spl22_30 ),
inference(avatar_contradiction_clause,[],[f1321]) ).
fof(f1334,plain,
( ssList(sK14(sK7,sK8))
| ~ ssItem(sK8)
| ~ ssList(sK7)
| ~ spl22_19 ),
inference(resolution,[],[f864,f211]) ).
fof(f1335,plain,
( ssList(sK13(sK7,sK8))
| ~ ssItem(sK8)
| ~ ssList(sK7)
| ~ spl22_19 ),
inference(resolution,[],[f864,f212]) ).
fof(f1342,plain,
( ssList(sK13(sK7,sK8))
| ~ ssList(sK7)
| ~ spl22_6
| ~ spl22_19 ),
inference(forward_subsumption_resolution,[],[f1335,f437]) ).
fof(f1343,plain,
( ssList(sK14(sK7,sK8))
| ~ ssList(sK7)
| ~ spl22_6
| ~ spl22_19 ),
inference(forward_subsumption_resolution,[],[f1334,f437]) ).
fof(f1347,plain,
( ssList(sK13(sK7,sK8))
| ~ spl22_6
| ~ spl22_10
| ~ spl22_19 ),
inference(forward_subsumption_resolution,[],[f1342,f612]) ).
fof(f1348,plain,
( ssList(sK14(sK7,sK8))
| ~ spl22_6
| ~ spl22_10
| ~ spl22_19 ),
inference(forward_subsumption_resolution,[],[f1343,f612]) ).
fof(f1450,definition,
( spl22_35
<=> ssList(sK14(sK7,sK8)) ),
introduced(definition,[new_symbols(definition,[spl22_35])],[avatar_definition]) ).
fof(f1452,plain,
( ssList(sK14(sK7,sK8))
| ~ spl22_35 ),
inference(avatar_component_clause,[],[f1450]) ).
fof(f1453,plain,
( spl22_35
| ~ spl22_6
| ~ spl22_10
| ~ spl22_19 ),
inference(avatar_split_clause,[],[f1348,f862,f610,f435,f1450]) ).
fof(f1787,definition,
( spl22_44
<=> ssList(sK13(sK7,sK8)) ),
introduced(definition,[new_symbols(definition,[spl22_44])],[avatar_definition]) ).
fof(f1789,plain,
( ssList(sK13(sK7,sK8))
| ~ spl22_44 ),
inference(avatar_component_clause,[],[f1787]) ).
fof(f1790,plain,
( spl22_44
| ~ spl22_6
| ~ spl22_10
| ~ spl22_19 ),
inference(avatar_split_clause,[],[f1347,f862,f610,f435,f1787]) ).
fof(f2025,definition,
( spl22_52
<=> ssList(app(sK6,cons(sK5,nil))) ),
introduced(definition,[new_symbols(definition,[spl22_52])],[avatar_definition]) ).
fof(f2026,plain,
( ssList(app(sK6,cons(sK5,nil)))
| ~ spl22_52 ),
inference(avatar_component_clause,[],[f2025]) ).
fof(f2027,plain,
( ~ ssList(app(sK6,cons(sK5,nil)))
| spl22_52 ),
inference(avatar_component_clause,[],[f2025]) ).
fof(f2033,plain,
( ~ ssList(cons(sK5,nil))
| ~ ssList(sK6)
| spl22_52 ),
inference(resolution,[],[f2027,f201]) ).
fof(f2042,plain,
( ~ ssList(sK6)
| ~ spl22_14
| spl22_52 ),
inference(forward_subsumption_resolution,[],[f2033,f687]) ).
fof(f2043,plain,
( $false
| ~ spl22_14
| ~ spl22_18
| spl22_52 ),
inference(forward_subsumption_resolution,[],[f2042,f802]) ).
fof(f2044,plain,
( ~ spl22_14
| ~ spl22_18
| spl22_52 ),
inference(avatar_contradiction_clause,[],[f2043]) ).
fof(f2096,plain,
( memberP(app(sK6,cons(sK5,nil)),sK5)
| ~ ssList(sK6)
| ~ ssList(nil)
| ~ ssItem(sK5)
| ~ spl22_52 ),
inference(resolution,[],[f2026,f246]) ).
fof(f2112,plain,
( ! [X0,X1] :
( app(app(app(sK6,cons(sK5,nil)),X0),X1) = app(app(sK6,cons(sK5,nil)),app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) )
| ~ spl22_52 ),
inference(resolution,[],[f2026,f195]) ).
fof(f2125,plain,
( ! [X0] :
( ssList(app(app(sK6,cons(sK5,nil)),X0))
| ~ ssList(X0) )
| ~ spl22_52 ),
inference(resolution,[],[f2026,f201]) ).
fof(f2162,plain,
( memberP(app(sK6,cons(sK5,nil)),sK5)
| ~ ssList(nil)
| ~ ssItem(sK5)
| ~ spl22_18
| ~ spl22_52 ),
inference(forward_subsumption_resolution,[],[f2096,f802]) ).
fof(f2163,plain,
( memberP(app(sK6,cons(sK5,nil)),sK5)
| ~ ssItem(sK5)
| ~ spl22_18
| ~ spl22_52 ),
inference(forward_subsumption_resolution,[],[f2162,f202]) ).
fof(f2164,plain,
( memberP(app(sK6,cons(sK5,nil)),sK5)
| ~ spl22_2
| ~ spl22_18
| ~ spl22_52 ),
inference(forward_subsumption_resolution,[],[f2163,f303]) ).
fof(f2179,definition,
( spl22_56
<=> ! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ strictorderedP(app(app(X2,cons(sK5,X1)),cons(sK8,X0)))
| ~ ssList(app(app(X2,cons(sK5,X1)),cons(sK8,X0))) ) ),
introduced(definition,[new_symbols(definition,[spl22_56])],[avatar_definition]) ).
fof(f2180,plain,
( ! [X2,X0,X1] :
( ~ strictorderedP(app(app(X2,cons(sK5,X1)),cons(sK8,X0)))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(app(app(X2,cons(sK5,X1)),cons(sK8,X0))) )
| ~ spl22_56 ),
inference(avatar_component_clause,[],[f2179]) ).
fof(f2181,plain,
( spl22_56
| ~ spl22_2
| ~ spl22_6
| spl22_11 ),
inference(avatar_split_clause,[],[f883,f672,f435,f301,f2179]) ).
fof(f2642,plain,
( ! [X0,X1] :
( ~ strictorderedP(app(X0,cons(sK8,X1)))
| ~ ssList(sK14(X0,sK5))
| ~ ssList(sK13(X0,sK5))
| ~ ssList(X1)
| ~ ssList(app(X0,cons(sK8,X1)))
| ~ memberP(X0,sK5)
| ~ ssItem(sK5)
| ~ ssList(X0) )
| ~ spl22_56 ),
inference(superposition,[],[f2180,f210]) ).
fof(f2663,plain,
( ! [X0,X1] :
( ~ strictorderedP(app(X0,cons(sK8,X1)))
| ~ ssList(sK14(X0,sK5))
| ~ ssList(sK13(X0,sK5))
| ~ ssList(X1)
| ~ ssList(app(X0,cons(sK8,X1)))
| ~ memberP(X0,sK5)
| ~ ssList(X0) )
| ~ spl22_2
| ~ spl22_56 ),
inference(forward_subsumption_resolution,[],[f2642,f303]) ).
fof(f2669,plain,
( ! [X0,X1] :
( ~ strictorderedP(app(X0,cons(sK8,X1)))
| ~ ssList(sK13(X0,sK5))
| ~ ssList(X1)
| ~ ssList(app(X0,cons(sK8,X1)))
| ~ memberP(X0,sK5)
| ~ ssList(X0) )
| ~ spl22_2
| ~ spl22_56 ),
inference(forward_subsumption_resolution,[],[f2663,f323]) ).
fof(f2671,plain,
( ! [X0,X1] :
( ~ strictorderedP(app(X0,cons(sK8,X1)))
| ~ ssList(X1)
| ~ ssList(app(X0,cons(sK8,X1)))
| ~ memberP(X0,sK5)
| ~ ssList(X0) )
| ~ spl22_2
| ~ spl22_56 ),
inference(forward_subsumption_resolution,[],[f2669,f324]) ).
fof(f2673,definition,
( spl22_65
<=> ! [X0,X1] :
( ~ strictorderedP(app(X0,cons(sK8,X1)))
| ~ ssList(X1)
| ~ ssList(app(X0,cons(sK8,X1)))
| ~ memberP(X0,sK5)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_65])],[avatar_definition]) ).
fof(f2674,plain,
( ! [X0,X1] :
( ~ strictorderedP(app(X0,cons(sK8,X1)))
| ~ ssList(X1)
| ~ ssList(app(X0,cons(sK8,X1)))
| ~ memberP(X0,sK5)
| ~ ssList(X0) )
| ~ spl22_65 ),
inference(avatar_component_clause,[],[f2673]) ).
fof(f2675,plain,
( spl22_65
| ~ spl22_2
| ~ spl22_56 ),
inference(avatar_split_clause,[],[f2671,f2179,f301,f2673]) ).
fof(f2731,definition,
( spl22_69
<=> memberP(app(sK6,cons(sK5,nil)),sK5) ),
introduced(definition,[new_symbols(definition,[spl22_69])],[avatar_definition]) ).
fof(f2733,plain,
( memberP(app(sK6,cons(sK5,nil)),sK5)
| ~ spl22_69 ),
inference(avatar_component_clause,[],[f2731]) ).
fof(f2734,plain,
( spl22_69
| ~ spl22_2
| ~ spl22_18
| ~ spl22_52 ),
inference(avatar_split_clause,[],[f2164,f2025,f800,f301,f2731]) ).
fof(f2740,plain,
( ! [X0] :
( memberP(app(app(sK6,cons(sK5,nil)),X0),sK5)
| ~ ssList(X0)
| ~ ssList(app(sK6,cons(sK5,nil)))
| ~ ssItem(sK5) )
| ~ spl22_69 ),
inference(resolution,[],[f2733,f209]) ).
fof(f2751,plain,
( ! [X0] :
( memberP(app(app(sK6,cons(sK5,nil)),X0),sK5)
| ~ ssList(X0)
| ~ ssItem(sK5) )
| ~ spl22_52
| ~ spl22_69 ),
inference(forward_subsumption_resolution,[],[f2740,f2026]) ).
fof(f2758,plain,
( ! [X0] :
( memberP(app(app(sK6,cons(sK5,nil)),X0),sK5)
| ~ ssList(X0) )
| ~ spl22_2
| ~ spl22_52
| ~ spl22_69 ),
inference(forward_subsumption_resolution,[],[f2751,f303]) ).
fof(f5126,definition,
( spl22_137
<=> ! [X0,X1] :
( app(app(app(sK6,cons(sK5,nil)),X0),X1) = app(app(sK6,cons(sK5,nil)),app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_137])],[avatar_definition]) ).
fof(f5127,plain,
( ! [X0,X1] :
( app(app(app(sK6,cons(sK5,nil)),X0),X1) = app(app(sK6,cons(sK5,nil)),app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) )
| ~ spl22_137 ),
inference(avatar_component_clause,[],[f5126]) ).
fof(f5128,plain,
( spl22_137
| ~ spl22_52 ),
inference(avatar_split_clause,[],[f2112,f2025,f5126]) ).
fof(f5153,plain,
( ! [X0,X1] :
( ssList(app(app(sK6,cons(sK5,nil)),app(X0,X1)))
| ~ ssList(X1)
| ~ ssList(app(app(sK6,cons(sK5,nil)),X0))
| ~ ssList(X1)
| ~ ssList(X0) )
| ~ spl22_137 ),
inference(superposition,[],[f201,f5127]) ).
fof(f5212,plain,
( ! [X0,X1] :
( ~ strictorderedP(app(app(sK6,cons(sK5,nil)),app(X0,cons(sK8,X1))))
| ~ ssList(X1)
| ~ ssList(app(app(sK6,cons(sK5,nil)),app(X0,cons(sK8,X1))))
| ~ memberP(app(app(sK6,cons(sK5,nil)),X0),sK5)
| ~ ssList(app(app(sK6,cons(sK5,nil)),X0))
| ~ ssList(cons(sK8,X1))
| ~ ssList(X0) )
| ~ spl22_65
| ~ spl22_137 ),
inference(superposition,[],[f2674,f5127]) ).
fof(f5238,plain,
( ! [X0,X1] :
( ssList(app(app(sK6,cons(sK5,nil)),app(X0,X1)))
| ~ ssList(X1)
| ~ ssList(app(app(sK6,cons(sK5,nil)),X0))
| ~ ssList(X0) )
| ~ spl22_137 ),
inference(duplicate_literal_removal,[],[f5153]) ).
fof(f5260,plain,
( ! [X0,X1] :
( ~ strictorderedP(app(app(sK6,cons(sK5,nil)),app(X0,cons(sK8,X1))))
| ~ ssList(X1)
| ~ ssList(app(app(sK6,cons(sK5,nil)),app(X0,cons(sK8,X1))))
| ~ memberP(app(app(sK6,cons(sK5,nil)),X0),sK5)
| ~ ssList(cons(sK8,X1))
| ~ ssList(X0) )
| ~ spl22_52
| ~ spl22_65
| ~ spl22_137 ),
inference(forward_subsumption_resolution,[],[f5212,f2125]) ).
fof(f5299,plain,
( ! [X0,X1] :
( ssList(app(app(sK6,cons(sK5,nil)),app(X0,X1)))
| ~ ssList(X1)
| ~ ssList(X0) )
| ~ spl22_52
| ~ spl22_137 ),
inference(forward_subsumption_resolution,[],[f5238,f2125]) ).
fof(f5318,plain,
( ! [X0,X1] :
( ~ strictorderedP(app(app(sK6,cons(sK5,nil)),app(X0,cons(sK8,X1))))
| ~ ssList(X1)
| ~ ssList(app(app(sK6,cons(sK5,nil)),app(X0,cons(sK8,X1))))
| ~ ssList(cons(sK8,X1))
| ~ ssList(X0) )
| ~ spl22_2
| ~ spl22_52
| ~ spl22_65
| ~ spl22_69
| ~ spl22_137 ),
inference(forward_subsumption_resolution,[],[f5260,f2758]) ).
fof(f5350,plain,
( ! [X0,X1] :
( ~ strictorderedP(app(app(sK6,cons(sK5,nil)),app(X0,cons(sK8,X1))))
| ~ ssList(X1)
| ~ ssList(cons(sK8,X1))
| ~ ssList(X0) )
| ~ spl22_2
| ~ spl22_52
| ~ spl22_65
| ~ spl22_69
| ~ spl22_137 ),
inference(forward_subsumption_resolution,[],[f5318,f5299]) ).
fof(f5355,plain,
( ! [X0,X1] :
( ~ strictorderedP(app(app(sK6,cons(sK5,nil)),app(X0,cons(sK8,X1))))
| ~ ssList(X1)
| ~ ssList(X0) )
| ~ spl22_2
| ~ spl22_6
| ~ spl22_52
| ~ spl22_65
| ~ spl22_69
| ~ spl22_137 ),
inference(forward_subsumption_resolution,[],[f5350,f461]) ).
fof(f5364,definition,
( spl22_139
<=> ! [X0,X1] :
( ~ strictorderedP(app(app(sK6,cons(sK5,nil)),app(X0,cons(sK8,X1))))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_139])],[avatar_definition]) ).
fof(f5365,plain,
( ! [X0,X1] :
( ~ strictorderedP(app(app(sK6,cons(sK5,nil)),app(X0,cons(sK8,X1))))
| ~ ssList(X1)
| ~ ssList(X0) )
| ~ spl22_139 ),
inference(avatar_component_clause,[],[f5364]) ).
fof(f5366,plain,
( spl22_139
| ~ spl22_2
| ~ spl22_6
| ~ spl22_52
| ~ spl22_65
| ~ spl22_69
| ~ spl22_137 ),
inference(avatar_split_clause,[],[f5355,f5126,f2731,f2673,f2025,f435,f301,f5364]) ).
fof(f5384,plain,
( ~ strictorderedP(app(app(sK6,cons(sK5,nil)),sK7))
| ~ ssList(sK14(sK7,sK8))
| ~ ssList(sK13(sK7,sK8))
| ~ spl22_24
| ~ spl22_139 ),
inference(superposition,[],[f5365,f1028]) ).
fof(f5400,plain,
( ~ strictorderedP(app(app(sK6,cons(sK5,nil)),sK7))
| ~ ssList(sK13(sK7,sK8))
| ~ spl22_24
| ~ spl22_35
| ~ spl22_139 ),
inference(forward_subsumption_resolution,[],[f5384,f1452]) ).
fof(f5407,plain,
( ~ strictorderedP(app(app(sK6,cons(sK5,nil)),sK7))
| ~ spl22_24
| ~ spl22_35
| ~ spl22_44
| ~ spl22_139 ),
inference(forward_subsumption_resolution,[],[f5400,f1789]) ).
fof(f5410,plain,
( ~ strictorderedP(sK2)
| ~ spl22_1
| ~ spl22_24
| ~ spl22_35
| ~ spl22_44
| ~ spl22_139 ),
inference(forward_demodulation,[],[f5407,f261]) ).
fof(f5411,plain,
( $false
| ~ spl22_1
| ~ spl22_17
| ~ spl22_24
| ~ spl22_35
| ~ spl22_44
| ~ spl22_139 ),
inference(forward_subsumption_resolution,[],[f5410,f797]) ).
fof(f5412,plain,
( ~ spl22_1
| ~ spl22_17
| ~ spl22_24
| ~ spl22_35
| ~ spl22_44
| ~ spl22_139 ),
inference(avatar_contradiction_clause,[],[f5411]) ).
cnf(s1,plain,
spl22_1,
inference(sat_conversion,[],[f262]) ).
cnf(s2,plain,
spl22_2,
inference(sat_conversion,[],[f304]) ).
cnf(s3,plain,
( ~ spl22_3
| ~ spl22_4 ),
inference(sat_conversion,[],[f365]) ).
cnf(s5,plain,
spl22_6,
inference(sat_conversion,[],[f438]) ).
cnf(s7,plain,
spl22_8,
inference(sat_conversion,[],[f511]) ).
cnf(s9,plain,
spl22_10,
inference(sat_conversion,[],[f613]) ).
cnf(s10,plain,
( ~ spl22_2
| spl22_3
| ~ spl22_11 ),
inference(sat_conversion,[],[f675]) ).
cnf(s12,plain,
( ~ spl22_3
| spl22_13 ),
inference(sat_conversion,[],[f684]) ).
cnf(s13,plain,
( ~ spl22_1
| ~ spl22_14
| spl22_15 ),
inference(sat_conversion,[],[f693]) ).
cnf(s14,plain,
( ~ spl22_2
| spl22_14 ),
inference(sat_conversion,[],[f713]) ).
cnf(s15,plain,
( ~ spl22_2
| ~ spl22_10
| ~ spl22_15
| spl22_16 ),
inference(sat_conversion,[],[f752]) ).
cnf(s16,plain,
spl22_17,
inference(sat_conversion,[],[f798]) ).
cnf(s17,plain,
spl22_18,
inference(sat_conversion,[],[f803]) ).
cnf(s18,plain,
( ~ spl22_4
| spl22_19 ),
inference(sat_conversion,[],[f865]) ).
cnf(s19,plain,
( ~ spl22_2
| spl22_4
| ~ spl22_6
| ~ spl22_20 ),
inference(sat_conversion,[],[f888]) ).
cnf(s21,plain,
( spl22_13
| spl22_19 ),
inference(sat_conversion,[],[f989]) ).
cnf(s23,plain,
( ~ spl22_6
| ~ spl22_10
| ~ spl22_19
| spl22_24 ),
inference(sat_conversion,[],[f1029]) ).
cnf(s24,plain,
( ~ spl22_6
| ~ spl22_13
| ~ spl22_18
| spl22_25 ),
inference(sat_conversion,[],[f1061]) ).
cnf(s26,plain,
( ~ spl22_2
| spl22_27 ),
inference(sat_conversion,[],[f1169]) ).
cnf(s29,plain,
( ~ spl22_6
| ~ spl22_13
| ~ spl22_18
| spl22_20
| ~ spl22_25
| ~ spl22_27
| spl22_30 ),
inference(sat_conversion,[],[f1298]) ).
cnf(s30,plain,
( ~ spl22_8
| ~ spl22_10
| ~ spl22_16
| ~ spl22_17
| ~ spl22_30 ),
inference(sat_conversion,[],[f1322]) ).
cnf(s35,plain,
( ~ spl22_6
| ~ spl22_10
| ~ spl22_19
| spl22_35 ),
inference(sat_conversion,[],[f1453]) ).
cnf(s44,plain,
( ~ spl22_6
| ~ spl22_10
| ~ spl22_19
| spl22_44 ),
inference(sat_conversion,[],[f1790]) ).
cnf(s54,plain,
( ~ spl22_14
| ~ spl22_18
| spl22_52 ),
inference(sat_conversion,[],[f2044]) ).
cnf(s58,plain,
( ~ spl22_2
| ~ spl22_6
| spl22_11
| spl22_56 ),
inference(sat_conversion,[],[f2181]) ).
cnf(s72,plain,
( ~ spl22_2
| ~ spl22_56
| spl22_65 ),
inference(sat_conversion,[],[f2675]) ).
cnf(s76,plain,
( ~ spl22_2
| ~ spl22_18
| ~ spl22_52
| spl22_69 ),
inference(sat_conversion,[],[f2734]) ).
cnf(s144,plain,
( ~ spl22_52
| spl22_137 ),
inference(sat_conversion,[],[f5128]) ).
cnf(s146,plain,
( ~ spl22_2
| ~ spl22_6
| ~ spl22_52
| ~ spl22_65
| ~ spl22_69
| ~ spl22_137
| spl22_139 ),
inference(sat_conversion,[],[f5366]) ).
cnf(s147,plain,
( ~ spl22_1
| ~ spl22_17
| ~ spl22_24
| ~ spl22_35
| ~ spl22_44
| ~ spl22_139 ),
inference(sat_conversion,[],[f5412]) ).
cnf(s197,plain,
spl22_27,
inference(rat,[],[s26,s2]) ).
cnf(s198,plain,
spl22_14,
inference(rat,[],[s14,s2]) ).
cnf(s201,plain,
spl22_52,
inference(rat,[],[s54,s17,s198]) ).
cnf(s206,plain,
spl22_137,
inference(rat,[],[s144,s201]) ).
cnf(s208,plain,
spl22_69,
inference(rat,[],[s76,s2,s17,s201]) ).
cnf(s213,plain,
spl22_15,
inference(rat,[],[s13,s198,s1]) ).
cnf(s221,plain,
spl22_16,
inference(rat,[],[s15,s2,s9,s213]) ).
cnf(s225,plain,
~ spl22_30,
inference(rat,[],[s30,s7,s16,s9,s221]) ).
cnf(s228,plain,
( ~ spl22_19
| ~ spl22_139 ),
inference(rat,[],[s147,s23,s35,s44,s16,s1,s9,s5]) ).
cnf(s229,plain,
spl22_19,
inference(rat,[],[s19,s18,s29,s24,s21,s5,s2,s17,s197,s225]) ).
cnf(s235,plain,
~ spl22_139,
inference(rat,[],[s228,s229]) ).
cnf(s238,plain,
~ spl22_65,
inference(rat,[],[s146,s201,s206,s208,s2,s5,s235]) ).
cnf(s241,plain,
~ spl22_56,
inference(rat,[],[s72,s2,s238]) ).
cnf(s242,plain,
spl22_11,
inference(rat,[],[s58,s2,s5,s241]) ).
cnf(s243,plain,
spl22_3,
inference(rat,[],[s10,s2,s242]) ).
cnf(s244,plain,
spl22_13,
inference(rat,[],[s12,s243]) ).
cnf(s245,plain,
~ spl22_4,
inference(rat,[],[s3,s243]) ).
cnf(s246,plain,
spl22_25,
inference(rat,[],[s24,s5,s17,s244]) ).
cnf(s247,plain,
spl22_20,
inference(rat,[],[s29,s225,s197,s246,s5,s17,s244]) ).
cnf(s248,plain,
$false,
inference(rat,[],[s19,s2,s5,s247,s245]) ).
fof(f5413,plain,
$false,
inference(avatar_sat_refutation,[],[s248]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC283+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.18 % Computer : n003.cluster.edu
% 0.11/0.18 % Model : x86_64 x86_64
% 0.11/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.18 % Memory : 8046.5625MB
% 0.11/0.18 % OS : Linux 6.8.0-71-generic
% 0.11/0.19 % CPULimit : 300
% 0.11/0.19 % WCLimit : 300
% 0.11/0.19 % DateTime : Mon Sep 28 08:53:42 UTC 2026
% 0.11/0.19 % CPUTime :
% 0.11/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.22 Running first-order theorem proving
% 0.11/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.31/2.29 % (1441689)Detected formulas, will run a generic FOF schedule.
% 11.31/2.29 % (1441698)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3702619232:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.31/2.29 % (1441699)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1664051385:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.31/2.29 % (1441694)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2807408822:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.31/2.29 % (1441696)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3192948367:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.31/2.29 % (1441695)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3260665847:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.31/2.29 % (1441697)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1597531051:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.31/2.29 % (1441698)Instruction limit reached!
% 11.31/2.29 % (1441698)------------------------------
% 11.31/2.29 % (1441698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.29 % (1441698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.29 % (1441698)CaDiCaL version: 2.1.3
% 11.31/2.29 % (1441698)Termination reason: Instruction limit
% 11.31/2.29 % (1441698)Termination phase: Saturation
% 11.31/2.29 % (1441698)Time elapsed: 0.038 s
% 11.31/2.29 % (1441698)Peak memory usage: 88 MB
% 11.31/2.29 % (1441698)Instructions burned: 119 (million)
% 11.31/2.29 % (1441700)dis-21_1_sil=8000:lcm=predicate:random_seed=2461460677:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.31/2.29 % (1441697)Instruction limit reached!
% 11.31/2.29 % (1441697)------------------------------
% 11.31/2.29 % (1441697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.29 % (1441697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.29 % (1441697)CaDiCaL version: 2.1.3
% 11.31/2.29 % (1441697)Termination reason: Instruction limit
% 11.31/2.29 % (1441697)Termination phase: Saturation
% 11.31/2.29 % (1441697)Time elapsed: 0.072 s
% 11.31/2.29 % (1441697)Peak memory usage: 89 MB
% 11.31/2.29 % (1441697)Instructions burned: 110 (million)
% 11.31/2.29 % (1441700)Instruction limit reached!
% 11.31/2.29 % (1441700)------------------------------
% 11.31/2.29 % (1441700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.29 % (1441700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.29 % (1441700)CaDiCaL version: 2.1.3
% 11.31/2.29 % (1441700)Termination reason: Instruction limit
% 11.31/2.29 % (1441700)Termination phase: Saturation
% 11.31/2.29 % (1441700)Time elapsed: 0.070 s
% 11.31/2.29 % (1441700)Peak memory usage: 91 MB
% 11.31/2.29 % (1441700)Instructions burned: 129 (million)
% 11.31/2.29 % (1441699)Instruction limit reached!
% 11.31/2.29 % (1441699)------------------------------
% 11.31/2.29 % (1441699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.29 % (1441699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.29 % (1441699)CaDiCaL version: 2.1.3
% 11.31/2.29 % (1441699)Termination reason: Instruction limit
% 11.31/2.29 % (1441699)Termination phase: Saturation
% 11.31/2.29 % (1441699)Time elapsed: 0.093 s
% 11.31/2.29 % (1441699)Peak memory usage: 90 MB
% 11.31/2.29 % (1441699)Instructions burned: 140 (million)
% 11.31/2.29 % (1441707)lrs+10_1_sil=8000:sp=occurrence:random_seed=2557456930:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 11.31/2.29 % (1441707)Instruction limit reached!
% 11.31/2.29 % (1441707)------------------------------
% 11.31/2.29 % (1441707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.29 % (1441707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.29 % (1441707)CaDiCaL version: 2.1.3
% 11.31/2.29 % (1441707)Termination reason: Instruction limit
% 11.31/2.29 % (1441707)Termination phase: Saturation
% 11.31/2.29 % (1441707)Time elapsed: 0.090 s
% 11.31/2.29 % (1441707)Peak memory usage: 93 MB
% 11.31/2.29 % (1441707)Instructions burned: 288 (million)
% 12.63/2.43 % (1441710)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2571800150:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 12.63/2.43 % (1441709)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2971387314:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.63/2.43 % (1441711)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3087303240:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 12.63/2.43 % (1441713)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2449090664:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 12.63/2.43 % (1441709)Instruction limit reached!
% 12.63/2.43 % (1441709)------------------------------
% 12.63/2.43 % (1441709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.43 % (1441709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.43 % (1441709)CaDiCaL version: 2.1.3
% 12.63/2.43 % (1441709)Termination reason: Instruction limit
% 12.63/2.43 % (1441709)Termination phase: Saturation
% 12.63/2.43 % (1441709)Time elapsed: 0.084 s
% 12.63/2.43 % (1441709)Peak memory usage: 94 MB
% 12.63/2.43 % (1441709)Instructions burned: 158 (million)
% 12.63/2.43 % (1441711)Instruction limit reached!
% 12.63/2.43 % (1441711)------------------------------
% 12.63/2.43 % (1441711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.43 % (1441711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.43 % (1441711)CaDiCaL version: 2.1.3
% 12.63/2.43 % (1441711)Termination reason: Instruction limit
% 12.63/2.43 % (1441711)Termination phase: Saturation
% 12.63/2.43 % (1441711)Time elapsed: 0.121 s
% 12.63/2.43 % (1441711)Peak memory usage: 95 MB
% 12.63/2.43 % (1441711)Instructions burned: 249 (million)
% 12.63/2.43 % (1441713)Instruction limit reached!
% 12.63/2.43 % (1441713)------------------------------
% 12.63/2.43 % (1441713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.43 % (1441713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.43 % (1441713)CaDiCaL version: 2.1.3
% 12.63/2.43 % (1441713)Termination reason: Instruction limit
% 12.63/2.43 % (1441713)Termination phase: Saturation
% 12.63/2.43 % (1441713)Time elapsed: 0.094 s
% 12.63/2.43 % (1441713)Peak memory usage: 90 MB
% 12.63/2.43 % (1441713)Instructions burned: 297 (million)
% 12.63/2.43 % (1441710)Instruction limit reached!
% 12.63/2.43 % (1441710)------------------------------
% 12.63/2.43 % (1441710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.43 % (1441710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.43 % (1441710)CaDiCaL version: 2.1.3
% 12.63/2.43 % (1441710)Termination reason: Instruction limit
% 12.63/2.43 % (1441710)Termination phase: Saturation
% 12.63/2.43 % (1441710)Time elapsed: 0.202 s
% 12.63/2.43 % (1441710)Peak memory usage: 92 MB
% 12.63/2.43 % (1441710)Instructions burned: 325 (million)
% 12.63/2.43 % (1441718)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1503054049:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 12.63/2.43 % (1441720)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=656175520:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 12.63/2.43 % (1441719)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=510886499:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 12.63/2.43 % (1441720)Instruction limit reached!
% 12.63/2.43 % (1441720)------------------------------
% 12.63/2.43 % (1441720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.43 % (1441720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.43 % (1441720)CaDiCaL version: 2.1.3
% 12.63/2.43 % (1441720)Termination reason: Instruction limit
% 12.63/2.43 % (1441720)Termination phase: Saturation
% 12.63/2.43 % (1441720)Time elapsed: 0.035 s
% 12.63/2.43 % (1441720)Peak memory usage: 90 MB
% 12.63/2.43 % (1441720)Instructions burned: 130 (million)
% 12.63/2.43 % (1441721)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1872818138:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 12.63/2.43 % (1441719)Instruction limit reached!
% 12.63/2.43 % (1441719)------------------------------
% 12.63/2.43 % (1441719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.43 % (1441719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.43 % (1441719)CaDiCaL version: 2.1.3
% 12.63/2.43 % (1441719)Termination reason: Instruction limit
% 12.63/2.43 % (1441719)Termination phase: Saturation
% 12.63/2.43 % (1441719)Time elapsed: 0.073 s
% 12.63/2.43 % (1441719)Peak memory usage: 90 MB
% 12.63/2.43 % (1441719)Instructions burned: 114 (million)
% 12.63/2.43 % (1441725)lrs+10_1_sil=8000:sp=occurrence:random_seed=411392146:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 12.63/2.43 % (1441721)Instruction limit reached!
% 12.63/2.43 % (1441721)------------------------------
% 12.63/2.43 % (1441721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.43 % (1441721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.43 % (1441721)CaDiCaL version: 2.1.3
% 12.63/2.43 % (1441721)Termination reason: Instruction limit
% 12.63/2.43 % (1441721)Termination phase: Saturation
% 12.63/2.43 % (1441721)Time elapsed: 0.068 s
% 12.63/2.43 % (1441721)Peak memory usage: 89 MB
% 12.63/2.43 % (1441721)Instructions burned: 115 (million)
% 12.63/2.43 % (1441727)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=800818844:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 12.63/2.43 % (1441729)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=812500164:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 12.63/2.43 % (1441725)Instruction limit reached!
% 12.63/2.43 % (1441725)------------------------------
% 12.63/2.43 % (1441725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.43 % (1441725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.43 % (1441725)CaDiCaL version: 2.1.3
% 12.63/2.43 % (1441725)Termination reason: Instruction limit
% 12.63/2.43 % (1441725)Termination phase: Saturation
% 12.63/2.43 % (1441725)Time elapsed: 0.263 s
% 12.63/2.43 % (1441725)Peak memory usage: 100 MB
% 12.63/2.43 % (1441725)Instructions burned: 907 (million)
% 12.63/2.43 % (1441727)Instruction limit reached!
% 12.63/2.43 % (1441727)------------------------------
% 12.63/2.43 % (1441727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.43 % (1441727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.43 % (1441727)CaDiCaL version: 2.1.3
% 12.63/2.43 % (1441727)Termination reason: Instruction limit
% 12.63/2.43 % (1441727)Termination phase: Saturation
% 12.63/2.43 % (1441727)Time elapsed: 0.254 s
% 12.63/2.43 % (1441727)Peak memory usage: 92 MB
% 12.63/2.43 % (1441727)Instructions burned: 437 (million)
% 12.63/2.43 % (1441732)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=34030824:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2990 on theBenchmark for (2990ds/134Mi)
% 12.63/2.43 % (1441732)Instruction limit reached!
% 12.63/2.43 % (1441732)------------------------------
% 12.63/2.43 % (1441732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.43 % (1441732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.43 % (1441732)CaDiCaL version: 2.1.3
% 12.63/2.43 % (1441732)Termination reason: Instruction limit
% 12.63/2.43 % (1441732)Termination phase: Saturation
% 12.63/2.43 % (1441732)Time elapsed: 0.034 s
% 12.63/2.43 % (1441732)Peak memory usage: 90 MB
% 12.63/2.43 % (1441732)Instructions burned: 136 (million)
% 12.63/2.43 % (1441735)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2121481449:st=3:i=13193:sd=3:ss=axioms_2988 on theBenchmark for (2988ds/13193Mi)
% 12.63/2.43 % (1441734)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2140136042:st=8:i=592:sd=3:ep=RST:ss=axioms_2989 on theBenchmark for (2989ds/592Mi)
% 12.63/2.43 % (1441696)First to succeed.
% 12.63/2.43 % (1441696)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1441689"
% 12.63/2.43 % (1441734)Instruction limit reached!
% 12.63/2.43 % (1441734)------------------------------
% 12.63/2.43 % (1441734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.43 % (1441734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.43 % (1441734)CaDiCaL version: 2.1.3
% 12.63/2.43 % (1441734)Termination reason: Instruction limit
% 12.63/2.43 % (1441734)Termination phase: Saturation
% 12.63/2.43 % (1441734)Time elapsed: 0.320 s
% 12.63/2.43 % (1441734)Peak memory usage: 95 MB
% 12.63/2.43 % (1441734)Instructions burned: 593 (million)
% 12.63/2.43 % (1441738)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3411641668:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi)
% 12.63/2.43 % (1441738)Instruction limit reached!
% 12.63/2.43 % (1441738)------------------------------
% 12.63/2.43 % (1441738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.43 % (1441738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.43 % (1441738)CaDiCaL version: 2.1.3
% 12.63/2.43 % (1441738)Termination reason: Instruction limit
% 12.63/2.43 % (1441738)Termination phase: Saturation
% 12.63/2.43 % (1441738)Time elapsed: 0.038 s
% 12.63/2.43 % (1441738)Peak memory usage: 91 MB
% 12.63/2.43 % (1441738)Instructions burned: 129 (million)
% 12.63/2.43 % (1441696)Refutation found. Thanks to Tanya!
% 12.63/2.43 % SZS status Theorem for theBenchmark
% 12.63/2.43 % SZS output start Proof for theBenchmark
% See solution above
% 13.02/2.52 % (1441696)------------------------------
% 13.02/2.52 % (1441696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.02/2.52 % (1441696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.02/2.52 % (1441696)CaDiCaL version: 2.1.3
% 13.02/2.52 % (1441696)Termination reason: Refutation
% 13.02/2.52 % (1441696)Time elapsed: 1.352 s
% 13.02/2.52 % (1441696)Peak memory usage: 142 MB
% 13.02/2.52 % (1441696)Instructions burned: 2103 (million)
% 13.02/2.52 % (1441696)------------------------------
% 13.02/2.52 % (1441696)------------------------------
% 13.02/2.52 % (1441689)Success in time 1.766 s
% 13.02/2.52 % Vampire exiting
%------------------------------------------------------------------------------