%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG232+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : 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 29.50s 7.29s
% Output : Refutation 30.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 20
% Syntax : Number of formulae : 144 ( 69 unt; 0 def)
% Number of atoms : 394 ( 72 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 432 ( 182 ~; 177 |; 45 &)
% ( 3 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 5 ( 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 : 300 ( 293 !; 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(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(f57,axiom,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
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(f108,axiom,
! [X0,X1] : k2_xboole_0(X0,k4_xboole_0(X1,X0)) = k2_xboole_0(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t39_xboole_1) ).
fof(f116,axiom,
! [X0,X1] : k4_xboole_0(X0,k3_xboole_0(X0,X1)) = k4_xboole_0(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t47_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(f120,axiom,
! [X0,X1] : k2_xboole_0(k3_xboole_0(X0,X1),k4_xboole_0(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t51_xboole_1) ).
fof(f121,axiom,
! [X0,X1,X2] : k4_xboole_0(X0,k4_xboole_0(X1,X2)) = k2_xboole_0(k4_xboole_0(X0,X1),k3_xboole_0(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t52_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(f8111,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(f8120,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(f8269,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(f38341,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(f42792,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(f42796,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(f42797,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(f42800,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(f42818,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(f42820,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(f42821,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)],[f42820]) ).
fof(f42930,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,[],[f42792]) ).
fof(f42931,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,[],[f42930]) ).
fof(f42938,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,[],[f42796]) ).
fof(f42939,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,[],[f42938]) ).
fof(f42940,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,[],[f42797]) ).
fof(f42941,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,[],[f42940]) ).
fof(f42946,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,[],[f42800]) ).
fof(f42947,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,[],[f42946]) ).
fof(f42976,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,[],[f42818]) ).
fof(f42979,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,[],[f42821]) ).
fof(f43031,plain,
! [X0,X1] :
( k6_closure2(X0,X1) = k1_closure2(X0,X1)
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f38341]) ).
fof(f43036,plain,
! [X0,X1] :
( ! [X2] :
( m1_pboole(X2,X0)
| ~ m4_pboole(X2,X0,X1) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f8269]) ).
fof(f43736,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,[],[f8120]) ).
fof(f43737,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,[],[f43736]) ).
fof(f43782,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,[],[f8111]) ).
fof(f43783,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,[],[f43782]) ).
fof(f49133,plain,
( ~ r2_pboole(sK52,k2_closure3(sK52,sK53,k4_closure3(sK52,sK53,sK54,sK55)),k3_pboole(sK52,k2_closure3(sK52,sK53,sK54),k2_closure3(sK52,sK53,sK55)))
& m1_subset_1(sK55,k1_zfmisc_1(k1_closure2(sK52,sK53)))
& m1_subset_1(sK54,k1_zfmisc_1(k1_closure2(sK52,sK53)))
& m1_pboole(sK53,sK52) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52,sK53,sK54,sK55]),skolemize(X0,sK52),skolemize(X1,sK53),skolemize(X2,sK54),skolemize(X3,sK55)],[f42979]) ).
fof(f49386,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,[],[f43737]) ).
fof(f49387,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,[],[f49386]) ).
fof(f49388,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,[],[f49387]) ).
fof(f49389,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,sK209(X0,X1,X2,X3))
& r2_pboole(X0,X2,sK209(X0,X1,X2,X3))
& r2_pboole(X0,X3,sK209(X0,X1,X2,X3))
& m1_pboole(sK209(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,[sK209]),skolemize(X4,sK209(X0,X1,X2,X3))],[f49388]) ).
fof(f51036,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,[],[f42931]) ).
fof(f51040,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,[],[f42939]) ).
fof(f51041,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,[],[f42941]) ).
fof(f51044,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,[],[f42947]) ).
fof(f51080,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ 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)))
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f42976]) ).
fof(f51082,plain,
m1_pboole(sK53,sK52),
inference(cnf_transformation,[],[f49133]) ).
fof(f51083,plain,
m1_subset_1(sK54,k1_zfmisc_1(k1_closure2(sK52,sK53))),
inference(cnf_transformation,[],[f49133]) ).
fof(f51084,plain,
m1_subset_1(sK55,k1_zfmisc_1(k1_closure2(sK52,sK53))),
inference(cnf_transformation,[],[f49133]) ).
fof(f51085,plain,
~ r2_pboole(sK52,k2_closure3(sK52,sK53,k4_closure3(sK52,sK53,sK54,sK55)),k3_pboole(sK52,k2_closure3(sK52,sK53,sK54),k2_closure3(sK52,sK53,sK55))),
inference(cnf_transformation,[],[f49133]) ).
fof(f51155,plain,
! [X0,X1] :
( ~ m1_pboole(X1,X0)
| k1_closure2(X0,X1) = k6_closure2(X0,X1) ),
inference(cnf_transformation,[],[f43031]) ).
fof(f51162,plain,
! [X2,X0,X1] :
( ~ m4_pboole(X2,X0,X1)
| m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f43036]) ).
fof(f51242,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k2_xboole_0(X1,X0),
inference(cnf_transformation,[],[f54]) ).
fof(f51309,plain,
! [X0,X1] : k2_xboole_0(X0,k3_xboole_0(X0,X1)) = X0,
inference(cnf_transformation,[],[f91]) ).
fof(f51320,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf_transformation,[],[f57]) ).
fof(f52129,plain,
! [X2,X3,X0,X1] :
( ~ r6_pboole(X0,X1,k2_pboole(X0,X2,X3))
| r2_pboole(X0,X3,X1)
| ~ m1_pboole(X3,X0)
| ~ m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f49389]) ).
fof(f52187,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,[],[f43783]) ).
fof(f52326,plain,
! [X0,X1] : k2_tarski(X0,X1) = k2_tarski(X1,X0),
inference(cnf_transformation,[],[f21]) ).
fof(f52455,plain,
! [X2,X0,X1] : k4_xboole_0(X0,k4_xboole_0(X1,X2)) = k2_xboole_0(k4_xboole_0(X0,X1),k3_xboole_0(X0,X2)),
inference(cnf_transformation,[],[f121]) ).
fof(f52456,plain,
! [X0,X1] : k2_xboole_0(k3_xboole_0(X0,X1),k4_xboole_0(X0,X1)) = X0,
inference(cnf_transformation,[],[f120]) ).
fof(f52459,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f52460,plain,
! [X0,X1] : k4_xboole_0(X0,X1) = k4_xboole_0(X0,k3_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f116]) ).
fof(f52468,plain,
! [X0,X1] : k2_xboole_0(X0,X1) = k2_xboole_0(X0,k4_xboole_0(X1,X0)),
inference(cnf_transformation,[],[f108]) ).
fof(f56535,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k1_setfam_1(k2_tarski(X0,X1)),
inference(cnf_transformation,[],[f602]) ).
fof(f59855,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,[],[f51044,f52459]) ).
fof(f59943,plain,
! [X0,X1] : k2_xboole_0(X0,k4_xboole_0(X0,k4_xboole_0(X0,X1))) = X0,
inference(definition_unfolding,[],[f51309,f52459]) ).
fof(f59954,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k4_xboole_0(X1,k4_xboole_0(X1,X0)),
inference(definition_unfolding,[],[f51320,f52459,f52459]) ).
fof(f60274,plain,
! [X2,X0,X1] : k4_xboole_0(X0,k4_xboole_0(X1,X2)) = k2_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(X0,k4_xboole_0(X0,X2))),
inference(definition_unfolding,[],[f52455,f52459]) ).
fof(f60275,plain,
! [X0,X1] : k2_xboole_0(k4_xboole_0(X0,k4_xboole_0(X0,X1)),k4_xboole_0(X0,X1)) = X0,
inference(definition_unfolding,[],[f52456,f52459]) ).
fof(f60278,plain,
! [X0,X1] : k4_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,k4_xboole_0(X0,X1))),
inference(definition_unfolding,[],[f52460,f52459]) ).
fof(f61131,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k1_setfam_1(k2_tarski(X0,X1)),
inference(definition_unfolding,[],[f56535,f52459]) ).
fof(f62553,plain,
! [X0,X1] : k4_xboole_0(X0,X1) = k1_setfam_1(k2_tarski(X0,k4_xboole_0(X0,X1))),
inference(forward_demodulation,[],[f60278,f61131]) ).
fof(f62556,plain,
! [X0,X1] : k2_xboole_0(k1_setfam_1(k2_tarski(X0,X1)),k4_xboole_0(X0,X1)) = X0,
inference(forward_demodulation,[],[f60275,f61131]) ).
fof(f62557,plain,
! [X2,X0,X1] : k4_xboole_0(X0,k4_xboole_0(X1,X2)) = k2_xboole_0(k4_xboole_0(X0,X1),k1_setfam_1(k2_tarski(X0,X2))),
inference(forward_demodulation,[],[f60274,f61131]) ).
fof(f62628,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k1_setfam_1(k2_tarski(X1,X0)),
inference(forward_demodulation,[],[f59954,f61131]) ).
fof(f62637,plain,
! [X0,X1] : k2_xboole_0(X0,k1_setfam_1(k2_tarski(X0,X1))) = X0,
inference(forward_demodulation,[],[f59943,f61131]) ).
fof(f62699,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,[],[f59855,f61131]) ).
fof(f62773,plain,
! [X0,X1] : k2_xboole_0(k4_xboole_0(X0,X1),k1_setfam_1(k2_tarski(X0,X1))) = X0,
inference(forward_demodulation,[],[f62556,f51242]) ).
fof(f62862,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X1,X1)) = X0,
inference(forward_demodulation,[],[f62773,f62557]) ).
fof(f62897,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK52,sK53)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK52,sK53)))
| k1_setfam_1(k2_tarski(X0,X1)) = k4_closure3(sK52,sK53,X0,X1) ),
inference(resolution,[],[f62699,f51082]) ).
fof(f62899,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK52,sK53)))
| k1_setfam_1(k2_tarski(X0,sK55)) = k4_closure3(sK52,sK53,X0,sK55) ),
inference(resolution,[],[f62897,f51084]) ).
fof(f62904,plain,
k4_closure3(sK52,sK53,sK54,sK55) = k1_setfam_1(k2_tarski(sK54,sK55)),
inference(resolution,[],[f62899,f51083]) ).
fof(f62907,plain,
~ r2_pboole(sK52,k2_closure3(sK52,sK53,k1_setfam_1(k2_tarski(sK54,sK55))),k3_pboole(sK52,k2_closure3(sK52,sK53,sK54),k2_closure3(sK52,sK53,sK55))),
inference(superposition,[],[f51085,f62904]) ).
fof(f62918,plain,
k1_closure2(sK52,sK53) = k6_closure2(sK52,sK53),
inference(resolution,[],[f51155,f51082]) ).
fof(f62919,plain,
m1_subset_1(sK54,k1_zfmisc_1(k6_closure2(sK52,sK53))),
inference(superposition,[],[f51083,f62918]) ).
fof(f62920,plain,
m1_subset_1(sK55,k1_zfmisc_1(k6_closure2(sK52,sK53))),
inference(superposition,[],[f51084,f62918]) ).
fof(f62928,plain,
! [X0,X1] :
( m1_subset_1(k4_closure3(sK52,sK53,X0,X1),k1_zfmisc_1(k1_closure2(sK52,sK53)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK52,sK53)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK52,sK53))) ),
inference(resolution,[],[f51041,f51082]) ).
fof(f62929,plain,
! [X0,X1] :
( m1_subset_1(k4_closure3(sK52,sK53,X0,X1),k1_zfmisc_1(k6_closure2(sK52,sK53)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK52,sK53)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK52,sK53))) ),
inference(forward_demodulation,[],[f62928,f62918]) ).
fof(f62930,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK52,sK53)))
| m1_subset_1(k4_closure3(sK52,sK53,X0,X1),k1_zfmisc_1(k6_closure2(sK52,sK53)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK52,sK53))) ),
inference(forward_demodulation,[],[f62929,f62918]) ).
fof(f62931,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK52,sK53)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k6_closure2(sK52,sK53)))
| m1_subset_1(k4_closure3(sK52,sK53,X0,X1),k1_zfmisc_1(k6_closure2(sK52,sK53))) ),
inference(forward_demodulation,[],[f62930,f62918]) ).
fof(f62932,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK52,sK53)))
| m1_subset_1(k4_closure3(sK52,sK53,sK54,X0),k1_zfmisc_1(k6_closure2(sK52,sK53))) ),
inference(resolution,[],[f62931,f62919]) ).
fof(f62935,plain,
m1_subset_1(k4_closure3(sK52,sK53,sK54,sK55),k1_zfmisc_1(k6_closure2(sK52,sK53))),
inference(resolution,[],[f62932,f62920]) ).
fof(f62936,plain,
m1_subset_1(k1_setfam_1(k2_tarski(sK54,sK55)),k1_zfmisc_1(k6_closure2(sK52,sK53))),
inference(forward_demodulation,[],[f62935,f62904]) ).
fof(f62976,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,[],[f51162,f51036]) ).
fof(f62977,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,[],[f62976]) ).
fof(f62978,plain,
! [X0,X1] :
( k2_xboole_0(X0,X1) = k3_closure3(sK52,sK53,X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK52,sK53)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK52,sK53))) ),
inference(resolution,[],[f51040,f51082]) ).
fof(f62981,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK52,sK53)))
| k2_xboole_0(X0,X1) = k3_closure3(sK52,sK53,X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK52,sK53))) ),
inference(forward_demodulation,[],[f62978,f62918]) ).
fof(f62983,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK52,sK53)))
| ~ m1_subset_1(X1,k1_zfmisc_1(k6_closure2(sK52,sK53)))
| k2_xboole_0(X0,X1) = k3_closure3(sK52,sK53,X0,X1) ),
inference(forward_demodulation,[],[f62981,f62918]) ).
fof(f62984,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK52,sK53)))
| k2_xboole_0(sK54,X0) = k3_closure3(sK52,sK53,sK54,X0) ),
inference(resolution,[],[f62983,f62919]) ).
fof(f62985,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK52,sK53)))
| k2_xboole_0(sK55,X0) = k3_closure3(sK52,sK53,sK55,X0) ),
inference(resolution,[],[f62983,f62920]) ).
fof(f63026,plain,
k2_xboole_0(sK54,k1_setfam_1(k2_tarski(sK54,sK55))) = k3_closure3(sK52,sK53,sK54,k1_setfam_1(k2_tarski(sK54,sK55))),
inference(resolution,[],[f62936,f62984]) ).
fof(f63027,plain,
k2_xboole_0(sK55,k1_setfam_1(k2_tarski(sK54,sK55))) = k3_closure3(sK52,sK53,sK55,k1_setfam_1(k2_tarski(sK54,sK55))),
inference(resolution,[],[f62936,f62985]) ).
fof(f63029,plain,
sK54 = k3_closure3(sK52,sK53,sK54,k1_setfam_1(k2_tarski(sK54,sK55))),
inference(forward_demodulation,[],[f63026,f62637]) ).
fof(f63039,plain,
! [X0] :
( m1_pboole(k2_closure3(sK52,sK53,X0),sK52)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK52,sK53))) ),
inference(resolution,[],[f62977,f51082]) ).
fof(f63042,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK52,sK53)))
| m1_pboole(k2_closure3(sK52,sK53,X0),sK52) ),
inference(forward_demodulation,[],[f63039,f62918]) ).
fof(f63043,plain,
m1_pboole(k2_closure3(sK52,sK53,sK54),sK52),
inference(resolution,[],[f63042,f62919]) ).
fof(f63044,plain,
m1_pboole(k2_closure3(sK52,sK53,sK55),sK52),
inference(resolution,[],[f63042,f62920]) ).
fof(f63045,plain,
m1_pboole(k2_closure3(sK52,sK53,k1_setfam_1(k2_tarski(sK54,sK55))),sK52),
inference(resolution,[],[f63042,f62936]) ).
fof(f63326,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK52,sK53)))
| r6_pboole(sK52,k2_closure3(sK52,sK53,k3_closure3(sK52,sK53,sK54,X0)),k2_pboole(sK52,k2_closure3(sK52,sK53,sK54),k2_closure3(sK52,sK53,X0)))
| ~ m1_pboole(sK53,sK52) ),
inference(resolution,[],[f51080,f51083]) ).
fof(f63327,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK52,sK53)))
| r6_pboole(sK52,k2_closure3(sK52,sK53,k3_closure3(sK52,sK53,sK55,X0)),k2_pboole(sK52,k2_closure3(sK52,sK53,sK55),k2_closure3(sK52,sK53,X0)))
| ~ m1_pboole(sK53,sK52) ),
inference(resolution,[],[f51080,f51084]) ).
fof(f63334,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK52,sK53)))
| r6_pboole(sK52,k2_closure3(sK52,sK53,k3_closure3(sK52,sK53,sK55,X0)),k2_pboole(sK52,k2_closure3(sK52,sK53,sK55),k2_closure3(sK52,sK53,X0))) ),
inference(forward_subsumption_resolution,[],[f63327,f51082]) ).
fof(f63335,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_closure2(sK52,sK53)))
| r6_pboole(sK52,k2_closure3(sK52,sK53,k3_closure3(sK52,sK53,sK54,X0)),k2_pboole(sK52,k2_closure3(sK52,sK53,sK54),k2_closure3(sK52,sK53,X0))) ),
inference(forward_subsumption_resolution,[],[f63326,f51082]) ).
fof(f63336,plain,
! [X0] :
( r6_pboole(sK52,k2_closure3(sK52,sK53,k3_closure3(sK52,sK53,sK55,X0)),k2_pboole(sK52,k2_closure3(sK52,sK53,sK55),k2_closure3(sK52,sK53,X0)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK52,sK53))) ),
inference(forward_demodulation,[],[f63334,f62918]) ).
fof(f63337,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK52,sK53)))
| r6_pboole(sK52,k2_closure3(sK52,sK53,k3_closure3(sK52,sK53,sK54,X0)),k2_pboole(sK52,k2_closure3(sK52,sK53,sK54),k2_closure3(sK52,sK53,X0))) ),
inference(forward_demodulation,[],[f63335,f62918]) ).
fof(f63347,plain,
r6_pboole(sK52,k2_closure3(sK52,sK53,k3_closure3(sK52,sK53,sK54,k1_setfam_1(k2_tarski(sK54,sK55)))),k2_pboole(sK52,k2_closure3(sK52,sK53,sK54),k2_closure3(sK52,sK53,k1_setfam_1(k2_tarski(sK54,sK55))))),
inference(resolution,[],[f63337,f62936]) ).
fof(f63348,plain,
r6_pboole(sK52,k2_closure3(sK52,sK53,sK54),k2_pboole(sK52,k2_closure3(sK52,sK53,sK54),k2_closure3(sK52,sK53,k1_setfam_1(k2_tarski(sK54,sK55))))),
inference(forward_demodulation,[],[f63347,f63029]) ).
fof(f63369,plain,
! [X0] :
( r2_pboole(sK52,k2_closure3(sK52,sK53,X0),k2_closure3(sK52,sK53,k3_closure3(sK52,sK53,sK55,X0)))
| ~ m1_pboole(k2_closure3(sK52,sK53,X0),sK52)
| ~ m1_pboole(k2_closure3(sK52,sK53,sK55),sK52)
| ~ m1_pboole(k2_closure3(sK52,sK53,k3_closure3(sK52,sK53,sK55,X0)),sK52)
| ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK52,sK53))) ),
inference(resolution,[],[f52129,f63336]) ).
fof(f63373,plain,
! [X0] :
( r2_pboole(sK52,k2_closure3(sK52,sK53,X0),k2_closure3(sK52,sK53,k3_closure3(sK52,sK53,sK55,X0)))
| ~ m1_pboole(k2_closure3(sK52,sK53,sK55),sK52)
| ~ m1_pboole(k2_closure3(sK52,sK53,k3_closure3(sK52,sK53,sK55,X0)),sK52)
| ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK52,sK53))) ),
inference(forward_subsumption_resolution,[],[f63369,f63042]) ).
fof(f63374,plain,
! [X0] :
( r2_pboole(sK52,k2_closure3(sK52,sK53,X0),k2_closure3(sK52,sK53,k3_closure3(sK52,sK53,sK55,X0)))
| ~ m1_pboole(k2_closure3(sK52,sK53,k3_closure3(sK52,sK53,sK55,X0)),sK52)
| ~ m1_subset_1(X0,k1_zfmisc_1(k6_closure2(sK52,sK53))) ),
inference(forward_subsumption_resolution,[],[f63373,f63044]) ).
fof(f63477,plain,
! [X0,X1] : k1_setfam_1(k2_tarski(k4_xboole_0(X1,X0),X1)) = k4_xboole_0(X1,k1_setfam_1(k2_tarski(X0,X1))),
inference(superposition,[],[f62628,f62628]) ).
fof(f63478,plain,
! [X0,X1] : k4_xboole_0(X1,k1_setfam_1(k2_tarski(X0,X1))) = k1_setfam_1(k2_tarski(X1,k4_xboole_0(X1,X0))),
inference(forward_demodulation,[],[f63477,f52326]) ).
fof(f63479,plain,
! [X0,X1] : k4_xboole_0(X1,X0) = k4_xboole_0(X1,k1_setfam_1(k2_tarski(X0,X1))),
inference(forward_demodulation,[],[f63478,f62553]) ).
fof(f65007,plain,
( r2_pboole(sK52,k2_closure3(sK52,sK53,k1_setfam_1(k2_tarski(sK54,sK55))),k2_closure3(sK52,sK53,k2_xboole_0(sK55,k1_setfam_1(k2_tarski(sK54,sK55)))))
| ~ m1_pboole(k2_closure3(sK52,sK53,k2_xboole_0(sK55,k1_setfam_1(k2_tarski(sK54,sK55)))),sK52)
| ~ m1_subset_1(k1_setfam_1(k2_tarski(sK54,sK55)),k1_zfmisc_1(k6_closure2(sK52,sK53))) ),
inference(superposition,[],[f63374,f63027]) ).
fof(f67059,plain,
( r2_pboole(sK52,k2_closure3(sK52,sK53,k1_setfam_1(k2_tarski(sK54,sK55))),k2_closure3(sK52,sK53,sK54))
| ~ m1_pboole(k2_closure3(sK52,sK53,k1_setfam_1(k2_tarski(sK54,sK55))),sK52)
| ~ m1_pboole(k2_closure3(sK52,sK53,sK54),sK52)
| ~ m1_pboole(k2_closure3(sK52,sK53,sK54),sK52) ),
inference(resolution,[],[f63348,f52129]) ).
fof(f67062,plain,
( r2_pboole(sK52,k2_closure3(sK52,sK53,k1_setfam_1(k2_tarski(sK54,sK55))),k2_closure3(sK52,sK53,sK54))
| ~ m1_pboole(k2_closure3(sK52,sK53,k1_setfam_1(k2_tarski(sK54,sK55))),sK52)
| ~ m1_pboole(k2_closure3(sK52,sK53,sK54),sK52) ),
inference(duplicate_literal_removal,[],[f67059]) ).
fof(f67063,plain,
( r2_pboole(sK52,k2_closure3(sK52,sK53,k1_setfam_1(k2_tarski(sK54,sK55))),k2_closure3(sK52,sK53,sK54))
| ~ m1_pboole(k2_closure3(sK52,sK53,sK54),sK52) ),
inference(forward_subsumption_resolution,[],[f67062,f63045]) ).
fof(f67064,plain,
r2_pboole(sK52,k2_closure3(sK52,sK53,k1_setfam_1(k2_tarski(sK54,sK55))),k2_closure3(sK52,sK53,sK54)),
inference(forward_subsumption_resolution,[],[f67063,f63043]) ).
fof(f67768,plain,
! [X0,X1] : k2_xboole_0(k4_xboole_0(X0,X1),k1_setfam_1(k2_tarski(X0,X1))) = k2_xboole_0(k4_xboole_0(X0,X1),X0),
inference(superposition,[],[f52468,f61131]) ).
fof(f67769,plain,
! [X0,X1] : k2_xboole_0(k4_xboole_0(X1,X0),X1) = k2_xboole_0(k4_xboole_0(X1,X0),k1_setfam_1(k2_tarski(X0,X1))),
inference(superposition,[],[f52468,f62628]) ).
fof(f67780,plain,
! [X0,X1] : k2_xboole_0(k4_xboole_0(X1,X0),k1_setfam_1(k2_tarski(X0,X1))) = k2_xboole_0(X1,k4_xboole_0(X1,X0)),
inference(forward_demodulation,[],[f67769,f51242]) ).
fof(f67781,plain,
! [X0,X1] : k2_xboole_0(k4_xboole_0(X0,X1),k1_setfam_1(k2_tarski(X0,X1))) = k2_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(forward_demodulation,[],[f67768,f51242]) ).
fof(f67784,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X1,X1)) = k2_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(forward_demodulation,[],[f67781,f62557]) ).
fof(f67785,plain,
! [X0,X1] : k2_xboole_0(X0,k4_xboole_0(X0,X1)) = X0,
inference(forward_demodulation,[],[f67784,f62862]) ).
fof(f69032,plain,
! [X0,X1] : k2_xboole_0(k1_setfam_1(k2_tarski(X1,X0)),X0) = k2_xboole_0(k1_setfam_1(k2_tarski(X1,X0)),k4_xboole_0(X0,X1)),
inference(superposition,[],[f52468,f63479]) ).
fof(f69100,plain,
! [X0,X1] : k2_xboole_0(k4_xboole_0(X0,X1),k1_setfam_1(k2_tarski(X1,X0))) = k2_xboole_0(k1_setfam_1(k2_tarski(X1,X0)),X0),
inference(forward_demodulation,[],[f69032,f51242]) ).
fof(f69102,plain,
! [X0,X1] : k2_xboole_0(k4_xboole_0(X0,X1),k1_setfam_1(k2_tarski(X1,X0))) = k2_xboole_0(X0,k1_setfam_1(k2_tarski(X1,X0))),
inference(forward_demodulation,[],[f69100,f51242]) ).
fof(f69103,plain,
! [X0,X1] : k2_xboole_0(X0,k4_xboole_0(X0,X1)) = k2_xboole_0(X0,k1_setfam_1(k2_tarski(X1,X0))),
inference(forward_demodulation,[],[f69102,f67780]) ).
fof(f69104,plain,
! [X0,X1] : k2_xboole_0(X0,k1_setfam_1(k2_tarski(X1,X0))) = X0,
inference(forward_demodulation,[],[f69103,f67785]) ).
fof(f70956,plain,
( r2_pboole(sK52,k2_closure3(sK52,sK53,k1_setfam_1(k2_tarski(sK54,sK55))),k2_closure3(sK52,sK53,k2_xboole_0(sK55,k1_setfam_1(k2_tarski(sK54,sK55)))))
| ~ m1_pboole(k2_closure3(sK52,sK53,k2_xboole_0(sK55,k1_setfam_1(k2_tarski(sK54,sK55)))),sK52) ),
inference(forward_subsumption_resolution,[],[f65007,f62936]) ).
fof(f71013,plain,
( r2_pboole(sK52,k2_closure3(sK52,sK53,k1_setfam_1(k2_tarski(sK54,sK55))),k2_closure3(sK52,sK53,sK55))
| ~ m1_pboole(k2_closure3(sK52,sK53,k2_xboole_0(sK55,k1_setfam_1(k2_tarski(sK54,sK55)))),sK52) ),
inference(forward_demodulation,[],[f70956,f69104]) ).
fof(f71021,plain,
( ~ m1_pboole(k2_closure3(sK52,sK53,sK55),sK52)
| r2_pboole(sK52,k2_closure3(sK52,sK53,k1_setfam_1(k2_tarski(sK54,sK55))),k2_closure3(sK52,sK53,sK55)) ),
inference(forward_demodulation,[],[f71013,f69104]) ).
fof(f71031,plain,
r2_pboole(sK52,k2_closure3(sK52,sK53,k1_setfam_1(k2_tarski(sK54,sK55))),k2_closure3(sK52,sK53,sK55)),
inference(forward_subsumption_resolution,[],[f71021,f63044]) ).
fof(f71033,plain,
$false,
inference(unit_resulting_resolution,[],[f52187,f63044,f63043,f63045,f67064,f62907,f71031]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG232+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n003.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 19:57:20 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 Running first-order theorem proving
% 0.09/0.20 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
% 15.79/5.37 % (1932894)Detected formulas, will run a generic FOF schedule.
% 15.79/5.37 % (1932904)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4247509944:s2a=on:i=139:gtg=position_2971 on theBenchmark for (2971ds/139Mi)
% 15.79/5.37 % (1932900)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=2169450994:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2971 on theBenchmark for (2971ds/134677Mi)
% 15.79/5.37 % (1932899)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=4270344316:i=141193_2971 on theBenchmark for (2971ds/141193Mi)
% 15.79/5.37 % (1932902)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=304786629:i=109:sd=1:ins=1:gsp=on:ss=axioms_2971 on theBenchmark for (2971ds/109Mi)
% 15.79/5.37 % (1932901)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=241721499:i=141695:sd=1:nm=32:gsp=on:ss=included_2971 on theBenchmark for (2971ds/141695Mi)
% 15.79/5.37 % (1932903)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2022984559:i=119:av=off:ss=axioms_2971 on theBenchmark for (2971ds/119Mi)
% 15.79/5.37 % (1932904)Instruction limit reached!
% 15.79/5.37 % (1932904)------------------------------
% 15.79/5.37 % (1932904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.79/5.37 % (1932904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.79/5.37 % (1932904)CaDiCaL version: 2.1.3
% 15.79/5.37 % (1932904)Termination reason: Instruction limit
% 15.79/5.37 % (1932904)Termination phase: Property scanning
% 15.79/5.37 % (1932904)Time elapsed: 0.035 s
% 15.79/5.37 % (1932904)Peak memory usage: 149 MB
% 15.79/5.37 % (1932904)Instructions burned: 140 (million)
% 15.79/5.37 % (1932905)dis-21_1_sil=8000:lcm=predicate:random_seed=243399433:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2971 on theBenchmark for (2971ds/129Mi)
% 15.79/5.37 % (1932902)Instruction limit reached!
% 15.79/5.37 % (1932902)------------------------------
% 15.79/5.37 % (1932902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.79/5.37 % (1932902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.79/5.37 % (1932902)CaDiCaL version: 2.1.3
% 15.79/5.37 % (1932902)Termination reason: Instruction limit
% 15.79/5.37 % (1932902)Termination phase: SInE selection
% 15.79/5.37 % (1932902)Time elapsed: 0.084 s
% 15.79/5.37 % (1932902)Peak memory usage: 148 MB
% 15.79/5.37 % (1932902)Instructions burned: 109 (million)
% 15.79/5.37 % (1932903)Instruction limit reached!
% 15.79/5.37 % (1932903)------------------------------
% 15.79/5.37 % (1932903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.79/5.37 % (1932903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.79/5.37 % (1932903)CaDiCaL version: 2.1.3
% 15.79/5.37 % (1932903)Termination reason: Instruction limit
% 15.79/5.37 % (1932903)Termination phase: SInE selection
% 15.79/5.37 % (1932903)Time elapsed: 0.092 s
% 15.79/5.37 % (1932903)Peak memory usage: 148 MB
% 15.79/5.37 % (1932903)Instructions burned: 119 (million)
% 15.79/5.37 % (1932905)Instruction limit reached!
% 15.79/5.37 % (1932905)------------------------------
% 15.79/5.37 % (1932905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.79/5.37 % (1932905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.79/5.37 % (1932905)CaDiCaL version: 2.1.3
% 15.79/5.37 % (1932905)Termination reason: Instruction limit
% 15.79/5.37 % (1932905)Termination phase: SInE selection
% 15.79/5.37 % (1932905)Time elapsed: 0.098 s
% 15.79/5.37 % (1932905)Peak memory usage: 149 MB
% 15.79/5.37 % (1932905)Instructions burned: 129 (million)
% 15.79/5.37 % (1932913)lrs+10_1_sil=8000:sp=occurrence:random_seed=1711785392:i=285:sd=3:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/285Mi)
% 15.79/5.37 % (1932913)Instruction limit reached!
% 15.79/5.37 % (1932913)------------------------------
% 15.79/5.37 % (1932913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.79/5.37 % (1932913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.79/5.37 % (1932913)CaDiCaL version: 2.1.3
% 15.79/5.37 % (1932913)Termination reason: Instruction limit
% 15.79/5.37 % (1932913)Termination phase: SInE selection
% 15.79/5.37 % (1932913)Time elapsed: 0.117 s
% 15.79/5.37 % (1932913)Peak memory usage: 149 MB
% 15.79/5.37 % (1932913)Instructions burned: 285 (million)
% 24.96/6.61 % (1932914)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2105518013:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/157Mi)
% 24.96/6.61 % (1932915)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4052704897:i=325:sd=1:ss=axioms:sgt=32_2968 on theBenchmark for (2968ds/325Mi)
% 24.96/6.61 % (1932916)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=4061264832:s2a=on:i=248:s2at=1.23:gtg=position_2968 on theBenchmark for (2968ds/248Mi)
% 24.96/6.61 % (1932914)Instruction limit reached!
% 24.96/6.61 % (1932914)------------------------------
% 24.96/6.61 % (1932914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/6.61 % (1932914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/6.61 % (1932914)CaDiCaL version: 2.1.3
% 24.96/6.61 % (1932914)Termination reason: Instruction limit
% 24.96/6.61 % (1932914)Termination phase: Property scanning
% 24.96/6.61 % (1932914)Time elapsed: 0.072 s
% 24.96/6.61 % (1932914)Peak memory usage: 149 MB
% 24.96/6.61 % (1932914)Instructions burned: 157 (million)
% 24.96/6.61 % (1932920)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2963307924:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2967 on theBenchmark for (2967ds/294Mi)
% 24.96/6.61 % (1932916)Instruction limit reached!
% 24.96/6.61 % (1932916)------------------------------
% 24.96/6.61 % (1932916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/6.61 % (1932916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/6.61 % (1932916)CaDiCaL version: 2.1.3
% 24.96/6.61 % (1932916)Termination reason: Instruction limit
% 24.96/6.61 % (1932916)Termination phase: Property scanning
% 24.96/6.61 % (1932916)Time elapsed: 0.114 s
% 24.96/6.61 % (1932916)Peak memory usage: 149 MB
% 24.96/6.61 % (1932916)Instructions burned: 249 (million)
% 24.96/6.61 % (1932920)Instruction limit reached!
% 24.96/6.61 % (1932920)------------------------------
% 24.96/6.61 % (1932920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/6.61 % (1932920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/6.61 % (1932920)CaDiCaL version: 2.1.3
% 24.96/6.61 % (1932920)Termination reason: Instruction limit
% 24.96/6.61 % (1932920)Termination phase: SInE selection
% 24.96/6.61 % (1932920)Time elapsed: 0.107 s
% 24.96/6.61 % (1932920)Peak memory usage: 149 MB
% 24.96/6.61 % (1932920)Instructions burned: 295 (million)
% 24.96/6.61 % (1932922)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2171751154:i=2350_2966 on theBenchmark for (2966ds/2350Mi)
% 24.96/6.61 % (1932915)Instruction limit reached!
% 24.96/6.61 % (1932915)------------------------------
% 24.96/6.61 % (1932915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/6.61 % (1932915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/6.61 % (1932915)CaDiCaL version: 2.1.3
% 24.96/6.61 % (1932915)Termination reason: Instruction limit
% 24.96/6.61 % (1932915)Termination phase: Saturation
% 24.96/6.61 % (1932915)Time elapsed: 0.267 s
% 24.96/6.61 % (1932915)Peak memory usage: 155 MB
% 24.96/6.61 % (1932915)Instructions burned: 325 (million)
% 24.96/6.61 % (1932924)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3771380790:cts=off:i=113:fsr=off:ss=included:sgt=4_2965 on theBenchmark for (2965ds/113Mi)
% 24.96/6.61 % (1932925)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2934901299:i=127:av=off:fsr=off:sup=off_2964 on theBenchmark for (2964ds/127Mi)
% 24.96/6.61 % (1932924)Instruction limit reached!
% 24.96/6.61 % (1932924)------------------------------
% 24.96/6.61 % (1932924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/6.61 % (1932924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/6.61 % (1932924)CaDiCaL version: 2.1.3
% 24.96/6.61 % (1932924)Termination reason: Instruction limit
% 24.96/6.61 % (1932924)Termination phase: SInE selection
% 24.96/6.61 % (1932924)Time elapsed: 0.092 s
% 24.96/6.61 % (1932924)Peak memory usage: 149 MB
% 24.96/6.61 % (1932924)Instructions burned: 113 (million)
% 24.96/6.61 % (1932925)Instruction limit reached!
% 24.96/6.61 % (1932925)------------------------------
% 24.96/6.61 % (1932925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.96/6.61 % (1932925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.96/6.61 % (1932925)CaDiCaL version: 2.1.3
% 29.50/7.29 % (1932925)Termination reason: Instruction limit
% 29.50/7.29 % (1932925)Termination phase: Preprocessing 1
% 29.50/7.29 % (1932925)Time elapsed: 0.056 s
% 29.50/7.29 % (1932925)Peak memory usage: 150 MB
% 29.50/7.29 % (1932925)Instructions burned: 129 (million)
% 29.50/7.29 % (1932927)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4057145481:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2964 on theBenchmark for (2964ds/114Mi)
% 29.50/7.29 % (1932927)Instruction limit reached!
% 29.50/7.29 % (1932927)------------------------------
% 29.50/7.29 % (1932927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.50/7.29 % (1932927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.50/7.29 % (1932927)CaDiCaL version: 2.1.3
% 29.50/7.29 % (1932927)Termination reason: Instruction limit
% 29.50/7.29 % (1932927)Termination phase: Property scanning
% 29.50/7.29 % (1932927)Time elapsed: 0.054 s
% 29.50/7.29 % (1932927)Peak memory usage: 149 MB
% 29.50/7.29 % (1932927)Instructions burned: 114 (million)
% 29.50/7.29 % (1932931)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1736173806:i=437:sd=1:aac=none:ss=included_2963 on theBenchmark for (2963ds/437Mi)
% 29.50/7.29 % (1932930)lrs+10_1_sil=8000:sp=occurrence:random_seed=2638299835:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2963 on theBenchmark for (2963ds/907Mi)
% 29.50/7.29 % (1932933)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2578338968:i=5202:ss=axioms:sgt=16_2962 on theBenchmark for (2962ds/5202Mi)
% 29.50/7.29 % (1932931)Instruction limit reached!
% 29.50/7.29 % (1932931)------------------------------
% 29.50/7.29 % (1932931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.50/7.29 % (1932931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.50/7.29 % (1932931)CaDiCaL version: 2.1.3
% 29.50/7.29 % (1932931)Termination reason: Instruction limit
% 29.50/7.29 % (1932931)Termination phase: Saturation
% 29.50/7.29 % (1932931)Time elapsed: 0.186 s
% 29.50/7.29 % (1932931)Peak memory usage: 156 MB
% 29.50/7.29 % (1932931)Instructions burned: 439 (million)
% 29.50/7.29 % (1932937)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2549288557:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2960 on theBenchmark for (2960ds/134Mi)
% 29.50/7.29 % (1932937)Instruction limit reached!
% 29.50/7.29 % (1932937)------------------------------
% 29.50/7.29 % (1932937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.50/7.29 % (1932937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.50/7.29 % (1932937)CaDiCaL version: 2.1.3
% 29.50/7.29 % (1932937)Termination reason: Instruction limit
% 29.50/7.29 % (1932937)Termination phase: SInE selection
% 29.50/7.29 % (1932937)Time elapsed: 0.059 s
% 29.50/7.29 % (1932937)Peak memory usage: 149 MB
% 29.50/7.29 % (1932937)Instructions burned: 134 (million)
% 29.50/7.29 % (1932939)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2976481896:st=8:i=592:sd=3:ep=RST:ss=axioms_2958 on theBenchmark for (2958ds/592Mi)
% 29.50/7.29 % (1932930)Instruction limit reached!
% 29.50/7.29 % (1932930)------------------------------
% 29.50/7.29 % (1932930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.50/7.29 % (1932930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.50/7.29 % (1932930)CaDiCaL version: 2.1.3
% 29.50/7.29 % (1932930)Termination reason: Instruction limit
% 29.50/7.29 % (1932930)Termination phase: Property scanning
% 29.50/7.29 % (1932930)Time elapsed: 0.592 s
% 29.50/7.29 % (1932930)Peak memory usage: 164 MB
% 29.50/7.29 % (1932930)Instructions burned: 909 (million)
% 29.50/7.29 % (1932939)Instruction limit reached!
% 29.50/7.29 % (1932939)------------------------------
% 29.50/7.29 % (1932939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.50/7.29 % (1932939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.50/7.29 % (1932939)CaDiCaL version: 2.1.3
% 29.50/7.29 % (1932939)Termination reason: Instruction limit
% 29.50/7.29 % (1932939)Termination phase: Preprocessing 1
% 29.50/7.29 % (1932939)Time elapsed: 0.254 s
% 29.50/7.29 % (1932939)Peak memory usage: 152 MB
% 29.50/7.29 % (1932939)Instructions burned: 594 (million)
% 29.50/7.29 % (1932941)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1704287322:st=3:i=13193:sd=3:ss=axioms_2955 on theBenchmark for (2955ds/13193Mi)
% 29.50/7.29 % (1932942)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=1949700822:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2954 on theBenchmark for (2954ds/125Mi)
% 29.50/7.29 % (1932942)Instruction limit reached!
% 29.50/7.29 % (1932942)------------------------------
% 29.50/7.29 % (1932942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.50/7.29 % (1932942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.50/7.29 % (1932942)CaDiCaL version: 2.1.3
% 29.50/7.29 % (1932942)Termination reason: Instruction limit
% 29.50/7.29 % (1932942)Termination phase: Property scanning
% 29.50/7.29 % (1932942)Time elapsed: 0.030 s
% 29.50/7.29 % (1932942)Peak memory usage: 149 MB
% 29.50/7.29 % (1932942)Instructions burned: 125 (million)
% 29.50/7.29 % (1932945)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3739955778:i=134:gtgl=5:slsql=off:gtg=exists_sym_2952 on theBenchmark for (2952ds/134Mi)
% 29.50/7.29 % (1932945)Instruction limit reached!
% 29.50/7.29 % (1932945)------------------------------
% 29.50/7.29 % (1932945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.50/7.29 % (1932945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.50/7.29 % (1932945)CaDiCaL version: 2.1.3
% 29.50/7.29 % (1932945)Termination reason: Instruction limit
% 29.50/7.29 % (1932945)Termination phase: Property scanning
% 29.50/7.29 % (1932945)Time elapsed: 0.061 s
% 29.50/7.29 % (1932945)Peak memory usage: 149 MB
% 29.50/7.29 % (1932945)Instructions burned: 135 (million)
% 29.50/7.29 % (1932922)Instruction limit reached!
% 29.50/7.29 % (1932922)------------------------------
% 29.50/7.29 % (1932922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.50/7.29 % (1932922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.50/7.29 % (1932922)CaDiCaL version: 2.1.3
% 29.50/7.29 % (1932922)Termination reason: Instruction limit
% 29.50/7.29 % (1932922)Termination phase: Preprocessing 3
% 29.50/7.29 % (1932922)Time elapsed: 1.621 s
% 29.50/7.29 % (1932922)Peak memory usage: 249 MB
% 29.50/7.29 % (1932922)Instructions burned: 2351 (million)
% 29.50/7.29 % (1932947)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3831971675:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2949 on theBenchmark for (2949ds/141Mi)
% 29.50/7.29 % (1932947)Instruction limit reached!
% 29.50/7.29 % (1932947)------------------------------
% 29.50/7.29 % (1932947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.50/7.29 % (1932947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.50/7.29 % (1932947)CaDiCaL version: 2.1.3
% 29.50/7.29 % (1932947)Termination reason: Instruction limit
% 29.50/7.29 % (1932947)Termination phase: SInE selection
% 29.50/7.29 % (1932947)Time elapsed: 0.108 s
% 29.50/7.29 % (1932947)Peak memory usage: 149 MB
% 29.50/7.29 % (1932947)Instructions burned: 142 (million)
% 29.50/7.29 % (1932948)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3453582457:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2948 on theBenchmark for (2948ds/431Mi)
% 29.50/7.29 % (1932950)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=1570529653:i=6060:aac=none:ins=25_2946 on theBenchmark for (2946ds/6060Mi)
% 29.50/7.29 % (1932948)Instruction limit reached!
% 29.50/7.29 % (1932948)------------------------------
% 29.50/7.29 % (1932948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.50/7.29 % (1932948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.50/7.29 % (1932948)CaDiCaL version: 2.1.3
% 29.50/7.29 % (1932948)Termination reason: Instruction limit
% 29.50/7.29 % (1932948)Termination phase: Saturation
% 29.50/7.29 % (1932948)Time elapsed: 0.319 s
% 29.50/7.29 % (1932948)Peak memory usage: 155 MB
% 29.50/7.29 % (1932948)Instructions burned: 433 (million)
% 29.50/7.29 % (1932953)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=2822738024:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2943 on theBenchmark for (2943ds/150Mi)
% 29.50/7.29 % (1932953)Instruction limit reached!
% 29.50/7.29 % (1932953)------------------------------
% 29.50/7.29 % (1932953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.50/7.29 % (1932953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.50/7.29 % (1932953)CaDiCaL version: 2.1.3
% 29.50/7.29 % (1932953)Termination reason: Instruction limit
% 29.50/7.29 % (1932953)Termination phase: SInE selection
% 29.50/7.29 % (1932953)Time elapsed: 0.117 s
% 29.50/7.29 % (1932953)Peak memory usage: 149 MB
% 29.50/7.29 % (1932953)Instructions burned: 150 (million)
% 29.50/7.29 % (1932955)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4073690852:i=14155:bd=all_2940 on theBenchmark for (2940ds/14155Mi)
% 29.50/7.29 % (1932900)First to succeed.
% 29.50/7.29 % (1932900)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1932894"
% 29.50/7.29 % (1932900)Refutation found. Thanks to Tanya!
% 29.50/7.29 % SZS status Theorem for theBenchmark
% 29.50/7.29 % SZS output start Proof for theBenchmark
% See solution above
% 30.28/7.52 % (1932900)------------------------------
% 30.28/7.52 % (1932900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.28/7.52 % (1932900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.28/7.52 % (1932900)CaDiCaL version: 2.1.3
% 30.28/7.52 % (1932900)Termination reason: Refutation
% 30.28/7.52 % (1932900)Time elapsed: 3.418 s
% 30.28/7.52 % (1932900)Peak memory usage: 314 MB
% 30.28/7.52 % (1932900)Instructions burned: 7497 (million)
% 30.28/7.52 % (1932900)------------------------------
% 30.28/7.52 % (1932900)------------------------------
% 30.28/7.52 % (1932894)Success in time 6.645 s
% 30.28/7.52 % Vampire exiting
%------------------------------------------------------------------------------