%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP048_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n031.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 0.47s 1.34s % Output : Refutation 0.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.22 % Problem : SYP048_1 : TPTP v9.3.0. Released v9.3.0. % 0.10/0.23 % Command : run_ksp %s % 0.15/0.45 % Computer : n031.cluster.edu % 0.15/0.45 % Model : x86_64 x86_64 % 0.15/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.45 % Memory : 8042.1875MB % 0.15/0.45 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.45 % CPULimit : 300 % 0.15/0.45 % WCLimit : 300 % 0.15/0.45 % DateTime : Mon May 4 16:30:38 EDT 2026 % 0.15/0.45 % CPUTime : % 0.31/1.01 ----KSP format--- % 0.31/1.01 set(box,FIVE). % 0.31/1.01 usable(formulas). % 0.31/1.01 true. % 0.31/1.01 end_of_list. % 0.31/1.01 sos(formulas). % 0.31/1.01 ~ (( [] ( [] ( ( [] ( 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.31/1.01 end_of_list. % 0.31/1.01 ----------------- % 0.31/1.01 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.bn6FX36K9Z/theBenchmark.ksp % 0.47/1.34 % 0.47/1.34 % SZS status Theorem % 0.47/1.34 % 0.47/1.34 ***************** % 0.47/1.34 FOUND PROOF 1 % 0.47/1.34 ***************** % 0.47/1.34 % SZS output start Refutation % 0.47/1.34 % 0.47/1.34 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.47/1.34 (107,1) [4279,0]. _t46 => ~box 1~ _t47 [ SNF ] [ Backward Subsumption, 4331 ] % 0.47/1.34 (1,1) [4280,0]. true => _t46 | ~_t0 [ SNF ] [ Backward Subsumption, 4321 ] % 0.47/1.34 (1,1) [4321,0]. true => _t46 [ Unit Resolution, 3, 4280, _t0 ] [ Modal Level Pure Literal Elimination, _t46 ] % 0.47/1.34 (107,1) [4331,0]. true => ~box 1~ _t47 [ LHS Unit Resolution, 4321, 4279, _t46 ] [ SNF++, 4813, _t47 ] % 0.47/1.34 (107,1) [4813,0]. true => ~box 1~ _t189 [ SNF++, 4331 ] % 0.47/1.34 (107,1) [45449,0]. true => false [ GEN1 Unit Resolution, 45448, 4813, _t189 ] % 0.47/1.34 (106,1) [4278,1]. _t47 => ~box 1~ _t48 [ SNF ] [ SNF++, 5055, _t48 ] % 0.47/1.34 (107,1) [4814,1]. true => ~_t189 | _t47 [ SNF++, 4331 ] [ Backward Subsumption, 45448 ] % 0.47/1.34 (106,1) [5055,1]. _t47 => ~box 1~ _t190 [ SNF++, 4278 ] [ Backward Subsumption, 45447 ] % 0.47/1.34 (106,1) [45447,1]. true => ~_t47 [ GEN1 Unit Resolution, 45446, 5055, _t190 ] [ Modal Level Pure Literal Elimination, ~_t47 ] % 0.47/1.34 (107,1) [45448,1]. true => ~_t189 [ Unit Resolution, 45447, 4814, _t47 ] % 0.47/1.34 (105,1) [4277,2]. _t48 => ~box 1~ _t49 [ SNF ] [ SNF++, 5297, _t49 ] % 0.47/1.34 (106,1) [5056,2]. true => ~_t190 | _t48 [ SNF++, 4278 ] [ Backward Subsumption, 45446 ] % 0.47/1.34 (105,1) [5297,2]. _t48 => ~box 1~ _t191 [ SNF++, 4277 ] [ Backward Subsumption, 45445 ] % 0.47/1.34 (105,1) [45445,2]. true => ~_t48 [ GEN1 Unit Resolution, 45444, 5297, _t191 ] [ Modal Level Pure Literal Elimination, ~_t48 ] % 0.47/1.34 (106,1) [45446,2]. true => ~_t190 [ Unit Resolution, 45445, 5056, _t48 ] [ Modal Level Pure Literal Elimination, ~_t190 ] % 0.47/1.34 (104,1) [4276,3]. _t49 => ~box 1~ _t50 [ SNF ] [ SNF++, 5539, _t50 ] % 0.47/1.34 (105,1) [5298,3]. true => ~_t191 | _t49 [ SNF++, 4277 ] [ Backward Subsumption, 45444 ] % 0.47/1.34 (104,1) [5539,3]. _t49 => ~box 1~ _t192 [ SNF++, 4276 ] [ Backward Subsumption, 45443 ] % 0.47/1.34 (104,1) [45443,3]. true => ~_t49 [ GEN1 Unit Resolution, 45442, 5539, _t192 ] [ Modal Level Pure Literal Elimination, ~_t49 ] % 0.47/1.34 (105,1) [45444,3]. true => ~_t191 [ Unit Resolution, 45443, 5298, _t49 ] [ Modal Level Pure Literal Elimination, ~_t191 ] % 0.47/1.34 (103,1) [4275,4]. _t50 => ~box 1~ _t51 [ SNF ] [ SNF++, 5781, _t51 ] % 0.47/1.34 (104,1) [5540,4]. true => ~_t192 | _t50 [ SNF++, 4276 ] [ Backward Subsumption, 45442 ] % 0.47/1.34 (103,1) [5781,4]. _t50 => ~box 1~ _t193 [ SNF++, 4275 ] [ Backward Subsumption, 45441 ] % 0.47/1.34 (103,1) [45441,4]. true => ~_t50 [ GEN1 Unit Resolution, 45440, 5781, _t193 ] [ Modal Level Pure Literal Elimination, ~_t50 ] % 0.47/1.34 (104,1) [45442,4]. true => ~_t192 [ Unit Resolution, 45441, 5540, _t50 ] [ Modal Level Pure Literal Elimination, ~_t192 ] % 0.47/1.34 (102,1) [4274,5]. _t51 => ~box 1~ _t52 [ SNF ] [ SNF++, 6023, _t52 ] % 0.47/1.34 (103,1) [5782,5]. true => ~_t193 | _t51 [ SNF++, 4275 ] [ Backward Subsumption, 45440 ] % 0.47/1.34 (102,1) [6023,5]. _t51 => ~box 1~ _t194 [ SNF++, 4274 ] [ Backward Subsumption, 45439 ] % 0.47/1.34 (102,1) [45439,5]. true => ~_t51 [ GEN1 Unit Resolution, 45438, 6023, _t194 ] [ Modal Level Pure Literal Elimination, ~_t51 ] % 0.47/1.34 (103,1) [45440,5]. true => ~_t193 [ Unit Resolution, 45439, 5782, _t51 ] [ Modal Level Pure Literal Elimination, ~_t193 ] % 0.47/1.34 (101,1) [4273,6]. _t52 => ~box 1~ _t53 [ SNF ] [ SNF++, 6265, _t53 ] % 0.47/1.34 (102,1) [6024,6]. true => ~_t194 | _t52 [ SNF++, 4274 ] [ Backward Subsumption, 45438 ] % 0.47/1.34 (101,1) [6265,6]. _t52 => ~box 1~ _t195 [ SNF++, 4273 ] [ Backward Subsumption, 45437 ] % 0.47/1.34 (101,1) [45437,6]. true => ~_t52 [ GEN1 Unit Resolution, 45436, 6265, _t195 ] [ Modal Level Pure Literal Elimination, ~_t52 ] % 0.47/1.34 (102,1) [45438,6]. true => ~_t194 [ Unit Resolution, 45437, 6024, _t52 ] [ Modal Level Pure Literal Elimination, ~_t194 ] % 0.47/1.34 (100,1) [4272,7]. _t53 => ~box 1~ _t54 [ SNF ] [ SNF++, 6507, _t54 ] % 0.47/1.34 (101,1) [6266,7]. true => ~_t195 | _t53 [ SNF++, 4273 ] [ Backward Subsumption, 45436 ] % 0.47/1.34 (100,1) [6507,7]. _t53 => ~box 1~ _t196 [ SNF++, 4272 ] [ Backward Subsumption, 45435 ] % 0.47/1.34 (100,1) [45435,7]. true => ~_t53 [ GEN1 Unit Resolution, 45434, 6507, _t196 ] [ Modal Level Pure Literal Elimination, ~_t53 ] % 0.47/1.34 (101,1) [45436,7]. true => ~_t195 [ Unit Resolution, 45435, 6266, _t53 ] [ Modal Level Pure Literal Elimination, ~_t195 ] % 0.47/1.34 (99,1) [4271,8]. _t54 => ~box 1~ _t55 [ SNF ] [ SNF++, 6749, _t55 ] % 0.47/1.34 (100,1) [6508,8]. true => ~_t196 | _t54 [ SNF++, 4272 ] [ Backward Subsumption, 45434 ] % 0.47/1.34 (99,1) [6749,8]. _t54 => ~box 1~ _t197 [ SNF++, 4271 ] [ Backward Subsumption, 45433 ] % 0.47/1.34 (99,1) [45433,8]. true => ~_t54 [ GEN1 Unit Resolution, 45432, 6749, _t197 ] [ Modal Level Pure Literal Elimination, ~_t54 ] % 0.47/1.34 (100,1) [45434,8]. true => ~_t196 [ Unit Resolution, 45433, 6508, _t54 ] [ Modal Level Pure Literal Elimination, ~_t196 ] % 0.47/1.34 (98,1) [4270,9]. _t55 => ~box 1~ _t56 [ SNF ] [ SNF++, 6991, _t56 ] % 0.47/1.34 (99,1) [6750,9]. true => ~_t197 | _t55 [ SNF++, 4271 ] [ Backward Subsumption, 45432 ] % 0.47/1.34 (98,1) [6991,9]. _t55 => ~box 1~ _t198 [ SNF++, 4270 ] [ Backward Subsumption, 45429 ] % 0.47/1.34 (98,1) [45429,9]. true => ~_t55 [ GEN1 Unit Resolution, 45389, 6991, _t198 ] [ Modal Level Pure Literal Elimination, ~_t55 ] % 0.47/1.34 (99,1) [45432,9]. true => ~_t197 [ Unit Resolution, 45429, 6750, _t55 ] [ Modal Level Pure Literal Elimination, ~_t197 ] % 0.47/1.34 (1,1) [55,10]. _t16 => box 1 p0 [ Axiom 5 ] [ SNF++, 6993, p0 ] % 0.47/1.34 (1,1) [57,10]. ~_t60 => box 1 ~_t16 [ Axiom 5 ] [ SNF++, 6995, ~_t16 ] % 0.47/1.34 (1,1) [59,10]. true => ~_t60 | _t16 [ Axiom 5 ] % 0.47/1.34 (97,1) [4269,10]. _t56 => ~box 1~ _t57 [ SNF ] [ SNF++, 7233, _t57 ] % 0.47/1.34 (98,1) [6992,10]. true => ~_t198 | _t56 [ SNF++, 4270 ] [ Modal Level Pure Literal Elimination, ~_t198 ] % 0.47/1.34 (1,1) [6993,10]. _t16 => box 1 _t89 [ SNF++, 55 ] % 0.47/1.34 (1,1) [6995,10]. ~_t60 => box 1 _t90 [ SNF++, 57 ] % 0.47/1.34 (97,1) [7233,10]. _t56 => ~box 1~ _t199 [ SNF++, 4269 ] [ Backward Subsumption, 45430 ] % 0.47/1.34 (97,1) [10900,10]. true => ~_t56 | ~_t16 [ GEN1, 6993, 7233, 9091, _t89, _t199 ] [ Modal Level Pure Literal Elimination, ~_t56 ] % 0.47/1.34 (97,1) [40918,10]. true => ~_t60 | ~_t56 [ LRES, 10900, 59, ~_t16 ] [ Modal Level Pure Literal Elimination, ~_t56 ] % 0.47/1.34 (98,1) [41218,10]. true => ~_t198 | ~_t60 [ LRES, 40918, 6992, ~_t56 ] [ Modal Level Pure Literal Elimination, ~_t198 ] % 0.47/1.34 (97,1) [44964,10]. true => _t60 | ~_t56 [ GEN1, 6995, 7233, 42463, _t90, _t199 ] [ Modal Level Pure Literal Elimination, ~_t56 ] % 0.47/1.34 (98,1) [45177,10]. true => ~_t198 | _t60 [ LRES, 44964, 6992, ~_t56 ] [ Modal Level Pure Literal Elimination, ~_t198 ] % 0.47/1.34 (98,1) [45389,10]. true => ~_t198 [ LRES, 45177, 41218, _t60 ] [ Modal Level Pure Literal Elimination, ~_t198 ] % 0.47/1.34 (1,1) [62,11]. ~_t60 => box 1 ~_t16 [ Axiom 5 ] [ SNF++, 7237, ~_t16 ] % 0.47/1.34 (1,1) [64,11]. true => ~_t60 | _t16 [ Axiom 5 ] % 0.47/1.34 (1,1) [162,11]. _t15 => box 1 _t16 [ Axiom 5 ] [ SNF++, 7241, _t16 ] % 0.47/1.34 (97,1) [4265,11]. true => ~_t57 | ~p0 [ SNF ] [ Modal Level Pure Literal Elimination, ~_t57 ] % 0.47/1.34 (94,1) [4267,11]. _t58 => ~box 1~ _t16 [ SNF ] [ SNF++, 7409, _t16 ] % 0.47/1.34 (97,1) [4268,11]. true => _t58 | ~_t57 [ SNF ] [ Modal Level Pure Literal Elimination, ~_t57 ] % 0.47/1.34 (1,1) [6994,11]. true => ~_t89 | p0 [ SNF++, 55 ] % 0.47/1.34 (1,1) [6996,11]. true => ~_t90 | ~_t16 [ SNF++, 57 ] % 0.47/1.34 (97,1) [7234,11]. true => ~_t199 | _t57 [ SNF++, 4269 ] [ Modal Level Pure Literal Elimination, ~_t199 ] % 0.47/1.34 (1,1) [7237,11]. ~_t60 => box 1 _t90 [ SNF++, 62 ] % 0.47/1.34 (94,1) [7409,11]. _t58 => ~box 1~ _t92 [ SNF++, 4267 ] [ Backward Subsumption, 45431 ] % 0.47/1.34 (97,1) [8825,11]. true => ~_t89 | ~_t57 [ LRES, 4265, 6994, ~p0 ] [ Modal Level Pure Literal Elimination, ~_t57 ] % 0.47/1.34 (97,1) [9091,11]. true => ~_t199 | ~_t89 [ LRES, 8825, 7234, ~_t57 ] [ Modal Level Pure Literal Elimination, ~_t199 ] % 0.47/1.34 (97,1) [9125,11]. true => ~_t199 | _t58 [ LRES, 4268, 7234, ~_t57 ] [ Modal Level Pure Literal Elimination, ~_t199 ] % 0.47/1.34 (1,1) [9159,11]. true => ~_t90 | ~_t60 [ LRES, 6996, 64, ~_t16 ] % 0.47/1.34 (94,1) [11913,11]. true => _t60 | ~_t58 [ GEN1, 7237, 7409, 8976, _t90, _t92 ] [ Modal Level Pure Literal Elimination, ~_t58 ] % 0.47/1.34 (97,1) [41449,11]. true => ~_t199 | _t60 [ LRES, 11913, 9125, ~_t58 ] [ Modal Level Pure Literal Elimination, ~_t199 ] % 0.47/1.34 (97,1) [42463,11]. true => ~_t199 | ~_t90 [ LRES, 41449, 9159, _t60 ] [ Modal Level Pure Literal Elimination, ~_t199 ] % 0.47/1.34 (1,1) [7238,12]. true => ~_t90 | ~_t16 [ SNF++, 62 ] % 0.47/1.34 (1,1) [7242,12]. true => ~_t92 | _t16 [ SNF++, 162 ] % 0.47/1.34 (1,1) [8976,12]. true => ~_t92 | ~_t90 [ LRES, 7238, 7242, ~_t16 ] % 0.47/1.36 % SZS output end Refutation % 0.47/1.36 % KSP exiting %------------------------------------------------------------------------------