%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC184+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:05:00 PM UTC 2026
% Result : Theorem 11.62s 2.07s
% Output : Refutation 11.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 54
% Syntax : Number of formulae : 431 ( 41 unt; 32 def)
% Number of atoms : 1602 ( 181 equ)
% Maximal formula atoms : 21 ( 3 avg)
% Number of connectives : 1899 ( 728 ~;1024 |; 42 &)
% ( 49 <=>; 56 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 41 ( 39 usr; 33 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-2 aty)
% Number of variables : 324 ( 0 sgn 302 !; 22 ?)
% 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/Axioms/SWC001+0.ax',ax3) ).
fof(f5,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( frontsegP(X0,X1)
<=> ? [X2] :
( ssList(X2)
& app(X1,X2) = X0 ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax5) ).
fof(f10,axiom,
! [X0] :
( ssList(X0)
=> ( strictorderP(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)
| lt(X2,X1) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax10) ).
fof(f16,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> ssList(cons(X1,X0)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax16) ).
fof(f17,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax17) ).
fof(f20,axiom,
! [X0] :
( ssList(X0)
=> ( nil = X0
| ? [X1] :
( ssList(X1)
& ? [X2] :
( ssItem(X2)
& cons(X2,X1) = X0 ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax20) ).
fof(f26,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ssList(app(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax26) ).
fof(f28,axiom,
! [X0] :
( ssList(X0)
=> app(nil,X0) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax28) ).
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/Axioms/SWC001+0.ax',ax36) ).
fof(f37,axiom,
! [X0] :
( ssItem(X0)
=> ! [X1] :
( ssItem(X1)
=> ! [X2] :
( ssList(X2)
=> ( memberP(cons(X1,X2),X0)
<=> ( X0 = X1
| memberP(X2,X0) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax37) ).
fof(f38,axiom,
! [X0] :
( ssItem(X0)
=> ~ memberP(nil,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax38) ).
fof(f41,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( ( frontsegP(X0,X1)
& frontsegP(X1,X0) )
=> X0 = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax41) ).
fof(f43,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ( frontsegP(X0,X1)
=> frontsegP(app(X0,X2),X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax43) ).
fof(f44,axiom,
! [X0] :
( ssItem(X0)
=> ! [X1] :
( ssItem(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ( frontsegP(cons(X0,X2),cons(X1,X3))
<=> ( X0 = X1
& frontsegP(X2,X3) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax44) ).
fof(f45,axiom,
! [X0] :
( ssList(X0)
=> frontsegP(X0,nil) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax45) ).
fof(f46,axiom,
! [X0] :
( ssList(X0)
=> ( frontsegP(nil,X0)
<=> nil = X0 ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax46) ).
fof(f63,axiom,
! [X0] :
( ssItem(X0)
=> strictorderP(cons(X0,nil)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax63) ).
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/Axioms/SWC001+0.ax',ax80) ).
fof(f83,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ( nil = app(X0,X1)
<=> ( nil = X1
& nil = X0 ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax83) ).
fof(f84,axiom,
! [X0] :
( ssList(X0)
=> app(X0,nil) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax84) ).
fof(f90,axiom,
! [X0] :
( ssItem(X0)
=> ~ lt(X0,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax90) ).
fof(f96,conjecture,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ~ ssList(X3)
| X1 != X3
| X0 != X2
| ! [X4] :
( ssItem(X4)
=> ! [X5] :
( ssList(X5)
=> ! [X6] :
( ~ ssList(X6)
| app(app(X5,cons(X4,nil)),X6) != X0
| ( ~ memberP(X5,X4)
& ~ memberP(X6,X4) ) ) ) )
| ( ! [X7] :
( ~ ssItem(X7)
| cons(X7,nil) != X2
| ~ memberP(X3,X7)
| ? [X8] :
( ssItem(X8)
& X7 != X8
& memberP(X3,X8)
& leq(X8,X7) ) )
& ( 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] :
( ssItem(X4)
=> ! [X5] :
( ssList(X5)
=> ! [X6] :
( ~ ssList(X6)
| app(app(X5,cons(X4,nil)),X6) != X0
| ( ~ memberP(X5,X4)
& ~ memberP(X6,X4) ) ) ) )
| ( ! [X7] :
( ~ ssItem(X7)
| cons(X7,nil) != X2
| ~ memberP(X3,X7)
| ? [X8] :
( ssItem(X8)
& X7 != X8
& memberP(X3,X8)
& leq(X8,X7) ) )
& ( nil != X3
| nil != X2 ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f99,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(f101,plain,
! [X0] :
( ! [X1] :
( ( frontsegP(X0,X1)
<=> ? [X2] :
( ssList(X2)
& app(X1,X2) = X0 ) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f5]) ).
fof(f108,plain,
! [X0] :
( ( strictorderP(X0)
<=> ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( lt(X1,X2)
| lt(X2,X1)
| 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,[],[f10]) ).
fof(f109,plain,
! [X0] :
( ( strictorderP(X0)
<=> ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( lt(X1,X2)
| lt(X2,X1)
| app(app(X3,cons(X1,X4)),cons(X2,X5)) != X0
| ~ ssList(X5) )
| ~ ssList(X4) )
| ~ ssList(X3) )
| ~ ssItem(X2) )
| ~ ssItem(X1) ) )
| ~ ssList(X0) ),
inference(flattening,[],[f108]) ).
fof(f119,plain,
! [X0] :
( ! [X1] :
( ssList(cons(X1,X0))
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f123,plain,
! [X0] :
( nil = X0
| ? [X1] :
( ssList(X1)
& ? [X2] :
( ssItem(X2)
& cons(X2,X1) = X0 ) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f124,plain,
! [X0] :
( nil = X0
| ? [X1] :
( ssList(X1)
& ? [X2] :
( ssItem(X2)
& cons(X2,X1) = X0 ) )
| ~ ssList(X0) ),
inference(flattening,[],[f123]) ).
fof(f132,plain,
! [X0] :
( ! [X1] :
( ssList(app(X0,X1))
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f134,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f28]) ).
fof(f146,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(f147,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( memberP(cons(X1,X2),X0)
<=> ( X0 = X1
| memberP(X2,X0) ) )
| ~ ssList(X2) )
| ~ ssItem(X1) )
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f148,plain,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f38]) ).
fof(f151,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f41]) ).
fof(f152,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(flattening,[],[f151]) ).
fof(f154,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( frontsegP(app(X0,X2),X1)
| ~ frontsegP(X0,X1)
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f43]) ).
fof(f155,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( frontsegP(app(X0,X2),X1)
| ~ frontsegP(X0,X1)
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(flattening,[],[f154]) ).
fof(f156,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( frontsegP(cons(X0,X2),cons(X1,X3))
<=> ( X0 = X1
& frontsegP(X2,X3) ) )
| ~ ssList(X3) )
| ~ ssList(X2) )
| ~ ssItem(X1) )
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f44]) ).
fof(f157,plain,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f45]) ).
fof(f158,plain,
! [X0] :
( ( frontsegP(nil,X0)
<=> nil = X0 )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f46]) ).
fof(f179,plain,
! [X0] :
( strictorderP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f63]) ).
fof(f196,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X2 = X0
| app(X1,X2) != app(X1,X0)
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f80]) ).
fof(f197,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X2 = X0
| app(X1,X2) != app(X1,X0)
| ~ ssList(X2) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(flattening,[],[f196]) ).
fof(f200,plain,
! [X0] :
( ! [X1] :
( ( nil = app(X0,X1)
<=> ( nil = X1
& nil = X0 ) )
| ~ ssList(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f83]) ).
fof(f201,plain,
! [X0] :
( app(X0,nil) = X0
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f84]) ).
fof(f211,plain,
! [X0] :
( ~ lt(X0,X0)
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f90]) ).
fof(f221,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ssList(X3)
& X1 = X3
& X0 = X2
& ? [X4] :
( ? [X5] :
( ? [X6] :
( ssList(X6)
& app(app(X5,cons(X4,nil)),X6) = X0
& ( memberP(X5,X4)
| memberP(X6,X4) ) )
& ssList(X5) )
& ssItem(X4) )
& ( ? [X7] :
( ssItem(X7)
& cons(X7,nil) = X2
& memberP(X3,X7)
& ! [X8] :
( ~ ssItem(X8)
| X7 = X8
| ~ memberP(X3,X8)
| ~ leq(X8,X7) ) )
| ( nil = X3
& nil = X2 ) ) )
& ssList(X2) )
& ssList(X1) )
& ssList(X0) ),
inference(ennf_transformation,[],[f97]) ).
fof(f227,plain,
! [X2,X3,X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| app(X2,cons(X1,X3)) != X0
| ~ ssList(X3)
| ~ ssList(X2)
| memberP(X0,X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f228,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| app(sK2(X0,X1),cons(X1,sK3(X0,X1))) = X0
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f229,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| ssList(sK3(X0,X1))
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f230,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| ssList(sK2(X0,X1))
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f236,plain,
! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| app(X1,X2) != X0
| ~ ssList(X2)
| frontsegP(X0,X1) ),
inference(cnf_transformation,[],[f101]) ).
fof(f262,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssItem(X2)
| ~ ssList(X3)
| ~ ssList(X4)
| ~ ssList(X5)
| app(app(X3,cons(X1,X4)),cons(X2,X5)) != X0
| lt(X2,X1)
| lt(X1,X2)
| ~ strictorderP(X0) ),
inference(cnf_transformation,[],[f109]) ).
fof(f304,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| ssList(cons(X1,X0)) ),
inference(cnf_transformation,[],[f119]) ).
fof(f305,plain,
ssList(nil),
inference(cnf_transformation,[],[f17]) ).
fof(f309,plain,
! [X0] :
( ~ ssList(X0)
| cons(sK44(X0),sK43(X0)) = X0
| nil = X0 ),
inference(cnf_transformation,[],[f124]) ).
fof(f310,plain,
! [X0] :
( ~ ssList(X0)
| ssItem(sK44(X0))
| nil = X0 ),
inference(cnf_transformation,[],[f124]) ).
fof(f311,plain,
! [X0] :
( ~ ssList(X0)
| ssList(sK43(X0))
| nil = X0 ),
inference(cnf_transformation,[],[f124]) ).
fof(f317,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ssList(app(X0,X1)) ),
inference(cnf_transformation,[],[f132]) ).
fof(f319,plain,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
inference(cnf_transformation,[],[f134]) ).
fof(f330,plain,
! [X2,X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ memberP(X2,X0)
| memberP(app(X1,X2),X0) ),
inference(cnf_transformation,[],[f146]) ).
fof(f332,plain,
! [X2,X0,X1] :
( ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| memberP(X2,X0)
| X0 = X1
| ~ memberP(cons(X1,X2),X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f335,plain,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[],[f148]) ).
fof(f338,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f152]) ).
fof(f340,plain,
! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X0,X1)
| frontsegP(app(X0,X2),X1) ),
inference(cnf_transformation,[],[f155]) ).
fof(f341,plain,
! [X2,X3,X0,X1] :
( ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X3)
| frontsegP(X2,X3)
| ~ frontsegP(cons(X0,X2),cons(X1,X3)) ),
inference(cnf_transformation,[],[f156]) ).
fof(f342,plain,
! [X2,X3,X0,X1] :
( ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X3)
| X0 = X1
| ~ frontsegP(cons(X0,X2),cons(X1,X3)) ),
inference(cnf_transformation,[],[f156]) ).
fof(f343,plain,
! [X2,X3,X0,X1] :
( ~ ssItem(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X3)
| ~ frontsegP(X2,X3)
| X0 != X1
| frontsegP(cons(X0,X2),cons(X1,X3)) ),
inference(cnf_transformation,[],[f156]) ).
fof(f344,plain,
! [X0] :
( ~ ssList(X0)
| frontsegP(X0,nil) ),
inference(cnf_transformation,[],[f157]) ).
fof(f346,plain,
! [X0] :
( ~ ssList(X0)
| nil = X0
| ~ frontsegP(nil,X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f365,plain,
! [X0] :
( strictorderP(cons(X0,nil))
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f179]) ).
fof(f390,plain,
! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| app(X1,X2) != app(X1,X0)
| X0 = X2 ),
inference(cnf_transformation,[],[f197]) ).
fof(f393,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| nil = X0
| nil != app(X0,X1) ),
inference(cnf_transformation,[],[f200]) ).
fof(f396,plain,
! [X0] :
( ~ ssList(X0)
| app(X0,nil) = X0 ),
inference(cnf_transformation,[],[f201]) ).
fof(f402,plain,
! [X0] :
( ~ lt(X0,X0)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f211]) ).
fof(f410,plain,
( memberP(sK54,sK51)
| memberP(sK53,sK51) ),
inference(cnf_transformation,[],[f221]) ).
fof(f411,plain,
sK47 = app(app(sK53,cons(sK51,nil)),sK54),
inference(cnf_transformation,[],[f221]) ).
fof(f412,plain,
ssList(sK54),
inference(cnf_transformation,[],[f221]) ).
fof(f415,plain,
ssList(sK53),
inference(cnf_transformation,[],[f221]) ).
fof(f420,plain,
( nil = sK49
| sK49 = cons(sK52,nil) ),
inference(cnf_transformation,[],[f221]) ).
fof(f421,plain,
( nil = sK49
| ssItem(sK52) ),
inference(cnf_transformation,[],[f221]) ).
fof(f422,plain,
ssItem(sK51),
inference(cnf_transformation,[],[f221]) ).
fof(f423,plain,
sK47 = sK49,
inference(cnf_transformation,[],[f221]) ).
fof(f428,plain,
ssList(sK47),
inference(cnf_transformation,[],[f221]) ).
fof(f429,plain,
ssList(sK49),
inference(definition_unfolding,[],[f428,f423]) ).
fof(f431,plain,
sK49 = app(app(sK53,cons(sK51,nil)),sK54),
inference(definition_unfolding,[],[f411,f423]) ).
fof(f433,plain,
! [X2,X3,X1] :
( ~ ssList(app(X2,cons(X1,X3)))
| ~ ssItem(X1)
| ~ ssList(X3)
| ~ ssList(X2)
| memberP(app(X2,cons(X1,X3)),X1) ),
inference(equality_resolution,[],[f227]) ).
fof(f435,plain,
! [X2,X1] :
( ~ ssList(app(X1,X2))
| ~ ssList(X1)
| ~ ssList(X2)
| frontsegP(app(X1,X2),X1) ),
inference(equality_resolution,[],[f236]) ).
fof(f440,plain,
! [X2,X3,X1,X4,X5] :
( ~ ssList(app(app(X3,cons(X1,X4)),cons(X2,X5)))
| ~ ssItem(X1)
| ~ ssItem(X2)
| ~ ssList(X3)
| ~ ssList(X4)
| ~ ssList(X5)
| lt(X2,X1)
| lt(X1,X2)
| ~ strictorderP(app(app(X3,cons(X1,X4)),cons(X2,X5))) ),
inference(equality_resolution,[],[f262]) ).
fof(f448,plain,
! [X2,X3,X1] :
( ~ ssItem(X1)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X3)
| ~ frontsegP(X2,X3)
| frontsegP(cons(X1,X2),cons(X1,X3)) ),
inference(equality_resolution,[],[f343]) ).
fof(f457,plain,
! [X0,X1] :
( ~ ssList(sK2(X0,X1))
| ~ ssItem(X1)
| ssList(X0)
| memberP(X0,X1) ),
inference(consistent_polarity_flipping,[],[f230]) ).
fof(f458,plain,
! [X0,X1] :
( ~ ssList(sK3(X0,X1))
| ~ ssItem(X1)
| ssList(X0)
| memberP(X0,X1) ),
inference(consistent_polarity_flipping,[],[f229]) ).
fof(f459,plain,
! [X0,X1] :
( memberP(X0,X1)
| ~ ssItem(X1)
| app(sK2(X0,X1),cons(X1,sK3(X0,X1))) = X0
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f228]) ).
fof(f460,plain,
! [X2,X3,X1] :
( ~ memberP(app(X2,cons(X1,X3)),X1)
| ~ ssItem(X1)
| ssList(X3)
| ssList(X2)
| ssList(app(X2,cons(X1,X3))) ),
inference(consistent_polarity_flipping,[],[f433]) ).
fof(f464,plain,
! [X2,X1] :
( ssList(app(X1,X2))
| ssList(X1)
| ssList(X2)
| frontsegP(app(X1,X2),X1) ),
inference(consistent_polarity_flipping,[],[f435]) ).
fof(f500,plain,
! [X2,X3,X1,X4,X5] :
( ~ strictorderP(app(app(X3,cons(X1,X4)),cons(X2,X5)))
| ~ ssItem(X1)
| ~ ssItem(X2)
| ssList(X3)
| ssList(X4)
| ssList(X5)
| lt(X2,X1)
| lt(X1,X2)
| ssList(app(app(X3,cons(X1,X4)),cons(X2,X5))) ),
inference(consistent_polarity_flipping,[],[f440]) ).
fof(f534,plain,
! [X0,X1] :
( ~ ssList(cons(X1,X0))
| ~ ssItem(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f304]) ).
fof(f535,plain,
~ ssList(nil),
inference(consistent_polarity_flipping,[],[f305]) ).
fof(f539,plain,
! [X0] :
( ~ ssList(sK43(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f311]) ).
fof(f540,plain,
! [X0] :
( ssItem(sK44(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f310]) ).
fof(f541,plain,
! [X0] :
( ssList(X0)
| cons(sK44(X0),sK43(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f309]) ).
fof(f547,plain,
! [X0,X1] :
( ~ ssList(app(X0,X1))
| ssList(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f317]) ).
fof(f549,plain,
! [X0] :
( ssList(X0)
| app(nil,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f319]) ).
fof(f553,plain,
! [X2,X0,X1] :
( ~ memberP(app(X1,X2),X0)
| ssList(X1)
| ssList(X2)
| memberP(X2,X0)
| ~ ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f330]) ).
fof(f557,plain,
! [X2,X0,X1] :
( ~ memberP(X2,X0)
| ~ ssItem(X1)
| ssList(X2)
| ~ ssItem(X0)
| X0 = X1
| memberP(cons(X1,X2),X0) ),
inference(consistent_polarity_flipping,[],[f332]) ).
fof(f558,plain,
! [X0] :
( memberP(nil,X0)
| ~ ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f335]) ).
fof(f560,plain,
! [X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X1)
| ~ frontsegP(X1,X0)
| ssList(X0)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f338]) ).
fof(f562,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X1)
| ssList(X2)
| ssList(X0)
| frontsegP(app(X0,X2),X1) ),
inference(consistent_polarity_flipping,[],[f340]) ).
fof(f563,plain,
! [X2,X3,X1] :
( ~ ssItem(X1)
| ~ ssItem(X1)
| ssList(X2)
| ssList(X3)
| ~ frontsegP(X2,X3)
| frontsegP(cons(X1,X2),cons(X1,X3)) ),
inference(consistent_polarity_flipping,[],[f448]) ).
fof(f564,plain,
! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X2),cons(X1,X3))
| ~ ssItem(X1)
| ssList(X2)
| ssList(X3)
| X0 = X1
| ~ ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f342]) ).
fof(f565,plain,
! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X2),cons(X1,X3))
| ~ ssItem(X1)
| ssList(X2)
| ssList(X3)
| frontsegP(X2,X3)
| ~ ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f341]) ).
fof(f566,plain,
! [X0] :
( frontsegP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f344]) ).
fof(f567,plain,
! [X0] :
( ~ frontsegP(nil,X0)
| nil = X0
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f346]) ).
fof(f602,plain,
! [X2,X0,X1] :
( app(X1,X2) != app(X1,X0)
| ssList(X1)
| ssList(X2)
| ssList(X0)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f390]) ).
fof(f607,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ssList(X1)
| nil = X0
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f393]) ).
fof(f608,plain,
! [X0] :
( ssList(X0)
| app(X0,nil) = X0 ),
inference(consistent_polarity_flipping,[],[f396]) ).
fof(f614,plain,
~ ssList(sK49),
inference(consistent_polarity_flipping,[],[f429]) ).
fof(f620,plain,
~ ssList(sK53),
inference(consistent_polarity_flipping,[],[f415]) ).
fof(f623,plain,
~ ssList(sK54),
inference(consistent_polarity_flipping,[],[f412]) ).
fof(f624,plain,
( ~ memberP(sK54,sK51)
| ~ memberP(sK53,sK51) ),
inference(consistent_polarity_flipping,[],[f410]) ).
fof(f627,plain,
! [X2,X3,X1] :
( ~ frontsegP(X2,X3)
| ssList(X2)
| ssList(X3)
| ~ ssItem(X1)
| frontsegP(cons(X1,X2),cons(X1,X3)) ),
inference(duplicate_literal_removal,[],[f563]) ).
fof(f633,definition,
( spl55_1
<=> memberP(sK53,sK51) ),
introduced(definition,[new_symbols(definition,[spl55_1])],[avatar_definition]) ).
fof(f634,plain,
( memberP(sK53,sK51)
| ~ spl55_1 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f635,plain,
( ~ memberP(sK53,sK51)
| spl55_1 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f637,definition,
( spl55_2
<=> memberP(sK54,sK51) ),
introduced(definition,[new_symbols(definition,[spl55_2])],[avatar_definition]) ).
fof(f639,plain,
( ~ memberP(sK54,sK51)
| spl55_2 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f640,plain,
( ~ spl55_1
| ~ spl55_2 ),
inference(avatar_split_clause,[],[f624,f637,f633]) ).
fof(f645,definition,
( spl55_4
<=> nil = sK49 ),
introduced(definition,[new_symbols(definition,[spl55_4])],[avatar_definition]) ).
fof(f647,plain,
( nil = sK49
| ~ spl55_4 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f660,definition,
( spl55_7
<=> sK49 = cons(sK52,nil) ),
introduced(definition,[new_symbols(definition,[spl55_7])],[avatar_definition]) ).
fof(f662,plain,
( sK49 = cons(sK52,nil)
| ~ spl55_7 ),
inference(avatar_component_clause,[],[f660]) ).
fof(f665,definition,
( spl55_8
<=> ssItem(sK52) ),
introduced(definition,[new_symbols(definition,[spl55_8])],[avatar_definition]) ).
fof(f667,plain,
( ssItem(sK52)
| ~ spl55_8 ),
inference(avatar_component_clause,[],[f665]) ).
fof(f670,plain,
( spl55_7
| spl55_4 ),
inference(avatar_split_clause,[],[f420,f645,f660]) ).
fof(f671,plain,
( spl55_8
| spl55_4 ),
inference(avatar_split_clause,[],[f421,f645,f665]) ).
fof(f677,definition,
( spl55_10
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl55_10])],[avatar_definition]) ).
fof(f678,plain,
( ~ ssList(nil)
| spl55_10 ),
inference(avatar_component_clause,[],[f677]) ).
fof(f706,plain,
~ spl55_10,
inference(avatar_split_clause,[],[f535,f677]) ).
fof(f711,plain,
( nil = app(app(sK53,cons(sK51,nil)),sK54)
| ~ spl55_4 ),
inference(forward_demodulation,[],[f431,f647]) ).
fof(f733,plain,
sK49 = app(nil,sK49),
inference(resolution,[],[f549,f614]) ).
fof(f760,plain,
sK49 = app(sK49,nil),
inference(resolution,[],[f608,f614]) ).
fof(f925,definition,
( spl55_17
<=> nil = sK54 ),
introduced(definition,[new_symbols(definition,[spl55_17])],[avatar_definition]) ).
fof(f926,plain,
( nil != sK54
| spl55_17 ),
inference(avatar_component_clause,[],[f925]) ).
fof(f927,plain,
( nil = sK54
| ~ spl55_17 ),
inference(avatar_component_clause,[],[f925]) ).
fof(f934,definition,
( spl55_19
<=> nil = sK53 ),
introduced(definition,[new_symbols(definition,[spl55_19])],[avatar_definition]) ).
fof(f935,plain,
( nil != sK53
| spl55_19 ),
inference(avatar_component_clause,[],[f934]) ).
fof(f936,plain,
( nil = sK53
| ~ spl55_19 ),
inference(avatar_component_clause,[],[f934]) ).
fof(f982,plain,
( ~ memberP(nil,sK51)
| spl55_2
| ~ spl55_17 ),
inference(superposition,[],[f639,f927]) ).
fof(f1064,plain,
( sK53 = cons(sK44(sK53),sK43(sK53))
| nil = sK53 ),
inference(resolution,[],[f541,f620]) ).
fof(f1104,plain,
( nil != nil
| ssList(sK54)
| nil = app(sK53,cons(sK51,nil))
| ssList(app(sK53,cons(sK51,nil)))
| ~ spl55_4 ),
inference(superposition,[],[f607,f711]) ).
fof(f1121,definition,
( spl55_24
<=> sK53 = cons(sK44(sK53),sK43(sK53)) ),
introduced(definition,[new_symbols(definition,[spl55_24])],[avatar_definition]) ).
fof(f1123,plain,
( sK53 = cons(sK44(sK53),sK43(sK53))
| ~ spl55_24 ),
inference(avatar_component_clause,[],[f1121]) ).
fof(f1124,plain,
( spl55_19
| spl55_24 ),
inference(avatar_split_clause,[],[f1064,f1121,f934]) ).
fof(f1131,definition,
( spl55_26
<=> ssList(app(sK53,cons(sK51,nil))) ),
introduced(definition,[new_symbols(definition,[spl55_26])],[avatar_definition]) ).
fof(f1132,plain,
( ~ ssList(app(sK53,cons(sK51,nil)))
| spl55_26 ),
inference(avatar_component_clause,[],[f1131]) ).
fof(f1133,plain,
( ssList(app(sK53,cons(sK51,nil)))
| ~ spl55_26 ),
inference(avatar_component_clause,[],[f1131]) ).
fof(f1135,definition,
( spl55_27
<=> nil = app(sK53,cons(sK51,nil)) ),
introduced(definition,[new_symbols(definition,[spl55_27])],[avatar_definition]) ).
fof(f1137,plain,
( nil = app(sK53,cons(sK51,nil))
| ~ spl55_27 ),
inference(avatar_component_clause,[],[f1135]) ).
fof(f1221,plain,
( ~ ssItem(sK51)
| spl55_2
| ~ spl55_17 ),
inference(resolution,[],[f982,f558]) ).
fof(f1222,plain,
( $false
| spl55_2
| ~ spl55_17 ),
inference(forward_subsumption_resolution,[],[f1221,f422]) ).
fof(f1223,plain,
( spl55_2
| ~ spl55_17 ),
inference(avatar_contradiction_clause,[],[f1222]) ).
fof(f1224,plain,
( ~ memberP(nil,sK51)
| spl55_1
| ~ spl55_19 ),
inference(forward_demodulation,[],[f635,f936]) ).
fof(f1226,plain,
( ~ ssItem(sK51)
| spl55_1
| ~ spl55_19 ),
inference(resolution,[],[f1224,f558]) ).
fof(f1227,plain,
( $false
| spl55_1
| ~ spl55_19 ),
inference(forward_subsumption_resolution,[],[f1226,f422]) ).
fof(f1228,plain,
( spl55_1
| ~ spl55_19 ),
inference(avatar_contradiction_clause,[],[f1227]) ).
fof(f1254,plain,
! [X2,X1] :
( frontsegP(app(X1,X2),X1)
| ssList(X2)
| ssList(X1) ),
inference(forward_subsumption_resolution,[],[f464,f547]) ).
fof(f1398,plain,
! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X0,X2))
| frontsegP(app(app(X0,X2),X1),X0)
| ssList(X2)
| ssList(X0) ),
inference(resolution,[],[f562,f1254]) ).
fof(f1399,plain,
! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X0,X2))
| frontsegP(app(app(X0,X2),X1),X0)
| ssList(X2) ),
inference(duplicate_literal_removal,[],[f1398]) ).
fof(f1403,plain,
! [X2,X0,X1] :
( frontsegP(app(app(X0,X2),X1),X0)
| ssList(X1)
| ssList(X0)
| ssList(X2) ),
inference(forward_subsumption_resolution,[],[f1399,f547]) ).
fof(f1498,plain,
( ssList(cons(sK51,nil))
| ssList(sK53)
| ~ spl55_26 ),
inference(resolution,[],[f1133,f547]) ).
fof(f1499,plain,
( ssList(cons(sK51,nil))
| ~ spl55_26 ),
inference(forward_subsumption_resolution,[],[f1498,f620]) ).
fof(f1500,plain,
( ~ ssItem(sK51)
| ssList(nil)
| ~ spl55_26 ),
inference(resolution,[],[f1499,f534]) ).
fof(f1501,plain,
( ssList(nil)
| ~ spl55_26 ),
inference(forward_subsumption_resolution,[],[f1500,f422]) ).
fof(f1502,plain,
( $false
| spl55_10
| ~ spl55_26 ),
inference(forward_subsumption_resolution,[],[f1501,f678]) ).
fof(f1503,plain,
( spl55_10
| ~ spl55_26 ),
inference(avatar_contradiction_clause,[],[f1502]) ).
fof(f1532,plain,
( ssList(sK54)
| nil = app(sK53,cons(sK51,nil))
| ssList(app(sK53,cons(sK51,nil)))
| ~ spl55_4 ),
inference(trivial_inequality_removal,[],[f1104]) ).
fof(f1538,plain,
( nil = app(sK53,cons(sK51,nil))
| ssList(app(sK53,cons(sK51,nil)))
| ~ spl55_4 ),
inference(forward_subsumption_resolution,[],[f1532,f623]) ).
fof(f1556,plain,
( spl55_26
| spl55_27
| ~ spl55_4 ),
inference(avatar_split_clause,[],[f1538,f645,f1135,f1131]) ).
fof(f1703,plain,
( strictorderP(sK49)
| ~ ssItem(sK52)
| ~ spl55_7 ),
inference(superposition,[],[f365,f662]) ).
fof(f1722,plain,
( strictorderP(sK49)
| ~ spl55_7
| ~ spl55_8 ),
inference(forward_subsumption_resolution,[],[f1703,f667]) ).
fof(f1877,plain,
! [X0,X1] :
( ssList(X0)
| ssList(nil)
| ~ ssItem(X1)
| frontsegP(cons(X1,X0),cons(X1,nil))
| ssList(X0) ),
inference(resolution,[],[f627,f566]) ).
fof(f1880,plain,
! [X0,X1] :
( ssList(X0)
| ssList(nil)
| ~ ssItem(X1)
| frontsegP(cons(X1,X0),cons(X1,nil)) ),
inference(duplicate_literal_removal,[],[f1877]) ).
fof(f1884,plain,
( ! [X0,X1] :
( frontsegP(cons(X1,X0),cons(X1,nil))
| ~ ssItem(X1)
| ssList(X0) )
| spl55_10 ),
inference(forward_subsumption_resolution,[],[f1880,f678]) ).
fof(f1918,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ssList(nil)
| ~ ssItem(X1)
| X0 = X1
| memberP(cons(X0,nil),X1)
| ~ ssItem(X1) ),
inference(resolution,[],[f557,f558]) ).
fof(f1921,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ssList(nil)
| ~ ssItem(X1)
| X0 = X1
| memberP(cons(X0,nil),X1) ),
inference(duplicate_literal_removal,[],[f1918]) ).
fof(f1924,plain,
( ! [X0,X1] :
( memberP(cons(X0,nil),X1)
| ~ ssItem(X1)
| X0 = X1
| ~ ssItem(X0) )
| spl55_10 ),
inference(forward_subsumption_resolution,[],[f1921,f678]) ).
fof(f2040,plain,
( ~ ssItem(sK51)
| sK53 = app(sK2(sK53,sK51),cons(sK51,sK3(sK53,sK51)))
| ssList(sK53)
| spl55_1 ),
inference(resolution,[],[f459,f635]) ).
fof(f2047,plain,
( sK53 = app(sK2(sK53,sK51),cons(sK51,sK3(sK53,sK51)))
| ssList(sK53)
| spl55_1 ),
inference(forward_subsumption_resolution,[],[f2040,f422]) ).
fof(f2053,plain,
( sK53 = app(sK2(sK53,sK51),cons(sK51,sK3(sK53,sK51)))
| spl55_1 ),
inference(forward_subsumption_resolution,[],[f2047,f620]) ).
fof(f2198,plain,
( ! [X0,X1] :
( ~ frontsegP(sK49,cons(X0,X1))
| ~ ssItem(X0)
| ssList(nil)
| ssList(X1)
| sK52 = X0
| ~ ssItem(sK52) )
| ~ spl55_7 ),
inference(superposition,[],[f564,f662]) ).
fof(f2202,plain,
( ! [X0,X1] :
( ~ frontsegP(sK49,cons(X0,X1))
| ~ ssItem(X0)
| ssList(X1)
| sK52 = X0
| ~ ssItem(sK52) )
| ~ spl55_7
| spl55_10 ),
inference(forward_subsumption_resolution,[],[f2198,f678]) ).
fof(f2204,plain,
( ! [X0,X1] :
( ~ frontsegP(sK49,cons(X0,X1))
| ~ ssItem(X0)
| ssList(X1)
| sK52 = X0 )
| ~ spl55_7
| ~ spl55_8
| spl55_10 ),
inference(forward_subsumption_resolution,[],[f2202,f667]) ).
fof(f2206,plain,
( ! [X0,X1] :
( ~ frontsegP(sK49,cons(X0,X1))
| ~ ssItem(X0)
| ssList(nil)
| ssList(X1)
| frontsegP(nil,X1)
| ~ ssItem(sK52) )
| ~ spl55_7 ),
inference(superposition,[],[f565,f662]) ).
fof(f2209,plain,
( ! [X0,X1] :
( ~ frontsegP(sK49,cons(X0,X1))
| ~ ssItem(X0)
| ssList(X1)
| frontsegP(nil,X1)
| ~ ssItem(sK52) )
| ~ spl55_7
| spl55_10 ),
inference(forward_subsumption_resolution,[],[f2206,f678]) ).
fof(f2210,plain,
( ! [X0,X1] :
( ~ frontsegP(sK49,cons(X0,X1))
| ~ ssItem(X0)
| ssList(X1)
| frontsegP(nil,X1) )
| ~ spl55_7
| ~ spl55_8
| spl55_10 ),
inference(forward_subsumption_resolution,[],[f2209,f667]) ).
fof(f2279,definition,
( spl55_56
<=> ssList(cons(sK51,nil)) ),
introduced(definition,[new_symbols(definition,[spl55_56])],[avatar_definition]) ).
fof(f2280,plain,
( ~ ssList(cons(sK51,nil))
| spl55_56 ),
inference(avatar_component_clause,[],[f2279]) ).
fof(f2281,plain,
( ssList(cons(sK51,nil))
| ~ spl55_56 ),
inference(avatar_component_clause,[],[f2279]) ).
fof(f2288,plain,
( ~ ssItem(sK51)
| ssList(nil)
| ~ spl55_56 ),
inference(resolution,[],[f2281,f534]) ).
fof(f2289,plain,
( ssList(nil)
| ~ spl55_56 ),
inference(forward_subsumption_resolution,[],[f2288,f422]) ).
fof(f2290,plain,
( $false
| spl55_10
| ~ spl55_56 ),
inference(forward_subsumption_resolution,[],[f2289,f678]) ).
fof(f2291,plain,
( spl55_10
| ~ spl55_56 ),
inference(avatar_contradiction_clause,[],[f2290]) ).
fof(f2511,plain,
( ! [X2,X0,X1] :
( ~ strictorderP(app(app(X0,cons(X1,X2)),sK49))
| ~ ssItem(X1)
| ~ ssItem(sK52)
| ssList(X0)
| ssList(X2)
| ssList(nil)
| lt(sK52,X1)
| lt(X1,sK52)
| ssList(app(app(X0,cons(X1,X2)),sK49)) )
| ~ spl55_7 ),
inference(superposition,[],[f500,f662]) ).
fof(f2513,plain,
( ! [X2,X0,X1] :
( ~ strictorderP(app(app(X0,cons(X1,X2)),sK49))
| ~ ssItem(X1)
| ssList(X0)
| ssList(X2)
| ssList(nil)
| lt(sK52,X1)
| lt(X1,sK52)
| ssList(app(app(X0,cons(X1,X2)),sK49)) )
| ~ spl55_7
| ~ spl55_8 ),
inference(forward_subsumption_resolution,[],[f2511,f667]) ).
fof(f2515,plain,
( ! [X2,X0,X1] :
( ~ strictorderP(app(app(X0,cons(X1,X2)),sK49))
| ~ ssItem(X1)
| ssList(X0)
| ssList(X2)
| lt(sK52,X1)
| lt(X1,sK52)
| ssList(app(app(X0,cons(X1,X2)),sK49)) )
| ~ spl55_7
| ~ spl55_8
| spl55_10 ),
inference(forward_subsumption_resolution,[],[f2513,f678]) ).
fof(f2647,definition,
( spl55_73
<=> ssList(sK43(sK53)) ),
introduced(definition,[new_symbols(definition,[spl55_73])],[avatar_definition]) ).
fof(f2648,plain,
( ~ ssList(sK43(sK53))
| spl55_73 ),
inference(avatar_component_clause,[],[f2647]) ).
fof(f2649,plain,
( ssList(sK43(sK53))
| ~ spl55_73 ),
inference(avatar_component_clause,[],[f2647]) ).
fof(f2651,definition,
( spl55_74
<=> ssItem(sK44(sK53)) ),
introduced(definition,[new_symbols(definition,[spl55_74])],[avatar_definition]) ).
fof(f2652,plain,
( ssItem(sK44(sK53))
| ~ spl55_74 ),
inference(avatar_component_clause,[],[f2651]) ).
fof(f2653,plain,
( ~ ssItem(sK44(sK53))
| spl55_74 ),
inference(avatar_component_clause,[],[f2651]) ).
fof(f2668,definition,
( spl55_78
<=> nil = sK43(sK53) ),
introduced(definition,[new_symbols(definition,[spl55_78])],[avatar_definition]) ).
fof(f2670,plain,
( nil = sK43(sK53)
| ~ spl55_78 ),
inference(avatar_component_clause,[],[f2668]) ).
fof(f2932,plain,
( ~ memberP(nil,sK51)
| ~ ssItem(sK51)
| ssList(nil)
| ssList(sK53)
| ssList(nil)
| ~ spl55_27 ),
inference(superposition,[],[f460,f1137]) ).
fof(f2953,plain,
( ~ memberP(nil,sK51)
| ~ ssItem(sK51)
| ssList(nil)
| ssList(sK53)
| ~ spl55_27 ),
inference(duplicate_literal_removal,[],[f2932]) ).
fof(f2971,plain,
( ~ ssItem(sK51)
| ssList(nil)
| ssList(sK53)
| ~ spl55_27 ),
inference(forward_subsumption_resolution,[],[f2953,f558]) ).
fof(f2990,plain,
( ssList(nil)
| ssList(sK53)
| ~ spl55_27 ),
inference(forward_subsumption_resolution,[],[f2971,f422]) ).
fof(f3004,plain,
( ssList(sK53)
| spl55_10
| ~ spl55_27 ),
inference(forward_subsumption_resolution,[],[f2990,f678]) ).
fof(f3005,plain,
( $false
| spl55_10
| ~ spl55_27 ),
inference(forward_subsumption_resolution,[],[f3004,f620]) ).
fof(f3006,plain,
( spl55_10
| ~ spl55_27 ),
inference(avatar_contradiction_clause,[],[f3005]) ).
fof(f3007,plain,
( ssList(sK53)
| nil = sK53
| spl55_74 ),
inference(resolution,[],[f2653,f540]) ).
fof(f3008,plain,
( nil = sK53
| spl55_74 ),
inference(forward_subsumption_resolution,[],[f3007,f620]) ).
fof(f3009,plain,
( $false
| spl55_19
| spl55_74 ),
inference(forward_subsumption_resolution,[],[f3008,f935]) ).
fof(f3010,plain,
( spl55_19
| spl55_74 ),
inference(avatar_contradiction_clause,[],[f3009]) ).
fof(f3011,plain,
( ssList(sK53)
| nil = sK53
| ~ spl55_73 ),
inference(resolution,[],[f2649,f539]) ).
fof(f3012,plain,
( nil = sK53
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f3011,f620]) ).
fof(f3013,plain,
( $false
| spl55_19
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f3012,f935]) ).
fof(f3014,plain,
( spl55_19
| ~ spl55_73 ),
inference(avatar_contradiction_clause,[],[f3013]) ).
fof(f4136,definition,
( spl55_271
<=> sK51 = sK52 ),
introduced(definition,[new_symbols(definition,[spl55_271])],[avatar_definition]) ).
fof(f4137,plain,
( sK51 != sK52
| spl55_271 ),
inference(avatar_component_clause,[],[f4136]) ).
fof(f4138,plain,
( sK51 = sK52
| ~ spl55_271 ),
inference(avatar_component_clause,[],[f4136]) ).
fof(f4140,definition,
( spl55_272
<=> memberP(sK49,sK51) ),
introduced(definition,[new_symbols(definition,[spl55_272])],[avatar_definition]) ).
fof(f4141,plain,
( ~ memberP(sK49,sK51)
| spl55_272 ),
inference(avatar_component_clause,[],[f4140]) ).
fof(f4329,definition,
( spl55_293
<=> sK52 = sK44(sK53) ),
introduced(definition,[new_symbols(definition,[spl55_293])],[avatar_definition]) ).
fof(f4331,plain,
( sK52 = sK44(sK53)
| ~ spl55_293 ),
inference(avatar_component_clause,[],[f4329]) ).
fof(f5170,definition,
( spl55_376
<=> sK49 = sK53 ),
introduced(definition,[new_symbols(definition,[spl55_376])],[avatar_definition]) ).
fof(f5171,plain,
( sK49 = sK53
| ~ spl55_376 ),
inference(avatar_component_clause,[],[f5170]) ).
fof(f5337,definition,
( spl55_394
<=> frontsegP(sK53,sK49) ),
introduced(definition,[new_symbols(definition,[spl55_394])],[avatar_definition]) ).
fof(f5344,plain,
( ~ frontsegP(sK49,sK53)
| ~ ssItem(sK44(sK53))
| ssList(sK43(sK53))
| sK52 = sK44(sK53)
| ~ spl55_7
| ~ spl55_8
| spl55_10
| ~ spl55_24 ),
inference(superposition,[],[f2204,f1123]) ).
fof(f5359,plain,
( ~ frontsegP(sK49,sK53)
| ssList(sK43(sK53))
| sK52 = sK44(sK53)
| ~ spl55_7
| ~ spl55_8
| spl55_10
| ~ spl55_24
| ~ spl55_74 ),
inference(forward_subsumption_resolution,[],[f5344,f2652]) ).
fof(f5364,plain,
( ~ frontsegP(sK49,sK53)
| sK52 = sK44(sK53)
| ~ spl55_7
| ~ spl55_8
| spl55_10
| ~ spl55_24
| spl55_73
| ~ spl55_74 ),
inference(forward_subsumption_resolution,[],[f5359,f2648]) ).
fof(f5367,definition,
( spl55_396
<=> frontsegP(sK49,sK53) ),
introduced(definition,[new_symbols(definition,[spl55_396])],[avatar_definition]) ).
fof(f5368,plain,
( frontsegP(sK49,sK53)
| ~ spl55_396 ),
inference(avatar_component_clause,[],[f5367]) ).
fof(f5373,plain,
( spl55_293
| ~ spl55_396
| ~ spl55_7
| ~ spl55_8
| spl55_10
| ~ spl55_24
| spl55_73
| ~ spl55_74 ),
inference(avatar_split_clause,[],[f5364,f2651,f2647,f1121,f677,f665,f660,f5367,f4329]) ).
fof(f5375,plain,
( ~ frontsegP(sK49,sK53)
| ~ ssItem(sK44(sK53))
| ssList(sK43(sK53))
| frontsegP(nil,sK43(sK53))
| ~ spl55_7
| ~ spl55_8
| spl55_10
| ~ spl55_24 ),
inference(superposition,[],[f2210,f1123]) ).
fof(f5417,definition,
( spl55_402
<=> frontsegP(nil,sK43(sK53)) ),
introduced(definition,[new_symbols(definition,[spl55_402])],[avatar_definition]) ).
fof(f5419,plain,
( frontsegP(nil,sK43(sK53))
| ~ spl55_402 ),
inference(avatar_component_clause,[],[f5417]) ).
fof(f6434,plain,
( ~ ssList(app(sK53,cons(sK52,nil)))
| spl55_26
| ~ spl55_271 ),
inference(superposition,[],[f1132,f4138]) ).
fof(f6453,plain,
( ~ ssList(app(sK53,sK49))
| ~ spl55_7
| spl55_26
| ~ spl55_271 ),
inference(forward_demodulation,[],[f6434,f662]) ).
fof(f7296,definition,
( spl55_454
<=> ssList(app(sK53,sK49)) ),
introduced(definition,[new_symbols(definition,[spl55_454])],[avatar_definition]) ).
fof(f7297,plain,
( ~ ssList(app(sK53,sK49))
| spl55_454 ),
inference(avatar_component_clause,[],[f7296]) ).
fof(f7435,definition,
( spl55_474
<=> lt(sK52,sK52) ),
introduced(definition,[new_symbols(definition,[spl55_474])],[avatar_definition]) ).
fof(f7436,plain,
( ~ lt(sK52,sK52)
| spl55_474 ),
inference(avatar_component_clause,[],[f7435]) ).
fof(f7437,plain,
( lt(sK52,sK52)
| ~ spl55_474 ),
inference(avatar_component_clause,[],[f7435]) ).
fof(f7444,definition,
( spl55_476
<=> lt(sK51,sK52) ),
introduced(definition,[new_symbols(definition,[spl55_476])],[avatar_definition]) ).
fof(f7446,plain,
( lt(sK51,sK52)
| ~ spl55_476 ),
inference(avatar_component_clause,[],[f7444]) ).
fof(f7696,plain,
( ~ strictorderP(app(sK53,sK49))
| ~ ssItem(sK51)
| ssList(sK2(sK53,sK51))
| ssList(sK3(sK53,sK51))
| lt(sK52,sK51)
| lt(sK51,sK52)
| ssList(app(sK53,sK49))
| spl55_1
| ~ spl55_7
| ~ spl55_8
| spl55_10 ),
inference(superposition,[],[f2515,f2053]) ).
fof(f7702,plain,
( ~ strictorderP(app(sK53,sK49))
| ssList(sK2(sK53,sK51))
| ssList(sK3(sK53,sK51))
| lt(sK52,sK51)
| lt(sK51,sK52)
| ssList(app(sK53,sK49))
| spl55_1
| ~ spl55_7
| ~ spl55_8
| spl55_10 ),
inference(forward_subsumption_resolution,[],[f7696,f422]) ).
fof(f7716,definition,
( spl55_506
<=> lt(sK52,sK51) ),
introduced(definition,[new_symbols(definition,[spl55_506])],[avatar_definition]) ).
fof(f7718,plain,
( lt(sK52,sK51)
| ~ spl55_506 ),
inference(avatar_component_clause,[],[f7716]) ).
fof(f8778,plain,
( ~ spl55_454
| ~ spl55_7
| spl55_26
| ~ spl55_271 ),
inference(avatar_split_clause,[],[f6453,f4136,f1131,f660,f7296]) ).
fof(f10059,plain,
( ~ ssItem(sK52)
| ~ spl55_474 ),
inference(resolution,[],[f7437,f402]) ).
fof(f10072,plain,
( $false
| ~ spl55_8
| ~ spl55_474 ),
inference(forward_subsumption_resolution,[],[f10059,f667]) ).
fof(f10073,plain,
( ~ spl55_8
| ~ spl55_474 ),
inference(avatar_contradiction_clause,[],[f10072]) ).
fof(f10630,plain,
( frontsegP(sK53,cons(sK44(sK53),nil))
| ~ ssItem(sK44(sK53))
| ssList(sK43(sK53))
| spl55_10
| ~ spl55_24 ),
inference(superposition,[],[f1884,f1123]) ).
fof(f10645,plain,
( frontsegP(sK53,cons(sK44(sK53),nil))
| ssList(sK43(sK53))
| spl55_10
| ~ spl55_24
| ~ spl55_74 ),
inference(forward_subsumption_resolution,[],[f10630,f2652]) ).
fof(f10657,plain,
( frontsegP(sK53,cons(sK44(sK53),nil))
| spl55_10
| ~ spl55_24
| spl55_73
| ~ spl55_74 ),
inference(forward_subsumption_resolution,[],[f10645,f2648]) ).
fof(f11701,plain,
( ! [X0] :
( memberP(sK49,X0)
| ~ ssItem(X0)
| sK52 = X0
| ~ ssItem(sK52) )
| ~ spl55_7
| spl55_10 ),
inference(superposition,[],[f1924,f662]) ).
fof(f11707,plain,
( ! [X0] :
( memberP(sK49,X0)
| ~ ssItem(X0)
| sK52 = X0 )
| ~ spl55_7
| ~ spl55_8
| spl55_10 ),
inference(forward_subsumption_resolution,[],[f11701,f667]) ).
fof(f12914,plain,
( ssList(sK53)
| ~ frontsegP(sK53,sK49)
| ssList(sK49)
| sK49 = sK53
| ~ spl55_396 ),
inference(resolution,[],[f5368,f560]) ).
fof(f14343,definition,
( spl55_759
<=> frontsegP(app(sK53,sK49),sK49) ),
introduced(definition,[new_symbols(definition,[spl55_759])],[avatar_definition]) ).
fof(f14344,plain,
( frontsegP(app(sK53,sK49),sK49)
| ~ spl55_759 ),
inference(avatar_component_clause,[],[f14343]) ).
fof(f14345,plain,
( ~ frontsegP(app(sK53,sK49),sK49)
| spl55_759 ),
inference(avatar_component_clause,[],[f14343]) ).
fof(f23155,plain,
( lt(sK52,sK52)
| ~ spl55_271
| ~ spl55_506 ),
inference(forward_demodulation,[],[f7718,f4138]) ).
fof(f23156,plain,
( $false
| ~ spl55_271
| spl55_474
| ~ spl55_506 ),
inference(forward_subsumption_resolution,[],[f23155,f7436]) ).
fof(f23157,plain,
( ~ spl55_271
| spl55_474
| ~ spl55_506 ),
inference(avatar_contradiction_clause,[],[f23156]) ).
fof(f23887,plain,
( sK53 = cons(sK52,sK43(sK53))
| ~ spl55_24
| ~ spl55_293 ),
inference(superposition,[],[f1123,f4331]) ).
fof(f23897,plain,
( sK53 = cons(sK52,nil)
| ~ spl55_24
| ~ spl55_78
| ~ spl55_293 ),
inference(forward_demodulation,[],[f23887,f2670]) ).
fof(f23898,plain,
( sK49 = sK53
| ~ spl55_7
| ~ spl55_24
| ~ spl55_78
| ~ spl55_293 ),
inference(forward_demodulation,[],[f23897,f662]) ).
fof(f23904,plain,
( spl55_376
| ~ spl55_7
| ~ spl55_24
| ~ spl55_78
| ~ spl55_293 ),
inference(avatar_split_clause,[],[f23898,f4329,f2668,f1121,f660,f5170]) ).
fof(f24349,plain,
( ~ ssList(app(sK49,sK49))
| ~ spl55_376
| spl55_454 ),
inference(superposition,[],[f7297,f5171]) ).
fof(f34086,plain,
( ~ frontsegP(sK53,sK49)
| ssList(sK49)
| sK49 = sK53
| ~ spl55_396 ),
inference(forward_subsumption_resolution,[],[f12914,f620]) ).
fof(f34882,plain,
( ~ frontsegP(sK53,sK49)
| sK49 = sK53
| ~ spl55_396 ),
inference(forward_subsumption_resolution,[],[f34086,f614]) ).
fof(f35677,plain,
( ~ memberP(sK49,sK51)
| spl55_1
| ~ spl55_376 ),
inference(superposition,[],[f635,f5171]) ).
fof(f47577,plain,
( nil = sK43(sK53)
| ssList(sK43(sK53))
| ~ spl55_402 ),
inference(resolution,[],[f5419,f567]) ).
fof(f48056,plain,
( nil = sK43(sK53)
| spl55_73
| ~ spl55_402 ),
inference(forward_subsumption_resolution,[],[f47577,f2648]) ).
fof(f48094,plain,
( spl55_78
| spl55_73
| ~ spl55_402 ),
inference(avatar_split_clause,[],[f48056,f5417,f2647,f2668]) ).
fof(f58165,plain,
( ~ frontsegP(app(sK49,sK49),sK49)
| ~ spl55_376
| spl55_759 ),
inference(forward_demodulation,[],[f14345,f5171]) ).
fof(f58212,plain,
( ssList(sK49)
| ssList(sK49)
| ~ spl55_376
| spl55_759 ),
inference(resolution,[],[f58165,f1254]) ).
fof(f58213,plain,
( ssList(sK49)
| ~ spl55_376
| spl55_759 ),
inference(duplicate_literal_removal,[],[f58212]) ).
fof(f58214,plain,
( $false
| ~ spl55_376
| spl55_759 ),
inference(forward_subsumption_resolution,[],[f58213,f614]) ).
fof(f58215,plain,
( ~ spl55_376
| spl55_759 ),
inference(avatar_contradiction_clause,[],[f58214]) ).
fof(f58216,plain,
( frontsegP(app(sK49,sK49),sK49)
| ~ spl55_376
| ~ spl55_759 ),
inference(forward_demodulation,[],[f14344,f5171]) ).
fof(f58299,plain,
( lt(sK52,sK52)
| ~ spl55_271
| ~ spl55_476 ),
inference(forward_demodulation,[],[f7446,f4138]) ).
fof(f58302,plain,
( $false
| ~ spl55_271
| spl55_474
| ~ spl55_476 ),
inference(forward_subsumption_resolution,[],[f58299,f7436]) ).
fof(f58303,plain,
( ~ spl55_271
| spl55_474
| ~ spl55_476 ),
inference(avatar_contradiction_clause,[],[f58302]) ).
fof(f58740,plain,
( sK49 = app(app(sK53,cons(sK52,nil)),sK54)
| ~ spl55_271 ),
inference(forward_demodulation,[],[f431,f4138]) ).
fof(f59315,plain,
( sK49 = app(app(sK53,sK49),sK54)
| ~ spl55_7
| ~ spl55_271 ),
inference(forward_demodulation,[],[f58740,f662]) ).
fof(f59462,plain,
( sK49 = app(app(sK49,sK49),sK54)
| ~ spl55_7
| ~ spl55_271
| ~ spl55_376 ),
inference(forward_demodulation,[],[f59315,f5171]) ).
fof(f59932,plain,
( frontsegP(sK49,app(sK49,sK49))
| ssList(sK54)
| ssList(app(sK49,sK49))
| ~ spl55_7
| ~ spl55_271
| ~ spl55_376 ),
inference(superposition,[],[f1254,f59462]) ).
fof(f59972,plain,
( frontsegP(sK49,app(sK49,sK49))
| ssList(app(sK49,sK49))
| ~ spl55_7
| ~ spl55_271
| ~ spl55_376 ),
inference(forward_subsumption_resolution,[],[f59932,f623]) ).
fof(f59995,plain,
( frontsegP(sK49,app(sK49,sK49))
| ~ spl55_7
| ~ spl55_271
| ~ spl55_376
| spl55_454 ),
inference(forward_subsumption_resolution,[],[f59972,f24349]) ).
fof(f60013,definition,
( spl55_2808
<=> sK49 = app(sK49,sK49) ),
introduced(definition,[new_symbols(definition,[spl55_2808])],[avatar_definition]) ).
fof(f60015,plain,
( sK49 = app(sK49,sK49)
| ~ spl55_2808 ),
inference(avatar_component_clause,[],[f60013]) ).
fof(f60017,definition,
( spl55_2809
<=> frontsegP(app(sK49,sK49),sK49) ),
introduced(definition,[new_symbols(definition,[spl55_2809])],[avatar_definition]) ).
fof(f60043,plain,
( ssList(app(sK49,sK49))
| ~ frontsegP(app(sK49,sK49),sK49)
| ssList(sK49)
| sK49 = app(sK49,sK49)
| ~ spl55_7
| ~ spl55_271
| ~ spl55_376
| spl55_454 ),
inference(resolution,[],[f59995,f560]) ).
fof(f60047,plain,
( ~ frontsegP(app(sK49,sK49),sK49)
| ssList(sK49)
| sK49 = app(sK49,sK49)
| ~ spl55_7
| ~ spl55_271
| ~ spl55_376
| spl55_454 ),
inference(forward_subsumption_resolution,[],[f60043,f24349]) ).
fof(f60054,plain,
( ~ frontsegP(app(sK49,sK49),sK49)
| sK49 = app(sK49,sK49)
| ~ spl55_7
| ~ spl55_271
| ~ spl55_376
| spl55_454 ),
inference(forward_subsumption_resolution,[],[f60047,f614]) ).
fof(f60060,plain,
( spl55_2808
| ~ spl55_2809
| ~ spl55_7
| ~ spl55_271
| ~ spl55_376
| spl55_454 ),
inference(avatar_split_clause,[],[f60054,f7296,f5170,f4136,f660,f60017,f60013]) ).
fof(f66049,plain,
( spl55_2809
| ~ spl55_376
| ~ spl55_759 ),
inference(avatar_split_clause,[],[f58216,f14343,f5170,f60017]) ).
fof(f66886,plain,
( ! [X0] :
( sK49 != app(app(sK53,sK49),X0)
| ssList(app(sK53,sK49))
| ssList(X0)
| ssList(sK54)
| sK54 = X0 )
| ~ spl55_7
| ~ spl55_271 ),
inference(superposition,[],[f602,f59315]) ).
fof(f66926,plain,
( ! [X0] :
( sK49 != app(app(sK53,sK49),X0)
| ssList(X0)
| ssList(sK54)
| sK54 = X0 )
| ~ spl55_7
| ~ spl55_271
| spl55_454 ),
inference(forward_subsumption_resolution,[],[f66886,f7297]) ).
fof(f66949,plain,
( ! [X0] :
( sK49 != app(app(sK53,sK49),X0)
| ssList(X0)
| sK54 = X0 )
| ~ spl55_7
| ~ spl55_271
| spl55_454 ),
inference(forward_subsumption_resolution,[],[f66926,f623]) ).
fof(f67793,plain,
( ! [X0] :
( sK49 != app(app(nil,sK49),X0)
| ssList(X0)
| sK54 = X0 )
| ~ spl55_7
| ~ spl55_19
| ~ spl55_271
| spl55_454 ),
inference(forward_demodulation,[],[f66949,f936]) ).
fof(f67794,plain,
( ! [X0] :
( sK49 != app(sK49,X0)
| ssList(X0)
| sK54 = X0 )
| ~ spl55_7
| ~ spl55_19
| ~ spl55_271
| spl55_454 ),
inference(forward_demodulation,[],[f67793,f733]) ).
fof(f67795,plain,
( sK49 != sK49
| ssList(nil)
| nil = sK54
| ~ spl55_7
| ~ spl55_19
| ~ spl55_271
| spl55_454 ),
inference(superposition,[],[f67794,f760]) ).
fof(f67796,plain,
( ssList(nil)
| nil = sK54
| ~ spl55_7
| ~ spl55_19
| ~ spl55_271
| spl55_454 ),
inference(trivial_inequality_removal,[],[f67795]) ).
fof(f67797,plain,
( nil = sK54
| ~ spl55_7
| spl55_10
| ~ spl55_19
| ~ spl55_271
| spl55_454 ),
inference(forward_subsumption_resolution,[],[f67796,f678]) ).
fof(f67798,plain,
( $false
| ~ spl55_7
| spl55_10
| spl55_17
| ~ spl55_19
| ~ spl55_271
| spl55_454 ),
inference(forward_subsumption_resolution,[],[f67797,f926]) ).
fof(f67799,plain,
( ~ spl55_7
| spl55_10
| spl55_17
| ~ spl55_19
| ~ spl55_271
| spl55_454 ),
inference(avatar_contradiction_clause,[],[f67798]) ).
fof(f67968,plain,
( frontsegP(sK53,cons(sK52,nil))
| spl55_10
| ~ spl55_24
| spl55_73
| ~ spl55_74
| ~ spl55_293 ),
inference(forward_demodulation,[],[f10657,f4331]) ).
fof(f69067,plain,
( frontsegP(sK53,sK49)
| ~ spl55_7
| spl55_10
| ~ spl55_24
| spl55_73
| ~ spl55_74
| ~ spl55_293 ),
inference(forward_demodulation,[],[f67968,f662]) ).
fof(f69177,plain,
( spl55_394
| ~ spl55_7
| spl55_10
| ~ spl55_24
| spl55_73
| ~ spl55_74
| ~ spl55_293 ),
inference(avatar_split_clause,[],[f69067,f4329,f2651,f2647,f1121,f677,f660,f5337]) ).
fof(f69381,plain,
( frontsegP(sK49,sK53)
| ssList(sK54)
| ssList(sK53)
| ssList(cons(sK51,nil)) ),
inference(superposition,[],[f1403,f431]) ).
fof(f69392,plain,
! [X0] :
( ~ memberP(sK49,X0)
| ssList(app(sK53,cons(sK51,nil)))
| ssList(sK54)
| memberP(sK54,X0)
| ~ ssItem(X0) ),
inference(superposition,[],[f553,f431]) ).
fof(f69435,plain,
( ! [X0] :
( ~ memberP(sK49,X0)
| ssList(sK54)
| memberP(sK54,X0)
| ~ ssItem(X0) )
| spl55_26 ),
inference(forward_subsumption_resolution,[],[f69392,f1132]) ).
fof(f69443,plain,
( frontsegP(sK49,sK53)
| ssList(sK53)
| ssList(cons(sK51,nil)) ),
inference(forward_subsumption_resolution,[],[f69381,f623]) ).
fof(f69463,plain,
( ! [X0] :
( memberP(sK54,X0)
| ~ memberP(sK49,X0)
| ~ ssItem(X0) )
| spl55_26 ),
inference(forward_subsumption_resolution,[],[f69435,f623]) ).
fof(f69471,plain,
( frontsegP(sK49,sK53)
| ssList(cons(sK51,nil)) ),
inference(forward_subsumption_resolution,[],[f69443,f620]) ).
fof(f69481,plain,
( frontsegP(sK49,sK53)
| spl55_56 ),
inference(forward_subsumption_resolution,[],[f69471,f2280]) ).
fof(f69487,plain,
( spl55_396
| spl55_56 ),
inference(avatar_split_clause,[],[f69481,f2279,f5367]) ).
fof(f70176,plain,
( ~ memberP(sK49,sK51)
| ~ ssItem(sK51)
| spl55_2
| spl55_26 ),
inference(resolution,[],[f69463,f639]) ).
fof(f70189,plain,
( ~ memberP(sK49,sK51)
| spl55_2
| spl55_26 ),
inference(forward_subsumption_resolution,[],[f70176,f422]) ).
fof(f70193,plain,
( ~ spl55_272
| spl55_2
| spl55_26 ),
inference(avatar_split_clause,[],[f70189,f1131,f637,f4140]) ).
fof(f70659,plain,
( ~ frontsegP(sK49,sK53)
| ssList(sK43(sK53))
| frontsegP(nil,sK43(sK53))
| ~ spl55_7
| ~ spl55_8
| spl55_10
| ~ spl55_24
| ~ spl55_74 ),
inference(forward_subsumption_resolution,[],[f5375,f2652]) ).
fof(f72481,plain,
( spl55_376
| ~ spl55_394
| ~ spl55_396 ),
inference(avatar_split_clause,[],[f34882,f5367,f5337,f5170]) ).
fof(f72537,plain,
( ~ frontsegP(sK49,sK53)
| frontsegP(nil,sK43(sK53))
| ~ spl55_7
| ~ spl55_8
| spl55_10
| ~ spl55_24
| spl55_73
| ~ spl55_74 ),
inference(forward_subsumption_resolution,[],[f70659,f2648]) ).
fof(f72786,plain,
( spl55_402
| ~ spl55_396
| ~ spl55_7
| ~ spl55_8
| spl55_10
| ~ spl55_24
| spl55_73
| ~ spl55_74 ),
inference(avatar_split_clause,[],[f72537,f2651,f2647,f1121,f677,f665,f660,f5367,f5417]) ).
fof(f74229,plain,
( memberP(sK49,sK51)
| ~ spl55_1
| ~ spl55_376 ),
inference(superposition,[],[f634,f5171]) ).
fof(f74261,plain,
( $false
| ~ spl55_1
| spl55_272
| ~ spl55_376 ),
inference(forward_subsumption_resolution,[],[f74229,f4141]) ).
fof(f74262,plain,
( ~ spl55_1
| spl55_272
| ~ spl55_376 ),
inference(avatar_contradiction_clause,[],[f74261]) ).
fof(f74283,plain,
( ~ strictorderP(app(sK53,sK49))
| ssList(sK2(sK53,sK51))
| ssList(sK3(sK53,sK51))
| lt(sK52,sK51)
| lt(sK51,sK52)
| spl55_1
| ~ spl55_7
| ~ spl55_8
| spl55_10
| spl55_454 ),
inference(forward_subsumption_resolution,[],[f7702,f7297]) ).
fof(f74342,plain,
( ~ strictorderP(app(sK49,sK49))
| ssList(sK2(sK53,sK51))
| ssList(sK3(sK53,sK51))
| lt(sK52,sK51)
| lt(sK51,sK52)
| spl55_1
| ~ spl55_7
| ~ spl55_8
| spl55_10
| ~ spl55_376
| spl55_454 ),
inference(forward_demodulation,[],[f74283,f5171]) ).
fof(f74395,plain,
( ssList(sK2(sK49,sK51))
| ~ strictorderP(app(sK49,sK49))
| ssList(sK3(sK53,sK51))
| lt(sK52,sK51)
| lt(sK51,sK52)
| spl55_1
| ~ spl55_7
| ~ spl55_8
| spl55_10
| ~ spl55_376
| spl55_454 ),
inference(forward_demodulation,[],[f74342,f5171]) ).
fof(f74446,definition,
( spl55_3823
<=> ssList(sK2(sK49,sK51)) ),
introduced(definition,[new_symbols(definition,[spl55_3823])],[avatar_definition]) ).
fof(f74448,plain,
( ssList(sK2(sK49,sK51))
| ~ spl55_3823 ),
inference(avatar_component_clause,[],[f74446]) ).
fof(f74464,plain,
( ssList(sK3(sK49,sK51))
| ssList(sK2(sK49,sK51))
| ~ strictorderP(app(sK49,sK49))
| lt(sK52,sK51)
| lt(sK51,sK52)
| spl55_1
| ~ spl55_7
| ~ spl55_8
| spl55_10
| ~ spl55_376
| spl55_454 ),
inference(forward_demodulation,[],[f74395,f5171]) ).
fof(f74505,definition,
( spl55_3833
<=> ssList(sK3(sK49,sK51)) ),
introduced(definition,[new_symbols(definition,[spl55_3833])],[avatar_definition]) ).
fof(f74507,plain,
( ssList(sK3(sK49,sK51))
| ~ spl55_3833 ),
inference(avatar_component_clause,[],[f74505]) ).
fof(f74596,definition,
( spl55_3852
<=> strictorderP(app(sK49,sK49)) ),
introduced(definition,[new_symbols(definition,[spl55_3852])],[avatar_definition]) ).
fof(f74598,plain,
( ~ strictorderP(app(sK49,sK49))
| spl55_3852 ),
inference(avatar_component_clause,[],[f74596]) ).
fof(f74599,plain,
( spl55_476
| spl55_506
| ~ spl55_3852
| spl55_3823
| spl55_3833
| spl55_1
| ~ spl55_7
| ~ spl55_8
| spl55_10
| ~ spl55_376
| spl55_454 ),
inference(avatar_split_clause,[],[f74464,f7296,f5170,f677,f665,f660,f633,f74505,f74446,f74596,f7716,f7444]) ).
fof(f81609,plain,
( ~ strictorderP(sK49)
| ~ spl55_2808
| spl55_3852 ),
inference(superposition,[],[f74598,f60015]) ).
fof(f81695,plain,
( $false
| ~ spl55_7
| ~ spl55_8
| ~ spl55_2808
| spl55_3852 ),
inference(forward_subsumption_resolution,[],[f81609,f1722]) ).
fof(f81696,plain,
( ~ spl55_7
| ~ spl55_8
| ~ spl55_2808
| spl55_3852 ),
inference(avatar_contradiction_clause,[],[f81695]) ).
fof(f94662,plain,
( ~ ssItem(sK51)
| ssList(sK49)
| memberP(sK49,sK51)
| ~ spl55_3833 ),
inference(resolution,[],[f74507,f458]) ).
fof(f94663,plain,
( ssList(sK49)
| memberP(sK49,sK51)
| ~ spl55_3833 ),
inference(forward_subsumption_resolution,[],[f94662,f422]) ).
fof(f94664,plain,
( memberP(sK49,sK51)
| ~ spl55_3833 ),
inference(forward_subsumption_resolution,[],[f94663,f614]) ).
fof(f94665,plain,
( $false
| spl55_272
| ~ spl55_3833 ),
inference(forward_subsumption_resolution,[],[f94664,f4141]) ).
fof(f94666,plain,
( spl55_272
| ~ spl55_3833 ),
inference(avatar_contradiction_clause,[],[f94665]) ).
fof(f94814,plain,
( ~ ssItem(sK51)
| ssList(sK49)
| memberP(sK49,sK51)
| ~ spl55_3823 ),
inference(resolution,[],[f74448,f457]) ).
fof(f94815,plain,
( ssList(sK49)
| memberP(sK49,sK51)
| ~ spl55_3823 ),
inference(forward_subsumption_resolution,[],[f94814,f422]) ).
fof(f94816,plain,
( memberP(sK49,sK51)
| ~ spl55_3823 ),
inference(forward_subsumption_resolution,[],[f94815,f614]) ).
fof(f94817,plain,
( $false
| spl55_272
| ~ spl55_3823 ),
inference(forward_subsumption_resolution,[],[f94816,f4141]) ).
fof(f94818,plain,
( spl55_272
| ~ spl55_3823 ),
inference(avatar_contradiction_clause,[],[f94817]) ).
fof(f107820,plain,
( ~ ssItem(sK51)
| sK51 = sK52
| ~ spl55_7
| ~ spl55_8
| spl55_10
| spl55_272 ),
inference(resolution,[],[f11707,f4141]) ).
fof(f107835,plain,
( sK51 = sK52
| ~ spl55_7
| ~ spl55_8
| spl55_10
| spl55_272 ),
inference(forward_subsumption_resolution,[],[f107820,f422]) ).
fof(f107840,plain,
( $false
| ~ spl55_7
| ~ spl55_8
| spl55_10
| spl55_271
| spl55_272 ),
inference(forward_subsumption_resolution,[],[f107835,f4137]) ).
fof(f107841,plain,
( ~ spl55_7
| ~ spl55_8
| spl55_10
| spl55_271
| spl55_272 ),
inference(avatar_contradiction_clause,[],[f107840]) ).
fof(f107847,plain,
( ~ spl55_272
| spl55_1
| ~ spl55_376 ),
inference(avatar_split_clause,[],[f35677,f5170,f633,f4140]) ).
cnf(s1,plain,
( ~ spl55_1
| ~ spl55_2 ),
inference(sat_conversion,[],[f640]) ).
cnf(s8,plain,
( spl55_4
| spl55_7 ),
inference(sat_conversion,[],[f670]) ).
cnf(s9,plain,
( spl55_4
| spl55_8 ),
inference(sat_conversion,[],[f671]) ).
cnf(s18,plain,
~ spl55_10,
inference(sat_conversion,[],[f706]) ).
cnf(s26,plain,
( spl55_19
| spl55_24 ),
inference(sat_conversion,[],[f1124]) ).
cnf(s42,plain,
( spl55_2
| ~ spl55_17 ),
inference(sat_conversion,[],[f1223]) ).
cnf(s43,plain,
( spl55_1
| ~ spl55_19 ),
inference(sat_conversion,[],[f1228]) ).
cnf(s47,plain,
( spl55_10
| ~ spl55_26 ),
inference(sat_conversion,[],[f1503]) ).
cnf(s65,plain,
( ~ spl55_4
| spl55_26
| spl55_27 ),
inference(sat_conversion,[],[f1556]) ).
cnf(s95,plain,
( spl55_10
| ~ spl55_56 ),
inference(sat_conversion,[],[f2291]) ).
cnf(s174,plain,
( spl55_10
| ~ spl55_27 ),
inference(sat_conversion,[],[f3006]) ).
cnf(s175,plain,
( spl55_19
| spl55_74 ),
inference(sat_conversion,[],[f3010]) ).
cnf(s176,plain,
( spl55_19
| ~ spl55_73 ),
inference(sat_conversion,[],[f3014]) ).
cnf(s431,plain,
( ~ spl55_7
| ~ spl55_8
| spl55_10
| ~ spl55_24
| spl55_73
| ~ spl55_74
| spl55_293
| ~ spl55_396 ),
inference(sat_conversion,[],[f5373]) ).
cnf(s616,plain,
( ~ spl55_7
| spl55_26
| ~ spl55_271
| ~ spl55_454 ),
inference(sat_conversion,[],[f8778]) ).
cnf(s665,plain,
( ~ spl55_8
| ~ spl55_474 ),
inference(sat_conversion,[],[f10073]) ).
cnf(s1389,plain,
( ~ spl55_271
| spl55_474
| ~ spl55_506 ),
inference(sat_conversion,[],[f23157]) ).
cnf(s1498,plain,
( ~ spl55_7
| ~ spl55_24
| ~ spl55_78
| ~ spl55_293
| spl55_376 ),
inference(sat_conversion,[],[f23904]) ).
cnf(s3202,plain,
( spl55_73
| spl55_78
| ~ spl55_402 ),
inference(sat_conversion,[],[f48094]) ).
cnf(s3796,plain,
( ~ spl55_376
| spl55_759 ),
inference(sat_conversion,[],[f58215]) ).
cnf(s3799,plain,
( ~ spl55_271
| spl55_474
| ~ spl55_476 ),
inference(sat_conversion,[],[f58303]) ).
cnf(s4173,plain,
( ~ spl55_7
| ~ spl55_271
| ~ spl55_376
| spl55_454
| spl55_2808
| ~ spl55_2809 ),
inference(sat_conversion,[],[f60060]) ).
cnf(s4780,plain,
( ~ spl55_376
| ~ spl55_759
| spl55_2809 ),
inference(sat_conversion,[],[f66049]) ).
cnf(s5217,plain,
( ~ spl55_7
| spl55_10
| spl55_17
| ~ spl55_19
| ~ spl55_271
| spl55_454 ),
inference(sat_conversion,[],[f67799]) ).
cnf(s5652,plain,
( ~ spl55_7
| spl55_10
| ~ spl55_24
| spl55_73
| ~ spl55_74
| ~ spl55_293
| spl55_394 ),
inference(sat_conversion,[],[f69177]) ).
cnf(s5691,plain,
( spl55_56
| spl55_396 ),
inference(sat_conversion,[],[f69487]) ).
cnf(s5724,plain,
( spl55_2
| spl55_26
| ~ spl55_272 ),
inference(sat_conversion,[],[f70193]) ).
cnf(s7295,plain,
( spl55_376
| ~ spl55_394
| ~ spl55_396 ),
inference(sat_conversion,[],[f72481]) ).
cnf(s7398,plain,
( ~ spl55_7
| ~ spl55_8
| spl55_10
| ~ spl55_24
| spl55_73
| ~ spl55_74
| ~ spl55_396
| spl55_402 ),
inference(sat_conversion,[],[f72786]) ).
cnf(s7675,plain,
( ~ spl55_1
| spl55_272
| ~ spl55_376 ),
inference(sat_conversion,[],[f74262]) ).
cnf(s7714,plain,
( spl55_1
| ~ spl55_7
| ~ spl55_8
| spl55_10
| ~ spl55_376
| spl55_454
| spl55_476
| spl55_506
| spl55_3823
| spl55_3833
| ~ spl55_3852 ),
inference(sat_conversion,[],[f74599]) ).
cnf(s8719,plain,
( ~ spl55_7
| ~ spl55_8
| ~ spl55_2808
| spl55_3852 ),
inference(sat_conversion,[],[f81696]) ).
cnf(s10562,plain,
( spl55_272
| ~ spl55_3833 ),
inference(sat_conversion,[],[f94666]) ).
cnf(s10677,plain,
( spl55_272
| ~ spl55_3823 ),
inference(sat_conversion,[],[f94818]) ).
cnf(s12334,plain,
( ~ spl55_7
| ~ spl55_8
| spl55_10
| spl55_271
| spl55_272 ),
inference(sat_conversion,[],[f107841]) ).
cnf(s12337,plain,
( spl55_1
| ~ spl55_272
| ~ spl55_376 ),
inference(sat_conversion,[],[f107847]) ).
cnf(s12359,plain,
~ spl55_27,
inference(rat,[],[s174,s18]) ).
cnf(s12362,plain,
~ spl55_56,
inference(rat,[],[s95,s18]) ).
cnf(s12363,plain,
~ spl55_26,
inference(rat,[],[s47,s18]) ).
cnf(s12367,plain,
spl55_396,
inference(rat,[],[s5691,s12362]) ).
cnf(s12464,plain,
~ spl55_4,
inference(rat,[],[s65,s12359,s12363]) ).
cnf(s12532,plain,
spl55_8,
inference(rat,[],[s9,s12464]) ).
cnf(s12534,plain,
~ spl55_474,
inference(rat,[],[s665,s12532]) ).
cnf(s12535,plain,
spl55_7,
inference(rat,[],[s8,s12464]) ).
cnf(s12920,plain,
spl55_1,
inference(rat,[],[s8719,s4173,s7714,s616,s1389,s3799,s12334,s10562,s10677,s4780,s12337,s3796,s1498,s3202,s431,s7398,s26,s175,s176,s43,s12532,s12535,s18,s12363,s12534,s12367]) ).
cnf(s12921,plain,
~ spl55_2,
inference(rat,[],[s1,s12920]) ).
cnf(s12924,plain,
~ spl55_272,
inference(rat,[],[s5724,s12363,s12921]) ).
cnf(s12925,plain,
~ spl55_17,
inference(rat,[],[s42,s12921]) ).
cnf(s12941,plain,
~ spl55_376,
inference(rat,[],[s7675,s12920,s12924]) ).
cnf(s12942,plain,
spl55_271,
inference(rat,[],[s12334,s12535,s12532,s18,s12924]) ).
cnf(s13017,plain,
~ spl55_394,
inference(rat,[],[s7295,s12367,s12941]) ).
cnf(s13084,plain,
~ spl55_454,
inference(rat,[],[s616,s12535,s12363,s12942]) ).
cnf(s13174,plain,
~ spl55_19,
inference(rat,[],[s5217,s12925,s12942,s12535,s18,s13084]) ).
cnf(s13217,plain,
~ spl55_73,
inference(rat,[],[s176,s13174]) ).
cnf(s13218,plain,
spl55_74,
inference(rat,[],[s175,s13174]) ).
cnf(s13220,plain,
spl55_24,
inference(rat,[],[s26,s13174]) ).
cnf(s13289,plain,
spl55_293,
inference(rat,[],[s431,s12367,s13217,s13218,s12535,s12532,s18,s13220]) ).
cnf(s13290,plain,
$false,
inference(rat,[],[s5652,s13017,s13217,s13218,s12535,s18,s13220,s13289]) ).
fof(f107853,plain,
$false,
inference(avatar_sat_refutation,[],[s13290]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC184+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.36 % Computer : n018.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 28 08:23:18 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 Running first-order model finding
% 0.11/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.62/2.07 % (3225707)Will run a generic schedule for satisfiability detection.
% 11.62/2.07 % (3225713)% WARNING: option uhcvi not known.
% 11.62/2.07 % (3225712)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3166737868_2999 on theBenchmark for (2999ds/0Mi)
% 11.62/2.07 % (3225714)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2977598009:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 11.62/2.07 % (3225715)dis+10_1_sil=32000:sp=arity:random_seed=1460568200:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 11.62/2.07 % (3225716)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3021682840:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 11.62/2.07 % (3225717)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=84192814:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 11.62/2.07 % (3225718)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1922152155:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 11.62/2.07 % (3225713)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1915113164:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 11.62/2.07 % TRYING [1]
% 11.62/2.07 % TRYING [2]
% 11.62/2.07 % TRYING [3]
% 11.62/2.07 % TRYING [4]
% 11.62/2.07 % (3225715)Instruction limit reached!
% 11.62/2.07 % (3225715)------------------------------
% 11.62/2.07 % (3225715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.62/2.07 % (3225715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.07 % (3225715)CaDiCaL version: 2.1.3
% 11.62/2.07 % (3225715)Termination reason: Instruction limit
% 11.62/2.07 % (3225715)Termination phase: Saturation
% 11.62/2.07 % (3225715)Time elapsed: 0.061 s
% 11.62/2.07 % (3225715)Peak memory usage: 13 MB
% 11.62/2.07 % (3225715)Instructions burned: 104 (million)
% 11.62/2.07 % (3225716)Instruction limit reached!
% 11.62/2.07 % (3225716)------------------------------
% 11.62/2.07 % (3225716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.62/2.07 % (3225716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.07 % (3225716)CaDiCaL version: 2.1.3
% 11.62/2.07 % (3225716)Termination reason: Instruction limit
% 11.62/2.07 % (3225716)Termination phase: Saturation
% 11.62/2.07 % (3225716)Time elapsed: 0.070 s
% 11.62/2.07 % (3225716)Peak memory usage: 14 MB
% 11.62/2.07 % (3225716)Instructions burned: 117 (million)
% 11.62/2.07 % (3225717)Instruction limit reached!
% 11.62/2.07 % (3225717)------------------------------
% 11.62/2.07 % (3225717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.62/2.07 % (3225717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.07 % (3225717)CaDiCaL version: 2.1.3
% 11.62/2.07 % (3225717)Termination reason: Instruction limit
% 11.62/2.07 % (3225717)Termination phase: Saturation
% 11.62/2.07 % (3225717)Time elapsed: 0.076 s
% 11.62/2.07 % (3225717)Peak memory usage: 14 MB
% 11.62/2.07 % (3225717)Instructions burned: 131 (million)
% 11.62/2.07 % (3225726)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=895984233:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 11.62/2.07 % TRYING [5]
% 11.62/2.07 % (3225727)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3317410393:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 11.62/2.07 % (3225718)Instruction limit reached!
% 11.62/2.07 % (3225718)------------------------------
% 11.62/2.07 % (3225718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.62/2.07 % (3225718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.07 % (3225718)CaDiCaL version: 2.1.3
% 11.62/2.07 % (3225718)Termination reason: Instruction limit
% 11.62/2.07 % (3225718)Termination phase: Saturation
% 11.62/2.07 % (3225718)Time elapsed: 0.095 s
% 11.62/2.07 % (3225718)Peak memory usage: 15 MB
% 11.62/2.07 % (3225718)Instructions burned: 159 (million)
% 11.62/2.07 % TRYING [1]
% 11.62/2.07 % (3225728)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3126557816:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 11.62/2.07 % TRYING [2]
% 11.62/2.07 % TRYING [3]
% 11.62/2.07 % (3225731)ott-21_1_sil=16000:fs=off:random_seed=3921305497:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 11.62/2.07 % TRYING [4]
% 11.62/2.07 % (3225727)Instruction limit reached!
% 11.62/2.07 % (3225727)------------------------------
% 11.62/2.07 % (3225727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.62/2.07 % (3225727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.07 % (3225727)CaDiCaL version: 2.1.3
% 11.62/2.07 % (3225727)Termination reason: Instruction limit
% 11.62/2.07 % (3225727)Termination phase: Saturation
% 11.62/2.07 % (3225727)Time elapsed: 0.072 s
% 11.62/2.07 % (3225727)Peak memory usage: 14 MB
% 11.62/2.07 % (3225727)Instructions burned: 132 (million)
% 11.62/2.07 % TRYING [5]
% 11.62/2.07 % (3225734)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2957866769:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 11.62/2.07 % (3225731)Instruction limit reached!
% 11.62/2.07 % (3225731)------------------------------
% 11.62/2.07 % (3225731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.62/2.07 % (3225731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.07 % (3225731)CaDiCaL version: 2.1.3
% 11.62/2.07 % (3225731)Termination reason: Instruction limit
% 11.62/2.07 % (3225731)Termination phase: Saturation
% 11.62/2.07 % (3225731)Time elapsed: 0.090 s
% 11.62/2.07 % (3225731)Peak memory usage: 13 MB
% 11.62/2.07 % (3225731)Instructions burned: 181 (million)
% 11.62/2.07 % TRYING [6]
% 11.62/2.07 % (3225736)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2967439339:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 11.62/2.07 % TRYING [1]
% 11.62/2.07 % TRYING [2]
% 11.62/2.07 % TRYING [3]
% 11.62/2.07 % TRYING [4]
% 11.62/2.07 % TRYING [6]
% 11.62/2.07 % (3225726)Instruction limit reached!
% 11.62/2.07 % (3225726)------------------------------
% 11.62/2.07 % (3225726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.62/2.07 % (3225726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.07 % (3225726)CaDiCaL version: 2.1.3
% 11.62/2.07 % (3225726)Termination reason: Instruction limit
% 11.62/2.07 % (3225726)Termination phase: Finite model building constraint generation
% 11.62/2.07 % (3225726)Time elapsed: 0.296 s
% 11.62/2.07 % (3225726)Peak memory usage: 28 MB
% 11.62/2.07 % (3225726)Instructions burned: 717 (million)
% 11.62/2.07 % TRYING [5]
% 11.62/2.07 % (3225738)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1165543297:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 11.62/2.07 % (3225728)Instruction limit reached!
% 11.62/2.07 % (3225728)------------------------------
% 11.62/2.07 % (3225728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.62/2.07 % (3225728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.07 % (3225728)CaDiCaL version: 2.1.3
% 11.62/2.07 % (3225728)Termination reason: Instruction limit
% 11.62/2.07 % (3225728)Termination phase: Saturation
% 11.62/2.07 % (3225728)Time elapsed: 0.363 s
% 11.62/2.07 % (3225728)Peak memory usage: 22 MB
% 11.62/2.07 % (3225728)Instructions burned: 685 (million)
% 11.62/2.07 % (3225740)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2719093764:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 11.62/2.07 % TRYING [7]
% 11.62/2.07 % (3225734)Instruction limit reached!
% 11.62/2.07 % (3225734)------------------------------
% 11.62/2.07 % (3225734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.62/2.07 % (3225734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.07 % (3225734)CaDiCaL version: 2.1.3
% 11.62/2.07 % (3225734)Termination reason: Instruction limit
% 11.62/2.07 % (3225734)Termination phase: Saturation
% 11.62/2.07 % (3225734)Time elapsed: 0.326 s
% 11.62/2.07 % (3225734)Peak memory usage: 15 MB
% 11.62/2.07 % (3225734)Instructions burned: 477 (million)
% 11.62/2.07 % (3225742)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2075384850:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 11.62/2.07 % (3225736)Instruction limit reached!
% 11.62/2.07 % (3225736)------------------------------
% 11.62/2.07 % (3225736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.62/2.07 % (3225736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.07 % (3225736)CaDiCaL version: 2.1.3
% 11.62/2.07 % (3225736)Termination reason: Instruction limit
% 11.62/2.07 % (3225736)Termination phase: Finite model building SAT solving
% 11.62/2.07 % (3225736)Time elapsed: 0.348 s
% 11.62/2.07 % (3225736)Peak memory usage: 23 MB
% 11.62/2.07 % (3225736)Instructions burned: 865 (million)
% 11.62/2.07 % TRYING [14]
% 11.62/2.07 % (3225744)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2370330295:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 11.62/2.07 % (3225740)Instruction limit reached!
% 11.62/2.07 % (3225740)------------------------------
% 11.62/2.07 % (3225740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.62/2.07 % (3225740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.07 % (3225740)CaDiCaL version: 2.1.3
% 11.62/2.07 % (3225740)Termination reason: Instruction limit
% 11.62/2.07 % (3225740)Termination phase: Finite model building constraint generation
% 11.62/2.07 % (3225740)Time elapsed: 0.318 s
% 11.62/2.07 % (3225740)Peak memory usage: 71 MB
% 11.62/2.07 % (3225740)Instructions burned: 892 (million)
% 11.62/2.07 % (3225746)fmb+10_1_sil=64000:random_seed=665034930:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 11.62/2.07 % TRYING [1]
% 11.62/2.07 % TRYING [2]
% 11.62/2.07 % TRYING [3]
% 11.62/2.07 % TRYING [4]
% 11.62/2.07 % (3225742)Instruction limit reached!
% 11.62/2.07 % (3225742)------------------------------
% 11.62/2.07 % (3225742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.62/2.07 % (3225742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.07 % (3225742)CaDiCaL version: 2.1.3
% 11.62/2.07 % (3225742)Termination reason: Instruction limit
% 11.62/2.07 % (3225742)Termination phase: Saturation
% 11.62/2.07 % (3225742)Time elapsed: 0.378 s
% 11.62/2.07 % (3225742)Peak memory usage: 26 MB
% 11.62/2.07 % (3225742)Instructions burned: 692 (million)
% 11.62/2.07 % (3225748)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2741090978:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 11.62/2.07 % TRYING [20]
% 11.62/2.07 % TRYING [5]
% 11.62/2.07 % (3225738)Instruction limit reached!
% 11.62/2.07 % (3225738)------------------------------
% 11.62/2.07 % (3225738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.62/2.07 % (3225738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.07 % (3225738)CaDiCaL version: 2.1.3
% 11.62/2.07 % (3225738)Termination reason: Instruction limit
% 11.62/2.07 % (3225738)Termination phase: Saturation
% 11.62/2.07 % (3225738)Time elapsed: 0.648 s
% 11.62/2.07 % (3225738)Peak memory usage: 26 MB
% 11.62/2.07 % (3225738)Instructions burned: 1180 (million)
% 11.62/2.07 % (3225744)Instruction limit reached!
% 11.62/2.07 % (3225744)------------------------------
% 11.62/2.07 % (3225744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.62/2.07 % (3225744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.07 % (3225744)CaDiCaL version: 2.1.3
% 11.62/2.07 % (3225744)Termination reason: Instruction limit
% 11.62/2.07 % (3225744)Termination phase: Saturation
% 11.62/2.07 % (3225744)Time elapsed: 0.476 s
% 11.62/2.07 % (3225744)Peak memory usage: 21 MB
% 11.62/2.07 % (3225744)Instructions burned: 879 (million)
% 11.62/2.07 % (3225750)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1446709456:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 11.62/2.07 % TRYING [8]
% 11.62/2.07 % (3225752)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3920627593:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 11.62/2.07 % TRYING [8]
% 11.62/2.07 % TRYING [6]
% 11.62/2.07 % (3225750)Instruction limit reached!
% 11.62/2.07 % (3225750)------------------------------
% 11.62/2.07 % (3225750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.62/2.07 % (3225750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.07 % (3225750)CaDiCaL version: 2.1.3
% 11.62/2.07 % (3225750)Termination reason: Instruction limit
% 11.62/2.07 % (3225750)Termination phase: Finite model building constraint generation
% 11.62/2.07 % (3225750)Time elapsed: 0.341 s
% 11.62/2.07 % (3225750)Peak memory usage: 69 MB
% 11.62/2.07 % (3225750)Instructions burned: 920 (million)
% 11.62/2.07 % (3225754)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1200305494:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 11.62/2.07 % (3225713) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3225707-3225713"...
% 11.62/2.07 % (3225713)...printing done.
% 11.62/2.07 % (3225713)Refutation found. Thanks to Tanya!
% 11.62/2.07 % SZS status Theorem for theBenchmark
% 11.62/2.07 % SZS output start Proof for theBenchmark
% See solution above
% 11.62/2.08 % (3225713)------------------------------
% 11.62/2.08 % (3225713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.62/2.08 % (3225713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.08 % (3225713)CaDiCaL version: 2.1.3
% 11.62/2.08 % (3225713)Termination reason: Refutation
% 11.62/2.08 % (3225713)Time elapsed: 1.610 s
% 11.62/2.08 % (3225713)Peak memory usage: 67 MB
% 11.62/2.08 % (3225713)Instructions burned: 5886 (million)
% 11.62/2.08 % (3225707)Success in time 1.669 s
% 11.62/2.08 % Vampire exiting
%------------------------------------------------------------------------------