%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP065_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n007.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:56 PM UTC 2026 % Result : Theorem 0.48s 0.71s % Output : Refutation 0.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP065_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.12 % Command : run_ksp %s % 0.17/0.34 % Computer : n007.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Mon May 4 17:06:08 EDT 2026 % 0.17/0.34 % CPUTime : % 0.39/0.60 ----KSP format--- % 0.39/0.60 set(box,SYM). % 0.39/0.60 usable(formulas). % 0.39/0.60 true. % 0.39/0.60 end_of_list. % 0.39/0.60 sos(formulas). % 0.39/0.60 ~ ([] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( 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.39/0.60 end_of_list. % 0.39/0.60 ----------------- % 0.39/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/sandbox2/tmp/tmp.2IGAoQliGQ/theBenchmark.ksp % 0.48/0.71 % 0.48/0.71 % SZS status Theorem % 0.48/0.71 % 0.48/0.71 ***************** % 0.48/0.71 FOUND PROOF 1 % 0.48/0.71 ***************** % 0.48/0.71 % SZS output start Refutation % 0.48/0.71 % 0.48/0.71 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.48/0.71 (1,1) [586,0]. _t52 => box 1 _t53 [ SNF ] [ Backward Subsumption, 1131 ] % 0.48/0.71 (1,1) [587,0]. true => _t52 | ~_t0 [ SNF ] [ Backward Subsumption, 1124 ] % 0.48/0.71 (141,1) [1075,0]. _t65 => ~box 1~ _t66 [ SNF ] [ Backward Subsumption, 1134 ] % 0.48/0.71 (1,1) [1076,0]. true => _t65 | ~_t0 [ SNF ] [ Backward Subsumption, 1078 ] % 0.48/0.71 (1,1) [1078,0]. true => _t65 [ Unit Resolution, 3, 1076, _t0 ] [ Modal Level Pure Literal Elimination, _t65 ] % 0.48/0.71 (1,1) [1124,0]. true => _t52 [ Unit Resolution, 3, 587, _t0 ] [ Modal Level Pure Literal Elimination, _t52 ] % 0.48/0.71 (1,1) [1131,0]. true => box 1 _t53 [ LHS Unit Resolution, 1124, 586, _t52 ] [ SNF++, 2414, _t53 ] % 0.48/0.71 (141,1) [1134,0]. true => ~box 1~ _t66 [ LHS Unit Resolution, 1078, 1075, _t65 ] [ SNF++, 2480, _t66 ] % 0.48/0.71 (1,1) [2414,0]. true => box 1 _t239 [ SNF++, 1131 ] % 0.48/0.71 (141,1) [2480,0]. true => ~box 1~ _t240 [ SNF++, 1134 ] % 0.48/0.71 (141,1) [5418,0]. true => false [ GEN1, 2414, 2480, 5395, _t239, _t240 ] % 0.48/0.71 (1,1) [582,1]. _t53 => box 1 _t54 [ SNF ] [ SNF++, 2242, _t54 ] % 0.48/0.71 (140,1) [1074,1]. _t66 => ~box 1~ _t67 [ SNF ] [ SNF++, 2340, _t67 ] % 0.48/0.71 (1,1) [2242,1]. _t53 => box 1 _t233 [ SNF++, 582 ] % 0.48/0.71 (140,1) [2340,1]. _t66 => ~box 1~ _t234 [ SNF++, 1074 ] % 0.48/0.71 (1,1) [2415,1]. true => ~_t239 | _t53 [ SNF++, 1131 ] % 0.48/0.71 (141,1) [2481,1]. true => ~_t240 | _t66 [ SNF++, 1134 ] % 0.48/0.71 (140,1) [5369,1]. true => ~_t66 | ~_t53 [ GEN1, 2242, 2340, 5346, _t233, _t234 ] % 0.48/0.71 (140,1) [5372,1]. true => ~_t239 | ~_t66 [ LRES, 5369, 2415, ~_t53 ] % 0.48/0.71 (141,1) [5395,1]. true => ~_t240 | ~_t239 [ LRES, 5372, 2481, ~_t66 ] % 0.48/0.71 (1,1) [575,2]. _t54 => box 1 _t55 [ SNF ] [ SNF++, 2050, _t55 ] % 0.48/0.71 (139,1) [1073,2]. _t67 => ~box 1~ _t68 [ SNF ] [ SNF++, 2138, _t68 ] % 0.48/0.71 (1,1) [2050,2]. _t54 => box 1 _t222 [ SNF++, 575 ] % 0.48/0.71 (139,1) [2138,2]. _t67 => ~box 1~ _t223 [ SNF++, 1073 ] % 0.48/0.71 (1,1) [2243,2]. true => ~_t233 | _t54 [ SNF++, 582 ] % 0.48/0.71 (140,1) [2341,2]. true => ~_t234 | _t67 [ SNF++, 1074 ] % 0.48/0.71 (139,1) [5303,2]. true => ~_t67 | ~_t54 [ GEN1, 2050, 2138, 5283, _t222, _t223 ] % 0.48/0.71 (139,1) [5322,2]. true => ~_t233 | ~_t67 [ LRES, 5303, 2243, ~_t54 ] % 0.48/0.71 (140,1) [5346,2]. true => ~_t234 | ~_t233 [ LRES, 5322, 2341, ~_t67 ] % 0.48/0.71 (1,1) [565,3]. _t55 => box 1 _t56 [ SNF ] [ SNF++, 1878, _t56 ] % 0.48/0.71 (138,1) [1072,3]. _t68 => ~box 1~ _t69 [ SNF ] [ SNF++, 1956, _t69 ] % 0.48/0.71 (1,1) [1878,3]. _t55 => box 1 _t211 [ SNF++, 565 ] % 0.48/0.71 (138,1) [1956,3]. _t68 => ~box 1~ _t212 [ SNF++, 1072 ] % 0.48/0.71 (1,1) [2051,3]. true => ~_t222 | _t55 [ SNF++, 575 ] % 0.48/0.71 (139,1) [2139,3]. true => ~_t223 | _t68 [ SNF++, 1073 ] % 0.48/0.71 (138,1) [5259,3]. true => ~_t68 | ~_t55 [ GEN1, 1878, 1956, 5229, _t211, _t212 ] % 0.48/0.71 (138,1) [5264,3]. true => ~_t222 | ~_t68 [ LRES, 5259, 2051, ~_t55 ] % 0.48/0.71 (139,1) [5283,3]. true => ~_t223 | ~_t222 [ LRES, 5264, 2139, ~_t68 ] % 0.48/0.71 (1,1) [552,4]. _t56 => box 1 _t57 [ SNF ] [ SNF++, 1726, _t57 ] % 0.48/0.71 (137,1) [1071,4]. _t69 => ~box 1~ _t70 [ SNF ] [ SNF++, 1794, _t70 ] % 0.48/0.71 (1,1) [1726,4]. _t56 => box 1 _t200 [ SNF++, 552 ] % 0.48/0.71 (137,1) [1794,4]. _t69 => ~box 1~ _t201 [ SNF++, 1071 ] % 0.48/0.71 (1,1) [1879,4]. true => ~_t211 | _t56 [ SNF++, 565 ] % 0.48/0.71 (138,1) [1957,4]. true => ~_t212 | _t69 [ SNF++, 1072 ] % 0.48/0.71 (137,1) [5201,4]. true => ~_t69 | ~_t56 [ GEN1, 1726, 1794, 5185, _t200, _t201 ] % 0.48/0.71 (137,1) [5216,4]. true => ~_t211 | ~_t69 [ LRES, 5201, 1879, ~_t56 ] % 0.48/0.71 (138,1) [5229,4]. true => ~_t212 | ~_t211 [ LRES, 5216, 1957, ~_t69 ] % 0.48/0.71 (1,1) [534,5]. _t57 => box 1 _t58 [ SNF ] [ SNF++, 1594, _t58 ] % 0.48/0.71 (136,1) [1070,5]. _t70 => ~box 1~ _t71 [ SNF ] [ SNF++, 1652, _t71 ] % 0.48/0.71 (1,1) [1594,5]. _t57 => box 1 _t189 [ SNF++, 534 ] % 0.48/0.71 (136,1) [1652,5]. _t70 => ~box 1~ _t190 [ SNF++, 1070 ] % 0.48/0.71 (1,1) [1727,5]. true => ~_t200 | _t57 [ SNF++, 552 ] % 0.48/0.71 (137,1) [1795,5]. true => ~_t201 | _t70 [ SNF++, 1071 ] % 0.48/0.71 (136,1) [5170,5]. true => ~_t70 | ~_t57 [ GEN1, 1594, 1652, 5159, _t189, _t190 ] % 0.48/0.71 (136,1) [5174,5]. true => ~_t200 | ~_t70 [ LRES, 5170, 1727, ~_t57 ] % 0.48/0.71 (137,1) [5185,5]. true => ~_t201 | ~_t200 [ LRES, 5174, 1795, ~_t70 ] % 0.48/0.71 (1,1) [514,6]. _t58 => box 1 _t59 [ SNF ] [ SNF++, 1482, _t59 ] % 0.48/0.71 (135,1) [1069,6]. _t71 => ~box 1~ _t72 [ SNF ] [ SNF++, 1530, _t72 ] % 0.48/0.71 (1,1) [1482,6]. _t58 => box 1 _t178 [ SNF++, 514 ] % 0.48/0.71 (135,1) [1530,6]. _t71 => ~box 1~ _t179 [ SNF++, 1069 ] % 0.48/0.71 (1,1) [1595,6]. true => ~_t189 | _t58 [ SNF++, 534 ] % 0.48/0.71 (136,1) [1653,6]. true => ~_t190 | _t71 [ SNF++, 1070 ] % 0.48/0.71 (135,1) [5128,6]. true => ~_t71 | ~_t58 [ GEN1, 1482, 1530, 5114, _t178, _t179 ] % 0.48/0.71 (135,1) [5145,6]. true => ~_t189 | ~_t71 [ LRES, 5128, 1595, ~_t58 ] % 0.48/0.71 (136,1) [5159,6]. true => ~_t190 | ~_t189 [ LRES, 5145, 1653, ~_t71 ] % 0.48/0.71 (1,1) [497,7]. _t59 => box 1 _t60 [ SNF ] [ SNF++, 1390, _t60 ] % 0.48/0.71 (134,1) [1068,7]. _t72 => ~box 1~ _t73 [ SNF ] [ SNF++, 1428, _t73 ] % 0.48/0.71 (1,1) [1390,7]. _t59 => box 1 _t167 [ SNF++, 497 ] % 0.48/0.71 (134,1) [1428,7]. _t72 => ~box 1~ _t168 [ SNF++, 1068 ] % 0.48/0.71 (1,1) [1483,7]. true => ~_t178 | _t59 [ SNF++, 514 ] % 0.48/0.71 (135,1) [1531,7]. true => ~_t179 | _t72 [ SNF++, 1069 ] % 0.48/0.71 (134,1) [5099,7]. true => ~_t72 | ~_t59 [ GEN1, 1390, 1428, 5090, _t167, _t168 ] % 0.48/0.71 (134,1) [5102,7]. true => ~_t178 | ~_t72 [ LRES, 5099, 1483, ~_t59 ] % 0.48/0.71 (135,1) [5114,7]. true => ~_t179 | ~_t178 [ LRES, 5102, 1531, ~_t72 ] % 0.48/0.71 (1,1) [483,8]. _t60 => box 1 _t61 [ SNF ] [ SNF++, 1318, _t61 ] % 0.48/0.71 (133,1) [1067,8]. _t73 => ~box 1~ _t74 [ SNF ] [ SNF++, 1346, _t74 ] % 0.48/0.71 (1,1) [1318,8]. _t60 => box 1 _t156 [ SNF++, 483 ] % 0.48/0.71 (133,1) [1346,8]. _t73 => ~box 1~ _t157 [ SNF++, 1067 ] % 0.48/0.71 (1,1) [1391,8]. true => ~_t167 | _t60 [ SNF++, 497 ] % 0.48/0.71 (134,1) [1429,8]. true => ~_t168 | _t73 [ SNF++, 1068 ] % 0.48/0.71 (133,1) [5076,8]. true => ~_t73 | ~_t60 [ GEN1, 1318, 1346, 5057, _t156, _t157 ] % 0.48/0.71 (133,1) [5078,8]. true => ~_t167 | ~_t73 [ LRES, 5076, 1391, ~_t60 ] % 0.48/0.71 (134,1) [5090,8]. true => ~_t168 | ~_t167 [ LRES, 5078, 1429, ~_t73 ] % 0.48/0.71 (1,1) [465,9]. _t118 => box 1 ~_t63 [ Axiom SYM ] [ SNF++, 1262, ~_t63 ] % 0.48/0.71 (1,1) [466,9]. _t64 => box 1 p0 [ SNF ] [ SNF++, 1264, p0 ] % 0.48/0.71 (1,1) [469,9]. true => _t118 | _t64 [ Axiom SYM ] % 0.48/0.71 (1,1) [472,9]. _t61 => box 1 _t62 [ SNF ] [ SNF++, 1266, _t62 ] % 0.48/0.71 (132,1) [1066,9]. _t74 => ~box 1~ _t75 [ SNF ] [ SNF++, 1284, _t75 ] % 0.48/0.71 (1,1) [1262,9]. _t118 => box 1 _t144 [ SNF++, 465 ] % 0.48/0.71 (1,1) [1264,9]. _t64 => box 1 _t128 [ SNF++, 466 ] % 0.48/0.71 (1,1) [1266,9]. _t61 => box 1 _t145 [ SNF++, 472 ] % 0.48/0.71 (132,1) [1284,9]. _t74 => ~box 1~ _t146 [ SNF++, 1066 ] % 0.48/0.71 (1,1) [1319,9]. true => ~_t156 | _t61 [ SNF++, 483 ] % 0.48/0.71 (133,1) [1347,9]. true => ~_t157 | _t74 [ SNF++, 1067 ] % 0.48/0.71 (132,1) [2929,9]. true => ~_t74 | ~_t64 [ GEN1, 1264, 1284, 2735, _t128, _t146 ] % 0.48/0.71 (132,1) [3164,9]. true => _t118 | ~_t74 [ LRES, 2929, 469, ~_t64 ] % 0.48/0.71 (133,1) [3429,9]. true => ~_t157 | _t118 [ LRES, 3164, 1347, ~_t74 ] % 0.48/0.71 (132,1) [4398,9]. true => ~_t118 | ~_t74 | ~_t61 [ GEN1, 1266, 1262, 1284, 4274, _t145, _t144, _t146 ] % 0.48/0.71 (132,1) [4652,9]. true => ~_t156 | ~_t118 | ~_t74 [ LRES, 4398, 1319, ~_t61 ] % 0.48/0.71 (133,1) [4670,9]. true => ~_t157 | ~_t156 | ~_t118 [ LRES, 4652, 1347, ~_t74 ] [ Backward Subsumption, 5057 ] % 0.48/0.71 (133,1) [5057,9]. true => ~_t157 | ~_t156 [ LRES, 4670, 3429, ~_t118 ] % 0.48/0.71 (7,1) [203,10]. _t38 => ~box 1~ p0 [ SNF ] [ SNF++, 1220, p0 ] % 0.48/0.71 (13,1) [470,10]. _t24 => ~box 1~ ~p0 [ SNF ] [ SNF++, 1224, ~p0 ] % 0.48/0.71 (1,1) [471,10]. true => _t63 | ~_t62 | _t24 [ SNF ] % 0.48/0.71 (1,1) [922,10]. _t64 => box 1 p0 [ SNF ] [ SNF++, 1242, p0 ] % 0.48/0.71 (132,1) [1064,10]. true => ~_t75 | ~p0 [ SNF ] % 0.48/0.71 (132,1) [1065,10]. true => ~_t75 | _t64 [ SNF ] % 0.48/0.71 (13,1) [1224,10]. _t24 => ~box 1~ _t130 [ SNF++, 470 ] % 0.48/0.71 (1,1) [1242,10]. _t64 => box 1 _t128 [ SNF++, 922 ] % 0.48/0.71 (1,1) [1263,10]. true => ~_t144 | ~_t63 [ SNF++, 465 ] % 0.48/0.71 (1,1) [1265,10]. true => ~_t128 | p0 [ SNF++, 466 ] % 0.48/0.71 (1,1) [1267,10]. true => ~_t145 | _t62 [ SNF++, 472 ] % 0.48/0.71 (132,1) [1285,10]. true => ~_t146 | _t75 [ SNF++, 1066 ] % 0.48/0.71 (132,1) [2555,10]. true => ~_t128 | ~_t75 [ LRES, 1064, 1265, ~p0 ] % 0.48/0.71 (13,1) [2617,10]. true => ~_t64 | ~_t24 [ GEN1, 1242, 1224, 2524, _t128, _t130 ] % 0.48/0.71 (132,1) [2735,10]. true => ~_t146 | ~_t128 [ LRES, 2555, 1285, ~_t75 ] % 0.48/0.71 (13,1) [2795,10]. true => ~_t64 | _t63 | ~_t62 [ LRES, 2617, 471, ~_t24 ] % 0.48/0.71 (13,1) [3654,10]. true => ~_t145 | ~_t64 | _t63 [ LRES, 2795, 1267, ~_t62 ] % 0.48/0.71 (13,1) [3918,10]. true => ~_t145 | ~_t144 | ~_t64 [ LRES, 3654, 1263, _t63 ] % 0.48/0.71 (132,1) [4106,10]. true => ~_t145 | ~_t144 | ~_t75 [ LRES, 3918, 1065, ~_t64 ] % 0.48/0.71 (132,1) [4274,10]. true => ~_t146 | ~_t145 | ~_t144 [ LRES, 4106, 1285, ~_t75 ] % 0.48/0.71 (7,1) [1221,11]. true => ~_t128 | p0 [ SNF++, 203 ] % 0.48/0.71 (13,1) [1225,11]. true => ~_t130 | ~p0 [ SNF++, 470 ] % 0.48/0.71 (13,1) [2524,11]. true => ~_t130 | ~_t128 [ LRES, 1225, 1221, ~p0 ] % 0.48/0.71 % SZS output end Refutation % 0.48/0.71 % KSP exiting %------------------------------------------------------------------------------