%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU301+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:41:35 AM UTC 2026
% Result : Theorem 64.73s 8.81s
% Output : CNFRefutation 64.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU301+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n020.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 09:09:19 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 64.73/8.81 % SZS status Theorem for theBenchmark.p
% 64.73/8.81 % SZS output start CNFRefutation for theBenchmark.p
% 64.73/8.81 fof(cc3_arytm_3, axiom, ! [X0] : ((element(X0,omega) => ('epsilon$utransitive'(X0) & ('epsilon$uconnected'(X0) & (ordinal(X0) & natural(X0))))))).
% 64.73/8.81 fof(s2_ordinal1__e18_27__finset_1__1, axiom, (! [X0] : ((ordinal(X0) => (! [X1] : ((ordinal(X1) => (in(X1,X0) => (in(X1,omega) => ! [X2] : ((element(X2,powerset(powerset(X1))) => ~((X2 != 'empty$uset' & ! [X3] : ~((in(X3,X2) & ! [X4] : (((in(X4,X2) & subset(X3,X4)) => X4 = X3)))))))))))) => (in(X0,omega) => ! [X5] : ((element(X5,powerset(powerset(X0))) => ~((X5 != 'empty$uset' & ! [X6] : ~((in(X6,X5) & ! [X7] : (((in(X7,X5) & subset(X6,X7)) => X7 = X6)))))))))))) => ! [X0] : ((ordinal(X0) => (in(X0,omega) => ! [X8] : ((element(X8,powerset(powerset(X0))) => ~((X8 != 'empty$uset' & ! [X9] : ~((in(X9,X8) & ! [X10] : (((in(X10,X8) & subset(X9,X10)) => X10 = X9))))))))))))).
% 64.73/8.81 fof(t10_ordinal1, axiom, ! [X0] : in(X0,succ(X0))).
% 64.73/8.81 fof(t1_subset, axiom, ! [X0] : ! [X1] : ((in(X0,X1) => element(X0,X1)))).
% 64.73/8.81 fof(t42_ordinal1, axiom, ! [X0] : ((ordinal(X0) => (~((~'being$ulimit$uordinal'(X0) & ! [X1] : ((ordinal(X1) => X0 != succ(X1))))) & ~((? [X1] : ((ordinal(X1) & X0 = succ(X1))) & 'being$ulimit$uordinal'(X0))))))).
% 64.73/8.81 fof(s1_ordinal2__e18_27__finset_1, conjecture, (((in('empty$uset',omega) => ! [X0] : ((element(X0,powerset(powerset('empty$uset'))) => ~((X0 != 'empty$uset' & ! [X1] : ~((in(X1,X0) & ! [X2] : (((in(X2,X0) & subset(X1,X2)) => X2 = X1))))))))) & (! [X3] : ((ordinal(X3) => ((in(X3,omega) => ! [X4] : ((element(X4,powerset(powerset(X3))) => ~((X4 != 'empty$uset' & ! [X5] : ~((in(X5,X4) & ! [X6] : (((in(X6,X4) & subset(X5,X6)) => X6 = X5))))))))) => (in(succ(X3),omega) => ! [X7] : ((element(X7,powerset(powerset(succ(X3)))) => ~((X7 != 'empty$uset' & ! [X8] : ~((in(X8,X7) & ! [X9] : (((in(X9,X7) & subset(X8,X9)) => X9 = X8)))))))))))) & ! [X3] : ((ordinal(X3) => (('being$ulimit$uordinal'(X3) & ! [X10] : ((ordinal(X10) => (in(X10,X3) => (in(X10,omega) => ! [X11] : ((element(X11,powerset(powerset(X10))) => ~((X11 != 'empty$uset' & ! [X12] : ~((in(X12,X11) & ! [X13] : (((in(X13,X11) & subset(X12,X13)) => X13 = X12))))))))))))) => (X3 = 'empty$uset' | (in(X3,omega) => ! [X14] : ((element(X14,powerset(powerset(X3))) => ~((X14 != 'empty$uset' & ! [X15] : ~((in(X15,X14) & ! [X16] : (((in(X16,X14) & subset(X15,X16)) => X16 = X15))))))))))))))) => ! [X3] : ((ordinal(X3) => (in(X3,omega) => ! [X17] : ((element(X17,powerset(powerset(X3))) => ~((X17 != 'empty$uset' & ! [X18] : ~((in(X18,X17) & ! [X19] : (((in(X19,X17) & subset(X18,X19)) => X19 = X18))))))))))))).
% 64.73/8.81 fof(negated_conjecture, negated_conjecture, ~((((in('empty$uset',omega) => ! [X0] : ((element(X0,powerset(powerset('empty$uset'))) => ~((X0 != 'empty$uset' & ! [X1] : ~((in(X1,X0) & ! [X2] : (((in(X2,X0) & subset(X1,X2)) => X2 = X1))))))))) & (! [X3] : ((ordinal(X3) => ((in(X3,omega) => ! [X4] : ((element(X4,powerset(powerset(X3))) => ~((X4 != 'empty$uset' & ! [X5] : ~((in(X5,X4) & ! [X6] : (((in(X6,X4) & subset(X5,X6)) => X6 = X5))))))))) => (in(succ(X3),omega) => ! [X7] : ((element(X7,powerset(powerset(succ(X3)))) => ~((X7 != 'empty$uset' & ! [X8] : ~((in(X8,X7) & ! [X9] : (((in(X9,X7) & subset(X8,X9)) => X9 = X8)))))))))))) & ! [X3] : ((ordinal(X3) => (('being$ulimit$uordinal'(X3) & ! [X10] : ((ordinal(X10) => (in(X10,X3) => (in(X10,omega) => ! [X11] : ((element(X11,powerset(powerset(X10))) => ~((X11 != 'empty$uset' & ! [X12] : ~((in(X12,X11) & ! [X13] : (((in(X13,X11) & subset(X12,X13)) => X13 = X12))))))))))))) => (X3 = 'empty$uset' | (in(X3,omega) => ! [X14] : ((element(X14,powerset(powerset(X3))) => ~((X14 != 'empty$uset' & ! [X15] : ~((in(X15,X14) & ! [X16] : (((in(X16,X14) & subset(X15,X16)) => X16 = X15))))))))))))))) => ! [X3] : ((ordinal(X3) => (in(X3,omega) => ! [X17] : ((element(X17,powerset(powerset(X3))) => ~((X17 != 'empty$uset' & ! [X18] : ~((in(X18,X17) & ! [X19] : (((in(X19,X17) & subset(X18,X19)) => X19 = X18))))))))))))), inference(negate_conjecture, [status(cth)], [s1_ordinal2__e18_27__finset_1])).
% 64.73/8.81 cnf(c98, plain, ~element(X0,omega) | ordinal(X0), inference(clausification, [status(esa)], [cc3_arytm_3])).
% 64.73/8.81 cnf(c117, plain, ~in(X0,omega) | X1 | ~ordinal(X0) | ~element(X2,powerset(powerset(X0))) | in(sK48(X2),X2) | X2 = 'empty$uset', inference(clausification, [status(esa)], [s2_ordinal1__e18_27__finset_1__1])).
% 64.73/8.81 cnf(c118, plain, ~in(X0,omega) | X1 | X2 = sK48(X3) | ~ordinal(X0) | ~element(X3,powerset(powerset(X0))) | X3 = 'empty$uset' | ~in(X2,X3) | ~subset(sK48(X3),X2), inference(clausification, [status(esa)], [s2_ordinal1__e18_27__finset_1__1])).
% 64.73/8.81 cnf(c119, plain, ~X0 | ordinal(sK50), inference(clausification, [status(esa)], [s2_ordinal1__e18_27__finset_1__1])).
% 64.73/8.81 cnf(c120, plain, X0 = 'empty$uset' | ~in(X1,omega) | in(sK53(X0),X0) | ~in(X1,sK50) | ~element(X0,powerset(powerset(X1))) | ~ordinal(X1) | ~X2, inference(clausification, [status(esa)], [s2_ordinal1__e18_27__finset_1__1])).
% 64.73/8.81 cnf(c121, plain, ~in(X0,X1) | X1 = 'empty$uset' | ~subset(sK53(X1),X0) | ~in(X2,omega) | X0 = sK53(X1) | ~in(X2,sK50) | ~element(X1,powerset(powerset(X2))) | ~ordinal(X2) | ~X3, inference(clausification, [status(esa)], [s2_ordinal1__e18_27__finset_1__1])).
% 64.73/8.81 cnf(c122, plain, ~X0 | in(sK50,omega), inference(clausification, [status(esa)], [s2_ordinal1__e18_27__finset_1__1])).
% 64.73/8.81 cnf(c123, plain, ~X0 | element(sK55,powerset(powerset(sK50))), inference(clausification, [status(esa)], [s2_ordinal1__e18_27__finset_1__1])).
% 64.73/8.81 cnf(c124, plain, ~X0 | sK55 != 'empty$uset', inference(clausification, [status(esa)], [s2_ordinal1__e18_27__finset_1__1])).
% 64.73/8.81 cnf(c125, plain, ~X0 | ~in(X1,sK55) | in(sK57(X1),sK55), inference(clausification, [status(esa)], [s2_ordinal1__e18_27__finset_1__1])).
% 64.73/8.81 cnf(c126, plain, ~X0 | ~in(X1,sK55) | subset(X1,sK57(X1)), inference(clausification, [status(esa)], [s2_ordinal1__e18_27__finset_1__1])).
% 64.73/8.81 cnf(c127, plain, ~X0 | ~in(X1,sK55) | sK57(X1) != X1, inference(clausification, [status(esa)], [s2_ordinal1__e18_27__finset_1__1])).
% 64.73/8.81 cnf(c135, plain, in(X0,succ(X0)), inference(clausification, [status(esa)], [t10_ordinal1])).
% 64.73/8.81 cnf(c137, plain, ~in(X0,X1) | element(X0,X1), inference(clausification, [status(esa)], [t1_subset])).
% 64.73/8.81 cnf(c139, plain, ~ordinal(X0) | 'being$ulimit$uordinal'(X0) | ordinal(sK77(X0)), inference(clausification, [status(esa)], [t42_ordinal1])).
% 64.73/8.81 cnf(c140, plain, ~ordinal(X0) | 'being$ulimit$uordinal'(X0) | X0 = succ(sK77(X0)), inference(clausification, [status(esa)], [t42_ordinal1])).
% 64.73/8.81 cnf(c145, plain, ~in('empty$uset',omega) | ~element(X0,powerset(powerset('empty$uset'))) | X0 = 'empty$uset' | in(sK87(X0),X0), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c146, plain, X0 = sK87(X1) | ~in('empty$uset',omega) | ~in(X0,X1) | ~element(X1,powerset(powerset('empty$uset'))) | X1 = 'empty$uset' | ~subset(sK87(X1),X0), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c147, plain, X0(X1) | ~in(succ(X1),omega) | ~ordinal(X1) | in(sK91(X2),X2) | ~element(X2,powerset(powerset(succ(X1)))) | X2 = 'empty$uset', inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c148, plain, X0 = sK91(X1) | X2(X3) | ~subset(sK91(X1),X0) | ~in(succ(X3),omega) | ~ordinal(X3) | X1 = 'empty$uset' | ~in(X0,X1) | ~element(X1,powerset(powerset(succ(X3)))), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c149, plain, ~'being$ulimit$uordinal'(X0) | X0 = 'empty$uset' | ~ordinal(X0) | ~X1(X0) | ~element(X2,powerset(powerset(X0))) | ~in(X0,omega) | in(sK95(X2),X2) | X2 = 'empty$uset', inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c150, plain, ~'being$ulimit$uordinal'(X0) | X0 = 'empty$uset' | ~subset(sK95(X1),X2) | ~ordinal(X0) | X1 = 'empty$uset' | X2 = sK95(X1) | ~in(X2,X1) | ~X3(X0) | ~element(X1,powerset(powerset(X0))) | ~in(X0,omega), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c151, plain, ordinal(sK97), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c152, plain, in(sK97,omega), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c153, plain, element(sK98,powerset(powerset(sK97))), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c154, plain, sK98 != 'empty$uset', inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c155, plain, ~in(X0,sK98) | in(sK100(X0),sK98), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c156, plain, ~in(X0,sK98) | subset(X0,sK100(X0)), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c157, plain, ~in(X0,sK98) | sK100(X0) != X0, inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c158, plain, ~X0(X1) | in(X1,omega), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c159, plain, ~X0(X1) | element(sK101(X1),powerset(powerset(X1))), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c160, plain, ~X0(X1) | sK101(X1) != 'empty$uset', inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c161, plain, ~X0(X1) | ~in(X2,sK101(X1)) | in(sK103(X1,X2),sK101(X1)), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c162, plain, ~X0(X1) | ~in(X2,sK101(X1)) | subset(X2,sK103(X1,X2)), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c163, plain, ~X0(X1) | ~in(X2,sK101(X1)) | sK103(X1,X2) != X2, inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c164, plain, X0(X1) | ordinal(sK104(X1)), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c165, plain, X0(X1) | in(sK104(X1),X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c166, plain, X0(X1) | in(sK104(X1),omega), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c167, plain, X0(X1) | element(sK105(X1),powerset(powerset(sK104(X1)))), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c168, plain, X0(X1) | sK105(X1) != 'empty$uset', inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c169, plain, X0(X1) | ~in(X2,sK105(X1)) | in(sK107(X1,X2),sK105(X1)), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c170, plain, X0(X1) | ~in(X2,sK105(X1)) | subset(X2,sK107(X1,X2)), inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(c171, plain, X0(X1) | ~in(X2,sK105(X1)) | sK107(X1,X2) != X2, inference(clausification, [status(esa)], [negated_conjecture])).
% 64.73/8.81 cnf(d0, plain, sK98 = 'empty$uset' | ~ordinal(sK97) | ~in(sK97,omega) | in(sK48(sK98),sK98) | 'Ts45', inference(resolution, [status(thm)], [c117,c153])).
% 64.73/8.81 cnf(d1, plain, sK98 = 'empty$uset' | in(sK48(sK98),sK98) | ~in(sK97,omega) | 'Ts45', inference(resolution, [status(thm)], [c151,d0])).
% 64.73/8.81 cnf(d2, plain, sK98 = 'empty$uset' | in(sK48(sK98),sK98) | 'Ts45', inference(resolution, [status(thm)], [c152,d1])).
% 64.73/8.81 cnf(d3, plain, in(sK48(sK98),sK98) | 'Ts45', inference(resolution, [status(thm)], [c154,d2])).
% 64.73/8.81 cnf(d4, plain, X0 = sK48(sK98) | sK98 = 'empty$uset' | ~ordinal(sK97) | ~subset(sK48(sK98),X0) | ~in(sK97,omega) | ~in(X0,sK98) | 'Ts45', inference(resolution, [status(thm)], [c118,c153])).
% 64.73/8.81 cnf(d5, plain, X0 = sK48(sK98) | sK98 = 'empty$uset' | ~subset(sK48(sK98),X0) | ~in(X0,sK98) | ~in(sK97,omega) | 'Ts45', inference(resolution, [status(thm)], [c151,d4])).
% 64.73/8.81 cnf(d6, plain, X0 = sK48(sK98) | sK98 = 'empty$uset' | ~subset(sK48(sK98),X0) | ~in(X0,sK98) | 'Ts45', inference(resolution, [status(thm)], [c152,d5])).
% 64.73/8.81 cnf(d7, plain, X0 = sK48(sK98) | ~subset(sK48(sK98),X0) | ~in(X0,sK98) | 'Ts45', inference(resolution, [status(thm)], [c154,d6])).
% 64.73/8.81 cnf(d8, plain, sK100(sK48(sK98)) = sK48(sK98) | ~in(sK100(sK48(sK98)),sK98) | 'Ts45' | ~in(sK48(sK98),sK98), inference(resolution, [status(thm)], [d7,c156])).
% 64.73/8.81 cnf(d9, plain, sK48(sK98) != sK48(sK98) | ~in(sK48(sK98),sK98) | ~in(sK48(sK98),sK98) | ~in(sK100(sK48(sK98)),sK98) | 'Ts45', inference(superposition, [status(thm)], [d8,c157])).
% 64.73/8.81 cnf(d10, plain, ~in(sK48(sK98),sK98) | ~in(sK100(sK48(sK98)),sK98) | 'Ts45', inference(equality_resolution, [status(thm)], [d9])).
% 64.73/8.81 cnf(d11, plain, ~in(sK48(sK98),sK98) | 'Ts45' | ~in(sK48(sK98),sK98), inference(resolution, [status(thm)], [d10,c155])).
% 64.73/8.81 cnf(d12, plain, 'Ts45' | 'Ts45', inference(resolution, [status(thm)], [d11,d3])).
% 64.73/8.81 cnf(d13, plain, X0 = 'empty$uset' | ~element(X0,powerset(powerset(X1))) | ~ordinal(X1) | ~in(X1,omega) | ~in(X1,sK50) | in(sK53(X0),X0), inference(resolution, [status(thm)], [d12,c120])).
% 64.73/8.81 cnf(d14, plain, sK105(X0) = 'empty$uset' | ~ordinal(sK104(X0)) | ~in(sK104(X0),omega) | ~in(sK104(X0),sK50) | in(sK53(sK105(X0)),sK105(X0)) | 'Ts85'(X0), inference(resolution, [status(thm)], [d13,c167])).
% 64.73/8.81 cnf(d15, plain, X0 = sK53(X1) | X1 = 'empty$uset' | ~element(X1,powerset(powerset(X2))) | ~ordinal(X2) | ~subset(sK53(X1),X0) | ~in(X0,X1) | ~in(X2,omega) | ~in(X2,sK50), inference(resolution, [status(thm)], [d12,c121])).
% 64.73/8.81 cnf(d16, plain, sK105(X0) = 'empty$uset' | X1 = sK53(sK105(X0)) | ~ordinal(sK104(X0)) | ~subset(sK53(sK105(X0)),X1) | ~in(sK104(X0),omega) | ~in(sK104(X0),sK50) | ~in(X1,sK105(X0)) | 'Ts85'(X0), inference(resolution, [status(thm)], [d15,c167])).
% 64.73/8.81 cnf(d17, plain, sK107(X0,sK53(sK105(X1))) = sK53(sK105(X1)) | sK105(X1) = 'empty$uset' | ~ordinal(sK104(X1)) | ~in(sK107(X0,sK53(sK105(X1))),sK105(X1)) | ~in(sK104(X1),omega) | ~in(sK104(X1),sK50) | 'Ts85'(X1) | ~in(sK53(sK105(X1)),sK105(X0)) | 'Ts85'(X0), inference(resolution, [status(thm)], [d16,c170])).
% 64.73/8.81 cnf(d18, plain, sK53(sK105(X1)) != sK53(sK105(X1)) | ~in(sK53(sK105(X1)),sK105(X0)) | 'Ts85'(X0) | sK105(X1) = 'empty$uset' | ~ordinal(sK104(X1)) | ~in(sK53(sK105(X1)),sK105(X0)) | ~in(sK104(X1),omega) | ~in(sK104(X1),sK50) | ~in(sK107(X0,sK53(sK105(X1))),sK105(X1)) | 'Ts85'(X1) | 'Ts85'(X0), inference(superposition, [status(thm)], [d17,c171])).
% 64.73/8.81 cnf(d19, plain, sK105(X0) = 'empty$uset' | ~ordinal(sK104(X0)) | ~in(sK53(sK105(X0)),sK105(X1)) | ~in(sK104(X0),omega) | ~in(sK104(X0),sK50) | ~in(sK107(X1,sK53(sK105(X0))),sK105(X0)) | 'Ts85'(X0) | 'Ts85'(X1), inference(equality_resolution, [status(thm)], [d18])).
% 64.73/8.81 cnf(d20, plain, sK105(X0) = 'empty$uset' | ~ordinal(sK104(X0)) | ~in(sK53(sK105(X0)),sK105(X0)) | ~in(sK104(X0),omega) | ~in(sK104(X0),sK50) | 'Ts85'(X0) | 'Ts85'(X0) | ~in(sK53(sK105(X0)),sK105(X0)) | 'Ts85'(X0), inference(resolution, [status(thm)], [d19,c169])).
% 64.73/8.81 cnf(d21, plain, sK105(X0) = 'empty$uset' | ~ordinal(sK104(X0)) | ~in(sK104(X0),omega) | ~in(sK104(X0),sK50) | 'Ts85'(X0) | sK105(X0) = 'empty$uset' | ~ordinal(sK104(X0)) | ~in(sK104(X0),omega) | ~in(sK104(X0),sK50) | 'Ts85'(X0), inference(resolution, [status(thm)], [d20,d14])).
% 64.73/8.81 cnf(d22, plain, sK105(sK50) = 'empty$uset' | ~ordinal(sK104(sK50)) | ~in(sK104(sK50),omega) | 'Ts85'(sK50) | 'Ts85'(sK50), inference(resolution, [status(thm)], [d21,c165])).
% 64.73/8.81 cnf(d23, plain, in(sK50,omega), inference(resolution, [status(thm)], [d12,c122])).
% 64.73/8.81 cnf(d24, plain, element(sK55,powerset(powerset(sK50))), inference(resolution, [status(thm)], [d12,c123])).
% 64.73/8.81 cnf(d25, plain, sK55 = 'empty$uset' | sK50 = 'empty$uset' | ~ordinal(sK50) | ~'being$ulimit$uordinal'(sK50) | ~in(sK50,omega) | in(sK95(sK55),sK55) | ~'Ts85'(sK50), inference(resolution, [status(thm)], [d24,c149])).
% 64.73/8.81 cnf(d26, plain, ordinal(sK50), inference(resolution, [status(thm)], [d12,c119])).
% 64.73/8.81 cnf(d27, plain, sK50 = 'empty$uset' | sK55 = 'empty$uset' | ~'being$ulimit$uordinal'(sK50) | ~in(sK50,omega) | in(sK95(sK55),sK55) | ~'Ts85'(sK50), inference(resolution, [status(thm)], [d26,d25])).
% 64.73/8.81 cnf(d28, plain, sK55 != 'empty$uset', inference(resolution, [status(thm)], [d12,c124])).
% 64.73/8.81 cnf(d29, plain, sK50 = 'empty$uset' | ~'being$ulimit$uordinal'(sK50) | ~in(sK50,omega) | in(sK95(sK55),sK55) | ~'Ts85'(sK50), inference(resolution, [status(thm)], [d28,d27])).
% 64.73/8.81 cnf(d30, plain, sK50 = 'empty$uset' | ~'being$ulimit$uordinal'(sK50) | in(sK95(sK55),sK55) | ~'Ts85'(sK50), inference(resolution, [status(thm)], [d23,d29])).
% 64.73/8.81 cnf(d31, plain, ~in(X0,sK55) | in(sK57(X0),sK55), inference(resolution, [status(thm)], [d12,c125])).
% 64.73/8.81 cnf(d32, plain, sK57(X0) != X0 | ~in(X0,sK55), inference(resolution, [status(thm)], [d12,c127])).
% 64.73/8.81 cnf(d33, plain, sK55 = 'empty$uset' | X0 = sK95(sK55) | sK50 = 'empty$uset' | ~ordinal(sK50) | ~'being$ulimit$uordinal'(sK50) | ~subset(sK95(sK55),X0) | ~in(X0,sK55) | ~in(sK50,omega) | ~'Ts85'(sK50), inference(resolution, [status(thm)], [d24,c150])).
% 64.73/8.81 cnf(d34, plain, X0 = sK95(sK55) | sK50 = 'empty$uset' | sK55 = 'empty$uset' | ~'being$ulimit$uordinal'(sK50) | ~subset(sK95(sK55),X0) | ~in(X0,sK55) | ~in(sK50,omega) | ~'Ts85'(sK50), inference(resolution, [status(thm)], [d26,d33])).
% 64.73/8.81 cnf(d35, plain, X0 = sK95(sK55) | sK50 = 'empty$uset' | ~'being$ulimit$uordinal'(sK50) | ~subset(sK95(sK55),X0) | ~in(X0,sK55) | ~in(sK50,omega) | ~'Ts85'(sK50), inference(resolution, [status(thm)], [d28,d34])).
% 64.73/8.81 cnf(d36, plain, X0 = sK95(sK55) | sK50 = 'empty$uset' | ~'being$ulimit$uordinal'(sK50) | ~subset(sK95(sK55),X0) | ~in(X0,sK55) | ~'Ts85'(sK50), inference(resolution, [status(thm)], [d23,d35])).
% 64.73/8.81 cnf(d37, plain, subset(X0,sK57(X0)) | ~in(X0,sK55), inference(resolution, [status(thm)], [d12,c126])).
% 64.73/8.81 cnf(d38, plain, ~in(sK95(sK55),sK55) | sK57(sK95(sK55)) = sK95(sK55) | sK50 = 'empty$uset' | ~'being$ulimit$uordinal'(sK50) | ~in(sK57(sK95(sK55)),sK55) | ~'Ts85'(sK50), inference(resolution, [status(thm)], [d37,d36])).
% 64.73/8.81 cnf(d39, plain, sK95(sK55) != sK95(sK55) | ~in(sK95(sK55),sK55) | sK50 = 'empty$uset' | ~'being$ulimit$uordinal'(sK50) | ~in(sK57(sK95(sK55)),sK55) | ~in(sK95(sK55),sK55) | ~'Ts85'(sK50), inference(superposition, [status(thm)], [d38,d32])).
% 64.73/8.81 cnf(d40, plain, sK50 = 'empty$uset' | ~'being$ulimit$uordinal'(sK50) | ~in(sK57(sK95(sK55)),sK55) | ~in(sK95(sK55),sK55) | ~'Ts85'(sK50), inference(equality_resolution, [status(thm)], [d39])).
% 64.73/8.81 cnf(d41, plain, sK50 = 'empty$uset' | ~'being$ulimit$uordinal'(sK50) | ~in(sK95(sK55),sK55) | ~'Ts85'(sK50) | ~in(sK95(sK55),sK55), inference(resolution, [status(thm)], [d40,d31])).
% 64.73/8.81 cnf(d42, plain, sK50 = 'empty$uset' | ~'being$ulimit$uordinal'(sK50) | ~'Ts85'(sK50) | sK50 = 'empty$uset' | ~'being$ulimit$uordinal'(sK50) | ~'Ts85'(sK50), inference(resolution, [status(thm)], [d41,d30])).
% 64.73/8.81 cnf(d43, plain, in('empty$uset',omega) | ~'being$ulimit$uordinal'(sK50) | ~'Ts85'(sK50), inference(superposition, [status(thm)], [d42,d23])).
% 64.73/8.81 cnf(d44, plain, element(sK55,powerset(powerset('empty$uset'))) | ~'being$ulimit$uordinal'(sK50) | ~'Ts85'(sK50), inference(superposition, [status(thm)], [d42,d24])).
% 64.73/8.81 cnf(d45, plain, ~'being$ulimit$uordinal'(sK50) | ~'Ts85'(sK50) | sK55 = 'empty$uset' | ~in('empty$uset',omega) | in(sK87(sK55),sK55), inference(resolution, [status(thm)], [d44,c145])).
% 64.73/8.81 cnf(d46, plain, ~'being$ulimit$uordinal'(sK50) | ~in('empty$uset',omega) | in(sK87(sK55),sK55) | ~'Ts85'(sK50), inference(resolution, [status(thm)], [d28,d45])).
% 64.73/8.81 cnf(d47, plain, ~'being$ulimit$uordinal'(sK50) | ~'Ts85'(sK50) | X0 = sK87(sK55) | sK55 = 'empty$uset' | ~subset(sK87(sK55),X0) | ~in(X0,sK55) | ~in('empty$uset',omega), inference(resolution, [status(thm)], [d44,c146])).
% 64.73/8.81 cnf(d48, plain, X0 = sK87(sK55) | ~'being$ulimit$uordinal'(sK50) | ~subset(sK87(sK55),X0) | ~in(X0,sK55) | ~in('empty$uset',omega) | ~'Ts85'(sK50), inference(resolution, [status(thm)], [d28,d47])).
% 64.73/8.81 cnf(d49, plain, sK57(sK87(sK55)) = sK87(sK55) | ~'being$ulimit$uordinal'(sK50) | ~in(sK57(sK87(sK55)),sK55) | ~in('empty$uset',omega) | ~'Ts85'(sK50) | ~in(sK87(sK55),sK55), inference(resolution, [status(thm)], [d48,d37])).
% 64.73/8.81 cnf(d50, plain, sK87(sK55) != sK87(sK55) | ~in(sK87(sK55),sK55) | ~'being$ulimit$uordinal'(sK50) | ~in('empty$uset',omega) | ~in(sK57(sK87(sK55)),sK55) | ~in(sK87(sK55),sK55) | ~'Ts85'(sK50), inference(superposition, [status(thm)], [d49,d32])).
% 64.73/8.81 cnf(d51, plain, ~'being$ulimit$uordinal'(sK50) | ~in('empty$uset',omega) | ~in(sK57(sK87(sK55)),sK55) | ~in(sK87(sK55),sK55) | ~'Ts85'(sK50), inference(equality_resolution, [status(thm)], [d50])).
% 64.73/8.81 cnf(d52, plain, ~'being$ulimit$uordinal'(sK50) | ~in('empty$uset',omega) | ~in(sK87(sK55),sK55) | ~'Ts85'(sK50) | ~in(sK87(sK55),sK55), inference(resolution, [status(thm)], [d51,d31])).
% 64.73/8.81 cnf(d53, plain, ~'being$ulimit$uordinal'(sK50) | ~in('empty$uset',omega) | ~'Ts85'(sK50) | ~'being$ulimit$uordinal'(sK50) | ~in('empty$uset',omega) | ~'Ts85'(sK50), inference(resolution, [status(thm)], [d52,d46])).
% 64.73/8.81 cnf(d54, plain, ~'being$ulimit$uordinal'(sK50) | ~'Ts85'(sK50) | ~'being$ulimit$uordinal'(sK50) | ~'Ts85'(sK50), inference(resolution, [status(thm)], [d53,d43])).
% 64.73/8.81 cnf(d55, plain, element(X0,omega) | ~'Ts84'(X0), inference(resolution, [status(thm)], [c137,c158])).
% 64.73/8.81 cnf(d56, plain, ~'Ts84'(X0) | ordinal(X0), inference(resolution, [status(thm)], [d55,c98])).
% 64.73/8.81 cnf(d57, plain, ~element(X1,powerset(powerset(X0))) | X1 = 'empty$uset' | ~ordinal(sK77(X0)) | ~in(succ(sK77(X0)),omega) | in(sK91(X1),X1) | 'Ts84'(sK77(X0)) | ~ordinal(X0) | 'being$ulimit$uordinal'(X0), inference(superposition, [status(thm)], [c140,c147])).
% 64.73/8.81 cnf(d58, plain, ~in(X0,omega) | X1 = 'empty$uset' | ~element(X1,powerset(powerset(X0))) | ~ordinal(X0) | ~ordinal(sK77(X0)) | 'being$ulimit$uordinal'(X0) | in(sK91(X1),X1) | 'Ts84'(sK77(X0)) | ~ordinal(X0) | 'being$ulimit$uordinal'(X0), inference(superposition, [status(thm)], [c140,d57])).
% 64.73/8.81 cnf(d59, plain, sK55 = 'empty$uset' | ~ordinal(sK50) | ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | ~in(sK50,omega) | in(sK91(sK55),sK55) | 'Ts84'(sK77(sK50)), inference(resolution, [status(thm)], [d58,d24])).
% 64.73/8.81 cnf(d60, plain, sK55 = 'empty$uset' | ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | ~in(sK50,omega) | in(sK91(sK55),sK55) | 'Ts84'(sK77(sK50)), inference(resolution, [status(thm)], [d26,d59])).
% 64.73/8.81 cnf(d61, plain, ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | ~in(sK50,omega) | in(sK91(sK55),sK55) | 'Ts84'(sK77(sK50)), inference(resolution, [status(thm)], [d28,d60])).
% 64.73/8.81 cnf(d62, plain, ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | in(sK91(sK55),sK55) | 'Ts84'(sK77(sK50)), inference(resolution, [status(thm)], [d23,d61])).
% 64.73/8.81 cnf(d63, plain, ~element(X1,powerset(powerset(X0))) | X2 = sK91(X1) | X1 = 'empty$uset' | ~ordinal(sK77(X0)) | ~subset(sK91(X1),X2) | ~in(X2,X1) | ~in(succ(sK77(X0)),omega) | 'Ts84'(sK77(X0)) | ~ordinal(X0) | 'being$ulimit$uordinal'(X0), inference(superposition, [status(thm)], [c140,c148])).
% 64.73/8.81 cnf(d64, plain, ~in(X0,omega) | X1 = sK91(X2) | X2 = 'empty$uset' | ~element(X2,powerset(powerset(X0))) | ~ordinal(X0) | ~ordinal(sK77(X0)) | 'being$ulimit$uordinal'(X0) | ~subset(sK91(X2),X1) | ~in(X1,X2) | 'Ts84'(sK77(X0)) | ~ordinal(X0) | 'being$ulimit$uordinal'(X0), inference(superposition, [status(thm)], [c140,d63])).
% 64.73/8.81 cnf(d65, plain, sK55 = 'empty$uset' | X0 = sK91(sK55) | ~ordinal(sK50) | ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | ~subset(sK91(sK55),X0) | ~in(X0,sK55) | ~in(sK50,omega) | 'Ts84'(sK77(sK50)), inference(resolution, [status(thm)], [d64,d24])).
% 64.73/8.81 cnf(d66, plain, X0 = sK91(sK55) | sK55 = 'empty$uset' | ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | ~subset(sK91(sK55),X0) | ~in(X0,sK55) | ~in(sK50,omega) | 'Ts84'(sK77(sK50)), inference(resolution, [status(thm)], [d26,d65])).
% 64.73/8.81 cnf(d67, plain, X0 = sK91(sK55) | ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | ~subset(sK91(sK55),X0) | ~in(X0,sK55) | ~in(sK50,omega) | 'Ts84'(sK77(sK50)), inference(resolution, [status(thm)], [d28,d66])).
% 64.73/8.81 cnf(d68, plain, X0 = sK91(sK55) | ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | ~subset(sK91(sK55),X0) | ~in(X0,sK55) | 'Ts84'(sK77(sK50)), inference(resolution, [status(thm)], [d23,d67])).
% 64.73/8.81 cnf(d69, plain, sK57(sK91(sK55)) = sK91(sK55) | ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | ~in(sK57(sK91(sK55)),sK55) | 'Ts84'(sK77(sK50)) | ~in(sK91(sK55),sK55), inference(resolution, [status(thm)], [d68,d37])).
% 64.73/8.81 cnf(d70, plain, sK91(sK55) != sK91(sK55) | ~in(sK91(sK55),sK55) | ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | ~in(sK57(sK91(sK55)),sK55) | ~in(sK91(sK55),sK55) | 'Ts84'(sK77(sK50)), inference(superposition, [status(thm)], [d69,d32])).
% 64.73/8.81 cnf(d71, plain, ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | ~in(sK57(sK91(sK55)),sK55) | ~in(sK91(sK55),sK55) | 'Ts84'(sK77(sK50)), inference(equality_resolution, [status(thm)], [d70])).
% 64.73/8.81 cnf(d72, plain, ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | ~in(sK91(sK55),sK55) | 'Ts84'(sK77(sK50)) | ~in(sK91(sK55),sK55), inference(resolution, [status(thm)], [d71,d31])).
% 64.73/8.81 cnf(d73, plain, ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | 'Ts84'(sK77(sK50)) | ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | 'Ts84'(sK77(sK50)), inference(resolution, [status(thm)], [d72,d62])).
% 64.73/8.81 cnf(d74, plain, 'being$ulimit$uordinal'(sK50) | 'Ts84'(sK77(sK50)) | ~ordinal(sK50) | 'being$ulimit$uordinal'(sK50), inference(resolution, [status(thm)], [d73,c139])).
% 64.73/8.81 cnf(d75, plain, 'being$ulimit$uordinal'(sK50) | 'Ts84'(sK77(sK50)), inference(resolution, [status(thm)], [d26,d74])).
% 64.73/8.81 cnf(d76, plain, 'being$ulimit$uordinal'(sK50) | ordinal(sK77(sK50)), inference(resolution, [status(thm)], [d75,d56])).
% 64.73/8.81 cnf(d77, plain, in(sK77(X0),X0) | ~ordinal(X0) | 'being$ulimit$uordinal'(X0), inference(superposition, [status(thm)], [c140,c135])).
% 64.73/8.81 cnf(d78, plain, sK101(X0) = 'empty$uset' | ~ordinal(X0) | ~in(X0,omega) | ~in(X0,sK50) | in(sK53(sK101(X0)),sK101(X0)) | ~'Ts84'(X0), inference(resolution, [status(thm)], [d13,c159])).
% 64.73/8.81 cnf(d79, plain, sK101(X0) = 'empty$uset' | X1 = sK53(sK101(X0)) | ~ordinal(X0) | ~subset(sK53(sK101(X0)),X1) | ~in(X0,omega) | ~in(X0,sK50) | ~in(X1,sK101(X0)) | ~'Ts84'(X0), inference(resolution, [status(thm)], [d15,c159])).
% 64.73/8.81 cnf(d80, plain, sK103(X0,sK53(sK101(X1))) = sK53(sK101(X1)) | sK101(X1) = 'empty$uset' | ~ordinal(X1) | ~in(sK103(X0,sK53(sK101(X1))),sK101(X1)) | ~in(X1,omega) | ~in(X1,sK50) | ~'Ts84'(X1) | ~in(sK53(sK101(X1)),sK101(X0)) | ~'Ts84'(X0), inference(resolution, [status(thm)], [d79,c162])).
% 64.73/8.81 cnf(d81, plain, sK53(sK101(X1)) != sK53(sK101(X1)) | ~in(sK53(sK101(X1)),sK101(X0)) | ~'Ts84'(X0) | sK101(X1) = 'empty$uset' | ~ordinal(X1) | ~in(X1,omega) | ~in(X1,sK50) | ~in(sK53(sK101(X1)),sK101(X0)) | ~in(sK103(X0,sK53(sK101(X1))),sK101(X1)) | ~'Ts84'(X1) | ~'Ts84'(X0), inference(superposition, [status(thm)], [d80,c163])).
% 64.73/8.81 cnf(d82, plain, sK101(X0) = 'empty$uset' | ~ordinal(X0) | ~in(X0,omega) | ~in(X0,sK50) | ~in(sK53(sK101(X0)),sK101(X1)) | ~in(sK103(X1,sK53(sK101(X0))),sK101(X0)) | ~'Ts84'(X0) | ~'Ts84'(X1), inference(equality_resolution, [status(thm)], [d81])).
% 64.73/8.81 cnf(d83, plain, sK101(X0) = 'empty$uset' | ~ordinal(X0) | ~in(X0,omega) | ~in(X0,sK50) | ~in(sK53(sK101(X0)),sK101(X0)) | ~'Ts84'(X0) | ~'Ts84'(X0) | ~in(sK53(sK101(X0)),sK101(X0)) | ~'Ts84'(X0), inference(resolution, [status(thm)], [d82,c161])).
% 64.73/8.81 cnf(d84, plain, sK101(X0) = 'empty$uset' | ~ordinal(X0) | ~in(X0,omega) | ~in(X0,sK50) | ~'Ts84'(X0) | sK101(X0) = 'empty$uset' | ~ordinal(X0) | ~in(X0,omega) | ~in(X0,sK50) | ~'Ts84'(X0), inference(resolution, [status(thm)], [d83,d78])).
% 64.73/8.81 cnf(d85, plain, 'empty$uset' != 'empty$uset' | ~'Ts84'(X0) | ~ordinal(X0) | ~in(X0,omega) | ~in(X0,sK50) | ~'Ts84'(X0), inference(superposition, [status(thm)], [d84,c160])).
% 64.73/8.81 cnf(d86, plain, ~ordinal(X0) | ~in(X0,omega) | ~in(X0,sK50) | ~'Ts84'(X0), inference(equality_resolution, [status(thm)], [d85])).
% 64.73/8.81 cnf(d87, plain, ~ordinal(sK77(sK50)) | ~in(sK77(sK50),omega) | ~'Ts84'(sK77(sK50)) | ~ordinal(sK50) | 'being$ulimit$uordinal'(sK50), inference(resolution, [status(thm)], [d86,d77])).
% 64.73/8.81 cnf(d88, plain, ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | ~in(sK77(sK50),omega) | ~'Ts84'(sK77(sK50)), inference(resolution, [status(thm)], [d26,d87])).
% 64.73/8.81 cnf(d89, plain, ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | ~'Ts84'(sK77(sK50)) | ~'Ts84'(sK77(sK50)), inference(resolution, [status(thm)], [d88,c158])).
% 64.73/8.81 cnf(d90, plain, ~ordinal(sK77(sK50)) | 'being$ulimit$uordinal'(sK50) | 'being$ulimit$uordinal'(sK50), inference(resolution, [status(thm)], [d89,d75])).
% 64.73/8.81 cnf(d91, plain, 'being$ulimit$uordinal'(sK50) | 'being$ulimit$uordinal'(sK50), inference(resolution, [status(thm)], [d90,d76])).
% 64.73/8.81 cnf(d92, plain, ~'Ts85'(sK50), inference(resolution, [status(thm)], [d91,d54])).
% 64.73/8.81 cnf(d93, plain, sK105(sK50) = 'empty$uset' | ~ordinal(sK104(sK50)) | ~in(sK104(sK50),omega), inference(resolution, [status(thm)], [d92,d22])).
% 64.73/8.81 cnf(d94, plain, sK105(sK50) = 'empty$uset' | ~ordinal(sK104(sK50)) | 'Ts85'(sK50), inference(resolution, [status(thm)], [d93,c166])).
% 64.73/8.81 cnf(d95, plain, sK105(sK50) = 'empty$uset' | ~ordinal(sK104(sK50)), inference(resolution, [status(thm)], [d92,d94])).
% 64.73/8.81 cnf(d96, plain, 'empty$uset' != 'empty$uset' | 'Ts85'(sK50) | ~ordinal(sK104(sK50)), inference(superposition, [status(thm)], [d95,c168])).
% 64.73/8.81 cnf(d97, plain, 'empty$uset' != 'empty$uset' | ~ordinal(sK104(sK50)), inference(resolution, [status(thm)], [d92,d96])).
% 64.73/8.81 cnf(d98, plain, ~ordinal(sK104(sK50)), inference(equality_resolution, [status(thm)], [d97])).
% 64.73/8.81 cnf(d99, plain, 'Ts85'(sK50), inference(resolution, [status(thm)], [d98,c164])).
% 64.73/8.81 cnf(d100, plain, $false, inference(resolution, [status(thm)], [d92,d99])).
% 64.73/8.81 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------