%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : TOP037+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:53:02 AM UTC 2026
% Result : Theorem 12.57s 3.86s
% Output : CNFRefutation 12.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 30
% Syntax : Number of formulae : 226 ( 56 unt; 0 def)
% Number of atoms : 818 ( 103 equ)
% Maximal formula atoms : 33 ( 3 avg)
% Number of connectives : 983 ( 391 ~; 444 |; 104 &)
% ( 3 <=>; 41 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 1 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 4 con; 0-4 aty)
% Number of variables : 312 ( 28 sgn 94 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_pre_topc,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A) )
=> ! [B] :
( m1_pre_topc(B,A)
=> v2_pre_topc(B) ) ),
file('theBenchmark.p',cc1_pre_topc) ).
fof(cc1_relset_1,axiom,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> v1_relat_1(C) ),
file('theBenchmark.p',cc1_relset_1) ).
fof(cc3_tsp_2,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_pre_topc(B,A)
=> ( v2_tsp_2(B,A)
=> ( v1_tex_3(B,A)
& v2_pre_topc(B) ) ) ) ),
file('theBenchmark.p',cc3_tsp_2) ).
fof(dt_k4_tsp_2,axiom,
! [A,B] :
( ( m1_pre_topc(B,A)
& v2_tsp_2(B,A)
& ~ v3_struct_0(B)
& l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ( m2_relset_1(k4_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))
& v5_pre_topc(k4_tsp_2(A,B),A,B)
& v1_funct_2(k4_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(k4_tsp_2(A,B)) ) ),
file('theBenchmark.p',dt_k4_tsp_2) ).
fof(dt_l1_pre_topc,axiom,
! [A] :
( l1_pre_topc(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l1_pre_topc) ).
fof(dt_m1_pre_topc,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m1_pre_topc(B,A)
=> l1_pre_topc(B) ) ),
file('theBenchmark.p',dt_m1_pre_topc) ).
fof(dt_m2_relset_1,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
=> m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
file('theBenchmark.p',dt_m2_relset_1) ).
fof(dt_m2_tsp_1,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m2_tsp_1(B,A)
=> l1_pre_topc(B) ) ),
file('theBenchmark.p',dt_m2_tsp_1) ).
fof(existence_m1_pre_topc,axiom,
! [A] :
( l1_pre_topc(A)
=> ? [B] : m1_pre_topc(B,A) ),
file('theBenchmark.p',existence_m1_pre_topc) ).
fof(existence_m1_subset_1,axiom,
! [A] :
? [B] : m1_subset_1(B,A),
file('theBenchmark.p',existence_m1_subset_1) ).
fof(existence_m2_tsp_1,axiom,
! [A] :
( l1_pre_topc(A)
=> ? [B] : m2_tsp_1(B,A) ),
file('theBenchmark.p',existence_m2_tsp_1) ).
fof(fc1_struct_0,axiom,
! [A] :
( ( l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('theBenchmark.p',fc1_struct_0) ).
fof(rc2_subset_1,axiom,
! [A] :
? [B] :
( v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(A)) ),
file('theBenchmark.p',rc2_subset_1) ).
fof(rc5_struct_0,axiom,
! [A] :
( ( l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ? [B] :
( ~ v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ),
file('theBenchmark.p',rc5_struct_0) ).
fof(rc5_tops_1,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A) )
=> ? [B] :
( v3_tops_1(B,A)
& v2_tops_1(B,A)
& v5_membered(B)
& v4_membered(B)
& v3_membered(B)
& v2_membered(B)
& v1_membered(B)
& v4_pre_topc(B,A)
& v3_pre_topc(B,A)
& v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ),
file('theBenchmark.p',rc5_tops_1) ).
fof(redefinition_k2_funct_2,axiom,
! [A,B,C,D] :
( ( m1_relset_1(C,A,B)
& v1_funct_2(C,A,B)
& v1_funct_1(C) )
=> k2_funct_2(A,B,C,D) = k9_relat_1(C,D) ),
file('theBenchmark.p',redefinition_k2_funct_2) ).
fof(redefinition_k4_pre_topc,axiom,
! [A,B,C,D] :
( ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C)
& l1_struct_0(B)
& l1_struct_0(A) )
=> k4_pre_topc(A,B,C,D) = k9_relat_1(C,D) ),
file('theBenchmark.p',redefinition_k4_pre_topc) ).
fof(redefinition_k5_pre_topc,axiom,
! [A,B,C,D] :
( ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C)
& l1_struct_0(B)
& l1_struct_0(A) )
=> k5_pre_topc(A,B,C,D) = k10_relat_1(C,D) ),
file('theBenchmark.p',redefinition_k5_pre_topc) ).
fof(redefinition_m2_relset_1,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('theBenchmark.p',redefinition_m2_relset_1) ).
fof(redefinition_m2_tsp_1,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m2_tsp_1(B,A)
<=> m1_pre_topc(B,A) ) ),
file('theBenchmark.p',redefinition_m2_tsp_1) ).
fof(t147_funct_1,axiom,
! [A,B] :
( ( v1_funct_1(B)
& v1_relat_1(B) )
=> ( r1_tarski(A,k2_relat_1(B))
=> k9_relat_1(B,k10_relat_1(B,A)) = A ) ),
file('theBenchmark.p',t147_funct_1) ).
fof(t156_relat_1,axiom,
! [A,B,C] :
( v1_relat_1(C)
=> ( r1_tarski(A,B)
=> r1_tarski(k9_relat_1(C,A),k9_relat_1(C,B)) ) ),
file('theBenchmark.p',t156_relat_1) ).
fof(t29_tsp_2,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_tsp_1(B,A)
& v2_tsp_2(B,A)
& ~ v3_struct_0(B) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
=> k5_pre_topc(A,B,k4_tsp_2(A,B),k4_pre_topc(A,B,k4_tsp_2(A,B),C)) = k3_tex_4(A,C) ) ) ),
file('theBenchmark.p',t29_tsp_2) ).
fof(t2_subset,axiom,
! [A,B] :
( m1_subset_1(A,B)
=> ( r2_hidden(A,B)
| v1_xboole_0(B) ) ),
file('theBenchmark.p',t2_subset) ).
fof(t3_subset,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('theBenchmark.p',t3_subset) ).
fof(t45_funct_2,axiom,
! [A,B,C] :
( ( m2_relset_1(C,A,B)
& v1_funct_2(C,A,B)
& v1_funct_1(C) )
=> ( ( B = k1_xboole_0
=> A = k1_xboole_0 )
=> k2_funct_2(A,B,C,A) = k2_relat_1(C) ) ),
file('theBenchmark.p',t45_funct_2) ).
fof(t4_subset,axiom,
! [A,B,C] :
( ( m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) )
=> m1_subset_1(A,C) ),
file('theBenchmark.p',t4_subset) ).
fof(t5_subset,axiom,
! [A,B,C] :
~ ( v1_xboole_0(C)
& m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) ),
file('theBenchmark.p',t5_subset) ).
fof(t6_boole,axiom,
! [A] :
( v1_xboole_0(A)
=> A = k1_xboole_0 ),
file('theBenchmark.p',t6_boole) ).
fof(t30_tsp_2,conjecture,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_tsp_1(B,A)
& v2_tsp_2(B,A)
& ~ v3_struct_0(B) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
=> k4_pre_topc(A,B,k4_tsp_2(A,B),C) = k4_pre_topc(A,B,k4_tsp_2(A,B),k3_tex_4(A,C)) ) ) ),
file('theBenchmark.p',t30_tsp_2) ).
fof(t30_tsp_2_neg,negated_conjecture,
~ ! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_tsp_1(B,A)
& v2_tsp_2(B,A)
& ~ v3_struct_0(B) )
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
=> k4_pre_topc(A,B,k4_tsp_2(A,B),C) = k4_pre_topc(A,B,k4_tsp_2(A,B),k3_tex_4(A,C)) ) ) ),
inference(assume_negation,[status(cth)],[t30_tsp_2]) ).
fof(nnf_110,plain,
? [A] :
( ? [B] :
( ? [C] :
( k4_pre_topc(A,B,k4_tsp_2(A,B),k3_tex_4(A,C)) != k4_pre_topc(A,B,k4_tsp_2(A,B),C)
& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) )
& m2_tsp_1(B,A)
& v2_tsp_2(B,A)
& ~ v3_struct_0(B) )
& l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t30_tsp_2_neg]) ).
fof(sk_t30_tsp_2_neg,plain,
( k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),k3_tex_4(sK1,sK8)) != k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),sK8)
& m1_subset_1(sK8,k1_zfmisc_1(u1_struct_0(sK1)))
& m2_tsp_1(sK0,sK1)
& v2_tsp_2(sK0,sK1)
& ~ v3_struct_0(sK0)
& l1_pre_topc(sK1)
& v2_pre_topc(sK1)
& ~ v3_struct_0(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK0,sK8]),skolemize(A,sK1),skolemize(B,sK0),skolemize(C,sK8)],[nnf_110]) ).
cnf(c_111,negated_conjecture,
v2_tsp_2(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_t30_tsp_2_neg]) ).
cnf(c_112,plain,
( k5_pre_topc(A,B,k4_tsp_2(A,B),k4_pre_topc(A,B,k4_tsp_2(A,B),C)) = k3_tex_4(A,C)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
| ~ m2_tsp_1(B,A)
| ~ v2_tsp_2(B,A)
| v3_struct_0(B)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t29_tsp_2]) ).
cnf(c_114,plain,
( m2_relset_1(k4_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))
| ~ m1_pre_topc(B,A)
| ~ v2_tsp_2(B,A)
| v3_struct_0(B)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k4_tsp_2]) ).
cnf(c_116,plain,
( v1_funct_2(k4_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))
| ~ m1_pre_topc(B,A)
| ~ v2_tsp_2(B,A)
| v3_struct_0(B)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k4_tsp_2]) ).
cnf(c_117,plain,
( v1_funct_1(k4_tsp_2(A,B))
| ~ m1_pre_topc(B,A)
| ~ v2_tsp_2(B,A)
| v3_struct_0(B)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k4_tsp_2]) ).
cnf(c_132,plain,
( v2_pre_topc(B)
| ~ v2_tsp_2(B,A)
| ~ m1_pre_topc(B,A)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[cc3_tsp_2]) ).
cnf(c_154,plain,
( k9_relat_1(A,k10_relat_1(A,B)) = B
| ~ r1_tarski(B,k2_relat_1(A))
| ~ v1_funct_1(A)
| ~ v1_relat_1(A) ),
inference(clausify,[status(thm)],[t147_funct_1]) ).
cnf(c_155,plain,
( v1_relat_1(A)
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,C))) ),
inference(clausify,[status(thm)],[cc1_relset_1]) ).
cnf(c_156,plain,
( r1_tarski(k9_relat_1(A,B),k9_relat_1(A,C))
| ~ r1_tarski(B,C)
| ~ v1_relat_1(A) ),
inference(clausify,[status(thm)],[t156_relat_1]) ).
cnf(c_182,negated_conjecture,
( v1_funct_1(k4_tsp_2(sK1,sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_111,c_117]) ).
cnf(c_184,plain,
( k2_relat_1(A) = k2_funct_2(B,C,A,B)
| k1_xboole_0 = C
| ~ m2_relset_1(A,B,C)
| ~ v1_funct_2(A,B,C)
| ~ v1_funct_1(A) ),
inference(clausify,[status(thm)],[t45_funct_2]) ).
cnf(c_185,plain,
( k10_relat_1(C,D) = k5_pre_topc(A,B,C,D)
| ~ m1_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C)
| ~ l1_struct_0(B)
| ~ l1_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_k5_pre_topc]) ).
cnf(c_186,plain,
( k9_relat_1(C,D) = k4_pre_topc(A,B,C,D)
| ~ m1_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C)
| ~ l1_struct_0(B)
| ~ l1_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_k4_pre_topc]) ).
cnf(c_187,plain,
( k9_relat_1(A,D) = k2_funct_2(B,C,A,D)
| ~ m1_relset_1(A,B,C)
| ~ v1_funct_2(A,B,C)
| ~ v1_funct_1(A) ),
inference(clausify,[status(thm)],[redefinition_k2_funct_2]) ).
cnf(c_192,plain,
( ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(C,D)))
| k9_relat_1(A,k10_relat_1(A,B)) = B
| ~ r1_tarski(B,k2_relat_1(A))
| ~ v1_funct_1(A) ),
inference(resolve,[status(thm)],[c_154,c_155]) ).
cnf(c_262,plain,
( v2_pre_topc(B)
| ~ m1_pre_topc(B,A)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A) ),
inference(clausify,[status(thm)],[cc1_pre_topc]) ).
cnf(c_275,plain,
( l1_struct_0(A)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[dt_l1_pre_topc]) ).
cnf(c_276,plain,
( l1_pre_topc(B)
| ~ m1_pre_topc(B,A)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[dt_m1_pre_topc]) ).
cnf(c_277,plain,
( m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,C)))
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[dt_m2_relset_1]) ).
cnf(c_278,plain,
( l1_pre_topc(B)
| ~ m2_tsp_1(B,A)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[dt_m2_tsp_1]) ).
fof(nnf_70,plain,
! [A] :
( ? [B] : m1_pre_topc(B,A)
| ~ l1_pre_topc(A) ),
inference(fof_nnf,[status(thm)],[existence_m1_pre_topc]) ).
fof(sk_existence_m1_pre_topc,plain,
! [A] :
( m1_pre_topc(sK2(A),A)
| ~ l1_pre_topc(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(B,sK2(A))],[nnf_70]) ).
cnf(c_281,plain,
( m1_pre_topc(sK2(A),A)
| ~ l1_pre_topc(A) ),
inference(split_conjunct,[status(thm)],[sk_existence_m1_pre_topc]) ).
fof(nnf_72,plain,
! [A] :
? [B] : m1_subset_1(B,A),
inference(fof_nnf,[status(thm)],[existence_m1_subset_1]) ).
fof(sk_existence_m1_subset_1,plain,
! [A] : m1_subset_1(sK3(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(B,sK3(A))],[nnf_72]) ).
cnf(c_283,plain,
m1_subset_1(sK3(A),A),
inference(split_conjunct,[status(thm)],[sk_existence_m1_subset_1]) ).
fof(nnf_74,plain,
! [A] :
( ? [B] : m2_tsp_1(B,A)
| ~ l1_pre_topc(A) ),
inference(fof_nnf,[status(thm)],[existence_m2_tsp_1]) ).
fof(sk_existence_m2_tsp_1,plain,
! [A] :
( m2_tsp_1(sK4(A),A)
| ~ l1_pre_topc(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(B,sK4(A))],[nnf_74]) ).
cnf(c_285,plain,
( m2_tsp_1(sK4(A),A)
| ~ l1_pre_topc(A) ),
inference(split_conjunct,[status(thm)],[sk_existence_m2_tsp_1]) ).
cnf(c_286,plain,
( ~ v1_xboole_0(u1_struct_0(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_struct_0]) ).
fof(nnf_82,plain,
! [A] :
? [B] :
( v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(A)) ),
inference(fof_nnf,[status(thm)],[rc2_subset_1]) ).
fof(sk_rc2_subset_1,plain,
! [A] :
( v1_xboole_0(sK5(A))
& m1_subset_1(sK5(A),k1_zfmisc_1(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(B,sK5(A))],[nnf_82]) ).
cnf(c_304,plain,
m1_subset_1(sK5(A),k1_zfmisc_1(A)),
inference(split_conjunct,[status(thm)],[sk_rc2_subset_1]) ).
cnf(c_305,plain,
v1_xboole_0(sK5(A)),
inference(split_conjunct,[status(thm)],[sk_rc2_subset_1]) ).
fof(nnf_87,plain,
! [A] :
( ? [B] :
( ~ v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[rc5_struct_0]) ).
fof(sk_rc5_struct_0_sk,plain,
! [A] :
( ( ~ v1_xboole_0(sK6(A))
& m1_subset_1(sK6(A),k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(B,sK6(A))],[nnf_87]) ).
fof(sk_rc5_struct_0,plain,
( ! [VAR_0] :
( ~ v1_xboole_0(sK6(VAR_0))
| ~ l1_struct_0(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0] :
( m1_subset_1(sK6(VAR_0),k1_zfmisc_1(u1_struct_0(VAR_0)))
| ~ l1_struct_0(VAR_0)
| v3_struct_0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_rc5_struct_0_sk]) ).
cnf(c_319,plain,
( m1_subset_1(sK6(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_rc5_struct_0]) ).
cnf(c_320,plain,
( ~ v1_xboole_0(sK6(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_rc5_struct_0]) ).
fof(nnf_88,plain,
! [A] :
( ? [B] :
( v3_tops_1(B,A)
& v2_tops_1(B,A)
& v5_membered(B)
& v4_membered(B)
& v3_membered(B)
& v2_membered(B)
& v1_membered(B)
& v4_pre_topc(B,A)
& v3_pre_topc(B,A)
& v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A) ),
inference(fof_nnf,[status(thm)],[rc5_tops_1]) ).
fof(sk_rc5_tops_1_sk,plain,
! [A] :
( ( v3_tops_1(sK7(A),A)
& v2_tops_1(sK7(A),A)
& v5_membered(sK7(A))
& v4_membered(sK7(A))
& v3_membered(sK7(A))
& v2_membered(sK7(A))
& v1_membered(sK7(A))
& v4_pre_topc(sK7(A),A)
& v3_pre_topc(sK7(A),A)
& v1_xboole_0(sK7(A))
& m1_subset_1(sK7(A),k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(B,sK7(A))],[nnf_88]) ).
fof(sk_rc5_tops_1,plain,
( ! [VAR_0] :
( v3_tops_1(sK7(VAR_0),VAR_0)
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v2_tops_1(sK7(VAR_0),VAR_0)
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v5_membered(sK7(VAR_0))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v4_membered(sK7(VAR_0))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v3_membered(sK7(VAR_0))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v2_membered(sK7(VAR_0))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v1_membered(sK7(VAR_0))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v4_pre_topc(sK7(VAR_0),VAR_0)
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v3_pre_topc(sK7(VAR_0),VAR_0)
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( v1_xboole_0(sK7(VAR_0))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) )
& ! [VAR_0] :
( m1_subset_1(sK7(VAR_0),k1_zfmisc_1(u1_struct_0(VAR_0)))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_rc5_tops_1_sk]) ).
cnf(c_322,plain,
( v1_xboole_0(sK7(A))
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A) ),
inference(split_conjunct,[status(thm)],[sk_rc5_tops_1]) ).
cnf(c_333,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_335,plain,
( m1_pre_topc(B,A)
| ~ m2_tsp_1(B,A)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[redefinition_m2_tsp_1]) ).
cnf(c_339,plain,
( r2_hidden(A,B)
| v1_xboole_0(B)
| ~ m1_subset_1(A,B) ),
inference(clausify,[status(thm)],[t2_subset]) ).
cnf(c_340,plain,
( r1_tarski(A,B)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[t3_subset]) ).
cnf(c_342,plain,
( m1_subset_1(A,C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(clausify,[status(thm)],[t4_subset]) ).
cnf(c_343,plain,
( ~ v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(clausify,[status(thm)],[t5_subset]) ).
cnf(c_344,plain,
( k1_xboole_0 = A
| ~ v1_xboole_0(A) ),
inference(clausify,[status(thm)],[t6_boole]) ).
cnf(c_347,negated_conjecture,
~ v3_struct_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t30_tsp_2_neg]) ).
cnf(c_348,negated_conjecture,
v2_pre_topc(sK1),
inference(split_conjunct,[status(thm)],[sk_t30_tsp_2_neg]) ).
cnf(c_349,negated_conjecture,
l1_pre_topc(sK1),
inference(split_conjunct,[status(thm)],[sk_t30_tsp_2_neg]) ).
cnf(c_350,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t30_tsp_2_neg]) ).
cnf(c_351,negated_conjecture,
m2_tsp_1(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_t30_tsp_2_neg]) ).
cnf(c_352,negated_conjecture,
m1_subset_1(sK8,k1_zfmisc_1(u1_struct_0(sK1))),
inference(split_conjunct,[status(thm)],[sk_t30_tsp_2_neg]) ).
cnf(c_353,negated_conjecture,
k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),k3_tex_4(sK1,sK8)) != k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),sK8),
inference(split_conjunct,[status(thm)],[sk_t30_tsp_2_neg]) ).
cnf(c_354,negated_conjecture,
( k5_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A)) = k3_tex_4(sK1,A)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_111,c_112]) ).
cnf(c_7763,negated_conjecture,
( k5_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A)) = k3_tex_4(sK1,A)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_347,c_354]) ).
cnf(c_7764,negated_conjecture,
( k5_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A)) = k3_tex_4(sK1,A)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_348,c_7763]) ).
cnf(c_7765,negated_conjecture,
( k5_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A)) = k3_tex_4(sK1,A)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_349,c_7764]) ).
cnf(c_7766,negated_conjecture,
( k5_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A)) = k3_tex_4(sK1,A)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_tsp_1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_350,c_7765]) ).
cnf(c_355,negated_conjecture,
( k5_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A)) = k3_tex_4(sK1,A)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(resolve,[status(thm)],[c_351,c_7766]) ).
cnf(c_358,negated_conjecture,
( m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_111,c_114]) ).
cnf(c_7767,negated_conjecture,
( m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_347,c_358]) ).
cnf(c_7768,negated_conjecture,
( m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_348,c_7767]) ).
cnf(c_7769,negated_conjecture,
( m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_349,c_7768]) ).
cnf(c_359,negated_conjecture,
( m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_350,c_7769]) ).
cnf(c_360,negated_conjecture,
( v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_111,c_116]) ).
cnf(c_7770,negated_conjecture,
( v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_347,c_360]) ).
cnf(c_7771,negated_conjecture,
( v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_348,c_7770]) ).
cnf(c_7772,negated_conjecture,
( v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_349,c_7771]) ).
cnf(c_361,negated_conjecture,
( v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_350,c_7772]) ).
cnf(c_376,negated_conjecture,
( v2_pre_topc(sK0)
| ~ m1_pre_topc(sK0,sK1)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_111,c_132]) ).
cnf(c_7773,negated_conjecture,
( v2_pre_topc(sK0)
| ~ m1_pre_topc(sK0,sK1)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_347,c_376]) ).
cnf(c_7774,negated_conjecture,
( v2_pre_topc(sK0)
| ~ m1_pre_topc(sK0,sK1)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_348,c_7773]) ).
cnf(c_377,negated_conjecture,
( v2_pre_topc(sK0)
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_349,c_7774]) ).
cnf(c_380,plain,
( ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(D,E)))
| r1_tarski(k9_relat_1(C,A),k9_relat_1(C,B))
| ~ r1_tarski(A,B) ),
inference(resolve,[status(thm)],[c_156,c_155]) ).
cnf(c_392,negated_conjecture,
( k2_relat_1(k4_tsp_2(sK1,sK0)) = k2_funct_2(A,B,k4_tsp_2(sK1,sK0),A)
| k1_xboole_0 = B
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),A,B)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),A,B)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_182,c_184]) ).
cnf(c_7775,negated_conjecture,
( k2_funct_2(A,B,k4_tsp_2(sK1,sK0),A) = k2_relat_1(k4_tsp_2(sK1,sK0))
| k1_xboole_0 = B
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),A,B)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),A,B)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_392]) ).
cnf(c_7776,negated_conjecture,
( k2_funct_2(A,B,k4_tsp_2(sK1,sK0),A) = k2_relat_1(k4_tsp_2(sK1,sK0))
| k1_xboole_0 = B
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),A,B)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),A,B)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_347,c_7775]) ).
cnf(c_7777,negated_conjecture,
( k2_funct_2(A,B,k4_tsp_2(sK1,sK0),A) = k2_relat_1(k4_tsp_2(sK1,sK0))
| k1_xboole_0 = B
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),A,B)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),A,B)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_348,c_7776]) ).
cnf(c_7778,negated_conjecture,
( k2_funct_2(A,B,k4_tsp_2(sK1,sK0),A) = k2_relat_1(k4_tsp_2(sK1,sK0))
| k1_xboole_0 = B
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),A,B)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),A,B)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_349,c_7777]) ).
cnf(c_393,negated_conjecture,
( k2_funct_2(A,B,k4_tsp_2(sK1,sK0),A) = k2_relat_1(k4_tsp_2(sK1,sK0))
| k1_xboole_0 = B
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),A,B)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),A,B)
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_350,c_7778]) ).
cnf(c_394,negated_conjecture,
( k10_relat_1(k4_tsp_2(sK1,sK0),C) = k5_pre_topc(A,B,k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_182,c_185]) ).
cnf(c_7779,negated_conjecture,
( k5_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k10_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_394]) ).
cnf(c_7780,negated_conjecture,
( k5_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k10_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_347,c_7779]) ).
cnf(c_7781,negated_conjecture,
( k5_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k10_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_348,c_7780]) ).
cnf(c_7782,negated_conjecture,
( k5_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k10_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_349,c_7781]) ).
cnf(c_395,negated_conjecture,
( k5_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k10_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_350,c_7782]) ).
cnf(c_396,negated_conjecture,
( k9_relat_1(k4_tsp_2(sK1,sK0),C) = k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_182,c_186]) ).
cnf(c_7783,negated_conjecture,
( k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_396]) ).
cnf(c_7784,negated_conjecture,
( k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_347,c_7783]) ).
cnf(c_7785,negated_conjecture,
( k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_348,c_7784]) ).
cnf(c_7786,negated_conjecture,
( k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_349,c_7785]) ).
cnf(c_397,negated_conjecture,
( k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A)
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_350,c_7786]) ).
cnf(c_398,negated_conjecture,
( k9_relat_1(k4_tsp_2(sK1,sK0),C) = k2_funct_2(A,B,k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),A,B)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),A,B)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_182,c_187]) ).
cnf(c_7787,negated_conjecture,
( k2_funct_2(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),A,B)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),A,B)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_398]) ).
cnf(c_7788,negated_conjecture,
( k2_funct_2(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),A,B)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),A,B)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_347,c_7787]) ).
cnf(c_7789,negated_conjecture,
( k2_funct_2(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),A,B)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),A,B)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_348,c_7788]) ).
cnf(c_7790,negated_conjecture,
( k2_funct_2(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),A,B)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),A,B)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_349,c_7789]) ).
cnf(c_399,negated_conjecture,
( k2_funct_2(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),A,B)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),A,B)
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_350,c_7790]) ).
cnf(c_424,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1)
| ~ m1_subset_1(k4_tsp_2(sK1,sK0),k1_zfmisc_1(k2_zfmisc_1(B,C)))
| k9_relat_1(k4_tsp_2(sK1,sK0),k10_relat_1(k4_tsp_2(sK1,sK0),A)) = A
| ~ r1_tarski(A,k2_relat_1(k4_tsp_2(sK1,sK0))) ),
inference(resolve,[status(thm)],[c_192,c_182]) ).
cnf(c_7791,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| ~ m1_subset_1(k4_tsp_2(sK1,sK0),k1_zfmisc_1(k2_zfmisc_1(B,C)))
| k9_relat_1(k4_tsp_2(sK1,sK0),k10_relat_1(k4_tsp_2(sK1,sK0),A)) = A
| ~ r1_tarski(A,k2_relat_1(k4_tsp_2(sK1,sK0))) ),
inference(resolve,[status(thm)],[c_347,c_424]) ).
cnf(c_7792,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ m1_subset_1(k4_tsp_2(sK1,sK0),k1_zfmisc_1(k2_zfmisc_1(B,C)))
| k9_relat_1(k4_tsp_2(sK1,sK0),k10_relat_1(k4_tsp_2(sK1,sK0),A)) = A
| ~ r1_tarski(A,k2_relat_1(k4_tsp_2(sK1,sK0))) ),
inference(resolve,[status(thm)],[c_348,c_7791]) ).
cnf(c_7793,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ m1_subset_1(k4_tsp_2(sK1,sK0),k1_zfmisc_1(k2_zfmisc_1(B,C)))
| k9_relat_1(k4_tsp_2(sK1,sK0),k10_relat_1(k4_tsp_2(sK1,sK0),A)) = A
| ~ r1_tarski(A,k2_relat_1(k4_tsp_2(sK1,sK0))) ),
inference(resolve,[status(thm)],[c_349,c_7792]) ).
cnf(c_425,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| ~ m1_subset_1(k4_tsp_2(sK1,sK0),k1_zfmisc_1(k2_zfmisc_1(B,C)))
| k9_relat_1(k4_tsp_2(sK1,sK0),k10_relat_1(k4_tsp_2(sK1,sK0),A)) = A
| ~ r1_tarski(A,k2_relat_1(k4_tsp_2(sK1,sK0))) ),
inference(resolve,[status(thm)],[c_350,c_7793]) ).
cnf(c_544,plain,
( r2_hidden(sK3(A),A)
| v1_xboole_0(A) ),
inference(resolve,[status(thm)],[c_339,c_283]) ).
cnf(c_7794,plain,
k1_xboole_0 = sK5(A),
inference(resolve,[status(thm)],[c_344,c_305]) ).
cnf(c_549,plain,
sK5(A) = k1_xboole_0,
inference(copy,[status(thm)],[c_7794]) ).
cnf(c_557,plain,
m1_subset_1(k1_xboole_0,k1_zfmisc_1(A)),
inference(paramod,[status(thm)],[c_549,c_304]) ).
cnf(c_582,plain,
l1_struct_0(sK1),
inference(resolve,[status(thm)],[c_349,c_275]) ).
cnf(c_7795,negated_conjecture,
( m1_pre_topc(sK0,sK1)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_351,c_335]) ).
cnf(c_585,negated_conjecture,
m1_pre_topc(sK0,sK1),
inference(resolve,[status(thm)],[c_349,c_7795]) ).
cnf(c_7796,negated_conjecture,
( l1_pre_topc(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_351,c_278]) ).
cnf(c_586,negated_conjecture,
l1_pre_topc(sK0),
inference(resolve,[status(thm)],[c_349,c_7796]) ).
cnf(c_595,negated_conjecture,
( ~ m1_subset_1(k4_tsp_2(sK1,sK0),k1_zfmisc_1(k2_zfmisc_1(B,C)))
| k9_relat_1(k4_tsp_2(sK1,sK0),k10_relat_1(k4_tsp_2(sK1,sK0),A)) = A
| ~ r1_tarski(A,k2_relat_1(k4_tsp_2(sK1,sK0))) ),
inference(resolve,[status(thm)],[c_585,c_425]) ).
cnf(c_608,negated_conjecture,
( k2_funct_2(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),A,B)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),A,B) ),
inference(resolve,[status(thm)],[c_585,c_399]) ).
cnf(c_609,negated_conjecture,
( k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k9_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A) ),
inference(resolve,[status(thm)],[c_585,c_397]) ).
cnf(c_610,negated_conjecture,
( k5_pre_topc(A,B,k4_tsp_2(sK1,sK0),C) = k10_relat_1(k4_tsp_2(sK1,sK0),C)
| ~ m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(A),u1_struct_0(B))
| ~ l1_struct_0(B)
| ~ l1_struct_0(A) ),
inference(resolve,[status(thm)],[c_585,c_395]) ).
cnf(c_611,negated_conjecture,
( k2_funct_2(A,B,k4_tsp_2(sK1,sK0),A) = k2_relat_1(k4_tsp_2(sK1,sK0))
| k1_xboole_0 = B
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),A,B)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),A,B) ),
inference(resolve,[status(thm)],[c_585,c_393]) ).
cnf(c_614,negated_conjecture,
v2_pre_topc(sK0),
inference(resolve,[status(thm)],[c_585,c_377]) ).
cnf(c_619,negated_conjecture,
v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_585,c_361]) ).
cnf(c_620,negated_conjecture,
m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_585,c_359]) ).
cnf(c_622,plain,
r1_tarski(sK8,u1_struct_0(sK1)),
inference(resolve,[status(thm)],[c_352,c_340]) ).
cnf(c_642,plain,
k5_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),sK8)) = k3_tex_4(sK1,sK8),
inference(resolve,[status(thm)],[c_355,c_352]) ).
cnf(c_661,plain,
m2_tsp_1(sK4(sK0),sK0),
inference(resolve,[status(thm)],[c_586,c_285]) ).
cnf(c_663,plain,
l1_struct_0(sK0),
inference(resolve,[status(thm)],[c_586,c_275]) ).
cnf(c_7797,plain,
( ~ v1_xboole_0(sK6(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_663,c_320]) ).
cnf(c_680,negated_conjecture,
~ v1_xboole_0(sK6(sK0)),
inference(resolve,[status(thm)],[c_350,c_7797]) ).
cnf(c_7798,plain,
( m1_subset_1(sK6(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_663,c_319]) ).
cnf(c_681,negated_conjecture,
m1_subset_1(sK6(sK0),k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_350,c_7798]) ).
cnf(c_7799,plain,
( ~ v1_xboole_0(u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_663,c_286]) ).
cnf(c_682,negated_conjecture,
~ v1_xboole_0(u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_350,c_7799]) ).
cnf(c_859,plain,
( ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,C)))
| r1_tarski(k9_relat_1(A,sK8),k9_relat_1(A,u1_struct_0(sK1))) ),
inference(resolve,[status(thm)],[c_622,c_380]) ).
cnf(c_7800,plain,
( m1_pre_topc(sK4(sK0),sK0)
| ~ l1_pre_topc(sK0) ),
inference(resolve,[status(thm)],[c_661,c_335]) ).
cnf(c_864,plain,
m1_pre_topc(sK4(sK0),sK0),
inference(resolve,[status(thm)],[c_586,c_7800]) ).
cnf(c_7801,plain,
( l1_pre_topc(sK4(sK0))
| ~ l1_pre_topc(sK0) ),
inference(resolve,[status(thm)],[c_661,c_278]) ).
cnf(c_865,plain,
l1_pre_topc(sK4(sK0)),
inference(resolve,[status(thm)],[c_586,c_7801]) ).
cnf(c_877,plain,
m1_pre_topc(sK2(sK4(sK0)),sK4(sK0)),
inference(resolve,[status(thm)],[c_865,c_281]) ).
cnf(c_7802,plain,
( v2_pre_topc(sK4(sK0))
| ~ l1_pre_topc(sK0)
| ~ v2_pre_topc(sK0) ),
inference(resolve,[status(thm)],[c_864,c_262]) ).
cnf(c_7803,negated_conjecture,
( v2_pre_topc(sK4(sK0))
| ~ l1_pre_topc(sK0) ),
inference(resolve,[status(thm)],[c_614,c_7802]) ).
cnf(c_946,negated_conjecture,
v2_pre_topc(sK4(sK0)),
inference(resolve,[status(thm)],[c_586,c_7803]) ).
cnf(c_1042,plain,
m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_620,c_333]) ).
cnf(c_1043,plain,
m1_subset_1(k4_tsp_2(sK1,sK0),k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK0)))),
inference(resolve,[status(thm)],[c_620,c_277]) ).
cnf(c_7804,negated_conjecture,
( k2_funct_2(u1_struct_0(sK1),u1_struct_0(sK0),k4_tsp_2(sK1,sK0),A) = k9_relat_1(k4_tsp_2(sK1,sK0),A)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_608,c_1042]) ).
cnf(c_1343,negated_conjecture,
k2_funct_2(u1_struct_0(sK1),u1_struct_0(sK0),k4_tsp_2(sK1,sK0),A) = k9_relat_1(k4_tsp_2(sK1,sK0),A),
inference(resolve,[status(thm)],[c_619,c_7804]) ).
cnf(c_7805,negated_conjecture,
( k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A) = k9_relat_1(k4_tsp_2(sK1,sK0),A)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ l1_struct_0(sK0)
| ~ l1_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_609,c_1042]) ).
cnf(c_7806,negated_conjecture,
( k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A) = k9_relat_1(k4_tsp_2(sK1,sK0),A)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ l1_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_582,c_7805]) ).
cnf(c_7807,negated_conjecture,
( k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A) = k9_relat_1(k4_tsp_2(sK1,sK0),A)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_663,c_7806]) ).
cnf(c_1345,negated_conjecture,
k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A) = k9_relat_1(k4_tsp_2(sK1,sK0),A),
inference(resolve,[status(thm)],[c_619,c_7807]) ).
cnf(c_1356,plain,
k5_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),k9_relat_1(k4_tsp_2(sK1,sK0),sK8)) = k3_tex_4(sK1,sK8),
inference(paramod,[status(thm)],[c_1345,c_642]) ).
cnf(c_7808,negated_conjecture,
k9_relat_1(k4_tsp_2(sK1,sK0),k3_tex_4(sK1,sK8)) != k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),sK8),
inference(paramod,[status(thm)],[c_1345,c_353]) ).
cnf(c_1358,negated_conjecture,
k9_relat_1(k4_tsp_2(sK1,sK0),k3_tex_4(sK1,sK8)) != k9_relat_1(k4_tsp_2(sK1,sK0),sK8),
inference(paramod,[status(thm)],[c_1345,c_7808]) ).
cnf(c_7809,negated_conjecture,
( k5_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A) = k10_relat_1(k4_tsp_2(sK1,sK0),A)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ l1_struct_0(sK0)
| ~ l1_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_610,c_1042]) ).
cnf(c_7810,negated_conjecture,
( k5_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A) = k10_relat_1(k4_tsp_2(sK1,sK0),A)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ l1_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_582,c_7809]) ).
cnf(c_7811,negated_conjecture,
( k5_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A) = k10_relat_1(k4_tsp_2(sK1,sK0),A)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_663,c_7810]) ).
cnf(c_1365,negated_conjecture,
k5_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A) = k10_relat_1(k4_tsp_2(sK1,sK0),A),
inference(resolve,[status(thm)],[c_619,c_7811]) ).
cnf(c_1367,plain,
k10_relat_1(k4_tsp_2(sK1,sK0),k9_relat_1(k4_tsp_2(sK1,sK0),sK8)) = k3_tex_4(sK1,sK8),
inference(paramod,[status(thm)],[c_1365,c_1356]) ).
cnf(c_7812,negated_conjecture,
( k2_funct_2(u1_struct_0(sK1),u1_struct_0(sK0),k4_tsp_2(sK1,sK0),u1_struct_0(sK1)) = k2_relat_1(k4_tsp_2(sK1,sK0))
| k1_xboole_0 = u1_struct_0(sK0)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_611,c_620]) ).
cnf(c_7813,negated_conjecture,
( k9_relat_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1)) = k2_relat_1(k4_tsp_2(sK1,sK0))
| k1_xboole_0 = u1_struct_0(sK0)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(paramod,[status(thm)],[c_1343,c_7812]) ).
cnf(c_7814,negated_conjecture,
( k9_relat_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1)) = k2_relat_1(k4_tsp_2(sK1,sK0))
| u1_struct_0(sK0) = k1_xboole_0
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(copy,[status(thm)],[c_7813]) ).
cnf(c_1386,negated_conjecture,
( k9_relat_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1)) = k2_relat_1(k4_tsp_2(sK1,sK0))
| u1_struct_0(sK0) = k1_xboole_0 ),
inference(resolve,[status(thm)],[c_619,c_7814]) ).
cnf(c_7815,plain,
( v1_xboole_0(A)
| m1_subset_1(sK3(A),B)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(resolve,[status(thm)],[c_342,c_544]) ).
cnf(c_7816,plain,
( v1_xboole_0(sK6(sK0))
| m1_subset_1(sK3(sK6(sK0)),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_7815,c_681]) ).
cnf(c_1677,plain,
m1_subset_1(sK3(sK6(sK0)),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_680,c_7816]) ).
cnf(c_7817,plain,
( l1_pre_topc(sK2(sK4(sK0)))
| ~ l1_pre_topc(sK4(sK0)) ),
inference(resolve,[status(thm)],[c_877,c_276]) ).
cnf(c_1987,plain,
l1_pre_topc(sK2(sK4(sK0))),
inference(resolve,[status(thm)],[c_865,c_7817]) ).
cnf(c_7818,plain,
( v2_pre_topc(sK2(sK4(sK0)))
| ~ l1_pre_topc(sK4(sK0))
| ~ v2_pre_topc(sK4(sK0)) ),
inference(resolve,[status(thm)],[c_877,c_262]) ).
cnf(c_7819,plain,
( v2_pre_topc(sK2(sK4(sK0)))
| ~ l1_pre_topc(sK4(sK0)) ),
inference(resolve,[status(thm)],[c_946,c_7818]) ).
cnf(c_1988,plain,
v2_pre_topc(sK2(sK4(sK0))),
inference(resolve,[status(thm)],[c_865,c_7819]) ).
cnf(c_2003,plain,
m2_tsp_1(sK4(sK2(sK4(sK0))),sK2(sK4(sK0))),
inference(resolve,[status(thm)],[c_1987,c_285]) ).
cnf(c_7820,plain,
( r2_hidden(sK3(sK6(sK0)),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1677,c_339]) ).
cnf(c_2121,plain,
r2_hidden(sK3(sK6(sK0)),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_682,c_7820]) ).
cnf(c_2209,plain,
( ~ v1_xboole_0(A)
| ~ m1_subset_1(u1_struct_0(sK0),k1_zfmisc_1(A)) ),
inference(resolve,[status(thm)],[c_2121,c_343]) ).
cnf(c_4584,plain,
r1_tarski(k9_relat_1(k4_tsp_2(sK1,sK0),sK8),k9_relat_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1))),
inference(resolve,[status(thm)],[c_1043,c_859]) ).
cnf(c_7821,plain,
( m1_pre_topc(sK4(sK2(sK4(sK0))),sK2(sK4(sK0)))
| ~ l1_pre_topc(sK2(sK4(sK0))) ),
inference(resolve,[status(thm)],[c_2003,c_335]) ).
cnf(c_6255,plain,
m1_pre_topc(sK4(sK2(sK4(sK0))),sK2(sK4(sK0))),
inference(resolve,[status(thm)],[c_1987,c_7821]) ).
cnf(c_7822,plain,
( l1_pre_topc(sK4(sK2(sK4(sK0))))
| ~ l1_pre_topc(sK2(sK4(sK0))) ),
inference(resolve,[status(thm)],[c_2003,c_278]) ).
cnf(c_6256,plain,
l1_pre_topc(sK4(sK2(sK4(sK0)))),
inference(resolve,[status(thm)],[c_1987,c_7822]) ).
cnf(c_6396,plain,
( r1_tarski(k9_relat_1(k4_tsp_2(sK1,sK0),sK8),k2_relat_1(k4_tsp_2(sK1,sK0)))
| u1_struct_0(sK0) = k1_xboole_0 ),
inference(paramod,[status(thm)],[c_1386,c_4584]) ).
cnf(c_7823,plain,
( v2_pre_topc(sK4(sK2(sK4(sK0))))
| ~ l1_pre_topc(sK2(sK4(sK0)))
| ~ v2_pre_topc(sK2(sK4(sK0))) ),
inference(resolve,[status(thm)],[c_6255,c_262]) ).
cnf(c_7824,plain,
( v2_pre_topc(sK4(sK2(sK4(sK0))))
| ~ l1_pre_topc(sK2(sK4(sK0))) ),
inference(resolve,[status(thm)],[c_1988,c_7823]) ).
cnf(c_6781,plain,
v2_pre_topc(sK4(sK2(sK4(sK0)))),
inference(resolve,[status(thm)],[c_1987,c_7824]) ).
cnf(c_7825,plain,
( v1_xboole_0(sK7(sK4(sK2(sK4(sK0)))))
| ~ l1_pre_topc(sK4(sK2(sK4(sK0)))) ),
inference(resolve,[status(thm)],[c_6781,c_322]) ).
cnf(c_6795,plain,
v1_xboole_0(sK7(sK4(sK2(sK4(sK0))))),
inference(resolve,[status(thm)],[c_6256,c_7825]) ).
cnf(c_7826,negated_conjecture,
( u1_struct_0(sK0) = k1_xboole_0
| ~ m1_subset_1(k4_tsp_2(sK1,sK0),k1_zfmisc_1(k2_zfmisc_1(A,B)))
| k9_relat_1(k4_tsp_2(sK1,sK0),k10_relat_1(k4_tsp_2(sK1,sK0),k9_relat_1(k4_tsp_2(sK1,sK0),sK8))) = k9_relat_1(k4_tsp_2(sK1,sK0),sK8) ),
inference(resolve,[status(thm)],[c_595,c_6396]) ).
cnf(c_7827,negated_conjecture,
( u1_struct_0(sK0) = k1_xboole_0
| k9_relat_1(k4_tsp_2(sK1,sK0),k10_relat_1(k4_tsp_2(sK1,sK0),k9_relat_1(k4_tsp_2(sK1,sK0),sK8))) = k9_relat_1(k4_tsp_2(sK1,sK0),sK8) ),
inference(resolve,[status(thm)],[c_7826,c_1043]) ).
cnf(c_7828,negated_conjecture,
( u1_struct_0(sK0) = k1_xboole_0
| k9_relat_1(k4_tsp_2(sK1,sK0),k3_tex_4(sK1,sK8)) = k9_relat_1(k4_tsp_2(sK1,sK0),sK8) ),
inference(paramod,[status(thm)],[c_1367,c_7827]) ).
cnf(c_7119,negated_conjecture,
u1_struct_0(sK0) = k1_xboole_0,
inference(resolve,[status(thm)],[c_1358,c_7828]) ).
cnf(c_7829,plain,
( ~ v1_xboole_0(A)
| ~ m1_subset_1(k1_xboole_0,k1_zfmisc_1(A)) ),
inference(paramod,[status(thm)],[c_7119,c_2209]) ).
cnf(c_7761,plain,
~ v1_xboole_0(A),
inference(resolve,[status(thm)],[c_557,c_7829]) ).
cnf(c_7762,plain,
$false,
inference(resolve,[status(thm)],[c_7761,c_6795]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : TOP037+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.42 % Computer : n003.cluster.edu
% 0.11/0.42 % Model : x86_64 x86_64
% 0.11/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.42 % Memory : 8046.5625MB
% 0.11/0.42 % OS : Linux 6.8.0-71-generic
% 0.11/0.42 % CPULimit : 300
% 0.11/0.42 % WCLimit : 300
% 0.11/0.42 % DateTime : Sat Sep 26 20:42:25 UTC 2026
% 0.11/0.43 % CPUTime :
% 0.11/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.44 % Process 3727008 was started by sandbox on n003,
% 0.11/0.44 % Sat Sep 26 20:42:25 2026
% 0.11/0.44 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.11/0.45
% 0.11/0.45 % From the command line: assign(max_seconds, 300).
% 12.57/3.86
% 12.57/3.86 % given #500 (T,wt=16): 1305 -v2_membered(u1_struct_0(c5)) | v1_membered(f7(c5)). [resolve(571,a,252,b)].
% 12.57/3.86
% 12.57/3.86 % given #1000 (T,wt=22): 2720 r1_tarski(f14(f1(c5)),u1_struct_0(f1(c5))). [resolve(843,a,340,a)].
% 12.57/3.86
% 12.57/3.86 % given #1500 (T,wt=23): 3689 -v3_membered(u1_struct_0(f5(c6))) | v3_membered(f14(f5(c6))). [resolve(950,a,256,b)].
% 12.57/3.86
% 12.57/3.86 % given #2000 (T,wt=26): 2836 -v1_xboole_0(k3_tex_4(c5,f7(c5))) | v2_tops_1(k3_tex_4(c5,f7(c5)),c5). [resolve(1289,a,269,b),unit_del(a,349)].
% 12.57/3.86
% 12.57/3.86 % given #2500 (F,wt=28): 6574 -r2_hidden(k1_zfmisc_1(u1_struct_0(f5(c6))),f9(f5(c6))). [resolve(3726,a,243,b)].
% 12.57/3.86
% 12.57/3.86 % SZS status Theorem for theBenchmark
% 12.57/3.86
% 12.57/3.86 % Proof 1 at 1.31 (+ 0.27) seconds.
% 12.57/3.86 % Length of proof is 142.
% 12.57/3.86 % Level of proof is 11.
% 12.57/3.86 % Maximum clause weight is 51.000.
% 12.57/3.86 % Given clauses 2665.
% 12.57/3.86
% 12.57/3.86 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------