%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : TOP028+3 : TPTP v9.2.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:56:38 PM UTC 2026
% Result : Theorem 48.15s 31.21s
% Output : CNFRefutation 48.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 24
% Syntax : Number of formulae : 126 ( 29 unt; 0 def)
% Number of atoms : 636 ( 51 equ)
% Maximal formula atoms : 194 ( 5 avg)
% Number of connectives : 856 ( 346 ~; 342 |; 112 &)
% ( 12 <=>; 44 =>; 0 <=; 0 <~>)
% Maximal formula depth : 36 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 2 con; 0-4 aty)
% Number of variables : 200 ( 8 sgn 112 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(rc3_tops_1,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v2_pre_topc(X1)
& l1_pre_topc(X1) )
=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
& ~ v1_xboole_0(X2)
& v3_pre_topc(X2,X1)
& v4_pre_topc(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+207.ax',rc3_tops_1) ).
fof(t10_tsp_2,conjecture,
! [X1] :
( ( ~ v3_struct_0(X1)
& v2_pre_topc(X1)
& l1_pre_topc(X1) )
=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
& v1_tsp_2(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_tsp_2) ).
fof(d2_subset_1,axiom,
! [X1,X2] :
( ( ~ v1_xboole_0(X1)
=> ( m1_subset_1(X2,X1)
<=> r2_hidden(X2,X1) ) )
& ( v1_xboole_0(X1)
=> ( m1_subset_1(X2,X1)
<=> v1_xboole_0(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+7.ax',d2_subset_1) ).
fof(t5_subset,axiom,
! [X1,X2,X3] :
~ ( r2_hidden(X1,X2)
& m1_subset_1(X2,k1_zfmisc_1(X3))
& v1_xboole_0(X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+9.ax',t5_subset) ).
fof(existence_m1_subset_1,axiom,
! [X1] :
? [X2] : m1_subset_1(X2,X1),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+7.ax',existence_m1_subset_1) ).
fof(t8_boole,axiom,
! [X1,X2] :
~ ( v1_xboole_0(X1)
& X1 != X2
& v1_xboole_0(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+3.ax',t8_boole) ).
fof(rc2_funct_1,axiom,
? [X1] :
( v1_relat_1(X1)
& v1_xboole_0(X1)
& v1_funct_1(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+11.ax',rc2_funct_1) ).
fof(rc4_tex_2,axiom,
! [X1] :
( ~ v1_xboole_0(X1)
=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
& ~ v1_xboole_0(X2)
& ~ v1_tex_2(X2,k1_zfmisc_1(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+387.ax',rc4_tex_2) ).
fof(rc2_subset_1,axiom,
! [X1] :
? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
& v1_xboole_0(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+7.ax',rc2_subset_1) ).
fof(t48_pre_topc,axiom,
! [X1] :
( l1_pre_topc(X1)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> r1_tarski(X2,k6_pre_topc(X1,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+206.ax',t48_pre_topc) ).
fof(t5_tex_2,axiom,
! [X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
=> ( v1_tex_2(X2,k1_zfmisc_1(X1))
<=> X2 != X1 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+387.ax',t5_tex_2) ).
fof(rc2_tex_2,axiom,
! [X1] :
? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
& ~ v1_tex_2(X2,k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+387.ax',rc2_tex_2) ).
fof(t3_subset,axiom,
! [X1,X2] :
( m1_subset_1(X1,k1_zfmisc_1(X2))
<=> r1_tarski(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+9.ax',t3_subset) ).
fof(t44_tops_1,axiom,
! [X1] :
( l1_pre_topc(X1)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> r1_tarski(k1_tops_1(X1,X2),X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+207.ax',t44_tops_1) ).
fof(t7_ordinal1,axiom,
! [X1,X2] :
~ ( r2_hidden(X1,X2)
& r1_tarski(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+14.ax',t7_ordinal1) ).
fof(d10_xboole_0,axiom,
! [X1,X2] :
( X1 = X2
<=> ( r1_tarski(X1,X2)
& r1_tarski(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+2.ax',d10_xboole_0) ).
fof(dt_k6_pre_topc,axiom,
! [X1,X2] :
( ( l1_pre_topc(X1)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
=> m1_subset_1(k6_pre_topc(X1,X2),k1_zfmisc_1(u1_struct_0(X1))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+206.ax',dt_k6_pre_topc) ).
fof(d3_tarski,axiom,
! [X1,X2] :
( r1_tarski(X1,X2)
<=> ! [X3] :
( r2_hidden(X3,X1)
=> r2_hidden(X3,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+1.ax',d3_tarski) ).
fof(d2_tops_3,axiom,
! [X1] :
( l1_pre_topc(X1)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ( v1_tops_1(X2,X1)
<=> k6_pre_topc(X1,X2) = u1_struct_0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+370.ax',d2_tops_3) ).
fof(d8_tsp_1,axiom,
! [X1] :
( l1_pre_topc(X1)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ( v1_tsp_1(X2,X1)
<=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ~ ( r2_hidden(X3,X2)
& r2_hidden(X4,X2)
& X3 != X4
& ! [X5] :
( m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1)))
=> ~ ( v3_pre_topc(X5,X1)
& r2_hidden(X3,X5)
& ~ r2_hidden(X4,X5) ) )
& ! [X5] :
( m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1)))
=> ~ ( v3_pre_topc(X5,X1)
& ~ r2_hidden(X3,X5)
& r2_hidden(X4,X5) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+406.ax',d8_tsp_1) ).
fof(d3_tops_1,axiom,
! [X1] :
( l1_pre_topc(X1)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ( v1_tops_1(X2,X1)
<=> k6_pre_topc(X1,X2) = k2_pre_topc(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+207.ax',d3_tops_1) ).
fof(t9_tsp_2,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v2_pre_topc(X1)
& l1_pre_topc(X1) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ~ ( v1_tsp_1(X2,X1)
& ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
=> ~ ( r1_tarski(X2,X3)
& v1_tsp_2(X3,X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t9_tsp_2) ).
fof(t13_tsp_1,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v2_pre_topc(X1)
& l1_pre_topc(X1) )
=> ! [X2] :
( ( v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
=> v1_tsp_1(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+406.ax',t13_tsp_1) ).
fof(dt_k1_tops_1,axiom,
! [X1,X2] :
( ( l1_pre_topc(X1)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
=> m1_subset_1(k1_tops_1(X1,X2),k1_zfmisc_1(u1_struct_0(X1))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+207.ax',dt_k1_tops_1) ).
fof(c_0_24,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v2_pre_topc(X1)
& l1_pre_topc(X1) )
=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
& ~ v1_xboole_0(X2)
& v3_pre_topc(X2,X1)
& v4_pre_topc(X2,X1) ) ),
inference(fof_simplification,[status(thm)],[rc3_tops_1]) ).
fof(c_0_25,negated_conjecture,
~ ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_pre_topc(X1)
& l1_pre_topc(X1) )
=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
& v1_tsp_2(X2,X1) ) ),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[t10_tsp_2])]) ).
fof(c_0_26,plain,
! [X1277] :
( ( m1_subset_1(esk65_1(X1277),k1_zfmisc_1(u1_struct_0(X1277)))
| v3_struct_0(X1277)
| ~ v2_pre_topc(X1277)
| ~ l1_pre_topc(X1277) )
& ( ~ v1_xboole_0(esk65_1(X1277))
| v3_struct_0(X1277)
| ~ v2_pre_topc(X1277)
| ~ l1_pre_topc(X1277) )
& ( v3_pre_topc(esk65_1(X1277),X1277)
| v3_struct_0(X1277)
| ~ v2_pre_topc(X1277)
| ~ l1_pre_topc(X1277) )
& ( v4_pre_topc(esk65_1(X1277),X1277)
| v3_struct_0(X1277)
| ~ v2_pre_topc(X1277)
| ~ l1_pre_topc(X1277) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_24])])])]) ).
fof(c_0_27,negated_conjecture,
! [X756] :
( ~ v3_struct_0(esk1_0)
& v2_pre_topc(esk1_0)
& l1_pre_topc(esk1_0)
& ( ~ m1_subset_1(X756,k1_zfmisc_1(u1_struct_0(esk1_0)))
| ~ v1_tsp_2(X756,esk1_0) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_25])])])]) ).
fof(c_0_28,plain,
! [X1,X2] :
( ( ~ v1_xboole_0(X1)
=> ( m1_subset_1(X2,X1)
<=> r2_hidden(X2,X1) ) )
& ( v1_xboole_0(X1)
=> ( m1_subset_1(X2,X1)
<=> v1_xboole_0(X2) ) ) ),
inference(fof_simplification,[status(thm)],[d2_subset_1]) ).
fof(c_0_29,plain,
! [X809,X810,X811] :
( ~ r2_hidden(X809,X810)
| ~ m1_subset_1(X810,k1_zfmisc_1(X811))
| ~ v1_xboole_0(X811) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t5_subset])]) ).
cnf(c_0_30,plain,
( m1_subset_1(esk65_1(X1),k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_31,negated_conjecture,
v2_pre_topc(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_32,negated_conjecture,
l1_pre_topc(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_33,negated_conjecture,
~ v3_struct_0(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
fof(c_0_34,plain,
! [X1334,X1335] :
( ( ~ m1_subset_1(X1335,X1334)
| r2_hidden(X1335,X1334)
| v1_xboole_0(X1334) )
& ( ~ r2_hidden(X1335,X1334)
| m1_subset_1(X1335,X1334)
| v1_xboole_0(X1334) )
& ( ~ m1_subset_1(X1335,X1334)
| v1_xboole_0(X1335)
| ~ v1_xboole_0(X1334) )
& ( ~ v1_xboole_0(X1335)
| m1_subset_1(X1335,X1334)
| ~ v1_xboole_0(X1334) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_28])])]) ).
fof(c_0_35,plain,
! [X788] : m1_subset_1(esk4_1(X788),X788),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[existence_m1_subset_1])]) ).
fof(c_0_36,plain,
! [X1332,X1333] :
( ~ v1_xboole_0(X1332)
| X1332 = X1333
| ~ v1_xboole_0(X1333) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t8_boole])]) ).
fof(c_0_37,plain,
( v1_relat_1(esk77_0)
& v1_xboole_0(esk77_0)
& v1_funct_1(esk77_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc2_funct_1])]) ).
fof(c_0_38,plain,
! [X1] :
( ~ v1_xboole_0(X1)
=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
& ~ v1_xboole_0(X2)
& ~ v1_tex_2(X2,k1_zfmisc_1(X1)) ) ),
inference(fof_simplification,[status(thm)],[rc4_tex_2]) ).
cnf(c_0_39,plain,
( ~ r2_hidden(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X3))
| ~ v1_xboole_0(X3) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
cnf(c_0_40,negated_conjecture,
m1_subset_1(esk65_1(esk1_0),k1_zfmisc_1(u1_struct_0(esk1_0))),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30,c_0_31]),c_0_32])]),c_0_33]) ).
cnf(c_0_41,plain,
( r2_hidden(X1,X2)
| v1_xboole_0(X2)
| ~ m1_subset_1(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
cnf(c_0_42,plain,
m1_subset_1(esk4_1(X1),X1),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
cnf(c_0_43,plain,
( X1 = X2
| ~ v1_xboole_0(X1)
| ~ v1_xboole_0(X2) ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
cnf(c_0_44,plain,
v1_xboole_0(esk77_0),
inference(split_conjunct,[status(thm)],[c_0_37]) ).
fof(c_0_45,plain,
! [X793] :
( m1_subset_1(esk6_1(X793),k1_zfmisc_1(X793))
& v1_xboole_0(esk6_1(X793)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc2_subset_1])]) ).
fof(c_0_46,plain,
! [X1397,X1398] :
( ~ l1_pre_topc(X1397)
| ~ m1_subset_1(X1398,k1_zfmisc_1(u1_struct_0(X1397)))
| r1_tarski(X1398,k6_pre_topc(X1397,X1398)) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t48_pre_topc])])]) ).
fof(c_0_47,plain,
! [X1202] :
( ( m1_subset_1(esk53_1(X1202),k1_zfmisc_1(X1202))
| v1_xboole_0(X1202) )
& ( ~ v1_xboole_0(esk53_1(X1202))
| v1_xboole_0(X1202) )
& ( ~ v1_tex_2(esk53_1(X1202),k1_zfmisc_1(X1202))
| v1_xboole_0(X1202) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_38])])])]) ).
cnf(c_0_48,negated_conjecture,
( ~ v1_xboole_0(u1_struct_0(esk1_0))
| ~ r2_hidden(X1,esk65_1(esk1_0)) ),
inference(spm,[status(thm)],[c_0_39,c_0_40]) ).
cnf(c_0_49,plain,
( v1_xboole_0(X1)
| r2_hidden(esk4_1(X1),X1) ),
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
cnf(c_0_50,plain,
( X1 = esk77_0
| ~ v1_xboole_0(X1) ),
inference(spm,[status(thm)],[c_0_43,c_0_44]) ).
cnf(c_0_51,plain,
v1_xboole_0(esk6_1(X1)),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
cnf(c_0_52,plain,
( r1_tarski(X2,k6_pre_topc(X1,X2))
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(split_conjunct,[status(thm)],[c_0_46]) ).
cnf(c_0_53,plain,
( m1_subset_1(esk53_1(X1),k1_zfmisc_1(X1))
| v1_xboole_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
cnf(c_0_54,plain,
( v3_struct_0(X1)
| ~ v1_xboole_0(esk65_1(X1))
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_55,negated_conjecture,
( v1_xboole_0(esk65_1(esk1_0))
| ~ v1_xboole_0(u1_struct_0(esk1_0)) ),
inference(spm,[status(thm)],[c_0_48,c_0_49]) ).
fof(c_0_56,plain,
! [X1230,X1231] :
( ( ~ v1_tex_2(X1231,k1_zfmisc_1(X1230))
| X1231 != X1230
| ~ m1_subset_1(X1231,k1_zfmisc_1(X1230)) )
& ( X1231 = X1230
| v1_tex_2(X1231,k1_zfmisc_1(X1230))
| ~ m1_subset_1(X1231,k1_zfmisc_1(X1230)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t5_tex_2])])]) ).
fof(c_0_57,plain,
! [X1] :
? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
& ~ v1_tex_2(X2,k1_zfmisc_1(X1)) ),
inference(fof_simplification,[status(thm)],[rc2_tex_2]) ).
fof(c_0_58,plain,
! [X842,X843] :
( ( ~ m1_subset_1(X842,k1_zfmisc_1(X843))
| r1_tarski(X842,X843) )
& ( ~ r1_tarski(X842,X843)
| m1_subset_1(X842,k1_zfmisc_1(X843)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t3_subset])]) ).
cnf(c_0_59,plain,
m1_subset_1(esk6_1(X1),k1_zfmisc_1(X1)),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
cnf(c_0_60,plain,
esk6_1(X1) = esk77_0,
inference(spm,[status(thm)],[c_0_50,c_0_51]) ).
cnf(c_0_61,plain,
( v1_xboole_0(u1_struct_0(X1))
| r1_tarski(esk53_1(u1_struct_0(X1)),k6_pre_topc(X1,esk53_1(u1_struct_0(X1))))
| ~ l1_pre_topc(X1) ),
inference(spm,[status(thm)],[c_0_52,c_0_53]) ).
cnf(c_0_62,negated_conjecture,
~ v1_xboole_0(u1_struct_0(esk1_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54,c_0_55]),c_0_31]),c_0_32])]),c_0_33]) ).
cnf(c_0_63,plain,
( X1 = X2
| v1_tex_2(X1,k1_zfmisc_1(X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(split_conjunct,[status(thm)],[c_0_56]) ).
cnf(c_0_64,plain,
( v1_xboole_0(X1)
| ~ v1_tex_2(esk53_1(X1),k1_zfmisc_1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
fof(c_0_65,plain,
! [X1190] :
( m1_subset_1(esk51_1(X1190),k1_zfmisc_1(X1190))
& ~ v1_tex_2(esk51_1(X1190),k1_zfmisc_1(X1190)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[c_0_57])]) ).
fof(c_0_66,plain,
! [X1436,X1437] :
( ~ l1_pre_topc(X1436)
| ~ m1_subset_1(X1437,k1_zfmisc_1(u1_struct_0(X1436)))
| r1_tarski(k1_tops_1(X1436,X1437),X1437) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t44_tops_1])])]) ).
fof(c_0_67,plain,
! [X846,X847] :
( ~ r2_hidden(X846,X847)
| ~ r1_tarski(X847,X846) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t7_ordinal1])]) ).
cnf(c_0_68,plain,
( r1_tarski(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
cnf(c_0_69,plain,
m1_subset_1(esk77_0,k1_zfmisc_1(X1)),
inference(rw,[status(thm)],[c_0_59,c_0_60]) ).
fof(c_0_70,plain,
! [X820,X821] :
( ( r1_tarski(X820,X821)
| X820 != X821 )
& ( r1_tarski(X821,X820)
| X820 != X821 )
& ( ~ r1_tarski(X820,X821)
| ~ r1_tarski(X821,X820)
| X820 = X821 ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[d10_xboole_0])])]) ).
cnf(c_0_71,negated_conjecture,
r1_tarski(esk53_1(u1_struct_0(esk1_0)),k6_pre_topc(esk1_0,esk53_1(u1_struct_0(esk1_0)))),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_61,c_0_32]),c_0_62]) ).
cnf(c_0_72,plain,
( esk53_1(X1) = X1
| v1_xboole_0(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_63,c_0_53]),c_0_64]) ).
fof(c_0_73,plain,
! [X1407,X1408] :
( ~ l1_pre_topc(X1407)
| ~ m1_subset_1(X1408,k1_zfmisc_1(u1_struct_0(X1407)))
| m1_subset_1(k6_pre_topc(X1407,X1408),k1_zfmisc_1(u1_struct_0(X1407))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_k6_pre_topc])]) ).
cnf(c_0_74,plain,
m1_subset_1(esk51_1(X1),k1_zfmisc_1(X1)),
inference(split_conjunct,[status(thm)],[c_0_65]) ).
cnf(c_0_75,plain,
~ v1_tex_2(esk51_1(X1),k1_zfmisc_1(X1)),
inference(split_conjunct,[status(thm)],[c_0_65]) ).
fof(c_0_76,plain,
! [X813,X814,X815,X816,X817] :
( ( ~ r1_tarski(X813,X814)
| ~ r2_hidden(X815,X813)
| r2_hidden(X815,X814) )
& ( r2_hidden(esk11_2(X816,X817),X816)
| r1_tarski(X816,X817) )
& ( ~ r2_hidden(esk11_2(X816,X817),X817)
| r1_tarski(X816,X817) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[d3_tarski])])])])])]) ).
cnf(c_0_77,plain,
( r1_tarski(k1_tops_1(X1,X2),X2)
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(split_conjunct,[status(thm)],[c_0_66]) ).
cnf(c_0_78,plain,
( ~ r2_hidden(X1,X2)
| ~ r1_tarski(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_67]) ).
cnf(c_0_79,plain,
r1_tarski(esk77_0,X1),
inference(spm,[status(thm)],[c_0_68,c_0_69]) ).
fof(c_0_80,plain,
! [X1134,X1135] :
( ( ~ v1_tops_1(X1135,X1134)
| k6_pre_topc(X1134,X1135) = u1_struct_0(X1134)
| ~ m1_subset_1(X1135,k1_zfmisc_1(u1_struct_0(X1134)))
| ~ l1_pre_topc(X1134) )
& ( k6_pre_topc(X1134,X1135) != u1_struct_0(X1134)
| v1_tops_1(X1135,X1134)
| ~ m1_subset_1(X1135,k1_zfmisc_1(u1_struct_0(X1134)))
| ~ l1_pre_topc(X1134) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[d2_tops_3])])])]) ).
cnf(c_0_81,plain,
( X1 = X2
| ~ r1_tarski(X1,X2)
| ~ r1_tarski(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_70]) ).
cnf(c_0_82,negated_conjecture,
r1_tarski(u1_struct_0(esk1_0),k6_pre_topc(esk1_0,u1_struct_0(esk1_0))),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_71,c_0_72]),c_0_62]) ).
cnf(c_0_83,plain,
( m1_subset_1(k6_pre_topc(X1,X2),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(split_conjunct,[status(thm)],[c_0_73]) ).
cnf(c_0_84,plain,
esk51_1(X1) = X1,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_63,c_0_74]),c_0_75]) ).
fof(c_0_85,plain,
! [X1] :
( l1_pre_topc(X1)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ( v1_tsp_1(X2,X1)
<=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ~ ( r2_hidden(X3,X2)
& r2_hidden(X4,X2)
& X3 != X4
& ! [X5] :
( m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1)))
=> ~ ( v3_pre_topc(X5,X1)
& r2_hidden(X3,X5)
& ~ r2_hidden(X4,X5) ) )
& ! [X5] :
( m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1)))
=> ~ ( v3_pre_topc(X5,X1)
& ~ r2_hidden(X3,X5)
& r2_hidden(X4,X5) ) ) ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[d8_tsp_1]) ).
cnf(c_0_86,plain,
( r2_hidden(X3,X2)
| ~ r1_tarski(X1,X2)
| ~ r2_hidden(X3,X1) ),
inference(split_conjunct,[status(thm)],[c_0_76]) ).
cnf(c_0_87,plain,
( r1_tarski(k1_tops_1(X1,esk77_0),esk77_0)
| ~ l1_pre_topc(X1) ),
inference(spm,[status(thm)],[c_0_77,c_0_69]) ).
cnf(c_0_88,plain,
~ r2_hidden(X1,esk77_0),
inference(spm,[status(thm)],[c_0_78,c_0_79]) ).
fof(c_0_89,plain,
! [X1112,X1113] :
( ( ~ v1_tops_1(X1113,X1112)
| k6_pre_topc(X1112,X1113) = k2_pre_topc(X1112)
| ~ m1_subset_1(X1113,k1_zfmisc_1(u1_struct_0(X1112)))
| ~ l1_pre_topc(X1112) )
& ( k6_pre_topc(X1112,X1113) != k2_pre_topc(X1112)
| v1_tops_1(X1113,X1112)
| ~ m1_subset_1(X1113,k1_zfmisc_1(u1_struct_0(X1112)))
| ~ l1_pre_topc(X1112) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[d3_tops_1])])])]) ).
cnf(c_0_90,plain,
( v1_tops_1(X2,X1)
| k6_pre_topc(X1,X2) != u1_struct_0(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_pre_topc(X1) ),
inference(split_conjunct,[status(thm)],[c_0_80]) ).
cnf(c_0_91,negated_conjecture,
( k6_pre_topc(esk1_0,u1_struct_0(esk1_0)) = u1_struct_0(esk1_0)
| ~ r1_tarski(k6_pre_topc(esk1_0,u1_struct_0(esk1_0)),u1_struct_0(esk1_0)) ),
inference(spm,[status(thm)],[c_0_81,c_0_82]) ).
cnf(c_0_92,plain,
( r1_tarski(k6_pre_topc(X1,X2),u1_struct_0(X1))
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(spm,[status(thm)],[c_0_68,c_0_83]) ).
cnf(c_0_93,plain,
m1_subset_1(X1,k1_zfmisc_1(X1)),
inference(rw,[status(thm)],[c_0_74,c_0_84]) ).
fof(c_0_94,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v2_pre_topc(X1)
& l1_pre_topc(X1) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ~ ( v1_tsp_1(X2,X1)
& ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
=> ~ ( r1_tarski(X2,X3)
& v1_tsp_2(X3,X1) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[t9_tsp_2]) ).
fof(c_0_95,plain,
! [X882,X883,X884,X885,X890,X891] :
( ( m1_subset_1(esk16_4(X882,X883,X884,X885),k1_zfmisc_1(u1_struct_0(X882)))
| m1_subset_1(esk15_4(X882,X883,X884,X885),k1_zfmisc_1(u1_struct_0(X882)))
| ~ r2_hidden(X884,X883)
| ~ r2_hidden(X885,X883)
| X884 = X885
| ~ m1_subset_1(X885,u1_struct_0(X882))
| ~ m1_subset_1(X884,u1_struct_0(X882))
| ~ v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( v3_pre_topc(esk16_4(X882,X883,X884,X885),X882)
| m1_subset_1(esk15_4(X882,X883,X884,X885),k1_zfmisc_1(u1_struct_0(X882)))
| ~ r2_hidden(X884,X883)
| ~ r2_hidden(X885,X883)
| X884 = X885
| ~ m1_subset_1(X885,u1_struct_0(X882))
| ~ m1_subset_1(X884,u1_struct_0(X882))
| ~ v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( ~ r2_hidden(X884,esk16_4(X882,X883,X884,X885))
| m1_subset_1(esk15_4(X882,X883,X884,X885),k1_zfmisc_1(u1_struct_0(X882)))
| ~ r2_hidden(X884,X883)
| ~ r2_hidden(X885,X883)
| X884 = X885
| ~ m1_subset_1(X885,u1_struct_0(X882))
| ~ m1_subset_1(X884,u1_struct_0(X882))
| ~ v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( r2_hidden(X885,esk16_4(X882,X883,X884,X885))
| m1_subset_1(esk15_4(X882,X883,X884,X885),k1_zfmisc_1(u1_struct_0(X882)))
| ~ r2_hidden(X884,X883)
| ~ r2_hidden(X885,X883)
| X884 = X885
| ~ m1_subset_1(X885,u1_struct_0(X882))
| ~ m1_subset_1(X884,u1_struct_0(X882))
| ~ v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( m1_subset_1(esk16_4(X882,X883,X884,X885),k1_zfmisc_1(u1_struct_0(X882)))
| v3_pre_topc(esk15_4(X882,X883,X884,X885),X882)
| ~ r2_hidden(X884,X883)
| ~ r2_hidden(X885,X883)
| X884 = X885
| ~ m1_subset_1(X885,u1_struct_0(X882))
| ~ m1_subset_1(X884,u1_struct_0(X882))
| ~ v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( v3_pre_topc(esk16_4(X882,X883,X884,X885),X882)
| v3_pre_topc(esk15_4(X882,X883,X884,X885),X882)
| ~ r2_hidden(X884,X883)
| ~ r2_hidden(X885,X883)
| X884 = X885
| ~ m1_subset_1(X885,u1_struct_0(X882))
| ~ m1_subset_1(X884,u1_struct_0(X882))
| ~ v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( ~ r2_hidden(X884,esk16_4(X882,X883,X884,X885))
| v3_pre_topc(esk15_4(X882,X883,X884,X885),X882)
| ~ r2_hidden(X884,X883)
| ~ r2_hidden(X885,X883)
| X884 = X885
| ~ m1_subset_1(X885,u1_struct_0(X882))
| ~ m1_subset_1(X884,u1_struct_0(X882))
| ~ v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( r2_hidden(X885,esk16_4(X882,X883,X884,X885))
| v3_pre_topc(esk15_4(X882,X883,X884,X885),X882)
| ~ r2_hidden(X884,X883)
| ~ r2_hidden(X885,X883)
| X884 = X885
| ~ m1_subset_1(X885,u1_struct_0(X882))
| ~ m1_subset_1(X884,u1_struct_0(X882))
| ~ v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( m1_subset_1(esk16_4(X882,X883,X884,X885),k1_zfmisc_1(u1_struct_0(X882)))
| r2_hidden(X884,esk15_4(X882,X883,X884,X885))
| ~ r2_hidden(X884,X883)
| ~ r2_hidden(X885,X883)
| X884 = X885
| ~ m1_subset_1(X885,u1_struct_0(X882))
| ~ m1_subset_1(X884,u1_struct_0(X882))
| ~ v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( v3_pre_topc(esk16_4(X882,X883,X884,X885),X882)
| r2_hidden(X884,esk15_4(X882,X883,X884,X885))
| ~ r2_hidden(X884,X883)
| ~ r2_hidden(X885,X883)
| X884 = X885
| ~ m1_subset_1(X885,u1_struct_0(X882))
| ~ m1_subset_1(X884,u1_struct_0(X882))
| ~ v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( ~ r2_hidden(X884,esk16_4(X882,X883,X884,X885))
| r2_hidden(X884,esk15_4(X882,X883,X884,X885))
| ~ r2_hidden(X884,X883)
| ~ r2_hidden(X885,X883)
| X884 = X885
| ~ m1_subset_1(X885,u1_struct_0(X882))
| ~ m1_subset_1(X884,u1_struct_0(X882))
| ~ v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( r2_hidden(X885,esk16_4(X882,X883,X884,X885))
| r2_hidden(X884,esk15_4(X882,X883,X884,X885))
| ~ r2_hidden(X884,X883)
| ~ r2_hidden(X885,X883)
| X884 = X885
| ~ m1_subset_1(X885,u1_struct_0(X882))
| ~ m1_subset_1(X884,u1_struct_0(X882))
| ~ v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( m1_subset_1(esk16_4(X882,X883,X884,X885),k1_zfmisc_1(u1_struct_0(X882)))
| ~ r2_hidden(X885,esk15_4(X882,X883,X884,X885))
| ~ r2_hidden(X884,X883)
| ~ r2_hidden(X885,X883)
| X884 = X885
| ~ m1_subset_1(X885,u1_struct_0(X882))
| ~ m1_subset_1(X884,u1_struct_0(X882))
| ~ v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( v3_pre_topc(esk16_4(X882,X883,X884,X885),X882)
| ~ r2_hidden(X885,esk15_4(X882,X883,X884,X885))
| ~ r2_hidden(X884,X883)
| ~ r2_hidden(X885,X883)
| X884 = X885
| ~ m1_subset_1(X885,u1_struct_0(X882))
| ~ m1_subset_1(X884,u1_struct_0(X882))
| ~ v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( ~ r2_hidden(X884,esk16_4(X882,X883,X884,X885))
| ~ r2_hidden(X885,esk15_4(X882,X883,X884,X885))
| ~ r2_hidden(X884,X883)
| ~ r2_hidden(X885,X883)
| X884 = X885
| ~ m1_subset_1(X885,u1_struct_0(X882))
| ~ m1_subset_1(X884,u1_struct_0(X882))
| ~ v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( r2_hidden(X885,esk16_4(X882,X883,X884,X885))
| ~ r2_hidden(X885,esk15_4(X882,X883,X884,X885))
| ~ r2_hidden(X884,X883)
| ~ r2_hidden(X885,X883)
| X884 = X885
| ~ m1_subset_1(X885,u1_struct_0(X882))
| ~ m1_subset_1(X884,u1_struct_0(X882))
| ~ v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( m1_subset_1(esk17_2(X882,X883),u1_struct_0(X882))
| v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( m1_subset_1(esk18_2(X882,X883),u1_struct_0(X882))
| v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( r2_hidden(esk17_2(X882,X883),X883)
| v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( r2_hidden(esk18_2(X882,X883),X883)
| v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( esk17_2(X882,X883) != esk18_2(X882,X883)
| v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( ~ m1_subset_1(X890,k1_zfmisc_1(u1_struct_0(X882)))
| ~ v3_pre_topc(X890,X882)
| ~ r2_hidden(esk17_2(X882,X883),X890)
| r2_hidden(esk18_2(X882,X883),X890)
| v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) )
& ( ~ m1_subset_1(X891,k1_zfmisc_1(u1_struct_0(X882)))
| ~ v3_pre_topc(X891,X882)
| r2_hidden(esk17_2(X882,X883),X891)
| ~ r2_hidden(esk18_2(X882,X883),X891)
| v1_tsp_1(X883,X882)
| ~ m1_subset_1(X883,k1_zfmisc_1(u1_struct_0(X882)))
| ~ l1_pre_topc(X882) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_85])])])])]) ).
cnf(c_0_96,plain,
( ~ l1_pre_topc(X1)
| ~ r2_hidden(X2,k1_tops_1(X1,esk77_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_87]),c_0_88]) ).
cnf(c_0_97,plain,
( k6_pre_topc(X2,X1) = k2_pre_topc(X2)
| ~ v1_tops_1(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X2)))
| ~ l1_pre_topc(X2) ),
inference(split_conjunct,[status(thm)],[c_0_89]) ).
cnf(c_0_98,plain,
( v1_tops_1(k6_pre_topc(X1,X2),X1)
| k6_pre_topc(X1,k6_pre_topc(X1,X2)) != u1_struct_0(X1)
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(spm,[status(thm)],[c_0_90,c_0_83]) ).
cnf(c_0_99,negated_conjecture,
k6_pre_topc(esk1_0,u1_struct_0(esk1_0)) = u1_struct_0(esk1_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91,c_0_92]),c_0_32]),c_0_93])]) ).
fof(c_0_100,plain,
! [X785,X786] :
( ( m1_subset_1(esk3_2(X785,X786),k1_zfmisc_1(u1_struct_0(X785)))
| ~ v1_tsp_1(X786,X785)
| ~ m1_subset_1(X786,k1_zfmisc_1(u1_struct_0(X785)))
| v3_struct_0(X785)
| ~ v2_pre_topc(X785)
| ~ l1_pre_topc(X785) )
& ( r1_tarski(X786,esk3_2(X785,X786))
| ~ v1_tsp_1(X786,X785)
| ~ m1_subset_1(X786,k1_zfmisc_1(u1_struct_0(X785)))
| v3_struct_0(X785)
| ~ v2_pre_topc(X785)
| ~ l1_pre_topc(X785) )
& ( v1_tsp_2(esk3_2(X785,X786),X785)
| ~ v1_tsp_1(X786,X785)
| ~ m1_subset_1(X786,k1_zfmisc_1(u1_struct_0(X785)))
| v3_struct_0(X785)
| ~ v2_pre_topc(X785)
| ~ l1_pre_topc(X785) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_94])])])])]) ).
cnf(c_0_101,plain,
( r2_hidden(esk17_2(X1,X2),X2)
| v1_tsp_1(X2,X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_pre_topc(X1) ),
inference(split_conjunct,[status(thm)],[c_0_95]) ).
fof(c_0_102,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v2_pre_topc(X1)
& l1_pre_topc(X1) )
=> ! [X2] :
( ( v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
=> v1_tsp_1(X2,X1) ) ),
inference(fof_simplification,[status(thm)],[t13_tsp_1]) ).
cnf(c_0_103,plain,
( v1_xboole_0(k1_tops_1(X1,esk77_0))
| ~ l1_pre_topc(X1) ),
inference(spm,[status(thm)],[c_0_96,c_0_49]) ).
cnf(c_0_104,plain,
( k6_pre_topc(X1,u1_struct_0(X1)) = k2_pre_topc(X1)
| ~ v1_tops_1(u1_struct_0(X1),X1)
| ~ l1_pre_topc(X1) ),
inference(spm,[status(thm)],[c_0_97,c_0_93]) ).
cnf(c_0_105,negated_conjecture,
v1_tops_1(u1_struct_0(esk1_0),esk1_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_98,c_0_99]),c_0_99]),c_0_32]),c_0_93])]) ).
cnf(c_0_106,plain,
( m1_subset_1(esk3_2(X1,X2),k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v1_tsp_1(X2,X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) ),
inference(split_conjunct,[status(thm)],[c_0_100]) ).
cnf(c_0_107,plain,
( v1_tsp_1(esk77_0,X1)
| ~ l1_pre_topc(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_101,c_0_69]),c_0_88]) ).
fof(c_0_108,plain,
! [X942,X943] :
( v3_struct_0(X942)
| ~ v2_pre_topc(X942)
| ~ l1_pre_topc(X942)
| ~ v1_xboole_0(X943)
| ~ m1_subset_1(X943,k1_zfmisc_1(u1_struct_0(X942)))
| v1_tsp_1(X943,X942) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_102])])]) ).
fof(c_0_109,plain,
! [X1467,X1468] :
( ~ l1_pre_topc(X1467)
| ~ m1_subset_1(X1468,k1_zfmisc_1(u1_struct_0(X1467)))
| m1_subset_1(k1_tops_1(X1467,X1468),k1_zfmisc_1(u1_struct_0(X1467))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_k1_tops_1])]) ).
cnf(c_0_110,plain,
( X1 = k1_tops_1(X2,esk77_0)
| ~ l1_pre_topc(X2)
| ~ v1_xboole_0(X1) ),
inference(spm,[status(thm)],[c_0_43,c_0_103]) ).
cnf(c_0_111,negated_conjecture,
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk1_0)))
| ~ v1_tsp_2(X1,esk1_0) ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_112,negated_conjecture,
u1_struct_0(esk1_0) = k2_pre_topc(esk1_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_104,c_0_105]),c_0_99]),c_0_32])]) ).
cnf(c_0_113,plain,
( v3_struct_0(X1)
| m1_subset_1(esk3_2(X1,esk77_0),k1_zfmisc_1(u1_struct_0(X1)))
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_106,c_0_69]),c_0_107]) ).
cnf(c_0_114,plain,
( v3_struct_0(X1)
| v1_tsp_1(X2,X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| ~ v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(split_conjunct,[status(thm)],[c_0_108]) ).
cnf(c_0_115,plain,
( m1_subset_1(k1_tops_1(X1,X2),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(split_conjunct,[status(thm)],[c_0_109]) ).
cnf(c_0_116,negated_conjecture,
( X1 = k1_tops_1(esk1_0,esk77_0)
| ~ v1_xboole_0(X1) ),
inference(spm,[status(thm)],[c_0_110,c_0_32]) ).
cnf(c_0_117,negated_conjecture,
( ~ v1_tsp_2(X1,esk1_0)
| ~ m1_subset_1(X1,k1_zfmisc_1(k2_pre_topc(esk1_0))) ),
inference(rw,[status(thm)],[c_0_111,c_0_112]) ).
cnf(c_0_118,negated_conjecture,
m1_subset_1(esk3_2(esk1_0,esk77_0),k1_zfmisc_1(k2_pre_topc(esk1_0))),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_113,c_0_31]),c_0_112]),c_0_32])]),c_0_33]) ).
cnf(c_0_119,plain,
( v1_tsp_2(esk3_2(X1,X2),X1)
| v3_struct_0(X1)
| ~ v1_tsp_1(X2,X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1) ),
inference(split_conjunct,[status(thm)],[c_0_100]) ).
cnf(c_0_120,plain,
( v1_tsp_1(k1_tops_1(X1,X2),X1)
| v3_struct_0(X1)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_xboole_0(k1_tops_1(X1,X2)) ),
inference(spm,[status(thm)],[c_0_114,c_0_115]) ).
cnf(c_0_121,negated_conjecture,
k1_tops_1(esk1_0,esk77_0) = esk77_0,
inference(spm,[status(thm)],[c_0_116,c_0_44]) ).
cnf(c_0_122,negated_conjecture,
~ v1_tsp_2(esk3_2(esk1_0,esk77_0),esk1_0),
inference(spm,[status(thm)],[c_0_117,c_0_118]) ).
cnf(c_0_123,negated_conjecture,
( v1_tsp_2(esk3_2(esk1_0,X1),esk1_0)
| ~ v1_tsp_1(X1,esk1_0)
| ~ m1_subset_1(X1,k1_zfmisc_1(k2_pre_topc(esk1_0))) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_119,c_0_112]),c_0_31]),c_0_32])]),c_0_33]) ).
cnf(c_0_124,negated_conjecture,
v1_tsp_1(esk77_0,esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_120,c_0_121]),c_0_31]),c_0_32]),c_0_69]),c_0_44])]),c_0_33]) ).
cnf(c_0_125,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_122,c_0_123]),c_0_124]),c_0_69])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : TOP028+3 : TPTP v9.2.1. Released v3.4.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.34 % Computer : n027.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Tue May 5 09:55:51 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.35 % start to proof: theBenchmark
% 48.15/31.21 % Version : CSE_E---1.7
% 48.15/31.21 % Problem : theBenchmark.p
% 48.15/31.21 % SZS status Theorem for theBenchmark.p
% 48.15/31.21 % SZS output start CNFRefutation
% See solution above
% 48.25/31.36 % Total time : 25.384s
%------------------------------------------------------------------------------