%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC183-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n019.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:00 PM UTC 2026
% Result : Unsatisfiable 5.22s 1.24s
% Output : Refutation 5.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 73
% Syntax : Number of formulae : 372 ( 60 unt; 32 def)
% Number of atoms : 1130 ( 132 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 1213 ( 455 ~; 726 |; 0 &)
% ( 32 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 41 ( 39 usr; 33 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 9 con; 0-2 aty)
% Number of variables : 214 ( 0 sgn 214 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f11,axiom,
~ singletonP(nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause11) ).
fof(f52,axiom,
! [X0,X1] : ssList(skaf43(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause52) ).
fof(f53,axiom,
! [X0,X1] : ssList(skaf42(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause53) ).
fof(f60,axiom,
! [X0] :
( ~ ssList(X0)
| frontsegP(X0,nil) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause60) ).
fof(f71,axiom,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause71) ).
fof(f72,axiom,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f73,axiom,
! [X0] :
( ~ ssList(X0)
| app(X0,nil) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause73) ).
fof(f74,axiom,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause74) ).
fof(f75,axiom,
! [X0] :
( ~ ssList(X0)
| ssList(tl(X0))
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause75) ).
fof(f76,axiom,
! [X0] :
( ~ ssList(X0)
| ssItem(hd(X0))
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause76) ).
fof(f80,axiom,
! [X0] :
( ~ segmentP(nil,X0)
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause80) ).
fof(f85,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ssList(app(X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ssList(cons(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause86) ).
fof(f100,axiom,
! [X0,X1] :
( cons(X0,X1) != X1
| ~ ssItem(X0)
| ~ ssList(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause99) ).
fof(f107,axiom,
! [X0] :
( ~ ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause104) ).
fof(f119,axiom,
! [X0,X1] :
( cons(X0,nil) != X1
| ~ ssItem(X0)
| ~ ssList(X1)
| singletonP(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause116) ).
fof(f125,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| app(cons(X0,nil),X1) = cons(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause120) ).
fof(f126,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(reorient_equations,[],[f125]) ).
fof(f138,axiom,
! [X0,X1] :
( ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause129) ).
fof(f139,plain,
! [X0,X1] :
( ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X0 = X1 ),
inference(reorient_equations,[],[f138]) ).
fof(f148,axiom,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| frontsegP(app(X0,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause137) ).
fof(f152,axiom,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssItem(X1)
| memberP(app(X2,X0),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause141) ).
fof(f155,axiom,
! [X2,X0,X1] :
( app(X0,X1) != X2
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| frontsegP(X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause144) ).
fof(f162,axiom,
! [X2,X0,X1] :
( app(X0,X1) != app(X0,X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause150) ).
fof(f173,axiom,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X2 = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause161) ).
fof(f174,plain,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X0 = X2 ),
inference(reorient_equations,[],[f173]) ).
fof(f182,axiom,
! [X0,X1] :
( ~ memberP(X0,X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| app(skaf42(X0,X1),cons(X1,skaf43(X1,X0))) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause169) ).
fof(f187,axiom,
! [X2,X3,X0,X1] :
( app(app(X0,X1),X2) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| segmentP(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause173) ).
fof(f190,axiom,
! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ~ ssList(X3)
| ~ ssList(X1)
| ~ ssItem(X2)
| ~ ssItem(X0)
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause176) ).
fof(f192,axiom,
! [X2,X3,X0,X1] :
( ~ frontsegP(X0,X1)
| X2 != X3
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X2)
| frontsegP(cons(X2,X0),cons(X3,X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause178) ).
fof(f193,axiom,
! [X2,X3,X0,X1,X4] :
( app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(X4)
| ~ ssList(X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(f200,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_1) ).
fof(f201,negated_conjecture,
ssList(sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_2) ).
fof(f204,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_5) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
ssList(sk6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
app(app(sk6,cons(sk5,nil)),sk7) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_10) ).
fof(f210,plain,
sk1 = app(app(sk6,cons(sk5,nil)),sk7),
inference(reorient_equations,[],[f209]) ).
fof(f211,negated_conjecture,
( memberP(sk6,sk5)
| memberP(sk7,sk5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_11) ).
fof(f213,negated_conjecture,
( ssItem(sk8)
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_13) ).
fof(f218,negated_conjecture,
( cons(sk8,nil) = sk3
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_17) ).
fof(f219,plain,
( sk3 = cons(sk8,nil)
| nil = sk3 ),
inference(reorient_equations,[],[f218]) ).
fof(f220,negated_conjecture,
( memberP(sk4,sk8)
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_18) ).
fof(f222,plain,
ssList(sk3),
inference(definition_unfolding,[],[f200,f205]) ).
fof(f223,plain,
ssList(sk4),
inference(definition_unfolding,[],[f201,f204]) ).
fof(f224,plain,
sk3 = app(app(sk6,cons(sk5,nil)),sk7),
inference(definition_unfolding,[],[f210,f205]) ).
fof(f232,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(cons(X0,nil))
| singletonP(cons(X0,nil)) ),
inference(equality_resolution,[],[f119]) ).
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(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(app(X0,X1),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(f250,plain,
~ ssList(nil),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f253,plain,
singletonP(nil),
inference(consistent_polarity_flipping,[],[f11]) ).
fof(f294,plain,
! [X0,X1] : ~ ssList(skaf43(X0,X1)),
inference(consistent_polarity_flipping,[],[f52]) ).
fof(f295,plain,
! [X0,X1] : ~ ssList(skaf42(X0,X1)),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f301,plain,
! [X0] :
( ~ frontsegP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f312,plain,
! [X0] :
( memberP(nil,X0)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f71]) ).
fof(f313,plain,
! [X0,X1] :
( ssList(X0)
| duplicatefreeP(X0)
| ~ ssItem(X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f314,plain,
! [X0] :
( ssList(X0)
| app(X0,nil) = X0 ),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f315,plain,
! [X0] :
( ssList(X0)
| app(nil,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f316,plain,
! [X0] :
( ~ ssList(tl(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f317,plain,
! [X0] :
( ~ ssItem(hd(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f321,plain,
! [X0] :
( segmentP(nil,X0)
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f326,plain,
! [X0,X1] :
( ~ ssList(app(X1,X0))
| ssList(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f327,plain,
! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f340,plain,
! [X0,X1] :
( cons(X0,X1) != X1
| ssItem(X0)
| ssList(X1) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f345,plain,
! [X0] :
( ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f357,plain,
! [X0] :
( ~ singletonP(cons(X0,nil))
| ssList(cons(X0,nil))
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f232]) ).
fof(f361,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f370,plain,
! [X0,X1] :
( frontsegP(X0,X1)
| frontsegP(X1,X0)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f378,plain,
! [X2,X0,X1] :
( ~ frontsegP(app(X0,X2),X1)
| ssList(X2)
| ssList(X1)
| ssList(X0)
| frontsegP(X0,X1) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f382,plain,
! [X2,X0,X1] :
( ~ memberP(app(X2,X0),X1)
| ssList(X0)
| ssList(X2)
| ssItem(X1)
| memberP(X0,X1) ),
inference(consistent_polarity_flipping,[],[f152]) ).
fof(f385,plain,
! [X0,X1] :
( ssList(X1)
| ssList(X0)
| ssList(app(X0,X1))
| ~ frontsegP(app(X0,X1),X0) ),
inference(consistent_polarity_flipping,[],[f236]) ).
fof(f391,plain,
! [X2,X0,X1] :
( app(X0,X1) != app(X0,X2)
| ssList(X1)
| ssList(X0)
| ssList(X2)
| X1 = X2 ),
inference(consistent_polarity_flipping,[],[f162]) ).
fof(f402,plain,
! [X2,X0,X1] :
( ~ memberP(X1,X2)
| ssList(X1)
| ssItem(X0)
| ssItem(X2)
| memberP(cons(X0,X1),X2)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f410,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(f414,plain,
! [X2,X0,X1] :
( ~ segmentP(app(app(X0,X1),X2),X1)
| ssList(X0)
| ssList(X1)
| ssList(app(app(X0,X1),X2))
| ssList(X2) ),
inference(consistent_polarity_flipping,[],[f239]) ).
fof(f417,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(f419,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(f420,plain,
! [X2,X3,X0,X1] :
( ssList(X3)
| ssList(X2)
| ssList(X0)
| ssItem(X1)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(consistent_polarity_flipping,[],[f242]) ).
fof(f427,plain,
~ ssList(sk3),
inference(consistent_polarity_flipping,[],[f222]) ).
fof(f428,plain,
~ ssList(sk4),
inference(consistent_polarity_flipping,[],[f223]) ).
fof(f431,plain,
~ ssItem(sk5),
inference(consistent_polarity_flipping,[],[f206]) ).
fof(f432,plain,
~ ssList(sk6),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f433,plain,
~ ssList(sk7),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f434,plain,
( ~ memberP(sk6,sk5)
| ~ memberP(sk7,sk5) ),
inference(consistent_polarity_flipping,[],[f211]) ).
fof(f436,plain,
( ~ ssItem(sk8)
| nil = sk3 ),
inference(consistent_polarity_flipping,[],[f213]) ).
fof(f439,plain,
( ~ memberP(sk4,sk8)
| nil = sk3 ),
inference(consistent_polarity_flipping,[],[f220]) ).
fof(f441,plain,
! [X3,X0,X1] :
( ~ frontsegP(cons(X3,X0),cons(X3,X1))
| ssList(X1)
| ssList(X0)
| ssItem(X3)
| frontsegP(X0,X1) ),
inference(duplicate_literal_removal,[],[f419]) ).
fof(f448,definition,
( spl0_1
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f450,plain,
( nil = sk3
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f456,definition,
( spl0_3
<=> memberP(sk4,sk8) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f458,plain,
( ~ memberP(sk4,sk8)
| spl0_3 ),
inference(avatar_component_clause,[],[f456]) ).
fof(f459,plain,
( spl0_1
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f439,f456,f448]) ).
fof(f461,definition,
( spl0_4
<=> sk3 = cons(sk8,nil) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f463,plain,
( sk3 = cons(sk8,nil)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f461]) ).
fof(f464,plain,
( spl0_1
| spl0_4 ),
inference(avatar_split_clause,[],[f219,f461,f448]) ).
fof(f473,definition,
( spl0_6
<=> ssItem(sk8) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f475,plain,
( ~ ssItem(sk8)
| spl0_6 ),
inference(avatar_component_clause,[],[f473]) ).
fof(f476,plain,
( spl0_1
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f436,f473,f448]) ).
fof(f479,definition,
( spl0_7
<=> memberP(sk7,sk5) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f481,plain,
( ~ memberP(sk7,sk5)
| spl0_7 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f483,definition,
( spl0_8
<=> memberP(sk6,sk5) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f485,plain,
( ~ memberP(sk6,sk5)
| spl0_8 ),
inference(avatar_component_clause,[],[f483]) ).
fof(f486,plain,
( ~ spl0_7
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f434,f483,f479]) ).
fof(f492,definition,
( spl0_10
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f493,plain,
( ~ ssList(nil)
| spl0_10 ),
inference(avatar_component_clause,[],[f492]) ).
fof(f520,definition,
( spl0_16
<=> ! [X1] : ~ ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f521,plain,
( ! [X1] : ~ ssItem(X1)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f520]) ).
fof(f523,definition,
( spl0_17
<=> ! [X0] :
( ssList(X0)
| duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f524,plain,
( ! [X0] :
( duplicatefreeP(X0)
| ssList(X0) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f525,plain,
( spl0_16
| spl0_17 ),
inference(avatar_split_clause,[],[f313,f523,f520]) ).
fof(f528,plain,
~ spl0_10,
inference(avatar_split_clause,[],[f250,f492]) ).
fof(f535,plain,
( ! [X0] : memberP(nil,X0)
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f312,f521]) ).
fof(f579,plain,
sk3 = app(sk3,nil),
inference(resolution,[],[f314,f427]) ).
fof(f611,plain,
sk3 = app(nil,sk3),
inference(resolution,[],[f315,f427]) ).
fof(f658,plain,
( ! [X0,X1] :
( cons(X0,X1) != X1
| ssList(X1) )
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f340,f521]) ).
fof(f803,plain,
( sk6 = cons(hd(sk6),tl(sk6))
| nil = sk6 ),
inference(resolution,[],[f345,f432]) ).
fof(f806,definition,
( spl0_18
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f807,plain,
( nil != sk7
| spl0_18 ),
inference(avatar_component_clause,[],[f806]) ).
fof(f808,plain,
( nil = sk7
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f806]) ).
fof(f815,definition,
( spl0_20
<=> nil = sk6 ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f816,plain,
( nil != sk6
| spl0_20 ),
inference(avatar_component_clause,[],[f815]) ).
fof(f817,plain,
( nil = sk6
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f815]) ).
fof(f819,definition,
( spl0_21
<=> sk6 = cons(hd(sk6),tl(sk6)) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f821,plain,
( sk6 = cons(hd(sk6),tl(sk6))
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f819]) ).
fof(f822,plain,
( spl0_20
| spl0_21 ),
inference(avatar_split_clause,[],[f803,f819,f815]) ).
fof(f842,plain,
( ~ memberP(nil,sk5)
| spl0_7
| ~ spl0_18 ),
inference(superposition,[],[f481,f808]) ).
fof(f853,definition,
( spl0_23
<=> sk5 = sk8 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f855,plain,
( sk5 = sk8
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f853]) ).
fof(f1213,definition,
( spl0_49
<=> ssList(app(nil,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f1215,plain,
( ssList(app(nil,cons(sk5,nil)))
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f1213]) ).
fof(f1230,definition,
( spl0_52
<=> ssList(app(sk6,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f1231,plain,
( ~ ssList(app(sk6,cons(sk5,nil)))
| spl0_52 ),
inference(avatar_component_clause,[],[f1230]) ).
fof(f1232,plain,
( ssList(app(sk6,cons(sk5,nil)))
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f1230]) ).
fof(f1466,plain,
! [X0,X1] :
( ~ frontsegP(app(X0,X1),X0)
| ssList(X0)
| ssList(X1) ),
inference(forward_subsumption_resolution,[],[f385,f326]) ).
fof(f1477,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| frontsegP(X0,app(X0,X1))
| ssList(app(X0,X1))
| ssList(X0)
| app(X0,X1) = X0 ),
inference(resolution,[],[f1466,f370]) ).
fof(f1490,plain,
( ~ frontsegP(sk3,app(sk6,cons(sk5,nil)))
| ssList(app(sk6,cons(sk5,nil)))
| ssList(sk7) ),
inference(superposition,[],[f1466,f224]) ).
fof(f1496,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| frontsegP(X0,app(X0,X1))
| ssList(app(X0,X1))
| app(X0,X1) = X0 ),
inference(duplicate_literal_removal,[],[f1477]) ).
fof(f1498,plain,
( ~ frontsegP(sk3,app(sk6,cons(sk5,nil)))
| ssList(app(sk6,cons(sk5,nil))) ),
inference(forward_subsumption_resolution,[],[f1490,f433]) ).
fof(f1499,plain,
! [X0,X1] :
( frontsegP(X0,app(X0,X1))
| ssList(X1)
| ssList(X0)
| app(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f1496,f326]) ).
fof(f1688,plain,
! [X0] :
( ~ frontsegP(sk3,X0)
| ssList(sk7)
| ssList(X0)
| ssList(app(sk6,cons(sk5,nil)))
| frontsegP(app(sk6,cons(sk5,nil)),X0) ),
inference(superposition,[],[f378,f224]) ).
fof(f1697,plain,
! [X0] :
( ~ frontsegP(sk3,X0)
| ssList(X0)
| ssList(app(sk6,cons(sk5,nil)))
| frontsegP(app(sk6,cons(sk5,nil)),X0) ),
inference(forward_subsumption_resolution,[],[f1688,f433]) ).
fof(f1793,plain,
( ssItem(sk5)
| spl0_7
| ~ spl0_18 ),
inference(resolution,[],[f842,f312]) ).
fof(f1794,plain,
( $false
| spl0_7
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1793,f431]) ).
fof(f1795,plain,
( spl0_7
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1794]) ).
fof(f1797,plain,
( ~ memberP(nil,sk5)
| spl0_8
| ~ spl0_20 ),
inference(forward_demodulation,[],[f485,f817]) ).
fof(f1825,plain,
( ssItem(sk5)
| spl0_8
| ~ spl0_20 ),
inference(resolution,[],[f1797,f312]) ).
fof(f1826,plain,
( $false
| spl0_8
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f1825,f431]) ).
fof(f1827,plain,
( spl0_8
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f1826]) ).
fof(f2009,plain,
! [X0] :
( sk3 != app(app(sk6,cons(sk5,nil)),X0)
| ssList(sk7)
| ssList(app(sk6,cons(sk5,nil)))
| ssList(X0)
| sk7 = X0 ),
inference(superposition,[],[f391,f224]) ).
fof(f2055,plain,
! [X0] :
( sk3 != app(app(sk6,cons(sk5,nil)),X0)
| ssList(app(sk6,cons(sk5,nil)))
| ssList(X0)
| sk7 = X0 ),
inference(forward_subsumption_resolution,[],[f2009,f433]) ).
fof(f2087,plain,
( ! [X0] :
( sk3 != app(app(nil,cons(sk5,nil)),X0)
| ssList(app(sk6,cons(sk5,nil)))
| ssList(X0)
| sk7 = X0 )
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2055,f817]) ).
fof(f2264,plain,
( ! [X0] :
( ~ frontsegP(cons(sk8,X0),sk3)
| ssList(nil)
| ssList(X0)
| ssItem(sk8)
| frontsegP(X0,nil) )
| ~ spl0_4 ),
inference(superposition,[],[f441,f463]) ).
fof(f2656,definition,
( spl0_80
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f2657,plain,
( ~ ssList(cons(sk5,nil))
| spl0_80 ),
inference(avatar_component_clause,[],[f2656]) ).
fof(f2658,plain,
( ssList(cons(sk5,nil))
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f2656]) ).
fof(f2717,plain,
( ~ segmentP(sk3,cons(sk5,nil))
| ssList(sk6)
| ssList(cons(sk5,nil))
| ssList(sk3)
| ssList(sk7) ),
inference(superposition,[],[f414,f224]) ).
fof(f2722,plain,
( ~ segmentP(sk3,cons(sk5,nil))
| ssList(cons(sk5,nil))
| ssList(sk3)
| ssList(sk7) ),
inference(forward_subsumption_resolution,[],[f2717,f432]) ).
fof(f2728,plain,
( ~ segmentP(sk3,cons(sk5,nil))
| ssList(cons(sk5,nil))
| ssList(sk7) ),
inference(forward_subsumption_resolution,[],[f2722,f427]) ).
fof(f2734,plain,
( ~ segmentP(sk3,cons(sk5,nil))
| ssList(cons(sk5,nil)) ),
inference(forward_subsumption_resolution,[],[f2728,f433]) ).
fof(f2739,plain,
( ~ segmentP(nil,cons(sk5,nil))
| ssList(cons(sk5,nil))
| ~ spl0_1 ),
inference(forward_demodulation,[],[f2734,f450]) ).
fof(f2745,definition,
( spl0_83
<=> segmentP(nil,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f2747,plain,
( ~ segmentP(nil,cons(sk5,nil))
| spl0_83 ),
inference(avatar_component_clause,[],[f2745]) ).
fof(f2748,plain,
( spl0_80
| ~ spl0_83
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f2739,f448,f2745,f2656]) ).
fof(f2776,plain,
( ! [X2,X3,X0,X1] :
( ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(X2)
| ssList(X0)
| ssItem(X1)
| ssList(X3) )
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f420,f524]) ).
fof(f2779,plain,
( ! [X0,X1] :
( ssList(app(app(X0,cons(sk8,X1)),sk3))
| ssList(X1)
| ssList(X0)
| ssItem(sk8)
| ssList(nil) )
| ~ spl0_4
| ~ spl0_17 ),
inference(superposition,[],[f2776,f463]) ).
fof(f2800,plain,
( ssList(cons(sk5,nil))
| nil = cons(sk5,nil)
| spl0_83 ),
inference(resolution,[],[f2747,f321]) ).
fof(f2804,definition,
( spl0_87
<=> nil = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f2806,plain,
( nil = cons(sk5,nil)
| ~ spl0_87 ),
inference(avatar_component_clause,[],[f2804]) ).
fof(f2807,plain,
( spl0_87
| spl0_80
| spl0_83 ),
inference(avatar_split_clause,[],[f2800,f2745,f2656,f2804]) ).
fof(f2820,plain,
( ~ singletonP(nil)
| ssList(nil)
| ssItem(sk5)
| ~ spl0_87 ),
inference(superposition,[],[f357,f2806]) ).
fof(f2865,plain,
( ssList(nil)
| ssItem(sk5)
| ~ spl0_87 ),
inference(forward_subsumption_resolution,[],[f2820,f253]) ).
fof(f2886,plain,
( ssItem(sk5)
| spl0_10
| ~ spl0_87 ),
inference(forward_subsumption_resolution,[],[f2865,f493]) ).
fof(f2891,plain,
( $false
| spl0_10
| ~ spl0_87 ),
inference(forward_subsumption_resolution,[],[f2886,f431]) ).
fof(f2892,plain,
( spl0_10
| ~ spl0_87 ),
inference(avatar_contradiction_clause,[],[f2891]) ).
fof(f2902,plain,
( ssList(nil)
| ssItem(sk5)
| ~ spl0_80 ),
inference(resolution,[],[f2658,f327]) ).
fof(f2903,plain,
( ssItem(sk5)
| spl0_10
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f2902,f493]) ).
fof(f2904,plain,
( $false
| spl0_10
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f2903,f431]) ).
fof(f2905,plain,
( spl0_10
| ~ spl0_80 ),
inference(avatar_contradiction_clause,[],[f2904]) ).
fof(f2910,plain,
( ! [X0] :
( ~ frontsegP(cons(sk8,X0),sk3)
| ssList(X0)
| ssItem(sk8)
| frontsegP(X0,nil) )
| ~ spl0_4
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f2264,f493]) ).
fof(f2921,plain,
( ! [X0,X1] :
( ssList(app(app(X0,cons(sk8,X1)),sk3))
| ssList(X1)
| ssList(X0)
| ssItem(sk8) )
| ~ spl0_4
| spl0_10
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2779,f493]) ).
fof(f2957,plain,
( ! [X0] :
( ssList(app(nil,cons(sk5,nil)))
| sk3 != app(app(nil,cons(sk5,nil)),X0)
| ssList(X0)
| sk7 = X0 )
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2087,f817]) ).
fof(f2971,plain,
( ! [X0] :
( ~ frontsegP(cons(sk8,X0),sk3)
| ssList(X0)
| ssItem(sk8) )
| ~ spl0_4
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f2910,f301]) ).
fof(f2977,definition,
( spl0_96
<=> sk4 = app(skaf42(sk4,sk8),cons(sk8,skaf43(sk8,sk4))) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f2979,plain,
( sk4 = app(skaf42(sk4,sk8),cons(sk8,skaf43(sk8,sk4)))
| ~ spl0_96 ),
inference(avatar_component_clause,[],[f2977]) ).
fof(f2996,definition,
( spl0_100
<=> ! [X0,X1] :
( frontsegP(sk3,cons(X0,X1))
| sk8 = X0
| ssItem(X0)
| ssList(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f2997,plain,
( ! [X0,X1] :
( frontsegP(sk3,cons(X0,X1))
| sk8 = X0
| ssItem(X0)
| ssList(X1) )
| ~ spl0_100 ),
inference(avatar_component_clause,[],[f2996]) ).
fof(f3008,definition,
( spl0_103
<=> ! [X0,X1] :
( ssList(app(app(X0,cons(sk8,X1)),sk3))
| ssList(X0)
| ssList(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f3009,plain,
( ! [X0,X1] :
( ssList(app(app(X0,cons(sk8,X1)),sk3))
| ssList(X0)
| ssList(X1) )
| ~ spl0_103 ),
inference(avatar_component_clause,[],[f3008]) ).
fof(f3073,definition,
( spl0_118
<=> ! [X0] :
( sk3 != app(app(nil,cons(sk5,nil)),X0)
| sk7 = X0
| ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f3074,plain,
( ! [X0] :
( sk3 != app(app(nil,cons(sk5,nil)),X0)
| sk7 = X0
| ssList(X0) )
| ~ spl0_118 ),
inference(avatar_component_clause,[],[f3073]) ).
fof(f3076,plain,
( spl0_118
| spl0_49
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f2957,f815,f1213,f3073]) ).
fof(f3088,definition,
( spl0_121
<=> ! [X0] :
( ~ frontsegP(cons(sk8,X0),sk3)
| ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f3089,plain,
( ! [X0] :
( ~ frontsegP(cons(sk8,X0),sk3)
| ssList(X0) )
| ~ spl0_121 ),
inference(avatar_component_clause,[],[f3088]) ).
fof(f3090,plain,
( spl0_6
| spl0_121
| ~ spl0_4
| spl0_10 ),
inference(avatar_split_clause,[],[f2971,f492,f461,f3088,f473]) ).
fof(f3127,plain,
( ! [X0] :
( ssList(X0)
| cons(sk8,X0) = app(cons(sk8,nil),X0) )
| spl0_6 ),
inference(resolution,[],[f475,f361]) ).
fof(f3130,plain,
( ! [X0] :
( ssList(X0)
| cons(sk8,X0) = app(sk3,X0) )
| ~ spl0_4
| spl0_6 ),
inference(forward_demodulation,[],[f3127,f463]) ).
fof(f3169,plain,
( ! [X2,X0,X1] :
( ~ memberP(app(X2,X0),X1)
| ssList(X0)
| ssList(X2)
| memberP(X0,X1) )
| ~ spl0_16 ),
inference(backward_subsumption_resolution,[],[f382,f521]) ).
fof(f3179,plain,
( ! [X2,X0,X1] :
( ~ memberP(X1,X2)
| ssList(X1)
| ssItem(X2)
| memberP(cons(X0,X1),X2)
| X0 = X2 )
| ~ spl0_16 ),
inference(backward_subsumption_resolution,[],[f402,f521]) ).
fof(f3214,plain,
( ! [X2,X0,X1] :
( ~ memberP(X1,X2)
| ssList(X1)
| memberP(cons(X0,X1),X2)
| X0 = X2 )
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f3179,f521]) ).
fof(f3439,plain,
( ssList(nil)
| ssList(cons(sk5,nil))
| ~ spl0_49 ),
inference(resolution,[],[f1215,f326]) ).
fof(f3440,plain,
( ssList(cons(sk5,nil))
| spl0_10
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f3439,f493]) ).
fof(f3441,plain,
( $false
| spl0_10
| ~ spl0_49
| spl0_80 ),
inference(forward_subsumption_resolution,[],[f3440,f2657]) ).
fof(f3442,plain,
( spl0_10
| ~ spl0_49
| spl0_80 ),
inference(avatar_contradiction_clause,[],[f3441]) ).
fof(f3734,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ssList(sk7)
| ssList(app(sk6,cons(sk5,nil)))
| memberP(sk7,X0) )
| ~ spl0_16 ),
inference(superposition,[],[f3169,f224]) ).
fof(f3767,plain,
( ! [X0,X1] :
( ssList(nil)
| memberP(cons(X0,nil),X1)
| X0 = X1 )
| ~ spl0_16 ),
inference(resolution,[],[f3214,f535]) ).
fof(f3770,plain,
( ! [X0,X1] :
( memberP(cons(X0,nil),X1)
| X0 = X1 )
| spl0_10
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f3767,f493]) ).
fof(f5008,definition,
( spl0_187
<=> memberP(sk3,sk5) ),
introduced(definition,[new_symbols(definition,[spl0_187])],[avatar_definition]) ).
fof(f5009,plain,
( ~ memberP(sk3,sk5)
| spl0_187 ),
inference(avatar_component_clause,[],[f5008]) ).
fof(f5010,plain,
( memberP(sk3,sk5)
| ~ spl0_187 ),
inference(avatar_component_clause,[],[f5008]) ).
fof(f5340,plain,
( cons(sk8,sk3) = app(sk3,sk3)
| ~ spl0_4
| spl0_6 ),
inference(resolution,[],[f3130,f427]) ).
fof(f5452,plain,
( ! [X0,X1] :
( ssList(app(app(X0,cons(sk8,X1)),sk3))
| ssList(X1)
| ssList(X0) )
| ~ spl0_4
| spl0_6
| spl0_10
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2921,f475]) ).
fof(f5462,plain,
( spl0_103
| ~ spl0_4
| spl0_6
| spl0_10
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f5452,f523,f492,f473,f461,f3008]) ).
fof(f6258,plain,
( ssItem(sk8)
| ssList(sk4)
| sk4 = app(skaf42(sk4,sk8),cons(sk8,skaf43(sk8,sk4)))
| spl0_3 ),
inference(resolution,[],[f410,f458]) ).
fof(f6270,plain,
( ssList(sk4)
| sk4 = app(skaf42(sk4,sk8),cons(sk8,skaf43(sk8,sk4)))
| spl0_3
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f6258,f475]) ).
fof(f6281,plain,
( sk4 = app(skaf42(sk4,sk8),cons(sk8,skaf43(sk8,sk4)))
| spl0_3
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f6270,f428]) ).
fof(f6285,plain,
( spl0_96
| spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f6281,f473,f456,f2977]) ).
fof(f6383,plain,
( ! [X0,X1] :
( frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| ssList(nil)
| ssItem(X0)
| ssItem(sk8)
| sk8 = X0 )
| ~ spl0_4 ),
inference(superposition,[],[f417,f463]) ).
fof(f6410,plain,
( ! [X0,X1] :
( frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| ssItem(X0)
| ssItem(sk8)
| sk8 = X0 )
| ~ spl0_4
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f6383,f493]) ).
fof(f6424,plain,
( ! [X0,X1] :
( frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| ssItem(X0)
| sk8 = X0 )
| ~ spl0_4
| spl0_6
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f6410,f475]) ).
fof(f6430,plain,
( spl0_100
| ~ spl0_4
| spl0_6
| spl0_10 ),
inference(avatar_split_clause,[],[f6424,f492,f473,f461,f2996]) ).
fof(f8339,plain,
( ssList(app(sk4,sk3))
| ssList(skaf42(sk4,sk8))
| ssList(skaf43(sk8,sk4))
| ~ spl0_96
| ~ spl0_103 ),
inference(superposition,[],[f3009,f2979]) ).
fof(f8342,plain,
( ssList(app(sk4,sk3))
| ssList(skaf43(sk8,sk4))
| ~ spl0_96
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f8339,f295]) ).
fof(f8346,plain,
( ssList(app(sk4,sk3))
| ~ spl0_96
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f8342,f294]) ).
fof(f8748,plain,
( ! [X0] :
( sk3 != app(app(nil,cons(sk8,nil)),X0)
| sk7 = X0
| ssList(X0) )
| ~ spl0_23
| ~ spl0_118 ),
inference(forward_demodulation,[],[f3074,f855]) ).
fof(f8749,plain,
( ! [X0] :
( sk3 != app(app(nil,sk3),X0)
| sk7 = X0
| ssList(X0) )
| ~ spl0_4
| ~ spl0_23
| ~ spl0_118 ),
inference(forward_demodulation,[],[f8748,f463]) ).
fof(f8750,plain,
( ! [X0] :
( sk3 != app(sk3,X0)
| sk7 = X0
| ssList(X0) )
| ~ spl0_4
| ~ spl0_23
| ~ spl0_118 ),
inference(forward_demodulation,[],[f8749,f611]) ).
fof(f8751,plain,
( sk3 != sk3
| nil = sk7
| ssList(nil)
| ~ spl0_4
| ~ spl0_23
| ~ spl0_118 ),
inference(superposition,[],[f8750,f579]) ).
fof(f8752,plain,
( nil = sk7
| ssList(nil)
| ~ spl0_4
| ~ spl0_23
| ~ spl0_118 ),
inference(trivial_inequality_removal,[],[f8751]) ).
fof(f8753,plain,
( ssList(nil)
| ~ spl0_4
| spl0_18
| ~ spl0_23
| ~ spl0_118 ),
inference(forward_subsumption_resolution,[],[f8752,f807]) ).
fof(f8754,plain,
( $false
| ~ spl0_4
| spl0_10
| spl0_18
| ~ spl0_23
| ~ spl0_118 ),
inference(forward_subsumption_resolution,[],[f8753,f493]) ).
fof(f8755,plain,
( ~ spl0_4
| spl0_10
| spl0_18
| ~ spl0_23
| ~ spl0_118 ),
inference(avatar_contradiction_clause,[],[f8754]) ).
fof(f8797,definition,
( spl0_258
<=> frontsegP(sk3,app(sk6,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_258])],[avatar_definition]) ).
fof(f8799,plain,
( ~ frontsegP(sk3,app(sk6,cons(sk5,nil)))
| spl0_258 ),
inference(avatar_component_clause,[],[f8797]) ).
fof(f8800,plain,
( spl0_52
| ~ spl0_258 ),
inference(avatar_split_clause,[],[f1498,f8797,f1230]) ).
fof(f8802,definition,
( spl0_259
<=> ! [X0] :
( ~ frontsegP(sk3,X0)
| frontsegP(app(sk6,cons(sk5,nil)),X0)
| ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_259])],[avatar_definition]) ).
fof(f8803,plain,
( ! [X0] :
( frontsegP(app(sk6,cons(sk5,nil)),X0)
| ~ frontsegP(sk3,X0)
| ssList(X0) )
| ~ spl0_259 ),
inference(avatar_component_clause,[],[f8802]) ).
fof(f8804,plain,
( spl0_52
| spl0_259 ),
inference(avatar_split_clause,[],[f1697,f8802,f1230]) ).
fof(f8853,plain,
( ssList(sk6)
| ssList(cons(sk5,nil))
| ~ spl0_52 ),
inference(resolution,[],[f1232,f326]) ).
fof(f8854,plain,
( ssList(cons(sk5,nil))
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f8853,f432]) ).
fof(f8855,plain,
( $false
| ~ spl0_52
| spl0_80 ),
inference(forward_subsumption_resolution,[],[f8854,f2657]) ).
fof(f8856,plain,
( ~ spl0_52
| spl0_80 ),
inference(avatar_contradiction_clause,[],[f8855]) ).
fof(f8980,plain,
( frontsegP(sk3,sk6)
| sk8 = hd(sk6)
| ssItem(hd(sk6))
| ssList(tl(sk6))
| ~ spl0_21
| ~ spl0_100 ),
inference(superposition,[],[f2997,f821]) ).
fof(f8982,definition,
( spl0_278
<=> ssList(tl(sk6)) ),
introduced(definition,[new_symbols(definition,[spl0_278])],[avatar_definition]) ).
fof(f8983,plain,
( ~ ssList(tl(sk6))
| spl0_278 ),
inference(avatar_component_clause,[],[f8982]) ).
fof(f8984,plain,
( ssList(tl(sk6))
| ~ spl0_278 ),
inference(avatar_component_clause,[],[f8982]) ).
fof(f8986,definition,
( spl0_279
<=> ssItem(hd(sk6)) ),
introduced(definition,[new_symbols(definition,[spl0_279])],[avatar_definition]) ).
fof(f8988,plain,
( ssItem(hd(sk6))
| ~ spl0_279 ),
inference(avatar_component_clause,[],[f8986]) ).
fof(f8990,definition,
( spl0_280
<=> sk8 = hd(sk6) ),
introduced(definition,[new_symbols(definition,[spl0_280])],[avatar_definition]) ).
fof(f8992,plain,
( sk8 = hd(sk6)
| ~ spl0_280 ),
inference(avatar_component_clause,[],[f8990]) ).
fof(f8994,definition,
( spl0_281
<=> frontsegP(sk3,sk6) ),
introduced(definition,[new_symbols(definition,[spl0_281])],[avatar_definition]) ).
fof(f8995,plain,
( ~ frontsegP(sk3,sk6)
| spl0_281 ),
inference(avatar_component_clause,[],[f8994]) ).
fof(f8997,plain,
( spl0_278
| spl0_279
| spl0_280
| spl0_281
| ~ spl0_21
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f8980,f2996,f819,f8994,f8990,f8986,f8982]) ).
fof(f8999,definition,
( spl0_282
<=> frontsegP(sk6,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_282])],[avatar_definition]) ).
fof(f9000,plain,
( ~ frontsegP(sk6,sk3)
| spl0_282 ),
inference(avatar_component_clause,[],[f8999]) ).
fof(f9008,definition,
( spl0_284
<=> sk3 = sk6 ),
introduced(definition,[new_symbols(definition,[spl0_284])],[avatar_definition]) ).
fof(f9009,plain,
( sk3 = sk6
| ~ spl0_284 ),
inference(avatar_component_clause,[],[f9008]) ).
fof(f9670,plain,
( ssList(sk6)
| nil = sk6
| ~ spl0_278 ),
inference(resolution,[],[f8984,f316]) ).
fof(f9671,plain,
( nil = sk6
| ~ spl0_278 ),
inference(forward_subsumption_resolution,[],[f9670,f432]) ).
fof(f9672,plain,
( $false
| spl0_20
| ~ spl0_278 ),
inference(forward_subsumption_resolution,[],[f9671,f816]) ).
fof(f9673,plain,
( spl0_20
| ~ spl0_278 ),
inference(avatar_contradiction_clause,[],[f9672]) ).
fof(f9812,plain,
( ssList(sk6)
| nil = sk6
| ~ spl0_279 ),
inference(resolution,[],[f8988,f317]) ).
fof(f9813,plain,
( nil = sk6
| ~ spl0_279 ),
inference(forward_subsumption_resolution,[],[f9812,f432]) ).
fof(f9814,plain,
( $false
| spl0_20
| ~ spl0_279 ),
inference(forward_subsumption_resolution,[],[f9813,f816]) ).
fof(f9815,plain,
( spl0_20
| ~ spl0_279 ),
inference(avatar_contradiction_clause,[],[f9814]) ).
fof(f9848,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ssList(app(sk6,cons(sk5,nil)))
| memberP(sk7,X0) )
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f3734,f433]) ).
fof(f9941,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| memberP(sk7,X0) )
| ~ spl0_16
| spl0_52 ),
inference(forward_subsumption_resolution,[],[f9848,f1231]) ).
fof(f10081,plain,
( ssList(sk4)
| ssList(sk3)
| ~ spl0_96
| ~ spl0_103 ),
inference(resolution,[],[f8346,f326]) ).
fof(f10082,plain,
( ssList(sk3)
| ~ spl0_96
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f10081,f428]) ).
fof(f10083,plain,
( $false
| ~ spl0_96
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f10082,f427]) ).
fof(f10084,plain,
( ~ spl0_96
| ~ spl0_103 ),
inference(avatar_contradiction_clause,[],[f10083]) ).
fof(f10089,plain,
( sk6 = cons(sk8,tl(sk6))
| ~ spl0_21
| ~ spl0_280 ),
inference(superposition,[],[f821,f8992]) ).
fof(f12162,plain,
( ~ frontsegP(sk3,sk6)
| ssList(sk6)
| ssList(sk6)
| ssList(cons(sk5,nil))
| ~ spl0_259 ),
inference(resolution,[],[f8803,f1466]) ).
fof(f12172,plain,
( ~ frontsegP(sk3,sk6)
| ssList(sk6)
| ssList(cons(sk5,nil))
| ~ spl0_259 ),
inference(duplicate_literal_removal,[],[f12162]) ).
fof(f12191,plain,
( ~ frontsegP(sk3,sk6)
| ssList(cons(sk5,nil))
| ~ spl0_259 ),
inference(forward_subsumption_resolution,[],[f12172,f432]) ).
fof(f12198,plain,
( ~ frontsegP(sk3,sk6)
| spl0_80
| ~ spl0_259 ),
inference(forward_subsumption_resolution,[],[f12191,f2657]) ).
fof(f12199,plain,
( ~ spl0_281
| spl0_80
| ~ spl0_259 ),
inference(avatar_split_clause,[],[f12198,f8802,f2656,f8994]) ).
fof(f21657,plain,
( ~ frontsegP(sk6,sk3)
| ssList(tl(sk6))
| ~ spl0_21
| ~ spl0_121
| ~ spl0_280 ),
inference(superposition,[],[f3089,f10089]) ).
fof(f21710,plain,
( ~ frontsegP(sk6,sk3)
| ~ spl0_21
| ~ spl0_121
| spl0_278
| ~ spl0_280 ),
inference(forward_subsumption_resolution,[],[f21657,f8983]) ).
fof(f21711,plain,
( ~ spl0_282
| ~ spl0_21
| ~ spl0_121
| spl0_278
| ~ spl0_280 ),
inference(avatar_split_clause,[],[f21710,f8990,f8982,f3088,f819,f8999]) ).
fof(f21714,plain,
( frontsegP(sk3,sk6)
| ssList(sk6)
| ssList(sk3)
| sk3 = sk6
| spl0_282 ),
inference(resolution,[],[f9000,f370]) ).
fof(f21715,plain,
( ssList(sk6)
| ssList(sk3)
| sk3 = sk6
| spl0_281
| spl0_282 ),
inference(forward_subsumption_resolution,[],[f21714,f8995]) ).
fof(f21718,plain,
( ssList(sk3)
| sk3 = sk6
| spl0_281
| spl0_282 ),
inference(forward_subsumption_resolution,[],[f21715,f432]) ).
fof(f21721,plain,
( sk3 = sk6
| spl0_281
| spl0_282 ),
inference(forward_subsumption_resolution,[],[f21718,f427]) ).
fof(f21775,plain,
( spl0_284
| spl0_281
| spl0_282 ),
inference(avatar_split_clause,[],[f21721,f8999,f8994,f9008]) ).
fof(f21928,plain,
( memberP(sk7,sk5)
| ~ spl0_16
| spl0_52
| ~ spl0_187 ),
inference(resolution,[],[f5010,f9941]) ).
fof(f22032,plain,
( ~ memberP(sk3,sk5)
| spl0_8
| ~ spl0_284 ),
inference(superposition,[],[f485,f9009]) ).
fof(f22543,plain,
( ! [X0] :
( memberP(sk3,X0)
| sk8 = X0 )
| ~ spl0_4
| spl0_10
| ~ spl0_16 ),
inference(superposition,[],[f3770,f463]) ).
fof(f22551,plain,
( sk5 = sk8
| ~ spl0_4
| spl0_10
| ~ spl0_16
| spl0_187 ),
inference(resolution,[],[f22543,f5009]) ).
fof(f22700,plain,
( spl0_23
| ~ spl0_4
| spl0_10
| ~ spl0_16
| spl0_187 ),
inference(avatar_split_clause,[],[f22551,f5008,f520,f492,f461,f853]) ).
fof(f22823,plain,
( ~ frontsegP(sk3,app(sk6,cons(sk8,nil)))
| ~ spl0_23
| spl0_258 ),
inference(superposition,[],[f8799,f855]) ).
fof(f22833,plain,
( ~ frontsegP(sk3,app(sk6,sk3))
| ~ spl0_4
| ~ spl0_23
| spl0_258 ),
inference(forward_demodulation,[],[f22823,f463]) ).
fof(f22848,plain,
( ~ frontsegP(sk3,app(sk3,sk3))
| ~ spl0_4
| ~ spl0_23
| spl0_258
| ~ spl0_284 ),
inference(forward_demodulation,[],[f22833,f9009]) ).
fof(f25372,plain,
( ~ frontsegP(sk3,cons(sk8,sk3))
| ~ spl0_4
| spl0_6
| ~ spl0_23
| spl0_258
| ~ spl0_284 ),
inference(superposition,[],[f22848,f5340]) ).
fof(f35175,plain,
( frontsegP(sk3,cons(sk8,sk3))
| ssList(sk3)
| ssList(sk3)
| sk3 = cons(sk8,sk3)
| ~ spl0_4
| spl0_6 ),
inference(superposition,[],[f1499,f5340]) ).
fof(f35178,plain,
( frontsegP(sk3,cons(sk8,sk3))
| ssList(sk3)
| sk3 = cons(sk8,sk3)
| ~ spl0_4
| spl0_6 ),
inference(duplicate_literal_removal,[],[f35175]) ).
fof(f35184,plain,
( frontsegP(sk3,cons(sk8,sk3))
| ssList(sk3)
| ~ spl0_4
| spl0_6
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f35178,f658]) ).
fof(f35229,plain,
( ssList(sk3)
| ~ spl0_4
| spl0_6
| ~ spl0_16
| ~ spl0_23
| spl0_258
| ~ spl0_284 ),
inference(forward_subsumption_resolution,[],[f35184,f25372]) ).
fof(f35250,plain,
( $false
| ~ spl0_4
| spl0_6
| ~ spl0_16
| ~ spl0_23
| spl0_258
| ~ spl0_284 ),
inference(forward_subsumption_resolution,[],[f35229,f427]) ).
fof(f35251,plain,
( ~ spl0_4
| spl0_6
| ~ spl0_16
| ~ spl0_23
| spl0_258
| ~ spl0_284 ),
inference(avatar_contradiction_clause,[],[f35250]) ).
fof(f35316,plain,
( spl0_7
| ~ spl0_16
| spl0_52
| ~ spl0_187 ),
inference(avatar_split_clause,[],[f21928,f5008,f1230,f520,f479]) ).
fof(f35320,plain,
( ~ spl0_187
| spl0_8
| ~ spl0_284 ),
inference(avatar_split_clause,[],[f22032,f9008,f483,f5008]) ).
cnf(s2,plain,
( spl0_1
| ~ spl0_3 ),
inference(sat_conversion,[],[f459]) ).
cnf(s3,plain,
( spl0_1
| spl0_4 ),
inference(sat_conversion,[],[f464]) ).
cnf(s7,plain,
( spl0_1
| ~ spl0_6 ),
inference(sat_conversion,[],[f476]) ).
cnf(s9,plain,
( ~ spl0_7
| ~ spl0_8 ),
inference(sat_conversion,[],[f486]) ).
cnf(s16,plain,
( spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f525]) ).
cnf(s19,plain,
~ spl0_10,
inference(sat_conversion,[],[f528]) ).
cnf(s22,plain,
( spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f822]) ).
cnf(s86,plain,
( spl0_7
| ~ spl0_18 ),
inference(sat_conversion,[],[f1795]) ).
cnf(s98,plain,
( spl0_8
| ~ spl0_20 ),
inference(sat_conversion,[],[f1827]) ).
cnf(s115,plain,
( ~ spl0_1
| spl0_80
| ~ spl0_83 ),
inference(sat_conversion,[],[f2748]) ).
cnf(s119,plain,
( spl0_80
| spl0_83
| spl0_87 ),
inference(sat_conversion,[],[f2807]) ).
cnf(s124,plain,
( spl0_10
| ~ spl0_87 ),
inference(sat_conversion,[],[f2892]) ).
cnf(s125,plain,
( spl0_10
| ~ spl0_80 ),
inference(sat_conversion,[],[f2905]) ).
cnf(s171,plain,
( ~ spl0_20
| spl0_49
| spl0_118 ),
inference(sat_conversion,[],[f3076]) ).
cnf(s174,plain,
( ~ spl0_4
| spl0_6
| spl0_10
| spl0_121 ),
inference(sat_conversion,[],[f3090]) ).
cnf(s210,plain,
( spl0_10
| ~ spl0_49
| spl0_80 ),
inference(sat_conversion,[],[f3442]) ).
cnf(s302,plain,
( ~ spl0_4
| spl0_6
| spl0_10
| ~ spl0_17
| spl0_103 ),
inference(sat_conversion,[],[f5462]) ).
cnf(s319,plain,
( spl0_3
| spl0_6
| spl0_96 ),
inference(sat_conversion,[],[f6285]) ).
cnf(s325,plain,
( ~ spl0_4
| spl0_6
| spl0_10
| spl0_100 ),
inference(sat_conversion,[],[f6430]) ).
cnf(s440,plain,
( ~ spl0_4
| spl0_10
| spl0_18
| ~ spl0_23
| ~ spl0_118 ),
inference(sat_conversion,[],[f8755]) ).
cnf(s450,plain,
( spl0_52
| ~ spl0_258 ),
inference(sat_conversion,[],[f8800]) ).
cnf(s451,plain,
( spl0_52
| spl0_259 ),
inference(sat_conversion,[],[f8804]) ).
cnf(s462,plain,
( ~ spl0_52
| spl0_80 ),
inference(sat_conversion,[],[f8856]) ).
cnf(s473,plain,
( ~ spl0_21
| ~ spl0_100
| spl0_278
| spl0_279
| spl0_280
| spl0_281 ),
inference(sat_conversion,[],[f8997]) ).
cnf(s576,plain,
( spl0_20
| ~ spl0_278 ),
inference(sat_conversion,[],[f9673]) ).
cnf(s590,plain,
( spl0_20
| ~ spl0_279 ),
inference(sat_conversion,[],[f9815]) ).
cnf(s604,plain,
( ~ spl0_96
| ~ spl0_103 ),
inference(sat_conversion,[],[f10084]) ).
cnf(s685,plain,
( spl0_80
| ~ spl0_259
| ~ spl0_281 ),
inference(sat_conversion,[],[f12199]) ).
cnf(s1063,plain,
( ~ spl0_21
| ~ spl0_121
| spl0_278
| ~ spl0_280
| ~ spl0_282 ),
inference(sat_conversion,[],[f21711]) ).
cnf(s1071,plain,
( spl0_281
| spl0_282
| spl0_284 ),
inference(sat_conversion,[],[f21775]) ).
cnf(s1152,plain,
( ~ spl0_4
| spl0_10
| ~ spl0_16
| spl0_23
| spl0_187 ),
inference(sat_conversion,[],[f22700]) ).
cnf(s1465,plain,
( ~ spl0_4
| spl0_6
| ~ spl0_16
| ~ spl0_23
| spl0_258
| ~ spl0_284 ),
inference(sat_conversion,[],[f35251]) ).
cnf(s1472,plain,
( spl0_7
| ~ spl0_16
| spl0_52
| ~ spl0_187 ),
inference(sat_conversion,[],[f35316]) ).
cnf(s1473,plain,
( spl0_8
| ~ spl0_187
| ~ spl0_284 ),
inference(sat_conversion,[],[f35320]) ).
cnf(s1646,plain,
~ spl0_80,
inference(rat,[],[s125,s19]) ).
cnf(s1647,plain,
~ spl0_87,
inference(rat,[],[s124,s19]) ).
cnf(s1648,plain,
~ spl0_52,
inference(rat,[],[s462,s1646]) ).
cnf(s1651,plain,
spl0_83,
inference(rat,[],[s119,s1647,s1646]) ).
cnf(s1652,plain,
~ spl0_1,
inference(rat,[],[s115,s1651,s1646]) ).
cnf(s1653,plain,
~ spl0_49,
inference(rat,[],[s210,s19,s1646]) ).
cnf(s1670,plain,
spl0_259,
inference(rat,[],[s451,s1648]) ).
cnf(s1671,plain,
~ spl0_258,
inference(rat,[],[s450,s1648]) ).
cnf(s1686,plain,
~ spl0_281,
inference(rat,[],[s685,s1646,s1670]) ).
cnf(s1732,plain,
~ spl0_6,
inference(rat,[],[s7,s1652]) ).
cnf(s1733,plain,
spl0_4,
inference(rat,[],[s3,s1652]) ).
cnf(s1776,plain,
spl0_100,
inference(rat,[],[s325,s1732,s19,s1733]) ).
cnf(s1780,plain,
spl0_121,
inference(rat,[],[s174,s1732,s19,s1733]) ).
cnf(s1794,plain,
~ spl0_3,
inference(rat,[],[s2,s1652]) ).
cnf(s1795,plain,
spl0_96,
inference(rat,[],[s319,s1732,s1794]) ).
cnf(s1797,plain,
~ spl0_103,
inference(rat,[],[s604,s1795]) ).
cnf(s1808,plain,
~ spl0_17,
inference(rat,[],[s302,s1733,s1732,s19,s1797]) ).
cnf(s1832,plain,
spl0_16,
inference(rat,[],[s16,s1808]) ).
cnf(s1899,plain,
( spl0_18
| ~ spl0_23 ),
inference(rat,[],[s1063,s473,s22,s576,s590,s1071,s171,s1465,s440,s19,s1832,s1671,s1733,s1732,s1653,s1686,s1776,s1780]) ).
cnf(s1900,plain,
spl0_7,
inference(rat,[],[s1899,s1152,s86,s1472,s19,s1733,s1832,s1648]) ).
cnf(s1901,plain,
~ spl0_8,
inference(rat,[],[s9,s1900]) ).
cnf(s1902,plain,
~ spl0_20,
inference(rat,[],[s98,s1901]) ).
cnf(s1907,plain,
~ spl0_279,
inference(rat,[],[s590,s1902]) ).
cnf(s1908,plain,
~ spl0_278,
inference(rat,[],[s576,s1902]) ).
cnf(s1915,plain,
spl0_21,
inference(rat,[],[s22,s1902]) ).
cnf(s1950,plain,
spl0_280,
inference(rat,[],[s473,s1686,s1908,s1907,s1776,s1915]) ).
cnf(s1965,plain,
~ spl0_282,
inference(rat,[],[s1063,s1915,s1908,s1780,s1950]) ).
cnf(s1966,plain,
spl0_284,
inference(rat,[],[s1071,s1686,s1965]) ).
cnf(s1998,plain,
~ spl0_23,
inference(rat,[],[s1465,s1832,s1671,s1733,s1732,s1966]) ).
cnf(s1999,plain,
~ spl0_187,
inference(rat,[],[s1473,s1901,s1966]) ).
cnf(s2011,plain,
$false,
inference(rat,[],[s1152,s1832,s1733,s19,s1999,s1998]) ).
fof(f35924,plain,
$false,
inference(avatar_sat_refutation,[],[s2011]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC183-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.37 % Computer : n019.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 28 08:21:12 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.22/1.24 % (3850013)Will run a generic schedule for satisfiability detection.
% 5.22/1.24 % (3850021)dis+10_1_sil=32000:sp=arity:random_seed=680127370:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.22/1.24 % (3850019)% WARNING: option uhcvi not known.
% 5.22/1.24 % (3850018)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=177864948_2999 on theBenchmark for (2999ds/0Mi)
% 5.22/1.24 % (3850019)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3973045430:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.22/1.24 % (3850020)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=845646742:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.22/1.24 % (3850022)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3946221630:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.22/1.24 % (3850023)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=564221085:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.22/1.24 % (3850024)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2356682292:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.22/1.24 % TRYING [1]
% 5.22/1.24 % TRYING [2]
% 5.22/1.24 % TRYING [3]
% 5.22/1.24 % (3850021)Instruction limit reached!
% 5.22/1.24 % (3850021)------------------------------
% 5.22/1.24 % (3850021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.22/1.24 % (3850021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.24 % (3850021)CaDiCaL version: 2.1.3
% 5.22/1.24 % (3850021)Termination reason: Instruction limit
% 5.22/1.24 % (3850021)Termination phase: Saturation
% 5.22/1.24 % (3850021)Time elapsed: 0.035 s
% 5.22/1.24 % (3850021)Peak memory usage: 13 MB
% 5.22/1.24 % (3850021)Instructions burned: 105 (million)
% 5.22/1.24 % TRYING [4]
% 5.22/1.24 % (3850032)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4031487506:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.22/1.24 % TRYING [1]
% 5.22/1.24 % TRYING [2]
% 5.22/1.24 % (3850022)Instruction limit reached!
% 5.22/1.24 % (3850022)------------------------------
% 5.22/1.24 % (3850022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.22/1.24 % (3850022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.24 % (3850022)CaDiCaL version: 2.1.3
% 5.22/1.24 % (3850022)Termination reason: Instruction limit
% 5.22/1.24 % (3850022)Termination phase: Saturation
% 5.22/1.24 % (3850022)Time elapsed: 0.061 s
% 5.22/1.24 % (3850022)Peak memory usage: 13 MB
% 5.22/1.24 % (3850022)Instructions burned: 116 (million)
% 5.22/1.24 % TRYING [3]
% 5.22/1.24 % (3850023)Instruction limit reached!
% 5.22/1.24 % (3850023)------------------------------
% 5.22/1.24 % (3850023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.22/1.24 % (3850023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.24 % (3850023)CaDiCaL version: 2.1.3
% 5.22/1.24 % (3850023)Termination reason: Instruction limit
% 5.22/1.24 % (3850023)Termination phase: Saturation
% 5.22/1.24 % (3850023)Time elapsed: 0.066 s
% 5.22/1.24 % (3850023)Peak memory usage: 14 MB
% 5.22/1.24 % (3850023)Instructions burned: 132 (million)
% 5.22/1.24 % (3850034)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1039110736:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 5.22/1.24 % TRYING [4]
% 5.22/1.24 % (3850035)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=3462839330:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.22/1.24 % (3850024)Instruction limit reached!
% 5.22/1.24 % (3850024)------------------------------
% 5.22/1.24 % (3850024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.22/1.24 % (3850024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.24 % (3850024)CaDiCaL version: 2.1.3
% 5.22/1.24 % (3850024)Termination reason: Instruction limit
% 5.22/1.24 % (3850024)Termination phase: Saturation
% 5.22/1.24 % (3850024)Time elapsed: 0.099 s
% 5.22/1.24 % (3850024)Peak memory usage: 14 MB
% 5.22/1.24 % (3850024)Instructions burned: 165 (million)
% 5.22/1.24 % TRYING [5]
% 5.22/1.24 % TRYING [5]
% 5.22/1.24 % (3850038)ott-21_1_sil=16000:fs=off:random_seed=850077983:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.22/1.24 % (3850034)Instruction limit reached!
% 5.22/1.24 % (3850034)------------------------------
% 5.22/1.24 % (3850034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.22/1.24 % (3850034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.24 % (3850034)CaDiCaL version: 2.1.3
% 5.22/1.24 % (3850034)Termination reason: Instruction limit
% 5.22/1.24 % (3850034)Termination phase: Saturation
% 5.22/1.24 % (3850034)Time elapsed: 0.071 s
% 5.22/1.24 % (3850034)Peak memory usage: 13 MB
% 5.22/1.24 % (3850034)Instructions burned: 132 (million)
% 5.22/1.24 % (3850040)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2914499788:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 5.22/1.24 % (3850038)Instruction limit reached!
% 5.22/1.24 % (3850038)------------------------------
% 5.22/1.24 % (3850038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.22/1.24 % (3850038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.24 % (3850038)CaDiCaL version: 2.1.3
% 5.22/1.24 % (3850038)Termination reason: Instruction limit
% 5.22/1.24 % (3850038)Termination phase: Saturation
% 5.22/1.24 % (3850038)Time elapsed: 0.089 s
% 5.22/1.24 % (3850038)Peak memory usage: 13 MB
% 5.22/1.24 % (3850038)Instructions burned: 180 (million)
% 5.22/1.24 % TRYING [6]
% 5.22/1.24 % (3850032)Instruction limit reached!
% 5.22/1.24 % (3850032)------------------------------
% 5.22/1.24 % (3850032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.22/1.24 % (3850032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.24 % (3850032)CaDiCaL version: 2.1.3
% 5.22/1.24 % (3850032)Termination reason: Instruction limit
% 5.22/1.24 % (3850032)Termination phase: Finite model building constraint generation
% 5.22/1.24 % (3850032)Time elapsed: 0.166 s
% 5.22/1.24 % (3850032)Peak memory usage: 34 MB
% 5.22/1.24 % (3850032)Instructions burned: 718 (million)
% 5.22/1.24 % (3850043)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=23173083:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 5.22/1.24 % (3850042)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1215203726:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 5.22/1.24 % TRYING [1]
% 5.22/1.24 % TRYING [2]
% 5.22/1.24 % TRYING [3]
% 5.22/1.24 % TRYING [6]
% 5.22/1.24 % TRYING [4]
% 5.22/1.24 % TRYING [5]
% 5.22/1.24 % (3850040)Instruction limit reached!
% 5.22/1.24 % (3850040)------------------------------
% 5.22/1.24 % (3850040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.22/1.24 % (3850040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.24 % (3850040)CaDiCaL version: 2.1.3
% 5.22/1.24 % (3850040)Termination reason: Instruction limit
% 5.22/1.24 % (3850040)Termination phase: Saturation
% 5.22/1.24 % (3850040)Time elapsed: 0.297 s
% 5.22/1.24 % (3850040)Peak memory usage: 14 MB
% 5.22/1.24 % (3850040)Instructions burned: 477 (million)
% 5.22/1.24 % (3850035)Instruction limit reached!
% 5.22/1.24 % (3850035)------------------------------
% 5.22/1.24 % (3850035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.22/1.24 % (3850035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.24 % (3850035)CaDiCaL version: 2.1.3
% 5.22/1.24 % (3850035)Termination reason: Instruction limit
% 5.22/1.24 % (3850035)Termination phase: Saturation
% 5.22/1.24 % (3850035)Time elapsed: 0.388 s
% 5.22/1.24 % (3850035)Peak memory usage: 19 MB
% 5.22/1.24 % (3850035)Instructions burned: 684 (million)
% 5.22/1.24 % (3850046)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1184049932:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 5.22/1.24 % (3850047)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=2188773093: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)
% 5.22/1.24 % (3850042)Instruction limit reached!
% 5.22/1.24 % (3850042)------------------------------
% 5.22/1.24 % (3850042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.22/1.24 % (3850042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.24 % (3850042)CaDiCaL version: 2.1.3
% 5.22/1.24 % (3850042)Termination reason: Instruction limit
% 5.22/1.24 % (3850042)Termination phase: Finite model building SAT solving
% 5.22/1.24 % (3850042)Time elapsed: 0.337 s
% 5.22/1.24 % (3850042)Peak memory usage: 22 MB
% 5.22/1.24 % (3850042)Instructions burned: 868 (million)
% 5.22/1.24 % (3850043)Instruction limit reached!
% 5.22/1.24 % (3850043)------------------------------
% 5.22/1.24 % (3850043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.22/1.24 % (3850050)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4279774569:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 5.22/1.24 % (3850043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.24 % (3850043)CaDiCaL version: 2.1.3
% 5.22/1.24 % (3850043)Termination reason: Instruction limit
% 5.22/1.24 % (3850043)Termination phase: Saturation
% 5.22/1.24 % (3850043)Time elapsed: 0.365 s
% 5.22/1.24 % (3850043)Peak memory usage: 27 MB
% 5.22/1.24 % (3850043)Instructions burned: 1181 (million)
% 5.22/1.24 % TRYING [14]
% 5.22/1.24 % (3850052)fmb+10_1_sil=64000:random_seed=2104478828:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 5.22/1.24 % TRYING [1]
% 5.22/1.24 % TRYING [2]
% 5.22/1.24 % TRYING [3]
% 5.22/1.24 % TRYING [4]
% 5.22/1.24 % TRYING [5]
% 5.22/1.24 % TRYING [7]
% 5.22/1.24 % (3850019) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3850013-3850019"...
% 5.22/1.24 % (3850019)...printing done.
% 5.22/1.24 % (3850019)Refutation found. Thanks to Tanya!
% 5.22/1.24 % SZS status Unsatisfiable for theBenchmark
% 5.22/1.24 % SZS output start Proof for theBenchmark
% See solution above
% 5.22/1.25 % (3850019)------------------------------
% 5.22/1.25 % (3850019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.22/1.25 % (3850019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.22/1.25 % (3850019)CaDiCaL version: 2.1.3
% 5.22/1.25 % (3850019)Termination reason: Refutation
% 5.22/1.25 % (3850019)Time elapsed: 0.778 s
% 5.22/1.25 % (3850019)Peak memory usage: 25 MB
% 5.22/1.25 % (3850019)Instructions burned: 1392 (million)
% 5.22/1.25 % (3850013)Success in time 0.825 s
% 5.22/1.25 % Vampire exiting
%------------------------------------------------------------------------------