%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC173-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 : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:04:57 PM UTC 2026
% Result : Unsatisfiable 10.33s 2.51s
% Output : Refutation 10.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 63
% Syntax : Number of formulae : 338 ( 53 unt; 25 def)
% Number of atoms : 1139 ( 102 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 1295 ( 494 ~; 776 |; 0 &)
% ( 25 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 26 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 230 ( 0 sgn 230 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f11,axiom,
~ singletonP(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause11) ).
fof(f13,axiom,
! [X0] : ssList(skaf82(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause13) ).
fof(f60,axiom,
! [X0] :
( ~ ssList(X0)
| frontsegP(X0,nil) ),
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(f74,axiom,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause74) ).
fof(f75,axiom,
! [X0] :
( ~ ssList(X0)
| ssList(tl(X0))
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause75) ).
fof(f80,axiom,
! [X0] :
( ~ segmentP(nil,X0)
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause80) ).
fof(f85,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ssList(app(X1,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(f97,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| hd(cons(X0,X1)) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause97) ).
fof(f100,axiom,
! [X0,X1] :
( cons(X0,X1) != X1
| ~ ssItem(X0)
| ~ ssList(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause99) ).
fof(f104,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssItem(X1)
| neq(X1,X0)
| X1 = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause102) ).
fof(f105,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssItem(X1)
| neq(X1,X0)
| X0 = X1 ),
inference(reorient_equations,[],[f104]) ).
fof(f107,axiom,
! [X0] :
( ~ ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
file('/export/starexec/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(f119,axiom,
! [X0,X1] :
( cons(X0,nil) != X1
| ~ ssItem(X0)
| ~ ssList(X1)
| singletonP(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause116) ).
fof(f125,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| app(cons(X0,nil),X1) = cons(X0,X1) ),
file('/export/starexec/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(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(f148,axiom,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| frontsegP(app(X0,X2),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause137) ).
fof(f151,axiom,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| memberP(app(X0,X2),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause140) ).
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(f166,axiom,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| frontsegP(X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause154) ).
fof(f173,axiom,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X2 = X0 ),
file('/export/starexec/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(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(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/sandbox/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/sandbox/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/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(f200,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_1) ).
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,
app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).
fof(f211,plain,
sk1 = app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8),
inference(reorient_equations,[],[f210]) ).
fof(f212,negated_conjecture,
~ neq(sk5,sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_12) ).
fof(f225,negated_conjecture,
( cons(sk9,nil) = sk3
| nil = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_23) ).
fof(f226,plain,
( sk3 = cons(sk9,nil)
| nil = sk3 ),
inference(reorient_equations,[],[f225]) ).
fof(f231,plain,
ssList(sk3),
inference(definition_unfolding,[],[f200,f205]) ).
fof(f233,plain,
sk3 = app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8),
inference(definition_unfolding,[],[f211,f205]) ).
fof(f241,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(cons(X0,nil))
| singletonP(cons(X0,nil)) ),
inference(equality_resolution,[],[f119]) ).
fof(f245,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1))
| frontsegP(app(X0,X1),X0) ),
inference(equality_resolution,[],[f155]) ).
fof(f248,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(f249,plain,
! [X2,X0,X1] :
( ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(app(X0,cons(X1,X2)))
| memberP(app(X0,cons(X1,X2)),X1) ),
inference(equality_resolution,[],[f189]) ).
fof(f250,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(f251,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(f260,plain,
~ ssList(nil),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f264,plain,
! [X0] : ~ ssList(skaf82(X0)),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f310,plain,
! [X0] :
( frontsegP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f321,plain,
! [X0] :
( ~ memberP(nil,X0)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f71]) ).
fof(f322,plain,
! [X0,X1] :
( ssList(X0)
| duplicatefreeP(X0)
| ~ ssItem(X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f324,plain,
! [X0] :
( ssList(X0)
| app(nil,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f325,plain,
! [X0] :
( ~ ssList(tl(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f330,plain,
! [X0] :
( ~ segmentP(nil,X0)
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f335,plain,
! [X0,X1] :
( ~ ssList(app(X1,X0))
| ssList(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f336,plain,
! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f347,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| hd(cons(X0,X1)) = X0 ),
inference(consistent_polarity_flipping,[],[f97]) ).
fof(f349,plain,
! [X0,X1] :
( cons(X0,X1) != X1
| ssItem(X0)
| ssList(X1) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f352,plain,
! [X0,X1] :
( ~ neq(X1,X0)
| ssItem(X1)
| ssItem(X0)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f105]) ).
fof(f354,plain,
! [X0] :
( ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f359,plain,
! [X0] :
( ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f366,plain,
! [X0] :
( singletonP(cons(X0,nil))
| ssList(cons(X0,nil))
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f241]) ).
fof(f370,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f379,plain,
! [X0,X1] :
( ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f387,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X2)
| ssList(X1)
| ssList(X0)
| frontsegP(app(X0,X2),X1) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f390,plain,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ssList(X2)
| ssList(X0)
| ssItem(X1)
| memberP(app(X0,X2),X1) ),
inference(consistent_polarity_flipping,[],[f151]) ).
fof(f394,plain,
! [X0,X1] :
( ssList(X1)
| ssList(X0)
| ssList(app(X0,X1))
| frontsegP(app(X0,X1),X0) ),
inference(consistent_polarity_flipping,[],[f245]) ).
fof(f404,plain,
! [X2,X0,X1] :
( ~ frontsegP(X1,X2)
| ~ frontsegP(X0,X1)
| ssList(X2)
| ssList(X1)
| ssList(X0)
| frontsegP(X0,X2) ),
inference(consistent_polarity_flipping,[],[f166]) ).
fof(f411,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(f423,plain,
! [X2,X0,X1] :
( segmentP(app(app(X0,X1),X2),X1)
| ssList(X0)
| ssList(X1)
| ssList(app(app(X0,X1),X2))
| ssList(X2) ),
inference(consistent_polarity_flipping,[],[f248]) ).
fof(f425,plain,
! [X2,X0,X1] :
( memberP(app(X0,cons(X1,X2)),X1)
| ssList(X0)
| ssItem(X1)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2) ),
inference(consistent_polarity_flipping,[],[f249]) ).
fof(f426,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(f428,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,[],[f250]) ).
fof(f429,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,[],[f251]) ).
fof(f436,plain,
~ ssList(sk3),
inference(consistent_polarity_flipping,[],[f231]) ).
fof(f440,plain,
~ ssItem(sk5),
inference(consistent_polarity_flipping,[],[f206]) ).
fof(f441,plain,
~ ssItem(sk6),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f442,plain,
~ ssList(sk7),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f443,plain,
~ ssList(sk8),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f444,plain,
neq(sk5,sk6),
inference(consistent_polarity_flipping,[],[f212]) ).
fof(f455,plain,
! [X3,X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| ssItem(X3)
| frontsegP(cons(X3,X0),cons(X3,X1)) ),
inference(duplicate_literal_removal,[],[f428]) ).
fof(f462,definition,
( spl0_1
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f464,plain,
( nil = sk3
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f462]) ).
fof(f479,definition,
( spl0_5
<=> sk3 = cons(sk9,nil) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f481,plain,
( sk3 = cons(sk9,nil)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f482,plain,
( spl0_1
| spl0_5 ),
inference(avatar_split_clause,[],[f226,f479,f462]) ).
fof(f514,definition,
( spl0_11
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f515,plain,
( ~ ssList(nil)
| spl0_11 ),
inference(avatar_component_clause,[],[f514]) ).
fof(f542,definition,
( spl0_17
<=> ! [X1] : ~ ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f543,plain,
( ! [X1] : ~ ssItem(X1)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f542]) ).
fof(f545,definition,
( spl0_18
<=> ! [X0] :
( ssList(X0)
| duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f546,plain,
( ! [X0] :
( duplicatefreeP(X0)
| ssList(X0) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f545]) ).
fof(f547,plain,
( spl0_17
| spl0_18 ),
inference(avatar_split_clause,[],[f322,f545,f542]) ).
fof(f550,plain,
~ spl0_11,
inference(avatar_split_clause,[],[f260,f514]) ).
fof(f556,plain,
( ! [X0] : ~ memberP(nil,X0)
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f321,f543]) ).
fof(f634,plain,
sk3 = app(nil,sk3),
inference(resolution,[],[f324,f436]) ).
fof(f666,plain,
( ! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1) )
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f336,f543]) ).
fof(f683,plain,
( ! [X0,X1] :
( cons(X0,X1) != X1
| ssList(X1) )
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f349,f543]) ).
fof(f727,plain,
( ! [X0,X1] :
( ssList(X1)
| hd(cons(X0,X1)) = X0 )
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f347,f543]) ).
fof(f729,plain,
( ! [X0,X1] : hd(cons(X0,skaf82(X1))) = X0
| ~ spl0_17 ),
inference(resolution,[],[f727,f264]) ).
fof(f770,definition,
( spl0_19
<=> sk5 = sk6 ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f772,plain,
( sk5 = sk6
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f770]) ).
fof(f848,plain,
( sk7 = cons(hd(sk7),tl(sk7))
| nil = sk7 ),
inference(resolution,[],[f354,f442]) ).
fof(f880,definition,
( spl0_28
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f882,plain,
( nil = sk7
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f880]) ).
fof(f884,definition,
( spl0_29
<=> sk7 = cons(hd(sk7),tl(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f886,plain,
( sk7 = cons(hd(sk7),tl(sk7))
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f884]) ).
fof(f887,plain,
( spl0_28
| spl0_29 ),
inference(avatar_split_clause,[],[f848,f884,f880]) ).
fof(f961,plain,
( sk7 = cons(skaf83(sk7),skaf82(sk7))
| nil = sk7 ),
inference(resolution,[],[f359,f442]) ).
fof(f978,definition,
( spl0_32
<=> ssList(app(app(nil,cons(sk5,nil)),cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f979,plain,
( ~ ssList(app(app(nil,cons(sk5,nil)),cons(sk5,nil)))
| spl0_32 ),
inference(avatar_component_clause,[],[f978]) ).
fof(f980,plain,
( ssList(app(app(nil,cons(sk5,nil)),cons(sk5,nil)))
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f978]) ).
fof(f1008,definition,
( spl0_37
<=> ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f1010,plain,
( ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f1008]) ).
fof(f1013,definition,
( spl0_38
<=> sk7 = cons(skaf83(sk7),skaf82(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f1015,plain,
( sk7 = cons(skaf83(sk7),skaf82(sk7))
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f1013]) ).
fof(f1016,plain,
( spl0_28
| spl0_38 ),
inference(avatar_split_clause,[],[f961,f1013,f880]) ).
fof(f1105,definition,
( spl0_45
<=> ssList(cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f1106,plain,
( ~ ssList(cons(sk6,nil))
| spl0_45 ),
inference(avatar_component_clause,[],[f1105]) ).
fof(f1107,plain,
( ssList(cons(sk6,nil))
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f1105]) ).
fof(f1109,definition,
( spl0_46
<=> ssList(app(nil,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f1111,plain,
( ssList(app(nil,cons(sk5,nil)))
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f1109]) ).
fof(f1151,plain,
( ssList(nil)
| ssItem(sk6)
| ~ spl0_45 ),
inference(resolution,[],[f336,f1107]) ).
fof(f1158,plain,
( ssItem(sk6)
| spl0_11
| ~ spl0_45 ),
inference(forward_subsumption_resolution,[],[f1151,f515]) ).
fof(f1159,plain,
( $false
| spl0_11
| ~ spl0_45 ),
inference(forward_subsumption_resolution,[],[f1158,f441]) ).
fof(f1160,plain,
( spl0_11
| ~ spl0_45 ),
inference(avatar_contradiction_clause,[],[f1159]) ).
fof(f1175,definition,
( spl0_50
<=> ssList(tl(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f1177,plain,
( ssList(tl(sk7))
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f1175]) ).
fof(f1244,plain,
( ssList(sk7)
| nil = sk7
| ~ spl0_50 ),
inference(resolution,[],[f1177,f325]) ).
fof(f1245,plain,
( nil = sk7
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f1244,f442]) ).
fof(f1299,plain,
( ssItem(sk5)
| ssItem(sk6)
| sk5 = sk6 ),
inference(resolution,[],[f352,f444]) ).
fof(f1304,plain,
( ssItem(sk6)
| sk5 = sk6 ),
inference(forward_subsumption_resolution,[],[f1299,f440]) ).
fof(f1305,plain,
sk5 = sk6,
inference(forward_subsumption_resolution,[],[f1304,f441]) ).
fof(f1312,plain,
spl0_19,
inference(avatar_split_clause,[],[f1305,f770]) ).
fof(f1454,plain,
( spl0_28
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f1245,f1175,f880]) ).
fof(f1539,plain,
( ~ ssList(cons(sk5,nil))
| ~ spl0_19
| spl0_45 ),
inference(forward_demodulation,[],[f1106,f772]) ).
fof(f1578,plain,
! [X0,X1] :
( frontsegP(app(X0,X1),X0)
| ssList(X0)
| ssList(X1) ),
inference(forward_subsumption_resolution,[],[f394,f335]) ).
fof(f1586,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,[],[f1578,f233]) ).
fof(f1593,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,[],[f1586,f443]) ).
fof(f1595,plain,
( frontsegP(sk3,app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1593,f772]) ).
fof(f1757,plain,
! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X1,X2))
| frontsegP(app(app(X1,X2),X0),X1)
| ssList(X1)
| ssList(X2) ),
inference(resolution,[],[f387,f1578]) ).
fof(f1758,plain,
! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X1,X2))
| frontsegP(app(app(X1,X2),X0),X1)
| ssList(X2) ),
inference(duplicate_literal_removal,[],[f1757]) ).
fof(f1762,plain,
! [X2,X0,X1] :
( frontsegP(app(app(X1,X2),X0),X1)
| ssList(X1)
| ssList(X0)
| ssList(X2) ),
inference(forward_subsumption_resolution,[],[f1758,f335]) ).
fof(f1799,plain,
( frontsegP(sk3,app(app(nil,cons(sk5,nil)),cons(sk5,nil)))
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ spl0_19
| ~ spl0_28 ),
inference(forward_demodulation,[],[f1595,f882]) ).
fof(f1862,definition,
( spl0_72
<=> nil = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f1863,plain,
( nil != cons(sk5,nil)
| spl0_72 ),
inference(avatar_component_clause,[],[f1862]) ).
fof(f1864,plain,
( nil = cons(sk5,nil)
| ~ spl0_72 ),
inference(avatar_component_clause,[],[f1862]) ).
fof(f1891,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,app(X1,X2))
| ssList(X1)
| ssList(app(X1,X2))
| ssList(X0)
| frontsegP(X0,X1)
| ssList(X1)
| ssList(X2) ),
inference(resolution,[],[f404,f1578]) ).
fof(f1892,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,app(X1,X2))
| ssList(X1)
| ssList(app(X1,X2))
| ssList(X0)
| frontsegP(X0,X1)
| ssList(X2) ),
inference(duplicate_literal_removal,[],[f1891]) ).
fof(f1896,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,app(X1,X2))
| ssList(X1)
| ssList(X0)
| frontsegP(X0,X1)
| ssList(X2) ),
inference(forward_subsumption_resolution,[],[f1892,f335]) ).
fof(f2456,plain,
( singletonP(nil)
| ssList(nil)
| ssItem(sk5)
| ~ spl0_72 ),
inference(superposition,[],[f366,f1864]) ).
fof(f2469,plain,
( ssList(nil)
| ssItem(sk5)
| ~ spl0_72 ),
inference(forward_subsumption_resolution,[],[f2456,f11]) ).
fof(f2476,plain,
( ssItem(sk5)
| spl0_11
| ~ spl0_72 ),
inference(forward_subsumption_resolution,[],[f2469,f515]) ).
fof(f2480,plain,
( $false
| spl0_11
| ~ spl0_72 ),
inference(forward_subsumption_resolution,[],[f2476,f440]) ).
fof(f2481,plain,
( spl0_11
| ~ spl0_72 ),
inference(avatar_contradiction_clause,[],[f2480]) ).
fof(f2608,plain,
( segmentP(sk3,cons(sk6,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| ssList(sk3)
| ssList(sk8) ),
inference(superposition,[],[f423,f233]) ).
fof(f2614,plain,
( segmentP(sk3,cons(sk6,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| ssList(sk8) ),
inference(forward_subsumption_resolution,[],[f2608,f436]) ).
fof(f2621,plain,
( segmentP(sk3,cons(sk6,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil)) ),
inference(forward_subsumption_resolution,[],[f2614,f443]) ).
fof(f2628,plain,
( segmentP(sk3,cons(sk5,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2621,f772]) ).
fof(f2633,plain,
( segmentP(nil,cons(sk5,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| ~ spl0_1
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2628,f464]) ).
fof(f2642,definition,
( spl0_78
<=> segmentP(nil,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f2643,plain,
( ~ segmentP(nil,cons(sk5,nil))
| spl0_78 ),
inference(avatar_component_clause,[],[f2642]) ).
fof(f2644,plain,
( segmentP(nil,cons(sk5,nil))
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f2642]) ).
fof(f2661,plain,
( ssList(cons(sk5,nil))
| nil = cons(sk5,nil)
| ~ spl0_78 ),
inference(resolution,[],[f2644,f330]) ).
fof(f2670,plain,
( nil = cons(sk5,nil)
| ~ spl0_19
| spl0_45
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f2661,f1539]) ).
fof(f2675,plain,
( $false
| ~ spl0_19
| spl0_45
| spl0_72
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f2670,f1863]) ).
fof(f2676,plain,
( ~ spl0_19
| spl0_45
| spl0_72
| ~ spl0_78 ),
inference(avatar_contradiction_clause,[],[f2675]) ).
fof(f2697,plain,
( ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| frontsegP(sk3,app(app(nil,cons(sk5,nil)),cons(sk5,nil)))
| ~ spl0_19
| ~ spl0_28 ),
inference(forward_demodulation,[],[f1799,f772]) ).
fof(f2712,plain,
( ssList(app(app(nil,cons(sk5,nil)),cons(sk5,nil)))
| frontsegP(sk3,app(app(nil,cons(sk5,nil)),cons(sk5,nil)))
| ~ spl0_19
| ~ spl0_28 ),
inference(forward_demodulation,[],[f2697,f882]) ).
fof(f2727,definition,
( spl0_82
<=> frontsegP(sk3,app(app(nil,cons(sk5,nil)),cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f2729,plain,
( frontsegP(sk3,app(app(nil,cons(sk5,nil)),cons(sk5,nil)))
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f2727]) ).
fof(f2730,plain,
( spl0_82
| spl0_32
| ~ spl0_19
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f2712,f880,f770,f978,f2727]) ).
fof(f2886,plain,
( ! [X2,X3,X0,X1] :
( ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(X2)
| ssList(X0)
| ssItem(X1)
| ssList(X3) )
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f429,f546]) ).
fof(f2948,plain,
( ! [X0,X1] :
( ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) )
| ~ spl0_17 ),
inference(backward_subsumption_resolution,[],[f370,f543]) ).
fof(f2957,plain,
( ! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ssList(X2)
| ssList(X0)
| memberP(app(X0,X2),X1) )
| ~ spl0_17 ),
inference(backward_subsumption_resolution,[],[f390,f543]) ).
fof(f2968,plain,
( ! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ssList(X1)
| ssItem(X2)
| memberP(X1,X2)
| X0 = X2 )
| ~ spl0_17 ),
inference(backward_subsumption_resolution,[],[f411,f543]) ).
fof(f2973,plain,
( ! [X2,X0,X1] :
( memberP(app(X0,cons(X1,X2)),X1)
| ssList(X0)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2) )
| ~ spl0_17 ),
inference(backward_subsumption_resolution,[],[f425,f543]) ).
fof(f2974,plain,
( ! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ssList(X3)
| ssList(X1)
| ssItem(X2)
| X0 = X2 )
| ~ spl0_17 ),
inference(backward_subsumption_resolution,[],[f426,f543]) ).
fof(f2976,plain,
( ! [X3,X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| frontsegP(cons(X3,X0),cons(X3,X1)) )
| ~ spl0_17 ),
inference(backward_subsumption_resolution,[],[f455,f543]) ).
fof(f3002,plain,
( ! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ssList(X1)
| memberP(X1,X2)
| X0 = X2 )
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2968,f543]) ).
fof(f3006,plain,
( ! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ssList(X3)
| ssList(X1)
| X0 = X2 )
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2974,f543]) ).
fof(f3282,plain,
( ! [X0] : cons(X0,sk3) = app(cons(X0,nil),sk3)
| ~ spl0_17 ),
inference(resolution,[],[f2948,f436]) ).
fof(f3332,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ssList(nil)
| memberP(nil,X0)
| sk9 = X0 )
| ~ spl0_5
| ~ spl0_17 ),
inference(superposition,[],[f3002,f481]) ).
fof(f3334,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| memberP(nil,X0)
| sk9 = X0 )
| ~ spl0_5
| spl0_11
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f3332,f515]) ).
fof(f3336,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| sk9 = X0 )
| ~ spl0_5
| spl0_11
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f3334,f556]) ).
fof(f3342,plain,
( ! [X0,X1] :
( ssList(nil)
| ssList(X0)
| frontsegP(cons(X1,X0),cons(X1,nil))
| ssList(X0) )
| ~ spl0_17 ),
inference(resolution,[],[f2976,f310]) ).
fof(f3347,plain,
( ! [X0,X1] :
( ssList(nil)
| ssList(X0)
| frontsegP(cons(X1,X0),cons(X1,nil)) )
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f3342]) ).
fof(f3350,plain,
( ! [X0,X1] :
( frontsegP(cons(X1,X0),cons(X1,nil))
| ssList(X0) )
| spl0_11
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f3347,f515]) ).
fof(f3394,plain,
( ! [X0,X1] :
( ~ frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| ssList(nil)
| sk9 = X0 )
| ~ spl0_5
| ~ spl0_17 ),
inference(superposition,[],[f3006,f481]) ).
fof(f3401,plain,
( ! [X0,X1] :
( ~ frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| sk9 = X0 )
| ~ spl0_5
| spl0_11
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f3394,f515]) ).
fof(f3536,plain,
( ! [X2,X3,X0,X1] :
( ssList(X0)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2)
| ssList(X3)
| ssList(app(X0,cons(X1,X2)))
| memberP(app(app(X0,cons(X1,X2)),X3),X1) )
| ~ spl0_17 ),
inference(resolution,[],[f2973,f2957]) ).
fof(f3544,plain,
( ! [X2,X3,X0,X1] :
( memberP(app(app(X0,cons(X1,X2)),X3),X1)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2)
| ssList(X3)
| ssList(X0) )
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f3536]) ).
fof(f3973,plain,
( app(sk3,sk3) = cons(sk9,sk3)
| ~ spl0_5
| ~ spl0_17 ),
inference(superposition,[],[f3282,f481]) ).
fof(f4019,plain,
( ssList(app(nil,cons(sk5,nil)))
| ssList(cons(sk5,nil))
| ~ spl0_32 ),
inference(resolution,[],[f980,f335]) ).
fof(f4020,plain,
( ssList(app(nil,cons(sk5,nil)))
| ~ spl0_19
| ~ spl0_32
| spl0_45 ),
inference(forward_subsumption_resolution,[],[f4019,f1539]) ).
fof(f4021,plain,
( spl0_46
| ~ spl0_19
| ~ spl0_32
| spl0_45 ),
inference(avatar_split_clause,[],[f4020,f1105,f978,f770,f1109]) ).
fof(f4321,plain,
( ssList(nil)
| ssList(cons(sk5,nil))
| ~ spl0_46 ),
inference(resolution,[],[f1111,f335]) ).
fof(f4322,plain,
( ssList(cons(sk5,nil))
| spl0_11
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f4321,f515]) ).
fof(f4323,plain,
( $false
| spl0_11
| ~ spl0_19
| spl0_45
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f4322,f1539]) ).
fof(f4324,plain,
( spl0_11
| ~ spl0_19
| spl0_45
| ~ spl0_46 ),
inference(avatar_contradiction_clause,[],[f4323]) ).
fof(f6098,plain,
( ssList(nil)
| ssList(nil)
| ssItem(sk5)
| ssList(nil)
| ~ spl0_18
| spl0_32 ),
inference(resolution,[],[f979,f2886]) ).
fof(f6121,plain,
( ssList(nil)
| ssItem(sk5)
| ~ spl0_18
| spl0_32 ),
inference(duplicate_literal_removal,[],[f6098]) ).
fof(f6126,plain,
( ssItem(sk5)
| spl0_11
| ~ spl0_18
| spl0_32 ),
inference(forward_subsumption_resolution,[],[f6121,f515]) ).
fof(f6127,plain,
( $false
| spl0_11
| ~ spl0_18
| spl0_32 ),
inference(forward_subsumption_resolution,[],[f6126,f440]) ).
fof(f6128,plain,
( spl0_11
| ~ spl0_18
| spl0_32 ),
inference(avatar_contradiction_clause,[],[f6127]) ).
fof(f9488,plain,
( frontsegP(cons(sk9,sk3),sk3)
| ssList(sk3)
| ssList(sk3)
| ~ spl0_5
| ~ spl0_17 ),
inference(superposition,[],[f1578,f3973]) ).
fof(f9491,plain,
( frontsegP(cons(sk9,sk3),sk3)
| ssList(sk3)
| ~ spl0_5
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f9488]) ).
fof(f9502,plain,
( frontsegP(cons(sk9,sk3),sk3)
| ~ spl0_5
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f9491,f436]) ).
fof(f9740,plain,
( ~ frontsegP(sk3,cons(sk9,sk3))
| ssList(sk3)
| ssList(cons(sk9,sk3))
| sk3 = cons(sk9,sk3)
| ~ spl0_5
| ~ spl0_17 ),
inference(resolution,[],[f9502,f379]) ).
fof(f9741,plain,
( ~ frontsegP(sk3,cons(sk9,sk3))
| ssList(sk3)
| sk3 = cons(sk9,sk3)
| ~ spl0_5
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f9740,f666]) ).
fof(f9746,plain,
( ~ frontsegP(sk3,cons(sk9,sk3))
| ssList(sk3)
| ~ spl0_5
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f9741,f683]) ).
fof(f9751,plain,
( ~ frontsegP(sk3,cons(sk9,sk3))
| ~ spl0_5
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f9746,f436]) ).
fof(f13318,plain,
( frontsegP(sk7,cons(hd(sk7),nil))
| ssList(tl(sk7))
| spl0_11
| ~ spl0_17
| ~ spl0_29 ),
inference(superposition,[],[f3350,f886]) ).
fof(f19412,plain,
( frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(sk8)
| ssList(cons(sk6,nil)) ),
inference(superposition,[],[f1762,f233]) ).
fof(f19420,plain,
( frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil)) ),
inference(forward_subsumption_resolution,[],[f19412,f443]) ).
fof(f59745,plain,
( memberP(sk3,sk6)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ssList(nil)
| ssList(sk8)
| ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_17 ),
inference(superposition,[],[f3544,f233]) ).
fof(f59747,plain,
( memberP(sk3,sk6)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ssList(sk8)
| ssList(app(sk7,cons(sk5,nil)))
| spl0_11
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f59745,f515]) ).
fof(f59791,plain,
( memberP(sk3,sk6)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ssList(app(sk7,cons(sk5,nil)))
| spl0_11
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f59747,f443]) ).
fof(f59799,plain,
( memberP(sk3,sk5)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ssList(app(sk7,cons(sk5,nil)))
| spl0_11
| ~ spl0_17
| ~ spl0_19 ),
inference(forward_demodulation,[],[f59791,f772]) ).
fof(f59802,plain,
( ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| memberP(sk3,sk5)
| ssList(app(sk7,cons(sk5,nil)))
| spl0_11
| ~ spl0_17
| ~ spl0_19 ),
inference(forward_demodulation,[],[f59799,f772]) ).
fof(f60144,definition,
( spl0_1267
<=> sk9 = hd(sk7) ),
introduced(definition,[new_symbols(definition,[spl0_1267])],[avatar_definition]) ).
fof(f60146,plain,
( sk9 = hd(sk7)
| ~ spl0_1267 ),
inference(avatar_component_clause,[],[f60144]) ).
fof(f60148,definition,
( spl0_1268
<=> sk3 = sk7 ),
introduced(definition,[new_symbols(definition,[spl0_1268])],[avatar_definition]) ).
fof(f60149,plain,
( sk3 = sk7
| ~ spl0_1268 ),
inference(avatar_component_clause,[],[f60148]) ).
fof(f60239,definition,
( spl0_1288
<=> frontsegP(sk3,sk7) ),
introduced(definition,[new_symbols(definition,[spl0_1288])],[avatar_definition]) ).
fof(f60240,plain,
( frontsegP(sk3,sk7)
| ~ spl0_1288 ),
inference(avatar_component_clause,[],[f60239]) ).
fof(f60260,definition,
( spl0_1293
<=> frontsegP(sk7,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_1293])],[avatar_definition]) ).
fof(f60400,definition,
( spl0_1314
<=> frontsegP(sk7,cons(hd(sk7),nil)) ),
introduced(definition,[new_symbols(definition,[spl0_1314])],[avatar_definition]) ).
fof(f60402,plain,
( frontsegP(sk7,cons(hd(sk7),nil))
| ~ spl0_1314 ),
inference(avatar_component_clause,[],[f60400]) ).
fof(f60403,plain,
( spl0_50
| spl0_1314
| spl0_11
| ~ spl0_17
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f13318,f884,f542,f514,f60400,f1175]) ).
fof(f60605,plain,
( ssList(cons(sk5,nil))
| frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_19 ),
inference(forward_demodulation,[],[f19420,f772]) ).
fof(f60967,definition,
( spl0_1396
<=> ssList(app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_1396])],[avatar_definition]) ).
fof(f60969,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_1396 ),
inference(avatar_component_clause,[],[f60967]) ).
fof(f60971,definition,
( spl0_1397
<=> memberP(sk3,sk5) ),
introduced(definition,[new_symbols(definition,[spl0_1397])],[avatar_definition]) ).
fof(f60973,plain,
( memberP(sk3,sk5)
| ~ spl0_1397 ),
inference(avatar_component_clause,[],[f60971]) ).
fof(f60974,plain,
( spl0_1396
| spl0_1397
| spl0_37
| spl0_11
| ~ spl0_17
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f59802,f770,f542,f514,f1008,f60971,f60967]) ).
fof(f61098,plain,
( frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_19
| spl0_45 ),
inference(forward_subsumption_resolution,[],[f60605,f1539]) ).
fof(f61210,definition,
( spl0_1410
<=> frontsegP(sk3,app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_1410])],[avatar_definition]) ).
fof(f61212,plain,
( frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ~ spl0_1410 ),
inference(avatar_component_clause,[],[f61210]) ).
fof(f61213,plain,
( spl0_1396
| spl0_1410
| ~ spl0_19
| spl0_45 ),
inference(avatar_split_clause,[],[f61098,f1105,f770,f61210,f60967]) ).
fof(f62201,plain,
( hd(sk7) = skaf83(sk7)
| ~ spl0_17
| ~ spl0_38 ),
inference(superposition,[],[f729,f1015]) ).
fof(f62231,plain,
( ~ frontsegP(sk3,sk7)
| ssList(skaf82(sk7))
| sk9 = skaf83(sk7)
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_38 ),
inference(superposition,[],[f3401,f1015]) ).
fof(f62536,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk5,nil))
| ~ spl0_37 ),
inference(resolution,[],[f1010,f335]) ).
fof(f62537,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_19
| ~ spl0_37
| spl0_45 ),
inference(forward_subsumption_resolution,[],[f62536,f1539]) ).
fof(f62538,plain,
( spl0_1396
| ~ spl0_19
| ~ spl0_37
| spl0_45 ),
inference(avatar_split_clause,[],[f62537,f1105,f1008,f770,f60967]) ).
fof(f71627,plain,
( ssList(sk7)
| ssList(cons(sk5,nil))
| ~ spl0_1396 ),
inference(resolution,[],[f60969,f335]) ).
fof(f71628,plain,
( ssList(cons(sk5,nil))
| ~ spl0_1396 ),
inference(forward_subsumption_resolution,[],[f71627,f442]) ).
fof(f71629,plain,
( $false
| ~ spl0_19
| spl0_45
| ~ spl0_1396 ),
inference(forward_subsumption_resolution,[],[f71628,f1539]) ).
fof(f71630,plain,
( ~ spl0_19
| spl0_45
| ~ spl0_1396 ),
inference(avatar_contradiction_clause,[],[f71629]) ).
fof(f72339,plain,
( sk5 = sk9
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_1397 ),
inference(resolution,[],[f60973,f3336]) ).
fof(f72442,plain,
( frontsegP(sk3,app(app(nil,cons(sk9,nil)),cons(sk9,nil)))
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_82
| ~ spl0_1397 ),
inference(superposition,[],[f2729,f72339]) ).
fof(f72526,plain,
( frontsegP(sk3,app(app(nil,sk3),sk3))
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_82
| ~ spl0_1397 ),
inference(forward_demodulation,[],[f72442,f481]) ).
fof(f72543,plain,
( frontsegP(sk3,app(sk3,sk3))
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_82
| ~ spl0_1397 ),
inference(forward_demodulation,[],[f72526,f634]) ).
fof(f72555,plain,
( frontsegP(sk3,cons(sk9,sk3))
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_82
| ~ spl0_1397 ),
inference(forward_demodulation,[],[f72543,f3973]) ).
fof(f72557,plain,
( $false
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_82
| ~ spl0_1397 ),
inference(forward_subsumption_resolution,[],[f72555,f9751]) ).
fof(f72558,plain,
( ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_82
| ~ spl0_1397 ),
inference(avatar_contradiction_clause,[],[f72557]) ).
fof(f80787,plain,
( frontsegP(sk3,app(sk7,cons(sk9,nil)))
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_1397
| ~ spl0_1410 ),
inference(forward_demodulation,[],[f61212,f72339]) ).
fof(f80788,plain,
( frontsegP(sk3,app(sk7,sk3))
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_1397
| ~ spl0_1410 ),
inference(forward_demodulation,[],[f80787,f481]) ).
fof(f80789,plain,
( ssList(sk7)
| ssList(sk3)
| frontsegP(sk3,sk7)
| ssList(sk3)
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_1397
| ~ spl0_1410 ),
inference(resolution,[],[f80788,f1896]) ).
fof(f80795,plain,
( ssList(sk7)
| ssList(sk3)
| frontsegP(sk3,sk7)
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_1397
| ~ spl0_1410 ),
inference(duplicate_literal_removal,[],[f80789]) ).
fof(f80801,plain,
( ssList(sk3)
| frontsegP(sk3,sk7)
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_1397
| ~ spl0_1410 ),
inference(forward_subsumption_resolution,[],[f80795,f442]) ).
fof(f80807,plain,
( frontsegP(sk3,sk7)
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_1397
| ~ spl0_1410 ),
inference(forward_subsumption_resolution,[],[f80801,f436]) ).
fof(f80830,plain,
( ~ frontsegP(sk3,sk7)
| sk9 = skaf83(sk7)
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f62231,f264]) ).
fof(f80832,plain,
( spl0_1288
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_1397
| ~ spl0_1410 ),
inference(avatar_split_clause,[],[f80807,f61210,f60971,f542,f514,f479,f60239]) ).
fof(f80838,plain,
( sk9 = hd(sk7)
| ~ frontsegP(sk3,sk7)
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_38 ),
inference(forward_demodulation,[],[f80830,f62201]) ).
fof(f80843,plain,
( ~ spl0_1288
| spl0_1267
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f80838,f1013,f542,f514,f479,f60144,f60239]) ).
fof(f80891,plain,
( ~ frontsegP(sk7,sk3)
| ssList(sk7)
| ssList(sk3)
| sk3 = sk7
| ~ spl0_1288 ),
inference(resolution,[],[f60240,f379]) ).
fof(f80920,plain,
( frontsegP(sk7,cons(sk9,nil))
| ~ spl0_1267
| ~ spl0_1314 ),
inference(superposition,[],[f60402,f60146]) ).
fof(f80933,plain,
( frontsegP(sk7,sk3)
| ~ spl0_5
| ~ spl0_1267
| ~ spl0_1314 ),
inference(forward_demodulation,[],[f80920,f481]) ).
fof(f80950,plain,
( ~ frontsegP(sk7,sk3)
| ssList(sk3)
| sk3 = sk7
| ~ spl0_1288 ),
inference(forward_subsumption_resolution,[],[f80891,f442]) ).
fof(f80951,plain,
( spl0_1293
| ~ spl0_5
| ~ spl0_1267
| ~ spl0_1314 ),
inference(avatar_split_clause,[],[f80933,f60400,f60144,f479,f60260]) ).
fof(f80957,plain,
( ~ frontsegP(sk7,sk3)
| sk3 = sk7
| ~ spl0_1288 ),
inference(forward_subsumption_resolution,[],[f80950,f436]) ).
fof(f80986,plain,
( spl0_1268
| ~ spl0_1293
| ~ spl0_1288 ),
inference(avatar_split_clause,[],[f80957,f60239,f60260,f60148]) ).
fof(f81199,plain,
( frontsegP(sk3,app(sk3,sk3))
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_1268
| ~ spl0_1397
| ~ spl0_1410 ),
inference(superposition,[],[f80788,f60149]) ).
fof(f81200,plain,
( frontsegP(sk3,cons(sk9,sk3))
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_1268
| ~ spl0_1397
| ~ spl0_1410 ),
inference(forward_demodulation,[],[f81199,f3973]) ).
fof(f81222,plain,
( $false
| ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_1268
| ~ spl0_1397
| ~ spl0_1410 ),
inference(forward_subsumption_resolution,[],[f81200,f9751]) ).
fof(f81223,plain,
( ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_1268
| ~ spl0_1397
| ~ spl0_1410 ),
inference(avatar_contradiction_clause,[],[f81222]) ).
fof(f81245,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| ~ spl0_1
| ~ spl0_19
| spl0_78 ),
inference(forward_subsumption_resolution,[],[f2633,f2643]) ).
fof(f82809,plain,
( ssList(cons(sk5,nil))
| ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_1
| ~ spl0_19
| spl0_78 ),
inference(forward_demodulation,[],[f81245,f772]) ).
fof(f83138,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_1
| ~ spl0_19
| spl0_45
| spl0_78 ),
inference(forward_subsumption_resolution,[],[f82809,f1539]) ).
fof(f83422,plain,
( spl0_1396
| ~ spl0_1
| ~ spl0_19
| spl0_45
| spl0_78 ),
inference(avatar_split_clause,[],[f83138,f2642,f1105,f770,f462,f60967]) ).
cnf(s4,plain,
( spl0_1
| spl0_5 ),
inference(sat_conversion,[],[f482]) ).
cnf(s21,plain,
( spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f547]) ).
cnf(s24,plain,
~ spl0_11,
inference(sat_conversion,[],[f550]) ).
cnf(s30,plain,
( spl0_28
| spl0_29 ),
inference(sat_conversion,[],[f887]) ).
cnf(s37,plain,
( spl0_28
| spl0_38 ),
inference(sat_conversion,[],[f1016]) ).
cnf(s63,plain,
( spl0_11
| ~ spl0_45 ),
inference(sat_conversion,[],[f1160]) ).
cnf(s74,plain,
spl0_19,
inference(sat_conversion,[],[f1312]) ).
cnf(s83,plain,
( spl0_28
| ~ spl0_50 ),
inference(sat_conversion,[],[f1454]) ).
cnf(s110,plain,
( spl0_11
| ~ spl0_72 ),
inference(sat_conversion,[],[f2481]) ).
cnf(s112,plain,
( ~ spl0_19
| spl0_45
| spl0_72
| ~ spl0_78 ),
inference(sat_conversion,[],[f2676]) ).
cnf(s122,plain,
( ~ spl0_19
| ~ spl0_28
| spl0_32
| spl0_82 ),
inference(sat_conversion,[],[f2730]) ).
cnf(s156,plain,
( ~ spl0_19
| ~ spl0_32
| spl0_45
| spl0_46 ),
inference(sat_conversion,[],[f4021]) ).
cnf(s222,plain,
( spl0_11
| ~ spl0_19
| spl0_45
| ~ spl0_46 ),
inference(sat_conversion,[],[f4324]) ).
cnf(s333,plain,
( spl0_11
| ~ spl0_18
| spl0_32 ),
inference(sat_conversion,[],[f6128]) ).
cnf(s1812,plain,
( spl0_11
| ~ spl0_17
| ~ spl0_29
| spl0_50
| spl0_1314 ),
inference(sat_conversion,[],[f60403]) ).
cnf(s1902,plain,
( spl0_11
| ~ spl0_17
| ~ spl0_19
| spl0_37
| spl0_1396
| spl0_1397 ),
inference(sat_conversion,[],[f60974]) ).
cnf(s1968,plain,
( ~ spl0_19
| spl0_45
| spl0_1396
| spl0_1410 ),
inference(sat_conversion,[],[f61213]) ).
cnf(s2135,plain,
( ~ spl0_19
| ~ spl0_37
| spl0_45
| spl0_1396 ),
inference(sat_conversion,[],[f62538]) ).
cnf(s2250,plain,
( ~ spl0_19
| spl0_45
| ~ spl0_1396 ),
inference(sat_conversion,[],[f71630]) ).
cnf(s2268,plain,
( ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_82
| ~ spl0_1397 ),
inference(sat_conversion,[],[f72558]) ).
cnf(s2934,plain,
( ~ spl0_5
| spl0_11
| ~ spl0_17
| spl0_1288
| ~ spl0_1397
| ~ spl0_1410 ),
inference(sat_conversion,[],[f80832]) ).
cnf(s2938,plain,
( ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_38
| spl0_1267
| ~ spl0_1288 ),
inference(sat_conversion,[],[f80843]) ).
cnf(s2953,plain,
( ~ spl0_5
| ~ spl0_1267
| spl0_1293
| ~ spl0_1314 ),
inference(sat_conversion,[],[f80951]) ).
cnf(s2959,plain,
( spl0_1268
| ~ spl0_1288
| ~ spl0_1293 ),
inference(sat_conversion,[],[f80986]) ).
cnf(s2995,plain,
( ~ spl0_5
| spl0_11
| ~ spl0_17
| ~ spl0_1268
| ~ spl0_1397
| ~ spl0_1410 ),
inference(sat_conversion,[],[f81223]) ).
cnf(s3459,plain,
( ~ spl0_1
| ~ spl0_19
| spl0_45
| spl0_78
| spl0_1396 ),
inference(sat_conversion,[],[f83422]) ).
cnf(s3500,plain,
~ spl0_72,
inference(rat,[],[s110,s24]) ).
cnf(s3501,plain,
~ spl0_45,
inference(rat,[],[s63,s24]) ).
cnf(s3502,plain,
~ spl0_1396,
inference(rat,[],[s2250,s74,s3501]) ).
cnf(s3505,plain,
~ spl0_78,
inference(rat,[],[s112,s3500,s74,s3501]) ).
cnf(s3510,plain,
~ spl0_1,
inference(rat,[],[s3459,s3502,s3505,s74,s3501]) ).
cnf(s3511,plain,
~ spl0_37,
inference(rat,[],[s2135,s3502,s74,s3501]) ).
cnf(s3513,plain,
~ spl0_46,
inference(rat,[],[s222,s24,s74,s3501]) ).
cnf(s3516,plain,
~ spl0_32,
inference(rat,[],[s156,s3513,s74,s3501]) ).
cnf(s3521,plain,
spl0_1410,
inference(rat,[],[s1968,s3501,s74,s3502]) ).
cnf(s3545,plain,
~ spl0_18,
inference(rat,[],[s333,s24,s3516]) ).
cnf(s3585,plain,
spl0_17,
inference(rat,[],[s21,s3545]) ).
cnf(s3591,plain,
spl0_1397,
inference(rat,[],[s1902,s3511,s3502,s24,s74,s3585]) ).
cnf(s3748,plain,
spl0_5,
inference(rat,[],[s4,s3510]) ).
cnf(s3749,plain,
~ spl0_1268,
inference(rat,[],[s2995,s3521,s3591,s3585,s24,s3748]) ).
cnf(s3750,plain,
spl0_1288,
inference(rat,[],[s2934,s3521,s3591,s3585,s24,s3748]) ).
cnf(s3754,plain,
~ spl0_82,
inference(rat,[],[s2268,s3591,s3585,s24,s3748]) ).
cnf(s3764,plain,
~ spl0_1293,
inference(rat,[],[s2959,s3749,s3750]) ).
cnf(s3765,plain,
~ spl0_28,
inference(rat,[],[s122,s3516,s74,s3754]) ).
cnf(s3934,plain,
~ spl0_50,
inference(rat,[],[s83,s3765]) ).
cnf(s3936,plain,
spl0_38,
inference(rat,[],[s37,s3765]) ).
cnf(s3937,plain,
spl0_29,
inference(rat,[],[s30,s3765]) ).
cnf(s3968,plain,
spl0_1267,
inference(rat,[],[s2938,s3750,s3748,s3585,s24,s3936]) ).
cnf(s4000,plain,
spl0_1314,
inference(rat,[],[s1812,s3934,s3585,s24,s3937]) ).
cnf(s4002,plain,
$false,
inference(rat,[],[s2953,s3764,s3748,s4000,s3968]) ).
fof(f83427,plain,
$false,
inference(avatar_sat_refutation,[],[s4002]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC173-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.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 28 08:22:32 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.39 Running first-order model finding
% 0.10/0.39 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
% 10.33/2.51 % (208099)Will run a generic schedule for satisfiability detection.
% 10.33/2.51 % (208106)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3172148461:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 10.33/2.51 % (208104)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3324717450_2999 on theBenchmark for (2999ds/0Mi)
% 10.33/2.51 % (208107)dis+10_1_sil=32000:sp=arity:random_seed=3155130833:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 10.33/2.51 % (208108)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1652894613:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 10.33/2.51 % (208109)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1979873489:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 10.33/2.51 % (208110)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1326091477:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 10.33/2.51 % (208105)% WARNING: option uhcvi not known.
% 10.33/2.51 % (208105)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4097830541:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 10.33/2.51 % TRYING [1]
% 10.33/2.51 % TRYING [2]
% 10.33/2.51 % TRYING [3]
% 10.33/2.51 % TRYING [4]
% 10.33/2.51 % (208107)Instruction limit reached!
% 10.33/2.51 % (208107)------------------------------
% 10.33/2.51 % (208107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.33/2.51 % (208107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.51 % (208107)CaDiCaL version: 2.1.3
% 10.33/2.51 % (208107)Termination reason: Instruction limit
% 10.33/2.51 % (208107)Termination phase: Saturation
% 10.33/2.51 % (208107)Time elapsed: 0.059 s
% 10.33/2.51 % (208107)Peak memory usage: 13 MB
% 10.33/2.51 % (208107)Instructions burned: 103 (million)
% 10.33/2.51 % (208108)Instruction limit reached!
% 10.33/2.51 % (208108)------------------------------
% 10.33/2.51 % (208108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.33/2.51 % (208108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.51 % (208108)CaDiCaL version: 2.1.3
% 10.33/2.51 % (208108)Termination reason: Instruction limit
% 10.33/2.51 % (208108)Termination phase: Saturation
% 10.33/2.51 % (208108)Time elapsed: 0.059 s
% 10.33/2.51 % (208108)Peak memory usage: 13 MB
% 10.33/2.51 % (208108)Instructions burned: 118 (million)
% 10.33/2.51 % (208109)Instruction limit reached!
% 10.33/2.51 % (208109)------------------------------
% 10.33/2.51 % (208109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.33/2.51 % (208109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.51 % (208109)CaDiCaL version: 2.1.3
% 10.33/2.51 % (208109)Termination reason: Instruction limit
% 10.33/2.51 % (208109)Termination phase: Saturation
% 10.33/2.51 % (208109)Time elapsed: 0.067 s
% 10.33/2.51 % (208109)Peak memory usage: 14 MB
% 10.33/2.51 % (208109)Instructions burned: 132 (million)
% 10.33/2.51 % (208118)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2363214453:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 10.33/2.51 % (208119)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3152619688:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 10.33/2.51 % (208120)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=3193710725:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 10.33/2.51 % TRYING [1]
% 10.33/2.51 % TRYING [2]
% 10.33/2.51 % TRYING [3]
% 10.33/2.51 % (208110)Instruction limit reached!
% 10.33/2.51 % (208110)------------------------------
% 10.33/2.51 % (208110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.33/2.51 % (208110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.51 % (208110)CaDiCaL version: 2.1.3
% 10.33/2.51 % (208110)Termination reason: Instruction limit
% 10.33/2.51 % (208110)Termination phase: Saturation
% 10.33/2.51 % (208110)Time elapsed: 0.099 s
% 10.33/2.51 % (208110)Peak memory usage: 14 MB
% 10.33/2.51 % (208110)Instructions burned: 163 (million)
% 10.33/2.51 % TRYING [5]
% 10.33/2.51 % TRYING [4]
% 10.33/2.51 % (208124)ott-21_1_sil=16000:fs=off:random_seed=2971560802:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 10.33/2.51 % (208119)Instruction limit reached!
% 10.33/2.51 % (208119)------------------------------
% 10.33/2.51 % (208119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.33/2.51 % (208119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.51 % (208119)CaDiCaL version: 2.1.3
% 10.33/2.51 % (208119)Termination reason: Instruction limit
% 10.33/2.51 % (208119)Termination phase: Saturation
% 10.33/2.51 % (208119)Time elapsed: 0.068 s
% 10.33/2.51 % (208119)Peak memory usage: 13 MB
% 10.33/2.51 % (208119)Instructions burned: 131 (million)
% 10.33/2.51 % (208126)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1668025776:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 10.33/2.51 % TRYING [5]
% 10.33/2.51 % (208124)Instruction limit reached!
% 10.33/2.51 % (208124)------------------------------
% 10.33/2.51 % (208124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.33/2.51 % (208124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.51 % (208124)CaDiCaL version: 2.1.3
% 10.33/2.51 % (208124)Termination reason: Instruction limit
% 10.33/2.51 % (208124)Termination phase: Saturation
% 10.33/2.51 % (208124)Time elapsed: 0.088 s
% 10.33/2.51 % (208124)Peak memory usage: 13 MB
% 10.33/2.51 % (208124)Instructions burned: 182 (million)
% 10.33/2.51 % (208128)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4263725352:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 10.33/2.51 % TRYING [1]
% 10.33/2.51 % TRYING [2]
% 10.33/2.51 % TRYING [3]
% 10.33/2.51 % TRYING [6]
% 10.33/2.51 % TRYING [4]
% 10.33/2.51 % TRYING [6]
% 10.33/2.51 % (208118)Instruction limit reached!
% 10.33/2.51 % (208118)------------------------------
% 10.33/2.51 % (208118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.33/2.51 % (208118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.51 % (208118)CaDiCaL version: 2.1.3
% 10.33/2.51 % (208118)Termination reason: Instruction limit
% 10.33/2.51 % (208118)Termination phase: Finite model building constraint generation
% 10.33/2.51 % (208118)Time elapsed: 0.273 s
% 10.33/2.51 % (208118)Peak memory usage: 34 MB
% 10.33/2.51 % (208118)Instructions burned: 716 (million)
% 10.33/2.51 % (208130)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1131365709:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 10.33/2.51 % TRYING [5]
% 10.33/2.51 % (208120)Instruction limit reached!
% 10.33/2.51 % (208120)------------------------------
% 10.33/2.51 % (208120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.33/2.51 % (208120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.51 % (208120)CaDiCaL version: 2.1.3
% 10.33/2.51 % (208120)Termination reason: Instruction limit
% 10.33/2.51 % (208120)Termination phase: Saturation
% 10.33/2.51 % (208120)Time elapsed: 0.382 s
% 10.33/2.51 % (208120)Peak memory usage: 21 MB
% 10.33/2.51 % (208120)Instructions burned: 685 (million)
% 10.33/2.51 % (208126)Instruction limit reached!
% 10.33/2.51 % (208126)------------------------------
% 10.33/2.51 % (208126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.33/2.51 % (208126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.51 % (208126)CaDiCaL version: 2.1.3
% 10.33/2.51 % (208126)Termination reason: Instruction limit
% 10.33/2.51 % (208126)Termination phase: Saturation
% 10.33/2.51 % (208126)Time elapsed: 0.317 s
% 10.33/2.51 % (208126)Peak memory usage: 14 MB
% 10.33/2.51 % (208126)Instructions burned: 478 (million)
% 10.33/2.51 % (208132)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1124510033:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 10.33/2.51 % (208133)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=1042985418: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)
% 10.33/2.51 % (208128)Instruction limit reached!
% 10.33/2.51 % (208128)------------------------------
% 10.33/2.51 % (208128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.33/2.51 % (208128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.51 % (208128)CaDiCaL version: 2.1.3
% 10.33/2.51 % (208128)Termination reason: Instruction limit
% 10.33/2.51 % (208128)Termination phase: Finite model building SAT solving
% 10.33/2.51 % (208128)Time elapsed: 0.342 s
% 10.33/2.51 % (208128)Peak memory usage: 22 MB
% 10.33/2.51 % (208128)Instructions burned: 866 (million)
% 10.33/2.51 % TRYING [14]
% 10.33/2.51 % (208136)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2590480537:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 10.33/2.51 % TRYING [7]
% 10.33/2.51 % (208132)Instruction limit reached!
% 10.33/2.51 % (208132)------------------------------
% 10.33/2.51 % (208132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.33/2.51 % (208132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.51 % (208132)CaDiCaL version: 2.1.3
% 10.33/2.51 % (208132)Termination reason: Instruction limit
% 10.33/2.51 % (208132)Termination phase: Finite model building constraint generation
% 10.33/2.51 % (208132)Time elapsed: 0.328 s
% 10.33/2.51 % (208132)Peak memory usage: 73 MB
% 10.33/2.51 % (208132)Instructions burned: 891 (million)
% 10.33/2.51 % (208138)fmb+10_1_sil=64000:random_seed=360043374:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 10.33/2.51 % TRYING [1]
% 10.33/2.51 % TRYING [2]
% 10.33/2.51 % TRYING [3]
% 10.33/2.51 % (208133)Instruction limit reached!
% 10.33/2.51 % (208133)------------------------------
% 10.33/2.51 % (208133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.33/2.51 % (208133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.51 % (208133)CaDiCaL version: 2.1.3
% 10.33/2.51 % (208133)Termination reason: Instruction limit
% 10.33/2.51 % (208133)Termination phase: Saturation
% 10.33/2.51 % (208133)Time elapsed: 0.403 s
% 10.33/2.51 % (208133)Peak memory usage: 19 MB
% 10.33/2.51 % (208133)Instructions burned: 694 (million)
% 10.33/2.51 % TRYING [4]
% 10.33/2.51 % (208140)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3010214212:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 10.33/2.51 % TRYING [20]
% 10.33/2.51 % (208130)Instruction limit reached!
% 10.33/2.51 % (208130)------------------------------
% 10.33/2.51 % (208130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.33/2.51 % (208130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.51 % (208130)CaDiCaL version: 2.1.3
% 10.33/2.51 % (208130)Termination reason: Instruction limit
% 10.33/2.51 % (208130)Termination phase: Saturation
% 10.33/2.51 % (208130)Time elapsed: 0.658 s
% 10.33/2.51 % (208130)Peak memory usage: 25 MB
% 10.33/2.51 % (208130)Instructions burned: 1179 (million)
% 10.33/2.51 % (208142)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2020222658:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 10.33/2.51 % TRYING [8]
% 10.33/2.51 % (208136)Instruction limit reached!
% 10.33/2.51 % (208136)------------------------------
% 10.33/2.51 % (208136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.33/2.51 % (208136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.51 % (208136)CaDiCaL version: 2.1.3
% 10.33/2.51 % (208136)Termination reason: Instruction limit
% 10.33/2.51 % (208136)Termination phase: Saturation
% 10.33/2.51 % (208136)Time elapsed: 0.477 s
% 10.33/2.51 % (208136)Peak memory usage: 20 MB
% 10.33/2.51 % (208136)Instructions burned: 880 (million)
% 10.33/2.51 % TRYING [5]
% 10.33/2.51 % (208144)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2829112861:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 10.33/2.51 % (208142)Instruction limit reached!
% 10.33/2.51 % (208142)------------------------------
% 10.33/2.51 % (208142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.33/2.51 % (208142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.51 % (208142)CaDiCaL version: 2.1.3
% 10.33/2.51 % (208142)Termination reason: Instruction limit
% 10.33/2.51 % (208142)Termination phase: Finite model building constraint generation
% 10.33/2.51 % (208142)Time elapsed: 0.332 s
% 10.33/2.51 % (208142)Peak memory usage: 79 MB
% 10.33/2.51 % (208142)Instructions burned: 921 (million)
% 10.33/2.51 % (208146)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=227268704:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 10.33/2.51 % TRYING [6]
% 10.33/2.51 % (208105) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-208099-208105"...
% 10.33/2.51 % (208105)...printing done.
% 10.33/2.51 % (208105)Refutation found. Thanks to Tanya!
% 10.33/2.51 % SZS status Unsatisfiable for theBenchmark
% 10.33/2.51 % SZS output start Proof for theBenchmark
% See solution above
% 10.33/2.52 % (208105)------------------------------
% 10.33/2.52 % (208105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.33/2.52 % (208105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.52 % (208105)CaDiCaL version: 2.1.3
% 10.33/2.52 % (208105)Termination reason: Refutation
% 10.33/2.52 % (208105)Time elapsed: 2.031 s
% 10.33/2.52 % (208105)Peak memory usage: 48 MB
% 10.33/2.52 % (208105)Instructions burned: 3877 (million)
% 10.33/2.52 % (208099)Success in time 2.117 s
% 10.33/2.52 % Vampire exiting
%------------------------------------------------------------------------------