%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GEO189+2 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n015.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:09 EDT 2022 % Result : Theorem 0.70s 0.90s % Output : Refutation 0.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GEO189+2 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n015.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 : Sat Jun 18 08:36:58 EDT 2022 % 0.12/0.33 % CPUTime : % 0.70/0.90 % 0.70/0.90 SPASS V 3.9 % 0.70/0.90 SPASS beiseite: Proof found. % 0.70/0.90 % SZS status Theorem % 0.70/0.90 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.70/0.90 SPASS derived 2354 clauses, backtracked 259 clauses, performed 7 splits and kept 876 clauses. % 0.70/0.90 SPASS allocated 86784 KBytes. % 0.70/0.90 SPASS spent 0:00:00.55 on the problem. % 0.70/0.90 0:00:00.03 for the input. % 0.70/0.90 0:00:00.03 for the FLOTTER CNF translation. % 0.70/0.90 0:00:00.05 for inferences. % 0.70/0.90 0:00:00.00 for the backtracking. % 0.70/0.90 0:00:00.41 for the reduction. % 0.70/0.90 % 0.70/0.90 % 0.70/0.90 Here is a proof with depth 7, length 77 : % 0.70/0.90 % SZS output start Refutation % 0.70/0.90 1[0:Inp] || -> distinct_points(skc5,skc3)*. % 0.70/0.90 2[0:Inp] || -> distinct_points(skc5,skc4)*. % 0.70/0.90 3[0:Inp] || -> distinct_points(skc3,skc4)*. % 0.70/0.90 4[0:Inp] || distinct_points(u,u)* -> . % 0.70/0.90 5[0:Inp] || distinct_lines(u,u)* -> . % 0.70/0.90 7[0:Inp] || -> apart_point_and_line(skc3,line_connecting(skc5,skc4))*. % 0.70/0.90 8[0:Inp] || apart_point_and_line(skc4,line_connecting(skc5,skc3))* -> . % 0.70/0.90 10[0:Inp] || distinct_points(u,v)*+ -> distinct_points(v,w)* distinct_points(u,w)*. % 0.70/0.90 11[0:Inp] || distinct_lines(u,v)*+ -> distinct_lines(v,w)* distinct_lines(u,w)*. % 0.70/0.90 13[0:Inp] || apart_point_and_line(u,v)*+ -> apart_point_and_line(w,v)* distinct_points(u,w)*. % 0.70/0.90 14[0:Inp] || apart_point_and_line(u,v)*+ -> distinct_lines(v,w)* apart_point_and_line(u,w)*. % 0.70/0.90 15[0:Inp] || distinct_points(u,v) apart_point_and_line(w,line_connecting(u,v))* -> distinct_points(w,u). % 0.70/0.90 16[0:Inp] || distinct_points(u,v) apart_point_and_line(w,line_connecting(u,v))* -> distinct_points(w,v). % 0.70/0.90 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.70/0.90 22[0:Res:3.0,15.1] || apart_point_and_line(u,line_connecting(skc3,skc4))* -> distinct_points(u,skc3). % 0.70/0.90 24[0:Res:2.0,19.0] || distinct_lines(u,v)* -> apart_point_and_line(skc4,u) apart_point_and_line(skc4,v) apart_point_and_line(skc5,v) apart_point_and_line(skc5,u). % 0.70/0.90 25[0:Res:2.0,10.0] || -> distinct_points(skc4,u)* distinct_points(skc5,u). % 0.70/0.90 26[0:Res:2.0,15.1] || apart_point_and_line(u,line_connecting(skc5,skc4))* -> distinct_points(u,skc5). % 0.70/0.90 28[0:Res:1.0,19.0] || distinct_lines(u,v)* -> apart_point_and_line(skc3,u) apart_point_and_line(skc3,v) apart_point_and_line(skc5,v) apart_point_and_line(skc5,u). % 0.70/0.90 29[0:Res:1.0,10.0] || -> distinct_points(skc3,u)* distinct_points(skc5,u). % 0.70/0.90 31[0:Res:1.0,16.1] || apart_point_and_line(u,line_connecting(skc5,skc3))* -> distinct_points(u,skc3). % 0.70/0.90 34[0:Res:7.0,13.0] || -> apart_point_and_line(u,line_connecting(skc5,skc4))* distinct_points(skc3,u). % 0.70/0.90 35[0:Res:7.0,14.0] || -> apart_point_and_line(skc3,u) distinct_lines(line_connecting(skc5,skc4),u)*. % 0.70/0.90 39[0:Res:14.1,8.0] || apart_point_and_line(skc4,u) -> distinct_lines(u,line_connecting(skc5,skc3))*. % 0.70/0.90 53[0:Res:35.1,11.0] || -> apart_point_and_line(skc3,u) distinct_lines(u,v)* distinct_lines(line_connecting(skc5,skc4),v)*. % 0.70/0.90 66[0:Res:25.0,10.0] || -> distinct_points(skc5,u)* distinct_points(u,v)* distinct_points(skc4,v)*. % 0.70/0.90 68[0:Res:34.0,26.0] || -> distinct_points(skc3,u)* distinct_points(u,skc5)*. % 0.70/0.90 70[0:Res:68.0,10.0] || -> distinct_points(u,skc5)* distinct_points(u,v)* distinct_points(skc3,v)*. % 0.70/0.90 73[0:Res:34.0,13.0] || -> distinct_points(skc3,u)* apart_point_and_line(v,line_connecting(skc5,skc4))* distinct_points(u,v)*. % 0.70/0.90 101[0:Res:34.0,14.0] || -> distinct_points(skc3,u) distinct_lines(line_connecting(skc5,skc4),v)* apart_point_and_line(u,v)*. % 0.70/0.90 118[0:Res:66.2,4.0] || -> distinct_points(skc5,u)* distinct_points(u,skc4)*. % 0.70/0.90 122[0:Res:118.0,10.0] || -> distinct_points(u,skc4)* distinct_points(u,v)* distinct_points(skc5,v)*. % 0.70/0.90 131[0:Res:70.2,4.0] || -> distinct_points(u,skc5) distinct_points(u,skc3)*. % 0.70/0.90 178[0:Res:122.2,4.0] || -> distinct_points(u,skc4)* distinct_points(u,skc5). % 0.70/0.90 236[0:Res:73.2,10.0] || -> distinct_points(skc3,u)* apart_point_and_line(v,line_connecting(skc5,skc4))* distinct_points(v,w)* distinct_points(u,w)*. % 0.70/0.90 253[0:Res:39.1,28.0] || apart_point_and_line(skc4,u)+ -> apart_point_and_line(skc3,u)* apart_point_and_line(skc3,line_connecting(skc5,skc3))* apart_point_and_line(skc5,line_connecting(skc5,skc3)) apart_point_and_line(skc5,u). % 0.70/0.90 270[0:Res:101.2,31.0] || -> distinct_points(skc3,u)* distinct_lines(line_connecting(skc5,skc4),line_connecting(skc5,skc3))* distinct_points(u,skc3)*. % 0.70/0.90 272[0:Res:101.2,22.0] || -> distinct_points(skc3,u)* distinct_lines(line_connecting(skc5,skc4),line_connecting(skc3,skc4))* distinct_points(u,skc3)*. % 0.70/0.90 309[0:Res:53.1,24.0] || -> apart_point_and_line(skc3,u)* distinct_lines(line_connecting(skc5,skc4),v)* apart_point_and_line(skc4,u) apart_point_and_line(skc4,v) apart_point_and_line(skc5,v) apart_point_and_line(skc5,u). % 0.70/0.90 862[1:Spt:270.0,270.2] || -> distinct_points(skc3,u)* distinct_points(u,skc3)*. % 0.70/0.90 863[1:Fac:862.0,862.1] || -> distinct_points(skc3,skc3)*. % 0.70/0.90 866[1:MRR:863.0,4.0] || -> . % 0.70/0.90 868[1:Spt:866.0,270.1] || -> distinct_lines(line_connecting(skc5,skc4),line_connecting(skc5,skc3))*. % 0.70/0.90 1034[2:Spt:272.0,272.2] || -> distinct_points(skc3,u)* distinct_points(u,skc3)*. % 0.70/0.90 1035[2:Fac:1034.0,1034.1] || -> distinct_points(skc3,skc3)*. % 0.70/0.90 1038[2:MRR:1035.0,4.0] || -> . % 0.70/0.90 1040[2:Spt:1038.0,272.1] || -> distinct_lines(line_connecting(skc5,skc4),line_connecting(skc3,skc4))*. % 0.70/0.90 1107[3:Spt:253.0,253.1,253.4] || apart_point_and_line(skc4,u) -> apart_point_and_line(skc3,u)* apart_point_and_line(skc5,u). % 0.70/0.90 1109[3:MRR:309.2,1107.0] || -> apart_point_and_line(skc3,u)* distinct_lines(line_connecting(skc5,skc4),v)* apart_point_and_line(skc4,v) apart_point_and_line(skc5,v) apart_point_and_line(skc5,u). % 0.70/0.90 2183[0:Res:236.3,4.0] || -> distinct_points(skc3,u)* apart_point_and_line(v,line_connecting(skc5,skc4))* distinct_points(v,u)*. % 0.70/0.90 2192[0:Res:2183.0,10.0] || -> apart_point_and_line(u,line_connecting(skc5,skc4))* distinct_points(u,v)* distinct_points(v,w)* distinct_points(skc3,w)*. % 0.70/0.90 2433[0:Fac:2192.2,2192.3] || -> apart_point_and_line(u,line_connecting(skc5,skc4))* distinct_points(u,skc3) distinct_points(skc3,v)*. % 0.70/0.90 2460[4:Spt:2433.2] || -> distinct_points(skc3,u)*. % 0.70/0.90 2461[4:UnC:2460.0,4.0] || -> . % 0.70/0.90 2462[4:Spt:2461.0,2433.0,2433.1] || -> apart_point_and_line(u,line_connecting(skc5,skc4))* distinct_points(u,skc3). % 0.70/0.90 2753[5:Spt:1109.1,1109.2,1109.3] || -> distinct_lines(line_connecting(skc5,skc4),u)* apart_point_and_line(skc4,u) apart_point_and_line(skc5,u). % 0.70/0.90 2754[5:Res:2753.0,5.0] || -> apart_point_and_line(skc4,line_connecting(skc5,skc4))* apart_point_and_line(skc5,line_connecting(skc5,skc4)). % 0.70/0.90 2766[6:Spt:2754.0] || -> apart_point_and_line(skc4,line_connecting(skc5,skc4))*. % 0.70/0.90 2770[6:Res:2766.0,16.1] || distinct_points(skc5,skc4) -> distinct_points(skc4,skc4)*. % 0.70/0.90 2777[6:MRR:2770.0,2770.1,118.0,4.0] || -> . % 0.70/0.90 2778[6:Spt:2777.0,2754.0,2766.0] || apart_point_and_line(skc4,line_connecting(skc5,skc4))* -> . % 0.70/0.90 2779[6:Spt:2777.0,2754.1] || -> apart_point_and_line(skc5,line_connecting(skc5,skc4))*. % 0.70/0.90 2799[6:Res:2779.0,15.1] || distinct_points(skc5,skc4)* -> distinct_points(skc5,skc5). % 0.70/0.90 2804[6:MRR:2799.0,2799.1,178.0,4.0] || -> . % 0.70/0.90 2805[5:Spt:2804.0,1109.0,1109.4] || -> apart_point_and_line(skc3,u)* apart_point_and_line(skc5,u). % 0.70/0.90 2809[5:Res:2805.0,31.0] || -> apart_point_and_line(skc5,line_connecting(skc5,skc3))* distinct_points(skc3,skc3). % 0.70/0.90 2817[5:MRR:2809.1,4.0] || -> apart_point_and_line(skc5,line_connecting(skc5,skc3))*. % 0.70/0.90 2822[5:Res:2817.0,15.1] || distinct_points(skc5,skc3)* -> distinct_points(skc5,skc5). % 0.70/0.90 2827[5:MRR:2822.0,2822.1,131.1,4.0] || -> . % 0.70/0.90 2828[3:Spt:2827.0,253.2,253.3] || -> apart_point_and_line(skc3,line_connecting(skc5,skc3))* apart_point_and_line(skc5,line_connecting(skc5,skc3)). % 0.70/0.90 2829[4:Spt:2828.0] || -> apart_point_and_line(skc3,line_connecting(skc5,skc3))*. % 0.70/0.90 2834[4:Res:2829.0,16.1] || distinct_points(skc5,skc3) -> distinct_points(skc3,skc3)*. % 0.70/0.90 2838[4:MRR:2834.0,2834.1,29.1,4.0] || -> . % 0.70/0.90 2839[4:Spt:2838.0,2828.0,2829.0] || apart_point_and_line(skc3,line_connecting(skc5,skc3))* -> . % 0.70/0.90 2840[4:Spt:2838.0,2828.1] || -> apart_point_and_line(skc5,line_connecting(skc5,skc3))*. % 0.70/0.90 2844[4:Res:2840.0,15.1] || distinct_points(skc5,skc3)* -> distinct_points(skc5,skc5). % 0.70/0.90 2849[4:MRR:2844.0,2844.1,131.1,4.0] || -> . % 0.70/0.90 % SZS output end Refutation % 0.70/0.90 Formulae used in the proof : con apart1 apart2 apart4 apart5 ceq1 ceq2 con1 cu1 % 0.70/0.90 %------------------------------------------------------------------------------