%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT061+1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n026.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:58 AM UTC 2026 % Result : Theorem 0.88s 1.19s % Output : Refutation 0.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT061+1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : run_spass %d %s % 0.09/0.34 % Computer : n026.cluster.edu % 0.09/0.34 % Model : x86_64 x86_64 % 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.34 % Memory : 8046.5625MB % 0.09/0.34 % OS : Linux 6.8.0-71-generic % 0.09/0.34 % CPULimit : 300 % 0.09/0.34 % WCLimit : 300 % 0.09/0.34 % DateTime : Mon Sep 7 13:37:57 UTC 2026 % 0.09/0.34 % CPUTime : % 0.88/1.19 % 0.88/1.19 SPASS V 3.9 % 0.88/1.19 SPASS beiseite: Proof found. % 0.88/1.19 % SZS status Theorem % 0.88/1.19 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.88/1.19 SPASS derived 3654 clauses, backtracked 0 clauses, performed 3 splits and kept 1208 clauses. % 0.88/1.19 SPASS allocated 100063 KBytes. % 0.88/1.19 SPASS spent 0:00:00.81 on the problem. % 0.88/1.19 0:00:00.06 for the input. % 0.88/1.19 0:00:00.05 for the FLOTTER CNF translation. % 0.88/1.19 0:00:00.08 for inferences. % 0.88/1.19 0:00:00.01 for the backtracking. % 0.88/1.19 0:00:00.56 for the reduction. % 0.88/1.19 % 0.88/1.19 % 0.88/1.19 Here is a proof with depth 4, length 64 : % 0.88/1.19 % SZS output start Refutation % 0.88/1.19 1[0:Inp] || -> fragile_position(skc4)*. % 0.88/1.19 2[0:Inp] || -> organization(skc4)*. % 0.88/1.19 3[0:Inp] || has_endowment(skc4)* -> . % 0.88/1.19 4[0:Inp] || -> greater(sigma,zero)*l. % 0.88/1.19 8[0:Inp] || -> greater(high,mod2)*l. % 0.88/1.19 9[0:Inp] || -> greater(mod2,low)*l. % 0.88/1.19 10[0:Inp] || -> greater(age(skc4,skc7),sigma)*l. % 0.88/1.19 11[0:Inp] || -> smaller_or_equal(age(skc4,skc6),sigma)*. % 0.88/1.19 12[0:Inp] || -> equal(age(skc4,skc5),zero)**. % 0.88/1.19 13[0:Inp] || dissimilar(u,v,w)* -> organization(u). % 0.88/1.19 14[0:Inp] || smaller(u,v)* -> smaller_or_equal(u,v). % 0.88/1.19 19[0:Inp] || greater(u,v) -> smaller(v,u)*. % 0.88/1.19 21[0:Inp] organization(u) || has_immunity(u,v)* -> has_endowment(u). % 0.88/1.19 27[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.88/1.19 28[0:Inp] organization(u) || equal(age(u,v),zero)** -> is_aligned(u,v). % 0.88/1.19 29[0:Inp] fragile_position(u) || smaller_or_equal(age(u,v),sigma)* -> positional_advantage(u,v). % 0.88/1.19 32[0:Inp] || is_aligned(u,v) is_aligned(u,w) dissimilar(u,w,v)* -> . % 0.88/1.19 33[0:Inp] fragile_position(u) || positional_advantage(u,v) greater(age(u,v),sigma)*l -> . % 0.88/1.19 35[0:Inp] organization(u) || is_aligned(u,v) -> is_aligned(u,w) dissimilar(u,v,w)*. % 0.88/1.19 38[0:Inp] || equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5)) greater(hazard_of_mortality(skc4,skc7),hazard_of_mortality(skc4,skc6))*l -> . % 0.88/1.19 39[0:Inp] organization(u) || -> has_immunity(u,v) positional_advantage(u,v) is_aligned(u,v) equal(hazard_of_mortality(u,v),high)**. % 0.88/1.19 42[0:Inp] organization(u) || greater(age(u,v),sigma) equal(age(u,w),zero) -> dissimilar(u,w,v)*. % 0.88/1.19 43[0:Inp] organization(u) || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 0.88/1.19 44[0:Inp] organization(u) || is_aligned(u,v) positional_advantage(u,v) -> has_immunity(u,v) equal(hazard_of_mortality(u,v),low)**. % 0.88/1.19 45[0:MRR:43.0,13.1] || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 0.88/1.19 47[0:Res:2.0,44.0] || positional_advantage(skc4,u) is_aligned(skc4,u) -> equal(hazard_of_mortality(skc4,u),low)** has_immunity(skc4,u). % 0.88/1.19 50[0:Res:2.0,39.0] || -> is_aligned(skc4,u) positional_advantage(skc4,u) equal(hazard_of_mortality(skc4,u),high)** has_immunity(skc4,u). % 0.88/1.19 51[0:Res:2.0,35.0] || is_aligned(skc4,u) -> is_aligned(skc4,v) dissimilar(skc4,u,v)*. % 0.88/1.19 55[0:Res:2.0,21.0] || has_immunity(skc4,u)* -> has_endowment(skc4). % 0.88/1.19 56[0:Res:1.0,33.0] || positional_advantage(skc4,u) greater(age(skc4,u),sigma)*l -> . % 0.88/1.19 57[0:Res:1.0,29.0] || smaller_or_equal(age(skc4,u),sigma)* -> positional_advantage(skc4,u). % 0.88/1.19 59[0:Res:12.0,45.0] || dissimilar(skc4,skc5,u)* -> greater(age(skc4,u),sigma). % 0.88/1.19 61[0:Res:12.0,28.1] organization(skc4) || -> is_aligned(skc4,skc5)*. % 0.88/1.19 66[0:Res:11.0,29.1] fragile_position(skc4) || -> positional_advantage(skc4,skc6)*. % 0.88/1.19 70[0:Res:4.0,19.0] || -> smaller(zero,sigma)*. % 0.88/1.19 73[0:Res:10.0,42.2] organization(skc4) || equal(age(skc4,u),zero) -> dissimilar(skc4,u,skc7)*. % 0.88/1.19 82[0:MRR:55.1,3.0] || has_immunity(skc4,u)* -> . % 0.88/1.19 83[0:MRR:61.0,2.0] || -> is_aligned(skc4,skc5)*. % 0.88/1.19 84[0:MRR:66.0,1.0] || -> positional_advantage(skc4,skc6)*. % 0.88/1.19 86[0:MRR:73.0,2.0] || equal(age(skc4,u),zero) -> dissimilar(skc4,u,skc7)*. % 0.88/1.19 87[0:MRR:50.3,82.0] || -> positional_advantage(skc4,u) is_aligned(skc4,u) equal(hazard_of_mortality(skc4,u),high)**. % 0.88/1.19 90[0:MRR:47.3,82.0] || is_aligned(skc4,u) positional_advantage(skc4,u) -> equal(hazard_of_mortality(skc4,u),low)**. % 0.88/1.19 94[0:Res:12.0,86.0] || -> dissimilar(skc4,skc5,skc7)*. % 0.88/1.19 100[0:Res:70.0,14.0] || -> smaller_or_equal(zero,sigma)*. % 0.88/1.19 103[0:SpL:12.0,57.0] || smaller_or_equal(zero,sigma) -> positional_advantage(skc4,skc5)*. % 0.88/1.19 106[0:MRR:103.0,100.0] || -> positional_advantage(skc4,skc5)*. % 0.88/1.19 144[0:Res:94.0,32.2] || is_aligned(skc4,skc7)* is_aligned(skc4,skc5) -> . % 0.88/1.19 148[0:MRR:144.1,83.0] || is_aligned(skc4,skc7)* -> . % 0.88/1.19 198[0:Res:51.2,59.0] || is_aligned(skc4,skc5) -> is_aligned(skc4,u) greater(age(skc4,u),sigma)*l. % 0.88/1.19 203[0:MRR:198.0,83.0] || -> is_aligned(skc4,u) greater(age(skc4,u),sigma)*l. % 0.88/1.19 209[0:Res:203.1,56.1] || positional_advantage(skc4,u)* -> is_aligned(skc4,u). % 0.88/1.19 217[0:MRR:87.0,209.0] || -> is_aligned(skc4,u) equal(hazard_of_mortality(skc4,u),high)**. % 0.88/1.19 218[0:MRR:90.0,209.1] || positional_advantage(skc4,u) -> equal(hazard_of_mortality(skc4,u),low)**. % 0.88/1.19 404[0:SpL:217.1,38.1] || equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5)) greater(high,hazard_of_mortality(skc4,skc6))*r -> is_aligned(skc4,skc7). % 0.88/1.19 411[0:MRR:404.2,148.0] || equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5)) greater(high,hazard_of_mortality(skc4,skc6))*r -> . % 0.88/1.19 951[0:CRe:27.0,8.0] || greater(mod2,u)*+ -> greater(high,u)*. % 0.88/1.19 1047[0:Res:9.0,951.0] || -> greater(high,low)*l. % 0.88/1.19 3835[0:SpL:218.1,411.1] || positional_advantage(skc4,skc6) equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5))** greater(high,low) -> . % 0.88/1.19 3846[0:Rew:218.1,3835.1] || positional_advantage(skc4,skc6) equal(hazard_of_mortality(skc4,skc5),low)** greater(high,low) -> . % 0.88/1.19 3847[0:MRR:3846.0,3846.2,84.0,1047.0] || equal(hazard_of_mortality(skc4,skc5),low)** -> . % 0.88/1.19 3851[0:SpL:44.4,3847.0] organization(skc4) || is_aligned(skc4,skc5) positional_advantage(skc4,skc5) equal(low,low) -> has_immunity(skc4,skc5)*. % 0.88/1.19 3858[0:Obv:3851.3] organization(skc4) || is_aligned(skc4,skc5) positional_advantage(skc4,skc5) -> has_immunity(skc4,skc5)*. % 0.88/1.19 3859[0:SSi:3858.0,1.0,2.0] || is_aligned(skc4,skc5) positional_advantage(skc4,skc5) -> has_immunity(skc4,skc5)*. % 0.88/1.19 3860[0:MRR:3859.0,3859.1,3859.2,209.1,106.0,82.0] || -> . % 0.88/1.19 % SZS output end Refutation % 0.88/1.19 Formulae used in the proof : theorem_7 assumption_18d assumption_18e definition_2 definition_smaller_or_equal definition_smaller assumption_1 meaning_postulate_greater_transitive assumption_13 definition_3 assumption_17 assumption_15 % 0.88/1.19 %------------------------------------------------------------------------------