%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU425+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:48:56 PM UTC 2026
% Result : Theorem 7.37s 4.52s
% Output : Refutation 0.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 30
% Syntax : Number of formulae : 210 ( 33 unt; 9 def)
% Number of atoms : 696 ( 134 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 839 ( 353 ~; 360 |; 88 &)
% ( 13 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 10 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-3 aty)
% Number of variables : 237 ( 0 sgn 229 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f438,axiom,
! [X0,X1] :
( k2_zfmisc_1(X0,X1) = k1_xboole_0
<=> ( X0 = k1_xboole_0
| X1 = k1_xboole_0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t113_zfmisc_1) ).
fof(f442,axiom,
! [X0,X1,X2] :
~ ( X0 != k1_xboole_0
& ( r1_tarski(k2_zfmisc_1(X1,X0),k2_zfmisc_1(X2,X0))
| r1_tarski(k2_zfmisc_1(X0,X1),k2_zfmisc_1(X0,X2)) )
& ~ r1_tarski(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t117_zfmisc_1) ).
fof(f443,axiom,
! [X0,X1,X2] :
( r1_tarski(X0,X1)
=> ( r1_tarski(k2_zfmisc_1(X0,X2),k2_zfmisc_1(X1,X2))
& r1_tarski(k2_zfmisc_1(X2,X0),k2_zfmisc_1(X2,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t118_zfmisc_1) ).
fof(f460,axiom,
! [X0,X1] :
( ( r1_tarski(X0,k2_zfmisc_1(X0,X1))
| r1_tarski(X0,k2_zfmisc_1(X1,X0)) )
=> X0 = k1_xboole_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t135_zfmisc_1) ).
fof(f703,axiom,
! [X0,X1] : v1_relat_1(k2_zfmisc_1(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_relat_1) ).
fof(f722,axiom,
! [X0] :
( v1_relat_1(X0)
=> r1_tarski(X0,k2_zfmisc_1(k1_relat_1(X0),k2_relat_1(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_relat_1) ).
fof(f764,axiom,
( k1_relat_1(k1_xboole_0) = k1_xboole_0
& k2_relat_1(k1_xboole_0) = k1_xboole_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t60_relat_1) ).
fof(f768,axiom,
! [X0] :
( v1_relat_1(X0)
=> ( ( k1_relat_1(X0) = k1_xboole_0
| k2_relat_1(X0) = k1_xboole_0 )
=> X0 = k1_xboole_0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t64_relat_1) ).
fof(f949,axiom,
! [X0,X1] :
~ ( ~ ( X0 = k1_xboole_0
& X1 != k1_xboole_0 )
& ! [X2] :
( ( v1_relat_1(X2)
& v1_funct_1(X2) )
=> ~ ( X1 = k1_relat_1(X2)
& r1_tarski(k2_relat_1(X2),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_funct_1) ).
fof(f1333,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f1345,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( ( r1_tarski(k1_relat_1(X2),X0)
& r1_tarski(k2_relat_1(X2),X1) )
=> m2_relset_1(X2,X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_relset_1) ).
fof(f1346,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> ( r1_tarski(k1_relat_1(X2),X0)
& r1_tarski(k2_relat_1(X2),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_relset_1) ).
fof(f1451,axiom,
! [X0] :
( ( v1_relat_1(X0)
& v1_funct_1(X0) )
=> ( v1_funct_1(X0)
& m2_relset_1(X0,k1_relat_1(X0),k2_relat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t24_partfun1) ).
fof(f1818,axiom,
! [X0] :
( ( v1_relat_1(X0)
& v1_funct_1(X0) )
=> ( v1_funct_1(X0)
& v1_funct_2(X0,k1_relat_1(X0),k2_relat_1(X0))
& m2_relset_1(X0,k1_relat_1(X0),k2_relat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_funct_2) ).
fof(f1819,axiom,
! [X0,X1] :
( ( v1_relat_1(X1)
& v1_funct_1(X1) )
=> ( r1_tarski(k2_relat_1(X1),X0)
=> ( v1_funct_1(X1)
& v1_funct_2(X1,k1_relat_1(X1),X0)
& m2_relset_1(X1,k1_relat_1(X1),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_funct_2) ).
fof(f1823,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
=> ( r1_tarski(k2_relat_1(X3),X2)
=> ( ( X1 = k1_xboole_0
& X0 != k1_xboole_0 )
| ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X2)
& m2_relset_1(X3,X0,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_funct_2) ).
fof(f5709,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( r1_tarski(X2,k2_zfmisc_1(X0,X1))
=> ( r1_tarski(k1_relat_1(X2),X0)
& r1_tarski(k2_relat_1(X2),X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_sysrel) ).
fof(f19060,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> ( v1_relat_1(k5_relset_2(X0,X1))
& v1_funct_1(k5_relset_2(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_relset_2) ).
fof(f19088,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> ! [X2] :
( ( v1_relat_1(X2)
& v1_funct_1(X2) )
=> ( X2 = k5_relset_2(X0,X1)
<=> ( k1_relat_1(X2) = k1_zfmisc_1(X0)
& ! [X3] :
( r1_tarski(X3,X0)
=> k1_funct_1(X2,X3) = k9_relat_1(X1,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_relset_2) ).
fof(f19090,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> r1_tarski(k2_relat_1(k5_relset_2(X0,X2)),k1_zfmisc_1(k2_relat_1(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t20_relset_2) ).
fof(f19091,conjecture,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ( v1_funct_1(k5_relset_2(X0,X2))
& v1_funct_2(k5_relset_2(X0,X2),k1_zfmisc_1(X0),k1_zfmisc_1(k2_relat_1(X2)))
& m2_relset_1(k5_relset_2(X0,X2),k1_zfmisc_1(X0),k1_zfmisc_1(k2_relat_1(X2))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_relset_2) ).
fof(f19092,negated_conjecture,
~ ! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ( v1_funct_1(k5_relset_2(X0,X2))
& v1_funct_2(k5_relset_2(X0,X2),k1_zfmisc_1(X0),k1_zfmisc_1(k2_relat_1(X2)))
& m2_relset_1(k5_relset_2(X0,X2),k1_zfmisc_1(X0),k1_zfmisc_1(k2_relat_1(X2))) ) ),
inference(negated_conjecture,[status(cth)],[f19091]) ).
fof(f19095,plain,
? [X0,X1,X2] :
( ( ~ v1_funct_1(k5_relset_2(X0,X2))
| ~ v1_funct_2(k5_relset_2(X0,X2),k1_zfmisc_1(X0),k1_zfmisc_1(k2_relat_1(X2)))
| ~ m2_relset_1(k5_relset_2(X0,X2),k1_zfmisc_1(X0),k1_zfmisc_1(k2_relat_1(X2))) )
& m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f19092]) ).
fof(f19097,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1333]) ).
fof(f19103,plain,
! [X0,X1] :
( X0 = k1_xboole_0
| ( ~ r1_tarski(X0,k2_zfmisc_1(X0,X1))
& ~ r1_tarski(X0,k2_zfmisc_1(X1,X0)) ) ),
inference(ennf_transformation,[],[f460]) ).
fof(f19108,plain,
! [X0,X1,X2] :
( ( r1_tarski(k2_zfmisc_1(X0,X2),k2_zfmisc_1(X1,X2))
& r1_tarski(k2_zfmisc_1(X2,X0),k2_zfmisc_1(X2,X1)) )
| ~ r1_tarski(X0,X1) ),
inference(ennf_transformation,[],[f443]) ).
fof(f19109,plain,
! [X0,X1,X2] :
( k1_xboole_0 = X0
| ( ~ r1_tarski(k2_zfmisc_1(X1,X0),k2_zfmisc_1(X2,X0))
& ~ r1_tarski(k2_zfmisc_1(X0,X1),k2_zfmisc_1(X0,X2)) )
| r1_tarski(X1,X2) ),
inference(ennf_transformation,[],[f442]) ).
fof(f19114,plain,
! [X0,X1,X2] :
( ( r1_tarski(k1_relat_1(X2),X0)
& r1_tarski(k2_relat_1(X2),X1) )
| ~ r1_tarski(X2,k2_zfmisc_1(X0,X1))
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f5709]) ).
fof(f19115,plain,
! [X0,X1,X2] :
( ( r1_tarski(k1_relat_1(X2),X0)
& r1_tarski(k2_relat_1(X2),X1) )
| ~ r1_tarski(X2,k2_zfmisc_1(X0,X1))
| ~ v1_relat_1(X2) ),
inference(flattening,[],[f19114]) ).
fof(f19125,plain,
! [X0,X1,X2,X3] :
( ( X1 = k1_xboole_0
& X0 != k1_xboole_0 )
| ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X2)
& m2_relset_1(X3,X0,X2) )
| ~ r1_tarski(k2_relat_1(X3),X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(ennf_transformation,[],[f1823]) ).
fof(f19126,plain,
! [X0,X1,X2,X3] :
( ( X1 = k1_xboole_0
& X0 != k1_xboole_0 )
| ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X2)
& m2_relset_1(X3,X0,X2) )
| ~ r1_tarski(k2_relat_1(X3),X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(flattening,[],[f19125]) ).
fof(f19129,plain,
! [X0,X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,k1_relat_1(X1),X0)
& m2_relset_1(X1,k1_relat_1(X1),X0) )
| ~ r1_tarski(k2_relat_1(X1),X0)
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(ennf_transformation,[],[f1819]) ).
fof(f19130,plain,
! [X0,X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,k1_relat_1(X1),X0)
& m2_relset_1(X1,k1_relat_1(X1),X0) )
| ~ r1_tarski(k2_relat_1(X1),X0)
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(flattening,[],[f19129]) ).
fof(f19131,plain,
! [X0] :
( ( v1_funct_1(X0)
& v1_funct_2(X0,k1_relat_1(X0),k2_relat_1(X0))
& m2_relset_1(X0,k1_relat_1(X0),k2_relat_1(X0)) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(ennf_transformation,[],[f1818]) ).
fof(f19132,plain,
! [X0] :
( ( v1_funct_1(X0)
& v1_funct_2(X0,k1_relat_1(X0),k2_relat_1(X0))
& m2_relset_1(X0,k1_relat_1(X0),k2_relat_1(X0)) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(flattening,[],[f19131]) ).
fof(f19139,plain,
! [X0] :
( ( v1_funct_1(X0)
& m2_relset_1(X0,k1_relat_1(X0),k2_relat_1(X0)) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(ennf_transformation,[],[f1451]) ).
fof(f19140,plain,
! [X0] :
( ( v1_funct_1(X0)
& m2_relset_1(X0,k1_relat_1(X0),k2_relat_1(X0)) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(flattening,[],[f19139]) ).
fof(f19143,plain,
! [X0,X1,X2] :
( ( r1_tarski(k1_relat_1(X2),X0)
& r1_tarski(k2_relat_1(X2),X1) )
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1346]) ).
fof(f19144,plain,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
| ~ r1_tarski(k1_relat_1(X2),X0)
| ~ r1_tarski(k2_relat_1(X2),X1)
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f1345]) ).
fof(f19145,plain,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
| ~ r1_tarski(k1_relat_1(X2),X0)
| ~ r1_tarski(k2_relat_1(X2),X1)
| ~ v1_relat_1(X2) ),
inference(flattening,[],[f19144]) ).
fof(f19152,plain,
! [X0,X1] :
( ( X0 = k1_xboole_0
& X1 != k1_xboole_0 )
| ? [X2] :
( X1 = k1_relat_1(X2)
& r1_tarski(k2_relat_1(X2),X0)
& v1_relat_1(X2)
& v1_funct_1(X2) ) ),
inference(ennf_transformation,[],[f949]) ).
fof(f19153,plain,
! [X0,X1] :
( ( X0 = k1_xboole_0
& X1 != k1_xboole_0 )
| ? [X2] :
( X1 = k1_relat_1(X2)
& r1_tarski(k2_relat_1(X2),X0)
& v1_relat_1(X2)
& v1_funct_1(X2) ) ),
inference(flattening,[],[f19152]) ).
fof(f19159,plain,
! [X0] :
( X0 = k1_xboole_0
| ( k1_xboole_0 != k1_relat_1(X0)
& k1_xboole_0 != k2_relat_1(X0) )
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f768]) ).
fof(f19160,plain,
! [X0] :
( X0 = k1_xboole_0
| ( k1_xboole_0 != k1_relat_1(X0)
& k1_xboole_0 != k2_relat_1(X0) )
| ~ v1_relat_1(X0) ),
inference(flattening,[],[f19159]) ).
fof(f19163,plain,
! [X0] :
( r1_tarski(X0,k2_zfmisc_1(k1_relat_1(X0),k2_relat_1(X0)))
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f722]) ).
fof(f19171,plain,
! [X0,X1,X2] :
( r1_tarski(k2_relat_1(k5_relset_2(X0,X2)),k1_zfmisc_1(k2_relat_1(X2)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f19090]) ).
fof(f19174,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = k5_relset_2(X0,X1)
<=> ( k1_relat_1(X2) = k1_zfmisc_1(X0)
& ! [X3] :
( k1_funct_1(X2,X3) = k9_relat_1(X1,X3)
| ~ r1_tarski(X3,X0) ) ) )
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2) )
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f19088]) ).
fof(f19175,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = k5_relset_2(X0,X1)
<=> ( k1_relat_1(X2) = k1_zfmisc_1(X0)
& ! [X3] :
( k1_funct_1(X2,X3) = k9_relat_1(X1,X3)
| ~ r1_tarski(X3,X0) ) ) )
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2) )
| ~ v1_relat_1(X1) ),
inference(flattening,[],[f19174]) ).
fof(f19177,plain,
! [X0,X1] :
( ( v1_relat_1(k5_relset_2(X0,X1))
& v1_funct_1(k5_relset_2(X0,X1)) )
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f19060]) ).
fof(f19178,plain,
( ( ~ v1_funct_1(k5_relset_2(sK0,sK2))
| ~ v1_funct_2(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),k1_zfmisc_1(k2_relat_1(sK2)))
| ~ m2_relset_1(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),k1_zfmisc_1(k2_relat_1(sK2))) )
& m1_subset_1(sK2,k1_zfmisc_1(k2_zfmisc_1(sK0,sK1))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f19095]) ).
fof(f19180,plain,
! [X0,X1] :
( ( k2_zfmisc_1(X0,X1) = k1_xboole_0
| ( k1_xboole_0 != X0
& k1_xboole_0 != X1 ) )
& ( X0 = k1_xboole_0
| X1 = k1_xboole_0
| k1_xboole_0 != k2_zfmisc_1(X0,X1) ) ),
inference(nnf_transformation,[],[f438]) ).
fof(f19181,plain,
! [X0,X1] :
( ( k2_zfmisc_1(X0,X1) = k1_xboole_0
| ( k1_xboole_0 != X0
& k1_xboole_0 != X1 ) )
& ( X0 = k1_xboole_0
| X1 = k1_xboole_0
| k1_xboole_0 != k2_zfmisc_1(X0,X1) ) ),
inference(flattening,[],[f19180]) ).
fof(f19185,plain,
! [X0,X1] :
( ( X0 = k1_xboole_0
& X1 != k1_xboole_0 )
| ( k1_relat_1(sK7(X0,X1)) = X1
& r1_tarski(k2_relat_1(sK7(X0,X1)),X0)
& v1_relat_1(sK7(X0,X1))
& v1_funct_1(sK7(X0,X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f19153]) ).
fof(f19193,plain,
! [X0,X1] :
( ! [X2] :
( ( ( X2 = k5_relset_2(X0,X1)
| k1_zfmisc_1(X0) != k1_relat_1(X2)
| ? [X3] :
( k1_funct_1(X2,X3) != k9_relat_1(X1,X3)
& r1_tarski(X3,X0) ) )
& ( ( k1_relat_1(X2) = k1_zfmisc_1(X0)
& ! [X3] :
( k1_funct_1(X2,X3) = k9_relat_1(X1,X3)
| ~ r1_tarski(X3,X0) ) )
| k5_relset_2(X0,X1) != X2 ) )
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2) )
| ~ v1_relat_1(X1) ),
inference(nnf_transformation,[],[f19175]) ).
fof(f19194,plain,
! [X0,X1] :
( ! [X2] :
( ( ( X2 = k5_relset_2(X0,X1)
| k1_zfmisc_1(X0) != k1_relat_1(X2)
| ? [X3] :
( k1_funct_1(X2,X3) != k9_relat_1(X1,X3)
& r1_tarski(X3,X0) ) )
& ( ( k1_relat_1(X2) = k1_zfmisc_1(X0)
& ! [X3] :
( k1_funct_1(X2,X3) = k9_relat_1(X1,X3)
| ~ r1_tarski(X3,X0) ) )
| k5_relset_2(X0,X1) != X2 ) )
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2) )
| ~ v1_relat_1(X1) ),
inference(flattening,[],[f19193]) ).
fof(f19195,plain,
! [X0,X1] :
( ! [X2] :
( ( ( X2 = k5_relset_2(X0,X1)
| k1_zfmisc_1(X0) != k1_relat_1(X2)
| ? [X3] :
( k1_funct_1(X2,X3) != k9_relat_1(X1,X3)
& r1_tarski(X3,X0) ) )
& ( ( k1_relat_1(X2) = k1_zfmisc_1(X0)
& ! [X4] :
( k1_funct_1(X2,X4) = k9_relat_1(X1,X4)
| ~ r1_tarski(X4,X0) ) )
| k5_relset_2(X0,X1) != X2 ) )
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2) )
| ~ v1_relat_1(X1) ),
inference(rectify,[],[f19194]) ).
fof(f19196,plain,
! [X0,X1] :
( ! [X2] :
( ( ( X2 = k5_relset_2(X0,X1)
| k1_zfmisc_1(X0) != k1_relat_1(X2)
| ( k1_funct_1(X2,sK14(X0,X1,X2)) != k9_relat_1(X1,sK14(X0,X1,X2))
& r1_tarski(sK14(X0,X1,X2),X0) ) )
& ( ( k1_relat_1(X2) = k1_zfmisc_1(X0)
& ! [X4] :
( k1_funct_1(X2,X4) = k9_relat_1(X1,X4)
| ~ r1_tarski(X4,X0) ) )
| k5_relset_2(X0,X1) != X2 ) )
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2) )
| ~ v1_relat_1(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X3,sK14(X0,X1,X2))],[f19195]) ).
fof(f19197,plain,
m1_subset_1(sK2,k1_zfmisc_1(k2_zfmisc_1(sK0,sK1))),
inference(cnf_transformation,[],[f19178]) ).
fof(f19198,plain,
( ~ v1_funct_1(k5_relset_2(sK0,sK2))
| ~ v1_funct_2(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),k1_zfmisc_1(k2_relat_1(sK2)))
| ~ m2_relset_1(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),k1_zfmisc_1(k2_relat_1(sK2))) ),
inference(cnf_transformation,[],[f19178]) ).
fof(f19202,plain,
! [X2,X0,X1] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f19097]) ).
fof(f19203,plain,
! [X0,X1] : v1_relat_1(k2_zfmisc_1(X0,X1)),
inference(cnf_transformation,[],[f703]) ).
fof(f19209,plain,
! [X0,X1] :
( ~ r1_tarski(X0,k2_zfmisc_1(X1,X0))
| k1_xboole_0 = X0 ),
inference(cnf_transformation,[],[f19103]) ).
fof(f19215,plain,
! [X2,X0,X1] :
( r1_tarski(k2_zfmisc_1(X0,X2),k2_zfmisc_1(X1,X2))
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f19108]) ).
fof(f19216,plain,
! [X2,X0,X1] :
( ~ r1_tarski(k2_zfmisc_1(X0,X1),k2_zfmisc_1(X0,X2))
| k1_xboole_0 = X0
| r1_tarski(X1,X2) ),
inference(cnf_transformation,[],[f19109]) ).
fof(f19223,plain,
! [X0,X1] :
( k1_xboole_0 = k2_zfmisc_1(X0,X1)
| k1_xboole_0 != X0 ),
inference(cnf_transformation,[],[f19181]) ).
fof(f19225,plain,
! [X2,X0,X1] :
( ~ v1_relat_1(X2)
| ~ r1_tarski(X2,k2_zfmisc_1(X0,X1))
| r1_tarski(k1_relat_1(X2),X0) ),
inference(cnf_transformation,[],[f19115]) ).
fof(f19239,plain,
! [X2,X3,X0,X1] :
( v1_funct_2(X3,X0,X2)
| k1_xboole_0 = X1
| ~ r1_tarski(k2_relat_1(X3),X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f19126]) ).
fof(f19243,plain,
! [X0,X1] :
( ~ v1_funct_1(X1)
| ~ r1_tarski(k2_relat_1(X1),X0)
| ~ v1_relat_1(X1)
| v1_funct_2(X1,k1_relat_1(X1),X0) ),
inference(cnf_transformation,[],[f19130]) ).
fof(f19246,plain,
! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_relat_1(X0)
| v1_funct_2(X0,k1_relat_1(X0),k2_relat_1(X0)) ),
inference(cnf_transformation,[],[f19132]) ).
fof(f19254,plain,
! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_relat_1(X0)
| m2_relset_1(X0,k1_relat_1(X0),k2_relat_1(X0)) ),
inference(cnf_transformation,[],[f19140]) ).
fof(f19259,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| r1_tarski(k1_relat_1(X2),X0) ),
inference(cnf_transformation,[],[f19143]) ).
fof(f19260,plain,
! [X2,X0,X1] :
( m2_relset_1(X2,X0,X1)
| ~ r1_tarski(k1_relat_1(X2),X0)
| ~ r1_tarski(k2_relat_1(X2),X1)
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f19145]) ).
fof(f19265,plain,
! [X0,X1] :
( k1_xboole_0 != X1
| v1_funct_1(sK7(X0,X1)) ),
inference(cnf_transformation,[],[f19185]) ).
fof(f19266,plain,
! [X0,X1] :
( k1_xboole_0 != X1
| v1_relat_1(sK7(X0,X1)) ),
inference(cnf_transformation,[],[f19185]) ).
fof(f19267,plain,
! [X0,X1] :
( k1_xboole_0 != X1
| r1_tarski(k2_relat_1(sK7(X0,X1)),X0) ),
inference(cnf_transformation,[],[f19185]) ).
fof(f19268,plain,
! [X0,X1] :
( k1_xboole_0 != X1
| k1_relat_1(sK7(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f19185]) ).
fof(f19282,plain,
! [X0] :
( k1_xboole_0 != k2_relat_1(X0)
| k1_xboole_0 = X0
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f19160]) ).
fof(f19283,plain,
! [X0] :
( k1_xboole_0 != k1_relat_1(X0)
| k1_xboole_0 = X0
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f19160]) ).
fof(f19284,plain,
k1_xboole_0 = k2_relat_1(k1_xboole_0),
inference(cnf_transformation,[],[f764]) ).
fof(f19285,plain,
k1_xboole_0 = k1_relat_1(k1_xboole_0),
inference(cnf_transformation,[],[f764]) ).
fof(f19288,plain,
! [X0] :
( ~ v1_relat_1(X0)
| r1_tarski(X0,k2_zfmisc_1(k1_relat_1(X0),k2_relat_1(X0))) ),
inference(cnf_transformation,[],[f19163]) ).
fof(f19295,plain,
! [X2,X0,X1] :
( r1_tarski(k2_relat_1(k5_relset_2(X0,X2)),k1_zfmisc_1(k2_relat_1(X2)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f19171]) ).
fof(f19298,plain,
! [X2,X0,X1] :
( k1_zfmisc_1(X0) = k1_relat_1(X2)
| k5_relset_2(X0,X1) != X2
| ~ v1_relat_1(X2)
| ~ v1_funct_1(X2)
| ~ v1_relat_1(X1) ),
inference(cnf_transformation,[],[f19196]) ).
fof(f19302,plain,
! [X0,X1] :
( v1_funct_1(k5_relset_2(X0,X1))
| ~ v1_relat_1(X1) ),
inference(cnf_transformation,[],[f19177]) ).
fof(f19303,plain,
! [X0,X1] :
( v1_relat_1(k5_relset_2(X0,X1))
| ~ v1_relat_1(X1) ),
inference(cnf_transformation,[],[f19177]) ).
fof(f19304,plain,
! [X1] : k1_xboole_0 = k2_zfmisc_1(k1_xboole_0,X1),
inference(equality_resolution,[],[f19223]) ).
fof(f19313,plain,
! [X0] : k1_xboole_0 = k1_relat_1(sK7(X0,k1_xboole_0)),
inference(equality_resolution,[],[f19268]) ).
fof(f19314,plain,
! [X0] : r1_tarski(k2_relat_1(sK7(X0,k1_xboole_0)),X0),
inference(equality_resolution,[],[f19267]) ).
fof(f19315,plain,
! [X0] : v1_relat_1(sK7(X0,k1_xboole_0)),
inference(equality_resolution,[],[f19266]) ).
fof(f19316,plain,
! [X0] : v1_funct_1(sK7(X0,k1_xboole_0)),
inference(equality_resolution,[],[f19265]) ).
fof(f19321,plain,
! [X0,X1] :
( k1_zfmisc_1(X0) = k1_relat_1(k5_relset_2(X0,X1))
| ~ v1_relat_1(k5_relset_2(X0,X1))
| ~ v1_funct_1(k5_relset_2(X0,X1))
| ~ v1_relat_1(X1) ),
inference(equality_resolution,[],[f19298]) ).
fof(f19324,plain,
! [X0,X1] :
( k1_zfmisc_1(X0) = k1_relat_1(k5_relset_2(X0,X1))
| ~ v1_funct_1(k5_relset_2(X0,X1))
| ~ v1_relat_1(X1) ),
inference(forward_subsumption_resolution,[],[f19321,f19303]) ).
fof(f19326,definition,
( spl15_1
<=> m2_relset_1(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),k1_zfmisc_1(k2_relat_1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl15_1])],[avatar_definition]) ).
fof(f19328,plain,
( ~ m2_relset_1(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),k1_zfmisc_1(k2_relat_1(sK2)))
| spl15_1 ),
inference(avatar_component_clause,[],[f19326]) ).
fof(f19330,definition,
( spl15_2
<=> v1_funct_2(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),k1_zfmisc_1(k2_relat_1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl15_2])],[avatar_definition]) ).
fof(f19332,plain,
( ~ v1_funct_2(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),k1_zfmisc_1(k2_relat_1(sK2)))
| spl15_2 ),
inference(avatar_component_clause,[],[f19330]) ).
fof(f19334,definition,
( spl15_3
<=> v1_funct_1(k5_relset_2(sK0,sK2)) ),
introduced(definition,[new_symbols(definition,[spl15_3])],[avatar_definition]) ).
fof(f19335,plain,
( v1_funct_1(k5_relset_2(sK0,sK2))
| ~ spl15_3 ),
inference(avatar_component_clause,[],[f19334]) ).
fof(f19336,plain,
( ~ v1_funct_1(k5_relset_2(sK0,sK2))
| spl15_3 ),
inference(avatar_component_clause,[],[f19334]) ).
fof(f19337,plain,
( ~ spl15_1
| ~ spl15_2
| ~ spl15_3 ),
inference(avatar_split_clause,[],[f19198,f19334,f19330,f19326]) ).
fof(f19339,plain,
! [X0,X1] :
( k1_zfmisc_1(X0) = k1_relat_1(k5_relset_2(X0,X1))
| ~ v1_relat_1(X1) ),
inference(forward_subsumption_resolution,[],[f19324,f19302]) ).
fof(f19340,plain,
v1_relat_1(k1_xboole_0),
inference(superposition,[],[f19203,f19304]) ).
fof(f19345,plain,
! [X0] :
( ~ r1_tarski(X0,k1_xboole_0)
| k1_xboole_0 = X0 ),
inference(superposition,[],[f19209,f19304]) ).
fof(f19346,plain,
k1_xboole_0 = k2_relat_1(sK7(k1_xboole_0,k1_xboole_0)),
inference(resolution,[],[f19345,f19314]) ).
fof(f19368,plain,
( k1_xboole_0 != k1_xboole_0
| k1_xboole_0 = sK7(k1_xboole_0,k1_xboole_0)
| ~ v1_relat_1(sK7(k1_xboole_0,k1_xboole_0)) ),
inference(superposition,[],[f19282,f19346]) ).
fof(f19371,plain,
( k1_xboole_0 = sK7(k1_xboole_0,k1_xboole_0)
| ~ v1_relat_1(sK7(k1_xboole_0,k1_xboole_0)) ),
inference(trivial_inequality_removal,[],[f19368]) ).
fof(f19372,plain,
k1_xboole_0 = sK7(k1_xboole_0,k1_xboole_0),
inference(forward_subsumption_resolution,[],[f19371,f19315]) ).
fof(f19376,plain,
v1_funct_1(k1_xboole_0),
inference(superposition,[],[f19316,f19372]) ).
fof(f19379,plain,
! [X0] :
( k1_xboole_0 != k1_xboole_0
| k1_xboole_0 = sK7(X0,k1_xboole_0)
| ~ v1_relat_1(sK7(X0,k1_xboole_0)) ),
inference(superposition,[],[f19283,f19313]) ).
fof(f19381,plain,
! [X0] :
( k1_xboole_0 = sK7(X0,k1_xboole_0)
| ~ v1_relat_1(sK7(X0,k1_xboole_0)) ),
inference(trivial_inequality_removal,[],[f19379]) ).
fof(f19383,plain,
! [X0] : k1_xboole_0 = sK7(X0,k1_xboole_0),
inference(forward_subsumption_resolution,[],[f19381,f19315]) ).
fof(f19395,plain,
! [X0] : r1_tarski(k2_relat_1(k1_xboole_0),X0),
inference(superposition,[],[f19314,f19383]) ).
fof(f19405,plain,
! [X0] : r1_tarski(k1_xboole_0,X0),
inference(forward_demodulation,[],[f19395,f19284]) ).
fof(f19835,definition,
( spl15_10
<=> r1_tarski(k2_relat_1(k5_relset_2(sK0,sK2)),k1_zfmisc_1(k2_relat_1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl15_10])],[avatar_definition]) ).
fof(f19836,plain,
( r1_tarski(k2_relat_1(k5_relset_2(sK0,sK2)),k1_zfmisc_1(k2_relat_1(sK2)))
| ~ spl15_10 ),
inference(avatar_component_clause,[],[f19835]) ).
fof(f19837,plain,
( ~ r1_tarski(k2_relat_1(k5_relset_2(sK0,sK2)),k1_zfmisc_1(k2_relat_1(sK2)))
| spl15_10 ),
inference(avatar_component_clause,[],[f19835]) ).
fof(f19881,plain,
! [X0,X1] :
( k1_xboole_0 = X0
| r1_tarski(X1,X1)
| ~ r1_tarski(X0,X0) ),
inference(resolution,[],[f19216,f19215]) ).
fof(f19886,definition,
( spl15_11
<=> ! [X1] : r1_tarski(X1,X1) ),
introduced(definition,[new_symbols(definition,[spl15_11])],[avatar_definition]) ).
fof(f19887,plain,
( ! [X1] : r1_tarski(X1,X1)
| ~ spl15_11 ),
inference(avatar_component_clause,[],[f19886]) ).
fof(f19889,definition,
( spl15_12
<=> ! [X0] :
( k1_xboole_0 = X0
| ~ r1_tarski(X0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl15_12])],[avatar_definition]) ).
fof(f19890,plain,
( ! [X0] :
( ~ r1_tarski(X0,X0)
| k1_xboole_0 = X0 )
| ~ spl15_12 ),
inference(avatar_component_clause,[],[f19889]) ).
fof(f19891,plain,
( spl15_11
| spl15_12 ),
inference(avatar_split_clause,[],[f19881,f19889,f19886]) ).
fof(f19916,plain,
! [X0] :
( ~ r1_tarski(k2_relat_1(k1_xboole_0),X0)
| ~ v1_relat_1(k1_xboole_0)
| v1_funct_2(k1_xboole_0,k1_relat_1(k1_xboole_0),X0) ),
inference(resolution,[],[f19243,f19376]) ).
fof(f19917,plain,
! [X0] :
( ~ r1_tarski(k2_relat_1(k1_xboole_0),X0)
| v1_funct_2(k1_xboole_0,k1_relat_1(k1_xboole_0),X0) ),
inference(forward_subsumption_resolution,[],[f19916,f19340]) ).
fof(f19921,plain,
! [X0] :
( ~ r1_tarski(k1_xboole_0,X0)
| v1_funct_2(k1_xboole_0,k1_relat_1(k1_xboole_0),X0) ),
inference(forward_demodulation,[],[f19917,f19284]) ).
fof(f19923,plain,
! [X0] : v1_funct_2(k1_xboole_0,k1_relat_1(k1_xboole_0),X0),
inference(forward_subsumption_resolution,[],[f19921,f19405]) ).
fof(f19925,plain,
! [X0] : v1_funct_2(k1_xboole_0,k1_xboole_0,X0),
inference(forward_demodulation,[],[f19923,f19285]) ).
fof(f19932,plain,
( ~ r1_tarski(k1_relat_1(k5_relset_2(sK0,sK2)),k1_zfmisc_1(sK0))
| ~ r1_tarski(k2_relat_1(k5_relset_2(sK0,sK2)),k1_zfmisc_1(k2_relat_1(sK2)))
| ~ v1_relat_1(k5_relset_2(sK0,sK2))
| spl15_1 ),
inference(resolution,[],[f19260,f19328]) ).
fof(f19937,plain,
( ! [X0] : ~ m1_subset_1(sK2,k1_zfmisc_1(k2_zfmisc_1(sK0,X0)))
| spl15_10 ),
inference(resolution,[],[f19295,f19837]) ).
fof(f19945,plain,
( $false
| spl15_10 ),
inference(resolution,[],[f19937,f19197]) ).
fof(f19947,plain,
spl15_10,
inference(avatar_contradiction_clause,[],[f19945]) ).
fof(f19948,plain,
( ~ r1_tarski(k1_relat_1(k5_relset_2(sK0,sK2)),k1_zfmisc_1(sK0))
| ~ v1_relat_1(k5_relset_2(sK0,sK2))
| spl15_1
| ~ spl15_10 ),
inference(forward_subsumption_resolution,[],[f19932,f19836]) ).
fof(f19950,definition,
( spl15_13
<=> v1_relat_1(k5_relset_2(sK0,sK2)) ),
introduced(definition,[new_symbols(definition,[spl15_13])],[avatar_definition]) ).
fof(f19951,plain,
( v1_relat_1(k5_relset_2(sK0,sK2))
| ~ spl15_13 ),
inference(avatar_component_clause,[],[f19950]) ).
fof(f19952,plain,
( ~ v1_relat_1(k5_relset_2(sK0,sK2))
| spl15_13 ),
inference(avatar_component_clause,[],[f19950]) ).
fof(f19954,definition,
( spl15_14
<=> r1_tarski(k1_relat_1(k5_relset_2(sK0,sK2)),k1_zfmisc_1(sK0)) ),
introduced(definition,[new_symbols(definition,[spl15_14])],[avatar_definition]) ).
fof(f19956,plain,
( ~ r1_tarski(k1_relat_1(k5_relset_2(sK0,sK2)),k1_zfmisc_1(sK0))
| spl15_14 ),
inference(avatar_component_clause,[],[f19954]) ).
fof(f19957,plain,
( ~ spl15_13
| ~ spl15_14
| spl15_1
| ~ spl15_10 ),
inference(avatar_split_clause,[],[f19948,f19835,f19326,f19954,f19950]) ).
fof(f19958,plain,
( ~ v1_relat_1(sK2)
| spl15_13 ),
inference(resolution,[],[f19952,f19303]) ).
fof(f19970,plain,
( ! [X0,X1] : ~ m1_subset_1(sK2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| spl15_13 ),
inference(resolution,[],[f19958,f19202]) ).
fof(f19982,plain,
( $false
| spl15_13 ),
inference(resolution,[],[f19970,f19197]) ).
fof(f19985,plain,
spl15_13,
inference(avatar_contradiction_clause,[],[f19982]) ).
fof(f20029,plain,
( ~ r1_tarski(k1_zfmisc_1(sK0),k1_zfmisc_1(sK0))
| ~ v1_relat_1(sK2)
| spl15_14 ),
inference(superposition,[],[f19956,f19339]) ).
fof(f20030,plain,
( ~ v1_relat_1(sK2)
| ~ spl15_11
| spl15_14 ),
inference(forward_subsumption_resolution,[],[f20029,f19887]) ).
fof(f20035,plain,
( ! [X0,X1] : ~ m1_subset_1(sK2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ spl15_11
| spl15_14 ),
inference(resolution,[],[f20030,f19202]) ).
fof(f20040,plain,
( $false
| ~ spl15_11
| spl15_14 ),
inference(resolution,[],[f20035,f19197]) ).
fof(f20043,plain,
( ~ spl15_11
| spl15_14 ),
inference(avatar_contradiction_clause,[],[f20040]) ).
fof(f20047,definition,
( spl15_18
<=> v1_relat_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl15_18])],[avatar_definition]) ).
fof(f20048,plain,
( v1_relat_1(sK2)
| ~ spl15_18 ),
inference(avatar_component_clause,[],[f20047]) ).
fof(f20049,plain,
( ~ v1_relat_1(sK2)
| spl15_18 ),
inference(avatar_component_clause,[],[f20047]) ).
fof(f20059,plain,
( ! [X0,X1] : ~ m1_subset_1(sK2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| spl15_18 ),
inference(resolution,[],[f20049,f19202]) ).
fof(f20062,plain,
( $false
| spl15_18 ),
inference(resolution,[],[f20059,f19197]) ).
fof(f20065,plain,
spl15_18,
inference(avatar_contradiction_clause,[],[f20062]) ).
fof(f20069,plain,
( ! [X0,X1] :
( ~ r1_tarski(sK2,k2_zfmisc_1(X0,X1))
| r1_tarski(k1_relat_1(sK2),X0) )
| ~ spl15_18 ),
inference(resolution,[],[f20048,f19225]) ).
fof(f20074,plain,
( r1_tarski(sK2,k2_zfmisc_1(k1_relat_1(sK2),k2_relat_1(sK2)))
| ~ spl15_18 ),
inference(resolution,[],[f20048,f19288]) ).
fof(f20118,plain,
( r1_tarski(k1_relat_1(sK2),k1_relat_1(sK2))
| ~ spl15_18 ),
inference(resolution,[],[f20069,f20074]) ).
fof(f20195,plain,
( k1_xboole_0 = k1_relat_1(sK2)
| ~ spl15_12
| ~ spl15_18 ),
inference(resolution,[],[f19890,f20118]) ).
fof(f20211,plain,
( k1_xboole_0 != k1_xboole_0
| k1_xboole_0 = sK2
| ~ v1_relat_1(sK2)
| ~ spl15_12
| ~ spl15_18 ),
inference(superposition,[],[f19283,f20195]) ).
fof(f20212,plain,
( k1_xboole_0 = sK2
| ~ v1_relat_1(sK2)
| ~ spl15_12
| ~ spl15_18 ),
inference(trivial_inequality_removal,[],[f20211]) ).
fof(f20214,plain,
( k1_xboole_0 = sK2
| ~ spl15_12
| ~ spl15_18 ),
inference(forward_subsumption_resolution,[],[f20212,f20048]) ).
fof(f20229,plain,
( ~ v1_relat_1(sK2)
| spl15_3 ),
inference(resolution,[],[f19336,f19302]) ).
fof(f20230,plain,
( $false
| spl15_3
| ~ spl15_18 ),
inference(forward_subsumption_resolution,[],[f20229,f20048]) ).
fof(f20231,plain,
( spl15_3
| ~ spl15_18 ),
inference(avatar_contradiction_clause,[],[f20230]) ).
fof(f20235,plain,
( ~ v1_relat_1(k5_relset_2(sK0,sK2))
| v1_funct_2(k5_relset_2(sK0,sK2),k1_relat_1(k5_relset_2(sK0,sK2)),k2_relat_1(k5_relset_2(sK0,sK2)))
| ~ spl15_3 ),
inference(resolution,[],[f19335,f19246]) ).
fof(f20236,plain,
( ~ v1_relat_1(k5_relset_2(sK0,sK2))
| m2_relset_1(k5_relset_2(sK0,sK2),k1_relat_1(k5_relset_2(sK0,sK2)),k2_relat_1(k5_relset_2(sK0,sK2)))
| ~ spl15_3 ),
inference(resolution,[],[f19335,f19254]) ).
fof(f20242,plain,
( m2_relset_1(k5_relset_2(sK0,sK2),k1_relat_1(k5_relset_2(sK0,sK2)),k2_relat_1(k5_relset_2(sK0,sK2)))
| ~ spl15_3
| ~ spl15_13 ),
inference(forward_subsumption_resolution,[],[f20236,f19951]) ).
fof(f20243,plain,
( v1_funct_2(k5_relset_2(sK0,sK2),k1_relat_1(k5_relset_2(sK0,sK2)),k2_relat_1(k5_relset_2(sK0,sK2)))
| ~ spl15_3
| ~ spl15_13 ),
inference(forward_subsumption_resolution,[],[f20235,f19951]) ).
fof(f20249,plain,
( ! [X0] :
( k1_xboole_0 = X0
| ~ r1_tarski(k2_relat_1(k5_relset_2(sK0,sK2)),k1_zfmisc_1(k2_relat_1(sK2)))
| ~ v1_funct_1(k5_relset_2(sK0,sK2))
| ~ v1_funct_2(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),X0)
| ~ m2_relset_1(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),X0) )
| spl15_2 ),
inference(resolution,[],[f19332,f19239]) ).
fof(f20250,plain,
( ! [X0] :
( k1_xboole_0 = X0
| ~ v1_funct_1(k5_relset_2(sK0,sK2))
| ~ v1_funct_2(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),X0)
| ~ m2_relset_1(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),X0) )
| spl15_2
| ~ spl15_10 ),
inference(forward_subsumption_resolution,[],[f20249,f19836]) ).
fof(f20251,plain,
( ! [X0] :
( ~ v1_funct_2(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),X0)
| k1_xboole_0 = X0
| ~ m2_relset_1(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),X0) )
| spl15_2
| ~ spl15_3
| ~ spl15_10 ),
inference(forward_subsumption_resolution,[],[f20250,f19335]) ).
fof(f20255,plain,
( m2_relset_1(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),k2_relat_1(k5_relset_2(sK0,sK2)))
| ~ v1_relat_1(sK2)
| ~ spl15_3
| ~ spl15_13 ),
inference(superposition,[],[f20242,f19339]) ).
fof(f20256,plain,
( m2_relset_1(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),k2_relat_1(k5_relset_2(sK0,sK2)))
| ~ spl15_3
| ~ spl15_13
| ~ spl15_18 ),
inference(forward_subsumption_resolution,[],[f20255,f20048]) ).
fof(f20258,plain,
( r1_tarski(k1_relat_1(k5_relset_2(sK0,sK2)),k1_zfmisc_1(sK0))
| ~ spl15_3
| ~ spl15_13
| ~ spl15_18 ),
inference(resolution,[],[f20256,f19259]) ).
fof(f20260,plain,
( v1_funct_2(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),k2_relat_1(k5_relset_2(sK0,sK2)))
| ~ v1_relat_1(sK2)
| ~ spl15_3
| ~ spl15_13 ),
inference(superposition,[],[f20243,f19339]) ).
fof(f20261,plain,
( v1_funct_2(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),k2_relat_1(k5_relset_2(sK0,sK2)))
| ~ spl15_3
| ~ spl15_13
| ~ spl15_18 ),
inference(forward_subsumption_resolution,[],[f20260,f20048]) ).
fof(f20285,plain,
( k1_xboole_0 = k2_relat_1(k5_relset_2(sK0,sK2))
| ~ m2_relset_1(k5_relset_2(sK0,sK2),k1_zfmisc_1(sK0),k2_relat_1(k5_relset_2(sK0,sK2)))
| spl15_2
| ~ spl15_3
| ~ spl15_10
| ~ spl15_13
| ~ spl15_18 ),
inference(resolution,[],[f20251,f20261]) ).
fof(f20287,plain,
( k1_xboole_0 = k2_relat_1(k5_relset_2(sK0,sK2))
| spl15_2
| ~ spl15_3
| ~ spl15_10
| ~ spl15_13
| ~ spl15_18 ),
inference(forward_subsumption_resolution,[],[f20285,f20256]) ).
fof(f20298,plain,
( k1_xboole_0 != k1_xboole_0
| k1_xboole_0 = k5_relset_2(sK0,sK2)
| ~ v1_relat_1(k5_relset_2(sK0,sK2))
| spl15_2
| ~ spl15_3
| ~ spl15_10
| ~ spl15_13
| ~ spl15_18 ),
inference(superposition,[],[f19282,f20287]) ).
fof(f20304,plain,
( k1_xboole_0 = k5_relset_2(sK0,sK2)
| ~ v1_relat_1(k5_relset_2(sK0,sK2))
| spl15_2
| ~ spl15_3
| ~ spl15_10
| ~ spl15_13
| ~ spl15_18 ),
inference(trivial_inequality_removal,[],[f20298]) ).
fof(f20308,plain,
( k1_xboole_0 = k5_relset_2(sK0,sK2)
| spl15_2
| ~ spl15_3
| ~ spl15_10
| ~ spl15_13
| ~ spl15_18 ),
inference(forward_subsumption_resolution,[],[f20304,f19951]) ).
fof(f20370,plain,
( k1_relat_1(k1_xboole_0) = k1_zfmisc_1(sK0)
| ~ v1_relat_1(sK2)
| spl15_2
| ~ spl15_3
| ~ spl15_10
| ~ spl15_13
| ~ spl15_18 ),
inference(superposition,[],[f19339,f20308]) ).
fof(f20373,plain,
( k1_relat_1(k1_xboole_0) = k1_zfmisc_1(sK0)
| spl15_2
| ~ spl15_3
| ~ spl15_10
| ~ spl15_13
| ~ spl15_18 ),
inference(forward_subsumption_resolution,[],[f20370,f20048]) ).
fof(f20388,plain,
( k1_xboole_0 = k1_zfmisc_1(sK0)
| spl15_2
| ~ spl15_3
| ~ spl15_10
| ~ spl15_13
| ~ spl15_18 ),
inference(forward_demodulation,[],[f20373,f19285]) ).
fof(f20425,plain,
( ~ v1_funct_2(k5_relset_2(sK0,sK2),k1_xboole_0,k1_zfmisc_1(k2_relat_1(sK2)))
| spl15_2
| ~ spl15_3
| ~ spl15_10
| ~ spl15_13
| ~ spl15_18 ),
inference(superposition,[],[f19332,f20388]) ).
fof(f20442,plain,
( ~ v1_funct_2(k1_xboole_0,k1_xboole_0,k1_zfmisc_1(k2_relat_1(sK2)))
| spl15_2
| ~ spl15_3
| ~ spl15_10
| ~ spl15_13
| ~ spl15_18 ),
inference(forward_demodulation,[],[f20425,f20308]) ).
fof(f20450,plain,
( $false
| spl15_2
| ~ spl15_3
| ~ spl15_10
| ~ spl15_13
| ~ spl15_18 ),
inference(forward_subsumption_resolution,[],[f20442,f19925]) ).
fof(f20451,plain,
( spl15_2
| ~ spl15_3
| ~ spl15_10
| ~ spl15_13
| ~ spl15_18 ),
inference(avatar_contradiction_clause,[],[f20450]) ).
fof(f20458,plain,
( ~ r1_tarski(k1_relat_1(k5_relset_2(sK0,k1_xboole_0)),k1_zfmisc_1(sK0))
| ~ spl15_12
| spl15_14
| ~ spl15_18 ),
inference(forward_demodulation,[],[f19956,f20214]) ).
fof(f20466,plain,
( r1_tarski(k1_relat_1(k5_relset_2(sK0,k1_xboole_0)),k1_zfmisc_1(sK0))
| ~ spl15_3
| ~ spl15_12
| ~ spl15_13
| ~ spl15_18 ),
inference(forward_demodulation,[],[f20258,f20214]) ).
fof(f20488,plain,
( $false
| ~ spl15_3
| ~ spl15_12
| ~ spl15_13
| spl15_14
| ~ spl15_18 ),
inference(forward_subsumption_resolution,[],[f20466,f20458]) ).
fof(f20489,plain,
( ~ spl15_3
| ~ spl15_12
| ~ spl15_13
| spl15_14
| ~ spl15_18 ),
inference(avatar_contradiction_clause,[],[f20488]) ).
cnf(s1,plain,
( ~ spl15_1
| ~ spl15_2
| ~ spl15_3 ),
inference(sat_conversion,[],[f19337]) ).
cnf(s13,plain,
( spl15_11
| spl15_12 ),
inference(sat_conversion,[],[f19891]) ).
cnf(s14,plain,
spl15_10,
inference(sat_conversion,[],[f19947]) ).
cnf(s15,plain,
( spl15_1
| ~ spl15_10
| ~ spl15_13
| ~ spl15_14 ),
inference(sat_conversion,[],[f19957]) ).
cnf(s16,plain,
spl15_13,
inference(sat_conversion,[],[f19985]) ).
cnf(s19,plain,
( ~ spl15_11
| spl15_14 ),
inference(sat_conversion,[],[f20043]) ).
cnf(s21,plain,
spl15_18,
inference(sat_conversion,[],[f20065]) ).
cnf(s26,plain,
( spl15_3
| ~ spl15_18 ),
inference(sat_conversion,[],[f20231]) ).
cnf(s30,plain,
( spl15_2
| ~ spl15_3
| ~ spl15_10
| ~ spl15_13
| ~ spl15_18 ),
inference(sat_conversion,[],[f20451]) ).
cnf(s31,plain,
( ~ spl15_3
| ~ spl15_12
| ~ spl15_13
| spl15_14
| ~ spl15_18 ),
inference(sat_conversion,[],[f20489]) ).
cnf(s33,plain,
spl15_3,
inference(rat,[],[s26,s21]) ).
cnf(s35,plain,
( spl15_1
| ~ spl15_10
| ~ spl15_14 ),
inference(rat,[],[s15,s16]) ).
cnf(s36,plain,
spl15_2,
inference(rat,[],[s30,s21,s16,s33,s14]) ).
cnf(s38,plain,
~ spl15_1,
inference(rat,[],[s1,s33,s36]) ).
cnf(s39,plain,
~ spl15_14,
inference(rat,[],[s35,s14,s38]) ).
cnf(s43,plain,
~ spl15_11,
inference(rat,[],[s19,s39]) ).
cnf(s44,plain,
~ spl15_12,
inference(rat,[],[s31,s21,s16,s33,s39]) ).
cnf(s46,plain,
$false,
inference(rat,[],[s13,s44,s43]) ).
fof(f20527,plain,
$false,
inference(avatar_sat_refutation,[],[s46]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU425+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.46 % Computer : n010.cluster.edu
% 0.20/0.46 % Model : x86_64 x86_64
% 0.20/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.46 % Memory : 8046.5625MB
% 0.20/0.46 % OS : Linux 6.8.0-71-generic
% 0.20/0.46 % CPULimit : 300
% 0.20/0.46 % WCLimit : 300
% 0.20/0.46 % DateTime : Mon Sep 28 05:21:51 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.46 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.51 Running first-order theorem proving
% 0.20/0.51 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
% 7.37/4.52 % (1585512)Detected formulas, will run a generic FOF schedule.
% 7.37/4.52 % (1585517)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=2650629564:i=141193_2981 on theBenchmark for (2981ds/141193Mi)
% 7.37/4.52 % (1585523)dis-21_1_sil=8000:lcm=predicate:random_seed=2604147825:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2981 on theBenchmark for (2981ds/129Mi)
% 7.37/4.52 % (1585518)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=820473308:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2981 on theBenchmark for (2981ds/134677Mi)
% 7.37/4.52 % (1585519)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=3656233519:i=141695:sd=1:nm=32:gsp=on:ss=included_2981 on theBenchmark for (2981ds/141695Mi)
% 7.37/4.52 % (1585520)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2241316575:i=109:sd=1:ins=1:gsp=on:ss=axioms_2981 on theBenchmark for (2981ds/109Mi)
% 7.37/4.52 % (1585521)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2721164884:i=119:av=off:ss=axioms_2981 on theBenchmark for (2981ds/119Mi)
% 7.37/4.52 % (1585522)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1635337358:s2a=on:i=139:gtg=position_2981 on theBenchmark for (2981ds/139Mi)
% 7.37/4.52 % (1585523)Instruction limit reached!
% 7.37/4.52 % (1585523)------------------------------
% 7.37/4.52 % (1585523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.37/4.52 % (1585523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/4.52 % (1585523)CaDiCaL version: 2.1.3
% 7.37/4.52 % (1585523)Termination reason: Instruction limit
% 7.37/4.52 % (1585523)Termination phase: SInE selection
% 7.37/4.52 % (1585523)Time elapsed: 0.083 s
% 7.37/4.52 % (1585523)Peak memory usage: 112 MB
% 7.37/4.52 % (1585523)Instructions burned: 129 (million)
% 7.37/4.52 % (1585522)Instruction limit reached!
% 7.37/4.52 % (1585522)------------------------------
% 7.37/4.52 % (1585522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.37/4.52 % (1585522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/4.52 % (1585522)CaDiCaL version: 2.1.3
% 7.37/4.52 % (1585522)Termination reason: Instruction limit
% 7.37/4.52 % (1585522)Termination phase: Property scanning
% 7.37/4.52 % (1585522)Time elapsed: 0.116 s
% 7.37/4.52 % (1585522)Peak memory usage: 112 MB
% 7.37/4.52 % (1585522)Instructions burned: 140 (million)
% 7.37/4.52 % (1585520)Instruction limit reached!
% 7.37/4.52 % (1585520)------------------------------
% 7.37/4.52 % (1585520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.37/4.52 % (1585520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/4.52 % (1585520)CaDiCaL version: 2.1.3
% 7.37/4.52 % (1585520)Termination reason: Instruction limit
% 7.37/4.52 % (1585520)Termination phase: SInE selection
% 7.37/4.52 % (1585520)Time elapsed: 0.122 s
% 7.37/4.52 % (1585520)Peak memory usage: 112 MB
% 7.37/4.52 % (1585520)Instructions burned: 109 (million)
% 7.37/4.52 % (1585521)Instruction limit reached!
% 7.37/4.52 % (1585521)------------------------------
% 7.37/4.52 % (1585521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.37/4.52 % (1585521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/4.52 % (1585521)CaDiCaL version: 2.1.3
% 7.37/4.52 % (1585521)Termination reason: Instruction limit
% 7.37/4.52 % (1585521)Termination phase: Unused predicate definition removal
% 7.37/4.52 % (1585521)Time elapsed: 0.147 s
% 7.37/4.52 % (1585521)Peak memory usage: 114 MB
% 7.37/4.52 % (1585521)Instructions burned: 119 (million)
% 7.37/4.52 % (1585531)lrs+10_1_sil=8000:sp=occurrence:random_seed=899142191:i=285:sd=3:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/285Mi)
% 7.37/4.52 % (1585532)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3315848854:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/157Mi)
% 7.37/4.52 % (1585533)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1052848434:i=325:sd=1:ss=axioms:sgt=32_2976 on theBenchmark for (2976ds/325Mi)
% 7.37/4.52 % (1585534)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=1608161968:s2a=on:i=248:s2at=1.23:gtg=position_2976 on theBenchmark for (2976ds/248Mi)
% 7.37/4.52 % (1585532)Instruction limit reached!
% 7.37/4.52 % (1585532)------------------------------
% 7.37/4.52 % (1585532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.37/4.52 % (1585532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/4.52 % (1585532)CaDiCaL version: 2.1.3
% 7.37/4.52 % (1585532)Termination reason: Instruction limit
% 7.37/4.52 % (1585532)Termination phase: Property scanning
% 7.37/4.52 % (1585532)Time elapsed: 0.130 s
% 7.37/4.52 % (1585532)Peak memory usage: 112 MB
% 7.37/4.52 % (1585532)Instructions burned: 158 (million)
% 7.37/4.52 % (1585531)Instruction limit reached!
% 7.37/4.52 % (1585531)------------------------------
% 7.37/4.52 % (1585531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.37/4.52 % (1585531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/4.52 % (1585531)CaDiCaL version: 2.1.3
% 7.37/4.52 % (1585531)Termination reason: Instruction limit
% 7.37/4.52 % (1585531)Termination phase: Saturation
% 7.37/4.52 % (1585531)Time elapsed: 0.208 s
% 7.37/4.52 % (1585531)Peak memory usage: 119 MB
% 7.37/4.52 % (1585531)Instructions burned: 287 (million)
% 7.37/4.52 % (1585533)First to succeed.
% 7.37/4.52 % (1585533)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1585512"
% 7.37/4.52 % (1585534)Instruction limit reached!
% 7.37/4.52 % (1585534)------------------------------
% 7.37/4.52 % (1585534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.37/4.52 % (1585534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.37/4.52 % (1585534)CaDiCaL version: 2.1.3
% 7.37/4.52 % (1585534)Termination reason: Instruction limit
% 7.37/4.52 % (1585534)Termination phase: Property scanning
% 7.37/4.52 % (1585534)Time elapsed: 0.203 s
% 7.37/4.52 % (1585534)Peak memory usage: 112 MB
% 7.37/4.52 % (1585534)Instructions burned: 248 (million)
% 7.37/4.52 % (1585540)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1173964558:i=2350_2972 on theBenchmark for (2972ds/2350Mi)
% 7.37/4.52 % (1585539)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3137135801:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2972 on theBenchmark for (2972ds/294Mi)
% 7.37/4.52 % (1585541)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=939746940:cts=off:i=113:fsr=off:ss=included:sgt=4_2971 on theBenchmark for (2971ds/113Mi)
% 7.37/4.52 % (1585533)Refutation found. Thanks to Tanya!
% 7.37/4.52 % SZS status Theorem for theBenchmark
% 7.37/4.52 % SZS output start Proof for theBenchmark
% See solution above
% 0.27/4.92 % (1585533)------------------------------
% 0.27/4.92 % (1585533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.27/4.92 % (1585533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.27/4.92 % (1585533)CaDiCaL version: 2.1.3
% 0.27/4.92 % (1585533)Termination reason: Refutation
% 0.27/4.92 % (1585533)Time elapsed: 0.221 s
% 0.27/4.92 % (1585533)Peak memory usage: 119 MB
% 0.27/4.92 % (1585533)Instructions burned: 168 (million)
% 0.27/4.92 % (1585533)------------------------------
% 0.27/4.92 % (1585533)------------------------------
% 0.27/4.92 % (1585512)Success in time 3.315 s
% 0.27/4.92 % Vampire exiting
%------------------------------------------------------------------------------