%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWC161+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 : n020.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:02:43 PM UTC 2026
% Result : Theorem 8.51s 2.06s
% Output : Refutation 8.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 27
% Syntax : Number of formulae : 197 ( 37 unt; 16 def)
% Number of atoms : 762 ( 112 equ)
% Maximal formula atoms : 38 ( 3 avg)
% Number of connectives : 970 ( 405 ~; 400 |; 102 &)
% ( 21 <=>; 42 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 17 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 13 con; 0-2 aty)
% Number of variables : 188 ( 0 sgn 150 !; 38 ?)
% Comments :
%------------------------------------------------------------------------------
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(f29,axiom,
! [X0] :
( ssItem(X0)
=> ! [X1] :
( ssItem(X1)
=> ( ( leq(X0,X1)
& leq(X1,X0) )
=> X0 = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax29) ).
fof(f80,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ( app(X1,X2) = app(X1,X0)
=> X2 = X0 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax80) ).
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(f90,axiom,
! [X0] :
( ssItem(X0)
=> ~ lt(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax90) ).
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)
=> ! [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) ) ) ) ) ) )
| ! [X14] :
( ssItem(X14)
=> ! [X15] :
( ssItem(X15)
=> ! [X16] :
( ssList(X16)
=> ! [X17] :
( ssList(X17)
=> ! [X18] :
( ~ ssList(X18)
| app(app(app(app(X16,cons(X14,nil)),X17),cons(X15,nil)),X18) != X0
| ~ leq(X15,X14)
| ( ! [X19] :
( ~ ssItem(X19)
| ~ memberP(X17,X19)
| ( leq(X14,X19)
& leq(X19,X15) ) )
& leq(X14,X15) ) ) ) ) ) )
| ( 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)
=> ! [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) ) ) ) ) ) )
| ! [X14] :
( ssItem(X14)
=> ! [X15] :
( ssItem(X15)
=> ! [X16] :
( ssList(X16)
=> ! [X17] :
( ssList(X17)
=> ! [X18] :
( ~ ssList(X18)
| app(app(app(app(X16,cons(X14,nil)),X17),cons(X15,nil)),X18) != X0
| ~ leq(X15,X14)
| ( ! [X19] :
( ~ ssItem(X19)
| ~ memberP(X17,X19)
| ( leq(X14,X19)
& leq(X19,X15) ) )
& leq(X14,X15) ) ) ) ) ) )
| ( nil != X3
& nil = X2 ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f98,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ssList(X3)
& X1 = X3
& X0 = X2
& ? [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) ) ) ) ) )
& ssList(X4) )
& ? [X14] :
( ? [X15] :
( ? [X16] :
( ? [X17] :
( ? [X18] :
( ssList(X18)
& app(app(app(app(X16,cons(X14,nil)),X17),cons(X15,nil)),X18) = X0
& leq(X15,X14)
& ( ? [X19] :
( ssItem(X19)
& memberP(X17,X19)
& ( ~ leq(X14,X19)
| ~ leq(X19,X15) ) )
| ~ leq(X14,X15) ) )
& ssList(X17) )
& ssList(X16) )
& ssItem(X15) )
& ssItem(X14) )
& ( nil = X3
| nil != X2 ) )
& ssList(X2) )
& ssList(X1) )
& ssList(X0) ),
inference(ennf_transformation,[],[f97]) ).
fof(f105,plain,
! [X0] :
( ! [X1] :
( ssList(cons(X1,X0))
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f108,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(f109,plain,
! [X0] :
( ! [X1] :
( cons(X1,X0) = app(cons(X1,nil),X0)
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f81]) ).
fof(f110,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X2 = X0
| app(X1,X2) != app(X1,X0)
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f80]) ).
fof(f111,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X2 = X0
| app(X1,X2) != app(X1,X0)
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(flattening,[],[f110]) ).
fof(f116,plain,
! [X0] :
( ! [X1] :
( ssList(app(X0,X1))
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f124,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ~ leq(X0,X1)
| ~ leq(X1,X0)
| ~ ssItem(X1) )
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f29]) ).
fof(f125,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ~ leq(X0,X1)
| ~ leq(X1,X0)
| ~ ssItem(X1) )
| ~ ssItem(X0) ),
inference(flattening,[],[f124]) ).
fof(f126,plain,
! [X0] :
( ! [X1] :
( ( lt(X0,X1)
<=> ( X0 != X1
& leq(X0,X1) ) )
| ~ ssItem(X1) )
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f93]) ).
fof(f131,plain,
! [X0] :
( ~ lt(X0,X0)
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f90]) ).
fof(f138,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(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(flattening,[],[f138]) ).
fof(f140,plain,
( ssList(sK3)
& sK1 = sK3
& sK0 = sK2
& ssList(sK5)
& sK3 = app(app(sK4,sK2),sK5)
& strictorderedP(sK2)
& ! [X6] :
( ~ ssItem(X6)
| ! [X7] :
( ~ ssList(X7)
| app(X7,cons(X6,nil)) != sK4
| ! [X8] :
( ~ ssItem(X8)
| ! [X9] :
( ~ ssList(X9)
| app(cons(X8,nil),X9) != sK2
| ~ lt(X6,X8) ) ) ) )
& ! [X10] :
( ~ ssItem(X10)
| ! [X11] :
( ~ ssList(X11)
| app(cons(X10,nil),X11) != sK5
| ! [X12] :
( ~ ssItem(X12)
| ! [X13] :
( ~ ssList(X13)
| app(X13,cons(X12,nil)) != sK2
| ~ lt(X12,X10) ) ) ) )
& ssList(sK4)
& ssList(sK10)
& sK0 = app(app(app(app(sK8,cons(sK6,nil)),sK9),cons(sK7,nil)),sK10)
& leq(sK7,sK6)
& ( ( ssItem(sK11)
& memberP(sK9,sK11)
& ( ~ leq(sK6,sK11)
| ~ leq(sK11,sK7) ) )
| ~ leq(sK6,sK7) )
& ssList(sK9)
& ssList(sK8)
& ssItem(sK7)
& ssItem(sK6)
& ( nil = sK3
| nil != sK2 )
& ssList(sK2)
& ssList(sK1)
& ssList(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X14,sK6),skolemize(X15,sK7),skolemize(X16,sK8),skolemize(X17,sK9),skolemize(X18,sK10),skolemize(X19,sK11)],[f98]) ).
fof(f152,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,[],[f126]) ).
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(flattening,[],[f152]) ).
fof(f156,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,[],[f139]) ).
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) ) )
& ( ! [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,[],[f156]) ).
fof(f158,plain,
! [X0] :
( ( ( strictorderedP(X0)
| ( ~ lt(sK18(X0),sK19(X0))
& app(app(sK20(X0),cons(sK18(X0),sK21(X0))),cons(sK19(X0),sK22(X0))) = X0
& ssList(sK22(X0))
& ssList(sK21(X0))
& ssList(sK20(X0))
& ssItem(sK19(X0))
& ssItem(sK18(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,[sK18,sK19,sK20,sK21,sK22]),skolemize(X1,sK18(X0)),skolemize(X2,sK19(X0)),skolemize(X3,sK20(X0)),skolemize(X4,sK21(X0)),skolemize(X5,sK22(X0))],[f157]) ).
fof(f159,plain,
ssList(sK0),
inference(cnf_transformation,[],[f140]) ).
fof(f163,plain,
ssItem(sK6),
inference(cnf_transformation,[],[f140]) ).
fof(f164,plain,
ssItem(sK7),
inference(cnf_transformation,[],[f140]) ).
fof(f165,plain,
ssList(sK8),
inference(cnf_transformation,[],[f140]) ).
fof(f166,plain,
ssList(sK9),
inference(cnf_transformation,[],[f140]) ).
fof(f170,plain,
leq(sK7,sK6),
inference(cnf_transformation,[],[f140]) ).
fof(f171,plain,
sK0 = app(app(app(app(sK8,cons(sK6,nil)),sK9),cons(sK7,nil)),sK10),
inference(cnf_transformation,[],[f140]) ).
fof(f172,plain,
ssList(sK10),
inference(cnf_transformation,[],[f140]) ).
fof(f176,plain,
strictorderedP(sK2),
inference(cnf_transformation,[],[f140]) ).
fof(f179,plain,
sK0 = sK2,
inference(cnf_transformation,[],[f140]) ).
fof(f192,plain,
! [X0,X1] :
( ssList(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f197,plain,
! [X2,X0,X1] :
( app(app(X0,X1),X2) = app(X0,app(X1,X2))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f198,plain,
! [X0,X1] :
( cons(X1,X0) = app(cons(X1,nil),X0)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f109]) ).
fof(f199,plain,
! [X2,X0,X1] :
( app(X1,X2) != app(X1,X0)
| X0 = X2
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f203,plain,
! [X0,X1] :
( ssList(app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f204,plain,
ssList(nil),
inference(cnf_transformation,[],[f17]) ).
fof(f218,plain,
! [X0,X1] :
( ~ leq(X1,X0)
| ~ leq(X0,X1)
| X0 = X1
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f219,plain,
! [X0,X1] :
( leq(X0,X1)
| ~ lt(X0,X1)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f153]) ).
fof(f224,plain,
! [X0] :
( ~ lt(X0,X0)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f131]) ).
fof(f234,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,[],[f158]) ).
fof(f249,plain,
! [X10,X8,X6,X9,X7] :
( ~ strictorderedP(app(app(X8,cons(X6,X9)),cons(X7,X10)))
| ~ ssList(X10)
| ~ ssList(X9)
| ~ ssList(X8)
| ~ ssItem(X7)
| ~ ssItem(X6)
| lt(X6,X7)
| ~ ssList(app(app(X8,cons(X6,X9)),cons(X7,X10))) ),
inference(equality_resolution,[],[f234]) ).
fof(f261,definition,
( spl23_3
<=> leq(sK6,sK7) ),
introduced(definition,[new_symbols(definition,[spl23_3])],[avatar_definition]) ).
fof(f262,plain,
( ~ leq(sK6,sK7)
| spl23_3 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f278,plain,
( ~ leq(sK6,sK7)
| sK6 = sK7
| ~ ssItem(sK7)
| ~ ssItem(sK6) ),
inference(resolution,[],[f170,f218]) ).
fof(f279,plain,
( ~ leq(sK6,sK7)
| sK6 = sK7
| ~ ssItem(sK6) ),
inference(forward_subsumption_resolution,[],[f278,f164]) ).
fof(f280,plain,
( ~ leq(sK6,sK7)
| sK6 = sK7 ),
inference(forward_subsumption_resolution,[],[f279,f163]) ).
fof(f282,definition,
( spl23_8
<=> sK6 = sK7 ),
introduced(definition,[new_symbols(definition,[spl23_8])],[avatar_definition]) ).
fof(f283,plain,
( sK6 = sK7
| ~ spl23_8 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f284,plain,
( spl23_8
| ~ spl23_3 ),
inference(avatar_split_clause,[],[f280,f261,f282]) ).
fof(f285,plain,
strictorderedP(sK0),
inference(superposition,[],[f176,f179]) ).
fof(f289,plain,
( ~ lt(sK6,sK7)
| ~ ssItem(sK7)
| ~ ssItem(sK6)
| spl23_3 ),
inference(resolution,[],[f262,f219]) ).
fof(f292,plain,
( ~ lt(sK6,sK7)
| ~ ssItem(sK6)
| spl23_3 ),
inference(forward_subsumption_resolution,[],[f289,f164]) ).
fof(f294,plain,
( ~ lt(sK6,sK7)
| spl23_3 ),
inference(forward_subsumption_resolution,[],[f292,f163]) ).
fof(f378,plain,
( sK0 = app(app(app(sK8,app(cons(sK6,nil),sK9)),cons(sK7,nil)),sK10)
| ~ ssList(sK9)
| ~ ssList(cons(sK6,nil))
| ~ ssList(sK8) ),
inference(superposition,[],[f171,f197]) ).
fof(f380,plain,
( sK0 = app(app(app(sK8,cons(sK6,nil)),sK9),app(cons(sK7,nil),sK10))
| ~ ssList(sK10)
| ~ ssList(cons(sK7,nil))
| ~ ssList(app(app(sK8,cons(sK6,nil)),sK9)) ),
inference(superposition,[],[f171,f197]) ).
fof(f402,plain,
( sK0 = app(app(app(sK8,cons(sK6,nil)),sK9),app(cons(sK7,nil),sK10))
| ~ ssList(cons(sK7,nil))
| ~ ssList(app(app(sK8,cons(sK6,nil)),sK9)) ),
inference(forward_subsumption_resolution,[],[f380,f172]) ).
fof(f404,plain,
( sK0 = app(app(app(sK8,app(cons(sK6,nil),sK9)),cons(sK7,nil)),sK10)
| ~ ssList(cons(sK6,nil))
| ~ ssList(sK8) ),
inference(forward_subsumption_resolution,[],[f378,f166]) ).
fof(f406,definition,
( spl23_19
<=> ssList(app(app(sK8,cons(sK6,nil)),sK9)) ),
introduced(definition,[new_symbols(definition,[spl23_19])],[avatar_definition]) ).
fof(f407,plain,
( ~ ssList(app(app(sK8,cons(sK6,nil)),sK9))
| spl23_19 ),
inference(avatar_component_clause,[],[f406]) ).
fof(f409,definition,
( spl23_20
<=> ssList(cons(sK7,nil)) ),
introduced(definition,[new_symbols(definition,[spl23_20])],[avatar_definition]) ).
fof(f410,plain,
( ~ ssList(cons(sK7,nil))
| spl23_20 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f412,definition,
( spl23_21
<=> sK0 = app(app(app(sK8,cons(sK6,nil)),sK9),app(cons(sK7,nil),sK10)) ),
introduced(definition,[new_symbols(definition,[spl23_21])],[avatar_definition]) ).
fof(f413,plain,
( sK0 = app(app(app(sK8,cons(sK6,nil)),sK9),app(cons(sK7,nil),sK10))
| ~ spl23_21 ),
inference(avatar_component_clause,[],[f412]) ).
fof(f444,plain,
( ~ spl23_19
| ~ spl23_20
| spl23_21 ),
inference(avatar_split_clause,[],[f402,f412,f409,f406]) ).
fof(f452,plain,
( sK0 = app(app(app(sK8,app(cons(sK6,nil),sK9)),cons(sK7,nil)),sK10)
| ~ ssList(cons(sK6,nil)) ),
inference(forward_subsumption_resolution,[],[f404,f165]) ).
fof(f454,definition,
( spl23_31
<=> ssList(cons(sK6,nil)) ),
introduced(definition,[new_symbols(definition,[spl23_31])],[avatar_definition]) ).
fof(f455,plain,
( ~ ssList(cons(sK6,nil))
| spl23_31 ),
inference(avatar_component_clause,[],[f454]) ).
fof(f457,definition,
( spl23_32
<=> sK0 = app(app(app(sK8,app(cons(sK6,nil),sK9)),cons(sK7,nil)),sK10) ),
introduced(definition,[new_symbols(definition,[spl23_32])],[avatar_definition]) ).
fof(f458,plain,
( sK0 = app(app(app(sK8,app(cons(sK6,nil),sK9)),cons(sK7,nil)),sK10)
| ~ spl23_32 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f459,plain,
( ~ spl23_31
| spl23_32 ),
inference(avatar_split_clause,[],[f452,f457,f454]) ).
fof(f461,plain,
( ~ ssItem(sK7)
| ~ ssList(nil)
| spl23_20 ),
inference(resolution,[],[f410,f192]) ).
fof(f462,plain,
( ~ ssList(nil)
| spl23_20 ),
inference(forward_subsumption_resolution,[],[f461,f164]) ).
fof(f463,plain,
( $false
| spl23_20 ),
inference(forward_subsumption_resolution,[],[f462,f204]) ).
fof(f464,plain,
spl23_20,
inference(avatar_contradiction_clause,[],[f463]) ).
fof(f466,plain,
( ~ ssItem(sK6)
| ~ ssList(nil)
| spl23_31 ),
inference(resolution,[],[f455,f192]) ).
fof(f467,plain,
( ~ ssList(nil)
| spl23_31 ),
inference(forward_subsumption_resolution,[],[f466,f163]) ).
fof(f468,plain,
( $false
| spl23_31 ),
inference(forward_subsumption_resolution,[],[f467,f204]) ).
fof(f469,plain,
spl23_31,
inference(avatar_contradiction_clause,[],[f468]) ).
fof(f548,plain,
( ~ ssList(app(sK8,app(cons(sK6,nil),sK9)))
| ~ ssList(sK9)
| ~ ssList(cons(sK6,nil))
| ~ ssList(sK8)
| spl23_19 ),
inference(superposition,[],[f407,f197]) ).
fof(f549,plain,
( ~ ssList(app(sK8,app(cons(sK6,nil),sK9)))
| ~ ssList(cons(sK6,nil))
| ~ ssList(sK8)
| spl23_19 ),
inference(forward_subsumption_resolution,[],[f548,f166]) ).
fof(f551,plain,
( ~ ssList(app(sK8,app(cons(sK6,nil),sK9)))
| ~ ssList(cons(sK6,nil))
| spl23_19 ),
inference(forward_subsumption_resolution,[],[f549,f165]) ).
fof(f554,definition,
( spl23_40
<=> ssList(app(sK8,app(cons(sK6,nil),sK9))) ),
introduced(definition,[new_symbols(definition,[spl23_40])],[avatar_definition]) ).
fof(f555,plain,
( ~ ssList(app(sK8,app(cons(sK6,nil),sK9)))
| spl23_40 ),
inference(avatar_component_clause,[],[f554]) ).
fof(f556,plain,
( ~ spl23_31
| ~ spl23_40
| spl23_19 ),
inference(avatar_split_clause,[],[f551,f406,f554,f454]) ).
fof(f737,plain,
( sK0 = app(app(app(sK8,cons(sK6,nil)),sK9),cons(sK7,sK10))
| ~ ssItem(sK7)
| ~ ssList(sK10)
| ~ spl23_21 ),
inference(superposition,[],[f413,f198]) ).
fof(f743,plain,
( ! [X0] :
( sK0 != app(app(app(sK8,cons(sK6,nil)),sK9),X0)
| app(cons(sK7,nil),sK10) = X0
| ~ ssList(app(cons(sK7,nil),sK10))
| ~ ssList(app(app(sK8,cons(sK6,nil)),sK9))
| ~ ssList(X0) )
| ~ spl23_21 ),
inference(superposition,[],[f199,f413]) ).
fof(f754,definition,
( spl23_54
<=> ssList(app(cons(sK7,nil),sK10)) ),
introduced(definition,[new_symbols(definition,[spl23_54])],[avatar_definition]) ).
fof(f755,plain,
( ~ ssList(app(cons(sK7,nil),sK10))
| spl23_54 ),
inference(avatar_component_clause,[],[f754]) ).
fof(f774,definition,
( spl23_59
<=> ! [X0] :
( sK0 != app(app(app(sK8,cons(sK6,nil)),sK9),X0)
| ~ ssList(X0)
| app(cons(sK7,nil),sK10) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl23_59])],[avatar_definition]) ).
fof(f775,plain,
( ! [X0] :
( sK0 != app(app(app(sK8,cons(sK6,nil)),sK9),X0)
| ~ ssList(X0)
| app(cons(sK7,nil),sK10) = X0 )
| ~ spl23_59 ),
inference(avatar_component_clause,[],[f774]) ).
fof(f777,plain,
( ~ spl23_19
| ~ spl23_54
| spl23_59
| ~ spl23_21 ),
inference(avatar_split_clause,[],[f743,f412,f774,f754,f406]) ).
fof(f784,plain,
( sK0 = app(app(app(sK8,cons(sK6,nil)),sK9),cons(sK7,sK10))
| ~ ssList(sK10)
| ~ spl23_21 ),
inference(forward_subsumption_resolution,[],[f737,f164]) ).
fof(f792,plain,
( sK0 = app(app(app(sK8,cons(sK6,nil)),sK9),cons(sK7,sK10))
| ~ spl23_21 ),
inference(forward_subsumption_resolution,[],[f784,f172]) ).
fof(f878,plain,
( ~ ssList(cons(sK7,sK10))
| ~ ssItem(sK7)
| ~ ssList(sK10)
| spl23_54 ),
inference(superposition,[],[f755,f198]) ).
fof(f881,plain,
( ~ ssItem(sK7)
| ~ ssList(sK10)
| spl23_54 ),
inference(forward_subsumption_resolution,[],[f878,f192]) ).
fof(f884,plain,
( ~ ssList(sK10)
| spl23_54 ),
inference(forward_subsumption_resolution,[],[f881,f164]) ).
fof(f887,plain,
( $false
| spl23_54 ),
inference(forward_subsumption_resolution,[],[f884,f172]) ).
fof(f888,plain,
spl23_54,
inference(avatar_contradiction_clause,[],[f887]) ).
fof(f889,plain,
( sK0 = app(app(app(sK8,cons(sK6,sK9)),cons(sK7,nil)),sK10)
| ~ ssItem(sK6)
| ~ ssList(sK9)
| ~ spl23_32 ),
inference(superposition,[],[f458,f198]) ).
fof(f916,plain,
( sK0 = app(app(app(sK8,cons(sK6,sK9)),cons(sK7,nil)),sK10)
| ~ ssList(sK9)
| ~ spl23_32 ),
inference(forward_subsumption_resolution,[],[f889,f163]) ).
fof(f942,definition,
( spl23_76
<=> ssList(app(cons(sK6,nil),sK9)) ),
introduced(definition,[new_symbols(definition,[spl23_76])],[avatar_definition]) ).
fof(f943,plain,
( ~ ssList(app(cons(sK6,nil),sK9))
| spl23_76 ),
inference(avatar_component_clause,[],[f942]) ).
fof(f949,plain,
( sK0 = app(app(app(sK8,cons(sK6,sK9)),cons(sK7,nil)),sK10)
| ~ spl23_32 ),
inference(forward_subsumption_resolution,[],[f916,f166]) ).
fof(f1031,plain,
( ~ ssList(cons(sK6,sK9))
| ~ ssItem(sK6)
| ~ ssList(sK9)
| spl23_76 ),
inference(superposition,[],[f943,f198]) ).
fof(f1034,plain,
( ~ ssItem(sK6)
| ~ ssList(sK9)
| spl23_76 ),
inference(forward_subsumption_resolution,[],[f1031,f192]) ).
fof(f1037,plain,
( ~ ssList(sK9)
| spl23_76 ),
inference(forward_subsumption_resolution,[],[f1034,f163]) ).
fof(f1040,plain,
( $false
| spl23_76 ),
inference(forward_subsumption_resolution,[],[f1037,f166]) ).
fof(f1041,plain,
spl23_76,
inference(avatar_contradiction_clause,[],[f1040]) ).
fof(f1287,plain,
( ~ ssList(app(cons(sK6,nil),sK9))
| ~ ssList(sK8)
| spl23_40 ),
inference(resolution,[],[f555,f203]) ).
fof(f1292,plain,
( ~ ssList(app(cons(sK6,nil),sK9))
| spl23_40 ),
inference(forward_subsumption_resolution,[],[f1287,f165]) ).
fof(f1295,plain,
( ~ spl23_76
| spl23_40 ),
inference(avatar_split_clause,[],[f1292,f554,f942]) ).
fof(f1405,definition,
( spl23_108
<=> ssList(cons(sK7,sK10)) ),
introduced(definition,[new_symbols(definition,[spl23_108])],[avatar_definition]) ).
fof(f1406,plain,
( ~ ssList(cons(sK7,sK10))
| spl23_108 ),
inference(avatar_component_clause,[],[f1405]) ).
fof(f1449,plain,
( sK0 = app(app(sK8,cons(sK6,sK9)),app(cons(sK7,nil),sK10))
| ~ ssList(sK10)
| ~ ssList(cons(sK7,nil))
| ~ ssList(app(sK8,cons(sK6,sK9)))
| ~ spl23_32 ),
inference(superposition,[],[f949,f197]) ).
fof(f1479,plain,
( sK0 = app(app(sK8,cons(sK6,sK9)),app(cons(sK7,nil),sK10))
| ~ ssList(cons(sK7,nil))
| ~ ssList(app(sK8,cons(sK6,sK9)))
| ~ spl23_32 ),
inference(forward_subsumption_resolution,[],[f1449,f172]) ).
fof(f1482,definition,
( spl23_119
<=> ssList(app(sK8,cons(sK6,sK9))) ),
introduced(definition,[new_symbols(definition,[spl23_119])],[avatar_definition]) ).
fof(f1483,plain,
( ~ ssList(app(sK8,cons(sK6,sK9)))
| spl23_119 ),
inference(avatar_component_clause,[],[f1482]) ).
fof(f1485,definition,
( spl23_120
<=> sK0 = app(app(sK8,cons(sK6,sK9)),app(cons(sK7,nil),sK10)) ),
introduced(definition,[new_symbols(definition,[spl23_120])],[avatar_definition]) ).
fof(f1486,plain,
( sK0 = app(app(sK8,cons(sK6,sK9)),app(cons(sK7,nil),sK10))
| ~ spl23_120 ),
inference(avatar_component_clause,[],[f1485]) ).
fof(f1510,plain,
( ~ spl23_119
| ~ spl23_20
| spl23_120
| ~ spl23_32 ),
inference(avatar_split_clause,[],[f1479,f457,f1485,f409,f1482]) ).
fof(f1512,definition,
( spl23_126
<=> ssList(cons(sK6,sK9)) ),
introduced(definition,[new_symbols(definition,[spl23_126])],[avatar_definition]) ).
fof(f1513,plain,
( ~ ssList(cons(sK6,sK9))
| spl23_126 ),
inference(avatar_component_clause,[],[f1512]) ).
fof(f1518,plain,
( ~ ssItem(sK7)
| ~ ssList(sK10)
| spl23_108 ),
inference(resolution,[],[f1406,f192]) ).
fof(f1519,plain,
( ~ ssList(sK10)
| spl23_108 ),
inference(forward_subsumption_resolution,[],[f1518,f164]) ).
fof(f1520,plain,
( $false
| spl23_108 ),
inference(forward_subsumption_resolution,[],[f1519,f172]) ).
fof(f1521,plain,
spl23_108,
inference(avatar_contradiction_clause,[],[f1520]) ).
fof(f1625,plain,
( ~ ssItem(sK6)
| ~ ssList(sK9)
| spl23_126 ),
inference(resolution,[],[f1513,f192]) ).
fof(f1626,plain,
( ~ ssList(sK9)
| spl23_126 ),
inference(forward_subsumption_resolution,[],[f1625,f163]) ).
fof(f1627,plain,
( $false
| spl23_126 ),
inference(forward_subsumption_resolution,[],[f1626,f166]) ).
fof(f1628,plain,
spl23_126,
inference(avatar_contradiction_clause,[],[f1627]) ).
fof(f1631,plain,
( ~ ssList(cons(sK6,sK9))
| ~ ssList(sK8)
| spl23_119 ),
inference(resolution,[],[f1483,f203]) ).
fof(f1632,plain,
( ~ ssList(cons(sK6,sK9))
| spl23_119 ),
inference(forward_subsumption_resolution,[],[f1631,f165]) ).
fof(f1633,plain,
( ~ spl23_126
| spl23_119 ),
inference(avatar_split_clause,[],[f1632,f1482,f1512]) ).
fof(f2561,plain,
( sK0 != sK0
| ~ ssList(cons(sK7,sK10))
| app(cons(sK7,nil),sK10) = cons(sK7,sK10)
| ~ spl23_21
| ~ spl23_59 ),
inference(superposition,[],[f775,f792]) ).
fof(f2565,plain,
( ~ ssList(cons(sK7,sK10))
| app(cons(sK7,nil),sK10) = cons(sK7,sK10)
| ~ spl23_21
| ~ spl23_59 ),
inference(trivial_inequality_removal,[],[f2561]) ).
fof(f2573,definition,
( spl23_227
<=> app(cons(sK7,nil),sK10) = cons(sK7,sK10) ),
introduced(definition,[new_symbols(definition,[spl23_227])],[avatar_definition]) ).
fof(f2574,plain,
( app(cons(sK7,nil),sK10) = cons(sK7,sK10)
| ~ spl23_227 ),
inference(avatar_component_clause,[],[f2573]) ).
fof(f2575,plain,
( spl23_227
| ~ spl23_108
| ~ spl23_21
| ~ spl23_59 ),
inference(avatar_split_clause,[],[f2565,f774,f412,f1405,f2573]) ).
fof(f5367,plain,
( sK0 = app(app(sK8,cons(sK6,sK9)),cons(sK7,sK10))
| ~ spl23_120
| ~ spl23_227 ),
inference(forward_demodulation,[],[f1486,f2574]) ).
fof(f5393,plain,
( ~ strictorderedP(sK0)
| ~ ssList(sK10)
| ~ ssList(sK9)
| ~ ssList(sK8)
| ~ ssItem(sK7)
| ~ ssItem(sK6)
| lt(sK6,sK7)
| ~ ssList(sK0)
| ~ spl23_120
| ~ spl23_227 ),
inference(superposition,[],[f249,f5367]) ).
fof(f5414,plain,
( ~ ssList(sK10)
| ~ ssList(sK9)
| ~ ssList(sK8)
| ~ ssItem(sK7)
| ~ ssItem(sK6)
| lt(sK6,sK7)
| ~ ssList(sK0)
| ~ spl23_120
| ~ spl23_227 ),
inference(forward_subsumption_resolution,[],[f5393,f285]) ).
fof(f5440,plain,
( ~ ssList(sK9)
| ~ ssList(sK8)
| ~ ssItem(sK7)
| ~ ssItem(sK6)
| lt(sK6,sK7)
| ~ ssList(sK0)
| ~ spl23_120
| ~ spl23_227 ),
inference(forward_subsumption_resolution,[],[f5414,f172]) ).
fof(f5447,plain,
( ~ ssList(sK8)
| ~ ssItem(sK7)
| ~ ssItem(sK6)
| lt(sK6,sK7)
| ~ ssList(sK0)
| ~ spl23_120
| ~ spl23_227 ),
inference(forward_subsumption_resolution,[],[f5440,f166]) ).
fof(f5450,plain,
( ~ ssItem(sK7)
| ~ ssItem(sK6)
| lt(sK6,sK7)
| ~ ssList(sK0)
| ~ spl23_120
| ~ spl23_227 ),
inference(forward_subsumption_resolution,[],[f5447,f165]) ).
fof(f5451,plain,
( ~ ssItem(sK6)
| lt(sK6,sK7)
| ~ ssList(sK0)
| ~ spl23_120
| ~ spl23_227 ),
inference(forward_subsumption_resolution,[],[f5450,f164]) ).
fof(f5452,plain,
( lt(sK6,sK7)
| ~ ssList(sK0)
| ~ spl23_120
| ~ spl23_227 ),
inference(forward_subsumption_resolution,[],[f5451,f163]) ).
fof(f5453,plain,
( ~ ssList(sK0)
| spl23_3
| ~ spl23_120
| ~ spl23_227 ),
inference(forward_subsumption_resolution,[],[f5452,f294]) ).
fof(f5454,plain,
( $false
| spl23_3
| ~ spl23_120
| ~ spl23_227 ),
inference(forward_subsumption_resolution,[],[f5453,f159]) ).
fof(f5455,plain,
( spl23_3
| ~ spl23_120
| ~ spl23_227 ),
inference(avatar_contradiction_clause,[],[f5454]) ).
fof(f5456,plain,
( lt(sK6,sK7)
| ~ spl23_120
| ~ spl23_227 ),
inference(forward_subsumption_resolution,[],[f5452,f159]) ).
fof(f5572,plain,
( lt(sK6,sK6)
| ~ spl23_8
| ~ spl23_120
| ~ spl23_227 ),
inference(forward_demodulation,[],[f5456,f283]) ).
fof(f5586,plain,
( ~ ssItem(sK6)
| ~ spl23_8
| ~ spl23_120
| ~ spl23_227 ),
inference(resolution,[],[f5572,f224]) ).
fof(f5592,plain,
( $false
| ~ spl23_8
| ~ spl23_120
| ~ spl23_227 ),
inference(forward_subsumption_resolution,[],[f5586,f163]) ).
fof(f5593,plain,
( ~ spl23_8
| ~ spl23_120
| ~ spl23_227 ),
inference(avatar_contradiction_clause,[],[f5592]) ).
cnf(s5,plain,
( ~ spl23_3
| spl23_8 ),
inference(sat_conversion,[],[f284]) ).
cnf(s26,plain,
( ~ spl23_19
| ~ spl23_20
| spl23_21 ),
inference(sat_conversion,[],[f444]) ).
cnf(s28,plain,
( ~ spl23_31
| spl23_32 ),
inference(sat_conversion,[],[f459]) ).
cnf(s29,plain,
spl23_20,
inference(sat_conversion,[],[f464]) ).
cnf(s30,plain,
spl23_31,
inference(sat_conversion,[],[f469]) ).
cnf(s42,plain,
( spl23_19
| ~ spl23_31
| ~ spl23_40 ),
inference(sat_conversion,[],[f556]) ).
cnf(s67,plain,
( ~ spl23_19
| ~ spl23_21
| ~ spl23_54
| spl23_59 ),
inference(sat_conversion,[],[f777]) ).
cnf(s83,plain,
spl23_54,
inference(sat_conversion,[],[f888]) ).
cnf(s108,plain,
spl23_76,
inference(sat_conversion,[],[f1041]) ).
cnf(s136,plain,
( spl23_40
| ~ spl23_76 ),
inference(sat_conversion,[],[f1295]) ).
cnf(s159,plain,
( ~ spl23_20
| ~ spl23_32
| ~ spl23_119
| spl23_120 ),
inference(sat_conversion,[],[f1510]) ).
cnf(s161,plain,
spl23_108,
inference(sat_conversion,[],[f1521]) ).
cnf(s179,plain,
spl23_126,
inference(sat_conversion,[],[f1628]) ).
cnf(s180,plain,
( spl23_119
| ~ spl23_126 ),
inference(sat_conversion,[],[f1633]) ).
cnf(s319,plain,
( ~ spl23_21
| ~ spl23_59
| ~ spl23_108
| spl23_227 ),
inference(sat_conversion,[],[f2575]) ).
cnf(s740,plain,
( spl23_3
| ~ spl23_120
| ~ spl23_227 ),
inference(sat_conversion,[],[f5455]) ).
cnf(s746,plain,
( ~ spl23_8
| ~ spl23_120
| ~ spl23_227 ),
inference(sat_conversion,[],[f5593]) ).
cnf(s785,plain,
spl23_119,
inference(rat,[],[s180,s179]) ).
cnf(s789,plain,
( ~ spl23_20
| ~ spl23_32
| spl23_120 ),
inference(rat,[],[s159,s785]) ).
cnf(s801,plain,
spl23_40,
inference(rat,[],[s136,s108]) ).
cnf(s809,plain,
( ~ spl23_19
| ~ spl23_21
| spl23_59 ),
inference(rat,[],[s67,s83]) ).
cnf(s816,plain,
( spl23_19
| ~ spl23_31 ),
inference(rat,[],[s42,s801]) ).
cnf(s832,plain,
spl23_19,
inference(rat,[],[s816,s30]) ).
cnf(s848,plain,
spl23_32,
inference(rat,[],[s28,s30]) ).
cnf(s857,plain,
spl23_120,
inference(rat,[],[s789,s29,s848]) ).
cnf(s965,plain,
spl23_21,
inference(rat,[],[s26,s29,s832]) ).
cnf(s981,plain,
spl23_59,
inference(rat,[],[s809,s832,s965]) ).
cnf(s999,plain,
spl23_227,
inference(rat,[],[s319,s965,s161,s981]) ).
cnf(s1027,plain,
~ spl23_8,
inference(rat,[],[s746,s857,s999]) ).
cnf(s1028,plain,
spl23_3,
inference(rat,[],[s740,s857,s999]) ).
cnf(s1119,plain,
$false,
inference(rat,[],[s5,s1027,s1028]) ).
fof(f5594,plain,
$false,
inference(avatar_sat_refutation,[],[s1119]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC161+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 % Computer : n020.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Mon Sep 28 08:15:35 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.44 Running first-order theorem proving
% 0.12/0.44 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
% 8.51/2.06 % (29023)Detected formulas, will run a generic FOF schedule.
% 8.51/2.06 % (29033)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2762834317:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.51/2.06 % (29029)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=2412317755:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.51/2.06 % (29031)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1983414680:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.51/2.06 % (29030)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=115258357:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.51/2.06 % (29034)dis-21_1_sil=8000:lcm=predicate:random_seed=1359457036: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)
% 8.51/2.06 % (29028)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=94740771:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.51/2.06 % (29032)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2645604856:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.51/2.06 % (29033)Instruction limit reached!
% 8.51/2.06 % (29033)------------------------------
% 8.51/2.06 % (29033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.51/2.06 % (29033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/2.06 % (29033)CaDiCaL version: 2.1.3
% 8.51/2.06 % (29033)Termination reason: Instruction limit
% 8.51/2.06 % (29033)Termination phase: Saturation
% 8.51/2.06 % (29033)Time elapsed: 0.049 s
% 8.51/2.06 % (29033)Peak memory usage: 90 MB
% 8.51/2.06 % (29033)Instructions burned: 141 (million)
% 8.51/2.06 % (29034)Instruction limit reached!
% 8.51/2.06 % (29034)------------------------------
% 8.51/2.06 % (29034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.51/2.06 % (29034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/2.06 % (29034)CaDiCaL version: 2.1.3
% 8.51/2.06 % (29034)Termination reason: Instruction limit
% 8.51/2.06 % (29034)Termination phase: Saturation
% 8.51/2.06 % (29034)Time elapsed: 0.069 s
% 8.51/2.06 % (29034)Peak memory usage: 91 MB
% 8.51/2.06 % (29034)Instructions burned: 129 (million)
% 8.51/2.06 % (29032)Instruction limit reached!
% 8.51/2.06 % (29032)------------------------------
% 8.51/2.06 % (29032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.51/2.06 % (29032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/2.06 % (29032)CaDiCaL version: 2.1.3
% 8.51/2.06 % (29032)Termination reason: Instruction limit
% 8.51/2.06 % (29032)Termination phase: Saturation
% 8.51/2.06 % (29032)Time elapsed: 0.070 s
% 8.51/2.06 % (29032)Peak memory usage: 88 MB
% 8.51/2.06 % (29032)Instructions burned: 119 (million)
% 8.51/2.06 % (29031)Instruction limit reached!
% 8.51/2.06 % (29031)------------------------------
% 8.51/2.06 % (29031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.51/2.06 % (29031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/2.06 % (29031)CaDiCaL version: 2.1.3
% 8.51/2.06 % (29031)Termination reason: Instruction limit
% 8.51/2.06 % (29031)Termination phase: Saturation
% 8.51/2.06 % (29031)Time elapsed: 0.071 s
% 8.51/2.06 % (29031)Peak memory usage: 89 MB
% 8.51/2.06 % (29031)Instructions burned: 109 (million)
% 8.51/2.06 % (29042)lrs+10_1_sil=8000:sp=occurrence:random_seed=3913570005:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 8.51/2.06 % (29042)Instruction limit reached!
% 8.51/2.06 % (29042)------------------------------
% 8.51/2.06 % (29042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.51/2.06 % (29042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/2.06 % (29042)CaDiCaL version: 2.1.3
% 8.51/2.06 % (29042)Termination reason: Instruction limit
% 8.51/2.06 % (29042)Termination phase: Saturation
% 8.51/2.06 % (29042)Time elapsed: 0.086 s
% 8.51/2.06 % (29042)Peak memory usage: 93 MB
% 8.51/2.06 % (29042)Instructions burned: 287 (million)
% 8.51/2.06 % (29044)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2914363259:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 8.51/2.06 % (29045)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=3547647184:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 8.51/2.06 % (29043)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1286320367:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.51/2.06 % (29043)Instruction limit reached!
% 8.51/2.06 % (29043)------------------------------
% 8.51/2.06 % (29043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.51/2.06 % (29043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/2.06 % (29043)CaDiCaL version: 2.1.3
% 8.51/2.06 % (29043)Termination reason: Instruction limit
% 8.51/2.06 % (29043)Termination phase: Saturation
% 8.51/2.06 % (29043)Time elapsed: 0.083 s
% 8.51/2.06 % (29043)Peak memory usage: 94 MB
% 8.51/2.06 % (29043)Instructions burned: 157 (million)
% 8.51/2.06 % (29047)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3497361166:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 8.51/2.06 % (29045)Instruction limit reached!
% 8.51/2.06 % (29045)------------------------------
% 8.51/2.06 % (29045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.51/2.06 % (29045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/2.06 % (29045)CaDiCaL version: 2.1.3
% 8.51/2.06 % (29045)Termination reason: Instruction limit
% 8.51/2.06 % (29045)Termination phase: Saturation
% 8.51/2.06 % (29045)Time elapsed: 0.125 s
% 8.51/2.06 % (29045)Peak memory usage: 98 MB
% 8.51/2.06 % (29045)Instructions burned: 248 (million)
% 8.51/2.06 % (29047)Instruction limit reached!
% 8.51/2.06 % (29047)------------------------------
% 8.51/2.06 % (29047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.51/2.06 % (29047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/2.06 % (29047)CaDiCaL version: 2.1.3
% 8.51/2.06 % (29047)Termination reason: Instruction limit
% 8.51/2.06 % (29047)Termination phase: Saturation
% 8.51/2.06 % (29047)Time elapsed: 0.094 s
% 8.51/2.06 % (29047)Peak memory usage: 90 MB
% 8.51/2.06 % (29047)Instructions burned: 295 (million)
% 8.51/2.06 % (29044)Instruction limit reached!
% 8.51/2.06 % (29044)------------------------------
% 8.51/2.06 % (29044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.51/2.06 % (29044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/2.06 % (29044)CaDiCaL version: 2.1.3
% 8.51/2.06 % (29044)Termination reason: Instruction limit
% 8.51/2.06 % (29044)Termination phase: Saturation
% 8.51/2.06 % (29044)Time elapsed: 0.201 s
% 8.51/2.06 % (29044)Peak memory usage: 92 MB
% 8.51/2.06 % (29044)Instructions burned: 325 (million)
% 8.51/2.06 % (29052)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=769490174:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 8.51/2.06 % (29053)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2661741020:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 8.51/2.06 % (29054)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=256554379:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 8.51/2.06 % (29054)Instruction limit reached!
% 8.51/2.06 % (29054)------------------------------
% 8.51/2.06 % (29054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.51/2.06 % (29054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/2.06 % (29054)CaDiCaL version: 2.1.3
% 8.51/2.06 % (29054)Termination reason: Instruction limit
% 8.51/2.06 % (29054)Termination phase: Saturation
% 8.51/2.06 % (29054)Time elapsed: 0.034 s
% 8.51/2.06 % (29054)Peak memory usage: 90 MB
% 8.51/2.06 % (29054)Instructions burned: 130 (million)
% 8.51/2.06 % (29055)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2483657305:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 8.51/2.06 % (29053)Instruction limit reached!
% 8.51/2.06 % (29053)------------------------------
% 8.51/2.06 % (29053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.51/2.06 % (29053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/2.06 % (29053)CaDiCaL version: 2.1.3
% 8.51/2.06 % (29053)Termination reason: Instruction limit
% 8.51/2.06 % (29053)Termination phase: Saturation
% 8.51/2.06 % (29053)Time elapsed: 0.073 s
% 8.51/2.06 % (29053)Peak memory usage: 91 MB
% 8.51/2.06 % (29053)Instructions burned: 114 (million)
% 8.51/2.06 % (29059)lrs+10_1_sil=8000:sp=occurrence:random_seed=3686957981:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 8.51/2.06 % (29055)Instruction limit reached!
% 8.51/2.06 % (29055)------------------------------
% 8.51/2.06 % (29055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.51/2.06 % (29055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/2.06 % (29055)CaDiCaL version: 2.1.3
% 8.51/2.06 % (29055)Termination reason: Instruction limit
% 8.51/2.06 % (29055)Termination phase: Saturation
% 8.51/2.06 % (29055)Time elapsed: 0.068 s
% 8.51/2.06 % (29055)Peak memory usage: 89 MB
% 8.51/2.06 % (29055)Instructions burned: 114 (million)
% 8.51/2.06 % (29061)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=917074254:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi)
% 8.51/2.06 % (29063)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2419302975:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 8.51/2.06 % (29061)First to succeed.
% 8.51/2.06 % (29061)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-29023"
% 8.51/2.06 % (29059)Instruction limit reached!
% 8.51/2.06 % (29059)------------------------------
% 8.51/2.06 % (29059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.51/2.06 % (29059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/2.06 % (29059)CaDiCaL version: 2.1.3
% 8.51/2.06 % (29059)Termination reason: Instruction limit
% 8.51/2.06 % (29059)Termination phase: Saturation
% 8.51/2.06 % (29059)Time elapsed: 0.261 s
% 8.51/2.06 % (29059)Peak memory usage: 99 MB
% 8.51/2.06 % (29059)Instructions burned: 911 (million)
% 8.51/2.06 % (29066)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1376839500:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 8.51/2.06 % (29066)Instruction limit reached!
% 8.51/2.06 % (29066)------------------------------
% 8.51/2.06 % (29066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.51/2.06 % (29066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.51/2.06 % (29066)CaDiCaL version: 2.1.3
% 8.51/2.06 % (29066)Termination reason: Instruction limit
% 8.51/2.06 % (29066)Termination phase: Saturation
% 8.51/2.06 % (29066)Time elapsed: 0.034 s
% 8.51/2.06 % (29066)Peak memory usage: 91 MB
% 8.51/2.06 % (29066)Instructions burned: 137 (million)
% 8.51/2.06 % (29061)Refutation found. Thanks to Tanya!
% 8.51/2.06 % SZS status Theorem for theBenchmark
% 8.51/2.06 % SZS output start Proof for theBenchmark
% See solution above
% 8.91/2.24 % (29061)------------------------------
% 8.91/2.24 % (29061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.91/2.24 % (29061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/2.24 % (29061)CaDiCaL version: 2.1.3
% 8.91/2.24 % (29061)Termination reason: Refutation
% 8.91/2.24 % (29061)Time elapsed: 0.117 s
% 8.91/2.24 % (29061)Peak memory usage: 92 MB
% 8.91/2.24 % (29061)Instructions burned: 191 (million)
% 8.91/2.24 % (29061)------------------------------
% 8.91/2.24 % (29061)------------------------------
% 8.91/2.24 % (29023)Success in time 1.179 s
% 8.91/2.24 % Vampire exiting
%------------------------------------------------------------------------------