%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU334+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n006.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:21 EDT 2022 % Result : Theorem 131.83s 132.08s % Output : Refutation 133.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SEU334+1 : TPTP v8.1.0. Released v3.3.0. % 0.07/0.14 % Command : run_spass %d %s % 0.14/0.35 % Computer : n006.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Sun Jun 19 20:44:40 EDT 2022 % 0.14/0.36 % CPUTime : % 131.83/132.08 % 131.83/132.08 SPASS V 3.9 % 131.83/132.08 SPASS beiseite: Proof found. % 131.83/132.08 % SZS status Theorem % 131.83/132.08 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 131.83/132.08 SPASS derived 36352 clauses, backtracked 5680 clauses, performed 32 splits and kept 27870 clauses. % 131.83/132.08 SPASS allocated 132741 KBytes. % 131.83/132.08 SPASS spent 0:2:11.67 on the problem. % 131.83/132.08 0:00:00.03 for the input. % 131.83/132.08 0:00:00.06 for the FLOTTER CNF translation. % 131.83/132.08 0:00:00.73 for inferences. % 131.83/132.08 0:00:02.94 for the backtracking. % 131.83/132.08 0:02:07.42 for the reduction. % 131.83/132.08 % 131.83/132.08 % 131.83/132.08 Here is a proof with depth 12, length 374 : % 131.83/132.08 % SZS output start Refutation % 131.83/132.08 1[0:Inp] || -> one_sorted_str(skc9)*. % 131.83/132.08 2[0:Inp] || -> v1_membered(skc12)*. % 131.83/132.08 3[0:Inp] || -> v2_membered(skc12)*. % 131.83/132.08 4[0:Inp] || -> v3_membered(skc12)*. % 131.83/132.08 5[0:Inp] || -> v4_membered(skc12)*. % 131.83/132.08 6[0:Inp] || -> v5_membered(skc12)*. % 131.83/132.08 9[0:Inp] || -> relation_empty_yielding(empty_set)*. % 131.83/132.08 11[0:Inp] || -> empty(empty_set)*. % 131.83/132.08 12[0:Inp] || -> relation(empty_set)*. % 131.83/132.08 22[0:Inp] || -> empty(skf16(u))*. % 131.83/132.08 26[0:Inp] || -> relation(skf17(u,v))*. % 131.83/132.08 27[0:Inp] || -> element(skf25(u),u)*. % 131.83/132.08 37[0:Inp] empty(u) || -> v5_membered(u)*. % 131.83/132.08 39[0:Inp] || -> element(skf16(u),powerset(u))*. % 131.83/132.08 40[0:Inp] empty(u) || -> function(u)*. % 131.83/132.08 41[0:Inp] empty(u) || -> relation(u)*. % 131.83/132.08 43[0:Inp] || empty(unordered_pair(u,v))* -> . % 131.83/132.08 44[0:Inp] || -> element(skc10,powerset(powerset(the_carrier(skc9))))*. % 131.83/132.08 46[0:Inp] empty(u) || -> empty(relation_dom(u))*. % 131.83/132.08 48[0:Inp] empty(u) || -> equal(u,empty_set)*. % 131.83/132.08 51[0:Inp] empty(u) || in(v,u)* -> . % 131.83/132.08 53[0:Inp] || -> SkP0(u,v)* in(skf20(v,w),v)*. % 131.83/132.08 54[0:Inp] || in(u,skc10) -> SkP1(skf13(u),skc9,u)*. % 131.83/132.08 55[0:Inp] || -> element(u,powerset(the_carrier(v)))* SkP1(w,v,u)*. % 131.83/132.08 72[0:Inp] || element(u,v) -> empty(v) in(u,v)*. % 131.83/132.08 74[0:Inp] v1_membered(u) || element(v,powerset(u))* -> v1_membered(v). % 131.83/132.08 76[0:Inp] v2_membered(u) || element(v,powerset(u))* -> v2_membered(v). % 131.83/132.08 79[0:Inp] v3_membered(u) || element(v,powerset(u))* -> v3_membered(v). % 131.83/132.08 83[0:Inp] v4_membered(u) || element(v,powerset(u))* -> v4_membered(v). % 131.83/132.08 84[0:Inp] v5_membered(u) || element(v,powerset(u))* -> v1_membered(v). % 131.83/132.08 85[0:Inp] v5_membered(u) || element(v,powerset(u))* -> v2_membered(v). % 131.83/132.08 86[0:Inp] v5_membered(u) || element(v,powerset(u))* -> v3_membered(v). % 131.83/132.08 87[0:Inp] v5_membered(u) || element(v,powerset(u))* -> v4_membered(v). % 131.83/132.08 88[0:Inp] v5_membered(u) || element(v,powerset(u))* -> v5_membered(v). % 131.83/132.08 90[0:Inp] || equal(u,subset_complement(the_carrier(v),w))*+ -> SkP1(u,v,w)*. % 131.83/132.08 92[0:Inp] || equal(skf19(u,v),skf18(u,v))**+ -> SkP0(w,x)*. % 131.83/132.08 95[0:Inp] || -> equal(u,v) in(skf26(v,u),v)* in(skf26(v,u),u)*. % 131.83/132.08 96[0:Inp] || in(skf23(u,v),v)* in(ordered_pair(skf23(u,v),w),u)*+ -> . % 131.83/132.08 97[0:Inp] function(u) relation(u) || equal(relation_dom(u),skc10)**+ -> in(skf14(v),skc10)*. % 131.83/132.08 98[0:Inp] || in(u,skc10) SkP1(v,skc9,u)*+ SkP1(w,skc9,u)* -> equal(w,v)*. % 131.83/132.08 100[0:Inp] relation(u) || equal(v,relation_dom(u))* in(ordered_pair(w,x),u)*+ -> in(w,v)*. % 131.83/132.08 101[0:Inp] one_sorted_str(u) || SkP0(u,v) element(v,powerset(powerset(the_carrier(u))))* -> function(skf17(u,v)). % 131.83/132.08 104[0:Inp] relation(u) || in(v,w)* equal(w,relation_dom(u))*+ -> in(ordered_pair(v,skf21(u,v)),u)*. % 131.83/132.08 105[0:Inp] function(u) relation(u) || equal(relation_dom(u),skc10) SkP1(apply(u,skf14(u)),skc9,skf14(u))* -> . % 131.83/132.08 106[0:Inp] relation(u) || -> equal(v,relation_dom(u)) in(skf23(u,v),v) in(ordered_pair(skf23(u,v),skf24(v,u)),u)*. % 131.83/132.08 107[0:Inp] || element(skf20(u,v),powerset(the_carrier(v)))* -> equal(subset_complement(the_carrier(v),skf20(u,v)),skf18(v,u)) SkP0(v,u). % 131.83/132.08 108[0:Inp] || element(skf20(u,v),powerset(the_carrier(v)))* -> equal(subset_complement(the_carrier(v),skf20(u,v)),skf19(v,u)) SkP0(v,u). % 131.83/132.08 109[0:Inp] function(u) relation(u) || in(v,relation_dom(u)) in(ordered_pair(v,w),u)* -> equal(w,apply(u,v)). % 131.83/132.08 110[0:Inp] function(u) relation(u) || in(v,relation_dom(u)) equal(w,apply(u,v)) -> in(ordered_pair(v,w),u)*. % 131.83/132.08 111[0:Inp] one_sorted_str(u) || SkP0(u,v) element(v,powerset(powerset(the_carrier(u)))) in(ordered_pair(w,x),skf17(u,v))* -> in(w,v). % 131.83/132.08 112[0:Inp] one_sorted_str(u) || in(v,w) SkP0(u,w) element(w,powerset(powerset(the_carrier(u)))) -> element(v,powerset(the_carrier(u))) in(ordered_pair(v,x),skf17(u,w))*. % 131.83/132.08 113[0:Inp] one_sorted_str(u) || SkP0(u,v) in(w,v) element(v,powerset(powerset(the_carrier(u)))) equal(x,subset_complement(the_carrier(u),w)) -> in(ordered_pair(w,x),skf17(u,v))*. % 131.83/132.08 114[0:Inp] one_sorted_str(u) || SkP0(u,v) element(w,powerset(the_carrier(u))) element(v,powerset(powerset(the_carrier(u)))) in(ordered_pair(w,x),skf17(u,v))* -> equal(x,subset_complement(the_carrier(u),w)). % 131.83/132.08 116[0:Rew:107.1,108.1] || element(skf20(u,v),powerset(the_carrier(v)))* -> equal(skf19(v,u),skf18(v,u)) SkP0(v,u). % 131.83/132.08 117[0:MRR:116.1,92.0] || element(skf20(u,v),powerset(the_carrier(v)))* -> SkP0(v,u). % 131.83/132.08 154[0:Res:44.0,111.1] one_sorted_str(skc9) || SkP0(skc9,skc10) in(ordered_pair(u,v),skf17(skc9,skc10))* -> in(u,skc10). % 131.83/132.08 155[0:Res:44.0,101.2] one_sorted_str(skc9) || SkP0(skc9,skc10) -> function(skf17(skc9,skc10))*. % 131.83/132.08 156[0:Res:44.0,113.2] one_sorted_str(skc9) || in(u,skc10) SkP0(skc9,skc10) equal(v,subset_complement(the_carrier(skc9),u)) -> in(ordered_pair(u,v),skf17(skc9,skc10))*. % 131.83/132.08 157[0:Res:44.0,114.2] one_sorted_str(skc9) || in(ordered_pair(u,v),skf17(skc9,skc10))* SkP0(skc9,skc10) element(u,powerset(the_carrier(skc9))) -> equal(v,subset_complement(the_carrier(skc9),u)). % 131.83/132.08 178[0:MRR:155.0,1.0] || SkP0(skc9,skc10) -> function(skf17(skc9,skc10))*. % 131.83/132.08 182[0:MRR:154.0,1.0] || SkP0(skc9,skc10) in(ordered_pair(u,v),skf17(skc9,skc10))* -> in(u,skc10). % 131.83/132.08 184[0:MRR:156.0,1.0] || in(u,skc10) equal(v,subset_complement(the_carrier(skc9),u)) SkP0(skc9,skc10) -> in(ordered_pair(u,v),skf17(skc9,skc10))*. % 131.83/132.08 185[0:MRR:157.0,1.0] || element(u,powerset(the_carrier(skc9))) SkP0(skc9,skc10) in(ordered_pair(u,v),skf17(skc9,skc10))* -> equal(v,subset_complement(the_carrier(skc9),u)). % 131.83/132.08 191[1:Spt:97.0,97.1,97.2] function(u) relation(u) || equal(relation_dom(u),skc10)** -> . % 131.83/132.08 192[0:EmS:48.0,22.0] || -> equal(skf16(u),empty_set)**. % 131.83/132.08 202[0:Rew:192.0,39.0] || -> element(empty_set,powerset(u))*. % 131.83/132.08 207[0:EmS:48.0,46.1] empty(u) || -> equal(relation_dom(u),empty_set)**. % 131.83/132.08 248[1:SpL:207.1,191.2] empty(u) function(u) relation(u) || equal(skc10,empty_set)** -> . % 131.83/132.08 249[1:SSi:248.2,248.1,41.1,40.1] empty(u) || equal(skc10,empty_set)** -> . % 131.83/132.08 250[1:EmS:249.0,11.0] || equal(skc10,empty_set)** -> . % 131.83/132.08 458[0:Res:202.0,74.1] v1_membered(u) || -> v1_membered(empty_set)*. % 131.83/132.08 465[0:EmS:458.0,2.0] || -> v1_membered(empty_set)*. % 131.83/132.08 497[0:Res:202.0,76.1] v2_membered(u) || -> v2_membered(empty_set)*. % 131.83/132.08 504[0:EmS:497.0,3.0] || -> v2_membered(empty_set)*. % 131.83/132.08 528[0:Res:202.0,79.1] v3_membered(u) || -> v3_membered(empty_set)*. % 131.83/132.08 535[0:EmS:528.0,4.0] || -> v3_membered(empty_set)*. % 131.83/132.08 552[0:Res:202.0,83.1] v4_membered(u) || -> v4_membered(empty_set)*. % 131.83/132.08 559[0:EmS:552.0,5.0] || -> v4_membered(empty_set)*. % 131.83/132.08 569[0:Res:202.0,88.1] v5_membered(u) || -> v5_membered(empty_set)*. % 131.83/132.08 575[0:EmS:569.0,6.0] || -> v5_membered(empty_set)*. % 131.83/132.08 618[0:EqR:90.0] || -> SkP1(subset_complement(the_carrier(u),v),u,v)*. % 131.83/132.08 672[0:Res:54.1,98.1] || in(u,skc10) in(u,skc10) SkP1(v,skc9,u)* -> equal(v,skf13(u)). % 131.83/132.08 673[0:Res:55.1,98.1] || in(u,skc10) SkP1(v,skc9,u)* -> element(u,powerset(the_carrier(skc9)))* equal(v,w)*. % 131.83/132.08 676[0:Obv:672.0] || in(u,skc10) SkP1(v,skc9,u)* -> equal(v,skf13(u)). % 131.83/132.08 677[0:MRR:673.1,55.1] || in(u,skc10)+ -> element(u,powerset(the_carrier(skc9)))* equal(v,w)*. % 131.83/132.08 723[0:EqR:104.2] relation(u) || in(v,relation_dom(u)) -> in(ordered_pair(v,skf21(u,v)),u)*. % 131.83/132.08 728[0:Res:106.3,51.1] relation(u) empty(u) || -> equal(v,relation_dom(u)) in(skf23(u,v),v)*. % 131.83/132.08 733[0:Rew:207.1,728.2] relation(u) empty(u) || -> equal(v,empty_set) in(skf23(u,v),v)*. % 131.83/132.08 734[0:SSi:733.0,41.1] empty(u) || -> equal(v,empty_set) in(skf23(u,v),v)*. % 131.83/132.08 743[0:Res:110.4,51.1] function(u) relation(u) empty(u) || in(v,relation_dom(u))* equal(w,apply(u,v))* -> . % 131.83/132.08 749[0:AED:743.4] function(u) relation(u) empty(u) || in(v,relation_dom(u))* -> . % 131.83/132.08 750[0:Rew:207.1,749.3] function(u) relation(u) empty(u) || in(v,empty_set)* -> . % 131.83/132.08 751[0:SSi:750.1,750.0,41.1,40.1] empty(u) || in(v,empty_set)* -> . % 131.83/132.08 756[0:EmS:751.0,11.0] || in(u,empty_set)* -> . % 131.83/132.08 757[0:Res:95.2,756.0] || -> equal(empty_set,u) in(skf26(u,empty_set),u)*. % 131.83/132.08 759[0:Res:110.4,756.0] function(empty_set) relation(empty_set) || in(u,relation_dom(empty_set))* equal(v,apply(empty_set,u))* -> . % 131.83/132.08 765[0:AED:759.3] function(empty_set) relation(empty_set) || in(u,relation_dom(empty_set))* -> . % 131.83/132.08 766[0:SSi:765.1,765.0,9.0,12.0,11.0,465.0,504.0,535.0,559.0,575.0,40.1,9.0,12.0,11.0,465.0,504.0,535.0,559.0,575.0] || in(u,relation_dom(empty_set))* -> . % 131.83/132.08 771[0:Res:72.2,766.0] || element(u,relation_dom(empty_set))* -> empty(relation_dom(empty_set)). % 131.83/132.08 782[0:Res:27.0,771.0] || -> empty(relation_dom(empty_set))*. % 131.83/132.08 785[0:EmS:48.0,782.0] || -> equal(relation_dom(empty_set),empty_set)**. % 131.83/132.08 807[0:Res:106.3,111.3] relation(skf17(u,v)) one_sorted_str(u) || SkP0(u,v) element(v,powerset(powerset(the_carrier(u)))) -> equal(w,relation_dom(skf17(u,v))) in(skf23(skf17(u,v),w),w)* in(skf23(skf17(u,v),w),v)*. % 131.83/132.08 808[0:Res:110.4,111.3] function(skf17(u,v)) relation(skf17(u,v)) one_sorted_str(u) || in(w,relation_dom(skf17(u,v)))* equal(x,apply(skf17(u,v),w))* SkP0(u,v) element(v,powerset(powerset(the_carrier(u)))) -> in(w,v). % 131.83/132.08 810[0:SSi:807.0,26.0] one_sorted_str(u) || SkP0(u,v) element(v,powerset(powerset(the_carrier(u))))+ -> equal(w,relation_dom(skf17(u,v))) in(skf23(skf17(u,v),w),w)* in(skf23(skf17(u,v),w),v)*. % 131.83/132.08 811[0:AED:808.4] function(skf17(u,v)) relation(skf17(u,v)) one_sorted_str(u) || in(w,relation_dom(skf17(u,v)))* SkP0(u,v) element(v,powerset(powerset(the_carrier(u)))) -> in(w,v). % 131.83/132.08 812[0:SSi:811.1,26.0] function(skf17(u,v)) one_sorted_str(u) || in(w,relation_dom(skf17(u,v)))* SkP0(u,v) element(v,powerset(powerset(the_carrier(u)))) -> in(w,v). % 131.83/132.08 813[0:MRR:812.0,101.3] one_sorted_str(u) || in(v,relation_dom(skf17(u,w)))* SkP0(u,w) element(w,powerset(powerset(the_carrier(u)))) -> in(v,w). % 131.83/132.08 818[0:SpL:785.0,104.2] relation(empty_set) || in(u,v)* equal(v,empty_set) -> in(ordered_pair(u,skf21(empty_set,u)),empty_set)*. % 131.83/132.08 819[0:SSi:818.0,9.0,12.0,11.0,465.0,504.0,535.0,559.0,575.0] || in(u,v)* equal(v,empty_set) -> in(ordered_pair(u,skf21(empty_set,u)),empty_set)*. % 131.83/132.08 820[0:MRR:819.2,756.0] || in(u,v)* equal(v,empty_set) -> . % 131.83/132.08 842[0:Res:112.5,109.3] one_sorted_str(u) function(skf17(u,v)) relation(skf17(u,v)) || in(w,v) SkP0(u,v) element(v,powerset(powerset(the_carrier(u)))) in(w,relation_dom(skf17(u,v)))* -> element(w,powerset(the_carrier(u))) equal(x,apply(skf17(u,v),w))*. % 131.83/132.08 848[0:SSi:842.2,26.0] one_sorted_str(u) function(skf17(u,v)) || in(w,v) SkP0(u,v) element(v,powerset(powerset(the_carrier(u)))) in(w,relation_dom(skf17(u,v)))* -> element(w,powerset(the_carrier(u))) equal(x,apply(skf17(u,v),w))*. % 131.83/132.08 849[0:MRR:848.1,101.3] one_sorted_str(u) || in(v,w) SkP0(u,w) element(w,powerset(powerset(the_carrier(u)))) in(v,relation_dom(skf17(u,w)))* -> element(v,powerset(the_carrier(u))) equal(x,apply(skf17(u,w),v))*. % 131.83/132.08 850[0:MRR:849.1,813.4] one_sorted_str(u) || SkP0(u,v) element(v,powerset(powerset(the_carrier(u))))+ in(w,relation_dom(skf17(u,v)))* -> element(w,powerset(the_carrier(u))) equal(x,apply(skf17(u,v),w))*. % 131.83/132.08 858[0:Res:72.2,820.0] || element(u,v)* equal(v,empty_set) -> empty(v). % 131.83/132.08 867[0:Res:113.5,96.1] one_sorted_str(u) || SkP0(u,v) in(skf23(skf17(u,v),w),v)* element(v,powerset(powerset(the_carrier(u)))) equal(x,subset_complement(the_carrier(u),skf23(skf17(u,v),w)))* in(skf23(skf17(u,v),w),w)* -> . % 131.83/132.08 868[0:Res:113.5,100.2] one_sorted_str(u) relation(skf17(u,v)) || SkP0(u,v) in(w,v)* element(v,powerset(powerset(the_carrier(u))))* equal(x,subset_complement(the_carrier(u),w))* equal(y,relation_dom(skf17(u,v)))* -> in(w,y)*. % 131.83/132.08 877[0:AED:868.5] one_sorted_str(u) relation(skf17(u,v)) || SkP0(u,v) in(w,v)* element(v,powerset(powerset(the_carrier(u))))* equal(x,relation_dom(skf17(u,v)))* -> in(w,x)*. % 131.83/132.08 878[0:SSi:877.1,26.0] one_sorted_str(u) || SkP0(u,v) in(w,v)* element(v,powerset(powerset(the_carrier(u))))*+ equal(x,relation_dom(skf17(u,v)))* -> in(w,x)*. % 131.83/132.08 879[0:AED:867.4] one_sorted_str(u) || SkP0(u,v) in(skf23(skf17(u,v),w),v)*+ element(v,powerset(powerset(the_carrier(u)))) in(skf23(skf17(u,v),w),w)* -> . % 131.83/132.08 982[0:Res:110.4,114.4] function(skf17(u,v)) relation(skf17(u,v)) one_sorted_str(u) || in(w,relation_dom(skf17(u,v)))* equal(x,apply(skf17(u,v),w))* SkP0(u,v) element(w,powerset(the_carrier(u))) element(v,powerset(powerset(the_carrier(u)))) -> equal(x,subset_complement(the_carrier(u),w)). % 131.83/132.08 986[0:SSi:982.1,26.0] function(skf17(u,v)) one_sorted_str(u) || in(w,relation_dom(skf17(u,v)))* equal(x,apply(skf17(u,v),w))* SkP0(u,v) element(w,powerset(the_carrier(u))) element(v,powerset(powerset(the_carrier(u)))) -> equal(x,subset_complement(the_carrier(u),w)). % 131.83/132.08 987[0:MRR:986.0,101.3] one_sorted_str(u) || in(v,relation_dom(skf17(u,w)))* equal(x,apply(skf17(u,w),v))*+ SkP0(u,w) element(v,powerset(the_carrier(u))) element(w,powerset(powerset(the_carrier(u)))) -> equal(x,subset_complement(the_carrier(u),v)). % 131.83/132.08 1013[0:Res:27.0,858.0] || equal(u,empty_set) -> empty(u)*. % 131.83/132.08 1062[0:Res:1013.1,43.0] || equal(unordered_pair(u,v),empty_set)** -> . % 131.83/132.08 1155[2:Spt:677.2] || -> equal(u,v)*. % 131.83/132.08 1156[2:UnC:1155.0,1062.0] || -> . % 131.83/132.08 1157[2:Spt:1156.0,677.0,677.1] || in(u,skc10) -> element(u,powerset(the_carrier(skc9)))*. % 131.83/132.08 1173[2:Res:1157.1,88.1] v5_membered(the_carrier(skc9)) || in(u,skc10)* -> v5_membered(u). % 131.83/132.08 1174[2:Res:1157.1,87.1] v5_membered(the_carrier(skc9)) || in(u,skc10)* -> v4_membered(u). % 131.83/132.08 1176[2:Res:1157.1,86.1] v5_membered(the_carrier(skc9)) || in(u,skc10)* -> v3_membered(u). % 131.83/132.08 1179[2:Res:1157.1,85.1] v5_membered(the_carrier(skc9)) || in(u,skc10)* -> v2_membered(u). % 131.83/132.08 1189[2:Res:1157.1,117.0] || in(skf20(u,skc9),skc10)* -> SkP0(skc9,u). % 131.83/132.08 1193[2:Res:72.2,1189.0] || element(skf20(u,skc9),skc10)* -> empty(skc10) SkP0(skc9,u). % 131.83/132.08 1194[2:Res:53.1,1189.0] || -> SkP0(u,skc10)* SkP0(skc9,skc10)*. % 131.83/132.08 1195[2:Con:1194.0] || -> SkP0(skc9,skc10)*. % 131.83/132.08 1196[2:MRR:178.0,1195.0] || -> function(skf17(skc9,skc10))*. % 131.83/132.08 1197[2:MRR:182.0,1195.0] || in(ordered_pair(u,v),skf17(skc9,skc10))* -> in(u,skc10). % 131.83/132.08 1198[2:MRR:184.2,1195.0] || in(u,skc10) equal(v,subset_complement(the_carrier(skc9),u)) -> in(ordered_pair(u,v),skf17(skc9,skc10))*. % 131.83/132.08 1200[2:SoR:1173.0,37.1] empty(the_carrier(skc9)) || in(u,skc10)* -> v5_membered(u). % 131.83/132.08 1201[2:SoR:1174.0,37.1] empty(the_carrier(skc9)) || in(u,skc10)* -> v4_membered(u). % 131.83/132.08 1204[2:SoR:1176.0,37.1] empty(the_carrier(skc9)) || in(u,skc10)* -> v3_membered(u). % 131.83/132.08 1205[2:Res:106.3,1197.0] relation(skf17(skc9,skc10)) || -> equal(u,relation_dom(skf17(skc9,skc10))) in(skf23(skf17(skc9,skc10),u),u)* in(skf23(skf17(skc9,skc10),u),skc10)*. % 131.83/132.08 1206[2:Res:110.4,1197.0] function(skf17(skc9,skc10)) relation(skf17(skc9,skc10)) || in(u,relation_dom(skf17(skc9,skc10)))* equal(v,apply(skf17(skc9,skc10),u))* -> in(u,skc10). % 131.83/132.08 1210[2:SSi:1205.0,1196.0,26.0,1.0] || -> equal(u,relation_dom(skf17(skc9,skc10))) in(skf23(skf17(skc9,skc10),u),u)* in(skf23(skf17(skc9,skc10),u),skc10)*. % 131.83/132.08 1211[2:AED:1206.3] function(skf17(skc9,skc10)) relation(skf17(skc9,skc10)) || in(u,relation_dom(skf17(skc9,skc10)))* -> in(u,skc10). % 131.83/132.08 1212[2:SSi:1211.1,1211.0,1196.0,26.0,1.0,1196.0,26.0,1.0] || in(u,relation_dom(skf17(skc9,skc10)))* -> in(u,skc10). % 131.83/132.08 1217[2:SoR:1179.0,37.1] empty(the_carrier(skc9)) || in(u,skc10)* -> v2_membered(u). % 131.83/132.08 1235[2:SoR:1200.0,1013.1] || in(u,skc10)* equal(the_carrier(skc9),empty_set) -> v5_membered(u). % 131.83/132.08 1237[2:SoR:1201.0,1013.1] || in(u,skc10)* equal(the_carrier(skc9),empty_set) -> v4_membered(u). % 131.83/132.08 1238[2:SoR:1204.0,1013.1] || in(u,skc10)* equal(the_carrier(skc9),empty_set) -> v3_membered(u). % 131.83/132.08 1240[2:Res:757.1,1212.0] || -> equal(relation_dom(skf17(skc9,skc10)),empty_set) in(skf26(relation_dom(skf17(skc9,skc10)),empty_set),skc10)*. % 131.83/132.08 1252[2:SoR:1217.0,1013.1] || in(u,skc10)* equal(the_carrier(skc9),empty_set) -> v2_membered(u). % 131.83/132.08 1435[3:Spt:1193.1] || -> empty(skc10)*. % 131.83/132.08 1439[3:EmS:48.0,1435.0] || -> equal(skc10,empty_set)**. % 131.83/132.08 1441[3:MRR:1439.0,250.0] || -> . % 131.83/132.08 1448[3:Spt:1441.0,1193.1,1435.0] || empty(skc10)* -> . % 131.83/132.08 1449[3:Spt:1441.0,1193.0,1193.2] || element(skf20(u,skc9),skc10)* -> SkP0(skc9,u). % 131.83/132.08 1523[2:Res:53.1,1235.0] || equal(the_carrier(skc9),empty_set)+ -> SkP0(u,skc10)* v5_membered(skf20(skc10,v))*. % 131.83/132.08 1543[2:Res:53.1,1237.0] || equal(the_carrier(skc9),empty_set)+ -> SkP0(u,skc10)* v4_membered(skf20(skc10,v))*. % 131.83/132.08 1562[2:Res:53.1,1238.0] || equal(the_carrier(skc9),empty_set)+ -> SkP0(u,skc10)* v3_membered(skf20(skc10,v))*. % 131.83/132.08 1582[2:Res:53.1,1252.0] || equal(the_carrier(skc9),empty_set)+ -> SkP0(u,skc10)* v2_membered(skf20(skc10,v))*. % 131.83/132.08 1615[0:Res:618.0,676.1] || in(u,skc10) -> equal(subset_complement(the_carrier(skc9),u),skf13(u))**. % 131.83/132.08 1617[2:Rew:1615.1,1198.1] || in(u,skc10) equal(v,skf13(u)) -> in(ordered_pair(u,v),skf17(skc9,skc10))*. % 131.83/132.08 1803[0:SpL:1615.1,90.0] || in(u,skc10) equal(v,skf13(u)) -> SkP1(v,skc9,u)*. % 131.83/132.08 1964[0:Res:723.2,109.3] relation(u) function(u) relation(u) || in(v,relation_dom(u))* in(v,relation_dom(u))* -> equal(skf21(u,v),apply(u,v)). % 131.83/132.08 1982[0:Obv:1964.3] function(u) relation(u) || in(v,relation_dom(u))* -> equal(skf21(u,v),apply(u,v)). % 131.83/132.08 2020[2:Res:1617.2,100.2] relation(skf17(skc9,skc10)) || in(u,skc10)* equal(v,skf13(u))* equal(w,relation_dom(skf17(skc9,skc10)))* -> in(u,w)*. % 131.83/132.08 2031[2:AED:2020.2] relation(skf17(skc9,skc10)) || in(u,skc10)* equal(v,relation_dom(skf17(skc9,skc10)))* -> in(u,v)*. % 131.83/132.08 2032[2:SSi:2031.0,1196.0,26.0,1.0] || in(u,skc10)* equal(v,relation_dom(skf17(skc9,skc10)))*+ -> in(u,v)*. % 131.83/132.08 2387[4:Spt:1523.1] || -> SkP0(u,skc10)*. % 131.83/132.08 2554[0:Res:44.0,878.3] one_sorted_str(skc9) || SkP0(skc9,skc10) in(u,skc10)* equal(v,relation_dom(skf17(skc9,skc10)))* -> in(u,v)*. % 131.83/132.08 2879[0:Res:44.0,810.2] one_sorted_str(skc9) || SkP0(skc9,skc10) -> equal(u,relation_dom(skf17(skc9,skc10))) in(skf23(skf17(skc9,skc10),u),u)* in(skf23(skf17(skc9,skc10),u),skc10)*. % 131.83/132.08 2940[0:EqR:987.2] one_sorted_str(u) || in(v,relation_dom(skf17(u,w)))* SkP0(u,w) element(v,powerset(the_carrier(u))) element(w,powerset(powerset(the_carrier(u)))) -> equal(apply(skf17(u,w),v),subset_complement(the_carrier(u),v)). % 131.83/132.08 2943[0:MRR:2940.3,850.4] one_sorted_str(u) || in(v,relation_dom(skf17(u,w)))* SkP0(u,w) element(w,powerset(powerset(the_carrier(u)))) -> equal(apply(skf17(u,w),v),subset_complement(the_carrier(u),v)). % 131.83/132.08 2946[0:Rew:2943.4,850.5] one_sorted_str(u) || SkP0(u,v) element(v,powerset(powerset(the_carrier(u))))+ in(w,relation_dom(skf17(u,v)))* -> element(w,powerset(the_carrier(u))) equal(x,subset_complement(the_carrier(u),w))*. % 131.83/132.08 2958[0:Res:44.0,2946.2] one_sorted_str(skc9) || SkP0(skc9,skc10) in(u,relation_dom(skf17(skc9,skc10)))* -> element(u,powerset(the_carrier(skc9))) equal(v,subset_complement(the_carrier(skc9),u))*. % 131.83/132.08 2968[0:SSi:2958.0,1.0] || SkP0(skc9,skc10) in(u,relation_dom(skf17(skc9,skc10)))* -> element(u,powerset(the_carrier(skc9))) equal(v,subset_complement(the_carrier(skc9),u))*. % 131.83/132.08 3181[2:EqR:2032.1] || in(u,skc10) -> in(u,relation_dom(skf17(skc9,skc10)))*. % 131.83/132.08 3496[5:Spt:1240.0] || -> equal(relation_dom(skf17(skc9,skc10)),empty_set)**. % 131.83/132.08 3497[5:Rew:3496.0,3181.1] || in(u,skc10)* -> in(u,empty_set). % 131.83/132.08 3539[5:MRR:3497.1,756.0] || in(u,skc10)* -> . % 131.83/132.08 3616[5:Res:734.2,3539.0] empty(u) || -> equal(skc10,empty_set)**. % 131.83/132.08 3632[5:MRR:3616.1,250.0] empty(u) || -> . % 131.83/132.08 3633[5:UnC:3632.0,11.0] || -> . % 131.83/132.08 3650[5:Spt:3633.0,1240.0,3496.0] || equal(relation_dom(skf17(skc9,skc10)),empty_set)** -> . % 131.83/132.08 3651[5:Spt:3633.0,1240.1] || -> in(skf26(relation_dom(skf17(skc9,skc10)),empty_set),skc10)*. % 131.83/132.08 7147[2:Fac:1210.1,1210.2] || -> equal(relation_dom(skf17(skc9,skc10)),skc10) in(skf23(skf17(skc9,skc10),skc10),skc10)*. % 131.83/132.08 7176[6:Spt:7147.0] || -> equal(relation_dom(skf17(skc9,skc10)),skc10)**. % 131.83/132.08 8181[6:SpL:7176.0,191.2] function(skf17(skc9,skc10)) relation(skf17(skc9,skc10)) || equal(skc10,skc10)* -> . % 131.83/132.08 8193[6:Obv:8181.2] function(skf17(skc9,skc10)) relation(skf17(skc9,skc10)) || -> . % 131.83/132.08 8194[6:SSi:8193.1,8193.0,1196.0,26.0,1.0,1196.0,26.0,1.0] || -> . % 131.83/132.08 8205[6:Spt:8194.0,7147.0,7176.0] || equal(relation_dom(skf17(skc9,skc10)),skc10)** -> . % 131.83/132.08 8206[6:Spt:8194.0,7147.1] || -> in(skf23(skf17(skc9,skc10),skc10),skc10)*. % 131.83/132.08 8212[6:Res:8206.0,879.2] one_sorted_str(skc9) || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 131.83/132.08 8220[6:SSi:8212.0,1.0] || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 131.83/132.08 8221[6:MRR:8220.0,8220.1,8220.2,2387.0,44.0,8206.0] || -> . % 131.83/132.08 8222[4:Spt:8221.0,1523.0,1523.2] || equal(the_carrier(skc9),empty_set) -> v5_membered(skf20(skc10,u))*. % 131.83/132.08 8383[5:Spt:1543.1] || -> SkP0(u,skc10)*. % 131.83/132.08 8384[6:Spt:7147.0] || -> equal(relation_dom(skf17(skc9,skc10)),skc10)**. % 131.83/132.08 8609[6:SpL:8384.0,191.2] function(skf17(skc9,skc10)) relation(skf17(skc9,skc10)) || equal(skc10,skc10)* -> . % 131.83/132.08 8626[6:Obv:8609.2] function(skf17(skc9,skc10)) relation(skf17(skc9,skc10)) || -> . % 131.83/132.08 8627[6:SSi:8626.1,8626.0,1196.0,26.0,1.0,1196.0,26.0,1.0] || -> . % 131.83/132.08 8638[6:Spt:8627.0,7147.0,8384.0] || equal(relation_dom(skf17(skc9,skc10)),skc10)** -> . % 131.83/132.08 8639[6:Spt:8627.0,7147.1] || -> in(skf23(skf17(skc9,skc10),skc10),skc10)*. % 131.83/132.08 8645[6:Res:8639.0,879.2] one_sorted_str(skc9) || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 131.83/132.08 8653[6:SSi:8645.0,1.0] || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 131.83/132.08 8654[6:MRR:8653.0,8653.1,8653.2,8383.0,44.0,8639.0] || -> . % 131.83/132.08 8655[5:Spt:8654.0,1543.0,1543.2] || equal(the_carrier(skc9),empty_set) -> v4_membered(skf20(skc10,u))*. % 131.83/132.08 8806[6:Spt:1562.1] || -> SkP0(u,skc10)*. % 131.83/132.08 8807[7:Spt:7147.0] || -> equal(relation_dom(skf17(skc9,skc10)),skc10)**. % 131.83/132.08 9032[7:SpL:8807.0,191.2] function(skf17(skc9,skc10)) relation(skf17(skc9,skc10)) || equal(skc10,skc10)* -> . % 131.83/132.08 9049[7:Obv:9032.2] function(skf17(skc9,skc10)) relation(skf17(skc9,skc10)) || -> . % 131.83/132.08 9050[7:SSi:9049.1,9049.0,1196.0,26.0,1.0,1196.0,26.0,1.0] || -> . % 131.83/132.08 9061[7:Spt:9050.0,7147.0,8807.0] || equal(relation_dom(skf17(skc9,skc10)),skc10)** -> . % 131.83/132.08 9062[7:Spt:9050.0,7147.1] || -> in(skf23(skf17(skc9,skc10),skc10),skc10)*. % 131.83/132.08 9068[7:Res:9062.0,879.2] one_sorted_str(skc9) || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 131.83/132.08 9076[7:SSi:9068.0,1.0] || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 131.83/132.08 9077[7:MRR:9076.0,9076.1,9076.2,8806.0,44.0,9062.0] || -> . % 131.83/132.08 9078[6:Spt:9077.0,1562.0,1562.2] || equal(the_carrier(skc9),empty_set) -> v3_membered(skf20(skc10,u))*. % 131.83/132.08 9229[7:Spt:1582.1] || -> SkP0(u,skc10)*. % 131.83/132.08 9230[8:Spt:7147.0] || -> equal(relation_dom(skf17(skc9,skc10)),skc10)**. % 131.83/132.08 9455[8:SpL:9230.0,191.2] function(skf17(skc9,skc10)) relation(skf17(skc9,skc10)) || equal(skc10,skc10)* -> . % 131.83/132.08 9472[8:Obv:9455.2] function(skf17(skc9,skc10)) relation(skf17(skc9,skc10)) || -> . % 131.83/132.08 9473[8:SSi:9472.1,9472.0,1196.0,26.0,1.0,1196.0,26.0,1.0] || -> . % 131.83/132.08 9484[8:Spt:9473.0,7147.0,9230.0] || equal(relation_dom(skf17(skc9,skc10)),skc10)** -> . % 131.83/132.08 9485[8:Spt:9473.0,7147.1] || -> in(skf23(skf17(skc9,skc10),skc10),skc10)*. % 131.83/132.08 9491[8:Res:9485.0,879.2] one_sorted_str(skc9) || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 131.83/132.08 9499[8:SSi:9491.0,1.0] || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 131.83/132.08 9500[8:MRR:9499.0,9499.1,9499.2,9229.0,44.0,9485.0] || -> . % 131.83/132.08 9501[7:Spt:9500.0,1582.0,1582.2] || equal(the_carrier(skc9),empty_set) -> v2_membered(skf20(skc10,u))*. % 131.83/132.08 9662[8:Spt:7147.0] || -> equal(relation_dom(skf17(skc9,skc10)),skc10)**. % 131.83/132.08 9888[8:SpL:9662.0,191.2] function(skf17(skc9,skc10)) relation(skf17(skc9,skc10)) || equal(skc10,skc10)* -> . % 131.83/132.08 9904[8:Obv:9888.2] function(skf17(skc9,skc10)) relation(skf17(skc9,skc10)) || -> . % 131.83/132.08 9905[8:SSi:9904.1,9904.0,1196.0,26.0,1.0,1196.0,26.0,1.0] || -> . % 131.83/132.08 9916[8:Spt:9905.0,7147.0,9662.0] || equal(relation_dom(skf17(skc9,skc10)),skc10)** -> . % 131.83/132.08 9917[8:Spt:9905.0,7147.1] || -> in(skf23(skf17(skc9,skc10),skc10),skc10)*. % 131.83/132.08 9923[8:Res:9917.0,879.2] one_sorted_str(skc9) || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 131.83/132.08 9931[8:SSi:9923.0,1.0] || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 131.83/132.08 9932[8:MRR:9931.0,9931.1,9931.2,1195.0,44.0,9917.0] || -> . % 131.83/132.08 9933[1:Spt:9932.0,97.3] || -> in(skf14(u),skc10)*. % 131.83/132.08 9966[0:SSi:2554.0,1.0] || SkP0(skc9,skc10) in(u,skc10)* equal(v,relation_dom(skf17(skc9,skc10)))* -> in(u,v)*. % 131.83/132.08 9969[0:SSi:2879.0,1.0] || SkP0(skc9,skc10) -> equal(u,relation_dom(skf17(skc9,skc10))) in(skf23(skf17(skc9,skc10),u),u)* in(skf23(skf17(skc9,skc10),u),skc10)*. % 131.83/132.08 10021[2:Spt:677.2] || -> equal(u,v)*. % 131.83/132.08 10022[2:UnC:10021.0,1062.0] || -> . % 131.83/132.08 10023[2:Spt:10022.0,677.0,677.1] || in(u,skc10) -> element(u,powerset(the_carrier(skc9)))*. % 131.83/132.08 10061[2:Res:10023.1,88.1] v5_membered(the_carrier(skc9)) || in(u,skc10)* -> v5_membered(u). % 131.83/132.08 10062[2:Res:10023.1,87.1] v5_membered(the_carrier(skc9)) || in(u,skc10)* -> v4_membered(u). % 131.83/132.08 10064[2:Res:10023.1,86.1] v5_membered(the_carrier(skc9)) || in(u,skc10)* -> v3_membered(u). % 131.83/132.08 10067[2:Res:10023.1,85.1] v5_membered(the_carrier(skc9)) || in(u,skc10)* -> v2_membered(u). % 131.83/132.08 10071[2:Res:10023.1,84.1] v5_membered(the_carrier(skc9)) || in(u,skc10)* -> v1_membered(u). % 131.83/132.08 10077[2:Res:10023.1,117.0] || in(skf20(u,skc9),skc10)* -> SkP0(skc9,u). % 131.83/132.08 10102[0:Res:723.2,182.1] relation(skf17(skc9,skc10)) || in(u,relation_dom(skf17(skc9,skc10)))* SkP0(skc9,skc10) -> in(u,skc10). % 131.83/132.08 10109[0:SSi:10102.0,26.0,1.0] || in(u,relation_dom(skf17(skc9,skc10)))* SkP0(skc9,skc10) -> in(u,skc10). % 131.83/132.08 10153[2:Res:53.1,10077.0] || -> SkP0(u,skc10)* SkP0(skc9,skc10)*. % 131.83/132.08 10154[2:Con:10153.0] || -> SkP0(skc9,skc10)*. % 131.83/132.08 10155[2:MRR:178.0,10154.0] || -> function(skf17(skc9,skc10))*. % 131.83/132.08 10157[2:MRR:9966.0,10154.0] || in(u,skc10)* equal(v,relation_dom(skf17(skc9,skc10)))*+ -> in(u,v)*. % 131.83/132.08 10158[2:MRR:2968.0,10154.0] || in(u,relation_dom(skf17(skc9,skc10)))*+ -> element(u,powerset(the_carrier(skc9))) equal(v,subset_complement(the_carrier(skc9),u))*. % 131.83/132.08 10161[2:MRR:185.1,10154.0] || element(u,powerset(the_carrier(skc9))) in(ordered_pair(u,v),skf17(skc9,skc10))* -> equal(v,subset_complement(the_carrier(skc9),u)). % 131.83/132.08 10163[2:MRR:9969.0,10154.0] || -> equal(u,relation_dom(skf17(skc9,skc10))) in(skf23(skf17(skc9,skc10),u),u)* in(skf23(skf17(skc9,skc10),u),skc10)*. % 131.83/132.08 10164[2:MRR:10109.1,10154.0] || in(u,relation_dom(skf17(skc9,skc10)))* -> in(u,skc10). % 131.83/132.08 10217[2:SoR:10061.0,37.1] empty(the_carrier(skc9)) || in(u,skc10)* -> v5_membered(u). % 131.83/132.08 10218[2:SoR:10062.0,37.1] empty(the_carrier(skc9)) || in(u,skc10)* -> v4_membered(u). % 131.83/132.08 10246[2:SoR:10064.0,37.1] empty(the_carrier(skc9)) || in(u,skc10)* -> v3_membered(u). % 131.83/132.08 10252[2:Res:723.2,10161.1] relation(skf17(skc9,skc10)) || in(u,relation_dom(skf17(skc9,skc10)))* element(u,powerset(the_carrier(skc9))) -> equal(skf21(skf17(skc9,skc10),u),subset_complement(the_carrier(skc9),u)). % 131.83/132.08 10261[2:SSi:10252.0,10155.0,26.0,1.0] || in(u,relation_dom(skf17(skc9,skc10)))* element(u,powerset(the_carrier(skc9))) -> equal(skf21(skf17(skc9,skc10),u),subset_complement(the_carrier(skc9),u)). % 131.83/132.08 10262[2:MRR:10261.1,10158.1] || in(u,relation_dom(skf17(skc9,skc10)))* -> equal(skf21(skf17(skc9,skc10),u),subset_complement(the_carrier(skc9),u)). % 131.83/132.08 10268[2:SoR:10067.0,37.1] empty(the_carrier(skc9)) || in(u,skc10)* -> v2_membered(u). % 131.83/132.08 10275[2:Res:757.1,10164.0] || -> equal(relation_dom(skf17(skc9,skc10)),empty_set) in(skf26(relation_dom(skf17(skc9,skc10)),empty_set),skc10)*. % 131.83/132.08 10359[2:SoR:10071.0,37.1] empty(the_carrier(skc9)) || in(u,skc10)* -> v1_membered(u). % 131.83/132.08 10364[2:EqR:10157.1] || in(u,skc10) -> in(u,relation_dom(skf17(skc9,skc10)))*. % 131.83/132.08 10371[2:SoR:10217.0,1013.1] || in(u,skc10)* equal(the_carrier(skc9),empty_set) -> v5_membered(u). % 131.83/132.08 10372[2:SoR:10218.0,1013.1] || in(u,skc10)* equal(the_carrier(skc9),empty_set) -> v4_membered(u). % 131.83/132.08 10382[2:SoR:10246.0,1013.1] || in(u,skc10)* equal(the_carrier(skc9),empty_set) -> v3_membered(u). % 131.83/132.08 10383[2:SoR:10268.0,1013.1] || in(u,skc10)* equal(the_carrier(skc9),empty_set) -> v2_membered(u). % 131.83/132.08 10388[2:SoR:10359.0,1013.1] || in(u,skc10)* equal(the_carrier(skc9),empty_set) -> v1_membered(u). % 131.83/132.08 10401[2:Res:10364.1,820.0] || in(u,skc10)* equal(relation_dom(skf17(skc9,skc10)),empty_set)**+ -> . % 131.83/132.08 10408[2:Res:10364.1,1982.2] function(skf17(skc9,skc10)) relation(skf17(skc9,skc10)) || in(u,skc10) -> equal(skf21(skf17(skc9,skc10),u),apply(skf17(skc9,skc10),u))**. % 131.83/132.08 10414[2:SSi:10408.1,10408.0,10155.0,26.0,1.0,10155.0,26.0,1.0] || in(u,skc10) -> equal(skf21(skf17(skc9,skc10),u),apply(skf17(skc9,skc10),u))**. % 131.83/132.08 10560[2:Res:10364.1,10262.0] || in(u,skc10) -> equal(skf21(skf17(skc9,skc10),u),subset_complement(the_carrier(skc9),u))**. % 131.83/132.08 10563[2:Rew:1615.1,10560.1] || in(u,skc10) -> equal(skf21(skf17(skc9,skc10),u),skf13(u))**. % 131.83/132.08 10564[2:Rew:10414.1,10563.1] || in(u,skc10) -> equal(apply(skf17(skc9,skc10),u),skf13(u))**. % 131.83/132.08 10633[2:Res:53.1,10371.0] || equal(the_carrier(skc9),empty_set)+ -> SkP0(u,skc10)* v5_membered(skf20(skc10,v))*. % 131.83/132.08 10724[2:Res:53.1,10372.0] || equal(the_carrier(skc9),empty_set)+ -> SkP0(u,skc10)* v4_membered(skf20(skc10,v))*. % 131.83/132.08 10818[2:Res:53.1,10382.0] || equal(the_carrier(skc9),empty_set)+ -> SkP0(u,skc10)* v3_membered(skf20(skc10,v))*. % 131.83/132.08 10913[2:Res:53.1,10383.0] || equal(the_carrier(skc9),empty_set)+ -> SkP0(u,skc10)* v2_membered(skf20(skc10,v))*. % 131.83/132.08 11010[2:Res:53.1,10388.0] || equal(the_carrier(skc9),empty_set)+ -> SkP0(u,skc10)* v1_membered(skf20(skc10,v))*. % 131.83/132.08 11388[3:Spt:10633.1] || -> SkP0(u,skc10)*. % 131.83/132.08 11419[2:SpL:10564.1,105.3] function(skf17(skc9,skc10)) relation(skf17(skc9,skc10)) || in(skf14(skf17(skc9,skc10)),skc10) equal(relation_dom(skf17(skc9,skc10)),skc10) SkP1(skf13(skf14(skf17(skc9,skc10))),skc9,skf14(skf17(skc9,skc10)))* -> . % 131.83/132.08 11420[2:SSi:11419.1,11419.0,10155.0,26.0,1.0,10155.0,26.0,1.0] || in(skf14(skf17(skc9,skc10)),skc10) equal(relation_dom(skf17(skc9,skc10)),skc10) SkP1(skf13(skf14(skf17(skc9,skc10))),skc9,skf14(skf17(skc9,skc10)))* -> . % 131.83/132.08 11421[2:MRR:11420.0,9933.0] || equal(relation_dom(skf17(skc9,skc10)),skc10) SkP1(skf13(skf14(skf17(skc9,skc10))),skc9,skf14(skf17(skc9,skc10)))* -> . % 131.83/132.08 11467[4:Spt:10275.0] || -> equal(relation_dom(skf17(skc9,skc10)),empty_set)**. % 131.83/132.08 11474[4:Rew:11467.0,10401.1] || in(u,skc10)* equal(empty_set,empty_set) -> . % 131.83/132.08 11725[4:Obv:11474.1] || in(u,skc10)* -> . % 131.83/132.08 11726[4:UnC:11725.0,9933.0] || -> . % 131.83/132.08 11948[4:Spt:11726.0,10275.0,11467.0] || equal(relation_dom(skf17(skc9,skc10)),empty_set)** -> . % 131.83/132.08 11949[4:Spt:11726.0,10275.1] || -> in(skf26(relation_dom(skf17(skc9,skc10)),empty_set),skc10)*. % 131.83/132.08 12543[2:Fac:10163.1,10163.2] || -> equal(relation_dom(skf17(skc9,skc10)),skc10) in(skf23(skf17(skc9,skc10),skc10),skc10)*. % 131.83/132.08 13474[5:Spt:12543.0] || -> equal(relation_dom(skf17(skc9,skc10)),skc10)**. % 131.83/132.08 13873[5:Rew:13474.0,11421.0] || equal(skc10,skc10) SkP1(skf13(skf14(skf17(skc9,skc10))),skc9,skf14(skf17(skc9,skc10)))* -> . % 131.83/132.08 14109[5:Obv:13873.0] || SkP1(skf13(skf14(skf17(skc9,skc10))),skc9,skf14(skf17(skc9,skc10)))* -> . % 131.83/132.08 16561[5:Res:1803.2,14109.0] || in(skf14(skf17(skc9,skc10)),skc10)* equal(skf13(skf14(skf17(skc9,skc10))),skf13(skf14(skf17(skc9,skc10)))) -> . % 131.83/132.08 16568[5:Obv:16561.1] || in(skf14(skf17(skc9,skc10)),skc10)* -> . % 131.83/132.08 16569[5:MRR:16568.0,9933.0] || -> . % 131.83/132.08 16570[5:Spt:16569.0,12543.0,13474.0] || equal(relation_dom(skf17(skc9,skc10)),skc10)** -> . % 131.83/132.08 16571[5:Spt:16569.0,12543.1] || -> in(skf23(skf17(skc9,skc10),skc10),skc10)*. % 131.83/132.08 16577[5:Res:16571.0,879.2] one_sorted_str(skc9) || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 131.83/132.08 16587[5:SSi:16577.0,1.0] || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 131.83/132.08 16588[5:MRR:16587.0,16587.1,16587.2,11388.0,44.0,16571.0] || -> . % 131.83/132.08 16589[3:Spt:16588.0,10633.0,10633.2] || equal(the_carrier(skc9),empty_set) -> v5_membered(skf20(skc10,u))*. % 131.83/132.08 16746[4:Spt:10724.1] || -> SkP0(u,skc10)*. % 131.83/132.08 16750[5:Spt:12543.0] || -> equal(relation_dom(skf17(skc9,skc10)),skc10)**. % 131.83/132.08 17278[5:Rew:16750.0,11421.0] || equal(skc10,skc10) SkP1(skf13(skf14(skf17(skc9,skc10))),skc9,skf14(skf17(skc9,skc10)))* -> . % 131.83/132.08 17294[5:Obv:17278.0] || SkP1(skf13(skf14(skf17(skc9,skc10))),skc9,skf14(skf17(skc9,skc10)))* -> . % 131.83/132.08 20048[5:Res:1803.2,17294.0] || in(skf14(skf17(skc9,skc10)),skc10)* equal(skf13(skf14(skf17(skc9,skc10))),skf13(skf14(skf17(skc9,skc10)))) -> . % 131.83/132.08 20055[5:Obv:20048.1] || in(skf14(skf17(skc9,skc10)),skc10)* -> . % 131.83/132.08 20056[5:MRR:20055.0,9933.0] || -> . % 131.83/132.08 20057[5:Spt:20056.0,12543.0,16750.0] || equal(relation_dom(skf17(skc9,skc10)),skc10)** -> . % 131.83/132.08 20058[5:Spt:20056.0,12543.1] || -> in(skf23(skf17(skc9,skc10),skc10),skc10)*. % 131.83/132.08 20067[5:Res:20058.0,879.2] one_sorted_str(skc9) || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 131.83/132.08 20077[5:SSi:20067.0,1.0] || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 133.49/133.74 20078[5:MRR:20077.0,20077.1,20077.2,16746.0,44.0,20058.0] || -> . % 133.49/133.74 20079[4:Spt:20078.0,10724.0,10724.2] || equal(the_carrier(skc9),empty_set) -> v4_membered(skf20(skc10,u))*. % 133.49/133.74 20246[5:Spt:10818.1] || -> SkP0(u,skc10)*. % 133.49/133.74 20263[6:Spt:12543.0] || -> equal(relation_dom(skf17(skc9,skc10)),skc10)**. % 133.49/133.74 20792[6:Rew:20263.0,11421.0] || equal(skc10,skc10) SkP1(skf13(skf14(skf17(skc9,skc10))),skc9,skf14(skf17(skc9,skc10)))* -> . % 133.49/133.74 20810[6:Obv:20792.0] || SkP1(skf13(skf14(skf17(skc9,skc10))),skc9,skf14(skf17(skc9,skc10)))* -> . % 133.49/133.74 23701[6:Res:1803.2,20810.0] || in(skf14(skf17(skc9,skc10)),skc10)* equal(skf13(skf14(skf17(skc9,skc10))),skf13(skf14(skf17(skc9,skc10)))) -> . % 133.49/133.74 23708[6:Obv:23701.1] || in(skf14(skf17(skc9,skc10)),skc10)* -> . % 133.49/133.74 23709[6:MRR:23708.0,9933.0] || -> . % 133.49/133.74 23710[6:Spt:23709.0,12543.0,20263.0] || equal(relation_dom(skf17(skc9,skc10)),skc10)** -> . % 133.49/133.74 23711[6:Spt:23709.0,12543.1] || -> in(skf23(skf17(skc9,skc10),skc10),skc10)*. % 133.49/133.74 23717[6:Res:23711.0,879.2] one_sorted_str(skc9) || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 133.49/133.74 23727[6:SSi:23717.0,1.0] || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 133.49/133.74 23728[6:MRR:23727.0,23727.1,23727.2,20246.0,44.0,23711.0] || -> . % 133.49/133.74 23729[5:Spt:23728.0,10818.0,10818.2] || equal(the_carrier(skc9),empty_set) -> v3_membered(skf20(skc10,u))*. % 133.49/133.74 23893[6:Spt:10913.1] || -> SkP0(u,skc10)*. % 133.49/133.74 23913[7:Spt:12543.0] || -> equal(relation_dom(skf17(skc9,skc10)),skc10)**. % 133.49/133.74 24445[7:Rew:23913.0,11421.0] || equal(skc10,skc10) SkP1(skf13(skf14(skf17(skc9,skc10))),skc9,skf14(skf17(skc9,skc10)))* -> . % 133.49/133.74 24460[7:Obv:24445.0] || SkP1(skf13(skf14(skf17(skc9,skc10))),skc9,skf14(skf17(skc9,skc10)))* -> . % 133.49/133.74 28116[7:Res:1803.2,24460.0] || in(skf14(skf17(skc9,skc10)),skc10)* equal(skf13(skf14(skf17(skc9,skc10))),skf13(skf14(skf17(skc9,skc10)))) -> . % 133.49/133.74 28123[7:Obv:28116.1] || in(skf14(skf17(skc9,skc10)),skc10)* -> . % 133.49/133.74 28124[7:MRR:28123.0,9933.0] || -> . % 133.49/133.74 28125[7:Spt:28124.0,12543.0,23913.0] || equal(relation_dom(skf17(skc9,skc10)),skc10)** -> . % 133.49/133.74 28126[7:Spt:28124.0,12543.1] || -> in(skf23(skf17(skc9,skc10),skc10),skc10)*. % 133.49/133.74 28132[7:Res:28126.0,879.2] one_sorted_str(skc9) || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 133.49/133.74 28142[7:SSi:28132.0,1.0] || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 133.49/133.74 28143[7:MRR:28142.0,28142.1,28142.2,23893.0,44.0,28126.0] || -> . % 133.49/133.74 28144[6:Spt:28143.0,10913.0,10913.2] || equal(the_carrier(skc9),empty_set) -> v2_membered(skf20(skc10,u))*. % 133.49/133.74 28314[7:Spt:11010.1] || -> SkP0(u,skc10)*. % 133.49/133.74 28331[8:Spt:12543.0] || -> equal(relation_dom(skf17(skc9,skc10)),skc10)**. % 133.49/133.74 28863[8:Rew:28331.0,11421.0] || equal(skc10,skc10) SkP1(skf13(skf14(skf17(skc9,skc10))),skc9,skf14(skf17(skc9,skc10)))* -> . % 133.49/133.74 28879[8:Obv:28863.0] || SkP1(skf13(skf14(skf17(skc9,skc10))),skc9,skf14(skf17(skc9,skc10)))* -> . % 133.49/133.74 34627[8:Res:1803.2,28879.0] || in(skf14(skf17(skc9,skc10)),skc10)* equal(skf13(skf14(skf17(skc9,skc10))),skf13(skf14(skf17(skc9,skc10)))) -> . % 133.49/133.74 34634[8:Obv:34627.1] || in(skf14(skf17(skc9,skc10)),skc10)* -> . % 133.49/133.74 34635[8:MRR:34634.0,9933.0] || -> . % 133.49/133.74 34636[8:Spt:34635.0,12543.0,28331.0] || equal(relation_dom(skf17(skc9,skc10)),skc10)** -> . % 133.49/133.74 34637[8:Spt:34635.0,12543.1] || -> in(skf23(skf17(skc9,skc10),skc10),skc10)*. % 133.49/133.74 34643[8:Res:34637.0,879.2] one_sorted_str(skc9) || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 133.49/133.74 34653[8:SSi:34643.0,1.0] || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 133.49/133.74 34654[8:MRR:34653.0,34653.1,34653.2,28314.0,44.0,34637.0] || -> . % 133.49/133.74 34655[7:Spt:34654.0,11010.0,11010.2] || equal(the_carrier(skc9),empty_set) -> v1_membered(skf20(skc10,u))*. % 133.49/133.74 34822[8:Spt:12543.0] || -> equal(relation_dom(skf17(skc9,skc10)),skc10)**. % 133.49/133.74 35355[8:Rew:34822.0,11421.0] || equal(skc10,skc10) SkP1(skf13(skf14(skf17(skc9,skc10))),skc9,skf14(skf17(skc9,skc10)))* -> . % 133.49/133.74 35371[8:Obv:35355.0] || SkP1(skf13(skf14(skf17(skc9,skc10))),skc9,skf14(skf17(skc9,skc10)))* -> . % 133.49/133.74 44271[8:Res:1803.2,35371.0] || in(skf14(skf17(skc9,skc10)),skc10)* equal(skf13(skf14(skf17(skc9,skc10))),skf13(skf14(skf17(skc9,skc10)))) -> . % 133.49/133.74 44278[8:Obv:44271.1] || in(skf14(skf17(skc9,skc10)),skc10)* -> . % 133.49/133.74 44279[8:MRR:44278.0,9933.0] || -> . % 133.49/133.74 44280[8:Spt:44279.0,12543.0,34822.0] || equal(relation_dom(skf17(skc9,skc10)),skc10)** -> . % 133.49/133.74 44281[8:Spt:44279.0,12543.1] || -> in(skf23(skf17(skc9,skc10),skc10),skc10)*. % 133.49/133.74 44297[8:Res:44281.0,879.2] one_sorted_str(skc9) || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 133.49/133.74 44309[8:SSi:44297.0,1.0] || SkP0(skc9,skc10) element(skc10,powerset(powerset(the_carrier(skc9)))) in(skf23(skf17(skc9,skc10),skc10),skc10)* -> . % 133.49/133.74 44310[8:MRR:44309.0,44309.1,44309.2,10154.0,44.0,44281.0] || -> . % 133.49/133.74 % SZS output end Refutation % 133.49/133.74 Formulae used in the proof : s2_funct_1__e4_7_2__tops_2 rc1_membered fc12_relat_1 fc4_relat_1 rc2_subset_1 s1_funct_1__e4_7_2__tops_2__1 rc3_relat_1 existence_m1_subset_1 cc15_membered cc1_funct_1 cc1_relat_1 fc3_subset_1 fc7_relat_1 t6_boole t7_boole t2_subset cc16_membered cc17_membered cc18_membered cc19_membered cc20_membered t2_tarski antisymmetry_r2_hidden d4_relat_1 d4_funct_1 % 133.49/133.74 %------------------------------------------------------------------------------