%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG230+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:29 AM UTC 2026
% Result : Theorem 52.70s 8.12s
% Output : Refutation 53.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 29
% Syntax : Number of formulae : 331 ( 39 unt; 14 def)
% Number of atoms : 1552 ( 154 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 2274 (1053 ~;1091 |; 82 &)
% ( 19 <=>; 28 =>; 0 <=; 1 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 8 prp; 0-4 aty)
% Number of functors : 30 ( 30 usr; 11 con; 0-5 aty)
% Number of variables : 742 ( 0 sgn 715 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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)))
=> 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/sandbox2/benchmark/theBenchmark.p',t11_closure3) ).
fof(f2,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)))
=> 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(negated_conjecture,[status(cth)],[f1]) ).
fof(f22,axiom,
! [X0,X1,X2] :
( X2 = k2_xboole_0(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ( r2_hidden(X3,X0)
| r2_hidden(X3,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_xboole_0) ).
fof(f23,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
=> ! [X3] :
( m4_pboole(X3,X0,X1)
=> ( X3 = k2_closure3(X0,X1,X2)
<=> ! [X4] :
( r2_hidden(X4,X0)
=> k1_funct_1(X3,X4) = k3_tarski(a_4_0_closure3(X0,X1,X2,X4)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_closure3) ).
fof(f24,axiom,
! [X0,X1] :
( X1 = k3_tarski(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> ? [X3] :
( r2_hidden(X2,X3)
& r2_hidden(X3,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_tarski) ).
fof(f25,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_pboole(X2,X0)
=> ! [X3] :
( m1_pboole(X3,X0)
=> ( X3 = k2_pboole(X0,X1,X2)
<=> ! [X4] :
( r2_hidden(X4,X0)
=> k1_funct_1(X3,X4) = k2_xboole_0(k1_funct_1(X1,X4),k1_funct_1(X2,X4)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d7_pboole) ).
fof(f30,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/sandbox2/benchmark/theBenchmark.p',dt_k2_closure3) ).
fof(f31,axiom,
! [X0,X1,X2] :
( ( m1_pboole(X1,X0)
& m1_pboole(X2,X0) )
=> m1_pboole(k2_pboole(X0,X1,X2),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_pboole) ).
fof(f33,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(k3_closure3(X0,X1,X2,X3),k1_zfmisc_1(k1_closure2(X0,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_closure3) ).
fof(f40,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m4_pboole(X2,X0,X1)
=> m1_pboole(X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m4_pboole) ).
fof(f55,axiom,
! [X0,X1,X2,X3,X4] :
( ( m1_pboole(X2,X1)
& m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2))) )
=> ( r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4))
<=> ? [X5] :
( m1_closure2(X5,X1,X2,k6_closure2(X1,X2))
& X0 = k1_funct_1(X5,X4)
& r2_hidden(X5,X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fraenkel_a_4_0_closure3) ).
fof(f82,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/sandbox2/benchmark/theBenchmark.p',redefinition_k3_closure3) ).
fof(f83,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> k6_closure2(X0,X1) = k1_closure2(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_closure2) ).
fof(f88,axiom,
! [X0,X1,X2] :
( ( m1_pboole(X1,X0)
& m1_pboole(X2,X0) )
=> r6_pboole(X0,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r6_pboole) ).
fof(f93,axiom,
! [X0,X1] :
( ! [X2] :
( r2_hidden(X2,X0)
<=> r2_hidden(X2,X1) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_tarski) ).
fof(f94,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_pboole(X2,X0)
=> ( ! [X3] :
( r2_hidden(X3,X0)
=> k1_funct_1(X1,X3) = k1_funct_1(X2,X3) )
=> X1 = X2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_pboole) ).
fof(f129,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,[],[f2]) ).
fof(f156,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k2_closure3(X0,X1,X2)
<=> ! [X4] :
( k1_funct_1(X3,X4) = k3_tarski(a_4_0_closure3(X0,X1,X2,X4))
| ~ r2_hidden(X4,X0) ) )
| ~ m4_pboole(X3,X0,X1) )
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f157,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k2_pboole(X0,X1,X2)
<=> ! [X4] :
( k1_funct_1(X3,X4) = k2_xboole_0(k1_funct_1(X1,X4),k1_funct_1(X2,X4))
| ~ r2_hidden(X4,X0) ) )
| ~ m1_pboole(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f158,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,[],[f30]) ).
fof(f159,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,[],[f158]) ).
fof(f160,plain,
! [X0,X1,X2] :
( m1_pboole(k2_pboole(X0,X1,X2),X0)
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(ennf_transformation,[],[f31]) ).
fof(f161,plain,
! [X0,X1,X2] :
( m1_pboole(k2_pboole(X0,X1,X2),X0)
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(flattening,[],[f160]) ).
fof(f162,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k3_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,[],[f33]) ).
fof(f163,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k3_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,[],[f162]) ).
fof(f170,plain,
! [X0,X1] :
( ! [X2] :
( m1_pboole(X2,X0)
| ~ m4_pboole(X2,X0,X1) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f40]) ).
fof(f187,plain,
! [X0,X1,X2,X3,X4] :
( ( r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4))
<=> ? [X5] :
( m1_closure2(X5,X1,X2,k6_closure2(X1,X2))
& X0 = k1_funct_1(X5,X4)
& r2_hidden(X5,X3) ) )
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(ennf_transformation,[],[f55]) ).
fof(f188,plain,
! [X0,X1,X2,X3,X4] :
( ( r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4))
<=> ? [X5] :
( m1_closure2(X5,X1,X2,k6_closure2(X1,X2))
& X0 = k1_funct_1(X5,X4)
& r2_hidden(X5,X3) ) )
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(flattening,[],[f187]) ).
fof(f206,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,[],[f82]) ).
fof(f207,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,[],[f206]) ).
fof(f208,plain,
! [X0,X1] :
( k6_closure2(X0,X1) = k1_closure2(X0,X1)
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f83]) ).
fof(f215,plain,
! [X0,X1,X2] :
( r6_pboole(X0,X1,X1)
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(ennf_transformation,[],[f88]) ).
fof(f216,plain,
! [X0,X1,X2] :
( r6_pboole(X0,X1,X1)
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(flattening,[],[f215]) ).
fof(f222,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( r2_hidden(X2,X0)
<~> r2_hidden(X2,X1) ) ),
inference(ennf_transformation,[],[f93]) ).
fof(f223,plain,
! [X0,X1] :
( ! [X2] :
( X1 = X2
| ? [X3] :
( k1_funct_1(X1,X3) != k1_funct_1(X2,X3)
& r2_hidden(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f94]) ).
fof(f224,plain,
! [X0,X1] :
( ! [X2] :
( X1 = X2
| ? [X3] :
( k1_funct_1(X1,X3) != k1_funct_1(X2,X3)
& r2_hidden(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(flattening,[],[f223]) ).
fof(f232,plain,
( ~ r6_pboole(sK0,k2_closure3(sK0,sK1,k3_closure3(sK0,sK1,sK2,sK3)),k2_pboole(sK0,k2_closure3(sK0,sK1,sK2),k2_closure3(sK0,sK1,sK3)))
& m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
& m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
& m1_pboole(sK1,sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f129]) ).
fof(f233,plain,
! [X0,X1,X2] :
( ( X2 = k2_xboole_0(X0,X1)
| ? [X3] :
( ( ( ~ r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) )
& ( r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ( ~ r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) ) )
& ( r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) ) )
| k2_xboole_0(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f22]) ).
fof(f234,plain,
! [X0,X1,X2] :
( ( X2 = k2_xboole_0(X0,X1)
| ? [X3] :
( ( ( ~ r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) )
& ( r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ( ~ r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) ) )
& ( r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) ) )
| k2_xboole_0(X0,X1) != X2 ) ),
inference(flattening,[],[f233]) ).
fof(f235,plain,
! [X0,X1,X2] :
( ( X2 = k2_xboole_0(X0,X1)
| ? [X3] :
( ( ( ~ r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) )
& ( r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| r2_hidden(X3,X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ( ~ r2_hidden(X4,X0)
& ~ r2_hidden(X4,X1) ) )
& ( r2_hidden(X4,X0)
| r2_hidden(X4,X1)
| ~ r2_hidden(X4,X2) ) )
| k2_xboole_0(X0,X1) != X2 ) ),
inference(rectify,[],[f234]) ).
fof(f236,plain,
! [X0,X1,X2] :
( ( X2 = k2_xboole_0(X0,X1)
| ( ( ( ~ r2_hidden(sK4(X0,X1,X2),X0)
& ~ r2_hidden(sK4(X0,X1,X2),X1) )
| ~ r2_hidden(sK4(X0,X1,X2),X2) )
& ( r2_hidden(sK4(X0,X1,X2),X0)
| r2_hidden(sK4(X0,X1,X2),X1)
| r2_hidden(sK4(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ( ~ r2_hidden(X4,X0)
& ~ r2_hidden(X4,X1) ) )
& ( r2_hidden(X4,X0)
| r2_hidden(X4,X1)
| ~ r2_hidden(X4,X2) ) )
| k2_xboole_0(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X3,sK4(X0,X1,X2))],[f235]) ).
fof(f237,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k2_closure3(X0,X1,X2)
| ? [X4] :
( k1_funct_1(X3,X4) != k3_tarski(a_4_0_closure3(X0,X1,X2,X4))
& r2_hidden(X4,X0) ) )
& ( ! [X4] :
( k1_funct_1(X3,X4) = k3_tarski(a_4_0_closure3(X0,X1,X2,X4))
| ~ r2_hidden(X4,X0) )
| k2_closure3(X0,X1,X2) != X3 ) )
| ~ m4_pboole(X3,X0,X1) )
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) )
| ~ m1_pboole(X1,X0) ),
inference(nnf_transformation,[],[f156]) ).
fof(f238,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k2_closure3(X0,X1,X2)
| ? [X4] :
( k1_funct_1(X3,X4) != k3_tarski(a_4_0_closure3(X0,X1,X2,X4))
& r2_hidden(X4,X0) ) )
& ( ! [X5] :
( k1_funct_1(X3,X5) = k3_tarski(a_4_0_closure3(X0,X1,X2,X5))
| ~ r2_hidden(X5,X0) )
| k2_closure3(X0,X1,X2) != X3 ) )
| ~ m4_pboole(X3,X0,X1) )
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) )
| ~ m1_pboole(X1,X0) ),
inference(rectify,[],[f237]) ).
fof(f239,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k2_closure3(X0,X1,X2)
| ( k1_funct_1(X3,sK5(X0,X1,X2,X3)) != k3_tarski(a_4_0_closure3(X0,X1,X2,sK5(X0,X1,X2,X3)))
& r2_hidden(sK5(X0,X1,X2,X3),X0) ) )
& ( ! [X5] :
( k1_funct_1(X3,X5) = k3_tarski(a_4_0_closure3(X0,X1,X2,X5))
| ~ r2_hidden(X5,X0) )
| k2_closure3(X0,X1,X2) != X3 ) )
| ~ m4_pboole(X3,X0,X1) )
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1))) )
| ~ m1_pboole(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X4,sK5(X0,X1,X2,X3))],[f238]) ).
fof(f240,plain,
! [X0,X1] :
( ( X1 = k3_tarski(X0)
| ? [X2] :
( ( ! [X3] :
( ~ r2_hidden(X2,X3)
| ~ r2_hidden(X3,X0) )
| ~ r2_hidden(X2,X1) )
& ( ? [X3] :
( r2_hidden(X2,X3)
& r2_hidden(X3,X0) )
| r2_hidden(X2,X1) ) ) )
& ( ! [X2] :
( ( r2_hidden(X2,X1)
| ! [X3] :
( ~ r2_hidden(X2,X3)
| ~ r2_hidden(X3,X0) ) )
& ( ? [X3] :
( r2_hidden(X2,X3)
& r2_hidden(X3,X0) )
| ~ r2_hidden(X2,X1) ) )
| k3_tarski(X0) != X1 ) ),
inference(nnf_transformation,[],[f24]) ).
fof(f241,plain,
! [X0,X1] :
( ( X1 = k3_tarski(X0)
| ? [X2] :
( ( ! [X3] :
( ~ r2_hidden(X2,X3)
| ~ r2_hidden(X3,X0) )
| ~ r2_hidden(X2,X1) )
& ( ? [X4] :
( r2_hidden(X2,X4)
& r2_hidden(X4,X0) )
| r2_hidden(X2,X1) ) ) )
& ( ! [X5] :
( ( r2_hidden(X5,X1)
| ! [X6] :
( ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0) ) )
& ( ? [X7] :
( r2_hidden(X5,X7)
& r2_hidden(X7,X0) )
| ~ r2_hidden(X5,X1) ) )
| k3_tarski(X0) != X1 ) ),
inference(rectify,[],[f240]) ).
fof(f242,plain,
! [X0,X1] :
( ( X1 = k3_tarski(X0)
| ( ( ! [X3] :
( ~ r2_hidden(sK6(X0,X1),X3)
| ~ r2_hidden(X3,X0) )
| ~ r2_hidden(sK6(X0,X1),X1) )
& ( ( r2_hidden(sK6(X0,X1),sK7(X0,X1))
& r2_hidden(sK7(X0,X1),X0) )
| r2_hidden(sK6(X0,X1),X1) ) ) )
& ( ! [X5] :
( ( r2_hidden(X5,X1)
| ! [X6] :
( ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0) ) )
& ( ( r2_hidden(X5,sK8(X0,X5))
& r2_hidden(sK8(X0,X5),X0) )
| ~ r2_hidden(X5,X1) ) )
| k3_tarski(X0) != X1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8]),skolemize(X2,sK6(X0,X1)),skolemize(X4,sK7(X0,X1)),skolemize(X7,sK8(X0,X5))],[f241]) ).
fof(f243,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k2_pboole(X0,X1,X2)
| ? [X4] :
( k1_funct_1(X3,X4) != k2_xboole_0(k1_funct_1(X1,X4),k1_funct_1(X2,X4))
& r2_hidden(X4,X0) ) )
& ( ! [X4] :
( k1_funct_1(X3,X4) = k2_xboole_0(k1_funct_1(X1,X4),k1_funct_1(X2,X4))
| ~ r2_hidden(X4,X0) )
| k2_pboole(X0,X1,X2) != X3 ) )
| ~ m1_pboole(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(nnf_transformation,[],[f157]) ).
fof(f244,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k2_pboole(X0,X1,X2)
| ? [X4] :
( k1_funct_1(X3,X4) != k2_xboole_0(k1_funct_1(X1,X4),k1_funct_1(X2,X4))
& r2_hidden(X4,X0) ) )
& ( ! [X5] :
( k1_funct_1(X3,X5) = k2_xboole_0(k1_funct_1(X1,X5),k1_funct_1(X2,X5))
| ~ r2_hidden(X5,X0) )
| k2_pboole(X0,X1,X2) != X3 ) )
| ~ m1_pboole(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(rectify,[],[f243]) ).
fof(f245,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k2_pboole(X0,X1,X2)
| ( k1_funct_1(X3,sK9(X0,X1,X2,X3)) != k2_xboole_0(k1_funct_1(X1,sK9(X0,X1,X2,X3)),k1_funct_1(X2,sK9(X0,X1,X2,X3)))
& r2_hidden(sK9(X0,X1,X2,X3),X0) ) )
& ( ! [X5] :
( k1_funct_1(X3,X5) = k2_xboole_0(k1_funct_1(X1,X5),k1_funct_1(X2,X5))
| ~ r2_hidden(X5,X0) )
| k2_pboole(X0,X1,X2) != X3 ) )
| ~ m1_pboole(X3,X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X4,sK9(X0,X1,X2,X3))],[f244]) ).
fof(f251,plain,
! [X0,X1,X2,X3,X4] :
( ( ( r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4))
| ! [X5] :
( ~ m1_closure2(X5,X1,X2,k6_closure2(X1,X2))
| k1_funct_1(X5,X4) != X0
| ~ r2_hidden(X5,X3) ) )
& ( ? [X5] :
( m1_closure2(X5,X1,X2,k6_closure2(X1,X2))
& X0 = k1_funct_1(X5,X4)
& r2_hidden(X5,X3) )
| ~ r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4)) ) )
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(nnf_transformation,[],[f188]) ).
fof(f252,plain,
! [X0,X1,X2,X3,X4] :
( ( ( r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4))
| ! [X5] :
( ~ m1_closure2(X5,X1,X2,k6_closure2(X1,X2))
| k1_funct_1(X5,X4) != X0
| ~ r2_hidden(X5,X3) ) )
& ( ? [X6] :
( m1_closure2(X6,X1,X2,k6_closure2(X1,X2))
& k1_funct_1(X6,X4) = X0
& r2_hidden(X6,X3) )
| ~ r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4)) ) )
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(rectify,[],[f251]) ).
fof(f253,plain,
! [X0,X1,X2,X3,X4] :
( ( ( r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4))
| ! [X5] :
( ~ m1_closure2(X5,X1,X2,k6_closure2(X1,X2))
| k1_funct_1(X5,X4) != X0
| ~ r2_hidden(X5,X3) ) )
& ( ( m1_closure2(sK15(X0,X1,X2,X3,X4),X1,X2,k6_closure2(X1,X2))
& k1_funct_1(sK15(X0,X1,X2,X3,X4),X4) = X0
& r2_hidden(sK15(X0,X1,X2,X3,X4),X3) )
| ~ r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4)) ) )
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X6,sK15(X0,X1,X2,X3,X4))],[f252]) ).
fof(f284,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( ( ~ r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) )
& ( r2_hidden(X2,X1)
| r2_hidden(X2,X0) ) ) ),
inference(nnf_transformation,[],[f222]) ).
fof(f285,plain,
! [X0,X1] :
( X0 = X1
| ( ( ~ r2_hidden(sK39(X0,X1),X1)
| ~ r2_hidden(sK39(X0,X1),X0) )
& ( r2_hidden(sK39(X0,X1),X1)
| r2_hidden(sK39(X0,X1),X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39]),skolemize(X2,sK39(X0,X1))],[f284]) ).
fof(f286,plain,
! [X0,X1] :
( ! [X2] :
( X1 = X2
| ( k1_funct_1(X1,sK40(X0,X1,X2)) != k1_funct_1(X2,sK40(X0,X1,X2))
& r2_hidden(sK40(X0,X1,X2),X0) )
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40]),skolemize(X3,sK40(X0,X1,X2))],[f224]) ).
fof(f287,plain,
m1_pboole(sK1,sK0),
inference(cnf_transformation,[],[f232]) ).
fof(f288,plain,
m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1))),
inference(cnf_transformation,[],[f232]) ).
fof(f289,plain,
m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))),
inference(cnf_transformation,[],[f232]) ).
fof(f290,plain,
~ r6_pboole(sK0,k2_closure3(sK0,sK1,k3_closure3(sK0,sK1,sK2,sK3)),k2_pboole(sK0,k2_closure3(sK0,sK1,sK2),k2_closure3(sK0,sK1,sK3))),
inference(cnf_transformation,[],[f232]) ).
fof(f308,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X0)
| r2_hidden(X4,X1)
| ~ r2_hidden(X4,X2)
| k2_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f236]) ).
fof(f309,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X1)
| k2_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f236]) ).
fof(f310,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| k2_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f236]) ).
fof(f314,plain,
! [X2,X3,X0,X1,X5] :
( k1_funct_1(X3,X5) = k3_tarski(a_4_0_closure3(X0,X1,X2,X5))
| ~ r2_hidden(X5,X0)
| k2_closure3(X0,X1,X2) != X3
| ~ m4_pboole(X3,X0,X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f239]) ).
fof(f317,plain,
! [X0,X1,X5] :
( r2_hidden(sK8(X0,X5),X0)
| ~ r2_hidden(X5,X1)
| k3_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f242]) ).
fof(f318,plain,
! [X0,X1,X5] :
( r2_hidden(X5,sK8(X0,X5))
| ~ r2_hidden(X5,X1)
| k3_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f242]) ).
fof(f319,plain,
! [X0,X1,X6,X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0)
| k3_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f242]) ).
fof(f323,plain,
! [X2,X3,X0,X1,X5] :
( k1_funct_1(X3,X5) = k2_xboole_0(k1_funct_1(X1,X5),k1_funct_1(X2,X5))
| ~ r2_hidden(X5,X0)
| k2_pboole(X0,X1,X2) != X3
| ~ m1_pboole(X3,X0)
| ~ m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f245]) ).
fof(f326,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,[],[f159]) ).
fof(f327,plain,
! [X2,X0,X1] :
( m1_pboole(k2_pboole(X0,X1,X2),X0)
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(cnf_transformation,[],[f161]) ).
fof(f328,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k3_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(cnf_transformation,[],[f163]) ).
fof(f338,plain,
! [X2,X0,X1] :
( ~ m4_pboole(X2,X0,X1)
| m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f358,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(sK15(X0,X1,X2,X3,X4),X3)
| ~ r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4))
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(cnf_transformation,[],[f253]) ).
fof(f359,plain,
! [X2,X3,X0,X1,X4] :
( k1_funct_1(sK15(X0,X1,X2,X3,X4),X4) = X0
| ~ r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4))
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(cnf_transformation,[],[f253]) ).
fof(f360,plain,
! [X2,X3,X0,X1,X4] :
( m1_closure2(sK15(X0,X1,X2,X3,X4),X1,X2,k6_closure2(X1,X2))
| ~ r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4))
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(cnf_transformation,[],[f253]) ).
fof(f361,plain,
! [X2,X3,X0,X1,X4,X5] :
( r2_hidden(X0,a_4_0_closure3(X1,X2,X3,X4))
| ~ m1_closure2(X5,X1,X2,k6_closure2(X1,X2))
| k1_funct_1(X5,X4) != X0
| ~ r2_hidden(X5,X3)
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(cnf_transformation,[],[f253]) ).
fof(f437,plain,
! [X2,X3,X0,X1] :
( 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(cnf_transformation,[],[f207]) ).
fof(f438,plain,
! [X0,X1] :
( k1_closure2(X0,X1) = k6_closure2(X0,X1)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f208]) ).
fof(f446,plain,
! [X2,X0,X1] :
( r6_pboole(X0,X1,X1)
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(X2,X0) ),
inference(cnf_transformation,[],[f216]) ).
fof(f451,plain,
! [X0,X1] :
( r2_hidden(sK39(X0,X1),X1)
| X0 = X1
| r2_hidden(sK39(X0,X1),X0) ),
inference(cnf_transformation,[],[f285]) ).
fof(f452,plain,
! [X0,X1] :
( ~ r2_hidden(sK39(X0,X1),X1)
| X0 = X1
| ~ r2_hidden(sK39(X0,X1),X0) ),
inference(cnf_transformation,[],[f285]) ).
fof(f453,plain,
! [X2,X0,X1] :
( r2_hidden(sK40(X0,X1,X2),X0)
| X1 = X2
| ~ m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f286]) ).
fof(f454,plain,
! [X2,X0,X1] :
( k1_funct_1(X1,sK40(X0,X1,X2)) != k1_funct_1(X2,sK40(X0,X1,X2))
| X1 = X2
| ~ m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f286]) ).
fof(f461,plain,
! [X0,X1,X4] :
( r2_hidden(X4,k2_xboole_0(X0,X1))
| ~ r2_hidden(X4,X0) ),
inference(equality_resolution,[],[f310]) ).
fof(f462,plain,
! [X0,X1,X4] :
( r2_hidden(X4,k2_xboole_0(X0,X1))
| ~ r2_hidden(X4,X1) ),
inference(equality_resolution,[],[f309]) ).
fof(f463,plain,
! [X0,X1,X4] :
( ~ r2_hidden(X4,k2_xboole_0(X0,X1))
| r2_hidden(X4,X1)
| r2_hidden(X4,X0) ),
inference(equality_resolution,[],[f308]) ).
fof(f464,plain,
! [X2,X0,X1,X5] :
( k3_tarski(a_4_0_closure3(X0,X1,X2,X5)) = k1_funct_1(k2_closure3(X0,X1,X2),X5)
| ~ r2_hidden(X5,X0)
| ~ m4_pboole(k2_closure3(X0,X1,X2),X0,X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0) ),
inference(equality_resolution,[],[f314]) ).
fof(f465,plain,
! [X0,X6,X5] :
( r2_hidden(X5,k3_tarski(X0))
| ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0) ),
inference(equality_resolution,[],[f319]) ).
fof(f466,plain,
! [X0,X5] :
( r2_hidden(X5,sK8(X0,X5))
| ~ r2_hidden(X5,k3_tarski(X0)) ),
inference(equality_resolution,[],[f318]) ).
fof(f467,plain,
! [X0,X5] :
( r2_hidden(sK8(X0,X5),X0)
| ~ r2_hidden(X5,k3_tarski(X0)) ),
inference(equality_resolution,[],[f317]) ).
fof(f468,plain,
! [X2,X0,X1,X5] :
( k2_xboole_0(k1_funct_1(X1,X5),k1_funct_1(X2,X5)) = k1_funct_1(k2_pboole(X0,X1,X2),X5)
| ~ r2_hidden(X5,X0)
| ~ m1_pboole(k2_pboole(X0,X1,X2),X0)
| ~ m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0) ),
inference(equality_resolution,[],[f323]) ).
fof(f469,plain,
! [X2,X3,X1,X4,X5] :
( r2_hidden(k1_funct_1(X5,X4),a_4_0_closure3(X1,X2,X3,X4))
| ~ m1_closure2(X5,X1,X2,k6_closure2(X1,X2))
| ~ r2_hidden(X5,X3)
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(equality_resolution,[],[f361]) ).
fof(f473,definition,
sF41 = k3_closure3(sK0,sK1,sK2,sK3),
introduced(definition,[new_symbols(definition,[sF41])],[function_definition]) ).
fof(f474,plain,
k3_closure3(sK0,sK1,sK2,sK3) = sF41,
inference(reorient_equations,[],[f473]) ).
fof(f475,definition,
sF42 = k2_closure3(sK0,sK1,sF41),
introduced(definition,[new_symbols(definition,[sF42])],[function_definition]) ).
fof(f476,plain,
k2_closure3(sK0,sK1,sF41) = sF42,
inference(reorient_equations,[],[f475]) ).
fof(f477,definition,
sF43 = k2_closure3(sK0,sK1,sK2),
introduced(definition,[new_symbols(definition,[sF43])],[function_definition]) ).
fof(f478,plain,
k2_closure3(sK0,sK1,sK2) = sF43,
inference(reorient_equations,[],[f477]) ).
fof(f479,definition,
sF44 = k2_closure3(sK0,sK1,sK3),
introduced(definition,[new_symbols(definition,[sF44])],[function_definition]) ).
fof(f480,plain,
k2_closure3(sK0,sK1,sK3) = sF44,
inference(reorient_equations,[],[f479]) ).
fof(f481,definition,
sF45 = k2_pboole(sK0,sF43,sF44),
introduced(definition,[new_symbols(definition,[sF45])],[function_definition]) ).
fof(f482,plain,
k2_pboole(sK0,sF43,sF44) = sF45,
inference(reorient_equations,[],[f481]) ).
fof(f483,plain,
~ r6_pboole(sK0,sF42,sF45),
inference(definition_folding,[],[f290,f482,f480,f478,f476,f474]) ).
fof(f484,definition,
sF46 = k1_closure2(sK0,sK1),
introduced(definition,[new_symbols(definition,[sF46])],[function_definition]) ).
fof(f485,plain,
k1_closure2(sK0,sK1) = sF46,
inference(reorient_equations,[],[f484]) ).
fof(f486,definition,
sF47 = k1_zfmisc_1(sF46),
introduced(definition,[new_symbols(definition,[sF47])],[function_definition]) ).
fof(f487,plain,
k1_zfmisc_1(sF46) = sF47,
inference(reorient_equations,[],[f486]) ).
fof(f488,plain,
m1_subset_1(sK3,sF47),
inference(definition_folding,[],[f289,f487,f485]) ).
fof(f489,plain,
m1_subset_1(sK2,sF47),
inference(definition_folding,[],[f288,f487,f485]) ).
fof(f491,plain,
! [X2,X0,X1,X5] :
( k2_xboole_0(k1_funct_1(X1,X5),k1_funct_1(X2,X5)) = k1_funct_1(k2_pboole(X0,X1,X2),X5)
| ~ r2_hidden(X5,X0)
| ~ m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0) ),
inference(forward_subsumption_resolution,[],[f468,f327]) ).
fof(f492,plain,
! [X2,X0,X1,X5] :
( k3_tarski(a_4_0_closure3(X0,X1,X2,X5)) = k1_funct_1(k2_closure3(X0,X1,X2),X5)
| ~ r2_hidden(X5,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0) ),
inference(forward_subsumption_resolution,[],[f464,f326]) ).
fof(f495,plain,
k1_closure2(sK0,sK1) = k6_closure2(sK0,sK1),
inference(unit_resulting_resolution,[],[f438,f287]) ).
fof(f496,plain,
sF46 = k6_closure2(sK0,sK1),
inference(forward_demodulation,[],[f495,f485]) ).
fof(f501,plain,
( sF41 = k2_xboole_0(sK2,sK3)
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[],[f474,f437]) ).
fof(f502,plain,
( sF41 = k2_xboole_0(sK2,sK3)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f501,f287]) ).
fof(f504,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(sF46))
| sF41 = k2_xboole_0(sK2,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_demodulation,[],[f502,f485]) ).
fof(f506,plain,
( ~ m1_subset_1(sK2,sF47)
| sF41 = k2_xboole_0(sK2,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_demodulation,[],[f504,f487]) ).
fof(f508,plain,
( sF41 = k2_xboole_0(sK2,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f506,f489]) ).
fof(f510,plain,
( ~ m1_subset_1(sK3,k1_zfmisc_1(sF46))
| sF41 = k2_xboole_0(sK2,sK3) ),
inference(forward_demodulation,[],[f508,f485]) ).
fof(f512,plain,
( ~ m1_subset_1(sK3,sF47)
| sF41 = k2_xboole_0(sK2,sK3) ),
inference(forward_demodulation,[],[f510,f487]) ).
fof(f514,plain,
sF41 = k2_xboole_0(sK2,sK3),
inference(forward_subsumption_resolution,[],[f512,f488]) ).
fof(f517,plain,
( m1_pboole(sF45,sK0)
| ~ m1_pboole(sF43,sK0)
| ~ m1_pboole(sF44,sK0) ),
inference(superposition,[],[f327,f482]) ).
fof(f523,definition,
( spl48_1
<=> m1_pboole(sF44,sK0) ),
introduced(definition,[new_symbols(definition,[spl48_1])],[avatar_definition]) ).
fof(f524,plain,
( m1_pboole(sF44,sK0)
| ~ spl48_1 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f525,plain,
( ~ m1_pboole(sF44,sK0)
| spl48_1 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f527,definition,
( spl48_2
<=> m1_pboole(sF43,sK0) ),
introduced(definition,[new_symbols(definition,[spl48_2])],[avatar_definition]) ).
fof(f528,plain,
( m1_pboole(sF43,sK0)
| ~ spl48_2 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f531,definition,
( spl48_3
<=> m1_pboole(sF45,sK0) ),
introduced(definition,[new_symbols(definition,[spl48_3])],[avatar_definition]) ).
fof(f533,plain,
( m1_pboole(sF45,sK0)
| ~ spl48_3 ),
inference(avatar_component_clause,[],[f531]) ).
fof(f534,plain,
( ~ spl48_1
| ~ spl48_2
| spl48_3 ),
inference(avatar_split_clause,[],[f517,f531,f527,f523]) ).
fof(f562,plain,
( m4_pboole(sF42,sK0,sK1)
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sF41,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[],[f326,f476]) ).
fof(f563,plain,
( m4_pboole(sF44,sK0,sK1)
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[],[f326,f480]) ).
fof(f564,plain,
( m4_pboole(sF43,sK0,sK1)
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[],[f326,f478]) ).
fof(f565,plain,
( m4_pboole(sF43,sK0,sK1)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f564,f287]) ).
fof(f566,plain,
( m4_pboole(sF44,sK0,sK1)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f563,f287]) ).
fof(f567,plain,
( m4_pboole(sF42,sK0,sK1)
| ~ m1_subset_1(sF41,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f562,f287]) ).
fof(f568,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(sF46))
| m4_pboole(sF43,sK0,sK1) ),
inference(forward_demodulation,[],[f565,f485]) ).
fof(f569,plain,
( ~ m1_subset_1(sK3,k1_zfmisc_1(sF46))
| m4_pboole(sF44,sK0,sK1) ),
inference(forward_demodulation,[],[f566,f485]) ).
fof(f570,plain,
( ~ m1_subset_1(sF41,k1_zfmisc_1(sF46))
| m4_pboole(sF42,sK0,sK1) ),
inference(forward_demodulation,[],[f567,f485]) ).
fof(f571,plain,
( ~ m1_subset_1(sK2,sF47)
| m4_pboole(sF43,sK0,sK1) ),
inference(forward_demodulation,[],[f568,f487]) ).
fof(f572,plain,
( ~ m1_subset_1(sK3,sF47)
| m4_pboole(sF44,sK0,sK1) ),
inference(forward_demodulation,[],[f569,f487]) ).
fof(f573,plain,
( ~ m1_subset_1(sF41,sF47)
| m4_pboole(sF42,sK0,sK1) ),
inference(forward_demodulation,[],[f570,f487]) ).
fof(f574,plain,
m4_pboole(sF43,sK0,sK1),
inference(forward_subsumption_resolution,[],[f571,f489]) ).
fof(f575,plain,
m4_pboole(sF44,sK0,sK1),
inference(forward_subsumption_resolution,[],[f572,f488]) ).
fof(f577,definition,
( spl48_4
<=> m4_pboole(sF42,sK0,sK1) ),
introduced(definition,[new_symbols(definition,[spl48_4])],[avatar_definition]) ).
fof(f579,plain,
( m4_pboole(sF42,sK0,sK1)
| ~ spl48_4 ),
inference(avatar_component_clause,[],[f577]) ).
fof(f581,definition,
( spl48_5
<=> m1_subset_1(sF41,sF47) ),
introduced(definition,[new_symbols(definition,[spl48_5])],[avatar_definition]) ).
fof(f582,plain,
( m1_subset_1(sF41,sF47)
| ~ spl48_5 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f583,plain,
( ~ m1_subset_1(sF41,sF47)
| spl48_5 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f584,plain,
( spl48_4
| ~ spl48_5 ),
inference(avatar_split_clause,[],[f573,f581,f577]) ).
fof(f601,plain,
! [X0] :
( k3_tarski(a_4_0_closure3(sK0,sK1,sF41,X0)) = k1_funct_1(sF42,X0)
| ~ r2_hidden(X0,sK0)
| ~ m1_subset_1(sF41,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_pboole(sK1,sK0) ),
inference(superposition,[],[f492,f476]) ).
fof(f603,plain,
! [X0] :
( k1_funct_1(sF43,X0) = k3_tarski(a_4_0_closure3(sK0,sK1,sK2,X0))
| ~ r2_hidden(X0,sK0)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_pboole(sK1,sK0) ),
inference(superposition,[],[f492,f478]) ).
fof(f606,plain,
! [X2,X3,X0,X1,X4,X5] :
( k1_funct_1(k2_pboole(X5,X4,k2_closure3(X0,X1,X2)),X3) = k2_xboole_0(k1_funct_1(X4,X3),k3_tarski(a_4_0_closure3(X0,X1,X2,X3)))
| ~ r2_hidden(X3,X5)
| ~ m1_pboole(k2_closure3(X0,X1,X2),X5)
| ~ m1_pboole(X4,X5)
| ~ r2_hidden(X3,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(X0,X1)))
| ~ m1_pboole(X1,X0) ),
inference(superposition,[],[f491,f492]) ).
fof(f608,plain,
! [X0] :
( k1_funct_1(sF43,X0) = k3_tarski(a_4_0_closure3(sK0,sK1,sK2,X0))
| ~ r2_hidden(X0,sK0)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f603,f287]) ).
fof(f610,plain,
! [X0] :
( k3_tarski(a_4_0_closure3(sK0,sK1,sF41,X0)) = k1_funct_1(sF42,X0)
| ~ r2_hidden(X0,sK0)
| ~ m1_subset_1(sF41,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f601,f287]) ).
fof(f611,plain,
! [X0] :
( ~ m1_subset_1(sK2,k1_zfmisc_1(sF46))
| k1_funct_1(sF43,X0) = k3_tarski(a_4_0_closure3(sK0,sK1,sK2,X0))
| ~ r2_hidden(X0,sK0) ),
inference(forward_demodulation,[],[f608,f485]) ).
fof(f613,plain,
! [X0] :
( ~ m1_subset_1(sF41,k1_zfmisc_1(sF46))
| k3_tarski(a_4_0_closure3(sK0,sK1,sF41,X0)) = k1_funct_1(sF42,X0)
| ~ r2_hidden(X0,sK0) ),
inference(forward_demodulation,[],[f610,f485]) ).
fof(f614,plain,
! [X0] :
( ~ m1_subset_1(sK2,sF47)
| k1_funct_1(sF43,X0) = k3_tarski(a_4_0_closure3(sK0,sK1,sK2,X0))
| ~ r2_hidden(X0,sK0) ),
inference(forward_demodulation,[],[f611,f487]) ).
fof(f616,plain,
! [X0] :
( ~ m1_subset_1(sF41,sF47)
| k3_tarski(a_4_0_closure3(sK0,sK1,sF41,X0)) = k1_funct_1(sF42,X0)
| ~ r2_hidden(X0,sK0) ),
inference(forward_demodulation,[],[f613,f487]) ).
fof(f617,plain,
! [X0] :
( k1_funct_1(sF43,X0) = k3_tarski(a_4_0_closure3(sK0,sK1,sK2,X0))
| ~ r2_hidden(X0,sK0) ),
inference(forward_subsumption_resolution,[],[f614,f489]) ).
fof(f707,plain,
m1_pboole(sF43,sK0),
inference(unit_resulting_resolution,[],[f338,f287,f574]) ).
fof(f709,plain,
( m1_pboole(sF44,sK0)
| ~ m1_pboole(sK1,sK0) ),
inference(resolution,[],[f338,f575]) ).
fof(f713,plain,
( ~ m1_pboole(sK1,sK0)
| spl48_1 ),
inference(forward_subsumption_resolution,[],[f709,f525]) ).
fof(f716,plain,
spl48_2,
inference(avatar_split_clause,[],[f707,f527]) ).
fof(f717,plain,
( $false
| spl48_1 ),
inference(forward_subsumption_resolution,[],[f713,f287]) ).
fof(f718,plain,
spl48_1,
inference(avatar_contradiction_clause,[],[f717]) ).
fof(f819,plain,
! [X0] :
( ~ r2_hidden(X0,sF41)
| r2_hidden(X0,sK3)
| r2_hidden(X0,sK2) ),
inference(superposition,[],[f463,f514]) ).
fof(f823,plain,
! [X2,X3,X0,X1] :
( r2_hidden(sK15(X0,X1,X2,sF41,X3),sK3)
| r2_hidden(sK15(X0,X1,X2,sF41,X3),sK2)
| ~ r2_hidden(X0,a_4_0_closure3(X1,X2,sF41,X3))
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(sF41,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(resolution,[],[f819,f358]) ).
fof(f865,plain,
! [X2,X0,X1] :
( m1_closure2(sK15(X0,sK0,sK1,X1,X2),sK0,sK1,sF46)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X1,X2))
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[],[f360,f496]) ).
fof(f867,plain,
! [X2,X0,X1] :
( m1_closure2(sK15(X0,sK0,sK1,X1,X2),sK0,sK1,sF46)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X1,X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f865,f287]) ).
fof(f868,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(sF46))
| m1_closure2(sK15(X0,sK0,sK1,X1,X2),sK0,sK1,sF46)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X1,X2)) ),
inference(forward_demodulation,[],[f867,f485]) ).
fof(f869,plain,
! [X2,X0,X1] :
( m1_closure2(sK15(X0,sK0,sK1,X1,X2),sK0,sK1,sF46)
| ~ m1_subset_1(X1,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X1,X2)) ),
inference(forward_demodulation,[],[f868,f487]) ).
fof(f1000,plain,
( m1_subset_1(sF41,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[],[f328,f474]) ).
fof(f1014,plain,
( m1_subset_1(sF41,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f1000,f287]) ).
fof(f1017,plain,
( m1_subset_1(sF41,k1_zfmisc_1(sF46))
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_demodulation,[],[f1014,f485]) ).
fof(f1019,plain,
( m1_subset_1(sF41,sF47)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_demodulation,[],[f1017,f487]) ).
fof(f1021,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| spl48_5 ),
inference(forward_subsumption_resolution,[],[f1019,f583]) ).
fof(f1022,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(sF46))
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| spl48_5 ),
inference(forward_demodulation,[],[f1021,f485]) ).
fof(f1023,plain,
( ~ m1_subset_1(sK2,sF47)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| spl48_5 ),
inference(forward_demodulation,[],[f1022,f487]) ).
fof(f1024,plain,
( ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| spl48_5 ),
inference(forward_subsumption_resolution,[],[f1023,f489]) ).
fof(f1025,plain,
( ~ m1_subset_1(sK3,k1_zfmisc_1(sF46))
| spl48_5 ),
inference(forward_demodulation,[],[f1024,f485]) ).
fof(f1026,plain,
( ~ m1_subset_1(sK3,sF47)
| spl48_5 ),
inference(forward_demodulation,[],[f1025,f487]) ).
fof(f1027,plain,
( $false
| spl48_5 ),
inference(forward_subsumption_resolution,[],[f1026,f488]) ).
fof(f1028,plain,
spl48_5,
inference(avatar_contradiction_clause,[],[f1027]) ).
fof(f1029,plain,
( ! [X0] :
( k3_tarski(a_4_0_closure3(sK0,sK1,sF41,X0)) = k1_funct_1(sF42,X0)
| ~ r2_hidden(X0,sK0) )
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f616,f582]) ).
fof(f1032,plain,
( m1_pboole(sF42,sK0)
| ~ spl48_4 ),
inference(unit_resulting_resolution,[],[f338,f287,f579]) ).
fof(f1062,plain,
( r6_pboole(sK0,sF42,sF42)
| ~ spl48_4 ),
inference(unit_resulting_resolution,[],[f446,f287,f1032]) ).
fof(f1427,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X2,a_4_0_closure3(sK0,sK1,sK2,X0))
| ~ r2_hidden(X1,X2)
| r2_hidden(X1,k1_funct_1(sF43,X0))
| ~ r2_hidden(X0,sK0) ),
inference(superposition,[],[f465,f617]) ).
fof(f1428,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X2,a_4_0_closure3(sK0,sK1,sF41,X0))
| ~ r2_hidden(X1,X2)
| r2_hidden(X1,k1_funct_1(sF42,X0))
| ~ r2_hidden(X0,sK0) )
| ~ spl48_5 ),
inference(superposition,[],[f465,f1029]) ).
fof(f1429,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,k1_funct_1(X1,X2))
| r2_hidden(X0,k1_funct_1(sF42,X2))
| ~ r2_hidden(X2,sK0)
| ~ m1_closure2(X1,sK0,sK1,k6_closure2(sK0,sK1))
| ~ r2_hidden(X1,sF41)
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sF41,k1_zfmisc_1(k1_closure2(sK0,sK1))) )
| ~ spl48_5 ),
inference(resolution,[],[f1428,f469]) ).
fof(f1434,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,k1_funct_1(X1,X2))
| r2_hidden(X0,k1_funct_1(sF42,X2))
| ~ r2_hidden(X2,sK0)
| ~ m1_closure2(X1,sK0,sK1,k6_closure2(sK0,sK1))
| ~ r2_hidden(X1,sF41)
| ~ m1_subset_1(sF41,k1_zfmisc_1(k1_closure2(sK0,sK1))) )
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f1429,f287]) ).
fof(f1435,plain,
( ! [X2,X0,X1] :
( ~ m1_closure2(X1,sK0,sK1,sF46)
| ~ r2_hidden(X0,k1_funct_1(X1,X2))
| r2_hidden(X0,k1_funct_1(sF42,X2))
| ~ r2_hidden(X2,sK0)
| ~ r2_hidden(X1,sF41)
| ~ m1_subset_1(sF41,k1_zfmisc_1(k1_closure2(sK0,sK1))) )
| ~ spl48_5 ),
inference(forward_demodulation,[],[f1434,f496]) ).
fof(f1436,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(sF41,k1_zfmisc_1(sF46))
| ~ m1_closure2(X1,sK0,sK1,sF46)
| ~ r2_hidden(X0,k1_funct_1(X1,X2))
| r2_hidden(X0,k1_funct_1(sF42,X2))
| ~ r2_hidden(X2,sK0)
| ~ r2_hidden(X1,sF41) )
| ~ spl48_5 ),
inference(forward_demodulation,[],[f1435,f485]) ).
fof(f1437,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(sF41,sF47)
| ~ m1_closure2(X1,sK0,sK1,sF46)
| ~ r2_hidden(X0,k1_funct_1(X1,X2))
| r2_hidden(X0,k1_funct_1(sF42,X2))
| ~ r2_hidden(X2,sK0)
| ~ r2_hidden(X1,sF41) )
| ~ spl48_5 ),
inference(forward_demodulation,[],[f1436,f487]) ).
fof(f1438,plain,
( ! [X2,X0,X1] :
( ~ m1_closure2(X1,sK0,sK1,sF46)
| ~ r2_hidden(X0,k1_funct_1(X1,X2))
| r2_hidden(X0,k1_funct_1(sF42,X2))
| ~ r2_hidden(X2,sK0)
| ~ r2_hidden(X1,sF41) )
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f1437,f582]) ).
fof(f1449,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,k1_funct_1(X1,X2))
| r2_hidden(X0,k1_funct_1(sF43,X2))
| ~ r2_hidden(X2,sK0)
| ~ m1_closure2(X1,sK0,sK1,k6_closure2(sK0,sK1))
| ~ r2_hidden(X1,sK2)
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(resolution,[],[f1427,f469]) ).
fof(f1454,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,k1_funct_1(X1,X2))
| r2_hidden(X0,k1_funct_1(sF43,X2))
| ~ r2_hidden(X2,sK0)
| ~ m1_closure2(X1,sK0,sK1,k6_closure2(sK0,sK1))
| ~ r2_hidden(X1,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f1449,f287]) ).
fof(f1455,plain,
! [X2,X0,X1] :
( ~ m1_closure2(X1,sK0,sK1,sF46)
| ~ r2_hidden(X0,k1_funct_1(X1,X2))
| r2_hidden(X0,k1_funct_1(sF43,X2))
| ~ r2_hidden(X2,sK0)
| ~ r2_hidden(X1,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_demodulation,[],[f1454,f496]) ).
fof(f1456,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sK2,k1_zfmisc_1(sF46))
| ~ m1_closure2(X1,sK0,sK1,sF46)
| ~ r2_hidden(X0,k1_funct_1(X1,X2))
| r2_hidden(X0,k1_funct_1(sF43,X2))
| ~ r2_hidden(X2,sK0)
| ~ r2_hidden(X1,sK2) ),
inference(forward_demodulation,[],[f1455,f485]) ).
fof(f1457,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sK2,sF47)
| ~ m1_closure2(X1,sK0,sK1,sF46)
| ~ r2_hidden(X0,k1_funct_1(X1,X2))
| r2_hidden(X0,k1_funct_1(sF43,X2))
| ~ r2_hidden(X2,sK0)
| ~ r2_hidden(X1,sK2) ),
inference(forward_demodulation,[],[f1456,f487]) ).
fof(f1458,plain,
! [X2,X0,X1] :
( ~ m1_closure2(X1,sK0,sK1,sF46)
| ~ r2_hidden(X0,k1_funct_1(X1,X2))
| r2_hidden(X0,k1_funct_1(sF43,X2))
| ~ r2_hidden(X2,sK0)
| ~ r2_hidden(X1,sK2) ),
inference(forward_subsumption_resolution,[],[f1457,f489]) ).
fof(f1461,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X0,k1_funct_1(sK15(X1,sK0,sK1,X2,X3),X4))
| r2_hidden(X0,k1_funct_1(sF42,X4))
| ~ r2_hidden(X4,sK0)
| ~ r2_hidden(sK15(X1,sK0,sK1,X2,X3),sF41)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,X2,X3)) )
| ~ spl48_5 ),
inference(resolution,[],[f1438,f869]) ).
fof(f1468,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X0,k1_funct_1(sK15(X1,sK0,sK1,X2,X3),X4))
| r2_hidden(X0,k1_funct_1(sF43,X4))
| ~ r2_hidden(X4,sK0)
| ~ r2_hidden(sK15(X1,sK0,sK1,X2,X3),sK2)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,X2,X3)) ),
inference(resolution,[],[f1458,f869]) ).
fof(f1484,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(X1,X0)
| r2_hidden(X1,k1_funct_1(sF42,X3))
| ~ r2_hidden(X3,sK0)
| ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sF41)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(sK0,sK1))) )
| ~ spl48_5 ),
inference(superposition,[],[f1461,f359]) ).
fof(f1485,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(X1,X0)
| r2_hidden(X1,k1_funct_1(sF42,X3))
| ~ r2_hidden(X3,sK0)
| ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sF41)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(sK0,sK1))) )
| ~ spl48_5 ),
inference(duplicate_literal_removal,[],[f1484]) ).
fof(f1486,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(X1,X0)
| r2_hidden(X1,k1_funct_1(sF42,X3))
| ~ r2_hidden(X3,sK0)
| ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sF41)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(sK0,sK1))) )
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f1485,f287]) ).
fof(f1487,plain,
( ! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(sF46))
| ~ r2_hidden(X1,X0)
| r2_hidden(X1,k1_funct_1(sF42,X3))
| ~ r2_hidden(X3,sK0)
| ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sF41)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3)) )
| ~ spl48_5 ),
inference(forward_demodulation,[],[f1486,f485]) ).
fof(f1488,plain,
( ! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X1,X0)
| r2_hidden(X1,k1_funct_1(sF42,X3))
| ~ r2_hidden(X3,sK0)
| ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sF41)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3)) )
| ~ spl48_5 ),
inference(forward_demodulation,[],[f1487,f487]) ).
fof(f1489,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sF41)
| ~ r2_hidden(X1,X0)
| r2_hidden(X1,k1_funct_1(sF42,X3))
| ~ r2_hidden(X3,sK0)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3)) )
| ~ spl48_5 ),
inference(duplicate_literal_removal,[],[f1488]) ).
fof(f1522,plain,
! [X0] :
( ~ r2_hidden(X0,sK2)
| r2_hidden(X0,sF41) ),
inference(superposition,[],[f461,f514]) ).
fof(f1524,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(X4,k1_funct_1(k2_pboole(X0,X1,X2),X3))
| ~ r2_hidden(X4,k1_funct_1(X1,X3))
| ~ r2_hidden(X3,X0)
| ~ m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0) ),
inference(superposition,[],[f461,f491]) ).
fof(f1527,plain,
! [X2,X3,X0,X1] :
( r2_hidden(sK15(X0,X1,X2,sK2,X3),sF41)
| ~ r2_hidden(X0,a_4_0_closure3(X1,X2,sK2,X3))
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(resolution,[],[f1522,f358]) ).
fof(f1534,plain,
! [X0,X1] :
( r2_hidden(X0,k1_funct_1(sF45,X1))
| ~ r2_hidden(X0,k1_funct_1(sF43,X1))
| ~ r2_hidden(X1,sK0)
| ~ m1_pboole(sF44,sK0)
| ~ m1_pboole(sF43,sK0) ),
inference(superposition,[],[f1524,f482]) ).
fof(f1560,plain,
( ! [X0,X1] :
( r2_hidden(X0,k1_funct_1(sF45,X1))
| ~ r2_hidden(X0,k1_funct_1(sF43,X1))
| ~ r2_hidden(X1,sK0)
| ~ m1_pboole(sF43,sK0) )
| ~ spl48_1 ),
inference(forward_subsumption_resolution,[],[f1534,f524]) ).
fof(f1561,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k1_funct_1(sF43,X1))
| r2_hidden(X0,k1_funct_1(sF45,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl48_1
| ~ spl48_2 ),
inference(forward_subsumption_resolution,[],[f1560,f528]) ).
fof(f1570,plain,
! [X0] :
( ~ r2_hidden(X0,sK3)
| r2_hidden(X0,sF41) ),
inference(superposition,[],[f462,f514]) ).
fof(f1575,plain,
! [X2,X3,X0,X1] :
( r2_hidden(sK15(X0,X1,X2,sK3,X3),sF41)
| ~ r2_hidden(X0,a_4_0_closure3(X1,X2,sK3,X3))
| ~ m1_pboole(X2,X1)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(X1,X2))) ),
inference(resolution,[],[f1570,f358]) ).
fof(f1836,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sK2,X1))
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0)
| ~ m1_subset_1(sK2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sK2,X1)) )
| ~ spl48_5 ),
inference(resolution,[],[f1527,f1489]) ).
fof(f1839,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sK2,X1))
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0)
| ~ m1_subset_1(sK2,sF47) )
| ~ spl48_5 ),
inference(duplicate_literal_removal,[],[f1836]) ).
fof(f1840,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sK2,X1))
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0)
| ~ m1_subset_1(sK2,sF47) )
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f1839,f287]) ).
fof(f1841,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sK2,X1))
| ~ m1_subset_1(sK2,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f1840,f489]) ).
fof(f1842,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(sK2,k1_zfmisc_1(sF46))
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sK2,X1))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl48_5 ),
inference(forward_demodulation,[],[f1841,f485]) ).
fof(f1843,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(sK2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sK2,X1))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl48_5 ),
inference(forward_demodulation,[],[f1842,f487]) ).
fof(f1844,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sK2,X1))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f1843,f489]) ).
fof(f1846,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,sK8(a_4_0_closure3(sK0,sK1,sK2,X1),X2))
| r2_hidden(X0,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0)
| ~ r2_hidden(X2,k3_tarski(a_4_0_closure3(sK0,sK1,sK2,X1))) )
| ~ spl48_5 ),
inference(resolution,[],[f1844,f467]) ).
fof(f1863,plain,
( ! [X0,X1] :
( r2_hidden(X0,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0)
| ~ r2_hidden(X0,k3_tarski(a_4_0_closure3(sK0,sK1,sK2,X1)))
| ~ r2_hidden(X0,k3_tarski(a_4_0_closure3(sK0,sK1,sK2,X1))) )
| ~ spl48_5 ),
inference(resolution,[],[f1846,f466]) ).
fof(f1869,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k3_tarski(a_4_0_closure3(sK0,sK1,sK2,X1)))
| ~ r2_hidden(X1,sK0)
| r2_hidden(X0,k1_funct_1(sF42,X1)) )
| ~ spl48_5 ),
inference(duplicate_literal_removal,[],[f1863]) ).
fof(f1876,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,k1_funct_1(sF43,X0))
| ~ r2_hidden(X0,sK0)
| r2_hidden(X1,k1_funct_1(sF42,X0))
| ~ r2_hidden(X0,sK0) )
| ~ spl48_5 ),
inference(superposition,[],[f1869,f617]) ).
fof(f1877,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,k1_funct_1(sF43,X0))
| ~ r2_hidden(X0,sK0)
| r2_hidden(X1,k1_funct_1(sF42,X0)) )
| ~ spl48_5 ),
inference(duplicate_literal_removal,[],[f1876]) ).
fof(f1883,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sK3,X1))
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0)
| ~ m1_subset_1(sK3,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sK3,X1)) )
| ~ spl48_5 ),
inference(resolution,[],[f1575,f1489]) ).
fof(f1886,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sK3,X1))
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0)
| ~ m1_subset_1(sK3,sF47) )
| ~ spl48_5 ),
inference(duplicate_literal_removal,[],[f1883]) ).
fof(f1887,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sK3,X1))
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0)
| ~ m1_subset_1(sK3,sF47) )
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f1886,f287]) ).
fof(f1888,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sK3,X1))
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f1887,f488]) ).
fof(f1889,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(sK3,k1_zfmisc_1(sF46))
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sK3,X1))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl48_5 ),
inference(forward_demodulation,[],[f1888,f485]) ).
fof(f1890,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(sK3,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sK3,X1))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl48_5 ),
inference(forward_demodulation,[],[f1889,f487]) ).
fof(f1891,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,sK3,X1))
| ~ r2_hidden(X2,X0)
| r2_hidden(X2,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f1890,f488]) ).
fof(f1893,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,sK8(a_4_0_closure3(sK0,sK1,sK3,X1),X2))
| r2_hidden(X0,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0)
| ~ r2_hidden(X2,k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X1))) )
| ~ spl48_5 ),
inference(resolution,[],[f1891,f467]) ).
fof(f1910,plain,
( ! [X0,X1] :
( r2_hidden(X0,k1_funct_1(sF42,X1))
| ~ r2_hidden(X1,sK0)
| ~ r2_hidden(X0,k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X1)))
| ~ r2_hidden(X0,k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X1))) )
| ~ spl48_5 ),
inference(resolution,[],[f1893,f466]) ).
fof(f1916,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X1)))
| ~ r2_hidden(X1,sK0)
| r2_hidden(X0,k1_funct_1(sF42,X1)) )
| ~ spl48_5 ),
inference(duplicate_literal_removal,[],[f1910]) ).
fof(f2631,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X1,X0)
| r2_hidden(X1,k1_funct_1(sF43,X3))
| ~ r2_hidden(X3,sK0)
| ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sK2)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(superposition,[],[f1468,f359]) ).
fof(f2632,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X1,X0)
| r2_hidden(X1,k1_funct_1(sF43,X3))
| ~ r2_hidden(X3,sK0)
| ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sK2)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(duplicate_literal_removal,[],[f2631]) ).
fof(f2633,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X1,X0)
| r2_hidden(X1,k1_funct_1(sF43,X3))
| ~ r2_hidden(X3,sK0)
| ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sK2)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f2632,f287]) ).
fof(f2634,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(sF46))
| ~ r2_hidden(X1,X0)
| r2_hidden(X1,k1_funct_1(sF43,X3))
| ~ r2_hidden(X3,sK0)
| ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sK2)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3)) ),
inference(forward_demodulation,[],[f2633,f485]) ).
fof(f2635,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X1,X0)
| r2_hidden(X1,k1_funct_1(sF43,X3))
| ~ r2_hidden(X3,sK0)
| ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sK2)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3)) ),
inference(forward_demodulation,[],[f2634,f487]) ).
fof(f2636,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sK2)
| ~ r2_hidden(X1,X0)
| r2_hidden(X1,k1_funct_1(sF43,X3))
| ~ r2_hidden(X3,sK0)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3)) ),
inference(duplicate_literal_removal,[],[f2635]) ).
fof(f7958,plain,
! [X2,X0,X1] :
( k2_xboole_0(k1_funct_1(X1,X2),k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X2))) = k1_funct_1(k2_pboole(X0,X1,sF44),X2)
| ~ r2_hidden(X2,X0)
| ~ m1_pboole(sF44,X0)
| ~ m1_pboole(X1,X0)
| ~ r2_hidden(X2,sK0)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1)))
| ~ m1_pboole(sK1,sK0) ),
inference(superposition,[],[f606,f480]) ).
fof(f8100,plain,
! [X2,X0,X1] :
( k2_xboole_0(k1_funct_1(X1,X2),k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X2))) = k1_funct_1(k2_pboole(X0,X1,sF44),X2)
| ~ r2_hidden(X2,X0)
| ~ m1_pboole(sF44,X0)
| ~ m1_pboole(X1,X0)
| ~ r2_hidden(X2,sK0)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f7958,f287]) ).
fof(f8106,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sK3,k1_zfmisc_1(sF46))
| k2_xboole_0(k1_funct_1(X1,X2),k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X2))) = k1_funct_1(k2_pboole(X0,X1,sF44),X2)
| ~ r2_hidden(X2,X0)
| ~ m1_pboole(sF44,X0)
| ~ m1_pboole(X1,X0)
| ~ r2_hidden(X2,sK0) ),
inference(forward_demodulation,[],[f8100,f485]) ).
fof(f8112,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sK3,sF47)
| k2_xboole_0(k1_funct_1(X1,X2),k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X2))) = k1_funct_1(k2_pboole(X0,X1,sF44),X2)
| ~ r2_hidden(X2,X0)
| ~ m1_pboole(sF44,X0)
| ~ m1_pboole(X1,X0)
| ~ r2_hidden(X2,sK0) ),
inference(forward_demodulation,[],[f8106,f487]) ).
fof(f8115,plain,
! [X2,X0,X1] :
( k2_xboole_0(k1_funct_1(X1,X2),k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X2))) = k1_funct_1(k2_pboole(X0,X1,sF44),X2)
| ~ r2_hidden(X2,X0)
| ~ m1_pboole(sF44,X0)
| ~ m1_pboole(X1,X0)
| ~ r2_hidden(X2,sK0) ),
inference(forward_subsumption_resolution,[],[f8112,f488]) ).
fof(f8159,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X3,k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X2)))
| r2_hidden(X3,k1_funct_1(k2_pboole(X0,X1,sF44),X2))
| ~ r2_hidden(X2,X0)
| ~ m1_pboole(sF44,X0)
| ~ m1_pboole(X1,X0)
| ~ r2_hidden(X2,sK0) ),
inference(superposition,[],[f462,f8115]) ).
fof(f8160,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X3,k1_funct_1(k2_pboole(X0,X1,sF44),X2))
| r2_hidden(X3,k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X2)))
| r2_hidden(X3,k1_funct_1(X1,X2))
| ~ r2_hidden(X2,X0)
| ~ m1_pboole(sF44,X0)
| ~ m1_pboole(X1,X0)
| ~ r2_hidden(X2,sK0) ),
inference(superposition,[],[f463,f8115]) ).
fof(f8484,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k1_funct_1(sF45,X1))
| r2_hidden(X0,k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X1)))
| r2_hidden(X0,k1_funct_1(sF43,X1))
| ~ r2_hidden(X1,sK0)
| ~ m1_pboole(sF44,sK0)
| ~ m1_pboole(sF43,sK0)
| ~ r2_hidden(X1,sK0) ),
inference(superposition,[],[f8160,f482]) ).
fof(f8515,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k1_funct_1(sF45,X1))
| r2_hidden(X0,k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X1)))
| r2_hidden(X0,k1_funct_1(sF43,X1))
| ~ r2_hidden(X1,sK0)
| ~ m1_pboole(sF44,sK0)
| ~ m1_pboole(sF43,sK0) ),
inference(duplicate_literal_removal,[],[f8484]) ).
fof(f8517,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k1_funct_1(sF45,X1))
| r2_hidden(X0,k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X1)))
| r2_hidden(X0,k1_funct_1(sF43,X1))
| ~ r2_hidden(X1,sK0)
| ~ m1_pboole(sF43,sK0) )
| ~ spl48_1 ),
inference(forward_subsumption_resolution,[],[f8515,f524]) ).
fof(f8518,plain,
( ! [X0,X1] :
( r2_hidden(X0,k3_tarski(a_4_0_closure3(sK0,sK1,sK3,X1)))
| ~ r2_hidden(X0,k1_funct_1(sF45,X1))
| r2_hidden(X0,k1_funct_1(sF43,X1))
| ~ r2_hidden(X1,sK0) )
| ~ spl48_1
| ~ spl48_2 ),
inference(forward_subsumption_resolution,[],[f8517,f528]) ).
fof(f8519,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k1_funct_1(sF45,X1))
| r2_hidden(X0,k1_funct_1(sF43,X1))
| ~ r2_hidden(X1,sK0)
| ~ r2_hidden(X1,sK0)
| r2_hidden(X0,k1_funct_1(sF42,X1)) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(resolution,[],[f8518,f1916]) ).
fof(f8531,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k1_funct_1(sF45,X1))
| r2_hidden(X0,k1_funct_1(sF43,X1))
| ~ r2_hidden(X1,sK0)
| r2_hidden(X0,k1_funct_1(sF42,X1)) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(duplicate_literal_removal,[],[f8519]) ).
fof(f8532,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k1_funct_1(sF45,X1))
| ~ r2_hidden(X1,sK0)
| r2_hidden(X0,k1_funct_1(sF42,X1)) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f8531,f1877]) ).
fof(f8546,plain,
( ! [X0,X1] :
( r2_hidden(sK39(X1,k1_funct_1(sF45,X0)),k1_funct_1(sF42,X0))
| ~ r2_hidden(X0,sK0)
| k1_funct_1(sF45,X0) = X1
| r2_hidden(sK39(X1,k1_funct_1(sF45,X0)),X1) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(resolution,[],[f8532,f451]) ).
fof(f9008,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(X0,k1_funct_1(k2_pboole(X1,X2,sF44),X3))
| ~ r2_hidden(X3,X1)
| ~ m1_pboole(sF44,X1)
| ~ m1_pboole(X2,X1)
| ~ r2_hidden(X3,sK0)
| ~ r2_hidden(X0,X4)
| ~ r2_hidden(X4,a_4_0_closure3(sK0,sK1,sK3,X3)) ),
inference(resolution,[],[f8159,f465]) ).
fof(f10912,plain,
( ! [X0] :
( r2_hidden(sK39(k1_funct_1(sF42,X0),k1_funct_1(sF45,X0)),k1_funct_1(sF42,X0))
| ~ r2_hidden(X0,sK0)
| k1_funct_1(sF42,X0) = k1_funct_1(sF45,X0) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(factoring,[],[f8546]) ).
fof(f11874,plain,
! [X2,X0,X1] :
( r2_hidden(X0,k1_funct_1(sF45,X1))
| ~ r2_hidden(X1,sK0)
| ~ m1_pboole(sF44,sK0)
| ~ m1_pboole(sF43,sK0)
| ~ r2_hidden(X1,sK0)
| ~ r2_hidden(X0,X2)
| ~ r2_hidden(X2,a_4_0_closure3(sK0,sK1,sK3,X1)) ),
inference(superposition,[],[f9008,f482]) ).
fof(f11911,plain,
! [X2,X0,X1] :
( r2_hidden(X0,k1_funct_1(sF45,X1))
| ~ r2_hidden(X1,sK0)
| ~ m1_pboole(sF44,sK0)
| ~ m1_pboole(sF43,sK0)
| ~ r2_hidden(X0,X2)
| ~ r2_hidden(X2,a_4_0_closure3(sK0,sK1,sK3,X1)) ),
inference(duplicate_literal_removal,[],[f11874]) ).
fof(f11916,plain,
( ! [X2,X0,X1] :
( r2_hidden(X0,k1_funct_1(sF45,X1))
| ~ r2_hidden(X1,sK0)
| ~ m1_pboole(sF43,sK0)
| ~ r2_hidden(X0,X2)
| ~ r2_hidden(X2,a_4_0_closure3(sK0,sK1,sK3,X1)) )
| ~ spl48_1 ),
inference(forward_subsumption_resolution,[],[f11911,f524]) ).
fof(f11917,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X2,a_4_0_closure3(sK0,sK1,sK3,X1))
| ~ r2_hidden(X1,sK0)
| ~ r2_hidden(X0,X2)
| r2_hidden(X0,k1_funct_1(sF45,X1)) )
| ~ spl48_1
| ~ spl48_2 ),
inference(forward_subsumption_resolution,[],[f11916,f528]) ).
fof(f11923,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,sK0)
| ~ r2_hidden(X1,k1_funct_1(X2,X0))
| r2_hidden(X1,k1_funct_1(sF45,X0))
| ~ m1_closure2(X2,sK0,sK1,k6_closure2(sK0,sK1))
| ~ r2_hidden(X2,sK3)
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) )
| ~ spl48_1
| ~ spl48_2 ),
inference(resolution,[],[f11917,f469]) ).
fof(f11941,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,sK0)
| ~ r2_hidden(X1,k1_funct_1(X2,X0))
| r2_hidden(X1,k1_funct_1(sF45,X0))
| ~ m1_closure2(X2,sK0,sK1,k6_closure2(sK0,sK1))
| ~ r2_hidden(X2,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) )
| ~ spl48_1
| ~ spl48_2 ),
inference(forward_subsumption_resolution,[],[f11923,f287]) ).
fof(f11944,plain,
( ! [X2,X0,X1] :
( ~ m1_closure2(X2,sK0,sK1,sF46)
| ~ r2_hidden(X0,sK0)
| ~ r2_hidden(X1,k1_funct_1(X2,X0))
| r2_hidden(X1,k1_funct_1(sF45,X0))
| ~ r2_hidden(X2,sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(k1_closure2(sK0,sK1))) )
| ~ spl48_1
| ~ spl48_2 ),
inference(forward_demodulation,[],[f11941,f496]) ).
fof(f11947,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(sK3,k1_zfmisc_1(sF46))
| ~ m1_closure2(X2,sK0,sK1,sF46)
| ~ r2_hidden(X0,sK0)
| ~ r2_hidden(X1,k1_funct_1(X2,X0))
| r2_hidden(X1,k1_funct_1(sF45,X0))
| ~ r2_hidden(X2,sK3) )
| ~ spl48_1
| ~ spl48_2 ),
inference(forward_demodulation,[],[f11944,f485]) ).
fof(f11950,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(sK3,sF47)
| ~ m1_closure2(X2,sK0,sK1,sF46)
| ~ r2_hidden(X0,sK0)
| ~ r2_hidden(X1,k1_funct_1(X2,X0))
| r2_hidden(X1,k1_funct_1(sF45,X0))
| ~ r2_hidden(X2,sK3) )
| ~ spl48_1
| ~ spl48_2 ),
inference(forward_demodulation,[],[f11947,f487]) ).
fof(f11953,plain,
( ! [X2,X0,X1] :
( ~ m1_closure2(X2,sK0,sK1,sF46)
| ~ r2_hidden(X0,sK0)
| ~ r2_hidden(X1,k1_funct_1(X2,X0))
| r2_hidden(X1,k1_funct_1(sF45,X0))
| ~ r2_hidden(X2,sK3) )
| ~ spl48_1
| ~ spl48_2 ),
inference(forward_subsumption_resolution,[],[f11950,f488]) ).
fof(f11957,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X1,k1_funct_1(sK15(X2,sK0,sK1,X3,X4),X0))
| ~ r2_hidden(X0,sK0)
| r2_hidden(X1,k1_funct_1(sF45,X0))
| ~ r2_hidden(sK15(X2,sK0,sK1,X3,X4),sK3)
| ~ m1_subset_1(X3,sF47)
| ~ r2_hidden(X2,a_4_0_closure3(sK0,sK1,X3,X4)) )
| ~ spl48_1
| ~ spl48_2 ),
inference(resolution,[],[f11953,f869]) ).
fof(f11976,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(X1,X0)
| ~ r2_hidden(X3,sK0)
| r2_hidden(X1,k1_funct_1(sF45,X3))
| ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sK3)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(sK0,sK1))) )
| ~ spl48_1
| ~ spl48_2 ),
inference(superposition,[],[f11957,f359]) ).
fof(f11977,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(X1,X0)
| ~ r2_hidden(X3,sK0)
| r2_hidden(X1,k1_funct_1(sF45,X3))
| ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sK3)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(sK0,sK1))) )
| ~ spl48_1
| ~ spl48_2 ),
inference(duplicate_literal_removal,[],[f11976]) ).
fof(f11978,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(X1,X0)
| ~ r2_hidden(X3,sK0)
| r2_hidden(X1,k1_funct_1(sF45,X3))
| ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sK3)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_closure2(sK0,sK1))) )
| ~ spl48_1
| ~ spl48_2 ),
inference(forward_subsumption_resolution,[],[f11977,f287]) ).
fof(f11979,plain,
( ! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(sF46))
| ~ r2_hidden(X1,X0)
| ~ r2_hidden(X3,sK0)
| r2_hidden(X1,k1_funct_1(sF45,X3))
| ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sK3)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3)) )
| ~ spl48_1
| ~ spl48_2 ),
inference(forward_demodulation,[],[f11978,f485]) ).
fof(f11980,plain,
( ! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X1,X0)
| ~ r2_hidden(X3,sK0)
| r2_hidden(X1,k1_funct_1(sF45,X3))
| ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sK3)
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3)) )
| ~ spl48_1
| ~ spl48_2 ),
inference(forward_demodulation,[],[f11979,f487]) ).
fof(f11981,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(sK15(X0,sK0,sK1,X2,X3),sK3)
| ~ r2_hidden(X1,X0)
| ~ r2_hidden(X3,sK0)
| r2_hidden(X1,k1_funct_1(sF45,X3))
| ~ m1_subset_1(X2,sF47)
| ~ r2_hidden(X0,a_4_0_closure3(sK0,sK1,X2,X3)) )
| ~ spl48_1
| ~ spl48_2 ),
inference(duplicate_literal_removal,[],[f11980]) ).
fof(f11982,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ r2_hidden(X2,sK0)
| r2_hidden(X0,k1_funct_1(sF45,X2))
| ~ m1_subset_1(sF41,sF47)
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,sF41,X2))
| r2_hidden(sK15(X1,sK0,sK1,sF41,X2),sK2)
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,sF41,X2))
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sF41,k1_zfmisc_1(k1_closure2(sK0,sK1))) )
| ~ spl48_1
| ~ spl48_2 ),
inference(resolution,[],[f11981,f823]) ).
fof(f11985,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ r2_hidden(X2,sK0)
| r2_hidden(X0,k1_funct_1(sF45,X2))
| ~ m1_subset_1(sF41,sF47)
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,sF41,X2))
| r2_hidden(sK15(X1,sK0,sK1,sF41,X2),sK2)
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sF41,k1_zfmisc_1(k1_closure2(sK0,sK1))) )
| ~ spl48_1
| ~ spl48_2 ),
inference(duplicate_literal_removal,[],[f11982]) ).
fof(f11986,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ r2_hidden(X2,sK0)
| r2_hidden(X0,k1_funct_1(sF45,X2))
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,sF41,X2))
| r2_hidden(sK15(X1,sK0,sK1,sF41,X2),sK2)
| ~ m1_pboole(sK1,sK0)
| ~ m1_subset_1(sF41,k1_zfmisc_1(k1_closure2(sK0,sK1))) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f11985,f582]) ).
fof(f11987,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ r2_hidden(X2,sK0)
| r2_hidden(X0,k1_funct_1(sF45,X2))
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,sF41,X2))
| r2_hidden(sK15(X1,sK0,sK1,sF41,X2),sK2)
| ~ m1_subset_1(sF41,k1_zfmisc_1(k1_closure2(sK0,sK1))) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f11986,f287]) ).
fof(f11988,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(sF41,k1_zfmisc_1(sF46))
| ~ r2_hidden(X0,X1)
| ~ r2_hidden(X2,sK0)
| r2_hidden(X0,k1_funct_1(sF45,X2))
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,sF41,X2))
| r2_hidden(sK15(X1,sK0,sK1,sF41,X2),sK2) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(forward_demodulation,[],[f11987,f485]) ).
fof(f11989,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(sF41,sF47)
| ~ r2_hidden(X0,X1)
| ~ r2_hidden(X2,sK0)
| r2_hidden(X0,k1_funct_1(sF45,X2))
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,sF41,X2))
| r2_hidden(sK15(X1,sK0,sK1,sF41,X2),sK2) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(forward_demodulation,[],[f11988,f487]) ).
fof(f11990,plain,
( ! [X2,X0,X1] :
( r2_hidden(sK15(X1,sK0,sK1,sF41,X2),sK2)
| ~ r2_hidden(X2,sK0)
| r2_hidden(X0,k1_funct_1(sF45,X2))
| ~ r2_hidden(X1,a_4_0_closure3(sK0,sK1,sF41,X2))
| ~ r2_hidden(X0,X1) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f11989,f582]) ).
fof(f11991,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(X0,sK0)
| r2_hidden(X1,k1_funct_1(sF45,X0))
| ~ r2_hidden(X2,a_4_0_closure3(sK0,sK1,sF41,X0))
| ~ r2_hidden(X1,X2)
| ~ r2_hidden(X3,X2)
| r2_hidden(X3,k1_funct_1(sF43,X0))
| ~ r2_hidden(X0,sK0)
| ~ m1_subset_1(sF41,sF47)
| ~ r2_hidden(X2,a_4_0_closure3(sK0,sK1,sF41,X0)) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(resolution,[],[f11990,f2636]) ).
fof(f12001,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(X0,sK0)
| r2_hidden(X1,k1_funct_1(sF45,X0))
| ~ r2_hidden(X2,a_4_0_closure3(sK0,sK1,sF41,X0))
| ~ r2_hidden(X1,X2)
| ~ r2_hidden(X3,X2)
| r2_hidden(X3,k1_funct_1(sF43,X0))
| ~ m1_subset_1(sF41,sF47) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(duplicate_literal_removal,[],[f11991]) ).
fof(f12004,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(X2,a_4_0_closure3(sK0,sK1,sF41,X0))
| r2_hidden(X1,k1_funct_1(sF45,X0))
| ~ r2_hidden(X0,sK0)
| ~ r2_hidden(X1,X2)
| ~ r2_hidden(X3,X2)
| r2_hidden(X3,k1_funct_1(sF43,X0)) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f12001,f582]) ).
fof(f12065,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(X3,sK8(a_4_0_closure3(sK0,sK1,sF41,X1),X2))
| ~ r2_hidden(X1,sK0)
| ~ r2_hidden(X0,sK8(a_4_0_closure3(sK0,sK1,sF41,X1),X2))
| r2_hidden(X0,k1_funct_1(sF45,X1))
| r2_hidden(X3,k1_funct_1(sF43,X1))
| ~ r2_hidden(X2,k3_tarski(a_4_0_closure3(sK0,sK1,sF41,X1))) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(resolution,[],[f12004,f467]) ).
fof(f16392,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,sK0)
| ~ r2_hidden(X1,sK8(a_4_0_closure3(sK0,sK1,sF41,X0),X2))
| r2_hidden(X1,k1_funct_1(sF45,X0))
| r2_hidden(X2,k1_funct_1(sF43,X0))
| ~ r2_hidden(X2,k3_tarski(a_4_0_closure3(sK0,sK1,sF41,X0)))
| ~ r2_hidden(X2,k3_tarski(a_4_0_closure3(sK0,sK1,sF41,X0))) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(resolution,[],[f12065,f466]) ).
fof(f16407,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X1,sK8(a_4_0_closure3(sK0,sK1,sF41,X0),X2))
| ~ r2_hidden(X0,sK0)
| r2_hidden(X1,k1_funct_1(sF45,X0))
| r2_hidden(X2,k1_funct_1(sF43,X0))
| ~ r2_hidden(X2,k3_tarski(a_4_0_closure3(sK0,sK1,sF41,X0))) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(duplicate_literal_removal,[],[f16392]) ).
fof(f16410,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sK0)
| r2_hidden(X1,k1_funct_1(sF45,X0))
| r2_hidden(X1,k1_funct_1(sF43,X0))
| ~ r2_hidden(X1,k3_tarski(a_4_0_closure3(sK0,sK1,sF41,X0)))
| ~ r2_hidden(X1,k3_tarski(a_4_0_closure3(sK0,sK1,sF41,X0))) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(resolution,[],[f16407,f466]) ).
fof(f16425,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sK0)
| r2_hidden(X1,k1_funct_1(sF45,X0))
| r2_hidden(X1,k1_funct_1(sF43,X0))
| ~ r2_hidden(X1,k3_tarski(a_4_0_closure3(sK0,sK1,sF41,X0))) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(duplicate_literal_removal,[],[f16410]) ).
fof(f16428,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,k3_tarski(a_4_0_closure3(sK0,sK1,sF41,X0)))
| r2_hidden(X1,k1_funct_1(sF45,X0))
| ~ r2_hidden(X0,sK0) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f16425,f1561]) ).
fof(f16445,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,k1_funct_1(sF42,X0))
| r2_hidden(X1,k1_funct_1(sF45,X0))
| ~ r2_hidden(X0,sK0)
| ~ r2_hidden(X0,sK0) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(superposition,[],[f16428,f1029]) ).
fof(f16446,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,k1_funct_1(sF42,X0))
| r2_hidden(X1,k1_funct_1(sF45,X0))
| ~ r2_hidden(X0,sK0) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(duplicate_literal_removal,[],[f16445]) ).
fof(f16471,plain,
( ! [X0] :
( r2_hidden(sK39(k1_funct_1(sF42,X0),k1_funct_1(sF45,X0)),k1_funct_1(sF45,X0))
| ~ r2_hidden(X0,sK0)
| ~ r2_hidden(X0,sK0)
| k1_funct_1(sF42,X0) = k1_funct_1(sF45,X0) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(resolution,[],[f16446,f10912]) ).
fof(f16473,plain,
( ! [X0] :
( r2_hidden(sK39(k1_funct_1(sF42,X0),k1_funct_1(sF45,X0)),k1_funct_1(sF45,X0))
| ~ r2_hidden(X0,sK0)
| k1_funct_1(sF42,X0) = k1_funct_1(sF45,X0) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(duplicate_literal_removal,[],[f16471]) ).
fof(f16484,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK0)
| k1_funct_1(sF42,X0) = k1_funct_1(sF45,X0)
| k1_funct_1(sF42,X0) = k1_funct_1(sF45,X0)
| ~ r2_hidden(sK39(k1_funct_1(sF42,X0),k1_funct_1(sF45,X0)),k1_funct_1(sF42,X0)) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(resolution,[],[f16473,f452]) ).
fof(f16495,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK0)
| k1_funct_1(sF42,X0) = k1_funct_1(sF45,X0)
| ~ r2_hidden(sK39(k1_funct_1(sF42,X0),k1_funct_1(sF45,X0)),k1_funct_1(sF42,X0)) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(duplicate_literal_removal,[],[f16484]) ).
fof(f16496,plain,
( ! [X0] :
( k1_funct_1(sF42,X0) = k1_funct_1(sF45,X0)
| ~ r2_hidden(X0,sK0) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(forward_subsumption_resolution,[],[f16495,f10912]) ).
fof(f16611,plain,
( ! [X0,X1] :
( k1_funct_1(sF42,sK40(X0,sF45,X1)) != k1_funct_1(X1,sK40(X0,sF45,X1))
| sF45 = X1
| ~ m1_pboole(X1,X0)
| ~ m1_pboole(sF45,X0)
| ~ r2_hidden(sK40(X0,sF45,X1),sK0) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(superposition,[],[f454,f16496]) ).
fof(f16719,definition,
( spl48_91
<=> sF42 = sF45 ),
introduced(definition,[new_symbols(definition,[spl48_91])],[avatar_definition]) ).
fof(f16721,plain,
( sF42 = sF45
| ~ spl48_91 ),
inference(avatar_component_clause,[],[f16719]) ).
fof(f17096,plain,
( ! [X0] :
( sF42 = sF45
| ~ m1_pboole(sF42,X0)
| ~ m1_pboole(sF45,X0)
| ~ r2_hidden(sK40(X0,sF45,sF42),sK0) )
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(equality_resolution,[],[f16611]) ).
fof(f17105,definition,
( spl48_114
<=> ! [X0] :
( ~ m1_pboole(sF42,X0)
| ~ r2_hidden(sK40(X0,sF45,sF42),sK0)
| ~ m1_pboole(sF45,X0) ) ),
introduced(definition,[new_symbols(definition,[spl48_114])],[avatar_definition]) ).
fof(f17106,plain,
( ! [X0] :
( ~ r2_hidden(sK40(X0,sF45,sF42),sK0)
| ~ m1_pboole(sF42,X0)
| ~ m1_pboole(sF45,X0) )
| ~ spl48_114 ),
inference(avatar_component_clause,[],[f17105]) ).
fof(f17107,plain,
( spl48_114
| spl48_91
| ~ spl48_1
| ~ spl48_2
| ~ spl48_5 ),
inference(avatar_split_clause,[],[f17096,f581,f527,f523,f16719,f17105]) ).
fof(f17110,plain,
( ~ m1_pboole(sF42,sK0)
| ~ m1_pboole(sF45,sK0)
| sF42 = sF45
| ~ m1_pboole(sF42,sK0)
| ~ m1_pboole(sF45,sK0)
| ~ spl48_114 ),
inference(resolution,[],[f17106,f453]) ).
fof(f17111,plain,
( ~ m1_pboole(sF42,sK0)
| ~ m1_pboole(sF45,sK0)
| sF42 = sF45
| ~ spl48_114 ),
inference(duplicate_literal_removal,[],[f17110]) ).
fof(f17112,plain,
( ~ m1_pboole(sF45,sK0)
| sF42 = sF45
| ~ spl48_4
| ~ spl48_114 ),
inference(forward_subsumption_resolution,[],[f17111,f1032]) ).
fof(f17113,plain,
( sF42 = sF45
| ~ spl48_3
| ~ spl48_4
| ~ spl48_114 ),
inference(forward_subsumption_resolution,[],[f17112,f533]) ).
fof(f17114,plain,
( spl48_91
| ~ spl48_3
| ~ spl48_4
| ~ spl48_114 ),
inference(avatar_split_clause,[],[f17113,f17105,f577,f531,f16719]) ).
fof(f17116,plain,
( ~ r6_pboole(sK0,sF42,sF42)
| ~ spl48_91 ),
inference(backward_demodulation,[],[f483,f16721]) ).
fof(f18148,plain,
( $false
| ~ spl48_4
| ~ spl48_91 ),
inference(forward_subsumption_resolution,[],[f17116,f1062]) ).
fof(f18149,plain,
( ~ spl48_4
| ~ spl48_91 ),
inference(avatar_contradiction_clause,[],[f18148]) ).
cnf(s1,plain,
( ~ spl48_1
| ~ spl48_2
| spl48_3 ),
inference(sat_conversion,[],[f534]) ).
cnf(s2,plain,
( spl48_4
| ~ spl48_5 ),
inference(sat_conversion,[],[f584]) ).
cnf(s6,plain,
spl48_2,
inference(sat_conversion,[],[f716]) ).
cnf(s8,plain,
spl48_1,
inference(sat_conversion,[],[f718]) ).
cnf(s15,plain,
spl48_5,
inference(sat_conversion,[],[f1028]) ).
cnf(s132,plain,
( ~ spl48_1
| ~ spl48_2
| ~ spl48_5
| spl48_91
| spl48_114 ),
inference(sat_conversion,[],[f17107]) ).
cnf(s133,plain,
( ~ spl48_3
| ~ spl48_4
| spl48_91
| ~ spl48_114 ),
inference(sat_conversion,[],[f17114]) ).
cnf(s138,plain,
( ~ spl48_4
| ~ spl48_91 ),
inference(sat_conversion,[],[f18149]) ).
cnf(s148,plain,
spl48_4,
inference(rat,[],[s2,s15]) ).
cnf(s149,plain,
~ spl48_91,
inference(rat,[],[s138,s148]) ).
cnf(s150,plain,
spl48_114,
inference(rat,[],[s132,s6,s8,s15,s149]) ).
cnf(s151,plain,
~ spl48_3,
inference(rat,[],[s133,s148,s149,s150]) ).
cnf(s152,plain,
$false,
inference(rat,[],[s1,s151,s6,s8]) ).
fof(f18304,plain,
$false,
inference(avatar_sat_refutation,[],[s152]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG230+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n016.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 19:59:03 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.25/2.41 % (3930166)Detected formulas, will run a generic FOF schedule.
% 12.25/2.41 % (3930369)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=2049048465:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.25/2.41 % (3930372)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1183562531:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.25/2.41 % (3930371)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4045881683:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.25/2.41 % (3930367)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=4204211063:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.25/2.41 % (3930366)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=574170654:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.25/2.41 % (3930371)Refutation not found, incomplete strategy
% 12.25/2.41 % (3930371)------------------------------
% 12.25/2.41 % (3930371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.25/2.41 % (3930371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.25/2.41 % (3930371)CaDiCaL version: 2.1.3
% 12.25/2.41 % (3930371)Termination reason: Refutation not found, incomplete strategy
% 12.25/2.41 % (3930371)Time elapsed: 0.003 s
% 12.25/2.41 % (3930371)Peak memory usage: 88 MB
% 12.25/2.41 % (3930371)Instructions burned: 3 (million)
% 12.25/2.41 % (3930374)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=950840862:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.25/2.41 % (3930376)dis-21_1_sil=8000:lcm=predicate:random_seed=3237968428:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 12.25/2.41 % (3930372)Instruction limit reached!
% 12.25/2.41 % (3930372)------------------------------
% 12.25/2.41 % (3930372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.25/2.41 % (3930372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.25/2.41 % (3930372)CaDiCaL version: 2.1.3
% 12.25/2.41 % (3930372)Termination reason: Instruction limit
% 12.25/2.41 % (3930372)Termination phase: Saturation
% 12.25/2.41 % (3930372)Time elapsed: 0.073 s
% 12.25/2.41 % (3930372)Peak memory usage: 88 MB
% 12.25/2.41 % (3930372)Instructions burned: 120 (million)
% 12.25/2.41 % (3930376)Instruction limit reached!
% 12.25/2.41 % (3930376)------------------------------
% 12.25/2.41 % (3930376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.25/2.41 % (3930376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.25/2.41 % (3930376)CaDiCaL version: 2.1.3
% 12.25/2.41 % (3930376)Termination reason: Instruction limit
% 12.25/2.41 % (3930376)Termination phase: Saturation
% 12.25/2.41 % (3930376)Time elapsed: 0.078 s
% 12.25/2.41 % (3930376)Peak memory usage: 90 MB
% 12.25/2.41 % (3930376)Instructions burned: 130 (million)
% 12.25/2.41 % (3930374)Instruction limit reached!
% 12.25/2.41 % (3930374)------------------------------
% 12.25/2.41 % (3930374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.25/2.41 % (3930374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.25/2.41 % (3930374)CaDiCaL version: 2.1.3
% 12.25/2.41 % (3930374)Termination reason: Instruction limit
% 12.25/2.41 % (3930374)Termination phase: Saturation
% 12.25/2.41 % (3930374)Time elapsed: 0.098 s
% 12.25/2.41 % (3930374)Peak memory usage: 90 MB
% 12.25/2.41 % (3930374)Instructions burned: 140 (million)
% 12.25/2.41 % (3930474)lrs+10_1_sil=8000:sp=occurrence:random_seed=2886480910:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.25/2.41 % (3930371)------------------------------
% 12.25/2.41 % (3930371)------------------------------
% 12.25/2.41 % (3930491)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1045185880:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.25/2.41 % (3930503)lrs+1011_1_sil=32000:sp=occurrence:random_seed=220910925:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 12.25/2.41 % (3930491)Instruction limit reached!
% 12.25/2.41 % (3930491)------------------------------
% 12.25/2.41 % (3930491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.72 % (3930491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.98/3.72 % (3930491)CaDiCaL version: 2.1.3
% 20.98/3.72 % (3930491)Termination reason: Instruction limit
% 20.98/3.72 % (3930491)Termination phase: Saturation
% 20.98/3.72 % (3930491)Time elapsed: 0.077 s
% 20.98/3.72 % (3930491)Peak memory usage: 89 MB
% 20.98/3.72 % (3930491)Instructions burned: 159 (million)
% 20.98/3.72 % (3930577)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=1845962892:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 20.98/3.72 % (3930474)Instruction limit reached!
% 20.98/3.72 % (3930474)------------------------------
% 20.98/3.72 % (3930474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.72 % (3930474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.98/3.72 % (3930474)CaDiCaL version: 2.1.3
% 20.98/3.72 % (3930474)Termination reason: Instruction limit
% 20.98/3.72 % (3930474)Termination phase: Saturation
% 20.98/3.72 % (3930474)Time elapsed: 0.185 s
% 20.98/3.72 % (3930474)Peak memory usage: 92 MB
% 20.98/3.72 % (3930474)Instructions burned: 286 (million)
% 20.98/3.72 % (3930503)Instruction limit reached!
% 20.98/3.72 % (3930503)------------------------------
% 20.98/3.72 % (3930503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.72 % (3930503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.98/3.72 % (3930503)CaDiCaL version: 2.1.3
% 20.98/3.72 % (3930503)Termination reason: Instruction limit
% 20.98/3.72 % (3930503)Termination phase: Saturation
% 20.98/3.72 % (3930503)Time elapsed: 0.213 s
% 20.98/3.72 % (3930503)Peak memory usage: 93 MB
% 20.98/3.72 % (3930503)Instructions burned: 326 (million)
% 20.98/3.72 % (3930624)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3696488426:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 20.98/3.72 % (3930624)Refutation not found, incomplete strategy
% 20.98/3.72 % (3930624)------------------------------
% 20.98/3.72 % (3930624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.72 % (3930624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.98/3.72 % (3930624)CaDiCaL version: 2.1.3
% 20.98/3.72 % (3930624)Termination reason: Refutation not found, incomplete strategy
% 20.98/3.72 % (3930624)Time elapsed: 0.006 s
% 20.98/3.72 % (3930624)Peak memory usage: 89 MB
% 20.98/3.72 % (3930624)Instructions burned: 9 (million)
% 20.98/3.72 % (3930577)Instruction limit reached!
% 20.98/3.72 % (3930577)------------------------------
% 20.98/3.72 % (3930577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.72 % (3930577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.98/3.72 % (3930577)CaDiCaL version: 2.1.3
% 20.98/3.72 % (3930577)Termination reason: Instruction limit
% 20.98/3.72 % (3930577)Termination phase: Saturation
% 20.98/3.72 % (3930577)Time elapsed: 0.143 s
% 20.98/3.72 % (3930577)Peak memory usage: 92 MB
% 20.98/3.72 % (3930577)Instructions burned: 249 (million)
% 20.98/3.72 % (3930665)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3300944590:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 20.98/3.72 % (3930710)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=925678595:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 20.98/3.72 % (3930742)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3607194145:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 20.98/3.72 % (3930710)Instruction limit reached!
% 20.98/3.72 % (3930710)------------------------------
% 20.98/3.72 % (3930710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.72 % (3930710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.98/3.72 % (3930710)CaDiCaL version: 2.1.3
% 20.98/3.72 % (3930710)Termination reason: Instruction limit
% 20.98/3.72 % (3930710)Termination phase: Saturation
% 20.98/3.72 % (3930710)Time elapsed: 0.076 s
% 20.98/3.72 % (3930710)Peak memory usage: 91 MB
% 20.98/3.72 % (3930710)Instructions burned: 113 (million)
% 20.98/3.72 % (3930624)------------------------------
% 20.98/3.72 % (3930624)------------------------------
% 20.98/3.72 % (3930742)Instruction limit reached!
% 20.98/3.72 % (3930742)------------------------------
% 20.98/3.72 % (3930742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.72 % (3930742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.23/7.35 % (3930742)CaDiCaL version: 2.1.3
% 47.23/7.35 % (3930742)Termination reason: Instruction limit
% 47.23/7.35 % (3930742)Termination phase: Saturation
% 47.23/7.35 % (3930742)Time elapsed: 0.068 s
% 47.23/7.35 % (3930742)Peak memory usage: 89 MB
% 47.23/7.35 % (3930742)Instructions burned: 127 (million)
% 47.23/7.35 % (3930835)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1861842330:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 47.23/7.35 % (3930856)lrs+10_1_sil=8000:sp=occurrence:random_seed=710712217:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 47.23/7.35 % (3930866)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=96826747:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 47.23/7.35 % (3930866)Refutation not found, incomplete strategy
% 47.23/7.35 % (3930866)------------------------------
% 47.23/7.35 % (3930866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.23/7.35 % (3930866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.23/7.35 % (3930866)CaDiCaL version: 2.1.3
% 47.23/7.35 % (3930866)Termination reason: Refutation not found, incomplete strategy
% 47.23/7.35 % (3930866)Time elapsed: 0.009 s
% 47.23/7.35 % (3930866)Peak memory usage: 89 MB
% 47.23/7.35 % (3930866)Instructions burned: 13 (million)
% 47.23/7.35 % (3930835)Instruction limit reached!
% 47.23/7.35 % (3930835)------------------------------
% 47.23/7.35 % (3930835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.23/7.35 % (3930835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.23/7.35 % (3930835)CaDiCaL version: 2.1.3
% 47.23/7.35 % (3930835)Termination reason: Instruction limit
% 47.23/7.35 % (3930835)Termination phase: Saturation
% 47.23/7.35 % (3930835)Time elapsed: 0.071 s
% 47.23/7.35 % (3930835)Peak memory usage: 89 MB
% 47.23/7.35 % (3930835)Instructions burned: 114 (million)
% 47.23/7.35 % (3930959)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2131507517:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 47.23/7.35 % (3930866)------------------------------
% 47.23/7.35 % (3930866)------------------------------
% 47.23/7.35 % (3931088)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3684856664:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 47.23/7.35 % (3931088)Instruction limit reached!
% 47.23/7.35 % (3931088)------------------------------
% 47.23/7.35 % (3931088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.23/7.35 % (3931088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.23/7.35 % (3931088)CaDiCaL version: 2.1.3
% 47.23/7.35 % (3931088)Termination reason: Instruction limit
% 47.23/7.35 % (3931088)Termination phase: Saturation
% 47.23/7.35 % (3931088)Time elapsed: 0.075 s
% 47.23/7.35 % (3931088)Peak memory usage: 91 MB
% 47.23/7.35 % (3931088)Instructions burned: 136 (million)
% 47.23/7.35 % (3930856)Instruction limit reached!
% 47.23/7.35 % (3930856)------------------------------
% 47.23/7.35 % (3930856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.23/7.35 % (3930856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.23/7.35 % (3930856)CaDiCaL version: 2.1.3
% 47.23/7.35 % (3930856)Termination reason: Instruction limit
% 47.23/7.35 % (3930856)Termination phase: Saturation
% 47.23/7.35 % (3930856)Time elapsed: 0.524 s
% 47.23/7.35 % (3930856)Peak memory usage: 98 MB
% 47.23/7.35 % (3930856)Instructions burned: 908 (million)
% 47.23/7.35 % (3931209)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1496865958:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 47.23/7.35 % (3931209)Refutation not found, incomplete strategy
% 47.23/7.35 % (3931209)------------------------------
% 47.23/7.35 % (3931209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.23/7.35 % (3931209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.23/7.35 % (3931209)CaDiCaL version: 2.1.3
% 47.23/7.35 % (3931209)Termination reason: Refutation not found, incomplete strategy
% 47.23/7.35 % (3931209)Time elapsed: 0.008 s
% 47.23/7.35 % (3931209)Peak memory usage: 89 MB
% 47.23/7.35 % (3931209)Instructions burned: 12 (million)
% 47.23/7.35 % (3931233)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=143059988:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 52.70/8.12 % (3931209)------------------------------
% 52.70/8.12 % (3931209)------------------------------
% 52.70/8.12 % (3931407)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=3047861846:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 52.70/8.12 % (3931407)Instruction limit reached!
% 52.70/8.12 % (3931407)------------------------------
% 52.70/8.12 % (3931407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.70/8.12 % (3931407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.70/8.12 % (3931407)CaDiCaL version: 2.1.3
% 52.70/8.12 % (3931407)Termination reason: Instruction limit
% 52.70/8.12 % (3931407)Termination phase: Saturation
% 52.70/8.12 % (3931407)Time elapsed: 0.084 s
% 52.70/8.12 % (3931407)Peak memory usage: 90 MB
% 52.70/8.12 % (3931407)Instructions burned: 126 (million)
% 52.70/8.12 % (3930665)Instruction limit reached!
% 52.70/8.12 % (3930665)------------------------------
% 52.70/8.12 % (3930665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.70/8.12 % (3930665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.70/8.12 % (3930665)CaDiCaL version: 2.1.3
% 52.70/8.12 % (3930665)Termination reason: Instruction limit
% 52.70/8.12 % (3930665)Termination phase: Saturation
% 52.70/8.12 % (3930665)Time elapsed: 1.506 s
% 52.70/8.12 % (3930665)Peak memory usage: 142 MB
% 52.70/8.12 % (3930665)Instructions burned: 2351 (million)
% 52.70/8.12 % (3931530)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1421708979:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 52.70/8.12 % (3931557)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1727981117:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi)
% 52.70/8.12 % (3931530)Instruction limit reached!
% 52.70/8.12 % (3931530)------------------------------
% 52.70/8.12 % (3931530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.70/8.12 % (3931530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.70/8.12 % (3931530)CaDiCaL version: 2.1.3
% 52.70/8.12 % (3931530)Termination reason: Instruction limit
% 52.70/8.12 % (3931530)Termination phase: Saturation
% 52.70/8.12 % (3931530)Time elapsed: 0.090 s
% 52.70/8.12 % (3931530)Peak memory usage: 90 MB
% 52.70/8.12 % (3931530)Instructions burned: 134 (million)
% 52.70/8.12 % (3931557)Instruction limit reached!
% 52.70/8.12 % (3931557)------------------------------
% 52.70/8.12 % (3931557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.70/8.12 % (3931557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.70/8.12 % (3931557)CaDiCaL version: 2.1.3
% 52.70/8.12 % (3931557)Termination reason: Instruction limit
% 52.70/8.12 % (3931557)Termination phase: Saturation
% 52.70/8.12 % (3931557)Time elapsed: 0.075 s
% 52.70/8.12 % (3931557)Peak memory usage: 91 MB
% 52.70/8.12 % (3931557)Instructions burned: 141 (million)
% 52.70/8.12 % (3931647)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2747631806:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/431Mi)
% 52.70/8.12 % (3931673)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=2961180066:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 52.70/8.12 % (3931647)Instruction limit reached!
% 52.70/8.12 % (3931647)------------------------------
% 52.70/8.12 % (3931647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.70/8.12 % (3931647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.70/8.12 % (3931647)CaDiCaL version: 2.1.3
% 52.70/8.12 % (3931647)Termination reason: Instruction limit
% 52.70/8.12 % (3931647)Termination phase: Saturation
% 52.70/8.12 % (3931647)Time elapsed: 0.258 s
% 52.70/8.12 % (3931647)Peak memory usage: 94 MB
% 52.70/8.12 % (3931647)Instructions burned: 431 (million)
% 52.70/8.12 % (3931847)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=2052374474:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2971 on theBenchmark for (2971ds/150Mi)
% 52.70/8.12 % (3931847)Instruction limit reached!
% 52.70/8.12 % (3931847)------------------------------
% 52.70/8.12 % (3931847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.70/8.12 % (3931847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.70/8.12 % (3931847)CaDiCaL version: 2.1.3
% 52.70/8.12 % (3931847)Termination reason: Instruction limit
% 52.70/8.12 % (3931847)Termination phase: Saturation
% 52.70/8.12 % (3931847)Time elapsed: 0.094 s
% 52.70/8.12 % (3931847)Peak memory usage: 91 MB
% 52.70/8.12 % (3931847)Instructions burned: 151 (million)
% 52.70/8.12 % (3931966)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1655801657:i=14155:bd=all_2969 on theBenchmark for (2969ds/14155Mi)
% 52.70/8.12 % (3930959)Instruction limit reached!
% 52.70/8.12 % (3930959)------------------------------
% 52.70/8.12 % (3930959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.70/8.12 % (3930959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.70/8.12 % (3930959)CaDiCaL version: 2.1.3
% 52.70/8.12 % (3930959)Termination reason: Instruction limit
% 52.70/8.12 % (3930959)Termination phase: Saturation
% 52.70/8.12 % (3930959)Time elapsed: 3.141 s
% 52.70/8.12 % (3930959)Peak memory usage: 162 MB
% 52.70/8.12 % (3930959)Instructions burned: 5203 (million)
% 52.70/8.12 % (3932629)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2770187783:i=667:av=off:fsr=off_2956 on theBenchmark for (2956ds/667Mi)
% 52.70/8.12 % (3932629)Instruction limit reached!
% 52.70/8.12 % (3932629)------------------------------
% 52.70/8.12 % (3932629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.70/8.12 % (3932629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.70/8.12 % (3932629)CaDiCaL version: 2.1.3
% 52.70/8.12 % (3932629)Termination reason: Instruction limit
% 52.70/8.12 % (3932629)Termination phase: Saturation
% 52.70/8.12 % (3932629)Time elapsed: 0.328 s
% 52.70/8.12 % (3932629)Peak memory usage: 104 MB
% 52.70/8.12 % (3932629)Instructions burned: 668 (million)
% 52.70/8.12 % (3932865)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3953814085:s2a=on:i=185:s2at=1.8:fdi=4_2951 on theBenchmark for (2951ds/185Mi)
% 52.70/8.12 % (3932865)Instruction limit reached!
% 52.70/8.12 % (3932865)------------------------------
% 52.70/8.12 % (3932865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.70/8.12 % (3932865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.70/8.12 % (3932865)CaDiCaL version: 2.1.3
% 52.70/8.12 % (3932865)Termination reason: Instruction limit
% 52.70/8.12 % (3932865)Termination phase: Saturation
% 52.70/8.12 % (3932865)Time elapsed: 0.103 s
% 52.70/8.12 % (3932865)Peak memory usage: 91 MB
% 52.70/8.12 % (3932865)Instructions burned: 186 (million)
% 52.70/8.12 % (3932989)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=340711963:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2948 on theBenchmark for (2948ds/193Mi)
% 52.70/8.12 % (3932989)Instruction limit reached!
% 52.70/8.12 % (3932989)------------------------------
% 52.70/8.12 % (3932989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.70/8.12 % (3932989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.70/8.12 % (3932989)CaDiCaL version: 2.1.3
% 52.70/8.12 % (3932989)Termination reason: Instruction limit
% 52.70/8.12 % (3932989)Termination phase: Saturation
% 52.70/8.12 % (3932989)Time elapsed: 0.126 s
% 52.70/8.12 % (3932989)Peak memory usage: 91 MB
% 52.70/8.12 % (3932989)Instructions burned: 194 (million)
% 52.70/8.12 % (3933087)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=453905620:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2946 on theBenchmark for (2946ds/4850Mi)
% 52.70/8.12 % (3931673)Instruction limit reached!
% 52.70/8.12 % (3931673)------------------------------
% 52.70/8.12 % (3931673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.70/8.12 % (3931673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.70/8.12 % (3931673)CaDiCaL version: 2.1.3
% 52.70/8.12 % (3931673)Termination reason: Instruction limit
% 52.70/8.12 % (3931673)Termination phase: Saturation
% 52.70/8.12 % (3931673)Time elapsed: 3.915 s
% 52.70/8.12 % (3931673)Peak memory usage: 167 MB
% 52.70/8.12 % (3931673)Instructions burned: 6061 (million)
% 52.70/8.12 % (3933219)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1999656068:i=12111:sd=1:ss=included_2934 on theBenchmark for (2934ds/12111Mi)
% 52.70/8.12 % (3931966)First to succeed.
% 52.70/8.12 % (3931966)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3930166"
% 52.70/8.12 % (3931966)Refutation found. Thanks to Tanya!
% 52.70/8.12 % SZS status Theorem for theBenchmark
% 52.70/8.12 % SZS output start Proof for theBenchmark
% See solution above
% 53.16/8.25 % (3931966)------------------------------
% 53.16/8.25 % (3931966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.16/8.25 % (3931966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.16/8.25 % (3931966)CaDiCaL version: 2.1.3
% 53.16/8.25 % (3931966)Termination reason: Refutation
% 53.16/8.25 % (3931966)Time elapsed: 3.957 s
% 53.16/8.25 % (3931966)Peak memory usage: 172 MB
% 53.16/8.25 % (3931966)Instructions burned: 6373 (million)
% 53.16/8.25 % (3931966)------------------------------
% 53.16/8.25 % (3931966)------------------------------
% 53.16/8.25 % (3930166)Success in time 7.442 s
% 53.16/8.25 % Vampire exiting
%------------------------------------------------------------------------------