%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GEO574+1 : TPTP v8.1.0. Released v7.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n024.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:19 EDT 2022 % Result : Theorem 34.95s 35.17s % Output : Refutation 35.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GEO574+1 : TPTP v8.1.0. Released v7.5.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n024.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sat Jun 18 13:09:02 EDT 2022 % 0.13/0.34 % CPUTime : % 34.95/35.17 % 34.95/35.17 SPASS V 3.9 % 34.95/35.17 SPASS beiseite: Proof found. % 34.95/35.17 % SZS status Theorem % 34.95/35.17 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 34.95/35.17 SPASS derived 29757 clauses, backtracked 12587 clauses, performed 2 splits and kept 27556 clauses. % 34.95/35.17 SPASS allocated 107188 KBytes. % 34.95/35.17 SPASS spent 0:0:34.79 on the problem. % 34.95/35.17 0:00:00.04 for the input. % 34.95/35.17 0:00:00.22 for the FLOTTER CNF translation. % 34.95/35.17 0:00:00.53 for inferences. % 34.95/35.17 0:00:00.09 for the backtracking. % 34.95/35.17 0:0:33.15 for the reduction. % 34.95/35.17 % 34.95/35.17 % 34.95/35.17 Here is a proof with depth 19, length 290 : % 34.95/35.17 % SZS output start Refutation % 34.95/35.17 1[0:Inp] || -> coll(skc9,skc13,skc12)*. % 34.95/35.17 2[0:Inp] || -> coll(skc11,skc13,skc8)*. % 34.95/35.17 3[0:Inp] || -> coll(skc10,skc12,skc11)*. % 34.95/35.17 4[0:Inp] || -> coll(skc10,skc8,skc9)*. % 34.95/35.17 7[0:Inp] || -> perp(skc9,skc8,skc13,skc12)*. % 34.95/35.17 8[0:Inp] || -> perp(skc11,skc12,skc13,skc8)*. % 34.95/35.17 9[0:Inp] || coll(u,v,w)*+ -> coll(u,w,v)*. % 34.95/35.17 10[0:Inp] || coll(u,v,w)*+ -> coll(v,u,w)*. % 34.95/35.17 13[0:Inp] || eqangle(skc14,skc13,skc13,skc12,skc12,skc13,skc13,skc15)* -> . % 34.95/35.17 14[0:Inp] || para(u,v,u,w)* -> coll(u,v,w). % 34.95/35.17 15[0:Inp] || midp(u,v,w) -> cong(u,v,u,w)*. % 34.95/35.17 16[0:Inp] || para(u,v,w,x)*+ -> para(u,v,x,w)*. % 34.95/35.17 17[0:Inp] || para(u,v,w,x)*+ -> para(w,x,u,v)*. % 34.95/35.17 18[0:Inp] || perp(u,v,w,x)*+ -> perp(u,v,x,w)*. % 34.95/35.17 19[0:Inp] || perp(u,v,w,x)*+ -> perp(w,x,u,v)*. % 34.95/35.17 21[0:Inp] || cyclic(u,v,w,x)*+ -> cyclic(u,w,v,x)*. % 34.95/35.17 22[0:Inp] || cyclic(u,v,w,x)*+ -> cyclic(v,u,w,x)*. % 34.95/35.17 23[0:Inp] || cong(u,v,w,x)*+ -> cong(u,v,x,w)*. % 34.95/35.17 24[0:Inp] || cong(u,v,w,x)*+ -> cong(w,x,u,v)*. % 34.95/35.17 27[0:Inp] || coll(u,v,w)*+ coll(u,v,x)* -> coll(x,w,u)*. % 34.95/35.17 34[0:Inp] || eqangle(u,v,w,x,y,z,w,x)* -> para(u,v,y,z). % 34.95/35.17 35[0:Inp] || para(u,v,w,x) -> eqangle(u,v,y,z,w,x,y,z)*. % 34.95/35.17 36[0:Inp] || cyclic(u,v,w,x) -> eqangle(w,u,w,v,x,u,x,v)*. % 34.95/35.17 38[0:Inp] || cong(u,v,u,w) -> eqangle(u,v,v,w,v,w,u,w)*. % 34.95/35.17 40[0:Inp] || coll(u,v,w) cong(u,v,u,w)* -> midp(u,v,w). % 34.95/35.17 41[0:Inp] || midp(u,v,w)* perp(v,x,x,w)*+ -> cong(v,u,x,u)*. % 34.95/35.17 43[0:Inp] || midp(u,v,w) perp(x,u,v,w)*+ -> cong(x,v,x,w)*. % 34.95/35.17 44[0:Inp] || para(u,v,w,x)*+ para(y,z,u,v)* -> para(y,z,w,x)*. % 34.95/35.17 45[0:Inp] || perp(u,v,w,x)*+ perp(y,z,u,v)* -> para(y,z,w,x)*. % 34.95/35.17 46[0:Inp] || perp(u,v,w,x)*+ para(y,z,u,v)* -> perp(y,z,w,x)*. % 34.95/35.17 47[0:Inp] || cong(u,v,u,w)*+ cong(u,v,u,x)* -> circle(u,v,x,w)*. % 34.95/35.17 48[0:Inp] || cyclic(u,v,w,x)*+ cyclic(u,v,w,y)* -> cyclic(v,w,y,x)*. % 34.95/35.17 50[0:Inp] || cong(u,v,w,v)*+ cong(u,x,w,x)* -> perp(u,w,x,v)*. % 34.95/35.17 56[0:Inp] || eqangle(u,v,w,x,y,z,x1,x2)*+ -> eqangle(w,x,u,v,x1,x2,y,z)*. % 34.95/35.17 57[0:Inp] || eqangle(u,v,w,x,y,z,x1,x2)*+ -> eqangle(y,z,x1,x2,u,v,w,x)*. % 34.95/35.17 58[0:Inp] || eqangle(u,v,w,x,y,z,x1,x2)*+ -> eqangle(u,v,y,z,w,x,x1,x2)*. % 34.95/35.17 63[0:Inp] || eqangle(u,v,u,w,x,v,x,w)* -> coll(u,x,v) cyclic(v,w,u,x). % 34.95/35.17 70[0:Inp] || perp(u,v,v,w)+ cyclic(u,w,v,x)* -> circle(skf35(v,w,u),u,w,v)*. % 34.95/35.17 76[0:Inp] || eqangle(u,v,w,x,w,x,u,v)* -> para(u,v,w,x) perp(u,v,w,x). % 34.95/35.17 78[0:Inp] || midp(u,v,w) circle(x,y,v,w) -> eqangle(y,v,y,w,x,v,x,u)*. % 34.95/35.17 80[0:Inp] || coll(u,v,w) eqangle(u,x,u,w,v,x,v,w)* -> cyclic(x,w,u,v). % 34.95/35.17 89[0:Inp] || midp(u,v,w)* para(v,x,w,y)*+ para(v,y,w,x)* -> midp(u,y,x)*. % 34.95/35.17 91[0:Inp] || para(u,v,w,x) cyclic(u,v,w,x) -> eqangle(u,x,w,x,w,x,w,v)*. % 34.95/35.17 93[0:Inp] || perp(u,v,v,w)*+ circle(u,v,x,y)* -> eqangle(v,w,v,x,y,v,y,x)*. % 34.95/35.17 96[0:Inp] || cyclic(u,v,w,x)*+ cong(u,x,v,x)* cong(u,w,v,w)* -> perp(w,u,u,x)*. % 34.95/35.17 108[0:Inp] || coll(u,v,w) circle(x,y,v,w) eqangle(y,v,y,w,x,v,x,u)* -> midp(u,v,w). % 34.95/35.17 116[0:Inp] || eqangle(u,v,w,x,y,z,x1,x2)*+ eqangle(x3,x4,x5,x6,u,v,w,x)* -> eqangle(x3,x4,x5,x6,y,z,x1,x2)*. % 34.95/35.17 122[0:Inp] || cyclic(u,v,w,x) cyclic(u,v,w,y) cyclic(u,v,w,z) eqangle(w,u,w,v,z,x,z,y)* -> cong(u,v,x,y). % 34.95/35.17 124[0:Res:4.0,27.0] || coll(skc10,skc8,u)* -> coll(skc9,u,skc10). % 34.95/35.17 125[0:Res:4.0,9.0] || -> coll(skc10,skc9,skc8)*. % 34.95/35.17 147[0:Res:3.0,27.0] || coll(skc10,skc12,u) -> coll(skc11,u,skc10)*. % 34.95/35.17 148[0:Res:3.0,9.0] || -> coll(skc10,skc11,skc12)*. % 34.95/35.17 170[0:Res:2.0,27.0] || coll(skc11,skc13,u)* -> coll(skc8,u,skc11). % 34.95/35.17 171[0:Res:2.0,9.0] || -> coll(skc11,skc8,skc13)*. % 34.95/35.17 172[0:Res:2.0,10.0] || -> coll(skc13,skc11,skc8)*. % 34.95/35.17 194[0:Res:1.0,9.0] || -> coll(skc9,skc12,skc13)*. % 34.95/35.17 195[0:Res:1.0,10.0] || -> coll(skc13,skc9,skc12)*. % 34.95/35.17 225[0:Res:8.0,19.0] || -> perp(skc13,skc8,skc11,skc12)*. % 34.95/35.17 230[0:Res:8.0,45.1] || perp(u,v,skc11,skc12) -> para(u,v,skc13,skc8)*. % 34.95/35.17 231[0:Res:8.0,46.1] || para(u,v,skc11,skc12)* -> perp(u,v,skc13,skc8). % 34.95/35.17 242[0:Res:7.0,45.0] || perp(skc13,skc12,u,v) -> para(skc9,skc8,u,v)*. % 34.95/35.17 243[0:Res:7.0,18.0] || -> perp(skc9,skc8,skc12,skc13)*. % 34.95/35.17 244[0:Res:7.0,19.0] || -> perp(skc13,skc12,skc9,skc8)*. % 34.95/35.17 249[0:Res:7.0,45.1] || perp(u,v,skc9,skc8) -> para(u,v,skc13,skc12)*. % 34.95/35.17 253[0:Res:2.0,170.0] || -> coll(skc8,skc8,skc11)*. % 34.95/35.17 255[0:Res:4.0,124.0] || -> coll(skc9,skc9,skc10)*. % 34.95/35.17 258[0:Res:148.0,10.0] || -> coll(skc11,skc10,skc12)*. % 34.95/35.17 295[0:Res:255.0,9.0] || -> coll(skc9,skc10,skc9)*. % 34.95/35.17 389[0:Res:244.0,18.0] || -> perp(skc13,skc12,skc8,skc9)*. % 34.95/35.17 396[0:Res:389.0,19.0] || -> perp(skc8,skc9,skc13,skc12)*. % 34.95/35.17 423[0:Res:148.0,27.0] || coll(skc10,skc11,u)*+ -> coll(u,skc12,skc10)*. % 34.95/35.17 425[0:Res:125.0,27.0] || coll(skc10,skc9,u)*+ -> coll(u,skc8,skc10)*. % 34.95/35.17 431[0:Res:195.0,27.0] || coll(skc13,skc9,u)*+ -> coll(u,skc12,skc13)*. % 34.95/35.17 432[0:Res:172.0,27.0] || coll(skc13,skc11,u)*+ -> coll(u,skc8,skc13)*. % 34.95/35.17 435[0:Res:194.0,27.0] || coll(skc9,skc12,u)*+ -> coll(u,skc13,skc9)*. % 34.95/35.17 436[0:Res:171.0,27.0] || coll(skc11,skc8,u)*+ -> coll(u,skc13,skc11)*. % 34.95/35.17 441[0:Res:258.0,27.0] || coll(skc11,skc10,u)*+ -> coll(u,skc12,skc11)*. % 34.95/35.17 445[0:Res:295.0,27.0] || coll(skc9,skc10,u)*+ -> coll(u,skc9,skc9)*. % 34.95/35.17 448[0:Res:253.0,27.0] || coll(skc8,skc8,u)*+ -> coll(u,skc11,skc8)*. % 34.95/35.17 510[0:Res:125.0,425.0] || -> coll(skc8,skc8,skc10)*. % 34.95/35.17 546[0:Res:195.0,431.0] || -> coll(skc12,skc12,skc13)*. % 34.95/35.17 596[0:Res:194.0,435.0] || -> coll(skc13,skc13,skc9)*. % 34.95/35.17 600[0:Res:596.0,9.0] || -> coll(skc13,skc9,skc13)*. % 34.95/35.17 603[0:Res:600.0,27.0] || coll(skc13,skc9,u)*+ -> coll(u,skc13,skc13)*. % 34.95/35.17 615[0:Res:38.1,34.0] || cong(u,u,u,v)* -> para(u,u,u,v). % 34.95/35.17 617[0:Res:36.1,34.0] || cyclic(u,v,w,w)*+ -> para(w,u,w,u)*. % 34.95/35.17 626[0:Res:147.1,436.0] || coll(skc10,skc12,skc8) -> coll(skc10,skc13,skc11)*. % 34.95/35.17 635[0:Res:396.0,43.1] || midp(skc9,skc13,skc12) -> cong(skc8,skc13,skc8,skc12)*. % 34.95/35.17 643[0:Res:243.0,43.1] || midp(skc8,skc12,skc13) -> cong(skc9,skc12,skc9,skc13)*. % 34.95/35.17 688[0:Res:626.1,10.0] || coll(skc10,skc12,skc8) -> coll(skc13,skc10,skc11)*. % 34.95/35.17 690[0:Res:688.1,9.0] || coll(skc10,skc12,skc8) -> coll(skc13,skc11,skc10)*. % 34.95/35.17 699[0:Res:690.1,10.0] || coll(skc10,skc12,skc8) -> coll(skc11,skc13,skc10)*. % 34.95/35.17 703[0:Res:699.1,9.0] || coll(skc10,skc12,skc8) -> coll(skc11,skc10,skc13)*. % 34.95/35.17 705[0:Res:15.1,47.0] || midp(u,v,w) cong(u,v,u,x)*+ -> circle(u,v,x,w)*. % 34.95/35.17 780[0:Res:703.1,441.0] || coll(skc10,skc12,skc8) -> coll(skc13,skc12,skc11)*. % 34.95/35.17 815[0:Res:780.1,9.0] || coll(skc10,skc12,skc8) -> coll(skc13,skc11,skc12)*. % 34.95/35.17 820[0:Res:815.1,432.0] || coll(skc10,skc12,skc8) -> coll(skc12,skc8,skc13)*. % 34.95/35.17 867[0:Res:820.1,10.0] || coll(skc10,skc12,skc8)* -> coll(skc8,skc12,skc13). % 34.95/35.17 1072[0:Res:35.1,63.0] || para(u,v,u,v)*+ -> coll(u,u,v) cyclic(v,w,u,u)*. % 34.95/35.17 1144[0:Res:35.1,58.0] || para(u,v,w,x) -> eqangle(u,v,w,x,y,z,y,z)*. % 34.95/35.17 1175[0:Res:38.1,56.0] || cong(u,v,u,w) -> eqangle(v,w,u,v,u,w,v,w)*. % 34.95/35.17 1176[0:Res:35.1,56.0] || para(u,v,w,x) -> eqangle(y,z,u,v,y,z,w,x)*. % 34.95/35.17 1210[0:Res:295.0,445.0] || -> coll(skc9,skc9,skc9)*. % 34.95/35.17 1221[0:Res:510.0,448.0] || -> coll(skc10,skc11,skc8)*. % 34.95/35.17 1226[0:Res:1221.0,423.0] || -> coll(skc8,skc12,skc10)*. % 34.95/35.17 1281[0:Res:1226.0,9.0] || -> coll(skc8,skc10,skc12)*. % 34.95/35.17 1359[0:Res:1281.0,10.0] || -> coll(skc10,skc8,skc12)*. % 34.95/35.17 1401[0:Res:35.1,80.1] || para(u,v,u,v)*+ coll(u,u,w) -> cyclic(v,w,u,u)*. % 34.95/35.17 1412[0:Res:1359.0,9.0] || -> coll(skc10,skc12,skc8)*. % 34.95/35.17 1428[0:MRR:867.0,1412.0] || -> coll(skc8,skc12,skc13)*. % 34.95/35.17 1481[0:Res:78.2,58.0] || midp(u,v,w) circle(x,y,v,w) -> eqangle(y,v,x,v,y,w,x,u)*. % 34.95/35.17 1500[0:Res:38.1,76.0] || cong(u,v,u,v)*+ -> para(u,v,v,v)* perp(u,v,v,v). % 34.95/35.17 1640[0:Res:91.2,57.0] || para(u,v,w,x) cyclic(u,v,w,x) -> eqangle(w,x,w,v,u,x,w,x)*. % 34.95/35.17 2556[0:Res:78.2,116.0] || midp(u,v,w)* circle(x,y,v,w)* eqangle(z,x1,x2,x3,y,v,y,w)*+ -> eqangle(z,x1,x2,x3,x,v,x,u)*. % 34.95/35.17 2661[0:Res:600.0,603.0] || -> coll(skc13,skc13,skc13)*. % 34.95/35.17 2715[0:Res:35.1,122.3] || para(u,v,u,w)*+ cyclic(v,x,u,w)* cyclic(v,x,u,x)* cyclic(v,x,u,u)* -> cong(v,x,w,x)*. % 34.95/35.17 2717[0:Res:91.2,122.3] || para(u,v,u,w)+ cyclic(u,v,u,w)* cyclic(w,w,u,w)* cyclic(w,w,u,v)* cyclic(w,w,u,u)* -> cong(w,w,w,v)*. % 34.95/35.17 2718[0:Res:36.1,122.3] || cyclic(u,v,w,x)* cyclic(u,v,w,u)* cyclic(u,v,w,v)* cyclic(u,v,w,x)* -> cong(u,v,u,v)*. % 34.95/35.17 2720[0:Obv:2718.0] || cyclic(u,v,w,u)* cyclic(u,v,w,v)* cyclic(u,v,w,x)* -> cong(u,v,u,v)*. % 34.95/35.17 2721[0:Con:2720.2] || cyclic(u,v,w,u)*+ cyclic(u,v,w,v)* -> cong(u,v,u,v)*. % 34.95/35.17 3102[0:Res:242.1,16.0] || perp(skc13,skc12,u,v) -> para(skc9,skc8,v,u)*. % 34.95/35.17 3202[0:Res:230.1,17.0] || perp(u,v,skc11,skc12) -> para(skc13,skc8,u,v)*. % 34.95/35.17 3296[0:Res:15.1,615.0] || midp(u,u,v) -> para(u,u,u,v)*. % 34.95/35.17 4151[0:Res:635.1,24.0] || midp(skc9,skc13,skc12) -> cong(skc8,skc12,skc8,skc13)*. % 34.95/35.17 4233[0:Res:643.1,23.0] || midp(skc8,skc12,skc13) -> cong(skc9,skc12,skc13,skc9)*. % 34.95/35.17 4728[0:Res:4151.1,40.1] || midp(skc9,skc13,skc12)* coll(skc8,skc12,skc13) -> midp(skc8,skc12,skc13). % 34.95/35.17 4732[0:MRR:4728.1,1428.0] || midp(skc9,skc13,skc12)* -> midp(skc8,skc12,skc13). % 34.95/35.17 4788[0:Res:4233.1,24.0] || midp(skc8,skc12,skc13) -> cong(skc13,skc9,skc9,skc12)*. % 34.95/35.17 4948[0:Res:1144.1,63.0] || para(u,v,u,v)* -> coll(u,w,v) cyclic(v,v,u,w)*. % 34.95/35.17 4959[0:Res:1144.1,80.1] || para(u,v,u,v)* coll(u,w,v) -> cyclic(v,v,u,w)*. % 34.95/35.17 4973[0:MRR:4959.1,4948.1] || para(u,v,u,v)*+ -> cyclic(v,v,u,w)*. % 34.95/35.17 5139[0:Res:4788.1,23.0] || midp(skc8,skc12,skc13) -> cong(skc13,skc9,skc12,skc9)*. % 34.95/35.17 5202[0:Res:1175.1,108.2] || cong(u,u,u,v)* coll(v,v,u) circle(u,u,v,u) -> midp(v,v,u)*. % 34.95/35.17 5225[0:Res:1176.1,34.0] || para(u,v,u,v)*+ -> para(w,x,w,x)*. % 34.95/35.17 5480[0:Res:15.1,705.1] || midp(u,v,w) midp(u,v,x) -> circle(u,v,w,x)*. % 34.95/35.17 5525[0:Res:5139.1,50.0] || midp(skc8,skc12,skc13) cong(skc13,u,skc12,u)* -> perp(skc13,skc12,u,skc9). % 34.95/35.17 5669[0:Res:249.1,1401.0] || perp(skc13,skc12,skc9,skc8) coll(skc13,skc13,u) -> cyclic(skc12,u,skc13,skc13)*. % 34.95/35.17 5670[0:Res:230.1,1401.0] || perp(skc13,skc8,skc11,skc12) coll(skc13,skc13,u) -> cyclic(skc8,u,skc13,skc13)*. % 34.95/35.17 5671[0:Res:242.1,1401.0] || perp(skc13,skc12,skc9,skc8) coll(skc9,skc9,u) -> cyclic(skc8,u,skc9,skc9)*. % 34.95/35.17 5673[0:MRR:5669.0,244.0] || coll(skc13,skc13,u) -> cyclic(skc12,u,skc13,skc13)*. % 34.95/35.17 5674[0:MRR:5670.0,225.0] || coll(skc13,skc13,u) -> cyclic(skc8,u,skc13,skc13)*. % 34.95/35.17 5675[0:MRR:5671.0,244.0] || coll(skc9,skc9,u) -> cyclic(skc8,u,skc9,skc9)*. % 34.95/35.17 5889[0:Res:5673.1,22.0] || coll(skc13,skc13,u) -> cyclic(u,skc12,skc13,skc13)*. % 34.95/35.17 5890[0:Res:5673.1,617.0] || coll(skc13,skc13,u)*+ -> para(skc13,skc12,skc13,skc12)*. % 34.95/35.17 5892[0:Res:596.0,5890.0] || -> para(skc13,skc12,skc13,skc12)*. % 34.95/35.17 5901[0:Res:5892.0,16.0] || -> para(skc13,skc12,skc12,skc13)*. % 34.95/35.17 5910[0:Res:5892.0,89.1] || midp(u,skc13,skc13)* para(skc13,skc12,skc13,skc12)* -> midp(u,skc12,skc12). % 34.95/35.17 5912[0:MRR:5910.1,5892.0] || midp(u,skc13,skc13)* -> midp(u,skc12,skc12). % 34.95/35.17 5915[0:Res:5901.0,17.0] || -> para(skc12,skc13,skc13,skc12)*. % 34.95/35.17 5929[0:Res:5915.0,16.0] || -> para(skc12,skc13,skc12,skc13)*. % 34.95/35.17 5945[0:Res:5929.0,1401.0] || coll(skc12,skc12,u) -> cyclic(skc13,u,skc12,skc12)*. % 34.95/35.17 5972[0:Res:5674.1,617.0] || coll(skc13,skc13,u)*+ -> para(skc13,skc8,skc13,skc8)*. % 34.95/35.17 5974[0:Res:596.0,5972.0] || -> para(skc13,skc8,skc13,skc8)*. % 34.95/35.17 5983[0:Res:5974.0,16.0] || -> para(skc13,skc8,skc8,skc13)*. % 34.95/35.17 5997[0:Res:5983.0,17.0] || -> para(skc8,skc13,skc13,skc8)*. % 34.95/35.17 6009[0:Res:5997.0,16.0] || -> para(skc8,skc13,skc8,skc13)*. % 34.95/35.17 6032[0:Res:6009.0,89.1] || midp(u,skc8,skc8) para(skc8,skc13,skc8,skc13)* -> midp(u,skc13,skc13)*. % 34.95/35.17 6034[0:MRR:6032.1,6009.0] || midp(u,skc8,skc8) -> midp(u,skc13,skc13)*. % 34.95/35.17 6044[0:Res:6034.1,5912.0] || midp(u,skc8,skc8) -> midp(u,skc12,skc12)*. % 34.95/35.17 6068[0:Res:5675.1,22.0] || coll(skc9,skc9,u) -> cyclic(u,skc8,skc9,skc9)*. % 34.95/35.17 6069[0:Res:5675.1,617.0] || coll(skc9,skc9,u)*+ -> para(skc9,skc8,skc9,skc8)*. % 34.95/35.17 6072[0:Res:255.0,6069.0] || -> para(skc9,skc8,skc9,skc8)*. % 34.95/35.17 6080[0:Res:6072.0,16.0] || -> para(skc9,skc8,skc8,skc9)*. % 34.95/35.17 6090[0:Res:6072.0,89.1] || midp(u,skc9,skc9)* para(skc9,skc8,skc9,skc8)* -> midp(u,skc8,skc8). % 34.95/35.17 6092[0:MRR:6090.1,6072.0] || midp(u,skc9,skc9)* -> midp(u,skc8,skc8). % 34.95/35.17 6101[0:Res:6080.0,17.0] || -> para(skc8,skc9,skc9,skc8)*. % 34.95/35.17 6113[0:Res:6101.0,16.0] || -> para(skc8,skc9,skc8,skc9)*. % 34.95/35.17 6354[0:Res:5889.1,2721.0] || coll(skc13,skc13,skc13) cyclic(skc13,skc12,skc13,skc12)* -> cong(skc13,skc12,skc13,skc12). % 34.95/35.17 6356[0:MRR:6354.0,2661.0] || cyclic(skc13,skc12,skc13,skc12)* -> cong(skc13,skc12,skc13,skc12). % 34.95/35.17 6364[0:Res:5945.1,22.0] || coll(skc12,skc12,u) -> cyclic(u,skc13,skc12,skc12)*. % 34.95/35.17 6443[0:Res:6068.1,21.0] || coll(skc9,skc9,u) -> cyclic(u,skc9,skc8,skc9)*. % 34.95/35.17 6537[0:Res:6364.1,21.0] || coll(skc12,skc12,u) -> cyclic(u,skc12,skc13,skc12)*. % 34.95/35.17 6626[0:Res:6443.1,2721.0] || coll(skc9,skc9,skc9) cyclic(skc9,skc9,skc8,skc9)* -> cong(skc9,skc9,skc9,skc9). % 34.95/35.17 6627[0:MRR:6626.0,1210.0] || cyclic(skc9,skc9,skc8,skc9)* -> cong(skc9,skc9,skc9,skc9). % 34.95/35.17 8260[0:Res:3296.1,17.0] || midp(u,u,v) -> para(u,v,u,u)*. % 34.95/35.17 8271[0:Res:3296.1,89.1] || midp(u,u,v) midp(w,u,u)* para(u,v,u,u)* -> midp(w,v,u)*. % 34.95/35.17 8278[0:MRR:8271.2,8260.1] || midp(u,u,v)* midp(w,u,u)* -> midp(w,v,u)*. % 34.95/35.17 9253[0:Res:1481.2,116.0] || midp(u,v,w)* circle(x,y,v,w)* eqangle(z,x1,x2,x3,y,v,x,v)* -> eqangle(z,x1,x2,x3,y,w,x,u)*. % 34.95/35.17 9456[0:Res:6537.1,6356.0] || coll(skc12,skc12,skc13) -> cong(skc13,skc12,skc13,skc12)*. % 34.95/35.17 9460[0:MRR:9456.0,546.0] || -> cong(skc13,skc12,skc13,skc12)*. % 34.95/35.17 9477[0:Res:9460.0,23.0] || -> cong(skc13,skc12,skc12,skc13)*. % 34.95/35.17 9482[0:Res:9460.0,1500.0] || -> para(skc13,skc12,skc12,skc12)* perp(skc13,skc12,skc12,skc12). % 34.95/35.17 9566[0:Res:9477.0,24.0] || -> cong(skc12,skc13,skc13,skc12)*. % 34.95/35.17 9569[0:Res:9566.0,23.0] || -> cong(skc12,skc13,skc12,skc13)*. % 34.95/35.17 9593[0:Res:9569.0,1500.0] || -> para(skc12,skc13,skc13,skc13)* perp(skc12,skc13,skc13,skc13). % 34.95/35.17 10192[0:Res:1640.2,116.0] || para(u,v,w,x) cyclic(u,v,w,x)* eqangle(y,z,x1,x2,w,x,w,v)* -> eqangle(y,z,x1,x2,u,x,w,x)*. % 34.95/35.17 13771[0:Res:1144.1,2556.2] || para(u,v,w,x) midp(y,z,z)* circle(x1,x2,z,z)* -> eqangle(u,v,w,x,x1,z,x1,y)*. % 34.95/35.17 14355[1:Spt:9482.0] || -> para(skc13,skc12,skc12,skc12)*. % 34.95/35.17 14360[1:Res:14355.0,17.0] || -> para(skc12,skc12,skc13,skc12)*. % 34.95/35.17 14387[1:Res:14360.0,16.0] || -> para(skc12,skc12,skc12,skc13)*. % 34.95/35.17 14437[1:Res:14387.0,17.0] || -> para(skc12,skc13,skc12,skc12)*. % 34.95/35.17 14444[1:Res:14387.0,89.1] || midp(u,skc12,skc12) para(skc12,skc13,skc12,skc12)* -> midp(u,skc13,skc12)*. % 34.95/35.17 14452[1:MRR:14444.1,14437.0] || midp(u,skc12,skc12) -> midp(u,skc13,skc12)*. % 34.95/35.17 14457[1:Res:14437.0,2715.0] || cyclic(skc13,u,skc12,skc12)* cyclic(skc13,u,skc12,u)* cyclic(skc13,u,skc12,skc12)* -> cong(skc13,u,skc12,u). % 34.95/35.17 14483[1:Obv:14457.0] || cyclic(skc13,u,skc12,u)* cyclic(skc13,u,skc12,skc12)* -> cong(skc13,u,skc12,u). % 34.95/35.17 14601[1:Res:14452.1,4732.0] || midp(skc9,skc12,skc12)* -> midp(skc8,skc12,skc13). % 34.95/35.17 14606[1:Res:6044.1,14601.0] || midp(skc9,skc8,skc8)* -> midp(skc8,skc12,skc13). % 34.95/35.17 14911[2:Spt:9593.0] || -> para(skc12,skc13,skc13,skc13)*. % 34.95/35.17 14916[2:Res:14911.0,17.0] || -> para(skc13,skc13,skc12,skc13)*. % 34.95/35.17 14938[2:Res:14916.0,16.0] || -> para(skc13,skc13,skc13,skc12)*. % 34.95/35.17 14971[2:Res:14938.0,2715.0] || cyclic(skc13,u,skc13,skc12) cyclic(skc13,u,skc13,u)* cyclic(skc13,u,skc13,skc13)* -> cong(skc13,u,skc12,u). % 34.95/35.17 15448[0:Res:3102.1,14.0] || perp(skc13,skc12,u,skc9)* -> coll(skc9,skc8,u). % 34.95/35.17 15459[0:Res:3102.1,231.0] || perp(skc13,skc12,skc12,skc11)* -> perp(skc9,skc8,skc13,skc8). % 34.95/35.17 15727[0:Res:3202.1,44.0] || perp(u,v,skc11,skc12) para(w,x,skc13,skc8)* -> para(w,x,u,v)*. % 34.95/35.17 16068[0:Res:6113.0,4973.0] || -> cyclic(skc9,skc9,skc8,u)*. % 34.95/35.17 16100[0:MRR:6627.0,16068.0] || -> cong(skc9,skc9,skc9,skc9)*. % 34.95/35.17 16382[0:Res:16100.0,40.1] || coll(skc9,skc9,skc9) -> midp(skc9,skc9,skc9)*. % 34.95/35.17 16400[0:MRR:16382.0,1210.0] || -> midp(skc9,skc9,skc9)*. % 34.95/35.17 16414[0:Res:16400.0,6092.0] || -> midp(skc9,skc8,skc8)*. % 34.95/35.17 16415[1:MRR:14606.0,16414.0] || -> midp(skc8,skc12,skc13)*. % 34.95/35.17 16460[1:MRR:5525.0,16415.0] || cong(skc13,u,skc12,u)* -> perp(skc13,skc12,u,skc9). % 34.95/35.17 17415[0:Res:5892.0,5225.0] || -> para(u,v,u,v)*. % 34.95/35.17 17443[0:MRR:1072.0,17415.0] || -> coll(u,u,v) cyclic(v,w,u,u)*. % 34.95/35.17 17444[0:MRR:1401.0,17415.0] || coll(u,u,v) -> cyclic(w,v,u,u)*. % 34.95/35.17 17446[0:MRR:4973.0,17415.0] || -> cyclic(u,u,v,w)*. % 34.95/35.17 17457[0:MRR:2717.4,2717.3,2717.2,17446.0] || para(u,v,u,w)+ cyclic(u,v,u,w)* -> cong(w,w,w,v)*. % 34.95/35.17 17687[0:Res:17443.1,22.0] || -> coll(u,u,v) cyclic(w,v,u,u)*. % 34.95/35.17 17734[0:MRR:17687.0,17444.0] || -> cyclic(u,v,w,w)*. % 34.95/35.17 17863[2:MRR:14971.2,17734.0] || cyclic(skc13,u,skc13,skc12)* cyclic(skc13,u,skc13,u)* -> cong(skc13,u,skc12,u). % 34.95/35.17 17864[1:MRR:14483.1,17734.0] || cyclic(skc13,u,skc12,u)* -> cong(skc13,u,skc12,u). % 34.95/35.17 19820[0:Res:17446.0,96.0] || cong(u,v,u,v)* cong(u,w,u,w)* -> perp(w,u,u,v)*. % 34.95/35.17 19821[0:Res:17446.0,48.0] || cyclic(u,u,v,w)* -> cyclic(u,v,w,x)*. % 35.16/35.35 19823[0:Res:17446.0,21.0] || -> cyclic(u,v,u,w)*. % 35.16/35.35 19829[0:MRR:17457.1,19823.0] || para(u,v,u,w)* -> cong(w,w,w,v)*. % 35.16/35.35 19878[2:MRR:17863.0,17863.1,19823.0] || -> cong(skc13,u,skc12,u)*. % 35.16/35.35 19921[2:MRR:16460.0,19878.0] || -> perp(skc13,skc12,u,skc9)*. % 35.16/35.35 19934[2:MRR:15448.0,19921.0] || -> coll(skc9,skc8,u)*. % 35.16/35.35 20101[0:MRR:19821.0,17446.0] || -> cyclic(u,v,w,x)*. % 35.16/35.35 20105[0:MRR:122.2,122.1,122.0,20101.0] || eqangle(u,v,u,w,x,y,x,z)* -> cong(v,w,y,z). % 35.16/35.35 20120[0:MRR:70.1,20101.0] || perp(u,v,v,w) -> circle(skf35(v,w,u),u,w,v)*. % 35.16/35.35 20121[0:MRR:2721.1,2721.0,20101.0] || -> cong(u,v,u,v)*. % 35.16/35.35 20153[0:MRR:10192.1,20101.0] || para(u,v,w,x)* eqangle(y,z,x1,x2,w,x,w,v)* -> eqangle(y,z,x1,x2,u,x,w,x)*. % 35.16/35.35 20537[0:MRR:19820.0,19820.1,20121.0,20121.0] || -> perp(u,v,v,w)*. % 35.16/35.35 20550[0:MRR:93.0,20537.0] || circle(u,v,w,x)*+ -> eqangle(v,y,v,w,x,v,x,w)*. % 35.16/35.35 20553[0:MRR:41.1,20537.0] || midp(u,v,w)*+ -> cong(v,u,x,u)*. % 35.16/35.35 20559[0:MRR:20120.0,20537.0] || -> circle(skf35(u,v,w),w,v,u)*. % 35.16/35.35 20791[2:Res:19934.0,27.0] || coll(skc9,skc8,u)* -> coll(u,v,skc9)*. % 35.16/35.35 20890[2:MRR:20791.0,19934.0] || -> coll(u,v,skc9)*. % 35.16/35.35 21022[2:Res:20890.0,9.0] || -> coll(u,skc9,v)*. % 35.16/35.35 22296[0:Res:20559.0,20550.0] || -> eqangle(u,v,u,w,x,u,x,w)*. % 35.16/35.35 22416[0:Res:20121.0,47.0] || cong(u,v,u,w)* -> circle(u,v,w,v)*. % 35.16/35.35 22417[0:Res:20121.0,40.1] || coll(u,v,v) -> midp(u,v,v)*. % 35.16/35.35 22427[0:MRR:5202.2,22416.1] || cong(u,u,u,v)* coll(v,v,u) -> midp(v,v,u)*. % 35.16/35.35 22700[2:Res:21022.0,27.0] || coll(u,skc9,v)* -> coll(v,w,u)*. % 35.16/35.35 22723[2:MRR:22700.0,21022.0] || -> coll(u,v,w)*. % 35.16/35.35 22827[2:MRR:22417.0,22723.0] || -> midp(u,v,v)*. % 35.16/35.35 22864[2:MRR:22427.1,22723.0] || cong(u,u,u,v)* -> midp(v,v,u)*. % 35.16/35.35 22888[2:MRR:13771.1,22827.0] || para(u,v,w,x) circle(y,z,x1,x1)* -> eqangle(u,v,w,x,y,x1,y,x2)*. % 35.16/35.35 22923[2:MRR:8278.1,22827.0] || midp(u,u,v)* -> midp(w,v,u)*. % 35.16/35.35 23218[2:Res:22827.0,20553.0] || -> cong(u,v,w,v)*. % 35.16/35.35 23224[2:MRR:50.1,50.0,23218.0] || -> perp(u,v,w,x)*. % 35.16/35.35 23235[2:MRR:45.1,45.0,23224.0] || -> para(u,v,w,x)*. % 35.16/35.35 23614[2:MRR:20153.0,23235.0] || eqangle(u,v,w,x,y,z,y,x1)* -> eqangle(u,v,w,x,x2,z,y,z)*. % 35.16/35.35 23642[2:MRR:22888.0,23235.0] || circle(u,v,w,w)* -> eqangle(x,y,z,x1,u,w,u,x2)*. % 35.16/35.35 23657[2:MRR:19829.0,23235.0] || -> cong(u,u,u,v)*. % 35.16/35.35 23723[2:MRR:22864.0,23657.0] || -> midp(u,u,v)*. % 35.16/35.35 23738[2:MRR:22923.0,23723.0] || -> midp(u,v,w)*. % 35.16/35.35 23839[2:MRR:5480.1,5480.0,23738.0] || -> circle(u,v,w,x)*. % 35.16/35.35 23865[2:MRR:9253.0,23738.0] || circle(u,v,w,x)* eqangle(y,z,x1,x2,v,w,u,w)* -> eqangle(y,z,x1,x2,v,x,u,x3)*. % 35.16/35.35 24300[2:MRR:23642.0,23839.0] || -> eqangle(u,v,w,x,y,z,y,x1)*. % 35.16/35.35 24307[2:MRR:23614.0,24300.0] || -> eqangle(u,v,w,x,y,z,x1,z)*. % 35.16/35.35 24313[2:MRR:23865.0,23865.1,23839.0,24307.0] || -> eqangle(u,v,w,x,y,z,x1,x2)*. % 35.16/35.35 24314[2:UnC:24313.0,13.0] || -> . % 35.16/35.35 24315[2:Spt:24314.0,9593.0,14911.0] || para(skc12,skc13,skc13,skc13)* -> . % 35.16/35.35 24316[2:Spt:24314.0,9593.1] || -> perp(skc12,skc13,skc13,skc13)*. % 35.16/35.35 24322[1:MRR:17864.0,20101.0] || -> cong(skc13,u,skc12,u)*. % 35.16/35.35 24326[1:MRR:16460.0,24322.0] || -> perp(skc13,skc12,u,skc9)*. % 35.16/35.35 24327[1:MRR:15448.0,24326.0] || -> coll(skc9,skc8,u)*. % 35.16/35.35 25821[1:Res:24327.0,27.0] || coll(skc9,skc8,u)* -> coll(u,v,skc9)*. % 35.16/35.35 25931[1:MRR:25821.0,24327.0] || -> coll(u,v,skc9)*. % 35.16/35.35 26005[1:Res:25931.0,9.0] || -> coll(u,skc9,v)*. % 35.16/35.35 26980[1:Res:26005.0,27.0] || coll(u,skc9,v)* -> coll(v,w,u)*. % 35.16/35.35 27005[1:MRR:26980.0,26005.0] || -> coll(u,v,w)*. % 35.16/35.35 27043[1:MRR:22417.0,27005.0] || -> midp(u,v,v)*. % 35.16/35.35 27472[1:Res:27043.0,20553.0] || -> cong(u,v,w,v)*. % 35.16/35.35 27474[1:MRR:50.1,50.0,27472.0] || -> perp(u,v,w,x)*. % 35.16/35.35 27585[1:MRR:230.0,27474.0] || -> para(u,v,skc13,skc8)*. % 35.16/35.35 27592[1:MRR:15727.0,27474.0] || para(u,v,skc13,skc8)* -> para(u,v,w,x)*. % 35.16/35.35 27841[1:MRR:27592.0,27585.0] || -> para(u,v,w,x)*. % 35.16/35.35 27842[2:UnC:27841.0,24315.0] || -> . % 35.16/35.35 27843[1:Spt:27842.0,9482.0,14355.0] || para(skc13,skc12,skc12,skc12)* -> . % 35.16/35.35 27844[1:Spt:27842.0,9482.1] || -> perp(skc13,skc12,skc12,skc12)*. % 35.16/35.35 27845[0:MRR:15459.0,20537.0] || -> perp(skc9,skc8,skc13,skc8)*. % 35.16/35.35 29551[0:Res:27845.0,45.0] || perp(u,v,skc9,skc8) -> para(u,v,skc13,skc8)*. % 35.16/35.35 30386[0:Res:22296.0,20105.0] || -> cong(u,v,w,v)*. % 35.16/35.35 30410[0:MRR:50.1,50.0,30386.0] || -> perp(u,v,w,x)*. % 35.16/35.35 30758[0:MRR:29551.0,30410.0] || -> para(u,v,skc13,skc8)*. % 35.16/35.35 30805[0:MRR:15727.0,30410.0] || para(u,v,skc13,skc8)* -> para(u,v,w,x)*. % 35.16/35.35 31650[0:MRR:30805.0,30758.0] || -> para(u,v,w,x)*. % 35.16/35.35 31651[1:UnC:31650.0,27843.0] || -> . % 35.16/35.35 % SZS output end Refutation % 35.16/35.35 Formulae used in the proof : exemplo6GDDFULL214036 ruleD1 ruleD2 ruleD66 ruleD68 ruleD4 ruleD5 ruleD7 ruleD8 ruleD15 ruleD16 ruleD23 ruleD24 ruleD3 ruleD39 ruleD40 ruleD41 ruleD46 ruleD67 ruleD52 ruleD55 ruleD6 ruleD9 ruleD10 ruleD12 ruleD17 ruleD56 ruleD19 ruleD20 ruleD21 ruleD42a ruleX14 ruleD72 ruleD50 ruleD42b ruleD64 ruleD54 ruleD48 ruleD57 ruleD51 ruleD22 ruleD43 % 35.16/35.35 %------------------------------------------------------------------------------