%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP011_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:52 PM UTC 2026 % Result : Theorem 0.46s 0.65s % Output : Refutation 0.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP011_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.16/0.33 % Computer : n023.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Mon May 4 16:07:38 EDT 2026 % 0.16/0.33 % CPUTime : % 0.34/0.61 ----KSP format--- % 0.34/0.61 usable(formulas). % 0.34/0.61 true. % 0.34/0.61 end_of_list. % 0.34/0.61 sos(formulas). % 0.34/0.61 ~ ([] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( 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.34/0.61 end_of_list. % 0.34/0.61 ----------------- % 0.34/0.62 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.HcaJG2tSBJ/theBenchmark.ksp % 0.46/0.65 % 0.46/0.65 % SZS status Theorem % 0.46/0.65 % 0.46/0.65 ***************** % 0.46/0.65 FOUND PROOF 1 % 0.46/0.65 ***************** % 0.46/0.65 % SZS output start Refutation % 0.46/0.65 % 0.46/0.65 (1,1) [1,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.46/0.65 (1,1) [12,0]. _t0 => box 1 _t2 [ SNF ] [ Backward Subsumption, 487 ] % 0.46/0.65 (1,1) [25,0]. _t0 => box 1 _t13 [ SNF ] [ Backward Subsumption, 486 ] % 0.46/0.65 (1,1) [68,0]. _t0 => box 1 _t53 [ SNF ] [ Backward Subsumption, 483 ] % 0.46/0.65 (141,1) [431,0]. _t0 => ~box 1~ _t66 [ SNF ] [ Backward Subsumption, 437 ] % 0.46/0.65 (141,1) [437,0]. true => ~box 1~ _t66 [ LHS Unit Resolution, 1, 431, _t0 ] [ SNF++, 1232, _t66 ] % 0.46/0.65 (1,1) [483,0]. true => box 1 _t53 [ LHS Unit Resolution, 1, 68, _t0 ] [ SNF++, 1140, _t53 ] % 0.46/0.65 (1,1) [486,0]. true => box 1 _t13 [ LHS Unit Resolution, 1, 25, _t0 ] [ SNF++, 1134, _t13 ] % 0.46/0.65 (1,1) [487,0]. true => box 1 _t2 [ LHS Unit Resolution, 1, 12, _t0 ] [ SNF++, 1132, _t2 ] % 0.46/0.65 (1,1) [1132,0]. true => box 1 _t138 [ SNF++, 487 ] % 0.46/0.65 (1,1) [1134,0]. true => box 1 _t139 [ SNF++, 486 ] % 0.46/0.65 (1,1) [1140,0]. true => box 1 _t142 [ SNF++, 483 ] % 0.46/0.65 (141,1) [1232,0]. true => ~box 1~ _t143 [ SNF++, 437 ] % 0.46/0.65 (141,1) [2323,0]. true => false [ GEN1, 1140, 1132, 1134, 1232, 2318, _t142, _t138, _t139, _t143 ] % 0.46/0.65 (1,1) [11,1]. _t2 => box 1 _t3 [ SNF ] [ SNF++, 1028, _t3 ] % 0.46/0.65 (1,1) [24,1]. _t13 => box 1 _t14 [ SNF ] [ SNF++, 1030, _t14 ] % 0.46/0.65 (1,1) [67,1]. _t53 => box 1 _t54 [ SNF ] [ SNF++, 1036, _t54 ] % 0.46/0.65 (140,1) [430,1]. _t66 => ~box 1~ _t67 [ SNF ] [ SNF++, 1130, _t67 ] % 0.46/0.65 (1,1) [1028,1]. _t2 => box 1 _t132 [ SNF++, 11 ] % 0.46/0.65 (1,1) [1030,1]. _t13 => box 1 _t133 [ SNF++, 24 ] % 0.46/0.65 (1,1) [1036,1]. _t53 => box 1 _t136 [ SNF++, 67 ] % 0.46/0.65 (140,1) [1130,1]. _t66 => ~box 1~ _t137 [ SNF++, 430 ] % 0.46/0.65 (1,1) [1133,1]. true => ~_t138 | _t2 [ SNF++, 487 ] % 0.46/0.65 (1,1) [1135,1]. true => ~_t139 | _t13 [ SNF++, 486 ] % 0.46/0.65 (1,1) [1141,1]. true => ~_t142 | _t53 [ SNF++, 483 ] % 0.46/0.65 (141,1) [1233,1]. true => ~_t143 | _t66 [ SNF++, 437 ] % 0.46/0.65 (140,1) [2283,1]. true => ~_t66 | ~_t53 | ~_t13 | ~_t2 [ GEN1, 1036, 1028, 1030, 1130, 2280, _t136, _t132, _t133, _t137 ] % 0.46/0.65 (140,1) [2288,1]. true => ~_t138 | ~_t66 | ~_t53 | ~_t13 [ LRES, 2283, 1133, ~_t2 ] % 0.46/0.65 (140,1) [2304,1]. true => ~_t139 | ~_t138 | ~_t66 | ~_t53 [ LRES, 2288, 1135, ~_t13 ] % 0.46/0.65 (140,1) [2311,1]. true => ~_t142 | ~_t139 | ~_t138 | ~_t66 [ LRES, 2304, 1141, ~_t53 ] % 0.46/0.65 (141,1) [2318,1]. true => ~_t143 | ~_t142 | ~_t139 | ~_t138 [ LRES, 2311, 1233, ~_t66 ] % 0.46/0.65 (1,1) [10,2]. _t3 => box 1 _t4 [ SNF ] [ SNF++, 928, _t4 ] % 0.46/0.65 (1,1) [23,2]. _t14 => box 1 _t15 [ SNF ] [ SNF++, 930, _t15 ] % 0.46/0.65 (1,1) [66,2]. _t54 => box 1 _t55 [ SNF ] [ SNF++, 936, _t55 ] % 0.46/0.65 (139,1) [429,2]. _t67 => ~box 1~ _t68 [ SNF ] [ SNF++, 1026, _t68 ] % 0.46/0.65 (1,1) [928,2]. _t3 => box 1 _t126 [ SNF++, 10 ] % 0.46/0.65 (1,1) [930,2]. _t14 => box 1 _t127 [ SNF++, 23 ] % 0.46/0.65 (1,1) [936,2]. _t54 => box 1 _t130 [ SNF++, 66 ] % 0.46/0.65 (139,1) [1026,2]. _t67 => ~box 1~ _t131 [ SNF++, 429 ] % 0.46/0.65 (1,1) [1029,2]. true => ~_t132 | _t3 [ SNF++, 11 ] % 0.46/0.65 (1,1) [1031,2]. true => ~_t133 | _t14 [ SNF++, 24 ] % 0.46/0.65 (1,1) [1037,2]. true => ~_t136 | _t54 [ SNF++, 67 ] % 0.46/0.65 (140,1) [1131,2]. true => ~_t137 | _t67 [ SNF++, 430 ] % 0.46/0.65 (139,1) [2264,2]. true => ~_t67 | ~_t54 | ~_t14 | ~_t3 [ GEN1, 936, 928, 930, 1026, 2258, _t130, _t126, _t127, _t131 ] % 0.46/0.65 (139,1) [2265,2]. true => ~_t132 | ~_t67 | ~_t54 | ~_t14 [ LRES, 2264, 1029, ~_t3 ] % 0.46/0.65 (139,1) [2271,2]. true => ~_t133 | ~_t132 | ~_t67 | ~_t54 [ LRES, 2265, 1031, ~_t14 ] % 0.46/0.65 (139,1) [2277,2]. true => ~_t136 | ~_t133 | ~_t132 | ~_t67 [ LRES, 2271, 1037, ~_t54 ] % 0.46/0.65 (140,1) [2280,2]. true => ~_t137 | ~_t136 | ~_t133 | ~_t132 [ LRES, 2277, 1131, ~_t67 ] % 0.46/0.65 (1,1) [9,3]. _t4 => box 1 _t5 [ SNF ] [ SNF++, 838, _t5 ] % 0.46/0.65 (1,1) [22,3]. _t15 => box 1 _t16 [ SNF ] [ SNF++, 840, _t16 ] % 0.46/0.65 (1,1) [65,3]. _t55 => box 1 _t56 [ SNF ] [ SNF++, 846, _t56 ] % 0.46/0.65 (138,1) [428,3]. _t68 => ~box 1~ _t69 [ SNF ] [ SNF++, 926, _t69 ] % 0.46/0.65 (1,1) [838,3]. _t4 => box 1 _t120 [ SNF++, 9 ] % 0.46/0.65 (1,1) [840,3]. _t15 => box 1 _t121 [ SNF++, 22 ] % 0.46/0.65 (1,1) [846,3]. _t55 => box 1 _t124 [ SNF++, 65 ] % 0.46/0.65 (138,1) [926,3]. _t68 => ~box 1~ _t125 [ SNF++, 428 ] % 0.46/0.65 (1,1) [929,3]. true => ~_t126 | _t4 [ SNF++, 10 ] % 0.46/0.65 (1,1) [931,3]. true => ~_t127 | _t15 [ SNF++, 23 ] % 0.46/0.65 (1,1) [937,3]. true => ~_t130 | _t55 [ SNF++, 66 ] % 0.46/0.65 (139,1) [1027,3]. true => ~_t131 | _t68 [ SNF++, 429 ] % 0.46/0.65 (138,1) [2236,3]. true => ~_t68 | ~_t55 | ~_t15 | ~_t4 [ GEN1, 846, 838, 840, 926, 2232, _t124, _t120, _t121, _t125 ] % 0.46/0.65 (138,1) [2237,3]. true => ~_t126 | ~_t68 | ~_t55 | ~_t15 [ LRES, 2236, 929, ~_t4 ] % 0.46/0.65 (138,1) [2241,3]. true => ~_t127 | ~_t126 | ~_t68 | ~_t55 [ LRES, 2237, 931, ~_t15 ] % 0.46/0.65 (138,1) [2251,3]. true => ~_t130 | ~_t127 | ~_t126 | ~_t68 [ LRES, 2241, 937, ~_t55 ] % 0.46/0.65 (139,1) [2258,3]. true => ~_t131 | ~_t130 | ~_t127 | ~_t126 [ LRES, 2251, 1027, ~_t68 ] % 0.46/0.65 (1,1) [8,4]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 758, _t6 ] % 0.46/0.65 (1,1) [21,4]. _t16 => box 1 _t17 [ SNF ] [ SNF++, 760, _t17 ] % 0.46/0.65 (1,1) [64,4]. _t56 => box 1 _t57 [ SNF ] [ SNF++, 766, _t57 ] % 0.46/0.65 (137,1) [427,4]. _t69 => ~box 1~ _t70 [ SNF ] [ SNF++, 836, _t70 ] % 0.46/0.65 (1,1) [758,4]. _t5 => box 1 _t114 [ SNF++, 8 ] % 0.46/0.65 (1,1) [760,4]. _t16 => box 1 _t115 [ SNF++, 21 ] % 0.46/0.65 (1,1) [766,4]. _t56 => box 1 _t118 [ SNF++, 64 ] % 0.46/0.65 (137,1) [836,4]. _t69 => ~box 1~ _t119 [ SNF++, 427 ] % 0.46/0.65 (1,1) [839,4]. true => ~_t120 | _t5 [ SNF++, 9 ] % 0.46/0.65 (1,1) [841,4]. true => ~_t121 | _t16 [ SNF++, 22 ] % 0.46/0.65 (1,1) [847,4]. true => ~_t124 | _t56 [ SNF++, 65 ] % 0.46/0.65 (138,1) [927,4]. true => ~_t125 | _t69 [ SNF++, 428 ] % 0.46/0.65 (137,1) [2220,4]. true => ~_t69 | ~_t56 | ~_t16 | ~_t5 [ GEN1, 766, 758, 760, 836, 2209, _t118, _t114, _t115, _t119 ] % 0.46/0.65 (137,1) [2221,4]. true => ~_t120 | ~_t69 | ~_t56 | ~_t16 [ LRES, 2220, 839, ~_t5 ] % 0.46/0.65 (137,1) [2225,4]. true => ~_t121 | ~_t120 | ~_t69 | ~_t56 [ LRES, 2221, 841, ~_t16 ] % 0.46/0.65 (137,1) [2229,4]. true => ~_t124 | ~_t121 | ~_t120 | ~_t69 [ LRES, 2225, 847, ~_t56 ] % 0.46/0.65 (138,1) [2232,4]. true => ~_t125 | ~_t124 | ~_t121 | ~_t120 [ LRES, 2229, 927, ~_t69 ] % 0.46/0.65 (1,1) [7,5]. _t6 => box 1 _t7 [ SNF ] [ SNF++, 688, _t7 ] % 0.46/0.65 (1,1) [20,5]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 690, _t18 ] % 0.46/0.65 (1,1) [63,5]. _t57 => box 1 _t58 [ SNF ] [ SNF++, 696, _t58 ] % 0.46/0.65 (136,1) [426,5]. _t70 => ~box 1~ _t71 [ SNF ] [ SNF++, 756, _t71 ] % 0.46/0.65 (1,1) [688,5]. _t6 => box 1 _t108 [ SNF++, 7 ] % 0.46/0.65 (1,1) [690,5]. _t17 => box 1 _t109 [ SNF++, 20 ] % 0.46/0.65 (1,1) [696,5]. _t57 => box 1 _t112 [ SNF++, 63 ] % 0.46/0.65 (136,1) [756,5]. _t70 => ~box 1~ _t113 [ SNF++, 426 ] % 0.46/0.65 (1,1) [759,5]. true => ~_t114 | _t6 [ SNF++, 8 ] % 0.46/0.65 (1,1) [761,5]. true => ~_t115 | _t17 [ SNF++, 21 ] % 0.46/0.65 (1,1) [767,5]. true => ~_t118 | _t57 [ SNF++, 64 ] % 0.46/0.65 (137,1) [837,5]. true => ~_t119 | _t70 [ SNF++, 427 ] % 0.46/0.65 (136,1) [2185,5]. true => ~_t70 | ~_t57 | ~_t17 | ~_t6 [ GEN1, 696, 688, 690, 756, 2178, _t112, _t108, _t109, _t113 ] % 0.46/0.65 (136,1) [2186,5]. true => ~_t114 | ~_t70 | ~_t57 | ~_t17 [ LRES, 2185, 759, ~_t6 ] % 0.46/0.65 (136,1) [2195,5]. true => ~_t115 | ~_t114 | ~_t70 | ~_t57 [ LRES, 2186, 761, ~_t17 ] % 0.46/0.65 (136,1) [2203,5]. true => ~_t118 | ~_t115 | ~_t114 | ~_t70 [ LRES, 2195, 767, ~_t57 ] % 0.46/0.65 (137,1) [2209,5]. true => ~_t119 | ~_t118 | ~_t115 | ~_t114 [ LRES, 2203, 837, ~_t70 ] % 0.46/0.65 (1,1) [6,6]. _t7 => box 1 _t8 [ SNF ] [ SNF++, 628, _t8 ] % 0.46/0.65 (1,1) [19,6]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 630, _t19 ] % 0.46/0.65 (1,1) [62,6]. _t58 => box 1 _t59 [ SNF ] [ SNF++, 636, _t59 ] % 0.46/0.65 (135,1) [425,6]. _t71 => ~box 1~ _t72 [ SNF ] [ SNF++, 686, _t72 ] % 0.46/0.65 (1,1) [628,6]. _t7 => box 1 _t102 [ SNF++, 6 ] % 0.46/0.65 (1,1) [630,6]. _t18 => box 1 _t103 [ SNF++, 19 ] % 0.46/0.65 (1,1) [636,6]. _t58 => box 1 _t106 [ SNF++, 62 ] % 0.46/0.65 (135,1) [686,6]. _t71 => ~box 1~ _t107 [ SNF++, 425 ] % 0.46/0.65 (1,1) [689,6]. true => ~_t108 | _t7 [ SNF++, 7 ] % 0.46/0.65 (1,1) [691,6]. true => ~_t109 | _t18 [ SNF++, 20 ] % 0.46/0.65 (1,1) [697,6]. true => ~_t112 | _t58 [ SNF++, 63 ] % 0.46/0.65 (136,1) [757,6]. true => ~_t113 | _t71 [ SNF++, 426 ] % 0.46/0.65 (135,1) [2149,6]. true => ~_t71 | ~_t58 | ~_t18 | ~_t7 [ GEN1, 636, 628, 630, 686, 2139, _t106, _t102, _t103, _t107 ] % 0.46/0.65 (135,1) [2150,6]. true => ~_t108 | ~_t71 | ~_t58 | ~_t18 [ LRES, 2149, 689, ~_t7 ] % 0.46/0.65 (135,1) [2166,6]. true => ~_t109 | ~_t108 | ~_t71 | ~_t58 [ LRES, 2150, 691, ~_t18 ] % 0.46/0.65 (135,1) [2172,6]. true => ~_t112 | ~_t109 | ~_t108 | ~_t71 [ LRES, 2166, 697, ~_t58 ] % 0.46/0.65 (136,1) [2178,6]. true => ~_t113 | ~_t112 | ~_t109 | ~_t108 [ LRES, 2172, 757, ~_t71 ] % 0.46/0.65 (1,1) [5,7]. _t8 => box 1 _t9 [ SNF ] [ SNF++, 578, _t9 ] % 0.46/0.65 (1,1) [18,7]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 580, _t20 ] % 0.46/0.65 (1,1) [61,7]. _t59 => box 1 _t60 [ SNF ] [ SNF++, 586, _t60 ] % 0.46/0.65 (134,1) [424,7]. _t72 => ~box 1~ _t73 [ SNF ] [ SNF++, 626, _t73 ] % 0.46/0.65 (1,1) [578,7]. _t8 => box 1 _t96 [ SNF++, 5 ] % 0.46/0.65 (1,1) [580,7]. _t19 => box 1 _t97 [ SNF++, 18 ] % 0.46/0.65 (1,1) [586,7]. _t59 => box 1 _t100 [ SNF++, 61 ] % 0.46/0.65 (134,1) [626,7]. _t72 => ~box 1~ _t101 [ SNF++, 424 ] % 0.46/0.65 (1,1) [629,7]. true => ~_t102 | _t8 [ SNF++, 6 ] % 0.46/0.65 (1,1) [631,7]. true => ~_t103 | _t19 [ SNF++, 19 ] % 0.46/0.65 (1,1) [637,7]. true => ~_t106 | _t59 [ SNF++, 62 ] % 0.46/0.65 (135,1) [687,7]. true => ~_t107 | _t72 [ SNF++, 425 ] % 0.46/0.65 (134,1) [2100,7]. true => ~_t72 | ~_t59 | ~_t19 | ~_t8 [ GEN1, 586, 578, 580, 626, 2089, _t100, _t96, _t97, _t101 ] % 0.46/0.65 (134,1) [2101,7]. true => ~_t102 | ~_t72 | ~_t59 | ~_t19 [ LRES, 2100, 629, ~_t8 ] % 0.46/0.65 (134,1) [2115,7]. true => ~_t103 | ~_t102 | ~_t72 | ~_t59 [ LRES, 2101, 631, ~_t19 ] % 0.46/0.65 (134,1) [2127,7]. true => ~_t106 | ~_t103 | ~_t102 | ~_t72 [ LRES, 2115, 637, ~_t59 ] % 0.46/0.65 (135,1) [2139,7]. true => ~_t107 | ~_t106 | ~_t103 | ~_t102 [ LRES, 2127, 687, ~_t72 ] % 0.46/0.65 (1,1) [4,8]. _t9 => box 1 _t10 [ SNF ] [ SNF++, 538, _t10 ] % 0.46/0.65 (1,1) [17,8]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 540, _t21 ] % 0.46/0.65 (1,1) [60,8]. _t60 => box 1 _t61 [ SNF ] [ SNF++, 546, _t61 ] % 0.46/0.65 (133,1) [423,8]. _t73 => ~box 1~ _t74 [ SNF ] [ SNF++, 576, _t74 ] % 0.46/0.65 (1,1) [538,8]. _t9 => box 1 _t90 [ SNF++, 4 ] % 0.46/0.65 (1,1) [540,8]. _t20 => box 1 _t91 [ SNF++, 17 ] % 0.46/0.65 (1,1) [546,8]. _t60 => box 1 _t94 [ SNF++, 60 ] % 0.46/0.65 (133,1) [576,8]. _t73 => ~box 1~ _t95 [ SNF++, 423 ] % 0.46/0.65 (1,1) [579,8]. true => ~_t96 | _t9 [ SNF++, 5 ] % 0.46/0.65 (1,1) [581,8]. true => ~_t97 | _t20 [ SNF++, 18 ] % 0.46/0.65 (1,1) [587,8]. true => ~_t100 | _t60 [ SNF++, 61 ] % 0.46/0.65 (134,1) [627,8]. true => ~_t101 | _t73 [ SNF++, 424 ] % 0.46/0.65 (133,1) [2026,8]. true => ~_t73 | ~_t60 | ~_t20 | ~_t9 [ GEN1, 546, 538, 540, 576, 2004, _t94, _t90, _t91, _t95 ] % 0.46/0.65 (133,1) [2027,8]. true => ~_t96 | ~_t73 | ~_t60 | ~_t20 [ LRES, 2026, 579, ~_t9 ] % 0.46/0.65 (133,1) [2048,8]. true => ~_t97 | ~_t96 | ~_t73 | ~_t60 [ LRES, 2027, 581, ~_t20 ] % 0.46/0.65 (133,1) [2079,8]. true => ~_t100 | ~_t97 | ~_t96 | ~_t73 [ LRES, 2048, 587, ~_t60 ] % 0.46/0.65 (134,1) [2089,8]. true => ~_t101 | ~_t100 | ~_t97 | ~_t96 [ LRES, 2079, 627, ~_t73 ] % 0.46/0.65 (1,1) [3,9]. _t10 => box 1 _t11 [ SNF ] [ SNF++, 508, _t11 ] % 0.46/0.65 (1,1) [16,9]. _t21 => box 1 _t22 [ SNF ] [ SNF++, 510, _t22 ] % 0.46/0.65 (1,1) [59,9]. _t61 => box 1 _t62 [ SNF ] [ SNF++, 516, _t62 ] % 0.46/0.65 (132,1) [422,9]. _t74 => ~box 1~ _t75 [ SNF ] [ SNF++, 536, _t75 ] % 0.46/0.65 (1,1) [508,9]. _t10 => box 1 _t84 [ SNF++, 3 ] % 0.46/0.65 (1,1) [510,9]. _t21 => box 1 _t85 [ SNF++, 16 ] % 0.46/0.65 (1,1) [516,9]. _t61 => box 1 _t88 [ SNF++, 59 ] % 0.46/0.65 (132,1) [536,9]. _t74 => ~box 1~ _t89 [ SNF++, 422 ] % 0.46/0.65 (1,1) [539,9]. true => ~_t90 | _t10 [ SNF++, 4 ] % 0.46/0.65 (1,1) [541,9]. true => ~_t91 | _t21 [ SNF++, 17 ] % 0.46/0.65 (1,1) [547,9]. true => ~_t94 | _t61 [ SNF++, 60 ] % 0.46/0.65 (133,1) [577,9]. true => ~_t95 | _t74 [ SNF++, 423 ] % 0.46/0.65 (132,1) [1946,9]. true => ~_t74 | ~_t61 | ~_t21 | ~_t10 [ GEN1, 516, 508, 510, 536, 1920, _t88, _t84, _t85, _t89 ] % 0.46/0.65 (132,1) [1947,9]. true => ~_t90 | ~_t74 | ~_t61 | ~_t21 [ LRES, 1946, 539, ~_t10 ] % 0.46/0.65 (132,1) [1973,9]. true => ~_t91 | ~_t90 | ~_t74 | ~_t61 [ LRES, 1947, 541, ~_t21 ] % 0.46/0.65 (132,1) [1997,9]. true => ~_t94 | ~_t91 | ~_t90 | ~_t74 [ LRES, 1973, 547, ~_t61 ] % 0.46/0.65 (133,1) [2004,9]. true => ~_t95 | ~_t94 | ~_t91 | ~_t90 [ LRES, 1997, 577, ~_t74 ] % 0.46/0.65 (3,1) [2,10]. _t11 => ~box 1~ true [ SNF ] % 0.46/0.65 (1,1) [14,10]. _t23 => box 1 _t24 [ SNF ] [ SNF++, 494, _t24 ] % 0.46/0.65 (1,1) [15,10]. true => _t23 | ~_t22 | p0 [ SNF ] % 0.46/0.65 (1,1) [56,10]. _t63 => box 1 _t64 [ SNF ] [ SNF++, 500, _t64 ] % 0.46/0.65 (13,1) [57,10]. _t24 => ~box 1~ ~p0 [ SNF ] [ SNF++, 490, ~p0 ] % 0.46/0.65 (1,1) [58,10]. true => _t63 | ~_t62 | _t24 [ SNF ] % 0.46/0.65 (17,1) [103,10]. _t38 => ~box 1~ p0 [ SNF ] [ SNF++, 492, p0 ] % 0.46/0.65 (132,1) [420,10]. true => ~_t75 | ~p0 [ SNF ] % 0.46/0.65 (1,1) [421,10]. _t75 => box 1 p0 [ SNF ] [ SNF++, 504, p0 ] % 0.46/0.65 (13,1) [490,10]. _t24 => ~box 1~ _t78 [ SNF++, 57 ] % 0.46/0.65 (1,1) [494,10]. _t23 => box 1 _t80 [ SNF++, 14 ] % 0.46/0.65 (1,1) [500,10]. _t63 => box 1 _t83 [ SNF++, 56 ] % 0.46/0.65 (1,1) [504,10]. _t75 => box 1 _t79 [ SNF++, 421 ] % 0.46/0.65 (1,1) [509,10]. true => ~_t84 | _t11 [ SNF++, 3 ] % 0.46/0.65 (1,1) [511,10]. true => ~_t85 | _t22 [ SNF++, 16 ] % 0.46/0.65 (1,1) [517,10]. true => ~_t88 | _t62 [ SNF++, 59 ] % 0.46/0.65 (132,1) [537,10]. true => ~_t89 | _t75 [ SNF++, 422 ] % 0.46/0.65 (132,1) [1264,10]. true => ~_t75 | _t23 | ~_t22 [ LRES, 420, 15, ~p0 ] % 0.46/0.65 (13,1) [1326,10]. true => ~_t75 | ~_t24 [ GEN1, 504, 490, 1262, _t79, _t78 ] % 0.46/0.65 (13,1) [1377,10]. true => ~_t75 | _t63 | ~_t62 [ LRES, 1326, 58, ~_t24 ] % 0.46/0.65 (1,1) [1411,10]. true => ~_t63 | ~_t23 | ~_t11 [ GEN3, 500, 494, 1387, 2, _t83, _t80, true ] % 0.46/0.65 (132,1) [1536,10]. true => ~_t85 | ~_t75 | _t23 [ LRES, 1264, 511, ~_t22 ] % 0.46/0.65 (1,1) [1541,10]. true => ~_t84 | ~_t63 | ~_t23 [ LRES, 1411, 509, ~_t11 ] % 0.46/0.65 (13,1) [1600,10]. true => ~_t88 | ~_t75 | _t63 [ LRES, 1377, 517, ~_t62 ] % 0.46/0.65 (132,1) [1650,10]. true => ~_t85 | ~_t84 | ~_t75 | ~_t63 [ LRES, 1536, 1541, _t23 ] % 0.46/0.65 (132,1) [1862,10]. true => ~_t88 | ~_t85 | ~_t84 | ~_t75 [ LRES, 1650, 1600, ~_t63 ] % 0.46/0.65 (132,1) [1920,10]. true => ~_t89 | ~_t88 | ~_t85 | ~_t84 [ LRES, 1862, 537, ~_t75 ] % 0.46/0.65 (11,1) [13,11]. _t24 => ~box 1~ ~p0 [ SNF ] [ SNF++, 1234, ~p0 ] % 0.46/0.65 (5,1) [42,11]. _t38 => ~box 1~ p0 [ SNF ] [ SNF++, 1236, p0 ] % 0.46/0.65 (1,1) [55,11]. _t64 => box 1 p0 [ SNF ] [ SNF++, 1242, p0 ] % 0.46/0.65 (13,1) [491,11]. true => ~_t78 | ~p0 [ SNF++, 57 ] % 0.46/0.65 (17,1) [493,11]. true => ~_t79 | p0 [ SNF++, 103 ] % 0.46/0.65 (1,1) [495,11]. true => ~_t80 | _t24 [ SNF++, 14 ] % 0.46/0.65 (1,1) [501,11]. true => ~_t83 | _t64 [ SNF++, 56 ] % 0.46/0.65 (11,1) [1234,11]. _t24 => ~box 1~ _t78 [ SNF++, 13 ] % 0.46/0.65 (1,1) [1242,11]. _t64 => box 1 _t79 [ SNF++, 55 ] % 0.46/0.65 (17,1) [1262,11]. true => ~_t79 | ~_t78 [ LRES, 491, 493, ~p0 ] % 0.46/0.65 (11,1) [1330,11]. true => ~_t64 | ~_t24 [ GEN1, 1242, 1234, 1263, _t79, _t78 ] % 0.46/0.65 (11,1) [1359,11]. true => ~_t80 | ~_t64 [ LRES, 1330, 495, ~_t24 ] % 0.46/0.65 (11,1) [1387,11]. true => ~_t83 | ~_t80 [ LRES, 1359, 501, ~_t64 ] % 0.46/0.65 (11,1) [1235,12]. true => ~_t78 | ~p0 [ SNF++, 13 ] % 0.46/0.65 (5,1) [1237,12]. true => ~_t79 | p0 [ SNF++, 42 ] % 0.46/0.65 (11,1) [1263,12]. true => ~_t79 | ~_t78 [ LRES, 1235, 1237, ~p0 ] % 0.46/0.65 % SZS output end Refutation % 0.46/0.65 % KSP exiting %------------------------------------------------------------------------------