%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP099_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n016.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 14.87s 15.05s % Output : Refutation 14.87s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP099_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : run_ksp %s % 0.15/0.34 % Computer : n016.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Mon May 4 17:36:06 EDT 2026 % 0.15/0.34 % CPUTime : % 0.44/0.67 ----KSP format--- % 0.44/0.67 set(box,REF). % 0.44/0.67 usable(formulas). % 0.44/0.67 true. % 0.44/0.67 end_of_list. % 0.44/0.67 sos(formulas). % 0.44/0.67 ~ (~ ( 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 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( p4 ) ) ) ) ) ) ) ) ) ) ) ). % 0.44/0.67 end_of_list. % 0.44/0.67 ----------------- % 0.44/0.67 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.7MqDGX6EfQ/theBenchmark.ksp % 14.87/15.05 % 14.87/15.05 % SZS status Theorem % 14.87/15.05 % 14.87/15.05 ***************** % 14.87/15.05 FOUND PROOF 1 % 14.87/15.05 ***************** % 14.87/15.05 % SZS output start Refutation % 14.87/15.05 % 14.87/15.05 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 14.87/15.05 (1,1) [4,0]. true => ~_t0 | ~p101 [ SNF ] [ Backward Subsumption, 3305 ] % 14.87/15.05 (1,1) [5,0]. true => ~_t0 | p100 [ SNF ] [ Backward Subsumption, 3304 ] % 14.87/15.05 (1,1) [97,0]. true => _t2 | ~_t1 [ Axiom T ] [ Backward Subsumption, 3306 ] % 14.87/15.05 (1,1) [99,0]. true => _t3 | ~_t2 [ Axiom T ] [ Backward Subsumption, 3371 ] % 14.87/15.05 (1,1) [101,0]. true => _t4 | ~_t3 [ Axiom T ] [ Backward Subsumption, 3381 ] % 14.87/15.05 (1,1) [103,0]. true => _t5 | ~_t4 [ Axiom T ] [ Backward Subsumption, 3391 ] % 14.87/15.05 (1,1) [105,0]. true => _t6 | ~_t5 [ Axiom T ] [ Backward Subsumption, 3398 ] % 14.87/15.05 (1,1) [106,0]. _t6 => box 1 _t7 [ Axiom T ] [ Backward Subsumption, 3406 ] % 14.87/15.05 (1,1) [116,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 3303 ] % 14.87/15.05 (1,1) [2943,0]. _t18 => box 1 _t19 [ Axiom T ] [ Backward Subsumption, 3315 ] % 14.87/15.05 (41,1) [3200,0]. _t170 => ~box 1~ _t171 [ Axiom T ] [ Backward Subsumption, 3380 ] % 14.87/15.05 (1,1) [3201,0]. true => _t170 | ~_t169 [ Axiom T ] [ Backward Subsumption, 3375 ] % 14.87/15.05 (1,1) [3207,0]. true => _t169 | ~_t168 | p101 | ~p100 [ Axiom T ] [ Backward Subsumption, 3332 ] % 14.87/15.05 (1,1) [3226,0]. true => _t18 | ~_t0 [ SNF ] [ Backward Subsumption, 3295 ] % 14.87/15.05 (1,1) [3258,0]. true => _t168 | ~_t0 [ SNF ] [ Backward Subsumption, 3263 ] % 14.87/15.05 (1,1) [3263,0]. true => _t168 [ Unit Resolution, 3, 3258, _t0 ] [ Modal Level Pure Literal Elimination, _t168 ] % 14.87/15.05 (1,1) [3295,0]. true => _t18 [ Unit Resolution, 3, 3226, _t0 ] [ Modal Level Pure Literal Elimination, _t18 ] % 14.87/15.05 (1,1) [3303,0]. true => _t1 [ Unit Resolution, 3, 116, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 14.87/15.05 (1,1) [3304,0]. true => p100 [ Unit Resolution, 3, 5, _t0 ] [ Modal Level Pure Literal Elimination, p100 ] % 14.87/15.05 (1,1) [3305,0]. true => ~p101 [ Unit Resolution, 3, 4, _t0 ] [ Modal Level Pure Literal Elimination, ~p101 ] % 14.87/15.05 (1,1) [3306,0]. true => _t2 [ Unit Resolution, 3303, 97, _t1 ] [ Modal Level Pure Literal Elimination, _t2 ] % 14.87/15.05 (1,1) [3315,0]. true => box 1 _t19 [ LHS Unit Resolution, 3295, 2943, _t18 ] [ SNF++, 4406, _t19 ] % 14.87/15.05 (1,1) [3332,0]. true => _t169 | p101 | ~p100 [ Unit Resolution, 3263, 3207, _t168 ] [ Backward Subsumption, 3333 ] % 14.87/15.05 (1,1) [3333,0]. true => _t169 | p101 [ Unit Resolution, 3304, 3332, p100 ] [ Backward Subsumption, 3337 ] % 14.87/15.05 (1,1) [3337,0]. true => _t169 [ Unit Resolution, 3305, 3333, p101 ] [ Modal Level Pure Literal Elimination, _t169 ] % 14.87/15.05 (1,1) [3371,0]. true => _t3 [ Unit Resolution, 3306, 99, _t2 ] [ Modal Level Pure Literal Elimination, _t3 ] % 14.87/15.05 (1,1) [3375,0]. true => _t170 [ Unit Resolution, 3337, 3201, _t169 ] [ Modal Level Pure Literal Elimination, _t170 ] % 14.87/15.05 (41,1) [3380,0]. true => ~box 1~ _t171 [ LHS Unit Resolution, 3375, 3200, _t170 ] [ SNF++, 4416, _t171 ] % 14.87/15.05 (1,1) [3381,0]. true => _t4 [ Unit Resolution, 3371, 101, _t3 ] [ Modal Level Pure Literal Elimination, _t4 ] % 14.87/15.05 (1,1) [3391,0]. true => _t5 [ Unit Resolution, 3381, 103, _t4 ] [ Modal Level Pure Literal Elimination, _t5 ] % 14.87/15.05 (1,1) [3398,0]. true => _t6 [ Unit Resolution, 3391, 105, _t5 ] [ Modal Level Pure Literal Elimination, _t6 ] % 14.87/15.05 (1,1) [3406,0]. true => box 1 _t7 [ LHS Unit Resolution, 3398, 106, _t6 ] [ SNF++, 4382, _t7 ] % 14.87/15.05 (1,1) [4382,0]. true => box 1 _t231 [ SNF++, 3406 ] % 14.87/15.05 (1,1) [4406,0]. true => box 1 _t228 [ SNF++, 3315 ] % 14.87/15.05 (41,1) [4416,0]. true => ~box 1~ _t221 [ SNF++, 3380 ] % 14.87/15.05 (41,1) [121663,0]. true => false [ GEN1, 4382, 4406, 4416, 116693, _t231, _t228, _t221 ] % 14.87/15.05 (1,1) [89,1]. true => _t8 | ~_t7 [ Axiom T ] % 14.87/15.05 (1,1) [90,1]. _t8 => box 1 _t9 [ Axiom T ] [ SNF++, 4264, _t9 ] % 14.87/15.05 (1,1) [2655,1]. _t19 => box 1 _t20 [ Axiom T ] [ SNF++, 4284, _t20 ] % 14.87/15.05 (1,1) [2656,1]. true => _t20 | ~_t19 [ Axiom T ] % 14.87/15.05 (1,1) [2658,1]. true => _t21 | ~_t20 [ Axiom T ] % 14.87/15.05 (35,1) [2903,1]. _t166 => ~box 1~ _t167 [ Axiom T ] [ SNF++, 4362, _t167 ] % 14.87/15.05 (1,1) [2904,1]. true => _t166 | ~_t163 [ Axiom T ] % 14.87/15.05 (1,1) [2905,1]. true => _t163 | ~_t162 | p102 | ~p101 [ Axiom T ] % 14.87/15.05 (1,1) [2906,1]. true => _t162 | ~_t21 [ Axiom T ] % 14.87/15.05 (41,1) [3198,1]. true => ~_t171 | ~p102 [ Axiom T ] % 14.87/15.05 (41,1) [3199,1]. true => ~_t171 | p101 [ Axiom T ] % 14.87/15.05 (1,1) [4264,1]. _t8 => box 1 _t227 [ SNF++, 90 ] % 14.87/15.05 (1,1) [4284,1]. _t19 => box 1 _t226 [ SNF++, 2655 ] % 14.87/15.05 (35,1) [4362,1]. _t166 => ~box 1~ _t220 [ SNF++, 2903 ] % 14.87/15.05 (1,1) [4383,1]. true => ~_t231 | _t7 [ SNF++, 3406 ] % 14.87/15.05 (1,1) [4407,1]. true => ~_t228 | _t19 [ SNF++, 3315 ] % 14.87/15.05 (41,1) [4417,1]. true => ~_t221 | _t171 [ SNF++, 3380 ] % 14.87/15.05 (1,1) [4574,1]. true => ~_t231 | _t8 [ LRES, 89, 4383, ~_t7 ] % 14.87/15.05 (1,1) [4696,1]. true => ~_t228 | _t20 [ LRES, 2656, 4407, ~_t19 ] % 14.87/15.05 (1,1) [6842,1]. true => ~_t228 | _t21 [ LRES, 4696, 2658, _t20 ] % 14.87/15.05 (1,1) [6875,1]. true => ~_t228 | _t162 [ LRES, 6842, 2906, _t21 ] % 14.87/15.05 (41,1) [13294,1]. true => ~_t171 | _t163 | ~_t162 | p102 [ LRES, 2905, 3199, ~p101 ] [ Backward Subsumption, 15138 ] % 14.87/15.05 (41,1) [15138,1]. true => ~_t171 | _t163 | ~_t162 [ LRES, 13294, 3198, p102 ] % 14.87/15.05 (41,1) [15166,1]. true => ~_t228 | ~_t171 | _t163 [ LRES, 15138, 6875, ~_t162 ] % 14.87/15.05 (41,1) [15286,1]. true => ~_t228 | ~_t171 | _t166 [ LRES, 15166, 2904, _t163 ] % 14.87/15.05 (35,1) [106810,1]. true => ~_t166 | ~_t19 | ~_t8 [ GEN1, 4264, 4284, 4362, 104988, _t227, _t226, _t220 ] % 14.87/15.05 (35,1) [109290,1]. true => ~_t231 | ~_t166 | ~_t19 [ LRES, 106810, 4574, ~_t8 ] % 14.87/15.05 (35,1) [110876,1]. true => ~_t231 | ~_t228 | ~_t166 [ LRES, 109290, 4407, ~_t19 ] % 14.87/15.05 (41,1) [111837,1]. true => ~_t231 | ~_t228 | ~_t171 [ LRES, 110876, 15286, ~_t166 ] % 14.87/15.05 (41,1) [116693,1]. true => ~_t231 | ~_t228 | ~_t221 [ LRES, 111837, 4417, ~_t171 ] % 14.87/15.05 (1,1) [74,2]. _t9 => box 1 _t10 [ Axiom T ] [ SNF++, 4148, _t10 ] % 14.87/15.05 (1,1) [2369,2]. _t20 => box 1 _t21 [ Axiom T ] [ SNF++, 4166, _t21 ] % 14.87/15.05 (1,1) [2370,2]. true => _t21 | ~_t20 [ Axiom T ] % 14.87/15.05 (33,1) [2598,2]. _t158 => ~box 1~ _t159 [ Axiom T ] [ SNF++, 4236, _t159 ] % 14.87/15.05 (1,1) [2599,2]. true => _t158 | ~_t157 [ Axiom T ] % 14.87/15.05 (1,1) [2605,2]. true => _t157 | ~_t156 | p103 | ~p102 [ Axiom T ] % 14.87/15.05 (1,1) [2606,2]. true => _t156 | ~_t21 [ Axiom T ] % 14.87/15.05 (35,1) [2901,2]. true => ~_t167 | ~p103 [ Axiom T ] % 14.87/15.05 (35,1) [2902,2]. true => ~_t167 | p102 [ Axiom T ] % 14.87/15.05 (1,1) [4148,2]. _t9 => box 1 _t225 [ SNF++, 74 ] % 14.87/15.05 (1,1) [4166,2]. _t20 => box 1 _t182 [ SNF++, 2369 ] % 14.87/15.05 (33,1) [4236,2]. _t158 => ~box 1~ _t217 [ SNF++, 2598 ] % 14.87/15.05 (1,1) [4265,2]. true => ~_t227 | _t9 [ SNF++, 90 ] % 14.87/15.05 (1,1) [4285,2]. true => ~_t226 | _t20 [ SNF++, 2655 ] % 14.87/15.05 (35,1) [4363,2]. true => ~_t220 | _t167 [ SNF++, 2903 ] % 14.87/15.05 (1,1) [4683,2]. true => ~_t226 | _t21 [ LRES, 2370, 4285, ~_t20 ] % 14.87/15.05 (1,1) [7415,2]. true => ~_t226 | _t156 [ LRES, 4683, 2606, _t21 ] % 14.87/15.05 (35,1) [43044,2]. true => ~_t167 | _t157 | ~_t156 | p103 [ LRES, 2605, 2902, ~p102 ] [ Backward Subsumption, 102960 ] % 14.87/15.05 (33,1) [87057,2]. true => ~_t158 | ~_t20 | ~_t9 [ GEN1, 4148, 4166, 4236, 87037, _t225, _t182, _t217 ] % 14.87/15.05 (33,1) [88823,2]. true => ~_t227 | ~_t158 | ~_t20 [ LRES, 87057, 4265, ~_t9 ] % 14.87/15.05 (33,1) [91368,2]. true => ~_t227 | ~_t226 | ~_t158 [ LRES, 88823, 4285, ~_t20 ] % 14.87/15.05 (35,1) [102960,2]. true => ~_t167 | _t157 | ~_t156 [ LRES, 43044, 2901, p103 ] % 14.87/15.05 (35,1) [103006,2]. true => ~_t226 | ~_t167 | _t157 [ LRES, 102960, 7415, ~_t156 ] % 14.87/15.05 (35,1) [103022,2]. true => ~_t226 | ~_t167 | _t158 [ LRES, 103006, 2599, _t157 ] % 14.87/15.05 (35,1) [104005,2]. true => ~_t227 | ~_t226 | ~_t167 [ LRES, 103022, 91368, _t158 ] % 14.87/15.05 (35,1) [104988,2]. true => ~_t227 | ~_t226 | ~_t220 [ LRES, 104005, 4363, ~_t167 ] % 14.87/15.05 (1,1) [60,3]. _t10 => box 1 p4 [ Axiom T ] [ SNF++, 4036, p4 ] % 14.87/15.05 (29,1) [2300,3]. _t152 => ~box 1~ _t153 [ Axiom T ] [ SNF++, 4116, _t153 ] % 14.87/15.05 (1,1) [2301,3]. true => _t152 | ~_t151 [ Axiom T ] % 14.87/15.05 (1,1) [2307,3]. true => _t151 | ~_t150 | p104 | ~p103 [ Axiom T ] % 14.87/15.05 (1,1) [2308,3]. true => _t150 | ~_t21 [ Axiom T ] % 14.87/15.05 (33,1) [2596,3]. true => ~_t159 | ~p104 [ Axiom T ] % 14.87/15.05 (33,1) [2597,3]. true => ~_t159 | p103 [ Axiom T ] % 14.87/15.05 (1,1) [4036,3]. _t10 => box 1 _t181 [ SNF++, 60 ] % 14.87/15.05 (29,1) [4116,3]. _t152 => ~box 1~ _t215 [ SNF++, 2300 ] % 14.87/15.05 (1,1) [4149,3]. true => ~_t225 | _t10 [ SNF++, 74 ] % 14.87/15.05 (1,1) [4167,3]. true => ~_t182 | _t21 [ SNF++, 2369 ] % 14.87/15.05 (33,1) [4237,3]. true => ~_t217 | _t159 [ SNF++, 2598 ] % 14.87/15.05 (1,1) [4718,3]. true => ~_t182 | _t150 [ LRES, 2308, 4167, ~_t21 ] % 14.87/15.05 (29,1) [9290,3]. true => ~_t152 | ~_t10 [ GEN1, 4036, 4116, 8669, _t181, _t215 ] % 14.87/15.11 (29,1) [10089,3]. true => ~_t225 | ~_t152 [ LRES, 9290, 4149, ~_t10 ] % 14.87/15.11 (33,1) [38810,3]. true => ~_t159 | _t151 | ~_t150 | p104 [ LRES, 2307, 2597, ~p103 ] [ Backward Subsumption, 84693 ] % 14.87/15.11 (33,1) [84693,3]. true => ~_t159 | _t151 | ~_t150 [ LRES, 38810, 2596, p104 ] % 14.87/15.11 (33,1) [84726,3]. true => ~_t182 | ~_t159 | _t151 [ LRES, 84693, 4718, ~_t150 ] % 14.87/15.11 (33,1) [84880,3]. true => ~_t182 | ~_t159 | _t152 [ LRES, 84726, 2301, _t151 ] % 14.87/15.11 (33,1) [84909,3]. true => ~_t225 | ~_t182 | ~_t159 [ LRES, 84880, 10089, _t152 ] % 14.87/15.11 (33,1) [87037,3]. true => ~_t225 | ~_t217 | ~_t182 [ LRES, 84909, 4237, ~_t159 ] % 14.87/15.11 (29,1) [2297,4]. true => ~_t153 | ~p4 [ Axiom T ] % 14.87/15.11 (1,1) [4037,4]. true => ~_t181 | p4 [ SNF++, 60 ] % 14.87/15.11 (29,1) [4117,4]. true => ~_t215 | _t153 [ SNF++, 2300 ] % 14.87/15.11 (29,1) [5550,4]. true => ~_t181 | ~_t153 [ LRES, 2297, 4037, ~p4 ] % 14.87/15.11 (29,1) [8669,4]. true => ~_t215 | ~_t181 [ LRES, 5550, 4117, ~_t153 ] % 14.87/15.11 % SZS output end Refutation % 14.87/15.12 % KSP exiting %------------------------------------------------------------------------------