%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP083_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n024.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:58 PM UTC 2026 % Result : Theorem 0.15s 0.40s % Output : Refutation 0.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : SYP083_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.06 % Command : run_ksp %s % 0.07/0.24 % Computer : n024.cluster.edu % 0.07/0.24 % Model : x86_64 x86_64 % 0.07/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.24 % Memory : 8042.1875MB % 0.07/0.24 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.24 % CPULimit : 300 % 0.07/0.24 % WCLimit : 300 % 0.07/0.24 % DateTime : Mon May 4 12:20:56 EDT 2026 % 0.07/0.24 % CPUTime : % 0.15/0.38 ----KSP format--- % 0.15/0.39 set(box,SER). % 0.15/0.39 usable(formulas). % 0.15/0.39 true. % 0.15/0.39 end_of_list. % 0.15/0.39 sos(formulas). % 0.15/0.39 ~ ([] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( [] ( $false ) ) | <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) | <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) | <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) | <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( [] ( $false ) ) ) | <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) | <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) | <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) | <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( [] ( $false ) ) ) ) | <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) | <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) | <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) | <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) | <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ). % 0.15/0.39 end_of_list. % 0.15/0.39 ----------------- % 0.15/0.39 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.7mXKplg1tt/theBenchmark.ksp % 0.15/0.40 % 0.15/0.40 % SZS status Theorem % 0.15/0.40 % 0.15/0.40 ***************** % 0.15/0.40 FOUND PROOF 1 % 0.15/0.40 ***************** % 0.15/0.40 % SZS output start Refutation % 0.15/0.40 % 0.15/0.40 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.15/0.40 (1,1) [48,0]. _t12 => box 1 _t13 [ SNF ] [ Backward Subsumption, 973 ] % 0.15/0.40 (1,1) [50,0]. true => _t12 | ~_t0 [ SNF ] [ Backward Subsumption, 871 ] % 0.15/0.40 (1,1) [130,0]. _t52 => box 1 _t53 [ SNF ] [ Backward Subsumption, 878 ] % 0.15/0.40 (1,1) [132,0]. true => _t52 | ~_t0 [ SNF ] [ Backward Subsumption, 868 ] % 0.15/0.40 (141,1) [819,0]. _t65 => ~box 1~ _t66 [ SNF ] [ Backward Subsumption, 923 ] % 0.15/0.40 (1,1) [820,0]. true => _t65 | ~_t0 [ SNF ] [ Backward Subsumption, 822 ] % 0.15/0.40 (1,1) [822,0]. true => _t65 [ Unit Resolution, 3, 820, _t0 ] [ Modal Level Pure Literal Elimination, _t65 ] % 0.15/0.40 (1,1) [868,0]. true => _t52 [ Unit Resolution, 3, 132, _t0 ] [ Modal Level Pure Literal Elimination, _t52 ] % 0.15/0.40 (1,1) [871,0]. true => _t12 [ Unit Resolution, 3, 50, _t0 ] [ Modal Level Pure Literal Elimination, _t12 ] % 0.15/0.40 (1,1) [878,0]. true => box 1 _t53 [ LHS Unit Resolution, 868, 130, _t52 ] [ SNF++, 2190, _t53 ] % 0.15/0.40 (141,1) [923,0]. true => ~box 1~ _t66 [ LHS Unit Resolution, 822, 819, _t65 ] [ SNF++, 2382, _t66 ] % 0.15/0.40 (1,1) [973,0]. true => box 1 _t13 [ LHS Unit Resolution, 871, 48, _t12 ] [ SNF++, 2184, _t13 ] % 0.15/0.40 (1,1) [2184,0]. true => box 1 _t193 [ SNF++, 973 ] % 0.15/0.40 (1,1) [2190,0]. true => box 1 _t196 [ SNF++, 878 ] % 0.15/0.40 (141,1) [2382,0]. true => ~box 1~ _t197 [ SNF++, 923 ] % 0.15/0.40 (141,1) [3746,0]. true => false [ GEN1, 2190, 2184, 2382, 3743, _t196, _t193, _t197 ] % 0.15/0.40 (1,1) [46,1]. _t13 => box 1 _t14 [ SNF ] [ SNF++, 1982, _t14 ] % 0.15/0.40 (1,1) [128,1]. _t53 => box 1 _t54 [ SNF ] [ SNF++, 1988, _t54 ] % 0.15/0.40 (140,1) [818,1]. _t66 => ~box 1~ _t67 [ SNF ] [ SNF++, 2180, _t67 ] % 0.15/0.40 (1,1) [1982,1]. _t13 => box 1 _t187 [ SNF++, 46 ] % 0.15/0.40 (1,1) [1988,1]. _t53 => box 1 _t190 [ SNF++, 128 ] % 0.15/0.40 (140,1) [2180,1]. _t66 => ~box 1~ _t191 [ SNF++, 818 ] % 0.15/0.40 (1,1) [2185,1]. true => ~_t193 | _t13 [ SNF++, 973 ] % 0.15/0.40 (1,1) [2191,1]. true => ~_t196 | _t53 [ SNF++, 878 ] % 0.15/0.40 (141,1) [2383,1]. true => ~_t197 | _t66 [ SNF++, 923 ] % 0.15/0.40 (140,1) [3679,1]. true => ~_t66 | ~_t53 | ~_t13 [ GEN1, 1988, 1982, 2180, 3677, _t190, _t187, _t191 ] % 0.15/0.40 (140,1) [3737,1]. true => ~_t193 | ~_t66 | ~_t53 [ LRES, 3679, 2185, ~_t13 ] % 0.15/0.40 (140,1) [3740,1]. true => ~_t196 | ~_t193 | ~_t66 [ LRES, 3737, 2191, ~_t53 ] % 0.15/0.40 (141,1) [3743,1]. true => ~_t197 | ~_t196 | ~_t193 [ LRES, 3740, 2383, ~_t66 ] % 0.15/0.40 (1,1) [44,2]. _t14 => box 1 _t15 [ SNF ] [ SNF++, 1790, _t15 ] % 0.15/0.40 (1,1) [126,2]. _t54 => box 1 _t55 [ SNF ] [ SNF++, 1796, _t55 ] % 0.15/0.40 (139,1) [817,2]. _t67 => ~box 1~ _t68 [ SNF ] [ SNF++, 1978, _t68 ] % 0.15/0.40 (1,1) [1790,2]. _t14 => box 1 _t181 [ SNF++, 44 ] % 0.15/0.40 (1,1) [1796,2]. _t54 => box 1 _t184 [ SNF++, 126 ] % 0.15/0.40 (139,1) [1978,2]. _t67 => ~box 1~ _t185 [ SNF++, 817 ] % 0.15/0.40 (1,1) [1983,2]. true => ~_t187 | _t14 [ SNF++, 46 ] % 0.15/0.40 (1,1) [1989,2]. true => ~_t190 | _t54 [ SNF++, 128 ] % 0.15/0.40 (140,1) [2181,2]. true => ~_t191 | _t67 [ SNF++, 818 ] % 0.15/0.40 (139,1) [3662,2]. true => ~_t67 | ~_t54 | ~_t14 [ GEN1, 1796, 1790, 1978, 3659, _t184, _t181, _t185 ] % 0.15/0.40 (139,1) [3669,2]. true => ~_t187 | ~_t67 | ~_t54 [ LRES, 3662, 1983, ~_t14 ] % 0.15/0.40 (139,1) [3674,2]. true => ~_t190 | ~_t187 | ~_t67 [ LRES, 3669, 1989, ~_t54 ] % 0.15/0.40 (140,1) [3677,2]. true => ~_t191 | ~_t190 | ~_t187 [ LRES, 3674, 2181, ~_t67 ] % 0.15/0.40 (1,1) [42,3]. _t15 => box 1 _t16 [ SNF ] [ SNF++, 1618, _t16 ] % 0.15/0.40 (1,1) [124,3]. _t55 => box 1 _t56 [ SNF ] [ SNF++, 1624, _t56 ] % 0.15/0.40 (138,1) [816,3]. _t68 => ~box 1~ _t69 [ SNF ] [ SNF++, 1786, _t69 ] % 0.15/0.40 (1,1) [1618,3]. _t15 => box 1 _t175 [ SNF++, 42 ] % 0.15/0.40 (1,1) [1624,3]. _t55 => box 1 _t178 [ SNF++, 124 ] % 0.15/0.40 (138,1) [1786,3]. _t68 => ~box 1~ _t179 [ SNF++, 816 ] % 0.15/0.40 (1,1) [1791,3]. true => ~_t181 | _t15 [ SNF++, 44 ] % 0.15/0.40 (1,1) [1797,3]. true => ~_t184 | _t55 [ SNF++, 126 ] % 0.15/0.40 (139,1) [1979,3]. true => ~_t185 | _t68 [ SNF++, 817 ] % 0.15/0.40 (138,1) [3589,3]. true => ~_t68 | ~_t55 | ~_t15 [ GEN1, 1624, 1618, 1786, 3587, _t178, _t175, _t179 ] % 0.15/0.40 (138,1) [3600,3]. true => ~_t181 | ~_t68 | ~_t55 [ LRES, 3589, 1791, ~_t15 ] % 0.15/0.40 (138,1) [3657,3]. true => ~_t184 | ~_t181 | ~_t68 [ LRES, 3600, 1797, ~_t55 ] % 0.15/0.40 (139,1) [3659,3]. true => ~_t185 | ~_t184 | ~_t181 [ LRES, 3657, 1979, ~_t68 ] % 0.15/0.40 (1,1) [40,4]. _t16 => box 1 _t17 [ SNF ] [ SNF++, 1466, _t17 ] % 0.15/0.40 (1,1) [122,4]. _t56 => box 1 _t57 [ SNF ] [ SNF++, 1472, _t57 ] % 0.15/0.40 (137,1) [815,4]. _t69 => ~box 1~ _t70 [ SNF ] [ SNF++, 1614, _t70 ] % 0.15/0.40 (1,1) [1466,4]. _t16 => box 1 _t169 [ SNF++, 40 ] % 0.15/0.40 (1,1) [1472,4]. _t56 => box 1 _t172 [ SNF++, 122 ] % 0.15/0.40 (137,1) [1614,4]. _t69 => ~box 1~ _t173 [ SNF++, 815 ] % 0.15/0.40 (1,1) [1619,4]. true => ~_t175 | _t16 [ SNF++, 42 ] % 0.15/0.40 (1,1) [1625,4]. true => ~_t178 | _t56 [ SNF++, 124 ] % 0.15/0.40 (138,1) [1787,4]. true => ~_t179 | _t69 [ SNF++, 816 ] % 0.15/0.40 (137,1) [3519,4]. true => ~_t69 | ~_t56 | ~_t16 [ GEN1, 1472, 1466, 1614, 3517, _t172, _t169, _t173 ] % 0.15/0.40 (137,1) [3531,4]. true => ~_t175 | ~_t69 | ~_t56 [ LRES, 3519, 1619, ~_t16 ] % 0.15/0.40 (137,1) [3585,4]. true => ~_t178 | ~_t175 | ~_t69 [ LRES, 3531, 1625, ~_t56 ] % 0.15/0.40 (138,1) [3587,4]. true => ~_t179 | ~_t178 | ~_t175 [ LRES, 3585, 1787, ~_t69 ] % 0.15/0.40 (1,1) [38,5]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 1334, _t18 ] % 0.15/0.40 (1,1) [120,5]. _t57 => box 1 _t58 [ SNF ] [ SNF++, 1340, _t58 ] % 0.15/0.40 (136,1) [814,5]. _t70 => ~box 1~ _t71 [ SNF ] [ SNF++, 1462, _t71 ] % 0.15/0.40 (1,1) [1334,5]. _t17 => box 1 _t163 [ SNF++, 38 ] % 0.15/0.40 (1,1) [1340,5]. _t57 => box 1 _t166 [ SNF++, 120 ] % 0.15/0.40 (136,1) [1462,5]. _t70 => ~box 1~ _t167 [ SNF++, 814 ] % 0.15/0.40 (1,1) [1467,5]. true => ~_t169 | _t17 [ SNF++, 40 ] % 0.15/0.40 (1,1) [1473,5]. true => ~_t172 | _t57 [ SNF++, 122 ] % 0.15/0.40 (137,1) [1615,5]. true => ~_t173 | _t70 [ SNF++, 815 ] % 0.15/0.40 (136,1) [3414,5]. true => ~_t70 | ~_t57 | ~_t17 [ GEN1, 1340, 1334, 1462, 3412, _t166, _t163, _t167 ] % 0.15/0.40 (136,1) [3464,5]. true => ~_t169 | ~_t70 | ~_t57 [ LRES, 3414, 1467, ~_t17 ] % 0.15/0.40 (136,1) [3513,5]. true => ~_t172 | ~_t169 | ~_t70 [ LRES, 3464, 1473, ~_t57 ] % 0.15/0.40 (137,1) [3517,5]. true => ~_t173 | ~_t172 | ~_t169 [ LRES, 3513, 1615, ~_t70 ] % 0.15/0.40 (1,1) [36,6]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 1222, _t19 ] % 0.15/0.40 (1,1) [118,6]. _t58 => box 1 _t59 [ SNF ] [ SNF++, 1228, _t59 ] % 0.15/0.40 (135,1) [813,6]. _t71 => ~box 1~ _t72 [ SNF ] [ SNF++, 1330, _t72 ] % 0.15/0.40 (1,1) [1222,6]. _t18 => box 1 _t157 [ SNF++, 36 ] % 0.15/0.40 (1,1) [1228,6]. _t58 => box 1 _t160 [ SNF++, 118 ] % 0.15/0.40 (135,1) [1330,6]. _t71 => ~box 1~ _t161 [ SNF++, 813 ] % 0.15/0.40 (1,1) [1335,6]. true => ~_t163 | _t18 [ SNF++, 38 ] % 0.15/0.40 (1,1) [1341,6]. true => ~_t166 | _t58 [ SNF++, 120 ] % 0.15/0.40 (136,1) [1463,6]. true => ~_t167 | _t71 [ SNF++, 814 ] % 0.15/0.40 (135,1) [3361,6]. true => ~_t71 | ~_t58 | ~_t18 [ GEN1, 1228, 1222, 1330, 3358, _t160, _t157, _t161 ] % 0.15/0.40 (135,1) [3401,6]. true => ~_t163 | ~_t71 | ~_t58 [ LRES, 3361, 1335, ~_t18 ] % 0.15/0.40 (135,1) [3409,6]. true => ~_t166 | ~_t163 | ~_t71 [ LRES, 3401, 1341, ~_t58 ] % 0.15/0.40 (136,1) [3412,6]. true => ~_t167 | ~_t166 | ~_t163 [ LRES, 3409, 1463, ~_t71 ] % 0.15/0.40 (1,1) [34,7]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 1130, _t20 ] % 0.15/0.40 (1,1) [116,7]. _t59 => box 1 _t60 [ SNF ] [ SNF++, 1136, _t60 ] % 0.15/0.40 (134,1) [812,7]. _t72 => ~box 1~ _t73 [ SNF ] [ SNF++, 1218, _t73 ] % 0.15/0.40 (1,1) [1130,7]. _t19 => box 1 _t151 [ SNF++, 34 ] % 0.15/0.40 (1,1) [1136,7]. _t59 => box 1 _t154 [ SNF++, 116 ] % 0.15/0.40 (134,1) [1218,7]. _t72 => ~box 1~ _t155 [ SNF++, 812 ] % 0.15/0.40 (1,1) [1223,7]. true => ~_t157 | _t19 [ SNF++, 36 ] % 0.15/0.40 (1,1) [1229,7]. true => ~_t160 | _t59 [ SNF++, 118 ] % 0.15/0.40 (135,1) [1331,7]. true => ~_t161 | _t72 [ SNF++, 813 ] % 0.15/0.40 (134,1) [3349,7]. true => ~_t72 | ~_t59 | ~_t19 [ GEN1, 1136, 1130, 1218, 3346, _t154, _t151, _t155 ] % 0.15/0.40 (134,1) [3352,7]. true => ~_t157 | ~_t72 | ~_t59 [ LRES, 3349, 1223, ~_t19 ] % 0.15/0.40 (134,1) [3354,7]. true => ~_t160 | ~_t157 | ~_t72 [ LRES, 3352, 1229, ~_t59 ] % 0.15/0.40 (135,1) [3358,7]. true => ~_t161 | ~_t160 | ~_t157 [ LRES, 3354, 1331, ~_t72 ] % 0.15/0.40 (1,1) [32,8]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 1058, _t21 ] % 0.15/0.40 (1,1) [114,8]. _t60 => box 1 _t61 [ SNF ] [ SNF++, 1064, _t61 ] % 0.15/0.40 (133,1) [811,8]. _t73 => ~box 1~ _t74 [ SNF ] [ SNF++, 1126, _t74 ] % 0.15/0.40 (1,1) [1058,8]. _t20 => box 1 _t145 [ SNF++, 32 ] % 0.15/0.40 (1,1) [1064,8]. _t60 => box 1 _t148 [ SNF++, 114 ] % 0.15/0.40 (133,1) [1126,8]. _t73 => ~box 1~ _t149 [ SNF++, 811 ] % 0.15/0.40 (1,1) [1131,8]. true => ~_t151 | _t20 [ SNF++, 34 ] % 0.15/0.40 (1,1) [1137,8]. true => ~_t154 | _t60 [ SNF++, 116 ] % 0.15/0.40 (134,1) [1219,8]. true => ~_t155 | _t73 [ SNF++, 812 ] % 0.15/0.40 (133,1) [3293,8]. true => ~_t73 | ~_t60 | ~_t20 [ GEN1, 1064, 1058, 1126, 3291, _t148, _t145, _t149 ] % 0.15/0.40 (133,1) [3302,8]. true => ~_t151 | ~_t73 | ~_t60 [ LRES, 3293, 1131, ~_t20 ] % 0.15/0.40 (133,1) [3340,8]. true => ~_t154 | ~_t151 | ~_t73 [ LRES, 3302, 1137, ~_t60 ] % 0.15/0.40 (134,1) [3346,8]. true => ~_t155 | ~_t154 | ~_t151 [ LRES, 3340, 1219, ~_t73 ] % 0.15/0.40 (1,1) [30,9]. _t21 => box 1 _t22 [ SNF ] [ SNF++, 1006, _t22 ] % 0.15/0.40 (1,1) [112,9]. _t61 => box 1 _t62 [ SNF ] [ SNF++, 1012, _t62 ] % 0.15/0.40 (132,1) [810,9]. _t74 => ~box 1~ _t75 [ SNF ] [ SNF++, 1054, _t75 ] % 0.15/0.40 (1,1) [1006,9]. _t21 => box 1 _t139 [ SNF++, 30 ] % 0.15/0.40 (1,1) [1012,9]. _t61 => box 1 _t142 [ SNF++, 112 ] % 0.15/0.40 (132,1) [1054,9]. _t74 => ~box 1~ _t143 [ SNF++, 810 ] % 0.15/0.40 (1,1) [1059,9]. true => ~_t145 | _t21 [ SNF++, 32 ] % 0.15/0.40 (1,1) [1065,9]. true => ~_t148 | _t61 [ SNF++, 114 ] % 0.15/0.40 (133,1) [1127,9]. true => ~_t149 | _t74 [ SNF++, 811 ] % 0.15/0.40 (132,1) [3259,9]. true => ~_t74 | ~_t61 | ~_t21 [ GEN1, 1012, 1006, 1054, 3258, _t142, _t139, _t143 ] % 0.15/0.40 (132,1) [3264,9]. true => ~_t145 | ~_t74 | ~_t61 [ LRES, 3259, 1059, ~_t21 ] % 0.15/0.40 (132,1) [3289,9]. true => ~_t148 | ~_t145 | ~_t74 [ LRES, 3264, 1065, ~_t61 ] % 0.15/0.40 (133,1) [3291,9]. true => ~_t149 | ~_t148 | ~_t145 [ LRES, 3289, 1127, ~_t74 ] % 0.15/0.40 (1,1) [27,10]. _t23 => box 1 _t24 [ SNF ] [ SNF++, 992, _t24 ] % 0.15/0.40 (1,1) [28,10]. _t23 => ~box 1~ _t24 [ Axiom SER ] [ SNF++, 974, _t24 ] % 0.15/0.40 (1,1) [29,10]. true => _t23 | ~_t22 | p0 [ SNF ] % 0.15/0.40 (1,1) [108,10]. _t63 => box 1 _t64 [ SNF ] [ SNF++, 998, _t64 ] % 0.15/0.40 (1,1) [109,10]. _t63 => ~box 1~ _t64 [ Axiom SER ] [ SNF++, 982, _t64 ] % 0.15/0.40 (13,1) [110,10]. _t24 => ~box 1~ ~p0 [ SNF ] [ SNF++, 986, ~p0 ] % 0.15/0.40 (1,1) [111,10]. true => _t63 | ~_t62 | _t24 [ SNF ] % 0.15/0.40 (1,1) [178,10]. _t40 => ~box 1~ ~p0 [ Axiom SER ] [ SNF++, 984, ~p0 ] % 0.15/0.40 (1,1) [223,10]. _t64 => box 1 p0 [ SNF ] [ SNF++, 1002, p0 ] % 0.15/0.40 (1,1) [224,10]. _t64 => ~box 1~ p0 [ Axiom SER ] [ SNF++, 988, p0 ] % 0.15/0.40 (132,1) [808,10]. true => ~_t75 | ~p0 [ SNF ] % 0.15/0.40 (132,1) [809,10]. true => ~_t75 | _t64 [ SNF ] % 0.15/0.40 (1,1) [982,10]. _t63 => ~box 1~ _t135 [ SNF++, 109 ] % 0.15/0.40 (13,1) [986,10]. _t24 => ~box 1~ _t136 [ SNF++, 110 ] % 0.15/0.40 (1,1) [992,10]. _t23 => box 1 _t131 [ SNF++, 27 ] % 0.15/0.40 (1,1) [998,10]. _t63 => box 1 _t135 [ SNF++, 108 ] % 0.15/0.40 (1,1) [1002,10]. _t64 => box 1 _t137 [ SNF++, 223 ] % 0.15/0.40 (1,1) [1007,10]. true => ~_t139 | _t22 [ SNF++, 30 ] % 0.15/0.40 (1,1) [1013,10]. true => ~_t142 | _t62 [ SNF++, 112 ] % 0.15/0.40 (132,1) [1055,10]. true => ~_t143 | _t75 [ SNF++, 810 ] % 0.15/0.40 (132,1) [2420,10]. true => ~_t75 | _t23 | ~_t22 [ LRES, 808, 29, ~p0 ] % 0.15/0.40 (13,1) [2715,10]. true => ~_t64 | ~_t24 [ GEN1, 1002, 986, 2418, _t137, _t136 ] % 0.15/0.40 (13,1) [2805,10]. true => ~_t64 | _t63 | ~_t62 [ LRES, 2715, 111, ~_t24 ] % 0.15/0.40 (1,1) [2826,10]. true => ~_t63 | ~_t23 [ GEN3, 998, 992, 2794, 982, _t135, _t131, _t135 ] % 0.15/0.40 (132,1) [3241,10]. true => ~_t139 | ~_t75 | _t23 [ LRES, 2420, 1007, ~_t22 ] % 0.15/0.40 (13,1) [3243,10]. true => ~_t142 | ~_t64 | _t63 [ LRES, 2805, 1013, ~_t62 ] % 0.15/0.40 (132,1) [3246,10]. true => ~_t139 | ~_t75 | ~_t63 [ LRES, 3241, 2826, _t23 ] % 0.15/0.40 (132,1) [3247,10]. true => ~_t142 | ~_t139 | ~_t75 | ~_t64 [ LRES, 3246, 3243, ~_t63 ] [ Backward Subsumption, 3254 ] % 0.15/0.40 (132,1) [3254,10]. true => ~_t142 | ~_t139 | ~_t75 [ LRES, 3247, 809, ~_t64 ] % 0.15/0.40 (132,1) [3258,10]. true => ~_t143 | ~_t142 | ~_t139 [ LRES, 3254, 1055, ~_t75 ] % 0.15/0.40 (11,1) [26,11]. _t24 => ~box 1~ ~p0 [ SNF ] [ SNF++, 2386, ~p0 ] % 0.15/0.40 (1,1) [57,11]. _t40 => ~box 1~ ~p0 [ Axiom SER ] [ SNF++, 2384, ~p0 ] % 0.15/0.40 (1,1) [106,11]. _t64 => box 1 p0 [ SNF ] [ SNF++, 2398, p0 ] % 0.15/0.40 (1,1) [107,11]. _t64 => ~box 1~ p0 [ Axiom SER ] [ SNF++, 2390, p0 ] % 0.15/0.40 (1,1) [975,11]. true => ~_t131 | _t24 [ SNF++, 28 ] % 0.15/0.40 (1,1) [983,11]. true => ~_t135 | _t64 [ SNF++, 109 ] % 0.15/0.40 (1,1) [985,11]. true => ~_t136 | ~p0 [ SNF++, 178 ] % 0.15/0.40 (1,1) [989,11]. true => ~_t137 | p0 [ SNF++, 224 ] % 0.15/0.40 (11,1) [2386,11]. _t24 => ~box 1~ _t136 [ SNF++, 26 ] % 0.15/0.40 (1,1) [2398,11]. _t64 => box 1 _t137 [ SNF++, 106 ] % 0.15/0.40 (1,1) [2418,11]. true => ~_t137 | ~_t136 [ LRES, 985, 989, ~p0 ] % 0.15/0.40 (11,1) [2724,11]. true => ~_t64 | ~_t24 [ GEN1, 2398, 2386, 2419, _t137, _t136 ] % 0.15/0.40 (11,1) [2777,11]. true => ~_t131 | ~_t64 [ LRES, 2724, 975, ~_t24 ] % 0.15/0.40 (11,1) [2794,11]. true => ~_t135 | ~_t131 [ LRES, 2777, 983, ~_t64 ] % 0.15/0.40 (1,1) [2385,12]. true => ~_t136 | ~p0 [ SNF++, 57 ] % 0.15/0.40 (1,1) [2391,12]. true => ~_t137 | p0 [ SNF++, 107 ] % 0.15/0.40 (1,1) [2419,12]. true => ~_t137 | ~_t136 [ LRES, 2385, 2391, ~p0 ] % 0.15/0.40 % SZS output end Refutation % 0.15/0.41 % KSP exiting %------------------------------------------------------------------------------