%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC172-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 : n005.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:57 PM UTC 2026
% Result : Unsatisfiable 30.79s 4.97s
% Output : Refutation 30.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 63
% Syntax : Number of formulae : 344 ( 51 unt; 28 def)
% Number of atoms : 1173 ( 103 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 1271 ( 442 ~; 801 |; 0 &)
% ( 28 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 39 ( 37 usr; 29 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-2 aty)
% Number of variables : 196 ( 0 sgn 196 !; 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(f60,axiom,
! [X0] :
( ~ ssList(X0)
| frontsegP(X0,nil) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause60) ).
fof(f63,axiom,
! [X0] :
( ~ lt(X0,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause63) ).
fof(f68,axiom,
! [X0] :
( ~ ssItem(X0)
| strictorderP(cons(X0,nil)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause68) ).
fof(f72,axiom,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause72) ).
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(f100,axiom,
! [X0,X1] :
( cons(X0,X1) != X1
| ~ ssItem(X0)
| ~ ssList(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause99) ).
fof(f103,axiom,
! [X0] :
( ~ singletonP(X0)
| ~ ssList(X0)
| cons(skaf44(X0),nil) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause101) ).
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(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(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(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(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(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(f197,axiom,
! [X2,X3,X0,X1,X4,X5] :
( app(app(X0,cons(X1,X2)),cons(X3,X4)) != X5
| ~ ssList(X4)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X1)
| ~ strictorderP(X5)
| ~ ssList(X5)
| lt(X1,X3)
| lt(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause183) ).
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(f219,negated_conjecture,
( cons(sk9,nil) = sk3
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_18) ).
fof(f220,plain,
( sk3 = cons(sk9,nil)
| nil = sk3 ),
inference(reorient_equations,[],[f219]) ).
fof(f223,plain,
ssList(sk3),
inference(definition_unfolding,[],[f200,f205]) ).
fof(f225,plain,
sk3 = app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8),
inference(definition_unfolding,[],[f211,f205]) ).
fof(f233,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(cons(X0,nil))
| singletonP(cons(X0,nil)) ),
inference(equality_resolution,[],[f119]) ).
fof(f237,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1))
| frontsegP(app(X0,X1),X0) ),
inference(equality_resolution,[],[f155]) ).
fof(f240,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(f242,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(f243,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] :
( ~ ssList(X4)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X1)
| ~ strictorderP(app(app(X0,cons(X1,X2)),cons(X3,X4)))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X3,X4)))
| lt(X1,X3)
| lt(X3,X1) ),
inference(equality_resolution,[],[f197]) ).
fof(f252,plain,
~ ssList(nil),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f302,plain,
! [X0] :
( ~ frontsegP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f305,plain,
! [X0] :
( ~ lt(X0,X0)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f63]) ).
fof(f310,plain,
! [X0] :
( ~ strictorderP(cons(X0,nil))
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f68]) ).
fof(f314,plain,
! [X0,X1] :
( ssList(X0)
| ~ duplicatefreeP(X0)
| ~ ssItem(X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f316,plain,
! [X0] :
( ssList(X0)
| app(nil,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f317,plain,
! [X0] :
( ~ ssList(tl(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f322,plain,
! [X0] :
( segmentP(nil,X0)
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f327,plain,
! [X0,X1] :
( ~ ssList(app(X1,X0))
| ssList(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f328,plain,
! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f341,plain,
! [X0,X1] :
( cons(X0,X1) != X1
| ssItem(X0)
| ssList(X1) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f343,plain,
! [X0] :
( ~ singletonP(X0)
| ssList(X0)
| cons(skaf44(X0),nil) = X0 ),
inference(consistent_polarity_flipping,[],[f103]) ).
fof(f344,plain,
! [X0,X1] :
( neq(X1,X0)
| ssItem(X1)
| ssItem(X0)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f105]) ).
fof(f346,plain,
! [X0] :
( ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f358,plain,
! [X0] :
( singletonP(cons(X0,nil))
| ssList(cons(X0,nil))
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f233]) ).
fof(f362,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f371,plain,
! [X0,X1] :
( frontsegP(X0,X1)
| frontsegP(X1,X0)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f379,plain,
! [X2,X0,X1] :
( ~ frontsegP(app(X0,X2),X1)
| ssList(X2)
| ssList(X1)
| ssList(X0)
| frontsegP(X0,X1) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f386,plain,
! [X0,X1] :
( ssList(X1)
| ssList(X0)
| ssList(app(X0,X1))
| ~ frontsegP(app(X0,X1),X0) ),
inference(consistent_polarity_flipping,[],[f237]) ).
fof(f415,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,[],[f240]) ).
fof(f418,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(f420,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,[],[f242]) ).
fof(f421,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,[],[f243]) ).
fof(f425,plain,
! [X2,X3,X0,X1,X4] :
( strictorderP(app(app(X0,cons(X1,X2)),cons(X3,X4)))
| ssList(X2)
| ssList(X0)
| ssItem(X3)
| ssItem(X1)
| ssList(X4)
| ssList(app(app(X0,cons(X1,X2)),cons(X3,X4)))
| lt(X1,X3)
| lt(X3,X1) ),
inference(consistent_polarity_flipping,[],[f247]) ).
fof(f428,plain,
~ ssList(sk3),
inference(consistent_polarity_flipping,[],[f223]) ).
fof(f432,plain,
~ ssItem(sk5),
inference(consistent_polarity_flipping,[],[f206]) ).
fof(f433,plain,
~ ssItem(sk6),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f434,plain,
~ ssList(sk7),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f435,plain,
~ ssList(sk8),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f437,plain,
( ~ ssItem(sk9)
| nil = sk3 ),
inference(consistent_polarity_flipping,[],[f214]) ).
fof(f442,plain,
! [X3,X0,X1] :
( ~ frontsegP(cons(X3,X0),cons(X3,X1))
| ssList(X1)
| ssList(X0)
| ssItem(X3)
| frontsegP(X0,X1) ),
inference(duplicate_literal_removal,[],[f420]) ).
fof(f449,definition,
( spl0_1
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f451,plain,
( nil = sk3
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f449]) ).
fof(f462,definition,
( spl0_4
<=> sk3 = cons(sk9,nil) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f464,plain,
( sk3 = cons(sk9,nil)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f462]) ).
fof(f465,plain,
( spl0_1
| spl0_4 ),
inference(avatar_split_clause,[],[f220,f462,f449]) ).
fof(f474,definition,
( spl0_6
<=> ssItem(sk9) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f476,plain,
( ~ ssItem(sk9)
| spl0_6 ),
inference(avatar_component_clause,[],[f474]) ).
fof(f477,plain,
( spl0_1
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f437,f474,f449]) ).
fof(f484,definition,
( spl0_8
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f485,plain,
( ~ ssList(nil)
| spl0_8 ),
inference(avatar_component_clause,[],[f484]) ).
fof(f512,definition,
( spl0_14
<=> ! [X1] : ~ ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f513,plain,
( ! [X1] : ~ ssItem(X1)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f515,definition,
( spl0_15
<=> ! [X0] :
( ssList(X0)
| ~ duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f516,plain,
( ! [X0] :
( ~ duplicatefreeP(X0)
| ssList(X0) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f515]) ).
fof(f517,plain,
( spl0_14
| spl0_15 ),
inference(avatar_split_clause,[],[f314,f515,f512]) ).
fof(f520,plain,
~ spl0_8,
inference(avatar_split_clause,[],[f252,f484]) ).
fof(f525,plain,
( ! [X0] : ~ lt(X0,X0)
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f305,f513]) ).
fof(f602,plain,
sk3 = app(nil,sk3),
inference(resolution,[],[f316,f428]) ).
fof(f636,plain,
( ! [X0,X1] :
( cons(X0,X1) != X1
| ssList(X1) )
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f341,f513]) ).
fof(f717,definition,
( spl0_16
<=> sk5 = sk6 ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f719,plain,
( sk5 = sk6
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f717]) ).
fof(f755,plain,
( ! [X0] :
( singletonP(cons(X0,nil))
| ssList(cons(X0,nil)) )
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f358,f513]) ).
fof(f756,plain,
( ! [X0] :
( ssList(cons(X0,nil))
| ssList(cons(X0,nil))
| cons(X0,nil) = cons(skaf44(cons(X0,nil)),nil) )
| ~ spl0_14 ),
inference(resolution,[],[f755,f343]) ).
fof(f758,plain,
( ! [X0] :
( ssList(cons(X0,nil))
| cons(X0,nil) = cons(skaf44(cons(X0,nil)),nil) )
| ~ spl0_14 ),
inference(duplicate_literal_removal,[],[f756]) ).
fof(f805,definition,
( spl0_21
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f806,plain,
( nil != sk7
| spl0_21 ),
inference(avatar_component_clause,[],[f805]) ).
fof(f807,plain,
( nil = sk7
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f805]) ).
fof(f809,definition,
( spl0_22
<=> sk7 = cons(hd(sk7),tl(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f811,plain,
( sk7 = cons(hd(sk7),tl(sk7))
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f809]) ).
fof(f859,plain,
( ~ strictorderP(sk3)
| ssItem(sk9)
| ~ spl0_4 ),
inference(superposition,[],[f310,f464]) ).
fof(f860,plain,
( ~ strictorderP(sk3)
| ~ spl0_4
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f859,f476]) ).
fof(f1029,plain,
( ssItem(sk5)
| ssItem(sk6)
| sk5 = sk6 ),
inference(resolution,[],[f344,f212]) ).
fof(f1113,plain,
( ! [X0] :
( ssList(X0)
| cons(sk9,X0) = app(cons(sk9,nil),X0) )
| spl0_6 ),
inference(resolution,[],[f362,f476]) ).
fof(f1144,plain,
( ! [X0] :
( ssList(X0)
| cons(sk9,X0) = app(sk3,X0) )
| ~ spl0_4
| spl0_6 ),
inference(forward_demodulation,[],[f1113,f464]) ).
fof(f1202,definition,
( spl0_39
<=> ssList(app(app(nil,cons(sk5,nil)),cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f1203,plain,
( ~ ssList(app(app(nil,cons(sk5,nil)),cons(sk5,nil)))
| spl0_39 ),
inference(avatar_component_clause,[],[f1202]) ).
fof(f1204,plain,
( ssList(app(app(nil,cons(sk5,nil)),cons(sk5,nil)))
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f1202]) ).
fof(f1311,plain,
! [X0,X1] :
( ~ frontsegP(app(X0,X1),X0)
| ssList(X0)
| ssList(X1) ),
inference(forward_subsumption_resolution,[],[f386,f327]) ).
fof(f1313,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| frontsegP(X0,app(X0,X1))
| ssList(app(X0,X1))
| ssList(X0)
| app(X0,X1) = X0 ),
inference(resolution,[],[f1311,f371]) ).
fof(f1317,plain,
( ~ frontsegP(sk3,app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ssList(sk8) ),
inference(superposition,[],[f1311,f225]) ).
fof(f1321,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| frontsegP(X0,app(X0,X1))
| ssList(app(X0,X1))
| app(X0,X1) = X0 ),
inference(duplicate_literal_removal,[],[f1313]) ).
fof(f1323,plain,
( ~ frontsegP(sk3,app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
inference(forward_subsumption_resolution,[],[f1317,f435]) ).
fof(f1324,plain,
! [X0,X1] :
( frontsegP(X0,app(X0,X1))
| ssList(X1)
| ssList(X0)
| app(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f1321,f327]) ).
fof(f1467,plain,
! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(X2)
| frontsegP(X2,X1)
| frontsegP(X1,app(X2,X0))
| ssList(app(X2,X0))
| ssList(X1)
| app(X2,X0) = X1 ),
inference(resolution,[],[f379,f371]) ).
fof(f1471,plain,
! [X0] :
( ~ frontsegP(sk3,X0)
| ssList(sk8)
| ssList(X0)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| frontsegP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0) ),
inference(superposition,[],[f379,f225]) ).
fof(f1475,plain,
! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(X2)
| frontsegP(X2,X1)
| frontsegP(X1,app(X2,X0))
| ssList(app(X2,X0))
| app(X2,X0) = X1 ),
inference(duplicate_literal_removal,[],[f1467]) ).
fof(f1478,plain,
! [X0] :
( ~ frontsegP(sk3,X0)
| ssList(X0)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| frontsegP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0) ),
inference(forward_subsumption_resolution,[],[f1471,f435]) ).
fof(f1481,plain,
! [X2,X0,X1] :
( frontsegP(X1,app(X2,X0))
| ssList(X1)
| ssList(X2)
| frontsegP(X2,X1)
| ssList(X0)
| app(X2,X0) = X1 ),
inference(forward_subsumption_resolution,[],[f1475,f327]) ).
fof(f2203,definition,
( spl0_50
<=> ssList(app(nil,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f2204,plain,
( ~ ssList(app(nil,cons(sk5,nil)))
| spl0_50 ),
inference(avatar_component_clause,[],[f2203]) ).
fof(f2205,plain,
( ssList(app(nil,cons(sk5,nil)))
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f2203]) ).
fof(f2207,definition,
( spl0_51
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f2208,plain,
( ~ ssList(cons(sk5,nil))
| spl0_51 ),
inference(avatar_component_clause,[],[f2207]) ).
fof(f2209,plain,
( ssList(cons(sk5,nil))
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f2207]) ).
fof(f2254,plain,
( ~ segmentP(sk3,cons(sk6,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| ssList(sk3)
| ssList(sk8) ),
inference(superposition,[],[f415,f225]) ).
fof(f2259,plain,
( ~ segmentP(sk3,cons(sk6,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| ssList(sk8) ),
inference(forward_subsumption_resolution,[],[f2254,f428]) ).
fof(f2263,plain,
( ~ segmentP(sk3,cons(sk6,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil)) ),
inference(forward_subsumption_resolution,[],[f2259,f435]) ).
fof(f2267,plain,
( ~ segmentP(sk3,cons(sk5,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2263,f719]) ).
fof(f2270,plain,
( ~ segmentP(nil,cons(sk5,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| ~ spl0_1
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2267,f451]) ).
fof(f2276,definition,
( spl0_54
<=> segmentP(nil,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f2277,plain,
( segmentP(nil,cons(sk5,nil))
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f2276]) ).
fof(f2278,plain,
( ~ segmentP(nil,cons(sk5,nil))
| spl0_54 ),
inference(avatar_component_clause,[],[f2276]) ).
fof(f2284,definition,
( spl0_55
<=> nil = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f2286,plain,
( nil = cons(sk5,nil)
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f2284]) ).
fof(f2299,plain,
( ssList(nil)
| ssList(cons(sk5,nil))
| ~ spl0_50 ),
inference(resolution,[],[f2205,f327]) ).
fof(f2300,plain,
( ssList(cons(sk5,nil))
| spl0_8
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f2299,f485]) ).
fof(f2301,plain,
( spl0_51
| spl0_8
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f2300,f2203,f484,f2207]) ).
fof(f2304,plain,
( ssItem(sk6)
| sk5 = sk6 ),
inference(forward_subsumption_resolution,[],[f1029,f432]) ).
fof(f2326,plain,
sk5 = sk6,
inference(forward_subsumption_resolution,[],[f2304,f433]) ).
fof(f2339,plain,
spl0_16,
inference(avatar_split_clause,[],[f2326,f717]) ).
fof(f2390,definition,
( spl0_68
<=> ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f2392,plain,
( ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ spl0_68 ),
inference(avatar_component_clause,[],[f2390]) ).
fof(f2406,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| ~ spl0_1
| ~ spl0_16
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f2270,f2277]) ).
fof(f2424,definition,
( spl0_74
<=> ssList(app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f2425,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| spl0_74 ),
inference(avatar_component_clause,[],[f2424]) ).
fof(f2426,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_74 ),
inference(avatar_component_clause,[],[f2424]) ).
fof(f2649,plain,
( ! [X2,X3,X0,X1] :
( ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(X2)
| ssList(X0)
| ssItem(X1)
| ssList(X3) )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f421,f516]) ).
fof(f2717,plain,
( ssList(nil)
| ssItem(sk5)
| ~ spl0_51 ),
inference(resolution,[],[f2209,f328]) ).
fof(f2718,plain,
( ssItem(sk5)
| spl0_8
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f2717,f485]) ).
fof(f2719,plain,
( $false
| spl0_8
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f2718,f432]) ).
fof(f2720,plain,
( spl0_8
| ~ spl0_51 ),
inference(avatar_contradiction_clause,[],[f2719]) ).
fof(f2741,plain,
( cons(sk5,nil) = app(nil,cons(sk5,nil))
| spl0_51 ),
inference(resolution,[],[f2208,f316]) ).
fof(f2834,plain,
( ssList(cons(sk5,nil))
| nil = cons(sk5,nil)
| spl0_54 ),
inference(resolution,[],[f2278,f322]) ).
fof(f2837,plain,
( nil = cons(sk5,nil)
| spl0_51
| spl0_54 ),
inference(forward_subsumption_resolution,[],[f2834,f2208]) ).
fof(f2839,plain,
( spl0_55
| spl0_51
| spl0_54 ),
inference(avatar_split_clause,[],[f2837,f2276,f2207,f2284]) ).
fof(f2891,plain,
( singletonP(nil)
| ssList(nil)
| ssItem(sk5)
| ~ spl0_55 ),
inference(superposition,[],[f358,f2286]) ).
fof(f2940,plain,
( ssList(nil)
| ssItem(sk5)
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f2891,f11]) ).
fof(f2966,plain,
( ssItem(sk5)
| spl0_8
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f2940,f485]) ).
fof(f2971,plain,
( $false
| spl0_8
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f2966,f432]) ).
fof(f2972,plain,
( spl0_8
| ~ spl0_55 ),
inference(avatar_contradiction_clause,[],[f2971]) ).
fof(f2979,plain,
( ssList(cons(sk5,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_1
| ~ spl0_16
| ~ spl0_54 ),
inference(forward_demodulation,[],[f2406,f719]) ).
fof(f2983,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_1
| ~ spl0_16
| spl0_51
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f2979,f2208]) ).
fof(f2985,plain,
( spl0_74
| ~ spl0_1
| ~ spl0_16
| spl0_51
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f2983,f2276,f2207,f717,f449,f2424]) ).
fof(f2989,plain,
( ssList(sk7)
| ssList(cons(sk5,nil))
| ~ spl0_74 ),
inference(resolution,[],[f2426,f327]) ).
fof(f2990,plain,
( ssList(cons(sk5,nil))
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f2989,f434]) ).
fof(f2991,plain,
( $false
| spl0_51
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f2990,f2208]) ).
fof(f2992,plain,
( spl0_51
| ~ spl0_74 ),
inference(avatar_contradiction_clause,[],[f2991]) ).
fof(f3128,plain,
( ! [X0] :
( ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ frontsegP(sk3,X0)
| ssList(X0)
| frontsegP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0) )
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1478,f719]) ).
fof(f3144,plain,
( ~ frontsegP(sk3,app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1323,f719]) ).
fof(f3161,plain,
( ! [X0] :
( frontsegP(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),X0)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ frontsegP(sk3,X0)
| ssList(X0) )
| ~ spl0_16 ),
inference(forward_demodulation,[],[f3128,f719]) ).
fof(f3174,definition,
( spl0_133
<=> frontsegP(sk3,app(app(sk7,cons(sk5,nil)),cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f3176,plain,
( ~ frontsegP(sk3,app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| spl0_133 ),
inference(avatar_component_clause,[],[f3174]) ).
fof(f3181,plain,
( ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ frontsegP(sk3,app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ spl0_16 ),
inference(forward_demodulation,[],[f3144,f719]) ).
fof(f3199,definition,
( spl0_136
<=> ! [X0] :
( frontsegP(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),X0)
| ssList(X0)
| ~ frontsegP(sk3,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f3200,plain,
( ! [X0] :
( frontsegP(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),X0)
| ssList(X0)
| ~ frontsegP(sk3,X0) )
| ~ spl0_136 ),
inference(avatar_component_clause,[],[f3199]) ).
fof(f3201,plain,
( spl0_68
| spl0_136
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f3161,f717,f3199,f2390]) ).
fof(f3223,plain,
( ~ spl0_133
| spl0_68
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f3181,f717,f2390,f3174]) ).
fof(f3275,plain,
( ! [X0] :
( ~ frontsegP(cons(sk9,X0),sk3)
| ssList(nil)
| ssList(X0)
| ssItem(sk9)
| frontsegP(X0,nil) )
| ~ spl0_4 ),
inference(superposition,[],[f442,f464]) ).
fof(f3284,plain,
( ! [X0] :
( ~ frontsegP(cons(sk9,X0),sk3)
| ssList(X0)
| ssItem(sk9)
| frontsegP(X0,nil) )
| ~ spl0_4
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f3275,f485]) ).
fof(f3313,plain,
( ! [X0] :
( ~ frontsegP(cons(sk9,X0),sk3)
| ssList(X0)
| frontsegP(X0,nil) )
| ~ spl0_4
| spl0_6
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f3284,f476]) ).
fof(f3331,plain,
( ! [X0] :
( ~ frontsegP(cons(sk9,X0),sk3)
| ssList(X0) )
| ~ spl0_4
| spl0_6
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f3313,f302]) ).
fof(f3415,definition,
( spl0_148
<=> ssList(tl(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f3417,plain,
( ssList(tl(sk7))
| ~ spl0_148 ),
inference(avatar_component_clause,[],[f3415]) ).
fof(f3804,plain,
( ! [X2,X3,X0,X1] :
( frontsegP(cons(X0,X1),cons(X2,X3))
| ssList(X3)
| ssList(X1)
| ssItem(X2)
| X0 = X2 )
| ~ spl0_14 ),
inference(backward_subsumption_resolution,[],[f418,f513]) ).
fof(f3808,plain,
( ! [X2,X3,X0,X1,X4] :
( strictorderP(app(app(X0,cons(X1,X2)),cons(X3,X4)))
| ssList(X2)
| ssList(X0)
| ssItem(X3)
| ssList(X4)
| ssList(app(app(X0,cons(X1,X2)),cons(X3,X4)))
| lt(X1,X3)
| lt(X3,X1) )
| ~ spl0_14 ),
inference(backward_subsumption_resolution,[],[f425,f513]) ).
fof(f3840,plain,
( ! [X2,X3,X0,X1] :
( frontsegP(cons(X0,X1),cons(X2,X3))
| ssList(X3)
| ssList(X1)
| X0 = X2 )
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f3804,f513]) ).
fof(f3844,plain,
( ! [X2,X3,X0,X1,X4] :
( strictorderP(app(app(X0,cons(X1,X2)),cons(X3,X4)))
| ssList(X2)
| ssList(X0)
| ssList(X4)
| ssList(app(app(X0,cons(X1,X2)),cons(X3,X4)))
| lt(X1,X3)
| lt(X3,X1) )
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f3808,f513]) ).
fof(f4329,plain,
( ! [X0,X1] :
( frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| ssList(nil)
| sk9 = X0 )
| ~ spl0_4
| ~ spl0_14 ),
inference(superposition,[],[f3840,f464]) ).
fof(f4344,plain,
( ! [X0,X1] :
( frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| sk9 = X0 )
| ~ spl0_4
| spl0_8
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f4329,f485]) ).
fof(f6246,plain,
( cons(sk9,sk3) = app(sk3,sk3)
| ~ spl0_4
| spl0_6 ),
inference(resolution,[],[f1144,f428]) ).
fof(f6428,plain,
( ssList(app(nil,cons(sk5,nil)))
| ssList(cons(sk5,nil))
| ~ spl0_39 ),
inference(resolution,[],[f1204,f327]) ).
fof(f6429,plain,
( ssList(cons(sk5,nil))
| ~ spl0_39
| spl0_50 ),
inference(forward_subsumption_resolution,[],[f6428,f2204]) ).
fof(f6430,plain,
( $false
| ~ spl0_39
| spl0_50
| spl0_51 ),
inference(forward_subsumption_resolution,[],[f6429,f2208]) ).
fof(f6431,plain,
( ~ spl0_39
| spl0_50
| spl0_51 ),
inference(avatar_contradiction_clause,[],[f6430]) ).
fof(f6432,plain,
( ssList(nil)
| ssList(nil)
| ssItem(sk5)
| ssList(nil)
| ~ spl0_15
| spl0_39 ),
inference(resolution,[],[f1203,f2649]) ).
fof(f6457,plain,
( ssList(nil)
| ssItem(sk5)
| ~ spl0_15
| spl0_39 ),
inference(duplicate_literal_removal,[],[f6432]) ).
fof(f6477,plain,
( ssItem(sk5)
| spl0_8
| ~ spl0_15
| spl0_39 ),
inference(forward_subsumption_resolution,[],[f6457,f485]) ).
fof(f6478,plain,
( $false
| spl0_8
| ~ spl0_15
| spl0_39 ),
inference(forward_subsumption_resolution,[],[f6477,f432]) ).
fof(f6479,plain,
( spl0_8
| ~ spl0_15
| spl0_39 ),
inference(avatar_contradiction_clause,[],[f6478]) ).
fof(f8051,plain,
( ssList(sk7)
| nil = sk7
| ~ spl0_148 ),
inference(resolution,[],[f3417,f317]) ).
fof(f8052,plain,
( nil = sk7
| ~ spl0_148 ),
inference(forward_subsumption_resolution,[],[f8051,f434]) ).
fof(f8133,plain,
( spl0_21
| ~ spl0_148 ),
inference(avatar_split_clause,[],[f8052,f3415,f805]) ).
fof(f24236,plain,
( cons(sk5,nil) = cons(skaf44(cons(sk5,nil)),nil)
| ~ spl0_14
| spl0_51 ),
inference(resolution,[],[f758,f2208]) ).
fof(f27153,plain,
( frontsegP(sk3,cons(sk9,sk3))
| ssList(sk3)
| ssList(sk3)
| sk3 = cons(sk9,sk3)
| ~ spl0_4
| spl0_6 ),
inference(superposition,[],[f1324,f6246]) ).
fof(f27155,plain,
( frontsegP(sk3,cons(sk9,sk3))
| ssList(sk3)
| sk3 = cons(sk9,sk3)
| ~ spl0_4
| spl0_6 ),
inference(duplicate_literal_removal,[],[f27153]) ).
fof(f73362,definition,
( spl0_1267
<=> sk3 = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[spl0_1267])],[avatar_definition]) ).
fof(f73364,plain,
( sk3 = cons(sk5,nil)
| ~ spl0_1267 ),
inference(avatar_component_clause,[],[f73362]) ).
fof(f98806,plain,
( frontsegP(sk3,cons(sk5,nil))
| ssList(nil)
| sk9 = skaf44(cons(sk5,nil))
| ~ spl0_4
| spl0_8
| ~ spl0_14
| spl0_51 ),
inference(superposition,[],[f4344,f24236]) ).
fof(f98865,plain,
( frontsegP(sk3,cons(sk5,nil))
| sk9 = skaf44(cons(sk5,nil))
| ~ spl0_4
| spl0_8
| ~ spl0_14
| spl0_51 ),
inference(forward_subsumption_resolution,[],[f98806,f485]) ).
fof(f98965,definition,
( spl0_2212
<=> sk9 = skaf44(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_2212])],[avatar_definition]) ).
fof(f98967,plain,
( sk9 = skaf44(cons(sk5,nil))
| ~ spl0_2212 ),
inference(avatar_component_clause,[],[f98965]) ).
fof(f98969,definition,
( spl0_2213
<=> frontsegP(sk3,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_2213])],[avatar_definition]) ).
fof(f98972,plain,
( spl0_2212
| spl0_2213
| ~ spl0_4
| spl0_8
| ~ spl0_14
| spl0_51 ),
inference(avatar_split_clause,[],[f98865,f2207,f512,f484,f462,f98969,f98965]) ).
fof(f99408,plain,
( cons(sk5,nil) = cons(sk9,nil)
| ~ spl0_14
| spl0_51
| ~ spl0_2212 ),
inference(superposition,[],[f24236,f98967]) ).
fof(f99410,plain,
( sk3 = cons(sk5,nil)
| ~ spl0_4
| ~ spl0_14
| spl0_51
| ~ spl0_2212 ),
inference(forward_demodulation,[],[f99408,f464]) ).
fof(f99415,plain,
( spl0_1267
| ~ spl0_4
| ~ spl0_14
| spl0_51
| ~ spl0_2212 ),
inference(avatar_split_clause,[],[f99410,f98965,f2207,f512,f462,f73362]) ).
fof(f106834,plain,
( frontsegP(sk3,cons(sk9,sk3))
| ssList(sk3)
| ~ spl0_4
| spl0_6
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f27155,f636]) ).
fof(f106924,plain,
( frontsegP(sk3,cons(sk9,sk3))
| ~ spl0_4
| spl0_6
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f106834,f428]) ).
fof(f107252,definition,
( spl0_2438
<=> ssList(sk7) ),
introduced(definition,[new_symbols(definition,[spl0_2438])],[avatar_definition]) ).
fof(f107253,plain,
( ~ ssList(sk7)
| spl0_2438 ),
inference(avatar_component_clause,[],[f107252]) ).
fof(f107741,definition,
( spl0_2471
<=> sk3 = app(app(sk7,cons(sk5,nil)),cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_2471])],[avatar_definition]) ).
fof(f107743,plain,
( sk3 = app(app(sk7,cons(sk5,nil)),cons(sk5,nil))
| ~ spl0_2471 ),
inference(avatar_component_clause,[],[f107741]) ).
fof(f107786,plain,
~ spl0_2438,
inference(avatar_split_clause,[],[f434,f107252]) ).
fof(f107834,plain,
( sk7 = cons(hd(sk7),tl(sk7))
| nil = sk7
| spl0_2438 ),
inference(resolution,[],[f107253,f346]) ).
fof(f108445,plain,
( sk7 = cons(hd(sk7),tl(sk7))
| spl0_21
| spl0_2438 ),
inference(forward_subsumption_resolution,[],[f107834,f806]) ).
fof(f108472,plain,
( spl0_22
| spl0_21
| spl0_2438 ),
inference(avatar_split_clause,[],[f108445,f107252,f805,f809]) ).
fof(f110552,definition,
( spl0_2659
<=> sk9 = hd(sk7) ),
introduced(definition,[new_symbols(definition,[spl0_2659])],[avatar_definition]) ).
fof(f110554,plain,
( sk9 = hd(sk7)
| ~ spl0_2659 ),
inference(avatar_component_clause,[],[f110552]) ).
fof(f110556,definition,
( spl0_2660
<=> frontsegP(sk3,sk7) ),
introduced(definition,[new_symbols(definition,[spl0_2660])],[avatar_definition]) ).
fof(f110566,definition,
( spl0_2662
<=> frontsegP(sk7,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_2662])],[avatar_definition]) ).
fof(f112224,plain,
( ssList(sk3)
| ssList(app(sk7,cons(sk5,nil)))
| frontsegP(app(sk7,cons(sk5,nil)),sk3)
| ssList(cons(sk5,nil))
| sk3 = app(app(sk7,cons(sk5,nil)),cons(sk5,nil))
| spl0_133 ),
inference(resolution,[],[f3176,f1481]) ).
fof(f112234,plain,
( ssList(app(sk7,cons(sk5,nil)))
| frontsegP(app(sk7,cons(sk5,nil)),sk3)
| ssList(cons(sk5,nil))
| sk3 = app(app(sk7,cons(sk5,nil)),cons(sk5,nil))
| spl0_133 ),
inference(forward_subsumption_resolution,[],[f112224,f428]) ).
fof(f112239,plain,
( frontsegP(app(sk7,cons(sk5,nil)),sk3)
| ssList(cons(sk5,nil))
| sk3 = app(app(sk7,cons(sk5,nil)),cons(sk5,nil))
| spl0_74
| spl0_133 ),
inference(forward_subsumption_resolution,[],[f112234,f2425]) ).
fof(f112240,plain,
( frontsegP(app(sk7,cons(sk5,nil)),sk3)
| sk3 = app(app(sk7,cons(sk5,nil)),cons(sk5,nil))
| spl0_51
| spl0_74
| spl0_133 ),
inference(forward_subsumption_resolution,[],[f112239,f2208]) ).
fof(f112242,definition,
( spl0_2765
<=> frontsegP(app(sk7,cons(sk5,nil)),sk3) ),
introduced(definition,[new_symbols(definition,[spl0_2765])],[avatar_definition]) ).
fof(f112244,plain,
( frontsegP(app(sk7,cons(sk5,nil)),sk3)
| ~ spl0_2765 ),
inference(avatar_component_clause,[],[f112242]) ).
fof(f112245,plain,
( spl0_2471
| spl0_2765
| spl0_51
| spl0_74
| spl0_133 ),
inference(avatar_split_clause,[],[f112240,f3174,f2424,f2207,f112242,f107741]) ).
fof(f113292,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk5,nil))
| ~ spl0_136 ),
inference(resolution,[],[f3200,f1311]) ).
fof(f113296,plain,
( ! [X0] :
( ssList(X0)
| ~ frontsegP(sk3,X0)
| ssList(cons(sk5,nil))
| ssList(X0)
| ssList(app(sk7,cons(sk5,nil)))
| frontsegP(app(sk7,cons(sk5,nil)),X0) )
| ~ spl0_136 ),
inference(resolution,[],[f3200,f379]) ).
fof(f113298,plain,
( ! [X0] :
( ssList(X0)
| ~ frontsegP(sk3,X0)
| ssList(cons(sk5,nil))
| ssList(app(sk7,cons(sk5,nil)))
| frontsegP(app(sk7,cons(sk5,nil)),X0) )
| ~ spl0_136 ),
inference(duplicate_literal_removal,[],[f113296]) ).
fof(f113302,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ssList(cons(sk5,nil))
| ~ spl0_136 ),
inference(duplicate_literal_removal,[],[f113292]) ).
fof(f113303,plain,
( ! [X0] :
( ssList(X0)
| ~ frontsegP(sk3,X0)
| ssList(app(sk7,cons(sk5,nil)))
| frontsegP(app(sk7,cons(sk5,nil)),X0) )
| spl0_51
| ~ spl0_136 ),
inference(forward_subsumption_resolution,[],[f113298,f2208]) ).
fof(f113306,plain,
( ~ frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ssList(cons(sk5,nil))
| spl0_74
| ~ spl0_136 ),
inference(forward_subsumption_resolution,[],[f113302,f2425]) ).
fof(f113307,plain,
( ! [X0] :
( frontsegP(app(sk7,cons(sk5,nil)),X0)
| ~ frontsegP(sk3,X0)
| ssList(X0) )
| spl0_51
| spl0_74
| ~ spl0_136 ),
inference(forward_subsumption_resolution,[],[f113303,f2425]) ).
fof(f113308,plain,
( ~ frontsegP(sk3,app(sk7,cons(sk5,nil)))
| spl0_51
| spl0_74
| ~ spl0_136 ),
inference(forward_subsumption_resolution,[],[f113306,f2208]) ).
fof(f113458,plain,
( sk7 = cons(sk9,tl(sk7))
| ~ spl0_22
| ~ spl0_2659 ),
inference(forward_demodulation,[],[f811,f110554]) ).
fof(f113487,plain,
( ~ frontsegP(sk7,sk3)
| ssList(tl(sk7))
| ~ spl0_4
| spl0_6
| spl0_8
| ~ spl0_22
| ~ spl0_2659 ),
inference(superposition,[],[f3331,f113458]) ).
fof(f113703,plain,
( frontsegP(sk3,sk7)
| ssList(tl(sk7))
| sk9 = hd(sk7)
| ~ spl0_4
| spl0_8
| ~ spl0_14
| ~ spl0_22 ),
inference(superposition,[],[f4344,f811]) ).
fof(f114057,plain,
( ~ frontsegP(sk3,app(app(sk7,sk3),sk3))
| spl0_133
| ~ spl0_1267 ),
inference(superposition,[],[f3176,f73364]) ).
fof(f117939,plain,
( ssList(cons(sk5,nil))
| ssList(sk3)
| ssList(sk7)
| frontsegP(sk7,sk3)
| ~ spl0_2765 ),
inference(resolution,[],[f112244,f379]) ).
fof(f135575,plain,
( strictorderP(sk3)
| ssList(nil)
| ssList(sk7)
| ssList(nil)
| ssList(sk3)
| lt(sk5,sk5)
| lt(sk5,sk5)
| ~ spl0_14
| ~ spl0_2471 ),
inference(superposition,[],[f3844,f107743]) ).
fof(f135621,plain,
( strictorderP(sk3)
| ssList(nil)
| ssList(sk7)
| ssList(sk3)
| lt(sk5,sk5)
| ~ spl0_14
| ~ spl0_2471 ),
inference(duplicate_literal_removal,[],[f135575]) ).
fof(f135650,plain,
( ssList(nil)
| ssList(sk7)
| ssList(sk3)
| lt(sk5,sk5)
| ~ spl0_4
| spl0_6
| ~ spl0_14
| ~ spl0_2471 ),
inference(forward_subsumption_resolution,[],[f135621,f860]) ).
fof(f135696,plain,
( ssList(sk7)
| ssList(sk3)
| lt(sk5,sk5)
| ~ spl0_4
| spl0_6
| spl0_8
| ~ spl0_14
| ~ spl0_2471 ),
inference(forward_subsumption_resolution,[],[f135650,f485]) ).
fof(f135723,plain,
( ssList(sk3)
| lt(sk5,sk5)
| ~ spl0_4
| spl0_6
| spl0_8
| ~ spl0_14
| spl0_2438
| ~ spl0_2471 ),
inference(forward_subsumption_resolution,[],[f135696,f107253]) ).
fof(f135739,plain,
( lt(sk5,sk5)
| ~ spl0_4
| spl0_6
| spl0_8
| ~ spl0_14
| spl0_2438
| ~ spl0_2471 ),
inference(forward_subsumption_resolution,[],[f135723,f428]) ).
fof(f135748,plain,
( $false
| ~ spl0_4
| spl0_6
| spl0_8
| ~ spl0_14
| spl0_2438
| ~ spl0_2471 ),
inference(forward_subsumption_resolution,[],[f135739,f525]) ).
fof(f135749,plain,
( ~ spl0_4
| spl0_6
| spl0_8
| ~ spl0_14
| spl0_2438
| ~ spl0_2471 ),
inference(avatar_contradiction_clause,[],[f135748]) ).
fof(f135797,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk5,nil))
| ~ spl0_68 ),
inference(resolution,[],[f2392,f327]) ).
fof(f135798,plain,
( ssList(cons(sk5,nil))
| ~ spl0_68
| spl0_74 ),
inference(forward_subsumption_resolution,[],[f135797,f2425]) ).
fof(f135799,plain,
( $false
| spl0_51
| ~ spl0_68
| spl0_74 ),
inference(forward_subsumption_resolution,[],[f135798,f2208]) ).
fof(f135800,plain,
( spl0_51
| ~ spl0_68
| spl0_74 ),
inference(avatar_contradiction_clause,[],[f135799]) ).
fof(f157425,plain,
( ~ frontsegP(sk3,sk7)
| ssList(sk7)
| ssList(sk7)
| ssList(cons(sk5,nil))
| spl0_51
| spl0_74
| ~ spl0_136 ),
inference(resolution,[],[f113307,f1311]) ).
fof(f157435,plain,
( ~ frontsegP(sk3,sk7)
| ssList(sk7)
| ssList(cons(sk5,nil))
| spl0_51
| spl0_74
| ~ spl0_136 ),
inference(duplicate_literal_removal,[],[f157425]) ).
fof(f157693,plain,
( ssList(sk3)
| ssList(sk7)
| frontsegP(sk7,sk3)
| spl0_51
| ~ spl0_2765 ),
inference(forward_subsumption_resolution,[],[f117939,f2208]) ).
fof(f157708,plain,
( ~ frontsegP(sk3,sk7)
| ssList(cons(sk5,nil))
| spl0_51
| spl0_74
| ~ spl0_136
| spl0_2438 ),
inference(forward_subsumption_resolution,[],[f157435,f107253]) ).
fof(f157843,plain,
( ssList(sk7)
| frontsegP(sk7,sk3)
| spl0_51
| ~ spl0_2765 ),
inference(forward_subsumption_resolution,[],[f157693,f428]) ).
fof(f157855,plain,
( ~ frontsegP(sk3,sk7)
| spl0_51
| spl0_74
| ~ spl0_136
| spl0_2438 ),
inference(forward_subsumption_resolution,[],[f157708,f2208]) ).
fof(f157898,plain,
( frontsegP(sk7,sk3)
| spl0_51
| spl0_2438
| ~ spl0_2765 ),
inference(forward_subsumption_resolution,[],[f157843,f107253]) ).
fof(f157910,plain,
( ~ spl0_2660
| spl0_51
| spl0_74
| ~ spl0_136
| spl0_2438 ),
inference(avatar_split_clause,[],[f157855,f107252,f3199,f2424,f2207,f110556]) ).
fof(f157921,plain,
( spl0_2662
| spl0_51
| spl0_2438
| ~ spl0_2765 ),
inference(avatar_split_clause,[],[f157898,f112242,f107252,f2207,f110566]) ).
fof(f158658,plain,
( spl0_148
| ~ spl0_2662
| ~ spl0_4
| spl0_6
| spl0_8
| ~ spl0_22
| ~ spl0_2659 ),
inference(avatar_split_clause,[],[f113487,f110552,f809,f484,f474,f462,f110566,f3415]) ).
fof(f159878,plain,
( spl0_2659
| spl0_148
| spl0_2660
| ~ spl0_4
| spl0_8
| ~ spl0_14
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f113703,f809,f512,f484,f462,f110556,f3415,f110552]) ).
fof(f160155,plain,
( ~ frontsegP(sk3,app(nil,cons(sk5,nil)))
| ~ spl0_21
| spl0_51
| spl0_74
| ~ spl0_136 ),
inference(superposition,[],[f113308,f807]) ).
fof(f160243,plain,
( ~ frontsegP(sk3,cons(sk5,nil))
| ~ spl0_21
| spl0_51
| spl0_74
| ~ spl0_136 ),
inference(forward_demodulation,[],[f160155,f2741]) ).
fof(f160472,plain,
( ~ frontsegP(sk3,app(app(nil,sk3),sk3))
| ~ spl0_21
| spl0_133
| ~ spl0_1267 ),
inference(forward_demodulation,[],[f114057,f807]) ).
fof(f160769,plain,
( ~ spl0_2213
| ~ spl0_21
| spl0_51
| spl0_74
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f160243,f3199,f2424,f2207,f805,f98969]) ).
fof(f160853,plain,
( ~ frontsegP(sk3,app(sk3,sk3))
| ~ spl0_21
| spl0_133
| ~ spl0_1267 ),
inference(forward_demodulation,[],[f160472,f602]) ).
fof(f161038,plain,
( ~ frontsegP(sk3,cons(sk9,sk3))
| ~ spl0_4
| spl0_6
| ~ spl0_21
| spl0_133
| ~ spl0_1267 ),
inference(forward_demodulation,[],[f160853,f6246]) ).
fof(f161175,plain,
( $false
| ~ spl0_4
| spl0_6
| ~ spl0_14
| ~ spl0_21
| spl0_133
| ~ spl0_1267 ),
inference(forward_subsumption_resolution,[],[f161038,f106924]) ).
fof(f161176,plain,
( ~ spl0_4
| spl0_6
| ~ spl0_14
| ~ spl0_21
| spl0_133
| ~ spl0_1267 ),
inference(avatar_contradiction_clause,[],[f161175]) ).
cnf(s3,plain,
( spl0_1
| spl0_4 ),
inference(sat_conversion,[],[f465]) ).
cnf(s7,plain,
( spl0_1
| ~ spl0_6 ),
inference(sat_conversion,[],[f477]) ).
cnf(s15,plain,
( spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f517]) ).
cnf(s18,plain,
~ spl0_8,
inference(sat_conversion,[],[f520]) ).
cnf(s55,plain,
( spl0_8
| ~ spl0_50
| spl0_51 ),
inference(sat_conversion,[],[f2301]) ).
cnf(s57,plain,
spl0_16,
inference(sat_conversion,[],[f2339]) ).
cnf(s155,plain,
( spl0_8
| ~ spl0_51 ),
inference(sat_conversion,[],[f2720]) ).
cnf(s170,plain,
( spl0_51
| spl0_54
| spl0_55 ),
inference(sat_conversion,[],[f2839]) ).
cnf(s180,plain,
( spl0_8
| ~ spl0_55 ),
inference(sat_conversion,[],[f2972]) ).
cnf(s183,plain,
( ~ spl0_1
| ~ spl0_16
| spl0_51
| ~ spl0_54
| spl0_74 ),
inference(sat_conversion,[],[f2985]) ).
cnf(s186,plain,
( spl0_51
| ~ spl0_74 ),
inference(sat_conversion,[],[f2992]) ).
cnf(s233,plain,
( ~ spl0_16
| spl0_68
| spl0_136 ),
inference(sat_conversion,[],[f3201]) ).
cnf(s240,plain,
( ~ spl0_16
| spl0_68
| ~ spl0_133 ),
inference(sat_conversion,[],[f3223]) ).
cnf(s445,plain,
( ~ spl0_39
| spl0_50
| spl0_51 ),
inference(sat_conversion,[],[f6431]) ).
cnf(s450,plain,
( spl0_8
| ~ spl0_15
| spl0_39 ),
inference(sat_conversion,[],[f6479]) ).
cnf(s529,plain,
( spl0_21
| ~ spl0_148 ),
inference(sat_conversion,[],[f8133]) ).
cnf(s6454,plain,
( ~ spl0_4
| spl0_8
| ~ spl0_14
| spl0_51
| spl0_2212
| spl0_2213 ),
inference(sat_conversion,[],[f98972]) ).
cnf(s6489,plain,
( ~ spl0_4
| ~ spl0_14
| spl0_51
| spl0_1267
| ~ spl0_2212 ),
inference(sat_conversion,[],[f99415]) ).
cnf(s7061,plain,
~ spl0_2438,
inference(sat_conversion,[],[f107786]) ).
cnf(s7084,plain,
( spl0_21
| spl0_22
| spl0_2438 ),
inference(sat_conversion,[],[f108472]) ).
cnf(s7426,plain,
( spl0_51
| spl0_74
| spl0_133
| spl0_2471
| spl0_2765 ),
inference(sat_conversion,[],[f112245]) ).
cnf(s9252,plain,
( ~ spl0_4
| spl0_6
| spl0_8
| ~ spl0_14
| spl0_2438
| ~ spl0_2471 ),
inference(sat_conversion,[],[f135749]) ).
cnf(s9265,plain,
( spl0_51
| ~ spl0_68
| spl0_74 ),
inference(sat_conversion,[],[f135800]) ).
cnf(s11354,plain,
( spl0_51
| spl0_74
| ~ spl0_136
| spl0_2438
| ~ spl0_2660 ),
inference(sat_conversion,[],[f157910]) ).
cnf(s11358,plain,
( spl0_51
| spl0_2438
| spl0_2662
| ~ spl0_2765 ),
inference(sat_conversion,[],[f157921]) ).
cnf(s11481,plain,
( ~ spl0_4
| spl0_6
| spl0_8
| ~ spl0_22
| spl0_148
| ~ spl0_2659
| ~ spl0_2662 ),
inference(sat_conversion,[],[f158658]) ).
cnf(s11843,plain,
( ~ spl0_4
| spl0_8
| ~ spl0_14
| ~ spl0_22
| spl0_148
| spl0_2659
| spl0_2660 ),
inference(sat_conversion,[],[f159878]) ).
cnf(s12037,plain,
( ~ spl0_21
| spl0_51
| spl0_74
| ~ spl0_136
| ~ spl0_2213 ),
inference(sat_conversion,[],[f160769]) ).
cnf(s12169,plain,
( ~ spl0_4
| spl0_6
| ~ spl0_14
| ~ spl0_21
| spl0_133
| ~ spl0_1267 ),
inference(sat_conversion,[],[f161176]) ).
cnf(s12311,plain,
~ spl0_55,
inference(rat,[],[s180,s18]) ).
cnf(s12312,plain,
~ spl0_51,
inference(rat,[],[s155,s18]) ).
cnf(s12313,plain,
~ spl0_50,
inference(rat,[],[s55,s12312,s18]) ).
cnf(s12320,plain,
~ spl0_74,
inference(rat,[],[s186,s12312]) ).
cnf(s12321,plain,
spl0_54,
inference(rat,[],[s170,s12311,s12312]) ).
cnf(s12325,plain,
~ spl0_1,
inference(rat,[],[s183,s12320,s12321,s57,s12312]) ).
cnf(s12327,plain,
~ spl0_39,
inference(rat,[],[s445,s12312,s12313]) ).
cnf(s12452,plain,
~ spl0_68,
inference(rat,[],[s9265,s12312,s12320]) ).
cnf(s12474,plain,
~ spl0_15,
inference(rat,[],[s450,s18,s12327]) ).
cnf(s12563,plain,
~ spl0_133,
inference(rat,[],[s240,s57,s12452]) ).
cnf(s12565,plain,
spl0_136,
inference(rat,[],[s233,s57,s12452]) ).
cnf(s12700,plain,
~ spl0_2660,
inference(rat,[],[s11354,s12320,s7061,s12312,s12565]) ).
cnf(s12703,plain,
spl0_14,
inference(rat,[],[s15,s12474]) ).
cnf(s13267,plain,
~ spl0_6,
inference(rat,[],[s7,s12325]) ).
cnf(s13311,plain,
spl0_4,
inference(rat,[],[s3,s12325]) ).
cnf(s13318,plain,
~ spl0_2471,
inference(rat,[],[s9252,s13267,s7061,s12703,s18,s13311]) ).
cnf(s13440,plain,
spl0_2765,
inference(rat,[],[s7426,s12563,s12320,s12312,s13318]) ).
cnf(s13607,plain,
spl0_2662,
inference(rat,[],[s11358,s12312,s7061,s13440]) ).
cnf(s14489,plain,
( spl0_148
| ~ spl0_22 ),
inference(rat,[],[s11481,s11843,s12700,s12703,s13607,s13311,s13267,s18]) ).
cnf(s14490,plain,
spl0_21,
inference(rat,[],[s14489,s529,s7084,s7061]) ).
cnf(s14491,plain,
~ spl0_2213,
inference(rat,[],[s12037,s12565,s12320,s12312,s14490]) ).
cnf(s14506,plain,
~ spl0_1267,
inference(rat,[],[s12169,s13311,s12563,s13267,s12703,s14490]) ).
cnf(s14511,plain,
spl0_2212,
inference(rat,[],[s6454,s13311,s12703,s12312,s18,s14491]) ).
cnf(s14516,plain,
$false,
inference(rat,[],[s6489,s13311,s12703,s12312,s14511,s14506]) ).
fof(f161279,plain,
$false,
inference(avatar_sat_refutation,[],[s14516]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC172-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.10/0.38 % Computer : n005.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Mon Sep 28 08:16:02 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.15/0.41 Running first-order model finding
% 0.15/0.41 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
% 26.29/4.16 % (634622)Will run a generic schedule for satisfiability detection.
% 26.29/4.16 % (634629)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=526259848:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 26.29/4.16 % (634628)% WARNING: option uhcvi not known.
% 26.29/4.16 % (634630)dis+10_1_sil=32000:sp=arity:random_seed=3883386606:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 26.29/4.16 % (634627)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=552181475_2999 on theBenchmark for (2999ds/0Mi)
% 26.29/4.16 % (634628)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=795920278:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 26.29/4.16 % (634631)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1044716137:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 26.29/4.16 % (634633)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=168015208:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 26.29/4.16 % (634632)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=900132660:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 26.29/4.16 % TRYING [1]
% 26.29/4.16 % TRYING [2]
% 26.29/4.16 % TRYING [3]
% 26.29/4.16 % TRYING [4]
% 26.29/4.16 % (634630)Instruction limit reached!
% 26.29/4.16 % (634630)------------------------------
% 26.29/4.16 % (634630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.29/4.16 % (634630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.29/4.16 % (634630)CaDiCaL version: 2.1.3
% 26.29/4.16 % (634630)Termination reason: Instruction limit
% 26.29/4.16 % (634630)Termination phase: Saturation
% 26.29/4.16 % (634630)Time elapsed: 0.057 s
% 26.29/4.16 % (634630)Peak memory usage: 13 MB
% 26.29/4.16 % (634630)Instructions burned: 104 (million)
% 26.29/4.16 % (634631)Instruction limit reached!
% 26.29/4.16 % (634631)------------------------------
% 26.29/4.16 % (634631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.29/4.16 % (634631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.29/4.16 % (634631)CaDiCaL version: 2.1.3
% 26.29/4.16 % (634631)Termination reason: Instruction limit
% 26.29/4.16 % (634631)Termination phase: Saturation
% 26.29/4.16 % (634631)Time elapsed: 0.060 s
% 26.29/4.16 % (634631)Peak memory usage: 13 MB
% 26.29/4.16 % (634631)Instructions burned: 116 (million)
% 26.29/4.16 % (634632)Instruction limit reached!
% 26.29/4.16 % (634632)------------------------------
% 26.29/4.16 % (634632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.29/4.16 % (634632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.29/4.16 % (634632)CaDiCaL version: 2.1.3
% 26.29/4.16 % (634632)Termination reason: Instruction limit
% 26.29/4.16 % (634632)Termination phase: Saturation
% 26.29/4.16 % (634632)Time elapsed: 0.064 s
% 26.29/4.16 % (634632)Peak memory usage: 14 MB
% 26.29/4.16 % (634632)Instructions burned: 131 (million)
% 26.29/4.16 % (634641)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3683773081:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 26.29/4.16 % (634642)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3679476465:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 26.29/4.16 % (634643)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=3007497315:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 26.29/4.16 % TRYING [1]
% 26.29/4.16 % TRYING [2]
% 26.29/4.16 % TRYING [3]
% 26.29/4.16 % (634633)Instruction limit reached!
% 26.29/4.16 % (634633)------------------------------
% 26.29/4.16 % (634633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.29/4.16 % (634633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.29/4.16 % (634633)CaDiCaL version: 2.1.3
% 26.29/4.16 % (634633)Termination reason: Instruction limit
% 26.29/4.16 % (634633)Termination phase: Saturation
% 26.29/4.16 % (634633)Time elapsed: 0.096 s
% 26.29/4.16 % (634633)Peak memory usage: 14 MB
% 26.29/4.16 % (634633)Instructions burned: 160 (million)
% 26.29/4.16 % TRYING [5]
% 26.29/4.16 % TRYING [4]
% 26.29/4.16 % (634647)ott-21_1_sil=16000:fs=off:random_seed=742416991:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 26.29/4.16 % (634642)Instruction limit reached!
% 26.29/4.16 % (634642)------------------------------
% 26.29/4.16 % (634642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.29/4.16 % (634642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.79/4.96 % (634642)CaDiCaL version: 2.1.3
% 30.79/4.96 % (634642)Termination reason: Instruction limit
% 30.79/4.96 % (634642)Termination phase: Saturation
% 30.79/4.96 % (634642)Time elapsed: 0.066 s
% 30.79/4.96 % (634642)Peak memory usage: 13 MB
% 30.79/4.96 % (634642)Instructions burned: 132 (million)
% 30.79/4.96 % (634649)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2256487990:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 30.79/4.96 % TRYING [5]
% 30.79/4.96 % (634647)Instruction limit reached!
% 30.79/4.96 % (634647)------------------------------
% 30.79/4.96 % (634647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.79/4.96 % (634647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.79/4.96 % (634647)CaDiCaL version: 2.1.3
% 30.79/4.96 % (634647)Termination reason: Instruction limit
% 30.79/4.96 % (634647)Termination phase: Saturation
% 30.79/4.96 % (634647)Time elapsed: 0.087 s
% 30.79/4.96 % (634647)Peak memory usage: 13 MB
% 30.79/4.96 % (634647)Instructions burned: 181 (million)
% 30.79/4.96 % (634651)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3348812073:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 30.79/4.96 % TRYING [1]
% 30.79/4.96 % TRYING [2]
% 30.79/4.96 % TRYING [3]
% 30.79/4.96 % TRYING [6]
% 30.79/4.96 % TRYING [4]
% 30.79/4.96 % TRYING [6]
% 30.79/4.96 % (634641)Instruction limit reached!
% 30.79/4.96 % (634641)------------------------------
% 30.79/4.96 % (634641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.79/4.96 % (634641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.79/4.96 % (634641)CaDiCaL version: 2.1.3
% 30.79/4.96 % (634641)Termination reason: Instruction limit
% 30.79/4.96 % (634641)Termination phase: Finite model building constraint generation
% 30.79/4.96 % (634641)Time elapsed: 0.275 s
% 30.79/4.96 % (634641)Peak memory usage: 34 MB
% 30.79/4.96 % (634641)Instructions burned: 716 (million)
% 30.79/4.96 % (634653)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=553166696:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 30.79/4.96 % TRYING [5]
% 30.79/4.96 % (634643)Instruction limit reached!
% 30.79/4.96 % (634643)------------------------------
% 30.79/4.96 % (634643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.79/4.96 % (634643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.79/4.96 % (634643)CaDiCaL version: 2.1.3
% 30.79/4.96 % (634643)Termination reason: Instruction limit
% 30.79/4.96 % (634643)Termination phase: Saturation
% 30.79/4.96 % (634643)Time elapsed: 0.390 s
% 30.79/4.96 % (634643)Peak memory usage: 21 MB
% 30.79/4.96 % (634643)Instructions burned: 684 (million)
% 30.79/4.96 % (634649)Instruction limit reached!
% 30.79/4.96 % (634649)------------------------------
% 30.79/4.96 % (634649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.79/4.96 % (634649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.79/4.96 % (634649)CaDiCaL version: 2.1.3
% 30.79/4.96 % (634649)Termination reason: Instruction limit
% 30.79/4.96 % (634649)Termination phase: Saturation
% 30.79/4.96 % (634649)Time elapsed: 0.328 s
% 30.79/4.96 % (634649)Peak memory usage: 15 MB
% 30.79/4.96 % (634649)Instructions burned: 478 (million)
% 30.79/4.96 % (634655)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1501922289:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 30.79/4.96 % (634656)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=3696554615: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)
% 30.79/4.97 % (634651)Instruction limit reached!
% 30.79/4.97 % (634651)------------------------------
% 30.79/4.97 % (634651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.79/4.97 % (634651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.79/4.97 % (634651)CaDiCaL version: 2.1.3
% 30.79/4.97 % (634651)Termination reason: Instruction limit
% 30.79/4.97 % (634651)Termination phase: Finite model building SAT solving
% 30.79/4.97 % (634651)Time elapsed: 0.337 s
% 30.79/4.97 % (634651)Peak memory usage: 22 MB
% 30.79/4.97 % (634651)Instructions burned: 867 (million)
% 30.79/4.97 % (634659)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1449764183:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 30.79/4.97 % TRYING [14]
% 30.79/4.97 % TRYING [7]
% 30.79/4.97 % (634655)Instruction limit reached!
% 30.79/4.97 % (634655)------------------------------
% 30.79/4.97 % (634655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.79/4.97 % (634655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.79/4.97 % (634655)CaDiCaL version: 2.1.3
% 30.79/4.97 % (634655)Termination reason: Instruction limit
% 30.79/4.97 % (634655)Termination phase: Finite model building constraint generation
% 30.79/4.97 % (634655)Time elapsed: 0.324 s
% 30.79/4.97 % (634655)Peak memory usage: 72 MB
% 30.79/4.97 % (634655)Instructions burned: 889 (million)
% 30.79/4.97 % (634661)fmb+10_1_sil=64000:random_seed=3320902256:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 30.79/4.97 % TRYING [1]
% 30.79/4.97 % TRYING [2]
% 30.79/4.97 % TRYING [3]
% 30.79/4.97 % (634656)Instruction limit reached!
% 30.79/4.97 % (634656)------------------------------
% 30.79/4.97 % (634656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.79/4.97 % (634656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.79/4.97 % (634656)CaDiCaL version: 2.1.3
% 30.79/4.97 % (634656)Termination reason: Instruction limit
% 30.79/4.97 % (634656)Termination phase: Saturation
% 30.79/4.97 % (634656)Time elapsed: 0.380 s
% 30.79/4.97 % (634656)Peak memory usage: 19 MB
% 30.79/4.97 % (634656)Instructions burned: 693 (million)
% 30.79/4.97 % (634663)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4109619777:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 30.79/4.97 % TRYING [20]
% 30.79/4.97 % TRYING [4]
% 30.79/4.97 % (634659)Instruction limit reached!
% 30.79/4.97 % (634659)------------------------------
% 30.79/4.97 % (634659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.79/4.97 % (634659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.79/4.97 % (634659)CaDiCaL version: 2.1.3
% 30.79/4.97 % (634659)Termination reason: Instruction limit
% 30.79/4.97 % (634659)Termination phase: Saturation
% 30.79/4.97 % (634659)Time elapsed: 0.462 s
% 30.79/4.97 % (634659)Peak memory usage: 20 MB
% 30.79/4.97 % (634659)Instructions burned: 881 (million)
% 30.79/4.97 % (634653)Instruction limit reached!
% 30.79/4.97 % (634653)------------------------------
% 30.79/4.97 % (634653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.79/4.97 % (634653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.79/4.97 % (634653)CaDiCaL version: 2.1.3
% 30.79/4.97 % (634653)Termination reason: Instruction limit
% 30.79/4.97 % (634653)Termination phase: Saturation
% 30.79/4.97 % (634653)Time elapsed: 0.676 s
% 30.79/4.97 % (634653)Peak memory usage: 27 MB
% 30.79/4.97 % (634653)Instructions burned: 1180 (million)
% 30.79/4.97 % (634665)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1258826057:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 30.79/4.97 % (634666)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1752195745:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 30.79/4.97 % TRYING [8]
% 30.79/4.97 % TRYING [5]
% 30.79/4.97 % (634665)Instruction limit reached!
% 30.79/4.97 % (634665)------------------------------
% 30.79/4.97 % (634665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.79/4.97 % (634665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.79/4.97 % (634665)CaDiCaL version: 2.1.3
% 30.79/4.97 % (634665)Termination reason: Instruction limit
% 30.79/4.97 % (634665)Termination phase: Finite model building constraint generation
% 30.79/4.97 % (634665)Time elapsed: 0.333 s
% 30.79/4.97 % (634665)Peak memory usage: 79 MB
% 30.79/4.97 % (634665)Instructions burned: 923 (million)
% 30.79/4.97 % (634669)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=666870790:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 30.79/4.97 % TRYING [6]
% 30.79/4.97 % TRYING [8]
% 30.79/4.97 % (634669)Instruction limit reached!
% 30.79/4.97 % (634669)------------------------------
% 30.79/4.97 % (634669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.79/4.97 % (634669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.79/4.97 % (634669)CaDiCaL version: 2.1.3
% 30.79/4.97 % (634669)Termination reason: Instruction limit
% 30.79/4.97 % (634669)Termination phase: Saturation
% 30.79/4.97 % (634669)Time elapsed: 0.668 s
% 30.79/4.97 % (634669)Peak memory usage: 16 MB
% 30.79/4.97 % (634669)Instructions burned: 1473 (million)
% 30.79/4.97 % (634671)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=779199554:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 30.79/4.97 % TRYING [77]
% 30.79/4.97 % TRYING [7]
% 30.79/4.97 % (634666)Instruction limit reached!
% 30.79/4.97 % (634666)------------------------------
% 30.79/4.97 % (634666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.79/4.97 % (634666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.79/4.97 % (634666)CaDiCaL version: 2.1.3
% 30.79/4.97 % (634666)Termination reason: Instruction limit
% 30.79/4.97 % (634666)Termination phase: Saturation
% 30.79/4.97 % (634666)Time elapsed: 2.622 s
% 30.79/4.97 % (634666)Peak memory usage: 54 MB
% 30.79/4.97 % (634666)Instructions burned: 5131 (million)
% 30.79/4.97 % (634673)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3089247470:fmbsr=2.30978:i=2174_2962 on theBenchmark for (2962ds/2174Mi)
% 30.79/4.97 % TRYING [16]
% 30.79/4.97 % TRYING [9]
% 30.79/4.97 % (634663)Instruction limit reached!
% 30.79/4.97 % (634663)------------------------------
% 30.79/4.97 % (634663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.79/4.97 % (634663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.79/4.97 % (634663)CaDiCaL version: 2.1.3
% 30.79/4.97 % (634663)Termination reason: Instruction limit
% 30.79/4.97 % (634663)Termination phase: Finite model building constraint generation
% 30.79/4.97 % (634663)Time elapsed: 3.267 s
% 30.79/4.97 % (634663)Peak memory usage: 588 MB
% 30.79/4.97 % (634663)Instructions burned: 9515 (million)
% 30.79/4.97 % TRYING [8]
% 30.79/4.97 % (634675)ott-2_1_sil=16000:newcnf=on:random_seed=1170672327:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 30.79/4.97 % (634671)Instruction limit reached!
% 30.79/4.97 % (634671)------------------------------
% 30.79/4.97 % (634671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.79/4.97 % (634671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.79/4.97 % (634671)CaDiCaL version: 2.1.3
% 30.79/4.97 % (634671)Termination reason: Instruction limit
% 30.79/4.97 % (634671)Termination phase: Finite model building constraint generation
% 30.79/4.97 % (634671)Time elapsed: 2.252 s
% 30.79/4.97 % (634671)Peak memory usage: 428 MB
% 30.79/4.97 % (634671)Instructions burned: 6327 (million)
% 30.79/4.97 % (634677)ott+10_1_sil=32000:tgt=ground:random_seed=172389429:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 30.79/4.97 % (634628) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-634622-634628"...
% 30.79/4.97 % (634628)...printing done.
% 30.79/4.97 % (634628)Refutation found. Thanks to Tanya!
% 30.79/4.97 % SZS status Unsatisfiable for theBenchmark
% 30.79/4.97 % SZS output start Proof for theBenchmark
% See solution above
% 30.79/4.97 % (634628)------------------------------
% 30.79/4.97 % (634628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.79/4.97 % (634628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.79/4.97 % (634628)CaDiCaL version: 2.1.3
% 30.79/4.97 % (634628)Termination reason: Refutation
% 30.79/4.97 % (634628)Time elapsed: 4.459 s
% 30.79/4.97 % (634628)Peak memory usage: 80 MB
% 30.79/4.97 % (634628)Instructions burned: 8379 (million)
% 30.79/4.97 % (634622)Success in time 4.544 s
% 30.79/4.97 % Vampire exiting
%------------------------------------------------------------------------------