%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : TOP025+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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 03:53:25 PM UTC 2026
% Result : Timeout 299.51s 38.52s
% Output : None
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 96
% Syntax : Number of formulae : 383 ( 114 unt; 59 def)
% Number of atoms : 895 ( 82 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 836 ( 324 ~; 286 |; 136 &)
% ( 65 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 89 ( 87 usr; 60 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 18 con; 0-2 aty)
% Number of variables : 132 ( 117 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [A,B] : r1_tarski(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
v1_xboole_0(k1_xboole_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f65,axiom,
! [A] : k4_xboole_0(k1_xboole_0,A) = k1_xboole_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [A] : r1_tarski(k1_xboole_0,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f105,axiom,
! [A,B] : r1_tarski(k4_xboole_0(A,B),A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f349,axiom,
! [A] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f443,axiom,
! [A] : m1_subset_1(k8_subset_1(A),A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1868,axiom,
k1_numbers != k2_numbers,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1869,axiom,
k3_numbers != k1_numbers,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1870,axiom,
k3_numbers != k2_numbers,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1871,axiom,
k4_numbers != k3_numbers,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1872,axiom,
k4_numbers != k1_numbers,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1873,axiom,
k4_numbers != k2_numbers,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2163,axiom,
? [A] :
( v1_pre_topc(A)
& l1_pre_topc(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2164,axiom,
? [A] :
( v2_pre_topc(A)
& v1_pre_topc(A)
& ~ v3_struct_0(A)
& l1_pre_topc(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2183,axiom,
! [A] :
( l1_struct_0(A)
=> k2_pre_topc(A) = u1_struct_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2240,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( ( ( k6_pre_topc(A,B) = B
& v2_pre_topc(A) )
=> v4_pre_topc(B,A) )
& ( v4_pre_topc(B,A)
=> k6_pre_topc(A,B) = B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2245,axiom,
! [A] :
( l1_pre_topc(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2246,axiom,
? [A] : l1_pre_topc(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2273,axiom,
! [A] :
( l1_pre_topc(A)
=> ? [B] :
( v2_tops_1(B,A)
& v5_membered(B)
& v4_membered(B)
& v3_membered(B)
& v2_membered(B)
& v1_membered(B)
& v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2362,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v1_tops_1(B,A)
<=> k6_pre_topc(A,B) = k2_pre_topc(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2402,axiom,
! [A,B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& l1_pre_topc(A) )
=> m1_subset_1(k1_tops_1(A,B),k1_zfmisc_1(u1_struct_0(A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2403,axiom,
! [A,B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& l1_pre_topc(A) )
=> m1_subset_1(k2_tops_1(A,B),k1_zfmisc_1(u1_struct_0(A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2599,axiom,
? [A] :
( v2_pcomps_1(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A)
& l1_pre_topc(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2602,axiom,
? [A] :
( v3_compts_1(A)
& v2_pre_topc(A)
& v1_pre_topc(A)
& ~ v3_struct_0(A)
& l1_pre_topc(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2603,axiom,
? [A] :
( v3_pcomps_1(A)
& v2_pre_topc(A)
& v1_pre_topc(A)
& ~ v3_struct_0(A)
& l1_pre_topc(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2824,axiom,
! [A] :
( l1_pre_topc(A)
=> m1_pre_topc(A,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3108,axiom,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(A))
=> ( v1_tex_2(B,k1_zfmisc_1(A))
<=> B != A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3317,axiom,
? [A] :
( v2_t_0topsp(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A)
& l1_pre_topc(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3435,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v3_pre_topc(B,A)
=> k3_tex_4(A,B) = B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3509,axiom,
? [A] :
( v2_t_0topsp(A)
& v2_pre_topc(A)
& v1_pre_topc(A)
& ~ v3_struct_0(A)
& l1_pre_topc(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3510,axiom,
? [A] :
( ~ v2_t_0topsp(A)
& v2_pre_topc(A)
& v1_pre_topc(A)
& ~ v3_realset2(A)
& ~ v3_struct_0(A)
& l1_pre_topc(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3519,axiom,
? [A] :
( v2_t_0topsp(A)
& ~ v2_tdlat_3(A)
& v2_pre_topc(A)
& v1_pre_topc(A)
& ~ v3_realset2(A)
& ~ v3_struct_0(A)
& l1_pre_topc(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3520,axiom,
? [A] :
( ~ v2_t_0topsp(A)
& ~ v1_tdlat_3(A)
& v2_pre_topc(A)
& v1_pre_topc(A)
& ~ v3_realset2(A)
& ~ v3_struct_0(A)
& l1_pre_topc(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3582,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v1_tsp_2(B,A)
<=> ( k3_tex_4(A,B) = u1_struct_0(A)
& v1_tsp_1(B,A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3583,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v1_tsp_2(B,A)
=> v1_tops_1(B,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3584,conjecture,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ~ ( v1_tex_2(B,k1_zfmisc_1(u1_struct_0(A)))
& v1_tsp_2(B,A)
& ( v4_pre_topc(B,A)
| v3_pre_topc(B,A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3585,negated_conjecture,
~ ! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ~ ( v1_tex_2(B,k1_zfmisc_1(u1_struct_0(A)))
& v1_tsp_2(B,A)
& ( v4_pre_topc(B,A)
| v3_pre_topc(B,A) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f3584]) ).
fof(f3661,plain,
! [A] : r1_tarski(A,A),
inference(miniscoping,[status(thm)],[f18]) ).
fof(f3662,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[status(thm)],[f3661]) ).
fof(f3664,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f3801,plain,
! [X0] : k4_xboole_0(k1_xboole_0,X0) = k1_xboole_0,
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f3814,plain,
! [X0] : r1_tarski(k1_xboole_0,X0),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f3883,plain,
! [X0,X1] : r1_tarski(k4_xboole_0(X0,X1),X0),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f4442,plain,
! [X0] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(thm)],[f349]) ).
fof(f4689,plain,
! [X0] : m1_subset_1(k8_subset_1(X0),X0),
inference(cnf_transformation,[status(thm)],[f443]) ).
fof(f8887,plain,
k1_numbers != k2_numbers,
inference(cnf_transformation,[status(thm)],[f1868]) ).
fof(f8888,plain,
k3_numbers != k1_numbers,
inference(cnf_transformation,[status(thm)],[f1869]) ).
fof(f8889,plain,
k3_numbers != k2_numbers,
inference(cnf_transformation,[status(thm)],[f1870]) ).
fof(f8890,plain,
k4_numbers != k3_numbers,
inference(cnf_transformation,[status(thm)],[f1871]) ).
fof(f8891,plain,
k4_numbers != k1_numbers,
inference(cnf_transformation,[status(thm)],[f1872]) ).
fof(f8892,plain,
k4_numbers != k2_numbers,
inference(cnf_transformation,[status(thm)],[f1873]) ).
fof(f10000,plain,
( v1_pre_topc(sK568_skl)
& l1_pre_topc(sK568_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK568_skl]),skolemize(A,sK568_skl)],[f2163]) ).
fof(f10001,plain,
l1_pre_topc(sK568_skl),
inference(cnf_transformation,[status(thm)],[f10000]) ).
fof(f10003,plain,
( v2_pre_topc(sK569_skl)
& v1_pre_topc(sK569_skl)
& ~ v3_struct_0(sK569_skl)
& l1_pre_topc(sK569_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK569_skl]),skolemize(A,sK569_skl)],[f2164]) ).
fof(f10004,plain,
l1_pre_topc(sK569_skl),
inference(cnf_transformation,[status(thm)],[f10003]) ).
fof(f10005,plain,
~ v3_struct_0(sK569_skl),
inference(cnf_transformation,[status(thm)],[f10003]) ).
fof(f10007,plain,
v2_pre_topc(sK569_skl),
inference(cnf_transformation,[status(thm)],[f10003]) ).
fof(f10075,plain,
! [A] :
( k2_pre_topc(A) = u1_struct_0(A)
| ~ l1_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2183]) ).
fof(f10076,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f10075]) ).
fof(f10194,plain,
! [A] :
( ! [B] :
( ( ( v4_pre_topc(B,A)
| k6_pre_topc(A,B) != B
| ~ v2_pre_topc(A) )
& ( k6_pre_topc(A,B) = B
| ~ v4_pre_topc(B,A) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2240]) ).
fof(f10195,plain,
! [X0,X1] :
( k6_pre_topc(X0,X1) = X1
| ~ v4_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(thm)],[f10194]) ).
fof(f10214,plain,
! [A] :
( l1_struct_0(A)
| ~ l1_pre_topc(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2245]) ).
fof(f10215,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(thm)],[f10214]) ).
fof(f10216,plain,
l1_pre_topc(sK592_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK592_skl]),skolemize(A,sK592_skl)],[f2246]) ).
fof(f10217,plain,
l1_pre_topc(sK592_skl),
inference(cnf_transformation,[status(thm)],[f10216]) ).
fof(f10306,plain,
! [A] :
( ? [B] :
( v2_tops_1(B,A)
& v5_membered(B)
& v4_membered(B)
& v3_membered(B)
& v2_membered(B)
& v1_membered(B)
& v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2273]) ).
fof(f10307,plain,
! [A] :
( ( v2_tops_1(sK596_skl(A),A)
& v5_membered(sK596_skl(A))
& v4_membered(sK596_skl(A))
& v3_membered(sK596_skl(A))
& v2_membered(sK596_skl(A))
& v1_membered(sK596_skl(A))
& v1_xboole_0(sK596_skl(A))
& m1_subset_1(sK596_skl(A),k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK596_skl]),skolemize(B,sK596_skl(A))],[f10306]) ).
fof(f10308,plain,
! [X0] :
( m1_subset_1(sK596_skl(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(thm)],[f10307]) ).
fof(f10512,plain,
! [A] :
( ! [B] :
( ( v1_tops_1(B,A)
<=> k6_pre_topc(A,B) = k2_pre_topc(A) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2362]) ).
fof(f10513,plain,
! [A] :
( ! [B] :
( ( ( k6_pre_topc(A,B) != k2_pre_topc(A)
| v1_tops_1(B,A) )
& ( k6_pre_topc(A,B) = k2_pre_topc(A)
| ~ v1_tops_1(B,A) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A) ),
inference(NNF_transformation,[status(thm)],[f10512]) ).
fof(f10514,plain,
! [X0,X1] :
( k6_pre_topc(X0,X1) = k2_pre_topc(X0)
| ~ v1_tops_1(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(thm)],[f10513]) ).
fof(f10631,plain,
! [A,B] :
( m1_subset_1(k1_tops_1(A,B),k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2402]) ).
fof(f10632,plain,
! [X0,X1] :
( m1_subset_1(k1_tops_1(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(thm)],[f10631]) ).
fof(f10633,plain,
! [A,B] :
( m1_subset_1(k2_tops_1(A,B),k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2403]) ).
fof(f10634,plain,
! [X0,X1] :
( m1_subset_1(k2_tops_1(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(thm)],[f10633]) ).
fof(f11339,plain,
( v2_pcomps_1(sK682_skl)
& v2_pre_topc(sK682_skl)
& ~ v3_struct_0(sK682_skl)
& l1_pre_topc(sK682_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK682_skl]),skolemize(A,sK682_skl)],[f2599]) ).
fof(f11340,plain,
l1_pre_topc(sK682_skl),
inference(cnf_transformation,[status(thm)],[f11339]) ).
fof(f11341,plain,
~ v3_struct_0(sK682_skl),
inference(cnf_transformation,[status(thm)],[f11339]) ).
fof(f11351,plain,
( v3_compts_1(sK683_skl)
& v2_pre_topc(sK683_skl)
& v1_pre_topc(sK683_skl)
& ~ v3_struct_0(sK683_skl)
& l1_pre_topc(sK683_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK683_skl]),skolemize(A,sK683_skl)],[f2602]) ).
fof(f11352,plain,
l1_pre_topc(sK683_skl),
inference(cnf_transformation,[status(thm)],[f11351]) ).
fof(f11353,plain,
~ v3_struct_0(sK683_skl),
inference(cnf_transformation,[status(thm)],[f11351]) ).
fof(f11357,plain,
( v3_pcomps_1(sK684_skl)
& v2_pre_topc(sK684_skl)
& v1_pre_topc(sK684_skl)
& ~ v3_struct_0(sK684_skl)
& l1_pre_topc(sK684_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK684_skl]),skolemize(A,sK684_skl)],[f2603]) ).
fof(f11358,plain,
l1_pre_topc(sK684_skl),
inference(cnf_transformation,[status(thm)],[f11357]) ).
fof(f11359,plain,
~ v3_struct_0(sK684_skl),
inference(cnf_transformation,[status(thm)],[f11357]) ).
fof(f12123,plain,
! [A] :
( m1_pre_topc(A,A)
| ~ l1_pre_topc(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2824]) ).
fof(f12124,plain,
! [X0] :
( m1_pre_topc(X0,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(thm)],[f12123]) ).
fof(f13510,plain,
! [A,B] :
( ( v1_tex_2(B,k1_zfmisc_1(A))
<=> B != A )
| ~ m1_subset_1(B,k1_zfmisc_1(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f3108]) ).
fof(f13511,plain,
! [A,B] :
( ( ( B = A
| v1_tex_2(B,k1_zfmisc_1(A)) )
& ( B != A
| ~ v1_tex_2(B,k1_zfmisc_1(A)) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(A)) ),
inference(NNF_transformation,[status(thm)],[f13510]) ).
fof(f13512,plain,
! [X0,X1] :
( X0 != X1
| ~ v1_tex_2(X0,k1_zfmisc_1(X1))
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[status(thm)],[f13511]) ).
fof(f14597,plain,
( v2_t_0topsp(sK970_skl)
& v2_pre_topc(sK970_skl)
& ~ v3_struct_0(sK970_skl)
& l1_pre_topc(sK970_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK970_skl]),skolemize(A,sK970_skl)],[f3317]) ).
fof(f14598,plain,
l1_pre_topc(sK970_skl),
inference(cnf_transformation,[status(thm)],[f14597]) ).
fof(f15101,plain,
! [A] :
( ! [B] :
( k3_tex_4(A,B) = B
| ~ v3_pre_topc(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3435]) ).
fof(f15102,plain,
! [X0,X1] :
( k3_tex_4(X0,X1) = X1
| ~ v3_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f15101]) ).
fof(f15365,plain,
( v2_t_0topsp(sK1022_skl)
& v2_pre_topc(sK1022_skl)
& v1_pre_topc(sK1022_skl)
& ~ v3_struct_0(sK1022_skl)
& l1_pre_topc(sK1022_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1022_skl]),skolemize(A,sK1022_skl)],[f3509]) ).
fof(f15366,plain,
l1_pre_topc(sK1022_skl),
inference(cnf_transformation,[status(thm)],[f15365]) ).
fof(f15371,plain,
( ~ v2_t_0topsp(sK1023_skl)
& v2_pre_topc(sK1023_skl)
& v1_pre_topc(sK1023_skl)
& ~ v3_realset2(sK1023_skl)
& ~ v3_struct_0(sK1023_skl)
& l1_pre_topc(sK1023_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1023_skl]),skolemize(A,sK1023_skl)],[f3510]) ).
fof(f15372,plain,
l1_pre_topc(sK1023_skl),
inference(cnf_transformation,[status(thm)],[f15371]) ).
fof(f15428,plain,
( v2_t_0topsp(sK1024_skl)
& ~ v2_tdlat_3(sK1024_skl)
& v2_pre_topc(sK1024_skl)
& v1_pre_topc(sK1024_skl)
& ~ v3_realset2(sK1024_skl)
& ~ v3_struct_0(sK1024_skl)
& l1_pre_topc(sK1024_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1024_skl]),skolemize(A,sK1024_skl)],[f3519]) ).
fof(f15429,plain,
l1_pre_topc(sK1024_skl),
inference(cnf_transformation,[status(thm)],[f15428]) ).
fof(f15436,plain,
( ~ v2_t_0topsp(sK1025_skl)
& ~ v1_tdlat_3(sK1025_skl)
& v2_pre_topc(sK1025_skl)
& v1_pre_topc(sK1025_skl)
& ~ v3_realset2(sK1025_skl)
& ~ v3_struct_0(sK1025_skl)
& l1_pre_topc(sK1025_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1025_skl]),skolemize(A,sK1025_skl)],[f3520]) ).
fof(f15437,plain,
l1_pre_topc(sK1025_skl),
inference(cnf_transformation,[status(thm)],[f15436]) ).
fof(f15441,plain,
v2_pre_topc(sK1025_skl),
inference(cnf_transformation,[status(thm)],[f15436]) ).
fof(f15825,plain,
! [A] :
( ! [B] :
( ( v1_tsp_2(B,A)
<=> ( k3_tex_4(A,B) = u1_struct_0(A)
& v1_tsp_1(B,A) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3582]) ).
fof(f15826,plain,
! [A] :
( ! [B] :
( ( ( k3_tex_4(A,B) != u1_struct_0(A)
| ~ v1_tsp_1(B,A)
| v1_tsp_2(B,A) )
& ( ( k3_tex_4(A,B) = u1_struct_0(A)
& v1_tsp_1(B,A) )
| ~ v1_tsp_2(B,A) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f15825]) ).
fof(f15828,plain,
! [X0,X1] :
( k3_tex_4(X0,X1) = u1_struct_0(X0)
| ~ v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f15826]) ).
fof(f15830,plain,
! [A] :
( ! [B] :
( v1_tops_1(B,A)
| ~ v1_tsp_2(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3583]) ).
fof(f15831,plain,
! [X0,X1] :
( v1_tops_1(X1,X0)
| ~ v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f15830]) ).
fof(f15832,plain,
? [A] :
( ? [B] :
( v1_tex_2(B,k1_zfmisc_1(u1_struct_0(A)))
& v1_tsp_2(B,A)
& ( v4_pre_topc(B,A)
| v3_pre_topc(B,A) )
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
& l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3585]) ).
fof(f15833,plain,
( v1_tex_2(sK1084_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl)))
& v1_tsp_2(sK1084_skl,sK1083_skl)
& ( v4_pre_topc(sK1084_skl,sK1083_skl)
| v3_pre_topc(sK1084_skl,sK1083_skl) )
& m1_subset_1(sK1084_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl)))
& l1_pre_topc(sK1083_skl)
& v2_pre_topc(sK1083_skl)
& ~ v3_struct_0(sK1083_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1083_skl,sK1084_skl]),skolemize(A,sK1083_skl),skolemize(B,sK1084_skl)],[f15832]) ).
fof(f15834,plain,
~ v3_struct_0(sK1083_skl),
inference(cnf_transformation,[status(thm)],[f15833]) ).
fof(f15835,plain,
v2_pre_topc(sK1083_skl),
inference(cnf_transformation,[status(thm)],[f15833]) ).
fof(f15836,plain,
l1_pre_topc(sK1083_skl),
inference(cnf_transformation,[status(thm)],[f15833]) ).
fof(f15837,plain,
m1_subset_1(sK1084_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl))),
inference(cnf_transformation,[status(thm)],[f15833]) ).
fof(f15838,plain,
( v4_pre_topc(sK1084_skl,sK1083_skl)
| v3_pre_topc(sK1084_skl,sK1083_skl) ),
inference(cnf_transformation,[status(thm)],[f15833]) ).
fof(f15839,plain,
v1_tsp_2(sK1084_skl,sK1083_skl),
inference(cnf_transformation,[status(thm)],[f15833]) ).
fof(f15840,plain,
v1_tex_2(sK1084_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl))),
inference(cnf_transformation,[status(thm)],[f15833]) ).
fof(f18009,definition,
! [X1] :
( sQ332_spl
<=> ( ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ332_spl])],[split_symbol_definition]) ).
fof(f18010,plain,
! [X0] :
( ~ sQ332_spl
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0) ),
inference(component_clause,[status(thm)],[f18009]) ).
fof(f18044,definition,
( sQ341_spl
<=> v3_pre_topc(sK1084_skl,sK1083_skl) ),
introduced(definition,[new_symbols(definition,[sQ341_spl])],[split_symbol_definition]) ).
fof(f18047,definition,
( sQ342_spl
<=> v4_pre_topc(sK1084_skl,sK1083_skl) ),
introduced(definition,[new_symbols(definition,[sQ342_spl])],[split_symbol_definition]) ).
fof(f18048,plain,
( ~ sQ342_spl
| v4_pre_topc(sK1084_skl,sK1083_skl) ),
inference(component_clause,[status(thm)],[f18047]) ).
fof(f18050,plain,
( sQ342_spl
| sQ341_spl ),
inference(split_clause,[status(thm)],[f15838,f18044,f18047]) ).
fof(f18921,plain,
! [X0] :
( ~ v1_tex_2(X0,k1_zfmisc_1(X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f13512]) ).
fof(f19143,definition,
( sQ427_spl
<=> v2_pre_topc(sK1083_skl) ),
introduced(definition,[new_symbols(definition,[sQ427_spl])],[split_symbol_definition]) ).
fof(f19145,plain,
( sQ427_spl
| ~ v2_pre_topc(sK1083_skl) ),
inference(component_clause,[status(thm)],[f19143]) ).
fof(f19146,definition,
( sQ428_spl
<=> l1_pre_topc(sK1083_skl) ),
introduced(definition,[new_symbols(definition,[sQ428_spl])],[split_symbol_definition]) ).
fof(f19148,plain,
( sQ428_spl
| ~ l1_pre_topc(sK1083_skl) ),
inference(component_clause,[status(thm)],[f19146]) ).
fof(f19149,definition,
( sQ429_spl
<=> m1_pre_topc(sK1083_skl,sK1083_skl) ),
introduced(definition,[new_symbols(definition,[sQ429_spl])],[split_symbol_definition]) ).
fof(f19151,plain,
( sQ429_spl
| ~ m1_pre_topc(sK1083_skl,sK1083_skl) ),
inference(component_clause,[status(thm)],[f19149]) ).
fof(f19173,plain,
( sQ428_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19148,f15836]) ).
fof(f19174,plain,
sQ428_spl,
inference(contradiction_clause,[status(thm)],[f19173]) ).
fof(f19175,plain,
( sQ427_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19145,f15835]) ).
fof(f19176,plain,
sQ427_spl,
inference(contradiction_clause,[status(thm)],[f19175]) ).
fof(f19198,definition,
( sQ435_spl
<=> m1_subset_1(sK1084_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
introduced(definition,[new_symbols(definition,[sQ435_spl])],[split_symbol_definition]) ).
fof(f19200,plain,
( sQ435_spl
| ~ m1_subset_1(sK1084_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
inference(component_clause,[status(thm)],[f19198]) ).
fof(f19204,definition,
( sQ437_spl
<=> r1_tarski(sK1084_skl,sK1084_skl) ),
introduced(definition,[new_symbols(definition,[sQ437_spl])],[split_symbol_definition]) ).
fof(f19206,plain,
( sQ437_spl
| ~ r1_tarski(sK1084_skl,sK1084_skl) ),
inference(component_clause,[status(thm)],[f19204]) ).
fof(f19217,plain,
( sQ435_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19200,f15837]) ).
fof(f19218,plain,
sQ435_spl,
inference(contradiction_clause,[status(thm)],[f19217]) ).
fof(f19262,definition,
( sQ440_spl
<=> v3_struct_0(sK1083_skl) ),
introduced(definition,[new_symbols(definition,[sQ440_spl])],[split_symbol_definition]) ).
fof(f19263,plain,
( ~ sQ440_spl
| v3_struct_0(sK1083_skl) ),
inference(component_clause,[status(thm)],[f19262]) ).
fof(f19270,plain,
( ~ sQ440_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19263,f15834]) ).
fof(f19271,plain,
~ sQ440_spl,
inference(contradiction_clause,[status(thm)],[f19270]) ).
fof(f19283,definition,
( sQ444_spl
<=> v1_xboole_0(k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ444_spl])],[split_symbol_definition]) ).
fof(f19285,plain,
( sQ444_spl
| ~ v1_xboole_0(k1_xboole_0) ),
inference(component_clause,[status(thm)],[f19283]) ).
fof(f19307,definition,
( sQ446_spl
<=> m1_subset_1(k1_tops_1(sK1083_skl,sK1084_skl),k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
introduced(definition,[new_symbols(definition,[sQ446_spl])],[split_symbol_definition]) ).
fof(f19309,plain,
( sQ446_spl
| ~ m1_subset_1(k1_tops_1(sK1083_skl,sK1084_skl),k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
inference(component_clause,[status(thm)],[f19307]) ).
fof(f19313,definition,
( sQ448_spl
<=> r1_tarski(k1_tops_1(sK1083_skl,sK1084_skl),k1_tops_1(sK1083_skl,sK1084_skl)) ),
introduced(definition,[new_symbols(definition,[sQ448_spl])],[split_symbol_definition]) ).
fof(f19315,plain,
( sQ448_spl
| ~ r1_tarski(k1_tops_1(sK1083_skl,sK1084_skl),k1_tops_1(sK1083_skl,sK1084_skl)) ),
inference(component_clause,[status(thm)],[f19313]) ).
fof(f19329,plain,
( sQ448_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19315,f3662]) ).
fof(f19330,plain,
sQ448_spl,
inference(contradiction_clause,[status(thm)],[f19329]) ).
fof(f19332,plain,
! [X0] :
( k3_tex_4(sK1083_skl,X0) = u1_struct_0(sK1083_skl)
| ~ v1_tsp_2(X0,sK1083_skl)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl)))
| ~ l1_pre_topc(sK1083_skl)
| v3_struct_0(sK1083_skl) ),
inference(resolution,[status(thm)],[f15828,f15835]) ).
fof(f19334,definition,
! [X0] :
( sQ452_spl
<=> ( k3_tex_4(sK1083_skl,X0) = u1_struct_0(sK1083_skl)
| ~ v1_tsp_2(X0,sK1083_skl)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ452_spl])],[split_symbol_definition]) ).
fof(f19335,plain,
! [X0] :
( ~ sQ452_spl
| k3_tex_4(sK1083_skl,X0) = u1_struct_0(sK1083_skl)
| ~ v1_tsp_2(X0,sK1083_skl)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
inference(component_clause,[status(thm)],[f19334]) ).
fof(f19337,plain,
( sQ452_spl
| ~ sQ428_spl
| sQ440_spl ),
inference(split_clause,[status(thm)],[f19332,f19262,f19146,f19334]) ).
fof(f19439,plain,
( ~ sQ452_spl
| k3_tex_4(sK1083_skl,sK1084_skl) = u1_struct_0(sK1083_skl)
| ~ m1_subset_1(sK1084_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
inference(resolution,[status(thm)],[f19335,f15839]) ).
fof(f19441,definition,
( sQ462_spl
<=> k3_tex_4(sK1083_skl,sK1084_skl) = u1_struct_0(sK1083_skl) ),
introduced(definition,[new_symbols(definition,[sQ462_spl])],[split_symbol_definition]) ).
fof(f19442,plain,
( ~ sQ462_spl
| k3_tex_4(sK1083_skl,sK1084_skl) = u1_struct_0(sK1083_skl) ),
inference(component_clause,[status(thm)],[f19441]) ).
fof(f19444,plain,
( ~ sQ452_spl
| sQ462_spl
| ~ sQ435_spl ),
inference(split_clause,[status(thm)],[f19439,f19198,f19441,f19334]) ).
fof(f19455,definition,
( sQ464_spl
<=> m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
introduced(definition,[new_symbols(definition,[sQ464_spl])],[split_symbol_definition]) ).
fof(f19457,plain,
( sQ464_spl
| ~ m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
inference(component_clause,[status(thm)],[f19455]) ).
fof(f19474,plain,
( sQ464_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19457,f4442]) ).
fof(f19475,plain,
sQ464_spl,
inference(contradiction_clause,[status(thm)],[f19474]) ).
fof(f19520,definition,
( sQ471_spl
<=> m1_subset_1(k1_tops_1(sK1083_skl,k1_xboole_0),k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
introduced(definition,[new_symbols(definition,[sQ471_spl])],[split_symbol_definition]) ).
fof(f19522,plain,
( sQ471_spl
| ~ m1_subset_1(k1_tops_1(sK1083_skl,k1_xboole_0),k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
inference(component_clause,[status(thm)],[f19520]) ).
fof(f19526,definition,
( sQ473_spl
<=> r1_tarski(k1_tops_1(sK1083_skl,k1_xboole_0),k1_tops_1(sK1083_skl,k1_xboole_0)) ),
introduced(definition,[new_symbols(definition,[sQ473_spl])],[split_symbol_definition]) ).
fof(f19528,plain,
( sQ473_spl
| ~ r1_tarski(k1_tops_1(sK1083_skl,k1_xboole_0),k1_tops_1(sK1083_skl,k1_xboole_0)) ),
inference(component_clause,[status(thm)],[f19526]) ).
fof(f19542,plain,
( sQ473_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19528,f3662]) ).
fof(f19543,plain,
sQ473_spl,
inference(contradiction_clause,[status(thm)],[f19542]) ).
fof(f19578,plain,
( sQ437_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19206,f3662]) ).
fof(f19579,plain,
sQ437_spl,
inference(contradiction_clause,[status(thm)],[f19578]) ).
fof(f19584,definition,
( sQ481_spl
<=> m1_subset_1(k1_tops_1(sK1083_skl,k8_subset_1(k1_zfmisc_1(u1_struct_0(sK1083_skl)))),k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
introduced(definition,[new_symbols(definition,[sQ481_spl])],[split_symbol_definition]) ).
fof(f19586,plain,
( sQ481_spl
| ~ m1_subset_1(k1_tops_1(sK1083_skl,k8_subset_1(k1_zfmisc_1(u1_struct_0(sK1083_skl)))),k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
inference(component_clause,[status(thm)],[f19584]) ).
fof(f19590,definition,
( sQ483_spl
<=> r1_tarski(k1_tops_1(sK1083_skl,k8_subset_1(k1_zfmisc_1(u1_struct_0(sK1083_skl)))),k1_tops_1(sK1083_skl,k8_subset_1(k1_zfmisc_1(u1_struct_0(sK1083_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ483_spl])],[split_symbol_definition]) ).
fof(f19592,plain,
( sQ483_spl
| ~ r1_tarski(k1_tops_1(sK1083_skl,k8_subset_1(k1_zfmisc_1(u1_struct_0(sK1083_skl)))),k1_tops_1(sK1083_skl,k8_subset_1(k1_zfmisc_1(u1_struct_0(sK1083_skl))))) ),
inference(component_clause,[status(thm)],[f19590]) ).
fof(f19606,plain,
( sQ483_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19592,f3662]) ).
fof(f19607,plain,
sQ483_spl,
inference(contradiction_clause,[status(thm)],[f19606]) ).
fof(f20033,definition,
( sQ495_spl
<=> v3_struct_0(sK569_skl) ),
introduced(definition,[new_symbols(definition,[sQ495_spl])],[split_symbol_definition]) ).
fof(f20034,plain,
( ~ sQ495_spl
| v3_struct_0(sK569_skl) ),
inference(component_clause,[status(thm)],[f20033]) ).
fof(f20036,definition,
( sQ496_spl
<=> v2_pre_topc(sK569_skl) ),
introduced(definition,[new_symbols(definition,[sQ496_spl])],[split_symbol_definition]) ).
fof(f20038,plain,
( sQ496_spl
| ~ v2_pre_topc(sK569_skl) ),
inference(component_clause,[status(thm)],[f20036]) ).
fof(f20050,definition,
( sQ499_spl
<=> l1_pre_topc(sK569_skl) ),
introduced(definition,[new_symbols(definition,[sQ499_spl])],[split_symbol_definition]) ).
fof(f20052,plain,
( sQ499_spl
| ~ l1_pre_topc(sK569_skl) ),
inference(component_clause,[status(thm)],[f20050]) ).
fof(f20059,plain,
( sQ499_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20052,f10004]) ).
fof(f20060,plain,
sQ499_spl,
inference(contradiction_clause,[status(thm)],[f20059]) ).
fof(f20075,definition,
( sQ502_spl
<=> l1_pre_topc(sK568_skl) ),
introduced(definition,[new_symbols(definition,[sQ502_spl])],[split_symbol_definition]) ).
fof(f20077,plain,
( sQ502_spl
| ~ l1_pre_topc(sK568_skl) ),
inference(component_clause,[status(thm)],[f20075]) ).
fof(f20079,plain,
( sQ502_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20077,f10001]) ).
fof(f20080,plain,
sQ502_spl,
inference(contradiction_clause,[status(thm)],[f20079]) ).
fof(f20093,plain,
( sQ496_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20038,f10007]) ).
fof(f20094,plain,
sQ496_spl,
inference(contradiction_clause,[status(thm)],[f20093]) ).
fof(f20095,plain,
( ~ sQ495_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20034,f10005]) ).
fof(f20096,plain,
~ sQ495_spl,
inference(contradiction_clause,[status(thm)],[f20095]) ).
fof(f20104,definition,
( sQ506_spl
<=> m1_pre_topc(sK568_skl,sK568_skl) ),
introduced(definition,[new_symbols(definition,[sQ506_spl])],[split_symbol_definition]) ).
fof(f20106,plain,
( sQ506_spl
| ~ m1_pre_topc(sK568_skl,sK568_skl) ),
inference(component_clause,[status(thm)],[f20104]) ).
fof(f20122,definition,
( sQ509_spl
<=> m1_pre_topc(sK569_skl,sK569_skl) ),
introduced(definition,[new_symbols(definition,[sQ509_spl])],[split_symbol_definition]) ).
fof(f20124,plain,
( sQ509_spl
| ~ m1_pre_topc(sK569_skl,sK569_skl) ),
inference(component_clause,[status(thm)],[f20122]) ).
fof(f20167,definition,
( sQ515_spl
<=> k2_numbers = k4_numbers ),
introduced(definition,[new_symbols(definition,[sQ515_spl])],[split_symbol_definition]) ).
fof(f20168,plain,
( ~ sQ515_spl
| k2_numbers = k4_numbers ),
inference(component_clause,[status(thm)],[f20167]) ).
fof(f20174,definition,
( sQ517_spl
<=> k1_numbers = k4_numbers ),
introduced(definition,[new_symbols(definition,[sQ517_spl])],[split_symbol_definition]) ).
fof(f20175,plain,
( ~ sQ517_spl
| k1_numbers = k4_numbers ),
inference(component_clause,[status(thm)],[f20174]) ).
fof(f20181,definition,
( sQ519_spl
<=> k3_numbers = k4_numbers ),
introduced(definition,[new_symbols(definition,[sQ519_spl])],[split_symbol_definition]) ).
fof(f20182,plain,
( ~ sQ519_spl
| k3_numbers = k4_numbers ),
inference(component_clause,[status(thm)],[f20181]) ).
fof(f20188,definition,
( sQ521_spl
<=> k2_numbers = k3_numbers ),
introduced(definition,[new_symbols(definition,[sQ521_spl])],[split_symbol_definition]) ).
fof(f20189,plain,
( ~ sQ521_spl
| k2_numbers = k3_numbers ),
inference(component_clause,[status(thm)],[f20188]) ).
fof(f20195,definition,
( sQ523_spl
<=> k1_numbers = k3_numbers ),
introduced(definition,[new_symbols(definition,[sQ523_spl])],[split_symbol_definition]) ).
fof(f20196,plain,
( ~ sQ523_spl
| k1_numbers = k3_numbers ),
inference(component_clause,[status(thm)],[f20195]) ).
fof(f20202,definition,
( sQ525_spl
<=> k2_numbers = k1_numbers ),
introduced(definition,[new_symbols(definition,[sQ525_spl])],[split_symbol_definition]) ).
fof(f20203,plain,
( ~ sQ525_spl
| k2_numbers = k1_numbers ),
inference(component_clause,[status(thm)],[f20202]) ).
fof(f20209,plain,
( ~ sQ525_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20203,f8887]) ).
fof(f20210,plain,
~ sQ525_spl,
inference(contradiction_clause,[status(thm)],[f20209]) ).
fof(f20211,plain,
( ~ sQ523_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20196,f8888]) ).
fof(f20212,plain,
~ sQ523_spl,
inference(contradiction_clause,[status(thm)],[f20211]) ).
fof(f20213,plain,
( ~ sQ521_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20189,f8889]) ).
fof(f20214,plain,
~ sQ521_spl,
inference(contradiction_clause,[status(thm)],[f20213]) ).
fof(f20215,plain,
( ~ sQ519_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20182,f8890]) ).
fof(f20216,plain,
~ sQ519_spl,
inference(contradiction_clause,[status(thm)],[f20215]) ).
fof(f20217,plain,
( ~ sQ517_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20175,f8891]) ).
fof(f20218,plain,
~ sQ517_spl,
inference(contradiction_clause,[status(thm)],[f20217]) ).
fof(f20219,plain,
( ~ sQ515_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20168,f8892]) ).
fof(f20220,plain,
~ sQ515_spl,
inference(contradiction_clause,[status(thm)],[f20219]) ).
fof(f20350,definition,
( sQ543_spl
<=> m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK569_skl))) ),
introduced(definition,[new_symbols(definition,[sQ543_spl])],[split_symbol_definition]) ).
fof(f20352,plain,
( sQ543_spl
| ~ m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK569_skl))) ),
inference(component_clause,[status(thm)],[f20350]) ).
fof(f20366,plain,
( sQ543_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20352,f4442]) ).
fof(f20367,plain,
sQ543_spl,
inference(contradiction_clause,[status(thm)],[f20366]) ).
fof(f20623,definition,
( sQ576_spl
<=> m1_subset_1(k8_subset_1(k1_zfmisc_1(u1_struct_0(sK1083_skl))),k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
introduced(definition,[new_symbols(definition,[sQ576_spl])],[split_symbol_definition]) ).
fof(f20625,plain,
( sQ576_spl
| ~ m1_subset_1(k8_subset_1(k1_zfmisc_1(u1_struct_0(sK1083_skl))),k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
inference(component_clause,[status(thm)],[f20623]) ).
fof(f20631,plain,
( sQ576_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20625,f4689]) ).
fof(f20632,plain,
sQ576_spl,
inference(contradiction_clause,[status(thm)],[f20631]) ).
fof(f20691,plain,
! [X0] :
( k6_pre_topc(sK1083_skl,X0) = X0
| ~ v4_pre_topc(X0,sK1083_skl)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
inference(resolution,[status(thm)],[f10195,f15836]) ).
fof(f20718,plain,
l1_struct_0(sK1083_skl),
inference(resolution,[status(thm)],[f10215,f15836]) ).
fof(f20819,plain,
( ~ sQ342_spl
| k6_pre_topc(sK1083_skl,sK1084_skl) = sK1084_skl
| ~ m1_subset_1(sK1084_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
inference(resolution,[status(thm)],[f20691,f18048]) ).
fof(f20826,definition,
( sQ604_spl
<=> k6_pre_topc(sK1083_skl,sK1084_skl) = sK1084_skl ),
introduced(definition,[new_symbols(definition,[sQ604_spl])],[split_symbol_definition]) ).
fof(f20827,plain,
( ~ sQ604_spl
| k6_pre_topc(sK1083_skl,sK1084_skl) = sK1084_skl ),
inference(component_clause,[status(thm)],[f20826]) ).
fof(f20828,plain,
( sQ604_spl
| k6_pre_topc(sK1083_skl,sK1084_skl) != sK1084_skl ),
inference(component_clause,[status(thm)],[f20826]) ).
fof(f20829,plain,
( ~ sQ342_spl
| sQ604_spl
| ~ sQ435_spl ),
inference(split_clause,[status(thm)],[f20819,f19198,f20826,f18047]) ).
fof(f20882,plain,
k2_pre_topc(sK1083_skl) = u1_struct_0(sK1083_skl),
inference(resolution,[status(thm)],[f20718,f10076]) ).
fof(f20901,definition,
( sQ613_spl
<=> r1_tarski(k1_xboole_0,sK1084_skl) ),
introduced(definition,[new_symbols(definition,[sQ613_spl])],[split_symbol_definition]) ).
fof(f20903,plain,
( sQ613_spl
| ~ r1_tarski(k1_xboole_0,sK1084_skl) ),
inference(component_clause,[status(thm)],[f20901]) ).
fof(f20912,plain,
( sQ613_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20903,f3814]) ).
fof(f20913,plain,
sQ613_spl,
inference(contradiction_clause,[status(thm)],[f20912]) ).
fof(f20918,definition,
( sQ617_spl
<=> l1_pre_topc(sK592_skl) ),
introduced(definition,[new_symbols(definition,[sQ617_spl])],[split_symbol_definition]) ).
fof(f20920,plain,
( sQ617_spl
| ~ l1_pre_topc(sK592_skl) ),
inference(component_clause,[status(thm)],[f20918]) ).
fof(f20922,plain,
( sQ617_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20920,f10217]) ).
fof(f20923,plain,
sQ617_spl,
inference(contradiction_clause,[status(thm)],[f20922]) ).
fof(f21081,plain,
m1_subset_1(sK596_skl(sK1083_skl),k1_zfmisc_1(u1_struct_0(sK1083_skl))),
inference(resolution,[status(thm)],[f10308,f15836]) ).
fof(f21464,plain,
( sQ444_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19285,f3664]) ).
fof(f21465,plain,
sQ444_spl,
inference(contradiction_clause,[status(thm)],[f21464]) ).
fof(f21917,plain,
! [X0,X1] :
( ~ v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| k6_pre_topc(X0,X1) = k2_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(resolution,[status(thm)],[f10514,f15831]) ).
fof(f21918,plain,
! [X0,X1] :
( ~ v1_tsp_2(X1,X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| k6_pre_topc(X0,X1) = k2_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f21917]) ).
fof(f22344,plain,
( ~ v2_pre_topc(sK1083_skl)
| v3_struct_0(sK1083_skl)
| k6_pre_topc(sK1083_skl,sK1084_skl) = k2_pre_topc(sK1083_skl)
| ~ m1_subset_1(sK1084_skl,k1_zfmisc_1(u1_struct_0(sK1083_skl)))
| ~ l1_pre_topc(sK1083_skl) ),
inference(resolution,[status(thm)],[f21918,f15839]) ).
fof(f22346,definition,
( sQ748_spl
<=> k6_pre_topc(sK1083_skl,sK1084_skl) = k2_pre_topc(sK1083_skl) ),
introduced(definition,[new_symbols(definition,[sQ748_spl])],[split_symbol_definition]) ).
fof(f22347,plain,
( ~ sQ748_spl
| k6_pre_topc(sK1083_skl,sK1084_skl) = k2_pre_topc(sK1083_skl) ),
inference(component_clause,[status(thm)],[f22346]) ).
fof(f22349,plain,
( ~ sQ427_spl
| sQ440_spl
| sQ748_spl
| ~ sQ435_spl
| ~ sQ428_spl ),
inference(split_clause,[status(thm)],[f22344,f19146,f19198,f22346,f19262,f19143]) ).
fof(f22351,plain,
( ~ sQ748_spl
| k6_pre_topc(sK1083_skl,sK1084_skl) = u1_struct_0(sK1083_skl) ),
inference(forward_demodulation,[status(thm)],[f20882,f22347]) ).
fof(f22922,plain,
! [X0] :
( m1_subset_1(k1_tops_1(sK1083_skl,X0),k1_zfmisc_1(u1_struct_0(sK1083_skl)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
inference(resolution,[status(thm)],[f10632,f15836]) ).
fof(f22926,plain,
! [X0] :
( m1_subset_1(k2_tops_1(sK1083_skl,X0),k1_zfmisc_1(u1_struct_0(sK1083_skl)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
inference(resolution,[status(thm)],[f10634,f15836]) ).
fof(f22984,plain,
( sQ604_spl
| ~ sQ748_spl
| u1_struct_0(sK1083_skl) != sK1084_skl ),
inference(backward_demodulation,[status(thm)],[f22351,f20828]) ).
fof(f23007,plain,
m1_subset_1(k1_tops_1(sK1083_skl,k8_subset_1(k1_zfmisc_1(u1_struct_0(sK1083_skl)))),k1_zfmisc_1(u1_struct_0(sK1083_skl))),
inference(resolution,[status(thm)],[f22922,f4689]) ).
fof(f23008,plain,
m1_subset_1(k1_tops_1(sK1083_skl,k1_xboole_0),k1_zfmisc_1(u1_struct_0(sK1083_skl))),
inference(resolution,[status(thm)],[f22922,f4442]) ).
fof(f23009,plain,
m1_subset_1(k1_tops_1(sK1083_skl,sK1084_skl),k1_zfmisc_1(u1_struct_0(sK1083_skl))),
inference(resolution,[status(thm)],[f22922,f15837]) ).
fof(f23010,plain,
( sQ481_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23007,f19586]) ).
fof(f23011,plain,
sQ481_spl,
inference(contradiction_clause,[status(thm)],[f23010]) ).
fof(f23012,plain,
( sQ471_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23008,f19522]) ).
fof(f23013,plain,
sQ471_spl,
inference(contradiction_clause,[status(thm)],[f23012]) ).
fof(f23014,plain,
( sQ446_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23009,f19309]) ).
fof(f23015,plain,
sQ446_spl,
inference(contradiction_clause,[status(thm)],[f23014]) ).
fof(f23648,definition,
! [X0,X1] :
( sQ868_spl
<=> ( ~ r1_tarski(X1,sK1084_skl)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(k1_xboole_0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ868_spl])],[split_symbol_definition]) ).
fof(f23649,plain,
! [X0,X1] :
( ~ sQ868_spl
| ~ r1_tarski(X1,sK1084_skl)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(k1_xboole_0,X0) ),
inference(component_clause,[status(thm)],[f23648]) ).
fof(f23652,plain,
! [X0,X1] :
( ~ sQ868_spl
| ~ r1_tarski(X1,sK1084_skl)
| ~ r1_tarski(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f23649,f3814]) ).
fof(f23712,definition,
! [X0] :
( sQ881_spl
<=> ( ~ r1_tarski(X0,sK1084_skl)
| ~ r1_tarski(k1_xboole_0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ881_spl])],[split_symbol_definition]) ).
fof(f23713,plain,
! [X0] :
( ~ sQ881_spl
| ~ r1_tarski(X0,sK1084_skl)
| ~ r1_tarski(k1_xboole_0,X0) ),
inference(component_clause,[status(thm)],[f23712]) ).
fof(f23716,plain,
! [X0] :
( ~ sQ881_spl
| ~ r1_tarski(X0,sK1084_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f23713,f3814]) ).
fof(f24210,definition,
( sQ921_spl
<=> v3_struct_0(sK682_skl) ),
introduced(definition,[new_symbols(definition,[sQ921_spl])],[split_symbol_definition]) ).
fof(f24211,plain,
( ~ sQ921_spl
| v3_struct_0(sK682_skl) ),
inference(component_clause,[status(thm)],[f24210]) ).
fof(f24309,definition,
! [X0] :
( sQ924_spl
<=> ~ r1_tarski(k1_xboole_0,X0) ),
introduced(definition,[new_symbols(definition,[sQ924_spl])],[split_symbol_definition]) ).
fof(f24310,plain,
! [X0] :
( ~ sQ924_spl
| ~ r1_tarski(k1_xboole_0,X0) ),
inference(component_clause,[status(thm)],[f24309]) ).
fof(f24313,plain,
( ~ sQ924_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24310,f3814]) ).
fof(f24314,plain,
~ sQ924_spl,
inference(contradiction_clause,[status(thm)],[f24313]) ).
fof(f24396,definition,
( sQ937_spl
<=> l1_pre_topc(sK682_skl) ),
introduced(definition,[new_symbols(definition,[sQ937_spl])],[split_symbol_definition]) ).
fof(f24398,plain,
( sQ937_spl
| ~ l1_pre_topc(sK682_skl) ),
inference(component_clause,[status(thm)],[f24396]) ).
fof(f24413,plain,
( sQ937_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24398,f11340]) ).
fof(f24414,plain,
sQ937_spl,
inference(contradiction_clause,[status(thm)],[f24413]) ).
fof(f24512,definition,
( sQ955_spl
<=> v3_struct_0(sK683_skl) ),
introduced(definition,[new_symbols(definition,[sQ955_spl])],[split_symbol_definition]) ).
fof(f24513,plain,
( ~ sQ955_spl
| v3_struct_0(sK683_skl) ),
inference(component_clause,[status(thm)],[f24512]) ).
fof(f24528,definition,
( sQ958_spl
<=> l1_pre_topc(sK683_skl) ),
introduced(definition,[new_symbols(definition,[sQ958_spl])],[split_symbol_definition]) ).
fof(f24530,plain,
( sQ958_spl
| ~ l1_pre_topc(sK683_skl) ),
inference(component_clause,[status(thm)],[f24528]) ).
fof(f24545,plain,
( sQ958_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24530,f11352]) ).
fof(f24546,plain,
sQ958_spl,
inference(contradiction_clause,[status(thm)],[f24545]) ).
fof(f24644,definition,
( sQ976_spl
<=> v3_struct_0(sK684_skl) ),
introduced(definition,[new_symbols(definition,[sQ976_spl])],[split_symbol_definition]) ).
fof(f24645,plain,
( ~ sQ976_spl
| v3_struct_0(sK684_skl) ),
inference(component_clause,[status(thm)],[f24644]) ).
fof(f24937,definition,
( sQ996_spl
<=> l1_pre_topc(sK684_skl) ),
introduced(definition,[new_symbols(definition,[sQ996_spl])],[split_symbol_definition]) ).
fof(f24939,plain,
( sQ996_spl
| ~ l1_pre_topc(sK684_skl) ),
inference(component_clause,[status(thm)],[f24937]) ).
fof(f24954,plain,
( sQ996_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24939,f11358]) ).
fof(f24955,plain,
sQ996_spl,
inference(contradiction_clause,[status(thm)],[f24954]) ).
fof(f25228,definition,
( sQ1016_spl
<=> m1_subset_1(sK596_skl(sK1083_skl),k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1016_spl])],[split_symbol_definition]) ).
fof(f25230,plain,
( sQ1016_spl
| ~ m1_subset_1(sK596_skl(sK1083_skl),k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
inference(component_clause,[status(thm)],[f25228]) ).
fof(f25237,plain,
( sQ1016_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25230,f21081]) ).
fof(f25238,plain,
sQ1016_spl,
inference(contradiction_clause,[status(thm)],[f25237]) ).
fof(f25627,plain,
( ~ sQ604_spl
| ~ sQ748_spl
| u1_struct_0(sK1083_skl) = sK1084_skl ),
inference(forward_demodulation,[status(thm)],[f22351,f20827]) ).
fof(f25900,definition,
( sQ1043_spl
<=> m1_subset_1(k1_xboole_0,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK1083_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ1043_spl])],[split_symbol_definition]) ).
fof(f25902,plain,
( sQ1043_spl
| ~ m1_subset_1(k1_xboole_0,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK1083_skl)))) ),
inference(component_clause,[status(thm)],[f25900]) ).
fof(f25907,plain,
( sQ1043_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25902,f4442]) ).
fof(f25908,plain,
sQ1043_spl,
inference(contradiction_clause,[status(thm)],[f25907]) ).
fof(f25949,plain,
m1_pre_topc(sK569_skl,sK569_skl),
inference(resolution,[status(thm)],[f12124,f10004]) ).
fof(f25950,plain,
m1_pre_topc(sK568_skl,sK568_skl),
inference(resolution,[status(thm)],[f12124,f10001]) ).
fof(f25951,plain,
m1_pre_topc(sK1083_skl,sK1083_skl),
inference(resolution,[status(thm)],[f12124,f15836]) ).
fof(f25952,plain,
( sQ509_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25949,f20124]) ).
fof(f25953,plain,
sQ509_spl,
inference(contradiction_clause,[status(thm)],[f25952]) ).
fof(f25954,plain,
( sQ506_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25950,f20106]) ).
fof(f25955,plain,
sQ506_spl,
inference(contradiction_clause,[status(thm)],[f25954]) ).
fof(f25956,plain,
( sQ429_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25951,f19151]) ).
fof(f25957,plain,
sQ429_spl,
inference(contradiction_clause,[status(thm)],[f25956]) ).
fof(f26161,plain,
! [X0] :
( ~ sQ868_spl
| ~ r1_tarski(X0,sK1084_skl) ),
inference(resolution,[status(thm)],[f23652,f3662]) ).
fof(f26167,plain,
( ~ sQ881_spl
| $false ),
inference(resolution,[status(thm)],[f23716,f3883]) ).
fof(f26176,plain,
~ sQ881_spl,
inference(contradiction_clause,[status(thm)],[f26167]) ).
fof(f26373,plain,
( ~ sQ921_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24211,f11341]) ).
fof(f26374,plain,
~ sQ921_spl,
inference(contradiction_clause,[status(thm)],[f26373]) ).
fof(f26561,plain,
( ~ sQ955_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24513,f11353]) ).
fof(f26562,plain,
~ sQ955_spl,
inference(contradiction_clause,[status(thm)],[f26561]) ).
fof(f26649,definition,
! [X0] :
( sQ1102_spl
<=> ~ r1_tarski(k1_xboole_0,k4_xboole_0(sK1084_skl,X0)) ),
introduced(definition,[new_symbols(definition,[sQ1102_spl])],[split_symbol_definition]) ).
fof(f26650,plain,
! [X0] :
( ~ sQ1102_spl
| ~ r1_tarski(k1_xboole_0,k4_xboole_0(sK1084_skl,X0)) ),
inference(component_clause,[status(thm)],[f26649]) ).
fof(f26653,plain,
( ~ sQ1102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26650,f3814]) ).
fof(f26654,plain,
~ sQ1102_spl,
inference(contradiction_clause,[status(thm)],[f26653]) ).
fof(f26742,definition,
( sQ1112_spl
<=> k4_xboole_0(k1_xboole_0,k2_tops_1(sK1083_skl,k1_xboole_0)) = k1_xboole_0 ),
introduced(definition,[new_symbols(definition,[sQ1112_spl])],[split_symbol_definition]) ).
fof(f26744,plain,
( sQ1112_spl
| k4_xboole_0(k1_xboole_0,k2_tops_1(sK1083_skl,k1_xboole_0)) != k1_xboole_0 ),
inference(component_clause,[status(thm)],[f26742]) ).
fof(f26746,plain,
( sQ1112_spl
| k1_xboole_0 != k1_xboole_0 ),
inference(forward_demodulation,[status(thm)],[f3801,f26744]) ).
fof(f26747,plain,
( sQ1112_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f26746]) ).
fof(f26748,plain,
sQ1112_spl,
inference(contradiction_clause,[status(thm)],[f26747]) ).
fof(f26756,definition,
( sQ1114_spl
<=> m1_subset_1(k2_tops_1(sK1083_skl,sK1084_skl),k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1114_spl])],[split_symbol_definition]) ).
fof(f26758,plain,
( sQ1114_spl
| ~ m1_subset_1(k2_tops_1(sK1083_skl,sK1084_skl),k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
inference(component_clause,[status(thm)],[f26756]) ).
fof(f26773,plain,
( ~ sQ976_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24645,f11359]) ).
fof(f26774,plain,
~ sQ976_spl,
inference(contradiction_clause,[status(thm)],[f26773]) ).
fof(f27807,plain,
( ~ sQ604_spl
| ~ sQ748_spl
| m1_subset_1(sK1084_skl,k1_zfmisc_1(sK1084_skl)) ),
inference(backward_demodulation,[status(thm)],[f25627,f15837]) ).
fof(f27810,plain,
( ~ sQ604_spl
| ~ sQ748_spl
| v1_tex_2(sK1084_skl,k1_zfmisc_1(sK1084_skl)) ),
inference(backward_demodulation,[status(thm)],[f25627,f15840]) ).
fof(f27983,definition,
( sQ1172_spl
<=> l1_struct_0(sK1083_skl) ),
introduced(definition,[new_symbols(definition,[sQ1172_spl])],[split_symbol_definition]) ).
fof(f27985,plain,
( sQ1172_spl
| ~ l1_struct_0(sK1083_skl) ),
inference(component_clause,[status(thm)],[f27983]) ).
fof(f28159,plain,
( sQ1172_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27985,f20718]) ).
fof(f28160,plain,
sQ1172_spl,
inference(contradiction_clause,[status(thm)],[f28159]) ).
fof(f28753,plain,
( ~ sQ868_spl
| $false ),
inference(resolution,[status(thm)],[f26161,f3883]) ).
fof(f28762,plain,
~ sQ868_spl,
inference(contradiction_clause,[status(thm)],[f28753]) ).
fof(f28769,plain,
( ~ sQ604_spl
| ~ sQ748_spl
| ~ v1_tex_2(sK1084_skl,k1_zfmisc_1(sK1084_skl)) ),
inference(resolution,[status(thm)],[f27807,f18921]) ).
fof(f28771,plain,
( ~ sQ604_spl
| ~ sQ748_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f28769,f27810]) ).
fof(f28772,plain,
( ~ sQ604_spl
| ~ sQ748_spl ),
inference(contradiction_clause,[status(thm)],[f28771]) ).
fof(f30326,definition,
( sQ1426_spl
<=> l1_pre_topc(sK970_skl) ),
introduced(definition,[new_symbols(definition,[sQ1426_spl])],[split_symbol_definition]) ).
fof(f30328,plain,
( sQ1426_spl
| ~ l1_pre_topc(sK970_skl) ),
inference(component_clause,[status(thm)],[f30326]) ).
fof(f30351,plain,
( sQ1426_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30328,f14598]) ).
fof(f30352,plain,
sQ1426_spl,
inference(contradiction_clause,[status(thm)],[f30351]) ).
fof(f31535,plain,
m1_subset_1(k2_tops_1(sK1083_skl,sK1084_skl),k1_zfmisc_1(u1_struct_0(sK1083_skl))),
inference(resolution,[status(thm)],[f22926,f15837]) ).
fof(f31546,plain,
( sQ1114_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f31535,f26758]) ).
fof(f31547,plain,
sQ1114_spl,
inference(contradiction_clause,[status(thm)],[f31546]) ).
fof(f32798,plain,
! [X0] :
( k3_tex_4(sK1083_skl,X0) = X0
| ~ v3_pre_topc(X0,sK1083_skl)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl)))
| ~ v2_pre_topc(sK1083_skl)
| v3_struct_0(sK1083_skl) ),
inference(resolution,[status(thm)],[f15102,f15836]) ).
fof(f32829,definition,
! [X0] :
( sQ1735_spl
<=> ( k3_tex_4(sK1083_skl,X0) = X0
| ~ v3_pre_topc(X0,sK1083_skl)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ1735_spl])],[split_symbol_definition]) ).
fof(f32830,plain,
! [X0] :
( ~ sQ1735_spl
| k3_tex_4(sK1083_skl,X0) = X0
| ~ v3_pre_topc(X0,sK1083_skl)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1083_skl))) ),
inference(component_clause,[status(thm)],[f32829]) ).
fof(f32832,plain,
( sQ1735_spl
| ~ sQ427_spl
| sQ440_spl ),
inference(split_clause,[status(thm)],[f32798,f19262,f19143,f32829]) ).
fof(f34988,definition,
( sQ1998_spl
<=> l1_pre_topc(sK1022_skl) ),
introduced(definition,[new_symbols(definition,[sQ1998_spl])],[split_symbol_definition]) ).
fof(f34990,plain,
( sQ1998_spl
| ~ l1_pre_topc(sK1022_skl) ),
inference(component_clause,[status(thm)],[f34988]) ).
fof(f35013,plain,
( sQ1998_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f34990,f15366]) ).
fof(f35014,plain,
sQ1998_spl,
inference(contradiction_clause,[status(thm)],[f35013]) ).
fof(f35492,definition,
( sQ2071_spl
<=> l1_pre_topc(sK1023_skl) ),
introduced(definition,[new_symbols(definition,[sQ2071_spl])],[split_symbol_definition]) ).
fof(f35494,plain,
( sQ2071_spl
| ~ l1_pre_topc(sK1023_skl) ),
inference(component_clause,[status(thm)],[f35492]) ).
fof(f35517,plain,
( sQ2071_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35494,f15372]) ).
fof(f35518,plain,
sQ2071_spl,
inference(contradiction_clause,[status(thm)],[f35517]) ).
fof(f35766,definition,
( sQ2120_spl
<=> l1_pre_topc(sK1024_skl) ),
introduced(definition,[new_symbols(definition,[sQ2120_spl])],[split_symbol_definition]) ).
fof(f35768,plain,
( sQ2120_spl
| ~ l1_pre_topc(sK1024_skl) ),
inference(component_clause,[status(thm)],[f35766]) ).
fof(f35791,plain,
( sQ2120_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35768,f15429]) ).
fof(f35792,plain,
sQ2120_spl,
inference(contradiction_clause,[status(thm)],[f35791]) ).
fof(f36146,definition,
( sQ2171_spl
<=> l1_pre_topc(sK1025_skl) ),
introduced(definition,[new_symbols(definition,[sQ2171_spl])],[split_symbol_definition]) ).
fof(f36148,plain,
( sQ2171_spl
| ~ l1_pre_topc(sK1025_skl) ),
inference(component_clause,[status(thm)],[f36146]) ).
fof(f36171,plain,
( sQ2171_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f36148,f15437]) ).
fof(f36172,plain,
sQ2171_spl,
inference(contradiction_clause,[status(thm)],[f36171]) ).
fof(f37596,plain,
( ~ sQ332_spl
| ~ v2_pre_topc(sK1025_skl) ),
inference(resolution,[status(thm)],[f18010,f15437]) ).
fof(f37609,plain,
( ~ sQ332_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f37596,f15441]) ).
fof(f37610,plain,
~ sQ332_spl,
inference(contradiction_clause,[status(thm)],[f37609]) ).
fof(f37655,plain,
( ~ sQ1735_spl
| k3_tex_4(sK1083_skl,sK1084_skl) = sK1084_skl
| ~ v3_pre_topc(sK1084_skl,sK1083_skl) ),
inference(resolution,[status(thm)],[f32830,f15837]) ).
fof(f37682,definition,
( sQ2324_spl
<=> k3_tex_4(sK1083_skl,sK1084_skl) = sK1084_skl ),
introduced(definition,[new_symbols(definition,[sQ2324_spl])],[split_symbol_definition]) ).
fof(f37683,plain,
( ~ sQ2324_spl
| k3_tex_4(sK1083_skl,sK1084_skl) = sK1084_skl ),
inference(component_clause,[status(thm)],[f37682]) ).
fof(f37685,plain,
( ~ sQ1735_spl
| sQ2324_spl
| ~ sQ341_spl ),
inference(split_clause,[status(thm)],[f37655,f18044,f37682,f32829]) ).
fof(f37694,plain,
( ~ sQ2324_spl
| ~ sQ462_spl
| u1_struct_0(sK1083_skl) = sK1084_skl ),
inference(forward_demodulation,[status(thm)],[f19442,f37683]) ).
fof(f37695,plain,
( ~ sQ2324_spl
| ~ sQ462_spl
| sQ604_spl
| ~ sQ748_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f37694,f22984]) ).
fof(f37696,plain,
( ~ sQ2324_spl
| ~ sQ462_spl
| sQ604_spl
| ~ sQ748_spl ),
inference(contradiction_clause,[status(thm)],[f37695]) ).
fof(f37697,plain,
$false,
inference(sat_refutation,[status(thm)],[f18050,f19174,f19176,f19218,f19271,f19330,f19337,f19444,f19475,f19543,f19579,f19607,f20060,f20080,f20094,f20096,f20210,f20212,f20214,f20216,f20218,f20220,f20367,f20632,f20829,f20913,f20923,f21465,f22349,f23011,f23013,f23015,f24314,f24414,f24546,f24955,f25238,f25908,f25953,f25955,f25957,f26176,f26374,f26562,f26654,f26748,f26774,f28160,f28762,f28772,f30352,f31547,f32832,f35014,f35518,f35792,f36172,f37610,f37685,f37696]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP025+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n018.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 12:42:14 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.34/0.60 % Drodi V4.1.1
% 299.51/38.52 % Refutation found
% 299.51/38.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 299.51/38.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 300.24/38.56
% 300.24/38.56 % SZS status Unknown for theBenchmark.p: SIGTERM
%------------------------------------------------------------------------------