%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP115_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n018.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:13:00 PM UTC 2026 % Result : Theorem 0.45s 0.75s % Output : Refutation 0.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP115_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.17/0.33 % Computer : n018.cluster.edu % 0.17/0.33 % Model : x86_64 x86_64 % 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.33 % Memory : 8042.1875MB % 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.33 % CPULimit : 300 % 0.17/0.33 % WCLimit : 300 % 0.17/0.33 % DateTime : Mon May 4 17:50:01 EDT 2026 % 0.17/0.33 % CPUTime : % 0.40/0.57 ----KSP format--- % 0.40/0.57 set(box,REF). % 0.40/0.57 usable(formulas). % 0.40/0.57 true. % 0.40/0.57 end_of_list. % 0.40/0.57 sos(formulas). % 0.40/0.57 ~ (<> ( ~ ( ( [] ( ~ ( 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 ) ) ) ) | <> ( ( [] ( <> ( p0 ) ) & [] ( ~ ( p0 ) | [] ( p3 ) ) ) | <> ( [] ( <> ( [] ( ~ ( p0 ) | [] ( p3 ) ) ) ) & [] ( <> ( p0 ) ) ) | ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) | [] ( p3 ) ) ) ) ) | <> ( <> ( [] ( <> ( p0 ) ) ) & p0 & <> ( ~ ( p0 ) | [] ( p3 ) ) ) | <> ( [] ( ~ ( p0 ) | [] ( p3 ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) | <> ( p4 ) ). % 0.40/0.57 end_of_list. % 0.40/0.57 ----------------- % 0.40/0.57 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.2t4CcISV6E/theBenchmark.ksp % 0.45/0.75 % 0.45/0.75 % SZS status Theorem % 0.45/0.75 % 0.45/0.75 ***************** % 0.45/0.75 FOUND PROOF 1 % 0.45/0.75 ***************** % 0.45/0.75 % SZS output start Refutation % 0.45/0.75 % 0.45/0.75 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.45/0.75 (1,1) [743,0]. _t1 => box 1 _t2 [ SNF ] [ Backward Subsumption, 988 ] % 0.45/0.75 (1,1) [838,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 986 ] % 0.45/0.75 (449,1) [978,0]. _t55 => ~box 1~ _t56 [ SNF ] [ Backward Subsumption, 992 ] % 0.45/0.75 (1,1) [979,0]. true => _t55 | ~_t0 [ SNF ] [ Backward Subsumption, 981 ] % 0.45/0.75 (1,1) [981,0]. true => _t55 [ Unit Resolution, 3, 979, _t0 ] [ Modal Level Pure Literal Elimination, _t55 ] % 0.45/0.75 (1,1) [986,0]. true => _t1 [ Unit Resolution, 3, 838, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 0.45/0.75 (1,1) [988,0]. true => box 1 _t2 [ LHS Unit Resolution, 986, 743, _t1 ] [ SNF++, 1663, _t2 ] % 0.45/0.75 (449,1) [992,0]. true => ~box 1~ _t56 [ LHS Unit Resolution, 981, 978, _t55 ] [ SNF++, 1727, _t56 ] % 0.45/0.75 (1,1) [1663,0]. true => box 1 _t114 [ SNF++, 988 ] % 0.45/0.75 (449,1) [1727,0]. true => ~box 1~ _t115 [ SNF++, 992 ] % 0.45/0.75 (449,1) [7760,0]. true => false [ GEN1, 1663, 1727, 7364, _t114, _t115 ] % 0.45/0.75 (1,1) [650,1]. _t3 => box 1 _t4 [ SNF ] [ SNF++, 1595, _t4 ] % 0.45/0.75 (1,1) [740,1]. true => _t3 | ~_t2 [ SNF ] % 0.45/0.75 (447,1) [976,1]. _t57 => ~box 1~ _t58 [ SNF ] [ SNF++, 1661, _t58 ] % 0.45/0.75 (449,1) [977,1]. true => _t57 | ~_t56 [ SNF ] % 0.45/0.75 (1,1) [1595,1]. _t3 => box 1 _t112 [ SNF++, 650 ] % 0.45/0.75 (447,1) [1661,1]. _t57 => ~box 1~ _t113 [ SNF++, 976 ] % 0.45/0.75 (1,1) [1664,1]. true => ~_t114 | _t2 [ SNF++, 988 ] % 0.45/0.75 (449,1) [1728,1]. true => ~_t115 | _t56 [ SNF++, 992 ] % 0.45/0.75 (1,1) [2355,1]. true => ~_t114 | _t3 [ LRES, 740, 1664, ~_t2 ] % 0.45/0.75 (449,1) [2403,1]. true => ~_t115 | _t57 [ LRES, 977, 1728, ~_t56 ] % 0.45/0.75 (447,1) [7062,1]. true => ~_t57 | ~_t3 [ GEN1, 1595, 1661, 6916, _t112, _t113 ] % 0.45/0.75 (447,1) [7275,1]. true => ~_t114 | ~_t57 [ LRES, 7062, 2355, ~_t3 ] % 0.45/0.75 (449,1) [7364,1]. true => ~_t115 | ~_t114 [ LRES, 7275, 2403, ~_t57 ] % 0.45/0.75 (1,1) [562,2]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 1529, _t6 ] % 0.45/0.75 (1,1) [647,2]. true => _t5 | ~_t4 [ SNF ] % 0.45/0.75 (446,1) [974,2]. _t59 => ~box 1~ _t60 [ SNF ] [ SNF++, 1593, _t60 ] % 0.45/0.75 (447,1) [975,2]. true => _t59 | ~_t58 [ SNF ] % 0.45/0.75 (1,1) [1529,2]. _t5 => box 1 _t110 [ SNF++, 562 ] % 0.45/0.75 (446,1) [1593,2]. _t59 => ~box 1~ _t111 [ SNF++, 974 ] % 0.45/0.75 (1,1) [1596,2]. true => ~_t112 | _t4 [ SNF++, 650 ] % 0.45/0.75 (447,1) [1662,2]. true => ~_t113 | _t58 [ SNF++, 976 ] % 0.45/0.75 (1,1) [2319,2]. true => ~_t112 | _t5 [ LRES, 647, 1596, ~_t4 ] % 0.45/0.75 (447,1) [2375,2]. true => ~_t113 | _t59 [ LRES, 975, 1662, ~_t58 ] % 0.45/0.75 (446,1) [6731,2]. true => ~_t59 | ~_t5 [ GEN1, 1529, 1593, 6630, _t110, _t111 ] % 0.45/0.75 (446,1) [6732,2]. true => ~_t112 | ~_t59 [ LRES, 6731, 2319, ~_t5 ] % 0.45/0.75 (447,1) [6916,2]. true => ~_t113 | ~_t112 [ LRES, 6732, 2375, ~_t59 ] % 0.45/0.75 (1,1) [479,3]. _t7 => box 1 _t8 [ SNF ] [ SNF++, 1465, _t8 ] % 0.45/0.75 (1,1) [559,3]. true => _t7 | ~_t6 [ SNF ] % 0.45/0.75 (445,1) [972,3]. _t61 => ~box 1~ _t62 [ SNF ] [ SNF++, 1527, _t62 ] % 0.45/0.75 (446,1) [973,3]. true => _t61 | ~_t60 [ SNF ] % 0.45/0.75 (1,1) [1465,3]. _t7 => box 1 _t108 [ SNF++, 479 ] % 0.45/0.75 (445,1) [1527,3]. _t61 => ~box 1~ _t109 [ SNF++, 972 ] % 0.45/0.75 (1,1) [1530,3]. true => ~_t110 | _t6 [ SNF++, 562 ] % 0.45/0.75 (446,1) [1594,3]. true => ~_t111 | _t60 [ SNF++, 974 ] % 0.45/0.75 (1,1) [2265,3]. true => ~_t110 | _t7 [ LRES, 559, 1530, ~_t6 ] % 0.45/0.75 (446,1) [2324,3]. true => ~_t111 | _t61 [ LRES, 973, 1594, ~_t60 ] % 0.45/0.75 (445,1) [6277,3]. true => ~_t61 | ~_t7 [ GEN1, 1465, 1527, 6130, _t108, _t109 ] % 0.45/0.75 (445,1) [6278,3]. true => ~_t110 | ~_t61 [ LRES, 6277, 2265, ~_t7 ] % 0.45/0.75 (446,1) [6630,3]. true => ~_t111 | ~_t110 [ LRES, 6278, 2324, ~_t61 ] % 0.45/0.75 (1,1) [401,4]. _t9 => box 1 _t10 [ SNF ] [ SNF++, 1403, _t10 ] % 0.45/0.75 (1,1) [476,4]. true => _t9 | ~_t8 [ SNF ] % 0.45/0.75 (444,1) [970,4]. _t63 => ~box 1~ _t64 [ SNF ] [ SNF++, 1463, _t64 ] % 0.45/0.75 (445,1) [971,4]. true => _t63 | ~_t62 [ SNF ] % 0.45/0.75 (1,1) [1403,4]. _t9 => box 1 _t106 [ SNF++, 401 ] % 0.45/0.75 (444,1) [1463,4]. _t63 => ~box 1~ _t107 [ SNF++, 970 ] % 0.45/0.75 (1,1) [1466,4]. true => ~_t108 | _t8 [ SNF++, 479 ] % 0.45/0.75 (445,1) [1528,4]. true => ~_t109 | _t62 [ SNF++, 972 ] % 0.45/0.75 (1,1) [2204,4]. true => ~_t108 | _t9 [ LRES, 476, 1466, ~_t8 ] % 0.45/0.75 (445,1) [2283,4]. true => ~_t109 | _t63 [ LRES, 971, 1528, ~_t62 ] % 0.45/0.75 (444,1) [6080,4]. true => ~_t63 | ~_t9 [ GEN1, 1403, 1463, 6057, _t106, _t107 ] % 0.45/0.75 (444,1) [6081,4]. true => ~_t108 | ~_t63 [ LRES, 6080, 2204, ~_t9 ] % 0.45/0.75 (445,1) [6130,4]. true => ~_t109 | ~_t108 [ LRES, 6081, 2283, ~_t63 ] % 0.45/0.75 (1,1) [328,5]. _t11 => box 1 _t12 [ SNF ] [ SNF++, 1343, _t12 ] % 0.45/0.75 (1,1) [398,5]. true => _t11 | ~_t10 [ SNF ] % 0.45/0.75 (443,1) [968,5]. _t65 => ~box 1~ _t66 [ SNF ] [ SNF++, 1401, _t66 ] % 0.45/0.75 (444,1) [969,5]. true => _t65 | ~_t64 [ SNF ] % 0.45/0.75 (1,1) [1343,5]. _t11 => box 1 _t104 [ SNF++, 328 ] % 0.45/0.75 (443,1) [1401,5]. _t65 => ~box 1~ _t105 [ SNF++, 968 ] % 0.45/0.75 (1,1) [1404,5]. true => ~_t106 | _t10 [ SNF++, 401 ] % 0.45/0.75 (444,1) [1464,5]. true => ~_t107 | _t64 [ SNF++, 970 ] % 0.45/0.75 (1,1) [2139,5]. true => ~_t106 | _t11 [ LRES, 398, 1404, ~_t10 ] % 0.45/0.75 (444,1) [2212,5]. true => ~_t107 | _t65 [ LRES, 969, 1464, ~_t64 ] % 0.45/0.75 (443,1) [6051,5]. true => ~_t65 | ~_t11 [ GEN1, 1343, 1401, 6039, _t104, _t105 ] % 0.45/0.75 (443,1) [6052,5]. true => ~_t106 | ~_t65 [ LRES, 6051, 2139, ~_t11 ] % 0.45/0.75 (444,1) [6057,5]. true => ~_t107 | ~_t106 [ LRES, 6052, 2212, ~_t65 ] % 0.45/0.75 (1,1) [260,6]. _t13 => box 1 _t14 [ SNF ] [ SNF++, 1285, _t14 ] % 0.45/0.75 (1,1) [325,6]. true => _t13 | ~_t12 [ SNF ] % 0.45/0.75 (442,1) [966,6]. _t67 => ~box 1~ _t68 [ SNF ] [ SNF++, 1341, _t68 ] % 0.45/0.75 (443,1) [967,6]. true => _t67 | ~_t66 [ SNF ] % 0.45/0.75 (1,1) [1285,6]. _t13 => box 1 _t102 [ SNF++, 260 ] % 0.45/0.75 (442,1) [1341,6]. _t67 => ~box 1~ _t103 [ SNF++, 966 ] % 0.45/0.75 (1,1) [1344,6]. true => ~_t104 | _t12 [ SNF++, 328 ] % 0.45/0.75 (443,1) [1402,6]. true => ~_t105 | _t66 [ SNF++, 968 ] % 0.45/0.75 (1,1) [2052,6]. true => ~_t104 | _t13 [ LRES, 325, 1344, ~_t12 ] % 0.45/0.75 (443,1) [2155,6]. true => ~_t105 | _t67 [ LRES, 967, 1402, ~_t66 ] % 0.45/0.75 (442,1) [6020,6]. true => ~_t67 | ~_t13 [ GEN1, 1285, 1341, 6011, _t102, _t103 ] % 0.45/0.75 (442,1) [6021,6]. true => ~_t104 | ~_t67 [ LRES, 6020, 2052, ~_t13 ] % 0.45/0.75 (443,1) [6039,6]. true => ~_t105 | ~_t104 [ LRES, 6021, 2155, ~_t67 ] % 0.45/0.75 (1,1) [197,7]. _t15 => box 1 _t16 [ SNF ] [ SNF++, 1229, _t16 ] % 0.45/0.75 (1,1) [257,7]. true => _t15 | ~_t14 [ SNF ] % 0.45/0.75 (441,1) [964,7]. _t69 => ~box 1~ _t70 [ SNF ] [ SNF++, 1283, _t70 ] % 0.45/0.75 (442,1) [965,7]. true => _t69 | ~_t68 [ SNF ] % 0.45/0.75 (1,1) [1229,7]. _t15 => box 1 _t100 [ SNF++, 197 ] % 0.45/0.75 (441,1) [1283,7]. _t69 => ~box 1~ _t101 [ SNF++, 964 ] % 0.45/0.75 (1,1) [1286,7]. true => ~_t102 | _t14 [ SNF++, 260 ] % 0.45/0.75 (442,1) [1342,7]. true => ~_t103 | _t68 [ SNF++, 966 ] % 0.45/0.75 (1,1) [2012,7]. true => ~_t102 | _t15 [ LRES, 257, 1286, ~_t14 ] % 0.45/0.75 (442,1) [2081,7]. true => ~_t103 | _t69 [ LRES, 965, 1342, ~_t68 ] % 0.45/0.75 (441,1) [6004,7]. true => ~_t69 | ~_t15 [ GEN1, 1229, 1283, 5994, _t100, _t101 ] % 0.45/0.75 (441,1) [6005,7]. true => ~_t102 | ~_t69 [ LRES, 6004, 2012, ~_t15 ] % 0.45/0.75 (442,1) [6011,7]. true => ~_t103 | ~_t102 [ LRES, 6005, 2081, ~_t69 ] % 0.45/0.75 (1,1) [139,8]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 1175, _t18 ] % 0.45/0.75 (1,1) [194,8]. true => _t17 | ~_t16 [ SNF ] % 0.45/0.75 (440,1) [962,8]. _t71 => ~box 1~ _t72 [ SNF ] [ SNF++, 1227, _t72 ] % 0.45/0.75 (441,1) [963,8]. true => _t71 | ~_t70 [ SNF ] % 0.45/0.75 (1,1) [1175,8]. _t17 => box 1 _t98 [ SNF++, 139 ] % 0.45/0.75 (440,1) [1227,8]. _t71 => ~box 1~ _t99 [ SNF++, 962 ] % 0.45/0.75 (1,1) [1230,8]. true => ~_t100 | _t16 [ SNF++, 197 ] % 0.45/0.75 (441,1) [1284,8]. true => ~_t101 | _t70 [ SNF++, 964 ] % 0.45/0.75 (1,1) [1981,8]. true => ~_t100 | _t17 [ LRES, 194, 1230, ~_t16 ] % 0.45/0.75 (441,1) [2021,8]. true => ~_t101 | _t71 [ LRES, 963, 1284, ~_t70 ] % 0.45/0.75 (440,1) [5983,8]. true => ~_t71 | ~_t17 [ GEN1, 1175, 1227, 5977, _t98, _t99 ] % 0.45/0.75 (440,1) [5984,8]. true => ~_t100 | ~_t71 [ LRES, 5983, 1981, ~_t17 ] % 0.45/0.75 (441,1) [5994,8]. true => ~_t101 | ~_t100 [ LRES, 5984, 2021, ~_t71 ] % 0.45/0.75 (1,1) [65,9]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 1123, _t20 ] % 0.45/0.75 (1,1) [96,9]. true => _t19 | ~_t18 [ SNF ] % 0.45/0.75 (436,1) [955,9]. _t73 => ~box 1~ _t74 [ SNF ] [ SNF++, 1171, _t74 ] % 0.45/0.75 (440,1) [956,9]. true => _t73 | ~_t72 [ SNF ] % 0.45/0.75 (1,1) [1123,9]. _t19 => box 1 _t92 [ SNF++, 65 ] % 0.45/0.75 (436,1) [1171,9]. _t73 => ~box 1~ _t96 [ SNF++, 955 ] % 0.45/0.75 (1,1) [1176,9]. true => ~_t98 | _t18 [ SNF++, 139 ] % 0.45/0.75 (440,1) [1228,9]. true => ~_t99 | _t72 [ SNF++, 962 ] % 0.45/0.75 (1,1) [1903,9]. true => ~_t98 | _t19 [ LRES, 96, 1176, ~_t18 ] % 0.45/0.75 (440,1) [1987,9]. true => ~_t99 | _t73 [ LRES, 956, 1228, ~_t72 ] % 0.45/0.75 (436,1) [5954,9]. true => ~_t73 | ~_t19 [ GEN1, 1123, 1171, 5938, _t92, _t96 ] % 0.45/0.75 (436,1) [5955,9]. true => ~_t98 | ~_t73 [ LRES, 5954, 1903, ~_t19 ] % 0.45/0.75 (440,1) [5977,9]. true => ~_t99 | ~_t98 [ LRES, 5955, 1987, ~_t73 ] % 0.45/0.75 (1,1) [8,10]. _t21 => box 1 _t22 [ SNF ] [ SNF++, 1075, _t22 ] % 0.45/0.75 (1,1) [9,10]. true => _t22 | ~_t21 [ Axiom T ] % 0.45/0.75 (6,1) [13,10]. _t22 => ~box 1~ _t23 [ Axiom T ] [ SNF++, 1103, _t23 ] % 0.45/0.75 (1,1) [14,10]. true => _t21 | ~_t20 [ SNF ] % 0.45/0.75 (8,1) [34,10]. _t27 => ~box 1~ _t28 [ Axiom T ] [ SNF++, 1105, _t28 ] % 0.45/0.75 (1,1) [48,10]. _t30 => box 1 _t31 [ SNF ] [ SNF++, 1079, _t31 ] % 0.45/0.75 (1,1) [52,10]. _t33 => box 1 _t23 [ Axiom T ] [ SNF++, 1083, _t23 ] % 0.45/0.75 (1,1) [58,10]. true => _t30 | ~_t20 [ SNF ] % 0.45/0.75 (1,1) [59,10]. _t35 => box 1 _t21 [ SNF ] [ SNF++, 1085, _t21 ] % 0.45/0.75 (1,1) [60,10]. true => ~_t35 | _t21 [ Axiom T ] % 0.45/0.75 (1,1) [61,10]. true => _t35 | ~_t34 | _t27 [ SNF ] % 0.45/0.75 (1,1) [62,10]. true => _t34 | ~_t20 [ SNF ] % 0.45/0.75 (1,1) [952,10]. _t74 => box 1 _t75 [ SNF ] [ SNF++, 1101, _t75 ] % 0.45/0.75 (1,1) [1075,10]. _t21 => box 1 _t80 [ SNF++, 8 ] % 0.45/0.75 (1,1) [1079,10]. _t30 => box 1 _t87 [ SNF++, 48 ] % 0.45/0.75 (1,1) [1085,10]. _t35 => box 1 _t81 [ SNF++, 59 ] % 0.45/0.75 (1,1) [1101,10]. _t74 => box 1 _t91 [ SNF++, 952 ] % 0.45/0.75 (6,1) [1103,10]. _t22 => ~box 1~ _t77 [ SNF++, 13 ] % 0.45/0.75 (8,1) [1105,10]. _t27 => ~box 1~ _t78 [ SNF++, 34 ] % 0.45/0.75 (1,1) [1124,10]. true => ~_t92 | _t20 [ SNF++, 65 ] % 0.45/0.75 (436,1) [1172,10]. true => ~_t96 | _t74 [ SNF++, 955 ] % 0.45/0.75 (1,1) [1731,10]. true => ~_t35 | _t22 [ LRES, 9, 60, ~_t21 ] % 0.45/0.75 (1,1) [1746,10]. true => ~_t92 | _t34 [ LRES, 62, 1124, ~_t20 ] % 0.45/0.75 (1,1) [1754,10]. true => ~_t92 | _t30 [ LRES, 58, 1124, ~_t20 ] % 0.45/0.75 (1,1) [1772,10]. true => ~_t92 | _t21 [ LRES, 14, 1124, ~_t20 ] % 0.45/0.75 (8,1) [2257,10]. true => ~_t27 | ~_t21 [ GEN1, 1075, 1105, 1979, _t80, _t78 ] % 0.45/0.75 (6,1) [2687,10]. true => ~_t74 | ~_t35 | ~_t30 | ~_t22 [ GEN1, 1101, 1085, 1079, 1103, 2668, _t91, _t81, _t87, _t77 ] [ Backward Subsumption, 5908 ] % 0.45/0.75 (8,1) [2844,10]. true => ~_t92 | ~_t27 [ LRES, 2257, 1772, ~_t21 ] % 0.45/0.75 (8,1) [2902,10]. true => ~_t92 | _t35 | ~_t34 [ LRES, 2844, 61, ~_t27 ] [ Backward Subsumption, 4774 ] % 0.45/0.75 (8,1) [4774,10]. true => ~_t92 | _t35 [ LRES, 2902, 1746, ~_t34 ] % 0.45/0.75 (6,1) [5908,10]. true => ~_t74 | ~_t35 | ~_t30 [ LRES, 2687, 1731, ~_t22 ] % 0.45/0.75 (6,1) [5916,10]. true => ~_t92 | ~_t74 | ~_t35 [ LRES, 5908, 1754, ~_t30 ] [ Backward Subsumption, 5920 ] % 0.45/0.75 (8,1) [5920,10]. true => ~_t92 | ~_t74 [ LRES, 5916, 4774, ~_t35 ] % 0.45/0.75 (436,1) [5938,10]. true => ~_t96 | ~_t92 [ LRES, 5920, 1172, ~_t74 ] % 0.45/0.75 (6,1) [7,11]. _t22 => ~box 1~ _t23 [ SNF ] [ SNF++, 1051, _t23 ] % 0.45/0.75 (6,1) [10,11]. true => ~_t23 | p0 [ Axiom T ] % 0.45/0.75 (8,1) [17,11]. _t27 => ~box 1~ _t28 [ SNF ] [ SNF++, 1053, _t28 ] % 0.45/0.75 (1,1) [32,11]. _t28 => box 1 ~p0 [ Axiom T ] [ SNF++, 1061, ~p0 ] % 0.45/0.75 (1,1) [35,11]. _t21 => box 1 _t22 [ Axiom T ] [ SNF++, 1063, _t22 ] % 0.45/0.75 (1,1) [44,11]. true => ~_t32 | _t27 [ Axiom T ] % 0.45/0.75 (1,1) [45,11]. _t33 => box 1 _t23 [ SNF ] [ SNF++, 1067, _t23 ] % 0.45/0.75 (1,1) [47,11]. true => _t33 | _t32 | ~_t31 | ~p0 [ SNF ] % 0.45/0.75 (435,1) [951,11]. _t75 => ~box 1~ ~p0 [ SNF ] [ SNF++, 1059, ~p0 ] % 0.45/0.75 (6,1) [1051,11]. _t22 => ~box 1~ _t77 [ SNF++, 7 ] % 0.45/0.75 (8,1) [1053,11]. _t27 => ~box 1~ _t78 [ SNF++, 17 ] % 0.45/0.75 (435,1) [1059,11]. _t75 => ~box 1~ _t79 [ SNF++, 951 ] % 0.45/0.75 (1,1) [1061,11]. _t28 => box 1 _t79 [ SNF++, 32 ] % 0.45/0.75 (1,1) [1063,11]. _t21 => box 1 _t80 [ SNF++, 35 ] % 0.45/0.75 (1,1) [1067,11]. _t33 => box 1 _t77 [ SNF++, 45 ] % 0.45/0.75 (1,1) [1076,11]. true => ~_t80 | _t22 [ SNF++, 8 ] % 0.45/0.75 (1,1) [1080,11]. true => ~_t87 | _t31 [ SNF++, 48 ] % 0.45/0.75 (1,1) [1084,11]. true => ~_t77 | _t23 [ SNF++, 52 ] % 0.45/0.75 (1,1) [1086,11]. true => ~_t81 | _t21 [ SNF++, 59 ] % 0.45/0.75 (1,1) [1102,11]. true => ~_t91 | _t75 [ SNF++, 952 ] % 0.45/0.75 (8,1) [1106,11]. true => ~_t78 | _t28 [ SNF++, 34 ] % 0.45/0.75 (6,1) [1864,11]. true => ~_t28 | ~_t22 [ GEN1, 1061, 1051, 1794, _t79, _t77 ] % 0.45/0.75 (435,1) [1865,11]. true => ~_t75 | ~_t33 [ GEN1, 1067, 1059, 1794, _t77, _t79 ] % 0.45/0.75 (8,1) [1949,11]. true => ~_t27 | ~_t21 [ GEN1, 1063, 1053, 1911, _t80, _t78 ] % 0.45/0.75 (6,1) [1973,11]. true => ~_t80 | ~_t28 [ LRES, 1864, 1076, ~_t22 ] % 0.45/0.75 (8,1) [1979,11]. true => ~_t80 | ~_t78 [ LRES, 1973, 1106, ~_t28 ] % 0.45/0.75 (8,1) [2165,11]. true => ~_t81 | ~_t27 [ LRES, 1949, 1086, ~_t21 ] % 0.45/0.75 (8,1) [2177,11]. true => ~_t81 | ~_t32 [ LRES, 2165, 44, ~_t27 ] % 0.45/0.75 (6,1) [2535,11]. true => _t33 | _t32 | ~_t31 | ~_t23 [ LRES, 47, 10, ~p0 ] % 0.45/0.75 (6,1) [2545,11]. true => ~_t77 | _t33 | _t32 | ~_t31 [ LRES, 2535, 1084, ~_t23 ] % 0.45/0.75 (6,1) [2560,11]. true => ~_t87 | ~_t77 | _t33 | _t32 [ LRES, 2545, 1080, ~_t31 ] % 0.45/0.75 (8,1) [2572,11]. true => ~_t87 | ~_t81 | ~_t77 | _t33 [ LRES, 2560, 2177, _t32 ] % 0.45/0.75 (435,1) [2593,11]. true => ~_t87 | ~_t81 | ~_t77 | ~_t75 [ LRES, 2572, 1865, _t33 ] % 0.45/0.75 (435,1) [2668,11]. true => ~_t91 | ~_t87 | ~_t81 | ~_t77 [ LRES, 2593, 1102, ~_t75 ] % 0.45/0.75 (6,1) [4,12]. true => ~_t23 | p0 [ SNF ] % 0.45/0.75 (1,1) [15,12]. _t28 => box 1 ~p0 [ SNF ] [ SNF++, 1047, ~p0 ] % 0.45/0.75 (14,1) [27,12]. _t22 => ~box 1~ _t23 [ Axiom T ] [ SNF++, 1043, _t23 ] % 0.45/0.75 (14,1) [1043,12]. _t22 => ~box 1~ _t77 [ SNF++, 27 ] % 0.45/0.75 (1,1) [1047,12]. _t28 => box 1 _t79 [ SNF++, 15 ] % 0.45/0.75 (6,1) [1052,12]. true => ~_t77 | _t23 [ SNF++, 7 ] % 0.45/0.75 (8,1) [1054,12]. true => ~_t78 | _t28 [ SNF++, 17 ] % 0.45/0.75 (435,1) [1060,12]. true => ~_t79 | ~p0 [ SNF++, 951 ] % 0.45/0.75 (1,1) [1064,12]. true => ~_t80 | _t22 [ SNF++, 35 ] % 0.45/0.75 (435,1) [1738,12]. true => ~_t79 | ~_t23 [ LRES, 1060, 4, ~p0 ] % 0.45/0.75 (435,1) [1794,12]. true => ~_t79 | ~_t77 [ LRES, 1738, 1052, ~_t23 ] % 0.45/0.75 (14,1) [1838,12]. true => ~_t28 | ~_t22 [ GEN1, 1047, 1043, 1775, _t79, _t77 ] % 0.45/0.75 (14,1) [1877,12]. true => ~_t80 | ~_t28 [ LRES, 1838, 1064, ~_t22 ] % 0.45/0.75 (14,1) [1911,12]. true => ~_t80 | ~_t78 [ LRES, 1877, 1054, ~_t28 ] % 0.45/0.75 (14,1) [24,13]. true => ~_t23 | p0 [ Axiom T ] % 0.45/0.75 (14,1) [1044,13]. true => ~_t77 | _t23 [ SNF++, 27 ] % 0.45/0.75 (1,1) [1048,13]. true => ~_t79 | ~p0 [ SNF++, 15 ] % 0.45/0.75 (14,1) [1742,13]. true => ~_t79 | ~_t23 [ LRES, 1048, 24, ~p0 ] % 0.45/0.75 (14,1) [1775,13]. true => ~_t79 | ~_t77 [ LRES, 1742, 1044, ~_t23 ] % 0.45/0.75 % SZS output end Refutation % 0.45/0.76 % KSP exiting %------------------------------------------------------------------------------