%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET843-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:46 PM UTC 2026
% Result : Unsatisfiable 0.07s 0.39s
% Output : CNFRefutation 0.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 71
% Syntax : Number of formulae : 237 ( 46 unt; 34 def)
% Number of atoms : 490 ( 100 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 472 ( 219 ~; 219 |; 0 &)
% ( 34 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 42 ( 40 usr; 35 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 9 con; 0-3 aty)
% Number of variables : 307 ( 307 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f61,axiom,
! [V_xs,V_ys,T_a,V_A] :
( c_in(V_ys,c_List_Olists(V_A,T_a),tc_List_Olist(T_a))
| ~ c_in(c_append(V_xs,V_ys,T_a),c_List_Olists(V_A,T_a),tc_List_Olist(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [V_xs,T_a] :
( V_xs = c_List_Olist_ONil
| c_Nat_Osize(V_xs,tc_List_Olist(T_a)) != c_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [T_a] : c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(T_a)) = c_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f79,axiom,
! [V_a_H,V_list_H,T_a] : c_List_Olist_ONil != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f93,axiom,
! [V_xs,T_a] :
( V_xs = c_List_Olist_ONil
| c_emptyset != c_List_Oset(V_xs,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [V_n,V_m] :
( c_lessequals(V_n,V_m,tc_nat)
| ~ c_lessequals(c_Suc(V_n),c_Suc(V_m),tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f101,axiom,
! [V_m,V_n] :
( c_less(c_Suc(V_m),c_Suc(V_n),tc_nat)
| ~ c_less(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f102,axiom,
! [V_m] : c_Suc(V_m) != c_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f112,axiom,
! [V_n] :
( V_n = c_0
| ~ c_less(V_n,c_Suc(c_0),tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f116,axiom,
! [V_n] :
( V_n = c_0
| c_less(c_0,V_n,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f123,axiom,
! [T_a,V_x] :
( ~ c_less(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f132,axiom,
! [T_a,V_x,V_y] :
( V_x = V_y
| c_SetInterval_OatLeast(V_x,T_a) != c_SetInterval_OatLeast(V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f173,axiom,
! [V_A,V_X,T_a,V_C] :
( c_in(V_A,c_Union(V_C,T_a),T_a)
| ~ c_in(V_X,V_C,tc_set(T_a))
| ~ c_in(V_A,V_X,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f174,axiom,
! [V_a,T_a] : ~ c_in(V_a,c_emptyset,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f226,axiom,
! [T_a] : c_in(c_emptyset,c_Finite__Set_OFinites,tc_set(T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f230,axiom,
! [V_A,T_a] :
( c_in(c_Union(V_A,T_a),c_Finite__Set_OFinites,tc_set(T_a))
| c_in(c_Main_Ofinite__Union__1(V_A,T_a),V_A,tc_set(T_a))
| ~ c_in(V_A,c_Finite__Set_OFinites,tc_set(tc_set(T_a))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f234,axiom,
! [V_S,T_a,V_y,V_x] :
( V_y = V_x
| ~ c_in(V_x,V_S,T_a)
| ~ c_in(V_y,V_S,T_a)
| ~ c_Infinite__Set_Oatmost__one(V_S,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f243,axiom,
! [V_xs,T_a] : c_in(c_List_Oset(V_xs,T_a),c_Finite__Set_OFinites,tc_set(T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f245,axiom,
! [V_xs,V_A,T_a] :
( c_in(c_Main_Oin__listsI__1(V_A,V_xs,T_a),c_List_Oset(V_xs,T_a),T_a)
| c_in(V_xs,c_List_Olists(V_A,T_a),tc_List_Olist(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f246,axiom,
! [V_A,V_xs,T_a] :
( c_in(V_xs,c_List_Olists(V_A,T_a),tc_List_Olist(T_a))
| ~ c_in(c_Main_Oin__listsI__1(V_A,V_xs,T_a),V_A,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f266,axiom,
! [T_a,V_x] :
( c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f296,axiom,
! [V_x,T_a] : c_in(V_x,c_UNIV,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f299,axiom,
! [V_A,T_a] : c_lessequals(c_emptyset,V_A,tc_set(T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f300,axiom,
! [V_A,V_B,T_a] :
( ~ c_lessequals(V_B,V_A,tc_set(T_a))
| ~ c_less(V_A,V_B,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f302,axiom,
! [V_A,V_B,T_a] :
( V_A = V_B
| c_less(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_A,V_B,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f310,axiom,
! [V_A,T_a] : c_lessequals(V_A,V_A,tc_set(T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f419,axiom,
class_Orderings_Oorder(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f441,axiom,
class_Orderings_Olinorder(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f447,axiom,
! [T_1] : class_Orderings_Oorder(tc_set(T_1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1360,axiom,
! [V_B,V_A,T_a] :
( c_lessequals(V_B,c_Union(V_A,T_a),tc_set(T_a))
| ~ c_in(V_B,V_A,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1361,axiom,
! [V_x,V_S,T_a] : c_lessequals(V_x,c_Zorn_Osucc(V_S,V_x,T_a),tc_set(tc_set(T_a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1362,axiom,
! [V_x,V_S,T_a] :
( c_in(c_Zorn_Osucc(V_S,V_x,T_a),c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_x,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1363,axiom,
! [V_Y,V_S,T_a] :
( c_in(c_Union(V_Y,tc_set(T_a)),c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_lessequals(V_Y,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(tc_set(T_a)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1364,axiom,
! [V_m,V_S,T_a,V_n] :
( c_lessequals(V_n,V_m,tc_set(tc_set(T_a)))
| V_m != c_Zorn_Osucc(V_S,V_m,T_a)
| ~ c_in(V_n,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_m,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1365,negated_conjecture,
c_in(v_m,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1366,negated_conjecture,
( v_m != c_Zorn_Osucc(v_S,v_m,t_a)
| v_m != c_Union(c_Zorn_OTFin(v_S,t_a),tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1367,negated_conjecture,
( v_m = c_Union(c_Zorn_OTFin(v_S,t_a),tc_set(t_a))
| v_m = c_Zorn_Osucc(v_S,v_m,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1450,plain,
! [V_ys,T_a,V_A] :
( c_in(V_ys,c_List_Olists(V_A,T_a),tc_List_Olist(T_a))
| ! [V_xs] : ~ c_in(c_append(V_xs,V_ys,T_a),c_List_Olists(V_A,T_a),tc_List_Olist(T_a)) ),
inference(miniscoping,[status(thm)],[f61]) ).
fof(f1451,plain,
! [X0,X1,X2,X3] :
( c_in(X1,c_List_Olists(X3,X2),tc_List_Olist(X2))
| ~ c_in(c_append(X0,X1,X2),c_List_Olists(X3,X2),tc_List_Olist(X2)) ),
inference(cnf_transformation,[status(thm)],[f1450]) ).
fof(f1470,plain,
! [V_xs] :
( V_xs = c_List_Olist_ONil
| ! [T_a] : c_Nat_Osize(V_xs,tc_List_Olist(T_a)) != c_0 ),
inference(miniscoping,[status(thm)],[f73]) ).
fof(f1471,plain,
! [X0,X1] :
( X0 = c_List_Olist_ONil
| c_Nat_Osize(X0,tc_List_Olist(X1)) != c_0 ),
inference(cnf_transformation,[status(thm)],[f1470]) ).
fof(f1472,plain,
! [X0] : c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(X0)) = c_0,
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f1478,plain,
! [X0,X1,X2] : c_List_Olist_ONil != c_List_Olist_OCons(X0,X1,X2),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f1499,plain,
! [V_xs] :
( V_xs = c_List_Olist_ONil
| ! [T_a] : c_emptyset != c_List_Oset(V_xs,T_a) ),
inference(miniscoping,[status(thm)],[f93]) ).
fof(f1500,plain,
! [X0,X1] :
( X0 = c_List_Olist_ONil
| c_emptyset != c_List_Oset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1499]) ).
fof(f1506,plain,
! [X0,X1] :
( c_lessequals(X0,X1,tc_nat)
| ~ c_lessequals(c_Suc(X0),c_Suc(X1),tc_nat) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f1509,plain,
! [X0,X1] :
( c_less(c_Suc(X0),c_Suc(X1),tc_nat)
| ~ c_less(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f1510,plain,
! [X0] : c_Suc(X0) != c_0,
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f1525,plain,
! [X0] :
( X0 = c_0
| ~ c_less(X0,c_Suc(c_0),tc_nat) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f1529,plain,
! [X0] :
( X0 = c_0
| c_less(c_0,X0,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f1536,plain,
! [T_a] :
( ! [V_x] : ~ c_less(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(miniscoping,[status(thm)],[f123]) ).
fof(f1537,plain,
! [X0,X1] :
( ~ c_less(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(thm)],[f1536]) ).
fof(f1549,plain,
! [V_x,V_y] :
( V_x = V_y
| ! [T_a] :
( c_SetInterval_OatLeast(V_x,T_a) != c_SetInterval_OatLeast(V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ) ),
inference(miniscoping,[status(thm)],[f132]) ).
fof(f1550,plain,
! [X0,X1,X2] :
( X1 = X2
| c_SetInterval_OatLeast(X1,X0) != c_SetInterval_OatLeast(X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(thm)],[f1549]) ).
fof(f1605,plain,
! [V_A,T_a,V_C] :
( c_in(V_A,c_Union(V_C,T_a),T_a)
| ! [V_X] :
( ~ c_in(V_X,V_C,tc_set(T_a))
| ~ c_in(V_A,V_X,T_a) ) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f1606,plain,
! [X0,X1,X2,X3] :
( c_in(X0,c_Union(X3,X2),X2)
| ~ c_in(X1,X3,tc_set(X2))
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1605]) ).
fof(f1607,plain,
! [X0,X1] : ~ c_in(X0,c_emptyset,X1),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f1683,plain,
! [X0] : c_in(c_emptyset,c_Finite__Set_OFinites,tc_set(X0)),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f1690,plain,
! [X0,X1] :
( c_in(c_Union(X0,X1),c_Finite__Set_OFinites,tc_set(X1))
| c_in(c_Main_Ofinite__Union__1(X0,X1),X0,tc_set(X1))
| ~ c_in(X0,c_Finite__Set_OFinites,tc_set(tc_set(X1))) ),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f1694,plain,
! [V_y,V_x] :
( V_y = V_x
| ! [V_S,T_a] :
( ~ c_in(V_x,V_S,T_a)
| ~ c_in(V_y,V_S,T_a)
| ~ c_Infinite__Set_Oatmost__one(V_S,T_a) ) ),
inference(miniscoping,[status(thm)],[f234]) ).
fof(f1695,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ c_in(X3,X0,X1)
| ~ c_in(X2,X0,X1)
| ~ c_Infinite__Set_Oatmost__one(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1694]) ).
fof(f1704,plain,
! [X0,X1] : c_in(c_List_Oset(X0,X1),c_Finite__Set_OFinites,tc_set(X1)),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f1707,plain,
! [X0,X1,X2] :
( c_in(c_Main_Oin__listsI__1(X1,X0,X2),c_List_Oset(X0,X2),X2)
| c_in(X0,c_List_Olists(X1,X2),tc_List_Olist(X2)) ),
inference(cnf_transformation,[status(thm)],[f245]) ).
fof(f1708,plain,
! [X0,X1,X2] :
( c_in(X1,c_List_Olists(X0,X2),tc_List_Olist(X2))
| ~ c_in(c_Main_Oin__listsI__1(X0,X1,X2),X0,X2) ),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f1732,plain,
! [T_a] :
( ! [V_x] : c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(miniscoping,[status(thm)],[f266]) ).
fof(f1733,plain,
! [X0,X1] :
( c_lessequals(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(thm)],[f1732]) ).
fof(f1767,plain,
! [X0,X1] : c_in(X0,c_UNIV,X1),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f1770,plain,
! [X0,X1] : c_lessequals(c_emptyset,X0,tc_set(X1)),
inference(cnf_transformation,[status(thm)],[f299]) ).
fof(f1771,plain,
! [X0,X1,X2] :
( ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_less(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f1773,plain,
! [V_A,V_B] :
( V_A = V_B
| ! [T_a] :
( c_less(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_A,V_B,tc_set(T_a)) ) ),
inference(miniscoping,[status(thm)],[f302]) ).
fof(f1774,plain,
! [X0,X1,X2] :
( X0 = X1
| c_less(X0,X1,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(thm)],[f1773]) ).
fof(f1786,plain,
! [X0,X1] : c_lessequals(X0,X0,tc_set(X1)),
inference(cnf_transformation,[status(thm)],[f310]) ).
fof(f1902,plain,
class_Orderings_Oorder(tc_nat),
inference(cnf_transformation,[status(thm)],[f419]) ).
fof(f1924,plain,
class_Orderings_Olinorder(tc_nat),
inference(cnf_transformation,[status(thm)],[f441]) ).
fof(f1931,plain,
! [X0] : class_Orderings_Oorder(tc_set(X0)),
inference(cnf_transformation,[status(thm)],[f447]) ).
fof(f2845,plain,
! [X0,X1,X2] :
( c_lessequals(X0,c_Union(X1,X2),tc_set(X2))
| ~ c_in(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(thm)],[f1360]) ).
fof(f2846,plain,
! [X0,X1,X2] : c_lessequals(X0,c_Zorn_Osucc(X1,X0,X2),tc_set(tc_set(X2))),
inference(cnf_transformation,[status(thm)],[f1361]) ).
fof(f2847,plain,
! [X0,X1,X2] :
( c_in(c_Zorn_Osucc(X1,X0,X2),c_Zorn_OTFin(X1,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,c_Zorn_OTFin(X1,X2),tc_set(tc_set(X2))) ),
inference(cnf_transformation,[status(thm)],[f1362]) ).
fof(f2848,plain,
! [X0,X1,X2] :
( c_in(c_Union(X0,tc_set(X2)),c_Zorn_OTFin(X1,X2),tc_set(tc_set(X2)))
| ~ c_lessequals(X0,c_Zorn_OTFin(X1,X2),tc_set(tc_set(tc_set(X2)))) ),
inference(cnf_transformation,[status(thm)],[f1363]) ).
fof(f2849,plain,
! [V_m,T_a,V_n] :
( c_lessequals(V_n,V_m,tc_set(tc_set(T_a)))
| ! [V_S] :
( V_m != c_Zorn_Osucc(V_S,V_m,T_a)
| ~ c_in(V_n,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_m,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a))) ) ),
inference(miniscoping,[status(thm)],[f1364]) ).
fof(f2850,plain,
! [X0,X1,X2,X3] :
( c_lessequals(X3,X0,tc_set(tc_set(X2)))
| X0 != c_Zorn_Osucc(X1,X0,X2)
| ~ c_in(X3,c_Zorn_OTFin(X1,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,c_Zorn_OTFin(X1,X2),tc_set(tc_set(X2))) ),
inference(cnf_transformation,[status(thm)],[f2849]) ).
fof(f2851,plain,
c_in(v_m,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))),
inference(cnf_transformation,[status(thm)],[f1365]) ).
fof(f2852,plain,
( v_m != c_Zorn_Osucc(v_S,v_m,t_a)
| v_m != c_Union(c_Zorn_OTFin(v_S,t_a),tc_set(t_a)) ),
inference(cnf_transformation,[status(thm)],[f1366]) ).
fof(f2853,plain,
( v_m = c_Union(c_Zorn_OTFin(v_S,t_a),tc_set(t_a))
| v_m = c_Zorn_Osucc(v_S,v_m,t_a) ),
inference(cnf_transformation,[status(thm)],[f1367]) ).
fof(f2854,definition,
( sQ0_spl
<=> v_m = c_Union(c_Zorn_OTFin(v_S,t_a),tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f2855,plain,
( ~ sQ0_spl
| v_m = c_Union(c_Zorn_OTFin(v_S,t_a),tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f2854]) ).
fof(f2857,definition,
( sQ1_spl
<=> v_m = c_Zorn_Osucc(v_S,v_m,t_a) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f2858,plain,
( ~ sQ1_spl
| v_m = c_Zorn_Osucc(v_S,v_m,t_a) ),
inference(component_clause,[status(thm)],[f2857]) ).
fof(f2860,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f2852,f2854,f2857]) ).
fof(f2861,plain,
( sQ0_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f2853,f2857,f2854]) ).
fof(f2864,definition,
( sQ2_spl
<=> c_in(v_m,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f2866,plain,
( sQ2_spl
| ~ c_in(v_m,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
inference(component_clause,[status(thm)],[f2864]) ).
fof(f2868,plain,
! [X0] :
( ~ sQ1_spl
| c_lessequals(X0,v_m,tc_set(tc_set(t_a)))
| ~ c_in(X0,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| ~ c_in(v_m,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[f2850,f2858]) ).
fof(f2870,definition,
! [X0] :
( sQ3_spl
<=> ( c_lessequals(X0,v_m,tc_set(tc_set(t_a)))
| ~ c_in(X0,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f2871,plain,
! [X0] :
( ~ sQ3_spl
| c_lessequals(X0,v_m,tc_set(tc_set(t_a)))
| ~ c_in(X0,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
inference(component_clause,[status(thm)],[f2870]) ).
fof(f2873,plain,
( ~ sQ1_spl
| sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f2868,f2864,f2870,f2857]) ).
fof(f2874,definition,
( sQ4_spl
<=> v_m = v_m ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f2876,plain,
( sQ4_spl
| v_m != v_m ),
inference(component_clause,[status(thm)],[f2874]) ).
fof(f2923,definition,
( sQ5_spl
<=> c_emptyset = c_emptyset ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f3098,definition,
( sQ6_spl
<=> c_List_Olist_ONil = c_List_Olist_ONil ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f3338,plain,
( c_List_Olist_ONil = c_List_Olist_ONil
| c_0 != c_0 ),
inference(paramodulation,[status(thm)],[f1472,f1471]) ).
fof(f3339,definition,
( sQ9_spl
<=> c_0 = c_0 ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f3342,plain,
( sQ6_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f3338,f3339,f3098]) ).
fof(f3673,plain,
( c_0 = c_0
| c_Suc(c_0) = c_0 ),
inference(resolution,[status(thm)],[f1529,f1525]) ).
fof(f3679,definition,
( sQ14_spl
<=> c_Suc(c_0) = c_0 ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f3680,plain,
( ~ sQ14_spl
| c_Suc(c_0) = c_0 ),
inference(component_clause,[status(thm)],[f3679]) ).
fof(f3682,plain,
( sQ9_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f3673,f3679,f3339]) ).
fof(f3683,plain,
( ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3680,f1510]) ).
fof(f3684,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f3683]) ).
fof(f3713,plain,
! [X0] :
( ~ c_less(X0,X0,tc_nat)
| ~ class_Orderings_Oorder(tc_nat) ),
inference(resolution,[status(thm)],[f1537,f1509]) ).
fof(f3715,definition,
( sQ15_spl
<=> class_Orderings_Oorder(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f3717,plain,
( sQ15_spl
| ~ class_Orderings_Oorder(tc_nat) ),
inference(component_clause,[status(thm)],[f3715]) ).
fof(f3718,definition,
! [X0] :
( sQ16_spl
<=> ~ c_less(X0,X0,tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f3721,plain,
( sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f3713,f3715,f3718]) ).
fof(f3723,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3717,f1902]) ).
fof(f3724,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f3723]) ).
fof(f3795,plain,
! [X0,X1] :
( X1 = X1
| ~ class_Orderings_Olinorder(X0) ),
inference(equality_resolution,[status(thm)],[f1550]) ).
fof(f3796,definition,
! [X0] :
( sQ17_spl
<=> ~ class_Orderings_Olinorder(X0) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f3797,plain,
! [X0] :
( ~ sQ17_spl
| ~ class_Orderings_Olinorder(X0) ),
inference(component_clause,[status(thm)],[f3796]) ).
fof(f3799,definition,
! [X1] :
( sQ18_spl
<=> X1 = X1 ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f3802,plain,
( sQ18_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f3795,f3796,f3799]) ).
fof(f3805,plain,
( ~ sQ17_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1924,f3797]) ).
fof(f3807,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f3805]) ).
fof(f4578,plain,
! [X0] :
( c_lessequals(X0,X0,tc_nat)
| ~ class_Orderings_Oorder(tc_nat) ),
inference(resolution,[status(thm)],[f1733,f1506]) ).
fof(f4586,definition,
! [X0] :
( sQ19_spl
<=> c_lessequals(X0,X0,tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f4589,plain,
( sQ19_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f4578,f3715,f4586]) ).
fof(f4590,definition,
( sQ20_spl
<=> class_Orderings_Oorder(tc_set(tc_set(tc_set(t_a)))) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f4592,plain,
( sQ20_spl
| ~ class_Orderings_Oorder(tc_set(tc_set(tc_set(t_a)))) ),
inference(component_clause,[status(thm)],[f4590]) ).
fof(f4622,plain,
! [X0] :
( ~ sQ3_spl
| ~ c_lessequals(X0,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(tc_set(t_a))))
| c_lessequals(c_Union(X0,tc_set(t_a)),v_m,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[f2871,f2848]) ).
fof(f4623,plain,
! [X0] :
( ~ sQ3_spl
| ~ c_in(X0,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,X0,t_a),v_m,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[f2871,f2847]) ).
fof(f4630,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2866,f2851]) ).
fof(f4631,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f4630]) ).
fof(f4632,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4592,f1931]) ).
fof(f4633,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f4632]) ).
fof(f4673,definition,
( sQ25_spl
<=> class_Orderings_Olinorder(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f4675,plain,
( sQ25_spl
| ~ class_Orderings_Olinorder(tc_nat) ),
inference(component_clause,[status(thm)],[f4673]) ).
fof(f4731,definition,
( sQ28_spl
<=> c_in(v_m,c_Finite__Set_OFinites,tc_set(tc_set(t_a))) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f4732,plain,
( ~ sQ28_spl
| c_in(v_m,c_Finite__Set_OFinites,tc_set(tc_set(t_a))) ),
inference(component_clause,[status(thm)],[f4731]) ).
fof(f4735,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4675,f1924]) ).
fof(f4736,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f4735]) ).
fof(f4780,plain,
! [X0,X1,X2,X3] :
( ~ c_lessequals(X3,c_Zorn_OTFin(X0,X1),tc_set(tc_set(tc_set(X1))))
| X2 = c_Union(X3,tc_set(X1))
| ~ c_in(X2,c_Zorn_OTFin(X0,X1),tc_set(tc_set(X1)))
| ~ c_Infinite__Set_Oatmost__one(c_Zorn_OTFin(X0,X1),tc_set(tc_set(X1))) ),
inference(resolution,[status(thm)],[f1695,f2848]) ).
fof(f4783,plain,
! [X0] :
( ~ sQ28_spl
| X0 = v_m
| ~ c_in(X0,c_Finite__Set_OFinites,tc_set(tc_set(t_a)))
| ~ c_Infinite__Set_Oatmost__one(c_Finite__Set_OFinites,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[f1695,f4732]) ).
fof(f4798,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ c_in(X1,c_UNIV,X0)
| ~ c_Infinite__Set_Oatmost__one(c_UNIV,X0) ),
inference(resolution,[status(thm)],[f1695,f1767]) ).
fof(f4854,definition,
( sQ43_spl
<=> c_Infinite__Set_Oatmost__one(c_Finite__Set_OFinites,tc_set(tc_set(t_a))) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f4857,definition,
! [X0] :
( sQ44_spl
<=> ( X0 = v_m
| ~ c_in(X0,c_Finite__Set_OFinites,tc_set(tc_set(t_a))) ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f4858,plain,
! [X0] :
( ~ sQ44_spl
| X0 = v_m
| ~ c_in(X0,c_Finite__Set_OFinites,tc_set(tc_set(t_a))) ),
inference(component_clause,[status(thm)],[f4857]) ).
fof(f4860,plain,
( ~ sQ28_spl
| sQ44_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f4783,f4854,f4857,f4731]) ).
fof(f4861,definition,
( sQ45_spl
<=> c_Infinite__Set_Oatmost__one(c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f4868,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ c_Infinite__Set_Oatmost__one(c_UNIV,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4798,f1767]) ).
fof(f4887,plain,
! [X0] :
( ~ sQ44_spl
| c_List_Oset(X0,tc_set(t_a)) = v_m ),
inference(resolution,[status(thm)],[f4858,f1704]) ).
fof(f4891,plain,
( ~ sQ44_spl
| c_emptyset = v_m ),
inference(resolution,[status(thm)],[f4858,f1683]) ).
fof(f4911,plain,
! [X0,X1] :
( ~ sQ44_spl
| X0 = c_List_Olist_ONil
| v_m != c_List_Oset(X0,X1) ),
inference(backward_demodulation,[status(thm)],[f4891,f1500]) ).
fof(f4963,plain,
! [X0] :
( ~ sQ44_spl
| X0 = c_List_Olist_ONil
| v_m != v_m ),
inference(paramodulation,[status(thm)],[f4887,f4911]) ).
fof(f4965,definition,
! [X0] :
( sQ47_spl
<=> X0 = c_List_Olist_ONil ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f4966,plain,
! [X0] :
( ~ sQ47_spl
| X0 = c_List_Olist_ONil ),
inference(component_clause,[status(thm)],[f4965]) ).
fof(f4968,plain,
( ~ sQ44_spl
| sQ47_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f4963,f2874,f4965,f4857]) ).
fof(f4969,plain,
( sQ4_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2876]) ).
fof(f4970,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f4969]) ).
fof(f4971,plain,
( ~ sQ47_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1478,f4966]) ).
fof(f4989,plain,
~ sQ47_spl,
inference(contradiction_clause,[status(thm)],[f4971]) ).
fof(f5032,plain,
! [X0,X1,X2] :
( X2 = c_Union(c_emptyset,tc_set(X1))
| ~ c_in(X2,c_Zorn_OTFin(X0,X1),tc_set(tc_set(X1)))
| ~ c_Infinite__Set_Oatmost__one(c_Zorn_OTFin(X0,X1),tc_set(tc_set(X1))) ),
inference(resolution,[status(thm)],[f1770,f4780]) ).
fof(f5071,plain,
! [X0,X1] : c_in(X0,c_List_Olists(c_UNIV,X1),tc_List_Olist(X1)),
inference(resolution,[status(thm)],[f1708,f1767]) ).
fof(f5072,plain,
! [X0,X1,X2,X3] :
( ~ c_in(X3,X1,tc_set(X2))
| ~ c_in(c_Main_Oin__listsI__1(c_Union(X1,X2),X0,X2),X3,X2)
| c_in(X0,c_List_Olists(c_Union(X1,X2),X2),tc_List_Olist(X2)) ),
inference(resolution,[status(thm)],[f1708,f1606]) ).
fof(f5092,plain,
( ~ sQ3_spl
| c_lessequals(c_Union(c_Zorn_OTFin(v_S,t_a),tc_set(t_a)),v_m,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[f4622,f1786]) ).
fof(f5107,plain,
( v_m = c_Union(c_emptyset,tc_set(t_a))
| ~ c_Infinite__Set_Oatmost__one(c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[f5032,f2851]) ).
fof(f5108,definition,
( sQ49_spl
<=> v_m = c_Union(c_emptyset,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f5109,plain,
( ~ sQ49_spl
| v_m = c_Union(c_emptyset,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f5108]) ).
fof(f5111,plain,
( sQ49_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f5107,f4861,f5108]) ).
fof(f5112,plain,
! [X0,X1,X2] :
( c_in(X0,c_List_Olists(c_Union(X1,X2),X2),tc_List_Olist(X2))
| ~ c_in(c_List_Oset(X0,X2),X1,tc_set(X2))
| c_in(X0,c_List_Olists(c_Union(X1,X2),X2),tc_List_Olist(X2)) ),
inference(resolution,[status(thm)],[f5072,f1707]) ).
fof(f5125,plain,
! [X0,X1,X2] :
( ~ c_in(c_UNIV,X1,tc_set(X2))
| c_in(X0,c_List_Olists(c_Union(X1,X2),X2),tc_List_Olist(X2)) ),
inference(resolution,[status(thm)],[f5072,f1767]) ).
fof(f5128,plain,
! [X0,X1,X2] :
( ~ c_in(c_List_Oset(X0,X2),X1,tc_set(X2))
| c_in(X0,c_List_Olists(c_Union(X1,X2),X2),tc_List_Olist(X2)) ),
inference(duplicate_literals_removal,[status(thm)],[f5112]) ).
fof(f5134,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ c_in(X2,c_List_Olists(c_Union(X0,X1),X1),tc_List_Olist(X1))
| ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_Union(X0,X1),X1),tc_List_Olist(X1))
| ~ c_in(c_UNIV,X0,tc_set(X1)) ),
inference(resolution,[status(thm)],[f5125,f1695]) ).
fof(f5135,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_Union(X0,X1),X1),tc_List_Olist(X1))
| ~ c_in(c_UNIV,X0,tc_set(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5134,f5125]) ).
fof(f5138,plain,
! [X0,X1,X2,X3] :
( c_in(X1,c_List_Olists(c_Union(X3,X2),X2),tc_List_Olist(X2))
| ~ c_in(c_List_Oset(c_append(X0,X1,X2),X2),X3,tc_set(X2)) ),
inference(resolution,[status(thm)],[f5128,f1451]) ).
fof(f5190,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ c_in(X1,c_List_Olists(c_UNIV,X0),tc_List_Olist(X0))
| ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_UNIV,X0),tc_List_Olist(X0)) ),
inference(resolution,[status(thm)],[f5071,f1695]) ).
fof(f5191,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_UNIV,X0),tc_List_Olist(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5190,f5071]) ).
fof(f5205,plain,
! [X0,X1] : c_in(X0,c_List_Olists(c_Union(c_Finite__Set_OFinites,X1),X1),tc_List_Olist(X1)),
inference(resolution,[status(thm)],[f5138,f1704]) ).
fof(f5218,plain,
! [X0,X1] : c_in(X0,c_List_Olists(c_Union(c_UNIV,X1),X1),tc_List_Olist(X1)),
inference(resolution,[status(thm)],[f5138,f1767]) ).
fof(f5228,plain,
! [X0,X1] : c_in(X0,c_List_Olists(c_List_Olists(c_Union(c_Finite__Set_OFinites,X1),X1),tc_List_Olist(X1)),tc_List_Olist(tc_List_Olist(X1))),
inference(resolution,[status(thm)],[f5205,f1708]) ).
fof(f5232,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ c_in(X1,c_List_Olists(c_Union(c_Finite__Set_OFinites,X0),X0),tc_List_Olist(X0))
| ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_Union(c_Finite__Set_OFinites,X0),X0),tc_List_Olist(X0)) ),
inference(resolution,[status(thm)],[f5205,f1695]) ).
fof(f5233,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_Union(c_Finite__Set_OFinites,X0),X0),tc_List_Olist(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5232,f5205]) ).
fof(f5235,plain,
! [X0,X1] : c_in(X0,c_List_Olists(c_List_Olists(c_Union(c_UNIV,X1),X1),tc_List_Olist(X1)),tc_List_Olist(tc_List_Olist(X1))),
inference(resolution,[status(thm)],[f5218,f1708]) ).
fof(f5239,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ c_in(X1,c_List_Olists(c_Union(c_UNIV,X0),X0),tc_List_Olist(X0))
| ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_Union(c_UNIV,X0),X0),tc_List_Olist(X0)) ),
inference(resolution,[status(thm)],[f5218,f1695]) ).
fof(f5240,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_Union(c_UNIV,X0),X0),tc_List_Olist(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5239,f5218]) ).
fof(f5264,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ c_in(X1,c_List_Olists(c_List_Olists(c_Union(c_Finite__Set_OFinites,X0),X0),tc_List_Olist(X0)),tc_List_Olist(tc_List_Olist(X0)))
| ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_List_Olists(c_Union(c_Finite__Set_OFinites,X0),X0),tc_List_Olist(X0)),tc_List_Olist(tc_List_Olist(X0))) ),
inference(resolution,[status(thm)],[f5228,f1695]) ).
fof(f5265,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_List_Olists(c_Union(c_Finite__Set_OFinites,X0),X0),tc_List_Olist(X0)),tc_List_Olist(tc_List_Olist(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f5264,f5228]) ).
fof(f5271,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ c_in(X1,c_List_Olists(c_List_Olists(c_Union(c_UNIV,X0),X0),tc_List_Olist(X0)),tc_List_Olist(tc_List_Olist(X0)))
| ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_List_Olists(c_Union(c_UNIV,X0),X0),tc_List_Olist(X0)),tc_List_Olist(tc_List_Olist(X0))) ),
inference(resolution,[status(thm)],[f5235,f1695]) ).
fof(f5272,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_List_Olists(c_Union(c_UNIV,X0),X0),tc_List_Olist(X0)),tc_List_Olist(tc_List_Olist(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f5271,f5235]) ).
fof(f5335,plain,
( ~ sQ3_spl
| c_Union(c_Zorn_OTFin(v_S,t_a),tc_set(t_a)) = v_m
| c_less(c_Union(c_Zorn_OTFin(v_S,t_a),tc_set(t_a)),v_m,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[f1774,f5092]) ).
fof(f5338,plain,
! [X0,X1] :
( c_emptyset = X0
| c_less(c_emptyset,X0,tc_set(X1)) ),
inference(resolution,[status(thm)],[f1774,f1770]) ).
fof(f5345,plain,
! [X0,X1,X2] :
( X0 = c_Zorn_Osucc(X1,X0,X2)
| c_less(X0,c_Zorn_Osucc(X1,X0,X2),tc_set(tc_set(X2))) ),
inference(resolution,[status(thm)],[f1774,f2846]) ).
fof(f5349,definition,
( sQ51_spl
<=> c_less(c_Union(c_Zorn_OTFin(v_S,t_a),tc_set(t_a)),v_m,tc_set(tc_set(t_a))) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f5350,plain,
( ~ sQ51_spl
| c_less(c_Union(c_Zorn_OTFin(v_S,t_a),tc_set(t_a)),v_m,tc_set(tc_set(t_a))) ),
inference(component_clause,[status(thm)],[f5349]) ).
fof(f5352,plain,
( ~ sQ3_spl
| sQ0_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f5335,f5349,f2854,f2870]) ).
fof(f5364,plain,
( ~ sQ49_spl
| c_in(v_m,c_Finite__Set_OFinites,tc_set(tc_set(t_a)))
| c_in(c_Main_Ofinite__Union__1(c_emptyset,tc_set(t_a)),c_emptyset,tc_set(tc_set(t_a)))
| ~ c_in(c_emptyset,c_Finite__Set_OFinites,tc_set(tc_set(tc_set(t_a)))) ),
inference(paramodulation,[status(thm)],[f5109,f1690]) ).
fof(f5374,definition,
! [X0,X1] :
( sQ55_spl
<=> X0 = X1 ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f5375,plain,
! [X0,X1] :
( ~ sQ55_spl
| X0 = X1 ),
inference(component_clause,[status(thm)],[f5374]) ).
fof(f5390,definition,
( sQ59_spl
<=> c_in(c_emptyset,c_Finite__Set_OFinites,tc_set(tc_set(tc_set(t_a)))) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f5392,plain,
( sQ59_spl
| ~ c_in(c_emptyset,c_Finite__Set_OFinites,tc_set(tc_set(tc_set(t_a)))) ),
inference(component_clause,[status(thm)],[f5390]) ).
fof(f5393,definition,
( sQ60_spl
<=> c_in(c_Main_Ofinite__Union__1(c_emptyset,tc_set(t_a)),c_emptyset,tc_set(tc_set(t_a))) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f5394,plain,
( ~ sQ60_spl
| c_in(c_Main_Ofinite__Union__1(c_emptyset,tc_set(t_a)),c_emptyset,tc_set(tc_set(t_a))) ),
inference(component_clause,[status(thm)],[f5393]) ).
fof(f5396,plain,
( ~ sQ49_spl
| sQ28_spl
| sQ60_spl
| ~ sQ59_spl ),
inference(split_clause,[status(thm)],[f5364,f5390,f5393,f4731,f5108]) ).
fof(f5398,plain,
( ~ sQ60_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5394,f1607]) ).
fof(f5399,plain,
~ sQ60_spl,
inference(contradiction_clause,[status(thm)],[f5398]) ).
fof(f5400,plain,
( sQ59_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5392,f1683]) ).
fof(f5401,plain,
sQ59_spl,
inference(contradiction_clause,[status(thm)],[f5400]) ).
fof(f5405,plain,
! [X0] :
( ~ class_Orderings_Oorder(tc_set(X0))
| c_emptyset = c_emptyset ),
inference(resolution,[status(thm)],[f5338,f1537]) ).
fof(f5406,definition,
! [X0] :
( sQ61_spl
<=> ~ class_Orderings_Oorder(tc_set(X0)) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f5407,plain,
! [X0] :
( ~ sQ61_spl
| ~ class_Orderings_Oorder(tc_set(X0)) ),
inference(component_clause,[status(thm)],[f5406]) ).
fof(f5409,plain,
( sQ61_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f5405,f2923,f5406]) ).
fof(f5410,plain,
( ~ sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5407,f1931]) ).
fof(f5411,plain,
~ sQ61_spl,
inference(contradiction_clause,[status(thm)],[f5410]) ).
fof(f5452,plain,
( ~ sQ55_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1478,f5375]) ).
fof(f5470,definition,
! [X0] :
( sQ66_spl
<=> ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_List_Olists(c_Union(c_UNIV,X0),X0),tc_List_Olist(X0)),tc_List_Olist(tc_List_Olist(X0))) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f5473,plain,
( sQ55_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f5272,f5470,f5374]) ).
fof(f5474,definition,
! [X0] :
( sQ67_spl
<=> ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_List_Olists(c_Union(c_Finite__Set_OFinites,X0),X0),tc_List_Olist(X0)),tc_List_Olist(tc_List_Olist(X0))) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f5477,plain,
( sQ55_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f5265,f5474,f5374]) ).
fof(f5478,definition,
! [X0] :
( sQ68_spl
<=> ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_Union(c_UNIV,X0),X0),tc_List_Olist(X0)) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f5481,plain,
( sQ55_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f5240,f5478,f5374]) ).
fof(f5482,definition,
! [X0] :
( sQ69_spl
<=> ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_Union(c_Finite__Set_OFinites,X0),X0),tc_List_Olist(X0)) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f5485,plain,
( sQ55_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f5233,f5482,f5374]) ).
fof(f5486,definition,
! [X0] :
( sQ70_spl
<=> ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_UNIV,X0),tc_List_Olist(X0)) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f5489,plain,
( sQ55_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f5191,f5486,f5374]) ).
fof(f5490,definition,
! [X0,X1] :
( sQ71_spl
<=> ( ~ c_Infinite__Set_Oatmost__one(c_List_Olists(c_Union(X0,X1),X1),tc_List_Olist(X1))
| ~ c_in(c_UNIV,X0,tc_set(X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f5493,plain,
( sQ55_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f5135,f5490,f5374]) ).
fof(f5494,definition,
! [X0] :
( sQ72_spl
<=> ~ c_Infinite__Set_Oatmost__one(c_UNIV,X0) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f5497,plain,
( sQ55_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f4868,f5494,f5374]) ).
fof(f5514,plain,
! [X0] :
( ~ sQ0_spl
| c_lessequals(X0,v_m,tc_set(tc_set(t_a)))
| ~ c_in(X0,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
inference(paramodulation,[status(thm)],[f2855,f2845]) ).
fof(f5521,plain,
! [X0,X1,X2] :
( ~ c_lessequals(c_Zorn_Osucc(X1,X0,X2),X0,tc_set(tc_set(X2)))
| X0 = c_Zorn_Osucc(X1,X0,X2) ),
inference(resolution,[status(thm)],[f5345,f1771]) ).
fof(f5522,plain,
( ~ sQ3_spl
| ~ c_in(v_m,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| v_m = c_Zorn_Osucc(v_S,v_m,t_a) ),
inference(resolution,[status(thm)],[f5521,f4623]) ).
fof(f5524,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f5522,f2857,f2864,f2870]) ).
fof(f5525,plain,
~ sQ55_spl,
inference(contradiction_clause,[status(thm)],[f5452]) ).
fof(f5577,plain,
( ~ sQ51_spl
| ~ c_lessequals(v_m,c_Union(c_Zorn_OTFin(v_S,t_a),tc_set(t_a)),tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[f5350,f1771]) ).
fof(f5578,plain,
( ~ sQ51_spl
| ~ c_in(v_m,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[f5577,f2845]) ).
fof(f5579,plain,
( ~ sQ51_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f5578,f2864,f5349]) ).
fof(f5580,plain,
( ~ sQ0_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f5514,f2870,f2854]) ).
fof(f5583,plain,
$false,
inference(sat_refutation,[status(thm)],[f2860,f2861,f2873,f3342,f3682,f3684,f3721,f3724,f3802,f3807,f4589,f4631,f4633,f4736,f4860,f4968,f4970,f4989,f5111,f5352,f5396,f5399,f5401,f5409,f5411,f5473,f5477,f5481,f5485,f5489,f5493,f5497,f5524,f5525,f5579,f5580]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SET843-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Mon Sep 21 05:40:54 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.07/0.32 % Drodi V4.1.1
% 0.07/0.39 % Refutation found
% 0.07/0.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.07/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.07/0.41 % Elapsed time: 0.104083 seconds
% 0.07/0.41 % CPU time: 0.511741 seconds
% 0.07/0.41 % Total memory used: 166.093 MB
% 0.07/0.41 % Net memory used: 165.158 MB
%------------------------------------------------------------------------------