%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC192-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 : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:05:03 PM UTC 2026
% Result : Unsatisfiable 13.66s 2.38s
% Output : Refutation 13.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 109
% Syntax : Number of formulae : 625 ( 81 unt; 60 def)
% Number of atoms : 2015 ( 249 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 2692 (1302 ~;1330 |; 0 &)
% ( 60 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 70 ( 68 usr; 61 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 9 con; 0-2 aty)
% Number of variables : 249 ( 0 sgn 249 !; 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(f52,axiom,
! [X0,X1] : ssList(skaf43(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause52) ).
fof(f53,axiom,
! [X0,X1] : ssList(skaf42(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause53) ).
fof(f60,axiom,
! [X0] :
( ~ ssList(X0)
| frontsegP(X0,nil) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause60) ).
fof(f71,axiom,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause71) ).
fof(f72,axiom,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f73,axiom,
! [X0] :
( ~ ssList(X0)
| app(X0,nil) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause73) ).
fof(f74,axiom,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause74) ).
fof(f75,axiom,
! [X0] :
( ssList(tl(X0))
| ~ ssList(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(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
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(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(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(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(f148,axiom,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| frontsegP(app(X0,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause137) ).
fof(f149,axiom,
! [X2,X0,X1] :
( X0 != X1
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0)
| memberP(cons(X1,X2),X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause138) ).
fof(f152,axiom,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssItem(X1)
| memberP(app(X2,X0),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause141) ).
fof(f154,axiom,
! [X2,X0,X1] :
( app(X0,X1) != X2
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| rearsegP(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause143) ).
fof(f155,axiom,
! [X2,X0,X1] :
( app(X0,X1) != X2
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| frontsegP(X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause144) ).
fof(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(f182,axiom,
! [X0,X1] :
( ~ memberP(X0,X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| app(skaf42(X0,X1),cons(X1,skaf43(X1,X0))) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause169) ).
fof(f187,axiom,
! [X2,X3,X0,X1] :
( app(app(X0,X1),X2) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| segmentP(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause173) ).
fof(f189,axiom,
! [X2,X3,X0,X1] :
( app(X0,cons(X1,X2)) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(X3)
| memberP(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause175) ).
fof(f190,axiom,
! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ~ ssList(X3)
| ~ ssList(X1)
| ~ ssItem(X2)
| ~ ssItem(X0)
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause176) ).
fof(f192,axiom,
! [X2,X3,X0,X1] :
( ~ frontsegP(X0,X1)
| X2 != X3
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X2)
| frontsegP(cons(X2,X0),cons(X3,X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause178) ).
fof(f193,axiom,
! [X2,X3,X0,X1,X4] :
( app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(X4)
| ~ ssList(X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(f202,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_3) ).
fof(f203,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_4) ).
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(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(f220,negated_conjecture,
( memberP(sk4,sk9)
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_18) ).
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(f233,plain,
! [X2,X1] :
( ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X1)
| memberP(cons(X1,X2),X1) ),
inference(equality_resolution,[],[f149]) ).
fof(f234,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(X0,X1))
| rearsegP(app(X0,X1),X1) ),
inference(equality_resolution,[],[f154]) ).
fof(f235,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1))
| frontsegP(app(X0,X1),X0) ),
inference(equality_resolution,[],[f155]) ).
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(app(X0,cons(X1,X2)))
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(X2)
| memberP(app(X0,cons(X1,X2)),X1) ),
inference(equality_resolution,[],[f189]) ).
fof(f240,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(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(f253,plain,
singletonP(nil),
inference(consistent_polarity_flipping,[],[f11]) ).
fof(f257,plain,
! [X0] :
( ~ frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f264,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ duplicatefreeP(X0)
| ssItem(X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f266,plain,
! [X0] :
( segmentP(nil,X0)
| ~ ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f282,plain,
! [X0] :
( ~ singletonP(cons(X0,nil))
| ~ ssList(cons(X0,nil))
| ~ ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f231]) ).
fof(f286,plain,
! [X0,X1] :
( ~ ssList(X1)
| segmentP(X1,X0)
| ~ ssList(X0)
| segmentP(X0,X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f287,plain,
! [X0,X1] :
( ~ ssList(X1)
| frontsegP(X1,X0)
| ~ ssList(X0)
| frontsegP(X0,X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f290,plain,
! [X2,X0,X1] :
( ~ frontsegP(app(X0,X2),X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| frontsegP(X0,X1) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f292,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1))
| ~ frontsegP(app(X0,X1),X0) ),
inference(consistent_polarity_flipping,[],[f235]) ).
fof(f303,plain,
! [X2,X0,X1] :
( ~ ssList(app(app(X0,X1),X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ segmentP(app(app(X0,X1),X2),X1) ),
inference(consistent_polarity_flipping,[],[f238]) ).
fof(f305,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(f306,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,[],[f240]) ).
fof(f307,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(f312,plain,
! [X3,X0,X1] :
( ~ frontsegP(cons(X3,X0),cons(X3,X1))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X3)
| frontsegP(X0,X1) ),
inference(duplicate_literal_removal,[],[f306]) ).
fof(f314,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X2) ),
inference(duplicate_literal_removal,[],[f233]) ).
fof(f319,definition,
( spl0_1
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f320,plain,
( nil != sk3
| spl0_1 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f321,plain,
( nil = sk3
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f323,definition,
( spl0_2
<=> memberP(sk4,sk9) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f325,plain,
( memberP(sk4,sk9)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f323]) ).
fof(f326,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f220,f323,f319]) ).
fof(f328,definition,
( spl0_3
<=> sk3 = cons(sk9,nil) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f330,plain,
( sk3 = cons(sk9,nil)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f328]) ).
fof(f331,plain,
( spl0_1
| spl0_3 ),
inference(avatar_split_clause,[],[f219,f328,f319]) ).
fof(f339,definition,
( spl0_5
<=> ssItem(sk9) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f341,plain,
( ssItem(sk9)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f342,plain,
( spl0_1
| spl0_5 ),
inference(avatar_split_clause,[],[f214,f339,f319]) ).
fof(f349,definition,
( spl0_7
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f350,plain,
( ssList(nil)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f349]) ).
fof(f377,definition,
( spl0_13
<=> ! [X1] : ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f378,plain,
( ! [X1] : ssItem(X1)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f377]) ).
fof(f380,definition,
( spl0_14
<=> ! [X0] :
( ~ ssList(X0)
| ~ duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f381,plain,
( ! [X0] :
( ~ duplicatefreeP(X0)
| ~ ssList(X0) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f382,plain,
( spl0_13
| spl0_14 ),
inference(avatar_split_clause,[],[f264,f380,f377]) ).
fof(f385,plain,
spl0_7,
inference(avatar_split_clause,[],[f8,f349]) ).
fof(f388,plain,
( ! [X0] : ~ memberP(nil,X0)
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f71,f378]) ).
fof(f433,plain,
sk3 = app(sk3,nil),
inference(resolution,[],[f73,f202]) ).
fof(f465,plain,
sk3 = app(nil,sk3),
inference(resolution,[],[f74,f202]) ).
fof(f468,plain,
sk8 = app(nil,sk8),
inference(resolution,[],[f74,f209]) ).
fof(f484,plain,
( ! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1) )
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f86,f378]) ).
fof(f512,plain,
( ! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssList(X2) )
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f314,f378]) ).
fof(f515,plain,
( ! [X0,X1] :
( ~ ssList(X1)
| tl(cons(X0,X1)) = X1 )
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f96,f378]) ).
fof(f517,plain,
( ! [X0,X1] : skaf82(X1) = tl(cons(X0,skaf82(X1)))
| ~ spl0_13 ),
inference(resolution,[],[f515,f13]) ).
fof(f549,plain,
( ! [X0] : sk7 = tl(cons(X0,sk7))
| ~ spl0_13 ),
inference(resolution,[],[f515,f208]) ).
fof(f550,plain,
( ! [X0] : sk8 = tl(cons(X0,sk8))
| ~ spl0_13 ),
inference(resolution,[],[f515,f209]) ).
fof(f647,plain,
! [X0] :
( ~ ssList(X0)
| nil = tl(X0)
| tl(X0) = cons(hd(tl(X0)),tl(tl(X0)))
| nil = X0 ),
inference(resolution,[],[f107,f75]) ).
fof(f653,definition,
( spl0_15
<=> nil = sk8 ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f654,plain,
( nil != sk8
| spl0_15 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f655,plain,
( nil = sk8
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f657,definition,
( spl0_16
<=> sk8 = cons(hd(sk8),tl(sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f659,plain,
( sk8 = cons(hd(sk8),tl(sk8))
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f662,definition,
( spl0_17
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f663,plain,
( nil != sk7
| spl0_17 ),
inference(avatar_component_clause,[],[f662]) ).
fof(f664,plain,
( nil = sk7
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f662]) ).
fof(f666,definition,
( spl0_18
<=> sk7 = cons(hd(sk7),tl(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f668,plain,
( sk7 = cons(hd(sk7),tl(sk7))
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f666]) ).
fof(f738,plain,
! [X0] :
( ~ ssList(X0)
| nil = tl(X0)
| tl(X0) = cons(skaf83(tl(X0)),skaf82(tl(X0)))
| nil = X0 ),
inference(resolution,[],[f112,f75]) ).
fof(f757,definition,
( spl0_21
<=> ssList(app(app(nil,cons(sk5,nil)),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f758,plain,
( ssList(app(app(nil,cons(sk5,nil)),cons(sk6,nil)))
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f757]) ).
fof(f759,plain,
( ~ ssList(app(app(nil,cons(sk5,nil)),cons(sk6,nil)))
| spl0_21 ),
inference(avatar_component_clause,[],[f757]) ).
fof(f834,plain,
! [X0,X1] :
( rearsegP(app(X0,X1),X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[],[f234,f85]) ).
fof(f844,plain,
( rearsegP(sk3,sk8)
| ~ ssList(sk8)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
inference(superposition,[],[f834,f223]) ).
fof(f851,plain,
( rearsegP(sk3,sk8)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
inference(forward_subsumption_resolution,[],[f844,f209]) ).
fof(f895,plain,
! [X0] :
( ~ ssList(X0)
| segmentP(sk8,X0)
| segmentP(X0,sk8)
| sk8 = X0 ),
inference(resolution,[],[f286,f209]) ).
fof(f943,plain,
! [X0] :
( ~ ssList(X0)
| frontsegP(sk3,X0)
| frontsegP(X0,sk3)
| sk3 = X0 ),
inference(resolution,[],[f287,f202]) ).
fof(f963,plain,
! [X0,X1] :
( ~ frontsegP(app(X0,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(forward_subsumption_resolution,[],[f292,f85]) ).
fof(f973,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,[],[f963,f223]) ).
fof(f979,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,[],[f973,f209]) ).
fof(f1056,plain,
( ! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X2)
| memberP(app(X2,X0),X1) )
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f152,f378]) ).
fof(f1057,plain,
( ! [X2,X0,X1] :
( ~ ssList(cons(X0,X1))
| ~ ssList(X2)
| memberP(app(X2,cons(X0,X1)),X0)
| ~ ssList(X1) )
| ~ spl0_13 ),
inference(resolution,[],[f1056,f512]) ).
fof(f1060,plain,
( ! [X2,X0,X1] :
( memberP(app(X2,cons(X0,X1)),X0)
| ~ ssList(X2)
| ~ ssList(X1) )
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f1057,f484]) ).
fof(f1082,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,[],[f290,f223]) ).
fof(f1089,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,[],[f1082,f209]) ).
fof(f1111,plain,
( ~ ssList(app(nil,cons(sk5,nil)))
| ~ ssList(cons(sk6,nil))
| spl0_21 ),
inference(resolution,[],[f759,f85]) ).
fof(f1113,definition,
( spl0_25
<=> ssList(cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f1114,plain,
( ssList(cons(sk6,nil))
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f1113]) ).
fof(f1115,plain,
( ~ ssList(cons(sk6,nil))
| spl0_25 ),
inference(avatar_component_clause,[],[f1113]) ).
fof(f1117,definition,
( spl0_26
<=> ssList(app(nil,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f1118,plain,
( ssList(app(nil,cons(sk5,nil)))
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f1117]) ).
fof(f1119,plain,
( ~ ssList(app(nil,cons(sk5,nil)))
| spl0_26 ),
inference(avatar_component_clause,[],[f1117]) ).
fof(f1120,plain,
( ~ spl0_25
| ~ spl0_26
| spl0_21 ),
inference(avatar_split_clause,[],[f1111,f757,f1117,f1113]) ).
fof(f1142,plain,
( ~ ssList(nil)
| ~ ssItem(sk6)
| spl0_25 ),
inference(resolution,[],[f86,f1115]) ).
fof(f1150,plain,
( ~ ssItem(sk6)
| ~ spl0_7
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f1142,f350]) ).
fof(f1151,plain,
( $false
| ~ spl0_7
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f1150,f207]) ).
fof(f1152,plain,
( ~ spl0_7
| spl0_25 ),
inference(avatar_contradiction_clause,[],[f1151]) ).
fof(f1161,definition,
( spl0_27
<=> nil = cons(sk6,nil) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f1162,plain,
( nil != cons(sk6,nil)
| spl0_27 ),
inference(avatar_component_clause,[],[f1161]) ).
fof(f1163,plain,
( nil = cons(sk6,nil)
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f1161]) ).
fof(f1231,plain,
( memberP(nil,sk6)
| ~ ssItem(sk6)
| ~ ssList(nil)
| ~ spl0_27 ),
inference(superposition,[],[f314,f1163]) ).
fof(f1239,plain,
( ~ ssItem(sk6)
| ~ ssList(nil)
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f1231,f71]) ).
fof(f1245,plain,
( ~ ssList(nil)
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f1239,f207]) ).
fof(f1247,plain,
( $false
| ~ spl0_7
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f1245,f350]) ).
fof(f1248,plain,
( ~ spl0_7
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f1247]) ).
fof(f1250,plain,
( ~ ssList(nil)
| ~ ssList(cons(sk5,nil))
| spl0_26 ),
inference(resolution,[],[f1119,f85]) ).
fof(f1251,plain,
( ~ ssList(cons(sk5,nil))
| ~ spl0_7
| spl0_26 ),
inference(forward_subsumption_resolution,[],[f1250,f350]) ).
fof(f1252,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ~ spl0_7
| spl0_26 ),
inference(resolution,[],[f1251,f86]) ).
fof(f1253,plain,
( ~ ssItem(sk5)
| ~ spl0_7
| spl0_26 ),
inference(forward_subsumption_resolution,[],[f1252,f350]) ).
fof(f1254,plain,
( $false
| ~ spl0_7
| spl0_26 ),
inference(forward_subsumption_resolution,[],[f1253,f206]) ).
fof(f1255,plain,
( ~ spl0_7
| spl0_26 ),
inference(avatar_contradiction_clause,[],[f1254]) ).
fof(f1262,definition,
( spl0_32
<=> nil = app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f1263,plain,
( nil != app(app(sk7,cons(sk5,nil)),cons(sk6,nil))
| spl0_32 ),
inference(avatar_component_clause,[],[f1262]) ).
fof(f1264,plain,
( nil = app(app(sk7,cons(sk5,nil)),cons(sk6,nil))
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f1262]) ).
fof(f1266,definition,
( spl0_33
<=> ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f1267,plain,
( ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f1266]) ).
fof(f1268,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| spl0_33 ),
inference(avatar_component_clause,[],[f1266]) ).
fof(f1471,definition,
( spl0_47
<=> nil = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f1472,plain,
( nil != cons(sk5,nil)
| spl0_47 ),
inference(avatar_component_clause,[],[f1471]) ).
fof(f1473,plain,
( nil = cons(sk5,nil)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f1471]) ).
fof(f1475,definition,
( spl0_48
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f1476,plain,
( ssList(cons(sk5,nil))
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f1475]) ).
fof(f1477,plain,
( ~ ssList(cons(sk5,nil))
| spl0_48 ),
inference(avatar_component_clause,[],[f1475]) ).
fof(f1484,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| spl0_48 ),
inference(resolution,[],[f1477,f86]) ).
fof(f1485,plain,
( ~ ssItem(sk5)
| ~ spl0_7
| spl0_48 ),
inference(forward_subsumption_resolution,[],[f1484,f350]) ).
fof(f1486,plain,
( $false
| ~ spl0_7
| spl0_48 ),
inference(forward_subsumption_resolution,[],[f1485,f206]) ).
fof(f1487,plain,
( ~ spl0_7
| spl0_48 ),
inference(avatar_contradiction_clause,[],[f1486]) ).
fof(f1517,plain,
( ~ singletonP(nil)
| ~ ssList(nil)
| ~ ssItem(sk5)
| ~ spl0_47 ),
inference(superposition,[],[f282,f1473]) ).
fof(f1530,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f1517,f253]) ).
fof(f1538,plain,
( ~ ssItem(sk5)
| ~ spl0_7
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f1530,f350]) ).
fof(f1542,plain,
( $false
| ~ spl0_7
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f1538,f206]) ).
fof(f1543,plain,
( ~ spl0_7
| ~ spl0_47 ),
inference(avatar_contradiction_clause,[],[f1542]) ).
fof(f1737,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,[],[f163,f223]) ).
fof(f1743,plain,
! [X0] :
( sk3 != app(X0,sk3)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(nil)
| nil = X0 ),
inference(superposition,[],[f163,f465]) ).
fof(f1746,plain,
! [X0] :
( sk8 != app(X0,sk8)
| ~ ssList(X0)
| ~ ssList(sk8)
| ~ ssList(nil)
| nil = X0 ),
inference(superposition,[],[f163,f468]) ).
fof(f1750,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,[],[f163,f223]) ).
fof(f1763,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,[],[f1750,f209]) ).
fof(f1767,plain,
! [X0] :
( sk8 != app(X0,sk8)
| ~ ssList(X0)
| ~ ssList(nil)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f1746,f209]) ).
fof(f1770,plain,
! [X0] :
( sk3 != app(X0,sk3)
| ~ ssList(X0)
| ~ ssList(nil)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f1743,f202]) ).
fof(f1775,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,[],[f1737,f209]) ).
fof(f1787,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_15 ),
inference(forward_demodulation,[],[f1763,f655]) ).
fof(f1791,plain,
( ! [X0] :
( sk8 != app(X0,sk8)
| ~ ssList(X0)
| nil = X0 )
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f1767,f350]) ).
fof(f1794,plain,
( ! [X0] :
( sk3 != app(X0,sk3)
| ~ ssList(X0)
| nil = X0 )
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f1770,f350]) ).
fof(f1843,definition,
( spl0_54
<=> sk8 = cons(skaf83(sk8),skaf82(sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f1845,plain,
( sk8 = cons(skaf83(sk8),skaf82(sk8))
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f1843]) ).
fof(f2169,definition,
( spl0_70
<=> ! [X0] :
( ~ frontsegP(sk3,X0)
| frontsegP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f2170,plain,
( ! [X0] :
( frontsegP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0)
| ~ frontsegP(sk3,X0)
| ~ ssList(X0) )
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f2169]) ).
fof(f2171,plain,
( ~ spl0_33
| spl0_70 ),
inference(avatar_split_clause,[],[f1089,f2169,f1266]) ).
fof(f2173,definition,
( spl0_71
<=> frontsegP(sk3,app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f2175,plain,
( ~ frontsegP(sk3,app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| spl0_71 ),
inference(avatar_component_clause,[],[f2173]) ).
fof(f2176,plain,
( ~ spl0_33
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f979,f2173,f1266]) ).
fof(f2183,definition,
( spl0_73
<=> rearsegP(sk3,sk8) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f2185,plain,
( rearsegP(sk3,sk8)
| ~ spl0_73 ),
inference(avatar_component_clause,[],[f2183]) ).
fof(f2186,plain,
( ~ spl0_33
| spl0_73 ),
inference(avatar_split_clause,[],[f851,f2183,f1266]) ).
fof(f2188,definition,
( spl0_74
<=> ! [X0] :
( sk3 != app(X0,sk8)
| app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f2189,plain,
( ! [X0] :
( sk3 != app(X0,sk8)
| app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) = X0
| ~ ssList(X0) )
| ~ spl0_74 ),
inference(avatar_component_clause,[],[f2188]) ).
fof(f2191,plain,
( ~ spl0_33
| spl0_74 ),
inference(avatar_split_clause,[],[f1775,f2188,f1266]) ).
fof(f2206,definition,
( spl0_78
<=> ssList(app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f2207,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f2206]) ).
fof(f2208,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| spl0_78 ),
inference(avatar_component_clause,[],[f2206]) ).
fof(f2235,plain,
( ~ ssItem(sk9)
| ~ ssList(sk4)
| sk4 = app(skaf42(sk4,sk9),cons(sk9,skaf43(sk9,sk4)))
| ~ spl0_2 ),
inference(resolution,[],[f325,f182]) ).
fof(f2240,plain,
( ~ ssList(sk4)
| sk4 = app(skaf42(sk4,sk9),cons(sk9,skaf43(sk9,sk4)))
| ~ spl0_2
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f2235,f341]) ).
fof(f2243,plain,
( sk4 = app(skaf42(sk4,sk9),cons(sk9,skaf43(sk9,sk4)))
| ~ spl0_2
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f2240,f203]) ).
fof(f2347,plain,
! [X0] :
( ~ ssList(app(sk3,X0))
| ~ ssList(nil)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ segmentP(app(sk3,X0),sk3) ),
inference(superposition,[],[f303,f465]) ).
fof(f2354,plain,
! [X0] :
( ~ ssList(app(sk3,X0))
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssList(sk8)
| ~ ssList(X0)
| ~ segmentP(app(sk3,X0),sk8) ),
inference(superposition,[],[f303,f223]) ).
fof(f2359,plain,
( ~ ssList(sk3)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk6,nil))
| ~ ssList(sk8)
| ~ segmentP(sk3,cons(sk6,nil)) ),
inference(superposition,[],[f303,f223]) ).
fof(f2362,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk6,nil))
| ~ ssList(sk8)
| ~ segmentP(sk3,cons(sk6,nil)) ),
inference(forward_subsumption_resolution,[],[f2359,f202]) ).
fof(f2363,plain,
! [X0] :
( ~ ssList(app(sk3,X0))
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssList(X0)
| ~ segmentP(app(sk3,X0),sk8) ),
inference(forward_subsumption_resolution,[],[f2354,f209]) ).
fof(f2367,plain,
( ! [X0] :
( ~ ssList(app(sk3,X0))
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ segmentP(app(sk3,X0),sk3) )
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f2347,f350]) ).
fof(f2369,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| ~ segmentP(sk3,cons(sk6,nil))
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f2362,f1114]) ).
fof(f2374,plain,
( ! [X0] :
( ~ segmentP(app(sk3,X0),sk3)
| ~ ssList(X0)
| ~ ssList(app(sk3,X0)) )
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f2367,f202]) ).
fof(f2375,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ segmentP(sk3,cons(sk6,nil))
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f2369,f209]) ).
fof(f2379,plain,
( ~ segmentP(nil,cons(sk6,nil))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_1
| ~ spl0_25 ),
inference(forward_demodulation,[],[f2375,f321]) ).
fof(f2387,definition,
( spl0_83
<=> segmentP(nil,cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f2389,plain,
( ~ segmentP(nil,cons(sk6,nil))
| spl0_83 ),
inference(avatar_component_clause,[],[f2387]) ).
fof(f2390,plain,
( ~ spl0_78
| ~ spl0_83
| ~ spl0_1
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f2379,f1113,f319,f2387,f2206]) ).
fof(f2395,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| spl0_78 ),
inference(resolution,[],[f2208,f85]) ).
fof(f2396,plain,
( ~ ssList(cons(sk5,nil))
| spl0_78 ),
inference(forward_subsumption_resolution,[],[f2395,f208]) ).
fof(f2397,plain,
( $false
| ~ spl0_48
| spl0_78 ),
inference(forward_subsumption_resolution,[],[f2396,f1476]) ).
fof(f2398,plain,
( ~ spl0_48
| spl0_78 ),
inference(avatar_contradiction_clause,[],[f2397]) ).
fof(f2401,plain,
( ~ ssList(cons(sk6,nil))
| nil = cons(sk6,nil)
| spl0_83 ),
inference(resolution,[],[f2389,f266]) ).
fof(f2404,plain,
( nil = cons(sk6,nil)
| ~ spl0_25
| spl0_83 ),
inference(forward_subsumption_resolution,[],[f2401,f1114]) ).
fof(f2406,plain,
( $false
| ~ spl0_25
| spl0_27
| spl0_83 ),
inference(forward_subsumption_resolution,[],[f2404,f1162]) ).
fof(f2407,plain,
( ~ spl0_25
| spl0_27
| spl0_83 ),
inference(avatar_contradiction_clause,[],[f2406]) ).
fof(f2412,definition,
( spl0_84
<=> ! [X0] :
( ~ ssList(app(sk3,X0))
| ~ segmentP(app(sk3,X0),sk8)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f2413,plain,
( ! [X0] :
( ~ segmentP(app(sk3,X0),sk8)
| ~ ssList(app(sk3,X0))
| ~ ssList(X0) )
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f2412]) ).
fof(f2414,plain,
( ~ spl0_33
| spl0_84 ),
inference(avatar_split_clause,[],[f2363,f2412,f1266]) ).
fof(f2448,plain,
( ! [X0,X1] :
( frontsegP(sk3,cons(X0,X1))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssItem(X0)
| ~ ssItem(sk9)
| sk9 = X0 )
| ~ spl0_3 ),
inference(superposition,[],[f305,f330]) ).
fof(f2450,plain,
( ! [X0] :
( ~ frontsegP(cons(sk9,X0),sk3)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(sk9)
| frontsegP(X0,nil) )
| ~ spl0_3 ),
inference(superposition,[],[f312,f330]) ).
fof(f2455,plain,
( ! [X0] :
( ~ frontsegP(cons(sk9,X0),sk3)
| ~ ssList(X0)
| ~ ssItem(sk9)
| frontsegP(X0,nil) )
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f2450,f350]) ).
fof(f2457,plain,
( ! [X0,X1] :
( frontsegP(sk3,cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(sk9)
| sk9 = X0 )
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f2448,f350]) ).
fof(f2474,plain,
( ! [X0] :
( ~ frontsegP(cons(sk9,X0),sk3)
| ~ ssList(X0)
| frontsegP(X0,nil) )
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f2455,f341]) ).
fof(f2476,plain,
( ! [X0,X1] :
( frontsegP(sk3,cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0)
| sk9 = X0 )
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f2457,f341]) ).
fof(f2484,plain,
( ! [X0] :
( ~ frontsegP(cons(sk9,X0),sk3)
| ~ ssList(X0) )
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f2474,f257]) ).
fof(f2495,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,[],[f307,f381]) ).
fof(f2498,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,cons(sk9,X1)),sk3))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(sk9)
| ~ ssList(nil) )
| ~ spl0_3
| ~ spl0_14 ),
inference(superposition,[],[f2495,f330]) ).
fof(f2499,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,cons(sk9,X1)),sk3))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(nil) )
| ~ spl0_3
| ~ spl0_5
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f2498,f341]) ).
fof(f2502,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,cons(sk9,X1)),sk3))
| ~ ssList(X1)
| ~ ssList(X0) )
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f2499,f350]) ).
fof(f2543,plain,
( ! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X2)
| memberP(X1,X2)
| X0 = X2 )
| ~ spl0_13 ),
inference(backward_subsumption_resolution,[],[f174,f378]) ).
fof(f2547,plain,
( ! [X2,X0,X1] :
( ~ ssList(app(X0,cons(X1,X2)))
| ~ ssList(X0)
| ~ ssList(X2)
| memberP(app(X0,cons(X1,X2)),X1) )
| ~ spl0_13 ),
inference(backward_subsumption_resolution,[],[f239,f378]) ).
fof(f2582,plain,
( ! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| memberP(X1,X2)
| X0 = X2 )
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f2543,f378]) ).
fof(f2663,definition,
( spl0_88
<=> nil = app(sk7,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f2664,plain,
( nil != app(sk7,cons(sk5,nil))
| spl0_88 ),
inference(avatar_component_clause,[],[f2663]) ).
fof(f2665,plain,
( nil = app(sk7,cons(sk5,nil))
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f2663]) ).
fof(f2797,definition,
( spl0_93
<=> ssList(tl(sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f2798,plain,
( ssList(tl(sk8))
| ~ spl0_93 ),
inference(avatar_component_clause,[],[f2797]) ).
fof(f2799,plain,
( ~ ssList(tl(sk8))
| spl0_93 ),
inference(avatar_component_clause,[],[f2797]) ).
fof(f2810,plain,
( ~ ssList(sk8)
| nil = sk8
| spl0_93 ),
inference(resolution,[],[f2799,f75]) ).
fof(f2811,plain,
( nil = sk8
| spl0_93 ),
inference(forward_subsumption_resolution,[],[f2810,f209]) ).
fof(f2820,definition,
( spl0_97
<=> ! [X0] :
( app(X0,nil) != sk3
| app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f2821,plain,
( ! [X0] :
( app(X0,nil) != sk3
| app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) = X0
| ~ ssList(X0) )
| ~ spl0_97 ),
inference(avatar_component_clause,[],[f2820]) ).
fof(f2824,plain,
( spl0_15
| spl0_93 ),
inference(avatar_split_clause,[],[f2811,f2797,f653]) ).
fof(f2954,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssList(nil)
| memberP(nil,X0)
| sk9 = X0 )
| ~ spl0_3
| ~ spl0_13 ),
inference(superposition,[],[f2582,f330]) ).
fof(f2960,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| memberP(nil,X0)
| sk9 = X0 )
| ~ spl0_3
| ~ spl0_7
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f2954,f350]) ).
fof(f2962,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| sk9 = X0 )
| ~ spl0_3
| ~ spl0_7
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f2960,f388]) ).
fof(f3011,definition,
( spl0_98
<=> ssList(tl(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f3012,plain,
( ssList(tl(sk7))
| ~ spl0_98 ),
inference(avatar_component_clause,[],[f3011]) ).
fof(f3013,plain,
( ~ ssList(tl(sk7))
| spl0_98 ),
inference(avatar_component_clause,[],[f3011]) ).
fof(f3072,plain,
( ~ ssList(sk7)
| nil = sk7
| spl0_98 ),
inference(resolution,[],[f3013,f75]) ).
fof(f3073,plain,
( nil = sk7
| spl0_98 ),
inference(forward_subsumption_resolution,[],[f3072,f208]) ).
fof(f3074,plain,
( $false
| spl0_17
| spl0_98 ),
inference(forward_subsumption_resolution,[],[f3073,f663]) ).
fof(f3075,plain,
( spl0_17
| spl0_98 ),
inference(avatar_contradiction_clause,[],[f3074]) ).
fof(f3378,plain,
( ! [X0] :
( ~ ssList(X0)
| cons(sk9,X0) = app(cons(sk9,nil),X0) )
| ~ spl0_5 ),
inference(resolution,[],[f126,f341]) ).
fof(f3379,plain,
( ! [X0] :
( ~ ssList(X0)
| app(sk3,X0) = cons(sk9,X0) )
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f3378,f330]) ).
fof(f6918,plain,
( ! [X0] : cons(sk9,skaf82(X0)) = app(sk3,skaf82(X0))
| ~ spl0_3
| ~ spl0_5 ),
inference(resolution,[],[f3379,f13]) ).
fof(f6959,plain,
( cons(sk9,sk8) = app(sk3,sk8)
| ~ spl0_3
| ~ spl0_5 ),
inference(resolution,[],[f3379,f209]) ).
fof(f7088,plain,
( ~ ssList(app(nil,cons(sk5,nil)))
| ~ ssItem(sk6)
| ~ ssList(nil)
| memberP(app(app(nil,cons(sk5,nil)),cons(sk6,nil)),sk6)
| ~ spl0_21 ),
inference(resolution,[],[f758,f239]) ).
fof(f7129,plain,
( ~ ssItem(sk6)
| ~ ssList(nil)
| memberP(app(app(nil,cons(sk5,nil)),cons(sk6,nil)),sk6)
| ~ spl0_21
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f7088,f1118]) ).
fof(f7135,plain,
( ~ ssList(nil)
| memberP(app(app(nil,cons(sk5,nil)),cons(sk6,nil)),sk6)
| ~ spl0_21
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f7129,f207]) ).
fof(f7141,plain,
( memberP(app(app(nil,cons(sk5,nil)),cons(sk6,nil)),sk6)
| ~ spl0_7
| ~ spl0_21
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f7135,f350]) ).
fof(f7419,definition,
( spl0_258
<=> sk3 = app(app(nil,cons(sk5,nil)),cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_258])],[avatar_definition]) ).
fof(f7421,plain,
( sk3 = app(app(nil,cons(sk5,nil)),cons(sk6,nil))
| ~ spl0_258 ),
inference(avatar_component_clause,[],[f7419]) ).
fof(f7543,plain,
( frontsegP(sk3,nil)
| frontsegP(nil,sk3)
| nil = sk3
| ~ spl0_7 ),
inference(resolution,[],[f943,f350]) ).
fof(f7635,plain,
( frontsegP(sk3,nil)
| frontsegP(nil,sk3)
| spl0_1
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f7543,f320]) ).
fof(f7643,definition,
( spl0_280
<=> frontsegP(nil,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_280])],[avatar_definition]) ).
fof(f7645,plain,
( frontsegP(nil,sk3)
| ~ spl0_280 ),
inference(avatar_component_clause,[],[f7643]) ).
fof(f7647,definition,
( spl0_281
<=> frontsegP(sk3,nil) ),
introduced(definition,[new_symbols(definition,[spl0_281])],[avatar_definition]) ).
fof(f7649,plain,
( frontsegP(sk3,nil)
| ~ spl0_281 ),
inference(avatar_component_clause,[],[f7647]) ).
fof(f7650,plain,
( spl0_280
| spl0_281
| spl0_1
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f7635,f349,f319,f7647,f7643]) ).
fof(f7915,definition,
( spl0_293
<=> sk6 = sk9 ),
introduced(definition,[new_symbols(definition,[spl0_293])],[avatar_definition]) ).
fof(f7917,plain,
( sk6 = sk9
| ~ spl0_293 ),
inference(avatar_component_clause,[],[f7915]) ).
fof(f9043,plain,
( ~ ssList(app(sk4,sk3))
| ~ ssList(skaf43(sk9,sk4))
| ~ ssList(skaf42(sk4,sk9))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_14 ),
inference(superposition,[],[f2502,f2243]) ).
fof(f9078,plain,
( ~ ssList(app(sk4,sk3))
| ~ ssList(skaf42(sk4,sk9))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f9043,f52]) ).
fof(f9124,plain,
( ~ ssList(app(sk4,sk3))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f9078,f53]) ).
fof(f9168,plain,
( ~ ssList(sk4)
| ~ ssList(sk3)
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_14 ),
inference(resolution,[],[f9124,f85]) ).
fof(f9169,plain,
( ~ ssList(sk3)
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f9168,f203]) ).
fof(f9170,plain,
( $false
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f9169,f202]) ).
fof(f9171,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f9170]) ).
fof(f9364,plain,
( ! [X0,X1] :
( frontsegP(sk3,cons(X0,X1))
| ~ ssList(X1)
| sk9 = X0 )
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13 ),
inference(backward_subsumption_resolution,[],[f2476,f378]) ).
fof(f10870,definition,
( spl0_395
<=> ssList(app(sk3,cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_395])],[avatar_definition]) ).
fof(f10871,plain,
( ssList(app(sk3,cons(sk6,nil)))
| ~ spl0_395 ),
inference(avatar_component_clause,[],[f10870]) ).
fof(f11999,definition,
( spl0_402
<=> frontsegP(sk7,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_402])],[avatar_definition]) ).
fof(f12003,definition,
( spl0_403
<=> frontsegP(sk3,sk7) ),
introduced(definition,[new_symbols(definition,[spl0_403])],[avatar_definition]) ).
fof(f12005,plain,
( frontsegP(sk3,sk7)
| ~ spl0_403 ),
inference(avatar_component_clause,[],[f12003]) ).
fof(f12804,plain,
( frontsegP(sk3,app(sk3,cons(sk6,nil)))
| frontsegP(app(sk3,cons(sk6,nil)),sk3)
| sk3 = app(sk3,cons(sk6,nil))
| ~ spl0_395 ),
inference(resolution,[],[f10871,f943]) ).
fof(f12836,definition,
( spl0_446
<=> sk3 = app(sk3,cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_446])],[avatar_definition]) ).
fof(f12837,plain,
( sk3 != app(sk3,cons(sk6,nil))
| spl0_446 ),
inference(avatar_component_clause,[],[f12836]) ).
fof(f12838,plain,
( sk3 = app(sk3,cons(sk6,nil))
| ~ spl0_446 ),
inference(avatar_component_clause,[],[f12836]) ).
fof(f12840,definition,
( spl0_447
<=> frontsegP(app(sk3,cons(sk6,nil)),sk3) ),
introduced(definition,[new_symbols(definition,[spl0_447])],[avatar_definition]) ).
fof(f12841,plain,
( ~ frontsegP(app(sk3,cons(sk6,nil)),sk3)
| spl0_447 ),
inference(avatar_component_clause,[],[f12840]) ).
fof(f12842,plain,
( frontsegP(app(sk3,cons(sk6,nil)),sk3)
| ~ spl0_447 ),
inference(avatar_component_clause,[],[f12840]) ).
fof(f12844,definition,
( spl0_448
<=> frontsegP(sk3,app(sk3,cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_448])],[avatar_definition]) ).
fof(f13323,definition,
( spl0_477
<=> sk9 = hd(sk7) ),
introduced(definition,[new_symbols(definition,[spl0_477])],[avatar_definition]) ).
fof(f13325,plain,
( sk9 = hd(sk7)
| ~ spl0_477 ),
inference(avatar_component_clause,[],[f13323]) ).
fof(f16838,plain,
( ~ ssList(sk3)
| ~ spl0_281 ),
inference(resolution,[],[f7649,f257]) ).
fof(f16845,plain,
( $false
| ~ spl0_281 ),
inference(forward_subsumption_resolution,[],[f16838,f202]) ).
fof(f16846,plain,
~ spl0_281,
inference(avatar_contradiction_clause,[],[f16845]) ).
fof(f17020,definition,
( spl0_559
<=> sk3 = sk8 ),
introduced(definition,[new_symbols(definition,[spl0_559])],[avatar_definition]) ).
fof(f17024,definition,
( spl0_560
<=> segmentP(sk8,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_560])],[avatar_definition]) ).
fof(f17028,definition,
( spl0_561
<=> segmentP(sk3,sk8) ),
introduced(definition,[new_symbols(definition,[spl0_561])],[avatar_definition]) ).
fof(f17201,definition,
( spl0_580
<=> ssList(sk8) ),
introduced(definition,[new_symbols(definition,[spl0_580])],[avatar_definition]) ).
fof(f17202,plain,
( ssList(sk8)
| ~ spl0_580 ),
inference(avatar_component_clause,[],[f17201]) ).
fof(f17583,plain,
spl0_580,
inference(avatar_split_clause,[],[f209,f17201]) ).
fof(f17592,plain,
( ~ ssList(sk8)
| ~ ssList(sk3)
| sk3 = app(skaf46(sk3,sk8),sk8)
| ~ spl0_73 ),
inference(resolution,[],[f2185,f142]) ).
fof(f17595,plain,
( ~ ssList(sk8)
| sk3 = app(skaf46(sk3,sk8),sk8)
| ~ spl0_73 ),
inference(forward_subsumption_resolution,[],[f17592,f202]) ).
fof(f17604,definition,
( spl0_598
<=> sk3 = app(skaf46(sk3,sk8),sk8) ),
introduced(definition,[new_symbols(definition,[spl0_598])],[avatar_definition]) ).
fof(f17606,plain,
( sk3 = app(skaf46(sk3,sk8),sk8)
| ~ spl0_598 ),
inference(avatar_component_clause,[],[f17604]) ).
fof(f17898,definition,
( spl0_603
<=> sk9 = hd(sk8) ),
introduced(definition,[new_symbols(definition,[spl0_603])],[avatar_definition]) ).
fof(f17900,plain,
( sk9 = hd(sk8)
| ~ spl0_603 ),
inference(avatar_component_clause,[],[f17898]) ).
fof(f18206,plain,
( segmentP(sk8,sk3)
| segmentP(sk3,sk8)
| sk3 = sk8 ),
inference(resolution,[],[f895,f202]) ).
fof(f18213,plain,
( spl0_559
| spl0_561
| spl0_560 ),
inference(avatar_split_clause,[],[f18206,f17024,f17028,f17020]) ).
fof(f18484,plain,
( ~ segmentP(sk3,sk8)
| ~ ssList(sk3)
| ~ ssList(nil)
| ~ spl0_84 ),
inference(superposition,[],[f2413,f433]) ).
fof(f18486,plain,
( ~ segmentP(sk3,sk8)
| ~ ssList(nil)
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f18484,f202]) ).
fof(f18488,plain,
( ~ segmentP(sk3,sk8)
| ~ spl0_7
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f18486,f350]) ).
fof(f18489,plain,
( ~ spl0_561
| ~ spl0_7
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f18488,f2412,f349,f17028]) ).
fof(f20942,plain,
( sk3 = app(skaf46(sk3,sk8),sk8)
| ~ spl0_73
| ~ spl0_580 ),
inference(forward_subsumption_resolution,[],[f17595,f17202]) ).
fof(f21003,plain,
( spl0_598
| ~ spl0_73
| ~ spl0_580 ),
inference(avatar_split_clause,[],[f20942,f17201,f2183,f17604]) ).
fof(f21232,plain,
( sk7 = cons(sk9,tl(sk7))
| ~ spl0_18
| ~ spl0_477 ),
inference(superposition,[],[f668,f13325]) ).
fof(f21588,plain,
( sk8 = cons(sk9,tl(sk8))
| ~ spl0_16
| ~ spl0_603 ),
inference(superposition,[],[f659,f17900]) ).
fof(f21699,plain,
( tl(sk8) = skaf82(sk8)
| ~ spl0_13
| ~ spl0_54 ),
inference(superposition,[],[f517,f1845]) ).
fof(f24517,plain,
( ! [X0] :
( memberP(app(X0,sk8),hd(sk8))
| ~ ssList(X0)
| ~ ssList(tl(sk8)) )
| ~ spl0_13
| ~ spl0_16 ),
inference(superposition,[],[f1060,f659]) ).
fof(f24521,plain,
( ! [X0] :
( memberP(app(X0,sk8),hd(sk8))
| ~ ssList(X0) )
| ~ spl0_13
| ~ spl0_16
| ~ spl0_93 ),
inference(forward_subsumption_resolution,[],[f24517,f2798]) ).
fof(f26861,definition,
( spl0_782
<=> nil = cons(sk9,sk7) ),
introduced(definition,[new_symbols(definition,[spl0_782])],[avatar_definition]) ).
fof(f26862,plain,
( nil != cons(sk9,sk7)
| spl0_782 ),
inference(avatar_component_clause,[],[f26861]) ).
fof(f26863,plain,
( nil = cons(sk9,sk7)
| ~ spl0_782 ),
inference(avatar_component_clause,[],[f26861]) ).
fof(f26865,definition,
( spl0_783
<=> ssList(cons(sk9,sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_783])],[avatar_definition]) ).
fof(f26866,plain,
( ssList(cons(sk9,sk7))
| ~ spl0_783 ),
inference(avatar_component_clause,[],[f26865]) ).
fof(f26867,plain,
( ~ ssList(cons(sk9,sk7))
| spl0_783 ),
inference(avatar_component_clause,[],[f26865]) ).
fof(f27056,plain,
( ~ ssList(sk7)
| ~ spl0_13
| spl0_783 ),
inference(resolution,[],[f26867,f484]) ).
fof(f27057,plain,
( $false
| ~ spl0_13
| spl0_783 ),
inference(forward_subsumption_resolution,[],[f27056,f208]) ).
fof(f27058,plain,
( ~ spl0_13
| spl0_783 ),
inference(avatar_contradiction_clause,[],[f27057]) ).
fof(f28515,definition,
( spl0_861
<=> nil = cons(sk9,sk8) ),
introduced(definition,[new_symbols(definition,[spl0_861])],[avatar_definition]) ).
fof(f28516,plain,
( nil != cons(sk9,sk8)
| spl0_861 ),
inference(avatar_component_clause,[],[f28515]) ).
fof(f28517,plain,
( nil = cons(sk9,sk8)
| ~ spl0_861 ),
inference(avatar_component_clause,[],[f28515]) ).
fof(f28519,definition,
( spl0_862
<=> ssList(cons(sk9,sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_862])],[avatar_definition]) ).
fof(f28520,plain,
( ssList(cons(sk9,sk8))
| ~ spl0_862 ),
inference(avatar_component_clause,[],[f28519]) ).
fof(f28521,plain,
( ~ ssList(cons(sk9,sk8))
| spl0_862 ),
inference(avatar_component_clause,[],[f28519]) ).
fof(f28753,plain,
( ~ ssList(sk8)
| ~ spl0_13
| spl0_862 ),
inference(resolution,[],[f28521,f484]) ).
fof(f28754,plain,
( $false
| ~ spl0_13
| ~ spl0_580
| spl0_862 ),
inference(forward_subsumption_resolution,[],[f28753,f17202]) ).
fof(f28755,plain,
( ~ spl0_13
| ~ spl0_580
| spl0_862 ),
inference(avatar_contradiction_clause,[],[f28754]) ).
fof(f28975,definition,
( spl0_875
<=> sk3 = cons(sk9,sk8) ),
introduced(definition,[new_symbols(definition,[spl0_875])],[avatar_definition]) ).
fof(f28976,plain,
( sk3 != cons(sk9,sk8)
| spl0_875 ),
inference(avatar_component_clause,[],[f28975]) ).
fof(f32249,plain,
( ~ frontsegP(nil,sk3)
| ~ ssList(sk7)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_782 ),
inference(superposition,[],[f2484,f26863]) ).
fof(f32325,plain,
( ~ ssList(sk7)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_280
| ~ spl0_782 ),
inference(forward_subsumption_resolution,[],[f32249,f7645]) ).
fof(f32344,plain,
( $false
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_280
| ~ spl0_782 ),
inference(forward_subsumption_resolution,[],[f32325,f208]) ).
fof(f32345,plain,
( ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_280
| ~ spl0_782 ),
inference(avatar_contradiction_clause,[],[f32344]) ).
fof(f34341,plain,
( ~ frontsegP(nil,sk3)
| ~ ssList(sk8)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_861 ),
inference(superposition,[],[f2484,f28517]) ).
fof(f34418,plain,
( ~ ssList(sk8)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_280
| ~ spl0_861 ),
inference(forward_subsumption_resolution,[],[f34341,f7645]) ).
fof(f34436,plain,
( $false
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_280
| ~ spl0_580
| ~ spl0_861 ),
inference(forward_subsumption_resolution,[],[f34418,f17202]) ).
fof(f34437,plain,
( ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_280
| ~ spl0_580
| ~ spl0_861 ),
inference(avatar_contradiction_clause,[],[f34436]) ).
fof(f43058,plain,
( ~ frontsegP(sk7,sk3)
| ~ ssList(tl(sk7))
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_18
| ~ spl0_477 ),
inference(superposition,[],[f2484,f21232]) ).
fof(f43159,plain,
( ~ frontsegP(sk7,sk3)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_18
| ~ spl0_98
| ~ spl0_477 ),
inference(forward_subsumption_resolution,[],[f43058,f3012]) ).
fof(f43166,plain,
( ~ spl0_402
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_18
| ~ spl0_98
| ~ spl0_477 ),
inference(avatar_split_clause,[],[f43159,f13323,f3011,f666,f349,f339,f328,f11999]) ).
fof(f45701,plain,
( nil = tl(cons(sk9,sk7))
| tl(cons(sk9,sk7)) = cons(hd(tl(cons(sk9,sk7))),tl(tl(cons(sk9,sk7))))
| nil = cons(sk9,sk7)
| ~ spl0_783 ),
inference(resolution,[],[f647,f26866]) ).
fof(f45702,plain,
( nil = tl(cons(sk9,sk8))
| tl(cons(sk9,sk8)) = cons(hd(tl(cons(sk9,sk8))),tl(tl(cons(sk9,sk8))))
| nil = cons(sk9,sk8)
| ~ spl0_862 ),
inference(resolution,[],[f647,f28520]) ).
fof(f45751,plain,
( nil = tl(cons(sk9,sk8))
| tl(cons(sk9,sk8)) = cons(hd(tl(cons(sk9,sk8))),tl(tl(cons(sk9,sk8))))
| spl0_861
| ~ spl0_862 ),
inference(forward_subsumption_resolution,[],[f45702,f28516]) ).
fof(f45752,plain,
( nil = tl(cons(sk9,sk7))
| tl(cons(sk9,sk7)) = cons(hd(tl(cons(sk9,sk7))),tl(tl(cons(sk9,sk7))))
| spl0_782
| ~ spl0_783 ),
inference(forward_subsumption_resolution,[],[f45701,f26862]) ).
fof(f45800,plain,
( nil = sk8
| tl(cons(sk9,sk8)) = cons(hd(tl(cons(sk9,sk8))),tl(tl(cons(sk9,sk8))))
| ~ spl0_13
| spl0_861
| ~ spl0_862 ),
inference(forward_demodulation,[],[f45751,f550]) ).
fof(f45801,plain,
( nil = sk7
| tl(cons(sk9,sk7)) = cons(hd(tl(cons(sk9,sk7))),tl(tl(cons(sk9,sk7))))
| ~ spl0_13
| spl0_782
| ~ spl0_783 ),
inference(forward_demodulation,[],[f45752,f549]) ).
fof(f45811,plain,
( tl(cons(sk9,sk8)) = cons(hd(tl(cons(sk9,sk8))),tl(tl(cons(sk9,sk8))))
| ~ spl0_13
| spl0_15
| spl0_861
| ~ spl0_862 ),
inference(forward_subsumption_resolution,[],[f45800,f654]) ).
fof(f45819,plain,
( sk8 = cons(hd(sk8),tl(sk8))
| ~ spl0_13
| spl0_15
| spl0_861
| ~ spl0_862 ),
inference(forward_demodulation,[],[f45811,f550]) ).
fof(f45858,plain,
( nil = tl(cons(sk9,sk8))
| tl(cons(sk9,sk8)) = cons(skaf83(tl(cons(sk9,sk8))),skaf82(tl(cons(sk9,sk8))))
| nil = cons(sk9,sk8)
| ~ spl0_862 ),
inference(resolution,[],[f738,f28520]) ).
fof(f45899,plain,
( nil = tl(cons(sk9,sk8))
| tl(cons(sk9,sk8)) = cons(skaf83(tl(cons(sk9,sk8))),skaf82(tl(cons(sk9,sk8))))
| spl0_861
| ~ spl0_862 ),
inference(forward_subsumption_resolution,[],[f45858,f28516]) ).
fof(f45932,plain,
( nil = sk8
| tl(cons(sk9,sk8)) = cons(skaf83(tl(cons(sk9,sk8))),skaf82(tl(cons(sk9,sk8))))
| ~ spl0_13
| spl0_861
| ~ spl0_862 ),
inference(forward_demodulation,[],[f45899,f550]) ).
fof(f45943,plain,
( tl(cons(sk9,sk8)) = cons(skaf83(tl(cons(sk9,sk8))),skaf82(tl(cons(sk9,sk8))))
| ~ spl0_13
| spl0_15
| spl0_861
| ~ spl0_862 ),
inference(forward_subsumption_resolution,[],[f45932,f654]) ).
fof(f45951,plain,
( sk8 = cons(skaf83(sk8),skaf82(sk8))
| ~ spl0_13
| spl0_15
| spl0_861
| ~ spl0_862 ),
inference(forward_demodulation,[],[f45943,f550]) ).
fof(f51670,plain,
( ~ ssList(sk3)
| ~ ssList(sk3)
| ~ ssList(nil)
| memberP(sk3,sk6)
| ~ spl0_13
| ~ spl0_446 ),
inference(superposition,[],[f2547,f12838]) ).
fof(f51696,plain,
( ~ ssList(sk3)
| ~ ssList(nil)
| memberP(sk3,sk6)
| ~ spl0_13
| ~ spl0_446 ),
inference(duplicate_literal_removal,[],[f51670]) ).
fof(f51711,plain,
( ~ ssList(nil)
| memberP(sk3,sk6)
| ~ spl0_13
| ~ spl0_446 ),
inference(forward_subsumption_resolution,[],[f51696,f202]) ).
fof(f51726,plain,
( memberP(sk3,sk6)
| ~ spl0_7
| ~ spl0_13
| ~ spl0_446 ),
inference(forward_subsumption_resolution,[],[f51711,f350]) ).
fof(f51777,definition,
( spl0_1189
<=> memberP(sk3,sk6) ),
introduced(definition,[new_symbols(definition,[spl0_1189])],[avatar_definition]) ).
fof(f51778,plain,
( ~ memberP(sk3,sk6)
| spl0_1189 ),
inference(avatar_component_clause,[],[f51777]) ).
fof(f51779,plain,
( memberP(sk3,sk6)
| ~ spl0_1189 ),
inference(avatar_component_clause,[],[f51777]) ).
fof(f51786,plain,
( sk6 = sk9
| ~ spl0_3
| ~ spl0_7
| ~ spl0_13
| ~ spl0_1189 ),
inference(resolution,[],[f51779,f2962]) ).
fof(f56572,plain,
( memberP(sk3,hd(sk8))
| ~ ssList(skaf46(sk3,sk8))
| ~ spl0_13
| ~ spl0_16
| ~ spl0_93
| ~ spl0_598 ),
inference(superposition,[],[f24521,f17606]) ).
fof(f56579,plain,
( memberP(sk3,hd(sk8))
| ~ spl0_13
| ~ spl0_16
| ~ spl0_93
| ~ spl0_598 ),
inference(forward_subsumption_resolution,[],[f56572,f50]) ).
fof(f56602,plain,
( sk9 = hd(sk8)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_13
| ~ spl0_16
| ~ spl0_93
| ~ spl0_598 ),
inference(resolution,[],[f56579,f2962]) ).
fof(f57592,plain,
( sk3 != cons(sk9,nil)
| ~ spl0_15
| spl0_875 ),
inference(superposition,[],[f28976,f655]) ).
fof(f57731,plain,
( $false
| ~ spl0_3
| ~ spl0_15
| spl0_875 ),
inference(forward_subsumption_resolution,[],[f57592,f330]) ).
fof(f57732,plain,
( ~ spl0_3
| ~ spl0_15
| spl0_875 ),
inference(avatar_contradiction_clause,[],[f57731]) ).
fof(f62013,plain,
( spl0_16
| ~ spl0_13
| spl0_15
| spl0_861
| ~ spl0_862 ),
inference(avatar_split_clause,[],[f45819,f28519,f28515,f653,f377,f657]) ).
fof(f62015,plain,
( spl0_54
| ~ spl0_13
| spl0_15
| spl0_861
| ~ spl0_862 ),
inference(avatar_split_clause,[],[f45951,f28519,f28515,f653,f377,f1843]) ).
fof(f62283,definition,
( spl0_1517
<=> sk3 = app(sk7,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_1517])],[avatar_definition]) ).
fof(f62285,plain,
( sk3 = app(sk7,cons(sk5,nil))
| ~ spl0_1517 ),
inference(avatar_component_clause,[],[f62283]) ).
fof(f62296,definition,
( spl0_1520
<=> frontsegP(app(sk7,cons(sk5,nil)),sk3) ),
introduced(definition,[new_symbols(definition,[spl0_1520])],[avatar_definition]) ).
fof(f62298,plain,
( frontsegP(app(sk7,cons(sk5,nil)),sk3)
| ~ spl0_1520 ),
inference(avatar_component_clause,[],[f62296]) ).
fof(f62300,definition,
( spl0_1521
<=> frontsegP(sk3,app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_1521])],[avatar_definition]) ).
fof(f62373,definition,
( spl0_1535
<=> frontsegP(app(sk7,cons(sk5,nil)),sk7) ),
introduced(definition,[new_symbols(definition,[spl0_1535])],[avatar_definition]) ).
fof(f62374,plain,
( ~ frontsegP(app(sk7,cons(sk5,nil)),sk7)
| spl0_1535 ),
inference(avatar_component_clause,[],[f62373]) ).
fof(f62375,plain,
( frontsegP(app(sk7,cons(sk5,nil)),sk7)
| ~ spl0_1535 ),
inference(avatar_component_clause,[],[f62373]) ).
fof(f62895,plain,
( frontsegP(sk3,app(sk7,cons(sk5,nil)))
| frontsegP(app(sk7,cons(sk5,nil)),sk3)
| sk3 = app(sk7,cons(sk5,nil))
| ~ spl0_78 ),
inference(resolution,[],[f2207,f943]) ).
fof(f63146,plain,
( spl0_1517
| spl0_1520
| spl0_1521
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f62895,f2206,f62300,f62296,f62283]) ).
fof(f63870,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk6,nil))
| spl0_33 ),
inference(resolution,[],[f1268,f85]) ).
fof(f63871,plain,
( ~ ssList(cons(sk6,nil))
| spl0_33
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f63870,f2207]) ).
fof(f63872,plain,
( $false
| ~ spl0_25
| spl0_33
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f63871,f1114]) ).
fof(f63873,plain,
( ~ spl0_25
| spl0_33
| ~ spl0_78 ),
inference(avatar_contradiction_clause,[],[f63872]) ).
fof(f64767,definition,
( spl0_1616
<=> frontsegP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk7) ),
introduced(definition,[new_symbols(definition,[spl0_1616])],[avatar_definition]) ).
fof(f64768,plain,
( ~ frontsegP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk7)
| spl0_1616 ),
inference(avatar_component_clause,[],[f64767]) ).
fof(f64769,plain,
( frontsegP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk7)
| ~ spl0_1616 ),
inference(avatar_component_clause,[],[f64767]) ).
fof(f64777,definition,
( spl0_1618
<=> sk3 = app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_1618])],[avatar_definition]) ).
fof(f64779,plain,
( sk3 = app(app(sk7,cons(sk5,nil)),cons(sk6,nil))
| ~ spl0_1618 ),
inference(avatar_component_clause,[],[f64777]) ).
fof(f64921,plain,
( nil != nil
| ~ ssList(cons(sk6,nil))
| ~ ssList(app(sk7,cons(sk5,nil)))
| nil = app(sk7,cons(sk5,nil))
| ~ spl0_32 ),
inference(superposition,[],[f122,f1264]) ).
fof(f64936,plain,
( ~ ssList(cons(sk6,nil))
| ~ ssList(app(sk7,cons(sk5,nil)))
| nil = app(sk7,cons(sk5,nil))
| ~ spl0_32 ),
inference(trivial_inequality_removal,[],[f64921]) ).
fof(f64954,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| nil = app(sk7,cons(sk5,nil))
| ~ spl0_25
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f64936,f1114]) ).
fof(f64981,plain,
( nil = app(sk7,cons(sk5,nil))
| ~ spl0_25
| ~ spl0_32
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f64954,f2207]) ).
fof(f65004,plain,
( spl0_88
| ~ spl0_25
| ~ spl0_32
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f64981,f2206,f1262,f1113,f2663]) ).
fof(f65121,plain,
( ~ frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk6,nil))
| ~ spl0_70 ),
inference(resolution,[],[f2170,f963]) ).
fof(f65131,plain,
( ~ frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk6,nil))
| ~ spl0_70 ),
inference(duplicate_literal_removal,[],[f65121]) ).
fof(f65135,plain,
( ~ frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk6,nil))
| ~ spl0_70
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f65131,f2207]) ).
fof(f65137,plain,
( ~ frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ~ spl0_25
| ~ spl0_70
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f65135,f1114]) ).
fof(f65138,plain,
( ~ spl0_1521
| ~ spl0_25
| ~ spl0_70
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f65137,f2206,f2169,f1113,f62300]) ).
fof(f65187,plain,
( sk3 != sk3
| sk3 = app(app(sk7,cons(sk5,nil)),cons(sk6,nil))
| ~ ssList(sk3)
| ~ spl0_97 ),
inference(superposition,[],[f2821,f433]) ).
fof(f65191,plain,
( sk3 = app(app(sk7,cons(sk5,nil)),cons(sk6,nil))
| ~ ssList(sk3)
| ~ spl0_97 ),
inference(trivial_inequality_removal,[],[f65187]) ).
fof(f65193,plain,
( sk3 = app(app(sk7,cons(sk5,nil)),cons(sk6,nil))
| ~ spl0_97 ),
inference(forward_subsumption_resolution,[],[f65191,f202]) ).
fof(f65222,plain,
( spl0_1618
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f65193,f2820,f64777]) ).
fof(f65874,plain,
( ssList(app(sk3,cons(sk6,nil)))
| ~ spl0_33
| ~ spl0_1517 ),
inference(superposition,[],[f1267,f62285]) ).
fof(f65876,plain,
( ~ frontsegP(sk3,app(sk3,cons(sk6,nil)))
| spl0_71
| ~ spl0_1517 ),
inference(superposition,[],[f2175,f62285]) ).
fof(f65984,plain,
( ~ ssList(cons(sk5,nil))
| ~ ssList(sk3)
| ~ ssList(sk7)
| frontsegP(sk7,sk3)
| ~ spl0_1520 ),
inference(resolution,[],[f62298,f290]) ).
fof(f65985,plain,
( ~ ssList(cons(sk5,nil))
| ~ ssList(sk7)
| frontsegP(sk7,sk3)
| ~ spl0_1520 ),
inference(forward_subsumption_resolution,[],[f65984,f202]) ).
fof(f65988,plain,
( ~ ssList(cons(sk5,nil))
| frontsegP(sk7,sk3)
| ~ spl0_1520 ),
inference(forward_subsumption_resolution,[],[f65985,f208]) ).
fof(f66113,plain,
( spl0_395
| ~ spl0_33
| ~ spl0_1517 ),
inference(avatar_split_clause,[],[f65874,f62283,f1266,f10870]) ).
fof(f66114,plain,
( ~ spl0_448
| spl0_71
| ~ spl0_1517 ),
inference(avatar_split_clause,[],[f65876,f62283,f2173,f12844]) ).
fof(f66454,plain,
( frontsegP(sk3,app(sk3,cons(sk6,nil)))
| frontsegP(app(sk3,cons(sk6,nil)),sk3)
| ~ spl0_395
| spl0_446 ),
inference(forward_subsumption_resolution,[],[f12804,f12837]) ).
fof(f68102,plain,
( ~ ssList(sk3)
| ~ ssList(cons(sk6,nil))
| ~ spl0_447 ),
inference(resolution,[],[f12842,f963]) ).
fof(f68110,plain,
( ~ ssList(cons(sk6,nil))
| ~ spl0_447 ),
inference(forward_subsumption_resolution,[],[f68102,f202]) ).
fof(f68114,plain,
( $false
| ~ spl0_25
| ~ spl0_447 ),
inference(forward_subsumption_resolution,[],[f68110,f1114]) ).
fof(f68115,plain,
( ~ spl0_25
| ~ spl0_447 ),
inference(avatar_contradiction_clause,[],[f68114]) ).
fof(f68198,plain,
( spl0_1189
| ~ spl0_7
| ~ spl0_13
| ~ spl0_446 ),
inference(avatar_split_clause,[],[f51726,f12836,f377,f349,f51777]) ).
fof(f68287,plain,
( spl0_293
| ~ spl0_3
| ~ spl0_7
| ~ spl0_13
| ~ spl0_1189 ),
inference(avatar_split_clause,[],[f51786,f51777,f377,f349,f328,f7915]) ).
fof(f69886,plain,
( spl0_402
| ~ spl0_48
| ~ spl0_1520 ),
inference(avatar_split_clause,[],[f65988,f62296,f1475,f11999]) ).
fof(f70047,plain,
( sk7 = cons(hd(sk7),tl(sk7))
| nil = sk7
| ~ spl0_13
| spl0_782
| ~ spl0_783 ),
inference(forward_demodulation,[],[f45801,f549]) ).
fof(f71365,plain,
( spl0_603
| ~ spl0_3
| ~ spl0_7
| ~ spl0_13
| ~ spl0_16
| ~ spl0_93
| ~ spl0_598 ),
inference(avatar_split_clause,[],[f56602,f17604,f2797,f657,f377,f349,f328,f17898]) ).
fof(f71943,plain,
( ! [X0] :
( sk3 != app(X0,sk8)
| app(app(nil,cons(sk5,nil)),cons(sk6,nil)) = X0
| ~ ssList(X0) )
| ~ spl0_17
| ~ spl0_74 ),
inference(forward_demodulation,[],[f2189,f664]) ).
fof(f74169,plain,
( sk3 != cons(sk9,sk8)
| sk3 = app(app(nil,cons(sk5,nil)),cons(sk6,nil))
| ~ ssList(sk3)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_17
| ~ spl0_74 ),
inference(superposition,[],[f71943,f6959]) ).
fof(f74171,plain,
( sk3 != cons(sk9,sk8)
| sk3 = app(app(nil,cons(sk5,nil)),cons(sk6,nil))
| ~ spl0_3
| ~ spl0_5
| ~ spl0_17
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f74169,f202]) ).
fof(f74174,plain,
( spl0_258
| ~ spl0_875
| ~ spl0_3
| ~ spl0_5
| ~ spl0_17
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f74171,f2188,f662,f339,f328,f28975,f7419]) ).
fof(f78650,plain,
( sk3 != sk8
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| nil = app(app(sk7,cons(sk5,nil)),cons(sk6,nil))
| ~ spl0_7 ),
inference(superposition,[],[f1791,f223]) ).
fof(f83064,plain,
( ! [X0] :
( ~ segmentP(cons(sk9,skaf82(X0)),sk3)
| ~ ssList(skaf82(X0))
| ~ ssList(cons(sk9,skaf82(X0))) )
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7 ),
inference(superposition,[],[f2374,f6918]) ).
fof(f83113,plain,
( ! [X0] :
( ~ segmentP(cons(sk9,skaf82(X0)),sk3)
| ~ ssList(skaf82(X0)) )
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f83064,f484]) ).
fof(f83139,plain,
( ! [X0] : ~ segmentP(cons(sk9,skaf82(X0)),sk3)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f83113,f13]) ).
fof(f98203,plain,
( ~ segmentP(cons(sk9,tl(sk8)),sk3)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_54 ),
inference(superposition,[],[f83139,f21699]) ).
fof(f98204,plain,
( ~ segmentP(sk8,sk3)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_16
| ~ spl0_54
| ~ spl0_603 ),
inference(forward_demodulation,[],[f98203,f21588]) ).
fof(f99541,plain,
( ~ spl0_560
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_16
| ~ spl0_54
| ~ spl0_603 ),
inference(avatar_split_clause,[],[f98204,f17898,f1843,f657,f377,f349,f339,f328,f17024]) ).
fof(f99542,plain,
( sk3 != sk8
| nil = app(app(sk7,cons(sk5,nil)),cons(sk6,nil))
| ~ spl0_7
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f78650,f1267]) ).
fof(f101342,plain,
( sk3 != sk8
| ~ spl0_7
| spl0_32
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f99542,f1263]) ).
fof(f101648,plain,
( ~ spl0_559
| ~ spl0_7
| spl0_32
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f101342,f1266,f1262,f349,f17020]) ).
fof(f101901,plain,
( ! [X0] :
( app(X0,nil) != sk3
| ~ ssList(X0)
| app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) = X0 )
| ~ spl0_15
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f1787,f1267]) ).
fof(f102624,plain,
( spl0_97
| ~ spl0_15
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f101901,f1266,f653,f2820]) ).
fof(f107742,plain,
( frontsegP(sk3,app(sk3,cons(sk6,nil)))
| ~ spl0_395
| spl0_446
| spl0_447 ),
inference(forward_subsumption_resolution,[],[f66454,f12841]) ).
fof(f110558,plain,
( spl0_17
| spl0_18
| ~ spl0_13
| spl0_782
| ~ spl0_783 ),
inference(avatar_split_clause,[],[f70047,f26865,f26861,f377,f666,f662]) ).
fof(f111102,plain,
( frontsegP(sk3,sk7)
| ~ ssList(tl(sk7))
| sk9 = hd(sk7)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_18 ),
inference(superposition,[],[f9364,f668]) ).
fof(f111128,plain,
( frontsegP(sk3,sk7)
| sk9 = hd(sk7)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_18
| ~ spl0_98 ),
inference(forward_subsumption_resolution,[],[f111102,f3012]) ).
fof(f111164,plain,
( spl0_477
| spl0_403
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_18
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f111128,f3011,f666,f377,f349,f339,f328,f12003,f13323]) ).
fof(f113956,plain,
( nil != nil
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7)
| nil = cons(sk5,nil)
| ~ spl0_88 ),
inference(superposition,[],[f124,f2665]) ).
fof(f113967,plain,
( ~ ssList(cons(sk5,nil))
| ~ ssList(sk7)
| nil = cons(sk5,nil)
| ~ spl0_88 ),
inference(trivial_inequality_removal,[],[f113956]) ).
fof(f113979,plain,
( ~ ssList(sk7)
| nil = cons(sk5,nil)
| ~ spl0_48
| ~ spl0_88 ),
inference(forward_subsumption_resolution,[],[f113967,f1476]) ).
fof(f114008,plain,
( nil = cons(sk5,nil)
| ~ spl0_48
| ~ spl0_88 ),
inference(forward_subsumption_resolution,[],[f113979,f208]) ).
fof(f114028,plain,
( $false
| spl0_47
| ~ spl0_48
| ~ spl0_88 ),
inference(forward_subsumption_resolution,[],[f114008,f1472]) ).
fof(f114029,plain,
( spl0_47
| ~ spl0_48
| ~ spl0_88 ),
inference(avatar_contradiction_clause,[],[f114028]) ).
fof(f114875,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ spl0_1535 ),
inference(resolution,[],[f62375,f963]) ).
fof(f114883,plain,
( ~ ssList(cons(sk5,nil))
| ~ spl0_1535 ),
inference(forward_subsumption_resolution,[],[f114875,f208]) ).
fof(f114887,plain,
( $false
| ~ spl0_48
| ~ spl0_1535 ),
inference(forward_subsumption_resolution,[],[f114883,f1476]) ).
fof(f114888,plain,
( ~ spl0_48
| ~ spl0_1535 ),
inference(avatar_contradiction_clause,[],[f114887]) ).
fof(f128240,plain,
( sk3 = app(app(sk7,cons(sk5,nil)),cons(sk9,nil))
| ~ spl0_293
| ~ spl0_1618 ),
inference(forward_demodulation,[],[f64779,f7917]) ).
fof(f128241,plain,
( sk3 = app(app(sk7,cons(sk5,nil)),sk3)
| ~ spl0_3
| ~ spl0_293
| ~ spl0_1618 ),
inference(forward_demodulation,[],[f128240,f330]) ).
fof(f128250,plain,
( sk3 != sk3
| ~ ssList(app(sk7,cons(sk5,nil)))
| nil = app(sk7,cons(sk5,nil))
| ~ spl0_3
| ~ spl0_7
| ~ spl0_293
| ~ spl0_1618 ),
inference(superposition,[],[f1794,f128241]) ).
fof(f128276,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| nil = app(sk7,cons(sk5,nil))
| ~ spl0_3
| ~ spl0_7
| ~ spl0_293
| ~ spl0_1618 ),
inference(trivial_inequality_removal,[],[f128250]) ).
fof(f128288,plain,
( nil = app(sk7,cons(sk5,nil))
| ~ spl0_3
| ~ spl0_7
| ~ spl0_78
| ~ spl0_293
| ~ spl0_1618 ),
inference(forward_subsumption_resolution,[],[f128276,f2207]) ).
fof(f128297,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_78
| spl0_88
| ~ spl0_293
| ~ spl0_1618 ),
inference(forward_subsumption_resolution,[],[f128288,f2664]) ).
fof(f128298,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_78
| spl0_88
| ~ spl0_293
| ~ spl0_1618 ),
inference(avatar_contradiction_clause,[],[f128297]) ).
fof(f128334,plain,
( spl0_448
| ~ spl0_395
| spl0_446
| spl0_447 ),
inference(avatar_split_clause,[],[f107742,f12840,f12836,f10870,f12844]) ).
fof(f130166,plain,
( memberP(sk3,sk6)
| ~ spl0_7
| ~ spl0_21
| ~ spl0_26
| ~ spl0_258 ),
inference(superposition,[],[f7141,f7421]) ).
fof(f130226,plain,
( $false
| ~ spl0_7
| ~ spl0_21
| ~ spl0_26
| ~ spl0_258
| spl0_1189 ),
inference(forward_subsumption_resolution,[],[f130166,f51778]) ).
fof(f130227,plain,
( ~ spl0_7
| ~ spl0_21
| ~ spl0_26
| ~ spl0_258
| spl0_1189 ),
inference(avatar_contradiction_clause,[],[f130226]) ).
fof(f130598,plain,
( ~ frontsegP(sk3,sk7)
| ~ ssList(sk7)
| ~ spl0_70
| spl0_1616 ),
inference(resolution,[],[f64768,f2170]) ).
fof(f130603,plain,
( ~ ssList(sk7)
| ~ spl0_70
| ~ spl0_403
| spl0_1616 ),
inference(forward_subsumption_resolution,[],[f130598,f12005]) ).
fof(f130606,plain,
( $false
| ~ spl0_70
| ~ spl0_403
| spl0_1616 ),
inference(forward_subsumption_resolution,[],[f130603,f208]) ).
fof(f130607,plain,
( ~ spl0_70
| ~ spl0_403
| spl0_1616 ),
inference(avatar_contradiction_clause,[],[f130606]) ).
fof(f130610,plain,
( ~ ssList(cons(sk6,nil))
| ~ ssList(sk7)
| ~ ssList(app(sk7,cons(sk5,nil)))
| frontsegP(app(sk7,cons(sk5,nil)),sk7)
| ~ spl0_1616 ),
inference(resolution,[],[f64769,f290]) ).
fof(f130611,plain,
( ~ ssList(sk7)
| ~ ssList(app(sk7,cons(sk5,nil)))
| frontsegP(app(sk7,cons(sk5,nil)),sk7)
| ~ spl0_25
| ~ spl0_1616 ),
inference(forward_subsumption_resolution,[],[f130610,f1114]) ).
fof(f130614,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| frontsegP(app(sk7,cons(sk5,nil)),sk7)
| ~ spl0_25
| ~ spl0_1616 ),
inference(forward_subsumption_resolution,[],[f130611,f208]) ).
fof(f130617,plain,
( frontsegP(app(sk7,cons(sk5,nil)),sk7)
| ~ spl0_25
| ~ spl0_78
| ~ spl0_1616 ),
inference(forward_subsumption_resolution,[],[f130614,f2207]) ).
fof(f130618,plain,
( $false
| ~ spl0_25
| ~ spl0_78
| spl0_1535
| ~ spl0_1616 ),
inference(forward_subsumption_resolution,[],[f130617,f62374]) ).
fof(f130619,plain,
( ~ spl0_25
| ~ spl0_78
| spl0_1535
| ~ spl0_1616 ),
inference(avatar_contradiction_clause,[],[f130618]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f326]) ).
cnf(s2,plain,
( spl0_1
| spl0_3 ),
inference(sat_conversion,[],[f331]) ).
cnf(s5,plain,
( spl0_1
| spl0_5 ),
inference(sat_conversion,[],[f342]) ).
cnf(s13,plain,
( spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f382]) ).
cnf(s16,plain,
spl0_7,
inference(sat_conversion,[],[f385]) ).
cnf(s26,plain,
( spl0_21
| ~ spl0_25
| ~ spl0_26 ),
inference(sat_conversion,[],[f1120]) ).
cnf(s28,plain,
( ~ spl0_7
| spl0_25 ),
inference(sat_conversion,[],[f1152]) ).
cnf(s34,plain,
( ~ spl0_7
| ~ spl0_27 ),
inference(sat_conversion,[],[f1248]) ).
cnf(s35,plain,
( ~ spl0_7
| spl0_26 ),
inference(sat_conversion,[],[f1255]) ).
cnf(s60,plain,
( ~ spl0_7
| spl0_48 ),
inference(sat_conversion,[],[f1487]) ).
cnf(s67,plain,
( ~ spl0_7
| ~ spl0_47 ),
inference(sat_conversion,[],[f1543]) ).
cnf(s125,plain,
( ~ spl0_33
| spl0_70 ),
inference(sat_conversion,[],[f2171]) ).
cnf(s126,plain,
( ~ spl0_33
| ~ spl0_71 ),
inference(sat_conversion,[],[f2176]) ).
cnf(s128,plain,
( ~ spl0_33
| spl0_73 ),
inference(sat_conversion,[],[f2186]) ).
cnf(s130,plain,
( ~ spl0_33
| spl0_74 ),
inference(sat_conversion,[],[f2191]) ).
cnf(s161,plain,
( ~ spl0_1
| ~ spl0_25
| ~ spl0_78
| ~ spl0_83 ),
inference(sat_conversion,[],[f2390]) ).
cnf(s162,plain,
( ~ spl0_48
| spl0_78 ),
inference(sat_conversion,[],[f2398]) ).
cnf(s164,plain,
( ~ spl0_25
| spl0_27
| spl0_83 ),
inference(sat_conversion,[],[f2407]) ).
cnf(s166,plain,
( ~ spl0_33
| spl0_84 ),
inference(sat_conversion,[],[f2414]) ).
cnf(s181,plain,
( spl0_15
| spl0_93 ),
inference(sat_conversion,[],[f2824]) ).
cnf(s194,plain,
( spl0_17
| spl0_98 ),
inference(sat_conversion,[],[f3075]) ).
cnf(s459,plain,
( spl0_1
| ~ spl0_7
| spl0_280
| spl0_281 ),
inference(sat_conversion,[],[f7650]) ).
cnf(s564,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_14 ),
inference(sat_conversion,[],[f9171]) ).
cnf(s1047,plain,
~ spl0_281,
inference(sat_conversion,[],[f16846]) ).
cnf(s1150,plain,
spl0_580,
inference(sat_conversion,[],[f17583]) ).
cnf(s1228,plain,
( spl0_559
| spl0_560
| spl0_561 ),
inference(sat_conversion,[],[f18213]) ).
cnf(s1247,plain,
( ~ spl0_7
| ~ spl0_84
| ~ spl0_561 ),
inference(sat_conversion,[],[f18489]) ).
cnf(s1318,plain,
( ~ spl0_73
| ~ spl0_580
| spl0_598 ),
inference(sat_conversion,[],[f21003]) ).
cnf(s1699,plain,
( ~ spl0_13
| spl0_783 ),
inference(sat_conversion,[],[f27058]) ).
cnf(s1772,plain,
( ~ spl0_13
| ~ spl0_580
| spl0_862 ),
inference(sat_conversion,[],[f28755]) ).
cnf(s1806,plain,
( ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_280
| ~ spl0_782 ),
inference(sat_conversion,[],[f32345]) ).
cnf(s1838,plain,
( ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_280
| ~ spl0_580
| ~ spl0_861 ),
inference(sat_conversion,[],[f34437]) ).
cnf(s2036,plain,
( ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_18
| ~ spl0_98
| ~ spl0_402
| ~ spl0_477 ),
inference(sat_conversion,[],[f43166]) ).
cnf(s2912,plain,
( ~ spl0_3
| ~ spl0_15
| spl0_875 ),
inference(sat_conversion,[],[f57732]) ).
cnf(s3322,plain,
( ~ spl0_13
| spl0_15
| spl0_16
| spl0_861
| ~ spl0_862 ),
inference(sat_conversion,[],[f62013]) ).
cnf(s3324,plain,
( ~ spl0_13
| spl0_15
| spl0_54
| spl0_861
| ~ spl0_862 ),
inference(sat_conversion,[],[f62015]) ).
cnf(s3664,plain,
( ~ spl0_78
| spl0_1517
| spl0_1520
| spl0_1521 ),
inference(sat_conversion,[],[f63146]) ).
cnf(s3749,plain,
( ~ spl0_25
| spl0_33
| ~ spl0_78 ),
inference(sat_conversion,[],[f63873]) ).
cnf(s3854,plain,
( ~ spl0_25
| ~ spl0_32
| ~ spl0_78
| spl0_88 ),
inference(sat_conversion,[],[f65004]) ).
cnf(s3869,plain,
( ~ spl0_25
| ~ spl0_70
| ~ spl0_78
| ~ spl0_1521 ),
inference(sat_conversion,[],[f65138]) ).
cnf(s3873,plain,
( ~ spl0_97
| spl0_1618 ),
inference(sat_conversion,[],[f65222]) ).
cnf(s3996,plain,
( ~ spl0_33
| spl0_395
| ~ spl0_1517 ),
inference(sat_conversion,[],[f66113]) ).
cnf(s3997,plain,
( spl0_71
| ~ spl0_448
| ~ spl0_1517 ),
inference(sat_conversion,[],[f66114]) ).
cnf(s4299,plain,
( ~ spl0_25
| ~ spl0_447 ),
inference(sat_conversion,[],[f68115]) ).
cnf(s4328,plain,
( ~ spl0_7
| ~ spl0_13
| ~ spl0_446
| spl0_1189 ),
inference(sat_conversion,[],[f68198]) ).
cnf(s4343,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_13
| spl0_293
| ~ spl0_1189 ),
inference(sat_conversion,[],[f68287]) ).
cnf(s4575,plain,
( ~ spl0_48
| spl0_402
| ~ spl0_1520 ),
inference(sat_conversion,[],[f69886]) ).
cnf(s5060,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_13
| ~ spl0_16
| ~ spl0_93
| ~ spl0_598
| spl0_603 ),
inference(sat_conversion,[],[f71365]) ).
cnf(s5945,plain,
( ~ spl0_3
| ~ spl0_5
| ~ spl0_17
| ~ spl0_74
| spl0_258
| ~ spl0_875 ),
inference(sat_conversion,[],[f74174]) ).
cnf(s8931,plain,
( ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_16
| ~ spl0_54
| ~ spl0_560
| ~ spl0_603 ),
inference(sat_conversion,[],[f99541]) ).
cnf(s9590,plain,
( ~ spl0_7
| spl0_32
| ~ spl0_33
| ~ spl0_559 ),
inference(sat_conversion,[],[f101648]) ).
cnf(s10003,plain,
( ~ spl0_15
| ~ spl0_33
| spl0_97 ),
inference(sat_conversion,[],[f102624]) ).
cnf(s11243,plain,
( ~ spl0_13
| spl0_17
| spl0_18
| spl0_782
| ~ spl0_783 ),
inference(sat_conversion,[],[f110558]) ).
cnf(s11501,plain,
( ~ spl0_3
| ~ spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_18
| ~ spl0_98
| spl0_403
| spl0_477 ),
inference(sat_conversion,[],[f111164]) ).
cnf(s11780,plain,
( spl0_47
| ~ spl0_48
| ~ spl0_88 ),
inference(sat_conversion,[],[f114029]) ).
cnf(s11826,plain,
( ~ spl0_48
| ~ spl0_1535 ),
inference(sat_conversion,[],[f114888]) ).
cnf(s12743,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_78
| spl0_88
| ~ spl0_293
| ~ spl0_1618 ),
inference(sat_conversion,[],[f128298]) ).
cnf(s12806,plain,
( ~ spl0_395
| spl0_446
| spl0_447
| spl0_448 ),
inference(sat_conversion,[],[f128334]) ).
cnf(s13128,plain,
( ~ spl0_7
| ~ spl0_21
| ~ spl0_26
| ~ spl0_258
| spl0_1189 ),
inference(sat_conversion,[],[f130227]) ).
cnf(s13155,plain,
( ~ spl0_70
| ~ spl0_403
| spl0_1616 ),
inference(sat_conversion,[],[f130607]) ).
cnf(s13156,plain,
( ~ spl0_25
| ~ spl0_78
| spl0_1535
| ~ spl0_1616 ),
inference(sat_conversion,[],[f130619]) ).
cnf(s13215,plain,
( spl0_1
| ~ spl0_7
| spl0_280 ),
inference(rat,[],[s459,s1047]) ).
cnf(s13231,plain,
~ spl0_47,
inference(rat,[],[s67,s16]) ).
cnf(s13232,plain,
spl0_48,
inference(rat,[],[s60,s16]) ).
cnf(s13234,plain,
spl0_26,
inference(rat,[],[s35,s16]) ).
cnf(s13235,plain,
~ spl0_27,
inference(rat,[],[s34,s16]) ).
cnf(s13236,plain,
spl0_25,
inference(rat,[],[s28,s16]) ).
cnf(s13237,plain,
~ spl0_1535,
inference(rat,[],[s11826,s13232]) ).
cnf(s13238,plain,
~ spl0_88,
inference(rat,[],[s11780,s13231,s13232]) ).
cnf(s13241,plain,
spl0_78,
inference(rat,[],[s162,s13232]) ).
cnf(s13249,plain,
~ spl0_447,
inference(rat,[],[s4299,s13236]) ).
cnf(s13250,plain,
~ spl0_32,
inference(rat,[],[s3854,s13238,s13241,s13236]) ).
cnf(s13251,plain,
spl0_33,
inference(rat,[],[s3749,s13241,s13236]) ).
cnf(s13253,plain,
spl0_83,
inference(rat,[],[s164,s13235,s13236]) ).
cnf(s13254,plain,
~ spl0_1,
inference(rat,[],[s161,s13253,s13241,s13236]) ).
cnf(s13257,plain,
spl0_21,
inference(rat,[],[s26,s13234,s13236]) ).
cnf(s13258,plain,
~ spl0_1616,
inference(rat,[],[s13156,s13236,s13237,s13241]) ).
cnf(s13280,plain,
spl0_84,
inference(rat,[],[s166,s13251]) ).
cnf(s13283,plain,
spl0_74,
inference(rat,[],[s130,s13251]) ).
cnf(s13284,plain,
spl0_73,
inference(rat,[],[s128,s13251]) ).
cnf(s13285,plain,
~ spl0_71,
inference(rat,[],[s126,s13251]) ).
cnf(s13286,plain,
spl0_70,
inference(rat,[],[s125,s13251]) ).
cnf(s13287,plain,
~ spl0_559,
inference(rat,[],[s9590,s13250,s16,s13251]) ).
cnf(s13298,plain,
spl0_280,
inference(rat,[],[s13215,s16,s13254]) ).
cnf(s13311,plain,
~ spl0_561,
inference(rat,[],[s1247,s16,s13280]) ).
cnf(s13315,plain,
spl0_598,
inference(rat,[],[s1318,s1150,s13284]) ).
cnf(s13316,plain,
~ spl0_403,
inference(rat,[],[s13155,s13258,s13286]) ).
cnf(s13317,plain,
~ spl0_1521,
inference(rat,[],[s3869,s13236,s13241,s13286]) ).
cnf(s13319,plain,
spl0_560,
inference(rat,[],[s1228,s13311,s13287]) ).
cnf(s13381,plain,
spl0_5,
inference(rat,[],[s5,s13254]) ).
cnf(s13382,plain,
spl0_3,
inference(rat,[],[s2,s13254]) ).
cnf(s13396,plain,
~ spl0_861,
inference(rat,[],[s1838,s13381,s1150,s13298,s16,s13382]) ).
cnf(s13397,plain,
~ spl0_782,
inference(rat,[],[s1806,s13381,s13298,s16,s13382]) ).
cnf(s13401,plain,
spl0_2,
inference(rat,[],[s1,s13254]) ).
cnf(s13402,plain,
~ spl0_14,
inference(rat,[],[s564,s13382,s16,s13381,s13401]) ).
cnf(s13404,plain,
spl0_13,
inference(rat,[],[s13,s13402]) ).
cnf(s13454,plain,
spl0_862,
inference(rat,[],[s1772,s1150,s13404]) ).
cnf(s13455,plain,
spl0_783,
inference(rat,[],[s1699,s13404]) ).
cnf(s13558,plain,
spl0_15,
inference(rat,[],[s5060,s8931,s181,s3322,s3324,s16,s13382,s13404,s13315,s13381,s13319,s13396,s13454]) ).
cnf(s13566,plain,
spl0_97,
inference(rat,[],[s10003,s13251,s13558]) ).
cnf(s13593,plain,
spl0_875,
inference(rat,[],[s2912,s13382,s13558]) ).
cnf(s13612,plain,
spl0_1618,
inference(rat,[],[s3873,s13566]) ).
cnf(s13631,plain,
~ spl0_293,
inference(rat,[],[s12743,s13382,s13241,s13238,s16,s13612]) ).
cnf(s13639,plain,
~ spl0_1189,
inference(rat,[],[s4343,s13404,s13382,s16,s13631]) ).
cnf(s13643,plain,
~ spl0_258,
inference(rat,[],[s13128,s13257,s13234,s16,s13639]) ).
cnf(s13644,plain,
~ spl0_446,
inference(rat,[],[s4328,s13404,s16,s13639]) ).
cnf(s13648,plain,
~ spl0_17,
inference(rat,[],[s5945,s13593,s13382,s13283,s13381,s13643]) ).
cnf(s13656,plain,
spl0_18,
inference(rat,[],[s11243,s13455,s13397,s13404,s13648]) ).
cnf(s13675,plain,
spl0_98,
inference(rat,[],[s194,s13648]) ).
cnf(s13793,plain,
spl0_477,
inference(rat,[],[s11501,s13656,s13316,s13404,s13382,s13381,s16,s13675]) ).
cnf(s13843,plain,
~ spl0_402,
inference(rat,[],[s2036,s13675,s13656,s13382,s13381,s16,s13793]) ).
cnf(s13864,plain,
~ spl0_1520,
inference(rat,[],[s4575,s13232,s13843]) ).
cnf(s13904,plain,
spl0_1517,
inference(rat,[],[s3664,s13317,s13241,s13864]) ).
cnf(s13938,plain,
spl0_395,
inference(rat,[],[s3996,s13251,s13904]) ).
cnf(s13939,plain,
~ spl0_448,
inference(rat,[],[s3997,s13285,s13904]) ).
cnf(s13943,plain,
$false,
inference(rat,[],[s12806,s13644,s13249,s13939,s13938]) ).
fof(f130620,plain,
$false,
inference(avatar_sat_refutation,[],[s13943]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWC192-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.03/0.32 % Computer : n012.cluster.edu
% 0.03/0.32 % Model : x86_64 x86_64
% 0.03/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.32 % Memory : 8046.5625MB
% 0.03/0.32 % OS : Linux 6.8.0-71-generic
% 0.03/0.32 % CPULimit : 300
% 0.03/0.32 % WCLimit : 300
% 0.03/0.32 % DateTime : Mon Sep 28 08:21:49 UTC 2026
% 0.03/0.32 % CPUTime :
% 0.03/0.32 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.33 Running first-order model finding
% 0.07/0.33 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
% 7.65/1.51 % (3233425)Will run a generic schedule for satisfiability detection.
% 7.65/1.51 % (3233431)% WARNING: option uhcvi not known.
% 7.65/1.51 % (3233435)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2087686683:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.65/1.51 % (3233431)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1085258348:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.65/1.51 % (3233432)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=223772481:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.65/1.51 % (3233433)dis+10_1_sil=32000:sp=arity:random_seed=1385846888:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.65/1.51 % (3233430)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1998289630_2999 on theBenchmark for (2999ds/0Mi)
% 7.65/1.51 % (3233434)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1297203418:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.65/1.51 % (3233436)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4053355029:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.65/1.51 % TRYING [1]
% 7.65/1.51 % TRYING [2]
% 7.65/1.51 % TRYING [3]
% 7.65/1.51 % TRYING [4]
% 7.65/1.51 % (3233433)Instruction limit reached!
% 7.65/1.51 % (3233433)------------------------------
% 7.65/1.51 % (3233433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.65/1.51 % (3233433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.65/1.51 % (3233433)CaDiCaL version: 2.1.3
% 7.65/1.51 % (3233433)Termination reason: Instruction limit
% 7.65/1.51 % (3233433)Termination phase: Saturation
% 7.65/1.51 % (3233433)Time elapsed: 0.032 s
% 7.65/1.51 % (3233433)Peak memory usage: 13 MB
% 7.65/1.51 % (3233433)Instructions burned: 103 (million)
% 7.65/1.51 % (3233434)Instruction limit reached!
% 7.65/1.51 % (3233434)------------------------------
% 7.65/1.51 % (3233434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.65/1.51 % (3233434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.65/1.51 % (3233434)CaDiCaL version: 2.1.3
% 7.65/1.51 % (3233434)Termination reason: Instruction limit
% 7.65/1.51 % (3233434)Termination phase: Saturation
% 7.65/1.51 % (3233434)Time elapsed: 0.033 s
% 7.65/1.51 % (3233434)Peak memory usage: 13 MB
% 7.65/1.51 % (3233434)Instructions burned: 120 (million)
% 7.65/1.51 % (3233435)Instruction limit reached!
% 7.65/1.51 % (3233435)------------------------------
% 7.65/1.51 % (3233435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.65/1.51 % (3233435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.65/1.51 % (3233435)CaDiCaL version: 2.1.3
% 7.65/1.51 % (3233435)Termination reason: Instruction limit
% 7.65/1.51 % (3233435)Termination phase: Saturation
% 7.65/1.51 % (3233435)Time elapsed: 0.040 s
% 7.65/1.51 % (3233435)Peak memory usage: 14 MB
% 7.65/1.51 % (3233435)Instructions burned: 145 (million)
% 7.65/1.51 % (3233445)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3743527990:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.65/1.51 % (3233444)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4078559803:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.65/1.51 % (3233436)Instruction limit reached!
% 7.65/1.51 % (3233436)------------------------------
% 7.65/1.51 % (3233436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.65/1.51 % (3233436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.65/1.51 % (3233436)CaDiCaL version: 2.1.3
% 7.65/1.51 % (3233436)Termination reason: Instruction limit
% 7.65/1.51 % (3233436)Termination phase: Saturation
% 7.65/1.51 % (3233436)Time elapsed: 0.049 s
% 7.65/1.51 % (3233436)Peak memory usage: 14 MB
% 7.65/1.51 % (3233436)Instructions burned: 162 (million)
% 7.65/1.51 % (3233446)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=2240374964:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 7.65/1.51 % TRYING [1]
% 7.65/1.51 % TRYING [2]
% 7.65/1.51 % TRYING [3]
% 7.65/1.51 % (3233449)ott-21_1_sil=16000:fs=off:random_seed=2815233483:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 7.65/1.51 % TRYING [5]
% 7.65/1.51 % TRYING [4]
% 7.65/1.51 % (3233445)Instruction limit reached!
% 7.65/1.51 % (3233445)------------------------------
% 7.65/1.51 % (3233445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.66/2.38 % (3233445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.38 % (3233445)CaDiCaL version: 2.1.3
% 13.66/2.38 % (3233445)Termination reason: Instruction limit
% 13.66/2.38 % (3233445)Termination phase: Saturation
% 13.66/2.38 % (3233445)Time elapsed: 0.039 s
% 13.66/2.38 % (3233445)Peak memory usage: 14 MB
% 13.66/2.38 % (3233445)Instructions burned: 131 (million)
% 13.66/2.38 % (3233452)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=251906102:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 13.66/2.38 % TRYING [5]
% 13.66/2.38 % (3233449)Instruction limit reached!
% 13.66/2.38 % (3233449)------------------------------
% 13.66/2.38 % (3233449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.66/2.38 % (3233449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.38 % (3233449)CaDiCaL version: 2.1.3
% 13.66/2.38 % (3233449)Termination reason: Instruction limit
% 13.66/2.38 % (3233449)Termination phase: Saturation
% 13.66/2.38 % (3233449)Time elapsed: 0.047 s
% 13.66/2.38 % (3233449)Peak memory usage: 13 MB
% 13.66/2.38 % (3233449)Instructions burned: 182 (million)
% 13.66/2.38 % (3233454)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=505299877:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 13.66/2.38 % TRYING [1]
% 13.66/2.38 % TRYING [2]
% 13.66/2.38 % TRYING [3]
% 13.66/2.38 % TRYING [6]
% 13.66/2.38 % TRYING [4]
% 13.66/2.38 % TRYING [6]
% 13.66/2.38 % (3233444)Instruction limit reached!
% 13.66/2.38 % (3233444)------------------------------
% 13.66/2.38 % (3233444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.66/2.38 % (3233444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.38 % (3233444)CaDiCaL version: 2.1.3
% 13.66/2.38 % (3233444)Termination reason: Instruction limit
% 13.66/2.38 % (3233444)Termination phase: Finite model building constraint generation
% 13.66/2.38 % (3233444)Time elapsed: 0.156 s
% 13.66/2.38 % (3233444)Peak memory usage: 34 MB
% 13.66/2.38 % (3233444)Instructions burned: 716 (million)
% 13.66/2.38 % TRYING [5]
% 13.66/2.38 % (3233456)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1362406668:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 13.66/2.38 % (3233452)Instruction limit reached!
% 13.66/2.38 % (3233452)------------------------------
% 13.66/2.38 % (3233452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.66/2.38 % (3233452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.38 % (3233452)CaDiCaL version: 2.1.3
% 13.66/2.38 % (3233452)Termination reason: Instruction limit
% 13.66/2.38 % (3233452)Termination phase: Saturation
% 13.66/2.38 % (3233452)Time elapsed: 0.157 s
% 13.66/2.38 % (3233452)Peak memory usage: 15 MB
% 13.66/2.38 % (3233452)Instructions burned: 477 (million)
% 13.66/2.38 % (3233458)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3818675600:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 13.66/2.38 % (3233446)Instruction limit reached!
% 13.66/2.38 % (3233446)------------------------------
% 13.66/2.38 % (3233446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.66/2.38 % (3233446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.38 % (3233446)CaDiCaL version: 2.1.3
% 13.66/2.38 % (3233446)Termination reason: Instruction limit
% 13.66/2.38 % (3233446)Termination phase: Saturation
% 13.66/2.38 % (3233446)Time elapsed: 0.217 s
% 13.66/2.38 % (3233446)Peak memory usage: 21 MB
% 13.66/2.38 % (3233446)Instructions burned: 686 (million)
% 13.66/2.38 % (3233460)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=4069578484:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 13.66/2.38 % (3233454)Instruction limit reached!
% 13.66/2.38 % (3233454)------------------------------
% 13.66/2.38 % (3233454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.66/2.38 % (3233454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.38 % (3233454)CaDiCaL version: 2.1.3
% 13.66/2.38 % (3233454)Termination reason: Instruction limit
% 13.66/2.38 % (3233454)Termination phase: Finite model building SAT solving
% 13.66/2.38 % (3233454)Time elapsed: 0.181 s
% 13.66/2.38 % (3233454)Peak memory usage: 22 MB
% 13.66/2.38 % (3233454)Instructions burned: 870 (million)
% 13.66/2.38 % (3233462)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1806462098:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 13.66/2.38 % TRYING [14]
% 13.66/2.38 % TRYING [7]
% 13.66/2.38 % (3233458)Instruction limit reached!
% 13.66/2.38 % (3233458)------------------------------
% 13.66/2.38 % (3233458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.66/2.38 % (3233458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.38 % (3233458)CaDiCaL version: 2.1.3
% 13.66/2.38 % (3233458)Termination reason: Instruction limit
% 13.66/2.38 % (3233458)Termination phase: Finite model building constraint generation
% 13.66/2.38 % (3233458)Time elapsed: 0.182 s
% 13.66/2.38 % (3233458)Peak memory usage: 72 MB
% 13.66/2.38 % (3233458)Instructions burned: 893 (million)
% 13.66/2.38 % (3233464)fmb+10_1_sil=64000:random_seed=32447965:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 13.66/2.38 % TRYING [1]
% 13.66/2.38 % TRYING [2]
% 13.66/2.38 % TRYING [3]
% 13.66/2.38 % (3233460)Instruction limit reached!
% 13.66/2.38 % (3233460)------------------------------
% 13.66/2.38 % (3233460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.66/2.38 % (3233460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.38 % (3233460)CaDiCaL version: 2.1.3
% 13.66/2.38 % (3233460)Termination reason: Instruction limit
% 13.66/2.38 % (3233460)Termination phase: Saturation
% 13.66/2.38 % (3233460)Time elapsed: 0.210 s
% 13.66/2.38 % (3233460)Peak memory usage: 19 MB
% 13.66/2.38 % (3233460)Instructions burned: 694 (million)
% 13.66/2.38 % (3233466)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=733801196:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 13.66/2.38 % TRYING [4]
% 13.66/2.38 % TRYING [20]
% 13.66/2.38 % (3233462)Instruction limit reached!
% 13.66/2.38 % (3233462)------------------------------
% 13.66/2.38 % (3233462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.66/2.38 % (3233462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.38 % (3233462)CaDiCaL version: 2.1.3
% 13.66/2.38 % (3233462)Termination reason: Instruction limit
% 13.66/2.38 % (3233462)Termination phase: Saturation
% 13.66/2.38 % (3233462)Time elapsed: 0.253 s
% 13.66/2.38 % (3233462)Peak memory usage: 20 MB
% 13.66/2.38 % (3233462)Instructions burned: 881 (million)
% 13.66/2.38 % (3233456)Instruction limit reached!
% 13.66/2.38 % (3233456)------------------------------
% 13.66/2.38 % (3233456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.66/2.38 % (3233456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.38 % (3233456)CaDiCaL version: 2.1.3
% 13.66/2.38 % (3233456)Termination reason: Instruction limit
% 13.66/2.38 % (3233456)Termination phase: Saturation
% 13.66/2.38 % (3233456)Time elapsed: 0.362 s
% 13.66/2.38 % (3233456)Peak memory usage: 26 MB
% 13.66/2.38 % (3233456)Instructions burned: 1181 (million)
% 13.66/2.38 % (3233468)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=601683437:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 13.66/2.38 % TRYING [8]
% 13.66/2.38 % TRYING [5]
% 13.66/2.38 % (3233470)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=503637755:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 13.66/2.38 % (3233468)Instruction limit reached!
% 13.66/2.38 % (3233468)------------------------------
% 13.66/2.38 % (3233468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.66/2.38 % (3233468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.38 % (3233468)CaDiCaL version: 2.1.3
% 13.66/2.38 % (3233468)Termination reason: Instruction limit
% 13.66/2.38 % (3233468)Termination phase: Finite model building constraint generation
% 13.66/2.38 % (3233468)Time elapsed: 0.183 s
% 13.66/2.38 % (3233468)Peak memory usage: 79 MB
% 13.66/2.38 % (3233468)Instructions burned: 924 (million)
% 13.66/2.38 % (3233472)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1221615346:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 13.66/2.38 % TRYING [6]
% 13.66/2.38 % TRYING [8]
% 13.66/2.38 % (3233472)Instruction limit reached!
% 13.66/2.38 % (3233472)------------------------------
% 13.66/2.38 % (3233472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.66/2.38 % (3233472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.38 % (3233472)CaDiCaL version: 2.1.3
% 13.66/2.38 % (3233472)Termination reason: Instruction limit
% 13.66/2.38 % (3233472)Termination phase: Saturation
% 13.66/2.38 % (3233472)Time elapsed: 0.349 s
% 13.66/2.38 % (3233472)Peak memory usage: 16 MB
% 13.66/2.38 % (3233472)Instructions burned: 1474 (million)
% 13.66/2.38 % (3233474)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=563100872:i=6324_2988 on theBenchmark for (2988ds/6324Mi)
% 13.66/2.38 % TRYING [77]
% 13.66/2.38 % TRYING [7]
% 13.66/2.38 % (3233431) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3233425-3233431"...
% 13.66/2.38 % (3233431)...printing done.
% 13.66/2.38 % (3233431)Refutation found. Thanks to Tanya!
% 13.66/2.38 % SZS status Unsatisfiable for theBenchmark
% 13.66/2.38 % SZS output start Proof for theBenchmark
% See solution above
% 13.66/2.38 % (3233431)------------------------------
% 13.66/2.38 % (3233431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.66/2.38 % (3233431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.38 % (3233431)CaDiCaL version: 2.1.3
% 13.66/2.38 % (3233431)Termination reason: Refutation
% 13.66/2.38 % (3233431)Time elapsed: 1.959 s
% 13.66/2.38 % (3233431)Peak memory usage: 63 MB
% 13.66/2.38 % (3233431)Instructions burned: 6151 (million)
% 13.66/2.38 % (3233425)Success in time 2.039 s
% 13.66/2.38 % Vampire exiting
%------------------------------------------------------------------------------