%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP051_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n014.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:55 PM UTC 2026 % Result : Theorem 5.66s 5.87s % Output : Refutation 5.76s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SYP051_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.14 % Command : run_ksp %s % 0.18/0.35 % Computer : n014.cluster.edu % 0.18/0.35 % Model : x86_64 x86_64 % 0.18/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.35 % Memory : 8042.1875MB % 0.18/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.35 % CPULimit : 300 % 0.18/0.35 % WCLimit : 300 % 0.18/0.35 % DateTime : Mon May 4 16:35:21 EDT 2026 % 0.18/0.36 % CPUTime : % 0.49/0.63 ----KSP format--- % 0.49/0.63 set(box,FIVE). % 0.49/0.63 usable(formulas). % 0.49/0.63 true. % 0.49/0.63 end_of_list. % 0.49/0.63 sos(formulas). % 0.49/0.63 ~ (( [] ( ( [] ( ( [] ( ( 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.49/0.63 end_of_list. % 0.49/0.63 ----------------- % 0.49/0.64 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.TDWuWOmIk0/theBenchmark.ksp % 5.66/5.87 % 5.66/5.87 % SZS status Theorem % 5.66/5.87 % 5.66/5.87 ***************** % 5.66/5.87 FOUND PROOF 1 % 5.66/5.87 ***************** % 5.66/5.87 % SZS output start Refutation % 5.66/5.87 % 5.66/5.87 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 5.66/5.87 (1,1) [96,0]. ~_t113 => box 1 ~_t5 [ Axiom 5 ] [ SNF++, 5357, ~_t5 ] % 5.66/5.87 (1,1) [97,0]. _t113 => box 1 _t113 [ Axiom 5 ] [ SNF++, 5359, _t113 ] % 5.66/5.87 (1,1) [209,0]. _t1 => box 1 _t2 [ SNF ] [ Backward Subsumption, 4449 ] % 5.66/5.87 (1,1) [366,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 4444 ] % 5.66/5.87 (1,1) [698,0]. _t18 => box 1 _t19 [ SNF ] [ Backward Subsumption, 4447 ] % 5.66/5.87 (1,1) [855,0]. true => _t18 | ~_t0 [ SNF ] [ Backward Subsumption, 4441 ] % 5.66/5.87 (24,1) [860,0]. _t22 => ~box 1~ ~p2 [ SNF ] [ Backward Subsumption, 4446 ] % 5.66/5.87 (1,1) [861,0]. true => _t22 | ~_t0 [ SNF ] [ Backward Subsumption, 4438 ] % 5.66/5.87 (1,1) [4438,0]. true => _t22 [ Unit Resolution, 3, 861, _t0 ] [ Modal Level Pure Literal Elimination, _t22 ] % 5.66/5.87 (1,1) [4441,0]. true => _t18 [ Unit Resolution, 3, 855, _t0 ] [ Modal Level Pure Literal Elimination, _t18 ] % 5.66/5.87 (1,1) [4444,0]. true => _t1 [ Unit Resolution, 3, 366, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 5.66/5.87 (24,1) [4446,0]. true => ~box 1~ ~p2 [ LHS Unit Resolution, 4438, 860, _t22 ] [ SNF++, 5531, ~p2 ] % 5.66/5.87 (1,1) [4447,0]. true => box 1 _t19 [ LHS Unit Resolution, 4441, 698, _t18 ] [ SNF++, 5379, _t19 ] % 5.66/5.87 (1,1) [4449,0]. true => box 1 _t2 [ LHS Unit Resolution, 4444, 209, _t1 ] [ SNF++, 5361, _t2 ] % 5.66/5.87 (1,1) [5357,0]. ~_t113 => box 1 _t144 [ SNF++, 96 ] % 5.66/5.87 (1,1) [5359,0]. _t113 => box 1 _t145 [ SNF++, 97 ] % 5.66/5.87 (1,1) [5361,0]. true => box 1 _t146 [ SNF++, 4449 ] % 5.66/5.87 (1,1) [5379,0]. true => box 1 _t155 [ SNF++, 4447 ] % 5.66/5.87 (24,1) [5531,0]. true => ~box 1~ _t233 [ SNF++, 4446 ] % 5.66/5.87 (24,1) [57872,0]. true => _t113 [ GEN1, 5361, 5357, 5531, 47198, _t146, _t144, _t233 ] % 5.66/5.87 (24,1) [71268,0]. true => ~_t113 [ GEN1, 5379, 5359, 5531, 71146, _t155, _t145, _t233 ] % 5.66/5.87 (24,1) [71274,0]. true => false [ LRES, 71268, 57872, ~_t113 ] % 5.66/5.87 (1,1) [101,1]. _t5 => box 1 _t6 [ Axiom 5 ] [ SNF++, 5587, _t6 ] % 5.66/5.87 (1,1) [103,1]. ~_t113 => box 1 ~_t5 [ Axiom 5 ] [ SNF++, 5589, ~_t5 ] % 5.66/5.87 (1,1) [105,1]. true => ~_t113 | _t5 [ Axiom 5 ] % 5.66/5.87 (3,1) [207,1]. _t3 => ~box 1~ _t4 [ SNF ] [ SNF++, 5751, _t4 ] % 5.66/5.87 (1,1) [208,1]. true => _t3 | ~_t2 | p2 [ SNF ] % 5.66/5.87 (18,1) [696,1]. _t20 => ~box 1~ _t21 [ SNF ] [ SNF++, 5763, _t21 ] % 5.66/5.87 (1,1) [697,1]. true => _t20 | ~_t19 | p2 [ SNF ] % 5.66/5.87 (1,1) [5358,1]. true => ~_t144 | ~_t5 [ SNF++, 96 ] % 5.66/5.87 (1,1) [5360,1]. true => ~_t145 | _t113 [ SNF++, 97 ] % 5.66/5.87 (1,1) [5362,1]. true => ~_t146 | _t2 [ SNF++, 4449 ] % 5.66/5.87 (1,1) [5380,1]. true => ~_t155 | _t19 [ SNF++, 4447 ] % 5.66/5.87 (24,1) [5532,1]. true => ~_t233 | ~p2 [ SNF++, 4446 ] % 5.66/5.87 (1,1) [5587,1]. _t5 => box 1 _t143 [ SNF++, 101 ] % 5.66/5.87 (1,1) [5589,1]. ~_t113 => box 1 _t144 [ SNF++, 103 ] % 5.66/5.87 (3,1) [5751,1]. _t3 => ~box 1~ _t225 [ SNF++, 207 ] % 5.66/5.87 (18,1) [5763,1]. _t20 => ~box 1~ _t234 [ SNF++, 696 ] % 5.66/5.87 (24,1) [9095,1]. true => ~_t233 | _t3 | ~_t2 [ LRES, 5532, 208, ~p2 ] % 5.66/5.87 (24,1) [9096,1]. true => ~_t233 | _t20 | ~_t19 [ LRES, 5532, 697, ~p2 ] % 5.66/5.87 (1,1) [12055,1]. true => ~_t144 | ~_t113 [ LRES, 5358, 105, ~_t5 ] % 5.66/5.87 (3,1) [14021,1]. true => _t113 | ~_t3 [ GEN1, 5589, 5751, 13254, _t144, _t225 ] % 5.66/5.87 (24,1) [26302,1]. true => ~_t233 | ~_t146 | _t3 [ LRES, 9095, 5362, ~_t2 ] % 5.66/5.87 (24,1) [28057,1]. true => ~_t233 | ~_t155 | _t20 [ LRES, 9096, 5380, ~_t19 ] % 5.66/5.87 (24,1) [33168,1]. true => ~_t233 | ~_t146 | _t113 [ LRES, 26302, 14021, _t3 ] % 5.66/5.87 (24,1) [47198,1]. true => ~_t233 | ~_t146 | ~_t144 [ LRES, 33168, 12055, _t113 ] % 5.66/5.87 (18,1) [68805,1]. true => ~_t20 | ~_t5 [ GEN1, 5587, 5763, 68759, _t143, _t234 ] % 5.66/5.87 (18,1) [68807,1]. true => ~_t113 | ~_t20 [ LRES, 68805, 105, ~_t5 ] % 5.66/5.87 (24,1) [68872,1]. true => ~_t233 | ~_t155 | ~_t113 [ LRES, 68807, 28057, ~_t20 ] % 5.66/5.87 (24,1) [71146,1]. true => ~_t233 | ~_t155 | ~_t145 [ LRES, 68872, 5360, ~_t113 ] % 5.66/5.87 (1,1) [16,2]. _t7 => box 1 p2 [ Axiom 5 ] [ SNF++, 5817, p2 ] % 5.66/5.87 (1,1) [100,2]. true => _t7 | ~_t6 | ~p2 [ Axiom 5 ] % 5.66/5.87 (3,1) [206,2]. true => _t5 | ~_t4 [ SNF ] % 5.66/5.87 (18,1) [693,2]. true => ~_t21 | p2 [ SNF ] % 5.66/5.87 (17,1) [694,2]. _t22 => ~box 1~ ~p2 [ SNF ] [ SNF++, 6003, ~p2 ] % 5.66/5.87 (18,1) [695,2]. true => _t22 | ~_t21 [ SNF ] % 5.76/5.91 (1,1) [5588,2]. true => ~_t143 | _t6 [ SNF++, 101 ] % 5.76/5.91 (1,1) [5590,2]. true => ~_t144 | ~_t5 [ SNF++, 103 ] % 5.76/5.91 (3,1) [5752,2]. true => ~_t225 | _t4 [ SNF++, 207 ] % 5.76/5.91 (18,1) [5764,2]. true => ~_t234 | _t21 [ SNF++, 696 ] % 5.76/5.91 (1,1) [5817,2]. _t7 => box 1 _t140 [ SNF++, 16 ] % 5.76/5.91 (17,1) [6003,2]. _t22 => ~box 1~ _t233 [ SNF++, 694 ] % 5.76/5.91 (3,1) [10390,2]. true => ~_t225 | _t5 [ LRES, 206, 5752, ~_t4 ] % 5.76/5.91 (18,1) [10606,2]. true => ~_t234 | _t22 [ LRES, 695, 5764, ~_t21 ] % 5.76/5.91 (17,1) [13085,2]. true => ~_t22 | ~_t7 [ GEN1, 5817, 6003, 9107, _t140, _t233 ] % 5.76/5.91 (3,1) [13254,2]. true => ~_t225 | ~_t144 [ LRES, 10390, 5590, _t5 ] % 5.76/5.91 (18,1) [31881,2]. true => ~_t21 | _t7 | ~_t6 [ LRES, 100, 693, ~p2 ] % 5.76/5.91 (18,1) [40158,2]. true => ~_t143 | ~_t21 | _t7 [ LRES, 31881, 5588, ~_t6 ] % 5.76/5.91 (18,1) [49490,2]. true => ~_t143 | ~_t22 | ~_t21 [ LRES, 40158, 13085, _t7 ] % 5.76/5.91 (18,1) [49539,2]. true => ~_t234 | ~_t143 | ~_t22 [ LRES, 49490, 5764, ~_t21 ] [ Backward Subsumption, 68759 ] % 5.76/5.91 (18,1) [68759,2]. true => ~_t234 | ~_t143 [ LRES, 49539, 10606, ~_t22 ] % 5.76/5.91 (1,1) [5818,3]. true => ~_t140 | p2 [ SNF++, 16 ] % 5.76/5.91 (17,1) [6004,3]. true => ~_t233 | ~p2 [ SNF++, 694 ] % 5.76/5.91 (17,1) [9107,3]. true => ~_t233 | ~_t140 [ LRES, 6004, 5818, ~p2 ] % 5.76/5.91 % SZS output end Refutation % 5.76/5.92 % KSP exiting %------------------------------------------------------------------------------