%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SET861-2 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n028.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 05:29:24 EDT 2022 % Result : Unsatisfiable 1.95s 2.16s % Output : Refutation 1.99s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SET861-2 : TPTP v8.1.0. Released v3.2.0. % 0.06/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n028.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 : Sat Jul 9 21:40:56 EDT 2022 % 0.13/0.34 % CPUTime : % 1.95/2.16 % 1.95/2.16 SPASS V 3.9 % 1.95/2.16 SPASS beiseite: Proof found. % 1.95/2.16 % SZS status Theorem % 1.95/2.16 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.95/2.16 SPASS derived 2183 clauses, backtracked 45 clauses, performed 4 splits and kept 1827 clauses. % 1.95/2.16 SPASS allocated 68797 KBytes. % 1.95/2.16 SPASS spent 0:00:01.81 on the problem. % 1.95/2.16 0:00:00.03 for the input. % 1.95/2.16 0:00:00.00 for the FLOTTER CNF translation. % 1.95/2.16 0:00:00.15 for inferences. % 1.95/2.16 0:00:00.05 for the backtracking. % 1.95/2.16 0:00:01.53 for the reduction. % 1.95/2.16 % 1.95/2.16 % 1.95/2.16 Here is a proof with depth 26, length 96 : % 1.95/2.16 % SZS output start Refutation % 1.95/2.16 1[0:Inp] || c_lessequals(u,v,tc_set(w))*+ c_lessequals(v,u,tc_set(w))* -> equal(u,v). % 1.95/2.16 2[0:Inp] || c_in(u,v,w)* c_lessequals(v,x,tc_set(w))*+ -> c_in(u,x,w)*. % 1.95/2.16 3[0:Inp] || -> c_lessequals(u,v,tc_set(w)) c_in(c_Main_OsubsetI__1(u,v,w),u,w)*. % 1.95/2.16 4[0:Inp] || c_in(c_Main_OsubsetI__1(u,v,w),v,w)* -> c_lessequals(u,v,tc_set(w)). % 1.95/2.16 5[0:Inp] || c_in(u,v,tc_set(w)) c_in(x,c_Zorn_Ochain(v,w),tc_set(tc_set(w)))+ -> c_in(c_Zorn_Ochain__extend__1(x,u,w),x,tc_set(w))* c_in(c_union(c_insert(u,c_emptyset,tc_set(w)),x,tc_set(w)),c_Zorn_Ochain(v,w),tc_set(tc_set(w)))*. % 1.95/2.16 6[0:Inp] || c_in(u,v,tc_set(w)) c_in(x,c_Zorn_Ochain(v,w),tc_set(tc_set(w)))+ c_lessequals(c_Zorn_Ochain__extend__1(x,u,w),u,tc_set(w))* -> c_in(c_union(c_insert(u,c_emptyset,tc_set(w)),x,tc_set(w)),c_Zorn_Ochain(v,w),tc_set(tc_set(w)))*. % 1.95/2.16 7[0:Inp] || -> c_in(c_Zorn_OHausdorff__1(u,v),c_Zorn_Omaxchain(u,v),tc_set(tc_set(v)))*. % 1.95/2.16 8[0:Inp] || -> c_lessequals(c_Zorn_Omaxchain(u,v),c_Zorn_Ochain(u,v),tc_set(tc_set(tc_set(v))))*. % 1.95/2.16 9[0:Inp] || c_in(u,v,w)* c_in(x,c_Zorn_Omaxchain(y,w),tc_set(tc_set(w))) c_in(c_union(c_insert(v,c_emptyset,tc_set(w)),x,tc_set(w)),c_Zorn_Ochain(y,w),tc_set(tc_set(w)))*+ -> c_in(u,z,w)* c_in(c_Zorn_Omaxchain__super__lemma__1(x,z,w),x,tc_set(w))*. % 1.95/2.16 10[0:Inp] || c_in(u,v,w)* c_in(x,c_Zorn_Omaxchain(y,w),tc_set(tc_set(w))) c_lessequals(c_Zorn_Omaxchain__super__lemma__1(x,z,w),z,tc_set(w))* c_in(c_union(c_insert(v,c_emptyset,tc_set(w)),x,tc_set(w)),c_Zorn_Ochain(y,w),tc_set(tc_set(w)))*+ -> c_in(u,z,w)*. % 1.95/2.16 11[0:Inp] || c_in(u,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))* -> c_in(v_x(u),v_S,tc_set(t_a)). % 1.95/2.16 12[0:Inp] || c_in(u,v_S,tc_set(t_a)) -> c_in(v_xa(u),v_S,tc_set(t_a))*. % 1.95/2.16 13[0:Inp] || c_in(u,v_S,tc_set(t_a)) -> c_lessequals(u,v_xa(u),tc_set(t_a))*. % 1.95/2.16 14[0:Inp] || equal(v_xa(u),u) c_in(u,v_S,tc_set(t_a))* -> . % 1.95/2.16 15[0:Inp] || c_in(u,v,tc_set(t_a)) c_in(v,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))*+ -> c_lessequals(u,v_x(v),tc_set(t_a))*. % 1.95/2.16 29[0:Res:8.0,2.1] || c_in(u,c_Zorn_Omaxchain(v,w),tc_set(tc_set(w)))* -> c_in(u,c_Zorn_Ochain(v,w),tc_set(tc_set(w))). % 1.95/2.16 30[0:Res:13.1,2.1] || c_in(u,v_S,tc_set(t_a))*+ c_in(v,u,t_a) -> c_in(v,v_xa(u),t_a)*. % 1.95/2.16 33[0:Res:12.1,30.0] || c_in(u,v_S,tc_set(t_a)) c_in(v,v_xa(u),t_a) -> c_in(v,v_xa(v_xa(u)),t_a)*. % 1.95/2.16 35[0:Res:7.0,29.0] || -> c_in(c_Zorn_OHausdorff__1(u,v),c_Zorn_Ochain(u,v),tc_set(tc_set(v)))*. % 1.95/2.16 37[0:Res:35.0,11.0] || -> c_in(v_x(c_Zorn_OHausdorff__1(v_S,t_a)),v_S,tc_set(t_a))*. % 1.95/2.16 38[0:Res:35.0,15.1] || c_in(u,c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a)) -> c_lessequals(u,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))*. % 1.95/2.16 39[0:Res:35.0,5.1] || c_in(u,v,tc_set(w)) -> c_in(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v,w),u,w),c_Zorn_OHausdorff__1(v,w),tc_set(w)) c_in(c_union(c_insert(u,c_emptyset,tc_set(w)),c_Zorn_OHausdorff__1(v,w),tc_set(w)),c_Zorn_Ochain(v,w),tc_set(tc_set(w)))*. % 1.95/2.16 41[0:Res:37.0,30.0] || c_in(u,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a) -> c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)*. % 1.95/2.16 44[0:Res:37.0,14.1] || equal(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)))** -> . % 1.95/2.16 45[0:Res:35.0,6.1] || c_in(u,v,tc_set(w)) c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v,w),u,w),u,tc_set(w))*+ -> c_in(c_union(c_insert(u,c_emptyset,tc_set(w)),c_Zorn_OHausdorff__1(v,w),tc_set(w)),c_Zorn_Ochain(v,w),tc_set(tc_set(w)))*. % 1.95/2.16 49[0:Res:38.1,2.1] || c_in(u,c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))*+ c_in(v,u,t_a)* -> c_in(v,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)*. % 1.95/2.16 51[0:Res:41.1,4.0] || c_in(c_Main_OsubsetI__1(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)* -> c_lessequals(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a)). % 1.95/2.16 52[0:Res:33.2,4.0] || c_in(u,v_S,tc_set(t_a)) c_in(c_Main_OsubsetI__1(v,v_xa(v_xa(u)),t_a),v_xa(u),t_a)* -> c_lessequals(v,v_xa(v_xa(u)),tc_set(t_a)). % 1.95/2.16 61[0:Res:3.1,51.0] || -> c_lessequals(v_x(c_Zorn_OHausdorff__1(v_S,t_a)),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a))* c_lessequals(v_x(c_Zorn_OHausdorff__1(v_S,t_a)),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a))*. % 1.95/2.16 62[0:Obv:61.0] || -> c_lessequals(v_x(c_Zorn_OHausdorff__1(v_S,t_a)),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a))*. % 1.95/2.16 68[0:Res:62.0,1.0] || c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))* -> equal(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a))). % 1.95/2.16 71[0:MRR:68.1,44.0] || c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))* -> . % 1.95/2.16 76[0:Res:41.1,52.1] || c_in(c_Main_OsubsetI__1(u,v_xa(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a)))),t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)* c_in(v_x(c_Zorn_OHausdorff__1(v_S,t_a)),v_S,tc_set(t_a)) -> c_lessequals(u,v_xa(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a)))),tc_set(t_a)). % 1.95/2.16 80[0:MRR:76.1,37.0] || c_in(c_Main_OsubsetI__1(u,v_xa(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a)))),t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)* -> c_lessequals(u,v_xa(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a)))),tc_set(t_a)). % 1.95/2.16 354[0:Res:39.2,10.3] || c_in(u,v,tc_set(w)) c_in(x,u,w)* c_in(c_Zorn_OHausdorff__1(v,w),c_Zorn_Omaxchain(v,w),tc_set(tc_set(w))) c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v,w),y,w),y,tc_set(w))* -> c_in(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v,w),u,w),c_Zorn_OHausdorff__1(v,w),tc_set(w))* c_in(x,y,w)*. % 1.95/2.16 355[0:Res:39.2,9.2] || c_in(u,v,tc_set(w)) c_in(x,u,w)* c_in(c_Zorn_OHausdorff__1(v,w),c_Zorn_Omaxchain(v,w),tc_set(tc_set(w))) -> c_in(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v,w),u,w),c_Zorn_OHausdorff__1(v,w),tc_set(w))* c_in(x,y,w)* c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v,w),y,w),c_Zorn_OHausdorff__1(v,w),tc_set(w))*. % 1.95/2.16 357[0:MRR:354.2,7.0] || c_in(u,v,tc_set(w)) c_in(x,u,w)* c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v,w),y,w),y,tc_set(w))*+ -> c_in(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v,w),u,w),c_Zorn_OHausdorff__1(v,w),tc_set(w))* c_in(x,y,w)*. % 1.95/2.16 358[0:MRR:355.2,7.0] || c_in(u,v,tc_set(w))+ c_in(x,u,w)* -> c_in(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v,w),u,w),c_Zorn_OHausdorff__1(v,w),tc_set(w))* c_in(x,y,w)* c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v,w),y,w),c_Zorn_OHausdorff__1(v,w),tc_set(w))*. % 1.95/2.16 719[0:Res:12.1,358.0] || c_in(u,v_S,tc_set(t_a))+ c_in(v,v_xa(u),t_a)* -> c_in(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(u),t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))* c_in(v,w,t_a)* c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),w,t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))*. % 1.95/2.16 1417[0:Res:37.0,719.0] || c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)*+ -> c_in(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))* c_in(u,v,t_a)* c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v,t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))*. % 1.95/2.16 1442[1:Spt:1417.0,1417.2,1417.3] || c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)*+ -> c_in(u,v,t_a)* c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v,t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))*. % 1.95/2.16 1443[1:Res:3.1,1442.0] || -> c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),u,tc_set(t_a)) c_in(c_Main_OsubsetI__1(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),u,t_a),v,t_a)* c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v,t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))*. % 1.95/2.16 1448[1:Res:1443.1,4.0] || -> c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),u,tc_set(t_a)) c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),u,t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))* c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),u,tc_set(t_a)). % 1.95/2.16 1499[1:Res:1443.1,80.0] || -> c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_xa(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a)))),tc_set(t_a)) c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))* c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_xa(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a)))),tc_set(t_a)). % 1.95/2.16 1516[1:Obv:1448.0] || -> c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),u,t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))* c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),u,tc_set(t_a)). % 1.95/2.16 1519[1:Obv:1499.0] || -> c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))* c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_xa(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a)))),tc_set(t_a)). % 1.95/2.16 1563[2:Spt:1519.0] || -> c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))*. % 1.95/2.16 1564[2:Res:1563.0,49.0] || c_in(u,c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a),t_a)* -> c_in(u,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a). % 1.95/2.16 1568[2:Res:3.1,1564.0] || -> c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a),u,tc_set(t_a)) c_in(c_Main_OsubsetI__1(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a),u,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)*. % 1.95/2.16 1575[2:Res:1568.1,4.0] || -> c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))* c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))*. % 1.95/2.16 1590[2:Obv:1575.0] || -> c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))*. % 1.95/2.16 1602[2:Res:1590.0,357.2] || c_in(u,v_S,tc_set(t_a))+ c_in(v,u,t_a)* -> c_in(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),u,t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))* c_in(v,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)*. % 1.95/2.16 1742[2:Res:12.1,1602.0] || c_in(u,v_S,tc_set(t_a))+ c_in(v,v_xa(u),t_a)* -> c_in(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(u),t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))* c_in(v,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)*. % 1.95/2.16 1799[2:Res:37.0,1742.0] || c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)*+ -> c_in(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))* c_in(u,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a). % 1.95/2.16 1806[3:Spt:1799.0,1799.2] || c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)* -> c_in(u,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a). % 1.95/2.16 1807[3:Res:3.1,1806.0] || -> c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),u,tc_set(t_a)) c_in(c_Main_OsubsetI__1(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),u,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)*. % 1.95/2.16 1814[3:Res:1807.1,4.0] || -> c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))* c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))*. % 1.95/2.16 1829[3:Obv:1814.0] || -> c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))*. % 1.95/2.16 1830[3:MRR:1829.0,71.0] || -> . % 1.95/2.16 1840[3:Spt:1830.0,1799.1] || -> c_in(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))*. % 1.95/2.16 1841[3:Res:1840.0,49.0] || c_in(u,c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),t_a)* -> c_in(u,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a). % 1.95/2.16 1845[3:Res:3.1,1841.0] || -> c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),u,tc_set(t_a)) c_in(c_Main_OsubsetI__1(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),u,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)*. % 1.95/2.16 1885[3:Res:1845.1,51.0] || -> c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a))* c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a))*. % 1.95/2.16 1895[3:Obv:1885.0] || -> c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a))*. % 1.95/2.16 1921[3:Res:1895.0,45.1] || c_in(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_S,tc_set(t_a)) -> c_in(c_union(c_insert(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),c_emptyset,tc_set(t_a)),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a)),c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))*. % 1.95/2.16 2033[3:Res:1921.1,10.3] || c_in(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_S,tc_set(t_a)) c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)* c_in(c_Zorn_OHausdorff__1(v_S,t_a),c_Zorn_Omaxchain(v_S,t_a),tc_set(tc_set(t_a)))* c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v,t_a),v,tc_set(t_a))* -> c_in(u,v,t_a)*. % 1.95/2.16 2038[3:MRR:2033.2,7.0] || c_in(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_S,tc_set(t_a)) c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)* c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v,t_a),v,tc_set(t_a))*+ -> c_in(u,v,t_a)*. % 1.95/2.16 2371[3:Res:1590.0,2038.2] || c_in(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_S,tc_set(t_a))*+ c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)* -> c_in(u,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a). % 1.95/2.16 2379[3:Res:12.1,2371.0] || c_in(v_x(c_Zorn_OHausdorff__1(v_S,t_a)),v_S,tc_set(t_a))* c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)* -> c_in(u,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a). % 1.95/2.16 2380[3:MRR:2379.0,37.0] || c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)* -> c_in(u,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a). % 1.95/2.16 2381[3:Res:3.1,2380.0] || -> c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),u,tc_set(t_a)) c_in(c_Main_OsubsetI__1(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),u,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)*. % 1.95/2.16 2405[3:Res:2381.1,4.0] || -> c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))* c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))*. % 1.95/2.16 2420[3:Obv:2405.0] || -> c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))*. % 1.95/2.16 2421[3:MRR:2420.0,71.0] || -> . % 1.95/2.16 2431[2:Spt:2421.0,1519.0,1563.0] || c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))* -> . % 1.95/2.16 2432[2:Spt:2421.0,1519.1] || -> c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_xa(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a)))),tc_set(t_a))*. % 1.95/2.16 2452[2:Res:1516.0,2431.0] || -> c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))*. % 1.95/2.16 2454[2:MRR:2452.0,71.0] || -> . % 1.95/2.16 2455[1:Spt:2454.0,1417.1] || -> c_in(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))*. % 1.95/2.16 2456[1:Res:2455.0,49.0] || c_in(u,c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),t_a)* -> c_in(u,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a). % 1.95/2.16 2476[1:Res:3.1,2456.0] || -> c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),u,tc_set(t_a)) c_in(c_Main_OsubsetI__1(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),u,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)*. % 1.99/2.18 2484[1:Res:2476.1,51.0] || -> c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a))* c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a))*. % 1.99/2.18 2494[1:Obv:2484.0] || -> c_lessequals(c_Zorn_Ochain__extend__1(c_Zorn_OHausdorff__1(v_S,t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a),v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),tc_set(t_a))*. % 1.99/2.18 2507[1:Res:2494.0,45.1] || c_in(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_S,tc_set(t_a)) -> c_in(c_union(c_insert(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),c_emptyset,tc_set(t_a)),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a)),c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))*. % 1.99/2.18 2603[1:Res:2507.1,10.3] || c_in(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_S,tc_set(t_a)) c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)* c_in(c_Zorn_OHausdorff__1(v_S,t_a),c_Zorn_Omaxchain(v_S,t_a),tc_set(tc_set(t_a)))* c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v,t_a),v,tc_set(t_a))* -> c_in(u,v,t_a)*. % 1.99/2.18 2604[1:Res:2507.1,9.2] || c_in(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_S,tc_set(t_a)) c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)* c_in(c_Zorn_OHausdorff__1(v_S,t_a),c_Zorn_Omaxchain(v_S,t_a),tc_set(tc_set(t_a))) -> c_in(u,v,t_a)* c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v,t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))*. % 1.99/2.18 2608[1:MRR:2603.2,7.0] || c_in(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_S,tc_set(t_a)) c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)* c_lessequals(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v,t_a),v,tc_set(t_a))*+ -> c_in(u,v,t_a)*. % 1.99/2.18 2609[1:MRR:2604.2,7.0] || c_in(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_S,tc_set(t_a)) c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)* -> c_in(u,v,t_a)* c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v,t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))*. % 1.99/2.18 2667[1:Res:38.1,2608.2] || c_in(c_Zorn_Omaxchain__super__lemma__1(c_Zorn_OHausdorff__1(v_S,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a),c_Zorn_OHausdorff__1(v_S,t_a),tc_set(t_a))* c_in(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_S,tc_set(t_a)) c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)* -> c_in(u,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a). % 1.99/2.18 2683[1:MRR:2667.0,2609.3] || c_in(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_S,tc_set(t_a))*+ c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)* -> c_in(u,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a). % 1.99/2.18 2698[1:Res:12.1,2683.0] || c_in(v_x(c_Zorn_OHausdorff__1(v_S,t_a)),v_S,tc_set(t_a))* c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)* -> c_in(u,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a). % 1.99/2.18 2699[1:MRR:2698.0,37.0] || c_in(u,v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),t_a)* -> c_in(u,v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a). % 1.99/2.18 2700[1:Res:3.1,2699.0] || -> c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),u,tc_set(t_a)) c_in(c_Main_OsubsetI__1(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),u,t_a),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),t_a)*. % 1.99/2.18 2706[1:Res:2700.1,4.0] || -> c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))* c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))*. % 1.99/2.18 2721[1:Obv:2706.0] || -> c_lessequals(v_xa(v_x(c_Zorn_OHausdorff__1(v_S,t_a))),v_x(c_Zorn_OHausdorff__1(v_S,t_a)),tc_set(t_a))*. % 1.99/2.18 2722[1:MRR:2721.0,71.0] || -> . % 1.99/2.18 % SZS output end Refutation % 1.99/2.18 Formulae used in the proof : cls_Set_Osubset__antisym_0 cls_Set_OsubsetD_0 cls_Set_OsubsetI_0 cls_Set_OsubsetI_1 cls_Zorn_Ochain__extend_0 cls_Zorn_Ochain__extend_1 cls_Zorn_OHausdorff_0 cls_Zorn_Omaxchain__subset__chain_0 cls_Zorn_Omaxchain__super__lemma_0 cls_Zorn_Omaxchain__super__lemma_1 cls_conjecture_0 cls_conjecture_1 cls_conjecture_2 cls_conjecture_3 cls_conjecture_4 % 1.99/2.18 %------------------------------------------------------------------------------