%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : GRA076_1.002 : TPTP v9.0.0. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n011.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 : Wed Apr 9 06:24:12 PM UTC 2025 % Result : Theorem 0.43s 0.60s % Output : Refutation 0.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRA076_1.002 : TPTP v9.0.0. Released v9.0.0. % 0.03/0.12 % Command : run_ksp %s % 0.13/0.33 % Computer : n011.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Mon Apr 7 21:04:03 EDT 2025 % 0.13/0.33 % CPUTime : % 0.43/0.59 ----KSP format--- % 0.43/0.59 usable(formulas). % 0.43/0.59 true. % 0.43/0.59 end_of_list. % 0.43/0.59 sos(formulas). % 0.43/0.59 ~ (~ ( ~ ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( p1 & p2 & p3 & p4 & p5 & p6 & p7 & p8 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( false | <> ( ( p1 <-> p2 ) ) ) | [] ( p3 ) | <> ( <> ( ( p2 <-> p3 ) ) ) ) | [] ( p4 ) | <> ( <> ( <> ( ( p3 <-> p4 ) ) ) ) ) | [] ( p5 ) | <> ( <> ( <> ( <> ( ( p4 <-> p5 ) ) ) ) ) ) | [] ( p6 ) | <> ( <> ( <> ( <> ( <> ( ( p5 <-> p6 ) ) ) ) ) ) ) | [] ( p7 ) | <> ( <> ( <> ( <> ( <> ( <> ( ( p6 <-> p7 ) ) ) ) ) ) ) ) | [] ( p8 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p7 <-> p1 ) ) ) ) ) ) ) ) ) | [] ( p9 ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( ~ ( p2 ) & ~ ( p4 ) & ~ ( p6 ) & ~ ( p8 ) & ~ ( p10 ) & ~ ( p12 ) & ~ ( p14 ) & ~ ( p16 ) ) ) ) ) ) ) ) ) ) ) ). % 0.43/0.59 end_of_list. % 0.43/0.59 ----------------- % 0.43/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.mD90J18vZY/theBenchmark.ksp % 0.43/0.60 % 0.43/0.60 % SZS status Theorem % 0.43/0.60 % 0.43/0.60 ***************** % 0.43/0.60 FOUND PROOF 1 % 0.43/0.60 ***************** % 0.43/0.60 % SZS output start Refutation % 0.43/0.60 % 0.43/0.60 (1,1) [1,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.43/0.60 (1,1) [70,0]. _t0 => box 1 _t2 [ SNF ] [ Backward Subsumption, 89 ] % 0.43/0.60 (45,1) [78,0]. _t0 => ~box 1~ _t70 [ SNF ] [ Backward Subsumption, 88 ] % 0.43/0.60 (45,1) [88,0]. true => ~box 1~ _t70 [ LHS Unit Resolution, 1, 78, _t0 ] [ SNF++, 172, _t70 ] % 0.43/0.60 (1,1) [89,0]. true => box 1 _t2 [ LHS Unit Resolution, 1, 70, _t0 ] [ SNF++, 170, _t2 ] % 0.43/0.60 (1,1) [170,0]. true => box 1 _t117 [ SNF++, 89 ] % 0.43/0.60 (45,1) [172,0]. true => ~box 1~ _t118 [ SNF++, 88 ] % 0.43/0.60 (45,1) [269,0]. true => false [ GEN1, 170, 172, 268, _t117, _t118 ] % 0.43/0.60 (1,1) [12,1]. _t2 => box 1 _t4 [ SNF ] [ SNF++, 164, _t4 ] % 0.43/0.60 (1,1) [68,1]. _t2 => box 1 _t14 [ SNF ] [ SNF++, 166, _t14 ] % 0.43/0.60 (44,1) [77,1]. _t70 => ~box 1~ _t71 [ SNF ] [ SNF++, 168, _t71 ] % 0.43/0.60 (1,1) [164,1]. _t2 => box 1 _t114 [ SNF++, 12 ] % 0.43/0.60 (1,1) [166,1]. _t2 => box 1 _t115 [ SNF++, 68 ] % 0.43/0.60 (44,1) [168,1]. _t70 => ~box 1~ _t116 [ SNF++, 77 ] % 0.43/0.60 (1,1) [171,1]. true => ~_t117 | _t2 [ SNF++, 89 ] % 0.43/0.60 (45,1) [173,1]. true => ~_t118 | _t70 [ SNF++, 88 ] % 0.43/0.60 (44,1) [266,1]. true => ~_t70 | ~_t2 [ GEN1, 166, 164, 168, 265, _t115, _t114, _t116 ] % 0.43/0.60 (44,1) [267,1]. true => ~_t117 | ~_t70 [ LRES, 266, 171, ~_t2 ] % 0.43/0.60 (45,1) [268,1]. true => ~_t118 | ~_t117 [ LRES, 267, 173, ~_t70 ] % 0.43/0.60 (1,1) [11,2]. _t4 => box 1 _t5 [ SNF ] [ SNF++, 156, _t5 ] % 0.43/0.60 (1,1) [22,2]. _t14 => box 1 _t16 [ SNF ] [ SNF++, 158, _t16 ] % 0.43/0.60 (1,1) [66,2]. _t14 => box 1 _t25 [ SNF ] [ SNF++, 160, _t25 ] % 0.43/0.60 (43,1) [76,2]. _t71 => ~box 1~ _t72 [ SNF ] [ SNF++, 162, _t72 ] % 0.43/0.60 (1,1) [156,2]. _t4 => box 1 _t110 [ SNF++, 11 ] % 0.43/0.60 (1,1) [158,2]. _t14 => box 1 _t111 [ SNF++, 22 ] % 0.43/0.60 (1,1) [160,2]. _t14 => box 1 _t112 [ SNF++, 66 ] % 0.43/0.60 (43,1) [162,2]. _t71 => ~box 1~ _t113 [ SNF++, 76 ] % 0.43/0.60 (1,1) [165,2]. true => ~_t114 | _t4 [ SNF++, 12 ] % 0.43/0.60 (1,1) [167,2]. true => ~_t115 | _t14 [ SNF++, 68 ] % 0.43/0.60 (44,1) [169,2]. true => ~_t116 | _t71 [ SNF++, 77 ] % 0.43/0.60 (43,1) [262,2]. true => ~_t71 | ~_t14 | ~_t4 [ GEN1, 160, 156, 158, 162, 261, _t112, _t110, _t111, _t113 ] % 0.43/0.60 (43,1) [263,2]. true => ~_t114 | ~_t71 | ~_t14 [ LRES, 262, 165, ~_t4 ] % 0.43/0.60 (43,1) [264,2]. true => ~_t115 | ~_t114 | ~_t71 [ LRES, 263, 167, ~_t14 ] % 0.43/0.60 (44,1) [265,2]. true => ~_t116 | ~_t115 | ~_t114 [ LRES, 264, 169, ~_t71 ] % 0.43/0.60 (1,1) [10,3]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 146, _t6 ] % 0.43/0.60 (1,1) [21,3]. _t16 => box 1 _t17 [ SNF ] [ SNF++, 148, _t17 ] % 0.43/0.60 (1,1) [31,3]. _t25 => box 1 _t27 [ SNF ] [ SNF++, 150, _t27 ] % 0.43/0.60 (1,1) [64,3]. _t25 => box 1 _t35 [ SNF ] [ SNF++, 152, _t35 ] % 0.43/0.60 (42,1) [75,3]. _t72 => ~box 1~ _t73 [ SNF ] [ SNF++, 154, _t73 ] % 0.43/0.60 (1,1) [146,3]. _t5 => box 1 _t105 [ SNF++, 10 ] % 0.43/0.60 (1,1) [148,3]. _t16 => box 1 _t106 [ SNF++, 21 ] % 0.43/0.60 (1,1) [150,3]. _t25 => box 1 _t107 [ SNF++, 31 ] % 0.43/0.60 (1,1) [152,3]. _t25 => box 1 _t108 [ SNF++, 64 ] % 0.43/0.60 (42,1) [154,3]. _t72 => ~box 1~ _t109 [ SNF++, 75 ] % 0.43/0.60 (1,1) [157,3]. true => ~_t110 | _t5 [ SNF++, 11 ] % 0.43/0.60 (1,1) [159,3]. true => ~_t111 | _t16 [ SNF++, 22 ] % 0.43/0.60 (1,1) [161,3]. true => ~_t112 | _t25 [ SNF++, 66 ] % 0.43/0.60 (43,1) [163,3]. true => ~_t113 | _t72 [ SNF++, 76 ] % 0.43/0.60 (42,1) [257,3]. true => ~_t72 | ~_t25 | ~_t16 | ~_t5 [ GEN1, 152, 148, 146, 150, 154, 256, _t108, _t106, _t105, _t107, _t109 ] % 0.43/0.60 (42,1) [258,3]. true => ~_t110 | ~_t72 | ~_t25 | ~_t16 [ LRES, 257, 157, ~_t5 ] % 0.43/0.60 (42,1) [259,3]. true => ~_t111 | ~_t110 | ~_t72 | ~_t25 [ LRES, 258, 159, ~_t16 ] % 0.43/0.60 (42,1) [260,3]. true => ~_t112 | ~_t111 | ~_t110 | ~_t72 [ LRES, 259, 161, ~_t25 ] % 0.43/0.60 (43,1) [261,3]. true => ~_t113 | ~_t112 | ~_t111 | ~_t110 [ LRES, 260, 163, ~_t72 ] % 0.43/0.60 (1,1) [9,4]. _t6 => box 1 _t7 [ SNF ] [ SNF++, 134, _t7 ] % 0.43/0.60 (1,1) [20,4]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 136, _t18 ] % 0.43/0.60 (1,1) [30,4]. _t27 => box 1 _t28 [ SNF ] [ SNF++, 138, _t28 ] % 0.43/0.60 (1,1) [39,4]. _t35 => box 1 _t37 [ SNF ] [ SNF++, 140, _t37 ] % 0.43/0.60 (1,1) [62,4]. _t35 => box 1 _t44 [ SNF ] [ SNF++, 142, _t44 ] % 0.43/0.60 (41,1) [74,4]. _t73 => ~box 1~ _t74 [ SNF ] [ SNF++, 144, _t74 ] % 0.43/0.60 (1,1) [134,4]. _t6 => box 1 _t99 [ SNF++, 9 ] % 0.43/0.60 (1,1) [136,4]. _t17 => box 1 _t100 [ SNF++, 20 ] % 0.43/0.60 (1,1) [138,4]. _t27 => box 1 _t101 [ SNF++, 30 ] % 0.43/0.60 (1,1) [140,4]. _t35 => box 1 _t102 [ SNF++, 39 ] % 0.43/0.60 (1,1) [142,4]. _t35 => box 1 _t103 [ SNF++, 62 ] % 0.43/0.60 (41,1) [144,4]. _t73 => ~box 1~ _t104 [ SNF++, 74 ] % 0.43/0.60 (1,1) [147,4]. true => ~_t105 | _t6 [ SNF++, 10 ] % 0.43/0.60 (1,1) [149,4]. true => ~_t106 | _t17 [ SNF++, 21 ] % 0.43/0.60 (1,1) [151,4]. true => ~_t107 | _t27 [ SNF++, 31 ] % 0.43/0.60 (1,1) [153,4]. true => ~_t108 | _t35 [ SNF++, 64 ] % 0.43/0.60 (42,1) [155,4]. true => ~_t109 | _t73 [ SNF++, 75 ] % 0.43/0.60 (41,1) [251,4]. true => ~_t73 | ~_t35 | ~_t27 | ~_t17 | ~_t6 [ GEN1, 142, 138, 134, 136, 140, 144, 250, _t103, _t101, _t99, _t100, _t102, _t104 ] % 0.43/0.60 (41,1) [252,4]. true => ~_t105 | ~_t73 | ~_t35 | ~_t27 | ~_t17 [ LRES, 251, 147, ~_t6 ] % 0.43/0.60 (41,1) [253,4]. true => ~_t106 | ~_t105 | ~_t73 | ~_t35 | ~_t27 [ LRES, 252, 149, ~_t17 ] % 0.43/0.60 (41,1) [254,4]. true => ~_t107 | ~_t106 | ~_t105 | ~_t73 | ~_t35 [ LRES, 253, 151, ~_t27 ] % 0.43/0.60 (41,1) [255,4]. true => ~_t108 | ~_t107 | ~_t106 | ~_t105 | ~_t73 [ LRES, 254, 153, ~_t35 ] % 0.43/0.60 (42,1) [256,4]. true => ~_t109 | ~_t108 | ~_t107 | ~_t106 | ~_t105 [ LRES, 255, 155, ~_t73 ] % 0.43/0.60 (1,1) [8,5]. _t7 => box 1 _t8 [ SNF ] [ SNF++, 120, _t8 ] % 0.43/0.60 (1,1) [19,5]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 122, _t19 ] % 0.43/0.60 (1,1) [29,5]. _t28 => box 1 _t29 [ SNF ] [ SNF++, 124, _t29 ] % 0.43/0.60 (1,1) [38,5]. _t37 => box 1 _t38 [ SNF ] [ SNF++, 126, _t38 ] % 0.43/0.60 (1,1) [46,5]. _t44 => box 1 _t46 [ SNF ] [ SNF++, 128, _t46 ] % 0.43/0.60 (1,1) [60,5]. _t44 => box 1 _t52 [ SNF ] [ SNF++, 130, _t52 ] % 0.43/0.60 (40,1) [73,5]. _t74 => ~box 1~ _t75 [ SNF ] [ SNF++, 132, _t75 ] % 0.43/0.60 (1,1) [120,5]. _t7 => box 1 _t92 [ SNF++, 8 ] % 0.43/0.60 (1,1) [122,5]. _t18 => box 1 _t93 [ SNF++, 19 ] % 0.43/0.60 (1,1) [124,5]. _t28 => box 1 _t94 [ SNF++, 29 ] % 0.43/0.60 (1,1) [126,5]. _t37 => box 1 _t95 [ SNF++, 38 ] % 0.43/0.60 (1,1) [128,5]. _t44 => box 1 _t96 [ SNF++, 46 ] % 0.43/0.60 (1,1) [130,5]. _t44 => box 1 _t97 [ SNF++, 60 ] % 0.43/0.60 (40,1) [132,5]. _t74 => ~box 1~ _t98 [ SNF++, 73 ] % 0.43/0.60 (1,1) [135,5]. true => ~_t99 | _t7 [ SNF++, 9 ] % 0.43/0.60 (1,1) [137,5]. true => ~_t100 | _t18 [ SNF++, 20 ] % 0.43/0.60 (1,1) [139,5]. true => ~_t101 | _t28 [ SNF++, 30 ] % 0.43/0.60 (1,1) [141,5]. true => ~_t102 | _t37 [ SNF++, 39 ] % 0.43/0.60 (1,1) [143,5]. true => ~_t103 | _t44 [ SNF++, 62 ] % 0.43/0.60 (41,1) [145,5]. true => ~_t104 | _t74 [ SNF++, 74 ] % 0.43/0.60 (40,1) [244,5]. true => ~_t74 | ~_t44 | ~_t37 | ~_t28 | ~_t18 | ~_t7 [ GEN1, 130, 126, 122, 120, 124, 128, 132, 243, _t97, _t95, _t93, _t92, _t94, _t96, _t98 ] % 0.43/0.60 (40,1) [245,5]. true => ~_t99 | ~_t74 | ~_t44 | ~_t37 | ~_t28 | ~_t18 [ LRES, 244, 135, ~_t7 ] % 0.43/0.60 (40,1) [246,5]. true => ~_t100 | ~_t99 | ~_t74 | ~_t44 | ~_t37 | ~_t28 [ LRES, 245, 137, ~_t18 ] % 0.43/0.60 (40,1) [247,5]. true => ~_t101 | ~_t100 | ~_t99 | ~_t74 | ~_t44 | ~_t37 [ LRES, 246, 139, ~_t28 ] % 0.43/0.60 (40,1) [248,5]. true => ~_t102 | ~_t101 | ~_t100 | ~_t99 | ~_t74 | ~_t44 [ LRES, 247, 141, ~_t37 ] % 0.43/0.60 (40,1) [249,5]. true => ~_t103 | ~_t102 | ~_t101 | ~_t100 | ~_t99 | ~_t74 [ LRES, 248, 143, ~_t44 ] % 0.43/0.60 (41,1) [250,5]. true => ~_t104 | ~_t103 | ~_t102 | ~_t101 | ~_t100 | ~_t99 [ LRES, 249, 145, ~_t74 ] % 0.43/0.60 (1,1) [7,6]. _t8 => box 1 _t9 [ SNF ] [ SNF++, 104, _t9 ] % 0.43/0.60 (1,1) [18,6]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 106, _t20 ] % 0.43/0.60 (1,1) [28,6]. _t29 => box 1 _t30 [ SNF ] [ SNF++, 108, _t30 ] % 0.43/0.60 (1,1) [37,6]. _t38 => box 1 _t39 [ SNF ] [ SNF++, 110, _t39 ] % 0.43/0.60 (1,1) [45,6]. _t46 => box 1 _t47 [ SNF ] [ SNF++, 112, _t47 ] % 0.43/0.60 (1,1) [52,6]. _t52 => box 1 _t54 [ SNF ] [ SNF++, 114, _t54 ] % 0.43/0.60 (1,1) [58,6]. _t52 => box 1 _t59 [ SNF ] [ SNF++, 116, _t59 ] % 0.43/0.60 (39,1) [72,6]. _t75 => ~box 1~ _t68 [ SNF ] [ SNF++, 118, _t68 ] % 0.43/0.60 (1,1) [104,6]. _t8 => box 1 _t84 [ SNF++, 7 ] % 0.43/0.60 (1,1) [106,6]. _t19 => box 1 _t85 [ SNF++, 18 ] % 0.43/0.60 (1,1) [108,6]. _t29 => box 1 _t86 [ SNF++, 28 ] % 0.43/0.60 (1,1) [110,6]. _t38 => box 1 _t87 [ SNF++, 37 ] % 0.43/0.60 (1,1) [112,6]. _t46 => box 1 _t88 [ SNF++, 45 ] % 0.43/0.60 (1,1) [114,6]. _t52 => box 1 _t89 [ SNF++, 52 ] % 0.43/0.60 (1,1) [116,6]. _t52 => box 1 _t90 [ SNF++, 58 ] % 0.43/0.60 (39,1) [118,6]. _t75 => ~box 1~ _t91 [ SNF++, 72 ] % 0.43/0.60 (1,1) [121,6]. true => ~_t92 | _t8 [ SNF++, 8 ] % 0.43/0.60 (1,1) [123,6]. true => ~_t93 | _t19 [ SNF++, 19 ] % 0.43/0.60 (1,1) [125,6]. true => ~_t94 | _t29 [ SNF++, 29 ] % 0.43/0.60 (1,1) [127,6]. true => ~_t95 | _t38 [ SNF++, 38 ] % 0.43/0.60 (1,1) [129,6]. true => ~_t96 | _t46 [ SNF++, 46 ] % 0.43/0.60 (1,1) [131,6]. true => ~_t97 | _t52 [ SNF++, 60 ] % 0.43/0.60 (40,1) [133,6]. true => ~_t98 | _t75 [ SNF++, 73 ] % 0.43/0.60 (39,1) [236,6]. true => ~_t75 | ~_t52 | ~_t46 | ~_t38 | ~_t29 | ~_t19 | ~_t8 [ GEN1, 116, 112, 108, 104, 106, 110, 114, 118, 235, _t90, _t88, _t86, _t84, _t85, _t87, _t89, _t91 ] % 0.43/0.60 (39,1) [237,6]. true => ~_t92 | ~_t75 | ~_t52 | ~_t46 | ~_t38 | ~_t29 | ~_t19 [ LRES, 236, 121, ~_t8 ] % 0.43/0.60 (39,1) [238,6]. true => ~_t93 | ~_t92 | ~_t75 | ~_t52 | ~_t46 | ~_t38 | ~_t29 [ LRES, 237, 123, ~_t19 ] % 0.43/0.60 (39,1) [239,6]. true => ~_t94 | ~_t93 | ~_t92 | ~_t75 | ~_t52 | ~_t46 | ~_t38 [ LRES, 238, 125, ~_t29 ] % 0.43/0.60 (39,1) [240,6]. true => ~_t95 | ~_t94 | ~_t93 | ~_t92 | ~_t75 | ~_t52 | ~_t46 [ LRES, 239, 127, ~_t38 ] % 0.43/0.60 (39,1) [241,6]. true => ~_t96 | ~_t95 | ~_t94 | ~_t93 | ~_t92 | ~_t75 | ~_t52 [ LRES, 240, 129, ~_t46 ] % 0.43/0.60 (39,1) [242,6]. true => ~_t97 | ~_t96 | ~_t95 | ~_t94 | ~_t93 | ~_t92 | ~_t75 [ LRES, 241, 131, ~_t52 ] % 0.43/0.60 (40,1) [243,6]. true => ~_t98 | ~_t97 | ~_t96 | ~_t95 | ~_t94 | ~_t93 | ~_t92 [ LRES, 242, 133, ~_t75 ] % 0.43/0.60 (1,1) [6,7]. _t9 => box 1 _t10 [ SNF ] [ SNF++, 90, _t10 ] % 0.43/0.60 (1,1) [17,7]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 92, _t21 ] % 0.43/0.60 (1,1) [27,7]. _t30 => box 1 _t31 [ SNF ] [ SNF++, 94, _t31 ] % 0.43/0.60 (1,1) [36,7]. _t39 => box 1 _t40 [ SNF ] [ SNF++, 96, _t40 ] % 0.43/0.60 (1,1) [44,7]. _t47 => box 1 _t48 [ SNF ] [ SNF++, 98, _t48 ] % 0.43/0.60 (1,1) [51,7]. _t54 => box 1 _t55 [ SNF ] [ SNF++, 100, _t55 ] % 0.43/0.60 (1,1) [57,7]. _t59 => box 1 _t60 [ SNF ] [ SNF++, 102, _t60 ] % 0.43/0.60 (38,1) [71,7]. _t68 => ~box 1~ true [ SNF ] % 0.43/0.60 (1,1) [90,7]. _t9 => box 1 _t77 [ SNF++, 6 ] % 0.43/0.60 (1,1) [92,7]. _t20 => box 1 _t78 [ SNF++, 17 ] % 0.43/0.60 (1,1) [94,7]. _t30 => box 1 _t79 [ SNF++, 27 ] % 0.43/0.60 (1,1) [96,7]. _t39 => box 1 _t80 [ SNF++, 36 ] % 0.43/0.60 (1,1) [98,7]. _t47 => box 1 _t81 [ SNF++, 44 ] % 0.43/0.60 (1,1) [100,7]. _t54 => box 1 _t82 [ SNF++, 51 ] % 0.43/0.60 (1,1) [102,7]. _t59 => box 1 _t83 [ SNF++, 57 ] % 0.43/0.60 (1,1) [105,7]. true => ~_t84 | _t9 [ SNF++, 7 ] % 0.43/0.60 (1,1) [107,7]. true => ~_t85 | _t20 [ SNF++, 18 ] % 0.43/0.60 (1,1) [109,7]. true => ~_t86 | _t30 [ SNF++, 28 ] % 0.43/0.60 (1,1) [111,7]. true => ~_t87 | _t39 [ SNF++, 37 ] % 0.43/0.60 (1,1) [113,7]. true => ~_t88 | _t47 [ SNF++, 45 ] % 0.43/0.60 (1,1) [115,7]. true => ~_t89 | _t54 [ SNF++, 52 ] % 0.43/0.60 (1,1) [117,7]. true => ~_t90 | _t59 [ SNF++, 58 ] % 0.43/0.60 (39,1) [119,7]. true => ~_t91 | _t68 [ SNF++, 72 ] % 0.43/0.60 (1,1) [227,7]. true => ~_t68 | ~_t59 | ~_t54 | ~_t47 | ~_t39 | ~_t30 | ~_t20 | ~_t9 [ GEN3, 92, 96, 100, 102, 98, 94, 90, 226, 71, _t78, _t80, _t82, _t83, _t81, _t79, _t77, true ] % 0.43/0.60 (1,1) [228,7]. true => ~_t84 | ~_t68 | ~_t59 | ~_t54 | ~_t47 | ~_t39 | ~_t30 | ~_t20 [ LRES, 227, 105, ~_t9 ] % 0.43/0.60 (1,1) [229,7]. true => ~_t85 | ~_t84 | ~_t68 | ~_t59 | ~_t54 | ~_t47 | ~_t39 | ~_t30 [ LRES, 228, 107, ~_t20 ] % 0.43/0.60 (1,1) [230,7]. true => ~_t86 | ~_t85 | ~_t84 | ~_t68 | ~_t59 | ~_t54 | ~_t47 | ~_t39 [ LRES, 229, 109, ~_t30 ] % 0.43/0.60 (1,1) [231,7]. true => ~_t87 | ~_t86 | ~_t85 | ~_t84 | ~_t68 | ~_t59 | ~_t54 | ~_t47 [ LRES, 230, 111, ~_t39 ] % 0.43/0.60 (1,1) [232,7]. true => ~_t88 | ~_t87 | ~_t86 | ~_t85 | ~_t84 | ~_t68 | ~_t59 | ~_t54 [ LRES, 231, 113, ~_t47 ] % 0.43/0.60 (1,1) [233,7]. true => ~_t89 | ~_t88 | ~_t87 | ~_t86 | ~_t85 | ~_t84 | ~_t68 | ~_t59 [ LRES, 232, 115, ~_t54 ] % 0.43/0.60 (1,1) [234,7]. true => ~_t90 | ~_t89 | ~_t88 | ~_t87 | ~_t86 | ~_t85 | ~_t84 | ~_t68 [ LRES, 233, 117, ~_t59 ] % 0.43/0.60 (39,1) [235,7]. true => ~_t91 | ~_t90 | ~_t89 | ~_t88 | ~_t87 | ~_t86 | ~_t85 | ~_t84 [ LRES, 234, 119, ~_t68 ] % 0.43/0.60 (1,1) [2,8]. true => ~_t11 | p7 | p1 [ SNF ] % 0.43/0.60 (1,1) [3,8]. true => _t11 | ~_t10 [ SNF ] % 0.43/0.60 (1,1) [4,8]. true => ~_t12 | ~p7 | ~p1 [ SNF ] % 0.43/0.60 (1,1) [5,8]. true => _t12 | ~_t10 [ SNF ] % 0.43/0.60 (1,1) [13,8]. true => ~_t22 | p7 | p6 [ SNF ] % 0.43/0.60 (1,1) [14,8]. true => _t22 | ~_t21 [ SNF ] % 0.43/0.60 (1,1) [15,8]. true => ~_t23 | ~p7 | ~p6 [ SNF ] % 0.43/0.60 (1,1) [16,8]. true => _t23 | ~_t21 [ SNF ] % 0.43/0.60 (1,1) [23,8]. true => ~_t32 | p6 | p5 [ SNF ] % 0.43/0.60 (1,1) [24,8]. true => _t32 | ~_t31 [ SNF ] % 0.43/0.60 (1,1) [25,8]. true => ~_t33 | ~p6 | ~p5 [ SNF ] % 0.43/0.60 (1,1) [26,8]. true => _t33 | ~_t31 [ SNF ] % 0.43/0.60 (1,1) [32,8]. true => ~_t41 | p5 | p4 [ SNF ] % 0.43/0.60 (1,1) [33,8]. true => _t41 | ~_t40 [ SNF ] % 0.43/0.60 (1,1) [34,8]. true => ~_t42 | ~p5 | ~p4 [ SNF ] % 0.43/0.60 (1,1) [35,8]. true => _t42 | ~_t40 [ SNF ] % 0.43/0.60 (1,1) [40,8]. true => ~_t49 | p4 | p3 [ SNF ] % 0.43/0.60 (1,1) [41,8]. true => _t49 | ~_t48 [ SNF ] % 0.43/0.60 (1,1) [42,8]. true => ~_t50 | ~p4 | ~p3 [ SNF ] % 0.43/0.60 (1,1) [43,8]. true => _t50 | ~_t48 [ SNF ] % 0.43/0.60 (1,1) [47,8]. true => ~_t56 | p3 | p2 [ SNF ] % 0.43/0.60 (1,1) [48,8]. true => _t56 | ~_t55 [ SNF ] % 0.43/0.60 (1,1) [49,8]. true => ~_t57 | ~p3 | ~p2 [ SNF ] % 0.43/0.60 (1,1) [50,8]. true => _t57 | ~_t55 [ SNF ] % 0.43/0.60 (1,1) [53,8]. true => ~_t61 | p2 | p1 [ SNF ] % 0.43/0.60 (1,1) [54,8]. true => _t61 | ~_t60 [ SNF ] % 0.43/0.60 (1,1) [55,8]. true => ~_t62 | ~p2 | ~p1 [ SNF ] % 0.43/0.60 (1,1) [56,8]. true => _t62 | ~_t60 [ SNF ] % 0.43/0.60 (1,1) [91,8]. true => ~_t77 | _t10 [ SNF++, 6 ] % 0.43/0.60 (1,1) [93,8]. true => ~_t78 | _t21 [ SNF++, 17 ] % 0.43/0.60 (1,1) [95,8]. true => ~_t79 | _t31 [ SNF++, 27 ] % 0.43/0.60 (1,1) [97,8]. true => ~_t80 | _t40 [ SNF++, 36 ] % 0.43/0.60 (1,1) [99,8]. true => ~_t81 | _t48 [ SNF++, 44 ] % 0.43/0.60 (1,1) [101,8]. true => ~_t82 | _t55 [ SNF++, 51 ] % 0.43/0.60 (1,1) [103,8]. true => ~_t83 | _t60 [ SNF++, 57 ] % 0.43/0.60 (1,1) [174,8]. true => ~_t77 | _t12 [ LRES, 5, 91, ~_t10 ] % 0.43/0.60 (1,1) [175,8]. true => ~_t77 | _t11 [ LRES, 3, 91, ~_t10 ] % 0.43/0.60 (1,1) [176,8]. true => ~_t78 | _t23 [ LRES, 16, 93, ~_t21 ] % 0.43/0.60 (1,1) [177,8]. true => ~_t78 | _t22 [ LRES, 14, 93, ~_t21 ] % 0.43/0.60 (1,1) [178,8]. true => ~_t79 | _t33 [ LRES, 26, 95, ~_t31 ] % 0.43/0.60 (1,1) [179,8]. true => ~_t79 | _t32 [ LRES, 24, 95, ~_t31 ] % 0.43/0.60 (1,1) [180,8]. true => ~_t80 | _t42 [ LRES, 35, 97, ~_t40 ] % 0.43/0.60 (1,1) [181,8]. true => ~_t80 | _t41 [ LRES, 33, 97, ~_t40 ] % 0.43/0.60 (1,1) [182,8]. true => ~_t81 | _t50 [ LRES, 43, 99, ~_t48 ] % 0.43/0.60 (1,1) [183,8]. true => ~_t81 | _t49 [ LRES, 41, 99, ~_t48 ] % 0.43/0.60 (1,1) [184,8]. true => ~_t82 | _t57 [ LRES, 50, 101, ~_t55 ] % 0.43/0.60 (1,1) [185,8]. true => ~_t82 | _t56 [ LRES, 48, 101, ~_t55 ] % 0.43/0.60 (1,1) [186,8]. true => ~_t83 | _t62 [ LRES, 56, 103, ~_t60 ] % 0.43/0.60 (1,1) [187,8]. true => ~_t83 | _t61 [ LRES, 54, 103, ~_t60 ] % 0.43/0.60 (1,1) [188,8]. true => ~_t62 | ~_t11 | p7 | ~p2 [ LRES, 55, 2, ~p1 ] % 0.43/0.60 (1,1) [191,8]. true => ~_t61 | ~_t12 | ~p7 | p2 [ LRES, 4, 53, ~p1 ] % 0.43/0.60 (1,1) [197,8]. true => ~_t62 | ~_t56 | ~_t11 | p7 | p3 [ LRES, 188, 47, ~p2 ] % 0.43/0.60 (1,1) [198,8]. true => ~_t61 | ~_t57 | ~_t12 | ~p7 | ~p3 [ LRES, 191, 49, p2 ] % 0.43/0.60 (1,1) [200,8]. true => ~_t62 | ~_t56 | ~_t50 | ~_t11 | p7 | ~p4 [ LRES, 197, 42, p3 ] % 0.43/0.60 (1,1) [201,8]. true => ~_t61 | ~_t57 | ~_t49 | ~_t12 | ~p7 | p4 [ LRES, 198, 40, ~p3 ] % 0.43/0.60 (1,1) [203,8]. true => ~_t62 | ~_t56 | ~_t50 | ~_t41 | ~_t11 | p7 | p5 [ LRES, 200, 32, ~p4 ] % 0.43/0.60 (1,1) [204,8]. true => ~_t61 | ~_t57 | ~_t49 | ~_t42 | ~_t12 | ~p7 | ~p5 [ LRES, 201, 34, p4 ] % 0.43/0.60 (1,1) [206,8]. true => ~_t62 | ~_t56 | ~_t50 | ~_t41 | ~_t33 | ~_t11 | p7 | ~p6 [ LRES, 203, 25, p5 ] % 0.43/0.60 (1,1) [207,8]. true => ~_t61 | ~_t57 | ~_t49 | ~_t42 | ~_t32 | ~_t12 | ~p7 | p6 [ LRES, 204, 23, ~p5 ] % 0.43/0.60 (1,1) [209,8]. true => ~_t62 | ~_t56 | ~_t50 | ~_t41 | ~_t33 | ~_t22 | ~_t11 | p7 [ LRES, 206, 13, ~p6 ] % 0.43/0.60 (1,1) [210,8]. true => ~_t61 | ~_t57 | ~_t49 | ~_t42 | ~_t32 | ~_t23 | ~_t12 | ~p7 [ LRES, 207, 15, p6 ] % 0.43/0.60 (1,1) [212,8]. true => ~_t62 | ~_t61 | ~_t57 | ~_t56 | ~_t50 | ~_t49 | ~_t42 | ~_t41 | ~_t33 | ~_t32 | ~_t23 | ~_t22 | ~_t12 | ~_t11 [ LRES, 210, 209, ~p7 ] % 0.43/0.60 (1,1) [213,8]. true => ~_t77 | ~_t62 | ~_t61 | ~_t57 | ~_t56 | ~_t50 | ~_t49 | ~_t42 | ~_t41 | ~_t33 | ~_t32 | ~_t23 | ~_t22 | ~_t12 [ LRES, 212, 175, ~_t11 ] [ Backward Subsumption, 214 ] % 0.43/0.60 (1,1) [214,8]. true => ~_t77 | ~_t62 | ~_t61 | ~_t57 | ~_t56 | ~_t50 | ~_t49 | ~_t42 | ~_t41 | ~_t33 | ~_t32 | ~_t23 | ~_t22 [ LRES, 213, 174, ~_t12 ] % 0.43/0.60 (1,1) [215,8]. true => ~_t78 | ~_t77 | ~_t62 | ~_t61 | ~_t57 | ~_t56 | ~_t50 | ~_t49 | ~_t42 | ~_t41 | ~_t33 | ~_t32 | ~_t23 [ LRES, 214, 177, ~_t22 ] [ Backward Subsumption, 216 ] % 0.43/0.60 (1,1) [216,8]. true => ~_t78 | ~_t77 | ~_t62 | ~_t61 | ~_t57 | ~_t56 | ~_t50 | ~_t49 | ~_t42 | ~_t41 | ~_t33 | ~_t32 [ LRES, 215, 176, ~_t23 ] % 0.43/0.60 (1,1) [217,8]. true => ~_t79 | ~_t78 | ~_t77 | ~_t62 | ~_t61 | ~_t57 | ~_t56 | ~_t50 | ~_t49 | ~_t42 | ~_t41 | ~_t33 [ LRES, 216, 179, ~_t32 ] [ Backward Subsumption, 218 ] % 0.43/0.60 (1,1) [218,8]. true => ~_t79 | ~_t78 | ~_t77 | ~_t62 | ~_t61 | ~_t57 | ~_t56 | ~_t50 | ~_t49 | ~_t42 | ~_t41 [ LRES, 217, 178, ~_t33 ] % 0.43/0.60 (1,1) [219,8]. true => ~_t80 | ~_t79 | ~_t78 | ~_t77 | ~_t62 | ~_t61 | ~_t57 | ~_t56 | ~_t50 | ~_t49 | ~_t42 [ LRES, 218, 181, ~_t41 ] [ Backward Subsumption, 220 ] % 0.43/0.60 (1,1) [220,8]. true => ~_t80 | ~_t79 | ~_t78 | ~_t77 | ~_t62 | ~_t61 | ~_t57 | ~_t56 | ~_t50 | ~_t49 [ LRES, 219, 180, ~_t42 ] % 0.43/0.60 (1,1) [221,8]. true => ~_t81 | ~_t80 | ~_t79 | ~_t78 | ~_t77 | ~_t62 | ~_t61 | ~_t57 | ~_t56 | ~_t50 [ LRES, 220, 183, ~_t49 ] [ Backward Subsumption, 222 ] % 0.43/0.60 (1,1) [222,8]. true => ~_t81 | ~_t80 | ~_t79 | ~_t78 | ~_t77 | ~_t62 | ~_t61 | ~_t57 | ~_t56 [ LRES, 221, 182, ~_t50 ] % 0.43/0.60 (1,1) [223,8]. true => ~_t82 | ~_t81 | ~_t80 | ~_t79 | ~_t78 | ~_t77 | ~_t62 | ~_t61 | ~_t57 [ LRES, 222, 185, ~_t56 ] [ Backward Subsumption, 224 ] % 0.43/0.60 (1,1) [224,8]. true => ~_t82 | ~_t81 | ~_t80 | ~_t79 | ~_t78 | ~_t77 | ~_t62 | ~_t61 [ LRES, 223, 184, ~_t57 ] % 0.43/0.60 (1,1) [225,8]. true => ~_t83 | ~_t82 | ~_t81 | ~_t80 | ~_t79 | ~_t78 | ~_t77 | ~_t62 [ LRES, 224, 187, ~_t61 ] [ Backward Subsumption, 226 ] % 0.43/0.60 (1,1) [226,8]. true => ~_t83 | ~_t82 | ~_t81 | ~_t80 | ~_t79 | ~_t78 | ~_t77 [ LRES, 225, 186, ~_t62 ] % 0.43/0.60 % SZS output end Refutation % 0.43/0.60 % KSP exiting %------------------------------------------------------------------------------