%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP025_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:53 PM UTC 2026 % Result : Theorem 0.37s 0.61s % Output : Refutation 0.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : SYP025_1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.13 % Command : run_ksp %s % 0.14/0.34 % Computer : n011.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Mon May 4 16:12:32 EDT 2026 % 0.14/0.34 % CPUTime : % 0.37/0.59 ----KSP format--- % 0.37/0.60 usable(formulas). % 0.37/0.60 true. % 0.37/0.60 end_of_list. % 0.37/0.60 sos(formulas). % 0.37/0.60 ~ (<> ( ~ ( ( [] ( ~ ( 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 ) ) ) ) | <> ( ( [] ( <> ( p0 ) ) & [] ( ~ ( p0 ) | [] ( p3 ) ) ) | <> ( [] ( <> ( [] ( ~ ( p0 ) | [] ( p3 ) ) ) ) & [] ( <> ( p0 ) ) ) | ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) | [] ( p3 ) ) ) ) ) | <> ( <> ( [] ( <> ( p0 ) ) ) & p0 & <> ( ~ ( p0 ) | [] ( p3 ) ) ) | <> ( [] ( ~ ( p0 ) | [] ( p3 ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) | <> ( p4 ) ). % 0.37/0.60 end_of_list. % 0.37/0.60 ----------------- % 0.37/0.60 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.GtHkj1d06r/theBenchmark.ksp % 0.37/0.61 % 0.37/0.61 % SZS status Theorem % 0.37/0.61 % 0.37/0.61 ***************** % 0.37/0.61 FOUND PROOF 1 % 0.37/0.61 ***************** % 0.37/0.61 % SZS output start Refutation % 0.37/0.61 % 0.37/0.61 (1,1) [1,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.37/0.61 (1,1) [152,0]. _t0 => box 1 _t2 [ SNF ] [ Backward Subsumption, 249 ] % 0.37/0.61 (449,1) [238,0]. _t0 => ~box 1~ _t56 [ SNF ] [ Backward Subsumption, 244 ] % 0.37/0.61 (449,1) [244,0]. true => ~box 1~ _t56 [ LHS Unit Resolution, 1, 238, _t0 ] [ SNF++, 632, _t56 ] % 0.37/0.61 (1,1) [249,0]. true => box 1 _t2 [ LHS Unit Resolution, 1, 152, _t0 ] [ SNF++, 622, _t2 ] % 0.37/0.61 (1,1) [622,0]. true => box 1 _t114 [ SNF++, 249 ] % 0.37/0.61 (449,1) [632,0]. true => ~box 1~ _t115 [ SNF++, 244 ] % 0.37/0.61 (449,1) [1385,0]. true => false [ GEN1, 622, 632, 1384, _t114, _t115 ] % 0.37/0.61 (1,1) [139,1]. _t2 => box 1 _t4 [ SNF ] [ SNF++, 594, _t4 ] % 0.37/0.61 (447,1) [237,1]. _t56 => ~box 1~ _t58 [ SNF ] [ SNF++, 620, _t58 ] % 0.37/0.61 (1,1) [594,1]. _t2 => box 1 _t112 [ SNF++, 139 ] % 0.37/0.61 (447,1) [620,1]. _t56 => ~box 1~ _t113 [ SNF++, 237 ] % 0.37/0.61 (1,1) [623,1]. true => ~_t114 | _t2 [ SNF++, 249 ] % 0.37/0.61 (449,1) [633,1]. true => ~_t115 | _t56 [ SNF++, 244 ] % 0.37/0.61 (447,1) [1382,1]. true => ~_t56 | ~_t2 [ GEN1, 594, 620, 1381, _t112, _t113 ] % 0.37/0.61 (447,1) [1383,1]. true => ~_t114 | ~_t56 [ LRES, 1382, 623, ~_t2 ] % 0.37/0.61 (449,1) [1384,1]. true => ~_t115 | ~_t114 [ LRES, 1383, 633, ~_t56 ] % 0.37/0.61 (1,1) [126,2]. _t4 => box 1 _t6 [ SNF ] [ SNF++, 560, _t6 ] % 0.37/0.61 (446,1) [236,2]. _t58 => ~box 1~ _t60 [ SNF ] [ SNF++, 592, _t60 ] % 0.37/0.61 (1,1) [560,2]. _t4 => box 1 _t110 [ SNF++, 126 ] % 0.37/0.61 (446,1) [592,2]. _t58 => ~box 1~ _t111 [ SNF++, 236 ] % 0.37/0.61 (1,1) [595,2]. true => ~_t112 | _t4 [ SNF++, 139 ] % 0.37/0.61 (447,1) [621,2]. true => ~_t113 | _t58 [ SNF++, 237 ] % 0.37/0.61 (446,1) [1379,2]. true => ~_t58 | ~_t4 [ GEN1, 560, 592, 1378, _t110, _t111 ] % 0.37/0.61 (446,1) [1380,2]. true => ~_t112 | ~_t58 [ LRES, 1379, 595, ~_t4 ] % 0.37/0.61 (447,1) [1381,2]. true => ~_t113 | ~_t112 [ LRES, 1380, 621, ~_t58 ] % 0.37/0.61 (1,1) [113,3]. _t6 => box 1 _t8 [ SNF ] [ SNF++, 526, _t8 ] % 0.37/0.61 (445,1) [235,3]. _t60 => ~box 1~ _t62 [ SNF ] [ SNF++, 558, _t62 ] % 0.37/0.61 (1,1) [526,3]. _t6 => box 1 _t108 [ SNF++, 113 ] % 0.37/0.61 (445,1) [558,3]. _t60 => ~box 1~ _t109 [ SNF++, 235 ] % 0.37/0.61 (1,1) [561,3]. true => ~_t110 | _t6 [ SNF++, 126 ] % 0.37/0.61 (446,1) [593,3]. true => ~_t111 | _t60 [ SNF++, 236 ] % 0.37/0.61 (445,1) [1376,3]. true => ~_t60 | ~_t6 [ GEN1, 526, 558, 1375, _t108, _t109 ] % 0.37/0.61 (445,1) [1377,3]. true => ~_t110 | ~_t60 [ LRES, 1376, 561, ~_t6 ] % 0.37/0.61 (446,1) [1378,3]. true => ~_t111 | ~_t110 [ LRES, 1377, 593, ~_t60 ] % 0.37/0.61 (1,1) [100,4]. _t8 => box 1 _t10 [ SNF ] [ SNF++, 492, _t10 ] % 0.37/0.61 (444,1) [234,4]. _t62 => ~box 1~ _t64 [ SNF ] [ SNF++, 524, _t64 ] % 0.37/0.61 (1,1) [492,4]. _t8 => box 1 _t106 [ SNF++, 100 ] % 0.37/0.61 (444,1) [524,4]. _t62 => ~box 1~ _t107 [ SNF++, 234 ] % 0.37/0.61 (1,1) [527,4]. true => ~_t108 | _t8 [ SNF++, 113 ] % 0.37/0.61 (445,1) [559,4]. true => ~_t109 | _t62 [ SNF++, 235 ] % 0.37/0.61 (444,1) [1373,4]. true => ~_t62 | ~_t8 [ GEN1, 492, 524, 1372, _t106, _t107 ] % 0.37/0.61 (444,1) [1374,4]. true => ~_t108 | ~_t62 [ LRES, 1373, 527, ~_t8 ] % 0.37/0.61 (445,1) [1375,4]. true => ~_t109 | ~_t108 [ LRES, 1374, 559, ~_t62 ] % 0.37/0.61 (1,1) [87,5]. _t10 => box 1 _t12 [ SNF ] [ SNF++, 458, _t12 ] % 0.37/0.61 (443,1) [233,5]. _t64 => ~box 1~ _t66 [ SNF ] [ SNF++, 490, _t66 ] % 0.37/0.61 (1,1) [458,5]. _t10 => box 1 _t104 [ SNF++, 87 ] % 0.37/0.61 (443,1) [490,5]. _t64 => ~box 1~ _t105 [ SNF++, 233 ] % 0.37/0.61 (1,1) [493,5]. true => ~_t106 | _t10 [ SNF++, 100 ] % 0.37/0.61 (444,1) [525,5]. true => ~_t107 | _t64 [ SNF++, 234 ] % 0.37/0.61 (443,1) [1370,5]. true => ~_t64 | ~_t10 [ GEN1, 458, 490, 1369, _t104, _t105 ] % 0.37/0.61 (443,1) [1371,5]. true => ~_t106 | ~_t64 [ LRES, 1370, 493, ~_t10 ] % 0.37/0.61 (444,1) [1372,5]. true => ~_t107 | ~_t106 [ LRES, 1371, 525, ~_t64 ] % 0.37/0.61 (1,1) [74,6]. _t12 => box 1 _t14 [ SNF ] [ SNF++, 424, _t14 ] % 0.37/0.61 (442,1) [232,6]. _t66 => ~box 1~ _t68 [ SNF ] [ SNF++, 456, _t68 ] % 0.37/0.61 (1,1) [424,6]. _t12 => box 1 _t102 [ SNF++, 74 ] % 0.37/0.61 (442,1) [456,6]. _t66 => ~box 1~ _t103 [ SNF++, 232 ] % 0.37/0.61 (1,1) [459,6]. true => ~_t104 | _t12 [ SNF++, 87 ] % 0.37/0.61 (443,1) [491,6]. true => ~_t105 | _t66 [ SNF++, 233 ] % 0.37/0.61 (442,1) [1367,6]. true => ~_t66 | ~_t12 [ GEN1, 424, 456, 1366, _t102, _t103 ] % 0.37/0.61 (442,1) [1368,6]. true => ~_t104 | ~_t66 [ LRES, 1367, 459, ~_t12 ] % 0.37/0.61 (443,1) [1369,6]. true => ~_t105 | ~_t104 [ LRES, 1368, 491, ~_t66 ] % 0.37/0.61 (1,1) [61,7]. _t14 => box 1 _t16 [ SNF ] [ SNF++, 390, _t16 ] % 0.37/0.61 (441,1) [231,7]. _t68 => ~box 1~ _t70 [ SNF ] [ SNF++, 422, _t70 ] % 0.37/0.61 (1,1) [390,7]. _t14 => box 1 _t100 [ SNF++, 61 ] % 0.37/0.61 (441,1) [422,7]. _t68 => ~box 1~ _t101 [ SNF++, 231 ] % 0.37/0.61 (1,1) [425,7]. true => ~_t102 | _t14 [ SNF++, 74 ] % 0.37/0.61 (442,1) [457,7]. true => ~_t103 | _t68 [ SNF++, 232 ] % 0.37/0.61 (441,1) [1364,7]. true => ~_t68 | ~_t14 [ GEN1, 390, 422, 1363, _t100, _t101 ] % 0.37/0.61 (441,1) [1365,7]. true => ~_t102 | ~_t68 [ LRES, 1364, 425, ~_t14 ] % 0.37/0.61 (442,1) [1366,7]. true => ~_t103 | ~_t102 [ LRES, 1365, 457, ~_t68 ] % 0.37/0.61 (1,1) [48,8]. _t16 => box 1 _t18 [ SNF ] [ SNF++, 356, _t18 ] % 0.37/0.61 (440,1) [230,8]. _t70 => ~box 1~ _t72 [ SNF ] [ SNF++, 388, _t72 ] % 0.37/0.61 (1,1) [356,8]. _t16 => box 1 _t98 [ SNF++, 48 ] % 0.37/0.61 (440,1) [388,8]. _t70 => ~box 1~ _t99 [ SNF++, 230 ] % 0.37/0.61 (1,1) [391,8]. true => ~_t100 | _t16 [ SNF++, 61 ] % 0.37/0.61 (441,1) [423,8]. true => ~_t101 | _t70 [ SNF++, 231 ] % 0.37/0.61 (440,1) [1361,8]. true => ~_t70 | ~_t16 [ GEN1, 356, 388, 1359, _t98, _t99 ] % 0.37/0.61 (440,1) [1362,8]. true => ~_t100 | ~_t70 [ LRES, 1361, 391, ~_t16 ] % 0.37/0.61 (441,1) [1363,8]. true => ~_t101 | ~_t100 [ LRES, 1362, 423, ~_t70 ] % 0.37/0.61 (1,1) [35,9]. _t18 => box 1 _t20 [ SNF ] [ SNF++, 322, _t20 ] % 0.37/0.61 (436,1) [226,9]. _t72 => ~box 1~ _t74 [ SNF ] [ SNF++, 352, _t74 ] % 0.37/0.61 (1,1) [322,9]. _t18 => box 1 _t92 [ SNF++, 35 ] % 0.37/0.61 (436,1) [352,9]. _t72 => ~box 1~ _t96 [ SNF++, 226 ] % 0.37/0.61 (1,1) [357,9]. true => ~_t98 | _t18 [ SNF++, 48 ] % 0.37/0.61 (440,1) [389,9]. true => ~_t99 | _t72 [ SNF++, 230 ] % 0.37/0.61 (436,1) [1357,9]. true => ~_t72 | ~_t18 [ GEN1, 322, 352, 1356, _t92, _t96 ] % 0.37/0.61 (436,1) [1358,9]. true => ~_t98 | ~_t72 [ LRES, 1357, 357, ~_t18 ] % 0.37/0.61 (440,1) [1359,9]. true => ~_t99 | ~_t98 [ LRES, 1358, 389, ~_t72 ] % 0.37/0.61 (1,1) [5,10]. _t20 => box 1 _t22 [ SNF ] [ SNF++, 282, _t22 ] % 0.37/0.61 (1,1) [14,10]. _t20 => box 1 _t26 [ SNF ] [ SNF++, 284, _t26 ] % 0.37/0.61 (1,1) [20,10]. _t20 => box 1 _t31 [ SNF ] [ SNF++, 286, _t31 ] % 0.37/0.61 (1,1) [25,10]. _t35 => box 1 _t21 [ SNF ] [ SNF++, 288, _t21 ] % 0.37/0.61 (26,1) [27,10]. _t27 => ~box 1~ _t28 [ SNF ] [ SNF++, 304, _t28 ] % 0.37/0.61 (1,1) [28,10]. true => _t35 | ~_t34 | _t27 [ SNF ] % 0.37/0.61 (1,1) [29,10]. true => _t34 | ~_t20 [ SNF ] % 0.37/0.61 (33,1) [32,10]. _t22 => ~box 1~ _t23 [ SNF ] [ SNF++, 306, _t23 ] % 0.37/0.61 (1,1) [33,10]. true => ~_t36 | _t27 | _t22 [ SNF ] % 0.37/0.61 (1,1) [34,10]. true => _t36 | ~_t20 [ SNF ] % 0.37/0.61 (1,1) [225,10]. _t74 => box 1 _t75 [ SNF ] [ SNF++, 302, _t75 ] % 0.37/0.61 (1,1) [282,10]. _t20 => box 1 _t80 [ SNF++, 5 ] % 0.37/0.61 (1,1) [284,10]. _t20 => box 1 _t86 [ SNF++, 14 ] % 0.37/0.61 (1,1) [286,10]. _t20 => box 1 _t87 [ SNF++, 20 ] % 0.37/0.61 (1,1) [288,10]. _t35 => box 1 _t81 [ SNF++, 25 ] % 0.37/0.61 (1,1) [302,10]. _t74 => box 1 _t91 [ SNF++, 225 ] % 0.37/0.61 (26,1) [304,10]. _t27 => ~box 1~ _t77 [ SNF++, 27 ] % 0.37/0.61 (33,1) [306,10]. _t22 => ~box 1~ _t78 [ SNF++, 32 ] % 0.37/0.61 (1,1) [323,10]. true => ~_t92 | _t20 [ SNF++, 35 ] % 0.37/0.61 (436,1) [353,10]. true => ~_t96 | _t74 [ SNF++, 226 ] % 0.37/0.61 (1,1) [638,10]. true => ~_t92 | _t36 [ LRES, 34, 323, ~_t20 ] % 0.37/0.61 (1,1) [661,10]. true => ~_t92 | _t34 [ LRES, 29, 323, ~_t20 ] % 0.37/0.61 (26,1) [869,10]. true => ~_t27 | ~_t20 [ GEN1, 282, 304, 799, _t80, _t77 ] % 0.37/0.61 (26,1) [930,10]. true => ~_t92 | ~_t27 [ LRES, 869, 323, ~_t20 ] % 0.37/0.61 (26,1) [946,10]. true => ~_t92 | _t35 | ~_t34 [ LRES, 930, 28, ~_t27 ] [ Backward Subsumption, 1052 ] % 0.37/0.61 (26,1) [1052,10]. true => ~_t92 | _t35 [ LRES, 946, 661, ~_t34 ] % 0.37/0.61 (33,1) [1261,10]. true => ~_t74 | ~_t35 | ~_t22 | ~_t20 [ GEN1, 302, 284, 288, 286, 306, 1247, _t91, _t86, _t81, _t87, _t78 ] % 0.37/0.61 (33,1) [1277,10]. true => ~_t92 | ~_t74 | ~_t35 | ~_t22 [ LRES, 1261, 323, ~_t20 ] [ Backward Subsumption, 1355 ] % 0.37/0.61 (33,1) [1330,10]. true => ~_t92 | ~_t74 | ~_t36 | ~_t35 | _t27 [ LRES, 1277, 33, ~_t22 ] [ Backward Subsumption, 1350 ] % 0.37/0.61 (33,1) [1350,10]. true => ~_t92 | ~_t74 | ~_t36 | ~_t35 [ LRES, 1330, 930, _t27 ] [ Backward Subsumption, 1354 ] % 0.37/0.61 (33,1) [1354,10]. true => ~_t92 | ~_t74 | ~_t36 [ LRES, 1350, 1052, ~_t35 ] [ Backward Subsumption, 1355 ] % 0.37/0.61 (33,1) [1355,10]. true => ~_t92 | ~_t74 [ LRES, 1354, 638, ~_t36 ] % 0.37/0.61 (436,1) [1356,10]. true => ~_t96 | ~_t92 [ LRES, 1355, 353, ~_t74 ] % 0.37/0.61 (6,1) [4,11]. _t22 => ~box 1~ _t23 [ SNF ] [ SNF++, 258, _t23 ] % 0.37/0.61 (8,1) [7,11]. _t27 => ~box 1~ _t28 [ SNF ] [ SNF++, 260, _t28 ] % 0.37/0.61 (15,1) [12,11]. _t29 => ~box 1~ _t21 [ SNF ] [ SNF++, 262, _t21 ] % 0.37/0.61 (1,1) [13,11]. true => _t29 | _t27 | ~_t26 [ SNF ] % 0.37/0.61 (1,1) [17,11]. _t32 => box 1 _t27 [ SNF ] [ SNF++, 268, _t27 ] % 0.37/0.61 (1,1) [18,11]. _t33 => box 1 _t23 [ SNF ] [ SNF++, 270, _t23 ] % 0.37/0.61 (1,1) [19,11]. true => _t33 | _t32 | ~_t31 | ~p0 [ SNF ] % 0.37/0.61 (1,1) [24,11]. _t21 => box 1 _t22 [ SNF ] [ SNF++, 272, _t22 ] % 0.37/0.61 (1,1) [26,11]. _t28 => box 1 ~p0 [ SNF ] [ SNF++, 274, ~p0 ] % 0.37/0.61 (33,1) [30,11]. true => ~_t23 | p0 [ SNF ] % 0.37/0.61 (435,1) [224,11]. _t75 => ~box 1~ ~p0 [ SNF ] [ SNF++, 266, ~p0 ] % 0.37/0.61 (6,1) [258,11]. _t22 => ~box 1~ _t78 [ SNF++, 4 ] % 0.37/0.61 (8,1) [260,11]. _t27 => ~box 1~ _t77 [ SNF++, 7 ] % 0.37/0.61 (15,1) [262,11]. _t29 => ~box 1~ _t81 [ SNF++, 12 ] % 0.37/0.61 (435,1) [266,11]. _t75 => ~box 1~ _t79 [ SNF++, 224 ] % 0.37/0.61 (1,1) [268,11]. _t32 => box 1 _t83 [ SNF++, 17 ] % 0.37/0.61 (1,1) [270,11]. _t33 => box 1 _t78 [ SNF++, 18 ] % 0.37/0.61 (1,1) [272,11]. _t21 => box 1 _t80 [ SNF++, 24 ] % 0.37/0.61 (1,1) [274,11]. _t28 => box 1 _t79 [ SNF++, 26 ] % 0.37/0.61 (1,1) [283,11]. true => ~_t80 | _t22 [ SNF++, 5 ] % 0.37/0.61 (1,1) [285,11]. true => ~_t86 | _t26 [ SNF++, 14 ] % 0.37/0.61 (1,1) [287,11]. true => ~_t87 | _t31 [ SNF++, 20 ] % 0.37/0.61 (1,1) [289,11]. true => ~_t81 | _t21 [ SNF++, 25 ] % 0.37/0.61 (1,1) [303,11]. true => ~_t91 | _t75 [ SNF++, 225 ] % 0.37/0.61 (26,1) [305,11]. true => ~_t77 | _t28 [ SNF++, 27 ] % 0.37/0.61 (33,1) [307,11]. true => ~_t78 | _t23 [ SNF++, 32 ] % 0.37/0.61 (1,1) [735,11]. true => ~_t86 | _t29 | _t27 [ LRES, 13, 285, ~_t26 ] % 0.37/0.61 (6,1) [775,11]. true => ~_t28 | ~_t22 [ GEN1, 274, 258, 733, _t79, _t78 ] % 0.37/0.61 (435,1) [776,11]. true => ~_t75 | ~_t33 [ GEN1, 270, 266, 733, _t78, _t79 ] % 0.37/0.61 (6,1) [789,11]. true => ~_t80 | ~_t28 [ LRES, 775, 283, ~_t22 ] % 0.37/0.61 (26,1) [799,11]. true => ~_t80 | ~_t77 [ LRES, 789, 305, ~_t28 ] % 0.37/0.61 (8,1) [853,11]. true => ~_t27 | ~_t21 [ GEN1, 272, 260, 798, _t80, _t77 ] % 0.37/0.61 (15,1) [890,11]. true => ~_t32 | ~_t29 [ GEN1, 268, 262, 868, _t83, _t81 ] % 0.37/0.61 (8,1) [902,11]. true => ~_t81 | ~_t27 [ LRES, 853, 289, ~_t21 ] % 0.37/0.61 (8,1) [914,11]. true => ~_t86 | ~_t81 | _t29 [ LRES, 735, 902, _t27 ] % 0.37/0.61 (15,1) [1011,11]. true => ~_t86 | ~_t81 | ~_t32 [ LRES, 914, 890, _t29 ] % 0.37/0.61 (33,1) [1145,11]. true => _t33 | _t32 | ~_t31 | ~_t23 [ LRES, 19, 30, ~p0 ] % 0.37/0.61 (33,1) [1217,11]. true => ~_t78 | _t33 | _t32 | ~_t31 [ LRES, 1145, 307, ~_t23 ] % 0.37/0.61 (33,1) [1235,11]. true => ~_t87 | ~_t78 | _t33 | _t32 [ LRES, 1217, 287, ~_t31 ] % 0.37/0.61 (33,1) [1239,11]. true => ~_t87 | ~_t86 | ~_t81 | ~_t78 | _t33 [ LRES, 1235, 1011, _t32 ] % 0.37/0.61 (435,1) [1242,11]. true => ~_t87 | ~_t86 | ~_t81 | ~_t78 | ~_t75 [ LRES, 1239, 776, _t33 ] % 0.37/0.61 (435,1) [1247,11]. true => ~_t91 | ~_t87 | ~_t86 | ~_t81 | ~_t78 [ LRES, 1242, 303, ~_t75 ] % 0.37/0.61 (6,1) [2,12]. true => ~_t23 | p0 [ SNF ] % 0.37/0.61 (1,1) [6,12]. _t28 => box 1 ~p0 [ SNF ] [ SNF++, 254, ~p0 ] % 0.37/0.61 (1,1) [11,12]. _t21 => box 1 _t22 [ SNF ] [ SNF++, 256, _t22 ] % 0.37/0.61 (17,1) [16,12]. _t27 => ~box 1~ _t28 [ SNF ] [ SNF++, 250, _t28 ] % 0.37/0.61 (24,1) [23,12]. _t22 => ~box 1~ _t23 [ SNF ] [ SNF++, 252, _t23 ] % 0.37/0.61 (17,1) [250,12]. _t27 => ~box 1~ _t77 [ SNF++, 16 ] % 0.37/0.61 (24,1) [252,12]. _t22 => ~box 1~ _t78 [ SNF++, 23 ] % 0.37/0.61 (1,1) [254,12]. _t28 => box 1 _t79 [ SNF++, 6 ] % 0.37/0.61 (1,1) [256,12]. _t21 => box 1 _t80 [ SNF++, 11 ] % 0.37/0.61 (6,1) [259,12]. true => ~_t78 | _t23 [ SNF++, 4 ] % 0.37/0.61 (8,1) [261,12]. true => ~_t77 | _t28 [ SNF++, 7 ] % 0.37/0.61 (15,1) [263,12]. true => ~_t81 | _t21 [ SNF++, 12 ] % 0.37/0.61 (435,1) [267,12]. true => ~_t79 | ~p0 [ SNF++, 224 ] % 0.37/0.61 (1,1) [269,12]. true => ~_t83 | _t27 [ SNF++, 17 ] % 0.37/0.61 (1,1) [273,12]. true => ~_t80 | _t22 [ SNF++, 24 ] % 0.37/0.61 (435,1) [634,12]. true => ~_t79 | ~_t23 [ LRES, 267, 2, ~p0 ] % 0.37/0.61 (435,1) [733,12]. true => ~_t79 | ~_t78 [ LRES, 634, 259, ~_t23 ] % 0.37/0.61 (24,1) [736,12]. true => ~_t28 | ~_t22 [ GEN1, 254, 252, 660, _t79, _t78 ] % 0.37/0.61 (24,1) [788,12]. true => ~_t80 | ~_t28 [ LRES, 736, 273, ~_t22 ] % 0.37/0.61 (17,1) [790,12]. true => ~_t27 | ~_t21 [ GEN1, 256, 250, 778, _t80, _t77 ] % 0.37/0.61 (24,1) [798,12]. true => ~_t80 | ~_t77 [ LRES, 788, 261, ~_t28 ] % 0.37/0.61 (17,1) [850,12]. true => ~_t81 | ~_t27 [ LRES, 790, 263, ~_t21 ] % 0.37/0.61 (17,1) [868,12]. true => ~_t83 | ~_t81 [ LRES, 850, 269, ~_t27 ] % 0.37/0.61 (14,1) [10,13]. _t22 => ~box 1~ _t23 [ SNF ] [ SNF++, 318, _t23 ] % 0.37/0.61 (1,1) [15,13]. _t28 => box 1 ~p0 [ SNF ] [ SNF++, 320, ~p0 ] % 0.37/0.61 (24,1) [21,13]. true => ~_t23 | p0 [ SNF ] % 0.37/0.61 (17,1) [251,13]. true => ~_t77 | _t28 [ SNF++, 16 ] % 0.37/0.61 (24,1) [253,13]. true => ~_t78 | _t23 [ SNF++, 23 ] % 0.37/0.61 (1,1) [255,13]. true => ~_t79 | ~p0 [ SNF++, 6 ] % 0.37/0.61 (1,1) [257,13]. true => ~_t80 | _t22 [ SNF++, 11 ] % 0.37/0.61 (14,1) [318,13]. _t22 => ~box 1~ _t78 [ SNF++, 10 ] % 0.37/0.61 (1,1) [320,13]. _t28 => box 1 _t79 [ SNF++, 15 ] % 0.37/0.61 (24,1) [637,13]. true => ~_t79 | ~_t23 [ LRES, 255, 21, ~p0 ] % 0.37/0.61 (24,1) [660,13]. true => ~_t79 | ~_t78 [ LRES, 637, 253, ~_t23 ] % 0.37/0.61 (14,1) [734,13]. true => ~_t28 | ~_t22 [ GEN1, 320, 318, 649, _t79, _t78 ] % 0.37/0.61 (14,1) [760,13]. true => ~_t80 | ~_t28 [ LRES, 734, 257, ~_t22 ] % 0.37/0.61 (17,1) [778,13]. true => ~_t80 | ~_t77 [ LRES, 760, 251, ~_t28 ] % 0.37/0.61 (14,1) [8,14]. true => ~_t23 | p0 [ SNF ] % 0.37/0.61 (14,1) [319,14]. true => ~_t78 | _t23 [ SNF++, 10 ] % 0.37/0.61 (1,1) [321,14]. true => ~_t79 | ~p0 [ SNF++, 15 ] % 0.37/0.61 (14,1) [635,14]. true => ~_t79 | ~_t23 [ LRES, 321, 8, ~p0 ] % 0.37/0.61 (14,1) [649,14]. true => ~_t79 | ~_t78 [ LRES, 635, 319, ~_t23 ] % 0.37/0.61 % SZS output end Refutation % 0.37/0.61 % KSP exiting %------------------------------------------------------------------------------