%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC162-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 : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:04:54 PM UTC 2026
% Result : Unsatisfiable 38.59s 10.62s
% Output : Refutation 38.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 85
% Syntax : Number of formulae : 451 ( 70 unt; 33 def)
% Number of atoms : 1428 ( 214 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 1510 ( 533 ~; 944 |; 0 &)
% ( 33 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 44 ( 42 usr; 34 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 10 con; 0-2 aty)
% Number of variables : 310 ( 0 sgn 310 !; 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(f50,axiom,
! [X0,X1] : ssList(skaf46(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause50) ).
fof(f57,axiom,
! [X0] :
( ~ ssList(X0)
| segmentP(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause57) ).
fof(f58,axiom,
! [X0] :
( ~ ssList(X0)
| rearsegP(X0,nil) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause58) ).
fof(f59,axiom,
! [X0] :
( ~ ssList(X0)
| rearsegP(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause59) ).
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(f96,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| tl(cons(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause96) ).
fof(f97,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| hd(cons(X0,X1)) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause97) ).
fof(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(f125,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| app(cons(X0,nil),X1) = cons(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause120) ).
fof(f126,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(reorient_equations,[],[f125]) ).
fof(f134,axiom,
! [X0,X1] :
( ~ segmentP(X0,X1)
| ~ segmentP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| X1 = X0 ),
file('/export/starexec/sandbox2/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(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(f142,axiom,
! [X0,X1] :
( ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| app(skaf46(X0,X1),X1) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause131) ).
fof(f149,axiom,
! [X2,X0,X1] :
( X0 != X1
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0)
| memberP(cons(X1,X2),X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause138) ).
fof(f151,axiom,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| memberP(app(X0,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause140) ).
fof(f152,axiom,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssItem(X1)
| memberP(app(X2,X0),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause141) ).
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(f163,axiom,
! [X2,X0,X1] :
( app(X0,X1) != app(X2,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause151) ).
fof(f173,axiom,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X2 = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause161) ).
fof(f174,plain,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X0 = X2 ),
inference(reorient_equations,[],[f173]) ).
fof(f186,axiom,
! [X2,X3,X0,X1] :
( ~ segmentP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X3)
| ~ ssList(X1)
| ~ ssList(X0)
| segmentP(app(app(X3,X0),X2),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause172) ).
fof(f187,axiom,
! [X2,X3,X0,X1] :
( app(app(X0,X1),X2) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| segmentP(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause173) ).
fof(f189,axiom,
! [X2,X3,X0,X1] :
( app(X0,cons(X1,X2)) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(X3)
| memberP(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause175) ).
fof(f193,axiom,
! [X2,X3,X0,X1,X4] :
( app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(X4)
| ~ ssList(X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(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,
ssList(sk9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_12) ).
fof(f212,negated_conjecture,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_13) ).
fof(f213,plain,
sk1 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(reorient_equations,[],[f212]) ).
fof(f218,negated_conjecture,
( singletonP(sk3)
| ~ neq(sk4,nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_18) ).
fof(f219,plain,
ssList(sk3),
inference(definition_unfolding,[],[f200,f205]) ).
fof(f220,plain,
ssList(sk4),
inference(definition_unfolding,[],[f201,f204]) ).
fof(f221,plain,
sk3 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(definition_unfolding,[],[f213,f205]) ).
fof(f229,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(cons(X0,nil))
| singletonP(cons(X0,nil)) ),
inference(equality_resolution,[],[f119]) ).
fof(f231,plain,
! [X2,X1] :
( ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X1)
| memberP(cons(X1,X2),X1) ),
inference(equality_resolution,[],[f149]) ).
fof(f232,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(X0,X1))
| rearsegP(app(X0,X1),X1) ),
inference(equality_resolution,[],[f154]) ).
fof(f233,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1))
| frontsegP(app(X0,X1),X0) ),
inference(equality_resolution,[],[f155]) ).
fof(f236,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(f237,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,
! [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(f249,plain,
~ ssList(nil),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f253,plain,
! [X0] : ~ ssList(skaf82(X0)),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f290,plain,
! [X0,X1] : ~ ssList(skaf46(X0,X1)),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f296,plain,
! [X0] :
( segmentP(X0,X0)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f57]) ).
fof(f297,plain,
! [X0] :
( ~ rearsegP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f58]) ).
fof(f298,plain,
! [X0] :
( ~ rearsegP(X0,X0)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f59]) ).
fof(f299,plain,
! [X0] :
( ~ frontsegP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f310,plain,
! [X0] :
( ~ memberP(nil,X0)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f71]) ).
fof(f311,plain,
! [X0,X1] :
( ssList(X0)
| duplicatefreeP(X0)
| ~ ssItem(X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f312,plain,
! [X0] :
( ssList(X0)
| app(X0,nil) = X0 ),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f313,plain,
! [X0] :
( ssList(X0)
| app(nil,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f314,plain,
! [X0] :
( ~ ssList(tl(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f319,plain,
! [X0] :
( ~ segmentP(nil,X0)
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f324,plain,
! [X0,X1] :
( ~ ssList(app(X1,X0))
| ssList(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f325,plain,
! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f335,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| tl(cons(X0,X1)) = X1 ),
inference(consistent_polarity_flipping,[],[f96]) ).
fof(f336,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| hd(cons(X0,X1)) = X0 ),
inference(consistent_polarity_flipping,[],[f97]) ).
fof(f339,plain,
! [X0,X1] :
( ~ neq(X1,X0)
| ssList(X1)
| ssList(X0)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f102]) ).
fof(f340,plain,
! [X0] :
( ~ singletonP(X0)
| ssList(X0)
| cons(skaf44(X0),nil) = X0 ),
inference(consistent_polarity_flipping,[],[f103]) ).
fof(f343,plain,
! [X0] :
( ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f348,plain,
! [X0] :
( ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f355,plain,
! [X0] :
( singletonP(cons(X0,nil))
| ssList(cons(X0,nil))
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f229]) ).
fof(f357,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ssList(X1)
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f122]) ).
fof(f359,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f366,plain,
! [X0,X1] :
( ~ segmentP(X1,X0)
| ~ segmentP(X0,X1)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f367,plain,
! [X0,X1] :
( rearsegP(X0,X1)
| rearsegP(X1,X0)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f137]) ).
fof(f368,plain,
! [X0,X1] :
( frontsegP(X0,X1)
| frontsegP(X1,X0)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f370,plain,
! [X0,X1] :
( rearsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| app(skaf46(X0,X1),X1) = X0 ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f377,plain,
! [X2,X1] :
( ssList(X2)
| ssItem(X1)
| ssItem(X1)
| memberP(cons(X1,X2),X1) ),
inference(consistent_polarity_flipping,[],[f231]) ).
fof(f379,plain,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ssList(X2)
| ssList(X0)
| ssItem(X1)
| memberP(app(X0,X2),X1) ),
inference(consistent_polarity_flipping,[],[f151]) ).
fof(f380,plain,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ssList(X0)
| ssList(X2)
| ssItem(X1)
| memberP(app(X2,X0),X1) ),
inference(consistent_polarity_flipping,[],[f152]) ).
fof(f382,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X0,X1))
| ~ rearsegP(app(X0,X1),X1) ),
inference(consistent_polarity_flipping,[],[f232]) ).
fof(f383,plain,
! [X0,X1] :
( ssList(X1)
| ssList(X0)
| ssList(app(X0,X1))
| ~ frontsegP(app(X0,X1),X0) ),
inference(consistent_polarity_flipping,[],[f233]) ).
fof(f390,plain,
! [X2,X0,X1] :
( app(X0,X1) != app(X2,X1)
| ssList(X0)
| ssList(X1)
| ssList(X2)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f400,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(f411,plain,
! [X2,X3,X0,X1] :
( ~ segmentP(X0,X1)
| ssList(X2)
| ssList(X3)
| ssList(X1)
| ssList(X0)
| segmentP(app(app(X3,X0),X2),X1) ),
inference(consistent_polarity_flipping,[],[f186]) ).
fof(f412,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,[],[f236]) ).
fof(f414,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,[],[f237]) ).
fof(f418,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,[],[f239]) ).
fof(f425,plain,
~ ssList(sk3),
inference(consistent_polarity_flipping,[],[f219]) ).
fof(f426,plain,
~ ssList(sk4),
inference(consistent_polarity_flipping,[],[f220]) ).
fof(f429,plain,
~ ssItem(sk5),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f430,plain,
~ ssItem(sk6),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f431,plain,
~ ssList(sk7),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f432,plain,
~ ssList(sk8),
inference(consistent_polarity_flipping,[],[f210]) ).
fof(f433,plain,
~ ssList(sk9),
inference(consistent_polarity_flipping,[],[f211]) ).
fof(f438,plain,
( singletonP(sk3)
| neq(sk4,nil) ),
inference(consistent_polarity_flipping,[],[f218]) ).
fof(f441,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ssItem(X1)
| ssList(X2) ),
inference(duplicate_literal_removal,[],[f377]) ).
fof(f446,definition,
( spl0_1
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f448,plain,
( neq(sk4,nil)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f446]) ).
fof(f450,definition,
( spl0_2
<=> singletonP(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f452,plain,
( singletonP(sk3)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f450]) ).
fof(f453,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f438,f450,f446]) ).
fof(f482,definition,
( spl0_9
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f483,plain,
( ~ ssList(nil)
| spl0_9 ),
inference(avatar_component_clause,[],[f482]) ).
fof(f510,definition,
( spl0_15
<=> ! [X1] : ~ ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f511,plain,
( ! [X1] : ~ ssItem(X1)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f513,definition,
( spl0_16
<=> ! [X0] :
( ssList(X0)
| duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f514,plain,
( ! [X0] :
( duplicatefreeP(X0)
| ssList(X0) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f513]) ).
fof(f515,plain,
( spl0_15
| spl0_16 ),
inference(avatar_split_clause,[],[f311,f513,f510]) ).
fof(f518,plain,
~ spl0_9,
inference(avatar_split_clause,[],[f249,f482]) ).
fof(f522,plain,
( ! [X0] : ~ memberP(nil,X0)
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f310,f511]) ).
fof(f559,plain,
sk3 = app(sk3,nil),
inference(resolution,[],[f312,f425]) ).
fof(f592,plain,
sk3 = app(nil,sk3),
inference(resolution,[],[f313,f425]) ).
fof(f627,plain,
( ! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1) )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f325,f511]) ).
fof(f636,plain,
( ! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ssList(X2) )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f441,f511]) ).
fof(f638,plain,
( ! [X0,X1] :
( ssList(X1)
| tl(cons(X0,X1)) = X1 )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f335,f511]) ).
fof(f639,plain,
( ! [X0] : nil = tl(cons(X0,nil))
| spl0_9
| ~ spl0_15 ),
inference(resolution,[],[f638,f483]) ).
fof(f640,plain,
( ! [X0,X1] : skaf82(X1) = tl(cons(X0,skaf82(X1)))
| ~ spl0_15 ),
inference(resolution,[],[f638,f253]) ).
fof(f675,plain,
( ! [X0,X1] :
( ssList(X1)
| hd(cons(X0,X1)) = X0 )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f336,f511]) ).
fof(f676,plain,
( ! [X0] : hd(cons(X0,nil)) = X0
| spl0_9
| ~ spl0_15 ),
inference(resolution,[],[f675,f483]) ).
fof(f714,plain,
( ssList(sk3)
| sk3 = cons(skaf44(sk3),nil)
| ~ spl0_2 ),
inference(resolution,[],[f340,f452]) ).
fof(f715,plain,
( sk3 = cons(skaf44(sk3),nil)
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f714,f425]) ).
fof(f773,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| nil = sk3 ),
inference(resolution,[],[f343,f425]) ).
fof(f779,definition,
( spl0_17
<=> nil = sk9 ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f780,plain,
( nil != sk9
| spl0_17 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f781,plain,
( nil = sk9
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f783,definition,
( spl0_18
<=> sk9 = cons(hd(sk9),tl(sk9)) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f785,plain,
( sk9 = cons(hd(sk9),tl(sk9))
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f783]) ).
fof(f806,definition,
( spl0_23
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f808,plain,
( nil = sk4
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f806]) ).
fof(f815,definition,
( spl0_25
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f819,definition,
( spl0_26
<=> sk3 = cons(hd(sk3),tl(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f821,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f819]) ).
fof(f822,plain,
( spl0_25
| spl0_26 ),
inference(avatar_split_clause,[],[f773,f819,f815]) ).
fof(f861,definition,
( spl0_27
<=> sk9 = cons(skaf83(sk9),skaf82(sk9)) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f863,plain,
( sk9 = cons(skaf83(sk9),skaf82(sk9))
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f861]) ).
fof(f889,plain,
( nil != sk3
| ssList(sk9)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) ),
inference(superposition,[],[f357,f221]) ).
fof(f895,plain,
( nil != sk3
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) ),
inference(forward_subsumption_resolution,[],[f889,f433]) ).
fof(f897,definition,
( spl0_32
<=> nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f898,plain,
( nil != app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| spl0_32 ),
inference(avatar_component_clause,[],[f897]) ).
fof(f899,plain,
( nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f897]) ).
fof(f901,definition,
( spl0_33
<=> ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f902,plain,
( ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| spl0_33 ),
inference(avatar_component_clause,[],[f901]) ).
fof(f903,plain,
( ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f901]) ).
fof(f904,plain,
( spl0_32
| spl0_33
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f895,f815,f901,f897]) ).
fof(f913,plain,
( ! [X0,X1] :
( ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f359,f511]) ).
fof(f919,plain,
( ! [X0,X1] : cons(X0,skaf82(X1)) = app(cons(X0,nil),skaf82(X1))
| ~ spl0_15 ),
inference(resolution,[],[f913,f253]) ).
fof(f980,plain,
( segmentP(nil,sk3)
| ~ spl0_23 ),
inference(superposition,[],[f206,f808]) ).
fof(f983,plain,
( ssList(sk3)
| nil = sk3
| ~ spl0_23 ),
inference(resolution,[],[f980,f319]) ).
fof(f984,plain,
( nil = sk3
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f983,f425]) ).
fof(f1033,plain,
! [X0,X1] :
( ~ rearsegP(app(X0,X1),X1)
| ssList(X1)
| ssList(X0) ),
inference(forward_subsumption_resolution,[],[f382,f324]) ).
fof(f1035,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| rearsegP(X0,app(X1,X0))
| ssList(app(X1,X0))
| ssList(X0)
| app(X1,X0) = X0 ),
inference(resolution,[],[f1033,f367]) ).
fof(f1052,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| rearsegP(X0,app(X1,X0))
| ssList(app(X1,X0))
| app(X1,X0) = X0 ),
inference(duplicate_literal_removal,[],[f1035]) ).
fof(f1055,plain,
! [X0,X1] :
( rearsegP(X0,app(X1,X0))
| ssList(X1)
| ssList(X0)
| app(X1,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f1052,f324]) ).
fof(f1069,plain,
! [X0,X1] :
( ~ frontsegP(app(X0,X1),X0)
| ssList(X0)
| ssList(X1) ),
inference(forward_subsumption_resolution,[],[f383,f324]) ).
fof(f1071,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| frontsegP(X0,app(X0,X1))
| ssList(app(X0,X1))
| ssList(X0)
| app(X0,X1) = X0 ),
inference(resolution,[],[f1069,f368]) ).
fof(f1088,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| frontsegP(X0,app(X0,X1))
| ssList(app(X0,X1))
| app(X0,X1) = X0 ),
inference(duplicate_literal_removal,[],[f1071]) ).
fof(f1091,plain,
! [X0,X1] :
( frontsegP(X0,app(X0,X1))
| ssList(X1)
| ssList(X0)
| app(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f1088,f324]) ).
fof(f1183,plain,
! [X0] :
( ssList(X0)
| ssList(X0)
| app(skaf46(X0,X0),X0) = X0
| ssList(X0) ),
inference(resolution,[],[f370,f298]) ).
fof(f1186,plain,
! [X0] :
( ssList(X0)
| app(skaf46(X0,X0),X0) = X0 ),
inference(duplicate_literal_removal,[],[f1183]) ).
fof(f1347,plain,
( ! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ssList(X2)
| ssList(X0)
| memberP(app(X0,X2),X1) )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f379,f511]) ).
fof(f1352,plain,
( ! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ssList(X0)
| ssList(X2)
| memberP(app(X2,X0),X1) )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f380,f511]) ).
fof(f1353,plain,
( ! [X2,X0,X1] :
( ssList(cons(X0,X1))
| ssList(X2)
| memberP(app(X2,cons(X0,X1)),X0)
| ssList(X1) )
| ~ spl0_15 ),
inference(resolution,[],[f1352,f636]) ).
fof(f1356,plain,
( ! [X2,X0,X1] :
( memberP(app(X2,cons(X0,X1)),X0)
| ssList(X2)
| ssList(X1) )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1353,f627]) ).
fof(f1662,plain,
! [X0] :
( sk3 != app(X0,sk9)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(sk9)
| ssList(X0)
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0 ),
inference(superposition,[],[f390,f221]) ).
fof(f1669,plain,
! [X0] :
( sk3 != app(X0,sk3)
| ssList(X0)
| ssList(sk3)
| ssList(nil)
| nil = X0 ),
inference(superposition,[],[f390,f592]) ).
fof(f1677,plain,
! [X0] :
( sk3 != app(X0,sk9)
| ssList(X0)
| ssList(sk9)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0 ),
inference(superposition,[],[f390,f221]) ).
fof(f1692,plain,
! [X0] :
( sk3 != app(X0,sk9)
| ssList(X0)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0 ),
inference(forward_subsumption_resolution,[],[f1677,f433]) ).
fof(f1700,plain,
! [X0] :
( sk3 != app(X0,sk3)
| ssList(X0)
| ssList(nil)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f1669,f425]) ).
fof(f1706,plain,
! [X0] :
( sk3 != app(X0,sk9)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(X0)
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0 ),
inference(forward_subsumption_resolution,[],[f1662,f433]) ).
fof(f1728,plain,
( ! [X0] :
( sk3 != app(X0,sk3)
| ssList(X0)
| nil = X0 )
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f1700,f483]) ).
fof(f2032,plain,
( ! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ssList(X1)
| ssItem(X0)
| memberP(X1,X2)
| X0 = X2 )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f400,f511]) ).
fof(f2033,plain,
( ! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ssList(X1)
| memberP(X1,X2)
| X0 = X2 )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f2032,f511]) ).
fof(f2162,plain,
( spl0_25
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f984,f806,f815]) ).
fof(f2676,plain,
( ssList(sk4)
| ssList(nil)
| nil = sk4
| ~ spl0_1 ),
inference(resolution,[],[f448,f339]) ).
fof(f2677,plain,
( ssList(nil)
| nil = sk4
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f2676,f426]) ).
fof(f2687,plain,
( nil = sk4
| ~ spl0_1
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f2677,f483]) ).
fof(f2688,plain,
( spl0_23
| ~ spl0_1
| spl0_9 ),
inference(avatar_split_clause,[],[f2687,f482,f446,f806]) ).
fof(f2953,plain,
! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(X2)
| ssList(X2)
| segmentP(app(app(X1,X2),X0),X2)
| ssList(X2) ),
inference(resolution,[],[f411,f296]) ).
fof(f2959,plain,
! [X2,X0,X1] :
( segmentP(app(app(X1,X2),X0),X2)
| ssList(X1)
| ssList(X2)
| ssList(X0) ),
inference(duplicate_literal_removal,[],[f2953]) ).
fof(f3005,plain,
! [X0] :
( segmentP(app(sk3,X0),sk9)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(sk9)
| ssList(app(sk3,X0))
| ssList(X0) ),
inference(superposition,[],[f412,f221]) ).
fof(f3018,plain,
! [X0] :
( segmentP(app(sk3,X0),sk9)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(app(sk3,X0))
| ssList(X0) ),
inference(forward_subsumption_resolution,[],[f3005,f433]) ).
fof(f3042,definition,
( spl0_79
<=> ssList(cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f3043,plain,
( ~ ssList(cons(sk6,nil))
| spl0_79 ),
inference(avatar_component_clause,[],[f3042]) ).
fof(f3044,plain,
( ssList(cons(sk6,nil))
| ~ spl0_79 ),
inference(avatar_component_clause,[],[f3042]) ).
fof(f3139,definition,
( spl0_92
<=> ! [X0] :
( app(X0,nil) != sk3
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0
| ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f3140,plain,
( ! [X0] :
( app(X0,nil) != sk3
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0
| ssList(X0) )
| ~ spl0_92 ),
inference(avatar_component_clause,[],[f3139]) ).
fof(f3145,definition,
( spl0_93
<=> ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f3146,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| spl0_93 ),
inference(avatar_component_clause,[],[f3145]) ).
fof(f3147,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_93 ),
inference(avatar_component_clause,[],[f3145]) ).
fof(f3196,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,[],[f418,f514]) ).
fof(f3206,definition,
( spl0_98
<=> ! [X3] : ssList(X3) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f3207,plain,
( ! [X3] : ssList(X3)
| ~ spl0_98 ),
inference(avatar_component_clause,[],[f3206]) ).
fof(f3209,definition,
( spl0_99
<=> ! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X1,cons(X2,X0)))
| ssItem(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f3210,plain,
( ! [X2,X0,X1] :
( ssList(app(X1,cons(X2,X0)))
| ssList(X1)
| ssList(X0)
| ssItem(X2) )
| ~ spl0_99 ),
inference(avatar_component_clause,[],[f3209]) ).
fof(f3311,definition,
( spl0_109
<=> nil = tl(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f3313,plain,
( nil = tl(sk3)
| ~ spl0_109 ),
inference(avatar_component_clause,[],[f3311]) ).
fof(f3378,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,[],[f414,f511]) ).
fof(f3614,plain,
( ssList(nil)
| ssItem(sk6)
| ~ spl0_79 ),
inference(resolution,[],[f325,f3044]) ).
fof(f3626,plain,
( ssItem(sk6)
| spl0_9
| ~ spl0_79 ),
inference(forward_subsumption_resolution,[],[f3614,f483]) ).
fof(f3627,plain,
( $false
| spl0_9
| ~ spl0_79 ),
inference(forward_subsumption_resolution,[],[f3626,f430]) ).
fof(f3628,plain,
( spl0_9
| ~ spl0_79 ),
inference(avatar_contradiction_clause,[],[f3627]) ).
fof(f5036,definition,
( spl0_145
<=> nil = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f5037,plain,
( nil != cons(sk5,nil)
| spl0_145 ),
inference(avatar_component_clause,[],[f5036]) ).
fof(f5038,plain,
( nil = cons(sk5,nil)
| ~ spl0_145 ),
inference(avatar_component_clause,[],[f5036]) ).
fof(f5040,definition,
( spl0_146
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f5041,plain,
( ~ ssList(cons(sk5,nil))
| spl0_146 ),
inference(avatar_component_clause,[],[f5040]) ).
fof(f5042,plain,
( ssList(cons(sk5,nil))
| ~ spl0_146 ),
inference(avatar_component_clause,[],[f5040]) ).
fof(f5065,plain,
( singletonP(nil)
| ssList(nil)
| ssItem(sk5)
| ~ spl0_145 ),
inference(superposition,[],[f355,f5038]) ).
fof(f5119,plain,
( ssList(nil)
| ssItem(sk5)
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f5065,f11]) ).
fof(f5147,plain,
( ssItem(sk5)
| spl0_9
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f5119,f483]) ).
fof(f5153,plain,
( $false
| spl0_9
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f5147,f429]) ).
fof(f5154,plain,
( spl0_9
| ~ spl0_145 ),
inference(avatar_contradiction_clause,[],[f5153]) ).
fof(f5195,plain,
( ssList(nil)
| ssItem(sk5)
| ~ spl0_146 ),
inference(resolution,[],[f5042,f325]) ).
fof(f5196,plain,
( ssItem(sk5)
| spl0_9
| ~ spl0_146 ),
inference(forward_subsumption_resolution,[],[f5195,f483]) ).
fof(f5197,plain,
( $false
| spl0_9
| ~ spl0_146 ),
inference(forward_subsumption_resolution,[],[f5196,f429]) ).
fof(f5198,plain,
( spl0_9
| ~ spl0_146 ),
inference(avatar_contradiction_clause,[],[f5197]) ).
fof(f6346,plain,
( ! [X2,X3,X0,X1] :
( ssList(X0)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2)
| ssList(X3)
| ssList(app(X0,cons(X1,X2)))
| memberP(app(app(X0,cons(X1,X2)),X3),X1) )
| ~ spl0_15 ),
inference(resolution,[],[f3378,f1347]) ).
fof(f6348,plain,
( ! [X2,X3,X0,X1] :
( memberP(app(app(X0,cons(X1,X2)),X3),X1)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2)
| ssList(X3)
| ssList(X0) )
| ~ spl0_15 ),
inference(duplicate_literal_removal,[],[f6346]) ).
fof(f6410,plain,
( ! [X0] :
( app(X0,nil) != sk3
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(X0)
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0 )
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1706,f781]) ).
fof(f6441,plain,
( spl0_33
| spl0_92
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f6410,f779,f3139,f901]) ).
fof(f7637,plain,
( sk3 = cons(hd(sk3),nil)
| ~ spl0_26
| ~ spl0_109 ),
inference(superposition,[],[f821,f3313]) ).
fof(f8320,plain,
( ! [X2,X3,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssItem(X2)
| ssList(X3)
| ssList(app(X1,cons(X2,X0)))
| ssList(cons(X2,X3)) )
| ~ spl0_16 ),
inference(resolution,[],[f3196,f324]) ).
fof(f8349,plain,
( ! [X2,X3,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssItem(X2)
| ssList(X3)
| ssList(app(X1,cons(X2,X0))) )
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f8320,f325]) ).
fof(f8364,plain,
( spl0_98
| spl0_99
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f8349,f513,f3209,f3206]) ).
fof(f9854,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ssList(cons(sk6,nil))
| ~ spl0_33 ),
inference(resolution,[],[f903,f324]) ).
fof(f10630,plain,
( nil != nil
| ssList(cons(sk6,nil))
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = app(app(sk7,cons(sk5,nil)),sk8)
| ~ spl0_32 ),
inference(superposition,[],[f357,f899]) ).
fof(f10643,plain,
( ssList(cons(sk6,nil))
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = app(app(sk7,cons(sk5,nil)),sk8)
| ~ spl0_32 ),
inference(trivial_inequality_removal,[],[f10630]) ).
fof(f10655,definition,
( spl0_372
<=> ssList(app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_372])],[avatar_definition]) ).
fof(f10656,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| spl0_372 ),
inference(avatar_component_clause,[],[f10655]) ).
fof(f10657,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_372 ),
inference(avatar_component_clause,[],[f10655]) ).
fof(f13541,plain,
( $false
| ~ spl0_98 ),
inference(backward_subsumption_resolution,[],[f433,f3207]) ).
fof(f13586,plain,
~ spl0_98,
inference(avatar_contradiction_clause,[],[f13541]) ).
fof(f17048,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ssList(sk8)
| ~ spl0_93 ),
inference(resolution,[],[f324,f3147]) ).
fof(f17146,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_93 ),
inference(forward_subsumption_resolution,[],[f17048,f432]) ).
fof(f17148,plain,
( spl0_372
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f17146,f3145,f10655]) ).
fof(f17167,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_33
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f9854,f3043]) ).
fof(f17169,plain,
( spl0_93
| ~ spl0_33
| spl0_79 ),
inference(avatar_split_clause,[],[f17167,f3042,f901,f3145]) ).
fof(f17386,definition,
( spl0_433
<=> sk3 = cons(sk6,nil) ),
introduced(definition,[new_symbols(definition,[spl0_433])],[avatar_definition]) ).
fof(f17388,plain,
( sk3 = cons(sk6,nil)
| ~ spl0_433 ),
inference(avatar_component_clause,[],[f17386]) ).
fof(f17665,definition,
( spl0_440
<=> nil = app(app(sk7,cons(sk5,nil)),sk8) ),
introduced(definition,[new_symbols(definition,[spl0_440])],[avatar_definition]) ).
fof(f17666,plain,
( nil != app(app(sk7,cons(sk5,nil)),sk8)
| spl0_440 ),
inference(avatar_component_clause,[],[f17665]) ).
fof(f17667,plain,
( nil = app(app(sk7,cons(sk5,nil)),sk8)
| ~ spl0_440 ),
inference(avatar_component_clause,[],[f17665]) ).
fof(f18076,plain,
( sk3 != sk3
| sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ssList(sk3)
| ~ spl0_92 ),
inference(superposition,[],[f3140,f559]) ).
fof(f18081,plain,
( sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ssList(sk3)
| ~ spl0_92 ),
inference(trivial_inequality_removal,[],[f18076]) ).
fof(f18085,plain,
( sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ spl0_92 ),
inference(forward_subsumption_resolution,[],[f18081,f425]) ).
fof(f20857,plain,
sk3 = app(skaf46(sk3,sk3),sk3),
inference(resolution,[],[f1186,f425]) ).
fof(f22266,plain,
( ssList(sk7)
| ssList(cons(sk5,nil))
| ~ spl0_372 ),
inference(resolution,[],[f10657,f324]) ).
fof(f22267,plain,
( ssList(cons(sk5,nil))
| ~ spl0_372 ),
inference(forward_subsumption_resolution,[],[f22266,f431]) ).
fof(f22268,plain,
( $false
| spl0_146
| ~ spl0_372 ),
inference(forward_subsumption_resolution,[],[f22267,f5041]) ).
fof(f22269,plain,
( spl0_146
| ~ spl0_372 ),
inference(avatar_contradiction_clause,[],[f22268]) ).
fof(f22631,definition,
( spl0_549
<=> nil = app(sk7,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_549])],[avatar_definition]) ).
fof(f22632,plain,
( nil != app(sk7,cons(sk5,nil))
| spl0_549 ),
inference(avatar_component_clause,[],[f22631]) ).
fof(f22633,plain,
( nil = app(sk7,cons(sk5,nil))
| ~ spl0_549 ),
inference(avatar_component_clause,[],[f22631]) ).
fof(f29082,plain,
( ssList(sk7)
| ssList(nil)
| ssItem(sk5)
| ~ spl0_99
| spl0_372 ),
inference(resolution,[],[f3210,f10656]) ).
fof(f29116,plain,
( ssList(nil)
| ssItem(sk5)
| ~ spl0_99
| spl0_372 ),
inference(forward_subsumption_resolution,[],[f29082,f431]) ).
fof(f29137,plain,
( ssItem(sk5)
| spl0_9
| ~ spl0_99
| spl0_372 ),
inference(forward_subsumption_resolution,[],[f29116,f483]) ).
fof(f29147,plain,
( $false
| spl0_9
| ~ spl0_99
| spl0_372 ),
inference(forward_subsumption_resolution,[],[f29137,f429]) ).
fof(f29148,plain,
( spl0_9
| ~ spl0_99
| spl0_372 ),
inference(avatar_contradiction_clause,[],[f29147]) ).
fof(f30544,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ssList(tl(sk3))
| memberP(tl(sk3),X0)
| hd(sk3) = X0 )
| ~ spl0_15
| ~ spl0_26 ),
inference(superposition,[],[f2033,f821]) ).
fof(f30559,plain,
( ! [X0] :
( ssList(nil)
| ~ memberP(sk3,X0)
| memberP(tl(sk3),X0)
| hd(sk3) = X0 )
| ~ spl0_15
| ~ spl0_26
| ~ spl0_109 ),
inference(forward_demodulation,[],[f30544,f3313]) ).
fof(f30574,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| memberP(tl(sk3),X0)
| hd(sk3) = X0 )
| spl0_9
| ~ spl0_15
| ~ spl0_26
| ~ spl0_109 ),
inference(forward_subsumption_resolution,[],[f30559,f483]) ).
fof(f30584,plain,
( ! [X0] :
( memberP(nil,X0)
| ~ memberP(sk3,X0)
| hd(sk3) = X0 )
| spl0_9
| ~ spl0_15
| ~ spl0_26
| ~ spl0_109 ),
inference(forward_demodulation,[],[f30574,f3313]) ).
fof(f30593,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| hd(sk3) = X0 )
| spl0_9
| ~ spl0_15
| ~ spl0_26
| ~ spl0_109 ),
inference(forward_subsumption_resolution,[],[f30584,f522]) ).
fof(f31296,definition,
( spl0_777
<=> sk6 = hd(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_777])],[avatar_definition]) ).
fof(f31298,plain,
( sk6 = hd(sk3)
| ~ spl0_777 ),
inference(avatar_component_clause,[],[f31296]) ).
fof(f35320,plain,
( ! [X0] : app(sk3,skaf82(X0)) = cons(skaf44(sk3),skaf82(X0))
| ~ spl0_2
| ~ spl0_15 ),
inference(superposition,[],[f919,f715]) ).
fof(f43257,plain,
! [X0] :
( segmentP(app(sk3,X0),sk3)
| ssList(nil)
| ssList(sk3)
| ssList(X0) ),
inference(superposition,[],[f2959,f592]) ).
fof(f43409,plain,
( ! [X0] :
( segmentP(app(sk3,X0),sk3)
| ssList(sk3)
| ssList(X0) )
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f43257,f483]) ).
fof(f43483,plain,
( ! [X0] :
( segmentP(app(sk3,X0),sk3)
| ssList(X0) )
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f43409,f425]) ).
fof(f72337,plain,
( rearsegP(cons(sk5,nil),nil)
| ssList(sk7)
| ssList(cons(sk5,nil))
| nil = cons(sk5,nil)
| ~ spl0_549 ),
inference(superposition,[],[f1055,f22633]) ).
fof(f72349,plain,
( ssList(sk7)
| ssList(cons(sk5,nil))
| nil = cons(sk5,nil)
| ~ spl0_549 ),
inference(forward_subsumption_resolution,[],[f72337,f297]) ).
fof(f72380,plain,
( ssList(cons(sk5,nil))
| nil = cons(sk5,nil)
| ~ spl0_549 ),
inference(forward_subsumption_resolution,[],[f72349,f431]) ).
fof(f72403,plain,
( nil = cons(sk5,nil)
| spl0_146
| ~ spl0_549 ),
inference(forward_subsumption_resolution,[],[f72380,f5041]) ).
fof(f72416,plain,
( $false
| spl0_145
| spl0_146
| ~ spl0_549 ),
inference(forward_subsumption_resolution,[],[f72403,f5037]) ).
fof(f72417,plain,
( spl0_145
| spl0_146
| ~ spl0_549 ),
inference(avatar_contradiction_clause,[],[f72416]) ).
fof(f87305,plain,
( memberP(sk3,sk6)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ssList(nil)
| ssList(sk9)
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_15 ),
inference(superposition,[],[f6348,f221]) ).
fof(f87307,plain,
( memberP(sk3,sk6)
| ssList(nil)
| ssList(sk9)
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_15
| spl0_33 ),
inference(forward_subsumption_resolution,[],[f87305,f902]) ).
fof(f87354,plain,
( memberP(sk3,sk6)
| ssList(sk9)
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| spl0_9
| ~ spl0_15
| spl0_33 ),
inference(forward_subsumption_resolution,[],[f87307,f483]) ).
fof(f87365,plain,
( memberP(sk3,sk6)
| ssList(sk9)
| spl0_9
| ~ spl0_15
| spl0_33
| spl0_93 ),
inference(forward_subsumption_resolution,[],[f87354,f3146]) ).
fof(f87522,plain,
( sk3 = cons(sk6,nil)
| ~ spl0_26
| ~ spl0_109
| ~ spl0_777 ),
inference(superposition,[],[f7637,f31298]) ).
fof(f87541,plain,
( spl0_433
| ~ spl0_26
| ~ spl0_109
| ~ spl0_777 ),
inference(avatar_split_clause,[],[f87522,f31296,f3311,f819,f17386]) ).
fof(f160266,plain,
( frontsegP(app(sk7,cons(sk5,nil)),nil)
| ssList(sk8)
| ssList(app(sk7,cons(sk5,nil)))
| nil = app(sk7,cons(sk5,nil))
| ~ spl0_440 ),
inference(superposition,[],[f1091,f17667]) ).
fof(f160285,plain,
( ssList(sk8)
| ssList(app(sk7,cons(sk5,nil)))
| nil = app(sk7,cons(sk5,nil))
| ~ spl0_440 ),
inference(forward_subsumption_resolution,[],[f160266,f299]) ).
fof(f160318,plain,
( ssList(app(sk7,cons(sk5,nil)))
| nil = app(sk7,cons(sk5,nil))
| ~ spl0_440 ),
inference(forward_subsumption_resolution,[],[f160285,f432]) ).
fof(f160346,plain,
( nil = app(sk7,cons(sk5,nil))
| spl0_372
| ~ spl0_440 ),
inference(forward_subsumption_resolution,[],[f160318,f10656]) ).
fof(f160362,plain,
( $false
| spl0_372
| ~ spl0_440
| spl0_549 ),
inference(forward_subsumption_resolution,[],[f160346,f22632]) ).
fof(f160363,plain,
( spl0_372
| ~ spl0_440
| spl0_549 ),
inference(avatar_contradiction_clause,[],[f160362]) ).
fof(f167794,plain,
( sk3 != sk3
| ssList(skaf46(sk3,sk3))
| nil = skaf46(sk3,sk3)
| spl0_9 ),
inference(superposition,[],[f1728,f20857]) ).
fof(f167799,plain,
( ssList(skaf46(sk3,sk3))
| nil = skaf46(sk3,sk3)
| spl0_9 ),
inference(trivial_inequality_removal,[],[f167794]) ).
fof(f167801,plain,
( nil = skaf46(sk3,sk3)
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f167799,f290]) ).
fof(f285899,plain,
( sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),sk3)
| ~ spl0_92
| ~ spl0_433 ),
inference(forward_demodulation,[],[f18085,f17388]) ).
fof(f285911,plain,
( sk3 != sk3
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = app(app(sk7,cons(sk5,nil)),sk8)
| spl0_9
| ~ spl0_92
| ~ spl0_433 ),
inference(superposition,[],[f1728,f285899]) ).
fof(f285935,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = app(app(sk7,cons(sk5,nil)),sk8)
| spl0_9
| ~ spl0_92
| ~ spl0_433 ),
inference(trivial_inequality_removal,[],[f285911]) ).
fof(f285951,plain,
( nil = app(app(sk7,cons(sk5,nil)),sk8)
| spl0_9
| ~ spl0_92
| spl0_93
| ~ spl0_433 ),
inference(forward_subsumption_resolution,[],[f285935,f3146]) ).
fof(f285968,plain,
( $false
| spl0_9
| ~ spl0_92
| spl0_93
| ~ spl0_433
| spl0_440 ),
inference(forward_subsumption_resolution,[],[f285951,f17666]) ).
fof(f285969,plain,
( spl0_9
| ~ spl0_92
| spl0_93
| ~ spl0_433
| spl0_440 ),
inference(avatar_contradiction_clause,[],[f285968]) ).
fof(f286044,definition,
( spl0_5589
<=> ssList(sk9) ),
introduced(definition,[new_symbols(definition,[spl0_5589])],[avatar_definition]) ).
fof(f286045,plain,
( ~ ssList(sk9)
| spl0_5589 ),
inference(avatar_component_clause,[],[f286044]) ).
fof(f286456,plain,
( ! [X0] :
( sk3 != app(X0,sk9)
| ssList(X0)
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0 )
| spl0_33 ),
inference(forward_subsumption_resolution,[],[f1692,f902]) ).
fof(f286458,plain,
( ! [X0] :
( segmentP(app(sk3,X0),sk9)
| ssList(app(sk3,X0))
| ssList(X0) )
| spl0_33 ),
inference(forward_subsumption_resolution,[],[f3018,f902]) ).
fof(f286505,plain,
~ spl0_5589,
inference(avatar_split_clause,[],[f433,f286044]) ).
fof(f286511,definition,
( spl0_5628
<=> sk3 = sk9 ),
introduced(definition,[new_symbols(definition,[spl0_5628])],[avatar_definition]) ).
fof(f286512,plain,
( sk3 = sk9
| ~ spl0_5628 ),
inference(avatar_component_clause,[],[f286511]) ).
fof(f286572,definition,
( spl0_5638
<=> memberP(sk3,sk6) ),
introduced(definition,[new_symbols(definition,[spl0_5638])],[avatar_definition]) ).
fof(f286574,plain,
( memberP(sk3,sk6)
| ~ spl0_5638 ),
inference(avatar_component_clause,[],[f286572]) ).
fof(f286575,plain,
( spl0_5589
| spl0_5638
| spl0_9
| ~ spl0_15
| spl0_33
| spl0_93 ),
inference(avatar_split_clause,[],[f87365,f3145,f901,f510,f482,f286572,f286044]) ).
fof(f287673,plain,
( sk9 = cons(hd(sk9),tl(sk9))
| nil = sk9
| spl0_5589 ),
inference(resolution,[],[f286045,f343]) ).
fof(f287674,plain,
( sk9 = cons(skaf83(sk9),skaf82(sk9))
| nil = sk9
| spl0_5589 ),
inference(resolution,[],[f286045,f348]) ).
fof(f288450,plain,
( sk9 = cons(skaf83(sk9),skaf82(sk9))
| spl0_17
| spl0_5589 ),
inference(forward_subsumption_resolution,[],[f287674,f780]) ).
fof(f288451,plain,
( sk9 = cons(hd(sk9),tl(sk9))
| spl0_17
| spl0_5589 ),
inference(forward_subsumption_resolution,[],[f287673,f780]) ).
fof(f288485,plain,
( spl0_27
| spl0_17
| spl0_5589 ),
inference(avatar_split_clause,[],[f288450,f286044,f779,f861]) ).
fof(f288486,plain,
( spl0_18
| spl0_17
| spl0_5589 ),
inference(avatar_split_clause,[],[f288451,f286044,f779,f783]) ).
fof(f290937,plain,
( ! [X0] :
( sk3 != app(X0,sk3)
| ssList(X0)
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0 )
| spl0_33
| ~ spl0_5628 ),
inference(forward_demodulation,[],[f286456,f286512]) ).
fof(f290942,plain,
( sk3 != sk3
| ssList(skaf46(sk3,sk3))
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = skaf46(sk3,sk3)
| spl0_33
| ~ spl0_5628 ),
inference(superposition,[],[f290937,f20857]) ).
fof(f290947,plain,
( ssList(skaf46(sk3,sk3))
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = skaf46(sk3,sk3)
| spl0_33
| ~ spl0_5628 ),
inference(trivial_inequality_removal,[],[f290942]) ).
fof(f290949,plain,
( app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = skaf46(sk3,sk3)
| spl0_33
| ~ spl0_5628 ),
inference(forward_subsumption_resolution,[],[f290947,f290]) ).
fof(f290951,plain,
( nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| spl0_9
| spl0_33
| ~ spl0_5628 ),
inference(forward_demodulation,[],[f290949,f167801]) ).
fof(f290954,plain,
( $false
| spl0_9
| spl0_32
| spl0_33
| ~ spl0_5628 ),
inference(forward_subsumption_resolution,[],[f290951,f898]) ).
fof(f290955,plain,
( spl0_9
| spl0_32
| spl0_33
| ~ spl0_5628 ),
inference(avatar_contradiction_clause,[],[f290954]) ).
fof(f290962,plain,
( ! [X0] :
( memberP(app(X0,sk9),hd(sk9))
| ssList(X0)
| ssList(tl(sk9)) )
| ~ spl0_15
| ~ spl0_18 ),
inference(superposition,[],[f1356,f785]) ).
fof(f291033,definition,
( spl0_5924
<=> ssList(tl(sk9)) ),
introduced(definition,[new_symbols(definition,[spl0_5924])],[avatar_definition]) ).
fof(f291035,plain,
( ssList(tl(sk9))
| ~ spl0_5924 ),
inference(avatar_component_clause,[],[f291033]) ).
fof(f291037,definition,
( spl0_5925
<=> sk6 = hd(sk9) ),
introduced(definition,[new_symbols(definition,[spl0_5925])],[avatar_definition]) ).
fof(f291039,plain,
( sk6 = hd(sk9)
| ~ spl0_5925 ),
inference(avatar_component_clause,[],[f291037]) ).
fof(f291338,definition,
( spl0_5995
<=> ! [X0] :
( memberP(app(X0,sk9),hd(sk9))
| ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_5995])],[avatar_definition]) ).
fof(f291339,plain,
( ! [X0] :
( memberP(app(X0,sk9),hd(sk9))
| ssList(X0) )
| ~ spl0_5995 ),
inference(avatar_component_clause,[],[f291338]) ).
fof(f291340,plain,
( spl0_5924
| spl0_5995
| ~ spl0_15
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f290962,f783,f510,f291338,f291033]) ).
fof(f291359,plain,
( tl(sk9) = skaf82(sk9)
| ~ spl0_15
| ~ spl0_27 ),
inference(superposition,[],[f640,f863]) ).
fof(f291970,plain,
( segmentP(sk3,sk9)
| ssList(sk3)
| ssList(nil)
| spl0_33 ),
inference(superposition,[],[f286458,f559]) ).
fof(f291979,plain,
( segmentP(sk3,sk9)
| ssList(nil)
| spl0_33 ),
inference(forward_subsumption_resolution,[],[f291970,f425]) ).
fof(f291986,plain,
( segmentP(sk3,sk9)
| spl0_9
| spl0_33 ),
inference(forward_subsumption_resolution,[],[f291979,f483]) ).
fof(f292713,plain,
( ~ segmentP(sk9,sk3)
| ssList(sk9)
| ssList(sk3)
| sk3 = sk9
| spl0_9
| spl0_33 ),
inference(resolution,[],[f291986,f366]) ).
fof(f292714,plain,
( ~ segmentP(sk9,sk3)
| ssList(sk3)
| sk3 = sk9
| spl0_9
| spl0_33
| spl0_5589 ),
inference(forward_subsumption_resolution,[],[f292713,f286045]) ).
fof(f292718,plain,
( ~ segmentP(sk9,sk3)
| sk3 = sk9
| spl0_9
| spl0_33
| spl0_5589 ),
inference(forward_subsumption_resolution,[],[f292714,f425]) ).
fof(f292723,plain,
( ssList(sk9)
| nil = sk9
| ~ spl0_5924 ),
inference(resolution,[],[f291035,f314]) ).
fof(f292724,plain,
( nil = sk9
| spl0_5589
| ~ spl0_5924 ),
inference(forward_subsumption_resolution,[],[f292723,f286045]) ).
fof(f292725,plain,
( $false
| spl0_17
| spl0_5589
| ~ spl0_5924 ),
inference(forward_subsumption_resolution,[],[f292724,f780]) ).
fof(f292726,plain,
( spl0_17
| spl0_5589
| ~ spl0_5924 ),
inference(avatar_contradiction_clause,[],[f292725]) ).
fof(f294127,plain,
( nil = tl(sk3)
| ~ spl0_2
| spl0_9
| ~ spl0_15 ),
inference(superposition,[],[f639,f715]) ).
fof(f294131,plain,
( spl0_109
| ~ spl0_2
| spl0_9
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f294127,f510,f482,f450,f3311]) ).
fof(f294134,plain,
( skaf44(sk3) = hd(sk3)
| ~ spl0_2
| spl0_9
| ~ spl0_15 ),
inference(superposition,[],[f676,f715]) ).
fof(f299097,plain,
( sk9 = cons(sk6,tl(sk9))
| ~ spl0_18
| ~ spl0_5925 ),
inference(superposition,[],[f785,f291039]) ).
fof(f299118,plain,
( sk6 = hd(sk3)
| spl0_9
| ~ spl0_15
| ~ spl0_26
| ~ spl0_109
| ~ spl0_5638 ),
inference(resolution,[],[f30593,f286574]) ).
fof(f299119,plain,
( spl0_777
| spl0_9
| ~ spl0_15
| ~ spl0_26
| ~ spl0_109
| ~ spl0_5638 ),
inference(avatar_split_clause,[],[f299118,f286572,f3311,f819,f510,f482,f31296]) ).
fof(f314419,plain,
( memberP(sk3,hd(sk9))
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ spl0_5995 ),
inference(superposition,[],[f291339,f221]) ).
fof(f314421,plain,
( memberP(sk3,hd(sk9))
| spl0_33
| ~ spl0_5995 ),
inference(forward_subsumption_resolution,[],[f314419,f902]) ).
fof(f314505,plain,
( hd(sk3) = hd(sk9)
| spl0_9
| ~ spl0_15
| ~ spl0_26
| spl0_33
| ~ spl0_109
| ~ spl0_5995 ),
inference(resolution,[],[f314421,f30593]) ).
fof(f314523,plain,
( sk6 = hd(sk9)
| spl0_9
| ~ spl0_15
| ~ spl0_26
| spl0_33
| ~ spl0_109
| ~ spl0_777
| ~ spl0_5995 ),
inference(forward_demodulation,[],[f314505,f31298]) ).
fof(f314552,plain,
( spl0_5925
| spl0_9
| ~ spl0_15
| ~ spl0_26
| spl0_33
| ~ spl0_109
| ~ spl0_777
| ~ spl0_5995 ),
inference(avatar_split_clause,[],[f314523,f291338,f31296,f3311,f901,f819,f510,f482,f291037]) ).
fof(f325570,plain,
( ! [X0] : app(sk3,skaf82(X0)) = cons(hd(sk3),skaf82(X0))
| ~ spl0_2
| spl0_9
| ~ spl0_15 ),
inference(forward_demodulation,[],[f35320,f294134]) ).
fof(f325571,plain,
( ! [X0] : cons(sk6,skaf82(X0)) = app(sk3,skaf82(X0))
| ~ spl0_2
| spl0_9
| ~ spl0_15
| ~ spl0_777 ),
inference(forward_demodulation,[],[f325570,f31298]) ).
fof(f325591,plain,
( ! [X0] :
( segmentP(cons(sk6,skaf82(X0)),sk3)
| ssList(skaf82(X0)) )
| ~ spl0_2
| spl0_9
| ~ spl0_15
| ~ spl0_777 ),
inference(superposition,[],[f43483,f325571]) ).
fof(f325645,plain,
( ! [X0] : segmentP(cons(sk6,skaf82(X0)),sk3)
| ~ spl0_2
| spl0_9
| ~ spl0_15
| ~ spl0_777 ),
inference(forward_subsumption_resolution,[],[f325591,f253]) ).
fof(f329908,plain,
( segmentP(cons(sk6,tl(sk9)),sk3)
| ~ spl0_2
| spl0_9
| ~ spl0_15
| ~ spl0_27
| ~ spl0_777 ),
inference(superposition,[],[f325645,f291359]) ).
fof(f363688,plain,
( segmentP(sk9,sk3)
| ~ spl0_2
| spl0_9
| ~ spl0_15
| ~ spl0_18
| ~ spl0_27
| ~ spl0_777
| ~ spl0_5925 ),
inference(forward_demodulation,[],[f329908,f299097]) ).
fof(f363774,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = app(app(sk7,cons(sk5,nil)),sk8)
| ~ spl0_32
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f10643,f3043]) ).
fof(f363817,definition,
( spl0_8006
<=> segmentP(sk9,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_8006])],[avatar_definition]) ).
fof(f363820,plain,
( spl0_5628
| ~ spl0_8006
| spl0_9
| spl0_33
| spl0_5589 ),
inference(avatar_split_clause,[],[f292718,f286044,f901,f482,f363817,f286511]) ).
fof(f363834,plain,
( spl0_8006
| ~ spl0_2
| spl0_9
| ~ spl0_15
| ~ spl0_18
| ~ spl0_27
| ~ spl0_777
| ~ spl0_5925 ),
inference(avatar_split_clause,[],[f363688,f291037,f31296,f861,f783,f510,f482,f450,f363817]) ).
fof(f364702,plain,
( nil = app(app(sk7,cons(sk5,nil)),sk8)
| ~ spl0_32
| spl0_79
| spl0_93 ),
inference(forward_subsumption_resolution,[],[f363774,f3146]) ).
fof(f365039,plain,
( $false
| ~ spl0_32
| spl0_79
| spl0_93
| spl0_440 ),
inference(forward_subsumption_resolution,[],[f364702,f17666]) ).
fof(f365040,plain,
( ~ spl0_32
| spl0_79
| spl0_93
| spl0_440 ),
inference(avatar_contradiction_clause,[],[f365039]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f453]) ).
cnf(s11,plain,
( spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f515]) ).
cnf(s14,plain,
~ spl0_9,
inference(sat_conversion,[],[f518]) ).
cnf(s19,plain,
( spl0_25
| spl0_26 ),
inference(sat_conversion,[],[f822]) ).
cnf(s25,plain,
( ~ spl0_25
| spl0_32
| spl0_33 ),
inference(sat_conversion,[],[f904]) ).
cnf(s59,plain,
( ~ spl0_23
| spl0_25 ),
inference(sat_conversion,[],[f2162]) ).
cnf(s123,plain,
( ~ spl0_1
| spl0_9
| spl0_23 ),
inference(sat_conversion,[],[f2688]) ).
cnf(s213,plain,
( spl0_9
| ~ spl0_79 ),
inference(sat_conversion,[],[f3628]) ).
cnf(s307,plain,
( spl0_9
| ~ spl0_145 ),
inference(sat_conversion,[],[f5154]) ).
cnf(s310,plain,
( spl0_9
| ~ spl0_146 ),
inference(sat_conversion,[],[f5198]) ).
cnf(s417,plain,
( ~ spl0_17
| spl0_33
| spl0_92 ),
inference(sat_conversion,[],[f6441]) ).
cnf(s555,plain,
( ~ spl0_16
| spl0_98
| spl0_99 ),
inference(sat_conversion,[],[f8364]) ).
cnf(s804,plain,
~ spl0_98,
inference(sat_conversion,[],[f13586]) ).
cnf(s876,plain,
( ~ spl0_93
| spl0_372 ),
inference(sat_conversion,[],[f17148]) ).
cnf(s895,plain,
( ~ spl0_33
| spl0_79
| spl0_93 ),
inference(sat_conversion,[],[f17169]) ).
cnf(s1069,plain,
( spl0_146
| ~ spl0_372 ),
inference(sat_conversion,[],[f22269]) ).
cnf(s1362,plain,
( spl0_9
| ~ spl0_99
| spl0_372 ),
inference(sat_conversion,[],[f29148]) ).
cnf(s2550,plain,
( spl0_145
| spl0_146
| ~ spl0_549 ),
inference(sat_conversion,[],[f72417]) ).
cnf(s3498,plain,
( ~ spl0_26
| ~ spl0_109
| spl0_433
| ~ spl0_777 ),
inference(sat_conversion,[],[f87541]) ).
cnf(s8454,plain,
( spl0_372
| ~ spl0_440
| spl0_549 ),
inference(sat_conversion,[],[f160363]) ).
cnf(s11113,plain,
( spl0_9
| ~ spl0_92
| spl0_93
| ~ spl0_433
| spl0_440 ),
inference(sat_conversion,[],[f285969]) ).
cnf(s11178,plain,
~ spl0_5589,
inference(sat_conversion,[],[f286505]) ).
cnf(s11194,plain,
( spl0_9
| ~ spl0_15
| spl0_33
| spl0_93
| spl0_5589
| spl0_5638 ),
inference(sat_conversion,[],[f286575]) ).
cnf(s11668,plain,
( spl0_17
| spl0_27
| spl0_5589 ),
inference(sat_conversion,[],[f288485]) ).
cnf(s11669,plain,
( spl0_17
| spl0_18
| spl0_5589 ),
inference(sat_conversion,[],[f288486]) ).
cnf(s11864,plain,
( spl0_9
| spl0_32
| spl0_33
| ~ spl0_5628 ),
inference(sat_conversion,[],[f290955]) ).
cnf(s11934,plain,
( ~ spl0_15
| ~ spl0_18
| spl0_5924
| spl0_5995 ),
inference(sat_conversion,[],[f291340]) ).
cnf(s11982,plain,
( spl0_17
| spl0_5589
| ~ spl0_5924 ),
inference(sat_conversion,[],[f292726]) ).
cnf(s11992,plain,
( ~ spl0_2
| spl0_9
| ~ spl0_15
| spl0_109 ),
inference(sat_conversion,[],[f294131]) ).
cnf(s12185,plain,
( spl0_9
| ~ spl0_15
| ~ spl0_26
| ~ spl0_109
| spl0_777
| ~ spl0_5638 ),
inference(sat_conversion,[],[f299119]) ).
cnf(s13696,plain,
( spl0_9
| ~ spl0_15
| ~ spl0_26
| spl0_33
| ~ spl0_109
| ~ spl0_777
| spl0_5925
| ~ spl0_5995 ),
inference(sat_conversion,[],[f314552]) ).
cnf(s15213,plain,
( spl0_9
| spl0_33
| spl0_5589
| spl0_5628
| ~ spl0_8006 ),
inference(sat_conversion,[],[f363820]) ).
cnf(s15215,plain,
( ~ spl0_2
| spl0_9
| ~ spl0_15
| ~ spl0_18
| ~ spl0_27
| ~ spl0_777
| ~ spl0_5925
| spl0_8006 ),
inference(sat_conversion,[],[f363834]) ).
cnf(s15485,plain,
( ~ spl0_32
| spl0_79
| spl0_93
| spl0_440 ),
inference(sat_conversion,[],[f365040]) ).
cnf(s16109,plain,
( ~ spl0_16
| spl0_99 ),
inference(rat,[],[s555,s804]) ).
cnf(s16132,plain,
~ spl0_146,
inference(rat,[],[s310,s14]) ).
cnf(s16133,plain,
~ spl0_145,
inference(rat,[],[s307,s14]) ).
cnf(s16135,plain,
~ spl0_79,
inference(rat,[],[s213,s14]) ).
cnf(s16136,plain,
~ spl0_372,
inference(rat,[],[s1069,s16132]) ).
cnf(s16137,plain,
~ spl0_549,
inference(rat,[],[s2550,s16132,s16133]) ).
cnf(s16146,plain,
~ spl0_440,
inference(rat,[],[s8454,s16137,s16136]) ).
cnf(s16147,plain,
~ spl0_93,
inference(rat,[],[s876,s16136]) ).
cnf(s16149,plain,
~ spl0_99,
inference(rat,[],[s1362,s14,s16136]) ).
cnf(s16300,plain,
~ spl0_32,
inference(rat,[],[s15485,s16146,s16135,s16147]) ).
cnf(s16301,plain,
~ spl0_33,
inference(rat,[],[s895,s16135,s16147]) ).
cnf(s16303,plain,
~ spl0_16,
inference(rat,[],[s16109,s16149]) ).
cnf(s16386,plain,
~ spl0_25,
inference(rat,[],[s25,s16301,s16300]) ).
cnf(s16399,plain,
~ spl0_5628,
inference(rat,[],[s11864,s16300,s14,s16301]) ).
cnf(s16415,plain,
~ spl0_23,
inference(rat,[],[s59,s16386]) ).
cnf(s16417,plain,
spl0_26,
inference(rat,[],[s19,s16386]) ).
cnf(s16420,plain,
~ spl0_8006,
inference(rat,[],[s15213,s16301,s14,s11178,s16399]) ).
cnf(s16744,plain,
~ spl0_1,
inference(rat,[],[s123,s14,s16415]) ).
cnf(s16895,plain,
spl0_15,
inference(rat,[],[s11,s16303]) ).
cnf(s16958,plain,
spl0_5638,
inference(rat,[],[s11194,s16301,s11178,s16147,s14,s16895]) ).
cnf(s17344,plain,
spl0_2,
inference(rat,[],[s1,s16744]) ).
cnf(s17345,plain,
spl0_109,
inference(rat,[],[s11992,s16895,s14,s17344]) ).
cnf(s17351,plain,
spl0_777,
inference(rat,[],[s12185,s16958,s16895,s16417,s14,s17345]) ).
cnf(s17581,plain,
spl0_433,
inference(rat,[],[s3498,s17345,s16417,s17351]) ).
cnf(s17603,plain,
~ spl0_92,
inference(rat,[],[s11113,s16146,s16147,s14,s17581]) ).
cnf(s17795,plain,
~ spl0_17,
inference(rat,[],[s417,s16301,s17603]) ).
cnf(s17803,plain,
~ spl0_5924,
inference(rat,[],[s11982,s11178,s17795]) ).
cnf(s17804,plain,
spl0_18,
inference(rat,[],[s11669,s11178,s17795]) ).
cnf(s17805,plain,
spl0_27,
inference(rat,[],[s11668,s11178,s17795]) ).
cnf(s18086,plain,
spl0_5995,
inference(rat,[],[s11934,s17803,s16895,s17804]) ).
cnf(s18132,plain,
~ spl0_5925,
inference(rat,[],[s15215,s16420,s17804,s17351,s17344,s16895,s14,s17805]) ).
cnf(s18333,plain,
$false,
inference(rat,[],[s13696,s17351,s17345,s16895,s16417,s16301,s14,s18086,s18132]) ).
fof(f365554,plain,
$false,
inference(avatar_sat_refutation,[],[s18333]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC162-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.11/0.38 % Computer : n013.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 08:13:22 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 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
% 13.25/2.38 % (1018537)Will run a generic schedule for satisfiability detection.
% 13.25/2.38 % (1018547)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2193632044:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.25/2.38 % (1018543)% WARNING: option uhcvi not known.
% 13.25/2.38 % (1018544)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1121194290:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.25/2.38 % (1018542)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=716967553_2999 on theBenchmark for (2999ds/0Mi)
% 13.25/2.38 % (1018543)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2272957446:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.25/2.38 % (1018545)dis+10_1_sil=32000:sp=arity:random_seed=96331810:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.25/2.38 % (1018546)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3517038698:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.25/2.38 % (1018548)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1206808310:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.25/2.38 % TRYING [1]
% 13.25/2.38 % TRYING [2]
% 13.25/2.38 % TRYING [3]
% 13.25/2.38 % (1018547)Instruction limit reached!
% 13.25/2.38 % (1018547)------------------------------
% 13.25/2.38 % (1018547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.25/2.38 % (1018547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.25/2.38 % (1018547)CaDiCaL version: 2.1.3
% 13.25/2.38 % (1018547)Termination reason: Instruction limit
% 13.25/2.38 % (1018547)Termination phase: Saturation
% 13.25/2.38 % (1018547)Time elapsed: 0.036 s
% 13.25/2.38 % (1018547)Peak memory usage: 14 MB
% 13.25/2.38 % (1018547)Instructions burned: 131 (million)
% 13.25/2.38 % TRYING [4]
% 13.25/2.38 % (1018556)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=416132827:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.25/2.38 % TRYING [1]
% 13.25/2.38 % TRYING [2]
% 13.25/2.38 % TRYING [3]
% 13.25/2.38 % (1018546)Instruction limit reached!
% 13.25/2.38 % (1018546)------------------------------
% 13.25/2.38 % (1018546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.25/2.38 % (1018546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.25/2.38 % (1018546)CaDiCaL version: 2.1.3
% 13.25/2.38 % (1018546)Termination reason: Instruction limit
% 13.25/2.38 % (1018546)Termination phase: Saturation
% 13.25/2.38 % (1018546)Time elapsed: 0.058 s
% 13.25/2.38 % (1018546)Peak memory usage: 13 MB
% 13.25/2.38 % (1018546)Instructions burned: 117 (million)
% 13.25/2.38 % (1018545)Instruction limit reached!
% 13.25/2.38 % (1018545)------------------------------
% 13.25/2.38 % (1018545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.25/2.38 % (1018545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.25/2.38 % (1018545)CaDiCaL version: 2.1.3
% 13.25/2.38 % (1018545)Termination reason: Instruction limit
% 13.25/2.38 % (1018545)Termination phase: Saturation
% 13.25/2.38 % (1018545)Time elapsed: 0.059 s
% 13.25/2.38 % (1018545)Peak memory usage: 13 MB
% 13.25/2.38 % (1018545)Instructions burned: 104 (million)
% 13.25/2.38 % TRYING [4]
% 13.25/2.38 % (1018558)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=847270460:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 13.25/2.38 % (1018559)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=3141371092:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 13.25/2.38 % (1018548)Instruction limit reached!
% 13.25/2.38 % (1018548)------------------------------
% 13.25/2.38 % (1018548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.25/2.38 % (1018548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.25/2.38 % TRYING [5]
% 13.25/2.38 % (1018548)CaDiCaL version: 2.1.3
% 13.25/2.38 % (1018548)Termination reason: Instruction limit
% 13.25/2.38 % (1018548)Termination phase: Saturation
% 13.25/2.38 % (1018548)Time elapsed: 0.095 s
% 13.25/2.38 % (1018548)Peak memory usage: 14 MB
% 13.25/2.38 % (1018548)Instructions burned: 159 (million)
% 13.25/2.38 % TRYING [5]
% 13.25/2.38 % (1018562)ott-21_1_sil=16000:fs=off:random_seed=1778741833:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.25/2.38 % (1018558)Instruction limit reached!
% 13.25/2.38 % (1018558)------------------------------
% 13.25/2.38 % (1018558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.44/5.87 % (1018558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.44/5.87 % (1018558)CaDiCaL version: 2.1.3
% 37.44/5.87 % (1018558)Termination reason: Instruction limit
% 37.44/5.87 % (1018558)Termination phase: Saturation
% 37.44/5.87 % (1018558)Time elapsed: 0.069 s
% 37.44/5.87 % (1018558)Peak memory usage: 14 MB
% 37.44/5.87 % (1018558)Instructions burned: 132 (million)
% 37.44/5.87 % (1018564)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3335197826:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 37.44/5.87 % TRYING [6]
% 37.44/5.87 % (1018556)Instruction limit reached!
% 37.44/5.87 % (1018556)------------------------------
% 37.44/5.87 % (1018556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.44/5.87 % (1018556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.44/5.87 % (1018556)CaDiCaL version: 2.1.3
% 37.44/5.87 % (1018556)Termination reason: Instruction limit
% 37.44/5.87 % (1018556)Termination phase: Finite model building constraint generation
% 37.44/5.87 % (1018556)Time elapsed: 0.150 s
% 37.44/5.87 % (1018556)Peak memory usage: 34 MB
% 37.44/5.87 % (1018556)Instructions burned: 716 (million)
% 37.44/5.87 % (1018562)Instruction limit reached!
% 37.44/5.87 % (1018562)------------------------------
% 37.44/5.87 % (1018562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.44/5.87 % (1018562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.44/5.87 % (1018562)CaDiCaL version: 2.1.3
% 37.44/5.87 % (1018562)Termination reason: Instruction limit
% 37.44/5.87 % (1018562)Termination phase: Saturation
% 37.44/5.87 % (1018562)Time elapsed: 0.090 s
% 37.44/5.87 % (1018562)Peak memory usage: 13 MB
% 37.44/5.87 % (1018562)Instructions burned: 181 (million)
% 37.44/5.87 % (1018566)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1878863476:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 37.44/5.87 % TRYING [1]
% 37.44/5.87 % TRYING [2]
% 37.44/5.87 % (1018567)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=25793926:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 37.44/5.87 % TRYING [3]
% 37.44/5.87 % TRYING [4]
% 37.44/5.87 % TRYING [6]
% 37.44/5.87 % TRYING [5]
% 37.44/5.87 % (1018566)Instruction limit reached!
% 37.44/5.87 % (1018566)------------------------------
% 37.44/5.87 % (1018566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.44/5.87 % (1018566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.44/5.87 % (1018566)CaDiCaL version: 2.1.3
% 37.44/5.87 % (1018566)Termination reason: Instruction limit
% 37.44/5.87 % (1018566)Termination phase: Finite model building SAT solving
% 37.44/5.87 % (1018566)Time elapsed: 0.193 s
% 37.44/5.87 % (1018566)Peak memory usage: 22 MB
% 37.44/5.87 % (1018566)Instructions burned: 865 (million)
% 37.44/5.87 % (1018570)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2643632943:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 37.44/5.87 % TRYING [14]
% 37.44/5.87 % (1018559)Instruction limit reached!
% 37.44/5.87 % (1018559)------------------------------
% 37.44/5.87 % (1018559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.44/5.87 % (1018559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.44/5.87 % (1018559)CaDiCaL version: 2.1.3
% 37.44/5.87 % (1018559)Termination reason: Instruction limit
% 37.44/5.87 % (1018559)Termination phase: Saturation
% 37.44/5.87 % (1018559)Time elapsed: 0.395 s
% 37.44/5.87 % (1018559)Peak memory usage: 21 MB
% 37.44/5.88 % (1018559)Instructions burned: 684 (million)
% 37.44/5.88 % (1018572)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=1581832802: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)
% 37.44/5.88 % (1018564)Instruction limit reached!
% 37.44/5.88 % (1018564)------------------------------
% 37.44/5.88 % (1018564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.44/5.88 % (1018564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.44/5.88 % (1018564)CaDiCaL version: 2.1.3
% 37.44/5.88 % (1018564)Termination reason: Instruction limit
% 37.44/5.88 % (1018564)Termination phase: Saturation
% 37.44/5.88 % (1018564)Time elapsed: 0.328 s
% 37.44/5.88 % (1018564)Peak memory usage: 15 MB
% 37.44/5.88 % (1018564)Instructions burned: 478 (million)
% 37.44/5.88 % (1018574)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=344622319:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 37.44/5.88 % (1018570)Instruction limit reached!
% 68.13/10.07 % (1018570)------------------------------
% 68.13/10.07 % (1018570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.13/10.07 % (1018570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.13/10.07 % (1018570)CaDiCaL version: 2.1.3
% 68.13/10.07 % (1018570)Termination reason: Instruction limit
% 68.13/10.07 % (1018570)Termination phase: Finite model building constraint generation
% 68.13/10.07 % (1018570)Time elapsed: 0.177 s
% 68.13/10.07 % (1018570)Peak memory usage: 73 MB
% 68.13/10.07 % (1018570)Instructions burned: 891 (million)
% 68.13/10.07 % (1018576)fmb+10_1_sil=64000:random_seed=584944391:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 68.13/10.07 % TRYING [1]
% 68.13/10.07 % TRYING [2]
% 68.13/10.07 % TRYING [3]
% 68.13/10.07 % TRYING [4]
% 68.13/10.07 % TRYING [5]
% 68.13/10.07 % TRYING [7]
% 68.13/10.07 % (1018567)Instruction limit reached!
% 68.13/10.07 % (1018567)------------------------------
% 68.13/10.07 % (1018567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.13/10.07 % (1018567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.13/10.07 % (1018567)CaDiCaL version: 2.1.3
% 68.13/10.07 % (1018567)Termination reason: Instruction limit
% 68.13/10.07 % (1018567)Termination phase: Saturation
% 68.13/10.07 % (1018567)Time elapsed: 0.638 s
% 68.13/10.07 % (1018567)Peak memory usage: 25 MB
% 68.13/10.07 % (1018567)Instructions burned: 1179 (million)
% 68.13/10.07 % (1018572)Instruction limit reached!
% 68.13/10.07 % (1018572)------------------------------
% 68.13/10.07 % (1018572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.13/10.07 % (1018572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.13/10.07 % (1018572)CaDiCaL version: 2.1.3
% 68.13/10.07 % (1018572)Termination reason: Instruction limit
% 68.13/10.07 % (1018572)Termination phase: Saturation
% 68.13/10.07 % (1018572)Time elapsed: 0.371 s
% 68.13/10.07 % (1018572)Peak memory usage: 22 MB
% 68.13/10.07 % (1018572)Instructions burned: 694 (million)
% 68.13/10.07 % (1018578)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4171648028:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 68.13/10.07 % (1018579)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=274403263:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 68.13/10.07 % TRYING [20]
% 68.13/10.07 % TRYING [8]
% 68.13/10.07 % TRYING [6]
% 68.13/10.07 % (1018574)Instruction limit reached!
% 68.13/10.07 % (1018574)------------------------------
% 68.13/10.07 % (1018574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.13/10.07 % (1018574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.13/10.07 % (1018574)CaDiCaL version: 2.1.3
% 68.13/10.07 % (1018574)Termination reason: Instruction limit
% 68.13/10.07 % (1018574)Termination phase: Saturation
% 68.13/10.07 % (1018574)Time elapsed: 0.456 s
% 68.13/10.07 % (1018574)Peak memory usage: 19 MB
% 68.13/10.07 % (1018574)Instructions burned: 880 (million)
% 68.13/10.07 % (1018582)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3618952651:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 68.13/10.07 % (1018579)Instruction limit reached!
% 68.13/10.07 % (1018579)------------------------------
% 68.13/10.07 % (1018579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.13/10.07 % (1018579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.13/10.07 % (1018579)CaDiCaL version: 2.1.3
% 68.13/10.07 % (1018579)Termination reason: Instruction limit
% 68.13/10.07 % (1018579)Termination phase: Finite model building constraint generation
% 68.13/10.07 % (1018579)Time elapsed: 0.336 s
% 68.13/10.07 % (1018579)Peak memory usage: 79 MB
% 68.13/10.07 % (1018579)Instructions burned: 923 (million)
% 68.13/10.07 % (1018584)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=709167760:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 68.13/10.07 % TRYING [7]
% 68.13/10.07 % TRYING [8]
% 68.13/10.07 % (1018584)Instruction limit reached!
% 68.13/10.07 % (1018584)------------------------------
% 68.13/10.07 % (1018584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.13/10.07 % (1018584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.13/10.07 % (1018584)CaDiCaL version: 2.1.3
% 68.13/10.07 % (1018584)Termination reason: Instruction limit
% 68.13/10.07 % (1018584)Termination phase: Saturation
% 68.13/10.07 % (1018584)Time elapsed: 0.641 s
% 68.13/10.07 % (1018584)Peak memory usage: 15 MB
% 68.13/10.07 % (1018584)Instructions burned: 1472 (million)
% 68.13/10.07 % (1018586)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=539462470:i=6324_2980 on theBenchmark for (2980ds/6324Mi)
% 38.59/10.61 % TRYING [77]
% 38.59/10.61 % TRYING [8]
% 38.59/10.61 % (1018582)Instruction limit reached!
% 38.59/10.61 % (1018582)------------------------------
% 38.59/10.61 % (1018582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.59/10.61 % (1018582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.59/10.61 % (1018582)CaDiCaL version: 2.1.3
% 38.59/10.61 % (1018582)Termination reason: Instruction limit
% 38.59/10.61 % (1018582)Termination phase: Saturation
% 38.59/10.61 % (1018582)Time elapsed: 2.596 s
% 38.59/10.61 % (1018582)Peak memory usage: 57 MB
% 38.59/10.61 % (1018582)Instructions burned: 5131 (million)
% 38.59/10.61 % (1018588)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3760041465:fmbsr=2.30978:i=2174_2963 on theBenchmark for (2963ds/2174Mi)
% 38.59/10.61 % TRYING [16]
% 38.59/10.61 % TRYING [9]
% 38.59/10.61 % (1018578)Instruction limit reached!
% 38.59/10.61 % (1018578)------------------------------
% 38.59/10.61 % (1018578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.59/10.61 % (1018578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.59/10.62 % (1018578)CaDiCaL version: 2.1.3
% 38.59/10.62 % (1018578)Termination reason: Instruction limit
% 38.59/10.62 % (1018578)Termination phase: Finite model building constraint generation
% 38.59/10.62 % (1018578)Time elapsed: 3.285 s
% 38.59/10.62 % (1018578)Peak memory usage: 588 MB
% 38.59/10.62 % (1018578)Instructions burned: 9517 (million)
% 38.59/10.62 % (1018586)Instruction limit reached!
% 38.59/10.62 % (1018586)------------------------------
% 38.59/10.62 % (1018586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.59/10.62 % (1018586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.59/10.62 % (1018586)CaDiCaL version: 2.1.3
% 38.59/10.62 % (1018586)Termination reason: Instruction limit
% 38.59/10.62 % (1018586)Termination phase: Finite model building constraint generation
% 38.59/10.62 % (1018586)Time elapsed: 2.256 s
% 38.59/10.62 % (1018586)Peak memory usage: 427 MB
% 38.59/10.62 % (1018586)Instructions burned: 6324 (million)
% 38.59/10.62 % (1018590)ott-2_1_sil=16000:newcnf=on:random_seed=3554664658:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 38.59/10.62 % (1018592)ott+10_1_sil=32000:tgt=ground:random_seed=1263363020:i=5114:av=off_2957 on theBenchmark for (2957ds/5114Mi)
% 38.59/10.62 % (1018588)Instruction limit reached!
% 38.59/10.62 % (1018588)------------------------------
% 38.59/10.62 % (1018588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.59/10.62 % (1018588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.59/10.62 % (1018588)CaDiCaL version: 2.1.3
% 38.59/10.62 % (1018588)Termination reason: Instruction limit
% 38.59/10.62 % (1018588)Termination phase: Finite model building constraint generation
% 38.59/10.62 % (1018588)Time elapsed: 0.761 s
% 38.59/10.62 % (1018588)Peak memory usage: 138 MB
% 38.59/10.62 % (1018588)Instructions burned: 2175 (million)
% 38.59/10.62 % (1018594)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1083669616:i=54282_2955 on theBenchmark for (2955ds/54282Mi)
% 38.59/10.62 % TRYING [1]
% 38.59/10.62 % TRYING [2]
% 38.59/10.62 % TRYING [3]
% 38.59/10.62 % TRYING [4]
% 38.59/10.62 % TRYING [5]
% 38.59/10.62 % TRYING [9]
% 38.59/10.62 % TRYING [6]
% 38.59/10.62 % (1018590)Instruction limit reached!
% 38.59/10.62 % (1018590)------------------------------
% 38.59/10.62 % (1018590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.59/10.62 % (1018590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.59/10.62 % (1018590)CaDiCaL version: 2.1.3
% 38.59/10.62 % (1018590)Termination reason: Instruction limit
% 38.59/10.62 % (1018590)Termination phase: Saturation
% 38.59/10.62 % (1018590)Time elapsed: 0.442 s
% 38.59/10.62 % (1018590)Peak memory usage: 22 MB
% 38.59/10.62 % (1018590)Instructions burned: 871 (million)
% 38.59/10.62 % (1018596)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3961277104:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi)
% 38.59/10.62 % TRYING [7]
% 38.59/10.62 % (1018576)Instruction limit reached!
% 38.59/10.62 % (1018576)------------------------------
% 38.59/10.62 % (1018576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.59/10.62 % (1018576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.59/10.62 % (1018576)CaDiCaL version: 2.1.3
% 38.59/10.62 % (1018576)Termination reason: Instruction limit
% 38.59/10.62 % (1018576)Termination phase: Finite model building constraint generation
% 38.59/10.62 % (1018576)Time elapsed: 4.800 s
% 38.59/10.62 % (1018576)Peak memory usage: 243 MB
% 38.59/10.62 % (1018576)Instructions burned: 22063 (million)
% 38.59/10.62 % (1018598)dis+21_1_sil=32000:sas=cadical:random_seed=1131651924:i=3773:amm=off_2945 on theBenchmark for (2945ds/3773Mi)
% 38.59/10.62 % TRYING [8]
% 38.59/10.62 % (1018598)Instruction limit reached!
% 38.59/10.62 % (1018598)------------------------------
% 38.59/10.62 % (1018598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.59/10.62 % (1018598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.59/10.62 % (1018598)CaDiCaL version: 2.1.3
% 38.59/10.62 % (1018598)Termination reason: Instruction limit
% 38.59/10.62 % (1018598)Termination phase: Saturation
% 38.59/10.62 % (1018598)Time elapsed: 1.087 s
% 38.59/10.62 % (1018598)Peak memory usage: 47 MB
% 38.59/10.62 % (1018598)Instructions burned: 3777 (million)
% 38.59/10.62 % (1018600)ott+11_1_sil=16000:gs=on:random_seed=1572593841:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2934 on theBenchmark for (2934ds/2251Mi)
% 38.59/10.62 % (1018596)Instruction limit reached!
% 38.59/10.62 % (1018596)------------------------------
% 38.59/10.62 % (1018596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.59/10.62 % (1018596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.59/10.62 % (1018596)CaDiCaL version: 2.1.3
% 38.59/10.62 % (1018596)Termination reason: Instruction limit
% 38.59/10.62 % (1018596)Termination phase: Saturation
% 38.59/10.62 % (1018596)Time elapsed: 1.872 s
% 38.59/10.62 % (1018596)Peak memory usage: 43 MB
% 38.59/10.62 % (1018596)Instructions burned: 3513 (million)
% 38.59/10.62 % (1018602)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2194350587:fmbsr=1.6:i=67534_2933 on theBenchmark for (2933ds/67534Mi)
% 38.59/10.62 % TRYING [7]
% 38.59/10.62 % (1018600)Instruction limit reached!
% 38.59/10.62 % (1018600)------------------------------
% 38.59/10.62 % (1018600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.59/10.62 % (1018600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.59/10.62 % (1018600)CaDiCaL version: 2.1.3
% 38.59/10.62 % (1018600)Termination reason: Instruction limit
% 38.59/10.62 % (1018600)Termination phase: Saturation
% 38.59/10.62 % (1018600)Time elapsed: 0.526 s
% 38.59/10.62 % (1018600)Peak memory usage: 16 MB
% 38.59/10.62 % (1018600)Instructions burned: 2254 (million)
% 38.59/10.62 % (1018592)Instruction limit reached!
% 38.59/10.62 % (1018592)------------------------------
% 38.59/10.62 % (1018592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.59/10.62 % (1018592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.59/10.62 % (1018592)CaDiCaL version: 2.1.3
% 38.59/10.62 % (1018592)Termination reason: Instruction limit
% 38.59/10.62 % (1018592)Termination phase: Saturation
% 38.59/10.62 % (1018592)Time elapsed: 2.803 s
% 38.59/10.62 % (1018592)Peak memory usage: 69 MB
% 38.59/10.62 % (1018592)Instructions burned: 5114 (million)
% 38.59/10.62 % (1018604)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2430338322:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2928 on theBenchmark for (2928ds/4591Mi)
% 38.59/10.62 % (1018606)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4253526562:i=29340_2928 on theBenchmark for (2928ds/29340Mi)
% 38.59/10.62 % (1018604)Instruction limit reached!
% 38.59/10.62 % (1018604)------------------------------
% 38.59/10.62 % (1018604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.59/10.62 % (1018604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.59/10.62 % (1018604)CaDiCaL version: 2.1.3
% 38.59/10.62 % (1018604)Termination reason: Instruction limit
% 38.59/10.62 % (1018604)Termination phase: Saturation
% 38.59/10.62 % (1018604)Time elapsed: 1.224 s
% 38.59/10.62 % (1018604)Peak memory usage: 47 MB
% 38.59/10.62 % (1018604)Instructions burned: 4592 (million)
% 38.59/10.62 % (1018608)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=889390214:i=5211_2916 on theBenchmark for (2916ds/5211Mi)
% 38.59/10.62 % TRYING [9]
% 38.59/10.62 % TRYING [8]
% 38.59/10.62 % TRYING [10]
% 38.59/10.62 % (1018608)Instruction limit reached!
% 38.59/10.62 % (1018608)------------------------------
% 38.59/10.62 % (1018608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.59/10.62 % (1018608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.59/10.62 % (1018608)CaDiCaL version: 2.1.3
% 38.59/10.62 % (1018608)Termination reason: Instruction limit
% 38.59/10.62 % (1018608)Termination phase: Saturation
% 38.59/10.62 % (1018608)Time elapsed: 1.281 s
% 38.59/10.62 % (1018608)Peak memory usage: 37 MB
% 38.59/10.62 % (1018608)Instructions burned: 5216 (million)
% 38.59/10.62 % (1018610)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3061111787:i=5497:nm=2_2903 on theBenchmark for (2903ds/5497Mi)
% 38.59/10.62 % TRYING [17]
% 38.59/10.62 % (1018543) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1018537-1018543"...
% 38.59/10.62 % (1018543)...printing done.
% 38.59/10.62 % (1018543)Refutation found. Thanks to Tanya!
% 38.59/10.62 % SZS status Unsatisfiable for theBenchmark
% 38.59/10.62 % SZS output start Proof for theBenchmark
% See solution above
% 38.59/10.62 % (1018543)------------------------------
% 38.59/10.62 % (1018543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.59/10.62 % (1018543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.59/10.62 % (1018543)CaDiCaL version: 2.1.3
% 38.59/10.62 % (1018543)Termination reason: Refutation
% 38.59/10.62 % (1018543)Time elapsed: 10.063 s
% 38.59/10.62 % (1018543)Peak memory usage: 168 MB
% 38.59/10.62 % (1018543)Instructions burned: 18642 (million)
% 38.59/10.62 % (1018537)Success in time 10.187 s
% 38.59/10.62 % Vampire exiting
%------------------------------------------------------------------------------