%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP088_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n010.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:58 PM UTC 2026 % Result : CounterSatisfiable 0.47s 0.64s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP088_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.16/0.33 % Computer : n010.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Mon May 4 17:24:36 EDT 2026 % 0.16/0.34 % CPUTime : % 0.36/0.60 ----KSP format--- % 0.36/0.60 set(box,SER). % 0.36/0.60 usable(formulas). % 0.36/0.60 true. % 0.36/0.60 end_of_list. % 0.36/0.60 sos(formulas). % 0.36/0.60 ~ (~ ( [] ( ( ( <> ( 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.36/0.60 end_of_list. % 0.36/0.60 ----------------- % 0.36/0.60 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.1GBVC5TkFH/theBenchmark.ksp % 0.47/0.64 % 0.47/0.64 % SZS status CounterSatisfiable % 0.47/0.64 % KSP exiting %------------------------------------------------------------------------------