%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG232+3 : 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 : n003.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 09:19:31 AM UTC 2026
% Result : Theorem 15.18s 5.17s
% Output : Refutation 26.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 16
% Syntax : Number of formulae : 132 ( 42 unt; 0 def)
% Number of atoms : 416 ( 54 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 495 ( 211 ~; 206 |; 47 &)
% ( 3 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 4 con; 0-4 aty)
% Number of variables : 283 ( 276 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21,axiom,
! [X0,X1] : k2_tarski(X0,X1) = k2_tarski(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f91,axiom,
! [X0,X1] : k2_xboole_0(X0,k3_xboole_0(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t22_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(f602,axiom,
! [X0,X1] : k1_setfam_1(k2_tarski(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_setfam_1) ).
fof(f5236,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_pboole(X2,X0)
=> ! [X3] :
( m1_pboole(X3,X0)
=> ( ( r2_pboole(X0,X1,X2)
& r2_pboole(X0,X1,X3) )
=> r2_pboole(X0,X1,k3_pboole(X0,X2,X3)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t19_pboole) ).
fof(f5245,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_pboole(X2,X0)
=> ! [X3] :
( m1_pboole(X3,X0)
=> ( r6_pboole(X0,X1,k2_pboole(X0,X2,X3))
<=> ( r2_pboole(X0,X2,X1)
& r2_pboole(X0,X3,X1)
& ! [X4] :
( m1_pboole(X4,X0)
=> ( ( r2_pboole(X0,X2,X4)
& r2_pboole(X0,X3,X4) )
=> r2_pboole(X0,X1,X4) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t28_pboole) ).
fof(f5394,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m4_pboole(X2,X0,X1)
=> m1_pboole(X2,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m4_pboole) ).
fof(f14409,axiom,
! [X0,X1,X2] :
( m1_pboole(X2,X0)
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X2)))
=> m1_subset_1(k4_xboole_0(X3,X1),k1_zfmisc_1(k1_closure2(X0,X2))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_closure2) ).
fof(f14481,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> k6_closure2(X0,X1) = k1_closure2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k6_closure2) ).
fof(f16932,axiom,
! [X0,X1,X2] :
( ( m1_pboole(X1,X0)
& m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) )
=> m4_pboole(k2_closure3(X0,X1,X2),X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_closure3) ).
fof(f16934,axiom,
! [X0,X1,X2,X3] :
( ( m1_pboole(X1,X0)
& m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
& m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) )
=> k3_closure3(X0,X1,X2,X3) = k3_closure3(X0,X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k3_closure3) ).
fof(f16936,axiom,
! [X0,X1,X2,X3] :
( ( m1_pboole(X1,X0)
& m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
& m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) )
=> k3_closure3(X0,X1,X2,X3) = k2_xboole_0(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k3_closure3) ).
fof(f16937,axiom,
! [X0,X1,X2,X3] :
( ( m1_pboole(X1,X0)
& m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
& m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) )
=> m1_subset_1(k4_closure3(X0,X1,X2,X3),k1_zfmisc_1(k1_closure2(X0,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_closure3) ).
fof(f16940,axiom,
! [X0,X1,X2,X3] :
( ( m1_pboole(X1,X0)
& m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
& m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) )
=> k4_closure3(X0,X1,X2,X3) = k3_xboole_0(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_closure3) ).
fof(f16958,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
=> r6_pboole(X0,k2_closure3(X0,X1,k3_closure3(X0,X1,X2,X3)),k2_pboole(X0,k2_closure3(X0,X1,X2),k2_closure3(X0,X1,X3))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t11_closure3) ).
fof(f16960,conjecture,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
=> r2_pboole(X0,k2_closure3(X0,X1,k4_closure3(X0,X1,X2,X3)),k3_pboole(X0,k2_closure3(X0,X1,X2),k2_closure3(X0,X1,X3))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t13_closure3) ).
fof(f16961,negated_conjecture,
~ ! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
=> r2_pboole(X0,k2_closure3(X0,X1,k4_closure3(X0,X1,X2,X3)),k3_pboole(X0,k2_closure3(X0,X1,X2),k2_closure3(X0,X1,X3))) ) ) ),
inference(negated_conjecture,[status(cth)],[f16960]) ).
fof(f17022,plain,
! [X0,X1,X2] :
( m4_pboole(k2_closure3(X0,X1,X2),X0,X1)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(ennf_transformation,[],[f16932]) ).
fof(f17023,plain,
! [X0,X1,X2] :
( m4_pboole(k2_closure3(X0,X1,X2),X0,X1)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(flattening,[],[f17022]) ).
fof(f17026,plain,
! [X0,X1,X2,X3] :
( k3_closure3(X0,X1,X2,X3) = k3_closure3(X0,X1,X3,X2)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(ennf_transformation,[],[f16934]) ).
fof(f17027,plain,
! [X0,X1,X2,X3] :
( k3_closure3(X0,X1,X2,X3) = k3_closure3(X0,X1,X3,X2)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(flattening,[],[f17026]) ).
fof(f17030,plain,
! [X0,X1,X2,X3] :
( k3_closure3(X0,X1,X2,X3) = k2_xboole_0(X2,X3)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(ennf_transformation,[],[f16936]) ).
fof(f17031,plain,
! [X0,X1,X2,X3] :
( k3_closure3(X0,X1,X2,X3) = k2_xboole_0(X2,X3)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(flattening,[],[f17030]) ).
fof(f17032,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_closure3(X0,X1,X2,X3),k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(ennf_transformation,[],[f16937]) ).
fof(f17033,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_closure3(X0,X1,X2,X3),k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(flattening,[],[f17032]) ).
fof(f17038,plain,
! [X0,X1,X2,X3] :
( k4_closure3(X0,X1,X2,X3) = k3_xboole_0(X2,X3)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(ennf_transformation,[],[f16940]) ).
fof(f17039,plain,
! [X0,X1,X2,X3] :
( k4_closure3(X0,X1,X2,X3) = k3_xboole_0(X2,X3)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(flattening,[],[f17038]) ).
fof(f17068,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( r6_pboole(X0,k2_closure3(X0,X1,k3_closure3(X0,X1,X2,X3)),k2_pboole(X0,k2_closure3(X0,X1,X2),k2_closure3(X0,X1,X3)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f16958]) ).
fof(f17071,plain,
? [X0,X1] :
( ? [X2] :
( ? [X3] :
( ~ r2_pboole(X0,k2_closure3(X0,X1,k4_closure3(X0,X1,X2,X3)),k3_pboole(X0,k2_closure3(X0,X1,X2),k2_closure3(X0,X1,X3)))
& m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) )
& m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) )
& m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f16961]) ).
fof(f17113,plain,
! [X0,X1,X2] :
( ! [X3] :
( m1_subset_1(k4_xboole_0(X3,X1),k1_zfmisc_1(k1_closure2(X0,X2)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X2))) )
| ~ m1_pboole(X2,X0) ),
inference(ennf_transformation,[],[f14409]) ).
fof(f17117,plain,
! [X0,X1] :
( k6_closure2(X0,X1) = k1_closure2(X0,X1)
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f14481]) ).
fof(f17127,plain,
! [X0,X1] :
( ! [X2] :
( m1_pboole(X2,X0)
| ~ m4_pboole(X2,X0,X1) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f5394]) ).
fof(f17679,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( r6_pboole(X0,X1,k2_pboole(X0,X2,X3))
<=> ( r2_pboole(X0,X2,X1)
& r2_pboole(X0,X3,X1)
& ! [X4] :
( r2_pboole(X0,X1,X4)
| ~ r2_pboole(X0,X2,X4)
| ~ r2_pboole(X0,X3,X4)
| ~ m1_pboole(X4,X0) ) ) )
| ~ m1_pboole(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f5245]) ).
fof(f17680,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( r6_pboole(X0,X1,k2_pboole(X0,X2,X3))
<=> ( r2_pboole(X0,X2,X1)
& r2_pboole(X0,X3,X1)
& ! [X4] :
( r2_pboole(X0,X1,X4)
| ~ r2_pboole(X0,X2,X4)
| ~ r2_pboole(X0,X3,X4)
| ~ m1_pboole(X4,X0) ) ) )
| ~ m1_pboole(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(flattening,[],[f17679]) ).
fof(f17715,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( r2_pboole(X0,X1,k3_pboole(X0,X2,X3))
| ~ r2_pboole(X0,X1,X2)
| ~ r2_pboole(X0,X1,X3)
| ~ m1_pboole(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f5236]) ).
fof(f17716,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( r2_pboole(X0,X1,k3_pboole(X0,X2,X3))
| ~ r2_pboole(X0,X1,X2)
| ~ r2_pboole(X0,X1,X3)
| ~ m1_pboole(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(flattening,[],[f17715]) ).
fof(f21008,plain,
( ~ r2_pboole(sK30,k2_closure3(sK30,sK31,k4_closure3(sK30,sK31,sK32,sK33)),k3_pboole(sK30,k2_closure3(sK30,sK31,sK32),k2_closure3(sK30,sK31,sK33)))
& m1_subset_1(sK33,k1_zfmisc_1(k1_closure2(sK30,sK31)))
& m1_subset_1(sK32,k1_zfmisc_1(k1_closure2(sK30,sK31)))
& m1_pboole(sK31,sK30) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30,sK31,sK32,sK33]),skolemize(X0,sK30),skolemize(X1,sK31),skolemize(X2,sK32),skolemize(X3,sK33)],[f17071]) ).
fof(f21205,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( ( r6_pboole(X0,X1,k2_pboole(X0,X2,X3))
| ~ r2_pboole(X0,X2,X1)
| ~ r2_pboole(X0,X3,X1)
| ? [X4] :
( ~ r2_pboole(X0,X1,X4)
& r2_pboole(X0,X2,X4)
& r2_pboole(X0,X3,X4)
& m1_pboole(X4,X0) ) )
& ( ( r2_pboole(X0,X2,X1)
& r2_pboole(X0,X3,X1)
& ! [X4] :
( r2_pboole(X0,X1,X4)
| ~ r2_pboole(X0,X2,X4)
| ~ r2_pboole(X0,X3,X4)
| ~ m1_pboole(X4,X0) ) )
| ~ r6_pboole(X0,X1,k2_pboole(X0,X2,X3)) ) )
| ~ m1_pboole(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(nnf_transformation,[],[f17680]) ).
fof(f21206,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( ( r6_pboole(X0,X1,k2_pboole(X0,X2,X3))
| ~ r2_pboole(X0,X2,X1)
| ~ r2_pboole(X0,X3,X1)
| ? [X4] :
( ~ r2_pboole(X0,X1,X4)
& r2_pboole(X0,X2,X4)
& r2_pboole(X0,X3,X4)
& m1_pboole(X4,X0) ) )
& ( ( r2_pboole(X0,X2,X1)
& r2_pboole(X0,X3,X1)
& ! [X4] :
( r2_pboole(X0,X1,X4)
| ~ r2_pboole(X0,X2,X4)
| ~ r2_pboole(X0,X3,X4)
| ~ m1_pboole(X4,X0) ) )
| ~ r6_pboole(X0,X1,k2_pboole(X0,X2,X3)) ) )
| ~ m1_pboole(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(flattening,[],[f21205]) ).
fof(f21207,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( ( r6_pboole(X0,X1,k2_pboole(X0,X2,X3))
| ~ r2_pboole(X0,X2,X1)
| ~ r2_pboole(X0,X3,X1)
| ? [X4] :
( ~ r2_pboole(X0,X1,X4)
& r2_pboole(X0,X2,X4)
& r2_pboole(X0,X3,X4)
& m1_pboole(X4,X0) ) )
& ( ( r2_pboole(X0,X2,X1)
& r2_pboole(X0,X3,X1)
& ! [X5] :
( r2_pboole(X0,X1,X5)
| ~ r2_pboole(X0,X2,X5)
| ~ r2_pboole(X0,X3,X5)
| ~ m1_pboole(X5,X0) ) )
| ~ r6_pboole(X0,X1,k2_pboole(X0,X2,X3)) ) )
| ~ m1_pboole(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(rectify,[],[f21206]) ).
fof(f21208,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( ( r6_pboole(X0,X1,k2_pboole(X0,X2,X3))
| ~ r2_pboole(X0,X2,X1)
| ~ r2_pboole(X0,X3,X1)
| ( ~ r2_pboole(X0,X1,sK151(X0,X1,X2,X3))
& r2_pboole(X0,X2,sK151(X0,X1,X2,X3))
& r2_pboole(X0,X3,sK151(X0,X1,X2,X3))
& m1_pboole(sK151(X0,X1,X2,X3),X0) ) )
& ( ( r2_pboole(X0,X2,X1)
& r2_pboole(X0,X3,X1)
& ! [X5] :
( r2_pboole(X0,X1,X5)
| ~ r2_pboole(X0,X2,X5)
| ~ r2_pboole(X0,X3,X5)
| ~ m1_pboole(X5,X0) ) )
| ~ r6_pboole(X0,X1,k2_pboole(X0,X2,X3)) ) )
| ~ m1_pboole(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK151]),skolemize(X4,sK151(X0,X1,X2,X3))],[f21207]) ).
fof(f22294,plain,
! [X2,X0,X1] :
( m4_pboole(k2_closure3(X0,X1,X2),X0,X1)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(cnf_transformation,[],[f17023]) ).
fof(f22296,plain,
! [X2,X3,X0,X1] :
( ~ m1_pboole(X1,X0)
| k3_closure3(X0,X1,X2,X3) = k3_closure3(X0,X1,X3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(cnf_transformation,[],[f17027]) ).
fof(f22298,plain,
! [X2,X3,X0,X1] :
( ~ m1_pboole(X1,X0)
| k2_xboole_0(X2,X3) = k3_closure3(X0,X1,X2,X3)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(cnf_transformation,[],[f17031]) ).
fof(f22299,plain,
! [X2,X3,X0,X1] :
( ~ m1_pboole(X1,X0)
| m1_subset_1(k4_closure3(X0,X1,X2,X3),k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(cnf_transformation,[],[f17033]) ).
fof(f22302,plain,
! [X2,X3,X0,X1] :
( k3_xboole_0(X2,X3) = k4_closure3(X0,X1,X2,X3)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(cnf_transformation,[],[f17039]) ).
fof(f22338,plain,
! [X2,X3,X0,X1] :
( ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| r6_pboole(X0,k2_closure3(X0,X1,k3_closure3(X0,X1,X2,X3)),k2_pboole(X0,k2_closure3(X0,X1,X2),k2_closure3(X0,X1,X3))) ),
inference(cnf_transformation,[],[f17068]) ).
fof(f22340,plain,
m1_pboole(sK31,sK30),
inference(cnf_transformation,[],[f21008]) ).
fof(f22341,plain,
m1_subset_1(sK32,k1_zfmisc_1(k1_closure2(sK30,sK31))),
inference(cnf_transformation,[],[f21008]) ).
fof(f22342,plain,
m1_subset_1(sK33,k1_zfmisc_1(k1_closure2(sK30,sK31))),
inference(cnf_transformation,[],[f21008]) ).
fof(f22343,plain,
~ r2_pboole(sK30,k2_closure3(sK30,sK31,k4_closure3(sK30,sK31,sK32,sK33)),k3_pboole(sK30,k2_closure3(sK30,sK31,sK32),k2_closure3(sK30,sK31,sK33))),
inference(cnf_transformation,[],[f21008]) ).
fof(f22388,plain,
! [X2,X3,X0,X1] :
( ~ m1_pboole(X2,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X2)))
| m1_subset_1(k4_xboole_0(X3,X1),k1_zfmisc_1(k1_closure2(X0,X2))) ),
inference(cnf_transformation,[],[f17113]) ).
fof(f22395,plain,
! [X0,X1] :
( ~ m1_pboole(X1,X0)
| k1_closure2(X0,X1) = k6_closure2(X0,X1) ),
inference(cnf_transformation,[],[f17117]) ).
fof(f22413,plain,
! [X2,X0,X1] :
( ~ m4_pboole(X2,X0,X1)
| m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f17127]) ).
fof(f22516,plain,
! [X0,X1] : k2_xboole_0(X0,k3_xboole_0(X0,X1)) = X0,
inference(cnf_transformation,[],[f91]) ).
fof(f23178,plain,
! [X2,X3,X0,X1] :
( ~ r6_pboole(X0,X1,k2_pboole(X0,X2,X3))
| r2_pboole(X0,X2,X1)
| ~ m1_pboole(X3,X0)
| ~ m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f21208]) ).
fof(f23220,plain,
! [X2,X3,X0,X1] :
( ~ m1_pboole(X1,X0)
| ~ r2_pboole(X0,X1,X2)
| ~ r2_pboole(X0,X1,X3)
| ~ m1_pboole(X3,X0)
| ~ m1_pboole(X2,X0)
| r2_pboole(X0,X1,k3_pboole(X0,X2,X3)) ),
inference(cnf_transformation,[],[f17716]) ).
fof(f23313,plain,
! [X0,X1] : k2_tarski(X0,X1) = k2_tarski(X1,X0),
inference(cnf_transformation,[],[f21]) ).
fof(f23398,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f25079,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k1_setfam_1(k2_tarski(X0,X1)),
inference(cnf_transformation,[],[f602]) ).
fof(f27919,plain,
! [X2,X3,X0,X1] :
( k4_closure3(X0,X1,X2,X3) = k4_xboole_0(X2,k4_xboole_0(X2,X3))
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(definition_unfolding,[],[f22302,f23398]) ).
fof(f27983,plain,
! [X0,X1] : k2_xboole_0(X0,k4_xboole_0(X0,k4_xboole_0(X0,X1))) = X0,
inference(definition_unfolding,[],[f22516,f23398]) ).
fof(f28804,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k1_setfam_1(k2_tarski(X0,X1)),
inference(definition_unfolding,[],[f25079,f23398]) ).
fof(f30275,plain,
! [X0,X1] : k2_xboole_0(X0,k1_setfam_1(k2_tarski(X0,X1))) = X0,
inference(forward_demodulation,[],[f27983,f28804]) ).
fof(f30313,plain,
! [X2,X3,X0,X1] :
( ~ m1_pboole(X1,X0)
| k4_closure3(X0,X1,X2,X3) = k1_setfam_1(k2_tarski(X2,X3))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(forward_demodulation,[],[f27919,f28804]) ).
fof(f30606,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK30,sK31)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK30,sK31)))
| k1_setfam_1(k2_tarski(X0,X1)) = k4_closure3(sK30,sK31,X0,X1) ),
inference(resolution,[],[f30313,f22340]) ).
fof(f30607,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK30,sK31)))
| k1_setfam_1(k2_tarski(X0,sK33)) = k4_closure3(sK30,sK31,X0,sK33) ),
inference(resolution,[],[f30606,f22342]) ).
fof(f30608,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK30,sK31)))
| k1_setfam_1(k2_tarski(X0,sK32)) = k4_closure3(sK30,sK31,X0,sK32) ),
inference(resolution,[],[f30606,f22341]) ).
fof(f30609,plain,
k1_setfam_1(k2_tarski(sK33,sK32)) = k4_closure3(sK30,sK31,sK33,sK32),
inference(resolution,[],[f30608,f22342]) ).
fof(f30612,plain,
k4_closure3(sK30,sK31,sK33,sK32) = k1_setfam_1(k2_tarski(sK32,sK33)),
inference(forward_demodulation,[],[f30609,f23313]) ).
fof(f30614,plain,
k4_closure3(sK30,sK31,sK32,sK33) = k1_setfam_1(k2_tarski(sK32,sK33)),
inference(resolution,[],[f30607,f22341]) ).
fof(f30616,plain,
~ r2_pboole(sK30,k2_closure3(sK30,sK31,k1_setfam_1(k2_tarski(sK32,sK33))),k3_pboole(sK30,k2_closure3(sK30,sK31,sK32),k2_closure3(sK30,sK31,sK33))),
inference(superposition,[],[f22343,f30614]) ).
fof(f30618,plain,
k1_closure2(sK30,sK31) = k6_closure2(sK30,sK31),
inference(resolution,[],[f22395,f22340]) ).
fof(f30622,plain,
m1_subset_1(sK32,k1_zfmisc_1(k6_closure2(sK30,sK31))),
inference(superposition,[],[f22341,f30618]) ).
fof(f30623,plain,
m1_subset_1(sK33,k1_zfmisc_1(k6_closure2(sK30,sK31))),
inference(superposition,[],[f22342,f30618]) ).
fof(f30636,plain,
! [X0,X1] :
( m1_subset_1(k4_closure3(sK30,sK31,X0,X1),k1_zfmisc_1(k1_closure2(sK30,sK31)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK30,sK31)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK30,sK31))) ),
inference(resolution,[],[f22299,f22340]) ).
fof(f30637,plain,
! [X0,X1] :
( m1_subset_1(k4_closure3(sK30,sK31,X0,X1),k1_zfmisc_1(k6_closure2(sK30,sK31)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK30,sK31)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK30,sK31))) ),
inference(forward_demodulation,[],[f30636,f30618]) ).
fof(f30638,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| m1_subset_1(k4_closure3(sK30,sK31,X0,X1),k1_zfmisc_1(k6_closure2(sK30,sK31)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK30,sK31))) ),
inference(forward_demodulation,[],[f30637,f30618]) ).
fof(f30639,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| m1_subset_1(k4_closure3(sK30,sK31,X0,X1),k1_zfmisc_1(k6_closure2(sK30,sK31))) ),
inference(forward_demodulation,[],[f30638,f30618]) ).
fof(f30640,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| m1_subset_1(k4_closure3(sK30,sK31,sK33,X0),k1_zfmisc_1(k6_closure2(sK30,sK31))) ),
inference(resolution,[],[f30639,f30623]) ).
fof(f30643,plain,
m1_subset_1(k4_closure3(sK30,sK31,sK33,sK32),k1_zfmisc_1(k6_closure2(sK30,sK31))),
inference(resolution,[],[f30640,f30622]) ).
fof(f30644,plain,
m1_subset_1(k1_setfam_1(k2_tarski(sK32,sK33)),k1_zfmisc_1(k6_closure2(sK30,sK31))),
inference(forward_demodulation,[],[f30643,f30612]) ).
fof(f30724,plain,
! [X0,X1] :
( k2_xboole_0(X0,X1) = k3_closure3(sK30,sK31,X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK30,sK31)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK30,sK31))) ),
inference(resolution,[],[f22298,f22340]) ).
fof(f30727,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| k2_xboole_0(X0,X1) = k3_closure3(sK30,sK31,X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK30,sK31))) ),
inference(forward_demodulation,[],[f30724,f30618]) ).
fof(f30729,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| k2_xboole_0(X0,X1) = k3_closure3(sK30,sK31,X0,X1) ),
inference(forward_demodulation,[],[f30727,f30618]) ).
fof(f30730,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| k2_xboole_0(sK33,X0) = k3_closure3(sK30,sK31,sK33,X0) ),
inference(resolution,[],[f30729,f30623]) ).
fof(f30731,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| k2_xboole_0(sK32,X0) = k3_closure3(sK30,sK31,sK32,X0) ),
inference(resolution,[],[f30729,f30622]) ).
fof(f30740,plain,
k2_xboole_0(sK32,k1_setfam_1(k2_tarski(sK32,sK33))) = k3_closure3(sK30,sK31,sK32,k1_setfam_1(k2_tarski(sK32,sK33))),
inference(resolution,[],[f30731,f30644]) ).
fof(f30741,plain,
sK32 = k3_closure3(sK30,sK31,sK32,k1_setfam_1(k2_tarski(sK32,sK33))),
inference(forward_demodulation,[],[f30740,f30275]) ).
fof(f30743,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK30,sK31)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK30,sK31)))
| r6_pboole(sK30,k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X1,X0)),k2_pboole(sK30,k2_closure3(sK30,sK31,X1),k2_closure3(sK30,sK31,X0))) ),
inference(resolution,[],[f22338,f22340]) ).
fof(f30746,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK30,sK31)))
| r6_pboole(sK30,k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X1,X0)),k2_pboole(sK30,k2_closure3(sK30,sK31,X1),k2_closure3(sK30,sK31,X0))) ),
inference(forward_demodulation,[],[f30743,f30618]) ).
fof(f30748,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| r6_pboole(sK30,k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X1,X0)),k2_pboole(sK30,k2_closure3(sK30,sK31,X1),k2_closure3(sK30,sK31,X0))) ),
inference(forward_demodulation,[],[f30746,f30618]) ).
fof(f30749,plain,
! [X0] :
( r6_pboole(sK30,k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X0,sK33)),k2_pboole(sK30,k2_closure3(sK30,sK31,X0),k2_closure3(sK30,sK31,sK33)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31))) ),
inference(resolution,[],[f30748,f30623]) ).
fof(f30750,plain,
! [X0] :
( r6_pboole(sK30,k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X0,sK32)),k2_pboole(sK30,k2_closure3(sK30,sK31,X0),k2_closure3(sK30,sK31,sK32)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31))) ),
inference(resolution,[],[f30748,f30622]) ).
fof(f30752,plain,
! [X2,X0,X1] :
( m1_pboole(k2_closure3(X0,X1,X2),X0)
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(resolution,[],[f22413,f22294]) ).
fof(f30753,plain,
! [X2,X0,X1] :
( ~ m1_pboole(X1,X0)
| m1_pboole(k2_closure3(X0,X1,X2),X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) ),
inference(duplicate_literal_removal,[],[f30752]) ).
fof(f30754,plain,
! [X0] :
( m1_pboole(k2_closure3(sK30,sK31,X0),sK30)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK30,sK31))) ),
inference(resolution,[],[f30753,f22340]) ).
fof(f30757,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| m1_pboole(k2_closure3(sK30,sK31,X0),sK30) ),
inference(forward_demodulation,[],[f30754,f30618]) ).
fof(f30758,plain,
m1_pboole(k2_closure3(sK30,sK31,sK33),sK30),
inference(resolution,[],[f30757,f30623]) ).
fof(f30759,plain,
m1_pboole(k2_closure3(sK30,sK31,sK32),sK30),
inference(resolution,[],[f30757,f30622]) ).
fof(f30760,plain,
m1_pboole(k2_closure3(sK30,sK31,k1_setfam_1(k2_tarski(sK32,sK33))),sK30),
inference(resolution,[],[f30757,f30644]) ).
fof(f31733,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK30,sK31)))
| m1_subset_1(k4_xboole_0(X0,X1),k1_zfmisc_1(k1_closure2(sK30,sK31))) ),
inference(resolution,[],[f22388,f22340]) ).
fof(f31744,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| m1_subset_1(k4_xboole_0(X0,X1),k1_zfmisc_1(k1_closure2(sK30,sK31))) ),
inference(forward_demodulation,[],[f31733,f30618]) ).
fof(f31750,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| m1_subset_1(k4_xboole_0(X0,X1),k1_zfmisc_1(k6_closure2(sK30,sK31))) ),
inference(forward_demodulation,[],[f31744,f30618]) ).
fof(f31755,plain,
! [X0] : m1_subset_1(k4_xboole_0(sK33,X0),k1_zfmisc_1(k6_closure2(sK30,sK31))),
inference(resolution,[],[f31750,f30623]) ).
fof(f31772,plain,
! [X0] : k2_xboole_0(sK33,k4_xboole_0(sK33,X0)) = k3_closure3(sK30,sK31,sK33,k4_xboole_0(sK33,X0)),
inference(resolution,[],[f31755,f30730]) ).
fof(f32372,plain,
! [X0,X1] :
( k3_closure3(sK30,sK31,X0,X1) = k3_closure3(sK30,sK31,X1,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK30,sK31)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK30,sK31))) ),
inference(resolution,[],[f22296,f22340]) ).
fof(f32383,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| k3_closure3(sK30,sK31,X0,X1) = k3_closure3(sK30,sK31,X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK30,sK31))) ),
inference(forward_demodulation,[],[f32372,f30618]) ).
fof(f32389,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| k3_closure3(sK30,sK31,X0,X1) = k3_closure3(sK30,sK31,X1,X0) ),
inference(forward_demodulation,[],[f32383,f30618]) ).
fof(f32397,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| k3_closure3(sK30,sK31,sK32,X0) = k3_closure3(sK30,sK31,X0,sK32) ),
inference(resolution,[],[f32389,f30622]) ).
fof(f32398,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| k3_closure3(sK30,sK31,sK33,X0) = k3_closure3(sK30,sK31,X0,sK33) ),
inference(resolution,[],[f32389,f30623]) ).
fof(f32405,plain,
! [X0] : k3_closure3(sK30,sK31,sK33,k4_xboole_0(sK33,X0)) = k3_closure3(sK30,sK31,k4_xboole_0(sK33,X0),sK33),
inference(resolution,[],[f32398,f31755]) ).
fof(f32425,plain,
! [X0] : k2_xboole_0(sK33,k4_xboole_0(sK33,X0)) = k3_closure3(sK30,sK31,k4_xboole_0(sK33,X0),sK33),
inference(forward_demodulation,[],[f32405,f31772]) ).
fof(f32434,plain,
k3_closure3(sK30,sK31,sK32,k1_setfam_1(k2_tarski(sK32,sK33))) = k3_closure3(sK30,sK31,k1_setfam_1(k2_tarski(sK32,sK33)),sK32),
inference(resolution,[],[f32397,f30644]) ).
fof(f32450,plain,
sK32 = k3_closure3(sK30,sK31,k1_setfam_1(k2_tarski(sK32,sK33)),sK32),
inference(forward_demodulation,[],[f32434,f30741]) ).
fof(f32875,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| r2_pboole(sK30,k2_closure3(sK30,sK31,X0),k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X0,sK32)))
| ~ m1_pboole(k2_closure3(sK30,sK31,sK32),sK30)
| ~ m1_pboole(k2_closure3(sK30,sK31,X0),sK30)
| ~ m1_pboole(k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X0,sK32)),sK30) ),
inference(resolution,[],[f30750,f23178]) ).
fof(f32896,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| r2_pboole(sK30,k2_closure3(sK30,sK31,X0),k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X0,sK32)))
| ~ m1_pboole(k2_closure3(sK30,sK31,sK32),sK30)
| ~ m1_pboole(k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X0,sK32)),sK30) ),
inference(forward_subsumption_resolution,[],[f32875,f30757]) ).
fof(f32898,plain,
! [X0] :
( ~ m1_pboole(k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X0,sK32)),sK30)
| r2_pboole(sK30,k2_closure3(sK30,sK31,X0),k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X0,sK32)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31))) ),
inference(forward_subsumption_resolution,[],[f32896,f30759]) ).
fof(f32923,plain,
( ~ m1_pboole(k2_closure3(sK30,sK31,sK32),sK30)
| r2_pboole(sK30,k2_closure3(sK30,sK31,k1_setfam_1(k2_tarski(sK32,sK33))),k2_closure3(sK30,sK31,sK32))
| ~ m1_subset_1(k1_setfam_1(k2_tarski(sK32,sK33)),k1_zfmisc_1(k6_closure2(sK30,sK31))) ),
inference(superposition,[],[f32898,f32450]) ).
fof(f32929,plain,
( r2_pboole(sK30,k2_closure3(sK30,sK31,k1_setfam_1(k2_tarski(sK32,sK33))),k2_closure3(sK30,sK31,sK32))
| ~ m1_subset_1(k1_setfam_1(k2_tarski(sK32,sK33)),k1_zfmisc_1(k6_closure2(sK30,sK31))) ),
inference(forward_subsumption_resolution,[],[f32923,f30759]) ).
fof(f32939,plain,
r2_pboole(sK30,k2_closure3(sK30,sK31,k1_setfam_1(k2_tarski(sK32,sK33))),k2_closure3(sK30,sK31,sK32)),
inference(forward_subsumption_resolution,[],[f32929,f30644]) ).
fof(f32956,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| r2_pboole(sK30,k2_closure3(sK30,sK31,X0),k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X0,sK33)))
| ~ m1_pboole(k2_closure3(sK30,sK31,sK33),sK30)
| ~ m1_pboole(k2_closure3(sK30,sK31,X0),sK30)
| ~ m1_pboole(k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X0,sK33)),sK30) ),
inference(resolution,[],[f30749,f23178]) ).
fof(f32969,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31)))
| r2_pboole(sK30,k2_closure3(sK30,sK31,X0),k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X0,sK33)))
| ~ m1_pboole(k2_closure3(sK30,sK31,sK33),sK30)
| ~ m1_pboole(k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X0,sK33)),sK30) ),
inference(forward_subsumption_resolution,[],[f32956,f30757]) ).
fof(f32971,plain,
! [X0] :
( ~ m1_pboole(k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X0,sK33)),sK30)
| r2_pboole(sK30,k2_closure3(sK30,sK31,X0),k2_closure3(sK30,sK31,k3_closure3(sK30,sK31,X0,sK33)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK30,sK31))) ),
inference(forward_subsumption_resolution,[],[f32969,f30758]) ).
fof(f33069,plain,
! [X0] : m1_subset_1(k1_setfam_1(k2_tarski(sK33,X0)),k1_zfmisc_1(k6_closure2(sK30,sK31))),
inference(superposition,[],[f31755,f28804]) ).
fof(f33081,plain,
! [X0] : k2_xboole_0(sK33,k1_setfam_1(k2_tarski(sK33,X0))) = k3_closure3(sK30,sK31,k1_setfam_1(k2_tarski(sK33,X0)),sK33),
inference(superposition,[],[f32425,f28804]) ).
fof(f33086,plain,
! [X0] : sK33 = k3_closure3(sK30,sK31,k1_setfam_1(k2_tarski(sK33,X0)),sK33),
inference(forward_demodulation,[],[f33081,f30275]) ).
fof(f33124,plain,
! [X0] :
( ~ m1_pboole(k2_closure3(sK30,sK31,sK33),sK30)
| r2_pboole(sK30,k2_closure3(sK30,sK31,k1_setfam_1(k2_tarski(sK33,X0))),k2_closure3(sK30,sK31,sK33))
| ~ m1_subset_1(k1_setfam_1(k2_tarski(sK33,X0)),k1_zfmisc_1(k6_closure2(sK30,sK31))) ),
inference(superposition,[],[f32971,f33086]) ).
fof(f33127,plain,
! [X0] :
( r2_pboole(sK30,k2_closure3(sK30,sK31,k1_setfam_1(k2_tarski(sK33,X0))),k2_closure3(sK30,sK31,sK33))
| ~ m1_subset_1(k1_setfam_1(k2_tarski(sK33,X0)),k1_zfmisc_1(k6_closure2(sK30,sK31))) ),
inference(forward_subsumption_resolution,[],[f33124,f30758]) ).
fof(f33128,plain,
! [X0] : r2_pboole(sK30,k2_closure3(sK30,sK31,k1_setfam_1(k2_tarski(sK33,X0))),k2_closure3(sK30,sK31,sK33)),
inference(forward_subsumption_resolution,[],[f33127,f33069]) ).
fof(f33130,plain,
! [X0] : r2_pboole(sK30,k2_closure3(sK30,sK31,k1_setfam_1(k2_tarski(X0,sK33))),k2_closure3(sK30,sK31,sK33)),
inference(superposition,[],[f33128,f23313]) ).
fof(f36639,plain,
$false,
inference(unit_resulting_resolution,[],[f23220,f30758,f30759,f32939,f33130,f30616,f30760]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG232+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.18 % Computer : n003.cluster.edu
% 0.06/0.18 % Model : x86_64 x86_64
% 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.18 % Memory : 8046.5625MB
% 0.06/0.18 % OS : Linux 6.8.0-71-generic
% 0.06/0.18 % CPULimit : 300
% 0.06/0.18 % WCLimit : 300
% 0.06/0.18 % DateTime : Mon Sep 28 19:57:01 UTC 2026
% 0.06/0.18 % CPUTime :
% 0.06/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.21 Running first-order theorem proving
% 0.06/0.21 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.60/3.30 % (1929334)Detected formulas, will run a generic FOF schedule.
% 13.60/3.30 % (1929343)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1794696468:i=119:av=off:ss=axioms_2990 on theBenchmark for (2990ds/119Mi)
% 13.60/3.30 % (1929340)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=2580236035:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2990 on theBenchmark for (2990ds/134677Mi)
% 13.60/3.30 % (1929339)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=1315749119:i=141193_2990 on theBenchmark for (2990ds/141193Mi)
% 13.60/3.30 % (1929341)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=752345015:i=141695:sd=1:nm=32:gsp=on:ss=included_2990 on theBenchmark for (2990ds/141695Mi)
% 13.60/3.30 % (1929344)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=514313472:s2a=on:i=139:gtg=position_2990 on theBenchmark for (2990ds/139Mi)
% 13.60/3.30 % (1929342)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=28380997:i=109:sd=1:ins=1:gsp=on:ss=axioms_2990 on theBenchmark for (2990ds/109Mi)
% 13.60/3.30 % (1929345)dis-21_1_sil=8000:lcm=predicate:random_seed=290701430:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2990 on theBenchmark for (2990ds/129Mi)
% 13.60/3.30 % (1929343)Instruction limit reached!
% 13.60/3.30 % (1929343)------------------------------
% 13.60/3.30 % (1929343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.60/3.30 % (1929343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.60/3.30 % (1929343)CaDiCaL version: 2.1.3
% 13.60/3.30 % (1929343)Termination reason: Instruction limit
% 13.60/3.30 % (1929343)Termination phase: Naming
% 13.60/3.30 % (1929343)Time elapsed: 0.062 s
% 13.60/3.30 % (1929343)Peak memory usage: 110 MB
% 13.60/3.30 % (1929343)Instructions burned: 119 (million)
% 13.60/3.30 % (1929344)Instruction limit reached!
% 13.60/3.30 % (1929344)------------------------------
% 13.60/3.30 % (1929344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.60/3.30 % (1929344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.60/3.30 % (1929344)CaDiCaL version: 2.1.3
% 13.60/3.30 % (1929344)Termination reason: Instruction limit
% 13.60/3.30 % (1929344)Termination phase: Property scanning
% 13.60/3.30 % (1929344)Time elapsed: 0.060 s
% 13.60/3.30 % (1929344)Peak memory usage: 108 MB
% 13.60/3.30 % (1929344)Instructions burned: 139 (million)
% 13.60/3.30 % (1929342)Instruction limit reached!
% 13.60/3.30 % (1929342)------------------------------
% 13.60/3.30 % (1929342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.60/3.30 % (1929342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.60/3.30 % (1929342)CaDiCaL version: 2.1.3
% 13.60/3.30 % (1929342)Termination reason: Instruction limit
% 13.60/3.30 % (1929342)Termination phase: Saturation
% 13.60/3.30 % (1929342)Time elapsed: 0.089 s
% 13.60/3.30 % (1929342)Peak memory usage: 112 MB
% 13.60/3.30 % (1929342)Instructions burned: 110 (million)
% 13.60/3.30 % (1929345)Instruction limit reached!
% 13.60/3.30 % (1929345)------------------------------
% 13.60/3.30 % (1929345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.60/3.30 % (1929345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.60/3.30 % (1929345)CaDiCaL version: 2.1.3
% 13.60/3.30 % (1929345)Termination reason: Instruction limit
% 13.60/3.30 % (1929345)Termination phase: SInE selection
% 13.60/3.30 % (1929345)Time elapsed: 0.089 s
% 13.60/3.30 % (1929345)Peak memory usage: 108 MB
% 13.60/3.30 % (1929345)Instructions burned: 129 (million)
% 13.60/3.30 % (1929353)lrs+10_1_sil=8000:sp=occurrence:random_seed=1523269958:i=285:sd=3:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/285Mi)
% 13.60/3.30 % (1929354)lrs+10_1_sil=32000:urr=on:br=off:random_seed=953547851:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/157Mi)
% 13.60/3.30 % (1929355)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3099994721:i=325:sd=1:ss=axioms:sgt=32_2988 on theBenchmark for (2988ds/325Mi)
% 13.60/3.30 % (1929356)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=1124742102:s2a=on:i=248:s2at=1.23:gtg=position_2988 on theBenchmark for (2988ds/248Mi)
% 13.60/3.30 % (1929353)Instruction limit reached!
% 20.56/4.31 % (1929353)------------------------------
% 20.56/4.31 % (1929353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.56/4.31 % (1929353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.56/4.31 % (1929353)CaDiCaL version: 2.1.3
% 20.56/4.31 % (1929353)Termination reason: Instruction limit
% 20.56/4.31 % (1929353)Termination phase: Saturation
% 20.56/4.31 % (1929353)Time elapsed: 0.117 s
% 20.56/4.31 % (1929353)Peak memory usage: 116 MB
% 20.56/4.31 % (1929353)Instructions burned: 286 (million)
% 20.56/4.31 % (1929354)Instruction limit reached!
% 20.56/4.31 % (1929354)------------------------------
% 20.56/4.31 % (1929354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.56/4.31 % (1929354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.56/4.31 % (1929354)CaDiCaL version: 2.1.3
% 20.56/4.31 % (1929354)Termination reason: Instruction limit
% 20.56/4.31 % (1929354)Termination phase: Property scanning
% 20.56/4.31 % (1929354)Time elapsed: 0.069 s
% 20.56/4.31 % (1929354)Peak memory usage: 108 MB
% 20.56/4.31 % (1929354)Instructions burned: 158 (million)
% 20.56/4.31 % (1929361)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2898330491:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2987 on theBenchmark for (2987ds/294Mi)
% 20.56/4.31 % (1929356)Instruction limit reached!
% 20.56/4.31 % (1929356)------------------------------
% 20.56/4.31 % (1929356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.56/4.31 % (1929356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.56/4.31 % (1929356)CaDiCaL version: 2.1.3
% 20.56/4.31 % (1929356)Termination reason: Instruction limit
% 20.56/4.31 % (1929356)Termination phase: SInE selection
% 20.56/4.31 % (1929356)Time elapsed: 0.119 s
% 20.56/4.31 % (1929356)Peak memory usage: 108 MB
% 20.56/4.31 % (1929356)Instructions burned: 249 (million)
% 20.56/4.31 % (1929362)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1274163348:i=2350_2986 on theBenchmark for (2986ds/2350Mi)
% 20.56/4.31 % (1929361)Instruction limit reached!
% 20.56/4.31 % (1929361)------------------------------
% 20.56/4.31 % (1929361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.56/4.31 % (1929361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.56/4.31 % (1929361)CaDiCaL version: 2.1.3
% 20.56/4.31 % (1929361)Termination reason: Instruction limit
% 20.56/4.31 % (1929361)Termination phase: Saturation
% 20.56/4.31 % (1929361)Time elapsed: 0.110 s
% 20.56/4.31 % (1929361)Peak memory usage: 116 MB
% 20.56/4.31 % (1929361)Instructions burned: 296 (million)
% 20.56/4.31 % (1929355)Instruction limit reached!
% 20.56/4.31 % (1929355)------------------------------
% 20.56/4.31 % (1929355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.56/4.31 % (1929355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.56/4.31 % (1929355)CaDiCaL version: 2.1.3
% 20.56/4.31 % (1929355)Termination reason: Instruction limit
% 20.56/4.31 % (1929355)Termination phase: Saturation
% 20.56/4.31 % (1929355)Time elapsed: 0.239 s
% 20.56/4.31 % (1929355)Peak memory usage: 115 MB
% 20.56/4.31 % (1929355)Instructions burned: 325 (million)
% 20.56/4.31 % (1929364)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=773760305:cts=off:i=113:fsr=off:ss=included:sgt=4_2985 on theBenchmark for (2985ds/113Mi)
% 20.56/4.31 % (1929366)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2795828710:i=127:av=off:fsr=off:sup=off_2984 on theBenchmark for (2984ds/127Mi)
% 20.56/4.31 % (1929364)Instruction limit reached!
% 20.56/4.31 % (1929364)------------------------------
% 20.56/4.31 % (1929364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.56/4.31 % (1929364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.56/4.31 % (1929364)CaDiCaL version: 2.1.3
% 20.56/4.31 % (1929364)Termination reason: Instruction limit
% 20.56/4.31 % (1929364)Termination phase: Preprocessing 1
% 20.56/4.31 % (1929364)Time elapsed: 0.098 s
% 20.56/4.31 % (1929364)Peak memory usage: 109 MB
% 20.56/4.31 % (1929364)Instructions burned: 114 (million)
% 20.56/4.31 % (1929367)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1610115807:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi)
% 20.56/4.31 % (1929366)Instruction limit reached!
% 20.56/4.31 % (1929366)------------------------------
% 20.56/4.31 % (1929366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.18/5.17 % (1929366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.18/5.17 % (1929366)CaDiCaL version: 2.1.3
% 15.18/5.17 % (1929366)Termination reason: Instruction limit
% 15.18/5.17 % (1929366)Termination phase: Preprocessing 1
% 15.18/5.17 % (1929366)Time elapsed: 0.055 s
% 15.18/5.17 % (1929366)Peak memory usage: 108 MB
% 15.18/5.17 % (1929366)Instructions burned: 130 (million)
% 15.18/5.17 % (1929367)Instruction limit reached!
% 15.18/5.17 % (1929367)------------------------------
% 15.18/5.17 % (1929367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.18/5.17 % (1929367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.18/5.17 % (1929367)CaDiCaL version: 2.1.3
% 15.18/5.17 % (1929367)Termination reason: Instruction limit
% 15.18/5.17 % (1929367)Termination phase: Property scanning
% 15.18/5.17 % (1929367)Time elapsed: 0.051 s
% 15.18/5.17 % (1929367)Peak memory usage: 108 MB
% 15.18/5.17 % (1929367)Instructions burned: 115 (million)
% 15.18/5.17 % (1929372)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3712728815:i=437:sd=1:aac=none:ss=included_2983 on theBenchmark for (2983ds/437Mi)
% 15.18/5.17 % (1929370)lrs+10_1_sil=8000:sp=occurrence:random_seed=3408438805:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2983 on theBenchmark for (2983ds/907Mi)
% 15.18/5.17 % (1929373)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2241922737:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 15.18/5.17 % (1929372)Instruction limit reached!
% 15.18/5.17 % (1929372)------------------------------
% 15.18/5.17 % (1929372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.18/5.17 % (1929372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.18/5.17 % (1929372)CaDiCaL version: 2.1.3
% 15.18/5.17 % (1929372)Termination reason: Instruction limit
% 15.18/5.17 % (1929372)Termination phase: Saturation
% 15.18/5.17 % (1929372)Time elapsed: 0.162 s
% 15.18/5.17 % (1929372)Peak memory usage: 116 MB
% 15.18/5.17 % (1929372)Instructions burned: 439 (million)
% 15.18/5.17 % (1929377)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1750250395:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 15.18/5.17 % (1929377)Instruction limit reached!
% 15.18/5.17 % (1929377)------------------------------
% 15.18/5.17 % (1929377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.18/5.17 % (1929377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.18/5.17 % (1929377)CaDiCaL version: 2.1.3
% 15.18/5.17 % (1929377)Termination reason: Instruction limit
% 15.18/5.17 % (1929377)Termination phase: Property scanning
% 15.18/5.17 % (1929377)Time elapsed: 0.065 s
% 15.18/5.17 % (1929377)Peak memory usage: 111 MB
% 15.18/5.17 % (1929377)Instructions burned: 137 (million)
% 15.18/5.17 % (1929379)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=51989034:st=8:i=592:sd=3:ep=RST:ss=axioms_2979 on theBenchmark for (2979ds/592Mi)
% 15.18/5.17 % (1929370)Instruction limit reached!
% 15.18/5.17 % (1929370)------------------------------
% 15.18/5.17 % (1929370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.18/5.17 % (1929370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.18/5.17 % (1929370)CaDiCaL version: 2.1.3
% 15.18/5.17 % (1929370)Termination reason: Instruction limit
% 15.18/5.17 % (1929370)Termination phase: Saturation
% 15.18/5.17 % (1929370)Time elapsed: 0.542 s
% 15.18/5.17 % (1929370)Peak memory usage: 127 MB
% 15.18/5.17 % (1929370)Instructions burned: 907 (million)
% 15.18/5.17 % (1929381)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=670948936:st=3:i=13193:sd=3:ss=axioms_2976 on theBenchmark for (2976ds/13193Mi)
% 15.18/5.17 % (1929379)Instruction limit reached!
% 15.18/5.17 % (1929379)------------------------------
% 15.18/5.17 % (1929379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.18/5.17 % (1929379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.18/5.17 % (1929379)CaDiCaL version: 2.1.3
% 15.18/5.17 % (1929379)Termination reason: Instruction limit
% 15.18/5.17 % (1929379)Termination phase: Property scanning
% 15.18/5.17 % (1929379)Time elapsed: 0.341 s
% 15.18/5.17 % (1929379)Peak memory usage: 131 MB
% 15.18/5.17 % (1929379)Instructions burned: 592 (million)
% 15.18/5.17 % (1929383)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=1671578050:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/125Mi)
% 15.18/5.17 % (1929383)Instruction limit reached!
% 15.18/5.17 % (1929383)------------------------------
% 15.18/5.17 % (1929383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.18/5.17 % (1929383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.18/5.17 % (1929383)CaDiCaL version: 2.1.3
% 15.18/5.17 % (1929383)Termination reason: Instruction limit
% 15.18/5.17 % (1929383)Termination phase: Property scanning
% 15.18/5.17 % (1929383)Time elapsed: 0.054 s
% 15.18/5.17 % (1929383)Peak memory usage: 108 MB
% 15.18/5.17 % (1929383)Instructions burned: 127 (million)
% 15.18/5.17 % (1929362)Instruction limit reached!
% 15.18/5.17 % (1929362)------------------------------
% 15.18/5.17 % (1929362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.18/5.17 % (1929362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.18/5.17 % (1929362)CaDiCaL version: 2.1.3
% 15.18/5.17 % (1929362)Termination reason: Instruction limit
% 15.18/5.17 % (1929362)Termination phase: Saturation
% 15.18/5.17 % (1929362)Time elapsed: 1.276 s
% 15.18/5.17 % (1929362)Peak memory usage: 173 MB
% 15.18/5.17 % (1929362)Instructions burned: 2351 (million)
% 15.18/5.17 % (1929385)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1172962661:i=134:gtgl=5:slsql=off:gtg=exists_sym_2972 on theBenchmark for (2972ds/134Mi)
% 15.18/5.17 % (1929386)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3619076688:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/141Mi)
% 15.18/5.17 % (1929385)Instruction limit reached!
% 15.18/5.17 % (1929385)------------------------------
% 15.18/5.17 % (1929385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.18/5.17 % (1929385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.18/5.17 % (1929385)CaDiCaL version: 2.1.3
% 15.18/5.17 % (1929385)Termination reason: Instruction limit
% 15.18/5.17 % (1929385)Termination phase: Property scanning
% 15.18/5.17 % (1929385)Time elapsed: 0.059 s
% 15.18/5.17 % (1929385)Peak memory usage: 108 MB
% 15.18/5.17 % (1929385)Instructions burned: 136 (million)
% 15.18/5.17 % (1929386)Instruction limit reached!
% 15.18/5.17 % (1929386)------------------------------
% 15.18/5.17 % (1929386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.18/5.17 % (1929386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.18/5.17 % (1929386)CaDiCaL version: 2.1.3
% 15.18/5.17 % (1929386)Termination reason: Instruction limit
% 15.18/5.17 % (1929386)Termination phase: Saturation
% 15.18/5.17 % (1929386)Time elapsed: 0.108 s
% 15.18/5.17 % (1929386)Peak memory usage: 113 MB
% 15.18/5.17 % (1929386)Instructions burned: 142 (million)
% 15.18/5.17 % (1929389)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3784809975:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2970 on theBenchmark for (2970ds/431Mi)
% 15.18/5.17 % (1929390)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=3041785632:i=6060:aac=none:ins=25_2970 on theBenchmark for (2970ds/6060Mi)
% 15.18/5.17 % (1929389)Refutation not found, incomplete strategy
% 15.18/5.17 % (1929389)------------------------------
% 15.18/5.17 % (1929389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.18/5.17 % (1929389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.18/5.17 % (1929389)CaDiCaL version: 2.1.3
% 15.18/5.17 % (1929389)Termination reason: Refutation not found, incomplete strategy
% 15.18/5.17 % (1929389)Time elapsed: 0.096 s
% 15.18/5.17 % (1929389)Peak memory usage: 113 MB
% 15.18/5.17 % (1929389)Instructions burned: 108 (million)
% 15.18/5.17 % (1929389)------------------------------
% 15.18/5.17 % (1929389)------------------------------
% 15.18/5.17 % (1929393)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=43174498:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2965 on theBenchmark for (2965ds/150Mi)
% 15.18/5.17 % (1929393)Instruction limit reached!
% 15.18/5.17 % (1929393)------------------------------
% 15.18/5.17 % (1929393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.18/5.17 % (1929393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.18/5.17 % (1929393)CaDiCaL version: 2.1.3
% 15.18/5.17 % (1929393)Termination reason: Instruction limit
% 15.18/5.17 % (1929393)Termination phase: Preprocessing 1
% 15.18/5.17 % (1929393)Time elapsed: 0.118 s
% 15.18/5.17 % (1929393)Peak memory usage: 109 MB
% 15.18/5.17 % (1929393)Instructions burned: 151 (million)
% 15.18/5.17 % (1929395)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3692578495:i=14155:bd=all_2963 on theBenchmark for (2963ds/14155Mi)
% 15.18/5.17 % (1929340)First to succeed.
% 15.18/5.17 % (1929340)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1929334"
% 15.18/5.17 % (1929340)Refutation found. Thanks to Tanya!
% 15.18/5.17 % SZS status Theorem for theBenchmark
% 15.18/5.17 % SZS output start Proof for theBenchmark
% See solution above
% 26.96/5.37 % (1929340)------------------------------
% 26.96/5.37 % (1929340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.96/5.37 % (1929340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.96/5.37 % (1929340)CaDiCaL version: 2.1.3
% 26.96/5.37 % (1929340)Termination reason: Refutation
% 26.96/5.37 % (1929340)Time elapsed: 3.126 s
% 26.96/5.37 % (1929340)Peak memory usage: 237 MB
% 26.96/5.37 % (1929340)Instructions burned: 4918 (million)
% 26.96/5.37 % (1929340)------------------------------
% 26.96/5.37 % (1929340)------------------------------
% 26.96/5.37 % (1929334)Success in time 4.53 s
% 26.96/5.37 % Vampire exiting
%------------------------------------------------------------------------------