%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP078_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n010.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:57 PM UTC 2026 % Result : Theorem 0.88s 1.10s % Output : Refutation 0.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP078_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.15/0.33 % Computer : n010.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 17:18:06 EDT 2026 % 0.15/0.34 % CPUTime : % 0.37/0.60 ----KSP format--- % 0.37/0.60 set(box,SYM). % 0.37/0.60 usable(formulas). % 0.37/0.60 true. % 0.37/0.60 end_of_list. % 0.37/0.60 sos(formulas). % 0.37/0.60 ~ (<> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( [] ( p0 ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) | <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( ( [] ( <> ( p0 ) ) & [] ( ~ ( p0 ) | [] ( p3 ) ) ) | <> ( [] ( <> ( [] ( ~ ( p0 ) | [] ( p3 ) ) ) ) & [] ( <> ( p0 ) ) ) | ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) | [] ( p3 ) ) ) ) ) | <> ( <> ( [] ( <> ( p0 ) ) ) & p0 & <> ( ~ ( p0 ) | [] ( p3 ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) | <> ( p4 ) ). % 0.37/0.60 end_of_list. % 0.37/0.60 ----------------- % 0.37/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.ZydVv6hoTn/theBenchmark.ksp % 0.88/1.10 % 0.88/1.10 % SZS status Theorem % 0.88/1.10 % 0.88/1.10 ***************** % 0.88/1.10 FOUND PROOF 1 % 0.88/1.10 ***************** % 0.88/1.10 % SZS output start Refutation % 0.88/1.10 % 0.88/1.10 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.88/1.10 (1,1) [1579,0]. _t1 => box 1 _t2 [ SNF ] [ Backward Subsumption, 1885 ] % 0.88/1.10 (1,1) [1580,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 1884 ] % 0.88/1.10 (1245,1) [1872,0]. _t73 => ~box 1~ _t74 [ SNF ] [ Backward Subsumption, 1888 ] % 0.88/1.10 (1,1) [1873,0]. true => _t73 | ~_t0 [ SNF ] [ Backward Subsumption, 1879 ] % 0.88/1.10 (1,1) [1879,0]. true => _t73 [ Unit Resolution, 3, 1873, _t0 ] [ Modal Level Pure Literal Elimination, _t73 ] % 0.88/1.10 (1,1) [1884,0]. true => _t1 [ Unit Resolution, 3, 1580, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 0.88/1.10 (1,1) [1885,0]. true => box 1 _t2 [ LHS Unit Resolution, 1884, 1579, _t1 ] [ SNF++, 3671, _t2 ] % 0.88/1.10 (1245,1) [1888,0]. true => ~box 1~ _t74 [ LHS Unit Resolution, 1879, 1872, _t73 ] [ SNF++, 3697, _t74 ] % 0.88/1.10 (1,1) [3671,0]. true => box 1 _t238 [ SNF++, 1885 ] % 0.88/1.10 (1245,1) [3697,0]. true => ~box 1~ _t239 [ SNF++, 1888 ] % 0.88/1.10 (1245,1) [20173,0]. true => false [ GEN1, 3671, 3697, 20147, _t238, _t239 ] % 0.88/1.10 (1,1) [1569,1]. _t3 => box 1 _t4 [ SNF ] [ SNF++, 3575, _t4 ] % 0.88/1.10 (1,1) [1576,1]. true => _t3 | ~_t2 [ SNF ] % 0.88/1.10 (1243,1) [1870,1]. _t75 => ~box 1~ _t76 [ SNF ] [ SNF++, 3599, _t76 ] % 0.88/1.10 (1245,1) [1871,1]. true => _t75 | ~_t74 [ SNF ] % 0.88/1.10 (1,1) [3575,1]. _t3 => box 1 _t235 [ SNF++, 1569 ] % 0.88/1.10 (1243,1) [3599,1]. _t75 => ~box 1~ _t236 [ SNF++, 1870 ] % 0.88/1.10 (1,1) [3672,1]. true => ~_t238 | _t2 [ SNF++, 1885 ] % 0.88/1.10 (1245,1) [3698,1]. true => ~_t239 | _t74 [ SNF++, 1888 ] % 0.88/1.10 (1,1) [4782,1]. true => ~_t238 | _t3 [ LRES, 1576, 3672, ~_t2 ] % 0.88/1.10 (1245,1) [4803,1]. true => ~_t239 | _t75 [ LRES, 1871, 3698, ~_t74 ] % 0.88/1.10 (1243,1) [20109,1]. true => ~_t75 | ~_t3 [ GEN1, 3575, 3599, 20072, _t235, _t236 ] % 0.88/1.10 (1243,1) [20110,1]. true => ~_t238 | ~_t75 [ LRES, 20109, 4782, ~_t3 ] % 0.88/1.10 (1245,1) [20147,1]. true => ~_t239 | ~_t238 [ LRES, 20110, 4803, ~_t75 ] % 0.88/1.10 (1,1) [1553,2]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 3467, _t6 ] % 0.88/1.10 (1,1) [1566,2]. true => _t5 | ~_t4 [ SNF ] % 0.88/1.10 (1242,1) [1868,2]. _t77 => ~box 1~ _t78 [ SNF ] [ SNF++, 3493, _t78 ] % 0.88/1.10 (1243,1) [1869,2]. true => _t77 | ~_t76 [ SNF ] % 0.88/1.10 (1,1) [3467,2]. _t5 => box 1 _t232 [ SNF++, 1553 ] % 0.88/1.10 (1242,1) [3493,2]. _t77 => ~box 1~ _t233 [ SNF++, 1868 ] % 0.88/1.10 (1,1) [3576,2]. true => ~_t235 | _t4 [ SNF++, 1569 ] % 0.88/1.10 (1243,1) [3600,2]. true => ~_t236 | _t76 [ SNF++, 1870 ] % 0.88/1.10 (1,1) [4741,2]. true => ~_t235 | _t5 [ LRES, 1566, 3576, ~_t4 ] % 0.88/1.10 (1243,1) [4781,2]. true => ~_t236 | _t77 [ LRES, 1869, 3600, ~_t76 ] % 0.88/1.10 (1242,1) [20034,2]. true => ~_t77 | ~_t5 [ GEN1, 3467, 3493, 19998, _t232, _t233 ] % 0.88/1.10 (1242,1) [20035,2]. true => ~_t235 | ~_t77 [ LRES, 20034, 4741, ~_t5 ] % 0.88/1.10 (1243,1) [20072,2]. true => ~_t236 | ~_t235 [ LRES, 20035, 4781, ~_t77 ] % 0.88/1.10 (1,1) [1531,3]. _t7 => box 1 _t8 [ SNF ] [ SNF++, 3363, _t8 ] % 0.88/1.10 (1,1) [1550,3]. true => _t7 | ~_t6 [ SNF ] % 0.88/1.10 (1241,1) [1866,3]. _t79 => ~box 1~ _t80 [ SNF ] [ SNF++, 3387, _t80 ] % 0.88/1.10 (1242,1) [1867,3]. true => _t79 | ~_t78 [ SNF ] % 0.88/1.10 (1,1) [3363,3]. _t7 => box 1 _t229 [ SNF++, 1531 ] % 0.88/1.10 (1241,1) [3387,3]. _t79 => ~box 1~ _t230 [ SNF++, 1866 ] % 0.88/1.10 (1,1) [3468,3]. true => ~_t232 | _t6 [ SNF++, 1553 ] % 0.88/1.10 (1242,1) [3494,3]. true => ~_t233 | _t78 [ SNF++, 1868 ] % 0.88/1.10 (1,1) [4767,3]. true => ~_t232 | _t7 [ LRES, 1550, 3468, ~_t6 ] % 0.88/1.10 (1242,1) [4793,3]. true => ~_t233 | _t79 [ LRES, 1867, 3494, ~_t78 ] % 0.88/1.10 (1241,1) [19959,3]. true => ~_t79 | ~_t7 [ GEN1, 3363, 3387, 19925, _t229, _t230 ] % 0.88/1.10 (1241,1) [19960,3]. true => ~_t232 | ~_t79 [ LRES, 19959, 4767, ~_t7 ] % 0.88/1.10 (1242,1) [19998,3]. true => ~_t233 | ~_t232 [ LRES, 19960, 4793, ~_t79 ] % 0.88/1.10 (1,1) [1503,4]. _t9 => box 1 _t10 [ SNF ] [ SNF++, 3259, _t10 ] % 0.88/1.10 (1,1) [1528,4]. true => _t9 | ~_t8 [ SNF ] % 0.88/1.10 (1240,1) [1864,4]. _t81 => ~box 1~ _t82 [ SNF ] [ SNF++, 3285, _t82 ] % 0.88/1.10 (1241,1) [1865,4]. true => _t81 | ~_t80 [ SNF ] % 0.88/1.10 (1,1) [3259,4]. _t9 => box 1 _t226 [ SNF++, 1503 ] % 0.88/1.10 (1240,1) [3285,4]. _t81 => ~box 1~ _t227 [ SNF++, 1864 ] % 0.88/1.10 (1,1) [3364,4]. true => ~_t229 | _t8 [ SNF++, 1531 ] % 0.88/1.10 (1241,1) [3388,4]. true => ~_t230 | _t80 [ SNF++, 1866 ] % 0.88/1.10 (1,1) [4674,4]. true => ~_t229 | _t9 [ LRES, 1528, 3364, ~_t8 ] % 0.88/1.10 (1241,1) [4714,4]. true => ~_t230 | _t81 [ LRES, 1865, 3388, ~_t80 ] % 0.88/1.10 (1240,1) [19888,4]. true => ~_t81 | ~_t9 [ GEN1, 3259, 3285, 19849, _t226, _t227 ] % 0.88/1.10 (1240,1) [19889,4]. true => ~_t229 | ~_t81 [ LRES, 19888, 4674, ~_t9 ] % 0.88/1.10 (1241,1) [19925,4]. true => ~_t230 | ~_t229 [ LRES, 19889, 4714, ~_t81 ] % 0.88/1.10 (1,1) [1469,5]. _t11 => box 1 _t12 [ SNF ] [ SNF++, 3159, _t12 ] % 0.88/1.10 (1,1) [1500,5]. true => _t11 | ~_t10 [ SNF ] % 0.88/1.10 (1239,1) [1862,5]. _t83 => ~box 1~ _t84 [ SNF ] [ SNF++, 3183, _t84 ] % 0.88/1.10 (1240,1) [1863,5]. true => _t83 | ~_t82 [ SNF ] % 0.88/1.10 (1,1) [3159,5]. _t11 => box 1 _t223 [ SNF++, 1469 ] % 0.88/1.10 (1239,1) [3183,5]. _t83 => ~box 1~ _t224 [ SNF++, 1862 ] % 0.88/1.10 (1,1) [3260,5]. true => ~_t226 | _t10 [ SNF++, 1503 ] % 0.88/1.10 (1240,1) [3286,5]. true => ~_t227 | _t82 [ SNF++, 1864 ] % 0.88/1.10 (1,1) [4699,5]. true => ~_t226 | _t11 [ LRES, 1500, 3260, ~_t10 ] % 0.88/1.10 (1240,1) [4739,5]. true => ~_t227 | _t83 [ LRES, 1863, 3286, ~_t82 ] % 0.88/1.10 (1239,1) [19801,5]. true => ~_t83 | ~_t11 [ GEN1, 3159, 3183, 19752, _t223, _t224 ] % 0.88/1.10 (1239,1) [19802,5]. true => ~_t226 | ~_t83 [ LRES, 19801, 4699, ~_t11 ] % 0.88/1.10 (1240,1) [19849,5]. true => ~_t227 | ~_t226 [ LRES, 19802, 4739, ~_t83 ] % 0.88/1.10 (1,1) [1429,6]. _t13 => box 1 _t14 [ SNF ] [ SNF++, 3059, _t14 ] % 0.88/1.10 (1,1) [1466,6]. true => _t13 | ~_t12 [ SNF ] % 0.88/1.10 (1238,1) [1860,6]. _t85 => ~box 1~ _t86 [ SNF ] [ SNF++, 3085, _t86 ] % 0.88/1.10 (1239,1) [1861,6]. true => _t85 | ~_t84 [ SNF ] % 0.88/1.10 (1,1) [3059,6]. _t13 => box 1 _t220 [ SNF++, 1429 ] % 0.88/1.10 (1238,1) [3085,6]. _t85 => ~box 1~ _t221 [ SNF++, 1860 ] % 0.88/1.10 (1,1) [3160,6]. true => ~_t223 | _t12 [ SNF++, 1469 ] % 0.88/1.10 (1239,1) [3184,6]. true => ~_t224 | _t84 [ SNF++, 1862 ] % 0.88/1.10 (1,1) [4603,6]. true => ~_t223 | _t13 [ LRES, 1466, 3160, ~_t12 ] % 0.88/1.10 (1239,1) [4652,6]. true => ~_t224 | _t85 [ LRES, 1861, 3184, ~_t84 ] % 0.88/1.10 (1238,1) [19710,6]. true => ~_t85 | ~_t13 [ GEN1, 3059, 3085, 19683, _t220, _t221 ] % 0.88/1.10 (1238,1) [19711,6]. true => ~_t223 | ~_t85 [ LRES, 19710, 4603, ~_t13 ] % 0.88/1.10 (1239,1) [19752,6]. true => ~_t224 | ~_t223 [ LRES, 19711, 4652, ~_t85 ] % 0.88/1.10 (1,1) [1383,7]. _t15 => box 1 _t16 [ SNF ] [ SNF++, 2963, _t16 ] % 0.88/1.10 (1,1) [1426,7]. true => _t15 | ~_t14 [ SNF ] % 0.88/1.10 (1237,1) [1858,7]. _t87 => ~box 1~ _t88 [ SNF ] [ SNF++, 2987, _t88 ] % 0.88/1.10 (1238,1) [1859,7]. true => _t87 | ~_t86 [ SNF ] % 0.88/1.10 (1,1) [2963,7]. _t15 => box 1 _t217 [ SNF++, 1383 ] % 0.88/1.10 (1237,1) [2987,7]. _t87 => ~box 1~ _t218 [ SNF++, 1858 ] % 0.88/1.10 (1,1) [3060,7]. true => ~_t220 | _t14 [ SNF++, 1429 ] % 0.88/1.10 (1238,1) [3086,7]. true => ~_t221 | _t86 [ SNF++, 1860 ] % 0.88/1.10 (1,1) [4628,7]. true => ~_t220 | _t15 [ LRES, 1426, 3060, ~_t14 ] % 0.88/1.10 (1238,1) [4672,7]. true => ~_t221 | _t87 [ LRES, 1859, 3086, ~_t86 ] % 0.88/1.10 (1237,1) [19642,7]. true => ~_t87 | ~_t15 [ GEN1, 2963, 2987, 19601, _t217, _t218 ] % 0.88/1.10 (1237,1) [19643,7]. true => ~_t220 | ~_t87 [ LRES, 19642, 4628, ~_t15 ] % 0.88/1.10 (1238,1) [19683,7]. true => ~_t221 | ~_t220 [ LRES, 19643, 4672, ~_t87 ] % 0.88/1.10 (1,1) [1331,8]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 2867, _t18 ] % 0.88/1.10 (1,1) [1380,8]. true => _t17 | ~_t16 [ SNF ] % 0.88/1.10 (1236,1) [1856,8]. _t89 => ~box 1~ _t90 [ SNF ] [ SNF++, 2893, _t90 ] % 0.88/1.10 (1237,1) [1857,8]. true => _t89 | ~_t88 [ SNF ] % 0.88/1.10 (1,1) [2867,8]. _t17 => box 1 _t214 [ SNF++, 1331 ] % 0.88/1.10 (1236,1) [2893,8]. _t89 => ~box 1~ _t215 [ SNF++, 1856 ] % 0.88/1.10 (1,1) [2964,8]. true => ~_t217 | _t16 [ SNF++, 1383 ] % 0.88/1.10 (1237,1) [2988,8]. true => ~_t218 | _t88 [ SNF++, 1858 ] % 0.88/1.10 (1,1) [4530,8]. true => ~_t217 | _t17 [ LRES, 1380, 2964, ~_t16 ] % 0.88/1.10 (1237,1) [4577,8]. true => ~_t218 | _t89 [ LRES, 1857, 2988, ~_t88 ] % 0.88/1.10 (1236,1) [19566,8]. true => ~_t89 | ~_t17 [ GEN1, 2867, 2893, 19498, _t214, _t215 ] % 0.88/1.10 (1236,1) [19567,8]. true => ~_t217 | ~_t89 [ LRES, 19566, 4530, ~_t17 ] % 0.88/1.10 (1237,1) [19601,8]. true => ~_t218 | ~_t217 [ LRES, 19567, 4577, ~_t89 ] % 0.88/1.10 (1,1) [1256,9]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 2775, _t20 ] % 0.88/1.10 (1,1) [1328,9]. true => _t19 | ~_t18 [ SNF ] % 0.88/1.10 (1235,1) [1854,9]. _t91 => ~box 1~ _t92 [ SNF ] [ SNF++, 2799, _t92 ] % 0.88/1.10 (1236,1) [1855,9]. true => _t91 | ~_t90 [ SNF ] % 0.88/1.10 (1,1) [2775,9]. _t19 => box 1 _t211 [ SNF++, 1256 ] % 0.88/1.10 (1235,1) [2799,9]. _t91 => ~box 1~ _t212 [ SNF++, 1854 ] % 0.88/1.10 (1,1) [2868,9]. true => ~_t214 | _t18 [ SNF++, 1331 ] % 0.88/1.10 (1236,1) [2894,9]. true => ~_t215 | _t90 [ SNF++, 1856 ] % 0.88/1.10 (1,1) [4550,9]. true => ~_t214 | _t19 [ LRES, 1328, 2868, ~_t18 ] % 0.88/1.10 (1236,1) [4601,9]. true => ~_t215 | _t91 [ LRES, 1855, 2894, ~_t90 ] % 0.88/1.10 (1235,1) [19429,9]. true => ~_t91 | ~_t19 [ GEN1, 2775, 2799, 19367, _t211, _t212 ] % 0.88/1.10 (1235,1) [19430,9]. true => ~_t214 | ~_t91 [ LRES, 19429, 4550, ~_t19 ] % 0.88/1.10 (1236,1) [19498,9]. true => ~_t215 | ~_t214 [ LRES, 19430, 4601, ~_t91 ] % 0.88/1.10 (1,1) [1126,10]. _t21 => box 1 _t22 [ SNF ] [ SNF++, 2683, _t22 ] % 0.88/1.10 (1,1) [1253,10]. true => _t21 | ~_t20 [ SNF ] % 0.88/1.10 (1234,1) [1852,10]. _t93 => ~box 1~ _t94 [ SNF ] [ SNF++, 2709, _t94 ] % 0.88/1.10 (1235,1) [1853,10]. true => _t93 | ~_t92 [ SNF ] % 0.88/1.10 (1,1) [2683,10]. _t21 => box 1 _t208 [ SNF++, 1126 ] % 0.88/1.10 (1234,1) [2709,10]. _t93 => ~box 1~ _t209 [ SNF++, 1852 ] % 0.88/1.10 (1,1) [2776,10]. true => ~_t211 | _t20 [ SNF++, 1256 ] % 0.88/1.10 (1235,1) [2800,10]. true => ~_t212 | _t92 [ SNF++, 1854 ] % 0.88/1.10 (1,1) [4449,10]. true => ~_t211 | _t21 [ LRES, 1253, 2776, ~_t20 ] % 0.88/1.10 (1235,1) [4498,10]. true => ~_t212 | _t93 [ LRES, 1853, 2800, ~_t92 ] % 0.88/1.10 (1234,1) [19307,10]. true => ~_t93 | ~_t21 [ GEN1, 2683, 2709, 19263, _t208, _t209 ] % 0.88/1.10 (1234,1) [19308,10]. true => ~_t211 | ~_t93 [ LRES, 19307, 4449, ~_t21 ] % 0.88/1.10 (1235,1) [19367,10]. true => ~_t212 | ~_t211 [ LRES, 19308, 4498, ~_t93 ] % 0.88/1.10 (1,1) [980,11]. _t23 => box 1 _t24 [ SNF ] [ SNF++, 2595, _t24 ] % 0.88/1.10 (1,1) [1123,11]. true => _t23 | ~_t22 [ SNF ] % 0.88/1.10 (1233,1) [1850,11]. _t95 => ~box 1~ _t96 [ SNF ] [ SNF++, 2619, _t96 ] % 0.88/1.10 (1234,1) [1851,11]. true => _t95 | ~_t94 [ SNF ] % 0.88/1.10 (1,1) [2595,11]. _t23 => box 1 _t205 [ SNF++, 980 ] % 0.88/1.10 (1233,1) [2619,11]. _t95 => ~box 1~ _t206 [ SNF++, 1850 ] % 0.88/1.10 (1,1) [2684,11]. true => ~_t208 | _t22 [ SNF++, 1126 ] % 0.88/1.10 (1234,1) [2710,11]. true => ~_t209 | _t94 [ SNF++, 1852 ] % 0.88/1.10 (1,1) [4473,11]. true => ~_t208 | _t23 [ LRES, 1123, 2684, ~_t22 ] % 0.88/1.10 (1234,1) [4528,11]. true => ~_t209 | _t95 [ LRES, 1851, 2710, ~_t94 ] % 0.88/1.10 (1233,1) [19222,11]. true => ~_t95 | ~_t23 [ GEN1, 2595, 2619, 19194, _t205, _t206 ] % 0.88/1.10 (1233,1) [19223,11]. true => ~_t208 | ~_t95 [ LRES, 19222, 4473, ~_t23 ] % 0.88/1.10 (1234,1) [19263,11]. true => ~_t209 | ~_t208 [ LRES, 19223, 4528, ~_t95 ] % 0.88/1.10 (1,1) [840,12]. _t25 => box 1 _t26 [ SNF ] [ SNF++, 2507, _t26 ] % 0.88/1.10 (1,1) [977,12]. true => _t25 | ~_t24 [ SNF ] % 0.88/1.10 (1232,1) [1848,12]. _t97 => ~box 1~ _t98 [ SNF ] [ SNF++, 2533, _t98 ] % 0.88/1.10 (1233,1) [1849,12]. true => _t97 | ~_t96 [ SNF ] % 0.88/1.10 (1,1) [2507,12]. _t25 => box 1 _t202 [ SNF++, 840 ] % 0.88/1.10 (1232,1) [2533,12]. _t97 => ~box 1~ _t203 [ SNF++, 1848 ] % 0.88/1.10 (1,1) [2596,12]. true => ~_t205 | _t24 [ SNF++, 980 ] % 0.88/1.10 (1233,1) [2620,12]. true => ~_t206 | _t96 [ SNF++, 1850 ] % 0.88/1.10 (1,1) [4345,12]. true => ~_t205 | _t25 [ LRES, 977, 2596, ~_t24 ] % 0.88/1.10 (1233,1) [4414,12]. true => ~_t206 | _t97 [ LRES, 1849, 2620, ~_t96 ] % 0.88/1.10 (1232,1) [19147,12]. true => ~_t97 | ~_t25 [ GEN1, 2507, 2533, 19108, _t202, _t203 ] % 0.88/1.10 (1232,1) [19148,12]. true => ~_t205 | ~_t97 [ LRES, 19147, 4345, ~_t25 ] % 0.88/1.10 (1233,1) [19194,12]. true => ~_t206 | ~_t205 [ LRES, 19148, 4414, ~_t97 ] % 0.88/1.10 (1,1) [706,13]. _t27 => box 1 _t28 [ SNF ] [ SNF++, 2423, _t28 ] % 0.88/1.10 (1,1) [837,13]. true => _t27 | ~_t26 [ SNF ] % 0.88/1.10 (1231,1) [1846,13]. _t99 => ~box 1~ _t100 [ SNF ] [ SNF++, 2447, _t100 ] % 0.88/1.10 (1232,1) [1847,13]. true => _t99 | ~_t98 [ SNF ] % 0.88/1.10 (1,1) [2423,13]. _t27 => box 1 _t199 [ SNF++, 706 ] % 0.88/1.10 (1231,1) [2447,13]. _t99 => ~box 1~ _t200 [ SNF++, 1846 ] % 0.88/1.10 (1,1) [2508,13]. true => ~_t202 | _t26 [ SNF++, 840 ] % 0.88/1.10 (1232,1) [2534,13]. true => ~_t203 | _t98 [ SNF++, 1848 ] % 0.88/1.10 (1,1) [4375,13]. true => ~_t202 | _t27 [ LRES, 837, 2508, ~_t26 ] % 0.88/1.10 (1232,1) [4447,13]. true => ~_t203 | _t99 [ LRES, 1847, 2534, ~_t98 ] % 0.88/1.10 (1231,1) [19076,13]. true => ~_t99 | ~_t27 [ GEN1, 2423, 2447, 19036, _t199, _t200 ] % 0.88/1.10 (1231,1) [19077,13]. true => ~_t202 | ~_t99 [ LRES, 19076, 4375, ~_t27 ] % 0.88/1.10 (1232,1) [19108,13]. true => ~_t203 | ~_t202 [ LRES, 19077, 4447, ~_t99 ] % 0.88/1.10 (1,1) [578,14]. _t29 => box 1 _t30 [ SNF ] [ SNF++, 2339, _t30 ] % 0.88/1.10 (1,1) [703,14]. true => _t29 | ~_t28 [ SNF ] % 0.88/1.10 (1230,1) [1844,14]. _t101 => ~box 1~ _t102 [ SNF ] [ SNF++, 2365, _t102 ] % 0.88/1.10 (1231,1) [1845,14]. true => _t101 | ~_t100 [ SNF ] % 0.88/1.10 (1,1) [2339,14]. _t29 => box 1 _t196 [ SNF++, 578 ] % 0.88/1.10 (1230,1) [2365,14]. _t101 => ~box 1~ _t197 [ SNF++, 1844 ] % 0.88/1.10 (1,1) [2424,14]. true => ~_t199 | _t28 [ SNF++, 706 ] % 0.88/1.10 (1231,1) [2448,14]. true => ~_t200 | _t100 [ SNF++, 1846 ] % 0.88/1.10 (1,1) [4229,14]. true => ~_t199 | _t29 [ LRES, 703, 2424, ~_t28 ] % 0.88/1.10 (1231,1) [4306,14]. true => ~_t200 | _t101 [ LRES, 1845, 2448, ~_t100 ] % 0.88/1.10 (1230,1) [19002,14]. true => ~_t101 | ~_t29 [ GEN1, 2339, 2365, 18970, _t196, _t197 ] % 0.88/1.10 (1230,1) [19003,14]. true => ~_t199 | ~_t101 [ LRES, 19002, 4229, ~_t29 ] % 0.88/1.10 (1231,1) [19036,14]. true => ~_t200 | ~_t199 [ LRES, 19003, 4306, ~_t101 ] % 0.88/1.10 (1,1) [456,15]. _t31 => box 1 _t32 [ SNF ] [ SNF++, 2259, _t32 ] % 0.88/1.10 (1,1) [575,15]. true => _t31 | ~_t30 [ SNF ] % 0.88/1.10 (1229,1) [1842,15]. _t103 => ~box 1~ _t104 [ SNF ] [ SNF++, 2283, _t104 ] % 0.88/1.10 (1230,1) [1843,15]. true => _t103 | ~_t102 [ SNF ] % 0.88/1.10 (1,1) [2259,15]. _t31 => box 1 _t193 [ SNF++, 456 ] % 0.88/1.10 (1229,1) [2283,15]. _t103 => ~box 1~ _t194 [ SNF++, 1842 ] % 0.88/1.10 (1,1) [2340,15]. true => ~_t196 | _t30 [ SNF++, 578 ] % 0.88/1.10 (1230,1) [2366,15]. true => ~_t197 | _t102 [ SNF++, 1844 ] % 0.88/1.10 (1,1) [4266,15]. true => ~_t196 | _t31 [ LRES, 575, 2340, ~_t30 ] % 0.88/1.10 (1230,1) [4343,15]. true => ~_t197 | _t103 [ LRES, 1843, 2366, ~_t102 ] % 0.88/1.10 (1229,1) [18940,15]. true => ~_t103 | ~_t31 [ GEN1, 2259, 2283, 18911, _t193, _t194 ] % 0.88/1.10 (1229,1) [18941,15]. true => ~_t196 | ~_t103 [ LRES, 18940, 4266, ~_t31 ] % 0.88/1.10 (1230,1) [18970,15]. true => ~_t197 | ~_t196 [ LRES, 18941, 4343, ~_t103 ] % 0.88/1.10 (1,1) [340,16]. _t33 => box 1 _t34 [ SNF ] [ SNF++, 2179, _t34 ] % 0.88/1.10 (1,1) [453,16]. true => _t33 | ~_t32 [ SNF ] % 0.88/1.10 (1228,1) [1840,16]. _t105 => ~box 1~ _t106 [ SNF ] [ SNF++, 2205, _t106 ] % 0.88/1.10 (1229,1) [1841,16]. true => _t105 | ~_t104 [ SNF ] % 0.88/1.10 (1,1) [2179,16]. _t33 => box 1 _t190 [ SNF++, 340 ] % 0.88/1.10 (1228,1) [2205,16]. _t105 => ~box 1~ _t191 [ SNF++, 1840 ] % 0.88/1.10 (1,1) [2260,16]. true => ~_t193 | _t32 [ SNF++, 456 ] % 0.88/1.10 (1229,1) [2284,16]. true => ~_t194 | _t104 [ SNF++, 1842 ] % 0.88/1.10 (1,1) [4129,16]. true => ~_t193 | _t33 [ LRES, 453, 2260, ~_t32 ] % 0.88/1.10 (1229,1) [4195,16]. true => ~_t194 | _t105 [ LRES, 1841, 2284, ~_t104 ] % 0.88/1.10 (1228,1) [18874,16]. true => ~_t105 | ~_t33 [ GEN1, 2179, 2205, 18847, _t190, _t191 ] % 0.88/1.10 (1228,1) [18875,16]. true => ~_t193 | ~_t105 [ LRES, 18874, 4129, ~_t33 ] % 0.88/1.10 (1229,1) [18911,16]. true => ~_t194 | ~_t193 [ LRES, 18875, 4195, ~_t105 ] % 0.88/1.10 (1,1) [202,17]. _t35 => box 1 _t36 [ SNF ] [ SNF++, 2089, _t36 ] % 0.88/1.10 (1,1) [283,17]. true => _t35 | ~_t34 [ SNF ] % 0.88/1.10 (1220,1) [1816,17]. _t70 => ~box 1~ _t71 [ SNF ] [ SNF++, 2125, _t71 ] % 0.88/1.10 (1228,1) [1817,17]. true => ~_t106 | _t70 [ SNF ] % 0.88/1.10 (1,1) [2089,17]. _t35 => box 1 _t186 [ SNF++, 202 ] % 0.88/1.10 (1220,1) [2125,17]. _t70 => ~box 1~ _t182 [ SNF++, 1816 ] % 0.88/1.10 (1,1) [2180,17]. true => ~_t190 | _t34 [ SNF++, 340 ] % 0.88/1.10 (1228,1) [2206,17]. true => ~_t191 | _t106 [ SNF++, 1840 ] % 0.88/1.10 (1,1) [4162,17]. true => ~_t190 | _t35 [ LRES, 283, 2180, ~_t34 ] % 0.88/1.10 (1220,1) [18758,17]. true => ~_t70 | ~_t35 [ GEN1, 2089, 2125, 18724, _t186, _t182 ] % 0.88/1.10 (1220,1) [18772,17]. true => ~_t190 | ~_t70 [ LRES, 18758, 4162, ~_t35 ] % 0.88/1.10 (1228,1) [18810,17]. true => ~_t190 | ~_t106 [ LRES, 18772, 1817, ~_t70 ] % 0.88/1.10 (1228,1) [18847,17]. true => ~_t191 | ~_t190 [ LRES, 18810, 2206, ~_t106 ] % 0.88/1.10 (1,1) [172,18]. _t61 => box 1 ~p1 [ SNF ] [ SNF++, 2009, ~p1 ] % 0.88/1.10 (1,1) [183,18]. _t126 => box 1 ~_t64 [ Axiom SYM ] [ SNF++, 2011, ~_t64 ] % 0.88/1.10 (1,1) [184,18]. _t65 => box 1 p1 [ SNF ] [ SNF++, 2013, p1 ] % 0.88/1.10 (1,1) [187,18]. true => _t126 | _t65 [ Axiom SYM ] % 0.88/1.10 (1,1) [190,18]. _t62 => box 1 _t63 [ SNF ] [ SNF++, 2015, _t63 ] % 0.88/1.10 (1,1) [201,18]. true => _t62 | ~_t36 [ SNF ] % 0.88/1.10 (1,1) [320,18]. _t64 => box 1 _t65 [ SNF ] [ SNF++, 2025, _t65 ] % 0.88/1.10 (40,1) [326,18]. _t66 => ~box 1~ ~p1 [ SNF ] [ SNF++, 2045, ~p1 ] % 0.88/1.10 (1220,1) [1813,18]. true => ~_t71 | _t66 [ SNF ] % 0.88/1.10 (1219,1) [1814,18]. _t72 => ~box 1~ _t65 [ SNF ] [ SNF++, 2047, _t65 ] % 0.88/1.10 (1220,1) [1815,18]. true => _t72 | ~_t71 [ SNF ] % 0.88/1.10 (1,1) [2011,18]. _t126 => box 1 _t176 [ SNF++, 183 ] % 0.88/1.10 (1,1) [2013,18]. _t65 => box 1 _t157 [ SNF++, 184 ] % 0.88/1.10 (1,1) [2015,18]. _t62 => box 1 _t177 [ SNF++, 190 ] % 0.88/1.10 (40,1) [2045,18]. _t66 => ~box 1~ _t156 [ SNF++, 326 ] % 0.88/1.10 (1219,1) [2047,18]. _t72 => ~box 1~ _t167 [ SNF++, 1814 ] % 0.88/1.11 (1,1) [2090,18]. true => ~_t186 | _t36 [ SNF++, 202 ] % 0.88/1.11 (1220,1) [2126,18]. true => ~_t182 | _t71 [ SNF++, 1816 ] % 0.88/1.11 (1,1) [3848,18]. true => ~_t186 | _t62 [ LRES, 201, 2090, ~_t36 ] % 0.88/1.11 (1220,1) [4049,18]. true => ~_t182 | _t72 [ LRES, 1815, 2126, ~_t71 ] % 0.88/1.11 (40,1) [4693,18]. true => ~_t66 | ~_t65 [ GEN1, 2013, 2045, 3928, _t157, _t156 ] % 0.88/1.11 (40,1) [5255,18]. true => _t126 | ~_t66 [ LRES, 4693, 187, ~_t65 ] % 0.88/1.11 (1220,1) [5350,18]. true => _t126 | ~_t71 [ LRES, 5255, 1813, ~_t66 ] % 0.88/1.11 (1220,1) [5791,18]. true => ~_t182 | _t126 [ LRES, 5350, 2126, ~_t71 ] % 0.88/1.11 (1219,1) [11692,18]. true => ~_t126 | ~_t72 | ~_t62 [ GEN1, 2015, 2011, 2047, 11163, _t177, _t176, _t167 ] % 0.88/1.11 (1219,1) [15597,18]. true => ~_t186 | ~_t126 | ~_t72 [ LRES, 11692, 3848, ~_t62 ] % 0.88/1.11 (1220,1) [17758,18]. true => ~_t186 | ~_t182 | ~_t126 [ LRES, 15597, 4049, ~_t72 ] [ Backward Subsumption, 18724 ] % 0.88/1.11 (1220,1) [18724,18]. true => ~_t186 | ~_t182 [ LRES, 17758, 5791, ~_t126 ] % 0.88/1.11 (34,1) [188,19]. _t66 => ~box 1~ ~p1 [ SNF ] [ SNF++, 1979, ~p1 ] % 0.88/1.11 (1,1) [189,19]. true => _t66 | _t64 | ~_t63 [ SNF ] % 0.88/1.11 (1,1) [296,19]. _t61 => box 1 ~p1 [ SNF ] [ SNF++, 1963, ~p1 ] % 0.88/1.11 (1,1) [317,19]. _t65 => box 1 p1 [ SNF ] [ SNF++, 1965, p1 ] % 0.88/1.11 (1,1) [1965,19]. _t65 => box 1 _t157 [ SNF++, 317 ] % 0.88/1.11 (34,1) [1979,19]. _t66 => ~box 1~ _t156 [ SNF++, 188 ] % 0.88/1.11 (1,1) [2010,19]. true => ~_t156 | ~p1 [ SNF++, 172 ] % 0.88/1.11 (1,1) [2012,19]. true => ~_t176 | ~_t64 [ SNF++, 183 ] % 0.88/1.11 (1,1) [2014,19]. true => ~_t157 | p1 [ SNF++, 184 ] % 0.88/1.11 (1,1) [2016,19]. true => ~_t177 | _t63 [ SNF++, 190 ] % 0.88/1.11 (1,1) [2026,19]. true => ~_t167 | _t65 [ SNF++, 320 ] % 0.88/1.11 (1,1) [3928,19]. true => ~_t157 | ~_t156 [ LRES, 2010, 2014, ~p1 ] % 0.88/1.11 (34,1) [4621,19]. true => ~_t66 | ~_t65 [ GEN1, 1965, 1979, 4125, _t157, _t156 ] % 0.88/1.11 (34,1) [5160,19]. true => ~_t167 | ~_t66 [ LRES, 4621, 2026, ~_t65 ] % 0.88/1.11 (1,1) [6032,19]. true => ~_t177 | _t66 | _t64 [ LRES, 189, 2016, ~_t63 ] % 0.88/1.11 (1,1) [9862,19]. true => ~_t177 | ~_t176 | _t66 [ LRES, 6032, 2012, _t64 ] % 0.88/1.11 (34,1) [11163,19]. true => ~_t177 | ~_t176 | ~_t167 [ LRES, 9862, 5160, _t66 ] % 0.88/1.11 (1,1) [1964,20]. true => ~_t156 | ~p1 [ SNF++, 296 ] % 0.88/1.11 (1,1) [1966,20]. true => ~_t157 | p1 [ SNF++, 317 ] % 0.88/1.11 (1,1) [4125,20]. true => ~_t157 | ~_t156 [ LRES, 1964, 1966, ~p1 ] % 0.88/1.11 % SZS output end Refutation % 0.88/1.11 % KSP exiting %------------------------------------------------------------------------------