%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET861-2 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:10:51 PM UTC 2026
% Result : Unsatisfiable 30.77s 4.41s
% Output : CNFRefutation 30.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 23
% Syntax : Number of formulae : 100 ( 11 unt; 8 def)
% Number of atoms : 357 ( 8 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 462 ( 205 ~; 249 |; 0 &)
% ( 8 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 9 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 3 con; 0-3 aty)
% Number of variables : 248 ( 248 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [V_B,V_A,T_a] :
( V_A = V_B
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_B,V_A,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [V_c,V_A,T_a,V_B] :
( c_in(V_c,V_B,T_a)
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_in(V_c,V_A,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [V_A,V_B,T_a] :
( c_lessequals(V_A,V_B,tc_set(T_a))
| c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_A,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [V_A,V_B,T_a] :
( c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_B,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [V_z,V_S,T_a,V_c] :
( c_in(c_union(c_insert(V_z,c_emptyset,tc_set(T_a)),V_c,tc_set(T_a)),c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(T_a)))
| c_in(c_Zorn_Ochain__extend__1(V_c,V_z,T_a),V_c,tc_set(T_a))
| ~ c_in(V_c,c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_z,V_S,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [V_z,V_S,T_a,V_c] :
( c_in(c_union(c_insert(V_z,c_emptyset,tc_set(T_a)),V_c,tc_set(T_a)),c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_lessequals(c_Zorn_Ochain__extend__1(V_c,V_z,T_a),V_z,tc_set(T_a))
| ~ c_in(V_c,c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_z,V_S,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [V_S,T_a] : c_in(c_Zorn_OHausdorff__1(V_S,T_a),c_Zorn_Omaxchain(V_S,T_a),tc_set(tc_set(T_a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [V_S,T_a] : c_lessequals(c_Zorn_Omaxchain(V_S,T_a),c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(tc_set(T_a)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [V_z,V_x,T_a,V_c,V_S,V_y] :
( c_in(c_Zorn_Omaxchain__super__lemma__1(V_c,V_y,T_a),V_c,tc_set(T_a))
| c_in(V_z,V_y,T_a)
| ~ c_in(c_union(c_insert(V_x,c_emptyset,tc_set(T_a)),V_c,tc_set(T_a)),c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_c,c_Zorn_Omaxchain(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_z,V_x,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [V_z,V_x,T_a,V_c,V_S,V_y] :
( c_in(V_z,V_y,T_a)
| ~ c_lessequals(c_Zorn_Omaxchain__super__lemma__1(V_c,V_y,T_a),V_y,tc_set(T_a))
| ~ c_in(c_union(c_insert(V_x,c_emptyset,tc_set(T_a)),V_c,tc_set(T_a)),c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_c,c_Zorn_Omaxchain(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_z,V_x,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,negated_conjecture,
! [V_U] :
( ~ c_in(V_U,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))
| c_in(v_x(V_U),v_S,tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,negated_conjecture,
! [V_U] :
( ~ c_in(V_U,v_S,tc_set(t_a))
| c_in(v_xa(V_U),v_S,tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,negated_conjecture,
! [V_U] :
( ~ c_in(V_U,v_S,tc_set(t_a))
| c_lessequals(V_U,v_xa(V_U),tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
! [V_U] :
( ~ c_in(V_U,v_S,tc_set(t_a))
| V_U != v_xa(V_U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
! [V_V,V_U] :
( ~ c_in(V_U,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))
| ~ c_in(V_V,V_U,tc_set(t_a))
| c_lessequals(V_V,v_x(V_U),tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,plain,
! [V_B,V_A] :
( V_A = V_B
| ! [T_a] :
( ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_B,V_A,tc_set(T_a)) ) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f17,plain,
! [X0,X1,X2] :
( X1 = X0
| ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f18,plain,
! [V_c,T_a,V_B] :
( c_in(V_c,V_B,T_a)
| ! [V_A] :
( ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_in(V_c,V_A,T_a) ) ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f19,plain,
! [X0,X1,X2,X3] :
( c_in(X0,X3,X2)
| ~ c_lessequals(X1,X3,tc_set(X2))
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f20,plain,
! [X0,X1,X2] :
( c_lessequals(X0,X1,tc_set(X2))
| c_in(c_Main_OsubsetI__1(X0,X1,X2),X0,X2) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f21,plain,
! [X0,X1,X2] :
( c_lessequals(X0,X1,tc_set(X2))
| ~ c_in(c_Main_OsubsetI__1(X0,X1,X2),X1,X2) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f22,plain,
! [X0,X1,X2,X3] :
( c_in(c_union(c_insert(X0,c_emptyset,tc_set(X2)),X3,tc_set(X2)),c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2)))
| c_in(c_Zorn_Ochain__extend__1(X3,X0,X2),X3,tc_set(X2))
| ~ c_in(X3,c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f23,plain,
! [X0,X1,X2,X3] :
( c_in(c_union(c_insert(X0,c_emptyset,tc_set(X2)),X3,tc_set(X2)),c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2)))
| ~ c_lessequals(c_Zorn_Ochain__extend__1(X3,X0,X2),X0,tc_set(X2))
| ~ c_in(X3,c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f24,plain,
! [X0,X1] : c_in(c_Zorn_OHausdorff__1(X0,X1),c_Zorn_Omaxchain(X0,X1),tc_set(tc_set(X1))),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f25,plain,
! [X0,X1] : c_lessequals(c_Zorn_Omaxchain(X0,X1),c_Zorn_Ochain(X0,X1),tc_set(tc_set(tc_set(X1)))),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f26,plain,
! [T_a,V_c,V_y] :
( c_in(c_Zorn_Omaxchain__super__lemma__1(V_c,V_y,T_a),V_c,tc_set(T_a))
| ! [V_z] :
( c_in(V_z,V_y,T_a)
| ! [V_x,V_S] :
( ~ c_in(c_union(c_insert(V_x,c_emptyset,tc_set(T_a)),V_c,tc_set(T_a)),c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_c,c_Zorn_Omaxchain(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_z,V_x,T_a) ) ) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f27,plain,
! [X0,X1,X2,X3,X4,X5] :
( c_in(c_Zorn_Omaxchain__super__lemma__1(X3,X5,X2),X3,tc_set(X2))
| c_in(X0,X5,X2)
| ~ c_in(c_union(c_insert(X1,c_emptyset,tc_set(X2)),X3,tc_set(X2)),c_Zorn_Ochain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(X3,c_Zorn_Omaxchain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f28,plain,
! [V_z,T_a,V_y] :
( c_in(V_z,V_y,T_a)
| ! [V_c] :
( ~ c_lessequals(c_Zorn_Omaxchain__super__lemma__1(V_c,V_y,T_a),V_y,tc_set(T_a))
| ! [V_x,V_S] :
( ~ c_in(c_union(c_insert(V_x,c_emptyset,tc_set(T_a)),V_c,tc_set(T_a)),c_Zorn_Ochain(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_c,c_Zorn_Omaxchain(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_z,V_x,T_a) ) ) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f29,plain,
! [X0,X1,X2,X3,X4,X5] :
( c_in(X0,X5,X2)
| ~ c_lessequals(c_Zorn_Omaxchain__super__lemma__1(X3,X5,X2),X5,tc_set(X2))
| ~ c_in(c_union(c_insert(X1,c_emptyset,tc_set(X2)),X3,tc_set(X2)),c_Zorn_Ochain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(X3,c_Zorn_Omaxchain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f30,plain,
! [X0] :
( ~ c_in(X0,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))
| c_in(v_x(X0),v_S,tc_set(t_a)) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f31,plain,
! [X0] :
( ~ c_in(X0,v_S,tc_set(t_a))
| c_in(v_xa(X0),v_S,tc_set(t_a)) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f32,plain,
! [X0] :
( ~ c_in(X0,v_S,tc_set(t_a))
| c_lessequals(X0,v_xa(X0),tc_set(t_a)) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f33,plain,
! [X0] :
( ~ c_in(X0,v_S,tc_set(t_a))
| X0 != v_xa(X0) ),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f34,plain,
! [V_U] :
( ~ c_in(V_U,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))
| ! [V_V] :
( ~ c_in(V_V,V_U,tc_set(t_a))
| c_lessequals(V_V,v_x(V_U),tc_set(t_a)) ) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f35,plain,
! [X0,X1] :
( ~ c_in(X1,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))
| ~ c_in(X0,X1,tc_set(t_a))
| c_lessequals(X0,v_x(X1),tc_set(t_a)) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f36,plain,
! [X0,X1] :
( c_in(X1,v_xa(X0),t_a)
| ~ c_in(X1,X0,t_a)
| ~ c_in(X0,v_S,tc_set(t_a)) ),
inference(resolution,[status(thm)],[f32,f19]) ).
fof(f58,plain,
! [X0,X1,X2] :
( c_in(X0,c_Zorn_Ochain(X1,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,c_Zorn_Omaxchain(X1,X2),tc_set(tc_set(X2))) ),
inference(resolution,[status(thm)],[f25,f19]) ).
fof(f61,plain,
! [X0,X1] : c_in(c_Zorn_OHausdorff__1(X0,X1),c_Zorn_Ochain(X0,X1),tc_set(tc_set(X1))),
inference(resolution,[status(thm)],[f58,f24]) ).
fof(f64,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ c_lessequals(c_Zorn_Ochain__extend__1(X3,X1,X2),X1,tc_set(X2))
| ~ c_in(X3,c_Zorn_Ochain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(X1,X4,tc_set(X2))
| c_in(c_Zorn_Omaxchain__super__lemma__1(X3,X5,X2),X3,tc_set(X2))
| c_in(X0,X5,X2)
| ~ c_in(X3,c_Zorn_Omaxchain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,X1,X2) ),
inference(resolution,[status(thm)],[f27,f23]) ).
fof(f65,plain,
! [X0,X1,X2,X3,X4,X5] :
( c_in(c_Zorn_Ochain__extend__1(X3,X1,X2),X3,tc_set(X2))
| ~ c_in(X3,c_Zorn_Ochain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(X1,X4,tc_set(X2))
| c_in(c_Zorn_Omaxchain__super__lemma__1(X3,X5,X2),X3,tc_set(X2))
| c_in(X0,X5,X2)
| ~ c_in(X3,c_Zorn_Omaxchain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,X1,X2) ),
inference(resolution,[status(thm)],[f27,f22]) ).
fof(f66,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ c_lessequals(c_Zorn_Ochain__extend__1(X3,X1,X2),X1,tc_set(X2))
| ~ c_in(X1,X4,tc_set(X2))
| c_in(c_Zorn_Omaxchain__super__lemma__1(X3,X5,X2),X3,tc_set(X2))
| c_in(X0,X5,X2)
| ~ c_in(X3,c_Zorn_Omaxchain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f64,f58]) ).
fof(f67,plain,
! [X0,X1,X2,X3,X4,X5] :
( c_in(c_Zorn_Ochain__extend__1(X3,X1,X2),X3,tc_set(X2))
| ~ c_in(X1,X4,tc_set(X2))
| c_in(c_Zorn_Omaxchain__super__lemma__1(X3,X5,X2),X3,tc_set(X2))
| c_in(X0,X5,X2)
| ~ c_in(X3,c_Zorn_Omaxchain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f65,f58]) ).
fof(f68,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ c_lessequals(c_Zorn_Ochain__extend__1(X3,X1,X2),X1,tc_set(X2))
| ~ c_in(X3,c_Zorn_Ochain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(X1,X4,tc_set(X2))
| c_in(X0,X5,X2)
| ~ c_lessequals(c_Zorn_Omaxchain__super__lemma__1(X3,X5,X2),X5,tc_set(X2))
| ~ c_in(X3,c_Zorn_Omaxchain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,X1,X2) ),
inference(resolution,[status(thm)],[f29,f23]) ).
fof(f69,plain,
! [X0,X1,X2,X3,X4,X5] :
( c_in(c_Zorn_Ochain__extend__1(X3,X1,X2),X3,tc_set(X2))
| ~ c_in(X3,c_Zorn_Ochain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(X1,X4,tc_set(X2))
| c_in(X0,X5,X2)
| ~ c_lessequals(c_Zorn_Omaxchain__super__lemma__1(X3,X5,X2),X5,tc_set(X2))
| ~ c_in(X3,c_Zorn_Omaxchain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,X1,X2) ),
inference(resolution,[status(thm)],[f29,f22]) ).
fof(f70,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ c_lessequals(c_Zorn_Ochain__extend__1(X3,X1,X2),X1,tc_set(X2))
| ~ c_in(X1,X4,tc_set(X2))
| c_in(X0,X5,X2)
| ~ c_lessequals(c_Zorn_Omaxchain__super__lemma__1(X3,X5,X2),X5,tc_set(X2))
| ~ c_in(X3,c_Zorn_Omaxchain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f68,f58]) ).
fof(f71,plain,
! [X0,X1,X2,X3,X4,X5] :
( c_in(c_Zorn_Ochain__extend__1(X3,X1,X2),X3,tc_set(X2))
| ~ c_in(X1,X4,tc_set(X2))
| c_in(X0,X5,X2)
| ~ c_lessequals(c_Zorn_Omaxchain__super__lemma__1(X3,X5,X2),X5,tc_set(X2))
| ~ c_in(X3,c_Zorn_Omaxchain(X4,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f69,f58]) ).
fof(f76,plain,
! [X0] :
( ~ c_in(X0,c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))
| c_lessequals(X0,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a)) ),
inference(resolution,[status(thm)],[f61,f35]) ).
fof(f77,plain,
c_in(v_x(c_Zorn_OHausdorff__1(v_S,t_a)),v_S,tc_set(t_a)),
inference(resolution,[status(thm)],[f61,f30]) ).
fof(f78,plain,
! [X0] :
( c_in(X0,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)
| ~ c_in(X0,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a) ),
inference(resolution,[status(thm)],[f77,f36]) ).
fof(f84,plain,
! [X0,X1] :
( c_in(X1,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X1,X0,t_a)
| ~ c_in(X0,c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a)) ),
inference(resolution,[status(thm)],[f76,f19]) ).
fof(f89,definition,
( sQ1_spl
<=> c_in(v_x(c_Zorn_OHausdorff__1(v_S,t_a)),v_S,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f91,plain,
( sQ1_spl
| ~ c_in(v_x(c_Zorn_OHausdorff__1(v_S,t_a)),v_S,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f89]) ).
fof(f94,plain,
! [X0] :
( c_lessequals(X0,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a))
| ~ c_in(c_Main_OsubsetI__1(X0,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a) ),
inference(resolution,[status(thm)],[f78,f21]) ).
fof(f99,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f91,f77]) ).
fof(f100,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f99]) ).
fof(f106,plain,
! [X0,X1,X2,X3,X4] :
( ~ c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(X4,X2),X1,X2),X1,tc_set(X2))
| ~ c_in(X1,X4,tc_set(X2))
| c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(X4,X2),X3,X2),c_Zorn_OHausdorff__1(X4,X2),tc_set(X2))
| c_in(X0,X3,X2)
| ~ c_in(X0,X1,X2) ),
inference(resolution,[status(thm)],[f66,f24]) ).
fof(f116,plain,
! [X0,X1,X2,X3,X4] :
( c_in(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(X4,X2),X1,X2),c_Zorn_OHausdorff__1(X4,X2),tc_set(X2))
| ~ c_in(X1,X4,tc_set(X2))
| c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(X4,X2),X3,X2),c_Zorn_OHausdorff__1(X4,X2),tc_set(X2))
| c_in(X0,X3,X2)
| ~ c_in(X0,X1,X2) ),
inference(resolution,[status(thm)],[f67,f24]) ).
fof(f118,plain,
! [X0,X1,X2,X3,X4] :
( ~ c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(X3,X2),X1,X2),X1,tc_set(X2))
| ~ c_in(X1,X3,tc_set(X2))
| c_in(X0,X4,X2)
| ~ c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(X3,X2),X4,X2),X4,tc_set(X2))
| ~ c_in(X0,X1,X2) ),
inference(resolution,[status(thm)],[f70,f24]) ).
fof(f132,definition,
( sQ5_spl
<=> v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))) = v_x(c_Zorn_OHausdorff__1(v_S,t_a)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f133,plain,
( ~ sQ5_spl
| v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))) = v_x(c_Zorn_OHausdorff__1(v_S,t_a)) ),
inference(component_clause,[status(thm)],[f132]) ).
fof(f149,plain,
! [X0,X1,X2,X3,X4] :
( c_in(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(X3,X2),X1,X2),c_Zorn_OHausdorff__1(X3,X2),tc_set(X2))
| ~ c_in(X1,X3,tc_set(X2))
| c_in(X0,X4,X2)
| ~ c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(X3,X2),X4,X2),X4,tc_set(X2))
| ~ c_in(X0,X1,X2) ),
inference(resolution,[status(thm)],[f71,f24]) ).
fof(f173,plain,
( c_lessequals(v_x(c_Zorn_OHausdorff__1(v_S,t_a)),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a))
| c_lessequals(v_x(c_Zorn_OHausdorff__1(v_S,t_a)),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a)) ),
inference(resolution,[status(thm)],[f94,f20]) ).
fof(f174,definition,
( sQ7_spl
<=> c_lessequals(v_x(c_Zorn_OHausdorff__1(v_S,t_a)),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f175,plain,
( ~ sQ7_spl
| c_lessequals(v_x(c_Zorn_OHausdorff__1(v_S,t_a)),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f174]) ).
fof(f177,plain,
sQ7_spl,
inference(split_clause,[status(thm)],[f173,f174]) ).
fof(f180,plain,
( ~ sQ7_spl
| v_x(c_Zorn_OHausdorff__1(v_S,t_a)) = v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a)))
| ~ c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a)) ),
inference(resolution,[status(thm)],[f175,f17]) ).
fof(f182,definition,
( sQ8_spl
<=> c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f185,plain,
( ~ sQ7_spl
| sQ5_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f180,f182,f132,f174]) ).
fof(f197,plain,
( ~ sQ5_spl
| ~ c_in(v_x(c_Zorn_OHausdorff__1(v_S,t_a)),v_S,tc_set(t_a)) ),
inference(resolution,[status(thm)],[f133,f33]) ).
fof(f217,plain,
( ~ sQ5_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f197,f89,f132]) ).
fof(f309,plain,
! [X0,X1,X2,X3] :
( c_in(X3,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X3,c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),X2,t_a),t_a)
| c_in(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))
| ~ c_in(X1,v_S,tc_set(t_a))
| c_in(X0,X2,t_a)
| ~ c_in(X0,X1,t_a) ),
inference(resolution,[status(thm)],[f116,f84]) ).
fof(f310,plain,
! [X0,X1,X2] :
( ~ c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(X2,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))
| ~ c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(X2,t_a),X1,t_a),X1,tc_set(t_a))
| ~ c_in(X1,X2,tc_set(t_a))
| c_in(X0,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X0,X1,t_a) ),
inference(resolution,[status(thm)],[f118,f76]) ).
fof(f319,plain,
! [X0,X1,X2,X3] :
( c_in(X3,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X3,c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),t_a)
| ~ c_in(X1,v_S,tc_set(t_a))
| c_in(X0,X2,t_a)
| ~ c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),X2,t_a),X2,tc_set(t_a))
| ~ c_in(X0,X1,t_a) ),
inference(resolution,[status(thm)],[f149,f84]) ).
fof(f435,definition,
! [X0] :
( sQ30_spl
<=> ( c_in(X0,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X0,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f436,plain,
! [X0] :
( ~ sQ30_spl
| c_in(X0,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X0,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a) ),
inference(component_clause,[status(thm)],[f435]) ).
fof(f439,definition,
( sQ31_spl
<=> c_in(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_S,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f441,plain,
( sQ31_spl
| ~ c_in(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_S,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f439]) ).
fof(f533,plain,
( sQ31_spl
| ~ c_in(v_x(c_Zorn_OHausdorff__1(v_S,t_a)),v_S,tc_set(t_a)) ),
inference(resolution,[status(thm)],[f441,f31]) ).
fof(f534,plain,
( sQ31_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f533,f89,f439]) ).
fof(f806,plain,
! [X0,X1,X2,X3] :
( ~ c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X3,t_a),X3,tc_set(t_a))
| ~ c_in(X3,v_S,tc_set(t_a))
| c_in(X2,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X2,X3,t_a)
| ~ c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),X1,tc_set(t_a))
| ~ c_in(X1,v_S,tc_set(t_a))
| c_in(X0,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X0,X1,t_a) ),
inference(resolution,[status(thm)],[f310,f106]) ).
fof(f807,definition,
! [X0,X1] :
( sQ79_spl
<=> ( ~ c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),X1,tc_set(t_a))
| ~ c_in(X1,v_S,tc_set(t_a))
| c_in(X0,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X0,X1,t_a) ) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f808,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),X1,tc_set(t_a))
| ~ c_in(X1,v_S,tc_set(t_a))
| c_in(X0,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X0,X1,t_a) ),
inference(component_clause,[status(thm)],[f807]) ).
fof(f814,plain,
sQ79_spl,
inference(split_clause,[status(thm)],[f806,f807]) ).
fof(f1228,plain,
! [X0,X1,X2,X3,X4] :
( c_in(X4,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X4,c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),t_a)
| c_in(X3,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X3,c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),X2,t_a),t_a)
| ~ c_in(X1,v_S,tc_set(t_a))
| c_in(X0,X2,t_a)
| ~ c_in(X0,X1,t_a) ),
inference(resolution,[status(thm)],[f309,f84]) ).
fof(f1234,definition,
! [X0,X1,X2] :
( sQ121_spl
<=> ( c_in(X2,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X2,c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),t_a)
| ~ c_in(X1,v_S,tc_set(t_a))
| c_in(X0,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X0,X1,t_a) ) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1235,plain,
! [X0,X1,X2] :
( ~ sQ121_spl
| c_in(X2,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X2,c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),t_a)
| ~ c_in(X1,v_S,tc_set(t_a))
| c_in(X0,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X0,X1,t_a) ),
inference(component_clause,[status(thm)],[f1234]) ).
fof(f2071,plain,
! [X0,X1,X2,X3,X4] :
( c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),X2,t_a),X3,tc_set(t_a))
| c_in(X4,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X4,c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),t_a)
| c_in(c_Main_OsubsetI__1(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),X2,t_a),X3,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X1,v_S,tc_set(t_a))
| c_in(X0,X2,t_a)
| ~ c_in(X0,X1,t_a) ),
inference(resolution,[status(thm)],[f1228,f20]) ).
fof(f3018,plain,
! [X0,X1,X2] :
( ~ sQ121_spl
| c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),X2,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),X2,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X1,v_S,tc_set(t_a))
| c_in(X0,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X0,X1,t_a) ),
inference(resolution,[status(thm)],[f1235,f20]) ).
fof(f3330,plain,
! [X0,X1,X2,X3] :
( c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),X2,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))
| c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),X2,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))
| c_in(X3,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X3,c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),t_a)
| ~ c_in(X1,v_S,tc_set(t_a))
| c_in(X0,X2,t_a)
| ~ c_in(X0,X1,t_a) ),
inference(resolution,[status(thm)],[f2071,f21]) ).
fof(f3336,plain,
! [X0,X1,X2,X3] :
( c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),X2,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))
| c_in(X3,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X3,c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),t_a)
| ~ c_in(X1,v_S,tc_set(t_a))
| c_in(X0,X2,t_a)
| ~ c_in(X0,X1,t_a) ),
inference(duplicate_literals_removal,[status(thm)],[f3330]) ).
fof(f4375,plain,
! [X0,X1] :
( ~ sQ121_spl
| c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a))
| c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a))
| ~ c_in(X1,v_S,tc_set(t_a))
| c_in(X0,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X0,X1,t_a) ),
inference(resolution,[status(thm)],[f3018,f94]) ).
fof(f4380,plain,
! [X0,X1] :
( ~ sQ121_spl
| c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a))
| ~ c_in(X1,v_S,tc_set(t_a))
| c_in(X0,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X0,X1,t_a) ),
inference(duplicate_literals_removal,[status(thm)],[f4375]) ).
fof(f8112,plain,
! [X0,X1,X2,X3,X4,X5] :
( c_in(X5,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X5,c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X4,t_a),t_a)
| ~ c_in(X4,v_S,tc_set(t_a))
| c_in(X3,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X3,X4,t_a)
| c_in(X2,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X2,c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),X1,t_a),t_a)
| ~ c_in(X1,v_S,tc_set(t_a))
| c_in(X0,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X0,X1,t_a) ),
inference(resolution,[status(thm)],[f3336,f319]) ).
fof(f8117,plain,
sQ121_spl,
inference(split_clause,[status(thm)],[f8112,f1234]) ).
fof(f8126,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ121_spl
| ~ c_in(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_S,tc_set(t_a))
| c_in(X1,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X1,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)
| ~ c_in(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_S,tc_set(t_a))
| c_in(X0,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)
| ~ c_in(X0,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a) ),
inference(resolution,[status(thm)],[f4380,f808]) ).
fof(f8133,plain,
( ~ sQ79_spl
| ~ sQ121_spl
| ~ sQ31_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f8126,f435,f439,f1234,f807]) ).
fof(f8145,plain,
! [X0] :
( ~ sQ30_spl
| c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),X0,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),X0,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a) ),
inference(resolution,[status(thm)],[f436,f20]) ).
fof(f8151,plain,
( ~ sQ30_spl
| c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))
| c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a)) ),
inference(resolution,[status(thm)],[f8145,f21]) ).
fof(f8156,plain,
( ~ sQ30_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f8151,f182,f435]) ).
fof(f8157,plain,
$false,
inference(sat_refutation,[status(thm)],[f100,f177,f185,f217,f534,f814,f8117,f8133,f8156]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET861-2 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n014.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 05:42:04 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 30.77/4.41 % Refutation found
% 30.77/4.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 30.77/4.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 30.59/4.50 % Elapsed time: 4.121565 seconds
% 30.59/4.50 % CPU time: 32.054813 seconds
% 30.59/4.50 % Total memory used: 314.091 MB
% 30.59/4.50 % Net memory used: 290.470 MB
%------------------------------------------------------------------------------