%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP079_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n002.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:57 PM UTC 2026 % Result : Theorem 0.44s 0.84s % Output : Refutation 0.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP079_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.16/0.33 % Computer : n002.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:18:46 EDT 2026 % 0.16/0.34 % CPUTime : % 0.34/0.59 ----KSP format--- % 0.34/0.59 set(box,SYM). % 0.34/0.59 usable(formulas). % 0.34/0.59 true. % 0.34/0.59 end_of_list. % 0.34/0.59 sos(formulas). % 0.34/0.59 ~ (<> ( ~ ( ( [] ( ~ ( 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.34/0.59 end_of_list. % 0.34/0.59 ----------------- % 0.34/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/sandbox2/tmp/tmp.sFErnN9Xjr/theBenchmark.ksp % 0.44/0.84 % 0.44/0.84 % SZS status Theorem % 0.44/0.84 % 0.44/0.84 ***************** % 0.44/0.84 FOUND PROOF 1 % 0.44/0.84 ***************** % 0.44/0.84 % SZS output start Refutation % 0.44/0.84 % 0.44/0.84 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.44/0.84 (1,1) [738,0]. _t1 => box 1 _t2 [ SNF ] [ Backward Subsumption, 905 ] % 0.44/0.84 (1,1) [739,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 904 ] % 0.44/0.84 (449,1) [896,0]. _t55 => ~box 1~ _t56 [ SNF ] [ Backward Subsumption, 908 ] % 0.44/0.84 (1,1) [897,0]. true => _t55 | ~_t0 [ SNF ] [ Backward Subsumption, 899 ] % 0.44/0.84 (1,1) [899,0]. true => _t55 [ Unit Resolution, 3, 897, _t0 ] [ Modal Level Pure Literal Elimination, _t55 ] % 0.44/0.84 (1,1) [904,0]. true => _t1 [ Unit Resolution, 3, 739, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 0.44/0.84 (1,1) [905,0]. true => box 1 _t2 [ LHS Unit Resolution, 904, 738, _t1 ] [ SNF++, 1791, _t2 ] % 0.44/0.84 (449,1) [908,0]. true => ~box 1~ _t56 [ LHS Unit Resolution, 899, 896, _t55 ] [ SNF++, 1815, _t56 ] % 0.44/0.84 (1,1) [1791,0]. true => box 1 _t166 [ SNF++, 905 ] % 0.44/0.84 (449,1) [1815,0]. true => ~box 1~ _t167 [ SNF++, 908 ] % 0.44/0.84 (449,1) [9614,0]. true => false [ GEN1, 1791, 1815, 9601, _t166, _t167 ] % 0.44/0.84 (1,1) [728,1]. _t3 => box 1 _t4 [ SNF ] [ SNF++, 1703, _t4 ] % 0.44/0.84 (1,1) [735,1]. true => _t3 | ~_t2 [ SNF ] % 0.44/0.84 (447,1) [894,1]. _t57 => ~box 1~ _t58 [ SNF ] [ SNF++, 1729, _t58 ] % 0.44/0.84 (449,1) [895,1]. true => _t57 | ~_t56 [ SNF ] % 0.44/0.84 (1,1) [1703,1]. _t3 => box 1 _t163 [ SNF++, 728 ] % 0.44/0.84 (447,1) [1729,1]. _t57 => ~box 1~ _t164 [ SNF++, 894 ] % 0.44/0.84 (1,1) [1792,1]. true => ~_t166 | _t2 [ SNF++, 905 ] % 0.44/0.84 (449,1) [1816,1]. true => ~_t167 | _t56 [ SNF++, 908 ] % 0.44/0.84 (1,1) [2192,1]. true => ~_t166 | _t3 [ LRES, 735, 1792, ~_t2 ] % 0.44/0.84 (449,1) [2224,1]. true => ~_t167 | _t57 [ LRES, 895, 1816, ~_t56 ] % 0.44/0.84 (447,1) [9589,1]. true => ~_t57 | ~_t3 [ GEN1, 1703, 1729, 9574, _t163, _t164 ] % 0.44/0.84 (447,1) [9590,1]. true => ~_t166 | ~_t57 [ LRES, 9589, 2192, ~_t3 ] % 0.44/0.84 (449,1) [9601,1]. true => ~_t167 | ~_t166 [ LRES, 9590, 2224, ~_t57 ] % 0.44/0.84 (1,1) [712,2]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 1615, _t6 ] % 0.44/0.84 (1,1) [725,2]. true => _t5 | ~_t4 [ SNF ] % 0.44/0.84 (446,1) [892,2]. _t59 => ~box 1~ _t60 [ SNF ] [ SNF++, 1639, _t60 ] % 0.44/0.84 (447,1) [893,2]. true => _t59 | ~_t58 [ SNF ] % 0.44/0.84 (1,1) [1615,2]. _t5 => box 1 _t160 [ SNF++, 712 ] % 0.44/0.84 (446,1) [1639,2]. _t59 => ~box 1~ _t161 [ SNF++, 892 ] % 0.44/0.84 (1,1) [1704,2]. true => ~_t163 | _t4 [ SNF++, 728 ] % 0.44/0.84 (447,1) [1730,2]. true => ~_t164 | _t58 [ SNF++, 894 ] % 0.44/0.84 (1,1) [2239,2]. true => ~_t163 | _t5 [ LRES, 725, 1704, ~_t4 ] % 0.44/0.84 (447,1) [2254,2]. true => ~_t164 | _t59 [ LRES, 893, 1730, ~_t58 ] % 0.44/0.84 (446,1) [9562,2]. true => ~_t59 | ~_t5 [ GEN1, 1615, 1639, 9548, _t160, _t161 ] % 0.44/0.84 (446,1) [9563,2]. true => ~_t163 | ~_t59 [ LRES, 9562, 2239, ~_t5 ] % 0.44/0.84 (447,1) [9574,2]. true => ~_t164 | ~_t163 [ LRES, 9563, 2254, ~_t59 ] % 0.44/0.84 (1,1) [690,3]. _t7 => box 1 _t8 [ SNF ] [ SNF++, 1527, _t8 ] % 0.44/0.84 (1,1) [709,3]. true => _t7 | ~_t6 [ SNF ] % 0.44/0.84 (445,1) [890,3]. _t61 => ~box 1~ _t62 [ SNF ] [ SNF++, 1553, _t62 ] % 0.44/0.84 (446,1) [891,3]. true => _t61 | ~_t60 [ SNF ] % 0.44/0.84 (1,1) [1527,3]. _t7 => box 1 _t157 [ SNF++, 690 ] % 0.44/0.84 (445,1) [1553,3]. _t61 => ~box 1~ _t158 [ SNF++, 890 ] % 0.44/0.84 (1,1) [1616,3]. true => ~_t160 | _t6 [ SNF++, 712 ] % 0.44/0.84 (446,1) [1640,3]. true => ~_t161 | _t60 [ SNF++, 892 ] % 0.44/0.84 (1,1) [2168,3]. true => ~_t160 | _t7 [ LRES, 709, 1616, ~_t6 ] % 0.44/0.84 (446,1) [2207,3]. true => ~_t161 | _t61 [ LRES, 891, 1640, ~_t60 ] % 0.44/0.84 (445,1) [9534,3]. true => ~_t61 | ~_t7 [ GEN1, 1527, 1553, 9523, _t157, _t158 ] % 0.44/0.84 (445,1) [9535,3]. true => ~_t160 | ~_t61 [ LRES, 9534, 2168, ~_t7 ] % 0.44/0.84 (446,1) [9548,3]. true => ~_t161 | ~_t160 [ LRES, 9535, 2207, ~_t61 ] % 0.44/0.84 (1,1) [660,4]. _t9 => box 1 _t10 [ SNF ] [ SNF++, 1443, _t10 ] % 0.44/0.84 (1,1) [687,4]. true => _t9 | ~_t8 [ SNF ] % 0.44/0.84 (444,1) [888,4]. _t63 => ~box 1~ _t64 [ SNF ] [ SNF++, 1467, _t64 ] % 0.44/0.84 (445,1) [889,4]. true => _t63 | ~_t62 [ SNF ] % 0.44/0.84 (1,1) [1443,4]. _t9 => box 1 _t154 [ SNF++, 660 ] % 0.44/0.84 (444,1) [1467,4]. _t63 => ~box 1~ _t155 [ SNF++, 888 ] % 0.44/0.84 (1,1) [1528,4]. true => ~_t157 | _t8 [ SNF++, 690 ] % 0.44/0.84 (445,1) [1554,4]. true => ~_t158 | _t62 [ SNF++, 890 ] % 0.44/0.84 (1,1) [2206,4]. true => ~_t157 | _t9 [ LRES, 687, 1528, ~_t8 ] % 0.44/0.84 (445,1) [2230,4]. true => ~_t158 | _t63 [ LRES, 889, 1554, ~_t62 ] % 0.44/0.84 (444,1) [9512,4]. true => ~_t63 | ~_t9 [ GEN1, 1443, 1467, 9502, _t154, _t155 ] % 0.44/0.84 (444,1) [9513,4]. true => ~_t157 | ~_t63 [ LRES, 9512, 2206, ~_t9 ] % 0.44/0.84 (445,1) [9523,4]. true => ~_t158 | ~_t157 [ LRES, 9513, 2230, ~_t63 ] % 0.44/0.84 (1,1) [583,5]. _t11 => box 1 _t12 [ SNF ] [ SNF++, 1359, _t12 ] % 0.44/0.84 (1,1) [657,5]. true => _t11 | ~_t10 [ SNF ] % 0.44/0.84 (443,1) [886,5]. _t65 => ~box 1~ _t66 [ SNF ] [ SNF++, 1385, _t66 ] % 0.44/0.84 (444,1) [887,5]. true => _t65 | ~_t64 [ SNF ] % 0.44/0.84 (1,1) [1359,5]. _t11 => box 1 _t151 [ SNF++, 583 ] % 0.44/0.84 (443,1) [1385,5]. _t65 => ~box 1~ _t152 [ SNF++, 886 ] % 0.44/0.84 (1,1) [1444,5]. true => ~_t154 | _t10 [ SNF++, 660 ] % 0.44/0.84 (444,1) [1468,5]. true => ~_t155 | _t64 [ SNF++, 888 ] % 0.44/0.84 (1,1) [2121,5]. true => ~_t154 | _t11 [ LRES, 657, 1444, ~_t10 ] % 0.44/0.84 (444,1) [2155,5]. true => ~_t155 | _t65 [ LRES, 887, 1468, ~_t64 ] % 0.44/0.84 (443,1) [9491,5]. true => ~_t65 | ~_t11 [ GEN1, 1359, 1385, 9464, _t151, _t152 ] % 0.44/0.84 (443,1) [9492,5]. true => ~_t154 | ~_t65 [ LRES, 9491, 2121, ~_t11 ] % 0.44/0.84 (444,1) [9502,5]. true => ~_t155 | ~_t154 [ LRES, 9492, 2155, ~_t65 ] % 0.44/0.84 (1,1) [460,6]. _t13 => box 1 _t14 [ SNF ] [ SNF++, 1279, _t14 ] % 0.44/0.84 (1,1) [580,6]. true => _t13 | ~_t12 [ SNF ] % 0.44/0.84 (442,1) [884,6]. _t67 => ~box 1~ _t68 [ SNF ] [ SNF++, 1303, _t68 ] % 0.44/0.84 (443,1) [885,6]. true => _t67 | ~_t66 [ SNF ] % 0.44/0.84 (1,1) [1279,6]. _t13 => box 1 _t148 [ SNF++, 460 ] % 0.44/0.84 (442,1) [1303,6]. _t67 => ~box 1~ _t149 [ SNF++, 884 ] % 0.44/0.84 (1,1) [1360,6]. true => ~_t151 | _t12 [ SNF++, 583 ] % 0.44/0.84 (443,1) [1386,6]. true => ~_t152 | _t66 [ SNF++, 886 ] % 0.44/0.84 (1,1) [2154,6]. true => ~_t151 | _t13 [ LRES, 580, 1360, ~_t12 ] % 0.44/0.84 (443,1) [2186,6]. true => ~_t152 | _t67 [ LRES, 885, 1386, ~_t66 ] % 0.44/0.84 (442,1) [9449,6]. true => ~_t67 | ~_t13 [ GEN1, 1279, 1303, 9426, _t148, _t149 ] % 0.44/0.84 (442,1) [9450,6]. true => ~_t151 | ~_t67 [ LRES, 9449, 2154, ~_t13 ] % 0.44/0.84 (443,1) [9464,6]. true => ~_t152 | ~_t151 [ LRES, 9450, 2186, ~_t67 ] % 0.44/0.84 (1,1) [343,7]. _t15 => box 1 _t16 [ SNF ] [ SNF++, 1199, _t16 ] % 0.44/0.84 (1,1) [457,7]. true => _t15 | ~_t14 [ SNF ] % 0.44/0.84 (441,1) [882,7]. _t69 => ~box 1~ _t70 [ SNF ] [ SNF++, 1225, _t70 ] % 0.44/0.84 (442,1) [883,7]. true => _t69 | ~_t68 [ SNF ] % 0.44/0.84 (1,1) [1199,7]. _t15 => box 1 _t145 [ SNF++, 343 ] % 0.44/0.84 (441,1) [1225,7]. _t69 => ~box 1~ _t146 [ SNF++, 882 ] % 0.44/0.84 (1,1) [1280,7]. true => ~_t148 | _t14 [ SNF++, 460 ] % 0.44/0.84 (442,1) [1304,7]. true => ~_t149 | _t68 [ SNF++, 884 ] % 0.44/0.84 (1,1) [2066,7]. true => ~_t148 | _t15 [ LRES, 457, 1280, ~_t14 ] % 0.44/0.84 (442,1) [2097,7]. true => ~_t149 | _t69 [ LRES, 883, 1304, ~_t68 ] % 0.44/0.84 (441,1) [9409,7]. true => ~_t69 | ~_t15 [ GEN1, 1199, 1225, 9393, _t145, _t146 ] % 0.44/0.84 (441,1) [9410,7]. true => ~_t148 | ~_t69 [ LRES, 9409, 2066, ~_t15 ] % 0.44/0.84 (442,1) [9426,7]. true => ~_t149 | ~_t148 [ LRES, 9410, 2097, ~_t69 ] % 0.44/0.84 (1,1) [204,8]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 1109, _t18 ] % 0.44/0.84 (1,1) [286,8]. true => _t17 | ~_t16 [ SNF ] % 0.44/0.84 (440,1) [880,8]. _t71 => ~box 1~ _t72 [ SNF ] [ SNF++, 1147, _t72 ] % 0.44/0.84 (441,1) [881,8]. true => _t71 | ~_t70 [ SNF ] % 0.44/0.84 (1,1) [1109,8]. _t17 => box 1 _t141 [ SNF++, 204 ] % 0.44/0.84 (440,1) [1147,8]. _t71 => ~box 1~ _t143 [ SNF++, 880 ] % 0.44/0.84 (1,1) [1200,8]. true => ~_t145 | _t16 [ SNF++, 343 ] % 0.44/0.84 (441,1) [1226,8]. true => ~_t146 | _t70 [ SNF++, 882 ] % 0.44/0.84 (1,1) [2096,8]. true => ~_t145 | _t17 [ LRES, 286, 1200, ~_t16 ] % 0.44/0.84 (441,1) [2132,8]. true => ~_t146 | _t71 [ LRES, 881, 1226, ~_t70 ] % 0.44/0.84 (440,1) [9376,8]. true => ~_t71 | ~_t17 [ GEN1, 1109, 1147, 9363, _t141, _t143 ] % 0.44/0.84 (440,1) [9377,8]. true => ~_t145 | ~_t71 [ LRES, 9376, 2096, ~_t17 ] % 0.44/0.84 (441,1) [9393,8]. true => ~_t146 | ~_t145 [ LRES, 9377, 2132, ~_t71 ] % 0.44/0.84 (1,1) [97,9]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 1017, _t20 ] % 0.44/0.84 (1,1) [147,9]. true => _t19 | ~_t18 [ SNF ] % 0.44/0.84 (436,1) [873,9]. _t73 => ~box 1~ _t74 [ SNF ] [ SNF++, 1067, _t74 ] % 0.44/0.84 (440,1) [874,9]. true => _t73 | ~_t72 [ SNF ] % 0.44/0.84 (1,1) [1017,9]. _t19 => box 1 _t128 [ SNF++, 97 ] % 0.44/0.84 (436,1) [1067,9]. _t73 => ~box 1~ _t136 [ SNF++, 873 ] % 0.44/0.84 (1,1) [1110,9]. true => ~_t141 | _t18 [ SNF++, 204 ] % 0.44/0.84 (440,1) [1148,9]. true => ~_t143 | _t72 [ SNF++, 880 ] % 0.44/0.84 (1,1) [1950,9]. true => ~_t141 | _t19 [ LRES, 147, 1110, ~_t18 ] % 0.44/0.84 (440,1) [2045,9]. true => ~_t143 | _t73 [ LRES, 874, 1148, ~_t72 ] % 0.44/0.84 (436,1) [9350,9]. true => ~_t73 | ~_t19 [ GEN1, 1017, 1067, 9337, _t128, _t136 ] % 0.44/0.84 (436,1) [9351,9]. true => ~_t141 | ~_t73 [ LRES, 9350, 1950, ~_t19 ] % 0.44/0.84 (440,1) [9363,9]. true => ~_t143 | ~_t141 [ LRES, 9351, 2045, ~_t73 ] % 0.44/0.84 (1,1) [8,10]. _t21 => box 1 _t22 [ SNF ] [ SNF++, 949, _t22 ] % 0.44/0.84 (1,1) [15,10]. true => _t21 | ~_t20 [ SNF ] % 0.44/0.84 (1,1) [29,10]. _t25 => box 1 _t26 [ SNF ] [ SNF++, 951, _t26 ] % 0.44/0.84 (1,1) [38,10]. true => _t25 | ~_t20 [ SNF ] % 0.44/0.84 (17,1) [48,10]. _t27 => ~box 1~ _t28 [ SNF ] [ SNF++, 987, _t28 ] % 0.44/0.84 (1,1) [54,10]. _t30 => box 1 _t31 [ SNF ] [ SNF++, 961, _t31 ] % 0.44/0.84 (1,1) [71,10]. true => _t30 | ~_t20 [ SNF ] % 0.44/0.84 (1,1) [77,10]. _t77 => box 1 ~_t21 [ Axiom SYM ] [ SNF++, 963, ~_t21 ] % 0.44/0.84 (24,1) [81,10]. _t22 => ~box 1~ _t23 [ SNF ] [ SNF++, 989, _t23 ] % 0.44/0.84 (1,1) [82,10]. true => _t77 | _t22 [ Axiom SYM ] % 0.44/0.84 (1,1) [83,10]. _t35 => box 1 _t21 [ SNF ] [ SNF++, 965, _t21 ] % 0.44/0.84 (1,1) [93,10]. true => _t35 | ~_t34 | _t27 [ SNF ] % 0.44/0.84 (1,1) [94,10]. true => _t34 | ~_t20 [ SNF ] % 0.44/0.84 (1,1) [95,10]. true => ~_t36 | _t27 | _t22 [ SNF ] % 0.44/0.84 (1,1) [96,10]. true => _t36 | ~_t20 [ SNF ] % 0.44/0.84 (1,1) [869,10]. _t74 => box 1 _t75 [ SNF ] [ SNF++, 985, _t75 ] % 0.44/0.84 (1,1) [949,10]. _t21 => box 1 _t106 [ SNF++, 8 ] % 0.44/0.84 (1,1) [951,10]. _t25 => box 1 _t114 [ SNF++, 29 ] % 0.44/0.84 (1,1) [961,10]. _t30 => box 1 _t117 [ SNF++, 54 ] % 0.44/0.84 (1,1) [963,10]. _t77 => box 1 _t110 [ SNF++, 77 ] % 0.44/0.84 (1,1) [965,10]. _t35 => box 1 _t108 [ SNF++, 83 ] % 0.44/0.84 (1,1) [985,10]. _t74 => box 1 _t124 [ SNF++, 869 ] % 0.44/0.84 (17,1) [987,10]. _t27 => ~box 1~ _t103 [ SNF++, 48 ] % 0.44/0.84 (24,1) [989,10]. _t22 => ~box 1~ _t104 [ SNF++, 81 ] % 0.44/0.84 (1,1) [1018,10]. true => ~_t128 | _t20 [ SNF++, 97 ] % 0.44/0.84 (436,1) [1068,10]. true => ~_t136 | _t74 [ SNF++, 873 ] % 0.44/0.84 (1,1) [1835,10]. true => ~_t128 | _t36 [ LRES, 96, 1018, ~_t20 ] % 0.44/0.84 (1,1) [1850,10]. true => ~_t128 | _t34 [ LRES, 94, 1018, ~_t20 ] % 0.44/0.84 (1,1) [1868,10]. true => ~_t128 | _t30 [ LRES, 71, 1018, ~_t20 ] % 0.44/0.84 (1,1) [1887,10]. true => ~_t128 | _t25 [ LRES, 38, 1018, ~_t20 ] % 0.44/0.84 (1,1) [1907,10]. true => ~_t128 | _t21 [ LRES, 15, 1018, ~_t20 ] % 0.44/0.84 (1,1) [2151,10]. true => ~_t77 | ~_t35 | ~_t22 [ GEN3, 963, 965, 1974, 989, _t110, _t108, _t104 ] % 0.44/0.84 (1,1) [2152,10]. true => ~_t77 | ~_t35 | ~_t27 [ GEN3, 963, 965, 1974, 987, _t110, _t108, _t103 ] % 0.44/0.84 (17,1) [2379,10]. true => ~_t27 | ~_t21 [ GEN1, 949, 987, 2300, _t106, _t103 ] % 0.44/0.84 (17,1) [2846,10]. true => ~_t128 | ~_t27 [ LRES, 2379, 1907, ~_t21 ] % 0.44/0.84 (17,1) [2895,10]. true => ~_t128 | _t35 | ~_t34 [ LRES, 2846, 93, ~_t27 ] [ Backward Subsumption, 5104 ] % 0.44/0.84 (1,1) [3694,10]. true => ~_t77 | ~_t36 | ~_t35 | _t27 [ LRES, 2151, 95, ~_t22 ] [ Backward Subsumption, 6672 ] % 0.44/0.84 (24,1) [4749,10]. true => ~_t74 | ~_t30 | ~_t25 | ~_t22 [ GEN1, 985, 951, 961, 989, 4726, _t124, _t114, _t117, _t104 ] % 0.44/0.84 (17,1) [5104,10]. true => ~_t128 | _t35 [ LRES, 2895, 1850, ~_t34 ] % 0.44/0.84 (24,1) [6147,10]. true => _t77 | ~_t74 | ~_t30 | ~_t25 [ LRES, 4749, 82, ~_t22 ] % 0.44/0.84 (1,1) [6672,10]. true => ~_t77 | ~_t36 | ~_t35 [ LRES, 3694, 2152, _t27 ] % 0.44/0.84 (17,1) [6701,10]. true => ~_t128 | ~_t77 | ~_t36 [ LRES, 6672, 5104, ~_t35 ] [ Backward Subsumption, 6722 ] % 0.44/0.84 (17,1) [6722,10]. true => ~_t128 | ~_t77 [ LRES, 6701, 1835, ~_t36 ] % 0.44/0.84 (24,1) [7486,10]. true => ~_t128 | _t77 | ~_t74 | ~_t30 [ LRES, 6147, 1887, ~_t25 ] [ Backward Subsumption, 9315 ] % 0.44/0.84 (24,1) [9315,10]. true => ~_t128 | _t77 | ~_t74 [ LRES, 7486, 1868, ~_t30 ] % 0.44/0.84 (436,1) [9326,10]. true => ~_t136 | ~_t128 | _t77 [ LRES, 9315, 1068, ~_t74 ] [ Backward Subsumption, 9337 ] % 0.44/0.84 (436,1) [9337,10]. true => ~_t136 | ~_t128 [ LRES, 9326, 6722, _t77 ] % 0.44/0.84 (6,1) [7,11]. _t22 => ~box 1~ _t23 [ SNF ] [ SNF++, 921, _t23 ] % 0.44/0.84 (1,1) [17,11]. _t78 => box 1 ~_t28 [ Axiom SYM ] [ SNF++, 931, ~_t28 ] % 0.44/0.84 (1,1) [18,11]. true => _t78 | ~p0 [ Axiom SYM ] % 0.44/0.84 (8,1) [19,11]. _t27 => ~box 1~ _t28 [ SNF ] [ SNF++, 923, _t28 ] % 0.44/0.84 (1,1) [25,11]. _t77 => box 1 ~_t21 [ Axiom SYM ] [ SNF++, 933, ~_t21 ] % 0.44/0.84 (1,1) [26,11]. true => _t77 | _t22 [ Axiom SYM ] % 0.44/0.84 (15,1) [27,11]. _t29 => ~box 1~ _t21 [ SNF ] [ SNF++, 925, _t21 ] % 0.44/0.84 (1,1) [28,11]. true => _t29 | _t27 | ~_t26 [ SNF ] % 0.44/0.84 (1,1) [43,11]. _t32 => box 1 _t27 [ SNF ] [ SNF++, 935, _t27 ] % 0.44/0.84 (1,1) [45,11]. _t28 => box 1 ~p0 [ SNF ] [ SNF++, 937, ~p0 ] % 0.44/0.84 (1,1) [50,11]. _t33 => box 1 _t23 [ SNF ] [ SNF++, 939, _t23 ] % 0.44/0.84 (1,1) [53,11]. true => _t33 | _t32 | ~_t31 | ~p0 [ SNF ] % 0.44/0.84 (24,1) [78,11]. true => ~_t23 | p0 [ SNF ] % 0.44/0.84 (435,1) [868,11]. _t75 => ~box 1~ ~p0 [ SNF ] [ SNF++, 929, ~p0 ] % 0.44/0.84 (6,1) [921,11]. _t22 => ~box 1~ _t104 [ SNF++, 7 ] % 0.44/0.84 (8,1) [923,11]. _t27 => ~box 1~ _t103 [ SNF++, 19 ] % 0.44/0.84 (15,1) [925,11]. _t29 => ~box 1~ _t108 [ SNF++, 27 ] % 0.44/0.84 (435,1) [929,11]. _t75 => ~box 1~ _t105 [ SNF++, 868 ] % 0.44/0.84 (1,1) [931,11]. _t78 => box 1 _t107 [ SNF++, 17 ] % 0.44/0.84 (1,1) [933,11]. _t77 => box 1 _t110 [ SNF++, 25 ] % 0.44/0.84 (1,1) [935,11]. _t32 => box 1 _t111 [ SNF++, 43 ] % 0.44/0.84 (1,1) [937,11]. _t28 => box 1 _t105 [ SNF++, 45 ] % 0.44/0.84 (1,1) [939,11]. _t33 => box 1 _t104 [ SNF++, 50 ] % 0.44/0.84 (1,1) [950,11]. true => ~_t106 | _t22 [ SNF++, 8 ] % 0.44/0.84 (1,1) [952,11]. true => ~_t114 | _t26 [ SNF++, 29 ] % 0.44/0.84 (1,1) [962,11]. true => ~_t117 | _t31 [ SNF++, 54 ] % 0.44/0.84 (1,1) [964,11]. true => ~_t110 | ~_t21 [ SNF++, 77 ] % 0.44/0.84 (1,1) [966,11]. true => ~_t108 | _t21 [ SNF++, 83 ] % 0.44/0.84 (1,1) [986,11]. true => ~_t124 | _t75 [ SNF++, 869 ] % 0.44/0.84 (17,1) [988,11]. true => ~_t103 | _t28 [ SNF++, 48 ] % 0.44/0.84 (24,1) [990,11]. true => ~_t104 | _t23 [ SNF++, 81 ] % 0.44/0.84 (24,1) [1837,11]. true => _t78 | ~_t23 [ LRES, 18, 78, ~p0 ] % 0.44/0.84 (24,1) [1852,11]. true => ~_t104 | _t78 [ LRES, 1837, 990, ~_t23 ] % 0.44/0.84 (1,1) [1974,11]. true => ~_t110 | ~_t108 [ LRES, 964, 966, ~_t21 ] % 0.44/0.84 (8,1) [1993,11]. true => ~_t78 | ~_t27 [ GEN1, 931, 923, 1867, _t107, _t103 ] % 0.44/0.84 (15,1) [2017,11]. true => ~_t77 | ~_t29 [ GEN1, 933, 925, 1886, _t110, _t108 ] % 0.44/0.84 (6,1) [2115,11]. true => ~_t28 | ~_t22 [ GEN1, 937, 921, 1969, _t105, _t104 ] % 0.44/0.84 (435,1) [2116,11]. true => ~_t75 | ~_t33 [ GEN1, 939, 929, 1969, _t104, _t105 ] % 0.44/0.84 (6,1) [2199,11]. true => ~_t32 | ~_t22 [ GEN1, 935, 921, 2143, _t111, _t104 ] % 0.44/0.84 (6,1) [2247,11]. true => _t77 | ~_t32 [ LRES, 2199, 26, ~_t22 ] % 0.44/0.84 (6,1) [2259,11]. true => ~_t106 | ~_t28 [ LRES, 2115, 950, ~_t22 ] % 0.44/0.84 (17,1) [2300,11]. true => ~_t106 | ~_t103 [ LRES, 2259, 988, ~_t28 ] % 0.44/0.84 (1,1) [2392,11]. true => ~_t114 | _t29 | _t27 [ LRES, 28, 952, ~_t26 ] % 0.44/0.84 (8,1) [2850,11]. true => ~_t114 | ~_t78 | _t29 [ LRES, 2392, 1993, _t27 ] % 0.44/0.84 (15,1) [3045,11]. true => ~_t114 | ~_t78 | ~_t77 [ LRES, 2850, 2017, _t29 ] % 0.44/0.84 (24,1) [3530,11]. true => _t33 | _t32 | ~_t31 | ~_t23 [ LRES, 53, 78, ~p0 ] % 0.44/0.84 (24,1) [3923,11]. true => ~_t104 | _t33 | _t32 | ~_t31 [ LRES, 3530, 990, ~_t23 ] % 0.44/0.84 (24,1) [4112,11]. true => ~_t117 | ~_t104 | _t33 | _t32 [ LRES, 3923, 962, ~_t31 ] % 0.44/0.84 (24,1) [4149,11]. true => ~_t117 | ~_t104 | _t77 | _t33 [ LRES, 4112, 2247, _t32 ] % 0.44/0.84 (435,1) [4253,11]. true => ~_t117 | ~_t104 | _t77 | ~_t75 [ LRES, 4149, 2116, _t33 ] % 0.44/0.84 (435,1) [4294,11]. true => ~_t124 | ~_t117 | ~_t104 | _t77 [ LRES, 4253, 986, ~_t75 ] % 0.44/0.84 (435,1) [4457,11]. true => ~_t124 | ~_t117 | ~_t114 | ~_t104 | ~_t78 [ LRES, 4294, 3045, _t77 ] [ Backward Subsumption, 4726 ] % 0.44/0.84 (435,1) [4726,11]. true => ~_t124 | ~_t117 | ~_t114 | ~_t104 [ LRES, 4457, 1852, ~_t78 ] % 0.44/0.84 (6,1) [4,12]. true => ~_t23 | p0 [ SNF ] % 0.44/0.84 (1,1) [40,12]. _t78 => box 1 ~_t28 [ Axiom SYM ] [ SNF++, 919, ~_t28 ] % 0.44/0.84 (1,1) [41,12]. true => _t78 | ~p0 [ Axiom SYM ] % 0.44/0.84 (17,1) [42,12]. _t27 => ~box 1~ _t28 [ SNF ] [ SNF++, 911, _t28 ] % 0.44/0.84 (17,1) [911,12]. _t27 => ~box 1~ _t103 [ SNF++, 42 ] % 0.44/0.84 (1,1) [919,12]. _t78 => box 1 _t107 [ SNF++, 40 ] % 0.44/0.84 (6,1) [922,12]. true => ~_t104 | _t23 [ SNF++, 7 ] % 0.44/0.84 (8,1) [924,12]. true => ~_t103 | _t28 [ SNF++, 19 ] % 0.44/0.84 (15,1) [926,12]. true => ~_t108 | _t21 [ SNF++, 27 ] % 0.44/0.84 (435,1) [930,12]. true => ~_t105 | ~p0 [ SNF++, 868 ] % 0.44/0.84 (1,1) [932,12]. true => ~_t107 | ~_t28 [ SNF++, 17 ] % 0.44/0.84 (1,1) [934,12]. true => ~_t110 | ~_t21 [ SNF++, 25 ] % 0.44/0.84 (1,1) [936,12]. true => ~_t111 | _t27 [ SNF++, 43 ] % 0.44/0.84 (435,1) [1834,12]. true => ~_t105 | ~_t23 [ LRES, 930, 4, ~p0 ] % 0.44/0.84 (6,1) [1849,12]. true => _t78 | ~_t23 [ LRES, 41, 4, ~p0 ] % 0.44/0.84 (8,1) [1867,12]. true => ~_t107 | ~_t103 [ LRES, 932, 924, ~_t28 ] % 0.44/0.84 (15,1) [1886,12]. true => ~_t110 | ~_t108 [ LRES, 934, 926, ~_t21 ] % 0.44/0.84 (17,1) [1911,12]. true => ~_t78 | ~_t27 [ GEN1, 919, 911, 1855, _t107, _t103 ] % 0.44/0.84 (6,1) [1948,12]. true => ~_t104 | _t78 [ LRES, 1849, 922, ~_t23 ] % 0.44/0.84 (435,1) [1969,12]. true => ~_t105 | ~_t104 [ LRES, 1834, 922, ~_t23 ] % 0.44/0.84 (17,1) [2063,12]. true => ~_t111 | ~_t78 [ LRES, 1911, 936, ~_t27 ] % 0.44/0.84 (17,1) [2143,12]. true => ~_t111 | ~_t104 [ LRES, 2063, 1948, ~_t78 ] % 0.44/0.84 (17,1) [912,13]. true => ~_t103 | _t28 [ SNF++, 42 ] % 0.44/0.84 (1,1) [920,13]. true => ~_t107 | ~_t28 [ SNF++, 40 ] % 0.44/0.84 (17,1) [1855,13]. true => ~_t107 | ~_t103 [ LRES, 920, 912, ~_t28 ] % 0.44/0.84 % SZS output end Refutation % 0.44/0.84 % KSP exiting %------------------------------------------------------------------------------