%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SET853-1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.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:18 EDT 2022 % Result : Unsatisfiable 3.73s 3.89s % Output : Refutation 3.81s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SET853-1 : TPTP v8.1.0. Released v3.2.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n019.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 : Sun Jul 10 13:06:38 EDT 2022 % 0.13/0.34 % CPUTime : % 3.73/3.89 % 3.73/3.89 SPASS V 3.9 % 3.73/3.89 SPASS beiseite: Proof found. % 3.73/3.89 % SZS status Theorem % 3.73/3.89 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.73/3.89 SPASS derived 5006 clauses, backtracked 548 clauses, performed 10 splits and kept 4579 clauses. % 3.73/3.89 SPASS allocated 86140 KBytes. % 3.73/3.89 SPASS spent 0:00:03.53 on the problem. % 3.73/3.89 0:00:00.09 for the input. % 3.73/3.89 0:00:00.00 for the FLOTTER CNF translation. % 3.73/3.89 0:00:00.18 for inferences. % 3.73/3.89 0:00:00.03 for the backtracking. % 3.73/3.89 0:00:02.94 for the reduction. % 3.73/3.89 % 3.73/3.89 % 3.73/3.89 Here is a proof with depth 7, length 116 : % 3.73/3.89 % SZS output start Refutation % 3.73/3.89 1[0:Inp] || -> c_lessequals(u,c_Zorn_Osucc(v,u,w),tc_set(tc_set(w)))*. % 3.73/3.89 2[0:Inp] || c_in(u,c_Zorn_OTFin(v,w),tc_set(tc_set(w)))+ c_in(x,c_Zorn_OTFin(v,w),tc_set(tc_set(w))) -> c_lessequals(u,x,tc_set(tc_set(w))) c_lessequals(c_Zorn_Osucc(v,x,w),u,tc_set(tc_set(w)))* c_in(c_Zorn_OTFin__linear__lemma1__1(v,x,w),c_Zorn_OTFin(v,w),tc_set(tc_set(w)))*. % 3.73/3.89 3[0:Inp] || c_in(u,c_Zorn_OTFin(v,w),tc_set(tc_set(w)))+ c_in(x,c_Zorn_OTFin(v,w),tc_set(tc_set(w))) -> c_lessequals(u,x,tc_set(tc_set(w))) c_lessequals(c_Zorn_Osucc(v,x,w),u,tc_set(tc_set(w)))* c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v,x,w),x,tc_set(tc_set(w)))*. % 3.73/3.89 4[0:Inp] || equal(c_Zorn_OTFin__linear__lemma1__1(u,v,w),v) c_in(x,c_Zorn_OTFin(u,w),tc_set(tc_set(w))) c_in(v,c_Zorn_OTFin(u,w),tc_set(tc_set(w))) -> c_lessequals(x,v,tc_set(tc_set(w))) c_lessequals(c_Zorn_Osucc(u,v,w),x,tc_set(tc_set(w)))*. % 3.73/3.89 5[0:Inp] || c_in(u,c_Zorn_OTFin(v,w),tc_set(tc_set(w))) c_in(x,c_Zorn_OTFin(v,w),tc_set(tc_set(w))) c_lessequals(c_Zorn_Osucc(v,c_Zorn_OTFin__linear__lemma1__1(v,x,w),w),x,tc_set(tc_set(w)))*+ -> c_lessequals(u,x,tc_set(tc_set(w))) c_lessequals(c_Zorn_Osucc(v,x,w),u,tc_set(tc_set(w)))*. % 3.73/3.89 9[0:Inp] || c_lessequals(u,v,tc_set(tc_set(w))) -> c_lessequals(u,c_Zorn_Osucc(x,v,w),tc_set(tc_set(w)))*. % 3.73/3.89 10[0:Inp] || -> c_in(v_x,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))*. % 3.73/3.89 11[0:Inp] || -> c_in(v_xa,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))*. % 3.73/3.89 12[0:Inp] || -> c_lessequals(v_xa,c_Zorn_Osucc(v_S,v_x,t_a),tc_set(tc_set(t_a)))*. % 3.73/3.89 13[0:Inp] || equal(c_Zorn_Osucc(v_S,v_x,t_a),v_xa)** -> . % 3.73/3.89 14[0:Inp] || c_lessequals(c_Zorn_Osucc(v_S,v_xa,t_a),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(tc_set(t_a)))* -> . % 3.73/3.89 15[0:Inp] || c_lessequals(u,v_x,tc_set(tc_set(t_a))) c_in(u,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) -> equal(u,v_x) c_lessequals(c_Zorn_Osucc(v_S,u,t_a),v_x,tc_set(tc_set(t_a)))*. % 3.73/3.89 131[0:Inp] || -> equal(u,c_0) c_less(c_0,u,tc_nat)*. % 3.73/3.89 135[0:Inp] || c_less(u,c_0,tc_nat)* -> . % 3.73/3.89 193[0:Inp] || c_less(u,c_emptyset,tc_set(v))* -> . % 3.73/3.89 212[0:Inp] || c_in(c_Pair(u,v,tc_nat,tc_nat),c_Wellfounded__Relations_Oless__than,tc_prod(tc_nat,tc_nat))* -> c_less(u,v,tc_nat). % 3.73/3.89 213[0:Inp] || c_less(u,v,tc_nat) -> c_in(c_Pair(u,v,tc_nat,tc_nat),c_Wellfounded__Relations_Oless__than,tc_prod(tc_nat,tc_nat))*. % 3.73/3.89 287[0:Inp] || c_in(u,v,w)* c_in(c_Pair(u,x,w,y),z,tc_prod(w,y))*+ -> c_in(x,c_Relation_OImage(z,v,w,y),y)*. % 3.73/3.89 288[0:Inp] || c_in(u,c_Relation_ORange(v,w,x),x) -> c_in(c_Pair(c_Main_ORangeE__1(u,v,x,w),u,w,x),v,tc_prod(w,x))*. % 3.73/3.89 289[0:Inp] || c_in(c_Pair(u,v,w,x),y,tc_prod(w,x))* -> c_in(v,c_Relation_ORange(y,w,x),x). % 3.73/3.89 311[0:Inp] || -> c_in(u,c_UNIV,v)*. % 3.73/3.89 314[0:Inp] || -> c_lessequals(c_emptyset,u,tc_set(v))*. % 3.73/3.89 317[0:Inp] || c_lessequals(u,v,tc_set(w)) -> equal(u,v) c_less(u,v,tc_set(w))*. % 3.73/3.89 322[0:Inp] || -> c_lessequals(u,v,tc_set(w)) c_in(c_Main_OsubsetI__1(u,v,w),u,w)*. % 3.73/3.89 323[0:Inp] || c_in(c_Main_OsubsetI__1(u,v,w),v,w)* -> c_lessequals(u,v,tc_set(w)). % 3.73/3.89 324[0:Inp] || c_lessequals(u,v,tc_set(w))*+ c_lessequals(v,u,tc_set(w))* -> equal(u,v). % 3.73/3.89 1459[0:Res:11.0,15.1] || c_lessequals(v_xa,v_x,tc_set(tc_set(t_a))) -> c_lessequals(c_Zorn_Osucc(v_S,v_xa,t_a),v_x,tc_set(tc_set(t_a)))* equal(v_xa,v_x). % 3.73/3.89 1488[0:Res:10.0,5.0] || c_in(u,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a)))* -> c_lessequals(u,v_x,tc_set(tc_set(t_a))) c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),u,tc_set(tc_set(t_a)))*. % 3.73/3.89 1489[0:Res:10.0,2.0] || c_in(u,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))+ -> c_lessequals(u,v_x,tc_set(tc_set(t_a))) c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),u,tc_set(tc_set(t_a)))* c_in(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))*. % 3.73/3.89 1490[0:Res:10.0,3.0] || c_in(u,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))+ -> c_lessequals(u,v_x,tc_set(tc_set(t_a))) c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),u,tc_set(tc_set(t_a)))* c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a)))*. % 3.73/3.89 1491[0:Res:10.0,4.0] || equal(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x) c_in(u,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) -> c_lessequals(u,v_x,tc_set(tc_set(t_a))) c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),u,tc_set(tc_set(t_a)))*. % 3.73/3.89 1508[0:Res:12.0,324.0] || c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),v_xa,tc_set(tc_set(t_a)))* -> equal(c_Zorn_Osucc(v_S,v_x,t_a),v_xa). % 3.73/3.89 1520[0:Res:9.1,14.0] || c_lessequals(c_Zorn_Osucc(v_S,v_xa,t_a),v_x,tc_set(tc_set(t_a)))* -> . % 3.73/3.89 1530[0:Res:323.1,14.0] || c_in(c_Main_OsubsetI__1(c_Zorn_Osucc(v_S,v_xa,t_a),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a)),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a))* -> . % 3.73/3.89 1531[0:Res:322.1,14.0] || -> c_in(c_Main_OsubsetI__1(c_Zorn_Osucc(v_S,v_xa,t_a),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a)),c_Zorn_Osucc(v_S,v_xa,t_a),tc_set(t_a))*. % 3.73/3.89 1535[0:Res:314.0,15.0] || c_in(c_emptyset,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) -> equal(c_emptyset,v_x) c_lessequals(c_Zorn_Osucc(v_S,c_emptyset,t_a),v_x,tc_set(tc_set(t_a)))*. % 3.73/3.89 1539[0:MRR:1508.1,13.0] || c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),v_xa,tc_set(tc_set(t_a)))* -> . % 3.73/3.89 1540[0:MRR:1459.1,1520.0] || c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))* -> equal(v_xa,v_x). % 3.73/3.89 1567[0:Res:11.0,1488.0] || c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a)))* -> c_lessequals(v_xa,v_x,tc_set(tc_set(t_a))) c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),v_xa,tc_set(tc_set(t_a))). % 3.73/3.89 1575[0:Res:11.0,1490.0] || -> c_lessequals(v_xa,v_x,tc_set(tc_set(t_a))) c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a)))* c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),v_xa,tc_set(tc_set(t_a))). % 3.73/3.89 1579[0:Res:11.0,1491.0] || equal(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x) -> c_lessequals(v_xa,v_x,tc_set(tc_set(t_a))) c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),v_xa,tc_set(tc_set(t_a)))*. % 3.73/3.89 1596[0:MRR:1579.2,1539.0] || equal(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x) -> c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))*. % 3.73/3.89 1598[0:MRR:1575.2,1539.0] || -> c_lessequals(v_xa,v_x,tc_set(tc_set(t_a))) c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a)))*. % 3.73/3.89 1602[0:MRR:1567.2,1539.0] || c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a)))* -> c_lessequals(v_xa,v_x,tc_set(tc_set(t_a))). % 3.73/3.89 1604[1:Spt:1490.0,1490.1,1490.2] || c_in(u,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) -> c_lessequals(u,v_x,tc_set(tc_set(t_a))) c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),u,tc_set(tc_set(t_a)))*. % 3.73/3.89 1633[2:Spt:1598.0] || -> c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))*. % 3.73/3.89 1634[2:MRR:1540.0,1633.0] || -> equal(v_xa,v_x)**. % 3.73/3.89 1636[2:Rew:1634.0,1530.0] || c_in(c_Main_OsubsetI__1(c_Zorn_Osucc(v_S,v_x,t_a),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a)),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a))* -> . % 3.73/3.89 1644[2:Rew:1634.0,1531.0] || -> c_in(c_Main_OsubsetI__1(c_Zorn_Osucc(v_S,v_x,t_a),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a)),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a))*. % 3.73/3.89 1677[2:MRR:1636.0,1644.0] || -> . % 3.73/3.89 1685[2:Spt:1677.0,1598.0,1633.0] || c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))* -> . % 3.73/3.89 1686[2:Spt:1677.0,1598.1] || -> c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a)))*. % 3.73/3.89 1736[1:Res:1604.2,1539.0] || c_in(v_xa,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))* -> c_lessequals(v_xa,v_x,tc_set(tc_set(t_a))). % 3.73/3.89 1737[2:MRR:1736.0,1736.1,11.0,1685.0] || -> . % 3.73/3.89 1738[1:Spt:1737.0,1490.3] || -> c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a)))*. % 3.73/3.89 1739[2:Spt:1489.0,1489.1,1489.2] || c_in(u,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) -> c_lessequals(u,v_x,tc_set(tc_set(t_a))) c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),u,tc_set(tc_set(t_a)))*. % 3.73/3.89 1740[2:Res:1739.2,1539.0] || c_in(v_xa,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))* -> c_lessequals(v_xa,v_x,tc_set(tc_set(t_a))). % 3.81/4.02 1741[2:MRR:1740.0,11.0] || -> c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))*. % 3.81/4.02 1742[2:MRR:1540.0,1741.0] || -> equal(v_xa,v_x)**. % 3.81/4.02 1753[2:Rew:1742.0,1530.0] || c_in(c_Main_OsubsetI__1(c_Zorn_Osucc(v_S,v_x,t_a),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a)),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a))* -> . % 3.81/4.02 1754[2:Rew:1742.0,1531.0] || -> c_in(c_Main_OsubsetI__1(c_Zorn_Osucc(v_S,v_x,t_a),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a)),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a))*. % 3.81/4.02 1791[2:MRR:1753.0,1754.0] || -> . % 3.81/4.02 1804[2:Spt:1791.0,1489.3] || -> c_in(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))*. % 3.81/4.02 1805[3:Spt:1535.1] || -> equal(c_emptyset,v_x)**. % 3.81/4.02 1814[3:Rew:1805.0,193.0] || c_less(u,v_x,tc_set(v))* -> . % 3.81/4.02 1962[0:Res:1596.1,1540.0] || equal(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x)** -> equal(v_xa,v_x). % 3.81/4.02 2044[0:Res:311.0,323.0] || -> c_lessequals(u,c_UNIV,tc_set(v))*. % 3.81/4.02 2136[3:Res:317.2,1814.0] || c_lessequals(u,v_x,tc_set(v))* -> equal(u,v_x). % 3.81/4.02 2142[3:Res:1738.0,2136.0] || -> equal(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x)**. % 3.81/4.02 2149[3:Rew:2142.0,1962.0] || equal(v_x,v_x) -> equal(v_xa,v_x)**. % 3.81/4.02 2153[3:Obv:2149.0] || -> equal(v_xa,v_x)**. % 3.81/4.02 2169[3:Rew:2153.0,1530.0] || c_in(c_Main_OsubsetI__1(c_Zorn_Osucc(v_S,v_x,t_a),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a)),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a))* -> . % 3.81/4.02 2170[3:Rew:2153.0,1531.0] || -> c_in(c_Main_OsubsetI__1(c_Zorn_Osucc(v_S,v_x,t_a),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a)),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a))*. % 3.81/4.02 2198[3:MRR:2169.0,2170.0] || -> . % 3.81/4.02 2209[3:Spt:2198.0,1535.1,1805.0] || equal(c_emptyset,v_x)** -> . % 3.81/4.02 2210[3:Spt:2198.0,1535.0,1535.2] || c_in(c_emptyset,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) -> c_lessequals(c_Zorn_Osucc(v_S,c_emptyset,t_a),v_x,tc_set(tc_set(t_a)))*. % 3.81/4.02 2373[0:Res:2044.0,324.0] || c_lessequals(c_UNIV,u,tc_set(v))* -> equal(u,c_UNIV). % 3.81/4.02 2376[1:Res:1738.0,324.0] || c_lessequals(v_x,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),tc_set(tc_set(t_a)))* -> equal(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x). % 3.81/4.02 3424[0:Res:213.1,289.0] || c_less(u,v,tc_nat)*+ -> c_in(v,c_Relation_ORange(c_Wellfounded__Relations_Oless__than,tc_nat,tc_nat),tc_nat)*. % 3.81/4.02 3680[0:Res:131.1,3424.0] || -> equal(u,c_0) c_in(u,c_Relation_ORange(c_Wellfounded__Relations_Oless__than,tc_nat,tc_nat),tc_nat)*. % 3.81/4.02 3690[0:Res:3680.1,323.0] || -> equal(c_Main_OsubsetI__1(u,c_Relation_ORange(c_Wellfounded__Relations_Oless__than,tc_nat,tc_nat),tc_nat),c_0) c_lessequals(u,c_Relation_ORange(c_Wellfounded__Relations_Oless__than,tc_nat,tc_nat),tc_set(tc_nat))*. % 3.81/4.02 3851[0:Res:3690.1,2373.0] || -> equal(c_Main_OsubsetI__1(c_UNIV,c_Relation_ORange(c_Wellfounded__Relations_Oless__than,tc_nat,tc_nat),tc_nat),c_0)** equal(c_Relation_ORange(c_Wellfounded__Relations_Oless__than,tc_nat,tc_nat),c_UNIV). % 3.81/4.02 3854[4:Spt:3851.1] || -> equal(c_Relation_ORange(c_Wellfounded__Relations_Oless__than,tc_nat,tc_nat),c_UNIV)**. % 3.81/4.02 4143[0:Res:288.1,212.0] || c_in(u,c_Relation_ORange(c_Wellfounded__Relations_Oless__than,tc_nat,tc_nat),tc_nat) -> c_less(c_Main_ORangeE__1(u,c_Wellfounded__Relations_Oless__than,tc_nat,tc_nat),u,tc_nat)*. % 3.81/4.02 4155[4:Rew:3854.0,4143.0] || c_in(u,c_UNIV,tc_nat) -> c_less(c_Main_ORangeE__1(u,c_Wellfounded__Relations_Oless__than,tc_nat,tc_nat),u,tc_nat)*. % 3.81/4.02 4156[4:MRR:4155.0,311.0] || -> c_less(c_Main_ORangeE__1(u,c_Wellfounded__Relations_Oless__than,tc_nat,tc_nat),u,tc_nat)*. % 3.81/4.02 4157[4:UnC:4156.0,135.0] || -> . % 3.81/4.02 4164[4:Spt:4157.0,3851.1,3854.0] || equal(c_Relation_ORange(c_Wellfounded__Relations_Oless__than,tc_nat,tc_nat),c_UNIV)** -> . % 3.81/4.02 4165[4:Spt:4157.0,3851.0] || -> equal(c_Main_OsubsetI__1(c_UNIV,c_Relation_ORange(c_Wellfounded__Relations_Oless__than,tc_nat,tc_nat),tc_nat),c_0)**. % 3.81/4.02 4528[0:Res:311.0,287.1] || c_in(u,v,w)*+ -> c_in(x,c_Relation_OImage(c_UNIV,v,w,y),y)*. % 3.81/4.02 4673[0:Res:322.1,4528.0] || -> c_lessequals(u,v,tc_set(w))* c_in(x,c_Relation_OImage(c_UNIV,u,w,y),y)*. % 3.81/4.02 5549[0:Res:4673.1,323.0] || -> c_lessequals(u,v,tc_set(w))* c_lessequals(x,c_Relation_OImage(c_UNIV,u,w,y),tc_set(y))*. % 3.81/4.02 5698[0:Res:5549.1,2373.0] || -> c_lessequals(u,v,tc_set(w))* equal(c_Relation_OImage(c_UNIV,u,w,x),c_UNIV)**. % 3.81/4.02 5779[0:Res:5698.0,324.0] || c_lessequals(u,v,tc_set(w))*+ -> equal(c_Relation_OImage(c_UNIV,v,w,x),c_UNIV)** equal(v,u). % 3.81/4.02 5781[1:Res:5698.0,2376.0] || -> equal(c_Relation_OImage(c_UNIV,v_x,tc_set(t_a),u),c_UNIV)** equal(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x). % 3.81/4.02 5815[5:Spt:5781.1] || -> equal(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x)**. % 3.81/4.02 5817[5:Rew:5815.0,1962.0] || equal(v_x,v_x) -> equal(v_xa,v_x)**. % 3.81/4.02 5831[5:Obv:5817.0] || -> equal(v_xa,v_x)**. % 3.81/4.02 5841[5:Rew:5831.0,1531.0] || -> c_in(c_Main_OsubsetI__1(c_Zorn_Osucc(v_S,v_x,t_a),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a)),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a))*. % 3.81/4.02 5861[5:Rew:5831.0,1530.0] || c_in(c_Main_OsubsetI__1(c_Zorn_Osucc(v_S,v_x,t_a),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a)),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a))* -> . % 3.81/4.02 5980[5:MRR:5861.0,5841.0] || -> . % 3.81/4.02 6008[5:Spt:5980.0,5781.1,5815.0] || equal(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x)** -> . % 3.81/4.02 6009[5:Spt:5980.0,5781.0] || -> equal(c_Relation_OImage(c_UNIV,v_x,tc_set(t_a),u),c_UNIV)**. % 3.81/4.02 6967[0:Res:1.0,5779.0] || -> equal(c_Relation_OImage(c_UNIV,c_Zorn_Osucc(u,v,w),tc_set(w),x),c_UNIV)** equal(c_Zorn_Osucc(u,v,w),v). % 3.81/4.02 6975[0:Res:12.0,5779.0] || -> equal(c_Relation_OImage(c_UNIV,c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a),u),c_UNIV)** equal(c_Zorn_Osucc(v_S,v_x,t_a),v_xa). % 3.81/4.02 6991[0:Rew:6967.1,6975.1] || -> equal(c_Relation_OImage(c_UNIV,c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a),u),c_UNIV)** equal(v_xa,v_x). % 3.81/4.02 7141[6:Spt:6991.1] || -> equal(v_xa,v_x)**. % 3.81/4.02 7167[6:Rew:7141.0,1530.0] || c_in(c_Main_OsubsetI__1(c_Zorn_Osucc(v_S,v_x,t_a),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a)),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a))* -> . % 3.81/4.02 7170[6:Rew:7141.0,1531.0] || -> c_in(c_Main_OsubsetI__1(c_Zorn_Osucc(v_S,v_x,t_a),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a)),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a))*. % 3.81/4.02 7295[6:MRR:7167.0,7170.0] || -> . % 3.81/4.02 7319[6:Spt:7295.0,6991.1,7141.0] || equal(v_xa,v_x)** -> . % 3.81/4.02 7320[6:Spt:7295.0,6991.0] || -> equal(c_Relation_OImage(c_UNIV,c_Zorn_Osucc(v_S,v_x,t_a),tc_set(t_a),u),c_UNIV)**. % 3.81/4.02 7321[6:MRR:1540.1,7319.0] || c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))* -> . % 3.81/4.02 7324[6:MRR:1602.1,7321.0] || c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a)))* -> . % 3.81/4.02 7424[6:Res:15.3,7324.0] || c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a))) c_in(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))* -> equal(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x). % 3.81/4.02 7428[6:MRR:7424.0,7424.1,7424.2,1738.0,1804.0,6008.0] || -> . % 3.81/4.02 % SZS output end Refutation % 3.81/4.02 Formulae used in the proof : cls_Zorn_OAbrial__axiom1_0 cls_Zorn_OTFin__linear__lemma1_0 cls_Zorn_OTFin__linear__lemma1_1 cls_Zorn_OTFin__linear__lemma1_2 cls_Zorn_OTFin__linear__lemma1_3 cls_Zorn_Osucc__trans_0 cls_conjecture_0 cls_conjecture_1 cls_conjecture_2 cls_conjecture_3 cls_conjecture_4 cls_conjecture_5 cls_Nat_Oneq0__conv__iff1_0 cls_Nat_Onot__less0__iff1_0 cls_Set_Onot__psubset__empty__iff1_0 cls_Wellfounded__Relations_Oless__than__iff__iff1_0 cls_Wellfounded__Relations_Oless__than__iff__iff2_0 cls_Relation_OImageI_0 cls_Relation_ORangeE_0 cls_Relation_ORangeI_0 cls_Set_OUNIV__I_0 cls_Set_Oempty__subsetI_0 cls_Set_OpsubsetI_0 cls_Set_OsubsetI_0 cls_Set_OsubsetI_1 cls_Set_Osubset__antisym_0 % 3.81/4.02 %------------------------------------------------------------------------------