%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP097_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n022.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:59 PM UTC 2026 % Result : Theorem 0.49s 0.63s % Output : Refutation 0.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP097_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.16/0.33 % Computer : n022.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Mon May 4 17:32:20 EDT 2026 % 0.16/0.33 % CPUTime : % 0.38/0.60 ----KSP format--- % 0.38/0.60 set(box,SER). % 0.38/0.60 usable(formulas). % 0.38/0.60 true. % 0.38/0.60 end_of_list. % 0.38/0.60 sos(formulas). % 0.38/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.38/0.60 end_of_list. % 0.38/0.60 ----------------- % 0.38/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/sandbox/tmp/tmp.BUht4i8k92/theBenchmark.ksp % 0.49/0.63 % 0.49/0.63 % SZS status Theorem % 0.49/0.63 % 0.49/0.63 ***************** % 0.49/0.63 FOUND PROOF 1 % 0.49/0.63 ***************** % 0.49/0.63 % SZS output start Refutation % 0.49/0.63 % 0.49/0.63 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.49/0.63 (1,1) [271,0]. _t1 => box 1 _t2 [ SNF ] [ Backward Subsumption, 438 ] % 0.49/0.63 (1,1) [273,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 436 ] % 0.49/0.63 (449,1) [428,0]. _t55 => ~box 1~ _t56 [ SNF ] [ Backward Subsumption, 442 ] % 0.49/0.63 (1,1) [429,0]. true => _t55 | ~_t0 [ SNF ] [ Backward Subsumption, 431 ] % 0.49/0.63 (1,1) [431,0]. true => _t55 [ Unit Resolution, 3, 429, _t0 ] [ Modal Level Pure Literal Elimination, _t55 ] % 0.49/0.63 (1,1) [436,0]. true => _t1 [ Unit Resolution, 3, 273, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 0.49/0.63 (1,1) [438,0]. true => box 1 _t2 [ LHS Unit Resolution, 436, 271, _t1 ] [ SNF++, 1015, _t2 ] % 0.49/0.63 (449,1) [442,0]. true => ~box 1~ _t56 [ LHS Unit Resolution, 431, 428, _t55 ] [ SNF++, 1033, _t56 ] % 0.49/0.63 (1,1) [1015,0]. true => box 1 _t134 [ SNF++, 438 ] % 0.49/0.63 (449,1) [1033,0]. true => ~box 1~ _t135 [ SNF++, 442 ] % 0.49/0.63 (449,1) [2279,0]. true => false [ GEN1, 1015, 1033, 2276, _t134, _t135 ] % 0.49/0.63 (1,1) [247,1]. _t3 => box 1 _t4 [ SNF ] [ SNF++, 975, _t4 ] % 0.49/0.63 (1,1) [249,1]. true => _t3 | ~_t2 [ SNF ] % 0.49/0.63 (447,1) [426,1]. _t57 => ~box 1~ _t58 [ SNF ] [ SNF++, 1013, _t58 ] % 0.49/0.63 (449,1) [427,1]. true => _t57 | ~_t56 [ SNF ] % 0.49/0.63 (1,1) [975,1]. _t3 => box 1 _t132 [ SNF++, 247 ] % 0.49/0.63 (447,1) [1013,1]. _t57 => ~box 1~ _t133 [ SNF++, 426 ] % 0.49/0.63 (1,1) [1016,1]. true => ~_t134 | _t2 [ SNF++, 438 ] % 0.49/0.63 (449,1) [1034,1]. true => ~_t135 | _t56 [ SNF++, 442 ] % 0.49/0.63 (1,1) [1073,1]. true => ~_t134 | _t3 [ LRES, 249, 1016, ~_t2 ] % 0.49/0.63 (449,1) [1120,1]. true => ~_t135 | _t57 [ LRES, 427, 1034, ~_t56 ] % 0.49/0.63 (447,1) [2269,1]. true => ~_t57 | ~_t3 [ GEN1, 975, 1013, 2264, _t132, _t133 ] % 0.49/0.63 (447,1) [2274,1]. true => ~_t134 | ~_t57 [ LRES, 2269, 1073, ~_t3 ] % 0.49/0.63 (449,1) [2276,1]. true => ~_t135 | ~_t134 [ LRES, 2274, 1120, ~_t57 ] % 0.49/0.63 (1,1) [223,2]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 923, _t6 ] % 0.49/0.63 (1,1) [225,2]. true => _t5 | ~_t4 [ SNF ] % 0.49/0.63 (446,1) [424,2]. _t59 => ~box 1~ _t60 [ SNF ] [ SNF++, 973, _t60 ] % 0.49/0.63 (447,1) [425,2]. true => _t59 | ~_t58 [ SNF ] % 0.49/0.63 (1,1) [923,2]. _t5 => box 1 _t130 [ SNF++, 223 ] % 0.49/0.63 (446,1) [973,2]. _t59 => ~box 1~ _t131 [ SNF++, 424 ] % 0.49/0.63 (1,1) [976,2]. true => ~_t132 | _t4 [ SNF++, 247 ] % 0.49/0.63 (447,1) [1014,2]. true => ~_t133 | _t58 [ SNF++, 426 ] % 0.49/0.63 (1,1) [1072,2]. true => ~_t132 | _t5 [ LRES, 225, 976, ~_t4 ] % 0.49/0.63 (447,1) [1119,2]. true => ~_t133 | _t59 [ LRES, 425, 1014, ~_t58 ] % 0.49/0.63 (446,1) [2258,2]. true => ~_t59 | ~_t5 [ GEN1, 923, 973, 2253, _t130, _t131 ] % 0.49/0.63 (446,1) [2259,2]. true => ~_t132 | ~_t59 [ LRES, 2258, 1072, ~_t5 ] % 0.49/0.63 (447,1) [2264,2]. true => ~_t133 | ~_t132 [ LRES, 2259, 1119, ~_t59 ] % 0.49/0.63 (1,1) [199,3]. _t7 => box 1 _t8 [ SNF ] [ SNF++, 871, _t8 ] % 0.49/0.63 (1,1) [201,3]. true => _t7 | ~_t6 [ SNF ] % 0.49/0.63 (445,1) [422,3]. _t61 => ~box 1~ _t62 [ SNF ] [ SNF++, 921, _t62 ] % 0.49/0.63 (446,1) [423,3]. true => _t61 | ~_t60 [ SNF ] % 0.49/0.63 (1,1) [871,3]. _t7 => box 1 _t128 [ SNF++, 199 ] % 0.49/0.63 (445,1) [921,3]. _t61 => ~box 1~ _t129 [ SNF++, 422 ] % 0.49/0.63 (1,1) [924,3]. true => ~_t130 | _t6 [ SNF++, 223 ] % 0.49/0.63 (446,1) [974,3]. true => ~_t131 | _t60 [ SNF++, 424 ] % 0.49/0.63 (1,1) [1071,3]. true => ~_t130 | _t7 [ LRES, 201, 924, ~_t6 ] % 0.49/0.63 (446,1) [1118,3]. true => ~_t131 | _t61 [ LRES, 423, 974, ~_t60 ] % 0.49/0.63 (445,1) [2246,3]. true => ~_t61 | ~_t7 [ GEN1, 871, 921, 2240, _t128, _t129 ] % 0.49/0.63 (445,1) [2247,3]. true => ~_t130 | ~_t61 [ LRES, 2246, 1071, ~_t7 ] % 0.49/0.63 (446,1) [2253,3]. true => ~_t131 | ~_t130 [ LRES, 2247, 1118, ~_t61 ] % 0.49/0.63 (1,1) [175,4]. _t9 => box 1 _t10 [ SNF ] [ SNF++, 819, _t10 ] % 0.49/0.63 (1,1) [177,4]. true => _t9 | ~_t8 [ SNF ] % 0.49/0.63 (444,1) [420,4]. _t63 => ~box 1~ _t64 [ SNF ] [ SNF++, 869, _t64 ] % 0.49/0.63 (445,1) [421,4]. true => _t63 | ~_t62 [ SNF ] % 0.49/0.63 (1,1) [819,4]. _t9 => box 1 _t126 [ SNF++, 175 ] % 0.49/0.63 (444,1) [869,4]. _t63 => ~box 1~ _t127 [ SNF++, 420 ] % 0.49/0.63 (1,1) [872,4]. true => ~_t128 | _t8 [ SNF++, 199 ] % 0.49/0.63 (445,1) [922,4]. true => ~_t129 | _t62 [ SNF++, 422 ] % 0.49/0.63 (1,1) [1070,4]. true => ~_t128 | _t9 [ LRES, 177, 872, ~_t8 ] % 0.49/0.63 (445,1) [1117,4]. true => ~_t129 | _t63 [ LRES, 421, 922, ~_t62 ] % 0.49/0.63 (444,1) [2237,4]. true => ~_t63 | ~_t9 [ GEN1, 819, 869, 2228, _t126, _t127 ] % 0.49/0.63 (444,1) [2238,4]. true => ~_t128 | ~_t63 [ LRES, 2237, 1070, ~_t9 ] % 0.49/0.63 (445,1) [2240,4]. true => ~_t129 | ~_t128 [ LRES, 2238, 1117, ~_t63 ] % 0.49/0.63 (1,1) [151,5]. _t11 => box 1 _t12 [ SNF ] [ SNF++, 767, _t12 ] % 0.49/0.63 (1,1) [153,5]. true => _t11 | ~_t10 [ SNF ] % 0.49/0.63 (443,1) [418,5]. _t65 => ~box 1~ _t66 [ SNF ] [ SNF++, 817, _t66 ] % 0.49/0.63 (444,1) [419,5]. true => _t65 | ~_t64 [ SNF ] % 0.49/0.63 (1,1) [767,5]. _t11 => box 1 _t124 [ SNF++, 151 ] % 0.49/0.63 (443,1) [817,5]. _t65 => ~box 1~ _t125 [ SNF++, 418 ] % 0.49/0.63 (1,1) [820,5]. true => ~_t126 | _t10 [ SNF++, 175 ] % 0.49/0.63 (444,1) [870,5]. true => ~_t127 | _t64 [ SNF++, 420 ] % 0.49/0.63 (1,1) [1069,5]. true => ~_t126 | _t11 [ LRES, 153, 820, ~_t10 ] % 0.49/0.63 (444,1) [1116,5]. true => ~_t127 | _t65 [ LRES, 419, 870, ~_t64 ] % 0.49/0.63 (443,1) [2223,5]. true => ~_t65 | ~_t11 [ GEN1, 767, 817, 2215, _t124, _t125 ] % 0.49/0.63 (443,1) [2224,5]. true => ~_t126 | ~_t65 [ LRES, 2223, 1069, ~_t11 ] % 0.49/0.63 (444,1) [2228,5]. true => ~_t127 | ~_t126 [ LRES, 2224, 1116, ~_t65 ] % 0.49/0.63 (1,1) [127,6]. _t13 => box 1 _t14 [ SNF ] [ SNF++, 715, _t14 ] % 0.49/0.63 (1,1) [129,6]. true => _t13 | ~_t12 [ SNF ] % 0.49/0.63 (442,1) [416,6]. _t67 => ~box 1~ _t68 [ SNF ] [ SNF++, 765, _t68 ] % 0.49/0.63 (443,1) [417,6]. true => _t67 | ~_t66 [ SNF ] % 0.49/0.63 (1,1) [715,6]. _t13 => box 1 _t122 [ SNF++, 127 ] % 0.49/0.63 (442,1) [765,6]. _t67 => ~box 1~ _t123 [ SNF++, 416 ] % 0.49/0.63 (1,1) [768,6]. true => ~_t124 | _t12 [ SNF++, 151 ] % 0.49/0.63 (443,1) [818,6]. true => ~_t125 | _t66 [ SNF++, 418 ] % 0.49/0.63 (1,1) [1068,6]. true => ~_t124 | _t13 [ LRES, 129, 768, ~_t12 ] % 0.49/0.63 (443,1) [1115,6]. true => ~_t125 | _t67 [ LRES, 417, 818, ~_t66 ] % 0.49/0.63 (442,1) [2212,6]. true => ~_t67 | ~_t13 [ GEN1, 715, 765, 2209, _t122, _t123 ] % 0.49/0.63 (442,1) [2213,6]. true => ~_t124 | ~_t67 [ LRES, 2212, 1068, ~_t13 ] % 0.49/0.63 (443,1) [2215,6]. true => ~_t125 | ~_t124 [ LRES, 2213, 1115, ~_t67 ] % 0.49/0.63 (1,1) [103,7]. _t15 => box 1 _t16 [ SNF ] [ SNF++, 663, _t16 ] % 0.49/0.63 (1,1) [105,7]. true => _t15 | ~_t14 [ SNF ] % 0.49/0.63 (441,1) [414,7]. _t69 => ~box 1~ _t70 [ SNF ] [ SNF++, 713, _t70 ] % 0.49/0.63 (442,1) [415,7]. true => _t69 | ~_t68 [ SNF ] % 0.49/0.63 (1,1) [663,7]. _t15 => box 1 _t120 [ SNF++, 103 ] % 0.49/0.63 (441,1) [713,7]. _t69 => ~box 1~ _t121 [ SNF++, 414 ] % 0.49/0.63 (1,1) [716,7]. true => ~_t122 | _t14 [ SNF++, 127 ] % 0.49/0.63 (442,1) [766,7]. true => ~_t123 | _t68 [ SNF++, 416 ] % 0.49/0.63 (1,1) [1067,7]. true => ~_t122 | _t15 [ LRES, 105, 716, ~_t14 ] % 0.49/0.63 (442,1) [1114,7]. true => ~_t123 | _t69 [ LRES, 415, 766, ~_t68 ] % 0.49/0.63 (441,1) [2207,7]. true => ~_t69 | ~_t15 [ GEN1, 663, 713, 2206, _t120, _t121 ] % 0.49/0.63 (441,1) [2208,7]. true => ~_t122 | ~_t69 [ LRES, 2207, 1067, ~_t15 ] % 0.49/0.63 (442,1) [2209,7]. true => ~_t123 | ~_t122 [ LRES, 2208, 1114, ~_t69 ] % 0.49/0.63 (1,1) [79,8]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 611, _t18 ] % 0.49/0.63 (1,1) [81,8]. true => _t17 | ~_t16 [ SNF ] % 0.49/0.63 (440,1) [412,8]. _t71 => ~box 1~ _t72 [ SNF ] [ SNF++, 661, _t72 ] % 0.49/0.63 (441,1) [413,8]. true => _t71 | ~_t70 [ SNF ] % 0.49/0.63 (1,1) [611,8]. _t17 => box 1 _t118 [ SNF++, 79 ] % 0.49/0.63 (440,1) [661,8]. _t71 => ~box 1~ _t119 [ SNF++, 412 ] % 0.49/0.63 (1,1) [664,8]. true => ~_t120 | _t16 [ SNF++, 103 ] % 0.49/0.63 (441,1) [714,8]. true => ~_t121 | _t70 [ SNF++, 414 ] % 0.49/0.63 (1,1) [1066,8]. true => ~_t120 | _t17 [ LRES, 81, 664, ~_t16 ] % 0.49/0.63 (441,1) [1113,8]. true => ~_t121 | _t71 [ LRES, 413, 714, ~_t70 ] % 0.49/0.63 (440,1) [2204,8]. true => ~_t71 | ~_t17 [ GEN1, 611, 661, 2203, _t118, _t119 ] % 0.49/0.63 (440,1) [2205,8]. true => ~_t120 | ~_t71 [ LRES, 2204, 1066, ~_t17 ] % 0.49/0.63 (441,1) [2206,8]. true => ~_t121 | ~_t120 [ LRES, 2205, 1113, ~_t71 ] % 0.49/0.63 (1,1) [55,9]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 559, _t20 ] % 0.49/0.63 (1,1) [57,9]. true => _t19 | ~_t18 [ SNF ] % 0.49/0.63 (436,1) [405,9]. _t73 => ~box 1~ _t74 [ SNF ] [ SNF++, 607, _t74 ] % 0.49/0.63 (440,1) [406,9]. true => _t73 | ~_t72 [ SNF ] % 0.49/0.63 (1,1) [559,9]. _t19 => box 1 _t112 [ SNF++, 55 ] % 0.49/0.63 (436,1) [607,9]. _t73 => ~box 1~ _t116 [ SNF++, 405 ] % 0.49/0.63 (1,1) [612,9]. true => ~_t118 | _t18 [ SNF++, 79 ] % 0.49/0.63 (440,1) [662,9]. true => ~_t119 | _t72 [ SNF++, 412 ] % 0.49/0.63 (1,1) [1065,9]. true => ~_t118 | _t19 [ LRES, 57, 612, ~_t18 ] % 0.49/0.63 (440,1) [1112,9]. true => ~_t119 | _t73 [ LRES, 406, 662, ~_t72 ] % 0.49/0.63 (436,1) [2200,9]. true => ~_t73 | ~_t19 [ GEN1, 559, 607, 2197, _t112, _t116 ] % 0.49/0.63 (436,1) [2201,9]. true => ~_t118 | ~_t73 [ LRES, 2200, 1065, ~_t19 ] % 0.49/0.63 (440,1) [2203,9]. true => ~_t119 | ~_t118 [ LRES, 2201, 1112, ~_t73 ] % 0.49/0.63 (1,1) [8,10]. _t21 => box 1 _t22 [ SNF ] [ SNF++, 497, _t22 ] % 0.49/0.63 (1,1) [10,10]. true => _t21 | ~_t20 [ SNF ] % 0.49/0.63 (1,1) [22,10]. _t25 => box 1 _t26 [ SNF ] [ SNF++, 499, _t26 ] % 0.49/0.63 (1,1) [24,10]. true => _t25 | ~_t20 [ SNF ] % 0.49/0.63 (1,1) [33,10]. _t30 => box 1 _t31 [ SNF ] [ SNF++, 501, _t31 ] % 0.49/0.63 (1,1) [35,10]. true => _t30 | ~_t20 [ SNF ] % 0.49/0.63 (1,1) [42,10]. _t35 => box 1 _t21 [ SNF ] [ SNF++, 503, _t21 ] % 0.49/0.63 (26,1) [46,10]. _t27 => ~box 1~ _t28 [ SNF ] [ SNF++, 527, _t28 ] % 0.49/0.63 (1,1) [47,10]. true => _t35 | ~_t34 | _t27 [ SNF ] % 0.49/0.63 (1,1) [48,10]. true => _t34 | ~_t20 [ SNF ] % 0.49/0.63 (33,1) [52,10]. _t22 => ~box 1~ _t23 [ SNF ] [ SNF++, 529, _t23 ] % 0.49/0.63 (1,1) [53,10]. true => ~_t36 | _t27 | _t22 [ SNF ] % 0.49/0.63 (1,1) [54,10]. true => _t36 | ~_t20 [ SNF ] % 0.49/0.63 (1,1) [403,10]. _t74 => box 1 _t75 [ SNF ] [ SNF++, 517, _t75 ] % 0.49/0.63 (1,1) [497,10]. _t21 => box 1 _t98 [ SNF++, 8 ] % 0.49/0.63 (1,1) [499,10]. _t25 => box 1 _t106 [ SNF++, 22 ] % 0.49/0.63 (1,1) [501,10]. _t30 => box 1 _t107 [ SNF++, 33 ] % 0.49/0.63 (1,1) [503,10]. _t35 => box 1 _t101 [ SNF++, 42 ] % 0.49/0.63 (1,1) [517,10]. _t74 => box 1 _t111 [ SNF++, 403 ] % 0.49/0.63 (26,1) [527,10]. _t27 => ~box 1~ _t99 [ SNF++, 46 ] % 0.49/0.63 (33,1) [529,10]. _t22 => ~box 1~ _t100 [ SNF++, 52 ] % 0.49/0.63 (1,1) [560,10]. true => ~_t112 | _t20 [ SNF++, 55 ] % 0.49/0.63 (436,1) [608,10]. true => ~_t116 | _t74 [ SNF++, 405 ] % 0.49/0.63 (1,1) [1036,10]. true => ~_t112 | _t36 [ LRES, 54, 560, ~_t20 ] % 0.49/0.63 (1,1) [1050,10]. true => ~_t112 | _t34 [ LRES, 48, 560, ~_t20 ] % 0.49/0.63 (1,1) [1064,10]. true => ~_t112 | _t30 [ LRES, 35, 560, ~_t20 ] % 0.49/0.63 (1,1) [1074,10]. true => ~_t112 | _t25 [ LRES, 24, 560, ~_t20 ] % 0.49/0.63 (1,1) [1108,10]. true => ~_t112 | _t21 [ LRES, 10, 560, ~_t20 ] % 0.49/0.63 (26,1) [1472,10]. true => ~_t27 | ~_t21 [ GEN1, 497, 527, 1356, _t98, _t99 ] % 0.49/0.63 (26,1) [1568,10]. true => ~_t112 | ~_t27 [ LRES, 1472, 1108, ~_t21 ] % 0.49/0.63 (26,1) [1630,10]. true => ~_t112 | _t35 | ~_t34 [ LRES, 1568, 47, ~_t27 ] [ Backward Subsumption, 1905 ] % 0.49/0.63 (33,1) [1856,10]. true => ~_t74 | ~_t35 | ~_t30 | ~_t25 | ~_t22 [ GEN1, 517, 499, 503, 501, 529, 1852, _t111, _t106, _t101, _t107, _t100 ] % 0.49/0.63 (26,1) [1905,10]. true => ~_t112 | _t35 [ LRES, 1630, 1050, ~_t34 ] % 0.49/0.63 (33,1) [2156,10]. true => ~_t74 | ~_t36 | ~_t35 | ~_t30 | _t27 | ~_t25 [ LRES, 1856, 53, ~_t22 ] % 0.49/0.63 (33,1) [2163,10]. true => ~_t112 | ~_t74 | ~_t36 | ~_t35 | ~_t30 | _t27 [ LRES, 2156, 1074, ~_t25 ] [ Backward Subsumption, 2165 ] % 0.49/0.63 (33,1) [2165,10]. true => ~_t112 | ~_t74 | ~_t36 | ~_t35 | ~_t30 [ LRES, 2163, 1568, _t27 ] [ Backward Subsumption, 2187 ] % 0.49/0.63 (33,1) [2187,10]. true => ~_t112 | ~_t74 | ~_t36 | ~_t35 [ LRES, 2165, 1064, ~_t30 ] [ Backward Subsumption, 2190 ] % 0.49/0.63 (33,1) [2190,10]. true => ~_t112 | ~_t74 | ~_t36 [ LRES, 2187, 1905, ~_t35 ] [ Backward Subsumption, 2193 ] % 0.49/0.63 (33,1) [2193,10]. true => ~_t112 | ~_t74 [ LRES, 2190, 1036, ~_t36 ] % 0.49/0.63 (436,1) [2197,10]. true => ~_t116 | ~_t112 [ LRES, 2193, 608, ~_t74 ] % 0.49/0.63 (6,1) [7,11]. _t22 => ~box 1~ _t23 [ SNF ] [ SNF++, 461, _t23 ] % 0.49/0.63 (8,1) [13,11]. _t27 => ~box 1~ _t28 [ SNF ] [ SNF++, 463, _t28 ] % 0.49/0.63 (15,1) [20,11]. _t29 => ~box 1~ _t21 [ SNF ] [ SNF++, 465, _t21 ] % 0.49/0.63 (1,1) [21,11]. true => _t29 | _t27 | ~_t26 [ SNF ] % 0.49/0.63 (1,1) [28,11]. _t32 => box 1 _t27 [ SNF ] [ SNF++, 483, _t27 ] % 0.49/0.63 (1,1) [29,11]. _t32 => ~box 1~ _t27 [ Axiom SER ] [ SNF++, 467, _t27 ] % 0.49/0.63 (1,1) [30,11]. _t33 => box 1 _t23 [ SNF ] [ SNF++, 485, _t23 ] % 0.49/0.63 (1,1) [31,11]. _t33 => ~box 1~ _t23 [ Axiom SER ] [ SNF++, 459, _t23 ] % 0.49/0.63 (1,1) [32,11]. true => _t33 | _t32 | ~_t31 | ~p0 [ SNF ] % 0.49/0.63 (1,1) [40,11]. _t21 => box 1 _t22 [ SNF ] [ SNF++, 487, _t22 ] % 0.49/0.63 (1,1) [41,11]. _t21 => ~box 1~ _t22 [ Axiom SER ] [ SNF++, 469, _t22 ] % 0.49/0.63 (1,1) [44,11]. _t28 => box 1 ~p0 [ SNF ] [ SNF++, 489, ~p0 ] % 0.49/0.63 (33,1) [49,11]. true => ~_t23 | p0 [ SNF ] % 0.49/0.63 (435,1) [402,11]. _t75 => ~box 1~ ~p0 [ SNF ] [ SNF++, 471, ~p0 ] % 0.49/0.63 (6,1) [461,11]. _t22 => ~box 1~ _t100 [ SNF++, 7 ] % 0.49/0.63 (8,1) [463,11]. _t27 => ~box 1~ _t99 [ SNF++, 13 ] % 0.49/0.63 (15,1) [465,11]. _t29 => ~box 1~ _t101 [ SNF++, 20 ] % 0.49/0.63 (435,1) [471,11]. _t75 => ~box 1~ _t97 [ SNF++, 402 ] % 0.49/0.63 (1,1) [483,11]. _t32 => box 1 _t102 [ SNF++, 28 ] % 0.49/0.63 (1,1) [485,11]. _t33 => box 1 _t100 [ SNF++, 30 ] % 0.49/0.63 (1,1) [487,11]. _t21 => box 1 _t98 [ SNF++, 40 ] % 0.49/0.63 (1,1) [489,11]. _t28 => box 1 _t97 [ SNF++, 44 ] % 0.49/0.63 (1,1) [498,11]. true => ~_t98 | _t22 [ SNF++, 8 ] % 0.49/0.63 (1,1) [500,11]. true => ~_t106 | _t26 [ SNF++, 22 ] % 0.49/0.63 (1,1) [502,11]. true => ~_t107 | _t31 [ SNF++, 33 ] % 0.49/0.63 (1,1) [504,11]. true => ~_t101 | _t21 [ SNF++, 42 ] % 0.49/0.63 (1,1) [518,11]. true => ~_t111 | _t75 [ SNF++, 403 ] % 0.49/0.63 (26,1) [528,11]. true => ~_t99 | _t28 [ SNF++, 46 ] % 0.49/0.63 (33,1) [530,11]. true => ~_t100 | _t23 [ SNF++, 52 ] % 0.49/0.63 (1,1) [1110,11]. true => ~_t106 | _t29 | _t27 [ LRES, 21, 500, ~_t26 ] % 0.49/0.63 (435,1) [1161,11]. true => ~_t75 | ~_t33 [ GEN1, 485, 471, 1107, _t100, _t97 ] % 0.49/0.63 (6,1) [1164,11]. true => ~_t28 | ~_t22 [ GEN1, 489, 461, 1107, _t97, _t100 ] % 0.49/0.63 (8,1) [1174,11]. true => ~_t27 | ~_t21 [ GEN1, 487, 463, 1171, _t98, _t99 ] % 0.49/0.63 (8,1) [1175,11]. true => ~_t101 | ~_t27 [ LRES, 1174, 504, ~_t21 ] % 0.49/0.63 (15,1) [1320,11]. true => ~_t32 | ~_t29 [ GEN1, 483, 465, 1177, _t102, _t101 ] % 0.49/0.63 (6,1) [1347,11]. true => ~_t98 | ~_t28 [ LRES, 1164, 498, ~_t22 ] % 0.49/0.63 (26,1) [1356,11]. true => ~_t99 | ~_t98 [ LRES, 1347, 528, ~_t28 ] % 0.49/0.63 (8,1) [1563,11]. true => ~_t106 | ~_t101 | _t29 [ LRES, 1110, 1175, _t27 ] % 0.49/0.63 (15,1) [1844,11]. true => ~_t106 | ~_t101 | ~_t32 [ LRES, 1563, 1320, _t29 ] % 0.49/0.63 (33,1) [1846,11]. true => _t33 | _t32 | ~_t31 | ~_t23 [ LRES, 32, 49, ~p0 ] % 0.49/0.63 (33,1) [1847,11]. true => ~_t100 | _t33 | _t32 | ~_t31 [ LRES, 1846, 530, ~_t23 ] % 0.49/0.63 (33,1) [1848,11]. true => ~_t107 | ~_t100 | _t33 | _t32 [ LRES, 1847, 502, ~_t31 ] % 0.49/0.63 (33,1) [1849,11]. true => ~_t107 | ~_t106 | ~_t101 | ~_t100 | _t33 [ LRES, 1848, 1844, _t32 ] % 0.49/0.63 (435,1) [1850,11]. true => ~_t107 | ~_t106 | ~_t101 | ~_t100 | ~_t75 [ LRES, 1849, 1161, _t33 ] % 0.49/0.63 (435,1) [1852,11]. true => ~_t111 | ~_t107 | ~_t106 | ~_t101 | ~_t100 [ LRES, 1850, 518, ~_t75 ] % 0.49/0.63 (6,1) [4,12]. true => ~_t23 | p0 [ SNF ] % 0.49/0.63 (1,1) [11,12]. _t28 => box 1 ~p0 [ SNF ] [ SNF++, 455, ~p0 ] % 0.49/0.63 (1,1) [12,12]. _t28 => ~box 1~ ~p0 [ Axiom SER ] [ SNF++, 447, ~p0 ] % 0.49/0.63 (1,1) [18,12]. _t21 => box 1 _t22 [ SNF ] [ SNF++, 457, _t22 ] % 0.49/0.63 (1,1) [19,12]. _t21 => ~box 1~ _t22 [ Axiom SER ] [ SNF++, 449, _t22 ] % 0.49/0.63 (17,1) [27,12]. _t27 => ~box 1~ _t28 [ SNF ] [ SNF++, 451, _t28 ] % 0.49/0.63 (24,1) [39,12]. _t22 => ~box 1~ _t23 [ SNF ] [ SNF++, 453, _t23 ] % 0.49/0.63 (17,1) [451,12]. _t27 => ~box 1~ _t99 [ SNF++, 27 ] % 0.49/0.63 (24,1) [453,12]. _t22 => ~box 1~ _t100 [ SNF++, 39 ] % 0.49/0.63 (1,1) [455,12]. _t28 => box 1 _t97 [ SNF++, 11 ] % 0.49/0.63 (1,1) [457,12]. _t21 => box 1 _t98 [ SNF++, 18 ] % 0.49/0.63 (1,1) [460,12]. true => ~_t100 | _t23 [ SNF++, 31 ] % 0.49/0.63 (8,1) [464,12]. true => ~_t99 | _t28 [ SNF++, 13 ] % 0.49/0.63 (15,1) [466,12]. true => ~_t101 | _t21 [ SNF++, 20 ] % 0.49/0.63 (1,1) [468,12]. true => ~_t102 | _t27 [ SNF++, 29 ] % 0.49/0.63 (1,1) [470,12]. true => ~_t98 | _t22 [ SNF++, 41 ] % 0.49/0.63 (435,1) [472,12]. true => ~_t97 | ~p0 [ SNF++, 402 ] % 0.49/0.63 (435,1) [1049,12]. true => ~_t97 | ~_t23 [ LRES, 472, 4, ~p0 ] % 0.49/0.63 (435,1) [1107,12]. true => ~_t100 | ~_t97 [ LRES, 1049, 460, ~_t23 ] % 0.49/0.63 (24,1) [1111,12]. true => ~_t28 | ~_t22 [ GEN1, 455, 453, 1097, _t97, _t100 ] % 0.49/0.63 (24,1) [1168,12]. true => ~_t98 | ~_t28 [ LRES, 1111, 470, ~_t22 ] % 0.49/0.63 (17,1) [1170,12]. true => ~_t27 | ~_t21 [ GEN1, 457, 451, 1167, _t98, _t99 ] % 0.49/0.63 (24,1) [1171,12]. true => ~_t99 | ~_t98 [ LRES, 1168, 464, ~_t28 ] % 0.49/0.63 (17,1) [1173,12]. true => ~_t101 | ~_t27 [ LRES, 1170, 466, ~_t21 ] % 0.49/0.63 (17,1) [1177,12]. true => ~_t102 | ~_t101 [ LRES, 1173, 468, ~_t27 ] % 0.49/0.63 (14,1) [17,13]. _t22 => ~box 1~ _t23 [ SNF ] [ SNF++, 553, _t23 ] % 0.49/0.63 (1,1) [25,13]. _t28 => box 1 ~p0 [ SNF ] [ SNF++, 557, ~p0 ] % 0.49/0.63 (1,1) [26,13]. _t28 => ~box 1~ ~p0 [ Axiom SER ] [ SNF++, 555, ~p0 ] % 0.49/0.63 (24,1) [36,13]. true => ~_t23 | p0 [ SNF ] % 0.49/0.63 (1,1) [448,13]. true => ~_t97 | ~p0 [ SNF++, 12 ] % 0.49/0.63 (1,1) [450,13]. true => ~_t98 | _t22 [ SNF++, 19 ] % 0.49/0.63 (17,1) [452,13]. true => ~_t99 | _t28 [ SNF++, 27 ] % 0.49/0.63 (24,1) [454,13]. true => ~_t100 | _t23 [ SNF++, 39 ] % 0.49/0.63 (14,1) [553,13]. _t22 => ~box 1~ _t100 [ SNF++, 17 ] % 0.49/0.63 (1,1) [557,13]. _t28 => box 1 _t97 [ SNF++, 25 ] % 0.49/0.63 (24,1) [1053,13]. true => ~_t97 | ~_t23 [ LRES, 448, 36, ~p0 ] % 0.49/0.63 (24,1) [1097,13]. true => ~_t100 | ~_t97 [ LRES, 1053, 454, ~_t23 ] % 0.49/0.63 (14,1) [1109,13]. true => ~_t28 | ~_t22 [ GEN1, 557, 553, 1075, _t97, _t100 ] % 0.49/0.63 (14,1) [1139,13]. true => ~_t98 | ~_t28 [ LRES, 1109, 450, ~_t22 ] % 0.49/0.63 (17,1) [1167,13]. true => ~_t99 | ~_t98 [ LRES, 1139, 452, ~_t28 ] % 0.49/0.63 (14,1) [14,14]. true => ~_t23 | p0 [ SNF ] % 0.49/0.63 (14,1) [554,14]. true => ~_t100 | _t23 [ SNF++, 17 ] % 0.49/0.63 (1,1) [556,14]. true => ~_t97 | ~p0 [ SNF++, 26 ] % 0.49/0.63 (14,1) [1051,14]. true => ~_t97 | ~_t23 [ LRES, 556, 14, ~p0 ] % 0.49/0.63 (14,1) [1075,14]. true => ~_t100 | ~_t97 [ LRES, 1051, 554, ~_t23 ] % 0.49/0.63 % SZS output end Refutation % 0.49/0.63 % KSP exiting %------------------------------------------------------------------------------