%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC166-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 : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:04:55 PM UTC 2026
% Result : Unsatisfiable 24.63s 4.00s
% Output : Refutation 24.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 47
% Syntax : Number of formulae : 266 ( 36 unt; 10 def)
% Number of atoms : 976 ( 146 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 1383 ( 673 ~; 700 |; 0 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 11 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-2 aty)
% Number of variables : 167 ( 0 sgn 167 !; 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(f47,axiom,
! [X0] : ssItem(skaf44(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause47) ).
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(f75,axiom,
! [X0] :
( ssList(tl(X0))
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause75) ).
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(f97,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| hd(cons(X0,X1)) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause97) ).
fof(f98,axiom,
! [X0,X1] :
( cons(X0,X1) != nil
| ~ ssItem(X0)
| ~ ssList(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause98) ).
fof(f99,plain,
! [X0,X1] :
( nil != cons(X0,X1)
| ~ ssItem(X0)
| ~ ssList(X1) ),
inference(reorient_equations,[],[f98]) ).
fof(f100,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| cons(X0,X1) != X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause99) ).
fof(f103,axiom,
! [X0] :
( ~ singletonP(X0)
| ~ ssList(X0)
| cons(skaf44(X0),nil) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause101) ).
fof(f104,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssItem(X1)
| neq(X1,X0)
| X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause102) ).
fof(f105,plain,
! [X0,X1] :
( neq(X1,X0)
| ~ ssItem(X1)
| ~ ssItem(X0)
| X0 = X1 ),
inference(reorient_equations,[],[f104]) ).
fof(f107,axiom,
! [X0] :
( ~ ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause104) ).
fof(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(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(f163,axiom,
! [X2,X0,X1] :
( app(X0,X1) != app(X2,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause151) ).
fof(f173,axiom,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X2 = X0 ),
file('/export/starexec/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(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(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(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
singletonP(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
ssItem(sk6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_10) ).
fof(f210,negated_conjecture,
ssList(sk8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_11) ).
fof(f211,negated_conjecture,
app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_12) ).
fof(f212,plain,
sk1 = app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8),
inference(reorient_equations,[],[f211]) ).
fof(f213,negated_conjecture,
~ neq(sk5,sk6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_13) ).
fof(f216,plain,
sk3 = app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8),
inference(definition_unfolding,[],[f212,f205]) ).
fof(f226,plain,
! [X2,X1] :
( ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X1)
| memberP(cons(X1,X2),X1) ),
inference(equality_resolution,[],[f149]) ).
fof(f228,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1))
| frontsegP(app(X0,X1),X0) ),
inference(equality_resolution,[],[f155]) ).
fof(f232,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(f234,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(f243,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X2) ),
inference(duplicate_literal_removal,[],[f226]) ).
fof(f248,definition,
( spl0_1
<=> ! [X1] : ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f249,plain,
( ! [X1] : ssItem(X1)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f251,definition,
( spl0_2
<=> ! [X0] :
( ~ ssList(X0)
| duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f252,plain,
( ! [X0] :
( duplicatefreeP(X0)
| ~ ssList(X0) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f253,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f72,f251,f248]) ).
fof(f314,plain,
sk3 = app(nil,sk3),
inference(resolution,[],[f74,f202]) ).
fof(f378,plain,
! [X0] :
( ~ ssList(X0)
| cons(sk5,X0) != X0 ),
inference(resolution,[],[f100,f207]) ).
fof(f410,plain,
nil != cons(sk5,nil),
inference(resolution,[],[f378,f8]) ).
fof(f463,plain,
! [X0] :
( ~ ssList(X0)
| tl(cons(sk5,X0)) = X0 ),
inference(resolution,[],[f96,f207]) ).
fof(f465,plain,
! [X0,X1] :
( ~ ssItem(X1)
| skaf82(X0) = tl(cons(X1,skaf82(X0))) ),
inference(resolution,[],[f96,f13]) ).
fof(f494,plain,
! [X0,X1] :
( ~ ssItem(X1)
| tl(X0) = tl(cons(X1,tl(X0)))
| ~ ssList(X0)
| nil = X0 ),
inference(resolution,[],[f96,f75]) ).
fof(f515,plain,
! [X0,X1] :
( ~ ssItem(X1)
| hd(cons(X1,skaf82(X0))) = X1 ),
inference(resolution,[],[f97,f13]) ).
fof(f544,plain,
! [X0,X1] :
( ~ ssItem(X1)
| hd(cons(X1,tl(X0))) = X1
| ~ ssList(X0)
| nil = X0 ),
inference(resolution,[],[f97,f75]) ).
fof(f550,plain,
( ~ ssList(sk3)
| sk3 = cons(skaf44(sk3),nil) ),
inference(resolution,[],[f103,f206]) ).
fof(f551,plain,
sk3 = cons(skaf44(sk3),nil),
inference(forward_subsumption_resolution,[],[f550,f202]) ).
fof(f552,plain,
( ~ ssItem(sk5)
| ~ ssItem(sk6)
| sk5 = sk6 ),
inference(resolution,[],[f105,f213]) ).
fof(f557,plain,
( ~ ssItem(sk6)
| sk5 = sk6 ),
inference(forward_subsumption_resolution,[],[f552,f207]) ).
fof(f558,plain,
sk5 = sk6,
inference(forward_subsumption_resolution,[],[f557,f208]) ).
fof(f574,plain,
( nil != sk3
| ~ ssItem(skaf44(sk3))
| ~ ssList(nil) ),
inference(superposition,[],[f99,f551]) ).
fof(f576,plain,
( nil != sk3
| ~ ssList(nil) ),
inference(forward_subsumption_resolution,[],[f574,f47]) ).
fof(f585,plain,
nil != sk3,
inference(forward_subsumption_resolution,[],[f576,f8]) ).
fof(f640,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| nil = sk3 ),
inference(resolution,[],[f107,f202]) ).
fof(f642,plain,
( sk7 = cons(hd(sk7),tl(sk7))
| nil = sk7 ),
inference(resolution,[],[f107,f209]) ).
fof(f676,plain,
( sk3 = cons(skaf83(sk3),skaf82(sk3))
| nil = sk3 ),
inference(resolution,[],[f112,f202]) ).
fof(f678,plain,
( sk7 = cons(skaf83(sk7),skaf82(sk7))
| nil = sk7 ),
inference(resolution,[],[f112,f209]) ).
fof(f725,plain,
! [X0,X1] :
( ~ ssItem(X1)
| cons(X1,skaf82(X0)) = app(cons(X1,nil),skaf82(X0)) ),
inference(resolution,[],[f126,f13]) ).
fof(f848,plain,
! [X0,X1] :
( frontsegP(app(X0,X1),X0)
| ~ ssList(X0)
| ~ ssList(X1) ),
inference(forward_subsumption_resolution,[],[f228,f85]) ).
fof(f850,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,app(X0,X1))
| ~ ssList(X0)
| ~ ssList(app(X0,X1))
| app(X0,X1) = X0 ),
inference(resolution,[],[f848,f139]) ).
fof(f869,plain,
( frontsegP(sk3,app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssList(sk8) ),
inference(superposition,[],[f848,f216]) ).
fof(f875,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,app(X0,X1))
| ~ ssList(app(X0,X1))
| app(X0,X1) = X0 ),
inference(duplicate_literal_removal,[],[f850]) ).
fof(f877,plain,
( frontsegP(sk3,app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
inference(forward_subsumption_resolution,[],[f869,f210]) ).
fof(f878,plain,
! [X0,X1] :
( ~ frontsegP(X0,app(X0,X1))
| ~ ssList(X1)
| ~ ssList(X0)
| app(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f875,f85]) ).
fof(f880,plain,
( frontsegP(sk3,app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
inference(forward_demodulation,[],[f877,f558]) ).
fof(f881,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| frontsegP(sk3,app(app(sk7,cons(sk5,nil)),cons(sk5,nil))) ),
inference(forward_demodulation,[],[f880,f558]) ).
fof(f1042,plain,
! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X2,X1)
| ~ frontsegP(X1,app(X2,X0))
| ~ ssList(X1)
| ~ ssList(app(X2,X0))
| app(X2,X0) = X1 ),
inference(resolution,[],[f148,f139]) ).
fof(f1061,plain,
! [X0] :
( frontsegP(sk3,X0)
| ~ ssList(sk8)
| ~ ssList(X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ frontsegP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0) ),
inference(superposition,[],[f148,f216]) ).
fof(f1067,plain,
! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X2,X1)
| ~ frontsegP(X1,app(X2,X0))
| ~ ssList(app(X2,X0))
| app(X2,X0) = X1 ),
inference(duplicate_literal_removal,[],[f1042]) ).
fof(f1070,plain,
! [X0] :
( frontsegP(sk3,X0)
| ~ ssList(X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ frontsegP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0) ),
inference(forward_subsumption_resolution,[],[f1061,f210]) ).
fof(f1075,plain,
! [X2,X0,X1] :
( ~ frontsegP(X1,app(X2,X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ frontsegP(X2,X1)
| ~ ssList(X0)
| app(X2,X0) = X1 ),
inference(forward_subsumption_resolution,[],[f1067,f85]) ).
fof(f1078,plain,
! [X0] :
( ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| frontsegP(sk3,X0)
| ~ ssList(X0)
| ~ frontsegP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0) ),
inference(forward_demodulation,[],[f1070,f558]) ).
fof(f1083,plain,
! [X0] :
( ~ frontsegP(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| frontsegP(sk3,X0)
| ~ ssList(X0) ),
inference(forward_demodulation,[],[f1078,f558]) ).
fof(f1103,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssList(sk8)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssItem(X0)
| ~ memberP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0) ),
inference(superposition,[],[f151,f216]) ).
fof(f1109,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ ssItem(X0)
| ~ memberP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0) ),
inference(forward_subsumption_resolution,[],[f1103,f210]) ).
fof(f1110,plain,
! [X0] :
( ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),X0) ),
inference(forward_demodulation,[],[f1109,f558]) ).
fof(f1111,plain,
! [X0] :
( ~ memberP(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),X0)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| memberP(sk3,X0)
| ~ ssItem(X0) ),
inference(forward_demodulation,[],[f1110,f558]) ).
fof(f1140,plain,
nil = tl(cons(sk5,nil)),
inference(resolution,[],[f463,f8]) ).
fof(f1541,plain,
! [X0] :
( sk3 != app(X0,sk3)
| ~ ssList(X0)
| ~ ssList(sk3)
| ~ ssList(nil)
| nil = X0 ),
inference(superposition,[],[f163,f314]) ).
fof(f1588,plain,
! [X0] :
( sk3 != app(X0,sk3)
| ~ ssList(X0)
| ~ ssList(nil)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f1541,f202]) ).
fof(f1632,plain,
! [X0] :
( sk3 != app(X0,sk3)
| ~ ssList(X0)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f1588,f8]) ).
fof(f1912,plain,
! [X0] :
( ~ memberP(sk3,X0)
| ~ ssList(nil)
| ~ ssItem(skaf44(sk3))
| ~ ssItem(X0)
| memberP(nil,X0)
| skaf44(sk3) = X0 ),
inference(superposition,[],[f174,f551]) ).
fof(f1915,plain,
! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(skaf44(sk3))
| ~ ssItem(X0)
| memberP(nil,X0)
| skaf44(sk3) = X0 ),
inference(forward_subsumption_resolution,[],[f1912,f8]) ).
fof(f1916,plain,
! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(X0)
| memberP(nil,X0)
| skaf44(sk3) = X0 ),
inference(forward_subsumption_resolution,[],[f1915,f47]) ).
fof(f1917,plain,
! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(X0)
| skaf44(sk3) = X0 ),
inference(forward_subsumption_resolution,[],[f1916,f71]) ).
fof(f2232,plain,
( ! [X2,X3,X0,X1] :
( ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(X3) )
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f234,f252]) ).
fof(f2366,plain,
sk3 = cons(hd(sk3),tl(sk3)),
inference(forward_subsumption_resolution,[],[f640,f585]) ).
fof(f2424,definition,
( spl0_5
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f2425,plain,
( nil != sk7
| spl0_5 ),
inference(avatar_component_clause,[],[f2424]) ).
fof(f2426,plain,
( nil = sk7
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f2424]) ).
fof(f2428,definition,
( spl0_6
<=> sk7 = cons(hd(sk7),tl(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f2430,plain,
( sk7 = cons(hd(sk7),tl(sk7))
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f2428]) ).
fof(f2431,plain,
( spl0_5
| spl0_6 ),
inference(avatar_split_clause,[],[f642,f2428,f2424]) ).
fof(f2462,plain,
sk3 = cons(skaf83(sk3),skaf82(sk3)),
inference(forward_subsumption_resolution,[],[f676,f585]) ).
fof(f2609,definition,
( spl0_9
<=> nil = skaf82(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f2610,plain,
( nil != skaf82(sk3)
| spl0_9 ),
inference(avatar_component_clause,[],[f2609]) ).
fof(f2611,plain,
( nil = skaf82(sk3)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f2609]) ).
fof(f3690,definition,
( spl0_14
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f3691,plain,
( ssList(cons(sk5,nil))
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f3690]) ).
fof(f3692,plain,
( ~ ssList(cons(sk5,nil))
| spl0_14 ),
inference(avatar_component_clause,[],[f3690]) ).
fof(f3698,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| spl0_14 ),
inference(resolution,[],[f3692,f86]) ).
fof(f3699,plain,
( ~ ssItem(sk5)
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f3698,f8]) ).
fof(f3700,plain,
( $false
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f3699,f207]) ).
fof(f3701,plain,
spl0_14,
inference(avatar_contradiction_clause,[],[f3700]) ).
fof(f3848,plain,
( sk7 = cons(skaf83(sk7),skaf82(sk7))
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f678,f2425]) ).
fof(f3951,definition,
( spl0_16
<=> ssList(app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f3952,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f3951]) ).
fof(f3953,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| spl0_16 ),
inference(avatar_component_clause,[],[f3951]) ).
fof(f3958,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| spl0_16 ),
inference(resolution,[],[f3953,f85]) ).
fof(f3959,plain,
( ~ ssList(cons(sk5,nil))
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f3958,f209]) ).
fof(f3960,plain,
( $false
| ~ spl0_14
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f3959,f3691]) ).
fof(f3961,plain,
( ~ spl0_14
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f3960]) ).
fof(f4102,definition,
( spl0_17
<=> ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f4103,plain,
( ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f4102]) ).
fof(f4104,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| spl0_17 ),
inference(avatar_component_clause,[],[f4102]) ).
fof(f4106,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk5,nil))
| spl0_17 ),
inference(resolution,[],[f4104,f85]) ).
fof(f4107,plain,
( ~ ssList(cons(sk5,nil))
| ~ spl0_16
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f4106,f3952]) ).
fof(f4108,plain,
( $false
| ~ spl0_14
| ~ spl0_16
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f4107,f3691]) ).
fof(f4109,plain,
( ~ spl0_14
| ~ spl0_16
| spl0_17 ),
inference(avatar_contradiction_clause,[],[f4108]) ).
fof(f4253,plain,
( ~ ssList(nil)
| ~ ssList(sk7)
| ~ ssItem(sk5)
| ~ ssList(nil)
| ~ spl0_2
| ~ spl0_17 ),
inference(resolution,[],[f4103,f2232]) ).
fof(f4297,plain,
( ~ ssList(nil)
| ~ ssList(sk7)
| ~ ssItem(sk5)
| ~ spl0_2
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f4253]) ).
fof(f4298,plain,
( ~ ssList(sk7)
| ~ ssItem(sk5)
| ~ spl0_2
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f4297,f8]) ).
fof(f4299,plain,
( ~ ssItem(sk5)
| ~ spl0_2
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f4298,f209]) ).
fof(f4300,plain,
( $false
| ~ spl0_2
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f4299,f207]) ).
fof(f4301,plain,
( ~ spl0_2
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f4300]) ).
fof(f5280,plain,
( frontsegP(sk3,app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f881,f4103]) ).
fof(f5323,plain,
( ! [X0] :
( ~ frontsegP(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),X0)
| frontsegP(sk3,X0)
| ~ ssList(X0) )
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1083,f4103]) ).
fof(f5327,plain,
( frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk5,nil))
| ~ spl0_17 ),
inference(resolution,[],[f5323,f848]) ).
fof(f5335,plain,
( frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk5,nil))
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f5327]) ).
fof(f5339,plain,
( frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ~ ssList(cons(sk5,nil))
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f5335,f3952]) ).
fof(f5342,plain,
( frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f5339,f3691]) ).
fof(f5348,plain,
( ! [X0] :
( ~ memberP(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),X0)
| memberP(sk3,X0)
| ~ ssItem(X0) )
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1111,f4103]) ).
fof(f5349,plain,
( ! [X0] :
( ~ memberP(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)),X0)
| memberP(sk3,X0) )
| ~ spl0_1
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f5348,f249]) ).
fof(f5354,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssList(cons(sk5,nil))
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssItem(X0)
| ~ memberP(app(sk7,cons(sk5,nil)),X0) )
| ~ spl0_1
| ~ spl0_17 ),
inference(resolution,[],[f5349,f151]) ).
fof(f5355,plain,
( memberP(sk3,sk5)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssItem(sk5)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ ssList(nil)
| ~ spl0_1
| ~ spl0_17 ),
inference(resolution,[],[f5349,f232]) ).
fof(f5356,plain,
( memberP(sk3,sk5)
| ~ ssItem(sk5)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ ssList(nil)
| ~ spl0_1
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f5355,f3952]) ).
fof(f5357,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssItem(X0)
| ~ memberP(app(sk7,cons(sk5,nil)),X0) )
| ~ spl0_1
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f5354,f3691]) ).
fof(f5359,plain,
( memberP(sk3,sk5)
| ~ ssList(app(app(sk7,cons(sk5,nil)),cons(sk5,nil)))
| ~ ssList(nil)
| ~ spl0_1
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f5356,f207]) ).
fof(f5360,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(app(sk7,cons(sk5,nil)),X0) )
| ~ spl0_1
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f5357,f3952]) ).
fof(f5362,plain,
( memberP(sk3,sk5)
| ~ ssList(nil)
| ~ spl0_1
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f5359,f4103]) ).
fof(f5363,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ memberP(app(sk7,cons(sk5,nil)),X0) )
| ~ spl0_1
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f5360,f249]) ).
fof(f5365,plain,
( memberP(sk3,sk5)
| ~ spl0_1
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f5362,f8]) ).
fof(f7395,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| skaf44(sk3) = X0 )
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f1917,f249]) ).
fof(f7844,plain,
( ! [X0,X1] : hd(cons(X1,skaf82(X0))) = X1
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f515,f249]) ).
fof(f7847,plain,
( hd(sk3) = skaf83(sk3)
| ~ spl0_1 ),
inference(superposition,[],[f7844,f2462]) ).
fof(f8969,plain,
( ! [X0,X1] : skaf82(X0) = tl(cons(X1,skaf82(X0)))
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f465,f249]) ).
fof(f8972,plain,
( tl(sk3) = skaf82(sk3)
| ~ spl0_1 ),
inference(superposition,[],[f8969,f2462]) ).
fof(f8973,plain,
( tl(sk7) = skaf82(sk7)
| ~ spl0_1
| spl0_5 ),
inference(superposition,[],[f8969,f3848]) ).
fof(f8979,plain,
( nil = tl(sk3)
| ~ spl0_1
| ~ spl0_9 ),
inference(forward_demodulation,[],[f8972,f2611]) ).
fof(f9003,plain,
( ssList(tl(sk7))
| ~ spl0_1
| spl0_5 ),
inference(superposition,[],[f13,f8973]) ).
fof(f10417,plain,
( ! [X0,X1] : cons(X1,skaf82(X0)) = app(cons(X1,nil),skaf82(X0))
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f725,f249]) ).
fof(f10422,plain,
( ! [X0] : app(sk3,skaf82(X0)) = cons(skaf44(sk3),skaf82(X0))
| ~ spl0_1 ),
inference(superposition,[],[f10417,f551]) ).
fof(f14056,plain,
( ! [X0,X1] :
( ~ ssList(X0)
| hd(cons(X1,tl(X0))) = X1
| nil = X0 )
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f544,f249]) ).
fof(f14093,plain,
( ! [X0] :
( hd(cons(X0,tl(cons(sk5,nil)))) = X0
| nil = cons(sk5,nil) )
| ~ spl0_1
| ~ spl0_14 ),
inference(resolution,[],[f14056,f3691]) ).
fof(f20428,plain,
( ! [X0,X1] :
( ~ ssList(X0)
| tl(X0) = tl(cons(X1,tl(X0)))
| nil = X0 )
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f494,f249]) ).
fof(f20461,plain,
( ! [X0] :
( tl(cons(sk5,nil)) = tl(cons(X0,tl(cons(sk5,nil))))
| nil = cons(sk5,nil) )
| ~ spl0_1
| ~ spl0_14 ),
inference(resolution,[],[f20428,f3691]) ).
fof(f60398,definition,
( spl0_36
<=> frontsegP(sk7,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f60399,plain,
( frontsegP(sk7,sk3)
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f60398]) ).
fof(f60400,plain,
( ~ frontsegP(sk7,sk3)
| spl0_36 ),
inference(avatar_component_clause,[],[f60398]) ).
fof(f60402,definition,
( spl0_37
<=> sk3 = app(sk7,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f60403,plain,
( sk3 != app(sk7,sk3)
| spl0_37 ),
inference(avatar_component_clause,[],[f60402]) ).
fof(f60404,plain,
( sk3 = app(sk7,sk3)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f60402]) ).
fof(f82428,plain,
( sk7 = cons(skaf83(sk7),skaf82(sk7))
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f678,f2425]) ).
fof(f82961,plain,
( tl(sk7) = skaf82(sk7)
| ~ spl0_1
| spl0_5 ),
inference(superposition,[],[f8969,f82428]) ).
fof(f82962,plain,
( hd(sk7) = skaf83(sk7)
| ~ spl0_1
| spl0_5 ),
inference(superposition,[],[f7844,f82428]) ).
fof(f82996,plain,
( memberP(sk7,skaf83(sk7))
| ~ ssItem(skaf83(sk7))
| ~ ssList(skaf82(sk7))
| spl0_5 ),
inference(superposition,[],[f243,f82428]) ).
fof(f83038,plain,
( memberP(sk7,skaf83(sk7))
| ~ ssList(skaf82(sk7))
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f82996,f12]) ).
fof(f83065,plain,
( memberP(sk7,skaf83(sk7))
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f83038,f13]) ).
fof(f83384,plain,
( memberP(sk7,hd(sk7))
| ~ spl0_1
| spl0_5 ),
inference(superposition,[],[f83065,f82962]) ).
fof(f83524,plain,
( sk3 != sk3
| ~ ssList(sk7)
| nil = sk7
| ~ spl0_37 ),
inference(superposition,[],[f1632,f60404]) ).
fof(f83550,plain,
( ~ ssList(sk7)
| nil = sk7
| ~ spl0_37 ),
inference(trivial_inequality_removal,[],[f83524]) ).
fof(f83566,plain,
( nil = sk7
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f83550,f209]) ).
fof(f83583,plain,
( $false
| spl0_5
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f83566,f2425]) ).
fof(f83584,plain,
( spl0_5
| ~ spl0_37 ),
inference(avatar_contradiction_clause,[],[f83583]) ).
fof(f83617,plain,
( ! [X0] : hd(cons(X0,tl(cons(sk5,nil)))) = X0
| ~ spl0_1
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f14093,f410]) ).
fof(f83664,plain,
( ! [X0] : tl(cons(sk5,nil)) = tl(cons(X0,tl(cons(sk5,nil))))
| ~ spl0_1
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f20461,f410]) ).
fof(f83923,plain,
( ! [X0] : hd(cons(X0,nil)) = X0
| ~ spl0_1
| ~ spl0_14 ),
inference(forward_demodulation,[],[f83617,f1140]) ).
fof(f83965,plain,
( ! [X0] : nil = tl(cons(X0,nil))
| ~ spl0_1
| ~ spl0_14 ),
inference(forward_demodulation,[],[f83664,f1140]) ).
fof(f84303,plain,
( sk3 = cons(hd(sk3),nil)
| ~ spl0_1
| ~ spl0_9 ),
inference(superposition,[],[f2366,f8979]) ).
fof(f87485,plain,
( skaf44(sk3) = hd(sk3)
| ~ spl0_1
| ~ spl0_14 ),
inference(superposition,[],[f83923,f551]) ).
fof(f87499,plain,
( nil = tl(sk3)
| ~ spl0_1
| ~ spl0_14 ),
inference(superposition,[],[f83965,f551]) ).
fof(f87519,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| hd(sk3) = X0 )
| ~ spl0_1
| ~ spl0_14 ),
inference(forward_demodulation,[],[f7395,f87485]) ).
fof(f88006,plain,
( sk5 = hd(sk3)
| ~ spl0_1
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(resolution,[],[f87519,f5365]) ).
fof(f88007,plain,
( sk3 = cons(sk5,nil)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(superposition,[],[f84303,f88006]) ).
fof(f88046,plain,
( frontsegP(sk3,app(sk7,sk3))
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(superposition,[],[f5342,f88007]) ).
fof(f89473,plain,
( ~ ssList(sk3)
| ~ ssList(sk7)
| ~ frontsegP(sk7,sk3)
| ~ ssList(sk3)
| sk3 = app(sk7,sk3)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(resolution,[],[f88046,f1075]) ).
fof(f89479,plain,
( ~ ssList(sk3)
| ~ ssList(sk7)
| ~ frontsegP(sk7,sk3)
| sk3 = app(sk7,sk3)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f89473]) ).
fof(f89484,plain,
( ~ ssList(sk7)
| ~ frontsegP(sk7,sk3)
| sk3 = app(sk7,sk3)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f89479,f202]) ).
fof(f89489,plain,
( ~ frontsegP(sk7,sk3)
| sk3 = app(sk7,sk3)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f89484,f209]) ).
fof(f89490,plain,
( sk3 = app(sk7,sk3)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17
| ~ spl0_36 ),
inference(forward_subsumption_resolution,[],[f89489,f60399]) ).
fof(f89491,plain,
( $false
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17
| ~ spl0_36
| spl0_37 ),
inference(forward_subsumption_resolution,[],[f89490,f60403]) ).
fof(f89492,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17
| ~ spl0_36
| spl0_37 ),
inference(avatar_contradiction_clause,[],[f89491]) ).
fof(f89511,plain,
( nil != tl(sk3)
| ~ spl0_1
| spl0_9 ),
inference(superposition,[],[f2610,f8972]) ).
fof(f90136,plain,
( $false
| ~ spl0_1
| spl0_9
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f89511,f87499]) ).
fof(f90137,plain,
( ~ spl0_1
| spl0_9
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f90136]) ).
fof(f90146,plain,
( sk3 = cons(skaf83(sk3),nil)
| ~ spl0_9 ),
inference(superposition,[],[f2462,f2611]) ).
fof(f90160,plain,
( sk3 = cons(hd(sk3),nil)
| ~ spl0_1
| ~ spl0_9 ),
inference(forward_demodulation,[],[f90146,f7847]) ).
fof(f90161,plain,
( sk3 = cons(sk5,nil)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_demodulation,[],[f90160,f88006]) ).
fof(f96026,plain,
( ! [X0] :
( ~ memberP(app(sk7,sk3),X0)
| memberP(sk3,X0) )
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_demodulation,[],[f5363,f90161]) ).
fof(f96035,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssList(sk3)
| ~ ssList(sk7)
| ~ ssItem(X0)
| ~ memberP(sk7,X0) )
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(resolution,[],[f96026,f151]) ).
fof(f96036,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssList(sk7)
| ~ ssItem(X0)
| ~ memberP(sk7,X0) )
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f96035,f202]) ).
fof(f96037,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ memberP(sk7,X0) )
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f96036,f209]) ).
fof(f96038,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ memberP(sk7,X0) )
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f96037,f249]) ).
fof(f96039,plain,
( ! [X0] :
( ~ memberP(sk7,X0)
| hd(sk3) = X0 )
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(resolution,[],[f96038,f87519]) ).
fof(f96048,plain,
( ! [X0] :
( ~ memberP(sk7,X0)
| sk5 = X0 )
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_demodulation,[],[f96039,f88006]) ).
fof(f96051,plain,
( sk5 = hd(sk7)
| ~ spl0_1
| spl0_5
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(resolution,[],[f96048,f83384]) ).
fof(f96056,plain,
( sk7 = cons(sk5,tl(sk7))
| ~ spl0_1
| spl0_5
| ~ spl0_6
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(superposition,[],[f2430,f96051]) ).
fof(f96343,plain,
( ! [X0] : app(sk3,skaf82(X0)) = cons(hd(sk3),skaf82(X0))
| ~ spl0_1
| ~ spl0_14 ),
inference(forward_demodulation,[],[f10422,f87485]) ).
fof(f96344,plain,
( ! [X0] : cons(sk5,skaf82(X0)) = app(sk3,skaf82(X0))
| ~ spl0_1
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_demodulation,[],[f96343,f88006]) ).
fof(f96348,plain,
( cons(sk5,tl(sk7)) = app(sk3,tl(sk7))
| ~ spl0_1
| spl0_5
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(superposition,[],[f96344,f82961]) ).
fof(f96408,plain,
( sk7 = app(sk3,tl(sk7))
| ~ spl0_1
| spl0_5
| ~ spl0_6
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_demodulation,[],[f96348,f96056]) ).
fof(f99809,plain,
( frontsegP(sk7,sk3)
| ~ ssList(sk3)
| ~ ssList(tl(sk7))
| ~ spl0_1
| spl0_5
| ~ spl0_6
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(superposition,[],[f848,f96408]) ).
fof(f99824,plain,
( ~ ssList(sk3)
| ~ ssList(tl(sk7))
| ~ spl0_1
| spl0_5
| ~ spl0_6
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17
| spl0_36 ),
inference(forward_subsumption_resolution,[],[f99809,f60400]) ).
fof(f99845,plain,
( ~ ssList(tl(sk7))
| ~ spl0_1
| spl0_5
| ~ spl0_6
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17
| spl0_36 ),
inference(forward_subsumption_resolution,[],[f99824,f202]) ).
fof(f99858,plain,
( $false
| ~ spl0_1
| spl0_5
| ~ spl0_6
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17
| spl0_36 ),
inference(forward_subsumption_resolution,[],[f99845,f9003]) ).
fof(f99859,plain,
( ~ spl0_1
| spl0_5
| ~ spl0_6
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17
| spl0_36 ),
inference(avatar_contradiction_clause,[],[f99858]) ).
fof(f99884,plain,
( frontsegP(sk3,app(app(nil,cons(sk5,nil)),cons(sk5,nil)))
| ~ spl0_5
| ~ spl0_17 ),
inference(superposition,[],[f5280,f2426]) ).
fof(f99980,plain,
( frontsegP(sk3,app(app(nil,sk3),sk3))
| ~ spl0_1
| ~ spl0_5
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_demodulation,[],[f99884,f90161]) ).
fof(f99990,plain,
( frontsegP(sk3,app(sk3,sk3))
| ~ spl0_1
| ~ spl0_5
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_demodulation,[],[f99980,f314]) ).
fof(f100040,plain,
( ~ ssList(sk3)
| ~ ssList(sk3)
| sk3 = app(sk3,sk3)
| ~ spl0_1
| ~ spl0_5
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(resolution,[],[f99990,f878]) ).
fof(f100048,plain,
( ~ ssList(sk3)
| sk3 = app(sk3,sk3)
| ~ spl0_1
| ~ spl0_5
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f100040]) ).
fof(f100054,plain,
( sk3 = app(sk3,sk3)
| ~ spl0_1
| ~ spl0_5
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f100048,f202]) ).
fof(f100365,plain,
( sk3 != sk3
| ~ ssList(sk3)
| nil = sk3
| ~ spl0_1
| ~ spl0_5
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(superposition,[],[f1632,f100054]) ).
fof(f100417,plain,
( ~ ssList(sk3)
| nil = sk3
| ~ spl0_1
| ~ spl0_5
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(trivial_inequality_removal,[],[f100365]) ).
fof(f100429,plain,
( nil = sk3
| ~ spl0_1
| ~ spl0_5
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f100417,f202]) ).
fof(f100434,plain,
( $false
| ~ spl0_1
| ~ spl0_5
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f100429,f585]) ).
fof(f100435,plain,
( ~ spl0_1
| ~ spl0_5
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f100434]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f253]) ).
cnf(s3,plain,
( spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f2431]) ).
cnf(s8,plain,
spl0_14,
inference(sat_conversion,[],[f3701]) ).
cnf(s11,plain,
( ~ spl0_14
| spl0_16 ),
inference(sat_conversion,[],[f3961]) ).
cnf(s13,plain,
( ~ spl0_14
| ~ spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f4109]) ).
cnf(s14,plain,
( ~ spl0_2
| ~ spl0_17 ),
inference(sat_conversion,[],[f4301]) ).
cnf(s44,plain,
( spl0_5
| ~ spl0_37 ),
inference(sat_conversion,[],[f83584]) ).
cnf(s47,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17
| ~ spl0_36
| spl0_37 ),
inference(sat_conversion,[],[f89492]) ).
cnf(s48,plain,
( ~ spl0_1
| spl0_9
| ~ spl0_14 ),
inference(sat_conversion,[],[f90137]) ).
cnf(s51,plain,
( ~ spl0_1
| spl0_5
| ~ spl0_6
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17
| spl0_36 ),
inference(sat_conversion,[],[f99859]) ).
cnf(s60,plain,
( ~ spl0_1
| ~ spl0_5
| ~ spl0_9
| ~ spl0_14
| ~ spl0_16
| ~ spl0_17 ),
inference(sat_conversion,[],[f100435]) ).
cnf(s63,plain,
spl0_16,
inference(rat,[],[s11,s8]) ).
cnf(s66,plain,
spl0_17,
inference(rat,[],[s13,s8,s63]) ).
cnf(s67,plain,
~ spl0_2,
inference(rat,[],[s14,s66]) ).
cnf(s68,plain,
spl0_1,
inference(rat,[],[s1,s67]) ).
cnf(s69,plain,
spl0_9,
inference(rat,[],[s48,s8,s68]) ).
cnf(s70,plain,
~ spl0_5,
inference(rat,[],[s60,s66,s63,s8,s68,s69]) ).
cnf(s71,plain,
~ spl0_37,
inference(rat,[],[s44,s70]) ).
cnf(s72,plain,
spl0_6,
inference(rat,[],[s3,s70]) ).
cnf(s73,plain,
~ spl0_36,
inference(rat,[],[s47,s69,s68,s66,s63,s8,s71]) ).
cnf(s74,plain,
$false,
inference(rat,[],[s51,s70,s66,s63,s8,s69,s68,s73,s72]) ).
fof(f100436,plain,
$false,
inference(avatar_sat_refutation,[],[s74]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC166-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.38 % Computer : n011.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Mon Sep 28 08:15:01 UTC 2026
% 0.14/0.38 % CPUTime :
% 0.14/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/0.41 Running first-order model finding
% 0.14/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.00/2.41 % (3242180)Will run a generic schedule for satisfiability detection.
% 14.00/2.41 % (3242190)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1402094604:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.00/2.41 % (3242186)% WARNING: option uhcvi not known.
% 14.00/2.41 % (3242185)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3376652816_2999 on theBenchmark for (2999ds/0Mi)
% 14.00/2.41 % (3242187)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2521169180:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.00/2.41 % (3242188)dis+10_1_sil=32000:sp=arity:random_seed=2218031668:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.00/2.41 % (3242189)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3473429243:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.00/2.41 % (3242191)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1136156571:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.00/2.41 % (3242186)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2539324281:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.00/2.41 % TRYING [1]
% 14.00/2.41 % TRYING [2]
% 14.00/2.41 % TRYING [3]
% 14.00/2.41 % (3242190)Instruction limit reached!
% 14.00/2.41 % (3242190)------------------------------
% 14.00/2.41 % (3242190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.00/2.41 % (3242190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.00/2.41 % (3242190)CaDiCaL version: 2.1.3
% 14.00/2.41 % (3242190)Termination reason: Instruction limit
% 14.00/2.41 % (3242190)Termination phase: Saturation
% 14.00/2.41 % (3242190)Time elapsed: 0.036 s
% 14.00/2.41 % (3242190)Peak memory usage: 13 MB
% 14.00/2.41 % (3242190)Instructions burned: 132 (million)
% 14.00/2.41 % TRYING [4]
% 14.00/2.41 % (3242199)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=811685009:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.00/2.41 % TRYING [1]
% 14.00/2.41 % TRYING [2]
% 14.00/2.41 % TRYING [3]
% 14.00/2.41 % (3242188)Instruction limit reached!
% 14.00/2.41 % (3242188)------------------------------
% 14.00/2.41 % (3242188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.00/2.41 % (3242188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.00/2.41 % (3242188)CaDiCaL version: 2.1.3
% 14.00/2.41 % (3242188)Termination reason: Instruction limit
% 14.00/2.41 % (3242188)Termination phase: Saturation
% 14.00/2.41 % (3242188)Time elapsed: 0.061 s
% 14.00/2.41 % (3242188)Peak memory usage: 13 MB
% 14.00/2.41 % (3242188)Instructions burned: 103 (million)
% 14.00/2.41 % (3242189)Instruction limit reached!
% 14.00/2.41 % (3242189)------------------------------
% 14.00/2.41 % (3242189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.00/2.41 % (3242189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.00/2.41 % (3242189)CaDiCaL version: 2.1.3
% 14.00/2.41 % (3242189)Termination reason: Instruction limit
% 14.00/2.41 % (3242189)Termination phase: Saturation
% 14.00/2.41 % (3242189)Time elapsed: 0.061 s
% 14.00/2.41 % (3242189)Peak memory usage: 13 MB
% 14.00/2.41 % (3242189)Instructions burned: 116 (million)
% 14.00/2.41 % TRYING [4]
% 14.00/2.41 % (3242202)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=612876561:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 14.00/2.41 % (3242201)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1736278734:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.00/2.41 % TRYING [5]
% 14.00/2.41 % (3242191)Instruction limit reached!
% 14.00/2.41 % (3242191)------------------------------
% 14.00/2.41 % (3242191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.00/2.41 % (3242191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.00/2.41 % (3242191)CaDiCaL version: 2.1.3
% 14.00/2.41 % (3242191)Termination reason: Instruction limit
% 14.00/2.41 % (3242191)Termination phase: Saturation
% 14.00/2.41 % (3242191)Time elapsed: 0.095 s
% 14.00/2.41 % (3242191)Peak memory usage: 14 MB
% 14.00/2.41 % (3242191)Instructions burned: 160 (million)
% 14.00/2.41 % TRYING [5]
% 14.00/2.41 % (3242205)ott-21_1_sil=16000:fs=off:random_seed=1726632099:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.00/2.41 % (3242201)Instruction limit reached!
% 14.00/2.41 % (3242201)------------------------------
% 14.00/2.41 % (3242201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/4.00 % (3242201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/4.00 % (3242201)CaDiCaL version: 2.1.3
% 24.63/4.00 % (3242201)Termination reason: Instruction limit
% 24.63/4.00 % (3242201)Termination phase: Saturation
% 24.63/4.00 % (3242201)Time elapsed: 0.067 s
% 24.63/4.00 % (3242201)Peak memory usage: 13 MB
% 24.63/4.00 % (3242201)Instructions burned: 133 (million)
% 24.63/4.00 % (3242207)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2836249948:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 24.63/4.00 % TRYING [6]
% 24.63/4.00 % (3242199)Instruction limit reached!
% 24.63/4.00 % (3242199)------------------------------
% 24.63/4.00 % (3242199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/4.00 % (3242199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/4.00 % (3242199)CaDiCaL version: 2.1.3
% 24.63/4.00 % (3242199)Termination reason: Instruction limit
% 24.63/4.00 % (3242199)Termination phase: Finite model building constraint generation
% 24.63/4.00 % (3242199)Time elapsed: 0.151 s
% 24.63/4.00 % (3242199)Peak memory usage: 34 MB
% 24.63/4.00 % (3242199)Instructions burned: 722 (million)
% 24.63/4.00 % (3242209)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2685075483:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 24.63/4.00 % (3242205)Instruction limit reached!
% 24.63/4.00 % (3242205)------------------------------
% 24.63/4.00 % (3242205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/4.00 % (3242205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/4.00 % (3242205)CaDiCaL version: 2.1.3
% 24.63/4.00 % (3242205)Termination reason: Instruction limit
% 24.63/4.00 % (3242205)Termination phase: Saturation
% 24.63/4.00 % (3242205)Time elapsed: 0.089 s
% 24.63/4.00 % (3242205)Peak memory usage: 13 MB
% 24.63/4.00 % (3242205)Instructions burned: 181 (million)
% 24.63/4.00 % TRYING [1]
% 24.63/4.00 % TRYING [2]
% 24.63/4.00 % TRYING [3]
% 24.63/4.00 % (3242211)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=587723396:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 24.63/4.00 % TRYING [4]
% 24.63/4.00 % TRYING [6]
% 24.63/4.00 % TRYING [5]
% 24.63/4.00 % (3242209)Instruction limit reached!
% 24.63/4.00 % (3242209)------------------------------
% 24.63/4.00 % (3242209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/4.00 % (3242209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/4.00 % (3242209)CaDiCaL version: 2.1.3
% 24.63/4.00 % (3242209)Termination reason: Instruction limit
% 24.63/4.00 % (3242209)Termination phase: Finite model building SAT solving
% 24.63/4.00 % (3242209)Time elapsed: 0.178 s
% 24.63/4.00 % (3242209)Peak memory usage: 22 MB
% 24.63/4.00 % (3242209)Instructions burned: 868 (million)
% 24.63/4.00 % (3242213)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4105768738:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 24.63/4.00 % TRYING [14]
% 24.63/4.00 % (3242202)Instruction limit reached!
% 24.63/4.00 % (3242202)------------------------------
% 24.63/4.00 % (3242202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/4.00 % (3242202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/4.00 % (3242202)CaDiCaL version: 2.1.3
% 24.63/4.00 % (3242202)Termination reason: Instruction limit
% 24.63/4.00 % (3242202)Termination phase: Saturation
% 24.63/4.00 % (3242202)Time elapsed: 0.380 s
% 24.63/4.00 % (3242202)Peak memory usage: 19 MB
% 24.63/4.00 % (3242202)Instructions burned: 685 (million)
% 24.63/4.00 % (3242215)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=692822992:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 24.63/4.00 % (3242207)Instruction limit reached!
% 24.63/4.00 % (3242207)------------------------------
% 24.63/4.00 % (3242207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/4.00 % (3242207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/4.00 % (3242207)CaDiCaL version: 2.1.3
% 24.63/4.00 % (3242207)Termination reason: Instruction limit
% 24.63/4.00 % (3242207)Termination phase: Saturation
% 24.63/4.00 % (3242207)Time elapsed: 0.323 s
% 24.63/4.00 % (3242207)Peak memory usage: 14 MB
% 24.63/4.00 % (3242207)Instructions burned: 477 (million)
% 24.63/4.00 % (3242217)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3245861098:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 24.63/4.00 % (3242213)Instruction limit reached!
% 24.63/4.00 % (3242213)------------------------------
% 24.63/4.00 % (3242213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/4.00 % (3242213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/4.00 % (3242213)CaDiCaL version: 2.1.3
% 24.63/4.00 % (3242213)Termination reason: Instruction limit
% 24.63/4.00 % (3242213)Termination phase: Finite model building constraint generation
% 24.63/4.00 % (3242213)Time elapsed: 0.179 s
% 24.63/4.00 % (3242213)Peak memory usage: 72 MB
% 24.63/4.00 % (3242213)Instructions burned: 889 (million)
% 24.63/4.00 % (3242219)fmb+10_1_sil=64000:random_seed=4115325788:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 24.63/4.00 % TRYING [1]
% 24.63/4.00 % TRYING [2]
% 24.63/4.00 % TRYING [3]
% 24.63/4.00 % TRYING [4]
% 24.63/4.00 % TRYING [5]
% 24.63/4.00 % TRYING [7]
% 24.63/4.00 % (3242215)Instruction limit reached!
% 24.63/4.00 % (3242215)------------------------------
% 24.63/4.00 % (3242215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/4.00 % (3242215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/4.00 % (3242215)CaDiCaL version: 2.1.3
% 24.63/4.00 % (3242215)Termination reason: Instruction limit
% 24.63/4.00 % (3242215)Termination phase: Saturation
% 24.63/4.00 % (3242215)Time elapsed: 0.344 s
% 24.63/4.00 % (3242215)Peak memory usage: 19 MB
% 24.63/4.00 % (3242215)Instructions burned: 693 (million)
% 24.63/4.00 % (3242221)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4217544746:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 24.63/4.00 % TRYING [20]
% 24.63/4.00 % (3242211)Instruction limit reached!
% 24.63/4.00 % (3242211)------------------------------
% 24.63/4.00 % (3242211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/4.00 % (3242211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/4.00 % (3242211)CaDiCaL version: 2.1.3
% 24.63/4.00 % (3242211)Termination reason: Instruction limit
% 24.63/4.00 % (3242211)Termination phase: Saturation
% 24.63/4.00 % (3242211)Time elapsed: 0.682 s
% 24.63/4.00 % (3242211)Peak memory usage: 26 MB
% 24.63/4.00 % (3242211)Instructions burned: 1179 (million)
% 24.63/4.00 % TRYING [6]
% 24.63/4.00 % (3242223)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1639479268:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 24.63/4.00 % TRYING [8]
% 24.63/4.00 % (3242217)Instruction limit reached!
% 24.63/4.00 % (3242217)------------------------------
% 24.63/4.00 % (3242217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/4.00 % (3242217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/4.00 % (3242217)CaDiCaL version: 2.1.3
% 24.63/4.00 % (3242217)Termination reason: Instruction limit
% 24.63/4.00 % (3242217)Termination phase: Saturation
% 24.63/4.00 % (3242217)Time elapsed: 0.453 s
% 24.63/4.00 % (3242217)Peak memory usage: 19 MB
% 24.63/4.00 % (3242217)Instructions burned: 879 (million)
% 24.63/4.00 % (3242225)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=592030577:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 24.63/4.00 % (3242223)Instruction limit reached!
% 24.63/4.00 % (3242223)------------------------------
% 24.63/4.00 % (3242223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/4.00 % (3242223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/4.00 % (3242223)CaDiCaL version: 2.1.3
% 24.63/4.00 % (3242223)Termination reason: Instruction limit
% 24.63/4.00 % (3242223)Termination phase: Finite model building constraint generation
% 24.63/4.00 % (3242223)Time elapsed: 0.334 s
% 24.63/4.00 % (3242223)Peak memory usage: 79 MB
% 24.63/4.00 % (3242223)Instructions burned: 921 (million)
% 24.63/4.00 % (3242227)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=759814904:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 24.63/4.00 % TRYING [7]
% 24.63/4.00 % TRYING [8]
% 24.63/4.00 % (3242227)Instruction limit reached!
% 24.63/4.00 % (3242227)------------------------------
% 24.63/4.00 % (3242227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/4.00 % (3242227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/4.00 % (3242227)CaDiCaL version: 2.1.3
% 24.63/4.00 % (3242227)Termination reason: Instruction limit
% 24.63/4.00 % (3242227)Termination phase: Saturation
% 24.63/4.00 % (3242227)Time elapsed: 0.636 s
% 24.63/4.00 % (3242227)Peak memory usage: 15 MB
% 24.63/4.00 % (3242227)Instructions burned: 1472 (million)
% 24.63/4.00 % (3242229)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=626797434:i=6324_2980 on theBenchmark for (2980ds/6324Mi)
% 24.63/4.00 % TRYING [77]
% 24.63/4.00 % TRYING [8]
% 24.63/4.00 % (3242225) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3242180-3242225"...
% 24.63/4.00 % (3242225)...printing done.
% 24.63/4.00 % (3242225)Refutation found. Thanks to Tanya!
% 24.63/4.00 % SZS status Unsatisfiable for theBenchmark
% 24.63/4.00 % SZS output start Proof for theBenchmark
% See solution above
% 24.63/4.00 % (3242225)------------------------------
% 24.63/4.00 % (3242225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.63/4.00 % (3242225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.63/4.00 % (3242225)CaDiCaL version: 2.1.3
% 24.63/4.00 % (3242225)Termination reason: Refutation
% 24.63/4.00 % (3242225)Time elapsed: 2.473 s
% 24.63/4.00 % (3242225)Peak memory usage: 52 MB
% 24.63/4.00 % (3242225)Instructions burned: 4924 (million)
% 24.63/4.00 % (3242180)Success in time 3.579 s
% 24.63/4.00 % Vampire exiting
%------------------------------------------------------------------------------