%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GEO254+1 : TPTP v8.1.0. Bugfixed v6.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n008.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:57 EDT 2022 % Result : Theorem 0.79s 0.94s % Output : Refutation 0.79s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GEO254+1 : TPTP v8.1.0. Bugfixed v6.4.0. % 0.07/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n008.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Sat Jun 18 14:37:37 EDT 2022 % 0.14/0.34 % CPUTime : % 0.79/0.94 % 0.79/0.94 SPASS V 3.9 % 0.79/0.94 SPASS beiseite: Proof found. % 0.79/0.94 % SZS status Theorem % 0.79/0.94 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.79/0.94 SPASS derived 2634 clauses, backtracked 28 clauses, performed 4 splits and kept 1165 clauses. % 0.79/0.94 SPASS allocated 99285 KBytes. % 0.79/0.94 SPASS spent 0:00:00.59 on the problem. % 0.79/0.94 0:00:00.04 for the input. % 0.79/0.94 0:00:00.04 for the FLOTTER CNF translation. % 0.79/0.94 0:00:00.04 for inferences. % 0.79/0.94 0:00:00.01 for the backtracking. % 0.79/0.94 0:00:00.45 for the reduction. % 0.79/0.94 % 0.79/0.94 % 0.79/0.94 Here is a proof with depth 20, length 71 : % 0.79/0.94 % SZS output start Refutation % 0.79/0.94 1[0:Inp] || -> distinct_points(skc5,skc3)*. % 0.79/0.94 4[0:Inp] || distinct_points(u,u)* -> . % 0.79/0.94 6[0:Inp] || unequally_directed_lines(u,u)* -> . % 0.79/0.94 7[0:Inp] || left_apart_point(u,v)* -> . % 0.79/0.94 8[0:Inp] || left_convergent_lines(u,v)* -> . % 0.79/0.94 22[0:Inp] || unequally_directed_lines(line_connecting(u,v),reverse_line(line_connecting(v,u)))* -> . % 0.79/0.94 23[0:Inp] || before_on_line(skc4,skc3,skc5)* before_on_line(skc4,skc5,skc3) -> . % 0.79/0.94 26[0:Inp] || distinct_points(u,v)*+ -> distinct_points(v,w)* distinct_points(u,w)*. % 0.79/0.94 28[0:Inp] || unequally_directed_lines(u,v)*+ -> unequally_directed_lines(v,w)* unequally_directed_lines(u,w)*. % 0.79/0.94 37[0:Inp] || unequally_directed_lines(u,line_connecting(v,w))* before_on_line(u,v,w) -> . % 0.79/0.94 56[0:Inp] || unequally_directed_lines(u,v) unequally_directed_lines(u,reverse_line(v)) -> left_convergent_lines(u,v) left_convergent_lines(u,reverse_line(v))*. % 0.79/0.94 59[0:Inp] || distinct_points(u,v) -> left_apart_point(u,w) left_apart_point(u,reverse_line(w)) left_apart_point(v,w) left_apart_point(v,reverse_line(w)) unequally_directed_lines(w,line_connecting(u,v))* before_on_line(w,u,v). % 0.79/0.94 63[0:MRR:56.2,56.3,8.0,8.0] || unequally_directed_lines(u,v) unequally_directed_lines(u,reverse_line(v))* -> . % 0.79/0.94 64[0:MRR:59.1,59.2,59.3,59.4,7.0,7.0,7.0,7.0] || distinct_points(u,v) -> unequally_directed_lines(w,line_connecting(u,v))* before_on_line(w,u,v). % 0.79/0.94 67[0:Res:1.0,64.0] || -> unequally_directed_lines(u,line_connecting(skc5,skc3))* before_on_line(u,skc5,skc3). % 0.79/0.94 69[0:Res:1.0,26.0] || -> distinct_points(skc3,u)* distinct_points(skc5,u). % 0.79/0.94 93[0:Res:69.0,26.0] || -> distinct_points(skc5,u)* distinct_points(u,v)* distinct_points(skc3,v)*. % 0.79/0.94 98[0:Res:93.2,4.0] || -> distinct_points(skc5,u)* distinct_points(u,skc3)*. % 0.79/0.94 100[0:Res:98.0,26.0] || -> distinct_points(u,skc3)* distinct_points(u,v)* distinct_points(skc5,v)*. % 0.79/0.94 110[0:Res:100.2,4.0] || -> distinct_points(u,skc3)* distinct_points(u,skc5). % 0.79/0.94 115[0:Res:110.0,4.0] || -> distinct_points(skc3,skc5)*. % 0.79/0.94 117[0:Res:67.0,28.0] || -> before_on_line(u,skc5,skc3)* unequally_directed_lines(line_connecting(skc5,skc3),v)* unequally_directed_lines(u,v)*. % 0.79/0.94 144[0:Res:117.1,28.0] || -> before_on_line(u,skc5,skc3)* unequally_directed_lines(u,v)* unequally_directed_lines(v,w)* unequally_directed_lines(line_connecting(skc5,skc3),w)*. % 0.79/0.94 147[0:Res:117.1,22.0] || -> before_on_line(u,skc5,skc3) unequally_directed_lines(u,reverse_line(line_connecting(skc3,skc5)))*. % 0.79/0.94 148[0:Res:117.2,6.0] || -> before_on_line(u,skc5,skc3) unequally_directed_lines(line_connecting(skc5,skc3),u)*. % 0.79/0.94 150[0:Res:117.2,28.0] || -> before_on_line(u,skc5,skc3)* unequally_directed_lines(line_connecting(skc5,skc3),v)* unequally_directed_lines(v,w)* unequally_directed_lines(u,w)*. % 0.79/0.94 157[0:Res:148.1,63.1] || unequally_directed_lines(line_connecting(skc5,skc3),u)* -> before_on_line(reverse_line(u),skc5,skc3). % 0.79/0.94 164[0:Res:147.1,63.1] || unequally_directed_lines(u,line_connecting(skc3,skc5))* -> before_on_line(u,skc5,skc3). % 0.79/0.94 173[0:Res:117.2,164.0] || -> before_on_line(u,skc5,skc3)* unequally_directed_lines(line_connecting(skc5,skc3),line_connecting(skc3,skc5))* before_on_line(u,skc5,skc3)*. % 0.79/0.94 176[0:Obv:173.0] || -> unequally_directed_lines(line_connecting(skc5,skc3),line_connecting(skc3,skc5))* before_on_line(u,skc5,skc3)*. % 0.79/0.94 177[1:Spt:176.1] || -> before_on_line(u,skc5,skc3)*. % 0.79/0.94 178[1:MRR:23.1,177.0] || before_on_line(skc4,skc3,skc5)* -> . % 0.79/0.94 182[0:Res:64.1,28.0] || distinct_points(u,v)+ -> before_on_line(w,u,v)* unequally_directed_lines(line_connecting(u,v),x)* unequally_directed_lines(w,x)*. % 0.79/0.94 689[0:Res:115.0,182.0] || -> before_on_line(u,skc3,skc5)* unequally_directed_lines(line_connecting(skc3,skc5),v)* unequally_directed_lines(u,v)*. % 0.79/0.94 714[0:Res:689.1,22.0] || -> before_on_line(u,skc3,skc5) unequally_directed_lines(u,reverse_line(line_connecting(skc5,skc3)))*. % 0.79/0.94 715[0:Res:689.2,6.0] || -> before_on_line(u,skc3,skc5) unequally_directed_lines(line_connecting(skc3,skc5),u)*. % 0.79/0.94 744[0:Res:715.1,63.1] || unequally_directed_lines(line_connecting(skc3,skc5),u)* -> before_on_line(reverse_line(u),skc3,skc5). % 0.79/0.94 751[0:Res:714.1,63.1] || unequally_directed_lines(u,line_connecting(skc5,skc3))* -> before_on_line(u,skc3,skc5). % 0.79/0.94 759[0:Res:689.2,751.0] || -> before_on_line(u,skc3,skc5)* unequally_directed_lines(line_connecting(skc3,skc5),line_connecting(skc5,skc3))* before_on_line(u,skc3,skc5)*. % 0.79/0.94 765[0:Obv:759.0] || -> unequally_directed_lines(line_connecting(skc3,skc5),line_connecting(skc5,skc3))* before_on_line(u,skc3,skc5)*. % 0.79/0.94 766[2:Spt:765.1] || -> before_on_line(u,skc3,skc5)*. % 0.79/0.94 767[2:UnC:766.0,178.0] || -> . % 0.79/0.94 768[2:Spt:767.0,765.0] || -> unequally_directed_lines(line_connecting(skc3,skc5),line_connecting(skc5,skc3))*. % 0.79/0.94 770[2:Res:768.0,37.0] || before_on_line(line_connecting(skc3,skc5),skc5,skc3)* -> . % 0.79/0.94 772[2:MRR:770.0,177.0] || -> . % 0.79/0.94 773[1:Spt:772.0,176.0] || -> unequally_directed_lines(line_connecting(skc5,skc3),line_connecting(skc3,skc5))*. % 0.79/0.94 775[1:Res:773.0,28.0] || -> unequally_directed_lines(line_connecting(skc3,skc5),u)* unequally_directed_lines(line_connecting(skc5,skc3),u). % 0.79/0.94 776[1:Res:773.0,37.0] || before_on_line(line_connecting(skc5,skc3),skc3,skc5)* -> . % 0.79/0.94 833[1:Res:775.0,63.1] || unequally_directed_lines(line_connecting(skc3,skc5),u) -> unequally_directed_lines(line_connecting(skc5,skc3),reverse_line(u))*. % 0.79/0.94 840[2:Spt:765.1] || -> before_on_line(u,skc3,skc5)*. % 0.79/0.94 841[2:UnC:840.0,776.0] || -> . % 0.79/0.94 842[2:Spt:841.0,765.0] || -> unequally_directed_lines(line_connecting(skc3,skc5),line_connecting(skc5,skc3))*. % 0.79/0.94 844[2:Res:842.0,37.0] || before_on_line(line_connecting(skc3,skc5),skc5,skc3)* -> . % 0.79/0.94 853[0:Res:689.1,744.0] || -> before_on_line(u,skc3,skc5)* unequally_directed_lines(u,v)* before_on_line(reverse_line(v),skc3,skc5)*. % 0.79/0.94 888[0:Res:117.1,157.0] || -> before_on_line(u,skc5,skc3)* unequally_directed_lines(u,v)* before_on_line(reverse_line(v),skc5,skc3)*. % 0.79/0.94 911[1:Res:833.1,63.1] || unequally_directed_lines(line_connecting(skc3,skc5),u)* unequally_directed_lines(line_connecting(skc5,skc3),u) -> . % 0.79/0.94 1118[0:Res:144.3,6.0] || -> before_on_line(u,skc5,skc3)* unequally_directed_lines(u,v)* unequally_directed_lines(v,line_connecting(skc5,skc3))*. % 0.79/0.94 1135[0:Fac:853.0,853.2] || -> unequally_directed_lines(reverse_line(u),u)* before_on_line(reverse_line(u),skc3,skc5)*. % 0.79/0.94 1224[0:Res:150.3,6.0] || -> before_on_line(u,skc5,skc3)* unequally_directed_lines(line_connecting(skc5,skc3),v)* unequally_directed_lines(v,u)*. % 0.79/0.94 1249[0:Fac:888.0,888.2] || -> unequally_directed_lines(reverse_line(u),u)* before_on_line(reverse_line(u),skc5,skc3)*. % 0.79/0.94 1596[2:Res:1118.0,844.0] || -> unequally_directed_lines(line_connecting(skc3,skc5),u)* unequally_directed_lines(u,line_connecting(skc5,skc3))*. % 0.79/0.94 1670[2:Res:1596.1,37.0] || before_on_line(u,skc5,skc3) -> unequally_directed_lines(line_connecting(skc3,skc5),u)*. % 0.79/0.94 1792[2:Res:1670.1,911.0] || before_on_line(u,skc5,skc3) unequally_directed_lines(line_connecting(skc5,skc3),u)* -> . % 0.79/0.94 2437[2:Res:1224.0,844.0] || -> unequally_directed_lines(line_connecting(skc5,skc3),u)* unequally_directed_lines(u,line_connecting(skc3,skc5))*. % 0.79/0.94 2495[2:Res:2437.0,1792.1] || before_on_line(u,skc5,skc3) -> unequally_directed_lines(u,line_connecting(skc3,skc5))*. % 0.79/0.94 2585[2:Res:2495.1,37.0] || before_on_line(u,skc5,skc3) before_on_line(u,skc3,skc5)* -> . % 0.79/0.94 2781[2:Res:1135.1,2585.1] || before_on_line(reverse_line(u),skc5,skc3)* -> unequally_directed_lines(reverse_line(u),u)*. % 0.79/0.94 2803[2:MRR:2781.0,1249.1] || -> unequally_directed_lines(reverse_line(u),u)*. % 0.79/0.94 2858[2:Res:2803.0,28.0] || -> unequally_directed_lines(u,v) unequally_directed_lines(reverse_line(u),v)*. % 0.79/0.94 2910[2:Res:2858.1,6.0] || -> unequally_directed_lines(u,reverse_line(u))*. % 0.79/0.94 2920[2:UnC:2910.0,22.0] || -> . % 0.79/0.94 % SZS output end Refutation % 0.79/0.94 Formulae used in the proof : con oag1 oag5 oag10 oag11 oagco9 oag2 oag6 bf_def oag9 % 0.79/0.94 %------------------------------------------------------------------------------