%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC295-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 : n002.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:26 PM UTC 2026
% Result : Unsatisfiable 8.03s 1.59s
% Output : Refutation 8.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 60
% Syntax : Number of formulae : 272 ( 37 unt; 16 def)
% Number of atoms : 955 ( 99 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 1268 ( 585 ~; 667 |; 0 &)
% ( 16 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 17 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-2 aty)
% Number of variables : 149 ( 0 sgn 149 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f12,axiom,
! [X0] : ssItem(skaf83(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause12) ).
fof(f13,axiom,
! [X0] : ssList(skaf82(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause13) ).
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] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
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(f74,axiom,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause74) ).
fof(f80,axiom,
! [X0] :
( ~ segmentP(nil,X0)
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause80) ).
fof(f84,axiom,
! [X0] :
( ~ frontsegP(nil,X0)
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause84) ).
fof(f85,axiom,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause86) ).
fof(f96,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| tl(cons(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause96) ).
fof(f100,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| cons(X0,X1) != X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause99) ).
fof(f112,axiom,
! [X0] :
( ~ ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause109) ).
fof(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(X1,X0)
| ~ frontsegP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| X0 = X1 ),
inference(reorient_equations,[],[f138]) ).
fof(f144,axiom,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| nil = X1
| tl(app(X1,X0)) = app(tl(X1),X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause133) ).
fof(f148,axiom,
! [X2,X0,X1] :
( frontsegP(app(X0,X2),X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause137) ).
fof(f149,axiom,
! [X2,X0,X1] :
( X0 != X1
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0)
| memberP(cons(X1,X2),X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause138) ).
fof(f151,axiom,
! [X2,X0,X1] :
( memberP(app(X0,X2),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ memberP(X0,X1) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SWC001-0.ax',clause144) ).
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(f188,axiom,
! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ~ ssList(X3)
| ~ ssList(X1)
| ~ ssItem(X2)
| ~ ssItem(X0)
| frontsegP(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause174) ).
fof(f189,axiom,
! [X2,X3,X0,X1] :
( app(X0,cons(X1,X2)) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(X3)
| memberP(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause175) ).
fof(f192,axiom,
! [X2,X3,X0,X1] :
( ~ frontsegP(X0,X1)
| X2 != X3
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X2)
| frontsegP(cons(X2,X0),cons(X3,X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause178) ).
fof(f193,axiom,
! [X2,X3,X0,X1,X4] :
( app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(X4)
| ~ ssList(X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(f202,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_3) ).
fof(f203,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_4) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
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,
ssItem(sk8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_11) ).
fof(f212,negated_conjecture,
( memberP(sk6,sk8)
| memberP(sk7,sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_12) ).
fof(f217,negated_conjecture,
( ssItem(sk9)
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_17) ).
fof(f218,negated_conjecture,
( cons(sk9,nil) = sk3
| nil = sk4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_18) ).
fof(f219,plain,
( sk3 = cons(sk9,nil)
| nil = sk4 ),
inference(reorient_equations,[],[f218]) ).
fof(f220,negated_conjecture,
( memberP(sk4,sk9)
| nil = sk4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_19) ).
fof(f222,negated_conjecture,
( cons(sk9,nil) = sk3
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_21) ).
fof(f223,plain,
( sk3 = cons(sk9,nil)
| nil = sk3 ),
inference(reorient_equations,[],[f222]) ).
fof(f224,negated_conjecture,
( memberP(sk4,sk9)
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_22) ).
fof(f228,plain,
sk3 = app(app(sk6,cons(sk5,nil)),sk7),
inference(definition_unfolding,[],[f210,f205]) ).
fof(f238,plain,
! [X2,X1] :
( ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X1)
| memberP(cons(X1,X2),X1) ),
inference(equality_resolution,[],[f149]) ).
fof(f240,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1))
| frontsegP(app(X0,X1),X0) ),
inference(equality_resolution,[],[f155]) ).
fof(f243,plain,
! [X2,X0,X1] :
( segmentP(app(app(X0,X1),X2),X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(app(X0,X1),X2))
| ~ ssList(X2) ),
inference(equality_resolution,[],[f187]) ).
fof(f244,plain,
! [X2,X0,X1] :
( memberP(app(X0,cons(X1,X2)),X1)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(app(X0,cons(X1,X2)))
| ~ ssList(X2) ),
inference(equality_resolution,[],[f189]) ).
fof(f245,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(f246,plain,
! [X2,X3,X0,X1] :
( ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(equality_resolution,[],[f193]) ).
fof(f253,plain,
! [X3,X0,X1] :
( frontsegP(cons(X3,X0),cons(X3,X1))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ frontsegP(X0,X1) ),
inference(duplicate_literal_removal,[],[f245]) ).
fof(f255,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X2) ),
inference(duplicate_literal_removal,[],[f238]) ).
fof(f260,definition,
( spl0_1
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f261,plain,
( nil != sk4
| spl0_1 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f262,plain,
( nil = sk4
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f264,definition,
( spl0_2
<=> ssItem(sk9) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f265,plain,
( ~ ssItem(sk9)
| spl0_2 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f266,plain,
( ssItem(sk9)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f269,definition,
( spl0_3
<=> memberP(sk7,sk8) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f271,plain,
( memberP(sk7,sk8)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f273,definition,
( spl0_4
<=> memberP(sk6,sk8) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f275,plain,
( memberP(sk6,sk8)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f273]) ).
fof(f276,plain,
( spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f212,f273,f269]) ).
fof(f283,definition,
( spl0_6
<=> memberP(sk4,sk9) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f285,plain,
( memberP(sk4,sk9)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f286,plain,
( spl0_1
| spl0_6 ),
inference(avatar_split_clause,[],[f220,f283,f260]) ).
fof(f288,plain,
( memberP(nil,sk9)
| nil = sk3
| ~ spl0_1 ),
inference(forward_demodulation,[],[f224,f262]) ).
fof(f290,definition,
( spl0_7
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f291,plain,
( nil != sk3
| spl0_7 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f292,plain,
( nil = sk3
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f294,definition,
( spl0_8
<=> memberP(nil,sk9) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f296,plain,
( memberP(nil,sk9)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f294]) ).
fof(f297,plain,
( spl0_7
| spl0_8
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f288,f260,f294,f290]) ).
fof(f316,definition,
( spl0_9
<=> ! [X1] : ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f317,plain,
( ! [X1] : ssItem(X1)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f316]) ).
fof(f319,definition,
( spl0_10
<=> ! [X0] :
( ~ ssList(X0)
| duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f320,plain,
( ! [X0] :
( duplicatefreeP(X0)
| ~ ssList(X0) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f321,plain,
( spl0_9
| spl0_10 ),
inference(avatar_split_clause,[],[f72,f319,f316]) ).
fof(f382,plain,
sk3 = app(nil,sk3),
inference(resolution,[],[f74,f202]) ).
fof(f385,plain,
sk7 = app(nil,sk7),
inference(resolution,[],[f74,f208]) ).
fof(f670,plain,
( sk6 = cons(skaf83(sk6),skaf82(sk6))
| nil = sk6 ),
inference(resolution,[],[f112,f207]) ).
fof(f904,plain,
! [X0,X1] :
( frontsegP(app(X0,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(forward_subsumption_resolution,[],[f240,f85]) ).
fof(f906,definition,
( spl0_15
<=> ssList(app(sk6,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f907,plain,
( ssList(app(sk6,cons(sk5,nil)))
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f906]) ).
fof(f908,plain,
( ~ ssList(app(sk6,cons(sk5,nil)))
| spl0_15 ),
inference(avatar_component_clause,[],[f906]) ).
fof(f935,plain,
( frontsegP(sk3,app(sk6,cons(sk5,nil)))
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(sk7) ),
inference(superposition,[],[f904,f228]) ).
fof(f943,plain,
( frontsegP(sk3,app(sk6,cons(sk5,nil)))
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(forward_subsumption_resolution,[],[f935,f208]) ).
fof(f949,plain,
( ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| spl0_15 ),
inference(resolution,[],[f908,f85]) ).
fof(f950,plain,
( ~ ssList(cons(sk5,nil))
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f949,f207]) ).
fof(f1028,plain,
( sk3 = cons(sk9,nil)
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f219,f261]) ).
fof(f1154,plain,
! [X0] :
( frontsegP(sk3,X0)
| ~ ssList(sk7)
| ~ ssList(X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ frontsegP(app(sk6,cons(sk5,nil)),X0) ),
inference(superposition,[],[f148,f228]) ).
fof(f1163,plain,
! [X0] :
( frontsegP(sk3,X0)
| ~ ssList(X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ frontsegP(app(sk6,cons(sk5,nil)),X0) ),
inference(forward_subsumption_resolution,[],[f1154,f208]) ).
fof(f1446,plain,
! [X0] :
( ~ ssList(X0)
| nil = sk3
| tl(app(sk3,X0)) = app(tl(sk3),X0) ),
inference(resolution,[],[f144,f202]) ).
fof(f1489,plain,
( ! [X0] :
( ~ ssList(X0)
| tl(app(sk3,X0)) = app(tl(sk3),X0) )
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f1446,f291]) ).
fof(f2514,plain,
( segmentP(sk3,cons(sk5,nil))
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk3)
| ~ ssList(sk7) ),
inference(superposition,[],[f243,f228]) ).
fof(f2519,plain,
( segmentP(sk3,cons(sk5,nil))
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk3)
| ~ ssList(sk7) ),
inference(forward_subsumption_resolution,[],[f2514,f207]) ).
fof(f2531,plain,
( segmentP(sk3,cons(sk5,nil))
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7) ),
inference(forward_subsumption_resolution,[],[f2519,f202]) ).
fof(f2541,plain,
( segmentP(sk3,cons(sk5,nil))
| ~ ssList(cons(sk5,nil)) ),
inference(forward_subsumption_resolution,[],[f2531,f208]) ).
fof(f2978,definition,
( spl0_19
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f2979,plain,
( ssList(cons(sk5,nil))
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f2978]) ).
fof(f2980,plain,
( ~ ssList(cons(sk5,nil))
| spl0_19 ),
inference(avatar_component_clause,[],[f2978]) ).
fof(f2982,definition,
( spl0_20
<=> segmentP(sk3,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f2984,plain,
( segmentP(sk3,cons(sk5,nil))
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f2982]) ).
fof(f2985,plain,
( ~ spl0_19
| spl0_20 ),
inference(avatar_split_clause,[],[f2541,f2982,f2978]) ).
fof(f3054,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| spl0_19 ),
inference(resolution,[],[f86,f2980]) ).
fof(f3067,plain,
( ~ ssItem(sk5)
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f3054,f8]) ).
fof(f3068,plain,
( $false
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f3067,f206]) ).
fof(f3069,plain,
spl0_19,
inference(avatar_contradiction_clause,[],[f3068]) ).
fof(f3103,plain,
! [X0] :
( ~ ssList(X0)
| cons(sk5,X0) != X0 ),
inference(resolution,[],[f100,f206]) ).
fof(f3139,plain,
nil != cons(sk5,nil),
inference(resolution,[],[f3103,f8]) ).
fof(f3200,plain,
( ! [X0] :
( ~ ssList(X0)
| tl(cons(sk9,X0)) = X0 )
| ~ spl0_2 ),
inference(resolution,[],[f96,f266]) ).
fof(f3382,plain,
( ! [X0] :
( ~ ssList(X0)
| cons(sk9,X0) = app(cons(sk9,nil),X0) )
| ~ spl0_2 ),
inference(resolution,[],[f126,f266]) ).
fof(f3535,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssList(sk7)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssItem(X0)
| ~ memberP(app(sk6,cons(sk5,nil)),X0) ),
inference(superposition,[],[f151,f228]) ).
fof(f3542,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssItem(X0)
| ~ memberP(app(sk6,cons(sk5,nil)),X0) ),
inference(forward_subsumption_resolution,[],[f3535,f208]) ).
fof(f3544,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(app(sk6,cons(sk5,nil)),X0) )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f3542,f907]) ).
fof(f3835,plain,
( ~ ssItem(sk9)
| ~ ssList(sk4)
| sk4 = app(skaf42(sk4,sk9),cons(sk9,skaf43(sk9,sk4)))
| ~ spl0_6 ),
inference(resolution,[],[f182,f285]) ).
fof(f3844,plain,
( ~ ssList(sk4)
| sk4 = app(skaf42(sk4,sk9),cons(sk9,skaf43(sk9,sk4)))
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f3835,f266]) ).
fof(f3852,plain,
( sk4 = app(skaf42(sk4,sk9),cons(sk9,skaf43(sk9,sk4)))
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f3844,f203]) ).
fof(f3936,plain,
( ! [X2,X3,X0,X1] :
( ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(X3) )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f246,f320]) ).
fof(f3940,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,cons(sk9,X1)),sk3))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(sk9)
| ~ ssList(nil) )
| spl0_1
| ~ spl0_10 ),
inference(superposition,[],[f3936,f1028]) ).
fof(f3943,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,cons(sk9,X1)),sk3))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(nil) )
| spl0_1
| ~ spl0_2
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f3940,f266]) ).
fof(f3948,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,cons(sk9,X1)),sk3))
| ~ ssList(X1)
| ~ ssList(X0) )
| spl0_1
| ~ spl0_2
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f3943,f8]) ).
fof(f4099,plain,
( nil = tl(cons(sk9,nil))
| ~ spl0_2 ),
inference(resolution,[],[f3200,f8]) ).
fof(f4420,definition,
( spl0_21
<=> nil = sk6 ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f4421,plain,
( nil != sk6
| spl0_21 ),
inference(avatar_component_clause,[],[f4420]) ).
fof(f4422,plain,
( nil = sk6
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f4420]) ).
fof(f4441,definition,
( spl0_23
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f4442,plain,
( nil != sk7
| spl0_23 ),
inference(avatar_component_clause,[],[f4441]) ).
fof(f4443,plain,
( nil = sk7
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f4441]) ).
fof(f4451,plain,
( memberP(nil,sk8)
| ~ spl0_3
| ~ spl0_23 ),
inference(superposition,[],[f271,f4443]) ).
fof(f4466,plain,
( ~ ssItem(sk8)
| ~ spl0_3
| ~ spl0_23 ),
inference(resolution,[],[f4451,f71]) ).
fof(f4469,plain,
( $false
| ~ spl0_3
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f4466,f211]) ).
fof(f4470,plain,
( ~ spl0_3
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f4469]) ).
fof(f5736,plain,
( ~ ssList(app(sk4,sk3))
| ~ ssList(skaf43(sk9,sk4))
| ~ ssList(skaf42(sk4,sk9))
| spl0_1
| ~ spl0_2
| ~ spl0_6
| ~ spl0_10 ),
inference(superposition,[],[f3948,f3852]) ).
fof(f5737,plain,
( ~ ssList(app(sk4,sk3))
| ~ ssList(skaf42(sk4,sk9))
| spl0_1
| ~ spl0_2
| ~ spl0_6
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f5736,f52]) ).
fof(f5741,plain,
( ~ ssList(app(sk4,sk3))
| spl0_1
| ~ spl0_2
| ~ spl0_6
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f5737,f53]) ).
fof(f5742,plain,
( ~ ssList(sk4)
| ~ ssList(sk3)
| spl0_1
| ~ spl0_2
| ~ spl0_6
| ~ spl0_10 ),
inference(resolution,[],[f5741,f85]) ).
fof(f5743,plain,
( ~ ssList(sk3)
| spl0_1
| ~ spl0_2
| ~ spl0_6
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f5742,f203]) ).
fof(f5744,plain,
( $false
| spl0_1
| ~ spl0_2
| ~ spl0_6
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f5743,f202]) ).
fof(f5745,plain,
( spl0_1
| ~ spl0_2
| ~ spl0_6
| ~ spl0_10 ),
inference(avatar_contradiction_clause,[],[f5744]) ).
fof(f5746,plain,
( sk3 = cons(sk9,nil)
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f223,f291]) ).
fof(f5784,plain,
( ~ ssItem(sk9)
| ~ spl0_8 ),
inference(resolution,[],[f296,f71]) ).
fof(f5787,plain,
( $false
| ~ spl0_2
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f5784,f266]) ).
fof(f5788,plain,
( ~ spl0_2
| ~ spl0_8 ),
inference(avatar_contradiction_clause,[],[f5787]) ).
fof(f5802,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssList(nil)
| ~ ssItem(sk9)
| ~ ssItem(X0)
| memberP(nil,X0)
| sk9 = X0 )
| spl0_7 ),
inference(superposition,[],[f174,f5746]) ).
fof(f5807,plain,
( ! [X0,X1] :
( ~ frontsegP(sk3,cons(X0,X1))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ ssItem(X0)
| ~ ssItem(sk9)
| frontsegP(nil,X1) )
| spl0_7 ),
inference(superposition,[],[f188,f5746]) ).
fof(f5823,plain,
( ! [X0] :
( frontsegP(cons(sk9,X0),sk3)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(sk9)
| ~ frontsegP(X0,nil) )
| spl0_7 ),
inference(superposition,[],[f253,f5746]) ).
fof(f5828,plain,
( ! [X0] :
( frontsegP(cons(sk9,X0),sk3)
| ~ ssList(X0)
| ~ ssItem(sk9)
| ~ frontsegP(X0,nil) )
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f5823,f8]) ).
fof(f5843,plain,
( ! [X0,X1] :
( ~ frontsegP(sk3,cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(sk9)
| frontsegP(nil,X1) )
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f5807,f8]) ).
fof(f5848,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(sk9)
| ~ ssItem(X0)
| memberP(nil,X0)
| sk9 = X0 )
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f5802,f8]) ).
fof(f5857,plain,
( ! [X0] :
( frontsegP(cons(sk9,X0),sk3)
| ~ ssList(X0)
| ~ frontsegP(X0,nil) )
| ~ spl0_2
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f5828,f266]) ).
fof(f5872,plain,
( ! [X0,X1] :
( ~ frontsegP(sk3,cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0)
| frontsegP(nil,X1) )
| ~ spl0_2
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f5843,f266]) ).
fof(f5877,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(X0)
| memberP(nil,X0)
| sk9 = X0 )
| ~ spl0_2
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f5848,f266]) ).
fof(f5879,plain,
( ! [X0] :
( frontsegP(cons(sk9,X0),sk3)
| ~ ssList(X0) )
| ~ spl0_2
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f5857,f60]) ).
fof(f5880,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(X0)
| sk9 = X0 )
| ~ spl0_2
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f5877,f71]) ).
fof(f6027,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| sk9 = X0 )
| ~ spl0_2
| spl0_7
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f5880,f317]) ).
fof(f6079,plain,
( nil = tl(sk3)
| ~ spl0_2
| spl0_7 ),
inference(forward_demodulation,[],[f4099,f5746]) ).
fof(f6342,plain,
( ! [X0] :
( ~ ssList(X0)
| app(nil,X0) = tl(app(sk3,X0)) )
| ~ spl0_2
| spl0_7 ),
inference(forward_demodulation,[],[f1489,f6079]) ).
fof(f6382,plain,
( app(nil,sk7) = tl(app(sk3,sk7))
| ~ spl0_2
| spl0_7 ),
inference(resolution,[],[f6342,f208]) ).
fof(f6383,plain,
( sk7 = tl(app(sk3,sk7))
| ~ spl0_2
| spl0_7 ),
inference(forward_demodulation,[],[f6382,f385]) ).
fof(f6395,plain,
( ! [X0] :
( ~ ssList(X0)
| app(sk3,X0) = cons(sk9,X0) )
| ~ spl0_2
| spl0_7 ),
inference(forward_demodulation,[],[f3382,f5746]) ).
fof(f6536,plain,
( cons(sk9,sk3) = app(sk3,sk3)
| ~ spl0_2
| spl0_7 ),
inference(resolution,[],[f6395,f202]) ).
fof(f6832,plain,
( ! [X0] :
( ~ memberP(app(sk6,cons(sk5,nil)),X0)
| memberP(sk3,X0) )
| ~ spl0_9
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f3544,f317]) ).
fof(f6940,plain,
( sk6 = cons(skaf83(sk6),skaf82(sk6))
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f670,f4421]) ).
fof(f6973,plain,
( memberP(sk6,skaf83(sk6))
| ~ ssItem(skaf83(sk6))
| ~ ssList(skaf82(sk6))
| spl0_21 ),
inference(superposition,[],[f255,f6940]) ).
fof(f6982,plain,
( memberP(sk6,skaf83(sk6))
| ~ ssList(skaf82(sk6))
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f6973,f12]) ).
fof(f7013,plain,
( memberP(sk6,skaf83(sk6))
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f6982,f13]) ).
fof(f7069,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk6)
| ~ ssItem(X0)
| ~ memberP(sk6,X0) )
| ~ spl0_9
| ~ spl0_15 ),
inference(resolution,[],[f6832,f151]) ).
fof(f7070,plain,
( memberP(sk3,sk5)
| ~ ssList(sk6)
| ~ ssItem(sk5)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(nil)
| ~ spl0_9
| ~ spl0_15 ),
inference(resolution,[],[f6832,f244]) ).
fof(f7071,plain,
( memberP(sk3,sk5)
| ~ ssItem(sk5)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(nil)
| ~ spl0_9
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f7070,f207]) ).
fof(f7072,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssList(sk6)
| ~ ssItem(X0)
| ~ memberP(sk6,X0) )
| ~ spl0_9
| ~ spl0_15
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f7069,f2979]) ).
fof(f7074,plain,
( memberP(sk3,sk5)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(nil)
| ~ spl0_9
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f7071,f206]) ).
fof(f7075,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk6,X0) )
| ~ spl0_9
| ~ spl0_15
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f7072,f207]) ).
fof(f7077,plain,
( memberP(sk3,sk5)
| ~ ssList(nil)
| ~ spl0_9
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f7074,f907]) ).
fof(f7078,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ memberP(sk6,X0) )
| ~ spl0_9
| ~ spl0_15
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f7075,f317]) ).
fof(f7080,plain,
( memberP(sk3,sk5)
| ~ spl0_9
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f7077,f8]) ).
fof(f7081,plain,
( sk5 = sk9
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15 ),
inference(resolution,[],[f7080,f6027]) ).
fof(f7272,plain,
( ! [X0,X1] :
( ~ frontsegP(sk3,cons(X0,X1))
| ~ ssList(X1)
| frontsegP(nil,X1) )
| ~ spl0_2
| spl0_7
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f5872,f317]) ).
fof(f7402,plain,
( frontsegP(sk3,app(sk6,cons(sk5,nil)))
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f943,f907]) ).
fof(f7403,plain,
( frontsegP(sk3,app(sk6,cons(sk9,nil)))
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15 ),
inference(forward_demodulation,[],[f7402,f7081]) ).
fof(f7404,plain,
( frontsegP(sk3,app(sk6,sk3))
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15 ),
inference(forward_demodulation,[],[f7403,f5746]) ).
fof(f7670,plain,
( ! [X0] :
( ~ memberP(sk6,X0)
| sk9 = X0 )
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_19 ),
inference(resolution,[],[f7078,f6027]) ).
fof(f7791,plain,
( sk9 = skaf83(sk6)
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_19
| spl0_21 ),
inference(resolution,[],[f7670,f7013]) ).
fof(f7795,plain,
( sk6 = cons(sk9,skaf82(sk6))
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_19
| spl0_21 ),
inference(superposition,[],[f6940,f7791]) ).
fof(f9071,plain,
( frontsegP(sk6,sk3)
| ~ ssList(skaf82(sk6))
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_19
| spl0_21 ),
inference(superposition,[],[f5879,f7795]) ).
fof(f9142,plain,
( frontsegP(sk6,sk3)
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_19
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f9071,f13]) ).
fof(f9196,plain,
( ~ frontsegP(sk3,sk6)
| ~ ssList(sk3)
| ~ ssList(sk6)
| sk3 = sk6
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_19
| spl0_21 ),
inference(resolution,[],[f9142,f139]) ).
fof(f9197,plain,
( ~ frontsegP(sk3,sk6)
| ~ ssList(sk6)
| sk3 = sk6
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_19
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f9196,f202]) ).
fof(f9200,plain,
( ~ frontsegP(sk3,sk6)
| sk3 = sk6
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_19
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f9197,f207]) ).
fof(f9318,definition,
( spl0_27
<=> sk3 = sk6 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f9320,plain,
( sk3 = sk6
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f9318]) ).
fof(f9322,definition,
( spl0_28
<=> frontsegP(sk3,sk6) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f9325,plain,
( spl0_27
| ~ spl0_28
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_19
| spl0_21 ),
inference(avatar_split_clause,[],[f9200,f4420,f2978,f906,f316,f290,f264,f9322,f9318]) ).
fof(f9331,plain,
( ! [X0] :
( frontsegP(sk3,X0)
| ~ ssList(X0)
| ~ frontsegP(app(sk6,cons(sk5,nil)),X0) )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1163,f907]) ).
fof(f9332,plain,
( ! [X0] :
( ~ frontsegP(app(sk6,cons(sk9,nil)),X0)
| frontsegP(sk3,X0)
| ~ ssList(X0) )
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15 ),
inference(forward_demodulation,[],[f9331,f7081]) ).
fof(f9333,plain,
( ! [X0] :
( ~ frontsegP(app(sk6,sk3),X0)
| frontsegP(sk3,X0)
| ~ ssList(X0) )
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15 ),
inference(forward_demodulation,[],[f9332,f5746]) ).
fof(f9337,plain,
( frontsegP(sk3,sk6)
| ~ ssList(sk6)
| ~ ssList(sk6)
| ~ ssList(sk3)
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15 ),
inference(resolution,[],[f9333,f904]) ).
fof(f9345,plain,
( frontsegP(sk3,sk6)
| ~ ssList(sk6)
| ~ ssList(sk3)
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15 ),
inference(duplicate_literal_removal,[],[f9337]) ).
fof(f9355,plain,
( frontsegP(sk3,sk6)
| ~ ssList(sk3)
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f9345,f207]) ).
fof(f9356,plain,
( frontsegP(sk3,sk6)
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f9355,f202]) ).
fof(f9363,plain,
( spl0_28
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f9356,f906,f316,f290,f264,f9322]) ).
fof(f9388,plain,
( frontsegP(sk3,app(sk3,sk3))
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_27 ),
inference(superposition,[],[f7404,f9320]) ).
fof(f12449,plain,
( frontsegP(sk3,cons(sk9,sk3))
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_27 ),
inference(superposition,[],[f9388,f6536]) ).
fof(f12700,plain,
( ~ ssList(sk3)
| frontsegP(nil,sk3)
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_27 ),
inference(resolution,[],[f12449,f7272]) ).
fof(f12704,plain,
( frontsegP(nil,sk3)
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f12700,f202]) ).
fof(f12711,plain,
( ~ ssList(sk3)
| nil = sk3
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_27 ),
inference(resolution,[],[f12704,f84]) ).
fof(f12714,plain,
( nil = sk3
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f12711,f202]) ).
fof(f12716,plain,
( $false
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f12714,f291]) ).
fof(f12717,plain,
( ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f12716]) ).
fof(f12734,plain,
( sk3 = app(app(nil,cons(sk5,nil)),sk7)
| ~ spl0_21 ),
inference(superposition,[],[f228,f4422]) ).
fof(f12767,plain,
( sk3 = app(app(nil,cons(sk9,nil)),sk7)
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_demodulation,[],[f12734,f7081]) ).
fof(f12770,plain,
( sk3 = app(app(nil,sk3),sk7)
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_demodulation,[],[f12767,f5746]) ).
fof(f12773,plain,
( sk3 = app(sk3,sk7)
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_demodulation,[],[f12770,f382]) ).
fof(f12798,plain,
( sk7 = tl(sk3)
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_21 ),
inference(superposition,[],[f6383,f12773]) ).
fof(f12825,plain,
( nil = sk7
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_demodulation,[],[f12798,f6079]) ).
fof(f12831,plain,
( $false
| ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_21
| spl0_23 ),
inference(forward_subsumption_resolution,[],[f12825,f4442]) ).
fof(f12832,plain,
( ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_21
| spl0_23 ),
inference(avatar_contradiction_clause,[],[f12831]) ).
fof(f12833,plain,
( memberP(nil,sk8)
| ~ spl0_4
| ~ spl0_21 ),
inference(forward_demodulation,[],[f275,f4422]) ).
fof(f12910,plain,
( ~ ssItem(sk8)
| ~ spl0_4
| ~ spl0_21 ),
inference(resolution,[],[f12833,f71]) ).
fof(f12913,plain,
( $false
| ~ spl0_4
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f12910,f211]) ).
fof(f12914,plain,
( ~ spl0_4
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f12913]) ).
fof(f13052,plain,
( segmentP(nil,cons(sk5,nil))
| ~ spl0_7
| ~ spl0_20 ),
inference(superposition,[],[f2984,f292]) ).
fof(f13331,plain,
( nil = sk3
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f217,f265]) ).
fof(f13332,plain,
( $false
| spl0_2
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f13331,f291]) ).
fof(f13333,plain,
( spl0_2
| spl0_7 ),
inference(avatar_contradiction_clause,[],[f13332]) ).
fof(f13336,plain,
( $false
| spl0_15
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f950,f2979]) ).
fof(f13337,plain,
( spl0_15
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f13336]) ).
fof(f14159,plain,
( ~ ssList(cons(sk5,nil))
| nil = cons(sk5,nil)
| ~ spl0_7
| ~ spl0_20 ),
inference(resolution,[],[f13052,f80]) ).
fof(f14162,plain,
( nil = cons(sk5,nil)
| ~ spl0_7
| ~ spl0_19
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f14159,f2979]) ).
fof(f14164,plain,
( $false
| ~ spl0_7
| ~ spl0_19
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f14162,f3139]) ).
fof(f14165,plain,
( ~ spl0_7
| ~ spl0_19
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f14164]) ).
cnf(s2,plain,
( spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f276]) ).
cnf(s4,plain,
( spl0_1
| spl0_6 ),
inference(sat_conversion,[],[f286]) ).
cnf(s5,plain,
( ~ spl0_1
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f297]) ).
cnf(s6,plain,
( spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f321]) ).
cnf(s16,plain,
( ~ spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f2985]) ).
cnf(s18,plain,
spl0_19,
inference(sat_conversion,[],[f3069]) ).
cnf(s21,plain,
( ~ spl0_3
| ~ spl0_23 ),
inference(sat_conversion,[],[f4470]) ).
cnf(s22,plain,
( spl0_1
| ~ spl0_2
| ~ spl0_6
| ~ spl0_10 ),
inference(sat_conversion,[],[f5745]) ).
cnf(s23,plain,
( ~ spl0_2
| ~ spl0_8 ),
inference(sat_conversion,[],[f5788]) ).
cnf(s27,plain,
( ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_19
| spl0_21
| spl0_27
| ~ spl0_28 ),
inference(sat_conversion,[],[f9325]) ).
cnf(s29,plain,
( ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| spl0_28 ),
inference(sat_conversion,[],[f9363]) ).
cnf(s30,plain,
( ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_27 ),
inference(sat_conversion,[],[f12717]) ).
cnf(s31,plain,
( ~ spl0_2
| spl0_7
| ~ spl0_9
| ~ spl0_15
| ~ spl0_21
| spl0_23 ),
inference(sat_conversion,[],[f12832]) ).
cnf(s32,plain,
( ~ spl0_4
| ~ spl0_21 ),
inference(sat_conversion,[],[f12914]) ).
cnf(s36,plain,
( spl0_2
| spl0_7 ),
inference(sat_conversion,[],[f13333]) ).
cnf(s37,plain,
( spl0_15
| ~ spl0_19 ),
inference(sat_conversion,[],[f13337]) ).
cnf(s40,plain,
( ~ spl0_7
| ~ spl0_19
| ~ spl0_20 ),
inference(sat_conversion,[],[f14165]) ).
cnf(s41,plain,
spl0_15,
inference(rat,[],[s37,s18]) ).
cnf(s42,plain,
spl0_20,
inference(rat,[],[s16,s18]) ).
cnf(s43,plain,
~ spl0_7,
inference(rat,[],[s40,s18,s42]) ).
cnf(s44,plain,
spl0_2,
inference(rat,[],[s36,s43]) ).
cnf(s45,plain,
~ spl0_8,
inference(rat,[],[s23,s44]) ).
cnf(s47,plain,
~ spl0_1,
inference(rat,[],[s5,s45,s43]) ).
cnf(s49,plain,
spl0_6,
inference(rat,[],[s4,s47]) ).
cnf(s50,plain,
~ spl0_10,
inference(rat,[],[s22,s47,s44,s49]) ).
cnf(s51,plain,
spl0_9,
inference(rat,[],[s6,s50]) ).
cnf(s52,plain,
~ spl0_27,
inference(rat,[],[s30,s44,s41,s43,s51]) ).
cnf(s53,plain,
spl0_28,
inference(rat,[],[s29,s44,s41,s43,s51]) ).
cnf(s54,plain,
spl0_21,
inference(rat,[],[s27,s53,s52,s44,s18,s41,s43,s51]) ).
cnf(s56,plain,
~ spl0_4,
inference(rat,[],[s32,s54]) ).
cnf(s57,plain,
spl0_23,
inference(rat,[],[s31,s51,s44,s41,s43,s54]) ).
cnf(s58,plain,
~ spl0_3,
inference(rat,[],[s21,s57]) ).
cnf(s60,plain,
$false,
inference(rat,[],[s2,s56,s58]) ).
fof(f14166,plain,
$false,
inference(avatar_sat_refutation,[],[s60]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC295-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.10/0.19 % Computer : n002.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Mon Sep 28 08:58:22 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 Running first-order model finding
% 0.10/0.22 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
% 8.03/1.58 % (222410)Will run a generic schedule for satisfiability detection.
% 8.03/1.58 % (222418)dis+10_1_sil=32000:sp=arity:random_seed=1623887606:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.03/1.58 % (222416)% WARNING: option uhcvi not known.
% 8.03/1.58 % (222415)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3444922068_2999 on theBenchmark for (2999ds/0Mi)
% 8.03/1.58 % (222416)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2898125185:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.03/1.58 % (222417)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4088997760:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.03/1.58 % (222419)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=609425320:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.03/1.58 % (222420)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2155273939:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.03/1.58 % (222421)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2879938195:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.03/1.59 % TRYING [1]
% 8.03/1.59 % TRYING [2]
% 8.03/1.59 % TRYING [3]
% 8.03/1.59 % (222418)Instruction limit reached!
% 8.03/1.59 % (222418)------------------------------
% 8.03/1.59 % (222418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.03/1.59 % (222418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.03/1.59 % (222418)CaDiCaL version: 2.1.3
% 8.03/1.59 % (222418)Termination reason: Instruction limit
% 8.03/1.59 % (222418)Termination phase: Saturation
% 8.03/1.59 % (222418)Time elapsed: 0.035 s
% 8.03/1.59 % (222418)Peak memory usage: 13 MB
% 8.03/1.59 % (222418)Instructions burned: 106 (million)
% 8.03/1.59 % TRYING [4]
% 8.03/1.59 % (222429)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4119620704:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 8.03/1.59 % TRYING [1]
% 8.03/1.59 % TRYING [2]
% 8.03/1.59 % TRYING [3]
% 8.03/1.59 % (222419)Instruction limit reached!
% 8.03/1.59 % (222419)------------------------------
% 8.03/1.59 % (222419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.03/1.59 % (222419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.03/1.59 % (222419)CaDiCaL version: 2.1.3
% 8.03/1.59 % (222419)Termination reason: Instruction limit
% 8.03/1.59 % (222419)Termination phase: Saturation
% 8.03/1.59 % (222419)Time elapsed: 0.060 s
% 8.03/1.59 % (222419)Peak memory usage: 13 MB
% 8.03/1.59 % (222419)Instructions burned: 116 (million)
% 8.03/1.59 % TRYING [4]
% 8.03/1.59 % (222420)Instruction limit reached!
% 8.03/1.59 % (222420)------------------------------
% 8.03/1.59 % (222420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.03/1.59 % (222420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.03/1.59 % (222420)CaDiCaL version: 2.1.3
% 8.03/1.59 % (222420)Termination reason: Instruction limit
% 8.03/1.59 % (222420)Termination phase: Saturation
% 8.03/1.59 % (222420)Time elapsed: 0.066 s
% 8.03/1.59 % (222420)Peak memory usage: 14 MB
% 8.03/1.59 % (222420)Instructions burned: 132 (million)
% 8.03/1.59 % (222431)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1739617905:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 8.03/1.59 % (222432)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=2629226813:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.03/1.59 % TRYING [5]
% 8.03/1.59 % (222421)Instruction limit reached!
% 8.03/1.59 % (222421)------------------------------
% 8.03/1.59 % (222421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.03/1.59 % (222421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.03/1.59 % (222421)CaDiCaL version: 2.1.3
% 8.03/1.59 % (222421)Termination reason: Instruction limit
% 8.03/1.59 % (222421)Termination phase: Saturation
% 8.03/1.59 % (222421)Time elapsed: 0.098 s
% 8.03/1.59 % (222421)Peak memory usage: 14 MB
% 8.03/1.59 % (222421)Instructions burned: 161 (million)
% 8.03/1.59 % TRYING [5]
% 8.03/1.59 % (222435)ott-21_1_sil=16000:fs=off:random_seed=3219286550:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.03/1.59 % (222431)Instruction limit reached!
% 8.03/1.59 % (222431)------------------------------
% 8.03/1.59 % (222431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.03/1.59 % (222431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.03/1.59 % (222431)CaDiCaL version: 2.1.3
% 8.03/1.59 % (222431)Termination reason: Instruction limit
% 8.03/1.59 % (222431)Termination phase: Saturation
% 8.03/1.59 % (222431)Time elapsed: 0.067 s
% 8.03/1.59 % (222431)Peak memory usage: 13 MB
% 8.03/1.59 % (222431)Instructions burned: 131 (million)
% 8.03/1.59 % (222437)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3961597981:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 8.03/1.59 % TRYING [6]
% 8.03/1.59 % (222429)Instruction limit reached!
% 8.03/1.59 % (222429)------------------------------
% 8.03/1.59 % (222429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.03/1.59 % (222429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.03/1.59 % (222429)CaDiCaL version: 2.1.3
% 8.03/1.59 % (222429)Termination reason: Instruction limit
% 8.03/1.59 % (222429)Termination phase: Finite model building constraint generation
% 8.03/1.59 % (222429)Time elapsed: 0.150 s
% 8.03/1.59 % (222429)Peak memory usage: 34 MB
% 8.03/1.59 % (222429)Instructions burned: 722 (million)
% 8.03/1.59 % (222439)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=598518600:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 8.03/1.59 % TRYING [1]
% 8.03/1.59 % (222435)Instruction limit reached!
% 8.03/1.59 % (222435)------------------------------
% 8.03/1.59 % (222435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.03/1.59 % TRYING [2]
% 8.03/1.59 % (222435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.03/1.59 % (222435)CaDiCaL version: 2.1.3
% 8.03/1.59 % (222435)Termination reason: Instruction limit
% 8.03/1.59 % (222435)Termination phase: Saturation
% 8.03/1.59 % (222435)Time elapsed: 0.089 s
% 8.03/1.59 % (222435)Peak memory usage: 13 MB
% 8.03/1.59 % (222435)Instructions burned: 181 (million)
% 8.03/1.59 % TRYING [3]
% 8.03/1.59 % (222441)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4115436424:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 8.03/1.59 % TRYING [4]
% 8.03/1.59 % TRYING [6]
% 8.03/1.59 % TRYING [5]
% 8.03/1.59 % (222439)Instruction limit reached!
% 8.03/1.59 % (222439)------------------------------
% 8.03/1.59 % (222439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.03/1.59 % (222439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.03/1.59 % (222439)CaDiCaL version: 2.1.3
% 8.03/1.59 % (222439)Termination reason: Instruction limit
% 8.03/1.59 % (222439)Termination phase: Finite model building SAT solving
% 8.03/1.59 % (222439)Time elapsed: 0.178 s
% 8.03/1.59 % (222439)Peak memory usage: 22 MB
% 8.03/1.59 % (222439)Instructions burned: 867 (million)
% 8.03/1.59 % (222443)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1816068598:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 8.03/1.59 % TRYING [14]
% 8.03/1.59 % (222437)Instruction limit reached!
% 8.03/1.59 % (222437)------------------------------
% 8.03/1.59 % (222437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.03/1.59 % (222437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.03/1.59 % (222437)CaDiCaL version: 2.1.3
% 8.03/1.59 % (222437)Termination reason: Instruction limit
% 8.03/1.59 % (222437)Termination phase: Saturation
% 8.03/1.59 % (222437)Time elapsed: 0.303 s
% 8.03/1.59 % (222437)Peak memory usage: 14 MB
% 8.03/1.59 % (222437)Instructions burned: 478 (million)
% 8.03/1.59 % (222432)Instruction limit reached!
% 8.03/1.59 % (222432)------------------------------
% 8.03/1.59 % (222432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.03/1.59 % (222432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.03/1.59 % (222432)CaDiCaL version: 2.1.3
% 8.03/1.59 % (222432)Termination reason: Instruction limit
% 8.03/1.59 % (222432)Termination phase: Saturation
% 8.03/1.59 % (222432)Time elapsed: 0.390 s
% 8.03/1.59 % (222432)Peak memory usage: 21 MB
% 8.03/1.59 % (222432)Instructions burned: 685 (million)
% 8.03/1.59 % (222445)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=192854654: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)
% 8.03/1.59 % (222446)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3935851816:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 8.03/1.59 % (222443)Instruction limit reached!
% 8.03/1.59 % (222443)------------------------------
% 8.03/1.59 % (222443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.03/1.59 % (222443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.03/1.59 % (222443)CaDiCaL version: 2.1.3
% 8.03/1.59 % (222443)Termination reason: Instruction limit
% 8.03/1.59 % (222443)Termination phase: Finite model building constraint generation
% 8.03/1.59 % (222443)Time elapsed: 0.181 s
% 8.03/1.59 % (222443)Peak memory usage: 73 MB
% 8.03/1.59 % (222443)Instructions burned: 894 (million)
% 8.03/1.59 % (222449)fmb+10_1_sil=64000:random_seed=2468015251:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 8.03/1.59 % TRYING [1]
% 8.03/1.59 % TRYING [2]
% 8.03/1.59 % TRYING [3]
% 8.03/1.59 % TRYING [4]
% 8.03/1.59 % TRYING [5]
% 8.03/1.59 % TRYING [7]
% 8.03/1.59 % (222445)Instruction limit reached!
% 8.03/1.59 % (222445)------------------------------
% 8.03/1.59 % (222445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.03/1.59 % (222445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.03/1.59 % (222445)CaDiCaL version: 2.1.3
% 8.03/1.59 % (222445)Termination reason: Instruction limit
% 8.03/1.59 % (222445)Termination phase: Saturation
% 8.03/1.59 % (222445)Time elapsed: 0.378 s
% 8.03/1.59 % (222445)Peak memory usage: 22 MB
% 8.03/1.59 % (222445)Instructions burned: 694 (million)
% 8.03/1.59 % (222451)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1761813142:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 8.03/1.59 % TRYING [20]
% 8.03/1.59 % (222441)Instruction limit reached!
% 8.03/1.59 % (222441)------------------------------
% 8.03/1.59 % (222441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.03/1.59 % (222441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.03/1.59 % (222441)CaDiCaL version: 2.1.3
% 8.03/1.59 % (222441)Termination reason: Instruction limit
% 8.03/1.59 % (222441)Termination phase: Saturation
% 8.03/1.59 % (222441)Time elapsed: 0.688 s
% 8.03/1.59 % (222441)Peak memory usage: 28 MB
% 8.03/1.59 % (222441)Instructions burned: 1179 (million)
% 8.03/1.59 % TRYING [6]
% 8.03/1.59 % (222453)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=145168512:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 8.03/1.59 % TRYING [8]
% 8.03/1.59 % (222446)Instruction limit reached!
% 8.03/1.59 % (222446)------------------------------
% 8.03/1.59 % (222446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.03/1.59 % (222446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.03/1.59 % (222446)CaDiCaL version: 2.1.3
% 8.03/1.59 % (222446)Termination reason: Instruction limit
% 8.03/1.59 % (222446)Termination phase: Saturation
% 8.03/1.59 % (222446)Time elapsed: 0.463 s
% 8.03/1.59 % (222446)Peak memory usage: 20 MB
% 8.03/1.59 % (222446)Instructions burned: 880 (million)
% 8.03/1.59 % (222455)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4031570193:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 8.03/1.59 % (222453)Instruction limit reached!
% 8.03/1.59 % (222453)------------------------------
% 8.03/1.59 % (222453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.03/1.59 % (222453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.03/1.59 % (222453)CaDiCaL version: 2.1.3
% 8.03/1.59 % (222453)Termination reason: Instruction limit
% 8.03/1.59 % (222453)Termination phase: Finite model building constraint generation
% 8.03/1.59 % (222453)Time elapsed: 0.333 s
% 8.03/1.59 % (222453)Peak memory usage: 79 MB
% 8.03/1.59 % (222453)Instructions burned: 922 (million)
% 8.03/1.59 % (222455) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-222410-222455"...
% 8.03/1.59 % (222455)...printing done.
% 8.03/1.59 % (222455)Refutation found. Thanks to Tanya!
% 8.03/1.59 % SZS status Unsatisfiable for theBenchmark
% 8.03/1.59 % SZS output start Proof for theBenchmark
% See solution above
% 8.03/1.59 % (222455)------------------------------
% 8.03/1.59 % (222455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.03/1.59 % (222455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.03/1.59 % (222455)CaDiCaL version: 2.1.3
% 8.03/1.59 % (222455)Termination reason: Refutation
% 8.03/1.59 % (222455)Time elapsed: 0.301 s
% 8.03/1.59 % (222455)Peak memory usage: 17 MB
% 8.03/1.59 % (222455)Instructions burned: 542 (million)
% 8.03/1.59 % (222410)Success in time 1.355 s
% 8.03/1.59 % Vampire exiting
%------------------------------------------------------------------------------