%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT053+1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n002.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:56 AM UTC 2026 % Result : Theorem 0.22s 0.53s % Output : Refutation 0.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT053+1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : run_spass %d %s % 0.08/0.35 % Computer : n002.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Mon Sep 7 13:25:52 UTC 2026 % 0.08/0.35 % CPUTime : % 0.22/0.53 % 0.22/0.53 SPASS V 3.9 % 0.22/0.53 SPASS beiseite: Proof found. % 0.22/0.53 % SZS status Theorem % 0.22/0.53 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.22/0.53 SPASS derived 95 clauses, backtracked 10 clauses, performed 3 splits and kept 68 clauses. % 0.22/0.53 SPASS allocated 97651 KBytes. % 0.22/0.53 SPASS spent 0:00:00.16 on the problem. % 0.22/0.53 0:00:00.07 for the input. % 0.22/0.53 0:00:00.04 for the FLOTTER CNF translation. % 0.22/0.53 0:00:00.00 for inferences. % 0.22/0.53 0:00:00.00 for the backtracking. % 0.22/0.53 0:00:00.00 for the reduction. % 0.22/0.53 % 0.22/0.53 % 0.22/0.53 Here is a proof with depth 6, length 41 : % 0.22/0.53 % SZS output start Refutation % 0.22/0.53 1[0:Inp] || dissimilar(u,v,w)*+ -> organization(u). % 0.22/0.53 8[0:Inp] || -> dissimilar(skc3,skc5,skc4)* dissimilar(skc3,skc4,skc5). % 0.22/0.53 11[0:Inp] || dissimilar(skc3,skc5,skc4)* dissimilar(skc3,skc4,skc5) -> . % 0.22/0.53 14[0:Inp] || dissimilar(u,v,w)*+ -> is_aligned(u,w) is_aligned(u,v). % 0.22/0.53 16[0:Inp] || is_aligned(u,v) is_aligned(u,w) dissimilar(u,w,v)*+ -> . % 0.22/0.53 17[0:Inp] organization(u) || is_aligned(u,v)+ -> is_aligned(u,w) dissimilar(u,v,w)*. % 0.22/0.53 18[0:Inp] organization(u) || is_aligned(u,v)+ -> is_aligned(u,w) dissimilar(u,w,v)*. % 0.22/0.53 21[1:Spt:8.0] || -> dissimilar(skc3,skc5,skc4)*. % 0.22/0.53 22[1:MRR:11.0,21.0] || dissimilar(skc3,skc4,skc5)*+ -> . % 0.22/0.53 23[1:Res:21.0,1.0] || -> organization(skc3)*. % 0.22/0.53 25[1:Res:21.0,14.0] || -> is_aligned(skc3,skc4) is_aligned(skc3,skc5)*. % 0.22/0.53 26[1:Res:21.0,16.2] || is_aligned(skc3,skc4)+ is_aligned(skc3,skc5)* -> . % 0.22/0.53 31[1:Res:25.1,18.1] organization(skc3) || -> is_aligned(skc3,skc4) is_aligned(skc3,u) dissimilar(skc3,u,skc5)*. % 0.22/0.53 32[1:SSi:31.0,23.0] || -> is_aligned(skc3,skc4) is_aligned(skc3,u) dissimilar(skc3,u,skc5)*. % 0.22/0.53 33[2:Spt:32.0] || -> is_aligned(skc3,skc4)*. % 0.22/0.53 34[2:MRR:26.0,33.0] || is_aligned(skc3,skc5)*+ -> . % 0.22/0.53 42[2:Res:33.0,17.1] organization(skc3) || -> is_aligned(skc3,u) dissimilar(skc3,skc4,u)*. % 0.22/0.53 43[2:SSi:42.0,23.0] || -> is_aligned(skc3,u) dissimilar(skc3,skc4,u)*. % 0.22/0.53 48[2:Res:43.1,22.0] || -> is_aligned(skc3,skc5)*. % 0.22/0.53 49[2:MRR:48.0,34.0] || -> . % 0.22/0.53 52[2:Spt:49.0,32.0,33.0] || is_aligned(skc3,skc4)* -> . % 0.22/0.53 53[2:Spt:49.0,32.1,32.2] || -> is_aligned(skc3,u) dissimilar(skc3,u,skc5)*. % 0.22/0.53 58[2:Res:53.1,22.0] || -> is_aligned(skc3,skc4)*. % 0.22/0.53 59[2:MRR:58.0,52.0] || -> . % 0.22/0.53 62[1:Spt:59.0,8.0,21.0] || dissimilar(skc3,skc5,skc4)*+ -> . % 0.22/0.53 63[1:Spt:59.0,8.1] || -> dissimilar(skc3,skc4,skc5)*. % 0.22/0.53 64[1:Res:63.0,14.0] || -> is_aligned(skc3,skc5)* is_aligned(skc3,skc4). % 0.22/0.53 65[1:Res:63.0,1.0] || -> organization(skc3)*. % 0.22/0.53 66[1:Res:63.0,16.2] || is_aligned(skc3,skc5)* is_aligned(skc3,skc4) -> . % 0.22/0.53 67[2:Spt:64.0] || -> is_aligned(skc3,skc5)*. % 0.22/0.53 68[2:MRR:66.0,67.0] || is_aligned(skc3,skc4)*+ -> . % 0.22/0.53 69[2:Res:67.0,17.1] organization(skc3) || -> is_aligned(skc3,u) dissimilar(skc3,skc5,u)*. % 0.22/0.53 71[2:SSi:69.0,65.0] || -> is_aligned(skc3,u) dissimilar(skc3,skc5,u)*. % 0.22/0.53 76[2:Res:71.1,62.0] || -> is_aligned(skc3,skc4)*. % 0.22/0.53 77[2:MRR:76.0,68.0] || -> . % 0.22/0.53 80[2:Spt:77.0,64.0,67.0] || is_aligned(skc3,skc5)*+ -> . % 0.22/0.53 81[2:Spt:77.0,64.1] || -> is_aligned(skc3,skc4)*. % 0.22/0.53 83[2:Res:81.0,18.1] organization(skc3) || -> is_aligned(skc3,u) dissimilar(skc3,u,skc4)*. % 0.22/0.53 85[2:SSi:83.0,65.0] || -> is_aligned(skc3,u) dissimilar(skc3,u,skc4)*. % 0.22/0.53 142[2:Res:85.1,62.0] || -> is_aligned(skc3,skc5)*. % 0.22/0.53 143[2:MRR:142.0,80.0] || -> . % 0.22/0.53 % SZS output end Refutation % 0.22/0.53 Formulae used in the proof : definition_2 lemma_7 % 0.22/0.53 %------------------------------------------------------------------------------