%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYO920_1.014 : TPTP v9.0.0. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n023.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 : Wed Apr 9 10:47:48 PM UTC 2025 % Result : Theorem 0.18s 0.60s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SYO920_1.014 : TPTP v9.0.0. Released v9.0.0. % 0.06/0.12 % Command : run_ksp %s % 0.11/0.33 % Computer : n023.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Wed Apr 9 10:26:24 EDT 2025 % 0.11/0.33 % CPUTime : % 0.18/0.58 ----KSP format--- % 0.18/0.58 usable(formulas). % 0.18/0.58 true. % 0.18/0.58 end_of_list. % 0.18/0.58 sos(formulas). % 0.18/0.58 ~ (~ ( ~ ( <> ( ~ ( ( [] ( ~ ( 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 ) ) ) ) | <> ( ( [] ( <> ( 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 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) | <> ( p4 ) ) ) ). % 0.18/0.58 end_of_list. % 0.18/0.58 ----------------- % 0.18/0.58 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.lNKFCGwLsz/theBenchmark.ksp % 0.18/0.60 % 0.18/0.60 % SZS status Theorem % 0.18/0.60 % 0.18/0.60 ***************** % 0.18/0.60 FOUND PROOF 1 % 0.18/0.60 ***************** % 0.18/0.60 % SZS output start Refutation % 0.18/0.60 % 0.18/0.60 (1,1) [1,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.18/0.60 (1,1) [204,0]. _t0 => box 1 _t2 [ SNF ] [ Backward Subsumption, 329 ] % 0.18/0.60 (755,1) [318,0]. _t0 => ~box 1~ _t64 [ SNF ] [ Backward Subsumption, 324 ] % 0.18/0.60 (755,1) [324,0]. true => ~box 1~ _t64 [ LHS Unit Resolution, 1, 318, _t0 ] [ SNF++, 848, _t64 ] % 0.18/0.60 (1,1) [329,0]. true => box 1 _t2 [ LHS Unit Resolution, 1, 204, _t0 ] [ SNF++, 838, _t2 ] % 0.18/0.60 (1,1) [838,0]. true => box 1 _t138 [ SNF++, 329 ] % 0.18/0.60 (755,1) [848,0]. true => ~box 1~ _t139 [ SNF++, 324 ] % 0.18/0.60 (755,1) [1853,0]. true => false [ GEN1, 838, 848, 1852, _t138, _t139 ] % 0.18/0.60 (1,1) [191,1]. _t2 => box 1 _t4 [ SNF ] [ SNF++, 810, _t4 ] % 0.18/0.60 (753,1) [317,1]. _t64 => ~box 1~ _t66 [ SNF ] [ SNF++, 836, _t66 ] % 0.18/0.60 (1,1) [810,1]. _t2 => box 1 _t136 [ SNF++, 191 ] % 0.18/0.60 (753,1) [836,1]. _t64 => ~box 1~ _t137 [ SNF++, 317 ] % 0.18/0.60 (1,1) [839,1]. true => ~_t138 | _t2 [ SNF++, 329 ] % 0.18/0.60 (755,1) [849,1]. true => ~_t139 | _t64 [ SNF++, 324 ] % 0.18/0.60 (753,1) [1850,1]. true => ~_t64 | ~_t2 [ GEN1, 810, 836, 1849, _t136, _t137 ] % 0.18/0.60 (753,1) [1851,1]. true => ~_t138 | ~_t64 [ LRES, 1850, 839, ~_t2 ] % 0.18/0.60 (755,1) [1852,1]. true => ~_t139 | ~_t138 [ LRES, 1851, 849, ~_t64 ] % 0.18/0.60 (1,1) [178,2]. _t4 => box 1 _t6 [ SNF ] [ SNF++, 776, _t6 ] % 0.18/0.60 (752,1) [316,2]. _t66 => ~box 1~ _t68 [ SNF ] [ SNF++, 808, _t68 ] % 0.18/0.60 (1,1) [776,2]. _t4 => box 1 _t134 [ SNF++, 178 ] % 0.18/0.60 (752,1) [808,2]. _t66 => ~box 1~ _t135 [ SNF++, 316 ] % 0.18/0.60 (1,1) [811,2]. true => ~_t136 | _t4 [ SNF++, 191 ] % 0.18/0.60 (753,1) [837,2]. true => ~_t137 | _t66 [ SNF++, 317 ] % 0.18/0.60 (752,1) [1847,2]. true => ~_t66 | ~_t4 [ GEN1, 776, 808, 1846, _t134, _t135 ] % 0.18/0.60 (752,1) [1848,2]. true => ~_t136 | ~_t66 [ LRES, 1847, 811, ~_t4 ] % 0.18/0.60 (753,1) [1849,2]. true => ~_t137 | ~_t136 [ LRES, 1848, 837, ~_t66 ] % 0.18/0.60 (1,1) [165,3]. _t6 => box 1 _t8 [ SNF ] [ SNF++, 742, _t8 ] % 0.18/0.60 (751,1) [315,3]. _t68 => ~box 1~ _t70 [ SNF ] [ SNF++, 774, _t70 ] % 0.18/0.60 (1,1) [742,3]. _t6 => box 1 _t132 [ SNF++, 165 ] % 0.18/0.60 (751,1) [774,3]. _t68 => ~box 1~ _t133 [ SNF++, 315 ] % 0.18/0.60 (1,1) [777,3]. true => ~_t134 | _t6 [ SNF++, 178 ] % 0.18/0.60 (752,1) [809,3]. true => ~_t135 | _t68 [ SNF++, 316 ] % 0.18/0.60 (751,1) [1844,3]. true => ~_t68 | ~_t6 [ GEN1, 742, 774, 1843, _t132, _t133 ] % 0.18/0.60 (751,1) [1845,3]. true => ~_t134 | ~_t68 [ LRES, 1844, 777, ~_t6 ] % 0.18/0.60 (752,1) [1846,3]. true => ~_t135 | ~_t134 [ LRES, 1845, 809, ~_t68 ] % 0.18/0.60 (1,1) [152,4]. _t8 => box 1 _t10 [ SNF ] [ SNF++, 708, _t10 ] % 0.18/0.60 (750,1) [314,4]. _t70 => ~box 1~ _t72 [ SNF ] [ SNF++, 740, _t72 ] % 0.18/0.60 (1,1) [708,4]. _t8 => box 1 _t130 [ SNF++, 152 ] % 0.18/0.60 (750,1) [740,4]. _t70 => ~box 1~ _t131 [ SNF++, 314 ] % 0.18/0.60 (1,1) [743,4]. true => ~_t132 | _t8 [ SNF++, 165 ] % 0.18/0.60 (751,1) [775,4]. true => ~_t133 | _t70 [ SNF++, 315 ] % 0.18/0.60 (750,1) [1841,4]. true => ~_t70 | ~_t8 [ GEN1, 708, 740, 1840, _t130, _t131 ] % 0.18/0.60 (750,1) [1842,4]. true => ~_t132 | ~_t70 [ LRES, 1841, 743, ~_t8 ] % 0.18/0.60 (751,1) [1843,4]. true => ~_t133 | ~_t132 [ LRES, 1842, 775, ~_t70 ] % 0.18/0.60 (1,1) [139,5]. _t10 => box 1 _t12 [ SNF ] [ SNF++, 674, _t12 ] % 0.18/0.60 (749,1) [313,5]. _t72 => ~box 1~ _t74 [ SNF ] [ SNF++, 706, _t74 ] % 0.18/0.60 (1,1) [674,5]. _t10 => box 1 _t128 [ SNF++, 139 ] % 0.18/0.60 (749,1) [706,5]. _t72 => ~box 1~ _t129 [ SNF++, 313 ] % 0.18/0.60 (1,1) [709,5]. true => ~_t130 | _t10 [ SNF++, 152 ] % 0.18/0.60 (750,1) [741,5]. true => ~_t131 | _t72 [ SNF++, 314 ] % 0.18/0.60 (749,1) [1838,5]. true => ~_t72 | ~_t10 [ GEN1, 674, 706, 1837, _t128, _t129 ] % 0.18/0.60 (749,1) [1839,5]. true => ~_t130 | ~_t72 [ LRES, 1838, 709, ~_t10 ] % 0.18/0.60 (750,1) [1840,5]. true => ~_t131 | ~_t130 [ LRES, 1839, 741, ~_t72 ] % 0.18/0.60 (1,1) [126,6]. _t12 => box 1 _t14 [ SNF ] [ SNF++, 640, _t14 ] % 0.18/0.60 (748,1) [312,6]. _t74 => ~box 1~ _t76 [ SNF ] [ SNF++, 672, _t76 ] % 0.18/0.60 (1,1) [640,6]. _t12 => box 1 _t126 [ SNF++, 126 ] % 0.18/0.60 (748,1) [672,6]. _t74 => ~box 1~ _t127 [ SNF++, 312 ] % 0.18/0.60 (1,1) [675,6]. true => ~_t128 | _t12 [ SNF++, 139 ] % 0.18/0.60 (749,1) [707,6]. true => ~_t129 | _t74 [ SNF++, 313 ] % 0.18/0.60 (748,1) [1835,6]. true => ~_t74 | ~_t12 [ GEN1, 640, 672, 1834, _t126, _t127 ] % 0.18/0.60 (748,1) [1836,6]. true => ~_t128 | ~_t74 [ LRES, 1835, 675, ~_t12 ] % 0.18/0.60 (749,1) [1837,6]. true => ~_t129 | ~_t128 [ LRES, 1836, 707, ~_t74 ] % 0.18/0.60 (1,1) [113,7]. _t14 => box 1 _t16 [ SNF ] [ SNF++, 606, _t16 ] % 0.18/0.60 (747,1) [311,7]. _t76 => ~box 1~ _t78 [ SNF ] [ SNF++, 638, _t78 ] % 0.18/0.60 (1,1) [606,7]. _t14 => box 1 _t124 [ SNF++, 113 ] % 0.18/0.60 (747,1) [638,7]. _t76 => ~box 1~ _t125 [ SNF++, 311 ] % 0.18/0.60 (1,1) [641,7]. true => ~_t126 | _t14 [ SNF++, 126 ] % 0.18/0.60 (748,1) [673,7]. true => ~_t127 | _t76 [ SNF++, 312 ] % 0.18/0.60 (747,1) [1832,7]. true => ~_t76 | ~_t14 [ GEN1, 606, 638, 1831, _t124, _t125 ] % 0.18/0.60 (747,1) [1833,7]. true => ~_t126 | ~_t76 [ LRES, 1832, 641, ~_t14 ] % 0.18/0.60 (748,1) [1834,7]. true => ~_t127 | ~_t126 [ LRES, 1833, 673, ~_t76 ] % 0.18/0.60 (1,1) [100,8]. _t16 => box 1 _t18 [ SNF ] [ SNF++, 572, _t18 ] % 0.18/0.60 (746,1) [310,8]. _t78 => ~box 1~ _t80 [ SNF ] [ SNF++, 604, _t80 ] % 0.18/0.60 (1,1) [572,8]. _t16 => box 1 _t122 [ SNF++, 100 ] % 0.18/0.60 (746,1) [604,8]. _t78 => ~box 1~ _t123 [ SNF++, 310 ] % 0.18/0.60 (1,1) [607,8]. true => ~_t124 | _t16 [ SNF++, 113 ] % 0.18/0.60 (747,1) [639,8]. true => ~_t125 | _t78 [ SNF++, 311 ] % 0.18/0.60 (746,1) [1829,8]. true => ~_t78 | ~_t16 [ GEN1, 572, 604, 1828, _t122, _t123 ] % 0.18/0.60 (746,1) [1830,8]. true => ~_t124 | ~_t78 [ LRES, 1829, 607, ~_t16 ] % 0.18/0.60 (747,1) [1831,8]. true => ~_t125 | ~_t124 [ LRES, 1830, 639, ~_t78 ] % 0.18/0.60 (1,1) [87,9]. _t18 => box 1 _t20 [ SNF ] [ SNF++, 538, _t20 ] % 0.18/0.60 (745,1) [309,9]. _t80 => ~box 1~ _t82 [ SNF ] [ SNF++, 570, _t82 ] % 0.18/0.60 (1,1) [538,9]. _t18 => box 1 _t120 [ SNF++, 87 ] % 0.18/0.60 (745,1) [570,9]. _t80 => ~box 1~ _t121 [ SNF++, 309 ] % 0.18/0.60 (1,1) [573,9]. true => ~_t122 | _t18 [ SNF++, 100 ] % 0.18/0.60 (746,1) [605,9]. true => ~_t123 | _t80 [ SNF++, 310 ] % 0.18/0.60 (745,1) [1826,9]. true => ~_t80 | ~_t18 [ GEN1, 538, 570, 1825, _t120, _t121 ] % 0.18/0.60 (745,1) [1827,9]. true => ~_t122 | ~_t80 [ LRES, 1826, 573, ~_t18 ] % 0.18/0.60 (746,1) [1828,9]. true => ~_t123 | ~_t122 [ LRES, 1827, 605, ~_t80 ] % 0.18/0.60 (1,1) [74,10]. _t20 => box 1 _t22 [ SNF ] [ SNF++, 504, _t22 ] % 0.18/0.60 (744,1) [308,10]. _t82 => ~box 1~ _t84 [ SNF ] [ SNF++, 536, _t84 ] % 0.18/0.60 (1,1) [504,10]. _t20 => box 1 _t118 [ SNF++, 74 ] % 0.18/0.60 (744,1) [536,10]. _t82 => ~box 1~ _t119 [ SNF++, 308 ] % 0.18/0.60 (1,1) [539,10]. true => ~_t120 | _t20 [ SNF++, 87 ] % 0.18/0.60 (745,1) [571,10]. true => ~_t121 | _t82 [ SNF++, 309 ] % 0.18/0.60 (744,1) [1823,10]. true => ~_t82 | ~_t20 [ GEN1, 504, 536, 1822, _t118, _t119 ] % 0.18/0.60 (744,1) [1824,10]. true => ~_t120 | ~_t82 [ LRES, 1823, 539, ~_t20 ] % 0.18/0.60 (745,1) [1825,10]. true => ~_t121 | ~_t120 [ LRES, 1824, 571, ~_t82 ] % 0.18/0.60 (1,1) [61,11]. _t22 => box 1 _t24 [ SNF ] [ SNF++, 470, _t24 ] % 0.18/0.60 (743,1) [307,11]. _t84 => ~box 1~ _t86 [ SNF ] [ SNF++, 502, _t86 ] % 0.18/0.60 (1,1) [470,11]. _t22 => box 1 _t116 [ SNF++, 61 ] % 0.18/0.60 (743,1) [502,11]. _t84 => ~box 1~ _t117 [ SNF++, 307 ] % 0.18/0.60 (1,1) [505,11]. true => ~_t118 | _t22 [ SNF++, 74 ] % 0.18/0.60 (744,1) [537,11]. true => ~_t119 | _t84 [ SNF++, 308 ] % 0.18/0.60 (743,1) [1819,11]. true => ~_t84 | ~_t22 [ GEN1, 470, 502, 1817, _t116, _t117 ] % 0.18/0.60 (743,1) [1821,11]. true => ~_t118 | ~_t84 [ LRES, 1819, 505, ~_t22 ] % 0.18/0.60 (744,1) [1822,11]. true => ~_t119 | ~_t118 [ LRES, 1821, 537, ~_t84 ] % 0.18/0.60 (1,1) [48,12]. _t24 => box 1 _t26 [ SNF ] [ SNF++, 436, _t26 ] % 0.18/0.60 (742,1) [306,12]. _t86 => ~box 1~ _t88 [ SNF ] [ SNF++, 468, _t88 ] % 0.18/0.60 (1,1) [436,12]. _t24 => box 1 _t114 [ SNF++, 48 ] % 0.18/0.60 (742,1) [468,12]. _t86 => ~box 1~ _t115 [ SNF++, 306 ] % 0.18/0.60 (1,1) [471,12]. true => ~_t116 | _t24 [ SNF++, 61 ] % 0.18/0.60 (743,1) [503,12]. true => ~_t117 | _t86 [ SNF++, 307 ] % 0.18/0.60 (742,1) [1812,12]. true => ~_t86 | ~_t24 [ GEN1, 436, 468, 1810, _t114, _t115 ] % 0.18/0.60 (742,1) [1814,12]. true => ~_t116 | ~_t86 [ LRES, 1812, 471, ~_t24 ] % 0.18/0.60 (743,1) [1817,12]. true => ~_t117 | ~_t116 [ LRES, 1814, 503, ~_t86 ] % 0.18/0.60 (1,1) [35,13]. _t26 => box 1 _t28 [ SNF ] [ SNF++, 402, _t28 ] % 0.18/0.60 (738,1) [302,13]. _t88 => ~box 1~ _t90 [ SNF ] [ SNF++, 432, _t90 ] % 0.18/0.60 (1,1) [402,13]. _t26 => box 1 _t108 [ SNF++, 35 ] % 0.18/0.60 (738,1) [432,13]. _t88 => ~box 1~ _t112 [ SNF++, 302 ] % 0.18/0.60 (1,1) [437,13]. true => ~_t114 | _t26 [ SNF++, 48 ] % 0.18/0.60 (742,1) [469,13]. true => ~_t115 | _t88 [ SNF++, 306 ] % 0.18/0.60 (738,1) [1806,13]. true => ~_t88 | ~_t26 [ GEN1, 402, 432, 1804, _t108, _t112 ] % 0.18/0.60 (738,1) [1808,13]. true => ~_t114 | ~_t88 [ LRES, 1806, 437, ~_t26 ] % 0.18/0.60 (742,1) [1810,13]. true => ~_t115 | ~_t114 [ LRES, 1808, 469, ~_t88 ] % 0.18/0.60 (1,1) [5,14]. _t28 => box 1 _t30 [ SNF ] [ SNF++, 362, _t30 ] % 0.18/0.60 (1,1) [14,14]. _t28 => box 1 _t34 [ SNF ] [ SNF++, 364, _t34 ] % 0.18/0.60 (1,1) [20,14]. _t28 => box 1 _t39 [ SNF ] [ SNF++, 366, _t39 ] % 0.18/0.60 (1,1) [25,14]. _t43 => box 1 _t29 [ SNF ] [ SNF++, 368, _t29 ] % 0.18/0.60 (26,1) [27,14]. _t35 => ~box 1~ _t36 [ SNF ] [ SNF++, 384, _t36 ] % 0.18/0.60 (1,1) [28,14]. true => _t43 | ~_t42 | _t35 [ SNF ] % 0.18/0.60 (1,1) [29,14]. true => _t42 | ~_t28 [ SNF ] % 0.18/0.60 (33,1) [32,14]. _t30 => ~box 1~ _t31 [ SNF ] [ SNF++, 386, _t31 ] % 0.18/0.60 (1,1) [33,14]. true => ~_t44 | _t35 | _t30 [ SNF ] % 0.18/0.60 (1,1) [34,14]. true => _t44 | ~_t28 [ SNF ] % 0.18/0.60 (1,1) [301,14]. _t90 => box 1 _t91 [ SNF ] [ SNF++, 382, _t91 ] % 0.18/0.60 (1,1) [362,14]. _t28 => box 1 _t96 [ SNF++, 5 ] % 0.18/0.60 (1,1) [364,14]. _t28 => box 1 _t102 [ SNF++, 14 ] % 0.18/0.60 (1,1) [366,14]. _t28 => box 1 _t103 [ SNF++, 20 ] % 0.18/0.60 (1,1) [368,14]. _t43 => box 1 _t97 [ SNF++, 25 ] % 0.18/0.60 (1,1) [382,14]. _t90 => box 1 _t107 [ SNF++, 301 ] % 0.18/0.60 (26,1) [384,14]. _t35 => ~box 1~ _t93 [ SNF++, 27 ] % 0.18/0.60 (33,1) [386,14]. _t30 => ~box 1~ _t94 [ SNF++, 32 ] % 0.18/0.60 (1,1) [403,14]. true => ~_t108 | _t28 [ SNF++, 35 ] % 0.18/0.60 (738,1) [433,14]. true => ~_t112 | _t90 [ SNF++, 302 ] % 0.18/0.60 (1,1) [854,14]. true => ~_t108 | _t44 [ LRES, 34, 403, ~_t28 ] % 0.18/0.60 (1,1) [881,14]. true => ~_t108 | _t42 [ LRES, 29, 403, ~_t28 ] % 0.18/0.60 (26,1) [1185,14]. true => ~_t35 | ~_t28 [ GEN1, 362, 384, 1079, _t96, _t93 ] % 0.18/0.60 (26,1) [1262,14]. true => ~_t108 | ~_t35 [ LRES, 1185, 403, ~_t28 ] % 0.18/0.60 (26,1) [1282,14]. true => ~_t108 | _t43 | ~_t42 [ LRES, 1262, 28, ~_t35 ] [ Backward Subsumption, 1428 ] % 0.18/0.60 (26,1) [1428,14]. true => ~_t108 | _t43 [ LRES, 1282, 881, ~_t42 ] % 0.18/0.60 (33,1) [1701,14]. true => ~_t90 | ~_t43 | ~_t30 | ~_t28 [ GEN1, 382, 364, 368, 366, 386, 1687, _t107, _t102, _t97, _t103, _t94 ] % 0.18/0.60 (33,1) [1717,14]. true => ~_t108 | ~_t90 | ~_t43 | ~_t30 [ LRES, 1701, 403, ~_t28 ] [ Backward Subsumption, 1802 ] % 0.18/0.60 (33,1) [1770,14]. true => ~_t108 | ~_t90 | ~_t44 | ~_t43 | _t35 [ LRES, 1717, 33, ~_t30 ] [ Backward Subsumption, 1795 ] % 0.18/0.60 (33,1) [1795,14]. true => ~_t108 | ~_t90 | ~_t44 | ~_t43 [ LRES, 1770, 1262, _t35 ] [ Backward Subsumption, 1800 ] % 0.18/0.60 (33,1) [1800,14]. true => ~_t108 | ~_t90 | ~_t44 [ LRES, 1795, 1428, ~_t43 ] [ Backward Subsumption, 1802 ] % 0.18/0.60 (33,1) [1802,14]. true => ~_t108 | ~_t90 [ LRES, 1800, 854, ~_t44 ] % 0.18/0.60 (738,1) [1804,14]. true => ~_t112 | ~_t108 [ LRES, 1802, 433, ~_t90 ] % 0.18/0.60 (6,1) [4,15]. _t30 => ~box 1~ _t31 [ SNF ] [ SNF++, 338, _t31 ] % 0.18/0.60 (8,1) [7,15]. _t35 => ~box 1~ _t36 [ SNF ] [ SNF++, 340, _t36 ] % 0.18/0.60 (15,1) [12,15]. _t37 => ~box 1~ _t29 [ SNF ] [ SNF++, 342, _t29 ] % 0.18/0.60 (1,1) [13,15]. true => _t37 | _t35 | ~_t34 [ SNF ] % 0.18/0.60 (1,1) [17,15]. _t40 => box 1 _t35 [ SNF ] [ SNF++, 348, _t35 ] % 0.18/0.60 (1,1) [18,15]. _t41 => box 1 _t31 [ SNF ] [ SNF++, 350, _t31 ] % 0.18/0.60 (1,1) [19,15]. true => _t41 | _t40 | ~_t39 | ~p0 [ SNF ] % 0.18/0.60 (1,1) [24,15]. _t29 => box 1 _t30 [ SNF ] [ SNF++, 352, _t30 ] % 0.18/0.60 (1,1) [26,15]. _t36 => box 1 ~p0 [ SNF ] [ SNF++, 354, ~p0 ] % 0.18/0.60 (33,1) [30,15]. true => ~_t31 | p0 [ SNF ] % 0.18/0.60 (737,1) [300,15]. _t91 => ~box 1~ ~p0 [ SNF ] [ SNF++, 346, ~p0 ] % 0.18/0.60 (6,1) [338,15]. _t30 => ~box 1~ _t94 [ SNF++, 4 ] % 0.18/0.60 (8,1) [340,15]. _t35 => ~box 1~ _t93 [ SNF++, 7 ] % 0.18/0.60 (15,1) [342,15]. _t37 => ~box 1~ _t97 [ SNF++, 12 ] % 0.18/0.60 (737,1) [346,15]. _t91 => ~box 1~ _t95 [ SNF++, 300 ] % 0.18/0.60 (1,1) [348,15]. _t40 => box 1 _t99 [ SNF++, 17 ] % 0.18/0.60 (1,1) [350,15]. _t41 => box 1 _t94 [ SNF++, 18 ] % 0.18/0.60 (1,1) [352,15]. _t29 => box 1 _t96 [ SNF++, 24 ] % 0.18/0.60 (1,1) [354,15]. _t36 => box 1 _t95 [ SNF++, 26 ] % 0.18/0.60 (1,1) [363,15]. true => ~_t96 | _t30 [ SNF++, 5 ] % 0.18/0.60 (1,1) [365,15]. true => ~_t102 | _t34 [ SNF++, 14 ] % 0.18/0.60 (1,1) [367,15]. true => ~_t103 | _t39 [ SNF++, 20 ] % 0.18/0.60 (1,1) [369,15]. true => ~_t97 | _t29 [ SNF++, 25 ] % 0.18/0.60 (1,1) [383,15]. true => ~_t107 | _t91 [ SNF++, 301 ] % 0.18/0.60 (26,1) [385,15]. true => ~_t93 | _t36 [ SNF++, 27 ] % 0.18/0.60 (33,1) [387,15]. true => ~_t94 | _t31 [ SNF++, 32 ] % 0.18/0.60 (1,1) [995,15]. true => ~_t102 | _t37 | _t35 [ LRES, 13, 365, ~_t34 ] % 0.18/0.60 (6,1) [1047,15]. true => ~_t36 | ~_t30 [ GEN1, 354, 338, 993, _t95, _t94 ] % 0.18/0.60 (737,1) [1048,15]. true => ~_t91 | ~_t41 [ GEN1, 350, 346, 993, _t94, _t95 ] % 0.18/0.60 (6,1) [1065,15]. true => ~_t96 | ~_t36 [ LRES, 1047, 363, ~_t30 ] % 0.18/0.60 (26,1) [1079,15]. true => ~_t96 | ~_t93 [ LRES, 1065, 385, ~_t36 ] % 0.18/0.60 (8,1) [1165,15]. true => ~_t35 | ~_t29 [ GEN1, 352, 340, 1078, _t96, _t93 ] % 0.18/0.60 (15,1) [1210,15]. true => ~_t40 | ~_t37 [ GEN1, 348, 342, 1184, _t99, _t97 ] % 0.18/0.60 (8,1) [1222,15]. true => ~_t97 | ~_t35 [ LRES, 1165, 369, ~_t29 ] % 0.18/0.60 (8,1) [1238,15]. true => ~_t102 | ~_t97 | _t37 [ LRES, 995, 1222, _t35 ] % 0.18/0.60 (15,1) [1371,15]. true => ~_t102 | ~_t97 | ~_t40 [ LRES, 1238, 1210, _t37 ] % 0.18/0.60 (33,1) [1557,15]. true => _t41 | _t40 | ~_t39 | ~_t31 [ LRES, 19, 30, ~p0 ] % 0.18/0.60 (33,1) [1649,15]. true => ~_t94 | _t41 | _t40 | ~_t39 [ LRES, 1557, 387, ~_t31 ] % 0.18/0.60 (33,1) [1675,15]. true => ~_t103 | ~_t94 | _t41 | _t40 [ LRES, 1649, 367, ~_t39 ] % 0.18/0.60 (33,1) [1679,15]. true => ~_t103 | ~_t102 | ~_t97 | ~_t94 | _t41 [ LRES, 1675, 1371, _t40 ] % 0.18/0.60 (737,1) [1682,15]. true => ~_t103 | ~_t102 | ~_t97 | ~_t94 | ~_t91 [ LRES, 1679, 1048, _t41 ] % 0.18/0.60 (737,1) [1687,15]. true => ~_t107 | ~_t103 | ~_t102 | ~_t97 | ~_t94 [ LRES, 1682, 383, ~_t91 ] % 0.18/0.60 (6,1) [2,16]. true => ~_t31 | p0 [ SNF ] % 0.18/0.60 (1,1) [6,16]. _t36 => box 1 ~p0 [ SNF ] [ SNF++, 334, ~p0 ] % 0.18/0.60 (1,1) [11,16]. _t29 => box 1 _t30 [ SNF ] [ SNF++, 336, _t30 ] % 0.18/0.60 (17,1) [16,16]. _t35 => ~box 1~ _t36 [ SNF ] [ SNF++, 330, _t36 ] % 0.18/0.60 (24,1) [23,16]. _t30 => ~box 1~ _t31 [ SNF ] [ SNF++, 332, _t31 ] % 0.18/0.60 (17,1) [330,16]. _t35 => ~box 1~ _t93 [ SNF++, 16 ] % 0.18/0.60 (24,1) [332,16]. _t30 => ~box 1~ _t94 [ SNF++, 23 ] % 0.18/0.60 (1,1) [334,16]. _t36 => box 1 _t95 [ SNF++, 6 ] % 0.18/0.60 (1,1) [336,16]. _t29 => box 1 _t96 [ SNF++, 11 ] % 0.18/0.60 (6,1) [339,16]. true => ~_t94 | _t31 [ SNF++, 4 ] % 0.18/0.60 (8,1) [341,16]. true => ~_t93 | _t36 [ SNF++, 7 ] % 0.18/0.60 (15,1) [343,16]. true => ~_t97 | _t29 [ SNF++, 12 ] % 0.18/0.60 (737,1) [347,16]. true => ~_t95 | ~p0 [ SNF++, 300 ] % 0.18/0.60 (1,1) [349,16]. true => ~_t99 | _t35 [ SNF++, 17 ] % 0.18/0.60 (1,1) [353,16]. true => ~_t96 | _t30 [ SNF++, 24 ] % 0.18/0.60 (737,1) [850,16]. true => ~_t95 | ~_t31 [ LRES, 347, 2, ~p0 ] % 0.18/0.60 (737,1) [993,16]. true => ~_t95 | ~_t94 [ LRES, 850, 339, ~_t31 ] % 0.18/0.60 (24,1) [996,16]. true => ~_t36 | ~_t30 [ GEN1, 334, 332, 880, _t95, _t94 ] % 0.18/0.60 (24,1) [1064,16]. true => ~_t96 | ~_t36 [ LRES, 996, 353, ~_t30 ] % 0.18/0.60 (17,1) [1066,16]. true => ~_t35 | ~_t29 [ GEN1, 336, 330, 1050, _t96, _t93 ] % 0.18/0.60 (24,1) [1078,16]. true => ~_t96 | ~_t93 [ LRES, 1064, 341, ~_t36 ] % 0.18/0.60 (17,1) [1162,16]. true => ~_t97 | ~_t35 [ LRES, 1066, 343, ~_t29 ] % 0.18/0.60 (17,1) [1184,16]. true => ~_t99 | ~_t97 [ LRES, 1162, 349, ~_t35 ] % 0.18/0.60 (14,1) [10,17]. _t30 => ~box 1~ _t31 [ SNF ] [ SNF++, 398, _t31 ] % 0.18/0.60 (1,1) [15,17]. _t36 => box 1 ~p0 [ SNF ] [ SNF++, 400, ~p0 ] % 0.18/0.60 (24,1) [21,17]. true => ~_t31 | p0 [ SNF ] % 0.18/0.60 (17,1) [331,17]. true => ~_t93 | _t36 [ SNF++, 16 ] % 0.18/0.60 (24,1) [333,17]. true => ~_t94 | _t31 [ SNF++, 23 ] % 0.18/0.60 (1,1) [335,17]. true => ~_t95 | ~p0 [ SNF++, 6 ] % 0.18/0.60 (1,1) [337,17]. true => ~_t96 | _t30 [ SNF++, 11 ] % 0.18/0.60 (14,1) [398,17]. _t30 => ~box 1~ _t94 [ SNF++, 10 ] % 0.18/0.60 (1,1) [400,17]. _t36 => box 1 _t95 [ SNF++, 15 ] % 0.18/0.60 (24,1) [853,17]. true => ~_t95 | ~_t31 [ LRES, 335, 21, ~p0 ] % 0.18/0.60 (24,1) [880,17]. true => ~_t95 | ~_t94 [ LRES, 853, 333, ~_t31 ] % 0.18/0.60 (14,1) [994,17]. true => ~_t36 | ~_t30 [ GEN1, 400, 398, 869, _t95, _t94 ] % 0.18/0.60 (14,1) [1028,17]. true => ~_t96 | ~_t36 [ LRES, 994, 337, ~_t30 ] % 0.18/0.60 (17,1) [1050,17]. true => ~_t96 | ~_t93 [ LRES, 1028, 331, ~_t36 ] % 0.18/0.60 (14,1) [8,18]. true => ~_t31 | p0 [ SNF ] % 0.18/0.60 (14,1) [399,18]. true => ~_t94 | _t31 [ SNF++, 10 ] % 0.18/0.60 (1,1) [401,18]. true => ~_t95 | ~p0 [ SNF++, 15 ] % 0.18/0.60 (14,1) [851,18]. true => ~_t95 | ~_t31 [ LRES, 401, 8, ~p0 ] % 0.18/0.60 (14,1) [869,18]. true => ~_t95 | ~_t94 [ LRES, 851, 399, ~_t31 ] % 0.18/0.60 % SZS output end Refutation % 0.18/0.60 % KSP exiting %------------------------------------------------------------------------------