%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP105_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n002.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.48s 0.62s % Output : Refutation 0.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP105_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.15/0.34 % Computer : n002.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Mon May 4 17:40:31 EDT 2026 % 0.15/0.34 % CPUTime : % 0.37/0.61 ----KSP format--- % 0.37/0.61 set(box,REF). % 0.37/0.61 usable(formulas). % 0.37/0.61 true. % 0.37/0.61 end_of_list. % 0.37/0.61 sos(formulas). % 0.37/0.61 ~ (( [] ( ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> p2 ) ) & ( [] ( ( [] ( ( ( [] ( $false ) | p1 ) -> [] ( [] ( $false ) | p1 ) ) ) -> ( [] ( $false ) | p1 ) ) ) -> ( [] ( $false ) | p1 ) ) & ( [] ( ( [] ( ( ( [] ( $false ) | p1 | p2 ) -> [] ( [] ( $false ) | p1 | p2 ) ) ) -> ( [] ( $false ) | p1 | p2 ) ) ) -> ( [] ( $false ) | p1 | p2 ) ) & ( [] ( ( [] ( ( ( [] ( $false ) | p1 | p2 | p3 ) -> [] ( [] ( $false ) | p1 | p2 | p3 ) ) ) -> ( [] ( $false ) | p1 | p2 | p3 ) ) ) -> ( [] ( $false ) | p1 | p2 | p3 ) ) & ( [] ( ( [] ( ( ( [] ( $false ) | p1 | p2 | p3 | p4 ) -> [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) ) ) -> ( [] ( $false ) | p1 | p2 | p3 | p4 ) ) ) -> ( [] ( $false ) | p1 | p2 | p3 | p4 ) ) & ( [] ( ( [] ( ( ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 ) -> [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 ) ) & ( [] ( ( [] ( ( ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 ) -> [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 ) ) & ( [] ( ( [] ( ( ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 ) -> [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 ) ) & ( [] ( ( [] ( ( ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) -> [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) ) & ( [] ( ( [] ( ( ( [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) | p1 ) -> [] ( [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) | p1 ) ) ) -> ( [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) | p1 ) ) ) -> ( [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) | p1 ) ) & ( [] ( ( [] ( ( ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) & ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> [] ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) ) ) ) -> [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) & ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> [] ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) ) ) ) ) ) -> ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) & ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> [] ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) ) ) ) ) ) -> ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) & ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> [] ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) ) ) ) ) ) -> ( ( [] ( ( [] ( ( p1 -> [] ( p1 ) ) ) -> p1 ) ) -> [] ( p1 ) ) | ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> [] ( p2 ) ) | ( [] ( ( [] ( ( p3 -> [] ( p3 ) ) ) -> p3 ) ) -> [] ( p3 ) ) ) ). % 0.37/0.61 end_of_list. % 0.37/0.61 ----------------- % 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.xZHxR53PfD/theBenchmark.ksp % 0.48/0.62 % 0.48/0.62 % SZS status Theorem % 0.48/0.62 % 0.48/0.62 ***************** % 0.48/0.62 FOUND PROOF 1 % 0.48/0.62 ***************** % 0.48/0.62 % SZS output start Refutation % 0.48/0.62 % 0.48/0.62 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.48/0.62 (1,1) [16,0]. _t1 => box 1 _t2 [ SNF ] [ Backward Subsumption, 506 ] % 0.48/0.62 (3,1) [25,0]. _t3 => ~box 1~ _t4 [ Axiom T ] [ SNF++, 578, _t4 ] % 0.48/0.62 (1,1) [27,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 505 ] % 0.48/0.62 (1,1) [59,0]. _t18 => box 1 _t19 [ SNF ] [ Backward Subsumption, 510 ] % 0.48/0.62 (1,1) [66,0]. true => _t18 | ~_t0 [ SNF ] [ Backward Subsumption, 502 ] % 0.48/0.62 (24,1) [71,0]. _t22 => ~box 1~ ~p2 [ SNF ] [ Backward Subsumption, 511 ] % 0.48/0.62 (1,1) [72,0]. true => _t22 | ~_t0 [ SNF ] [ Backward Subsumption, 499 ] % 0.48/0.62 (77,1) [149,0]. _t24 => ~box 1~ _t25 [ SNF ] [ SNF++, 586, _t25 ] % 0.48/0.62 (1,1) [151,0]. _t31 => box 1 _t18 [ SNF ] [ SNF++, 576, _t18 ] % 0.48/0.62 (1,1) [153,0]. true => _t31 | ~_t30 | _t3 [ SNF ] [ Backward Subsumption, 875 ] % 0.48/0.62 (1,1) [154,0]. true => _t30 | ~_t29 [ SNF ] [ Backward Subsumption, 979 ] % 0.48/0.62 (1,1) [155,0]. true => _t29 | _t24 | ~_t23 [ SNF ] [ Backward Subsumption, 509 ] % 0.48/0.62 (1,1) [156,0]. true => _t23 | ~_t0 [ SNF ] [ Backward Subsumption, 498 ] % 0.48/0.62 (1,1) [498,0]. true => _t23 [ Unit Resolution, 3, 156, _t0 ] [ Modal Level Pure Literal Elimination, _t23 ] % 0.48/0.62 (1,1) [499,0]. true => _t22 [ Unit Resolution, 3, 72, _t0 ] [ Modal Level Pure Literal Elimination, _t22 ] % 0.48/0.62 (1,1) [502,0]. true => _t18 [ Unit Resolution, 3, 66, _t0 ] [ Modal Level Pure Literal Elimination, _t18 ] % 0.48/0.62 (1,1) [505,0]. true => _t1 [ Unit Resolution, 3, 27, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 0.48/0.62 (1,1) [506,0]. true => box 1 _t2 [ LHS Unit Resolution, 505, 16, _t1 ] [ SNF++, 568, _t2 ] % 0.48/0.62 (1,1) [509,0]. true => _t29 | _t24 [ Unit Resolution, 498, 155, _t23 ] [ Backward Subsumption, 980 ] % 0.48/0.62 (1,1) [510,0]. true => box 1 _t19 [ LHS Unit Resolution, 502, 59, _t18 ] [ SNF++, 574, _t19 ] % 0.48/0.62 (24,1) [511,0]. true => ~box 1~ ~p2 [ LHS Unit Resolution, 499, 71, _t22 ] [ SNF++, 584, ~p2 ] % 0.48/0.62 (1,1) [568,0]. true => box 1 _t124 [ SNF++, 506 ] % 0.48/0.62 (1,1) [574,0]. true => box 1 _t114 [ SNF++, 510 ] % 0.48/0.62 (1,1) [576,0]. _t31 => box 1 _t113 [ SNF++, 151 ] [ Backward Subsumption, 978 ] % 0.48/0.62 (3,1) [578,0]. _t3 => ~box 1~ _t117 [ SNF++, 25 ] [ Backward Subsumption, 884 ] % 0.48/0.62 (24,1) [584,0]. true => ~box 1~ _t118 [ SNF++, 511 ] % 0.48/0.62 (77,1) [586,0]. _t24 => ~box 1~ _t129 [ SNF++, 149 ] [ Backward Subsumption, 981 ] % 0.48/0.62 (3,1) [874,0]. true => ~_t3 [ GEN1, 574, 578, 848, _t114, _t117 ] [ Modal Level Pure Literal Elimination, ~_t3 ] % 0.48/0.62 (3,1) [875,0]. true => _t31 | ~_t30 [ LRES, 874, 153, ~_t3 ] [ Backward Subsumption, 977 ] % 0.48/0.62 (24,1) [976,0]. true => ~_t31 [ GEN1, 568, 576, 584, 961, _t124, _t113, _t118 ] [ Modal Level Pure Literal Elimination, ~_t31 ] % 0.48/0.62 (24,1) [977,0]. true => ~_t30 [ Unit Resolution, 976, 875, _t31 ] [ Modal Level Pure Literal Elimination, ~_t30 ] % 0.48/0.62 (24,1) [979,0]. true => ~_t29 [ Unit Resolution, 977, 154, _t30 ] [ Modal Level Pure Literal Elimination, ~_t29 ] % 0.48/0.62 (24,1) [980,0]. true => _t24 [ Unit Resolution, 979, 509, _t29 ] [ Modal Level Pure Literal Elimination, _t24 ] % 0.48/0.62 (77,1) [981,0]. true => ~box 1~ _t129 [ LHS Unit Resolution, 980, 586, _t24 ] % 0.48/0.62 (77,1) [1198,0]. true => false [ GEN1, 574, 981, 1194, _t114, _t129 ] % 0.48/0.62 (3,1) [14,1]. _t3 => ~box 1~ _t4 [ SNF ] [ SNF++, 546, _t4 ] % 0.48/0.62 (1,1) [15,1]. true => _t3 | ~_t2 | p2 [ SNF ] % 0.48/0.62 (3,1) [18,1]. true => ~_t4 | ~p2 [ Axiom T ] % 0.48/0.62 (1,1) [19,1]. _t5 => box 1 _t6 [ Axiom T ] [ SNF++, 556, _t6 ] % 0.48/0.62 (3,1) [24,1]. true => _t5 | ~_t4 [ Axiom T ] % 0.48/0.62 (18,1) [57,1]. _t20 => ~box 1~ _t21 [ SNF ] [ SNF++, 552, _t21 ] % 0.48/0.62 (1,1) [58,1]. true => _t20 | ~_t19 | p2 [ SNF ] % 0.48/0.62 (1,1) [131,1]. _t26 => box 1 _t27 [ SNF ] [ SNF++, 560, _t27 ] % 0.48/0.62 (1,1) [132,1]. true => _t27 | ~_t26 [ Axiom T ] % 0.48/0.62 (1,1) [133,1]. _t28 => box 1 _t29 [ Axiom T ] [ SNF++, 562, _t29 ] % 0.48/0.62 (1,1) [134,1]. true => _t29 | ~_t28 [ Axiom T ] % 0.48/0.62 (1,1) [136,1]. _t31 => box 1 _t18 [ Axiom T ] [ SNF++, 564, _t18 ] % 0.48/0.62 (1,1) [138,1]. _t18 => box 1 _t19 [ Axiom T ] [ SNF++, 566, _t19 ] % 0.48/0.62 (1,1) [140,1]. true => _t31 | ~_t30 | _t3 [ Axiom T ] % 0.48/0.62 (1,1) [141,1]. true => _t30 | ~_t29 [ Axiom T ] % 0.48/0.62 (1,1) [142,1]. true => ~_t32 | _t18 [ Axiom T ] % 0.48/0.62 (72,1) [143,1]. _t33 => ~box 1~ _t3 [ Axiom T ] [ SNF++, 554, _t3 ] % 0.48/0.62 (1,1) [144,1]. true => _t33 | ~_t32 [ Axiom T ] % 0.48/0.62 (1,1) [145,1]. true => _t32 | _t28 | ~_t27 | _t4 [ Axiom T ] % 0.48/0.62 (77,1) [146,1]. true => _t26 | ~_t25 [ SNF ] % 0.48/0.62 (77,1) [147,1]. true => ~_t34 | _t32 | _t4 [ SNF ] % 0.48/0.62 (77,1) [148,1]. true => _t34 | ~_t25 [ SNF ] % 0.48/0.62 (3,1) [546,1]. _t3 => ~box 1~ _t117 [ SNF++, 14 ] % 0.48/0.62 (18,1) [552,1]. _t20 => ~box 1~ _t116 [ SNF++, 57 ] % 0.48/0.62 (72,1) [554,1]. _t33 => ~box 1~ _t120 [ SNF++, 143 ] % 0.48/0.62 (1,1) [556,1]. _t5 => box 1 _t115 [ SNF++, 19 ] % 0.48/0.62 (1,1) [560,1]. _t26 => box 1 _t123 [ SNF++, 131 ] % 0.48/0.62 (1,1) [562,1]. _t28 => box 1 _t119 [ SNF++, 133 ] % 0.48/0.62 (1,1) [564,1]. _t31 => box 1 _t113 [ SNF++, 136 ] % 0.48/0.62 (1,1) [566,1]. _t18 => box 1 _t114 [ SNF++, 138 ] % 0.48/0.62 (1,1) [569,1]. true => ~_t124 | _t2 [ SNF++, 506 ] % 0.48/0.62 (1,1) [575,1]. true => ~_t114 | _t19 [ SNF++, 510 ] % 0.48/0.62 (1,1) [577,1]. true => ~_t113 | _t18 [ SNF++, 151 ] [ Modal Level Pure Literal Elimination, ~_t113 ] % 0.48/0.62 (3,1) [579,1]. true => ~_t117 | _t4 [ SNF++, 25 ] [ Modal Level Pure Literal Elimination, ~_t117 ] % 0.48/0.62 (24,1) [585,1]. true => ~_t118 | ~p2 [ SNF++, 511 ] % 0.48/0.62 (77,1) [587,1]. true => ~_t129 | _t25 [ SNF++, 149 ] % 0.48/0.62 (24,1) [612,1]. true => ~_t118 | _t3 | ~_t2 [ LRES, 585, 15, ~p2 ] % 0.48/0.62 (3,1) [623,1]. true => _t20 | ~_t19 | ~_t4 [ LRES, 18, 58, ~p2 ] % 0.48/0.62 (3,1) [655,1]. true => _t32 | _t28 | ~_t27 | _t5 [ LRES, 24, 145, ~_t4 ] % 0.48/0.62 (77,1) [656,1]. true => ~_t34 | _t32 | _t5 [ LRES, 24, 147, ~_t4 ] % 0.48/0.62 (3,1) [657,1]. true => ~_t117 | _t5 [ LRES, 24, 579, ~_t4 ] [ Modal Level Pure Literal Elimination, ~_t117 ] % 0.48/0.62 (77,1) [683,1]. true => ~_t129 | _t34 [ LRES, 148, 587, ~_t25 ] % 0.48/0.62 (77,1) [688,1]. true => ~_t129 | _t26 [ LRES, 146, 587, ~_t25 ] % 0.48/0.62 (77,1) [713,1]. true => ~_t129 | _t27 [ LRES, 688, 132, _t26 ] % 0.48/0.62 (3,1) [732,1]. true => _t32 | _t28 | ~_t27 | _t20 | ~_t19 [ LRES, 623, 145, ~_t4 ] % 0.48/0.62 (77,1) [733,1]. true => ~_t34 | _t32 | _t20 | ~_t19 [ LRES, 623, 147, ~_t4 ] % 0.48/0.62 (3,1) [734,1]. true => ~_t117 | _t20 | ~_t19 [ LRES, 623, 579, ~_t4 ] [ Modal Level Pure Literal Elimination, ~_t117 ] % 0.48/0.62 (24,1) [745,1]. true => ~_t124 | ~_t118 | _t3 [ LRES, 612, 569, ~_t2 ] % 0.48/0.62 (3,1) [760,1]. true => ~_t117 | ~_t114 | _t20 [ LRES, 734, 575, ~_t19 ] [ Backward Subsumption, 848 ] % 0.48/0.62 (18,1) [833,1]. true => ~_t20 | ~_t5 [ GEN1, 556, 552, 830, _t115, _t116 ] % 0.48/0.62 (18,1) [842,1]. true => ~_t117 | ~_t20 [ LRES, 833, 657, ~_t5 ] [ Modal Level Pure Literal Elimination, ~_t117 ] % 0.48/0.62 (77,1) [843,1]. true => ~_t34 | _t32 | ~_t20 [ LRES, 833, 656, ~_t5 ] % 0.48/0.62 (18,1) [848,1]. true => ~_t117 | ~_t114 [ LRES, 842, 760, ~_t20 ] [ Modal Level Pure Literal Elimination, ~_t117 ] % 0.48/0.62 (72,1) [888,1]. true => ~_t33 | ~_t31 [ GEN1, 564, 554, 873, _t113, _t120 ] % 0.48/0.62 (77,1) [906,1]. true => ~_t114 | ~_t34 | _t32 | _t20 [ LRES, 733, 575, ~_t19 ] [ Backward Subsumption, 997 ] % 0.48/0.62 (18,1) [909,1]. true => _t32 | _t28 | ~_t27 | ~_t20 [ LRES, 655, 833, _t5 ] % 0.48/0.62 (3,1) [939,1]. true => ~_t18 | ~_t3 [ GEN1, 566, 546, 926, _t114, _t117 ] % 0.48/0.62 (24,1) [941,1]. true => ~_t124 | ~_t118 | ~_t18 [ LRES, 939, 745, ~_t3 ] % 0.48/0.62 (3,1) [943,1]. true => ~_t28 | ~_t3 [ GEN1, 562, 546, 937, _t119, _t117 ] % 0.48/0.62 (3,1) [948,1]. true => _t31 | ~_t30 | ~_t28 [ LRES, 943, 140, ~_t3 ] % 0.48/0.62 (24,1) [961,1]. true => ~_t124 | ~_t118 | ~_t113 [ LRES, 941, 577, ~_t18 ] [ Modal Level Pure Literal Elimination, ~_t113 ] % 0.48/0.62 (77,1) [997,1]. true => ~_t114 | ~_t34 | _t32 [ LRES, 906, 843, _t20 ] % 0.48/0.62 (77,1) [1001,1]. true => ~_t114 | ~_t34 | _t33 [ LRES, 997, 144, _t32 ] % 0.48/0.62 (3,1) [1077,1]. true => ~_t114 | _t32 | _t28 | ~_t27 | _t20 [ LRES, 732, 575, ~_t19 ] [ Backward Subsumption, 1099 ] % 0.48/0.62 (18,1) [1099,1]. true => ~_t114 | _t32 | _t28 | ~_t27 [ LRES, 1077, 909, _t20 ] % 0.48/0.62 (77,1) [1100,1]. true => ~_t129 | ~_t114 | _t32 | _t28 [ LRES, 1099, 713, ~_t27 ] [ Backward Subsumption, 1194 ] % 0.48/0.62 (77,1) [1101,1]. true => ~_t129 | ~_t114 | _t32 | _t29 [ LRES, 1100, 134, _t28 ] [ Backward Subsumption, 1194 ] % 0.48/0.62 (77,1) [1103,1]. true => ~_t129 | ~_t114 | _t32 | _t31 | ~_t30 [ LRES, 1100, 948, _t28 ] [ Backward Subsumption, 1145 ] % 0.48/0.62 (77,1) [1105,1]. true => ~_t129 | ~_t114 | _t32 | _t30 [ LRES, 1101, 141, _t29 ] [ Backward Subsumption, 1194 ] % 0.48/0.62 (77,1) [1145,1]. true => ~_t129 | ~_t114 | _t32 | _t31 [ LRES, 1103, 1105, ~_t30 ] [ Backward Subsumption, 1194 ] % 0.48/0.62 (77,1) [1149,1]. true => ~_t129 | ~_t114 | ~_t33 | _t32 [ LRES, 1145, 888, _t31 ] [ Backward Subsumption, 1189 ] % 0.48/0.62 (72,1) [1182,1]. true => ~_t33 | ~_t26 | ~_t18 [ GEN1, 560, 566, 554, 1179, _t123, _t114, _t120 ] % 0.48/0.62 (72,1) [1186,1]. true => ~_t33 | ~_t32 | ~_t26 [ LRES, 1182, 142, ~_t18 ] % 0.48/0.62 (77,1) [1187,1]. true => ~_t129 | ~_t33 | ~_t32 [ LRES, 1186, 688, ~_t26 ] % 0.48/0.62 (77,1) [1189,1]. true => ~_t129 | ~_t114 | ~_t33 [ LRES, 1187, 1149, ~_t32 ] [ Backward Subsumption, 1194 ] % 0.48/0.62 (77,1) [1193,1]. true => ~_t129 | ~_t114 | ~_t34 [ LRES, 1189, 1001, ~_t33 ] [ Backward Subsumption, 1194 ] % 0.48/0.62 (77,1) [1194,1]. true => ~_t129 | ~_t114 [ LRES, 1193, 683, ~_t34 ] % 0.48/0.62 (3,1) [4,2]. true => ~_t4 | ~p2 [ SNF ] % 0.48/0.62 (1,1) [8,2]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 528, _t6 ] % 0.48/0.62 (1,1) [10,2]. _t7 => box 1 p2 [ Axiom T ] [ SNF++, 530, p2 ] % 0.48/0.62 (1,1) [12,2]. true => _t7 | ~_t6 | ~p2 [ Axiom T ] % 0.48/0.62 (3,1) [13,2]. true => _t5 | ~_t4 [ SNF ] % 0.48/0.62 (18,1) [54,2]. true => ~_t21 | p2 [ SNF ] % 0.48/0.62 (17,1) [55,2]. _t22 => ~box 1~ ~p2 [ SNF ] [ SNF++, 538, ~p2 ] % 0.48/0.62 (18,1) [56,2]. true => _t22 | ~_t21 [ SNF ] % 0.48/0.62 (1,1) [108,2]. _t28 => box 1 _t29 [ SNF ] [ SNF++, 532, _t29 ] % 0.48/0.62 (65,1) [113,2]. _t20 => ~box 1~ _t21 [ Axiom T ] [ SNF++, 540, _t21 ] % 0.48/0.62 (1,1) [114,2]. true => _t20 | ~_t19 | p2 [ Axiom T ] % 0.48/0.62 (1,1) [115,2]. true => ~_t29 | _t19 [ Axiom T ] % 0.48/0.62 (1,1) [118,2]. _t18 => box 1 _t19 [ Axiom T ] [ SNF++, 536, _t19 ] % 0.48/0.62 (68,1) [124,2]. _t3 => ~box 1~ _t4 [ Axiom T ] [ SNF++, 542, _t4 ] % 0.48/0.62 (1,1) [127,2]. true => ~_t32 | _t18 [ SNF ] % 0.48/0.62 (1,1) [130,2]. true => _t32 | _t28 | ~_t27 | _t4 [ SNF ] % 0.48/0.62 (1,1) [528,2]. _t5 => box 1 _t115 [ SNF++, 8 ] % 0.48/0.62 (1,1) [530,2]. _t7 => box 1 _t112 [ SNF++, 10 ] % 0.48/0.62 (1,1) [532,2]. _t28 => box 1 _t119 [ SNF++, 108 ] % 0.48/0.62 (1,1) [536,2]. _t18 => box 1 _t114 [ SNF++, 118 ] % 0.48/0.62 (17,1) [538,2]. _t22 => ~box 1~ _t118 [ SNF++, 55 ] % 0.48/0.62 (65,1) [540,2]. _t20 => ~box 1~ _t116 [ SNF++, 113 ] % 0.48/0.62 (68,1) [542,2]. _t3 => ~box 1~ _t117 [ SNF++, 124 ] % 0.48/0.62 (3,1) [547,2]. true => ~_t117 | _t4 [ SNF++, 14 ] % 0.48/0.62 (18,1) [553,2]. true => ~_t116 | _t21 [ SNF++, 57 ] % 0.48/0.62 (72,1) [555,2]. true => ~_t120 | _t3 [ SNF++, 143 ] % 0.48/0.62 (1,1) [557,2]. true => ~_t115 | _t6 [ SNF++, 19 ] % 0.48/0.62 (1,1) [561,2]. true => ~_t123 | _t27 [ SNF++, 131 ] % 0.48/0.62 (1,1) [563,2]. true => ~_t119 | _t29 [ SNF++, 133 ] % 0.48/0.62 (1,1) [565,2]. true => ~_t113 | _t18 [ SNF++, 136 ] % 0.48/0.62 (1,1) [567,2]. true => ~_t114 | _t19 [ SNF++, 138 ] % 0.48/0.62 (3,1) [607,2]. true => _t20 | ~_t19 | ~_t4 [ LRES, 4, 114, ~p2 ] % 0.48/0.62 (3,1) [659,2]. true => _t32 | _t28 | ~_t27 | _t5 [ LRES, 13, 130, ~_t4 ] % 0.48/0.62 (3,1) [660,2]. true => ~_t117 | _t5 [ LRES, 13, 547, ~_t4 ] % 0.48/0.62 (18,1) [679,2]. true => ~_t116 | _t22 [ LRES, 56, 553, ~_t21 ] % 0.48/0.62 (17,1) [699,2]. true => ~_t22 | ~_t7 [ GEN1, 530, 538, 610, _t112, _t118 ] % 0.48/0.62 (18,1) [749,2]. true => ~_t21 | _t7 | ~_t6 [ LRES, 12, 54, ~p2 ] % 0.48/0.62 (3,1) [763,2]. true => _t32 | _t28 | ~_t27 | _t20 | ~_t19 [ LRES, 607, 130, ~_t4 ] % 0.48/0.62 (3,1) [764,2]. true => ~_t117 | _t20 | ~_t19 [ LRES, 607, 547, ~_t4 ] % 0.48/0.62 (18,1) [782,2]. true => ~_t115 | ~_t21 | _t7 [ LRES, 749, 557, ~_t6 ] % 0.48/0.62 (3,1) [790,2]. true => ~_t117 | ~_t29 | _t20 [ LRES, 764, 115, ~_t19 ] [ Backward Subsumption, 925 ] % 0.48/0.62 (3,1) [791,2]. true => ~_t117 | ~_t114 | _t20 [ LRES, 764, 567, ~_t19 ] [ Backward Subsumption, 926 ] % 0.48/0.62 (18,1) [798,2]. true => ~_t115 | ~_t22 | ~_t21 [ LRES, 782, 699, _t7 ] % 0.48/0.62 (18,1) [804,2]. true => ~_t116 | ~_t115 | ~_t22 [ LRES, 798, 553, ~_t21 ] [ Backward Subsumption, 830 ] % 0.48/0.62 (18,1) [830,2]. true => ~_t116 | ~_t115 [ LRES, 804, 679, ~_t22 ] % 0.48/0.62 (68,1) [863,2]. true => ~_t18 | ~_t3 [ GEN1, 536, 542, 837, _t114, _t117 ] % 0.48/0.62 (72,1) [869,2]. true => ~_t120 | ~_t18 [ LRES, 863, 555, ~_t3 ] % 0.48/0.62 (68,1) [870,2]. true => ~_t28 | ~_t3 [ GEN1, 532, 542, 862, _t119, _t117 ] % 0.48/0.62 (72,1) [872,2]. true => ~_t120 | ~_t32 [ LRES, 869, 127, ~_t18 ] % 0.48/0.62 (72,1) [873,2]. true => ~_t120 | ~_t113 [ LRES, 869, 565, ~_t18 ] % 0.48/0.62 (72,1) [877,2]. true => ~_t120 | ~_t28 [ LRES, 870, 555, ~_t3 ] % 0.48/0.62 (65,1) [918,2]. true => ~_t20 | ~_t5 [ GEN1, 528, 540, 914, _t115, _t116 ] % 0.48/0.62 (65,1) [919,2]. true => ~_t117 | ~_t20 [ LRES, 918, 660, ~_t5 ] % 0.48/0.62 (65,1) [925,2]. true => ~_t117 | ~_t29 [ LRES, 919, 790, ~_t20 ] % 0.48/0.62 (65,1) [926,2]. true => ~_t117 | ~_t114 [ LRES, 919, 791, ~_t20 ] % 0.48/0.62 (65,1) [937,2]. true => ~_t119 | ~_t117 [ LRES, 925, 563, ~_t29 ] % 0.48/0.62 (65,1) [998,2]. true => _t32 | _t28 | ~_t27 | ~_t20 [ LRES, 659, 918, _t5 ] % 0.48/0.62 (3,1) [1140,2]. true => ~_t114 | _t32 | _t28 | ~_t27 | _t20 [ LRES, 763, 567, ~_t19 ] [ Backward Subsumption, 1173 ] % 0.48/0.62 (65,1) [1173,2]. true => ~_t114 | _t32 | _t28 | ~_t27 [ LRES, 1140, 998, _t20 ] % 0.48/0.62 (65,1) [1174,2]. true => ~_t123 | ~_t114 | _t32 | _t28 [ LRES, 1173, 561, ~_t27 ] % 0.48/0.62 (72,1) [1175,2]. true => ~_t123 | ~_t120 | ~_t114 | _t32 [ LRES, 1174, 877, _t28 ] [ Backward Subsumption, 1179 ] % 0.48/0.62 (72,1) [1179,2]. true => ~_t123 | ~_t120 | ~_t114 [ LRES, 1175, 872, _t32 ] % 0.48/0.62 (1,1) [5,3]. _t7 => box 1 p2 [ SNF ] [ SNF++, 514, p2 ] % 0.48/0.62 (1,1) [7,3]. true => _t7 | ~_t6 | ~p2 [ SNF ] % 0.48/0.62 (65,1) [76,3]. _t20 => ~box 1~ _t21 [ SNF ] [ SNF++, 522, _t21 ] % 0.48/0.62 (1,1) [77,3]. true => _t20 | ~_t19 | p2 [ SNF ] % 0.48/0.62 (1,1) [78,3]. true => ~_t29 | _t19 [ SNF ] % 0.48/0.62 (65,1) [110,3]. true => ~_t21 | p2 [ Axiom T ] % 0.48/0.62 (64,1) [111,3]. _t22 => ~box 1~ ~p2 [ Axiom T ] [ SNF++, 526, ~p2 ] % 0.48/0.62 (65,1) [112,3]. true => _t22 | ~_t21 [ Axiom T ] % 0.48/0.62 (68,1) [120,3]. true => ~_t4 | ~p2 [ Axiom T ] % 0.48/0.62 (1,1) [121,3]. _t5 => box 1 _t6 [ Axiom T ] [ SNF++, 520, _t6 ] % 0.48/0.62 (68,1) [123,3]. true => _t5 | ~_t4 [ Axiom T ] % 0.48/0.62 (1,1) [514,3]. _t7 => box 1 _t112 [ SNF++, 5 ] % 0.48/0.62 (1,1) [520,3]. _t5 => box 1 _t115 [ SNF++, 121 ] % 0.48/0.62 (65,1) [522,3]. _t20 => ~box 1~ _t116 [ SNF++, 76 ] % 0.48/0.62 (64,1) [526,3]. _t22 => ~box 1~ _t118 [ SNF++, 111 ] % 0.48/0.62 (1,1) [529,3]. true => ~_t115 | _t6 [ SNF++, 8 ] % 0.48/0.62 (1,1) [531,3]. true => ~_t112 | p2 [ SNF++, 10 ] % 0.48/0.62 (1,1) [533,3]. true => ~_t119 | _t29 [ SNF++, 108 ] % 0.48/0.62 (1,1) [537,3]. true => ~_t114 | _t19 [ SNF++, 118 ] % 0.48/0.62 (17,1) [539,3]. true => ~_t118 | ~p2 [ SNF++, 55 ] % 0.48/0.62 (65,1) [541,3]. true => ~_t116 | _t21 [ SNF++, 113 ] % 0.48/0.62 (68,1) [543,3]. true => ~_t117 | _t4 [ SNF++, 124 ] % 0.48/0.62 (17,1) [610,3]. true => ~_t118 | ~_t112 [ LRES, 539, 531, ~p2 ] % 0.48/0.62 (68,1) [621,3]. true => _t20 | ~_t19 | ~_t4 [ LRES, 120, 77, ~p2 ] % 0.48/0.62 (65,1) [661,3]. true => ~_t116 | _t22 [ LRES, 112, 541, ~_t21 ] % 0.48/0.62 (68,1) [682,3]. true => ~_t117 | _t5 [ LRES, 123, 543, ~_t4 ] % 0.48/0.62 (64,1) [706,3]. true => ~_t22 | ~_t7 [ GEN1, 514, 526, 638, _t112, _t118 ] % 0.48/0.62 (65,1) [738,3]. true => ~_t21 | _t7 | ~_t6 [ LRES, 7, 110, ~p2 ] % 0.48/0.62 (68,1) [744,3]. true => ~_t117 | _t20 | ~_t19 [ LRES, 621, 543, ~_t4 ] % 0.48/0.62 (68,1) [754,3]. true => ~_t117 | ~_t29 | _t20 [ LRES, 744, 78, ~_t19 ] [ Backward Subsumption, 836 ] % 0.48/0.62 (68,1) [755,3]. true => ~_t117 | ~_t114 | _t20 [ LRES, 744, 537, ~_t19 ] [ Backward Subsumption, 837 ] % 0.48/0.62 (65,1) [784,3]. true => ~_t115 | ~_t21 | _t7 [ LRES, 738, 529, ~_t6 ] % 0.48/0.62 (65,1) [824,3]. true => ~_t115 | ~_t22 | ~_t21 [ LRES, 784, 706, _t7 ] % 0.48/0.62 (65,1) [829,3]. true => ~_t20 | ~_t5 [ GEN1, 520, 522, 822, _t115, _t116 ] % 0.48/0.62 (68,1) [831,3]. true => ~_t117 | ~_t20 [ LRES, 829, 682, ~_t5 ] % 0.48/0.62 (68,1) [836,3]. true => ~_t117 | ~_t29 [ LRES, 831, 754, ~_t20 ] % 0.48/0.62 (68,1) [837,3]. true => ~_t117 | ~_t114 [ LRES, 831, 755, ~_t20 ] % 0.48/0.62 (68,1) [862,3]. true => ~_t119 | ~_t117 [ LRES, 836, 533, ~_t29 ] % 0.48/0.62 (65,1) [897,3]. true => ~_t116 | ~_t115 | ~_t22 [ LRES, 824, 541, ~_t21 ] [ Backward Subsumption, 914 ] % 0.48/0.62 (65,1) [914,3]. true => ~_t116 | ~_t115 [ LRES, 897, 661, ~_t22 ] % 0.48/0.62 (65,1) [73,4]. true => ~_t21 | p2 [ SNF ] % 0.48/0.62 (64,1) [74,4]. _t22 => ~box 1~ ~p2 [ SNF ] [ SNF++, 588, ~p2 ] % 0.48/0.62 (65,1) [75,4]. true => _t22 | ~_t21 [ SNF ] % 0.48/0.62 (1,1) [101,4]. _t7 => box 1 p2 [ Axiom T ] [ SNF++, 596, p2 ] % 0.48/0.62 (1,1) [103,4]. true => _t7 | ~_t6 | ~p2 [ Axiom T ] % 0.48/0.62 (1,1) [515,4]. true => ~_t112 | p2 [ SNF++, 5 ] % 0.48/0.62 (1,1) [521,4]. true => ~_t115 | _t6 [ SNF++, 121 ] % 0.48/0.62 (65,1) [523,4]. true => ~_t116 | _t21 [ SNF++, 76 ] % 0.48/0.62 (64,1) [527,4]. true => ~_t118 | ~p2 [ SNF++, 111 ] % 0.48/0.62 (64,1) [588,4]. _t22 => ~box 1~ _t118 [ SNF++, 74 ] % 0.48/0.62 (1,1) [596,4]. _t7 => box 1 _t112 [ SNF++, 101 ] % 0.48/0.62 (65,1) [615,4]. true => ~_t116 | _t22 [ LRES, 75, 523, ~_t21 ] % 0.48/0.62 (64,1) [638,4]. true => ~_t118 | ~_t112 [ LRES, 527, 515, ~p2 ] % 0.48/0.62 (64,1) [665,4]. true => ~_t22 | ~_t7 [ GEN1, 596, 588, 631, _t112, _t118 ] % 0.48/0.62 (65,1) [721,4]. true => ~_t21 | _t7 | ~_t6 [ LRES, 103, 73, ~p2 ] % 0.48/0.62 (65,1) [762,4]. true => ~_t115 | ~_t21 | _t7 [ LRES, 721, 521, ~_t6 ] % 0.48/0.62 (65,1) [808,4]. true => ~_t115 | ~_t22 | ~_t21 [ LRES, 762, 665, _t7 ] % 0.48/0.62 (65,1) [821,4]. true => ~_t116 | ~_t115 | ~_t22 [ LRES, 808, 523, ~_t21 ] [ Backward Subsumption, 822 ] % 0.48/0.62 (65,1) [822,4]. true => ~_t116 | ~_t115 [ LRES, 821, 615, ~_t22 ] % 0.48/0.62 (64,1) [589,5]. true => ~_t118 | ~p2 [ SNF++, 74 ] % 0.48/0.62 (1,1) [597,5]. true => ~_t112 | p2 [ SNF++, 101 ] % 0.48/0.62 (64,1) [631,5]. true => ~_t118 | ~_t112 [ LRES, 589, 597, ~p2 ] % 0.48/0.62 % SZS output end Refutation % 0.48/0.62 % KSP exiting %------------------------------------------------------------------------------