%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP047_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 5 07:12:55 PM UTC 2026 % Result : Theorem 1.00s 1.43s % Output : Refutation 1.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.18 % Problem : SYP047_1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.19 % Command : run_ksp %s % 0.15/0.41 % Computer : n015.cluster.edu % 0.15/0.41 % Model : x86_64 x86_64 % 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.41 % Memory : 8042.1875MB % 0.15/0.41 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.41 % CPULimit : 300 % 0.15/0.41 % WCLimit : 300 % 0.15/0.41 % DateTime : Mon May 4 16:28:17 EDT 2026 % 0.15/0.41 % CPUTime : % 0.29/0.85 ----KSP format--- % 0.29/0.85 set(box,FIVE). % 0.29/0.85 usable(formulas). % 0.29/0.85 true. % 0.29/0.85 end_of_list. % 0.29/0.85 sos(formulas). % 0.29/0.85 ~ ([] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( [] ( $false ) ) | <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) | <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) | <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) | <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( [] ( $false ) ) ) | <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) | <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) | <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) | <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( [] ( $false ) ) ) ) | <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) | <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) | <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) | <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) | <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ). % 0.29/0.85 end_of_list. % 0.29/0.85 ----------------- % 0.29/0.85 ksp -tstp -pproof -early_ple -mlple -ord -snf++ -unit -lhs_unit -fsub -bsub -limited_reuse_renaming -bnfsimp -maxproof 1 -populate_max_lit_positive -short -global2local -i /export/starexec/sandbox2/tmp/tmp.d4G7IheLoz/theBenchmark.ksp % 1.00/1.43 % 1.00/1.43 % SZS status Theorem % 1.00/1.43 % 1.00/1.43 ***************** % 1.00/1.43 FOUND PROOF 1 % 1.00/1.43 ***************** % 1.00/1.43 % SZS output start Refutation % 1.00/1.43 % 1.00/1.43 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 1.00/1.43 (141,1) [8978,0]. _t65 => ~box 1~ _t66 [ SNF ] [ Backward Subsumption, 9094 ] % 1.00/1.43 (1,1) [8979,0]. true => _t65 | ~_t0 [ SNF ] [ Backward Subsumption, 9043 ] % 1.00/1.43 (1,1) [9043,0]. true => _t65 [ Unit Resolution, 3, 8979, _t0 ] [ Modal Level Pure Literal Elimination, _t65 ] % 1.00/1.43 (141,1) [9094,0]. true => ~box 1~ _t66 [ LHS Unit Resolution, 9043, 8978, _t65 ] [ SNF++, 10959, _t66 ] % 1.00/1.43 (141,1) [10959,0]. true => ~box 1~ _t312 [ SNF++, 9094 ] % 1.00/1.43 (141,1) [119070,0]. true => false [ GEN1 Unit Resolution, 119069, 10959, _t312 ] % 1.00/1.43 (140,1) [8977,1]. _t66 => ~box 1~ _t67 [ SNF ] [ SNF++, 10173, _t67 ] % 1.00/1.43 (140,1) [10173,1]. _t66 => ~box 1~ _t311 [ SNF++, 8977 ] [ Backward Subsumption, 119068 ] % 1.00/1.43 (141,1) [10960,1]. true => ~_t312 | _t66 [ SNF++, 9094 ] [ Backward Subsumption, 119069 ] % 1.00/1.43 (140,1) [119068,1]. true => ~_t66 [ GEN1 Unit Resolution, 119067, 10173, _t311 ] [ Modal Level Pure Literal Elimination, ~_t66 ] % 1.00/1.43 (141,1) [119069,1]. true => ~_t312 [ Unit Resolution, 119068, 10960, _t66 ] % 1.00/1.43 (139,1) [8976,2]. _t67 => ~box 1~ _t68 [ SNF ] [ SNF++, 11079, _t68 ] % 1.00/1.43 (140,1) [10174,2]. true => ~_t311 | _t67 [ SNF++, 8977 ] [ Backward Subsumption, 119067 ] % 1.00/1.43 (139,1) [11079,2]. _t67 => ~box 1~ _t313 [ SNF++, 8976 ] [ Backward Subsumption, 119066 ] % 1.00/1.43 (139,1) [119066,2]. true => ~_t67 [ GEN1 Unit Resolution, 119065, 11079, _t313 ] [ Modal Level Pure Literal Elimination, ~_t67 ] % 1.00/1.43 (140,1) [119067,2]. true => ~_t311 [ Unit Resolution, 119066, 10174, _t67 ] [ Modal Level Pure Literal Elimination, ~_t311 ] % 1.00/1.43 (138,1) [8975,3]. _t68 => ~box 1~ _t69 [ SNF ] [ SNF++, 11535, _t69 ] % 1.00/1.43 (139,1) [11080,3]. true => ~_t313 | _t68 [ SNF++, 8976 ] [ Backward Subsumption, 119065 ] % 1.00/1.43 (138,1) [11535,3]. _t68 => ~box 1~ _t314 [ SNF++, 8975 ] [ Backward Subsumption, 119064 ] % 1.00/1.43 (138,1) [119064,3]. true => ~_t68 [ GEN1 Unit Resolution, 119063, 11535, _t314 ] [ Modal Level Pure Literal Elimination, ~_t68 ] % 1.00/1.43 (139,1) [119065,3]. true => ~_t313 [ Unit Resolution, 119064, 11080, _t68 ] [ Modal Level Pure Literal Elimination, ~_t313 ] % 1.00/1.43 (137,1) [8974,4]. _t69 => ~box 1~ _t70 [ SNF ] [ SNF++, 11991, _t70 ] % 1.00/1.43 (138,1) [11536,4]. true => ~_t314 | _t69 [ SNF++, 8975 ] [ Backward Subsumption, 119063 ] % 1.00/1.43 (137,1) [11991,4]. _t69 => ~box 1~ _t315 [ SNF++, 8974 ] [ Backward Subsumption, 119062 ] % 1.00/1.43 (137,1) [119062,4]. true => ~_t69 [ GEN1 Unit Resolution, 119061, 11991, _t315 ] [ Modal Level Pure Literal Elimination, ~_t69 ] % 1.00/1.43 (138,1) [119063,4]. true => ~_t314 [ Unit Resolution, 119062, 11536, _t69 ] [ Modal Level Pure Literal Elimination, ~_t314 ] % 1.00/1.43 (136,1) [8973,5]. _t70 => ~box 1~ _t71 [ SNF ] [ SNF++, 12447, _t71 ] % 1.00/1.43 (137,1) [11992,5]. true => ~_t315 | _t70 [ SNF++, 8974 ] [ Backward Subsumption, 119061 ] % 1.00/1.43 (136,1) [12447,5]. _t70 => ~box 1~ _t316 [ SNF++, 8973 ] [ Backward Subsumption, 119060 ] % 1.00/1.43 (136,1) [119060,5]. true => ~_t70 [ GEN1 Unit Resolution, 119059, 12447, _t316 ] [ Modal Level Pure Literal Elimination, ~_t70 ] % 1.00/1.43 (137,1) [119061,5]. true => ~_t315 [ Unit Resolution, 119060, 11992, _t70 ] [ Modal Level Pure Literal Elimination, ~_t315 ] % 1.00/1.43 (135,1) [8972,6]. _t71 => ~box 1~ _t72 [ SNF ] [ SNF++, 12903, _t72 ] % 1.00/1.43 (136,1) [12448,6]. true => ~_t316 | _t71 [ SNF++, 8973 ] [ Backward Subsumption, 119059 ] % 1.00/1.43 (135,1) [12903,6]. _t71 => ~box 1~ _t317 [ SNF++, 8972 ] [ Backward Subsumption, 119058 ] % 1.00/1.43 (135,1) [119058,6]. true => ~_t71 [ GEN1 Unit Resolution, 119057, 12903, _t317 ] [ Modal Level Pure Literal Elimination, ~_t71 ] % 1.00/1.43 (136,1) [119059,6]. true => ~_t316 [ Unit Resolution, 119058, 12448, _t71 ] [ Modal Level Pure Literal Elimination, ~_t316 ] % 1.00/1.43 (134,1) [8971,7]. _t72 => ~box 1~ _t73 [ SNF ] [ SNF++, 13359, _t73 ] % 1.00/1.43 (135,1) [12904,7]. true => ~_t317 | _t72 [ SNF++, 8972 ] [ Backward Subsumption, 119057 ] % 1.00/1.43 (134,1) [13359,7]. _t72 => ~box 1~ _t318 [ SNF++, 8971 ] [ Backward Subsumption, 119056 ] % 1.00/1.43 (134,1) [119056,7]. true => ~_t72 [ GEN1 Unit Resolution, 119055, 13359, _t318 ] [ Modal Level Pure Literal Elimination, ~_t72 ] % 1.09/1.53 (135,1) [119057,7]. true => ~_t317 [ Unit Resolution, 119056, 12904, _t72 ] [ Modal Level Pure Literal Elimination, ~_t317 ] % 1.09/1.53 (133,1) [8970,8]. _t73 => ~box 1~ _t74 [ SNF ] [ SNF++, 13815, _t74 ] % 1.09/1.53 (134,1) [13360,8]. true => ~_t318 | _t73 [ SNF++, 8971 ] [ Backward Subsumption, 119055 ] % 1.09/1.53 (133,1) [13815,8]. _t73 => ~box 1~ _t319 [ SNF++, 8970 ] [ Backward Subsumption, 119053 ] % 1.09/1.53 (133,1) [119053,8]. true => ~_t73 [ GEN1 Unit Resolution, 118985, 13815, _t319 ] [ Modal Level Pure Literal Elimination, ~_t73 ] % 1.09/1.53 (134,1) [119055,8]. true => ~_t318 [ Unit Resolution, 119053, 13360, _t73 ] [ Modal Level Pure Literal Elimination, ~_t318 ] % 1.09/1.53 (1,1) [4238,9]. _t64 => box 1 p0 [ Axiom 5 ] [ SNF++, 9863, p0 ] % 1.09/1.53 (1,1) [4240,9]. ~_t121 => box 1 ~_t64 [ Axiom 5 ] [ SNF++, 9865, ~_t64 ] % 1.09/1.53 (1,1) [4242,9]. true => ~_t121 | _t64 [ Axiom 5 ] % 1.09/1.53 (132,1) [8969,9]. _t74 => ~box 1~ _t75 [ SNF ] [ SNF++, 10053, _t75 ] % 1.09/1.53 (1,1) [9863,9]. _t64 => box 1 _t155 [ SNF++, 4238 ] % 1.09/1.53 (1,1) [9865,9]. ~_t121 => box 1 _t285 [ SNF++, 4240 ] % 1.09/1.53 (132,1) [10053,9]. _t74 => ~box 1~ _t310 [ SNF++, 8969 ] [ Backward Subsumption, 119054 ] % 1.09/1.53 (133,1) [13816,9]. true => ~_t319 | _t74 [ SNF++, 8970 ] [ Modal Level Pure Literal Elimination, ~_t319 ] % 1.09/1.53 (132,1) [70281,9]. true => _t121 | ~_t74 [ GEN1, 9865, 10053, 19694, _t285, _t310 ] [ Modal Level Pure Literal Elimination, ~_t74 ] % 1.09/1.53 (132,1) [71127,9]. true => ~_t74 | ~_t64 [ GEN1, 9863, 10053, 20070, _t155, _t310 ] [ Modal Level Pure Literal Elimination, ~_t74 ] % 1.09/1.53 (132,1) [116907,9]. true => ~_t121 | ~_t74 [ LRES, 71127, 4242, ~_t64 ] [ Modal Level Pure Literal Elimination, ~_t74 ] % 1.09/1.53 (133,1) [117930,9]. true => ~_t319 | ~_t121 [ LRES, 116907, 13816, ~_t74 ] [ Modal Level Pure Literal Elimination, ~_t319 ] % 1.09/1.53 (133,1) [118001,9]. true => ~_t319 | _t121 [ LRES, 70281, 13816, ~_t74 ] [ Modal Level Pure Literal Elimination, ~_t319 ] % 1.09/1.53 (133,1) [118985,9]. true => ~_t319 [ LRES, 118001, 117930, _t121 ] [ Modal Level Pure Literal Elimination, ~_t319 ] % 1.09/1.53 (132,1) [8967,10]. true => ~_t75 | ~p0 [ SNF ] [ Modal Level Pure Literal Elimination, ~_t75 ] % 1.09/1.53 (132,1) [8968,10]. true => ~_t75 | _t64 [ SNF ] [ Modal Level Pure Literal Elimination, ~_t75 ] % 1.09/1.53 (1,1) [9864,10]. true => ~_t155 | p0 [ SNF++, 4238 ] % 1.09/1.53 (1,1) [9866,10]. true => ~_t285 | ~_t64 [ SNF++, 4240 ] % 1.09/1.53 (132,1) [10054,10]. true => ~_t310 | _t75 [ SNF++, 8969 ] [ Modal Level Pure Literal Elimination, ~_t310 ] % 1.09/1.53 (132,1) [16347,10]. true => ~_t155 | ~_t75 [ LRES, 8967, 9864, ~p0 ] [ Modal Level Pure Literal Elimination, ~_t75 ] % 1.09/1.53 (132,1) [17742,10]. true => ~_t285 | ~_t75 [ LRES, 9866, 8968, ~_t64 ] [ Modal Level Pure Literal Elimination, ~_t75 ] % 1.09/1.53 (132,1) [19694,10]. true => ~_t310 | ~_t285 [ LRES, 17742, 10054, ~_t75 ] [ Modal Level Pure Literal Elimination, ~_t310 ] % 1.09/1.53 (132,1) [20070,10]. true => ~_t310 | ~_t155 [ LRES, 16347, 10054, ~_t75 ] [ Modal Level Pure Literal Elimination, ~_t310 ] % 1.09/1.53 % SZS output end Refutation % 1.09/1.53 % KSP exiting %------------------------------------------------------------------------------