%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP060_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n017.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:56 PM UTC 2026 % Result : Theorem 2.16s 2.37s % Output : Refutation 2.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP060_1 : TPTP v9.3.0. Released v9.3.0. % 0.13/0.13 % Command : run_ksp %s % 0.17/0.34 % Computer : n017.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Mon May 4 16:54:27 EDT 2026 % 0.17/0.35 % CPUTime : % 0.38/0.62 ----KSP format--- % 0.38/0.62 set(box,FIVE). % 0.38/0.62 usable(formulas). % 0.38/0.62 true. % 0.38/0.62 end_of_list. % 0.38/0.62 sos(formulas). % 0.38/0.62 ~ (<> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( [] ( p0 ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) | <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( ( [] ( <> ( p0 ) ) & [] ( ~ ( p0 ) | [] ( p3 ) ) ) | <> ( [] ( <> ( [] ( ~ ( p0 ) | [] ( p3 ) ) ) ) & [] ( <> ( p0 ) ) ) | ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) | [] ( p3 ) ) ) ) ) | <> ( <> ( [] ( <> ( p0 ) ) ) & p0 & <> ( ~ ( p0 ) | [] ( p3 ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) | <> ( p4 ) ). % 0.38/0.62 end_of_list. % 0.38/0.62 ----------------- % 0.38/0.62 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.dcMO79D9ex/theBenchmark.ksp % 2.16/2.37 % 2.16/2.37 % SZS status Theorem % 2.16/2.37 % 2.16/2.37 ***************** % 2.16/2.37 FOUND PROOF 1 % 2.16/2.37 ***************** % 2.16/2.37 % SZS output start Refutation % 2.16/2.37 % 2.16/2.37 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 2.16/2.37 (1245,1) [11655,0]. _t73 => ~box 1~ _t74 [ SNF ] [ Backward Subsumption, 11736 ] % 2.16/2.37 (1,1) [11656,0]. true => _t73 | ~_t0 [ SNF ] [ Backward Subsumption, 11725 ] % 2.16/2.37 (1,1) [11725,0]. true => _t73 [ Unit Resolution, 3, 11656, _t0 ] [ Modal Level Pure Literal Elimination, _t73 ] % 2.16/2.37 (1245,1) [11736,0]. true => ~box 1~ _t74 [ LHS Unit Resolution, 11725, 11655, _t73 ] [ SNF++, 12329, _t74 ] % 2.16/2.37 (1245,1) [12329,0]. true => ~box 1~ _t290 [ SNF++, 11736 ] % 2.16/2.37 (1245,1) [164958,0]. true => false [ GEN1 Unit Resolution, 164955, 12329, _t290 ] % 2.16/2.37 (1243,1) [11653,1]. _t75 => ~box 1~ _t76 [ SNF ] [ SNF++, 12637, _t76 ] % 2.16/2.37 (1245,1) [11654,1]. true => _t75 | ~_t74 [ SNF ] [ Backward Subsumption, 164956 ] % 2.16/2.37 (1245,1) [12330,1]. true => ~_t290 | _t74 [ SNF++, 11736 ] [ Backward Subsumption, 164957 ] % 2.16/2.37 (1243,1) [12637,1]. _t75 => ~box 1~ _t291 [ SNF++, 11653 ] [ Backward Subsumption, 164952 ] % 2.16/2.37 (1245,1) [22825,1]. true => ~_t290 | _t75 [ LRES, 11654, 12330, ~_t74 ] [ Backward Subsumption, 164955 ] % 2.16/2.37 (1243,1) [164952,1]. true => ~_t75 [ GEN1 Unit Resolution, 164949, 12637, _t291 ] [ Modal Level Pure Literal Elimination, ~_t75 ] % 2.16/2.37 (1245,1) [164955,1]. true => ~_t290 [ Unit Resolution, 164952, 22825, _t75 ] % 2.16/2.37 (1242,1) [11651,2]. _t77 => ~box 1~ _t78 [ SNF ] [ SNF++, 12945, _t78 ] % 2.16/2.37 (1243,1) [11652,2]. true => _t77 | ~_t76 [ SNF ] [ Backward Subsumption, 164950 ] % 2.16/2.37 (1243,1) [12638,2]. true => ~_t291 | _t76 [ SNF++, 11653 ] [ Backward Subsumption, 164951 ] % 2.16/2.37 (1242,1) [12945,2]. _t77 => ~box 1~ _t292 [ SNF++, 11651 ] [ Backward Subsumption, 164946 ] % 2.16/2.37 (1243,1) [22826,2]. true => ~_t291 | _t77 [ LRES, 11652, 12638, ~_t76 ] [ Backward Subsumption, 164949 ] % 2.16/2.37 (1242,1) [164946,2]. true => ~_t77 [ GEN1 Unit Resolution, 164943, 12945, _t292 ] [ Modal Level Pure Literal Elimination, ~_t77 ] % 2.16/2.37 (1243,1) [164949,2]. true => ~_t291 [ Unit Resolution, 164946, 22826, _t77 ] [ Modal Level Pure Literal Elimination, ~_t291 ] % 2.16/2.37 (1241,1) [11649,3]. _t79 => ~box 1~ _t80 [ SNF ] [ SNF++, 13253, _t80 ] % 2.16/2.37 (1242,1) [11650,3]. true => _t79 | ~_t78 [ SNF ] [ Backward Subsumption, 164944 ] % 2.16/2.37 (1242,1) [12946,3]. true => ~_t292 | _t78 [ SNF++, 11651 ] [ Backward Subsumption, 164945 ] % 2.16/2.37 (1241,1) [13253,3]. _t79 => ~box 1~ _t293 [ SNF++, 11649 ] [ Backward Subsumption, 164940 ] % 2.16/2.37 (1242,1) [22827,3]. true => ~_t292 | _t79 [ LRES, 11650, 12946, ~_t78 ] [ Backward Subsumption, 164943 ] % 2.16/2.37 (1241,1) [164940,3]. true => ~_t79 [ GEN1 Unit Resolution, 164937, 13253, _t293 ] [ Modal Level Pure Literal Elimination, ~_t79 ] % 2.16/2.37 (1242,1) [164943,3]. true => ~_t292 [ Unit Resolution, 164940, 22827, _t79 ] [ Modal Level Pure Literal Elimination, ~_t292 ] % 2.16/2.37 (1240,1) [11647,4]. _t81 => ~box 1~ _t82 [ SNF ] [ SNF++, 13561, _t82 ] % 2.16/2.37 (1241,1) [11648,4]. true => _t81 | ~_t80 [ SNF ] [ Backward Subsumption, 164938 ] % 2.16/2.37 (1241,1) [13254,4]. true => ~_t293 | _t80 [ SNF++, 11649 ] [ Backward Subsumption, 164939 ] % 2.16/2.37 (1240,1) [13561,4]. _t81 => ~box 1~ _t294 [ SNF++, 11647 ] [ Backward Subsumption, 164934 ] % 2.16/2.37 (1241,1) [22828,4]. true => ~_t293 | _t81 [ LRES, 11648, 13254, ~_t80 ] [ Backward Subsumption, 164937 ] % 2.16/2.37 (1240,1) [164934,4]. true => ~_t81 [ GEN1 Unit Resolution, 164931, 13561, _t294 ] [ Modal Level Pure Literal Elimination, ~_t81 ] % 2.16/2.37 (1241,1) [164937,4]. true => ~_t293 [ Unit Resolution, 164934, 22828, _t81 ] [ Modal Level Pure Literal Elimination, ~_t293 ] % 2.16/2.37 (1239,1) [11645,5]. _t83 => ~box 1~ _t84 [ SNF ] [ SNF++, 13869, _t84 ] % 2.16/2.37 (1240,1) [11646,5]. true => _t83 | ~_t82 [ SNF ] [ Backward Subsumption, 164932 ] % 2.16/2.37 (1240,1) [13562,5]. true => ~_t294 | _t82 [ SNF++, 11647 ] [ Backward Subsumption, 164933 ] % 2.16/2.37 (1239,1) [13869,5]. _t83 => ~box 1~ _t295 [ SNF++, 11645 ] [ Backward Subsumption, 164928 ] % 2.16/2.37 (1240,1) [22829,5]. true => ~_t294 | _t83 [ LRES, 11646, 13562, ~_t82 ] [ Backward Subsumption, 164931 ] % 2.16/2.37 (1239,1) [164928,5]. true => ~_t83 [ GEN1 Unit Resolution, 164925, 13869, _t295 ] [ Modal Level Pure Literal Elimination, ~_t83 ] % 2.16/2.37 (1240,1) [164931,5]. true => ~_t294 [ Unit Resolution, 164928, 22829, _t83 ] [ Modal Level Pure Literal Elimination, ~_t294 ] % 2.16/2.37 (1238,1) [11643,6]. _t85 => ~box 1~ _t86 [ SNF ] [ SNF++, 14177, _t86 ] % 2.16/2.37 (1239,1) [11644,6]. true => _t85 | ~_t84 [ SNF ] [ Backward Subsumption, 164926 ] % 2.16/2.37 (1239,1) [13870,6]. true => ~_t295 | _t84 [ SNF++, 11645 ] [ Backward Subsumption, 164927 ] % 2.16/2.37 (1238,1) [14177,6]. _t85 => ~box 1~ _t296 [ SNF++, 11643 ] [ Backward Subsumption, 164922 ] % 2.16/2.37 (1239,1) [22830,6]. true => ~_t295 | _t85 [ LRES, 11644, 13870, ~_t84 ] [ Backward Subsumption, 164925 ] % 2.16/2.37 (1238,1) [164922,6]. true => ~_t85 [ GEN1 Unit Resolution, 164919, 14177, _t296 ] [ Modal Level Pure Literal Elimination, ~_t85 ] % 2.16/2.37 (1239,1) [164925,6]. true => ~_t295 [ Unit Resolution, 164922, 22830, _t85 ] [ Modal Level Pure Literal Elimination, ~_t295 ] % 2.16/2.37 (1237,1) [11641,7]. _t87 => ~box 1~ _t88 [ SNF ] [ SNF++, 14485, _t88 ] % 2.16/2.37 (1238,1) [11642,7]. true => _t87 | ~_t86 [ SNF ] [ Backward Subsumption, 164920 ] % 2.16/2.37 (1238,1) [14178,7]. true => ~_t296 | _t86 [ SNF++, 11643 ] [ Backward Subsumption, 164921 ] % 2.16/2.37 (1237,1) [14485,7]. _t87 => ~box 1~ _t297 [ SNF++, 11641 ] [ Backward Subsumption, 164916 ] % 2.16/2.37 (1238,1) [22831,7]. true => ~_t296 | _t87 [ LRES, 11642, 14178, ~_t86 ] [ Backward Subsumption, 164919 ] % 2.16/2.37 (1237,1) [164916,7]. true => ~_t87 [ GEN1 Unit Resolution, 164913, 14485, _t297 ] [ Modal Level Pure Literal Elimination, ~_t87 ] % 2.16/2.37 (1238,1) [164919,7]. true => ~_t296 [ Unit Resolution, 164916, 22831, _t87 ] [ Modal Level Pure Literal Elimination, ~_t296 ] % 2.16/2.37 (1236,1) [11639,8]. _t89 => ~box 1~ _t90 [ SNF ] [ SNF++, 14793, _t90 ] % 2.16/2.37 (1237,1) [11640,8]. true => _t89 | ~_t88 [ SNF ] [ Backward Subsumption, 164914 ] % 2.16/2.37 (1237,1) [14486,8]. true => ~_t297 | _t88 [ SNF++, 11641 ] [ Backward Subsumption, 164915 ] % 2.16/2.37 (1236,1) [14793,8]. _t89 => ~box 1~ _t298 [ SNF++, 11639 ] [ Backward Subsumption, 164910 ] % 2.16/2.37 (1237,1) [22832,8]. true => ~_t297 | _t89 [ LRES, 11640, 14486, ~_t88 ] [ Backward Subsumption, 164913 ] % 2.16/2.37 (1236,1) [164910,8]. true => ~_t89 [ GEN1 Unit Resolution, 164907, 14793, _t298 ] [ Modal Level Pure Literal Elimination, ~_t89 ] % 2.16/2.37 (1237,1) [164913,8]. true => ~_t297 [ Unit Resolution, 164910, 22832, _t89 ] [ Modal Level Pure Literal Elimination, ~_t297 ] % 2.16/2.37 (1235,1) [11637,9]. _t91 => ~box 1~ _t92 [ SNF ] [ SNF++, 15101, _t92 ] % 2.16/2.37 (1236,1) [11638,9]. true => _t91 | ~_t90 [ SNF ] [ Backward Subsumption, 164908 ] % 2.16/2.37 (1236,1) [14794,9]. true => ~_t298 | _t90 [ SNF++, 11639 ] [ Backward Subsumption, 164909 ] % 2.16/2.37 (1235,1) [15101,9]. _t91 => ~box 1~ _t299 [ SNF++, 11637 ] [ Backward Subsumption, 164904 ] % 2.16/2.37 (1236,1) [22833,9]. true => ~_t298 | _t91 [ LRES, 11638, 14794, ~_t90 ] [ Backward Subsumption, 164907 ] % 2.16/2.37 (1235,1) [164904,9]. true => ~_t91 [ GEN1 Unit Resolution, 164901, 15101, _t299 ] [ Modal Level Pure Literal Elimination, ~_t91 ] % 2.16/2.37 (1236,1) [164907,9]. true => ~_t298 [ Unit Resolution, 164904, 22833, _t91 ] [ Modal Level Pure Literal Elimination, ~_t298 ] % 2.16/2.37 (1234,1) [11635,10]. _t93 => ~box 1~ _t94 [ SNF ] [ SNF++, 15409, _t94 ] % 2.16/2.37 (1235,1) [11636,10]. true => _t93 | ~_t92 [ SNF ] [ Backward Subsumption, 164902 ] % 2.16/2.37 (1235,1) [15102,10]. true => ~_t299 | _t92 [ SNF++, 11637 ] [ Backward Subsumption, 164903 ] % 2.16/2.37 (1234,1) [15409,10]. _t93 => ~box 1~ _t300 [ SNF++, 11635 ] [ Backward Subsumption, 164898 ] % 2.16/2.37 (1235,1) [22834,10]. true => ~_t299 | _t93 [ LRES, 11636, 15102, ~_t92 ] [ Backward Subsumption, 164901 ] % 2.16/2.37 (1234,1) [164898,10]. true => ~_t93 [ GEN1 Unit Resolution, 164895, 15409, _t300 ] [ Modal Level Pure Literal Elimination, ~_t93 ] % 2.16/2.37 (1235,1) [164901,10]. true => ~_t299 [ Unit Resolution, 164898, 22834, _t93 ] [ Modal Level Pure Literal Elimination, ~_t299 ] % 2.16/2.37 (1233,1) [11633,11]. _t95 => ~box 1~ _t96 [ SNF ] [ SNF++, 15717, _t96 ] % 2.16/2.37 (1234,1) [11634,11]. true => _t95 | ~_t94 [ SNF ] [ Backward Subsumption, 164896 ] % 2.16/2.37 (1234,1) [15410,11]. true => ~_t300 | _t94 [ SNF++, 11635 ] [ Backward Subsumption, 164897 ] % 2.16/2.37 (1233,1) [15717,11]. _t95 => ~box 1~ _t301 [ SNF++, 11633 ] [ Backward Subsumption, 164892 ] % 2.16/2.37 (1234,1) [22835,11]. true => ~_t300 | _t95 [ LRES, 11634, 15410, ~_t94 ] [ Backward Subsumption, 164895 ] % 2.16/2.37 (1233,1) [164892,11]. true => ~_t95 [ GEN1 Unit Resolution, 164889, 15717, _t301 ] [ Modal Level Pure Literal Elimination, ~_t95 ] % 2.16/2.37 (1234,1) [164895,11]. true => ~_t300 [ Unit Resolution, 164892, 22835, _t95 ] [ Modal Level Pure Literal Elimination, ~_t300 ] % 2.16/2.37 (1232,1) [11631,12]. _t97 => ~box 1~ _t98 [ SNF ] [ SNF++, 16025, _t98 ] % 2.16/2.37 (1233,1) [11632,12]. true => _t97 | ~_t96 [ SNF ] [ Backward Subsumption, 164890 ] % 2.16/2.37 (1233,1) [15718,12]. true => ~_t301 | _t96 [ SNF++, 11633 ] [ Backward Subsumption, 164891 ] % 2.16/2.37 (1232,1) [16025,12]. _t97 => ~box 1~ _t302 [ SNF++, 11631 ] [ Backward Subsumption, 164886 ] % 2.16/2.37 (1233,1) [22836,12]. true => ~_t301 | _t97 [ LRES, 11632, 15718, ~_t96 ] [ Backward Subsumption, 164889 ] % 2.16/2.37 (1232,1) [164886,12]. true => ~_t97 [ GEN1 Unit Resolution, 164883, 16025, _t302 ] [ Modal Level Pure Literal Elimination, ~_t97 ] % 2.16/2.37 (1233,1) [164889,12]. true => ~_t301 [ Unit Resolution, 164886, 22836, _t97 ] [ Modal Level Pure Literal Elimination, ~_t301 ] % 2.16/2.37 (1231,1) [11629,13]. _t99 => ~box 1~ _t100 [ SNF ] [ SNF++, 16333, _t100 ] % 2.16/2.37 (1232,1) [11630,13]. true => _t99 | ~_t98 [ SNF ] [ Backward Subsumption, 164884 ] % 2.16/2.37 (1232,1) [16026,13]. true => ~_t302 | _t98 [ SNF++, 11631 ] [ Backward Subsumption, 164885 ] % 2.16/2.37 (1231,1) [16333,13]. _t99 => ~box 1~ _t303 [ SNF++, 11629 ] [ Backward Subsumption, 164880 ] % 2.16/2.37 (1232,1) [22837,13]. true => ~_t302 | _t99 [ LRES, 11630, 16026, ~_t98 ] [ Backward Subsumption, 164883 ] % 2.16/2.37 (1231,1) [164880,13]. true => ~_t99 [ GEN1 Unit Resolution, 164877, 16333, _t303 ] [ Modal Level Pure Literal Elimination, ~_t99 ] % 2.16/2.37 (1232,1) [164883,13]. true => ~_t302 [ Unit Resolution, 164880, 22837, _t99 ] [ Modal Level Pure Literal Elimination, ~_t302 ] % 2.16/2.37 (1230,1) [11627,14]. _t101 => ~box 1~ _t102 [ SNF ] [ SNF++, 16641, _t102 ] % 2.16/2.37 (1231,1) [11628,14]. true => _t101 | ~_t100 [ SNF ] [ Backward Subsumption, 164878 ] % 2.16/2.37 (1231,1) [16334,14]. true => ~_t303 | _t100 [ SNF++, 11629 ] [ Backward Subsumption, 164879 ] % 2.16/2.37 (1230,1) [16641,14]. _t101 => ~box 1~ _t304 [ SNF++, 11627 ] [ Backward Subsumption, 164874 ] % 2.16/2.37 (1231,1) [22838,14]. true => ~_t303 | _t101 [ LRES, 11628, 16334, ~_t100 ] [ Backward Subsumption, 164877 ] % 2.16/2.37 (1230,1) [164874,14]. true => ~_t101 [ GEN1 Unit Resolution, 164871, 16641, _t304 ] [ Modal Level Pure Literal Elimination, ~_t101 ] % 2.16/2.37 (1231,1) [164877,14]. true => ~_t303 [ Unit Resolution, 164874, 22838, _t101 ] [ Modal Level Pure Literal Elimination, ~_t303 ] % 2.16/2.37 (1229,1) [11625,15]. _t103 => ~box 1~ _t104 [ SNF ] [ SNF++, 16949, _t104 ] % 2.16/2.37 (1230,1) [11626,15]. true => _t103 | ~_t102 [ SNF ] [ Backward Subsumption, 164872 ] % 2.16/2.37 (1230,1) [16642,15]. true => ~_t304 | _t102 [ SNF++, 11627 ] [ Backward Subsumption, 164873 ] % 2.16/2.37 (1229,1) [16949,15]. _t103 => ~box 1~ _t305 [ SNF++, 11625 ] [ Backward Subsumption, 164868 ] % 2.16/2.37 (1230,1) [22839,15]. true => ~_t304 | _t103 [ LRES, 11626, 16642, ~_t102 ] [ Backward Subsumption, 164871 ] % 2.16/2.37 (1229,1) [164868,15]. true => ~_t103 [ GEN1 Unit Resolution, 164865, 16949, _t305 ] [ Modal Level Pure Literal Elimination, ~_t103 ] % 2.16/2.37 (1230,1) [164871,15]. true => ~_t304 [ Unit Resolution, 164868, 22839, _t103 ] [ Modal Level Pure Literal Elimination, ~_t304 ] % 2.16/2.37 (1228,1) [11623,16]. _t105 => ~box 1~ _t106 [ SNF ] [ SNF++, 17257, _t106 ] % 2.16/2.37 (1229,1) [11624,16]. true => _t105 | ~_t104 [ SNF ] [ Backward Subsumption, 164866 ] % 2.16/2.37 (1229,1) [16950,16]. true => ~_t305 | _t104 [ SNF++, 11625 ] [ Backward Subsumption, 164867 ] % 2.16/2.37 (1228,1) [17257,16]. _t105 => ~box 1~ _t306 [ SNF++, 11623 ] [ Backward Subsumption, 164862 ] % 2.16/2.37 (1229,1) [22840,16]. true => ~_t305 | _t105 [ LRES, 11624, 16950, ~_t104 ] [ Backward Subsumption, 164865 ] % 2.16/2.37 (1228,1) [164862,16]. true => ~_t105 [ GEN1 Unit Resolution, 164859, 17257, _t306 ] [ Modal Level Pure Literal Elimination, ~_t105 ] % 2.16/2.37 (1229,1) [164865,16]. true => ~_t305 [ Unit Resolution, 164862, 22840, _t105 ] [ Modal Level Pure Literal Elimination, ~_t305 ] % 2.16/2.37 (1227,1) [11621,17]. _t107 => ~box 1~ _t108 [ SNF ] [ SNF++, 17565, _t108 ] % 2.16/2.37 (1228,1) [11622,17]. true => _t107 | ~_t106 [ SNF ] [ Backward Subsumption, 164860 ] % 2.36/2.55 (1228,1) [17258,17]. true => ~_t306 | _t106 [ SNF++, 11623 ] [ Backward Subsumption, 164861 ] % 2.36/2.55 (1227,1) [17565,17]. _t107 => ~box 1~ _t307 [ SNF++, 11621 ] [ Backward Subsumption, 164857 ] % 2.36/2.55 (1228,1) [22841,17]. true => ~_t306 | _t107 [ LRES, 11622, 17258, ~_t106 ] [ Backward Subsumption, 164859 ] % 2.36/2.55 (1227,1) [164857,17]. true => ~_t107 [ GEN1 Unit Resolution, 164856, 17565, _t307 ] [ Modal Level Pure Literal Elimination, ~_t107 ] % 2.36/2.55 (1228,1) [164859,17]. true => ~_t306 [ Unit Resolution, 164857, 22841, _t107 ] [ Modal Level Pure Literal Elimination, ~_t306 ] % 2.36/2.55 (1226,1) [11619,18]. _t70 => ~box 1~ _t71 [ SNF ] [ SNF++, 17873, _t71 ] % 2.36/2.55 (1227,1) [11620,18]. true => ~_t108 | _t70 [ SNF ] [ Backward Subsumption, 164855 ] % 2.36/2.55 (1227,1) [17566,18]. true => ~_t307 | _t108 [ SNF++, 11621 ] [ Backward Subsumption, 164856 ] % 2.36/2.55 (1226,1) [17873,18]. _t70 => ~box 1~ _t289 [ SNF++, 11619 ] [ Backward Subsumption, 164853 ] % 2.36/2.55 (1226,1) [164853,18]. true => ~_t70 [ GEN1 Unit Resolution, 164796, 17873, _t289 ] [ Modal Level Pure Literal Elimination, ~_t70 ] % 2.36/2.55 (1227,1) [164855,18]. true => ~_t108 [ Unit Resolution, 164853, 11620, _t70 ] [ Modal Level Pure Literal Elimination, ~_t108 ] % 2.36/2.55 (1227,1) [164856,18]. true => ~_t307 [ Unit Resolution, 164855, 17566, _t108 ] [ Modal Level Pure Literal Elimination, ~_t307 ] % 2.36/2.55 (1,1) [2259,19]. _t61 => box 1 ~p1 [ Axiom 5 ] [ SNF++, 17935, ~p1 ] % 2.36/2.55 (1,1) [2673,19]. _t65 => box 1 p1 [ Axiom 5 ] [ SNF++, 17947, p1 ] % 2.36/2.55 (1,1) [2675,19]. ~_t125 => box 1 ~_t65 [ Axiom 5 ] [ SNF++, 17949, ~_t65 ] % 2.36/2.55 (1,1) [2677,19]. true => ~_t125 | _t65 [ Axiom 5 ] % 2.36/2.55 (1,1) [2727,19]. _t64 => box 1 _t65 [ SNF ] [ SNF++, 17953, _t65 ] % 2.36/2.55 (34,1) [2905,19]. _t66 => ~box 1~ ~p1 [ SNF ] [ SNF++, 18131, ~p1 ] % 2.36/2.55 (1226,1) [11616,19]. true => ~_t71 | _t66 [ SNF ] [ Modal Level Pure Literal Elimination, ~_t71 ] % 2.36/2.55 (1225,1) [11617,19]. _t72 => ~box 1~ _t65 [ SNF ] [ SNF++, 18125, _t65 ] % 2.36/2.55 (1226,1) [11618,19]. true => _t72 | ~_t71 [ SNF ] [ Modal Level Pure Literal Elimination, ~_t71 ] % 2.36/2.55 (1226,1) [17874,19]. true => ~_t289 | _t71 [ SNF++, 11619 ] [ Modal Level Pure Literal Elimination, ~_t289 ] % 2.36/2.55 (1,1) [17947,19]. _t65 => box 1 _t185 [ SNF++, 2673 ] % 2.36/2.55 (1,1) [17949,19]. ~_t125 => box 1 _t186 [ SNF++, 2675 ] % 2.36/2.55 (1225,1) [18125,19]. _t72 => ~box 1~ _t188 [ SNF++, 11617 ] [ Backward Subsumption, 164854 ] % 2.36/2.55 (34,1) [18131,19]. _t66 => ~box 1~ _t179 [ SNF++, 2905 ] % 2.36/2.55 (1226,1) [22803,19]. true => ~_t289 | _t72 [ LRES, 11618, 17874, ~_t71 ] [ Modal Level Pure Literal Elimination, ~_t289 ] % 2.36/2.55 (34,1) [46138,19]. true => ~_t66 | ~_t65 [ GEN1, 17947, 18131, 23376, _t185, _t179 ] % 2.36/2.55 (1225,1) [76683,19]. true => _t125 | ~_t72 [ GEN1, 17949, 18125, 23525, _t186, _t188 ] [ Modal Level Pure Literal Elimination, ~_t72 ] % 2.36/2.55 (34,1) [158970,19]. true => ~_t125 | ~_t66 [ LRES, 46138, 2677, ~_t65 ] % 2.36/2.55 (1226,1) [159073,19]. true => ~_t125 | ~_t71 [ LRES, 158970, 11616, ~_t66 ] [ Modal Level Pure Literal Elimination, ~_t71 ] % 2.36/2.55 (1226,1) [159120,19]. true => ~_t289 | _t125 [ LRES, 76683, 22803, ~_t72 ] [ Modal Level Pure Literal Elimination, ~_t289 ] % 2.36/2.55 (1226,1) [160573,19]. true => ~_t289 | ~_t125 [ LRES, 159073, 17874, ~_t71 ] [ Modal Level Pure Literal Elimination, ~_t289 ] % 2.36/2.55 (1226,1) [164796,19]. true => ~_t289 [ LRES, 160573, 159120, ~_t125 ] [ Modal Level Pure Literal Elimination, ~_t289 ] % 2.36/2.55 (1,1) [17936,20]. true => ~_t179 | ~p1 [ SNF++, 2259 ] % 2.36/2.55 (1,1) [17948,20]. true => ~_t185 | p1 [ SNF++, 2673 ] % 2.36/2.55 (1,1) [17950,20]. true => ~_t186 | ~_t65 [ SNF++, 2675 ] % 2.36/2.55 (1,1) [17954,20]. true => ~_t188 | _t65 [ SNF++, 2727 ] % 2.36/2.55 (1,1) [23376,20]. true => ~_t185 | ~_t179 [ LRES, 17936, 17948, ~p1 ] % 2.36/2.55 (1,1) [23525,20]. true => ~_t188 | ~_t186 [ LRES, 17950, 17954, ~_t65 ] % 2.36/2.55 % SZS output end Refutation % 2.36/2.56 % KSP exiting %------------------------------------------------------------------------------