%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : TOP024+2 : TPTP v9.2.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n005.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:36 PM UTC 2026
% Result : Theorem 195.07s 164.06s
% Output : CNFRefutation 195.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 14
% Syntax : Number of formulae : 76 ( 30 unt; 0 def)
% Number of atoms : 264 ( 67 equ)
% Maximal formula atoms : 19 ( 3 avg)
% Number of connectives : 311 ( 123 ~; 114 |; 37 &)
% ( 4 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 3 con; 0-2 aty)
% Number of variables : 99 ( 4 sgn 56 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d5_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_2(X2,X1)
<=> ( v1_tsp_1(X2,X1)
& k3_tex_4(X1,X2) = u1_struct_0(X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_tsp_2) ).
fof(t7_pcomps_1,axiom,
! [X1] : u1_pre_topc(k2_pcomps_1(X1)) = k1_pcomps_1(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+301.ax',t7_pcomps_1) ).
fof(redefinition_k1_pcomps_1,axiom,
! [X1] : k1_pcomps_1(X1) = k1_zfmisc_1(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+301.ax',redefinition_k1_pcomps_1) ).
fof(t2_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)
=> v1_tops_1(X2,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_tsp_2) ).
fof(dt_k3_tex_4,axiom,
! [X1,X2] :
( ( ~ v3_struct_0(X1)
& l1_pre_topc(X1)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
=> m1_subset_1(k3_tex_4(X1,X2),k1_zfmisc_1(u1_struct_0(X1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+405.ax',dt_k3_tex_4) ).
fof(t2_tops_3,axiom,
! [X1] :
( l1_pre_topc(X1)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ( ( X2 = k2_pre_topc(X1)
=> k3_subset_1(u1_struct_0(X1),X2) = k1_pre_topc(X1) )
& ( k3_subset_1(u1_struct_0(X1),X2) = k1_pre_topc(X1)
=> X2 = k2_pre_topc(X1) )
& ( X2 = u1_struct_0(X1)
=> k3_subset_1(u1_struct_0(X1),X2) = k1_xboole_0 )
& ( k3_subset_1(u1_struct_0(X1),X2) = k1_xboole_0
=> X2 = u1_struct_0(X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+370.ax',t2_tops_3) ).
fof(t41_pre_topc,axiom,
! [X1] :
( l1_pre_topc(X1)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ~ ( X2 != k1_pre_topc(X1)
& ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ~ r2_hidden(X3,X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+206.ax',t41_pre_topc) ).
fof(t7_ordinal1,axiom,
! [X1,X2] :
~ ( r2_hidden(X1,X2)
& r1_tarski(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+14.ax',t7_ordinal1) ).
fof(t2_xboole_1,axiom,
! [X1] : r1_tarski(k1_xboole_0,X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+4.ax',t2_xboole_1) ).
fof(t4_subset_1,axiom,
! [X1] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+7.ax',t4_subset_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/sandbox/benchmark/Axioms/SET007/SET007+207.ax',d3_tops_1) ).
fof(t64_tex_4,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)))
=> k6_pre_topc(X1,k3_tex_4(X1,X2)) = k6_pre_topc(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+405.ax',t64_tex_4) ).
fof(fc9_tops_1,axiom,
! [X1] :
( l1_pre_topc(X1)
=> v1_tops_1(k2_pre_topc(X1),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+207.ax',fc9_tops_1) ).
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/sandbox/benchmark/Axioms/SET007/SET007+370.ax',d2_tops_3) ).
fof(c_0_14,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_2(X2,X1)
<=> ( v1_tsp_1(X2,X1)
& k3_tex_4(X1,X2) = u1_struct_0(X1) ) ) ) ),
inference(fof_simplification,[status(thm)],[d5_tsp_2]) ).
fof(c_0_15,plain,
! [X14622] : u1_pre_topc(k2_pcomps_1(X14622)) = k1_pcomps_1(X14622),
inference(variable_rename,[status(thm)],[t7_pcomps_1]) ).
fof(c_0_16,plain,
! [X14624] : k1_pcomps_1(X14624) = k1_zfmisc_1(X14624),
inference(variable_rename,[status(thm)],[redefinition_k1_pcomps_1]) ).
fof(c_0_17,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)
=> v1_tops_1(X2,X1) ) ) ),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[t2_tsp_2])]) ).
fof(c_0_18,plain,
! [X1,X2] :
( ( ~ v3_struct_0(X1)
& l1_pre_topc(X1)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
=> m1_subset_1(k3_tex_4(X1,X2),k1_zfmisc_1(u1_struct_0(X1))) ),
inference(fof_simplification,[status(thm)],[dt_k3_tex_4]) ).
fof(c_0_19,plain,
! [X7707,X7708] :
( ( v1_tsp_1(X7708,X7707)
| ~ v1_tsp_2(X7708,X7707)
| ~ m1_subset_1(X7708,k1_zfmisc_1(u1_struct_0(X7707)))
| v3_struct_0(X7707)
| ~ v2_pre_topc(X7707)
| ~ l1_pre_topc(X7707) )
& ( k3_tex_4(X7707,X7708) = u1_struct_0(X7707)
| ~ v1_tsp_2(X7708,X7707)
| ~ m1_subset_1(X7708,k1_zfmisc_1(u1_struct_0(X7707)))
| v3_struct_0(X7707)
| ~ v2_pre_topc(X7707)
| ~ l1_pre_topc(X7707) )
& ( ~ v1_tsp_1(X7708,X7707)
| k3_tex_4(X7707,X7708) != u1_struct_0(X7707)
| v1_tsp_2(X7708,X7707)
| ~ m1_subset_1(X7708,k1_zfmisc_1(u1_struct_0(X7707)))
| v3_struct_0(X7707)
| ~ v2_pre_topc(X7707)
| ~ l1_pre_topc(X7707) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_14])])])]) ).
cnf(c_0_20,plain,
u1_pre_topc(k2_pcomps_1(X1)) = k1_pcomps_1(X1),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
cnf(c_0_21,plain,
k1_pcomps_1(X1) = k1_zfmisc_1(X1),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
fof(c_0_22,negated_conjecture,
( ~ v3_struct_0(esk1_0)
& v2_pre_topc(esk1_0)
& l1_pre_topc(esk1_0)
& m1_subset_1(esk2_0,k1_zfmisc_1(u1_struct_0(esk1_0)))
& v1_tsp_2(esk2_0,esk1_0)
& ~ v1_tops_1(esk2_0,esk1_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_17])])]) ).
fof(c_0_23,plain,
! [X10513,X10514] :
( v3_struct_0(X10513)
| ~ l1_pre_topc(X10513)
| ~ m1_subset_1(X10514,k1_zfmisc_1(u1_struct_0(X10513)))
| m1_subset_1(k3_tex_4(X10513,X10514),k1_zfmisc_1(u1_struct_0(X10513))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_18])]) ).
cnf(c_0_24,plain,
( k3_tex_4(X1,X2) = u1_struct_0(X1)
| v3_struct_0(X1)
| ~ v1_tsp_2(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_19]) ).
cnf(c_0_25,plain,
u1_pre_topc(k2_pcomps_1(X1)) = k1_zfmisc_1(X1),
inference(rw,[status(thm)],[c_0_20,c_0_21]) ).
cnf(c_0_26,negated_conjecture,
m1_subset_1(esk2_0,k1_zfmisc_1(u1_struct_0(esk1_0))),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
fof(c_0_27,plain,
! [X7924,X7925] :
( ( X7925 != k2_pre_topc(X7924)
| k3_subset_1(u1_struct_0(X7924),X7925) = k1_pre_topc(X7924)
| ~ m1_subset_1(X7925,k1_zfmisc_1(u1_struct_0(X7924)))
| ~ l1_pre_topc(X7924) )
& ( k3_subset_1(u1_struct_0(X7924),X7925) != k1_pre_topc(X7924)
| X7925 = k2_pre_topc(X7924)
| ~ m1_subset_1(X7925,k1_zfmisc_1(u1_struct_0(X7924)))
| ~ l1_pre_topc(X7924) )
& ( X7925 != u1_struct_0(X7924)
| k3_subset_1(u1_struct_0(X7924),X7925) = k1_xboole_0
| ~ m1_subset_1(X7925,k1_zfmisc_1(u1_struct_0(X7924)))
| ~ l1_pre_topc(X7924) )
& ( k3_subset_1(u1_struct_0(X7924),X7925) != k1_xboole_0
| X7925 = u1_struct_0(X7924)
| ~ m1_subset_1(X7925,k1_zfmisc_1(u1_struct_0(X7924)))
| ~ l1_pre_topc(X7924) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t2_tops_3])])])]) ).
cnf(c_0_28,plain,
( v3_struct_0(X1)
| m1_subset_1(k3_tex_4(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_23]) ).
cnf(c_0_29,plain,
( k3_tex_4(X1,X2) = u1_struct_0(X1)
| v3_struct_0(X1)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ v1_tsp_2(X2,X1)
| ~ m1_subset_1(X2,u1_pre_topc(k2_pcomps_1(u1_struct_0(X1)))) ),
inference(rw,[status(thm)],[c_0_24,c_0_25]) ).
cnf(c_0_30,negated_conjecture,
m1_subset_1(esk2_0,u1_pre_topc(k2_pcomps_1(u1_struct_0(esk1_0)))),
inference(rw,[status(thm)],[c_0_26,c_0_25]) ).
cnf(c_0_31,negated_conjecture,
v1_tsp_2(esk2_0,esk1_0),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_32,negated_conjecture,
v2_pre_topc(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_33,negated_conjecture,
l1_pre_topc(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_34,negated_conjecture,
~ v3_struct_0(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
fof(c_0_35,plain,
! [X1] :
( l1_pre_topc(X1)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ~ ( X2 != k1_pre_topc(X1)
& ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ~ r2_hidden(X3,X2) ) ) ) ),
inference(fof_simplification,[status(thm)],[t41_pre_topc]) ).
cnf(c_0_36,plain,
( k3_subset_1(u1_struct_0(X2),X1) = k1_xboole_0
| X1 != u1_struct_0(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X2)))
| ~ l1_pre_topc(X2) ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_37,plain,
( v3_struct_0(X1)
| m1_subset_1(k3_tex_4(X1,X2),u1_pre_topc(k2_pcomps_1(u1_struct_0(X1))))
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(X2,u1_pre_topc(k2_pcomps_1(u1_struct_0(X1)))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_28,c_0_25]),c_0_25]) ).
cnf(c_0_38,negated_conjecture,
k3_tex_4(esk1_0,esk2_0) = u1_struct_0(esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29,c_0_30]),c_0_31]),c_0_32]),c_0_33])]),c_0_34]) ).
fof(c_0_39,plain,
! [X8620,X8621] :
( ~ r2_hidden(X8620,X8621)
| ~ r1_tarski(X8621,X8620) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t7_ordinal1])]) ).
fof(c_0_40,plain,
! [X8376] : r1_tarski(k1_xboole_0,X8376),
inference(variable_rename,[status(thm)],[t2_xboole_1]) ).
fof(c_0_41,plain,
! [X11175,X11176] :
( ( m1_subset_1(esk428_2(X11175,X11176),u1_struct_0(X11175))
| X11176 = k1_pre_topc(X11175)
| ~ m1_subset_1(X11176,k1_zfmisc_1(u1_struct_0(X11175)))
| ~ l1_pre_topc(X11175) )
& ( r2_hidden(esk428_2(X11175,X11176),X11176)
| X11176 = k1_pre_topc(X11175)
| ~ m1_subset_1(X11176,k1_zfmisc_1(u1_struct_0(X11175)))
| ~ l1_pre_topc(X11175) ) ),
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_35])])])])]) ).
fof(c_0_42,plain,
! [X7715] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(X7715)),
inference(variable_rename,[status(thm)],[t4_subset_1]) ).
cnf(c_0_43,plain,
( X2 = k2_pre_topc(X1)
| k3_subset_1(u1_struct_0(X1),X2) != k1_pre_topc(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_pre_topc(X1) ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_44,plain,
( k3_subset_1(u1_struct_0(X2),X1) = k1_xboole_0
| X1 != u1_struct_0(X2)
| ~ l1_pre_topc(X2)
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(u1_struct_0(X2)))) ),
inference(rw,[status(thm)],[c_0_36,c_0_25]) ).
cnf(c_0_45,negated_conjecture,
m1_subset_1(u1_struct_0(esk1_0),u1_pre_topc(k2_pcomps_1(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_37,c_0_38]),c_0_33]),c_0_30])]),c_0_34]) ).
cnf(c_0_46,plain,
( ~ r2_hidden(X1,X2)
| ~ r1_tarski(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_47,plain,
r1_tarski(k1_xboole_0,X1),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_48,plain,
( r2_hidden(esk428_2(X1,X2),X2)
| X2 = k1_pre_topc(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_pre_topc(X1) ),
inference(split_conjunct,[status(thm)],[c_0_41]) ).
cnf(c_0_49,plain,
m1_subset_1(k1_xboole_0,k1_zfmisc_1(X1)),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
fof(c_0_50,plain,
! [X7577,X7578] :
( ( ~ v1_tops_1(X7578,X7577)
| k6_pre_topc(X7577,X7578) = k2_pre_topc(X7577)
| ~ m1_subset_1(X7578,k1_zfmisc_1(u1_struct_0(X7577)))
| ~ l1_pre_topc(X7577) )
& ( k6_pre_topc(X7577,X7578) != k2_pre_topc(X7577)
| v1_tops_1(X7578,X7577)
| ~ m1_subset_1(X7578,k1_zfmisc_1(u1_struct_0(X7577)))
| ~ l1_pre_topc(X7577) ) ),
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_51,plain,
( X2 = k2_pre_topc(X1)
| k3_subset_1(u1_struct_0(X1),X2) != k1_pre_topc(X1)
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(X2,u1_pre_topc(k2_pcomps_1(u1_struct_0(X1)))) ),
inference(rw,[status(thm)],[c_0_43,c_0_25]) ).
cnf(c_0_52,negated_conjecture,
k3_subset_1(u1_struct_0(esk1_0),u1_struct_0(esk1_0)) = k1_xboole_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44,c_0_45]),c_0_33])]) ).
cnf(c_0_53,plain,
~ r2_hidden(X1,k1_xboole_0),
inference(spm,[status(thm)],[c_0_46,c_0_47]) ).
cnf(c_0_54,plain,
( X2 = k1_pre_topc(X1)
| r2_hidden(esk428_2(X1,X2),X2)
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(X2,u1_pre_topc(k2_pcomps_1(u1_struct_0(X1)))) ),
inference(rw,[status(thm)],[c_0_48,c_0_25]) ).
cnf(c_0_55,plain,
m1_subset_1(k1_xboole_0,u1_pre_topc(k2_pcomps_1(X1))),
inference(rw,[status(thm)],[c_0_49,c_0_25]) ).
fof(c_0_56,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)))
=> k6_pre_topc(X1,k3_tex_4(X1,X2)) = k6_pre_topc(X1,X2) ) ),
inference(fof_simplification,[status(thm)],[t64_tex_4]) ).
cnf(c_0_57,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_50]) ).
fof(c_0_58,plain,
! [X7574] :
( ~ l1_pre_topc(X7574)
| v1_tops_1(k2_pre_topc(X7574),X7574) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fc9_tops_1])]) ).
cnf(c_0_59,negated_conjecture,
( k2_pre_topc(esk1_0) = u1_struct_0(esk1_0)
| k1_pre_topc(esk1_0) != k1_xboole_0 ),
inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_45]),c_0_33])]),c_0_52]) ).
cnf(c_0_60,plain,
( k1_pre_topc(X1) = k1_xboole_0
| ~ l1_pre_topc(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_54]),c_0_55])]) ).
fof(c_0_61,plain,
! [X7596,X7597] :
( ( ~ v1_tops_1(X7597,X7596)
| k6_pre_topc(X7596,X7597) = u1_struct_0(X7596)
| ~ m1_subset_1(X7597,k1_zfmisc_1(u1_struct_0(X7596)))
| ~ l1_pre_topc(X7596) )
& ( k6_pre_topc(X7596,X7597) != u1_struct_0(X7596)
| v1_tops_1(X7597,X7596)
| ~ m1_subset_1(X7597,k1_zfmisc_1(u1_struct_0(X7596)))
| ~ l1_pre_topc(X7596) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[d2_tops_3])])])]) ).
fof(c_0_62,plain,
! [X8326,X8327] :
( v3_struct_0(X8326)
| ~ v2_pre_topc(X8326)
| ~ l1_pre_topc(X8326)
| ~ m1_subset_1(X8327,k1_zfmisc_1(u1_struct_0(X8326)))
| k6_pre_topc(X8326,k3_tex_4(X8326,X8327)) = k6_pre_topc(X8326,X8327) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_56])])]) ).
cnf(c_0_63,plain,
( k6_pre_topc(X2,X1) = k2_pre_topc(X2)
| ~ l1_pre_topc(X2)
| ~ v1_tops_1(X1,X2)
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(u1_struct_0(X2)))) ),
inference(rw,[status(thm)],[c_0_57,c_0_25]) ).
cnf(c_0_64,plain,
( v1_tops_1(k2_pre_topc(X1),X1)
| ~ l1_pre_topc(X1) ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
cnf(c_0_65,negated_conjecture,
k2_pre_topc(esk1_0) = u1_struct_0(esk1_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59,c_0_60]),c_0_33])]) ).
cnf(c_0_66,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_61]) ).
cnf(c_0_67,plain,
( v3_struct_0(X1)
| k6_pre_topc(X1,k3_tex_4(X1,X2)) = k6_pre_topc(X1,X2)
| ~ v2_pre_topc(X1)
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(split_conjunct,[status(thm)],[c_0_62]) ).
cnf(c_0_68,negated_conjecture,
( k6_pre_topc(esk1_0,u1_struct_0(esk1_0)) = k2_pre_topc(esk1_0)
| ~ v1_tops_1(u1_struct_0(esk1_0),esk1_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63,c_0_45]),c_0_33])]) ).
cnf(c_0_69,negated_conjecture,
v1_tops_1(u1_struct_0(esk1_0),esk1_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_64,c_0_65]),c_0_33])]) ).
cnf(c_0_70,plain,
( v1_tops_1(X2,X1)
| k6_pre_topc(X1,X2) != u1_struct_0(X1)
| ~ l1_pre_topc(X1)
| ~ m1_subset_1(X2,u1_pre_topc(k2_pcomps_1(u1_struct_0(X1)))) ),
inference(rw,[status(thm)],[c_0_66,c_0_25]) ).
cnf(c_0_71,negated_conjecture,
~ v1_tops_1(esk2_0,esk1_0),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_72,plain,
( k6_pre_topc(X1,k3_tex_4(X1,X2)) = k6_pre_topc(X1,X2)
| v3_struct_0(X1)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ m1_subset_1(X2,u1_pre_topc(k2_pcomps_1(u1_struct_0(X1)))) ),
inference(rw,[status(thm)],[c_0_67,c_0_25]) ).
cnf(c_0_73,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)],[c_0_68,c_0_65]),c_0_69])]) ).
cnf(c_0_74,negated_conjecture,
k6_pre_topc(esk1_0,esk2_0) != u1_struct_0(esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_70,c_0_30]),c_0_33])]),c_0_71]) ).
cnf(c_0_75,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72,c_0_30]),c_0_32]),c_0_33])]),c_0_34]),c_0_38]),c_0_73]),c_0_74]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : TOP024+2 : TPTP v9.2.1. Released v3.4.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.32 % Computer : n005.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Tue May 5 09:54:46 EDT 2026
% 0.14/0.32 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 195.07/164.06 % Version : CSE_E---1.7
% 195.07/164.06 % Problem : theBenchmark.p
% 195.07/164.06 % SZS status Theorem for theBenchmark.p
% 195.07/164.06 % SZS output start CNFRefutation
% See solution above
% 195.24/164.28 % Total time : 155.235s
%------------------------------------------------------------------------------