%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : TOP041+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 : n015.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:03 AM UTC 2026
% Result : Theorem 147.45s 42.64s
% Output : CNFRefutation 147.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 17
% Syntax : Number of formulae : 158 ( 32 unt; 0 def)
% Number of atoms : 799 ( 129 equ)
% Maximal formula atoms : 18 ( 5 avg)
% Number of connectives : 1124 ( 483 ~; 534 |; 67 &)
% ( 6 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 18 ( 16 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-4 aty)
% Number of variables : 216 ( 12 sgn 48 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k5_subset_1,axiom,
! [A,B,C] :
( ( m1_subset_1(C,k1_zfmisc_1(A))
& m1_subset_1(B,k1_zfmisc_1(A)) )
=> k5_subset_1(A,B,C) = k5_subset_1(A,C,B) ),
file('theBenchmark.p',commutativity_k5_subset_1) ).
fof(d12_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] :
( ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v5_pre_topc(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> ( C = k4_tsp_2(A,B)
<=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
=> ( D = u1_struct_0(B)
=> ! [E] :
( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A)))
=> k5_subset_1(u1_struct_0(A),D,k3_tex_4(A,E)) = k4_pre_topc(A,B,C,E) ) ) ) ) ) ) ),
file('theBenchmark.p',d12_tsp_2) ).
fof(d1_tsp_1,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( l1_pre_topc(B)
=> ( m1_tsp_1(B,A)
<=> ( ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
=> ( v3_pre_topc(C,B)
<=> ? [D] :
( C = k3_xboole_0(D,u1_struct_0(B))
& v3_pre_topc(D,A)
& m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) ) ) )
& r1_tarski(u1_struct_0(B),u1_struct_0(A)) ) ) ) ),
file('theBenchmark.p',d1_tsp_1) ).
fof(dt_k1_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(k1_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))
& v5_pre_topc(k1_tsp_2(A,B),A,B)
& v1_funct_2(k1_tsp_2(A,B),u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(k1_tsp_2(A,B)) ) ),
file('theBenchmark.p',dt_k1_tsp_2) ).
fof(dt_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) )
=> m1_subset_1(k4_pre_topc(A,B,C,D),k1_zfmisc_1(u1_struct_0(B))) ),
file('theBenchmark.p',dt_k4_pre_topc) ).
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_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(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_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) )
=> k4_tsp_2(A,B) = k1_tsp_2(A,B) ),
file('theBenchmark.p',redefinition_k4_tsp_2) ).
fof(redefinition_k5_subset_1,axiom,
! [A,B,C] :
( ( m1_subset_1(C,k1_zfmisc_1(A))
& m1_subset_1(B,k1_zfmisc_1(A)) )
=> k5_subset_1(A,B,C) = k3_xboole_0(B,C) ),
file('theBenchmark.p',redefinition_k5_subset_1) ).
fof(redefinition_m1_tsp_1,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m1_tsp_1(B,A)
<=> m1_pre_topc(B,A) ) ),
file('theBenchmark.p',redefinition_m1_tsp_1) ).
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(t1_tsep_1,axiom,
! [A] :
( l1_pre_topc(A)
=> ! [B] :
( m1_pre_topc(B,A)
=> m1_subset_1(u1_struct_0(B),k1_zfmisc_1(u1_struct_0(A))) ) ),
file('theBenchmark.p',t1_tsep_1) ).
fof(t58_tex_4,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('theBenchmark.p',t58_tex_4) ).
fof(t34_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)))
=> ( v3_pre_topc(C,A)
=> v3_pre_topc(k4_pre_topc(A,B,k4_tsp_2(A,B),C),B) ) ) ) ),
file('theBenchmark.p',t34_tsp_2) ).
fof(t34_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)))
=> ( v3_pre_topc(C,A)
=> v3_pre_topc(k4_pre_topc(A,B,k4_tsp_2(A,B),C),B) ) ) ) ),
inference(assume_negation,[status(cth)],[t34_tsp_2]) ).
fof(nnf_125,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ v3_pre_topc(k4_pre_topc(A,B,k4_tsp_2(A,B),C),B)
& v3_pre_topc(C,A)
& 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)],[t34_tsp_2_neg]) ).
fof(sk_t34_tsp_2_neg,plain,
( ~ v3_pre_topc(k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),sK2),sK0)
& v3_pre_topc(sK2,sK1)
& m1_subset_1(sK2,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,sK2]),skolemize(A,sK1),skolemize(B,sK0),skolemize(C,sK2)],[nnf_125]) ).
cnf(c_126,negated_conjecture,
v2_tsp_2(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_t34_tsp_2_neg]) ).
cnf(c_127,plain,
( k1_tsp_2(A,B) = 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)],[redefinition_k4_tsp_2]) ).
cnf(c_128,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_129,plain,
( v5_pre_topc(k4_tsp_2(A,B),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_130,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_131,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_135,plain,
( v1_funct_1(k1_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_k1_tsp_2]) ).
cnf(c_140,plain,
( k5_subset_1(u1_struct_0(A),D,k3_tex_4(A,E)) = k4_pre_topc(A,B,C,E)
| ~ m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A)))
| u1_struct_0(B) != D
| ~ m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
| k4_tsp_2(A,B) != C
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v5_pre_topc(C,A,B)
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C)
| ~ 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)],[d12_tsp_2]) ).
cnf(c_197,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_126,c_131]) ).
cnf(c_198,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_199,plain,
( m1_subset_1(k4_pre_topc(A,B,C,D),k1_zfmisc_1(u1_struct_0(B)))
| ~ 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)],[dt_k4_pre_topc]) ).
cnf(c_200,negated_conjecture,
( v1_funct_1(k1_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_126,c_135]) ).
cnf(c_205,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),B,k3_tex_4(sK1,C)) = k4_pre_topc(sK1,sK0,A,C)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != B
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| k4_tsp_2(sK1,sK0) != A
| ~ m2_relset_1(A,u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(A,sK1,sK0)
| ~ v1_funct_2(A,u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ 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_126,c_140]) ).
cnf(c_207,plain,
( ~ m1_pre_topc(B,A)
| m1_tsp_1(B,A)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[redefinition_m1_tsp_1]) ).
cnf(c_215,plain,
( k3_xboole_0(D,u1_struct_0(B)) != C
| ~ v3_pre_topc(D,A)
| ~ m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
| v3_pre_topc(C,B)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
| ~ m1_tsp_1(B,A)
| ~ l1_pre_topc(B)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[d1_tsp_1]) ).
cnf(c_266,plain,
( ~ m1_pre_topc(B,A)
| ~ l1_pre_topc(A)
| k3_xboole_0(D,u1_struct_0(B)) != C
| ~ v3_pre_topc(D,A)
| ~ m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
| v3_pre_topc(C,B)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
| ~ l1_pre_topc(B)
| ~ l1_pre_topc(A) ),
inference(resolve,[status(thm)],[c_215,c_207]) ).
cnf(c_267,plain,
( ~ m1_pre_topc(B,A)
| k3_xboole_0(D,u1_struct_0(B)) != C
| ~ v3_pre_topc(D,A)
| ~ m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
| v3_pre_topc(C,B)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
| ~ l1_pre_topc(B)
| ~ l1_pre_topc(A) ),
inference(copy,[status(thm)],[c_266]) ).
cnf(c_325,plain,
( k5_subset_1(B,C,A) = k5_subset_1(B,A,C)
| ~ m1_subset_1(C,k1_zfmisc_1(B))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[commutativity_k5_subset_1]) ).
cnf(c_328,plain,
( l1_struct_0(A)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[dt_l1_pre_topc]) ).
cnf(c_331,plain,
( l1_pre_topc(B)
| ~ m2_tsp_1(B,A)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[dt_m2_tsp_1]) ).
cnf(c_421,plain,
( k5_subset_1(B,A,C) = k3_xboole_0(A,C)
| ~ m1_subset_1(C,k1_zfmisc_1(B))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[redefinition_k5_subset_1]) ).
cnf(c_422,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_424,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_428,plain,
( m1_subset_1(u1_struct_0(B),k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_pre_topc(B,A)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[t1_tsep_1]) ).
cnf(c_434,plain,
( 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(clausify,[status(thm)],[t58_tex_4]) ).
cnf(c_439,negated_conjecture,
~ v3_struct_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t34_tsp_2_neg]) ).
cnf(c_440,negated_conjecture,
v2_pre_topc(sK1),
inference(split_conjunct,[status(thm)],[sk_t34_tsp_2_neg]) ).
cnf(c_441,negated_conjecture,
l1_pre_topc(sK1),
inference(split_conjunct,[status(thm)],[sk_t34_tsp_2_neg]) ).
cnf(c_442,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t34_tsp_2_neg]) ).
cnf(c_443,negated_conjecture,
m2_tsp_1(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_t34_tsp_2_neg]) ).
cnf(c_444,negated_conjecture,
m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))),
inference(split_conjunct,[status(thm)],[sk_t34_tsp_2_neg]) ).
cnf(c_445,negated_conjecture,
v3_pre_topc(sK2,sK1),
inference(split_conjunct,[status(thm)],[sk_t34_tsp_2_neg]) ).
cnf(c_446,negated_conjecture,
~ v3_pre_topc(k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),sK2),sK0),
inference(split_conjunct,[status(thm)],[sk_t34_tsp_2_neg]) ).
cnf(c_447,negated_conjecture,
( k1_tsp_2(sK1,sK0) = 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_126,c_127]) ).
cnf(c_28777,negated_conjecture,
( k1_tsp_2(sK1,sK0) = k4_tsp_2(sK1,sK0)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_439,c_447]) ).
cnf(c_28778,negated_conjecture,
( k1_tsp_2(sK1,sK0) = k4_tsp_2(sK1,sK0)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_440,c_28777]) ).
cnf(c_28779,negated_conjecture,
( k1_tsp_2(sK1,sK0) = k4_tsp_2(sK1,sK0)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_441,c_28778]) ).
cnf(c_448,negated_conjecture,
( k1_tsp_2(sK1,sK0) = k4_tsp_2(sK1,sK0)
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_442,c_28779]) ).
cnf(c_449,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_126,c_128]) ).
cnf(c_28780,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_439,c_449]) ).
cnf(c_28781,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_440,c_28780]) ).
cnf(c_28782,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_441,c_28781]) ).
cnf(c_450,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_442,c_28782]) ).
cnf(c_451,negated_conjecture,
( v5_pre_topc(k4_tsp_2(sK1,sK0),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_126,c_129]) ).
cnf(c_28783,negated_conjecture,
( v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_439,c_451]) ).
cnf(c_28784,negated_conjecture,
( v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_440,c_28783]) ).
cnf(c_28785,negated_conjecture,
( v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_441,c_28784]) ).
cnf(c_452,negated_conjecture,
( v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ m1_pre_topc(sK0,sK1) ),
inference(resolve,[status(thm)],[c_442,c_28785]) ).
cnf(c_453,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_126,c_130]) ).
cnf(c_28786,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_439,c_453]) ).
cnf(c_28787,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_440,c_28786]) ).
cnf(c_28788,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_441,c_28787]) ).
cnf(c_454,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_442,c_28788]) ).
cnf(c_537,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_197,c_198]) ).
cnf(c_28789,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_537]) ).
cnf(c_28790,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_439,c_28789]) ).
cnf(c_28791,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_440,c_28790]) ).
cnf(c_28792,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_441,c_28791]) ).
cnf(c_538,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_442,c_28792]) ).
cnf(c_539,negated_conjecture,
( m1_subset_1(k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C),k1_zfmisc_1(u1_struct_0(B)))
| ~ 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_197,c_199]) ).
cnf(c_28793,negated_conjecture,
( m1_subset_1(k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C),k1_zfmisc_1(u1_struct_0(B)))
| ~ 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_439,c_539]) ).
cnf(c_28794,negated_conjecture,
( m1_subset_1(k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C),k1_zfmisc_1(u1_struct_0(B)))
| ~ 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_440,c_28793]) ).
cnf(c_28795,negated_conjecture,
( m1_subset_1(k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C),k1_zfmisc_1(u1_struct_0(B)))
| ~ 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_441,c_28794]) ).
cnf(c_540,negated_conjecture,
( m1_subset_1(k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C),k1_zfmisc_1(u1_struct_0(B)))
| ~ 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_442,c_28795]) ).
cnf(c_550,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k4_tsp_2(sK1,sK0) != k1_tsp_2(sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ 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_205,c_200]) ).
cnf(c_28796,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k1_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_550]) ).
cnf(c_28797,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k1_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_28796]) ).
cnf(c_28798,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k1_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_28797]) ).
cnf(c_28799,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| v3_struct_0(sK0)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k1_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_28798]) ).
cnf(c_28800,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k1_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_28799]) ).
cnf(c_28801,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k1_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_439,c_28800]) ).
cnf(c_28802,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k1_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_440,c_28801]) ).
cnf(c_28803,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k1_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_441,c_28802]) ).
cnf(c_28804,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k1_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_tsp_1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_442,c_28803]) ).
cnf(c_551,negated_conjecture,
( ~ m1_pre_topc(sK0,sK1)
| k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k1_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_443,c_28804]) ).
cnf(c_788,plain,
l1_struct_0(sK1),
inference(resolve,[status(thm)],[c_441,c_328]) ).
cnf(c_28805,negated_conjecture,
( m1_pre_topc(sK0,sK1)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_443,c_424]) ).
cnf(c_791,negated_conjecture,
m1_pre_topc(sK0,sK1),
inference(resolve,[status(thm)],[c_441,c_28805]) ).
cnf(c_28806,negated_conjecture,
( l1_pre_topc(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_443,c_331]) ).
cnf(c_792,negated_conjecture,
l1_pre_topc(sK0),
inference(resolve,[status(thm)],[c_441,c_28806]) ).
cnf(c_800,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k1_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_791,c_551]) ).
cnf(c_803,negated_conjecture,
( m1_subset_1(k4_pre_topc(A,B,k4_tsp_2(sK1,sK0),C),k1_zfmisc_1(u1_struct_0(B)))
| ~ 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_791,c_540]) ).
cnf(c_804,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_791,c_538]) ).
cnf(c_812,negated_conjecture,
v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_791,c_454]) ).
cnf(c_813,negated_conjecture,
v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0),
inference(resolve,[status(thm)],[c_791,c_452]) ).
cnf(c_814,negated_conjecture,
m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_791,c_450]) ).
cnf(c_815,negated_conjecture,
k1_tsp_2(sK1,sK0) = k4_tsp_2(sK1,sK0),
inference(resolve,[status(thm)],[c_791,c_448]) ).
cnf(c_28807,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k1_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k1_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(paramod,[status(thm)],[c_815,c_800]) ).
cnf(c_28808,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k1_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k1_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(paramod,[status(thm)],[c_815,c_28807]) ).
cnf(c_28809,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k1_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(paramod,[status(thm)],[c_815,c_28808]) ).
cnf(c_28810,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k1_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k4_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(paramod,[status(thm)],[c_815,c_28809]) ).
cnf(c_28811,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| k4_tsp_2(sK1,sK0) != k4_tsp_2(sK1,sK0)
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(paramod,[status(thm)],[c_815,c_28810]) ).
cnf(c_28812,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0)
| ~ v1_funct_2(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(copy,[status(thm)],[c_28811]) ).
cnf(c_28813,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v5_pre_topc(k4_tsp_2(sK1,sK0),sK1,sK0) ),
inference(resolve,[status(thm)],[c_812,c_28812]) ).
cnf(c_28814,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_813,c_28813]) ).
cnf(c_817,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,B)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(resolve,[status(thm)],[c_814,c_28814]) ).
cnf(c_821,plain,
( k5_subset_1(u1_struct_0(sK1),sK2,A) = k3_xboole_0(sK2,A)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(resolve,[status(thm)],[c_444,c_421]) ).
cnf(c_825,plain,
( k5_subset_1(u1_struct_0(sK1),sK2,A) = k5_subset_1(u1_struct_0(sK1),A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(resolve,[status(thm)],[c_444,c_325]) ).
cnf(c_28815,negated_conjecture,
( k3_tex_4(sK1,sK2) = sK2
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_445,c_434]) ).
cnf(c_28816,negated_conjecture,
( k3_tex_4(sK1,sK2) = sK2
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_439,c_28815]) ).
cnf(c_28817,negated_conjecture,
( k3_tex_4(sK1,sK2) = sK2
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_440,c_28816]) ).
cnf(c_28818,negated_conjecture,
( k3_tex_4(sK1,sK2) = sK2
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(resolve,[status(thm)],[c_441,c_28817]) ).
cnf(c_842,negated_conjecture,
k3_tex_4(sK1,sK2) = sK2,
inference(resolve,[status(thm)],[c_444,c_28818]) ).
cnf(c_929,plain,
l1_struct_0(sK0),
inference(resolve,[status(thm)],[c_792,c_328]) ).
cnf(c_28819,plain,
( m1_subset_1(u1_struct_0(sK0),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_791,c_428]) ).
cnf(c_982,negated_conjecture,
m1_subset_1(u1_struct_0(sK0),k1_zfmisc_1(u1_struct_0(sK1))),
inference(resolve,[status(thm)],[c_441,c_28819]) ).
cnf(c_28820,plain,
( k3_xboole_0(B,u1_struct_0(sK0)) != A
| ~ v3_pre_topc(B,sK1)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_pre_topc(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_pre_topc(sK0)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_791,c_267]) ).
cnf(c_28821,negated_conjecture,
( k3_xboole_0(B,u1_struct_0(sK0)) != A
| ~ v3_pre_topc(B,sK1)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_pre_topc(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_pre_topc(sK0) ),
inference(resolve,[status(thm)],[c_441,c_28820]) ).
cnf(c_984,negated_conjecture,
( k3_xboole_0(B,u1_struct_0(sK0)) != A
| ~ v3_pre_topc(B,sK1)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_pre_topc(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_792,c_28821]) ).
cnf(c_2467,plain,
m1_relset_1(k4_tsp_2(sK1,sK0),u1_struct_0(sK1),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_814,c_422]) ).
cnf(c_28822,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,k3_tex_4(sK1,sK2)) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),sK2)
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(resolve,[status(thm)],[c_817,c_444]) ).
cnf(c_2496,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,sK2) = k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),sK2)
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(paramod,[status(thm)],[c_842,c_28822]) ).
cnf(c_28823,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_2467,c_804]) ).
cnf(c_28824,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_788,c_28823]) ).
cnf(c_28825,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_929,c_28824]) ).
cnf(c_2672,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_812,c_28825]) ).
cnf(c_28826,negated_conjecture,
( m1_subset_1(k4_pre_topc(sK1,sK0,k4_tsp_2(sK1,sK0),A),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ 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_2467,c_803]) ).
cnf(c_28827,negated_conjecture,
( m1_subset_1(k9_relat_1(k4_tsp_2(sK1,sK0),A),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ 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(paramod,[status(thm)],[c_2672,c_28826]) ).
cnf(c_28828,negated_conjecture,
( m1_subset_1(k9_relat_1(k4_tsp_2(sK1,sK0),A),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ 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_788,c_28827]) ).
cnf(c_28829,negated_conjecture,
( m1_subset_1(k9_relat_1(k4_tsp_2(sK1,sK0),A),k1_zfmisc_1(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_929,c_28828]) ).
cnf(c_2673,negated_conjecture,
m1_subset_1(k9_relat_1(k4_tsp_2(sK1,sK0),A),k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_812,c_28829]) ).
cnf(c_28830,negated_conjecture,
( k5_subset_1(u1_struct_0(sK1),A,sK2) = k9_relat_1(k4_tsp_2(sK1,sK0),sK2)
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(paramod,[status(thm)],[c_2672,c_2496]) ).
cnf(c_2679,negated_conjecture,
( k9_relat_1(k4_tsp_2(sK1,sK0),sK2) = k5_subset_1(u1_struct_0(sK1),A,sK2)
| u1_struct_0(sK0) != A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(copy,[status(thm)],[c_28830]) ).
cnf(c_2709,negated_conjecture,
~ v3_pre_topc(k9_relat_1(k4_tsp_2(sK1,sK0),sK2),sK0),
inference(paramod,[status(thm)],[c_2672,c_446]) ).
cnf(c_28831,plain,
k5_subset_1(u1_struct_0(sK1),sK2,u1_struct_0(sK0)) = k5_subset_1(u1_struct_0(sK1),u1_struct_0(sK0),sK2),
inference(resolve,[status(thm)],[c_982,c_825]) ).
cnf(c_3835,plain,
k5_subset_1(u1_struct_0(sK1),u1_struct_0(sK0),sK2) = k5_subset_1(u1_struct_0(sK1),sK2,u1_struct_0(sK0)),
inference(copy,[status(thm)],[c_28831]) ).
cnf(c_3837,plain,
k5_subset_1(u1_struct_0(sK1),sK2,u1_struct_0(sK0)) = k3_xboole_0(sK2,u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_982,c_821]) ).
cnf(c_3872,plain,
k5_subset_1(u1_struct_0(sK1),u1_struct_0(sK0),sK2) = k3_xboole_0(sK2,u1_struct_0(sK0)),
inference(paramod,[status(thm)],[c_3837,c_3835]) ).
cnf(c_28832,negated_conjecture,
( k3_xboole_0(sK2,u1_struct_0(sK0)) != A
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_pre_topc(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_984,c_445]) ).
cnf(c_3888,negated_conjecture,
( k3_xboole_0(sK2,u1_struct_0(sK0)) != A
| v3_pre_topc(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_444,c_28832]) ).
cnf(c_28833,plain,
( k9_relat_1(k4_tsp_2(sK1,sK0),sK2) = k5_subset_1(u1_struct_0(sK1),u1_struct_0(sK0),sK2)
| u1_struct_0(sK0) != u1_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_2679,c_982]) ).
cnf(c_28834,plain,
( k9_relat_1(k4_tsp_2(sK1,sK0),sK2) = k3_xboole_0(sK2,u1_struct_0(sK0))
| u1_struct_0(sK0) != u1_struct_0(sK0) ),
inference(paramod,[status(thm)],[c_3872,c_28833]) ).
cnf(c_26069,plain,
k9_relat_1(k4_tsp_2(sK1,sK0),sK2) = k3_xboole_0(sK2,u1_struct_0(sK0)),
inference(copy,[status(thm)],[c_28834]) ).
cnf(c_26100,negated_conjecture,
~ v3_pre_topc(k3_xboole_0(sK2,u1_struct_0(sK0)),sK0),
inference(paramod,[status(thm)],[c_26069,c_2709]) ).
cnf(c_26102,plain,
m1_subset_1(k3_xboole_0(sK2,u1_struct_0(sK0)),k1_zfmisc_1(u1_struct_0(sK0))),
inference(paramod,[status(thm)],[c_26069,c_2673]) ).
cnf(c_28835,plain,
( k3_xboole_0(sK2,u1_struct_0(sK0)) != k3_xboole_0(sK2,u1_struct_0(sK0))
| v3_pre_topc(k3_xboole_0(sK2,u1_struct_0(sK0)),sK0) ),
inference(resolve,[status(thm)],[c_3888,c_26102]) ).
cnf(c_28836,plain,
v3_pre_topc(k3_xboole_0(sK2,u1_struct_0(sK0)),sK0),
inference(copy,[status(thm)],[c_28835]) ).
cnf(c_28776,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_26100,c_28836]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : TOP041+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/10.46 % Computer : n015.cluster.edu
% 0.12/10.46 % Model : x86_64 x86_64
% 0.12/10.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.46 % Memory : 8046.5625MB
% 0.12/10.46 % OS : Linux 6.8.0-71-generic
% 0.12/10.46 % CPULimit : 300
% 0.12/10.46 % WCLimit : 300
% 0.12/10.46 % DateTime : Sat Sep 26 20:46:55 UTC 2026
% 0.12/10.46 % CPUTime :
% 0.12/10.47 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/10.47 % Process 721910 was started by sandbox on n015,
% 0.12/10.47 % Sat Sep 26 20:46:55 2026
% 0.12/10.47 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/10.48
% 0.12/10.48 % From the command line: assign(max_seconds, 300).
% 147.45/42.64
% 147.45/42.64 % given #500 (W,wt=16): 744 v1_xboole_0(A) | r2_hidden(f8(A),A). [resolve(430,a,336,a)].
% 147.45/42.64
% 147.45/42.64 % given #1000 (A,wt=32): 995 m1_subset_1(k5_subset_1(A,f8(k1_zfmisc_1(A)),f12(A)),k1_zfmisc_1(A)) | v1_xboole_0(A). [resolve(637,a,386,b)].
% 147.45/42.64
% 147.45/42.64 % given #1500 (T,wt=22): 7024 -v1_membered(u1_struct_0(c6)) | v1_membered(u1_struct_0(f6(c6))). [resolve(1609,a,302,b)].
% 147.45/42.64
% 147.45/42.64 % given #2000 (W,wt=23): 9419 -v3_membered(u1_struct_0(c6)) | v3_membered(k3_tex_4(c6,f18(c6))). [resolve(3702,a,307,b)].
% 147.45/42.64
% 147.45/42.64 % given #2500 (T,wt=23): 15956 -v5_membered(u1_struct_0(f6(c6))) | v1_membered(f15(f6(c6))). [resolve(1661,a,315,b)].
% 147.45/42.64
% 147.45/42.64 % given #3000 (T,wt=25): 4947 v1_xboole_0(f17(f6(f11(c5)))). [resolve(4924,a,400,a)].
% 147.45/42.64
% 147.45/42.64 % given #3500 (T,wt=23): 19776 -v3_membered(u1_struct_0(f11(c6))) | v1_membered(f20(f11(c6))). [resolve(1984,a,305,b)].
% 147.45/42.64
% 147.45/42.64 % given #4000 (A,wt=60): 2131 -m1_subset_1(f4(f11(c6),f11(c6)),k1_zfmisc_1(u1_struct_0(f11(c6)))) | -v3_pre_topc(f4(f11(c6),f11(c6)),f11(c6)) | m1_subset_1(f3(f11(c6),f11(c6),f4(f11(c6),f11(c6))),k1_zfmisc_1(u1_struct_0(f11(c6)))) | f4(f11(c6),f11(c6)) != k1_xboole_0. [resolve(1982,a,621,f),rewrite([741(52)]),unit_del(a,1584),unit_del(e,760)].
% 147.45/42.64
% 147.45/42.64 % given #4500 (A,wt=30): 2378 -m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c5))) | m1_subset_1(k5_subset_1(u1_struct_0(c5),f16(c5),A),k1_zfmisc_1(u1_struct_0(c5))). [resolve(773,a,327,a)].
% 147.45/42.64
% 147.45/42.64 % given #5000 (A,wt=49): 2618 v3_pre_topc(f4(c5,c5),c5) | k3_xboole_0(u1_struct_0(c5),f5(c5,c5)) = f4(c5,c5) | -m1_subset_1(f3(c5,c5,c7),k1_zfmisc_1(u1_struct_0(c5))) | m1_subset_1(f3(c5,c5,f3(c5,c5,c7)),k1_zfmisc_1(u1_struct_0(c5))). [resolve(858,a,559,c),merge(f),merge(g),unit_del(c,441)].
% 147.45/42.64
% 147.45/42.64 % given #5500 (T,wt=28): 3287 m2_tsp_1(f11(f9(f6(c6))),f9(f6(c6))). [resolve(1638,a,338,a)].
% 147.45/42.64
% 147.45/42.64 % given #6000 (T,wt=28): 21547 k5_subset_1(A,A,f12(A)) = k3_xboole_0(A,f12(A)) | k1_xboole_0 = A. [resolve(2255,b,436,a)].
% 147.45/42.64
% 147.45/42.64 % SZS status Theorem for theBenchmark
% 147.45/42.64
% 147.45/42.64 % Proof 1 at 5.77 (+ 1.61) seconds.
% 147.45/42.64 % Length of proof is 95.
% 147.45/42.64 % Level of proof is 11.
% 147.45/42.64 % Maximum clause weight is 76.000.
% 147.45/42.64 % Given clauses 6419.
% 147.45/42.64
% 147.45/42.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------