%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GEO528+1 : TPTP v8.1.0. Released v7.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n014.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 : Sat Jul 16 06:25:05 EDT 2022 % Result : Theorem 159.52s 159.70s % Output : Refutation 161.28s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.14 % Problem : GEO528+1 : TPTP v8.1.0. Released v7.0.0. % 0.13/0.15 % Command : run_spass %d %s % 0.15/0.37 % Computer : n014.cluster.edu % 0.15/0.37 % Model : x86_64 x86_64 % 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.37 % Memory : 8042.1875MB % 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.37 % CPULimit : 300 % 0.15/0.37 % WCLimit : 600 % 0.15/0.37 % DateTime : Sat Jun 18 08:59:04 EDT 2022 % 0.15/0.37 % CPUTime : % 159.52/159.70 % 159.52/159.70 SPASS V 3.9 % 159.52/159.70 SPASS beiseite: Proof found. % 159.52/159.70 % SZS status Theorem % 159.52/159.70 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 159.52/159.70 SPASS derived 68653 clauses, backtracked 2796 clauses, performed 11 splits and kept 27500 clauses. % 159.52/159.70 SPASS allocated 138585 KBytes. % 159.52/159.70 SPASS spent 0:2:39.25 on the problem. % 159.52/159.70 0:00:00.04 for the input. % 159.52/159.70 0:00:00.08 for the FLOTTER CNF translation. % 159.52/159.70 0:00:02.75 for inferences. % 159.52/159.70 0:00:07.53 for the backtracking. % 159.52/159.70 0:2:26.59 for the reduction. % 159.52/159.70 % 159.52/159.70 % 159.52/159.70 Here is a proof with depth 9, length 158 : % 159.52/159.70 % SZS output start Refutation % 159.52/159.70 1[0:Inp] || equal(skc4,skc3)** -> . % 159.52/159.70 8[0:Inp] || -> s_col(u,v,u)*. % 159.52/159.70 11[0:Inp] || s_col(skc3,skc4,skc5)* -> . % 159.52/159.70 16[0:Inp] || -> equal(s(u,u),u)**. % 159.52/159.70 22[0:Inp] || -> s_m(u,midpoint(u,v),v)*. % 159.52/159.70 25[0:Inp] || -> equal(s(u,s(u,v)),v)**. % 159.52/159.70 32[0:Inp] || opposite(skc5,skc3,skc4,reflect(skc3,skc4,skc5))* -> . % 159.52/159.70 38[0:Inp] || s_col(u,v,w)*+ -> s_col(v,u,w)*. % 159.52/159.70 44[0:Inp] || s_m(u,v,w)*+ -> s_m(w,v,u)*. % 159.52/159.70 46[0:Inp] || -> s_e(u,v,s(w,u),s(w,v))*. % 159.52/159.70 47[0:Inp] || s_r(u,v,w)*+ -> s_r(w,v,u)*. % 159.52/159.70 53[0:Inp] || s_m(u,v,w)* -> s_t(u,v,w). % 159.52/159.70 59[0:Inp] || s_m(u,v,w)* -> equal(w,s(v,u)). % 159.52/159.70 69[0:Inp] || equal(s(u,v),s(w,v))* -> equal(u,w). % 159.52/159.70 84[0:Inp] || equal(u,v) perpAt(u,v,w,x,y)* -> . % 159.52/159.70 94[0:Inp] || -> s_col(u,v,w) perp(u,v,w,foot(u,v,w))*. % 159.52/159.70 96[0:Inp] || -> equal(u,v) s_col(u,v,midpoint(w,reflect(u,v,w)))*. % 159.52/159.70 99[0:Inp] || -> equal(u,v) equal(reflect(u,v,reflect(u,v,w)),w)**. % 159.52/159.70 101[0:Inp] || s_e(u,v,u,s(w,v))* -> s_r(u,w,v). % 159.52/159.70 109[0:Inp] || s_r(u,v,w)*+ s_r(u,w,v)* -> equal(w,v). % 159.52/159.70 132[0:Inp] || equal(reflect(u,v,w),w)** -> equal(u,v) s_col(u,v,w). % 159.52/159.70 133[0:Inp] || s_col(u,v,w) -> equal(u,v) equal(reflect(u,v,w),w)**. % 159.52/159.70 174[0:Inp] || s_t(u,v,w) -> equal(v,u) equal(xb,u) sameside(v,u,w)*. % 159.52/159.70 187[0:Inp] || perp(u,v,w,x) -> perpAt(u,v,il(u,v,w,x),w,x)*. % 159.52/159.70 229[0:Inp] || sameside(u,v,w)*+ s_t(x,v,w)* -> equal(v,w) equal(v,x) s_col(u,v,x)*. % 159.52/159.70 234[0:Inp] || -> equal(u,v) s_col(u,v,w) s_col(u,v,x) opposite(x,u,v,w)* samesideline(x,w,u,v). % 159.52/159.70 261[0:Inp] || s_col(u,v,w)*+ s_t(x,w,y)* -> equal(u,v) s_col(u,v,x) s_col(u,v,y) opposite(x,u,v,y)*. % 159.52/159.70 267[0:Inp] || s_col(xa,xb,xq) s_col(xa,xb,xp) perp(xc,xd,xa,xb) -> equal(xb,xa) equal(xq,xp) perp(xc,xd,xp,xq)*. % 159.52/159.70 358[0:Res:99.1,1.0] || -> equal(reflect(skc4,skc3,reflect(skc4,skc3,u)),u)**. % 159.52/159.70 376[0:Res:174.2,1.0] || s_t(skc3,skc4,u) -> equal(skc3,xb) sameside(skc4,skc3,u)*. % 159.52/159.70 476[0:Res:99.1,1.0] || -> equal(reflect(skc3,skc4,reflect(skc3,skc4,u)),u)**. % 159.52/159.70 494[0:Res:174.2,1.0] || s_t(skc4,skc3,u) -> equal(skc4,xb) sameside(skc3,skc4,u)*. % 159.52/159.70 557[0:Res:132.1,11.0] || equal(reflect(skc3,skc4,skc5),skc5)** -> equal(skc4,skc3). % 159.52/159.70 578[0:Res:229.3,11.0] || sameside(skc3,skc4,u)* s_t(skc5,skc4,u) -> equal(skc4,u) equal(skc5,skc4). % 159.52/159.70 593[0:Res:234.2,32.0] || -> s_col(skc3,skc4,skc5) samesideline(skc5,reflect(skc3,skc4,skc5),skc3,skc4)* s_col(skc3,skc4,reflect(skc3,skc4,skc5)) equal(skc4,skc3). % 159.52/159.70 594[0:Res:261.2,32.0] || s_t(skc5,u,reflect(skc3,skc4,skc5))* s_col(skc3,skc4,u) -> s_col(skc3,skc4,reflect(skc3,skc4,skc5))* s_col(skc3,skc4,skc5) equal(skc4,skc3). % 159.52/159.70 596[0:MRR:557.1,1.0] || equal(reflect(skc3,skc4,skc5),skc5)** -> . % 159.52/159.70 604[0:MRR:593.0,593.3,11.0,1.0] || -> s_col(skc3,skc4,reflect(skc3,skc4,skc5)) samesideline(skc5,reflect(skc3,skc4,skc5),skc3,skc4)*. % 159.52/159.70 609[0:MRR:594.3,594.4,11.0,1.0] || s_t(skc5,u,reflect(skc3,skc4,skc5))* s_col(skc3,skc4,u) -> s_col(skc3,skc4,reflect(skc3,skc4,skc5))*. % 159.52/159.70 614[1:Spt:494.1] || -> equal(skc4,xb)**. % 159.52/159.70 615[1:Rew:614.0,596.0] || equal(reflect(skc3,xb,skc5),skc5)** -> . % 159.52/159.70 616[1:Rew:614.0,609.0] || s_t(skc5,u,reflect(skc3,xb,skc5))* s_col(skc3,skc4,u) -> s_col(skc3,skc4,reflect(skc3,skc4,skc5))*. % 159.52/159.70 811[1:Rew:614.0,604.0] || -> s_col(skc3,xb,reflect(skc3,xb,skc5)) samesideline(skc5,reflect(skc3,skc4,skc5),skc3,skc4)*. % 159.52/159.70 825[1:Rew:614.0,1.0] || equal(skc3,xb)** -> . % 159.52/159.70 858[1:Rew:614.0,476.0] || -> equal(reflect(skc3,xb,reflect(skc3,xb,u)),u)**. % 159.52/159.70 860[1:Rew:614.0,358.0] || -> equal(reflect(xb,skc3,reflect(xb,skc3,u)),u)**. % 159.52/159.70 931[1:Rew:614.0,811.1] || -> s_col(skc3,xb,reflect(skc3,xb,skc5)) samesideline(skc5,reflect(skc3,xb,skc5),skc3,xb)*. % 159.52/159.70 965[1:Rew:614.0,616.2,614.0,616.1] || s_t(skc5,u,reflect(skc3,xb,skc5))* s_col(skc3,xb,u) -> s_col(skc3,xb,reflect(skc3,xb,skc5))*. % 159.52/159.70 1127[0:SpR:16.0,46.0] || -> s_e(u,v,u,s(u,v))*. % 159.52/159.70 1130[0:Res:22.0,44.0] || -> s_m(u,midpoint(v,u),v)*. % 159.52/159.70 1139[0:SpR:25.0,1127.0] || -> s_e(u,s(u,v),u,v)*. % 159.52/159.70 1155[0:Res:22.0,53.0] || -> s_t(u,midpoint(u,v),v)*. % 159.52/159.70 1223[0:Res:8.0,38.0] || -> s_col(u,v,v)*. % 159.52/159.70 1443[0:Res:22.0,59.0] || -> equal(s(midpoint(u,v),u),v)**. % 159.52/159.70 1444[0:Res:1130.0,59.0] || -> equal(s(midpoint(u,v),v),u)**. % 159.52/159.70 1454[0:SpR:1443.0,1127.0] || -> s_e(midpoint(u,v),u,midpoint(u,v),v)*. % 159.52/159.70 1456[0:SpR:1443.0,1139.0] || -> s_e(midpoint(u,v),v,midpoint(u,v),u)*. % 159.52/159.70 1717[0:SpL:1443.0,69.0] || equal(u,s(v,w))*+ -> equal(midpoint(w,u),v)*. % 159.52/159.70 2504[0:Res:1456.0,101.0] || -> s_r(midpoint(s(u,v),v),u,v)*. % 159.52/159.70 2509[0:Res:1454.0,101.0] || -> s_r(midpoint(u,s(v,u)),v,u)*. % 159.52/159.70 2517[0:SpR:1443.0,2504.0] || -> s_r(midpoint(u,v),midpoint(v,u),v)*. % 159.52/159.70 2529[0:SpR:1444.0,2509.0] || -> s_r(midpoint(u,v),midpoint(v,u),u)*. % 159.52/159.70 2538[0:Res:2517.0,47.0] || -> s_r(u,midpoint(u,v),midpoint(v,u))*. % 159.52/159.70 2554[0:Res:2529.0,47.0] || -> s_r(u,midpoint(v,u),midpoint(u,v))*. % 159.52/159.70 2659[0:Res:2538.0,109.0] || s_r(u,midpoint(v,u),midpoint(u,v))* -> equal(midpoint(v,u),midpoint(u,v)). % 159.52/159.70 2669[0:MRR:2659.0,2554.0] || -> equal(midpoint(u,v),midpoint(v,u))*. % 159.52/159.70 3466[0:SpR:133.2,99.1] || s_col(u,v,reflect(u,v,w))* -> equal(u,v) equal(u,v) equal(reflect(u,v,w),w). % 159.52/159.70 3509[0:Obv:3466.1] || s_col(u,v,reflect(u,v,w))* -> equal(u,v) equal(reflect(u,v,w),w). % 159.52/159.70 4005[0:SpL:1443.0,1717.0] || equal(u,v) -> equal(midpoint(w,u),midpoint(w,v))*. % 159.52/159.70 4007[0:SpL:1444.0,1717.0] || equal(u,v) -> equal(midpoint(w,u),midpoint(v,w))*. % 159.52/159.70 4129[0:SpR:4005.1,1155.0] || equal(u,v) -> s_t(w,midpoint(w,v),u)*. % 159.52/159.70 4311[0:SpR:2669.0,4129.1] || equal(u,v) -> s_t(w,midpoint(v,w),u)*. % 159.52/159.70 6451[0:Res:187.1,84.1] || perp(u,v,w,x)* equal(u,v) -> . % 159.52/159.70 6988[0:Res:94.1,6451.0] || equal(u,v) -> s_col(u,v,w)*. % 159.52/159.70 8400[0:SpR:4007.1,96.1] || equal(reflect(u,v,w),x) -> equal(u,v) s_col(u,v,midpoint(x,w))*. % 159.52/159.70 8585[0:MRR:8400.1,6988.0] || equal(reflect(u,v,w),x) -> s_col(u,v,midpoint(x,w))*. % 159.52/159.70 15479[2:Spt:267.3] || -> equal(xb,xa)**. % 159.52/159.70 15482[2:Rew:15479.0,825.0] || equal(skc3,xa)** -> . % 159.52/159.70 15521[2:Rew:15479.0,615.0] || equal(reflect(skc3,xa,skc5),skc5)** -> . % 159.52/159.70 15603[2:Rew:15479.0,860.0] || -> equal(reflect(xa,skc3,reflect(xa,skc3,u)),u)**. % 159.52/159.70 16160[2:Rew:15479.0,965.0] || s_t(skc5,u,reflect(skc3,xa,skc5))* s_col(skc3,xb,u) -> s_col(skc3,xb,reflect(skc3,xb,skc5))*. % 159.52/159.70 16744[2:Rew:15479.0,931.0] || -> s_col(skc3,xa,reflect(skc3,xa,skc5)) samesideline(skc5,reflect(skc3,xb,skc5),skc3,xb)*. % 159.52/159.70 17783[2:Rew:15479.0,16744.1] || -> s_col(skc3,xa,reflect(skc3,xa,skc5)) samesideline(skc5,reflect(skc3,xa,skc5),skc3,xa)*. % 159.52/159.70 18022[2:Rew:15479.0,16160.2,15479.0,16160.1] || s_t(skc5,u,reflect(skc3,xa,skc5))* s_col(skc3,xa,u) -> s_col(skc3,xa,reflect(skc3,xa,skc5))*. % 159.52/159.70 39347[3:Spt:17783.0] || -> s_col(skc3,xa,reflect(skc3,xa,skc5))*. % 159.52/159.70 54065[3:Res:39347.0,3509.0] || -> equal(skc3,xa) equal(reflect(skc3,xa,skc5),skc5)**. % 159.52/159.70 54066[3:MRR:54065.0,54065.1,15482.0,15521.0] || -> . % 159.52/159.70 54074[3:Spt:54066.0,17783.0,39347.0] || s_col(skc3,xa,reflect(skc3,xa,skc5))* -> . % 159.52/159.70 54075[3:Spt:54066.0,17783.1] || -> samesideline(skc5,reflect(skc3,xa,skc5),skc3,xa)*. % 159.52/159.70 54077[3:MRR:18022.2,54074.0] || s_t(skc5,u,reflect(skc3,xa,skc5))* s_col(skc3,xa,u) -> . % 159.52/159.70 54312[3:Res:4311.1,54077.0] || equal(reflect(skc3,xa,skc5),u) s_col(skc3,xa,midpoint(u,skc5))* -> . % 159.52/159.70 54338[3:MRR:54312.1,8585.1] || equal(reflect(skc3,xa,skc5),u)* -> . % 159.52/159.70 54339[3:UnC:54338.0,15603.0] || -> . % 159.52/159.70 54344[2:Spt:54339.0,267.3,15479.0] || equal(xb,xa)** -> . % 159.52/159.70 54345[2:Spt:54339.0,267.0,267.1,267.2,267.4,267.5] || s_col(xa,xb,xq) s_col(xa,xb,xp) perp(xc,xd,xa,xb) -> equal(xq,xp) perp(xc,xd,xp,xq)*. % 159.52/159.70 60436[3:Spt:931.0] || -> s_col(skc3,xb,reflect(skc3,xb,skc5))*. % 159.52/159.70 60452[3:Res:60436.0,3509.0] || -> equal(skc3,xb) equal(reflect(skc3,xb,skc5),skc5)**. % 159.52/159.70 60455[3:MRR:60452.0,60452.1,825.0,615.0] || -> . % 159.52/159.70 60461[3:Spt:60455.0,931.0,60436.0] || s_col(skc3,xb,reflect(skc3,xb,skc5))* -> . % 159.52/159.70 60462[3:Spt:60455.0,931.1] || -> samesideline(skc5,reflect(skc3,xb,skc5),skc3,xb)*. % 159.52/159.70 60464[3:MRR:965.2,60461.0] || s_t(skc5,u,reflect(skc3,xb,skc5))* s_col(skc3,xb,u) -> . % 159.52/159.70 60682[3:Res:4311.1,60464.0] || equal(reflect(skc3,xb,skc5),u) s_col(skc3,xb,midpoint(u,skc5))* -> . % 161.28/161.49 60708[3:MRR:60682.1,8585.1] || equal(reflect(skc3,xb,skc5),u)* -> . % 161.28/161.49 60709[3:UnC:60708.0,858.0] || -> . % 161.28/161.49 60714[1:Spt:60709.0,494.1,614.0] || equal(skc4,xb)** -> . % 161.28/161.49 60715[1:Spt:60709.0,494.0,494.2] || s_t(skc4,skc3,u) -> sameside(skc3,skc4,u)*. % 161.28/161.49 60780[2:Spt:376.1] || -> equal(skc3,xb)**. % 161.28/161.49 60815[2:Rew:60780.0,596.0] || equal(reflect(xb,skc4,skc5),skc5)** -> . % 161.28/161.49 60816[2:Rew:60780.0,609.0] || s_t(skc5,u,reflect(xb,skc4,skc5))* s_col(skc3,skc4,u) -> s_col(skc3,skc4,reflect(skc3,skc4,skc5))*. % 161.28/161.49 60834[2:Rew:60780.0,358.0] || -> equal(reflect(skc4,xb,reflect(skc4,xb,u)),u)**. % 161.28/161.49 60840[2:Rew:60780.0,476.0] || -> equal(reflect(xb,skc4,reflect(xb,skc4,u)),u)**. % 161.28/161.49 60995[2:Rew:60780.0,604.0] || -> s_col(xb,skc4,reflect(xb,skc4,skc5)) samesideline(skc5,reflect(skc3,skc4,skc5),skc3,skc4)*. % 161.28/161.49 61105[2:Rew:60780.0,60995.1] || -> s_col(xb,skc4,reflect(xb,skc4,skc5)) samesideline(skc5,reflect(xb,skc4,skc5),xb,skc4)*. % 161.28/161.49 61140[2:Rew:60780.0,60816.2,60780.0,60816.1] || s_t(skc5,u,reflect(xb,skc4,skc5))* s_col(xb,skc4,u) -> s_col(xb,skc4,reflect(xb,skc4,skc5))*. % 161.28/161.49 61324[3:Spt:267.3] || -> equal(xb,xa)**. % 161.28/161.49 61327[3:Rew:61324.0,60714.0] || equal(skc4,xa)** -> . % 161.28/161.49 61373[3:Rew:61324.0,60815.0] || equal(reflect(xa,skc4,skc5),skc5)** -> . % 161.28/161.49 61374[3:Rew:61324.0,61140.0] || s_t(skc5,u,reflect(xa,skc4,skc5))* s_col(xb,skc4,u) -> s_col(xb,skc4,reflect(xb,skc4,skc5))*. % 161.28/161.49 61415[3:Rew:61324.0,60840.0] || -> equal(reflect(xa,skc4,reflect(xa,skc4,u)),u)**. % 161.28/161.49 61550[3:Rew:61324.0,61105.0] || -> s_col(xa,skc4,reflect(xa,skc4,skc5)) samesideline(skc5,reflect(xb,skc4,skc5),xb,skc4)*. % 161.28/161.49 61660[3:Rew:61324.0,61550.1] || -> s_col(xa,skc4,reflect(xa,skc4,skc5)) samesideline(skc5,reflect(xa,skc4,skc5),xa,skc4)*. % 161.28/161.49 61695[3:Rew:61324.0,61374.2,61324.0,61374.1] || s_t(skc5,u,reflect(xa,skc4,skc5))* s_col(xa,skc4,u) -> s_col(xa,skc4,reflect(xa,skc4,skc5))*. % 161.28/161.49 67698[4:Spt:61660.0] || -> s_col(xa,skc4,reflect(xa,skc4,skc5))*. % 161.28/161.49 67714[4:Res:67698.0,3509.0] || -> equal(skc4,xa) equal(reflect(xa,skc4,skc5),skc5)**. % 161.28/161.49 67717[4:MRR:67714.0,67714.1,61327.0,61373.0] || -> . % 161.28/161.49 67723[4:Spt:67717.0,61660.0,67698.0] || s_col(xa,skc4,reflect(xa,skc4,skc5))* -> . % 161.28/161.49 67724[4:Spt:67717.0,61660.1] || -> samesideline(skc5,reflect(xa,skc4,skc5),xa,skc4)*. % 161.28/161.49 67726[4:MRR:61695.2,67723.0] || s_t(skc5,u,reflect(xa,skc4,skc5))* s_col(xa,skc4,u) -> . % 161.28/161.49 67944[4:Res:4311.1,67726.0] || equal(reflect(xa,skc4,skc5),u) s_col(xa,skc4,midpoint(u,skc5))* -> . % 161.28/161.49 67970[4:MRR:67944.1,8585.1] || equal(reflect(xa,skc4,skc5),u)* -> . % 161.28/161.49 67971[4:UnC:67970.0,61415.0] || -> . % 161.28/161.49 67976[3:Spt:67971.0,267.3,61324.0] || equal(xb,xa)** -> . % 161.28/161.49 67977[3:Spt:67971.0,267.0,267.1,267.2,267.4,267.5] || s_col(xa,xb,xq) s_col(xa,xb,xp) perp(xc,xd,xa,xb) -> equal(xq,xp) perp(xc,xd,xp,xq)*. % 161.28/161.49 73878[4:Spt:61105.0] || -> s_col(xb,skc4,reflect(xb,skc4,skc5))*. % 161.28/161.49 73894[4:Res:73878.0,3509.0] || -> equal(skc4,xb) equal(reflect(xb,skc4,skc5),skc5)**. % 161.28/161.49 73897[4:MRR:73894.0,73894.1,60714.0,60815.0] || -> . % 161.28/161.49 73903[4:Spt:73897.0,61105.0,73878.0] || s_col(xb,skc4,reflect(xb,skc4,skc5))* -> . % 161.28/161.49 73904[4:Spt:73897.0,61105.1] || -> samesideline(skc5,reflect(xb,skc4,skc5),xb,skc4)*. % 161.28/161.49 73906[4:MRR:61140.2,73903.0] || s_t(skc5,u,reflect(xb,skc4,skc5))* s_col(xb,skc4,u) -> . % 161.28/161.49 74124[4:Res:4311.1,73906.0] || equal(reflect(xb,skc4,skc5),u) s_col(xb,skc4,midpoint(u,skc5))* -> . % 161.28/161.49 74150[4:MRR:74124.1,8585.1] || equal(reflect(xb,skc4,skc5),u)* -> . % 161.28/161.49 74151[4:UnC:74150.0,60834.0] || -> . % 161.28/161.49 74156[2:Spt:74151.0,376.1,60780.0] || equal(skc3,xb)** -> . % 161.28/161.49 74157[2:Spt:74151.0,376.0,376.2] || s_t(skc3,skc4,u) -> sameside(skc4,skc3,u)*. % 161.28/161.49 74175[3:Spt:578.3] || -> equal(skc5,skc4)**. % 161.28/161.49 74185[3:Rew:74175.0,11.0] || s_col(skc3,skc4,skc4)* -> . % 161.28/161.49 74226[3:MRR:74185.0,1223.0] || -> . % 161.28/161.49 74245[3:Spt:74226.0,578.3,74175.0] || equal(skc5,skc4)** -> . % 161.28/161.49 74246[3:Spt:74226.0,578.0,578.1,578.2] || sameside(skc3,skc4,u)* s_t(skc5,skc4,u) -> equal(skc4,u). % 161.28/161.49 80000[4:Spt:604.0] || -> s_col(skc3,skc4,reflect(skc3,skc4,skc5))*. % 161.28/161.49 80016[4:Res:80000.0,3509.0] || -> equal(skc4,skc3) equal(reflect(skc3,skc4,skc5),skc5)**. % 161.28/161.49 80019[4:MRR:80016.0,80016.1,1.0,596.0] || -> . % 161.28/161.49 80025[4:Spt:80019.0,604.0,80000.0] || s_col(skc3,skc4,reflect(skc3,skc4,skc5))* -> . % 161.28/161.49 80026[4:Spt:80019.0,604.1] || -> samesideline(skc5,reflect(skc3,skc4,skc5),skc3,skc4)*. % 161.28/161.49 80028[4:MRR:609.2,80025.0] || s_t(skc5,u,reflect(skc3,skc4,skc5))* s_col(skc3,skc4,u) -> . % 161.28/161.49 80262[4:Res:4311.1,80028.0] || equal(reflect(skc3,skc4,skc5),u) s_col(skc3,skc4,midpoint(u,skc5))* -> . % 161.28/161.49 80288[4:MRR:80262.1,8585.1] || equal(reflect(skc3,skc4,skc5),u)* -> . % 161.28/161.49 80289[4:UnC:80288.0,358.0] || -> . % 161.28/161.49 % SZS output end Refutation % 161.28/161.49 Formulae used in the proof : aSatz10_14 aSatz4_12b aSatz7_10b aSatz8_22 aSatz7_7 aSatz4_11d aSatz7_2 aSatz7_13 aSatz8_2 d_Defn7_1 aSatz7_6 aSatz7_18 d_Defn8_11a aSatz8_18 aSatz10_2a aSatz10_6 d_Defn8_1 aSatz8_7 aSatz10_8a aSatz10_8b d_Defn6_1 d_Defn8_11b aSatz6_15c aLemma9_13f d_Defn9_1 aExtPerp6 % 161.28/161.49 %------------------------------------------------------------------------------