%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP052_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n003.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 34.20s 34.45s % Output : Refutation 34.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.16 % Problem : SYP052_1 : TPTP v9.3.0. Released v9.3.0. % 0.08/0.17 % Command : run_ksp %s % 0.18/0.39 % Computer : n003.cluster.edu % 0.18/0.39 % Model : x86_64 x86_64 % 0.18/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.39 % Memory : 8042.1875MB % 0.18/0.39 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.39 % CPULimit : 300 % 0.18/0.39 % WCLimit : 300 % 0.18/0.39 % DateTime : Mon May 4 16:36:41 EDT 2026 % 0.18/0.40 % CPUTime : % 0.33/0.73 ----KSP format--- % 0.33/0.73 set(box,FIVE). % 0.33/0.73 usable(formulas). % 0.33/0.73 true. % 0.33/0.73 end_of_list. % 0.33/0.73 sos(formulas). % 0.33/0.73 ~ (~ ( [] ( ( ( <> ( p1 ) & [] ( <> ( p1 ) ) ) -> p2 ) ) | [] ( ( ( p2 & [] ( p2 ) ) -> <> ( p1 ) ) ) ) | ~ ( [] ( ( ( ( p1 -> [] ( p2 ) ) & [] ( ( p1 -> [] ( p2 ) ) ) ) -> p2 ) ) | [] ( ( ( p2 & [] ( p2 ) ) -> ( p1 -> [] ( p2 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p2 ) & [] ( <> ( p2 ) ) ) -> p3 ) ) | [] ( ( ( p3 & [] ( p3 ) ) -> <> ( p2 ) ) ) ) | ~ ( [] ( ( ( ( p2 -> [] ( p3 ) ) & [] ( ( p2 -> [] ( p3 ) ) ) ) -> p3 ) ) | [] ( ( ( p3 & [] ( p3 ) ) -> ( p2 -> [] ( p3 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p3 ) & [] ( <> ( p3 ) ) ) -> p4 ) ) | [] ( ( ( p4 & [] ( p4 ) ) -> <> ( p3 ) ) ) ) | ~ ( [] ( ( ( ( p3 -> [] ( p4 ) ) & [] ( ( p3 -> [] ( p4 ) ) ) ) -> p4 ) ) | [] ( ( ( p4 & [] ( p4 ) ) -> ( p3 -> [] ( p4 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p4 ) & [] ( <> ( p4 ) ) ) -> p5 ) ) | [] ( ( ( p5 & [] ( p5 ) ) -> <> ( p4 ) ) ) ) | ~ ( [] ( ( ( ( p4 -> [] ( p5 ) ) & [] ( ( p4 -> [] ( p5 ) ) ) ) -> p5 ) ) | [] ( ( ( p5 & [] ( p5 ) ) -> ( p4 -> [] ( p5 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p5 ) & [] ( <> ( p5 ) ) ) -> p6 ) ) | [] ( ( ( p6 & [] ( p6 ) ) -> <> ( p5 ) ) ) ) | ~ ( [] ( ( ( ( p5 -> [] ( p6 ) ) & [] ( ( p5 -> [] ( p6 ) ) ) ) -> p6 ) ) | [] ( ( ( p6 & [] ( p6 ) ) -> ( p5 -> [] ( p6 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p6 ) & [] ( <> ( p6 ) ) ) -> p7 ) ) | [] ( ( ( p7 & [] ( p7 ) ) -> <> ( p6 ) ) ) ) | ~ ( [] ( ( ( ( p6 -> [] ( p7 ) ) & [] ( ( p6 -> [] ( p7 ) ) ) ) -> p7 ) ) | [] ( ( ( p7 & [] ( p7 ) ) -> ( p6 -> [] ( p7 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p7 ) & [] ( <> ( p7 ) ) ) -> p8 ) ) | [] ( ( ( p8 & [] ( p8 ) ) -> <> ( p7 ) ) ) ) | ~ ( [] ( ( ( ( p7 -> [] ( p8 ) ) & [] ( ( p7 -> [] ( p8 ) ) ) ) -> p8 ) ) | [] ( ( ( p8 & [] ( p8 ) ) -> ( p7 -> [] ( p8 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p8 ) & [] ( <> ( p8 ) ) ) -> p9 ) ) | [] ( ( ( p9 & [] ( p9 ) ) -> <> ( p8 ) ) ) ) | ~ ( [] ( ( ( ( p8 -> [] ( p9 ) ) & [] ( ( p8 -> [] ( p9 ) ) ) ) -> p9 ) ) | [] ( ( ( p9 & [] ( p9 ) ) -> ( p8 -> [] ( p9 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p9 ) & [] ( <> ( p9 ) ) ) -> p10 ) ) | [] ( ( ( p10 & [] ( p10 ) ) -> <> ( p9 ) ) ) ) | ~ ( [] ( ( ( ( p9 -> [] ( p10 ) ) & [] ( ( p9 -> [] ( p10 ) ) ) ) -> p10 ) ) | [] ( ( ( p10 & [] ( p10 ) ) -> ( p9 -> [] ( p10 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p10 ) & [] ( <> ( p10 ) ) ) -> p11 ) ) | [] ( ( ( p11 & [] ( p11 ) ) -> <> ( p10 ) ) ) ) | ~ ( [] ( ( ( ( p10 -> [] ( p11 ) ) & [] ( ( p10 -> [] ( p11 ) ) ) ) -> p11 ) ) | [] ( ( ( p11 & [] ( p11 ) ) -> ( p10 -> [] ( p11 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p11 ) & [] ( <> ( p11 ) ) ) -> p12 ) ) | [] ( ( ( p12 & [] ( p12 ) ) -> <> ( p11 ) ) ) ) | ~ ( [] ( ( ( ( p11 -> [] ( p12 ) ) & [] ( ( p11 -> [] ( p12 ) ) ) ) -> p12 ) ) | [] ( ( ( p12 & [] ( p12 ) ) -> ( p11 -> [] ( p12 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p12 ) & [] ( <> ( p12 ) ) ) -> p13 ) ) | [] ( ( ( p13 & [] ( p13 ) ) -> <> ( p12 ) ) ) ) | ~ ( [] ( ( ( ( p12 -> [] ( p13 ) ) & [] ( ( p12 -> [] ( p13 ) ) ) ) -> p13 ) ) | [] ( ( ( p13 & [] ( p13 ) ) -> ( p12 -> [] ( p13 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p13 ) & [] ( <> ( p13 ) ) ) -> p14 ) ) | [] ( ( ( p14 & [] ( p14 ) ) -> <> ( p13 ) ) ) ) | ~ ( [] ( ( ( ( p13 -> [] ( p14 ) ) & [] ( ( p13 -> [] ( p14 ) ) ) ) -> p14 ) ) | [] ( ( ( p14 & [] ( p14 ) ) -> ( p13 -> [] ( p14 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p14 ) & [] ( <> ( p14 ) ) ) -> p15 ) ) | [] ( ( ( p15 & [] ( p15 ) ) -> <> ( p14 ) ) ) ) | ~ ( [] ( ( ( ( p14 -> [] ( p15 ) ) & [] ( ( p14 -> [] ( p15 ) ) ) ) -> p15 ) ) | [] ( ( ( p15 & [] ( p15 ) ) -> ( p14 -> [] ( p15 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p15 ) & [] ( <> ( p15 ) ) ) -> p16 ) ) | [] ( ( ( p16 & [] ( p16 ) ) -> <> ( p15 ) ) ) ) | ~ ( [] ( ( ( ( p15 -> [] ( p16 ) ) & [] ( ( p15 -> [] ( p16 ) ) ) ) -> p16 ) ) | [] ( ( ( p16 & [] ( p16 ) ) -> ( p15 -> [] ( p16 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p16 ) & [] ( <> ( p16 ) ) ) -> p17 ) ) | [] ( ( ( p17 & [] ( p17 ) ) -> <> ( p16 ) ) ) ) | ~ ( [] ( ( ( ( p16 -> [] ( p17 ) ) & [] ( ( p16 -> [] ( p17 ) ) ) ) -> p17 ) ) | [] ( ( ( p17 & [] ( p17 ) ) -> ( p16 -> [] ( p17 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p17 ) & [] ( <> ( p17 ) ) ) -> p18 ) ) | [] ( ( ( p18 & [] ( p18 ) ) -> <> ( p17 ) ) ) ) | ~ ( [] ( ( ( ( p17 -> [] ( p18 ) ) & [] ( ( p17 -> [] ( p18 ) ) ) ) -> p18 ) ) | [] ( ( ( p18 & [] ( p18 ) ) -> ( p17 -> [] ( p18 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p18 ) & [] ( <> ( p18 ) ) ) -> p19 ) ) | [] ( ( ( p19 & [] ( p19 ) ) -> <> ( p18 ) ) ) ) | ~ ( [] ( ( ( ( p18 -> [] ( p19 ) ) & [] ( ( p18 -> [] ( p19 ) ) ) ) -> p19 ) ) | [] ( ( ( p19 & [] ( p19 ) ) -> ( p18 -> [] ( p19 ) ) ) ) ) | [] ( ( [] ( p10 ) -> p10 ) ) | [] ( ( [] ( p10 ) -> p10 ) ) | ~ ( [] ( ( ( <> ( p20 ) & [] ( <> ( p20 ) ) ) -> p21 ) ) | [] ( ( ( p21 & [] ( p21 ) ) -> <> ( p20 ) ) ) ) | ~ ( [] ( ( ( ( p20 -> [] ( p21 ) ) & [] ( ( p20 -> [] ( p21 ) ) ) ) -> p21 ) ) | [] ( ( ( p21 & [] ( p21 ) ) -> ( p20 -> [] ( p21 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p21 ) & [] ( <> ( p21 ) ) ) -> p22 ) ) | [] ( ( ( p22 & [] ( p22 ) ) -> <> ( p21 ) ) ) ) | ~ ( [] ( ( ( ( p21 -> [] ( p22 ) ) & [] ( ( p21 -> [] ( p22 ) ) ) ) -> p22 ) ) | [] ( ( ( p22 & [] ( p22 ) ) -> ( p21 -> [] ( p22 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p22 ) & [] ( <> ( p22 ) ) ) -> p23 ) ) | [] ( ( ( p23 & [] ( p23 ) ) -> <> ( p22 ) ) ) ) | ~ ( [] ( ( ( ( p22 -> [] ( p23 ) ) & [] ( ( p22 -> [] ( p23 ) ) ) ) -> p23 ) ) | [] ( ( ( p23 & [] ( p23 ) ) -> ( p22 -> [] ( p23 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p23 ) & [] ( <> ( p23 ) ) ) -> p24 ) ) | [] ( ( ( p24 & [] ( p24 ) ) -> <> ( p23 ) ) ) ) | ~ ( [] ( ( ( ( p23 -> [] ( p24 ) ) & [] ( ( p23 -> [] ( p24 ) ) ) ) -> p24 ) ) | [] ( ( ( p24 & [] ( p24 ) ) -> ( p23 -> [] ( p24 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p24 ) & [] ( <> ( p24 ) ) ) -> p25 ) ) | [] ( ( ( p25 & [] ( p25 ) ) -> <> ( p24 ) ) ) ) | ~ ( [] ( ( ( ( p24 -> [] ( p25 ) ) & [] ( ( p24 -> [] ( p25 ) ) ) ) -> p25 ) ) | [] ( ( ( p25 & [] ( p25 ) ) -> ( p24 -> [] ( p25 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p25 ) & [] ( <> ( p25 ) ) ) -> p26 ) ) | [] ( ( ( p26 & [] ( p26 ) ) -> <> ( p25 ) ) ) ) | ~ ( [] ( ( ( ( p25 -> [] ( p26 ) ) & [] ( ( p25 -> [] ( p26 ) ) ) ) -> p26 ) ) | [] ( ( ( p26 & [] ( p26 ) ) -> ( p25 -> [] ( p26 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p26 ) & [] ( <> ( p26 ) ) ) -> p27 ) ) | [] ( ( ( p27 & [] ( p27 ) ) -> <> ( p26 ) ) ) ) | ~ ( [] ( ( ( ( p26 -> [] ( p27 ) ) & [] ( ( p26 -> [] ( p27 ) ) ) ) -> p27 ) ) | [] ( ( ( p27 & [] ( p27 ) ) -> ( p26 -> [] ( p27 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p27 ) & [] ( <> ( p27 ) ) ) -> p28 ) ) | [] ( ( ( p28 & [] ( p28 ) ) -> <> ( p27 ) ) ) ) | ~ ( [] ( ( ( ( p27 -> [] ( p28 ) ) & [] ( ( p27 -> [] ( p28 ) ) ) ) -> p28 ) ) | [] ( ( ( p28 & [] ( p28 ) ) -> ( p27 -> [] ( p28 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p28 ) & [] ( <> ( p28 ) ) ) -> p29 ) ) | [] ( ( ( p29 & [] ( p29 ) ) -> <> ( p28 ) ) ) ) | ~ ( [] ( ( ( ( p28 -> [] ( p29 ) ) & [] ( ( p28 -> [] ( p29 ) ) ) ) -> p29 ) ) | [] ( ( ( p29 & [] ( p29 ) ) -> ( p28 -> [] ( p29 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p29 ) & [] ( <> ( p29 ) ) ) -> p30 ) ) | [] ( ( ( p30 & [] ( p30 ) ) -> <> ( p29 ) ) ) ) | ~ ( [] ( ( ( ( p29 -> [] ( p30 ) ) & [] ( ( p29 -> [] ( p30 ) ) ) ) -> p30 ) ) | [] ( ( ( p30 & [] ( p30 ) ) -> ( p29 -> [] ( p30 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p30 ) & [] ( <> ( p30 ) ) ) -> p31 ) ) | [] ( ( ( p31 & [] ( p31 ) ) -> <> ( p30 ) ) ) ) | ~ ( [] ( ( ( ( p30 -> [] ( p31 ) ) & [] ( ( p30 -> [] ( p31 ) ) ) ) -> p31 ) ) | [] ( ( ( p31 & [] ( p31 ) ) -> ( p30 -> [] ( p31 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p31 ) & [] ( <> ( p31 ) ) ) -> p32 ) ) | [] ( ( ( p32 & [] ( p32 ) ) -> <> ( p31 ) ) ) ) | ~ ( [] ( ( ( ( p31 -> [] ( p32 ) ) & [] ( ( p31 -> [] ( p32 ) ) ) ) -> p32 ) ) | [] ( ( ( p32 & [] ( p32 ) ) -> ( p31 -> [] ( p32 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p32 ) & [] ( <> ( p32 ) ) ) -> p33 ) ) | [] ( ( ( p33 & [] ( p33 ) ) -> <> ( p32 ) ) ) ) | ~ ( [] ( ( ( ( p32 -> [] ( p33 ) ) & [] ( ( p32 -> [] ( p33 ) ) ) ) -> p33 ) ) | [] ( ( ( p33 & [] ( p33 ) ) -> ( p32 -> [] ( p33 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p33 ) & [] ( <> ( p33 ) ) ) -> p34 ) ) | [] ( ( ( p34 & [] ( p34 ) ) -> <> ( p33 ) ) ) ) | ~ ( [] ( ( ( ( p33 -> [] ( p34 ) ) & [] ( ( p33 -> [] ( p34 ) ) ) ) -> p34 ) ) | [] ( ( ( p34 & [] ( p34 ) ) -> ( p33 -> [] ( p34 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p34 ) & [] ( <> ( p34 ) ) ) -> p35 ) ) | [] ( ( ( p35 & [] ( p35 ) ) -> <> ( p34 ) ) ) ) | ~ ( [] ( ( ( ( p34 -> [] ( p35 ) ) & [] ( ( p34 -> [] ( p35 ) ) ) ) -> p35 ) ) | [] ( ( ( p35 & [] ( p35 ) ) -> ( p34 -> [] ( p35 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p35 ) & [] ( <> ( p35 ) ) ) -> p36 ) ) | [] ( ( ( p36 & [] ( p36 ) ) -> <> ( p35 ) ) ) ) | ~ ( [] ( ( ( ( p35 -> [] ( p36 ) ) & [] ( ( p35 -> [] ( p36 ) ) ) ) -> p36 ) ) | [] ( ( ( p36 & [] ( p36 ) ) -> ( p35 -> [] ( p36 ) ) ) ) ) | ~ ( [] ( ( ( <> ( p36 ) & [] ( <> ( p36 ) ) ) -> p37 ) ) | [] ( ( ( p37 & [] ( p37 ) ) -> <> ( p36 ) ) ) ) | ~ ( [] ( ( ( ( p36 -> [] ( p37 ) ) & [] ( ( p36 -> [] ( p37 ) ) ) ) -> p37 ) ) | [] ( ( ( p37 & [] ( p37 ) ) -> ( p36 -> [] ( p37 ) ) ) ) ) ). % 0.33/0.73 end_of_list. % 0.33/0.73 ----------------- % 0.33/0.73 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.8ADuj1uVyx/theBenchmark.ksp % 34.20/34.45 % 34.20/34.45 % SZS status Theorem % 34.20/34.45 % 34.20/34.45 ***************** % 34.20/34.45 FOUND PROOF 1 % 34.20/34.45 ***************** % 34.20/34.45 % SZS output start Refutation % 34.20/34.45 % 34.20/34.45 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 34.20/34.45 (1,1) [6,0]. _t3 => box 1 p10 [ Axiom 5 ] [ SNF++, 99928, p10 ] % 34.20/34.45 (1,1) [8,0]. ~_t320 => box 1 ~_t3 [ Axiom 5 ] [ SNF++, 99930, ~_t3 ] % 34.20/34.45 (1,1) [10,0]. true => ~_t320 | _t3 [ Axiom 5 ] [ Modal Level Pure Literal Elimination, ~_t320 ] % 34.20/34.45 (3,1) [546,0]. _t1 => ~box 1~ _t2 [ SNF ] [ Backward Subsumption, 98834 ] % 34.20/34.45 (1,1) [547,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 98833 ] % 34.20/34.45 (1,1) [98833,0]. true => _t1 [ Unit Resolution, 3, 547, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 34.20/34.45 (3,1) [98834,0]. true => ~box 1~ _t2 [ LHS Unit Resolution, 98833, 546, _t1 ] [ SNF++, 100562, _t2 ] % 34.20/34.45 (1,1) [99928,0]. _t3 => box 1 _t426 [ SNF++, 6 ] [ Backward Subsumption, 242856 ] % 34.20/34.45 (1,1) [99930,0]. ~_t320 => box 1 _t427 [ SNF++, 8 ] [ Backward Subsumption, 242853 ] % 34.20/34.45 (3,1) [100562,0]. true => ~box 1~ _t886 [ SNF++, 98834 ] % 34.20/34.45 (3,1) [242638,0]. true => ~_t3 [ GEN1, 99928, 100562, 212890, _t426, _t886 ] [ Modal Level Pure Literal Elimination, ~_t3 ] % 34.20/34.45 (3,1) [242852,0]. true => ~_t320 [ LRES, 242638, 10, ~_t3 ] [ Modal Level Pure Literal Elimination, ~_t320 ] % 34.20/34.45 (1,1) [242853,0]. true => box 1 _t427 [ LHS Unit Resolution, 242852, 99930, ~_t320 ] % 34.20/34.45 (3,1) [2406384,0]. true => false [ GEN1, 242853, 100562, 242857, _t427, _t886 ] % 34.20/34.45 (3,1) [4,1]. true => ~_t2 | ~p10 [ SNF ] % 34.20/34.45 (3,1) [545,1]. true => _t3 | ~_t2 [ SNF ] % 34.20/34.45 (1,1) [99929,1]. true => ~_t426 | p10 [ SNF++, 6 ] [ Modal Level Pure Literal Elimination, ~_t426 ] % 34.20/34.45 (1,1) [99931,1]. true => ~_t427 | ~_t3 [ SNF++, 8 ] % 34.20/34.45 (3,1) [100563,1]. true => ~_t886 | _t2 [ SNF++, 98834 ] % 34.20/34.45 (3,1) [212676,1]. true => ~_t426 | ~_t2 [ LRES, 4, 99929, ~p10 ] [ Modal Level Pure Literal Elimination, ~_t426 ] % 34.20/34.45 (3,1) [212890,1]. true => ~_t886 | ~_t426 [ LRES, 212676, 100563, ~_t2 ] [ Modal Level Pure Literal Elimination, ~_t426 ] % 34.20/34.45 (3,1) [213104,1]. true => ~_t886 | _t3 [ LRES, 545, 100563, ~_t2 ] % 34.20/34.45 (3,1) [242857,1]. true => ~_t886 | ~_t427 [ LRES, 213104, 99931, _t3 ] % 34.20/34.45 % SZS output end Refutation % 0.55/34.52 % KSP exiting %------------------------------------------------------------------------------