%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT347+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:09 AM UTC 2026
% Result : Theorem 48.26s 9.33s
% Output : Refutation 56.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 17
% Syntax : Number of formulae : 110 ( 28 unt; 7 def)
% Number of atoms : 348 ( 22 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 388 ( 150 ~; 147 |; 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 : 50 ( 0 sgn 46 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6772,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_lattice3) ).
fof(f6848,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v1_orders_2(k7_lattice3(X0))
& l1_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_lattice3) ).
fof(f8415,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/sandbox2/benchmark/theBenchmark.p',fc10_yellow_7) ).
fof(f8424,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_orders_2(X0)
<=> v2_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_yellow_7) ).
fof(f8425,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v4_orders_2(X0)
<=> v4_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_yellow_7) ).
fof(f8426,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v3_orders_2(X0)
<=> v3_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_yellow_7) ).
fof(f8436,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
<=> v1_lattice3(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t16_yellow_7) ).
fof(f8649,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/sandbox2/benchmark/theBenchmark.p',t9_waybel13) ).
fof(f8783,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/sandbox2/benchmark/theBenchmark.p',t7_waybel16) ).
fof(f8950,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/sandbox2/benchmark/theBenchmark.p',t1_waybel22) ).
fof(f8951,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)],[f8950]) ).
fof(f9217,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,[],[f8951]) ).
fof(f9218,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,[],[f9217]) ).
fof(f9222,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,[],[f8649]) ).
fof(f9223,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,[],[f9222]) ).
fof(f9307,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f6772]) ).
fof(f9308,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9307]) ).
fof(f9315,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,[],[f8415]) ).
fof(f9316,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v1_yellow_0(k7_lattice3(X0)) )
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9315]) ).
fof(f9465,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,[],[f8783]) ).
fof(f9466,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,[],[f9465]) ).
fof(f10566,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& l1_orders_2(k7_lattice3(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f6848]) ).
fof(f10658,plain,
! [X0] :
( ( v2_lattice3(X0)
<=> v1_lattice3(k7_lattice3(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8436]) ).
fof(f10659,plain,
! [X0] :
( ( v3_orders_2(X0)
<=> v3_orders_2(k7_lattice3(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8426]) ).
fof(f10660,plain,
! [X0] :
( ( v4_orders_2(X0)
<=> v4_orders_2(k7_lattice3(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8425]) ).
fof(f10661,plain,
! [X0] :
( ( v2_orders_2(X0)
<=> v2_orders_2(k7_lattice3(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8424]) ).
fof(f14027,plain,
( k3_tarski(sK178) != k1_yellow_0(k2_yellow_1(k9_waybel_0(sK177)),sK178)
& ~ v1_xboole_0(sK178)
& v1_waybel_0(sK178,k2_yellow_1(k9_waybel_0(sK177)))
& m1_subset_1(sK178,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK177)))))
& v2_orders_2(sK177)
& v3_orders_2(sK177)
& v4_orders_2(sK177)
& v2_yellow_0(sK177)
& v2_lattice3(sK177)
& l1_orders_2(sK177) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK177,sK178]),skolemize(X0,sK177),skolemize(X1,sK178)],[f9218]) ).
fof(f14729,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,[],[f10658]) ).
fof(f14730,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,[],[f10659]) ).
fof(f14731,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,[],[f10660]) ).
fof(f14732,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,[],[f10661]) ).
fof(f15836,plain,
l1_orders_2(sK177),
inference(cnf_transformation,[],[f14027]) ).
fof(f15837,plain,
v2_lattice3(sK177),
inference(cnf_transformation,[],[f14027]) ).
fof(f15838,plain,
v2_yellow_0(sK177),
inference(cnf_transformation,[],[f14027]) ).
fof(f15839,plain,
v4_orders_2(sK177),
inference(cnf_transformation,[],[f14027]) ).
fof(f15840,plain,
v3_orders_2(sK177),
inference(cnf_transformation,[],[f14027]) ).
fof(f15841,plain,
v2_orders_2(sK177),
inference(cnf_transformation,[],[f14027]) ).
fof(f15842,plain,
m1_subset_1(sK178,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK177))))),
inference(cnf_transformation,[],[f14027]) ).
fof(f15843,plain,
v1_waybel_0(sK178,k2_yellow_1(k9_waybel_0(sK177))),
inference(cnf_transformation,[],[f14027]) ).
fof(f15844,plain,
~ v1_xboole_0(sK178),
inference(cnf_transformation,[],[f14027]) ).
fof(f15845,plain,
k3_tarski(sK178) != k1_yellow_0(k2_yellow_1(k9_waybel_0(sK177)),sK178),
inference(cnf_transformation,[],[f14027]) ).
fof(f15849,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,[],[f9223]) ).
fof(f16009,plain,
! [X0] :
( ~ v2_lattice3(X0)
| ~ v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9308]) ).
fof(f16031,plain,
! [X0] :
( v1_yellow_0(k7_lattice3(X0))
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9316]) ).
fof(f16462,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,[],[f9466]) ).
fof(f18436,plain,
! [X0] :
( l1_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f10566]) ).
fof(f18831,plain,
! [X0] :
( v1_lattice3(k7_lattice3(X0))
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f14729]) ).
fof(f18833,plain,
! [X0] :
( v3_orders_2(k7_lattice3(X0))
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f14730]) ).
fof(f18835,plain,
! [X0] :
( v4_orders_2(k7_lattice3(X0))
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f14731]) ).
fof(f18837,plain,
! [X0] :
( v2_orders_2(k7_lattice3(X0))
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f14732]) ).
fof(f27518,plain,
( ~ v3_struct_0(sK177)
| ~ l1_orders_2(sK177) ),
inference(resolution,[],[f16009,f15837]) ).
fof(f27529,plain,
( v3_struct_0(sK177)
| ~ v2_orders_2(sK177)
| k9_waybel_0(sK177) = k8_waybel_0(k7_lattice3(sK177))
| ~ l1_orders_2(sK177) ),
inference(resolution,[],[f16462,f15840]) ).
fof(f28049,plain,
~ v3_struct_0(sK177),
inference(forward_subsumption_resolution,[],[f27518,f15836]) ).
fof(f28054,plain,
( v3_struct_0(sK177)
| k9_waybel_0(sK177) = k8_waybel_0(k7_lattice3(sK177))
| ~ l1_orders_2(sK177) ),
inference(forward_subsumption_resolution,[],[f27529,f15841]) ).
fof(f28260,plain,
( k9_waybel_0(sK177) = k8_waybel_0(k7_lattice3(sK177))
| ~ l1_orders_2(sK177) ),
inference(forward_subsumption_resolution,[],[f28054,f28049]) ).
fof(f28373,plain,
k9_waybel_0(sK177) = k8_waybel_0(k7_lattice3(sK177)),
inference(forward_subsumption_resolution,[],[f28260,f15836]) ).
fof(f28626,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK177)))))
| v1_xboole_0(X0)
| ~ v1_waybel_0(X0,k2_yellow_1(k9_waybel_0(sK177)))
| k3_tarski(X0) = k1_yellow_0(k2_yellow_1(k9_waybel_0(sK177)),X0)
| ~ v2_orders_2(k7_lattice3(sK177))
| ~ v3_orders_2(k7_lattice3(sK177))
| ~ v4_orders_2(k7_lattice3(sK177))
| ~ v1_lattice3(k7_lattice3(sK177))
| ~ v1_yellow_0(k7_lattice3(sK177))
| ~ l1_orders_2(k7_lattice3(sK177)) ),
inference(superposition,[],[f15849,f28373]) ).
fof(f28628,definition,
( spl1130_58
<=> l1_orders_2(k7_lattice3(sK177)) ),
introduced(definition,[new_symbols(definition,[spl1130_58])],[avatar_definition]) ).
fof(f28630,plain,
( ~ l1_orders_2(k7_lattice3(sK177))
| spl1130_58 ),
inference(avatar_component_clause,[],[f28628]) ).
fof(f28632,definition,
( spl1130_59
<=> v1_yellow_0(k7_lattice3(sK177)) ),
introduced(definition,[new_symbols(definition,[spl1130_59])],[avatar_definition]) ).
fof(f28634,plain,
( ~ v1_yellow_0(k7_lattice3(sK177))
| spl1130_59 ),
inference(avatar_component_clause,[],[f28632]) ).
fof(f28636,definition,
( spl1130_60
<=> v1_lattice3(k7_lattice3(sK177)) ),
introduced(definition,[new_symbols(definition,[spl1130_60])],[avatar_definition]) ).
fof(f28638,plain,
( ~ v1_lattice3(k7_lattice3(sK177))
| spl1130_60 ),
inference(avatar_component_clause,[],[f28636]) ).
fof(f28640,definition,
( spl1130_61
<=> v4_orders_2(k7_lattice3(sK177)) ),
introduced(definition,[new_symbols(definition,[spl1130_61])],[avatar_definition]) ).
fof(f28642,plain,
( ~ v4_orders_2(k7_lattice3(sK177))
| spl1130_61 ),
inference(avatar_component_clause,[],[f28640]) ).
fof(f28644,definition,
( spl1130_62
<=> v3_orders_2(k7_lattice3(sK177)) ),
introduced(definition,[new_symbols(definition,[spl1130_62])],[avatar_definition]) ).
fof(f28646,plain,
( ~ v3_orders_2(k7_lattice3(sK177))
| spl1130_62 ),
inference(avatar_component_clause,[],[f28644]) ).
fof(f28648,definition,
( spl1130_63
<=> v2_orders_2(k7_lattice3(sK177)) ),
introduced(definition,[new_symbols(definition,[spl1130_63])],[avatar_definition]) ).
fof(f28650,plain,
( ~ v2_orders_2(k7_lattice3(sK177))
| spl1130_63 ),
inference(avatar_component_clause,[],[f28648]) ).
fof(f28652,definition,
( spl1130_64
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK177)))))
| k3_tarski(X0) = k1_yellow_0(k2_yellow_1(k9_waybel_0(sK177)),X0)
| ~ v1_waybel_0(X0,k2_yellow_1(k9_waybel_0(sK177)))
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl1130_64])],[avatar_definition]) ).
fof(f28653,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK177)))))
| k3_tarski(X0) = k1_yellow_0(k2_yellow_1(k9_waybel_0(sK177)),X0)
| ~ v1_waybel_0(X0,k2_yellow_1(k9_waybel_0(sK177)))
| v1_xboole_0(X0) )
| ~ spl1130_64 ),
inference(avatar_component_clause,[],[f28652]) ).
fof(f28654,plain,
( ~ spl1130_58
| ~ spl1130_59
| ~ spl1130_60
| ~ spl1130_61
| ~ spl1130_62
| ~ spl1130_63
| spl1130_64 ),
inference(avatar_split_clause,[],[f28626,f28652,f28648,f28644,f28640,f28636,f28632,f28628]) ).
fof(f28673,plain,
( ~ l1_orders_2(sK177)
| spl1130_58 ),
inference(resolution,[],[f28630,f18436]) ).
fof(f28674,plain,
( $false
| spl1130_58 ),
inference(forward_subsumption_resolution,[],[f28673,f15836]) ).
fof(f28675,plain,
spl1130_58,
inference(avatar_contradiction_clause,[],[f28674]) ).
fof(f28676,plain,
( ~ v3_orders_2(sK177)
| ~ l1_orders_2(sK177)
| spl1130_62 ),
inference(resolution,[],[f28646,f18833]) ).
fof(f28677,plain,
( ~ l1_orders_2(sK177)
| spl1130_62 ),
inference(forward_subsumption_resolution,[],[f28676,f15840]) ).
fof(f28678,plain,
( $false
| spl1130_62 ),
inference(forward_subsumption_resolution,[],[f28677,f15836]) ).
fof(f28679,plain,
spl1130_62,
inference(avatar_contradiction_clause,[],[f28678]) ).
fof(f28680,plain,
( ~ v2_orders_2(sK177)
| ~ l1_orders_2(sK177)
| spl1130_63 ),
inference(resolution,[],[f28650,f18837]) ).
fof(f28681,plain,
( ~ l1_orders_2(sK177)
| spl1130_63 ),
inference(forward_subsumption_resolution,[],[f28680,f15841]) ).
fof(f28682,plain,
( $false
| spl1130_63 ),
inference(forward_subsumption_resolution,[],[f28681,f15836]) ).
fof(f28683,plain,
spl1130_63,
inference(avatar_contradiction_clause,[],[f28682]) ).
fof(f28700,plain,
( ~ v4_orders_2(sK177)
| ~ l1_orders_2(sK177)
| spl1130_61 ),
inference(resolution,[],[f28642,f18835]) ).
fof(f28701,plain,
( ~ l1_orders_2(sK177)
| spl1130_61 ),
inference(forward_subsumption_resolution,[],[f28700,f15839]) ).
fof(f28702,plain,
( $false
| spl1130_61 ),
inference(forward_subsumption_resolution,[],[f28701,f15836]) ).
fof(f28703,plain,
spl1130_61,
inference(avatar_contradiction_clause,[],[f28702]) ).
fof(f28823,plain,
( ~ v2_lattice3(sK177)
| ~ l1_orders_2(sK177)
| spl1130_60 ),
inference(resolution,[],[f28638,f18831]) ).
fof(f28824,plain,
( ~ l1_orders_2(sK177)
| spl1130_60 ),
inference(forward_subsumption_resolution,[],[f28823,f15837]) ).
fof(f28825,plain,
( $false
| spl1130_60 ),
inference(forward_subsumption_resolution,[],[f28824,f15836]) ).
fof(f28826,plain,
spl1130_60,
inference(avatar_contradiction_clause,[],[f28825]) ).
fof(f28842,plain,
( ~ v2_yellow_0(sK177)
| ~ l1_orders_2(sK177)
| spl1130_59 ),
inference(resolution,[],[f28634,f16031]) ).
fof(f28843,plain,
( ~ l1_orders_2(sK177)
| spl1130_59 ),
inference(forward_subsumption_resolution,[],[f28842,f15838]) ).
fof(f28844,plain,
( $false
| spl1130_59 ),
inference(forward_subsumption_resolution,[],[f28843,f15836]) ).
fof(f28845,plain,
spl1130_59,
inference(avatar_contradiction_clause,[],[f28844]) ).
fof(f28855,plain,
( k3_tarski(sK178) = k1_yellow_0(k2_yellow_1(k9_waybel_0(sK177)),sK178)
| ~ v1_waybel_0(sK178,k2_yellow_1(k9_waybel_0(sK177)))
| v1_xboole_0(sK178)
| ~ spl1130_64 ),
inference(resolution,[],[f28653,f15842]) ).
fof(f28856,plain,
( ~ v1_waybel_0(sK178,k2_yellow_1(k9_waybel_0(sK177)))
| v1_xboole_0(sK178)
| ~ spl1130_64 ),
inference(forward_subsumption_resolution,[],[f28855,f15845]) ).
fof(f28863,plain,
( v1_xboole_0(sK178)
| ~ spl1130_64 ),
inference(forward_subsumption_resolution,[],[f28856,f15843]) ).
fof(f28870,plain,
( $false
| ~ spl1130_64 ),
inference(forward_subsumption_resolution,[],[f28863,f15844]) ).
fof(f28871,plain,
~ spl1130_64,
inference(avatar_contradiction_clause,[],[f28870]) ).
cnf(s48,plain,
( ~ spl1130_58
| ~ spl1130_59
| ~ spl1130_60
| ~ spl1130_61
| ~ spl1130_62
| ~ spl1130_63
| spl1130_64 ),
inference(sat_conversion,[],[f28654]) ).
cnf(s52,plain,
spl1130_58,
inference(sat_conversion,[],[f28675]) ).
cnf(s53,plain,
spl1130_62,
inference(sat_conversion,[],[f28679]) ).
cnf(s54,plain,
spl1130_63,
inference(sat_conversion,[],[f28683]) ).
cnf(s56,plain,
spl1130_61,
inference(sat_conversion,[],[f28703]) ).
cnf(s64,plain,
spl1130_60,
inference(sat_conversion,[],[f28826]) ).
cnf(s66,plain,
spl1130_59,
inference(sat_conversion,[],[f28845]) ).
cnf(s67,plain,
~ spl1130_64,
inference(sat_conversion,[],[f28871]) ).
cnf(s72,plain,
$false,
inference(rat,[],[s48,s67,s54,s53,s56,s64,s66,s52]) ).
fof(f28877,plain,
$false,
inference(avatar_sat_refutation,[],[s72]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT347+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.41 % Computer : n004.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Sun Sep 27 14:52:23 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.46 Running first-order theorem proving
% 0.14/0.46 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.79/4.70 % (3615483)Detected formulas, will run a generic FOF schedule.
% 22.79/4.70 % (3615488)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=806476952:i=141193_2994 on theBenchmark for (2994ds/141193Mi)
% 22.79/4.70 % (3615493)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1883300319:s2a=on:i=139:gtg=position_2994 on theBenchmark for (2994ds/139Mi)
% 22.79/4.70 % (3615490)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=1910941867:i=141695:sd=1:nm=32:gsp=on:ss=included_2994 on theBenchmark for (2994ds/141695Mi)
% 22.79/4.70 % (3615489)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=700940612:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2994 on theBenchmark for (2994ds/134677Mi)
% 22.79/4.70 % (3615491)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=873469453:i=109:sd=1:ins=1:gsp=on:ss=axioms_2994 on theBenchmark for (2994ds/109Mi)
% 22.79/4.70 % (3615492)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3270785567:i=119:av=off:ss=axioms_2994 on theBenchmark for (2994ds/119Mi)
% 22.79/4.70 % (3615494)dis-21_1_sil=8000:lcm=predicate:random_seed=997026067:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2994 on theBenchmark for (2994ds/129Mi)
% 22.79/4.70 % (3615493)Instruction limit reached!
% 22.79/4.70 % (3615493)------------------------------
% 22.79/4.70 % (3615493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.79/4.70 % (3615493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/4.70 % (3615493)CaDiCaL version: 2.1.3
% 22.79/4.70 % (3615493)Termination reason: Instruction limit
% 22.79/4.70 % (3615493)Termination phase: SInE selection
% 22.79/4.70 % (3615493)Time elapsed: 0.128 s
% 22.79/4.70 % (3615493)Peak memory usage: 96 MB
% 22.79/4.70 % (3615493)Instructions burned: 139 (million)
% 22.79/4.70 % (3615491)Instruction limit reached!
% 22.79/4.70 % (3615491)------------------------------
% 22.79/4.70 % (3615491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.79/4.70 % (3615491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/4.70 % (3615491)CaDiCaL version: 2.1.3
% 22.79/4.70 % (3615491)Termination reason: Instruction limit
% 22.79/4.70 % (3615491)Termination phase: Saturation
% 22.79/4.70 % (3615491)Time elapsed: 0.124 s
% 22.79/4.70 % (3615491)Peak memory usage: 100 MB
% 22.79/4.70 % (3615491)Instructions burned: 110 (million)
% 22.79/4.70 % (3615492)Instruction limit reached!
% 22.79/4.70 % (3615492)------------------------------
% 22.79/4.70 % (3615492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.79/4.70 % (3615492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/4.70 % (3615492)CaDiCaL version: 2.1.3
% 22.79/4.70 % (3615492)Termination reason: Instruction limit
% 22.79/4.70 % (3615492)Termination phase: Function definition elimination
% 22.79/4.70 % (3615492)Time elapsed: 0.138 s
% 22.79/4.70 % (3615492)Peak memory usage: 100 MB
% 22.79/4.70 % (3615492)Instructions burned: 119 (million)
% 22.79/4.70 % (3615494)Instruction limit reached!
% 22.79/4.70 % (3615494)------------------------------
% 22.79/4.70 % (3615494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.79/4.70 % (3615494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/4.70 % (3615494)CaDiCaL version: 2.1.3
% 22.79/4.70 % (3615494)Termination reason: Instruction limit
% 22.79/4.70 % (3615494)Termination phase: Preprocessing 2
% 22.79/4.70 % (3615494)Time elapsed: 0.158 s
% 22.79/4.70 % (3615494)Peak memory usage: 98 MB
% 22.79/4.70 % (3615494)Instructions burned: 129 (million)
% 22.79/4.70 % (3615502)lrs+10_1_sil=8000:sp=occurrence:random_seed=3594040143:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 22.79/4.70 % (3615503)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1941397608:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 22.79/4.70 % (3615504)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2280544495:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 22.79/4.70 % (3615505)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=1818277425:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 22.79/4.70 % (3615502)Instruction limit reached!
% 30.74/5.91 % (3615502)------------------------------
% 30.74/5.91 % (3615502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.91 % (3615502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.91 % (3615502)CaDiCaL version: 2.1.3
% 30.74/5.91 % (3615502)Termination reason: Instruction limit
% 30.74/5.91 % (3615502)Termination phase: Saturation
% 30.74/5.91 % (3615502)Time elapsed: 0.273 s
% 30.74/5.91 % (3615502)Peak memory usage: 104 MB
% 30.74/5.91 % (3615502)Instructions burned: 285 (million)
% 30.74/5.91 % (3615503)Instruction limit reached!
% 30.74/5.91 % (3615503)------------------------------
% 30.74/5.91 % (3615503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.91 % (3615503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.91 % (3615503)CaDiCaL version: 2.1.3
% 30.74/5.91 % (3615503)Termination reason: Instruction limit
% 30.74/5.91 % (3615503)Termination phase: Preprocessing 3
% 30.74/5.91 % (3615503)Time elapsed: 0.153 s
% 30.74/5.91 % (3615503)Peak memory usage: 97 MB
% 30.74/5.91 % (3615503)Instructions burned: 157 (million)
% 30.74/5.91 % (3615505)Instruction limit reached!
% 30.74/5.91 % (3615505)------------------------------
% 30.74/5.91 % (3615505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.91 % (3615505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.91 % (3615505)CaDiCaL version: 2.1.3
% 30.74/5.91 % (3615505)Termination reason: Instruction limit
% 30.74/5.91 % (3615505)Termination phase: Unused predicate definition removal
% 30.74/5.91 % (3615505)Time elapsed: 0.255 s
% 30.74/5.91 % (3615505)Peak memory usage: 98 MB
% 30.74/5.91 % (3615505)Instructions burned: 248 (million)
% 30.74/5.91 % (3615504)Instruction limit reached!
% 30.74/5.91 % (3615504)------------------------------
% 30.74/5.91 % (3615504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.91 % (3615504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.91 % (3615504)CaDiCaL version: 2.1.3
% 30.74/5.91 % (3615504)Termination reason: Instruction limit
% 30.74/5.91 % (3615504)Termination phase: Saturation
% 30.74/5.91 % (3615504)Time elapsed: 0.357 s
% 30.74/5.91 % (3615504)Peak memory usage: 103 MB
% 30.74/5.91 % (3615504)Instructions burned: 326 (million)
% 30.74/5.91 % (3615510)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1217852913:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2986 on theBenchmark for (2986ds/294Mi)
% 30.74/5.91 % (3615511)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=149851254:i=2350_2986 on theBenchmark for (2986ds/2350Mi)
% 30.74/5.91 % (3615513)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3211067762:i=127:av=off:fsr=off:sup=off_2983 on theBenchmark for (2983ds/127Mi)
% 30.74/5.91 % (3615512)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3110171745:cts=off:i=113:fsr=off:ss=included:sgt=4_2984 on theBenchmark for (2984ds/113Mi)
% 30.74/5.91 % (3615513)Instruction limit reached!
% 30.74/5.91 % (3615513)------------------------------
% 30.74/5.91 % (3615513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.91 % (3615513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.91 % (3615513)CaDiCaL version: 2.1.3
% 30.74/5.91 % (3615513)Termination reason: Instruction limit
% 30.74/5.91 % (3615513)Termination phase: Naming
% 30.74/5.91 % (3615513)Time elapsed: 0.113 s
% 30.74/5.91 % (3615513)Peak memory usage: 105 MB
% 30.74/5.91 % (3615513)Instructions burned: 128 (million)
% 30.74/5.91 % (3615510)Instruction limit reached!
% 30.74/5.91 % (3615510)------------------------------
% 30.74/5.91 % (3615510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.91 % (3615510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.91 % (3615510)CaDiCaL version: 2.1.3
% 30.74/5.91 % (3615510)Termination reason: Instruction limit
% 30.74/5.91 % (3615510)Termination phase: Saturation
% 30.74/5.91 % (3615510)Time elapsed: 0.296 s
% 30.74/5.91 % (3615510)Peak memory usage: 104 MB
% 30.74/5.91 % (3615510)Instructions burned: 294 (million)
% 30.74/5.91 % (3615512)Instruction limit reached!
% 30.74/5.91 % (3615512)------------------------------
% 30.74/5.91 % (3615512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.74/5.91 % (3615512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.74/5.91 % (3615512)CaDiCaL version: 2.1.3
% 48.26/9.33 % (3615512)Termination reason: Instruction limit
% 48.26/9.33 % (3615512)Termination phase: Function definition elimination
% 48.26/9.33 % (3615512)Time elapsed: 0.134 s
% 48.26/9.33 % (3615512)Peak memory usage: 99 MB
% 48.26/9.33 % (3615512)Instructions burned: 113 (million)
% 48.26/9.33 % (3615518)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1357252580:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2980 on theBenchmark for (2980ds/114Mi)
% 48.26/9.33 % (3615519)lrs+10_1_sil=8000:sp=occurrence:random_seed=615308679:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2980 on theBenchmark for (2980ds/907Mi)
% 48.26/9.33 % (3615520)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2892921412:i=437:sd=1:aac=none:ss=included_2980 on theBenchmark for (2980ds/437Mi)
% 48.26/9.33 % (3615518)Instruction limit reached!
% 48.26/9.33 % (3615518)------------------------------
% 48.26/9.33 % (3615518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.26/9.33 % (3615518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.26/9.33 % (3615518)CaDiCaL version: 2.1.3
% 48.26/9.33 % (3615518)Termination reason: Instruction limit
% 48.26/9.33 % (3615518)Termination phase: Initialization
% 48.26/9.33 % (3615518)Time elapsed: 0.098 s
% 48.26/9.33 % (3615518)Peak memory usage: 96 MB
% 48.26/9.33 % (3615518)Instructions burned: 115 (million)
% 48.26/9.33 % (3615524)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3565048993:i=5202:ss=axioms:sgt=16_2977 on theBenchmark for (2977ds/5202Mi)
% 48.26/9.33 % (3615520)Instruction limit reached!
% 48.26/9.33 % (3615520)------------------------------
% 48.26/9.33 % (3615520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.26/9.33 % (3615520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.26/9.33 % (3615520)CaDiCaL version: 2.1.3
% 48.26/9.33 % (3615520)Termination reason: Instruction limit
% 48.26/9.33 % (3615520)Termination phase: Saturation
% 48.26/9.33 % (3615520)Time elapsed: 0.474 s
% 48.26/9.33 % (3615520)Peak memory usage: 102 MB
% 48.26/9.33 % (3615520)Instructions burned: 437 (million)
% 48.26/9.33 % (3615526)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2106550894:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2972 on theBenchmark for (2972ds/134Mi)
% 48.26/9.33 % (3615526)Instruction limit reached!
% 48.26/9.33 % (3615526)------------------------------
% 48.26/9.33 % (3615526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.26/9.33 % (3615526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.26/9.33 % (3615526)CaDiCaL version: 2.1.3
% 48.26/9.33 % (3615526)Termination reason: Instruction limit
% 48.26/9.33 % (3615526)Termination phase: Saturation
% 48.26/9.33 % (3615526)Time elapsed: 0.101 s
% 48.26/9.33 % (3615526)Peak memory usage: 102 MB
% 48.26/9.33 % (3615526)Instructions burned: 139 (million)
% 48.26/9.33 % (3615519)Instruction limit reached!
% 48.26/9.33 % (3615519)------------------------------
% 48.26/9.33 % (3615519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.26/9.33 % (3615519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.26/9.33 % (3615519)CaDiCaL version: 2.1.3
% 48.26/9.33 % (3615519)Termination reason: Instruction limit
% 48.26/9.33 % (3615519)Termination phase: Saturation
% 48.26/9.33 % (3615519)Time elapsed: 0.903 s
% 48.26/9.33 % (3615519)Peak memory usage: 115 MB
% 48.26/9.33 % (3615519)Instructions burned: 907 (million)
% 48.26/9.33 % (3615528)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1177027891:st=8:i=592:sd=3:ep=RST:ss=axioms_2969 on theBenchmark for (2969ds/592Mi)
% 48.26/9.33 % (3615529)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1880726779:st=3:i=13193:sd=3:ss=axioms_2968 on theBenchmark for (2968ds/13193Mi)
% 48.26/9.33 % (3615528)Instruction limit reached!
% 48.26/9.33 % (3615528)------------------------------
% 48.26/9.33 % (3615528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.26/9.33 % (3615528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.26/9.33 % (3615528)CaDiCaL version: 2.1.3
% 48.26/9.33 % (3615528)Termination reason: Instruction limit
% 48.26/9.33 % (3615528)Termination phase: Property scanning
% 48.26/9.33 % (3615528)Time elapsed: 0.371 s
% 48.26/9.33 % (3615528)Peak memory usage: 114 MB
% 48.26/9.33 % (3615528)Instructions burned: 593 (million)
% 48.26/9.33 % (3615511)Instruction limit reached!
% 48.26/9.33 % (3615511)------------------------------
% 48.26/9.33 % (3615511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.26/9.33 % (3615511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.26/9.33 % (3615511)CaDiCaL version: 2.1.3
% 48.26/9.33 % (3615511)Termination reason: Instruction limit
% 48.26/9.33 % (3615511)Termination phase: Saturation
% 48.26/9.33 % (3615511)Time elapsed: 2.037 s
% 48.26/9.33 % (3615511)Peak memory usage: 268 MB
% 48.26/9.33 % (3615511)Instructions burned: 2350 (million)
% 48.26/9.33 % (3615532)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=389264877:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2964 on theBenchmark for (2964ds/125Mi)
% 48.26/9.33 % (3615532)Instruction limit reached!
% 48.26/9.33 % (3615532)------------------------------
% 48.26/9.33 % (3615532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.26/9.33 % (3615532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.26/9.33 % (3615532)CaDiCaL version: 2.1.3
% 48.26/9.33 % (3615532)Termination reason: Instruction limit
% 48.26/9.33 % (3615532)Termination phase: SInE selection
% 48.26/9.33 % (3615532)Time elapsed: 0.061 s
% 48.26/9.33 % (3615532)Peak memory usage: 96 MB
% 48.26/9.33 % (3615532)Instructions burned: 125 (million)
% 48.26/9.33 % (3615534)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=435757234:i=134:gtgl=5:slsql=off:gtg=exists_sym_2962 on theBenchmark for (2962ds/134Mi)
% 48.26/9.33 % (3615535)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=116174061:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2962 on theBenchmark for (2962ds/141Mi)
% 48.26/9.33 % (3615534)Instruction limit reached!
% 48.26/9.33 % (3615534)------------------------------
% 48.26/9.33 % (3615534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.26/9.33 % (3615534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.26/9.33 % (3615534)CaDiCaL version: 2.1.3
% 48.26/9.33 % (3615534)Termination reason: Instruction limit
% 48.26/9.33 % (3615534)Termination phase: Initialization
% 48.26/9.33 % (3615534)Time elapsed: 0.108 s
% 48.26/9.33 % (3615534)Peak memory usage: 96 MB
% 48.26/9.33 % (3615534)Instructions burned: 134 (million)
% 48.26/9.33 % (3615535)Instruction limit reached!
% 48.26/9.33 % (3615535)------------------------------
% 48.26/9.33 % (3615535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.26/9.33 % (3615535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.26/9.33 % (3615535)CaDiCaL version: 2.1.3
% 48.26/9.33 % (3615535)Termination reason: Instruction limit
% 48.26/9.33 % (3615535)Termination phase: Saturation
% 48.26/9.33 % (3615535)Time elapsed: 0.097 s
% 48.26/9.33 % (3615535)Peak memory usage: 101 MB
% 48.26/9.33 % (3615535)Instructions burned: 142 (million)
% 48.26/9.33 % (3615538)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2415007192:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2959 on theBenchmark for (2959ds/431Mi)
% 48.26/9.33 % (3615539)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=3379989859:i=6060:aac=none:ins=25_2959 on theBenchmark for (2959ds/6060Mi)
% 48.26/9.33 % (3615538)Instruction limit reached!
% 48.26/9.33 % (3615538)------------------------------
% 48.26/9.33 % (3615538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.26/9.33 % (3615538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.26/9.33 % (3615538)CaDiCaL version: 2.1.3
% 48.26/9.33 % (3615538)Termination reason: Instruction limit
% 48.26/9.33 % (3615538)Termination phase: Saturation
% 48.26/9.33 % (3615538)Time elapsed: 0.292 s
% 48.26/9.33 % (3615538)Peak memory usage: 103 MB
% 48.26/9.33 % (3615538)Instructions burned: 432 (million)
% 48.26/9.33 % (3615542)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=4106388533:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2954 on theBenchmark for (2954ds/150Mi)
% 48.26/9.33 % (3615542)Instruction limit reached!
% 48.26/9.33 % (3615542)------------------------------
% 48.26/9.33 % (3615542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.26/9.33 % (3615542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.26/9.33 % (3615542)CaDiCaL version: 2.1.3
% 48.26/9.33 % (3615542)Termination reason: Instruction limit
% 48.26/9.33 % (3615542)Termination phase: Preprocessing 2
% 48.26/9.33 % (3615542)Time elapsed: 0.228 s
% 48.26/9.33 % (3615542)Peak memory usage: 103 MB
% 48.26/9.33 % (3615542)Instructions burned: 150 (million)
% 48.26/9.33 % (3615544)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1361495757:i=14155:bd=all_2950 on theBenchmark for (2950ds/14155Mi)
% 48.26/9.33 % (3615524)Instruction limit reached!
% 48.26/9.33 % (3615524)------------------------------
% 48.26/9.33 % (3615524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.26/9.33 % (3615524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.26/9.33 % (3615524)CaDiCaL version: 2.1.3
% 48.26/9.33 % (3615524)Termination reason: Instruction limit
% 48.26/9.33 % (3615524)Termination phase: Saturation
% 48.26/9.33 % (3615524)Time elapsed: 4.787 s
% 48.26/9.33 % (3615524)Peak memory usage: 183 MB
% 48.26/9.33 % (3615524)Instructions burned: 5204 (million)
% 48.26/9.33 % (3615546)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=129343158:i=667:av=off:fsr=off_2926 on theBenchmark for (2926ds/667Mi)
% 48.26/9.33 % (3615529)First to succeed.
% 48.26/9.33 % (3615529)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3615483"
% 48.26/9.33 % (3615546)Instruction limit reached!
% 48.26/9.33 % (3615546)------------------------------
% 48.26/9.33 % (3615546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.26/9.33 % (3615546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.26/9.33 % (3615546)CaDiCaL version: 2.1.3
% 48.26/9.33 % (3615546)Termination reason: Instruction limit
% 48.26/9.33 % (3615546)Termination phase: Property scanning
% 48.26/9.33 % (3615546)Time elapsed: 0.429 s
% 48.26/9.33 % (3615546)Peak memory usage: 120 MB
% 48.26/9.33 % (3615546)Instructions burned: 668 (million)
% 48.26/9.33 % (3615548)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=1609756352:s2a=on:i=185:s2at=1.8:fdi=4_2920 on theBenchmark for (2920ds/185Mi)
% 48.26/9.33 % (3615529)Refutation found. Thanks to Tanya!
% 48.26/9.33 % SZS status Theorem for theBenchmark
% 48.26/9.33 % SZS output start Proof for theBenchmark
% See solution above
% 56.07/9.55 % (3615529)------------------------------
% 56.07/9.55 % (3615529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.07/9.55 % (3615529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.07/9.55 % (3615529)CaDiCaL version: 2.1.3
% 56.07/9.55 % (3615529)Termination reason: Refutation
% 56.07/9.55 % (3615529)Time elapsed: 4.444 s
% 56.07/9.55 % (3615529)Peak memory usage: 243 MB
% 56.07/9.55 % (3615529)Instructions burned: 4532 (million)
% 56.07/9.55 % (3615529)------------------------------
% 56.07/9.55 % (3615529)------------------------------
% 56.07/9.55 % (3615483)Success in time 8.347 s
% 56.07/9.55 % Vampire exiting
%------------------------------------------------------------------------------