%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT351+3 : 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 : n018.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:12 AM UTC 2026
% Result : Theorem 21.02s 5.14s
% Output : Refutation 21.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 12
% Syntax : Number of formulae : 107 ( 41 unt; 0 def)
% Number of atoms : 642 ( 35 equ)
% Maximal formula atoms : 21 ( 6 avg)
% Number of connectives : 917 ( 382 ~; 367 |; 157 &)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 8 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 21 ( 19 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-1 aty)
% Number of variables : 139 ( 133 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11561,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_lattice3) ).
fof(f15074,axiom,
! [X0] :
( v1_orders_2(k2_yellow_1(X0))
& v2_orders_2(k2_yellow_1(X0))
& v3_orders_2(k2_yellow_1(X0))
& v4_orders_2(k2_yellow_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_yellow_1) ).
fof(f15095,axiom,
! [X0] : k3_yellow_1(X0) = k2_yellow_1(k1_zfmisc_1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_yellow_1) ).
fof(f15126,axiom,
! [X0] :
( v1_orders_2(k2_yellow_1(X0))
& l1_orders_2(k2_yellow_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_yellow_1) ).
fof(f16000,axiom,
! [X0] :
( ~ v3_struct_0(k3_yellow_1(X0))
& v1_orders_2(k3_yellow_1(X0))
& v2_orders_2(k3_yellow_1(X0))
& v3_orders_2(k3_yellow_1(X0))
& v4_orders_2(k3_yellow_1(X0))
& v1_yellow_0(k3_yellow_1(X0))
& v2_yellow_0(k3_yellow_1(X0))
& v3_yellow_0(k3_yellow_1(X0))
& v7_waybel_0(k3_yellow_1(X0))
& v24_waybel_0(k3_yellow_1(X0))
& v25_waybel_0(k3_yellow_1(X0))
& ~ v1_yellow_3(k3_yellow_1(X0))
& v1_lattice3(k3_yellow_1(X0))
& v2_lattice3(k3_yellow_1(X0))
& v3_lattice3(k3_yellow_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc8_yellow_6) ).
fof(f17255,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v2_lattice3(X0)
& v2_yellow_0(X0)
& l1_orders_2(X0) )
=> ( ~ v3_struct_0(k2_yellow_1(k9_waybel_0(X0)))
& v1_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v2_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v3_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v4_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v2_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v3_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v1_yellow_0(k2_yellow_1(k9_waybel_0(X0)))
& v24_waybel_0(k2_yellow_1(k9_waybel_0(X0)))
& v25_waybel_0(k2_yellow_1(k9_waybel_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_waybel16) ).
fof(f17790,axiom,
! [X0] :
( ( ~ v3_struct_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) )
=> ( ~ v3_struct_0(k2_yellow_1(k9_waybel_0(X0)))
& v1_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v2_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v3_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v4_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v1_yellow_0(k2_yellow_1(k9_waybel_0(X0)))
& v2_yellow_0(k2_yellow_1(k9_waybel_0(X0)))
& v3_yellow_0(k2_yellow_1(k9_waybel_0(X0)))
& v24_waybel_0(k2_yellow_1(k9_waybel_0(X0)))
& v25_waybel_0(k2_yellow_1(k9_waybel_0(X0)))
& v1_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v2_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v3_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v3_waybel_3(k2_yellow_1(k9_waybel_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_waybel22) ).
fof(f17795,axiom,
! [X0] : k1_waybel22(X0) = a_1_0_waybel22(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_waybel22) ).
fof(f17797,axiom,
! [X0] : k1_card_1(k1_waybel22(X0)) = k1_card_1(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_waybel22) ).
fof(f17807,axiom,
! [X0] : r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),k1_waybel22(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t16_waybel22) ).
fof(f17808,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& v3_waybel_3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1) )
=> ! [X2,X3] :
( ( r1_waybel22(X0,X2)
& r1_waybel22(X1,X3)
& k1_card_1(X2) = k1_card_1(X3) )
=> r5_waybel_1(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t17_waybel22) ).
fof(f17809,conjecture,
! [X0,X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( r1_waybel22(X1,X2)
& k1_card_1(X2) = k1_card_1(X0) )
=> r5_waybel_1(X1,k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_waybel22) ).
fof(f17810,negated_conjecture,
~ ! [X0,X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( r1_waybel22(X1,X2)
& k1_card_1(X2) = k1_card_1(X0) )
=> r5_waybel_1(X1,k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))) ) ),
inference(negated_conjecture,[status(cth)],[f17809]) ).
fof(f17888,plain,
! [X0] :
( ( ~ v3_struct_0(k2_yellow_1(k9_waybel_0(X0)))
& v1_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v2_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v3_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v4_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v1_yellow_0(k2_yellow_1(k9_waybel_0(X0)))
& v2_yellow_0(k2_yellow_1(k9_waybel_0(X0)))
& v3_yellow_0(k2_yellow_1(k9_waybel_0(X0)))
& v24_waybel_0(k2_yellow_1(k9_waybel_0(X0)))
& v25_waybel_0(k2_yellow_1(k9_waybel_0(X0)))
& v1_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v2_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v3_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v3_waybel_3(k2_yellow_1(k9_waybel_0(X0))) )
| v3_struct_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,[],[f17790]) ).
fof(f17889,plain,
! [X0] :
( ( ~ v3_struct_0(k2_yellow_1(k9_waybel_0(X0)))
& v1_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v2_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v3_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v4_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v1_yellow_0(k2_yellow_1(k9_waybel_0(X0)))
& v2_yellow_0(k2_yellow_1(k9_waybel_0(X0)))
& v3_yellow_0(k2_yellow_1(k9_waybel_0(X0)))
& v24_waybel_0(k2_yellow_1(k9_waybel_0(X0)))
& v25_waybel_0(k2_yellow_1(k9_waybel_0(X0)))
& v1_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v2_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v3_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v3_waybel_3(k2_yellow_1(k9_waybel_0(X0))) )
| v3_struct_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,[],[f17888]) ).
fof(f17915,plain,
! [X0] :
( ! [X1] :
( ! [X2,X3] :
( r5_waybel_1(X0,X1)
| ~ r1_waybel22(X0,X2)
| ~ r1_waybel22(X1,X3)
| k1_card_1(X2) != k1_card_1(X3) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ v3_waybel_3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f17808]) ).
fof(f17916,plain,
! [X0] :
( ! [X1] :
( ! [X2,X3] :
( r5_waybel_1(X0,X1)
| ~ r1_waybel22(X0,X2)
| ~ r1_waybel22(X1,X3)
| k1_card_1(X2) != k1_card_1(X3) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ v3_waybel_3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f17915]) ).
fof(f17917,plain,
? [X0,X1] :
( ? [X2] :
( ~ r5_waybel_1(X1,k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))
& r1_waybel22(X1,X2)
& k1_card_1(X2) = k1_card_1(X0) )
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1) ),
inference(ennf_transformation,[],[f17810]) ).
fof(f17918,plain,
? [X0,X1] :
( ? [X2] :
( ~ r5_waybel_1(X1,k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))
& r1_waybel22(X1,X2)
& k1_card_1(X2) = k1_card_1(X0) )
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1) ),
inference(flattening,[],[f17917]) ).
fof(f18018,plain,
! [X0] :
( ( ~ v3_struct_0(k2_yellow_1(k9_waybel_0(X0)))
& v1_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v2_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v3_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v4_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v2_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v3_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v1_yellow_0(k2_yellow_1(k9_waybel_0(X0)))
& v24_waybel_0(k2_yellow_1(k9_waybel_0(X0)))
& v25_waybel_0(k2_yellow_1(k9_waybel_0(X0))) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f17255]) ).
fof(f18019,plain,
! [X0] :
( ( ~ v3_struct_0(k2_yellow_1(k9_waybel_0(X0)))
& v1_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v2_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v3_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v4_orders_2(k2_yellow_1(k9_waybel_0(X0)))
& v2_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v3_lattice3(k2_yellow_1(k9_waybel_0(X0)))
& v1_yellow_0(k2_yellow_1(k9_waybel_0(X0)))
& v24_waybel_0(k2_yellow_1(k9_waybel_0(X0)))
& v25_waybel_0(k2_yellow_1(k9_waybel_0(X0))) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f18018]) ).
fof(f18071,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f11561]) ).
fof(f18072,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f18071]) ).
fof(f22200,plain,
( ~ r5_waybel_1(sK44,k2_yellow_1(k9_waybel_0(k3_yellow_1(sK43))))
& r1_waybel22(sK44,sK45)
& k1_card_1(sK43) = k1_card_1(sK45)
& v2_orders_2(sK44)
& v3_orders_2(sK44)
& v4_orders_2(sK44)
& v1_lattice3(sK44)
& v2_lattice3(sK44)
& v3_lattice3(sK44)
& v3_waybel_3(sK44)
& l1_orders_2(sK44) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43,sK44,sK45]),skolemize(X0,sK43),skolemize(X1,sK44),skolemize(X2,sK45)],[f17918]) ).
fof(f23652,plain,
! [X0] :
( v3_waybel_3(k2_yellow_1(k9_waybel_0(X0)))
| v3_struct_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(cnf_transformation,[],[f17889]) ).
fof(f23655,plain,
! [X0] :
( v1_lattice3(k2_yellow_1(k9_waybel_0(X0)))
| v3_struct_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(cnf_transformation,[],[f17889]) ).
fof(f23685,plain,
! [X0] : k1_waybel22(X0) = a_1_0_waybel22(X0),
inference(cnf_transformation,[],[f17795]) ).
fof(f23687,plain,
! [X0] : k1_card_1(X0) = k1_card_1(k1_waybel22(X0)),
inference(cnf_transformation,[],[f17797]) ).
fof(f23709,plain,
! [X0] : r1_waybel22(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),k1_waybel22(X0)),
inference(cnf_transformation,[],[f17807]) ).
fof(f23710,plain,
! [X2,X3,X0,X1] :
( ~ v3_waybel_3(X0)
| ~ r1_waybel22(X0,X2)
| ~ r1_waybel22(X1,X3)
| k1_card_1(X2) != k1_card_1(X3)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| r5_waybel_1(X0,X1)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f17916]) ).
fof(f23711,plain,
l1_orders_2(sK44),
inference(cnf_transformation,[],[f22200]) ).
fof(f23712,plain,
v3_waybel_3(sK44),
inference(cnf_transformation,[],[f22200]) ).
fof(f23713,plain,
v3_lattice3(sK44),
inference(cnf_transformation,[],[f22200]) ).
fof(f23714,plain,
v2_lattice3(sK44),
inference(cnf_transformation,[],[f22200]) ).
fof(f23715,plain,
v1_lattice3(sK44),
inference(cnf_transformation,[],[f22200]) ).
fof(f23716,plain,
v4_orders_2(sK44),
inference(cnf_transformation,[],[f22200]) ).
fof(f23717,plain,
v3_orders_2(sK44),
inference(cnf_transformation,[],[f22200]) ).
fof(f23718,plain,
v2_orders_2(sK44),
inference(cnf_transformation,[],[f22200]) ).
fof(f23719,plain,
k1_card_1(sK43) = k1_card_1(sK45),
inference(cnf_transformation,[],[f22200]) ).
fof(f23720,plain,
r1_waybel22(sK44,sK45),
inference(cnf_transformation,[],[f22200]) ).
fof(f23721,plain,
~ r5_waybel_1(sK44,k2_yellow_1(k9_waybel_0(k3_yellow_1(sK43)))),
inference(cnf_transformation,[],[f22200]) ).
fof(f23831,plain,
! [X0] : k3_yellow_1(X0) = k2_yellow_1(k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f15095]) ).
fof(f23878,plain,
! [X0] :
( ~ v2_yellow_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| v3_lattice3(k2_yellow_1(k9_waybel_0(X0)))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18019]) ).
fof(f23879,plain,
! [X0] :
( ~ v2_yellow_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| v2_lattice3(k2_yellow_1(k9_waybel_0(X0)))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18019]) ).
fof(f23886,plain,
! [X0] : l1_orders_2(k2_yellow_1(X0)),
inference(cnf_transformation,[],[f15126]) ).
fof(f23899,plain,
! [X0] : v4_orders_2(k2_yellow_1(X0)),
inference(cnf_transformation,[],[f15074]) ).
fof(f23900,plain,
! [X0] : v3_orders_2(k2_yellow_1(X0)),
inference(cnf_transformation,[],[f15074]) ).
fof(f23901,plain,
! [X0] : v2_orders_2(k2_yellow_1(X0)),
inference(cnf_transformation,[],[f15074]) ).
fof(f23974,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18072]) ).
fof(f28391,plain,
! [X0] : v2_lattice3(k3_yellow_1(X0)),
inference(cnf_transformation,[],[f16000]) ).
fof(f28398,plain,
! [X0] : v2_yellow_0(k3_yellow_1(X0)),
inference(cnf_transformation,[],[f16000]) ).
fof(f28400,plain,
! [X0] : v4_orders_2(k3_yellow_1(X0)),
inference(cnf_transformation,[],[f16000]) ).
fof(f28401,plain,
! [X0] : v3_orders_2(k3_yellow_1(X0)),
inference(cnf_transformation,[],[f16000]) ).
fof(f28402,plain,
! [X0] : v2_orders_2(k3_yellow_1(X0)),
inference(cnf_transformation,[],[f16000]) ).
fof(f30220,plain,
! [X0] : k1_card_1(X0) = k1_card_1(a_1_0_waybel22(X0)),
inference(definition_unfolding,[],[f23687,f23685]) ).
fof(f30240,plain,
! [X0] : r1_waybel22(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),a_1_0_waybel22(X0)),
inference(definition_unfolding,[],[f23709,f23831,f23685]) ).
fof(f30241,plain,
~ r5_waybel_1(sK44,k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK43))))),
inference(definition_unfolding,[],[f23721,f23831]) ).
fof(f31491,plain,
! [X0] : v2_orders_2(k2_yellow_1(k1_zfmisc_1(X0))),
inference(definition_unfolding,[],[f28402,f23831]) ).
fof(f31492,plain,
! [X0] : v3_orders_2(k2_yellow_1(k1_zfmisc_1(X0))),
inference(definition_unfolding,[],[f28401,f23831]) ).
fof(f31493,plain,
! [X0] : v4_orders_2(k2_yellow_1(k1_zfmisc_1(X0))),
inference(definition_unfolding,[],[f28400,f23831]) ).
fof(f31495,plain,
! [X0] : v2_yellow_0(k2_yellow_1(k1_zfmisc_1(X0))),
inference(definition_unfolding,[],[f28398,f23831]) ).
fof(f31502,plain,
! [X0] : v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0))),
inference(definition_unfolding,[],[f28391,f23831]) ).
fof(f32660,plain,
! [X0] :
( ~ v2_yellow_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| v3_waybel_3(k2_yellow_1(k9_waybel_0(X0)))
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f23652,f23974]) ).
fof(f32661,plain,
! [X0] :
( ~ v2_yellow_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| v1_lattice3(k2_yellow_1(k9_waybel_0(X0)))
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f23655,f23974]) ).
fof(f33064,plain,
! [X2,X0,X1] :
( ~ r1_waybel22(sK44,X0)
| ~ r1_waybel22(X1,X2)
| k1_card_1(X0) != k1_card_1(X2)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(sK44)
| ~ v3_orders_2(sK44)
| ~ v4_orders_2(sK44)
| ~ v1_lattice3(sK44)
| ~ v2_lattice3(sK44)
| ~ v3_lattice3(sK44)
| r5_waybel_1(sK44,X1)
| ~ l1_orders_2(sK44) ),
inference(resolution,[],[f23710,f23712]) ).
fof(f33070,plain,
! [X2,X0,X1] :
( ~ r1_waybel22(sK44,X0)
| ~ r1_waybel22(X1,X2)
| k1_card_1(X0) != k1_card_1(X2)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v3_orders_2(sK44)
| ~ v4_orders_2(sK44)
| ~ v1_lattice3(sK44)
| ~ v2_lattice3(sK44)
| ~ v3_lattice3(sK44)
| r5_waybel_1(sK44,X1)
| ~ l1_orders_2(sK44) ),
inference(forward_subsumption_resolution,[],[f33064,f23718]) ).
fof(f33071,plain,
! [X2,X0,X1] :
( ~ r1_waybel22(sK44,X0)
| ~ r1_waybel22(X1,X2)
| k1_card_1(X0) != k1_card_1(X2)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v4_orders_2(sK44)
| ~ v1_lattice3(sK44)
| ~ v2_lattice3(sK44)
| ~ v3_lattice3(sK44)
| r5_waybel_1(sK44,X1)
| ~ l1_orders_2(sK44) ),
inference(forward_subsumption_resolution,[],[f33070,f23717]) ).
fof(f33072,plain,
! [X2,X0,X1] :
( ~ r1_waybel22(sK44,X0)
| ~ r1_waybel22(X1,X2)
| k1_card_1(X0) != k1_card_1(X2)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v1_lattice3(sK44)
| ~ v2_lattice3(sK44)
| ~ v3_lattice3(sK44)
| r5_waybel_1(sK44,X1)
| ~ l1_orders_2(sK44) ),
inference(forward_subsumption_resolution,[],[f33071,f23716]) ).
fof(f33073,plain,
! [X2,X0,X1] :
( ~ r1_waybel22(sK44,X0)
| ~ r1_waybel22(X1,X2)
| k1_card_1(X0) != k1_card_1(X2)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(sK44)
| ~ v3_lattice3(sK44)
| r5_waybel_1(sK44,X1)
| ~ l1_orders_2(sK44) ),
inference(forward_subsumption_resolution,[],[f33072,f23715]) ).
fof(f33074,plain,
! [X2,X0,X1] :
( ~ r1_waybel22(sK44,X0)
| ~ r1_waybel22(X1,X2)
| k1_card_1(X0) != k1_card_1(X2)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v3_lattice3(sK44)
| r5_waybel_1(sK44,X1)
| ~ l1_orders_2(sK44) ),
inference(forward_subsumption_resolution,[],[f33073,f23714]) ).
fof(f33075,plain,
! [X2,X0,X1] :
( ~ r1_waybel22(sK44,X0)
| ~ r1_waybel22(X1,X2)
| k1_card_1(X0) != k1_card_1(X2)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| r5_waybel_1(sK44,X1)
| ~ l1_orders_2(sK44) ),
inference(forward_subsumption_resolution,[],[f33074,f23713]) ).
fof(f33076,plain,
! [X2,X0,X1] :
( ~ r1_waybel22(sK44,X0)
| ~ r1_waybel22(X1,X2)
| k1_card_1(X0) != k1_card_1(X2)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| r5_waybel_1(sK44,X1) ),
inference(forward_subsumption_resolution,[],[f33075,f23711]) ).
fof(f33077,plain,
! [X0,X1] :
( ~ r1_waybel22(X0,X1)
| k1_card_1(X1) != k1_card_1(sK45)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ v3_waybel_3(X0)
| ~ l1_orders_2(X0)
| r5_waybel_1(sK44,X0) ),
inference(resolution,[],[f33076,f23720]) ).
fof(f33078,plain,
! [X0,X1] :
( ~ v3_waybel_3(X0)
| ~ r1_waybel22(X0,X1)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| k1_card_1(X1) != k1_card_1(sK43)
| ~ l1_orders_2(X0)
| r5_waybel_1(sK44,X0) ),
inference(forward_demodulation,[],[f33077,f23719]) ).
fof(f33802,plain,
! [X0] :
( ~ v2_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v3_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v4_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0)))
| v3_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(resolution,[],[f31495,f23878]) ).
fof(f33803,plain,
! [X0] :
( ~ v2_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v3_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v4_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0)))
| v2_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(resolution,[],[f31495,f23879]) ).
fof(f33804,plain,
! [X0] :
( ~ v2_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v3_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v4_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| v1_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(resolution,[],[f31495,f32661]) ).
fof(f33805,plain,
! [X0] :
( ~ v2_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v3_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v4_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| v3_waybel_3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(resolution,[],[f31495,f32660]) ).
fof(f33806,plain,
! [X0] :
( ~ v3_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v4_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| v3_waybel_3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(forward_subsumption_resolution,[],[f33805,f31491]) ).
fof(f33807,plain,
! [X0] :
( ~ v3_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v4_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| v1_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(forward_subsumption_resolution,[],[f33804,f31491]) ).
fof(f33808,plain,
! [X0] :
( ~ v3_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v4_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0)))
| v2_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(forward_subsumption_resolution,[],[f33803,f31491]) ).
fof(f33809,plain,
! [X0] :
( ~ v3_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v4_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0)))
| v3_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(forward_subsumption_resolution,[],[f33802,f31491]) ).
fof(f33811,plain,
! [X0] :
( ~ v4_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| v3_waybel_3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(forward_subsumption_resolution,[],[f33806,f31492]) ).
fof(f33812,plain,
! [X0] :
( ~ v4_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| v1_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(forward_subsumption_resolution,[],[f33807,f31492]) ).
fof(f33813,plain,
! [X0] :
( ~ v4_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0)))
| v2_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(forward_subsumption_resolution,[],[f33808,f31492]) ).
fof(f33814,plain,
! [X0] :
( ~ v4_orders_2(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0)))
| v3_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(forward_subsumption_resolution,[],[f33809,f31492]) ).
fof(f33816,plain,
! [X0] :
( v3_waybel_3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(forward_subsumption_resolution,[],[f33811,f31493]) ).
fof(f33817,plain,
! [X0] :
( v1_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0)))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(forward_subsumption_resolution,[],[f33812,f31493]) ).
fof(f33818,plain,
! [X0] :
( ~ v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0)))
| v2_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(forward_subsumption_resolution,[],[f33813,f31493]) ).
fof(f33819,plain,
! [X0] :
( ~ v2_lattice3(k2_yellow_1(k1_zfmisc_1(X0)))
| v3_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(forward_subsumption_resolution,[],[f33814,f31493]) ).
fof(f33821,plain,
! [X0] :
( v3_waybel_3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(forward_subsumption_resolution,[],[f33816,f31502]) ).
fof(f33822,plain,
! [X0] :
( v1_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(forward_subsumption_resolution,[],[f33817,f31502]) ).
fof(f33823,plain,
! [X0] :
( v2_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(forward_subsumption_resolution,[],[f33818,f31502]) ).
fof(f33824,plain,
! [X0] :
( v3_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(X0))) ),
inference(forward_subsumption_resolution,[],[f33819,f31502]) ).
fof(f33826,plain,
! [X0] : v3_waybel_3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),
inference(forward_subsumption_resolution,[],[f33821,f23886]) ).
fof(f33827,plain,
! [X0] : v1_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),
inference(forward_subsumption_resolution,[],[f33822,f23886]) ).
fof(f33828,plain,
! [X0] : v2_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),
inference(forward_subsumption_resolution,[],[f33823,f23886]) ).
fof(f33829,plain,
! [X0] : v3_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),
inference(forward_subsumption_resolution,[],[f33824,f23886]) ).
fof(f33832,plain,
! [X0,X1] :
( ~ r1_waybel22(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),X1)
| ~ v2_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v3_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v4_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| k1_card_1(X1) != k1_card_1(sK43)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| r5_waybel_1(sK44,k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))) ),
inference(resolution,[],[f33826,f33078]) ).
fof(f33835,plain,
! [X0,X1] :
( ~ r1_waybel22(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),X1)
| ~ v3_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v4_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| k1_card_1(X1) != k1_card_1(sK43)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| r5_waybel_1(sK44,k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))) ),
inference(forward_subsumption_resolution,[],[f33832,f23901]) ).
fof(f33838,plain,
! [X0,X1] :
( ~ r1_waybel22(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),X1)
| ~ v4_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| k1_card_1(X1) != k1_card_1(sK43)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| r5_waybel_1(sK44,k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))) ),
inference(forward_subsumption_resolution,[],[f33835,f23900]) ).
fof(f33841,plain,
! [X0,X1] :
( ~ r1_waybel22(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),X1)
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| k1_card_1(X1) != k1_card_1(sK43)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| r5_waybel_1(sK44,k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))) ),
inference(forward_subsumption_resolution,[],[f33838,f23899]) ).
fof(f33844,plain,
! [X0,X1] :
( ~ r1_waybel22(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),X1)
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| k1_card_1(X1) != k1_card_1(sK43)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| r5_waybel_1(sK44,k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))) ),
inference(forward_subsumption_resolution,[],[f33841,f33827]) ).
fof(f33847,plain,
! [X0,X1] :
( ~ r1_waybel22(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),X1)
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| k1_card_1(X1) != k1_card_1(sK43)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| r5_waybel_1(sK44,k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))) ),
inference(forward_subsumption_resolution,[],[f33844,f33828]) ).
fof(f33850,plain,
! [X0,X1] :
( ~ r1_waybel22(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),X1)
| k1_card_1(X1) != k1_card_1(sK43)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))
| r5_waybel_1(sK44,k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))) ),
inference(forward_subsumption_resolution,[],[f33847,f33829]) ).
fof(f33853,plain,
! [X0,X1] :
( ~ r1_waybel22(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),X1)
| k1_card_1(X1) != k1_card_1(sK43)
| r5_waybel_1(sK44,k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))) ),
inference(forward_subsumption_resolution,[],[f33850,f23886]) ).
fof(f33854,plain,
$false,
inference(unit_resulting_resolution,[],[f33853,f30220,f30240,f30241]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT351+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.40 % Computer : n018.cluster.edu
% 0.15/0.40 % Model : x86_64 x86_64
% 0.15/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.40 % Memory : 8046.5625MB
% 0.15/0.40 % OS : Linux 6.8.0-71-generic
% 0.15/0.40 % CPULimit : 300
% 0.15/0.40 % WCLimit : 300
% 0.15/0.40 % DateTime : Sun Sep 27 14:58:26 UTC 2026
% 0.15/0.40 % CPUTime :
% 0.15/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.46 Running first-order theorem proving
% 0.15/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
% 21.02/5.14 % (2450849)Detected formulas, will run a generic FOF schedule.
% 21.02/5.14 % (2450855)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=4022230586:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2987 on theBenchmark for (2987ds/134677Mi)
% 21.02/5.14 % (2450857)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1894639736:i=109:sd=1:ins=1:gsp=on:ss=axioms_2987 on theBenchmark for (2987ds/109Mi)
% 21.02/5.14 % (2450854)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=1951950595:i=141193_2987 on theBenchmark for (2987ds/141193Mi)
% 21.02/5.14 % (2450856)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=2569321417:i=141695:sd=1:nm=32:gsp=on:ss=included_2987 on theBenchmark for (2987ds/141695Mi)
% 21.02/5.14 % (2450860)dis-21_1_sil=8000:lcm=predicate:random_seed=952865527:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2987 on theBenchmark for (2987ds/129Mi)
% 21.02/5.14 % (2450858)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=51144763:i=119:av=off:ss=axioms_2987 on theBenchmark for (2987ds/119Mi)
% 21.02/5.14 % (2450859)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3108266291:s2a=on:i=139:gtg=position_2987 on theBenchmark for (2987ds/139Mi)
% 21.02/5.14 % (2450857)Instruction limit reached!
% 21.02/5.14 % (2450857)------------------------------
% 21.02/5.14 % (2450857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/5.14 % (2450857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/5.14 % (2450857)CaDiCaL version: 2.1.3
% 21.02/5.14 % (2450857)Termination reason: Instruction limit
% 21.02/5.14 % (2450857)Termination phase: Clausification
% 21.02/5.14 % (2450857)Time elapsed: 0.130 s
% 21.02/5.14 % (2450857)Peak memory usage: 112 MB
% 21.02/5.14 % (2450857)Instructions burned: 109 (million)
% 21.02/5.14 % (2450859)Instruction limit reached!
% 21.02/5.14 % (2450859)------------------------------
% 21.02/5.14 % (2450859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/5.14 % (2450859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/5.14 % (2450859)CaDiCaL version: 2.1.3
% 21.02/5.14 % (2450859)Termination reason: Instruction limit
% 21.02/5.14 % (2450859)Termination phase: Property scanning
% 21.02/5.14 % (2450859)Time elapsed: 0.115 s
% 21.02/5.14 % (2450859)Peak memory usage: 109 MB
% 21.02/5.14 % (2450859)Instructions burned: 140 (million)
% 21.02/5.14 % (2450860)Instruction limit reached!
% 21.02/5.14 % (2450860)------------------------------
% 21.02/5.14 % (2450860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/5.14 % (2450860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/5.14 % (2450860)CaDiCaL version: 2.1.3
% 21.02/5.14 % (2450860)Termination reason: Instruction limit
% 21.02/5.14 % (2450860)Termination phase: SInE selection
% 21.02/5.14 % (2450860)Time elapsed: 0.123 s
% 21.02/5.14 % (2450860)Peak memory usage: 109 MB
% 21.02/5.14 % (2450860)Instructions burned: 129 (million)
% 21.02/5.14 % (2450858)Instruction limit reached!
% 21.02/5.14 % (2450858)------------------------------
% 21.02/5.14 % (2450858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/5.14 % (2450858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/5.14 % (2450858)CaDiCaL version: 2.1.3
% 21.02/5.14 % (2450858)Termination reason: Instruction limit
% 21.02/5.14 % (2450858)Termination phase: Preprocessing 1
% 21.02/5.14 % (2450858)Time elapsed: 0.143 s
% 21.02/5.14 % (2450858)Peak memory usage: 111 MB
% 21.02/5.14 % (2450858)Instructions burned: 119 (million)
% 21.02/5.14 % (2450868)lrs+10_1_sil=8000:sp=occurrence:random_seed=3527838646:i=285:sd=3:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/285Mi)
% 21.02/5.14 % (2450869)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2808445628:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/157Mi)
% 21.02/5.14 % (2450870)lrs+1011_1_sil=32000:sp=occurrence:random_seed=188215176:i=325:sd=1:ss=axioms:sgt=32_2983 on theBenchmark for (2983ds/325Mi)
% 21.02/5.14 % (2450871)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=2437612581:s2a=on:i=248:s2at=1.23:gtg=position_2983 on theBenchmark for (2983ds/248Mi)
% 21.02/5.14 % (2450869)Instruction limit reached!
% 21.02/5.14 % (2450869)------------------------------
% 21.02/5.14 % (2450869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/5.14 % (2450869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/5.14 % (2450869)CaDiCaL version: 2.1.3
% 21.02/5.14 % (2450869)Termination reason: Instruction limit
% 21.02/5.14 % (2450869)Termination phase: Property scanning
% 21.02/5.14 % (2450869)Time elapsed: 0.131 s
% 21.02/5.14 % (2450869)Peak memory usage: 109 MB
% 21.02/5.14 % (2450869)Instructions burned: 157 (million)
% 21.02/5.14 % (2450871)Instruction limit reached!
% 21.02/5.14 % (2450871)------------------------------
% 21.02/5.14 % (2450871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/5.14 % (2450871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/5.14 % (2450871)CaDiCaL version: 2.1.3
% 21.02/5.14 % (2450871)Termination reason: Instruction limit
% 21.02/5.14 % (2450871)Termination phase: Property scanning
% 21.02/5.14 % (2450871)Time elapsed: 0.208 s
% 21.02/5.14 % (2450871)Peak memory usage: 109 MB
% 21.02/5.14 % (2450871)Instructions burned: 249 (million)
% 21.02/5.14 % (2450868)Instruction limit reached!
% 21.02/5.14 % (2450868)------------------------------
% 21.02/5.14 % (2450868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/5.14 % (2450868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/5.14 % (2450868)CaDiCaL version: 2.1.3
% 21.02/5.14 % (2450868)Termination reason: Instruction limit
% 21.02/5.14 % (2450868)Termination phase: Saturation
% 21.02/5.14 % (2450868)Time elapsed: 0.313 s
% 21.02/5.14 % (2450868)Peak memory usage: 117 MB
% 21.02/5.14 % (2450868)Instructions burned: 286 (million)
% 21.02/5.14 % (2450870)Instruction limit reached!
% 21.02/5.14 % (2450870)------------------------------
% 21.02/5.14 % (2450870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/5.14 % (2450870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/5.14 % (2450870)CaDiCaL version: 2.1.3
% 21.02/5.14 % (2450870)Termination reason: Instruction limit
% 21.02/5.14 % (2450870)Termination phase: Saturation
% 21.02/5.14 % (2450870)Time elapsed: 0.315 s
% 21.02/5.14 % (2450870)Peak memory usage: 116 MB
% 21.02/5.14 % (2450870)Instructions burned: 325 (million)
% 21.02/5.14 % (2450880)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=611678532:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2980 on theBenchmark for (2980ds/294Mi)
% 21.02/5.14 % (2450881)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=471002471:i=2350_2978 on theBenchmark for (2978ds/2350Mi)
% 21.02/5.14 % (2450882)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3841283830:cts=off:i=113:fsr=off:ss=included:sgt=4_2978 on theBenchmark for (2978ds/113Mi)
% 21.02/5.14 % (2450883)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=677820097:i=127:av=off:fsr=off:sup=off_2978 on theBenchmark for (2978ds/127Mi)
% 21.02/5.14 % (2450882)Instruction limit reached!
% 21.02/5.14 % (2450882)------------------------------
% 21.02/5.14 % (2450882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/5.14 % (2450882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/5.14 % (2450882)CaDiCaL version: 2.1.3
% 21.02/5.14 % (2450882)Termination reason: Instruction limit
% 21.02/5.14 % (2450882)Termination phase: Preprocessing 1
% 21.02/5.14 % (2450882)Time elapsed: 0.144 s
% 21.02/5.14 % (2450882)Peak memory usage: 110 MB
% 21.02/5.14 % (2450882)Instructions burned: 113 (million)
% 21.02/5.14 % (2450880)Instruction limit reached!
% 21.02/5.14 % (2450880)------------------------------
% 21.02/5.14 % (2450880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/5.14 % (2450880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/5.14 % (2450880)CaDiCaL version: 2.1.3
% 21.02/5.14 % (2450880)Termination reason: Instruction limit
% 21.02/5.14 % (2450880)Termination phase: Property scanning
% 21.02/5.14 % (2450880)Time elapsed: 0.334 s
% 21.02/5.14 % (2450880)Peak memory usage: 118 MB
% 21.02/5.14 % (2450880)Instructions burned: 294 (million)
% 21.02/5.14 % (2450883)Instruction limit reached!
% 21.02/5.14 % (2450883)------------------------------
% 21.02/5.14 % (2450883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/5.14 % (2450883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/5.14 % (2450883)CaDiCaL version: 2.1.3
% 21.02/5.14 % (2450883)Termination reason: Instruction limit
% 21.02/5.14 % (2450883)Termination phase: Preprocessing 1
% 21.02/5.14 % (2450883)Time elapsed: 0.149 s
% 21.02/5.14 % (2450883)Peak memory usage: 111 MB
% 21.02/5.14 % (2450883)Instructions burned: 127 (million)
% 21.02/5.14 % (2450888)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2201892784:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2974 on theBenchmark for (2974ds/114Mi)
% 21.02/5.14 % (2450889)lrs+10_1_sil=8000:sp=occurrence:random_seed=3705141931:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2973 on theBenchmark for (2973ds/907Mi)
% 21.02/5.14 % (2450888)Instruction limit reached!
% 21.02/5.14 % (2450888)------------------------------
% 21.02/5.14 % (2450888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/5.14 % (2450888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/5.14 % (2450888)CaDiCaL version: 2.1.3
% 21.02/5.14 % (2450888)Termination reason: Instruction limit
% 21.02/5.14 % (2450888)Termination phase: Property scanning
% 21.02/5.14 % (2450888)Time elapsed: 0.096 s
% 21.02/5.14 % (2450888)Peak memory usage: 109 MB
% 21.02/5.14 % (2450888)Instructions burned: 114 (million)
% 21.02/5.14 % (2450890)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2269541168:i=437:sd=1:aac=none:ss=included_2973 on theBenchmark for (2973ds/437Mi)
% 21.02/5.14 % (2450894)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3582007273:i=5202:ss=axioms:sgt=16_2970 on theBenchmark for (2970ds/5202Mi)
% 21.02/5.14 % (2450890)Instruction limit reached!
% 21.02/5.14 % (2450890)------------------------------
% 21.02/5.14 % (2450890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/5.14 % (2450890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/5.14 % (2450890)CaDiCaL version: 2.1.3
% 21.02/5.14 % (2450890)Termination reason: Instruction limit
% 21.02/5.14 % (2450890)Termination phase: Saturation
% 21.02/5.14 % (2450890)Time elapsed: 0.445 s
% 21.02/5.14 % (2450890)Peak memory usage: 117 MB
% 21.02/5.14 % (2450890)Instructions burned: 437 (million)
% 21.02/5.14 % (2450896)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1950904:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2966 on theBenchmark for (2966ds/134Mi)
% 21.02/5.14 % (2450855)First to succeed.
% 21.02/5.14 % (2450855)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2450849"
% 21.02/5.14 % (2450889)Instruction limit reached!
% 21.02/5.14 % (2450889)------------------------------
% 21.02/5.14 % (2450889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/5.14 % (2450889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/5.14 % (2450889)CaDiCaL version: 2.1.3
% 21.02/5.14 % (2450889)Termination reason: Instruction limit
% 21.02/5.14 % (2450889)Termination phase: Saturation
% 21.02/5.14 % (2450889)Time elapsed: 0.859 s
% 21.02/5.14 % (2450889)Peak memory usage: 129 MB
% 21.02/5.14 % (2450889)Instructions burned: 907 (million)
% 21.02/5.14 % (2450896)Instruction limit reached!
% 21.02/5.14 % (2450896)------------------------------
% 21.02/5.14 % (2450896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.02/5.14 % (2450896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.02/5.14 % (2450896)CaDiCaL version: 2.1.3
% 21.02/5.14 % (2450896)Termination reason: Instruction limit
% 21.02/5.14 % (2450896)Termination phase: NewCNF
% 21.02/5.14 % (2450896)Time elapsed: 0.166 s
% 21.02/5.14 % (2450896)Peak memory usage: 113 MB
% 21.02/5.14 % (2450896)Instructions burned: 134 (million)
% 21.02/5.14 % (2450855)Refutation found. Thanks to Tanya!
% 21.02/5.14 % SZS status Theorem for theBenchmark
% 21.02/5.14 % SZS output start Proof for theBenchmark
% See solution above
% 21.70/5.32 % (2450855)------------------------------
% 21.70/5.32 % (2450855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.70/5.32 % (2450855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.70/5.32 % (2450855)CaDiCaL version: 2.1.3
% 21.70/5.32 % (2450855)Termination reason: Refutation
% 21.70/5.32 % (2450855)Time elapsed: 2.363 s
% 21.70/5.32 % (2450855)Peak memory usage: 241 MB
% 21.70/5.32 % (2450855)Instructions burned: 4684 (million)
% 21.70/5.32 % (2450855)------------------------------
% 21.70/5.32 % (2450855)------------------------------
% 21.70/5.32 % (2450849)Success in time 3.995 s
% 21.70/5.32 % Vampire exiting
%------------------------------------------------------------------------------