%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC193-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 : n004.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:03 PM UTC 2026
% Result : Unsatisfiable 41.43s 11.83s
% Output : Refutation 41.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 82
% Syntax : Number of formulae : 462 ( 67 unt; 37 def)
% Number of atoms : 1518 ( 189 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 1652 ( 596 ~;1019 |; 0 &)
% ( 37 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 48 ( 46 usr; 38 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-2 aty)
% Number of variables : 285 ( 0 sgn 285 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f11,axiom,
~ singletonP(nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause11) ).
fof(f13,axiom,
! [X0] : ssList(skaf82(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause13) ).
fof(f58,axiom,
! [X0] :
( ~ ssList(X0)
| rearsegP(X0,nil) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause58) ).
fof(f60,axiom,
! [X0] :
( ~ ssList(X0)
| frontsegP(X0,nil) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause60) ).
fof(f71,axiom,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause71) ).
fof(f72,axiom,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f73,axiom,
! [X0] :
( ~ ssList(X0)
| app(X0,nil) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause73) ).
fof(f74,axiom,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause74) ).
fof(f75,axiom,
! [X0] :
( ~ ssList(X0)
| ssList(tl(X0))
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause75) ).
fof(f80,axiom,
! [X0] :
( ~ segmentP(nil,X0)
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause80) ).
fof(f85,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ssList(app(X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ssList(cons(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause86) ).
fof(f97,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| hd(cons(X0,X1)) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause97) ).
fof(f101,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| neq(X1,X0)
| X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause100) ).
fof(f102,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| neq(X1,X0)
| X0 = X1 ),
inference(reorient_equations,[],[f101]) ).
fof(f103,axiom,
! [X0] :
( ~ singletonP(X0)
| ~ ssList(X0)
| cons(skaf44(X0),nil) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause101) ).
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(f119,axiom,
! [X0,X1] :
( cons(X0,nil) != X1
| ~ ssItem(X0)
| ~ ssList(X1)
| singletonP(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause116) ).
fof(f121,axiom,
! [X0,X1] :
( app(X0,X1) != nil
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause118) ).
fof(f122,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X0 ),
inference(reorient_equations,[],[f121]) ).
fof(f136,axiom,
! [X0,X1] :
( ~ rearsegP(X0,X1)
| ~ rearsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause128) ).
fof(f137,plain,
! [X0,X1] :
( ~ rearsegP(X0,X1)
| ~ rearsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X0 = X1 ),
inference(reorient_equations,[],[f136]) ).
fof(f138,axiom,
! [X0,X1] :
( ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause129) ).
fof(f139,plain,
! [X0,X1] :
( ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X0 = X1 ),
inference(reorient_equations,[],[f138]) ).
fof(f148,axiom,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| frontsegP(app(X0,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause137) ).
fof(f154,axiom,
! [X2,X0,X1] :
( app(X0,X1) != X2
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| rearsegP(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause143) ).
fof(f155,axiom,
! [X2,X0,X1] :
( app(X0,X1) != X2
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| frontsegP(X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause144) ).
fof(f162,axiom,
! [X2,X0,X1] :
( app(X0,X1) != app(X0,X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause150) ).
fof(f166,axiom,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| frontsegP(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause154) ).
fof(f173,axiom,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X2 = X0 ),
file('/export/starexec/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(f184,axiom,
! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X3)
| ~ ssList(X1)
| X3 = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause171) ).
fof(f185,plain,
! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X3)
| ~ ssList(X1)
| X1 = X3 ),
inference(reorient_equations,[],[f184]) ).
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(f190,axiom,
! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ~ ssList(X3)
| ~ ssList(X1)
| ~ ssItem(X2)
| ~ ssItem(X0)
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause176) ).
fof(f192,axiom,
! [X2,X3,X0,X1] :
( ~ frontsegP(X0,X1)
| X2 != X3
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X2)
| frontsegP(cons(X2,X0),cons(X3,X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause178) ).
fof(f193,axiom,
! [X2,X3,X0,X1,X4] :
( app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(X4)
| ~ ssList(X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(f200,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_1) ).
fof(f201,negated_conjecture,
ssList(sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_2) ).
fof(f204,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_5) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
segmentP(sk4,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,
sk5 != sk6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_13) ).
fof(f214,negated_conjecture,
( singletonP(sk3)
| ~ neq(sk4,nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_14) ).
fof(f215,plain,
ssList(sk3),
inference(definition_unfolding,[],[f200,f205]) ).
fof(f216,plain,
ssList(sk4),
inference(definition_unfolding,[],[f201,f204]) ).
fof(f217,plain,
sk3 = app(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)),sk8),
inference(definition_unfolding,[],[f212,f205]) ).
fof(f225,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(cons(X0,nil))
| singletonP(cons(X0,nil)) ),
inference(equality_resolution,[],[f119]) ).
fof(f228,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(X0,X1))
| rearsegP(app(X0,X1),X1) ),
inference(equality_resolution,[],[f154]) ).
fof(f229,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1))
| frontsegP(app(X0,X1),X0) ),
inference(equality_resolution,[],[f155]) ).
fof(f233,plain,
! [X2,X0,X1] :
( ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(app(X0,cons(X1,X2)))
| memberP(app(X0,cons(X1,X2)),X1) ),
inference(equality_resolution,[],[f189]) ).
fof(f234,plain,
! [X3,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X3)
| frontsegP(cons(X3,X0),cons(X3,X1)) ),
inference(equality_resolution,[],[f192]) ).
fof(f235,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(f246,plain,
~ ssList(nil),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f249,plain,
singletonP(nil),
inference(consistent_polarity_flipping,[],[f11]) ).
fof(f251,plain,
! [X0] : ~ ssList(skaf82(X0)),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f295,plain,
! [X0] :
( rearsegP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f58]) ).
fof(f297,plain,
! [X0] :
( frontsegP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f308,plain,
! [X0] :
( memberP(nil,X0)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f71]) ).
fof(f309,plain,
! [X0,X1] :
( ssList(X0)
| ~ duplicatefreeP(X0)
| ~ ssItem(X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f310,plain,
! [X0] :
( ssList(X0)
| app(X0,nil) = X0 ),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f311,plain,
! [X0] :
( ssList(X0)
| app(nil,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f312,plain,
! [X0] :
( ~ ssList(tl(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f317,plain,
! [X0] :
( segmentP(nil,X0)
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f322,plain,
! [X0,X1] :
( ~ ssList(app(X1,X0))
| ssList(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f323,plain,
! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f334,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| hd(cons(X0,X1)) = X0 ),
inference(consistent_polarity_flipping,[],[f97]) ).
fof(f337,plain,
! [X0,X1] :
( ~ neq(X1,X0)
| ssList(X1)
| ssList(X0)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f102]) ).
fof(f338,plain,
! [X0] :
( singletonP(X0)
| ssList(X0)
| cons(skaf44(X0),nil) = X0 ),
inference(consistent_polarity_flipping,[],[f103]) ).
fof(f341,plain,
! [X0] :
( ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f346,plain,
! [X0] :
( ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f353,plain,
! [X0] :
( ~ singletonP(cons(X0,nil))
| ssList(cons(X0,nil))
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f225]) ).
fof(f355,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ssList(X1)
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f122]) ).
fof(f365,plain,
! [X0,X1] :
( ~ rearsegP(X1,X0)
| ~ rearsegP(X0,X1)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f137]) ).
fof(f366,plain,
! [X0,X1] :
( ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f374,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X2)
| ssList(X1)
| ssList(X0)
| frontsegP(app(X0,X2),X1) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f380,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X0,X1))
| rearsegP(app(X0,X1),X1) ),
inference(consistent_polarity_flipping,[],[f228]) ).
fof(f381,plain,
! [X0,X1] :
( ssList(X1)
| ssList(X0)
| ssList(app(X0,X1))
| frontsegP(app(X0,X1),X0) ),
inference(consistent_polarity_flipping,[],[f229]) ).
fof(f387,plain,
! [X2,X0,X1] :
( app(X0,X1) != app(X0,X2)
| ssList(X1)
| ssList(X0)
| ssList(X2)
| X1 = X2 ),
inference(consistent_polarity_flipping,[],[f162]) ).
fof(f391,plain,
! [X2,X0,X1] :
( ~ frontsegP(X1,X2)
| ~ frontsegP(X0,X1)
| ssList(X2)
| ssList(X1)
| ssList(X0)
| frontsegP(X0,X2) ),
inference(consistent_polarity_flipping,[],[f166]) ).
fof(f398,plain,
! [X2,X0,X1] :
( ~ memberP(X1,X2)
| ssList(X1)
| ssItem(X0)
| ssItem(X2)
| memberP(cons(X0,X1),X2)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f408,plain,
! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| ssItem(X2)
| ssItem(X0)
| ssList(X3)
| ssList(X1)
| X1 = X3 ),
inference(consistent_polarity_flipping,[],[f185]) ).
fof(f412,plain,
! [X2,X0,X1] :
( ~ memberP(app(X0,cons(X1,X2)),X1)
| ssList(X0)
| ssItem(X1)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2) ),
inference(consistent_polarity_flipping,[],[f233]) ).
fof(f413,plain,
! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ssList(X3)
| ssList(X1)
| ssItem(X2)
| ssItem(X0)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f190]) ).
fof(f415,plain,
! [X3,X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| ssItem(X3)
| ssItem(X3)
| frontsegP(cons(X3,X0),cons(X3,X1)) ),
inference(consistent_polarity_flipping,[],[f234]) ).
fof(f416,plain,
! [X2,X3,X0,X1] :
( ssList(X3)
| ssList(X2)
| ssList(X0)
| ssItem(X1)
| duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(consistent_polarity_flipping,[],[f235]) ).
fof(f423,plain,
~ ssList(sk3),
inference(consistent_polarity_flipping,[],[f215]) ).
fof(f424,plain,
~ ssList(sk4),
inference(consistent_polarity_flipping,[],[f216]) ).
fof(f427,plain,
~ segmentP(sk4,sk3),
inference(consistent_polarity_flipping,[],[f206]) ).
fof(f428,plain,
~ ssItem(sk5),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f429,plain,
~ ssItem(sk6),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f430,plain,
~ ssList(sk7),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f431,plain,
~ ssList(sk8),
inference(consistent_polarity_flipping,[],[f210]) ).
fof(f432,plain,
( ~ singletonP(sk3)
| neq(sk4,nil) ),
inference(consistent_polarity_flipping,[],[f214]) ).
fof(f433,plain,
! [X3,X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| ssItem(X3)
| frontsegP(cons(X3,X0),cons(X3,X1)) ),
inference(duplicate_literal_removal,[],[f415]) ).
fof(f440,definition,
( spl0_1
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f442,plain,
( neq(sk4,nil)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f440]) ).
fof(f444,definition,
( spl0_2
<=> singletonP(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f446,plain,
( ~ singletonP(sk3)
| spl0_2 ),
inference(avatar_component_clause,[],[f444]) ).
fof(f447,plain,
( spl0_1
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f432,f444,f440]) ).
fof(f453,definition,
( spl0_4
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f454,plain,
( ~ ssList(nil)
| spl0_4 ),
inference(avatar_component_clause,[],[f453]) ).
fof(f481,definition,
( spl0_10
<=> ! [X1] : ~ ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f482,plain,
( ! [X1] : ~ ssItem(X1)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f481]) ).
fof(f484,definition,
( spl0_11
<=> ! [X0] :
( ssList(X0)
| ~ duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f485,plain,
( ! [X0] :
( ~ duplicatefreeP(X0)
| ssList(X0) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f484]) ).
fof(f486,plain,
( spl0_10
| spl0_11 ),
inference(avatar_split_clause,[],[f309,f484,f481]) ).
fof(f489,plain,
~ spl0_4,
inference(avatar_split_clause,[],[f246,f453]) ).
fof(f493,plain,
( ! [X0] : memberP(nil,X0)
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f308,f482]) ).
fof(f530,plain,
sk3 = app(sk3,nil),
inference(resolution,[],[f310,f423]) ).
fof(f598,plain,
( ! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1) )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f323,f482]) ).
fof(f599,plain,
( ! [X0,X1] :
( ssList(X0)
| cons(X1,X0) = app(nil,cons(X1,X0)) )
| ~ spl0_10 ),
inference(resolution,[],[f598,f311]) ).
fof(f647,plain,
( ! [X0,X1] :
( ssList(X1)
| hd(cons(X0,X1)) = X0 )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f334,f482]) ).
fof(f649,plain,
( ! [X0,X1] : hd(cons(X0,skaf82(X1))) = X0
| ~ spl0_10 ),
inference(resolution,[],[f647,f251]) ).
fof(f681,plain,
( ! [X0] : hd(cons(X0,sk7)) = X0
| ~ spl0_10 ),
inference(resolution,[],[f647,f430]) ).
fof(f685,plain,
( ssList(sk3)
| sk3 = cons(skaf44(sk3),nil)
| spl0_2 ),
inference(resolution,[],[f338,f446]) ).
fof(f686,plain,
( sk3 = cons(skaf44(sk3),nil)
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f685,f423]) ).
fof(f744,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| nil = sk3 ),
inference(resolution,[],[f341,f423]) ).
fof(f758,definition,
( spl0_14
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f760,plain,
( nil = sk7
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f758]) ).
fof(f762,definition,
( spl0_15
<=> sk7 = cons(hd(sk7),tl(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f764,plain,
( sk7 = cons(hd(sk7),tl(sk7))
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f762]) ).
fof(f767,definition,
( spl0_16
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f769,plain,
( nil = sk4
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f767]) ).
fof(f776,definition,
( spl0_18
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f777,plain,
( nil != sk3
| spl0_18 ),
inference(avatar_component_clause,[],[f776]) ).
fof(f780,definition,
( spl0_19
<=> sk3 = cons(hd(sk3),tl(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f782,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f780]) ).
fof(f783,plain,
( spl0_18
| spl0_19 ),
inference(avatar_split_clause,[],[f744,f780,f776]) ).
fof(f826,definition,
( spl0_21
<=> sk7 = cons(skaf83(sk7),skaf82(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f828,plain,
( sk7 = cons(skaf83(sk7),skaf82(sk7))
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f826]) ).
fof(f856,plain,
( nil != sk3
| ssList(sk8)
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| nil = app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) ),
inference(superposition,[],[f355,f217]) ).
fof(f861,plain,
( nil != sk3
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| nil = app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) ),
inference(forward_subsumption_resolution,[],[f856,f431]) ).
fof(f863,definition,
( spl0_24
<=> nil = app(app(sk7,cons(sk5,nil)),cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f865,plain,
( nil = app(app(sk7,cons(sk5,nil)),cons(sk6,nil))
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f863]) ).
fof(f867,definition,
( spl0_25
<=> ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f869,plain,
( ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f867]) ).
fof(f870,plain,
( spl0_24
| spl0_25
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f861,f776,f867,f863]) ).
fof(f926,plain,
( ~ segmentP(nil,sk3)
| ~ spl0_16 ),
inference(superposition,[],[f427,f769]) ).
fof(f933,plain,
( ssList(sk3)
| nil = sk3
| ~ spl0_16 ),
inference(resolution,[],[f926,f317]) ).
fof(f934,plain,
( nil = sk3
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f933,f423]) ).
fof(f1005,plain,
! [X0,X1] :
( rearsegP(app(X0,X1),X1)
| ssList(X1)
| ssList(X0) ),
inference(forward_subsumption_resolution,[],[f380,f322]) ).
fof(f1006,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| ~ rearsegP(X0,app(X1,X0))
| ssList(X0)
| ssList(app(X1,X0))
| app(X1,X0) = X0 ),
inference(resolution,[],[f1005,f365]) ).
fof(f1027,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| ~ rearsegP(X0,app(X1,X0))
| ssList(app(X1,X0))
| app(X1,X0) = X0 ),
inference(duplicate_literal_removal,[],[f1006]) ).
fof(f1029,plain,
! [X0,X1] :
( ~ rearsegP(X0,app(X1,X0))
| ssList(X1)
| ssList(X0)
| app(X1,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f1027,f322]) ).
fof(f1037,definition,
( spl0_29
<=> ssList(app(app(nil,cons(sk5,nil)),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f1038,plain,
( ~ ssList(app(app(nil,cons(sk5,nil)),cons(sk6,nil)))
| spl0_29 ),
inference(avatar_component_clause,[],[f1037]) ).
fof(f1039,plain,
( ssList(app(app(nil,cons(sk5,nil)),cons(sk6,nil)))
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f1037]) ).
fof(f1047,plain,
! [X0,X1] :
( frontsegP(app(X0,X1),X0)
| ssList(X0)
| ssList(X1) ),
inference(forward_subsumption_resolution,[],[f381,f322]) ).
fof(f1048,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| ~ frontsegP(X0,app(X0,X1))
| ssList(X0)
| ssList(app(X0,X1))
| app(X0,X1) = X0 ),
inference(resolution,[],[f1047,f366]) ).
fof(f1063,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,[],[f1047,f217]) ).
fof(f1069,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| ~ frontsegP(X0,app(X0,X1))
| ssList(app(X0,X1))
| app(X0,X1) = X0 ),
inference(duplicate_literal_removal,[],[f1048]) ).
fof(f1070,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,[],[f1063,f431]) ).
fof(f1071,plain,
! [X0,X1] :
( ~ frontsegP(X0,app(X0,X1))
| ssList(X1)
| ssList(X0)
| app(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f1069,f322]) ).
fof(f1072,plain,
( frontsegP(sk3,app(app(nil,cons(sk5,nil)),cons(sk6,nil)))
| ssList(app(app(sk7,cons(sk5,nil)),cons(sk6,nil)))
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1070,f760]) ).
fof(f1073,plain,
( ssList(app(app(nil,cons(sk5,nil)),cons(sk6,nil)))
| frontsegP(sk3,app(app(nil,cons(sk5,nil)),cons(sk6,nil)))
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1072,f760]) ).
fof(f1075,definition,
( spl0_31
<=> frontsegP(sk3,app(app(nil,cons(sk5,nil)),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f1077,plain,
( frontsegP(sk3,app(app(nil,cons(sk5,nil)),cons(sk6,nil)))
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f1075]) ).
fof(f1199,plain,
! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X1,X2))
| frontsegP(app(app(X1,X2),X0),X1)
| ssList(X1)
| ssList(X2) ),
inference(resolution,[],[f374,f1047]) ).
fof(f1200,plain,
! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X1,X2))
| frontsegP(app(app(X1,X2),X0),X1)
| ssList(X2) ),
inference(duplicate_literal_removal,[],[f1199]) ).
fof(f1204,plain,
! [X2,X0,X1] :
( frontsegP(app(app(X1,X2),X0),X1)
| ssList(X1)
| ssList(X0)
| ssList(X2) ),
inference(forward_subsumption_resolution,[],[f1200,f322]) ).
fof(f1299,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,app(X1,X2))
| ssList(X1)
| ssList(app(X1,X2))
| ssList(X0)
| frontsegP(X0,X1)
| ssList(X1)
| ssList(X2) ),
inference(resolution,[],[f391,f1047]) ).
fof(f1300,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,app(X1,X2))
| ssList(X1)
| ssList(app(X1,X2))
| ssList(X0)
| frontsegP(X0,X1)
| ssList(X2) ),
inference(duplicate_literal_removal,[],[f1299]) ).
fof(f1304,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,app(X1,X2))
| ssList(X1)
| ssList(X0)
| frontsegP(X0,X1)
| ssList(X2) ),
inference(forward_subsumption_resolution,[],[f1300,f322]) ).
fof(f1429,plain,
! [X0] :
( sk3 != app(sk3,X0)
| ssList(X0)
| ssList(sk3)
| ssList(nil)
| nil = X0 ),
inference(superposition,[],[f387,f530]) ).
fof(f1440,plain,
! [X0] :
( sk3 != app(sk3,X0)
| ssList(X0)
| ssList(nil)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f1429,f423]) ).
fof(f1476,plain,
( ! [X0] :
( sk3 != app(sk3,X0)
| ssList(X0)
| nil = X0 )
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f1440,f454]) ).
fof(f1676,plain,
( ! [X3,X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| frontsegP(cons(X3,X0),cons(X3,X1)) )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f433,f482]) ).
fof(f1678,plain,
( ! [X0,X1] :
( ssList(nil)
| ssList(X0)
| frontsegP(cons(X1,X0),cons(X1,nil))
| ssList(X0) )
| ~ spl0_10 ),
inference(resolution,[],[f1676,f297]) ).
fof(f1683,plain,
( ! [X0,X1] :
( ssList(nil)
| ssList(X0)
| frontsegP(cons(X1,X0),cons(X1,nil)) )
| ~ spl0_10 ),
inference(duplicate_literal_removal,[],[f1678]) ).
fof(f1686,plain,
( ! [X0,X1] :
( frontsegP(cons(X1,X0),cons(X1,nil))
| ssList(X0) )
| spl0_4
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f1683,f454]) ).
fof(f1898,plain,
( ! [X2,X0,X1] :
( memberP(cons(X0,X1),X2)
| ssList(X1)
| ssItem(X0)
| ~ memberP(X1,X2)
| X0 = X2 )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f398,f482]) ).
fof(f1899,plain,
( ! [X2,X0,X1] :
( ~ memberP(X1,X2)
| ssList(X1)
| memberP(cons(X0,X1),X2)
| X0 = X2 )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f1898,f482]) ).
fof(f1900,plain,
( ! [X0,X1] :
( ssList(nil)
| memberP(cons(X0,nil),X1)
| X0 = X1 )
| ~ spl0_10 ),
inference(resolution,[],[f1899,f493]) ).
fof(f1901,plain,
( ! [X0,X1] :
( memberP(cons(X0,nil),X1)
| X0 = X1 )
| spl0_4
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f1900,f454]) ).
fof(f1943,plain,
( ! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| ssItem(X2)
| ssList(X3)
| ssList(X1)
| X1 = X3 )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f408,f482]) ).
fof(f1944,plain,
( ! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| ssList(X3)
| ssList(X1)
| X1 = X3 )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f1943,f482]) ).
fof(f1946,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk3
| ssList(nil)
| ssList(X1)
| nil = X1 )
| spl0_2
| ~ spl0_10 ),
inference(superposition,[],[f1944,f686]) ).
fof(f1949,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk3
| ssList(X1)
| nil = X1 )
| spl0_2
| spl0_4
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f1946,f454]) ).
fof(f2018,definition,
( spl0_38
<=> ssList(cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f2019,plain,
( ~ ssList(cons(sk6,nil))
| spl0_38 ),
inference(avatar_component_clause,[],[f2018]) ).
fof(f2020,plain,
( ssList(cons(sk6,nil))
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f2018]) ).
fof(f2025,definition,
( spl0_40
<=> ssList(app(nil,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f2026,plain,
( ~ ssList(app(nil,cons(sk5,nil)))
| spl0_40 ),
inference(avatar_component_clause,[],[f2025]) ).
fof(f2027,plain,
( ssList(app(nil,cons(sk5,nil)))
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f2025]) ).
fof(f2071,definition,
( spl0_47
<=> ssList(app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f2072,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| spl0_47 ),
inference(avatar_component_clause,[],[f2071]) ).
fof(f2073,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f2071]) ).
fof(f2182,plain,
( ssList(nil)
| ssItem(sk6)
| ~ spl0_38 ),
inference(resolution,[],[f323,f2020]) ).
fof(f2202,plain,
( ssItem(sk6)
| spl0_4
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f2182,f454]) ).
fof(f2203,plain,
( $false
| spl0_4
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f2202,f429]) ).
fof(f2204,plain,
( spl0_4
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f2203]) ).
fof(f2236,definition,
( spl0_57
<=> ssList(tl(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f2237,plain,
( ~ ssList(tl(sk3))
| spl0_57 ),
inference(avatar_component_clause,[],[f2236]) ).
fof(f2238,plain,
( ssList(tl(sk3))
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f2236]) ).
fof(f2401,definition,
( spl0_64
<=> nil = cons(sk6,nil) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f2402,plain,
( nil != cons(sk6,nil)
| spl0_64 ),
inference(avatar_component_clause,[],[f2401]) ).
fof(f2403,plain,
( nil = cons(sk6,nil)
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f2401]) ).
fof(f2502,definition,
( spl0_69
<=> nil = tl(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f2504,plain,
( nil = tl(sk3)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f2502]) ).
fof(f2593,plain,
( spl0_18
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f934,f767,f776]) ).
fof(f3148,plain,
( ! [X2,X3,X0,X1] :
( ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(X2)
| ssList(X0)
| ssItem(X1)
| ssList(X3) )
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f416,f485]) ).
fof(f3158,definition,
( spl0_100
<=> ! [X3] : ssList(X3) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f3159,plain,
( ! [X3] : ssList(X3)
| ~ spl0_100 ),
inference(avatar_component_clause,[],[f3158]) ).
fof(f3161,definition,
( spl0_101
<=> ! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X1,cons(X2,X0)))
| ssItem(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f3162,plain,
( ! [X2,X0,X1] :
( ssList(app(X1,cons(X2,X0)))
| ssList(X1)
| ssList(X0)
| ssItem(X2) )
| ~ spl0_101 ),
inference(avatar_component_clause,[],[f3161]) ).
fof(f3255,plain,
( ~ singletonP(nil)
| ssList(nil)
| ssItem(sk6)
| ~ spl0_64 ),
inference(superposition,[],[f353,f2403]) ).
fof(f3307,plain,
( ssList(nil)
| ssItem(sk6)
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f3255,f249]) ).
fof(f3331,plain,
( ssItem(sk6)
| spl0_4
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f3307,f454]) ).
fof(f3335,plain,
( $false
| spl0_4
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f3331,f429]) ).
fof(f3336,plain,
( spl0_4
| ~ spl0_64 ),
inference(avatar_contradiction_clause,[],[f3335]) ).
fof(f3341,plain,
( ssList(nil)
| ssList(cons(sk5,nil))
| ~ spl0_40 ),
inference(resolution,[],[f2027,f322]) ).
fof(f3342,plain,
( ssList(cons(sk5,nil))
| spl0_4
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f3341,f454]) ).
fof(f3384,plain,
( ssList(nil)
| ssItem(sk5)
| spl0_4
| ~ spl0_40 ),
inference(resolution,[],[f3342,f323]) ).
fof(f3385,plain,
( ssItem(sk5)
| spl0_4
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f3384,f454]) ).
fof(f3386,plain,
( $false
| spl0_4
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f3385,f428]) ).
fof(f3387,plain,
( spl0_4
| ~ spl0_40 ),
inference(avatar_contradiction_clause,[],[f3386]) ).
fof(f3449,plain,
( ssList(sk7)
| ssList(cons(sk5,nil))
| ~ spl0_47 ),
inference(resolution,[],[f2073,f322]) ).
fof(f3450,plain,
( ssList(cons(sk5,nil))
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f3449,f430]) ).
fof(f3451,plain,
( ssList(nil)
| ssItem(sk5)
| ~ spl0_47 ),
inference(resolution,[],[f3450,f323]) ).
fof(f3452,plain,
( ssItem(sk5)
| spl0_4
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f3451,f454]) ).
fof(f3453,plain,
( $false
| spl0_4
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f3452,f428]) ).
fof(f3454,plain,
( spl0_4
| ~ spl0_47 ),
inference(avatar_contradiction_clause,[],[f3453]) ).
fof(f3592,plain,
( ssList(sk4)
| ssList(nil)
| nil = sk4
| ~ spl0_1 ),
inference(resolution,[],[f442,f337]) ).
fof(f3593,plain,
( ssList(nil)
| nil = sk4
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f3592,f424]) ).
fof(f3599,plain,
( nil = sk4
| ~ spl0_1
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f3593,f454]) ).
fof(f3600,plain,
( spl0_16
| ~ spl0_1
| spl0_4 ),
inference(avatar_split_clause,[],[f3599,f453,f440,f767]) ).
fof(f3774,definition,
( spl0_142
<=> ssList(tl(sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f3775,plain,
( ~ ssList(tl(sk7))
| spl0_142 ),
inference(avatar_component_clause,[],[f3774]) ).
fof(f3776,plain,
( ssList(tl(sk7))
| ~ spl0_142 ),
inference(avatar_component_clause,[],[f3774]) ).
fof(f4338,plain,
( ssList(sk3)
| nil = sk3
| ~ spl0_57 ),
inference(resolution,[],[f2238,f312]) ).
fof(f4339,plain,
( nil = sk3
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f4338,f423]) ).
fof(f4340,plain,
( $false
| spl0_18
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f4339,f777]) ).
fof(f4341,plain,
( spl0_18
| ~ spl0_57 ),
inference(avatar_contradiction_clause,[],[f4340]) ).
fof(f4485,plain,
( ! [X0] : hd(cons(X0,nil)) = X0
| ~ spl0_10
| ~ spl0_14 ),
inference(forward_demodulation,[],[f681,f760]) ).
fof(f4571,plain,
( ! [X2,X0,X1] :
( ~ memberP(app(X0,cons(X1,X2)),X1)
| ssList(X0)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2) )
| ~ spl0_10 ),
inference(backward_subsumption_resolution,[],[f412,f482]) ).
fof(f4572,plain,
( ! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ssList(X3)
| ssList(X1)
| ssItem(X2)
| X0 = X2 )
| ~ spl0_10 ),
inference(backward_subsumption_resolution,[],[f413,f482]) ).
fof(f4605,plain,
( ! [X2,X3,X0,X1] :
( ~ frontsegP(cons(X0,X1),cons(X2,X3))
| ssList(X3)
| ssList(X1)
| X0 = X2 )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f4572,f482]) ).
fof(f4736,plain,
( sk3 = cons(hd(sk3),nil)
| ~ spl0_19
| ~ spl0_69 ),
inference(superposition,[],[f782,f2504]) ).
fof(f4947,plain,
( skaf44(sk3) = hd(sk3)
| spl0_2
| ~ spl0_10
| ~ spl0_14 ),
inference(superposition,[],[f4485,f686]) ).
fof(f5184,plain,
( ! [X0,X1] :
( ~ frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| ssList(tl(sk3))
| hd(sk3) = X0 )
| ~ spl0_10
| ~ spl0_19 ),
inference(superposition,[],[f4605,f782]) ).
fof(f5204,plain,
( ! [X0,X1] :
( ~ frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| hd(sk3) = X0 )
| ~ spl0_10
| ~ spl0_19
| spl0_57 ),
inference(forward_subsumption_resolution,[],[f5184,f2237]) ).
fof(f5952,plain,
( ssList(app(nil,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| ~ spl0_29 ),
inference(resolution,[],[f1039,f322]) ).
fof(f5953,plain,
( ssList(cons(sk6,nil))
| ~ spl0_29
| spl0_40 ),
inference(forward_subsumption_resolution,[],[f5952,f2026]) ).
fof(f5954,plain,
( $false
| ~ spl0_29
| spl0_38
| spl0_40 ),
inference(forward_subsumption_resolution,[],[f5953,f2019]) ).
fof(f5955,plain,
( ~ spl0_29
| spl0_38
| spl0_40 ),
inference(avatar_contradiction_clause,[],[f5954]) ).
fof(f6090,plain,
( ssList(sk7)
| nil = sk7
| ~ spl0_142 ),
inference(resolution,[],[f3776,f312]) ).
fof(f6091,plain,
( nil = sk7
| ~ spl0_142 ),
inference(forward_subsumption_resolution,[],[f6090,f430]) ).
fof(f6106,plain,
( spl0_31
| spl0_29
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f1073,f758,f1037,f1075]) ).
fof(f6130,plain,
( spl0_14
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f6091,f3774,f758]) ).
fof(f6168,definition,
( spl0_245
<=> nil = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[spl0_245])],[avatar_definition]) ).
fof(f6169,plain,
( nil != cons(sk5,nil)
| spl0_245 ),
inference(avatar_component_clause,[],[f6168]) ).
fof(f6170,plain,
( nil = cons(sk5,nil)
| ~ spl0_245 ),
inference(avatar_component_clause,[],[f6168]) ).
fof(f6172,definition,
( spl0_246
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_246])],[avatar_definition]) ).
fof(f6173,plain,
( ~ ssList(cons(sk5,nil))
| spl0_246 ),
inference(avatar_component_clause,[],[f6172]) ).
fof(f6174,plain,
( ssList(cons(sk5,nil))
| ~ spl0_246 ),
inference(avatar_component_clause,[],[f6172]) ).
fof(f7271,plain,
( ! [X2,X3,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssItem(X2)
| ssList(X3)
| ssList(app(X1,cons(X2,X0)))
| ssList(cons(X2,X3)) )
| ~ spl0_11 ),
inference(resolution,[],[f3148,f322]) ).
fof(f7296,plain,
( ! [X2,X3,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssItem(X2)
| ssList(X3)
| ssList(app(X1,cons(X2,X0))) )
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f7271,f323]) ).
fof(f7309,plain,
( spl0_100
| spl0_101
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f7296,f484,f3161,f3158]) ).
fof(f7417,plain,
( ~ singletonP(nil)
| ssList(nil)
| ssItem(sk5)
| ~ spl0_245 ),
inference(superposition,[],[f353,f6170]) ).
fof(f7453,plain,
( ssList(nil)
| ssItem(sk5)
| ~ spl0_245 ),
inference(forward_subsumption_resolution,[],[f7417,f249]) ).
fof(f7473,plain,
( ssItem(sk5)
| spl0_4
| ~ spl0_245 ),
inference(forward_subsumption_resolution,[],[f7453,f454]) ).
fof(f7477,plain,
( $false
| spl0_4
| ~ spl0_245 ),
inference(forward_subsumption_resolution,[],[f7473,f428]) ).
fof(f7478,plain,
( spl0_4
| ~ spl0_245 ),
inference(avatar_contradiction_clause,[],[f7477]) ).
fof(f7480,plain,
( ssList(nil)
| ssItem(sk5)
| ~ spl0_246 ),
inference(resolution,[],[f6174,f323]) ).
fof(f7481,plain,
( ssItem(sk5)
| spl0_4
| ~ spl0_246 ),
inference(forward_subsumption_resolution,[],[f7480,f454]) ).
fof(f7482,plain,
( $false
| spl0_4
| ~ spl0_246 ),
inference(forward_subsumption_resolution,[],[f7481,f428]) ).
fof(f7483,plain,
( spl0_4
| ~ spl0_246 ),
inference(avatar_contradiction_clause,[],[f7482]) ).
fof(f8012,plain,
( ~ frontsegP(app(app(nil,cons(sk5,nil)),cons(sk6,nil)),sk3)
| ssList(app(app(nil,cons(sk5,nil)),cons(sk6,nil)))
| ssList(sk3)
| sk3 = app(app(nil,cons(sk5,nil)),cons(sk6,nil))
| ~ spl0_31 ),
inference(resolution,[],[f1077,f366]) ).
fof(f8013,plain,
( ~ frontsegP(app(app(nil,cons(sk5,nil)),cons(sk6,nil)),sk3)
| ssList(sk3)
| sk3 = app(app(nil,cons(sk5,nil)),cons(sk6,nil))
| spl0_29
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f8012,f1038]) ).
fof(f8018,plain,
( ~ frontsegP(app(app(nil,cons(sk5,nil)),cons(sk6,nil)),sk3)
| sk3 = app(app(nil,cons(sk5,nil)),cons(sk6,nil))
| spl0_29
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f8013,f423]) ).
fof(f8024,definition,
( spl0_286
<=> sk3 = app(app(nil,cons(sk5,nil)),cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_286])],[avatar_definition]) ).
fof(f8026,plain,
( sk3 = app(app(nil,cons(sk5,nil)),cons(sk6,nil))
| ~ spl0_286 ),
inference(avatar_component_clause,[],[f8024]) ).
fof(f8028,definition,
( spl0_287
<=> frontsegP(app(app(nil,cons(sk5,nil)),cons(sk6,nil)),sk3) ),
introduced(definition,[new_symbols(definition,[spl0_287])],[avatar_definition]) ).
fof(f8030,plain,
( ~ frontsegP(app(app(nil,cons(sk5,nil)),cons(sk6,nil)),sk3)
| spl0_287 ),
inference(avatar_component_clause,[],[f8028]) ).
fof(f8031,plain,
( spl0_286
| ~ spl0_287
| spl0_29
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f8018,f1075,f1037,f8028,f8024]) ).
fof(f11830,plain,
( $false
| ~ spl0_100 ),
inference(backward_subsumption_resolution,[],[f431,f3159]) ).
fof(f11876,plain,
~ spl0_100,
inference(avatar_contradiction_clause,[],[f11830]) ).
fof(f14846,definition,
( spl0_385
<=> sk3 = sk7 ),
introduced(definition,[new_symbols(definition,[spl0_385])],[avatar_definition]) ).
fof(f14847,plain,
( sk3 = sk7
| ~ spl0_385 ),
inference(avatar_component_clause,[],[f14846]) ).
fof(f14856,plain,
( sk7 = cons(hd(sk7),tl(sk7))
| nil = sk7 ),
inference(resolution,[],[f430,f341]) ).
fof(f14857,plain,
( sk7 = cons(skaf83(sk7),skaf82(sk7))
| nil = sk7 ),
inference(resolution,[],[f430,f346]) ).
fof(f14915,plain,
( spl0_14
| spl0_21 ),
inference(avatar_split_clause,[],[f14857,f826,f758]) ).
fof(f14916,plain,
( spl0_14
| spl0_15 ),
inference(avatar_split_clause,[],[f14856,f762,f758]) ).
fof(f24250,plain,
( ssList(sk7)
| ssList(nil)
| ssItem(sk5)
| spl0_47
| ~ spl0_101 ),
inference(resolution,[],[f3162,f2072]) ).
fof(f24267,plain,
( ssList(nil)
| ssItem(sk5)
| spl0_47
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f24250,f430]) ).
fof(f24279,plain,
( ssItem(sk5)
| spl0_4
| spl0_47
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f24267,f454]) ).
fof(f24289,plain,
( $false
| spl0_4
| spl0_47
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f24279,f428]) ).
fof(f24290,plain,
( spl0_4
| spl0_47
| ~ spl0_101 ),
inference(avatar_contradiction_clause,[],[f24289]) ).
fof(f27198,plain,
( ! [X0] :
( memberP(sk3,X0)
| skaf44(sk3) = X0 )
| spl0_2
| spl0_4
| ~ spl0_10 ),
inference(superposition,[],[f1901,f686]) ).
fof(f27498,plain,
( ! [X0] : cons(X0,sk7) = app(nil,cons(X0,sk7))
| ~ spl0_10 ),
inference(resolution,[],[f599,f430]) ).
fof(f27499,plain,
( ! [X0] : cons(X0,nil) = app(nil,cons(X0,nil))
| ~ spl0_10
| ~ spl0_14 ),
inference(forward_demodulation,[],[f27498,f760]) ).
fof(f32294,plain,
( frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ssList(app(sk7,cons(sk5,nil)))
| ssList(sk8)
| ssList(cons(sk6,nil)) ),
inference(superposition,[],[f1204,f217]) ).
fof(f32303,plain,
( frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ssList(sk8)
| ssList(cons(sk6,nil))
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f32294,f2072]) ).
fof(f32341,plain,
( frontsegP(sk3,app(sk7,cons(sk5,nil)))
| ssList(sk8)
| spl0_38
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f32303,f2019]) ).
fof(f32350,plain,
( frontsegP(sk3,app(nil,cons(sk5,nil)))
| ssList(sk8)
| ~ spl0_14
| spl0_38
| spl0_47 ),
inference(forward_demodulation,[],[f32341,f760]) ).
fof(f59870,definition,
( spl0_746
<=> sk3 = cons(hd(sk3),nil) ),
introduced(definition,[new_symbols(definition,[spl0_746])],[avatar_definition]) ).
fof(f59872,plain,
( sk3 = cons(hd(sk3),nil)
| ~ spl0_746 ),
inference(avatar_component_clause,[],[f59870]) ).
fof(f60570,plain,
( spl0_746
| ~ spl0_19
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f4736,f2502,f780,f59870]) ).
fof(f64241,plain,
( ! [X0] :
( memberP(sk3,X0)
| hd(sk3) = X0 )
| spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_14 ),
inference(forward_demodulation,[],[f27198,f4947]) ).
fof(f85441,definition,
( spl0_1315
<=> sk3 = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[spl0_1315])],[avatar_definition]) ).
fof(f85443,plain,
( sk3 = cons(sk5,nil)
| ~ spl0_1315 ),
inference(avatar_component_clause,[],[f85441]) ).
fof(f85966,plain,
( sk3 != sk3
| ssList(tl(sk3))
| nil = tl(sk3)
| spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_19 ),
inference(superposition,[],[f1949,f782]) ).
fof(f85968,plain,
( ssList(tl(sk3))
| nil = tl(sk3)
| spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_19 ),
inference(trivial_inequality_removal,[],[f85966]) ).
fof(f111576,plain,
( sk3 = app(cons(sk5,nil),cons(sk6,nil))
| ~ spl0_10
| ~ spl0_14
| ~ spl0_286 ),
inference(forward_demodulation,[],[f8026,f27499]) ).
fof(f111578,plain,
( ~ memberP(sk3,sk6)
| ssList(cons(sk5,nil))
| ssList(sk3)
| ssList(nil)
| ~ spl0_10
| ~ spl0_14
| ~ spl0_286 ),
inference(superposition,[],[f4571,f111576]) ).
fof(f111649,plain,
( ~ memberP(sk3,sk6)
| ssList(sk3)
| ssList(nil)
| ~ spl0_10
| ~ spl0_14
| ~ spl0_286 ),
inference(forward_subsumption_resolution,[],[f111578,f598]) ).
fof(f111681,plain,
( ~ memberP(sk3,sk6)
| ssList(nil)
| ~ spl0_10
| ~ spl0_14
| ~ spl0_286 ),
inference(forward_subsumption_resolution,[],[f111649,f423]) ).
fof(f111684,plain,
( ~ memberP(sk3,sk6)
| spl0_4
| ~ spl0_10
| ~ spl0_14
| ~ spl0_286 ),
inference(forward_subsumption_resolution,[],[f111681,f454]) ).
fof(f111685,plain,
( ~ frontsegP(app(cons(sk5,nil),cons(sk6,nil)),sk3)
| ~ spl0_10
| ~ spl0_14
| spl0_287 ),
inference(forward_demodulation,[],[f8030,f27499]) ).
fof(f111691,plain,
( sk6 = hd(sk3)
| spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_14
| ~ spl0_286 ),
inference(resolution,[],[f111684,f64241]) ).
fof(f112403,definition,
( spl0_1818
<=> ssList(sk8) ),
introduced(definition,[new_symbols(definition,[spl0_1818])],[avatar_definition]) ).
fof(f112404,plain,
( ~ ssList(sk8)
| spl0_1818 ),
inference(avatar_component_clause,[],[f112403]) ).
fof(f112420,plain,
( frontsegP(sk3,cons(sk5,nil))
| ssList(sk8)
| ~ spl0_10
| ~ spl0_14
| spl0_38
| spl0_47 ),
inference(forward_demodulation,[],[f32350,f27499]) ).
fof(f112679,definition,
( spl0_1845
<=> frontsegP(sk3,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_1845])],[avatar_definition]) ).
fof(f112681,plain,
( frontsegP(sk3,cons(sk5,nil))
| ~ spl0_1845 ),
inference(avatar_component_clause,[],[f112679]) ).
fof(f112682,plain,
( spl0_1818
| spl0_1845
| ~ spl0_10
| ~ spl0_14
| spl0_38
| spl0_47 ),
inference(avatar_split_clause,[],[f112420,f2071,f2018,f758,f481,f112679,f112403]) ).
fof(f112794,plain,
~ spl0_1818,
inference(avatar_split_clause,[],[f431,f112403]) ).
fof(f118008,plain,
( ssList(nil)
| sk5 = hd(sk3)
| ~ spl0_10
| ~ spl0_19
| spl0_57
| ~ spl0_1845 ),
inference(resolution,[],[f112681,f5204]) ).
fof(f118019,plain,
( sk5 = hd(sk3)
| spl0_4
| ~ spl0_10
| ~ spl0_19
| spl0_57
| ~ spl0_1845 ),
inference(forward_subsumption_resolution,[],[f118008,f454]) ).
fof(f118024,plain,
( sk3 = cons(sk5,tl(sk3))
| spl0_4
| ~ spl0_10
| ~ spl0_19
| spl0_57
| ~ spl0_1845 ),
inference(superposition,[],[f782,f118019]) ).
fof(f118081,plain,
( sk3 = cons(sk5,nil)
| spl0_4
| ~ spl0_10
| ~ spl0_19
| spl0_57
| ~ spl0_69
| ~ spl0_1845 ),
inference(forward_demodulation,[],[f118024,f2504]) ).
fof(f118084,plain,
( spl0_1315
| spl0_4
| ~ spl0_10
| ~ spl0_19
| spl0_57
| ~ spl0_69
| ~ spl0_1845 ),
inference(avatar_split_clause,[],[f118081,f112679,f2502,f2236,f780,f481,f453,f85441]) ).
fof(f118438,plain,
( spl0_69
| spl0_57
| spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f85968,f780,f481,f453,f444,f2236,f2502]) ).
fof(f132507,plain,
( ~ frontsegP(app(sk3,cons(sk6,nil)),sk3)
| ~ spl0_10
| ~ spl0_14
| spl0_287
| ~ spl0_1315 ),
inference(forward_demodulation,[],[f111685,f85443]) ).
fof(f132508,plain,
( ssList(sk3)
| ssList(cons(sk6,nil))
| ~ spl0_10
| ~ spl0_14
| spl0_287
| ~ spl0_1315 ),
inference(resolution,[],[f132507,f1047]) ).
fof(f132509,plain,
( ssList(cons(sk6,nil))
| ~ spl0_10
| ~ spl0_14
| spl0_287
| ~ spl0_1315 ),
inference(forward_subsumption_resolution,[],[f132508,f423]) ).
fof(f132510,plain,
( $false
| ~ spl0_10
| ~ spl0_14
| spl0_38
| spl0_287
| ~ spl0_1315 ),
inference(forward_subsumption_resolution,[],[f132509,f2019]) ).
fof(f132511,plain,
( ~ spl0_10
| ~ spl0_14
| spl0_38
| spl0_287
| ~ spl0_1315 ),
inference(avatar_contradiction_clause,[],[f132510]) ).
fof(f132547,plain,
( sk5 = sk6
| spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_14
| ~ spl0_19
| spl0_57
| ~ spl0_286
| ~ spl0_1845 ),
inference(forward_demodulation,[],[f111691,f118019]) ).
fof(f132885,plain,
( $false
| spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_14
| ~ spl0_19
| spl0_57
| ~ spl0_286
| ~ spl0_1845 ),
inference(forward_subsumption_resolution,[],[f132547,f213]) ).
fof(f132886,plain,
( spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_14
| ~ spl0_19
| spl0_57
| ~ spl0_286
| ~ spl0_1845 ),
inference(avatar_contradiction_clause,[],[f132885]) ).
fof(f133654,plain,
( frontsegP(sk3,app(sk7,cons(sk5,nil)))
| spl0_38
| spl0_47
| spl0_1818 ),
inference(forward_subsumption_resolution,[],[f32341,f112404]) ).
fof(f137763,plain,
( frontsegP(sk7,cons(hd(sk7),nil))
| ssList(tl(sk7))
| spl0_4
| ~ spl0_10
| ~ spl0_15 ),
inference(superposition,[],[f1686,f764]) ).
fof(f137858,plain,
( frontsegP(sk7,cons(hd(sk7),nil))
| spl0_4
| ~ spl0_10
| ~ spl0_15
| spl0_142 ),
inference(forward_subsumption_resolution,[],[f137763,f3775]) ).
fof(f137881,definition,
( spl0_3219
<=> frontsegP(sk3,sk7) ),
introduced(definition,[new_symbols(definition,[spl0_3219])],[avatar_definition]) ).
fof(f137882,plain,
( frontsegP(sk3,sk7)
| ~ spl0_3219 ),
inference(avatar_component_clause,[],[f137881]) ).
fof(f137923,definition,
( spl0_3227
<=> frontsegP(sk7,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_3227])],[avatar_definition]) ).
fof(f137925,plain,
( ~ frontsegP(sk7,sk3)
| spl0_3227 ),
inference(avatar_component_clause,[],[f137923]) ).
fof(f137931,plain,
( hd(sk7) = skaf83(sk7)
| ~ spl0_10
| ~ spl0_21 ),
inference(superposition,[],[f649,f828]) ).
fof(f137973,plain,
( ~ frontsegP(sk3,sk7)
| ssList(skaf82(sk7))
| hd(sk3) = skaf83(sk7)
| ~ spl0_10
| ~ spl0_19
| ~ spl0_21
| spl0_57 ),
inference(superposition,[],[f5204,f828]) ).
fof(f138008,plain,
( ~ frontsegP(sk3,sk7)
| hd(sk3) = skaf83(sk7)
| ~ spl0_10
| ~ spl0_19
| ~ spl0_21
| spl0_57 ),
inference(forward_subsumption_resolution,[],[f137973,f251]) ).
fof(f145672,definition,
( spl0_3401
<=> hd(sk3) = hd(sk7) ),
introduced(definition,[new_symbols(definition,[spl0_3401])],[avatar_definition]) ).
fof(f145674,plain,
( hd(sk3) = hd(sk7)
| ~ spl0_3401 ),
inference(avatar_component_clause,[],[f145672]) ).
fof(f146543,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| ~ spl0_25 ),
inference(resolution,[],[f869,f322]) ).
fof(f146544,plain,
( ssList(cons(sk6,nil))
| ~ spl0_25
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f146543,f2072]) ).
fof(f146545,plain,
( $false
| ~ spl0_25
| spl0_38
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f146544,f2019]) ).
fof(f146546,plain,
( ~ spl0_25
| spl0_38
| spl0_47 ),
inference(avatar_contradiction_clause,[],[f146545]) ).
fof(f147478,plain,
( ~ rearsegP(cons(sk6,nil),nil)
| ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| nil = cons(sk6,nil)
| ~ spl0_24 ),
inference(superposition,[],[f1029,f865]) ).
fof(f147533,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ssList(cons(sk6,nil))
| nil = cons(sk6,nil)
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f147478,f295]) ).
fof(f147580,plain,
( ssList(cons(sk6,nil))
| nil = cons(sk6,nil)
| ~ spl0_24
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f147533,f2072]) ).
fof(f147619,plain,
( nil = cons(sk6,nil)
| ~ spl0_24
| spl0_38
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f147580,f2019]) ).
fof(f147634,plain,
( $false
| ~ spl0_24
| spl0_38
| spl0_47
| spl0_64 ),
inference(forward_subsumption_resolution,[],[f147619,f2402]) ).
fof(f147635,plain,
( ~ spl0_24
| spl0_38
| spl0_47
| spl0_64 ),
inference(avatar_contradiction_clause,[],[f147634]) ).
fof(f152386,plain,
( ssList(sk7)
| ssList(sk3)
| frontsegP(sk3,sk7)
| ssList(cons(sk5,nil))
| spl0_38
| spl0_47
| spl0_1818 ),
inference(resolution,[],[f133654,f1304]) ).
fof(f155156,plain,
( hd(sk3) = hd(sk7)
| ~ frontsegP(sk3,sk7)
| ~ spl0_10
| ~ spl0_19
| ~ spl0_21
| spl0_57 ),
inference(forward_demodulation,[],[f138008,f137931]) ).
fof(f155157,plain,
( ssList(sk3)
| frontsegP(sk3,sk7)
| ssList(cons(sk5,nil))
| spl0_38
| spl0_47
| spl0_1818 ),
inference(forward_subsumption_resolution,[],[f152386,f430]) ).
fof(f155161,plain,
( frontsegP(sk3,sk7)
| ssList(cons(sk5,nil))
| spl0_38
| spl0_47
| spl0_1818 ),
inference(forward_subsumption_resolution,[],[f155157,f423]) ).
fof(f155163,plain,
( frontsegP(sk3,sk7)
| spl0_38
| spl0_47
| spl0_246
| spl0_1818 ),
inference(forward_subsumption_resolution,[],[f155161,f6173]) ).
fof(f155164,plain,
( spl0_3219
| spl0_38
| spl0_47
| spl0_246
| spl0_1818 ),
inference(avatar_split_clause,[],[f155163,f112403,f6172,f2071,f2018,f137881]) ).
fof(f155215,plain,
( ~ frontsegP(sk7,sk3)
| ssList(sk7)
| ssList(sk3)
| sk3 = sk7
| ~ spl0_3219 ),
inference(resolution,[],[f137882,f366]) ).
fof(f159371,plain,
( ~ frontsegP(sk7,sk3)
| ssList(sk3)
| sk3 = sk7
| ~ spl0_3219 ),
inference(forward_subsumption_resolution,[],[f155215,f430]) ).
fof(f159378,plain,
( ~ frontsegP(sk7,sk3)
| sk3 = sk7
| ~ spl0_3219 ),
inference(forward_subsumption_resolution,[],[f159371,f423]) ).
fof(f159379,plain,
( spl0_385
| ~ spl0_3227
| ~ spl0_3219 ),
inference(avatar_split_clause,[],[f159378,f137881,f137923,f14846]) ).
fof(f159419,plain,
( frontsegP(sk3,app(sk3,cons(sk5,nil)))
| spl0_38
| spl0_47
| ~ spl0_385
| spl0_1818 ),
inference(superposition,[],[f133654,f14847]) ).
fof(f201296,definition,
( spl0_5062
<=> sk3 = app(sk3,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_5062])],[avatar_definition]) ).
fof(f201298,plain,
( sk3 = app(sk3,cons(sk5,nil))
| ~ spl0_5062 ),
inference(avatar_component_clause,[],[f201296]) ).
fof(f221100,plain,
( ssList(cons(sk5,nil))
| ssList(sk3)
| sk3 = app(sk3,cons(sk5,nil))
| spl0_38
| spl0_47
| ~ spl0_385
| spl0_1818 ),
inference(resolution,[],[f159419,f1071]) ).
fof(f221113,plain,
( ssList(sk3)
| sk3 = app(sk3,cons(sk5,nil))
| spl0_38
| spl0_47
| spl0_246
| ~ spl0_385
| spl0_1818 ),
inference(forward_subsumption_resolution,[],[f221100,f6173]) ).
fof(f221119,plain,
( sk3 = app(sk3,cons(sk5,nil))
| spl0_38
| spl0_47
| spl0_246
| ~ spl0_385
| spl0_1818 ),
inference(forward_subsumption_resolution,[],[f221113,f423]) ).
fof(f221121,plain,
( spl0_5062
| spl0_38
| spl0_47
| spl0_246
| ~ spl0_385
| spl0_1818 ),
inference(avatar_split_clause,[],[f221119,f112403,f14846,f6172,f2071,f2018,f201296]) ).
fof(f233094,plain,
( sk3 != sk3
| ssList(cons(sk5,nil))
| nil = cons(sk5,nil)
| spl0_4
| ~ spl0_5062 ),
inference(superposition,[],[f1476,f201298]) ).
fof(f233127,plain,
( ssList(cons(sk5,nil))
| nil = cons(sk5,nil)
| spl0_4
| ~ spl0_5062 ),
inference(trivial_inequality_removal,[],[f233094]) ).
fof(f233145,plain,
( nil = cons(sk5,nil)
| spl0_4
| spl0_246
| ~ spl0_5062 ),
inference(forward_subsumption_resolution,[],[f233127,f6173]) ).
fof(f233178,plain,
( $false
| spl0_4
| spl0_245
| spl0_246
| ~ spl0_5062 ),
inference(forward_subsumption_resolution,[],[f233145,f6169]) ).
fof(f233179,plain,
( spl0_4
| spl0_245
| spl0_246
| ~ spl0_5062 ),
inference(avatar_contradiction_clause,[],[f233178]) ).
fof(f234589,plain,
( hd(sk3) = hd(sk7)
| ~ spl0_10
| ~ spl0_19
| ~ spl0_21
| spl0_57
| ~ spl0_3219 ),
inference(forward_subsumption_resolution,[],[f155156,f137882]) ).
fof(f237337,plain,
( spl0_3401
| ~ spl0_10
| ~ spl0_19
| ~ spl0_21
| spl0_57
| ~ spl0_3219 ),
inference(avatar_split_clause,[],[f234589,f137881,f2236,f826,f780,f481,f145672]) ).
fof(f241922,plain,
( frontsegP(sk7,cons(hd(sk3),nil))
| spl0_4
| ~ spl0_10
| ~ spl0_15
| spl0_142
| ~ spl0_3401 ),
inference(superposition,[],[f137858,f145674]) ).
fof(f241931,plain,
( frontsegP(sk7,sk3)
| spl0_4
| ~ spl0_10
| ~ spl0_15
| spl0_142
| ~ spl0_746
| ~ spl0_3401 ),
inference(forward_demodulation,[],[f241922,f59872]) ).
fof(f241937,plain,
( $false
| spl0_4
| ~ spl0_10
| ~ spl0_15
| spl0_142
| ~ spl0_746
| spl0_3227
| ~ spl0_3401 ),
inference(forward_subsumption_resolution,[],[f241931,f137925]) ).
fof(f241938,plain,
( spl0_4
| ~ spl0_10
| ~ spl0_15
| spl0_142
| ~ spl0_746
| spl0_3227
| ~ spl0_3401 ),
inference(avatar_contradiction_clause,[],[f241937]) ).
cnf(s1,plain,
( spl0_1
| ~ spl0_2 ),
inference(sat_conversion,[],[f447]) ).
cnf(s8,plain,
( spl0_10
| spl0_11 ),
inference(sat_conversion,[],[f486]) ).
cnf(s11,plain,
~ spl0_4,
inference(sat_conversion,[],[f489]) ).
cnf(s15,plain,
( spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f783]) ).
cnf(s20,plain,
( ~ spl0_18
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f870]) ).
cnf(s66,plain,
( spl0_4
| ~ spl0_38 ),
inference(sat_conversion,[],[f2204]) ).
cnf(s97,plain,
( ~ spl0_16
| spl0_18 ),
inference(sat_conversion,[],[f2593]) ).
cnf(s143,plain,
( spl0_4
| ~ spl0_64 ),
inference(sat_conversion,[],[f3336]) ).
cnf(s144,plain,
( spl0_4
| ~ spl0_40 ),
inference(sat_conversion,[],[f3387]) ).
cnf(s154,plain,
( spl0_4
| ~ spl0_47 ),
inference(sat_conversion,[],[f3454]) ).
cnf(s196,plain,
( ~ spl0_1
| spl0_4
| spl0_16 ),
inference(sat_conversion,[],[f3600]) ).
cnf(s290,plain,
( spl0_18
| ~ spl0_57 ),
inference(sat_conversion,[],[f4341]) ).
cnf(s335,plain,
( ~ spl0_29
| spl0_38
| spl0_40 ),
inference(sat_conversion,[],[f5955]) ).
cnf(s368,plain,
( ~ spl0_14
| spl0_29
| spl0_31 ),
inference(sat_conversion,[],[f6106]) ).
cnf(s380,plain,
( spl0_14
| ~ spl0_142 ),
inference(sat_conversion,[],[f6130]) ).
cnf(s433,plain,
( ~ spl0_11
| spl0_100
| spl0_101 ),
inference(sat_conversion,[],[f7309]) ).
cnf(s438,plain,
( spl0_4
| ~ spl0_245 ),
inference(sat_conversion,[],[f7478]) ).
cnf(s439,plain,
( spl0_4
| ~ spl0_246 ),
inference(sat_conversion,[],[f7483]) ).
cnf(s451,plain,
( spl0_29
| ~ spl0_31
| spl0_286
| ~ spl0_287 ),
inference(sat_conversion,[],[f8031]) ).
cnf(s715,plain,
~ spl0_100,
inference(sat_conversion,[],[f11876]) ).
cnf(s815,plain,
( spl0_14
| spl0_21 ),
inference(sat_conversion,[],[f14915]) ).
cnf(s816,plain,
( spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f14916]) ).
cnf(s1128,plain,
( spl0_4
| spl0_47
| ~ spl0_101 ),
inference(sat_conversion,[],[f24290]) ).
cnf(s1593,plain,
( ~ spl0_19
| ~ spl0_69
| spl0_746 ),
inference(sat_conversion,[],[f60570]) ).
cnf(s2855,plain,
( ~ spl0_10
| ~ spl0_14
| spl0_38
| spl0_47
| spl0_1818
| spl0_1845 ),
inference(sat_conversion,[],[f112682]) ).
cnf(s2871,plain,
~ spl0_1818,
inference(sat_conversion,[],[f112794]) ).
cnf(s3053,plain,
( spl0_4
| ~ spl0_10
| ~ spl0_19
| spl0_57
| ~ spl0_69
| spl0_1315
| ~ spl0_1845 ),
inference(sat_conversion,[],[f118084]) ).
cnf(s3094,plain,
( spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_19
| spl0_57
| spl0_69 ),
inference(sat_conversion,[],[f118438]) ).
cnf(s4742,plain,
( ~ spl0_10
| ~ spl0_14
| spl0_38
| spl0_287
| ~ spl0_1315 ),
inference(sat_conversion,[],[f132511]) ).
cnf(s4757,plain,
( spl0_2
| spl0_4
| ~ spl0_10
| ~ spl0_14
| ~ spl0_19
| spl0_57
| ~ spl0_286
| ~ spl0_1845 ),
inference(sat_conversion,[],[f132886]) ).
cnf(s6365,plain,
( ~ spl0_25
| spl0_38
| spl0_47 ),
inference(sat_conversion,[],[f146546]) ).
cnf(s6606,plain,
( ~ spl0_24
| spl0_38
| spl0_47
| spl0_64 ),
inference(sat_conversion,[],[f147635]) ).
cnf(s7332,plain,
( spl0_38
| spl0_47
| spl0_246
| spl0_1818
| spl0_3219 ),
inference(sat_conversion,[],[f155164]) ).
cnf(s7577,plain,
( spl0_385
| ~ spl0_3219
| ~ spl0_3227 ),
inference(sat_conversion,[],[f159379]) ).
cnf(s10255,plain,
( spl0_38
| spl0_47
| spl0_246
| ~ spl0_385
| spl0_1818
| spl0_5062 ),
inference(sat_conversion,[],[f221121]) ).
cnf(s10451,plain,
( spl0_4
| spl0_245
| spl0_246
| ~ spl0_5062 ),
inference(sat_conversion,[],[f233179]) ).
cnf(s10758,plain,
( ~ spl0_10
| ~ spl0_19
| ~ spl0_21
| spl0_57
| ~ spl0_3219
| spl0_3401 ),
inference(sat_conversion,[],[f237337]) ).
cnf(s11065,plain,
( spl0_4
| ~ spl0_10
| ~ spl0_15
| spl0_142
| ~ spl0_746
| spl0_3227
| ~ spl0_3401 ),
inference(sat_conversion,[],[f241938]) ).
cnf(s11394,plain,
( ~ spl0_10
| ~ spl0_14
| spl0_38
| spl0_47
| spl0_1845 ),
inference(rat,[],[s2855,s2871]) ).
cnf(s11562,plain,
( ~ spl0_11
| spl0_101 ),
inference(rat,[],[s433,s715]) ).
cnf(s11594,plain,
~ spl0_246,
inference(rat,[],[s439,s11]) ).
cnf(s11595,plain,
~ spl0_245,
inference(rat,[],[s438,s11]) ).
cnf(s11596,plain,
~ spl0_47,
inference(rat,[],[s154,s11]) ).
cnf(s11597,plain,
~ spl0_40,
inference(rat,[],[s144,s11]) ).
cnf(s11598,plain,
~ spl0_64,
inference(rat,[],[s143,s11]) ).
cnf(s11599,plain,
~ spl0_38,
inference(rat,[],[s66,s11]) ).
cnf(s11619,plain,
~ spl0_5062,
inference(rat,[],[s10451,s11594,s11,s11595]) ).
cnf(s11625,plain,
~ spl0_101,
inference(rat,[],[s1128,s11,s11596]) ).
cnf(s11637,plain,
~ spl0_385,
inference(rat,[],[s10255,s11619,s2871,s11596,s11594,s11599]) ).
cnf(s11639,plain,
spl0_3219,
inference(rat,[],[s7332,s11596,s2871,s11594,s11599]) ).
cnf(s11640,plain,
~ spl0_24,
inference(rat,[],[s6606,s11598,s11596,s11599]) ).
cnf(s11641,plain,
~ spl0_25,
inference(rat,[],[s6365,s11596,s11599]) ).
cnf(s11652,plain,
~ spl0_29,
inference(rat,[],[s335,s11597,s11599]) ).
cnf(s11740,plain,
~ spl0_11,
inference(rat,[],[s11562,s11625]) ).
cnf(s11741,plain,
~ spl0_3227,
inference(rat,[],[s7577,s11637,s11639]) ).
cnf(s11742,plain,
~ spl0_18,
inference(rat,[],[s20,s11641,s11640]) ).
cnf(s12015,plain,
~ spl0_57,
inference(rat,[],[s290,s11742]) ).
cnf(s12018,plain,
~ spl0_16,
inference(rat,[],[s97,s11742]) ).
cnf(s12020,plain,
spl0_19,
inference(rat,[],[s15,s11742]) ).
cnf(s12366,plain,
~ spl0_1,
inference(rat,[],[s196,s11,s12018]) ).
cnf(s12862,plain,
spl0_10,
inference(rat,[],[s8,s11740]) ).
cnf(s13552,plain,
~ spl0_2,
inference(rat,[],[s1,s12366]) ).
cnf(s13555,plain,
spl0_69,
inference(rat,[],[s3094,s12862,s12015,s12020,s11,s13552]) ).
cnf(s13666,plain,
spl0_746,
inference(rat,[],[s1593,s12020,s13555]) ).
cnf(s13683,plain,
spl0_14,
inference(rat,[],[s11065,s10758,s380,s815,s816,s11,s12862,s13666,s11741,s12020,s12015,s11639]) ).
cnf(s13687,plain,
spl0_1845,
inference(rat,[],[s11394,s12862,s11596,s11599,s13683]) ).
cnf(s13748,plain,
spl0_31,
inference(rat,[],[s368,s11652,s13683]) ).
cnf(s13755,plain,
~ spl0_286,
inference(rat,[],[s4757,s13687,s13552,s12015,s12020,s12862,s11,s13683]) ).
cnf(s13827,plain,
spl0_1315,
inference(rat,[],[s3053,s13555,s12862,s12020,s12015,s11,s13687]) ).
cnf(s13960,plain,
~ spl0_287,
inference(rat,[],[s451,s13748,s11652,s13755]) ).
cnf(s13973,plain,
$false,
inference(rat,[],[s4742,s13683,s12862,s11599,s13827,s13960]) ).
fof(f241941,plain,
$false,
inference(avatar_sat_refutation,[],[s13973]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC193-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.12/0.39 % Computer : n004.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Mon Sep 28 08:22:53 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.44 Running first-order model finding
% 0.12/0.44 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
% 44.39/6.71 % (208032)Will run a generic schedule for satisfiability detection.
% 44.39/6.71 % (208039)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3617882960:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 44.39/6.71 % (208038)% WARNING: option uhcvi not known.
% 44.39/6.71 % (208038)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1592290377:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 44.39/6.71 % (208037)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3122333406_2999 on theBenchmark for (2999ds/0Mi)
% 44.39/6.71 % (208043)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4231673388:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 44.39/6.71 % (208040)dis+10_1_sil=32000:sp=arity:random_seed=1347506782:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 44.39/6.71 % (208041)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2963426903:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 44.39/6.71 % (208042)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1746330684:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 44.39/6.71 % TRYING [1]
% 44.39/6.71 % TRYING [2]
% 44.39/6.71 % TRYING [3]
% 44.39/6.71 % TRYING [4]
% 44.39/6.71 % (208040)Instruction limit reached!
% 44.39/6.71 % (208040)------------------------------
% 44.39/6.71 % (208040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.39/6.71 % (208040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.39/6.71 % (208040)CaDiCaL version: 2.1.3
% 44.39/6.71 % (208040)Termination reason: Instruction limit
% 44.39/6.71 % (208040)Termination phase: Saturation
% 44.39/6.71 % (208040)Time elapsed: 0.088 s
% 44.39/6.71 % (208040)Peak memory usage: 13 MB
% 44.39/6.71 % (208040)Instructions burned: 104 (million)
% 44.39/6.71 % (208041)Instruction limit reached!
% 44.39/6.71 % (208041)------------------------------
% 44.39/6.71 % (208041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.39/6.71 % (208041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.39/6.71 % (208041)CaDiCaL version: 2.1.3
% 44.39/6.71 % (208041)Termination reason: Instruction limit
% 44.39/6.71 % (208041)Termination phase: Saturation
% 44.39/6.71 % (208041)Time elapsed: 0.102 s
% 44.39/6.71 % (208041)Peak memory usage: 13 MB
% 44.39/6.71 % (208041)Instructions burned: 116 (million)
% 44.39/6.71 % (208042)Instruction limit reached!
% 44.39/6.71 % (208042)------------------------------
% 44.39/6.71 % (208042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.39/6.71 % (208042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.39/6.71 % (208042)CaDiCaL version: 2.1.3
% 44.39/6.71 % (208042)Termination reason: Instruction limit
% 44.39/6.71 % (208042)Termination phase: Saturation
% 44.39/6.71 % (208042)Time elapsed: 0.100 s
% 44.39/6.71 % (208042)Peak memory usage: 14 MB
% 44.39/6.71 % (208042)Instructions burned: 132 (million)
% 44.39/6.71 % (208052)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=273677408:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 44.39/6.71 % TRYING [1]
% 44.39/6.71 % TRYING [2]
% 44.39/6.71 % TRYING [3]
% 44.39/6.71 % (208054)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=1181466322:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 44.39/6.71 % (208053)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3186495123:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 44.39/6.71 % TRYING [4]
% 44.39/6.71 % (208043)Instruction limit reached!
% 44.39/6.71 % (208043)------------------------------
% 44.39/6.71 % (208043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.39/6.71 % (208043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.39/6.71 % (208043)CaDiCaL version: 2.1.3
% 44.39/6.71 % (208043)Termination reason: Instruction limit
% 44.39/6.71 % (208043)Termination phase: Saturation
% 44.39/6.71 % (208043)Time elapsed: 0.154 s
% 44.39/6.71 % (208043)Peak memory usage: 14 MB
% 44.39/6.71 % (208043)Instructions burned: 159 (million)
% 44.39/6.71 % (208060)ott-21_1_sil=16000:fs=off:random_seed=1244116795:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 44.39/6.71 % TRYING [5]
% 44.39/6.71 % (208053)Instruction limit reached!
% 44.39/6.71 % (208053)------------------------------
% 44.39/6.71 % (208053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.39/6.71 % (208053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208053)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208053)Termination reason: Instruction limit
% 41.43/11.83 % (208053)Termination phase: Saturation
% 41.43/11.83 % (208053)Time elapsed: 0.129 s
% 41.43/11.83 % (208053)Peak memory usage: 14 MB
% 41.43/11.83 % (208053)Instructions burned: 131 (million)
% 41.43/11.83 % TRYING [5]
% 41.43/11.83 % (208065)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1427594032:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 41.43/11.83 % (208060)Instruction limit reached!
% 41.43/11.83 % (208060)------------------------------
% 41.43/11.83 % (208060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.83 % (208060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208060)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208060)Termination reason: Instruction limit
% 41.43/11.83 % (208060)Termination phase: Saturation
% 41.43/11.83 % (208060)Time elapsed: 0.148 s
% 41.43/11.83 % (208060)Peak memory usage: 13 MB
% 41.43/11.83 % (208060)Instructions burned: 181 (million)
% 41.43/11.83 % (208067)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=148571370:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 41.43/11.83 % TRYING [1]
% 41.43/11.83 % TRYING [2]
% 41.43/11.83 % TRYING [3]
% 41.43/11.83 % TRYING [4]
% 41.43/11.83 % TRYING [6]
% 41.43/11.83 % TRYING [5]
% 41.43/11.83 % TRYING [6]
% 41.43/11.83 % (208052)Instruction limit reached!
% 41.43/11.83 % (208052)------------------------------
% 41.43/11.83 % (208052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.83 % (208052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208052)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208052)Termination reason: Instruction limit
% 41.43/11.83 % (208052)Termination phase: Finite model building constraint generation
% 41.43/11.83 % (208052)Time elapsed: 0.499 s
% 41.43/11.83 % (208052)Peak memory usage: 34 MB
% 41.43/11.83 % (208052)Instructions burned: 715 (million)
% 41.43/11.83 % (208074)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2064583576:i=1179_2993 on theBenchmark for (2993ds/1179Mi)
% 41.43/11.83 % (208054)Instruction limit reached!
% 41.43/11.83 % (208054)------------------------------
% 41.43/11.83 % (208054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.83 % (208054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208054)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208054)Termination reason: Instruction limit
% 41.43/11.83 % (208054)Termination phase: Saturation
% 41.43/11.83 % (208054)Time elapsed: 0.642 s
% 41.43/11.83 % (208054)Peak memory usage: 21 MB
% 41.43/11.83 % (208054)Instructions burned: 684 (million)
% 41.43/11.83 % (208065)Instruction limit reached!
% 41.43/11.83 % (208065)------------------------------
% 41.43/11.83 % (208065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.83 % (208065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208065)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208065)Termination reason: Instruction limit
% 41.43/11.83 % (208065)Termination phase: Saturation
% 41.43/11.83 % (208065)Time elapsed: 0.488 s
% 41.43/11.83 % (208065)Peak memory usage: 14 MB
% 41.43/11.83 % (208065)Instructions burned: 477 (million)
% 41.43/11.83 % (208079)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2747415328:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 41.43/11.83 % (208080)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=1111131474:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 41.43/11.83 % (208067)Instruction limit reached!
% 41.43/11.83 % (208067)------------------------------
% 41.43/11.83 % (208067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.83 % (208067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208067)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208067)Termination reason: Instruction limit
% 41.43/11.83 % (208067)Termination phase: Finite model building SAT solving
% 41.43/11.83 % (208067)Time elapsed: 0.556 s
% 41.43/11.83 % (208067)Peak memory usage: 22 MB
% 41.43/11.83 % (208067)Instructions burned: 867 (million)
% 41.43/11.83 % (208086)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4152577030:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 41.43/11.83 % TRYING [14]
% 41.43/11.83 % TRYING [7]
% 41.43/11.83 % (208079)Instruction limit reached!
% 41.43/11.83 % (208079)------------------------------
% 41.43/11.83 % (208079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.83 % (208079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208079)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208079)Termination reason: Instruction limit
% 41.43/11.83 % (208079)Termination phase: Finite model building constraint generation
% 41.43/11.83 % (208079)Time elapsed: 0.659 s
% 41.43/11.83 % (208079)Peak memory usage: 72 MB
% 41.43/11.83 % (208079)Instructions burned: 890 (million)
% 41.43/11.83 % (208080)Instruction limit reached!
% 41.43/11.83 % (208080)------------------------------
% 41.43/11.83 % (208080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.83 % (208080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208080)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208080)Termination reason: Instruction limit
% 41.43/11.83 % (208080)Termination phase: Saturation
% 41.43/11.83 % (208080)Time elapsed: 0.694 s
% 41.43/11.83 % (208080)Peak memory usage: 21 MB
% 41.43/11.83 % (208080)Instructions burned: 692 (million)
% 41.43/11.83 % (208092)fmb+10_1_sil=64000:random_seed=2346537151:i=22061:nm=2:gsp=on_2984 on theBenchmark for (2984ds/22061Mi)
% 41.43/11.83 % TRYING [1]
% 41.43/11.83 % TRYING [2]
% 41.43/11.83 % (208094)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1312393191:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 41.43/11.83 % TRYING [20]
% 41.43/11.83 % TRYING [3]
% 41.43/11.83 % TRYING [4]
% 41.43/11.83 % (208086)Instruction limit reached!
% 41.43/11.83 % (208086)------------------------------
% 41.43/11.83 % (208086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.83 % (208086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208086)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208086)Termination reason: Instruction limit
% 41.43/11.83 % (208086)Termination phase: Saturation
% 41.43/11.83 % (208086)Time elapsed: 0.776 s
% 41.43/11.83 % (208086)Peak memory usage: 21 MB
% 41.43/11.83 % (208086)Instructions burned: 880 (million)
% 41.43/11.83 % (208098)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1790147742:fmbsr=1.7:i=920_2982 on theBenchmark for (2982ds/920Mi)
% 41.43/11.83 % TRYING [8]
% 41.43/11.83 % (208074)Instruction limit reached!
% 41.43/11.83 % (208074)------------------------------
% 41.43/11.83 % (208074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.83 % (208074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208074)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208074)Termination reason: Instruction limit
% 41.43/11.83 % (208074)Termination phase: Saturation
% 41.43/11.83 % (208074)Time elapsed: 1.122 s
% 41.43/11.83 % (208074)Peak memory usage: 27 MB
% 41.43/11.83 % (208074)Instructions burned: 1180 (million)
% 41.43/11.83 % (208100)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=502734001:i=5131_2981 on theBenchmark for (2981ds/5131Mi)
% 41.43/11.83 % TRYING [5]
% 41.43/11.83 % (208098)Instruction limit reached!
% 41.43/11.83 % (208098)------------------------------
% 41.43/11.83 % (208098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.83 % (208098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208098)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208098)Termination reason: Instruction limit
% 41.43/11.83 % (208098)Termination phase: Finite model building constraint generation
% 41.43/11.83 % (208098)Time elapsed: 0.658 s
% 41.43/11.83 % (208098)Peak memory usage: 79 MB
% 41.43/11.83 % (208098)Instructions burned: 920 (million)
% 41.43/11.83 % (208108)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3247476657:i=1472:ins=7:fdi=8:gsp=on_2975 on theBenchmark for (2975ds/1472Mi)
% 41.43/11.83 % TRYING [6]
% 41.43/11.83 % TRYING [8]
% 41.43/11.83 % (208108)Instruction limit reached!
% 41.43/11.83 % (208108)------------------------------
% 41.43/11.83 % (208108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.83 % (208108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208108)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208108)Termination reason: Instruction limit
% 41.43/11.83 % (208108)Termination phase: Saturation
% 41.43/11.83 % (208108)Time elapsed: 1.132 s
% 41.43/11.83 % (208108)Peak memory usage: 15 MB
% 41.43/11.83 % (208108)Instructions burned: 1474 (million)
% 41.43/11.83 % (208118)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=494824211:i=6324_2963 on theBenchmark for (2963ds/6324Mi)
% 41.43/11.83 % TRYING [77]
% 41.43/11.83 % TRYING [7]
% 41.43/11.83 % (208100)Instruction limit reached!
% 41.43/11.83 % (208100)------------------------------
% 41.43/11.83 % (208100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.83 % (208100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208100)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208100)Termination reason: Instruction limit
% 41.43/11.83 % (208100)Termination phase: Saturation
% 41.43/11.83 % (208100)Time elapsed: 4.428 s
% 41.43/11.83 % (208100)Peak memory usage: 52 MB
% 41.43/11.83 % (208100)Instructions burned: 5131 (million)
% 41.43/11.83 % (208123)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2254115170:fmbsr=2.30978:i=2174_2937 on theBenchmark for (2937ds/2174Mi)
% 41.43/11.83 % TRYING [16]
% 41.43/11.83 % TRYING [8]
% 41.43/11.83 % TRYING [9]
% 41.43/11.83 % (208118)Instruction limit reached!
% 41.43/11.83 % (208118)------------------------------
% 41.43/11.83 % (208118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.83 % (208118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208118)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208118)Termination reason: Instruction limit
% 41.43/11.83 % (208118)Termination phase: Finite model building constraint generation
% 41.43/11.83 % (208118)Time elapsed: 4.110 s
% 41.43/11.83 % (208118)Peak memory usage: 423 MB
% 41.43/11.83 % (208118)Instructions burned: 6326 (million)
% 41.43/11.83 % (208123)Instruction limit reached!
% 41.43/11.83 % (208123)------------------------------
% 41.43/11.83 % (208123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.83 % (208123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208123)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208123)Termination reason: Instruction limit
% 41.43/11.83 % (208123)Termination phase: Finite model building constraint generation
% 41.43/11.83 % (208123)Time elapsed: 1.538 s
% 41.43/11.83 % (208123)Peak memory usage: 137 MB
% 41.43/11.83 % (208123)Instructions burned: 2175 (million)
% 41.43/11.83 % (208135)ott-2_1_sil=16000:newcnf=on:random_seed=415499721:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2921 on theBenchmark for (2921ds/869Mi)
% 41.43/11.83 % (208136)ott+10_1_sil=32000:tgt=ground:random_seed=1274361270:i=5114:av=off_2921 on theBenchmark for (2921ds/5114Mi)
% 41.43/11.83 % (208094)Instruction limit reached!
% 41.43/11.83 % (208094)------------------------------
% 41.43/11.83 % (208094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.83 % (208094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208094)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208094)Termination reason: Instruction limit
% 41.43/11.83 % (208094)Termination phase: Finite model building constraint generation
% 41.43/11.83 % (208094)Time elapsed: 6.617 s
% 41.43/11.83 % (208094)Peak memory usage: 588 MB
% 41.43/11.83 % (208094)Instructions burned: 9515 (million)
% 41.43/11.83 % (208139)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1512096441:i=54282_2916 on theBenchmark for (2916ds/54282Mi)
% 41.43/11.83 % TRYING [1]
% 41.43/11.83 % TRYING [2]
% 41.43/11.83 % TRYING [3]
% 41.43/11.83 % TRYING [4]
% 41.43/11.83 % TRYING [5]
% 41.43/11.83 % (208135)Instruction limit reached!
% 41.43/11.83 % (208135)------------------------------
% 41.43/11.83 % (208135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.83 % (208135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.83 % (208135)CaDiCaL version: 2.1.3
% 41.43/11.83 % (208135)Termination reason: Instruction limit
% 41.43/11.83 % (208135)Termination phase: Saturation
% 41.43/11.83 % (208135)Time elapsed: 0.776 s
% 41.43/11.83 % (208135)Peak memory usage: 23 MB
% 41.43/11.83 % (208135)Instructions burned: 869 (million)
% 41.43/11.83 % (208141)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2644704902:i=3512:aac=none_2913 on theBenchmark for (2913ds/3512Mi)
% 41.43/11.83 % TRYING [6]
% 41.43/11.83 % TRYING [7]
% 41.43/11.83 % (208038) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-208032-208038"...
% 41.43/11.83 % (208038)...printing done.
% 41.43/11.83 % (208038)Refutation found. Thanks to Tanya!
% 41.43/11.83 % SZS status Unsatisfiable for theBenchmark
% 41.43/11.83 % SZS output start Proof for theBenchmark
% See solution above
% 41.43/11.84 % (208038)------------------------------
% 41.43/11.84 % (208038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.43/11.84 % (208038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/11.84 % (208038)CaDiCaL version: 2.1.3
% 41.43/11.84 % (208038)Termination reason: Refutation
% 41.43/11.84 % (208038)Time elapsed: 11.239 s
% 41.43/11.84 % (208038)Peak memory usage: 111 MB
% 41.43/11.84 % (208038)Instructions burned: 12594 (million)
% 41.43/11.84 % (208032)Success in time 11.38 s
% 41.43/11.84 % Vampire exiting
%------------------------------------------------------------------------------