%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC177-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 : n002.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:04:58 PM UTC 2026
% Result : Unsatisfiable 11.22s 4.38s
% Output : Refutation 11.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 69
% Syntax : Number of formulae : 360 ( 59 unt; 27 def)
% Number of atoms : 1172 ( 174 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 1293 ( 481 ~; 785 |; 0 &)
% ( 27 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 39 ( 37 usr; 28 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 8 con; 0-2 aty)
% Number of variables : 224 ( 0 sgn 224 !; 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(f13,axiom,
! [X0] : ssList(skaf82(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause13) ).
fof(f50,axiom,
! [X0,X1] : ssList(skaf46(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause50) ).
fof(f59,axiom,
! [X0] :
( ~ ssList(X0)
| rearsegP(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause59) ).
fof(f62,axiom,
! [X0] :
( ~ ssItem(X0)
| leq(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause62) ).
fof(f70,axiom,
! [X0] :
( ~ ssItem(X0)
| cyclefreeP(cons(X0,nil)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause70) ).
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(f80,axiom,
! [X0] :
( ~ segmentP(nil,X0)
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause80) ).
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(f104,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssItem(X1)
| neq(X1,X0)
| X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause102) ).
fof(f105,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssItem(X1)
| neq(X1,X0)
| X0 = X1 ),
inference(reorient_equations,[],[f104]) ).
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(f121,axiom,
! [X0,X1] :
( app(X0,X1) != nil
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause118) ).
fof(f122,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X0 ),
inference(reorient_equations,[],[f121]) ).
fof(f123,axiom,
! [X0,X1] :
( app(X0,X1) != nil
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause119) ).
fof(f124,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X1 ),
inference(reorient_equations,[],[f123]) ).
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(f142,axiom,
! [X0,X1] :
( ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| app(skaf46(X0,X1),X1) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause131) ).
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(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(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(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(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(f199,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ leq(X0,X1)
| ~ leq(X1,X0)
| app(app(X2,cons(X0,X3)),cons(X1,X4)) != X5
| ~ ssList(X4)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0)
| ~ cyclefreeP(X5)
| ~ ssList(X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause185) ).
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,
app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_11) ).
fof(f211,plain,
sk1 = app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8),
inference(reorient_equations,[],[f210]) ).
fof(f212,negated_conjecture,
~ neq(sk5,sk6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_12) ).
fof(f214,negated_conjecture,
( ssItem(sk9)
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_14) ).
fof(f218,negated_conjecture,
( cons(sk9,nil) = sk3
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_17) ).
fof(f219,plain,
( sk3 = cons(sk9,nil)
| nil = sk3 ),
inference(reorient_equations,[],[f218]) ).
fof(f221,plain,
ssList(sk3),
inference(definition_unfolding,[],[f200,f205]) ).
fof(f223,plain,
sk3 = app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8),
inference(definition_unfolding,[],[f211,f205]) ).
fof(f231,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(cons(X0,nil))
| singletonP(cons(X0,nil)) ),
inference(equality_resolution,[],[f119]) ).
fof(f234,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(X0,X1))
| rearsegP(app(X0,X1),X1) ),
inference(equality_resolution,[],[f154]) ).
fof(f238,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(f239,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(f241,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(f247,plain,
! [X2,X3,X0,X1,X4] :
( ~ leq(X0,X1)
| ~ leq(X1,X0)
| ~ ssList(X4)
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0)
| ~ cyclefreeP(app(app(X2,cons(X0,X3)),cons(X1,X4)))
| ~ ssList(app(app(X2,cons(X0,X3)),cons(X1,X4))) ),
inference(equality_resolution,[],[f199]) ).
fof(f251,plain,
~ ssList(nil),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f255,plain,
! [X0] : ~ ssList(skaf82(X0)),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f292,plain,
! [X0,X1] : ~ ssList(skaf46(X0,X1)),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f300,plain,
! [X0] :
( ~ rearsegP(X0,X0)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f59]) ).
fof(f303,plain,
! [X0] :
( ~ leq(X0,X0)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f62]) ).
fof(f311,plain,
! [X0] :
( cyclefreeP(cons(X0,nil))
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f70]) ).
fof(f312,plain,
! [X0] :
( memberP(nil,X0)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f71]) ).
fof(f313,plain,
! [X0,X1] :
( ssList(X0)
| duplicatefreeP(X0)
| ~ ssItem(X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f314,plain,
! [X0] :
( ssList(X0)
| app(X0,nil) = X0 ),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f315,plain,
! [X0] :
( ssList(X0)
| app(nil,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f316,plain,
! [X0] :
( ~ ssList(tl(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f321,plain,
! [X0] :
( segmentP(nil,X0)
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f326,plain,
! [X0,X1] :
( ~ ssList(app(X1,X0))
| ssList(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f327,plain,
! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f337,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| tl(cons(X0,X1)) = X1 ),
inference(consistent_polarity_flipping,[],[f96]) ).
fof(f343,plain,
! [X0,X1] :
( neq(X1,X0)
| ssItem(X1)
| ssItem(X0)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f105]) ).
fof(f345,plain,
! [X0] :
( ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f350,plain,
! [X0] :
( ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f357,plain,
! [X0] :
( singletonP(cons(X0,nil))
| ssList(cons(X0,nil))
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f231]) ).
fof(f359,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ssList(X1)
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f122]) ).
fof(f360,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ssList(X1)
| ssList(X0)
| nil = X1 ),
inference(consistent_polarity_flipping,[],[f124]) ).
fof(f361,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f368,plain,
! [X0,X1] :
( segmentP(X0,X1)
| segmentP(X1,X0)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f372,plain,
! [X0,X1] :
( rearsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| app(skaf46(X0,X1),X1) = X0 ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f384,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X0,X1))
| ~ rearsegP(app(X0,X1),X1) ),
inference(consistent_polarity_flipping,[],[f234]) ).
fof(f392,plain,
! [X2,X0,X1] :
( app(X0,X1) != app(X2,X1)
| ssList(X0)
| ssList(X1)
| ssList(X2)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f402,plain,
! [X2,X0,X1] :
( ~ memberP(X1,X2)
| ssList(X1)
| ssItem(X0)
| ssItem(X2)
| memberP(cons(X0,X1),X2)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f414,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,[],[f238]) ).
fof(f416,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,[],[f239]) ).
fof(f420,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,[],[f241]) ).
fof(f426,plain,
! [X2,X3,X0,X1,X4] :
( ~ cyclefreeP(app(app(X2,cons(X0,X3)),cons(X1,X4)))
| leq(X1,X0)
| ssList(X4)
| ssList(X3)
| ssList(X2)
| ssItem(X1)
| ssItem(X0)
| leq(X0,X1)
| ssList(app(app(X2,cons(X0,X3)),cons(X1,X4))) ),
inference(consistent_polarity_flipping,[],[f247]) ).
fof(f427,plain,
~ ssList(sk3),
inference(consistent_polarity_flipping,[],[f221]) ).
fof(f431,plain,
~ ssItem(sk5),
inference(consistent_polarity_flipping,[],[f206]) ).
fof(f432,plain,
~ ssItem(sk6),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f433,plain,
~ ssList(sk7),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f434,plain,
~ ssList(sk8),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f436,plain,
( ~ ssItem(sk9)
| nil = sk3 ),
inference(consistent_polarity_flipping,[],[f214]) ).
fof(f446,definition,
( spl0_1
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f448,plain,
( nil = sk3
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f446]) ).
fof(f455,definition,
( spl0_3
<=> sk3 = cons(sk9,nil) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f457,plain,
( sk3 = cons(sk9,nil)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f458,plain,
( spl0_1
| spl0_3 ),
inference(avatar_split_clause,[],[f219,f455,f446]) ).
fof(f466,definition,
( spl0_5
<=> ssItem(sk9) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f468,plain,
( ~ ssItem(sk9)
| spl0_5 ),
inference(avatar_component_clause,[],[f466]) ).
fof(f469,plain,
( spl0_1
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f436,f466,f446]) ).
fof(f476,definition,
( spl0_7
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f477,plain,
( ~ ssList(nil)
| spl0_7 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f504,definition,
( spl0_13
<=> ! [X1] : ~ ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f505,plain,
( ! [X1] : ~ ssItem(X1)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f504]) ).
fof(f507,definition,
( spl0_14
<=> ! [X0] :
( ssList(X0)
| duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f508,plain,
( ! [X0] :
( duplicatefreeP(X0)
| ssList(X0) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f509,plain,
( spl0_13
| spl0_14 ),
inference(avatar_split_clause,[],[f313,f507,f504]) ).
fof(f512,plain,
~ spl0_7,
inference(avatar_split_clause,[],[f251,f476]) ).
fof(f514,plain,
( ! [X0] : ~ leq(X0,X0)
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f303,f505]) ).
fof(f516,plain,
( ! [X0] : memberP(nil,X0)
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f312,f505]) ).
fof(f560,plain,
sk3 = app(sk3,nil),
inference(resolution,[],[f314,f427]) ).
fof(f595,plain,
sk8 = app(nil,sk8),
inference(resolution,[],[f315,f434]) ).
fof(f634,plain,
( ! [X0,X1] :
( ssList(X1)
| tl(cons(X0,X1)) = X1 )
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f337,f505]) ).
fof(f636,plain,
( ! [X0,X1] : skaf82(X1) = tl(cons(X0,skaf82(X1)))
| ~ spl0_13 ),
inference(resolution,[],[f634,f255]) ).
fof(f714,definition,
( spl0_15
<=> sk5 = sk6 ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f716,plain,
( sk5 = sk6
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f714]) ).
fof(f800,definition,
( spl0_18
<=> nil = sk8 ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f801,plain,
( nil != sk8
| spl0_18 ),
inference(avatar_component_clause,[],[f800]) ).
fof(f802,plain,
( nil = sk8
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f800]) ).
fof(f804,definition,
( spl0_19
<=> sk8 = cons(hd(sk8),tl(sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f806,plain,
( sk8 = cons(hd(sk8),tl(sk8))
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f804]) ).
fof(f882,definition,
( spl0_24
<=> sk8 = cons(skaf83(sk8),skaf82(sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f884,plain,
( sk8 = cons(skaf83(sk8),skaf82(sk8))
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f882]) ).
fof(f909,definition,
( spl0_26
<=> ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f910,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| spl0_26 ),
inference(avatar_component_clause,[],[f909]) ).
fof(f911,plain,
( ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f909]) ).
fof(f913,definition,
( spl0_27
<=> nil = app(app(sk7,cons(sk5,nil)),cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f914,plain,
( nil != app(app(sk7,cons(sk5,nil)),cons(sk5,nil))
| spl0_27 ),
inference(avatar_component_clause,[],[f913]) ).
fof(f915,plain,
( nil = app(app(sk7,cons(sk5,nil)),cons(sk5,nil))
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f913]) ).
fof(f973,plain,
( cyclefreeP(sk3)
| ssItem(sk9)
| ~ spl0_3 ),
inference(superposition,[],[f311,f457]) ).
fof(f974,plain,
( cyclefreeP(sk3)
| ~ spl0_3
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f973,f468]) ).
fof(f1151,plain,
( ssItem(sk5)
| ssItem(sk6)
| sk5 = sk6 ),
inference(resolution,[],[f343,f212]) ).
fof(f1156,plain,
( ssItem(sk6)
| sk5 = sk6 ),
inference(forward_subsumption_resolution,[],[f1151,f431]) ).
fof(f1157,plain,
sk5 = sk6,
inference(forward_subsumption_resolution,[],[f1156,f432]) ).
fof(f1162,plain,
spl0_15,
inference(avatar_split_clause,[],[f1157,f714]) ).
fof(f1220,plain,
( ! [X0] :
( ssList(X0)
| cons(sk9,X0) = app(cons(sk9,nil),X0) )
| spl0_5 ),
inference(resolution,[],[f361,f468]) ).
fof(f1251,plain,
( ! [X0] :
( ssList(X0)
| cons(sk9,X0) = app(sk3,X0) )
| ~ spl0_3
| spl0_5 ),
inference(forward_demodulation,[],[f1220,f457]) ).
fof(f1306,plain,
! [X0,X1] :
( ~ rearsegP(app(X0,X1),X1)
| ssList(X1)
| ssList(X0) ),
inference(forward_subsumption_resolution,[],[f384,f326]) ).
fof(f1314,plain,
( ~ rearsegP(sk3,sk8)
| ssList(sk8)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
inference(superposition,[],[f1306,f223]) ).
fof(f1324,plain,
( ~ rearsegP(sk3,sk8)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
inference(forward_subsumption_resolution,[],[f1314,f434]) ).
fof(f1469,plain,
! [X0] :
( ssList(X0)
| ssList(X0)
| app(skaf46(X0,X0),X0) = X0
| ssList(X0) ),
inference(resolution,[],[f372,f300]) ).
fof(f1472,plain,
! [X0] :
( ssList(X0)
| app(skaf46(X0,X0),X0) = X0 ),
inference(duplicate_literal_removal,[],[f1469]) ).
fof(f2135,plain,
! [X0] :
( sk3 != app(X0,sk8)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ssList(sk8)
| ssList(X0)
| app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) = X0 ),
inference(superposition,[],[f392,f223]) ).
fof(f2146,plain,
! [X0] :
( sk3 != app(X0,sk8)
| ssList(X0)
| ssList(sk8)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) = X0 ),
inference(superposition,[],[f392,f223]) ).
fof(f2161,plain,
! [X0] :
( sk3 != app(X0,sk8)
| ssList(X0)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) = X0 ),
inference(forward_subsumption_resolution,[],[f2146,f434]) ).
fof(f2171,plain,
! [X0] :
( sk3 != app(X0,sk8)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ssList(X0)
| app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) = X0 ),
inference(forward_subsumption_resolution,[],[f2135,f434]) ).
fof(f2181,plain,
( ! [X0] :
( app(X0,nil) != sk3
| ssList(X0)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) = X0 )
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2161,f802]) ).
fof(f2650,definition,
( spl0_65
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f2651,plain,
( ~ ssList(cons(sk5,nil))
| spl0_65 ),
inference(avatar_component_clause,[],[f2650]) ).
fof(f2652,plain,
( ssList(cons(sk5,nil))
| ~ spl0_65 ),
inference(avatar_component_clause,[],[f2650]) ).
fof(f2712,plain,
! [X0] :
( ~ segmentP(app(sk3,X0),sk8)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ssList(sk8)
| ssList(app(sk3,X0))
| ssList(X0) ),
inference(superposition,[],[f414,f223]) ).
fof(f2718,plain,
( ~ segmentP(sk3,cons(sk6,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| ssList(sk3)
| ssList(sk8) ),
inference(superposition,[],[f414,f223]) ).
fof(f2725,plain,
( ~ segmentP(sk3,cons(sk6,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| ssList(sk8) ),
inference(forward_subsumption_resolution,[],[f2718,f427]) ).
fof(f2726,plain,
! [X0] :
( ~ segmentP(app(sk3,X0),sk8)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ssList(app(sk3,X0))
| ssList(X0) ),
inference(forward_subsumption_resolution,[],[f2712,f434]) ).
fof(f2732,plain,
( ~ segmentP(sk3,cons(sk6,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil)) ),
inference(forward_subsumption_resolution,[],[f2725,f434]) ).
fof(f2739,plain,
( ~ segmentP(sk3,cons(sk5,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| ~ spl0_15 ),
inference(forward_demodulation,[],[f2732,f716]) ).
fof(f2745,plain,
( ~ segmentP(nil,cons(sk5,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| ~ spl0_1
| ~ spl0_15 ),
inference(forward_demodulation,[],[f2739,f448]) ).
fof(f2753,definition,
( spl0_67
<=> segmentP(nil,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f2755,plain,
( ~ segmentP(nil,cons(sk5,nil))
| spl0_67 ),
inference(avatar_component_clause,[],[f2753]) ).
fof(f2783,plain,
( ! [X2,X3,X0,X1] :
( ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(X2)
| ssList(X0)
| ssItem(X1)
| ssList(X3) )
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f420,f508]) ).
fof(f2787,plain,
( ssList(nil)
| ssItem(sk5)
| ~ spl0_65 ),
inference(resolution,[],[f2652,f327]) ).
fof(f2788,plain,
( ssItem(sk5)
| spl0_7
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f2787,f477]) ).
fof(f2789,plain,
( $false
| spl0_7
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f2788,f431]) ).
fof(f2790,plain,
( spl0_7
| ~ spl0_65 ),
inference(avatar_contradiction_clause,[],[f2789]) ).
fof(f2808,definition,
( spl0_68
<=> nil = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f2809,plain,
( nil != cons(sk5,nil)
| spl0_68 ),
inference(avatar_component_clause,[],[f2808]) ).
fof(f2810,plain,
( nil = cons(sk5,nil)
| ~ spl0_68 ),
inference(avatar_component_clause,[],[f2808]) ).
fof(f2905,plain,
( ssList(cons(sk5,nil))
| nil = cons(sk5,nil)
| spl0_67 ),
inference(resolution,[],[f2755,f321]) ).
fof(f2908,plain,
( nil = cons(sk5,nil)
| spl0_65
| spl0_67 ),
inference(forward_subsumption_resolution,[],[f2905,f2651]) ).
fof(f2910,plain,
( spl0_68
| spl0_65
| spl0_67 ),
inference(avatar_split_clause,[],[f2908,f2753,f2650,f2808]) ).
fof(f3002,plain,
( singletonP(nil)
| ssList(nil)
| ssItem(sk5)
| ~ spl0_68 ),
inference(superposition,[],[f357,f2810]) ).
fof(f3051,plain,
( ssList(nil)
| ssItem(sk5)
| ~ spl0_68 ),
inference(forward_subsumption_resolution,[],[f3002,f11]) ).
fof(f3075,plain,
( ssItem(sk5)
| spl0_7
| ~ spl0_68 ),
inference(forward_subsumption_resolution,[],[f3051,f477]) ).
fof(f3081,plain,
( $false
| spl0_7
| ~ spl0_68 ),
inference(forward_subsumption_resolution,[],[f3075,f431]) ).
fof(f3082,plain,
( spl0_7
| ~ spl0_68 ),
inference(avatar_contradiction_clause,[],[f3081]) ).
fof(f3119,plain,
( ssList(cons(sk5,nil))
| ~ segmentP(nil,cons(sk5,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_1
| ~ spl0_15 ),
inference(forward_demodulation,[],[f2745,f716]) ).
fof(f3139,plain,
( ~ segmentP(nil,cons(sk5,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_1
| ~ spl0_15
| spl0_65 ),
inference(forward_subsumption_resolution,[],[f3119,f2651]) ).
fof(f3153,definition,
( spl0_81
<=> ssList(app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f3154,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| spl0_81 ),
inference(avatar_component_clause,[],[f3153]) ).
fof(f3155,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f3153]) ).
fof(f3156,plain,
( spl0_81
| ~ spl0_67
| ~ spl0_1
| ~ spl0_15
| spl0_65 ),
inference(avatar_split_clause,[],[f3139,f2650,f714,f446,f2753,f3153]) ).
fof(f3161,plain,
( ssList(sk7)
| ssList(cons(sk5,nil))
| ~ spl0_81 ),
inference(resolution,[],[f3155,f326]) ).
fof(f3162,plain,
( ssList(cons(sk5,nil))
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f3161,f433]) ).
fof(f3163,plain,
( $false
| spl0_65
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f3162,f2651]) ).
fof(f3164,plain,
( spl0_65
| ~ spl0_81 ),
inference(avatar_contradiction_clause,[],[f3163]) ).
fof(f3317,plain,
( ! [X0] :
( ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| app(X0,nil) != sk3
| ssList(X0)
| app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) = X0 )
| ~ spl0_15
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2181,f716]) ).
fof(f3434,plain,
( ! [X0] :
( app(app(sk7,cons(sk5,nil)),cons(sk5,nil)) = X0
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| app(X0,nil) != sk3
| ssList(X0) )
| ~ spl0_15
| ~ spl0_18 ),
inference(forward_demodulation,[],[f3317,f716]) ).
fof(f3461,definition,
( spl0_139
<=> ! [X0] :
( app(app(sk7,cons(sk5,nil)),cons(sk5,nil)) = X0
| ssList(X0)
| app(X0,nil) != sk3 ) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f3462,plain,
( ! [X0] :
( app(X0,nil) != sk3
| ssList(X0)
| app(app(sk7,cons(sk5,nil)),cons(sk5,nil)) = X0 )
| ~ spl0_139 ),
inference(avatar_component_clause,[],[f3461]) ).
fof(f3623,definition,
( spl0_145
<=> nil = app(sk7,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f3625,plain,
( nil = app(sk7,cons(sk5,nil))
| ~ spl0_145 ),
inference(avatar_component_clause,[],[f3623]) ).
fof(f4606,plain,
( ! [X0] : cons(sk9,skaf82(X0)) = app(sk3,skaf82(X0))
| ~ spl0_3
| spl0_5 ),
inference(resolution,[],[f1251,f255]) ).
fof(f4772,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk5,nil))
| ~ spl0_26 ),
inference(resolution,[],[f911,f326]) ).
fof(f4773,plain,
( ssList(cons(sk5,nil))
| ~ spl0_26
| spl0_81 ),
inference(forward_subsumption_resolution,[],[f4772,f3154]) ).
fof(f4774,plain,
( $false
| ~ spl0_26
| spl0_65
| spl0_81 ),
inference(forward_subsumption_resolution,[],[f4773,f2651]) ).
fof(f4775,plain,
( ~ spl0_26
| spl0_65
| spl0_81 ),
inference(avatar_contradiction_clause,[],[f4774]) ).
fof(f4777,plain,
( ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ rearsegP(sk3,sk8)
| ~ spl0_15 ),
inference(forward_demodulation,[],[f1324,f716]) ).
fof(f4787,plain,
( ! [X0] :
( ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| sk3 != app(X0,sk8)
| ssList(X0)
| app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) = X0 )
| ~ spl0_15 ),
inference(forward_demodulation,[],[f2171,f716]) ).
fof(f4788,plain,
( ! [X0] :
( ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ segmentP(app(sk3,X0),sk8)
| ssList(app(sk3,X0))
| ssList(X0) )
| ~ spl0_15 ),
inference(forward_demodulation,[],[f2726,f716]) ).
fof(f4808,definition,
( spl0_207
<=> rearsegP(sk3,sk8) ),
introduced(definition,[new_symbols(definition,[spl0_207])],[avatar_definition]) ).
fof(f4810,plain,
( ~ rearsegP(sk3,sk8)
| spl0_207 ),
inference(avatar_component_clause,[],[f4808]) ).
fof(f4811,plain,
( ~ spl0_207
| spl0_26
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f4777,f714,f909,f4808]) ).
fof(f4813,plain,
( ! [X0] :
( app(app(sk7,cons(sk5,nil)),cons(sk5,nil)) = X0
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| sk3 != app(X0,sk8)
| ssList(X0) )
| ~ spl0_15 ),
inference(forward_demodulation,[],[f4787,f716]) ).
fof(f4815,definition,
( spl0_208
<=> ! [X0] :
( ~ segmentP(app(sk3,X0),sk8)
| ssList(X0)
| ssList(app(sk3,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl0_208])],[avatar_definition]) ).
fof(f4816,plain,
( ! [X0] :
( ~ segmentP(app(sk3,X0),sk8)
| ssList(X0)
| ssList(app(sk3,X0)) )
| ~ spl0_208 ),
inference(avatar_component_clause,[],[f4815]) ).
fof(f4817,plain,
( spl0_208
| spl0_26
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f4788,f714,f909,f4815]) ).
fof(f4819,definition,
( spl0_209
<=> ! [X0] :
( app(app(sk7,cons(sk5,nil)),cons(sk5,nil)) = X0
| ssList(X0)
| sk3 != app(X0,sk8) ) ),
introduced(definition,[new_symbols(definition,[spl0_209])],[avatar_definition]) ).
fof(f4820,plain,
( ! [X0] :
( sk3 != app(X0,sk8)
| ssList(X0)
| app(app(sk7,cons(sk5,nil)),cons(sk5,nil)) = X0 )
| ~ spl0_209 ),
inference(avatar_component_clause,[],[f4819]) ).
fof(f4822,plain,
( spl0_26
| spl0_209
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f4813,f714,f4819,f909]) ).
fof(f5008,plain,
( ssList(nil)
| ssList(sk7)
| ssItem(sk5)
| ssList(nil)
| ~ spl0_14
| spl0_26 ),
inference(resolution,[],[f910,f2783]) ).
fof(f5033,plain,
( ssList(nil)
| ssList(sk7)
| ssItem(sk5)
| ~ spl0_14
| spl0_26 ),
inference(duplicate_literal_removal,[],[f5008]) ).
fof(f5052,plain,
( ssList(sk7)
| ssItem(sk5)
| spl0_7
| ~ spl0_14
| spl0_26 ),
inference(forward_subsumption_resolution,[],[f5033,f477]) ).
fof(f5053,plain,
( ssItem(sk5)
| spl0_7
| ~ spl0_14
| spl0_26 ),
inference(forward_subsumption_resolution,[],[f5052,f433]) ).
fof(f5054,plain,
( $false
| spl0_7
| ~ spl0_14
| spl0_26 ),
inference(forward_subsumption_resolution,[],[f5053,f431]) ).
fof(f5055,plain,
( spl0_7
| ~ spl0_14
| spl0_26 ),
inference(avatar_contradiction_clause,[],[f5054]) ).
fof(f5103,plain,
( ! [X2,X0,X1] :
( ~ memberP(X1,X2)
| ssList(X1)
| ssItem(X2)
| memberP(cons(X0,X1),X2)
| X0 = X2 )
| ~ spl0_13 ),
inference(backward_subsumption_resolution,[],[f402,f505]) ).
fof(f5108,plain,
( ! [X2,X0,X1] :
( ~ memberP(app(X0,cons(X1,X2)),X1)
| ssList(X0)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2) )
| ~ spl0_13 ),
inference(backward_subsumption_resolution,[],[f416,f505]) ).
fof(f5115,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ cyclefreeP(app(app(X2,cons(X0,X3)),cons(X1,X4)))
| leq(X1,X0)
| ssList(X4)
| ssList(X3)
| ssList(X2)
| ssItem(X1)
| leq(X0,X1)
| ssList(app(app(X2,cons(X0,X3)),cons(X1,X4))) )
| ~ spl0_13 ),
inference(backward_subsumption_resolution,[],[f426,f505]) ).
fof(f5140,plain,
( ! [X2,X0,X1] :
( ~ memberP(X1,X2)
| ssList(X1)
| memberP(cons(X0,X1),X2)
| X0 = X2 )
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f5103,f505]) ).
fof(f5150,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ cyclefreeP(app(app(X2,cons(X0,X3)),cons(X1,X4)))
| leq(X1,X0)
| ssList(X4)
| ssList(X3)
| ssList(X2)
| leq(X0,X1)
| ssList(app(app(X2,cons(X0,X3)),cons(X1,X4))) )
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f5115,f505]) ).
fof(f5679,plain,
( ! [X0,X1] :
( ssList(nil)
| memberP(cons(X0,nil),X1)
| X0 = X1 )
| ~ spl0_13 ),
inference(resolution,[],[f5140,f516]) ).
fof(f5680,plain,
( ! [X0,X1] :
( memberP(cons(X0,nil),X1)
| X0 = X1 )
| spl0_7
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f5679,f477]) ).
fof(f6763,plain,
( ssList(sk8)
| ssList(sk3)
| sk3 = app(skaf46(sk3,sk8),sk8)
| spl0_207 ),
inference(resolution,[],[f4810,f372]) ).
fof(f6764,plain,
( ssList(sk3)
| sk3 = app(skaf46(sk3,sk8),sk8)
| spl0_207 ),
inference(forward_subsumption_resolution,[],[f6763,f434]) ).
fof(f6765,plain,
( sk3 = app(skaf46(sk3,sk8),sk8)
| spl0_207 ),
inference(forward_subsumption_resolution,[],[f6764,f427]) ).
fof(f6807,definition,
( spl0_242
<=> ssList(tl(sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_242])],[avatar_definition]) ).
fof(f6809,plain,
( ssList(tl(sk8))
| ~ spl0_242 ),
inference(avatar_component_clause,[],[f6807]) ).
fof(f6819,definition,
( spl0_245
<=> sk9 = hd(sk8) ),
introduced(definition,[new_symbols(definition,[spl0_245])],[avatar_definition]) ).
fof(f6821,plain,
( sk9 = hd(sk8)
| ~ spl0_245 ),
inference(avatar_component_clause,[],[f6819]) ).
fof(f6832,definition,
( spl0_248
<=> sk3 = sk8 ),
introduced(definition,[new_symbols(definition,[spl0_248])],[avatar_definition]) ).
fof(f6834,plain,
( sk3 != sk8
| spl0_248 ),
inference(avatar_component_clause,[],[f6832]) ).
fof(f6880,definition,
( spl0_259
<=> ! [X0] :
( ~ memberP(app(X0,sk8),hd(sk8))
| ssList(app(X0,sk8))
| ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_259])],[avatar_definition]) ).
fof(f6881,plain,
( ! [X0] :
( ~ memberP(app(X0,sk8),hd(sk8))
| ssList(app(X0,sk8))
| ssList(X0) )
| ~ spl0_259 ),
inference(avatar_component_clause,[],[f6880]) ).
fof(f6925,plain,
( ! [X0] :
( app(app(sk7,cons(sk5,nil)),cons(sk5,nil)) = X0
| app(X0,nil) != sk3
| ssList(X0) )
| ~ spl0_15
| ~ spl0_18
| spl0_26 ),
inference(forward_subsumption_resolution,[],[f3434,f910]) ).
fof(f6989,plain,
( spl0_139
| ~ spl0_15
| ~ spl0_18
| spl0_26 ),
inference(avatar_split_clause,[],[f6925,f909,f800,f714,f3461]) ).
fof(f7231,plain,
( nil != nil
| ssList(cons(sk5,nil))
| ssList(app(sk7,cons(sk5,nil)))
| nil = app(sk7,cons(sk5,nil))
| ~ spl0_27 ),
inference(superposition,[],[f359,f915]) ).
fof(f7250,plain,
( ssList(cons(sk5,nil))
| ssList(app(sk7,cons(sk5,nil)))
| nil = app(sk7,cons(sk5,nil))
| ~ spl0_27 ),
inference(trivial_inequality_removal,[],[f7231]) ).
fof(f7269,plain,
( ssList(app(sk7,cons(sk5,nil)))
| nil = app(sk7,cons(sk5,nil))
| ~ spl0_27
| spl0_65 ),
inference(forward_subsumption_resolution,[],[f7250,f2651]) ).
fof(f7290,plain,
( nil = app(sk7,cons(sk5,nil))
| ~ spl0_27
| spl0_65
| spl0_81 ),
inference(forward_subsumption_resolution,[],[f7269,f3154]) ).
fof(f7302,plain,
( spl0_145
| ~ spl0_27
| spl0_65
| spl0_81 ),
inference(avatar_split_clause,[],[f7290,f3153,f2650,f913,f3623]) ).
fof(f9776,plain,
( sk3 != sk3
| ssList(sk3)
| sk3 = app(app(sk7,cons(sk5,nil)),cons(sk5,nil))
| ~ spl0_139 ),
inference(superposition,[],[f3462,f560]) ).
fof(f9780,plain,
( ssList(sk3)
| sk3 = app(app(sk7,cons(sk5,nil)),cons(sk5,nil))
| ~ spl0_139 ),
inference(trivial_inequality_removal,[],[f9776]) ).
fof(f9782,plain,
( sk3 = app(app(sk7,cons(sk5,nil)),cons(sk5,nil))
| ~ spl0_139 ),
inference(forward_subsumption_resolution,[],[f9780,f427]) ).
fof(f15858,plain,
( nil != nil
| ssList(cons(sk5,nil))
| ssList(sk7)
| nil = cons(sk5,nil)
| ~ spl0_145 ),
inference(superposition,[],[f360,f3625]) ).
fof(f15871,plain,
( ssList(cons(sk5,nil))
| ssList(sk7)
| nil = cons(sk5,nil)
| ~ spl0_145 ),
inference(trivial_inequality_removal,[],[f15858]) ).
fof(f15886,plain,
( ssList(sk7)
| nil = cons(sk5,nil)
| spl0_65
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f15871,f2651]) ).
fof(f15906,plain,
( nil = cons(sk5,nil)
| spl0_65
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f15886,f433]) ).
fof(f15917,plain,
( $false
| spl0_65
| spl0_68
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f15906,f2809]) ).
fof(f15918,plain,
( spl0_65
| spl0_68
| ~ spl0_145 ),
inference(avatar_contradiction_clause,[],[f15917]) ).
fof(f15956,plain,
( ! [X0] :
( memberP(sk3,X0)
| sk9 = X0 )
| ~ spl0_3
| spl0_7
| ~ spl0_13 ),
inference(superposition,[],[f5680,f457]) ).
fof(f16498,plain,
sk3 = app(skaf46(sk3,sk3),sk3),
inference(resolution,[],[f1472,f427]) ).
fof(f29038,definition,
( spl0_1019
<=> sk3 = app(app(sk7,cons(sk5,nil)),cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_1019])],[avatar_definition]) ).
fof(f29040,plain,
( sk3 = app(app(sk7,cons(sk5,nil)),cons(sk5,nil))
| ~ spl0_1019 ),
inference(avatar_component_clause,[],[f29038]) ).
fof(f52301,plain,
! [X0] :
( ~ segmentP(app(sk3,X0),sk3)
| ssList(skaf46(sk3,sk3))
| ssList(sk3)
| ssList(app(sk3,X0))
| ssList(X0) ),
inference(superposition,[],[f414,f16498]) ).
fof(f52310,plain,
! [X0] :
( ~ segmentP(app(sk3,X0),sk3)
| ssList(skaf46(sk3,sk3))
| ssList(sk3)
| ssList(X0) ),
inference(forward_subsumption_resolution,[],[f52301,f326]) ).
fof(f52322,plain,
! [X0] :
( ~ segmentP(app(sk3,X0),sk3)
| ssList(sk3)
| ssList(X0) ),
inference(forward_subsumption_resolution,[],[f52310,f292]) ).
fof(f52338,plain,
! [X0] :
( ~ segmentP(app(sk3,X0),sk3)
| ssList(X0) ),
inference(forward_subsumption_resolution,[],[f52322,f427]) ).
fof(f78559,plain,
( ! [X0] :
( ~ segmentP(cons(sk9,skaf82(X0)),sk3)
| ssList(skaf82(X0)) )
| ~ spl0_3
| spl0_5 ),
inference(superposition,[],[f52338,f4606]) ).
fof(f78603,plain,
( ! [X0] : ~ segmentP(cons(sk9,skaf82(X0)),sk3)
| ~ spl0_3
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f78559,f255]) ).
fof(f100893,plain,
( spl0_1019
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f9782,f3461,f29038]) ).
fof(f117898,plain,
( ~ cyclefreeP(sk3)
| leq(sk5,sk5)
| ssList(nil)
| ssList(nil)
| ssList(sk7)
| leq(sk5,sk5)
| ssList(sk3)
| ~ spl0_13
| ~ spl0_1019 ),
inference(superposition,[],[f5150,f29040]) ).
fof(f117934,plain,
( ~ cyclefreeP(sk3)
| leq(sk5,sk5)
| ssList(nil)
| ssList(sk7)
| ssList(sk3)
| ~ spl0_13
| ~ spl0_1019 ),
inference(duplicate_literal_removal,[],[f117898]) ).
fof(f117964,plain,
( leq(sk5,sk5)
| ssList(nil)
| ssList(sk7)
| ssList(sk3)
| ~ spl0_3
| spl0_5
| ~ spl0_13
| ~ spl0_1019 ),
inference(forward_subsumption_resolution,[],[f117934,f974]) ).
fof(f118004,plain,
( ssList(nil)
| ssList(sk7)
| ssList(sk3)
| ~ spl0_3
| spl0_5
| ~ spl0_13
| ~ spl0_1019 ),
inference(forward_subsumption_resolution,[],[f117964,f514]) ).
fof(f118036,plain,
( ssList(sk7)
| ssList(sk3)
| ~ spl0_3
| spl0_5
| spl0_7
| ~ spl0_13
| ~ spl0_1019 ),
inference(forward_subsumption_resolution,[],[f118004,f477]) ).
fof(f118045,plain,
( ssList(sk3)
| ~ spl0_3
| spl0_5
| spl0_7
| ~ spl0_13
| ~ spl0_1019 ),
inference(forward_subsumption_resolution,[],[f118036,f433]) ).
fof(f118053,plain,
( $false
| ~ spl0_3
| spl0_5
| spl0_7
| ~ spl0_13
| ~ spl0_1019 ),
inference(forward_subsumption_resolution,[],[f118045,f427]) ).
fof(f118054,plain,
( ~ spl0_3
| spl0_5
| spl0_7
| ~ spl0_13
| ~ spl0_1019 ),
inference(avatar_contradiction_clause,[],[f118053]) ).
fof(f118124,definition,
( spl0_4473
<=> ssList(sk8) ),
introduced(definition,[new_symbols(definition,[spl0_4473])],[avatar_definition]) ).
fof(f118126,plain,
( ~ ssList(sk8)
| spl0_4473 ),
inference(avatar_component_clause,[],[f118124]) ).
fof(f118971,plain,
~ spl0_4473,
inference(avatar_split_clause,[],[f434,f118124]) ).
fof(f118974,plain,
( sk8 = cons(hd(sk8),tl(sk8))
| nil = sk8
| spl0_4473 ),
inference(resolution,[],[f118126,f345]) ).
fof(f118975,plain,
( sk8 = cons(skaf83(sk8),skaf82(sk8))
| nil = sk8
| spl0_4473 ),
inference(resolution,[],[f118126,f350]) ).
fof(f119835,plain,
( spl0_18
| spl0_24
| spl0_4473 ),
inference(avatar_split_clause,[],[f118975,f118124,f882,f800]) ).
fof(f119836,plain,
( spl0_18
| spl0_19
| spl0_4473 ),
inference(avatar_split_clause,[],[f118974,f118124,f804,f800]) ).
fof(f119843,plain,
( ! [X0] :
( ~ memberP(app(X0,sk8),hd(sk8))
| ssList(X0)
| ssList(app(X0,sk8))
| ssList(tl(sk8)) )
| ~ spl0_13
| ~ spl0_19 ),
inference(superposition,[],[f5108,f806]) ).
fof(f120109,plain,
( spl0_242
| spl0_259
| ~ spl0_13
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f119843,f804,f504,f6880,f6807]) ).
fof(f120114,plain,
( tl(sk8) = skaf82(sk8)
| ~ spl0_13
| ~ spl0_24 ),
inference(superposition,[],[f636,f884]) ).
fof(f120635,plain,
( ssList(sk8)
| nil = sk8
| ~ spl0_242 ),
inference(resolution,[],[f6809,f316]) ).
fof(f120636,plain,
( nil = sk8
| ~ spl0_242
| spl0_4473 ),
inference(forward_subsumption_resolution,[],[f120635,f118126]) ).
fof(f120637,plain,
( $false
| spl0_18
| ~ spl0_242
| spl0_4473 ),
inference(forward_subsumption_resolution,[],[f120636,f801]) ).
fof(f120638,plain,
( spl0_18
| ~ spl0_242
| spl0_4473 ),
inference(avatar_contradiction_clause,[],[f120637]) ).
fof(f120648,plain,
( ~ segmentP(sk3,sk8)
| ssList(nil)
| ssList(sk3)
| ~ spl0_208 ),
inference(superposition,[],[f4816,f560]) ).
fof(f120726,plain,
( ~ segmentP(sk3,sk8)
| ssList(sk3)
| spl0_7
| ~ spl0_208 ),
inference(forward_subsumption_resolution,[],[f120648,f477]) ).
fof(f120769,plain,
( ~ segmentP(sk3,sk8)
| spl0_7
| ~ spl0_208 ),
inference(forward_subsumption_resolution,[],[f120726,f427]) ).
fof(f123005,plain,
( sk3 != sk8
| ssList(nil)
| nil = app(app(sk7,cons(sk5,nil)),cons(sk5,nil))
| ~ spl0_209 ),
inference(superposition,[],[f4820,f595]) ).
fof(f123010,plain,
( sk3 != sk8
| nil = app(app(sk7,cons(sk5,nil)),cons(sk5,nil))
| spl0_7
| ~ spl0_209 ),
inference(forward_subsumption_resolution,[],[f123005,f477]) ).
fof(f123012,plain,
( sk3 != sk8
| spl0_7
| spl0_27
| ~ spl0_209 ),
inference(forward_subsumption_resolution,[],[f123010,f914]) ).
fof(f123013,plain,
( ~ spl0_248
| spl0_7
| spl0_27
| ~ spl0_209 ),
inference(avatar_split_clause,[],[f123012,f4819,f913,f476,f6832]) ).
fof(f123848,plain,
( sk8 = cons(sk9,tl(sk8))
| ~ spl0_19
| ~ spl0_245 ),
inference(superposition,[],[f806,f6821]) ).
fof(f131443,plain,
( ~ segmentP(cons(sk9,tl(sk8)),sk3)
| ~ spl0_3
| spl0_5
| ~ spl0_13
| ~ spl0_24 ),
inference(superposition,[],[f78603,f120114]) ).
fof(f141827,plain,
( ~ memberP(sk3,hd(sk8))
| ssList(sk3)
| ssList(skaf46(sk3,sk8))
| spl0_207
| ~ spl0_259 ),
inference(superposition,[],[f6881,f6765]) ).
fof(f141840,plain,
( ~ memberP(sk3,hd(sk8))
| ssList(skaf46(sk3,sk8))
| spl0_207
| ~ spl0_259 ),
inference(forward_subsumption_resolution,[],[f141827,f427]) ).
fof(f141844,plain,
( ~ memberP(sk3,hd(sk8))
| spl0_207
| ~ spl0_259 ),
inference(forward_subsumption_resolution,[],[f141840,f292]) ).
fof(f141854,plain,
( sk9 = hd(sk8)
| ~ spl0_3
| spl0_7
| ~ spl0_13
| spl0_207
| ~ spl0_259 ),
inference(resolution,[],[f141844,f15956]) ).
fof(f141874,plain,
( spl0_245
| ~ spl0_3
| spl0_7
| ~ spl0_13
| spl0_207
| ~ spl0_259 ),
inference(avatar_split_clause,[],[f141854,f6880,f4808,f504,f476,f455,f6819]) ).
fof(f152798,plain,
( ~ segmentP(sk8,sk3)
| ~ spl0_3
| spl0_5
| ~ spl0_13
| ~ spl0_19
| ~ spl0_24
| ~ spl0_245 ),
inference(forward_demodulation,[],[f131443,f123848]) ).
fof(f152849,plain,
( segmentP(sk3,sk8)
| ssList(sk8)
| ssList(sk3)
| sk3 = sk8
| ~ spl0_3
| spl0_5
| ~ spl0_13
| ~ spl0_19
| ~ spl0_24
| ~ spl0_245 ),
inference(resolution,[],[f152798,f368]) ).
fof(f152865,plain,
( ssList(sk8)
| ssList(sk3)
| sk3 = sk8
| ~ spl0_3
| spl0_5
| spl0_7
| ~ spl0_13
| ~ spl0_19
| ~ spl0_24
| ~ spl0_208
| ~ spl0_245 ),
inference(forward_subsumption_resolution,[],[f152849,f120769]) ).
fof(f152873,plain,
( ssList(sk3)
| sk3 = sk8
| ~ spl0_3
| spl0_5
| spl0_7
| ~ spl0_13
| ~ spl0_19
| ~ spl0_24
| ~ spl0_208
| ~ spl0_245
| spl0_4473 ),
inference(forward_subsumption_resolution,[],[f152865,f118126]) ).
fof(f152876,plain,
( sk3 = sk8
| ~ spl0_3
| spl0_5
| spl0_7
| ~ spl0_13
| ~ spl0_19
| ~ spl0_24
| ~ spl0_208
| ~ spl0_245
| spl0_4473 ),
inference(forward_subsumption_resolution,[],[f152873,f427]) ).
fof(f152879,plain,
( $false
| ~ spl0_3
| spl0_5
| spl0_7
| ~ spl0_13
| ~ spl0_19
| ~ spl0_24
| ~ spl0_208
| ~ spl0_245
| spl0_248
| spl0_4473 ),
inference(forward_subsumption_resolution,[],[f152876,f6834]) ).
fof(f152880,plain,
( ~ spl0_3
| spl0_5
| spl0_7
| ~ spl0_13
| ~ spl0_19
| ~ spl0_24
| ~ spl0_208
| ~ spl0_245
| spl0_248
| spl0_4473 ),
inference(avatar_contradiction_clause,[],[f152879]) ).
cnf(s2,plain,
( spl0_1
| spl0_3 ),
inference(sat_conversion,[],[f458]) ).
cnf(s5,plain,
( spl0_1
| ~ spl0_5 ),
inference(sat_conversion,[],[f469]) ).
cnf(s13,plain,
( spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f509]) ).
cnf(s16,plain,
~ spl0_7,
inference(sat_conversion,[],[f512]) ).
cnf(s43,plain,
spl0_15,
inference(sat_conversion,[],[f1162]) ).
cnf(s112,plain,
( spl0_7
| ~ spl0_65 ),
inference(sat_conversion,[],[f2790]) ).
cnf(s118,plain,
( spl0_65
| spl0_67
| spl0_68 ),
inference(sat_conversion,[],[f2910]) ).
cnf(s122,plain,
( spl0_7
| ~ spl0_68 ),
inference(sat_conversion,[],[f3082]) ).
cnf(s135,plain,
( ~ spl0_1
| ~ spl0_15
| spl0_65
| ~ spl0_67
| spl0_81 ),
inference(sat_conversion,[],[f3156]) ).
cnf(s137,plain,
( spl0_65
| ~ spl0_81 ),
inference(sat_conversion,[],[f3164]) ).
cnf(s376,plain,
( ~ spl0_26
| spl0_65
| spl0_81 ),
inference(sat_conversion,[],[f4775]) ).
cnf(s385,plain,
( ~ spl0_15
| spl0_26
| ~ spl0_207 ),
inference(sat_conversion,[],[f4811]) ).
cnf(s386,plain,
( ~ spl0_15
| spl0_26
| spl0_208 ),
inference(sat_conversion,[],[f4817]) ).
cnf(s388,plain,
( ~ spl0_15
| spl0_26
| spl0_209 ),
inference(sat_conversion,[],[f4822]) ).
cnf(s419,plain,
( spl0_7
| ~ spl0_14
| spl0_26 ),
inference(sat_conversion,[],[f5055]) ).
cnf(s592,plain,
( ~ spl0_15
| ~ spl0_18
| spl0_26
| spl0_139 ),
inference(sat_conversion,[],[f6989]) ).
cnf(s615,plain,
( ~ spl0_27
| spl0_65
| spl0_81
| spl0_145 ),
inference(sat_conversion,[],[f7302]) ).
cnf(s913,plain,
( spl0_65
| spl0_68
| ~ spl0_145 ),
inference(sat_conversion,[],[f15918]) ).
cnf(s4191,plain,
( ~ spl0_139
| spl0_1019 ),
inference(sat_conversion,[],[f100893]) ).
cnf(s5808,plain,
( ~ spl0_3
| spl0_5
| spl0_7
| ~ spl0_13
| ~ spl0_1019 ),
inference(sat_conversion,[],[f118054]) ).
cnf(s5885,plain,
~ spl0_4473,
inference(sat_conversion,[],[f118971]) ).
cnf(s5972,plain,
( spl0_18
| spl0_24
| spl0_4473 ),
inference(sat_conversion,[],[f119835]) ).
cnf(s5973,plain,
( spl0_18
| spl0_19
| spl0_4473 ),
inference(sat_conversion,[],[f119836]) ).
cnf(s6033,plain,
( ~ spl0_13
| ~ spl0_19
| spl0_242
| spl0_259 ),
inference(sat_conversion,[],[f120109]) ).
cnf(s6131,plain,
( spl0_18
| ~ spl0_242
| spl0_4473 ),
inference(sat_conversion,[],[f120638]) ).
cnf(s6254,plain,
( spl0_7
| spl0_27
| ~ spl0_209
| ~ spl0_248 ),
inference(sat_conversion,[],[f123013]) ).
cnf(s7816,plain,
( ~ spl0_3
| spl0_7
| ~ spl0_13
| spl0_207
| spl0_245
| ~ spl0_259 ),
inference(sat_conversion,[],[f141874]) ).
cnf(s8090,plain,
( ~ spl0_3
| spl0_5
| spl0_7
| ~ spl0_13
| ~ spl0_19
| ~ spl0_24
| ~ spl0_208
| ~ spl0_245
| spl0_248
| spl0_4473 ),
inference(sat_conversion,[],[f152880]) ).
cnf(s8270,plain,
~ spl0_68,
inference(rat,[],[s122,s16]) ).
cnf(s8271,plain,
~ spl0_65,
inference(rat,[],[s112,s16]) ).
cnf(s8276,plain,
~ spl0_145,
inference(rat,[],[s913,s8270,s8271]) ).
cnf(s8278,plain,
~ spl0_81,
inference(rat,[],[s137,s8271]) ).
cnf(s8279,plain,
spl0_67,
inference(rat,[],[s118,s8270,s8271]) ).
cnf(s8280,plain,
~ spl0_1,
inference(rat,[],[s135,s8278,s8279,s43,s8271]) ).
cnf(s8298,plain,
~ spl0_27,
inference(rat,[],[s615,s8276,s8271,s8278]) ).
cnf(s8299,plain,
~ spl0_26,
inference(rat,[],[s376,s8271,s8278]) ).
cnf(s8324,plain,
spl0_209,
inference(rat,[],[s388,s43,s8299]) ).
cnf(s8325,plain,
spl0_208,
inference(rat,[],[s386,s43,s8299]) ).
cnf(s8326,plain,
~ spl0_207,
inference(rat,[],[s385,s43,s8299]) ).
cnf(s8335,plain,
~ spl0_14,
inference(rat,[],[s419,s16,s8299]) ).
cnf(s8547,plain,
~ spl0_248,
inference(rat,[],[s6254,s8298,s16,s8324]) ).
cnf(s8596,plain,
spl0_13,
inference(rat,[],[s13,s8335]) ).
cnf(s9993,plain,
~ spl0_5,
inference(rat,[],[s5,s8280]) ).
cnf(s9994,plain,
spl0_3,
inference(rat,[],[s2,s8280]) ).
cnf(s10005,plain,
~ spl0_1019,
inference(rat,[],[s5808,s9993,s8596,s16,s9994]) ).
cnf(s10186,plain,
~ spl0_139,
inference(rat,[],[s4191,s10005]) ).
cnf(s10211,plain,
~ spl0_18,
inference(rat,[],[s592,s8299,s43,s10186]) ).
cnf(s10224,plain,
~ spl0_242,
inference(rat,[],[s6131,s5885,s10211]) ).
cnf(s10225,plain,
spl0_19,
inference(rat,[],[s5973,s5885,s10211]) ).
cnf(s10226,plain,
spl0_24,
inference(rat,[],[s5972,s5885,s10211]) ).
cnf(s10412,plain,
spl0_259,
inference(rat,[],[s6033,s10224,s8596,s10225]) ).
cnf(s10450,plain,
~ spl0_245,
inference(rat,[],[s8090,s5885,s8547,s10225,s8325,s9994,s9993,s8596,s16,s10226]) ).
cnf(s10633,plain,
$false,
inference(rat,[],[s7816,s9994,s8596,s8326,s16,s10412,s10450]) ).
fof(f152881,plain,
$false,
inference(avatar_sat_refutation,[],[s10633]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC177-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.12/0.40 % Computer : n002.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Mon Sep 28 08:20:52 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.43 Running first-order model finding
% 0.12/0.43 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
% 25.33/4.09 % (206904)Will run a generic schedule for satisfiability detection.
% 25.33/4.09 % (206913)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2317236934:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 25.33/4.09 % (206910)% WARNING: option uhcvi not known.
% 25.33/4.09 % (206909)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3172897079_2999 on theBenchmark for (2999ds/0Mi)
% 25.33/4.09 % (206910)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=574572786:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 25.33/4.09 % (206911)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3385357257:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 25.33/4.09 % (206912)dis+10_1_sil=32000:sp=arity:random_seed=2105113566:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 25.33/4.09 % (206915)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2905165095:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 25.33/4.09 % (206914)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2626090247:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 25.33/4.09 % TRYING [1]
% 25.33/4.09 % TRYING [2]
% 25.33/4.09 % TRYING [3]
% 25.33/4.09 % (206913)Instruction limit reached!
% 25.33/4.09 % (206913)------------------------------
% 25.33/4.09 % (206913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.33/4.09 % (206913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.33/4.09 % (206913)CaDiCaL version: 2.1.3
% 25.33/4.09 % (206913)Termination reason: Instruction limit
% 25.33/4.09 % (206913)Termination phase: Saturation
% 25.33/4.09 % (206913)Time elapsed: 0.034 s
% 25.33/4.09 % (206913)Peak memory usage: 13 MB
% 25.33/4.09 % (206913)Instructions burned: 119 (million)
% 25.33/4.09 % (206923)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2113008365:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 25.33/4.09 % TRYING [4]
% 25.33/4.09 % TRYING [1]
% 25.33/4.09 % TRYING [2]
% 25.33/4.09 % TRYING [3]
% 25.33/4.09 % (206912)Instruction limit reached!
% 25.33/4.09 % (206912)------------------------------
% 25.33/4.09 % (206912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.33/4.09 % (206912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.33/4.09 % (206912)CaDiCaL version: 2.1.3
% 25.33/4.09 % (206912)Termination reason: Instruction limit
% 25.33/4.09 % (206912)Termination phase: Saturation
% 25.33/4.09 % (206912)Time elapsed: 0.059 s
% 25.33/4.09 % (206912)Peak memory usage: 13 MB
% 25.33/4.09 % (206912)Instructions burned: 103 (million)
% 25.33/4.09 % TRYING [4]
% 25.33/4.09 % (206914)Instruction limit reached!
% 25.33/4.09 % (206914)------------------------------
% 25.33/4.09 % (206914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.33/4.09 % (206914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.33/4.09 % (206914)CaDiCaL version: 2.1.3
% 25.33/4.09 % (206914)Termination reason: Instruction limit
% 25.33/4.09 % (206914)Termination phase: Saturation
% 25.33/4.09 % (206914)Time elapsed: 0.070 s
% 25.33/4.09 % (206914)Peak memory usage: 14 MB
% 25.33/4.09 % (206914)Instructions burned: 131 (million)
% 25.33/4.09 % (206925)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3228636243:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 25.33/4.09 % (206915)Instruction limit reached!
% 25.33/4.09 % (206915)------------------------------
% 25.33/4.09 % (206915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.33/4.09 % (206915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.33/4.09 % (206915)CaDiCaL version: 2.1.3
% 25.33/4.09 % (206915)Termination reason: Instruction limit
% 25.33/4.09 % (206915)Termination phase: Saturation
% 25.33/4.09 % (206915)Time elapsed: 0.088 s
% 25.33/4.09 % (206915)Peak memory usage: 14 MB
% 25.33/4.09 % (206915)Instructions burned: 159 (million)
% 25.33/4.09 % (206926)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=3271789390:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 25.33/4.09 % TRYING [5]
% 25.33/4.09 % TRYING [5]
% 25.33/4.09 % (206928)ott-21_1_sil=16000:fs=off:random_seed=1891242105:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 25.33/4.09 % (206925)Instruction limit reached!
% 25.33/4.09 % (206925)------------------------------
% 25.33/4.09 % (206925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.33/4.09 % (206925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/4.38 % (206925)CaDiCaL version: 2.1.3
% 11.22/4.38 % (206925)Termination reason: Instruction limit
% 11.22/4.38 % (206925)Termination phase: Saturation
% 11.22/4.38 % (206925)Time elapsed: 0.072 s
% 11.22/4.38 % (206925)Peak memory usage: 14 MB
% 11.22/4.38 % (206925)Instructions burned: 131 (million)
% 11.22/4.38 % (206931)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3046026560:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 11.22/4.38 % TRYING [6]
% 11.22/4.38 % (206923)Instruction limit reached!
% 11.22/4.38 % (206923)------------------------------
% 11.22/4.38 % (206923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.22/4.38 % (206923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/4.38 % (206923)CaDiCaL version: 2.1.3
% 11.22/4.38 % (206923)Termination reason: Instruction limit
% 11.22/4.38 % (206923)Termination phase: Finite model building constraint generation
% 11.22/4.38 % (206923)Time elapsed: 0.150 s
% 11.22/4.38 % (206923)Peak memory usage: 34 MB
% 11.22/4.38 % (206923)Instructions burned: 720 (million)
% 11.22/4.38 % (206928)Instruction limit reached!
% 11.22/4.38 % (206928)------------------------------
% 11.22/4.38 % (206928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.22/4.38 % (206928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/4.38 % (206928)CaDiCaL version: 2.1.3
% 11.22/4.38 % (206928)Termination reason: Instruction limit
% 11.22/4.38 % (206928)Termination phase: Saturation
% 11.22/4.38 % (206928)Time elapsed: 0.088 s
% 11.22/4.38 % (206928)Peak memory usage: 13 MB
% 11.22/4.38 % (206928)Instructions burned: 180 (million)
% 11.22/4.38 % (206933)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2981630210:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 11.22/4.38 % TRYING [1]
% 11.22/4.38 % TRYING [2]
% 11.22/4.38 % TRYING [3]
% 11.22/4.38 % (206934)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2932351219:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 11.22/4.38 % TRYING [4]
% 11.22/4.38 % TRYING [6]
% 11.22/4.38 % TRYING [5]
% 11.22/4.38 % (206933)Instruction limit reached!
% 11.22/4.38 % (206933)------------------------------
% 11.22/4.38 % (206933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.22/4.38 % (206933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/4.38 % (206933)CaDiCaL version: 2.1.3
% 11.22/4.38 % (206933)Termination reason: Instruction limit
% 11.22/4.38 % (206933)Termination phase: Finite model building SAT solving
% 11.22/4.38 % (206933)Time elapsed: 0.178 s
% 11.22/4.38 % (206933)Peak memory usage: 22 MB
% 11.22/4.38 % (206933)Instructions burned: 871 (million)
% 11.22/4.38 % (206937)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2923543546:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 11.22/4.38 % TRYING [14]
% 11.22/4.38 % (206926)Instruction limit reached!
% 11.22/4.38 % (206926)------------------------------
% 11.22/4.38 % (206926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.22/4.38 % (206926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/4.38 % (206926)CaDiCaL version: 2.1.3
% 11.22/4.38 % (206926)Termination reason: Instruction limit
% 11.22/4.38 % (206926)Termination phase: Saturation
% 11.22/4.38 % (206926)Time elapsed: 0.392 s
% 11.22/4.38 % (206926)Peak memory usage: 21 MB
% 11.22/4.38 % (206926)Instructions burned: 684 (million)
% 11.22/4.38 % (206931)Instruction limit reached!
% 11.22/4.38 % (206931)------------------------------
% 11.22/4.38 % (206931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.22/4.38 % (206931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/4.38 % (206931)CaDiCaL version: 2.1.3
% 11.22/4.38 % (206931)Termination reason: Instruction limit
% 11.22/4.38 % (206931)Termination phase: Saturation
% 11.22/4.38 % (206931)Time elapsed: 0.317 s
% 11.22/4.38 % (206931)Peak memory usage: 15 MB
% 11.22/4.38 % (206931)Instructions burned: 478 (million)
% 11.22/4.38 % (206939)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=613545159:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 11.22/4.38 % (206940)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=739494192:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 11.22/4.38 % (206937)Instruction limit reached!
% 11.22/4.38 % (206937)------------------------------
% 11.22/4.38 % (206937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.22/4.38 % (206937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/4.38 % (206937)CaDiCaL version: 2.1.3
% 11.22/4.38 % (206937)Termination reason: Instruction limit
% 11.22/4.38 % (206937)Termination phase: Finite model building constraint generation
% 11.22/4.38 % (206937)Time elapsed: 0.179 s
% 11.22/4.38 % (206937)Peak memory usage: 73 MB
% 11.22/4.38 % (206937)Instructions burned: 893 (million)
% 11.22/4.38 % (206943)fmb+10_1_sil=64000:random_seed=1460377436:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 11.22/4.38 % TRYING [1]
% 11.22/4.38 % TRYING [2]
% 11.22/4.38 % TRYING [3]
% 11.22/4.38 % TRYING [4]
% 11.22/4.38 % TRYING [5]
% 11.22/4.38 % TRYING [7]
% 11.22/4.38 % (206939)Instruction limit reached!
% 11.22/4.38 % (206939)------------------------------
% 11.22/4.38 % (206939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.22/4.38 % (206939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/4.38 % (206939)CaDiCaL version: 2.1.3
% 11.22/4.38 % (206939)Termination reason: Instruction limit
% 11.22/4.38 % (206939)Termination phase: Saturation
% 11.22/4.38 % (206939)Time elapsed: 0.353 s
% 11.22/4.38 % (206939)Peak memory usage: 19 MB
% 11.22/4.38 % (206939)Instructions burned: 693 (million)
% 11.22/4.38 % (206945)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=86888785:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 11.22/4.38 % TRYING [20]
% 11.22/4.38 % (206934)Instruction limit reached!
% 11.22/4.38 % (206934)------------------------------
% 11.22/4.38 % (206934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.22/4.38 % (206934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/4.38 % (206934)CaDiCaL version: 2.1.3
% 11.22/4.38 % (206934)Termination reason: Instruction limit
% 11.22/4.38 % (206934)Termination phase: Saturation
% 11.22/4.38 % (206934)Time elapsed: 0.681 s
% 11.22/4.38 % (206934)Peak memory usage: 27 MB
% 11.22/4.38 % (206934)Instructions burned: 1180 (million)
% 11.22/4.38 % (206947)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=857828362:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 11.22/4.38 % TRYING [6]
% 11.22/4.38 % TRYING [8]
% 11.22/4.38 % (206940)Instruction limit reached!
% 11.22/4.38 % (206940)------------------------------
% 11.22/4.38 % (206940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.22/4.38 % (206940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/4.38 % (206940)CaDiCaL version: 2.1.3
% 11.22/4.38 % (206940)Termination reason: Instruction limit
% 11.22/4.38 % (206940)Termination phase: Saturation
% 11.22/4.38 % (206940)Time elapsed: 0.468 s
% 11.22/4.38 % (206940)Peak memory usage: 20 MB
% 11.22/4.38 % (206940)Instructions burned: 879 (million)
% 11.22/4.38 % (206949)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1389124290:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 11.22/4.38 % (206947)Instruction limit reached!
% 11.22/4.38 % (206947)------------------------------
% 11.22/4.38 % (206947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.22/4.38 % (206947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/4.38 % (206947)CaDiCaL version: 2.1.3
% 11.22/4.38 % (206947)Termination reason: Instruction limit
% 11.22/4.38 % (206947)Termination phase: Finite model building constraint generation
% 11.22/4.38 % (206947)Time elapsed: 0.333 s
% 11.22/4.38 % (206947)Peak memory usage: 79 MB
% 11.22/4.38 % (206947)Instructions burned: 923 (million)
% 11.22/4.38 % (206951)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3217941037:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 11.22/4.38 % TRYING [7]
% 11.22/4.38 % TRYING [8]
% 11.22/4.38 % (206951)Instruction limit reached!
% 11.22/4.38 % (206951)------------------------------
% 11.22/4.38 % (206951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.22/4.38 % (206951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/4.38 % (206951)CaDiCaL version: 2.1.3
% 11.22/4.38 % (206951)Termination reason: Instruction limit
% 11.22/4.38 % (206951)Termination phase: Saturation
% 11.22/4.38 % (206951)Time elapsed: 0.661 s
% 11.22/4.38 % (206951)Peak memory usage: 16 MB
% 11.22/4.38 % (206951)Instructions burned: 1473 (million)
% 11.22/4.38 % (206953)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=534311186:i=6324_2980 on theBenchmark for (2980ds/6324Mi)
% 11.22/4.38 % TRYING [77]
% 11.22/4.38 % TRYING [8]
% 11.22/4.38 % (206949)Instruction limit reached!
% 11.22/4.38 % (206949)------------------------------
% 11.22/4.38 % (206949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.22/4.38 % (206949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/4.38 % (206949)CaDiCaL version: 2.1.3
% 11.22/4.38 % (206949)Termination reason: Instruction limit
% 11.22/4.38 % (206949)Termination phase: Saturation
% 11.22/4.38 % (206949)Time elapsed: 2.607 s
% 11.22/4.38 % (206949)Peak memory usage: 55 MB
% 11.22/4.38 % (206949)Instructions burned: 5131 (million)
% 11.22/4.38 % (206955)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1097695154:fmbsr=2.30978:i=2174_2963 on theBenchmark for (2963ds/2174Mi)
% 11.22/4.38 % TRYING [16]
% 11.22/4.38 % (206910) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-206904-206910"...
% 11.22/4.38 % (206910)...printing done.
% 11.22/4.38 % (206910)Refutation found. Thanks to Tanya!
% 11.22/4.38 % SZS status Unsatisfiable for theBenchmark
% 11.22/4.38 % SZS output start Proof for theBenchmark
% See solution above
% 11.22/4.39 % (206910)------------------------------
% 11.22/4.39 % (206910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.22/4.39 % (206910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.22/4.39 % (206910)CaDiCaL version: 2.1.3
% 11.22/4.39 % (206910)Termination reason: Refutation
% 11.22/4.39 % (206910)Time elapsed: 3.796 s
% 11.22/4.39 % (206910)Peak memory usage: 80 MB
% 11.22/4.39 % (206910)Instructions burned: 7101 (million)
% 11.22/4.39 % (206904)Success in time 3.939 s
% 11.22/4.39 % Vampire exiting
%------------------------------------------------------------------------------