%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC299-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:05:27 PM UTC 2026
% Result : Unsatisfiable 59.60s 21.67s
% Output : Refutation 59.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 111
% Syntax : Number of formulae : 638 ( 51 unt; 60 def)
% Number of atoms : 2282 ( 274 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 2509 ( 865 ~;1584 |; 0 &)
% ( 60 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 70 ( 68 usr; 61 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 9 con; 0-2 aty)
% Number of variables : 383 ( 0 sgn 383 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f11,axiom,
~ singletonP(nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause11) ).
fof(f12,axiom,
! [X0] : ssItem(skaf83(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause12) ).
fof(f13,axiom,
! [X0] : ssList(skaf82(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause13) ).
fof(f56,axiom,
! [X0] :
( ~ ssList(X0)
| segmentP(X0,nil) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause56) ).
fof(f57,axiom,
! [X0] :
( ~ ssList(X0)
| segmentP(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause57) ).
fof(f58,axiom,
! [X0] :
( ~ ssList(X0)
| rearsegP(X0,nil) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause58) ).
fof(f60,axiom,
! [X0] :
( ~ ssList(X0)
| frontsegP(X0,nil) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause60) ).
fof(f71,axiom,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause71) ).
fof(f72,axiom,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f73,axiom,
! [X0] :
( ~ ssList(X0)
| app(X0,nil) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause73) ).
fof(f74,axiom,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause74) ).
fof(f75,axiom,
! [X0] :
( ~ ssList(X0)
| ssList(tl(X0))
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause75) ).
fof(f85,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ssList(app(X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ssList(cons(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause86) ).
fof(f96,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| tl(cons(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause96) ).
fof(f97,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| hd(cons(X0,X1)) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause97) ).
fof(f100,axiom,
! [X0,X1] :
( cons(X0,X1) != X1
| ~ ssItem(X0)
| ~ ssList(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause99) ).
fof(f107,axiom,
! [X0] :
( ~ ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause104) ).
fof(f112,axiom,
! [X0] :
( ~ ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause109) ).
fof(f119,axiom,
! [X0,X1] :
( cons(X0,nil) != X1
| ~ ssItem(X0)
| ~ ssList(X1)
| singletonP(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause116) ).
fof(f125,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| app(cons(X0,nil),X1) = cons(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause120) ).
fof(f126,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(reorient_equations,[],[f125]) ).
fof(f134,axiom,
! [X0,X1] :
( ~ segmentP(X0,X1)
| ~ segmentP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause127) ).
fof(f135,plain,
! [X0,X1] :
( ~ segmentP(X0,X1)
| ~ segmentP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X0 = X1 ),
inference(reorient_equations,[],[f134]) ).
fof(f136,axiom,
! [X0,X1] :
( ~ rearsegP(X0,X1)
| ~ rearsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause128) ).
fof(f137,plain,
! [X0,X1] :
( ~ rearsegP(X0,X1)
| ~ rearsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X0 = X1 ),
inference(reorient_equations,[],[f136]) ).
fof(f138,axiom,
! [X0,X1] :
( ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause129) ).
fof(f139,plain,
! [X0,X1] :
( ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X0 = X1 ),
inference(reorient_equations,[],[f138]) ).
fof(f148,axiom,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| frontsegP(app(X0,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause137) ).
fof(f149,axiom,
! [X2,X0,X1] :
( X0 != X1
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0)
| memberP(cons(X1,X2),X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause138) ).
fof(f151,axiom,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| memberP(app(X0,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause140) ).
fof(f152,axiom,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssItem(X1)
| memberP(app(X2,X0),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause141) ).
fof(f154,axiom,
! [X2,X0,X1] :
( app(X0,X1) != X2
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| rearsegP(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause143) ).
fof(f155,axiom,
! [X2,X0,X1] :
( app(X0,X1) != X2
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| frontsegP(X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause144) ).
fof(f162,axiom,
! [X2,X0,X1] :
( app(X0,X1) != app(X0,X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause150) ).
fof(f163,axiom,
! [X2,X0,X1] :
( app(X0,X1) != app(X2,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause151) ).
fof(f166,axiom,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| frontsegP(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause154) ).
fof(f173,axiom,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X2 = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause161) ).
fof(f174,plain,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X0 = X2 ),
inference(reorient_equations,[],[f173]) ).
fof(f186,axiom,
! [X2,X3,X0,X1] :
( ~ segmentP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X3)
| ~ ssList(X1)
| ~ ssList(X0)
| segmentP(app(app(X3,X0),X2),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause172) ).
fof(f187,axiom,
! [X2,X3,X0,X1] :
( app(app(X0,X1),X2) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| segmentP(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause173) ).
fof(f189,axiom,
! [X2,X3,X0,X1] :
( app(X0,cons(X1,X2)) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(X3)
| memberP(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause175) ).
fof(f190,axiom,
! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ~ ssList(X3)
| ~ ssList(X1)
| ~ ssItem(X2)
| ~ ssItem(X0)
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause176) ).
fof(f192,axiom,
! [X2,X3,X0,X1] :
( ~ frontsegP(X0,X1)
| X2 != X3
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X2)
| frontsegP(cons(X2,X0),cons(X3,X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause178) ).
fof(f193,axiom,
! [X2,X3,X0,X1,X4] :
( app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(X4)
| ~ ssList(X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(f200,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_1) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
ssItem(sk6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
ssList(sk8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_10) ).
fof(f210,negated_conjecture,
ssList(sk9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_11) ).
fof(f211,negated_conjecture,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_12) ).
fof(f212,plain,
sk1 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(reorient_equations,[],[f211]) ).
fof(f215,negated_conjecture,
( ssItem(sk10)
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_15) ).
fof(f226,negated_conjecture,
( cons(sk10,nil) = sk3
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_24) ).
fof(f227,plain,
( sk3 = cons(sk10,nil)
| nil = sk3 ),
inference(reorient_equations,[],[f226]) ).
fof(f232,plain,
ssList(sk3),
inference(definition_unfolding,[],[f200,f205]) ).
fof(f234,plain,
sk3 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(definition_unfolding,[],[f212,f205]) ).
fof(f242,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(cons(X0,nil))
| singletonP(cons(X0,nil)) ),
inference(equality_resolution,[],[f119]) ).
fof(f244,plain,
! [X2,X1] :
( ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X1)
| memberP(cons(X1,X2),X1) ),
inference(equality_resolution,[],[f149]) ).
fof(f245,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(X0,X1))
| rearsegP(app(X0,X1),X1) ),
inference(equality_resolution,[],[f154]) ).
fof(f246,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1))
| frontsegP(app(X0,X1),X0) ),
inference(equality_resolution,[],[f155]) ).
fof(f249,plain,
! [X2,X0,X1] :
( ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(app(X0,X1),X2))
| segmentP(app(app(X0,X1),X2),X1) ),
inference(equality_resolution,[],[f187]) ).
fof(f250,plain,
! [X2,X0,X1] :
( ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(app(X0,cons(X1,X2)))
| memberP(app(X0,cons(X1,X2)),X1) ),
inference(equality_resolution,[],[f189]) ).
fof(f251,plain,
! [X3,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X3)
| frontsegP(cons(X3,X0),cons(X3,X1)) ),
inference(equality_resolution,[],[f192]) ).
fof(f252,plain,
! [X2,X3,X0,X1] :
( ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(equality_resolution,[],[f193]) ).
fof(f263,plain,
~ ssList(nil),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f264,plain,
! [X0] : ~ ssList(skaf82(X0)),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f292,plain,
! [X0] :
( segmentP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f56]) ).
fof(f293,plain,
! [X0] :
( segmentP(X0,X0)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f57]) ).
fof(f294,plain,
! [X0] :
( ~ rearsegP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f58]) ).
fof(f296,plain,
! [X0] :
( ~ frontsegP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f303,plain,
! [X0,X1] :
( ssList(X0)
| ~ duplicatefreeP(X0)
| ssItem(X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f304,plain,
! [X0] :
( ssList(X0)
| app(X0,nil) = X0 ),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f305,plain,
! [X0] :
( ssList(X0)
| app(nil,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f306,plain,
! [X0] :
( ~ ssList(tl(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f316,plain,
! [X0,X1] :
( ~ ssList(app(X1,X0))
| ssList(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f317,plain,
! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1)
| ~ ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f327,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ssList(X1)
| tl(cons(X0,X1)) = X1 ),
inference(consistent_polarity_flipping,[],[f96]) ).
fof(f328,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ssList(X1)
| hd(cons(X0,X1)) = X0 ),
inference(consistent_polarity_flipping,[],[f97]) ).
fof(f330,plain,
! [X0,X1] :
( cons(X0,X1) != X1
| ~ ssItem(X0)
| ssList(X1) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f334,plain,
! [X0] :
( ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f337,plain,
! [X0] :
( ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f341,plain,
! [X0] :
( singletonP(cons(X0,nil))
| ssList(cons(X0,nil))
| ~ ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f242]) ).
fof(f344,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f351,plain,
! [X0,X1] :
( ~ segmentP(X1,X0)
| ~ segmentP(X0,X1)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f352,plain,
! [X0,X1] :
( rearsegP(X0,X1)
| rearsegP(X1,X0)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f137]) ).
fof(f353,plain,
! [X0,X1] :
( frontsegP(X0,X1)
| frontsegP(X1,X0)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f361,plain,
! [X2,X0,X1] :
( ~ frontsegP(app(X0,X2),X1)
| ssList(X2)
| ssList(X1)
| ssList(X0)
| frontsegP(X0,X1) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f362,plain,
! [X2,X1] :
( ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X1)
| memberP(cons(X1,X2),X1) ),
inference(consistent_polarity_flipping,[],[f244]) ).
fof(f364,plain,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ssList(X2)
| ssList(X0)
| ~ ssItem(X1)
| memberP(app(X0,X2),X1) ),
inference(consistent_polarity_flipping,[],[f151]) ).
fof(f365,plain,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ssList(X0)
| ssList(X2)
| ~ ssItem(X1)
| memberP(app(X2,X0),X1) ),
inference(consistent_polarity_flipping,[],[f152]) ).
fof(f367,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X0,X1))
| ~ rearsegP(app(X0,X1),X1) ),
inference(consistent_polarity_flipping,[],[f245]) ).
fof(f368,plain,
! [X0,X1] :
( ssList(X1)
| ssList(X0)
| ssList(app(X0,X1))
| ~ frontsegP(app(X0,X1),X0) ),
inference(consistent_polarity_flipping,[],[f246]) ).
fof(f373,plain,
! [X2,X0,X1] :
( app(X0,X1) != app(X0,X2)
| ssList(X1)
| ssList(X0)
| ssList(X2)
| X1 = X2 ),
inference(consistent_polarity_flipping,[],[f162]) ).
fof(f374,plain,
! [X2,X0,X1] :
( app(X0,X1) != app(X2,X1)
| ssList(X0)
| ssList(X1)
| ssList(X2)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f377,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,X2)
| frontsegP(X1,X2)
| ssList(X2)
| ssList(X1)
| ssList(X0)
| frontsegP(X0,X1) ),
inference(consistent_polarity_flipping,[],[f166]) ).
fof(f383,plain,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f394,plain,
! [X2,X3,X0,X1] :
( ~ segmentP(X0,X1)
| ssList(X2)
| ssList(X3)
| ssList(X1)
| ssList(X0)
| segmentP(app(app(X3,X0),X2),X1) ),
inference(consistent_polarity_flipping,[],[f186]) ).
fof(f395,plain,
! [X2,X0,X1] :
( segmentP(app(app(X0,X1),X2),X1)
| ssList(X0)
| ssList(X1)
| ssList(app(app(X0,X1),X2))
| ssList(X2) ),
inference(consistent_polarity_flipping,[],[f249]) ).
fof(f397,plain,
! [X2,X0,X1] :
( memberP(app(X0,cons(X1,X2)),X1)
| ssList(X0)
| ~ ssItem(X1)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2) ),
inference(consistent_polarity_flipping,[],[f250]) ).
fof(f398,plain,
! [X2,X3,X0,X1] :
( frontsegP(cons(X0,X1),cons(X2,X3))
| ssList(X3)
| ssList(X1)
| ~ ssItem(X2)
| ~ ssItem(X0)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f190]) ).
fof(f400,plain,
! [X3,X0,X1] :
( frontsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X3)
| ~ frontsegP(cons(X3,X0),cons(X3,X1)) ),
inference(consistent_polarity_flipping,[],[f251]) ).
fof(f401,plain,
! [X2,X3,X0,X1] :
( ssList(X3)
| ssList(X2)
| ssList(X0)
| ~ ssItem(X1)
| duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(consistent_polarity_flipping,[],[f252]) ).
fof(f408,plain,
~ ssList(sk3),
inference(consistent_polarity_flipping,[],[f232]) ).
fof(f412,plain,
~ ssList(sk7),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f413,plain,
~ ssList(sk8),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f414,plain,
~ ssList(sk9),
inference(consistent_polarity_flipping,[],[f210]) ).
fof(f419,plain,
! [X3,X0,X1] :
( ~ frontsegP(cons(X3,X0),cons(X3,X1))
| ssList(X1)
| ssList(X0)
| ~ ssItem(X3)
| frontsegP(X0,X1) ),
inference(duplicate_literal_removal,[],[f400]) ).
fof(f421,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssItem(X1)
| ssList(X2) ),
inference(duplicate_literal_removal,[],[f362]) ).
fof(f426,definition,
( spl0_1
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f427,plain,
( nil != sk3
| spl0_1 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f428,plain,
( nil = sk3
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f443,definition,
( spl0_5
<=> sk3 = cons(sk10,nil) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f445,plain,
( sk3 = cons(sk10,nil)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f446,plain,
( spl0_1
| spl0_5 ),
inference(avatar_split_clause,[],[f227,f443,f426]) ).
fof(f468,definition,
( spl0_9
<=> ssItem(sk10) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f470,plain,
( ssItem(sk10)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f471,plain,
( spl0_1
| spl0_9 ),
inference(avatar_split_clause,[],[f215,f468,f426]) ).
fof(f478,definition,
( spl0_11
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f479,plain,
( ~ ssList(nil)
| spl0_11 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f506,definition,
( spl0_17
<=> ! [X1] : ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f507,plain,
( ! [X1] : ssItem(X1)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f506]) ).
fof(f509,definition,
( spl0_18
<=> ! [X0] :
( ssList(X0)
| ~ duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f510,plain,
( ! [X0] :
( ~ duplicatefreeP(X0)
| ssList(X0) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f509]) ).
fof(f511,plain,
( spl0_17
| spl0_18 ),
inference(avatar_split_clause,[],[f303,f509,f506]) ).
fof(f514,plain,
~ spl0_11,
inference(avatar_split_clause,[],[f263,f478]) ).
fof(f518,plain,
( ! [X0] : ~ memberP(nil,X0)
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f71,f507]) ).
fof(f564,plain,
sk3 = app(sk3,nil),
inference(resolution,[],[f304,f408]) ).
fof(f599,plain,
sk3 = app(nil,sk3),
inference(resolution,[],[f305,f408]) ).
fof(f603,plain,
sk9 = app(nil,sk9),
inference(resolution,[],[f305,f414]) ).
fof(f632,plain,
( ! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1) )
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f317,f507]) ).
fof(f633,plain,
( ! [X0,X1] :
( ssList(X0)
| cons(X1,X0) = app(nil,cons(X1,X0)) )
| ~ spl0_17 ),
inference(resolution,[],[f632,f305]) ).
fof(f647,plain,
( ! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ssList(X2) )
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f421,f507]) ).
fof(f670,plain,
( ! [X0,X1] :
( ssList(X1)
| tl(cons(X0,X1)) = X1 )
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f327,f507]) ).
fof(f672,plain,
( ! [X0,X1] : skaf82(X1) = tl(cons(X0,skaf82(X1)))
| ~ spl0_17 ),
inference(resolution,[],[f670,f264]) ).
fof(f706,plain,
( ! [X0] : sk9 = tl(cons(X0,sk9))
| ~ spl0_17 ),
inference(resolution,[],[f670,f414]) ).
fof(f710,plain,
( ! [X0,X1] :
( ssList(X1)
| hd(cons(X0,X1)) = X0 )
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f328,f507]) ).
fof(f712,plain,
( ! [X0,X1] : hd(cons(X0,skaf82(X1))) = X0
| ~ spl0_17 ),
inference(resolution,[],[f710,f264]) ).
fof(f797,plain,
! [X0] :
( ssList(X0)
| nil = tl(X0)
| tl(X0) = cons(hd(tl(X0)),tl(tl(X0)))
| nil = X0 ),
inference(resolution,[],[f334,f306]) ).
fof(f824,definition,
( spl0_23
<=> nil = sk9 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f825,plain,
( nil != sk9
| spl0_23 ),
inference(avatar_component_clause,[],[f824]) ).
fof(f826,plain,
( nil = sk9
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f824]) ).
fof(f828,definition,
( spl0_24
<=> sk9 = cons(hd(sk9),tl(sk9)) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f830,plain,
( sk9 = cons(hd(sk9),tl(sk9))
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f828]) ).
fof(f842,definition,
( spl0_27
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f843,plain,
( nil != sk7
| spl0_27 ),
inference(avatar_component_clause,[],[f842]) ).
fof(f844,plain,
( nil = sk7
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f842]) ).
fof(f902,plain,
! [X0] :
( ssList(X0)
| nil = tl(X0)
| tl(X0) = cons(skaf83(tl(X0)),skaf82(tl(X0)))
| nil = X0 ),
inference(resolution,[],[f337,f306]) ).
fof(f909,definition,
( spl0_31
<=> sk9 = cons(skaf83(sk9),skaf82(sk9)) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f911,plain,
( sk9 = cons(skaf83(sk9),skaf82(sk9))
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f909]) ).
fof(f919,definition,
( spl0_33
<=> sk7 = cons(skaf83(sk7),skaf82(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f921,plain,
( sk7 = cons(skaf83(sk7),skaf82(sk7))
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f919]) ).
fof(f940,plain,
( sk3 = app(app(app(app(nil,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9)
| ~ spl0_27 ),
inference(superposition,[],[f234,f844]) ).
fof(f942,plain,
( sk3 = app(app(app(app(nil,cons(sk5,nil)),sk8),cons(sk6,nil)),nil)
| ~ spl0_23
| ~ spl0_27 ),
inference(forward_demodulation,[],[f940,f826]) ).
fof(f975,definition,
( spl0_36
<=> sk3 = cons(skaf83(sk3),skaf82(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f977,plain,
( sk3 = cons(skaf83(sk3),skaf82(sk3))
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f975]) ).
fof(f1010,definition,
( spl0_40
<=> ssList(app(app(app(nil,cons(sk5,nil)),sk8),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f1011,plain,
( ~ ssList(app(app(app(nil,cons(sk5,nil)),sk8),cons(sk6,nil)))
| spl0_40 ),
inference(avatar_component_clause,[],[f1010]) ).
fof(f1012,plain,
( ssList(app(app(app(nil,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f1010]) ).
fof(f1021,definition,
( spl0_42
<=> nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f1022,plain,
( nil != app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| spl0_42 ),
inference(avatar_component_clause,[],[f1021]) ).
fof(f1023,plain,
( nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f1021]) ).
fof(f1025,definition,
( spl0_43
<=> ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f1026,plain,
( ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| spl0_43 ),
inference(avatar_component_clause,[],[f1025]) ).
fof(f1027,plain,
( ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f1025]) ).
fof(f1144,plain,
! [X0] :
( ssList(X0)
| tl(cons(sk5,X0)) = X0 ),
inference(resolution,[],[f327,f206]) ).
fof(f1210,plain,
! [X0] :
( ssList(X0)
| cons(sk5,X0) = app(cons(sk5,nil),X0) ),
inference(resolution,[],[f344,f206]) ).
fof(f1212,plain,
( ! [X0] :
( ssList(X0)
| cons(sk10,X0) = app(cons(sk10,nil),X0) )
| ~ spl0_9 ),
inference(resolution,[],[f344,f470]) ).
fof(f1213,plain,
( ! [X0] :
( ssList(X0)
| cons(sk10,X0) = app(sk3,X0) )
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f1212,f445]) ).
fof(f1349,plain,
! [X0,X1] :
( ~ rearsegP(app(X0,X1),X1)
| ssList(X1)
| ssList(X0) ),
inference(forward_subsumption_resolution,[],[f367,f316]) ).
fof(f1351,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| rearsegP(X0,app(X1,X0))
| ssList(app(X1,X0))
| ssList(X0)
| app(X1,X0) = X0 ),
inference(resolution,[],[f1349,f352]) ).
fof(f1366,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| rearsegP(X0,app(X1,X0))
| ssList(app(X1,X0))
| app(X1,X0) = X0 ),
inference(duplicate_literal_removal,[],[f1351]) ).
fof(f1370,plain,
! [X0,X1] :
( rearsegP(X0,app(X1,X0))
| ssList(X1)
| ssList(X0)
| app(X1,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f1366,f316]) ).
fof(f1382,plain,
! [X0,X1] :
( ~ frontsegP(app(X0,X1),X0)
| ssList(X0)
| ssList(X1) ),
inference(forward_subsumption_resolution,[],[f368,f316]) ).
fof(f1384,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| frontsegP(X0,app(X0,X1))
| ssList(app(X0,X1))
| ssList(X0)
| app(X0,X1) = X0 ),
inference(resolution,[],[f1382,f353]) ).
fof(f1399,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| frontsegP(X0,app(X0,X1))
| ssList(app(X0,X1))
| app(X0,X1) = X0 ),
inference(duplicate_literal_removal,[],[f1384]) ).
fof(f1403,plain,
! [X0,X1] :
( frontsegP(X0,app(X0,X1))
| ssList(X1)
| ssList(X0)
| app(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f1399,f316]) ).
fof(f1717,plain,
! [X0] :
( ~ frontsegP(sk3,X0)
| ssList(sk9)
| ssList(X0)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| frontsegP(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),X0) ),
inference(superposition,[],[f361,f234]) ).
fof(f1727,plain,
! [X0] :
( ~ frontsegP(sk3,X0)
| ssList(X0)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| frontsegP(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),X0) ),
inference(forward_subsumption_resolution,[],[f1717,f414]) ).
fof(f1817,plain,
! [X2,X0,X1] :
( frontsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| ssList(X2)
| frontsegP(X2,X0)
| frontsegP(X1,X2)
| ssList(X2)
| ssList(X1)
| X1 = X2 ),
inference(resolution,[],[f377,f353]) ).
fof(f1818,plain,
! [X2,X0,X1] :
( frontsegP(X0,X1)
| frontsegP(X2,X0)
| frontsegP(X1,X2)
| ssList(X2)
| ssList(X1)
| ssList(X0)
| X1 = X2 ),
inference(duplicate_literal_removal,[],[f1817]) ).
fof(f1943,plain,
! [X0] :
( sk3 != app(sk3,X0)
| ssList(X0)
| ssList(sk3)
| ssList(nil)
| nil = X0 ),
inference(superposition,[],[f373,f564]) ).
fof(f1956,plain,
! [X0] :
( sk3 != app(sk3,X0)
| ssList(X0)
| ssList(nil)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f1943,f408]) ).
fof(f1978,plain,
( ! [X0] :
( sk3 != app(sk3,X0)
| ssList(X0)
| nil = X0 )
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f1956,f479]) ).
fof(f2023,plain,
! [X0] :
( sk3 != app(X0,sk9)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(sk9)
| ssList(X0)
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0 ),
inference(superposition,[],[f374,f234]) ).
fof(f2030,plain,
! [X0] :
( sk3 != app(X0,sk3)
| ssList(X0)
| ssList(sk3)
| ssList(nil)
| nil = X0 ),
inference(superposition,[],[f374,f599]) ).
fof(f2037,plain,
! [X0] :
( app(X0,nil) != sk3
| ssList(X0)
| ssList(nil)
| ssList(sk3)
| sk3 = X0 ),
inference(superposition,[],[f374,f564]) ).
fof(f2050,plain,
( ! [X0] :
( app(X0,nil) != sk3
| ssList(X0)
| ssList(sk3)
| sk3 = X0 )
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f2037,f479]) ).
fof(f2056,plain,
! [X0] :
( sk3 != app(X0,sk3)
| ssList(X0)
| ssList(nil)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f2030,f408]) ).
fof(f2062,plain,
! [X0] :
( sk3 != app(X0,sk9)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(X0)
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0 ),
inference(forward_subsumption_resolution,[],[f2023,f414]) ).
fof(f2072,plain,
( ! [X0] :
( app(X0,nil) != sk3
| ssList(X0)
| sk3 = X0 )
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f2050,f408]) ).
fof(f2078,plain,
( ! [X0] :
( sk3 != app(X0,sk3)
| ssList(X0)
| nil = X0 )
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f2056,f479]) ).
fof(f2370,definition,
( spl0_78
<=> ssList(tl(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f2371,plain,
( ~ ssList(tl(sk7))
| spl0_78 ),
inference(avatar_component_clause,[],[f2370]) ).
fof(f2372,plain,
( ssList(tl(sk7))
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f2370]) ).
fof(f2450,plain,
! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(X2)
| ssList(X2)
| segmentP(app(app(X1,X2),X0),X2)
| ssList(X2) ),
inference(resolution,[],[f394,f293]) ).
fof(f2451,plain,
! [X2,X0,X1] :
( segmentP(app(app(X1,X2),X0),X2)
| ssList(X1)
| ssList(X2)
| ssList(X0) ),
inference(duplicate_literal_removal,[],[f2450]) ).
fof(f2525,plain,
! [X0] :
( segmentP(app(sk3,X0),sk9)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(sk9)
| ssList(app(sk3,X0))
| ssList(X0) ),
inference(superposition,[],[f395,f234]) ).
fof(f2539,plain,
! [X0] :
( segmentP(app(sk3,X0),sk9)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(app(sk3,X0))
| ssList(X0) ),
inference(forward_subsumption_resolution,[],[f2525,f414]) ).
fof(f2557,definition,
( spl0_97
<=> ssList(cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f2558,plain,
( ~ ssList(cons(sk6,nil))
| spl0_97 ),
inference(avatar_component_clause,[],[f2557]) ).
fof(f2559,plain,
( ssList(cons(sk6,nil))
| ~ spl0_97 ),
inference(avatar_component_clause,[],[f2557]) ).
fof(f2561,definition,
( spl0_98
<=> ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f2562,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| spl0_98 ),
inference(avatar_component_clause,[],[f2561]) ).
fof(f2563,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_98 ),
inference(avatar_component_clause,[],[f2561]) ).
fof(f2565,definition,
( spl0_99
<=> segmentP(nil,cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f2566,plain,
( ~ segmentP(nil,cons(sk6,nil))
| spl0_99 ),
inference(avatar_component_clause,[],[f2565]) ).
fof(f2567,plain,
( segmentP(nil,cons(sk6,nil))
| ~ spl0_99 ),
inference(avatar_component_clause,[],[f2565]) ).
fof(f2675,plain,
( ! [X2,X3,X0,X1] :
( ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(X2)
| ssList(X0)
| ~ ssItem(X1)
| ssList(X3) )
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f401,f510]) ).
fof(f2696,definition,
( spl0_100
<=> ! [X3] : ssList(X3) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f2697,plain,
( ! [X3] : ssList(X3)
| ~ spl0_100 ),
inference(avatar_component_clause,[],[f2696]) ).
fof(f2699,definition,
( spl0_101
<=> ! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X1,cons(X2,X0)))
| ~ ssItem(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f2700,plain,
( ! [X2,X0,X1] :
( ssList(app(X1,cons(X2,X0)))
| ssList(X1)
| ssList(X0)
| ~ ssItem(X2) )
| ~ spl0_101 ),
inference(avatar_component_clause,[],[f2699]) ).
fof(f3091,plain,
sk3 = tl(cons(sk5,sk3)),
inference(resolution,[],[f1144,f408]) ).
fof(f3324,plain,
cons(sk5,sk8) = app(cons(sk5,nil),sk8),
inference(resolution,[],[f1210,f413]) ).
fof(f4077,plain,
( ssList(nil)
| ~ ssItem(sk6)
| ~ spl0_97 ),
inference(resolution,[],[f2559,f317]) ).
fof(f4078,plain,
( ~ ssItem(sk6)
| spl0_11
| ~ spl0_97 ),
inference(forward_subsumption_resolution,[],[f4077,f479]) ).
fof(f4079,plain,
( $false
| spl0_11
| ~ spl0_97 ),
inference(forward_subsumption_resolution,[],[f4078,f207]) ).
fof(f4080,plain,
( spl0_11
| ~ spl0_97 ),
inference(avatar_contradiction_clause,[],[f4079]) ).
fof(f4104,definition,
( spl0_167
<=> nil = cons(sk6,nil) ),
introduced(definition,[new_symbols(definition,[spl0_167])],[avatar_definition]) ).
fof(f4105,plain,
( nil != cons(sk6,nil)
| spl0_167 ),
inference(avatar_component_clause,[],[f4104]) ).
fof(f4106,plain,
( nil = cons(sk6,nil)
| ~ spl0_167 ),
inference(avatar_component_clause,[],[f4104]) ).
fof(f4166,definition,
( spl0_173
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_173])],[avatar_definition]) ).
fof(f4167,plain,
( ~ ssList(cons(sk5,nil))
| spl0_173 ),
inference(avatar_component_clause,[],[f4166]) ).
fof(f4168,plain,
( ssList(cons(sk5,nil))
| ~ spl0_173 ),
inference(avatar_component_clause,[],[f4166]) ).
fof(f4258,definition,
( spl0_182
<=> nil = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[spl0_182])],[avatar_definition]) ).
fof(f4259,plain,
( nil != cons(sk5,nil)
| spl0_182 ),
inference(avatar_component_clause,[],[f4258]) ).
fof(f4260,plain,
( nil = cons(sk5,nil)
| ~ spl0_182 ),
inference(avatar_component_clause,[],[f4258]) ).
fof(f5210,plain,
( $false
| ~ spl0_100 ),
inference(backward_subsumption_resolution,[],[f414,f2697]) ).
fof(f5244,plain,
~ spl0_100,
inference(avatar_contradiction_clause,[],[f5210]) ).
fof(f5326,plain,
( nil != nil
| ~ ssItem(sk5)
| ssList(nil)
| ~ spl0_182 ),
inference(superposition,[],[f330,f4260]) ).
fof(f5345,plain,
( ~ ssItem(sk5)
| ssList(nil)
| ~ spl0_182 ),
inference(trivial_inequality_removal,[],[f5326]) ).
fof(f5360,plain,
( ssList(nil)
| ~ spl0_182 ),
inference(forward_subsumption_resolution,[],[f5345,f206]) ).
fof(f5416,plain,
( spl0_11
| ~ spl0_182 ),
inference(avatar_split_clause,[],[f5360,f4258,f478]) ).
fof(f5499,plain,
( ! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ssList(X2)
| ssList(X0)
| memberP(app(X0,X2),X1) )
| ~ spl0_17 ),
inference(backward_subsumption_resolution,[],[f364,f507]) ).
fof(f5500,plain,
( ! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ssList(X0)
| ssList(X2)
| memberP(app(X2,X0),X1) )
| ~ spl0_17 ),
inference(backward_subsumption_resolution,[],[f365,f507]) ).
fof(f5508,plain,
( ! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ssList(X1)
| ~ ssItem(X2)
| memberP(X1,X2)
| X0 = X2 )
| ~ spl0_17 ),
inference(backward_subsumption_resolution,[],[f383,f507]) ).
fof(f5513,plain,
( ! [X2,X0,X1] :
( memberP(app(X0,cons(X1,X2)),X1)
| ssList(X0)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2) )
| ~ spl0_17 ),
inference(backward_subsumption_resolution,[],[f397,f507]) ).
fof(f5557,plain,
( ! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ssList(X1)
| memberP(X1,X2)
| X0 = X2 )
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f5508,f507]) ).
fof(f6609,definition,
( spl0_219
<=> ssList(sk7) ),
introduced(definition,[new_symbols(definition,[spl0_219])],[avatar_definition]) ).
fof(f6611,plain,
( ~ ssList(sk7)
| spl0_219 ),
inference(avatar_component_clause,[],[f6609]) ).
fof(f6666,plain,
~ spl0_219,
inference(avatar_split_clause,[],[f412,f6609]) ).
fof(f6682,plain,
( sk7 = cons(skaf83(sk7),skaf82(sk7))
| nil = sk7
| spl0_219 ),
inference(resolution,[],[f6611,f337]) ).
fof(f6715,plain,
( spl0_27
| spl0_33
| spl0_219 ),
inference(avatar_split_clause,[],[f6682,f6609,f919,f842]) ).
fof(f6777,plain,
( ssList(sk7)
| nil = sk7
| ~ spl0_78 ),
inference(resolution,[],[f2372,f306]) ).
fof(f6778,plain,
( nil = sk7
| ~ spl0_78
| spl0_219 ),
inference(forward_subsumption_resolution,[],[f6777,f6611]) ).
fof(f6779,plain,
( $false
| spl0_27
| ~ spl0_78
| spl0_219 ),
inference(forward_subsumption_resolution,[],[f6778,f843]) ).
fof(f6780,plain,
( spl0_27
| ~ spl0_78
| spl0_219 ),
inference(avatar_contradiction_clause,[],[f6779]) ).
fof(f7085,plain,
( ~ segmentP(cons(sk6,nil),nil)
| ssList(cons(sk6,nil))
| ssList(nil)
| nil = cons(sk6,nil)
| ~ spl0_99 ),
inference(resolution,[],[f2567,f351]) ).
fof(f7086,plain,
( ssList(cons(sk6,nil))
| ssList(nil)
| nil = cons(sk6,nil)
| ~ spl0_99 ),
inference(forward_subsumption_resolution,[],[f7085,f292]) ).
fof(f7091,plain,
( ssList(nil)
| nil = cons(sk6,nil)
| spl0_97
| ~ spl0_99 ),
inference(forward_subsumption_resolution,[],[f7086,f2558]) ).
fof(f7096,plain,
( nil = cons(sk6,nil)
| spl0_11
| spl0_97
| ~ spl0_99 ),
inference(forward_subsumption_resolution,[],[f7091,f479]) ).
fof(f7098,plain,
( spl0_167
| spl0_11
| spl0_97
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f7096,f2565,f2557,f478,f4104]) ).
fof(f7136,plain,
( singletonP(nil)
| ssList(nil)
| ~ ssItem(sk6)
| ~ spl0_167 ),
inference(superposition,[],[f341,f4106]) ).
fof(f7152,plain,
( ssList(nil)
| ~ ssItem(sk6)
| ~ spl0_167 ),
inference(forward_subsumption_resolution,[],[f7136,f11]) ).
fof(f7163,plain,
( ~ ssItem(sk6)
| spl0_11
| ~ spl0_167 ),
inference(forward_subsumption_resolution,[],[f7152,f479]) ).
fof(f7168,plain,
( $false
| spl0_11
| ~ spl0_167 ),
inference(forward_subsumption_resolution,[],[f7163,f207]) ).
fof(f7169,plain,
( spl0_11
| ~ spl0_167 ),
inference(avatar_contradiction_clause,[],[f7168]) ).
fof(f7289,definition,
( spl0_243
<=> ! [X0,X1] :
( frontsegP(sk3,cons(X0,X1))
| sk10 = X0
| ~ ssItem(X0)
| ssList(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_243])],[avatar_definition]) ).
fof(f7290,plain,
( ! [X0,X1] :
( frontsegP(sk3,cons(X0,X1))
| sk10 = X0
| ~ ssItem(X0)
| ssList(X1) )
| ~ spl0_243 ),
inference(avatar_component_clause,[],[f7289]) ).
fof(f7391,definition,
( spl0_262
<=> ! [X0] :
( ~ frontsegP(cons(sk10,X0),sk3)
| ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_262])],[avatar_definition]) ).
fof(f7392,plain,
( ! [X0] :
( ~ frontsegP(cons(sk10,X0),sk3)
| ssList(X0) )
| ~ spl0_262 ),
inference(avatar_component_clause,[],[f7391]) ).
fof(f7429,definition,
( spl0_269
<=> ssList(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_269])],[avatar_definition]) ).
fof(f7430,plain,
( ~ ssList(sk3)
| spl0_269 ),
inference(avatar_component_clause,[],[f7429]) ).
fof(f7469,plain,
~ spl0_269,
inference(avatar_split_clause,[],[f408,f7429]) ).
fof(f7539,plain,
( ! [X0] :
( ~ frontsegP(cons(sk10,X0),sk3)
| ssList(nil)
| ssList(X0)
| ~ ssItem(sk10)
| frontsegP(X0,nil) )
| ~ spl0_5 ),
inference(superposition,[],[f419,f445]) ).
fof(f7544,plain,
( ! [X0] :
( ~ frontsegP(cons(sk10,X0),sk3)
| ssList(X0)
| ~ ssItem(sk10)
| frontsegP(X0,nil) )
| ~ spl0_5
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f7539,f479]) ).
fof(f7556,plain,
( ! [X0] :
( ~ frontsegP(cons(sk10,X0),sk3)
| ssList(X0)
| frontsegP(X0,nil) )
| ~ spl0_5
| ~ spl0_9
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f7544,f470]) ).
fof(f7560,plain,
( ! [X0] :
( ~ frontsegP(cons(sk10,X0),sk3)
| ssList(X0) )
| ~ spl0_5
| ~ spl0_9
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f7556,f296]) ).
fof(f7562,plain,
( spl0_262
| ~ spl0_5
| ~ spl0_9
| spl0_11 ),
inference(avatar_split_clause,[],[f7560,f478,f468,f443,f7391]) ).
fof(f8368,plain,
( ! [X2,X0,X1] :
( ssList(cons(X0,X1))
| ssList(X2)
| memberP(app(X2,cons(X0,X1)),X0)
| ssList(X1) )
| ~ spl0_17 ),
inference(resolution,[],[f5500,f647]) ).
fof(f8377,plain,
( ! [X2,X0,X1] :
( memberP(app(X2,cons(X0,X1)),X0)
| ssList(X2)
| ssList(X1) )
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f8368,f632]) ).
fof(f8398,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ssList(nil)
| memberP(nil,X0)
| sk10 = X0 )
| ~ spl0_5
| ~ spl0_17 ),
inference(superposition,[],[f5557,f445]) ).
fof(f8401,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| memberP(nil,X0)
| sk10 = X0 )
| ~ spl0_5
| spl0_11
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f8398,f479]) ).
fof(f8404,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| sk10 = X0 )
| ~ spl0_5
| spl0_11
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f8401,f518]) ).
fof(f8636,plain,
( ! [X2,X3,X0,X1] :
( ssList(X0)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2)
| ssList(X3)
| ssList(app(X0,cons(X1,X2)))
| memberP(app(app(X0,cons(X1,X2)),X3),X1) )
| ~ spl0_17 ),
inference(resolution,[],[f5513,f5499]) ).
fof(f8642,plain,
( ! [X2,X3,X0,X1] :
( memberP(app(app(X0,cons(X1,X2)),X3),X1)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2)
| ssList(X3)
| ssList(X0) )
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f8636]) ).
fof(f9047,definition,
( spl0_329
<=> nil = cons(sk5,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_329])],[avatar_definition]) ).
fof(f9048,plain,
( nil != cons(sk5,sk3)
| spl0_329 ),
inference(avatar_component_clause,[],[f9047]) ).
fof(f9049,plain,
( nil = cons(sk5,sk3)
| ~ spl0_329 ),
inference(avatar_component_clause,[],[f9047]) ).
fof(f9051,definition,
( spl0_330
<=> ssList(cons(sk5,sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_330])],[avatar_definition]) ).
fof(f9052,plain,
( ~ ssList(cons(sk5,sk3))
| spl0_330 ),
inference(avatar_component_clause,[],[f9051]) ).
fof(f9053,plain,
( ssList(cons(sk5,sk3))
| ~ spl0_330 ),
inference(avatar_component_clause,[],[f9051]) ).
fof(f9059,plain,
( ssList(sk3)
| ~ ssItem(sk5)
| ~ spl0_330 ),
inference(resolution,[],[f9053,f317]) ).
fof(f9060,plain,
( ~ ssItem(sk5)
| spl0_269
| ~ spl0_330 ),
inference(forward_subsumption_resolution,[],[f9059,f7430]) ).
fof(f9061,plain,
( $false
| spl0_269
| ~ spl0_330 ),
inference(forward_subsumption_resolution,[],[f9060,f206]) ).
fof(f9062,plain,
( spl0_269
| ~ spl0_330 ),
inference(avatar_contradiction_clause,[],[f9061]) ).
fof(f9384,plain,
( memberP(nil,sk5)
| ~ ssItem(sk5)
| ssList(sk3)
| ~ spl0_329 ),
inference(superposition,[],[f421,f9049]) ).
fof(f9390,plain,
( ~ ssItem(sk5)
| ssList(sk3)
| ~ spl0_329 ),
inference(forward_subsumption_resolution,[],[f9384,f71]) ).
fof(f9395,plain,
( ssList(sk3)
| ~ spl0_329 ),
inference(forward_subsumption_resolution,[],[f9390,f206]) ).
fof(f9396,plain,
( $false
| spl0_269
| ~ spl0_329 ),
inference(forward_subsumption_resolution,[],[f9395,f7430]) ).
fof(f9397,plain,
( spl0_269
| ~ spl0_329 ),
inference(avatar_contradiction_clause,[],[f9396]) ).
fof(f9746,plain,
( ! [X0,X1] :
( frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| ssList(nil)
| ~ ssItem(X0)
| ~ ssItem(sk10)
| sk10 = X0 )
| ~ spl0_5 ),
inference(superposition,[],[f398,f445]) ).
fof(f9757,plain,
( ! [X0,X1] :
( frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(sk10)
| sk10 = X0 )
| ~ spl0_5
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f9746,f479]) ).
fof(f9767,plain,
( ! [X0,X1] :
( frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| ~ ssItem(X0)
| sk10 = X0 )
| ~ spl0_5
| ~ spl0_9
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f9757,f470]) ).
fof(f9775,plain,
( spl0_243
| ~ spl0_5
| ~ spl0_9
| spl0_11 ),
inference(avatar_split_clause,[],[f9767,f478,f468,f443,f7289]) ).
fof(f9786,plain,
( ! [X2,X3,X0,X1] :
( ssList(X0)
| ssList(X1)
| ~ ssItem(X2)
| ssList(X3)
| ssList(app(X1,cons(X2,X0)))
| ssList(cons(X2,X3)) )
| ~ spl0_18 ),
inference(resolution,[],[f2675,f316]) ).
fof(f9803,plain,
( ! [X2,X3,X0,X1] :
( ssList(X0)
| ssList(X1)
| ~ ssItem(X2)
| ssList(X3)
| ssList(app(X1,cons(X2,X0))) )
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f9786,f317]) ).
fof(f9812,plain,
( spl0_100
| spl0_101
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f9803,f509,f2699,f2696]) ).
fof(f10953,plain,
( ! [X0] : cons(sk10,skaf82(X0)) = app(sk3,skaf82(X0))
| ~ spl0_5
| ~ spl0_9 ),
inference(resolution,[],[f1213,f264]) ).
fof(f11318,definition,
( spl0_442
<=> sk6 = sk10 ),
introduced(definition,[new_symbols(definition,[spl0_442])],[avatar_definition]) ).
fof(f11320,plain,
( sk6 = sk10
| ~ spl0_442 ),
inference(avatar_component_clause,[],[f11318]) ).
fof(f12596,definition,
( spl0_542
<=> ! [X0] :
( segmentP(app(sk3,X0),sk9)
| ssList(X0)
| ssList(app(sk3,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl0_542])],[avatar_definition]) ).
fof(f12597,plain,
( ! [X0] :
( segmentP(app(sk3,X0),sk9)
| ssList(X0)
| ssList(app(sk3,X0)) )
| ~ spl0_542 ),
inference(avatar_component_clause,[],[f12596]) ).
fof(f12610,definition,
( spl0_545
<=> ssList(sk9) ),
introduced(definition,[new_symbols(definition,[spl0_545])],[avatar_definition]) ).
fof(f12611,plain,
( ~ ssList(sk9)
| spl0_545 ),
inference(avatar_component_clause,[],[f12610]) ).
fof(f12614,plain,
~ spl0_545,
inference(avatar_split_clause,[],[f414,f12610]) ).
fof(f12634,plain,
( cons(sk10,sk9) = app(sk3,sk9)
| ~ spl0_5
| ~ spl0_9
| spl0_545 ),
inference(resolution,[],[f12611,f1213]) ).
fof(f13023,plain,
( segmentP(sk3,sk9)
| ssList(nil)
| ssList(sk3)
| ~ spl0_542 ),
inference(superposition,[],[f12597,f564]) ).
fof(f13028,plain,
( segmentP(sk3,sk9)
| ssList(sk3)
| spl0_11
| ~ spl0_542 ),
inference(forward_subsumption_resolution,[],[f13023,f479]) ).
fof(f13033,plain,
( segmentP(sk3,sk9)
| spl0_11
| spl0_269
| ~ spl0_542 ),
inference(forward_subsumption_resolution,[],[f13028,f7430]) ).
fof(f13233,definition,
( spl0_596
<=> sk10 = hd(sk9) ),
introduced(definition,[new_symbols(definition,[spl0_596])],[avatar_definition]) ).
fof(f13235,plain,
( sk10 = hd(sk9)
| ~ spl0_596 ),
inference(avatar_component_clause,[],[f13233]) ).
fof(f13237,definition,
( spl0_597
<=> sk3 = sk9 ),
introduced(definition,[new_symbols(definition,[spl0_597])],[avatar_definition]) ).
fof(f13269,definition,
( spl0_601
<=> sk10 = skaf83(sk7) ),
introduced(definition,[new_symbols(definition,[spl0_601])],[avatar_definition]) ).
fof(f13271,plain,
( sk10 = skaf83(sk7)
| ~ spl0_601 ),
inference(avatar_component_clause,[],[f13269]) ).
fof(f13273,definition,
( spl0_602
<=> sk3 = sk7 ),
introduced(definition,[new_symbols(definition,[spl0_602])],[avatar_definition]) ).
fof(f13274,plain,
( sk3 = sk7
| ~ spl0_602 ),
inference(avatar_component_clause,[],[f13273]) ).
fof(f13347,plain,
( frontsegP(sk3,sk7)
| sk10 = skaf83(sk7)
| ~ ssItem(skaf83(sk7))
| ssList(skaf82(sk7))
| ~ spl0_33
| ~ spl0_243 ),
inference(superposition,[],[f7290,f921]) ).
fof(f13353,plain,
( frontsegP(sk3,sk7)
| sk10 = skaf83(sk7)
| ssList(skaf82(sk7))
| ~ spl0_33
| ~ spl0_243 ),
inference(forward_subsumption_resolution,[],[f13347,f12]) ).
fof(f13370,plain,
( frontsegP(sk3,sk7)
| sk10 = skaf83(sk7)
| ~ spl0_33
| ~ spl0_243 ),
inference(forward_subsumption_resolution,[],[f13353,f264]) ).
fof(f13387,definition,
( spl0_608
<=> frontsegP(sk3,sk7) ),
introduced(definition,[new_symbols(definition,[spl0_608])],[avatar_definition]) ).
fof(f13389,plain,
( frontsegP(sk3,sk7)
| ~ spl0_608 ),
inference(avatar_component_clause,[],[f13387]) ).
fof(f13390,plain,
( spl0_601
| spl0_608
| ~ spl0_33
| ~ spl0_243 ),
inference(avatar_split_clause,[],[f13370,f7289,f919,f13387,f13269]) ).
fof(f13456,definition,
( spl0_612
<=> frontsegP(sk7,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_612])],[avatar_definition]) ).
fof(f13457,plain,
( ~ frontsegP(sk7,sk3)
| spl0_612 ),
inference(avatar_component_clause,[],[f13456]) ).
fof(f13476,definition,
( spl0_613
<=> ! [X1] :
( ssList(X1)
| ssList(app(X1,sk3)) ) ),
introduced(definition,[new_symbols(definition,[spl0_613])],[avatar_definition]) ).
fof(f13477,plain,
( ! [X1] :
( ssList(app(X1,sk3))
| ssList(X1) )
| ~ spl0_613 ),
inference(avatar_component_clause,[],[f13476]) ).
fof(f13858,plain,
( ~ segmentP(sk9,sk3)
| ssList(sk9)
| ssList(sk3)
| sk3 = sk9
| spl0_11
| spl0_269
| ~ spl0_542 ),
inference(resolution,[],[f13033,f351]) ).
fof(f13859,plain,
( ~ segmentP(sk9,sk3)
| ssList(sk3)
| sk3 = sk9
| spl0_11
| spl0_269
| ~ spl0_542
| spl0_545 ),
inference(forward_subsumption_resolution,[],[f13858,f12611]) ).
fof(f13863,plain,
( ~ segmentP(sk9,sk3)
| sk3 = sk9
| spl0_11
| spl0_269
| ~ spl0_542
| spl0_545 ),
inference(forward_subsumption_resolution,[],[f13859,f7430]) ).
fof(f13868,definition,
( spl0_651
<=> segmentP(sk9,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_651])],[avatar_definition]) ).
fof(f13870,plain,
( ~ segmentP(sk9,sk3)
| spl0_651 ),
inference(avatar_component_clause,[],[f13868]) ).
fof(f13871,plain,
( spl0_597
| ~ spl0_651
| spl0_11
| spl0_269
| ~ spl0_542
| spl0_545 ),
inference(avatar_split_clause,[],[f13863,f12610,f12596,f7429,f478,f13868,f13237]) ).
fof(f21102,plain,
( ! [X0] :
( frontsegP(X0,sk7)
| ssList(sk7)
| ssList(X0)
| ssList(sk3)
| frontsegP(sk3,X0) )
| ~ spl0_608 ),
inference(resolution,[],[f13389,f377]) ).
fof(f21103,plain,
( ! [X0] :
( frontsegP(X0,sk7)
| ssList(X0)
| ssList(sk3)
| frontsegP(sk3,X0) )
| spl0_219
| ~ spl0_608 ),
inference(forward_subsumption_resolution,[],[f21102,f6611]) ).
fof(f21105,plain,
( ! [X0] :
( frontsegP(X0,sk7)
| ssList(X0)
| frontsegP(sk3,X0) )
| spl0_219
| spl0_269
| ~ spl0_608 ),
inference(forward_subsumption_resolution,[],[f21103,f7430]) ).
fof(f21726,plain,
( ! [X0] :
( ssList(app(X0,sk3))
| ssList(X0)
| ssList(skaf82(sk3))
| ~ ssItem(skaf83(sk3)) )
| ~ spl0_36
| ~ spl0_101 ),
inference(superposition,[],[f2700,f977]) ).
fof(f21736,plain,
( ! [X0] :
( ssList(app(X0,sk3))
| ssList(X0)
| ~ ssItem(skaf83(sk3)) )
| ~ spl0_36
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f21726,f264]) ).
fof(f21750,plain,
( ! [X0] :
( ssList(app(X0,sk3))
| ssList(X0) )
| ~ spl0_36
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f21736,f12]) ).
fof(f21763,plain,
( spl0_613
| ~ spl0_36
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f21750,f2699,f975,f13476]) ).
fof(f25678,plain,
( hd(sk9) = skaf83(sk9)
| ~ spl0_17
| ~ spl0_31 ),
inference(superposition,[],[f712,f911]) ).
fof(f26077,plain,
( tl(sk7) = skaf82(sk7)
| ~ spl0_17
| ~ spl0_33 ),
inference(superposition,[],[f672,f921]) ).
fof(f26078,plain,
( tl(sk9) = skaf82(sk9)
| ~ spl0_17
| ~ spl0_31 ),
inference(superposition,[],[f672,f911]) ).
fof(f26106,plain,
( sk7 = cons(skaf83(sk7),tl(sk7))
| ~ spl0_17
| ~ spl0_33 ),
inference(superposition,[],[f921,f26077]) ).
fof(f26113,plain,
( sk7 = cons(sk10,tl(sk7))
| ~ spl0_17
| ~ spl0_33
| ~ spl0_601 ),
inference(forward_demodulation,[],[f26106,f13271]) ).
fof(f26245,plain,
( ! [X0] :
( ssList(X0)
| ssList(X0)
| ssList(sk3) )
| ~ spl0_613 ),
inference(resolution,[],[f13477,f316]) ).
fof(f26249,plain,
( ! [X0] :
( ssList(X0)
| ssList(sk3) )
| ~ spl0_613 ),
inference(duplicate_literal_removal,[],[f26245]) ).
fof(f26254,plain,
( ! [X0] : ssList(X0)
| spl0_269
| ~ spl0_613 ),
inference(forward_subsumption_resolution,[],[f26249,f7430]) ).
fof(f26259,plain,
( spl0_100
| spl0_269
| ~ spl0_613 ),
inference(avatar_split_clause,[],[f26254,f13476,f7429,f2696]) ).
fof(f26416,plain,
( ! [X0] : cons(X0,sk9) = app(nil,cons(X0,sk9))
| ~ spl0_17
| spl0_545 ),
inference(resolution,[],[f633,f12611]) ).
fof(f27103,plain,
( ! [X0] :
( memberP(app(X0,sk9),skaf83(sk9))
| ssList(X0)
| ssList(skaf82(sk9)) )
| ~ spl0_17
| ~ spl0_31 ),
inference(superposition,[],[f8377,f911]) ).
fof(f27121,plain,
( ! [X0] :
( memberP(app(X0,sk9),skaf83(sk9))
| ssList(X0) )
| ~ spl0_17
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f27103,f264]) ).
fof(f27130,plain,
( ! [X0] :
( memberP(app(X0,sk9),hd(sk9))
| ssList(X0) )
| ~ spl0_17
| ~ spl0_31 ),
inference(forward_demodulation,[],[f27121,f25678]) ).
fof(f30338,plain,
! [X0] :
( segmentP(app(sk3,X0),sk3)
| ssList(nil)
| ssList(sk3)
| ssList(X0) ),
inference(superposition,[],[f2451,f599]) ).
fof(f30406,plain,
( segmentP(sk3,cons(sk6,nil))
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ssList(cons(sk6,nil))
| ssList(sk9) ),
inference(superposition,[],[f2451,f234]) ).
fof(f30478,plain,
( ! [X0] :
( segmentP(app(sk3,X0),sk3)
| ssList(sk3)
| ssList(X0) )
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f30338,f479]) ).
fof(f30552,plain,
( ! [X0] :
( segmentP(app(sk3,X0),sk3)
| ssList(X0) )
| spl0_11
| spl0_269 ),
inference(forward_subsumption_resolution,[],[f30478,f7430]) ).
fof(f34865,plain,
( ~ frontsegP(sk7,sk3)
| ssList(tl(sk7))
| ~ spl0_17
| ~ spl0_33
| ~ spl0_262
| ~ spl0_601 ),
inference(superposition,[],[f7392,f26113]) ).
fof(f34964,plain,
( ~ frontsegP(sk7,sk3)
| ~ spl0_17
| ~ spl0_33
| spl0_78
| ~ spl0_262
| ~ spl0_601 ),
inference(forward_subsumption_resolution,[],[f34865,f2371]) ).
fof(f34965,plain,
( ~ spl0_612
| ~ spl0_17
| ~ spl0_33
| spl0_78
| ~ spl0_262
| ~ spl0_601 ),
inference(avatar_split_clause,[],[f34964,f13269,f7391,f2370,f919,f506,f13456]) ).
fof(f40792,plain,
( sk9 = cons(sk10,tl(sk9))
| ~ spl0_24
| ~ spl0_596 ),
inference(superposition,[],[f830,f13235]) ).
fof(f54749,plain,
( ! [X0] :
( frontsegP(X0,sk7)
| frontsegP(sk3,X0)
| ssList(sk3)
| ssList(sk7)
| ssList(X0)
| sk3 = sk7 )
| spl0_612 ),
inference(resolution,[],[f1818,f13457]) ).
fof(f57330,plain,
( nil = tl(cons(sk5,sk3))
| tl(cons(sk5,sk3)) = cons(skaf83(tl(cons(sk5,sk3))),skaf82(tl(cons(sk5,sk3))))
| nil = cons(sk5,sk3)
| spl0_330 ),
inference(resolution,[],[f902,f9052]) ).
fof(f57364,plain,
( nil = tl(cons(sk5,sk3))
| tl(cons(sk5,sk3)) = cons(skaf83(tl(cons(sk5,sk3))),skaf82(tl(cons(sk5,sk3))))
| spl0_329
| spl0_330 ),
inference(forward_subsumption_resolution,[],[f57330,f9048]) ).
fof(f57387,plain,
( nil = sk3
| tl(cons(sk5,sk3)) = cons(skaf83(tl(cons(sk5,sk3))),skaf82(tl(cons(sk5,sk3))))
| spl0_329
| spl0_330 ),
inference(forward_demodulation,[],[f57364,f3091]) ).
fof(f70015,plain,
( memberP(sk3,sk6)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(nil)
| ssList(sk9)
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_17 ),
inference(superposition,[],[f8642,f234]) ).
fof(f70017,plain,
( memberP(sk3,sk6)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(sk9)
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| spl0_11
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f70015,f479]) ).
fof(f70066,plain,
( memberP(sk3,sk6)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| spl0_11
| ~ spl0_17
| spl0_545 ),
inference(forward_subsumption_resolution,[],[f70017,f12611]) ).
fof(f74977,definition,
( spl0_1670
<=> nil = cons(sk10,sk9) ),
introduced(definition,[new_symbols(definition,[spl0_1670])],[avatar_definition]) ).
fof(f74978,plain,
( nil != cons(sk10,sk9)
| spl0_1670 ),
inference(avatar_component_clause,[],[f74977]) ).
fof(f74981,definition,
( spl0_1671
<=> ssList(cons(sk10,sk9)) ),
introduced(definition,[new_symbols(definition,[spl0_1671])],[avatar_definition]) ).
fof(f74982,plain,
( ~ ssList(cons(sk10,sk9))
| spl0_1671 ),
inference(avatar_component_clause,[],[f74981]) ).
fof(f74983,plain,
( ssList(cons(sk10,sk9))
| ~ spl0_1671 ),
inference(avatar_component_clause,[],[f74981]) ).
fof(f75441,definition,
( spl0_1674
<=> ssList(app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_1674])],[avatar_definition]) ).
fof(f75442,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| spl0_1674 ),
inference(avatar_component_clause,[],[f75441]) ).
fof(f75443,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_1674 ),
inference(avatar_component_clause,[],[f75441]) ).
fof(f75479,plain,
( ssList(sk7)
| ssList(cons(sk5,nil))
| ~ spl0_1674 ),
inference(resolution,[],[f75443,f316]) ).
fof(f75480,plain,
( ssList(cons(sk5,nil))
| spl0_219
| ~ spl0_1674 ),
inference(forward_subsumption_resolution,[],[f75479,f6611]) ).
fof(f75481,plain,
( spl0_173
| spl0_219
| ~ spl0_1674 ),
inference(avatar_split_clause,[],[f75480,f75441,f6609,f4166]) ).
fof(f87242,plain,
( sk3 = cons(skaf83(sk3),skaf82(sk3))
| nil = sk3
| spl0_329
| spl0_330 ),
inference(forward_demodulation,[],[f57387,f3091]) ).
fof(f90058,definition,
( spl0_3056
<=> memberP(sk3,sk6) ),
introduced(definition,[new_symbols(definition,[spl0_3056])],[avatar_definition]) ).
fof(f90060,plain,
( memberP(sk3,sk6)
| ~ spl0_3056 ),
inference(avatar_component_clause,[],[f90058]) ).
fof(f91070,plain,
( segmentP(sk3,cons(sk6,nil))
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ssList(sk9)
| spl0_97 ),
inference(forward_subsumption_resolution,[],[f30406,f2558]) ).
fof(f91390,plain,
( segmentP(sk3,cons(sk6,nil))
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| spl0_97
| spl0_545 ),
inference(forward_subsumption_resolution,[],[f91070,f12611]) ).
fof(f91700,plain,
( ~ ssList(cons(sk5,nil))
| ~ spl0_1
| spl0_330 ),
inference(superposition,[],[f9052,f428]) ).
fof(f91755,plain,
( ~ spl0_173
| ~ spl0_1
| spl0_330 ),
inference(avatar_split_clause,[],[f91700,f9051,f426,f4166]) ).
fof(f92037,definition,
( spl0_3173
<=> ! [X0] :
( memberP(app(X0,sk9),hd(sk9))
| ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_3173])],[avatar_definition]) ).
fof(f92038,plain,
( ! [X0] :
( memberP(app(X0,sk9),hd(sk9))
| ssList(X0) )
| ~ spl0_3173 ),
inference(avatar_component_clause,[],[f92037]) ).
fof(f94265,plain,
( spl0_3173
| ~ spl0_17
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f27130,f909,f506,f92037]) ).
fof(f97984,definition,
( spl0_3500
<=> nil = cons(sk5,sk8) ),
introduced(definition,[new_symbols(definition,[spl0_3500])],[avatar_definition]) ).
fof(f97985,plain,
( nil != cons(sk5,sk8)
| spl0_3500 ),
inference(avatar_component_clause,[],[f97984]) ).
fof(f97986,plain,
( nil = cons(sk5,sk8)
| ~ spl0_3500 ),
inference(avatar_component_clause,[],[f97984]) ).
fof(f97988,definition,
( spl0_3501
<=> ssList(cons(sk5,sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_3501])],[avatar_definition]) ).
fof(f97989,plain,
( ~ ssList(cons(sk5,sk8))
| spl0_3501 ),
inference(avatar_component_clause,[],[f97988]) ).
fof(f97990,plain,
( ssList(cons(sk5,sk8))
| ~ spl0_3501 ),
inference(avatar_component_clause,[],[f97988]) ).
fof(f97992,definition,
( spl0_3502
<=> ssList(sk8) ),
introduced(definition,[new_symbols(definition,[spl0_3502])],[avatar_definition]) ).
fof(f97994,plain,
( ~ ssList(sk8)
| spl0_3502 ),
inference(avatar_component_clause,[],[f97992]) ).
fof(f98089,plain,
( segmentP(nil,cons(sk6,nil))
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_1
| spl0_97
| spl0_545 ),
inference(forward_demodulation,[],[f91390,f428]) ).
fof(f98616,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_1
| spl0_97
| spl0_99
| spl0_545 ),
inference(forward_subsumption_resolution,[],[f98089,f2566]) ).
fof(f98733,plain,
( spl0_98
| ~ spl0_1
| spl0_97
| spl0_99
| spl0_545 ),
inference(avatar_split_clause,[],[f98616,f12610,f2565,f2557,f426,f2561]) ).
fof(f98765,plain,
~ spl0_3502,
inference(avatar_split_clause,[],[f413,f97992]) ).
fof(f100773,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ssList(sk8)
| ~ spl0_98 ),
inference(resolution,[],[f2563,f316]) ).
fof(f104570,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_98
| spl0_3502 ),
inference(forward_subsumption_resolution,[],[f100773,f97994]) ).
fof(f104585,definition,
( spl0_3872
<=> ! [X0] :
( frontsegP(X0,sk7)
| ssList(X0)
| frontsegP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_3872])],[avatar_definition]) ).
fof(f104586,plain,
( ! [X0] :
( frontsegP(X0,sk7)
| frontsegP(sk3,X0)
| ssList(X0) )
| ~ spl0_3872 ),
inference(avatar_component_clause,[],[f104585]) ).
fof(f104898,plain,
( spl0_1
| spl0_36
| spl0_329
| spl0_330 ),
inference(avatar_split_clause,[],[f87242,f9051,f9047,f975,f426]) ).
fof(f104903,plain,
( spl0_3872
| spl0_219
| spl0_269
| ~ spl0_608 ),
inference(avatar_split_clause,[],[f21105,f13387,f7429,f6609,f104585]) ).
fof(f105189,definition,
( spl0_3967
<=> ! [X0] :
( ~ frontsegP(sk3,X0)
| frontsegP(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),X0)
| ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_3967])],[avatar_definition]) ).
fof(f105190,plain,
( ! [X0] :
( frontsegP(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),X0)
| ~ frontsegP(sk3,X0)
| ssList(X0) )
| ~ spl0_3967 ),
inference(avatar_component_clause,[],[f105189]) ).
fof(f105191,plain,
( spl0_43
| spl0_3967 ),
inference(avatar_split_clause,[],[f1727,f105189,f1025]) ).
fof(f105200,definition,
( spl0_3969
<=> ! [X0] :
( sk3 != app(X0,sk9)
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0
| ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_3969])],[avatar_definition]) ).
fof(f105201,plain,
( ! [X0] :
( sk3 != app(X0,sk9)
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0
| ssList(X0) )
| ~ spl0_3969 ),
inference(avatar_component_clause,[],[f105200]) ).
fof(f105203,plain,
( spl0_43
| spl0_3969 ),
inference(avatar_split_clause,[],[f2062,f105200,f1025]) ).
fof(f105204,plain,
( spl0_43
| spl0_542 ),
inference(avatar_split_clause,[],[f2539,f12596,f1025]) ).
fof(f106300,plain,
( spl0_1674
| ~ spl0_98
| spl0_3502 ),
inference(avatar_split_clause,[],[f104570,f97992,f2561,f75441]) ).
fof(f111974,plain,
( ssList(app(app(nil,cons(sk5,nil)),sk8))
| ssList(cons(sk6,nil))
| ~ spl0_40 ),
inference(resolution,[],[f1012,f316]) ).
fof(f111975,plain,
( ssList(app(app(nil,cons(sk5,nil)),sk8))
| ~ spl0_40
| spl0_97 ),
inference(forward_subsumption_resolution,[],[f111974,f2558]) ).
fof(f111976,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ssList(cons(sk6,nil))
| ~ spl0_43 ),
inference(resolution,[],[f1027,f316]) ).
fof(f115430,plain,
( ssList(nil)
| ~ spl0_17
| ~ spl0_173 ),
inference(resolution,[],[f4168,f632]) ).
fof(f115431,plain,
( $false
| spl0_11
| ~ spl0_17
| ~ spl0_173 ),
inference(forward_subsumption_resolution,[],[f115430,f479]) ).
fof(f115432,plain,
( spl0_11
| ~ spl0_17
| ~ spl0_173 ),
inference(avatar_contradiction_clause,[],[f115431]) ).
fof(f116028,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_43
| spl0_97 ),
inference(forward_subsumption_resolution,[],[f111976,f2558]) ).
fof(f116946,plain,
( spl0_98
| ~ spl0_43
| spl0_97 ),
inference(avatar_split_clause,[],[f116028,f2557,f1025,f2561]) ).
fof(f117039,plain,
( spl0_98
| spl0_43
| spl0_3056
| spl0_11
| ~ spl0_17
| spl0_545 ),
inference(avatar_split_clause,[],[f70066,f12610,f506,f478,f90058,f1025,f2561]) ).
fof(f119198,plain,
( rearsegP(cons(sk6,nil),nil)
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ssList(cons(sk6,nil))
| nil = cons(sk6,nil)
| ~ spl0_42 ),
inference(superposition,[],[f1370,f1023]) ).
fof(f119227,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ssList(cons(sk6,nil))
| nil = cons(sk6,nil)
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f119198,f294]) ).
fof(f119271,plain,
( ssList(cons(sk6,nil))
| nil = cons(sk6,nil)
| ~ spl0_42
| spl0_98 ),
inference(forward_subsumption_resolution,[],[f119227,f2562]) ).
fof(f119309,plain,
( nil = cons(sk6,nil)
| ~ spl0_42
| spl0_97
| spl0_98 ),
inference(forward_subsumption_resolution,[],[f119271,f2558]) ).
fof(f119327,plain,
( $false
| ~ spl0_42
| spl0_97
| spl0_98
| spl0_167 ),
inference(forward_subsumption_resolution,[],[f119309,f4105]) ).
fof(f119328,plain,
( ~ spl0_42
| spl0_97
| spl0_98
| spl0_167 ),
inference(avatar_contradiction_clause,[],[f119327]) ).
fof(f119391,plain,
( ! [X0] :
( ~ frontsegP(sk3,X0)
| ssList(X0)
| ssList(cons(sk6,nil))
| ssList(X0)
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| frontsegP(app(app(sk7,cons(sk5,nil)),sk8),X0) )
| ~ spl0_3967 ),
inference(resolution,[],[f105190,f361]) ).
fof(f119393,plain,
( ! [X0] :
( ~ frontsegP(sk3,X0)
| ssList(X0)
| ssList(cons(sk6,nil))
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| frontsegP(app(app(sk7,cons(sk5,nil)),sk8),X0) )
| ~ spl0_3967 ),
inference(duplicate_literal_removal,[],[f119391]) ).
fof(f119398,plain,
( ! [X0] :
( ~ frontsegP(sk3,X0)
| ssList(X0)
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| frontsegP(app(app(sk7,cons(sk5,nil)),sk8),X0) )
| spl0_97
| ~ spl0_3967 ),
inference(forward_subsumption_resolution,[],[f119393,f2558]) ).
fof(f119402,plain,
( ! [X0] :
( frontsegP(app(app(sk7,cons(sk5,nil)),sk8),X0)
| ssList(X0)
| ~ frontsegP(sk3,X0) )
| spl0_97
| spl0_98
| ~ spl0_3967 ),
inference(forward_subsumption_resolution,[],[f119398,f2562]) ).
fof(f119406,plain,
( sk6 = sk10
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_3056 ),
inference(resolution,[],[f90060,f8404]) ).
fof(f119891,plain,
( spl0_442
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_3056 ),
inference(avatar_split_clause,[],[f119406,f90058,f506,f478,f443,f11318]) ).
fof(f120096,plain,
( sk3 != sk9
| nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ssList(nil)
| ~ spl0_3969 ),
inference(superposition,[],[f105201,f603]) ).
fof(f124102,definition,
( spl0_4540
<=> nil = app(sk3,sk9) ),
introduced(definition,[new_symbols(definition,[spl0_4540])],[avatar_definition]) ).
fof(f124103,plain,
( nil != app(sk3,sk9)
| spl0_4540 ),
inference(avatar_component_clause,[],[f124102]) ).
fof(f124104,plain,
( nil = app(sk3,sk9)
| ~ spl0_4540 ),
inference(avatar_component_clause,[],[f124102]) ).
fof(f137325,plain,
( frontsegP(sk3,nil)
| ssList(sk9)
| ssList(sk3)
| nil = sk3
| ~ spl0_4540 ),
inference(superposition,[],[f1403,f124104]) ).
fof(f137345,plain,
( ssList(sk9)
| ssList(sk3)
| nil = sk3
| ~ spl0_4540 ),
inference(forward_subsumption_resolution,[],[f137325,f296]) ).
fof(f137371,plain,
( ssList(sk3)
| nil = sk3
| spl0_545
| ~ spl0_4540 ),
inference(forward_subsumption_resolution,[],[f137345,f12611]) ).
fof(f137395,plain,
( nil = sk3
| spl0_269
| spl0_545
| ~ spl0_4540 ),
inference(forward_subsumption_resolution,[],[f137371,f7430]) ).
fof(f137408,plain,
( $false
| spl0_1
| spl0_269
| spl0_545
| ~ spl0_4540 ),
inference(forward_subsumption_resolution,[],[f137395,f427]) ).
fof(f137409,plain,
( spl0_1
| spl0_269
| spl0_545
| ~ spl0_4540 ),
inference(avatar_contradiction_clause,[],[f137408]) ).
fof(f137414,plain,
( ssList(sk9)
| ~ spl0_17
| ~ spl0_1671 ),
inference(resolution,[],[f74983,f632]) ).
fof(f137415,plain,
( $false
| ~ spl0_17
| spl0_545
| ~ spl0_1671 ),
inference(forward_subsumption_resolution,[],[f137414,f12611]) ).
fof(f137416,plain,
( ~ spl0_17
| spl0_545
| ~ spl0_1671 ),
inference(avatar_contradiction_clause,[],[f137415]) ).
fof(f137457,plain,
( nil = tl(cons(sk10,sk9))
| tl(cons(sk10,sk9)) = cons(hd(tl(cons(sk10,sk9))),tl(tl(cons(sk10,sk9))))
| nil = cons(sk10,sk9)
| spl0_1671 ),
inference(resolution,[],[f74982,f797]) ).
fof(f137461,plain,
( nil = tl(cons(sk10,sk9))
| tl(cons(sk10,sk9)) = cons(skaf83(tl(cons(sk10,sk9))),skaf82(tl(cons(sk10,sk9))))
| nil = cons(sk10,sk9)
| spl0_1671 ),
inference(resolution,[],[f74982,f902]) ).
fof(f138117,plain,
( nil = sk9
| tl(cons(sk10,sk9)) = cons(skaf83(tl(cons(sk10,sk9))),skaf82(tl(cons(sk10,sk9))))
| nil = cons(sk10,sk9)
| ~ spl0_17
| spl0_1671 ),
inference(forward_demodulation,[],[f137461,f706]) ).
fof(f138118,plain,
( nil = sk9
| tl(cons(sk10,sk9)) = cons(hd(tl(cons(sk10,sk9))),tl(tl(cons(sk10,sk9))))
| nil = cons(sk10,sk9)
| ~ spl0_17
| spl0_1671 ),
inference(forward_demodulation,[],[f137457,f706]) ).
fof(f138448,plain,
( tl(cons(sk10,sk9)) = cons(skaf83(tl(cons(sk10,sk9))),skaf82(tl(cons(sk10,sk9))))
| nil = cons(sk10,sk9)
| ~ spl0_17
| spl0_23
| spl0_1671 ),
inference(forward_subsumption_resolution,[],[f138117,f825]) ).
fof(f138449,plain,
( tl(cons(sk10,sk9)) = cons(hd(tl(cons(sk10,sk9))),tl(tl(cons(sk10,sk9))))
| nil = cons(sk10,sk9)
| ~ spl0_17
| spl0_23
| spl0_1671 ),
inference(forward_subsumption_resolution,[],[f138118,f825]) ).
fof(f138464,plain,
( sk9 = cons(skaf83(sk9),skaf82(sk9))
| nil = cons(sk10,sk9)
| ~ spl0_17
| spl0_23
| spl0_1671 ),
inference(forward_demodulation,[],[f138448,f706]) ).
fof(f138465,plain,
( sk9 = cons(hd(sk9),tl(sk9))
| nil = cons(sk10,sk9)
| ~ spl0_17
| spl0_23
| spl0_1671 ),
inference(forward_demodulation,[],[f138449,f706]) ).
fof(f138478,plain,
( nil != cons(sk10,sk9)
| ~ spl0_5
| ~ spl0_9
| spl0_545
| spl0_4540 ),
inference(superposition,[],[f124103,f12634]) ).
fof(f138479,plain,
( ~ spl0_1670
| ~ spl0_5
| ~ spl0_9
| spl0_545
| spl0_4540 ),
inference(avatar_split_clause,[],[f138478,f124102,f12610,f468,f443,f74977]) ).
fof(f162550,definition,
( spl0_7173
<=> ssList(app(nil,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_7173])],[avatar_definition]) ).
fof(f162551,plain,
( ~ ssList(app(nil,cons(sk5,nil)))
| spl0_7173 ),
inference(avatar_component_clause,[],[f162550]) ).
fof(f162552,plain,
( ssList(app(nil,cons(sk5,nil)))
| ~ spl0_7173 ),
inference(avatar_component_clause,[],[f162550]) ).
fof(f162558,plain,
( ssList(nil)
| ssList(cons(sk5,nil))
| ~ spl0_7173 ),
inference(resolution,[],[f162552,f316]) ).
fof(f162559,plain,
( ssList(nil)
| ~ spl0_17
| ~ spl0_7173 ),
inference(forward_subsumption_resolution,[],[f162558,f632]) ).
fof(f162560,plain,
( $false
| spl0_11
| ~ spl0_17
| ~ spl0_7173 ),
inference(forward_subsumption_resolution,[],[f162559,f479]) ).
fof(f162561,plain,
( spl0_11
| ~ spl0_17
| ~ spl0_7173 ),
inference(avatar_contradiction_clause,[],[f162560]) ).
fof(f176192,plain,
( ssList(app(nil,cons(sk5,nil)))
| ssList(sk8)
| ~ spl0_40
| spl0_97 ),
inference(resolution,[],[f111975,f316]) ).
fof(f176193,plain,
( ssList(sk8)
| ~ spl0_40
| spl0_97
| spl0_7173 ),
inference(forward_subsumption_resolution,[],[f176192,f162551]) ).
fof(f176194,plain,
( $false
| ~ spl0_40
| spl0_97
| spl0_3502
| spl0_7173 ),
inference(forward_subsumption_resolution,[],[f176193,f97994]) ).
fof(f176195,plain,
( ~ spl0_40
| spl0_97
| spl0_3502
| spl0_7173 ),
inference(avatar_contradiction_clause,[],[f176194]) ).
fof(f176196,plain,
( ~ ssList(app(app(app(nil,cons(sk5,nil)),sk8),cons(sk10,nil)))
| spl0_40
| ~ spl0_442 ),
inference(forward_demodulation,[],[f1011,f11320]) ).
fof(f176197,plain,
( ~ ssList(app(app(app(nil,cons(sk5,nil)),sk8),sk3))
| ~ spl0_5
| spl0_40
| ~ spl0_442 ),
inference(forward_demodulation,[],[f176196,f445]) ).
fof(f178460,plain,
( ! [X0] :
( segmentP(cons(sk10,skaf82(X0)),sk3)
| ssList(skaf82(X0)) )
| ~ spl0_5
| ~ spl0_9
| spl0_11
| spl0_269 ),
inference(superposition,[],[f30552,f10953]) ).
fof(f178506,plain,
( ! [X0] : segmentP(cons(sk10,skaf82(X0)),sk3)
| ~ spl0_5
| ~ spl0_9
| spl0_11
| spl0_269 ),
inference(forward_subsumption_resolution,[],[f178460,f264]) ).
fof(f187132,plain,
( ! [X0] : cons(X0,nil) = app(nil,cons(X0,nil))
| ~ spl0_17
| ~ spl0_23
| spl0_545 ),
inference(forward_demodulation,[],[f26416,f826]) ).
fof(f197310,definition,
( spl0_8736
<=> ssList(app(sk3,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_8736])],[avatar_definition]) ).
fof(f197311,plain,
( ~ ssList(app(sk3,cons(sk5,nil)))
| spl0_8736 ),
inference(avatar_component_clause,[],[f197310]) ).
fof(f197312,plain,
( ssList(app(sk3,cons(sk5,nil)))
| ~ spl0_8736 ),
inference(avatar_component_clause,[],[f197310]) ).
fof(f273045,plain,
( ssList(sk8)
| ~ spl0_17
| ~ spl0_3501 ),
inference(resolution,[],[f97990,f632]) ).
fof(f273046,plain,
( $false
| ~ spl0_17
| ~ spl0_3501
| spl0_3502 ),
inference(forward_subsumption_resolution,[],[f273045,f97994]) ).
fof(f273047,plain,
( ~ spl0_17
| ~ spl0_3501
| spl0_3502 ),
inference(avatar_contradiction_clause,[],[f273046]) ).
fof(f274223,plain,
( memberP(nil,sk5)
| ssList(sk8)
| ~ spl0_17
| ~ spl0_3500 ),
inference(superposition,[],[f647,f97986]) ).
fof(f274351,plain,
( ssList(sk8)
| ~ spl0_17
| ~ spl0_3500 ),
inference(forward_subsumption_resolution,[],[f274223,f518]) ).
fof(f274388,plain,
( $false
| ~ spl0_17
| ~ spl0_3500
| spl0_3502 ),
inference(forward_subsumption_resolution,[],[f274351,f97994]) ).
fof(f274389,plain,
( ~ spl0_17
| ~ spl0_3500
| spl0_3502 ),
inference(avatar_contradiction_clause,[],[f274388]) ).
fof(f375697,plain,
( ! [X0] :
( frontsegP(sk3,app(sk7,X0))
| ssList(app(sk7,X0))
| ssList(sk7)
| ssList(X0) )
| ~ spl0_3872 ),
inference(resolution,[],[f104586,f1382]) ).
fof(f375725,plain,
( ! [X0] :
( frontsegP(sk3,app(sk7,X0))
| ssList(sk7)
| ssList(X0) )
| ~ spl0_3872 ),
inference(forward_subsumption_resolution,[],[f375697,f316]) ).
fof(f375728,plain,
( ! [X0] :
( frontsegP(sk3,app(sk7,X0))
| ssList(X0) )
| spl0_219
| ~ spl0_3872 ),
inference(forward_subsumption_resolution,[],[f375725,f6611]) ).
fof(f538555,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(sk8)
| spl0_97
| spl0_98
| ~ spl0_3967 ),
inference(resolution,[],[f119402,f1382]) ).
fof(f538565,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ssList(sk8)
| spl0_97
| spl0_98
| ~ spl0_3967 ),
inference(duplicate_literal_removal,[],[f538555]) ).
fof(f538569,plain,
( ~ frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ssList(sk8)
| spl0_97
| spl0_98
| spl0_1674
| ~ spl0_3967 ),
inference(forward_subsumption_resolution,[],[f538565,f75442]) ).
fof(f538571,plain,
( ~ frontsegP(sk3,app(sk7,cons(sk5,nil)))
| spl0_97
| spl0_98
| spl0_1674
| spl0_3502
| ~ spl0_3967 ),
inference(forward_subsumption_resolution,[],[f538569,f97994]) ).
fof(f576650,plain,
( ssList(cons(sk5,nil))
| spl0_97
| spl0_98
| spl0_219
| spl0_1674
| spl0_3502
| ~ spl0_3872
| ~ spl0_3967 ),
inference(resolution,[],[f538571,f375728]) ).
fof(f576664,plain,
( $false
| spl0_97
| spl0_98
| spl0_173
| spl0_219
| spl0_1674
| spl0_3502
| ~ spl0_3872
| ~ spl0_3967 ),
inference(forward_subsumption_resolution,[],[f576650,f4167]) ).
fof(f576665,plain,
( spl0_97
| spl0_98
| spl0_173
| spl0_219
| spl0_1674
| spl0_3502
| ~ spl0_3872
| ~ spl0_3967 ),
inference(avatar_contradiction_clause,[],[f576664]) ).
fof(f576674,plain,
( sk3 = app(app(app(app(nil,cons(sk5,nil)),sk8),cons(sk10,nil)),nil)
| ~ spl0_23
| ~ spl0_27
| ~ spl0_442 ),
inference(forward_demodulation,[],[f942,f11320]) ).
fof(f577276,plain,
( sk3 = app(app(app(app(nil,cons(sk5,nil)),sk8),sk3),nil)
| ~ spl0_5
| ~ spl0_23
| ~ spl0_27
| ~ spl0_442 ),
inference(forward_demodulation,[],[f576674,f445]) ).
fof(f583610,plain,
( ! [X0] :
( frontsegP(X0,sk7)
| frontsegP(sk3,X0)
| ssList(sk7)
| ssList(X0)
| sk3 = sk7 )
| spl0_269
| spl0_612 ),
inference(forward_subsumption_resolution,[],[f54749,f7430]) ).
fof(f585853,plain,
( ! [X0] :
( frontsegP(X0,sk7)
| frontsegP(sk3,X0)
| ssList(X0)
| sk3 = sk7 )
| spl0_219
| spl0_269
| spl0_612 ),
inference(forward_subsumption_resolution,[],[f583610,f6611]) ).
fof(f586663,plain,
( spl0_602
| spl0_3872
| spl0_219
| spl0_269
| spl0_612 ),
inference(avatar_split_clause,[],[f585853,f13456,f7429,f6609,f104585,f13273]) ).
fof(f587549,plain,
( ~ frontsegP(sk3,app(sk3,cons(sk5,nil)))
| spl0_97
| spl0_98
| ~ spl0_602
| spl0_1674
| spl0_3502
| ~ spl0_3967 ),
inference(superposition,[],[f538571,f13274]) ).
fof(f590617,definition,
( spl0_15671
<=> frontsegP(app(sk3,cons(sk5,nil)),sk3) ),
introduced(definition,[new_symbols(definition,[spl0_15671])],[avatar_definition]) ).
fof(f590618,plain,
( ~ frontsegP(app(sk3,cons(sk5,nil)),sk3)
| spl0_15671 ),
inference(avatar_component_clause,[],[f590617]) ).
fof(f590619,plain,
( frontsegP(app(sk3,cons(sk5,nil)),sk3)
| ~ spl0_15671 ),
inference(avatar_component_clause,[],[f590617]) ).
fof(f719418,plain,
( ssList(sk3)
| ssList(cons(sk5,nil))
| ~ spl0_15671 ),
inference(resolution,[],[f590619,f1382]) ).
fof(f719426,plain,
( ssList(cons(sk5,nil))
| spl0_269
| ~ spl0_15671 ),
inference(forward_subsumption_resolution,[],[f719418,f7430]) ).
fof(f719430,plain,
( $false
| spl0_173
| spl0_269
| ~ spl0_15671 ),
inference(forward_subsumption_resolution,[],[f719426,f4167]) ).
fof(f719431,plain,
( spl0_173
| spl0_269
| ~ spl0_15671 ),
inference(avatar_contradiction_clause,[],[f719430]) ).
fof(f719986,plain,
( frontsegP(sk3,app(sk3,cons(sk5,nil)))
| ssList(app(sk3,cons(sk5,nil)))
| ssList(sk3)
| sk3 = app(sk3,cons(sk5,nil))
| spl0_15671 ),
inference(resolution,[],[f590618,f353]) ).
fof(f720007,plain,
( frontsegP(sk3,app(sk3,cons(sk5,nil)))
| ssList(sk3)
| sk3 = app(sk3,cons(sk5,nil))
| spl0_8736
| spl0_15671 ),
inference(forward_subsumption_resolution,[],[f719986,f197311]) ).
fof(f720023,definition,
( spl0_16096
<=> sk3 = app(sk3,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_16096])],[avatar_definition]) ).
fof(f720025,plain,
( sk3 = app(sk3,cons(sk5,nil))
| ~ spl0_16096 ),
inference(avatar_component_clause,[],[f720023]) ).
fof(f720036,definition,
( spl0_16098
<=> frontsegP(sk3,app(sk3,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_16098])],[avatar_definition]) ).
fof(f749936,plain,
( ~ spl0_16098
| spl0_97
| spl0_98
| ~ spl0_602
| spl0_1674
| spl0_3502
| ~ spl0_3967 ),
inference(avatar_split_clause,[],[f587549,f105189,f97992,f75441,f13273,f2561,f2557,f720036]) ).
fof(f749979,plain,
( sk3 != sk3
| ssList(cons(sk5,nil))
| nil = cons(sk5,nil)
| spl0_11
| ~ spl0_16096 ),
inference(superposition,[],[f1978,f720025]) ).
fof(f750034,plain,
( ssList(cons(sk5,nil))
| nil = cons(sk5,nil)
| spl0_11
| ~ spl0_16096 ),
inference(trivial_inequality_removal,[],[f749979]) ).
fof(f750067,plain,
( nil = cons(sk5,nil)
| spl0_11
| spl0_173
| ~ spl0_16096 ),
inference(forward_subsumption_resolution,[],[f750034,f4167]) ).
fof(f750109,plain,
( $false
| spl0_11
| spl0_173
| spl0_182
| ~ spl0_16096 ),
inference(forward_subsumption_resolution,[],[f750067,f4259]) ).
fof(f750110,plain,
( spl0_11
| spl0_173
| spl0_182
| ~ spl0_16096 ),
inference(avatar_contradiction_clause,[],[f750109]) ).
fof(f795399,plain,
( ~ ssList(app(app(cons(sk5,nil),sk8),sk3))
| ~ spl0_5
| ~ spl0_17
| ~ spl0_23
| spl0_40
| ~ spl0_442
| spl0_545 ),
inference(superposition,[],[f176197,f187132]) ).
fof(f795508,plain,
( ~ ssList(app(cons(sk5,sk8),sk3))
| ~ spl0_5
| ~ spl0_17
| ~ spl0_23
| spl0_40
| ~ spl0_442
| spl0_545 ),
inference(forward_demodulation,[],[f795399,f3324]) ).
fof(f799823,definition,
( spl0_17517
<=> ssList(app(cons(sk5,sk8),sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_17517])],[avatar_definition]) ).
fof(f799824,plain,
( ~ ssList(app(cons(sk5,sk8),sk3))
| spl0_17517 ),
inference(avatar_component_clause,[],[f799823]) ).
fof(f853941,definition,
( spl0_18450
<=> sk3 = app(cons(sk5,sk8),sk3) ),
introduced(definition,[new_symbols(definition,[spl0_18450])],[avatar_definition]) ).
fof(f853943,plain,
( sk3 = app(cons(sk5,sk8),sk3)
| ~ spl0_18450 ),
inference(avatar_component_clause,[],[f853941]) ).
fof(f896587,plain,
( ssList(sk3)
| ssList(cons(sk5,nil))
| ~ spl0_8736 ),
inference(resolution,[],[f197312,f316]) ).
fof(f896588,plain,
( ssList(cons(sk5,nil))
| spl0_269
| ~ spl0_8736 ),
inference(forward_subsumption_resolution,[],[f896587,f7430]) ).
fof(f896589,plain,
( $false
| spl0_173
| spl0_269
| ~ spl0_8736 ),
inference(forward_subsumption_resolution,[],[f896588,f4167]) ).
fof(f896590,plain,
( spl0_173
| spl0_269
| ~ spl0_8736 ),
inference(avatar_contradiction_clause,[],[f896589]) ).
fof(f897014,plain,
( frontsegP(sk3,app(sk3,cons(sk5,nil)))
| sk3 = app(sk3,cons(sk5,nil))
| spl0_269
| spl0_8736
| spl0_15671 ),
inference(forward_subsumption_resolution,[],[f720007,f7430]) ).
fof(f897472,plain,
( spl0_16096
| spl0_16098
| spl0_269
| spl0_8736
| spl0_15671 ),
inference(avatar_split_clause,[],[f897014,f590617,f197310,f7429,f720036,f720023]) ).
fof(f899414,plain,
( ~ spl0_17517
| ~ spl0_5
| ~ spl0_17
| ~ spl0_23
| spl0_40
| ~ spl0_442
| spl0_545 ),
inference(avatar_split_clause,[],[f795508,f12610,f11318,f1010,f824,f506,f443,f799823]) ).
fof(f926522,plain,
( sk3 = app(app(app(cons(sk5,nil),sk8),sk3),nil)
| ~ spl0_5
| ~ spl0_17
| ~ spl0_23
| ~ spl0_27
| ~ spl0_442
| spl0_545 ),
inference(forward_demodulation,[],[f577276,f187132]) ).
fof(f926523,plain,
( sk3 = app(app(cons(sk5,sk8),sk3),nil)
| ~ spl0_5
| ~ spl0_17
| ~ spl0_23
| ~ spl0_27
| ~ spl0_442
| spl0_545 ),
inference(forward_demodulation,[],[f926522,f3324]) ).
fof(f926535,plain,
( sk3 != sk3
| ssList(app(cons(sk5,sk8),sk3))
| sk3 = app(cons(sk5,sk8),sk3)
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_23
| ~ spl0_27
| ~ spl0_442
| spl0_545 ),
inference(superposition,[],[f2072,f926523]) ).
fof(f926565,plain,
( ssList(app(cons(sk5,sk8),sk3))
| sk3 = app(cons(sk5,sk8),sk3)
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_23
| ~ spl0_27
| ~ spl0_442
| spl0_545 ),
inference(trivial_inequality_removal,[],[f926535]) ).
fof(f926581,plain,
( sk3 = app(cons(sk5,sk8),sk3)
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_23
| ~ spl0_27
| ~ spl0_442
| spl0_545
| spl0_17517 ),
inference(forward_subsumption_resolution,[],[f926565,f799824]) ).
fof(f926594,plain,
( spl0_18450
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_23
| ~ spl0_27
| ~ spl0_442
| spl0_545
| spl0_17517 ),
inference(avatar_split_clause,[],[f926581,f799823,f12610,f11318,f842,f824,f506,f478,f443,f853941]) ).
fof(f1139648,plain,
( sk3 != sk3
| ssList(cons(sk5,sk8))
| nil = cons(sk5,sk8)
| spl0_11
| ~ spl0_18450 ),
inference(superposition,[],[f2078,f853943]) ).
fof(f1139691,plain,
( ssList(cons(sk5,sk8))
| nil = cons(sk5,sk8)
| spl0_11
| ~ spl0_18450 ),
inference(trivial_inequality_removal,[],[f1139648]) ).
fof(f1139715,plain,
( nil = cons(sk5,sk8)
| spl0_11
| spl0_3501
| ~ spl0_18450 ),
inference(forward_subsumption_resolution,[],[f1139691,f97989]) ).
fof(f1139742,plain,
( $false
| spl0_11
| spl0_3500
| spl0_3501
| ~ spl0_18450 ),
inference(forward_subsumption_resolution,[],[f1139715,f97985]) ).
fof(f1139743,plain,
( spl0_11
| spl0_3500
| spl0_3501
| ~ spl0_18450 ),
inference(avatar_contradiction_clause,[],[f1139742]) ).
fof(f1139784,plain,
( sk9 = cons(skaf83(sk9),skaf82(sk9))
| ~ spl0_17
| spl0_23
| spl0_1670
| spl0_1671 ),
inference(forward_subsumption_resolution,[],[f138464,f74978]) ).
fof(f1139785,plain,
( sk9 = cons(hd(sk9),tl(sk9))
| ~ spl0_17
| spl0_23
| spl0_1670
| spl0_1671 ),
inference(forward_subsumption_resolution,[],[f138465,f74978]) ).
fof(f1140950,plain,
( sk3 != sk9
| ssList(nil)
| spl0_42
| ~ spl0_3969 ),
inference(forward_subsumption_resolution,[],[f120096,f1022]) ).
fof(f1145272,plain,
( spl0_31
| ~ spl0_17
| spl0_23
| spl0_1670
| spl0_1671 ),
inference(avatar_split_clause,[],[f1139784,f74981,f74977,f824,f506,f909]) ).
fof(f1145273,plain,
( spl0_24
| ~ spl0_17
| spl0_23
| spl0_1670
| spl0_1671 ),
inference(avatar_split_clause,[],[f1139785,f74981,f74977,f824,f506,f828]) ).
fof(f1145604,plain,
( sk3 != sk9
| spl0_11
| spl0_42
| ~ spl0_3969 ),
inference(forward_subsumption_resolution,[],[f1140950,f479]) ).
fof(f1148033,plain,
( ~ spl0_597
| spl0_11
| spl0_42
| ~ spl0_3969 ),
inference(avatar_split_clause,[],[f1145604,f105200,f1021,f478,f13237]) ).
fof(f1160660,plain,
( memberP(sk3,hd(sk9))
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ spl0_3173 ),
inference(superposition,[],[f92038,f234]) ).
fof(f1160663,plain,
( memberP(sk3,hd(sk9))
| spl0_43
| ~ spl0_3173 ),
inference(forward_subsumption_resolution,[],[f1160660,f1026]) ).
fof(f1160745,plain,
( sk10 = hd(sk9)
| ~ spl0_5
| spl0_11
| ~ spl0_17
| spl0_43
| ~ spl0_3173 ),
inference(resolution,[],[f1160663,f8404]) ).
fof(f1160912,plain,
( spl0_596
| ~ spl0_5
| spl0_11
| ~ spl0_17
| spl0_43
| ~ spl0_3173 ),
inference(avatar_split_clause,[],[f1160745,f92037,f1025,f506,f478,f443,f13233]) ).
fof(f1161128,plain,
( segmentP(cons(sk10,tl(sk9)),sk3)
| ~ spl0_5
| ~ spl0_9
| spl0_11
| ~ spl0_17
| ~ spl0_31
| spl0_269 ),
inference(superposition,[],[f178506,f26078]) ).
fof(f1280644,plain,
( segmentP(sk9,sk3)
| ~ spl0_5
| ~ spl0_9
| spl0_11
| ~ spl0_17
| ~ spl0_24
| ~ spl0_31
| spl0_269
| ~ spl0_596 ),
inference(forward_demodulation,[],[f1161128,f40792]) ).
fof(f1280645,plain,
( $false
| ~ spl0_5
| ~ spl0_9
| spl0_11
| ~ spl0_17
| ~ spl0_24
| ~ spl0_31
| spl0_269
| ~ spl0_596
| spl0_651 ),
inference(forward_subsumption_resolution,[],[f1280644,f13870]) ).
fof(f1280646,plain,
( ~ spl0_5
| ~ spl0_9
| spl0_11
| ~ spl0_17
| ~ spl0_24
| ~ spl0_31
| spl0_269
| ~ spl0_596
| spl0_651 ),
inference(avatar_contradiction_clause,[],[f1280645]) ).
cnf(s4,plain,
( spl0_1
| spl0_5 ),
inference(sat_conversion,[],[f446]) ).
cnf(s13,plain,
( spl0_1
| spl0_9 ),
inference(sat_conversion,[],[f471]) ).
cnf(s21,plain,
( spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f511]) ).
cnf(s24,plain,
~ spl0_11,
inference(sat_conversion,[],[f514]) ).
cnf(s228,plain,
( spl0_11
| ~ spl0_97 ),
inference(sat_conversion,[],[f4080]) ).
cnf(s351,plain,
~ spl0_100,
inference(sat_conversion,[],[f5244]) ).
cnf(s376,plain,
( spl0_11
| ~ spl0_182 ),
inference(sat_conversion,[],[f5416]) ).
cnf(s420,plain,
~ spl0_219,
inference(sat_conversion,[],[f6666]) ).
cnf(s425,plain,
( spl0_27
| spl0_33
| spl0_219 ),
inference(sat_conversion,[],[f6715]) ).
cnf(s428,plain,
( spl0_27
| ~ spl0_78
| spl0_219 ),
inference(sat_conversion,[],[f6780]) ).
cnf(s448,plain,
( spl0_11
| spl0_97
| ~ spl0_99
| spl0_167 ),
inference(sat_conversion,[],[f7098]) ).
cnf(s455,plain,
( spl0_11
| ~ spl0_167 ),
inference(sat_conversion,[],[f7169]) ).
cnf(s563,plain,
~ spl0_269,
inference(sat_conversion,[],[f7469]) ).
cnf(s583,plain,
( ~ spl0_5
| ~ spl0_9
| spl0_11
| spl0_262 ),
inference(sat_conversion,[],[f7562]) ).
cnf(s677,plain,
( spl0_269
| ~ spl0_330 ),
inference(sat_conversion,[],[f9062]) ).
cnf(s688,plain,
( spl0_269
| ~ spl0_329 ),
inference(sat_conversion,[],[f9397]) ).
cnf(s724,plain,
( ~ spl0_5
| ~ spl0_9
| spl0_11
| spl0_243 ),
inference(sat_conversion,[],[f9775]) ).
cnf(s728,plain,
( ~ spl0_18
| spl0_100
| spl0_101 ),
inference(sat_conversion,[],[f9812]) ).
cnf(s936,plain,
~ spl0_545,
inference(sat_conversion,[],[f12614]) ).
cnf(s1015,plain,
( ~ spl0_33
| ~ spl0_243
| spl0_601
| spl0_608 ),
inference(sat_conversion,[],[f13390]) ).
cnf(s1064,plain,
( spl0_11
| spl0_269
| ~ spl0_542
| spl0_545
| spl0_597
| ~ spl0_651 ),
inference(sat_conversion,[],[f13871]) ).
cnf(s1259,plain,
( ~ spl0_36
| ~ spl0_101
| spl0_613 ),
inference(sat_conversion,[],[f21763]) ).
cnf(s1584,plain,
( spl0_100
| spl0_269
| ~ spl0_613 ),
inference(sat_conversion,[],[f26259]) ).
cnf(s1817,plain,
( ~ spl0_17
| ~ spl0_33
| spl0_78
| ~ spl0_262
| ~ spl0_601
| ~ spl0_612 ),
inference(sat_conversion,[],[f34965]) ).
cnf(s3004,plain,
( spl0_173
| spl0_219
| ~ spl0_1674 ),
inference(sat_conversion,[],[f75481]) ).
cnf(s5630,plain,
( ~ spl0_1
| ~ spl0_173
| spl0_330 ),
inference(sat_conversion,[],[f91755]) ).
cnf(s6416,plain,
( ~ spl0_17
| ~ spl0_31
| spl0_3173 ),
inference(sat_conversion,[],[f94265]) ).
cnf(s7825,plain,
( ~ spl0_1
| spl0_97
| spl0_98
| spl0_99
| spl0_545 ),
inference(sat_conversion,[],[f98733]) ).
cnf(s7837,plain,
~ spl0_3502,
inference(sat_conversion,[],[f98765]) ).
cnf(s9936,plain,
( spl0_1
| spl0_36
| spl0_329
| spl0_330 ),
inference(sat_conversion,[],[f104898]) ).
cnf(s9939,plain,
( spl0_219
| spl0_269
| ~ spl0_608
| spl0_3872 ),
inference(sat_conversion,[],[f104903]) ).
cnf(s10069,plain,
( spl0_43
| spl0_3967 ),
inference(sat_conversion,[],[f105191]) ).
cnf(s10075,plain,
( spl0_43
| spl0_3969 ),
inference(sat_conversion,[],[f105203]) ).
cnf(s10076,plain,
( spl0_43
| spl0_542 ),
inference(sat_conversion,[],[f105204]) ).
cnf(s10656,plain,
( ~ spl0_98
| spl0_1674
| spl0_3502 ),
inference(sat_conversion,[],[f106300]) ).
cnf(s12633,plain,
( spl0_11
| ~ spl0_17
| ~ spl0_173 ),
inference(sat_conversion,[],[f115432]) ).
cnf(s12940,plain,
( ~ spl0_43
| spl0_97
| spl0_98 ),
inference(sat_conversion,[],[f116946]) ).
cnf(s12968,plain,
( spl0_11
| ~ spl0_17
| spl0_43
| spl0_98
| spl0_545
| spl0_3056 ),
inference(sat_conversion,[],[f117039]) ).
cnf(s13209,plain,
( ~ spl0_42
| spl0_97
| spl0_98
| spl0_167 ),
inference(sat_conversion,[],[f119328]) ).
cnf(s13423,plain,
( ~ spl0_5
| spl0_11
| ~ spl0_17
| spl0_442
| ~ spl0_3056 ),
inference(sat_conversion,[],[f119891]) ).
cnf(s15695,plain,
( spl0_1
| spl0_269
| spl0_545
| ~ spl0_4540 ),
inference(sat_conversion,[],[f137409]) ).
cnf(s15698,plain,
( ~ spl0_17
| spl0_545
| ~ spl0_1671 ),
inference(sat_conversion,[],[f137416]) ).
cnf(s15785,plain,
( ~ spl0_5
| ~ spl0_9
| spl0_545
| ~ spl0_1670
| spl0_4540 ),
inference(sat_conversion,[],[f138479]) ).
cnf(s17899,plain,
( spl0_11
| ~ spl0_17
| ~ spl0_7173 ),
inference(sat_conversion,[],[f162561]) ).
cnf(s19852,plain,
( ~ spl0_40
| spl0_97
| spl0_3502
| spl0_7173 ),
inference(sat_conversion,[],[f176195]) ).
cnf(s24763,plain,
( ~ spl0_17
| ~ spl0_3501
| spl0_3502 ),
inference(sat_conversion,[],[f273047]) ).
cnf(s24858,plain,
( ~ spl0_17
| ~ spl0_3500
| spl0_3502 ),
inference(sat_conversion,[],[f274389]) ).
cnf(s34549,plain,
( spl0_97
| spl0_98
| spl0_173
| spl0_219
| spl0_1674
| spl0_3502
| ~ spl0_3872
| ~ spl0_3967 ),
inference(sat_conversion,[],[f576665]) ).
cnf(s36639,plain,
( spl0_219
| spl0_269
| spl0_602
| spl0_612
| spl0_3872 ),
inference(sat_conversion,[],[f586663]) ).
cnf(s37849,plain,
( spl0_173
| spl0_269
| ~ spl0_15671 ),
inference(sat_conversion,[],[f719431]) ).
cnf(s38234,plain,
( spl0_97
| spl0_98
| ~ spl0_602
| spl0_1674
| spl0_3502
| ~ spl0_3967
| ~ spl0_16098 ),
inference(sat_conversion,[],[f749936]) ).
cnf(s38235,plain,
( spl0_11
| spl0_173
| spl0_182
| ~ spl0_16096 ),
inference(sat_conversion,[],[f750110]) ).
cnf(s44593,plain,
( spl0_173
| spl0_269
| ~ spl0_8736 ),
inference(sat_conversion,[],[f896590]) ).
cnf(s44691,plain,
( spl0_269
| spl0_8736
| spl0_15671
| spl0_16096
| spl0_16098 ),
inference(sat_conversion,[],[f897472]) ).
cnf(s44870,plain,
( ~ spl0_5
| ~ spl0_17
| ~ spl0_23
| spl0_40
| ~ spl0_442
| spl0_545
| ~ spl0_17517 ),
inference(sat_conversion,[],[f899414]) ).
cnf(s45256,plain,
( ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_23
| ~ spl0_27
| ~ spl0_442
| spl0_545
| spl0_17517
| spl0_18450 ),
inference(sat_conversion,[],[f926594]) ).
cnf(s49527,plain,
( spl0_11
| spl0_3500
| spl0_3501
| ~ spl0_18450 ),
inference(sat_conversion,[],[f1139743]) ).
cnf(s50822,plain,
( ~ spl0_17
| spl0_23
| spl0_31
| spl0_1670
| spl0_1671 ),
inference(sat_conversion,[],[f1145272]) ).
cnf(s50823,plain,
( ~ spl0_17
| spl0_23
| spl0_24
| spl0_1670
| spl0_1671 ),
inference(sat_conversion,[],[f1145273]) ).
cnf(s51137,plain,
( spl0_11
| spl0_42
| ~ spl0_597
| ~ spl0_3969 ),
inference(sat_conversion,[],[f1148033]) ).
cnf(s52020,plain,
( ~ spl0_5
| spl0_11
| ~ spl0_17
| spl0_43
| spl0_596
| ~ spl0_3173 ),
inference(sat_conversion,[],[f1160912]) ).
cnf(s55109,plain,
( ~ spl0_5
| ~ spl0_9
| spl0_11
| ~ spl0_17
| ~ spl0_24
| ~ spl0_31
| spl0_269
| ~ spl0_596
| spl0_651 ),
inference(sat_conversion,[],[f1280646]) ).
cnf(s55178,plain,
~ spl0_329,
inference(rat,[],[s688,s563]) ).
cnf(s55179,plain,
~ spl0_330,
inference(rat,[],[s677,s563]) ).
cnf(s55259,plain,
~ spl0_613,
inference(rat,[],[s1584,s563,s351]) ).
cnf(s55281,plain,
~ spl0_167,
inference(rat,[],[s455,s24]) ).
cnf(s55282,plain,
~ spl0_182,
inference(rat,[],[s376,s24]) ).
cnf(s55283,plain,
~ spl0_97,
inference(rat,[],[s228,s24]) ).
cnf(s55285,plain,
~ spl0_99,
inference(rat,[],[s448,s55281,s24,s55283]) ).
cnf(s55300,plain,
( spl0_23
| spl0_1 ),
inference(rat,[],[s52020,s55109,s6416,s50822,s50823,s15785,s4,s13,s15695,s15698,s1064,s51137,s10075,s13209,s10076,s12940,s10656,s3004,s12633,s21,s728,s1259,s9936,s24,s563,s55283,s7837,s420,s351,s55259,s55179,s55178,s936,s55281]) ).
cnf(s55301,plain,
spl0_1,
inference(rat,[],[s1817,s1015,s425,s428,s45256,s44870,s55300,s9939,s36639,s13423,s34549,s38234,s12968,s10069,s12940,s10656,s44691,s3004,s37849,s38235,s44593,s19852,s49527,s12633,s17899,s24763,s24858,s21,s728,s583,s724,s1259,s4,s13,s9936,s420,s24,s936,s563,s55283,s7837,s55282,s351,s55259,s55178,s55179]) ).
cnf(s55303,plain,
spl0_98,
inference(rat,[],[s7825,s936,s55285,s55283,s55301]) ).
cnf(s55305,plain,
~ spl0_173,
inference(rat,[],[s5630,s55179,s55301]) ).
cnf(s55308,plain,
spl0_1674,
inference(rat,[],[s10656,s7837,s55303]) ).
cnf(s55314,plain,
$false,
inference(rat,[],[s3004,s420,s55308,s55305]) ).
fof(f1280647,plain,
$false,
inference(avatar_sat_refutation,[],[s55314]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC299-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n003.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 08:59:43 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 Running first-order model finding
% 0.09/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.74/2.31 % (1444331)Will run a generic schedule for satisfiability detection.
% 14.74/2.31 % (1444337)% WARNING: option uhcvi not known.
% 14.74/2.31 % (1444337)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3756320852:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.74/2.31 % (1444336)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2877910251_2999 on theBenchmark for (2999ds/0Mi)
% 14.74/2.31 % (1444338)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=860387604:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.74/2.31 % (1444339)dis+10_1_sil=32000:sp=arity:random_seed=794160051:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.74/2.31 % (1444340)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=148422330:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.74/2.31 % (1444342)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1158605371:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.74/2.31 % (1444341)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1261522382:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.74/2.31 % TRYING [1]
% 14.74/2.31 % TRYING [2]
% 14.74/2.31 % TRYING [3]
% 14.74/2.31 % TRYING [4]
% 14.74/2.31 % (1444339)Instruction limit reached!
% 14.74/2.31 % (1444339)------------------------------
% 14.74/2.31 % (1444339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.74/2.31 % (1444339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.74/2.31 % (1444339)CaDiCaL version: 2.1.3
% 14.74/2.31 % (1444339)Termination reason: Instruction limit
% 14.74/2.31 % (1444339)Termination phase: Saturation
% 14.74/2.31 % (1444339)Time elapsed: 0.058 s
% 14.74/2.31 % (1444339)Peak memory usage: 13 MB
% 14.74/2.31 % (1444339)Instructions burned: 104 (million)
% 14.74/2.31 % (1444340)Instruction limit reached!
% 14.74/2.31 % (1444340)------------------------------
% 14.74/2.31 % (1444340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.74/2.31 % (1444340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.74/2.31 % (1444340)CaDiCaL version: 2.1.3
% 14.74/2.31 % (1444340)Termination reason: Instruction limit
% 14.74/2.31 % (1444340)Termination phase: Saturation
% 14.74/2.31 % (1444340)Time elapsed: 0.059 s
% 14.74/2.31 % (1444340)Peak memory usage: 13 MB
% 14.74/2.31 % (1444340)Instructions burned: 118 (million)
% 14.74/2.31 % (1444341)Instruction limit reached!
% 14.74/2.31 % (1444341)------------------------------
% 14.74/2.31 % (1444341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.74/2.31 % (1444341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.74/2.31 % (1444341)CaDiCaL version: 2.1.3
% 14.74/2.31 % (1444341)Termination reason: Instruction limit
% 14.74/2.31 % (1444341)Termination phase: Saturation
% 14.74/2.31 % (1444341)Time elapsed: 0.065 s
% 14.74/2.31 % (1444341)Peak memory usage: 14 MB
% 14.74/2.31 % (1444341)Instructions burned: 132 (million)
% 14.74/2.31 % (1444350)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3842165122:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 14.74/2.31 % (1444351)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2325481638:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.74/2.31 % (1444352)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=3901727348:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.74/2.31 % (1444342)Instruction limit reached!
% 14.74/2.31 % (1444342)------------------------------
% 14.74/2.31 % (1444342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.74/2.31 % (1444342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.74/2.31 % (1444342)CaDiCaL version: 2.1.3
% 14.74/2.31 % (1444342)Termination reason: Instruction limit
% 14.74/2.31 % (1444342)Termination phase: Saturation
% 14.74/2.31 % (1444342)Time elapsed: 0.089 s
% 14.74/2.31 % (1444342)Peak memory usage: 14 MB
% 14.74/2.31 % (1444342)Instructions burned: 159 (million)
% 14.74/2.31 % TRYING [1]
% 14.74/2.31 % TRYING [2]
% 14.74/2.31 % TRYING [3]
% 14.74/2.31 % TRYING [5]
% 14.74/2.31 % (1444356)ott-21_1_sil=16000:fs=off:random_seed=4247802821:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.74/2.31 % TRYING [4]
% 14.74/2.31 % (1444351)Instruction limit reached!
% 14.74/2.31 % (1444351)------------------------------
% 14.74/2.31 % (1444351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.66/6.82 % (1444351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.66/6.82 % (1444351)CaDiCaL version: 2.1.3
% 46.66/6.82 % (1444351)Termination reason: Instruction limit
% 46.66/6.82 % (1444351)Termination phase: Saturation
% 46.66/6.82 % (1444351)Time elapsed: 0.070 s
% 46.66/6.82 % (1444351)Peak memory usage: 13 MB
% 46.66/6.82 % (1444351)Instructions burned: 133 (million)
% 46.66/6.82 % (1444358)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3810687402:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 46.66/6.82 % TRYING [5]
% 46.66/6.82 % (1444356)Instruction limit reached!
% 46.66/6.82 % (1444356)------------------------------
% 46.66/6.82 % (1444356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.66/6.82 % (1444356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.66/6.82 % (1444356)CaDiCaL version: 2.1.3
% 46.66/6.82 % (1444356)Termination reason: Instruction limit
% 46.66/6.82 % (1444356)Termination phase: Saturation
% 46.66/6.82 % (1444356)Time elapsed: 0.089 s
% 46.66/6.82 % (1444356)Peak memory usage: 13 MB
% 46.66/6.82 % (1444356)Instructions burned: 180 (million)
% 46.66/6.82 % (1444360)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=775394035:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 46.66/6.82 % TRYING [1]
% 46.66/6.82 % TRYING [2]
% 46.66/6.82 % TRYING [3]
% 46.66/6.82 % TRYING [6]
% 46.66/6.82 % TRYING [4]
% 46.66/6.82 % TRYING [6]
% 46.66/6.82 % (1444350)Instruction limit reached!
% 46.66/6.82 % (1444350)------------------------------
% 46.66/6.82 % (1444350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.66/6.82 % (1444350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.66/6.82 % (1444350)CaDiCaL version: 2.1.3
% 46.66/6.82 % (1444350)Termination reason: Instruction limit
% 46.66/6.82 % (1444350)Termination phase: Finite model building constraint generation
% 46.66/6.82 % (1444350)Time elapsed: 0.272 s
% 46.66/6.82 % (1444350)Peak memory usage: 35 MB
% 46.66/6.82 % (1444350)Instructions burned: 716 (million)
% 46.66/6.82 % (1444362)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=160568910:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 46.66/6.82 % TRYING [5]
% 46.66/6.82 % (1444352)Instruction limit reached!
% 46.66/6.82 % (1444352)------------------------------
% 46.66/6.82 % (1444352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.66/6.82 % (1444352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.66/6.82 % (1444352)CaDiCaL version: 2.1.3
% 46.66/6.82 % (1444352)Termination reason: Instruction limit
% 46.66/6.82 % (1444352)Termination phase: Saturation
% 46.66/6.82 % (1444352)Time elapsed: 0.388 s
% 46.66/6.82 % (1444352)Peak memory usage: 21 MB
% 46.66/6.82 % (1444352)Instructions burned: 685 (million)
% 46.66/6.82 % (1444358)Instruction limit reached!
% 46.66/6.82 % (1444358)------------------------------
% 46.66/6.82 % (1444358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.66/6.82 % (1444358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.66/6.82 % (1444358)CaDiCaL version: 2.1.3
% 46.66/6.82 % (1444358)Termination reason: Instruction limit
% 46.66/6.82 % (1444358)Termination phase: Saturation
% 46.66/6.82 % (1444358)Time elapsed: 0.317 s
% 46.66/6.82 % (1444358)Peak memory usage: 14 MB
% 46.66/6.82 % (1444358)Instructions burned: 478 (million)
% 46.66/6.82 % (1444364)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2822283693:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 46.66/6.82 % (1444365)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=636110394: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)
% 46.66/6.82 % (1444360)Instruction limit reached!
% 46.66/6.82 % (1444360)------------------------------
% 46.66/6.82 % (1444360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.66/6.82 % (1444360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.66/6.82 % (1444360)CaDiCaL version: 2.1.3
% 46.66/6.82 % (1444360)Termination reason: Instruction limit
% 46.66/6.82 % (1444360)Termination phase: Finite model building SAT solving
% 46.66/6.82 % (1444360)Time elapsed: 0.335 s
% 46.66/6.82 % (1444360)Peak memory usage: 23 MB
% 46.66/6.82 % (1444360)Instructions burned: 866 (million)
% 46.66/6.82 % (1444368)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1099215389:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 46.66/6.82 % TRYING [14]
% 46.66/6.82 % TRYING [7]
% 46.66/6.82 % (1444364)Instruction limit reached!
% 94.19/13.50 % (1444364)------------------------------
% 94.19/13.50 % (1444364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.19/13.50 % (1444364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.19/13.50 % (1444364)CaDiCaL version: 2.1.3
% 94.19/13.50 % (1444364)Termination reason: Instruction limit
% 94.19/13.50 % (1444364)Termination phase: Finite model building constraint generation
% 94.19/13.50 % (1444364)Time elapsed: 0.326 s
% 94.19/13.50 % (1444364)Peak memory usage: 73 MB
% 94.19/13.50 % (1444364)Instructions burned: 892 (million)
% 94.19/13.50 % (1444370)fmb+10_1_sil=64000:random_seed=1073555941:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 94.19/13.50 % TRYING [1]
% 94.19/13.50 % TRYING [2]
% 94.19/13.50 % TRYING [3]
% 94.19/13.50 % (1444365)Instruction limit reached!
% 94.19/13.50 % (1444365)------------------------------
% 94.19/13.50 % (1444365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.19/13.50 % (1444365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.19/13.50 % (1444365)CaDiCaL version: 2.1.3
% 94.19/13.50 % (1444365)Termination reason: Instruction limit
% 94.19/13.50 % (1444365)Termination phase: Saturation
% 94.19/13.50 % (1444365)Time elapsed: 0.376 s
% 94.19/13.50 % (1444365)Peak memory usage: 19 MB
% 94.19/13.50 % (1444365)Instructions burned: 692 (million)
% 94.19/13.50 % (1444372)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1298285107:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 94.19/13.50 % TRYING [20]
% 94.19/13.50 % TRYING [4]
% 94.19/13.50 % (1444362)Instruction limit reached!
% 94.19/13.50 % (1444362)------------------------------
% 94.19/13.50 % (1444362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.19/13.50 % (1444362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.19/13.50 % (1444362)CaDiCaL version: 2.1.3
% 94.19/13.50 % (1444362)Termination reason: Instruction limit
% 94.19/13.50 % (1444362)Termination phase: Saturation
% 94.19/13.50 % (1444362)Time elapsed: 0.642 s
% 94.19/13.50 % (1444362)Peak memory usage: 25 MB
% 94.19/13.50 % (1444362)Instructions burned: 1179 (million)
% 94.19/13.50 % (1444368)Instruction limit reached!
% 94.19/13.50 % (1444368)------------------------------
% 94.19/13.50 % (1444368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.19/13.50 % (1444368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.19/13.50 % (1444368)CaDiCaL version: 2.1.3
% 94.19/13.50 % (1444368)Termination reason: Instruction limit
% 94.19/13.50 % (1444368)Termination phase: Saturation
% 94.19/13.50 % (1444368)Time elapsed: 0.455 s
% 94.19/13.50 % (1444368)Peak memory usage: 20 MB
% 94.19/13.50 % (1444368)Instructions burned: 880 (million)
% 94.19/13.50 % (1444374)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1343222955:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 94.19/13.50 % TRYING [8]
% 94.19/13.50 % (1444375)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3523634997:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 94.19/13.50 % TRYING [5]
% 94.19/13.50 % (1444374)Instruction limit reached!
% 94.19/13.50 % (1444374)------------------------------
% 94.19/13.50 % (1444374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.19/13.50 % (1444374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.19/13.50 % (1444374)CaDiCaL version: 2.1.3
% 94.19/13.50 % (1444374)Termination reason: Instruction limit
% 94.19/13.50 % (1444374)Termination phase: Finite model building constraint generation
% 94.19/13.50 % (1444374)Time elapsed: 0.330 s
% 94.19/13.50 % (1444374)Peak memory usage: 79 MB
% 94.19/13.50 % (1444374)Instructions burned: 920 (million)
% 94.19/13.50 % (1444378)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=528608216:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 94.19/13.50 % TRYING [6]
% 94.19/13.50 % TRYING [8]
% 94.19/13.50 % (1444378)Instruction limit reached!
% 94.19/13.50 % (1444378)------------------------------
% 94.19/13.50 % (1444378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.19/13.50 % (1444378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.19/13.50 % (1444378)CaDiCaL version: 2.1.3
% 94.19/13.50 % (1444378)Termination reason: Instruction limit
% 94.19/13.50 % (1444378)Termination phase: Saturation
% 94.19/13.50 % (1444378)Time elapsed: 0.638 s
% 94.19/13.50 % (1444378)Peak memory usage: 15 MB
% 94.19/13.50 % (1444378)Instructions burned: 1474 (million)
% 94.19/13.50 % (1444380)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3543861257:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 59.60/21.67 % TRYING [77]
% 59.60/21.67 % TRYING [7]
% 59.60/21.67 % (1444375)Instruction limit reached!
% 59.60/21.67 % (1444375)------------------------------
% 59.60/21.67 % (1444375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.60/21.67 % (1444375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.60/21.67 % (1444375)CaDiCaL version: 2.1.3
% 59.60/21.67 % (1444375)Termination reason: Instruction limit
% 59.60/21.67 % (1444375)Termination phase: Saturation
% 59.60/21.67 % (1444375)Time elapsed: 2.605 s
% 59.60/21.67 % (1444375)Peak memory usage: 48 MB
% 59.60/21.67 % (1444375)Instructions burned: 5133 (million)
% 59.60/21.67 % (1444382)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2085777179:fmbsr=2.30978:i=2174_2962 on theBenchmark for (2962ds/2174Mi)
% 59.60/21.67 % TRYING [9]
% 59.60/21.67 % TRYING [16]
% 59.60/21.67 % (1444372)Instruction limit reached!
% 59.60/21.67 % (1444372)------------------------------
% 59.60/21.67 % (1444372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.60/21.67 % (1444372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.60/21.67 % (1444372)CaDiCaL version: 2.1.3
% 59.60/21.67 % (1444372)Termination reason: Instruction limit
% 59.60/21.67 % (1444372)Termination phase: Finite model building constraint generation
% 59.60/21.67 % (1444372)Time elapsed: 3.245 s
% 59.60/21.67 % (1444372)Peak memory usage: 589 MB
% 59.60/21.67 % (1444372)Instructions burned: 9515 (million)
% 59.60/21.67 % (1444384)ott-2_1_sil=16000:newcnf=on:random_seed=938976816:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 59.60/21.67 % TRYING [8]
% 59.60/21.67 % (1444380)Instruction limit reached!
% 59.60/21.67 % (1444380)------------------------------
% 59.60/21.67 % (1444380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.60/21.67 % (1444380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.60/21.67 % (1444380)CaDiCaL version: 2.1.3
% 59.60/21.67 % (1444380)Termination reason: Instruction limit
% 59.60/21.67 % (1444380)Termination phase: Finite model building constraint generation
% 59.60/21.67 % (1444380)Time elapsed: 2.249 s
% 59.60/21.67 % (1444380)Peak memory usage: 439 MB
% 59.60/21.67 % (1444380)Instructions burned: 6326 (million)
% 59.60/21.67 % (1444386)ott+10_1_sil=32000:tgt=ground:random_seed=2219355932:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 59.60/21.67 % (1444382)Instruction limit reached!
% 59.60/21.67 % (1444382)------------------------------
% 59.60/21.67 % (1444382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.60/21.67 % (1444382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.60/21.67 % (1444382)CaDiCaL version: 2.1.3
% 59.60/21.67 % (1444382)Termination reason: Instruction limit
% 59.60/21.67 % (1444382)Termination phase: Finite model building constraint generation
% 59.60/21.67 % (1444382)Time elapsed: 0.756 s
% 59.60/21.67 % (1444382)Peak memory usage: 138 MB
% 59.60/21.67 % (1444382)Instructions burned: 2174 (million)
% 59.60/21.67 % (1444388)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3278989931:i=54282_2955 on theBenchmark for (2955ds/54282Mi)
% 59.60/21.67 % TRYING [1]
% 59.60/21.67 % TRYING [2]
% 59.60/21.67 % TRYING [3]
% 59.60/21.67 % TRYING [4]
% 59.60/21.67 % TRYING [5]
% 59.60/21.67 % (1444384)Instruction limit reached!
% 59.60/21.67 % (1444384)------------------------------
% 59.60/21.67 % (1444384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.60/21.67 % (1444384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.60/21.67 % (1444384)CaDiCaL version: 2.1.3
% 59.60/21.67 % (1444384)Termination reason: Instruction limit
% 59.60/21.67 % (1444384)Termination phase: Saturation
% 59.60/21.67 % (1444384)Time elapsed: 0.449 s
% 59.60/21.67 % (1444384)Peak memory usage: 20 MB
% 59.60/21.67 % (1444384)Instructions burned: 870 (million)
% 59.60/21.67 % (1444390)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3307781948:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi)
% 59.60/21.67 % TRYING [6]
% 59.60/21.67 % TRYING [7]
% 59.60/21.67 % TRYING [8]
% 59.60/21.67 % (1444390)Instruction limit reached!
% 59.60/21.67 % (1444390)------------------------------
% 59.60/21.67 % (1444390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.60/21.67 % (1444390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.60/21.67 % (1444390)CaDiCaL version: 2.1.3
% 59.60/21.67 % (1444390)Termination reason: Instruction limit
% 59.60/21.67 % (1444390)Termination phase: Saturation
% 59.60/21.67 % (1444390)Time elapsed: 1.850 s
% 59.60/21.67 % (1444390)Peak memory usage: 41 MB
% 59.60/21.67 % (1444390)Instructions burned: 3512 (million)
% 59.60/21.67 % (1444392)dis+21_1_sil=32000:sas=cadical:random_seed=1926935083:i=3773:amm=off_2933 on theBenchmark for (2933ds/3773Mi)
% 59.60/21.67 % (1444386)Instruction limit reached!
% 59.60/21.67 % (1444386)------------------------------
% 59.60/21.67 % (1444386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.60/21.67 % (1444386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.60/21.67 % (1444386)CaDiCaL version: 2.1.3
% 59.60/21.67 % (1444386)Termination reason: Instruction limit
% 59.60/21.67 % (1444386)Termination phase: Saturation
% 59.60/21.67 % (1444386)Time elapsed: 2.756 s
% 59.60/21.67 % (1444386)Peak memory usage: 68 MB
% 59.60/21.67 % (1444386)Instructions burned: 5115 (million)
% 59.60/21.67 % (1444394)ott+11_1_sil=16000:gs=on:random_seed=2569252950:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2928 on theBenchmark for (2928ds/2251Mi)
% 59.60/21.67 % TRYING [10]
% 59.60/21.67 % TRYING [9]
% 59.60/21.67 % (1444394)Instruction limit reached!
% 59.60/21.67 % (1444394)------------------------------
% 59.60/21.67 % (1444394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.60/21.67 % (1444394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.60/21.67 % (1444394)CaDiCaL version: 2.1.3
% 59.60/21.67 % (1444394)Termination reason: Instruction limit
% 59.60/21.67 % (1444394)Termination phase: Saturation
% 59.60/21.67 % (1444394)Time elapsed: 0.997 s
% 59.60/21.67 % (1444394)Peak memory usage: 16 MB
% 59.60/21.67 % (1444394)Instructions burned: 2253 (million)
% 59.60/21.67 % (1444396)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3775462922:fmbsr=1.6:i=67534_2917 on theBenchmark for (2917ds/67534Mi)
% 59.60/21.67 % TRYING [7]
% 59.60/21.67 % TRYING [9]
% 59.60/21.67 % (1444392)Instruction limit reached!
% 59.60/21.67 % (1444392)------------------------------
% 59.60/21.67 % (1444392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.60/21.67 % (1444392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.60/21.67 % (1444392)CaDiCaL version: 2.1.3
% 59.60/21.67 % (1444392)Termination reason: Instruction limit
% 59.60/21.67 % (1444392)Termination phase: Saturation
% 59.60/21.67 % (1444392)Time elapsed: 2.031 s
% 59.60/21.67 % (1444392)Peak memory usage: 44 MB
% 59.60/21.67 % (1444392)Instructions burned: 3774 (million)
% 59.60/21.67 % (1444398)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1649694788:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2913 on theBenchmark for (2913ds/4591Mi)
% 59.60/21.67 % (1444370)Instruction limit reached!
% 59.60/21.67 % (1444370)------------------------------
% 59.60/21.67 % (1444370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.60/21.67 % (1444370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.60/21.67 % (1444370)CaDiCaL version: 2.1.3
% 59.60/21.67 % (1444370)Termination reason: Instruction limit
% 59.60/21.67 % (1444370)Termination phase: Finite model building constraint generation
% 59.60/21.67 % (1444370)Time elapsed: 8.461 s
% 59.60/21.67 % (1444370)Peak memory usage: 235 MB
% 59.60/21.67 % (1444370)Instructions burned: 22062 (million)
% 59.60/21.67 % (1444400)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1638158315:i=29340_2906 on theBenchmark for (2906ds/29340Mi)
% 59.60/21.67 % TRYING [8]
% 59.60/21.67 % (1444398)Instruction limit reached!
% 59.60/21.67 % (1444398)------------------------------
% 59.60/21.67 % (1444398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.60/21.67 % (1444398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.60/21.67 % (1444398)CaDiCaL version: 2.1.3
% 59.60/21.67 % (1444398)Termination reason: Instruction limit
% 59.60/21.67 % (1444398)Termination phase: Saturation
% 59.60/21.67 % (1444398)Time elapsed: 2.054 s
% 59.60/21.67 % (1444398)Peak memory usage: 53 MB
% 59.60/21.67 % (1444398)Instructions burned: 4593 (million)
% 59.60/21.67 % (1444402)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=530166102:i=5211_2892 on theBenchmark for (2892ds/5211Mi)
% 59.60/21.67 % TRYING [10]
% 59.60/21.67 % (1444402)Instruction limit reached!
% 59.60/21.67 % (1444402)------------------------------
% 59.60/21.67 % (1444402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.60/21.67 % (1444402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.60/21.67 % (1444402)CaDiCaL version: 2.1.3
% 59.60/21.67 % (1444402)Termination reason: Instruction limit
% 59.60/21.67 % (1444402)Termination phase: Saturation
% 59.60/21.67 % (1444402)Time elapsed: 2.504 s
% 59.60/21.67 % (1444402)Peak memory usage: 49 MB
% 59.60/21.67 % (1444402)Instructions burned: 5211 (million)
% 59.60/21.67 % (1444404)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2894205159:i=5497:nm=2_2867 on theBenchmark for (2867ds/5497Mi)
% 59.60/21.67 % TRYING [17]
% 59.60/21.67 % TRYING [9]
% 59.60/21.67 % (1444404)Instruction limit reached!
% 59.60/21.67 % (1444404)------------------------------
% 59.60/21.67 % (1444404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.60/21.67 % (1444404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.60/21.67 % (1444404)CaDiCaL version: 2.1.3
% 59.60/21.67 % (1444404)Termination reason: Instruction limit
% 59.60/21.67 % (1444404)Termination phase: Finite model building constraint generation
% 59.60/21.67 % (1444404)Time elapsed: 1.856 s
% 59.60/21.67 % (1444404)Peak memory usage: 344 MB
% 59.60/21.67 % (1444404)Instructions burned: 5497 (million)
% 59.60/21.67 % (1444445)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2588997916:fmbsr=2:i=46332_2847 on theBenchmark for (2847ds/46332Mi)
% 59.60/21.67 % TRYING [15]
% 59.60/21.67 % (1444337) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1444331-1444337"...
% 59.60/21.67 % (1444337)...printing done.
% 59.60/21.67 % (1444337)Refutation found. Thanks to Tanya!
% 59.60/21.67 % SZS status Unsatisfiable for theBenchmark
% 59.60/21.67 % SZS output start Proof for theBenchmark
% See solution above
% 59.60/21.68 % (1444337)------------------------------
% 59.60/21.68 % (1444337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.60/21.68 % (1444337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.60/21.68 % (1444337)CaDiCaL version: 2.1.3
% 59.60/21.68 % (1444337)Termination reason: Refutation
% 59.60/21.68 % (1444337)Time elapsed: 21.231 s
% 59.60/21.68 % (1444337)Peak memory usage: 512 MB
% 59.60/21.68 % (1444337)Instructions burned: 70795 (million)
% 59.60/21.68 % (1444331)Success in time 21.466 s
% 59.60/21.68 % Vampire exiting
%------------------------------------------------------------------------------