%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU425+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 : Thu Sep 24 02:20:32 PM UTC 2026
% Result : Theorem 78.78s 15.56s
% Output : CNFRefutation 76.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 186
% Syntax : Number of formulae : 757 ( 274 unt; 104 def)
% Number of atoms : 1710 ( 405 equ)
% Maximal formula atoms : 20 ( 2 avg)
% Number of connectives : 1624 ( 671 ~; 536 |; 253 &)
% ( 122 <=>; 42 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 127 ( 125 usr; 105 prp; 0-3 aty)
% Number of functors : 85 ( 85 usr; 44 con; 0-4 aty)
% Number of variables : 505 ( 463 !; 42 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [A,B] :
( B = k1_tarski(A)
<=> ! [C] :
( r2_hidden(C,B)
<=> C = A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A] :
( A = k1_xboole_0
<=> ! [B] : ~ r2_hidden(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A] :
( v1_xboole_0(A)
<=> A = k1_xboole_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [A,B] :
( r2_xboole_0(A,B)
=> ~ r2_xboole_0(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,axiom,
! [A] : k4_xboole_0(k1_xboole_0,A) = k1_xboole_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [A] :
( v1_xboole_0(A)
=> A = k1_xboole_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,axiom,
! [A] :
( r1_tarski(A,k1_xboole_0)
=> A = k1_xboole_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [A,B] : r1_tarski(A,k2_xboole_0(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f81,axiom,
! [A,B] :
( r1_tarski(A,B)
=> k2_xboole_0(A,B) = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,axiom,
! [A,B] : k4_xboole_0(k2_xboole_0(A,B),B) = k4_xboole_0(A,B),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f152,axiom,
! [A,B] :
( r1_xboole_0(A,B)
<=> k4_xboole_0(A,B) = A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f174,axiom,
! [A,B] :
~ ( k4_xboole_0(B,A) = k1_xboole_0
& r2_xboole_0(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f185,axiom,
! [A,B] :
( B = k1_zfmisc_1(A)
<=> ! [C] :
( r2_hidden(C,B)
<=> r1_tarski(C,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f189,axiom,
k1_zfmisc_1(k1_xboole_0) = k1_tarski(k1_xboole_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f190,axiom,
k3_tarski(k1_xboole_0) = k1_xboole_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f202,axiom,
! [A,B] : k2_xboole_0(k1_tarski(A),k2_tarski(A,B)) = k2_tarski(A,B),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f204,axiom,
! [A,B] :
~ ( A = B
& r1_xboole_0(k1_tarski(A),k1_tarski(B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f237,axiom,
! [A,B] : k2_xboole_0(k1_tarski(A),B) != k1_xboole_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f263,axiom,
! [A,B,C] :
( k4_xboole_0(A,k2_tarski(B,C)) = k1_xboole_0
<=> ~ ( A != k2_tarski(B,C)
& A != k1_tarski(C)
& A != k1_tarski(B)
& A != k1_xboole_0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f334,axiom,
! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f345,axiom,
! [A] : k2_subset_1(A) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f349,axiom,
! [A] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f427,axiom,
! [A] : m1_subset_1(k2_subset_1(A),k1_zfmisc_1(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f453,axiom,
! [A,B] :
( ( A = k1_xboole_0
=> ( B = k1_setfam_1(A)
<=> B = k1_xboole_0 ) )
& ( A != k1_xboole_0
=> ( B = k1_setfam_1(A)
<=> ! [C] :
( r2_hidden(C,B)
<=> ! [D] :
( r2_hidden(D,A)
=> r2_hidden(C,D) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f540,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f543,axiom,
? [A] :
( v1_relat_1(A)
& v1_xboole_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f566,axiom,
! [A,B] : v1_relat_1(k2_zfmisc_1(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f650,axiom,
k6_relat_1(k1_xboole_0) = k1_xboole_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f772,axiom,
! [A] : v1_relat_1(k6_relat_1(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f781,axiom,
? [A] :
( v1_funct_1(A)
& v1_xboole_0(A)
& v1_relat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1040,axiom,
? [A] :
( v3_ordinal1(A)
& v2_ordinal1(A)
& v1_ordinal1(A)
& v1_xboole_0(A)
& v2_funct_1(A)
& v1_funct_1(A)
& v1_relat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1062,axiom,
! [A] : A != k1_ordinal1(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1110,axiom,
? [A] :
( ! [B] :
( v3_ordinal1(B)
=> ! [C] :
( ( v5_ordinal1(C)
& v1_funct_1(C)
& v1_relat_1(C) )
=> ( ( C = k2_ordinal1(A,B)
& r2_hidden(B,f1_s4_ordinal1) )
=> k1_funct_1(A,B) = f2_s4_ordinal1(C) ) ) )
& k1_relat_1(A) = f1_s4_ordinal1
& v5_ordinal1(A)
& v1_funct_1(A)
& v1_relat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1120,axiom,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> v1_relat_1(C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1131,axiom,
! [A,B] :
( v1_relat_1(B)
=> ( r1_tarski(k2_relat_1(B),A)
=> m2_relset_1(B,k1_relat_1(B),A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1146,axiom,
! [A,B] : m2_relset_1(k1_xboole_0,A,B),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1209,axiom,
? [A] :
( v1_xboole_0(A)
& v2_funct_1(A)
& v1_funct_1(A)
& v1_relat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1408,axiom,
? [A] :
( ! [B] :
( r2_hidden(B,f1_s1_partfun1)
=> ( ( ~ p1_s1_partfun1(B)
=> k1_funct_1(A,B) = f3_s1_partfun1(B) )
& ( p1_s1_partfun1(B)
=> k1_funct_1(A,B) = f2_s1_partfun1(B) ) ) )
& k1_relat_1(A) = f1_s1_partfun1
& v1_funct_1(A)
& v1_relat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1423,axiom,
! [A] : k6_partfun1(A) = k6_relat_1(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1567,axiom,
! [A,B] :
( ( v1_funct_1(B)
& v1_relat_1(B) )
=> ( r1_tarski(k2_relat_1(B),A)
=> ( m2_relset_1(B,k1_relat_1(B),A)
& v1_funct_2(B,k1_relat_1(B),A)
& v1_funct_1(B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1740,axiom,
? [A] :
( ! [B] :
( m1_subset_1(B,f1_s4_funct_2)
=> k8_funct_2(f1_s4_funct_2,f2_s4_funct_2,A,B) = f3_s4_funct_2(B) )
& m2_relset_1(A,f1_s4_funct_2,f2_s4_funct_2)
& v1_funct_2(A,f1_s4_funct_2,f2_s4_funct_2)
& v1_funct_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1744,axiom,
? [A] :
( ! [B] :
( m1_subset_1(B,f1_s8_funct_2)
=> ! [C] :
( m1_subset_1(C,f2_s8_funct_2)
=> k1_funct_1(A,k4_tarski(B,C)) = f4_s8_funct_2(B,C) ) )
& m2_relset_1(A,k2_zfmisc_1(f1_s8_funct_2,f2_s8_funct_2),f3_s8_funct_2)
& v1_funct_2(A,k2_zfmisc_1(f1_s8_funct_2,f2_s8_funct_2),f3_s8_funct_2)
& v1_funct_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1746,axiom,
? [A] :
( ! [B] :
( m1_subset_1(B,f1_s10_funct_2)
=> ( B != f3_s10_funct_2
=> k8_funct_2(f1_s10_funct_2,f2_s10_funct_2,A,B) = f5_s10_funct_2(B) ) )
& k8_funct_2(f1_s10_funct_2,f2_s10_funct_2,A,f3_s10_funct_2) = f4_s10_funct_2
& m2_relset_1(A,f1_s10_funct_2,f2_s10_funct_2)
& v1_funct_2(A,f1_s10_funct_2,f2_s10_funct_2)
& v1_funct_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2024,axiom,
( ~ v1_xboole_0(k5_ordinal2)
& v3_ordinal1(k5_ordinal2)
& v2_ordinal1(k5_ordinal2)
& v1_ordinal1(k5_ordinal2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2046,axiom,
! [A] : r1_tarski(k3_ordinal2(A),A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2051,axiom,
k4_ordinal2 = k1_ordinal1(k1_xboole_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2121,axiom,
? [A] :
( ! [B] :
( v3_ordinal1(B)
=> ( ( v4_ordinal1(B)
& r2_hidden(B,f1_s5_ordinal2) )
=> ( k1_funct_1(A,B) = f4_s5_ordinal2(B,k2_ordinal1(A,B))
| B = k1_xboole_0 ) ) )
& ! [B] :
( v3_ordinal1(B)
=> ( r2_hidden(k1_ordinal1(B),f1_s5_ordinal2)
=> k1_funct_1(A,k1_ordinal1(B)) = f3_s5_ordinal2(B,k1_funct_1(A,B)) ) )
& ( r2_hidden(k1_xboole_0,f1_s5_ordinal2)
=> k1_funct_1(A,k1_xboole_0) = f2_s5_ordinal2 )
& k1_relat_1(A) = f1_s5_ordinal2
& v5_ordinal1(A)
& v1_funct_1(A)
& v1_relat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2127,axiom,
? [A] :
( ! [B] :
( v3_ordinal1(B)
=> ( ( v4_ordinal1(B)
& r2_hidden(B,f1_s11_ordinal2) )
=> ( k1_funct_1(A,B) = f4_s11_ordinal2(B,k2_ordinal1(A,B))
| B = k1_xboole_0 ) ) )
& ! [B] :
( v3_ordinal1(B)
=> ( r2_hidden(k1_ordinal1(B),f1_s11_ordinal2)
=> k1_funct_1(A,k1_ordinal1(B)) = f3_s11_ordinal2(B,k1_funct_1(A,B)) ) )
& ( r2_hidden(k1_xboole_0,f1_s11_ordinal2)
=> k1_funct_1(A,k1_xboole_0) = f2_s11_ordinal2 )
& k1_relat_1(A) = f1_s11_ordinal2
& v1_ordinal2(A)
& v5_ordinal1(A)
& v1_funct_1(A)
& v1_relat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2206,axiom,
~ v1_xboole_0(k1_numbers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2208,axiom,
~ v1_xboole_0(k3_numbers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2213,axiom,
r2_xboole_0(k1_numbers,k2_numbers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2214,axiom,
r2_xboole_0(k3_numbers,k1_numbers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2215,axiom,
r2_xboole_0(k3_numbers,k2_numbers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2216,axiom,
r2_xboole_0(k4_numbers,k3_numbers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2217,axiom,
r2_xboole_0(k4_numbers,k1_numbers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2218,axiom,
r2_xboole_0(k4_numbers,k2_numbers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2219,axiom,
r2_xboole_0(k5_numbers,k4_numbers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2220,axiom,
r2_xboole_0(k5_numbers,k3_numbers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2221,axiom,
r2_xboole_0(k5_numbers,k1_numbers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2222,axiom,
r2_xboole_0(k5_numbers,k2_numbers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2232,axiom,
r1_tarski(k5_numbers,k2_numbers),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2233,axiom,
k1_numbers != k2_numbers,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2234,axiom,
k3_numbers != k1_numbers,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2235,axiom,
k3_numbers != k2_numbers,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2236,axiom,
k4_numbers != k3_numbers,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2237,axiom,
k4_numbers != k1_numbers,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2238,axiom,
k4_numbers != k2_numbers,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2239,axiom,
k5_numbers != k4_numbers,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2240,axiom,
k5_numbers != k3_numbers,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2241,axiom,
k5_numbers != k1_numbers,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2242,axiom,
k5_numbers != k2_numbers,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2248,axiom,
k5_numbers = k5_ordinal2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2485,axiom,
np__0 = k1_xboole_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2534,axiom,
( v1_finseq_1(k1_xboole_0)
& v1_finset_1(k1_xboole_0)
& v2_funct_1(k1_xboole_0)
& v1_funct_1(k1_xboole_0)
& v3_relat_1(k1_xboole_0)
& v1_relat_1(k1_xboole_0)
& v1_xboole_0(k1_xboole_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2536,axiom,
? [A] :
( v1_finseq_1(A)
& v1_finset_1(A)
& v2_funct_1(A)
& v1_funct_1(A)
& v1_relat_1(A)
& v1_xboole_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2540,axiom,
! [A,B] :
( v1_funct_1(k10_finseq_1(A,B))
& v1_relat_1(k10_finseq_1(A,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2547,axiom,
? [A] :
( v1_finset_1(A)
& v2_funct_1(A)
& v1_funct_1(A)
& v1_relat_1(A)
& v1_xboole_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3068,axiom,
? [A] :
( ! [B] :
( ( v1_funct_1(B)
& v1_relat_1(B) )
=> ( r2_hidden(B,f1_s1_funct_5)
=> k1_funct_1(A,B) = f2_s1_funct_5(B) ) )
& k1_relat_1(A) = f1_s1_funct_5
& v1_funct_1(A)
& v1_relat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4461,axiom,
! [A,B] :
( v1_relat_1(B)
=> ( v1_funct_1(k5_relset_2(A,B))
& v1_relat_1(k5_relset_2(A,B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4489,axiom,
! [A,B] :
( v1_relat_1(B)
=> ! [C] :
( ( v1_funct_1(C)
& v1_relat_1(C) )
=> ( C = k5_relset_2(A,B)
<=> ( ! [D] :
( r1_tarski(D,A)
=> k1_funct_1(C,D) = k9_relat_1(B,D) )
& k1_relat_1(C) = k1_zfmisc_1(A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4491,axiom,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> r1_tarski(k2_relat_1(k5_relset_2(A,C)),k1_zfmisc_1(k2_relat_1(C))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4492,conjecture,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> ( m2_relset_1(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))
& v1_funct_2(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))
& v1_funct_1(k5_relset_2(A,C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4493,negated_conjecture,
~ ! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> ( m2_relset_1(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))
& v1_funct_2(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))
& v1_funct_1(k5_relset_2(A,C)) ) ),
inference(negated_conjecture,[status(cth)],[f4492]) ).
fof(f4501,plain,
! [A,B] :
( ( ? [C] :
( ( C = A
| r2_hidden(C,B) )
& ( C != A
| ~ r2_hidden(C,B) ) )
| B = k1_tarski(A) )
& ( ! [C] :
( ( C != A
| r2_hidden(C,B) )
& ( C = A
| ~ r2_hidden(C,B) ) )
| B != k1_tarski(A) ) ),
inference(NNF_transformation,[status(thm)],[f4]) ).
fof(f4502,plain,
( ! [A,B] :
( ? [C] :
( ( C = A
| r2_hidden(C,B) )
& ( C != A
| ~ r2_hidden(C,B) ) )
| B = k1_tarski(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| r2_hidden(C,B) )
& ! [C] :
( C = A
| ~ r2_hidden(C,B) ) )
| B != k1_tarski(A) ) ),
inference(miniscoping,[status(thm)],[f4501]) ).
fof(f4503,plain,
( ! [A,B] :
( ( ( sK1_skl(B,A) = A
| r2_hidden(sK1_skl(B,A),B) )
& ( sK1_skl(B,A) != A
| ~ r2_hidden(sK1_skl(B,A),B) ) )
| B = k1_tarski(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| r2_hidden(C,B) )
& ! [C] :
( C = A
| ~ r2_hidden(C,B) ) )
| B != k1_tarski(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(C,sK1_skl(B,A))],[f4502]) ).
fof(f4505,plain,
! [X0,X1,X2] :
( X2 != X1
| r2_hidden(X2,X0)
| X0 != k1_tarski(X1) ),
inference(cnf_transformation,[status(thm)],[f4503]) ).
fof(f4583,plain,
! [A] :
( ( ? [B] : r2_hidden(B,A)
| A = k1_xboole_0 )
& ( ! [B] : ~ r2_hidden(B,A)
| A != k1_xboole_0 ) ),
inference(NNF_transformation,[status(thm)],[f29]) ).
fof(f4584,plain,
( ! [A] :
( ? [B] : r2_hidden(B,A)
| A = k1_xboole_0 )
& ! [A] :
( ! [B] : ~ r2_hidden(B,A)
| A != k1_xboole_0 ) ),
inference(miniscoping,[status(thm)],[f4583]) ).
fof(f4585,plain,
( ! [A] :
( r2_hidden(sK22_skl(A),A)
| A = k1_xboole_0 )
& ! [A] :
( ! [B] : ~ r2_hidden(B,A)
| A != k1_xboole_0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(B,sK22_skl(A))],[f4584]) ).
fof(f4586,plain,
! [X0,X1] :
( ~ r2_hidden(X1,X0)
| X0 != k1_xboole_0 ),
inference(cnf_transformation,[status(thm)],[f4585]) ).
fof(f4615,plain,
! [A] :
( ( A != k1_xboole_0
| v1_xboole_0(A) )
& ( A = k1_xboole_0
| ~ v1_xboole_0(A) ) ),
inference(NNF_transformation,[status(thm)],[f33]) ).
fof(f4616,plain,
( ! [A] :
( A != k1_xboole_0
| v1_xboole_0(A) )
& ! [A] :
( A = k1_xboole_0
| ~ v1_xboole_0(A) ) ),
inference(miniscoping,[status(thm)],[f4615]) ).
fof(f4617,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f4616]) ).
fof(f4693,plain,
! [A,B] :
( ~ r2_xboole_0(B,A)
| ~ r2_xboole_0(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f4694,plain,
! [X0,X1] :
( ~ r2_xboole_0(X1,X0)
| ~ r2_xboole_0(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4693]) ).
fof(f4709,plain,
! [X0] : k4_xboole_0(k1_xboole_0,X0) = k1_xboole_0,
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f4711,plain,
! [A] :
( A = k1_xboole_0
| ~ v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f67]) ).
fof(f4712,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f4711]) ).
fof(f4723,plain,
! [A] :
( A = k1_xboole_0
| ~ r1_tarski(A,k1_xboole_0) ),
inference(pre_NNF_transformation,[status(thm)],[f72]) ).
fof(f4724,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ r1_tarski(X0,k1_xboole_0) ),
inference(cnf_transformation,[status(thm)],[f4723]) ).
fof(f4728,plain,
! [X0,X1] : r1_tarski(X0,k2_xboole_0(X0,X1)),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f4740,plain,
! [A,B] :
( k2_xboole_0(A,B) = B
| ~ r1_tarski(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f81]) ).
fof(f4741,plain,
! [X0,X1] :
( k2_xboole_0(X0,X1) = X1
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4740]) ).
fof(f4800,plain,
! [X0,X1] : k4_xboole_0(k2_xboole_0(X0,X1),X1) = k4_xboole_0(X0,X1),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f4889,plain,
! [A,B] :
( ( k4_xboole_0(A,B) != A
| r1_xboole_0(A,B) )
& ( k4_xboole_0(A,B) = A
| ~ r1_xboole_0(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f152]) ).
fof(f4890,plain,
( ! [A,B] :
( k4_xboole_0(A,B) != A
| r1_xboole_0(A,B) )
& ! [A,B] :
( k4_xboole_0(A,B) = A
| ~ r1_xboole_0(A,B) ) ),
inference(miniscoping,[status(thm)],[f4889]) ).
fof(f4892,plain,
! [X0,X1] :
( k4_xboole_0(X0,X1) != X0
| r1_xboole_0(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4890]) ).
fof(f4928,plain,
! [A,B] :
( k4_xboole_0(B,A) != k1_xboole_0
| ~ r2_xboole_0(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f174]) ).
fof(f4929,plain,
! [X0,X1] :
( k4_xboole_0(X1,X0) != k1_xboole_0
| ~ r2_xboole_0(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4928]) ).
fof(f4952,plain,
! [A,B] :
( ( ? [C] :
( ( r1_tarski(C,A)
| r2_hidden(C,B) )
& ( ~ r1_tarski(C,A)
| ~ r2_hidden(C,B) ) )
| B = k1_zfmisc_1(A) )
& ( ! [C] :
( ( ~ r1_tarski(C,A)
| r2_hidden(C,B) )
& ( r1_tarski(C,A)
| ~ r2_hidden(C,B) ) )
| B != k1_zfmisc_1(A) ) ),
inference(NNF_transformation,[status(thm)],[f185]) ).
fof(f4953,plain,
( ! [A,B] :
( ? [C] :
( ( r1_tarski(C,A)
| r2_hidden(C,B) )
& ( ~ r1_tarski(C,A)
| ~ r2_hidden(C,B) ) )
| B = k1_zfmisc_1(A) )
& ! [A,B] :
( ( ! [C] :
( ~ r1_tarski(C,A)
| r2_hidden(C,B) )
& ! [C] :
( r1_tarski(C,A)
| ~ r2_hidden(C,B) ) )
| B != k1_zfmisc_1(A) ) ),
inference(miniscoping,[status(thm)],[f4952]) ).
fof(f4954,plain,
( ! [A,B] :
( ( ( r1_tarski(sK36_skl(B,A),A)
| r2_hidden(sK36_skl(B,A),B) )
& ( ~ r1_tarski(sK36_skl(B,A),A)
| ~ r2_hidden(sK36_skl(B,A),B) ) )
| B = k1_zfmisc_1(A) )
& ! [A,B] :
( ( ! [C] :
( ~ r1_tarski(C,A)
| r2_hidden(C,B) )
& ! [C] :
( r1_tarski(C,A)
| ~ r2_hidden(C,B) ) )
| B != k1_zfmisc_1(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl]),skolemize(C,sK36_skl(B,A))],[f4953]) ).
fof(f4956,plain,
! [X0,X1,X2] :
( ~ r1_tarski(X2,X1)
| r2_hidden(X2,X0)
| X0 != k1_zfmisc_1(X1) ),
inference(cnf_transformation,[status(thm)],[f4954]) ).
fof(f4970,plain,
k1_zfmisc_1(k1_xboole_0) = k1_tarski(k1_xboole_0),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f4971,plain,
k3_tarski(k1_xboole_0) = k1_xboole_0,
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f4986,plain,
! [X0,X1] : k2_xboole_0(k1_tarski(X0),k2_tarski(X0,X1)) = k2_tarski(X0,X1),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f4987,plain,
! [A,B] :
( A != B
| ~ r1_xboole_0(k1_tarski(A),k1_tarski(B)) ),
inference(pre_NNF_transformation,[status(thm)],[f204]) ).
fof(f4988,plain,
! [X0,X1] :
( X0 != X1
| ~ r1_xboole_0(k1_tarski(X0),k1_tarski(X1)) ),
inference(cnf_transformation,[status(thm)],[f4987]) ).
fof(f5080,plain,
! [X0,X1] : k2_xboole_0(k1_tarski(X0),X1) != k1_xboole_0,
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f5146,plain,
! [A,B,C] :
( k4_xboole_0(A,k2_tarski(B,C)) = k1_xboole_0
<=> ( A = k2_tarski(B,C)
| A = k1_tarski(C)
| A = k1_tarski(B)
| A = k1_xboole_0 ) ),
inference(pre_NNF_transformation,[status(thm)],[f263]) ).
fof(f5147,plain,
! [A,B,C] :
( ( ( A != k2_tarski(B,C)
& A != k1_tarski(C)
& A != k1_tarski(B)
& A != k1_xboole_0 )
| k4_xboole_0(A,k2_tarski(B,C)) = k1_xboole_0 )
& ( A = k2_tarski(B,C)
| A = k1_tarski(C)
| A = k1_tarski(B)
| A = k1_xboole_0
| k4_xboole_0(A,k2_tarski(B,C)) != k1_xboole_0 ) ),
inference(NNF_transformation,[status(thm)],[f5146]) ).
fof(f5148,plain,
( ! [A,B,C] :
( ( A != k2_tarski(B,C)
& A != k1_tarski(C)
& A != k1_tarski(B)
& A != k1_xboole_0 )
| k4_xboole_0(A,k2_tarski(B,C)) = k1_xboole_0 )
& ! [A,B,C] :
( A = k2_tarski(B,C)
| A = k1_tarski(C)
| A = k1_tarski(B)
| A = k1_xboole_0
| k4_xboole_0(A,k2_tarski(B,C)) != k1_xboole_0 ) ),
inference(miniscoping,[status(thm)],[f5147]) ).
fof(f5152,plain,
! [X0,X1,X2] :
( X0 != k1_tarski(X2)
| k4_xboole_0(X0,k2_tarski(X1,X2)) = k1_xboole_0 ),
inference(cnf_transformation,[status(thm)],[f5148]) ).
fof(f5325,plain,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(thm)],[f334]) ).
fof(f5349,plain,
! [X0] : k2_subset_1(X0) = X0,
inference(cnf_transformation,[status(thm)],[f345]) ).
fof(f5350,plain,
! [X0] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(thm)],[f349]) ).
fof(f5564,plain,
! [X0] : m1_subset_1(k2_subset_1(X0),k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(thm)],[f427]) ).
fof(f5621,plain,
! [A,B] :
( ( ( B = k1_setfam_1(A)
<=> B = k1_xboole_0 )
| A != k1_xboole_0 )
& ( ( B = k1_setfam_1(A)
<=> ! [C] :
( r2_hidden(C,B)
<=> ! [D] :
( r2_hidden(C,D)
| ~ r2_hidden(D,A) ) ) )
| A = k1_xboole_0 ) ),
inference(pre_NNF_transformation,[status(thm)],[f453]) ).
fof(f5622,plain,
! [A,B] :
( ( ( ( B != k1_xboole_0
| B = k1_setfam_1(A) )
& ( B = k1_xboole_0
| B != k1_setfam_1(A) ) )
| A != k1_xboole_0 )
& ( ( ( ? [C] :
( ( ! [D] :
( r2_hidden(C,D)
| ~ r2_hidden(D,A) )
| r2_hidden(C,B) )
& ( ? [D] :
( ~ r2_hidden(C,D)
& r2_hidden(D,A) )
| ~ r2_hidden(C,B) ) )
| B = k1_setfam_1(A) )
& ( ! [C] :
( ( ? [D] :
( ~ r2_hidden(C,D)
& r2_hidden(D,A) )
| r2_hidden(C,B) )
& ( ! [D] :
( r2_hidden(C,D)
| ~ r2_hidden(D,A) )
| ~ r2_hidden(C,B) ) )
| B != k1_setfam_1(A) ) )
| A = k1_xboole_0 ) ),
inference(NNF_transformation,[status(thm)],[f5621]) ).
fof(f5623,plain,
( ! [A] :
( ( ! [B] :
( B != k1_xboole_0
| B = k1_setfam_1(A) )
& ! [B] :
( B = k1_xboole_0
| B != k1_setfam_1(A) ) )
| A != k1_xboole_0 )
& ! [A] :
( ( ! [B] :
( ? [C] :
( ( ! [D] :
( r2_hidden(C,D)
| ~ r2_hidden(D,A) )
| r2_hidden(C,B) )
& ( ? [D] :
( ~ r2_hidden(C,D)
& r2_hidden(D,A) )
| ~ r2_hidden(C,B) ) )
| B = k1_setfam_1(A) )
& ! [B] :
( ( ! [C] :
( ? [D] :
( ~ r2_hidden(C,D)
& r2_hidden(D,A) )
| r2_hidden(C,B) )
& ! [C] :
( ! [D] :
( r2_hidden(C,D)
| ~ r2_hidden(D,A) )
| ~ r2_hidden(C,B) ) )
| B != k1_setfam_1(A) ) )
| A = k1_xboole_0 ) ),
inference(miniscoping,[status(thm)],[f5622]) ).
fof(f5624,plain,
( ! [A] :
( ( ! [B] :
( B != k1_xboole_0
| B = k1_setfam_1(A) )
& ! [B] :
( B = k1_xboole_0
| B != k1_setfam_1(A) ) )
| A != k1_xboole_0 )
& ! [A] :
( ( ! [B] :
( ( ( ! [D] :
( r2_hidden(sK91_skl(B,A),D)
| ~ r2_hidden(D,A) )
| r2_hidden(sK91_skl(B,A),B) )
& ( ( ~ r2_hidden(sK91_skl(B,A),sK92_skl(B,A))
& r2_hidden(sK92_skl(B,A),A) )
| ~ r2_hidden(sK91_skl(B,A),B) ) )
| B = k1_setfam_1(A) )
& ! [B] :
( ( ! [C] :
( ( ~ r2_hidden(C,sK90_skl(C,B,A))
& r2_hidden(sK90_skl(C,B,A),A) )
| r2_hidden(C,B) )
& ! [C] :
( ! [D] :
( r2_hidden(C,D)
| ~ r2_hidden(D,A) )
| ~ r2_hidden(C,B) ) )
| B != k1_setfam_1(A) ) )
| A = k1_xboole_0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK90_skl,sK91_skl,sK92_skl]),skolemize(D,sK90_skl(C,B,A)),skolemize(C,sK91_skl(B,A)),skolemize(D,sK92_skl(B,A))],[f5623]) ).
fof(f5631,plain,
! [X0,X1] :
( X1 = k1_xboole_0
| X1 != k1_setfam_1(X0)
| X0 != k1_xboole_0 ),
inference(cnf_transformation,[status(thm)],[f5624]) ).
fof(f5824,plain,
! [A,B] :
( ( ~ r1_tarski(A,B)
| m1_subset_1(A,k1_zfmisc_1(B)) )
& ( r1_tarski(A,B)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ) ),
inference(NNF_transformation,[status(thm)],[f540]) ).
fof(f5825,plain,
( ! [A,B] :
( ~ r1_tarski(A,B)
| m1_subset_1(A,k1_zfmisc_1(B)) )
& ! [A,B] :
( r1_tarski(A,B)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ) ),
inference(miniscoping,[status(thm)],[f5824]) ).
fof(f5826,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[status(thm)],[f5825]) ).
fof(f5834,plain,
( v1_relat_1(sK118_skl)
& v1_xboole_0(sK118_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK118_skl]),skolemize(A,sK118_skl)],[f543]) ).
fof(f5835,plain,
v1_xboole_0(sK118_skl),
inference(cnf_transformation,[status(thm)],[f5834]) ).
fof(f5891,plain,
! [X0,X1] : v1_relat_1(k2_zfmisc_1(X0,X1)),
inference(cnf_transformation,[status(thm)],[f566]) ).
fof(f6105,plain,
k6_relat_1(k1_xboole_0) = k1_xboole_0,
inference(cnf_transformation,[status(thm)],[f650]) ).
fof(f6465,plain,
! [X0] : v1_relat_1(k6_relat_1(X0)),
inference(cnf_transformation,[status(thm)],[f772]) ).
fof(f6483,plain,
( v1_funct_1(sK162_skl)
& v1_xboole_0(sK162_skl)
& v1_relat_1(sK162_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK162_skl]),skolemize(A,sK162_skl)],[f781]) ).
fof(f6485,plain,
v1_xboole_0(sK162_skl),
inference(cnf_transformation,[status(thm)],[f6483]) ).
fof(f7183,plain,
( v3_ordinal1(sK235_skl)
& v2_ordinal1(sK235_skl)
& v1_ordinal1(sK235_skl)
& v1_xboole_0(sK235_skl)
& v2_funct_1(sK235_skl)
& v1_funct_1(sK235_skl)
& v1_relat_1(sK235_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK235_skl]),skolemize(A,sK235_skl)],[f1040]) ).
fof(f7187,plain,
v1_xboole_0(sK235_skl),
inference(cnf_transformation,[status(thm)],[f7183]) ).
fof(f7248,plain,
! [X0] : X0 != k1_ordinal1(X0),
inference(cnf_transformation,[status(thm)],[f1062]) ).
fof(f7402,plain,
? [A] :
( ! [B] :
( ! [C] :
( k1_funct_1(A,B) = f2_s4_ordinal1(C)
| C != k2_ordinal1(A,B)
| ~ r2_hidden(B,f1_s4_ordinal1)
| ~ v5_ordinal1(C)
| ~ v1_funct_1(C)
| ~ v1_relat_1(C) )
| ~ v3_ordinal1(B) )
& k1_relat_1(A) = f1_s4_ordinal1
& v5_ordinal1(A)
& v1_funct_1(A)
& v1_relat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f1110]) ).
fof(f7403,plain,
( ! [B] :
( ! [C] :
( k1_funct_1(sK258_skl,B) = f2_s4_ordinal1(C)
| C != k2_ordinal1(sK258_skl,B)
| ~ r2_hidden(B,f1_s4_ordinal1)
| ~ v5_ordinal1(C)
| ~ v1_funct_1(C)
| ~ v1_relat_1(C) )
| ~ v3_ordinal1(B) )
& k1_relat_1(sK258_skl) = f1_s4_ordinal1
& v5_ordinal1(sK258_skl)
& v1_funct_1(sK258_skl)
& v1_relat_1(sK258_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK258_skl]),skolemize(A,sK258_skl)],[f7402]) ).
fof(f7404,plain,
v1_relat_1(sK258_skl),
inference(cnf_transformation,[status(thm)],[f7403]) ).
fof(f7405,plain,
v1_funct_1(sK258_skl),
inference(cnf_transformation,[status(thm)],[f7403]) ).
fof(f7436,plain,
! [A,B,C] :
( v1_relat_1(C)
| ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(pre_NNF_transformation,[status(thm)],[f1120]) ).
fof(f7437,plain,
! [C] :
( v1_relat_1(C)
| ! [A,B] : ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(miniscoping,[status(thm)],[f7436]) ).
fof(f7438,plain,
! [X0,X1,X2] :
( v1_relat_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[status(thm)],[f7437]) ).
fof(f7457,plain,
! [A,B] :
( m2_relset_1(B,k1_relat_1(B),A)
| ~ r1_tarski(k2_relat_1(B),A)
| ~ v1_relat_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f1131]) ).
fof(f7458,plain,
! [B] :
( ! [A] :
( m2_relset_1(B,k1_relat_1(B),A)
| ~ r1_tarski(k2_relat_1(B),A) )
| ~ v1_relat_1(B) ),
inference(miniscoping,[status(thm)],[f7457]) ).
fof(f7459,plain,
! [X0,X1] :
( m2_relset_1(X0,k1_relat_1(X0),X1)
| ~ r1_tarski(k2_relat_1(X0),X1)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f7458]) ).
fof(f7498,plain,
! [X0,X1] : m2_relset_1(k1_xboole_0,X0,X1),
inference(cnf_transformation,[status(thm)],[f1146]) ).
fof(f7669,plain,
( v1_xboole_0(sK279_skl)
& v2_funct_1(sK279_skl)
& v1_funct_1(sK279_skl)
& v1_relat_1(sK279_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK279_skl]),skolemize(A,sK279_skl)],[f1209]) ).
fof(f7673,plain,
v1_xboole_0(sK279_skl),
inference(cnf_transformation,[status(thm)],[f7669]) ).
fof(f8083,plain,
? [A] :
( ! [B] :
( ( ( k1_funct_1(A,B) = f3_s1_partfun1(B)
| p1_s1_partfun1(B) )
& ( k1_funct_1(A,B) = f2_s1_partfun1(B)
| ~ p1_s1_partfun1(B) ) )
| ~ r2_hidden(B,f1_s1_partfun1) )
& k1_relat_1(A) = f1_s1_partfun1
& v1_funct_1(A)
& v1_relat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f1408]) ).
fof(f8084,plain,
( ! [B] :
( ( ( k1_funct_1(sK302_skl,B) = f3_s1_partfun1(B)
| p1_s1_partfun1(B) )
& ( k1_funct_1(sK302_skl,B) = f2_s1_partfun1(B)
| ~ p1_s1_partfun1(B) ) )
| ~ r2_hidden(B,f1_s1_partfun1) )
& k1_relat_1(sK302_skl) = f1_s1_partfun1
& v1_funct_1(sK302_skl)
& v1_relat_1(sK302_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK302_skl]),skolemize(A,sK302_skl)],[f8083]) ).
fof(f8085,plain,
v1_relat_1(sK302_skl),
inference(cnf_transformation,[status(thm)],[f8084]) ).
fof(f8086,plain,
v1_funct_1(sK302_skl),
inference(cnf_transformation,[status(thm)],[f8084]) ).
fof(f8164,plain,
! [X0] : k6_partfun1(X0) = k6_relat_1(X0),
inference(cnf_transformation,[status(thm)],[f1423]) ).
fof(f8684,plain,
! [A,B] :
( ( m2_relset_1(B,k1_relat_1(B),A)
& v1_funct_2(B,k1_relat_1(B),A)
& v1_funct_1(B) )
| ~ r1_tarski(k2_relat_1(B),A)
| ~ v1_funct_1(B)
| ~ v1_relat_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f1567]) ).
fof(f8685,plain,
! [B] :
( ! [A] :
( ( m2_relset_1(B,k1_relat_1(B),A)
& v1_funct_2(B,k1_relat_1(B),A)
& v1_funct_1(B) )
| ~ r1_tarski(k2_relat_1(B),A) )
| ~ v1_funct_1(B)
| ~ v1_relat_1(B) ),
inference(miniscoping,[status(thm)],[f8684]) ).
fof(f8687,plain,
! [X0,X1] :
( v1_funct_2(X0,k1_relat_1(X0),X1)
| ~ r1_tarski(k2_relat_1(X0),X1)
| ~ v1_funct_1(X0)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f8685]) ).
fof(f9133,plain,
? [A] :
( ! [B] :
( k8_funct_2(f1_s4_funct_2,f2_s4_funct_2,A,B) = f3_s4_funct_2(B)
| ~ m1_subset_1(B,f1_s4_funct_2) )
& m2_relset_1(A,f1_s4_funct_2,f2_s4_funct_2)
& v1_funct_2(A,f1_s4_funct_2,f2_s4_funct_2)
& v1_funct_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f1740]) ).
fof(f9134,plain,
( ! [B] :
( k8_funct_2(f1_s4_funct_2,f2_s4_funct_2,sK438_skl,B) = f3_s4_funct_2(B)
| ~ m1_subset_1(B,f1_s4_funct_2) )
& m2_relset_1(sK438_skl,f1_s4_funct_2,f2_s4_funct_2)
& v1_funct_2(sK438_skl,f1_s4_funct_2,f2_s4_funct_2)
& v1_funct_1(sK438_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK438_skl]),skolemize(A,sK438_skl)],[f9133]) ).
fof(f9135,plain,
v1_funct_1(sK438_skl),
inference(cnf_transformation,[status(thm)],[f9134]) ).
fof(f9163,plain,
? [A] :
( ! [B] :
( ! [C] :
( k1_funct_1(A,k4_tarski(B,C)) = f4_s8_funct_2(B,C)
| ~ m1_subset_1(C,f2_s8_funct_2) )
| ~ m1_subset_1(B,f1_s8_funct_2) )
& m2_relset_1(A,k2_zfmisc_1(f1_s8_funct_2,f2_s8_funct_2),f3_s8_funct_2)
& v1_funct_2(A,k2_zfmisc_1(f1_s8_funct_2,f2_s8_funct_2),f3_s8_funct_2)
& v1_funct_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f1744]) ).
fof(f9164,plain,
( ! [B] :
( ! [C] :
( k1_funct_1(sK447_skl,k4_tarski(B,C)) = f4_s8_funct_2(B,C)
| ~ m1_subset_1(C,f2_s8_funct_2) )
| ~ m1_subset_1(B,f1_s8_funct_2) )
& m2_relset_1(sK447_skl,k2_zfmisc_1(f1_s8_funct_2,f2_s8_funct_2),f3_s8_funct_2)
& v1_funct_2(sK447_skl,k2_zfmisc_1(f1_s8_funct_2,f2_s8_funct_2),f3_s8_funct_2)
& v1_funct_1(sK447_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK447_skl]),skolemize(A,sK447_skl)],[f9163]) ).
fof(f9165,plain,
v1_funct_1(sK447_skl),
inference(cnf_transformation,[status(thm)],[f9164]) ).
fof(f9178,plain,
? [A] :
( ! [B] :
( k8_funct_2(f1_s10_funct_2,f2_s10_funct_2,A,B) = f5_s10_funct_2(B)
| B = f3_s10_funct_2
| ~ m1_subset_1(B,f1_s10_funct_2) )
& k8_funct_2(f1_s10_funct_2,f2_s10_funct_2,A,f3_s10_funct_2) = f4_s10_funct_2
& m2_relset_1(A,f1_s10_funct_2,f2_s10_funct_2)
& v1_funct_2(A,f1_s10_funct_2,f2_s10_funct_2)
& v1_funct_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f1746]) ).
fof(f9179,plain,
( ! [B] :
( k8_funct_2(f1_s10_funct_2,f2_s10_funct_2,sK450_skl,B) = f5_s10_funct_2(B)
| B = f3_s10_funct_2
| ~ m1_subset_1(B,f1_s10_funct_2) )
& k8_funct_2(f1_s10_funct_2,f2_s10_funct_2,sK450_skl,f3_s10_funct_2) = f4_s10_funct_2
& m2_relset_1(sK450_skl,f1_s10_funct_2,f2_s10_funct_2)
& v1_funct_2(sK450_skl,f1_s10_funct_2,f2_s10_funct_2)
& v1_funct_1(sK450_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK450_skl]),skolemize(A,sK450_skl)],[f9178]) ).
fof(f9180,plain,
v1_funct_1(sK450_skl),
inference(cnf_transformation,[status(thm)],[f9179]) ).
fof(f10106,plain,
~ v1_xboole_0(k5_ordinal2),
inference(cnf_transformation,[status(thm)],[f2024]) ).
fof(f10172,plain,
! [X0] : r1_tarski(k3_ordinal2(X0),X0),
inference(cnf_transformation,[status(thm)],[f2046]) ).
fof(f10185,plain,
k4_ordinal2 = k1_ordinal1(k1_xboole_0),
inference(cnf_transformation,[status(thm)],[f2051]) ).
fof(f10511,plain,
? [A] :
( ! [B] :
( k1_funct_1(A,B) = f4_s5_ordinal2(B,k2_ordinal1(A,B))
| B = k1_xboole_0
| ~ v4_ordinal1(B)
| ~ r2_hidden(B,f1_s5_ordinal2)
| ~ v3_ordinal1(B) )
& ! [B] :
( k1_funct_1(A,k1_ordinal1(B)) = f3_s5_ordinal2(B,k1_funct_1(A,B))
| ~ r2_hidden(k1_ordinal1(B),f1_s5_ordinal2)
| ~ v3_ordinal1(B) )
& ( k1_funct_1(A,k1_xboole_0) = f2_s5_ordinal2
| ~ r2_hidden(k1_xboole_0,f1_s5_ordinal2) )
& k1_relat_1(A) = f1_s5_ordinal2
& v5_ordinal1(A)
& v1_funct_1(A)
& v1_relat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2121]) ).
fof(f10512,plain,
( ! [B] :
( k1_funct_1(sK631_skl,B) = f4_s5_ordinal2(B,k2_ordinal1(sK631_skl,B))
| B = k1_xboole_0
| ~ v4_ordinal1(B)
| ~ r2_hidden(B,f1_s5_ordinal2)
| ~ v3_ordinal1(B) )
& ! [B] :
( k1_funct_1(sK631_skl,k1_ordinal1(B)) = f3_s5_ordinal2(B,k1_funct_1(sK631_skl,B))
| ~ r2_hidden(k1_ordinal1(B),f1_s5_ordinal2)
| ~ v3_ordinal1(B) )
& ( k1_funct_1(sK631_skl,k1_xboole_0) = f2_s5_ordinal2
| ~ r2_hidden(k1_xboole_0,f1_s5_ordinal2) )
& k1_relat_1(sK631_skl) = f1_s5_ordinal2
& v5_ordinal1(sK631_skl)
& v1_funct_1(sK631_skl)
& v1_relat_1(sK631_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK631_skl]),skolemize(A,sK631_skl)],[f10511]) ).
fof(f10513,plain,
v1_relat_1(sK631_skl),
inference(cnf_transformation,[status(thm)],[f10512]) ).
fof(f10514,plain,
v1_funct_1(sK631_skl),
inference(cnf_transformation,[status(thm)],[f10512]) ).
fof(f10629,plain,
? [A] :
( ! [B] :
( k1_funct_1(A,B) = f4_s11_ordinal2(B,k2_ordinal1(A,B))
| B = k1_xboole_0
| ~ v4_ordinal1(B)
| ~ r2_hidden(B,f1_s11_ordinal2)
| ~ v3_ordinal1(B) )
& ! [B] :
( k1_funct_1(A,k1_ordinal1(B)) = f3_s11_ordinal2(B,k1_funct_1(A,B))
| ~ r2_hidden(k1_ordinal1(B),f1_s11_ordinal2)
| ~ v3_ordinal1(B) )
& ( k1_funct_1(A,k1_xboole_0) = f2_s11_ordinal2
| ~ r2_hidden(k1_xboole_0,f1_s11_ordinal2) )
& k1_relat_1(A) = f1_s11_ordinal2
& v1_ordinal2(A)
& v5_ordinal1(A)
& v1_funct_1(A)
& v1_relat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2127]) ).
fof(f10630,plain,
( ! [B] :
( k1_funct_1(sK650_skl,B) = f4_s11_ordinal2(B,k2_ordinal1(sK650_skl,B))
| B = k1_xboole_0
| ~ v4_ordinal1(B)
| ~ r2_hidden(B,f1_s11_ordinal2)
| ~ v3_ordinal1(B) )
& ! [B] :
( k1_funct_1(sK650_skl,k1_ordinal1(B)) = f3_s11_ordinal2(B,k1_funct_1(sK650_skl,B))
| ~ r2_hidden(k1_ordinal1(B),f1_s11_ordinal2)
| ~ v3_ordinal1(B) )
& ( k1_funct_1(sK650_skl,k1_xboole_0) = f2_s11_ordinal2
| ~ r2_hidden(k1_xboole_0,f1_s11_ordinal2) )
& k1_relat_1(sK650_skl) = f1_s11_ordinal2
& v1_ordinal2(sK650_skl)
& v5_ordinal1(sK650_skl)
& v1_funct_1(sK650_skl)
& v1_relat_1(sK650_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK650_skl]),skolemize(A,sK650_skl)],[f10629]) ).
fof(f10631,plain,
v1_relat_1(sK650_skl),
inference(cnf_transformation,[status(thm)],[f10630]) ).
fof(f10632,plain,
v1_funct_1(sK650_skl),
inference(cnf_transformation,[status(thm)],[f10630]) ).
fof(f10916,plain,
~ v1_xboole_0(k1_numbers),
inference(cnf_transformation,[status(thm)],[f2206]) ).
fof(f10918,plain,
~ v1_xboole_0(k3_numbers),
inference(cnf_transformation,[status(thm)],[f2208]) ).
fof(f10923,plain,
r2_xboole_0(k1_numbers,k2_numbers),
inference(cnf_transformation,[status(thm)],[f2213]) ).
fof(f10924,plain,
r2_xboole_0(k3_numbers,k1_numbers),
inference(cnf_transformation,[status(thm)],[f2214]) ).
fof(f10925,plain,
r2_xboole_0(k3_numbers,k2_numbers),
inference(cnf_transformation,[status(thm)],[f2215]) ).
fof(f10926,plain,
r2_xboole_0(k4_numbers,k3_numbers),
inference(cnf_transformation,[status(thm)],[f2216]) ).
fof(f10927,plain,
r2_xboole_0(k4_numbers,k1_numbers),
inference(cnf_transformation,[status(thm)],[f2217]) ).
fof(f10928,plain,
r2_xboole_0(k4_numbers,k2_numbers),
inference(cnf_transformation,[status(thm)],[f2218]) ).
fof(f10929,plain,
r2_xboole_0(k5_numbers,k4_numbers),
inference(cnf_transformation,[status(thm)],[f2219]) ).
fof(f10930,plain,
r2_xboole_0(k5_numbers,k3_numbers),
inference(cnf_transformation,[status(thm)],[f2220]) ).
fof(f10931,plain,
r2_xboole_0(k5_numbers,k1_numbers),
inference(cnf_transformation,[status(thm)],[f2221]) ).
fof(f10932,plain,
r2_xboole_0(k5_numbers,k2_numbers),
inference(cnf_transformation,[status(thm)],[f2222]) ).
fof(f10942,plain,
r1_tarski(k5_numbers,k2_numbers),
inference(cnf_transformation,[status(thm)],[f2232]) ).
fof(f10943,plain,
k1_numbers != k2_numbers,
inference(cnf_transformation,[status(thm)],[f2233]) ).
fof(f10944,plain,
k3_numbers != k1_numbers,
inference(cnf_transformation,[status(thm)],[f2234]) ).
fof(f10945,plain,
k3_numbers != k2_numbers,
inference(cnf_transformation,[status(thm)],[f2235]) ).
fof(f10946,plain,
k4_numbers != k3_numbers,
inference(cnf_transformation,[status(thm)],[f2236]) ).
fof(f10947,plain,
k4_numbers != k1_numbers,
inference(cnf_transformation,[status(thm)],[f2237]) ).
fof(f10948,plain,
k4_numbers != k2_numbers,
inference(cnf_transformation,[status(thm)],[f2238]) ).
fof(f10949,plain,
k5_numbers != k4_numbers,
inference(cnf_transformation,[status(thm)],[f2239]) ).
fof(f10950,plain,
k5_numbers != k3_numbers,
inference(cnf_transformation,[status(thm)],[f2240]) ).
fof(f10951,plain,
k5_numbers != k1_numbers,
inference(cnf_transformation,[status(thm)],[f2241]) ).
fof(f10952,plain,
k5_numbers != k2_numbers,
inference(cnf_transformation,[status(thm)],[f2242]) ).
fof(f10954,plain,
k5_numbers = k5_ordinal2,
inference(cnf_transformation,[status(thm)],[f2248]) ).
fof(f11697,plain,
np__0 = k1_xboole_0,
inference(cnf_transformation,[status(thm)],[f2485]) ).
fof(f11790,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[status(thm)],[f2534]) ).
fof(f11793,plain,
v1_funct_1(k1_xboole_0),
inference(cnf_transformation,[status(thm)],[f2534]) ).
fof(f11803,plain,
( v1_finseq_1(sK727_skl)
& v1_finset_1(sK727_skl)
& v2_funct_1(sK727_skl)
& v1_funct_1(sK727_skl)
& v1_relat_1(sK727_skl)
& v1_xboole_0(sK727_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK727_skl]),skolemize(A,sK727_skl)],[f2536]) ).
fof(f11804,plain,
v1_xboole_0(sK727_skl),
inference(cnf_transformation,[status(thm)],[f11803]) ).
fof(f11826,plain,
( ! [A,B] : v1_funct_1(k10_finseq_1(A,B))
& ! [A,B] : v1_relat_1(k10_finseq_1(A,B)) ),
inference(miniscoping,[status(thm)],[f2540]) ).
fof(f11827,plain,
! [X0,X1] : v1_relat_1(k10_finseq_1(X0,X1)),
inference(cnf_transformation,[status(thm)],[f11826]) ).
fof(f11828,plain,
! [X0,X1] : v1_funct_1(k10_finseq_1(X0,X1)),
inference(cnf_transformation,[status(thm)],[f11826]) ).
fof(f11852,plain,
( v1_finset_1(sK730_skl)
& v2_funct_1(sK730_skl)
& v1_funct_1(sK730_skl)
& v1_relat_1(sK730_skl)
& v1_xboole_0(sK730_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK730_skl]),skolemize(A,sK730_skl)],[f2547]) ).
fof(f11853,plain,
v1_xboole_0(sK730_skl),
inference(cnf_transformation,[status(thm)],[f11852]) ).
fof(f13278,plain,
? [A] :
( ! [B] :
( k1_funct_1(A,B) = f2_s1_funct_5(B)
| ~ r2_hidden(B,f1_s1_funct_5)
| ~ v1_funct_1(B)
| ~ v1_relat_1(B) )
& k1_relat_1(A) = f1_s1_funct_5
& v1_funct_1(A)
& v1_relat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3068]) ).
fof(f13279,plain,
( ! [B] :
( k1_funct_1(sK828_skl,B) = f2_s1_funct_5(B)
| ~ r2_hidden(B,f1_s1_funct_5)
| ~ v1_funct_1(B)
| ~ v1_relat_1(B) )
& k1_relat_1(sK828_skl) = f1_s1_funct_5
& v1_funct_1(sK828_skl)
& v1_relat_1(sK828_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK828_skl]),skolemize(A,sK828_skl)],[f13278]) ).
fof(f13280,plain,
v1_relat_1(sK828_skl),
inference(cnf_transformation,[status(thm)],[f13279]) ).
fof(f13281,plain,
v1_funct_1(sK828_skl),
inference(cnf_transformation,[status(thm)],[f13279]) ).
fof(f17473,plain,
! [A,B] :
( ( v1_funct_1(k5_relset_2(A,B))
& v1_relat_1(k5_relset_2(A,B)) )
| ~ v1_relat_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f4461]) ).
fof(f17474,plain,
! [B] :
( ( ! [A] : v1_funct_1(k5_relset_2(A,B))
& ! [A] : v1_relat_1(k5_relset_2(A,B)) )
| ~ v1_relat_1(B) ),
inference(miniscoping,[status(thm)],[f17473]) ).
fof(f17475,plain,
! [X0,X1] :
( v1_relat_1(k5_relset_2(X1,X0))
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f17474]) ).
fof(f17476,plain,
! [X0,X1] :
( v1_funct_1(k5_relset_2(X1,X0))
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f17474]) ).
fof(f17545,plain,
! [A,B] :
( ! [C] :
( ( C = k5_relset_2(A,B)
<=> ( ! [D] :
( k1_funct_1(C,D) = k9_relat_1(B,D)
| ~ r1_tarski(D,A) )
& k1_relat_1(C) = k1_zfmisc_1(A) ) )
| ~ v1_funct_1(C)
| ~ v1_relat_1(C) )
| ~ v1_relat_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f4489]) ).
fof(f17546,plain,
! [A,B] :
( ! [C] :
( ( ( ? [D] :
( k1_funct_1(C,D) != k9_relat_1(B,D)
& r1_tarski(D,A) )
| k1_relat_1(C) != k1_zfmisc_1(A)
| C = k5_relset_2(A,B) )
& ( ( ! [D] :
( k1_funct_1(C,D) = k9_relat_1(B,D)
| ~ r1_tarski(D,A) )
& k1_relat_1(C) = k1_zfmisc_1(A) )
| C != k5_relset_2(A,B) ) )
| ~ v1_funct_1(C)
| ~ v1_relat_1(C) )
| ~ v1_relat_1(B) ),
inference(NNF_transformation,[status(thm)],[f17545]) ).
fof(f17547,plain,
! [B] :
( ! [C] :
( ( ! [A] :
( ? [D] :
( k1_funct_1(C,D) != k9_relat_1(B,D)
& r1_tarski(D,A) )
| k1_relat_1(C) != k1_zfmisc_1(A)
| C = k5_relset_2(A,B) )
& ! [A] :
( ( ! [D] :
( k1_funct_1(C,D) = k9_relat_1(B,D)
| ~ r1_tarski(D,A) )
& k1_relat_1(C) = k1_zfmisc_1(A) )
| C != k5_relset_2(A,B) ) )
| ~ v1_funct_1(C)
| ~ v1_relat_1(C) )
| ~ v1_relat_1(B) ),
inference(miniscoping,[status(thm)],[f17546]) ).
fof(f17548,plain,
! [B] :
( ! [C] :
( ( ! [A] :
( ( k1_funct_1(C,sK1204_skl(A,C,B)) != k9_relat_1(B,sK1204_skl(A,C,B))
& r1_tarski(sK1204_skl(A,C,B),A) )
| k1_relat_1(C) != k1_zfmisc_1(A)
| C = k5_relset_2(A,B) )
& ! [A] :
( ( ! [D] :
( k1_funct_1(C,D) = k9_relat_1(B,D)
| ~ r1_tarski(D,A) )
& k1_relat_1(C) = k1_zfmisc_1(A) )
| C != k5_relset_2(A,B) ) )
| ~ v1_funct_1(C)
| ~ v1_relat_1(C) )
| ~ v1_relat_1(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1204_skl]),skolemize(D,sK1204_skl(A,C,B))],[f17547]) ).
fof(f17549,plain,
! [X0,X1,X2] :
( k1_relat_1(X1) = k1_zfmisc_1(X2)
| X1 != k5_relset_2(X2,X0)
| ~ v1_funct_1(X1)
| ~ v1_relat_1(X1)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f17548]) ).
fof(f17556,plain,
! [A,B,C] :
( r1_tarski(k2_relat_1(k5_relset_2(A,C)),k1_zfmisc_1(k2_relat_1(C)))
| ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(pre_NNF_transformation,[status(thm)],[f4491]) ).
fof(f17557,plain,
! [A,C] :
( r1_tarski(k2_relat_1(k5_relset_2(A,C)),k1_zfmisc_1(k2_relat_1(C)))
| ! [B] : ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(miniscoping,[status(thm)],[f17556]) ).
fof(f17558,plain,
! [X0,X1,X2] :
( r1_tarski(k2_relat_1(k5_relset_2(X1,X0)),k1_zfmisc_1(k2_relat_1(X0)))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[status(thm)],[f17557]) ).
fof(f17559,plain,
? [A,B,C] :
( ( ~ m2_relset_1(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))
| ~ v1_funct_2(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))
| ~ v1_funct_1(k5_relset_2(A,C)) )
& m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(pre_NNF_transformation,[status(thm)],[f4493]) ).
fof(f17560,plain,
? [A,C] :
( ( ~ m2_relset_1(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))
| ~ v1_funct_2(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))
| ~ v1_funct_1(k5_relset_2(A,C)) )
& ? [B] : m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(miniscoping,[status(thm)],[f17559]) ).
fof(f17561,plain,
( ( ~ m2_relset_1(k5_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(sK1205_skl),k1_zfmisc_1(k2_relat_1(sK1206_skl)))
| ~ v1_funct_2(k5_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(sK1205_skl),k1_zfmisc_1(k2_relat_1(sK1206_skl)))
| ~ v1_funct_1(k5_relset_2(sK1205_skl,sK1206_skl)) )
& m1_subset_1(sK1206_skl,k1_zfmisc_1(k2_zfmisc_1(sK1205_skl,sK1207_skl))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1205_skl,sK1206_skl,sK1207_skl]),skolemize(A,sK1205_skl),skolemize(C,sK1206_skl),skolemize(B,sK1207_skl)],[f17560]) ).
fof(f17562,plain,
m1_subset_1(sK1206_skl,k1_zfmisc_1(k2_zfmisc_1(sK1205_skl,sK1207_skl))),
inference(cnf_transformation,[status(thm)],[f17561]) ).
fof(f17563,plain,
( ~ m2_relset_1(k5_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(sK1205_skl),k1_zfmisc_1(k2_relat_1(sK1206_skl)))
| ~ v1_funct_2(k5_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(sK1205_skl),k1_zfmisc_1(k2_relat_1(sK1206_skl)))
| ~ v1_funct_1(k5_relset_2(sK1205_skl,sK1206_skl)) ),
inference(cnf_transformation,[status(thm)],[f17561]) ).
fof(f19129,definition,
! [X1] :
( sQ84_spl
<=> ( ~ v1_funct_1(X1)
| ~ v1_relat_1(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f19130,plain,
! [X0] :
( ~ sQ84_spl
| ~ v1_funct_1(X0)
| ~ v1_relat_1(X0) ),
inference(component_clause,[status(thm)],[f19129]) ).
fof(f20392,definition,
( sQ419_spl
<=> v1_funct_1(k5_relset_2(sK1205_skl,sK1206_skl)) ),
introduced(definition,[new_symbols(definition,[sQ419_spl])],[split_symbol_definition]) ).
fof(f20393,plain,
( ~ sQ419_spl
| v1_funct_1(k5_relset_2(sK1205_skl,sK1206_skl)) ),
inference(component_clause,[status(thm)],[f20392]) ).
fof(f20394,plain,
( sQ419_spl
| ~ v1_funct_1(k5_relset_2(sK1205_skl,sK1206_skl)) ),
inference(component_clause,[status(thm)],[f20392]) ).
fof(f20395,definition,
( sQ420_spl
<=> v1_funct_2(k5_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(sK1205_skl),k1_zfmisc_1(k2_relat_1(sK1206_skl))) ),
introduced(definition,[new_symbols(definition,[sQ420_spl])],[split_symbol_definition]) ).
fof(f20397,plain,
( sQ420_spl
| ~ v1_funct_2(k5_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(sK1205_skl),k1_zfmisc_1(k2_relat_1(sK1206_skl))) ),
inference(component_clause,[status(thm)],[f20395]) ).
fof(f20398,definition,
( sQ421_spl
<=> m2_relset_1(k5_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(sK1205_skl),k1_zfmisc_1(k2_relat_1(sK1206_skl))) ),
introduced(definition,[new_symbols(definition,[sQ421_spl])],[split_symbol_definition]) ).
fof(f20400,plain,
( sQ421_spl
| ~ m2_relset_1(k5_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(sK1205_skl),k1_zfmisc_1(k2_relat_1(sK1206_skl))) ),
inference(component_clause,[status(thm)],[f20398]) ).
fof(f20401,plain,
( ~ sQ421_spl
| ~ sQ420_spl
| ~ sQ419_spl ),
inference(split_clause,[status(thm)],[f17563,f20392,f20395,f20398]) ).
fof(f21038,plain,
! [X0] : r2_hidden(X0,k1_tarski(X0)),
inference(destructive_equality_resolution,[status(thm)],[f4505]) ).
fof(f21047,plain,
! [X0] : ~ r2_hidden(X0,k1_xboole_0),
inference(destructive_equality_resolution,[status(thm)],[f4586]) ).
fof(f21064,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| r2_hidden(X0,k1_zfmisc_1(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f4956]) ).
fof(f21067,plain,
! [X0] : ~ r1_xboole_0(k1_tarski(X0),k1_tarski(X0)),
inference(destructive_equality_resolution,[status(thm)],[f4988]) ).
fof(f21081,plain,
! [X0,X1] : k4_xboole_0(k1_tarski(X0),k2_tarski(X1,X0)) = k1_xboole_0,
inference(destructive_equality_resolution,[status(thm)],[f5152]) ).
fof(f21092,plain,
k1_setfam_1(k1_xboole_0) = k1_xboole_0,
inference(destructive_equality_resolution,[status(thm)],[f5631]) ).
fof(f21911,plain,
! [X0,X1] :
( k1_relat_1(k5_relset_2(X1,X0)) = k1_zfmisc_1(X1)
| ~ v1_funct_1(k5_relset_2(X1,X0))
| ~ v1_relat_1(k5_relset_2(X1,X0))
| ~ v1_relat_1(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f17549]) ).
fof(f22127,plain,
r1_tarski(sK1206_skl,k2_zfmisc_1(sK1205_skl,sK1207_skl)),
inference(resolution,[status(thm)],[f5826,f17562]) ).
fof(f22129,plain,
! [X0] : r1_tarski(k1_xboole_0,X0),
inference(resolution,[status(thm)],[f5350,f5826]) ).
fof(f22162,plain,
( sQ419_spl
| ~ v1_relat_1(sK1206_skl) ),
inference(resolution,[status(thm)],[f17476,f20394]) ).
fof(f22246,definition,
( sQ591_spl
<=> sK162_skl = k1_xboole_0 ),
introduced(definition,[new_symbols(definition,[sQ591_spl])],[split_symbol_definition]) ).
fof(f22248,plain,
( sQ591_spl
| sK162_skl != k1_xboole_0 ),
inference(component_clause,[status(thm)],[f22246]) ).
fof(f22281,definition,
( sQ601_spl
<=> sK118_skl = k1_xboole_0 ),
introduced(definition,[new_symbols(definition,[sQ601_spl])],[split_symbol_definition]) ).
fof(f22283,plain,
( sQ601_spl
| sK118_skl != k1_xboole_0 ),
inference(component_clause,[status(thm)],[f22281]) ).
fof(f22394,definition,
( sQ616_spl
<=> sK235_skl = k1_xboole_0 ),
introduced(definition,[new_symbols(definition,[sQ616_spl])],[split_symbol_definition]) ).
fof(f22396,plain,
( sQ616_spl
| sK235_skl != k1_xboole_0 ),
inference(component_clause,[status(thm)],[f22394]) ).
fof(f22484,definition,
! [X1] :
( sQ624_spl
<=> r2_hidden(sK7_skl(k1_xboole_0),X1) ),
introduced(definition,[new_symbols(definition,[sQ624_spl])],[split_symbol_definition]) ).
fof(f22485,plain,
! [X0] :
( ~ sQ624_spl
| r2_hidden(sK7_skl(k1_xboole_0),X0) ),
inference(component_clause,[status(thm)],[f22484]) ).
fof(f22591,definition,
( sQ638_spl
<=> sK279_skl = k1_xboole_0 ),
introduced(definition,[new_symbols(definition,[sQ638_spl])],[split_symbol_definition]) ).
fof(f22593,plain,
( sQ638_spl
| sK279_skl != k1_xboole_0 ),
inference(component_clause,[status(thm)],[f22591]) ).
fof(f22653,plain,
! [X0,X1] :
( sQ419_spl
| ~ m1_subset_1(sK1206_skl,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(resolution,[status(thm)],[f7438,f22162]) ).
fof(f22677,plain,
( sQ419_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f17562,f22653]) ).
fof(f22683,plain,
sQ419_spl,
inference(contradiction_clause,[status(thm)],[f22677]) ).
fof(f23085,plain,
~ v1_xboole_0(k5_numbers),
inference(backward_demodulation,[status(thm)],[f10954,f10106]) ).
fof(f23235,plain,
( sQ616_spl
| sK235_skl != np__0 ),
inference(backward_demodulation,[status(thm)],[f11697,f22396]) ).
fof(f23253,plain,
( sQ591_spl
| sK162_skl != np__0 ),
inference(backward_demodulation,[status(thm)],[f11697,f22248]) ).
fof(f23258,plain,
( sQ601_spl
| sK118_skl != np__0 ),
inference(backward_demodulation,[status(thm)],[f11697,f22283]) ).
fof(f23272,plain,
! [X0] : r1_tarski(np__0,X0),
inference(backward_demodulation,[status(thm)],[f11697,f22129]) ).
fof(f23273,plain,
! [X0] : m1_subset_1(np__0,k1_zfmisc_1(X0)),
inference(backward_demodulation,[status(thm)],[f11697,f5350]) ).
fof(f23276,plain,
! [X0,X1] : m2_relset_1(np__0,X0,X1),
inference(backward_demodulation,[status(thm)],[f11697,f7498]) ).
fof(f23292,plain,
v1_xboole_0(np__0),
inference(forward_demodulation,[status(thm)],[f11697,f11790]) ).
fof(f23364,plain,
v1_funct_1(np__0),
inference(forward_demodulation,[status(thm)],[f11697,f11793]) ).
fof(f23568,plain,
! [X0] :
( X0 = np__0
| ~ v1_xboole_0(X0) ),
inference(forward_demodulation,[status(thm)],[f11697,f4617]) ).
fof(f23569,plain,
sK730_skl = np__0,
inference(resolution,[status(thm)],[f23568,f11853]) ).
fof(f23570,plain,
sK727_skl = np__0,
inference(resolution,[status(thm)],[f23568,f11804]) ).
fof(f24278,plain,
( sQ638_spl
| sK279_skl != np__0 ),
inference(forward_demodulation,[status(thm)],[f11697,f22593]) ).
fof(f24502,definition,
( sQ738_spl
<=> v1_relat_1(sK1206_skl) ),
introduced(definition,[new_symbols(definition,[sQ738_spl])],[split_symbol_definition]) ).
fof(f24504,plain,
( sQ738_spl
| ~ v1_relat_1(sK1206_skl) ),
inference(component_clause,[status(thm)],[f24502]) ).
fof(f24608,plain,
! [X0,X1] :
( k1_relat_1(k5_relset_2(X1,X0)) = k1_zfmisc_1(X1)
| ~ v1_funct_1(k5_relset_2(X1,X0))
| ~ v1_relat_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f21911,f17475]) ).
fof(f24736,plain,
( ~ sQ419_spl
| k1_relat_1(k5_relset_2(sK1205_skl,sK1206_skl)) = k1_zfmisc_1(sK1205_skl)
| ~ v1_relat_1(sK1206_skl) ),
inference(resolution,[status(thm)],[f20393,f24608]) ).
fof(f24737,definition,
( sQ760_spl
<=> k1_relat_1(k5_relset_2(sK1205_skl,sK1206_skl)) = k1_zfmisc_1(sK1205_skl) ),
introduced(definition,[new_symbols(definition,[sQ760_spl])],[split_symbol_definition]) ).
fof(f24738,plain,
( ~ sQ760_spl
| k1_relat_1(k5_relset_2(sK1205_skl,sK1206_skl)) = k1_zfmisc_1(sK1205_skl) ),
inference(component_clause,[status(thm)],[f24737]) ).
fof(f24740,plain,
( ~ sQ419_spl
| sQ760_spl
| ~ sQ738_spl ),
inference(split_clause,[status(thm)],[f24736,f24502,f24737,f20392]) ).
fof(f24743,plain,
! [X0,X1] :
( sQ738_spl
| ~ m1_subset_1(sK1206_skl,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(resolution,[status(thm)],[f24504,f7438]) ).
fof(f24946,plain,
! [X0] :
( ~ sQ760_spl
| v1_funct_2(k5_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(sK1205_skl),X0)
| ~ r1_tarski(k2_relat_1(k5_relset_2(sK1205_skl,sK1206_skl)),X0)
| ~ v1_funct_1(k5_relset_2(sK1205_skl,sK1206_skl))
| ~ v1_relat_1(k5_relset_2(sK1205_skl,sK1206_skl)) ),
inference(paramodulation,[status(thm)],[f24738,f8687]) ).
fof(f24949,plain,
! [X0] :
( ~ sQ760_spl
| m2_relset_1(k5_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(sK1205_skl),X0)
| ~ r1_tarski(k2_relat_1(k5_relset_2(sK1205_skl,sK1206_skl)),X0)
| ~ v1_relat_1(k5_relset_2(sK1205_skl,sK1206_skl)) ),
inference(paramodulation,[status(thm)],[f24738,f7459]) ).
fof(f24951,definition,
( sQ764_spl
<=> v1_relat_1(k5_relset_2(sK1205_skl,sK1206_skl)) ),
introduced(definition,[new_symbols(definition,[sQ764_spl])],[split_symbol_definition]) ).
fof(f24953,plain,
( sQ764_spl
| ~ v1_relat_1(k5_relset_2(sK1205_skl,sK1206_skl)) ),
inference(component_clause,[status(thm)],[f24951]) ).
fof(f24954,definition,
! [X0] :
( sQ765_spl
<=> ( v1_funct_2(k5_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(sK1205_skl),X0)
| ~ r1_tarski(k2_relat_1(k5_relset_2(sK1205_skl,sK1206_skl)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ765_spl])],[split_symbol_definition]) ).
fof(f24955,plain,
! [X0] :
( ~ sQ765_spl
| v1_funct_2(k5_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(sK1205_skl),X0)
| ~ r1_tarski(k2_relat_1(k5_relset_2(sK1205_skl,sK1206_skl)),X0) ),
inference(component_clause,[status(thm)],[f24954]) ).
fof(f24957,plain,
( ~ sQ760_spl
| sQ765_spl
| ~ sQ419_spl
| ~ sQ764_spl ),
inference(split_clause,[status(thm)],[f24946,f24951,f20392,f24954,f24737]) ).
fof(f24966,definition,
! [X0] :
( sQ768_spl
<=> ( m2_relset_1(k5_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(sK1205_skl),X0)
| ~ r1_tarski(k2_relat_1(k5_relset_2(sK1205_skl,sK1206_skl)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ768_spl])],[split_symbol_definition]) ).
fof(f24967,plain,
! [X0] :
( ~ sQ768_spl
| m2_relset_1(k5_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(sK1205_skl),X0)
| ~ r1_tarski(k2_relat_1(k5_relset_2(sK1205_skl,sK1206_skl)),X0) ),
inference(component_clause,[status(thm)],[f24966]) ).
fof(f24969,plain,
( ~ sQ760_spl
| sQ768_spl
| ~ sQ764_spl ),
inference(split_clause,[status(thm)],[f24949,f24951,f24966,f24737]) ).
fof(f25009,plain,
( sQ764_spl
| ~ v1_relat_1(sK1206_skl) ),
inference(resolution,[status(thm)],[f24953,f17475]) ).
fof(f25063,plain,
( sQ738_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17562,f24743]) ).
fof(f25064,plain,
sQ738_spl,
inference(contradiction_clause,[status(thm)],[f25063]) ).
fof(f25065,plain,
( sQ764_spl
| ~ sQ738_spl ),
inference(split_clause,[status(thm)],[f25009,f24502,f24951]) ).
fof(f25080,definition,
! [X0,X1] :
( sQ773_spl
<=> ~ m2_relset_1(np__0,X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ773_spl])],[split_symbol_definition]) ).
fof(f25081,plain,
! [X0,X1] :
( ~ sQ773_spl
| ~ m2_relset_1(np__0,X0,X1) ),
inference(component_clause,[status(thm)],[f25080]) ).
fof(f25085,plain,
( ~ sQ773_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25081,f23276]) ).
fof(f25086,plain,
~ sQ773_spl,
inference(contradiction_clause,[status(thm)],[f25085]) ).
fof(f25361,definition,
( sQ811_spl
<=> sK730_skl = np__0 ),
introduced(definition,[new_symbols(definition,[sQ811_spl])],[split_symbol_definition]) ).
fof(f25363,plain,
( sQ811_spl
| sK730_skl != np__0 ),
inference(component_clause,[status(thm)],[f25361]) ).
fof(f25369,definition,
( sQ813_spl
<=> sK727_skl = np__0 ),
introduced(definition,[new_symbols(definition,[sQ813_spl])],[split_symbol_definition]) ).
fof(f25371,plain,
( sQ813_spl
| sK727_skl != np__0 ),
inference(component_clause,[status(thm)],[f25369]) ).
fof(f25379,plain,
np__0 = k1_xboole_0,
inference(resolution,[status(thm)],[f4724,f23272]) ).
fof(f25633,plain,
! [X0] :
( X0 = np__0
| ~ v1_xboole_0(X0) ),
inference(backward_demodulation,[status(thm)],[f25379,f4712]) ).
fof(f25635,plain,
! [X0] : k4_xboole_0(k1_xboole_0,X0) = np__0,
inference(backward_demodulation,[status(thm)],[f25379,f4709]) ).
fof(f25640,plain,
! [X0] : k4_xboole_0(np__0,X0) = np__0,
inference(forward_demodulation,[status(thm)],[f25379,f25635]) ).
fof(f25744,definition,
! [X0] :
( sQ821_spl
<=> ~ m2_relset_1(np__0,X0,np__0) ),
introduced(definition,[new_symbols(definition,[sQ821_spl])],[split_symbol_definition]) ).
fof(f25745,plain,
! [X0] :
( ~ sQ821_spl
| ~ m2_relset_1(np__0,X0,np__0) ),
inference(component_clause,[status(thm)],[f25744]) ).
fof(f25769,plain,
( ~ sQ821_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25745,f23276]) ).
fof(f25770,plain,
~ sQ821_spl,
inference(contradiction_clause,[status(thm)],[f25769]) ).
fof(f25774,plain,
! [X0] : k2_xboole_0(np__0,X0) = X0,
inference(resolution,[status(thm)],[f4741,f23272]) ).
fof(f26140,definition,
( sQ838_spl
<=> r1_tarski(np__0,sK1206_skl) ),
introduced(definition,[new_symbols(definition,[sQ838_spl])],[split_symbol_definition]) ).
fof(f26142,plain,
( sQ838_spl
| ~ r1_tarski(np__0,sK1206_skl) ),
inference(component_clause,[status(thm)],[f26140]) ).
fof(f26144,plain,
( sQ838_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26142,f23272]) ).
fof(f26145,plain,
sQ838_spl,
inference(contradiction_clause,[status(thm)],[f26144]) ).
fof(f26215,plain,
r1_tarski(k2_relat_1(k5_relset_2(sK1205_skl,sK1206_skl)),k1_zfmisc_1(k2_relat_1(sK1206_skl))),
inference(resolution,[status(thm)],[f17562,f17558]) ).
fof(f26573,plain,
sK235_skl = np__0,
inference(resolution,[status(thm)],[f25633,f7187]) ).
fof(f26574,plain,
sK162_skl = np__0,
inference(resolution,[status(thm)],[f25633,f6485]) ).
fof(f26575,plain,
sK118_skl = np__0,
inference(resolution,[status(thm)],[f25633,f5835]) ).
fof(f26580,plain,
( sQ616_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26573,f23235]) ).
fof(f26581,plain,
sQ616_spl,
inference(contradiction_clause,[status(thm)],[f26580]) ).
fof(f26582,plain,
( sQ591_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26574,f23253]) ).
fof(f26583,plain,
sQ591_spl,
inference(contradiction_clause,[status(thm)],[f26582]) ).
fof(f26584,plain,
( sQ601_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26575,f23258]) ).
fof(f26585,plain,
sQ601_spl,
inference(contradiction_clause,[status(thm)],[f26584]) ).
fof(f26609,plain,
sK279_skl = np__0,
inference(resolution,[status(thm)],[f7673,f25633]) ).
fof(f26613,plain,
( sQ638_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26609,f24278]) ).
fof(f26614,plain,
sQ638_spl,
inference(contradiction_clause,[status(thm)],[f26613]) ).
fof(f26857,definition,
! [X0] :
( sQ850_spl
<=> ~ r1_tarski(k1_relat_1(sK1206_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ850_spl])],[split_symbol_definition]) ).
fof(f26858,plain,
! [X0] :
( ~ sQ850_spl
| ~ r1_tarski(k1_relat_1(sK1206_skl),X0) ),
inference(component_clause,[status(thm)],[f26857]) ).
fof(f26892,definition,
! [X0] :
( sQ852_spl
<=> ~ r1_tarski(sK1207_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ852_spl])],[split_symbol_definition]) ).
fof(f26893,plain,
! [X0] :
( ~ sQ852_spl
| ~ r1_tarski(sK1207_skl,X0) ),
inference(component_clause,[status(thm)],[f26892]) ).
fof(f26966,plain,
( sQ811_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23569,f25363]) ).
fof(f26967,plain,
sQ811_spl,
inference(contradiction_clause,[status(thm)],[f26966]) ).
fof(f26968,plain,
( sQ813_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23570,f25371]) ).
fof(f26969,plain,
sQ813_spl,
inference(contradiction_clause,[status(thm)],[f26968]) ).
fof(f27025,plain,
( ~ sQ852_spl
| $false ),
inference(resolution,[status(thm)],[f26893,f4728]) ).
fof(f27033,plain,
~ sQ852_spl,
inference(contradiction_clause,[status(thm)],[f27025]) ).
fof(f27044,plain,
( ~ sQ850_spl
| $false ),
inference(resolution,[status(thm)],[f26858,f4728]) ).
fof(f27052,plain,
~ sQ850_spl,
inference(contradiction_clause,[status(thm)],[f27044]) ).
fof(f27215,definition,
! [X0] :
( sQ875_spl
<=> ~ r1_tarski(np__0,X0) ),
introduced(definition,[new_symbols(definition,[sQ875_spl])],[split_symbol_definition]) ).
fof(f27216,plain,
! [X0] :
( ~ sQ875_spl
| ~ r1_tarski(np__0,X0) ),
inference(component_clause,[status(thm)],[f27215]) ).
fof(f27219,plain,
( ~ sQ875_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27216,f23272]) ).
fof(f27220,plain,
~ sQ875_spl,
inference(contradiction_clause,[status(thm)],[f27219]) ).
fof(f27286,definition,
( sQ878_spl
<=> v1_funct_1(sK438_skl) ),
introduced(definition,[new_symbols(definition,[sQ878_spl])],[split_symbol_definition]) ).
fof(f27288,plain,
( sQ878_spl
| ~ v1_funct_1(sK438_skl) ),
inference(component_clause,[status(thm)],[f27286]) ).
fof(f27334,plain,
( sQ878_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27288,f9135]) ).
fof(f27335,plain,
sQ878_spl,
inference(contradiction_clause,[status(thm)],[f27334]) ).
fof(f27597,definition,
( sQ899_spl
<=> v1_funct_1(sK447_skl) ),
introduced(definition,[new_symbols(definition,[sQ899_spl])],[split_symbol_definition]) ).
fof(f27599,plain,
( sQ899_spl
| ~ v1_funct_1(sK447_skl) ),
inference(component_clause,[status(thm)],[f27597]) ).
fof(f27645,plain,
( sQ899_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27599,f9165]) ).
fof(f27646,plain,
sQ899_spl,
inference(contradiction_clause,[status(thm)],[f27645]) ).
fof(f27661,definition,
( sQ911_spl
<=> v1_funct_1(sK450_skl) ),
introduced(definition,[new_symbols(definition,[sQ911_spl])],[split_symbol_definition]) ).
fof(f27663,plain,
( sQ911_spl
| ~ v1_funct_1(sK450_skl) ),
inference(component_clause,[status(thm)],[f27661]) ).
fof(f27709,plain,
( sQ911_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27663,f9180]) ).
fof(f27710,plain,
sQ911_spl,
inference(contradiction_clause,[status(thm)],[f27709]) ).
fof(f27726,plain,
! [X0] : k4_xboole_0(X0,X0) = k4_xboole_0(np__0,X0),
inference(paramodulation,[status(thm)],[f25774,f4800]) ).
fof(f27749,plain,
! [X0] : k4_xboole_0(X0,X0) = np__0,
inference(forward_demodulation,[status(thm)],[f25640,f27726]) ).
fof(f27883,definition,
! [X0] :
( sQ923_spl
<=> X0 != np__0 ),
introduced(definition,[new_symbols(definition,[sQ923_spl])],[split_symbol_definition]) ).
fof(f27884,plain,
! [X0] :
( ~ sQ923_spl
| X0 != np__0 ),
inference(component_clause,[status(thm)],[f27883]) ).
fof(f27887,plain,
( ~ sQ923_spl
| $false ),
inference(destructive_equality_resolution,[status(thm)],[f27884]) ).
fof(f27888,plain,
~ sQ923_spl,
inference(contradiction_clause,[status(thm)],[f27887]) ).
fof(f29742,definition,
! [X0] :
( sQ1000_spl
<=> ~ r1_tarski(sK1206_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ1000_spl])],[split_symbol_definition]) ).
fof(f29743,plain,
! [X0] :
( ~ sQ1000_spl
| ~ r1_tarski(sK1206_skl,X0) ),
inference(component_clause,[status(thm)],[f29742]) ).
fof(f29747,plain,
( ~ sQ1000_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f22127,f29743]) ).
fof(f29757,plain,
~ sQ1000_spl,
inference(contradiction_clause,[status(thm)],[f29747]) ).
fof(f30050,definition,
! [X0] :
( sQ1011_spl
<=> ~ m1_subset_1(np__0,k1_zfmisc_1(k2_zfmisc_1(sK1205_skl,X0))) ),
introduced(definition,[new_symbols(definition,[sQ1011_spl])],[split_symbol_definition]) ).
fof(f30051,plain,
! [X0] :
( ~ sQ1011_spl
| ~ m1_subset_1(np__0,k1_zfmisc_1(k2_zfmisc_1(sK1205_skl,X0))) ),
inference(component_clause,[status(thm)],[f30050]) ).
fof(f30061,plain,
( ~ sQ1011_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30051,f23273]) ).
fof(f30062,plain,
~ sQ1011_spl,
inference(contradiction_clause,[status(thm)],[f30061]) ).
fof(f31534,plain,
! [X0,X1] :
( k4_xboole_0(X1,X0) != np__0
| ~ r2_xboole_0(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f25379,f4929]) ).
fof(f31780,definition,
! [X0] :
( sQ1017_spl
<=> ~ r1_tarski(k2_relat_1(sK1207_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ1017_spl])],[split_symbol_definition]) ).
fof(f31781,plain,
! [X0] :
( ~ sQ1017_spl
| ~ r1_tarski(k2_relat_1(sK1207_skl),X0) ),
inference(component_clause,[status(thm)],[f31780]) ).
fof(f31784,definition,
! [X0] :
( sQ1018_spl
<=> ~ r1_tarski(k1_relat_1(sK1207_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ1018_spl])],[split_symbol_definition]) ).
fof(f31785,plain,
! [X0] :
( ~ sQ1018_spl
| ~ r1_tarski(k1_relat_1(sK1207_skl),X0) ),
inference(component_clause,[status(thm)],[f31784]) ).
fof(f31800,plain,
( ~ sQ1017_spl
| $false ),
inference(resolution,[status(thm)],[f31781,f4728]) ).
fof(f31816,plain,
~ sQ1017_spl,
inference(contradiction_clause,[status(thm)],[f31800]) ).
fof(f32314,plain,
( ~ sQ1018_spl
| $false ),
inference(resolution,[status(thm)],[f31785,f4728]) ).
fof(f32322,plain,
~ sQ1018_spl,
inference(contradiction_clause,[status(thm)],[f32314]) ).
fof(f32401,definition,
( sQ1031_spl
<=> v1_relat_1(k2_zfmisc_1(k1_relat_1(sK1207_skl),k2_relat_1(sK1207_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1031_spl])],[split_symbol_definition]) ).
fof(f32403,plain,
( sQ1031_spl
| ~ v1_relat_1(k2_zfmisc_1(k1_relat_1(sK1207_skl),k2_relat_1(sK1207_skl))) ),
inference(component_clause,[status(thm)],[f32401]) ).
fof(f32405,plain,
( sQ1031_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f32403,f5891]) ).
fof(f32406,plain,
sQ1031_spl,
inference(contradiction_clause,[status(thm)],[f32405]) ).
fof(f32492,plain,
! [X0] : ~ r2_hidden(X0,np__0),
inference(forward_demodulation,[status(thm)],[f25379,f21047]) ).
fof(f32676,plain,
k1_zfmisc_1(np__0) = k1_tarski(k1_xboole_0),
inference(forward_demodulation,[status(thm)],[f25379,f4970]) ).
fof(f32677,plain,
k1_zfmisc_1(np__0) = k1_tarski(np__0),
inference(forward_demodulation,[status(thm)],[f25379,f32676]) ).
fof(f32683,plain,
k3_tarski(np__0) = k1_xboole_0,
inference(forward_demodulation,[status(thm)],[f25379,f4971]) ).
fof(f32684,plain,
k3_tarski(np__0) = np__0,
inference(forward_demodulation,[status(thm)],[f25379,f32683]) ).
fof(f32798,plain,
k1_setfam_1(np__0) = k1_xboole_0,
inference(forward_demodulation,[status(thm)],[f25379,f21092]) ).
fof(f32799,plain,
k1_setfam_1(np__0) = np__0,
inference(forward_demodulation,[status(thm)],[f25379,f32798]) ).
fof(f32942,plain,
k6_relat_1(np__0) = k1_xboole_0,
inference(forward_demodulation,[status(thm)],[f25379,f6105]) ).
fof(f32943,plain,
k6_relat_1(np__0) = np__0,
inference(forward_demodulation,[status(thm)],[f25379,f32942]) ).
fof(f33103,plain,
! [X0] : k4_xboole_0(k1_tarski(X0),k1_tarski(X0)) != k1_tarski(X0),
inference(resolution,[status(thm)],[f21067,f4892]) ).
fof(f33116,plain,
! [X0] : np__0 != k1_tarski(X0),
inference(forward_demodulation,[status(thm)],[f27749,f33103]) ).
fof(f33165,plain,
np__0 != k1_zfmisc_1(np__0),
inference(paramodulation,[status(thm)],[f32677,f33116]) ).
fof(f33310,definition,
( sQ1035_spl
<=> v1_relat_1(sK302_skl) ),
introduced(definition,[new_symbols(definition,[sQ1035_spl])],[split_symbol_definition]) ).
fof(f33312,plain,
( sQ1035_spl
| ~ v1_relat_1(sK302_skl) ),
inference(component_clause,[status(thm)],[f33310]) ).
fof(f33313,definition,
( sQ1036_spl
<=> v1_funct_1(sK302_skl) ),
introduced(definition,[new_symbols(definition,[sQ1036_spl])],[split_symbol_definition]) ).
fof(f33315,plain,
( sQ1036_spl
| ~ v1_funct_1(sK302_skl) ),
inference(component_clause,[status(thm)],[f33313]) ).
fof(f33336,plain,
( sQ1035_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f33312,f8085]) ).
fof(f33337,plain,
sQ1035_spl,
inference(contradiction_clause,[status(thm)],[f33336]) ).
fof(f33338,plain,
( sQ1036_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f33315,f8086]) ).
fof(f33339,plain,
sQ1036_spl,
inference(contradiction_clause,[status(thm)],[f33338]) ).
fof(f33340,plain,
k6_partfun1(np__0) = np__0,
inference(backward_demodulation,[status(thm)],[f8164,f32943]) ).
fof(f33349,plain,
! [X0] : v1_relat_1(k6_partfun1(X0)),
inference(backward_demodulation,[status(thm)],[f8164,f6465]) ).
fof(f33632,plain,
! [X0] : r2_hidden(k3_ordinal2(X0),k1_zfmisc_1(X0)),
inference(resolution,[status(thm)],[f10172,f21064]) ).
fof(f33800,plain,
k4_ordinal2 = k1_ordinal1(np__0),
inference(forward_demodulation,[status(thm)],[f25379,f10185]) ).
fof(f33803,plain,
np__0 != k4_ordinal2,
inference(paramodulation,[status(thm)],[f33800,f7248]) ).
fof(f33819,definition,
( sQ1043_spl
<=> v1_relat_1(sK631_skl) ),
introduced(definition,[new_symbols(definition,[sQ1043_spl])],[split_symbol_definition]) ).
fof(f33821,plain,
( sQ1043_spl
| ~ v1_relat_1(sK631_skl) ),
inference(component_clause,[status(thm)],[f33819]) ).
fof(f33822,definition,
( sQ1044_spl
<=> v1_funct_1(sK631_skl) ),
introduced(definition,[new_symbols(definition,[sQ1044_spl])],[split_symbol_definition]) ).
fof(f33824,plain,
( sQ1044_spl
| ~ v1_funct_1(sK631_skl) ),
inference(component_clause,[status(thm)],[f33822]) ).
fof(f33845,plain,
( sQ1043_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f33821,f10513]) ).
fof(f33846,plain,
sQ1043_spl,
inference(contradiction_clause,[status(thm)],[f33845]) ).
fof(f33847,plain,
( sQ1044_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f33824,f10514]) ).
fof(f33848,plain,
sQ1044_spl,
inference(contradiction_clause,[status(thm)],[f33847]) ).
fof(f33856,definition,
( sQ1050_spl
<=> v1_relat_1(sK650_skl) ),
introduced(definition,[new_symbols(definition,[sQ1050_spl])],[split_symbol_definition]) ).
fof(f33858,plain,
( sQ1050_spl
| ~ v1_relat_1(sK650_skl) ),
inference(component_clause,[status(thm)],[f33856]) ).
fof(f33859,definition,
( sQ1051_spl
<=> v1_funct_1(sK650_skl) ),
introduced(definition,[new_symbols(definition,[sQ1051_spl])],[split_symbol_definition]) ).
fof(f33861,plain,
( sQ1051_spl
| ~ v1_funct_1(sK650_skl) ),
inference(component_clause,[status(thm)],[f33859]) ).
fof(f33882,plain,
( sQ1050_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f33858,f10631]) ).
fof(f33883,plain,
sQ1050_spl,
inference(contradiction_clause,[status(thm)],[f33882]) ).
fof(f33884,plain,
( sQ1051_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f33861,f10632]) ).
fof(f33885,plain,
sQ1051_spl,
inference(contradiction_clause,[status(thm)],[f33884]) ).
fof(f33937,plain,
! [X0] :
( ~ sQ624_spl
| r2_hidden(sK7_skl(np__0),X0) ),
inference(forward_demodulation,[status(thm)],[f25379,f22485]) ).
fof(f33938,plain,
( ~ sQ624_spl
| $false ),
inference(resolution,[status(thm)],[f33937,f32492]) ).
fof(f33951,plain,
~ sQ624_spl,
inference(contradiction_clause,[status(thm)],[f33938]) ).
fof(f33997,plain,
~ r2_xboole_0(k2_numbers,k1_numbers),
inference(resolution,[status(thm)],[f10923,f4694]) ).
fof(f34006,plain,
~ r2_xboole_0(k1_numbers,k3_numbers),
inference(resolution,[status(thm)],[f10924,f4694]) ).
fof(f34015,plain,
~ r2_xboole_0(k2_numbers,k3_numbers),
inference(resolution,[status(thm)],[f10925,f4694]) ).
fof(f34024,plain,
~ r2_xboole_0(k3_numbers,k4_numbers),
inference(resolution,[status(thm)],[f10926,f4694]) ).
fof(f34033,plain,
~ r2_xboole_0(k1_numbers,k4_numbers),
inference(resolution,[status(thm)],[f10927,f4694]) ).
fof(f34042,plain,
~ r2_xboole_0(k2_numbers,k4_numbers),
inference(resolution,[status(thm)],[f10928,f4694]) ).
fof(f34044,plain,
k4_xboole_0(k4_numbers,k5_numbers) != np__0,
inference(resolution,[status(thm)],[f10929,f31534]) ).
fof(f34051,plain,
~ r2_xboole_0(k4_numbers,k5_numbers),
inference(resolution,[status(thm)],[f10929,f4694]) ).
fof(f34132,definition,
! [X0] :
( sQ1060_spl
<=> ~ r1_tarski(k1_relat_1(sK438_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ1060_spl])],[split_symbol_definition]) ).
fof(f34133,plain,
! [X0] :
( ~ sQ1060_spl
| ~ r1_tarski(k1_relat_1(sK438_skl),X0) ),
inference(component_clause,[status(thm)],[f34132]) ).
fof(f34144,definition,
! [X0] :
( sQ1061_spl
<=> ~ r1_tarski(k2_relat_1(sK438_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ1061_spl])],[split_symbol_definition]) ).
fof(f34145,plain,
! [X0] :
( ~ sQ1061_spl
| ~ r1_tarski(k2_relat_1(sK438_skl),X0) ),
inference(component_clause,[status(thm)],[f34144]) ).
fof(f34171,definition,
! [X0] :
( sQ1065_spl
<=> ~ r1_tarski(k1_relat_1(sK447_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ1065_spl])],[split_symbol_definition]) ).
fof(f34172,plain,
! [X0] :
( ~ sQ1065_spl
| ~ r1_tarski(k1_relat_1(sK447_skl),X0) ),
inference(component_clause,[status(thm)],[f34171]) ).
fof(f34183,definition,
! [X0] :
( sQ1066_spl
<=> ~ r1_tarski(k2_relat_1(sK447_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ1066_spl])],[split_symbol_definition]) ).
fof(f34184,plain,
! [X0] :
( ~ sQ1066_spl
| ~ r1_tarski(k2_relat_1(sK447_skl),X0) ),
inference(component_clause,[status(thm)],[f34183]) ).
fof(f34210,definition,
! [X0] :
( sQ1070_spl
<=> ~ r1_tarski(k1_relat_1(sK450_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ1070_spl])],[split_symbol_definition]) ).
fof(f34211,plain,
! [X0] :
( ~ sQ1070_spl
| ~ r1_tarski(k1_relat_1(sK450_skl),X0) ),
inference(component_clause,[status(thm)],[f34210]) ).
fof(f34240,plain,
k4_xboole_0(k3_numbers,k5_numbers) != np__0,
inference(resolution,[status(thm)],[f10930,f31534]) ).
fof(f34247,plain,
~ r2_xboole_0(k3_numbers,k5_numbers),
inference(resolution,[status(thm)],[f10930,f4694]) ).
fof(f34249,plain,
k4_xboole_0(k1_numbers,k5_numbers) != np__0,
inference(resolution,[status(thm)],[f10931,f31534]) ).
fof(f34256,plain,
~ r2_xboole_0(k1_numbers,k5_numbers),
inference(resolution,[status(thm)],[f10931,f4694]) ).
fof(f34258,plain,
k4_xboole_0(k2_numbers,k5_numbers) != np__0,
inference(resolution,[status(thm)],[f10932,f31534]) ).
fof(f34265,plain,
~ r2_xboole_0(k2_numbers,k5_numbers),
inference(resolution,[status(thm)],[f10932,f4694]) ).
fof(f34283,definition,
( sQ1071_spl
<=> k2_numbers = k1_numbers ),
introduced(definition,[new_symbols(definition,[sQ1071_spl])],[split_symbol_definition]) ).
fof(f34284,plain,
( ~ sQ1071_spl
| k2_numbers = k1_numbers ),
inference(component_clause,[status(thm)],[f34283]) ).
fof(f34290,plain,
( ~ sQ1071_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f34284,f10943]) ).
fof(f34291,plain,
~ sQ1071_spl,
inference(contradiction_clause,[status(thm)],[f34290]) ).
fof(f34308,definition,
( sQ1073_spl
<=> k1_numbers = k3_numbers ),
introduced(definition,[new_symbols(definition,[sQ1073_spl])],[split_symbol_definition]) ).
fof(f34309,plain,
( ~ sQ1073_spl
| k1_numbers = k3_numbers ),
inference(component_clause,[status(thm)],[f34308]) ).
fof(f34315,plain,
( ~ sQ1073_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f34309,f10944]) ).
fof(f34316,plain,
~ sQ1073_spl,
inference(contradiction_clause,[status(thm)],[f34315]) ).
fof(f34333,definition,
( sQ1075_spl
<=> k2_numbers = k3_numbers ),
introduced(definition,[new_symbols(definition,[sQ1075_spl])],[split_symbol_definition]) ).
fof(f34334,plain,
( ~ sQ1075_spl
| k2_numbers = k3_numbers ),
inference(component_clause,[status(thm)],[f34333]) ).
fof(f34340,plain,
( ~ sQ1075_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f34334,f10945]) ).
fof(f34341,plain,
~ sQ1075_spl,
inference(contradiction_clause,[status(thm)],[f34340]) ).
fof(f34358,definition,
( sQ1077_spl
<=> k3_numbers = k4_numbers ),
introduced(definition,[new_symbols(definition,[sQ1077_spl])],[split_symbol_definition]) ).
fof(f34359,plain,
( ~ sQ1077_spl
| k3_numbers = k4_numbers ),
inference(component_clause,[status(thm)],[f34358]) ).
fof(f34365,plain,
( ~ sQ1077_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f34359,f10946]) ).
fof(f34366,plain,
~ sQ1077_spl,
inference(contradiction_clause,[status(thm)],[f34365]) ).
fof(f34383,definition,
( sQ1079_spl
<=> k1_numbers = k4_numbers ),
introduced(definition,[new_symbols(definition,[sQ1079_spl])],[split_symbol_definition]) ).
fof(f34384,plain,
( ~ sQ1079_spl
| k1_numbers = k4_numbers ),
inference(component_clause,[status(thm)],[f34383]) ).
fof(f34390,plain,
( ~ sQ1079_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f34384,f10947]) ).
fof(f34391,plain,
~ sQ1079_spl,
inference(contradiction_clause,[status(thm)],[f34390]) ).
fof(f34408,definition,
( sQ1081_spl
<=> k2_numbers = k4_numbers ),
introduced(definition,[new_symbols(definition,[sQ1081_spl])],[split_symbol_definition]) ).
fof(f34409,plain,
( ~ sQ1081_spl
| k2_numbers = k4_numbers ),
inference(component_clause,[status(thm)],[f34408]) ).
fof(f34415,plain,
( ~ sQ1081_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f34409,f10948]) ).
fof(f34416,plain,
~ sQ1081_spl,
inference(contradiction_clause,[status(thm)],[f34415]) ).
fof(f34433,definition,
( sQ1083_spl
<=> k4_numbers = k5_numbers ),
introduced(definition,[new_symbols(definition,[sQ1083_spl])],[split_symbol_definition]) ).
fof(f34434,plain,
( ~ sQ1083_spl
| k4_numbers = k5_numbers ),
inference(component_clause,[status(thm)],[f34433]) ).
fof(f34440,plain,
( ~ sQ1083_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f34434,f10949]) ).
fof(f34441,plain,
~ sQ1083_spl,
inference(contradiction_clause,[status(thm)],[f34440]) ).
fof(f34458,definition,
( sQ1085_spl
<=> k3_numbers = k5_numbers ),
introduced(definition,[new_symbols(definition,[sQ1085_spl])],[split_symbol_definition]) ).
fof(f34459,plain,
( ~ sQ1085_spl
| k3_numbers = k5_numbers ),
inference(component_clause,[status(thm)],[f34458]) ).
fof(f34465,plain,
( ~ sQ1085_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f34459,f10950]) ).
fof(f34466,plain,
~ sQ1085_spl,
inference(contradiction_clause,[status(thm)],[f34465]) ).
fof(f34483,definition,
( sQ1087_spl
<=> k1_numbers = k5_numbers ),
introduced(definition,[new_symbols(definition,[sQ1087_spl])],[split_symbol_definition]) ).
fof(f34484,plain,
( ~ sQ1087_spl
| k1_numbers = k5_numbers ),
inference(component_clause,[status(thm)],[f34483]) ).
fof(f34490,plain,
( ~ sQ1087_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f34484,f10951]) ).
fof(f34491,plain,
~ sQ1087_spl,
inference(contradiction_clause,[status(thm)],[f34490]) ).
fof(f34547,definition,
! [X0] :
( sQ1089_spl
<=> ~ r1_tarski(k2_relat_1(sK450_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ1089_spl])],[split_symbol_definition]) ).
fof(f34548,plain,
! [X0] :
( ~ sQ1089_spl
| ~ r1_tarski(k2_relat_1(sK450_skl),X0) ),
inference(component_clause,[status(thm)],[f34547]) ).
fof(f34672,plain,
r2_hidden(k5_numbers,k1_zfmisc_1(k2_numbers)),
inference(resolution,[status(thm)],[f10942,f21064]) ).
fof(f34673,definition,
( sQ1090_spl
<=> k2_numbers = k5_numbers ),
introduced(definition,[new_symbols(definition,[sQ1090_spl])],[split_symbol_definition]) ).
fof(f34674,plain,
( ~ sQ1090_spl
| k2_numbers = k5_numbers ),
inference(component_clause,[status(thm)],[f34673]) ).
fof(f34680,plain,
( ~ sQ1090_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f34674,f10952]) ).
fof(f34681,plain,
~ sQ1090_spl,
inference(contradiction_clause,[status(thm)],[f34680]) ).
fof(f35218,definition,
( sQ1099_spl
<=> r2_hidden(np__0,np__0) ),
introduced(definition,[new_symbols(definition,[sQ1099_spl])],[split_symbol_definition]) ).
fof(f35219,plain,
( ~ sQ1099_spl
| r2_hidden(np__0,np__0) ),
inference(component_clause,[status(thm)],[f35218]) ).
fof(f35222,plain,
( ~ sQ1099_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35219,f32492]) ).
fof(f35223,plain,
~ sQ1099_spl,
inference(contradiction_clause,[status(thm)],[f35222]) ).
fof(f35291,definition,
! [X0] :
( sQ1100_spl
<=> np__0 = k1_tarski(X0) ),
introduced(definition,[new_symbols(definition,[sQ1100_spl])],[split_symbol_definition]) ).
fof(f35292,plain,
! [X0] :
( ~ sQ1100_spl
| np__0 = k1_tarski(X0) ),
inference(component_clause,[status(thm)],[f35291]) ).
fof(f35296,plain,
( ~ sQ1100_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35292,f33116]) ).
fof(f35297,plain,
~ sQ1100_spl,
inference(contradiction_clause,[status(thm)],[f35296]) ).
fof(f35419,definition,
( sQ1101_spl
<=> v1_relat_1(sK828_skl) ),
introduced(definition,[new_symbols(definition,[sQ1101_spl])],[split_symbol_definition]) ).
fof(f35421,plain,
( sQ1101_spl
| ~ v1_relat_1(sK828_skl) ),
inference(component_clause,[status(thm)],[f35419]) ).
fof(f35422,definition,
( sQ1102_spl
<=> v1_funct_1(sK828_skl) ),
introduced(definition,[new_symbols(definition,[sQ1102_spl])],[split_symbol_definition]) ).
fof(f35424,plain,
( sQ1102_spl
| ~ v1_funct_1(sK828_skl) ),
inference(component_clause,[status(thm)],[f35422]) ).
fof(f35445,plain,
( sQ1101_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35421,f13280]) ).
fof(f35446,plain,
sQ1101_spl,
inference(contradiction_clause,[status(thm)],[f35445]) ).
fof(f35447,plain,
( sQ1102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35424,f13281]) ).
fof(f35448,plain,
sQ1102_spl,
inference(contradiction_clause,[status(thm)],[f35447]) ).
fof(f35511,definition,
( sQ1108_spl
<=> m2_relset_1(np__0,np__0,np__0) ),
introduced(definition,[new_symbols(definition,[sQ1108_spl])],[split_symbol_definition]) ).
fof(f35513,plain,
( sQ1108_spl
| ~ m2_relset_1(np__0,np__0,np__0) ),
inference(component_clause,[status(thm)],[f35511]) ).
fof(f35519,plain,
( sQ1108_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35513,f23276]) ).
fof(f35520,plain,
sQ1108_spl,
inference(contradiction_clause,[status(thm)],[f35519]) ).
fof(f35759,definition,
! [X0] :
( sQ1120_spl
<=> ( k1_tarski(X0) = np__0
| np__0 = k1_tarski(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1120_spl])],[split_symbol_definition]) ).
fof(f35760,plain,
! [X0] :
( ~ sQ1120_spl
| k1_tarski(X0) = np__0
| np__0 = k1_tarski(X0) ),
inference(component_clause,[status(thm)],[f35759]) ).
fof(f35766,definition,
! [X0,X1] :
( sQ1121_spl
<=> ( X1 = np__0
| np__0 = X1
| k1_tarski(X0) != X1 ) ),
introduced(definition,[new_symbols(definition,[sQ1121_spl])],[split_symbol_definition]) ).
fof(f35767,plain,
! [X0,X1] :
( ~ sQ1121_spl
| X1 = np__0
| np__0 = X1
| k1_tarski(X0) != X1 ),
inference(component_clause,[status(thm)],[f35766]) ).
fof(f35775,plain,
! [X0,X1] :
( ~ sQ1121_spl
| np__0 = X1
| k1_tarski(X0) != X1 ),
inference(duplicate_literals_removal,[status(thm)],[f35767]) ).
fof(f35776,plain,
! [X0] :
( ~ sQ1121_spl
| np__0 = k1_tarski(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f35775]) ).
fof(f35777,plain,
( ~ sQ1121_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35776,f33116]) ).
fof(f35778,plain,
~ sQ1121_spl,
inference(contradiction_clause,[status(thm)],[f35777]) ).
fof(f35779,plain,
! [X0] :
( ~ sQ1120_spl
| np__0 = k1_tarski(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f35760]) ).
fof(f35780,plain,
( ~ sQ1120_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35779,f33116]) ).
fof(f35781,plain,
~ sQ1120_spl,
inference(contradiction_clause,[status(thm)],[f35780]) ).
fof(f35817,plain,
( ~ sQ1060_spl
| $false ),
inference(resolution,[status(thm)],[f34133,f4728]) ).
fof(f35829,plain,
~ sQ1060_spl,
inference(contradiction_clause,[status(thm)],[f35817]) ).
fof(f35837,plain,
( ~ sQ1061_spl
| $false ),
inference(resolution,[status(thm)],[f34145,f4728]) ).
fof(f35857,plain,
~ sQ1061_spl,
inference(contradiction_clause,[status(thm)],[f35837]) ).
fof(f35862,plain,
( ~ sQ1065_spl
| $false ),
inference(resolution,[status(thm)],[f34172,f4728]) ).
fof(f35874,plain,
~ sQ1065_spl,
inference(contradiction_clause,[status(thm)],[f35862]) ).
fof(f35882,plain,
( ~ sQ1066_spl
| $false ),
inference(resolution,[status(thm)],[f34184,f4728]) ).
fof(f35902,plain,
~ sQ1066_spl,
inference(contradiction_clause,[status(thm)],[f35882]) ).
fof(f36172,plain,
! [X0,X1] : k2_xboole_0(k1_tarski(X0),X1) != np__0,
inference(forward_demodulation,[status(thm)],[f25379,f5080]) ).
fof(f36173,plain,
! [X0,X1] : k2_tarski(X0,X1) != np__0,
inference(paramodulation,[status(thm)],[f4986,f36172]) ).
fof(f36542,plain,
( ~ sQ1070_spl
| $false ),
inference(resolution,[status(thm)],[f34211,f4728]) ).
fof(f36554,plain,
~ sQ1070_spl,
inference(contradiction_clause,[status(thm)],[f36542]) ).
fof(f36562,plain,
( ~ sQ1089_spl
| $false ),
inference(resolution,[status(thm)],[f34548,f4728]) ).
fof(f36582,plain,
~ sQ1089_spl,
inference(contradiction_clause,[status(thm)],[f36562]) ).
fof(f37188,definition,
( sQ1162_spl
<=> r1_tarski(np__0,np__0) ),
introduced(definition,[new_symbols(definition,[sQ1162_spl])],[split_symbol_definition]) ).
fof(f37190,plain,
( sQ1162_spl
| ~ r1_tarski(np__0,np__0) ),
inference(component_clause,[status(thm)],[f37188]) ).
fof(f39229,definition,
! [X0] :
( sQ1208_spl
<=> ~ r2_hidden(X0,k1_zfmisc_1(np__0)) ),
introduced(definition,[new_symbols(definition,[sQ1208_spl])],[split_symbol_definition]) ).
fof(f39230,plain,
! [X0] :
( ~ sQ1208_spl
| ~ r2_hidden(X0,k1_zfmisc_1(np__0)) ),
inference(component_clause,[status(thm)],[f39229]) ).
fof(f39628,plain,
( ~ sQ1208_spl
| $false ),
inference(resolution,[status(thm)],[f39230,f33632]) ).
fof(f39657,plain,
~ sQ1208_spl,
inference(contradiction_clause,[status(thm)],[f39628]) ).
fof(f39872,definition,
( sQ1228_spl
<=> k2_numbers = np__0 ),
introduced(definition,[new_symbols(definition,[sQ1228_spl])],[split_symbol_definition]) ).
fof(f39873,plain,
( ~ sQ1228_spl
| k2_numbers = np__0 ),
inference(component_clause,[status(thm)],[f39872]) ).
fof(f39900,plain,
( ~ sQ1228_spl
| k4_xboole_0(np__0,k5_numbers) != np__0 ),
inference(backward_demodulation,[status(thm)],[f39873,f34258]) ).
fof(f39918,plain,
( ~ sQ1228_spl
| np__0 != np__0 ),
inference(forward_demodulation,[status(thm)],[f25640,f39900]) ).
fof(f39919,plain,
( ~ sQ1228_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f39918]) ).
fof(f39920,plain,
~ sQ1228_spl,
inference(contradiction_clause,[status(thm)],[f39919]) ).
fof(f40008,plain,
! [X0,X1] : k4_xboole_0(k1_tarski(X0),k2_tarski(X1,X0)) = np__0,
inference(forward_demodulation,[status(thm)],[f25379,f21081]) ).
fof(f40164,definition,
( sQ1232_spl
<=> k1_numbers = np__0 ),
introduced(definition,[new_symbols(definition,[sQ1232_spl])],[split_symbol_definition]) ).
fof(f40165,plain,
( ~ sQ1232_spl
| k1_numbers = np__0 ),
inference(component_clause,[status(thm)],[f40164]) ).
fof(f40190,plain,
( ~ sQ1232_spl
| k4_xboole_0(np__0,k5_numbers) != np__0 ),
inference(backward_demodulation,[status(thm)],[f40165,f34249]) ).
fof(f40205,plain,
( ~ sQ1232_spl
| np__0 != np__0 ),
inference(forward_demodulation,[status(thm)],[f25640,f40190]) ).
fof(f40206,plain,
( ~ sQ1232_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f40205]) ).
fof(f40207,plain,
~ sQ1232_spl,
inference(contradiction_clause,[status(thm)],[f40206]) ).
fof(f40523,definition,
( sQ1236_spl
<=> k3_numbers = np__0 ),
introduced(definition,[new_symbols(definition,[sQ1236_spl])],[split_symbol_definition]) ).
fof(f40524,plain,
( ~ sQ1236_spl
| k3_numbers = np__0 ),
inference(component_clause,[status(thm)],[f40523]) ).
fof(f40553,plain,
( ~ sQ1236_spl
| k4_xboole_0(np__0,k5_numbers) != np__0 ),
inference(backward_demodulation,[status(thm)],[f40524,f34240]) ).
fof(f40563,plain,
( ~ sQ1236_spl
| np__0 != np__0 ),
inference(forward_demodulation,[status(thm)],[f25640,f40553]) ).
fof(f40564,plain,
( ~ sQ1236_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f40563]) ).
fof(f40565,plain,
~ sQ1236_spl,
inference(contradiction_clause,[status(thm)],[f40564]) ).
fof(f41170,plain,
! [X0,X1] :
( ~ sQ84_spl
| ~ v1_funct_1(k10_finseq_1(X0,X1)) ),
inference(resolution,[status(thm)],[f19130,f11827]) ).
fof(f41206,plain,
( ~ sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f41170,f11828]) ).
fof(f41207,plain,
~ sQ84_spl,
inference(contradiction_clause,[status(thm)],[f41206]) ).
fof(f41397,definition,
( sQ1244_spl
<=> k4_numbers = np__0 ),
introduced(definition,[new_symbols(definition,[sQ1244_spl])],[split_symbol_definition]) ).
fof(f41398,plain,
( ~ sQ1244_spl
| k4_numbers = np__0 ),
inference(component_clause,[status(thm)],[f41397]) ).
fof(f41431,plain,
( ~ sQ1244_spl
| k4_xboole_0(np__0,k5_numbers) != np__0 ),
inference(backward_demodulation,[status(thm)],[f41398,f34044]) ).
fof(f41437,plain,
( ~ sQ1244_spl
| np__0 != np__0 ),
inference(forward_demodulation,[status(thm)],[f25640,f41431]) ).
fof(f41438,plain,
( ~ sQ1244_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f41437]) ).
fof(f41439,plain,
~ sQ1244_spl,
inference(contradiction_clause,[status(thm)],[f41438]) ).
fof(f42065,definition,
( sQ1245_spl
<=> r2_xboole_0(k2_numbers,k1_numbers) ),
introduced(definition,[new_symbols(definition,[sQ1245_spl])],[split_symbol_definition]) ).
fof(f42066,plain,
( ~ sQ1245_spl
| r2_xboole_0(k2_numbers,k1_numbers) ),
inference(component_clause,[status(thm)],[f42065]) ).
fof(f42088,definition,
( sQ1248_spl
<=> r2_xboole_0(k1_numbers,k3_numbers) ),
introduced(definition,[new_symbols(definition,[sQ1248_spl])],[split_symbol_definition]) ).
fof(f42089,plain,
( ~ sQ1248_spl
| r2_xboole_0(k1_numbers,k3_numbers) ),
inference(component_clause,[status(thm)],[f42088]) ).
fof(f42618,definition,
( sQ1251_spl
<=> r2_xboole_0(k2_numbers,k3_numbers) ),
introduced(definition,[new_symbols(definition,[sQ1251_spl])],[split_symbol_definition]) ).
fof(f42619,plain,
( ~ sQ1251_spl
| r2_xboole_0(k2_numbers,k3_numbers) ),
inference(component_clause,[status(thm)],[f42618]) ).
fof(f42641,definition,
( sQ1254_spl
<=> r2_xboole_0(k3_numbers,k4_numbers) ),
introduced(definition,[new_symbols(definition,[sQ1254_spl])],[split_symbol_definition]) ).
fof(f42642,plain,
( ~ sQ1254_spl
| r2_xboole_0(k3_numbers,k4_numbers) ),
inference(component_clause,[status(thm)],[f42641]) ).
fof(f42664,definition,
( sQ1257_spl
<=> r2_xboole_0(k1_numbers,k4_numbers) ),
introduced(definition,[new_symbols(definition,[sQ1257_spl])],[split_symbol_definition]) ).
fof(f42665,plain,
( ~ sQ1257_spl
| r2_xboole_0(k1_numbers,k4_numbers) ),
inference(component_clause,[status(thm)],[f42664]) ).
fof(f42851,definition,
( sQ1260_spl
<=> v1_relat_1(k2_zfmisc_1(k1_relat_1(sK438_skl),k2_relat_1(sK438_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1260_spl])],[split_symbol_definition]) ).
fof(f42853,plain,
( sQ1260_spl
| ~ v1_relat_1(k2_zfmisc_1(k1_relat_1(sK438_skl),k2_relat_1(sK438_skl))) ),
inference(component_clause,[status(thm)],[f42851]) ).
fof(f42855,plain,
( sQ1260_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f42853,f5891]) ).
fof(f42856,plain,
sQ1260_spl,
inference(contradiction_clause,[status(thm)],[f42855]) ).
fof(f42880,definition,
( sQ1261_spl
<=> v1_relat_1(k2_zfmisc_1(k1_relat_1(sK447_skl),k2_relat_1(sK447_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1261_spl])],[split_symbol_definition]) ).
fof(f42882,plain,
( sQ1261_spl
| ~ v1_relat_1(k2_zfmisc_1(k1_relat_1(sK447_skl),k2_relat_1(sK447_skl))) ),
inference(component_clause,[status(thm)],[f42880]) ).
fof(f42884,plain,
( sQ1261_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f42882,f5891]) ).
fof(f42885,plain,
sQ1261_spl,
inference(contradiction_clause,[status(thm)],[f42884]) ).
fof(f42951,definition,
( sQ1262_spl
<=> r2_xboole_0(k2_numbers,k4_numbers) ),
introduced(definition,[new_symbols(definition,[sQ1262_spl])],[split_symbol_definition]) ).
fof(f42952,plain,
( ~ sQ1262_spl
| r2_xboole_0(k2_numbers,k4_numbers) ),
inference(component_clause,[status(thm)],[f42951]) ).
fof(f42974,definition,
( sQ1265_spl
<=> r2_xboole_0(k4_numbers,k5_numbers) ),
introduced(definition,[new_symbols(definition,[sQ1265_spl])],[split_symbol_definition]) ).
fof(f42975,plain,
( ~ sQ1265_spl
| r2_xboole_0(k4_numbers,k5_numbers) ),
inference(component_clause,[status(thm)],[f42974]) ).
fof(f43136,definition,
( sQ1268_spl
<=> v1_relat_1(k2_zfmisc_1(k1_relat_1(sK450_skl),k2_relat_1(sK450_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1268_spl])],[split_symbol_definition]) ).
fof(f43138,plain,
( sQ1268_spl
| ~ v1_relat_1(k2_zfmisc_1(k1_relat_1(sK450_skl),k2_relat_1(sK450_skl))) ),
inference(component_clause,[status(thm)],[f43136]) ).
fof(f43140,plain,
( sQ1268_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f43138,f5891]) ).
fof(f43141,plain,
sQ1268_spl,
inference(contradiction_clause,[status(thm)],[f43140]) ).
fof(f43422,definition,
( sQ1269_spl
<=> r2_xboole_0(k3_numbers,k5_numbers) ),
introduced(definition,[new_symbols(definition,[sQ1269_spl])],[split_symbol_definition]) ).
fof(f43423,plain,
( ~ sQ1269_spl
| r2_xboole_0(k3_numbers,k5_numbers) ),
inference(component_clause,[status(thm)],[f43422]) ).
fof(f43445,definition,
( sQ1272_spl
<=> r2_xboole_0(k1_numbers,k5_numbers) ),
introduced(definition,[new_symbols(definition,[sQ1272_spl])],[split_symbol_definition]) ).
fof(f43446,plain,
( ~ sQ1272_spl
| r2_xboole_0(k1_numbers,k5_numbers) ),
inference(component_clause,[status(thm)],[f43445]) ).
fof(f43598,definition,
( sQ1275_spl
<=> k1_zfmisc_1(np__0) = np__0 ),
introduced(definition,[new_symbols(definition,[sQ1275_spl])],[split_symbol_definition]) ).
fof(f43599,plain,
( ~ sQ1275_spl
| k1_zfmisc_1(np__0) = np__0 ),
inference(component_clause,[status(thm)],[f43598]) ).
fof(f43609,definition,
( sQ1278_spl
<=> k1_zfmisc_1(np__0) = k3_tarski(np__0) ),
introduced(definition,[new_symbols(definition,[sQ1278_spl])],[split_symbol_definition]) ).
fof(f43610,plain,
( ~ sQ1278_spl
| k1_zfmisc_1(np__0) = k3_tarski(np__0) ),
inference(component_clause,[status(thm)],[f43609]) ).
fof(f43623,plain,
( ~ sQ1275_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f43599,f33165]) ).
fof(f43624,plain,
~ sQ1275_spl,
inference(contradiction_clause,[status(thm)],[f43623]) ).
fof(f43625,plain,
( ~ sQ1278_spl
| k1_zfmisc_1(np__0) = np__0 ),
inference(forward_demodulation,[status(thm)],[f32684,f43610]) ).
fof(f43626,plain,
( ~ sQ1278_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f43625,f33165]) ).
fof(f43627,plain,
~ sQ1278_spl,
inference(contradiction_clause,[status(thm)],[f43626]) ).
fof(f43722,plain,
( sQ1162_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f37190,f23272]) ).
fof(f43723,plain,
sQ1162_spl,
inference(contradiction_clause,[status(thm)],[f43722]) ).
fof(f43745,definition,
( sQ1287_spl
<=> r2_xboole_0(k2_numbers,k5_numbers) ),
introduced(definition,[new_symbols(definition,[sQ1287_spl])],[split_symbol_definition]) ).
fof(f43746,plain,
( ~ sQ1287_spl
| r2_xboole_0(k2_numbers,k5_numbers) ),
inference(component_clause,[status(thm)],[f43745]) ).
fof(f44026,definition,
! [X0,X1] :
( sQ1293_spl
<=> ~ r2_hidden(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ1293_spl])],[split_symbol_definition]) ).
fof(f44027,plain,
! [X0,X1] :
( ~ sQ1293_spl
| ~ r2_hidden(X0,X1) ),
inference(component_clause,[status(thm)],[f44026]) ).
fof(f44229,plain,
( ~ sQ1293_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f34672,f44027]) ).
fof(f44281,plain,
~ sQ1293_spl,
inference(contradiction_clause,[status(thm)],[f44229]) ).
fof(f44414,definition,
! [X0,X1] :
( sQ1316_spl
<=> ~ r1_tarski(np__0,k2_zfmisc_1(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ1316_spl])],[split_symbol_definition]) ).
fof(f44415,plain,
! [X0,X1] :
( ~ sQ1316_spl
| ~ r1_tarski(np__0,k2_zfmisc_1(X0,X1)) ),
inference(component_clause,[status(thm)],[f44414]) ).
fof(f44421,plain,
( ~ sQ1316_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f44415,f23272]) ).
fof(f44422,plain,
~ sQ1316_spl,
inference(contradiction_clause,[status(thm)],[f44421]) ).
fof(f44491,definition,
( sQ1320_spl
<=> v1_xboole_0(k1_numbers) ),
introduced(definition,[new_symbols(definition,[sQ1320_spl])],[split_symbol_definition]) ).
fof(f44492,plain,
( ~ sQ1320_spl
| v1_xboole_0(k1_numbers) ),
inference(component_clause,[status(thm)],[f44491]) ).
fof(f44499,plain,
( ~ sQ1320_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f44492,f10916]) ).
fof(f44500,plain,
~ sQ1320_spl,
inference(contradiction_clause,[status(thm)],[f44499]) ).
fof(f44708,plain,
( ~ sQ1245_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f42066,f33997]) ).
fof(f44709,plain,
~ sQ1245_spl,
inference(contradiction_clause,[status(thm)],[f44708]) ).
fof(f44710,plain,
( ~ sQ1248_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f42089,f34006]) ).
fof(f44711,plain,
~ sQ1248_spl,
inference(contradiction_clause,[status(thm)],[f44710]) ).
fof(f44712,plain,
( ~ sQ1251_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f42619,f34015]) ).
fof(f44713,plain,
~ sQ1251_spl,
inference(contradiction_clause,[status(thm)],[f44712]) ).
fof(f44714,plain,
( ~ sQ1254_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f42642,f34024]) ).
fof(f44715,plain,
~ sQ1254_spl,
inference(contradiction_clause,[status(thm)],[f44714]) ).
fof(f44872,definition,
( sQ1328_spl
<=> v1_xboole_0(k3_numbers) ),
introduced(definition,[new_symbols(definition,[sQ1328_spl])],[split_symbol_definition]) ).
fof(f44873,plain,
( ~ sQ1328_spl
| v1_xboole_0(k3_numbers) ),
inference(component_clause,[status(thm)],[f44872]) ).
fof(f44877,plain,
( ~ sQ1328_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f44873,f10918]) ).
fof(f44878,plain,
~ sQ1328_spl,
inference(contradiction_clause,[status(thm)],[f44877]) ).
fof(f44885,plain,
( ~ sQ1257_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f42665,f34033]) ).
fof(f44886,plain,
~ sQ1257_spl,
inference(contradiction_clause,[status(thm)],[f44885]) ).
fof(f44887,plain,
( ~ sQ1262_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f42952,f34042]) ).
fof(f44888,plain,
~ sQ1262_spl,
inference(contradiction_clause,[status(thm)],[f44887]) ).
fof(f44889,plain,
( ~ sQ1265_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f42975,f34051]) ).
fof(f44890,plain,
~ sQ1265_spl,
inference(contradiction_clause,[status(thm)],[f44889]) ).
fof(f44891,plain,
( ~ sQ1269_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f43423,f34247]) ).
fof(f44892,plain,
~ sQ1269_spl,
inference(contradiction_clause,[status(thm)],[f44891]) ).
fof(f44893,plain,
( ~ sQ1272_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f43446,f34256]) ).
fof(f44894,plain,
~ sQ1272_spl,
inference(contradiction_clause,[status(thm)],[f44893]) ).
fof(f44895,plain,
( ~ sQ1287_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f43746,f34265]) ).
fof(f44896,plain,
~ sQ1287_spl,
inference(contradiction_clause,[status(thm)],[f44895]) ).
fof(f46212,definition,
! [X1,X2] :
( sQ1339_spl
<=> ~ r2_hidden(X1,k1_tarski(X2)) ),
introduced(definition,[new_symbols(definition,[sQ1339_spl])],[split_symbol_definition]) ).
fof(f46213,plain,
! [X0,X1] :
( ~ sQ1339_spl
| ~ r2_hidden(X0,k1_tarski(X1)) ),
inference(component_clause,[status(thm)],[f46212]) ).
fof(f47006,plain,
( ~ sQ1339_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f21038,f46213]) ).
fof(f47013,plain,
~ sQ1339_spl,
inference(contradiction_clause,[status(thm)],[f47006]) ).
fof(f47709,definition,
( sQ1347_spl
<=> v1_funct_1(k6_partfun1(np__0)) ),
introduced(definition,[new_symbols(definition,[sQ1347_spl])],[split_symbol_definition]) ).
fof(f47711,plain,
( sQ1347_spl
| ~ v1_funct_1(k6_partfun1(np__0)) ),
inference(component_clause,[status(thm)],[f47709]) ).
fof(f47728,plain,
( sQ1347_spl
| ~ v1_funct_1(np__0) ),
inference(forward_demodulation,[status(thm)],[f33340,f47711]) ).
fof(f47729,plain,
( sQ1347_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f47728,f23364]) ).
fof(f47730,plain,
sQ1347_spl,
inference(contradiction_clause,[status(thm)],[f47729]) ).
fof(f48071,definition,
( sQ1351_spl
<=> v1_xboole_0(k1_zfmisc_1(k2_zfmisc_1(sK1205_skl,sK1207_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1351_spl])],[split_symbol_definition]) ).
fof(f48072,plain,
( ~ sQ1351_spl
| v1_xboole_0(k1_zfmisc_1(k2_zfmisc_1(sK1205_skl,sK1207_skl))) ),
inference(component_clause,[status(thm)],[f48071]) ).
fof(f48160,plain,
( ~ sQ1351_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f48072,f5325]) ).
fof(f48161,plain,
~ sQ1351_spl,
inference(contradiction_clause,[status(thm)],[f48160]) ).
fof(f48276,definition,
( sQ1388_spl
<=> k5_numbers = np__0 ),
introduced(definition,[new_symbols(definition,[sQ1388_spl])],[split_symbol_definition]) ).
fof(f48277,plain,
( ~ sQ1388_spl
| k5_numbers = np__0 ),
inference(component_clause,[status(thm)],[f48276]) ).
fof(f48782,plain,
( ~ sQ1388_spl
| v1_xboole_0(k5_numbers) ),
inference(backward_demodulation,[status(thm)],[f48277,f23292]) ).
fof(f48840,plain,
( ~ sQ1388_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f48782,f23085]) ).
fof(f48841,plain,
~ sQ1388_spl,
inference(contradiction_clause,[status(thm)],[f48840]) ).
fof(f48928,definition,
( sQ1407_spl
<=> v1_relat_1(k6_partfun1(np__0)) ),
introduced(definition,[new_symbols(definition,[sQ1407_spl])],[split_symbol_definition]) ).
fof(f48930,plain,
( sQ1407_spl
| ~ v1_relat_1(k6_partfun1(np__0)) ),
inference(component_clause,[status(thm)],[f48928]) ).
fof(f48937,plain,
( sQ1407_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f48930,f33349]) ).
fof(f48938,plain,
sQ1407_spl,
inference(contradiction_clause,[status(thm)],[f48937]) ).
fof(f49058,definition,
! [X1,X2] :
( sQ1411_spl
<=> k2_tarski(X1,X2) = np__0 ),
introduced(definition,[new_symbols(definition,[sQ1411_spl])],[split_symbol_definition]) ).
fof(f49059,plain,
! [X0,X1] :
( ~ sQ1411_spl
| k2_tarski(X0,X1) = np__0 ),
inference(component_clause,[status(thm)],[f49058]) ).
fof(f50184,definition,
( sQ1426_spl
<=> m1_subset_1(sK1205_skl,k1_zfmisc_1(sK1205_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1426_spl])],[split_symbol_definition]) ).
fof(f50186,plain,
( sQ1426_spl
| ~ m1_subset_1(sK1205_skl,k1_zfmisc_1(sK1205_skl)) ),
inference(component_clause,[status(thm)],[f50184]) ).
fof(f50385,definition,
( sQ1438_spl
<=> m1_subset_1(sK1206_skl,k1_zfmisc_1(k2_zfmisc_1(sK1205_skl,sK1207_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1438_spl])],[split_symbol_definition]) ).
fof(f50387,plain,
( sQ1438_spl
| ~ m1_subset_1(sK1206_skl,k1_zfmisc_1(k2_zfmisc_1(sK1205_skl,sK1207_skl))) ),
inference(component_clause,[status(thm)],[f50385]) ).
fof(f50396,plain,
( sQ1438_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f50387,f17562]) ).
fof(f50397,plain,
sQ1438_spl,
inference(contradiction_clause,[status(thm)],[f50396]) ).
fof(f51392,definition,
( sQ1487_spl
<=> v1_xboole_0(k1_zfmisc_1(f1_s1_subset_1)) ),
introduced(definition,[new_symbols(definition,[sQ1487_spl])],[split_symbol_definition]) ).
fof(f51393,plain,
( ~ sQ1487_spl
| v1_xboole_0(k1_zfmisc_1(f1_s1_subset_1)) ),
inference(component_clause,[status(thm)],[f51392]) ).
fof(f51399,plain,
( ~ sQ1487_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f51393,f5325]) ).
fof(f51400,plain,
~ sQ1487_spl,
inference(contradiction_clause,[status(thm)],[f51399]) ).
fof(f51624,definition,
( sQ1489_spl
<=> v1_xboole_0(k1_zfmisc_1(f1_s3_subset_1)) ),
introduced(definition,[new_symbols(definition,[sQ1489_spl])],[split_symbol_definition]) ).
fof(f51625,plain,
( ~ sQ1489_spl
| v1_xboole_0(k1_zfmisc_1(f1_s3_subset_1)) ),
inference(component_clause,[status(thm)],[f51624]) ).
fof(f51631,plain,
( ~ sQ1489_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f51625,f5325]) ).
fof(f51632,plain,
~ sQ1489_spl,
inference(contradiction_clause,[status(thm)],[f51631]) ).
fof(f51648,definition,
( sQ1493_spl
<=> m1_subset_1(sK1206_skl,k1_zfmisc_1(sK1206_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1493_spl])],[split_symbol_definition]) ).
fof(f51650,plain,
( sQ1493_spl
| ~ m1_subset_1(sK1206_skl,k1_zfmisc_1(sK1206_skl)) ),
inference(component_clause,[status(thm)],[f51648]) ).
fof(f52077,plain,
! [X0] : m1_subset_1(X0,k1_zfmisc_1(X0)),
inference(forward_demodulation,[status(thm)],[f5349,f5564]) ).
fof(f53367,definition,
! [X0] :
( sQ1553_spl
<=> r2_hidden(X0,k1_setfam_1(np__0)) ),
introduced(definition,[new_symbols(definition,[sQ1553_spl])],[split_symbol_definition]) ).
fof(f53368,plain,
! [X0] :
( ~ sQ1553_spl
| r2_hidden(X0,k1_setfam_1(np__0)) ),
inference(component_clause,[status(thm)],[f53367]) ).
fof(f53386,plain,
! [X0] :
( ~ sQ1553_spl
| r2_hidden(X0,np__0) ),
inference(forward_demodulation,[status(thm)],[f32799,f53368]) ).
fof(f53387,plain,
( ~ sQ1553_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f53386,f32492]) ).
fof(f53388,plain,
~ sQ1553_spl,
inference(contradiction_clause,[status(thm)],[f53387]) ).
fof(f53531,definition,
! [X0] :
( sQ1560_spl
<=> k4_xboole_0(k1_tarski(X0),k1_tarski(X0)) = k1_tarski(X0) ),
introduced(definition,[new_symbols(definition,[sQ1560_spl])],[split_symbol_definition]) ).
fof(f53532,plain,
! [X0] :
( ~ sQ1560_spl
| k4_xboole_0(k1_tarski(X0),k1_tarski(X0)) = k1_tarski(X0) ),
inference(component_clause,[status(thm)],[f53531]) ).
fof(f53562,plain,
! [X0] :
( ~ sQ1560_spl
| np__0 = k1_tarski(X0) ),
inference(forward_demodulation,[status(thm)],[f27749,f53532]) ).
fof(f53563,plain,
( ~ sQ1560_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f53562,f33116]) ).
fof(f53564,plain,
~ sQ1560_spl,
inference(contradiction_clause,[status(thm)],[f53563]) ).
fof(f53673,plain,
( sQ1426_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f50186,f52077]) ).
fof(f53674,plain,
sQ1426_spl,
inference(contradiction_clause,[status(thm)],[f53673]) ).
fof(f53896,plain,
( sQ1493_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f51650,f52077]) ).
fof(f53897,plain,
sQ1493_spl,
inference(contradiction_clause,[status(thm)],[f53896]) ).
fof(f54263,plain,
( ~ sQ1411_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f49059,f36173]) ).
fof(f54264,plain,
~ sQ1411_spl,
inference(contradiction_clause,[status(thm)],[f54263]) ).
fof(f54650,definition,
! [X0] :
( sQ1576_spl
<=> ~ m1_subset_1(np__0,k1_zfmisc_1(X0)) ),
introduced(definition,[new_symbols(definition,[sQ1576_spl])],[split_symbol_definition]) ).
fof(f54651,plain,
! [X0] :
( ~ sQ1576_spl
| ~ m1_subset_1(np__0,k1_zfmisc_1(X0)) ),
inference(component_clause,[status(thm)],[f54650]) ).
fof(f54654,plain,
( ~ sQ1576_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f54651,f23273]) ).
fof(f54655,plain,
~ sQ1576_spl,
inference(contradiction_clause,[status(thm)],[f54654]) ).
fof(f54660,definition,
( sQ1577_spl
<=> v1_relat_1(sK258_skl) ),
introduced(definition,[new_symbols(definition,[sQ1577_spl])],[split_symbol_definition]) ).
fof(f54662,plain,
( sQ1577_spl
| ~ v1_relat_1(sK258_skl) ),
inference(component_clause,[status(thm)],[f54660]) ).
fof(f54663,definition,
( sQ1578_spl
<=> v1_funct_1(sK258_skl) ),
introduced(definition,[new_symbols(definition,[sQ1578_spl])],[split_symbol_definition]) ).
fof(f54665,plain,
( sQ1578_spl
| ~ v1_funct_1(sK258_skl) ),
inference(component_clause,[status(thm)],[f54663]) ).
fof(f54682,plain,
( sQ1577_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f54662,f7404]) ).
fof(f54683,plain,
sQ1577_spl,
inference(contradiction_clause,[status(thm)],[f54682]) ).
fof(f54684,plain,
( sQ1578_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f54665,f7405]) ).
fof(f54685,plain,
sQ1578_spl,
inference(contradiction_clause,[status(thm)],[f54684]) ).
fof(f54843,definition,
! [X0,X1] :
( sQ1583_spl
<=> k4_xboole_0(k1_tarski(X0),k2_tarski(X1,X0)) = k1_tarski(X0) ),
introduced(definition,[new_symbols(definition,[sQ1583_spl])],[split_symbol_definition]) ).
fof(f54844,plain,
! [X0,X1] :
( ~ sQ1583_spl
| k4_xboole_0(k1_tarski(X0),k2_tarski(X1,X0)) = k1_tarski(X0) ),
inference(component_clause,[status(thm)],[f54843]) ).
fof(f54860,plain,
! [X0] :
( ~ sQ1583_spl
| np__0 = k1_tarski(X0) ),
inference(forward_demodulation,[status(thm)],[f40008,f54844]) ).
fof(f54861,plain,
( ~ sQ1583_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f54860,f33116]) ).
fof(f54862,plain,
~ sQ1583_spl,
inference(contradiction_clause,[status(thm)],[f54861]) ).
fof(f55012,plain,
( sQ420_spl
| ~ sQ765_spl
| ~ r1_tarski(k2_relat_1(k5_relset_2(sK1205_skl,sK1206_skl)),k1_zfmisc_1(k2_relat_1(sK1206_skl))) ),
inference(resolution,[status(thm)],[f24955,f20397]) ).
fof(f55014,plain,
( sQ420_spl
| ~ sQ765_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f55012,f26215]) ).
fof(f55015,plain,
( sQ420_spl
| ~ sQ765_spl ),
inference(contradiction_clause,[status(thm)],[f55014]) ).
fof(f55019,definition,
( sQ1585_spl
<=> v1_xboole_0(k1_zfmisc_1(sK1205_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1585_spl])],[split_symbol_definition]) ).
fof(f55020,plain,
( ~ sQ1585_spl
| v1_xboole_0(k1_zfmisc_1(sK1205_skl)) ),
inference(component_clause,[status(thm)],[f55019]) ).
fof(f55024,plain,
( ~ sQ1585_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f55020,f5325]) ).
fof(f55025,plain,
~ sQ1585_spl,
inference(contradiction_clause,[status(thm)],[f55024]) ).
fof(f55040,definition,
( sQ1587_spl
<=> k4_ordinal2 = np__0 ),
introduced(definition,[new_symbols(definition,[sQ1587_spl])],[split_symbol_definition]) ).
fof(f55041,plain,
( ~ sQ1587_spl
| k4_ordinal2 = np__0 ),
inference(component_clause,[status(thm)],[f55040]) ).
fof(f55068,plain,
( ~ sQ1587_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f55041,f33803]) ).
fof(f55069,plain,
~ sQ1587_spl,
inference(contradiction_clause,[status(thm)],[f55068]) ).
fof(f55393,plain,
( ~ sQ768_spl
| sQ421_spl
| ~ r1_tarski(k2_relat_1(k5_relset_2(sK1205_skl,sK1206_skl)),k1_zfmisc_1(k2_relat_1(sK1206_skl))) ),
inference(resolution,[status(thm)],[f20400,f24967]) ).
fof(f55395,plain,
( ~ sQ768_spl
| sQ421_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f55393,f26215]) ).
fof(f55396,plain,
( ~ sQ768_spl
| sQ421_spl ),
inference(contradiction_clause,[status(thm)],[f55395]) ).
fof(f55397,plain,
$false,
inference(sat_refutation,[status(thm)],[f20401,f22683,f24740,f24957,f24969,f25064,f25065,f25086,f25770,f26145,f26581,f26583,f26585,f26614,f26967,f26969,f27033,f27052,f27220,f27335,f27646,f27710,f27888,f29757,f30062,f31816,f32322,f32406,f33337,f33339,f33846,f33848,f33883,f33885,f33951,f34291,f34316,f34341,f34366,f34391,f34416,f34441,f34466,f34491,f34681,f35223,f35297,f35446,f35448,f35520,f35778,f35781,f35829,f35857,f35874,f35902,f36554,f36582,f39657,f39920,f40207,f40565,f41207,f41439,f42856,f42885,f43141,f43624,f43627,f43723,f44281,f44422,f44500,f44709,f44711,f44713,f44715,f44878,f44886,f44888,f44890,f44892,f44894,f44896,f47013,f47730,f48161,f48841,f48938,f50397,f51400,f51632,f53388,f53564,f53674,f53897,f54264,f54655,f54683,f54685,f54862,f55015,f55025,f55069,f55396]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU425+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/5.41 % Computer : n017.cluster.edu
% 0.13/5.41 % Model : x86_64 x86_64
% 0.13/5.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/5.41 % Memory : 8046.5625MB
% 0.13/5.41 % OS : Linux 6.8.0-71-generic
% 0.13/5.41 % CPULimit : 300
% 0.13/5.41 % WCLimit : 300
% 0.13/5.41 % DateTime : Mon Sep 21 06:22:32 UTC 2026
% 0.13/5.42 % CPUTime :
% 0.17/5.58 % Drodi V4.1.1
% 78.78/15.56 % Refutation found
% 78.78/15.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 78.78/15.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 34.74/15.78 % Elapsed time: 10.345308 seconds
% 34.74/15.78 % CPU time: 79.811689 seconds
% 34.74/15.78 % Total memory used: 1.087 GB
% 34.74/15.78 % Net memory used: 1.023 GB
%------------------------------------------------------------------------------