%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP101_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n006.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.26s 0.53s % Output : Refutation 0.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SYP101_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.13/0.32 % Computer : n006.cluster.edu % 0.13/0.32 % Model : x86_64 x86_64 % 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.32 % Memory : 8042.1875MB % 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.32 % CPULimit : 300 % 0.13/0.32 % WCLimit : 300 % 0.13/0.32 % DateTime : Mon May 4 17:36:45 EDT 2026 % 0.13/0.32 % CPUTime : % 0.26/0.52 ----KSP format--- % 0.26/0.52 set(box,REF). % 0.26/0.52 usable(formulas). % 0.26/0.52 true. % 0.26/0.52 end_of_list. % 0.26/0.52 sos(formulas). % 0.26/0.52 ~ ([] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( [] ( $false ) ) | <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) | <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) | <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) | <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( [] ( $false ) ) ) | <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) | <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) | <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) | <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( [] ( $false ) ) ) ) | <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) | <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) | <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) | <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) | <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) ) ) ) ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( <> ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( $false ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( p0 ) & <> ( <> ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( [] ( <> ( p0 ) ) & <> ( <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( p0 & <> ( [] ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p0 ) & <> ( [] ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ). % 0.26/0.52 end_of_list. % 0.26/0.52 ----------------- % 0.26/0.52 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.FSGXRRw0kw/theBenchmark.ksp % 0.26/0.53 % 0.26/0.53 % SZS status Theorem % 0.26/0.53 % 0.26/0.53 ***************** % 0.26/0.53 FOUND PROOF 1 % 0.26/0.53 ***************** % 0.26/0.53 % SZS output start Refutation % 0.26/0.53 % 0.26/0.53 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.26/0.53 (141,1) [842,0]. _t65 => ~box 1~ _t66 [ SNF ] [ Backward Subsumption, 946 ] % 0.26/0.53 (1,1) [843,0]. true => _t65 | ~_t0 [ SNF ] [ Backward Subsumption, 845 ] % 0.26/0.53 (1,1) [845,0]. true => _t65 [ Unit Resolution, 3, 843, _t0 ] [ Modal Level Pure Literal Elimination, _t65 ] % 0.26/0.53 (141,1) [946,0]. true => ~box 1~ _t66 [ LHS Unit Resolution, 845, 842, _t65 ] [ SNF++, 1766, _t66 ] % 0.26/0.53 (141,1) [1766,0]. true => ~box 1~ _t143 [ SNF++, 946 ] % 0.26/0.53 (141,1) [1919,0]. true => false [ GEN1 Unit Resolution, 1918, 1766, _t143 ] % 0.26/0.53 (140,1) [841,1]. _t66 => ~box 1~ _t67 [ SNF ] [ SNF++, 1648, _t67 ] % 0.26/0.53 (140,1) [1648,1]. _t66 => ~box 1~ _t137 [ SNF++, 841 ] [ Backward Subsumption, 1917 ] % 0.26/0.53 (141,1) [1767,1]. true => ~_t143 | _t66 [ SNF++, 946 ] [ Backward Subsumption, 1918 ] % 0.26/0.53 (140,1) [1917,1]. true => ~_t66 [ GEN1 Unit Resolution, 1916, 1648, _t137 ] [ Modal Level Pure Literal Elimination, ~_t66 ] % 0.26/0.53 (141,1) [1918,1]. true => ~_t143 [ Unit Resolution, 1917, 1767, _t66 ] % 0.26/0.53 (139,1) [840,2]. _t67 => ~box 1~ _t68 [ SNF ] [ SNF++, 1538, _t68 ] % 0.26/0.53 (139,1) [1538,2]. _t67 => ~box 1~ _t131 [ SNF++, 840 ] [ Backward Subsumption, 1915 ] % 0.26/0.53 (140,1) [1649,2]. true => ~_t137 | _t67 [ SNF++, 841 ] [ Backward Subsumption, 1916 ] % 0.26/0.53 (139,1) [1915,2]. true => ~_t67 [ GEN1 Unit Resolution, 1914, 1538, _t131 ] [ Modal Level Pure Literal Elimination, ~_t67 ] % 0.26/0.53 (140,1) [1916,2]. true => ~_t137 [ Unit Resolution, 1915, 1649, _t67 ] [ Modal Level Pure Literal Elimination, ~_t137 ] % 0.26/0.53 (138,1) [839,3]. _t68 => ~box 1~ _t69 [ SNF ] [ SNF++, 1438, _t69 ] % 0.26/0.53 (138,1) [1438,3]. _t68 => ~box 1~ _t125 [ SNF++, 839 ] [ Backward Subsumption, 1913 ] % 0.26/0.53 (139,1) [1539,3]. true => ~_t131 | _t68 [ SNF++, 840 ] [ Backward Subsumption, 1914 ] % 0.26/0.53 (138,1) [1913,3]. true => ~_t68 [ GEN1 Unit Resolution, 1912, 1438, _t125 ] [ Modal Level Pure Literal Elimination, ~_t68 ] % 0.26/0.53 (139,1) [1914,3]. true => ~_t131 [ Unit Resolution, 1913, 1539, _t68 ] [ Modal Level Pure Literal Elimination, ~_t131 ] % 0.26/0.53 (137,1) [838,4]. _t69 => ~box 1~ _t70 [ SNF ] [ SNF++, 1348, _t70 ] % 0.26/0.53 (137,1) [1348,4]. _t69 => ~box 1~ _t119 [ SNF++, 838 ] [ Backward Subsumption, 1911 ] % 0.26/0.53 (138,1) [1439,4]. true => ~_t125 | _t69 [ SNF++, 839 ] [ Backward Subsumption, 1912 ] % 0.26/0.53 (137,1) [1911,4]. true => ~_t69 [ GEN1 Unit Resolution, 1910, 1348, _t119 ] [ Modal Level Pure Literal Elimination, ~_t69 ] % 0.26/0.53 (138,1) [1912,4]. true => ~_t125 [ Unit Resolution, 1911, 1439, _t69 ] [ Modal Level Pure Literal Elimination, ~_t125 ] % 0.26/0.53 (136,1) [837,5]. _t70 => ~box 1~ _t71 [ SNF ] [ SNF++, 1268, _t71 ] % 0.26/0.53 (136,1) [1268,5]. _t70 => ~box 1~ _t113 [ SNF++, 837 ] [ Backward Subsumption, 1909 ] % 0.26/0.53 (137,1) [1349,5]. true => ~_t119 | _t70 [ SNF++, 838 ] [ Backward Subsumption, 1910 ] % 0.26/0.53 (136,1) [1909,5]. true => ~_t70 [ GEN1 Unit Resolution, 1908, 1268, _t113 ] [ Modal Level Pure Literal Elimination, ~_t70 ] % 0.26/0.53 (137,1) [1910,5]. true => ~_t119 [ Unit Resolution, 1909, 1349, _t70 ] [ Modal Level Pure Literal Elimination, ~_t119 ] % 0.35/0.53 (135,1) [836,6]. _t71 => ~box 1~ _t72 [ SNF ] [ SNF++, 1198, _t72 ] % 0.35/0.53 (135,1) [1198,6]. _t71 => ~box 1~ _t107 [ SNF++, 836 ] [ Backward Subsumption, 1907 ] % 0.35/0.53 (136,1) [1269,6]. true => ~_t113 | _t71 [ SNF++, 837 ] [ Backward Subsumption, 1908 ] % 0.35/0.53 (135,1) [1907,6]. true => ~_t71 [ GEN1 Unit Resolution, 1906, 1198, _t107 ] [ Modal Level Pure Literal Elimination, ~_t71 ] % 0.35/0.53 (136,1) [1908,6]. true => ~_t113 [ Unit Resolution, 1907, 1269, _t71 ] [ Modal Level Pure Literal Elimination, ~_t113 ] % 0.35/0.53 (134,1) [835,7]. _t72 => ~box 1~ _t73 [ SNF ] [ SNF++, 1138, _t73 ] % 0.35/0.53 (134,1) [1138,7]. _t72 => ~box 1~ _t101 [ SNF++, 835 ] [ Backward Subsumption, 1905 ] % 0.35/0.53 (135,1) [1199,7]. true => ~_t107 | _t72 [ SNF++, 836 ] [ Backward Subsumption, 1906 ] % 0.35/0.53 (134,1) [1905,7]. true => ~_t72 [ GEN1 Unit Resolution, 1904, 1138, _t101 ] [ Modal Level Pure Literal Elimination, ~_t72 ] % 0.35/0.53 (135,1) [1906,7]. true => ~_t107 [ Unit Resolution, 1905, 1199, _t72 ] [ Modal Level Pure Literal Elimination, ~_t107 ] % 0.35/0.54 (133,1) [834,8]. _t73 => ~box 1~ _t74 [ SNF ] [ SNF++, 1088, _t74 ] % 0.35/0.54 (133,1) [1088,8]. _t73 => ~box 1~ _t95 [ SNF++, 834 ] [ Backward Subsumption, 1903 ] % 0.35/0.54 (134,1) [1139,8]. true => ~_t101 | _t73 [ SNF++, 835 ] [ Backward Subsumption, 1904 ] % 0.35/0.54 (133,1) [1903,8]. true => ~_t73 [ GEN1 Unit Resolution, 1902, 1088, _t95 ] [ Modal Level Pure Literal Elimination, ~_t73 ] % 0.35/0.54 (134,1) [1904,8]. true => ~_t101 [ Unit Resolution, 1903, 1139, _t73 ] [ Modal Level Pure Literal Elimination, ~_t101 ] % 0.35/0.54 (132,1) [833,9]. _t74 => ~box 1~ _t75 [ SNF ] [ SNF++, 1048, _t75 ] % 0.35/0.54 (132,1) [1048,9]. _t74 => ~box 1~ _t89 [ SNF++, 833 ] [ Backward Subsumption, 1901 ] % 0.35/0.54 (133,1) [1089,9]. true => ~_t95 | _t74 [ SNF++, 834 ] [ Backward Subsumption, 1902 ] % 0.35/0.54 (132,1) [1901,9]. true => ~_t74 [ GEN1 Unit Resolution, 1900, 1048, _t89 ] [ Modal Level Pure Literal Elimination, ~_t74 ] % 0.35/0.54 (133,1) [1902,9]. true => ~_t95 [ Unit Resolution, 1901, 1089, _t74 ] [ Modal Level Pure Literal Elimination, ~_t95 ] % 0.35/0.54 (1,1) [623,10]. true => ~_t64 | p0 [ Axiom T ] % 0.35/0.54 (132,1) [831,10]. true => ~_t75 | ~p0 [ SNF ] [ Modal Level Pure Literal Elimination, ~_t75 ] % 0.35/0.54 (132,1) [832,10]. true => ~_t75 | _t64 [ SNF ] [ Modal Level Pure Literal Elimination, ~_t75 ] % 0.35/0.54 (132,1) [1049,10]. true => ~_t89 | _t75 [ SNF++, 833 ] [ Backward Subsumption, 1900 ] % 0.35/0.54 (132,1) [1838,10]. true => ~_t75 | ~_t64 [ LRES, 831, 623, ~p0 ] [ Modal Level Pure Literal Elimination, ~_t75 ] % 0.35/0.54 (132,1) [1897,10]. true => ~_t75 [ LRES, 1838, 832, ~_t64 ] [ Modal Level Pure Literal Elimination, ~_t75 ] % 0.35/0.54 (132,1) [1900,10]. true => ~_t89 [ Unit Resolution, 1897, 1049, _t75 ] [ Modal Level Pure Literal Elimination, ~_t89 ] % 0.35/0.54 % SZS output end Refutation % 0.35/0.54 % KSP exiting %------------------------------------------------------------------------------