%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP087_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n016.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:58 PM UTC 2026 % Result : Theorem 0.36s 0.61s % Output : Refutation 0.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP087_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : run_ksp %s % 0.15/0.34 % Computer : n016.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:24:21 EDT 2026 % 0.15/0.34 % CPUTime : % 0.36/0.60 ----KSP format--- % 0.36/0.60 set(box,SER). % 0.36/0.60 usable(formulas). % 0.36/0.60 true. % 0.36/0.60 end_of_list. % 0.36/0.60 sos(formulas). % 0.36/0.60 ~ (( [] ( ( [] ( ( [] ( ( 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.36/0.60 end_of_list. % 0.36/0.60 ----------------- % 0.36/0.60 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/sandbox2/tmp/tmp.MQMlZv2b74/theBenchmark.ksp % 0.36/0.61 % 0.36/0.61 % SZS status Theorem % 0.36/0.61 % 0.36/0.61 ***************** % 0.36/0.61 FOUND PROOF 1 % 0.36/0.61 ***************** % 0.36/0.61 % SZS output start Refutation % 0.36/0.61 % 0.36/0.61 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.36/0.61 (1,1) [13,0]. _t1 => box 1 _t2 [ SNF ] [ Backward Subsumption, 416 ] % 0.36/0.61 (1,1) [15,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 414 ] % 0.36/0.61 (1,1) [37,0]. _t18 => box 1 _t19 [ SNF ] [ Backward Subsumption, 424 ] % 0.36/0.61 (1,1) [39,0]. true => _t18 | ~_t0 [ SNF ] [ Backward Subsumption, 411 ] % 0.36/0.61 (24,1) [44,0]. _t22 => ~box 1~ ~p2 [ SNF ] [ Backward Subsumption, 420 ] % 0.36/0.61 (1,1) [45,0]. true => _t22 | ~_t0 [ SNF ] [ Backward Subsumption, 408 ] % 0.36/0.61 (77,1) [109,0]. _t24 => ~box 1~ _t25 [ SNF ] [ SNF++, 515, _t25 ] % 0.36/0.61 (1,1) [116,0]. _t31 => box 1 _t18 [ SNF ] [ SNF++, 499, _t18 ] % 0.36/0.61 (89,1) [118,0]. _t3 => ~box 1~ _t4 [ SNF ] [ SNF++, 519, _t4 ] % 0.36/0.61 (1,1) [119,0]. true => _t31 | ~_t30 | _t3 [ SNF ] [ Backward Subsumption, 645 ] % 0.36/0.61 (1,1) [120,0]. true => _t30 | ~_t29 [ SNF ] [ Backward Subsumption, 702 ] % 0.36/0.61 (1,1) [121,0]. true => _t29 | _t24 | ~_t23 [ SNF ] [ Backward Subsumption, 421 ] % 0.36/0.61 (1,1) [122,0]. true => _t23 | ~_t0 [ SNF ] [ Backward Subsumption, 407 ] % 0.36/0.61 (1,1) [407,0]. true => _t23 [ Unit Resolution, 3, 122, _t0 ] [ Modal Level Pure Literal Elimination, _t23 ] % 0.36/0.61 (1,1) [408,0]. true => _t22 [ Unit Resolution, 3, 45, _t0 ] [ Modal Level Pure Literal Elimination, _t22 ] % 0.36/0.61 (1,1) [411,0]. true => _t18 [ Unit Resolution, 3, 39, _t0 ] [ Modal Level Pure Literal Elimination, _t18 ] % 0.36/0.61 (1,1) [414,0]. true => _t1 [ Unit Resolution, 3, 15, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 0.36/0.61 (1,1) [416,0]. true => box 1 _t2 [ LHS Unit Resolution, 414, 13, _t1 ] [ SNF++, 491, _t2 ] % 0.36/0.61 (24,1) [420,0]. true => ~box 1~ ~p2 [ LHS Unit Resolution, 408, 44, _t22 ] [ SNF++, 513, ~p2 ] % 0.36/0.61 (1,1) [421,0]. true => _t29 | _t24 [ Unit Resolution, 407, 121, _t23 ] [ Backward Subsumption, 703 ] % 0.36/0.61 (1,1) [424,0]. true => box 1 _t19 [ LHS Unit Resolution, 411, 37, _t18 ] [ SNF++, 497, _t19 ] % 0.36/0.61 (1,1) [491,0]. true => box 1 _t151 [ SNF++, 416 ] % 0.36/0.61 (1,1) [497,0]. true => box 1 _t146 [ SNF++, 424 ] % 0.36/0.61 (1,1) [499,0]. _t31 => box 1 _t140 [ SNF++, 116 ] [ Backward Subsumption, 701 ] % 0.36/0.61 (24,1) [513,0]. true => ~box 1~ _t144 [ SNF++, 420 ] % 0.36/0.61 (77,1) [515,0]. _t24 => ~box 1~ _t156 [ SNF++, 109 ] [ Backward Subsumption, 704 ] % 0.36/0.61 (89,1) [519,0]. _t3 => ~box 1~ _t143 [ SNF++, 118 ] [ Backward Subsumption, 646 ] % 0.36/0.61 (89,1) [644,0]. true => ~_t3 [ GEN1, 497, 519, 641, _t146, _t143 ] [ Modal Level Pure Literal Elimination, ~_t3 ] % 0.36/0.61 (89,1) [645,0]. true => _t31 | ~_t30 [ Unit Resolution, 644, 119, _t3 ] [ Backward Subsumption, 699 ] % 0.36/0.61 (24,1) [698,0]. true => ~_t31 [ GEN1, 491, 499, 513, 693, _t151, _t140, _t144 ] [ Modal Level Pure Literal Elimination, ~_t31 ] % 0.36/0.61 (89,1) [699,0]. true => ~_t30 [ Unit Resolution, 698, 645, _t31 ] [ Modal Level Pure Literal Elimination, ~_t30 ] % 0.36/0.61 (89,1) [702,0]. true => ~_t29 [ Unit Resolution, 699, 120, _t30 ] [ Modal Level Pure Literal Elimination, ~_t29 ] % 0.36/0.61 (89,1) [703,0]. true => _t24 [ Unit Resolution, 702, 421, _t29 ] [ Modal Level Pure Literal Elimination, _t24 ] % 0.36/0.61 (77,1) [704,0]. true => ~box 1~ _t156 [ LHS Unit Resolution, 703, 515, _t24 ] % 0.36/0.61 (77,1) [740,0]. true => false [ GEN1, 497, 704, 739, _t146, _t156 ] % 0.36/0.61 (3,1) [11,1]. _t3 => ~box 1~ _t4 [ SNF ] [ SNF++, 469, _t4 ] % 0.36/0.61 (1,1) [12,1]. true => _t3 | ~_t2 | p2 [ SNF ] % 0.36/0.61 (18,1) [35,1]. _t20 => ~box 1~ _t21 [ SNF ] [ SNF++, 475, _t21 ] % 0.36/0.61 (1,1) [36,1]. true => _t20 | ~_t19 | p2 [ SNF ] % 0.36/0.61 (1,1) [79,1]. _t26 => box 1 _t27 [ SNF ] [ SNF++, 485, _t27 ] % 0.36/0.61 (1,1) [80,1]. _t26 => ~box 1~ _t27 [ Axiom SER ] [ SNF++, 477, _t27 ] % 0.36/0.61 (77,1) [81,1]. true => _t26 | ~_t25 [ SNF ] % 0.36/0.61 (1,1) [87,1]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 487, _t19 ] % 0.36/0.61 (1,1) [88,1]. _t18 => ~box 1~ _t19 [ Axiom SER ] [ SNF++, 479, _t19 ] % 0.36/0.61 (77,1) [89,1]. true => ~_t32 | _t18 [ SNF ] % 0.36/0.61 (76,1) [98,1]. _t33 => ~box 1~ _t3 [ SNF ] [ SNF++, 481, _t3 ] % 0.36/0.61 (77,1) [99,1]. true => _t33 | ~_t32 [ SNF ] % 0.36/0.61 (77,1) [100,1]. true => ~_t4 | ~p2 [ SNF ] % 0.36/0.61 (1,1) [104,1]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 489, _t6 ] % 0.36/0.61 (1,1) [105,1]. _t5 => ~box 1~ _t6 [ Axiom SER ] [ SNF++, 483, _t6 ] % 0.36/0.61 (77,1) [106,1]. true => _t5 | ~_t4 [ SNF ] % 0.36/0.61 (77,1) [107,1]. true => ~_t34 | _t32 | _t4 [ SNF ] % 0.36/0.61 (77,1) [108,1]. true => _t34 | ~_t25 [ SNF ] % 0.36/0.61 (3,1) [469,1]. _t3 => ~box 1~ _t143 [ SNF++, 11 ] % 0.36/0.61 (18,1) [475,1]. _t20 => ~box 1~ _t142 [ SNF++, 35 ] % 0.36/0.61 (76,1) [481,1]. _t33 => ~box 1~ _t147 [ SNF++, 98 ] % 0.36/0.61 (1,1) [485,1]. _t26 => box 1 _t150 [ SNF++, 79 ] % 0.36/0.61 (1,1) [487,1]. _t18 => box 1 _t146 [ SNF++, 87 ] % 0.36/0.61 (1,1) [489,1]. _t5 => box 1 _t141 [ SNF++, 104 ] % 0.36/0.61 (1,1) [492,1]. true => ~_t151 | _t2 [ SNF++, 416 ] % 0.36/0.61 (1,1) [498,1]. true => ~_t146 | _t19 [ SNF++, 424 ] % 0.36/0.61 (1,1) [500,1]. true => ~_t140 | _t18 [ SNF++, 116 ] [ Modal Level Pure Literal Elimination, ~_t140 ] % 0.36/0.61 (24,1) [514,1]. true => ~_t144 | ~p2 [ SNF++, 420 ] % 0.36/0.61 (77,1) [516,1]. true => ~_t156 | _t25 [ SNF++, 109 ] % 0.36/0.61 (89,1) [520,1]. true => ~_t143 | _t4 [ SNF++, 118 ] [ Modal Level Pure Literal Elimination, ~_t143 ] % 0.36/0.61 (77,1) [542,1]. true => ~_t156 | _t34 [ LRES, 108, 516, ~_t25 ] % 0.36/0.61 (77,1) [552,1]. true => ~_t156 | _t26 [ LRES, 81, 516, ~_t25 ] % 0.36/0.61 (24,1) [565,1]. true => ~_t144 | _t3 | ~_t2 [ LRES, 514, 12, ~p2 ] % 0.36/0.61 (77,1) [572,1]. true => _t20 | ~_t19 | ~_t4 [ LRES, 100, 36, ~p2 ] % 0.36/0.61 (77,1) [577,1]. true => ~_t34 | _t32 | _t5 [ LRES, 106, 107, ~_t4 ] % 0.36/0.61 (89,1) [578,1]. true => ~_t143 | _t5 [ LRES, 106, 520, ~_t4 ] [ Modal Level Pure Literal Elimination, ~_t143 ] % 0.36/0.61 (77,1) [592,1]. true => ~_t34 | _t32 | _t20 | ~_t19 [ LRES, 572, 107, ~_t4 ] % 0.36/0.61 (89,1) [593,1]. true => ~_t143 | _t20 | ~_t19 [ LRES, 572, 520, ~_t4 ] [ Modal Level Pure Literal Elimination, ~_t143 ] % 0.36/0.61 (24,1) [597,1]. true => ~_t151 | ~_t144 | _t3 [ LRES, 565, 492, ~_t2 ] % 0.36/0.61 (89,1) [598,1]. true => ~_t146 | ~_t143 | _t20 [ LRES, 593, 498, ~_t19 ] [ Backward Subsumption, 641 ] % 0.36/0.61 (77,1) [634,1]. true => ~_t146 | ~_t34 | _t32 | _t20 [ LRES, 592, 498, ~_t19 ] [ Backward Subsumption, 652 ] % 0.36/0.61 (18,1) [635,1]. true => ~_t20 | ~_t5 [ GEN1, 489, 475, 633, _t141, _t142 ] % 0.36/0.61 (89,1) [637,1]. true => ~_t143 | ~_t20 [ LRES, 635, 578, ~_t5 ] [ Modal Level Pure Literal Elimination, ~_t143 ] % 0.36/0.61 (77,1) [638,1]. true => ~_t34 | _t32 | ~_t20 [ LRES, 635, 577, ~_t5 ] % 0.36/0.61 (89,1) [641,1]. true => ~_t146 | ~_t143 [ LRES, 637, 598, ~_t20 ] [ Modal Level Pure Literal Elimination, ~_t143 ] % 0.36/0.61 (77,1) [652,1]. true => ~_t146 | ~_t34 | _t32 [ LRES, 634, 638, _t20 ] % 0.36/0.61 (77,1) [656,1]. true => ~_t146 | ~_t34 | _t33 [ LRES, 652, 99, _t32 ] % 0.36/0.61 (3,1) [684,1]. true => ~_t18 | ~_t3 [ GEN1, 487, 469, 681, _t146, _t143 ] % 0.36/0.61 (24,1) [687,1]. true => ~_t151 | ~_t144 | ~_t18 [ LRES, 684, 597, ~_t3 ] % 0.36/0.61 (24,1) [693,1]. true => ~_t151 | ~_t144 | ~_t140 [ LRES, 687, 500, ~_t18 ] [ Modal Level Pure Literal Elimination, ~_t140 ] % 0.36/0.61 (76,1) [730,1]. true => ~_t33 | ~_t26 | ~_t18 [ GEN1, 485, 487, 481, 728, _t150, _t146, _t147 ] % 0.36/0.61 (77,1) [731,1]. true => ~_t33 | ~_t32 | ~_t26 [ LRES, 730, 89, ~_t18 ] % 0.36/0.61 (77,1) [732,1]. true => ~_t156 | ~_t33 | ~_t32 [ LRES, 731, 552, ~_t26 ] % 0.36/0.61 (77,1) [735,1]. true => ~_t156 | ~_t146 | ~_t34 | ~_t33 [ LRES, 732, 652, ~_t32 ] [ Backward Subsumption, 737 ] % 0.36/0.61 (77,1) [737,1]. true => ~_t156 | ~_t146 | ~_t34 [ LRES, 735, 656, ~_t33 ] [ Backward Subsumption, 739 ] % 0.36/0.61 (77,1) [739,1]. true => ~_t156 | ~_t146 [ LRES, 737, 542, ~_t34 ] % 0.36/0.61 (3,1) [4,2]. true => ~_t4 | ~p2 [ SNF ] % 0.36/0.61 (1,1) [8,2]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 445, _t6 ] % 0.36/0.61 (3,1) [10,2]. true => _t5 | ~_t4 [ SNF ] % 0.36/0.61 (18,1) [32,2]. true => ~_t21 | p2 [ SNF ] % 0.36/0.61 (17,1) [33,2]. _t22 => ~box 1~ ~p2 [ SNF ] [ SNF++, 455, ~p2 ] % 0.36/0.61 (18,1) [34,2]. true => _t22 | ~_t21 [ SNF ] % 0.36/0.61 (1,1) [71,2]. _t28 => box 1 _t29 [ SNF ] [ SNF++, 447, _t29 ] % 0.36/0.61 (1,1) [73,2]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 449, _t19 ] % 0.36/0.61 (1,1) [75,2]. true => ~_t32 | _t18 [ SNF ] % 0.36/0.61 (1,1) [78,2]. true => _t32 | _t28 | ~_t27 | _t4 [ SNF ] % 0.36/0.61 (74,1) [85,2]. _t20 => ~box 1~ _t21 [ SNF ] [ SNF++, 463, _t21 ] % 0.36/0.61 (1,1) [86,2]. true => _t20 | ~_t19 | p2 [ SNF ] % 0.36/0.61 (75,1) [97,2]. _t3 => ~box 1~ _t4 [ SNF ] [ SNF++, 465, _t4 ] % 0.36/0.61 (1,1) [101,2]. _t7 => box 1 p2 [ SNF ] [ SNF++, 451, p2 ] % 0.36/0.61 (1,1) [103,2]. true => _t7 | ~_t6 | ~p2 [ SNF ] % 0.36/0.61 (1,1) [445,2]. _t5 => box 1 _t141 [ SNF++, 8 ] % 0.36/0.61 (1,1) [447,2]. _t28 => box 1 _t145 [ SNF++, 71 ] % 0.36/0.61 (1,1) [449,2]. _t18 => box 1 _t146 [ SNF++, 73 ] % 0.36/0.61 (1,1) [451,2]. _t7 => box 1 _t139 [ SNF++, 101 ] % 0.36/0.61 (17,1) [455,2]. _t22 => ~box 1~ _t144 [ SNF++, 33 ] % 0.36/0.61 (74,1) [463,2]. _t20 => ~box 1~ _t142 [ SNF++, 85 ] % 0.36/0.61 (75,1) [465,2]. _t3 => ~box 1~ _t143 [ SNF++, 97 ] % 0.36/0.61 (3,1) [470,2]. true => ~_t143 | _t4 [ SNF++, 11 ] % 0.36/0.61 (18,1) [476,2]. true => ~_t142 | _t21 [ SNF++, 35 ] % 0.36/0.61 (1,1) [478,2]. true => ~_t150 | _t27 [ SNF++, 80 ] % 0.36/0.61 (1,1) [480,2]. true => ~_t146 | _t19 [ SNF++, 88 ] % 0.36/0.61 (76,1) [482,2]. true => ~_t147 | _t3 [ SNF++, 98 ] % 0.36/0.61 (1,1) [484,2]. true => ~_t141 | _t6 [ SNF++, 105 ] % 0.36/0.61 (3,1) [538,2]. true => _t20 | ~_t19 | ~_t4 [ LRES, 4, 86, ~p2 ] % 0.36/0.61 (3,1) [556,2]. true => _t32 | _t28 | ~_t27 | _t5 [ LRES, 10, 78, ~_t4 ] % 0.36/0.61 (3,1) [557,2]. true => ~_t143 | _t5 [ LRES, 10, 470, ~_t4 ] % 0.36/0.61 (18,1) [580,2]. true => ~_t142 | _t22 [ LRES, 34, 476, ~_t21 ] % 0.36/0.61 (17,1) [589,2]. true => ~_t22 | ~_t7 [ GEN1, 451, 455, 541, _t139, _t144 ] % 0.36/0.61 (18,1) [604,2]. true => ~_t21 | _t7 | ~_t6 [ LRES, 103, 32, ~p2 ] % 0.36/0.61 (3,1) [607,2]. true => _t32 | _t28 | ~_t27 | _t20 | ~_t19 [ LRES, 538, 78, ~_t4 ] % 0.36/0.61 (3,1) [608,2]. true => ~_t143 | _t20 | ~_t19 [ LRES, 538, 470, ~_t4 ] % 0.36/0.61 (18,1) [611,2]. true => ~_t141 | ~_t21 | _t7 [ LRES, 604, 484, ~_t6 ] % 0.36/0.61 (3,1) [614,2]. true => ~_t146 | ~_t143 | _t20 [ LRES, 608, 480, ~_t19 ] [ Backward Subsumption, 681 ] % 0.36/0.61 (18,1) [619,2]. true => ~_t141 | ~_t22 | ~_t21 [ LRES, 611, 589, _t7 ] % 0.36/0.61 (18,1) [627,2]. true => ~_t142 | ~_t141 | ~_t22 [ LRES, 619, 476, ~_t21 ] [ Backward Subsumption, 633 ] % 0.36/0.61 (18,1) [633,2]. true => ~_t142 | ~_t141 [ LRES, 627, 580, ~_t22 ] % 0.36/0.61 (75,1) [655,2]. true => ~_t18 | ~_t3 [ GEN1, 449, 465, 651, _t146, _t143 ] % 0.36/0.61 (76,1) [657,2]. true => ~_t147 | ~_t18 [ LRES, 655, 482, ~_t3 ] % 0.36/0.61 (76,1) [659,2]. true => ~_t147 | ~_t32 [ LRES, 657, 75, ~_t18 ] % 0.36/0.61 (75,1) [661,2]. true => ~_t28 | ~_t3 [ GEN1, 447, 465, 660, _t145, _t143 ] % 0.36/0.61 (76,1) [662,2]. true => ~_t147 | ~_t28 [ LRES, 661, 482, ~_t3 ] % 0.36/0.61 (74,1) [677,2]. true => ~_t20 | ~_t5 [ GEN1, 445, 463, 674, _t141, _t142 ] % 0.36/0.61 (74,1) [678,2]. true => ~_t143 | ~_t20 [ LRES, 677, 557, ~_t5 ] % 0.36/0.61 (74,1) [679,2]. true => _t32 | _t28 | ~_t27 | ~_t20 [ LRES, 677, 556, ~_t5 ] % 0.36/0.61 (74,1) [681,2]. true => ~_t146 | ~_t143 [ LRES, 678, 614, ~_t20 ] % 0.36/0.61 (3,1) [717,2]. true => ~_t146 | _t32 | _t28 | ~_t27 | _t20 [ LRES, 607, 480, ~_t19 ] [ Backward Subsumption, 723 ] % 0.36/0.61 (74,1) [723,2]. true => ~_t146 | _t32 | _t28 | ~_t27 [ LRES, 717, 679, _t20 ] % 0.36/0.61 (74,1) [725,2]. true => ~_t150 | ~_t146 | _t32 | _t28 [ LRES, 723, 478, ~_t27 ] % 0.36/0.61 (76,1) [727,2]. true => ~_t150 | ~_t147 | ~_t146 | _t32 [ LRES, 725, 662, _t28 ] [ Backward Subsumption, 728 ] % 0.36/0.61 (76,1) [728,2]. true => ~_t150 | ~_t147 | ~_t146 [ LRES, 727, 659, _t32 ] % 0.36/0.61 (1,1) [5,3]. _t7 => box 1 p2 [ SNF ] [ SNF++, 427, p2 ] % 0.36/0.61 (1,1) [7,3]. true => _t7 | ~_t6 | ~p2 [ SNF ] % 0.36/0.61 (65,1) [49,3]. _t20 => ~box 1~ _t21 [ SNF ] [ SNF++, 435, _t21 ] % 0.36/0.61 (1,1) [50,3]. true => _t20 | ~_t19 | p2 [ SNF ] % 0.36/0.61 (1,1) [51,3]. true => ~_t29 | _t19 [ SNF ] % 0.36/0.61 (74,1) [82,3]. true => ~_t21 | p2 [ SNF ] % 0.36/0.61 (73,1) [83,3]. _t22 => ~box 1~ ~p2 [ SNF ] [ SNF++, 441, ~p2 ] % 0.36/0.61 (74,1) [84,3]. true => _t22 | ~_t21 [ SNF ] % 0.36/0.61 (75,1) [90,3]. true => ~_t4 | ~p2 [ SNF ] % 0.36/0.61 (1,1) [94,3]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 431, _t6 ] % 0.36/0.61 (75,1) [96,3]. true => _t5 | ~_t4 [ SNF ] % 0.36/0.61 (1,1) [427,3]. _t7 => box 1 _t139 [ SNF++, 5 ] % 0.36/0.61 (1,1) [431,3]. _t5 => box 1 _t141 [ SNF++, 94 ] % 0.36/0.61 (65,1) [435,3]. _t20 => ~box 1~ _t142 [ SNF++, 49 ] % 0.36/0.61 (73,1) [441,3]. _t22 => ~box 1~ _t144 [ SNF++, 83 ] % 0.36/0.61 (1,1) [446,3]. true => ~_t141 | _t6 [ SNF++, 8 ] % 0.36/0.61 (1,1) [448,3]. true => ~_t145 | _t29 [ SNF++, 71 ] % 0.36/0.61 (1,1) [450,3]. true => ~_t146 | _t19 [ SNF++, 73 ] % 0.36/0.61 (1,1) [452,3]. true => ~_t139 | p2 [ SNF++, 101 ] % 0.36/0.61 (17,1) [456,3]. true => ~_t144 | ~p2 [ SNF++, 33 ] % 0.36/0.61 (74,1) [464,3]. true => ~_t142 | _t21 [ SNF++, 85 ] % 0.36/0.61 (75,1) [466,3]. true => ~_t143 | _t4 [ SNF++, 97 ] % 0.36/0.61 (17,1) [541,3]. true => ~_t144 | ~_t139 [ LRES, 456, 452, ~p2 ] % 0.36/0.61 (75,1) [549,3]. true => _t20 | ~_t19 | ~_t4 [ LRES, 90, 50, ~p2 ] % 0.36/0.61 (74,1) [570,3]. true => ~_t142 | _t22 [ LRES, 84, 464, ~_t21 ] % 0.36/0.61 (75,1) [583,3]. true => ~_t143 | _t5 [ LRES, 96, 466, ~_t4 ] % 0.36/0.61 (73,1) [591,3]. true => ~_t22 | ~_t7 [ GEN1, 427, 441, 554, _t139, _t144 ] % 0.36/0.61 (74,1) [616,3]. true => ~_t21 | _t7 | ~_t6 [ LRES, 7, 82, ~p2 ] % 0.36/0.61 (75,1) [621,3]. true => ~_t143 | _t20 | ~_t19 [ LRES, 549, 466, ~_t4 ] % 0.36/0.61 (75,1) [624,3]. true => ~_t143 | ~_t29 | _t20 [ LRES, 621, 51, ~_t19 ] [ Backward Subsumption, 658 ] % 0.36/0.61 (75,1) [625,3]. true => ~_t146 | ~_t143 | _t20 [ LRES, 621, 450, ~_t19 ] [ Backward Subsumption, 651 ] % 0.36/0.61 (65,1) [630,3]. true => ~_t20 | ~_t5 [ GEN1, 431, 435, 626, _t141, _t142 ] % 0.36/0.61 (75,1) [631,3]. true => ~_t143 | ~_t20 [ LRES, 630, 583, ~_t5 ] % 0.36/0.61 (74,1) [640,3]. true => ~_t141 | ~_t21 | _t7 [ LRES, 616, 446, ~_t6 ] % 0.36/0.61 (75,1) [651,3]. true => ~_t146 | ~_t143 [ LRES, 625, 631, _t20 ] % 0.36/0.61 (75,1) [658,3]. true => ~_t143 | ~_t29 [ LRES, 624, 631, _t20 ] % 0.36/0.61 (75,1) [660,3]. true => ~_t145 | ~_t143 [ LRES, 658, 448, ~_t29 ] % 0.36/0.61 (74,1) [663,3]. true => ~_t141 | ~_t22 | ~_t21 [ LRES, 640, 591, _t7 ] % 0.36/0.61 (74,1) [673,3]. true => ~_t142 | ~_t141 | ~_t22 [ LRES, 663, 464, ~_t21 ] [ Backward Subsumption, 674 ] % 0.36/0.61 (74,1) [674,3]. true => ~_t142 | ~_t141 [ LRES, 673, 570, ~_t22 ] % 0.36/0.61 (65,1) [46,4]. true => ~_t21 | p2 [ SNF ] % 0.36/0.61 (64,1) [47,4]. _t22 => ~box 1~ ~p2 [ SNF ] [ SNF++, 521, ~p2 ] % 0.36/0.61 (65,1) [48,4]. true => _t22 | ~_t21 [ SNF ] % 0.36/0.61 (1,1) [91,4]. _t7 => box 1 p2 [ SNF ] [ SNF++, 533, p2 ] % 0.36/0.61 (1,1) [92,4]. _t7 => ~box 1~ p2 [ Axiom SER ] [ SNF++, 527, p2 ] % 0.36/0.61 (1,1) [93,4]. true => _t7 | ~_t6 | ~p2 [ SNF ] % 0.36/0.61 (1,1) [428,4]. true => ~_t139 | p2 [ SNF++, 5 ] % 0.36/0.61 (1,1) [432,4]. true => ~_t141 | _t6 [ SNF++, 94 ] % 0.36/0.61 (65,1) [436,4]. true => ~_t142 | _t21 [ SNF++, 49 ] % 0.36/0.61 (73,1) [442,4]. true => ~_t144 | ~p2 [ SNF++, 83 ] % 0.36/0.61 (64,1) [521,4]. _t22 => ~box 1~ _t144 [ SNF++, 47 ] % 0.36/0.61 (1,1) [533,4]. _t7 => box 1 _t139 [ SNF++, 91 ] % 0.36/0.61 (65,1) [543,4]. true => ~_t142 | _t22 [ LRES, 48, 436, ~_t21 ] % 0.36/0.61 (73,1) [554,4]. true => ~_t144 | ~_t139 [ LRES, 442, 428, ~p2 ] % 0.36/0.61 (64,1) [555,4]. true => ~_t22 | ~_t7 [ GEN1, 533, 521, 546, _t139, _t144 ] % 0.36/0.61 (65,1) [602,4]. true => ~_t21 | _t7 | ~_t6 [ LRES, 93, 46, ~p2 ] % 0.36/0.61 (65,1) [610,4]. true => ~_t141 | ~_t21 | _t7 [ LRES, 602, 432, ~_t6 ] % 0.36/0.61 (65,1) [613,4]. true => ~_t141 | ~_t22 | ~_t21 [ LRES, 610, 555, _t7 ] % 0.36/0.61 (65,1) [622,4]. true => ~_t142 | ~_t141 | ~_t22 [ LRES, 613, 436, ~_t21 ] [ Backward Subsumption, 626 ] % 0.36/0.61 (65,1) [626,4]. true => ~_t142 | ~_t141 [ LRES, 622, 543, ~_t22 ] % 0.36/0.61 (64,1) [522,5]. true => ~_t144 | ~p2 [ SNF++, 47 ] % 0.36/0.61 (1,1) [528,5]. true => ~_t139 | p2 [ SNF++, 92 ] % 0.36/0.61 (64,1) [546,5]. true => ~_t144 | ~_t139 [ LRES, 522, 528, ~p2 ] % 0.36/0.61 % SZS output end Refutation % 0.36/0.61 % KSP exiting %------------------------------------------------------------------------------