%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP104_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:59 PM UTC 2026 % Result : Theorem 0.35s 0.63s % Output : Refutation 0.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP104_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.13/0.32 % Computer : n023.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:39:53 EDT 2026 % 0.13/0.32 % CPUTime : % 0.24/0.52 ----KSP format--- % 0.24/0.52 set(box,REF). % 0.24/0.52 usable(formulas). % 0.24/0.52 true. % 0.24/0.52 end_of_list. % 0.24/0.52 sos(formulas). % 0.24/0.52 ~ (( [] ( ( [] ( ( [] ( ( 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.24/0.52 end_of_list. % 0.24/0.52 ----------------- % 0.24/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.90x3oWR2Im/theBenchmark.ksp % 0.35/0.63 % 0.35/0.63 % SZS status Theorem % 0.35/0.63 % 0.35/0.63 ***************** % 0.35/0.63 FOUND PROOF 1 % 0.35/0.63 ***************** % 0.35/0.63 % SZS output start Refutation % 0.35/0.63 % 0.35/0.63 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.35/0.63 (1,1) [6,0]. true => ~_t0 | ~p2 [ SNF ] [ Backward Subsumption, 480 ] % 0.35/0.63 (1,1) [22,0]. true => _t2 | ~_t1 [ Axiom T ] [ Backward Subsumption, 496 ] % 0.35/0.63 (1,1) [24,0]. true => ~_t3 | p2 [ Axiom T ] [ Backward Subsumption, 510 ] % 0.35/0.63 (18,1) [30,0]. _t4 => ~box 1~ _t5 [ Axiom T ] [ Backward Subsumption, 543 ] % 0.35/0.63 (1,1) [31,0]. true => _t4 | _t3 | ~_t2 [ Axiom T ] [ Backward Subsumption, 533 ] % 0.35/0.63 (1,1) [32,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 479 ] % 0.35/0.63 (1,1) [64,0]. _t18 => box 1 _t19 [ SNF ] [ Backward Subsumption, 523 ] % 0.35/0.63 (1,1) [71,0]. true => _t18 | ~_t0 [ SNF ] [ Backward Subsumption, 476 ] % 0.35/0.63 (1,1) [476,0]. true => _t18 [ Unit Resolution, 3, 71, _t0 ] [ Modal Level Pure Literal Elimination, _t18 ] % 0.35/0.63 (1,1) [479,0]. true => _t1 [ Unit Resolution, 3, 32, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 0.35/0.63 (1,1) [480,0]. true => ~p2 [ Unit Resolution, 3, 6, _t0 ] [ Modal Level Pure Literal Elimination, ~p2 ] % 0.35/0.63 (1,1) [496,0]. true => _t2 [ Unit Resolution, 479, 22, _t1 ] [ Modal Level Pure Literal Elimination, _t2 ] % 0.35/0.63 (1,1) [510,0]. true => ~_t3 [ Unit Resolution, 480, 24, p2 ] [ Modal Level Pure Literal Elimination, ~_t3 ] % 0.35/0.63 (1,1) [523,0]. true => box 1 _t19 [ LHS Unit Resolution, 476, 64, _t18 ] [ SNF++, 692, _t19 ] % 0.35/0.63 (1,1) [533,0]. true => _t4 | ~_t2 [ Unit Resolution, 510, 31, _t3 ] [ Backward Subsumption, 534 ] % 0.35/0.63 (1,1) [534,0]. true => _t4 [ Unit Resolution, 496, 533, _t2 ] [ Modal Level Pure Literal Elimination, _t4 ] % 0.35/0.63 (18,1) [543,0]. true => ~box 1~ _t5 [ LHS Unit Resolution, 534, 30, _t4 ] [ SNF++, 708, _t5 ] % 0.35/0.63 (1,1) [692,0]. true => box 1 _t122 [ SNF++, 523 ] % 0.35/0.63 (18,1) [708,0]. true => ~box 1~ _t136 [ SNF++, 543 ] % 0.35/0.63 (18,1) [3245,0]. true => false [ GEN1, 692, 708, 3191, _t122, _t136 ] % 0.35/0.63 (18,1) [25,1]. true => ~_t5 | ~p2 [ Axiom T ] % 0.35/0.63 (1,1) [26,1]. _t6 => box 1 _t7 [ Axiom T ] [ SNF++, 556, _t7 ] % 0.35/0.63 (18,1) [29,1]. true => _t6 | ~_t5 [ Axiom T ] % 0.35/0.63 (16,1) [62,1]. _t20 => ~box 1~ _t21 [ SNF ] [ SNF++, 612, _t21 ] % 0.35/0.63 (1,1) [63,1]. true => _t20 | ~_t19 | p2 [ SNF ] % 0.35/0.63 (1,1) [556,1]. _t6 => box 1 _t113 [ SNF++, 26 ] % 0.35/0.63 (16,1) [612,1]. _t20 => ~box 1~ _t141 [ SNF++, 62 ] % 0.35/0.63 (1,1) [693,1]. true => ~_t122 | _t19 [ SNF++, 523 ] % 0.35/0.63 (18,1) [709,1]. true => ~_t136 | _t5 [ SNF++, 543 ] % 0.35/0.63 (18,1) [1042,1]. true => _t20 | ~_t19 | ~_t5 [ LRES, 25, 63, ~p2 ] % 0.35/0.63 (18,1) [1065,1]. true => ~_t136 | _t6 [ LRES, 29, 709, ~_t5 ] % 0.35/0.63 (18,1) [2036,1]. true => ~_t136 | _t20 | ~_t19 [ LRES, 1042, 709, ~_t5 ] % 0.35/0.63 (18,1) [2041,1]. true => ~_t136 | ~_t122 | _t20 [ LRES, 2036, 693, ~_t19 ] [ Backward Subsumption, 3191 ] % 0.35/0.63 (16,1) [3183,1]. true => ~_t20 | ~_t6 [ GEN1, 556, 612, 3182, _t113, _t141 ] % 0.35/0.63 (18,1) [3184,1]. true => ~_t136 | ~_t20 [ LRES, 3183, 1065, ~_t6 ] % 0.35/0.63 (18,1) [3191,1]. true => ~_t136 | ~_t122 [ LRES, 3184, 2041, ~_t20 ] % 0.35/0.63 (1,1) [15,2]. _t3 => box 1 p2 [ Axiom T ] [ SNF++, 644, p2 ] % 0.35/0.63 (1,1) [17,2]. true => ~_t7 | _t3 | ~p2 [ Axiom T ] % 0.35/0.63 (16,1) [59,2]. true => ~_t21 | p2 [ SNF ] % 0.35/0.63 (15,1) [60,2]. _t22 => ~box 1~ ~p2 [ SNF ] [ SNF++, 674, ~p2 ] % 0.35/0.63 (16,1) [61,2]. true => _t22 | ~_t21 [ SNF ] % 0.35/0.63 (1,1) [557,2]. true => ~_t113 | _t7 [ SNF++, 26 ] % 0.35/0.63 (16,1) [613,2]. true => ~_t141 | _t21 [ SNF++, 62 ] % 0.35/0.63 (1,1) [644,2]. _t3 => box 1 _t112 [ SNF++, 15 ] % 0.35/0.63 (15,1) [674,2]. _t22 => ~box 1~ _t142 [ SNF++, 60 ] % 0.35/0.63 (16,1) [1094,2]. true => ~_t141 | _t22 [ LRES, 61, 613, ~_t21 ] % 0.35/0.63 (15,1) [1188,2]. true => ~_t22 | ~_t3 [ GEN1, 644, 674, 774, _t112, _t142 ] % 0.35/0.63 (16,1) [1628,2]. true => ~_t21 | ~_t7 | _t3 [ LRES, 17, 59, ~p2 ] % 0.35/0.63 (16,1) [1980,2]. true => ~_t22 | ~_t21 | ~_t7 [ LRES, 1628, 1188, _t3 ] % 0.35/0.63 (16,1) [2690,2]. true => ~_t113 | ~_t22 | ~_t21 [ LRES, 1980, 557, ~_t7 ] % 0.35/0.63 (16,1) [2699,2]. true => ~_t141 | ~_t113 | ~_t22 [ LRES, 2690, 613, ~_t21 ] [ Backward Subsumption, 3182 ] % 0.35/0.63 (16,1) [3182,2]. true => ~_t141 | ~_t113 [ LRES, 2699, 1094, ~_t22 ] % 0.35/0.63 (1,1) [645,3]. true => ~_t112 | p2 [ SNF++, 15 ] % 0.35/0.63 (15,1) [675,3]. true => ~_t142 | ~p2 [ SNF++, 60 ] % 0.35/0.63 (15,1) [774,3]. true => ~_t142 | ~_t112 [ LRES, 675, 645, ~p2 ] % 0.35/0.63 % SZS output end Refutation % 0.35/0.64 % KSP exiting %------------------------------------------------------------------------------