%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP103_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n022.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:59 PM UTC 2026 % Result : Theorem 0.45s 0.87s % Output : Refutation 0.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP103_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.16/0.33 % Computer : n022.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Mon May 4 17:38:35 EDT 2026 % 0.16/0.33 % CPUTime : % 0.37/0.59 ----KSP format--- % 0.37/0.59 set(box,REF). % 0.37/0.59 usable(formulas). % 0.37/0.59 true. % 0.37/0.59 end_of_list. % 0.37/0.59 sos(formulas). % 0.37/0.59 ~ (( [] ( [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) ) & [] ( [] ( [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) ) ) & [] ( [] ( [] ( [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( [] ( [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) ) ) ) ) ) & ~ ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> p0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) -> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> [] ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) ) ) & [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( ( p0 -> [] ( p0 ) ) -> [] ( ( p0 -> [] ( p0 ) ) ) ) ) -> ( p0 -> [] ( p0 ) ) ) ) -> ( <> ( [] ( ( p0 -> [] ( p0 ) ) ) ) -> ( ( p0 -> [] ( p0 ) ) | [] ( ( p0 -> [] ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ). % 0.37/0.59 end_of_list. % 0.37/0.59 ----------------- % 0.37/0.59 ksp -tstp -pproof -early_ple -mlple -ord -snf++ -unit -lhs_unit -fsub -bsub -limited_reuse_renaming -bnfsimp -maxproof 1 -populate_max_lit_positive -short -global2local -i /export/starexec/sandbox/tmp/tmp.zbE99lzOOj/theBenchmark.ksp % 0.45/0.87 % 0.45/0.87 % SZS status Theorem % 0.45/0.87 % 0.45/0.87 ***************** % 0.45/0.87 FOUND PROOF 1 % 0.45/0.87 ***************** % 0.45/0.87 % SZS output start Refutation % 0.45/0.87 % 0.45/0.87 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.45/0.87 (1,1) [584,0]. _t1 => box 1 _t2 [ SNF ] [ Backward Subsumption, 792 ] % 0.45/0.87 (1,1) [646,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 790 ] % 0.45/0.87 (107,1) [779,0]. _t46 => ~box 1~ _t47 [ SNF ] [ Backward Subsumption, 801 ] % 0.45/0.87 (1,1) [780,0]. true => _t46 | ~_t0 [ SNF ] [ Backward Subsumption, 781 ] % 0.45/0.87 (1,1) [781,0]. true => _t46 [ Unit Resolution, 3, 780, _t0 ] [ Modal Level Pure Literal Elimination, _t46 ] % 0.45/0.87 (1,1) [790,0]. true => _t1 [ Unit Resolution, 3, 646, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 0.45/0.87 (1,1) [792,0]. true => box 1 _t2 [ LHS Unit Resolution, 790, 584, _t1 ] [ SNF++, 1357, _t2 ] % 0.45/0.87 (107,1) [801,0]. true => ~box 1~ _t47 [ LHS Unit Resolution, 781, 779, _t46 ] [ SNF++, 1421, _t47 ] % 0.45/0.87 (1,1) [1357,0]. true => box 1 _t101 [ SNF++, 792 ] % 0.45/0.87 (107,1) [1421,0]. true => ~box 1~ _t103 [ SNF++, 801 ] % 0.45/0.87 (107,1) [13339,0]. true => false [ GEN1, 1357, 1421, 13329, _t101, _t103 ] % 0.45/0.87 (1,1) [524,1]. _t2 => box 1 _t3 [ SNF ] [ SNF++, 1293, _t3 ] % 0.45/0.87 (106,1) [778,1]. _t47 => ~box 1~ _t48 [ SNF ] [ SNF++, 1355, _t48 ] % 0.45/0.87 (1,1) [1293,1]. _t2 => box 1 _t98 [ SNF++, 524 ] % 0.45/0.87 (106,1) [1355,1]. _t47 => ~box 1~ _t100 [ SNF++, 778 ] % 0.45/0.87 (1,1) [1358,1]. true => ~_t101 | _t2 [ SNF++, 792 ] % 0.45/0.87 (107,1) [1422,1]. true => ~_t103 | _t47 [ SNF++, 801 ] % 0.45/0.87 (106,1) [13321,1]. true => ~_t47 | ~_t2 [ GEN1, 1293, 1355, 13303, _t98, _t100 ] % 0.45/0.87 (106,1) [13322,1]. true => ~_t101 | ~_t47 [ LRES, 13321, 1358, ~_t2 ] % 0.45/0.87 (107,1) [13329,1]. true => ~_t103 | ~_t101 [ LRES, 13322, 1422, ~_t47 ] % 0.45/0.87 (1,1) [466,2]. _t3 => box 1 _t4 [ SNF ] [ SNF++, 1233, _t4 ] % 0.45/0.87 (105,1) [777,2]. _t48 => ~box 1~ _t49 [ SNF ] [ SNF++, 1291, _t49 ] % 0.45/0.87 (1,1) [1233,2]. _t3 => box 1 _t95 [ SNF++, 466 ] % 0.45/0.87 (105,1) [1291,2]. _t48 => ~box 1~ _t97 [ SNF++, 777 ] % 0.45/0.87 (1,1) [1294,2]. true => ~_t98 | _t3 [ SNF++, 524 ] % 0.45/0.87 (106,1) [1356,2]. true => ~_t100 | _t48 [ SNF++, 778 ] % 0.45/0.87 (105,1) [13296,2]. true => ~_t48 | ~_t3 [ GEN1, 1233, 1291, 13291, _t95, _t97 ] % 0.45/0.87 (105,1) [13297,2]. true => ~_t98 | ~_t48 [ LRES, 13296, 1294, ~_t3 ] % 0.45/0.87 (106,1) [13303,2]. true => ~_t100 | ~_t98 [ LRES, 13297, 1356, ~_t48 ] % 0.45/0.87 (1,1) [410,3]. _t4 => box 1 _t5 [ SNF ] [ SNF++, 1177, _t5 ] % 0.45/0.87 (104,1) [776,3]. _t49 => ~box 1~ _t50 [ SNF ] [ SNF++, 1231, _t50 ] % 0.45/0.87 (1,1) [1177,3]. _t4 => box 1 _t92 [ SNF++, 410 ] % 0.45/0.87 (104,1) [1231,3]. _t49 => ~box 1~ _t94 [ SNF++, 776 ] % 0.45/0.87 (1,1) [1234,3]. true => ~_t95 | _t4 [ SNF++, 466 ] % 0.45/0.87 (105,1) [1292,3]. true => ~_t97 | _t49 [ SNF++, 777 ] % 0.45/0.87 (104,1) [13281,3]. true => ~_t49 | ~_t4 [ GEN1, 1177, 1231, 13276, _t92, _t94 ] % 0.45/0.87 (104,1) [13282,3]. true => ~_t95 | ~_t49 [ LRES, 13281, 1234, ~_t4 ] % 0.45/0.87 (105,1) [13291,3]. true => ~_t97 | ~_t95 [ LRES, 13282, 1292, ~_t49 ] % 0.45/0.87 (1,1) [356,4]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 1125, _t6 ] % 0.45/0.87 (103,1) [775,4]. _t50 => ~box 1~ _t51 [ SNF ] [ SNF++, 1175, _t51 ] % 0.45/0.87 (1,1) [1125,4]. _t5 => box 1 _t89 [ SNF++, 356 ] % 0.45/0.87 (103,1) [1175,4]. _t50 => ~box 1~ _t91 [ SNF++, 775 ] % 0.45/0.87 (1,1) [1178,4]. true => ~_t92 | _t5 [ SNF++, 410 ] % 0.45/0.87 (104,1) [1232,4]. true => ~_t94 | _t50 [ SNF++, 776 ] % 0.45/0.87 (103,1) [13259,4]. true => ~_t50 | ~_t5 [ GEN1, 1125, 1175, 13249, _t89, _t91 ] % 0.45/0.87 (103,1) [13260,4]. true => ~_t92 | ~_t50 [ LRES, 13259, 1178, ~_t5 ] % 0.45/0.87 (104,1) [13276,4]. true => ~_t94 | ~_t92 [ LRES, 13260, 1232, ~_t50 ] % 0.45/0.87 (1,1) [304,5]. _t6 => box 1 _t7 [ SNF ] [ SNF++, 1077, _t7 ] % 0.45/0.87 (102,1) [774,5]. _t51 => ~box 1~ _t52 [ SNF ] [ SNF++, 1123, _t52 ] % 0.45/0.87 (1,1) [1077,5]. _t6 => box 1 _t86 [ SNF++, 304 ] % 0.45/0.87 (102,1) [1123,5]. _t51 => ~box 1~ _t88 [ SNF++, 774 ] % 0.45/0.87 (1,1) [1126,5]. true => ~_t89 | _t6 [ SNF++, 356 ] % 0.45/0.87 (103,1) [1176,5]. true => ~_t91 | _t51 [ SNF++, 775 ] % 0.45/0.87 (102,1) [13236,5]. true => ~_t51 | ~_t6 [ GEN1, 1077, 1123, 13218, _t86, _t88 ] % 0.45/0.87 (102,1) [13237,5]. true => ~_t89 | ~_t51 [ LRES, 13236, 1126, ~_t6 ] % 0.45/0.87 (103,1) [13249,5]. true => ~_t91 | ~_t89 [ LRES, 13237, 1176, ~_t51 ] % 0.45/0.87 (1,1) [254,6]. _t7 => box 1 _t8 [ SNF ] [ SNF++, 1033, _t8 ] % 0.45/0.87 (101,1) [773,6]. _t52 => ~box 1~ _t53 [ SNF ] [ SNF++, 1075, _t53 ] % 0.45/0.87 (1,1) [1033,6]. _t7 => box 1 _t83 [ SNF++, 254 ] % 0.45/0.87 (101,1) [1075,6]. _t52 => ~box 1~ _t85 [ SNF++, 773 ] % 0.45/0.87 (1,1) [1078,6]. true => ~_t86 | _t7 [ SNF++, 304 ] % 0.45/0.87 (102,1) [1124,6]. true => ~_t88 | _t52 [ SNF++, 774 ] % 0.45/0.87 (101,1) [13214,6]. true => ~_t52 | ~_t7 [ GEN1, 1033, 1075, 13195, _t83, _t85 ] % 0.45/0.87 (101,1) [13215,6]. true => ~_t86 | ~_t52 [ LRES, 13214, 1078, ~_t7 ] % 0.45/0.87 (102,1) [13218,6]. true => ~_t88 | ~_t86 [ LRES, 13215, 1124, ~_t52 ] % 0.45/0.87 (1,1) [206,7]. _t8 => box 1 _t9 [ SNF ] [ SNF++, 993, _t9 ] % 0.45/0.87 (100,1) [772,7]. _t53 => ~box 1~ _t54 [ SNF ] [ SNF++, 1031, _t54 ] % 0.45/0.87 (1,1) [993,7]. _t8 => box 1 _t80 [ SNF++, 206 ] % 0.45/0.87 (100,1) [1031,7]. _t53 => ~box 1~ _t82 [ SNF++, 772 ] % 0.45/0.87 (1,1) [1034,7]. true => ~_t83 | _t8 [ SNF++, 254 ] % 0.45/0.87 (101,1) [1076,7]. true => ~_t85 | _t53 [ SNF++, 773 ] % 0.45/0.87 (100,1) [13177,7]. true => ~_t53 | ~_t8 [ GEN1, 993, 1031, 13147, _t80, _t82 ] % 0.45/0.87 (100,1) [13178,7]. true => ~_t83 | ~_t53 [ LRES, 13177, 1034, ~_t8 ] % 0.45/0.87 (101,1) [13195,7]. true => ~_t85 | ~_t83 [ LRES, 13178, 1076, ~_t53 ] % 0.45/0.87 (1,1) [160,8]. _t9 => box 1 _t10 [ SNF ] [ SNF++, 957, _t10 ] % 0.45/0.87 (99,1) [771,8]. _t54 => ~box 1~ _t55 [ SNF ] [ SNF++, 991, _t55 ] % 0.45/0.87 (1,1) [957,8]. _t9 => box 1 _t77 [ SNF++, 160 ] % 0.45/0.87 (99,1) [991,8]. _t54 => ~box 1~ _t79 [ SNF++, 771 ] % 0.45/0.87 (1,1) [994,8]. true => ~_t80 | _t9 [ SNF++, 206 ] % 0.45/0.87 (100,1) [1032,8]. true => ~_t82 | _t54 [ SNF++, 772 ] % 0.45/0.87 (99,1) [13135,8]. true => ~_t54 | ~_t9 [ GEN1, 957, 991, 13073, _t77, _t79 ] % 0.45/0.87 (99,1) [13136,8]. true => ~_t80 | ~_t54 [ LRES, 13135, 994, ~_t9 ] % 0.45/0.87 (100,1) [13147,8]. true => ~_t82 | ~_t80 [ LRES, 13136, 1032, ~_t54 ] % 0.45/0.87 (1,1) [116,9]. _t10 => box 1 _t11 [ SNF ] [ SNF++, 925, _t11 ] % 0.45/0.87 (98,1) [770,9]. _t55 => ~box 1~ _t56 [ SNF ] [ SNF++, 955, _t56 ] % 0.45/0.87 (1,1) [925,9]. _t10 => box 1 _t75 [ SNF++, 116 ] % 0.45/0.87 (98,1) [955,9]. _t55 => ~box 1~ _t76 [ SNF++, 770 ] % 0.45/0.87 (1,1) [958,9]. true => ~_t77 | _t10 [ SNF++, 160 ] % 0.45/0.87 (99,1) [992,9]. true => ~_t79 | _t55 [ SNF++, 771 ] % 0.45/0.87 (98,1) [13049,9]. true => ~_t55 | ~_t10 [ GEN1, 925, 955, 13030, _t75, _t76 ] % 0.45/0.87 (98,1) [13050,9]. true => ~_t77 | ~_t55 [ LRES, 13049, 958, ~_t10 ] % 0.45/0.87 (99,1) [13073,9]. true => ~_t79 | ~_t77 [ LRES, 13050, 992, ~_t55 ] % 0.45/0.87 (1,1) [74,10]. _t11 => box 1 _t12 [ SNF ] [ SNF++, 895, _t12 ] % 0.45/0.87 (97,1) [769,10]. _t56 => ~box 1~ _t57 [ SNF ] [ SNF++, 923, _t57 ] % 0.45/0.87 (1,1) [895,10]. _t11 => box 1 _t73 [ SNF++, 74 ] % 0.45/0.87 (97,1) [923,10]. _t56 => ~box 1~ _t74 [ SNF++, 769 ] % 0.45/0.87 (1,1) [926,10]. true => ~_t75 | _t11 [ SNF++, 116 ] % 0.45/0.87 (98,1) [956,10]. true => ~_t76 | _t56 [ SNF++, 770 ] % 0.45/0.87 (97,1) [13014,10]. true => ~_t56 | ~_t11 [ GEN1, 895, 923, 12984, _t73, _t74 ] % 0.45/0.87 (97,1) [13015,10]. true => ~_t75 | ~_t56 [ LRES, 13014, 926, ~_t11 ] % 0.45/0.87 (98,1) [13030,10]. true => ~_t76 | ~_t75 [ LRES, 13015, 956, ~_t56 ] % 0.45/0.87 (1,1) [14,11]. _t15 => box 1 _t16 [ Axiom T ] [ SNF++, 865, _t16 ] % 0.45/0.87 (1,1) [17,11]. true => ~_t16 | p0 [ Axiom T ] % 0.45/0.87 (1,1) [35,11]. _t20 => box 1 _t21 [ Axiom T ] [ SNF++, 871, _t21 ] % 0.45/0.87 (10,1) [47,11]. _t24 => ~box 1~ _t25 [ SNF ] [ SNF++, 885, _t25 ] % 0.45/0.87 (1,1) [50,11]. _t29 => box 1 _t17 [ SNF ] [ SNF++, 873, _t17 ] % 0.45/0.87 (1,1) [52,11]. true => _t29 | ~_t28 | _t24 | _t16 | p0 [ SNF ] % 0.45/0.87 (1,1) [53,11]. true => _t28 | ~_t12 [ SNF ] % 0.45/0.87 (97,1) [765,11]. true => ~_t57 | ~p0 [ SNF ] % 0.45/0.87 (97,1) [766,11]. true => ~_t57 | _t20 [ SNF ] % 0.45/0.87 (94,1) [767,11]. _t58 => ~box 1~ _t16 [ SNF ] [ SNF++, 889, _t16 ] % 0.45/0.87 (97,1) [768,11]. true => _t58 | ~_t57 [ SNF ] % 0.45/0.87 (1,1) [871,11]. _t20 => box 1 _t65 [ SNF++, 35 ] % 0.45/0.87 (1,1) [873,11]. _t29 => box 1 _t69 [ SNF++, 50 ] % 0.45/0.87 (10,1) [885,11]. _t24 => ~box 1~ _t71 [ SNF++, 47 ] % 0.45/0.87 (94,1) [889,11]. _t58 => ~box 1~ _t64 [ SNF++, 767 ] % 0.45/0.87 (1,1) [896,11]. true => ~_t73 | _t12 [ SNF++, 74 ] % 0.45/0.87 (97,1) [924,11]. true => ~_t74 | _t57 [ SNF++, 769 ] % 0.45/0.87 (1,1) [1478,11]. true => ~_t73 | _t28 [ LRES, 53, 896, ~_t12 ] % 0.45/0.87 (97,1) [1575,11]. true => ~_t57 | ~_t16 [ LRES, 765, 17, ~p0 ] % 0.45/0.87 (97,1) [1580,11]. true => ~_t57 | _t29 | ~_t28 | _t24 | _t16 [ LRES, 765, 52, ~p0 ] [ Backward Subsumption, 12831 ] % 0.45/0.87 (97,1) [1826,11]. true => ~_t74 | _t58 [ LRES, 768, 924, ~_t57 ] % 0.45/0.87 (94,1) [2041,11]. true => ~_t58 | ~_t29 [ GEN1, 873, 889, 1885, _t69, _t64 ] % 0.45/0.87 (10,1) [2815,11]. true => ~_t24 | ~_t20 [ GEN1, 871, 885, 2796, _t65, _t71 ] % 0.45/0.88 (97,1) [2816,11]. true => ~_t57 | ~_t24 [ LRES, 2815, 766, ~_t20 ] % 0.45/0.88 (97,1) [12831,11]. true => ~_t57 | _t29 | ~_t28 | _t24 [ LRES, 1580, 1575, _t16 ] [ Backward Subsumption, 12852 ] % 0.45/0.88 (97,1) [12852,11]. true => ~_t57 | _t29 | ~_t28 [ LRES, 12831, 2816, _t24 ] % 0.45/0.88 (97,1) [12889,11]. true => ~_t73 | ~_t57 | _t29 [ LRES, 12852, 1478, ~_t28 ] % 0.45/0.88 (97,1) [12899,11]. true => ~_t73 | ~_t58 | ~_t57 [ LRES, 12889, 2041, _t29 ] % 0.45/0.88 (97,1) [12970,11]. true => ~_t74 | ~_t73 | ~_t58 [ LRES, 12899, 924, ~_t57 ] [ Backward Subsumption, 12984 ] % 0.45/0.88 (97,1) [12984,11]. true => ~_t74 | ~_t73 [ LRES, 12970, 1826, ~_t58 ] % 0.45/0.88 (1,1) [8,12]. _t16 => box 1 p0 [ Axiom T ] [ SNF++, 851, p0 ] % 0.45/0.88 (3,1) [10,12]. _t17 => ~box 1~ ~p0 [ SNF ] [ SNF++, 859, ~p0 ] % 0.45/0.88 (8,1) [31,12]. _t22 => ~box 1~ _t23 [ Axiom T ] [ SNF++, 861, _t23 ] % 0.45/0.88 (1,1) [32,12]. true => _t22 | ~_t21 | p0 [ Axiom T ] % 0.45/0.88 (10,1) [41,12]. true => ~_t25 | ~p0 [ SNF ] % 0.45/0.88 (1,1) [43,12]. _t26 => box 1 _t27 [ SNF ] [ SNF++, 855, _t27 ] % 0.45/0.88 (10,1) [46,12]. true => _t26 | ~_t25 [ SNF ] % 0.45/0.88 (1,1) [851,12]. _t16 => box 1 _t60 [ SNF++, 8 ] % 0.45/0.88 (1,1) [855,12]. _t26 => box 1 _t61 [ SNF++, 43 ] % 0.45/0.88 (3,1) [859,12]. _t17 => ~box 1~ _t63 [ SNF++, 10 ] % 0.45/0.88 (8,1) [861,12]. _t22 => ~box 1~ _t62 [ SNF++, 31 ] % 0.45/0.88 (1,1) [866,12]. true => ~_t64 | _t16 [ SNF++, 14 ] % 0.45/0.88 (1,1) [872,12]. true => ~_t65 | _t21 [ SNF++, 35 ] % 0.45/0.88 (1,1) [874,12]. true => ~_t69 | _t17 [ SNF++, 50 ] % 0.45/0.88 (10,1) [886,12]. true => ~_t71 | _t25 [ SNF++, 47 ] % 0.45/0.88 (10,1) [1477,12]. true => ~_t25 | _t22 | ~_t21 [ LRES, 41, 32, ~p0 ] % 0.45/0.88 (3,1) [1488,12]. true => ~_t17 | ~_t16 [ GEN1, 851, 859, 1426, _t60, _t63 ] % 0.45/0.88 (10,1) [1530,12]. true => ~_t71 | _t26 [ LRES, 46, 886, ~_t25 ] % 0.45/0.88 (3,1) [1645,12]. true => ~_t64 | ~_t17 [ LRES, 1488, 866, ~_t16 ] % 0.45/0.88 (8,1) [1848,12]. true => ~_t26 | ~_t22 [ GEN1, 855, 861, 1838, _t61, _t62 ] % 0.45/0.88 (3,1) [1885,12]. true => ~_t69 | ~_t64 [ LRES, 1645, 874, ~_t17 ] % 0.45/0.88 (10,1) [2115,12]. true => ~_t65 | ~_t25 | _t22 [ LRES, 1477, 872, ~_t21 ] % 0.45/0.88 (10,1) [2276,12]. true => ~_t65 | ~_t26 | ~_t25 [ LRES, 2115, 1848, _t22 ] % 0.45/0.88 (10,1) [2473,12]. true => ~_t71 | ~_t65 | ~_t26 [ LRES, 2276, 886, ~_t25 ] [ Backward Subsumption, 2796 ] % 0.45/0.88 (10,1) [2796,12]. true => ~_t71 | ~_t65 [ LRES, 2473, 1530, ~_t26 ] % 0.45/0.88 (1,1) [4,13]. _t16 => box 1 p0 [ SNF ] [ SNF++, 841, p0 ] % 0.45/0.88 (8,1) [28,13]. true => ~_t23 | p0 [ Axiom T ] % 0.45/0.88 (7,1) [29,13]. _t17 => ~box 1~ ~p0 [ Axiom T ] [ SNF++, 847, ~p0 ] % 0.45/0.88 (8,1) [30,13]. true => ~_t23 | _t17 [ Axiom T ] % 0.45/0.88 (1,1) [42,13]. true => ~_t27 | _t16 | ~p0 [ SNF ] % 0.45/0.88 (1,1) [841,13]. _t16 => box 1 _t60 [ SNF++, 4 ] % 0.45/0.88 (7,1) [847,13]. _t17 => ~box 1~ _t63 [ SNF++, 29 ] % 0.45/0.88 (1,1) [852,13]. true => ~_t60 | p0 [ SNF++, 8 ] % 0.45/0.88 (1,1) [856,13]. true => ~_t61 | _t27 [ SNF++, 43 ] % 0.45/0.88 (3,1) [860,13]. true => ~_t63 | ~p0 [ SNF++, 10 ] % 0.45/0.88 (8,1) [862,13]. true => ~_t62 | _t23 [ SNF++, 31 ] % 0.45/0.88 (3,1) [1426,13]. true => ~_t63 | ~_t60 [ LRES, 860, 852, ~p0 ] % 0.45/0.88 (7,1) [1490,13]. true => ~_t17 | ~_t16 [ GEN1, 841, 847, 1430, _t60, _t63 ] % 0.45/0.88 (8,1) [1595,13]. true => ~_t27 | ~_t23 | _t16 [ LRES, 42, 28, ~p0 ] [ Backward Subsumption, 1810 ] % 0.45/0.88 (8,1) [1728,13]. true => ~_t27 | ~_t23 | ~_t17 [ LRES, 1595, 1490, _t16 ] [ Backward Subsumption, 1810 ] % 0.45/0.88 (8,1) [1810,13]. true => ~_t27 | ~_t23 [ LRES, 1728, 30, ~_t17 ] % 0.45/0.88 (8,1) [1824,13]. true => ~_t62 | ~_t27 [ LRES, 1810, 862, ~_t23 ] % 0.45/0.88 (8,1) [1838,13]. true => ~_t62 | ~_t61 [ LRES, 1824, 856, ~_t27 ] % 0.45/0.88 (1,1) [842,14]. true => ~_t60 | p0 [ SNF++, 4 ] % 0.45/0.88 (7,1) [848,14]. true => ~_t63 | ~p0 [ SNF++, 29 ] % 0.45/0.88 (7,1) [1430,14]. true => ~_t63 | ~_t60 [ LRES, 848, 842, ~p0 ] % 0.45/0.88 % SZS output end Refutation % 0.45/0.88 % KSP exiting %------------------------------------------------------------------------------