%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GEO169+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n007.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:22:52 EDT 2022 % Result : Theorem 0.86s 1.07s % Output : Refutation 0.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : GEO169+1 : TPTP v8.1.0. Released v3.2.0. % 0.07/0.14 % Command : run_spass %d %s % 0.12/0.35 % Computer : n007.cluster.edu % 0.12/0.35 % Model : x86_64 x86_64 % 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.35 % Memory : 8042.1875MB % 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.35 % CPULimit : 300 % 0.12/0.35 % WCLimit : 600 % 0.12/0.35 % DateTime : Sat Jun 18 15:20:43 EDT 2022 % 0.12/0.35 % CPUTime : % 0.86/1.07 % 0.86/1.07 SPASS V 3.9 % 0.86/1.07 SPASS beiseite: Proof found. % 0.86/1.07 % SZS status Theorem % 0.86/1.07 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.86/1.07 SPASS derived 9471 clauses, backtracked 1680 clauses, performed 173 splits and kept 6425 clauses. % 0.86/1.07 SPASS allocated 89235 KBytes. % 0.86/1.07 SPASS spent 0:00:00.71 on the problem. % 0.86/1.07 0:00:00.04 for the input. % 0.86/1.07 0:00:00.03 for the FLOTTER CNF translation. % 0.86/1.07 0:00:00.07 for inferences. % 0.86/1.07 0:00:00.02 for the backtracking. % 0.86/1.07 0:00:00.49 for the reduction. % 0.86/1.07 % 0.86/1.07 % 0.86/1.07 Here is a proof with depth 15, length 857 : % 0.86/1.07 % SZS output start Refutation % 0.86/1.07 1[0:Inp] || goal*+ -> . % 0.86/1.07 2[0:Inp] || -> incident(a1,a1b1)*. % 0.86/1.07 3[0:Inp] || -> incident(b1,a1b1)*. % 0.86/1.07 4[0:Inp] || -> incident(a2,a2b2)*. % 0.86/1.07 5[0:Inp] || -> incident(b2,a2b2)*. % 0.86/1.07 6[0:Inp] || -> incident(a1,a1c1)*. % 0.86/1.07 7[0:Inp] || -> incident(c1,a1c1)*. % 0.86/1.07 8[0:Inp] || -> incident(a2,a2c2)*. % 0.86/1.07 9[0:Inp] || -> incident(c2,a2c2)*. % 0.86/1.07 10[0:Inp] || -> incident(c1,b1c1)*. % 0.86/1.07 11[0:Inp] || -> incident(b1,b1c1)*. % 0.86/1.07 12[0:Inp] || -> incident(c2,b2c2)*. % 0.86/1.07 13[0:Inp] || -> incident(b2,b2c2)*. % 0.86/1.07 14[0:Inp] || -> incident(o,oa)*. % 0.86/1.07 15[0:Inp] || -> incident(o,ob)*. % 0.86/1.07 16[0:Inp] || -> incident(o,oc)*. % 0.86/1.07 17[0:Inp] || -> incident(a1,oa)*. % 0.86/1.07 18[0:Inp] || -> incident(a2,oa)*. % 0.86/1.07 19[0:Inp] || -> incident(b1,ob)*. % 0.86/1.07 20[0:Inp] || -> incident(b2,ob)*. % 0.86/1.07 21[0:Inp] || -> incident(c1,oc)*. % 0.86/1.07 22[0:Inp] || -> incident(c2,oc)*. % 0.86/1.07 23[0:Inp] || -> incident(bc,b1c1)*. % 0.86/1.07 24[0:Inp] || -> incident(bc,b2c2)*. % 0.86/1.07 25[0:Inp] || -> incident(ac,a1c1)*. % 0.86/1.07 26[0:Inp] || -> incident(ac,a2c2)*. % 0.86/1.07 27[0:Inp] || -> incident(ab,a1b1)*. % 0.86/1.07 28[0:Inp] || -> incident(ab,a2b2)*. % 0.86/1.07 29[0:Inp] || point_equal(a2,a1) -> goal*. % 0.86/1.07 30[0:Inp] || point_equal(b2,b1) -> goal*. % 0.86/1.07 31[0:Inp] || point_equal(c2,c1) -> goal*. % 0.86/1.07 32[0:Inp] || line_equal(b1c1,b2c2) -> goal*. % 0.86/1.07 33[0:Inp] || line_equal(a1c1,a2c2) -> goal*. % 0.86/1.07 34[0:Inp] || line_equal(a1b1,a2b2) -> goal*. % 0.86/1.07 35[0:Inp] || -> incident(b2,a1c1) incident(a1,b2c2)*. % 0.86/1.07 36[0:Inp] || -> incident(c2,a1b1) incident(b1,a2c2)*. % 0.86/1.07 37[0:Inp] || -> incident(a2,b1c1) incident(c1,a2b2)*. % 0.86/1.07 39[0:Inp] || point_equal(u,v)*+ -> point_equal(v,u). % 0.86/1.07 40[0:Inp] || incident(u,v)*+ -> line_equal(v,v). % 0.86/1.07 41[0:Inp] || line_equal(u,v)*+ -> line_equal(v,u). % 0.86/1.07 42[0:Inp] || point_equal(u,v)* point_equal(v,w)* -> point_equal(u,w)*. % 0.86/1.07 43[0:Inp] || line_equal(u,v)* line_equal(v,w)* -> line_equal(u,w)*. % 0.86/1.07 44[0:Inp] || incident(u,v)* point_equal(w,u)*+ -> incident(w,v)*. % 0.86/1.07 45[0:Inp] || line_equal(u,v)*+ incident(w,u)* -> incident(w,v)*. % 0.86/1.07 46[0:Inp] || incident(a1,b2c2)* incident(b1,a2c2) incident(c1,a2b2) -> goal. % 0.86/1.07 47[0:Inp] || incident(a2,b1c1)* incident(b2,a1c1) incident(c2,a1b1) -> goal. % 0.86/1.07 48[0:Inp] || incident(a1,u)* incident(b1,u) incident(c1,u) -> goal. % 0.86/1.07 49[0:Inp] || incident(a2,u)* incident(b2,u) incident(c2,u) -> goal. % 0.86/1.07 50[0:Inp] || line_equal(u,u) incident(bc,u)* incident(ac,u) incident(ab,u) -> goal. % 0.86/1.07 51[0:Inp] || incident(u,v)*+ incident(u,w)* incident(x,w)* incident(x,v)* -> line_equal(v,w)* point_equal(x,u)*. % 0.86/1.07 52[0:MRR:34.1,1.0] || line_equal(a1b1,a2b2)*r+ -> . % 0.86/1.07 53[0:MRR:33.1,1.0] || line_equal(a1c1,a2c2)*r+ -> . % 0.86/1.07 54[0:MRR:32.1,1.0] || line_equal(b1c1,b2c2)*r+ -> . % 0.86/1.07 55[0:MRR:31.1,1.0] || point_equal(c2,c1)*r+ -> . % 0.86/1.07 56[0:MRR:30.1,1.0] || point_equal(b2,b1)*r+ -> . % 0.86/1.07 57[0:MRR:29.1,1.0] || point_equal(a2,a1)*r+ -> . % 0.86/1.07 58[0:MRR:49.3,1.0] || incident(c2,u)+ incident(b2,u) incident(a2,u)* -> . % 0.86/1.07 59[0:MRR:48.3,1.0] || incident(c1,u)+ incident(b1,u) incident(a1,u)* -> . % 0.86/1.07 60[0:MRR:47.3,1.0] || incident(c2,a1b1) incident(b2,a1c1) incident(a2,b1c1)* -> . % 0.86/1.07 61[0:MRR:46.3,1.0] || incident(c1,a2b2) incident(b1,a2c2) incident(a1,b2c2)* -> . % 0.86/1.07 62[0:MRR:50.0,50.4,40.1,1.0] || incident(ab,u)+ incident(ac,u) incident(bc,u)* -> . % 0.86/1.07 63[0:Res:51.5,52.0] || incident(u,a1b1)+ incident(u,a2b2)* incident(v,a2b2)* incident(v,a1b1) -> point_equal(v,u)*. % 0.86/1.07 65[0:Res:51.5,53.0] || incident(u,a1c1)+ incident(u,a2c2)* incident(v,a2c2)* incident(v,a1c1) -> point_equal(v,u)*. % 0.86/1.07 66[0:Res:41.1,53.0] || line_equal(a2c2,a1c1)*l+ -> . % 0.86/1.07 67[0:Res:51.5,54.0] || incident(u,b1c1)+ incident(u,b2c2)* incident(v,b2c2)* incident(v,b1c1) -> point_equal(v,u)*. % 0.86/1.07 68[0:Res:41.1,54.0] || line_equal(b2c2,b1c1)*l+ -> . % 0.86/1.07 69[0:Res:51.4,55.0] || incident(c1,u)*+ incident(c1,v)* incident(c2,v) incident(c2,u) -> line_equal(u,v)*. % 0.86/1.07 70[0:Res:39.1,55.0] || point_equal(c1,c2)*l+ -> . % 0.86/1.07 71[0:Res:51.4,56.0] || incident(b1,u)*+ incident(b1,v)* incident(b2,v) incident(b2,u) -> line_equal(u,v)*. % 0.86/1.07 72[0:Res:39.1,56.0] || point_equal(b1,b2)*l+ -> . % 0.86/1.07 73[0:Res:51.4,57.0] || incident(a1,u)*+ incident(a1,v)* incident(a2,v) incident(a2,u) -> line_equal(u,v)*. % 0.86/1.07 74[0:Res:39.1,57.0] || point_equal(a1,a2)*l+ -> . % 0.86/1.07 75[0:Res:18.0,58.0] || incident(c2,oa)+ incident(b2,oa)* -> . % 0.86/1.07 76[0:Res:8.0,58.0] || incident(b2,a2c2)* incident(c2,a2c2) -> . % 0.86/1.07 77[0:Res:4.0,58.0] || incident(b2,a2b2)* incident(c2,a2b2) -> . % 0.86/1.07 78[0:Res:20.0,58.1] || incident(c2,ob)+ incident(a2,ob)* -> . % 0.86/1.07 79[0:Res:13.0,58.1] || incident(a2,b2c2)* incident(c2,b2c2) -> . % 0.86/1.07 85[0:Res:6.0,59.0] || incident(b1,a1c1)* incident(c1,a1c1) -> . % 0.86/1.07 87[0:Res:19.0,59.1] || incident(c1,ob)+ incident(a1,ob)* -> . % 0.86/1.07 88[0:Res:11.0,59.1] || incident(a1,b1c1)* incident(c1,b1c1) -> . % 0.86/1.07 90[0:Res:21.0,59.2] || incident(b1,oc)+ incident(a1,oc)* -> . % 0.86/1.07 95[0:Res:26.0,62.1] || incident(ab,a2c2)+ incident(bc,a2c2)* -> . % 0.86/1.07 97[0:Res:28.0,62.2] || incident(ac,a2b2)+ incident(bc,a2b2)* -> . % 0.86/1.07 98[0:Res:27.0,62.2] || incident(ac,a1b1)+ incident(bc,a1b1)* -> . % 0.86/1.07 99[0:MRR:76.1,9.0] || incident(b2,a2c2)*+ -> . % 0.86/1.07 100[0:MRR:77.0,5.0] || incident(c2,a2b2)*+ -> . % 0.86/1.07 101[0:MRR:79.1,12.0] || incident(a2,b2c2)*+ -> . % 0.86/1.07 102[0:MRR:85.1,7.0] || incident(b1,a1c1)*+ -> . % 0.86/1.07 104[0:MRR:88.1,10.0] || incident(a1,b1c1)*+ -> . % 0.86/1.07 105[1:Spt:37.0] || -> incident(a2,b1c1)*. % 0.86/1.07 106[1:MRR:60.2,105.0] || incident(c2,a1b1) incident(b2,a1c1)* -> . % 0.86/1.07 107[2:Spt:36.0] || -> incident(c2,a1b1)*. % 0.86/1.07 108[2:MRR:106.0,107.0] || incident(b2,a1c1)*+ -> . % 0.86/1.07 109[2:MRR:35.0,108.0] || -> incident(a1,b2c2)*. % 0.86/1.07 218[0:Res:21.0,69.0] || incident(c1,u)* incident(c2,u) incident(c2,oc) -> line_equal(oc,u). % 0.86/1.07 219[0:Res:10.0,69.0] || incident(c1,u)*+ incident(c2,u) incident(c2,b1c1) -> line_equal(b1c1,u). % 0.86/1.07 221[0:MRR:218.2,22.0] || incident(c1,u)*+ incident(c2,u) -> line_equal(oc,u). % 0.86/1.07 223[0:Res:10.0,221.0] || incident(c2,b1c1)*+ -> line_equal(oc,b1c1). % 0.86/1.07 224[0:Res:7.0,221.0] || incident(c2,a1c1)*+ -> line_equal(oc,a1c1). % 0.86/1.07 231[0:Res:22.0,51.0] || incident(c2,u)*+ incident(v,u)* incident(v,oc)* -> line_equal(oc,u) point_equal(v,c2). % 0.86/1.07 232[0:Res:21.0,51.0] || incident(c1,u)*+ incident(v,u)* incident(v,oc)* -> line_equal(oc,u) point_equal(v,c1). % 0.86/1.07 233[0:Res:16.0,51.0] || incident(o,u)*+ incident(v,u)* incident(v,oc)* -> line_equal(oc,u) point_equal(v,o). % 0.86/1.07 235[0:Res:19.0,51.0] || incident(b1,u)*+ incident(v,u)* incident(v,ob)* -> line_equal(ob,u) point_equal(v,b1). % 0.86/1.07 236[0:Res:15.0,51.0] || incident(o,u)*+ incident(v,u)* incident(v,ob)* -> line_equal(ob,u) point_equal(v,o). % 0.86/1.07 237[0:Res:18.0,51.0] || incident(a2,u)*+ incident(v,u)* incident(v,oa)* -> line_equal(oa,u) point_equal(v,a2). % 0.86/1.07 238[0:Res:17.0,51.0] || incident(a1,u)*+ incident(v,u)* incident(v,oa)* -> line_equal(oa,u) point_equal(v,a1). % 0.86/1.07 239[0:Res:14.0,51.0] || incident(o,u)*+ incident(v,u)* incident(v,oa)* -> line_equal(oa,u) point_equal(v,o). % 0.86/1.07 240[0:Res:13.0,51.0] || incident(b2,u)*+ incident(v,u)* incident(v,b2c2)* -> line_equal(b2c2,u) point_equal(v,b2). % 0.86/1.07 241[0:Res:12.0,51.0] || incident(c2,u)*+ incident(v,u)* incident(v,b2c2)* -> line_equal(b2c2,u) point_equal(v,c2). % 0.86/1.07 242[2:Res:109.0,51.0] || incident(a1,u)*+ incident(v,u)* incident(v,b2c2)* -> line_equal(b2c2,u) point_equal(v,a1). % 0.86/1.07 243[0:Res:11.0,51.0] || incident(b1,u)*+ incident(v,u)* incident(v,b1c1)* -> line_equal(b1c1,u) point_equal(v,b1). % 0.86/1.07 244[0:Res:10.0,51.0] || incident(c1,u)*+ incident(v,u)* incident(v,b1c1)* -> line_equal(b1c1,u) point_equal(v,c1). % 0.86/1.07 246[0:Res:9.0,51.0] || incident(c2,u)*+ incident(v,u)* incident(v,a2c2)* -> line_equal(a2c2,u) point_equal(v,c2). % 0.86/1.07 247[0:Res:8.0,51.0] || incident(a2,u)*+ incident(v,u)* incident(v,a2c2)* -> line_equal(a2c2,u) point_equal(v,a2). % 0.86/1.07 248[0:Res:7.0,51.0] || incident(c1,u)*+ incident(v,u)* incident(v,a1c1)* -> line_equal(a1c1,u) point_equal(v,c1). % 0.86/1.07 250[0:Res:5.0,51.0] || incident(b2,u)*+ incident(v,u)* incident(v,a2b2)* -> line_equal(a2b2,u) point_equal(v,b2). % 0.86/1.07 251[0:Res:4.0,51.0] || incident(a2,u)*+ incident(v,u)* incident(v,a2b2)* -> line_equal(a2b2,u) point_equal(v,a2). % 0.86/1.07 252[0:Res:3.0,51.0] || incident(b1,u)*+ incident(v,u)* incident(v,a1b1)* -> line_equal(a1b1,u) point_equal(v,b1). % 0.86/1.07 253[0:Res:2.0,51.0] || incident(a1,u)*+ incident(v,u)* incident(v,a1b1)* -> line_equal(a1b1,u) point_equal(v,a1). % 0.86/1.07 260[0:Res:19.0,71.0] || incident(b1,u)* incident(b2,u) incident(b2,ob) -> line_equal(ob,u). % 0.86/1.07 263[0:MRR:260.2,20.0] || incident(b1,u)*+ incident(b2,u) -> line_equal(ob,u). % 0.86/1.07 265[0:Res:11.0,263.0] || incident(b2,b1c1)*+ -> line_equal(ob,b1c1). % 0.86/1.07 266[0:Res:3.0,263.0] || incident(b2,a1b1)*+ -> line_equal(ob,a1b1). % 0.86/1.07 267[0:Res:17.0,73.0] || incident(a1,u)* incident(a2,u) incident(a2,oa) -> line_equal(oa,u). % 0.86/1.07 271[0:MRR:267.2,18.0] || incident(a1,u)*+ incident(a2,u) -> line_equal(oa,u). % 0.86/1.07 276[0:Res:21.0,219.0] || incident(c2,oc) incident(c2,b1c1)* -> line_equal(b1c1,oc). % 0.86/1.07 279[0:MRR:276.0,22.0] || incident(c2,b1c1)*+ -> line_equal(b1c1,oc). % 0.86/1.07 281[0:Res:27.0,63.0] || incident(ab,a2b2)* incident(u,a2b2)* incident(u,a1b1) -> point_equal(u,ab). % 0.86/1.07 285[0:MRR:281.0,28.0] || incident(u,a2b2)*+ incident(u,a1b1) -> point_equal(u,ab). % 0.86/1.07 288[0:Res:4.0,285.0] || incident(a2,a1b1)*+ -> point_equal(a2,ab). % 0.86/1.07 289[0:Res:25.0,65.0] || incident(ac,a2c2)* incident(u,a2c2)* incident(u,a1c1) -> point_equal(u,ac). % 0.86/1.07 291[0:Res:6.0,65.0] || incident(a1,a2c2)*+ incident(u,a2c2)* incident(u,a1c1) -> point_equal(u,a1). % 0.86/1.07 292[0:MRR:289.0,26.0] || incident(u,a2c2)*+ incident(u,a1c1) -> point_equal(u,ac). % 0.86/1.07 294[0:Res:9.0,292.0] || incident(c2,a1c1)*+ -> point_equal(c2,ac). % 0.86/1.07 295[0:Res:8.0,292.0] || incident(a2,a1c1)*+ -> point_equal(a2,ac). % 0.86/1.07 298[0:Res:10.0,67.0] || incident(c1,b2c2)*+ incident(u,b2c2)* incident(u,b1c1) -> point_equal(u,c1). % 0.86/1.07 311[2:Res:109.0,253.0] || incident(u,b2c2)*+ incident(u,a1b1) -> line_equal(a1b1,b2c2) point_equal(u,a1). % 0.86/1.07 320[0:Res:19.0,252.0] || incident(u,ob)+ incident(u,a1b1)* -> line_equal(a1b1,ob) point_equal(u,b1). % 0.86/1.07 330[0:Res:18.0,251.0] || incident(u,oa)+ incident(u,a2b2)* -> line_equal(a2b2,oa) point_equal(u,a2). % 0.86/1.07 332[0:Res:8.0,251.0] || incident(u,a2c2)*+ incident(u,a2b2) -> line_equal(a2b2,a2c2) point_equal(u,a2). % 0.86/1.07 341[0:Res:20.0,250.0] || incident(u,ob)+ incident(u,a2b2)* -> line_equal(a2b2,ob) point_equal(u,b2). % 0.86/1.07 342[0:Res:13.0,250.0] || incident(u,b2c2)*+ incident(u,a2b2) -> line_equal(a2b2,b2c2) point_equal(u,b2). % 0.86/1.07 354[3:Spt:311.0,311.1,311.3] || incident(u,b2c2)*+ incident(u,a1b1) -> point_equal(u,a1). % 0.86/1.07 356[3:Res:13.0,354.0] || incident(b2,a1b1)*+ -> point_equal(b2,a1). % 0.86/1.07 357[3:Res:12.0,354.0] || incident(c2,a1b1)* -> point_equal(c2,a1). % 0.86/1.07 359[3:MRR:357.0,107.0] || -> point_equal(c2,a1)*r. % 0.86/1.07 360[0:Res:21.0,248.0] || incident(u,oc)+ incident(u,a1c1)* -> line_equal(a1c1,oc) point_equal(u,c1). % 0.86/1.07 361[0:Res:10.0,248.0] || incident(u,b1c1)*+ incident(u,a1c1) -> line_equal(a1c1,b1c1) point_equal(u,c1). % 0.86/1.07 364[3:Res:359.0,44.1] || incident(a1,u)*+ -> incident(c2,u). % 0.86/1.07 365[3:Res:359.0,39.0] || -> point_equal(a1,c2)*l. % 0.86/1.07 369[3:Res:17.0,364.0] || -> incident(c2,oa)*. % 0.86/1.07 371[3:Res:6.0,364.0] || -> incident(c2,a1c1)*. % 0.86/1.07 373[3:MRR:75.0,369.0] || incident(b2,oa)*+ -> . % 0.86/1.07 374[3:MRR:224.0,371.0] || -> line_equal(oc,a1c1)*r. % 0.86/1.07 379[3:MRR:294.0,371.0] || -> point_equal(c2,ac)*r. % 0.86/1.07 391[3:Res:365.0,44.1] || incident(c2,u)+ -> incident(a1,u)*. % 0.86/1.07 400[3:Res:9.0,391.0] || -> incident(a1,a2c2)*. % 0.86/1.07 415[3:Res:400.0,292.0] || incident(a1,a1c1)* -> point_equal(a1,ac). % 0.86/1.07 421[3:Res:400.0,271.0] || incident(a2,a2c2)* -> line_equal(oa,a2c2). % 0.86/1.07 426[3:MRR:415.0,6.0] || -> point_equal(a1,ac)*r. % 0.86/1.07 427[3:MRR:421.0,8.0] || -> line_equal(oa,a2c2)*r. % 0.86/1.07 432[3:Res:374.0,45.0] || incident(u,oc)+ -> incident(u,a1c1)*. % 0.86/1.07 437[3:Res:16.0,432.0] || -> incident(o,a1c1)*. % 0.86/1.07 444[0:Res:18.0,247.0] || incident(u,oa)+ incident(u,a2c2)* -> line_equal(a2c2,oa) point_equal(u,a2). % 0.86/1.07 445[1:Res:105.0,247.0] || incident(u,b1c1)+ incident(u,a2c2)* -> line_equal(a2c2,b1c1) point_equal(u,a2). % 0.86/1.07 464[3:Res:379.0,39.0] || -> point_equal(ac,c2)*l. % 0.86/1.07 467[0:Res:22.0,246.0] || incident(u,oc)+ incident(u,a2c2)* -> line_equal(a2c2,oc) point_equal(u,c2). % 0.86/1.07 469[0:Res:12.0,246.0] || incident(u,b2c2)*+ incident(u,a2c2) -> line_equal(a2c2,b2c2) point_equal(u,c2). % 0.86/1.07 479[3:NCh:42.2,42.1,426.0,44.1] || incident(ac,u)* point_equal(v,a1)+ -> incident(v,u)*. % 0.86/1.07 485[3:Res:427.0,45.0] || incident(u,oa)+ -> incident(u,a2c2)*. % 0.86/1.07 492[0:Res:21.0,244.0] || incident(u,oc)+ incident(u,b1c1)* -> line_equal(b1c1,oc) point_equal(u,c1). % 0.86/1.07 498[3:Res:14.0,485.0] || -> incident(o,a2c2)*. % 0.86/1.07 501[3:Res:498.0,292.0] || incident(o,a1c1)* -> point_equal(o,ac). % 0.86/1.07 505[3:MRR:501.0,437.0] || -> point_equal(o,ac)*r. % 0.86/1.07 506[3:Res:464.0,44.1] || incident(c2,u)+ -> incident(ac,u)*. % 0.86/1.07 513[3:Res:369.0,506.0] || -> incident(ac,oa)*. % 0.86/1.07 517[3:Res:107.0,506.0] || -> incident(ac,a1b1)*. % 0.86/1.07 539[0:Res:19.0,243.0] || incident(u,ob)+ incident(u,b1c1)* -> line_equal(b1c1,ob) point_equal(u,b1). % 0.86/1.07 567[2:Res:17.0,242.0] || incident(u,oa)+ incident(u,b2c2)* -> line_equal(b2c2,oa) point_equal(u,a1). % 0.86/1.07 573[3:Res:505.0,44.1] || incident(ac,u)*+ -> incident(o,u). % 0.86/1.07 574[3:Res:505.0,39.0] || -> point_equal(ac,o)*l. % 0.86/1.07 584[3:Res:517.0,573.0] || -> incident(o,a1b1)*. % 0.86/1.07 594[0:Res:22.0,241.0] || incident(u,oc)+ incident(u,b2c2)* -> line_equal(b2c2,oc) point_equal(u,c2). % 0.86/1.07 604[3:OCh:42.1,42.0,574.0,426.0] || -> point_equal(a1,o)*l. % 0.86/1.07 655[0:Res:20.0,240.0] || incident(u,ob)+ incident(u,b2c2)* -> line_equal(b2c2,ob) point_equal(u,b2). % 0.86/1.07 683[0:Res:15.0,239.0] || incident(u,ob)+ incident(u,oa)* -> line_equal(oa,ob) point_equal(u,o). % 0.86/1.07 696[3:NCh:42.2,42.0,604.0,44.1] || incident(u,v)* point_equal(o,u)+ -> incident(a1,v)*. % 0.86/1.07 710[0:Res:6.0,238.0] || incident(u,a1c1)*+ incident(u,oa) -> line_equal(oa,a1c1) point_equal(u,a1). % 0.86/1.07 711[0:Res:2.0,238.0] || incident(u,a1b1)*+ incident(u,oa) -> line_equal(oa,a1b1) point_equal(u,a1). % 0.86/1.07 719[1:Res:105.0,237.0] || incident(u,b1c1)*+ incident(u,oa) -> line_equal(oa,b1c1) point_equal(u,a2). % 0.86/1.07 723[0:Res:16.0,236.0] || incident(u,oc)+ incident(u,ob)* -> line_equal(ob,oc) point_equal(u,o). % 0.86/1.07 732[0:Res:11.0,235.0] || incident(u,b1c1)*+ incident(u,ob) -> line_equal(ob,b1c1) point_equal(u,b1). % 0.86/1.07 733[0:Res:3.0,235.0] || incident(u,a1b1)*+ incident(u,ob) -> line_equal(ob,a1b1) point_equal(u,b1). % 0.86/1.07 770[0:Res:15.0,233.0] || incident(u,ob)*+ incident(u,oc) -> line_equal(oc,ob) point_equal(u,o). % 0.86/1.07 771[0:Res:14.0,233.0] || incident(u,oa)*+ incident(u,oc) -> line_equal(oc,oa) point_equal(u,o). % 0.86/1.07 794[0:Res:7.0,232.0] || incident(u,a1c1)*+ incident(u,oc) -> line_equal(oc,a1c1) point_equal(u,c1). % 0.86/1.07 825[0:Res:9.0,231.0] || incident(u,a2c2)*+ incident(u,oc) -> line_equal(oc,a2c2) point_equal(u,c2). % 0.86/1.07 1132[4:Spt:320.0,320.1,320.3] || incident(u,ob)+ incident(u,a1b1)* -> point_equal(u,b1). % 0.86/1.07 1135[4:Res:15.0,1132.0] || incident(o,a1b1)* -> point_equal(o,b1). % 0.86/1.07 1140[4:MRR:1135.0,584.0] || -> point_equal(o,b1)*r. % 0.86/1.07 1156[4:Res:1140.0,696.1] || incident(b1,u) -> incident(a1,u)*. % 0.86/1.07 1173[4:MRR:59.2,1156.1] || incident(c1,u)+ incident(b1,u)* -> . % 0.86/1.07 1179[4:Res:10.0,1173.0] || incident(b1,b1c1)* -> . % 0.86/1.07 1181[4:MRR:1179.0,11.0] || -> . % 0.86/1.07 1182[4:Spt:1181.0,320.2] || -> line_equal(a1b1,ob)*l. % 0.86/1.07 1183[4:Res:1182.0,41.0] || -> line_equal(ob,a1b1)*r. % 0.86/1.07 1210[4:Res:1183.0,45.0] || incident(u,ob)+ -> incident(u,a1b1)*. % 0.86/1.07 1218[4:Res:20.0,1210.0] || -> incident(b2,a1b1)*. % 0.86/1.07 1226[4:MRR:356.0,1218.0] || -> point_equal(b2,a1)*r. % 0.86/1.07 1261[4:Res:1226.0,479.1] || incident(ac,u)*+ -> incident(b2,u). % 0.86/1.07 1292[4:Res:513.0,1261.0] || -> incident(b2,oa)*. % 0.86/1.07 1297[4:MRR:1292.0,373.0] || -> . % 0.86/1.07 1298[3:Spt:1297.0,311.2] || -> line_equal(a1b1,b2c2)*r. % 0.86/1.07 1299[3:Res:1298.0,41.0] || -> line_equal(b2c2,a1b1)*l. % 0.86/1.07 1300[3:Res:1298.0,45.0] || incident(u,a1b1)+ -> incident(u,b2c2)*. % 0.86/1.07 1311[3:Res:3.0,1300.0] || -> incident(b1,b2c2)*. % 0.86/1.07 1328[3:Res:1311.0,263.0] || incident(b2,b2c2)* -> line_equal(ob,b2c2). % 0.86/1.07 1334[3:MRR:1328.0,13.0] || -> line_equal(ob,b2c2)*r. % 0.86/1.07 1338[3:Res:1299.0,45.0] || incident(u,b2c2)*+ -> incident(u,a1b1). % 0.86/1.07 1343[3:Res:24.0,1338.0] || -> incident(bc,a1b1)*. % 0.86/1.07 1349[3:MRR:98.1,1343.0] || incident(ac,a1b1)*+ -> . % 0.86/1.07 1380[3:Res:1334.0,45.0] || incident(u,ob)+ -> incident(u,b2c2)*. % 0.86/1.07 1395[3:Res:15.0,1380.0] || -> incident(o,b2c2)*. % 0.86/1.07 1702[4:Spt:567.0,567.1,567.3] || incident(u,oa)+ incident(u,b2c2)* -> point_equal(u,a1). % 0.86/1.07 1705[4:Res:14.0,1702.0] || incident(o,b2c2)* -> point_equal(o,a1). % 0.86/1.07 1706[4:MRR:1705.0,1395.0] || -> point_equal(o,a1)*r. % 0.86/1.07 1708[4:Res:1706.0,39.0] || -> point_equal(a1,o)*l. % 0.86/1.07 1727[4:Res:1708.0,44.1] || incident(o,u)+ -> incident(a1,u)*. % 0.86/1.07 1737[5:Spt:594.0,594.1,594.3] || incident(u,oc)+ incident(u,b2c2)* -> point_equal(u,c2). % 0.86/1.07 1740[5:Res:16.0,1737.0] || incident(o,b2c2)* -> point_equal(o,c2). % 0.86/1.07 1742[5:MRR:1740.0,1395.0] || -> point_equal(o,c2)*r. % 0.86/1.07 1743[4:Res:16.0,1727.0] || -> incident(a1,oc)*. % 0.86/1.07 1749[4:MRR:90.1,1743.0] || incident(b1,oc)*+ -> . % 0.86/1.07 1765[5:Res:1742.0,44.1] || incident(c2,u)*+ -> incident(o,u). % 0.86/1.07 1772[5:Res:9.0,1765.0] || -> incident(o,a2c2)*. % 0.86/1.07 1776[5:Res:1772.0,1727.0] || -> incident(a1,a2c2)*. % 0.86/1.07 1783[5:MRR:291.0,1776.0] || incident(u,a2c2)*+ incident(u,a1c1) -> point_equal(u,a1). % 0.86/1.07 1801[5:Res:26.0,1783.0] || incident(ac,a1c1)* -> point_equal(ac,a1). % 0.86/1.07 1806[5:MRR:1801.0,25.0] || -> point_equal(ac,a1)*l. % 0.86/1.07 1909[5:Res:1806.0,44.1] || incident(a1,u)+ -> incident(ac,u)*. % 0.86/1.07 1924[5:Res:2.0,1909.0] || -> incident(ac,a1b1)*. % 0.86/1.07 1927[5:MRR:1924.0,1349.0] || -> . % 0.86/1.07 1928[5:Spt:1927.0,594.2] || -> line_equal(b2c2,oc)*l. % 0.86/1.07 1930[5:Res:1928.0,45.0] || incident(u,b2c2)*+ -> incident(u,oc). % 0.86/1.07 1947[5:Res:1311.0,1930.0] || -> incident(b1,oc)*. % 0.86/1.07 1950[5:MRR:1947.0,1749.0] || -> . % 0.86/1.07 1951[4:Spt:1950.0,567.2] || -> line_equal(b2c2,oa)*l. % 0.86/1.07 1953[4:Res:1951.0,45.0] || incident(u,b2c2)*+ -> incident(u,oa). % 0.86/1.07 1967[4:Res:13.0,1953.0] || -> incident(b2,oa)*. % 0.86/1.07 1968[4:Res:12.0,1953.0] || -> incident(c2,oa)*. % 0.86/1.07 1973[4:MRR:75.1,1967.0] || incident(c2,oa)* -> . % 0.86/1.07 1975[4:MRR:1973.0,1968.0] || -> . % 0.86/1.07 1976[2:Spt:1975.0,36.0,107.0] || incident(c2,a1b1)*+ -> . % 0.86/1.07 1977[2:Spt:1975.0,36.1] || -> incident(b1,a2c2)*. % 0.86/1.07 1978[2:MRR:61.1,1977.0] || incident(c1,a2b2)+ incident(a1,b2c2)* -> . % 0.86/1.07 1981[2:Res:1977.0,243.0] || incident(u,a2c2)*+ incident(u,b1c1) -> line_equal(b1c1,a2c2) point_equal(u,b1). % 0.86/1.07 1991[0:Res:35.1,253.0] || incident(u,b2c2)* incident(u,a1b1) -> incident(b2,a1c1)* line_equal(a1b1,b2c2) point_equal(u,a1). % 0.86/1.07 2031[3:Spt:770.0,770.1,770.3] || incident(u,ob)*+ incident(u,oc) -> point_equal(u,o). % 0.86/1.07 2032[3:Res:20.0,2031.0] || incident(b2,oc)*+ -> point_equal(b2,o). % 0.86/1.07 2033[3:Res:19.0,2031.0] || incident(b1,oc)*+ -> point_equal(b1,o). % 0.86/1.07 2044[4:Spt:711.0,711.1,711.3] || incident(u,a1b1)*+ incident(u,oa) -> point_equal(u,a1). % 0.86/1.07 2046[4:Res:3.0,2044.0] || incident(b1,oa)*+ -> point_equal(b1,a1). % 0.86/1.07 2048[5:Spt:710.0,710.1,710.3] || incident(u,a1c1)*+ incident(u,oa) -> point_equal(u,a1). % 0.86/1.07 2052[6:Spt:444.0,444.1,444.3] || incident(u,oa)+ incident(u,a2c2)* -> point_equal(u,a2). % 0.86/1.07 2055[6:Res:14.0,2052.0] || incident(o,a2c2)*+ -> point_equal(o,a2). % 0.86/1.07 2061[7:Spt:683.0,683.1,683.3] || incident(u,ob)+ incident(u,oa)* -> point_equal(u,o). % 0.86/1.07 2074[8:Spt:732.0,732.1,732.3] || incident(u,b1c1)*+ incident(u,ob) -> point_equal(u,b1). % 0.86/1.07 2078[8:Res:105.0,2074.0] || incident(a2,ob)*+ -> point_equal(a2,b1). % 0.86/1.07 2108[9:Spt:341.0,341.1,341.3] || incident(u,ob)+ incident(u,a2b2)* -> point_equal(u,b2). % 0.86/1.07 2110[9:Res:19.0,2108.0] || incident(b1,a2b2)* -> point_equal(b1,b2). % 0.86/1.07 2111[9:Res:15.0,2108.0] || incident(o,a2b2)*+ -> point_equal(o,b2). % 0.86/1.07 2112[9:MRR:2110.1,72.0] || incident(b1,a2b2)*+ -> . % 0.86/1.07 2118[10:Spt:445.0,445.1,445.3] || incident(u,b1c1)+ incident(u,a2c2)* -> point_equal(u,a2). % 0.86/1.07 2120[10:Res:11.0,2118.0] || incident(b1,a2c2)* -> point_equal(b1,a2). % 0.86/1.07 2123[10:MRR:2120.0,1977.0] || -> point_equal(b1,a2)*l. % 0.86/1.07 2124[10:Res:2123.0,44.1] || incident(a2,u)+ -> incident(b1,u)*. % 0.86/1.07 2132[10:Res:4.0,2124.0] || -> incident(b1,a2b2)*. % 0.86/1.07 2136[10:MRR:2132.0,2112.0] || -> . % 0.86/1.07 2137[10:Spt:2136.0,445.2] || -> line_equal(a2c2,b1c1)*l. % 0.86/1.07 2138[10:Res:2137.0,41.0] || -> line_equal(b1c1,a2c2)*r. % 0.86/1.07 2139[10:Res:2137.0,45.0] || incident(u,a2c2)*+ -> incident(u,b1c1). % 0.86/1.07 2146[10:Res:9.0,2139.0] || -> incident(c2,b1c1)*. % 0.86/1.07 2150[10:MRR:223.0,2146.0] || -> line_equal(oc,b1c1)*r. % 0.86/1.07 2151[10:MRR:279.0,2146.0] || -> line_equal(b1c1,oc)*l. % 0.86/1.07 2184[10:Res:2138.0,45.0] || incident(u,b1c1)+ -> incident(u,a2c2)*. % 0.86/1.07 2223[10:Res:2150.0,45.0] || incident(u,oc)+ -> incident(u,b1c1)*. % 0.86/1.07 2228[10:Res:16.0,2223.0] || -> incident(o,b1c1)*. % 0.86/1.07 2229[10:Res:2228.0,2184.0] || -> incident(o,a2c2)*. % 0.86/1.07 2241[10:MRR:2055.0,2229.0] || -> point_equal(o,a2)*r. % 0.86/1.07 2260[10:Res:2151.0,45.0] || incident(u,b1c1)*+ -> incident(u,oc). % 0.86/1.07 2265[10:Res:11.0,2260.0] || -> incident(b1,oc)*. % 0.86/1.07 2272[10:MRR:2033.0,2265.0] || -> point_equal(b1,o)*l. % 0.86/1.07 2389[10:Res:2241.0,44.1] || incident(a2,u)*+ -> incident(o,u). % 0.86/1.07 2397[10:Res:4.0,2389.0] || -> incident(o,a2b2)*. % 0.86/1.07 2398[10:MRR:2111.0,2397.0] || -> point_equal(o,b2)*r. % 0.86/1.07 2440[10:NCh:42.2,42.0,2272.0,72.0] || point_equal(o,b2)*r -> . % 0.86/1.07 2443[10:MRR:2440.0,2398.0] || -> . % 0.86/1.07 2444[9:Spt:2443.0,341.2] || -> line_equal(a2b2,ob)*l. % 0.86/1.07 2446[9:Res:2444.0,45.0] || incident(u,a2b2)*+ -> incident(u,ob). % 0.86/1.07 2454[9:Res:4.0,2446.0] || -> incident(a2,ob)*. % 0.86/1.07 2457[9:MRR:2078.0,2454.0] || -> point_equal(a2,b1)*r. % 0.86/1.07 2547[9:Res:2457.0,44.1] || incident(b1,u)*+ -> incident(a2,u). % 0.86/1.07 2556[9:Res:3.0,2547.0] || -> incident(a2,a1b1)*. % 0.86/1.07 2564[9:Res:2556.0,2044.0] || incident(a2,oa)* -> point_equal(a2,a1). % 0.86/1.07 2572[9:MRR:2564.0,2564.1,18.0,57.0] || -> . % 0.86/1.07 2574[8:Spt:2572.0,732.2] || -> line_equal(ob,b1c1)*r. % 0.86/1.07 2575[8:Res:2574.0,41.0] || -> line_equal(b1c1,ob)*l. % 0.86/1.07 2603[8:Res:2575.0,45.0] || incident(u,b1c1)*+ -> incident(u,ob). % 0.86/1.07 2609[8:Res:10.0,2603.0] || -> incident(c1,ob)*. % 0.86/1.07 2610[8:Res:105.0,2603.0] || -> incident(a2,ob)*. % 0.86/1.07 2625[8:Res:2609.0,2031.0] || incident(c1,oc)* -> point_equal(c1,o). % 0.86/1.07 2635[8:MRR:2625.0,21.0] || -> point_equal(c1,o)*l. % 0.86/1.07 2637[8:Res:2610.0,2061.0] || incident(a2,oa)* -> point_equal(a2,o). % 0.86/1.07 2645[8:MRR:2637.0,18.0] || -> point_equal(a2,o)*l. % 0.86/1.07 2658[8:Res:2635.0,39.0] || -> point_equal(o,c1)*r. % 0.86/1.07 2680[8:Res:2645.0,44.1] || incident(o,u)+ -> incident(a2,u)*. % 0.86/1.07 2719[8:Res:2658.0,44.1] || incident(c1,u)*+ -> incident(o,u). % 0.86/1.07 2729[8:Res:7.0,2719.0] || -> incident(o,a1c1)*. % 0.86/1.07 2734[8:Res:2729.0,2680.0] || -> incident(a2,a1c1)*. % 0.86/1.07 2751[8:Res:2734.0,2048.0] || incident(a2,oa)* -> point_equal(a2,a1). % 0.86/1.07 2761[8:MRR:2751.0,2751.1,18.0,57.0] || -> . % 0.86/1.07 2763[7:Spt:2761.0,683.2] || -> line_equal(oa,ob)*l. % 0.86/1.07 2764[7:Res:2763.0,41.0] || -> line_equal(ob,oa)*r. % 0.86/1.07 2793[7:Res:2764.0,45.0] || incident(u,ob)+ -> incident(u,oa)*. % 0.86/1.07 2802[7:Res:19.0,2793.0] || -> incident(b1,oa)*. % 0.86/1.07 2808[7:MRR:2046.0,2802.0] || -> point_equal(b1,a1)*r. % 0.86/1.07 2831[7:Res:2808.0,44.1] || incident(a1,u)*+ -> incident(b1,u). % 0.86/1.07 2841[7:Res:6.0,2831.0] || -> incident(b1,a1c1)*. % 0.86/1.07 2843[7:MRR:2841.0,102.0] || -> . % 0.86/1.07 2844[6:Spt:2843.0,444.2] || -> line_equal(a2c2,oa)*l. % 0.86/1.07 2846[6:Res:2844.0,45.0] || incident(u,a2c2)*+ -> incident(u,oa). % 0.86/1.07 2858[6:Res:1977.0,2846.0] || -> incident(b1,oa)*. % 0.86/1.07 2862[6:MRR:2046.0,2858.0] || -> point_equal(b1,a1)*r. % 0.86/1.07 2957[6:Res:2862.0,44.1] || incident(a1,u)*+ -> incident(b1,u). % 0.86/1.07 2966[6:Res:6.0,2957.0] || -> incident(b1,a1c1)*. % 0.86/1.07 2968[6:MRR:2966.0,102.0] || -> . % 0.86/1.07 2969[5:Spt:2968.0,710.2] || -> line_equal(oa,a1c1)*r. % 0.86/1.07 2971[5:Res:2969.0,45.0] || incident(u,oa)+ -> incident(u,a1c1)*. % 0.86/1.07 2975[6:Spt:35.1] || -> incident(a1,b2c2)*. % 0.86/1.07 2976[6:MRR:1978.1,2975.0] || incident(c1,a2b2)*+ -> . % 0.86/1.07 2988[5:Res:18.0,2971.0] || -> incident(a2,a1c1)*. % 0.86/1.07 2990[5:Res:14.0,2971.0] || -> incident(o,a1c1)*. % 0.86/1.07 2991[5:MRR:295.0,2988.0] || -> point_equal(a2,ac)*r. % 0.86/1.07 3045[5:Res:2991.0,44.1] || incident(ac,u)*+ -> incident(a2,u). % 0.86/1.07 3046[5:Res:2991.0,39.0] || -> point_equal(ac,a2)*l. % 0.86/1.07 3074[5:Res:3046.0,44.1] || incident(a2,u)+ -> incident(ac,u)*. % 0.86/1.07 3080[5:Res:105.0,3074.0] || -> incident(ac,b1c1)*. % 0.86/1.07 3143[7:Spt:361.0,361.1,361.3] || incident(u,b1c1)*+ incident(u,a1c1) -> point_equal(u,c1). % 0.86/1.07 3147[7:Res:105.0,3143.0] || incident(a2,a1c1)* -> point_equal(a2,c1). % 0.86/1.07 3150[7:MRR:3147.0,2988.0] || -> point_equal(a2,c1)*r. % 0.86/1.07 3153[7:Res:3150.0,39.0] || -> point_equal(c1,a2)*l. % 0.86/1.07 3214[7:Res:3153.0,44.1] || incident(a2,u)+ -> incident(c1,u)*. % 0.86/1.07 3227[7:Res:4.0,3214.0] || -> incident(c1,a2b2)*. % 0.86/1.07 3229[7:MRR:3227.0,2976.0] || -> . % 0.86/1.07 3230[7:Spt:3229.0,361.2] || -> line_equal(a1c1,b1c1)*r. % 0.86/1.07 3232[7:Res:3230.0,45.0] || incident(u,a1c1)+ -> incident(u,b1c1)*. % 0.86/1.07 3239[7:Res:6.0,3232.0] || -> incident(a1,b1c1)*. % 0.86/1.07 3242[7:MRR:3239.0,104.0] || -> . % 0.86/1.07 3243[6:Spt:3242.0,35.1,2975.0] || incident(a1,b2c2)*+ -> . % 0.86/1.07 3244[6:Spt:3242.0,35.0] || -> incident(b2,a1c1)*. % 0.86/1.07 3262[7:Spt:825.0,825.1,825.3] || incident(u,a2c2)*+ incident(u,oc) -> point_equal(u,c2). % 0.86/1.07 3276[8:Spt:1981.0,1981.1,1981.3] || incident(u,a2c2)*+ incident(u,b1c1) -> point_equal(u,b1). % 0.86/1.07 3277[8:Res:26.0,3276.0] || incident(ac,b1c1)* -> point_equal(ac,b1). % 0.86/1.07 3281[8:MRR:3277.0,3080.0] || -> point_equal(ac,b1)*l. % 0.86/1.07 3283[8:Res:3281.0,44.1] || incident(b1,u)+ -> incident(ac,u)*. % 0.86/1.07 3291[8:Res:3.0,3283.0] || -> incident(ac,a1b1)*. % 0.86/1.07 3304[8:Res:3291.0,3045.0] || -> incident(a2,a1b1)*. % 0.86/1.07 3326[8:Res:3304.0,2044.0] || incident(a2,oa)* -> point_equal(a2,a1). % 0.86/1.07 3335[8:MRR:3326.0,3326.1,18.0,57.0] || -> . % 0.86/1.07 3337[8:Spt:3335.0,1981.2] || -> line_equal(b1c1,a2c2)*r. % 0.86/1.07 3339[8:Res:3337.0,45.0] || incident(u,b1c1)+ -> incident(u,a2c2)*. % 0.86/1.07 3349[8:Res:10.0,3339.0] || -> incident(c1,a2c2)*. % 0.86/1.07 3366[8:Res:3349.0,3262.0] || incident(c1,oc)* -> point_equal(c1,c2). % 0.86/1.07 3382[8:MRR:3366.0,3366.1,21.0,70.0] || -> . % 0.86/1.07 3387[7:Spt:3382.0,825.2] || -> line_equal(oc,a2c2)*r. % 0.86/1.07 3388[7:Res:3387.0,41.0] || -> line_equal(a2c2,oc)*l. % 0.86/1.07 3434[7:Res:3388.0,45.0] || incident(u,a2c2)*+ -> incident(u,oc). % 0.86/1.07 3443[7:Res:1977.0,3434.0] || -> incident(b1,oc)*. % 0.86/1.07 3450[7:MRR:2033.0,3443.0] || -> point_equal(b1,o)*l. % 0.86/1.07 3611[7:Res:3450.0,44.1] || incident(o,u)+ -> incident(b1,u)*. % 0.86/1.07 3621[7:Res:2990.0,3611.0] || -> incident(b1,a1c1)*. % 0.86/1.07 3624[7:MRR:3621.0,102.0] || -> . % 0.86/1.07 3628[4:Spt:3624.0,711.2] || -> line_equal(oa,a1b1)*r. % 0.86/1.07 3629[4:Res:3628.0,41.0] || -> line_equal(a1b1,oa)*l. % 0.86/1.07 3630[4:Res:3628.0,45.0] || incident(u,oa)+ -> incident(u,a1b1)*. % 0.86/1.07 3642[4:Res:18.0,3630.0] || -> incident(a2,a1b1)*. % 0.86/1.07 3644[4:Res:14.0,3630.0] || -> incident(o,a1b1)*. % 0.86/1.07 3646[4:MRR:288.0,3642.0] || -> point_equal(a2,ab)*r. % 0.86/1.07 3665[4:Res:3629.0,45.0] || incident(u,a1b1)*+ -> incident(u,oa). % 0.86/1.07 3670[4:Res:3.0,3665.0] || -> incident(b1,oa)*. % 0.86/1.07 3696[4:Res:3646.0,39.0] || -> point_equal(ab,a2)*l. % 0.86/1.07 3697[4:NCh:42.2,42.1,3646.0,44.1] || incident(ab,u)* point_equal(v,a2)+ -> incident(v,u)*. % 0.86/1.07 3705[4:Res:3696.0,44.1] || incident(a2,u)+ -> incident(ab,u)*. % 0.86/1.07 3712[4:Res:8.0,3705.0] || -> incident(ab,a2c2)*. % 0.86/1.07 3716[4:MRR:95.0,3712.0] || incident(bc,a2c2)*+ -> . % 0.86/1.07 3764[5:Spt:719.0,719.1,719.3] || incident(u,b1c1)*+ incident(u,oa) -> point_equal(u,a2). % 0.86/1.07 3766[5:Res:11.0,3764.0] || incident(b1,oa)* -> point_equal(b1,a2). % 0.86/1.07 3770[5:MRR:3766.0,3670.0] || -> point_equal(b1,a2)*l. % 0.86/1.07 3771[5:Res:3770.0,3697.1] || incident(ab,u)*+ -> incident(b1,u). % 0.86/1.07 3778[5:Res:28.0,3771.0] || -> incident(b1,a2b2)*. % 0.86/1.07 3791[5:Res:3778.0,263.0] || incident(b2,a2b2)* -> line_equal(ob,a2b2). % 0.86/1.07 3797[5:MRR:3791.0,5.0] || -> line_equal(ob,a2b2)*r. % 0.86/1.07 3858[5:NCh:43.2,43.1,3797.0,52.0] || line_equal(a1b1,ob)*l+ -> . % 0.86/1.07 3865[5:MRR:320.2,3858.0] || incident(u,ob)+ incident(u,a1b1)* -> point_equal(u,b1). % 0.86/1.07 3869[5:Res:15.0,3865.0] || incident(o,a1b1)* -> point_equal(o,b1). % 0.86/1.07 3872[5:MRR:3869.0,3644.0] || -> point_equal(o,b1)*r. % 0.86/1.07 3921[5:Res:3872.0,44.1] || incident(b1,u)*+ -> incident(o,u). % 0.86/1.07 3922[5:Res:3872.0,39.0] || -> point_equal(b1,o)*l. % 0.86/1.07 3924[5:NCh:42.2,42.1,3872.0,56.0] || point_equal(b2,o)*l+ -> . % 0.86/1.07 3928[5:MRR:2032.1,3924.0] || incident(b2,oc)*+ -> . % 0.86/1.07 3938[5:Res:11.0,3921.0] || -> incident(o,b1c1)*. % 0.86/1.07 3999[5:Res:3922.0,44.1] || incident(o,u)+ -> incident(b1,u)*. % 0.86/1.07 4098[6:Spt:594.0,594.1,594.3] || incident(u,oc)+ incident(u,b2c2)* -> point_equal(u,c2). % 0.86/1.07 4134[7:Spt:492.0,492.1,492.3] || incident(u,oc)+ incident(u,b1c1)* -> point_equal(u,c1). % 0.86/1.07 4137[7:Res:16.0,4134.0] || incident(o,b1c1)* -> point_equal(o,c1). % 0.86/1.07 4142[7:MRR:4137.0,3938.0] || -> point_equal(o,c1)*r. % 0.86/1.07 4146[7:Res:4142.0,44.1] || incident(c1,u)*+ -> incident(o,u). % 0.86/1.07 4155[7:Res:7.0,4146.0] || -> incident(o,a1c1)*. % 0.86/1.07 4161[7:Res:4155.0,3999.0] || -> incident(b1,a1c1)*. % 0.86/1.07 4172[7:MRR:4161.0,102.0] || -> . % 0.86/1.07 4174[7:Spt:4172.0,492.2] || -> line_equal(b1c1,oc)*l. % 0.86/1.07 4176[7:Res:4174.0,45.0] || incident(u,b1c1)*+ -> incident(u,oc). % 0.86/1.07 4183[7:Res:23.0,4176.0] || -> incident(bc,oc)*. % 0.86/1.07 4190[7:Res:4183.0,4098.0] || incident(bc,b2c2)* -> point_equal(bc,c2). % 0.86/1.07 4196[7:MRR:4190.0,24.0] || -> point_equal(bc,c2)*l. % 0.86/1.07 4233[7:Res:4196.0,44.1] || incident(c2,u)+ -> incident(bc,u)*. % 0.86/1.07 4244[7:Res:9.0,4233.0] || -> incident(bc,a2c2)*. % 0.86/1.07 4245[7:MRR:4244.0,3716.0] || -> . % 0.86/1.07 4246[6:Spt:4245.0,594.2] || -> line_equal(b2c2,oc)*l. % 0.86/1.07 4248[6:Res:4246.0,45.0] || incident(u,b2c2)*+ -> incident(u,oc). % 0.86/1.07 4259[6:Res:13.0,4248.0] || -> incident(b2,oc)*. % 0.86/1.07 4262[6:MRR:4259.0,3928.0] || -> . % 0.86/1.07 4263[5:Spt:4262.0,719.2] || -> line_equal(oa,b1c1)*r. % 0.86/1.07 4265[5:Res:4263.0,45.0] || incident(u,oa)+ -> incident(u,b1c1)*. % 0.86/1.07 4278[5:Res:17.0,4265.0] || -> incident(a1,b1c1)*. % 0.86/1.07 4282[5:MRR:4278.0,104.0] || -> . % 0.86/1.07 4283[3:Spt:4282.0,770.2] || -> line_equal(oc,ob)*r. % 0.86/1.07 4284[3:Res:4283.0,41.0] || -> line_equal(ob,oc)*l. % 0.86/1.07 4285[3:Res:4283.0,45.0] || incident(u,oc)+ -> incident(u,ob)*. % 0.86/1.07 4302[3:Res:22.0,4285.0] || -> incident(c2,ob)*. % 0.86/1.07 4305[3:MRR:78.0,4302.0] || incident(a2,ob)*+ -> . % 0.86/1.07 4330[3:NCh:43.2,43.0,4284.0,45.0] || line_equal(oc,u)+ incident(v,ob)* -> incident(v,u)*. % 0.86/1.07 4410[4:Spt:1981.0,1981.1,1981.3] || incident(u,a2c2)*+ incident(u,b1c1) -> point_equal(u,b1). % 0.86/1.07 4413[4:Res:8.0,4410.0] || incident(a2,b1c1)* -> point_equal(a2,b1). % 0.86/1.07 4415[4:MRR:4413.0,105.0] || -> point_equal(a2,b1)*r. % 0.86/1.07 4416[4:Res:4415.0,44.1] || incident(b1,u)*+ -> incident(a2,u). % 0.86/1.07 4422[4:Res:19.0,4416.0] || -> incident(a2,ob)*. % 0.86/1.07 4427[4:MRR:4422.0,4305.0] || -> . % 0.86/1.07 4434[4:Spt:4427.0,1981.2] || -> line_equal(b1c1,a2c2)*r. % 0.86/1.07 4435[4:Res:4434.0,41.0] || -> line_equal(a2c2,b1c1)*l. % 0.86/1.07 4441[4:NCh:43.2,43.1,4434.0,4330.0] || line_equal(oc,b1c1) incident(u,ob) -> incident(u,a2c2)*. % 0.86/1.07 4477[4:Res:4435.0,45.0] || incident(u,a2c2)*+ -> incident(u,b1c1). % 0.86/1.07 4489[4:Res:9.0,4477.0] || -> incident(c2,b1c1)*. % 0.86/1.07 4495[4:MRR:223.0,4489.0] || -> line_equal(oc,b1c1)*r. % 0.86/1.07 4501[4:MRR:4441.0,4495.0] || incident(u,ob)+ -> incident(u,a2c2)*. % 0.86/1.07 4533[4:Res:20.0,4501.0] || -> incident(b2,a2c2)*. % 0.86/1.07 4538[4:MRR:4533.0,99.0] || -> . % 0.86/1.07 4539[1:Spt:4538.0,37.0,105.0] || incident(a2,b1c1)*+ -> . % 0.86/1.07 4540[1:Spt:4538.0,37.1] || -> incident(c1,a2b2)*. % 0.86/1.07 4541[1:MRR:61.0,4540.0] || incident(b1,a2c2)+ incident(a1,b2c2)* -> . % 0.86/1.07 4544[1:Res:4540.0,232.0] || incident(u,a2b2)*+ incident(u,oc) -> line_equal(oc,a2b2) point_equal(u,c1). % 0.86/1.07 4546[1:Res:4540.0,248.0] || incident(u,a2b2)*+ incident(u,a1c1) -> line_equal(a1c1,a2b2) point_equal(u,c1). % 0.86/1.07 4552[2:Spt:35.0] || -> incident(b2,a1c1)*. % 0.86/1.07 4556[2:Res:4552.0,250.0] || incident(u,a1c1)+ incident(u,a2b2)* -> line_equal(a2b2,a1c1) point_equal(u,b2). % 0.86/1.07 4570[1:Res:36.1,4541.0] || incident(a1,b2c2)*+ -> incident(c2,a1b1). % 0.86/1.07 4596[3:Spt:710.0,710.1,710.3] || incident(u,a1c1)*+ incident(u,oa) -> point_equal(u,a1). % 0.86/1.07 4600[3:Res:4552.0,4596.0] || incident(b2,oa)*+ -> point_equal(b2,a1). % 0.86/1.07 4601[4:Spt:794.0,794.1,794.3] || incident(u,a1c1)*+ incident(u,oc) -> point_equal(u,c1). % 0.86/1.07 4602[4:Res:25.0,4601.0] || incident(ac,oc)*+ -> point_equal(ac,c1). % 0.86/1.07 4604[4:Res:6.0,4601.0] || incident(a1,oc)*+ -> point_equal(a1,c1). % 0.86/1.07 4606[5:Spt:467.0,467.1,467.3] || incident(u,oc)+ incident(u,a2c2)* -> point_equal(u,c2). % 0.86/1.07 4620[6:Spt:683.0,683.1,683.3] || incident(u,ob)+ incident(u,oa)* -> point_equal(u,o). % 0.86/1.07 4624[7:Spt:733.0,733.1,733.3] || incident(u,a1b1)*+ incident(u,ob) -> point_equal(u,b1). % 0.86/1.07 4628[8:Spt:341.0,341.1,341.3] || incident(u,ob)+ incident(u,a2b2)* -> point_equal(u,b2). % 0.86/1.07 4633[9:Spt:655.0,655.1,655.3] || incident(u,ob)+ incident(u,b2c2)* -> point_equal(u,b2). % 0.86/1.07 4636[9:Res:15.0,4633.0] || incident(o,b2c2)*+ -> point_equal(o,b2). % 0.86/1.07 4638[10:Spt:330.0,330.1,330.3] || incident(u,oa)+ incident(u,a2b2)* -> point_equal(u,a2). % 0.86/1.07 4640[10:Res:17.0,4638.0] || incident(a1,a2b2)* -> point_equal(a1,a2). % 0.86/1.07 4641[10:Res:14.0,4638.0] || incident(o,a2b2)*+ -> point_equal(o,a2). % 0.86/1.07 4642[10:MRR:4640.1,74.0] || incident(a1,a2b2)*+ -> . % 0.86/1.07 4647[11:Spt:594.0,594.1,594.3] || incident(u,oc)+ incident(u,b2c2)* -> point_equal(u,c2). % 0.86/1.07 4649[11:Res:21.0,4647.0] || incident(c1,b2c2)* -> point_equal(c1,c2). % 0.86/1.07 4651[11:MRR:4649.1,70.0] || incident(c1,b2c2)*+ -> . % 0.86/1.07 4678[12:Spt:539.0,539.1,539.3] || incident(u,ob)+ incident(u,b1c1)* -> point_equal(u,b1). % 0.86/1.07 4679[12:Res:20.0,4678.0] || incident(b2,b1c1)* -> point_equal(b2,b1). % 0.86/1.07 4682[12:MRR:4679.1,56.0] || incident(b2,b1c1)*+ -> . % 0.86/1.07 4693[13:Spt:4546.0,4546.1,4546.3] || incident(u,a2b2)*+ incident(u,a1c1) -> point_equal(u,c1). % 0.86/1.07 4695[13:Res:5.0,4693.0] || incident(b2,a1c1)* -> point_equal(b2,c1). % 0.86/1.07 4698[13:MRR:4695.0,4552.0] || -> point_equal(b2,c1)*r. % 0.86/1.07 4704[13:Res:4698.0,44.1] || incident(c1,u)*+ -> incident(b2,u). % 0.86/1.07 4710[13:Res:10.0,4704.0] || -> incident(b2,b1c1)*. % 0.86/1.07 4715[13:MRR:4710.0,4682.0] || -> . % 0.86/1.07 4716[13:Spt:4715.0,4546.2] || -> line_equal(a1c1,a2b2)*r. % 0.86/1.07 4718[13:Res:4716.0,45.0] || incident(u,a1c1)+ -> incident(u,a2b2)*. % 0.86/1.07 4725[13:Res:6.0,4718.0] || -> incident(a1,a2b2)*. % 0.86/1.07 4729[13:MRR:4725.0,4642.0] || -> . % 0.86/1.07 4730[12:Spt:4729.0,539.2] || -> line_equal(b1c1,ob)*l. % 0.86/1.07 4732[12:Res:4730.0,45.0] || incident(u,b1c1)*+ -> incident(u,ob). % 0.86/1.07 4738[12:Res:10.0,4732.0] || -> incident(c1,ob)*. % 0.86/1.07 4752[12:Res:4738.0,4628.0] || incident(c1,a2b2)* -> point_equal(c1,b2). % 0.86/1.07 4765[12:MRR:4752.0,4540.0] || -> point_equal(c1,b2)*l. % 0.86/1.07 4875[12:Res:4765.0,44.1] || incident(b2,u)+ -> incident(c1,u)*. % 0.86/1.07 4881[12:Res:13.0,4875.0] || -> incident(c1,b2c2)*. % 0.86/1.07 4885[12:MRR:4881.0,4651.0] || -> . % 0.86/1.07 4886[11:Spt:4885.0,594.2] || -> line_equal(b2c2,oc)*l. % 0.86/1.07 4887[11:Res:4886.0,41.0] || -> line_equal(oc,b2c2)*r. % 0.86/1.07 4914[11:Res:4887.0,45.0] || incident(u,oc)+ -> incident(u,b2c2)*. % 0.86/1.07 4922[11:Res:16.0,4914.0] || -> incident(o,b2c2)*. % 0.86/1.07 4926[11:MRR:4636.0,4922.0] || -> point_equal(o,b2)*r. % 0.86/1.07 4987[11:Res:4926.0,44.1] || incident(b2,u)*+ -> incident(o,u). % 0.86/1.07 4988[11:Res:4926.0,39.0] || -> point_equal(b2,o)*l. % 0.86/1.07 4996[11:Res:5.0,4987.0] || -> incident(o,a2b2)*. % 0.86/1.07 4999[11:MRR:4641.0,4996.0] || -> point_equal(o,a2)*r. % 0.86/1.07 5143[11:Res:4988.0,44.1] || incident(o,u)+ -> incident(b2,u)*. % 0.86/1.07 5237[11:Res:4999.0,44.1] || incident(a2,u)*+ -> incident(o,u). % 0.86/1.07 5242[11:Res:8.0,5237.0] || -> incident(o,a2c2)*. % 0.86/1.07 5247[11:Res:5242.0,5143.0] || -> incident(b2,a2c2)*. % 0.86/1.07 5254[11:MRR:5247.0,99.0] || -> . % 0.86/1.07 5256[10:Spt:5254.0,330.2] || -> line_equal(a2b2,oa)*l. % 0.86/1.07 5258[10:Res:5256.0,45.0] || incident(u,a2b2)*+ -> incident(u,oa). % 0.86/1.07 5266[10:Res:5.0,5258.0] || -> incident(b2,oa)*. % 0.86/1.07 5271[10:MRR:4600.0,5266.0] || -> point_equal(b2,a1)*r. % 0.86/1.07 5368[10:Res:5271.0,44.1] || incident(a1,u)*+ -> incident(b2,u). % 0.86/1.07 5376[10:Res:2.0,5368.0] || -> incident(b2,a1b1)*. % 0.86/1.07 5384[10:Res:5376.0,4624.0] || incident(b2,ob)* -> point_equal(b2,b1). % 0.86/1.07 5393[10:MRR:5384.0,5384.1,20.0,56.0] || -> . % 0.86/1.07 5395[9:Spt:5393.0,655.2] || -> line_equal(b2c2,ob)*l. % 0.86/1.07 5398[9:NCh:43.2,43.0,5395.0,68.0] || line_equal(ob,b1c1)*r+ -> . % 0.86/1.07 5402[9:MRR:265.1,5398.0] || incident(b2,b1c1)*+ -> . % 0.86/1.07 5848[10:Spt:4556.0,4556.1,4556.3] || incident(u,a1c1)+ incident(u,a2b2)* -> point_equal(u,b2). % 0.86/1.07 5850[10:Res:7.0,5848.0] || incident(c1,a2b2)* -> point_equal(c1,b2). % 0.86/1.07 5853[10:MRR:5850.0,4540.0] || -> point_equal(c1,b2)*l. % 0.86/1.07 5855[10:Res:5853.0,39.0] || -> point_equal(b2,c1)*r. % 0.86/1.07 5902[10:Res:5855.0,44.1] || incident(c1,u)*+ -> incident(b2,u). % 0.86/1.07 5911[10:Res:10.0,5902.0] || -> incident(b2,b1c1)*. % 0.86/1.07 5915[10:MRR:5911.0,5402.0] || -> . % 0.86/1.07 5916[10:Spt:5915.0,4556.2] || -> line_equal(a2b2,a1c1)*l. % 0.86/1.07 5918[10:Res:5916.0,45.0] || incident(u,a2b2)*+ -> incident(u,a1c1). % 0.86/1.07 5926[10:Res:4.0,5918.0] || -> incident(a2,a1c1)*. % 0.86/1.07 5945[10:Res:5926.0,4596.0] || incident(a2,oa)* -> point_equal(a2,a1). % 0.86/1.07 5953[10:MRR:5945.0,5945.1,18.0,57.0] || -> . % 0.86/1.07 5955[8:Spt:5953.0,341.2] || -> line_equal(a2b2,ob)*l. % 0.86/1.07 5957[8:Res:5955.0,45.0] || incident(u,a2b2)*+ -> incident(u,ob). % 0.86/1.07 5976[8:Res:4.0,5957.0] || -> incident(a2,ob)*. % 0.86/1.07 5988[8:Res:5976.0,4620.0] || incident(a2,oa)* -> point_equal(a2,o). % 0.86/1.07 5995[8:MRR:5988.0,18.0] || -> point_equal(a2,o)*l. % 0.86/1.07 6059[8:Res:5995.0,44.1] || incident(o,u)+ -> incident(a2,u)*. % 0.86/1.07 6063[8:Res:16.0,6059.0] || -> incident(a2,oc)*. % 0.86/1.07 6068[8:Res:6063.0,4606.0] || incident(a2,a2c2)* -> point_equal(a2,c2). % 0.86/1.07 6075[8:MRR:6068.0,8.0] || -> point_equal(a2,c2)*l. % 0.86/1.07 6110[8:Res:6075.0,44.1] || incident(c2,u)+ -> incident(a2,u)*. % 0.86/1.07 6117[8:Res:12.0,6110.0] || -> incident(a2,b2c2)*. % 0.86/1.07 6120[8:MRR:6117.0,101.0] || -> . % 0.86/1.07 6128[7:Spt:6120.0,733.2] || -> line_equal(ob,a1b1)*r. % 0.86/1.07 6129[7:Res:6128.0,41.0] || -> line_equal(a1b1,ob)*l. % 0.86/1.07 6176[7:Res:6129.0,45.0] || incident(u,a1b1)*+ -> incident(u,ob). % 0.86/1.07 6182[7:Res:2.0,6176.0] || -> incident(a1,ob)*. % 0.86/1.07 6195[7:Res:6182.0,4620.0] || incident(a1,oa)* -> point_equal(a1,o). % 0.86/1.07 6204[7:MRR:6195.0,17.0] || -> point_equal(a1,o)*l. % 0.86/1.07 6230[7:Res:6204.0,44.1] || incident(o,u)+ -> incident(a1,u)*. % 0.86/1.07 6241[7:Res:16.0,6230.0] || -> incident(a1,oc)*. % 0.86/1.07 6246[7:MRR:4604.0,6241.0] || -> point_equal(a1,c1)*l. % 0.86/1.07 6444[7:Res:6246.0,44.1] || incident(c1,u)+ -> incident(a1,u)*. % 0.86/1.07 6453[7:Res:10.0,6444.0] || -> incident(a1,b1c1)*. % 0.86/1.07 6456[7:MRR:6453.0,104.0] || -> . % 0.86/1.07 6457[6:Spt:6456.0,683.2] || -> line_equal(oa,ob)*l. % 0.86/1.07 6458[6:Res:6457.0,41.0] || -> line_equal(ob,oa)*r. % 0.86/1.07 6459[6:Res:6457.0,45.0] || incident(u,oa)*+ -> incident(u,ob). % 0.86/1.07 6463[7:Spt:36.0] || -> incident(c2,a1b1)*. % 0.86/1.07 6466[7:Res:6463.0,58.0] || incident(b2,a1b1)+ incident(a2,a1b1)* -> . % 0.86/1.07 6473[6:Res:18.0,6459.0] || -> incident(a2,ob)*. % 0.86/1.07 6498[6:Res:6458.0,45.0] || incident(u,ob)+ -> incident(u,oa)*. % 0.86/1.07 6502[6:Res:20.0,6498.0] || -> incident(b2,oa)*. % 0.86/1.07 6508[6:MRR:4600.0,6502.0] || -> point_equal(b2,a1)*r. % 0.86/1.07 6530[6:Res:6508.0,44.1] || incident(a1,u)*+ -> incident(b2,u). % 0.86/1.07 6531[6:Res:6508.0,39.0] || -> point_equal(a1,b2)*l. % 0.86/1.07 6538[6:Res:2.0,6530.0] || -> incident(b2,a1b1)*. % 0.86/1.07 6539[7:MRR:6466.0,6538.0] || incident(a2,a1b1)*+ -> . % 0.86/1.07 6540[6:MRR:266.0,6538.0] || -> line_equal(ob,a1b1)*r. % 0.86/1.07 6555[6:Res:6531.0,44.1] || incident(b2,u)+ -> incident(a1,u)*. % 0.86/1.07 6563[6:Res:13.0,6555.0] || -> incident(a1,b2c2)*. % 0.86/1.07 6594[6:Res:6540.0,45.0] || incident(u,ob)+ -> incident(u,a1b1)*. % 0.86/1.07 6600[6:Res:6473.0,6594.0] || -> incident(a2,a1b1)*. % 0.86/1.07 6602[7:MRR:6600.0,6539.0] || -> . % 0.86/1.07 6603[7:Spt:6602.0,36.0,6463.0] || incident(c2,a1b1)* -> . % 0.86/1.07 6604[7:Spt:6602.0,36.1] || -> incident(b1,a2c2)*. % 0.86/1.07 6606[6:MRR:4570.0,6563.0] || -> incident(c2,a1b1)*. % 0.86/1.07 6607[7:MRR:6606.0,6603.0] || -> . % 0.86/1.07 6617[5:Spt:6607.0,467.2] || -> line_equal(a2c2,oc)*l. % 0.86/1.07 6619[5:Res:6617.0,45.0] || incident(u,a2c2)*+ -> incident(u,oc). % 0.86/1.07 6634[5:Res:26.0,6619.0] || -> incident(ac,oc)*. % 0.86/1.07 6637[5:MRR:4602.0,6634.0] || -> point_equal(ac,c1)*l. % 0.86/1.07 6686[5:Res:6637.0,44.1] || incident(c1,u)+ -> incident(ac,u)*. % 0.86/1.07 6691[5:Res:10.0,6686.0] || -> incident(ac,b1c1)*. % 0.86/1.07 6694[5:Res:4540.0,6686.0] || -> incident(ac,a2b2)*. % 0.86/1.07 6762[6:Spt:332.0,332.1,332.3] || incident(u,a2c2)*+ incident(u,a2b2) -> point_equal(u,a2). % 0.86/1.07 6763[6:Res:26.0,6762.0] || incident(ac,a2b2)* -> point_equal(ac,a2). % 0.86/1.07 6768[6:MRR:6763.0,6694.0] || -> point_equal(ac,a2)*l. % 0.86/1.07 6771[6:Res:6768.0,39.0] || -> point_equal(a2,ac)*r. % 0.86/1.07 6812[6:Res:6771.0,44.1] || incident(ac,u)*+ -> incident(a2,u). % 0.86/1.07 6823[6:Res:6691.0,6812.0] || -> incident(a2,b1c1)*. % 0.86/1.07 6830[6:MRR:6823.0,4539.0] || -> . % 0.86/1.07 6831[6:Spt:6830.0,332.2] || -> line_equal(a2b2,a2c2)*r. % 0.86/1.07 6833[6:Res:6831.0,45.0] || incident(u,a2b2)+ -> incident(u,a2c2)*. % 0.86/1.07 6844[6:Res:5.0,6833.0] || -> incident(b2,a2c2)*. % 0.86/1.07 6849[6:MRR:6844.0,99.0] || -> . % 0.86/1.07 6850[4:Spt:6849.0,794.2] || -> line_equal(oc,a1c1)*r. % 0.86/1.07 6851[4:Res:6850.0,41.0] || -> line_equal(a1c1,oc)*l. % 0.86/1.07 6852[4:Res:6850.0,45.0] || incident(u,oc)+ -> incident(u,a1c1)*. % 0.86/1.07 6856[5:Spt:36.1] || -> incident(b1,a2c2)*. % 0.86/1.07 6857[5:MRR:4541.0,6856.0] || incident(a1,b2c2)*+ -> . % 0.86/1.07 6873[4:Res:16.0,6852.0] || -> incident(o,a1c1)*. % 0.86/1.07 6889[4:Res:6873.0,4596.0] || incident(o,oa)* -> point_equal(o,a1). % 0.86/1.07 6897[4:MRR:6889.0,14.0] || -> point_equal(o,a1)*r. % 0.86/1.07 6899[4:Res:6851.0,45.0] || incident(u,a1c1)*+ -> incident(u,oc). % 0.86/1.07 6905[4:Res:6.0,6899.0] || -> incident(a1,oc)*. % 0.86/1.07 6906[4:Res:4552.0,6899.0] || -> incident(b2,oc)*. % 0.86/1.07 6909[4:MRR:90.1,6905.0] || incident(b1,oc)*+ -> . % 0.86/1.07 6946[4:Res:6897.0,39.0] || -> point_equal(a1,o)*l. % 0.86/1.07 6982[4:Res:6946.0,44.1] || incident(o,u)+ -> incident(a1,u)*. % 0.86/1.07 6989[4:Res:15.0,6982.0] || -> incident(a1,ob)*. % 0.86/1.07 6993[4:MRR:87.1,6989.0] || incident(c1,ob)*+ -> . % 0.86/1.07 7013[6:Spt:723.0,723.1,723.3] || incident(u,oc)+ incident(u,ob)* -> point_equal(u,o). % 0.86/1.07 7019[6:Res:6906.0,7013.0] || incident(b2,ob)* -> point_equal(b2,o). % 0.86/1.07 7020[6:MRR:7019.0,20.0] || -> point_equal(b2,o)*l. % 0.86/1.07 7022[6:Res:7020.0,39.0] || -> point_equal(o,b2)*r. % 0.86/1.07 7053[6:Res:7022.0,44.1] || incident(b2,u)*+ -> incident(o,u). % 0.86/1.07 7061[6:Res:13.0,7053.0] || -> incident(o,b2c2)*. % 0.86/1.07 7069[6:Res:7061.0,6982.0] || -> incident(a1,b2c2)*. % 0.86/1.07 7076[6:MRR:7069.0,6857.0] || -> . % 0.86/1.07 7077[6:Spt:7076.0,723.2] || -> line_equal(ob,oc)*l. % 0.86/1.07 7079[6:Res:7077.0,45.0] || incident(u,ob)*+ -> incident(u,oc). % 0.86/1.07 7084[6:Res:19.0,7079.0] || -> incident(b1,oc)*. % 0.86/1.07 7087[6:MRR:7084.0,6909.0] || -> . % 0.86/1.07 7088[5:Spt:7087.0,36.1,6856.0] || incident(b1,a2c2)*+ -> . % 0.86/1.07 7089[5:Spt:7087.0,36.0] || -> incident(c2,a1b1)*. % 0.86/1.07 7111[6:Spt:4544.0,4544.1,4544.3] || incident(u,a2b2)*+ incident(u,oc) -> point_equal(u,c1). % 0.86/1.07 7113[6:Res:5.0,7111.0] || incident(b2,oc)* -> point_equal(b2,c1). % 0.86/1.07 7116[6:MRR:7113.0,6906.0] || -> point_equal(b2,c1)*r. % 0.86/1.07 7118[6:Res:7116.0,39.0] || -> point_equal(c1,b2)*l. % 0.86/1.07 7140[6:Res:7118.0,44.1] || incident(b2,u)+ -> incident(c1,u)*. % 0.86/1.07 7150[6:Res:20.0,7140.0] || -> incident(c1,ob)*. % 0.86/1.07 7155[6:MRR:7150.0,6993.0] || -> . % 0.86/1.07 7157[6:Spt:7155.0,4544.2] || -> line_equal(oc,a2b2)*r. % 0.86/1.07 7159[6:Res:7157.0,45.0] || incident(u,oc)+ -> incident(u,a2b2)*. % 0.86/1.07 7165[6:Res:22.0,7159.0] || -> incident(c2,a2b2)*. % 0.86/1.07 7171[6:MRR:7165.0,100.0] || -> . % 0.86/1.07 7177[3:Spt:7171.0,710.2] || -> line_equal(oa,a1c1)*r. % 0.86/1.07 7178[3:Res:7177.0,41.0] || -> line_equal(a1c1,oa)*l. % 0.86/1.07 7179[3:Res:7177.0,45.0] || incident(u,oa)+ -> incident(u,a1c1)*. % 0.86/1.07 7192[3:Res:18.0,7179.0] || -> incident(a2,a1c1)*. % 0.86/1.07 7194[3:Res:14.0,7179.0] || -> incident(o,a1c1)*. % 0.86/1.07 7195[3:MRR:295.0,7192.0] || -> point_equal(a2,ac)*r. % 0.86/1.07 7215[3:Res:7178.0,45.0] || incident(u,a1c1)*+ -> incident(u,oa). % 0.86/1.07 7220[3:Res:7.0,7215.0] || -> incident(c1,oa)*. % 0.86/1.07 7222[3:Res:4552.0,7215.0] || -> incident(b2,oa)*. % 0.86/1.07 7226[3:MRR:75.1,7222.0] || incident(c2,oa)*+ -> . % 0.86/1.07 7251[3:Res:7195.0,44.1] || incident(ac,u)*+ -> incident(a2,u). % 0.86/1.07 7252[3:Res:7195.0,39.0] || -> point_equal(ac,a2)*l. % 0.86/1.07 7261[3:Res:7252.0,44.1] || incident(a2,u)+ -> incident(ac,u)*. % 0.86/1.07 7269[3:Res:4.0,7261.0] || -> incident(ac,a2b2)*. % 0.86/1.07 7270[3:MRR:97.0,7269.0] || incident(bc,a2b2)*+ -> . % 0.86/1.07 7797[4:Spt:4556.0,4556.1,4556.3] || incident(u,a1c1)+ incident(u,a2b2)* -> point_equal(u,b2). % 0.86/1.07 7798[4:Res:25.0,7797.0] || incident(ac,a2b2)* -> point_equal(ac,b2). % 0.86/1.07 7804[4:MRR:7798.0,7269.0] || -> point_equal(ac,b2)*l. % 0.86/1.07 7807[4:Res:7804.0,44.1] || incident(b2,u)+ -> incident(ac,u)*. % 0.86/1.07 7816[4:Res:13.0,7807.0] || -> incident(ac,b2c2)*. % 0.86/1.07 7828[4:Res:7816.0,7251.0] || -> incident(a2,b2c2)*. % 0.86/1.07 7834[4:MRR:7828.0,101.0] || -> . % 0.86/1.07 7835[4:Spt:7834.0,4556.2] || -> line_equal(a2b2,a1c1)*l. % 0.86/1.07 7836[4:Res:7835.0,41.0] || -> line_equal(a1c1,a2b2)*r. % 0.86/1.07 7870[4:Res:7836.0,45.0] || incident(u,a1c1)+ -> incident(u,a2b2)*. % 0.86/1.07 7880[4:Res:6.0,7870.0] || -> incident(a1,a2b2)*. % 0.86/1.07 7883[4:Res:7194.0,7870.0] || -> incident(o,a2b2)*. % 0.86/1.07 7989[5:Spt:341.0,341.1,341.3] || incident(u,ob)+ incident(u,a2b2)* -> point_equal(u,b2). % 0.86/1.07 7992[5:Res:15.0,7989.0] || incident(o,a2b2)* -> point_equal(o,b2). % 0.86/1.07 7993[5:MRR:7992.0,7883.0] || -> point_equal(o,b2)*r. % 0.86/1.07 7994[5:Res:7993.0,44.1] || incident(b2,u)*+ -> incident(o,u). % 0.86/1.07 8000[5:Res:13.0,7994.0] || -> incident(o,b2c2)*. % 0.86/1.07 8098[6:Spt:771.0,771.1,771.3] || incident(u,oa)*+ incident(u,oc) -> point_equal(u,o). % 0.86/1.07 8103[6:Res:7220.0,8098.0] || incident(c1,oc)* -> point_equal(c1,o). % 0.86/1.07 8106[6:MRR:8103.0,21.0] || -> point_equal(c1,o)*l. % 0.86/1.07 8107[6:Res:8106.0,44.1] || incident(o,u)+ -> incident(c1,u)*. % 0.86/1.07 8118[6:Res:8000.0,8107.0] || -> incident(c1,b2c2)*. % 0.86/1.07 8122[6:MRR:298.0,8118.0] || incident(u,b2c2)*+ incident(u,b1c1) -> point_equal(u,c1). % 0.86/1.07 8170[6:Res:24.0,8122.0] || incident(bc,b1c1)* -> point_equal(bc,c1). % 0.86/1.07 8175[6:MRR:8170.0,23.0] || -> point_equal(bc,c1)*l. % 0.86/1.07 8256[6:Res:8175.0,44.1] || incident(c1,u)+ -> incident(bc,u)*. % 0.86/1.07 8271[6:Res:4540.0,8256.0] || -> incident(bc,a2b2)*. % 0.86/1.07 8274[6:MRR:8271.0,7270.0] || -> . % 0.86/1.07 8275[6:Spt:8274.0,771.2] || -> line_equal(oc,oa)*r. % 0.86/1.07 8277[6:Res:8275.0,45.0] || incident(u,oc)+ -> incident(u,oa)*. % 0.86/1.07 8295[6:Res:22.0,8277.0] || -> incident(c2,oa)*. % 0.86/1.07 8299[6:MRR:8295.0,7226.0] || -> . % 0.86/1.07 8300[5:Spt:8299.0,341.2] || -> line_equal(a2b2,ob)*l. % 0.86/1.07 8302[5:Res:8300.0,45.0] || incident(u,a2b2)*+ -> incident(u,ob). % 0.86/1.07 8319[5:Res:4540.0,8302.0] || -> incident(c1,ob)*. % 0.86/1.07 8321[5:Res:7880.0,8302.0] || -> incident(a1,ob)*. % 0.86/1.07 8324[5:MRR:87.0,8319.0] || incident(a1,ob)* -> . % 0.86/1.07 8325[5:MRR:8324.0,8321.0] || -> . % 0.86/1.07 8326[2:Spt:8325.0,35.0,4552.0] || incident(b2,a1c1)*+ -> . % 0.86/1.07 8327[2:Spt:8325.0,35.1] || -> incident(a1,b2c2)*. % 0.86/1.07 8328[2:MRR:4570.0,8327.0] || -> incident(c2,a1b1)*. % 0.86/1.07 8330[2:MRR:1991.2,8326.0] || incident(u,b2c2)*+ incident(u,a1b1) -> line_equal(a1b1,b2c2) point_equal(u,a1). % 0.86/1.07 8379[3:Spt:469.0,469.1,469.3] || incident(u,b2c2)*+ incident(u,a2c2) -> point_equal(u,c2). % 0.86/1.07 8383[3:Res:8327.0,8379.0] || incident(a1,a2c2)*+ -> point_equal(a1,c2). % 0.86/1.07 8388[4:Spt:723.0,723.1,723.3] || incident(u,oc)+ incident(u,ob)* -> point_equal(u,o). % 0.86/1.07 8389[4:Res:22.0,8388.0] || incident(c2,ob)*+ -> point_equal(c2,o). % 0.86/1.07 8397[5:Spt:655.0,655.1,655.3] || incident(u,ob)+ incident(u,b2c2)* -> point_equal(u,b2). % 0.86/1.07 8399[5:Res:19.0,8397.0] || incident(b1,b2c2)* -> point_equal(b1,b2). % 0.86/1.07 8400[5:Res:15.0,8397.0] || incident(o,b2c2)*+ -> point_equal(o,b2). % 0.86/1.07 8401[5:MRR:8399.1,72.0] || incident(b1,b2c2)*+ -> . % 0.86/1.07 8406[6:Spt:342.0,342.1,342.3] || incident(u,b2c2)*+ incident(u,a2b2) -> point_equal(u,b2). % 0.86/1.07 8415[7:Spt:594.0,594.1,594.3] || incident(u,oc)+ incident(u,b2c2)* -> point_equal(u,c2). % 0.86/1.07 8424[8:Spt:444.0,444.1,444.3] || incident(u,oa)+ incident(u,a2c2)* -> point_equal(u,a2). % 0.86/1.07 8426[8:Res:17.0,8424.0] || incident(a1,a2c2)* -> point_equal(a1,a2). % 0.86/1.07 8428[8:MRR:8426.1,74.0] || incident(a1,a2c2)*+ -> . % 0.86/1.07 8446[9:Spt:360.0,360.1,360.3] || incident(u,oc)+ incident(u,a1c1)* -> point_equal(u,c1). % 0.86/1.07 8447[9:Res:22.0,8446.0] || incident(c2,a1c1)* -> point_equal(c2,c1). % 0.86/1.07 8450[9:MRR:8447.1,55.0] || incident(c2,a1c1)*+ -> . % 0.86/1.07 8489[10:Spt:8330.0,8330.1,8330.3] || incident(u,b2c2)*+ incident(u,a1b1) -> point_equal(u,a1). % 0.86/1.07 8492[10:Res:12.0,8489.0] || incident(c2,a1b1)* -> point_equal(c2,a1). % 0.86/1.07 8494[10:MRR:8492.0,8328.0] || -> point_equal(c2,a1)*r. % 0.86/1.07 8500[10:Res:8494.0,44.1] || incident(a1,u)*+ -> incident(c2,u). % 0.86/1.07 8507[10:Res:6.0,8500.0] || -> incident(c2,a1c1)*. % 0.86/1.07 8510[10:MRR:8507.0,8450.0] || -> . % 0.86/1.07 8511[10:Spt:8510.0,8330.2] || -> line_equal(a1b1,b2c2)*r. % 0.86/1.07 8513[10:Res:8511.0,45.0] || incident(u,a1b1)+ -> incident(u,b2c2)*. % 0.86/1.07 8520[10:Res:3.0,8513.0] || -> incident(b1,b2c2)*. % 0.86/1.07 8524[10:MRR:8520.0,8401.0] || -> . % 0.86/1.07 8525[9:Spt:8524.0,360.2] || -> line_equal(a1c1,oc)*l. % 0.86/1.07 8527[9:Res:8525.0,45.0] || incident(u,a1c1)*+ -> incident(u,oc). % 0.86/1.07 8533[9:Res:6.0,8527.0] || -> incident(a1,oc)*. % 0.86/1.07 8546[9:Res:8533.0,8415.0] || incident(a1,b2c2)* -> point_equal(a1,c2). % 0.86/1.07 8559[9:MRR:8546.0,8327.0] || -> point_equal(a1,c2)*l. % 0.86/1.07 8648[9:Res:8559.0,44.1] || incident(c2,u)+ -> incident(a1,u)*. % 0.86/1.07 8655[9:Res:9.0,8648.0] || -> incident(a1,a2c2)*. % 0.86/1.07 8658[9:MRR:8655.0,8428.0] || -> . % 0.86/1.07 8659[8:Spt:8658.0,444.2] || -> line_equal(a2c2,oa)*l. % 0.86/1.07 8660[8:Res:8659.0,41.0] || -> line_equal(oa,a2c2)*r. % 0.86/1.07 8661[8:Res:8659.0,45.0] || incident(u,a2c2)*+ -> incident(u,oa). % 0.86/1.07 8662[8:NCh:43.2,43.0,8659.0,66.0] || line_equal(oa,a1c1)*r -> . % 0.86/1.07 8667[8:MRR:710.2,8662.0] || incident(u,a1c1)*+ incident(u,oa) -> point_equal(u,a1). % 0.86/1.07 8668[8:Res:26.0,8661.0] || -> incident(ac,oa)*. % 0.86/1.07 8685[8:Res:8660.0,45.0] || incident(u,oa)+ -> incident(u,a2c2)*. % 0.86/1.07 8692[8:Res:17.0,8685.0] || -> incident(a1,a2c2)*. % 0.86/1.07 8693[8:Res:14.0,8685.0] || -> incident(o,a2c2)*. % 0.86/1.07 8696[8:MRR:8383.0,8692.0] || -> point_equal(a1,c2)*l. % 0.86/1.07 8713[8:Res:25.0,8667.0] || incident(ac,oa)* -> point_equal(ac,a1). % 0.86/1.07 8716[8:MRR:8713.0,8668.0] || -> point_equal(ac,a1)*l. % 0.86/1.07 8718[8:Res:8693.0,292.0] || incident(o,a1c1)* -> point_equal(o,ac). % 0.86/1.07 8726[8:Res:8696.0,39.0] || -> point_equal(c2,a1)*r. % 0.86/1.07 8755[8:Res:8716.0,44.1] || incident(a1,u)+ -> incident(ac,u)*. % 0.86/1.07 8762[8:Res:8327.0,8755.0] || -> incident(ac,b2c2)*. % 0.86/1.07 8798[8:Res:8726.0,44.1] || incident(a1,u)*+ -> incident(c2,u). % 0.86/1.07 8808[8:Res:6.0,8798.0] || -> incident(c2,a1c1)*. % 0.86/1.07 8811[8:MRR:224.0,8808.0] || -> line_equal(oc,a1c1)*r. % 0.86/1.07 8812[8:MRR:294.0,8808.0] || -> point_equal(c2,ac)*r. % 0.86/1.07 8857[8:Res:8811.0,45.0] || incident(u,oc)+ -> incident(u,a1c1)*. % 0.86/1.07 8863[8:Res:16.0,8857.0] || -> incident(o,a1c1)*. % 0.86/1.07 8866[8:MRR:8718.0,8863.0] || -> point_equal(o,ac)*r. % 0.86/1.07 8880[8:Res:8812.0,44.1] || incident(ac,u)*+ -> incident(c2,u). % 0.86/1.07 8892[8:Res:8866.0,44.1] || incident(ac,u)*+ -> incident(o,u). % 0.86/1.07 8893[8:Res:8866.0,39.0] || -> point_equal(ac,o)*l. % 0.86/1.07 8902[8:Res:8762.0,8892.0] || -> incident(o,b2c2)*. % 0.86/1.07 8904[8:MRR:8400.0,8902.0] || -> point_equal(o,b2)*r. % 0.86/1.07 8940[8:Res:8893.0,44.1] || incident(o,u)+ -> incident(ac,u)*. % 0.86/1.07 9010[8:Res:8904.0,44.1] || incident(b2,u)*+ -> incident(o,u). % 0.86/1.07 9023[8:Res:5.0,9010.0] || -> incident(o,a2b2)*. % 0.86/1.07 9027[8:Res:9023.0,8940.0] || -> incident(ac,a2b2)*. % 0.86/1.07 9040[8:Res:9027.0,8880.0] || -> incident(c2,a2b2)*. % 0.86/1.07 9047[8:MRR:9040.0,100.0] || -> . % 0.86/1.07 9051[7:Spt:9047.0,594.2] || -> line_equal(b2c2,oc)*l. % 0.86/1.07 9052[7:Res:9051.0,41.0] || -> line_equal(oc,b2c2)*r. % 0.86/1.07 9092[7:Res:9052.0,45.0] || incident(u,oc)+ -> incident(u,b2c2)*. % 0.86/1.07 9099[7:Res:21.0,9092.0] || -> incident(c1,b2c2)*. % 0.86/1.07 9112[7:Res:9099.0,8406.0] || incident(c1,a2b2)* -> point_equal(c1,b2). % 0.86/1.07 9124[7:MRR:9112.0,4540.0] || -> point_equal(c1,b2)*l. % 0.86/1.07 9200[7:Res:9124.0,39.0] || -> point_equal(b2,c1)*r. % 0.86/1.07 9276[7:Res:9200.0,44.1] || incident(c1,u)*+ -> incident(b2,u). % 0.86/1.07 9287[7:Res:7.0,9276.0] || -> incident(b2,a1c1)*. % 0.86/1.07 9294[7:MRR:9287.0,8326.0] || -> . % 0.86/1.07 9295[6:Spt:9294.0,342.2] || -> line_equal(a2b2,b2c2)*r. % 0.92/1.09 9297[6:Res:9295.0,45.0] || incident(u,a2b2)+ -> incident(u,b2c2)*. % 0.92/1.09 9304[6:Res:4.0,9297.0] || -> incident(a2,b2c2)*. % 0.92/1.09 9307[6:MRR:9304.0,101.0] || -> . % 0.92/1.09 9309[5:Spt:9307.0,655.2] || -> line_equal(b2c2,ob)*l. % 0.92/1.09 9311[5:Res:9309.0,45.0] || incident(u,b2c2)*+ -> incident(u,ob). % 0.92/1.09 9312[5:NCh:43.2,43.0,9309.0,68.0] || line_equal(ob,b1c1)*r+ -> . % 0.92/1.09 9317[5:MRR:732.2,9312.0] || incident(u,b1c1)*+ incident(u,ob) -> point_equal(u,b1). % 0.92/1.09 9318[5:Res:24.0,9311.0] || -> incident(bc,ob)*. % 0.92/1.09 9320[5:Res:12.0,9311.0] || -> incident(c2,ob)*. % 0.92/1.09 9321[5:Res:8327.0,9311.0] || -> incident(a1,ob)*. % 0.92/1.09 9322[5:MRR:78.0,9320.0] || incident(a2,ob)*+ -> . % 0.92/1.09 9323[5:MRR:8389.0,9320.0] || -> point_equal(c2,o)*l. % 0.92/1.09 9347[5:Res:23.0,9317.0] || incident(bc,ob)* -> point_equal(bc,b1). % 0.92/1.09 9350[5:MRR:9347.0,9318.0] || -> point_equal(bc,b1)*l. % 0.92/1.09 9395[5:Res:9323.0,44.1] || incident(o,u)+ -> incident(c2,u)*. % 0.92/1.09 9401[5:Res:14.0,9395.0] || -> incident(c2,oa)*. % 0.92/1.09 9417[5:Res:9350.0,44.1] || incident(b1,u)+ -> incident(bc,u)*. % 0.92/1.09 9424[5:Res:3.0,9417.0] || -> incident(bc,a1b1)*. % 0.92/1.09 9425[5:MRR:98.1,9424.0] || incident(ac,a1b1)*+ -> . % 0.92/1.09 9485[6:Spt:711.0,711.1,711.3] || incident(u,a1b1)*+ incident(u,oa) -> point_equal(u,a1). % 0.92/1.09 9489[6:Res:8328.0,9485.0] || incident(c2,oa)* -> point_equal(c2,a1). % 0.92/1.09 9492[6:MRR:9489.0,9401.0] || -> point_equal(c2,a1)*r. % 0.92/1.09 9494[6:Res:9492.0,44.1] || incident(a1,u)*+ -> incident(c2,u). % 0.92/1.09 9502[6:Res:6.0,9494.0] || -> incident(c2,a1c1)*. % 0.92/1.09 9505[6:MRR:294.0,9502.0] || -> point_equal(c2,ac)*r. % 0.92/1.09 9594[6:Res:9505.0,39.0] || -> point_equal(ac,c2)*l. % 0.92/1.09 9693[6:Res:9594.0,44.1] || incident(c2,u)+ -> incident(ac,u)*. % 0.92/1.09 9706[6:Res:8328.0,9693.0] || -> incident(ac,a1b1)*. % 0.92/1.09 9708[6:MRR:9706.0,9425.0] || -> . % 0.92/1.09 9709[6:Spt:9708.0,711.2] || -> line_equal(oa,a1b1)*r. % 0.92/1.09 9711[6:Res:9709.0,45.0] || incident(u,oa)+ -> incident(u,a1b1)*. % 0.92/1.09 9715[6:Res:18.0,9711.0] || -> incident(a2,a1b1)*. % 0.92/1.09 9819[7:Spt:320.0,320.1,320.3] || incident(u,ob)+ incident(u,a1b1)* -> point_equal(u,b1). % 0.92/1.09 9825[7:Res:9321.0,9819.0] || incident(a1,a1b1)* -> point_equal(a1,b1). % 0.92/1.09 9828[7:MRR:9825.0,2.0] || -> point_equal(a1,b1)*l. % 0.92/1.10 9884[7:Res:9828.0,44.1] || incident(b1,u) -> incident(a1,u)*. % 0.92/1.10 9890[7:MRR:59.2,9884.1] || incident(c1,u)+ incident(b1,u)* -> . % 0.92/1.10 9892[7:Res:10.0,9890.0] || incident(b1,b1c1)* -> . % 0.92/1.10 9895[7:MRR:9892.0,11.0] || -> . % 0.92/1.10 9896[7:Spt:9895.0,320.2] || -> line_equal(a1b1,ob)*l. % 0.92/1.10 9898[7:Res:9896.0,45.0] || incident(u,a1b1)*+ -> incident(u,ob). % 0.92/1.10 9910[7:Res:9715.0,9898.0] || -> incident(a2,ob)*. % 0.92/1.10 9911[7:MRR:9910.0,9322.0] || -> . % 0.92/1.10 9912[4:Spt:9911.0,723.2] || -> line_equal(ob,oc)*l. % 0.92/1.10 9913[4:Res:9912.0,41.0] || -> line_equal(oc,ob)*r. % 0.92/1.10 9914[4:Res:9912.0,45.0] || incident(u,ob)*+ -> incident(u,oc). % 0.92/1.10 9918[4:Res:20.0,9914.0] || -> incident(b2,oc)*. % 0.92/1.10 9919[4:Res:19.0,9914.0] || -> incident(b1,oc)*. % 0.92/1.10 9933[4:Res:9919.0,71.0] || incident(b1,u)* incident(b2,u) incident(b2,oc) -> line_equal(oc,u). % 0.92/1.10 9937[4:MRR:9933.2,9918.0] || incident(b1,u)*+ incident(b2,u) -> line_equal(oc,u). % 0.92/1.10 9943[4:Res:9913.0,45.0] || incident(u,oc)+ -> incident(u,ob)*. % 0.92/1.10 9947[4:Res:22.0,9943.0] || -> incident(c2,ob)*. % 0.92/1.10 9948[4:Res:21.0,9943.0] || -> incident(c1,ob)*. % 0.92/1.10 9953[4:MRR:87.0,9948.0] || incident(a1,ob)*+ -> . % 0.92/1.10 10003[5:Spt:8330.0,8330.1,8330.3] || incident(u,b2c2)*+ incident(u,a1b1) -> point_equal(u,a1). % 0.92/1.10 10006[5:Res:12.0,10003.0] || incident(c2,a1b1)* -> point_equal(c2,a1). % 0.92/1.10 10008[5:MRR:10006.0,8328.0] || -> point_equal(c2,a1)*r. % 0.92/1.10 10010[5:Res:10008.0,39.0] || -> point_equal(a1,c2)*l. % 0.92/1.10 10042[5:Res:10010.0,44.1] || incident(c2,u)+ -> incident(a1,u)*. % 0.92/1.10 10049[5:Res:9947.0,10042.0] || -> incident(a1,ob)*. % 0.92/1.10 10056[5:MRR:10049.0,9953.0] || -> . % 0.92/1.10 10058[5:Spt:10056.0,8330.2] || -> line_equal(a1b1,b2c2)*r. % 0.92/1.10 10060[5:Res:10058.0,45.0] || incident(u,a1b1)+ -> incident(u,b2c2)*. % 0.92/1.10 10068[5:Res:3.0,10060.0] || -> incident(b1,b2c2)*. % 0.92/1.10 10083[5:Res:10068.0,9937.0] || incident(b2,b2c2)* -> line_equal(oc,b2c2). % 0.92/1.10 10095[5:MRR:10083.0,13.0] || -> line_equal(oc,b2c2)*r. % 0.92/1.10 10151[5:Res:10095.0,45.0] || incident(u,oc)+ -> incident(u,b2c2)*. % 0.92/1.10 10167[5:Res:21.0,10151.0] || -> incident(c1,b2c2)*. % 0.92/1.10 10176[5:Res:10167.0,59.0] || incident(b1,b2c2) incident(a1,b2c2)* -> . % 0.92/1.10 10186[5:MRR:10176.0,10176.1,10068.0,8327.0] || -> . % 0.92/1.10 10191[3:Spt:10186.0,469.2] || -> line_equal(a2c2,b2c2)*r. % 0.92/1.10 10193[3:Res:10191.0,45.0] || incident(u,a2c2)+ -> incident(u,b2c2)*. % 0.92/1.10 10200[3:Res:8.0,10193.0] || -> incident(a2,b2c2)*. % 0.92/1.10 10202[3:MRR:10200.0,101.0] || -> . % 0.92/1.10 % SZS output end Refutation % 0.92/1.10 Formulae used in the proof : goal_to_be_proved ia1b1 ib1a1 ia2b2 ib2a2 ia1c1 ic1a1 ia2c2 ic2a2 ic1b1 ib1c1 ic2b2 ib2c2 iooa ioob iooc ia1oa ia2oa ib1ob ib2ob ic1oc ic2oc ibc1 ibc2 iac1 iac2 iab1 iab2 notaa notbb notcc notbc notac notab gap_a gap_b gap_c symmetry_of_point_equal reflexivity_of_line_equal symmetry_of_line_equal transitivity_of_point_equal transitivity_of_line_equal pcon lcon t1in2 t2in1 triangle1 triangle2 goal_normal unique % 0.92/1.10 %------------------------------------------------------------------------------