%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT065+1 : TPTP v9.3.0. Released v2.4.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 : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:19:59 AM UTC 2026 % Result : Theorem 2.79s 3.05s % Output : Refutation 2.79s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT065+1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.10/0.36 % Computer : n015.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Mon Sep 7 13:48:00 UTC 2026 % 0.10/0.36 % CPUTime : % 2.79/3.05 % 2.79/3.05 SPASS V 3.9 % 2.79/3.05 SPASS beiseite: Proof found. % 2.79/3.05 % SZS status Theorem % 2.79/3.05 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 2.79/3.05 SPASS derived 10099 clauses, backtracked 637 clauses, performed 6 splits and kept 2770 clauses. % 2.79/3.05 SPASS allocated 103645 KBytes. % 2.79/3.05 SPASS spent 0:00:02.55 on the problem. % 2.79/3.05 0:00:00.06 for the input. % 2.79/3.05 0:00:00.05 for the FLOTTER CNF translation. % 2.79/3.05 0:00:00.21 for inferences. % 2.79/3.05 0:00:00.01 for the backtracking. % 2.79/3.05 0:00:02.13 for the reduction. % 2.79/3.05 % 2.79/3.05 % 2.79/3.05 Here is a proof with depth 3, length 66 : % 2.79/3.05 % SZS output start Refutation % 2.79/3.05 1[0:Inp] || -> has_endowment(skc4)*. % 2.79/3.05 2[0:Inp] || -> organization(skc4)*. % 2.79/3.05 5[0:Inp] || -> greater(eta,zero)*r. % 2.79/3.05 7[0:Inp] || -> greater(mod1,low)*l. % 2.79/3.05 8[0:Inp] || -> greater(low,very_low)*l. % 2.79/3.05 9[0:Inp] || -> greater(high,mod2)*l. % 2.79/3.05 10[0:Inp] || -> greater(mod2,low)*l. % 2.79/3.05 12[0:Inp] || -> greater(age(skc4,skc7),sigma)*l. % 2.79/3.05 14[0:Inp] || -> greater(age(skc4,skc7),eta)*l. % 2.79/3.05 15[0:Inp] || -> smaller_or_equal(age(skc4,skc6),eta)*. % 2.79/3.05 18[0:Inp] || -> equal(age(skc4,skc5),zero)**. % 2.79/3.05 21[0:Inp] || smaller(u,v)* -> smaller_or_equal(u,v). % 2.79/3.05 26[0:Inp] || greater(u,v) -> smaller(v,u)*. % 2.79/3.05 32[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 2.79/3.05 33[0:Inp] has_endowment(u) || smaller_or_equal(age(u,v),eta)* -> has_immunity(u,v). % 2.79/3.05 34[0:Inp] organization(u) || equal(age(u,v),zero)** -> is_aligned(u,v). % 2.79/3.05 35[0:Inp] organization(u) || has_immunity(u,v) -> equal(hazard_of_mortality(u,v),very_low)**. % 2.79/3.05 36[0:Inp] has_endowment(u) || has_immunity(u,v) greater(age(u,v),eta)*l -> . % 2.79/3.05 37[0:Inp] || is_aligned(u,v) is_aligned(u,w) dissimilar(u,w,v)* -> . % 2.79/3.05 42[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 -> . % 2.79/3.05 45[0:Inp] organization(u) || -> has_immunity(u,v) positional_advantage(u,v) is_aligned(u,v) equal(hazard_of_mortality(u,v),high)**. % 2.79/3.05 46[0:Inp] organization(u) || positional_advantage(u,v) -> has_immunity(u,v) is_aligned(u,v) equal(hazard_of_mortality(u,v),mod1)**. % 2.79/3.05 48[0:Inp] organization(u) || greater(age(u,v),sigma) equal(age(u,w),zero) -> dissimilar(u,w,v)*. % 2.79/3.05 63[0:Res:2.0,34.0] || equal(age(skc4,u),zero)** -> is_aligned(skc4,u). % 2.79/3.05 64[0:Res:2.0,35.0] || has_immunity(skc4,u) -> equal(hazard_of_mortality(skc4,u),very_low)**. % 2.79/3.05 66[0:Res:1.0,33.0] || smaller_or_equal(age(skc4,u),eta)* -> has_immunity(skc4,u). % 2.79/3.05 77[0:Res:15.0,33.1] has_endowment(skc4) || -> has_immunity(skc4,skc6)*. % 2.79/3.05 81[0:Res:5.0,26.0] || -> smaller(zero,eta)*. % 2.79/3.05 91[0:Res:14.0,36.2] has_endowment(skc4) || has_immunity(skc4,skc7)* -> . % 2.79/3.05 100[0:Res:12.0,48.2] organization(skc4) || equal(age(skc4,u),zero) -> dissimilar(skc4,u,skc7)*. % 2.79/3.05 110[0:MRR:77.0,1.0] || -> has_immunity(skc4,skc6)*. % 2.79/3.05 111[0:MRR:91.0,1.0] || has_immunity(skc4,skc7)* -> . % 2.79/3.05 112[0:MRR:100.0,2.0] || equal(age(skc4,u),zero) -> dissimilar(skc4,u,skc7)*. % 2.79/3.05 151[0:Res:81.0,21.0] || -> smaller_or_equal(zero,eta)*. % 2.79/3.05 155[0:SpL:18.0,66.0] || smaller_or_equal(zero,eta) -> has_immunity(skc4,skc5)*. % 2.79/3.05 157[0:MRR:155.0,151.0] || -> has_immunity(skc4,skc5)*. % 2.79/3.05 189[0:Res:112.1,37.2] || equal(age(skc4,u),zero)** is_aligned(skc4,skc7) is_aligned(skc4,u) -> . % 2.79/3.05 192[0:MRR:189.2,63.1] || equal(age(skc4,u),zero)** is_aligned(skc4,skc7) -> . % 2.79/3.05 194[0:SpL:18.0,192.0] || equal(zero,zero) is_aligned(skc4,skc7)* -> . % 2.79/3.05 195[0:Obv:194.0] || is_aligned(skc4,skc7)* -> . % 2.79/3.05 437[0:SpL:46.4,42.1] organization(skc4) || positional_advantage(skc4,skc7) equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5)) greater(mod1,hazard_of_mortality(skc4,skc6))*r -> has_immunity(skc4,skc7) is_aligned(skc4,skc7). % 2.79/3.05 439[0:SpL:45.4,42.1] organization(skc4) || equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5)) greater(high,hazard_of_mortality(skc4,skc6))*r -> has_immunity(skc4,skc7) positional_advantage(skc4,skc7) is_aligned(skc4,skc7). % 2.79/3.05 924[0:CRe:32.0,10.0] || greater(low,u)*+ -> greater(mod2,u)*. % 2.79/3.05 926[0:CRe:32.0,7.0] || greater(low,u)*+ -> greater(mod1,u)*. % 2.79/3.05 928[0:CRe:32.0,9.0] || greater(mod2,u)*+ -> greater(high,u)*. % 2.79/3.05 989[0:Res:8.0,924.0] || -> greater(mod2,very_low)*l. % 2.79/3.05 1049[0:Res:8.0,926.0] || -> greater(mod1,very_low)*l. % 2.79/3.05 1082[0:Res:989.0,928.0] || -> greater(high,very_low)*l. % 2.79/3.05 9597[0:SSi:439.0,1.0,2.0] || equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5)) greater(high,hazard_of_mortality(skc4,skc6))*r -> has_immunity(skc4,skc7) positional_advantage(skc4,skc7) is_aligned(skc4,skc7). % 2.79/3.05 9598[0:MRR:9597.2,9597.4,111.0,195.0] || equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5)) greater(high,hazard_of_mortality(skc4,skc6))*r -> positional_advantage(skc4,skc7). % 2.79/3.05 9599[0:SSi:437.0,1.0,2.0] || positional_advantage(skc4,skc7) equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5)) greater(mod1,hazard_of_mortality(skc4,skc6))*r -> has_immunity(skc4,skc7) is_aligned(skc4,skc7). % 2.79/3.05 9600[0:MRR:9599.3,9599.4,111.0,195.0] || positional_advantage(skc4,skc7) equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5)) greater(mod1,hazard_of_mortality(skc4,skc6))*r -> . % 2.79/3.05 10468[0:SpL:64.1,9598.1] || has_immunity(skc4,skc6) equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5))** greater(high,very_low) -> positional_advantage(skc4,skc7). % 2.79/3.05 10478[0:Rew:64.1,10468.1] || has_immunity(skc4,skc6) equal(hazard_of_mortality(skc4,skc5),very_low)** greater(high,very_low) -> positional_advantage(skc4,skc7). % 2.79/3.05 10479[0:MRR:10478.0,10478.2,110.0,1082.0] || equal(hazard_of_mortality(skc4,skc5),very_low)** -> positional_advantage(skc4,skc7). % 2.79/3.05 10485[0:SpL:64.1,10479.0] || has_immunity(skc4,skc5) equal(very_low,very_low) -> positional_advantage(skc4,skc7)*. % 2.79/3.05 10491[0:Obv:10485.1] || has_immunity(skc4,skc5) -> positional_advantage(skc4,skc7)*. % 2.79/3.05 10492[0:MRR:10491.0,157.0] || -> positional_advantage(skc4,skc7)*. % 2.79/3.05 10493[0:MRR:9600.0,10492.0] || equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5)) greater(mod1,hazard_of_mortality(skc4,skc6))*r -> . % 2.79/3.05 10507[0:SpL:64.1,10493.1] || has_immunity(skc4,skc6) equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5))** greater(mod1,very_low) -> . % 2.79/3.05 10517[0:Rew:64.1,10507.1] || has_immunity(skc4,skc6) equal(hazard_of_mortality(skc4,skc5),very_low)** greater(mod1,very_low) -> . % 2.79/3.05 10518[0:MRR:10517.0,10517.2,110.0,1049.0] || equal(hazard_of_mortality(skc4,skc5),very_low)** -> . % 2.79/3.05 10529[0:SpL:35.2,10518.0] organization(skc4) || has_immunity(skc4,skc5)* equal(very_low,very_low) -> . % 2.79/3.05 10532[0:Obv:10529.2] organization(skc4) || has_immunity(skc4,skc5)* -> . % 2.79/3.05 10533[0:SSi:10532.0,1.0,2.0] || has_immunity(skc4,skc5)* -> . % 2.79/3.05 10534[0:MRR:10533.0,157.0] || -> . % 2.79/3.05 % SZS output end Refutation % 2.79/3.05 Formulae used in the proof : theorem_11 assumption_18b assumption_18c assumption_18d assumption_18e definition_smaller_or_equal definition_smaller meaning_postulate_greater_transitive definition_1 assumption_13 assumption_17 definition_2 assumption_15 % 2.79/3.05 %------------------------------------------------------------------------------