%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT055+1 : TPTP v9.3.0. Released v2.4.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 : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:19:57 AM UTC 2026 % Result : Theorem 3.65s 3.96s % Output : Refutation 3.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT055+1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : run_spass %d %s % 0.09/0.36 % Computer : n006.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 13:26:01 UTC 2026 % 0.09/0.36 % CPUTime : % 3.65/3.96 % 3.65/3.96 SPASS V 3.9 % 3.65/3.96 SPASS beiseite: Proof found. % 3.65/3.96 % SZS status Theorem % 3.65/3.96 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.65/3.96 SPASS derived 7921 clauses, backtracked 250 clauses, performed 4 splits and kept 1825 clauses. % 3.65/3.96 SPASS allocated 103594 KBytes. % 3.65/3.96 SPASS spent 0:00:03.58 on the problem. % 3.65/3.96 0:00:00.06 for the input. % 3.65/3.96 0:00:00.05 for the FLOTTER CNF translation. % 3.65/3.96 0:00:00.20 for inferences. % 3.65/3.96 0:00:00.01 for the backtracking. % 3.65/3.96 0:00:03.20 for the reduction. % 3.65/3.96 % 3.65/3.96 % 3.65/3.96 Here is a proof with depth 5, length 86 : % 3.65/3.96 % SZS output start Refutation % 3.65/3.96 1[0:Inp] || -> organization(skc5)*. % 3.65/3.96 2[0:Inp] || -> has_endowment(skc5)*. % 3.65/3.96 3[0:Inp] || -> greater(eta,zero)*r. % 3.65/3.96 4[0:Inp] || -> greater(sigma,eta)*l. % 3.65/3.96 5[0:Inp] || -> greater(age(skc5,skc9),sigma)*l. % 3.65/3.96 6[0:Inp] || -> smaller_or_equal(age(skc5,skc8),sigma)*. % 3.65/3.96 7[0:Inp] || -> greater(age(skc5,skc8),eta)*l. % 3.65/3.96 8[0:Inp] || -> smaller_or_equal(age(skc5,skc7),eta)*. % 3.65/3.96 9[0:Inp] || -> equal(age(skc5,skc6),zero)**. % 3.65/3.96 11[0:Inp] || dissimilar(u,v,w)* -> organization(u). % 3.65/3.96 12[0:Inp] || smaller(u,v)* -> smaller_or_equal(u,v). % 3.65/3.96 16[0:Inp] || smaller(u,v)* -> greater(v,u). % 3.65/3.96 17[0:Inp] || greater(u,v) -> smaller(v,u)*. % 3.65/3.96 18[0:Inp] || greater(u,v)*+ greater(v,u)* -> . % 3.65/3.96 20[0:Inp] || smaller_or_equal(u,v) -> equal(u,v) smaller(u,v)*. % 3.65/3.96 23[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 3.65/3.96 24[0:Inp] has_endowment(u) || smaller_or_equal(age(u,v),eta)* -> has_immunity(u,v). % 3.65/3.96 25[0:Inp] organization(u) || equal(age(u,v),zero)** -> is_aligned(u,v). % 3.65/3.96 26[0:Inp] has_endowment(u) || has_immunity(u,v) greater(age(u,v),eta)*l -> . % 3.65/3.96 27[0:Inp] || is_aligned(u,v) is_aligned(u,w) dissimilar(u,w,v)* -> . % 3.65/3.96 29[0:Inp] organization(u) || is_aligned(u,v) -> is_aligned(u,w) dissimilar(u,v,w)*. % 3.65/3.96 34[0:Inp] organization(u) || has_immunity(u,v) -> has_immunity(u,w) greater(hazard_of_mortality(u,w),hazard_of_mortality(u,v))*. % 3.65/3.96 35[0:Inp] organization(u) || is_aligned(u,v) -> is_aligned(u,w) greater(capability(u,v),capability(u,w))*. % 3.65/3.96 36[0:Inp] organization(u) || has_immunity(u,v) has_immunity(u,w) -> equal(hazard_of_mortality(u,v),hazard_of_mortality(u,w))*. % 3.65/3.96 37[0:Inp] organization(u) || greater(age(u,v),sigma) equal(age(u,w),zero) -> dissimilar(u,w,v)*. % 3.65/3.96 38[0:Inp] organization(u) || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 3.65/3.96 39[0:Inp] organization(u) || greater(capability(u,v),capability(u,w))* -> has_immunity(u,w) greater(hazard_of_mortality(u,w),hazard_of_mortality(u,v)) has_immunity(u,v). % 3.65/3.96 40[0:Inp] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) greater(hazard_of_mortality(skc5,skc8),hazard_of_mortality(skc5,skc7)) greater(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc8))*l -> . % 3.65/3.96 41[0:MRR:38.0,11.1] || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 3.65/3.96 42[0:MRR:39.4,34.1] organization(u) || greater(capability(u,v),capability(u,w))* -> has_immunity(u,w) greater(hazard_of_mortality(u,w),hazard_of_mortality(u,v)). % 3.65/3.96 43[0:Res:2.0,26.0] || has_immunity(skc5,u) greater(age(skc5,u),eta)*l -> . % 3.65/3.96 44[0:Res:2.0,24.0] || smaller_or_equal(age(skc5,u),eta)* -> has_immunity(skc5,u). % 3.65/3.96 49[0:Res:1.0,34.0] || has_immunity(skc5,u) -> has_immunity(skc5,v) greater(hazard_of_mortality(skc5,v),hazard_of_mortality(skc5,u))*. % 3.65/3.96 52[0:Res:1.0,36.0] || has_immunity(skc5,u) has_immunity(skc5,v) -> equal(hazard_of_mortality(skc5,u),hazard_of_mortality(skc5,v))*. % 3.65/3.96 55[0:Res:1.0,29.0] || is_aligned(skc5,u) -> is_aligned(skc5,v) dissimilar(skc5,u,v)*. % 3.65/3.96 57[0:Res:1.0,25.0] || equal(age(skc5,u),zero)** -> is_aligned(skc5,u). % 3.65/3.96 58[0:Res:9.0,41.0] || dissimilar(skc5,skc6,u)* -> greater(age(skc5,u),sigma). % 3.65/3.96 60[0:Res:9.0,25.1] organization(skc5) || -> is_aligned(skc5,skc6)*. % 3.65/3.96 65[0:Res:8.0,24.1] has_endowment(skc5) || -> has_immunity(skc5,skc7)*. % 3.65/3.96 67[0:Res:6.0,20.0] || -> equal(age(skc5,skc8),sigma) smaller(age(skc5,skc8),sigma)*. % 3.65/3.96 74[0:Res:3.0,17.0] || -> smaller(zero,eta)*. % 3.65/3.96 76[0:Res:7.0,26.2] has_endowment(skc5) || has_immunity(skc5,skc8)* -> . % 3.65/3.96 81[0:Res:5.0,37.2] organization(skc5) || equal(age(skc5,u),zero) -> dissimilar(skc5,u,skc9)*. % 3.65/3.96 90[0:MRR:60.0,1.0] || -> is_aligned(skc5,skc6)*. % 3.65/3.96 91[0:MRR:65.0,2.0] || -> has_immunity(skc5,skc7)*. % 3.65/3.96 92[0:MRR:76.0,2.0] || has_immunity(skc5,skc8)* -> . % 3.65/3.96 93[0:MRR:81.0,1.0] || equal(age(skc5,u),zero) -> dissimilar(skc5,u,skc9)*. % 3.65/3.96 95[1:Spt:67.0] || -> equal(age(skc5,skc8),sigma)**. % 3.65/3.96 103[0:Res:74.0,12.0] || -> smaller_or_equal(zero,eta)*. % 3.65/3.96 110[0:SpL:9.0,44.0] || smaller_or_equal(zero,eta) -> has_immunity(skc5,skc6)*. % 3.65/3.96 114[0:MRR:110.0,103.0] || -> has_immunity(skc5,skc6)*. % 3.65/3.96 143[0:Res:93.1,27.2] || equal(age(skc5,u),zero)** is_aligned(skc5,skc9) is_aligned(skc5,u) -> . % 3.65/3.96 146[0:MRR:143.2,57.1] || equal(age(skc5,u),zero)** is_aligned(skc5,skc9) -> . % 3.65/3.96 148[0:SpL:9.0,146.0] || equal(zero,zero) is_aligned(skc5,skc9)* -> . % 3.65/3.96 149[0:Obv:148.0] || is_aligned(skc5,skc9)* -> . % 3.65/3.96 190[0:Res:55.2,58.0] || is_aligned(skc5,skc6) -> is_aligned(skc5,u) greater(age(skc5,u),sigma)*l. % 3.65/3.96 193[0:MRR:190.0,90.0] || -> is_aligned(skc5,u) greater(age(skc5,u),sigma)*l. % 3.65/3.96 194[1:SpR:95.0,193.1] || -> is_aligned(skc5,skc8)* greater(sigma,sigma). % 3.65/3.96 210[0:NCh:23.2,23.0,43.1,5.0] || has_immunity(skc5,skc9)* greater(sigma,eta) -> . % 3.65/3.96 215[0:MRR:210.1,4.0] || has_immunity(skc5,skc9)* -> . % 3.65/3.96 222[0:Res:193.1,18.0] || greater(sigma,age(skc5,u))*r -> is_aligned(skc5,u). % 3.65/3.96 260[1:SpL:95.0,222.0] || greater(sigma,sigma) -> is_aligned(skc5,skc8)*. % 3.65/3.96 263[1:MRR:260.0,194.1] || -> is_aligned(skc5,skc8)*. % 3.65/3.96 857[0:Res:35.3,42.1] organization(u) organization(u) || is_aligned(u,v) -> is_aligned(u,w) has_immunity(u,w) greater(hazard_of_mortality(u,w),hazard_of_mortality(u,v))*. % 3.65/3.96 877[0:Obv:857.0] organization(u) || is_aligned(u,v) -> is_aligned(u,w) has_immunity(u,w) greater(hazard_of_mortality(u,w),hazard_of_mortality(u,v))*. % 3.65/3.96 3354[0:Res:877.4,40.2] organization(skc5) || is_aligned(skc5,skc8) equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) greater(hazard_of_mortality(skc5,skc8),hazard_of_mortality(skc5,skc7))*l -> is_aligned(skc5,skc9) has_immunity(skc5,skc9). % 3.65/3.96 3427[0:SSi:3354.0,2.0,1.0] || is_aligned(skc5,skc8) equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) greater(hazard_of_mortality(skc5,skc8),hazard_of_mortality(skc5,skc7))*l -> is_aligned(skc5,skc9) has_immunity(skc5,skc9). % 3.65/3.96 3428[1:MRR:3427.0,3427.3,3427.4,263.0,149.0,215.0] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) greater(hazard_of_mortality(skc5,skc8),hazard_of_mortality(skc5,skc7))*l -> . % 3.65/3.96 5293[1:Res:49.2,3428.1] || has_immunity(skc5,skc7) equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6))** -> has_immunity(skc5,skc8). % 3.65/3.96 5316[1:MRR:5293.0,5293.2,91.0,92.0] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6))** -> . % 3.65/3.96 5319[1:SpL:52.2,5316.0] || has_immunity(skc5,u) has_immunity(skc5,skc7) equal(hazard_of_mortality(skc5,u),hazard_of_mortality(skc5,skc6))* -> . % 3.65/3.96 5321[1:MRR:5319.1,91.0] || has_immunity(skc5,u) equal(hazard_of_mortality(skc5,u),hazard_of_mortality(skc5,skc6))* -> . % 3.65/3.96 5322[1:EqR:5321.1] || has_immunity(skc5,skc6)* -> . % 3.65/3.96 5331[1:MRR:5322.0,114.0] || -> . % 3.65/3.96 5341[1:Spt:5331.0,67.0,95.0] || equal(age(skc5,skc8),sigma)** -> . % 3.65/3.96 5342[1:Spt:5331.0,67.1] || -> smaller(age(skc5,skc8),sigma)*. % 3.65/3.96 5345[0:MRR:3427.3,3427.4,149.0,215.0] || is_aligned(skc5,skc8) equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) greater(hazard_of_mortality(skc5,skc8),hazard_of_mortality(skc5,skc7))*l -> . % 3.65/3.96 5350[1:Res:5342.0,16.0] || -> greater(sigma,age(skc5,skc8))*r. % 3.65/3.96 5486[1:Res:5350.0,222.0] || -> is_aligned(skc5,skc8)*. % 3.65/3.96 5556[1:MRR:5345.0,5486.0] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) greater(hazard_of_mortality(skc5,skc8),hazard_of_mortality(skc5,skc7))*l -> . % 3.65/3.96 8398[1:Res:49.2,5556.1] || has_immunity(skc5,skc7) equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6))** -> has_immunity(skc5,skc8). % 3.65/3.96 8423[1:MRR:8398.0,8398.2,91.0,92.0] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6))** -> . % 3.65/3.96 8426[1:SpL:52.2,8423.0] || has_immunity(skc5,u) has_immunity(skc5,skc7) equal(hazard_of_mortality(skc5,u),hazard_of_mortality(skc5,skc6))* -> . % 3.65/3.96 8428[1:MRR:8426.1,91.0] || has_immunity(skc5,u) equal(hazard_of_mortality(skc5,u),hazard_of_mortality(skc5,skc6))* -> . % 3.65/3.96 8430[1:EqR:8428.1] || has_immunity(skc5,skc6)* -> . % 3.78/4.11 8439[1:MRR:8430.0,114.0] || -> . % 3.78/4.11 % SZS output end Refutation % 3.78/4.11 Formulae used in the proof : lemma_8 definition_2 definition_smaller_or_equal definition_smaller meaning_postulate_greater_strict meaning_postulate_greater_transitive definition_1 assumption_13 assumption_3 assumption_14 assumption_2 assumption_15 assumption_16 % 3.78/4.11 %------------------------------------------------------------------------------