%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYO924_1.002 : TPTP v9.0.0. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n006.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 10:47:48 PM UTC 2025 % Result : Theorem 47.50s 47.68s % Output : Refutation 47.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SYO924_1.002 : TPTP v9.0.0. Released v9.0.0. % 0.08/0.13 % Command : run_ksp %s % 0.14/0.35 % Computer : n006.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Wed Apr 9 10:26:22 EDT 2025 % 0.14/0.35 % CPUTime : % 0.22/0.61 ----KSP format--- % 0.22/0.61 set(box,REF,FIVE). % 0.22/0.61 usable(formulas). % 0.22/0.61 true. % 0.22/0.61 end_of_list. % 0.22/0.61 sos(formulas). % 0.22/0.61 ~ (~ ( ( x0 & [] ( ~ ( x0 ) ) ) | ( [] ( <> ( p1 | ( ~ ( y1 ) & [] ( y1 ) ) | ( ~ ( z1 ) & <> ( <> ( <> ( [] ( z1 ) ) ) ) ) ) | [] ( [] ( ~ ( p1 ) | ( ~ ( y1 ) & [] ( y1 ) ) | ( ~ ( z1 ) & <> ( <> ( <> ( [] ( z1 ) ) ) ) ) ) ) ) & <> ( [] ( <> ( p1 | ( ~ ( y1 ) & [] ( y1 ) ) | ( ~ ( z1 ) & <> ( <> ( <> ( [] ( z1 ) ) ) ) ) ) | [] ( [] ( ~ ( p1 ) | ( ~ ( y1 ) & [] ( y1 ) ) | ( ~ ( z1 ) & <> ( <> ( <> ( [] ( z1 ) ) ) ) ) ) ) ) & <> ( [] ( <> ( ~ ( p0 ) | ( ~ ( y0 ) & [] ( y0 ) ) | ( ~ ( z0 ) & <> ( <> ( <> ( [] ( z0 ) ) ) ) ) ) ) ) & <> ( <> ( ~ ( p1 ) | ( ~ ( y1 ) & [] ( y1 ) ) | ( ~ ( z1 ) & <> ( <> ( <> ( [] ( z1 ) ) ) ) ) ) & <> ( [] ( p1 | ( ~ ( y1 ) & [] ( y1 ) ) | ( ~ ( z1 ) & <> ( <> ( <> ( [] ( z1 ) ) ) ) ) ) ) ) ) & <> ( <> ( ~ ( p1 ) | ( ~ ( y1 ) & [] ( y1 ) ) | ( ~ ( z1 ) & <> ( <> ( <> ( [] ( z1 ) ) ) ) ) ) & <> ( [] ( p1 | ( ~ ( y1 ) & [] ( y1 ) ) | ( ~ ( z1 ) & <> ( <> ( <> ( [] ( z1 ) ) ) ) ) ) ) ) & [] ( <> ( ~ ( p1 ) | ( ~ ( y1 ) & [] ( y1 ) ) | ( ~ ( z1 ) & <> ( <> ( <> ( [] ( z1 ) ) ) ) ) ) | [] ( [] ( p1 | ( ~ ( y1 ) & [] ( y1 ) ) | ( ~ ( z1 ) & <> ( <> ( <> ( [] ( z1 ) ) ) ) ) ) ) ) & [] ( [] ( <> ( ~ ( p1 ) | ( ~ ( y1 ) & [] ( y1 ) ) | ( ~ ( z1 ) & <> ( <> ( <> ( [] ( z1 ) ) ) ) ) ) | [] ( [] ( p1 | ( ~ ( y1 ) & [] ( y1 ) ) | ( ~ ( z1 ) & <> ( <> ( <> ( [] ( z1 ) ) ) ) ) ) ) ) & [] ( ( <> ( [] ( ~ ( p0 ) | ( ~ ( y0 ) & [] ( y0 ) ) | ( ~ ( z0 ) & <> ( <> ( <> ( [] ( z0 ) ) ) ) ) ) ) | <> ( ( p0 | ( ~ ( y0 ) & [] ( y0 ) ) | ( ~ ( z0 ) & <> ( <> ( <> ( [] ( z0 ) ) ) ) ) ) & <> ( ~ ( p3 ) | ( ~ ( y3 ) & [] ( y3 ) ) | ( ~ ( z3 ) & <> ( <> ( <> ( [] ( z3 ) ) ) ) ) ) ) ) & [] ( <> ( [] ( <> ( ( p0 | ( ~ ( y0 ) & [] ( y0 ) ) | ( ~ ( z0 ) & <> ( <> ( <> ( [] ( z0 ) ) ) ) ) ) & <> ( ~ ( p3 ) | ( ~ ( y3 ) & [] ( y3 ) ) | ( ~ ( z3 ) & <> ( <> ( <> ( [] ( z3 ) ) ) ) ) ) ) ) ) | <> ( [] ( ~ ( p0 ) | ( ~ ( y0 ) & [] ( y0 ) ) | ( ~ ( z0 ) & <> ( <> ( <> ( [] ( z0 ) ) ) ) ) ) ) ) & ( <> ( [] ( ~ ( p0 ) | ( ~ ( y0 ) & [] ( y0 ) ) | ( ~ ( z0 ) & <> ( <> ( <> ( [] ( z0 ) ) ) ) ) ) ) | [] ( [] ( <> ( ( p0 | ( ~ ( y0 ) & [] ( y0 ) ) | ( ~ ( z0 ) & <> ( <> ( <> ( [] ( z0 ) ) ) ) ) ) & <> ( ~ ( p3 ) | ( ~ ( y3 ) & [] ( y3 ) ) | ( ~ ( z3 ) & <> ( <> ( <> ( [] ( z3 ) ) ) ) ) ) ) ) ) ) & [] ( [] ( <> ( [] ( ~ ( p0 ) | ( ~ ( y0 ) & [] ( y0 ) ) | ( ~ ( z0 ) & <> ( <> ( <> ( [] ( z0 ) ) ) ) ) ) ) ) | ~ ( p0 ) | ( ~ ( y0 ) & [] ( y0 ) ) | ( ~ ( z0 ) & <> ( <> ( <> ( [] ( z0 ) ) ) ) ) | [] ( ( p0 | ( ~ ( y0 ) & [] ( y0 ) ) | ( ~ ( z0 ) & <> ( <> ( <> ( [] ( z0 ) ) ) ) ) ) & <> ( ~ ( p3 ) | ( ~ ( y3 ) & [] ( y3 ) ) | ( ~ ( z3 ) & <> ( <> ( <> ( [] ( z3 ) ) ) ) ) ) ) ) & [] ( <> ( ( p0 | ( ~ ( y0 ) & [] ( y0 ) ) | ( ~ ( z0 ) & <> ( <> ( <> ( [] ( z0 ) ) ) ) ) ) & <> ( ~ ( p3 ) | ( ~ ( y3 ) & [] ( y3 ) ) | ( ~ ( z3 ) & <> ( <> ( <> ( [] ( z3 ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( ~ ( p1 ) | ( ~ ( y1 ) & [] ( y1 ) ) | ( ~ ( z1 ) & <> ( <> ( <> ( [] ( z1 ) ) ) ) ) ) ) | [] ( [] ( <> ( p1 | ( ~ ( y1 ) & [] ( y1 ) ) | ( ~ ( z1 ) & <> ( <> ( <> ( [] ( z1 ) ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( ~ ( p1 ) | ( ~ ( y1 ) & [] ( y1 ) ) | ( ~ ( z1 ) & <> ( <> ( <> ( [] ( z1 ) ) ) ) ) ) ) | [] ( [] ( <> ( p1 | ( ~ ( y1 ) & [] ( y1 ) ) | ( ~ ( z1 ) & <> ( <> ( <> ( [] ( z1 ) ) ) ) ) ) ) ) ) & [] ( ~ ( p4 ) | ( ~ ( y4 ) & [] ( y4 ) ) | ( ~ ( z4 ) & <> ( <> ( <> ( [] ( z4 ) ) ) ) ) ) ) ) ). % 0.22/0.61 end_of_list. % 0.22/0.61 ----------------- % 0.22/0.61 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.OKc0hoF7h1/theBenchmark.ksp % 47.50/47.68 % 47.50/47.68 % SZS status Theorem % 47.50/47.68 % 47.50/47.68 ***************** % 47.50/47.68 FOUND PROOF 1 % 47.50/47.68 ***************** % 47.50/47.68 % SZS output start Refutation % 47.50/47.68 % 47.50/47.68 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 47.50/47.68 (1,1) [4,0]. true => ~_t1 | x0 [ SNF ] [ Modal Level Pure Literal Elimination, ~_t1 ] % 47.50/47.68 (1,1) [6,0]. true => ~_t2 | ~x0 [ Axiom T ] [ Modal Level Pure Literal Elimination, ~x0 ] % 47.50/47.68 (1,1) [159,0]. true => _t2 | ~_t1 [ SNF ] [ Modal Level Pure Literal Elimination, ~_t1 ] % 47.50/47.68 (1,1) [10516,0]. true => _t86 | ~_t4 [ Axiom T ] [ Backward Subsumption, 19422 ] % 47.50/47.68 (1,1) [10517,0]. _t86 => box 1 _t86 [ Axiom 5 ] [ SNF++, 12070, _t86 ] % 47.50/47.68 (1,1) [10846,0]. true => _t4 | ~_t3 [ SNF ] [ Backward Subsumption, 19420 ] % 47.50/47.68 (356,1) [11871,0]. _t60 => ~box 1~ _t61 [ SNF ] [ SNF++, 12158, _t61 ] % 47.50/47.68 (1,1) [11872,0]. true => _t60 | ~_t3 [ SNF ] [ Backward Subsumption, 19415 ] % 47.50/47.68 (1,1) [11873,0]. true => _t3 | _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 11947 ] % 47.50/47.68 (1,1) [11947,0]. true => _t3 | _t1 [ Unit Resolution, 3, 11873, _t0 ] [ Modal Level Pure Literal Elimination, _t3 ] % 47.50/47.68 (1,1) [12070,0]. _t86 => box 1 _t151 [ SNF++, 10517 ] [ Backward Subsumption, 19446 ] % 47.50/47.68 (356,1) [12158,0]. _t60 => ~box 1~ _t184 [ SNF++, 11871 ] [ Backward Subsumption, 19428 ] % 47.50/47.68 (1,1) [16598,0]. true => ~_t2 | ~_t1 [ LRES, 6, 4, ~x0 ] [ Modal Level Pure Literal Elimination, ~_t1 ] % 47.50/47.68 (1,1) [16686,0]. true => _t3 | ~_t2 [ LRES, 16598, 11947, ~_t1 ] [ Modal Level Pure Literal Elimination, _t3 ] % 47.50/47.68 (1,1) [16730,0]. true => _t3 | _t2 [ LRES, 159, 11947, ~_t1 ] [ Modal Level Pure Literal Elimination, _t3 ] % 47.50/47.68 (1,1) [19351,0]. true => _t3 [ LRES, 16730, 16686, _t2 ] [ Modal Level Pure Literal Elimination, _t3 ] % 47.50/47.68 (1,1) [19415,0]. true => _t60 [ Unit Resolution, 19351, 11872, _t3 ] [ Modal Level Pure Literal Elimination, _t60 ] % 47.50/47.68 (1,1) [19420,0]. true => _t4 [ Unit Resolution, 19351, 10846, _t3 ] [ Modal Level Pure Literal Elimination, _t4 ] % 47.50/47.68 (1,1) [19422,0]. true => _t86 [ Unit Resolution, 19420, 10516, _t4 ] [ Modal Level Pure Literal Elimination, _t86 ] % 47.50/47.68 (356,1) [19428,0]. true => ~box 1~ _t184 [ LHS Unit Resolution, 19415, 12158, _t60 ] % 47.50/47.68 (1,1) [19446,0]. true => box 1 _t151 [ LHS Unit Resolution, 19422, 12070, _t86 ] % 47.50/47.68 (356,1) [514109,0]. true => false [ GEN1, 19446, 19428, 513780, _t151, _t184 ] % 47.50/47.68 (1,1) [10528,1]. _t4 => box 1 _t5 [ Axiom 5 ] [ SNF++, 12278, _t5 ] % 47.50/47.68 (1,1) [10534,1]. true => ~_t86 | _t4 [ Axiom 5 ] % 47.50/47.68 (348,1) [11869,1]. _t57 => ~box 1~ _t58 [ SNF ] [ SNF++, 12376, _t58 ] % 47.50/47.68 (356,1) [11870,1]. true => ~_t61 | _t57 [ SNF ] % 47.50/47.68 (1,1) [12071,1]. true => ~_t151 | _t86 [ SNF++, 10517 ] % 47.50/47.68 (356,1) [12159,1]. true => ~_t184 | _t61 [ SNF++, 11871 ] % 47.50/47.68 (1,1) [12278,1]. _t4 => box 1 _t149 [ SNF++, 10528 ] % 47.50/47.68 (348,1) [12376,1]. _t57 => ~box 1~ _t182 [ SNF++, 11869 ] % 47.50/47.68 (348,1) [513668,1]. true => ~_t57 | ~_t4 [ GEN1, 12278, 12376, 513647, _t149, _t182 ] % 47.50/47.68 (348,1) [513682,1]. true => ~_t86 | ~_t57 [ LRES, 513668, 10534, ~_t4 ] % 47.50/47.68 (356,1) [513715,1]. true => ~_t86 | ~_t61 [ LRES, 513682, 11870, ~_t57 ] % 47.50/47.68 (356,1) [513730,1]. true => ~_t184 | ~_t86 [ LRES, 513715, 12159, ~_t61 ] % 47.50/47.68 (356,1) [513780,1]. true => ~_t184 | ~_t151 [ LRES, 513730, 12071, ~_t86 ] % 47.50/47.68 (1,1) [6931,2]. ~_t79 => box 1 ~_t36 [ Axiom 5 ] [ SNF++, 12456, ~_t36 ] % 47.50/47.68 (1,1) [6933,2]. _t79 => box 1 _t79 [ Axiom 5 ] [ SNF++, 12458, _t79 ] % 47.50/47.68 (1,1) [7261,2]. _t35 => box 1 _t36 [ SNF ] [ SNF++, 12460, _t36 ] % 47.50/47.68 (1,1) [7588,2]. ~_t80 => box 1 ~_t35 [ Axiom 5 ] [ SNF++, 12462, ~_t35 ] % 47.50/47.68 (1,1) [7590,2]. _t80 => box 1 _t80 [ Axiom 5 ] [ SNF++, 12464, _t80 ] % 47.50/47.68 (171,1) [7762,2]. _t45 => ~box 1~ _t46 [ SNF ] [ SNF++, 12570, _t46 ] % 47.50/47.68 (1,1) [8099,2]. _t81 => ~box 1~ _t33 [ Axiom 5 ] [ SNF++, 12572, _t33 ] % 47.50/47.68 (1,1) [8101,2]. true => _t81 | ~_t33 [ Axiom T ] % 47.50/47.68 (1,1) [8102,2]. _t81 => box 1 _t81 [ Axiom 5 ] [ SNF++, 12470, _t81 ] % 47.50/47.68 (1,1) [9020,2]. _t53 => box 1 _t46 [ Axiom 5 ] [ SNF++, 12484, _t46 ] % 47.50/47.68 (1,1) [10524,2]. true => _t33 | ~_t5 [ Axiom 5 ] % 47.50/47.68 (343,1) [11866,2]. _t59 => ~box 1~ _t36 [ SNF ] [ SNF++, 12564, _t36 ] % 47.50/47.68 (348,1) [11867,2]. true => _t59 | ~_t58 [ SNF ] % 47.50/47.68 (348,1) [11868,2]. true => ~_t58 | _t45 [ SNF ] % 47.50/47.68 (1,1) [12279,2]. true => ~_t149 | _t5 [ SNF++, 10528 ] % 47.50/47.68 (348,1) [12377,2]. true => ~_t182 | _t58 [ SNF++, 11869 ] % 47.50/47.68 (1,1) [12456,2]. ~_t79 => box 1 _t129 [ SNF++, 6931 ] % 47.50/47.68 (1,1) [12458,2]. _t79 => box 1 _t130 [ SNF++, 6933 ] % 47.50/47.68 (1,1) [12462,2]. ~_t80 => box 1 _t132 [ SNF++, 7588 ] % 47.50/47.68 (1,1) [12464,2]. _t80 => box 1 _t133 [ SNF++, 7590 ] % 47.50/47.68 (1,1) [12470,2]. _t81 => box 1 _t136 [ SNF++, 8102 ] % 47.50/47.68 (343,1) [12564,2]. _t59 => ~box 1~ _t131 [ SNF++, 11866 ] % 47.50/47.68 (171,1) [12570,2]. _t45 => ~box 1~ _t143 [ SNF++, 7762 ] % 47.50/47.68 (1,1) [12572,2]. _t81 => ~box 1~ _t176 [ SNF++, 8099 ] % 47.50/47.68 (1,1) [19647,2]. true => ~_t149 | _t33 [ LRES, 10524, 12279, ~_t5 ] % 47.50/47.68 (348,1) [20243,2]. true => ~_t182 | _t59 [ LRES, 11867, 12377, ~_t58 ] % 47.50/47.68 (343,1) [33515,2]. true => _t79 | ~_t59 [ GEN1, 12456, 12564, 18563, _t129, _t131 ] % 47.50/47.68 (1,1) [42536,2]. true => ~_t149 | _t81 [ LRES, 19647, 8101, _t33 ] % 47.50/47.68 (348,1) [49546,2]. true => ~_t182 | _t79 [ LRES, 33515, 20243, ~_t59 ] % 47.50/47.68 (1,1) [428541,2]. true => ~_t81 | _t80 | ~_t79 [ GEN3, 12462, 12470, 12458, 428349, 12572, _t132, _t136, _t130, _t176 ] % 47.50/47.68 (348,1) [428644,2]. true => ~_t182 | ~_t81 | _t80 [ LRES, 428541, 49546, ~_t79 ] [ Backward Subsumption, 513636 ] % 47.50/47.68 (171,1) [513548,2]. true => ~_t80 | ~_t45 [ GEN1, 12464, 12570, 513482, _t133, _t143 ] % 47.50/47.68 (348,1) [513559,2]. true => ~_t80 | ~_t58 [ LRES, 513548, 11868, ~_t45 ] % 47.50/47.68 (348,1) [513627,2]. true => ~_t182 | ~_t80 [ LRES, 513559, 12377, ~_t58 ] % 47.50/47.68 (348,1) [513636,2]. true => ~_t182 | ~_t81 [ LRES, 513627, 428644, ~_t80 ] % 47.50/47.68 (348,1) [513647,2]. true => ~_t182 | ~_t149 [ LRES, 513636, 42536, ~_t81 ] % 47.50/47.68 (1,1) [5965,3]. true => ~_t42 | z1 [ Axiom T ] % 47.50/47.68 (1,1) [5967,3]. ~_t77 => box 1 ~_t42 [ Axiom 5 ] [ SNF++, 12662, ~_t42 ] % 47.50/47.68 (1,1) [5970,3]. true => ~_t77 | _t42 [ Axiom 5 ] % 47.50/47.68 (1,1) [6124,3]. true => ~_t44 | y1 [ Axiom T ] % 47.50/47.68 (1,1) [6257,3]. true => _t37 | ~_t36 [ Axiom T ] % 47.50/47.68 (1,1) [6258,3]. true => ~_t38 | ~z1 [ Axiom T ] % 47.50/47.68 (157,1) [6415,3]. _t39 => ~box 1~ _t40 [ Axiom T ] [ SNF++, 12778, _t40 ] % 47.50/47.68 (1,1) [6416,3]. true => _t39 | ~_t38 [ Axiom T ] % 47.50/47.68 (1,1) [6417,3]. true => ~_t43 | ~y1 [ Axiom T ] % 47.50/47.68 (1,1) [6572,3]. true => _t44 | ~_t43 [ Axiom T ] % 47.50/47.68 (1,1) [6573,3]. true => _t43 | _t38 | ~_t37 | p1 [ Axiom T ] % 47.50/47.68 (1,1) [6938,3]. _t79 => box 1 _t79 [ Axiom 5 ] [ SNF++, 12676, _t79 ] % 47.50/47.68 (1,1) [7595,3]. true => _t36 | ~_t35 [ Axiom T ] % 47.50/47.68 (1,1) [7597,3]. ~_t80 => box 1 ~_t35 [ Axiom 5 ] [ SNF++, 12680, ~_t35 ] % 47.50/47.68 (1,1) [7600,3]. true => ~_t80 | _t35 [ Axiom 5 ] % 47.50/47.68 (171,1) [7761,3]. true => ~_t46 | _t43 | _t38 | ~p1 [ SNF ] % 47.50/47.68 (1,1) [8111,3]. _t81 => ~box 1~ _t33 [ Axiom 5 ] [ SNF++, 12788, _t33 ] % 47.50/47.68 (1,1) [8114,3]. _t81 => box 1 _t81 [ Axiom 5 ] [ SNF++, 12688, _t81 ] % 47.50/47.68 (1,1) [12457,3]. true => ~_t129 | ~_t36 [ SNF++, 6931 ] % 47.50/47.68 (1,1) [12459,3]. true => ~_t130 | _t79 [ SNF++, 6933 ] % 47.50/47.68 (1,1) [12461,3]. true => ~_t131 | _t36 [ SNF++, 7261 ] % 47.50/47.68 (1,1) [12463,3]. true => ~_t132 | ~_t35 [ SNF++, 7588 ] % 47.50/47.68 (1,1) [12465,3]. true => ~_t133 | _t80 [ SNF++, 7590 ] % 47.50/47.68 (1,1) [12471,3]. true => ~_t136 | _t81 [ SNF++, 8102 ] % 47.50/47.68 (1,1) [12485,3]. true => ~_t143 | _t46 [ SNF++, 9020 ] % 47.50/47.68 (1,1) [12662,3]. ~_t77 => box 1 _t123 [ SNF++, 5967 ] % 47.50/47.68 (1,1) [12676,3]. _t79 => box 1 _t130 [ SNF++, 6938 ] % 47.50/47.68 (1,1) [12680,3]. ~_t80 => box 1 _t132 [ SNF++, 7597 ] % 47.50/47.68 (1,1) [12688,3]. _t81 => box 1 _t136 [ SNF++, 8114 ] % 47.50/47.68 (157,1) [12778,3]. _t39 => ~box 1~ _t174 [ SNF++, 6415 ] % 47.50/47.68 (1,1) [12788,3]. _t81 => ~box 1~ _t176 [ SNF++, 8111 ] % 47.50/47.68 (1,1) [18563,3]. true => ~_t131 | ~_t129 [ LRES, 12457, 12461, ~_t36 ] % 47.50/47.68 (1,1) [18614,3]. true => ~_t42 | ~_t38 [ LRES, 6258, 5965, ~z1 ] % 47.50/47.68 (1,1) [18662,3]. true => ~_t44 | ~_t43 [ LRES, 6417, 6124, ~y1 ] % 47.50/47.68 (1,1) [18782,3]. true => ~_t132 | ~_t80 [ LRES, 12463, 7600, ~_t35 ] % 47.50/47.68 (1,1) [18866,3]. true => ~_t80 | _t36 [ LRES, 7595, 7600, ~_t35 ] % 47.50/47.68 (1,1) [35281,3]. true => ~_t80 | _t37 [ LRES, 18866, 6257, _t36 ] % 47.50/47.68 (157,1) [67218,3]. true => _t77 | ~_t39 [ GEN1, 12662, 12778, 67169, _t123, _t174 ] % 47.50/47.68 (171,1) [122679,3]. true => ~_t46 | _t43 | _t38 | ~_t37 [ LRES, 7761, 6573, ~p1 ] % 47.50/47.68 (171,1) [157749,3]. true => ~_t80 | ~_t46 | _t43 | _t38 [ LRES, 122679, 35281, ~_t37 ] % 47.50/47.68 (171,1) [171805,3]. true => ~_t80 | ~_t46 | _t43 | _t39 [ LRES, 157749, 6416, _t38 ] % 47.50/47.68 (171,1) [171806,3]. true => ~_t80 | ~_t46 | _t43 | ~_t42 [ LRES, 157749, 18614, _t38 ] % 47.50/47.68 (171,1) [172858,3]. true => ~_t80 | _t77 | ~_t46 | _t43 [ LRES, 171805, 67218, _t39 ] [ Backward Subsumption, 509701 ] % 47.50/47.68 (171,1) [173181,3]. true => ~_t80 | ~_t77 | ~_t46 | _t43 [ LRES, 171806, 5970, ~_t42 ] [ Backward Subsumption, 513435 ] % 47.50/47.68 (171,1) [173652,3]. true => ~_t80 | ~_t77 | ~_t46 | _t44 [ LRES, 173181, 6572, _t43 ] [ Backward Subsumption, 513435 ] % 47.50/47.68 (171,1) [173653,3]. true => ~_t80 | ~_t77 | ~_t46 | ~_t44 [ LRES, 173181, 18662, _t43 ] [ Backward Subsumption, 513435 ] % 47.50/47.68 (171,1) [173874,3]. true => ~_t80 | _t77 | ~_t46 | _t44 [ LRES, 172858, 6572, _t43 ] [ Backward Subsumption, 509701 ] % 47.50/47.68 (171,1) [173875,3]. true => ~_t80 | _t77 | ~_t46 | ~_t44 [ LRES, 172858, 18662, _t43 ] [ Backward Subsumption, 509701 ] % 47.50/47.68 (1,1) [427257,3]. true => ~_t81 | _t80 | ~_t79 [ GEN3, 12680, 12688, 12676, 427075, 12788, _t132, _t136, _t130, _t176 ] % 47.50/47.68 (1,1) [427351,3]. true => ~_t130 | ~_t81 | _t80 [ LRES, 427257, 12459, ~_t79 ] % 47.50/47.68 (1,1) [428266,3]. true => ~_t132 | ~_t130 | ~_t81 [ LRES, 427351, 18782, _t80 ] % 47.50/47.68 (1,1) [428349,3]. true => ~_t136 | ~_t132 | ~_t130 [ LRES, 428266, 12471, ~_t81 ] % 47.50/47.68 (171,1) [509701,3]. true => ~_t80 | _t77 | ~_t46 [ LRES, 173875, 173874, ~_t44 ] % 47.50/47.68 (171,1) [509710,3]. true => ~_t143 | ~_t80 | _t77 [ LRES, 509701, 12485, ~_t46 ] [ Backward Subsumption, 513470 ] % 47.50/47.68 (171,1) [513435,3]. true => ~_t80 | ~_t77 | ~_t46 [ LRES, 173653, 173652, ~_t44 ] % 47.50/47.68 (171,1) [513439,3]. true => ~_t143 | ~_t80 | ~_t77 [ LRES, 513435, 12485, ~_t46 ] [ Backward Subsumption, 513470 ] % 47.50/47.68 (171,1) [513470,3]. true => ~_t143 | ~_t80 [ LRES, 513439, 509710, ~_t77 ] % 47.50/47.68 (171,1) [513482,3]. true => ~_t143 | ~_t133 [ LRES, 513470, 12465, ~_t80 ] % 47.50/47.68 (1,1) [5974,4]. ~_t77 => box 1 ~_t42 [ Axiom 5 ] [ SNF++, 12878, ~_t42 ] % 47.50/47.68 (1,1) [5977,4]. true => ~_t77 | _t42 [ Axiom 5 ] % 47.50/47.68 (156,1) [6414,4]. _t40 => ~box 1~ _t41 [ Axiom T ] [ SNF++, 12996, _t41 ] % 47.50/47.68 (1,1) [6957,4]. _t79 => box 1 _t79 [ Axiom 5 ] [ SNF++, 12892, _t79 ] % 47.50/47.68 (1,1) [7606,4]. ~_t80 => box 1 ~_t35 [ Axiom 5 ] [ SNF++, 12896, ~_t35 ] % 47.50/47.68 (1,1) [7609,4]. true => ~_t80 | _t35 [ Axiom 5 ] % 47.50/47.68 (1,1) [8123,4]. _t81 => ~box 1~ _t33 [ Axiom 5 ] [ SNF++, 13004, _t33 ] % 47.50/47.68 (1,1) [8126,4]. _t81 => box 1 _t81 [ Axiom 5 ] [ SNF++, 12904, _t81 ] % 47.50/47.68 (1,1) [12663,4]. true => ~_t123 | ~_t42 [ SNF++, 5967 ] % 47.50/47.68 (1,1) [12677,4]. true => ~_t130 | _t79 [ SNF++, 6938 ] % 47.50/47.68 (1,1) [12681,4]. true => ~_t132 | ~_t35 [ SNF++, 7597 ] % 47.50/47.68 (1,1) [12689,4]. true => ~_t136 | _t81 [ SNF++, 8114 ] % 47.50/47.68 (157,1) [12779,4]. true => ~_t174 | _t40 [ SNF++, 6415 ] % 47.50/47.68 (1,1) [12878,4]. ~_t77 => box 1 _t123 [ SNF++, 5974 ] % 47.50/47.68 (1,1) [12892,4]. _t79 => box 1 _t130 [ SNF++, 6957 ] % 47.50/47.68 (1,1) [12896,4]. ~_t80 => box 1 _t132 [ SNF++, 7606 ] % 47.50/47.68 (1,1) [12904,4]. _t81 => box 1 _t136 [ SNF++, 8126 ] % 47.50/47.68 (156,1) [12996,4]. _t40 => ~box 1~ _t186 [ SNF++, 6414 ] % 47.50/47.68 (1,1) [13004,4]. _t81 => ~box 1~ _t176 [ SNF++, 8123 ] % 47.50/47.68 (1,1) [18435,4]. true => ~_t123 | ~_t77 [ LRES, 12663, 5977, ~_t42 ] % 47.50/47.68 (1,1) [18784,4]. true => ~_t132 | ~_t80 [ LRES, 12681, 7609, ~_t35 ] % 47.50/47.68 (156,1) [64029,4]. true => _t77 | ~_t40 [ GEN1, 12878, 12996, 53284, _t123, _t186 ] % 47.50/47.68 (157,1) [64125,4]. true => ~_t174 | _t77 [ LRES, 64029, 12779, ~_t40 ] % 47.50/47.68 (157,1) [67169,4]. true => ~_t174 | ~_t123 [ LRES, 64125, 18435, _t77 ] % 47.50/47.68 (1,1) [426228,4]. true => ~_t81 | _t80 | ~_t79 [ GEN3, 12896, 12904, 12892, 425866, 13004, _t132, _t136, _t130, _t176 ] % 47.50/47.68 (1,1) [426318,4]. true => ~_t130 | ~_t81 | _t80 [ LRES, 426228, 12677, ~_t79 ] % 47.50/47.68 (1,1) [426984,4]. true => ~_t132 | ~_t130 | ~_t81 [ LRES, 426318, 18784, _t80 ] % 47.50/47.68 (1,1) [427075,4]. true => ~_t136 | ~_t132 | ~_t130 [ LRES, 426984, 12689, ~_t81 ] % 47.50/47.68 (1,1) [5981,5]. ~_t77 => box 1 ~_t42 [ Axiom 5 ] [ SNF++, 13094, ~_t42 ] % 47.50/47.68 (1,1) [5984,5]. true => ~_t77 | _t42 [ Axiom 5 ] % 47.50/47.68 (155,1) [6413,5]. _t41 => ~box 1~ _t42 [ Axiom T ] [ SNF++, 13204, _t42 ] % 47.50/47.68 (1,1) [6976,5]. _t79 => box 1 _t79 [ Axiom 5 ] [ SNF++, 13108, _t79 ] % 47.50/47.68 (1,1) [7615,5]. ~_t80 => box 1 ~_t35 [ Axiom 5 ] [ SNF++, 13112, ~_t35 ] % 47.50/47.68 (1,1) [7618,5]. true => ~_t80 | _t35 [ Axiom 5 ] % 47.50/47.68 (1,1) [8135,5]. _t81 => ~box 1~ _t33 [ Axiom 5 ] [ SNF++, 13220, _t33 ] % 47.50/47.68 (1,1) [8138,5]. _t81 => box 1 _t81 [ Axiom 5 ] [ SNF++, 13120, _t81 ] % 47.50/47.68 (1,1) [12879,5]. true => ~_t123 | ~_t42 [ SNF++, 5974 ] % 47.50/47.68 (1,1) [12893,5]. true => ~_t130 | _t79 [ SNF++, 6957 ] % 47.50/47.68 (1,1) [12897,5]. true => ~_t132 | ~_t35 [ SNF++, 7606 ] % 47.50/47.68 (1,1) [12905,5]. true => ~_t136 | _t81 [ SNF++, 8126 ] % 47.50/47.68 (156,1) [12997,5]. true => ~_t186 | _t41 [ SNF++, 6414 ] % 47.50/47.68 (1,1) [13094,5]. ~_t77 => box 1 _t123 [ SNF++, 5981 ] % 47.50/47.68 (1,1) [13108,5]. _t79 => box 1 _t130 [ SNF++, 6976 ] % 47.50/47.68 (1,1) [13112,5]. ~_t80 => box 1 _t132 [ SNF++, 7615 ] % 47.50/47.68 (1,1) [13120,5]. _t81 => box 1 _t136 [ SNF++, 8138 ] % 47.50/47.68 (155,1) [13204,5]. _t41 => ~box 1~ _t172 [ SNF++, 6413 ] % 47.50/47.68 (1,1) [13220,5]. _t81 => ~box 1~ _t176 [ SNF++, 8135 ] % 47.50/47.68 (1,1) [18394,5]. true => ~_t123 | ~_t77 [ LRES, 12879, 5984, ~_t42 ] % 47.50/47.68 (1,1) [18786,5]. true => ~_t132 | ~_t80 [ LRES, 12897, 7618, ~_t35 ] % 47.50/47.68 (155,1) [31725,5]. true => _t77 | ~_t41 [ GEN1, 13094, 13204, 18397, _t123, _t172 ] % 47.50/47.68 (156,1) [49466,5]. true => ~_t186 | _t77 [ LRES, 31725, 12997, ~_t41 ] % 47.50/47.68 (156,1) [53284,5]. true => ~_t186 | ~_t123 [ LRES, 49466, 18394, _t77 ] % 47.50/47.68 (1,1) [424898,5]. true => ~_t81 | _t80 | ~_t79 [ GEN3, 13112, 13120, 13108, 424312, 13220, _t132, _t136, _t130, _t176 ] % 47.50/47.68 (1,1) [424951,5]. true => ~_t130 | ~_t81 | _t80 [ LRES, 424898, 12893, ~_t79 ] % 47.50/47.68 (1,1) [425785,5]. true => ~_t132 | ~_t130 | ~_t81 [ LRES, 424951, 18786, _t80 ] % 47.50/47.68 (1,1) [425866,5]. true => ~_t136 | ~_t132 | ~_t130 [ LRES, 425785, 12905, ~_t81 ] % 47.50/47.68 (1,1) [6995,6]. _t79 => box 1 _t79 [ Axiom 5 ] [ SNF++, 13324, _t79 ] % 47.50/47.68 (1,1) [7624,6]. ~_t80 => box 1 ~_t35 [ Axiom 5 ] [ SNF++, 13328, ~_t35 ] % 47.50/47.68 (1,1) [7627,6]. true => ~_t80 | _t35 [ Axiom 5 ] % 47.50/47.68 (1,1) [8147,6]. _t81 => ~box 1~ _t33 [ Axiom 5 ] [ SNF++, 13436, _t33 ] % 47.50/47.68 (1,1) [8150,6]. _t81 => box 1 _t81 [ Axiom 5 ] [ SNF++, 13336, _t81 ] % 47.50/47.68 (1,1) [13095,6]. true => ~_t123 | ~_t42 [ SNF++, 5981 ] % 47.50/47.68 (1,1) [13109,6]. true => ~_t130 | _t79 [ SNF++, 6976 ] % 47.50/47.68 (1,1) [13113,6]. true => ~_t132 | ~_t35 [ SNF++, 7615 ] % 47.50/47.68 (1,1) [13121,6]. true => ~_t136 | _t81 [ SNF++, 8138 ] % 47.50/47.68 (155,1) [13205,6]. true => ~_t172 | _t42 [ SNF++, 6413 ] % 47.50/47.68 (1,1) [13324,6]. _t79 => box 1 _t130 [ SNF++, 6995 ] % 47.50/47.68 (1,1) [13328,6]. ~_t80 => box 1 _t132 [ SNF++, 7624 ] % 47.50/47.68 (1,1) [13336,6]. _t81 => box 1 _t136 [ SNF++, 8150 ] % 47.50/47.68 (1,1) [13436,6]. _t81 => ~box 1~ _t176 [ SNF++, 8147 ] % 47.50/47.68 (155,1) [18397,6]. true => ~_t172 | ~_t123 [ LRES, 13095, 13205, ~_t42 ] % 47.50/47.68 (1,1) [18788,6]. true => ~_t132 | ~_t80 [ LRES, 13113, 7627, ~_t35 ] % 47.50/47.68 (1,1) [424067,6]. true => ~_t81 | _t80 | ~_t79 [ GEN3, 13328, 13336, 13324, 424004, 13436, _t132, _t136, _t130, _t176 ] % 47.50/47.68 (1,1) [424209,6]. true => ~_t130 | ~_t81 | _t80 [ LRES, 424067, 13109, ~_t79 ] % 47.50/47.68 (1,1) [424247,6]. true => ~_t132 | ~_t130 | ~_t81 [ LRES, 424209, 18788, _t80 ] % 47.50/47.68 (1,1) [424312,6]. true => ~_t136 | ~_t132 | ~_t130 [ LRES, 424247, 13121, ~_t81 ] % 47.50/47.68 (1,1) [7014,7]. _t79 => box 1 _t79 [ Axiom 5 ] [ SNF++, 13540, _t79 ] % 47.50/47.68 (1,1) [7633,7]. ~_t80 => box 1 ~_t35 [ Axiom 5 ] [ SNF++, 13544, ~_t35 ] % 47.50/47.68 (1,1) [7636,7]. true => ~_t80 | _t35 [ Axiom 5 ] % 47.50/47.68 (1,1) [8159,7]. _t81 => ~box 1~ _t33 [ Axiom 5 ] [ SNF++, 13652, _t33 ] % 47.50/47.68 (1,1) [8162,7]. _t81 => box 1 _t81 [ Axiom 5 ] [ SNF++, 13552, _t81 ] % 47.50/47.68 (1,1) [13325,7]. true => ~_t130 | _t79 [ SNF++, 6995 ] % 47.50/47.68 (1,1) [13329,7]. true => ~_t132 | ~_t35 [ SNF++, 7624 ] % 47.50/47.68 (1,1) [13337,7]. true => ~_t136 | _t81 [ SNF++, 8150 ] % 47.50/47.68 (1,1) [13540,7]. _t79 => box 1 _t130 [ SNF++, 7014 ] % 47.50/47.68 (1,1) [13544,7]. ~_t80 => box 1 _t132 [ SNF++, 7633 ] % 47.50/47.68 (1,1) [13552,7]. _t81 => box 1 _t136 [ SNF++, 8162 ] % 47.50/47.68 (1,1) [13652,7]. _t81 => ~box 1~ _t176 [ SNF++, 8159 ] % 47.50/47.68 (1,1) [18790,7]. true => ~_t132 | ~_t80 [ LRES, 13329, 7636, ~_t35 ] % 47.50/47.68 (1,1) [423822,7]. true => ~_t81 | _t80 | ~_t79 [ GEN3, 13544, 13552, 13540, 423454, 13652, _t132, _t136, _t130, _t176 ] % 47.50/47.68 (1,1) [423925,7]. true => ~_t130 | ~_t81 | _t80 [ LRES, 423822, 13325, ~_t79 ] % 47.50/47.68 (1,1) [423948,7]. true => ~_t132 | ~_t130 | ~_t81 [ LRES, 423925, 18790, _t80 ] % 47.50/47.68 (1,1) [424004,7]. true => ~_t136 | ~_t132 | ~_t130 [ LRES, 423948, 13337, ~_t81 ] % 47.50/47.68 (1,1) [7033,8]. _t79 => box 1 _t79 [ Axiom 5 ] [ SNF++, 13756, _t79 ] % 47.50/47.68 (1,1) [7642,8]. ~_t80 => box 1 ~_t35 [ Axiom 5 ] [ SNF++, 13760, ~_t35 ] % 47.50/47.68 (1,1) [7645,8]. true => ~_t80 | _t35 [ Axiom 5 ] % 47.50/47.68 (1,1) [8171,8]. _t81 => ~box 1~ _t33 [ Axiom 5 ] [ SNF++, 13868, _t33 ] % 47.50/47.68 (1,1) [8174,8]. _t81 => box 1 _t81 [ Axiom 5 ] [ SNF++, 13768, _t81 ] % 47.50/47.68 (1,1) [13541,8]. true => ~_t130 | _t79 [ SNF++, 7014 ] % 47.50/47.68 (1,1) [13545,8]. true => ~_t132 | ~_t35 [ SNF++, 7633 ] % 47.50/47.68 (1,1) [13553,8]. true => ~_t136 | _t81 [ SNF++, 8162 ] % 47.50/47.68 (1,1) [13756,8]. _t79 => box 1 _t130 [ SNF++, 7033 ] % 47.50/47.68 (1,1) [13760,8]. ~_t80 => box 1 _t132 [ SNF++, 7642 ] % 47.50/47.68 (1,1) [13768,8]. _t81 => box 1 _t136 [ SNF++, 8174 ] % 47.50/47.68 (1,1) [13868,8]. _t81 => ~box 1~ _t176 [ SNF++, 8171 ] % 47.50/47.68 (1,1) [18792,8]. true => ~_t132 | ~_t80 [ LRES, 13545, 7645, ~_t35 ] % 47.50/47.68 (1,1) [422138,8]. true => ~_t81 | _t80 | ~_t79 [ GEN3, 13760, 13768, 13756, 421989, 13868, _t132, _t136, _t130, _t176 ] % 47.50/47.68 (1,1) [422193,8]. true => ~_t130 | ~_t81 | _t80 [ LRES, 422138, 13541, ~_t79 ] % 47.50/47.68 (1,1) [423403,8]. true => ~_t132 | ~_t130 | ~_t81 [ LRES, 422193, 18792, _t80 ] % 47.50/47.68 (1,1) [423454,8]. true => ~_t136 | ~_t132 | ~_t130 [ LRES, 423403, 13553, ~_t81 ] % 47.50/47.68 (1,1) [7052,9]. _t79 => box 1 _t79 [ Axiom 5 ] [ SNF++, 13972, _t79 ] % 47.50/47.68 (1,1) [7651,9]. ~_t80 => box 1 ~_t35 [ Axiom 5 ] [ SNF++, 13976, ~_t35 ] % 47.50/47.68 (1,1) [7654,9]. true => ~_t80 | _t35 [ Axiom 5 ] % 47.50/47.68 (1,1) [8183,9]. _t81 => ~box 1~ _t33 [ Axiom 5 ] [ SNF++, 14084, _t33 ] % 47.50/47.68 (1,1) [8186,9]. _t81 => box 1 _t81 [ Axiom 5 ] [ SNF++, 13984, _t81 ] % 47.50/47.68 (1,1) [13757,9]. true => ~_t130 | _t79 [ SNF++, 7033 ] % 47.50/47.68 (1,1) [13761,9]. true => ~_t132 | ~_t35 [ SNF++, 7642 ] % 47.50/47.68 (1,1) [13769,9]. true => ~_t136 | _t81 [ SNF++, 8174 ] % 47.50/47.68 (1,1) [13972,9]. _t79 => box 1 _t130 [ SNF++, 7052 ] % 47.50/47.68 (1,1) [13976,9]. ~_t80 => box 1 _t132 [ SNF++, 7651 ] % 47.50/47.68 (1,1) [13984,9]. _t81 => box 1 _t136 [ SNF++, 8186 ] % 47.50/47.68 (1,1) [14084,9]. _t81 => ~box 1~ _t176 [ SNF++, 8183 ] % 47.50/47.68 (1,1) [18794,9]. true => ~_t132 | ~_t80 [ LRES, 13761, 7654, ~_t35 ] % 47.50/47.68 (1,1) [421122,9]. true => ~_t81 | _t80 | ~_t79 [ GEN3, 13976, 13984, 13972, 420864, 14084, _t132, _t136, _t130, _t176 ] % 47.50/47.68 (1,1) [421168,9]. true => ~_t130 | ~_t81 | _t80 [ LRES, 421122, 13757, ~_t79 ] % 47.50/47.68 (1,1) [421939,9]. true => ~_t132 | ~_t130 | ~_t81 [ LRES, 421168, 18794, _t80 ] % 47.50/47.68 (1,1) [421989,9]. true => ~_t136 | ~_t132 | ~_t130 [ LRES, 421939, 13769, ~_t81 ] % 47.50/47.68 (1,1) [7071,10]. _t79 => box 1 _t79 [ Axiom 5 ] [ SNF++, 14188, _t79 ] % 47.50/47.68 (1,1) [7660,10]. ~_t80 => box 1 ~_t35 [ Axiom 5 ] [ SNF++, 14192, ~_t35 ] % 47.50/47.68 (1,1) [7663,10]. true => ~_t80 | _t35 [ Axiom 5 ] % 47.50/47.68 (1,1) [8195,10]. _t81 => ~box 1~ _t33 [ Axiom 5 ] [ SNF++, 14300, _t33 ] % 47.50/47.68 (1,1) [8198,10]. _t81 => box 1 _t81 [ Axiom 5 ] [ SNF++, 14200, _t81 ] % 47.50/47.68 (1,1) [13973,10]. true => ~_t130 | _t79 [ SNF++, 7052 ] % 47.50/47.68 (1,1) [13977,10]. true => ~_t132 | ~_t35 [ SNF++, 7651 ] % 47.50/47.68 (1,1) [13985,10]. true => ~_t136 | _t81 [ SNF++, 8186 ] % 47.50/47.68 (1,1) [14188,10]. _t79 => box 1 _t130 [ SNF++, 7071 ] % 47.50/47.68 (1,1) [14192,10]. ~_t80 => box 1 _t132 [ SNF++, 7660 ] % 47.50/47.68 (1,1) [14200,10]. _t81 => box 1 _t136 [ SNF++, 8198 ] % 47.50/47.68 (1,1) [14300,10]. _t81 => ~box 1~ _t176 [ SNF++, 8195 ] % 47.50/47.68 (1,1) [18796,10]. true => ~_t132 | ~_t80 [ LRES, 13977, 7663, ~_t35 ] % 47.50/47.68 (1,1) [419652,10]. true => ~_t81 | _t80 | ~_t79 [ GEN3, 14192, 14200, 14188, 419606, 14300, _t132, _t136, _t130, _t176 ] % 47.50/47.68 (1,1) [419752,10]. true => ~_t130 | ~_t81 | _t80 [ LRES, 419652, 13973, ~_t79 ] % 47.50/47.68 (1,1) [420783,10]. true => ~_t132 | ~_t130 | ~_t81 [ LRES, 419752, 18796, _t80 ] % 47.50/47.68 (1,1) [420864,10]. true => ~_t136 | ~_t132 | ~_t130 [ LRES, 420783, 13985, ~_t81 ] % 47.50/47.68 (1,1) [7090,11]. _t79 => box 1 _t79 [ Axiom 5 ] [ SNF++, 14404, _t79 ] % 47.50/47.68 (1,1) [7669,11]. ~_t80 => box 1 ~_t35 [ Axiom 5 ] [ SNF++, 14408, ~_t35 ] % 47.50/47.68 (1,1) [7672,11]. true => ~_t80 | _t35 [ Axiom 5 ] % 47.50/47.68 (1,1) [8207,11]. _t81 => ~box 1~ _t33 [ Axiom 5 ] [ SNF++, 14516, _t33 ] % 47.50/47.68 (1,1) [8210,11]. _t81 => box 1 _t81 [ Axiom 5 ] [ SNF++, 14416, _t81 ] % 47.50/47.68 (1,1) [14189,11]. true => ~_t130 | _t79 [ SNF++, 7071 ] % 47.50/47.68 (1,1) [14193,11]. true => ~_t132 | ~_t35 [ SNF++, 7660 ] % 47.50/47.68 (1,1) [14201,11]. true => ~_t136 | _t81 [ SNF++, 8198 ] % 47.50/47.68 (1,1) [14404,11]. _t79 => box 1 _t130 [ SNF++, 7090 ] % 47.50/47.68 (1,1) [14408,11]. ~_t80 => box 1 _t132 [ SNF++, 7669 ] % 47.50/47.68 (1,1) [14416,11]. _t81 => box 1 _t136 [ SNF++, 8210 ] % 47.50/47.68 (1,1) [14516,11]. _t81 => ~box 1~ _t176 [ SNF++, 8207 ] % 47.50/47.68 (1,1) [18798,11]. true => ~_t132 | ~_t80 [ LRES, 14193, 7672, ~_t35 ] % 47.50/47.68 (1,1) [418522,11]. true => ~_t81 | _t80 | ~_t79 [ GEN3, 14408, 14416, 14404, 418145, 14516, _t132, _t136, _t130, _t176 ] % 47.50/47.68 (1,1) [418579,11]. true => ~_t130 | ~_t81 | _t80 [ LRES, 418522, 14189, ~_t79 ] % 47.50/47.68 (1,1) [419550,11]. true => ~_t132 | ~_t130 | ~_t81 [ LRES, 418579, 18798, _t80 ] % 47.50/47.68 (1,1) [419606,11]. true => ~_t136 | ~_t132 | ~_t130 [ LRES, 419550, 14201, ~_t81 ] % 47.50/47.68 (1,1) [7109,12]. _t79 => box 1 _t79 [ Axiom 5 ] [ SNF++, 14620, _t79 ] % 47.50/47.68 (1,1) [7678,12]. ~_t80 => box 1 ~_t35 [ Axiom 5 ] [ SNF++, 14624, ~_t35 ] % 47.50/47.68 (1,1) [7681,12]. true => ~_t80 | _t35 [ Axiom 5 ] % 47.50/47.68 (1,1) [8219,12]. _t81 => ~box 1~ _t33 [ Axiom 5 ] [ SNF++, 14732, _t33 ] % 47.50/47.68 (1,1) [8222,12]. _t81 => box 1 _t81 [ Axiom 5 ] [ SNF++, 14632, _t81 ] % 47.50/47.68 (1,1) [14405,12]. true => ~_t130 | _t79 [ SNF++, 7090 ] % 47.50/47.68 (1,1) [14409,12]. true => ~_t132 | ~_t35 [ SNF++, 7669 ] % 47.50/47.68 (1,1) [14417,12]. true => ~_t136 | _t81 [ SNF++, 8210 ] % 47.50/47.68 (1,1) [14620,12]. _t79 => box 1 _t130 [ SNF++, 7109 ] % 47.50/47.68 (1,1) [14624,12]. ~_t80 => box 1 _t132 [ SNF++, 7678 ] % 47.50/47.68 (1,1) [14632,12]. _t81 => box 1 _t136 [ SNF++, 8222 ] % 47.50/47.68 (1,1) [14732,12]. _t81 => ~box 1~ _t176 [ SNF++, 8219 ] % 47.50/47.68 (1,1) [18800,12]. true => ~_t132 | ~_t80 [ LRES, 14409, 7681, ~_t35 ] % 47.50/47.68 (1,1) [416999,12]. true => ~_t81 | _t80 | ~_t79 [ GEN3, 14624, 14632, 14620, 416806, 14732, _t132, _t136, _t130, _t176 ] % 47.50/47.68 (1,1) [417058,12]. true => ~_t130 | ~_t81 | _t80 [ LRES, 416999, 14405, ~_t79 ] % 47.50/47.68 (1,1) [418019,12]. true => ~_t132 | ~_t130 | ~_t81 [ LRES, 417058, 18800, _t80 ] % 47.50/47.68 (1,1) [418145,12]. true => ~_t136 | ~_t132 | ~_t130 [ LRES, 418019, 14417, ~_t81 ] % 47.50/47.68 (1,1) [7128,13]. _t79 => box 1 _t79 [ Axiom 5 ] [ SNF++, 14836, _t79 ] % 47.50/47.68 (1,1) [7687,13]. ~_t80 => box 1 ~_t35 [ Axiom 5 ] [ SNF++, 14840, ~_t35 ] % 47.50/47.68 (1,1) [7690,13]. true => ~_t80 | _t35 [ Axiom 5 ] % 47.50/47.68 (1,1) [8231,13]. _t81 => ~box 1~ _t33 [ Axiom 5 ] [ SNF++, 14948, _t33 ] % 47.50/47.68 (1,1) [8234,13]. _t81 => box 1 _t81 [ Axiom 5 ] [ SNF++, 14848, _t81 ] % 47.50/47.68 (1,1) [14621,13]. true => ~_t130 | _t79 [ SNF++, 7109 ] % 47.50/47.68 (1,1) [14625,13]. true => ~_t132 | ~_t35 [ SNF++, 7678 ] % 47.50/47.68 (1,1) [14633,13]. true => ~_t136 | _t81 [ SNF++, 8222 ] % 47.50/47.68 (1,1) [14836,13]. _t79 => box 1 _t130 [ SNF++, 7128 ] % 47.50/47.68 (1,1) [14840,13]. ~_t80 => box 1 _t132 [ SNF++, 7687 ] % 47.50/47.68 (1,1) [14848,13]. _t81 => box 1 _t136 [ SNF++, 8234 ] % 47.50/47.68 (1,1) [14948,13]. _t81 => ~box 1~ _t176 [ SNF++, 8231 ] % 47.50/47.68 (1,1) [18802,13]. true => ~_t132 | ~_t80 [ LRES, 14625, 7690, ~_t35 ] % 47.50/47.68 (1,1) [415611,13]. true => ~_t81 | _t80 | ~_t79 [ GEN3, 14840, 14848, 14836, 415587, 14948, _t132, _t136, _t130, _t176 ] % 47.50/47.68 (1,1) [415645,13]. true => ~_t130 | ~_t81 | _t80 [ LRES, 415611, 14621, ~_t79 ] % 47.50/47.68 (1,1) [416729,13]. true => ~_t132 | ~_t130 | ~_t81 [ LRES, 415645, 18802, _t80 ] % 47.50/47.68 (1,1) [416806,13]. true => ~_t136 | ~_t132 | ~_t130 [ LRES, 416729, 14633, ~_t81 ] % 47.50/47.68 (1,1) [7147,14]. _t79 => box 1 _t79 [ Axiom 5 ] [ SNF++, 15052, _t79 ] % 47.50/47.68 (1,1) [7696,14]. ~_t80 => box 1 ~_t35 [ Axiom 5 ] [ SNF++, 15056, ~_t35 ] % 47.56/47.68 (1,1) [7699,14]. true => ~_t80 | _t35 [ Axiom 5 ] % 47.56/47.68 (1,1) [8243,14]. _t81 => ~box 1~ _t33 [ Axiom 5 ] [ SNF++, 15164, _t33 ] % 47.56/47.68 (1,1) [8246,14]. _t81 => box 1 _t81 [ Axiom 5 ] [ SNF++, 15064, _t81 ] % 47.56/47.68 (1,1) [14837,14]. true => ~_t130 | _t79 [ SNF++, 7128 ] % 47.56/47.68 (1,1) [14841,14]. true => ~_t132 | ~_t35 [ SNF++, 7687 ] % 47.56/47.68 (1,1) [14849,14]. true => ~_t136 | _t81 [ SNF++, 8234 ] % 47.56/47.68 (1,1) [15052,14]. _t79 => box 1 _t130 [ SNF++, 7147 ] % 47.56/47.68 (1,1) [15056,14]. ~_t80 => box 1 _t132 [ SNF++, 7696 ] % 47.56/47.68 (1,1) [15064,14]. _t81 => box 1 _t136 [ SNF++, 8246 ] % 47.56/47.68 (1,1) [15164,14]. _t81 => ~box 1~ _t176 [ SNF++, 8243 ] % 47.56/47.68 (1,1) [18804,14]. true => ~_t132 | ~_t80 [ LRES, 14841, 7699, ~_t35 ] % 47.56/47.68 (1,1) [414545,14]. true => ~_t81 | _t80 | ~_t79 [ GEN3, 15056, 15064, 15052, 414284, 15164, _t132, _t136, _t130, _t176 ] % 47.56/47.68 (1,1) [414612,14]. true => ~_t130 | ~_t81 | _t80 [ LRES, 414545, 14837, ~_t79 ] % 47.56/47.68 (1,1) [415545,14]. true => ~_t132 | ~_t130 | ~_t81 [ LRES, 414612, 18804, _t80 ] % 47.56/47.68 (1,1) [415587,14]. true => ~_t136 | ~_t132 | ~_t130 [ LRES, 415545, 14849, ~_t81 ] % 47.56/47.68 (1,1) [7166,15]. _t79 => box 1 _t79 [ Axiom 5 ] [ SNF++, 15268, _t79 ] % 47.56/47.68 (1,1) [7705,15]. ~_t80 => box 1 ~_t35 [ Axiom 5 ] [ SNF++, 15272, ~_t35 ] % 47.56/47.68 (1,1) [7708,15]. true => ~_t80 | _t35 [ Axiom 5 ] % 47.56/47.68 (1,1) [8255,15]. _t81 => ~box 1~ _t33 [ Axiom 5 ] [ SNF++, 15380, _t33 ] % 47.56/47.68 (1,1) [8258,15]. _t81 => box 1 _t81 [ Axiom 5 ] [ SNF++, 15280, _t81 ] % 47.56/47.68 (1,1) [15053,15]. true => ~_t130 | _t79 [ SNF++, 7147 ] % 47.56/47.68 (1,1) [15057,15]. true => ~_t132 | ~_t35 [ SNF++, 7696 ] % 47.56/47.68 (1,1) [15065,15]. true => ~_t136 | _t81 [ SNF++, 8246 ] % 47.56/47.68 (1,1) [15268,15]. _t79 => box 1 _t130 [ SNF++, 7166 ] % 47.56/47.68 (1,1) [15272,15]. ~_t80 => box 1 _t132 [ SNF++, 7705 ] % 47.56/47.68 (1,1) [15280,15]. _t81 => box 1 _t136 [ SNF++, 8258 ] % 47.56/47.68 (1,1) [15380,15]. _t81 => ~box 1~ _t176 [ SNF++, 8255 ] % 47.56/47.68 (1,1) [18806,15]. true => ~_t132 | ~_t80 [ LRES, 15057, 7708, ~_t35 ] % 47.56/47.68 (1,1) [413018,15]. true => ~_t81 | _t80 | ~_t79 [ GEN3, 15272, 15280, 15268, 412832, 15380, _t132, _t136, _t130, _t176 ] % 47.56/47.68 (1,1) [413177,15]. true => ~_t130 | ~_t81 | _t80 [ LRES, 413018, 15053, ~_t79 ] % 47.56/47.68 (1,1) [413947,15]. true => ~_t132 | ~_t130 | ~_t81 [ LRES, 413177, 18806, _t80 ] % 47.56/47.68 (1,1) [414284,15]. true => ~_t136 | ~_t132 | ~_t130 [ LRES, 413947, 15065, ~_t81 ] % 47.56/47.68 (1,1) [7185,16]. _t79 => box 1 _t79 [ Axiom 5 ] [ SNF++, 15484, _t79 ] % 47.56/47.68 (1,1) [7714,16]. ~_t80 => box 1 ~_t35 [ Axiom 5 ] [ SNF++, 15488, ~_t35 ] % 47.56/47.68 (1,1) [7717,16]. true => ~_t80 | _t35 [ Axiom 5 ] % 47.56/47.68 (1,1) [8267,16]. _t81 => ~box 1~ _t33 [ Axiom 5 ] [ SNF++, 15596, _t33 ] % 47.56/47.68 (1,1) [8270,16]. _t81 => box 1 _t81 [ Axiom 5 ] [ SNF++, 15496, _t81 ] % 47.56/47.68 (1,1) [15269,16]. true => ~_t130 | _t79 [ SNF++, 7166 ] % 47.56/47.68 (1,1) [15273,16]. true => ~_t132 | ~_t35 [ SNF++, 7705 ] % 47.56/47.68 (1,1) [15281,16]. true => ~_t136 | _t81 [ SNF++, 8258 ] % 47.56/47.68 (1,1) [15484,16]. _t79 => box 1 _t130 [ SNF++, 7185 ] % 47.56/47.68 (1,1) [15488,16]. ~_t80 => box 1 _t132 [ SNF++, 7714 ] % 47.56/47.68 (1,1) [15496,16]. _t81 => box 1 _t136 [ SNF++, 8270 ] % 47.56/47.68 (1,1) [15596,16]. _t81 => ~box 1~ _t176 [ SNF++, 8267 ] % 47.56/47.68 (1,1) [18808,16]. true => ~_t132 | ~_t80 [ LRES, 15273, 7717, ~_t35 ] % 47.56/47.68 (1,1) [411213,16]. true => ~_t81 | _t80 | ~_t79 [ GEN3, 15488, 15496, 15484, 410899, 15596, _t132, _t136, _t130, _t176 ] % 47.56/47.68 (1,1) [411278,16]. true => ~_t130 | ~_t81 | _t80 [ LRES, 411213, 15269, ~_t79 ] % 47.56/47.68 (1,1) [412795,16]. true => ~_t132 | ~_t130 | ~_t81 [ LRES, 411278, 18808, _t80 ] % 47.56/47.68 (1,1) [412832,16]. true => ~_t136 | ~_t132 | ~_t130 [ LRES, 412795, 15281, ~_t81 ] % 47.56/47.68 (1,1) [7201,17]. _t79 => ~box 1~ _t36 [ Axiom 5 ] [ SNF++, 15806, _t36 ] % 47.56/47.68 (1,1) [7720,17]. _t35 => box 1 _t36 [ Axiom 5 ] [ SNF++, 15702, _t36 ] % 47.56/47.68 (1,1) [7723,17]. ~_t80 => box 1 ~_t35 [ Axiom 5 ] [ SNF++, 15704, ~_t35 ] % 47.56/47.68 (1,1) [7726,17]. true => ~_t80 | _t35 [ Axiom 5 ] % 47.56/47.68 (1,1) [8282,17]. _t81 => box 1 _t81 [ Axiom 5 ] [ SNF++, 15712, _t81 ] % 47.56/47.68 (1,1) [15485,17]. true => ~_t130 | _t79 [ SNF++, 7185 ] % 47.56/47.68 (1,1) [15489,17]. true => ~_t132 | ~_t35 [ SNF++, 7714 ] % 47.56/47.68 (1,1) [15497,17]. true => ~_t136 | _t81 [ SNF++, 8270 ] % 47.56/47.68 (1,1) [15704,17]. ~_t80 => box 1 _t132 [ SNF++, 7723 ] % 47.56/47.68 (1,1) [15712,17]. _t81 => box 1 _t136 [ SNF++, 8282 ] % 47.56/47.68 (1,1) [15806,17]. _t79 => ~box 1~ _t131 [ SNF++, 7201 ] % 47.56/47.68 (1,1) [18810,17]. true => ~_t132 | ~_t80 [ LRES, 15489, 7726, ~_t35 ] % 47.56/47.68 (1,1) [344753,17]. true => ~_t81 | _t80 | ~_t79 [ GEN1, 15712, 15704, 15806, 317367, _t136, _t132, _t131 ] % 47.56/47.68 (1,1) [344808,17]. true => ~_t130 | ~_t81 | _t80 [ LRES, 344753, 15485, ~_t79 ] % 47.56/47.68 (1,1) [410849,17]. true => ~_t132 | ~_t130 | ~_t81 [ LRES, 344808, 18810, _t80 ] % 47.56/47.68 (1,1) [410899,17]. true => ~_t136 | ~_t132 | ~_t130 [ LRES, 410849, 15497, ~_t81 ] % 47.56/47.68 (1,1) [7216,18]. _t36 => box 1 _t37 [ Axiom 5 ] [ SNF++, 15912, _t37 ] % 47.56/47.68 (171,1) [8275,18]. _t45 => ~box 1~ _t46 [ Axiom 5 ] [ SNF++, 16026, _t46 ] % 47.56/47.68 (1,1) [8276,18]. true => _t45 | _t35 | ~_t34 [ Axiom 5 ] % 47.56/47.68 (1,1) [8290,18]. true => _t34 | ~_t33 [ Axiom T ] % 47.56/47.68 (1,1) [8295,18]. true => ~_t81 | _t33 [ Axiom 5 ] % 47.56/47.68 (1,1) [9130,18]. _t53 => box 1 _t46 [ Axiom 5 ] [ SNF++, 15942, _t46 ] % 47.56/47.68 (1,1) [15703,18]. true => ~_t131 | _t36 [ SNF++, 7720 ] % 47.56/47.68 (1,1) [15705,18]. true => ~_t132 | ~_t35 [ SNF++, 7723 ] % 47.56/47.68 (1,1) [15713,18]. true => ~_t136 | _t81 [ SNF++, 8282 ] % 47.56/47.68 (1,1) [15912,18]. _t36 => box 1 _t128 [ SNF++, 7216 ] % 47.56/47.68 (171,1) [16026,18]. _t45 => ~box 1~ _t143 [ SNF++, 8275 ] % 47.56/47.68 (1,1) [19022,18]. true => ~_t81 | _t34 [ LRES, 8290, 8295, ~_t33 ] % 47.56/47.68 (1,1) [67253,18]. true => ~_t81 | _t45 | _t35 [ LRES, 8276, 19022, ~_t34 ] % 47.56/47.68 (1,1) [96082,18]. true => ~_t132 | ~_t81 | _t45 [ LRES, 67253, 15705, _t35 ] % 47.56/47.68 (171,1) [307728,18]. true => ~_t45 | ~_t36 [ GEN1, 15912, 16026, 307661, _t128, _t143 ] % 47.56/47.68 (171,1) [313509,18]. true => ~_t131 | ~_t45 [ LRES, 307728, 15703, ~_t36 ] % 47.56/47.68 (171,1) [313547,18]. true => ~_t132 | ~_t131 | ~_t81 [ LRES, 313509, 96082, ~_t45 ] % 47.56/47.68 (171,1) [317367,18]. true => ~_t136 | ~_t132 | ~_t131 [ LRES, 313547, 15713, ~_t81 ] % 47.56/47.68 (1,1) [6075,19]. true => ~_t42 | z1 [ Axiom T ] % 47.56/47.68 (1,1) [6077,19]. ~_t77 => box 1 ~_t42 [ Axiom 5 ] [ SNF++, 16118, ~_t42 ] % 47.56/47.68 (1,1) [6080,19]. true => ~_t77 | _t42 [ Axiom 5 ] % 47.56/47.68 (1,1) [6234,19]. true => ~_t44 | y1 [ Axiom T ] % 47.56/47.68 (1,1) [7206,19]. true => ~_t38 | ~z1 [ Axiom 5 ] % 47.56/47.68 (157,1) [7209,19]. _t39 => ~box 1~ _t40 [ Axiom 5 ] [ SNF++, 16236, _t40 ] % 47.56/47.68 (1,1) [7210,19]. true => _t39 | ~_t38 [ Axiom 5 ] % 47.56/47.68 (1,1) [7211,19]. true => ~_t43 | ~y1 [ Axiom 5 ] % 47.56/47.68 (1,1) [7214,19]. true => _t44 | ~_t43 [ Axiom 5 ] % 47.56/47.68 (1,1) [7215,19]. true => _t43 | _t38 | ~_t37 | p1 [ Axiom 5 ] % 47.56/47.68 (171,1) [8274,19]. true => ~_t46 | _t43 | _t38 | ~p1 [ Axiom 5 ] % 47.56/47.68 (1,1) [15913,19]. true => ~_t128 | _t37 [ SNF++, 7216 ] % 47.56/47.68 (1,1) [15943,19]. true => ~_t143 | _t46 [ SNF++, 9130 ] % 47.56/47.68 (1,1) [16118,19]. ~_t77 => box 1 _t123 [ SNF++, 6077 ] % 47.56/47.68 (157,1) [16236,19]. _t39 => ~box 1~ _t174 [ SNF++, 7209 ] % 47.56/47.68 (1,1) [18592,19]. true => ~_t42 | ~_t38 [ LRES, 7206, 6075, ~z1 ] % 47.56/47.68 (1,1) [18651,19]. true => ~_t44 | ~_t43 [ LRES, 7211, 6234, ~y1 ] % 47.56/47.68 (157,1) [64262,19]. true => _t77 | ~_t39 [ GEN1, 16118, 16236, 54638, _t123, _t174 ] % 47.56/47.68 (171,1) [122526,19]. true => ~_t46 | _t43 | _t38 | ~_t37 [ LRES, 8274, 7215, ~p1 ] % 47.56/47.68 (171,1) [129777,19]. true => ~_t128 | ~_t46 | _t43 | _t38 [ LRES, 122526, 15913, ~_t37 ] % 47.56/47.68 (171,1) [130149,19]. true => ~_t128 | ~_t46 | _t43 | _t39 [ LRES, 129777, 7210, _t38 ] % 47.56/47.68 (171,1) [130150,19]. true => ~_t128 | ~_t46 | _t43 | ~_t42 [ LRES, 129777, 18592, _t38 ] % 47.56/47.68 (171,1) [130369,19]. true => ~_t128 | _t77 | ~_t46 | _t43 [ LRES, 130149, 64262, _t39 ] [ Backward Subsumption, 299962 ] % 47.56/47.68 (171,1) [130387,19]. true => ~_t128 | ~_t77 | ~_t46 | _t43 [ LRES, 130150, 6080, ~_t42 ] [ Backward Subsumption, 307560 ] % 47.56/47.68 (171,1) [130396,19]. true => ~_t128 | ~_t77 | ~_t46 | _t44 [ LRES, 130387, 7214, _t43 ] [ Backward Subsumption, 307560 ] % 47.56/47.68 (171,1) [130397,19]. true => ~_t128 | ~_t77 | ~_t46 | ~_t44 [ LRES, 130387, 18651, _t43 ] [ Backward Subsumption, 307560 ] % 47.56/47.68 (171,1) [130435,19]. true => ~_t128 | _t77 | ~_t46 | _t44 [ LRES, 130369, 7214, _t43 ] [ Backward Subsumption, 299962 ] % 47.56/47.68 (171,1) [130436,19]. true => ~_t128 | _t77 | ~_t46 | ~_t44 [ LRES, 130369, 18651, _t43 ] [ Backward Subsumption, 299962 ] % 47.56/47.68 (171,1) [299962,19]. true => ~_t128 | _t77 | ~_t46 [ LRES, 130436, 130435, ~_t44 ] % 47.56/47.68 (171,1) [299968,19]. true => ~_t143 | ~_t128 | _t77 [ LRES, 299962, 15943, ~_t46 ] [ Backward Subsumption, 307661 ] % 47.56/47.68 (171,1) [307560,19]. true => ~_t128 | ~_t77 | ~_t46 [ LRES, 130397, 130396, ~_t44 ] % 47.56/47.68 (171,1) [307630,19]. true => ~_t143 | ~_t128 | ~_t77 [ LRES, 307560, 15943, ~_t46 ] [ Backward Subsumption, 307661 ] % 47.56/47.68 (171,1) [307661,19]. true => ~_t143 | ~_t128 [ LRES, 307630, 299968, ~_t77 ] % 47.56/47.68 (1,1) [6084,20]. ~_t77 => box 1 ~_t42 [ Axiom 5 ] [ SNF++, 16334, ~_t42 ] % 47.56/47.68 (1,1) [6087,20]. true => ~_t77 | _t42 [ Axiom 5 ] % 47.56/47.68 (156,1) [7208,20]. _t40 => ~box 1~ _t41 [ Axiom 5 ] [ SNF++, 16450, _t41 ] % 47.56/47.68 (1,1) [16119,20]. true => ~_t123 | ~_t42 [ SNF++, 6077 ] % 47.56/47.68 (157,1) [16237,20]. true => ~_t174 | _t40 [ SNF++, 7209 ] % 47.56/47.68 (1,1) [16334,20]. ~_t77 => box 1 _t123 [ SNF++, 6084 ] % 47.56/47.68 (156,1) [16450,20]. _t40 => ~box 1~ _t186 [ SNF++, 7208 ] % 47.56/47.68 (1,1) [18424,20]. true => ~_t123 | ~_t77 [ LRES, 16119, 6087, ~_t42 ] % 47.56/47.68 (156,1) [49547,20]. true => _t77 | ~_t40 [ GEN1, 16334, 16450, 32709, _t123, _t186 ] % 47.56/47.68 (157,1) [50345,20]. true => ~_t174 | _t77 [ LRES, 49547, 16237, ~_t40 ] % 47.86/47.99 (157,1) [54638,20]. true => ~_t174 | ~_t123 [ LRES, 50345, 18424, _t77 ] % 47.86/47.99 (1,1) [6091,21]. ~_t77 => box 1 ~_t42 [ Axiom 5 ] [ SNF++, 16508, ~_t42 ] % 47.86/47.99 (1,1) [6094,21]. true => ~_t77 | _t42 [ Axiom 5 ] % 47.86/47.99 (155,1) [7207,21]. _t41 => ~box 1~ _t42 [ Axiom 5 ] [ SNF++, 16568, _t42 ] % 47.86/47.99 (1,1) [16335,21]. true => ~_t123 | ~_t42 [ SNF++, 6084 ] % 47.86/47.99 (156,1) [16451,21]. true => ~_t186 | _t41 [ SNF++, 7208 ] % 47.86/47.99 (1,1) [16508,21]. ~_t77 => box 1 _t123 [ SNF++, 6091 ] % 47.86/47.99 (155,1) [16568,21]. _t41 => ~box 1~ _t172 [ SNF++, 7207 ] % 47.86/47.99 (155,1) [18021,21]. true => _t77 | ~_t41 [ GEN1, 16508, 16568, 17009, _t123, _t172 ] % 47.86/47.99 (1,1) [18426,21]. true => ~_t123 | ~_t77 [ LRES, 16335, 6094, ~_t42 ] % 47.86/47.99 (156,1) [29893,21]. true => ~_t186 | _t77 [ LRES, 18021, 16451, ~_t41 ] % 47.86/47.99 (156,1) [32709,21]. true => ~_t186 | ~_t123 [ LRES, 29893, 18426, _t77 ] % 47.86/47.99 (1,1) [16509,22]. true => ~_t123 | ~_t42 [ SNF++, 6091 ] % 47.86/47.99 (155,1) [16569,22]. true => ~_t172 | _t42 [ SNF++, 7207 ] % 47.86/47.99 (155,1) [17009,22]. true => ~_t172 | ~_t123 [ LRES, 16509, 16569, ~_t42 ] % 47.86/47.99 % SZS output end Refutation % 47.86/48.01 % KSP exiting %------------------------------------------------------------------------------