%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP080_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:57 PM UTC 2026 % Result : CounterSatisfiable 56.66s 56.87s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP080_1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.13 % Command : run_ksp %s % 0.16/0.34 % Computer : n010.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Mon May 4 17:19:21 EDT 2026 % 0.16/0.34 % CPUTime : % 0.47/0.65 ----KSP format--- % 0.47/0.65 set(box,SER). % 0.47/0.65 usable(formulas). % 0.47/0.65 true. % 0.47/0.65 end_of_list. % 0.47/0.65 sos(formulas). % 0.47/0.65 ~ (~ ( p100 & ~ ( p101 ) & ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) & [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) & [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) & [] ( [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( [] ( [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ). % 0.47/0.65 end_of_list. % 0.47/0.65 ----------------- % 0.47/0.65 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.4JoRgzCHOu/theBenchmark.ksp % 56.66/56.87 % 56.66/56.87 % SZS status CounterSatisfiable % 56.66/56.89 % KSP exiting %------------------------------------------------------------------------------