%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC306-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:05:28 PM UTC 2026
% Result : Unsatisfiable 48.41s 7.11s
% Output : Refutation 48.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 83
% Syntax : Number of formulae : 473 ( 60 unt; 41 def)
% Number of atoms : 1635 ( 220 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 2186 (1024 ~;1121 |; 0 &)
% ( 41 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 49 ( 47 usr; 42 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 9 con; 0-2 aty)
% Number of variables : 240 ( 0 sgn 240 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f13,axiom,
! [X0] : ssList(skaf82(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause13) ).
fof(f52,axiom,
! [X0,X1] : ssList(skaf43(X0,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause52) ).
fof(f53,axiom,
! [X0,X1] : ssList(skaf42(X0,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause53) ).
fof(f56,axiom,
! [X0] :
( segmentP(X0,nil)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause56) ).
fof(f60,axiom,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause60) ).
fof(f71,axiom,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause71) ).
fof(f72,axiom,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f73,axiom,
! [X0] :
( ~ ssList(X0)
| app(X0,nil) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause73) ).
fof(f74,axiom,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause74) ).
fof(f75,axiom,
! [X0] :
( ssList(tl(X0))
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause75) ).
fof(f76,axiom,
! [X0] :
( ~ ssList(X0)
| ssItem(hd(X0))
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause76) ).
fof(f85,axiom,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ssList(cons(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause86) ).
fof(f96,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| tl(cons(X0,X1)) = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause96) ).
fof(f98,axiom,
! [X0,X1] :
( cons(X0,X1) != nil
| ~ ssItem(X0)
| ~ ssList(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause98) ).
fof(f99,plain,
! [X0,X1] :
( nil != cons(X0,X1)
| ~ ssItem(X0)
| ~ ssList(X1) ),
inference(reorient_equations,[],[f98]) ).
fof(f107,axiom,
! [X0] :
( ~ ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause104) ).
fof(f112,axiom,
! [X0] :
( ~ ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause109) ).
fof(f123,axiom,
! [X0,X1] :
( app(X0,X1) != nil
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X1 ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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(f149,axiom,
! [X2,X0,X1] :
( X0 != X1
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0)
| memberP(cons(X1,X2),X0) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/SWC001-0.ax',clause141) ).
fof(f155,axiom,
! [X2,X0,X1] :
( app(X0,X1) != X2
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| frontsegP(X2,X0) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/SWC001-0.ax',clause169) ).
fof(f183,axiom,
! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X3)
| ~ ssList(X1)
| X0 = X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause170) ).
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/sandbox/benchmark/Axioms/SWC001-0.ax',clause173) ).
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/sandbox/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/sandbox/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(f202,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_3) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
ssItem(sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
ssList(sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_10) ).
fof(f210,negated_conjecture,
ssList(sk9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).
fof(f211,negated_conjecture,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_12) ).
fof(f212,plain,
sk1 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(reorient_equations,[],[f211]) ).
fof(f215,negated_conjecture,
( ssItem(sk10)
| nil = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_15) ).
fof(f219,negated_conjecture,
( cons(sk10,nil) = sk3
| nil = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_18) ).
fof(f220,plain,
( sk3 = cons(sk10,nil)
| nil = sk3 ),
inference(reorient_equations,[],[f219]) ).
fof(f224,plain,
sk3 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(definition_unfolding,[],[f212,f205]) ).
fof(f234,plain,
! [X2,X1] :
( ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X1)
| memberP(cons(X1,X2),X1) ),
inference(equality_resolution,[],[f149]) ).
fof(f236,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1))
| frontsegP(app(X0,X1),X0) ),
inference(equality_resolution,[],[f155]) ).
fof(f239,plain,
! [X2,X0,X1] :
( ~ ssList(app(app(X0,X1),X2))
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| segmentP(app(app(X0,X1),X2),X1) ),
inference(equality_resolution,[],[f187]) ).
fof(f241,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(f242,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(f283,plain,
! [X0] :
( ~ memberP(nil,X0)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f71]) ).
fof(f284,plain,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ~ ssItem(X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f285,plain,
! [X0] :
( ~ ssItem(hd(X0))
| ~ ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f289,plain,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f297,plain,
! [X0,X1] :
( ~ ssList(X1)
| ssItem(X0)
| tl(cons(X0,X1)) = X1 ),
inference(consistent_polarity_flipping,[],[f96]) ).
fof(f299,plain,
! [X0,X1] :
( nil != cons(X0,X1)
| ssItem(X0)
| ~ ssList(X1) ),
inference(consistent_polarity_flipping,[],[f99]) ).
fof(f315,plain,
! [X0,X1] :
( ~ ssList(X1)
| ssItem(X0)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f327,plain,
! [X2,X1] :
( ~ ssList(X2)
| ssItem(X1)
| ssItem(X1)
| memberP(cons(X1,X2),X1) ),
inference(consistent_polarity_flipping,[],[f234]) ).
fof(f330,plain,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ssItem(X1)
| memberP(app(X2,X0),X1) ),
inference(consistent_polarity_flipping,[],[f152]) ).
fof(f343,plain,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ssItem(X0)
| ssItem(X2)
| memberP(X1,X2)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f347,plain,
! [X0,X1] :
( ~ memberP(X0,X1)
| ssItem(X1)
| ~ ssList(X0)
| app(skaf42(X0,X1),cons(X1,skaf43(X1,X0))) = X0 ),
inference(consistent_polarity_flipping,[],[f182]) ).
fof(f348,plain,
! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| ssItem(X2)
| ssItem(X0)
| ~ ssList(X3)
| ~ ssList(X1)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f183]) ).
fof(f353,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,[],[f241]) ).
fof(f354,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,[],[f242]) ).
fof(f361,plain,
~ ssItem(sk5),
inference(consistent_polarity_flipping,[],[f206]) ).
fof(f362,plain,
~ ssItem(sk6),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f364,plain,
( ~ ssItem(sk10)
| nil = sk3 ),
inference(consistent_polarity_flipping,[],[f215]) ).
fof(f365,plain,
! [X3,X0,X1] :
( frontsegP(cons(X3,X0),cons(X3,X1))
| ~ ssList(X1)
| ~ ssList(X0)
| ssItem(X3)
| ~ frontsegP(X0,X1) ),
inference(duplicate_literal_removal,[],[f353]) ).
fof(f367,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ssItem(X1)
| ~ ssList(X2) ),
inference(duplicate_literal_removal,[],[f327]) ).
fof(f372,definition,
( spl0_1
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f373,plain,
( nil != sk3
| spl0_1 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f374,plain,
( nil = sk3
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f381,definition,
( spl0_3
<=> sk3 = cons(sk10,nil) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f383,plain,
( sk3 = cons(sk10,nil)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f381]) ).
fof(f384,plain,
( spl0_1
| spl0_3 ),
inference(avatar_split_clause,[],[f220,f381,f372]) ).
fof(f392,definition,
( spl0_5
<=> ssItem(sk10) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f394,plain,
( ~ ssItem(sk10)
| spl0_5 ),
inference(avatar_component_clause,[],[f392]) ).
fof(f395,plain,
( spl0_1
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f364,f392,f372]) ).
fof(f402,definition,
( spl0_7
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f403,plain,
( ssList(nil)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f430,definition,
( spl0_13
<=> ! [X1] : ~ ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f431,plain,
( ! [X1] : ~ ssItem(X1)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f430]) ).
fof(f433,definition,
( spl0_14
<=> ! [X0] :
( ~ ssList(X0)
| duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f434,plain,
( ! [X0] :
( duplicatefreeP(X0)
| ~ ssList(X0) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f433]) ).
fof(f435,plain,
( spl0_13
| spl0_14 ),
inference(avatar_split_clause,[],[f284,f433,f430]) ).
fof(f438,plain,
spl0_7,
inference(avatar_split_clause,[],[f8,f402]) ).
fof(f486,plain,
sk3 = app(sk3,nil),
inference(resolution,[],[f73,f202]) ).
fof(f519,plain,
sk3 = app(nil,sk3),
inference(resolution,[],[f74,f202]) ).
fof(f523,plain,
sk9 = app(nil,sk9),
inference(resolution,[],[f74,f210]) ).
fof(f552,plain,
( ! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1) )
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f289,f431]) ).
fof(f559,plain,
( ! [X0,X1] :
( nil != cons(X0,X1)
| ~ ssList(X1) )
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f299,f431]) ).
fof(f565,plain,
( ! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssList(X2) )
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f367,f431]) ).
fof(f573,plain,
( ! [X0,X1] :
( ~ ssList(X1)
| tl(cons(X0,X1)) = X1 )
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f297,f431]) ).
fof(f575,plain,
( ! [X0,X1] : skaf82(X1) = tl(cons(X0,skaf82(X1)))
| ~ spl0_13 ),
inference(resolution,[],[f573,f13]) ).
fof(f609,plain,
( ! [X0] : sk9 = tl(cons(X0,sk9))
| ~ spl0_13 ),
inference(resolution,[],[f573,f210]) ).
fof(f719,definition,
( spl0_15
<=> nil = sk9 ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f721,plain,
( nil = sk9
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f719]) ).
fof(f723,definition,
( spl0_16
<=> sk9 = cons(hd(sk9),tl(sk9)) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f725,plain,
( sk9 = cons(hd(sk9),tl(sk9))
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f723]) ).
fof(f762,definition,
( spl0_22
<=> sk3 = cons(hd(sk3),tl(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f764,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f762]) ).
fof(f808,plain,
! [X0] :
( ~ ssList(X0)
| nil = tl(X0)
| tl(X0) = cons(skaf83(tl(X0)),skaf82(tl(X0)))
| nil = X0 ),
inference(resolution,[],[f112,f75]) ).
fof(f836,definition,
( spl0_25
<=> nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f838,plain,
( nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f836]) ).
fof(f840,definition,
( spl0_26
<=> ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f842,plain,
( ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| spl0_26 ),
inference(avatar_component_clause,[],[f840]) ).
fof(f869,plain,
! [X0,X1] :
( frontsegP(app(X0,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(forward_subsumption_resolution,[],[f236,f85]) ).
fof(f870,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,app(X0,X1))
| ~ ssList(app(X0,X1))
| ~ ssList(X0)
| app(X0,X1) = X0 ),
inference(resolution,[],[f869,f139]) ).
fof(f886,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,app(X0,X1))
| ~ ssList(app(X0,X1))
| app(X0,X1) = X0 ),
inference(duplicate_literal_removal,[],[f870]) ).
fof(f888,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X0,app(X0,X1))
| app(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f886,f85]) ).
fof(f910,plain,
( ! [X0,X1] :
( ~ ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) )
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f315,f431]) ).
fof(f912,plain,
( ! [X0,X1] : cons(X0,skaf82(X1)) = app(cons(X0,nil),skaf82(X1))
| ~ spl0_13 ),
inference(resolution,[],[f910,f13]) ).
fof(f946,plain,
( ! [X0] : cons(X0,sk9) = app(cons(X0,nil),sk9)
| ~ spl0_13 ),
inference(resolution,[],[f910,f210]) ).
fof(f947,plain,
( ! [X0] : cons(X0,nil) = app(cons(X0,nil),nil)
| ~ spl0_13
| ~ spl0_15 ),
inference(forward_demodulation,[],[f946,f721]) ).
fof(f976,definition,
( spl0_31
<=> ssList(cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f977,plain,
( ssList(cons(sk6,nil))
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f976]) ).
fof(f978,plain,
( ~ ssList(cons(sk6,nil))
| spl0_31 ),
inference(avatar_component_clause,[],[f976]) ).
fof(f995,plain,
( ~ ssList(nil)
| ssItem(sk6)
| spl0_31 ),
inference(resolution,[],[f289,f978]) ).
fof(f1000,plain,
( ssItem(sk6)
| ~ spl0_7
| spl0_31 ),
inference(forward_subsumption_resolution,[],[f995,f403]) ).
fof(f1001,plain,
( $false
| ~ spl0_7
| spl0_31 ),
inference(forward_subsumption_resolution,[],[f1000,f362]) ).
fof(f1002,plain,
( ~ spl0_7
| spl0_31 ),
inference(avatar_contradiction_clause,[],[f1001]) ).
fof(f1050,definition,
( spl0_33
<=> nil = cons(sk6,nil) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f1051,plain,
( nil != cons(sk6,nil)
| spl0_33 ),
inference(avatar_component_clause,[],[f1050]) ).
fof(f1052,plain,
( nil = cons(sk6,nil)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f1050]) ).
fof(f1120,plain,
( memberP(nil,sk6)
| ssItem(sk6)
| ~ ssList(nil)
| ~ spl0_33 ),
inference(superposition,[],[f367,f1052]) ).
fof(f1128,plain,
( ssItem(sk6)
| ~ ssList(nil)
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f1120,f283]) ).
fof(f1134,plain,
( ~ ssList(nil)
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f1128,f362]) ).
fof(f1136,plain,
( $false
| ~ spl0_7
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f1134,f403]) ).
fof(f1137,plain,
( ~ spl0_7
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f1136]) ).
fof(f1775,plain,
! [X0] :
( sk3 != app(X0,sk9)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssList(sk9)
| ~ ssList(X0)
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0 ),
inference(superposition,[],[f163,f224]) ).
fof(f1783,plain,
! [X0] :
( sk3 != app(X0,sk3)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(nil)
| nil = X0 ),
inference(superposition,[],[f163,f519]) ).
fof(f1787,plain,
! [X0] :
( sk9 != app(X0,sk9)
| ~ ssList(X0)
| ~ ssList(sk9)
| ~ ssList(nil)
| nil = X0 ),
inference(superposition,[],[f163,f523]) ).
fof(f1790,plain,
! [X0] :
( sk3 != app(X0,sk9)
| ~ ssList(X0)
| ~ ssList(sk9)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0 ),
inference(superposition,[],[f163,f224]) ).
fof(f1806,plain,
! [X0] :
( sk3 != app(X0,sk9)
| ~ ssList(X0)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0 ),
inference(forward_subsumption_resolution,[],[f1790,f210]) ).
fof(f1809,plain,
! [X0] :
( sk9 != app(X0,sk9)
| ~ ssList(X0)
| ~ ssList(nil)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f1787,f210]) ).
fof(f1813,plain,
! [X0] :
( sk3 != app(X0,sk3)
| ~ ssList(X0)
| ~ ssList(nil)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f1783,f202]) ).
fof(f1819,plain,
! [X0] :
( sk3 != app(X0,sk9)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssList(X0)
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0 ),
inference(forward_subsumption_resolution,[],[f1775,f210]) ).
fof(f1835,plain,
( ! [X0] :
( sk9 != app(X0,sk9)
| ~ ssList(X0)
| nil = X0 )
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f1809,f403]) ).
fof(f1839,plain,
( ! [X0] :
( sk3 != app(X0,sk3)
| ~ ssList(X0)
| nil = X0 )
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f1813,f403]) ).
fof(f2049,plain,
! [X0] :
( ~ ssList(app(sk3,X0))
| ~ ssList(nil)
| ~ ssList(sk3)
| ~ ssList(X0)
| segmentP(app(sk3,X0),sk3) ),
inference(superposition,[],[f239,f519]) ).
fof(f2056,plain,
! [X0] :
( ~ ssList(app(sk3,X0))
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssList(sk9)
| ~ ssList(X0)
| segmentP(app(sk3,X0),sk9) ),
inference(superposition,[],[f239,f224]) ).
fof(f2063,plain,
( ~ ssList(sk3)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| ~ ssList(sk9)
| segmentP(sk3,cons(sk6,nil)) ),
inference(superposition,[],[f239,f224]) ).
fof(f2069,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| ~ ssList(sk9)
| segmentP(sk3,cons(sk6,nil)) ),
inference(forward_subsumption_resolution,[],[f2063,f202]) ).
fof(f2070,plain,
! [X0] :
( ~ ssList(app(sk3,X0))
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssList(X0)
| segmentP(app(sk3,X0),sk9) ),
inference(forward_subsumption_resolution,[],[f2056,f210]) ).
fof(f2075,plain,
( ! [X0] :
( ~ ssList(app(sk3,X0))
| ~ ssList(sk3)
| ~ ssList(X0)
| segmentP(app(sk3,X0),sk3) )
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f2049,f403]) ).
fof(f2078,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(sk9)
| segmentP(sk3,cons(sk6,nil))
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f2069,f977]) ).
fof(f2084,plain,
( ! [X0] :
( segmentP(app(sk3,X0),sk3)
| ~ ssList(X0)
| ~ ssList(app(sk3,X0)) )
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f2075,f202]) ).
fof(f2086,definition,
( spl0_36
<=> segmentP(nil,cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f2088,plain,
( segmentP(nil,cons(sk6,nil))
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f2086]) ).
fof(f2090,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| segmentP(sk3,cons(sk6,nil))
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f2078,f210]) ).
fof(f2159,definition,
( spl0_38
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f2160,plain,
( ssList(cons(sk5,nil))
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f2159]) ).
fof(f2161,plain,
( ~ ssList(cons(sk5,nil))
| spl0_38 ),
inference(avatar_component_clause,[],[f2159]) ).
fof(f2208,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,[],[f354,f434]) ).
fof(f2226,plain,
( ~ ssList(nil)
| ssItem(sk5)
| spl0_38 ),
inference(resolution,[],[f2161,f289]) ).
fof(f2227,plain,
( ssItem(sk5)
| ~ spl0_7
| spl0_38 ),
inference(forward_subsumption_resolution,[],[f2226,f403]) ).
fof(f2228,plain,
( $false
| ~ spl0_7
| spl0_38 ),
inference(forward_subsumption_resolution,[],[f2227,f361]) ).
fof(f2229,plain,
( ~ spl0_7
| spl0_38 ),
inference(avatar_contradiction_clause,[],[f2228]) ).
fof(f2231,definition,
( spl0_50
<=> sk9 = cons(skaf83(sk9),skaf82(sk9)) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f2233,plain,
( sk9 = cons(skaf83(sk9),skaf82(sk9))
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f2231]) ).
fof(f2683,definition,
( spl0_92
<=> ssList(tl(sk9)) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f2684,plain,
( ssList(tl(sk9))
| ~ spl0_92 ),
inference(avatar_component_clause,[],[f2683]) ).
fof(f2685,plain,
( ~ ssList(tl(sk9))
| spl0_92 ),
inference(avatar_component_clause,[],[f2683]) ).
fof(f6100,plain,
( segmentP(nil,cons(sk6,nil))
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_1
| ~ spl0_31 ),
inference(forward_demodulation,[],[f2090,f374]) ).
fof(f6153,definition,
( spl0_164
<=> ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f6154,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_164 ),
inference(avatar_component_clause,[],[f6153]) ).
fof(f6155,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| spl0_164 ),
inference(avatar_component_clause,[],[f6153]) ).
fof(f6412,definition,
( spl0_200
<=> ssList(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_200])],[avatar_definition]) ).
fof(f6414,plain,
( ssList(sk3)
| ~ spl0_200 ),
inference(avatar_component_clause,[],[f6412]) ).
fof(f6451,plain,
( ~ spl0_164
| spl0_36
| ~ spl0_1
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f6100,f976,f372,f2086,f6153]) ).
fof(f6493,plain,
spl0_200,
inference(avatar_split_clause,[],[f202,f6412]) ).
fof(f7149,definition,
( spl0_275
<=> ssList(sk9) ),
introduced(definition,[new_symbols(definition,[spl0_275])],[avatar_definition]) ).
fof(f7151,plain,
( ssList(sk9)
| ~ spl0_275 ),
inference(avatar_component_clause,[],[f7149]) ).
fof(f7661,plain,
spl0_275,
inference(avatar_split_clause,[],[f210,f7149]) ).
fof(f7933,plain,
( ! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X2)
| memberP(app(X2,X0),X1) )
| ~ spl0_13 ),
inference(backward_subsumption_resolution,[],[f330,f431]) ).
fof(f8053,plain,
( ~ segmentP(cons(sk6,nil),nil)
| ~ ssList(nil)
| ~ ssList(cons(sk6,nil))
| nil = cons(sk6,nil)
| ~ spl0_36 ),
inference(resolution,[],[f2088,f135]) ).
fof(f8054,plain,
( ~ ssList(nil)
| ~ ssList(cons(sk6,nil))
| nil = cons(sk6,nil)
| ~ spl0_36 ),
inference(forward_subsumption_resolution,[],[f8053,f56]) ).
fof(f8059,plain,
( ~ ssList(cons(sk6,nil))
| nil = cons(sk6,nil)
| ~ spl0_7
| ~ spl0_36 ),
inference(forward_subsumption_resolution,[],[f8054,f403]) ).
fof(f8065,plain,
( nil = cons(sk6,nil)
| ~ spl0_7
| ~ spl0_31
| ~ spl0_36 ),
inference(forward_subsumption_resolution,[],[f8059,f977]) ).
fof(f8066,plain,
( $false
| ~ spl0_7
| ~ spl0_31
| spl0_33
| ~ spl0_36 ),
inference(forward_subsumption_resolution,[],[f8065,f1051]) ).
fof(f8067,plain,
( ~ spl0_7
| ~ spl0_31
| spl0_33
| ~ spl0_36 ),
inference(avatar_contradiction_clause,[],[f8066]) ).
fof(f8320,plain,
( ! [X2,X0,X1] :
( ~ ssList(cons(X0,X1))
| ~ ssList(X2)
| memberP(app(X2,cons(X0,X1)),X0)
| ~ ssList(X1) )
| ~ spl0_13 ),
inference(resolution,[],[f7933,f565]) ).
fof(f8321,plain,
( ! [X2,X0,X1] :
( memberP(app(X2,cons(X0,X1)),X0)
| ~ ssList(X2)
| ~ ssList(X1) )
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f8320,f552]) ).
fof(f8855,plain,
( ! [X0,X1] :
( ~ ssList(app(cons(X0,nil),X1))
| ~ ssList(cons(X0,nil))
| ~ ssList(nil)
| ~ ssList(X1)
| segmentP(app(cons(X0,nil),X1),nil) )
| ~ spl0_13
| ~ spl0_15 ),
inference(superposition,[],[f239,f947]) ).
fof(f8862,plain,
( ! [X0,X1] :
( ~ ssList(cons(X0,nil))
| ~ ssList(nil)
| ~ ssList(X1)
| segmentP(app(cons(X0,nil),X1),nil) )
| ~ spl0_13
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f8855,f85]) ).
fof(f8870,plain,
( ! [X0,X1] :
( ~ ssList(nil)
| ~ ssList(X1)
| segmentP(app(cons(X0,nil),X1),nil) )
| ~ spl0_13
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f8862,f552]) ).
fof(f8875,plain,
( ! [X0,X1] :
( segmentP(app(cons(X0,nil),X1),nil)
| ~ ssList(X1) )
| ~ spl0_7
| ~ spl0_13
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f8870,f403]) ).
fof(f13623,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssList(nil)
| ssItem(sk10)
| ssItem(X0)
| memberP(nil,X0)
| sk10 = X0 )
| ~ spl0_3 ),
inference(superposition,[],[f343,f383]) ).
fof(f13625,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk3
| ssItem(sk10)
| ssItem(X0)
| ~ ssList(nil)
| ~ ssList(X1)
| sk10 = X0 )
| ~ spl0_3 ),
inference(superposition,[],[f348,f383]) ).
fof(f13644,plain,
( ! [X0] :
( frontsegP(cons(sk10,X0),sk3)
| ~ ssList(nil)
| ~ ssList(X0)
| ssItem(sk10)
| ~ frontsegP(X0,nil) )
| ~ spl0_3 ),
inference(superposition,[],[f365,f383]) ).
fof(f13646,plain,
( memberP(sk3,sk10)
| ssItem(sk10)
| ~ ssList(nil)
| ~ spl0_3 ),
inference(superposition,[],[f367,f383]) ).
fof(f13651,plain,
( memberP(sk3,sk10)
| ~ ssList(nil)
| ~ spl0_3
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f13646,f394]) ).
fof(f13653,plain,
( ! [X0] :
( frontsegP(cons(sk10,X0),sk3)
| ~ ssList(X0)
| ssItem(sk10)
| ~ frontsegP(X0,nil) )
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f13644,f403]) ).
fof(f13671,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk3
| ssItem(X0)
| ~ ssList(nil)
| ~ ssList(X1)
| sk10 = X0 )
| ~ spl0_3
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f13625,f394]) ).
fof(f13673,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssList(nil)
| ssItem(sk10)
| ssItem(X0)
| sk10 = X0 )
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f13623,f283]) ).
fof(f13685,plain,
( memberP(sk3,sk10)
| ~ spl0_3
| spl0_5
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f13651,f403]) ).
fof(f13687,plain,
( ! [X0] :
( frontsegP(cons(sk10,X0),sk3)
| ~ ssList(X0)
| ~ frontsegP(X0,nil) )
| ~ spl0_3
| spl0_5
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f13653,f394]) ).
fof(f13705,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk3
| ssItem(X0)
| ~ ssList(X1)
| sk10 = X0 )
| ~ spl0_3
| spl0_5
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f13671,f403]) ).
fof(f13707,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ssItem(sk10)
| ssItem(X0)
| sk10 = X0 )
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f13673,f403]) ).
fof(f13714,plain,
( ! [X0] :
( frontsegP(cons(sk10,X0),sk3)
| ~ ssList(X0) )
| ~ spl0_3
| spl0_5
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f13687,f60]) ).
fof(f13715,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ssItem(X0)
| sk10 = X0 )
| ~ spl0_3
| spl0_5
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f13707,f394]) ).
fof(f13772,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| nil = sk3
| ~ spl0_200 ),
inference(resolution,[],[f6414,f107]) ).
fof(f13817,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| spl0_1
| ~ spl0_200 ),
inference(forward_subsumption_resolution,[],[f13772,f373]) ).
fof(f13822,plain,
( spl0_22
| spl0_1
| ~ spl0_200 ),
inference(avatar_split_clause,[],[f13817,f6412,f372,f762]) ).
fof(f13828,plain,
( ssItem(sk10)
| ~ ssList(sk3)
| sk3 = app(skaf42(sk3,sk10),cons(sk10,skaf43(sk10,sk3)))
| ~ spl0_3
| spl0_5
| ~ spl0_7 ),
inference(resolution,[],[f13685,f347]) ).
fof(f13833,plain,
( ~ ssList(sk3)
| sk3 = app(skaf42(sk3,sk10),cons(sk10,skaf43(sk10,sk3)))
| ~ spl0_3
| spl0_5
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f13828,f394]) ).
fof(f13836,plain,
( sk3 = app(skaf42(sk3,sk10),cons(sk10,skaf43(sk10,sk3)))
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_200 ),
inference(forward_subsumption_resolution,[],[f13833,f6414]) ).
fof(f13850,definition,
( spl0_423
<=> sk3 = cons(sk6,nil) ),
introduced(definition,[new_symbols(definition,[spl0_423])],[avatar_definition]) ).
fof(f13851,plain,
( sk3 != cons(sk6,nil)
| spl0_423 ),
inference(avatar_component_clause,[],[f13850]) ).
fof(f13852,plain,
( sk3 = cons(sk6,nil)
| ~ spl0_423 ),
inference(avatar_component_clause,[],[f13850]) ).
fof(f14156,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,cons(hd(sk3),X1)),sk3))
| ~ ssList(X1)
| ~ ssList(X0)
| ssItem(hd(sk3))
| ~ ssList(tl(sk3)) )
| ~ spl0_14
| ~ spl0_22 ),
inference(superposition,[],[f2208,f764]) ).
fof(f14158,definition,
( spl0_460
<=> ssList(tl(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_460])],[avatar_definition]) ).
fof(f14160,plain,
( ~ ssList(tl(sk3))
| spl0_460 ),
inference(avatar_component_clause,[],[f14158]) ).
fof(f14162,definition,
( spl0_461
<=> ssItem(hd(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_461])],[avatar_definition]) ).
fof(f14164,plain,
( ssItem(hd(sk3))
| ~ spl0_461 ),
inference(avatar_component_clause,[],[f14162]) ).
fof(f14166,definition,
( spl0_462
<=> ! [X0,X1] :
( ~ ssList(app(app(X0,cons(hd(sk3),X1)),sk3))
| ~ ssList(X0)
| ~ ssList(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_462])],[avatar_definition]) ).
fof(f14167,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,cons(hd(sk3),X1)),sk3))
| ~ ssList(X0)
| ~ ssList(X1) )
| ~ spl0_462 ),
inference(avatar_component_clause,[],[f14166]) ).
fof(f14168,plain,
( ~ spl0_460
| spl0_461
| spl0_462
| ~ spl0_14
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f14156,f762,f433,f14166,f14162,f14158]) ).
fof(f15612,definition,
( spl0_582
<=> sk10 = hd(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_582])],[avatar_definition]) ).
fof(f15614,plain,
( sk10 = hd(sk3)
| ~ spl0_582 ),
inference(avatar_component_clause,[],[f15612]) ).
fof(f15860,plain,
( sk3 != sk3
| ssItem(hd(sk3))
| ~ ssList(tl(sk3))
| sk10 = hd(sk3)
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_22 ),
inference(superposition,[],[f13705,f764]) ).
fof(f15865,plain,
( ssItem(hd(sk3))
| ~ ssList(tl(sk3))
| sk10 = hd(sk3)
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_22 ),
inference(trivial_inequality_removal,[],[f15860]) ).
fof(f15869,plain,
( spl0_582
| ~ spl0_460
| spl0_461
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f15865,f762,f402,f392,f381,f14162,f14158,f15612]) ).
fof(f15910,plain,
( ~ ssList(sk3)
| nil = sk3
| spl0_460 ),
inference(resolution,[],[f14160,f75]) ).
fof(f15911,plain,
( nil = sk3
| ~ spl0_200
| spl0_460 ),
inference(forward_subsumption_resolution,[],[f15910,f6414]) ).
fof(f15912,plain,
( $false
| spl0_1
| ~ spl0_200
| spl0_460 ),
inference(forward_subsumption_resolution,[],[f15911,f373]) ).
fof(f15913,plain,
( spl0_1
| ~ spl0_200
| spl0_460 ),
inference(avatar_contradiction_clause,[],[f15912]) ).
fof(f16058,plain,
( ~ ssList(sk3)
| nil = sk3
| ~ spl0_461 ),
inference(resolution,[],[f14164,f285]) ).
fof(f16059,plain,
( nil = sk3
| ~ spl0_200
| ~ spl0_461 ),
inference(forward_subsumption_resolution,[],[f16058,f6414]) ).
fof(f16060,plain,
( $false
| spl0_1
| ~ spl0_200
| ~ spl0_461 ),
inference(forward_subsumption_resolution,[],[f16059,f373]) ).
fof(f16061,plain,
( spl0_1
| ~ spl0_200
| ~ spl0_461 ),
inference(avatar_contradiction_clause,[],[f16060]) ).
fof(f16508,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| sk10 = X0 )
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_13 ),
inference(backward_subsumption_resolution,[],[f13715,f431]) ).
fof(f19160,definition,
( spl0_656
<=> sk6 = sk10 ),
introduced(definition,[new_symbols(definition,[spl0_656])],[avatar_definition]) ).
fof(f19161,plain,
( sk6 != sk10
| spl0_656 ),
inference(avatar_component_clause,[],[f19160]) ).
fof(f19162,plain,
( sk6 = sk10
| ~ spl0_656 ),
inference(avatar_component_clause,[],[f19160]) ).
fof(f20146,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,cons(sk10,X1)),sk3))
| ~ ssList(X0)
| ~ ssList(X1) )
| ~ spl0_462
| ~ spl0_582 ),
inference(forward_demodulation,[],[f14167,f15614]) ).
fof(f21526,definition,
( spl0_681
<=> sk10 = hd(sk9) ),
introduced(definition,[new_symbols(definition,[spl0_681])],[avatar_definition]) ).
fof(f21527,plain,
( sk10 != hd(sk9)
| spl0_681 ),
inference(avatar_component_clause,[],[f21526]) ).
fof(f21528,plain,
( sk10 = hd(sk9)
| ~ spl0_681 ),
inference(avatar_component_clause,[],[f21526]) ).
fof(f21545,definition,
( spl0_685
<=> sk3 = sk9 ),
introduced(definition,[new_symbols(definition,[spl0_685])],[avatar_definition]) ).
fof(f21547,plain,
( sk3 != sk9
| spl0_685 ),
inference(avatar_component_clause,[],[f21545]) ).
fof(f21824,plain,
( sk9 = cons(hd(sk9),tl(sk9))
| nil = sk9
| ~ spl0_275 ),
inference(resolution,[],[f7151,f107]) ).
fof(f21899,plain,
( ~ ssList(sk9)
| nil = sk9
| spl0_92 ),
inference(resolution,[],[f2685,f75]) ).
fof(f21900,plain,
( nil = sk9
| spl0_92
| ~ spl0_275 ),
inference(forward_subsumption_resolution,[],[f21899,f7151]) ).
fof(f22385,plain,
( spl0_15
| spl0_16
| ~ spl0_275 ),
inference(avatar_split_clause,[],[f21824,f7149,f723,f719]) ).
fof(f25108,definition,
( spl0_798
<=> frontsegP(nil,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_798])],[avatar_definition]) ).
fof(f25110,plain,
( ~ frontsegP(nil,sk3)
| spl0_798 ),
inference(avatar_component_clause,[],[f25108]) ).
fof(f25940,definition,
( spl0_802
<=> ssList(app(sk3,sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_802])],[avatar_definition]) ).
fof(f25941,plain,
( ssList(app(sk3,sk3))
| ~ spl0_802 ),
inference(avatar_component_clause,[],[f25940]) ).
fof(f25942,plain,
( ~ ssList(app(sk3,sk3))
| spl0_802 ),
inference(avatar_component_clause,[],[f25940]) ).
fof(f31037,plain,
( ~ ssList(sk3)
| ~ ssList(sk3)
| spl0_802 ),
inference(resolution,[],[f25942,f85]) ).
fof(f31038,plain,
( ~ ssList(sk3)
| spl0_802 ),
inference(duplicate_literal_removal,[],[f31037]) ).
fof(f31039,plain,
( $false
| ~ spl0_200
| spl0_802 ),
inference(forward_subsumption_resolution,[],[f31038,f6414]) ).
fof(f31040,plain,
( ~ spl0_200
| spl0_802 ),
inference(avatar_contradiction_clause,[],[f31039]) ).
fof(f32017,plain,
( ! [X0] : cons(sk10,skaf82(X0)) = app(sk3,skaf82(X0))
| ~ spl0_3
| ~ spl0_13 ),
inference(superposition,[],[f912,f383]) ).
fof(f38903,plain,
( ! [X0] :
( ~ frontsegP(X0,app(X0,sk3))
| ~ ssList(X0)
| app(X0,sk3) = X0 )
| ~ spl0_200 ),
inference(resolution,[],[f888,f6414]) ).
fof(f65312,plain,
( ! [X0] :
( segmentP(cons(X0,nil),nil)
| ~ ssList(nil) )
| ~ spl0_7
| ~ spl0_13
| ~ spl0_15 ),
inference(superposition,[],[f8875,f947]) ).
fof(f65373,plain,
( ! [X0] : segmentP(cons(X0,nil),nil)
| ~ spl0_7
| ~ spl0_13
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f65312,f403]) ).
fof(f65397,plain,
( ! [X0] :
( ~ segmentP(nil,cons(X0,nil))
| ~ ssList(cons(X0,nil))
| ~ ssList(nil)
| nil = cons(X0,nil) )
| ~ spl0_7
| ~ spl0_13
| ~ spl0_15 ),
inference(resolution,[],[f65373,f135]) ).
fof(f65401,plain,
( ! [X0] :
( ~ segmentP(nil,cons(X0,nil))
| ~ ssList(nil)
| nil = cons(X0,nil) )
| ~ spl0_7
| ~ spl0_13
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f65397,f552]) ).
fof(f65403,plain,
( ! [X0] :
( ~ segmentP(nil,cons(X0,nil))
| ~ ssList(nil) )
| ~ spl0_7
| ~ spl0_13
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f65401,f559]) ).
fof(f65405,plain,
( ! [X0] : ~ segmentP(nil,cons(X0,nil))
| ~ spl0_7
| ~ spl0_13
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f65403,f403]) ).
fof(f78583,plain,
( ! [X0] :
( segmentP(cons(sk10,skaf82(X0)),sk3)
| ~ ssList(skaf82(X0))
| ~ ssList(cons(sk10,skaf82(X0))) )
| ~ spl0_3
| ~ spl0_7
| ~ spl0_13 ),
inference(superposition,[],[f2084,f32017]) ).
fof(f78641,plain,
( ! [X0] :
( segmentP(cons(sk10,skaf82(X0)),sk3)
| ~ ssList(skaf82(X0)) )
| ~ spl0_3
| ~ spl0_7
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f78583,f552]) ).
fof(f78672,plain,
( ! [X0] : segmentP(cons(sk10,skaf82(X0)),sk3)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f78641,f13]) ).
fof(f101427,definition,
( spl0_2504
<=> ssList(app(app(app(sk7,cons(sk5,nil)),sk8),sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_2504])],[avatar_definition]) ).
fof(f101428,plain,
( ssList(app(app(app(sk7,cons(sk5,nil)),sk8),sk3))
| ~ spl0_2504 ),
inference(avatar_component_clause,[],[f101427]) ).
fof(f101429,plain,
( ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),sk3))
| spl0_2504 ),
inference(avatar_component_clause,[],[f101427]) ).
fof(f103257,definition,
( spl0_2573
<=> nil = app(app(sk7,cons(sk5,nil)),sk8) ),
introduced(definition,[new_symbols(definition,[spl0_2573])],[avatar_definition]) ).
fof(f103259,plain,
( nil = app(app(sk7,cons(sk5,nil)),sk8)
| ~ spl0_2573 ),
inference(avatar_component_clause,[],[f103257]) ).
fof(f103943,definition,
( spl0_2628
<=> sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),sk3) ),
introduced(definition,[new_symbols(definition,[spl0_2628])],[avatar_definition]) ).
fof(f103945,plain,
( sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),sk3)
| ~ spl0_2628 ),
inference(avatar_component_clause,[],[f103943]) ).
fof(f104695,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(sk8)
| spl0_164 ),
inference(resolution,[],[f6155,f85]) ).
fof(f104696,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| spl0_164 ),
inference(forward_subsumption_resolution,[],[f104695,f209]) ).
fof(f108862,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| spl0_164 ),
inference(resolution,[],[f104696,f85]) ).
fof(f108863,plain,
( ~ ssList(cons(sk5,nil))
| spl0_164 ),
inference(forward_subsumption_resolution,[],[f108862,f208]) ).
fof(f108864,plain,
( $false
| ~ spl0_38
| spl0_164 ),
inference(forward_subsumption_resolution,[],[f108863,f2160]) ).
fof(f108865,plain,
( ~ spl0_38
| spl0_164 ),
inference(avatar_contradiction_clause,[],[f108864]) ).
fof(f114206,plain,
( ~ ssList(nil)
| ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk8)
| segmentP(nil,cons(sk5,nil))
| ~ spl0_2573 ),
inference(superposition,[],[f239,f103259]) ).
fof(f114253,plain,
( ~ ssList(nil)
| ~ ssList(sk7)
| ~ ssList(sk8)
| segmentP(nil,cons(sk5,nil))
| ~ spl0_13
| ~ spl0_2573 ),
inference(forward_subsumption_resolution,[],[f114206,f552]) ).
fof(f114291,plain,
( ~ ssList(sk7)
| ~ ssList(sk8)
| segmentP(nil,cons(sk5,nil))
| ~ spl0_7
| ~ spl0_13
| ~ spl0_2573 ),
inference(forward_subsumption_resolution,[],[f114253,f403]) ).
fof(f114295,plain,
( ~ ssList(sk8)
| segmentP(nil,cons(sk5,nil))
| ~ spl0_7
| ~ spl0_13
| ~ spl0_2573 ),
inference(forward_subsumption_resolution,[],[f114291,f208]) ).
fof(f114297,plain,
( segmentP(nil,cons(sk5,nil))
| ~ spl0_7
| ~ spl0_13
| ~ spl0_2573 ),
inference(forward_subsumption_resolution,[],[f114295,f209]) ).
fof(f114298,plain,
( $false
| ~ spl0_7
| ~ spl0_13
| ~ spl0_15
| ~ spl0_2573 ),
inference(forward_subsumption_resolution,[],[f114297,f65405]) ).
fof(f114299,plain,
( ~ spl0_7
| ~ spl0_13
| ~ spl0_15
| ~ spl0_2573 ),
inference(avatar_contradiction_clause,[],[f114298]) ).
fof(f119276,plain,
( sk3 != sk3
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = app(app(sk7,cons(sk5,nil)),sk8)
| ~ spl0_7
| ~ spl0_2628 ),
inference(superposition,[],[f1839,f103945]) ).
fof(f119298,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = app(app(sk7,cons(sk5,nil)),sk8)
| ~ spl0_7
| ~ spl0_2628 ),
inference(trivial_inequality_removal,[],[f119276]) ).
fof(f119312,plain,
( nil = app(app(sk7,cons(sk5,nil)),sk8)
| ~ spl0_7
| ~ spl0_164
| ~ spl0_2628 ),
inference(forward_subsumption_resolution,[],[f119298,f6154]) ).
fof(f119498,plain,
( spl0_2573
| ~ spl0_7
| ~ spl0_164
| ~ spl0_2628 ),
inference(avatar_split_clause,[],[f119312,f103943,f6153,f402,f103257]) ).
fof(f119648,plain,
( ! [X0] :
( ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),sk3))
| sk3 != app(X0,sk9)
| ~ ssList(X0)
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0 )
| ~ spl0_423 ),
inference(forward_demodulation,[],[f1806,f13852]) ).
fof(f119865,plain,
( ! [X0] :
( sk3 != app(X0,sk9)
| ~ ssList(X0)
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0 )
| ~ spl0_423
| ~ spl0_2504 ),
inference(forward_subsumption_resolution,[],[f119648,f101428]) ).
fof(f119963,plain,
( ! [X0] :
( sk3 != app(X0,sk9)
| app(app(app(sk7,cons(sk5,nil)),sk8),sk3) = X0
| ~ ssList(X0) )
| ~ spl0_423
| ~ spl0_2504 ),
inference(forward_demodulation,[],[f119865,f13852]) ).
fof(f120491,plain,
( ! [X0] :
( memberP(app(X0,sk9),hd(sk9))
| ~ ssList(X0)
| ~ ssList(tl(sk9)) )
| ~ spl0_13
| ~ spl0_16 ),
inference(superposition,[],[f8321,f725]) ).
fof(f120567,plain,
( ! [X0] :
( memberP(app(X0,sk9),hd(sk9))
| ~ ssList(X0) )
| ~ spl0_13
| ~ spl0_16
| ~ spl0_92 ),
inference(forward_subsumption_resolution,[],[f120491,f2684]) ).
fof(f120742,plain,
( tl(sk9) = skaf82(sk9)
| ~ spl0_13
| ~ spl0_50 ),
inference(superposition,[],[f575,f2233]) ).
fof(f121003,plain,
( app(sk3,sk9) = cons(sk10,sk9)
| ~ spl0_3
| ~ spl0_13 ),
inference(superposition,[],[f946,f383]) ).
fof(f123280,plain,
( sk9 = cons(sk10,tl(sk9))
| ~ spl0_16
| ~ spl0_681 ),
inference(superposition,[],[f725,f21528]) ).
fof(f123484,plain,
( segmentP(cons(sk10,tl(sk9)),sk3)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_13
| ~ spl0_50 ),
inference(superposition,[],[f78672,f120742]) ).
fof(f123852,plain,
( sk3 != cons(sk10,sk9)
| sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),sk3)
| ~ ssList(sk3)
| ~ spl0_3
| ~ spl0_13
| ~ spl0_423
| ~ spl0_2504 ),
inference(superposition,[],[f119963,f121003]) ).
fof(f123871,plain,
( sk3 != cons(sk10,sk9)
| sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),sk3)
| ~ spl0_3
| ~ spl0_13
| ~ spl0_200
| ~ spl0_423
| ~ spl0_2504 ),
inference(forward_subsumption_resolution,[],[f123852,f6414]) ).
fof(f123886,definition,
( spl0_3732
<=> sk3 = cons(sk10,sk9) ),
introduced(definition,[new_symbols(definition,[spl0_3732])],[avatar_definition]) ).
fof(f123888,plain,
( sk3 != cons(sk10,sk9)
| spl0_3732 ),
inference(avatar_component_clause,[],[f123886]) ).
fof(f123889,plain,
( spl0_2628
| ~ spl0_3732
| ~ spl0_3
| ~ spl0_13
| ~ spl0_200
| ~ spl0_423
| ~ spl0_2504 ),
inference(avatar_split_clause,[],[f123871,f101427,f13850,f6412,f430,f381,f123886,f103943]) ).
fof(f124288,plain,
( memberP(sk3,hd(sk9))
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ spl0_13
| ~ spl0_16
| ~ spl0_92 ),
inference(superposition,[],[f120567,f224]) ).
fof(f127264,definition,
( spl0_3933
<=> segmentP(sk9,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_3933])],[avatar_definition]) ).
fof(f128082,plain,
( sk3 != sk9
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ spl0_7 ),
inference(superposition,[],[f1835,f224]) ).
fof(f130467,definition,
( spl0_4005
<=> ssList(cons(sk10,sk9)) ),
introduced(definition,[new_symbols(definition,[spl0_4005])],[avatar_definition]) ).
fof(f130468,plain,
( ssList(cons(sk10,sk9))
| ~ spl0_4005 ),
inference(avatar_component_clause,[],[f130467]) ).
fof(f130469,plain,
( ~ ssList(cons(sk10,sk9))
| spl0_4005 ),
inference(avatar_component_clause,[],[f130467]) ).
fof(f130486,plain,
( ~ ssList(sk9)
| ~ spl0_13
| spl0_4005 ),
inference(resolution,[],[f130469,f552]) ).
fof(f130487,plain,
( $false
| ~ spl0_13
| ~ spl0_275
| spl0_4005 ),
inference(forward_subsumption_resolution,[],[f130486,f7151]) ).
fof(f130488,plain,
( ~ spl0_13
| ~ spl0_275
| spl0_4005 ),
inference(avatar_contradiction_clause,[],[f130487]) ).
fof(f130515,plain,
( nil = tl(cons(sk10,sk9))
| tl(cons(sk10,sk9)) = cons(skaf83(tl(cons(sk10,sk9))),skaf82(tl(cons(sk10,sk9))))
| nil = cons(sk10,sk9)
| ~ spl0_4005 ),
inference(resolution,[],[f130468,f808]) ).
fof(f130880,plain,
( nil = sk9
| tl(cons(sk10,sk9)) = cons(skaf83(tl(cons(sk10,sk9))),skaf82(tl(cons(sk10,sk9))))
| nil = cons(sk10,sk9)
| ~ spl0_13
| ~ spl0_4005 ),
inference(forward_demodulation,[],[f130515,f609]) ).
fof(f130889,definition,
( spl0_4028
<=> nil = cons(sk10,sk9) ),
introduced(definition,[new_symbols(definition,[spl0_4028])],[avatar_definition]) ).
fof(f130890,plain,
( nil != cons(sk10,sk9)
| spl0_4028 ),
inference(avatar_component_clause,[],[f130889]) ).
fof(f130891,plain,
( nil = cons(sk10,sk9)
| ~ spl0_4028 ),
inference(avatar_component_clause,[],[f130889]) ).
fof(f131795,plain,
( ~ ssList(app(sk3,sk3))
| ~ ssList(skaf42(sk3,sk10))
| ~ ssList(skaf43(sk10,sk3))
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_200
| ~ spl0_462
| ~ spl0_582 ),
inference(superposition,[],[f20146,f13836]) ).
fof(f131796,plain,
( ~ ssList(skaf42(sk3,sk10))
| ~ ssList(skaf43(sk10,sk3))
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_200
| ~ spl0_462
| ~ spl0_582
| ~ spl0_802 ),
inference(forward_subsumption_resolution,[],[f131795,f25941]) ).
fof(f131806,plain,
( ~ ssList(skaf43(sk10,sk3))
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_200
| ~ spl0_462
| ~ spl0_582
| ~ spl0_802 ),
inference(forward_subsumption_resolution,[],[f131796,f53]) ).
fof(f131812,plain,
( $false
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_200
| ~ spl0_462
| ~ spl0_582
| ~ spl0_802 ),
inference(forward_subsumption_resolution,[],[f131806,f52]) ).
fof(f131813,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_200
| ~ spl0_462
| ~ spl0_582
| ~ spl0_802 ),
inference(avatar_contradiction_clause,[],[f131812]) ).
fof(f133653,plain,
( ~ frontsegP(nil,sk3)
| ~ ssList(nil)
| nil = sk3
| ~ spl0_200 ),
inference(superposition,[],[f38903,f519]) ).
fof(f156813,plain,
( ~ frontsegP(nil,sk3)
| nil = sk3
| ~ spl0_7
| ~ spl0_200 ),
inference(forward_subsumption_resolution,[],[f133653,f403]) ).
fof(f156822,plain,
( ~ frontsegP(nil,sk3)
| spl0_1
| ~ spl0_7
| ~ spl0_200 ),
inference(forward_subsumption_resolution,[],[f156813,f373]) ).
fof(f156824,plain,
( ~ spl0_798
| spl0_1
| ~ spl0_7
| ~ spl0_200 ),
inference(avatar_split_clause,[],[f156822,f6412,f402,f372,f25108]) ).
fof(f160343,plain,
( frontsegP(nil,sk3)
| ~ ssList(sk9)
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_4028 ),
inference(superposition,[],[f13714,f130891]) ).
fof(f160442,plain,
( ~ ssList(sk9)
| ~ spl0_3
| spl0_5
| ~ spl0_7
| spl0_798
| ~ spl0_4028 ),
inference(forward_subsumption_resolution,[],[f160343,f25110]) ).
fof(f160491,plain,
( $false
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_275
| spl0_798
| ~ spl0_4028 ),
inference(forward_subsumption_resolution,[],[f160442,f7151]) ).
fof(f160492,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_275
| spl0_798
| ~ spl0_4028 ),
inference(avatar_contradiction_clause,[],[f160491]) ).
fof(f190551,plain,
( segmentP(sk9,sk3)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_13
| ~ spl0_16
| ~ spl0_50
| ~ spl0_681 ),
inference(forward_demodulation,[],[f123484,f123280]) ).
fof(f191118,plain,
( spl0_3933
| ~ spl0_3
| ~ spl0_7
| ~ spl0_13
| ~ spl0_16
| ~ spl0_50
| ~ spl0_681 ),
inference(avatar_split_clause,[],[f190551,f21526,f2231,f723,f430,f402,f381,f127264]) ).
fof(f196544,definition,
( spl0_5022
<=> ! [X0] :
( ~ ssList(app(sk3,X0))
| segmentP(app(sk3,X0),sk9)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_5022])],[avatar_definition]) ).
fof(f196545,plain,
( ! [X0] :
( segmentP(app(sk3,X0),sk9)
| ~ ssList(app(sk3,X0))
| ~ ssList(X0) )
| ~ spl0_5022 ),
inference(avatar_component_clause,[],[f196544]) ).
fof(f196558,definition,
( spl0_5024
<=> memberP(sk3,hd(sk9)) ),
introduced(definition,[new_symbols(definition,[spl0_5024])],[avatar_definition]) ).
fof(f196560,plain,
( memberP(sk3,hd(sk9))
| ~ spl0_5024 ),
inference(avatar_component_clause,[],[f196558]) ).
fof(f196882,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(sk3)
| spl0_2504 ),
inference(resolution,[],[f101429,f85]) ).
fof(f196883,plain,
( ~ ssList(sk3)
| ~ spl0_164
| spl0_2504 ),
inference(forward_subsumption_resolution,[],[f196882,f6154]) ).
fof(f196884,plain,
( $false
| ~ spl0_164
| ~ spl0_200
| spl0_2504 ),
inference(forward_subsumption_resolution,[],[f196883,f6414]) ).
fof(f196885,plain,
( ~ spl0_164
| ~ spl0_200
| spl0_2504 ),
inference(avatar_contradiction_clause,[],[f196884]) ).
fof(f196886,plain,
( sk3 != cons(sk10,nil)
| spl0_423
| ~ spl0_656 ),
inference(forward_demodulation,[],[f13851,f19162]) ).
fof(f197621,plain,
( $false
| ~ spl0_3
| spl0_423
| ~ spl0_656 ),
inference(forward_subsumption_resolution,[],[f196886,f383]) ).
fof(f197622,plain,
( ~ spl0_3
| spl0_423
| ~ spl0_656 ),
inference(avatar_contradiction_clause,[],[f197621]) ).
fof(f199056,plain,
( ~ spl0_26
| spl0_5022 ),
inference(avatar_split_clause,[],[f2070,f196544,f840]) ).
fof(f199100,definition,
( spl0_5106
<=> ! [X0] :
( sk3 != app(X0,sk9)
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_5106])],[avatar_definition]) ).
fof(f199101,plain,
( ! [X0] :
( sk3 != app(X0,sk9)
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0
| ~ ssList(X0) )
| ~ spl0_5106 ),
inference(avatar_component_clause,[],[f199100]) ).
fof(f199103,plain,
( ~ spl0_26
| spl0_5106 ),
inference(avatar_split_clause,[],[f1819,f199100,f840]) ).
fof(f199133,plain,
( ~ spl0_26
| spl0_5024
| ~ spl0_13
| ~ spl0_16
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f124288,f2683,f723,f430,f196558,f840]) ).
fof(f199169,plain,
( spl0_25
| ~ spl0_26
| ~ spl0_685
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f128082,f402,f21545,f840,f836]) ).
fof(f199606,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| spl0_26 ),
inference(resolution,[],[f842,f85]) ).
fof(f199607,plain,
( ~ ssList(cons(sk6,nil))
| spl0_26
| ~ spl0_164 ),
inference(forward_subsumption_resolution,[],[f199606,f6154]) ).
fof(f199608,plain,
( $false
| spl0_26
| ~ spl0_31
| ~ spl0_164 ),
inference(forward_subsumption_resolution,[],[f199607,f977]) ).
fof(f199609,plain,
( spl0_26
| ~ spl0_31
| ~ spl0_164 ),
inference(avatar_contradiction_clause,[],[f199608]) ).
fof(f199646,plain,
( segmentP(sk3,sk9)
| ~ ssList(sk3)
| ~ ssList(nil)
| ~ spl0_5022 ),
inference(superposition,[],[f196545,f486]) ).
fof(f199723,plain,
( segmentP(sk3,sk9)
| ~ ssList(nil)
| ~ spl0_200
| ~ spl0_5022 ),
inference(forward_subsumption_resolution,[],[f199646,f6414]) ).
fof(f199764,plain,
( segmentP(sk3,sk9)
| ~ spl0_7
| ~ spl0_200
| ~ spl0_5022 ),
inference(forward_subsumption_resolution,[],[f199723,f403]) ).
fof(f200265,definition,
( spl0_5151
<=> sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_5151])],[avatar_definition]) ).
fof(f200267,plain,
( sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ spl0_5151 ),
inference(avatar_component_clause,[],[f200265]) ).
fof(f200895,plain,
( ~ segmentP(sk9,sk3)
| ~ ssList(sk3)
| ~ ssList(sk9)
| sk3 = sk9
| ~ spl0_7
| ~ spl0_200
| ~ spl0_5022 ),
inference(resolution,[],[f199764,f135]) ).
fof(f200896,plain,
( ~ segmentP(sk9,sk3)
| ~ ssList(sk9)
| sk3 = sk9
| ~ spl0_7
| ~ spl0_200
| ~ spl0_5022 ),
inference(forward_subsumption_resolution,[],[f200895,f6414]) ).
fof(f200900,plain,
( ~ segmentP(sk9,sk3)
| sk3 = sk9
| ~ spl0_7
| ~ spl0_200
| ~ spl0_275
| ~ spl0_5022 ),
inference(forward_subsumption_resolution,[],[f200896,f7151]) ).
fof(f200904,plain,
( ~ segmentP(sk9,sk3)
| ~ spl0_7
| ~ spl0_200
| ~ spl0_275
| spl0_685
| ~ spl0_5022 ),
inference(forward_subsumption_resolution,[],[f200900,f21547]) ).
fof(f200905,plain,
( ~ spl0_3933
| ~ spl0_7
| ~ spl0_200
| ~ spl0_275
| spl0_685
| ~ spl0_5022 ),
inference(avatar_split_clause,[],[f200904,f196544,f21545,f7149,f6412,f402,f127264]) ).
fof(f200921,plain,
( nil != nil
| ~ ssList(cons(sk6,nil))
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = cons(sk6,nil)
| ~ spl0_25 ),
inference(superposition,[],[f124,f838]) ).
fof(f200930,plain,
( ~ ssList(cons(sk6,nil))
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = cons(sk6,nil)
| ~ spl0_25 ),
inference(trivial_inequality_removal,[],[f200921]) ).
fof(f200941,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = cons(sk6,nil)
| ~ spl0_25
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f200930,f977]) ).
fof(f200961,plain,
( nil = cons(sk6,nil)
| ~ spl0_25
| ~ spl0_31
| ~ spl0_164 ),
inference(forward_subsumption_resolution,[],[f200941,f6154]) ).
fof(f200976,plain,
( $false
| ~ spl0_25
| ~ spl0_31
| spl0_33
| ~ spl0_164 ),
inference(forward_subsumption_resolution,[],[f200961,f1051]) ).
fof(f200977,plain,
( ~ spl0_25
| ~ spl0_31
| spl0_33
| ~ spl0_164 ),
inference(avatar_contradiction_clause,[],[f200976]) ).
fof(f201096,plain,
( sk3 != cons(sk10,sk9)
| sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ ssList(sk3)
| ~ spl0_3
| ~ spl0_13
| ~ spl0_5106 ),
inference(superposition,[],[f199101,f121003]) ).
fof(f208105,plain,
( sk10 = hd(sk9)
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_5024 ),
inference(resolution,[],[f196560,f16508]) ).
fof(f208120,plain,
( $false
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_13
| spl0_681
| ~ spl0_5024 ),
inference(forward_subsumption_resolution,[],[f208105,f21527]) ).
fof(f208121,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_13
| spl0_681
| ~ spl0_5024 ),
inference(avatar_contradiction_clause,[],[f208120]) ).
fof(f209784,plain,
( spl0_15
| spl0_92
| ~ spl0_275 ),
inference(avatar_split_clause,[],[f21900,f7149,f2683,f719]) ).
fof(f209915,plain,
( nil = sk9
| tl(cons(sk10,sk9)) = cons(skaf83(tl(cons(sk10,sk9))),skaf82(tl(cons(sk10,sk9))))
| ~ spl0_13
| ~ spl0_4005
| spl0_4028 ),
inference(forward_subsumption_resolution,[],[f130880,f130890]) ).
fof(f211264,plain,
( sk9 = cons(skaf83(sk9),skaf82(sk9))
| nil = sk9
| ~ spl0_13
| ~ spl0_4005
| spl0_4028 ),
inference(forward_demodulation,[],[f209915,f609]) ).
fof(f212636,plain,
( spl0_15
| spl0_50
| ~ spl0_13
| ~ spl0_4005
| spl0_4028 ),
inference(avatar_split_clause,[],[f211264,f130889,f130467,f430,f2231,f719]) ).
fof(f214935,plain,
( sk3 != cons(sk10,nil)
| ~ spl0_15
| spl0_3732 ),
inference(superposition,[],[f123888,f721]) ).
fof(f215105,plain,
( $false
| ~ spl0_3
| ~ spl0_15
| spl0_3732 ),
inference(forward_subsumption_resolution,[],[f214935,f383]) ).
fof(f215106,plain,
( ~ spl0_3
| ~ spl0_15
| spl0_3732 ),
inference(avatar_contradiction_clause,[],[f215105]) ).
fof(f215586,plain,
( sk3 != cons(sk10,sk9)
| sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ spl0_3
| ~ spl0_13
| ~ spl0_200
| ~ spl0_5106 ),
inference(forward_subsumption_resolution,[],[f201096,f6414]) ).
fof(f215843,plain,
( sk3 != cons(sk10,nil)
| sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ spl0_3
| ~ spl0_13
| ~ spl0_15
| ~ spl0_200
| ~ spl0_5106 ),
inference(forward_demodulation,[],[f215586,f721]) ).
fof(f215950,plain,
( sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ spl0_3
| ~ spl0_13
| ~ spl0_15
| ~ spl0_200
| ~ spl0_5106 ),
inference(forward_subsumption_resolution,[],[f215843,f383]) ).
fof(f216013,plain,
( spl0_5151
| ~ spl0_3
| ~ spl0_13
| ~ spl0_15
| ~ spl0_200
| ~ spl0_5106 ),
inference(avatar_split_clause,[],[f215950,f199100,f6412,f719,f430,f381,f200265]) ).
fof(f232464,plain,
( memberP(sk3,sk6)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(nil)
| ~ spl0_13
| ~ spl0_5151 ),
inference(superposition,[],[f8321,f200267]) ).
fof(f232489,plain,
( memberP(sk3,sk6)
| ~ ssList(nil)
| ~ spl0_13
| ~ spl0_164
| ~ spl0_5151 ),
inference(forward_subsumption_resolution,[],[f232464,f6154]) ).
fof(f232509,plain,
( memberP(sk3,sk6)
| ~ spl0_7
| ~ spl0_13
| ~ spl0_164
| ~ spl0_5151 ),
inference(forward_subsumption_resolution,[],[f232489,f403]) ).
fof(f232529,plain,
( sk6 = sk10
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_164
| ~ spl0_5151 ),
inference(resolution,[],[f232509,f16508]) ).
fof(f232544,plain,
( $false
| ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_164
| spl0_656
| ~ spl0_5151 ),
inference(forward_subsumption_resolution,[],[f232529,f19161]) ).
fof(f232545,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_164
| spl0_656
| ~ spl0_5151 ),
inference(avatar_contradiction_clause,[],[f232544]) ).
cnf(s2,plain,
( spl0_1
| spl0_3 ),
inference(sat_conversion,[],[f384]) ).
cnf(s5,plain,
( spl0_1
| ~ spl0_5 ),
inference(sat_conversion,[],[f395]) ).
cnf(s13,plain,
( spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f435]) ).
cnf(s16,plain,
spl0_7,
inference(sat_conversion,[],[f438]) ).
cnf(s30,plain,
( ~ spl0_7
| spl0_31 ),
inference(sat_conversion,[],[f1002]) ).
cnf(s35,plain,
( ~ spl0_7
| ~ spl0_33 ),
inference(sat_conversion,[],[f1137]) ).
cnf(s51,plain,
( ~ spl0_7
| spl0_38 ),
inference(sat_conversion,[],[f2229]) ).
cnf(s509,plain,
( ~ spl0_1
| ~ spl0_31
| spl0_36
| ~ spl0_164 ),
inference(sat_conversion,[],[f6451]) ).
cnf(s541,plain,
spl0_200,
inference(sat_conversion,[],[f6493]) ).
cnf(s887,plain,
spl0_275,
inference(sat_conversion,[],[f7661]) ).
cnf(s918,plain,
( ~ spl0_7
| ~ spl0_31
| spl0_33
| ~ spl0_36 ),
inference(sat_conversion,[],[f8067]) ).
cnf(s1129,plain,
( spl0_1
| spl0_22
| ~ spl0_200 ),
inference(sat_conversion,[],[f13822]) ).
cnf(s1171,plain,
( ~ spl0_14
| ~ spl0_22
| ~ spl0_460
| spl0_461
| spl0_462 ),
inference(sat_conversion,[],[f14168]) ).
cnf(s1282,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_22
| ~ spl0_460
| spl0_461
| spl0_582 ),
inference(sat_conversion,[],[f15869]) ).
cnf(s1286,plain,
( spl0_1
| ~ spl0_200
| spl0_460 ),
inference(sat_conversion,[],[f15913]) ).
cnf(s1299,plain,
( spl0_1
| ~ spl0_200
| ~ spl0_461 ),
inference(sat_conversion,[],[f16061]) ).
cnf(s1674,plain,
( spl0_15
| spl0_16
| ~ spl0_275 ),
inference(sat_conversion,[],[f22385]) ).
cnf(s2544,plain,
( ~ spl0_200
| spl0_802 ),
inference(sat_conversion,[],[f31040]) ).
cnf(s6696,plain,
( ~ spl0_38
| spl0_164 ),
inference(sat_conversion,[],[f108865]) ).
cnf(s7184,plain,
( ~ spl0_7
| ~ spl0_13
| ~ spl0_15
| ~ spl0_2573 ),
inference(sat_conversion,[],[f114299]) ).
cnf(s7491,plain,
( ~ spl0_7
| ~ spl0_164
| spl0_2573
| ~ spl0_2628 ),
inference(sat_conversion,[],[f119498]) ).
cnf(s7887,plain,
( ~ spl0_3
| ~ spl0_13
| ~ spl0_200
| ~ spl0_423
| ~ spl0_2504
| spl0_2628
| ~ spl0_3732 ),
inference(sat_conversion,[],[f123889]) ).
cnf(s8526,plain,
( ~ spl0_13
| ~ spl0_275
| spl0_4005 ),
inference(sat_conversion,[],[f130488]) ).
cnf(s8584,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_200
| ~ spl0_462
| ~ spl0_582
| ~ spl0_802 ),
inference(sat_conversion,[],[f131813]) ).
cnf(s10850,plain,
( spl0_1
| ~ spl0_7
| ~ spl0_200
| ~ spl0_798 ),
inference(sat_conversion,[],[f156824]) ).
cnf(s10944,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_275
| spl0_798
| ~ spl0_4028 ),
inference(sat_conversion,[],[f160492]) ).
cnf(s11766,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_13
| ~ spl0_16
| ~ spl0_50
| ~ spl0_681
| spl0_3933 ),
inference(sat_conversion,[],[f191118]) ).
cnf(s12821,plain,
( ~ spl0_164
| ~ spl0_200
| spl0_2504 ),
inference(sat_conversion,[],[f196885]) ).
cnf(s12840,plain,
( ~ spl0_3
| spl0_423
| ~ spl0_656 ),
inference(sat_conversion,[],[f197622]) ).
cnf(s12925,plain,
( ~ spl0_26
| spl0_5022 ),
inference(sat_conversion,[],[f199056]) ).
cnf(s12934,plain,
( ~ spl0_26
| spl0_5106 ),
inference(sat_conversion,[],[f199103]) ).
cnf(s12939,plain,
( ~ spl0_13
| ~ spl0_16
| ~ spl0_26
| ~ spl0_92
| spl0_5024 ),
inference(sat_conversion,[],[f199133]) ).
cnf(s12950,plain,
( ~ spl0_7
| spl0_25
| ~ spl0_26
| ~ spl0_685 ),
inference(sat_conversion,[],[f199169]) ).
cnf(s12965,plain,
( spl0_26
| ~ spl0_31
| ~ spl0_164 ),
inference(sat_conversion,[],[f199609]) ).
cnf(s13077,plain,
( ~ spl0_7
| ~ spl0_200
| ~ spl0_275
| spl0_685
| ~ spl0_3933
| ~ spl0_5022 ),
inference(sat_conversion,[],[f200905]) ).
cnf(s13082,plain,
( ~ spl0_25
| ~ spl0_31
| spl0_33
| ~ spl0_164 ),
inference(sat_conversion,[],[f200977]) ).
cnf(s13477,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_13
| spl0_681
| ~ spl0_5024 ),
inference(sat_conversion,[],[f208121]) ).
cnf(s13524,plain,
( spl0_15
| spl0_92
| ~ spl0_275 ),
inference(sat_conversion,[],[f209784]) ).
cnf(s13877,plain,
( ~ spl0_13
| spl0_15
| spl0_50
| ~ spl0_4005
| spl0_4028 ),
inference(sat_conversion,[],[f212636]) ).
cnf(s14655,plain,
( ~ spl0_3
| ~ spl0_15
| spl0_3732 ),
inference(sat_conversion,[],[f215106]) ).
cnf(s14952,plain,
( ~ spl0_3
| ~ spl0_13
| ~ spl0_15
| ~ spl0_200
| ~ spl0_5106
| spl0_5151 ),
inference(sat_conversion,[],[f216013]) ).
cnf(s15606,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_7
| ~ spl0_13
| ~ spl0_164
| spl0_656
| ~ spl0_5151 ),
inference(sat_conversion,[],[f232545]) ).
cnf(s15672,plain,
spl0_802,
inference(rat,[],[s2544,s541]) ).
cnf(s15712,plain,
spl0_38,
inference(rat,[],[s51,s16]) ).
cnf(s15713,plain,
~ spl0_33,
inference(rat,[],[s35,s16]) ).
cnf(s15714,plain,
spl0_31,
inference(rat,[],[s30,s16]) ).
cnf(s15724,plain,
spl0_164,
inference(rat,[],[s6696,s15712]) ).
cnf(s15731,plain,
~ spl0_25,
inference(rat,[],[s13082,s15724,s15713,s15714]) ).
cnf(s15732,plain,
spl0_26,
inference(rat,[],[s12965,s15724,s15714]) ).
cnf(s15733,plain,
~ spl0_36,
inference(rat,[],[s918,s15713,s16,s15714]) ).
cnf(s15735,plain,
~ spl0_1,
inference(rat,[],[s509,s15724,s15733,s15714]) ).
cnf(s15738,plain,
spl0_2504,
inference(rat,[],[s12821,s541,s15724]) ).
cnf(s15749,plain,
spl0_5106,
inference(rat,[],[s12934,s15732]) ).
cnf(s15752,plain,
spl0_5022,
inference(rat,[],[s12925,s15732]) ).
cnf(s15755,plain,
~ spl0_685,
inference(rat,[],[s12950,s15731,s16,s15732]) ).
cnf(s15757,plain,
~ spl0_798,
inference(rat,[],[s10850,s16,s541,s15735]) ).
cnf(s15770,plain,
~ spl0_461,
inference(rat,[],[s1299,s541,s15735]) ).
cnf(s15771,plain,
spl0_460,
inference(rat,[],[s1286,s541,s15735]) ).
cnf(s15772,plain,
spl0_22,
inference(rat,[],[s1129,s541,s15735]) ).
cnf(s15785,plain,
~ spl0_3933,
inference(rat,[],[s13077,s15752,s16,s541,s887,s15755]) ).
cnf(s15866,plain,
~ spl0_5,
inference(rat,[],[s5,s15735]) ).
cnf(s15873,plain,
spl0_3,
inference(rat,[],[s2,s15735]) ).
cnf(s15874,plain,
~ spl0_4028,
inference(rat,[],[s10944,s15866,s15757,s887,s16,s15873]) ).
cnf(s15882,plain,
spl0_582,
inference(rat,[],[s1282,s15866,s15770,s15771,s15772,s16,s15873]) ).
cnf(s15899,plain,
~ spl0_462,
inference(rat,[],[s8584,s15672,s15873,s15866,s541,s16,s15882]) ).
cnf(s15902,plain,
~ spl0_14,
inference(rat,[],[s1171,s15772,s15770,s15771,s15899]) ).
cnf(s15903,plain,
spl0_13,
inference(rat,[],[s13,s15902]) ).
cnf(s15919,plain,
spl0_4005,
inference(rat,[],[s8526,s887,s15903]) ).
cnf(s16261,plain,
spl0_15,
inference(rat,[],[s13477,s11766,s12939,s1674,s13524,s13877,s16,s15866,s15873,s15903,s15785,s15732,s887,s15919,s15874]) ).
cnf(s16273,plain,
spl0_3732,
inference(rat,[],[s14655,s15873,s16261]) ).
cnf(s16287,plain,
~ spl0_2573,
inference(rat,[],[s7184,s15903,s16,s16261]) ).
cnf(s16295,plain,
spl0_5151,
inference(rat,[],[s14952,s15903,s15749,s541,s15873,s16261]) ).
cnf(s16314,plain,
~ spl0_2628,
inference(rat,[],[s7491,s15724,s16,s16287]) ).
cnf(s16323,plain,
spl0_656,
inference(rat,[],[s15606,s15903,s15873,s15724,s15866,s16,s16295]) ).
cnf(s16326,plain,
~ spl0_423,
inference(rat,[],[s7887,s16273,s15903,s15738,s15873,s541,s16314]) ).
cnf(s16334,plain,
$false,
inference(rat,[],[s12840,s15873,s16323,s16326]) ).
fof(f232547,plain,
$false,
inference(avatar_sat_refutation,[],[s16334]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC306-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.17 % Computer : n018.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 09:01:54 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 Running first-order model finding
% 0.08/0.19 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.83/2.34 % (3239512)Will run a generic schedule for satisfiability detection.
% 14.83/2.34 % (3239519)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=782109856:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.83/2.34 % (3239518)% WARNING: option uhcvi not known.
% 14.83/2.34 % (3239520)dis+10_1_sil=32000:sp=arity:random_seed=4040630241:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.83/2.34 % (3239517)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1568778837_2999 on theBenchmark for (2999ds/0Mi)
% 14.83/2.34 % (3239521)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3070010349:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.83/2.34 % (3239522)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2682474392:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.83/2.34 % (3239523)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=429424137:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.83/2.34 % (3239518)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3408640113:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.83/2.34 % TRYING [1]
% 14.83/2.34 % TRYING [2]
% 14.83/2.34 % TRYING [3]
% 14.83/2.34 % TRYING [4]
% 14.83/2.34 % (3239520)Instruction limit reached!
% 14.83/2.34 % (3239520)------------------------------
% 14.83/2.34 % (3239520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.83/2.34 % (3239520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/2.34 % (3239520)CaDiCaL version: 2.1.3
% 14.83/2.34 % (3239520)Termination reason: Instruction limit
% 14.83/2.34 % (3239520)Termination phase: Saturation
% 14.83/2.34 % (3239520)Time elapsed: 0.059 s
% 14.83/2.34 % (3239520)Peak memory usage: 13 MB
% 14.83/2.34 % (3239520)Instructions burned: 104 (million)
% 14.83/2.34 % (3239521)Instruction limit reached!
% 14.83/2.34 % (3239521)------------------------------
% 14.83/2.34 % (3239521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.83/2.34 % (3239521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/2.34 % (3239521)CaDiCaL version: 2.1.3
% 14.83/2.34 % (3239521)Termination reason: Instruction limit
% 14.83/2.34 % (3239521)Termination phase: Saturation
% 14.83/2.34 % (3239521)Time elapsed: 0.060 s
% 14.83/2.34 % (3239521)Peak memory usage: 13 MB
% 14.83/2.34 % (3239521)Instructions burned: 118 (million)
% 14.83/2.34 % (3239522)Instruction limit reached!
% 14.83/2.34 % (3239522)------------------------------
% 14.83/2.34 % (3239522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.83/2.34 % (3239522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/2.34 % (3239522)CaDiCaL version: 2.1.3
% 14.83/2.34 % (3239522)Termination reason: Instruction limit
% 14.83/2.34 % (3239522)Termination phase: Saturation
% 14.83/2.34 % (3239522)Time elapsed: 0.065 s
% 14.83/2.34 % (3239522)Peak memory usage: 14 MB
% 14.83/2.34 % (3239522)Instructions burned: 133 (million)
% 14.83/2.34 % (3239531)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=705574865:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.83/2.34 % (3239532)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4208251434:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.83/2.34 % (3239533)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=2235060456:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.83/2.34 % TRYING [1]
% 14.83/2.34 % TRYING [2]
% 14.83/2.34 % TRYING [3]
% 14.83/2.34 % (3239523)Instruction limit reached!
% 14.83/2.34 % (3239523)------------------------------
% 14.83/2.34 % (3239523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.83/2.34 % (3239523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/2.34 % (3239523)CaDiCaL version: 2.1.3
% 14.83/2.34 % (3239523)Termination reason: Instruction limit
% 14.83/2.34 % (3239523)Termination phase: Saturation
% 14.83/2.34 % (3239523)Time elapsed: 0.097 s
% 14.83/2.34 % (3239523)Peak memory usage: 14 MB
% 14.83/2.34 % (3239523)Instructions burned: 167 (million)
% 14.83/2.34 % TRYING [5]
% 14.83/2.34 % TRYING [4]
% 14.83/2.34 % (3239537)ott-21_1_sil=16000:fs=off:random_seed=2998841892:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.83/2.34 % (3239532)Instruction limit reached!
% 14.83/2.34 % (3239532)------------------------------
% 14.83/2.34 % (3239532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.70/6.89 % (3239532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.70/6.89 % (3239532)CaDiCaL version: 2.1.3
% 46.70/6.89 % (3239532)Termination reason: Instruction limit
% 46.70/6.89 % (3239532)Termination phase: Saturation
% 46.70/6.89 % (3239532)Time elapsed: 0.072 s
% 46.70/6.89 % (3239532)Peak memory usage: 13 MB
% 46.70/6.89 % (3239532)Instructions burned: 132 (million)
% 46.70/6.89 % (3239539)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3187870949:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 46.70/6.89 % TRYING [5]
% 46.70/6.89 % (3239537)Instruction limit reached!
% 46.70/6.89 % (3239537)------------------------------
% 46.70/6.89 % (3239537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.70/6.89 % (3239537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.70/6.89 % (3239537)CaDiCaL version: 2.1.3
% 46.70/6.89 % (3239537)Termination reason: Instruction limit
% 46.70/6.89 % (3239537)Termination phase: Saturation
% 46.70/6.89 % (3239537)Time elapsed: 0.089 s
% 46.70/6.89 % (3239537)Peak memory usage: 13 MB
% 46.70/6.89 % (3239537)Instructions burned: 181 (million)
% 46.70/6.89 % (3239541)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1948037851:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 46.70/6.89 % TRYING [1]
% 46.70/6.89 % TRYING [2]
% 46.70/6.89 % TRYING [3]
% 46.70/6.89 % TRYING [6]
% 46.70/6.89 % TRYING [4]
% 46.70/6.89 % TRYING [6]
% 46.70/6.89 % (3239531)Instruction limit reached!
% 46.70/6.89 % (3239531)------------------------------
% 46.70/6.89 % (3239531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.70/6.89 % (3239531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.70/6.89 % (3239531)CaDiCaL version: 2.1.3
% 46.70/6.89 % (3239531)Termination reason: Instruction limit
% 46.70/6.89 % (3239531)Termination phase: Finite model building constraint generation
% 46.70/6.89 % (3239531)Time elapsed: 0.271 s
% 46.70/6.89 % (3239531)Peak memory usage: 34 MB
% 46.70/6.89 % (3239531)Instructions burned: 716 (million)
% 46.70/6.89 % (3239543)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3550470773:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 46.70/6.89 % TRYING [5]
% 46.70/6.89 % (3239533)Instruction limit reached!
% 46.70/6.89 % (3239533)------------------------------
% 46.70/6.89 % (3239533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.70/6.89 % (3239533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.70/6.89 % (3239533)CaDiCaL version: 2.1.3
% 46.70/6.89 % (3239533)Termination reason: Instruction limit
% 46.70/6.89 % (3239533)Termination phase: Saturation
% 46.70/6.89 % (3239533)Time elapsed: 0.385 s
% 46.70/6.89 % (3239533)Peak memory usage: 21 MB
% 46.70/6.89 % (3239533)Instructions burned: 684 (million)
% 46.70/6.89 % (3239539)Instruction limit reached!
% 46.70/6.89 % (3239539)------------------------------
% 46.70/6.89 % (3239539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.70/6.89 % (3239539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.70/6.89 % (3239539)CaDiCaL version: 2.1.3
% 46.70/6.89 % (3239539)Termination reason: Instruction limit
% 46.70/6.89 % (3239539)Termination phase: Saturation
% 46.70/6.89 % (3239539)Time elapsed: 0.311 s
% 46.70/6.89 % (3239539)Peak memory usage: 15 MB
% 46.70/6.89 % (3239539)Instructions burned: 478 (million)
% 46.70/6.89 % (3239545)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1095655318:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 46.70/6.89 % (3239546)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=1458058576:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 46.70/6.89 % (3239541)Instruction limit reached!
% 46.70/6.89 % (3239541)------------------------------
% 46.70/6.89 % (3239541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.70/6.89 % (3239541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.70/6.89 % (3239541)CaDiCaL version: 2.1.3
% 46.70/6.89 % (3239541)Termination reason: Instruction limit
% 46.70/6.89 % (3239541)Termination phase: Finite model building SAT solving
% 46.70/6.89 % (3239541)Time elapsed: 0.346 s
% 46.70/6.89 % (3239541)Peak memory usage: 22 MB
% 46.70/6.89 % (3239541)Instructions burned: 867 (million)
% 46.70/6.89 % TRYING [14]
% 46.70/6.89 % (3239549)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3481530793:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 46.70/6.89 % TRYING [7]
% 48.41/7.11 % (3239545)Instruction limit reached!
% 48.41/7.11 % (3239545)------------------------------
% 48.41/7.11 % (3239545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.41/7.11 % (3239545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.41/7.11 % (3239545)CaDiCaL version: 2.1.3
% 48.41/7.11 % (3239545)Termination reason: Instruction limit
% 48.41/7.11 % (3239545)Termination phase: Finite model building constraint generation
% 48.41/7.11 % (3239545)Time elapsed: 0.321 s
% 48.41/7.11 % (3239545)Peak memory usage: 72 MB
% 48.41/7.11 % (3239545)Instructions burned: 889 (million)
% 48.41/7.11 % (3239551)fmb+10_1_sil=64000:random_seed=2699531348:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 48.41/7.11 % TRYING [1]
% 48.41/7.11 % TRYING [2]
% 48.41/7.11 % TRYING [3]
% 48.41/7.11 % (3239546)Instruction limit reached!
% 48.41/7.11 % (3239546)------------------------------
% 48.41/7.11 % (3239546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.41/7.11 % (3239546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.41/7.11 % (3239546)CaDiCaL version: 2.1.3
% 48.41/7.11 % (3239546)Termination reason: Instruction limit
% 48.41/7.11 % (3239546)Termination phase: Saturation
% 48.41/7.11 % (3239546)Time elapsed: 0.387 s
% 48.41/7.11 % (3239546)Peak memory usage: 18 MB
% 48.41/7.11 % (3239546)Instructions burned: 692 (million)
% 48.41/7.11 % (3239553)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1689528715:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 48.41/7.11 % TRYING [4]
% 48.41/7.11 % TRYING [20]
% 48.41/7.11 % (3239543)Instruction limit reached!
% 48.41/7.11 % (3239543)------------------------------
% 48.41/7.11 % (3239543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.41/7.11 % (3239543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.41/7.11 % (3239543)CaDiCaL version: 2.1.3
% 48.41/7.11 % (3239543)Termination reason: Instruction limit
% 48.41/7.11 % (3239543)Termination phase: Saturation
% 48.41/7.11 % (3239543)Time elapsed: 0.678 s
% 48.41/7.11 % (3239543)Peak memory usage: 29 MB
% 48.41/7.11 % (3239543)Instructions burned: 1179 (million)
% 48.41/7.11 % (3239549)Instruction limit reached!
% 48.41/7.11 % (3239549)------------------------------
% 48.41/7.11 % (3239549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.41/7.11 % (3239549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.41/7.11 % (3239549)CaDiCaL version: 2.1.3
% 48.41/7.11 % (3239549)Termination reason: Instruction limit
% 48.41/7.11 % (3239549)Termination phase: Saturation
% 48.41/7.11 % (3239549)Time elapsed: 0.471 s
% 48.41/7.11 % (3239549)Peak memory usage: 20 MB
% 48.41/7.11 % (3239549)Instructions burned: 879 (million)
% 48.41/7.11 % (3239555)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3167389186:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 48.41/7.11 % TRYING [5]
% 48.41/7.11 % TRYING [8]
% 48.41/7.11 % (3239556)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2311906076:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 48.41/7.11 % (3239555)Instruction limit reached!
% 48.41/7.11 % (3239555)------------------------------
% 48.41/7.11 % (3239555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.41/7.11 % (3239555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.41/7.11 % (3239555)CaDiCaL version: 2.1.3
% 48.41/7.11 % (3239555)Termination reason: Instruction limit
% 48.41/7.11 % (3239555)Termination phase: Finite model building constraint generation
% 48.41/7.11 % (3239555)Time elapsed: 0.338 s
% 48.41/7.11 % (3239555)Peak memory usage: 79 MB
% 48.41/7.11 % (3239555)Instructions burned: 922 (million)
% 48.41/7.11 % (3239559)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=47636121:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 48.41/7.11 % TRYING [6]
% 48.41/7.11 % TRYING [8]
% 48.41/7.11 % (3239559)Instruction limit reached!
% 48.41/7.11 % (3239559)------------------------------
% 48.41/7.11 % (3239559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.41/7.11 % (3239559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.41/7.11 % (3239559)CaDiCaL version: 2.1.3
% 48.41/7.11 % (3239559)Termination reason: Instruction limit
% 48.41/7.11 % (3239559)Termination phase: Saturation
% 48.41/7.11 % (3239559)Time elapsed: 0.637 s
% 48.41/7.11 % (3239559)Peak memory usage: 15 MB
% 48.41/7.11 % (3239559)Instructions burned: 1473 (million)
% 48.41/7.11 % (3239561)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2049229776:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 48.41/7.11 % TRYING [77]
% 48.41/7.11 % TRYING [7]
% 48.41/7.11 % (3239556)Instruction limit reached!
% 48.41/7.11 % (3239556)------------------------------
% 48.41/7.11 % (3239556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.41/7.11 % (3239556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.41/7.11 % (3239556)CaDiCaL version: 2.1.3
% 48.41/7.11 % (3239556)Termination reason: Instruction limit
% 48.41/7.11 % (3239556)Termination phase: Saturation
% 48.41/7.11 % (3239556)Time elapsed: 2.609 s
% 48.41/7.11 % (3239556)Peak memory usage: 56 MB
% 48.41/7.11 % (3239556)Instructions burned: 5133 (million)
% 48.41/7.11 % (3239563)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1647547736:fmbsr=2.30978:i=2174_2962 on theBenchmark for (2962ds/2174Mi)
% 48.41/7.11 % TRYING [16]
% 48.41/7.11 % TRYING [9]
% 48.41/7.11 % (3239553)Instruction limit reached!
% 48.41/7.11 % (3239553)------------------------------
% 48.41/7.11 % (3239553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.41/7.11 % (3239553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.41/7.11 % (3239553)CaDiCaL version: 2.1.3
% 48.41/7.11 % (3239553)Termination reason: Instruction limit
% 48.41/7.11 % (3239553)Termination phase: Finite model building constraint generation
% 48.41/7.11 % (3239553)Time elapsed: 3.258 s
% 48.41/7.11 % (3239553)Peak memory usage: 589 MB
% 48.41/7.11 % (3239553)Instructions burned: 9515 (million)
% 48.41/7.11 % TRYING [8]
% 48.41/7.11 % (3239565)ott-2_1_sil=16000:newcnf=on:random_seed=2013978880:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 48.41/7.11 % (3239561)Instruction limit reached!
% 48.41/7.11 % (3239561)------------------------------
% 48.41/7.11 % (3239561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.41/7.11 % (3239561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.41/7.11 % (3239561)CaDiCaL version: 2.1.3
% 48.41/7.11 % (3239561)Termination reason: Instruction limit
% 48.41/7.11 % (3239561)Termination phase: Finite model building constraint generation
% 48.41/7.11 % (3239561)Time elapsed: 2.237 s
% 48.41/7.11 % (3239561)Peak memory usage: 431 MB
% 48.41/7.11 % (3239561)Instructions burned: 6325 (million)
% 48.41/7.11 % (3239567)ott+10_1_sil=32000:tgt=ground:random_seed=2874533734:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 48.41/7.11 % (3239563)Instruction limit reached!
% 48.41/7.11 % (3239563)------------------------------
% 48.41/7.11 % (3239563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.41/7.11 % (3239563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.41/7.11 % (3239563)CaDiCaL version: 2.1.3
% 48.41/7.11 % (3239563)Termination reason: Instruction limit
% 48.41/7.11 % (3239563)Termination phase: Finite model building constraint generation
% 48.41/7.11 % (3239563)Time elapsed: 0.750 s
% 48.41/7.11 % (3239563)Peak memory usage: 138 MB
% 48.41/7.11 % (3239563)Instructions burned: 2174 (million)
% 48.41/7.11 % (3239569)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4048547451:i=54282_2954 on theBenchmark for (2954ds/54282Mi)
% 48.41/7.11 % TRYING [1]
% 48.41/7.11 % TRYING [2]
% 48.41/7.11 % TRYING [3]
% 48.41/7.11 % TRYING [4]
% 48.41/7.11 % TRYING [5]
% 48.41/7.11 % (3239565)Instruction limit reached!
% 48.41/7.11 % (3239565)------------------------------
% 48.41/7.11 % (3239565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.41/7.11 % (3239565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.41/7.11 % (3239565)CaDiCaL version: 2.1.3
% 48.41/7.11 % (3239565)Termination reason: Instruction limit
% 48.41/7.11 % (3239565)Termination phase: Saturation
% 48.41/7.11 % (3239565)Time elapsed: 0.451 s
% 48.41/7.11 % (3239565)Peak memory usage: 25 MB
% 48.41/7.11 % (3239565)Instructions burned: 869 (million)
% 48.41/7.11 % (3239571)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3885994627:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi)
% 48.41/7.11 % TRYING [6]
% 48.41/7.11 % TRYING [7]
% 48.41/7.11 % TRYING [8]
% 48.41/7.11 % (3239571)Instruction limit reached!
% 48.41/7.11 % (3239571)------------------------------
% 48.41/7.11 % (3239571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.41/7.11 % (3239571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.41/7.11 % (3239571)CaDiCaL version: 2.1.3
% 48.41/7.11 % (3239571)Termination reason: Instruction limit
% 48.41/7.11 % (3239571)Termination phase: Saturation
% 48.41/7.11 % (3239571)Time elapsed: 1.908 s
% 48.41/7.11 % (3239571)Peak memory usage: 42 MB
% 48.41/7.11 % (3239571)Instructions burned: 3512 (million)
% 48.41/7.11 % (3239573)dis+21_1_sil=32000:sas=cadical:random_seed=156706145:i=3773:amm=off_2933 on theBenchmark for (2933ds/3773Mi)
% 48.41/7.11 % (3239518) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3239512-3239518"...
% 48.41/7.11 % (3239518)...printing done.
% 48.41/7.11 % (3239518)Refutation found. Thanks to Tanya!
% 48.41/7.11 % SZS status Unsatisfiable for theBenchmark
% 48.41/7.11 % SZS output start Proof for theBenchmark
% See solution above
% 48.41/7.12 % (3239518)------------------------------
% 48.41/7.12 % (3239518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.41/7.12 % (3239518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.41/7.12 % (3239518)CaDiCaL version: 2.1.3
% 48.41/7.12 % (3239518)Termination reason: Refutation
% 48.41/7.12 % (3239518)Time elapsed: 6.799 s
% 48.41/7.12 % (3239518)Peak memory usage: 106 MB
% 48.41/7.12 % (3239518)Instructions burned: 11700 (million)
% 48.41/7.12 % (3239512)Success in time 6.913 s
% 48.41/7.12 % Vampire exiting
%------------------------------------------------------------------------------