%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP015_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:53 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 : SYP015_1 : TPTP v9.3.0. Released v9.3.0. % 0.11/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 16:08:01 EDT 2026 % 0.15/0.34 % CPUTime : % 0.36/0.60 ----KSP format--- % 0.36/0.61 usable(formulas). % 0.36/0.61 true. % 0.36/0.61 end_of_list. % 0.36/0.61 sos(formulas). % 0.36/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.36/0.61 end_of_list. % 0.36/0.61 ----------------- % 0.36/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/sandbox2/tmp/tmp.iQPt4uNp4Q/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) [1,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.36/0.61 (1,1) [8,0]. _t0 => box 1 _t2 [ SNF ] [ Backward Subsumption, 314 ] % 0.36/0.61 (1,1) [23,0]. _t0 => box 1 _t19 [ SNF ] [ Backward Subsumption, 311 ] % 0.36/0.61 (24,1) [26,0]. _t0 => ~box 1~ ~p2 [ SNF ] [ Backward Subsumption, 308 ] % 0.36/0.61 (77,1) [67,0]. _t24 => ~box 1~ _t25 [ SNF ] [ SNF++, 378, _t25 ] % 0.36/0.61 (1,1) [74,0]. _t31 => box 1 _t18 [ SNF ] [ SNF++, 370, _t18 ] % 0.36/0.61 (89,1) [75,0]. _t3 => ~box 1~ _t4 [ SNF ] [ SNF++, 380, _t4 ] % 0.36/0.61 (1,1) [76,0]. true => _t31 | ~_t30 | _t3 [ SNF ] [ Backward Subsumption, 481 ] % 0.36/0.61 (1,1) [77,0]. true => _t30 | ~_t29 [ SNF ] [ Backward Subsumption, 527 ] % 0.36/0.61 (1,1) [78,0]. true => _t29 | _t24 | ~_t23 [ SNF ] [ Backward Subsumption, 315 ] % 0.36/0.61 (1,1) [79,0]. true => _t23 | ~_t0 [ SNF ] [ Backward Subsumption, 307 ] % 0.36/0.61 (1,1) [307,0]. true => _t23 [ Unit Resolution, 1, 79, _t0 ] [ Modal Level Pure Literal Elimination, _t23 ] % 0.36/0.61 (24,1) [308,0]. true => ~box 1~ ~p2 [ LHS Unit Resolution, 1, 26, _t0 ] [ SNF++, 376, ~p2 ] % 0.36/0.61 (1,1) [311,0]. true => box 1 _t19 [ LHS Unit Resolution, 1, 23, _t0 ] [ SNF++, 368, _t19 ] % 0.36/0.61 (1,1) [314,0]. true => box 1 _t2 [ LHS Unit Resolution, 1, 8, _t0 ] [ SNF++, 362, _t2 ] % 0.36/0.61 (1,1) [315,0]. true => _t29 | _t24 [ Unit Resolution, 307, 78, _t23 ] [ Backward Subsumption, 528 ] % 0.36/0.61 (1,1) [362,0]. true => box 1 _t124 [ SNF++, 314 ] % 0.36/0.61 (1,1) [368,0]. true => box 1 _t119 [ SNF++, 311 ] % 0.36/0.61 (1,1) [370,0]. _t31 => box 1 _t113 [ SNF++, 74 ] [ Backward Subsumption, 525 ] % 0.36/0.61 (24,1) [376,0]. true => ~box 1~ _t117 [ SNF++, 308 ] % 0.36/0.61 (77,1) [378,0]. _t24 => ~box 1~ _t129 [ SNF++, 67 ] [ Backward Subsumption, 529 ] % 0.36/0.61 (89,1) [380,0]. _t3 => ~box 1~ _t116 [ SNF++, 75 ] [ Backward Subsumption, 482 ] % 0.36/0.61 (89,1) [480,0]. true => ~_t3 [ GEN1, 368, 380, 476, _t119, _t116 ] [ Modal Level Pure Literal Elimination, ~_t3 ] % 0.36/0.61 (89,1) [481,0]. true => _t31 | ~_t30 [ Unit Resolution, 480, 76, _t3 ] [ Backward Subsumption, 524 ] % 0.36/0.61 (24,1) [523,0]. true => ~_t31 [ GEN1, 362, 370, 376, 519, _t124, _t113, _t117 ] [ Modal Level Pure Literal Elimination, ~_t31 ] % 0.36/0.61 (89,1) [524,0]. true => ~_t30 [ Unit Resolution, 523, 481, _t31 ] [ Modal Level Pure Literal Elimination, ~_t30 ] % 0.36/0.61 (89,1) [527,0]. true => ~_t29 [ Unit Resolution, 524, 77, _t30 ] [ Modal Level Pure Literal Elimination, ~_t29 ] % 0.36/0.61 (89,1) [528,0]. true => _t24 [ Unit Resolution, 527, 315, _t29 ] [ Modal Level Pure Literal Elimination, _t24 ] % 0.36/0.61 (77,1) [529,0]. true => ~box 1~ _t129 [ LHS Unit Resolution, 528, 378, _t24 ] % 0.36/0.61 (77,1) [551,0]. true => false [ GEN1, 368, 529, 549, _t119, _t129 ] % 0.36/0.61 (3,1) [6,1]. _t3 => ~box 1~ _t4 [ SNF ] [ SNF++, 344, _t4 ] % 0.36/0.61 (1,1) [7,1]. true => _t3 | ~_t2 | p2 [ SNF ] % 0.36/0.61 (18,1) [21,1]. _t20 => ~box 1~ _t21 [ SNF ] [ SNF++, 350, _t21 ] % 0.36/0.61 (1,1) [22,1]. true => _t20 | ~_t19 | p2 [ SNF ] % 0.36/0.61 (1,1) [49,1]. _t25 => box 1 _t27 [ SNF ] [ SNF++, 354, _t27 ] % 0.36/0.61 (1,1) [54,1]. _t32 => box 1 _t19 [ SNF ] [ SNF++, 358, _t19 ] % 0.36/0.61 (76,1) [60,1]. _t32 => ~box 1~ _t3 [ SNF ] [ SNF++, 352, _t3 ] % 0.36/0.61 (77,1) [61,1]. true => ~_t4 | ~p2 [ SNF ] % 0.36/0.61 (1,1) [64,1]. _t4 => box 1 _t6 [ SNF ] [ SNF++, 360, _t6 ] % 0.36/0.61 (77,1) [65,1]. true => ~_t34 | _t32 | _t4 [ SNF ] % 0.36/0.61 (77,1) [66,1]. true => _t34 | ~_t25 [ SNF ] % 0.36/0.61 (1,1) [73,1]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 356, _t19 ] % 0.36/0.61 (3,1) [344,1]. _t3 => ~box 1~ _t116 [ SNF++, 6 ] % 0.36/0.61 (18,1) [350,1]. _t20 => ~box 1~ _t115 [ SNF++, 21 ] % 0.36/0.61 (76,1) [352,1]. _t32 => ~box 1~ _t120 [ SNF++, 60 ] % 0.36/0.61 (1,1) [354,1]. _t25 => box 1 _t123 [ SNF++, 49 ] % 0.36/0.61 (1,1) [356,1]. _t18 => box 1 _t119 [ SNF++, 73 ] [ Backward Subsumption, 526 ] % 0.36/0.61 (1,1) [358,1]. _t32 => box 1 _t119 [ SNF++, 54 ] % 0.36/0.61 (1,1) [360,1]. _t4 => box 1 _t114 [ SNF++, 64 ] % 0.36/0.61 (1,1) [363,1]. true => ~_t124 | _t2 [ SNF++, 314 ] % 0.36/0.61 (1,1) [369,1]. true => ~_t119 | _t19 [ SNF++, 311 ] % 0.36/0.61 (1,1) [371,1]. true => ~_t113 | _t18 [ SNF++, 74 ] [ Modal Level Pure Literal Elimination, ~_t113 ] % 0.36/0.61 (24,1) [377,1]. true => ~_t117 | ~p2 [ SNF++, 308 ] % 0.36/0.61 (77,1) [379,1]. true => ~_t129 | _t25 [ SNF++, 67 ] % 0.36/0.61 (89,1) [381,1]. true => ~_t116 | _t4 [ SNF++, 75 ] [ Modal Level Pure Literal Elimination, ~_t116 ] % 0.36/0.61 (24,1) [395,1]. true => ~_t117 | _t3 | ~_t2 [ LRES, 377, 7, ~p2 ] % 0.36/0.61 (77,1) [407,1]. true => _t20 | ~_t19 | ~_t4 [ LRES, 61, 22, ~p2 ] % 0.36/0.61 (77,1) [413,1]. true => ~_t129 | _t34 [ LRES, 66, 379, ~_t25 ] % 0.36/0.61 (24,1) [431,1]. true => ~_t124 | ~_t117 | _t3 [ LRES, 395, 363, ~_t2 ] % 0.36/0.61 (77,1) [436,1]. true => ~_t34 | _t32 | _t20 | ~_t19 [ LRES, 407, 65, ~_t4 ] % 0.36/0.61 (89,1) [437,1]. true => ~_t116 | _t20 | ~_t19 [ LRES, 407, 381, ~_t4 ] [ Modal Level Pure Literal Elimination, ~_t116 ] % 0.36/0.61 (18,1) [442,1]. true => ~_t20 | ~_t4 [ GEN1, 360, 350, 439, _t114, _t115 ] % 0.36/0.61 (77,1) [444,1]. true => ~_t34 | _t32 | ~_t20 [ LRES, 442, 65, ~_t4 ] % 0.36/0.61 (89,1) [445,1]. true => ~_t116 | ~_t20 [ LRES, 442, 381, ~_t4 ] [ Modal Level Pure Literal Elimination, ~_t116 ] % 0.36/0.61 (89,1) [467,1]. true => ~_t119 | ~_t116 | _t20 [ LRES, 437, 369, ~_t19 ] [ Backward Subsumption, 476 ] % 0.36/0.61 (89,1) [476,1]. true => ~_t119 | ~_t116 [ LRES, 467, 445, _t20 ] [ Modal Level Pure Literal Elimination, ~_t116 ] % 0.36/0.61 (77,1) [484,1]. true => ~_t119 | ~_t34 | _t32 | _t20 [ LRES, 436, 369, ~_t19 ] [ Backward Subsumption, 490 ] % 0.36/0.61 (77,1) [490,1]. true => ~_t119 | ~_t34 | _t32 [ LRES, 484, 444, _t20 ] % 0.36/0.61 (3,1) [503,1]. true => ~_t18 | ~_t3 [ GEN1, 356, 344, 498, _t119, _t116 ] [ Modal Level Pure Literal Elimination, ~_t18 ] % 0.36/0.61 (24,1) [508,1]. true => ~_t124 | ~_t117 | ~_t18 [ LRES, 503, 431, ~_t3 ] [ Modal Level Pure Literal Elimination, ~_t18 ] % 0.36/0.61 (24,1) [519,1]. true => ~_t124 | ~_t117 | ~_t113 [ LRES, 508, 371, ~_t18 ] [ Modal Level Pure Literal Elimination, ~_t113 ] % 0.36/0.61 (76,1) [543,1]. true => ~_t32 | ~_t25 [ GEN1, 354, 358, 352, 542, _t123, _t119, _t120 ] % 0.36/0.61 (77,1) [544,1]. true => ~_t129 | ~_t32 [ LRES, 543, 379, ~_t25 ] % 0.36/0.61 (77,1) [547,1]. true => ~_t129 | ~_t119 | ~_t34 [ LRES, 544, 490, ~_t32 ] [ Backward Subsumption, 549 ] % 0.36/0.61 (77,1) [549,1]. true => ~_t129 | ~_t119 [ LRES, 547, 413, ~_t34 ] % 0.36/0.61 (3,1) [2,2]. true => ~_t4 | ~p2 [ SNF ] % 0.36/0.61 (1,1) [5,2]. _t4 => box 1 _t6 [ SNF ] [ SNF++, 328, _t6 ] % 0.36/0.61 (18,1) [19,2]. true => ~_t21 | p2 [ SNF ] % 0.36/0.61 (17,1) [20,2]. _t21 => ~box 1~ ~p2 [ SNF ] [ SNF++, 336, ~p2 ] % 0.36/0.61 (1,1) [45,2]. _t28 => box 1 _t29 [ SNF ] [ SNF++, 330, _t29 ] % 0.36/0.61 (1,1) [46,2]. _t32 => box 1 _t19 [ SNF ] [ SNF++, 332, _t19 ] % 0.36/0.61 (1,1) [48,2]. true => _t32 | _t28 | ~_t27 | _t4 [ SNF ] % 0.36/0.61 (74,1) [52,2]. _t20 => ~box 1~ _t21 [ SNF ] [ SNF++, 340, _t21 ] % 0.36/0.61 (1,1) [53,2]. true => _t20 | ~_t19 | p2 [ SNF ] % 0.36/0.61 (75,1) [59,2]. _t3 => ~box 1~ _t4 [ SNF ] [ SNF++, 342, _t4 ] % 0.36/0.61 (1,1) [62,2]. _t7 => box 1 p2 [ SNF ] [ SNF++, 334, p2 ] % 0.36/0.61 (1,1) [63,2]. true => _t7 | ~_t6 | ~p2 [ SNF ] % 0.36/0.61 (1,1) [328,2]. _t4 => box 1 _t114 [ SNF++, 5 ] % 0.36/0.61 (1,1) [330,2]. _t28 => box 1 _t118 [ SNF++, 45 ] % 0.36/0.61 (1,1) [332,2]. _t32 => box 1 _t119 [ SNF++, 46 ] % 0.36/0.61 (1,1) [334,2]. _t7 => box 1 _t112 [ SNF++, 62 ] % 0.36/0.61 (17,1) [336,2]. _t21 => ~box 1~ _t117 [ SNF++, 20 ] % 0.36/0.61 (74,1) [340,2]. _t20 => ~box 1~ _t115 [ SNF++, 52 ] % 0.36/0.61 (75,1) [342,2]. _t3 => ~box 1~ _t116 [ SNF++, 59 ] % 0.36/0.61 (3,1) [345,2]. true => ~_t116 | _t4 [ SNF++, 6 ] % 0.36/0.61 (18,1) [351,2]. true => ~_t115 | _t21 [ SNF++, 21 ] % 0.36/0.61 (76,1) [353,2]. true => ~_t120 | _t3 [ SNF++, 60 ] % 0.36/0.61 (1,1) [355,2]. true => ~_t123 | _t27 [ SNF++, 49 ] % 0.36/0.61 (1,1) [357,2]. true => ~_t119 | _t19 [ SNF++, 73 ] % 0.36/0.61 (1,1) [361,2]. true => ~_t114 | _t6 [ SNF++, 64 ] % 0.36/0.61 (3,1) [391,2]. true => _t20 | ~_t19 | ~_t4 [ LRES, 2, 53, ~p2 ] % 0.36/0.61 (18,1) [419,2]. true => ~_t21 | _t7 | ~_t6 [ LRES, 63, 19, ~p2 ] % 0.36/0.61 (17,1) [421,2]. true => ~_t21 | ~_t7 [ GEN1, 334, 336, 394, _t112, _t117 ] % 0.36/0.61 (3,1) [426,2]. true => _t32 | _t28 | ~_t27 | _t20 | ~_t19 [ LRES, 391, 48, ~_t4 ] % 0.36/0.61 (3,1) [427,2]. true => ~_t116 | _t20 | ~_t19 [ LRES, 391, 345, ~_t4 ] % 0.36/0.61 (18,1) [430,2]. true => ~_t114 | ~_t21 | _t7 [ LRES, 419, 361, ~_t6 ] [ Backward Subsumption, 435 ] % 0.36/0.61 (3,1) [432,2]. true => ~_t119 | ~_t116 | _t20 [ LRES, 427, 357, ~_t19 ] [ Backward Subsumption, 498 ] % 0.36/0.61 (18,1) [435,2]. true => ~_t114 | ~_t21 [ LRES, 430, 421, _t7 ] % 0.36/0.61 (18,1) [439,2]. true => ~_t115 | ~_t114 [ LRES, 435, 351, ~_t21 ] % 0.36/0.61 (3,1) [478,2]. true => ~_t119 | _t32 | _t28 | ~_t27 | _t20 [ LRES, 426, 357, ~_t19 ] [ Backward Subsumption, 506 ] % 0.36/0.61 (74,1) [492,2]. true => ~_t20 | ~_t4 [ GEN1, 328, 340, 491, _t114, _t115 ] % 0.36/0.61 (74,1) [496,2]. true => _t32 | _t28 | ~_t27 | ~_t20 [ LRES, 492, 48, ~_t4 ] % 0.36/0.61 (74,1) [497,2]. true => ~_t116 | ~_t20 [ LRES, 492, 345, ~_t4 ] % 0.36/0.61 (74,1) [498,2]. true => ~_t119 | ~_t116 [ LRES, 497, 432, ~_t20 ] % 0.36/0.61 (74,1) [506,2]. true => ~_t119 | _t32 | _t28 | ~_t27 [ LRES, 496, 478, ~_t20 ] % 0.36/0.61 (75,1) [509,2]. true => ~_t32 | ~_t3 [ GEN1, 332, 342, 504, _t119, _t116 ] % 0.36/0.61 (76,1) [510,2]. true => ~_t120 | ~_t32 [ LRES, 509, 353, ~_t3 ] % 0.36/0.61 (75,1) [517,2]. true => ~_t28 | ~_t3 [ GEN1, 330, 342, 515, _t118, _t116 ] % 0.36/0.61 (76,1) [518,2]. true => ~_t120 | ~_t28 [ LRES, 517, 353, ~_t3 ] % 0.36/0.61 (74,1) [522,2]. true => ~_t123 | ~_t119 | _t32 | _t28 [ LRES, 506, 355, ~_t27 ] % 0.36/0.61 (76,1) [538,2]. true => ~_t123 | ~_t120 | ~_t119 | _t32 [ LRES, 522, 518, _t28 ] [ Backward Subsumption, 542 ] % 0.36/0.61 (76,1) [542,2]. true => ~_t123 | ~_t120 | ~_t119 [ LRES, 538, 510, _t32 ] % 0.36/0.61 (1,1) [3,3]. _t7 => box 1 p2 [ SNF ] [ SNF++, 316, p2 ] % 0.36/0.61 (1,1) [4,3]. true => _t7 | ~_t6 | ~p2 [ SNF ] % 0.36/0.61 (65,1) [29,3]. _t20 => ~box 1~ _t21 [ SNF ] [ SNF++, 322, _t21 ] % 0.36/0.61 (1,1) [30,3]. true => _t20 | ~_t19 | p2 [ SNF ] % 0.36/0.61 (1,1) [31,3]. true => ~_t29 | _t19 [ SNF ] % 0.36/0.61 (74,1) [50,3]. true => ~_t21 | p2 [ SNF ] % 0.36/0.61 (73,1) [51,3]. _t21 => ~box 1~ ~p2 [ SNF ] [ SNF++, 326, ~p2 ] % 0.36/0.61 (75,1) [55,3]. true => ~_t4 | ~p2 [ SNF ] % 0.36/0.61 (1,1) [58,3]. _t4 => box 1 _t6 [ SNF ] [ SNF++, 320, _t6 ] % 0.36/0.61 (1,1) [316,3]. _t7 => box 1 _t112 [ SNF++, 3 ] % 0.36/0.61 (1,1) [320,3]. _t4 => box 1 _t114 [ SNF++, 58 ] % 0.36/0.61 (65,1) [322,3]. _t20 => ~box 1~ _t115 [ SNF++, 29 ] % 0.36/0.61 (73,1) [326,3]. _t21 => ~box 1~ _t117 [ SNF++, 51 ] % 0.36/0.61 (1,1) [329,3]. true => ~_t114 | _t6 [ SNF++, 5 ] % 0.36/0.61 (1,1) [331,3]. true => ~_t118 | _t29 [ SNF++, 45 ] % 0.36/0.61 (1,1) [333,3]. true => ~_t119 | _t19 [ SNF++, 46 ] % 0.36/0.61 (1,1) [335,3]. true => ~_t112 | p2 [ SNF++, 62 ] % 0.36/0.61 (17,1) [337,3]. true => ~_t117 | ~p2 [ SNF++, 20 ] % 0.36/0.61 (74,1) [341,3]. true => ~_t115 | _t21 [ SNF++, 52 ] % 0.36/0.61 (75,1) [343,3]. true => ~_t116 | _t4 [ SNF++, 59 ] % 0.36/0.61 (17,1) [394,3]. true => ~_t117 | ~_t112 [ LRES, 337, 335, ~p2 ] % 0.36/0.61 (75,1) [403,3]. true => _t20 | ~_t19 | ~_t4 [ LRES, 55, 30, ~p2 ] % 0.36/0.61 (73,1) [418,3]. true => ~_t21 | ~_t7 [ GEN1, 316, 326, 398, _t112, _t117 ] % 0.36/0.61 (74,1) [457,3]. true => ~_t21 | _t7 | ~_t6 [ LRES, 4, 50, ~p2 ] % 0.36/0.61 (65,1) [464,3]. true => ~_t20 | ~_t4 [ GEN1, 320, 322, 459, _t114, _t115 ] % 0.36/0.61 (75,1) [466,3]. true => ~_t116 | ~_t20 [ LRES, 464, 343, ~_t4 ] % 0.36/0.61 (75,1) [471,3]. true => ~_t116 | _t20 | ~_t19 [ LRES, 403, 343, ~_t4 ] % 0.36/0.61 (74,1) [475,3]. true => ~_t114 | ~_t21 | _t7 [ LRES, 457, 329, ~_t6 ] [ Backward Subsumption, 488 ] % 0.36/0.61 (75,1) [485,3]. true => ~_t116 | ~_t29 | _t20 [ LRES, 471, 31, ~_t19 ] [ Backward Subsumption, 513 ] % 0.36/0.61 (75,1) [486,3]. true => ~_t119 | ~_t116 | _t20 [ LRES, 471, 333, ~_t19 ] [ Backward Subsumption, 504 ] % 0.36/0.61 (74,1) [488,3]. true => ~_t114 | ~_t21 [ LRES, 475, 418, _t7 ] % 0.36/0.61 (74,1) [491,3]. true => ~_t115 | ~_t114 [ LRES, 488, 341, ~_t21 ] % 0.36/0.61 (75,1) [504,3]. true => ~_t119 | ~_t116 [ LRES, 486, 466, _t20 ] % 0.36/0.61 (75,1) [513,3]. true => ~_t116 | ~_t29 [ LRES, 485, 466, _t20 ] % 0.36/0.61 (75,1) [515,3]. true => ~_t118 | ~_t116 [ LRES, 513, 331, ~_t29 ] % 0.36/0.61 (65,1) [27,4]. true => ~_t21 | p2 [ SNF ] % 0.36/0.61 (64,1) [28,4]. _t21 => ~box 1~ ~p2 [ SNF ] [ SNF++, 382, ~p2 ] % 0.36/0.61 (1,1) [56,4]. _t7 => box 1 p2 [ SNF ] [ SNF++, 386, p2 ] % 0.36/0.61 (1,1) [57,4]. true => _t7 | ~_t6 | ~p2 [ SNF ] % 0.36/0.61 (1,1) [317,4]. true => ~_t112 | p2 [ SNF++, 3 ] % 0.36/0.61 (1,1) [321,4]. true => ~_t114 | _t6 [ SNF++, 58 ] % 0.36/0.61 (65,1) [323,4]. true => ~_t115 | _t21 [ SNF++, 29 ] % 0.36/0.61 (73,1) [327,4]. true => ~_t117 | ~p2 [ SNF++, 51 ] % 0.36/0.61 (64,1) [382,4]. _t21 => ~box 1~ _t117 [ SNF++, 28 ] % 0.36/0.61 (1,1) [386,4]. _t7 => box 1 _t112 [ SNF++, 56 ] % 0.36/0.61 (73,1) [398,4]. true => ~_t117 | ~_t112 [ LRES, 327, 317, ~p2 ] % 0.36/0.61 (64,1) [410,4]. true => ~_t21 | ~_t7 [ GEN1, 386, 382, 400, _t112, _t117 ] % 0.36/0.61 (65,1) [446,4]. true => ~_t21 | _t7 | ~_t6 [ LRES, 57, 27, ~p2 ] % 0.36/0.61 (65,1) [453,4]. true => ~_t114 | ~_t21 | _t7 [ LRES, 446, 321, ~_t6 ] [ Backward Subsumption, 454 ] % 0.36/0.61 (65,1) [454,4]. true => ~_t114 | ~_t21 [ LRES, 453, 410, _t7 ] % 0.36/0.61 (65,1) [459,4]. true => ~_t115 | ~_t114 [ LRES, 454, 323, ~_t21 ] % 0.36/0.61 (64,1) [383,5]. true => ~_t117 | ~p2 [ SNF++, 28 ] % 0.36/0.61 (1,1) [387,5]. true => ~_t112 | p2 [ SNF++, 56 ] % 0.36/0.61 (64,1) [400,5]. true => ~_t117 | ~_t112 [ LRES, 383, 387, ~p2 ] % 0.36/0.61 % SZS output end Refutation % 0.36/0.61 % KSP exiting %------------------------------------------------------------------------------