%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP046_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n011.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.26s 1.46s % Output : Refutation 1.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP046_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.15/0.33 % Computer : n011.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Mon May 4 16:26:32 EDT 2026 % 0.15/0.34 % CPUTime : % 0.42/0.59 ----KSP format--- % 0.42/0.59 set(box,FIVE). % 0.42/0.59 usable(formulas). % 0.42/0.59 true. % 0.42/0.59 end_of_list. % 0.42/0.59 sos(formulas). % 0.42/0.59 ~ ([] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( p0 ) | [] ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( [] ( $false ) ) | <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) | <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) | <> ( [] ( p0 ) & [] ( ~ ( p0 ) ) ) | <> ( [] ( [] ( ~ ( p0 ) ) | p0 ) & <> ( <> ( <> ( p0 ) & ~ ( p0 ) ) ) ) | <> ( [] ( <> ( ~ ( p0 ) ) | p0 ) & <> ( <> ( [] ( p0 ) & ~ ( p0 ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( p0 ) | [] ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( [] ( $false ) ) ) | <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) | <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) | <> ( <> ( [] ( p0 ) & [] ( ~ ( p0 ) ) ) ) | <> ( <> ( [] ( [] ( ~ ( p0 ) ) | p0 ) & <> ( <> ( <> ( p0 ) & ~ ( p0 ) ) ) ) ) | <> ( <> ( [] ( <> ( ~ ( p0 ) ) | p0 ) & <> ( <> ( [] ( p0 ) & ~ ( p0 ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( p0 ) | [] ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( [] ( $false ) ) ) ) | <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) | <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) | <> ( <> ( <> ( [] ( p0 ) & [] ( ~ ( p0 ) ) ) ) ) | <> ( <> ( <> ( [] ( [] ( ~ ( p0 ) ) | p0 ) & <> ( <> ( <> ( p0 ) & ~ ( p0 ) ) ) ) ) ) | <> ( <> ( <> ( [] ( <> ( ~ ( p0 ) ) | p0 ) & <> ( <> ( [] ( p0 ) & ~ ( p0 ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( p0 ) | [] ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) | <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( [] ( p0 ) & [] ( ~ ( p0 ) ) ) ) ) ) | <> ( <> ( <> ( <> ( [] ( [] ( ~ ( p0 ) ) | p0 ) & <> ( <> ( <> ( p0 ) & ~ ( p0 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( [] ( <> ( ~ ( p0 ) ) | p0 ) & <> ( <> ( [] ( p0 ) & ~ ( p0 ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( p0 ) | [] ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & [] ( ~ ( p0 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( [] ( [] ( ~ ( p0 ) ) | p0 ) & <> ( <> ( <> ( p0 ) & ~ ( p0 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( [] ( <> ( ~ ( p0 ) ) | p0 ) & <> ( <> ( [] ( p0 ) & ~ ( p0 ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( p0 ) | [] ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & [] ( ~ ( p0 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( [] ( [] ( ~ ( p0 ) ) | p0 ) & <> ( <> ( <> ( p0 ) & ~ ( p0 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( ~ ( p0 ) ) | p0 ) & <> ( <> ( [] ( p0 ) & ~ ( p0 ) ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( p0 ) | [] ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( [] ( ~ ( p0 ) ) | p0 ) & <> ( <> ( <> ( p0 ) & ~ ( p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( ~ ( p0 ) ) | p0 ) & <> ( <> ( [] ( p0 ) & ~ ( p0 ) ) ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( p0 ) | [] ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( [] ( ~ ( p0 ) ) | p0 ) & <> ( <> ( <> ( p0 ) & ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( ~ ( p0 ) ) | p0 ) & <> ( <> ( [] ( p0 ) & ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( p0 ) | [] ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( [] ( ~ ( p0 ) ) | p0 ) & <> ( <> ( <> ( p0 ) & ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( ~ ( p0 ) ) | p0 ) & <> ( <> ( [] ( p0 ) & ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( p0 ) | [] ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( [] ( ~ ( p0 ) ) | p0 ) & <> ( <> ( <> ( p0 ) & ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( ~ ( p0 ) ) | p0 ) & <> ( <> ( [] ( p0 ) & ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) ). % 0.42/0.59 end_of_list. % 0.42/0.59 ----------------- % 0.42/0.59 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/sandbox/tmp/tmp.SClKn3aufe/theBenchmark.ksp % 1.26/1.46 % 1.26/1.46 % SZS status Theorem % 1.26/1.46 % 1.26/1.46 ***************** % 1.26/1.46 FOUND PROOF 1 % 1.26/1.46 ***************** % 1.26/1.46 % SZS output start Refutation % 1.26/1.46 % 1.26/1.46 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 1.26/1.46 (217,1) [11148,0]. _t74 => ~box 1~ _t75 [ SNF ] [ Backward Subsumption, 11270 ] % 1.26/1.46 (1,1) [11149,0]. true => _t74 | ~_t0 [ SNF ] [ Backward Subsumption, 11219 ] % 1.26/1.46 (1,1) [11219,0]. true => _t74 [ Unit Resolution, 3, 11149, _t0 ] [ Modal Level Pure Literal Elimination, _t74 ] % 1.26/1.46 (217,1) [11270,0]. true => ~box 1~ _t75 [ LHS Unit Resolution, 11219, 11148, _t74 ] [ SNF++, 13245, _t75 ] % 1.26/1.46 (217,1) [13245,0]. true => ~box 1~ _t337 [ SNF++, 11270 ] % 1.26/1.46 (217,1) [158774,0]. true => false [ GEN1 Unit Resolution, 158773, 13245, _t337 ] % 1.26/1.46 (216,1) [11147,1]. _t75 => ~box 1~ _t76 [ SNF ] [ SNF++, 12417, _t76 ] % 1.26/1.46 (216,1) [12417,1]. _t75 => ~box 1~ _t336 [ SNF++, 11147 ] [ Backward Subsumption, 158772 ] % 1.26/1.46 (217,1) [13246,1]. true => ~_t337 | _t75 [ SNF++, 11270 ] [ Backward Subsumption, 158773 ] % 1.26/1.46 (216,1) [158772,1]. true => ~_t75 [ GEN1 Unit Resolution, 158771, 12417, _t336 ] [ Modal Level Pure Literal Elimination, ~_t75 ] % 1.26/1.46 (217,1) [158773,1]. true => ~_t337 [ Unit Resolution, 158772, 13246, _t75 ] % 1.26/1.46 (215,1) [11146,2]. _t76 => ~box 1~ _t77 [ SNF ] [ SNF++, 13375, _t77 ] % 1.26/1.46 (216,1) [12418,2]. true => ~_t336 | _t76 [ SNF++, 11147 ] [ Backward Subsumption, 158771 ] % 1.26/1.46 (215,1) [13375,2]. _t76 => ~box 1~ _t338 [ SNF++, 11146 ] [ Backward Subsumption, 158770 ] % 1.26/1.46 (215,1) [158770,2]. true => ~_t76 [ GEN1 Unit Resolution, 158769, 13375, _t338 ] [ Modal Level Pure Literal Elimination, ~_t76 ] % 1.26/1.46 (216,1) [158771,2]. true => ~_t336 [ Unit Resolution, 158770, 12418, _t76 ] [ Modal Level Pure Literal Elimination, ~_t336 ] % 1.26/1.46 (214,1) [11145,3]. _t77 => ~box 1~ _t78 [ SNF ] [ SNF++, 13859, _t78 ] % 1.26/1.46 (215,1) [13376,3]. true => ~_t338 | _t77 [ SNF++, 11146 ] [ Backward Subsumption, 158769 ] % 1.26/1.46 (214,1) [13859,3]. _t77 => ~box 1~ _t339 [ SNF++, 11145 ] [ Backward Subsumption, 158768 ] % 1.26/1.46 (214,1) [158768,3]. true => ~_t77 [ GEN1 Unit Resolution, 158767, 13859, _t339 ] [ Modal Level Pure Literal Elimination, ~_t77 ] % 1.26/1.46 (215,1) [158769,3]. true => ~_t338 [ Unit Resolution, 158768, 13376, _t77 ] [ Modal Level Pure Literal Elimination, ~_t338 ] % 1.26/1.46 (213,1) [11144,4]. _t78 => ~box 1~ _t79 [ SNF ] [ SNF++, 14343, _t79 ] % 1.26/1.46 (214,1) [13860,4]. true => ~_t339 | _t78 [ SNF++, 11145 ] [ Backward Subsumption, 158767 ] % 1.26/1.46 (213,1) [14343,4]. _t78 => ~box 1~ _t340 [ SNF++, 11144 ] [ Backward Subsumption, 158766 ] % 1.26/1.46 (213,1) [158766,4]. true => ~_t78 [ GEN1 Unit Resolution, 158765, 14343, _t340 ] [ Modal Level Pure Literal Elimination, ~_t78 ] % 1.26/1.46 (214,1) [158767,4]. true => ~_t339 [ Unit Resolution, 158766, 13860, _t78 ] [ Modal Level Pure Literal Elimination, ~_t339 ] % 1.26/1.46 (212,1) [11143,5]. _t79 => ~box 1~ _t80 [ SNF ] [ SNF++, 14827, _t80 ] % 1.26/1.46 (213,1) [14344,5]. true => ~_t340 | _t79 [ SNF++, 11144 ] [ Backward Subsumption, 158765 ] % 1.26/1.46 (212,1) [14827,5]. _t79 => ~box 1~ _t341 [ SNF++, 11143 ] [ Backward Subsumption, 158764 ] % 1.26/1.46 (212,1) [158764,5]. true => ~_t79 [ GEN1 Unit Resolution, 158763, 14827, _t341 ] [ Modal Level Pure Literal Elimination, ~_t79 ] % 1.26/1.46 (213,1) [158765,5]. true => ~_t340 [ Unit Resolution, 158764, 14344, _t79 ] [ Modal Level Pure Literal Elimination, ~_t340 ] % 1.26/1.46 (211,1) [11142,6]. _t80 => ~box 1~ _t81 [ SNF ] [ SNF++, 15311, _t81 ] % 1.26/1.46 (212,1) [14828,6]. true => ~_t341 | _t80 [ SNF++, 11143 ] [ Backward Subsumption, 158763 ] % 1.26/1.46 (211,1) [15311,6]. _t80 => ~box 1~ _t342 [ SNF++, 11142 ] [ Backward Subsumption, 158762 ] % 1.26/1.46 (211,1) [158762,6]. true => ~_t80 [ GEN1 Unit Resolution, 158761, 15311, _t342 ] [ Modal Level Pure Literal Elimination, ~_t80 ] % 1.26/1.46 (212,1) [158763,6]. true => ~_t341 [ Unit Resolution, 158762, 14828, _t80 ] [ Modal Level Pure Literal Elimination, ~_t341 ] % 1.26/1.46 (210,1) [11141,7]. _t81 => ~box 1~ _t82 [ SNF ] [ SNF++, 15795, _t82 ] % 1.26/1.46 (211,1) [15312,7]. true => ~_t342 | _t81 [ SNF++, 11142 ] [ Backward Subsumption, 158761 ] % 1.26/1.46 (210,1) [15795,7]. _t81 => ~box 1~ _t343 [ SNF++, 11141 ] [ Backward Subsumption, 158760 ] % 1.26/1.46 (210,1) [158760,7]. true => ~_t81 [ GEN1 Unit Resolution, 158759, 15795, _t343 ] [ Modal Level Pure Literal Elimination, ~_t81 ] % 1.35/1.59 (211,1) [158761,7]. true => ~_t342 [ Unit Resolution, 158760, 15312, _t81 ] [ Modal Level Pure Literal Elimination, ~_t342 ] % 1.35/1.59 (209,1) [11140,8]. _t82 => ~box 1~ _t83 [ SNF ] [ SNF++, 16279, _t83 ] % 1.35/1.59 (210,1) [15796,8]. true => ~_t343 | _t82 [ SNF++, 11141 ] [ Backward Subsumption, 158759 ] % 1.35/1.59 (209,1) [16279,8]. _t82 => ~box 1~ _t344 [ SNF++, 11140 ] [ Backward Subsumption, 158758 ] % 1.35/1.59 (209,1) [158758,8]. true => ~_t82 [ GEN1 Unit Resolution, 158757, 16279, _t344 ] [ Modal Level Pure Literal Elimination, ~_t82 ] % 1.35/1.59 (210,1) [158759,8]. true => ~_t343 [ Unit Resolution, 158758, 15796, _t82 ] [ Modal Level Pure Literal Elimination, ~_t343 ] % 1.35/1.59 (208,1) [11139,9]. _t83 => ~box 1~ _t84 [ SNF ] [ SNF++, 12287, _t84 ] % 1.35/1.59 (208,1) [12287,9]. _t83 => ~box 1~ _t335 [ SNF++, 11139 ] [ Backward Subsumption, 158755 ] % 1.35/1.59 (209,1) [16280,9]. true => ~_t344 | _t83 [ SNF++, 11140 ] [ Backward Subsumption, 158757 ] % 1.35/1.59 (208,1) [158755,9]. true => ~_t83 [ GEN1 Unit Resolution, 158485, 12287, _t335 ] [ Modal Level Pure Literal Elimination, ~_t83 ] % 1.35/1.59 (209,1) [158757,9]. true => ~_t344 [ Unit Resolution, 158755, 16280, _t83 ] [ Modal Level Pure Literal Elimination, ~_t344 ] % 1.35/1.59 (12,1) [1192,10]. _t26 => ~box 1~ ~p0 [ Axiom 5 ] [ SNF++, 11341, ~p0 ] % 1.35/1.59 (1,1) [1421,10]. _t29 => box 1 p0 [ Axiom 5 ] [ SNF++, 11523, p0 ] % 1.35/1.59 (1,1) [1423,10]. ~_t99 => box 1 ~_t29 [ Axiom 5 ] [ SNF++, 11525, ~_t29 ] % 1.35/1.59 (1,1) [1425,10]. true => ~_t99 | _t29 [ Axiom 5 ] % 1.35/1.59 (16,1) [2727,10]. _t43 => ~box 1~ p0 [ Axiom 5 ] [ SNF++, 11373, p0 ] % 1.35/1.59 (208,1) [11136,10]. true => ~_t84 | _t26 [ SNF ] [ Modal Level Pure Literal Elimination, ~_t84 ] % 1.35/1.59 (207,1) [11137,10]. _t85 => ~box 1~ _t29 [ SNF ] [ SNF++, 11347, _t29 ] % 1.35/1.59 (208,1) [11138,10]. true => _t85 | ~_t84 [ SNF ] [ Modal Level Pure Literal Elimination, ~_t84 ] % 1.35/1.59 (12,1) [11341,10]. _t26 => ~box 1~ _t156 [ SNF++, 1192 ] % 1.35/1.59 (207,1) [11347,10]. _t85 => ~box 1~ _t159 [ SNF++, 11137 ] [ Backward Subsumption, 158756 ] % 1.35/1.59 (1,1) [11523,10]. _t29 => box 1 _t171 [ SNF++, 1421 ] % 1.35/1.59 (1,1) [11525,10]. ~_t99 => box 1 _t235 [ SNF++, 1423 ] % 1.35/1.59 (208,1) [12288,10]. true => ~_t335 | _t84 [ SNF++, 11139 ] [ Modal Level Pure Literal Elimination, ~_t335 ] % 1.35/1.59 (208,1) [20573,10]. true => ~_t335 | _t85 [ LRES, 11138, 12288, ~_t84 ] [ Modal Level Pure Literal Elimination, ~_t335 ] % 1.35/1.59 (12,1) [23728,10]. true => ~_t29 | ~_t26 [ GEN1, 11523, 11341, 20384, _t171, _t156 ] % 1.35/1.59 (207,1) [38893,10]. true => _t99 | ~_t85 [ GEN1, 11525, 11347, 21019, _t235, _t159 ] [ Modal Level Pure Literal Elimination, ~_t85 ] % 1.35/1.59 (208,1) [87559,10]. true => ~_t84 | ~_t29 [ LRES, 23728, 11136, ~_t26 ] [ Modal Level Pure Literal Elimination, ~_t84 ] % 1.35/1.59 (208,1) [87808,10]. true => ~_t99 | ~_t84 [ LRES, 87559, 1425, ~_t29 ] [ Modal Level Pure Literal Elimination, ~_t84 ] % 1.35/1.59 (208,1) [106163,10]. true => ~_t335 | _t99 [ LRES, 38893, 20573, ~_t85 ] [ Modal Level Pure Literal Elimination, ~_t335 ] % 1.35/1.59 (208,1) [156769,10]. true => ~_t335 | ~_t99 [ LRES, 87808, 12288, ~_t84 ] [ Modal Level Pure Literal Elimination, ~_t335 ] % 1.35/1.59 (208,1) [158485,10]. true => ~_t335 [ LRES, 156769, 106163, ~_t99 ] [ Modal Level Pure Literal Elimination, ~_t335 ] % 1.35/1.59 (12,1) [11342,11]. true => ~_t156 | ~p0 [ SNF++, 1192 ] % 1.35/1.59 (207,1) [11348,11]. true => ~_t159 | _t29 [ SNF++, 11137 ] % 1.35/1.59 (16,1) [11374,11]. true => ~_t171 | p0 [ SNF++, 2727 ] % 1.35/1.59 (1,1) [11526,11]. true => ~_t235 | ~_t29 [ SNF++, 1423 ] % 1.35/1.59 (16,1) [20384,11]. true => ~_t171 | ~_t156 [ LRES, 11342, 11374, ~p0 ] % 1.35/1.59 (207,1) [21019,11]. true => ~_t235 | ~_t159 [ LRES, 11526, 11348, ~_t29 ] % 1.35/1.59 % SZS output end Refutation % 0.46/1.60 % KSP exiting %------------------------------------------------------------------------------