%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GEO196+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 06:23:15 EDT 2022 % Result : Theorem 0.55s 0.76s % Output : Refutation 0.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GEO196+1 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n019.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jun 17 18:05:54 EDT 2022 % 0.12/0.34 % CPUTime : % 0.55/0.76 % 0.55/0.76 SPASS V 3.9 % 0.55/0.76 SPASS beiseite: Proof found. % 0.55/0.76 % SZS status Theorem % 0.55/0.76 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.55/0.76 SPASS derived 1633 clauses, backtracked 8 clauses, performed 4 splits and kept 853 clauses. % 0.55/0.76 SPASS allocated 85991 KBytes. % 0.55/0.76 SPASS spent 0:00:00.41 on the problem. % 0.55/0.76 0:00:00.03 for the input. % 0.55/0.76 0:00:00.03 for the FLOTTER CNF translation. % 0.55/0.76 0:00:00.03 for inferences. % 0.55/0.76 0:00:00.00 for the backtracking. % 0.55/0.76 0:00:00.29 for the reduction. % 0.55/0.76 % 0.55/0.76 % 0.55/0.76 Here is a proof with depth 10, length 59 : % 0.55/0.76 % SZS output start Refutation % 0.55/0.76 1[0:Inp] || -> convergent_lines(skc7,skc6)*. % 0.55/0.76 2[0:Inp] || -> convergent_lines(skc4,skc5)*. % 0.55/0.76 4[0:Inp] || distinct_lines(u,u)* -> . % 0.55/0.76 5[0:Inp] || convergent_lines(u,u)* -> . % 0.55/0.76 6[0:Inp] || apart_point_and_line(intersection_point(skc7,skc6),skc4)* -> . % 0.55/0.76 7[0:Inp] || apart_point_and_line(intersection_point(skc7,skc6),skc5)* -> . % 0.55/0.76 8[0:Inp] || -> apart_point_and_line(intersection_point(skc4,skc5),skc6)* apart_point_and_line(intersection_point(skc4,skc5),skc7). % 0.55/0.76 10[0:Inp] || distinct_lines(u,v)*+ -> distinct_lines(v,w)* distinct_lines(u,w)*. % 0.55/0.76 11[0:Inp] || convergent_lines(u,v)*+ -> convergent_lines(v,w)* convergent_lines(u,w)*. % 0.55/0.76 14[0:Inp] || convergent_lines(u,v) apart_point_and_line(intersection_point(u,v),u)* -> . % 0.55/0.76 15[0:Inp] || convergent_lines(u,v) apart_point_and_line(intersection_point(u,v),v)* -> . % 0.55/0.76 16[0:Inp] || apart_point_and_line(u,v)*+ -> apart_point_and_line(w,v)* distinct_points(u,w)*. % 0.55/0.76 18[0:Inp] || convergent_lines(u,v)*+ -> distinct_lines(v,w)* convergent_lines(u,w)*. % 0.55/0.76 19[0:Inp] || distinct_lines(u,v)*+ distinct_points(w,x)* -> apart_point_and_line(x,u)* apart_point_and_line(x,v)* apart_point_and_line(w,v)* apart_point_and_line(w,u)*. % 0.55/0.76 20[0:Res:2.0,11.0] || -> convergent_lines(skc5,u) convergent_lines(skc4,u)*. % 0.55/0.76 22[0:Res:2.0,15.0] || apart_point_and_line(intersection_point(skc4,skc5),skc5)* -> . % 0.55/0.76 24[0:Res:1.0,11.0] || -> convergent_lines(skc6,u)* convergent_lines(skc7,u). % 0.55/0.76 25[0:Res:1.0,14.0] || apart_point_and_line(intersection_point(skc7,skc6),skc7)* -> . % 0.55/0.76 26[0:Res:1.0,15.0] || apart_point_and_line(intersection_point(skc7,skc6),skc6)* -> . % 0.55/0.76 32[0:Res:19.4,7.0] || distinct_lines(u,skc5) distinct_points(v,intersection_point(skc7,skc6))*+ -> apart_point_and_line(v,u)* apart_point_and_line(v,skc5) apart_point_and_line(intersection_point(skc7,skc6),u)*. % 0.55/0.76 33[0:Res:19.5,7.0] || distinct_points(u,intersection_point(skc7,skc6))*+ distinct_lines(skc5,v) -> apart_point_and_line(u,v)* apart_point_and_line(u,skc5) apart_point_and_line(intersection_point(skc7,skc6),v)*. % 0.55/0.76 48[0:Res:24.0,11.0] || -> convergent_lines(skc7,u)* convergent_lines(u,v)* convergent_lines(skc6,v)*. % 0.55/0.76 49[0:Res:20.1,11.0] || -> convergent_lines(skc5,u)* convergent_lines(u,v)* convergent_lines(skc4,v)*. % 0.55/0.76 55[0:Res:48.2,5.0] || -> convergent_lines(skc7,u)* convergent_lines(u,skc6)*. % 0.55/0.76 57[0:Res:55.0,11.0] || -> convergent_lines(u,skc6)* convergent_lines(u,v)* convergent_lines(skc7,v)*. % 0.55/0.76 64[0:Res:49.2,5.0] || -> convergent_lines(skc5,u)* convergent_lines(u,skc4)*. % 0.55/0.76 80[0:Res:64.0,11.0] || -> convergent_lines(u,skc4)* convergent_lines(u,v)* convergent_lines(skc5,v)*. % 0.55/0.76 94[0:Res:57.2,5.0] || -> convergent_lines(u,skc6)* convergent_lines(u,skc7). % 0.55/0.76 101[0:Res:94.0,18.0] || -> convergent_lines(u,skc7)* distinct_lines(skc6,v)* convergent_lines(u,v)*. % 0.55/0.76 115[0:Res:8.0,16.0] || -> apart_point_and_line(intersection_point(skc4,skc5),skc7) apart_point_and_line(u,skc6) distinct_points(intersection_point(skc4,skc5),u)*. % 0.55/0.76 123[0:Res:80.0,18.0] || -> convergent_lines(u,v)* convergent_lines(skc5,v)* distinct_lines(skc4,w)* convergent_lines(u,w)*. % 0.55/0.76 128[0:Res:80.2,5.0] || -> convergent_lines(u,skc4)* convergent_lines(u,skc5). % 0.55/0.76 144[0:Res:128.0,18.0] || -> convergent_lines(u,skc5)* distinct_lines(skc4,v)* convergent_lines(u,v)*. % 0.55/0.76 153[0:Fac:101.0,101.2] || -> distinct_lines(skc6,skc7)* convergent_lines(u,skc7)*. % 0.55/0.76 161[1:Spt:153.1] || -> convergent_lines(u,skc7)*. % 0.55/0.76 162[1:UnC:161.0,5.0] || -> . % 0.55/0.76 163[1:Spt:162.0,153.0] || -> distinct_lines(skc6,skc7)*. % 0.55/0.76 222[2:Spt:115.1,115.2] || -> apart_point_and_line(u,skc6) distinct_points(intersection_point(skc4,skc5),u)*. % 0.55/0.76 274[0:Fac:144.0,144.2] || -> distinct_lines(skc4,skc5)* convergent_lines(u,skc5)*. % 0.55/0.76 286[3:Spt:274.1] || -> convergent_lines(u,skc5)*. % 0.55/0.76 287[3:UnC:286.0,5.0] || -> . % 0.55/0.76 288[3:Spt:287.0,274.0] || -> distinct_lines(skc4,skc5)*. % 0.55/0.76 290[3:Res:288.0,10.0] || -> distinct_lines(skc5,u) distinct_lines(skc4,u)*. % 0.55/0.76 294[3:Res:290.1,4.0] || -> distinct_lines(skc5,skc4)*. % 0.55/0.76 333[2:Res:222.1,33.0] || distinct_lines(skc5,u) -> apart_point_and_line(intersection_point(skc7,skc6),skc6) apart_point_and_line(intersection_point(skc4,skc5),u)* apart_point_and_line(intersection_point(skc4,skc5),skc5)* apart_point_and_line(intersection_point(skc7,skc6),u). % 0.55/0.76 334[2:MRR:333.1,333.3,26.0,22.0] || distinct_lines(skc5,u) -> apart_point_and_line(intersection_point(skc4,skc5),u)* apart_point_and_line(intersection_point(skc7,skc6),u). % 0.55/0.76 1095[0:Res:123.3,5.0] || -> convergent_lines(u,v)* convergent_lines(skc5,v)* distinct_lines(skc4,u)*. % 0.55/0.76 1100[0:Fac:1095.0,1095.1] || -> convergent_lines(skc5,u)* distinct_lines(skc4,skc5)*. % 0.55/0.76 1226[2:Res:334.1,14.1] || distinct_lines(skc5,skc4) convergent_lines(skc4,skc5) -> apart_point_and_line(intersection_point(skc7,skc6),skc4)*. % 0.55/0.76 1238[3:MRR:1226.0,1226.1,1226.2,294.0,2.0,6.0] || -> . % 0.55/0.76 1240[2:Spt:1238.0,115.0] || -> apart_point_and_line(intersection_point(skc4,skc5),skc7)*. % 0.55/0.76 1242[2:Res:1240.0,16.0] || -> apart_point_and_line(u,skc7) distinct_points(intersection_point(skc4,skc5),u)*. % 0.55/0.76 1243[3:Spt:1100.0] || -> convergent_lines(skc5,u)*. % 0.55/0.76 1244[3:UnC:1243.0,5.0] || -> . % 0.55/0.76 1245[3:Spt:1244.0,1100.1] || -> distinct_lines(skc4,skc5)*. % 0.55/0.76 1274[2:Res:1242.1,32.1] || distinct_lines(u,skc5) -> apart_point_and_line(intersection_point(skc7,skc6),skc7) apart_point_and_line(intersection_point(skc4,skc5),u)* apart_point_and_line(intersection_point(skc4,skc5),skc5)* apart_point_and_line(intersection_point(skc7,skc6),u). % 0.55/0.76 1276[2:MRR:1274.1,1274.3,25.0,22.0] || distinct_lines(u,skc5) -> apart_point_and_line(intersection_point(skc4,skc5),u)* apart_point_and_line(intersection_point(skc7,skc6),u). % 0.55/0.76 1754[2:Res:1276.1,14.1] || distinct_lines(skc4,skc5) convergent_lines(skc4,skc5) -> apart_point_and_line(intersection_point(skc7,skc6),skc4)*. % 0.55/0.76 1769[3:MRR:1754.0,1754.1,1754.2,1245.0,2.0,6.0] || -> . % 0.55/0.76 % SZS output end Refutation % 0.55/0.76 Formulae used in the proof : con apart2 apart3 apart5 ax6 ci3 ci4 ceq1 ceq3 cu1 % 0.55/0.76 %------------------------------------------------------------------------------