%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT347+4 : TPTP v9.3.1. Released v3.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 11:47:10 AM UTC 2026
% Result : Theorem 44.50s 12.91s
% Output : Refutation 65.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 17
% Syntax : Number of formulae : 122 ( 29 unt; 7 def)
% Number of atoms : 414 ( 27 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 493 ( 201 ~; 201 |; 61 &)
% ( 15 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 22 ( 20 usr; 8 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 2 con; 0-2 aty)
% Number of variables : 55 ( 0 sgn 51 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f28605,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_lattice3) ).
fof(f28681,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v1_orders_2(k7_lattice3(X0))
& l1_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_lattice3) ).
fof(f41351,axiom,
! [X0] :
( ( v2_yellow_0(X0)
& l1_orders_2(X0) )
=> ( v1_orders_2(k7_lattice3(X0))
& v1_yellow_0(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc10_yellow_7) ).
fof(f41360,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_orders_2(X0)
<=> v2_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_yellow_7) ).
fof(f41361,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v4_orders_2(X0)
<=> v4_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_yellow_7) ).
fof(f41362,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v3_orders_2(X0)
<=> v3_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_yellow_7) ).
fof(f41372,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
<=> v1_lattice3(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t16_yellow_7) ).
fof(f42383,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v1_yellow_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& v1_waybel_0(X1,k2_yellow_1(k8_waybel_0(X0)))
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(X0))))) )
=> k1_yellow_0(k2_yellow_1(k8_waybel_0(X0)),X1) = k3_tarski(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t9_waybel13) ).
fof(f44129,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& l1_orders_2(X0) )
=> k9_waybel_0(X0) = k8_waybel_0(k7_lattice3(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_waybel16) ).
fof(f45777,conjecture,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v2_yellow_0(X0)
& v2_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& v1_waybel_0(X1,k2_yellow_1(k9_waybel_0(X0)))
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(X0))))) )
=> k1_yellow_0(k2_yellow_1(k9_waybel_0(X0)),X1) = k3_tarski(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_waybel22) ).
fof(f45778,negated_conjecture,
~ ! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v2_yellow_0(X0)
& v2_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& v1_waybel_0(X1,k2_yellow_1(k9_waybel_0(X0)))
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(X0))))) )
=> k1_yellow_0(k2_yellow_1(k9_waybel_0(X0)),X1) = k3_tarski(X1) ) ),
inference(negated_conjecture,[status(cth)],[f45777]) ).
fof(f46217,plain,
? [X0] :
( ? [X1] :
( k3_tarski(X1) != k1_yellow_0(k2_yellow_1(k9_waybel_0(X0)),X1)
& ~ v1_xboole_0(X1)
& v1_waybel_0(X1,k2_yellow_1(k9_waybel_0(X0)))
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(X0))))) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v2_yellow_0(X0)
& v2_lattice3(X0)
& l1_orders_2(X0) ),
inference(ennf_transformation,[],[f45778]) ).
fof(f46218,plain,
? [X0] :
( ? [X1] :
( k3_tarski(X1) != k1_yellow_0(k2_yellow_1(k9_waybel_0(X0)),X1)
& ~ v1_xboole_0(X1)
& v1_waybel_0(X1,k2_yellow_1(k9_waybel_0(X0)))
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(X0))))) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v2_yellow_0(X0)
& v2_lattice3(X0)
& l1_orders_2(X0) ),
inference(flattening,[],[f46217]) ).
fof(f46295,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f28605]) ).
fof(f46296,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f46295]) ).
fof(f46327,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v1_yellow_0(k7_lattice3(X0)) )
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f41351]) ).
fof(f46328,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v1_yellow_0(k7_lattice3(X0)) )
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f46327]) ).
fof(f46375,plain,
! [X0] :
( ! [X1] :
( k1_yellow_0(k2_yellow_1(k8_waybel_0(X0)),X1) = k3_tarski(X1)
| v1_xboole_0(X1)
| ~ v1_waybel_0(X1,k2_yellow_1(k8_waybel_0(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(X0))))) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v1_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f42383]) ).
fof(f46376,plain,
! [X0] :
( ! [X1] :
( k1_yellow_0(k2_yellow_1(k8_waybel_0(X0)),X1) = k3_tarski(X1)
| v1_xboole_0(X1)
| ~ v1_waybel_0(X1,k2_yellow_1(k8_waybel_0(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(X0))))) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v1_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f46375]) ).
fof(f46528,plain,
! [X0] :
( k9_waybel_0(X0) = k8_waybel_0(k7_lattice3(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f44129]) ).
fof(f46529,plain,
! [X0] :
( k9_waybel_0(X0) = k8_waybel_0(k7_lattice3(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f46528]) ).
fof(f48083,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& l1_orders_2(k7_lattice3(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f28681]) ).
fof(f48723,plain,
! [X0] :
( ( v2_lattice3(X0)
<=> v1_lattice3(k7_lattice3(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f41372]) ).
fof(f48724,plain,
! [X0] :
( ( v3_orders_2(X0)
<=> v3_orders_2(k7_lattice3(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f41362]) ).
fof(f48725,plain,
! [X0] :
( ( v4_orders_2(X0)
<=> v4_orders_2(k7_lattice3(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f41361]) ).
fof(f48726,plain,
! [X0] :
( ( v2_orders_2(X0)
<=> v2_orders_2(k7_lattice3(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f41360]) ).
fof(f59381,plain,
( k3_tarski(sK403) != k1_yellow_0(k2_yellow_1(k9_waybel_0(sK402)),sK403)
& ~ v1_xboole_0(sK403)
& v1_waybel_0(sK403,k2_yellow_1(k9_waybel_0(sK402)))
& m1_subset_1(sK403,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK402)))))
& v2_orders_2(sK402)
& v3_orders_2(sK402)
& v4_orders_2(sK402)
& v2_yellow_0(sK402)
& v2_lattice3(sK402)
& l1_orders_2(sK402) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK402,sK403]),skolemize(X0,sK402),skolemize(X1,sK403)],[f46218]) ).
fof(f60437,plain,
! [X0] :
( ( ( v2_lattice3(X0)
| ~ v1_lattice3(k7_lattice3(X0)) )
& ( v1_lattice3(k7_lattice3(X0))
| ~ v2_lattice3(X0) ) )
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f48723]) ).
fof(f60438,plain,
! [X0] :
( ( ( v3_orders_2(X0)
| ~ v3_orders_2(k7_lattice3(X0)) )
& ( v3_orders_2(k7_lattice3(X0))
| ~ v3_orders_2(X0) ) )
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f48724]) ).
fof(f60439,plain,
! [X0] :
( ( ( v4_orders_2(X0)
| ~ v4_orders_2(k7_lattice3(X0)) )
& ( v4_orders_2(k7_lattice3(X0))
| ~ v4_orders_2(X0) ) )
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f48725]) ).
fof(f60440,plain,
! [X0] :
( ( ( v2_orders_2(X0)
| ~ v2_orders_2(k7_lattice3(X0)) )
& ( v2_orders_2(k7_lattice3(X0))
| ~ v2_orders_2(X0) ) )
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f48726]) ).
fof(f63515,plain,
l1_orders_2(sK402),
inference(cnf_transformation,[],[f59381]) ).
fof(f63516,plain,
v2_lattice3(sK402),
inference(cnf_transformation,[],[f59381]) ).
fof(f63517,plain,
v2_yellow_0(sK402),
inference(cnf_transformation,[],[f59381]) ).
fof(f63518,plain,
v4_orders_2(sK402),
inference(cnf_transformation,[],[f59381]) ).
fof(f63519,plain,
v3_orders_2(sK402),
inference(cnf_transformation,[],[f59381]) ).
fof(f63520,plain,
v2_orders_2(sK402),
inference(cnf_transformation,[],[f59381]) ).
fof(f63521,plain,
m1_subset_1(sK403,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK402))))),
inference(cnf_transformation,[],[f59381]) ).
fof(f63522,plain,
v1_waybel_0(sK403,k2_yellow_1(k9_waybel_0(sK402))),
inference(cnf_transformation,[],[f59381]) ).
fof(f63523,plain,
~ v1_xboole_0(sK403),
inference(cnf_transformation,[],[f59381]) ).
fof(f63524,plain,
k3_tarski(sK403) != k1_yellow_0(k2_yellow_1(k9_waybel_0(sK402)),sK403),
inference(cnf_transformation,[],[f59381]) ).
fof(f63667,plain,
! [X0] :
( ~ v2_lattice3(X0)
| ~ v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f46296]) ).
fof(f63722,plain,
! [X0] :
( v1_yellow_0(k7_lattice3(X0))
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f46328]) ).
fof(f63899,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(X0)))))
| v1_xboole_0(X1)
| ~ v1_waybel_0(X1,k2_yellow_1(k8_waybel_0(X0)))
| k3_tarski(X1) = k1_yellow_0(k2_yellow_1(k8_waybel_0(X0)),X1)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v1_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f46376]) ).
fof(f64182,plain,
! [X0] :
( ~ v3_orders_2(X0)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| k9_waybel_0(X0) = k8_waybel_0(k7_lattice3(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f46529]) ).
fof(f66995,plain,
! [X0] :
( l1_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f48083]) ).
fof(f68079,plain,
! [X0] :
( v1_lattice3(k7_lattice3(X0))
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f60437]) ).
fof(f68081,plain,
! [X0] :
( v3_orders_2(k7_lattice3(X0))
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f60438]) ).
fof(f68083,plain,
! [X0] :
( v4_orders_2(k7_lattice3(X0))
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f60439]) ).
fof(f68085,plain,
! [X0] :
( v2_orders_2(k7_lattice3(X0))
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f60440]) ).
fof(f90271,plain,
( ~ v3_struct_0(sK402)
| ~ l1_orders_2(sK402) ),
inference(resolution,[],[f63667,f63516]) ).
fof(f90301,plain,
( v3_struct_0(sK402)
| ~ v2_orders_2(sK402)
| k9_waybel_0(sK402) = k8_waybel_0(k7_lattice3(sK402))
| ~ l1_orders_2(sK402) ),
inference(resolution,[],[f64182,f63519]) ).
fof(f91033,plain,
~ v3_struct_0(sK402),
inference(forward_subsumption_resolution,[],[f90271,f63515]) ).
fof(f91035,definition,
( spl2620_126
<=> l1_orders_2(k7_lattice3(sK402)) ),
introduced(definition,[new_symbols(definition,[spl2620_126])],[avatar_definition]) ).
fof(f91036,plain,
( l1_orders_2(k7_lattice3(sK402))
| ~ spl2620_126 ),
inference(avatar_component_clause,[],[f91035]) ).
fof(f91037,plain,
( ~ l1_orders_2(k7_lattice3(sK402))
| spl2620_126 ),
inference(avatar_component_clause,[],[f91035]) ).
fof(f91048,definition,
( spl2620_129
<=> v4_orders_2(k7_lattice3(sK402)) ),
introduced(definition,[new_symbols(definition,[spl2620_129])],[avatar_definition]) ).
fof(f91049,plain,
( v4_orders_2(k7_lattice3(sK402))
| ~ spl2620_129 ),
inference(avatar_component_clause,[],[f91048]) ).
fof(f91050,plain,
( ~ v4_orders_2(k7_lattice3(sK402))
| spl2620_129 ),
inference(avatar_component_clause,[],[f91048]) ).
fof(f91052,definition,
( spl2620_130
<=> v2_orders_2(k7_lattice3(sK402)) ),
introduced(definition,[new_symbols(definition,[spl2620_130])],[avatar_definition]) ).
fof(f91053,plain,
( v2_orders_2(k7_lattice3(sK402))
| ~ spl2620_130 ),
inference(avatar_component_clause,[],[f91052]) ).
fof(f91054,plain,
( ~ v2_orders_2(k7_lattice3(sK402))
| spl2620_130 ),
inference(avatar_component_clause,[],[f91052]) ).
fof(f91060,plain,
( v3_struct_0(sK402)
| k9_waybel_0(sK402) = k8_waybel_0(k7_lattice3(sK402))
| ~ l1_orders_2(sK402) ),
inference(forward_subsumption_resolution,[],[f90301,f63520]) ).
fof(f91063,definition,
( spl2620_132
<=> v3_orders_2(k7_lattice3(sK402)) ),
introduced(definition,[new_symbols(definition,[spl2620_132])],[avatar_definition]) ).
fof(f91064,plain,
( v3_orders_2(k7_lattice3(sK402))
| ~ spl2620_132 ),
inference(avatar_component_clause,[],[f91063]) ).
fof(f91065,plain,
( ~ v3_orders_2(k7_lattice3(sK402))
| spl2620_132 ),
inference(avatar_component_clause,[],[f91063]) ).
fof(f91299,plain,
( k9_waybel_0(sK402) = k8_waybel_0(k7_lattice3(sK402))
| ~ l1_orders_2(sK402) ),
inference(forward_subsumption_resolution,[],[f91060,f91033]) ).
fof(f91318,definition,
( spl2620_156
<=> v1_lattice3(k7_lattice3(sK402)) ),
introduced(definition,[new_symbols(definition,[spl2620_156])],[avatar_definition]) ).
fof(f91319,plain,
( v1_lattice3(k7_lattice3(sK402))
| ~ spl2620_156 ),
inference(avatar_component_clause,[],[f91318]) ).
fof(f91320,plain,
( ~ v1_lattice3(k7_lattice3(sK402))
| spl2620_156 ),
inference(avatar_component_clause,[],[f91318]) ).
fof(f91383,plain,
k9_waybel_0(sK402) = k8_waybel_0(k7_lattice3(sK402)),
inference(forward_subsumption_resolution,[],[f91299,f63515]) ).
fof(f91688,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK402)))))
| v1_xboole_0(X0)
| ~ v1_waybel_0(X0,k2_yellow_1(k9_waybel_0(sK402)))
| k3_tarski(X0) = k1_yellow_0(k2_yellow_1(k9_waybel_0(sK402)),X0)
| ~ v2_orders_2(k7_lattice3(sK402))
| ~ v3_orders_2(k7_lattice3(sK402))
| ~ v4_orders_2(k7_lattice3(sK402))
| ~ v1_lattice3(k7_lattice3(sK402))
| ~ v1_yellow_0(k7_lattice3(sK402))
| ~ l1_orders_2(k7_lattice3(sK402)) ),
inference(superposition,[],[f63899,f91383]) ).
fof(f91787,plain,
( ~ l1_orders_2(sK402)
| spl2620_126 ),
inference(resolution,[],[f91037,f66995]) ).
fof(f91788,plain,
( $false
| spl2620_126 ),
inference(forward_subsumption_resolution,[],[f91787,f63515]) ).
fof(f91789,plain,
spl2620_126,
inference(avatar_contradiction_clause,[],[f91788]) ).
fof(f91834,plain,
( ~ v4_orders_2(sK402)
| ~ l1_orders_2(sK402)
| spl2620_129 ),
inference(resolution,[],[f91050,f68083]) ).
fof(f91835,plain,
( ~ l1_orders_2(sK402)
| spl2620_129 ),
inference(forward_subsumption_resolution,[],[f91834,f63518]) ).
fof(f91836,plain,
( $false
| spl2620_129 ),
inference(forward_subsumption_resolution,[],[f91835,f63515]) ).
fof(f91837,plain,
spl2620_129,
inference(avatar_contradiction_clause,[],[f91836]) ).
fof(f91839,plain,
( ~ v2_orders_2(sK402)
| ~ l1_orders_2(sK402)
| spl2620_130 ),
inference(resolution,[],[f91054,f68085]) ).
fof(f91840,plain,
( ~ l1_orders_2(sK402)
| spl2620_130 ),
inference(forward_subsumption_resolution,[],[f91839,f63520]) ).
fof(f91841,plain,
( $false
| spl2620_130 ),
inference(forward_subsumption_resolution,[],[f91840,f63515]) ).
fof(f91842,plain,
spl2620_130,
inference(avatar_contradiction_clause,[],[f91841]) ).
fof(f91855,plain,
( ~ v3_orders_2(sK402)
| ~ l1_orders_2(sK402)
| spl2620_132 ),
inference(resolution,[],[f91065,f68081]) ).
fof(f91856,plain,
( ~ l1_orders_2(sK402)
| spl2620_132 ),
inference(forward_subsumption_resolution,[],[f91855,f63519]) ).
fof(f91857,plain,
( $false
| spl2620_132 ),
inference(forward_subsumption_resolution,[],[f91856,f63515]) ).
fof(f91858,plain,
spl2620_132,
inference(avatar_contradiction_clause,[],[f91857]) ).
fof(f92699,plain,
( ~ v2_lattice3(sK402)
| ~ l1_orders_2(sK402)
| spl2620_156 ),
inference(resolution,[],[f91320,f68079]) ).
fof(f92700,plain,
( ~ l1_orders_2(sK402)
| spl2620_156 ),
inference(forward_subsumption_resolution,[],[f92699,f63516]) ).
fof(f92701,plain,
( $false
| spl2620_156 ),
inference(forward_subsumption_resolution,[],[f92700,f63515]) ).
fof(f92702,plain,
spl2620_156,
inference(avatar_contradiction_clause,[],[f92701]) ).
fof(f92705,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK402)))))
| v1_xboole_0(X0)
| ~ v1_waybel_0(X0,k2_yellow_1(k9_waybel_0(sK402)))
| k3_tarski(X0) = k1_yellow_0(k2_yellow_1(k9_waybel_0(sK402)),X0)
| ~ v3_orders_2(k7_lattice3(sK402))
| ~ v4_orders_2(k7_lattice3(sK402))
| ~ v1_lattice3(k7_lattice3(sK402))
| ~ v1_yellow_0(k7_lattice3(sK402))
| ~ l1_orders_2(k7_lattice3(sK402)) )
| ~ spl2620_130 ),
inference(forward_subsumption_resolution,[],[f91688,f91053]) ).
fof(f92708,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK402)))))
| v1_xboole_0(X0)
| ~ v1_waybel_0(X0,k2_yellow_1(k9_waybel_0(sK402)))
| k3_tarski(X0) = k1_yellow_0(k2_yellow_1(k9_waybel_0(sK402)),X0)
| ~ v4_orders_2(k7_lattice3(sK402))
| ~ v1_lattice3(k7_lattice3(sK402))
| ~ v1_yellow_0(k7_lattice3(sK402))
| ~ l1_orders_2(k7_lattice3(sK402)) )
| ~ spl2620_130
| ~ spl2620_132 ),
inference(forward_subsumption_resolution,[],[f92705,f91064]) ).
fof(f92711,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK402)))))
| v1_xboole_0(X0)
| ~ v1_waybel_0(X0,k2_yellow_1(k9_waybel_0(sK402)))
| k3_tarski(X0) = k1_yellow_0(k2_yellow_1(k9_waybel_0(sK402)),X0)
| ~ v1_lattice3(k7_lattice3(sK402))
| ~ v1_yellow_0(k7_lattice3(sK402))
| ~ l1_orders_2(k7_lattice3(sK402)) )
| ~ spl2620_129
| ~ spl2620_130
| ~ spl2620_132 ),
inference(forward_subsumption_resolution,[],[f92708,f91049]) ).
fof(f92714,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK402)))))
| v1_xboole_0(X0)
| ~ v1_waybel_0(X0,k2_yellow_1(k9_waybel_0(sK402)))
| k3_tarski(X0) = k1_yellow_0(k2_yellow_1(k9_waybel_0(sK402)),X0)
| ~ v1_yellow_0(k7_lattice3(sK402))
| ~ l1_orders_2(k7_lattice3(sK402)) )
| ~ spl2620_129
| ~ spl2620_130
| ~ spl2620_132
| ~ spl2620_156 ),
inference(forward_subsumption_resolution,[],[f92711,f91319]) ).
fof(f92717,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK402)))))
| v1_xboole_0(X0)
| ~ v1_waybel_0(X0,k2_yellow_1(k9_waybel_0(sK402)))
| k3_tarski(X0) = k1_yellow_0(k2_yellow_1(k9_waybel_0(sK402)),X0)
| ~ v1_yellow_0(k7_lattice3(sK402)) )
| ~ spl2620_126
| ~ spl2620_129
| ~ spl2620_130
| ~ spl2620_132
| ~ spl2620_156 ),
inference(forward_subsumption_resolution,[],[f92714,f91036]) ).
fof(f92719,definition,
( spl2620_194
<=> v1_yellow_0(k7_lattice3(sK402)) ),
introduced(definition,[new_symbols(definition,[spl2620_194])],[avatar_definition]) ).
fof(f92721,plain,
( ~ v1_yellow_0(k7_lattice3(sK402))
| spl2620_194 ),
inference(avatar_component_clause,[],[f92719]) ).
fof(f92723,definition,
( spl2620_195
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK402)))))
| k3_tarski(X0) = k1_yellow_0(k2_yellow_1(k9_waybel_0(sK402)),X0)
| ~ v1_waybel_0(X0,k2_yellow_1(k9_waybel_0(sK402)))
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2620_195])],[avatar_definition]) ).
fof(f92724,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK402)))))
| k3_tarski(X0) = k1_yellow_0(k2_yellow_1(k9_waybel_0(sK402)),X0)
| ~ v1_waybel_0(X0,k2_yellow_1(k9_waybel_0(sK402)))
| v1_xboole_0(X0) )
| ~ spl2620_195 ),
inference(avatar_component_clause,[],[f92723]) ).
fof(f92725,plain,
( ~ spl2620_194
| spl2620_195
| ~ spl2620_126
| ~ spl2620_129
| ~ spl2620_130
| ~ spl2620_132
| ~ spl2620_156 ),
inference(avatar_split_clause,[],[f92717,f91318,f91063,f91052,f91048,f91035,f92723,f92719]) ).
fof(f92727,plain,
( ~ v2_yellow_0(sK402)
| ~ l1_orders_2(sK402)
| spl2620_194 ),
inference(resolution,[],[f92721,f63722]) ).
fof(f92728,plain,
( ~ l1_orders_2(sK402)
| spl2620_194 ),
inference(forward_subsumption_resolution,[],[f92727,f63517]) ).
fof(f92729,plain,
( $false
| spl2620_194 ),
inference(forward_subsumption_resolution,[],[f92728,f63515]) ).
fof(f92730,plain,
spl2620_194,
inference(avatar_contradiction_clause,[],[f92729]) ).
fof(f92752,plain,
( k3_tarski(sK403) = k1_yellow_0(k2_yellow_1(k9_waybel_0(sK402)),sK403)
| ~ v1_waybel_0(sK403,k2_yellow_1(k9_waybel_0(sK402)))
| v1_xboole_0(sK403)
| ~ spl2620_195 ),
inference(resolution,[],[f92724,f63521]) ).
fof(f92756,plain,
( ~ v1_waybel_0(sK403,k2_yellow_1(k9_waybel_0(sK402)))
| v1_xboole_0(sK403)
| ~ spl2620_195 ),
inference(forward_subsumption_resolution,[],[f92752,f63524]) ).
fof(f92763,plain,
( v1_xboole_0(sK403)
| ~ spl2620_195 ),
inference(forward_subsumption_resolution,[],[f92756,f63522]) ).
fof(f92770,plain,
( $false
| ~ spl2620_195 ),
inference(forward_subsumption_resolution,[],[f92763,f63523]) ).
fof(f92771,plain,
~ spl2620_195,
inference(avatar_contradiction_clause,[],[f92770]) ).
cnf(s171,plain,
spl2620_126,
inference(sat_conversion,[],[f91789]) ).
cnf(s177,plain,
spl2620_129,
inference(sat_conversion,[],[f91837]) ).
cnf(s178,plain,
spl2620_130,
inference(sat_conversion,[],[f91842]) ).
cnf(s180,plain,
spl2620_132,
inference(sat_conversion,[],[f91858]) ).
cnf(s188,plain,
spl2620_156,
inference(sat_conversion,[],[f92702]) ).
cnf(s189,plain,
( ~ spl2620_126
| ~ spl2620_129
| ~ spl2620_130
| ~ spl2620_132
| ~ spl2620_156
| ~ spl2620_194
| spl2620_195 ),
inference(sat_conversion,[],[f92725]) ).
cnf(s190,plain,
spl2620_194,
inference(sat_conversion,[],[f92730]) ).
cnf(s191,plain,
~ spl2620_195,
inference(sat_conversion,[],[f92771]) ).
cnf(s192,plain,
( ~ spl2620_126
| ~ spl2620_129
| ~ spl2620_130
| ~ spl2620_132
| ~ spl2620_156 ),
inference(rat,[],[s189,s191,s190]) ).
cnf(s193,plain,
~ spl2620_126,
inference(rat,[],[s192,s188,s180,s178,s177]) ).
cnf(s194,plain,
$false,
inference(rat,[],[s171,s193]) ).
fof(f92776,plain,
$false,
inference(avatar_sat_refutation,[],[s194]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT347+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n026.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 14:56:05 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 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
% 14.27/5.78 % (2933594)Detected formulas, will run a generic FOF schedule.
% 14.27/5.78 % (2933603)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2470148066:i=119:av=off:ss=axioms_2967 on theBenchmark for (2967ds/119Mi)
% 14.27/5.78 % (2933602)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=914532904:i=109:sd=1:ins=1:gsp=on:ss=axioms_2967 on theBenchmark for (2967ds/109Mi)
% 14.27/5.78 % (2933599)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=649808985:i=141193_2967 on theBenchmark for (2967ds/141193Mi)
% 14.27/5.78 % (2933600)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3094771367:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2967 on theBenchmark for (2967ds/134677Mi)
% 14.27/5.78 % (2933601)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3637389066:i=141695:sd=1:nm=32:gsp=on:ss=included_2967 on theBenchmark for (2967ds/141695Mi)
% 14.27/5.78 % (2933605)dis-21_1_sil=8000:lcm=predicate:random_seed=4150145966:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2967 on theBenchmark for (2967ds/129Mi)
% 14.27/5.78 % (2933604)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=485350217:s2a=on:i=139:gtg=position_2967 on theBenchmark for (2967ds/139Mi)
% 14.27/5.78 % (2933603)Instruction limit reached!
% 14.27/5.78 % (2933603)------------------------------
% 14.27/5.78 % (2933603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.27/5.78 % (2933603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.27/5.78 % (2933603)CaDiCaL version: 2.1.3
% 14.27/5.78 % (2933603)Termination reason: Instruction limit
% 14.27/5.78 % (2933603)Termination phase: SInE selection
% 14.27/5.78 % (2933603)Time elapsed: 0.057 s
% 14.27/5.78 % (2933603)Peak memory usage: 154 MB
% 14.27/5.78 % (2933603)Instructions burned: 120 (million)
% 14.27/5.78 % (2933604)Instruction limit reached!
% 14.27/5.78 % (2933604)------------------------------
% 14.27/5.78 % (2933604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.27/5.78 % (2933604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.27/5.78 % (2933604)CaDiCaL version: 2.1.3
% 14.27/5.78 % (2933604)Termination reason: Instruction limit
% 14.27/5.78 % (2933604)Termination phase: Property scanning
% 14.27/5.78 % (2933604)Time elapsed: 0.064 s
% 14.27/5.78 % (2933604)Peak memory usage: 154 MB
% 14.27/5.78 % (2933604)Instructions burned: 140 (million)
% 14.27/5.78 % (2933602)Instruction limit reached!
% 14.27/5.78 % (2933602)------------------------------
% 14.27/5.78 % (2933602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.27/5.78 % (2933602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.27/5.78 % (2933602)CaDiCaL version: 2.1.3
% 14.27/5.78 % (2933602)Termination reason: Instruction limit
% 14.27/5.78 % (2933602)Termination phase: SInE selection
% 14.27/5.78 % (2933602)Time elapsed: 0.085 s
% 14.27/5.78 % (2933602)Peak memory usage: 154 MB
% 14.27/5.78 % (2933602)Instructions burned: 109 (million)
% 14.27/5.78 % (2933605)Instruction limit reached!
% 14.27/5.78 % (2933605)------------------------------
% 14.27/5.78 % (2933605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.27/5.78 % (2933605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.27/5.78 % (2933605)CaDiCaL version: 2.1.3
% 14.27/5.78 % (2933605)Termination reason: Instruction limit
% 14.27/5.78 % (2933605)Termination phase: SInE selection
% 14.27/5.78 % (2933605)Time elapsed: 0.101 s
% 14.27/5.78 % (2933605)Peak memory usage: 154 MB
% 14.27/5.78 % (2933605)Instructions burned: 130 (million)
% 14.27/5.78 % (2933613)lrs+10_1_sil=8000:sp=occurrence:random_seed=3501291706:i=285:sd=3:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/285Mi)
% 14.27/5.78 % (2933615)lrs+1011_1_sil=32000:sp=occurrence:random_seed=461348031:i=325:sd=1:ss=axioms:sgt=32_2965 on theBenchmark for (2965ds/325Mi)
% 14.27/5.78 % (2933614)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2666747579:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/157Mi)
% 14.27/5.78 % (2933613)Instruction limit reached!
% 14.27/5.78 % (2933613)------------------------------
% 14.27/5.78 % (2933613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.27/5.78 % (2933613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.47/6.77 % (2933613)CaDiCaL version: 2.1.3
% 21.47/6.77 % (2933613)Termination reason: Instruction limit
% 21.47/6.77 % (2933613)Termination phase: SInE selection
% 21.47/6.77 % (2933613)Time elapsed: 0.123 s
% 21.47/6.77 % (2933613)Peak memory usage: 154 MB
% 21.47/6.77 % (2933613)Instructions burned: 285 (million)
% 21.47/6.77 % (2933616)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1481697236:s2a=on:i=248:s2at=1.23:gtg=position_2965 on theBenchmark for (2965ds/248Mi)
% 21.47/6.77 % (2933614)Instruction limit reached!
% 21.47/6.77 % (2933614)------------------------------
% 21.47/6.77 % (2933614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.47/6.77 % (2933614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.47/6.77 % (2933614)CaDiCaL version: 2.1.3
% 21.47/6.77 % (2933614)Termination reason: Instruction limit
% 21.47/6.77 % (2933614)Termination phase: Property scanning
% 21.47/6.77 % (2933614)Time elapsed: 0.070 s
% 21.47/6.77 % (2933614)Peak memory usage: 154 MB
% 21.47/6.77 % (2933614)Instructions burned: 157 (million)
% 21.47/6.77 % (2933616)Instruction limit reached!
% 21.47/6.77 % (2933616)------------------------------
% 21.47/6.77 % (2933616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.47/6.77 % (2933616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.47/6.77 % (2933616)CaDiCaL version: 2.1.3
% 21.47/6.77 % (2933616)Termination reason: Instruction limit
% 21.47/6.77 % (2933616)Termination phase: Property scanning
% 21.47/6.77 % (2933616)Time elapsed: 0.109 s
% 21.47/6.77 % (2933616)Peak memory usage: 154 MB
% 21.47/6.77 % (2933616)Instructions burned: 250 (million)
% 21.47/6.77 % (2933621)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1738427524:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2963 on theBenchmark for (2963ds/294Mi)
% 21.47/6.77 % (2933622)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2415161703:i=2350_2963 on theBenchmark for (2963ds/2350Mi)
% 21.47/6.77 % (2933615)Instruction limit reached!
% 21.47/6.77 % (2933615)------------------------------
% 21.47/6.77 % (2933615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.47/6.77 % (2933615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.47/6.77 % (2933615)CaDiCaL version: 2.1.3
% 21.47/6.77 % (2933615)Termination reason: Instruction limit
% 21.47/6.77 % (2933615)Termination phase: SInE selection
% 21.47/6.77 % (2933615)Time elapsed: 0.237 s
% 21.47/6.77 % (2933615)Peak memory usage: 155 MB
% 21.47/6.77 % (2933615)Instructions burned: 325 (million)
% 21.47/6.77 % (2933623)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2695384760:cts=off:i=113:fsr=off:ss=included:sgt=4_2962 on theBenchmark for (2962ds/113Mi)
% 21.47/6.77 % (2933626)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=695475487:i=127:av=off:fsr=off:sup=off_2961 on theBenchmark for (2961ds/127Mi)
% 21.47/6.77 % (2933621)Instruction limit reached!
% 21.47/6.77 % (2933621)------------------------------
% 21.47/6.77 % (2933621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.47/6.77 % (2933621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.47/6.77 % (2933621)CaDiCaL version: 2.1.3
% 21.47/6.77 % (2933621)Termination reason: Instruction limit
% 21.47/6.77 % (2933621)Termination phase: SInE selection
% 21.47/6.77 % (2933621)Time elapsed: 0.201 s
% 21.47/6.77 % (2933621)Peak memory usage: 154 MB
% 21.47/6.77 % (2933621)Instructions burned: 295 (million)
% 21.47/6.77 % (2933623)Instruction limit reached!
% 21.47/6.77 % (2933623)------------------------------
% 21.47/6.77 % (2933623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.47/6.77 % (2933623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.47/6.77 % (2933623)CaDiCaL version: 2.1.3
% 21.47/6.77 % (2933623)Termination reason: Instruction limit
% 21.47/6.77 % (2933623)Termination phase: SInE selection
% 21.47/6.77 % (2933623)Time elapsed: 0.088 s
% 21.47/6.77 % (2933623)Peak memory usage: 154 MB
% 21.47/6.77 % (2933623)Instructions burned: 113 (million)
% 21.47/6.77 % (2933626)Instruction limit reached!
% 21.47/6.77 % (2933626)------------------------------
% 21.47/6.77 % (2933626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.47/6.77 % (2933626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.47/6.77 % (2933626)CaDiCaL version: 2.1.3
% 59.07/11.97 % (2933626)Termination reason: Instruction limit
% 59.07/11.97 % (2933626)Termination phase: Preprocessing 1
% 59.07/11.97 % (2933626)Time elapsed: 0.097 s
% 59.07/11.97 % (2933626)Peak memory usage: 155 MB
% 59.07/11.97 % (2933626)Instructions burned: 127 (million)
% 59.07/11.97 % (2933629)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4221471874:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2960 on theBenchmark for (2960ds/114Mi)
% 59.07/11.97 % (2933630)lrs+10_1_sil=8000:sp=occurrence:random_seed=3899453627:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2960 on theBenchmark for (2960ds/907Mi)
% 59.07/11.97 % (2933629)Instruction limit reached!
% 59.07/11.97 % (2933629)------------------------------
% 59.07/11.97 % (2933629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.07/11.97 % (2933629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.07/11.97 % (2933629)CaDiCaL version: 2.1.3
% 59.07/11.97 % (2933629)Termination reason: Instruction limit
% 59.07/11.97 % (2933629)Termination phase: Property scanning
% 59.07/11.97 % (2933629)Time elapsed: 0.054 s
% 59.07/11.97 % (2933629)Peak memory usage: 154 MB
% 59.07/11.97 % (2933629)Instructions burned: 116 (million)
% 59.07/11.97 % (2933631)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=297159125:i=437:sd=1:aac=none:ss=included_2959 on theBenchmark for (2959ds/437Mi)
% 59.07/11.97 % (2933634)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2231025154:i=5202:ss=axioms:sgt=16_2958 on theBenchmark for (2958ds/5202Mi)
% 59.07/11.97 % (2933631)Instruction limit reached!
% 59.07/11.97 % (2933631)------------------------------
% 59.07/11.97 % (2933631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.07/11.97 % (2933631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.07/11.97 % (2933631)CaDiCaL version: 2.1.3
% 59.07/11.97 % (2933631)Termination reason: Instruction limit
% 59.07/11.97 % (2933631)Termination phase: Saturation
% 59.07/11.97 % (2933631)Time elapsed: 0.335 s
% 59.07/11.97 % (2933631)Peak memory usage: 160 MB
% 59.07/11.97 % (2933631)Instructions burned: 438 (million)
% 59.07/11.97 % (2933637)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2248041750:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2954 on theBenchmark for (2954ds/134Mi)
% 59.07/11.97 % (2933622)Instruction limit reached!
% 59.07/11.97 % (2933622)------------------------------
% 59.07/11.97 % (2933622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.07/11.97 % (2933622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.07/11.97 % (2933622)CaDiCaL version: 2.1.3
% 59.07/11.97 % (2933622)Termination reason: Instruction limit
% 59.07/11.97 % (2933622)Termination phase: Preprocessing 3
% 59.07/11.97 % (2933622)Time elapsed: 0.981 s
% 59.07/11.97 % (2933622)Peak memory usage: 255 MB
% 59.07/11.97 % (2933622)Instructions burned: 2350 (million)
% 59.07/11.97 % (2933630)Instruction limit reached!
% 59.07/11.97 % (2933630)------------------------------
% 59.07/11.97 % (2933630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.07/11.97 % (2933630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.07/11.97 % (2933630)CaDiCaL version: 2.1.3
% 59.07/11.97 % (2933630)Termination reason: Instruction limit
% 59.07/11.97 % (2933630)Termination phase: Property scanning
% 59.07/11.97 % (2933630)Time elapsed: 0.642 s
% 59.07/11.97 % (2933630)Peak memory usage: 173 MB
% 59.07/11.97 % (2933630)Instructions burned: 908 (million)
% 59.07/11.97 % (2933637)Instruction limit reached!
% 59.07/11.97 % (2933637)------------------------------
% 59.07/11.97 % (2933637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.07/11.97 % (2933637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.07/11.97 % (2933637)CaDiCaL version: 2.1.3
% 59.07/11.97 % (2933637)Termination reason: Instruction limit
% 59.07/11.97 % (2933637)Termination phase: SInE selection
% 59.07/11.97 % (2933637)Time elapsed: 0.103 s
% 59.07/11.97 % (2933637)Peak memory usage: 154 MB
% 59.07/11.97 % (2933637)Instructions burned: 135 (million)
% 59.07/11.97 % (2933639)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3149085630:st=8:i=592:sd=3:ep=RST:ss=axioms_2952 on theBenchmark for (2952ds/592Mi)
% 59.07/11.97 % (2933640)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1615271439:st=3:i=13193:sd=3:ss=axioms_2952 on theBenchmark for (2952ds/13193Mi)
% 59.07/11.97 % (2933641)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1620094929:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2952 on theBenchmark for (2952ds/125Mi)
% 44.50/12.91 % (2933641)Instruction limit reached!
% 44.50/12.91 % (2933641)------------------------------
% 44.50/12.91 % (2933641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.50/12.91 % (2933641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.50/12.91 % (2933641)CaDiCaL version: 2.1.3
% 44.50/12.91 % (2933641)Termination reason: Instruction limit
% 44.50/12.91 % (2933641)Termination phase: Property scanning
% 44.50/12.91 % (2933641)Time elapsed: 0.059 s
% 44.50/12.91 % (2933641)Peak memory usage: 154 MB
% 44.50/12.91 % (2933641)Instructions burned: 127 (million)
% 44.50/12.91 % (2933645)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3311786935:i=134:gtgl=5:slsql=off:gtg=exists_sym_2950 on theBenchmark for (2950ds/134Mi)
% 44.50/12.91 % (2933639)Instruction limit reached!
% 44.50/12.91 % (2933639)------------------------------
% 44.50/12.91 % (2933639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.50/12.91 % (2933639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.50/12.91 % (2933639)CaDiCaL version: 2.1.3
% 44.50/12.91 % (2933639)Termination reason: Instruction limit
% 44.50/12.91 % (2933639)Termination phase: Preprocessing 1
% 44.50/12.91 % (2933639)Time elapsed: 0.257 s
% 44.50/12.91 % (2933639)Peak memory usage: 157 MB
% 44.50/12.91 % (2933639)Instructions burned: 593 (million)
% 44.50/12.91 % (2933645)Instruction limit reached!
% 44.50/12.91 % (2933645)------------------------------
% 44.50/12.91 % (2933645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.50/12.91 % (2933645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.50/12.91 % (2933645)CaDiCaL version: 2.1.3
% 44.50/12.91 % (2933645)Termination reason: Instruction limit
% 44.50/12.91 % (2933645)Termination phase: Property scanning
% 44.50/12.91 % (2933645)Time elapsed: 0.062 s
% 44.50/12.91 % (2933645)Peak memory usage: 154 MB
% 44.50/12.91 % (2933645)Instructions burned: 136 (million)
% 44.50/12.91 % (2933647)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=899141542:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2948 on theBenchmark for (2948ds/141Mi)
% 44.50/12.91 % (2933647)Instruction limit reached!
% 44.50/12.91 % (2933647)------------------------------
% 44.50/12.91 % (2933647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.50/12.91 % (2933647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.50/12.91 % (2933647)CaDiCaL version: 2.1.3
% 44.50/12.91 % (2933647)Termination reason: Instruction limit
% 44.50/12.91 % (2933647)Termination phase: SInE selection
% 44.50/12.91 % (2933647)Time elapsed: 0.067 s
% 44.50/12.91 % (2933647)Peak memory usage: 154 MB
% 44.50/12.91 % (2933647)Instructions burned: 141 (million)
% 44.50/12.91 % (2933648)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3249170589:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2948 on theBenchmark for (2948ds/431Mi)
% 44.50/12.91 % (2933650)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3889837131:i=6060:aac=none:ins=25_2946 on theBenchmark for (2946ds/6060Mi)
% 44.50/12.91 % (2933648)Instruction limit reached!
% 44.50/12.91 % (2933648)------------------------------
% 44.50/12.91 % (2933648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.50/12.91 % (2933648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.50/12.91 % (2933648)CaDiCaL version: 2.1.3
% 44.50/12.91 % (2933648)Termination reason: Instruction limit
% 44.50/12.91 % (2933648)Termination phase: Saturation
% 44.50/12.91 % (2933648)Time elapsed: 0.334 s
% 44.50/12.91 % (2933648)Peak memory usage: 160 MB
% 44.50/12.91 % (2933648)Instructions burned: 432 (million)
% 44.50/12.91 % (2933653)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2099353317:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2943 on theBenchmark for (2943ds/150Mi)
% 44.50/12.91 % (2933653)Instruction limit reached!
% 44.50/12.91 % (2933653)------------------------------
% 44.50/12.91 % (2933653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.50/12.91 % (2933653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.50/12.91 % (2933653)CaDiCaL version: 2.1.3
% 44.50/12.91 % (2933653)Termination reason: Instruction limit
% 44.50/12.91 % (2933653)Termination phase: SInE selection
% 44.50/12.91 % (2933653)Time elapsed: 0.115 s
% 44.50/12.91 % (2933653)Peak memory usage: 154 MB
% 44.50/12.91 % (2933653)Instructions burned: 150 (million)
% 44.50/12.91 % (2933655)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3124064660:i=14155:bd=all_2940 on theBenchmark for (2940ds/14155Mi)
% 44.50/12.91 % (2933634)Instruction limit reached!
% 44.50/12.91 % (2933634)------------------------------
% 44.50/12.91 % (2933634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.50/12.91 % (2933634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.50/12.91 % (2933634)CaDiCaL version: 2.1.3
% 44.50/12.91 % (2933634)Termination reason: Instruction limit
% 44.50/12.91 % (2933634)Termination phase: Saturation
% 44.50/12.91 % (2933634)Time elapsed: 3.281 s
% 44.50/12.91 % (2933634)Peak memory usage: 292 MB
% 44.50/12.91 % (2933634)Instructions burned: 5202 (million)
% 44.50/12.91 % (2933657)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2370269953:i=667:av=off:fsr=off_2924 on theBenchmark for (2924ds/667Mi)
% 44.50/12.91 % (2933650)Instruction limit reached!
% 44.50/12.91 % (2933650)------------------------------
% 44.50/12.91 % (2933650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.50/12.91 % (2933650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.50/12.91 % (2933650)CaDiCaL version: 2.1.3
% 44.50/12.91 % (2933650)Termination reason: Instruction limit
% 44.50/12.91 % (2933650)Termination phase: NewCNF
% 44.50/12.91 % (2933650)Time elapsed: 2.684 s
% 44.50/12.91 % (2933650)Peak memory usage: 302 MB
% 44.50/12.91 % (2933650)Instructions burned: 6060 (million)
% 44.50/12.91 % (2933659)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1225137312:s2a=on:i=185:s2at=1.8:fdi=4_2918 on theBenchmark for (2918ds/185Mi)
% 44.50/12.91 % (2933659)Instruction limit reached!
% 44.50/12.91 % (2933659)------------------------------
% 44.50/12.91 % (2933659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.50/12.91 % (2933659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.50/12.91 % (2933659)CaDiCaL version: 2.1.3
% 44.50/12.91 % (2933659)Termination reason: Instruction limit
% 44.50/12.91 % (2933659)Termination phase: SInE selection
% 44.50/12.91 % (2933659)Time elapsed: 0.079 s
% 44.50/12.91 % (2933659)Peak memory usage: 154 MB
% 44.50/12.91 % (2933659)Instructions burned: 188 (million)
% 44.50/12.91 % (2933657)Instruction limit reached!
% 44.50/12.91 % (2933657)------------------------------
% 44.50/12.91 % (2933657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.50/12.91 % (2933657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.50/12.91 % (2933657)CaDiCaL version: 2.1.3
% 44.50/12.91 % (2933657)Termination reason: Instruction limit
% 44.50/12.91 % (2933657)Termination phase: NewCNF
% 44.50/12.91 % (2933657)Time elapsed: 0.598 s
% 44.50/12.91 % (2933657)Peak memory usage: 212 MB
% 44.50/12.91 % (2933657)Instructions burned: 667 (million)
% 44.50/12.91 % (2933661)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3167410024:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2917 on theBenchmark for (2917ds/193Mi)
% 44.50/12.91 % (2933661)Instruction limit reached!
% 44.50/12.91 % (2933661)------------------------------
% 44.50/12.91 % (2933661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.50/12.91 % (2933661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.50/12.91 % (2933661)CaDiCaL version: 2.1.3
% 44.50/12.91 % (2933661)Termination reason: Instruction limit
% 44.50/12.91 % (2933661)Termination phase: SInE selection
% 44.50/12.91 % (2933661)Time elapsed: 0.085 s
% 44.50/12.91 % (2933661)Peak memory usage: 154 MB
% 44.50/12.91 % (2933661)Instructions burned: 194 (million)
% 44.50/12.91 % (2933662)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=234468226:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2916 on theBenchmark for (2916ds/4850Mi)
% 44.50/12.91 % (2933664)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3620372825:i=12111:sd=1:ss=included_2915 on theBenchmark for (2915ds/12111Mi)
% 44.50/12.91 % (2933662)Instruction limit reached!
% 44.50/12.91 % (2933662)------------------------------
% 44.50/12.91 % (2933662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.50/12.91 % (2933662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.50/12.91 % (2933662)CaDiCaL version: 2.1.3
% 44.50/12.91 % (2933662)Termination reason: Instruction limit
% 44.50/12.91 % (2933662)Termination phase: Function definition elimination
% 44.50/12.91 % (2933662)Time elapsed: 2.611 s
% 44.50/12.91 % (2933662)Peak memory usage: 239 MB
% 44.50/12.91 % (2933662)Instructions burned: 4851 (million)
% 44.50/12.91 % (2933667)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2311930995:i=319:kws=precedence:fsr=off_2888 on theBenchmark for (2888ds/319Mi)
% 44.50/12.91 % (2933667)Instruction limit reached!
% 44.50/12.91 % (2933667)------------------------------
% 44.50/12.91 % (2933667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.50/12.91 % (2933667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.50/12.91 % (2933667)CaDiCaL version: 2.1.3
% 44.50/12.91 % (2933667)Termination reason: Instruction limit
% 44.50/12.91 % (2933667)Termination phase: Preprocessing 1
% 44.50/12.91 % (2933667)Time elapsed: 0.227 s
% 44.50/12.91 % (2933667)Peak memory usage: 156 MB
% 44.50/12.91 % (2933667)Instructions burned: 319 (million)
% 44.50/12.91 % (2933640)First to succeed.
% 44.50/12.91 % (2933640)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2933594"
% 44.50/12.91 % (2933669)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=94989315:i=2064:ep=RST_2884 on theBenchmark for (2884ds/2064Mi)
% 44.50/12.91 % (2933600)Also succeeded, but the first one will report.
% 44.50/12.91 % (2933640)Refutation found. Thanks to Tanya!
% 44.50/12.91 % SZS status Theorem for theBenchmark
% 44.50/12.91 % SZS output start Proof for theBenchmark
% See solution above
% 65.98/13.17 % (2933640)------------------------------
% 65.98/13.17 % (2933640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.98/13.17 % (2933640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.98/13.17 % (2933640)CaDiCaL version: 2.1.3
% 65.98/13.17 % (2933640)Termination reason: Refutation
% 65.98/13.17 % (2933640)Time elapsed: 6.710 s
% 65.98/13.17 % (2933640)Peak memory usage: 390 MB
% 65.98/13.17 % (2933640)Instructions burned: 11391 (million)
% 65.98/13.17 % (2933640)------------------------------
% 65.98/13.17 % (2933640)------------------------------
% 65.98/13.17 % (2933594)Success in time 12.055 s
% 65.98/13.17 % Vampire exiting
%------------------------------------------------------------------------------