%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC187-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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:01 PM UTC 2026
% Result : Unsatisfiable 5.38s 1.27s
% Output : Refutation 5.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 80
% Syntax : Number of formulae : 413 ( 66 unt; 33 def)
% Number of atoms : 1314 ( 164 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 1501 ( 600 ~; 868 |; 0 &)
% ( 33 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 42 ( 40 usr; 34 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 9 con; 0-2 aty)
% Number of variables : 249 ( 0 sgn 249 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f11,axiom,
~ singletonP(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause11) ).
fof(f12,axiom,
! [X0] : ssItem(skaf83(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause12) ).
fof(f13,axiom,
! [X0] : ssList(skaf82(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause13) ).
fof(f52,axiom,
! [X0,X1] : ssList(skaf43(X0,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause52) ).
fof(f53,axiom,
! [X0,X1] : ssList(skaf42(X0,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause53) ).
fof(f56,axiom,
! [X0] :
( ~ ssList(X0)
| segmentP(X0,nil) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause56) ).
fof(f60,axiom,
! [X0] :
( ~ ssList(X0)
| frontsegP(X0,nil) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause60) ).
fof(f71,axiom,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause71) ).
fof(f72,axiom,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f74,axiom,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause74) ).
fof(f75,axiom,
! [X0] :
( ~ ssList(X0)
| ssList(tl(X0))
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause75) ).
fof(f76,axiom,
! [X0] :
( ~ ssList(X0)
| ssItem(hd(X0))
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause76) ).
fof(f85,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ssList(app(X1,X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ssList(cons(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause86) ).
fof(f96,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| tl(cons(X0,X1)) = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause96) ).
fof(f100,axiom,
! [X0,X1] :
( cons(X0,X1) != X1
| ~ ssItem(X0)
| ~ ssList(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause99) ).
fof(f107,axiom,
! [X0] :
( ~ ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause104) ).
fof(f112,axiom,
! [X0] :
( ~ ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause109) ).
fof(f119,axiom,
! [X0,X1] :
( cons(X0,nil) != X1
| ~ ssItem(X0)
| ~ ssList(X1)
| singletonP(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause116) ).
fof(f125,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| app(cons(X0,nil),X1) = cons(X0,X1) ),
file('/export/starexec/sandbox/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(f134,axiom,
! [X0,X1] :
( ~ segmentP(X0,X1)
| ~ segmentP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X1 = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause127) ).
fof(f135,plain,
! [X0,X1] :
( ~ segmentP(X0,X1)
| ~ segmentP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X0 = X1 ),
inference(reorient_equations,[],[f134]) ).
fof(f138,axiom,
! [X0,X1] :
( ~ frontsegP(X0,X1)
| ~ frontsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X1 = X0 ),
file('/export/starexec/sandbox/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(f144,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| nil = X1
| tl(app(X1,X0)) = app(tl(X1),X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause133) ).
fof(f148,axiom,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| frontsegP(app(X0,X2),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause137) ).
fof(f151,axiom,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| memberP(app(X0,X2),X1) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/SWC001-0.ax',clause144) ).
fof(f173,axiom,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X2 = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause161) ).
fof(f174,plain,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X0 = X2 ),
inference(reorient_equations,[],[f173]) ).
fof(f182,axiom,
! [X0,X1] :
( ~ memberP(X0,X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| app(skaf42(X0,X1),cons(X1,skaf43(X1,X0))) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause169) ).
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/sandbox/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(f187,axiom,
! [X2,X3,X0,X1] :
( app(app(X0,X1),X2) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| segmentP(X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause173) ).
fof(f189,axiom,
! [X2,X3,X0,X1] :
( app(X0,cons(X1,X2)) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(X3)
| memberP(X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause175) ).
fof(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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(f200,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_1) ).
fof(f201,negated_conjecture,
ssList(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_2) ).
fof(f204,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_5) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
ssList(sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
app(app(sk6,cons(sk5,nil)),sk7) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_10) ).
fof(f210,plain,
sk1 = app(app(sk6,cons(sk5,nil)),sk7),
inference(reorient_equations,[],[f209]) ).
fof(f211,negated_conjecture,
( memberP(sk6,sk5)
| memberP(sk7,sk5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).
fof(f213,negated_conjecture,
( ssItem(sk8)
| nil = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_13) ).
fof(f217,negated_conjecture,
( cons(sk8,nil) = sk3
| nil = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_16) ).
fof(f218,plain,
( sk3 = cons(sk8,nil)
| nil = sk3 ),
inference(reorient_equations,[],[f217]) ).
fof(f219,negated_conjecture,
( memberP(sk4,sk8)
| nil = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_17) ).
fof(f220,plain,
ssList(sk3),
inference(definition_unfolding,[],[f200,f205]) ).
fof(f221,plain,
ssList(sk4),
inference(definition_unfolding,[],[f201,f204]) ).
fof(f222,plain,
sk3 = app(app(sk6,cons(sk5,nil)),sk7),
inference(definition_unfolding,[],[f210,f205]) ).
fof(f230,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(cons(X0,nil))
| singletonP(cons(X0,nil)) ),
inference(equality_resolution,[],[f119]) ).
fof(f234,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1))
| frontsegP(app(X0,X1),X0) ),
inference(equality_resolution,[],[f155]) ).
fof(f237,plain,
! [X2,X0,X1] :
( ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(app(X0,X1),X2))
| segmentP(app(app(X0,X1),X2),X1) ),
inference(equality_resolution,[],[f187]) ).
fof(f238,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(f239,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(f240,plain,
! [X2,X3,X0,X1] :
( ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(equality_resolution,[],[f193]) ).
fof(f250,plain,
~ ssList(nil),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f251,plain,
singletonP(nil),
inference(consistent_polarity_flipping,[],[f11]) ).
fof(f252,plain,
! [X0] : ~ ssList(skaf82(X0)),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f277,plain,
! [X0,X1] : ~ ssList(skaf43(X0,X1)),
inference(consistent_polarity_flipping,[],[f52]) ).
fof(f278,plain,
! [X0,X1] : ~ ssList(skaf42(X0,X1)),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f279,plain,
! [X0] :
( segmentP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f56]) ).
fof(f283,plain,
! [X0] :
( frontsegP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f289,plain,
! [X0,X1] :
( ssList(X0)
| ~ duplicatefreeP(X0)
| ssItem(X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f291,plain,
! [X0] :
( ssList(X0)
| app(nil,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f292,plain,
! [X0] :
( ~ ssList(tl(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f293,plain,
! [X0] :
( ssItem(hd(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f302,plain,
! [X0,X1] :
( ~ ssList(app(X1,X0))
| ssList(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f303,plain,
! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1)
| ~ ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f313,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ssList(X1)
| tl(cons(X0,X1)) = X1 ),
inference(consistent_polarity_flipping,[],[f96]) ).
fof(f316,plain,
! [X0,X1] :
( cons(X0,X1) != X1
| ~ ssItem(X0)
| ssList(X1) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f320,plain,
! [X0] :
( ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f323,plain,
! [X0] :
( ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f330,plain,
! [X0] :
( ~ singletonP(cons(X0,nil))
| ssList(cons(X0,nil))
| ~ ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f230]) ).
fof(f333,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f339,plain,
! [X0,X1] :
( ~ segmentP(X1,X0)
| ~ segmentP(X0,X1)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f341,plain,
! [X0,X1] :
( ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f344,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| nil = X1
| tl(app(X1,X0)) = app(tl(X1),X0) ),
inference(consistent_polarity_flipping,[],[f144]) ).
fof(f348,plain,
! [X2,X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X2)
| ssList(X1)
| ssList(X0)
| frontsegP(app(X0,X2),X1) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f351,plain,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ssList(X2)
| ssList(X0)
| ~ ssItem(X1)
| memberP(app(X0,X2),X1) ),
inference(consistent_polarity_flipping,[],[f151]) ).
fof(f355,plain,
! [X0,X1] :
( ssList(X1)
| ssList(X0)
| ssList(app(X0,X1))
| frontsegP(app(X0,X1),X0) ),
inference(consistent_polarity_flipping,[],[f234]) ).
fof(f370,plain,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f378,plain,
! [X0,X1] :
( ~ memberP(X0,X1)
| ~ ssItem(X1)
| ssList(X0)
| app(skaf42(X0,X1),cons(X1,skaf43(X1,X0))) = X0 ),
inference(consistent_polarity_flipping,[],[f182]) ).
fof(f380,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(f382,plain,
! [X2,X0,X1] :
( segmentP(app(app(X0,X1),X2),X1)
| ssList(X0)
| ssList(X1)
| ssList(app(app(X0,X1),X2))
| ssList(X2) ),
inference(consistent_polarity_flipping,[],[f237]) ).
fof(f384,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,[],[f238]) ).
fof(f385,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(f387,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,[],[f239]) ).
fof(f388,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,[],[f240]) ).
fof(f395,plain,
~ ssList(sk3),
inference(consistent_polarity_flipping,[],[f220]) ).
fof(f396,plain,
~ ssList(sk4),
inference(consistent_polarity_flipping,[],[f221]) ).
fof(f399,plain,
~ ssList(sk6),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f400,plain,
~ ssList(sk7),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f401,plain,
! [X3,X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| ~ ssItem(X3)
| frontsegP(cons(X3,X0),cons(X3,X1)) ),
inference(duplicate_literal_removal,[],[f387]) ).
fof(f408,definition,
( spl0_1
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f409,plain,
( nil != sk3
| spl0_1 ),
inference(avatar_component_clause,[],[f408]) ).
fof(f410,plain,
( nil = sk3
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f408]) ).
fof(f412,definition,
( spl0_2
<=> memberP(sk4,sk8) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f414,plain,
( memberP(sk4,sk8)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f412]) ).
fof(f415,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f219,f412,f408]) ).
fof(f417,definition,
( spl0_3
<=> sk3 = cons(sk8,nil) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f419,plain,
( sk3 = cons(sk8,nil)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f420,plain,
( spl0_1
| spl0_3 ),
inference(avatar_split_clause,[],[f218,f417,f408]) ).
fof(f428,definition,
( spl0_5
<=> ssItem(sk8) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f430,plain,
( ssItem(sk8)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f428]) ).
fof(f431,plain,
( spl0_1
| spl0_5 ),
inference(avatar_split_clause,[],[f213,f428,f408]) ).
fof(f434,definition,
( spl0_6
<=> memberP(sk7,sk5) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f436,plain,
( memberP(sk7,sk5)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f438,definition,
( spl0_7
<=> memberP(sk6,sk5) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f440,plain,
( memberP(sk6,sk5)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f441,plain,
( spl0_6
| spl0_7 ),
inference(avatar_split_clause,[],[f211,f438,f434]) ).
fof(f447,definition,
( spl0_9
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f448,plain,
( ~ ssList(nil)
| spl0_9 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f475,definition,
( spl0_15
<=> ! [X1] : ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f476,plain,
( ! [X1] : ssItem(X1)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f475]) ).
fof(f478,definition,
( spl0_16
<=> ! [X0] :
( ssList(X0)
| ~ duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f479,plain,
( ! [X0] :
( ~ duplicatefreeP(X0)
| ssList(X0) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f480,plain,
( spl0_15
| spl0_16 ),
inference(avatar_split_clause,[],[f289,f478,f475]) ).
fof(f483,plain,
~ spl0_9,
inference(avatar_split_clause,[],[f250,f447]) ).
fof(f486,plain,
( ! [X0] : ~ memberP(nil,X0)
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f71,f476]) ).
fof(f563,plain,
sk3 = app(nil,sk3),
inference(resolution,[],[f291,f395]) ).
fof(f566,plain,
sk7 = app(nil,sk7),
inference(resolution,[],[f291,f400]) ).
fof(f617,plain,
( ! [X0,X1] :
( ssList(X1)
| tl(cons(X0,X1)) = X1 )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f313,f476]) ).
fof(f619,plain,
( ! [X0,X1] : skaf82(X1) = tl(cons(X0,skaf82(X1)))
| ~ spl0_15 ),
inference(resolution,[],[f617,f252]) ).
fof(f649,plain,
( ! [X0] : sk3 = tl(cons(X0,sk3))
| ~ spl0_15 ),
inference(resolution,[],[f617,f395]) ).
fof(f747,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| nil = sk3 ),
inference(resolution,[],[f320,f395]) ).
fof(f752,definition,
( spl0_17
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f753,plain,
( nil != sk7
| spl0_17 ),
inference(avatar_component_clause,[],[f752]) ).
fof(f754,plain,
( nil = sk7
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f752]) ).
fof(f761,definition,
( spl0_19
<=> nil = sk6 ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f762,plain,
( nil != sk6
| spl0_19 ),
inference(avatar_component_clause,[],[f761]) ).
fof(f763,plain,
( nil = sk6
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f761]) ).
fof(f774,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f747,f409]) ).
fof(f786,plain,
( memberP(nil,sk5)
| ~ spl0_6
| ~ spl0_17 ),
inference(superposition,[],[f436,f754]) ).
fof(f790,plain,
( sk3 = app(app(nil,cons(sk5,nil)),sk7)
| ~ spl0_19 ),
inference(superposition,[],[f222,f763]) ).
fof(f794,plain,
( ~ ssItem(sk5)
| ~ spl0_6
| ~ spl0_17 ),
inference(resolution,[],[f71,f786]) ).
fof(f795,plain,
( $false
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f794,f206]) ).
fof(f796,plain,
( ~ spl0_6
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f795]) ).
fof(f900,plain,
( memberP(nil,sk5)
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_demodulation,[],[f440,f763]) ).
fof(f903,plain,
( ~ ssItem(sk5)
| ~ spl0_7
| ~ spl0_19 ),
inference(resolution,[],[f900,f71]) ).
fof(f904,plain,
( $false
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f903,f206]) ).
fof(f905,plain,
( ~ spl0_7
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f904]) ).
fof(f1015,plain,
( sk6 = cons(skaf83(sk6),skaf82(sk6))
| nil = sk6 ),
inference(resolution,[],[f323,f399]) ).
fof(f1017,plain,
( sk6 = cons(skaf83(sk6),skaf82(sk6))
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1015,f762]) ).
fof(f1076,plain,
( ! [X0] :
( ssList(X0)
| cons(sk8,X0) = app(cons(sk8,nil),X0) )
| ~ spl0_5 ),
inference(resolution,[],[f333,f430]) ).
fof(f1077,plain,
( ! [X0] :
( ssList(X0)
| cons(sk8,X0) = app(sk3,X0) )
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f1076,f419]) ).
fof(f1124,definition,
( spl0_28
<=> ssList(tl(sk6)) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f1125,plain,
( ~ ssList(tl(sk6))
| spl0_28 ),
inference(avatar_component_clause,[],[f1124]) ).
fof(f1126,plain,
( ssList(tl(sk6))
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f1124]) ).
fof(f1163,plain,
( ssList(sk6)
| nil = sk6
| ~ spl0_28 ),
inference(resolution,[],[f1126,f292]) ).
fof(f1164,plain,
( nil = sk6
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f1163,f399]) ).
fof(f1165,plain,
( $false
| spl0_19
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f1164,f762]) ).
fof(f1166,plain,
( spl0_19
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f1165]) ).
fof(f1194,definition,
( spl0_35
<=> ssList(app(sk6,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f1195,plain,
( ~ ssList(app(sk6,cons(sk5,nil)))
| spl0_35 ),
inference(avatar_component_clause,[],[f1194]) ).
fof(f1196,plain,
( ssList(app(sk6,cons(sk5,nil)))
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f1194]) ).
fof(f1202,plain,
! [X0,X1] :
( frontsegP(app(X0,X1),X0)
| ssList(X0)
| ssList(X1) ),
inference(forward_subsumption_resolution,[],[f355,f302]) ).
fof(f1209,plain,
( frontsegP(sk3,app(sk6,cons(sk5,nil)))
| ssList(app(sk6,cons(sk5,nil)))
| ssList(sk7) ),
inference(superposition,[],[f1202,f222]) ).
fof(f1216,plain,
( frontsegP(sk3,app(sk6,cons(sk5,nil)))
| ssList(app(sk6,cons(sk5,nil))) ),
inference(forward_subsumption_resolution,[],[f1209,f400]) ).
fof(f1219,definition,
( spl0_37
<=> frontsegP(sk3,app(sk6,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f1221,plain,
( frontsegP(sk3,app(sk6,cons(sk5,nil)))
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f1219]) ).
fof(f1222,plain,
( spl0_35
| spl0_37 ),
inference(avatar_split_clause,[],[f1216,f1219,f1194]) ).
fof(f1364,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,[],[f348,f1202]) ).
fof(f1365,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,[],[f1364]) ).
fof(f1369,plain,
! [X2,X0,X1] :
( frontsegP(app(app(X1,X2),X0),X1)
| ssList(X1)
| ssList(X0)
| ssList(X2) ),
inference(forward_subsumption_resolution,[],[f1365,f302]) ).
fof(f1632,plain,
! [X0] :
( ssList(X0)
| nil = sk3
| tl(app(sk3,X0)) = app(tl(sk3),X0) ),
inference(resolution,[],[f344,f395]) ).
fof(f1639,plain,
( ! [X0] :
( ssList(X0)
| tl(app(sk3,X0)) = app(tl(sk3),X0) )
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f1632,f409]) ).
fof(f2071,plain,
( ~ ssItem(sk8)
| ssList(sk4)
| sk4 = app(skaf42(sk4,sk8),cons(sk8,skaf43(sk8,sk4)))
| ~ spl0_2 ),
inference(resolution,[],[f378,f414]) ).
fof(f2078,plain,
( ssList(sk4)
| sk4 = app(skaf42(sk4,sk8),cons(sk8,skaf43(sk8,sk4)))
| ~ spl0_2
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f2071,f430]) ).
fof(f2085,plain,
( sk4 = app(skaf42(sk4,sk8),cons(sk8,skaf43(sk8,sk4)))
| ~ spl0_2
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f2078,f396]) ).
fof(f2118,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk3
| ~ ssItem(sk8)
| ~ ssItem(X0)
| ssList(nil)
| ssList(X1)
| nil = X1 )
| ~ spl0_3 ),
inference(superposition,[],[f380,f419]) ).
fof(f2127,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk3
| ~ ssItem(X0)
| ssList(nil)
| ssList(X1)
| nil = X1 )
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f2118,f430]) ).
fof(f2135,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk3
| ~ ssItem(X0)
| ssList(X1)
| nil = X1 )
| ~ spl0_3
| ~ spl0_5
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f2127,f448]) ).
fof(f2210,plain,
( ! [X0,X1] :
( ~ frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| ssList(nil)
| ~ ssItem(X0)
| ~ ssItem(sk8)
| sk8 = X0 )
| ~ spl0_3 ),
inference(superposition,[],[f385,f419]) ).
fof(f2230,plain,
( ! [X0,X1] :
( ~ frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(sk8)
| sk8 = X0 )
| ~ spl0_3
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f2210,f448]) ).
fof(f2240,plain,
( ! [X0,X1] :
( ~ frontsegP(sk3,cons(X0,X1))
| ssList(X1)
| ~ ssItem(X0)
| sk8 = X0 )
| ~ spl0_3
| ~ spl0_5
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f2230,f430]) ).
fof(f2359,definition,
( spl0_78
<=> sk3 = cons(hd(sk3),tl(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f2361,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f2359]) ).
fof(f2378,definition,
( spl0_81
<=> ! [X0] :
( ssList(X0)
| tl(app(sk3,X0)) = app(tl(sk3),X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f2379,plain,
( ! [X0] :
( ssList(X0)
| tl(app(sk3,X0)) = app(tl(sk3),X0) )
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f2378]) ).
fof(f2426,plain,
( segmentP(sk3,cons(sk5,nil))
| ssList(sk6)
| ssList(cons(sk5,nil))
| ssList(sk3)
| ssList(sk7) ),
inference(superposition,[],[f382,f222]) ).
fof(f2432,plain,
( segmentP(sk3,cons(sk5,nil))
| ssList(cons(sk5,nil))
| ssList(sk3)
| ssList(sk7) ),
inference(forward_subsumption_resolution,[],[f2426,f399]) ).
fof(f2438,plain,
( segmentP(sk3,cons(sk5,nil))
| ssList(cons(sk5,nil))
| ssList(sk7) ),
inference(forward_subsumption_resolution,[],[f2432,f395]) ).
fof(f2444,plain,
( segmentP(sk3,cons(sk5,nil))
| ssList(cons(sk5,nil)) ),
inference(forward_subsumption_resolution,[],[f2438,f400]) ).
fof(f2448,plain,
( segmentP(nil,cons(sk5,nil))
| ssList(cons(sk5,nil))
| ~ spl0_1 ),
inference(forward_demodulation,[],[f2444,f410]) ).
fof(f2453,definition,
( spl0_84
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f2454,plain,
( ~ ssList(cons(sk5,nil))
| spl0_84 ),
inference(avatar_component_clause,[],[f2453]) ).
fof(f2455,plain,
( ssList(cons(sk5,nil))
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f2453]) ).
fof(f2457,definition,
( spl0_85
<=> segmentP(nil,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f2459,plain,
( segmentP(nil,cons(sk5,nil))
| ~ spl0_85 ),
inference(avatar_component_clause,[],[f2457]) ).
fof(f2460,plain,
( spl0_84
| spl0_85
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f2448,f408,f2457,f2453]) ).
fof(f2486,plain,
( ssList(nil)
| ~ ssItem(sk5)
| ~ spl0_84 ),
inference(resolution,[],[f2455,f303]) ).
fof(f2487,plain,
( ~ ssItem(sk5)
| spl0_9
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f2486,f448]) ).
fof(f2488,plain,
( $false
| spl0_9
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f2487,f206]) ).
fof(f2489,plain,
( spl0_9
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f2488]) ).
fof(f2502,definition,
( spl0_86
<=> nil = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f2504,plain,
( nil = cons(sk5,nil)
| ~ spl0_86 ),
inference(avatar_component_clause,[],[f2502]) ).
fof(f2534,plain,
( ! [X2,X3,X0,X1] :
( ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(X2)
| ssList(X0)
| ~ ssItem(X1)
| ssList(X3) )
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f388,f479]) ).
fof(f2539,plain,
( ~ segmentP(cons(sk5,nil),nil)
| ssList(cons(sk5,nil))
| ssList(nil)
| nil = cons(sk5,nil)
| ~ spl0_85 ),
inference(resolution,[],[f2459,f339]) ).
fof(f2540,plain,
( ssList(cons(sk5,nil))
| ssList(nil)
| nil = cons(sk5,nil)
| ~ spl0_85 ),
inference(forward_subsumption_resolution,[],[f2539,f279]) ).
fof(f2545,plain,
( ssList(nil)
| nil = cons(sk5,nil)
| spl0_84
| ~ spl0_85 ),
inference(forward_subsumption_resolution,[],[f2540,f2454]) ).
fof(f2550,plain,
( nil = cons(sk5,nil)
| spl0_9
| spl0_84
| ~ spl0_85 ),
inference(forward_subsumption_resolution,[],[f2545,f448]) ).
fof(f2552,plain,
( spl0_86
| spl0_9
| spl0_84
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f2550,f2457,f2453,f447,f2502]) ).
fof(f2601,plain,
( ~ singletonP(nil)
| ssList(nil)
| ~ ssItem(sk5)
| ~ spl0_86 ),
inference(superposition,[],[f330,f2504]) ).
fof(f2634,plain,
( ssList(nil)
| ~ ssItem(sk5)
| ~ spl0_86 ),
inference(forward_subsumption_resolution,[],[f2601,f251]) ).
fof(f2648,plain,
( ~ ssItem(sk5)
| spl0_9
| ~ spl0_86 ),
inference(forward_subsumption_resolution,[],[f2634,f448]) ).
fof(f2652,plain,
( $false
| spl0_9
| ~ spl0_86 ),
inference(forward_subsumption_resolution,[],[f2648,f206]) ).
fof(f2653,plain,
( spl0_9
| ~ spl0_86 ),
inference(avatar_contradiction_clause,[],[f2652]) ).
fof(f2655,plain,
( spl0_78
| spl0_1 ),
inference(avatar_split_clause,[],[f774,f408,f2359]) ).
fof(f2658,plain,
( spl0_81
| spl0_1 ),
inference(avatar_split_clause,[],[f1639,f408,f2378]) ).
fof(f2777,plain,
( ! [X0,X1] :
( ssList(app(app(X0,cons(sk8,X1)),sk3))
| ssList(X1)
| ssList(X0)
| ~ ssItem(sk8)
| ssList(nil) )
| ~ spl0_3
| ~ spl0_16 ),
inference(superposition,[],[f2534,f419]) ).
fof(f2778,plain,
( ! [X0,X1] :
( ssList(app(app(X0,cons(sk8,X1)),sk3))
| ssList(X1)
| ssList(X0)
| ssList(nil) )
| ~ spl0_3
| ~ spl0_5
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2777,f430]) ).
fof(f2797,plain,
( ! [X0,X1] :
( ssList(app(app(X0,cons(sk8,X1)),sk3))
| ssList(X1)
| ssList(X0) )
| ~ spl0_3
| ~ spl0_5
| spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2778,f448]) ).
fof(f3312,plain,
( sk3 != tl(sk3)
| ~ ssItem(hd(sk3))
| ssList(tl(sk3))
| ~ spl0_78 ),
inference(superposition,[],[f316,f2361]) ).
fof(f3335,definition,
( spl0_111
<=> ssList(tl(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f3337,plain,
( ssList(tl(sk3))
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f3335]) ).
fof(f3339,definition,
( spl0_112
<=> ssItem(hd(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f3340,plain,
( ssItem(hd(sk3))
| ~ spl0_112 ),
inference(avatar_component_clause,[],[f3339]) ).
fof(f3341,plain,
( ~ ssItem(hd(sk3))
| spl0_112 ),
inference(avatar_component_clause,[],[f3339]) ).
fof(f3416,definition,
( spl0_130
<=> sk3 = tl(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f3418,plain,
( sk3 != tl(sk3)
| spl0_130 ),
inference(avatar_component_clause,[],[f3416]) ).
fof(f3419,plain,
( spl0_111
| ~ spl0_112
| ~ spl0_130
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f3312,f2359,f3416,f3339,f3335]) ).
fof(f3421,definition,
( spl0_131
<=> nil = tl(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f3423,plain,
( nil = tl(sk3)
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f3421]) ).
fof(f3520,plain,
( ssList(sk3)
| nil = sk3
| spl0_112 ),
inference(resolution,[],[f3341,f293]) ).
fof(f3521,plain,
( nil = sk3
| spl0_112 ),
inference(forward_subsumption_resolution,[],[f3520,f395]) ).
fof(f3522,plain,
( $false
| spl0_1
| spl0_112 ),
inference(forward_subsumption_resolution,[],[f3521,f409]) ).
fof(f3523,plain,
( spl0_1
| spl0_112 ),
inference(avatar_contradiction_clause,[],[f3522]) ).
fof(f3524,plain,
( ssList(sk3)
| nil = sk3
| ~ spl0_111 ),
inference(resolution,[],[f3337,f292]) ).
fof(f3525,plain,
( nil = sk3
| ~ spl0_111 ),
inference(forward_subsumption_resolution,[],[f3524,f395]) ).
fof(f3526,plain,
( $false
| spl0_1
| ~ spl0_111 ),
inference(forward_subsumption_resolution,[],[f3525,f409]) ).
fof(f3527,plain,
( spl0_1
| ~ spl0_111 ),
inference(avatar_contradiction_clause,[],[f3526]) ).
fof(f3567,plain,
( ! [X2,X0,X1] :
( memberP(app(X0,X2),X1)
| ssList(X2)
| ssList(X0)
| ~ memberP(X0,X1) )
| ~ spl0_15 ),
inference(backward_subsumption_resolution,[],[f351,f476]) ).
fof(f3576,plain,
( ! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ssList(X1)
| ~ ssItem(X2)
| memberP(X1,X2)
| X0 = X2 )
| ~ spl0_15 ),
inference(backward_subsumption_resolution,[],[f370,f476]) ).
fof(f3581,plain,
( ! [X2,X0,X1] :
( memberP(app(X0,cons(X1,X2)),X1)
| ssList(X0)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2) )
| ~ spl0_15 ),
inference(backward_subsumption_resolution,[],[f384,f476]) ).
fof(f3589,plain,
( ! [X3,X0,X1] :
( ~ frontsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| frontsegP(cons(X3,X0),cons(X3,X1)) )
| ~ spl0_15 ),
inference(backward_subsumption_resolution,[],[f401,f476]) ).
fof(f3611,plain,
( ! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ssList(X1)
| memberP(X1,X2)
| X0 = X2 )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f3576,f476]) ).
fof(f4022,plain,
( ! [X0] :
( memberP(sk3,X0)
| ssList(sk7)
| ssList(app(sk6,cons(sk5,nil)))
| ~ memberP(app(sk6,cons(sk5,nil)),X0) )
| ~ spl0_15 ),
inference(superposition,[],[f3567,f222]) ).
fof(f4028,plain,
( ! [X0] :
( memberP(sk3,X0)
| ssList(app(sk6,cons(sk5,nil)))
| ~ memberP(app(sk6,cons(sk5,nil)),X0) )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f4022,f400]) ).
fof(f4030,definition,
( spl0_141
<=> ! [X0] :
( memberP(sk3,X0)
| ~ memberP(app(sk6,cons(sk5,nil)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f4031,plain,
( ! [X0] :
( ~ memberP(app(sk6,cons(sk5,nil)),X0)
| memberP(sk3,X0) )
| ~ spl0_141 ),
inference(avatar_component_clause,[],[f4030]) ).
fof(f4095,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ssList(nil)
| memberP(nil,X0)
| sk8 = X0 )
| ~ spl0_3
| ~ spl0_15 ),
inference(superposition,[],[f3611,f419]) ).
fof(f4098,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| memberP(nil,X0)
| sk8 = X0 )
| ~ spl0_3
| spl0_9
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f4095,f448]) ).
fof(f4108,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| sk8 = X0 )
| ~ spl0_3
| spl0_9
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f4098,f486]) ).
fof(f4125,plain,
( ssList(sk6)
| ssList(cons(sk5,nil))
| ~ spl0_35 ),
inference(resolution,[],[f1196,f302]) ).
fof(f4126,plain,
( ssList(cons(sk5,nil))
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f4125,f399]) ).
fof(f4127,plain,
( $false
| ~ spl0_35
| spl0_84 ),
inference(forward_subsumption_resolution,[],[f4126,f2454]) ).
fof(f4128,plain,
( ~ spl0_35
| spl0_84 ),
inference(avatar_contradiction_clause,[],[f4127]) ).
fof(f4130,plain,
( ! [X0,X1] :
( ssList(nil)
| ssList(X0)
| frontsegP(cons(X1,X0),cons(X1,nil))
| ssList(X0) )
| ~ spl0_15 ),
inference(resolution,[],[f3589,f283]) ).
fof(f4136,plain,
( ! [X0,X1] :
( ssList(nil)
| ssList(X0)
| frontsegP(cons(X1,X0),cons(X1,nil)) )
| ~ spl0_15 ),
inference(duplicate_literal_removal,[],[f4130]) ).
fof(f4140,plain,
( ! [X0,X1] :
( frontsegP(cons(X1,X0),cons(X1,nil))
| ssList(X0) )
| spl0_9
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f4136,f448]) ).
fof(f5279,definition,
( spl0_159
<=> ssList(app(sk3,sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f5280,plain,
( ~ ssList(app(sk3,sk3))
| spl0_159 ),
inference(avatar_component_clause,[],[f5279]) ).
fof(f5281,plain,
( ssList(app(sk3,sk3))
| ~ spl0_159 ),
inference(avatar_component_clause,[],[f5279]) ).
fof(f5437,plain,
( memberP(sk3,sk5)
| ssList(sk6)
| ssList(app(sk6,cons(sk5,nil)))
| ssList(nil)
| ~ spl0_15
| ~ spl0_141 ),
inference(resolution,[],[f4031,f3581]) ).
fof(f5444,plain,
( memberP(sk3,sk5)
| ssList(app(sk6,cons(sk5,nil)))
| ssList(nil)
| ~ spl0_15
| ~ spl0_141 ),
inference(forward_subsumption_resolution,[],[f5437,f399]) ).
fof(f5447,plain,
( memberP(sk3,sk5)
| ssList(nil)
| ~ spl0_15
| spl0_35
| ~ spl0_141 ),
inference(forward_subsumption_resolution,[],[f5444,f1195]) ).
fof(f5448,plain,
( memberP(sk3,sk5)
| spl0_9
| ~ spl0_15
| spl0_35
| ~ spl0_141 ),
inference(forward_subsumption_resolution,[],[f5447,f448]) ).
fof(f5483,definition,
( spl0_167
<=> sk3 = sk6 ),
introduced(definition,[new_symbols(definition,[spl0_167])],[avatar_definition]) ).
fof(f5484,plain,
( sk3 = sk6
| ~ spl0_167 ),
inference(avatar_component_clause,[],[f5483]) ).
fof(f5494,definition,
( spl0_169
<=> sk8 = skaf83(sk6) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f5496,plain,
( sk8 = skaf83(sk6)
| ~ spl0_169 ),
inference(avatar_component_clause,[],[f5494]) ).
fof(f5578,definition,
( spl0_175
<=> frontsegP(sk6,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_175])],[avatar_definition]) ).
fof(f5579,plain,
( frontsegP(sk6,sk3)
| ~ spl0_175 ),
inference(avatar_component_clause,[],[f5578]) ).
fof(f5609,definition,
( spl0_176
<=> frontsegP(sk3,sk6) ),
introduced(definition,[new_symbols(definition,[spl0_176])],[avatar_definition]) ).
fof(f8283,plain,
( ! [X0] :
( ssList(X0)
| app(nil,X0) = tl(app(sk3,X0)) )
| ~ spl0_81
| ~ spl0_131 ),
inference(forward_demodulation,[],[f2379,f3423]) ).
fof(f8323,plain,
( app(nil,sk7) = tl(app(sk3,sk7))
| ~ spl0_81
| ~ spl0_131 ),
inference(resolution,[],[f8283,f400]) ).
fof(f8712,definition,
( spl0_254
<=> sk5 = sk8 ),
introduced(definition,[new_symbols(definition,[spl0_254])],[avatar_definition]) ).
fof(f8714,plain,
( sk5 = sk8
| ~ spl0_254 ),
inference(avatar_component_clause,[],[f8712]) ).
fof(f8781,plain,
( sk3 != sk3
| ~ ssItem(hd(sk3))
| ssList(tl(sk3))
| nil = tl(sk3)
| ~ spl0_3
| ~ spl0_5
| spl0_9
| ~ spl0_78 ),
inference(superposition,[],[f2135,f2361]) ).
fof(f8782,plain,
( ~ ssItem(hd(sk3))
| ssList(tl(sk3))
| nil = tl(sk3)
| ~ spl0_3
| ~ spl0_5
| spl0_9
| ~ spl0_78 ),
inference(trivial_inequality_removal,[],[f8781]) ).
fof(f8841,plain,
( ~ frontsegP(sk3,sk6)
| ssList(skaf82(sk6))
| ~ ssItem(skaf83(sk6))
| sk8 = skaf83(sk6)
| ~ spl0_3
| ~ spl0_5
| spl0_9
| spl0_19 ),
inference(superposition,[],[f2240,f1017]) ).
fof(f8878,plain,
( ssList(app(sk4,sk3))
| ssList(skaf43(sk8,sk4))
| ssList(skaf42(sk4,sk8))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| spl0_9
| ~ spl0_16 ),
inference(superposition,[],[f2797,f2085]) ).
fof(f8879,plain,
( ssList(app(sk4,sk3))
| ssList(skaf42(sk4,sk8))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f8878,f277]) ).
fof(f8882,plain,
( ssList(app(sk4,sk3))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f8879,f278]) ).
fof(f8895,plain,
( ssList(sk4)
| ssList(sk3)
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| spl0_9
| ~ spl0_16 ),
inference(resolution,[],[f8882,f302]) ).
fof(f8896,plain,
( ssList(sk3)
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f8895,f396]) ).
fof(f8897,plain,
( $false
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f8896,f395]) ).
fof(f8898,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| spl0_9
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f8897]) ).
fof(f8990,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ memberP(app(sk6,cons(sk5,nil)),X0) )
| ~ spl0_15
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f4028,f1195]) ).
fof(f9246,plain,
( spl0_141
| ~ spl0_15
| spl0_35 ),
inference(avatar_split_clause,[],[f8990,f1194,f475,f4030]) ).
fof(f9703,plain,
( ssList(sk3)
| ssList(sk3)
| ~ spl0_159 ),
inference(resolution,[],[f5281,f302]) ).
fof(f9704,plain,
( ssList(sk3)
| ~ spl0_159 ),
inference(duplicate_literal_removal,[],[f9703]) ).
fof(f9705,plain,
( $false
| ~ spl0_159 ),
inference(forward_subsumption_resolution,[],[f9704,f395]) ).
fof(f9706,plain,
~ spl0_159,
inference(avatar_contradiction_clause,[],[f9705]) ).
fof(f12669,plain,
( frontsegP(sk3,app(sk3,cons(sk5,nil)))
| ~ spl0_37
| ~ spl0_167 ),
inference(superposition,[],[f1221,f5484]) ).
fof(f12748,plain,
( frontsegP(sk3,app(sk3,cons(sk8,nil)))
| ~ spl0_37
| ~ spl0_167
| ~ spl0_254 ),
inference(forward_demodulation,[],[f12669,f8714]) ).
fof(f12765,plain,
( ~ frontsegP(sk3,sk6)
| ~ ssItem(skaf83(sk6))
| sk8 = skaf83(sk6)
| ~ spl0_3
| ~ spl0_5
| spl0_9
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f8841,f252]) ).
fof(f12791,plain,
( ~ frontsegP(sk3,sk6)
| sk8 = skaf83(sk6)
| ~ spl0_3
| ~ spl0_5
| spl0_9
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f12765,f12]) ).
fof(f13005,definition,
( spl0_352
<=> sk3 = app(sk3,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_352])],[avatar_definition]) ).
fof(f13006,plain,
( sk3 != app(sk3,sk3)
| spl0_352 ),
inference(avatar_component_clause,[],[f13005]) ).
fof(f13007,plain,
( sk3 = app(sk3,sk3)
| ~ spl0_352 ),
inference(avatar_component_clause,[],[f13005]) ).
fof(f13009,definition,
( spl0_353
<=> frontsegP(app(sk3,sk3),sk3) ),
introduced(definition,[new_symbols(definition,[spl0_353])],[avatar_definition]) ).
fof(f13010,plain,
( frontsegP(app(sk3,sk3),sk3)
| ~ spl0_353 ),
inference(avatar_component_clause,[],[f13009]) ).
fof(f13011,plain,
( ~ frontsegP(app(sk3,sk3),sk3)
| spl0_353 ),
inference(avatar_component_clause,[],[f13009]) ).
fof(f13265,plain,
( ssList(sk3)
| ssList(sk3)
| spl0_353 ),
inference(resolution,[],[f13011,f1202]) ).
fof(f13266,plain,
( ssList(sk3)
| spl0_353 ),
inference(duplicate_literal_removal,[],[f13265]) ).
fof(f13267,plain,
( $false
| spl0_353 ),
inference(forward_subsumption_resolution,[],[f13266,f395]) ).
fof(f13268,plain,
spl0_353,
inference(avatar_contradiction_clause,[],[f13267]) ).
fof(f14895,plain,
( cons(sk8,sk3) = app(sk3,sk3)
| ~ spl0_3
| ~ spl0_5 ),
inference(resolution,[],[f395,f1077]) ).
fof(f14963,plain,
( sk3 = cons(sk8,sk3)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_352 ),
inference(forward_demodulation,[],[f14895,f13007]) ).
fof(f16302,plain,
( sk3 = tl(sk3)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_15
| ~ spl0_352 ),
inference(superposition,[],[f649,f14963]) ).
fof(f16347,plain,
( $false
| ~ spl0_3
| ~ spl0_5
| ~ spl0_15
| spl0_130
| ~ spl0_352 ),
inference(forward_subsumption_resolution,[],[f16302,f3418]) ).
fof(f16348,plain,
( ~ spl0_3
| ~ spl0_5
| ~ spl0_15
| spl0_130
| ~ spl0_352 ),
inference(avatar_contradiction_clause,[],[f16347]) ).
fof(f16483,definition,
( spl0_378
<=> ssList(sk6) ),
introduced(definition,[new_symbols(definition,[spl0_378])],[avatar_definition]) ).
fof(f16484,plain,
( ~ ssList(sk6)
| spl0_378 ),
inference(avatar_component_clause,[],[f16483]) ).
fof(f16634,plain,
( spl0_169
| ~ spl0_176
| ~ spl0_3
| ~ spl0_5
| spl0_9
| spl0_19 ),
inference(avatar_split_clause,[],[f12791,f761,f447,f428,f417,f5609,f5494]) ).
fof(f16659,plain,
~ spl0_378,
inference(avatar_split_clause,[],[f399,f16483]) ).
fof(f19300,plain,
( sk7 = tl(app(sk3,sk7))
| ~ spl0_81
| ~ spl0_131 ),
inference(forward_demodulation,[],[f8323,f566]) ).
fof(f22322,plain,
( ~ frontsegP(sk3,app(sk3,sk3))
| ssList(sk3)
| ssList(app(sk3,sk3))
| sk3 = app(sk3,sk3)
| ~ spl0_353 ),
inference(resolution,[],[f13010,f341]) ).
fof(f22323,plain,
( ~ frontsegP(sk3,app(sk3,sk3))
| ssList(app(sk3,sk3))
| sk3 = app(sk3,sk3)
| ~ spl0_353 ),
inference(forward_subsumption_resolution,[],[f22322,f395]) ).
fof(f22328,plain,
( ~ frontsegP(sk3,app(sk3,sk3))
| sk3 = app(sk3,sk3)
| spl0_159
| ~ spl0_353 ),
inference(forward_subsumption_resolution,[],[f22323,f5280]) ).
fof(f22333,plain,
( ~ frontsegP(sk3,app(sk3,sk3))
| spl0_159
| spl0_352
| ~ spl0_353 ),
inference(forward_subsumption_resolution,[],[f22328,f13006]) ).
fof(f22871,plain,
( tl(sk6) = skaf82(sk6)
| ~ spl0_15
| spl0_19 ),
inference(superposition,[],[f619,f1017]) ).
fof(f22876,plain,
( sk6 = cons(skaf83(sk6),tl(sk6))
| ~ spl0_15
| spl0_19 ),
inference(superposition,[],[f1017,f22871]) ).
fof(f22890,plain,
( sk6 = cons(sk8,tl(sk6))
| ~ spl0_15
| spl0_19
| ~ spl0_169 ),
inference(forward_demodulation,[],[f22876,f5496]) ).
fof(f24761,plain,
( ~ frontsegP(sk3,sk6)
| ssList(sk3)
| ssList(sk6)
| sk3 = sk6
| ~ spl0_175 ),
inference(resolution,[],[f5579,f341]) ).
fof(f25140,plain,
( frontsegP(sk6,cons(sk8,nil))
| ssList(tl(sk6))
| spl0_9
| ~ spl0_15
| spl0_19
| ~ spl0_169 ),
inference(superposition,[],[f4140,f22890]) ).
fof(f25153,plain,
( frontsegP(sk6,cons(sk8,nil))
| spl0_9
| ~ spl0_15
| spl0_19
| spl0_28
| ~ spl0_169 ),
inference(forward_subsumption_resolution,[],[f25140,f1125]) ).
fof(f25172,plain,
( frontsegP(sk6,sk3)
| ~ spl0_3
| spl0_9
| ~ spl0_15
| spl0_19
| spl0_28
| ~ spl0_169 ),
inference(forward_demodulation,[],[f25153,f419]) ).
fof(f32368,plain,
( frontsegP(sk3,sk6)
| ssList(sk6)
| ssList(sk7)
| ssList(cons(sk5,nil)) ),
inference(superposition,[],[f1369,f222]) ).
fof(f32430,plain,
( sk3 = app(app(nil,cons(sk8,nil)),sk7)
| ~ spl0_19
| ~ spl0_254 ),
inference(forward_demodulation,[],[f790,f8714]) ).
fof(f32437,plain,
( frontsegP(sk3,sk6)
| ssList(sk7)
| ssList(cons(sk5,nil))
| spl0_378 ),
inference(forward_subsumption_resolution,[],[f32368,f16484]) ).
fof(f32577,plain,
( sk3 = app(app(nil,sk3),sk7)
| ~ spl0_3
| ~ spl0_19
| ~ spl0_254 ),
inference(forward_demodulation,[],[f32430,f419]) ).
fof(f32583,plain,
( frontsegP(sk3,sk6)
| ssList(cons(sk5,nil))
| spl0_378 ),
inference(forward_subsumption_resolution,[],[f32437,f400]) ).
fof(f32727,plain,
( sk3 = app(sk3,sk7)
| ~ spl0_3
| ~ spl0_19
| ~ spl0_254 ),
inference(forward_demodulation,[],[f32577,f563]) ).
fof(f35787,plain,
( sk7 = tl(sk3)
| ~ spl0_3
| ~ spl0_19
| ~ spl0_81
| ~ spl0_131
| ~ spl0_254 ),
inference(superposition,[],[f19300,f32727]) ).
fof(f35824,plain,
( nil = sk7
| ~ spl0_3
| ~ spl0_19
| ~ spl0_81
| ~ spl0_131
| ~ spl0_254 ),
inference(forward_demodulation,[],[f35787,f3423]) ).
fof(f35832,plain,
( $false
| ~ spl0_3
| spl0_17
| ~ spl0_19
| ~ spl0_81
| ~ spl0_131
| ~ spl0_254 ),
inference(forward_subsumption_resolution,[],[f35824,f753]) ).
fof(f35833,plain,
( ~ spl0_3
| spl0_17
| ~ spl0_19
| ~ spl0_81
| ~ spl0_131
| ~ spl0_254 ),
inference(avatar_contradiction_clause,[],[f35832]) ).
fof(f35857,plain,
( ssList(tl(sk3))
| nil = tl(sk3)
| ~ spl0_3
| ~ spl0_5
| spl0_9
| ~ spl0_78
| ~ spl0_112 ),
inference(forward_subsumption_resolution,[],[f8782,f3340]) ).
fof(f35940,plain,
( spl0_131
| spl0_111
| ~ spl0_3
| ~ spl0_5
| spl0_9
| ~ spl0_78
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f35857,f3339,f2359,f447,f428,f417,f3335,f3421]) ).
fof(f37185,plain,
( sk5 = sk8
| ~ spl0_3
| spl0_9
| ~ spl0_15
| spl0_35
| ~ spl0_141 ),
inference(resolution,[],[f5448,f4108]) ).
fof(f37188,plain,
( spl0_254
| ~ spl0_3
| spl0_9
| ~ spl0_15
| spl0_35
| ~ spl0_141 ),
inference(avatar_split_clause,[],[f37185,f4030,f1194,f475,f447,f417,f8712]) ).
fof(f37459,plain,
( spl0_175
| ~ spl0_3
| spl0_9
| ~ spl0_15
| spl0_19
| spl0_28
| ~ spl0_169 ),
inference(avatar_split_clause,[],[f25172,f5494,f1124,f761,f475,f447,f417,f5578]) ).
fof(f38555,plain,
( frontsegP(sk3,app(sk3,sk3))
| ~ spl0_3
| ~ spl0_37
| ~ spl0_167
| ~ spl0_254 ),
inference(forward_demodulation,[],[f12748,f419]) ).
fof(f38629,plain,
( ~ frontsegP(sk3,sk6)
| ssList(sk6)
| sk3 = sk6
| ~ spl0_175 ),
inference(forward_subsumption_resolution,[],[f24761,f395]) ).
fof(f39267,plain,
( frontsegP(sk3,sk6)
| spl0_84
| spl0_378 ),
inference(forward_subsumption_resolution,[],[f32583,f2454]) ).
fof(f39954,plain,
( $false
| ~ spl0_3
| ~ spl0_37
| spl0_159
| ~ spl0_167
| ~ spl0_254
| spl0_352
| ~ spl0_353 ),
inference(forward_subsumption_resolution,[],[f38555,f22333]) ).
fof(f39955,plain,
( ~ spl0_3
| ~ spl0_37
| spl0_159
| ~ spl0_167
| ~ spl0_254
| spl0_352
| ~ spl0_353 ),
inference(avatar_contradiction_clause,[],[f39954]) ).
fof(f39989,plain,
( ~ frontsegP(sk3,sk6)
| sk3 = sk6
| ~ spl0_175
| spl0_378 ),
inference(forward_subsumption_resolution,[],[f38629,f16484]) ).
fof(f40084,plain,
( spl0_176
| spl0_84
| spl0_378 ),
inference(avatar_split_clause,[],[f39267,f16483,f2453,f5609]) ).
fof(f40359,plain,
( spl0_167
| ~ spl0_176
| ~ spl0_175
| spl0_378 ),
inference(avatar_split_clause,[],[f39989,f16483,f5578,f5609,f5483]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f415]) ).
cnf(s2,plain,
( spl0_1
| spl0_3 ),
inference(sat_conversion,[],[f420]) ).
cnf(s5,plain,
( spl0_1
| spl0_5 ),
inference(sat_conversion,[],[f431]) ).
cnf(s7,plain,
( spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f441]) ).
cnf(s14,plain,
( spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f480]) ).
cnf(s17,plain,
~ spl0_9,
inference(sat_conversion,[],[f483]) ).
cnf(s23,plain,
( ~ spl0_6
| ~ spl0_17 ),
inference(sat_conversion,[],[f796]) ).
cnf(s29,plain,
( ~ spl0_7
| ~ spl0_19 ),
inference(sat_conversion,[],[f905]) ).
cnf(s40,plain,
( spl0_19
| ~ spl0_28 ),
inference(sat_conversion,[],[f1166]) ).
cnf(s42,plain,
( spl0_35
| spl0_37 ),
inference(sat_conversion,[],[f1222]) ).
cnf(s98,plain,
( ~ spl0_1
| spl0_84
| spl0_85 ),
inference(sat_conversion,[],[f2460]) ).
cnf(s99,plain,
( spl0_9
| ~ spl0_84 ),
inference(sat_conversion,[],[f2489]) ).
cnf(s105,plain,
( spl0_9
| spl0_84
| ~ spl0_85
| spl0_86 ),
inference(sat_conversion,[],[f2552]) ).
cnf(s110,plain,
( spl0_9
| ~ spl0_86 ),
inference(sat_conversion,[],[f2653]) ).
cnf(s111,plain,
( spl0_1
| spl0_78 ),
inference(sat_conversion,[],[f2655]) ).
cnf(s114,plain,
( spl0_1
| spl0_81 ),
inference(sat_conversion,[],[f2658]) ).
cnf(s194,plain,
( ~ spl0_78
| spl0_111
| ~ spl0_112
| ~ spl0_130 ),
inference(sat_conversion,[],[f3419]) ).
cnf(s199,plain,
( spl0_1
| spl0_112 ),
inference(sat_conversion,[],[f3523]) ).
cnf(s200,plain,
( spl0_1
| ~ spl0_111 ),
inference(sat_conversion,[],[f3527]) ).
cnf(s208,plain,
( ~ spl0_35
| spl0_84 ),
inference(sat_conversion,[],[f4128]) ).
cnf(s397,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| spl0_9
| ~ spl0_16 ),
inference(sat_conversion,[],[f8898]) ).
cnf(s413,plain,
( ~ spl0_15
| spl0_35
| spl0_141 ),
inference(sat_conversion,[],[f9246]) ).
cnf(s427,plain,
~ spl0_159,
inference(sat_conversion,[],[f9706]) ).
cnf(s574,plain,
spl0_353,
inference(sat_conversion,[],[f13268]) ).
cnf(s672,plain,
( ~ spl0_3
| ~ spl0_5
| ~ spl0_15
| spl0_130
| ~ spl0_352 ),
inference(sat_conversion,[],[f16348]) ).
cnf(s723,plain,
( ~ spl0_3
| ~ spl0_5
| spl0_9
| spl0_19
| spl0_169
| ~ spl0_176 ),
inference(sat_conversion,[],[f16634]) ).
cnf(s738,plain,
~ spl0_378,
inference(sat_conversion,[],[f16659]) ).
cnf(s1613,plain,
( ~ spl0_3
| spl0_17
| ~ spl0_19
| ~ spl0_81
| ~ spl0_131
| ~ spl0_254 ),
inference(sat_conversion,[],[f35833]) ).
cnf(s1632,plain,
( ~ spl0_3
| ~ spl0_5
| spl0_9
| ~ spl0_78
| spl0_111
| ~ spl0_112
| spl0_131 ),
inference(sat_conversion,[],[f35940]) ).
cnf(s1716,plain,
( ~ spl0_3
| spl0_9
| ~ spl0_15
| spl0_35
| ~ spl0_141
| spl0_254 ),
inference(sat_conversion,[],[f37188]) ).
cnf(s1731,plain,
( ~ spl0_3
| spl0_9
| ~ spl0_15
| spl0_19
| spl0_28
| ~ spl0_169
| spl0_175 ),
inference(sat_conversion,[],[f37459]) ).
cnf(s2128,plain,
( ~ spl0_3
| ~ spl0_37
| spl0_159
| ~ spl0_167
| ~ spl0_254
| spl0_352
| ~ spl0_353 ),
inference(sat_conversion,[],[f39955]) ).
cnf(s2174,plain,
( spl0_84
| spl0_176
| spl0_378 ),
inference(sat_conversion,[],[f40084]) ).
cnf(s2213,plain,
( spl0_167
| ~ spl0_175
| ~ spl0_176
| spl0_378 ),
inference(sat_conversion,[],[f40359]) ).
cnf(s2284,plain,
~ spl0_86,
inference(rat,[],[s110,s17]) ).
cnf(s2285,plain,
~ spl0_84,
inference(rat,[],[s99,s17]) ).
cnf(s2286,plain,
spl0_176,
inference(rat,[],[s2174,s738,s2285]) ).
cnf(s2290,plain,
~ spl0_35,
inference(rat,[],[s208,s2285]) ).
cnf(s2291,plain,
~ spl0_85,
inference(rat,[],[s105,s2284,s17,s2285]) ).
cnf(s2295,plain,
~ spl0_1,
inference(rat,[],[s98,s2291,s2285]) ).
cnf(s2308,plain,
spl0_37,
inference(rat,[],[s42,s2290]) ).
cnf(s2315,plain,
~ spl0_111,
inference(rat,[],[s200,s2295]) ).
cnf(s2316,plain,
spl0_112,
inference(rat,[],[s199,s2295]) ).
cnf(s2317,plain,
spl0_81,
inference(rat,[],[s114,s2295]) ).
cnf(s2320,plain,
spl0_78,
inference(rat,[],[s111,s2295]) ).
cnf(s2366,plain,
~ spl0_130,
inference(rat,[],[s194,s2315,s2316,s2320]) ).
cnf(s2377,plain,
spl0_5,
inference(rat,[],[s5,s2295]) ).
cnf(s2378,plain,
spl0_3,
inference(rat,[],[s2,s2295]) ).
cnf(s2379,plain,
spl0_131,
inference(rat,[],[s1632,s2377,s2316,s2315,s2320,s17,s2378]) ).
cnf(s2395,plain,
spl0_2,
inference(rat,[],[s1,s2295]) ).
cnf(s2396,plain,
~ spl0_16,
inference(rat,[],[s397,s2378,s17,s2377,s2395]) ).
cnf(s2398,plain,
spl0_15,
inference(rat,[],[s14,s2396]) ).
cnf(s2417,plain,
spl0_141,
inference(rat,[],[s413,s2290,s2398]) ).
cnf(s2424,plain,
~ spl0_352,
inference(rat,[],[s672,s2378,s2366,s2377,s2398]) ).
cnf(s2471,plain,
spl0_254,
inference(rat,[],[s1716,s2398,s2378,s2290,s17,s2417]) ).
cnf(s2482,plain,
~ spl0_167,
inference(rat,[],[s2128,s574,s2424,s2378,s2308,s427,s2471]) ).
cnf(s2490,plain,
~ spl0_175,
inference(rat,[],[s2213,s738,s2286,s2482]) ).
cnf(s2492,plain,
spl0_19,
inference(rat,[],[s1731,s723,s40,s17,s2378,s2398,s2490,s2377,s2286]) ).
cnf(s2500,plain,
~ spl0_7,
inference(rat,[],[s29,s2492]) ).
cnf(s2503,plain,
spl0_17,
inference(rat,[],[s1613,s2471,s2379,s2317,s2378,s2492]) ).
cnf(s2506,plain,
spl0_6,
inference(rat,[],[s7,s2500]) ).
cnf(s2517,plain,
$false,
inference(rat,[],[s23,s2503,s2506]) ).
fof(f40541,plain,
$false,
inference(avatar_sat_refutation,[],[s2517]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC187-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.36 % Computer : n008.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 28 08:22:24 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 Running first-order model finding
% 0.11/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.38/1.27 % (2096080)Will run a generic schedule for satisfiability detection.
% 5.38/1.27 % (2096090)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=738042707:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.38/1.27 % (2096086)% WARNING: option uhcvi not known.
% 5.38/1.27 % (2096085)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=309442114_2999 on theBenchmark for (2999ds/0Mi)
% 5.38/1.27 % (2096088)dis+10_1_sil=32000:sp=arity:random_seed=242111916:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.38/1.27 % (2096086)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3878789417:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.38/1.27 % (2096087)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=883469733:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.38/1.27 % (2096089)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2530813369:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.38/1.27 % (2096091)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=726715954:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.38/1.27 % TRYING [1]
% 5.38/1.27 % TRYING [2]
% 5.38/1.27 % TRYING [3]
% 5.38/1.27 % (2096090)Instruction limit reached!
% 5.38/1.27 % (2096090)------------------------------
% 5.38/1.27 % (2096090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.38/1.27 % (2096090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.27 % (2096090)CaDiCaL version: 2.1.3
% 5.38/1.27 % (2096090)Termination reason: Instruction limit
% 5.38/1.27 % (2096090)Termination phase: Saturation
% 5.38/1.27 % (2096090)Time elapsed: 0.037 s
% 5.38/1.27 % (2096090)Peak memory usage: 14 MB
% 5.38/1.27 % (2096090)Instructions burned: 131 (million)
% 5.38/1.27 % TRYING [4]
% 5.38/1.27 % (2096099)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1971991098:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.38/1.27 % TRYING [1]
% 5.38/1.27 % TRYING [2]
% 5.38/1.27 % TRYING [3]
% 5.38/1.27 % (2096088)Instruction limit reached!
% 5.38/1.27 % (2096088)------------------------------
% 5.38/1.27 % (2096088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.38/1.27 % (2096088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.27 % (2096088)CaDiCaL version: 2.1.3
% 5.38/1.27 % (2096088)Termination reason: Instruction limit
% 5.38/1.27 % (2096088)Termination phase: Saturation
% 5.38/1.27 % (2096088)Time elapsed: 0.062 s
% 5.38/1.27 % (2096088)Peak memory usage: 13 MB
% 5.38/1.27 % (2096088)Instructions burned: 103 (million)
% 5.38/1.27 % (2096089)Instruction limit reached!
% 5.38/1.27 % (2096089)------------------------------
% 5.38/1.27 % (2096089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.38/1.27 % (2096089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.27 % (2096089)CaDiCaL version: 2.1.3
% 5.38/1.27 % (2096089)Termination reason: Instruction limit
% 5.38/1.27 % (2096089)Termination phase: Saturation
% 5.38/1.27 % (2096089)Time elapsed: 0.062 s
% 5.38/1.27 % (2096089)Peak memory usage: 13 MB
% 5.38/1.27 % (2096089)Instructions burned: 116 (million)
% 5.38/1.27 % TRYING [4]
% 5.38/1.27 % (2096101)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4291231378:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 5.38/1.27 % (2096102)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=1604310689:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.38/1.27 % (2096091)Instruction limit reached!
% 5.38/1.27 % (2096091)------------------------------
% 5.38/1.27 % (2096091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.38/1.27 % (2096091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.27 % (2096091)CaDiCaL version: 2.1.3
% 5.38/1.27 % (2096091)Termination reason: Instruction limit
% 5.38/1.27 % (2096091)Termination phase: Saturation
% 5.38/1.27 % (2096091)Time elapsed: 0.098 s
% 5.38/1.27 % (2096091)Peak memory usage: 14 MB
% 5.38/1.27 % (2096091)Instructions burned: 160 (million)
% 5.38/1.27 % TRYING [5]
% 5.38/1.27 % TRYING [5]
% 5.38/1.27 % (2096105)ott-21_1_sil=16000:fs=off:random_seed=1616310022:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.38/1.27 % (2096101)Instruction limit reached!
% 5.38/1.27 % (2096101)------------------------------
% 5.38/1.27 % (2096101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.38/1.27 % (2096101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.27 % (2096101)CaDiCaL version: 2.1.3
% 5.38/1.27 % (2096101)Termination reason: Instruction limit
% 5.38/1.27 % (2096101)Termination phase: Saturation
% 5.38/1.27 % (2096101)Time elapsed: 0.070 s
% 5.38/1.27 % (2096101)Peak memory usage: 13 MB
% 5.38/1.27 % (2096101)Instructions burned: 132 (million)
% 5.38/1.27 % (2096107)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1543826353:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 5.38/1.27 % TRYING [6]
% 5.38/1.27 % (2096099)Instruction limit reached!
% 5.38/1.27 % (2096099)------------------------------
% 5.38/1.27 % (2096099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.38/1.27 % (2096099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.27 % (2096099)CaDiCaL version: 2.1.3
% 5.38/1.27 % (2096099)Termination reason: Instruction limit
% 5.38/1.27 % (2096099)Termination phase: Finite model building constraint generation
% 5.38/1.27 % (2096099)Time elapsed: 0.154 s
% 5.38/1.27 % (2096099)Peak memory usage: 34 MB
% 5.38/1.27 % (2096099)Instructions burned: 716 (million)
% 5.38/1.27 % (2096105)Instruction limit reached!
% 5.38/1.27 % (2096105)------------------------------
% 5.38/1.27 % (2096105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.38/1.27 % (2096105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.27 % (2096105)CaDiCaL version: 2.1.3
% 5.38/1.27 % (2096105)Termination reason: Instruction limit
% 5.38/1.27 % (2096105)Termination phase: Saturation
% 5.38/1.27 % (2096105)Time elapsed: 0.087 s
% 5.38/1.27 % (2096105)Peak memory usage: 13 MB
% 5.38/1.27 % (2096105)Instructions burned: 181 (million)
% 5.38/1.27 % (2096109)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=110804127:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 5.38/1.27 % TRYING [1]
% 5.38/1.27 % TRYING [2]
% 5.38/1.27 % TRYING [3]
% 5.38/1.27 % (2096110)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2499481770:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 5.38/1.27 % TRYING [4]
% 5.38/1.27 % TRYING [6]
% 5.38/1.27 % TRYING [5]
% 5.38/1.27 % (2096109)Instruction limit reached!
% 5.38/1.27 % (2096109)------------------------------
% 5.38/1.27 % (2096109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.38/1.27 % (2096109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.27 % (2096109)CaDiCaL version: 2.1.3
% 5.38/1.27 % (2096109)Termination reason: Instruction limit
% 5.38/1.27 % (2096109)Termination phase: Finite model building SAT solving
% 5.38/1.27 % (2096109)Time elapsed: 0.179 s
% 5.38/1.27 % (2096109)Peak memory usage: 22 MB
% 5.38/1.27 % (2096109)Instructions burned: 869 (million)
% 5.38/1.27 % (2096113)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1656951509:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 5.38/1.27 % TRYING [14]
% 5.38/1.27 % (2096102)Instruction limit reached!
% 5.38/1.27 % (2096102)------------------------------
% 5.38/1.27 % (2096102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.38/1.27 % (2096102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.27 % (2096102)CaDiCaL version: 2.1.3
% 5.38/1.27 % (2096102)Termination reason: Instruction limit
% 5.38/1.27 % (2096102)Termination phase: Saturation
% 5.38/1.27 % (2096102)Time elapsed: 0.390 s
% 5.38/1.27 % (2096102)Peak memory usage: 19 MB
% 5.38/1.27 % (2096102)Instructions burned: 684 (million)
% 5.38/1.27 % (2096107)Instruction limit reached!
% 5.38/1.27 % (2096107)------------------------------
% 5.38/1.27 % (2096107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.38/1.27 % (2096107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.27 % (2096107)CaDiCaL version: 2.1.3
% 5.38/1.27 % (2096107)Termination reason: Instruction limit
% 5.38/1.27 % (2096107)Termination phase: Saturation
% 5.38/1.27 % (2096107)Time elapsed: 0.315 s
% 5.38/1.27 % (2096107)Peak memory usage: 14 MB
% 5.38/1.27 % (2096107)Instructions burned: 478 (million)
% 5.38/1.27 % (2096115)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=709946615:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 5.38/1.27 % (2096116)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2400888312:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 5.38/1.27 % (2096113)Instruction limit reached!
% 5.38/1.27 % (2096113)------------------------------
% 5.38/1.27 % (2096113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.38/1.27 % (2096113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.27 % (2096113)CaDiCaL version: 2.1.3
% 5.38/1.27 % (2096113)Termination reason: Instruction limit
% 5.38/1.27 % (2096113)Termination phase: Finite model building constraint generation
% 5.38/1.27 % (2096113)Time elapsed: 0.178 s
% 5.38/1.27 % (2096113)Peak memory usage: 73 MB
% 5.38/1.27 % (2096113)Instructions burned: 895 (million)
% 5.38/1.27 % (2096119)fmb+10_1_sil=64000:random_seed=1767522817:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 5.38/1.27 % TRYING [1]
% 5.38/1.27 % TRYING [2]
% 5.38/1.27 % TRYING [3]
% 5.38/1.27 % TRYING [4]
% 5.38/1.27 % TRYING [5]
% 5.38/1.27 % TRYING [7]
% 5.38/1.27 % (2096086) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2096080-2096086"...
% 5.38/1.27 % (2096086)...printing done.
% 5.38/1.27 % (2096086)Refutation found. Thanks to Tanya!
% 5.38/1.27 % SZS status Unsatisfiable for theBenchmark
% 5.38/1.27 % SZS output start Proof for theBenchmark
% See solution above
% 5.38/1.28 % (2096086)------------------------------
% 5.38/1.28 % (2096086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.38/1.28 % (2096086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.28 % (2096086)CaDiCaL version: 2.1.3
% 5.38/1.28 % (2096086)Termination reason: Refutation
% 5.38/1.28 % (2096086)Time elapsed: 0.811 s
% 5.38/1.28 % (2096086)Peak memory usage: 27 MB
% 5.38/1.28 % (2096086)Instructions burned: 1445 (million)
% 5.38/1.28 % (2096080)Success in time 0.862 s
% 5.38/1.28 % Vampire exiting
%------------------------------------------------------------------------------