%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP061_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n012.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:56 PM UTC 2026 % Result : Theorem 0.64s 0.88s % Output : Refutation 0.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.07 % Problem : SYP061_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.07 % Command : run_ksp %s % 0.09/0.25 % Computer : n012.cluster.edu % 0.09/0.25 % Model : x86_64 x86_64 % 0.09/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.25 % Memory : 8042.1875MB % 0.09/0.25 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.25 % CPULimit : 300 % 0.09/0.25 % WCLimit : 300 % 0.09/0.25 % DateTime : Mon May 4 16:58:45 EDT 2026 % 0.09/0.25 % CPUTime : % 0.16/0.40 ----KSP format--- % 0.16/0.40 set(box,FIVE). % 0.16/0.40 usable(formulas). % 0.16/0.40 true. % 0.16/0.40 end_of_list. % 0.16/0.40 sos(formulas). % 0.16/0.40 ~ (<> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( ~ ( ( [] ( ~ ( p1 ) ) -> [] ( [] ( ~ ( p1 ) ) ) ) ) ) | [] ( <> ( [] ( p0 ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) ) | [] ( ( ~ ( [] ( p1 ) ) -> [] ( ~ ( [] ( p1 ) ) ) ) ) | <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( <> ( [] ( p1 ) & <> ( <> ( ~ ( p1 ) ) ) ) | <> ( ( [] ( <> ( p0 ) ) & [] ( ~ ( p0 ) | [] ( p3 ) ) ) | <> ( [] ( <> ( [] ( ~ ( p0 ) | [] ( p3 ) ) ) ) & [] ( <> ( p0 ) ) ) | ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) | [] ( p3 ) ) ) ) ) | <> ( <> ( [] ( <> ( p0 ) ) ) & p0 & <> ( ~ ( p0 ) | [] ( p3 ) ) ) | <> ( [] ( ~ ( p0 ) | [] ( p3 ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) ) | <> ( [] ( <> ( p1 ) ) & <> ( <> ( [] ( ~ ( p1 ) ) ) ) ) | <> ( p4 ) ). % 0.16/0.40 end_of_list. % 0.16/0.40 ----------------- % 0.16/0.40 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.CrECbblFyM/theBenchmark.ksp % 0.64/0.88 % 0.64/0.88 % SZS status Theorem % 0.64/0.88 % 0.64/0.88 ***************** % 0.64/0.88 FOUND PROOF 1 % 0.64/0.88 ***************** % 0.64/0.88 % SZS output start Refutation % 0.64/0.88 % 0.64/0.88 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.64/0.88 (103,1) [4470,0]. _t52 => ~box 1~ _t53 [ SNF ] [ Backward Subsumption, 5672 ] % 0.64/0.88 (1,1) [4471,0]. true => _t52 | ~_t0 [ SNF ] [ Backward Subsumption, 5667 ] % 0.64/0.88 (1,1) [5667,0]. true => _t52 [ Unit Resolution, 3, 4471, _t0 ] [ Modal Level Pure Literal Elimination, _t52 ] % 0.64/0.88 (103,1) [5672,0]. true => ~box 1~ _t53 [ LHS Unit Resolution, 5667, 4470, _t52 ] [ SNF++, 7056, _t53 ] % 0.64/0.88 (103,1) [7056,0]. true => ~box 1~ _t208 [ SNF++, 5672 ] % 0.64/0.88 (103,1) [63638,0]. true => false [ GEN1 Unit Resolution, 63505, 7056, _t208 ] % 0.64/0.88 (35,1) [1383,1]. _t41 => ~box 1~ p1 [ Axiom 5 ] [ SNF++, 6628, p1 ] % 0.64/0.88 (1,1) [1924,1]. _t47 => box 1 p1 [ Axiom 5 ] [ SNF++, 6752, p1 ] % 0.64/0.88 (1,1) [1926,1]. ~_t89 => box 1 ~_t47 [ Axiom 5 ] [ SNF++, 6754, ~_t47 ] % 0.64/0.88 (1,1) [1928,1]. true => ~_t89 | _t47 [ Axiom 5 ] % 0.64/0.88 (39,1) [2151,1]. _t48 => ~box 1~ ~p1 [ Axiom 5 ] [ SNF++, 6646, ~p1 ] % 0.64/0.88 (103,1) [4467,1]. true => ~_t53 | _t48 [ SNF ] % 0.64/0.88 (102,1) [4468,1]. _t54 => ~box 1~ _t47 [ SNF ] [ SNF++, 6640, _t47 ] % 0.64/0.88 (103,1) [4469,1]. true => _t54 | ~_t53 [ SNF ] % 0.64/0.88 (102,1) [6640,1]. _t54 => ~box 1~ _t118 [ SNF++, 4468 ] % 0.64/0.88 (39,1) [6646,1]. _t48 => ~box 1~ _t120 [ SNF++, 2151 ] % 0.64/0.88 (1,1) [6752,1]. _t47 => box 1 _t113 [ SNF++, 1924 ] % 0.64/0.88 (1,1) [6754,1]. ~_t89 => box 1 _t166 [ SNF++, 1926 ] % 0.64/0.88 (103,1) [7057,1]. true => ~_t208 | _t53 [ SNF++, 5672 ] % 0.64/0.88 (103,1) [11244,1]. true => ~_t208 | _t54 [ LRES, 4469, 7057, ~_t53 ] % 0.64/0.88 (39,1) [13855,1]. true => ~_t48 | ~_t47 [ GEN1, 6752, 6646, 11296, _t113, _t120 ] % 0.64/0.88 (102,1) [17007,1]. true => _t89 | ~_t54 [ GEN1, 6754, 6640, 11926, _t166, _t118 ] % 0.64/0.88 (39,1) [52188,1]. true => ~_t89 | ~_t48 [ LRES, 13855, 1928, ~_t47 ] % 0.64/0.88 (103,1) [57091,1]. true => ~_t89 | ~_t53 [ LRES, 52188, 4467, ~_t48 ] % 0.64/0.88 (103,1) [58108,1]. true => ~_t208 | _t89 [ LRES, 17007, 11244, ~_t54 ] % 0.64/0.88 (103,1) [61505,1]. true => ~_t208 | ~_t89 [ LRES, 57091, 7057, ~_t53 ] % 0.64/0.88 (103,1) [63505,1]. true => ~_t208 [ LRES, 61505, 58108, ~_t89 ] % 0.64/0.88 (35,1) [6629,2]. true => ~_t113 | p1 [ SNF++, 1383 ] % 0.64/0.88 (102,1) [6641,2]. true => ~_t118 | _t47 [ SNF++, 4468 ] % 0.64/0.88 (39,1) [6647,2]. true => ~_t120 | ~p1 [ SNF++, 2151 ] % 0.64/0.88 (1,1) [6755,2]. true => ~_t166 | ~_t47 [ SNF++, 1926 ] % 0.64/0.88 (39,1) [11296,2]. true => ~_t120 | ~_t113 [ LRES, 6647, 6629, ~p1 ] % 0.64/0.88 (102,1) [11926,2]. true => ~_t166 | ~_t118 [ LRES, 6755, 6641, ~_t47 ] % 0.64/0.88 % SZS output end Refutation % 0.64/0.89 % KSP exiting %------------------------------------------------------------------------------