%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC298-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 : n012.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:27 PM UTC 2026
% Result : Unsatisfiable 36.11s 13.89s
% Output : Refutation 36.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 73
% Syntax : Number of formulae : 379 ( 61 unt; 28 def)
% Number of atoms : 1210 ( 191 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 1345 ( 514 ~; 803 |; 0 &)
% ( 28 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 38 ( 36 usr; 29 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 11 con; 0-2 aty)
% Number of variables : 211 ( 0 sgn 211 !; 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(f13,axiom,
! [X0] : ssList(skaf82(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause13) ).
fof(f50,axiom,
! [X0,X1] : ssList(skaf46(X0,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause50) ).
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(f59,axiom,
! [X0] :
( ~ ssList(X0)
| rearsegP(X0,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause59) ).
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(f73,axiom,
! [X0] :
( ~ ssList(X0)
| app(X0,nil) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause73) ).
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(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(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(f121,axiom,
! [X0,X1] :
( app(X0,X1) != nil
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/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(f123,axiom,
! [X0,X1] :
( app(X0,X1) != nil
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause119) ).
fof(f124,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X1 ),
inference(reorient_equations,[],[f123]) ).
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(f142,axiom,
! [X0,X1] :
( ~ rearsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| app(skaf46(X0,X1),X1) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause131) ).
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(f163,axiom,
! [X2,X0,X1] :
( app(X0,X1) != app(X2,X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| X0 = X2 ),
file('/export/starexec/sandbox/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/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(f187,axiom,
! [X2,X3,X0,X1] :
( app(app(X0,X1),X2) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| segmentP(X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause173) ).
fof(f189,axiom,
! [X2,X3,X0,X1] :
( app(X0,cons(X1,X2)) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(X3)
| memberP(X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause175) ).
fof(f193,axiom,
! [X2,X3,X0,X1,X4] :
( app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(X4)
| ~ ssList(X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(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,
ssItem(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,
ssList(sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_10) ).
fof(f210,negated_conjecture,
ssList(sk9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).
fof(f211,negated_conjecture,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_12) ).
fof(f212,plain,
sk1 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(reorient_equations,[],[f211]) ).
fof(f215,negated_conjecture,
( ssItem(sk10)
| nil = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_15) ).
fof(f220,negated_conjecture,
( cons(sk10,nil) = sk3
| nil = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_19) ).
fof(f221,plain,
( sk3 = cons(sk10,nil)
| nil = sk3 ),
inference(reorient_equations,[],[f220]) ).
fof(f222,negated_conjecture,
( memberP(sk4,sk10)
| nil = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_20) ).
fof(f224,plain,
ssList(sk3),
inference(definition_unfolding,[],[f200,f205]) ).
fof(f225,plain,
ssList(sk4),
inference(definition_unfolding,[],[f201,f204]) ).
fof(f226,plain,
sk3 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(definition_unfolding,[],[f212,f205]) ).
fof(f234,plain,
! [X0] :
( ~ ssItem(X0)
| ~ ssList(cons(X0,nil))
| singletonP(cons(X0,nil)) ),
inference(equality_resolution,[],[f119]) ).
fof(f238,plain,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| ~ ssList(app(X0,X1))
| frontsegP(app(X0,X1),X0) ),
inference(equality_resolution,[],[f155]) ).
fof(f241,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(f242,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(f244,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(f255,plain,
~ ssList(nil),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f256,plain,
! [X0] : ~ ssList(skaf82(X0)),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f279,plain,
! [X0,X1] : ~ ssList(skaf46(X0,X1)),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f281,plain,
! [X0,X1] : ~ ssList(skaf43(X0,X1)),
inference(consistent_polarity_flipping,[],[f52]) ).
fof(f282,plain,
! [X0,X1] : ~ ssList(skaf42(X0,X1)),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f287,plain,
! [X0] :
( rearsegP(X0,X0)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f59]) ).
fof(f288,plain,
! [X0] :
( ~ frontsegP(X0,nil)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f295,plain,
! [X0] :
( memberP(nil,X0)
| ~ ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f71]) ).
fof(f296,plain,
! [X0,X1] :
( ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f297,plain,
! [X0] :
( ssList(X0)
| app(X0,nil) = X0 ),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f298,plain,
! [X0] :
( ssList(X0)
| app(nil,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f299,plain,
! [X0] :
( ~ ssList(tl(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f309,plain,
! [X0,X1] :
( ~ ssList(app(X1,X0))
| ssList(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f310,plain,
! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1)
| ~ ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f320,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ssList(X1)
| tl(cons(X0,X1)) = X1 ),
inference(consistent_polarity_flipping,[],[f96]) ).
fof(f327,plain,
! [X0] :
( ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f332,plain,
! [X0] :
( ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f339,plain,
! [X0] :
( singletonP(cons(X0,nil))
| ssList(cons(X0,nil))
| ~ ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f234]) ).
fof(f340,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ssList(X1)
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f122]) ).
fof(f341,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ssList(X1)
| ssList(X0)
| nil = X1 ),
inference(consistent_polarity_flipping,[],[f124]) ).
fof(f342,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f349,plain,
! [X0,X1] :
( segmentP(X0,X1)
| segmentP(X1,X0)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f351,plain,
! [X0,X1] :
( frontsegP(X0,X1)
| frontsegP(X1,X0)
| ssList(X0)
| ssList(X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f352,plain,
! [X0,X1] :
( ~ rearsegP(X0,X1)
| ssList(X1)
| ssList(X0)
| app(skaf46(X0,X1),X1) = X0 ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f365,plain,
! [X0,X1] :
( ssList(X1)
| ssList(X0)
| ssList(app(X0,X1))
| ~ frontsegP(app(X0,X1),X0) ),
inference(consistent_polarity_flipping,[],[f238]) ).
fof(f372,plain,
! [X2,X0,X1] :
( app(X0,X1) != app(X2,X1)
| ssList(X0)
| ssList(X1)
| ssList(X2)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f381,plain,
! [X2,X0,X1] :
( ~ memberP(X1,X2)
| ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(cons(X0,X1),X2)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f389,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(f393,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,[],[f241]) ).
fof(f395,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,[],[f242]) ).
fof(f399,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,[],[f244]) ).
fof(f406,plain,
~ ssList(sk3),
inference(consistent_polarity_flipping,[],[f224]) ).
fof(f407,plain,
~ ssList(sk4),
inference(consistent_polarity_flipping,[],[f225]) ).
fof(f410,plain,
~ ssList(sk7),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f411,plain,
~ ssList(sk8),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f412,plain,
~ ssList(sk9),
inference(consistent_polarity_flipping,[],[f210]) ).
fof(f416,plain,
( ~ memberP(sk4,sk10)
| nil = sk3 ),
inference(consistent_polarity_flipping,[],[f222]) ).
fof(f425,definition,
( spl0_1
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f427,plain,
( nil = sk3
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f433,definition,
( spl0_3
<=> memberP(sk4,sk10) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f435,plain,
( ~ memberP(sk4,sk10)
| spl0_3 ),
inference(avatar_component_clause,[],[f433]) ).
fof(f436,plain,
( spl0_1
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f416,f433,f425]) ).
fof(f438,definition,
( spl0_4
<=> sk3 = cons(sk10,nil) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f440,plain,
( sk3 = cons(sk10,nil)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f441,plain,
( spl0_1
| spl0_4 ),
inference(avatar_split_clause,[],[f221,f438,f425]) ).
fof(f450,definition,
( spl0_6
<=> ssItem(sk10) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f452,plain,
( ssItem(sk10)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f450]) ).
fof(f453,plain,
( spl0_1
| spl0_6 ),
inference(avatar_split_clause,[],[f215,f450,f425]) ).
fof(f460,definition,
( spl0_8
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f461,plain,
( ~ ssList(nil)
| spl0_8 ),
inference(avatar_component_clause,[],[f460]) ).
fof(f488,definition,
( spl0_14
<=> ! [X1] : ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f489,plain,
( ! [X1] : ssItem(X1)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f491,definition,
( spl0_15
<=> ! [X0] :
( ssList(X0)
| duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f492,plain,
( ! [X0] :
( duplicatefreeP(X0)
| ssList(X0) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f491]) ).
fof(f493,plain,
( spl0_14
| spl0_15 ),
inference(avatar_split_clause,[],[f296,f491,f488]) ).
fof(f496,plain,
~ spl0_8,
inference(avatar_split_clause,[],[f255,f460]) ).
fof(f546,plain,
sk3 = app(sk3,nil),
inference(resolution,[],[f297,f406]) ).
fof(f579,plain,
sk3 = app(nil,sk3),
inference(resolution,[],[f298,f406]) ).
fof(f583,plain,
sk9 = app(nil,sk9),
inference(resolution,[],[f298,f412]) ).
fof(f630,plain,
( ! [X0,X1] :
( ssList(X1)
| tl(cons(X0,X1)) = X1 )
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f320,f489]) ).
fof(f632,plain,
( ! [X0,X1] : skaf82(X1) = tl(cons(X0,skaf82(X1)))
| ~ spl0_14 ),
inference(resolution,[],[f630,f256]) ).
fof(f777,definition,
( spl0_16
<=> nil = sk9 ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f778,plain,
( nil != sk9
| spl0_16 ),
inference(avatar_component_clause,[],[f777]) ).
fof(f779,plain,
( nil = sk9
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f777]) ).
fof(f781,definition,
( spl0_17
<=> sk9 = cons(hd(sk9),tl(sk9)) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f783,plain,
( sk9 = cons(hd(sk9),tl(sk9))
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f781]) ).
fof(f865,definition,
( spl0_24
<=> sk9 = cons(skaf83(sk9),skaf82(sk9)) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f867,plain,
( sk9 = cons(skaf83(sk9),skaf82(sk9))
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f865]) ).
fof(f880,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,[],[f340,f226]) ).
fof(f886,plain,
( 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))
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f880,f427]) ).
fof(f887,plain,
( ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f886,f412]) ).
fof(f889,definition,
( spl0_27
<=> nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f890,plain,
( nil != app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| spl0_27 ),
inference(avatar_component_clause,[],[f889]) ).
fof(f891,plain,
( nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f889]) ).
fof(f893,definition,
( spl0_28
<=> ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f894,plain,
( ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| spl0_28 ),
inference(avatar_component_clause,[],[f893]) ).
fof(f895,plain,
( ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f893]) ).
fof(f913,plain,
( spl0_27
| spl0_28
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f887,f425,f893,f889]) ).
fof(f962,definition,
( spl0_33
<=> ssList(cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f963,plain,
( ~ ssList(cons(sk6,nil))
| spl0_33 ),
inference(avatar_component_clause,[],[f962]) ).
fof(f964,plain,
( ssList(cons(sk6,nil))
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f962]) ).
fof(f1183,plain,
( ! [X0] :
( ssList(X0)
| cons(sk10,X0) = app(cons(sk10,nil),X0) )
| ~ spl0_6 ),
inference(resolution,[],[f342,f452]) ).
fof(f1184,plain,
( ! [X0] :
( ssList(X0)
| cons(sk10,X0) = app(sk3,X0) )
| ~ spl0_4
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1183,f440]) ).
fof(f1341,plain,
! [X0,X1] :
( ~ frontsegP(app(X0,X1),X0)
| ssList(X0)
| ssList(X1) ),
inference(forward_subsumption_resolution,[],[f365,f309]) ).
fof(f1343,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| frontsegP(X0,app(X0,X1))
| ssList(app(X0,X1))
| ssList(X0)
| app(X0,X1) = X0 ),
inference(resolution,[],[f1341,f351]) ).
fof(f1357,plain,
! [X0,X1] :
( ssList(X0)
| ssList(X1)
| frontsegP(X0,app(X0,X1))
| ssList(app(X0,X1))
| app(X0,X1) = X0 ),
inference(duplicate_literal_removal,[],[f1343]) ).
fof(f1360,plain,
! [X0,X1] :
( frontsegP(X0,app(X0,X1))
| ssList(X1)
| ssList(X0)
| app(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f1357,f309]) ).
fof(f1451,plain,
! [X0] :
( ssList(X0)
| ssList(X0)
| app(skaf46(X0,X0),X0) = X0
| ssList(X0) ),
inference(resolution,[],[f352,f287]) ).
fof(f1454,plain,
! [X0] :
( ssList(X0)
| app(skaf46(X0,X0),X0) = X0 ),
inference(duplicate_literal_removal,[],[f1451]) ).
fof(f1990,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,[],[f372,f226]) ).
fof(f1997,plain,
! [X0] :
( sk3 != app(X0,sk3)
| ssList(X0)
| ssList(sk3)
| ssList(nil)
| nil = X0 ),
inference(superposition,[],[f372,f579]) ).
fof(f2002,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,[],[f372,f226]) ).
fof(f2017,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,[],[f2002,f412]) ).
fof(f2022,plain,
! [X0] :
( sk3 != app(X0,sk3)
| ssList(X0)
| ssList(nil)
| nil = X0 ),
inference(forward_subsumption_resolution,[],[f1997,f406]) ).
fof(f2028,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,[],[f1990,f412]) ).
fof(f2044,plain,
( ! [X0] :
( sk3 != app(X0,sk3)
| ssList(X0)
| nil = X0 )
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f2022,f461]) ).
fof(f2279,plain,
! [X0,X1] :
( ssList(nil)
| ~ ssItem(X0)
| ~ ssItem(X1)
| memberP(cons(X0,nil),X1)
| X0 = X1
| ~ ssItem(X1) ),
inference(resolution,[],[f381,f295]) ).
fof(f2282,plain,
! [X0,X1] :
( ssList(nil)
| ~ ssItem(X0)
| ~ ssItem(X1)
| memberP(cons(X0,nil),X1)
| X0 = X1 ),
inference(duplicate_literal_removal,[],[f2279]) ).
fof(f2285,plain,
( ! [X0,X1] :
( memberP(cons(X0,nil),X1)
| ~ ssItem(X1)
| ~ ssItem(X0)
| X0 = X1 )
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f2282,f461]) ).
fof(f2479,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,[],[f393,f226]) ).
fof(f2491,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,[],[f2479,f412]) ).
fof(f2539,plain,
( ! [X2,X3,X0,X1] :
( ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(X2)
| ssList(X0)
| ~ ssItem(X1)
| ssList(X3) )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f399,f492]) ).
fof(f3541,definition,
( spl0_123
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f3542,plain,
( ~ ssList(cons(sk5,nil))
| spl0_123 ),
inference(avatar_component_clause,[],[f3541]) ).
fof(f3543,plain,
( ssList(cons(sk5,nil))
| ~ spl0_123 ),
inference(avatar_component_clause,[],[f3541]) ).
fof(f5155,definition,
( spl0_130
<=> sk6 = sk10 ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f5156,plain,
( sk6 != sk10
| spl0_130 ),
inference(avatar_component_clause,[],[f5155]) ).
fof(f5157,plain,
( sk6 = sk10
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f5155]) ).
fof(f7220,plain,
sk3 = app(skaf46(sk3,sk3),sk3),
inference(resolution,[],[f1454,f406]) ).
fof(f11670,definition,
( spl0_153
<=> nil = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f11671,plain,
( nil != cons(sk5,nil)
| spl0_153 ),
inference(avatar_component_clause,[],[f11670]) ).
fof(f11672,plain,
( nil = cons(sk5,nil)
| ~ spl0_153 ),
inference(avatar_component_clause,[],[f11670]) ).
fof(f11712,plain,
( singletonP(nil)
| ssList(nil)
| ~ ssItem(sk5)
| ~ spl0_153 ),
inference(superposition,[],[f339,f11672]) ).
fof(f11756,plain,
( ssList(nil)
| ~ ssItem(sk5)
| ~ spl0_153 ),
inference(forward_subsumption_resolution,[],[f11712,f11]) ).
fof(f11777,plain,
( ~ ssItem(sk5)
| spl0_8
| ~ spl0_153 ),
inference(forward_subsumption_resolution,[],[f11756,f461]) ).
fof(f11784,plain,
( $false
| spl0_8
| ~ spl0_153 ),
inference(forward_subsumption_resolution,[],[f11777,f206]) ).
fof(f11785,plain,
( spl0_8
| ~ spl0_153 ),
inference(avatar_contradiction_clause,[],[f11784]) ).
fof(f13261,definition,
( spl0_161
<=> nil = cons(sk6,nil) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f13262,plain,
( nil != cons(sk6,nil)
| spl0_161 ),
inference(avatar_component_clause,[],[f13261]) ).
fof(f13263,plain,
( nil = cons(sk6,nil)
| ~ spl0_161 ),
inference(avatar_component_clause,[],[f13261]) ).
fof(f13389,plain,
( ssList(nil)
| ~ ssItem(sk6)
| ~ spl0_33 ),
inference(resolution,[],[f964,f310]) ).
fof(f13390,plain,
( ~ ssItem(sk6)
| spl0_8
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f13389,f461]) ).
fof(f13391,plain,
( $false
| spl0_8
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f13390,f207]) ).
fof(f13392,plain,
( spl0_8
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f13391]) ).
fof(f13741,plain,
( singletonP(nil)
| ssList(nil)
| ~ ssItem(sk6)
| ~ spl0_161 ),
inference(superposition,[],[f339,f13263]) ).
fof(f13785,plain,
( ssList(nil)
| ~ ssItem(sk6)
| ~ spl0_161 ),
inference(forward_subsumption_resolution,[],[f13741,f11]) ).
fof(f13804,plain,
( ~ ssItem(sk6)
| spl0_8
| ~ spl0_161 ),
inference(forward_subsumption_resolution,[],[f13785,f461]) ).
fof(f13809,plain,
( $false
| spl0_8
| ~ spl0_161 ),
inference(forward_subsumption_resolution,[],[f13804,f207]) ).
fof(f13810,plain,
( spl0_8
| ~ spl0_161 ),
inference(avatar_contradiction_clause,[],[f13809]) ).
fof(f34029,plain,
( ssList(nil)
| ~ ssItem(sk5)
| ~ spl0_123 ),
inference(resolution,[],[f3543,f310]) ).
fof(f34030,plain,
( ~ ssItem(sk5)
| spl0_8
| ~ spl0_123 ),
inference(forward_subsumption_resolution,[],[f34029,f461]) ).
fof(f34031,plain,
( $false
| spl0_8
| ~ spl0_123 ),
inference(forward_subsumption_resolution,[],[f34030,f206]) ).
fof(f34032,plain,
( spl0_8
| ~ spl0_123 ),
inference(avatar_contradiction_clause,[],[f34031]) ).
fof(f46238,plain,
( ! [X2,X0,X1] :
( ~ memberP(app(X0,cons(X1,X2)),X1)
| ssList(X0)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2) )
| ~ spl0_14 ),
inference(backward_subsumption_resolution,[],[f395,f489]) ).
fof(f46338,plain,
( ! [X0,X1] :
( memberP(cons(X0,nil),X1)
| ~ ssItem(X1)
| X0 = X1 )
| spl0_8
| ~ spl0_14 ),
inference(backward_subsumption_resolution,[],[f2285,f489]) ).
fof(f46396,plain,
( ! [X0,X1] :
( memberP(cons(X0,nil),X1)
| X0 = X1 )
| spl0_8
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f46338,f489]) ).
fof(f50371,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_16 ),
inference(forward_demodulation,[],[f2028,f779]) ).
fof(f54635,plain,
( ~ ssItem(sk10)
| ssList(sk4)
| sk4 = app(skaf42(sk4,sk10),cons(sk10,skaf43(sk10,sk4)))
| spl0_3 ),
inference(resolution,[],[f389,f435]) ).
fof(f54644,plain,
( ssList(sk4)
| sk4 = app(skaf42(sk4,sk10),cons(sk10,skaf43(sk10,sk4)))
| spl0_3
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f54635,f452]) ).
fof(f54651,plain,
( sk4 = app(skaf42(sk4,sk10),cons(sk10,skaf43(sk10,sk4)))
| spl0_3
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f54644,f407]) ).
fof(f55321,plain,
( ! [X0,X1] :
( ssList(app(app(X0,cons(sk10,X1)),sk3))
| ssList(X1)
| ssList(X0)
| ~ ssItem(sk10)
| ssList(nil) )
| ~ spl0_4
| ~ spl0_15 ),
inference(superposition,[],[f2539,f440]) ).
fof(f55322,plain,
( ! [X0,X1] :
( ssList(app(app(X0,cons(sk10,X1)),sk3))
| ssList(X1)
| ssList(X0)
| ssList(nil) )
| ~ spl0_4
| ~ spl0_6
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f55321,f452]) ).
fof(f55347,plain,
( ! [X0,X1] :
( ssList(app(app(X0,cons(sk10,X1)),sk3))
| ssList(X1)
| ssList(X0) )
| ~ spl0_4
| ~ spl0_6
| spl0_8
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f55322,f461]) ).
fof(f56803,plain,
( ! [X0] : cons(sk10,skaf82(X0)) = app(sk3,skaf82(X0))
| ~ spl0_4
| ~ spl0_6 ),
inference(resolution,[],[f1184,f256]) ).
fof(f58536,plain,
( ssList(app(sk4,sk3))
| ssList(skaf43(sk10,sk4))
| ssList(skaf42(sk4,sk10))
| spl0_3
| ~ spl0_4
| ~ spl0_6
| spl0_8
| ~ spl0_15 ),
inference(superposition,[],[f55347,f54651]) ).
fof(f58537,plain,
( ssList(app(sk4,sk3))
| ssList(skaf42(sk4,sk10))
| spl0_3
| ~ spl0_4
| ~ spl0_6
| spl0_8
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f58536,f281]) ).
fof(f58540,plain,
( ssList(app(sk4,sk3))
| spl0_3
| ~ spl0_4
| ~ spl0_6
| spl0_8
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f58537,f282]) ).
fof(f58721,plain,
( ssList(sk4)
| ssList(sk3)
| spl0_3
| ~ spl0_4
| ~ spl0_6
| spl0_8
| ~ spl0_15 ),
inference(resolution,[],[f58540,f309]) ).
fof(f58722,plain,
( ssList(sk3)
| spl0_3
| ~ spl0_4
| ~ spl0_6
| spl0_8
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f58721,f407]) ).
fof(f58723,plain,
( $false
| spl0_3
| ~ spl0_4
| ~ spl0_6
| spl0_8
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f58722,f406]) ).
fof(f58724,plain,
( spl0_3
| ~ spl0_4
| ~ spl0_6
| spl0_8
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f58723]) ).
fof(f70220,definition,
( spl0_1493
<=> ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_1493])],[avatar_definition]) ).
fof(f70221,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| spl0_1493 ),
inference(avatar_component_clause,[],[f70220]) ).
fof(f70222,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_1493 ),
inference(avatar_component_clause,[],[f70220]) ).
fof(f70241,definition,
( spl0_1495
<=> sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_1495])],[avatar_definition]) ).
fof(f70243,plain,
( sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ spl0_1495 ),
inference(avatar_component_clause,[],[f70241]) ).
fof(f70258,definition,
( spl0_1498
<=> ! [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_1498])],[avatar_definition]) ).
fof(f70259,plain,
( ! [X0] :
( app(X0,nil) != sk3
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0
| ssList(X0) )
| ~ spl0_1498 ),
inference(avatar_component_clause,[],[f70258]) ).
fof(f70266,plain,
( spl0_28
| spl0_1498
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f50371,f777,f70258,f893]) ).
fof(f72425,definition,
( spl0_1563
<=> ssList(app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_1563])],[avatar_definition]) ).
fof(f72426,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| spl0_1563 ),
inference(avatar_component_clause,[],[f72425]) ).
fof(f72427,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_1563 ),
inference(avatar_component_clause,[],[f72425]) ).
fof(f107592,plain,
( ! [X0] :
( memberP(sk3,X0)
| sk10 = X0 )
| ~ spl0_4
| spl0_8
| ~ spl0_14 ),
inference(superposition,[],[f46396,f440]) ).
fof(f122830,plain,
! [X0] :
( ~ segmentP(app(sk3,X0),sk3)
| ssList(skaf46(sk3,sk3))
| ssList(sk3)
| ssList(app(sk3,X0))
| ssList(X0) ),
inference(superposition,[],[f393,f7220]) ).
fof(f122852,plain,
! [X0] :
( ~ segmentP(app(sk3,X0),sk3)
| ssList(skaf46(sk3,sk3))
| ssList(sk3)
| ssList(X0) ),
inference(forward_subsumption_resolution,[],[f122830,f309]) ).
fof(f122870,plain,
! [X0] :
( ~ segmentP(app(sk3,X0),sk3)
| ssList(sk3)
| ssList(X0) ),
inference(forward_subsumption_resolution,[],[f122852,f279]) ).
fof(f122890,plain,
! [X0] :
( ~ segmentP(app(sk3,X0),sk3)
| ssList(X0) ),
inference(forward_subsumption_resolution,[],[f122870,f406]) ).
fof(f162737,plain,
( ! [X0] :
( ~ segmentP(cons(sk10,skaf82(X0)),sk3)
| ssList(skaf82(X0)) )
| ~ spl0_4
| ~ spl0_6 ),
inference(superposition,[],[f122890,f56803]) ).
fof(f162783,plain,
( ! [X0] : ~ segmentP(cons(sk10,skaf82(X0)),sk3)
| ~ spl0_4
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f162737,f256]) ).
fof(f169171,definition,
( spl0_4963
<=> nil = app(sk7,cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_4963])],[avatar_definition]) ).
fof(f169172,plain,
( nil != app(sk7,cons(sk5,nil))
| spl0_4963 ),
inference(avatar_component_clause,[],[f169171]) ).
fof(f169173,plain,
( nil = app(sk7,cons(sk5,nil))
| ~ spl0_4963 ),
inference(avatar_component_clause,[],[f169171]) ).
fof(f169203,plain,
( ssList(sk7)
| ssList(cons(sk5,nil))
| ~ spl0_1563 ),
inference(resolution,[],[f72427,f309]) ).
fof(f169204,plain,
( ssList(cons(sk5,nil))
| ~ spl0_1563 ),
inference(forward_subsumption_resolution,[],[f169203,f410]) ).
fof(f169205,plain,
( $false
| spl0_123
| ~ spl0_1563 ),
inference(forward_subsumption_resolution,[],[f169204,f3542]) ).
fof(f169206,plain,
( spl0_123
| ~ spl0_1563 ),
inference(avatar_contradiction_clause,[],[f169205]) ).
fof(f217209,plain,
( nil != nil
| ssList(cons(sk5,nil))
| ssList(sk7)
| nil = cons(sk5,nil)
| ~ spl0_4963 ),
inference(superposition,[],[f341,f169173]) ).
fof(f217231,plain,
( ssList(cons(sk5,nil))
| ssList(sk7)
| nil = cons(sk5,nil)
| ~ spl0_4963 ),
inference(trivial_inequality_removal,[],[f217209]) ).
fof(f217255,plain,
( ssList(sk7)
| nil = cons(sk5,nil)
| spl0_123
| ~ spl0_4963 ),
inference(forward_subsumption_resolution,[],[f217231,f3542]) ).
fof(f217306,plain,
( nil = cons(sk5,nil)
| spl0_123
| ~ spl0_4963 ),
inference(forward_subsumption_resolution,[],[f217255,f410]) ).
fof(f217336,plain,
( $false
| spl0_123
| spl0_153
| ~ spl0_4963 ),
inference(forward_subsumption_resolution,[],[f217306,f11671]) ).
fof(f217337,plain,
( spl0_123
| spl0_153
| ~ spl0_4963 ),
inference(avatar_contradiction_clause,[],[f217336]) ).
fof(f261741,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ssList(cons(sk6,nil))
| ~ spl0_28 ),
inference(resolution,[],[f895,f309]) ).
fof(f261742,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_28
| spl0_33 ),
inference(forward_subsumption_resolution,[],[f261741,f963]) ).
fof(f261743,plain,
( spl0_1493
| ~ spl0_28
| spl0_33 ),
inference(avatar_split_clause,[],[f261742,f962,f893,f70220]) ).
fof(f263620,plain,
( sk3 != sk3
| sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ssList(sk3)
| ~ spl0_1498 ),
inference(superposition,[],[f70259,f546]) ).
fof(f263625,plain,
( sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ssList(sk3)
| ~ spl0_1498 ),
inference(trivial_inequality_removal,[],[f263620]) ).
fof(f263628,plain,
( sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| ~ spl0_1498 ),
inference(forward_subsumption_resolution,[],[f263625,f406]) ).
fof(f263661,plain,
( spl0_1495
| ~ spl0_1498 ),
inference(avatar_split_clause,[],[f263628,f70258,f70241]) ).
fof(f267776,plain,
( ssList(app(sk7,cons(sk5,nil)))
| ssList(sk8)
| ~ spl0_1493 ),
inference(resolution,[],[f70222,f309]) ).
fof(f267777,plain,
( ssList(sk8)
| ~ spl0_1493
| spl0_1563 ),
inference(forward_subsumption_resolution,[],[f267776,f72426]) ).
fof(f267778,plain,
( $false
| ~ spl0_1493
| spl0_1563 ),
inference(forward_subsumption_resolution,[],[f267777,f411]) ).
fof(f267779,plain,
( ~ spl0_1493
| spl0_1563 ),
inference(avatar_contradiction_clause,[],[f267778]) ).
fof(f268951,plain,
( nil != nil
| ssList(cons(sk6,nil))
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = cons(sk6,nil)
| ~ spl0_27 ),
inference(superposition,[],[f341,f891]) ).
fof(f268973,plain,
( ssList(cons(sk6,nil))
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = cons(sk6,nil)
| ~ spl0_27 ),
inference(trivial_inequality_removal,[],[f268951]) ).
fof(f268997,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = cons(sk6,nil)
| ~ spl0_27
| spl0_33 ),
inference(forward_subsumption_resolution,[],[f268973,f963]) ).
fof(f269072,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ spl0_27
| spl0_33
| spl0_161 ),
inference(forward_subsumption_resolution,[],[f268997,f13262]) ).
fof(f269074,definition,
( spl0_9018
<=> nil = app(app(sk7,cons(sk5,nil)),sk8) ),
introduced(definition,[new_symbols(definition,[spl0_9018])],[avatar_definition]) ).
fof(f269075,plain,
( nil != app(app(sk7,cons(sk5,nil)),sk8)
| spl0_9018 ),
inference(avatar_component_clause,[],[f269074]) ).
fof(f269076,plain,
( nil = app(app(sk7,cons(sk5,nil)),sk8)
| ~ spl0_9018 ),
inference(avatar_component_clause,[],[f269074]) ).
fof(f269150,plain,
( spl0_1493
| ~ spl0_27
| spl0_33
| spl0_161 ),
inference(avatar_split_clause,[],[f269072,f13261,f962,f889,f70220]) ).
fof(f274702,plain,
( frontsegP(app(sk7,cons(sk5,nil)),nil)
| ssList(sk8)
| ssList(app(sk7,cons(sk5,nil)))
| nil = app(sk7,cons(sk5,nil))
| ~ spl0_9018 ),
inference(superposition,[],[f1360,f269076]) ).
fof(f274724,plain,
( ssList(sk8)
| ssList(app(sk7,cons(sk5,nil)))
| nil = app(sk7,cons(sk5,nil))
| ~ spl0_9018 ),
inference(forward_subsumption_resolution,[],[f274702,f288]) ).
fof(f274753,plain,
( ssList(app(sk7,cons(sk5,nil)))
| nil = app(sk7,cons(sk5,nil))
| ~ spl0_9018 ),
inference(forward_subsumption_resolution,[],[f274724,f411]) ).
fof(f274776,plain,
( nil = app(sk7,cons(sk5,nil))
| spl0_1563
| ~ spl0_9018 ),
inference(forward_subsumption_resolution,[],[f274753,f72426]) ).
fof(f274793,plain,
( $false
| spl0_1563
| spl0_4963
| ~ spl0_9018 ),
inference(forward_subsumption_resolution,[],[f274776,f169172]) ).
fof(f274794,plain,
( spl0_1563
| spl0_4963
| ~ spl0_9018 ),
inference(avatar_contradiction_clause,[],[f274793]) ).
fof(f320936,plain,
( sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk10,nil))
| ~ spl0_130
| ~ spl0_1495 ),
inference(forward_demodulation,[],[f70243,f5157]) ).
fof(f320937,plain,
( sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),sk3)
| ~ spl0_4
| ~ spl0_130
| ~ spl0_1495 ),
inference(forward_demodulation,[],[f320936,f440]) ).
fof(f360243,plain,
( sk3 != sk3
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = app(app(sk7,cons(sk5,nil)),sk8)
| ~ spl0_4
| spl0_8
| ~ spl0_130
| ~ spl0_1495 ),
inference(superposition,[],[f2044,f320937]) ).
fof(f360272,plain,
( ssList(app(app(sk7,cons(sk5,nil)),sk8))
| nil = app(app(sk7,cons(sk5,nil)),sk8)
| ~ spl0_4
| spl0_8
| ~ spl0_130
| ~ spl0_1495 ),
inference(trivial_inequality_removal,[],[f360243]) ).
fof(f360293,plain,
( nil = app(app(sk7,cons(sk5,nil)),sk8)
| ~ spl0_4
| spl0_8
| ~ spl0_130
| spl0_1493
| ~ spl0_1495 ),
inference(forward_subsumption_resolution,[],[f360272,f70221]) ).
fof(f360312,plain,
( $false
| ~ spl0_4
| spl0_8
| ~ spl0_130
| spl0_1493
| ~ spl0_1495
| spl0_9018 ),
inference(forward_subsumption_resolution,[],[f360293,f269075]) ).
fof(f360313,plain,
( ~ spl0_4
| spl0_8
| ~ spl0_130
| spl0_1493
| ~ spl0_1495
| spl0_9018 ),
inference(avatar_contradiction_clause,[],[f360312]) ).
fof(f366595,plain,
( ~ memberP(sk3,sk6)
| ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ssList(sk3)
| ssList(nil)
| ~ spl0_14
| ~ spl0_1495 ),
inference(superposition,[],[f46238,f70243]) ).
fof(f366667,plain,
( ~ memberP(sk3,sk6)
| ssList(sk3)
| ssList(nil)
| ~ spl0_14
| spl0_1493
| ~ spl0_1495 ),
inference(forward_subsumption_resolution,[],[f366595,f70221]) ).
fof(f366708,plain,
( ~ memberP(sk3,sk6)
| ssList(nil)
| ~ spl0_14
| spl0_1493
| ~ spl0_1495 ),
inference(forward_subsumption_resolution,[],[f366667,f406]) ).
fof(f366721,plain,
( ~ memberP(sk3,sk6)
| spl0_8
| ~ spl0_14
| spl0_1493
| ~ spl0_1495 ),
inference(forward_subsumption_resolution,[],[f366708,f461]) ).
fof(f368133,plain,
( sk6 = sk10
| ~ spl0_4
| spl0_8
| ~ spl0_14
| spl0_1493
| ~ spl0_1495 ),
inference(resolution,[],[f366721,f107592]) ).
fof(f368142,plain,
( $false
| ~ spl0_4
| spl0_8
| ~ spl0_14
| spl0_130
| spl0_1493
| ~ spl0_1495 ),
inference(forward_subsumption_resolution,[],[f368133,f5156]) ).
fof(f368143,plain,
( ~ spl0_4
| spl0_8
| ~ spl0_14
| spl0_130
| spl0_1493
| ~ spl0_1495 ),
inference(avatar_contradiction_clause,[],[f368142]) ).
fof(f368145,plain,
( ! [X0] :
( sk3 != app(X0,sk9)
| ssList(X0)
| app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)) = X0 )
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f2017,f894]) ).
fof(f368147,plain,
( ! [X0] :
( ~ segmentP(app(sk3,X0),sk9)
| ssList(app(sk3,X0))
| ssList(X0) )
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f2491,f894]) ).
fof(f368224,definition,
( spl0_11649
<=> ssList(sk9) ),
introduced(definition,[new_symbols(definition,[spl0_11649])],[avatar_definition]) ).
fof(f368225,plain,
( ~ ssList(sk9)
| spl0_11649 ),
inference(avatar_component_clause,[],[f368224]) ).
fof(f368324,definition,
( spl0_11650
<=> sk3 = sk9 ),
introduced(definition,[new_symbols(definition,[spl0_11650])],[avatar_definition]) ).
fof(f368325,plain,
( sk3 != sk9
| spl0_11650 ),
inference(avatar_component_clause,[],[f368324]) ).
fof(f368415,plain,
~ spl0_11649,
inference(avatar_split_clause,[],[f412,f368224]) ).
fof(f368418,plain,
( sk9 = cons(hd(sk9),tl(sk9))
| nil = sk9
| spl0_11649 ),
inference(resolution,[],[f368225,f327]) ).
fof(f368419,plain,
( sk9 = cons(skaf83(sk9),skaf82(sk9))
| nil = sk9
| spl0_11649 ),
inference(resolution,[],[f368225,f332]) ).
fof(f369287,plain,
( spl0_16
| spl0_24
| spl0_11649 ),
inference(avatar_split_clause,[],[f368419,f368224,f865,f777]) ).
fof(f369288,plain,
( spl0_16
| spl0_17
| spl0_11649 ),
inference(avatar_split_clause,[],[f368418,f368224,f781,f777]) ).
fof(f369535,definition,
( spl0_11672
<=> sk10 = hd(sk9) ),
introduced(definition,[new_symbols(definition,[spl0_11672])],[avatar_definition]) ).
fof(f369537,plain,
( sk10 = hd(sk9)
| ~ spl0_11672 ),
inference(avatar_component_clause,[],[f369535]) ).
fof(f369632,plain,
( tl(sk9) = skaf82(sk9)
| ~ spl0_14
| ~ spl0_24 ),
inference(superposition,[],[f632,f867]) ).
fof(f370371,plain,
( ~ segmentP(sk3,sk9)
| ssList(sk3)
| ssList(nil)
| spl0_28 ),
inference(superposition,[],[f368147,f546]) ).
fof(f370447,plain,
( ~ segmentP(sk3,sk9)
| ssList(nil)
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f370371,f406]) ).
fof(f370489,plain,
( ~ segmentP(sk3,sk9)
| spl0_8
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f370447,f461]) ).
fof(f372659,plain,
( sk3 != sk9
| ssList(nil)
| nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| spl0_28 ),
inference(superposition,[],[f368145,f583]) ).
fof(f372661,plain,
( sk3 != sk9
| nil = app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))
| spl0_8
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f372659,f461]) ).
fof(f372662,plain,
( sk3 != sk9
| spl0_8
| spl0_27
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f372661,f890]) ).
fof(f372663,plain,
( ~ spl0_11650
| spl0_8
| spl0_27
| spl0_28 ),
inference(avatar_split_clause,[],[f372662,f893,f889,f460,f368324]) ).
fof(f372680,plain,
( ! [X0] :
( ~ memberP(app(X0,sk9),hd(sk9))
| ssList(X0)
| ssList(app(X0,sk9))
| ssList(tl(sk9)) )
| ~ spl0_14
| ~ spl0_17 ),
inference(superposition,[],[f46238,f783]) ).
fof(f372749,definition,
( spl0_11731
<=> ssList(tl(sk9)) ),
introduced(definition,[new_symbols(definition,[spl0_11731])],[avatar_definition]) ).
fof(f372751,plain,
( ssList(tl(sk9))
| ~ spl0_11731 ),
inference(avatar_component_clause,[],[f372749]) ).
fof(f372957,definition,
( spl0_11777
<=> ! [X0] :
( ~ memberP(app(X0,sk9),hd(sk9))
| ssList(app(X0,sk9))
| ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_11777])],[avatar_definition]) ).
fof(f372958,plain,
( ! [X0] :
( ~ memberP(app(X0,sk9),hd(sk9))
| ssList(app(X0,sk9))
| ssList(X0) )
| ~ spl0_11777 ),
inference(avatar_component_clause,[],[f372957]) ).
fof(f372959,plain,
( spl0_11731
| spl0_11777
| ~ spl0_14
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f372680,f781,f488,f372957,f372749]) ).
fof(f373514,plain,
( ssList(sk9)
| nil = sk9
| ~ spl0_11731 ),
inference(resolution,[],[f372751,f299]) ).
fof(f373515,plain,
( nil = sk9
| spl0_11649
| ~ spl0_11731 ),
inference(forward_subsumption_resolution,[],[f373514,f368225]) ).
fof(f373516,plain,
( $false
| spl0_16
| spl0_11649
| ~ spl0_11731 ),
inference(forward_subsumption_resolution,[],[f373515,f778]) ).
fof(f373517,plain,
( spl0_16
| spl0_11649
| ~ spl0_11731 ),
inference(avatar_contradiction_clause,[],[f373516]) ).
fof(f374479,plain,
( sk9 = cons(sk10,tl(sk9))
| ~ spl0_17
| ~ spl0_11672 ),
inference(superposition,[],[f783,f369537]) ).
fof(f374577,plain,
( ~ segmentP(cons(sk10,tl(sk9)),sk3)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_14
| ~ spl0_24 ),
inference(superposition,[],[f162783,f369632]) ).
fof(f397566,plain,
( ~ memberP(sk3,hd(sk9))
| ssList(sk3)
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ spl0_11777 ),
inference(superposition,[],[f372958,f226]) ).
fof(f397571,plain,
( ~ memberP(sk3,hd(sk9))
| ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ spl0_11777 ),
inference(forward_subsumption_resolution,[],[f397566,f406]) ).
fof(f397577,plain,
( ~ memberP(sk3,hd(sk9))
| spl0_28
| ~ spl0_11777 ),
inference(forward_subsumption_resolution,[],[f397571,f894]) ).
fof(f397606,plain,
( sk10 = hd(sk9)
| ~ spl0_4
| spl0_8
| ~ spl0_14
| spl0_28
| ~ spl0_11777 ),
inference(resolution,[],[f397577,f107592]) ).
fof(f397929,plain,
( spl0_11672
| ~ spl0_4
| spl0_8
| ~ spl0_14
| spl0_28
| ~ spl0_11777 ),
inference(avatar_split_clause,[],[f397606,f372957,f893,f488,f460,f438,f369535]) ).
fof(f788836,plain,
( ~ segmentP(sk9,sk3)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_14
| ~ spl0_17
| ~ spl0_24
| ~ spl0_11672 ),
inference(forward_demodulation,[],[f374577,f374479]) ).
fof(f802910,plain,
( segmentP(sk3,sk9)
| ssList(sk9)
| ssList(sk3)
| sk3 = sk9
| ~ spl0_4
| ~ spl0_6
| ~ spl0_14
| ~ spl0_17
| ~ spl0_24
| ~ spl0_11672 ),
inference(resolution,[],[f788836,f349]) ).
fof(f802927,plain,
( ssList(sk9)
| ssList(sk3)
| sk3 = sk9
| ~ spl0_4
| ~ spl0_6
| spl0_8
| ~ spl0_14
| ~ spl0_17
| ~ spl0_24
| spl0_28
| ~ spl0_11672 ),
inference(forward_subsumption_resolution,[],[f802910,f370489]) ).
fof(f802936,plain,
( ssList(sk3)
| sk3 = sk9
| ~ spl0_4
| ~ spl0_6
| spl0_8
| ~ spl0_14
| ~ spl0_17
| ~ spl0_24
| spl0_28
| spl0_11649
| ~ spl0_11672 ),
inference(forward_subsumption_resolution,[],[f802927,f368225]) ).
fof(f802940,plain,
( sk3 = sk9
| ~ spl0_4
| ~ spl0_6
| spl0_8
| ~ spl0_14
| ~ spl0_17
| ~ spl0_24
| spl0_28
| spl0_11649
| ~ spl0_11672 ),
inference(forward_subsumption_resolution,[],[f802936,f406]) ).
fof(f802943,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| spl0_8
| ~ spl0_14
| ~ spl0_17
| ~ spl0_24
| spl0_28
| spl0_11649
| spl0_11650
| ~ spl0_11672 ),
inference(forward_subsumption_resolution,[],[f802940,f368325]) ).
fof(f802944,plain,
( ~ spl0_4
| ~ spl0_6
| spl0_8
| ~ spl0_14
| ~ spl0_17
| ~ spl0_24
| spl0_28
| spl0_11649
| spl0_11650
| ~ spl0_11672 ),
inference(avatar_contradiction_clause,[],[f802943]) ).
cnf(s2,plain,
( spl0_1
| ~ spl0_3 ),
inference(sat_conversion,[],[f436]) ).
cnf(s3,plain,
( spl0_1
| spl0_4 ),
inference(sat_conversion,[],[f441]) ).
cnf(s7,plain,
( spl0_1
| spl0_6 ),
inference(sat_conversion,[],[f453]) ).
cnf(s15,plain,
( spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f493]) ).
cnf(s18,plain,
~ spl0_8,
inference(sat_conversion,[],[f496]) ).
cnf(s37,plain,
( ~ spl0_1
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f913]) ).
cnf(s264,plain,
( spl0_8
| ~ spl0_153 ),
inference(sat_conversion,[],[f11785]) ).
cnf(s273,plain,
( spl0_8
| ~ spl0_33 ),
inference(sat_conversion,[],[f13392]) ).
cnf(s304,plain,
( spl0_8
| ~ spl0_161 ),
inference(sat_conversion,[],[f13810]) ).
cnf(s590,plain,
( spl0_8
| ~ spl0_123 ),
inference(sat_conversion,[],[f34032]) ).
cnf(s2053,plain,
( spl0_3
| ~ spl0_4
| ~ spl0_6
| spl0_8
| ~ spl0_15 ),
inference(sat_conversion,[],[f58724]) ).
cnf(s2641,plain,
( ~ spl0_16
| spl0_28
| spl0_1498 ),
inference(sat_conversion,[],[f70266]) ).
cnf(s9061,plain,
( spl0_123
| ~ spl0_1563 ),
inference(sat_conversion,[],[f169206]) ).
cnf(s14258,plain,
( spl0_123
| spl0_153
| ~ spl0_4963 ),
inference(sat_conversion,[],[f217337]) ).
cnf(s15977,plain,
( ~ spl0_28
| spl0_33
| spl0_1493 ),
inference(sat_conversion,[],[f261743]) ).
cnf(s15998,plain,
( spl0_1495
| ~ spl0_1498 ),
inference(sat_conversion,[],[f263661]) ).
cnf(s16299,plain,
( ~ spl0_1493
| spl0_1563 ),
inference(sat_conversion,[],[f267779]) ).
cnf(s16526,plain,
( ~ spl0_27
| spl0_33
| spl0_161
| spl0_1493 ),
inference(sat_conversion,[],[f269150]) ).
cnf(s16988,plain,
( spl0_1563
| spl0_4963
| ~ spl0_9018 ),
inference(sat_conversion,[],[f274794]) ).
cnf(s26110,plain,
( ~ spl0_4
| spl0_8
| ~ spl0_130
| spl0_1493
| ~ spl0_1495
| spl0_9018 ),
inference(sat_conversion,[],[f360313]) ).
cnf(s26729,plain,
( ~ spl0_4
| spl0_8
| ~ spl0_14
| spl0_130
| spl0_1493
| ~ spl0_1495 ),
inference(sat_conversion,[],[f368143]) ).
cnf(s26742,plain,
~ spl0_11649,
inference(sat_conversion,[],[f368415]) ).
cnf(s26836,plain,
( spl0_16
| spl0_24
| spl0_11649 ),
inference(sat_conversion,[],[f369287]) ).
cnf(s26837,plain,
( spl0_16
| spl0_17
| spl0_11649 ),
inference(sat_conversion,[],[f369288]) ).
cnf(s26954,plain,
( spl0_8
| spl0_27
| spl0_28
| ~ spl0_11650 ),
inference(sat_conversion,[],[f372663]) ).
cnf(s27019,plain,
( ~ spl0_14
| ~ spl0_17
| spl0_11731
| spl0_11777 ),
inference(sat_conversion,[],[f372959]) ).
cnf(s27071,plain,
( spl0_16
| spl0_11649
| ~ spl0_11731 ),
inference(sat_conversion,[],[f373517]) ).
cnf(s29893,plain,
( ~ spl0_4
| spl0_8
| ~ spl0_14
| spl0_28
| spl0_11672
| ~ spl0_11777 ),
inference(sat_conversion,[],[f397929]) ).
cnf(s50037,plain,
( ~ spl0_4
| ~ spl0_6
| spl0_8
| ~ spl0_14
| ~ spl0_17
| ~ spl0_24
| spl0_28
| spl0_11649
| spl0_11650
| ~ spl0_11672 ),
inference(sat_conversion,[],[f802944]) ).
cnf(s50761,plain,
~ spl0_123,
inference(rat,[],[s590,s18]) ).
cnf(s50764,plain,
~ spl0_161,
inference(rat,[],[s304,s18]) ).
cnf(s50765,plain,
~ spl0_33,
inference(rat,[],[s273,s18]) ).
cnf(s50766,plain,
~ spl0_153,
inference(rat,[],[s264,s18]) ).
cnf(s50767,plain,
~ spl0_1563,
inference(rat,[],[s9061,s50761]) ).
cnf(s50864,plain,
~ spl0_4963,
inference(rat,[],[s14258,s50761,s50766]) ).
cnf(s50865,plain,
~ spl0_1493,
inference(rat,[],[s16299,s50767]) ).
cnf(s50949,plain,
~ spl0_9018,
inference(rat,[],[s16988,s50767,s50864]) ).
cnf(s51026,plain,
~ spl0_27,
inference(rat,[],[s16526,s50765,s50764,s50865]) ).
cnf(s51027,plain,
~ spl0_28,
inference(rat,[],[s15977,s50765,s50865]) ).
cnf(s51349,plain,
~ spl0_1,
inference(rat,[],[s37,s51027,s51026]) ).
cnf(s51434,plain,
~ spl0_11650,
inference(rat,[],[s26954,s51026,s18,s51027]) ).
cnf(s51818,plain,
spl0_6,
inference(rat,[],[s7,s51349]) ).
cnf(s51822,plain,
spl0_4,
inference(rat,[],[s3,s51349]) ).
cnf(s52118,plain,
~ spl0_3,
inference(rat,[],[s2,s51349]) ).
cnf(s52119,plain,
~ spl0_15,
inference(rat,[],[s2053,s51822,s18,s51818,s52118]) ).
cnf(s52121,plain,
spl0_14,
inference(rat,[],[s15,s52119]) ).
cnf(s56109,plain,
spl0_16,
inference(rat,[],[s29893,s50037,s27019,s26836,s26837,s27071,s18,s51027,s51822,s52121,s51818,s26742,s51434]) ).
cnf(s56123,plain,
spl0_1498,
inference(rat,[],[s2641,s51027,s56109]) ).
cnf(s56199,plain,
spl0_1495,
inference(rat,[],[s15998,s56123]) ).
cnf(s56206,plain,
~ spl0_130,
inference(rat,[],[s26110,s50949,s51822,s50865,s18,s56199]) ).
cnf(s56208,plain,
$false,
inference(rat,[],[s26729,s52121,s50865,s51822,s18,s56199,s56206]) ).
fof(f802945,plain,
$false,
inference(avatar_sat_refutation,[],[s56208]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWC298-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 08:56:36 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.13 Running first-order model finding
% 0.09/0.13 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
% 9.26/1.56 % (3243654)Will run a generic schedule for satisfiability detection.
% 9.26/1.56 % (3243664)% WARNING: option uhcvi not known.
% 9.26/1.56 % (3243665)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1423326035:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 9.26/1.56 % (3243666)dis+10_1_sil=32000:sp=arity:random_seed=2146020341:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 9.26/1.56 % (3243667)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1970541992:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 9.26/1.56 % (3243668)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=751661604:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 9.26/1.56 % (3243663)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2208769216_2999 on theBenchmark for (2999ds/0Mi)
% 9.26/1.56 % (3243664)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2086859977:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 9.26/1.56 % (3243669)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3221250969:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 9.26/1.56 % TRYING [1]
% 9.26/1.56 % TRYING [2]
% 9.26/1.56 % TRYING [3]
% 9.26/1.56 % TRYING [4]
% 9.26/1.56 % (3243667)Instruction limit reached!
% 9.26/1.56 % (3243667)------------------------------
% 9.26/1.56 % (3243667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.26/1.56 % (3243667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.26/1.56 % (3243667)CaDiCaL version: 2.1.3
% 9.26/1.56 % (3243667)Termination reason: Instruction limit
% 9.26/1.56 % (3243667)Termination phase: Saturation
% 9.26/1.56 % (3243667)Time elapsed: 0.031 s
% 9.26/1.56 % (3243667)Peak memory usage: 13 MB
% 9.26/1.56 % (3243667)Instructions burned: 117 (million)
% 9.26/1.56 % (3243668)Instruction limit reached!
% 9.26/1.56 % (3243668)------------------------------
% 9.26/1.56 % (3243668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.26/1.56 % (3243668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.26/1.56 % (3243668)CaDiCaL version: 2.1.3
% 9.26/1.56 % (3243668)Termination reason: Instruction limit
% 9.26/1.56 % (3243668)Termination phase: Saturation
% 9.26/1.56 % (3243668)Time elapsed: 0.035 s
% 9.26/1.56 % (3243668)Peak memory usage: 14 MB
% 9.26/1.56 % (3243668)Instructions burned: 134 (million)
% 9.26/1.56 % (3243677)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3924960898:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 9.26/1.56 % (3243678)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1079862532:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 9.26/1.56 % TRYING [1]
% 9.26/1.56 % TRYING [2]
% 9.26/1.56 % (3243669)Instruction limit reached!
% 9.26/1.56 % (3243669)------------------------------
% 9.26/1.56 % (3243669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.26/1.56 % (3243669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.26/1.56 % (3243669)CaDiCaL version: 2.1.3
% 9.26/1.56 % (3243669)Termination reason: Instruction limit
% 9.26/1.56 % (3243669)Termination phase: Saturation
% 9.26/1.56 % (3243669)Time elapsed: 0.050 s
% 9.26/1.56 % (3243669)Peak memory usage: 14 MB
% 9.26/1.56 % (3243669)Instructions burned: 161 (million)
% 9.26/1.56 % TRYING [3]
% 9.26/1.56 % (3243666)Instruction limit reached!
% 9.26/1.56 % (3243666)------------------------------
% 9.26/1.56 % (3243666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.26/1.56 % (3243666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.26/1.56 % (3243666)CaDiCaL version: 2.1.3
% 9.26/1.56 % (3243666)Termination reason: Instruction limit
% 9.26/1.56 % (3243666)Termination phase: Saturation
% 9.26/1.56 % (3243666)Time elapsed: 0.053 s
% 9.26/1.56 % (3243666)Peak memory usage: 12 MB
% 9.26/1.56 % (3243666)Instructions burned: 105 (million)
% 9.26/1.56 % TRYING [5]
% 9.26/1.56 % TRYING [4]
% 9.26/1.56 % (3243682)ott-21_1_sil=16000:fs=off:random_seed=883941788:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 9.26/1.56 % (3243681)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=4291953494:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 9.26/1.56 % (3243678)Instruction limit reached!
% 9.26/1.56 % (3243678)------------------------------
% 9.26/1.56 % (3243678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.98/4.14 % (3243678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.98/4.14 % (3243678)CaDiCaL version: 2.1.3
% 27.98/4.14 % (3243678)Termination reason: Instruction limit
% 27.98/4.14 % (3243678)Termination phase: Saturation
% 27.98/4.14 % (3243678)Time elapsed: 0.035 s
% 27.98/4.14 % (3243678)Peak memory usage: 13 MB
% 27.98/4.14 % (3243678)Instructions burned: 134 (million)
% 27.98/4.14 % (3243685)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2092880730:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 27.98/4.14 % TRYING [5]
% 27.98/4.14 % (3243682)Instruction limit reached!
% 27.98/4.14 % (3243682)------------------------------
% 27.98/4.14 % (3243682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.98/4.14 % (3243682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.98/4.14 % (3243682)CaDiCaL version: 2.1.3
% 27.98/4.14 % (3243682)Termination reason: Instruction limit
% 27.98/4.14 % (3243682)Termination phase: Saturation
% 27.98/4.14 % (3243682)Time elapsed: 0.048 s
% 27.98/4.14 % (3243682)Peak memory usage: 13 MB
% 27.98/4.14 % (3243682)Instructions burned: 184 (million)
% 27.98/4.14 % (3243687)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2470035449:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 27.98/4.14 % TRYING [1]
% 27.98/4.14 % TRYING [2]
% 27.98/4.14 % TRYING [3]
% 27.98/4.14 % TRYING [6]
% 27.98/4.14 % TRYING [4]
% 27.98/4.14 % TRYING [6]
% 27.98/4.14 % (3243677)Instruction limit reached!
% 27.98/4.14 % (3243677)------------------------------
% 27.98/4.14 % (3243677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.98/4.14 % (3243677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.98/4.14 % (3243677)CaDiCaL version: 2.1.3
% 27.98/4.14 % (3243677)Termination reason: Instruction limit
% 27.98/4.14 % (3243677)Termination phase: Finite model building constraint generation
% 27.98/4.14 % (3243677)Time elapsed: 0.150 s
% 27.98/4.14 % (3243677)Peak memory usage: 34 MB
% 27.98/4.14 % (3243677)Instructions burned: 716 (million)
% 27.98/4.14 % (3243689)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3850323358:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 27.98/4.14 % TRYING [5]
% 27.98/4.14 % (3243685)Instruction limit reached!
% 27.98/4.14 % (3243685)------------------------------
% 27.98/4.14 % (3243685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.98/4.14 % (3243685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.98/4.14 % (3243685)CaDiCaL version: 2.1.3
% 27.98/4.14 % (3243685)Termination reason: Instruction limit
% 27.98/4.14 % (3243685)Termination phase: Saturation
% 27.98/4.14 % (3243685)Time elapsed: 0.158 s
% 27.98/4.14 % (3243685)Peak memory usage: 14 MB
% 27.98/4.14 % (3243685)Instructions burned: 479 (million)
% 27.98/4.14 % (3243691)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4235198219:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 27.98/4.14 % (3243687)Instruction limit reached!
% 27.98/4.14 % (3243687)------------------------------
% 27.98/4.14 % (3243687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.98/4.14 % (3243687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.98/4.14 % (3243687)CaDiCaL version: 2.1.3
% 27.98/4.14 % (3243687)Termination reason: Instruction limit
% 27.98/4.14 % (3243687)Termination phase: Finite model building SAT solving
% 27.98/4.14 % (3243687)Time elapsed: 0.189 s
% 27.98/4.14 % (3243687)Peak memory usage: 22 MB
% 27.98/4.14 % (3243687)Instructions burned: 868 (million)
% 27.98/4.14 % TRYING [14]
% 27.98/4.14 % (3243693)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=2450179497:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 27.98/4.14 % (3243681)Instruction limit reached!
% 27.98/4.14 % (3243681)------------------------------
% 27.98/4.14 % (3243681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.98/4.14 % (3243681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.98/4.14 % (3243681)CaDiCaL version: 2.1.3
% 27.98/4.14 % (3243681)Termination reason: Instruction limit
% 27.98/4.14 % (3243681)Termination phase: Saturation
% 27.98/4.14 % (3243681)Time elapsed: 0.354 s
% 27.98/4.14 % (3243681)Peak memory usage: 21 MB
% 27.98/4.14 % (3243681)Instructions burned: 685 (million)
% 27.98/4.14 % (3243703)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=806734274:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 27.98/4.14 % TRYING [7]
% 53.96/7.84 % (3243691)Instruction limit reached!
% 53.96/7.84 % (3243691)------------------------------
% 53.96/7.84 % (3243691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.96/7.84 % (3243691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.96/7.84 % (3243691)CaDiCaL version: 2.1.3
% 53.96/7.84 % (3243691)Termination reason: Instruction limit
% 53.96/7.84 % (3243691)Termination phase: Finite model building constraint generation
% 53.96/7.84 % (3243691)Time elapsed: 0.233 s
% 53.96/7.84 % (3243691)Peak memory usage: 72 MB
% 53.96/7.84 % (3243691)Instructions burned: 890 (million)
% 53.96/7.84 % (3243705)fmb+10_1_sil=64000:random_seed=438217145:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 53.96/7.84 % TRYING [1]
% 53.96/7.84 % TRYING [2]
% 53.96/7.84 % TRYING [3]
% 53.96/7.84 % TRYING [4]
% 53.96/7.84 % (3243693)Instruction limit reached!
% 53.96/7.84 % (3243693)------------------------------
% 53.96/7.84 % (3243693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.96/7.84 % (3243693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.96/7.84 % (3243693)CaDiCaL version: 2.1.3
% 53.96/7.84 % (3243693)Termination reason: Instruction limit
% 53.96/7.84 % (3243693)Termination phase: Saturation
% 53.96/7.84 % (3243693)Time elapsed: 0.296 s
% 53.96/7.84 % (3243693)Peak memory usage: 19 MB
% 53.96/7.84 % (3243693)Instructions burned: 692 (million)
% 53.96/7.84 % (3243718)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2886929359:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi)
% 53.96/7.84 % TRYING [20]
% 53.96/7.84 % TRYING [5]
% 53.96/7.84 % (3243689)Instruction limit reached!
% 53.96/7.84 % (3243689)------------------------------
% 53.96/7.84 % (3243689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.96/7.84 % (3243689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.96/7.84 % (3243689)CaDiCaL version: 2.1.3
% 53.96/7.84 % (3243689)Termination reason: Instruction limit
% 53.96/7.84 % (3243689)Termination phase: Saturation
% 53.96/7.84 % (3243689)Time elapsed: 0.487 s
% 53.96/7.84 % (3243689)Peak memory usage: 29 MB
% 53.96/7.84 % (3243689)Instructions burned: 1180 (million)
% 53.96/7.84 % (3243720)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3992446603:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi)
% 53.96/7.84 % TRYING [8]
% 53.96/7.84 % (3243703)Instruction limit reached!
% 53.96/7.84 % (3243703)------------------------------
% 53.96/7.84 % (3243703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.96/7.84 % (3243703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.96/7.84 % (3243703)CaDiCaL version: 2.1.3
% 53.96/7.84 % (3243703)Termination reason: Instruction limit
% 53.96/7.84 % (3243703)Termination phase: Saturation
% 53.96/7.84 % (3243703)Time elapsed: 0.320 s
% 53.96/7.84 % (3243703)Peak memory usage: 20 MB
% 53.96/7.84 % (3243703)Instructions burned: 881 (million)
% 53.96/7.84 % (3243722)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1515056768:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 53.96/7.84 % TRYING [6]
% 53.96/7.84 % (3243720)Instruction limit reached!
% 53.96/7.84 % (3243720)------------------------------
% 53.96/7.84 % (3243720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.96/7.84 % (3243720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.96/7.84 % (3243720)CaDiCaL version: 2.1.3
% 53.96/7.84 % (3243720)Termination reason: Instruction limit
% 53.96/7.84 % (3243720)Termination phase: Finite model building constraint generation
% 53.96/7.84 % (3243720)Time elapsed: 0.317 s
% 53.96/7.84 % (3243720)Peak memory usage: 79 MB
% 53.96/7.84 % (3243720)Instructions burned: 923 (million)
% 53.96/7.84 % (3243732)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3097944069:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi)
% 53.96/7.84 % TRYING [8]
% 53.96/7.84 % (3243732)Instruction limit reached!
% 53.96/7.84 % (3243732)------------------------------
% 53.96/7.84 % (3243732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.96/7.84 % (3243732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.96/7.84 % (3243732)CaDiCaL version: 2.1.3
% 53.96/7.84 % (3243732)Termination reason: Instruction limit
% 53.96/7.84 % (3243732)Termination phase: Saturation
% 53.96/7.84 % (3243732)Time elapsed: 0.347 s
% 53.96/7.84 % (3243732)Peak memory usage: 15 MB
% 53.96/7.84 % (3243732)Instructions burned: 1473 (million)
% 53.96/7.84 % (3243744)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=544511265:i=6324_2985 on theBenchmark for (2985ds/6324Mi)
% 36.11/13.89 % TRYING [77]
% 36.11/13.89 % TRYING [7]
% 36.11/13.89 % (3243722)Instruction limit reached!
% 36.11/13.89 % (3243722)------------------------------
% 36.11/13.89 % (3243722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.11/13.89 % (3243722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.11/13.89 % (3243722)CaDiCaL version: 2.1.3
% 36.11/13.89 % (3243722)Termination reason: Instruction limit
% 36.11/13.89 % (3243722)Termination phase: Saturation
% 36.11/13.89 % (3243722)Time elapsed: 1.507 s
% 36.11/13.89 % (3243722)Peak memory usage: 55 MB
% 36.11/13.89 % (3243722)Instructions burned: 5131 (million)
% 36.11/13.89 % (3243891)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2725872015:fmbsr=2.30978:i=2174_2976 on theBenchmark for (2976ds/2174Mi)
% 36.11/13.89 % TRYING [16]
% 36.11/13.89 % TRYING [9]
% 36.11/13.89 % (3243744)Instruction limit reached!
% 36.11/13.89 % (3243744)------------------------------
% 36.11/13.89 % (3243744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.11/13.89 % (3243744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.11/13.89 % (3243744)CaDiCaL version: 2.1.3
% 36.11/13.89 % (3243744)Termination reason: Instruction limit
% 36.11/13.89 % (3243744)Termination phase: Finite model building constraint generation
% 36.11/13.89 % (3243744)Time elapsed: 1.231 s
% 36.11/13.89 % (3243744)Peak memory usage: 432 MB
% 36.11/13.89 % (3243744)Instructions burned: 6328 (million)
% 36.11/13.89 % (3243718)Instruction limit reached!
% 36.11/13.89 % (3243718)------------------------------
% 36.11/13.89 % (3243718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.11/13.89 % (3243718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.11/13.89 % (3243718)CaDiCaL version: 2.1.3
% 36.11/13.89 % (3243718)Termination reason: Instruction limit
% 36.11/13.89 % (3243718)Termination phase: Finite model building constraint generation
% 36.11/13.89 % (3243718)Time elapsed: 2.032 s
% 36.11/13.89 % (3243718)Peak memory usage: 588 MB
% 36.11/13.89 % (3243718)Instructions burned: 9517 (million)
% 36.11/13.89 % (3243893)ott-2_1_sil=16000:newcnf=on:random_seed=1072350864:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2973 on theBenchmark for (2973ds/869Mi)
% 36.11/13.89 % TRYING [8]
% 36.11/13.89 % (3243891)Instruction limit reached!
% 36.11/13.89 % (3243891)------------------------------
% 36.11/13.89 % (3243891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.11/13.89 % (3243891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.11/13.89 % (3243891)CaDiCaL version: 2.1.3
% 36.11/13.89 % (3243891)Termination reason: Instruction limit
% 36.11/13.89 % (3243891)Termination phase: Finite model building constraint generation
% 36.11/13.89 % (3243891)Time elapsed: 0.414 s
% 36.11/13.89 % (3243891)Peak memory usage: 138 MB
% 36.11/13.89 % (3243891)Instructions burned: 2175 (million)
% 36.11/13.89 % (3243895)ott+10_1_sil=32000:tgt=ground:random_seed=2300264105:i=5114:av=off_2972 on theBenchmark for (2972ds/5114Mi)
% 36.11/13.89 % (3243896)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2529808716:i=54282_2972 on theBenchmark for (2972ds/54282Mi)
% 36.11/13.89 % TRYING [1]
% 36.11/13.89 % TRYING [2]
% 36.11/13.89 % TRYING [3]
% 36.11/13.89 % TRYING [4]
% 36.11/13.89 % TRYING [5]
% 36.11/13.89 % TRYING [6]
% 36.11/13.89 % (3243893)Instruction limit reached!
% 36.11/13.89 % (3243893)------------------------------
% 36.11/13.89 % (3243893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.11/13.89 % (3243893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.11/13.89 % (3243893)CaDiCaL version: 2.1.3
% 36.11/13.89 % (3243893)Termination reason: Instruction limit
% 36.11/13.89 % (3243893)Termination phase: Saturation
% 36.11/13.89 % (3243893)Time elapsed: 0.245 s
% 36.11/13.89 % (3243893)Peak memory usage: 25 MB
% 36.11/13.89 % (3243893)Instructions burned: 872 (million)
% 36.11/13.89 % (3243899)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2314655542:i=3512:aac=none_2970 on theBenchmark for (2970ds/3512Mi)
% 36.11/13.89 % TRYING [7]
% 36.11/13.89 % TRYING [8]
% 36.11/13.89 % (3243899)Instruction limit reached!
% 36.11/13.89 % (3243899)------------------------------
% 36.11/13.89 % (3243899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.11/13.89 % (3243899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.11/13.89 % (3243899)CaDiCaL version: 2.1.3
% 36.11/13.89 % (3243899)Termination reason: Instruction limit
% 36.11/13.89 % (3243899)Termination phase: Saturation
% 36.11/13.89 % (3243899)Time elapsed: 1.044 s
% 36.11/13.89 % (3243899)Peak memory usage: 39 MB
% 36.11/13.89 % (3243899)Instructions burned: 3514 (million)
% 36.11/13.89 % (3243901)dis+21_1_sil=32000:sas=cadical:random_seed=3787128034:i=3773:amm=off_2959 on theBenchmark for (2959ds/3773Mi)
% 36.11/13.89 % (3243895)Instruction limit reached!
% 36.11/13.89 % (3243895)------------------------------
% 36.11/13.89 % (3243895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.11/13.89 % (3243895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.11/13.89 % (3243895)CaDiCaL version: 2.1.3
% 36.11/13.89 % (3243895)Termination reason: Instruction limit
% 36.11/13.89 % (3243895)Termination phase: Saturation
% 36.11/13.89 % (3243895)Time elapsed: 1.538 s
% 36.11/13.89 % (3243895)Peak memory usage: 72 MB
% 36.11/13.89 % (3243895)Instructions burned: 5114 (million)
% 36.11/13.89 % (3243903)ott+11_1_sil=16000:gs=on:random_seed=67029329:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2956 on theBenchmark for (2956ds/2251Mi)
% 36.11/13.89 % (3243903)Instruction limit reached!
% 36.11/13.89 % (3243903)------------------------------
% 36.11/13.89 % (3243903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.11/13.89 % (3243903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.11/13.89 % (3243903)CaDiCaL version: 2.1.3
% 36.11/13.89 % (3243903)Termination reason: Instruction limit
% 36.11/13.89 % (3243903)Termination phase: Saturation
% 36.11/13.89 % (3243903)Time elapsed: 0.494 s
% 36.11/13.89 % (3243903)Peak memory usage: 15 MB
% 36.11/13.89 % (3243903)Instructions burned: 2253 (million)
% 36.11/13.89 % (3243905)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=858619714:fmbsr=1.6:i=67534_2951 on theBenchmark for (2951ds/67534Mi)
% 36.11/13.89 % TRYING [7]
% 36.11/13.89 % TRYING [10]
% 36.11/13.89 % TRYING [9]
% 36.11/13.89 % TRYING [9]
% 36.11/13.89 % (3243901)Instruction limit reached!
% 36.11/13.89 % (3243901)------------------------------
% 36.11/13.89 % (3243901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.11/13.89 % (3243901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.11/13.89 % (3243901)CaDiCaL version: 2.1.3
% 36.11/13.89 % (3243901)Termination reason: Instruction limit
% 36.11/13.89 % (3243901)Termination phase: Saturation
% 36.11/13.89 % (3243901)Time elapsed: 1.127 s
% 36.11/13.89 % (3243901)Peak memory usage: 46 MB
% 36.11/13.89 % (3243901)Instructions burned: 3773 (million)
% 36.11/13.89 % (3243907)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=826363878:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2948 on theBenchmark for (2948ds/4591Mi)
% 36.11/13.89 % (3243705)Instruction limit reached!
% 36.11/13.89 % (3243705)------------------------------
% 36.11/13.89 % (3243705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.11/13.89 % (3243705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.11/13.89 % (3243705)CaDiCaL version: 2.1.3
% 36.11/13.89 % (3243705)Termination reason: Instruction limit
% 36.11/13.89 % (3243705)Termination phase: Finite model building constraint generation
% 36.11/13.89 % (3243705)Time elapsed: 5.232 s
% 36.11/13.89 % (3243705)Peak memory usage: 242 MB
% 36.11/13.89 % (3243705)Instructions burned: 22064 (million)
% 36.11/13.89 % (3243909)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2317680702:i=29340_2942 on theBenchmark for (2942ds/29340Mi)
% 36.11/13.89 % TRYING [8]
% 36.11/13.89 % (3243907)Instruction limit reached!
% 36.11/13.89 % (3243907)------------------------------
% 36.11/13.89 % (3243907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.11/13.89 % (3243907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.11/13.89 % (3243907)CaDiCaL version: 2.1.3
% 36.11/13.89 % (3243907)Termination reason: Instruction limit
% 36.11/13.89 % (3243907)Termination phase: Saturation
% 36.11/13.89 % (3243907)Time elapsed: 1.077 s
% 36.11/13.89 % (3243907)Peak memory usage: 53 MB
% 36.11/13.89 % (3243907)Instructions burned: 4595 (million)
% 36.11/13.89 % (3243911)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3141483369:i=5211_2937 on theBenchmark for (2937ds/5211Mi)
% 36.11/13.89 % (3243911)Instruction limit reached!
% 36.11/13.89 % (3243911)------------------------------
% 36.11/13.89 % (3243911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.11/13.89 % (3243911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.11/13.89 % (3243911)CaDiCaL version: 2.1.3
% 36.11/13.89 % (3243911)Termination reason: Instruction limit
% 36.11/13.89 % (3243911)Termination phase: Saturation
% 36.11/13.89 % (3243911)Time elapsed: 1.447 s
% 36.11/13.89 % (3243911)Peak memory usage: 47 MB
% 36.11/13.89 % (3243911)Instructions burned: 5215 (million)
% 36.11/13.89 % (3243913)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1028768854:i=5497:nm=2_2922 on theBenchmark for (2922ds/5497Mi)
% 36.11/13.89 % TRYING [17]
% 36.11/13.89 % TRYING [9]
% 36.11/13.89 % (3243913)Instruction limit reached!
% 36.11/13.89 % (3243913)------------------------------
% 36.11/13.89 % (3243913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.11/13.89 % (3243913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.11/13.89 % (3243913)CaDiCaL version: 2.1.3
% 36.11/13.89 % (3243913)Termination reason: Instruction limit
% 36.11/13.89 % (3243913)Termination phase: Finite model building constraint generation
% 36.11/13.89 % (3243913)Time elapsed: 1.034 s
% 36.11/13.89 % (3243913)Peak memory usage: 344 MB
% 36.11/13.89 % (3243913)Instructions burned: 5499 (million)
% 36.11/13.89 % (3243915)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3785903223:fmbsr=2:i=46332_2912 on theBenchmark for (2912ds/46332Mi)
% 36.11/13.89 % TRYING [15]
% 36.11/13.89 % TRYING [10]
% 36.11/13.89 % TRYING [10]
% 36.11/13.89 % (3243664) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3243654-3243664"...
% 36.11/13.89 % (3243664)...printing done.
% 36.11/13.89 % (3243664)Refutation found. Thanks to Tanya!
% 36.11/13.89 % SZS status Unsatisfiable for theBenchmark
% 36.11/13.89 % SZS output start Proof for theBenchmark
% See solution above
% 36.11/13.89 % (3243664)------------------------------
% 36.11/13.89 % (3243664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.11/13.89 % (3243664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.11/13.89 % (3243664)CaDiCaL version: 2.1.3
% 36.11/13.89 % (3243664)Termination reason: Refutation
% 36.11/13.89 % (3243664)Time elapsed: 13.584 s
% 36.11/13.89 % (3243664)Peak memory usage: 330 MB
% 36.11/13.89 % (3243664)Instructions burned: 43648 (million)
% 36.11/13.89 % (3243654)Success in time 13.76 s
% 36.11/13.89 % Vampire exiting
%------------------------------------------------------------------------------