%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEV515+1 : TPTP v8.1.0. Released v7.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n006.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 : Tue Jul 19 18:14:52 EDT 2022 % Result : Theorem 0.18s 0.44s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SEV515+1 : TPTP v8.1.0. Released v7.0.0. % 0.11/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n006.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 : Tue Jun 28 12:11:38 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.44 % 0.18/0.44 SPASS V 3.9 % 0.18/0.44 SPASS beiseite: Proof found. % 0.18/0.44 % SZS status Theorem % 0.18/0.44 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.44 SPASS derived 115 clauses, backtracked 4 clauses, performed 2 splits and kept 89 clauses. % 0.18/0.44 SPASS allocated 85185 KBytes. % 0.18/0.44 SPASS spent 0:00:00.10 on the problem. % 0.18/0.44 0:00:00.04 for the input. % 0.18/0.44 0:00:00.03 for the FLOTTER CNF translation. % 0.18/0.44 0:00:00.00 for inferences. % 0.18/0.44 0:00:00.00 for the backtracking. % 0.18/0.44 0:00:00.00 for the reduction. % 0.18/0.44 % 0.18/0.44 % 0.18/0.44 Here is a proof with depth 5, length 44 : % 0.18/0.44 % SZS output start Refutation % 0.18/0.44 1[0:Inp] || SkP0(skc2,u)* -> . % 0.18/0.44 2[0:Inp] || SkP1(skc2,u)* -> . % 0.18/0.44 5[0:Inp] || SkP2(u,v)* -> g_true_only(v,u). % 0.18/0.44 6[0:Inp] || SkP2(u,v)*+ -> g_false_only(v,v)*. % 0.18/0.44 7[0:Inp] || g_true_only(u,v) -> g_true(u,v)*. % 0.18/0.44 11[0:Inp] || g_false_only(u,u)*+ g_false_only(u,skc2)* -> . % 0.18/0.44 12[0:Inp] || g_both(u,u)*+ g_false_only(u,skc2)* -> . % 0.18/0.44 13[0:Inp] || SkC0 -> g_false_only(u,skc3) SkP2(skc3,u)*. % 0.18/0.44 14[0:Inp] || SkC0+ -> g_true_only(u,u)* SkP2(skc3,u)*. % 0.18/0.44 16[0:Inp] || g_false_only(u,v) g_true(u,v)* -> . % 0.18/0.44 17[0:Inp] || -> g_false_only(u,v)* g_both(u,v) g_true_only(u,v). % 0.18/0.44 18[0:Inp] || -> g_both(skf5(u),skf5(u)) g_false_only(skf5(u),skf5(u))*. % 0.18/0.44 24[0:Inp] || g_true_only(u,v)+ g_true_only(u,u)* -> SkP0(v,u)*. % 0.18/0.44 28[0:Inp] || g_both(u,u)*+ g_both(u,v)* -> SkC0 SkP1(v,skf4(v))* SkP0(v,skf3(v)) g_false_only(skf5(v),v). % 0.18/0.44 29[1:Spt:28.0,28.1,28.3,28.4,28.5] || g_both(u,u)*+ g_both(u,v)* -> SkP1(v,skf4(v))* SkP0(v,skf3(v)) g_false_only(skf5(v),v). % 0.18/0.44 30[0:Res:13.2,6.0] || SkC0+ -> g_false_only(u,skc3)* g_false_only(u,u)*. % 0.18/0.44 33[0:Res:7.1,16.1] || g_true_only(u,v) g_false_only(u,v)* -> . % 0.18/0.44 39[0:Res:17.0,11.0] || g_false_only(u,skc2)* -> g_both(u,u)* g_true_only(u,u). % 0.18/0.44 40[0:MRR:39.1,12.0] || g_false_only(u,skc2)*+ -> g_true_only(u,u)*. % 0.18/0.44 41[0:Res:17.0,40.0] || -> g_both(u,skc2)* g_true_only(u,skc2) g_true_only(u,u)*. % 0.18/0.44 47[0:Res:18.1,11.0] || g_false_only(skf5(u),skc2) -> g_both(skf5(u),skf5(u))*. % 0.18/0.44 48[0:MRR:47.1,12.0] || g_false_only(skf5(u),skc2)* -> . % 0.18/0.44 53[1:Res:41.0,29.0] || g_both(skc2,u) -> g_true_only(skc2,skc2) g_true_only(skc2,skc2) SkP1(u,skf4(u))* SkP0(u,skf3(u)) g_false_only(skf5(u),u). % 0.18/0.44 57[1:Obv:53.1] || g_both(skc2,u) -> g_true_only(skc2,skc2) SkP1(u,skf4(u))* SkP0(u,skf3(u)) g_false_only(skf5(u),u). % 0.18/0.44 89[0:Res:41.2,24.0] || g_true_only(u,u) -> g_both(u,skc2) g_true_only(u,skc2) SkP0(u,u)*. % 0.18/0.44 91[0:MRR:89.0,41.2] || -> g_both(u,skc2) g_true_only(u,skc2) SkP0(u,u)*. % 0.18/0.44 92[0:Res:91.2,1.0] || -> g_both(skc2,skc2)* g_true_only(skc2,skc2). % 0.18/0.44 95[2:Spt:57.0,57.2,57.3,57.4] || g_both(skc2,u) -> SkP1(u,skf4(u))* SkP0(u,skf3(u)) g_false_only(skf5(u),u). % 0.18/0.44 96[2:Res:95.1,2.0] || g_both(skc2,skc2) -> SkP0(skc2,skf3(skc2))* g_false_only(skf5(skc2),skc2). % 0.18/0.44 99[2:MRR:96.1,96.2,1.0,48.0] || g_both(skc2,skc2)* -> . % 0.18/0.44 100[2:MRR:92.0,99.0] || -> g_true_only(skc2,skc2)*. % 0.18/0.44 101[2:Res:100.0,24.0] || g_true_only(skc2,skc2) -> SkP0(skc2,skc2)*. % 0.18/0.44 103[2:MRR:101.0,101.1,100.0,1.0] || -> . % 0.18/0.44 104[2:Spt:103.0,57.1] || -> g_true_only(skc2,skc2)*. % 0.18/0.44 105[2:Res:104.0,24.0] || g_true_only(skc2,skc2) -> SkP0(skc2,skc2)*. % 0.18/0.44 107[2:MRR:105.0,105.1,104.0,1.0] || -> . % 0.18/0.44 109[1:Spt:107.0,28.2] || -> SkC0*. % 0.18/0.44 112[1:MRR:14.0,109.0] || -> g_true_only(u,u)* SkP2(skc3,u)*. % 0.18/0.44 113[1:MRR:30.0,109.0] || -> g_false_only(u,skc3)* g_false_only(u,u)*. % 0.18/0.44 133[1:Res:112.1,5.0] || -> g_true_only(u,u)* g_true_only(u,skc3)*. % 0.18/0.44 139[1:Fac:113.0,113.1] || -> g_false_only(skc3,skc3)*. % 0.18/0.44 148[1:Res:139.0,33.1] || g_true_only(skc3,skc3)* -> . % 0.18/0.44 154[1:Fac:133.0,133.1] || -> g_true_only(skc3,skc3)*. % 0.18/0.44 160[1:MRR:154.0,148.0] || -> . % 0.18/0.44 % SZS output end Refutation % 0.18/0.44 Formulae used in the proof : nc1 exhaustion_g true_only_g false_only_g % 0.18/0.44 %------------------------------------------------------------------------------