%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU298+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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 22.66s 5.53s
% Output : CNFRefutation 22.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU298+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n009.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Sat Sep 26 09:07:59 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.43 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.66/5.53 % SZS status Theorem for theBenchmark.p
% 22.66/5.53 % SZS output start CNFRefutation for theBenchmark.p
% 22.66/5.53 fof(s1_tarski__e4_27_3_1__finset_1__1, axiom, ! [X0] : ! [X1] : (((ordinal(X0) & element(X1,powerset(powerset(succ(X0))))) => (! [X2] : ! [X3] : ! [X4] : (((X2 = X3 & (? [X5] : ((in(X5,X1) & X3 = 'set$udifference'(X5,singleton(X0)))) & (X2 = X4 & ? [X6] : ((in(X6,X1) & X4 = 'set$udifference'(X6,singleton(X0))))))) => X3 = X4)) => ? [X2] : ! [X3] : ((in(X3,X2) <=> ? [X4] : ((in(X4,powerset(X0)) & (X4 = X3 & ? [X7] : ((in(X7,X1) & X3 = 'set$udifference'(X7,singleton(X0))))))))))))).
% 22.66/5.53 fof(s1_xboole_0__e4_27_3_1__finset_1, conjecture, ! [X0] : ! [X1] : (((ordinal(X0) & element(X1,powerset(powerset(succ(X0))))) => ? [X2] : ! [X3] : ((in(X3,X2) <=> (in(X3,powerset(X0)) & ? [X4] : ((in(X4,X1) & X3 = 'set$udifference'(X4,singleton(X0)))))))))).
% 22.66/5.53 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : (((ordinal(X0) & element(X1,powerset(powerset(succ(X0))))) => ? [X2] : ! [X3] : ((in(X3,X2) <=> (in(X3,powerset(X0)) & ? [X4] : ((in(X4,X1) & X3 = 'set$udifference'(X4,singleton(X0))))))))), inference(negate_conjecture, [status(cth)], [s1_xboole_0__e4_27_3_1__finset_1])).
% 22.66/5.53 cnf(c90, plain, ~ordinal(X0) | ~element(X1,powerset(powerset(succ(X0)))) | ~in(X2,sK49(X0,X1)) | X3(X0,X1,X2) | X4(X0,X1), inference(clausification, [status(esa)], [s1_tarski__e4_27_3_1__finset_1__1])).
% 22.66/5.53 cnf(c91, plain, ~ordinal(X0) | in(X1,sK49(X0,X2)) | ~X3(X0,X2,X1) | ~element(X2,powerset(powerset(succ(X0)))) | X4(X0,X2), inference(clausification, [status(esa)], [s1_tarski__e4_27_3_1__finset_1__1])).
% 22.66/5.53 cnf(c92, plain, ~X0(X1,X2,X3) | in(sK51(X1,X2,X3),powerset(X1)), inference(clausification, [status(esa)], [s1_tarski__e4_27_3_1__finset_1__1])).
% 22.66/5.53 cnf(c93, plain, ~X0(X1,X2,X3) | sK51(X1,X2,X3) = X3, inference(clausification, [status(esa)], [s1_tarski__e4_27_3_1__finset_1__1])).
% 22.66/5.53 cnf(c94, plain, ~X0(X1,X2,X3) | in(sK52(X1,X2,X3),X2), inference(clausification, [status(esa)], [s1_tarski__e4_27_3_1__finset_1__1])).
% 22.66/5.53 cnf(c95, plain, ~X0(X1,X2,X3) | X3 = 'set$udifference'(sK52(X1,X2,X3),singleton(X1)), inference(clausification, [status(esa)], [s1_tarski__e4_27_3_1__finset_1__1])).
% 22.66/5.53 cnf(c96, plain, X0 != 'set$udifference'(X1,singleton(X2)) | X3(X2,X4,X0) | ~in(X1,X4) | ~in(X5,powerset(X2)) | X5 != X0, inference(clausification, [status(esa)], [s1_tarski__e4_27_3_1__finset_1__1])).
% 22.66/5.53 cnf(c97, plain, ~X0(X1,X2) | sK55(X1,X2) = sK56(X1,X2), inference(clausification, [status(esa)], [s1_tarski__e4_27_3_1__finset_1__1])).
% 22.66/5.53 cnf(c100, plain, ~X0(X1,X2) | sK55(X1,X2) = sK57(X1,X2), inference(clausification, [status(esa)], [s1_tarski__e4_27_3_1__finset_1__1])).
% 22.66/5.53 cnf(c103, plain, ~X0(X1,X2) | sK56(X1,X2) != sK57(X1,X2), inference(clausification, [status(esa)], [s1_tarski__e4_27_3_1__finset_1__1])).
% 22.66/5.53 cnf(c104, plain, ordinal(sK60), inference(clausification, [status(esa)], [negated_conjecture])).
% 22.66/5.53 cnf(c105, plain, element(sK61,powerset(powerset(succ(sK60)))), inference(clausification, [status(esa)], [negated_conjecture])).
% 22.66/5.53 cnf(c107, plain, in(sK63(X0),X0) | in(sK63(X0),powerset(sK60)), inference(clausification, [status(esa)], [negated_conjecture])).
% 22.66/5.53 cnf(c108, plain, in(sK63(X0),X0) | in(sK65(X0),sK61), inference(clausification, [status(esa)], [negated_conjecture])).
% 22.66/5.53 cnf(c109, plain, in(sK63(X0),X0) | sK63(X0) = 'set$udifference'(sK65(X0),singleton(sK60)), inference(clausification, [status(esa)], [negated_conjecture])).
% 22.66/5.53 cnf(c110, plain, ~in(sK63(X0),powerset(sK60)) | ~in(X1,sK61) | sK63(X0) != 'set$udifference'(X1,singleton(sK60)) | ~in(sK63(X0),X0), inference(clausification, [status(esa)], [negated_conjecture])).
% 22.66/5.53 cnf(c113, plain, ~in(sK63(X0),powerset(sK60)) | ~in(X1,sK61) | sK63(X0) != 'set$udifference'(X1,singleton(sK60)) | sK63(X0) = 'set$udifference'(sK65(X0),singleton(sK60)), inference(clausification, [status(esa)], [negated_conjecture])).
% 22.66/5.53 cnf(d0, plain, ~ordinal(sK60) | ~in(X0,sK49(sK60,sK61)) | 'Ts45'(sK60,sK61,X0) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [c90,c105])).
% 22.66/5.53 cnf(d1, plain, ~in(X0,sK49(sK60,sK61)) | 'Ts45'(sK60,sK61,X0) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [c104,d0])).
% 22.66/5.53 cnf(d2, plain, 'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | 'Ts46'(sK60,sK61) | in(sK65(sK49(sK60,sK61)),sK61), inference(resolution, [status(thm)], [d1,c108])).
% 22.66/5.53 cnf(d3, plain, sK63(sK49(sK60,sK61)) = 'set$udifference'(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),singleton(sK60)) | in(sK65(sK49(sK60,sK61)),sK61) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [c95,d2])).
% 22.66/5.53 cnf(d4, plain, 'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | 'Ts46'(sK60,sK61) | in(sK63(sK49(sK60,sK61)),powerset(sK60)), inference(resolution, [status(thm)], [d1,c107])).
% 22.66/5.53 cnf(d5, plain, in(sK65(sK49(sK60,sK61)),sK61) | 'Ts46'(sK60,sK61) | sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)), inference(resolution, [status(thm)], [d2,c93])).
% 22.66/5.53 cnf(d6, plain, 'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | 'Ts46'(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)), inference(resolution, [status(thm)], [d1,c109])).
% 22.66/5.53 cnf(d7, plain, sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | 'Ts46'(sK60,sK61) | sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)), inference(resolution, [status(thm)], [d6,c93])).
% 22.66/5.53 cnf(d8, plain, sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | sK55(sK60,sK61) = sK57(sK60,sK61), inference(resolution, [status(thm)], [d7,c100])).
% 22.66/5.53 cnf(d9, plain, in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | sK55(sK60,sK61) = sK57(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)), inference(superposition, [status(thm)], [d8,c92])).
% 22.66/5.53 cnf(d10, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | in(sK63(sK49(sK60,sK61)),powerset(sK60)) | in(sK63(sK49(sK60,sK61)),powerset(sK60)) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d9,d4])).
% 22.66/5.53 cnf(d11, plain, sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | 'Ts46'(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),singleton(sK60)), inference(resolution, [status(thm)], [d6,c95])).
% 22.66/5.53 cnf(d12, plain, sK63(sK49(sK60,sK61)) = 'set$udifference'(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),singleton(sK60)) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | sK55(sK60,sK61) = sK57(sK60,sK61), inference(resolution, [status(thm)], [d11,c100])).
% 22.66/5.53 cnf(d13, plain, sK63(X0) != sK63(sK49(sK60,sK61)) | sK63(X0) = 'set$udifference'(sK65(X0),singleton(sK60)) | ~in(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),sK61) | ~in(sK63(X0),powerset(sK60)) | sK55(sK60,sK61) = sK57(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)), inference(superposition, [status(thm)], [d12,c113])).
% 22.66/5.53 cnf(d14, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | ~in(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),sK61) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)), inference(equality_resolution, [status(thm)], [d13])).
% 22.66/5.53 cnf(d15, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))), inference(resolution, [status(thm)], [d14,c94])).
% 22.66/5.53 cnf(d16, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d15,d6])).
% 22.66/5.53 cnf(d17, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | 'Ts46'(sK60,sK61) | sK55(sK60,sK61) = sK57(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d16,d10])).
% 22.66/5.53 cnf(d18, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | sK55(sK60,sK61) = sK57(sK60,sK61), inference(resolution, [status(thm)], [d17,c100])).
% 22.66/5.53 cnf(d19, plain, X0 != sK63(sK49(sK60,sK61)) | X1 != X0 | ~in(sK65(sK49(sK60,sK61)),X2) | ~in(X1,powerset(sK60)) | 'Ts45'(sK60,X2,X0) | sK55(sK60,sK61) = sK57(sK60,sK61), inference(superposition, [status(thm)], [d18,c96])).
% 22.66/5.53 cnf(d20, plain, X0 != sK63(sK49(sK60,sK61)) | sK55(sK60,sK61) = sK57(sK60,sK61) | ~in(X0,powerset(sK60)) | ~in(sK65(sK49(sK60,sK61)),X1) | 'Ts45'(sK60,X1,sK63(sK49(sK60,sK61))), inference(equality_resolution, [status(thm)], [d19])).
% 22.66/5.53 cnf(d21, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK65(sK49(sK60,sK61)),X0) | 'Ts45'(sK60,X0,sK63(sK49(sK60,sK61))), inference(equality_resolution, [status(thm)], [d20])).
% 22.66/5.53 cnf(d22, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | ~in(sK65(sK49(sK60,sK61)),X0) | 'Ts45'(sK60,X0,sK63(sK49(sK60,sK61))) | in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)), inference(resolution, [status(thm)], [d21,c107])).
% 22.66/5.53 cnf(d23, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | ~in(sK65(sK49(sK60,sK61)),X0) | 'Ts45'(sK60,X0,sK63(sK49(sK60,sK61))) | 'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d22,d1])).
% 22.66/5.53 cnf(d24, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | ~in(sK65(sK49(sK60,sK61)),sK61) | 'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | 'Ts46'(sK60,sK61), inference(factoring, [status(thm)], [d23])).
% 22.66/5.53 cnf(d25, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | ~in(sK65(sK49(sK60,sK61)),sK61) | 'Ts46'(sK60,sK61) | sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)), inference(resolution, [status(thm)], [d24,c93])).
% 22.66/5.53 cnf(d26, plain, sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)) | sK55(sK60,sK61) = sK57(sK60,sK61) | 'Ts46'(sK60,sK61) | sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d25,d5])).
% 22.66/5.53 cnf(d27, plain, sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)) | sK55(sK60,sK61) = sK57(sK60,sK61) | sK55(sK60,sK61) = sK57(sK60,sK61), inference(resolution, [status(thm)], [d26,c100])).
% 22.66/5.53 cnf(d28, plain, in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | sK55(sK60,sK61) = sK57(sK60,sK61), inference(superposition, [status(thm)], [d27,c92])).
% 22.66/5.53 cnf(d29, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | in(sK63(sK49(sK60,sK61)),powerset(sK60)) | in(sK63(sK49(sK60,sK61)),powerset(sK60)) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d28,d4])).
% 22.66/5.53 cnf(d30, plain, ~ordinal(sK60) | in(X0,sK49(sK60,sK61)) | ~'Ts45'(sK60,sK61,X0) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [c91,c105])).
% 22.66/5.53 cnf(d31, plain, in(X0,sK49(sK60,sK61)) | ~'Ts45'(sK60,sK61,X0) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [c104,d30])).
% 22.66/5.53 cnf(d32, plain, sK63(X0) != sK63(sK49(sK60,sK61)) | ~in(sK65(sK49(sK60,sK61)),sK61) | ~in(sK63(X0),X0) | ~in(sK63(X0),powerset(sK60)) | sK55(sK60,sK61) = sK57(sK60,sK61), inference(superposition, [status(thm)], [d18,c110])).
% 22.66/5.53 cnf(d33, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | ~in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK65(sK49(sK60,sK61)),sK61), inference(equality_resolution, [status(thm)], [d32])).
% 22.66/5.53 cnf(d34, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK65(sK49(sK60,sK61)),sK61) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d33,d31])).
% 22.66/5.53 cnf(d35, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | ~in(sK65(sK49(sK60,sK61)),sK61) | 'Ts46'(sK60,sK61) | sK55(sK60,sK61) = sK57(sK60,sK61) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK65(sK49(sK60,sK61)),sK61) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d24,d34])).
% 22.66/5.53 cnf(d36, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | 'Ts46'(sK60,sK61) | sK55(sK60,sK61) = sK57(sK60,sK61) | ~in(sK65(sK49(sK60,sK61)),sK61) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d29,d35])).
% 22.66/5.53 cnf(d37, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | 'Ts46'(sK60,sK61) | in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)), inference(resolution, [status(thm)], [d36,c108])).
% 22.66/5.53 cnf(d38, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | 'Ts46'(sK60,sK61) | 'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d37,d1])).
% 22.66/5.53 cnf(d39, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | 'Ts46'(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),singleton(sK60)) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d36,d3])).
% 22.66/5.53 cnf(d40, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),singleton(sK60)) | sK55(sK60,sK61) = sK57(sK60,sK61), inference(resolution, [status(thm)], [d39,c100])).
% 22.66/5.53 cnf(d41, plain, sK63(X0) != sK63(sK49(sK60,sK61)) | ~in(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),sK61) | ~in(sK63(X0),X0) | ~in(sK63(X0),powerset(sK60)) | sK55(sK60,sK61) = sK57(sK60,sK61), inference(superposition, [status(thm)], [d40,c110])).
% 22.66/5.53 cnf(d42, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | ~in(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),sK61) | ~in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)), inference(equality_resolution, [status(thm)], [d41])).
% 22.66/5.53 cnf(d43, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))), inference(resolution, [status(thm)], [d42,c94])).
% 22.66/5.53 cnf(d44, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | sK55(sK60,sK61) = sK57(sK60,sK61) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d43,d37])).
% 22.66/5.53 cnf(d45, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | 'Ts46'(sK60,sK61) | sK55(sK60,sK61) = sK57(sK60,sK61) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d44,d38])).
% 22.66/5.53 cnf(d46, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | 'Ts46'(sK60,sK61) | sK55(sK60,sK61) = sK57(sK60,sK61) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d45,d29])).
% 22.66/5.53 cnf(d47, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | sK55(sK60,sK61) = sK57(sK60,sK61), inference(resolution, [status(thm)], [d46,c100])).
% 22.66/5.53 cnf(d48, plain, sK55(sK60,sK61) = sK57(sK60,sK61) | sK55(sK60,sK61) = sK56(sK60,sK61), inference(resolution, [status(thm)], [d46,c97])).
% 22.66/5.53 cnf(d49, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | sK55(sK60,sK61) = sK57(sK60,sK61), inference(demodulation, [status(thm)], [d48,d47])).
% 22.66/5.53 cnf(d50, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | sK57(sK60,sK61) = sK57(sK60,sK61), inference(demodulation, [status(thm)], [d49,d47])).
% 22.66/5.53 cnf(d51, plain, X0 != 'set$udifference'(X1,singleton(X2)) | ~in(X1,X3) | ~in(X0,powerset(X2)) | 'Ts45'(X2,X3,'set$udifference'(X1,singleton(X2))), inference(equality_resolution, [status(thm)], [c96])).
% 22.66/5.53 cnf(d52, plain, ~in(X0,X1) | ~in('set$udifference'(X0,singleton(X2)),powerset(X2)) | 'Ts45'(X2,X1,'set$udifference'(X0,singleton(X2))), inference(equality_resolution, [status(thm)], [d51])).
% 22.66/5.53 cnf(d53, plain, sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | sK55(sK60,sK61) = sK56(sK60,sK61), inference(resolution, [status(thm)], [d7,c97])).
% 22.66/5.53 cnf(d54, plain, in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | sK55(sK60,sK61) = sK56(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)), inference(superposition, [status(thm)], [d53,c92])).
% 22.66/5.53 cnf(d55, plain, sK55(sK60,sK61) = sK56(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | in(sK63(sK49(sK60,sK61)),powerset(sK60)) | in(sK63(sK49(sK60,sK61)),powerset(sK60)) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d54,d4])).
% 22.66/5.53 cnf(d56, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | in(sK63(sK49(sK60,sK61)),powerset(sK60)) | 'Ts46'(sK60,sK61), inference(demodulation, [status(thm)], [d55,d47])).
% 22.66/5.53 cnf(d57, plain, sK63(sK49(sK60,sK61)) = 'set$udifference'(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),singleton(sK60)) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | sK55(sK60,sK61) = sK56(sK60,sK61), inference(resolution, [status(thm)], [d11,c97])).
% 22.66/5.53 cnf(d58, plain, sK63(X0) != sK63(sK49(sK60,sK61)) | sK63(X0) = 'set$udifference'(sK65(X0),singleton(sK60)) | ~in(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),sK61) | ~in(sK63(X0),powerset(sK60)) | sK55(sK60,sK61) = sK56(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)), inference(superposition, [status(thm)], [d57,c113])).
% 22.66/5.53 cnf(d59, plain, sK55(sK60,sK61) = sK56(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | ~in(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),sK61) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)), inference(equality_resolution, [status(thm)], [d58])).
% 22.66/5.53 cnf(d60, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | ~in(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),sK61) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)), inference(demodulation, [status(thm)], [d59,d47])).
% 22.66/5.53 cnf(d61, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))), inference(resolution, [status(thm)], [d60,c94])).
% 22.66/5.53 cnf(d62, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d61,d6])).
% 22.66/5.53 cnf(d63, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | 'Ts46'(sK60,sK61) | sK57(sK60,sK61) = sK56(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d62,d56])).
% 22.66/5.53 cnf(d64, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | sK55(sK60,sK61) = sK56(sK60,sK61), inference(resolution, [status(thm)], [d63,c97])).
% 22.66/5.53 cnf(d65, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | sK57(sK60,sK61) = sK56(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)), inference(demodulation, [status(thm)], [d64,d47])).
% 22.66/5.53 cnf(d66, plain, ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK65(sK49(sK60,sK61)),X0) | 'Ts45'(sK60,X0,'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60))) | sK57(sK60,sK61) = sK56(sK60,sK61) | sK57(sK60,sK61) = sK56(sK60,sK61), inference(superposition, [status(thm)], [d65,d52])).
% 22.66/5.53 cnf(d67, plain, 'Ts45'(sK60,X0,sK63(sK49(sK60,sK61))) | sK57(sK60,sK61) = sK56(sK60,sK61) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK65(sK49(sK60,sK61)),X0) | sK57(sK60,sK61) = sK56(sK60,sK61) | sK57(sK60,sK61) = sK56(sK60,sK61), inference(superposition, [status(thm)], [d65,d66])).
% 22.66/5.53 cnf(d68, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | ~in(sK65(sK49(sK60,sK61)),X0) | 'Ts45'(sK60,X0,sK63(sK49(sK60,sK61))) | in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)), inference(resolution, [status(thm)], [d67,c107])).
% 22.66/5.53 cnf(d69, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | ~in(sK65(sK49(sK60,sK61)),X0) | 'Ts45'(sK60,X0,sK63(sK49(sK60,sK61))) | 'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d68,d1])).
% 22.66/5.53 cnf(d70, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | ~in(sK65(sK49(sK60,sK61)),sK61) | 'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | 'Ts46'(sK60,sK61), inference(factoring, [status(thm)], [d69])).
% 22.66/5.53 cnf(d71, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | ~in(sK65(sK49(sK60,sK61)),sK61) | 'Ts46'(sK60,sK61) | sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)), inference(resolution, [status(thm)], [d70,c93])).
% 22.66/5.53 cnf(d72, plain, sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)) | sK57(sK60,sK61) = sK56(sK60,sK61) | 'Ts46'(sK60,sK61) | sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d71,d5])).
% 22.66/5.53 cnf(d73, plain, sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)) | sK57(sK60,sK61) = sK56(sK60,sK61) | sK55(sK60,sK61) = sK56(sK60,sK61), inference(resolution, [status(thm)], [d72,c97])).
% 22.66/5.53 cnf(d74, plain, sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)) | sK57(sK60,sK61) = sK56(sK60,sK61) | sK57(sK60,sK61) = sK56(sK60,sK61), inference(demodulation, [status(thm)], [d73,d47])).
% 22.66/5.53 cnf(d75, plain, in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | sK57(sK60,sK61) = sK56(sK60,sK61) | sK57(sK60,sK61) = sK56(sK60,sK61), inference(superposition, [status(thm)], [d74,c92])).
% 22.66/5.53 cnf(d76, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | in(sK63(sK49(sK60,sK61)),powerset(sK60)) | in(sK63(sK49(sK60,sK61)),powerset(sK60)) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d75,d4])).
% 22.66/5.53 cnf(d77, plain, sK63(X0) != sK63(sK49(sK60,sK61)) | ~in(sK65(sK49(sK60,sK61)),sK61) | ~in(sK63(X0),X0) | ~in(sK63(X0),powerset(sK60)) | sK57(sK60,sK61) = sK56(sK60,sK61) | sK57(sK60,sK61) = sK56(sK60,sK61), inference(superposition, [status(thm)], [d65,c110])).
% 22.66/5.53 cnf(d78, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | ~in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK65(sK49(sK60,sK61)),sK61), inference(equality_resolution, [status(thm)], [d77])).
% 22.66/5.53 cnf(d79, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK65(sK49(sK60,sK61)),sK61) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d78,d31])).
% 22.66/5.53 cnf(d80, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | ~in(sK65(sK49(sK60,sK61)),sK61) | 'Ts46'(sK60,sK61) | sK57(sK60,sK61) = sK56(sK60,sK61) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK65(sK49(sK60,sK61)),sK61) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d70,d79])).
% 22.66/5.53 cnf(d81, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | 'Ts46'(sK60,sK61) | sK57(sK60,sK61) = sK56(sK60,sK61) | ~in(sK65(sK49(sK60,sK61)),sK61) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d76,d80])).
% 22.66/5.53 cnf(d82, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | 'Ts46'(sK60,sK61) | in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)), inference(resolution, [status(thm)], [d81,c108])).
% 22.66/5.53 cnf(d83, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | 'Ts46'(sK60,sK61) | 'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d82,d1])).
% 22.66/5.53 cnf(d84, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | 'Ts46'(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),singleton(sK60)) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d81,d3])).
% 22.66/5.53 cnf(d85, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),singleton(sK60)) | sK55(sK60,sK61) = sK56(sK60,sK61), inference(resolution, [status(thm)], [d84,c97])).
% 22.66/5.53 cnf(d86, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | sK57(sK60,sK61) = sK56(sK60,sK61) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),singleton(sK60)), inference(demodulation, [status(thm)], [d85,d47])).
% 22.66/5.53 cnf(d87, plain, sK63(X0) != sK63(sK49(sK60,sK61)) | ~in(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),sK61) | ~in(sK63(X0),X0) | ~in(sK63(X0),powerset(sK60)) | sK57(sK60,sK61) = sK56(sK60,sK61) | sK57(sK60,sK61) = sK56(sK60,sK61), inference(superposition, [status(thm)], [d86,c110])).
% 22.66/5.53 cnf(d88, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | ~in(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),sK61) | ~in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)), inference(equality_resolution, [status(thm)], [d87])).
% 22.66/5.53 cnf(d89, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))), inference(resolution, [status(thm)], [d88,c94])).
% 22.66/5.53 cnf(d90, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | sK57(sK60,sK61) = sK56(sK60,sK61) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d89,d82])).
% 22.66/5.53 cnf(d91, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | 'Ts46'(sK60,sK61) | sK57(sK60,sK61) = sK56(sK60,sK61) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d90,d83])).
% 22.66/5.53 cnf(d92, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | 'Ts46'(sK60,sK61) | sK57(sK60,sK61) = sK56(sK60,sK61) | 'Ts46'(sK60,sK61), inference(resolution, [status(thm)], [d91,d76])).
% 22.66/5.53 cnf(d93, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | sK55(sK60,sK61) = sK56(sK60,sK61), inference(resolution, [status(thm)], [d92,c97])).
% 22.66/5.53 cnf(d94, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | sK57(sK60,sK61) = sK56(sK60,sK61), inference(demodulation, [status(thm)], [d93,d47])).
% 22.66/5.53 cnf(d95, plain, sK57(sK60,sK61) = sK56(sK60,sK61) | sK57(sK60,sK61) = sK56(sK60,sK61) | sK57(sK60,sK61) = sK56(sK60,sK61), inference(superposition, [status(thm)], [d94,d50])).
% 22.66/5.53 cnf(d96, plain, sK56(sK60,sK61) != sK56(sK60,sK61) | ~'Ts46'(sK60,sK61), inference(superposition, [status(thm)], [d95,c103])).
% 22.66/5.53 cnf(d97, plain, ~'Ts46'(sK60,sK61), inference(equality_resolution, [status(thm)], [d96])).
% 22.66/5.53 cnf(d98, plain, sK63(sK49(sK60,sK61)) = 'set$udifference'(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),singleton(sK60)) | in(sK65(sK49(sK60,sK61)),sK61), inference(resolution, [status(thm)], [d97,d3])).
% 22.66/5.53 cnf(d99, plain, in(X0,sK49(sK60,sK61)) | ~'Ts45'(sK60,sK61,X0), inference(resolution, [status(thm)], [d97,d31])).
% 22.66/5.53 cnf(d100, plain, sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | 'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))), inference(resolution, [status(thm)], [d97,d6])).
% 22.66/5.53 cnf(d101, plain, sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)), inference(resolution, [status(thm)], [d97,d7])).
% 22.66/5.53 cnf(d102, plain, in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)), inference(superposition, [status(thm)], [d101,c92])).
% 22.66/5.53 cnf(d103, plain, sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | in(sK63(sK49(sK60,sK61)),powerset(sK60)) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)), inference(resolution, [status(thm)], [d102,d100])).
% 22.66/5.53 cnf(d104, plain, sK63(sK49(sK60,sK61)) = 'set$udifference'(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),singleton(sK60)) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)), inference(resolution, [status(thm)], [d97,d11])).
% 22.66/5.53 cnf(d105, plain, sK63(X0) != sK63(sK49(sK60,sK61)) | ~in(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),sK61) | ~in(sK63(X0),X0) | ~in(sK63(X0),powerset(sK60)) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)), inference(superposition, [status(thm)], [d104,c110])).
% 22.66/5.53 cnf(d106, plain, sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | ~in(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),sK61) | ~in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)), inference(equality_resolution, [status(thm)], [d105])).
% 22.66/5.53 cnf(d107, plain, sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))), inference(resolution, [status(thm)], [d106,c94])).
% 22.66/5.53 cnf(d108, plain, sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)), inference(resolution, [status(thm)], [d107,c109])).
% 22.66/5.53 cnf(d109, plain, sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)), inference(resolution, [status(thm)], [d108,d100])).
% 22.66/5.53 cnf(d110, plain, sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)) | sK63(sK49(sK60,sK61)) = 'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60)), inference(resolution, [status(thm)], [d109,d103])).
% 22.66/5.53 cnf(d111, plain, sK63(X0) != sK63(sK49(sK60,sK61)) | ~in(sK65(sK49(sK60,sK61)),sK61) | ~in(sK63(X0),X0) | ~in(sK63(X0),powerset(sK60)), inference(superposition, [status(thm)], [d110,c110])).
% 22.66/5.53 cnf(d112, plain, ~in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK65(sK49(sK60,sK61)),sK61), inference(equality_resolution, [status(thm)], [d111])).
% 22.66/5.53 cnf(d113, plain, ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK65(sK49(sK60,sK61)),sK61) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))), inference(resolution, [status(thm)], [d112,d99])).
% 22.66/5.53 cnf(d114, plain, ~in(X0,sK49(sK60,sK61)) | 'Ts45'(sK60,sK61,X0), inference(resolution, [status(thm)], [d97,d1])).
% 22.66/5.53 cnf(d115, plain, ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK65(sK49(sK60,sK61)),X0) | 'Ts45'(sK60,X0,'set$udifference'(sK65(sK49(sK60,sK61)),singleton(sK60))), inference(superposition, [status(thm)], [d110,d52])).
% 22.66/5.53 cnf(d116, plain, ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK65(sK49(sK60,sK61)),X0) | 'Ts45'(sK60,X0,sK63(sK49(sK60,sK61))), inference(demodulation, [status(thm)], [d115,d110])).
% 22.66/5.53 cnf(d117, plain, ~in(sK65(sK49(sK60,sK61)),X0) | 'Ts45'(sK60,X0,sK63(sK49(sK60,sK61))) | in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)), inference(resolution, [status(thm)], [d116,c107])).
% 22.66/5.53 cnf(d118, plain, ~in(sK65(sK49(sK60,sK61)),X0) | 'Ts45'(sK60,X0,sK63(sK49(sK60,sK61))) | 'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))), inference(resolution, [status(thm)], [d117,d114])).
% 22.66/5.53 cnf(d119, plain, ~in(sK65(sK49(sK60,sK61)),sK61) | 'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))), inference(factoring, [status(thm)], [d118])).
% 22.66/5.53 cnf(d120, plain, ~in(sK65(sK49(sK60,sK61)),sK61) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~in(sK65(sK49(sK60,sK61)),sK61), inference(resolution, [status(thm)], [d119,d113])).
% 22.66/5.53 cnf(d121, plain, in(sK63(sK49(sK60,sK61)),powerset(sK60)) | 'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))), inference(resolution, [status(thm)], [d97,d4])).
% 22.66/5.53 cnf(d122, plain, sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)) | in(sK65(sK49(sK60,sK61)),sK61), inference(resolution, [status(thm)], [d97,d5])).
% 22.66/5.53 cnf(d123, plain, ~in(sK65(sK49(sK60,sK61)),sK61) | sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)), inference(resolution, [status(thm)], [d119,c93])).
% 22.66/5.53 cnf(d124, plain, sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)) | sK51(sK60,sK61,sK63(sK49(sK60,sK61))) = sK63(sK49(sK60,sK61)), inference(resolution, [status(thm)], [d123,d122])).
% 22.66/5.53 cnf(d125, plain, in(sK63(sK49(sK60,sK61)),powerset(sK60)) | ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))), inference(superposition, [status(thm)], [d124,c92])).
% 22.66/5.53 cnf(d126, plain, in(sK63(sK49(sK60,sK61)),powerset(sK60)) | in(sK63(sK49(sK60,sK61)),powerset(sK60)), inference(resolution, [status(thm)], [d125,d121])).
% 22.66/5.53 cnf(d127, plain, ~in(sK65(sK49(sK60,sK61)),sK61), inference(resolution, [status(thm)], [d126,d120])).
% 22.66/5.53 cnf(d128, plain, sK63(sK49(sK60,sK61)) = 'set$udifference'(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),singleton(sK60)), inference(resolution, [status(thm)], [d127,d98])).
% 22.66/5.53 cnf(d129, plain, sK63(X0) != sK63(sK49(sK60,sK61)) | ~in(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),sK61) | ~in(sK63(X0),X0) | ~in(sK63(X0),powerset(sK60)), inference(superposition, [status(thm)], [d128,c110])).
% 22.66/5.53 cnf(d130, plain, ~in(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),sK61) | ~in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)) | ~in(sK63(sK49(sK60,sK61)),powerset(sK60)), inference(equality_resolution, [status(thm)], [d129])).
% 22.66/5.53 cnf(d131, plain, ~in(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),sK61) | ~in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)), inference(resolution, [status(thm)], [d126,d130])).
% 22.66/5.53 cnf(d132, plain, in(sK63(sK49(sK60,sK61)),sK49(sK60,sK61)), inference(resolution, [status(thm)], [d127,c108])).
% 22.66/5.53 cnf(d133, plain, ~in(sK52(sK60,sK61,sK63(sK49(sK60,sK61))),sK61), inference(resolution, [status(thm)], [d132,d131])).
% 22.66/5.53 cnf(d134, plain, ~'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))), inference(resolution, [status(thm)], [d133,c94])).
% 22.66/5.53 cnf(d135, plain, in(sK65(sK49(sK60,sK61)),sK61) | 'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))), inference(resolution, [status(thm)], [d97,d2])).
% 22.66/5.53 cnf(d136, plain, 'Ts45'(sK60,sK61,sK63(sK49(sK60,sK61))), inference(resolution, [status(thm)], [d127,d135])).
% 22.66/5.53 cnf(d137, plain, $false, inference(resolution, [status(thm)], [d136,d134])).
% 22.66/5.53 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------