%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU407+2 : 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 : n009.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 12:48:45 PM UTC 2026
% Result : Theorem 20.55s 4.07s
% Output : Refutation 24.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 23
% Syntax : Number of formulae : 146 ( 51 unt; 10 def)
% Number of atoms : 425 ( 87 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 487 ( 208 ~; 192 |; 61 &)
% ( 12 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 6 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 8 con; 0-6 aty)
% Number of variables : 143 ( 0 sgn 134 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f32,axiom,
! [X0,X1,X2] :
( X2 = k4_xboole_0(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_xboole_0) ).
fof(f54,axiom,
! [X0,X1] : k2_xboole_0(X0,X1) = k2_xboole_0(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k2_xboole_0) ).
fof(f109,axiom,
! [X0,X1] : k4_xboole_0(k2_xboole_0(X0,X1),X1) = k4_xboole_0(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t40_xboole_1) ).
fof(f117,axiom,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f163,axiom,
! [X0,X1] : k2_xboole_0(X0,X1) = k5_xboole_0(k5_xboole_0(X0,X1),k3_xboole_0(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t94_xboole_1) ).
fof(f167,axiom,
! [X0,X1] : k2_xboole_0(X0,X1) = k5_xboole_0(X0,k4_xboole_0(X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t98_xboole_1) ).
fof(f445,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
fof(f3005,axiom,
! [X0] :
( l1_struct_0(X0)
=> ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_struct_0) ).
fof(f3343,axiom,
! [X0] :
( l1_orders_2(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f4433,axiom,
! [X0,X1] :
( ( l1_orders_2(X0)
& l1_orders_2(X1) )
=> ( v1_orders_2(k1_latsum_1(X0,X1))
& l1_orders_2(k1_latsum_1(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_latsum_1) ).
fof(f4436,axiom,
! [X0] :
( l1_orders_2(X0)
=> ! [X1] :
( l1_orders_2(X1)
=> ! [X2] :
( ( v1_orders_2(X2)
& l1_orders_2(X2) )
=> ( X2 = k1_latsum_1(X0,X1)
<=> ( u1_struct_0(X2) = k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1))
& u1_orders_2(X2) = k2_xboole_0(k2_xboole_0(u1_orders_2(X0),u1_orders_2(X1)),k7_relset_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X1),u1_orders_2(X0),u1_orders_2(X1))) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_latsum_1) ).
fof(f4437,axiom,
! [X0,X1] :
( ( l1_orders_2(X0)
& ~ v3_struct_0(X1)
& l1_orders_2(X1) )
=> ( ~ v3_struct_0(k1_latsum_1(X0,X1))
& v1_orders_2(k1_latsum_1(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_latsum_1) ).
fof(f4444,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k1_latsum_1(X0,X1)))
=> ( r2_hidden(X2,u1_struct_0(X0))
| r2_hidden(X2,k4_xboole_0(u1_struct_0(X1),u1_struct_0(X0))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_latsum_1) ).
fof(f4445,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k1_latsum_1(X0,X1)))
=> ( r2_hidden(X2,u1_struct_0(X0))
| r2_hidden(X2,k4_xboole_0(u1_struct_0(X1),u1_struct_0(X0))) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f4444]) ).
fof(f4946,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f445]) ).
fof(f4947,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f4946]) ).
fof(f7802,plain,
! [X0] :
( ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f3005]) ).
fof(f8139,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f3343]) ).
fof(f10111,plain,
! [X0,X1] :
( ( v1_orders_2(k1_latsum_1(X0,X1))
& l1_orders_2(k1_latsum_1(X0,X1)) )
| ~ l1_orders_2(X0)
| ~ l1_orders_2(X1) ),
inference(ennf_transformation,[],[f4433]) ).
fof(f10112,plain,
! [X0,X1] :
( ( v1_orders_2(k1_latsum_1(X0,X1))
& l1_orders_2(k1_latsum_1(X0,X1)) )
| ~ l1_orders_2(X0)
| ~ l1_orders_2(X1) ),
inference(flattening,[],[f10111]) ).
fof(f10116,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k1_latsum_1(X0,X1)
<=> ( u1_struct_0(X2) = k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1))
& u1_orders_2(X2) = k2_xboole_0(k2_xboole_0(u1_orders_2(X0),u1_orders_2(X1)),k7_relset_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X1),u1_orders_2(X0),u1_orders_2(X1))) ) )
| ~ v1_orders_2(X2)
| ~ l1_orders_2(X2) )
| ~ l1_orders_2(X1) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f4436]) ).
fof(f10117,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k1_latsum_1(X0,X1)
<=> ( u1_struct_0(X2) = k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1))
& u1_orders_2(X2) = k2_xboole_0(k2_xboole_0(u1_orders_2(X0),u1_orders_2(X1)),k7_relset_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X1),u1_orders_2(X0),u1_orders_2(X1))) ) )
| ~ v1_orders_2(X2)
| ~ l1_orders_2(X2) )
| ~ l1_orders_2(X1) )
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f10116]) ).
fof(f10118,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k1_latsum_1(X0,X1))
& v1_orders_2(k1_latsum_1(X0,X1)) )
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1) ),
inference(ennf_transformation,[],[f4437]) ).
fof(f10119,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k1_latsum_1(X0,X1))
& v1_orders_2(k1_latsum_1(X0,X1)) )
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1) ),
inference(flattening,[],[f10118]) ).
fof(f10130,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r2_hidden(X2,u1_struct_0(X0))
& ~ r2_hidden(X2,k4_xboole_0(u1_struct_0(X1),u1_struct_0(X0)))
& m1_subset_1(X2,u1_struct_0(k1_latsum_1(X0,X1))) )
& ~ v3_struct_0(X1)
& l1_orders_2(X1) )
& ~ v3_struct_0(X0)
& l1_orders_2(X0) ),
inference(ennf_transformation,[],[f4445]) ).
fof(f10131,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r2_hidden(X2,u1_struct_0(X0))
& ~ r2_hidden(X2,k4_xboole_0(u1_struct_0(X1),u1_struct_0(X0)))
& m1_subset_1(X2,u1_struct_0(k1_latsum_1(X0,X1))) )
& ~ v3_struct_0(X1)
& l1_orders_2(X1) )
& ~ v3_struct_0(X0)
& l1_orders_2(X0) ),
inference(flattening,[],[f10130]) ).
fof(f10535,plain,
! [X0,X1,X2] :
( ( X2 = k4_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1) )
& ( ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) ) )
| k4_xboole_0(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f32]) ).
fof(f10536,plain,
! [X0,X1,X2] :
( ( X2 = k4_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1) )
& ( ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) ) )
| k4_xboole_0(X0,X1) != X2 ) ),
inference(flattening,[],[f10535]) ).
fof(f10537,plain,
! [X0,X1,X2] :
( ( X2 = k4_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| r2_hidden(X4,X1) )
& ( ( r2_hidden(X4,X0)
& ~ r2_hidden(X4,X1) )
| ~ r2_hidden(X4,X2) ) )
| k4_xboole_0(X0,X1) != X2 ) ),
inference(rectify,[],[f10536]) ).
fof(f10538,plain,
! [X0,X1,X2] :
( ( X2 = k4_xboole_0(X0,X1)
| ( ( ~ r2_hidden(sK254(X0,X1,X2),X0)
| r2_hidden(sK254(X0,X1,X2),X1)
| ~ r2_hidden(sK254(X0,X1,X2),X2) )
& ( ( r2_hidden(sK254(X0,X1,X2),X0)
& ~ r2_hidden(sK254(X0,X1,X2),X1) )
| r2_hidden(sK254(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| r2_hidden(X4,X1) )
& ( ( r2_hidden(X4,X0)
& ~ r2_hidden(X4,X1) )
| ~ r2_hidden(X4,X2) ) )
| k4_xboole_0(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK254]),skolemize(X3,sK254(X0,X1,X2))],[f10537]) ).
fof(f11847,plain,
! [X0] :
( ( ( v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) )
& ( v1_xboole_0(u1_struct_0(X0))
| ~ v3_struct_0(X0) ) )
| ~ l1_struct_0(X0) ),
inference(nnf_transformation,[],[f7802]) ).
fof(f12970,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k1_latsum_1(X0,X1)
| u1_struct_0(X2) != k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1))
| u1_orders_2(X2) != k2_xboole_0(k2_xboole_0(u1_orders_2(X0),u1_orders_2(X1)),k7_relset_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X1),u1_orders_2(X0),u1_orders_2(X1))) )
& ( ( u1_struct_0(X2) = k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1))
& u1_orders_2(X2) = k2_xboole_0(k2_xboole_0(u1_orders_2(X0),u1_orders_2(X1)),k7_relset_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X1),u1_orders_2(X0),u1_orders_2(X1))) )
| k1_latsum_1(X0,X1) != X2 ) )
| ~ v1_orders_2(X2)
| ~ l1_orders_2(X2) )
| ~ l1_orders_2(X1) )
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f10117]) ).
fof(f12971,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k1_latsum_1(X0,X1)
| u1_struct_0(X2) != k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1))
| u1_orders_2(X2) != k2_xboole_0(k2_xboole_0(u1_orders_2(X0),u1_orders_2(X1)),k7_relset_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X1),u1_orders_2(X0),u1_orders_2(X1))) )
& ( ( u1_struct_0(X2) = k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1))
& u1_orders_2(X2) = k2_xboole_0(k2_xboole_0(u1_orders_2(X0),u1_orders_2(X1)),k7_relset_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X1),u1_orders_2(X0),u1_orders_2(X1))) )
| k1_latsum_1(X0,X1) != X2 ) )
| ~ v1_orders_2(X2)
| ~ l1_orders_2(X2) )
| ~ l1_orders_2(X1) )
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f12970]) ).
fof(f12972,plain,
( ~ r2_hidden(sK1534,u1_struct_0(sK1532))
& ~ r2_hidden(sK1534,k4_xboole_0(u1_struct_0(sK1533),u1_struct_0(sK1532)))
& m1_subset_1(sK1534,u1_struct_0(k1_latsum_1(sK1532,sK1533)))
& ~ v3_struct_0(sK1533)
& l1_orders_2(sK1533)
& ~ v3_struct_0(sK1532)
& l1_orders_2(sK1532) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1532,sK1533,sK1534]),skolemize(X0,sK1532),skolemize(X1,sK1533),skolemize(X2,sK1534)],[f10131]) ).
fof(f13049,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| r2_hidden(X4,X1)
| k4_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f10538]) ).
fof(f13100,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k2_xboole_0(X1,X0),
inference(cnf_transformation,[],[f54]) ).
fof(f13157,plain,
! [X0,X1] : k4_xboole_0(X0,X1) = k4_xboole_0(k2_xboole_0(X0,X1),X1),
inference(cnf_transformation,[],[f109]) ).
fof(f13165,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f13215,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k5_xboole_0(k5_xboole_0(X0,X1),k3_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f163]) ).
fof(f13219,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k5_xboole_0(X0,k4_xboole_0(X1,X0)),
inference(cnf_transformation,[],[f167]) ).
fof(f13610,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f4947]) ).
fof(f18069,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f11847]) ).
fof(f18573,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f8139]) ).
fof(f21955,plain,
! [X0,X1] :
( l1_orders_2(k1_latsum_1(X0,X1))
| ~ l1_orders_2(X0)
| ~ l1_orders_2(X1) ),
inference(cnf_transformation,[],[f10112]) ).
fof(f21956,plain,
! [X0,X1] :
( v1_orders_2(k1_latsum_1(X0,X1))
| ~ l1_orders_2(X0)
| ~ l1_orders_2(X1) ),
inference(cnf_transformation,[],[f10112]) ).
fof(f21974,plain,
! [X2,X0,X1] :
( u1_struct_0(X2) = k2_xboole_0(u1_struct_0(X0),u1_struct_0(X1))
| k1_latsum_1(X0,X1) != X2
| ~ v1_orders_2(X2)
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f12971]) ).
fof(f21977,plain,
! [X0,X1] :
( ~ v3_struct_0(k1_latsum_1(X0,X1))
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1) ),
inference(cnf_transformation,[],[f10119]) ).
fof(f21987,plain,
l1_orders_2(sK1532),
inference(cnf_transformation,[],[f12972]) ).
fof(f21989,plain,
l1_orders_2(sK1533),
inference(cnf_transformation,[],[f12972]) ).
fof(f21990,plain,
~ v3_struct_0(sK1533),
inference(cnf_transformation,[],[f12972]) ).
fof(f21991,plain,
m1_subset_1(sK1534,u1_struct_0(k1_latsum_1(sK1532,sK1533))),
inference(cnf_transformation,[],[f12972]) ).
fof(f21992,plain,
~ r2_hidden(sK1534,k4_xboole_0(u1_struct_0(sK1533),u1_struct_0(sK1532))),
inference(cnf_transformation,[],[f12972]) ).
fof(f21993,plain,
~ r2_hidden(sK1534,u1_struct_0(sK1532)),
inference(cnf_transformation,[],[f12972]) ).
fof(f21998,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),
inference(definition_unfolding,[],[f13215,f13165]) ).
fof(f22047,plain,
! [X0,X1] : k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))) = k5_xboole_0(k5_xboole_0(X1,X0),k4_xboole_0(X1,k4_xboole_0(X1,X0))),
inference(definition_unfolding,[],[f13100,f21998,f21998]) ).
fof(f22095,plain,
! [X0,X1] : k4_xboole_0(X0,X1) = k4_xboole_0(k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),X1),
inference(definition_unfolding,[],[f13157,f21998]) ).
fof(f22134,plain,
! [X0,X1] : k5_xboole_0(X0,k4_xboole_0(X1,X0)) = k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))),
inference(definition_unfolding,[],[f13219,f21998]) ).
fof(f23733,plain,
! [X2,X0,X1] :
( u1_struct_0(X2) = k5_xboole_0(k5_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k4_xboole_0(u1_struct_0(X0),k4_xboole_0(u1_struct_0(X0),u1_struct_0(X1))))
| k1_latsum_1(X0,X1) != X2
| ~ v1_orders_2(X2)
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(definition_unfolding,[],[f21974,f21998]) ).
fof(f23755,plain,
! [X0,X1,X4] :
( r2_hidden(X4,k4_xboole_0(X0,X1))
| ~ r2_hidden(X4,X0)
| r2_hidden(X4,X1) ),
inference(equality_resolution,[],[f13049]) ).
fof(f24510,plain,
! [X0,X1] :
( ~ v1_orders_2(k1_latsum_1(X0,X1))
| u1_struct_0(k1_latsum_1(X0,X1)) = k5_xboole_0(k5_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k4_xboole_0(u1_struct_0(X0),k4_xboole_0(u1_struct_0(X0),u1_struct_0(X1))))
| ~ l1_orders_2(k1_latsum_1(X0,X1))
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(equality_resolution,[],[f23733]) ).
fof(f24512,definition,
sF1535 = u1_struct_0(sK1532),
introduced(definition,[new_symbols(definition,[sF1535])],[function_definition]) ).
fof(f24513,plain,
u1_struct_0(sK1532) = sF1535,
inference(reorient_equations,[],[f24512]) ).
fof(f24514,plain,
~ r2_hidden(sK1534,sF1535),
inference(definition_folding,[],[f21993,f24513]) ).
fof(f24515,definition,
sF1536 = u1_struct_0(sK1533),
introduced(definition,[new_symbols(definition,[sF1536])],[function_definition]) ).
fof(f24516,plain,
u1_struct_0(sK1533) = sF1536,
inference(reorient_equations,[],[f24515]) ).
fof(f24517,definition,
sF1537 = k4_xboole_0(sF1536,sF1535),
introduced(definition,[new_symbols(definition,[sF1537])],[function_definition]) ).
fof(f24518,plain,
k4_xboole_0(sF1536,sF1535) = sF1537,
inference(reorient_equations,[],[f24517]) ).
fof(f24519,plain,
~ r2_hidden(sK1534,sF1537),
inference(definition_folding,[],[f21992,f24518,f24513,f24516]) ).
fof(f24520,definition,
sF1538 = k1_latsum_1(sK1532,sK1533),
introduced(definition,[new_symbols(definition,[sF1538])],[function_definition]) ).
fof(f24521,plain,
k1_latsum_1(sK1532,sK1533) = sF1538,
inference(reorient_equations,[],[f24520]) ).
fof(f24522,definition,
sF1539 = u1_struct_0(sF1538),
introduced(definition,[new_symbols(definition,[sF1539])],[function_definition]) ).
fof(f24523,plain,
u1_struct_0(sF1538) = sF1539,
inference(reorient_equations,[],[f24522]) ).
fof(f24524,plain,
m1_subset_1(sK1534,sF1539),
inference(definition_folding,[],[f21991,f24523,f24521]) ).
fof(f27512,plain,
! [X0,X1] : k4_xboole_0(X0,X1) = k4_xboole_0(k5_xboole_0(X0,k4_xboole_0(X1,X0)),X1),
inference(forward_demodulation,[],[f22095,f22134]) ).
fof(f27540,plain,
! [X0,X1] : k5_xboole_0(k5_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X1))) = k5_xboole_0(X1,k4_xboole_0(X0,X1)),
inference(forward_demodulation,[],[f22047,f22134]) ).
fof(f27855,plain,
! [X0,X1] : k5_xboole_0(X0,k4_xboole_0(X1,X0)) = k5_xboole_0(X1,k4_xboole_0(X0,X1)),
inference(forward_demodulation,[],[f27540,f22134]) ).
fof(f28288,plain,
( ~ v1_orders_2(sF1538)
| u1_struct_0(sF1538) = k5_xboole_0(k5_xboole_0(u1_struct_0(sK1532),u1_struct_0(sK1533)),k4_xboole_0(u1_struct_0(sK1532),k4_xboole_0(u1_struct_0(sK1532),u1_struct_0(sK1533))))
| ~ l1_orders_2(sF1538)
| ~ l1_orders_2(sK1533)
| ~ l1_orders_2(sK1532) ),
inference(superposition,[],[f24510,f24521]) ).
fof(f28289,plain,
( ~ v1_orders_2(sF1538)
| u1_struct_0(sF1538) = k5_xboole_0(k5_xboole_0(u1_struct_0(sK1532),u1_struct_0(sK1533)),k4_xboole_0(u1_struct_0(sK1532),k4_xboole_0(u1_struct_0(sK1532),u1_struct_0(sK1533))))
| ~ l1_orders_2(sF1538)
| ~ l1_orders_2(sK1532) ),
inference(forward_subsumption_resolution,[],[f28288,f21989]) ).
fof(f28290,plain,
( ~ v1_orders_2(sF1538)
| u1_struct_0(sF1538) = k5_xboole_0(k5_xboole_0(u1_struct_0(sK1532),u1_struct_0(sK1533)),k4_xboole_0(u1_struct_0(sK1532),k4_xboole_0(u1_struct_0(sK1532),u1_struct_0(sK1533))))
| ~ l1_orders_2(sF1538) ),
inference(forward_subsumption_resolution,[],[f28289,f21987]) ).
fof(f28291,plain,
( u1_struct_0(sF1538) = k5_xboole_0(u1_struct_0(sK1532),k4_xboole_0(u1_struct_0(sK1533),u1_struct_0(sK1532)))
| ~ v1_orders_2(sF1538)
| ~ l1_orders_2(sF1538) ),
inference(forward_demodulation,[],[f28290,f22134]) ).
fof(f28292,plain,
( u1_struct_0(sF1538) = k5_xboole_0(sF1535,k4_xboole_0(u1_struct_0(sK1533),sF1535))
| ~ v1_orders_2(sF1538)
| ~ l1_orders_2(sF1538) ),
inference(forward_demodulation,[],[f28291,f24513]) ).
fof(f28293,plain,
( u1_struct_0(sF1538) = k5_xboole_0(sF1535,k4_xboole_0(sF1536,sF1535))
| ~ v1_orders_2(sF1538)
| ~ l1_orders_2(sF1538) ),
inference(forward_demodulation,[],[f28292,f24516]) ).
fof(f28294,plain,
( u1_struct_0(sF1538) = k5_xboole_0(sF1535,sF1537)
| ~ v1_orders_2(sF1538)
| ~ l1_orders_2(sF1538) ),
inference(forward_demodulation,[],[f28293,f24518]) ).
fof(f28295,plain,
( sF1539 = k5_xboole_0(sF1535,sF1537)
| ~ v1_orders_2(sF1538)
| ~ l1_orders_2(sF1538) ),
inference(forward_demodulation,[],[f28294,f24523]) ).
fof(f28297,definition,
( spl1540_543
<=> l1_orders_2(sF1538) ),
introduced(definition,[new_symbols(definition,[spl1540_543])],[avatar_definition]) ).
fof(f28298,plain,
( l1_orders_2(sF1538)
| ~ spl1540_543 ),
inference(avatar_component_clause,[],[f28297]) ).
fof(f28299,plain,
( ~ l1_orders_2(sF1538)
| spl1540_543 ),
inference(avatar_component_clause,[],[f28297]) ).
fof(f28301,definition,
( spl1540_544
<=> v1_orders_2(sF1538) ),
introduced(definition,[new_symbols(definition,[spl1540_544])],[avatar_definition]) ).
fof(f28303,plain,
( ~ v1_orders_2(sF1538)
| spl1540_544 ),
inference(avatar_component_clause,[],[f28301]) ).
fof(f28305,definition,
( spl1540_545
<=> sF1539 = k5_xboole_0(sF1535,sF1537) ),
introduced(definition,[new_symbols(definition,[spl1540_545])],[avatar_definition]) ).
fof(f28307,plain,
( sF1539 = k5_xboole_0(sF1535,sF1537)
| ~ spl1540_545 ),
inference(avatar_component_clause,[],[f28305]) ).
fof(f28308,plain,
( ~ spl1540_543
| ~ spl1540_544
| spl1540_545 ),
inference(avatar_split_clause,[],[f28295,f28305,f28301,f28297]) ).
fof(f28309,plain,
( l1_orders_2(sF1538)
| ~ l1_orders_2(sK1532)
| ~ l1_orders_2(sK1533) ),
inference(superposition,[],[f21955,f24521]) ).
fof(f28310,plain,
( ~ l1_orders_2(sK1532)
| ~ l1_orders_2(sK1533)
| spl1540_543 ),
inference(forward_subsumption_resolution,[],[f28309,f28299]) ).
fof(f28311,plain,
( ~ l1_orders_2(sK1533)
| spl1540_543 ),
inference(forward_subsumption_resolution,[],[f28310,f21987]) ).
fof(f28312,plain,
( $false
| spl1540_543 ),
inference(forward_subsumption_resolution,[],[f28311,f21989]) ).
fof(f28313,plain,
spl1540_543,
inference(avatar_contradiction_clause,[],[f28312]) ).
fof(f28317,plain,
( ~ v3_struct_0(sF1538)
| ~ l1_orders_2(sK1532)
| v3_struct_0(sK1533)
| ~ l1_orders_2(sK1533) ),
inference(superposition,[],[f21977,f24521]) ).
fof(f28318,plain,
( ~ v3_struct_0(sF1538)
| v3_struct_0(sK1533)
| ~ l1_orders_2(sK1533) ),
inference(forward_subsumption_resolution,[],[f28317,f21987]) ).
fof(f28319,plain,
( ~ v3_struct_0(sF1538)
| ~ l1_orders_2(sK1533) ),
inference(forward_subsumption_resolution,[],[f28318,f21990]) ).
fof(f28320,plain,
~ v3_struct_0(sF1538),
inference(forward_subsumption_resolution,[],[f28319,f21989]) ).
fof(f28342,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ l1_orders_2(X1)
| u1_struct_0(k1_latsum_1(X0,X1)) = k5_xboole_0(k5_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k4_xboole_0(u1_struct_0(X0),k4_xboole_0(u1_struct_0(X0),u1_struct_0(X1))))
| ~ l1_orders_2(k1_latsum_1(X0,X1))
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(resolution,[],[f21956,f24510]) ).
fof(f28343,plain,
( v1_orders_2(sF1538)
| ~ l1_orders_2(sK1532)
| ~ l1_orders_2(sK1533) ),
inference(superposition,[],[f21956,f24521]) ).
fof(f28344,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ l1_orders_2(X1)
| u1_struct_0(k1_latsum_1(X0,X1)) = k5_xboole_0(k5_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k4_xboole_0(u1_struct_0(X0),k4_xboole_0(u1_struct_0(X0),u1_struct_0(X1))))
| ~ l1_orders_2(k1_latsum_1(X0,X1)) ),
inference(duplicate_literal_removal,[],[f28342]) ).
fof(f28345,plain,
( ~ l1_orders_2(sK1532)
| ~ l1_orders_2(sK1533)
| spl1540_544 ),
inference(forward_subsumption_resolution,[],[f28343,f28303]) ).
fof(f28346,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ l1_orders_2(X1)
| u1_struct_0(k1_latsum_1(X0,X1)) = k5_xboole_0(k5_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k4_xboole_0(u1_struct_0(X0),k4_xboole_0(u1_struct_0(X0),u1_struct_0(X1)))) ),
inference(forward_subsumption_resolution,[],[f28344,f21955]) ).
fof(f28347,plain,
( ~ l1_orders_2(sK1533)
| spl1540_544 ),
inference(forward_subsumption_resolution,[],[f28345,f21987]) ).
fof(f28348,plain,
! [X0,X1] :
( ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| u1_struct_0(k1_latsum_1(X0,X1)) = k5_xboole_0(u1_struct_0(X0),k4_xboole_0(u1_struct_0(X1),u1_struct_0(X0))) ),
inference(forward_demodulation,[],[f28346,f22134]) ).
fof(f28349,plain,
( $false
| spl1540_544 ),
inference(forward_subsumption_resolution,[],[f28347,f21989]) ).
fof(f28350,plain,
spl1540_544,
inference(avatar_contradiction_clause,[],[f28349]) ).
fof(f28352,plain,
! [X0] :
( ~ l1_orders_2(X0)
| u1_struct_0(k1_latsum_1(X0,sK1532)) = k5_xboole_0(u1_struct_0(X0),k4_xboole_0(u1_struct_0(sK1532),u1_struct_0(X0))) ),
inference(resolution,[],[f28348,f21987]) ).
fof(f28357,plain,
! [X0] :
( ~ l1_orders_2(X0)
| u1_struct_0(k1_latsum_1(X0,sK1532)) = k5_xboole_0(u1_struct_0(X0),k4_xboole_0(sF1535,u1_struct_0(X0))) ),
inference(forward_demodulation,[],[f28352,f24513]) ).
fof(f28387,plain,
u1_struct_0(k1_latsum_1(sK1533,sK1532)) = k5_xboole_0(u1_struct_0(sK1533),k4_xboole_0(sF1535,u1_struct_0(sK1533))),
inference(resolution,[],[f28357,f21989]) ).
fof(f28390,plain,
u1_struct_0(k1_latsum_1(sK1533,sK1532)) = k5_xboole_0(sF1536,k4_xboole_0(sF1535,sF1536)),
inference(forward_demodulation,[],[f28387,f24516]) ).
fof(f28399,plain,
( r2_hidden(sK1534,sF1539)
| v1_xboole_0(sF1539) ),
inference(resolution,[],[f13610,f24524]) ).
fof(f28419,plain,
( ~ v1_xboole_0(sF1539)
| v3_struct_0(sF1538)
| ~ l1_struct_0(sF1538) ),
inference(superposition,[],[f18069,f24523]) ).
fof(f28748,plain,
( l1_struct_0(sF1538)
| ~ spl1540_543 ),
inference(resolution,[],[f18573,f28298]) ).
fof(f28756,definition,
( spl1540_557
<=> v1_xboole_0(sF1539) ),
introduced(definition,[new_symbols(definition,[spl1540_557])],[avatar_definition]) ).
fof(f28760,definition,
( spl1540_558
<=> r2_hidden(sK1534,sF1539) ),
introduced(definition,[new_symbols(definition,[spl1540_558])],[avatar_definition]) ).
fof(f28762,plain,
( r2_hidden(sK1534,sF1539)
| ~ spl1540_558 ),
inference(avatar_component_clause,[],[f28760]) ).
fof(f28763,plain,
( spl1540_557
| spl1540_558 ),
inference(avatar_split_clause,[],[f28399,f28760,f28756]) ).
fof(f28764,plain,
( ~ v1_xboole_0(sF1539)
| ~ l1_struct_0(sF1538) ),
inference(forward_subsumption_resolution,[],[f28419,f28320]) ).
fof(f28783,plain,
( ~ v1_xboole_0(sF1539)
| ~ spl1540_543 ),
inference(forward_subsumption_resolution,[],[f28764,f28748]) ).
fof(f28786,plain,
( ~ spl1540_557
| ~ spl1540_543 ),
inference(avatar_split_clause,[],[f28783,f28297,f28756]) ).
fof(f29357,plain,
k5_xboole_0(sF1535,sF1537) = k5_xboole_0(sF1536,k4_xboole_0(sF1535,sF1536)),
inference(superposition,[],[f27855,f24518]) ).
fof(f29370,plain,
k5_xboole_0(sF1535,sF1537) = u1_struct_0(k1_latsum_1(sK1533,sK1532)),
inference(forward_demodulation,[],[f29357,f28390]) ).
fof(f29395,plain,
( sF1539 = u1_struct_0(k1_latsum_1(sK1533,sK1532))
| ~ spl1540_545 ),
inference(forward_demodulation,[],[f29370,f28307]) ).
fof(f29741,plain,
k4_xboole_0(sF1536,sF1535) = k4_xboole_0(u1_struct_0(k1_latsum_1(sK1533,sK1532)),sF1535),
inference(superposition,[],[f27512,f28390]) ).
fof(f29787,plain,
( k4_xboole_0(sF1536,sF1535) = k4_xboole_0(sF1539,sF1535)
| ~ spl1540_545 ),
inference(forward_demodulation,[],[f29741,f29395]) ).
fof(f29820,plain,
( sF1537 = k4_xboole_0(sF1539,sF1535)
| ~ spl1540_545 ),
inference(forward_demodulation,[],[f29787,f24518]) ).
fof(f29842,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF1539)
| r2_hidden(X0,sF1537)
| r2_hidden(X0,sF1535) )
| ~ spl1540_545 ),
inference(superposition,[],[f23755,f29820]) ).
fof(f29878,plain,
( r2_hidden(sK1534,sF1537)
| r2_hidden(sK1534,sF1535)
| ~ spl1540_545
| ~ spl1540_558 ),
inference(resolution,[],[f29842,f28762]) ).
fof(f29879,plain,
( r2_hidden(sK1534,sF1535)
| ~ spl1540_545
| ~ spl1540_558 ),
inference(forward_subsumption_resolution,[],[f29878,f24519]) ).
fof(f29880,plain,
( $false
| ~ spl1540_545
| ~ spl1540_558 ),
inference(forward_subsumption_resolution,[],[f29879,f24514]) ).
fof(f29881,plain,
( ~ spl1540_545
| ~ spl1540_558 ),
inference(avatar_contradiction_clause,[],[f29880]) ).
cnf(s474,plain,
( ~ spl1540_543
| ~ spl1540_544
| spl1540_545 ),
inference(sat_conversion,[],[f28308]) ).
cnf(s475,plain,
spl1540_543,
inference(sat_conversion,[],[f28313]) ).
cnf(s476,plain,
spl1540_544,
inference(sat_conversion,[],[f28350]) ).
cnf(s487,plain,
( spl1540_557
| spl1540_558 ),
inference(sat_conversion,[],[f28763]) ).
cnf(s490,plain,
( ~ spl1540_543
| ~ spl1540_557 ),
inference(sat_conversion,[],[f28786]) ).
cnf(s497,plain,
( ~ spl1540_545
| ~ spl1540_558 ),
inference(sat_conversion,[],[f29881]) ).
cnf(s503,plain,
~ spl1540_557,
inference(rat,[],[s490,s475]) ).
cnf(s504,plain,
spl1540_558,
inference(rat,[],[s487,s503]) ).
cnf(s505,plain,
~ spl1540_545,
inference(rat,[],[s497,s504]) ).
cnf(s506,plain,
$false,
inference(rat,[],[s474,s505,s476,s475]) ).
fof(f29882,plain,
$false,
inference(avatar_sat_refutation,[],[s506]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU407+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n009.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Mon Sep 28 05:10:16 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/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
% 13.24/2.69 % (2675272)Detected formulas, will run a generic FOF schedule.
% 13.24/2.69 % (2675282)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2666964689:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 13.24/2.69 % (2675279)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=2888622961:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 13.24/2.69 % (2675280)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1149746414:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 13.24/2.69 % (2675278)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=2257633125:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 13.24/2.69 % (2675283)dis-21_1_sil=8000:lcm=predicate:random_seed=3768895547:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 13.24/2.69 % (2675277)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=2524932112:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 13.24/2.69 % (2675281)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2383737782:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 13.24/2.69 % (2675280)Refutation not found, incomplete strategy
% 13.24/2.69 % (2675280)------------------------------
% 13.24/2.69 % (2675280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.24/2.69 % (2675280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.24/2.69 % (2675280)CaDiCaL version: 2.1.3
% 13.24/2.69 % (2675280)Termination reason: Refutation not found, incomplete strategy
% 13.24/2.69 % (2675280)Time elapsed: 0.022 s
% 13.24/2.69 % (2675280)Peak memory usage: 93 MB
% 13.24/2.69 % (2675280)Instructions burned: 28 (million)
% 13.24/2.69 % (2675281)Instruction limit reached!
% 13.24/2.69 % (2675281)------------------------------
% 13.24/2.69 % (2675281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.24/2.69 % (2675281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.24/2.69 % (2675281)CaDiCaL version: 2.1.3
% 13.24/2.69 % (2675281)Termination reason: Instruction limit
% 13.24/2.69 % (2675281)Termination phase: Saturation
% 13.24/2.69 % (2675281)Time elapsed: 0.080 s
% 13.24/2.69 % (2675281)Peak memory usage: 94 MB
% 13.24/2.69 % (2675281)Instructions burned: 119 (million)
% 13.24/2.69 % (2675282)Instruction limit reached!
% 13.24/2.69 % (2675282)------------------------------
% 13.24/2.69 % (2675282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.24/2.69 % (2675282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.24/2.69 % (2675282)CaDiCaL version: 2.1.3
% 13.24/2.69 % (2675282)Termination reason: Instruction limit
% 13.24/2.69 % (2675282)Termination phase: Preprocessing 3
% 13.24/2.69 % (2675282)Time elapsed: 0.087 s
% 13.24/2.69 % (2675282)Peak memory usage: 95 MB
% 13.24/2.69 % (2675282)Instructions burned: 139 (million)
% 13.24/2.69 % (2675283)Instruction limit reached!
% 13.24/2.69 % (2675283)------------------------------
% 13.24/2.69 % (2675283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.24/2.69 % (2675283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.24/2.69 % (2675283)CaDiCaL version: 2.1.3
% 13.24/2.69 % (2675283)Termination reason: Instruction limit
% 13.24/2.69 % (2675283)Termination phase: Preprocessing 3
% 13.24/2.69 % (2675283)Time elapsed: 0.091 s
% 13.24/2.69 % (2675283)Peak memory usage: 95 MB
% 13.24/2.69 % (2675283)Instructions burned: 129 (million)
% 13.24/2.69 % (2675292)lrs+10_1_sil=32000:urr=on:br=off:random_seed=901246654:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 13.24/2.69 % (2675291)lrs+10_1_sil=8000:sp=occurrence:random_seed=476050943:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 13.24/2.69 % (2675293)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4193054595:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 13.24/2.69 % (2675280)------------------------------
% 13.24/2.69 % (2675280)------------------------------
% 13.24/2.69 % (2675292)Instruction limit reached!
% 13.24/2.69 % (2675292)------------------------------
% 13.24/2.69 % (2675292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.24/3.67 % (2675292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/3.67 % (2675292)CaDiCaL version: 2.1.3
% 20.24/3.67 % (2675292)Termination reason: Instruction limit
% 20.24/3.67 % (2675292)Termination phase: Saturation
% 20.24/3.67 % (2675292)Time elapsed: 0.046 s
% 20.24/3.67 % (2675292)Peak memory usage: 95 MB
% 20.24/3.67 % (2675292)Instructions burned: 160 (million)
% 20.24/3.67 % (2675298)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1229906587:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 20.24/3.67 % (2675291)Instruction limit reached!
% 20.24/3.67 % (2675291)------------------------------
% 20.24/3.67 % (2675291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.24/3.67 % (2675291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/3.67 % (2675291)CaDiCaL version: 2.1.3
% 20.24/3.67 % (2675291)Termination reason: Instruction limit
% 20.24/3.67 % (2675291)Termination phase: Saturation
% 20.24/3.67 % (2675291)Time elapsed: 0.198 s
% 20.24/3.67 % (2675291)Peak memory usage: 97 MB
% 20.24/3.67 % (2675291)Instructions burned: 285 (million)
% 20.24/3.67 % (2675297)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=1643952294:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 20.24/3.67 % (2675293)Instruction limit reached!
% 20.24/3.67 % (2675293)------------------------------
% 20.24/3.67 % (2675293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.24/3.67 % (2675293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/3.67 % (2675293)CaDiCaL version: 2.1.3
% 20.24/3.67 % (2675293)Termination reason: Instruction limit
% 20.24/3.67 % (2675293)Termination phase: Saturation
% 20.24/3.67 % (2675293)Time elapsed: 0.221 s
% 20.24/3.67 % (2675293)Peak memory usage: 97 MB
% 20.24/3.67 % (2675293)Instructions burned: 326 (million)
% 20.24/3.67 % (2675298)Instruction limit reached!
% 20.24/3.67 % (2675298)------------------------------
% 20.24/3.67 % (2675298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.24/3.67 % (2675298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/3.67 % (2675298)CaDiCaL version: 2.1.3
% 20.24/3.67 % (2675298)Termination reason: Instruction limit
% 20.24/3.67 % (2675298)Termination phase: Saturation
% 20.24/3.67 % (2675298)Time elapsed: 0.095 s
% 20.24/3.67 % (2675298)Peak memory usage: 97 MB
% 20.24/3.67 % (2675298)Instructions burned: 294 (million)
% 20.24/3.67 % (2675300)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2359934816:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 20.24/3.67 % (2675297)Instruction limit reached!
% 20.24/3.67 % (2675297)------------------------------
% 20.24/3.67 % (2675297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.24/3.67 % (2675297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/3.67 % (2675297)CaDiCaL version: 2.1.3
% 20.24/3.67 % (2675297)Termination reason: Instruction limit
% 20.24/3.67 % (2675297)Termination phase: Property scanning
% 20.24/3.67 % (2675297)Time elapsed: 0.155 s
% 20.24/3.67 % (2675297)Peak memory usage: 100 MB
% 20.24/3.67 % (2675297)Instructions burned: 249 (million)
% 20.24/3.67 % (2675303)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4218871860:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 20.24/3.67 % (2675302)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4173711891:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 20.24/3.67 % (2675303)Instruction limit reached!
% 20.24/3.67 % (2675303)------------------------------
% 20.24/3.67 % (2675303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.24/3.67 % (2675303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.24/3.67 % (2675303)CaDiCaL version: 2.1.3
% 20.24/3.67 % (2675303)Termination reason: Instruction limit
% 20.24/3.67 % (2675303)Termination phase: Preprocessing 3
% 20.24/3.67 % (2675303)Time elapsed: 0.051 s
% 20.24/3.67 % (2675303)Peak memory usage: 97 MB
% 20.24/3.67 % (2675303)Instructions burned: 128 (million)
% 20.24/3.67 % (2675302)Instruction limit reached!
% 20.24/3.67 % (2675302)------------------------------
% 20.24/3.67 % (2675302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.24/3.67 % (2675302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.55/4.07 % (2675302)CaDiCaL version: 2.1.3
% 20.55/4.07 % (2675302)Termination reason: Instruction limit
% 20.55/4.07 % (2675302)Termination phase: Saturation
% 20.55/4.07 % (2675302)Time elapsed: 0.074 s
% 20.55/4.07 % (2675302)Peak memory usage: 96 MB
% 20.55/4.07 % (2675302)Instructions burned: 115 (million)
% 20.55/4.07 % (2675305)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3522123733:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 20.55/4.07 % (2675308)lrs+10_1_sil=8000:sp=occurrence:random_seed=4009382345:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 20.55/4.07 % (2675305)Instruction limit reached!
% 20.55/4.07 % (2675305)------------------------------
% 20.55/4.07 % (2675305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.55/4.07 % (2675305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.55/4.07 % (2675305)CaDiCaL version: 2.1.3
% 20.55/4.07 % (2675305)Termination reason: Instruction limit
% 20.55/4.07 % (2675305)Termination phase: SInE selection
% 20.55/4.07 % (2675305)Time elapsed: 0.052 s
% 20.55/4.07 % (2675305)Peak memory usage: 89 MB
% 20.55/4.07 % (2675305)Instructions burned: 115 (million)
% 20.55/4.07 % (2675309)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3293492684:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 20.55/4.07 % (2675312)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=295450295:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 20.55/4.07 % (2675308)Instruction limit reached!
% 20.55/4.07 % (2675308)------------------------------
% 20.55/4.07 % (2675308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.55/4.07 % (2675308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.55/4.07 % (2675308)CaDiCaL version: 2.1.3
% 20.55/4.07 % (2675308)Termination reason: Instruction limit
% 20.55/4.07 % (2675308)Termination phase: Saturation
% 20.55/4.07 % (2675308)Time elapsed: 0.328 s
% 20.55/4.07 % (2675308)Peak memory usage: 107 MB
% 20.55/4.07 % (2675308)Instructions burned: 907 (million)
% 20.55/4.07 % (2675309)Instruction limit reached!
% 20.55/4.07 % (2675309)------------------------------
% 20.55/4.07 % (2675309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.55/4.07 % (2675309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.55/4.07 % (2675309)CaDiCaL version: 2.1.3
% 20.55/4.07 % (2675309)Termination reason: Instruction limit
% 20.55/4.07 % (2675309)Termination phase: Saturation
% 20.55/4.07 % (2675309)Time elapsed: 0.275 s
% 20.55/4.07 % (2675309)Peak memory usage: 97 MB
% 20.55/4.07 % (2675309)Instructions burned: 437 (million)
% 20.55/4.07 % (2675315)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2614569545:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 20.55/4.07 % (2675315)Instruction limit reached!
% 20.55/4.07 % (2675315)------------------------------
% 20.55/4.07 % (2675315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.55/4.07 % (2675315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.55/4.07 % (2675315)CaDiCaL version: 2.1.3
% 20.55/4.07 % (2675315)Termination reason: Instruction limit
% 20.55/4.07 % (2675315)Termination phase: Saturation
% 20.55/4.07 % (2675315)Time elapsed: 0.049 s
% 20.55/4.07 % (2675315)Peak memory usage: 96 MB
% 20.55/4.07 % (2675315)Instructions burned: 134 (million)
% 20.55/4.07 % (2675316)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2928813599:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 20.55/4.07 % (2675318)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=442548451:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 20.55/4.07 % (2675316)Instruction limit reached!
% 20.55/4.07 % (2675316)------------------------------
% 20.55/4.07 % (2675316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.55/4.07 % (2675316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.55/4.07 % (2675316)CaDiCaL version: 2.1.3
% 20.55/4.07 % (2675316)Termination reason: Instruction limit
% 20.55/4.07 % (2675316)Termination phase: Saturation
% 20.55/4.07 % (2675316)Time elapsed: 0.330 s
% 20.55/4.07 % (2675316)Peak memory usage: 107 MB
% 20.55/4.07 % (2675316)Instructions burned: 594 (million)
% 20.55/4.07 % (2675321)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=564962456:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 20.55/4.07 % (2675321)Instruction limit reached!
% 20.55/4.07 % (2675321)------------------------------
% 20.55/4.07 % (2675321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.55/4.07 % (2675321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.55/4.07 % (2675321)CaDiCaL version: 2.1.3
% 20.55/4.07 % (2675321)Termination reason: Instruction limit
% 20.55/4.07 % (2675321)Termination phase: Saturation
% 20.55/4.07 % (2675321)Time elapsed: 0.075 s
% 20.55/4.07 % (2675321)Peak memory usage: 94 MB
% 20.55/4.07 % (2675321)Instructions burned: 125 (million)
% 20.55/4.07 % (2675323)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=25615768:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 20.55/4.07 % (2675300)Instruction limit reached!
% 20.55/4.07 % (2675300)------------------------------
% 20.55/4.07 % (2675300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.55/4.07 % (2675300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.55/4.07 % (2675300)CaDiCaL version: 2.1.3
% 20.55/4.07 % (2675300)Termination reason: Instruction limit
% 20.55/4.07 % (2675300)Termination phase: Saturation
% 20.55/4.07 % (2675300)Time elapsed: 1.506 s
% 20.55/4.07 % (2675300)Peak memory usage: 241 MB
% 20.55/4.07 % (2675300)Instructions burned: 2351 (million)
% 20.55/4.07 % (2675323)Instruction limit reached!
% 20.55/4.07 % (2675323)------------------------------
% 20.55/4.07 % (2675323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.55/4.07 % (2675323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.55/4.07 % (2675323)CaDiCaL version: 2.1.3
% 20.55/4.07 % (2675323)Termination reason: Instruction limit
% 20.55/4.07 % (2675323)Termination phase: Preprocessing 1
% 20.55/4.07 % (2675323)Time elapsed: 0.068 s
% 20.55/4.07 % (2675323)Peak memory usage: 90 MB
% 20.55/4.07 % (2675323)Instructions burned: 134 (million)
% 20.55/4.07 % (2675325)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2865414781:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 20.55/4.07 % (2675326)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4097907567:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 20.55/4.07 % (2675325)Instruction limit reached!
% 20.55/4.07 % (2675325)------------------------------
% 20.55/4.07 % (2675325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.55/4.07 % (2675325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.55/4.07 % (2675325)CaDiCaL version: 2.1.3
% 20.55/4.07 % (2675325)Termination reason: Instruction limit
% 20.55/4.07 % (2675325)Termination phase: Saturation
% 20.55/4.07 % (2675325)Time elapsed: 0.084 s
% 20.55/4.07 % (2675325)Peak memory usage: 96 MB
% 20.55/4.07 % (2675325)Instructions burned: 143 (million)
% 20.55/4.07 % (2675329)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=3916260624:i=6060:aac=none:ins=25_2974 on theBenchmark for (2974ds/6060Mi)
% 20.55/4.07 % (2675326)Instruction limit reached!
% 20.55/4.07 % (2675326)------------------------------
% 20.55/4.07 % (2675326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.55/4.07 % (2675326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.55/4.07 % (2675326)CaDiCaL version: 2.1.3
% 20.55/4.07 % (2675326)Termination reason: Instruction limit
% 20.55/4.07 % (2675326)Termination phase: Saturation
% 20.55/4.07 % (2675326)Time elapsed: 0.238 s
% 20.55/4.07 % (2675326)Peak memory usage: 96 MB
% 20.55/4.07 % (2675326)Instructions burned: 432 (million)
% 20.55/4.07 % (2675331)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=1316307885:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 20.55/4.07 % (2675331)Instruction limit reached!
% 20.55/4.07 % (2675331)------------------------------
% 20.55/4.07 % (2675331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.55/4.07 % (2675331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.55/4.07 % (2675331)CaDiCaL version: 2.1.3
% 20.55/4.07 % (2675331)Termination reason: Instruction limit
% 20.55/4.07 % (2675331)Termination phase: Preprocessing 3
% 20.55/4.07 % (2675331)Time elapsed: 0.101 s
% 20.55/4.07 % (2675331)Peak memory usage: 97 MB
% 20.55/4.07 % (2675331)Instructions burned: 150 (million)
% 20.55/4.07 % (2675277)First to succeed.
% 20.55/4.07 % (2675277)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2675272"
% 20.55/4.07 % (2675333)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3294817350:i=14155:bd=all_2969 on theBenchmark for (2969ds/14155Mi)
% 20.55/4.07 % (2675277)Refutation found. Thanks to Tanya!
% 20.55/4.07 % SZS status Theorem for theBenchmark
% 20.55/4.07 % SZS output start Proof for theBenchmark
% See solution above
% 24.34/4.27 % (2675277)------------------------------
% 24.34/4.27 % (2675277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.34/4.27 % (2675277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.34/4.27 % (2675277)CaDiCaL version: 2.1.3
% 24.34/4.27 % (2675277)Termination reason: Refutation
% 24.34/4.27 % (2675277)Time elapsed: 2.924 s
% 24.34/4.27 % (2675277)Peak memory usage: 280 MB
% 24.34/4.27 % (2675277)Instructions burned: 4906 (million)
% 24.34/4.27 % (2675277)------------------------------
% 24.34/4.27 % (2675277)------------------------------
% 24.34/4.27 % (2675272)Success in time 3.448 s
% 24.34/4.27 % Vampire exiting
%------------------------------------------------------------------------------