%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT004+1 : TPTP v9.3.0. Released v2.0.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 : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:19:44 AM UTC 2026 % Result : Theorem 0.31s 0.62s % Output : Refutation 0.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT004+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.04 % Command : run_spass %d %s % 0.09/0.36 % Computer : n019.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Mon Sep 7 11:35:22 UTC 2026 % 0.09/0.36 % CPUTime : % 0.31/0.62 % 0.31/0.62 SPASS V 3.9 % 0.31/0.62 SPASS beiseite: Proof found. % 0.31/0.62 % SZS status Theorem % 0.31/0.62 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.31/0.62 SPASS derived 151 clauses, backtracked 31 clauses, performed 11 splits and kept 143 clauses. % 0.31/0.62 SPASS allocated 85457 KBytes. % 0.31/0.62 SPASS spent 0:00:00.24 on the problem. % 0.31/0.62 0:00:00.06 for the input. % 0.31/0.62 0:00:00.06 for the FLOTTER CNF translation. % 0.31/0.62 0:00:00.01 for inferences. % 0.31/0.62 0:00:00.00 for the backtracking. % 0.31/0.62 0:00:00.06 for the reduction. % 0.31/0.62 % 0.31/0.62 % 0.31/0.62 Here is a proof with depth 11, length 57 : % 0.31/0.62 % SZS output start Refutation % 0.31/0.62 1[0:Inp] || -> organization(skc13,skc9)*. % 0.31/0.62 2[0:Inp] || -> organization(skc13,skc7)*. % 0.31/0.62 3[0:Inp] || -> greater(skc7,skc9)*. % 0.31/0.62 4[0:Inp] || -> reorganization(skc13,skc10,skc8)*. % 0.31/0.62 5[0:Inp] || -> survival_chance(skc13,skc12,skc9)*. % 0.31/0.62 6[0:Inp] || -> survival_chance(skc13,skc11,skc7)*. % 0.31/0.62 7[0:Inp] || greater(skc12,skc11)* -> . % 0.31/0.62 8[0:Inp] || greater(skc10,skc9)* -> . % 0.31/0.62 9[0:Inp] || greater(skc7,skc8)* -> . % 0.31/0.62 10[0:Inp] || organization(u,v) -> reliability(u,skf2(v,u),v)*. % 0.31/0.62 11[0:Inp] || organization(u,v) -> accountability(u,skf3(v,u),v)*. % 0.31/0.62 12[0:Inp] || greater(u,v)* organization(w,u) organization(w,v) accountability(w,x,u)*+ accountability(w,y,v)* reliability(w,z,u)* reliability(w,x1,v)* reorganization(w,x2,x3)* -> greater(u,x3)* greater(x2,v)* greater(y,x)*. % 0.31/0.62 13[0:Inp] || greater(u,v)* organization(w,u) organization(w,v) accountability(w,x,u)*+ accountability(w,y,v)* reliability(w,z,u)* reliability(w,x1,v)* reorganization(w,x2,x3)* -> greater(u,x3)* greater(x2,v)* greater(x1,z)*. % 0.31/0.62 14[0:Inp] || greater(u,v)* greater(w,x)* organization(y,z) organization(x1,x2) survival_chance(y,x3,z)*+ accountability(y,v,z)* reliability(y,x,z)* reliability(x1,w,x2)* accountability(x1,u,x2)* survival_chance(x1,x4,x2)* -> greater(x4,x3)*. % 0.31/0.62 21[0:Res:2.0,10.0] || -> reliability(skc13,skf2(skc7,skc13),skc7)*. % 0.31/0.62 22[0:Res:2.0,11.0] || -> accountability(skc13,skf3(skc7,skc13),skc7)*. % 0.31/0.62 24[0:Res:2.0,13.1] || greater(skc7,u) organization(skc13,u) accountability(skc13,v,u)*+ reliability(skc13,w,u)* reorganization(skc13,x,y)* accountability(skc13,z,skc7)* reliability(skc13,x1,skc7)* -> greater(x,u)* greater(w,x1)* greater(skc7,y). % 0.31/0.62 25[0:Res:2.0,12.1] || greater(skc7,u) organization(skc13,u) accountability(skc13,v,u)*+ reliability(skc13,w,u)* reorganization(skc13,x,y)* accountability(skc13,z,skc7)* reliability(skc13,x1,skc7)* -> greater(x,u)* greater(v,z)* greater(skc7,y). % 0.31/0.62 29[0:Res:1.0,10.0] || -> reliability(skc13,skf2(skc9,skc13),skc9)*. % 0.31/0.62 30[0:Res:1.0,11.0] || -> accountability(skc13,skf3(skc9,skc13),skc9)*. % 0.31/0.62 36[0:Res:30.0,24.2] || greater(skc7,skc9) organization(skc13,skc9) reliability(skc13,u,skc9)* reorganization(skc13,v,w)* accountability(skc13,x,skc7)* reliability(skc13,y,skc7)* -> greater(v,skc9) greater(u,y)* greater(skc7,w). % 0.31/0.62 39[0:MRR:36.0,36.1,3.0,1.0] || reliability(skc13,u,skc9)*+ reorganization(skc13,v,w)* accountability(skc13,x,skc7)* reliability(skc13,y,skc7)* -> greater(v,skc9) greater(u,y)* greater(skc7,w). % 0.31/0.62 41[1:Spt:39.0,39.3,39.5] || reliability(skc13,u,skc9)*+ reliability(skc13,v,skc7)* -> greater(u,v)*. % 0.31/0.62 49[0:Res:22.0,13.3] || greater(skc7,u) organization(skc13,skc7) organization(skc13,u) accountability(skc13,v,u)* reliability(skc13,w,skc7)* reliability(skc13,x,u)* reorganization(skc13,y,z)* -> greater(skc7,z) greater(y,u)* greater(x,w)*. % 0.31/0.62 50[0:MRR:49.1,2.0] || greater(skc7,u) organization(skc13,u) accountability(skc13,v,u)*+ reliability(skc13,w,skc7)* reliability(skc13,x,u)* reorganization(skc13,y,z)* -> greater(skc7,z) greater(y,u)* greater(x,w)*. % 0.31/0.62 67[0:Res:11.1,50.2] || organization(skc13,u) greater(skc7,u) organization(skc13,u) reliability(skc13,v,skc7)* reliability(skc13,w,u)* reorganization(skc13,x,y)* -> greater(skc7,y) greater(x,u)* greater(w,v)*. % 0.31/0.62 70[0:Obv:67.0] || greater(skc7,u) organization(skc13,u) reliability(skc13,v,skc7)*+ reliability(skc13,w,u)* reorganization(skc13,x,y)* -> greater(skc7,y) greater(x,u)* greater(w,v)*. % 0.31/0.62 71[0:Res:21.0,70.2] || greater(skc7,u) organization(skc13,u) reliability(skc13,v,u)*+ reorganization(skc13,w,x)* -> greater(skc7,x) greater(w,u)* greater(v,skf2(skc7,skc13))*. % 0.31/0.62 73[0:Res:29.0,71.2] || greater(skc7,skc9) organization(skc13,skc9) reorganization(skc13,u,v)* -> greater(skc7,v) greater(u,skc9) greater(skf2(skc9,skc13),skf2(skc7,skc13))*. % 0.31/0.62 77[0:MRR:73.0,73.1,3.0,1.0] || reorganization(skc13,u,v)*+ -> greater(skc7,v) greater(u,skc9) greater(skf2(skc9,skc13),skf2(skc7,skc13))*. % 0.31/0.62 79[0:Res:6.0,14.4] || greater(u,v)* greater(w,x)* organization(skc13,skc7) organization(y,z) accountability(skc13,v,skc7)* reliability(skc13,x,skc7)* reliability(y,w,z)* accountability(y,u,z)* survival_chance(y,x1,z)* -> greater(x1,skc11). % 0.31/0.62 82[0:MRR:79.2,2.0] || greater(u,v)* greater(w,x)* organization(y,z) accountability(skc13,v,skc7)*+ reliability(skc13,x,skc7)* reliability(y,w,z)* accountability(y,u,z)* survival_chance(y,x1,z)* -> greater(x1,skc11). % 0.31/0.62 83[2:Spt:77.0,77.1,77.2] || reorganization(skc13,u,v)* -> greater(skc7,v) greater(u,skc9). % 0.31/0.62 84[2:Res:4.0,83.0] || -> greater(skc7,skc8)* greater(skc10,skc9). % 0.31/0.62 85[2:MRR:84.0,84.1,9.0,8.0] || -> . % 0.31/0.62 86[2:Spt:85.0,77.3] || -> greater(skf2(skc9,skc13),skf2(skc7,skc13))*. % 0.31/0.62 104[0:Res:22.0,82.3] || greater(u,skf3(skc7,skc13))*+ greater(v,w)* organization(x,y) reliability(skc13,w,skc7)* reliability(x,v,y)* accountability(x,u,y)* survival_chance(x,z,y)* -> greater(z,skc11). % 0.31/0.62 129[0:Res:30.0,25.2] || greater(skc7,skc9) organization(skc13,skc9) reliability(skc13,u,skc9)* reorganization(skc13,v,w)* accountability(skc13,x,skc7) reliability(skc13,y,skc7)* -> greater(v,skc9) greater(skf3(skc9,skc13),x)* greater(skc7,w). % 0.31/0.62 132[0:MRR:129.0,129.1,3.0,1.0] || reliability(skc13,u,skc9)*+ reorganization(skc13,v,w)* accountability(skc13,x,skc7) reliability(skc13,y,skc7)* -> greater(v,skc9) greater(skf3(skc9,skc13),x)* greater(skc7,w). % 0.31/0.62 134[3:Spt:132.1,132.4,132.6] || reorganization(skc13,u,v)* -> greater(u,skc9) greater(skc7,v). % 0.31/0.62 135[3:Res:4.0,134.0] || -> greater(skc10,skc9) greater(skc7,skc8)*. % 0.31/0.62 136[3:MRR:135.0,135.1,8.0,9.0] || -> . % 0.31/0.62 137[3:Spt:136.0,132.0,132.2,132.3,132.5] || reliability(skc13,u,skc9)*+ accountability(skc13,v,skc7) reliability(skc13,w,skc7)* -> greater(skf3(skc9,skc13),v)*. % 0.31/0.62 138[3:Res:29.0,137.0] || accountability(skc13,u,skc7)+ reliability(skc13,v,skc7)* -> greater(skf3(skc9,skc13),u)*. % 0.31/0.62 141[3:Res:22.0,138.0] || reliability(skc13,u,skc7)*+ -> greater(skf3(skc9,skc13),skf3(skc7,skc13))*. % 0.31/0.62 142[3:Res:21.0,141.0] || -> greater(skf3(skc9,skc13),skf3(skc7,skc13))*. % 0.31/0.62 204[3:Res:142.0,104.0] || greater(u,v)* organization(w,x) reliability(skc13,v,skc7)* reliability(w,u,x)* accountability(w,skf3(skc9,skc13),x)*+ survival_chance(w,y,x)* -> greater(y,skc11). % 0.31/0.62 210[3:Res:30.0,204.4] || greater(u,v)* organization(skc13,skc9) reliability(skc13,v,skc7)* reliability(skc13,u,skc9)* survival_chance(skc13,w,skc9)* -> greater(w,skc11). % 0.31/0.62 211[3:MRR:210.0,210.1,41.2,1.0] || reliability(skc13,u,skc7)*+ reliability(skc13,v,skc9)* survival_chance(skc13,w,skc9)* -> greater(w,skc11). % 0.31/0.62 213[3:Res:21.0,211.0] || reliability(skc13,u,skc9)*+ survival_chance(skc13,v,skc9)* -> greater(v,skc11). % 0.31/0.62 215[3:Res:29.0,213.0] || survival_chance(skc13,u,skc9)* -> greater(u,skc11). % 0.31/0.62 223[3:Res:5.0,215.0] || -> greater(skc12,skc11)*. % 0.31/0.62 224[3:MRR:223.0,7.0] || -> . % 0.31/0.62 225[1:Spt:224.0,39.1,39.2,39.4,39.6] || reorganization(skc13,u,v)*+ accountability(skc13,w,skc7)* -> greater(u,skc9) greater(skc7,v). % 0.31/0.62 231[1:Res:4.0,225.0] || accountability(skc13,u,skc7)* -> greater(skc10,skc9) greater(skc7,skc8). % 0.31/0.62 232[1:MRR:231.1,231.2,8.0,9.0] || accountability(skc13,u,skc7)* -> . % 0.31/0.62 233[1:UnC:232.0,22.0] || -> . % 0.31/0.62 % SZS output end Refutation % 0.31/0.62 Formulae used in the proof : t4_FOL mp1 mp2 a6_FOL a1_FOL % 0.31/0.62 %------------------------------------------------------------------------------