%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWC197-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:02:54 PM UTC 2026
% Result : Unsatisfiable 13.91s 2.99s
% Output : Refutation 15.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 65
% Syntax : Number of formulae : 344 ( 53 unt; 33 def)
% Number of atoms : 1095 ( 183 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 1447 ( 696 ~; 724 |; 0 &)
% ( 27 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 28 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 15 con; 0-2 aty)
% Number of variables : 112 ( 0 sgn 112 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
fof(f47,axiom,
! [X0] : ssItem(skaf44(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
fof(f72,axiom,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause72) ).
fof(f73,axiom,
! [X0] :
( ~ ssList(X0)
| app(X0,nil) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause73) ).
fof(f74,axiom,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause74) ).
fof(f77,axiom,
! [X0] :
( ssList(tl(X0))
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
fof(f78,axiom,
! [X0] :
( ssItem(hd(X0))
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause78) ).
fof(f80,axiom,
! [X0] :
( ~ segmentP(nil,X0)
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause80) ).
fof(f85,axiom,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause86) ).
fof(f96,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| tl(cons(X0,X1)) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause96) ).
fof(f98,axiom,
! [X0,X1] :
( cons(X0,X1) != nil
| ~ ssItem(X0)
| ~ ssList(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause98) ).
fof(f99,plain,
! [X0,X1] :
( nil != cons(X0,X1)
| ~ ssItem(X0)
| ~ ssList(X1) ),
inference(reorient_equations,[],[f98]) ).
fof(f101,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| neq(X1,X0)
| X1 = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause100) ).
fof(f102,plain,
! [X0,X1] :
( neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0)
| X0 = X1 ),
inference(reorient_equations,[],[f101]) ).
fof(f103,axiom,
! [X0] :
( ~ singletonP(X0)
| ~ ssList(X0)
| cons(skaf44(X0),nil) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause101) ).
fof(f107,axiom,
! [X0] :
( ~ ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause104) ).
fof(f121,axiom,
! [X0,X1] :
( app(X0,X1) != nil
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',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/theBenchmark.p',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/theBenchmark.p',clause120) ).
fof(f126,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(reorient_equations,[],[f125]) ).
fof(f144,axiom,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| nil = X1
| tl(app(X1,X0)) = app(tl(X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause133) ).
fof(f184,axiom,
! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X3)
| ~ ssList(X1)
| X3 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause171) ).
fof(f185,plain,
! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X3)
| ~ ssList(X1)
| X1 = X3 ),
inference(reorient_equations,[],[f184]) ).
fof(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/theBenchmark.p',clause179) ).
fof(f202,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_3) ).
fof(f203,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_4) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
segmentP(sk4,sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
ssItem(sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_10) ).
fof(f210,negated_conjecture,
ssList(sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).
fof(f211,negated_conjecture,
ssList(sk9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_12) ).
fof(f212,negated_conjecture,
app(app(app(app(sk7,cons(sk5,nil)),sk9),cons(sk6,nil)),sk8) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_13) ).
fof(f213,plain,
sk1 = app(app(app(app(sk7,cons(sk5,nil)),sk9),cons(sk6,nil)),sk8),
inference(reorient_equations,[],[f212]) ).
fof(f215,negated_conjecture,
( singletonP(sk3)
| ~ neq(sk4,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_15) ).
fof(f218,plain,
sk3 = app(app(app(app(sk7,cons(sk5,nil)),sk9),cons(sk6,nil)),sk8),
inference(definition_unfolding,[],[f213,f205]) ).
fof(f236,plain,
! [X2,X3,X0,X1] :
( ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(X3) ),
inference(equality_resolution,[],[f193]) ).
fof(f243,definition,
sF0 = cons(sk5,nil),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f244,plain,
cons(sk5,nil) = sF0,
inference(reorient_equations,[],[f243]) ).
fof(f245,definition,
sF1 = app(sk7,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f246,plain,
app(sk7,sF0) = sF1,
inference(reorient_equations,[],[f245]) ).
fof(f247,definition,
sF2 = app(sF1,sk9),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f248,plain,
app(sF1,sk9) = sF2,
inference(reorient_equations,[],[f247]) ).
fof(f249,definition,
sF3 = cons(sk6,nil),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f250,plain,
cons(sk6,nil) = sF3,
inference(reorient_equations,[],[f249]) ).
fof(f251,definition,
sF4 = app(sF2,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f252,plain,
app(sF2,sF3) = sF4,
inference(reorient_equations,[],[f251]) ).
fof(f253,definition,
sF5 = app(sF4,sk8),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f254,plain,
app(sF4,sk8) = sF5,
inference(reorient_equations,[],[f253]) ).
fof(f255,plain,
sk3 = sF5,
inference(definition_folding,[],[f218,f254,f252,f250,f248,f246,f244]) ).
fof(f263,definition,
( spl6_1
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[spl6_1])],[avatar_definition]) ).
fof(f265,plain,
( ~ neq(sk4,nil)
| spl6_1 ),
inference(avatar_component_clause,[],[f263]) ).
fof(f267,definition,
( spl6_2
<=> singletonP(sk3) ),
introduced(definition,[new_symbols(definition,[spl6_2])],[avatar_definition]) ).
fof(f269,plain,
( singletonP(sk3)
| ~ spl6_2 ),
inference(avatar_component_clause,[],[f267]) ).
fof(f270,plain,
( ~ spl6_1
| spl6_2 ),
inference(avatar_split_clause,[],[f215,f267,f263]) ).
fof(f276,definition,
( spl6_4
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl6_4])],[avatar_definition]) ).
fof(f277,plain,
( ssList(nil)
| ~ spl6_4 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f304,definition,
( spl6_10
<=> ! [X1] : ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl6_10])],[avatar_definition]) ).
fof(f305,plain,
( ! [X1] : ssItem(X1)
| ~ spl6_10 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f307,definition,
( spl6_11
<=> ! [X0] :
( ~ ssList(X0)
| duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl6_11])],[avatar_definition]) ).
fof(f308,plain,
( ! [X0] :
( ~ ssList(X0)
| duplicatefreeP(X0) )
| ~ spl6_11 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f309,plain,
( spl6_10
| spl6_11 ),
inference(avatar_split_clause,[],[f72,f307,f304]) ).
fof(f312,plain,
spl6_4,
inference(avatar_split_clause,[],[f8,f276]) ).
fof(f313,plain,
sk3 = app(sF4,sk8),
inference(forward_demodulation,[],[f254,f255]) ).
fof(f314,plain,
( ~ ssList(sk4)
| ~ ssList(nil)
| nil = sk4
| spl6_1 ),
inference(resolution,[],[f102,f265]) ).
fof(f315,plain,
( ~ ssList(nil)
| nil = sk4
| spl6_1 ),
inference(forward_subsumption_resolution,[],[f314,f203]) ).
fof(f316,plain,
( nil = sk4
| spl6_1
| ~ spl6_4 ),
inference(forward_subsumption_resolution,[],[f315,f277]) ).
fof(f317,plain,
( ssList(sF1)
| ~ ssList(sk7)
| ~ ssList(sF0) ),
inference(superposition,[],[f85,f246]) ).
fof(f318,plain,
( ssList(sF2)
| ~ ssList(sF1)
| ~ ssList(sk9) ),
inference(superposition,[],[f85,f248]) ).
fof(f319,plain,
( ssList(sF4)
| ~ ssList(sF2)
| ~ ssList(sF3) ),
inference(superposition,[],[f85,f252]) ).
fof(f322,definition,
( spl6_12
<=> ssList(sF3) ),
introduced(definition,[new_symbols(definition,[spl6_12])],[avatar_definition]) ).
fof(f323,plain,
( ssList(sF3)
| ~ spl6_12 ),
inference(avatar_component_clause,[],[f322]) ).
fof(f324,plain,
( ~ ssList(sF3)
| spl6_12 ),
inference(avatar_component_clause,[],[f322]) ).
fof(f326,definition,
( spl6_13
<=> ssList(sF2) ),
introduced(definition,[new_symbols(definition,[spl6_13])],[avatar_definition]) ).
fof(f327,plain,
( ssList(sF2)
| ~ spl6_13 ),
inference(avatar_component_clause,[],[f326]) ).
fof(f330,definition,
( spl6_14
<=> ssList(sF4) ),
introduced(definition,[new_symbols(definition,[spl6_14])],[avatar_definition]) ).
fof(f332,plain,
( ssList(sF4)
| ~ spl6_14 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f333,plain,
( ~ spl6_12
| ~ spl6_13
| spl6_14 ),
inference(avatar_split_clause,[],[f319,f330,f326,f322]) ).
fof(f334,plain,
( ssList(sF2)
| ~ ssList(sF1) ),
inference(forward_subsumption_resolution,[],[f318,f211]) ).
fof(f335,plain,
( ssList(sF1)
| ~ ssList(sF0) ),
inference(forward_subsumption_resolution,[],[f317,f209]) ).
fof(f337,definition,
( spl6_15
<=> ssList(sF1) ),
introduced(definition,[new_symbols(definition,[spl6_15])],[avatar_definition]) ).
fof(f338,plain,
( ssList(sF1)
| ~ spl6_15 ),
inference(avatar_component_clause,[],[f337]) ).
fof(f340,plain,
( ~ spl6_15
| spl6_13 ),
inference(avatar_split_clause,[],[f334,f326,f337]) ).
fof(f342,definition,
( spl6_16
<=> ssList(sF0) ),
introduced(definition,[new_symbols(definition,[spl6_16])],[avatar_definition]) ).
fof(f343,plain,
( ssList(sF0)
| ~ spl6_16 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f344,plain,
( ~ ssList(sF0)
| spl6_16 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f345,plain,
( ~ spl6_16
| spl6_15 ),
inference(avatar_split_clause,[],[f335,f337,f342]) ).
fof(f346,plain,
( ssList(sF0)
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(superposition,[],[f86,f244]) ).
fof(f347,plain,
( ssList(sF3)
| ~ ssList(nil)
| ~ ssItem(sk6) ),
inference(superposition,[],[f86,f250]) ).
fof(f348,plain,
( ~ ssList(nil)
| ~ ssItem(sk6)
| spl6_12 ),
inference(forward_subsumption_resolution,[],[f347,f324]) ).
fof(f349,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| spl6_16 ),
inference(forward_subsumption_resolution,[],[f346,f344]) ).
fof(f350,plain,
( ~ ssItem(sk6)
| ~ spl6_4
| spl6_12 ),
inference(forward_subsumption_resolution,[],[f348,f277]) ).
fof(f351,plain,
( ~ ssItem(sk5)
| ~ spl6_4
| spl6_16 ),
inference(forward_subsumption_resolution,[],[f349,f277]) ).
fof(f352,plain,
( $false
| ~ spl6_4
| spl6_12 ),
inference(forward_subsumption_resolution,[],[f350,f208]) ).
fof(f353,plain,
( ~ spl6_4
| spl6_12 ),
inference(avatar_contradiction_clause,[],[f352]) ).
fof(f354,plain,
( $false
| ~ spl6_4
| spl6_16 ),
inference(forward_subsumption_resolution,[],[f351,f207]) ).
fof(f355,plain,
( ~ spl6_4
| spl6_16 ),
inference(avatar_contradiction_clause,[],[f354]) ).
fof(f362,plain,
( sF0 = app(nil,sF0)
| ~ spl6_16 ),
inference(resolution,[],[f74,f343]) ).
fof(f372,plain,
( segmentP(nil,sk3)
| spl6_1
| ~ spl6_4 ),
inference(superposition,[],[f206,f316]) ).
fof(f384,plain,
( sF4 = app(sF4,nil)
| ~ spl6_14 ),
inference(resolution,[],[f73,f332]) ).
fof(f388,plain,
! [X0] :
( ~ ssList(X0)
| cons(sk5,X0) = app(cons(sk5,nil),X0) ),
inference(resolution,[],[f126,f207]) ).
fof(f389,plain,
! [X0] :
( ~ ssList(X0)
| cons(sk6,X0) = app(cons(sk6,nil),X0) ),
inference(resolution,[],[f126,f208]) ).
fof(f390,plain,
! [X0] :
( ~ ssList(X0)
| cons(sk6,X0) = app(sF3,X0) ),
inference(forward_demodulation,[],[f389,f250]) ).
fof(f391,plain,
! [X0] :
( ~ ssList(X0)
| cons(sk5,X0) = app(sF0,X0) ),
inference(forward_demodulation,[],[f388,f244]) ).
fof(f401,plain,
( cons(sk6,sF2) = app(sF3,sF2)
| ~ spl6_13 ),
inference(resolution,[],[f390,f327]) ).
fof(f414,plain,
cons(sk5,sk9) = app(sF0,sk9),
inference(resolution,[],[f391,f211]) ).
fof(f424,plain,
( ~ ssList(sk3)
| nil = sk3
| spl6_1
| ~ spl6_4 ),
inference(resolution,[],[f80,f372]) ).
fof(f425,plain,
( nil = sk3
| spl6_1
| ~ spl6_4 ),
inference(forward_subsumption_resolution,[],[f424,f202]) ).
fof(f429,plain,
( nil != sF0
| ~ ssItem(sk5)
| ~ ssList(nil) ),
inference(superposition,[],[f99,f244]) ).
fof(f430,plain,
( nil != sF3
| ~ ssItem(sk6)
| ~ ssList(nil) ),
inference(superposition,[],[f99,f250]) ).
fof(f431,plain,
( nil != sF3
| ~ ssList(nil) ),
inference(forward_subsumption_resolution,[],[f430,f208]) ).
fof(f432,plain,
( nil != sF0
| ~ ssList(nil) ),
inference(forward_subsumption_resolution,[],[f429,f207]) ).
fof(f433,plain,
( nil != sF3
| ~ spl6_4 ),
inference(forward_subsumption_resolution,[],[f431,f277]) ).
fof(f434,plain,
( nil != sF0
| ~ spl6_4 ),
inference(forward_subsumption_resolution,[],[f432,f277]) ).
fof(f486,plain,
( nil != sF1
| ~ ssList(sF0)
| ~ ssList(sk7)
| nil = sF0 ),
inference(superposition,[],[f124,f246]) ).
fof(f488,plain,
( nil != sF4
| ~ ssList(sF3)
| ~ ssList(sF2)
| nil = sF3 ),
inference(superposition,[],[f124,f252]) ).
fof(f489,plain,
( nil != sk3
| ~ ssList(sk8)
| ~ ssList(sF4)
| nil = sk8 ),
inference(superposition,[],[f124,f313]) ).
fof(f490,plain,
( ~ ssList(sk8)
| ~ ssList(sF4)
| nil = sk8
| spl6_1
| ~ spl6_4 ),
inference(forward_subsumption_resolution,[],[f489,f425]) ).
fof(f491,plain,
( nil != sF4
| ~ ssList(sF2)
| nil = sF3
| ~ spl6_12 ),
inference(forward_subsumption_resolution,[],[f488,f323]) ).
fof(f493,plain,
( nil != sF1
| ~ ssList(sk7)
| nil = sF0
| ~ spl6_16 ),
inference(forward_subsumption_resolution,[],[f486,f343]) ).
fof(f494,plain,
( ~ ssList(sF4)
| nil = sk8
| spl6_1
| ~ spl6_4 ),
inference(forward_subsumption_resolution,[],[f490,f210]) ).
fof(f495,plain,
( nil != sF4
| nil = sF3
| ~ spl6_12
| ~ spl6_13 ),
inference(forward_subsumption_resolution,[],[f491,f327]) ).
fof(f497,plain,
( nil != sF1
| nil = sF0
| ~ spl6_16 ),
inference(forward_subsumption_resolution,[],[f493,f209]) ).
fof(f498,plain,
( nil = sk8
| spl6_1
| ~ spl6_4
| ~ spl6_14 ),
inference(forward_subsumption_resolution,[],[f494,f332]) ).
fof(f499,plain,
( nil != sF4
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13 ),
inference(forward_subsumption_resolution,[],[f495,f433]) ).
fof(f505,definition,
( spl6_18
<=> nil = sF2 ),
introduced(definition,[new_symbols(definition,[spl6_18])],[avatar_definition]) ).
fof(f506,plain,
( nil = sF2
| ~ spl6_18 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f507,plain,
( nil != sF2
| spl6_18 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f509,plain,
( nil != sF1
| ~ spl6_4
| ~ spl6_16 ),
inference(forward_subsumption_resolution,[],[f497,f434]) ).
fof(f511,plain,
( sk3 = app(sF4,nil)
| spl6_1
| ~ spl6_4
| ~ spl6_14 ),
inference(superposition,[],[f313,f498]) ).
fof(f512,plain,
( sk3 = sF4
| spl6_1
| ~ spl6_4
| ~ spl6_14 ),
inference(forward_demodulation,[],[f511,f384]) ).
fof(f513,plain,
( nil = sF4
| spl6_1
| ~ spl6_4
| ~ spl6_14 ),
inference(forward_demodulation,[],[f512,f425]) ).
fof(f514,plain,
( $false
| spl6_1
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14 ),
inference(forward_subsumption_resolution,[],[f513,f499]) ).
fof(f515,plain,
( spl6_1
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14 ),
inference(avatar_contradiction_clause,[],[f514]) ).
fof(f516,plain,
( nil != sk3
| ~ ssList(sF4)
| nil = sk8 ),
inference(forward_subsumption_resolution,[],[f489,f210]) ).
fof(f517,plain,
( nil != sk3
| nil = sk8
| ~ spl6_14 ),
inference(forward_subsumption_resolution,[],[f516,f332]) ).
fof(f519,definition,
( spl6_19
<=> nil = sk8 ),
introduced(definition,[new_symbols(definition,[spl6_19])],[avatar_definition]) ).
fof(f520,plain,
( nil != sk8
| spl6_19 ),
inference(avatar_component_clause,[],[f519]) ).
fof(f521,plain,
( nil = sk8
| ~ spl6_19 ),
inference(avatar_component_clause,[],[f519]) ).
fof(f523,definition,
( spl6_20
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl6_20])],[avatar_definition]) ).
fof(f524,plain,
( nil = sk3
| ~ spl6_20 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f525,plain,
( nil != sk3
| spl6_20 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f526,plain,
( spl6_19
| ~ spl6_20
| ~ spl6_14 ),
inference(avatar_split_clause,[],[f517,f330,f523,f519]) ).
fof(f527,plain,
( ~ ssList(sk3)
| sk3 = cons(skaf44(sk3),nil)
| ~ spl6_2 ),
inference(resolution,[],[f269,f103]) ).
fof(f528,plain,
( sk3 = cons(skaf44(sk3),nil)
| ~ spl6_2 ),
inference(forward_subsumption_resolution,[],[f527,f202]) ).
fof(f538,plain,
! [X0] :
( ~ ssList(X0)
| tl(cons(sk6,X0)) = X0 ),
inference(resolution,[],[f96,f208]) ).
fof(f549,plain,
( ! [X0] :
( ~ ssList(X0)
| nil = sF2
| tl(app(sF2,X0)) = app(tl(sF2),X0) )
| ~ spl6_13 ),
inference(resolution,[],[f144,f327]) ).
fof(f550,plain,
( ! [X0] :
( ~ ssList(X0)
| nil = sF3
| tl(app(sF3,X0)) = app(tl(sF3),X0) )
| ~ spl6_12 ),
inference(resolution,[],[f144,f323]) ).
fof(f551,plain,
( ! [X0] :
( ~ ssList(X0)
| nil = sF4
| tl(app(sF4,X0)) = app(tl(sF4),X0) )
| ~ spl6_14 ),
inference(resolution,[],[f144,f332]) ).
fof(f552,plain,
( ! [X0] :
( ~ ssList(X0)
| tl(app(sF4,X0)) = app(tl(sF4),X0) )
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14 ),
inference(forward_subsumption_resolution,[],[f551,f499]) ).
fof(f553,plain,
( ! [X0] :
( ~ ssList(X0)
| tl(app(sF3,X0)) = app(tl(sF3),X0) )
| ~ spl6_4
| ~ spl6_12 ),
inference(forward_subsumption_resolution,[],[f550,f433]) ).
fof(f554,plain,
( ! [X0] :
( ~ ssList(X0)
| tl(app(sF2,X0)) = app(tl(sF2),X0) )
| ~ spl6_13
| spl6_18 ),
inference(forward_subsumption_resolution,[],[f549,f507]) ).
fof(f566,definition,
( spl6_23
<=> nil = sk7 ),
introduced(definition,[new_symbols(definition,[spl6_23])],[avatar_definition]) ).
fof(f567,plain,
( nil != sk7
| spl6_23 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f568,plain,
( nil = sk7
| ~ spl6_23 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f585,plain,
( sk3 = app(sF4,nil)
| ~ spl6_19 ),
inference(superposition,[],[f313,f521]) ).
fof(f586,plain,
( sk3 = sF4
| ~ spl6_14
| ~ spl6_19 ),
inference(forward_demodulation,[],[f585,f384]) ).
fof(f593,plain,
( tl(app(sF4,sk8)) = app(tl(sF4),sk8)
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14 ),
inference(resolution,[],[f552,f210]) ).
fof(f620,plain,
( tl(app(sF2,sF3)) = app(tl(sF2),sF3)
| ~ spl6_12
| ~ spl6_13
| spl6_18 ),
inference(resolution,[],[f554,f323]) ).
fof(f622,plain,
( tl(sF4) = app(tl(sF2),sF3)
| ~ spl6_12
| ~ spl6_13
| spl6_18 ),
inference(forward_demodulation,[],[f620,f252]) ).
fof(f632,plain,
( nil != tl(sF4)
| ~ ssList(sF3)
| ~ ssList(tl(sF2))
| nil = sF3
| ~ spl6_12
| ~ spl6_13
| spl6_18 ),
inference(superposition,[],[f124,f622]) ).
fof(f633,plain,
( ssList(tl(sF4))
| ~ ssList(tl(sF2))
| ~ ssList(sF3)
| ~ spl6_12
| ~ spl6_13
| spl6_18 ),
inference(superposition,[],[f85,f622]) ).
fof(f634,plain,
( ssList(tl(sF4))
| ~ ssList(tl(sF2))
| ~ spl6_12
| ~ spl6_13
| spl6_18 ),
inference(forward_subsumption_resolution,[],[f633,f323]) ).
fof(f635,plain,
( nil != tl(sF4)
| ~ ssList(tl(sF2))
| nil = sF3
| ~ spl6_12
| ~ spl6_13
| spl6_18 ),
inference(forward_subsumption_resolution,[],[f632,f323]) ).
fof(f637,definition,
( spl6_27
<=> ssList(tl(sF2)) ),
introduced(definition,[new_symbols(definition,[spl6_27])],[avatar_definition]) ).
fof(f639,plain,
( ~ ssList(tl(sF2))
| spl6_27 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f641,definition,
( spl6_28
<=> ssList(tl(sF4)) ),
introduced(definition,[new_symbols(definition,[spl6_28])],[avatar_definition]) ).
fof(f643,plain,
( ssList(tl(sF4))
| ~ spl6_28 ),
inference(avatar_component_clause,[],[f641]) ).
fof(f644,plain,
( ~ spl6_27
| spl6_28
| ~ spl6_12
| ~ spl6_13
| spl6_18 ),
inference(avatar_split_clause,[],[f634,f505,f326,f322,f641,f637]) ).
fof(f645,plain,
( nil != tl(sF4)
| ~ ssList(tl(sF2))
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| spl6_18 ),
inference(forward_subsumption_resolution,[],[f635,f433]) ).
fof(f647,definition,
( spl6_29
<=> nil = tl(sF4) ),
introduced(definition,[new_symbols(definition,[spl6_29])],[avatar_definition]) ).
fof(f649,plain,
( nil != tl(sF4)
| spl6_29 ),
inference(avatar_component_clause,[],[f647]) ).
fof(f650,plain,
( ~ spl6_27
| ~ spl6_29
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| spl6_18 ),
inference(avatar_split_clause,[],[f645,f505,f326,f322,f276,f647,f637]) ).
fof(f661,plain,
( tl(app(sF3,sF2)) = app(tl(sF3),sF2)
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13 ),
inference(resolution,[],[f553,f327]) ).
fof(f666,plain,
( app(tl(sF3),sF2) = tl(cons(sk6,sF2))
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13 ),
inference(forward_demodulation,[],[f661,f401]) ).
fof(f685,plain,
( sF1 = app(nil,sF0)
| ~ spl6_23 ),
inference(superposition,[],[f246,f568]) ).
fof(f686,plain,
( sF0 = sF1
| ~ spl6_16
| ~ spl6_23 ),
inference(forward_demodulation,[],[f685,f362]) ).
fof(f809,plain,
( nil != sF2
| ~ ssList(sk9)
| ~ ssList(sF1)
| nil = sF1 ),
inference(superposition,[],[f122,f248]) ).
fof(f1013,plain,
( ~ ssList(sF2)
| nil = sF2
| spl6_27 ),
inference(resolution,[],[f77,f639]) ).
fof(f1028,plain,
( nil = sF2
| ~ spl6_13
| spl6_27 ),
inference(forward_subsumption_resolution,[],[f1013,f327]) ).
fof(f1029,plain,
( $false
| ~ spl6_13
| spl6_18
| spl6_27 ),
inference(forward_subsumption_resolution,[],[f1028,f507]) ).
fof(f1030,plain,
( ~ spl6_13
| spl6_18
| spl6_27 ),
inference(avatar_contradiction_clause,[],[f1029]) ).
fof(f1031,plain,
( ~ ssList(sk9)
| ~ ssList(sF1)
| nil = sF1
| ~ spl6_18 ),
inference(forward_subsumption_resolution,[],[f809,f506]) ).
fof(f1033,plain,
( ~ ssList(sF1)
| nil = sF1
| ~ spl6_18 ),
inference(forward_subsumption_resolution,[],[f1031,f211]) ).
fof(f1035,plain,
( nil = sF1
| ~ spl6_15
| ~ spl6_18 ),
inference(forward_subsumption_resolution,[],[f1033,f338]) ).
fof(f1038,plain,
( $false
| ~ spl6_4
| ~ spl6_15
| ~ spl6_16
| ~ spl6_18 ),
inference(forward_subsumption_resolution,[],[f1035,f509]) ).
fof(f1039,plain,
( ~ spl6_4
| ~ spl6_15
| ~ spl6_16
| ~ spl6_18 ),
inference(avatar_contradiction_clause,[],[f1038]) ).
fof(f1503,definition,
( spl6_42
<=> ssList(tl(sk7)) ),
introduced(definition,[new_symbols(definition,[spl6_42])],[avatar_definition]) ).
fof(f1504,plain,
( ssList(tl(sk7))
| ~ spl6_42 ),
inference(avatar_component_clause,[],[f1503]) ).
fof(f1505,plain,
( ~ ssList(tl(sk7))
| spl6_42 ),
inference(avatar_component_clause,[],[f1503]) ).
fof(f1512,plain,
( ~ ssList(sk7)
| nil = sk7
| spl6_42 ),
inference(resolution,[],[f1505,f77]) ).
fof(f1513,plain,
( nil = sk7
| spl6_42 ),
inference(forward_subsumption_resolution,[],[f1512,f209]) ).
fof(f1514,plain,
( $false
| spl6_23
| spl6_42 ),
inference(forward_subsumption_resolution,[],[f1513,f567]) ).
fof(f1515,plain,
( spl6_23
| spl6_42 ),
inference(avatar_contradiction_clause,[],[f1514]) ).
fof(f1718,definition,
( spl6_50
<=> ssList(tl(sF3)) ),
introduced(definition,[new_symbols(definition,[spl6_50])],[avatar_definition]) ).
fof(f1719,plain,
( ssList(tl(sF3))
| ~ spl6_50 ),
inference(avatar_component_clause,[],[f1718]) ).
fof(f1720,plain,
( ~ ssList(tl(sF3))
| spl6_50 ),
inference(avatar_component_clause,[],[f1718]) ).
fof(f1741,plain,
( ~ ssList(sF3)
| nil = sF3
| spl6_50 ),
inference(resolution,[],[f1720,f77]) ).
fof(f1742,plain,
( nil = sF3
| ~ spl6_12
| spl6_50 ),
inference(forward_subsumption_resolution,[],[f1741,f323]) ).
fof(f1743,plain,
( $false
| ~ spl6_4
| ~ spl6_12
| spl6_50 ),
inference(forward_subsumption_resolution,[],[f1742,f433]) ).
fof(f1744,plain,
( ~ spl6_4
| ~ spl6_12
| spl6_50 ),
inference(avatar_contradiction_clause,[],[f1743]) ).
fof(f2030,plain,
( tl(sk3) = app(tl(sF4),sk8)
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14 ),
inference(forward_demodulation,[],[f593,f313]) ).
fof(f2097,plain,
( nil != tl(sk3)
| ~ ssList(sk8)
| ~ ssList(tl(sF4))
| nil = sk8
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14 ),
inference(superposition,[],[f124,f2030]) ).
fof(f2098,plain,
( ssList(tl(sk3))
| ~ ssList(tl(sF4))
| ~ ssList(sk8)
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14 ),
inference(superposition,[],[f85,f2030]) ).
fof(f2099,plain,
( ssList(tl(sk3))
| ~ ssList(sk8)
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14
| ~ spl6_28 ),
inference(forward_subsumption_resolution,[],[f2098,f643]) ).
fof(f2100,plain,
( nil != tl(sk3)
| ~ ssList(tl(sF4))
| nil = sk8
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14 ),
inference(forward_subsumption_resolution,[],[f2097,f210]) ).
fof(f2103,plain,
( ssList(tl(sk3))
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14
| ~ spl6_28 ),
inference(forward_subsumption_resolution,[],[f2099,f210]) ).
fof(f2104,plain,
( nil != tl(sk3)
| nil = sk8
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14
| ~ spl6_28 ),
inference(forward_subsumption_resolution,[],[f2100,f643]) ).
fof(f2107,plain,
( nil != tl(sk3)
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14
| spl6_19
| ~ spl6_28 ),
inference(forward_subsumption_resolution,[],[f2104,f520]) ).
fof(f4660,definition,
( spl6_149
<=> ssList(app(sk8,sk7)) ),
introduced(definition,[new_symbols(definition,[spl6_149])],[avatar_definition]) ).
fof(f4661,plain,
( ssList(app(sk8,sk7))
| ~ spl6_149 ),
inference(avatar_component_clause,[],[f4660]) ).
fof(f4662,plain,
( ~ ssList(app(sk8,sk7))
| spl6_149 ),
inference(avatar_component_clause,[],[f4660]) ).
fof(f4688,plain,
( ~ ssList(sk8)
| ~ ssList(sk7)
| spl6_149 ),
inference(resolution,[],[f4662,f85]) ).
fof(f4689,plain,
( ~ ssList(sk7)
| spl6_149 ),
inference(forward_subsumption_resolution,[],[f4688,f210]) ).
fof(f4690,plain,
( $false
| spl6_149 ),
inference(forward_subsumption_resolution,[],[f4689,f209]) ).
fof(f4691,plain,
spl6_149,
inference(avatar_contradiction_clause,[],[f4690]) ).
fof(f4818,plain,
( sF2 = tl(cons(sk6,sF2))
| ~ spl6_13 ),
inference(resolution,[],[f538,f327]) ).
fof(f5602,definition,
( spl6_198
<=> sF0 = sF1 ),
introduced(definition,[new_symbols(definition,[spl6_198])],[avatar_definition]) ).
fof(f5603,plain,
( sF0 != sF1
| spl6_198 ),
inference(avatar_component_clause,[],[f5602]) ).
fof(f5604,plain,
( sF0 = sF1
| ~ spl6_198 ),
inference(avatar_component_clause,[],[f5602]) ).
fof(f5606,definition,
( spl6_199
<=> sF2 = cons(sk5,sk9) ),
introduced(definition,[new_symbols(definition,[spl6_199])],[avatar_definition]) ).
fof(f5607,plain,
( sF2 = cons(sk5,sk9)
| ~ spl6_199 ),
inference(avatar_component_clause,[],[f5606]) ).
fof(f5608,plain,
( sF2 != cons(sk5,sk9)
| spl6_199 ),
inference(avatar_component_clause,[],[f5606]) ).
fof(f5912,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| nil = sk3 ),
inference(resolution,[],[f107,f202]) ).
fof(f5914,plain,
( sk7 = cons(hd(sk7),tl(sk7))
| nil = sk7 ),
inference(resolution,[],[f107,f209]) ).
fof(f5929,plain,
( sk7 = cons(hd(sk7),tl(sk7))
| spl6_23 ),
inference(forward_subsumption_resolution,[],[f5914,f567]) ).
fof(f5931,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| spl6_20 ),
inference(forward_subsumption_resolution,[],[f5912,f525]) ).
fof(f6116,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,sk7),cons(hd(sk7),X1)))
| ~ ssList(tl(sk7))
| ~ ssList(X0)
| ~ ssItem(hd(sk7))
| ~ duplicatefreeP(app(app(X0,sk7),cons(hd(sk7),X1)))
| ~ ssList(X1) )
| spl6_23 ),
inference(superposition,[],[f236,f5929]) ).
fof(f6119,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,sk7),cons(hd(sk7),X1)))
| ~ ssList(X0)
| ~ ssItem(hd(sk7))
| ~ duplicatefreeP(app(app(X0,sk7),cons(hd(sk7),X1)))
| ~ ssList(X1) )
| spl6_23
| ~ spl6_42 ),
inference(forward_subsumption_resolution,[],[f6116,f1504]) ).
fof(f7808,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk3
| ~ ssItem(skaf44(sk3))
| ~ ssItem(X0)
| ~ ssList(nil)
| ~ ssList(X1)
| nil = X1 )
| ~ spl6_2 ),
inference(superposition,[],[f185,f528]) ).
fof(f7817,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk3
| ~ ssItem(X0)
| ~ ssList(nil)
| ~ ssList(X1)
| nil = X1 )
| ~ spl6_2 ),
inference(forward_subsumption_resolution,[],[f7808,f47]) ).
fof(f7829,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk3
| ~ ssItem(X0)
| ~ ssList(X1)
| nil = X1 )
| ~ spl6_2
| ~ spl6_4 ),
inference(forward_subsumption_resolution,[],[f7817,f277]) ).
fof(f7841,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk3
| ~ ssList(X1)
| nil = X1 )
| ~ spl6_2
| ~ spl6_4
| ~ spl6_10 ),
inference(forward_subsumption_resolution,[],[f7829,f305]) ).
fof(f11780,plain,
( sk3 != sk3
| ~ ssList(tl(sk3))
| nil = tl(sk3)
| ~ spl6_2
| ~ spl6_4
| ~ spl6_10
| spl6_20 ),
inference(superposition,[],[f7841,f5931]) ).
fof(f11787,plain,
( ~ ssList(tl(sk3))
| nil = tl(sk3)
| ~ spl6_2
| ~ spl6_4
| ~ spl6_10
| spl6_20 ),
inference(trivial_inequality_removal,[],[f11780]) ).
fof(f11789,plain,
( nil = tl(sk3)
| ~ spl6_2
| ~ spl6_4
| ~ spl6_10
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14
| spl6_20
| ~ spl6_28 ),
inference(forward_subsumption_resolution,[],[f11787,f2103]) ).
fof(f11799,plain,
( $false
| ~ spl6_2
| ~ spl6_4
| ~ spl6_10
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14
| spl6_19
| spl6_20
| ~ spl6_28 ),
inference(forward_subsumption_resolution,[],[f11789,f2107]) ).
fof(f11800,plain,
( ~ spl6_2
| ~ spl6_4
| ~ spl6_10
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14
| spl6_19
| spl6_20
| ~ spl6_28 ),
inference(avatar_contradiction_clause,[],[f11799]) ).
fof(f11820,plain,
( nil = tl(sF4)
| ~ spl6_2
| ~ spl6_4
| ~ spl6_10
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14
| ~ spl6_19
| spl6_20
| ~ spl6_28 ),
inference(forward_demodulation,[],[f11789,f586]) ).
fof(f11823,plain,
( $false
| ~ spl6_2
| ~ spl6_4
| ~ spl6_10
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14
| ~ spl6_19
| spl6_20
| ~ spl6_28
| spl6_29 ),
inference(forward_subsumption_resolution,[],[f11820,f649]) ).
fof(f11824,plain,
( ~ spl6_2
| ~ spl6_4
| ~ spl6_10
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14
| ~ spl6_19
| spl6_20
| ~ spl6_28
| spl6_29 ),
inference(avatar_contradiction_clause,[],[f11823]) ).
fof(f11826,plain,
( nil = sF4
| ~ spl6_14
| ~ spl6_19
| ~ spl6_20 ),
inference(forward_demodulation,[],[f524,f586]) ).
fof(f11849,plain,
( $false
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14
| ~ spl6_19
| ~ spl6_20 ),
inference(forward_subsumption_resolution,[],[f11826,f499]) ).
fof(f11850,plain,
( ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14
| ~ spl6_19
| ~ spl6_20 ),
inference(avatar_contradiction_clause,[],[f11849]) ).
fof(f11917,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,sk7),cons(hd(sk7),X1)))
| ~ ssList(X0)
| ~ ssItem(hd(sk7))
| ~ ssList(X1) )
| ~ spl6_11
| spl6_23
| ~ spl6_42 ),
inference(forward_subsumption_resolution,[],[f6119,f308]) ).
fof(f11966,definition,
( spl6_312
<=> ssItem(hd(sk7)) ),
introduced(definition,[new_symbols(definition,[spl6_312])],[avatar_definition]) ).
fof(f11967,plain,
( ssItem(hd(sk7))
| ~ spl6_312 ),
inference(avatar_component_clause,[],[f11966]) ).
fof(f11968,plain,
( ~ ssItem(hd(sk7))
| spl6_312 ),
inference(avatar_component_clause,[],[f11966]) ).
fof(f12002,definition,
( spl6_317
<=> ! [X0,X1] :
( ~ ssList(app(app(X0,sk7),cons(hd(sk7),X1)))
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[spl6_317])],[avatar_definition]) ).
fof(f12003,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,sk7),cons(hd(sk7),X1)))
| ~ ssList(X1)
| ~ ssList(X0) )
| ~ spl6_317 ),
inference(avatar_component_clause,[],[f12002]) ).
fof(f12004,plain,
( ~ spl6_312
| spl6_317
| ~ spl6_11
| spl6_23
| ~ spl6_42 ),
inference(avatar_split_clause,[],[f11917,f1503,f566,f307,f12002,f11966]) ).
fof(f12223,plain,
( ~ ssList(sk7)
| nil = sk7
| spl6_312 ),
inference(resolution,[],[f11968,f78]) ).
fof(f12224,plain,
( nil = sk7
| spl6_312 ),
inference(forward_subsumption_resolution,[],[f12223,f209]) ).
fof(f12225,plain,
( $false
| spl6_23
| spl6_312 ),
inference(forward_subsumption_resolution,[],[f12224,f567]) ).
fof(f12226,plain,
( spl6_23
| spl6_312 ),
inference(avatar_contradiction_clause,[],[f12225]) ).
fof(f12699,plain,
( ! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(X1,sk7))
| ~ ssList(cons(hd(sk7),X0)) )
| ~ spl6_317 ),
inference(resolution,[],[f12003,f85]) ).
fof(f12729,definition,
( spl6_325
<=> ! [X1] :
( ~ ssList(X1)
| ~ ssList(app(X1,sk7)) ) ),
introduced(definition,[new_symbols(definition,[spl6_325])],[avatar_definition]) ).
fof(f12730,plain,
( ! [X1] :
( ~ ssList(app(X1,sk7))
| ~ ssList(X1) )
| ~ spl6_325 ),
inference(avatar_component_clause,[],[f12729]) ).
fof(f12732,definition,
( spl6_326
<=> ! [X0] :
( ~ ssList(X0)
| ~ ssList(cons(hd(sk7),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl6_326])],[avatar_definition]) ).
fof(f12733,plain,
( ! [X0] :
( ~ ssList(cons(hd(sk7),X0))
| ~ ssList(X0) )
| ~ spl6_326 ),
inference(avatar_component_clause,[],[f12732]) ).
fof(f12734,plain,
( spl6_325
| spl6_326
| ~ spl6_317 ),
inference(avatar_split_clause,[],[f12699,f12002,f12732,f12729]) ).
fof(f12744,plain,
( ! [X0] :
( ~ ssList(X0)
| ~ ssList(X0)
| ~ ssItem(hd(sk7)) )
| ~ spl6_326 ),
inference(resolution,[],[f12733,f86]) ).
fof(f12747,plain,
( ! [X0] :
( ~ ssList(X0)
| ~ ssItem(hd(sk7)) )
| ~ spl6_326 ),
inference(duplicate_literal_removal,[],[f12744]) ).
fof(f12750,plain,
( ! [X0] : ~ ssList(X0)
| ~ spl6_312
| ~ spl6_326 ),
inference(forward_subsumption_resolution,[],[f12747,f11967]) ).
fof(f12757,plain,
( ~ ssList(sk8)
| ~ spl6_149
| ~ spl6_325 ),
inference(resolution,[],[f12730,f4661]) ).
fof(f12789,plain,
( $false
| ~ spl6_149
| ~ spl6_325 ),
inference(forward_subsumption_resolution,[],[f12757,f210]) ).
fof(f12790,plain,
( ~ spl6_149
| ~ spl6_325 ),
inference(avatar_contradiction_clause,[],[f12789]) ).
fof(f12816,plain,
( $false
| ~ spl6_16
| ~ spl6_23
| spl6_198 ),
inference(forward_subsumption_resolution,[],[f686,f5603]) ).
fof(f12817,plain,
( ~ spl6_16
| ~ spl6_23
| spl6_198 ),
inference(avatar_contradiction_clause,[],[f12816]) ).
fof(f12896,plain,
( $false
| ~ spl6_4
| ~ spl6_312
| ~ spl6_326 ),
inference(resolution,[],[f12750,f277]) ).
fof(f12994,plain,
( ~ spl6_4
| ~ spl6_312
| ~ spl6_326 ),
inference(avatar_contradiction_clause,[],[f12896]) ).
fof(f13125,plain,
( sF2 = app(sF0,sk9)
| ~ spl6_198 ),
inference(superposition,[],[f248,f5604]) ).
fof(f13175,plain,
( sF2 = cons(sk5,sk9)
| ~ spl6_198 ),
inference(forward_demodulation,[],[f13125,f414]) ).
fof(f13191,plain,
( $false
| ~ spl6_198
| spl6_199 ),
inference(forward_subsumption_resolution,[],[f13175,f5608]) ).
fof(f13192,plain,
( ~ spl6_198
| spl6_199 ),
inference(avatar_contradiction_clause,[],[f13191]) ).
fof(f16991,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,sF2),cons(sk5,X1)))
| ~ ssList(sk9)
| ~ ssList(X0)
| ~ ssItem(sk5)
| ~ duplicatefreeP(app(app(X0,sF2),cons(sk5,X1)))
| ~ ssList(X1) )
| ~ spl6_199 ),
inference(superposition,[],[f236,f5607]) ).
fof(f17006,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,sF2),cons(sk5,X1)))
| ~ ssList(sk9)
| ~ ssList(X0)
| ~ ssItem(sk5)
| ~ ssList(X1) )
| ~ spl6_11
| ~ spl6_199 ),
inference(forward_subsumption_resolution,[],[f16991,f308]) ).
fof(f17021,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,sF2),cons(sk5,X1)))
| ~ ssList(X0)
| ~ ssItem(sk5)
| ~ ssList(X1) )
| ~ spl6_11
| ~ spl6_199 ),
inference(forward_subsumption_resolution,[],[f17006,f211]) ).
fof(f17032,plain,
( ! [X0,X1] :
( ~ ssList(app(app(X0,sF2),cons(sk5,X1)))
| ~ ssList(X0)
| ~ ssList(X1) )
| ~ spl6_11
| ~ spl6_199 ),
inference(forward_subsumption_resolution,[],[f17021,f207]) ).
fof(f17039,plain,
( ! [X0] :
( ~ ssList(app(tl(cons(sk6,sF2)),cons(sk5,X0)))
| ~ ssList(tl(sF3))
| ~ ssList(X0) )
| ~ spl6_4
| ~ spl6_11
| ~ spl6_12
| ~ spl6_13
| ~ spl6_199 ),
inference(superposition,[],[f17032,f666]) ).
fof(f17044,plain,
( ! [X0] :
( ~ ssList(app(tl(cons(sk6,sF2)),cons(sk5,X0)))
| ~ ssList(X0) )
| ~ spl6_4
| ~ spl6_11
| ~ spl6_12
| ~ spl6_13
| ~ spl6_50
| ~ spl6_199 ),
inference(forward_subsumption_resolution,[],[f17039,f1719]) ).
fof(f17047,definition,
( spl6_365
<=> ! [X1] :
( ~ ssList(X1)
| ~ ssList(cons(sk5,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl6_365])],[avatar_definition]) ).
fof(f17048,plain,
( ! [X1] :
( ~ ssList(cons(sk5,X1))
| ~ ssList(X1) )
| ~ spl6_365 ),
inference(avatar_component_clause,[],[f17047]) ).
fof(f17053,plain,
( ! [X0] :
( ~ ssList(app(sF2,cons(sk5,X0)))
| ~ ssList(X0) )
| ~ spl6_4
| ~ spl6_11
| ~ spl6_12
| ~ spl6_13
| ~ spl6_50
| ~ spl6_199 ),
inference(forward_demodulation,[],[f17044,f4818]) ).
fof(f17055,plain,
( ! [X0] :
( ~ ssList(X0)
| ~ ssList(sF2)
| ~ ssList(cons(sk5,X0)) )
| ~ spl6_4
| ~ spl6_11
| ~ spl6_12
| ~ spl6_13
| ~ spl6_50
| ~ spl6_199 ),
inference(resolution,[],[f17053,f85]) ).
fof(f17059,plain,
( ! [X0] :
( ~ ssList(X0)
| ~ ssList(cons(sk5,X0)) )
| ~ spl6_4
| ~ spl6_11
| ~ spl6_12
| ~ spl6_13
| ~ spl6_50
| ~ spl6_199 ),
inference(forward_subsumption_resolution,[],[f17055,f327]) ).
fof(f17061,plain,
( spl6_365
| ~ spl6_4
| ~ spl6_11
| ~ spl6_12
| ~ spl6_13
| ~ spl6_50
| ~ spl6_199 ),
inference(avatar_split_clause,[],[f17059,f5606,f1718,f326,f322,f307,f276,f17047]) ).
fof(f17063,plain,
( ~ ssList(sF0)
| ~ ssList(nil)
| ~ spl6_365 ),
inference(superposition,[],[f17048,f244]) ).
fof(f17067,plain,
( ~ ssList(nil)
| ~ spl6_16
| ~ spl6_365 ),
inference(forward_subsumption_resolution,[],[f17063,f343]) ).
fof(f17071,plain,
( $false
| ~ spl6_4
| ~ spl6_16
| ~ spl6_365 ),
inference(forward_subsumption_resolution,[],[f17067,f277]) ).
fof(f17072,plain,
( ~ spl6_4
| ~ spl6_16
| ~ spl6_365 ),
inference(avatar_contradiction_clause,[],[f17071]) ).
cnf(s1,plain,
( ~ spl6_1
| spl6_2 ),
inference(sat_conversion,[],[f270]) ).
cnf(s8,plain,
( spl6_10
| spl6_11 ),
inference(sat_conversion,[],[f309]) ).
cnf(s11,plain,
spl6_4,
inference(sat_conversion,[],[f312]) ).
cnf(s12,plain,
( ~ spl6_12
| ~ spl6_13
| spl6_14 ),
inference(sat_conversion,[],[f333]) ).
cnf(s13,plain,
( spl6_13
| ~ spl6_15 ),
inference(sat_conversion,[],[f340]) ).
cnf(s14,plain,
( spl6_15
| ~ spl6_16 ),
inference(sat_conversion,[],[f345]) ).
cnf(s15,plain,
( ~ spl6_4
| spl6_12 ),
inference(sat_conversion,[],[f353]) ).
cnf(s16,plain,
( ~ spl6_4
| spl6_16 ),
inference(sat_conversion,[],[f355]) ).
cnf(s18,plain,
( spl6_1
| ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14 ),
inference(sat_conversion,[],[f515]) ).
cnf(s19,plain,
( ~ spl6_14
| spl6_19
| ~ spl6_20 ),
inference(sat_conversion,[],[f526]) ).
cnf(s24,plain,
( ~ spl6_12
| ~ spl6_13
| spl6_18
| ~ spl6_27
| spl6_28 ),
inference(sat_conversion,[],[f644]) ).
cnf(s25,plain,
( ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| spl6_18
| ~ spl6_27
| ~ spl6_29 ),
inference(sat_conversion,[],[f650]) ).
cnf(s30,plain,
( ~ spl6_13
| spl6_18
| spl6_27 ),
inference(sat_conversion,[],[f1030]) ).
cnf(s32,plain,
( ~ spl6_4
| ~ spl6_15
| ~ spl6_16
| ~ spl6_18 ),
inference(sat_conversion,[],[f1039]) ).
cnf(s47,plain,
( spl6_23
| spl6_42 ),
inference(sat_conversion,[],[f1515]) ).
cnf(s58,plain,
( ~ spl6_4
| ~ spl6_12
| spl6_50 ),
inference(sat_conversion,[],[f1744]) ).
cnf(s174,plain,
spl6_149,
inference(sat_conversion,[],[f4691]) ).
cnf(s317,plain,
( ~ spl6_2
| ~ spl6_4
| ~ spl6_10
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14
| spl6_19
| spl6_20
| ~ spl6_28 ),
inference(sat_conversion,[],[f11800]) ).
cnf(s318,plain,
( ~ spl6_2
| ~ spl6_4
| ~ spl6_10
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14
| ~ spl6_19
| spl6_20
| ~ spl6_28
| spl6_29 ),
inference(sat_conversion,[],[f11824]) ).
cnf(s319,plain,
( ~ spl6_4
| ~ spl6_12
| ~ spl6_13
| ~ spl6_14
| ~ spl6_19
| ~ spl6_20 ),
inference(sat_conversion,[],[f11850]) ).
cnf(s323,plain,
( ~ spl6_11
| spl6_23
| ~ spl6_42
| ~ spl6_312
| spl6_317 ),
inference(sat_conversion,[],[f12004]) ).
cnf(s335,plain,
( spl6_23
| spl6_312 ),
inference(sat_conversion,[],[f12226]) ).
cnf(s341,plain,
( ~ spl6_317
| spl6_325
| spl6_326 ),
inference(sat_conversion,[],[f12734]) ).
cnf(s346,plain,
( ~ spl6_149
| ~ spl6_325 ),
inference(sat_conversion,[],[f12790]) ).
cnf(s358,plain,
( ~ spl6_16
| ~ spl6_23
| spl6_198 ),
inference(sat_conversion,[],[f12817]) ).
cnf(s408,plain,
( ~ spl6_4
| ~ spl6_312
| ~ spl6_326 ),
inference(sat_conversion,[],[f12994]) ).
cnf(s411,plain,
( ~ spl6_198
| spl6_199 ),
inference(sat_conversion,[],[f13192]) ).
cnf(s477,plain,
( ~ spl6_4
| ~ spl6_11
| ~ spl6_12
| ~ spl6_13
| ~ spl6_50
| ~ spl6_199
| spl6_365 ),
inference(sat_conversion,[],[f17061]) ).
cnf(s479,plain,
( ~ spl6_4
| ~ spl6_16
| ~ spl6_365 ),
inference(sat_conversion,[],[f17072]) ).
cnf(s480,plain,
~ spl6_325,
inference(rat,[],[s346,s174]) ).
cnf(s501,plain,
spl6_16,
inference(rat,[],[s16,s11]) ).
cnf(s502,plain,
spl6_12,
inference(rat,[],[s15,s11]) ).
cnf(s503,plain,
~ spl6_365,
inference(rat,[],[s479,s11,s501]) ).
cnf(s512,plain,
spl6_15,
inference(rat,[],[s14,s501]) ).
cnf(s518,plain,
spl6_50,
inference(rat,[],[s58,s11,s502]) ).
cnf(s539,plain,
~ spl6_18,
inference(rat,[],[s32,s501,s11,s512]) ).
cnf(s540,plain,
spl6_13,
inference(rat,[],[s13,s512]) ).
cnf(s563,plain,
spl6_27,
inference(rat,[],[s30,s539,s540]) ).
cnf(s564,plain,
spl6_14,
inference(rat,[],[s12,s502,s540]) ).
cnf(s565,plain,
spl6_1,
inference(rat,[],[s18,s564,s502,s11,s540]) ).
cnf(s572,plain,
~ spl6_29,
inference(rat,[],[s25,s540,s539,s502,s11,s563]) ).
cnf(s573,plain,
spl6_28,
inference(rat,[],[s24,s540,s539,s502,s563]) ).
cnf(s603,plain,
spl6_2,
inference(rat,[],[s1,s565]) ).
cnf(s604,plain,
~ spl6_11,
inference(rat,[],[s341,s323,s408,s47,s335,s358,s411,s477,s480,s11,s501,s502,s518,s540,s503]) ).
cnf(s605,plain,
spl6_10,
inference(rat,[],[s8,s604]) ).
cnf(s606,plain,
spl6_19,
inference(rat,[],[s317,s19,s11,s502,s540,s564,s603,s605,s573]) ).
cnf(s607,plain,
~ spl6_20,
inference(rat,[],[s319,s564,s540,s502,s11,s606]) ).
cnf(s609,plain,
$false,
inference(rat,[],[s318,s572,s573,s605,s603,s564,s540,s502,s11,s607,s606]) ).
fof(f17073,plain,
$false,
inference(avatar_sat_refutation,[],[s609]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC197-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n026.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 28 08:27:42 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.33/2.15 % (3695616)Input is clausal, will run a generic CNF schedule.
% 9.33/2.15 % (3695621)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3601742736:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.33/2.15 % (3695622)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2968116747:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.33/2.15 % (3695627)dis-21_1_sil=8000:lcm=predicate:random_seed=3779359333:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 9.33/2.15 % (3695624)lrs+10_1_sil=8000:sp=occurrence:random_seed=3310988058:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.33/2.15 % (3695626)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4089365223:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.33/2.15 % (3695623)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=915810556:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.33/2.15 % (3695625)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2587071863:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.33/2.15 % (3695627)Instruction limit reached!
% 9.33/2.15 % (3695627)------------------------------
% 9.33/2.15 % (3695627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.33/2.15 % (3695627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.33/2.15 % (3695627)CaDiCaL version: 2.1.3
% 9.33/2.15 % (3695627)Termination reason: Instruction limit
% 9.33/2.15 % (3695627)Termination phase: Saturation
% 9.33/2.15 % (3695627)Time elapsed: 0.064 s
% 9.33/2.15 % (3695627)Peak memory usage: 90 MB
% 9.33/2.15 % (3695627)Instructions burned: 118 (million)
% 9.33/2.15 % (3695624)Instruction limit reached!
% 9.33/2.15 % (3695624)------------------------------
% 9.33/2.15 % (3695624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.33/2.15 % (3695624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.33/2.15 % (3695624)CaDiCaL version: 2.1.3
% 9.33/2.15 % (3695624)Termination reason: Instruction limit
% 9.33/2.15 % (3695624)Termination phase: Saturation
% 9.33/2.15 % (3695624)Time elapsed: 0.066 s
% 9.33/2.15 % (3695624)Peak memory usage: 90 MB
% 9.33/2.15 % (3695624)Instructions burned: 108 (million)
% 9.33/2.15 % (3695625)Instruction limit reached!
% 9.33/2.15 % (3695625)------------------------------
% 9.33/2.15 % (3695625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.33/2.15 % (3695625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.33/2.15 % (3695625)CaDiCaL version: 2.1.3
% 9.33/2.15 % (3695625)Termination reason: Instruction limit
% 9.33/2.15 % (3695625)Termination phase: Saturation
% 9.33/2.15 % (3695625)Time elapsed: 0.068 s
% 9.33/2.15 % (3695625)Peak memory usage: 89 MB
% 9.33/2.15 % (3695625)Instructions burned: 114 (million)
% 9.33/2.15 % (3695626)Instruction limit reached!
% 9.33/2.15 % (3695626)------------------------------
% 9.33/2.15 % (3695626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.33/2.15 % (3695626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.33/2.15 % (3695626)CaDiCaL version: 2.1.3
% 9.33/2.15 % (3695626)Termination reason: Instruction limit
% 9.33/2.15 % (3695626)Termination phase: Saturation
% 9.33/2.15 % (3695626)Time elapsed: 0.118 s
% 9.33/2.15 % (3695626)Peak memory usage: 90 MB
% 9.33/2.15 % (3695626)Instructions burned: 181 (million)
% 9.33/2.15 % (3695636)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2641982141:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 9.33/2.15 % (3695637)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1158097522:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 9.33/2.15 % (3695635)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=53378300:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 9.33/2.15 % (3695638)lrs+10_64_to=lpo:sil=8000:random_seed=3930694977:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 9.33/2.15 % (3695635)Instruction limit reached!
% 13.91/2.99 % (3695635)------------------------------
% 13.91/2.99 % (3695635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/2.99 % (3695635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.99 % (3695635)CaDiCaL version: 2.1.3
% 13.91/2.99 % (3695635)Termination reason: Instruction limit
% 13.91/2.99 % (3695635)Termination phase: Saturation
% 13.91/2.99 % (3695635)Time elapsed: 0.090 s
% 13.91/2.99 % (3695635)Peak memory usage: 89 MB
% 13.91/2.99 % (3695635)Instructions burned: 143 (million)
% 13.91/2.99 % (3695636)Instruction limit reached!
% 13.91/2.99 % (3695636)------------------------------
% 13.91/2.99 % (3695636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/2.99 % (3695636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.99 % (3695636)CaDiCaL version: 2.1.3
% 13.91/2.99 % (3695636)Termination reason: Instruction limit
% 13.91/2.99 % (3695636)Termination phase: Saturation
% 13.91/2.99 % (3695636)Time elapsed: 0.100 s
% 13.91/2.99 % (3695636)Peak memory usage: 90 MB
% 13.91/2.99 % (3695636)Instructions burned: 190 (million)
% 13.91/2.99 % (3695638)Instruction limit reached!
% 13.91/2.99 % (3695638)------------------------------
% 13.91/2.99 % (3695638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/2.99 % (3695638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.99 % (3695638)CaDiCaL version: 2.1.3
% 13.91/2.99 % (3695638)Termination reason: Instruction limit
% 13.91/2.99 % (3695638)Termination phase: Saturation
% 13.91/2.99 % (3695638)Time elapsed: 0.064 s
% 13.91/2.99 % (3695638)Peak memory usage: 90 MB
% 13.91/2.99 % (3695638)Instructions burned: 126 (million)
% 13.91/2.99 % (3695637)Instruction limit reached!
% 13.91/2.99 % (3695637)------------------------------
% 13.91/2.99 % (3695637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/2.99 % (3695637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.99 % (3695637)CaDiCaL version: 2.1.3
% 13.91/2.99 % (3695637)Termination reason: Instruction limit
% 13.91/2.99 % (3695637)Termination phase: Saturation
% 13.91/2.99 % (3695637)Time elapsed: 0.130 s
% 13.91/2.99 % (3695637)Peak memory usage: 90 MB
% 13.91/2.99 % (3695637)Instructions burned: 221 (million)
% 13.91/2.99 % (3695643)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=19366745:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 13.91/2.99 % (3695644)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3551958980:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 13.91/2.99 % (3695645)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1466011013:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 13.91/2.99 % (3695643)Instruction limit reached!
% 13.91/2.99 % (3695643)------------------------------
% 13.91/2.99 % (3695643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/2.99 % (3695643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.99 % (3695643)CaDiCaL version: 2.1.3
% 13.91/2.99 % (3695643)Termination reason: Instruction limit
% 13.91/2.99 % (3695643)Termination phase: Saturation
% 13.91/2.99 % (3695643)Time elapsed: 0.065 s
% 13.91/2.99 % (3695643)Peak memory usage: 90 MB
% 13.91/2.99 % (3695643)Instructions burned: 194 (million)
% 13.91/2.99 % (3695646)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=325506768:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 13.91/2.99 % (3695644)Instruction limit reached!
% 13.91/2.99 % (3695644)------------------------------
% 13.91/2.99 % (3695644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/2.99 % (3695644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.99 % (3695644)CaDiCaL version: 2.1.3
% 13.91/2.99 % (3695644)Termination reason: Instruction limit
% 13.91/2.99 % (3695644)Termination phase: Saturation
% 13.91/2.99 % (3695644)Time elapsed: 0.094 s
% 13.91/2.99 % (3695644)Peak memory usage: 92 MB
% 13.91/2.99 % (3695644)Instructions burned: 158 (million)
% 13.91/2.99 % (3695646)Instruction limit reached!
% 13.91/2.99 % (3695646)------------------------------
% 13.91/2.99 % (3695646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/2.99 % (3695646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.99 % (3695646)CaDiCaL version: 2.1.3
% 13.91/2.99 % (3695646)Termination reason: Instruction limit
% 13.91/2.99 % (3695646)Termination phase: Saturation
% 13.91/2.99 % (3695646)Time elapsed: 0.057 s
% 13.91/2.99 % (3695646)Peak memory usage: 90 MB
% 13.91/2.99 % (3695646)Instructions burned: 107 (million)
% 13.91/2.99 % (3695650)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3573470775:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 13.91/2.99 % (3695650)Instruction limit reached!
% 13.91/2.99 % (3695650)------------------------------
% 13.91/2.99 % (3695650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/2.99 % (3695650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.99 % (3695650)CaDiCaL version: 2.1.3
% 13.91/2.99 % (3695650)Termination reason: Instruction limit
% 13.91/2.99 % (3695650)Termination phase: Saturation
% 13.91/2.99 % (3695650)Time elapsed: 0.034 s
% 13.91/2.99 % (3695650)Peak memory usage: 90 MB
% 13.91/2.99 % (3695650)Instructions burned: 108 (million)
% 13.91/2.99 % (3695653)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4017790331:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 13.91/2.99 % (3695652)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3234972998:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 13.91/2.99 % (3695655)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4143597246:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 13.91/2.99 % (3695655)Instruction limit reached!
% 13.91/2.99 % (3695655)------------------------------
% 13.91/2.99 % (3695655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/2.99 % (3695655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.99 % (3695655)CaDiCaL version: 2.1.3
% 13.91/2.99 % (3695655)Termination reason: Instruction limit
% 13.91/2.99 % (3695655)Termination phase: Saturation
% 13.91/2.99 % (3695655)Time elapsed: 0.048 s
% 13.91/2.99 % (3695655)Peak memory usage: 90 MB
% 13.91/2.99 % (3695655)Instructions burned: 136 (million)
% 13.91/2.99 % (3695652)Instruction limit reached!
% 13.91/2.99 % (3695652)------------------------------
% 13.91/2.99 % (3695652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/2.99 % (3695652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.99 % (3695652)CaDiCaL version: 2.1.3
% 13.91/2.99 % (3695652)Termination reason: Instruction limit
% 13.91/2.99 % (3695652)Termination phase: Saturation
% 13.91/2.99 % (3695652)Time elapsed: 0.156 s
% 13.91/2.99 % (3695652)Peak memory usage: 90 MB
% 13.91/2.99 % (3695652)Instructions burned: 243 (million)
% 13.91/2.99 % (3695659)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2350957910:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 13.91/2.99 % (3695660)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3413318723:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 13.91/2.99 % (3695659)Instruction limit reached!
% 13.91/2.99 % (3695659)------------------------------
% 13.91/2.99 % (3695659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/2.99 % (3695659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.99 % (3695659)CaDiCaL version: 2.1.3
% 13.91/2.99 % (3695659)Termination reason: Instruction limit
% 13.91/2.99 % (3695659)Termination phase: Saturation
% 13.91/2.99 % (3695659)Time elapsed: 0.139 s
% 13.91/2.99 % (3695659)Peak memory usage: 103 MB
% 13.91/2.99 % (3695659)Instructions burned: 500 (million)
% 13.91/2.99 % (3695660)Instruction limit reached!
% 13.91/2.99 % (3695660)------------------------------
% 13.91/2.99 % (3695660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/2.99 % (3695660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.99 % (3695660)CaDiCaL version: 2.1.3
% 13.91/2.99 % (3695660)Termination reason: Instruction limit
% 13.91/2.99 % (3695660)Termination phase: Saturation
% 13.91/2.99 % (3695660)Time elapsed: 0.104 s
% 13.91/2.99 % (3695660)Peak memory usage: 91 MB
% 13.91/2.99 % (3695660)Instructions burned: 193 (million)
% 13.91/2.99 % (3695663)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3268612694:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi)
% 13.91/2.99 % (3695663)Instruction limit reached!
% 13.91/2.99 % (3695663)------------------------------
% 13.91/2.99 % (3695663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/2.99 % (3695663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.99 % (3695663)CaDiCaL version: 2.1.3
% 13.91/2.99 % (3695663)Termination reason: Instruction limit
% 13.91/2.99 % (3695663)Termination phase: Saturation
% 13.91/2.99 % (3695663)Time elapsed: 0.075 s
% 13.91/2.99 % (3695663)Peak memory usage: 91 MB
% 13.91/2.99 % (3695663)Instructions burned: 267 (million)
% 13.91/2.99 % (3695664)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4225904105:cond=on:i=156:bs=on:gtg=exists_all:er=known_2988 on theBenchmark for (2988ds/156Mi)
% 13.91/2.99 % (3695666)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1974717117:i=3256:kws=precedence:bd=preordered:av=off_2987 on theBenchmark for (2987ds/3256Mi)
% 13.91/2.99 % (3695664)Instruction limit reached!
% 13.91/2.99 % (3695664)------------------------------
% 13.91/2.99 % (3695664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/2.99 % (3695664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.99 % (3695664)CaDiCaL version: 2.1.3
% 13.91/2.99 % (3695664)Termination reason: Instruction limit
% 13.91/2.99 % (3695664)Termination phase: Saturation
% 13.91/2.99 % (3695664)Time elapsed: 0.098 s
% 13.91/2.99 % (3695664)Peak memory usage: 90 MB
% 13.91/2.99 % (3695664)Instructions burned: 157 (million)
% 13.91/2.99 % (3695669)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=4281816003:i=537:av=off:ss=included_2985 on theBenchmark for (2985ds/537Mi)
% 13.91/2.99 % (3695621)First to succeed.
% 13.91/2.99 % (3695621)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3695616"
% 13.91/2.99 % (3695669)Instruction limit reached!
% 13.91/2.99 % (3695669)------------------------------
% 13.91/2.99 % (3695669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/2.99 % (3695669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.99 % (3695669)CaDiCaL version: 2.1.3
% 13.91/2.99 % (3695669)Termination reason: Instruction limit
% 13.91/2.99 % (3695669)Termination phase: Saturation
% 13.91/2.99 % (3695669)Time elapsed: 0.293 s
% 13.91/2.99 % (3695669)Peak memory usage: 93 MB
% 13.91/2.99 % (3695669)Instructions burned: 539 (million)
% 13.91/2.99 % (3695671)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1698235251:i=180:bd=preordered:av=off_2981 on theBenchmark for (2981ds/180Mi)
% 13.91/2.99 % (3695671)Instruction limit reached!
% 13.91/2.99 % (3695671)------------------------------
% 13.91/2.99 % (3695671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/2.99 % (3695671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.99 % (3695671)CaDiCaL version: 2.1.3
% 13.91/2.99 % (3695671)Termination reason: Instruction limit
% 13.91/2.99 % (3695671)Termination phase: Saturation
% 13.91/2.99 % (3695671)Time elapsed: 0.091 s
% 13.91/2.99 % (3695671)Peak memory usage: 91 MB
% 13.91/2.99 % (3695671)Instructions burned: 180 (million)
% 13.91/2.99 % (3695621)Refutation found. Thanks to Tanya!
% 13.91/2.99 % SZS status Unsatisfiable for theBenchmark
% 13.91/2.99 % SZS output start Proof for theBenchmark
% See solution above
% 15.65/3.19 % (3695621)------------------------------
% 15.65/3.19 % (3695621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.65/3.19 % (3695621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.65/3.19 % (3695621)CaDiCaL version: 2.1.3
% 15.65/3.19 % (3695621)Termination reason: Refutation
% 15.65/3.19 % (3695621)Time elapsed: 1.736 s
% 15.65/3.19 % (3695621)Peak memory usage: 152 MB
% 15.65/3.19 % (3695621)Instructions burned: 3220 (million)
% 15.65/3.19 % (3695621)------------------------------
% 15.65/3.19 % (3695621)------------------------------
% 15.65/3.19 % (3695616)Success in time 2.137 s
% 15.65/3.19 % Vampire exiting
%------------------------------------------------------------------------------