%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP066_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n023.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.47s 0.63s % Output : Refutation 0.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP066_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.12 % Command : run_ksp %s % 0.15/0.33 % Computer : n023.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Mon May 4 17:07:38 EDT 2026 % 0.15/0.34 % CPUTime : % 0.39/0.59 ----KSP format--- % 0.39/0.59 set(box,SYM). % 0.39/0.59 usable(formulas). % 0.39/0.59 true. % 0.39/0.59 end_of_list. % 0.39/0.59 sos(formulas). % 0.39/0.59 ~ (( [] ( [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) ) & [] ( [] ( [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) ) ) & [] ( [] ( [] ( [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( [] ( [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) ) ) ) ) ) & ~ ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> p0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) -> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> [] ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) ) ) & [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( ( p0 -> [] ( p0 ) ) -> [] ( ( p0 -> [] ( p0 ) ) ) ) ) -> ( p0 -> [] ( p0 ) ) ) ) -> ( <> ( [] ( ( p0 -> [] ( p0 ) ) ) ) -> ( ( p0 -> [] ( p0 ) ) | [] ( ( p0 -> [] ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( [] ( ( [] ( p0 ) -> [] ( [] ( p0 ) ) ) ) & ( [] ( ( [] ( ( p0 -> [] ( p0 ) ) ) -> p0 ) ) -> ( <> ( [] ( p0 ) ) -> ( p0 | [] ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ). % 0.39/0.59 end_of_list. % 0.39/0.59 ----------------- % 0.39/0.59 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.r2zmMmCGW5/theBenchmark.ksp % 0.47/0.63 % 0.47/0.63 % SZS status Theorem % 0.47/0.63 % 0.47/0.63 ***************** % 0.47/0.63 FOUND PROOF 1 % 0.47/0.63 ***************** % 0.47/0.63 % SZS output start Refutation % 0.47/0.63 % 0.47/0.63 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.47/0.63 (107,1) [718,0]. _t46 => ~box 1~ _t47 [ SNF ] [ Backward Subsumption, 738 ] % 0.47/0.63 (1,1) [719,0]. true => _t46 | ~_t0 [ SNF ] [ Backward Subsumption, 720 ] % 0.47/0.63 (1,1) [720,0]. true => _t46 [ Unit Resolution, 3, 719, _t0 ] [ Modal Level Pure Literal Elimination, _t46 ] % 0.47/0.63 (107,1) [738,0]. true => ~box 1~ _t47 [ LHS Unit Resolution, 720, 718, _t46 ] [ SNF++, 1484, _t47 ] % 0.47/0.63 (107,1) [1484,0]. true => ~box 1~ _t156 [ SNF++, 738 ] % 0.47/0.63 (107,1) [2417,0]. true => false [ GEN1 Unit Resolution, 2416, 1484, _t156 ] % 0.47/0.63 (106,1) [717,1]. _t47 => ~box 1~ _t48 [ SNF ] [ SNF++, 1408, _t48 ] % 0.47/0.63 (106,1) [1408,1]. _t47 => ~box 1~ _t152 [ SNF++, 717 ] [ Backward Subsumption, 2415 ] % 0.47/0.63 (107,1) [1485,1]. true => ~_t156 | _t47 [ SNF++, 738 ] [ Backward Subsumption, 2416 ] % 0.47/0.63 (106,1) [2415,1]. true => ~_t47 [ GEN1 Unit Resolution, 2414, 1408, _t152 ] [ Modal Level Pure Literal Elimination, ~_t47 ] % 0.47/0.63 (107,1) [2416,1]. true => ~_t156 [ Unit Resolution, 2415, 1485, _t47 ] % 0.47/0.63 (105,1) [716,2]. _t48 => ~box 1~ _t49 [ SNF ] [ SNF++, 1320, _t49 ] % 0.47/0.63 (105,1) [1320,2]. _t48 => ~box 1~ _t147 [ SNF++, 716 ] [ Backward Subsumption, 2413 ] % 0.47/0.63 (106,1) [1409,2]. true => ~_t152 | _t48 [ SNF++, 717 ] [ Backward Subsumption, 2414 ] % 0.47/0.63 (105,1) [2413,2]. true => ~_t48 [ GEN1 Unit Resolution, 2412, 1320, _t147 ] [ Modal Level Pure Literal Elimination, ~_t48 ] % 0.47/0.63 (106,1) [2414,2]. true => ~_t152 [ Unit Resolution, 2413, 1409, _t48 ] [ Modal Level Pure Literal Elimination, ~_t152 ] % 0.47/0.63 (104,1) [715,3]. _t49 => ~box 1~ _t50 [ SNF ] [ SNF++, 1240, _t50 ] % 0.47/0.63 (104,1) [1240,3]. _t49 => ~box 1~ _t142 [ SNF++, 715 ] [ Backward Subsumption, 2411 ] % 0.47/0.63 (105,1) [1321,3]. true => ~_t147 | _t49 [ SNF++, 716 ] [ Backward Subsumption, 2412 ] % 0.47/0.63 (104,1) [2411,3]. true => ~_t49 [ GEN1 Unit Resolution, 2410, 1240, _t142 ] [ Modal Level Pure Literal Elimination, ~_t49 ] % 0.47/0.63 (105,1) [2412,3]. true => ~_t147 [ Unit Resolution, 2411, 1321, _t49 ] [ Modal Level Pure Literal Elimination, ~_t147 ] % 0.47/0.63 (103,1) [714,4]. _t50 => ~box 1~ _t51 [ SNF ] [ SNF++, 1164, _t51 ] % 0.47/0.63 (103,1) [1164,4]. _t50 => ~box 1~ _t137 [ SNF++, 714 ] [ Backward Subsumption, 2409 ] % 0.47/0.63 (104,1) [1241,4]. true => ~_t142 | _t50 [ SNF++, 715 ] [ Backward Subsumption, 2410 ] % 0.47/0.63 (103,1) [2409,4]. true => ~_t50 [ GEN1 Unit Resolution, 2408, 1164, _t137 ] [ Modal Level Pure Literal Elimination, ~_t50 ] % 0.47/0.63 (104,1) [2410,4]. true => ~_t142 [ Unit Resolution, 2409, 1241, _t50 ] [ Modal Level Pure Literal Elimination, ~_t142 ] % 0.47/0.63 (102,1) [713,5]. _t51 => ~box 1~ _t52 [ SNF ] [ SNF++, 1096, _t52 ] % 0.47/0.63 (102,1) [1096,5]. _t51 => ~box 1~ _t132 [ SNF++, 713 ] [ Backward Subsumption, 2407 ] % 0.47/0.63 (103,1) [1165,5]. true => ~_t137 | _t51 [ SNF++, 714 ] [ Backward Subsumption, 2408 ] % 0.47/0.63 (102,1) [2407,5]. true => ~_t51 [ GEN1 Unit Resolution, 2406, 1096, _t132 ] [ Modal Level Pure Literal Elimination, ~_t51 ] % 0.47/0.63 (103,1) [2408,5]. true => ~_t137 [ Unit Resolution, 2407, 1165, _t51 ] [ Modal Level Pure Literal Elimination, ~_t137 ] % 0.47/0.63 (101,1) [712,6]. _t52 => ~box 1~ _t53 [ SNF ] [ SNF++, 1032, _t53 ] % 0.47/0.63 (101,1) [1032,6]. _t52 => ~box 1~ _t127 [ SNF++, 712 ] [ Backward Subsumption, 2405 ] % 0.47/0.63 (102,1) [1097,6]. true => ~_t132 | _t52 [ SNF++, 713 ] [ Backward Subsumption, 2406 ] % 0.47/0.63 (101,1) [2405,6]. true => ~_t52 [ GEN1 Unit Resolution, 2404, 1032, _t127 ] [ Modal Level Pure Literal Elimination, ~_t52 ] % 0.47/0.63 (102,1) [2406,6]. true => ~_t132 [ Unit Resolution, 2405, 1097, _t52 ] [ Modal Level Pure Literal Elimination, ~_t132 ] % 0.47/0.63 (100,1) [711,7]. _t53 => ~box 1~ _t54 [ SNF ] [ SNF++, 976, _t54 ] % 0.47/0.63 (100,1) [976,7]. _t53 => ~box 1~ _t122 [ SNF++, 711 ] [ Backward Subsumption, 2403 ] % 0.47/0.63 (101,1) [1033,7]. true => ~_t127 | _t53 [ SNF++, 712 ] [ Backward Subsumption, 2404 ] % 0.47/0.63 (100,1) [2403,7]. true => ~_t53 [ GEN1 Unit Resolution, 2402, 976, _t122 ] [ Modal Level Pure Literal Elimination, ~_t53 ] % 0.47/0.63 (101,1) [2404,7]. true => ~_t127 [ Unit Resolution, 2403, 1033, _t53 ] [ Modal Level Pure Literal Elimination, ~_t127 ] % 0.47/0.63 (99,1) [710,8]. _t54 => ~box 1~ _t55 [ SNF ] [ SNF++, 920, _t55 ] % 0.47/0.63 (99,1) [920,8]. _t54 => ~box 1~ _t117 [ SNF++, 710 ] [ Backward Subsumption, 2401 ] % 0.47/0.63 (100,1) [977,8]. true => ~_t122 | _t54 [ SNF++, 711 ] [ Backward Subsumption, 2402 ] % 0.47/0.63 (99,1) [2401,8]. true => ~_t54 [ GEN1 Unit Resolution, 2400, 920, _t117 ] [ Modal Level Pure Literal Elimination, ~_t54 ] % 0.47/0.63 (100,1) [2402,8]. true => ~_t122 [ Unit Resolution, 2401, 977, _t54 ] [ Modal Level Pure Literal Elimination, ~_t122 ] % 0.47/0.63 (98,1) [709,9]. _t55 => ~box 1~ _t56 [ SNF ] [ SNF++, 876, _t56 ] % 0.47/0.63 (98,1) [876,9]. _t55 => ~box 1~ _t113 [ SNF++, 709 ] [ Backward Subsumption, 2399 ] % 0.47/0.63 (99,1) [921,9]. true => ~_t117 | _t55 [ SNF++, 710 ] [ Backward Subsumption, 2400 ] % 0.47/0.63 (98,1) [2399,9]. true => ~_t55 [ GEN1 Unit Resolution, 2398, 876, _t113 ] [ Modal Level Pure Literal Elimination, ~_t55 ] % 0.47/0.63 (99,1) [2400,9]. true => ~_t117 [ Unit Resolution, 2399, 921, _t55 ] [ Modal Level Pure Literal Elimination, ~_t117 ] % 0.47/0.63 (97,1) [708,10]. _t56 => ~box 1~ _t57 [ SNF ] [ SNF++, 838, _t57 ] % 0.47/0.63 (97,1) [838,10]. _t56 => ~box 1~ _t110 [ SNF++, 708 ] [ Backward Subsumption, 2394 ] % 0.47/0.63 (98,1) [877,10]. true => ~_t113 | _t56 [ SNF++, 709 ] [ Backward Subsumption, 2398 ] % 0.47/0.63 (97,1) [2394,10]. true => ~_t56 [ GEN1 Unit Resolution, 2377, 838, _t110 ] [ Modal Level Pure Literal Elimination, ~_t56 ] % 0.47/0.63 (98,1) [2398,10]. true => ~_t113 [ Unit Resolution, 2394, 877, _t56 ] [ Modal Level Pure Literal Elimination, ~_t113 ] % 0.47/0.63 (1,1) [76,11]. _t60 => box 1 ~_t16 [ Axiom SYM ] [ SNF++, 790, ~_t16 ] % 0.47/0.63 (1,1) [77,11]. true => _t60 | p0 [ Axiom SYM ] % 0.47/0.63 (97,1) [699,11]. true => ~_t57 | ~p0 [ SNF ] [ Modal Level Pure Literal Elimination, ~_t57 ] % 0.47/0.63 (94,1) [706,11]. _t58 => ~box 1~ _t16 [ SNF ] [ SNF++, 806, _t16 ] % 0.47/0.63 (97,1) [707,11]. true => _t58 | ~_t57 [ SNF ] [ Modal Level Pure Literal Elimination, ~_t57 ] % 0.47/0.63 (1,1) [790,11]. _t60 => box 1 _t88 [ SNF++, 76 ] % 0.47/0.63 (94,1) [806,11]. _t58 => ~box 1~ _t92 [ SNF++, 706 ] [ Backward Subsumption, 2395 ] % 0.47/0.63 (97,1) [839,11]. true => ~_t110 | _t57 [ SNF++, 708 ] [ Modal Level Pure Literal Elimination, ~_t110 ] % 0.47/0.63 (97,1) [1659,11]. true => _t60 | ~_t57 [ LRES, 699, 77, ~p0 ] [ Modal Level Pure Literal Elimination, ~_t57 ] % 0.47/0.63 (97,1) [1709,11]. true => ~_t110 | _t60 [ LRES, 1659, 839, ~_t57 ] [ Modal Level Pure Literal Elimination, ~_t110 ] % 0.47/0.63 (97,1) [1724,11]. true => ~_t110 | _t58 [ LRES, 707, 839, ~_t57 ] [ Modal Level Pure Literal Elimination, ~_t110 ] % 0.47/0.63 (94,1) [1963,11]. true => ~_t60 | ~_t58 [ GEN1, 790, 806, 1796, _t88, _t92 ] [ Modal Level Pure Literal Elimination, ~_t58 ] % 0.47/0.63 (97,1) [2132,11]. true => ~_t110 | ~_t60 [ LRES, 1963, 1724, ~_t58 ] [ Modal Level Pure Literal Elimination, ~_t110 ] % 0.47/0.63 (97,1) [2377,11]. true => ~_t110 [ LRES, 2132, 1709, ~_t60 ] [ Modal Level Pure Literal Elimination, ~_t110 ] % 0.47/0.63 (1,1) [791,12]. true => ~_t88 | ~_t16 [ SNF++, 76 ] % 0.47/0.63 (94,1) [807,12]. true => ~_t92 | _t16 [ SNF++, 706 ] [ Modal Level Pure Literal Elimination, ~_t92 ] % 0.47/0.63 (94,1) [1796,12]. true => ~_t92 | ~_t88 [ LRES, 791, 807, ~_t16 ] [ Modal Level Pure Literal Elimination, ~_t92 ] % 0.47/0.63 % SZS output end Refutation % 0.47/0.63 % KSP exiting %------------------------------------------------------------------------------