%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU329+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n008.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Tue Jul 19 14:36:19 EDT 2022 % Result : Theorem 2.48s 2.71s % Output : Refutation 2.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SEU329+1 : TPTP v8.1.0. Released v3.3.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n008.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jun 20 08:52:37 EDT 2022 % 0.13/0.35 % CPUTime : % 2.48/2.71 % 2.48/2.71 SPASS V 3.9 % 2.48/2.71 SPASS beiseite: Proof found. % 2.48/2.71 % SZS status Theorem % 2.48/2.71 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.48/2.71 SPASS derived 4839 clauses, backtracked 547 clauses, performed 23 splits and kept 3371 clauses. % 2.48/2.71 SPASS allocated 104953 KBytes. % 2.48/2.71 SPASS spent 0:00:02.35 on the problem. % 2.48/2.71 0:00:00.03 for the input. % 2.48/2.71 0:00:00.09 for the FLOTTER CNF translation. % 2.48/2.71 0:00:00.20 for inferences. % 2.48/2.71 0:00:00.05 for the backtracking. % 2.48/2.71 0:00:01.89 for the reduction. % 2.48/2.71 % 2.48/2.71 % 2.48/2.71 Here is a proof with depth 14, length 174 : % 2.48/2.71 % SZS output start Refutation % 2.48/2.71 1[0:Inp] || -> one_sorted_str(skc4)*. % 2.48/2.71 21[0:Inp] || -> element(skc5,powerset(powerset(the_carrier(skc4))))*. % 2.48/2.71 56[0:Inp] || -> in(skf15(u),u)* in(skf16(v),complements_of_subsets(the_carrier(skc4),skc5))*. % 2.48/2.71 60[0:Inp] || equal(skf27(u,v),skf27(u,v))* -> SkP0(w,x)*. % 2.48/2.71 61[0:Inp] || -> in(skf15(u),u) equal(ordered_pair(skf16(u),skf17(u)),skf15(u))**. % 2.48/2.71 63[0:Inp] || -> in(skf15(u),u)* in(skf15(u),cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),skc6))*. % 2.48/2.71 64[0:Inp] || element(u,powerset(powerset(v))) -> equal(complements_of_subsets(v,complements_of_subsets(v,u)),u)**. % 2.48/2.71 65[0:Inp] || element(u,powerset(powerset(v))) -> element(complements_of_subsets(v,u),powerset(powerset(v)))*. % 2.48/2.71 68[0:Inp] || element(skf16(u),powerset(the_carrier(skc4)))* -> equal(subset_complement(the_carrier(skc4),skf16(u)),skf17(u)). % 2.48/2.71 71[0:Inp] || element(skf25(u,v,w),powerset(the_carrier(v)))* -> equal(subset_complement(the_carrier(v),skf25(u,v,w)),skf26(w,v,u)). % 2.48/2.71 72[0:Inp] one_sorted_str(u) || in(v,skf24(w,x,u)) SkP0(x,u) element(x,powerset(powerset(the_carrier(u)))) -> in(v,cartesian_product2(complements_of_subsets(the_carrier(u),x),w))*. % 2.48/2.71 73[0:Inp] one_sorted_str(u) || in(v,skf24(w,x,u))* SkP0(x,u) element(x,powerset(powerset(the_carrier(u)))) -> in(skf25(x,u,y),complements_of_subsets(the_carrier(u),x))*. % 2.48/2.71 74[0:Inp] one_sorted_str(u) || in(v,skf24(w,x,u))* SkP0(x,u) element(x,powerset(powerset(the_carrier(u)))) -> equal(ordered_pair(skf25(x,u,v),skf26(v,u,x)),v)**. % 2.48/2.71 75[0:Inp] || in(u,complements_of_subsets(the_carrier(v),w))* in(x,cartesian_product2(complements_of_subsets(the_carrier(v),w),y))*+ equal(ordered_pair(u,z),x)* -> element(u,powerset(the_carrier(v))) in(x,skf24(y,w,v)). % 2.48/2.71 76[0:Inp] || in(u,complements_of_subsets(the_carrier(skc4),skc5))* in(skf15(v),v)* in(skf15(v),cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),skc6))*+ equal(ordered_pair(u,w),skf15(v))* -> element(u,powerset(the_carrier(skc4))). % 2.48/2.71 77[0:Inp] || in(u,complements_of_subsets(the_carrier(v),w))* equal(x,subset_complement(the_carrier(v),u))* in(y,cartesian_product2(complements_of_subsets(the_carrier(v),w),z))*+ equal(ordered_pair(u,x),y)* -> in(y,skf24(z,w,v)). % 2.48/2.71 78[0:Inp] || equal(u,subset_complement(the_carrier(skc4),v))* in(v,complements_of_subsets(the_carrier(skc4),skc5))* in(skf15(w),w)* in(skf15(w),cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),skc6))*+ equal(ordered_pair(v,u),skf15(w))* -> . % 2.48/2.71 79[0:Obv:60.0] || -> SkP0(u,v)*. % 2.48/2.71 80[0:MRR:72.2,79.0] one_sorted_str(u) || element(v,powerset(powerset(the_carrier(u)))) in(w,skf24(x,v,u)) -> in(w,cartesian_product2(complements_of_subsets(the_carrier(u),v),x))*. % 2.48/2.71 81[0:MRR:73.2,79.0] one_sorted_str(u) || element(v,powerset(powerset(the_carrier(u))))+ in(w,skf24(x,v,u))* -> in(skf25(v,u,y),complements_of_subsets(the_carrier(u),v))*. % 2.48/2.71 82[0:MRR:74.2,79.0] one_sorted_str(u) || element(v,powerset(powerset(the_carrier(u))))+ in(w,skf24(x,v,u))* -> equal(ordered_pair(skf25(v,u,w),skf26(w,u,v)),w)**. % 2.48/2.71 85[0:Res:1.0,80.0] || element(u,powerset(powerset(the_carrier(skc4)))) in(v,skf24(w,u,skc4)) -> in(v,cartesian_product2(complements_of_subsets(the_carrier(skc4),u),w))*. % 2.48/2.71 101[0:Res:21.0,82.2] one_sorted_str(skc4) || in(u,skf24(v,skc5,skc4))* -> equal(ordered_pair(skf25(skc5,skc4,u),skf26(u,skc4,skc5)),u)**. % 2.48/2.71 102[0:Res:21.0,81.2] one_sorted_str(skc4) || in(u,skf24(v,skc5,skc4))* -> in(skf25(skc5,skc4,w),complements_of_subsets(the_carrier(skc4),skc5))*. % 2.48/2.71 103[0:Res:21.0,80.2] one_sorted_str(skc4) || in(u,skf24(v,skc5,skc4)) -> in(u,cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),v))*. % 2.48/2.71 106[0:Res:21.0,64.0] || -> equal(complements_of_subsets(the_carrier(skc4),complements_of_subsets(the_carrier(skc4),skc5)),skc5)**. % 2.48/2.71 107[0:Res:21.0,65.0] || -> element(complements_of_subsets(the_carrier(skc4),skc5),powerset(powerset(the_carrier(skc4))))*. % 2.48/2.71 123[0:MRR:103.0,1.0] || in(u,skf24(v,skc5,skc4)) -> in(u,cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),v))*. % 2.48/2.71 124[0:MRR:102.0,1.0] || in(u,skf24(v,skc5,skc4))*+ -> in(skf25(skc5,skc4,w),complements_of_subsets(the_carrier(skc4),skc5))*. % 2.48/2.71 125[0:MRR:101.0,1.0] || in(u,skf24(v,skc5,skc4))*+ -> equal(ordered_pair(skf25(skc5,skc4,u),skf26(u,skc4,skc5)),u)**. % 2.48/2.71 129[1:Spt:56.0] || -> in(skf15(u),u)*. % 2.48/2.71 130[1:MRR:76.1,129.0] || in(u,complements_of_subsets(the_carrier(skc4),skc5))* in(skf15(v),cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),skc6))*+ equal(ordered_pair(u,w),skf15(v))* -> element(u,powerset(the_carrier(skc4))). % 2.48/2.71 131[1:MRR:78.2,129.0] || equal(u,subset_complement(the_carrier(skc4),v))* in(v,complements_of_subsets(the_carrier(skc4),skc5))* in(skf15(w),cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),skc6))*+ equal(ordered_pair(v,u),skf15(w))* -> . % 2.48/2.71 531[0:SpR:64.1,80.3] one_sorted_str(u) || element(v,powerset(powerset(the_carrier(u)))) element(complements_of_subsets(the_carrier(u),v),powerset(powerset(the_carrier(u)))) in(w,skf24(x,complements_of_subsets(the_carrier(u),v),u))* -> in(w,cartesian_product2(v,x)). % 2.48/2.71 535[0:MRR:531.2,65.1] one_sorted_str(u) || element(v,powerset(powerset(the_carrier(u)))) in(w,skf24(x,complements_of_subsets(the_carrier(u),v),u))* -> in(w,cartesian_product2(v,x)). % 2.48/2.71 700[1:Res:129.0,124.0] || -> in(skf25(skc5,skc4,u),complements_of_subsets(the_carrier(skc4),skc5))*. % 2.48/2.71 702[1:Res:129.0,125.0] || -> equal(ordered_pair(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5)),skf15(skf24(u,skc5,skc4)))**. % 2.48/2.71 708[0:SpR:64.1,85.2] || element(u,powerset(powerset(the_carrier(skc4)))) element(complements_of_subsets(the_carrier(skc4),u),powerset(powerset(the_carrier(skc4)))) in(v,skf24(w,complements_of_subsets(the_carrier(skc4),u),skc4))* -> in(v,cartesian_product2(u,w)). % 2.48/2.71 715[0:MRR:708.1,65.1] || element(u,powerset(powerset(the_carrier(skc4)))) in(v,skf24(w,complements_of_subsets(the_carrier(skc4),u),skc4))* -> in(v,cartesian_product2(u,w)). % 2.48/2.71 718[1:Res:129.0,715.1] || element(u,powerset(powerset(the_carrier(skc4)))) -> in(skf15(skf24(v,complements_of_subsets(the_carrier(skc4),u),skc4)),cartesian_product2(u,v))*. % 2.48/2.71 722[1:Res:718.1,130.1] || element(complements_of_subsets(the_carrier(skc4),skc5),powerset(powerset(the_carrier(skc4)))) in(u,complements_of_subsets(the_carrier(skc4),skc5))* equal(ordered_pair(u,v),skf15(skf24(skc6,complements_of_subsets(the_carrier(skc4),complements_of_subsets(the_carrier(skc4),skc5)),skc4)))* -> element(u,powerset(the_carrier(skc4))). % 2.48/2.71 723[1:Res:718.1,131.2] || element(complements_of_subsets(the_carrier(skc4),skc5),powerset(powerset(the_carrier(skc4)))) equal(u,subset_complement(the_carrier(skc4),v))* in(v,complements_of_subsets(the_carrier(skc4),skc5))* equal(ordered_pair(v,u),skf15(skf24(skc6,complements_of_subsets(the_carrier(skc4),complements_of_subsets(the_carrier(skc4),skc5)),skc4)))* -> . % 2.48/2.71 728[1:Rew:106.0,722.2] || element(complements_of_subsets(the_carrier(skc4),skc5),powerset(powerset(the_carrier(skc4))))* in(u,complements_of_subsets(the_carrier(skc4),skc5))* equal(ordered_pair(u,v),skf15(skf24(skc6,skc5,skc4)))* -> element(u,powerset(the_carrier(skc4))). % 2.48/2.71 729[1:MRR:728.0,107.0] || in(u,complements_of_subsets(the_carrier(skc4),skc5))* equal(ordered_pair(u,v),skf15(skf24(skc6,skc5,skc4)))*+ -> element(u,powerset(the_carrier(skc4))). % 2.48/2.71 730[1:Rew:106.0,723.3] || element(complements_of_subsets(the_carrier(skc4),skc5),powerset(powerset(the_carrier(skc4))))* equal(u,subset_complement(the_carrier(skc4),v))* in(v,complements_of_subsets(the_carrier(skc4),skc5))* equal(ordered_pair(v,u),skf15(skf24(skc6,skc5,skc4)))* -> . % 2.48/2.71 731[1:MRR:730.0,107.0] || equal(u,subset_complement(the_carrier(skc4),v))* in(v,complements_of_subsets(the_carrier(skc4),skc5))* equal(ordered_pair(v,u),skf15(skf24(skc6,skc5,skc4)))*+ -> . % 2.48/2.71 765[1:SpL:702.0,729.1] || in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),powerset(the_carrier(skc4))). % 2.48/2.71 766[1:MRR:765.0,700.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),powerset(the_carrier(skc4)))*. % 2.48/2.71 821[1:Res:766.1,71.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5))**. % 2.48/2.71 840[1:SpL:702.0,731.2] || equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5)) in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> . % 2.48/2.71 841[1:Rew:821.1,840.0] || equal(skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5)) in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> . % 2.48/2.71 842[1:Obv:841.0] || in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> . % 2.48/2.71 843[1:MRR:842.0,700.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4)))* -> . % 2.48/2.71 844[1:EqR:843.0] || -> . % 2.48/2.71 845[1:Spt:844.0,56.1] || -> in(skf16(u),complements_of_subsets(the_carrier(skc4),skc5))*. % 2.48/2.71 857[0:Res:63.0,535.2] one_sorted_str(u) || element(v,powerset(powerset(the_carrier(u))))+ -> in(skf15(skf24(w,complements_of_subsets(the_carrier(u),v),u)),cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),skc6))* in(skf15(skf24(w,complements_of_subsets(the_carrier(u),v),u)),cartesian_product2(v,w))*. % 2.48/2.71 859[0:Res:63.1,75.1] || in(u,complements_of_subsets(the_carrier(skc4),skc5))*+ equal(ordered_pair(u,v),skf15(w))* -> in(skf15(w),w)* element(u,powerset(the_carrier(skc4))) in(skf15(w),skf24(skc6,skc5,skc4))*. % 2.48/2.71 865[0:Res:123.1,76.2] || in(skf15(u),skf24(skc6,skc5,skc4))*+ in(v,complements_of_subsets(the_carrier(skc4),skc5))* in(skf15(u),u)* equal(ordered_pair(v,w),skf15(u))* -> element(v,powerset(the_carrier(skc4))). % 2.48/2.71 870[0:Res:63.0,124.0] || -> in(skf15(skf24(u,skc5,skc4)),cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),skc6))* in(skf25(skc5,skc4,v),complements_of_subsets(the_carrier(skc4),skc5))*. % 2.48/2.71 872[2:Spt:870.1] || -> in(skf25(skc5,skc4,u),complements_of_subsets(the_carrier(skc4),skc5))*. % 2.48/2.71 875[0:Res:123.1,78.3] || in(skf15(u),skf24(skc6,skc5,skc4))*+ equal(v,subset_complement(the_carrier(skc4),w))* in(w,complements_of_subsets(the_carrier(skc4),skc5))* in(skf15(u),u)* equal(ordered_pair(w,v),skf15(u))* -> . % 2.48/2.71 915[1:Res:845.0,859.0] || equal(ordered_pair(skf16(u),v),skf15(w))*+ -> in(skf15(w),w)* element(skf16(u),powerset(the_carrier(skc4)))* in(skf15(w),skf24(skc6,skc5,skc4))*. % 2.48/2.71 917[1:SpL:61.1,915.0] || equal(skf15(u),skf15(v))*+ -> in(skf15(u),u)* in(skf15(v),v)* element(skf16(u),powerset(the_carrier(skc4)))* in(skf15(v),skf24(skc6,skc5,skc4))*. % 2.48/2.71 918[1:EqR:917.0] || -> in(skf15(u),u)* in(skf15(u),u)* element(skf16(u),powerset(the_carrier(skc4))) in(skf15(u),skf24(skc6,skc5,skc4))*. % 2.48/2.71 919[1:Obv:918.0] || -> in(skf15(u),u)* element(skf16(u),powerset(the_carrier(skc4))) in(skf15(u),skf24(skc6,skc5,skc4))*. % 2.48/2.71 920[1:Fac:919.0,919.2] || -> element(skf16(skf24(skc6,skc5,skc4)),powerset(the_carrier(skc4))) in(skf15(skf24(skc6,skc5,skc4)),skf24(skc6,skc5,skc4))*. % 2.48/2.71 922[1:Res:919.0,125.0] || -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4))) in(skf15(skf24(u,skc5,skc4)),skf24(skc6,skc5,skc4)) equal(ordered_pair(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5)),skf15(skf24(u,skc5,skc4)))**. % 2.48/2.71 945[1:MRR:922.1,125.0] || -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4))) equal(ordered_pair(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5)),skf15(skf24(u,skc5,skc4)))**. % 2.48/2.71 1014[1:Res:920.1,865.0] || in(u,complements_of_subsets(the_carrier(skc4),skc5))* in(skf15(skf24(skc6,skc5,skc4)),skf24(skc6,skc5,skc4))* equal(ordered_pair(u,v),skf15(skf24(skc6,skc5,skc4)))* -> element(skf16(skf24(skc6,skc5,skc4)),powerset(the_carrier(skc4))) element(u,powerset(the_carrier(skc4))). % 2.48/2.71 1015[1:MRR:1014.1,920.1] || in(u,complements_of_subsets(the_carrier(skc4),skc5))* equal(ordered_pair(u,v),skf15(skf24(skc6,skc5,skc4)))*+ -> element(skf16(skf24(skc6,skc5,skc4)),powerset(the_carrier(skc4)))* element(u,powerset(the_carrier(skc4))). % 2.48/2.71 1016[3:Spt:1015.0,1015.1,1015.3] || in(u,complements_of_subsets(the_carrier(skc4),skc5))* equal(ordered_pair(u,v),skf15(skf24(skc6,skc5,skc4)))*+ -> element(u,powerset(the_carrier(skc4))). % 2.48/2.71 1018[3:SpL:945.1,1016.1] || in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4))) element(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),powerset(the_carrier(skc4))). % 2.48/2.71 1021[3:MRR:1018.0,872.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4))) element(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),powerset(the_carrier(skc4)))*. % 2.48/2.71 1084[3:Res:1021.2,71.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4))) equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5))**. % 2.48/2.71 1145[1:Res:920.1,875.0] || equal(u,subset_complement(the_carrier(skc4),v))* in(v,complements_of_subsets(the_carrier(skc4),skc5))* in(skf15(skf24(skc6,skc5,skc4)),skf24(skc6,skc5,skc4))* equal(ordered_pair(v,u),skf15(skf24(skc6,skc5,skc4)))* -> element(skf16(skf24(skc6,skc5,skc4)),powerset(the_carrier(skc4))). % 2.48/2.71 1146[1:MRR:1145.2,920.1] || equal(u,subset_complement(the_carrier(skc4),v))* in(v,complements_of_subsets(the_carrier(skc4),skc5))* equal(ordered_pair(v,u),skf15(skf24(skc6,skc5,skc4)))*+ -> element(skf16(skf24(skc6,skc5,skc4)),powerset(the_carrier(skc4)))*. % 2.48/2.71 1148[1:SpL:945.1,1146.2] || equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5)) in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4))) element(skf16(skf24(skc6,skc5,skc4)),powerset(the_carrier(skc4))). % 2.48/2.71 1151[3:Rew:1084.2,1148.0] || equal(skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5)) in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4))) element(skf16(skf24(skc6,skc5,skc4)),powerset(the_carrier(skc4))). % 2.48/2.71 1152[3:Obv:1151.0] || in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4))) element(skf16(skf24(skc6,skc5,skc4)),powerset(the_carrier(skc4))). % 2.48/2.71 1153[3:MRR:1152.0,872.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4)))+ -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4)))* element(skf16(skf24(skc6,skc5,skc4)),powerset(the_carrier(skc4)))*. % 2.48/2.71 1154[4:Spt:1153.0,1153.1] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4)))*. % 2.48/2.71 1170[4:Res:1154.1,68.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> equal(subset_complement(the_carrier(skc4),skf16(skf24(u,skc5,skc4))),skf17(skf24(u,skc5,skc4)))**. % 2.48/2.71 1245[0:Res:107.0,857.1] one_sorted_str(skc4) || -> in(skf15(skf24(u,complements_of_subsets(the_carrier(skc4),complements_of_subsets(the_carrier(skc4),skc5)),skc4)),cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),skc6))* in(skf15(skf24(u,complements_of_subsets(the_carrier(skc4),complements_of_subsets(the_carrier(skc4),skc5)),skc4)),cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),u))*. % 2.48/2.71 1249[0:Rew:106.0,1245.2,106.0,1245.1] one_sorted_str(skc4) || -> in(skf15(skf24(u,skc5,skc4)),cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),skc6))* in(skf15(skf24(u,skc5,skc4)),cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),u))*. % 2.48/2.71 1250[0:SSi:1249.0,1.0] || -> in(skf15(skf24(u,skc5,skc4)),cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),skc6))* in(skf15(skf24(u,skc5,skc4)),cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),u))*. % 2.48/2.71 1288[0:Fac:1250.0,1250.1] || -> in(skf15(skf24(skc6,skc5,skc4)),cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),skc6))*. % 2.48/2.71 1298[0:Res:1288.0,76.2] || in(u,complements_of_subsets(the_carrier(skc4),skc5))* in(skf15(skf24(skc6,skc5,skc4)),skf24(skc6,skc5,skc4))* equal(ordered_pair(u,v),skf15(skf24(skc6,skc5,skc4)))* -> element(u,powerset(the_carrier(skc4))). % 2.48/2.71 1299[0:Res:1288.0,75.1] || in(u,complements_of_subsets(the_carrier(skc4),skc5))* equal(ordered_pair(u,v),skf15(skf24(skc6,skc5,skc4)))* -> element(u,powerset(the_carrier(skc4))) in(skf15(skf24(skc6,skc5,skc4)),skf24(skc6,skc5,skc4))*. % 2.48/2.71 1300[0:Res:1288.0,77.2] || in(u,complements_of_subsets(the_carrier(skc4),skc5))* equal(v,subset_complement(the_carrier(skc4),u))* equal(ordered_pair(u,v),skf15(skf24(skc6,skc5,skc4)))* -> in(skf15(skf24(skc6,skc5,skc4)),skf24(skc6,skc5,skc4))*. % 2.48/2.71 1301[0:Res:1288.0,78.3] || equal(u,subset_complement(the_carrier(skc4),v))* in(v,complements_of_subsets(the_carrier(skc4),skc5))* in(skf15(skf24(skc6,skc5,skc4)),skf24(skc6,skc5,skc4))* equal(ordered_pair(v,u),skf15(skf24(skc6,skc5,skc4)))* -> . % 2.48/2.71 1302[0:MRR:1301.2,1300.3] || equal(u,subset_complement(the_carrier(skc4),v))* in(v,complements_of_subsets(the_carrier(skc4),skc5))* equal(ordered_pair(v,u),skf15(skf24(skc6,skc5,skc4)))*+ -> . % 2.48/2.71 1309[1:SpL:945.1,1302.2] || equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5)) in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4))). % 2.48/2.71 1310[0:SpL:61.1,1302.2] || equal(subset_complement(the_carrier(skc4),skf16(u)),skf17(u)) in(skf16(u),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(u),skf15(skf24(skc6,skc5,skc4))) -> in(skf15(u),u)*. % 2.48/2.71 1311[1:MRR:1310.1,845.0] || equal(subset_complement(the_carrier(skc4),skf16(u)),skf17(u))**+ equal(skf15(u),skf15(skf24(skc6,skc5,skc4))) -> in(skf15(u),u)*. % 2.48/2.71 1342[4:SpL:1170.1,1311.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) equal(skf17(skf24(u,skc5,skc4)),skf17(skf24(u,skc5,skc4))) equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> in(skf15(skf24(u,skc5,skc4)),skf24(u,skc5,skc4))*. % 2.48/2.71 1365[4:Obv:1342.1] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> in(skf15(skf24(u,skc5,skc4)),skf24(u,skc5,skc4))*. % 2.48/2.71 1443[4:Res:1365.1,125.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> equal(ordered_pair(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5)),skf15(skf24(u,skc5,skc4)))**. % 2.48/2.71 2047[4:SpL:1443.1,1016.1] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),powerset(the_carrier(skc4))). % 2.48/2.71 2051[4:SpL:1443.1,1302.2] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5)) in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> . % 2.48/2.71 2054[4:Obv:2047.0] || in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),powerset(the_carrier(skc4))). % 2.48/2.71 2055[4:MRR:2054.0,872.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),powerset(the_carrier(skc4)))*. % 2.48/2.71 2056[4:Obv:2051.0] || equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5)) in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> . % 2.48/2.71 2057[4:MRR:2056.1,872.0] || equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5))** equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> . % 2.48/2.71 2084[4:Res:2055.1,71.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5))**. % 2.48/2.71 2100[4:MRR:2084.1,2057.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4)))* -> . % 2.48/2.71 2101[4:EqR:2100.0] || -> . % 2.48/2.71 2102[4:Spt:2101.0,1153.2] || -> element(skf16(skf24(skc6,skc5,skc4)),powerset(the_carrier(skc4)))*. % 2.48/2.71 2121[4:Res:2102.0,68.0] || -> equal(subset_complement(the_carrier(skc4),skf16(skf24(skc6,skc5,skc4))),skf17(skf24(skc6,skc5,skc4)))**. % 2.48/2.71 2316[4:SpL:2121.0,1311.0] || equal(skf17(skf24(skc6,skc5,skc4)),skf17(skf24(skc6,skc5,skc4))) equal(skf15(skf24(skc6,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> in(skf15(skf24(skc6,skc5,skc4)),skf24(skc6,skc5,skc4))*. % 2.48/2.71 2341[4:Obv:2316.1] || -> in(skf15(skf24(skc6,skc5,skc4)),skf24(skc6,skc5,skc4))*. % 2.48/2.71 2458[4:Res:2341.0,125.0] || -> equal(ordered_pair(skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4))),skf26(skf15(skf24(skc6,skc5,skc4)),skc4,skc5)),skf15(skf24(skc6,skc5,skc4)))**. % 2.48/2.71 2753[4:SpL:2458.0,1016.1] || in(skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(skc6,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4))),powerset(the_carrier(skc4))). % 2.48/2.71 2759[4:SpL:2458.0,1302.2] || equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4)))),skf26(skf15(skf24(skc6,skc5,skc4)),skc4,skc5)) in(skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(skc6,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> . % 2.48/2.71 2768[4:Obv:2753.1] || in(skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* -> element(skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4))),powerset(the_carrier(skc4))). % 2.48/2.71 2769[4:MRR:2768.0,872.0] || -> element(skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4))),powerset(the_carrier(skc4)))*. % 2.48/2.71 2770[4:Obv:2759.2] || equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4)))),skf26(skf15(skf24(skc6,skc5,skc4)),skc4,skc5)) in(skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* -> . % 2.48/2.71 2771[4:MRR:2770.1,872.0] || equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4)))),skf26(skf15(skf24(skc6,skc5,skc4)),skc4,skc5))** -> . % 2.48/2.71 2787[4:Res:2769.0,71.0] || -> equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4)))),skf26(skf15(skf24(skc6,skc5,skc4)),skc4,skc5))**. % 2.48/2.71 2803[4:MRR:2787.0,2771.0] || -> . % 2.48/2.71 2804[3:Spt:2803.0,1015.2] || -> element(skf16(skf24(skc6,skc5,skc4)),powerset(the_carrier(skc4)))*. % 2.48/2.71 2805[0:MRR:1298.1,1299.3] || in(u,complements_of_subsets(the_carrier(skc4),skc5))* equal(ordered_pair(u,v),skf15(skf24(skc6,skc5,skc4)))*+ -> element(u,powerset(the_carrier(skc4))). % 2.48/2.71 2823[3:Res:2804.0,68.0] || -> equal(subset_complement(the_carrier(skc4),skf16(skf24(skc6,skc5,skc4))),skf17(skf24(skc6,skc5,skc4)))**. % 2.48/2.71 2942[3:SpL:2823.0,1311.0] || equal(skf17(skf24(skc6,skc5,skc4)),skf17(skf24(skc6,skc5,skc4))) equal(skf15(skf24(skc6,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> in(skf15(skf24(skc6,skc5,skc4)),skf24(skc6,skc5,skc4))*. % 2.48/2.71 2967[3:Obv:2942.1] || -> in(skf15(skf24(skc6,skc5,skc4)),skf24(skc6,skc5,skc4))*. % 2.48/2.71 3082[3:Res:2967.0,125.0] || -> equal(ordered_pair(skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4))),skf26(skf15(skf24(skc6,skc5,skc4)),skc4,skc5)),skf15(skf24(skc6,skc5,skc4)))**. % 2.48/2.71 3217[1:SpL:945.1,2805.1] || in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4))) element(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),powerset(the_carrier(skc4))). % 2.48/2.71 3246[3:SpL:3082.0,2805.1] || in(skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(skc6,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4))),powerset(the_carrier(skc4))). % 2.48/2.71 3248[3:SpL:3082.0,1302.2] || equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4)))),skf26(skf15(skf24(skc6,skc5,skc4)),skc4,skc5)) in(skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(skc6,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> . % 2.48/2.71 3257[3:Obv:3246.1] || in(skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* -> element(skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4))),powerset(the_carrier(skc4))). % 2.48/2.71 3258[3:MRR:3257.0,872.0] || -> element(skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4))),powerset(the_carrier(skc4)))*. % 2.48/2.71 3259[3:Obv:3248.2] || equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4)))),skf26(skf15(skf24(skc6,skc5,skc4)),skc4,skc5)) in(skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* -> . % 2.48/2.71 3260[3:MRR:3259.1,872.0] || equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4)))),skf26(skf15(skf24(skc6,skc5,skc4)),skc4,skc5))** -> . % 2.48/2.71 3276[3:Res:3258.0,71.0] || -> equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(skc6,skc5,skc4)))),skf26(skf15(skf24(skc6,skc5,skc4)),skc4,skc5))**. % 2.48/2.71 3292[3:MRR:3276.0,3260.0] || -> . % 2.48/2.71 3293[2:Spt:3292.0,870.0] || -> in(skf15(skf24(u,skc5,skc4)),cartesian_product2(complements_of_subsets(the_carrier(skc4),skc5),skc6))*. % 2.48/2.71 3304[1:Res:919.0,124.0] || -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4))) in(skf15(skf24(u,skc5,skc4)),skf24(skc6,skc5,skc4))* in(skf25(skc5,skc4,v),complements_of_subsets(the_carrier(skc4),skc5))*. % 2.48/2.71 3306[1:Res:919.2,124.0] || -> in(skf15(u),u)* element(skf16(u),powerset(the_carrier(skc4)))* in(skf25(skc5,skc4,v),complements_of_subsets(the_carrier(skc4),skc5))*. % 2.48/2.71 3307[1:MRR:3304.1,124.0] || -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4)))* in(skf25(skc5,skc4,v),complements_of_subsets(the_carrier(skc4),skc5))*. % 2.48/2.71 3308[1:MRR:3217.0,3307.1] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4))) element(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),powerset(the_carrier(skc4)))*. % 2.48/2.71 3310[1:MRR:1309.1,3307.1] || equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5))** equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4))). % 2.48/2.71 3316[3:Spt:3307.1] || -> in(skf25(skc5,skc4,u),complements_of_subsets(the_carrier(skc4),skc5))*. % 2.48/2.71 3393[1:Res:3308.2,71.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4))) equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5))**. % 2.48/2.71 3409[1:MRR:3393.2,3310.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4)))*. % 2.48/2.71 3425[1:Res:3409.1,68.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> equal(subset_complement(the_carrier(skc4),skf16(skf24(u,skc5,skc4))),skf17(skf24(u,skc5,skc4)))**. % 2.48/2.71 3563[1:SpL:3425.1,1311.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) equal(skf17(skf24(u,skc5,skc4)),skf17(skf24(u,skc5,skc4))) equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> in(skf15(skf24(u,skc5,skc4)),skf24(u,skc5,skc4))*. % 2.48/2.71 3589[1:Obv:3563.1] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> in(skf15(skf24(u,skc5,skc4)),skf24(u,skc5,skc4))*. % 2.48/2.71 3682[1:Res:3589.1,125.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> equal(ordered_pair(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5)),skf15(skf24(u,skc5,skc4)))**. % 2.48/2.71 4203[1:SpL:3682.1,2805.1] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),powerset(the_carrier(skc4))). % 2.48/2.71 4207[1:SpL:3682.1,1302.2] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5)) in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> . % 2.48/2.71 4217[1:Obv:4203.0] || in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),powerset(the_carrier(skc4))). % 2.48/2.71 4218[3:MRR:4217.0,3316.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),powerset(the_carrier(skc4)))*. % 2.48/2.71 4219[1:Obv:4207.0] || equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5)) in(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),complements_of_subsets(the_carrier(skc4),skc5))* equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> . % 2.48/2.71 4220[3:MRR:4219.1,3316.0] || equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5))** equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> . % 2.48/2.71 4245[3:Res:4218.1,71.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5))**. % 2.48/2.71 4261[3:MRR:4245.1,4220.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4)))* -> . % 2.48/2.71 4262[3:EqR:4261.0] || -> . % 2.48/2.71 4263[3:Spt:4262.0,3307.0] || -> element(skf16(skf24(u,skc5,skc4)),powerset(the_carrier(skc4)))*. % 2.48/2.71 4717[4:Spt:3306.0,3306.1] || -> in(skf15(u),u)* element(skf16(u),powerset(the_carrier(skc4)))*. % 2.48/2.71 4777[4:Res:4717.1,68.0] || -> in(skf15(u),u)* equal(subset_complement(the_carrier(skc4),skf16(u)),skf17(u))**. % 2.48/2.71 4795[4:Rew:4777.1,1311.0] || equal(skf17(u),skf17(u)) equal(skf15(u),skf15(skf24(skc6,skc5,skc4)))* -> in(skf15(u),u)*. % 2.48/2.71 4801[4:Obv:4795.0] || equal(skf15(u),skf15(skf24(skc6,skc5,skc4)))*+ -> in(skf15(u),u)*. % 2.48/2.71 5317[4:EqR:4801.0] || -> in(skf15(skf24(skc6,skc5,skc4)),skf24(skc6,skc5,skc4))*. % 2.48/2.71 5333[4:Res:5317.0,124.0] || -> in(skf25(skc5,skc4,u),complements_of_subsets(the_carrier(skc4),skc5))*. % 2.48/2.71 5339[4:MRR:4217.0,5333.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),powerset(the_carrier(skc4)))*. % 2.48/2.71 5340[4:MRR:4219.1,5333.0] || equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5))** equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> . % 2.55/2.74 5499[4:Res:5339.1,71.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5))**. % 2.55/2.74 5515[4:MRR:5499.1,5340.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4)))* -> . % 2.55/2.74 5516[4:EqR:5515.0] || -> . % 2.55/2.74 5517[4:Spt:5516.0,3306.2] || -> in(skf25(skc5,skc4,u),complements_of_subsets(the_carrier(skc4),skc5))*. % 2.55/2.74 5518[4:MRR:4217.0,5517.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> element(skf25(skc5,skc4,skf15(skf24(u,skc5,skc4))),powerset(the_carrier(skc4)))*. % 2.55/2.74 5519[4:MRR:4219.1,5517.0] || equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5))** equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> . % 2.55/2.74 5608[4:Res:5518.1,71.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4))) -> equal(subset_complement(the_carrier(skc4),skf25(skc5,skc4,skf15(skf24(u,skc5,skc4)))),skf26(skf15(skf24(u,skc5,skc4)),skc4,skc5))**. % 2.55/2.74 5624[4:MRR:5608.1,5519.0] || equal(skf15(skf24(u,skc5,skc4)),skf15(skf24(skc6,skc5,skc4)))* -> . % 2.55/2.74 5626[4:EqR:5624.0] || -> . % 2.55/2.74 % SZS output end Refutation % 2.55/2.74 Formulae used in the proof : s1_xboole_0__e4_7_1__tops_2__1 antisymmetry_r2_hidden dt_k3_subset_1 involutiveness_k3_subset_1 s1_tarski__e4_7_1__tops_2__2 involutiveness_k7_setfam_1 dt_k7_setfam_1 % 2.55/2.74 %------------------------------------------------------------------------------