%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP029_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n015.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:54 PM UTC 2026 % Result : Theorem 7.12s 7.31s % Output : Refutation 7.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP029_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.15/0.33 % Computer : n015.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Mon May 4 16:14:46 EDT 2026 % 0.15/0.33 % CPUTime : % 0.35/0.59 ----KSP format--- % 0.35/0.59 set(box,TRANS). % 0.35/0.59 usable(formulas). % 0.35/0.59 true. % 0.35/0.59 end_of_list. % 0.35/0.59 sos(formulas). % 0.35/0.59 ~ ([] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( 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.35/0.59 end_of_list. % 0.35/0.59 ----------------- % 0.35/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/sandbox/tmp/tmp.u04tmUbyjv/theBenchmark.ksp % 7.12/7.31 % 7.12/7.31 % SZS status Theorem % 7.12/7.31 % 7.12/7.31 ***************** % 7.12/7.31 FOUND PROOF 1 % 7.12/7.31 ***************** % 7.12/7.31 % SZS output start Refutation % 7.12/7.31 % 7.12/7.31 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 7.12/7.31 (1,1) [150097,0]. _t19 => box 1 _t19 [ Axiom 4 ] [ Backward Subsumption, 170669 ] % 7.12/7.31 (1,1) [150568,0]. true => _t19 | ~_t0 [ SNF ] [ Backward Subsumption, 170596 ] % 7.12/7.31 (1,1) [157606,0]. _t9 => box 1 _t9 [ Axiom 4 ] [ Backward Subsumption, 170673 ] % 7.12/7.31 (1,1) [158077,0]. true => _t9 | ~_t0 [ SNF ] [ Backward Subsumption, 170592 ] % 7.12/7.31 (141,1) [169861,0]. _t65 => ~box 1~ _t66 [ SNF ] [ Backward Subsumption, 170683 ] % 7.12/7.31 (1,1) [169862,0]. true => _t65 | ~_t0 [ SNF ] [ Backward Subsumption, 170582 ] % 7.12/7.31 (1,1) [170582,0]. true => _t65 [ Unit Resolution, 3, 169862, _t0 ] [ Modal Level Pure Literal Elimination, _t65 ] % 7.12/7.31 (1,1) [170592,0]. true => _t9 [ Unit Resolution, 3, 158077, _t0 ] [ Modal Level Pure Literal Elimination, _t9 ] % 7.12/7.31 (1,1) [170596,0]. true => _t19 [ Unit Resolution, 3, 150568, _t0 ] [ Modal Level Pure Literal Elimination, _t19 ] % 7.12/7.31 (1,1) [170669,0]. true => box 1 _t19 [ LHS Unit Resolution, 170596, 150097, _t19 ] [ SNF++, 223428, _t19 ] % 7.12/7.31 (1,1) [170673,0]. true => box 1 _t9 [ LHS Unit Resolution, 170592, 157606, _t9 ] [ SNF++, 223436, _t9 ] % 7.12/7.31 (141,1) [170683,0]. true => ~box 1~ _t66 [ LHS Unit Resolution, 170582, 169861, _t65 ] [ SNF++, 223466, _t66 ] % 7.12/7.31 (1,1) [223428,0]. true => box 1 _t96 [ SNF++, 170669 ] % 7.12/7.31 (1,1) [223436,0]. true => box 1 _t82 [ SNF++, 170673 ] % 7.12/7.31 (141,1) [223466,0]. true => ~box 1~ _t151 [ SNF++, 170683 ] % 7.12/7.31 (141,1) [409264,0]. true => false [ GEN1, 223428, 223436, 223466, 404147, _t96, _t82, _t151 ] % 7.12/7.31 (1,1) [138383,1]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 223290, _t20 ] % 7.12/7.31 (1,1) [147749,1]. _t9 => box 1 _t9 [ Axiom 4 ] [ SNF++, 223284, _t9 ] % 7.12/7.31 (1,1) [149627,1]. _t20 => box 1 _t20 [ Axiom 4 ] [ SNF++, 223288, _t20 ] % 7.12/7.31 (140,1) [169860,1]. _t66 => ~box 1~ _t67 [ SNF ] [ SNF++, 223354, _t67 ] % 7.12/7.31 (1,1) [223284,1]. _t9 => box 1 _t82 [ SNF++, 147749 ] % 7.12/7.31 (1,1) [223290,1]. _t19 => box 1 _t95 [ SNF++, 138383 ] % 7.12/7.31 (140,1) [223354,1]. _t66 => ~box 1~ _t150 [ SNF++, 169860 ] % 7.12/7.31 (1,1) [223429,1]. true => ~_t96 | _t19 [ SNF++, 170669 ] % 7.12/7.31 (1,1) [223437,1]. true => ~_t82 | _t9 [ SNF++, 170673 ] % 7.12/7.31 (141,1) [223467,1]. true => ~_t151 | _t66 [ SNF++, 170683 ] % 7.12/7.31 (140,1) [388451,1]. true => ~_t66 | ~_t19 | ~_t9 [ GEN1, 223290, 223284, 223354, 388151, _t95, _t82, _t150 ] % 7.12/7.31 (140,1) [388455,1]. true => ~_t82 | ~_t66 | ~_t19 [ LRES, 388451, 223437, ~_t9 ] % 7.12/7.31 (140,1) [388903,1]. true => ~_t96 | ~_t82 | ~_t66 [ LRES, 388455, 223429, ~_t19 ] % 7.12/7.31 (141,1) [404147,1]. true => ~_t151 | ~_t96 | ~_t82 [ LRES, 388903, 223467, ~_t66 ] % 7.12/7.31 (1,1) [135573,2]. _t9 => box 1 _t10 [ SNF ] [ SNF++, 223074, _t10 ] % 7.12/7.31 (1,1) [137915,2]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 223078, _t21 ] % 7.12/7.31 (1,1) [147281,2]. _t10 => box 1 _t10 [ Axiom 4 ] [ SNF++, 223072, _t10 ] % 7.12/7.31 (1,1) [149159,2]. _t21 => box 1 _t21 [ Axiom 4 ] [ SNF++, 223076, _t21 ] % 7.12/7.31 (139,1) [169859,2]. _t67 => ~box 1~ _t68 [ SNF ] [ SNF++, 223132, _t68 ] % 7.12/7.31 (1,1) [223074,2]. _t9 => box 1 _t81 [ SNF++, 135573 ] % 7.12/7.31 (1,1) [223078,2]. _t20 => box 1 _t94 [ SNF++, 137915 ] % 7.12/7.31 (139,1) [223132,2]. _t67 => ~box 1~ _t149 [ SNF++, 169859 ] % 7.12/7.31 (1,1) [223285,2]. true => ~_t82 | _t9 [ SNF++, 147749 ] % 7.12/7.31 (1,1) [223289,2]. true => ~_t95 | _t20 [ SNF++, 149627 ] % 7.12/7.31 (140,1) [223355,2]. true => ~_t150 | _t67 [ SNF++, 169860 ] % 7.12/7.31 (139,1) [374108,2]. true => ~_t67 | ~_t20 | ~_t9 [ GEN1, 223078, 223074, 223132, 373893, _t94, _t81, _t149 ] % 7.12/7.31 (139,1) [374675,2]. true => ~_t82 | ~_t67 | ~_t20 [ LRES, 374108, 223285, ~_t9 ] % 7.12/7.31 (139,1) [374698,2]. true => ~_t95 | ~_t82 | ~_t67 [ LRES, 374675, 223289, ~_t20 ] % 7.12/7.31 (140,1) [388151,2]. true => ~_t150 | ~_t95 | ~_t82 [ LRES, 374698, 223355, ~_t67 ] % 7.12/7.31 (1,1) [135108,3]. _t10 => box 1 _t10 [ Axiom 4 ] [ SNF++, 222840, _t10 ] % 7.12/7.31 (1,1) [137450,3]. _t21 => box 1 _t21 [ Axiom 4 ] [ SNF++, 222844, _t21 ] % 7.12/7.31 (138,1) [169858,3]. _t68 => ~box 1~ _t69 [ SNF ] [ SNF++, 222900, _t69 ] % 7.12/7.31 (1,1) [222840,3]. _t10 => box 1 _t81 [ SNF++, 135108 ] % 7.12/7.31 (1,1) [222844,3]. _t21 => box 1 _t94 [ SNF++, 137450 ] % 7.12/7.31 (138,1) [222900,3]. _t68 => ~box 1~ _t148 [ SNF++, 169858 ] % 7.12/7.31 (1,1) [223073,3]. true => ~_t81 | _t10 [ SNF++, 147281 ] % 7.12/7.31 (1,1) [223077,3]. true => ~_t94 | _t21 [ SNF++, 149159 ] % 7.12/7.31 (139,1) [223133,3]. true => ~_t149 | _t68 [ SNF++, 169859 ] % 7.12/7.31 (138,1) [336121,3]. true => ~_t68 | ~_t21 | ~_t10 [ GEN1, 222844, 222840, 222900, 334876, _t94, _t81, _t148 ] % 7.12/7.31 (138,1) [336124,3]. true => ~_t81 | ~_t68 | ~_t21 [ LRES, 336121, 223073, ~_t10 ] % 7.12/7.31 (138,1) [341724,3]. true => ~_t94 | ~_t81 | ~_t68 [ LRES, 336124, 223077, ~_t21 ] % 7.12/7.31 (139,1) [373893,3]. true => ~_t149 | ~_t94 | ~_t81 [ LRES, 341724, 223133, ~_t68 ] % 7.12/7.31 (1,1) [120627,4]. _t10 => box 1 _t10 [ Axiom 4 ] [ SNF++, 222608, _t10 ] % 7.12/7.31 (1,1) [123431,4]. _t21 => box 1 _t21 [ Axiom 4 ] [ SNF++, 222612, _t21 ] % 7.12/7.31 (137,1) [169857,4]. _t69 => ~box 1~ _t70 [ SNF ] [ SNF++, 222668, _t70 ] % 7.12/7.31 (1,1) [222608,4]. _t10 => box 1 _t81 [ SNF++, 120627 ] % 7.12/7.31 (1,1) [222612,4]. _t21 => box 1 _t94 [ SNF++, 123431 ] % 7.12/7.31 (137,1) [222668,4]. _t69 => ~box 1~ _t147 [ SNF++, 169857 ] % 7.12/7.31 (1,1) [222841,4]. true => ~_t81 | _t10 [ SNF++, 135108 ] % 7.12/7.31 (1,1) [222845,4]. true => ~_t94 | _t21 [ SNF++, 137450 ] % 7.12/7.31 (138,1) [222901,4]. true => ~_t148 | _t69 [ SNF++, 169858 ] % 7.12/7.31 (137,1) [333262,4]. true => ~_t69 | ~_t21 | ~_t10 [ GEN1, 222612, 222608, 222668, 332666, _t94, _t81, _t147 ] % 7.12/7.31 (137,1) [333265,4]. true => ~_t81 | ~_t69 | ~_t21 [ LRES, 333262, 222841, ~_t10 ] % 7.12/7.31 (137,1) [333534,4]. true => ~_t94 | ~_t81 | ~_t69 [ LRES, 333265, 222845, ~_t21 ] % 7.12/7.31 (138,1) [334876,4]. true => ~_t148 | ~_t94 | ~_t81 [ LRES, 333534, 222901, ~_t69 ] % 7.12/7.31 (1,1) [103848,5]. _t10 => box 1 _t10 [ Axiom 4 ] [ SNF++, 222376, _t10 ] % 7.12/7.31 (1,1) [107112,5]. _t21 => box 1 _t21 [ Axiom 4 ] [ SNF++, 222380, _t21 ] % 7.12/7.31 (136,1) [169856,5]. _t70 => ~box 1~ _t71 [ SNF ] [ SNF++, 222436, _t71 ] % 7.12/7.31 (1,1) [222376,5]. _t10 => box 1 _t81 [ SNF++, 103848 ] % 7.12/7.31 (1,1) [222380,5]. _t21 => box 1 _t94 [ SNF++, 107112 ] % 7.12/7.31 (136,1) [222436,5]. _t70 => ~box 1~ _t146 [ SNF++, 169856 ] % 7.12/7.31 (1,1) [222609,5]. true => ~_t81 | _t10 [ SNF++, 120627 ] % 7.12/7.31 (1,1) [222613,5]. true => ~_t94 | _t21 [ SNF++, 123431 ] % 7.12/7.31 (137,1) [222669,5]. true => ~_t147 | _t70 [ SNF++, 169857 ] % 7.12/7.31 (136,1) [296020,5]. true => ~_t70 | ~_t21 | ~_t10 [ GEN1, 222380, 222376, 222436, 293492, _t94, _t81, _t146 ] % 7.12/7.31 (136,1) [296023,5]. true => ~_t81 | ~_t70 | ~_t21 [ LRES, 296020, 222609, ~_t10 ] % 7.12/7.31 (136,1) [306594,5]. true => ~_t94 | ~_t81 | ~_t70 [ LRES, 296023, 222613, ~_t21 ] % 7.12/7.31 (137,1) [332666,5]. true => ~_t147 | ~_t94 | ~_t81 [ LRES, 306594, 222669, ~_t70 ] % 7.12/7.31 (1,1) [84781,6]. _t10 => box 1 _t10 [ Axiom 4 ] [ SNF++, 222144, _t10 ] % 7.12/7.31 (1,1) [88503,6]. _t21 => box 1 _t21 [ Axiom 4 ] [ SNF++, 222148, _t21 ] % 7.12/7.31 (135,1) [169855,6]. _t71 => ~box 1~ _t72 [ SNF ] [ SNF++, 222204, _t72 ] % 7.12/7.31 (1,1) [222144,6]. _t10 => box 1 _t81 [ SNF++, 84781 ] % 7.12/7.31 (1,1) [222148,6]. _t21 => box 1 _t94 [ SNF++, 88503 ] % 7.12/7.31 (135,1) [222204,6]. _t71 => ~box 1~ _t145 [ SNF++, 169855 ] % 7.12/7.31 (1,1) [222377,6]. true => ~_t81 | _t10 [ SNF++, 103848 ] % 7.12/7.31 (1,1) [222381,6]. true => ~_t94 | _t21 [ SNF++, 107112 ] % 7.12/7.31 (136,1) [222437,6]. true => ~_t146 | _t71 [ SNF++, 169856 ] % 7.12/7.31 (135,1) [276148,6]. true => ~_t71 | ~_t21 | ~_t10 [ GEN1, 222148, 222144, 222204, 274782, _t94, _t81, _t145 ] % 7.12/7.31 (135,1) [276151,6]. true => ~_t81 | ~_t71 | ~_t21 [ LRES, 276148, 222377, ~_t10 ] % 7.12/7.31 (135,1) [285614,6]. true => ~_t94 | ~_t81 | ~_t71 [ LRES, 276151, 222381, ~_t21 ] % 7.12/7.31 (136,1) [293492,6]. true => ~_t146 | ~_t94 | ~_t81 [ LRES, 285614, 222437, ~_t71 ] % 7.12/7.31 (1,1) [63436,7]. _t10 => box 1 _t10 [ Axiom 4 ] [ SNF++, 221912, _t10 ] % 7.12/7.31 (1,1) [67614,7]. _t21 => box 1 _t21 [ Axiom 4 ] [ SNF++, 221916, _t21 ] % 7.12/7.31 (134,1) [169854,7]. _t72 => ~box 1~ _t73 [ SNF ] [ SNF++, 221972, _t73 ] % 7.12/7.31 (1,1) [221912,7]. _t10 => box 1 _t81 [ SNF++, 63436 ] % 7.12/7.31 (1,1) [221916,7]. _t21 => box 1 _t94 [ SNF++, 67614 ] % 7.12/7.31 (134,1) [221972,7]. _t72 => ~box 1~ _t144 [ SNF++, 169854 ] % 7.12/7.31 (1,1) [222145,7]. true => ~_t81 | _t10 [ SNF++, 84781 ] % 7.12/7.31 (1,1) [222149,7]. true => ~_t94 | _t21 [ SNF++, 88503 ] % 7.12/7.31 (135,1) [222205,7]. true => ~_t145 | _t72 [ SNF++, 169855 ] % 7.12/7.31 (134,1) [262140,7]. true => ~_t72 | ~_t21 | ~_t10 [ GEN1, 221916, 221912, 221972, 262125, _t94, _t81, _t144 ] % 7.12/7.31 (134,1) [262143,7]. true => ~_t81 | ~_t72 | ~_t21 [ LRES, 262140, 222145, ~_t10 ] % 7.12/7.31 (134,1) [262664,7]. true => ~_t94 | ~_t81 | ~_t72 [ LRES, 262143, 222149, ~_t21 ] % 7.12/7.31 (135,1) [274782,7]. true => ~_t145 | ~_t94 | ~_t81 [ LRES, 262664, 222205, ~_t72 ] % 7.12/7.31 (1,1) [39823,8]. _t10 => box 1 _t10 [ Axiom 4 ] [ SNF++, 221510, _t10 ] % 7.12/7.31 (1,1) [44455,8]. _t21 => box 1 _t21 [ Axiom 4 ] [ SNF++, 221548, _t21 ] % 7.12/7.31 (133,1) [169853,8]. _t73 => ~box 1~ _t74 [ SNF ] [ SNF++, 221740, _t74 ] % 7.12/7.31 (1,1) [221510,8]. _t10 => box 1 _t81 [ SNF++, 39823 ] % 7.12/7.31 (1,1) [221548,8]. _t21 => box 1 _t94 [ SNF++, 44455 ] % 7.12/7.31 (133,1) [221740,8]. _t73 => ~box 1~ _t143 [ SNF++, 169853 ] % 7.12/7.31 (1,1) [221913,8]. true => ~_t81 | _t10 [ SNF++, 63436 ] % 7.12/7.31 (1,1) [221917,8]. true => ~_t94 | _t21 [ SNF++, 67614 ] % 7.12/7.31 (134,1) [221973,8]. true => ~_t144 | _t73 [ SNF++, 169854 ] % 7.12/7.31 (133,1) [259925,8]. true => ~_t73 | ~_t21 | ~_t10 [ GEN1, 221548, 221510, 221740, 259914, _t94, _t81, _t143 ] % 7.12/7.31 (133,1) [259938,8]. true => ~_t81 | ~_t73 | ~_t21 [ LRES, 259925, 221913, ~_t10 ] % 7.12/7.31 (133,1) [260947,8]. true => ~_t94 | ~_t81 | ~_t73 [ LRES, 259938, 221917, ~_t21 ] % 7.12/7.31 (134,1) [262125,8]. true => ~_t144 | ~_t94 | ~_t81 [ LRES, 260947, 221973, ~_t73 ] % 7.12/7.31 (1,1) [5,9]. _t10 => box 1 _t11 [ SNF ] [ SNF++, 170964, _t11 ] % 7.12/7.31 (1,1) [7609,9]. _t21 => box 1 _t22 [ SNF ] [ SNF++, 171004, _t22 ] % 7.12/7.31 (132,1) [169852,9]. _t74 => ~box 1~ _t75 [ SNF ] [ SNF++, 171194, _t75 ] % 7.12/7.31 (1,1) [170964,9]. _t10 => box 1 _t80 [ SNF++, 5 ] % 7.12/7.31 (1,1) [171004,9]. _t21 => box 1 _t93 [ SNF++, 7609 ] % 7.12/7.31 (132,1) [171194,9]. _t74 => ~box 1~ _t142 [ SNF++, 169852 ] % 7.12/7.31 (1,1) [221511,9]. true => ~_t81 | _t10 [ SNF++, 39823 ] % 7.12/7.31 (1,1) [221549,9]. true => ~_t94 | _t21 [ SNF++, 44455 ] % 7.12/7.31 (133,1) [221741,9]. true => ~_t143 | _t74 [ SNF++, 169853 ] % 7.12/7.31 (132,1) [259663,9]. true => ~_t74 | ~_t21 | ~_t10 [ GEN1, 171004, 170964, 171194, 259650, _t93, _t80, _t142 ] % 7.12/7.31 (132,1) [259667,9]. true => ~_t81 | ~_t74 | ~_t21 [ LRES, 259663, 221511, ~_t10 ] % 7.12/7.31 (132,1) [259903,9]. true => ~_t94 | ~_t81 | ~_t74 [ LRES, 259667, 221549, ~_t21 ] % 7.12/7.31 (133,1) [259914,9]. true => ~_t143 | ~_t94 | ~_t81 [ LRES, 259903, 221741, ~_t74 ] % 7.12/7.31 (3,1) [4,10]. _t11 => ~box 1~ true [ SNF ] % 7.12/7.31 (1,1) [6932,10]. _t23 => box 1 _t24 [ SNF ] [ SNF++, 170780, _t24 ] % 7.12/7.31 (1,1) [7608,10]. true => _t23 | ~_t22 | p0 [ SNF ] % 7.12/7.31 (1,1) [58350,10]. _t64 => box 1 _t64 [ Axiom 4 ] [ SNF++, 170912, _t64 ] % 7.12/7.31 (132,1) [169850,10]. true => ~_t75 | ~p0 [ SNF ] % 7.12/7.31 (132,1) [169851,10]. true => ~_t75 | _t64 [ SNF ] % 7.12/7.31 (1,1) [170780,10]. _t23 => box 1 _t91 [ SNF++, 6932 ] % 7.12/7.31 (1,1) [170912,10]. _t64 => box 1 _t129 [ SNF++, 58350 ] % 7.12/7.31 (1,1) [170965,10]. true => ~_t80 | _t11 [ SNF++, 5 ] % 7.12/7.31 (1,1) [171005,10]. true => ~_t93 | _t22 [ SNF++, 7609 ] % 7.12/7.31 (132,1) [171195,10]. true => ~_t142 | _t75 [ SNF++, 169852 ] % 7.12/7.31 (132,1) [223936,10]. true => ~_t75 | _t23 | ~_t22 [ LRES, 169850, 7608, ~p0 ] % 7.12/7.31 (1,1) [227687,10]. true => ~_t64 | ~_t23 | ~_t11 [ GEN3, 170912, 170780, 226286, 4, _t129, _t91, true ] % 7.12/7.31 (132,1) [231687,10]. true => ~_t93 | ~_t75 | _t23 [ LRES, 223936, 171005, ~_t22 ] % 7.12/7.31 (1,1) [232160,10]. true => ~_t80 | ~_t64 | ~_t23 [ LRES, 227687, 170965, ~_t11 ] % 7.12/7.31 (132,1) [238187,10]. true => ~_t93 | ~_t80 | ~_t75 | ~_t64 [ LRES, 231687, 232160, _t23 ] [ Backward Subsumption, 259636 ] % 7.12/7.31 (132,1) [259636,10]. true => ~_t93 | ~_t80 | ~_t75 [ LRES, 238187, 169851, ~_t64 ] % 7.12/7.31 (132,1) [259650,10]. true => ~_t142 | ~_t93 | ~_t80 [ LRES, 259636, 171195, ~_t75 ] % 7.12/7.31 (11,1) [6931,11]. _t24 => ~box 1~ ~p0 [ SNF ] [ SNF++, 171196, ~p0 ] % 7.12/7.31 (5,1) [24162,11]. _t38 => ~box 1~ p0 [ SNF ] [ SNF++, 171200, p0 ] % 7.12/7.31 (1,1) [31542,11]. _t64 => box 1 p0 [ SNF ] [ SNF++, 171378, p0 ] % 7.12/7.31 (1,1) [170781,11]. true => ~_t91 | _t24 [ SNF++, 6932 ] % 7.12/7.31 (1,1) [170913,11]. true => ~_t129 | _t64 [ SNF++, 58350 ] % 7.12/7.31 (11,1) [171196,11]. _t24 => ~box 1~ _t78 [ SNF++, 6931 ] % 7.12/7.31 (1,1) [171378,11]. _t64 => box 1 _t79 [ SNF++, 31542 ] % 7.12/7.31 (11,1) [223948,11]. true => ~_t64 | ~_t24 [ GEN1, 171378, 171196, 223473, _t79, _t78 ] % 7.12/7.31 (11,1) [225585,11]. true => ~_t91 | ~_t64 [ LRES, 223948, 170781, ~_t24 ] % 7.12/7.31 (11,1) [226286,11]. true => ~_t129 | ~_t91 [ LRES, 225585, 170913, ~_t64 ] % 7.12/7.31 (11,1) [171197,12]. true => ~_t78 | ~p0 [ SNF++, 6931 ] % 7.32/7.57 (5,1) [171201,12]. true => ~_t79 | p0 [ SNF++, 24162 ] % 7.32/7.57 (11,1) [223473,12]. true => ~_t79 | ~_t78 [ LRES, 171197, 171201, ~p0 ] % 7.32/7.57 % SZS output end Refutation % 7.32/7.58 % KSP exiting %------------------------------------------------------------------------------