%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC285-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:23 PM UTC 2026
% Result : Unsatisfiable 17.17s 2.75s
% Output : Refutation 17.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 57
% Syntax : Number of formulae : 251 ( 34 unt; 16 def)
% Number of atoms : 863 ( 80 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 1198 ( 586 ~; 596 |; 0 &)
% ( 16 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 17 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 8 con; 0-2 aty)
% Number of variables : 134 ( 0 sgn 134 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f12,axiom,
! [X0] : ssItem(skaf83(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause12) ).
fof(f13,axiom,
! [X0] : ssList(skaf82(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause13) ).
fof(f47,axiom,
! [X0] : ssItem(skaf44(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause47) ).
fof(f56,axiom,
! [X0] :
( segmentP(X0,nil)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause56) ).
fof(f62,axiom,
! [X0] :
( leq(X0,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause62) ).
fof(f71,axiom,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause71) ).
fof(f72,axiom,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f74,axiom,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause74) ).
fof(f75,axiom,
! [X0] :
( ssList(tl(X0))
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause75) ).
fof(f80,axiom,
! [X0] :
( ~ segmentP(nil,X0)
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause80) ).
fof(f85,axiom,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause86) ).
fof(f96,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| tl(cons(X0,X1)) = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause96) ).
fof(f97,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| hd(cons(X0,X1)) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause97) ).
fof(f100,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| cons(X0,X1) != X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause99) ).
fof(f101,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| neq(X1,X0)
| X1 = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause100) ).
fof(f102,plain,
! [X0,X1] :
( neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0)
| X0 = X1 ),
inference(reorient_equations,[],[f101]) ).
fof(f103,axiom,
! [X0] :
( ~ singletonP(X0)
| ~ ssList(X0)
| cons(skaf44(X0),nil) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause101) ).
fof(f112,axiom,
! [X0] :
( ~ ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause109) ).
fof(f134,axiom,
! [X0,X1] :
( ~ segmentP(X0,X1)
| ~ segmentP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X1 = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause127) ).
fof(f135,plain,
! [X0,X1] :
( ~ segmentP(X1,X0)
| ~ segmentP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| X0 = X1 ),
inference(reorient_equations,[],[f134]) ).
fof(f149,axiom,
! [X2,X0,X1] :
( X0 != X1
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0)
| memberP(cons(X1,X2),X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause138) ).
fof(f151,axiom,
! [X2,X0,X1] :
( memberP(app(X0,X2),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ memberP(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause140) ).
fof(f152,axiom,
! [X2,X0,X1] :
( memberP(app(X2,X0),X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ memberP(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause141) ).
fof(f173,axiom,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X2 = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause161) ).
fof(f174,plain,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X0 = X2 ),
inference(reorient_equations,[],[f173]) ).
fof(f187,axiom,
! [X2,X3,X0,X1] :
( app(app(X0,X1),X2) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| segmentP(X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause173) ).
fof(f189,axiom,
! [X2,X3,X0,X1] :
( app(X0,cons(X1,X2)) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(X3)
| memberP(X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause175) ).
fof(f193,axiom,
! [X2,X3,X0,X1,X4] :
( app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(X4)
| ~ ssList(X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(f202,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_3) ).
fof(f203,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_4) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
segmentP(sk4,sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
ssList(sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_10) ).
fof(f210,negated_conjecture,
app(app(sk6,cons(sk5,nil)),sk7) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).
fof(f211,plain,
sk1 = app(app(sk6,cons(sk5,nil)),sk7),
inference(reorient_equations,[],[f210]) ).
fof(f212,negated_conjecture,
ssItem(sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_12) ).
fof(f213,negated_conjecture,
( memberP(sk6,sk8)
| memberP(sk7,sk8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_13) ).
fof(f214,negated_conjecture,
( memberP(sk6,sk8)
| ~ leq(sk5,sk8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_14) ).
fof(f215,negated_conjecture,
( ~ leq(sk8,sk5)
| memberP(sk7,sk8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_15) ).
fof(f216,negated_conjecture,
( ~ leq(sk8,sk5)
| ~ leq(sk5,sk8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_16) ).
fof(f217,negated_conjecture,
( singletonP(sk3)
| ~ neq(sk4,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_17) ).
fof(f220,plain,
sk3 = app(app(sk6,cons(sk5,nil)),sk7),
inference(definition_unfolding,[],[f211,f205]) ).
fof(f230,plain,
! [X2,X1] :
( ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X1)
| memberP(cons(X1,X2),X1) ),
inference(equality_resolution,[],[f149]) ).
fof(f235,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(f236,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(f238,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(f247,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X2) ),
inference(duplicate_literal_removal,[],[f230]) ).
fof(f252,definition,
( spl0_1
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f254,plain,
( ~ neq(sk4,nil)
| spl0_1 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f256,definition,
( spl0_2
<=> singletonP(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f258,plain,
( singletonP(sk3)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f259,plain,
( ~ spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f217,f256,f252]) ).
fof(f261,definition,
( spl0_3
<=> memberP(sk7,sk8) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f262,plain,
( ~ memberP(sk7,sk8)
| spl0_3 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f263,plain,
( memberP(sk7,sk8)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f265,definition,
( spl0_4
<=> memberP(sk6,sk8) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f267,plain,
( memberP(sk6,sk8)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f268,plain,
( spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f213,f265,f261]) ).
fof(f270,definition,
( spl0_5
<=> leq(sk5,sk8) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f271,plain,
( leq(sk5,sk8)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f272,plain,
( ~ leq(sk5,sk8)
| spl0_5 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f273,plain,
( ~ spl0_5
| spl0_4 ),
inference(avatar_split_clause,[],[f214,f265,f270]) ).
fof(f275,definition,
( spl0_6
<=> ! [X1] : ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f276,plain,
( ! [X1] : ssItem(X1)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f278,definition,
( spl0_7
<=> ! [X0] :
( ~ ssList(X0)
| duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f279,plain,
( ! [X0] :
( duplicatefreeP(X0)
| ~ ssList(X0) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f280,plain,
( spl0_6
| spl0_7 ),
inference(avatar_split_clause,[],[f72,f278,f275]) ).
fof(f499,plain,
( ~ ssList(sk4)
| ~ ssList(nil)
| nil = sk4
| spl0_1 ),
inference(resolution,[],[f102,f254]) ).
fof(f504,plain,
( ~ ssList(nil)
| nil = sk4
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f499,f203]) ).
fof(f505,plain,
( nil = sk4
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f504,f8]) ).
fof(f644,plain,
( sk7 = cons(skaf83(sk7),skaf82(sk7))
| nil = sk7 ),
inference(resolution,[],[f112,f209]) ).
fof(f691,definition,
( spl0_10
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f692,plain,
( nil != sk7
| spl0_10 ),
inference(avatar_component_clause,[],[f691]) ).
fof(f693,plain,
( nil = sk7
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f691]) ).
fof(f821,plain,
( ~ segmentP(sk3,sk4)
| ~ ssList(sk4)
| ~ ssList(sk3)
| sk3 = sk4 ),
inference(resolution,[],[f135,f206]) ).
fof(f827,plain,
( ~ segmentP(sk3,sk4)
| ~ ssList(sk3)
| sk3 = sk4 ),
inference(forward_subsumption_resolution,[],[f821,f203]) ).
fof(f829,plain,
( ~ segmentP(sk3,sk4)
| sk3 = sk4 ),
inference(forward_subsumption_resolution,[],[f827,f202]) ).
fof(f1193,definition,
( spl0_14
<=> sk3 = sk4 ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f1195,plain,
( sk3 = sk4
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f1193]) ).
fof(f1197,definition,
( spl0_15
<=> segmentP(sk3,sk4) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f1199,plain,
( ~ segmentP(sk3,sk4)
| spl0_15 ),
inference(avatar_component_clause,[],[f1197]) ).
fof(f1200,plain,
( spl0_14
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f829,f1197,f1193]) ).
fof(f2515,plain,
( segmentP(sk3,cons(sk5,nil))
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk3)
| ~ ssList(sk7) ),
inference(superposition,[],[f235,f220]) ).
fof(f2522,plain,
( segmentP(sk3,cons(sk5,nil))
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk3)
| ~ ssList(sk7) ),
inference(forward_subsumption_resolution,[],[f2515,f208]) ).
fof(f2533,plain,
( segmentP(sk3,cons(sk5,nil))
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7) ),
inference(forward_subsumption_resolution,[],[f2522,f202]) ).
fof(f2541,plain,
( segmentP(sk3,cons(sk5,nil))
| ~ ssList(cons(sk5,nil)) ),
inference(forward_subsumption_resolution,[],[f2533,f209]) ).
fof(f3151,definition,
( spl0_16
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f3152,plain,
( ssList(cons(sk5,nil))
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f3151]) ).
fof(f3153,plain,
( ~ ssList(cons(sk5,nil))
| spl0_16 ),
inference(avatar_component_clause,[],[f3151]) ).
fof(f3155,definition,
( spl0_17
<=> segmentP(sk3,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f3157,plain,
( segmentP(sk3,cons(sk5,nil))
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f3155]) ).
fof(f3158,plain,
( ~ spl0_16
| spl0_17 ),
inference(avatar_split_clause,[],[f2541,f3155,f3151]) ).
fof(f3171,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| spl0_16 ),
inference(resolution,[],[f86,f3153]) ).
fof(f3188,plain,
( ~ ssItem(sk5)
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f3171,f8]) ).
fof(f3189,plain,
( $false
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f3188,f207]) ).
fof(f3190,plain,
spl0_16,
inference(avatar_contradiction_clause,[],[f3189]) ).
fof(f3192,plain,
( cons(sk5,nil) = app(nil,cons(sk5,nil))
| ~ spl0_16 ),
inference(resolution,[],[f3152,f74]) ).
fof(f3229,plain,
! [X0] :
( ~ ssList(X0)
| cons(sk5,X0) != X0 ),
inference(resolution,[],[f100,f207]) ).
fof(f3263,plain,
nil != cons(sk5,nil),
inference(resolution,[],[f3229,f8]) ).
fof(f3324,plain,
! [X0] :
( ~ ssList(X0)
| tl(cons(sk5,X0)) = X0 ),
inference(resolution,[],[f96,f207]) ).
fof(f3409,plain,
! [X0,X1] :
( ~ ssItem(X1)
| ~ ssList(X0)
| hd(cons(X1,tl(X0))) = X1
| nil = X0 ),
inference(resolution,[],[f97,f75]) ).
fof(f3609,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,f220]) ).
fof(f3615,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssItem(X0)
| ~ memberP(app(sk6,cons(sk5,nil)),X0) ),
inference(forward_subsumption_resolution,[],[f3609,f209]) ).
fof(f3639,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssList(sk7)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssItem(X0)
| ~ memberP(sk7,X0) ),
inference(superposition,[],[f152,f220]) ).
fof(f3645,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssItem(X0)
| ~ memberP(sk7,X0) ),
inference(forward_subsumption_resolution,[],[f3639,f209]) ).
fof(f4050,plain,
nil = tl(cons(sk5,nil)),
inference(resolution,[],[f3324,f8]) ).
fof(f4267,definition,
( spl0_18
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f4269,plain,
( nil = sk4
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f4267]) ).
fof(f4282,plain,
( ~ segmentP(sk3,nil)
| spl0_15
| ~ spl0_18 ),
inference(superposition,[],[f1199,f4269]) ).
fof(f4323,plain,
( ~ leq(sk8,sk5)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f215,f262]) ).
fof(f4414,plain,
( ~ ssList(sk3)
| spl0_15
| ~ spl0_18 ),
inference(resolution,[],[f4282,f56]) ).
fof(f4417,plain,
( $false
| spl0_15
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f4414,f202]) ).
fof(f4418,plain,
( spl0_15
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f4417]) ).
fof(f4421,plain,
( nil = sk3
| ~ spl0_14
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1195,f4269]) ).
fof(f4440,plain,
( segmentP(nil,cons(sk5,nil))
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18 ),
inference(superposition,[],[f3157,f4421]) ).
fof(f4458,definition,
( spl0_20
<=> ssList(app(sk6,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f4459,plain,
( ssList(app(sk6,cons(sk5,nil)))
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f4458]) ).
fof(f4460,plain,
( ~ ssList(app(sk6,cons(sk5,nil)))
| spl0_20 ),
inference(avatar_component_clause,[],[f4458]) ).
fof(f4466,plain,
( ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| spl0_20 ),
inference(resolution,[],[f4460,f85]) ).
fof(f4467,plain,
( ~ ssList(cons(sk5,nil))
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f4466,f208]) ).
fof(f4468,plain,
( $false
| ~ spl0_16
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f4467,f3152]) ).
fof(f4469,plain,
( ~ spl0_16
| spl0_20 ),
inference(avatar_contradiction_clause,[],[f4468]) ).
fof(f4497,plain,
( ~ ssList(cons(sk5,nil))
| nil = cons(sk5,nil)
| ~ spl0_14
| ~ spl0_17
| ~ spl0_18 ),
inference(resolution,[],[f4440,f80]) ).
fof(f4500,plain,
( nil = cons(sk5,nil)
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f4497,f3152]) ).
fof(f4502,plain,
( $false
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f4500,f3263]) ).
fof(f4503,plain,
( ~ spl0_14
| ~ spl0_16
| ~ spl0_17
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f4502]) ).
fof(f4509,plain,
( spl0_18
| spl0_1 ),
inference(avatar_split_clause,[],[f505,f252,f4267]) ).
fof(f4510,plain,
( ~ ssList(sk3)
| sk3 = cons(skaf44(sk3),nil)
| ~ spl0_2 ),
inference(resolution,[],[f258,f103]) ).
fof(f4511,plain,
( sk3 = cons(skaf44(sk3),nil)
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f4510,f202]) ).
fof(f4531,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssList(nil)
| ~ ssItem(skaf44(sk3))
| ~ ssItem(X0)
| memberP(nil,X0)
| skaf44(sk3) = X0 )
| ~ spl0_2 ),
inference(superposition,[],[f174,f4511]) ).
fof(f4581,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(skaf44(sk3))
| ~ ssItem(X0)
| memberP(nil,X0)
| skaf44(sk3) = X0 )
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f4531,f8]) ).
fof(f4609,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(X0)
| memberP(nil,X0)
| skaf44(sk3) = X0 )
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f4581,f47]) ).
fof(f4612,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(X0)
| skaf44(sk3) = X0 )
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f4609,f71]) ).
fof(f5885,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk7,X0) )
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f3645,f4459]) ).
fof(f7259,plain,
( ! [X0] :
( ~ memberP(app(sk6,cons(sk5,nil)),X0)
| ~ ssItem(X0)
| memberP(sk3,X0) )
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f3615,f4459]) ).
fof(f7264,plain,
( ! [X0] :
( ~ ssItem(X0)
| memberP(sk3,X0)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk6)
| ~ ssItem(X0)
| ~ memberP(sk6,X0) )
| ~ spl0_20 ),
inference(resolution,[],[f7259,f151]) ).
fof(f7265,plain,
( ~ ssItem(sk5)
| memberP(sk3,sk5)
| ~ ssList(sk6)
| ~ ssItem(sk5)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(nil)
| ~ spl0_20 ),
inference(resolution,[],[f7259,f236]) ).
fof(f7266,plain,
( ~ ssItem(sk5)
| memberP(sk3,sk5)
| ~ ssList(sk6)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(nil)
| ~ spl0_20 ),
inference(duplicate_literal_removal,[],[f7265]) ).
fof(f7267,plain,
( ! [X0] :
( ~ ssItem(X0)
| memberP(sk3,X0)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk6)
| ~ memberP(sk6,X0) )
| ~ spl0_20 ),
inference(duplicate_literal_removal,[],[f7264]) ).
fof(f7269,plain,
( memberP(sk3,sk5)
| ~ ssList(sk6)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(nil)
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f7266,f207]) ).
fof(f7270,plain,
( ! [X0] :
( ~ ssItem(X0)
| memberP(sk3,X0)
| ~ ssList(sk6)
| ~ memberP(sk6,X0) )
| ~ spl0_16
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f7267,f3152]) ).
fof(f7272,plain,
( memberP(sk3,sk5)
| ~ ssList(app(sk6,cons(sk5,nil)))
| ~ ssList(nil)
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f7269,f208]) ).
fof(f7273,plain,
( ! [X0] :
( ~ ssItem(X0)
| memberP(sk3,X0)
| ~ memberP(sk6,X0) )
| ~ spl0_16
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f7270,f208]) ).
fof(f7275,plain,
( memberP(sk3,sk5)
| ~ ssList(nil)
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f7272,f4459]) ).
fof(f7276,plain,
( memberP(sk3,sk5)
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f7275,f8]) ).
fof(f19987,plain,
( ! [X0] :
( ~ ssItem(X0)
| hd(cons(X0,tl(cons(sk5,nil)))) = X0
| nil = cons(sk5,nil) )
| ~ spl0_16 ),
inference(resolution,[],[f3409,f3152]) ).
fof(f19994,plain,
( ! [X0] :
( ~ ssItem(X0)
| hd(cons(X0,tl(cons(sk5,nil)))) = X0 )
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f19987,f3263]) ).
fof(f19997,plain,
( ! [X0] :
( hd(cons(X0,nil)) = X0
| ~ ssItem(X0) )
| ~ spl0_16 ),
inference(forward_demodulation,[],[f19994,f4050]) ).
fof(f20179,plain,
( ! [X0,X1] :
( ~ ssList(X1)
| hd(cons(X0,X1)) = X0 )
| ~ spl0_6 ),
inference(resolution,[],[f276,f97]) ).
fof(f20561,plain,
( ! [X0] : hd(cons(X0,sk7)) = X0
| ~ spl0_6 ),
inference(resolution,[],[f20179,f209]) ).
fof(f20562,plain,
( ! [X0] : hd(cons(X0,nil)) = X0
| ~ spl0_6
| ~ spl0_10 ),
inference(forward_demodulation,[],[f20561,f693]) ).
fof(f20750,plain,
( hd(sk3) = skaf44(sk3)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_10 ),
inference(superposition,[],[f20562,f4511]) ).
fof(f24081,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ memberP(sk6,X0) )
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f7273,f276]) ).
fof(f42508,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| skaf44(sk3) = X0 )
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f4612,f276]) ).
fof(f42509,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| hd(sk3) = X0 )
| ~ spl0_2
| ~ spl0_6
| ~ spl0_10 ),
inference(forward_demodulation,[],[f42508,f20750]) ).
fof(f42597,plain,
( ! [X0] :
( hd(sk3) = X0
| ~ memberP(sk6,X0) )
| ~ spl0_2
| ~ spl0_6
| ~ spl0_10
| ~ spl0_16
| ~ spl0_20 ),
inference(resolution,[],[f42509,f24081]) ).
fof(f42601,plain,
( sk5 = hd(sk3)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_10
| ~ spl0_20 ),
inference(resolution,[],[f42509,f7276]) ).
fof(f45764,plain,
( ! [X0] :
( ~ memberP(sk6,X0)
| sk5 = X0 )
| ~ spl0_2
| ~ spl0_6
| ~ spl0_10
| ~ spl0_16
| ~ spl0_20 ),
inference(forward_demodulation,[],[f42597,f42601]) ).
fof(f45895,plain,
( sk5 = sk8
| ~ spl0_2
| ~ spl0_4
| ~ spl0_6
| ~ spl0_10
| ~ spl0_16
| ~ spl0_20 ),
inference(resolution,[],[f45764,f267]) ).
fof(f46002,plain,
( ~ leq(sk8,sk8)
| ~ spl0_2
| spl0_3
| ~ spl0_4
| ~ spl0_6
| ~ spl0_10
| ~ spl0_16
| ~ spl0_20 ),
inference(superposition,[],[f4323,f45895]) ).
fof(f46074,plain,
( leq(sk8,sk8)
| ~ spl0_2
| ~ spl0_4
| ~ spl0_5
| ~ spl0_6
| ~ spl0_10
| ~ spl0_16
| ~ spl0_20 ),
inference(forward_demodulation,[],[f271,f45895]) ).
fof(f46078,plain,
( $false
| ~ spl0_2
| spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_6
| ~ spl0_10
| ~ spl0_16
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f46002,f46074]) ).
fof(f46079,plain,
( ~ spl0_2
| spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_6
| ~ spl0_10
| ~ spl0_16
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f46078]) ).
fof(f46081,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ memberP(sk7,X0) )
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f5885,f276]) ).
fof(f46098,plain,
( ! [X0] : hd(cons(X0,nil)) = X0
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f19997,f276]) ).
fof(f46317,plain,
( sk7 = cons(skaf83(sk7),skaf82(sk7))
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f644,f692]) ).
fof(f46351,plain,
( memberP(sk7,skaf83(sk7))
| ~ ssItem(skaf83(sk7))
| ~ ssList(skaf82(sk7))
| spl0_10 ),
inference(superposition,[],[f247,f46317]) ).
fof(f46368,plain,
( memberP(sk7,skaf83(sk7))
| ~ ssList(skaf82(sk7))
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f46351,f12]) ).
fof(f46400,plain,
( memberP(sk7,skaf83(sk7))
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f46368,f13]) ).
fof(f49622,plain,
( hd(sk3) = skaf44(sk3)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_16 ),
inference(superposition,[],[f46098,f4511]) ).
fof(f50111,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| hd(sk3) = X0 )
| ~ spl0_2
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_demodulation,[],[f42508,f49622]) ).
fof(f50888,plain,
( ! [X0] :
( hd(sk3) = X0
| ~ memberP(sk7,X0) )
| ~ spl0_2
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(resolution,[],[f50111,f46081]) ).
fof(f50889,plain,
( ! [X0] :
( hd(sk3) = X0
| ~ memberP(sk6,X0) )
| ~ spl0_2
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(resolution,[],[f50111,f24081]) ).
fof(f50893,plain,
( sk5 = hd(sk3)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(resolution,[],[f50111,f7276]) ).
fof(f51970,plain,
( ! [X0] :
( ~ memberP(sk7,X0)
| sk5 = X0 )
| ~ spl0_2
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(forward_demodulation,[],[f50888,f50893]) ).
fof(f51976,plain,
( sk5 = skaf83(sk7)
| ~ spl0_2
| ~ spl0_6
| spl0_10
| ~ spl0_16
| ~ spl0_20 ),
inference(resolution,[],[f51970,f46400]) ).
fof(f51983,plain,
( memberP(sk7,sk5)
| ~ spl0_2
| ~ spl0_6
| spl0_10
| ~ spl0_16
| ~ spl0_20 ),
inference(superposition,[],[f46400,f51976]) ).
fof(f52378,plain,
( ! [X0] :
( ~ memberP(sk6,X0)
| sk5 = X0 )
| ~ spl0_2
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(forward_demodulation,[],[f50889,f50893]) ).
fof(f52382,plain,
( sk5 = sk8
| ~ spl0_2
| ~ spl0_4
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(resolution,[],[f52378,f267]) ).
fof(f52521,plain,
( memberP(sk7,sk8)
| ~ spl0_2
| ~ spl0_4
| ~ spl0_6
| spl0_10
| ~ spl0_16
| ~ spl0_20 ),
inference(superposition,[],[f51983,f52382]) ).
fof(f52525,plain,
( $false
| ~ spl0_2
| spl0_3
| ~ spl0_4
| ~ spl0_6
| spl0_10
| ~ spl0_16
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f52521,f262]) ).
fof(f52526,plain,
( ~ spl0_2
| spl0_3
| ~ spl0_4
| ~ spl0_6
| spl0_10
| ~ spl0_16
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f52525]) ).
fof(f52532,plain,
( ~ leq(sk8,sk5)
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f216,f271]) ).
fof(f52533,plain,
( ~ leq(sk8,sk8)
| ~ spl0_2
| ~ spl0_4
| ~ spl0_5
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(forward_demodulation,[],[f52532,f52382]) ).
fof(f52534,plain,
( sk5 = sk8
| ~ spl0_2
| ~ spl0_3
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(resolution,[],[f263,f51970]) ).
fof(f52544,plain,
( ~ ssItem(sk8)
| ~ spl0_2
| ~ spl0_4
| ~ spl0_5
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(resolution,[],[f52533,f62]) ).
fof(f52553,plain,
( $false
| ~ spl0_2
| ~ spl0_4
| ~ spl0_5
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f52544,f212]) ).
fof(f52554,plain,
( ~ spl0_2
| ~ spl0_4
| ~ spl0_5
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f52553]) ).
fof(f52556,plain,
( ~ leq(sk8,sk8)
| ~ spl0_2
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(forward_demodulation,[],[f272,f52382]) ).
fof(f52561,plain,
( ~ ssItem(sk8)
| ~ spl0_2
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(resolution,[],[f52556,f62]) ).
fof(f52570,plain,
( $false
| ~ spl0_2
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f52561,f212]) ).
fof(f52571,plain,
( ~ spl0_2
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f52570]) ).
fof(f52608,plain,
( ~ leq(sk8,sk8)
| ~ spl0_2
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(superposition,[],[f272,f52534]) ).
fof(f52836,plain,
( ~ ssItem(sk8)
| ~ spl0_2
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(resolution,[],[f52608,f62]) ).
fof(f52845,plain,
( $false
| ~ spl0_2
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f52836,f212]) ).
fof(f52846,plain,
( ~ spl0_2
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f52845]) ).
fof(f52999,plain,
( ! [X2,X3,X0,X1] :
( ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(X3) )
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f238,f279]) ).
fof(f53000,plain,
( ! [X2,X3,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssItem(X2)
| ~ ssList(X3)
| ~ ssList(app(X1,cons(X2,X0)))
| ~ ssList(cons(X2,X3)) )
| ~ spl0_7 ),
inference(resolution,[],[f52999,f85]) ).
fof(f53206,plain,
( ! [X2,X3,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssItem(X2)
| ~ ssList(X3)
| ~ ssList(app(X1,cons(X2,X0))) )
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f53000,f86]) ).
fof(f53319,definition,
( spl0_42
<=> ! [X3] : ~ ssList(X3) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f53320,plain,
( ! [X3] : ~ ssList(X3)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f53319]) ).
fof(f53322,definition,
( spl0_43
<=> ! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(X1,cons(X2,X0)))
| ~ ssItem(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f53323,plain,
( ! [X2,X0,X1] :
( ~ ssList(app(X1,cons(X2,X0)))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X2) )
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f53322]) ).
fof(f53324,plain,
( spl0_42
| spl0_43
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f53206,f278,f53322,f53319]) ).
fof(f53325,plain,
( $false
| ~ spl0_42 ),
inference(resolution,[],[f53320,f8]) ).
fof(f53401,plain,
~ spl0_42,
inference(avatar_contradiction_clause,[],[f53325]) ).
fof(f53469,plain,
( ~ ssList(cons(sk5,nil))
| ~ ssList(nil)
| ~ ssList(nil)
| ~ ssItem(sk5)
| ~ spl0_16
| ~ spl0_43 ),
inference(superposition,[],[f53323,f3192]) ).
fof(f53471,plain,
( ~ ssList(cons(sk5,nil))
| ~ ssList(nil)
| ~ ssItem(sk5)
| ~ spl0_16
| ~ spl0_43 ),
inference(duplicate_literal_removal,[],[f53469]) ).
fof(f53475,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| ~ spl0_16
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f53471,f86]) ).
fof(f53516,plain,
( ~ ssItem(sk5)
| ~ spl0_16
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f53475,f8]) ).
fof(f53554,plain,
( $false
| ~ spl0_16
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f53516,f207]) ).
fof(f53555,plain,
( ~ spl0_16
| ~ spl0_43 ),
inference(avatar_contradiction_clause,[],[f53554]) ).
cnf(s1,plain,
( ~ spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f259]) ).
cnf(s2,plain,
( spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f268]) ).
cnf(s3,plain,
( spl0_4
| ~ spl0_5 ),
inference(sat_conversion,[],[f273]) ).
cnf(s4,plain,
( spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f280]) ).
cnf(s11,plain,
( spl0_14
| ~ spl0_15 ),
inference(sat_conversion,[],[f1200]) ).
cnf(s12,plain,
( ~ spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f3158]) ).
cnf(s14,plain,
spl0_16,
inference(sat_conversion,[],[f3190]) ).
cnf(s20,plain,
( spl0_15
| ~ spl0_18 ),
inference(sat_conversion,[],[f4418]) ).
cnf(s23,plain,
( ~ spl0_16
| spl0_20 ),
inference(sat_conversion,[],[f4469]) ).
cnf(s24,plain,
( ~ spl0_14
| ~ spl0_16
| ~ spl0_17
| ~ spl0_18 ),
inference(sat_conversion,[],[f4503]) ).
cnf(s25,plain,
( spl0_1
| spl0_18 ),
inference(sat_conversion,[],[f4509]) ).
cnf(s75,plain,
( ~ spl0_2
| spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_6
| ~ spl0_10
| ~ spl0_16
| ~ spl0_20 ),
inference(sat_conversion,[],[f46079]) ).
cnf(s79,plain,
( ~ spl0_2
| spl0_3
| ~ spl0_4
| ~ spl0_6
| spl0_10
| ~ spl0_16
| ~ spl0_20 ),
inference(sat_conversion,[],[f52526]) ).
cnf(s80,plain,
( ~ spl0_2
| ~ spl0_4
| ~ spl0_5
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(sat_conversion,[],[f52554]) ).
cnf(s81,plain,
( ~ spl0_2
| ~ spl0_4
| spl0_5
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(sat_conversion,[],[f52571]) ).
cnf(s82,plain,
( ~ spl0_2
| ~ spl0_3
| spl0_5
| ~ spl0_6
| ~ spl0_16
| ~ spl0_20 ),
inference(sat_conversion,[],[f52846]) ).
cnf(s83,plain,
( ~ spl0_7
| spl0_42
| spl0_43 ),
inference(sat_conversion,[],[f53324]) ).
cnf(s120,plain,
~ spl0_42,
inference(sat_conversion,[],[f53401]) ).
cnf(s122,plain,
( ~ spl0_16
| ~ spl0_43 ),
inference(sat_conversion,[],[f53555]) ).
cnf(s125,plain,
( ~ spl0_7
| spl0_43 ),
inference(rat,[],[s83,s120]) ).
cnf(s126,plain,
~ spl0_43,
inference(rat,[],[s122,s14]) ).
cnf(s127,plain,
spl0_20,
inference(rat,[],[s23,s14]) ).
cnf(s129,plain,
~ spl0_7,
inference(rat,[],[s125,s126]) ).
cnf(s130,plain,
spl0_17,
inference(rat,[],[s12,s14]) ).
cnf(s132,plain,
spl0_6,
inference(rat,[],[s4,s129]) ).
cnf(s133,plain,
~ spl0_18,
inference(rat,[],[s11,s24,s20,s14,s130]) ).
cnf(s134,plain,
spl0_1,
inference(rat,[],[s25,s133]) ).
cnf(s136,plain,
spl0_2,
inference(rat,[],[s1,s134]) ).
cnf(s140,plain,
( ~ spl0_4
| ~ spl0_10
| spl0_3 ),
inference(rat,[],[s81,s75,s127,s14,s132,s136]) ).
cnf(s141,plain,
( ~ spl0_4
| spl0_3 ),
inference(rat,[],[s140,s79,s127,s14,s136,s132]) ).
cnf(s142,plain,
spl0_3,
inference(rat,[],[s141,s2]) ).
cnf(s143,plain,
spl0_5,
inference(rat,[],[s82,s127,s14,s132,s136,s142]) ).
cnf(s145,plain,
spl0_4,
inference(rat,[],[s3,s143]) ).
cnf(s146,plain,
$false,
inference(rat,[],[s80,s127,s14,s132,s136,s145,s143]) ).
fof(f53560,plain,
$false,
inference(avatar_sat_refutation,[],[s146]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC285-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.17 % Computer : n014.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Mon Sep 28 08:52:31 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.20 Running first-order model finding
% 0.10/0.20 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.72/2.34 % (1643623)Will run a generic schedule for satisfiability detection.
% 14.72/2.34 % (1643628)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1842830817_2999 on theBenchmark for (2999ds/0Mi)
% 14.72/2.34 % (1643629)% WARNING: option uhcvi not known.
% 14.72/2.34 % TRYING [1]
% 14.72/2.34 % TRYING [2]
% 14.72/2.34 % (1643629)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2940698644:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.72/2.34 % (1643630)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3662522917:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.72/2.34 % (1643631)dis+10_1_sil=32000:sp=arity:random_seed=2221452448:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.72/2.34 % (1643632)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1706326458:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.72/2.34 % (1643634)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3948667855:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.72/2.34 % (1643633)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3813532532:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.72/2.34 % TRYING [3]
% 14.72/2.34 % TRYING [4]
% 14.72/2.34 % TRYING [5]
% 14.72/2.34 % (1643632)Instruction limit reached!
% 14.72/2.34 % (1643632)------------------------------
% 14.72/2.34 % (1643632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.72/2.34 % (1643632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.72/2.34 % (1643632)CaDiCaL version: 2.1.3
% 14.72/2.34 % (1643632)Termination reason: Instruction limit
% 14.72/2.34 % (1643632)Termination phase: Saturation
% 14.72/2.34 % (1643632)Time elapsed: 0.059 s
% 14.72/2.34 % (1643632)Peak memory usage: 13 MB
% 14.72/2.34 % (1643632)Instructions burned: 116 (million)
% 14.72/2.34 % (1643631)Instruction limit reached!
% 14.72/2.34 % (1643631)------------------------------
% 14.72/2.34 % (1643631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.72/2.34 % (1643631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.72/2.34 % (1643631)CaDiCaL version: 2.1.3
% 14.72/2.34 % (1643631)Termination reason: Instruction limit
% 14.72/2.34 % (1643631)Termination phase: Saturation
% 14.72/2.34 % (1643631)Time elapsed: 0.060 s
% 14.72/2.34 % (1643631)Peak memory usage: 13 MB
% 14.72/2.34 % (1643631)Instructions burned: 105 (million)
% 14.72/2.34 % (1643633)Instruction limit reached!
% 14.72/2.34 % (1643633)------------------------------
% 14.72/2.34 % (1643633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.72/2.34 % (1643633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.72/2.34 % (1643633)CaDiCaL version: 2.1.3
% 14.72/2.34 % (1643633)Termination reason: Instruction limit
% 14.72/2.34 % (1643633)Termination phase: Saturation
% 14.72/2.34 % (1643633)Time elapsed: 0.064 s
% 14.72/2.34 % (1643633)Peak memory usage: 14 MB
% 14.72/2.34 % (1643633)Instructions burned: 132 (million)
% 14.72/2.34 % (1643643)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3781360620:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.72/2.34 % (1643642)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4243622217:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 14.72/2.34 % (1643644)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=2987221517:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.72/2.34 % (1643634)Instruction limit reached!
% 14.72/2.34 % (1643634)------------------------------
% 14.72/2.34 % (1643634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.72/2.34 % TRYING [1]
% 14.72/2.34 % (1643634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.72/2.34 % (1643634)CaDiCaL version: 2.1.3
% 14.72/2.34 % (1643634)Termination reason: Instruction limit
% 14.72/2.34 % (1643634)Termination phase: Saturation
% 14.72/2.34 % (1643634)Time elapsed: 0.090 s
% 14.72/2.34 % (1643634)Peak memory usage: 14 MB
% 14.72/2.34 % (1643634)Instructions burned: 159 (million)
% 14.72/2.34 % TRYING [2]
% 14.72/2.34 % TRYING [3]
% 14.72/2.34 % (1643648)ott-21_1_sil=16000:fs=off:random_seed=3301643360:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.72/2.34 % TRYING [4]
% 14.72/2.34 % TRYING [6]
% 14.72/2.34 % (1643643)Instruction limit reached!
% 14.72/2.34 % (1643643)------------------------------
% 14.72/2.34 % (1643643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.17/2.75 % (1643643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/2.75 % (1643643)CaDiCaL version: 2.1.3
% 17.17/2.75 % (1643643)Termination reason: Instruction limit
% 17.17/2.75 % (1643643)Termination phase: Saturation
% 17.17/2.75 % (1643643)Time elapsed: 0.067 s
% 17.17/2.75 % (1643643)Peak memory usage: 13 MB
% 17.17/2.75 % (1643643)Instructions burned: 133 (million)
% 17.17/2.75 % (1643650)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2953544077:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 17.17/2.75 % TRYING [5]
% 17.17/2.75 % (1643648)Instruction limit reached!
% 17.17/2.75 % (1643648)------------------------------
% 17.17/2.75 % (1643648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.17/2.75 % (1643648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/2.75 % (1643648)CaDiCaL version: 2.1.3
% 17.17/2.75 % (1643648)Termination reason: Instruction limit
% 17.17/2.75 % (1643648)Termination phase: Saturation
% 17.17/2.75 % (1643648)Time elapsed: 0.090 s
% 17.17/2.75 % (1643648)Peak memory usage: 13 MB
% 17.17/2.75 % (1643648)Instructions burned: 181 (million)
% 17.17/2.75 % (1643652)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=561100261:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 17.17/2.75 % TRYING [1]
% 17.17/2.75 % TRYING [2]
% 17.17/2.75 % TRYING [3]
% 17.17/2.75 % TRYING [4]
% 17.17/2.75 % TRYING [6]
% 17.17/2.75 % (1643642)Instruction limit reached!
% 17.17/2.75 % (1643642)------------------------------
% 17.17/2.75 % (1643642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.17/2.75 % (1643642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/2.75 % (1643642)CaDiCaL version: 2.1.3
% 17.17/2.75 % (1643642)Termination reason: Instruction limit
% 17.17/2.75 % (1643642)Termination phase: Finite model building constraint generation
% 17.17/2.75 % (1643642)Time elapsed: 0.280 s
% 17.17/2.75 % (1643642)Peak memory usage: 34 MB
% 17.17/2.75 % (1643642)Instructions burned: 716 (million)
% 17.17/2.75 % TRYING [5]
% 17.17/2.75 % (1643654)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=371349804:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 17.17/2.75 % TRYING [7]
% 17.17/2.75 % (1643644)Instruction limit reached!
% 17.17/2.75 % (1643644)------------------------------
% 17.17/2.75 % (1643644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.17/2.75 % (1643644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/2.75 % (1643644)CaDiCaL version: 2.1.3
% 17.17/2.75 % (1643644)Termination reason: Instruction limit
% 17.17/2.75 % (1643644)Termination phase: Saturation
% 17.17/2.75 % (1643644)Time elapsed: 0.371 s
% 17.17/2.75 % (1643644)Peak memory usage: 19 MB
% 17.17/2.75 % (1643644)Instructions burned: 684 (million)
% 17.17/2.75 % (1643656)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3309150045:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 17.17/2.75 % (1643650)Instruction limit reached!
% 17.17/2.75 % (1643650)------------------------------
% 17.17/2.75 % (1643650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.17/2.75 % (1643650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/2.75 % (1643650)CaDiCaL version: 2.1.3
% 17.17/2.75 % (1643650)Termination reason: Instruction limit
% 17.17/2.75 % (1643650)Termination phase: Saturation
% 17.17/2.75 % (1643650)Time elapsed: 0.324 s
% 17.17/2.75 % (1643650)Peak memory usage: 14 MB
% 17.17/2.75 % (1643650)Instructions burned: 477 (million)
% 17.17/2.75 % (1643658)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=3719349325: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)
% 17.17/2.75 % (1643652)Instruction limit reached!
% 17.17/2.75 % (1643652)------------------------------
% 17.17/2.75 % (1643652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.17/2.75 % (1643652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/2.75 % (1643652)CaDiCaL version: 2.1.3
% 17.17/2.75 % (1643652)Termination reason: Instruction limit
% 17.17/2.75 % (1643652)Termination phase: Finite model building SAT solving
% 17.17/2.75 % (1643652)Time elapsed: 0.333 s
% 17.17/2.75 % (1643652)Peak memory usage: 22 MB
% 17.17/2.75 % (1643652)Instructions burned: 865 (million)
% 17.17/2.75 % (1643660)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1686698441:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 17.17/2.75 % TRYING [14]
% 17.17/2.75 % (1643656)Instruction limit reached!
% 17.17/2.75 % (1643656)------------------------------
% 17.17/2.75 % (1643656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.17/2.75 % (1643656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/2.75 % (1643656)CaDiCaL version: 2.1.3
% 17.17/2.75 % (1643656)Termination reason: Instruction limit
% 17.17/2.75 % (1643656)Termination phase: Finite model building constraint generation
% 17.17/2.75 % (1643656)Time elapsed: 0.325 s
% 17.17/2.75 % (1643656)Peak memory usage: 72 MB
% 17.17/2.75 % (1643656)Instructions burned: 890 (million)
% 17.17/2.75 % (1643662)fmb+10_1_sil=64000:random_seed=1760983353:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 17.17/2.75 % TRYING [1]
% 17.17/2.75 % TRYING [2]
% 17.17/2.75 % TRYING [3]
% 17.17/2.75 % (1643658)Instruction limit reached!
% 17.17/2.75 % (1643658)------------------------------
% 17.17/2.75 % (1643658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.17/2.75 % (1643658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/2.75 % (1643658)CaDiCaL version: 2.1.3
% 17.17/2.75 % (1643658)Termination reason: Instruction limit
% 17.17/2.75 % (1643658)Termination phase: Saturation
% 17.17/2.75 % (1643658)Time elapsed: 0.386 s
% 17.17/2.75 % (1643658)Peak memory usage: 21 MB
% 17.17/2.75 % (1643658)Instructions burned: 693 (million)
% 17.17/2.75 % TRYING [4]
% 17.17/2.75 % (1643664)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2180447949:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 17.17/2.75 % TRYING [20]
% 17.17/2.75 % (1643660)Instruction limit reached!
% 17.17/2.75 % (1643660)------------------------------
% 17.17/2.75 % (1643660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.17/2.75 % (1643660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/2.75 % (1643660)CaDiCaL version: 2.1.3
% 17.17/2.75 % (1643660)Termination reason: Instruction limit
% 17.17/2.75 % (1643660)Termination phase: Saturation
% 17.17/2.75 % (1643660)Time elapsed: 0.473 s
% 17.17/2.75 % (1643660)Peak memory usage: 20 MB
% 17.17/2.75 % (1643660)Instructions burned: 881 (million)
% 17.17/2.75 % (1643654)Instruction limit reached!
% 17.17/2.75 % (1643654)------------------------------
% 17.17/2.75 % (1643654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.17/2.75 % (1643654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/2.75 % (1643654)CaDiCaL version: 2.1.3
% 17.17/2.75 % (1643654)Termination reason: Instruction limit
% 17.17/2.75 % (1643654)Termination phase: Saturation
% 17.17/2.75 % (1643654)Time elapsed: 0.670 s
% 17.17/2.75 % (1643654)Peak memory usage: 27 MB
% 17.17/2.75 % (1643654)Instructions burned: 1179 (million)
% 17.17/2.75 % (1643666)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2481240705:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 17.17/2.75 % (1643667)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1686911371:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 17.17/2.75 % TRYING [5]
% 17.17/2.75 % TRYING [8]
% 17.17/2.75 % TRYING [8]
% 17.17/2.75 % (1643666)Instruction limit reached!
% 17.17/2.75 % (1643666)------------------------------
% 17.17/2.75 % (1643666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.17/2.75 % (1643666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/2.75 % (1643666)CaDiCaL version: 2.1.3
% 17.17/2.75 % (1643666)Termination reason: Instruction limit
% 17.17/2.75 % (1643666)Termination phase: Finite model building constraint generation
% 17.17/2.75 % (1643666)Time elapsed: 0.330 s
% 17.17/2.75 % (1643666)Peak memory usage: 79 MB
% 17.17/2.75 % (1643666)Instructions burned: 920 (million)
% 17.17/2.75 % (1643670)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2494477173:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 17.17/2.75 % TRYING [6]
% 17.17/2.75 % (1643670)Instruction limit reached!
% 17.17/2.75 % (1643670)------------------------------
% 17.17/2.75 % (1643670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.17/2.75 % (1643670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/2.75 % (1643670)CaDiCaL version: 2.1.3
% 17.17/2.75 % (1643670)Termination reason: Instruction limit
% 17.17/2.75 % (1643670)Termination phase: Saturation
% 17.17/2.75 % (1643670)Time elapsed: 0.629 s
% 17.17/2.75 % (1643670)Peak memory usage: 15 MB
% 17.17/2.75 % (1643670)Instructions burned: 1474 (million)
% 17.17/2.75 % (1643672)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2607152767:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 17.17/2.75 % TRYING [77]
% 17.17/2.75 % TRYING [9]
% 17.17/2.75 % TRYING [7]
% 17.17/2.75 % (1643667) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1643623-1643667"...
% 17.17/2.75 % (1643667)...printing done.
% 17.17/2.75 % (1643667)Refutation found. Thanks to Tanya!
% 17.17/2.75 % SZS status Unsatisfiable for theBenchmark
% 17.17/2.75 % SZS output start Proof for theBenchmark
% See solution above
% 17.17/2.76 % (1643667)------------------------------
% 17.17/2.76 % (1643667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.17/2.76 % (1643667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/2.76 % (1643667)CaDiCaL version: 2.1.3
% 17.17/2.76 % (1643667)Termination reason: Refutation
% 17.17/2.76 % (1643667)Time elapsed: 1.363 s
% 17.17/2.76 % (1643667)Peak memory usage: 34 MB
% 17.17/2.76 % (1643667)Instructions burned: 2698 (million)
% 17.17/2.76 % (1643623)Success in time 2.54 s
% 17.17/2.76 % Vampire exiting
%------------------------------------------------------------------------------