%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP069_1 : TPTP v9.3.0. Released v9.3.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 : Tue May 5 07:12:57 PM UTC 2026 % Result : Theorem 0.42s 0.73s % Output : Refutation 0.42s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SYP069_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.11 % Command : run_ksp %s % 0.12/0.31 % Computer : n023.cluster.edu % 0.12/0.31 % Model : x86_64 x86_64 % 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.31 % Memory : 8042.1875MB % 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.31 % CPULimit : 300 % 0.12/0.31 % WCLimit : 300 % 0.12/0.31 % DateTime : Mon May 4 17:09:08 EDT 2026 % 0.12/0.31 % CPUTime : % 0.39/0.56 ----KSP format--- % 0.39/0.56 set(box,SYM). % 0.39/0.56 usable(formulas). % 0.39/0.56 true. % 0.39/0.56 end_of_list. % 0.39/0.56 sos(formulas). % 0.39/0.56 ~ (( [] ( ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> p2 ) ) & ( [] ( ( [] ( ( ( [] ( $false ) | p1 ) -> [] ( [] ( $false ) | p1 ) ) ) -> ( [] ( $false ) | p1 ) ) ) -> ( [] ( $false ) | p1 ) ) & ( [] ( ( [] ( ( ( [] ( $false ) | p1 | p2 ) -> [] ( [] ( $false ) | p1 | p2 ) ) ) -> ( [] ( $false ) | p1 | p2 ) ) ) -> ( [] ( $false ) | p1 | p2 ) ) & ( [] ( ( [] ( ( ( [] ( $false ) | p1 | p2 | p3 ) -> [] ( [] ( $false ) | p1 | p2 | p3 ) ) ) -> ( [] ( $false ) | p1 | p2 | p3 ) ) ) -> ( [] ( $false ) | p1 | p2 | p3 ) ) & ( [] ( ( [] ( ( ( [] ( $false ) | p1 | p2 | p3 | p4 ) -> [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) ) ) -> ( [] ( $false ) | p1 | p2 | p3 | p4 ) ) ) -> ( [] ( $false ) | p1 | p2 | p3 | p4 ) ) & ( [] ( ( [] ( ( ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 ) -> [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 ) ) & ( [] ( ( [] ( ( ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 ) -> [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 ) ) & ( [] ( ( [] ( ( ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 ) -> [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 ) ) & ( [] ( ( [] ( ( ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) -> [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) ) & ( [] ( ( [] ( ( ( [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) | p1 ) -> [] ( [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) | p1 ) ) ) -> ( [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) | p1 ) ) ) -> ( [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) | p1 ) ) & ( [] ( ( [] ( ( ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) & ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> [] ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) ) ) ) -> [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) & ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> [] ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) ) ) ) ) ) -> ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) & ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> [] ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) ) ) ) ) ) -> ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) & ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> [] ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) ) ) ) ) ) -> ( ( [] ( ( [] ( ( p1 -> [] ( p1 ) ) ) -> p1 ) ) -> [] ( p1 ) ) | ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> [] ( p2 ) ) | ( [] ( ( [] ( ( p3 -> [] ( p3 ) ) ) -> p3 ) ) -> [] ( p3 ) ) ) ). % 0.39/0.56 end_of_list. % 0.39/0.56 ----------------- % 0.39/0.56 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.SU1TiStZ4u/theBenchmark.ksp % 0.42/0.73 % 0.42/0.73 % SZS status Theorem % 0.42/0.73 % 0.42/0.73 ***************** % 0.42/0.73 FOUND PROOF 1 % 0.42/0.73 ***************** % 0.42/0.73 % SZS output start Refutation % 0.42/0.73 % 0.42/0.73 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.42/0.73 (1,1) [19,0]. _t1 => box 1 _t2 [ SNF ] [ Backward Subsumption, 478 ] % 0.42/0.73 (1,1) [20,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 475 ] % 0.42/0.73 (1,1) [40,0]. _t18 => box 1 _t19 [ SNF ] [ Backward Subsumption, 486 ] % 0.42/0.73 (1,1) [41,0]. true => _t18 | ~_t0 [ SNF ] [ Backward Subsumption, 472 ] % 0.42/0.73 (24,1) [46,0]. _t22 => ~box 1~ ~p2 [ SNF ] [ Backward Subsumption, 492 ] % 0.42/0.73 (1,1) [47,0]. true => _t22 | ~_t0 [ SNF ] [ Backward Subsumption, 469 ] % 0.42/0.73 (77,1) [144,0]. _t24 => ~box 1~ _t25 [ SNF ] [ SNF++, 774, _t25 ] % 0.42/0.73 (1,1) [146,0]. _t31 => box 1 _t18 [ SNF ] [ SNF++, 720, _t18 ] % 0.42/0.73 (89,1) [147,0]. _t3 => ~box 1~ _t4 [ SNF ] [ SNF++, 776, _t4 ] % 0.42/0.73 (1,1) [148,0]. true => _t31 | ~_t30 | _t3 [ SNF ] [ Backward Subsumption, 2991 ] % 0.42/0.73 (1,1) [149,0]. true => _t30 | ~_t29 [ SNF ] [ Backward Subsumption, 5814 ] % 0.42/0.73 (1,1) [150,0]. true => _t29 | _t24 | ~_t23 [ SNF ] [ Backward Subsumption, 481 ] % 0.42/0.73 (1,1) [151,0]. true => _t23 | ~_t0 [ SNF ] [ Backward Subsumption, 468 ] % 0.42/0.73 (1,1) [468,0]. true => _t23 [ Unit Resolution, 3, 151, _t0 ] [ Modal Level Pure Literal Elimination, _t23 ] % 0.42/0.73 (1,1) [469,0]. true => _t22 [ Unit Resolution, 3, 47, _t0 ] [ Modal Level Pure Literal Elimination, _t22 ] % 0.42/0.73 (1,1) [472,0]. true => _t18 [ Unit Resolution, 3, 41, _t0 ] [ Modal Level Pure Literal Elimination, _t18 ] % 0.42/0.73 (1,1) [475,0]. true => _t1 [ Unit Resolution, 3, 20, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 0.42/0.73 (1,1) [478,0]. true => box 1 _t2 [ LHS Unit Resolution, 475, 19, _t1 ] [ SNF++, 700, _t2 ] % 0.42/0.73 (1,1) [481,0]. true => _t29 | _t24 [ Unit Resolution, 468, 150, _t23 ] [ Backward Subsumption, 5824 ] % 0.42/0.73 (1,1) [486,0]. true => box 1 _t19 [ LHS Unit Resolution, 472, 40, _t18 ] [ SNF++, 706, _t19 ] % 0.42/0.73 (24,1) [492,0]. true => ~box 1~ ~p2 [ LHS Unit Resolution, 469, 46, _t22 ] [ SNF++, 768, ~p2 ] % 0.42/0.73 (1,1) [700,0]. true => box 1 _t186 [ SNF++, 478 ] % 0.42/0.73 (1,1) [706,0]. true => box 1 _t152 [ SNF++, 486 ] % 0.42/0.73 (1,1) [720,0]. _t31 => box 1 _t139 [ SNF++, 146 ] [ Backward Subsumption, 5812 ] % 0.42/0.73 (24,1) [768,0]. true => ~box 1~ _t149 [ SNF++, 492 ] % 0.42/0.73 (77,1) [774,0]. _t24 => ~box 1~ _t199 [ SNF++, 144 ] [ Backward Subsumption, 5825 ] % 0.42/0.73 (89,1) [776,0]. _t3 => ~box 1~ _t148 [ SNF++, 147 ] [ Backward Subsumption, 2992 ] % 0.42/0.73 (89,1) [2990,0]. true => ~_t3 [ GEN1, 706, 776, 2981, _t152, _t148 ] [ Modal Level Pure Literal Elimination, ~_t3 ] % 0.42/0.73 (89,1) [2991,0]. true => _t31 | ~_t30 [ Unit Resolution, 2990, 148, _t3 ] [ Backward Subsumption, 5811 ] % 0.42/0.73 (24,1) [5809,0]. true => ~_t31 [ GEN1, 700, 720, 768, 3590, _t186, _t139, _t149 ] [ Modal Level Pure Literal Elimination, ~_t31 ] % 0.42/0.73 (89,1) [5811,0]. true => ~_t30 [ Unit Resolution, 5809, 2991, _t31 ] [ Modal Level Pure Literal Elimination, ~_t30 ] % 0.42/0.73 (89,1) [5814,0]. true => ~_t29 [ Unit Resolution, 5811, 149, _t30 ] [ Modal Level Pure Literal Elimination, ~_t29 ] % 0.42/0.73 (89,1) [5824,0]. true => _t24 [ Unit Resolution, 5814, 481, _t29 ] [ Modal Level Pure Literal Elimination, _t24 ] % 0.42/0.73 (77,1) [5825,0]. true => ~box 1~ _t199 [ LHS Unit Resolution, 5824, 774, _t24 ] % 0.42/0.73 (77,1) [6344,0]. true => false [ GEN1, 706, 5825, 6343, _t152, _t199 ] % 0.42/0.73 (3,1) [17,1]. _t3 => ~box 1~ _t4 [ SNF ] [ SNF++, 682, _t4 ] % 0.42/0.73 (1,1) [18,1]. true => _t3 | ~_t2 | p2 [ SNF ] % 0.42/0.73 (18,1) [38,1]. _t20 => ~box 1~ _t21 [ SNF ] [ SNF++, 688, _t21 ] % 0.42/0.73 (1,1) [39,1]. true => _t20 | ~_t19 | p2 [ SNF ] % 0.42/0.73 (1,1) [93,1]. _t26 => box 1 _t27 [ SNF ] [ SNF++, 632, _t27 ] % 0.42/0.73 (77,1) [104,1]. true => _t26 | ~_t25 [ SNF ] % 0.42/0.73 (1,1) [110,1]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 634, _t19 ] % 0.42/0.73 (77,1) [118,1]. true => ~_t32 | _t18 [ SNF ] % 0.42/0.73 (76,1) [133,1]. _t33 => ~box 1~ _t3 [ SNF ] [ SNF++, 692, _t3 ] % 0.42/0.73 (77,1) [134,1]. true => _t33 | ~_t32 [ SNF ] % 0.42/0.73 (77,1) [135,1]. true => ~_t4 | ~p2 [ SNF ] % 0.42/0.73 (1,1) [136,1]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 638, _t6 ] % 0.42/0.73 (77,1) [141,1]. true => _t5 | ~_t4 [ SNF ] % 0.42/0.73 (77,1) [142,1]. true => ~_t34 | _t32 | _t4 [ SNF ] % 0.42/0.73 (77,1) [143,1]. true => _t34 | ~_t25 [ SNF ] % 0.42/0.73 (1,1) [632,1]. _t26 => box 1 _t167 [ SNF++, 93 ] % 0.42/0.73 (1,1) [634,1]. _t18 => box 1 _t152 [ SNF++, 110 ] % 0.42/0.73 (1,1) [638,1]. _t5 => box 1 _t142 [ SNF++, 136 ] % 0.42/0.73 (3,1) [682,1]. _t3 => ~box 1~ _t148 [ SNF++, 17 ] % 0.42/0.73 (18,1) [688,1]. _t20 => ~box 1~ _t147 [ SNF++, 38 ] % 0.42/0.73 (76,1) [692,1]. _t33 => ~box 1~ _t164 [ SNF++, 133 ] % 0.42/0.73 (1,1) [701,1]. true => ~_t186 | _t2 [ SNF++, 478 ] % 0.42/0.73 (1,1) [707,1]. true => ~_t152 | _t19 [ SNF++, 486 ] % 0.42/0.73 (1,1) [721,1]. true => ~_t139 | _t18 [ SNF++, 146 ] [ Modal Level Pure Literal Elimination, ~_t139 ] % 0.42/0.73 (24,1) [769,1]. true => ~_t149 | ~p2 [ SNF++, 492 ] % 0.42/0.73 (77,1) [775,1]. true => ~_t199 | _t25 [ SNF++, 144 ] % 0.42/0.73 (89,1) [777,1]. true => ~_t148 | _t4 [ SNF++, 147 ] [ Modal Level Pure Literal Elimination, ~_t148 ] % 0.42/0.73 (24,1) [833,1]. true => ~_t149 | _t3 | ~_t2 [ LRES, 769, 18, ~p2 ] % 0.42/0.73 (77,1) [1118,1]. true => _t20 | ~_t19 | ~_t4 [ LRES, 135, 39, ~p2 ] % 0.42/0.73 (77,1) [1141,1]. true => ~_t199 | _t34 [ LRES, 143, 775, ~_t25 ] % 0.42/0.73 (77,1) [1148,1]. true => ~_t199 | _t26 [ LRES, 104, 775, ~_t25 ] % 0.42/0.73 (77,1) [1218,1]. true => ~_t34 | _t32 | _t5 [ LRES, 141, 142, ~_t4 ] % 0.42/0.73 (89,1) [1219,1]. true => ~_t148 | _t5 [ LRES, 141, 777, ~_t4 ] [ Modal Level Pure Literal Elimination, ~_t148 ] % 0.42/0.73 (77,1) [1931,1]. true => ~_t34 | _t32 | _t20 | ~_t19 [ LRES, 1118, 142, ~_t4 ] % 0.42/0.73 (89,1) [1932,1]. true => ~_t148 | _t20 | ~_t19 [ LRES, 1118, 777, ~_t4 ] [ Modal Level Pure Literal Elimination, ~_t148 ] % 0.42/0.73 (24,1) [1974,1]. true => ~_t186 | ~_t149 | _t3 [ LRES, 833, 701, ~_t2 ] % 0.42/0.73 (89,1) [1979,1]. true => ~_t152 | ~_t148 | _t20 [ LRES, 1932, 707, ~_t19 ] [ Backward Subsumption, 2981 ] % 0.42/0.73 (3,1) [2179,1]. true => ~_t18 | ~_t3 [ GEN1, 634, 682, 2154, _t152, _t148 ] % 0.42/0.73 (18,1) [2579,1]. true => ~_t20 | ~_t5 [ GEN1, 638, 688, 2577, _t142, _t147 ] % 0.42/0.73 (89,1) [2583,1]. true => ~_t148 | ~_t20 [ LRES, 2579, 1219, ~_t5 ] [ Modal Level Pure Literal Elimination, ~_t148 ] % 0.42/0.73 (77,1) [2584,1]. true => ~_t34 | _t32 | ~_t20 [ LRES, 2579, 1218, ~_t5 ] % 0.42/0.73 (24,1) [2601,1]. true => ~_t186 | ~_t149 | ~_t18 [ LRES, 1974, 2179, _t3 ] % 0.42/0.73 (89,1) [2981,1]. true => ~_t152 | ~_t148 [ LRES, 1979, 2583, _t20 ] [ Modal Level Pure Literal Elimination, ~_t148 ] % 0.42/0.73 (24,1) [3590,1]. true => ~_t186 | ~_t149 | ~_t139 [ LRES, 2601, 721, ~_t18 ] [ Modal Level Pure Literal Elimination, ~_t139 ] % 0.42/0.73 (77,1) [5978,1]. true => ~_t152 | ~_t34 | _t32 | _t20 [ LRES, 1931, 707, ~_t19 ] [ Backward Subsumption, 6272 ] % 0.42/0.73 (76,1) [6022,1]. true => ~_t33 | ~_t26 | ~_t18 [ GEN1, 632, 634, 692, 6015, _t167, _t152, _t164 ] % 0.42/0.73 (77,1) [6023,1]. true => ~_t33 | ~_t32 | ~_t26 [ LRES, 6022, 118, ~_t18 ] % 0.42/0.73 (77,1) [6024,1]. true => ~_t199 | ~_t33 | ~_t32 [ LRES, 6023, 1148, ~_t26 ] % 0.42/0.73 (77,1) [6272,1]. true => ~_t152 | ~_t34 | _t32 [ LRES, 5978, 2584, _t20 ] % 0.42/0.73 (77,1) [6277,1]. true => ~_t152 | ~_t34 | _t33 [ LRES, 6272, 134, _t32 ] % 0.42/0.73 (77,1) [6278,1]. true => ~_t199 | ~_t152 | ~_t34 | ~_t33 [ LRES, 6272, 6024, _t32 ] [ Backward Subsumption, 6336 ] % 0.42/0.73 (77,1) [6336,1]. true => ~_t199 | ~_t152 | ~_t34 [ LRES, 6278, 6277, ~_t33 ] [ Backward Subsumption, 6343 ] % 0.42/0.73 (77,1) [6343,1]. true => ~_t199 | ~_t152 [ LRES, 6336, 1141, ~_t34 ] % 0.42/0.73 (3,1) [4,2]. true => ~_t4 | ~p2 [ SNF ] % 0.42/0.73 (1,1) [9,2]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 570, _t6 ] % 0.42/0.73 (3,1) [16,2]. true => _t5 | ~_t4 [ SNF ] % 0.42/0.73 (18,1) [35,2]. true => ~_t21 | p2 [ SNF ] % 0.42/0.73 (17,1) [36,2]. _t22 => ~box 1~ ~p2 [ SNF ] [ SNF++, 610, ~p2 ] % 0.42/0.73 (18,1) [37,2]. true => _t22 | ~_t21 [ SNF ] % 0.42/0.73 (1,1) [64,2]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 574, _t19 ] % 0.42/0.73 (1,1) [80,2]. _t28 => box 1 _t29 [ SNF ] [ SNF++, 576, _t29 ] % 0.42/0.73 (1,1) [89,2]. true => ~_t32 | _t18 [ SNF ] % 0.42/0.73 (1,1) [92,2]. true => _t32 | _t28 | ~_t27 | _t4 [ SNF ] % 0.42/0.73 (74,1) [108,2]. _t20 => ~box 1~ _t21 [ SNF ] [ SNF++, 614, _t21 ] % 0.42/0.73 (1,1) [109,2]. true => _t20 | ~_t19 | p2 [ SNF ] % 0.42/0.73 (1,1) [126,2]. _t7 => box 1 p2 [ SNF ] [ SNF++, 580, p2 ] % 0.42/0.73 (1,1) [129,2]. true => _t7 | ~_t6 | ~p2 [ SNF ] % 0.42/0.73 (75,1) [132,2]. _t3 => ~box 1~ _t4 [ SNF ] [ SNF++, 616, _t4 ] % 0.42/0.73 (1,1) [570,2]. _t5 => box 1 _t142 [ SNF++, 9 ] % 0.42/0.73 (1,1) [574,2]. _t18 => box 1 _t152 [ SNF++, 64 ] % 0.42/0.73 (1,1) [576,2]. _t28 => box 1 _t153 [ SNF++, 80 ] % 0.42/0.73 (1,1) [580,2]. _t7 => box 1 _t137 [ SNF++, 126 ] % 0.42/0.73 (17,1) [610,2]. _t22 => ~box 1~ _t149 [ SNF++, 36 ] % 0.42/0.73 (74,1) [614,2]. _t20 => ~box 1~ _t147 [ SNF++, 108 ] % 0.42/0.73 (75,1) [616,2]. _t3 => ~box 1~ _t148 [ SNF++, 132 ] % 0.42/0.73 (1,1) [633,2]. true => ~_t167 | _t27 [ SNF++, 93 ] % 0.42/0.73 (1,1) [635,2]. true => ~_t152 | _t19 [ SNF++, 110 ] % 0.42/0.73 (1,1) [639,2]. true => ~_t142 | _t6 [ SNF++, 136 ] % 0.42/0.73 (3,1) [683,2]. true => ~_t148 | _t4 [ SNF++, 17 ] % 0.42/0.73 (18,1) [689,2]. true => ~_t147 | _t21 [ SNF++, 38 ] % 0.42/0.73 (76,1) [693,2]. true => ~_t164 | _t3 [ SNF++, 133 ] % 0.42/0.73 (3,1) [1079,2]. true => _t20 | ~_t19 | ~_t4 [ LRES, 4, 109, ~p2 ] % 0.42/0.73 (3,1) [1138,2]. true => _t32 | _t28 | ~_t27 | _t5 [ LRES, 16, 92, ~_t4 ] % 0.42/0.73 (3,1) [1139,2]. true => ~_t148 | _t5 [ LRES, 16, 683, ~_t4 ] % 0.42/0.73 (18,1) [1201,2]. true => ~_t147 | _t22 [ LRES, 37, 689, ~_t21 ] % 0.42/0.73 (17,1) [1267,2]. true => ~_t22 | ~_t7 [ GEN1, 580, 610, 826, _t137, _t149 ] % 0.42/0.73 (75,1) [1610,2]. true => ~_t18 | ~_t3 [ GEN1, 574, 616, 1606, _t152, _t148 ] % 0.42/0.73 (75,1) [1623,2]. true => ~_t28 | ~_t3 [ GEN1, 576, 616, 1621, _t153, _t148 ] % 0.42/0.73 (76,1) [1650,2]. true => ~_t164 | ~_t28 [ LRES, 1623, 693, ~_t3 ] % 0.42/0.73 (76,1) [1653,2]. true => ~_t164 | ~_t18 [ LRES, 1610, 693, ~_t3 ] % 0.42/0.73 (76,1) [1756,2]. true => ~_t164 | ~_t32 [ LRES, 1653, 89, ~_t18 ] % 0.42/0.73 (18,1) [1787,2]. true => ~_t21 | _t7 | ~_t6 [ LRES, 129, 35, ~p2 ] % 0.42/0.73 (3,1) [1795,2]. true => _t32 | _t28 | ~_t27 | _t20 | ~_t19 [ LRES, 1079, 92, ~_t4 ] % 0.42/0.73 (3,1) [1796,2]. true => ~_t148 | _t20 | ~_t19 [ LRES, 1079, 683, ~_t4 ] % 0.42/0.73 (3,1) [1822,2]. true => ~_t152 | ~_t148 | _t20 [ LRES, 1796, 635, ~_t19 ] [ Backward Subsumption, 2154 ] % 0.42/0.73 (18,1) [1881,2]. true => ~_t142 | ~_t21 | _t7 [ LRES, 1787, 639, ~_t6 ] % 0.42/0.73 (18,1) [2032,2]. true => ~_t142 | ~_t22 | ~_t21 [ LRES, 1881, 1267, _t7 ] % 0.42/0.73 (18,1) [2046,2]. true => ~_t147 | ~_t142 | ~_t22 [ LRES, 2032, 689, ~_t21 ] [ Backward Subsumption, 2577 ] % 0.42/0.73 (74,1) [2121,2]. true => ~_t20 | ~_t5 [ GEN1, 570, 614, 2103, _t142, _t147 ] % 0.42/0.73 (74,1) [2137,2]. true => ~_t148 | ~_t20 [ LRES, 2121, 1139, ~_t5 ] % 0.42/0.73 (74,1) [2154,2]. true => ~_t152 | ~_t148 [ LRES, 2137, 1822, ~_t20 ] % 0.42/0.73 (18,1) [2577,2]. true => ~_t147 | ~_t142 [ LRES, 2046, 1201, ~_t22 ] % 0.42/0.73 (74,1) [3274,2]. true => _t32 | _t28 | ~_t27 | ~_t20 [ LRES, 1138, 2121, _t5 ] % 0.42/0.73 (3,1) [5657,2]. true => ~_t152 | _t32 | _t28 | ~_t27 | _t20 [ LRES, 1795, 635, ~_t19 ] [ Backward Subsumption, 5991 ] % 0.42/0.73 (74,1) [5991,2]. true => ~_t152 | _t32 | _t28 | ~_t27 [ LRES, 5657, 3274, _t20 ] % 0.42/0.73 (74,1) [5992,2]. true => ~_t167 | ~_t152 | _t32 | _t28 [ LRES, 5991, 633, ~_t27 ] % 0.42/0.73 (76,1) [5993,2]. true => ~_t167 | ~_t164 | ~_t152 | _t32 [ LRES, 5992, 1650, _t28 ] [ Backward Subsumption, 6015 ] % 0.42/0.73 (76,1) [6015,2]. true => ~_t167 | ~_t164 | ~_t152 [ LRES, 5993, 1756, _t32 ] % 0.42/0.73 (1,1) [5,3]. _t7 => box 1 p2 [ SNF ] [ SNF++, 540, p2 ] % 0.42/0.73 (1,1) [8,3]. true => _t7 | ~_t6 | ~p2 [ SNF ] % 0.42/0.73 (65,1) [51,3]. _t20 => ~box 1~ _t21 [ SNF ] [ SNF++, 560, _t21 ] % 0.42/0.73 (1,1) [52,3]. true => _t20 | ~_t19 | p2 [ SNF ] % 0.42/0.73 (1,1) [53,3]. true => ~_t29 | _t19 [ SNF ] % 0.42/0.73 (74,1) [105,3]. true => ~_t21 | p2 [ SNF ] % 0.42/0.73 (73,1) [106,3]. _t22 => ~box 1~ ~p2 [ SNF ] [ SNF++, 564, ~p2 ] % 0.42/0.73 (74,1) [107,3]. true => _t22 | ~_t21 [ SNF ] % 0.42/0.73 (75,1) [119,3]. true => ~_t4 | ~p2 [ SNF ] % 0.42/0.73 (1,1) [124,3]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 550, _t6 ] % 0.42/0.73 (75,1) [131,3]. true => _t5 | ~_t4 [ SNF ] % 0.42/0.73 (1,1) [540,3]. _t7 => box 1 _t137 [ SNF++, 5 ] % 0.42/0.73 (1,1) [550,3]. _t5 => box 1 _t142 [ SNF++, 124 ] % 0.42/0.73 (65,1) [560,3]. _t20 => ~box 1~ _t147 [ SNF++, 51 ] % 0.42/0.73 (73,1) [564,3]. _t22 => ~box 1~ _t149 [ SNF++, 106 ] % 0.42/0.73 (1,1) [571,3]. true => ~_t142 | _t6 [ SNF++, 9 ] % 0.42/0.73 (1,1) [575,3]. true => ~_t152 | _t19 [ SNF++, 64 ] % 0.42/0.73 (1,1) [577,3]. true => ~_t153 | _t29 [ SNF++, 80 ] % 0.42/0.73 (1,1) [581,3]. true => ~_t137 | p2 [ SNF++, 126 ] % 0.42/0.73 (17,1) [611,3]. true => ~_t149 | ~p2 [ SNF++, 36 ] % 0.42/0.73 (74,1) [615,3]. true => ~_t147 | _t21 [ SNF++, 108 ] % 0.42/0.73 (75,1) [617,3]. true => ~_t148 | _t4 [ SNF++, 132 ] % 0.42/0.73 (17,1) [826,3]. true => ~_t149 | ~_t137 [ LRES, 611, 581, ~p2 ] % 0.42/0.73 (75,1) [949,3]. true => _t20 | ~_t19 | ~_t4 [ LRES, 119, 52, ~p2 ] % 0.42/0.73 (74,1) [1099,3]. true => ~_t147 | _t22 [ LRES, 107, 615, ~_t21 ] % 0.42/0.73 (75,1) [1147,3]. true => ~_t148 | _t5 [ LRES, 131, 617, ~_t4 ] % 0.42/0.73 (73,1) [1216,3]. true => ~_t22 | ~_t7 [ GEN1, 540, 564, 887, _t137, _t149 ] % 0.42/0.73 (65,1) [1338,3]. true => ~_t20 | ~_t5 [ GEN1, 550, 560, 1335, _t142, _t147 ] % 0.42/0.73 (75,1) [1388,3]. true => ~_t148 | ~_t20 [ LRES, 1338, 1147, ~_t5 ] % 0.42/0.73 (74,1) [1415,3]. true => ~_t21 | _t7 | ~_t6 [ LRES, 8, 105, ~p2 ] % 0.42/0.73 (75,1) [1435,3]. true => ~_t148 | _t20 | ~_t19 [ LRES, 949, 617, ~_t4 ] % 0.42/0.73 (75,1) [1438,3]. true => ~_t148 | ~_t29 | _t20 [ LRES, 1435, 53, ~_t19 ] [ Backward Subsumption, 1617 ] % 0.42/0.73 (75,1) [1440,3]. true => ~_t152 | ~_t148 | _t20 [ LRES, 1435, 575, ~_t19 ] [ Backward Subsumption, 1606 ] % 0.42/0.73 (74,1) [1570,3]. true => ~_t142 | ~_t21 | _t7 [ LRES, 1415, 571, ~_t6 ] % 0.42/0.73 (75,1) [1606,3]. true => ~_t152 | ~_t148 [ LRES, 1440, 1388, _t20 ] % 0.42/0.73 (75,1) [1617,3]. true => ~_t148 | ~_t29 [ LRES, 1438, 1388, _t20 ] % 0.42/0.73 (75,1) [1621,3]. true => ~_t153 | ~_t148 [ LRES, 1617, 577, ~_t29 ] % 0.42/0.73 (74,1) [1733,3]. true => ~_t142 | ~_t22 | ~_t21 [ LRES, 1570, 1216, _t7 ] % 0.42/0.73 (74,1) [2063,3]. true => ~_t147 | ~_t142 | ~_t22 [ LRES, 1733, 615, ~_t21 ] [ Backward Subsumption, 2103 ] % 0.42/0.73 (74,1) [2103,3]. true => ~_t147 | ~_t142 [ LRES, 2063, 1099, ~_t22 ] % 0.42/0.73 (65,1) [48,4]. true => ~_t21 | p2 [ SNF ] % 0.42/0.73 (64,1) [49,4]. _t22 => ~box 1~ ~p2 [ SNF ] [ SNF++, 800, ~p2 ] % 0.42/0.73 (65,1) [50,4]. true => _t22 | ~_t21 [ SNF ] % 0.42/0.73 (1,1) [120,4]. _t7 => box 1 p2 [ SNF ] [ SNF++, 808, p2 ] % 0.42/0.73 (1,1) [123,4]. true => _t7 | ~_t6 | ~p2 [ SNF ] % 0.42/0.73 (1,1) [541,4]. true => ~_t137 | p2 [ SNF++, 5 ] % 0.42/0.73 (1,1) [551,4]. true => ~_t142 | _t6 [ SNF++, 124 ] % 0.42/0.73 (65,1) [561,4]. true => ~_t147 | _t21 [ SNF++, 51 ] % 0.42/0.73 (73,1) [565,4]. true => ~_t149 | ~p2 [ SNF++, 106 ] % 0.42/0.73 (64,1) [800,4]. _t22 => ~box 1~ _t149 [ SNF++, 49 ] % 0.42/0.73 (1,1) [808,4]. _t7 => box 1 _t137 [ SNF++, 120 ] % 0.42/0.73 (65,1) [844,4]. true => ~_t147 | _t22 [ LRES, 50, 561, ~_t21 ] % 0.42/0.73 (73,1) [887,4]. true => ~_t149 | ~_t137 [ LRES, 565, 541, ~p2 ] % 0.42/0.73 (64,1) [932,4]. true => ~_t22 | ~_t7 [ GEN1, 808, 800, 847, _t137, _t149 ] % 0.42/0.73 (65,1) [1292,4]. true => ~_t21 | _t7 | ~_t6 [ LRES, 123, 48, ~p2 ] % 0.42/0.73 (65,1) [1305,4]. true => ~_t142 | ~_t21 | _t7 [ LRES, 1292, 551, ~_t6 ] % 0.42/0.73 (65,1) [1307,4]. true => ~_t142 | ~_t22 | ~_t21 [ LRES, 1305, 932, _t7 ] % 0.42/0.73 (65,1) [1325,4]. true => ~_t147 | ~_t142 | ~_t22 [ LRES, 1307, 561, ~_t21 ] [ Backward Subsumption, 1335 ] % 0.42/0.73 (65,1) [1335,4]. true => ~_t147 | ~_t142 [ LRES, 1325, 844, ~_t22 ] % 0.42/0.73 (64,1) [801,5]. true => ~_t149 | ~p2 [ SNF++, 49 ] % 0.42/0.73 (1,1) [809,5]. true => ~_t137 | p2 [ SNF++, 120 ] % 0.42/0.73 (64,1) [847,5]. true => ~_t149 | ~_t137 [ LRES, 801, 809, ~p2 ] % 0.42/0.73 % SZS output end Refutation % 0.42/0.73 % KSP exiting %------------------------------------------------------------------------------