%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP009_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n001.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:52 PM UTC 2026 % Result : Theorem 18.16s 18.33s % Output : Refutation 18.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP009_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.15/0.33 % Computer : n001.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Mon May 4 16:22:18 EDT 2026 % 0.15/0.34 % CPUTime : % 0.48/0.65 ----KSP format--- % 0.48/0.65 usable(formulas). % 0.48/0.65 true. % 0.48/0.65 end_of_list. % 0.48/0.65 sos(formulas). % 0.48/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 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( p4 ) ) ) ) ) ) ) ) ) ) ) ). % 0.48/0.65 end_of_list. % 0.48/0.65 ----------------- % 0.48/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.cIGV3VNhnY/theBenchmark.ksp % 18.16/18.33 % 18.16/18.33 % SZS status Theorem % 18.16/18.33 % 18.16/18.33 ***************** % 18.16/18.33 FOUND PROOF 1 % 18.16/18.33 ***************** % 18.16/18.33 % SZS output start Refutation % 18.16/18.33 % 18.16/18.33 (1,1) [1,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 18.16/18.33 (1,1) [2,0]. true => ~_t0 | ~p101 [ SNF ] [ Backward Subsumption, 2626 ] % 18.16/18.33 (1,1) [3,0]. true => ~_t0 | p100 [ SNF ] [ Backward Subsumption, 2625 ] % 18.16/18.33 (1,1) [13,0]. _t0 => box 1 _t2 [ SNF ] [ Backward Subsumption, 2624 ] % 18.16/18.33 (1,1) [251,0]. _t0 => box 1 _t12 [ SNF ] [ Backward Subsumption, 2623 ] % 18.16/18.33 (1,1) [488,0]. _t0 => box 1 _t13 [ SNF ] [ Backward Subsumption, 2622 ] % 18.16/18.33 (1,1) [724,0]. _t0 => box 1 _t14 [ SNF ] [ Backward Subsumption, 2621 ] % 18.16/18.33 (1,1) [959,0]. _t0 => box 1 _t15 [ SNF ] [ Backward Subsumption, 2620 ] % 18.16/18.33 (1,1) [1193,0]. _t0 => box 1 _t16 [ SNF ] [ Backward Subsumption, 2619 ] % 18.16/18.33 (1,1) [1426,0]. _t0 => box 1 _t17 [ SNF ] [ Backward Subsumption, 2618 ] % 18.16/18.33 (1,1) [1658,0]. _t0 => box 1 _t18 [ SNF ] [ Backward Subsumption, 2617 ] % 18.16/18.33 (1,1) [1889,0]. _t0 => box 1 _t19 [ SNF ] [ Backward Subsumption, 2616 ] % 18.16/18.33 (1,1) [2119,0]. _t0 => box 1 _t20 [ SNF ] [ Backward Subsumption, 2615 ] % 18.16/18.33 (1,1) [2348,0]. _t0 => box 1 _t21 [ SNF ] [ Backward Subsumption, 2614 ] % 18.16/18.33 (439,1) [2566,0]. _t169 => ~box 1~ _t173 [ SNF ] [ Backward Subsumption, 2666 ] % 18.16/18.33 (1,1) [2567,0]. true => _t169 | ~_t168 | p101 | ~p100 [ SNF ] [ Backward Subsumption, 2644 ] % 18.16/18.33 (1,1) [2568,0]. true => _t168 | ~_t0 [ SNF ] [ Backward Subsumption, 2584 ] % 18.16/18.33 (1,1) [2584,0]. true => _t168 [ Unit Resolution, 1, 2568, _t0 ] [ Modal Level Pure Literal Elimination, _t168 ] % 18.16/18.33 (1,1) [2614,0]. true => box 1 _t21 [ LHS Unit Resolution, 1, 2348, _t0 ] [ SNF++, 3598, _t21 ] % 18.16/18.33 (1,1) [2615,0]. true => box 1 _t20 [ LHS Unit Resolution, 1, 2119, _t0 ] [ SNF++, 3596, _t20 ] % 18.16/18.33 (1,1) [2616,0]. true => box 1 _t19 [ LHS Unit Resolution, 1, 1889, _t0 ] [ SNF++, 3594, _t19 ] % 18.16/18.33 (1,1) [2617,0]. true => box 1 _t18 [ LHS Unit Resolution, 1, 1658, _t0 ] [ SNF++, 3592, _t18 ] % 18.16/18.33 (1,1) [2618,0]. true => box 1 _t17 [ LHS Unit Resolution, 1, 1426, _t0 ] [ SNF++, 3590, _t17 ] % 18.16/18.33 (1,1) [2619,0]. true => box 1 _t16 [ LHS Unit Resolution, 1, 1193, _t0 ] [ SNF++, 3588, _t16 ] % 18.16/18.33 (1,1) [2620,0]. true => box 1 _t15 [ LHS Unit Resolution, 1, 959, _t0 ] [ SNF++, 3586, _t15 ] % 18.16/18.33 (1,1) [2621,0]. true => box 1 _t14 [ LHS Unit Resolution, 1, 724, _t0 ] [ SNF++, 3584, _t14 ] % 18.16/18.33 (1,1) [2622,0]. true => box 1 _t13 [ LHS Unit Resolution, 1, 488, _t0 ] [ SNF++, 3582, _t13 ] % 18.16/18.33 (1,1) [2623,0]. true => box 1 _t12 [ LHS Unit Resolution, 1, 251, _t0 ] [ SNF++, 3580, _t12 ] % 18.16/18.33 (1,1) [2624,0]. true => box 1 _t2 [ LHS Unit Resolution, 1, 13, _t0 ] [ SNF++, 3578, _t2 ] % 18.16/18.33 (1,1) [2625,0]. true => p100 [ Unit Resolution, 1, 3, _t0 ] [ Modal Level Pure Literal Elimination, p100 ] % 18.16/18.33 (1,1) [2626,0]. true => ~p101 [ Unit Resolution, 1, 2, _t0 ] [ Modal Level Pure Literal Elimination, ~p101 ] % 18.16/18.33 (1,1) [2644,0]. true => _t169 | ~_t168 | ~p100 [ Unit Resolution, 2626, 2567, p101 ] [ Backward Subsumption, 2645 ] % 18.16/18.33 (1,1) [2645,0]. true => _t169 | ~_t168 [ Unit Resolution, 2625, 2644, p100 ] [ Backward Subsumption, 2647 ] % 18.16/18.33 (1,1) [2647,0]. true => _t169 [ Unit Resolution, 2584, 2645, _t168 ] [ Modal Level Pure Literal Elimination, _t169 ] % 18.16/18.33 (439,1) [2666,0]. true => ~box 1~ _t173 [ LHS Unit Resolution, 2647, 2566, _t169 ] [ SNF++, 3606, _t173 ] % 18.16/18.33 (1,1) [3578,0]. true => box 1 _t241 [ SNF++, 2624 ] % 18.16/18.33 (1,1) [3580,0]. true => box 1 _t242 [ SNF++, 2623 ] % 18.16/18.33 (1,1) [3582,0]. true => box 1 _t240 [ SNF++, 2622 ] % 18.16/18.33 (1,1) [3584,0]. true => box 1 _t238 [ SNF++, 2621 ] % 18.16/18.33 (1,1) [3586,0]. true => box 1 _t236 [ SNF++, 2620 ] % 18.16/18.33 (1,1) [3588,0]. true => box 1 _t234 [ SNF++, 2619 ] % 18.16/18.33 (1,1) [3590,0]. true => box 1 _t232 [ SNF++, 2618 ] % 18.16/18.33 (1,1) [3592,0]. true => box 1 _t230 [ SNF++, 2617 ] % 18.16/18.33 (1,1) [3594,0]. true => box 1 _t228 [ SNF++, 2616 ] % 18.16/18.33 (1,1) [3596,0]. true => box 1 _t226 [ SNF++, 2615 ] % 18.16/18.33 (1,1) [3598,0]. true => box 1 _t182 [ SNF++, 2614 ] % 18.16/18.33 (439,1) [3606,0]. true => ~box 1~ _t222 [ SNF++, 2666 ] % 18.16/18.33 (439,1) [143778,0]. true => false [ GEN1, 3580, 3582, 3586, 3590, 3594, 3598, 3596, 3592, 3588, 3584, 3578, 3606, 143776, _t242, _t240, _t236, _t232, _t228, _t182, _t226, _t230, _t234, _t238, _t241, _t222 ] % 18.16/18.33 (1,1) [12,1]. _t2 => box 1 _t3 [ SNF ] [ SNF++, 3474, _t3 ] % 18.16/18.33 (1,1) [250,1]. _t12 => box 1 _t13 [ SNF ] [ SNF++, 3476, _t13 ] % 18.16/18.33 (1,1) [487,1]. _t13 => box 1 _t14 [ SNF ] [ SNF++, 3478, _t14 ] % 18.16/18.33 (1,1) [723,1]. _t14 => box 1 _t15 [ SNF ] [ SNF++, 3480, _t15 ] % 18.16/18.33 (1,1) [958,1]. _t15 => box 1 _t16 [ SNF ] [ SNF++, 3482, _t16 ] % 18.16/18.33 (1,1) [1192,1]. _t16 => box 1 _t17 [ SNF ] [ SNF++, 3484, _t17 ] % 18.16/18.33 (1,1) [1425,1]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 3486, _t18 ] % 18.16/18.33 (1,1) [1657,1]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 3488, _t19 ] % 18.16/18.33 (1,1) [1888,1]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 3490, _t20 ] % 18.16/18.33 (1,1) [2118,1]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 3492, _t21 ] % 18.16/18.33 (395,1) [2327,1]. _t163 => ~box 1~ _t167 [ SNF ] [ SNF++, 3568, _t167 ] % 18.16/18.33 (1,1) [2328,1]. true => _t163 | ~_t162 | p102 | ~p101 [ SNF ] % 18.16/18.33 (1,1) [2329,1]. true => _t162 | ~_t21 [ SNF ] % 18.16/18.33 (439,1) [2564,1]. true => ~_t173 | ~p102 [ SNF ] % 18.16/18.33 (439,1) [2565,1]. true => ~_t173 | p101 [ SNF ] % 18.16/18.33 (1,1) [3474,1]. _t2 => box 1 _t239 [ SNF++, 12 ] % 18.16/18.33 (1,1) [3476,1]. _t12 => box 1 _t240 [ SNF++, 250 ] % 18.16/18.33 (1,1) [3478,1]. _t13 => box 1 _t238 [ SNF++, 487 ] % 18.16/18.33 (1,1) [3480,1]. _t14 => box 1 _t236 [ SNF++, 723 ] % 18.16/18.33 (1,1) [3482,1]. _t15 => box 1 _t234 [ SNF++, 958 ] % 18.16/18.33 (1,1) [3484,1]. _t16 => box 1 _t232 [ SNF++, 1192 ] % 18.16/18.33 (1,1) [3486,1]. _t17 => box 1 _t230 [ SNF++, 1425 ] % 18.16/18.33 (1,1) [3488,1]. _t18 => box 1 _t228 [ SNF++, 1657 ] % 18.16/18.33 (1,1) [3490,1]. _t19 => box 1 _t226 [ SNF++, 1888 ] % 18.16/18.33 (1,1) [3492,1]. _t20 => box 1 _t182 [ SNF++, 2118 ] % 18.16/18.33 (395,1) [3568,1]. _t163 => ~box 1~ _t220 [ SNF++, 2327 ] % 18.16/18.33 (1,1) [3579,1]. true => ~_t241 | _t2 [ SNF++, 2624 ] % 18.16/18.33 (1,1) [3581,1]. true => ~_t242 | _t12 [ SNF++, 2623 ] % 18.16/18.33 (1,1) [3583,1]. true => ~_t240 | _t13 [ SNF++, 2622 ] % 18.16/18.33 (1,1) [3585,1]. true => ~_t238 | _t14 [ SNF++, 2621 ] % 18.16/18.33 (1,1) [3587,1]. true => ~_t236 | _t15 [ SNF++, 2620 ] % 18.16/18.33 (1,1) [3589,1]. true => ~_t234 | _t16 [ SNF++, 2619 ] % 18.16/18.33 (1,1) [3591,1]. true => ~_t232 | _t17 [ SNF++, 2618 ] % 18.16/18.33 (1,1) [3593,1]. true => ~_t230 | _t18 [ SNF++, 2617 ] % 18.16/18.33 (1,1) [3595,1]. true => ~_t228 | _t19 [ SNF++, 2616 ] % 18.16/18.33 (1,1) [3597,1]. true => ~_t226 | _t20 [ SNF++, 2615 ] % 18.16/18.33 (1,1) [3599,1]. true => ~_t182 | _t21 [ SNF++, 2614 ] % 18.16/18.33 (439,1) [3607,1]. true => ~_t222 | _t173 [ SNF++, 2666 ] % 18.16/18.33 (1,1) [3724,1]. true => ~_t182 | _t162 [ LRES, 2329, 3599, ~_t21 ] % 18.16/18.33 (439,1) [5201,1]. true => ~_t173 | _t163 | ~_t162 | p102 [ LRES, 2328, 2565, ~p101 ] [ Backward Subsumption, 5429 ] % 18.16/18.33 (439,1) [5429,1]. true => ~_t173 | _t163 | ~_t162 [ LRES, 5201, 2564, p102 ] % 18.16/18.33 (439,1) [5444,1]. true => ~_t182 | ~_t173 | _t163 [ LRES, 5429, 3724, ~_t162 ] % 18.16/18.33 (395,1) [143655,1]. true => ~_t163 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 | ~_t13 | ~_t12 | ~_t2 [ GEN1, 3476, 3478, 3482, 3486, 3490, 3492, 3488, 3484, 3480, 3474, 3568, 141179, _t240, _t238, _t234, _t230, _t226, _t182, _t228, _t232, _t236, _t239, _t220 ] % 18.16/18.33 (395,1) [143657,1]. true => ~_t241 | ~_t163 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 | ~_t13 | ~_t12 [ LRES, 143655, 3579, ~_t2 ] % 18.16/18.33 (395,1) [143659,1]. true => ~_t242 | ~_t241 | ~_t163 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 | ~_t13 [ LRES, 143657, 3581, ~_t12 ] % 18.16/18.33 (395,1) [143663,1]. true => ~_t242 | ~_t241 | ~_t240 | ~_t163 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 [ LRES, 143659, 3583, ~_t13 ] % 18.16/18.33 (395,1) [143666,1]. true => ~_t242 | ~_t241 | ~_t240 | ~_t238 | ~_t163 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 [ LRES, 143663, 3585, ~_t14 ] % 18.16/18.33 (395,1) [143668,1]. true => ~_t242 | ~_t241 | ~_t240 | ~_t238 | ~_t236 | ~_t163 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 [ LRES, 143666, 3587, ~_t15 ] % 18.16/18.33 (395,1) [143671,1]. true => ~_t242 | ~_t241 | ~_t240 | ~_t238 | ~_t236 | ~_t234 | ~_t163 | ~_t20 | ~_t19 | ~_t18 | ~_t17 [ LRES, 143668, 3589, ~_t16 ] % 18.16/18.33 (395,1) [143676,1]. true => ~_t242 | ~_t241 | ~_t240 | ~_t238 | ~_t236 | ~_t234 | ~_t232 | ~_t163 | ~_t20 | ~_t19 | ~_t18 [ LRES, 143671, 3591, ~_t17 ] % 18.16/18.33 (395,1) [143682,1]. true => ~_t242 | ~_t241 | ~_t240 | ~_t238 | ~_t236 | ~_t234 | ~_t232 | ~_t230 | ~_t163 | ~_t20 | ~_t19 [ LRES, 143676, 3593, ~_t18 ] % 18.16/18.33 (395,1) [143688,1]. true => ~_t242 | ~_t241 | ~_t240 | ~_t238 | ~_t236 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t163 | ~_t20 [ LRES, 143682, 3595, ~_t19 ] % 18.16/18.33 (395,1) [143709,1]. true => ~_t242 | ~_t241 | ~_t240 | ~_t238 | ~_t236 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t163 [ LRES, 143688, 3597, ~_t20 ] % 18.16/18.33 (439,1) [143767,1]. true => ~_t242 | ~_t241 | ~_t240 | ~_t238 | ~_t236 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t182 | ~_t173 [ LRES, 143709, 5444, ~_t163 ] % 18.16/18.33 (439,1) [143776,1]. true => ~_t242 | ~_t241 | ~_t240 | ~_t238 | ~_t236 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t222 | ~_t182 [ LRES, 143767, 3607, ~_t173 ] % 18.16/18.33 (1,1) [11,2]. _t3 => box 1 _t4 [ SNF ] [ SNF++, 3372, _t4 ] % 18.16/18.33 (1,1) [249,2]. _t13 => box 1 _t14 [ SNF ] [ SNF++, 3374, _t14 ] % 18.16/18.33 (1,1) [486,2]. _t14 => box 1 _t15 [ SNF ] [ SNF++, 3376, _t15 ] % 18.16/18.33 (1,1) [722,2]. _t15 => box 1 _t16 [ SNF ] [ SNF++, 3378, _t16 ] % 18.16/18.33 (1,1) [957,2]. _t16 => box 1 _t17 [ SNF ] [ SNF++, 3380, _t17 ] % 18.16/18.33 (1,1) [1191,2]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 3382, _t18 ] % 18.16/18.33 (1,1) [1424,2]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 3384, _t19 ] % 18.16/18.33 (1,1) [1656,2]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 3386, _t20 ] % 18.16/18.33 (1,1) [1887,2]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 3388, _t21 ] % 18.16/18.33 (351,1) [2087,2]. _t157 => ~box 1~ _t161 [ SNF ] [ SNF++, 3460, _t161 ] % 18.16/18.33 (1,1) [2088,2]. true => _t157 | ~_t156 | p103 | ~p102 [ SNF ] % 18.16/18.33 (1,1) [2089,2]. true => _t156 | ~_t21 [ SNF ] % 18.16/18.33 (395,1) [2325,2]. true => ~_t167 | ~p103 [ SNF ] % 18.16/18.33 (395,1) [2326,2]. true => ~_t167 | p102 [ SNF ] % 18.16/18.33 (1,1) [3372,2]. _t3 => box 1 _t237 [ SNF++, 11 ] % 18.16/18.33 (1,1) [3374,2]. _t13 => box 1 _t238 [ SNF++, 249 ] % 18.16/18.33 (1,1) [3376,2]. _t14 => box 1 _t236 [ SNF++, 486 ] % 18.16/18.33 (1,1) [3378,2]. _t15 => box 1 _t234 [ SNF++, 722 ] % 18.16/18.33 (1,1) [3380,2]. _t16 => box 1 _t232 [ SNF++, 957 ] % 18.16/18.33 (1,1) [3382,2]. _t17 => box 1 _t230 [ SNF++, 1191 ] % 18.16/18.33 (1,1) [3384,2]. _t18 => box 1 _t228 [ SNF++, 1424 ] % 18.16/18.33 (1,1) [3386,2]. _t19 => box 1 _t226 [ SNF++, 1656 ] % 18.16/18.33 (1,1) [3388,2]. _t20 => box 1 _t182 [ SNF++, 1887 ] % 18.16/18.33 (351,1) [3460,2]. _t157 => ~box 1~ _t218 [ SNF++, 2087 ] % 18.16/18.33 (1,1) [3475,2]. true => ~_t239 | _t3 [ SNF++, 12 ] % 18.16/18.33 (1,1) [3477,2]. true => ~_t240 | _t13 [ SNF++, 250 ] % 18.16/18.33 (1,1) [3479,2]. true => ~_t238 | _t14 [ SNF++, 487 ] % 18.16/18.33 (1,1) [3481,2]. true => ~_t236 | _t15 [ SNF++, 723 ] % 18.16/18.33 (1,1) [3483,2]. true => ~_t234 | _t16 [ SNF++, 958 ] % 18.16/18.33 (1,1) [3485,2]. true => ~_t232 | _t17 [ SNF++, 1192 ] % 18.16/18.33 (1,1) [3487,2]. true => ~_t230 | _t18 [ SNF++, 1425 ] % 18.16/18.33 (1,1) [3489,2]. true => ~_t228 | _t19 [ SNF++, 1657 ] % 18.16/18.33 (1,1) [3491,2]. true => ~_t226 | _t20 [ SNF++, 1888 ] % 18.16/18.33 (1,1) [3493,2]. true => ~_t182 | _t21 [ SNF++, 2118 ] % 18.16/18.33 (395,1) [3569,2]. true => ~_t220 | _t167 [ SNF++, 2327 ] % 18.16/18.33 (1,1) [3735,2]. true => ~_t182 | _t156 [ LRES, 2089, 3493, ~_t21 ] % 18.16/18.33 (395,1) [11376,2]. true => ~_t167 | _t157 | ~_t156 | p103 [ LRES, 2088, 2326, ~p102 ] [ Backward Subsumption, 15706 ] % 18.16/18.33 (395,1) [15706,2]. true => ~_t167 | _t157 | ~_t156 [ LRES, 11376, 2325, p103 ] % 18.16/18.33 (395,1) [15724,2]. true => ~_t182 | ~_t167 | _t157 [ LRES, 15706, 3735, ~_t156 ] % 18.16/18.33 (351,1) [132153,2]. true => ~_t157 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 | ~_t13 | ~_t3 [ GEN1, 3374, 3376, 3380, 3384, 3388, 3386, 3382, 3378, 3372, 3460, 132151, _t238, _t236, _t232, _t228, _t182, _t226, _t230, _t234, _t237, _t218 ] % 18.16/18.33 (351,1) [132763,2]. true => ~_t239 | ~_t157 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 | ~_t13 [ LRES, 132153, 3475, ~_t3 ] % 18.16/18.33 (351,1) [132765,2]. true => ~_t240 | ~_t239 | ~_t157 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 [ LRES, 132763, 3477, ~_t13 ] % 18.16/18.33 (351,1) [132767,2]. true => ~_t240 | ~_t239 | ~_t238 | ~_t157 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 [ LRES, 132765, 3479, ~_t14 ] % 18.16/18.33 (351,1) [132769,2]. true => ~_t240 | ~_t239 | ~_t238 | ~_t236 | ~_t157 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 [ LRES, 132767, 3481, ~_t15 ] % 18.16/18.33 (351,1) [132771,2]. true => ~_t240 | ~_t239 | ~_t238 | ~_t236 | ~_t234 | ~_t157 | ~_t20 | ~_t19 | ~_t18 | ~_t17 [ LRES, 132769, 3483, ~_t16 ] % 18.16/18.33 (351,1) [132774,2]. true => ~_t240 | ~_t239 | ~_t238 | ~_t236 | ~_t234 | ~_t232 | ~_t157 | ~_t20 | ~_t19 | ~_t18 [ LRES, 132771, 3485, ~_t17 ] % 18.16/18.33 (351,1) [132777,2]. true => ~_t240 | ~_t239 | ~_t238 | ~_t236 | ~_t234 | ~_t232 | ~_t230 | ~_t157 | ~_t20 | ~_t19 [ LRES, 132774, 3487, ~_t18 ] % 18.16/18.33 (351,1) [132797,2]. true => ~_t240 | ~_t239 | ~_t238 | ~_t236 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t157 | ~_t20 [ LRES, 132777, 3489, ~_t19 ] % 18.16/18.33 (351,1) [132836,2]. true => ~_t240 | ~_t239 | ~_t238 | ~_t236 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t157 [ LRES, 132797, 3491, ~_t20 ] % 18.16/18.33 (395,1) [132839,2]. true => ~_t240 | ~_t239 | ~_t238 | ~_t236 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t182 | ~_t167 [ LRES, 132836, 15724, ~_t157 ] % 18.16/18.33 (395,1) [141179,2]. true => ~_t240 | ~_t239 | ~_t238 | ~_t236 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t220 | ~_t182 [ LRES, 132839, 3569, ~_t167 ] % 18.16/18.33 (1,1) [10,3]. _t4 => box 1 _t5 [ SNF ] [ SNF++, 3272, _t5 ] % 18.16/18.33 (1,1) [248,3]. _t14 => box 1 _t15 [ SNF ] [ SNF++, 3274, _t15 ] % 18.16/18.33 (1,1) [485,3]. _t15 => box 1 _t16 [ SNF ] [ SNF++, 3276, _t16 ] % 18.16/18.33 (1,1) [721,3]. _t16 => box 1 _t17 [ SNF ] [ SNF++, 3278, _t17 ] % 18.16/18.33 (1,1) [956,3]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 3280, _t18 ] % 18.16/18.33 (1,1) [1190,3]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 3282, _t19 ] % 18.16/18.33 (1,1) [1423,3]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 3284, _t20 ] % 18.16/18.33 (1,1) [1655,3]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 3286, _t21 ] % 18.16/18.33 (309,1) [1842,3]. _t151 => ~box 1~ _t153 [ SNF ] [ SNF++, 3352, _t153 ] % 18.16/18.33 (1,1) [1847,3]. true => _t151 | ~_t150 | p104 | ~p103 [ SNF ] % 18.16/18.33 (1,1) [1848,3]. true => _t150 | ~_t21 [ SNF ] % 18.16/18.33 (351,1) [2085,3]. true => ~_t161 | ~p104 [ SNF ] % 18.16/18.33 (351,1) [2086,3]. true => ~_t161 | p103 [ SNF ] % 18.16/18.33 (1,1) [3272,3]. _t4 => box 1 _t235 [ SNF++, 10 ] % 18.16/18.33 (1,1) [3274,3]. _t14 => box 1 _t236 [ SNF++, 248 ] % 18.16/18.33 (1,1) [3276,3]. _t15 => box 1 _t234 [ SNF++, 485 ] % 18.16/18.33 (1,1) [3278,3]. _t16 => box 1 _t232 [ SNF++, 721 ] % 18.16/18.33 (1,1) [3280,3]. _t17 => box 1 _t230 [ SNF++, 956 ] % 18.16/18.33 (1,1) [3282,3]. _t18 => box 1 _t228 [ SNF++, 1190 ] % 18.16/18.33 (1,1) [3284,3]. _t19 => box 1 _t226 [ SNF++, 1423 ] % 18.16/18.33 (1,1) [3286,3]. _t20 => box 1 _t182 [ SNF++, 1655 ] % 18.16/18.33 (309,1) [3352,3]. _t151 => ~box 1~ _t215 [ SNF++, 1842 ] % 18.16/18.33 (1,1) [3373,3]. true => ~_t237 | _t4 [ SNF++, 11 ] % 18.16/18.33 (1,1) [3375,3]. true => ~_t238 | _t14 [ SNF++, 249 ] % 18.16/18.33 (1,1) [3377,3]. true => ~_t236 | _t15 [ SNF++, 486 ] % 18.16/18.33 (1,1) [3379,3]. true => ~_t234 | _t16 [ SNF++, 722 ] % 18.16/18.33 (1,1) [3381,3]. true => ~_t232 | _t17 [ SNF++, 957 ] % 18.16/18.33 (1,1) [3383,3]. true => ~_t230 | _t18 [ SNF++, 1191 ] % 18.16/18.33 (1,1) [3385,3]. true => ~_t228 | _t19 [ SNF++, 1424 ] % 18.16/18.33 (1,1) [3387,3]. true => ~_t226 | _t20 [ SNF++, 1656 ] % 18.16/18.33 (1,1) [3389,3]. true => ~_t182 | _t21 [ SNF++, 1887 ] % 18.16/18.33 (351,1) [3461,3]. true => ~_t218 | _t161 [ SNF++, 2087 ] % 18.16/18.33 (1,1) [3746,3]. true => ~_t182 | _t150 [ LRES, 1848, 3389, ~_t21 ] % 18.16/18.33 (351,1) [11265,3]. true => ~_t161 | _t151 | ~_t150 | p104 [ LRES, 1847, 2086, ~p103 ] [ Backward Subsumption, 15315 ] % 18.16/18.33 (351,1) [15315,3]. true => ~_t161 | _t151 | ~_t150 [ LRES, 11265, 2085, p104 ] % 18.16/18.33 (351,1) [15349,3]. true => ~_t182 | ~_t161 | _t151 [ LRES, 15315, 3746, ~_t150 ] % 18.16/18.33 (309,1) [130353,3]. true => ~_t151 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 | ~_t4 [ GEN1, 3274, 3276, 3280, 3284, 3286, 3282, 3278, 3272, 3352, 130303, _t236, _t234, _t230, _t226, _t182, _t228, _t232, _t235, _t215 ] % 18.16/18.33 (309,1) [132085,3]. true => ~_t237 | ~_t151 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 [ LRES, 130353, 3373, ~_t4 ] % 18.16/18.33 (309,1) [132087,3]. true => ~_t238 | ~_t237 | ~_t151 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 [ LRES, 132085, 3375, ~_t14 ] % 18.16/18.33 (309,1) [132090,3]. true => ~_t238 | ~_t237 | ~_t236 | ~_t151 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 [ LRES, 132087, 3377, ~_t15 ] % 18.16/18.33 (309,1) [132110,3]. true => ~_t238 | ~_t237 | ~_t236 | ~_t234 | ~_t151 | ~_t20 | ~_t19 | ~_t18 | ~_t17 [ LRES, 132090, 3379, ~_t16 ] % 18.16/18.33 (309,1) [132119,3]. true => ~_t238 | ~_t237 | ~_t236 | ~_t234 | ~_t232 | ~_t151 | ~_t20 | ~_t19 | ~_t18 [ LRES, 132110, 3381, ~_t17 ] % 18.16/18.33 (309,1) [132121,3]. true => ~_t238 | ~_t237 | ~_t236 | ~_t234 | ~_t232 | ~_t230 | ~_t151 | ~_t20 | ~_t19 [ LRES, 132119, 3383, ~_t18 ] % 18.16/18.33 (309,1) [132136,3]. true => ~_t238 | ~_t237 | ~_t236 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t151 | ~_t20 [ LRES, 132121, 3385, ~_t19 ] % 18.16/18.33 (309,1) [132147,3]. true => ~_t238 | ~_t237 | ~_t236 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t151 [ LRES, 132136, 3387, ~_t20 ] % 18.16/18.33 (351,1) [132149,3]. true => ~_t238 | ~_t237 | ~_t236 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t182 | ~_t161 [ LRES, 132147, 15349, ~_t151 ] % 18.16/18.33 (351,1) [132151,3]. true => ~_t238 | ~_t237 | ~_t236 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t218 | ~_t182 [ LRES, 132149, 3461, ~_t161 ] % 18.16/18.33 (1,1) [9,4]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 3174, _t6 ] % 18.16/18.33 (1,1) [247,4]. _t15 => box 1 _t16 [ SNF ] [ SNF++, 3176, _t16 ] % 18.16/18.33 (1,1) [484,4]. _t16 => box 1 _t17 [ SNF ] [ SNF++, 3178, _t17 ] % 18.16/18.33 (1,1) [720,4]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 3180, _t18 ] % 18.16/18.33 (1,1) [955,4]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 3182, _t19 ] % 18.16/18.33 (1,1) [1189,4]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 3184, _t20 ] % 18.16/18.33 (1,1) [1422,4]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 3186, _t21 ] % 18.16/18.33 (1,1) [1508,4]. _t83 => box 1 _t84 [ SNF ] [ SNF++, 3212, _t84 ] % 18.16/18.33 (1,1) [1509,4]. true => _t83 | ~_t82 | p4 [ SNF ] % 18.16/18.33 (1,1) [1510,4]. true => _t82 | ~_t81 [ SNF ] % 18.16/18.33 (1,1) [1515,4]. true => _t81 | ~_t80 | ~p104 [ SNF ] % 18.16/18.33 (1,1) [1516,4]. true => _t80 | ~_t21 [ SNF ] % 18.16/18.33 (265,1) [1600,4]. _t145 => ~box 1~ _t147 [ SNF ] [ SNF++, 3248, _t147 ] % 18.16/18.33 (1,1) [1605,4]. true => _t145 | ~_t144 | p105 | ~p104 [ SNF ] % 18.16/18.33 (1,1) [1606,4]. true => _t144 | ~_t21 [ SNF ] % 18.16/18.33 (309,1) [1839,4]. true => ~_t153 | ~p4 [ SNF ] % 18.16/18.33 (309,1) [1840,4]. true => ~_t153 | ~p105 [ SNF ] % 18.16/18.33 (309,1) [1841,4]. true => ~_t153 | p104 [ SNF ] % 18.16/18.33 (1,1) [3174,4]. _t5 => box 1 _t233 [ SNF++, 9 ] % 18.16/18.33 (1,1) [3176,4]. _t15 => box 1 _t234 [ SNF++, 247 ] % 18.16/18.33 (1,1) [3178,4]. _t16 => box 1 _t232 [ SNF++, 484 ] % 18.16/18.33 (1,1) [3180,4]. _t17 => box 1 _t230 [ SNF++, 720 ] % 18.16/18.33 (1,1) [3182,4]. _t18 => box 1 _t228 [ SNF++, 955 ] % 18.16/18.33 (1,1) [3184,4]. _t19 => box 1 _t226 [ SNF++, 1189 ] % 18.16/18.33 (1,1) [3186,4]. _t20 => box 1 _t182 [ SNF++, 1422 ] % 18.16/18.33 (1,1) [3212,4]. _t83 => box 1 _t195 [ SNF++, 1508 ] % 18.16/18.33 (265,1) [3248,4]. _t145 => ~box 1~ _t213 [ SNF++, 1600 ] % 18.16/18.33 (1,1) [3273,4]. true => ~_t235 | _t5 [ SNF++, 10 ] % 18.16/18.33 (1,1) [3275,4]. true => ~_t236 | _t15 [ SNF++, 248 ] % 18.16/18.33 (1,1) [3277,4]. true => ~_t234 | _t16 [ SNF++, 485 ] % 18.16/18.33 (1,1) [3279,4]. true => ~_t232 | _t17 [ SNF++, 721 ] % 18.16/18.33 (1,1) [3281,4]. true => ~_t230 | _t18 [ SNF++, 956 ] % 18.16/18.33 (1,1) [3283,4]. true => ~_t228 | _t19 [ SNF++, 1190 ] % 18.16/18.33 (1,1) [3285,4]. true => ~_t226 | _t20 [ SNF++, 1423 ] % 18.16/18.33 (1,1) [3287,4]. true => ~_t182 | _t21 [ SNF++, 1655 ] % 18.16/18.33 (309,1) [3353,4]. true => ~_t215 | _t153 [ SNF++, 1842 ] % 18.16/18.33 (1,1) [3757,4]. true => ~_t182 | _t144 [ LRES, 1606, 3287, ~_t21 ] % 18.16/18.33 (1,1) [3865,4]. true => ~_t182 | _t80 [ LRES, 1516, 3287, ~_t21 ] % 18.16/18.33 (309,1) [4514,4]. true => ~_t153 | _t83 | ~_t82 [ LRES, 1839, 1509, ~p4 ] % 18.16/18.33 (309,1) [6887,4]. true => ~_t153 | _t81 | ~_t80 [ LRES, 1515, 1841, ~p104 ] % 18.16/18.33 (309,1) [8342,4]. true => ~_t182 | ~_t153 | _t81 [ LRES, 6887, 3865, ~_t80 ] % 18.16/18.33 (309,1) [9335,4]. true => ~_t182 | ~_t153 | _t82 [ LRES, 8342, 1510, _t81 ] % 18.16/18.33 (309,1) [9844,4]. true => ~_t182 | ~_t153 | _t83 [ LRES, 9335, 4514, _t82 ] % 18.16/18.33 (309,1) [11153,4]. true => ~_t153 | _t145 | ~_t144 | p105 [ LRES, 1605, 1841, ~p104 ] [ Backward Subsumption, 14927 ] % 18.16/18.33 (309,1) [14927,4]. true => ~_t153 | _t145 | ~_t144 [ LRES, 11153, 1840, p105 ] % 18.16/18.33 (309,1) [14970,4]. true => ~_t182 | ~_t153 | _t145 [ LRES, 14927, 3757, ~_t144 ] % 18.16/18.33 (265,1) [124830,4]. true => ~_t145 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t5 [ GEN1, 3176, 3178, 3182, 3212, 3186, 3184, 3180, 3174, 3248, 124802, _t234, _t232, _t228, _t195, _t182, _t226, _t230, _t233, _t213 ] % 18.16/18.33 (265,1) [124849,4]. true => ~_t235 | ~_t145 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 [ LRES, 124830, 3273, ~_t5 ] % 18.16/18.33 (265,1) [124892,4]. true => ~_t236 | ~_t235 | ~_t145 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 [ LRES, 124849, 3275, ~_t15 ] % 18.16/18.33 (265,1) [124933,4]. true => ~_t236 | ~_t235 | ~_t234 | ~_t145 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 [ LRES, 124892, 3277, ~_t16 ] % 18.16/18.33 (265,1) [125023,4]. true => ~_t236 | ~_t235 | ~_t234 | ~_t232 | ~_t145 | ~_t83 | ~_t20 | ~_t19 | ~_t18 [ LRES, 124933, 3279, ~_t17 ] % 18.16/18.33 (265,1) [125039,4]. true => ~_t236 | ~_t235 | ~_t234 | ~_t232 | ~_t230 | ~_t145 | ~_t83 | ~_t20 | ~_t19 [ LRES, 125023, 3281, ~_t18 ] % 18.16/18.33 (265,1) [125041,4]. true => ~_t236 | ~_t235 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t145 | ~_t83 | ~_t20 [ LRES, 125039, 3283, ~_t19 ] % 18.16/18.33 (265,1) [125043,4]. true => ~_t236 | ~_t235 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t145 | ~_t83 [ LRES, 125041, 3285, ~_t20 ] % 18.16/18.33 (309,1) [125045,4]. true => ~_t236 | ~_t235 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t182 | ~_t153 | ~_t145 [ LRES, 125043, 9844, ~_t83 ] [ Backward Subsumption, 130284 ] % 18.16/18.33 (309,1) [130284,4]. true => ~_t236 | ~_t235 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t182 | ~_t153 [ LRES, 125045, 14970, ~_t145 ] % 18.16/18.33 (309,1) [130303,4]. true => ~_t236 | ~_t235 | ~_t234 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t215 | ~_t182 [ LRES, 130284, 3353, ~_t153 ] % 18.16/18.33 (1,1) [8,5]. _t6 => box 1 _t7 [ SNF ] [ SNF++, 3078, _t7 ] % 18.16/18.33 (1,1) [246,5]. _t16 => box 1 _t17 [ SNF ] [ SNF++, 3080, _t17 ] % 18.16/18.33 (1,1) [483,5]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 3082, _t18 ] % 18.16/18.33 (1,1) [719,5]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 3084, _t19 ] % 18.16/18.33 (1,1) [954,5]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 3086, _t20 ] % 18.16/18.33 (1,1) [1188,5]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 3088, _t21 ] % 18.16/18.33 (1,1) [1204,5]. true => ~_t27 | ~p105 | p104 [ SNF ] % 18.16/18.33 (1,1) [1205,5]. true => _t27 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [1275,5]. _t83 => box 1 _t84 [ SNF ] [ SNF++, 3114, _t84 ] % 18.16/18.33 (1,1) [1276,5]. true => _t83 | ~_t82 | p4 [ SNF ] % 18.16/18.33 (1,1) [1277,5]. true => _t82 | ~_t81 [ SNF ] % 18.16/18.33 (1,1) [1282,5]. true => _t81 | ~_t80 | ~p104 [ SNF ] % 18.16/18.33 (1,1) [1283,5]. true => _t80 | ~_t21 [ SNF ] % 18.16/18.33 (219,1) [1361,5]. _t139 => ~box 1~ _t143 [ SNF ] [ SNF++, 3148, _t143 ] % 18.16/18.33 (1,1) [1362,5]. true => _t139 | ~_t138 | p106 | ~p105 [ SNF ] % 18.16/18.33 (1,1) [1363,5]. true => _t138 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [1507,5]. true => ~_t84 | ~p4 | ~p104 [ SNF ] % 18.16/18.33 (265,1) [1598,5]. true => ~_t147 | ~p106 [ SNF ] % 18.16/18.33 (265,1) [1599,5]. true => ~_t147 | p105 [ SNF ] % 18.16/18.33 (1,1) [3078,5]. _t6 => box 1 _t231 [ SNF++, 8 ] % 18.16/18.33 (1,1) [3080,5]. _t16 => box 1 _t232 [ SNF++, 246 ] % 18.16/18.33 (1,1) [3082,5]. _t17 => box 1 _t230 [ SNF++, 483 ] % 18.16/18.33 (1,1) [3084,5]. _t18 => box 1 _t228 [ SNF++, 719 ] % 18.16/18.33 (1,1) [3086,5]. _t19 => box 1 _t226 [ SNF++, 954 ] % 18.16/18.33 (1,1) [3088,5]. _t20 => box 1 _t182 [ SNF++, 1188 ] % 18.16/18.33 (1,1) [3114,5]. _t83 => box 1 _t195 [ SNF++, 1275 ] % 18.16/18.33 (219,1) [3148,5]. _t139 => ~box 1~ _t212 [ SNF++, 1361 ] % 18.16/18.33 (1,1) [3175,5]. true => ~_t233 | _t6 [ SNF++, 9 ] % 18.16/18.33 (1,1) [3177,5]. true => ~_t234 | _t16 [ SNF++, 247 ] % 18.16/18.33 (1,1) [3179,5]. true => ~_t232 | _t17 [ SNF++, 484 ] % 18.16/18.33 (1,1) [3181,5]. true => ~_t230 | _t18 [ SNF++, 720 ] % 18.16/18.33 (1,1) [3183,5]. true => ~_t228 | _t19 [ SNF++, 955 ] % 18.16/18.33 (1,1) [3185,5]. true => ~_t226 | _t20 [ SNF++, 1189 ] % 18.16/18.33 (1,1) [3187,5]. true => ~_t182 | _t21 [ SNF++, 1422 ] % 18.16/18.33 (1,1) [3213,5]. true => ~_t195 | _t84 [ SNF++, 1508 ] % 18.16/18.33 (265,1) [3249,5]. true => ~_t213 | _t147 [ SNF++, 1600 ] % 18.16/18.33 (1,1) [3768,5]. true => ~_t182 | _t138 [ LRES, 1363, 3187, ~_t21 ] % 18.16/18.33 (1,1) [3864,5]. true => ~_t182 | _t80 [ LRES, 1283, 3187, ~_t21 ] % 18.16/18.33 (1,1) [3988,5]. true => ~_t182 | _t27 [ LRES, 1205, 3187, ~_t21 ] % 18.16/18.33 (1,1) [6855,5]. true => ~_t84 | ~_t27 | ~p4 | ~p105 [ LRES, 1507, 1204, ~p104 ] % 18.16/18.33 (1,1) [6883,5]. true => _t81 | ~_t80 | ~_t27 | ~p105 [ LRES, 1282, 1204, ~p104 ] % 18.16/18.33 (265,1) [10853,5]. true => ~_t147 | _t81 | ~_t80 | ~_t27 [ LRES, 6883, 1599, ~p105 ] % 18.16/18.33 (265,1) [10880,5]. true => ~_t147 | ~_t84 | ~_t27 | ~p4 [ LRES, 6855, 1599, ~p105 ] % 18.16/18.33 (265,1) [10988,5]. true => ~_t147 | _t139 | ~_t138 | p106 [ LRES, 1362, 1599, ~p105 ] [ Backward Subsumption, 14356 ] % 18.16/18.33 (265,1) [14047,5]. true => ~_t182 | ~_t147 | _t81 | ~_t80 [ LRES, 10853, 3988, ~_t27 ] [ Backward Subsumption, 17121 ] % 18.16/18.33 (265,1) [14081,5]. true => ~_t147 | ~_t84 | _t83 | ~_t82 | ~_t27 [ LRES, 10880, 1276, ~p4 ] % 18.16/18.33 (265,1) [14356,5]. true => ~_t147 | _t139 | ~_t138 [ LRES, 10988, 1598, p106 ] % 18.16/18.33 (265,1) [14411,5]. true => ~_t182 | ~_t147 | _t139 [ LRES, 14356, 3768, ~_t138 ] % 18.16/18.33 (265,1) [17121,5]. true => ~_t182 | ~_t147 | _t81 [ LRES, 14047, 3864, ~_t80 ] % 18.16/18.33 (265,1) [17131,5]. true => ~_t182 | ~_t147 | _t82 [ LRES, 17121, 1277, _t81 ] % 18.16/18.33 (265,1) [22790,5]. true => ~_t182 | ~_t147 | ~_t84 | _t83 | ~_t82 [ LRES, 14081, 3988, ~_t27 ] [ Backward Subsumption, 30340 ] % 18.16/18.33 (265,1) [30340,5]. true => ~_t182 | ~_t147 | ~_t84 | _t83 [ LRES, 22790, 17131, ~_t82 ] % 18.16/18.33 (219,1) [120168,5]. true => ~_t139 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t6 [ GEN1, 3080, 3082, 3086, 3088, 3114, 3084, 3078, 3148, 120167, _t232, _t230, _t226, _t182, _t195, _t228, _t231, _t212 ] % 18.16/18.33 (219,1) [120431,5]. true => ~_t233 | ~_t139 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 [ LRES, 120168, 3175, ~_t6 ] % 18.16/18.33 (219,1) [120449,5]. true => ~_t234 | ~_t233 | ~_t139 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 [ LRES, 120431, 3177, ~_t16 ] % 18.16/18.33 (219,1) [120490,5]. true => ~_t234 | ~_t233 | ~_t232 | ~_t139 | ~_t83 | ~_t20 | ~_t19 | ~_t18 [ LRES, 120449, 3179, ~_t17 ] % 18.16/18.33 (219,1) [120494,5]. true => ~_t234 | ~_t233 | ~_t232 | ~_t230 | ~_t139 | ~_t83 | ~_t20 | ~_t19 [ LRES, 120490, 3181, ~_t18 ] % 18.16/18.33 (219,1) [120498,5]. true => ~_t234 | ~_t233 | ~_t232 | ~_t230 | ~_t228 | ~_t139 | ~_t83 | ~_t20 [ LRES, 120494, 3183, ~_t19 ] % 18.16/18.33 (219,1) [120546,5]. true => ~_t234 | ~_t233 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t139 | ~_t83 [ LRES, 120498, 3185, ~_t20 ] % 18.16/18.33 (265,1) [120655,5]. true => ~_t234 | ~_t233 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t182 | ~_t147 | ~_t139 | ~_t84 [ LRES, 120546, 30340, ~_t83 ] % 18.16/18.33 (265,1) [122481,5]. true => ~_t234 | ~_t233 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t195 | ~_t182 | ~_t147 | ~_t139 [ LRES, 120655, 3213, ~_t84 ] [ Backward Subsumption, 124786 ] % 18.16/18.33 (265,1) [124786,5]. true => ~_t234 | ~_t233 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t195 | ~_t182 | ~_t147 [ LRES, 122481, 14411, ~_t139 ] % 18.16/18.33 (265,1) [124802,5]. true => ~_t234 | ~_t233 | ~_t232 | ~_t230 | ~_t228 | ~_t226 | ~_t213 | ~_t195 | ~_t182 [ LRES, 124786, 3249, ~_t147 ] % 18.16/18.33 (1,1) [7,6]. _t7 => box 1 _t8 [ SNF ] [ SNF++, 2984, _t8 ] % 18.16/18.33 (1,1) [245,6]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 2986, _t18 ] % 18.16/18.33 (1,1) [482,6]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 2988, _t19 ] % 18.16/18.33 (1,1) [718,6]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 2990, _t20 ] % 18.16/18.33 (1,1) [953,6]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 2992, _t21 ] % 18.16/18.33 (1,1) [968,6]. true => ~_t26 | ~p106 | p105 [ SNF ] % 18.16/18.33 (1,1) [969,6]. true => _t26 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [970,6]. true => ~_t27 | ~p105 | p104 [ SNF ] % 18.16/18.33 (1,1) [971,6]. true => _t27 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [1041,6]. _t83 => box 1 _t84 [ SNF ] [ SNF++, 3018, _t84 ] % 18.16/18.33 (1,1) [1042,6]. true => _t83 | ~_t82 | p4 [ SNF ] % 18.16/18.33 (1,1) [1043,6]. true => _t82 | ~_t81 [ SNF ] % 18.16/18.33 (1,1) [1048,6]. true => _t81 | ~_t80 | ~p104 [ SNF ] % 18.16/18.33 (1,1) [1049,6]. true => _t80 | ~_t21 [ SNF ] % 18.16/18.33 (177,1) [1113,6]. _t133 => ~box 1~ _t135 [ SNF ] [ SNF++, 3046, _t135 ] % 18.16/18.33 (1,1) [1118,6]. true => _t133 | ~_t132 | p107 | ~p106 [ SNF ] % 18.16/18.33 (1,1) [1119,6]. true => _t132 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [1274,6]. true => ~_t84 | ~p4 | ~p104 [ SNF ] % 18.16/18.33 (219,1) [1359,6]. true => ~_t143 | ~p107 [ SNF ] % 18.16/18.33 (219,1) [1360,6]. true => ~_t143 | p106 [ SNF ] % 18.16/18.33 (1,1) [2984,6]. _t7 => box 1 _t229 [ SNF++, 7 ] % 18.16/18.33 (1,1) [2986,6]. _t17 => box 1 _t230 [ SNF++, 245 ] % 18.16/18.33 (1,1) [2988,6]. _t18 => box 1 _t228 [ SNF++, 482 ] % 18.16/18.33 (1,1) [2990,6]. _t19 => box 1 _t226 [ SNF++, 718 ] % 18.16/18.33 (1,1) [2992,6]. _t20 => box 1 _t182 [ SNF++, 953 ] % 18.16/18.33 (1,1) [3018,6]. _t83 => box 1 _t195 [ SNF++, 1041 ] % 18.16/18.33 (177,1) [3046,6]. _t133 => ~box 1~ _t209 [ SNF++, 1113 ] % 18.16/18.33 (1,1) [3079,6]. true => ~_t231 | _t7 [ SNF++, 8 ] % 18.16/18.33 (1,1) [3081,6]. true => ~_t232 | _t17 [ SNF++, 246 ] % 18.16/18.33 (1,1) [3083,6]. true => ~_t230 | _t18 [ SNF++, 483 ] % 18.16/18.33 (1,1) [3085,6]. true => ~_t228 | _t19 [ SNF++, 719 ] % 18.16/18.33 (1,1) [3087,6]. true => ~_t226 | _t20 [ SNF++, 954 ] % 18.16/18.33 (1,1) [3089,6]. true => ~_t182 | _t21 [ SNF++, 1188 ] % 18.16/18.33 (1,1) [3115,6]. true => ~_t195 | _t84 [ SNF++, 1275 ] % 18.16/18.33 (219,1) [3149,6]. true => ~_t212 | _t143 [ SNF++, 1361 ] % 18.16/18.33 (1,1) [3779,6]. true => ~_t182 | _t132 [ LRES, 1119, 3089, ~_t21 ] % 18.16/18.33 (1,1) [3863,6]. true => ~_t182 | _t80 [ LRES, 1049, 3089, ~_t21 ] % 18.16/18.33 (1,1) [3987,6]. true => ~_t182 | _t27 [ LRES, 971, 3089, ~_t21 ] % 18.16/18.33 (1,1) [3998,6]. true => ~_t182 | _t26 [ LRES, 969, 3089, ~_t21 ] % 18.16/18.33 (1,1) [6852,6]. true => ~_t84 | ~_t27 | ~p4 | ~p105 [ LRES, 1274, 970, ~p104 ] % 18.16/18.33 (1,1) [6880,6]. true => _t81 | ~_t80 | ~_t27 | ~p105 [ LRES, 1048, 970, ~p104 ] % 18.16/18.33 (219,1) [10824,6]. true => ~_t143 | _t133 | ~_t132 | p107 [ LRES, 1118, 1360, ~p106 ] [ Backward Subsumption, 13636 ] % 18.16/18.33 (1,1) [10849,6]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~p106 [ LRES, 6880, 968, ~p105 ] % 18.16/18.33 (1,1) [10876,6]. true => ~_t84 | ~_t27 | ~_t26 | ~p4 | ~p106 [ LRES, 6852, 968, ~p105 ] % 18.16/18.33 (219,1) [13636,6]. true => ~_t143 | _t133 | ~_t132 [ LRES, 10824, 1359, p107 ] % 18.16/18.33 (219,1) [13706,6]. true => ~_t182 | ~_t143 | _t133 [ LRES, 13636, 3779, ~_t132 ] % 18.16/18.33 (219,1) [19485,6]. true => ~_t143 | ~_t84 | ~_t27 | ~_t26 | ~p4 [ LRES, 10876, 1360, ~p106 ] % 18.16/18.33 (219,1) [19510,6]. true => ~_t143 | _t81 | ~_t80 | ~_t27 | ~_t26 [ LRES, 10849, 1360, ~p106 ] % 18.16/18.33 (219,1) [22016,6]. true => ~_t182 | ~_t143 | _t81 | ~_t80 | ~_t27 [ LRES, 19510, 3998, ~_t26 ] [ Backward Subsumption, 22633 ] % 18.16/18.33 (219,1) [22633,6]. true => ~_t182 | ~_t143 | _t81 | ~_t80 [ LRES, 22016, 3987, ~_t27 ] [ Backward Subsumption, 22640 ] % 18.16/18.33 (219,1) [22640,6]. true => ~_t182 | ~_t143 | _t81 [ LRES, 22633, 3863, ~_t80 ] % 18.16/18.33 (219,1) [22649,6]. true => ~_t182 | ~_t143 | _t82 [ LRES, 22640, 1043, _t81 ] % 18.16/18.33 (219,1) [23518,6]. true => ~_t143 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 [ LRES, 19485, 1042, ~p4 ] % 18.16/18.33 (219,1) [34662,6]. true => ~_t182 | ~_t143 | ~_t84 | _t83 | ~_t82 | ~_t27 [ LRES, 23518, 3998, ~_t26 ] [ Backward Subsumption, 34890 ] % 18.16/18.33 (219,1) [34890,6]. true => ~_t182 | ~_t143 | ~_t84 | _t83 | ~_t82 [ LRES, 34662, 3987, ~_t27 ] [ Backward Subsumption, 34897 ] % 18.16/18.33 (219,1) [34897,6]. true => ~_t182 | ~_t143 | ~_t84 | _t83 [ LRES, 34890, 22649, ~_t82 ] % 18.16/18.33 (177,1) [119682,6]. true => ~_t133 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t7 [ GEN1, 2986, 2988, 3018, 2992, 2990, 2984, 3046, 119680, _t230, _t228, _t195, _t182, _t226, _t229, _t209 ] % 18.16/18.33 (177,1) [119933,6]. true => ~_t231 | ~_t133 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 [ LRES, 119682, 3079, ~_t7 ] % 18.16/18.33 (177,1) [119952,6]. true => ~_t232 | ~_t231 | ~_t133 | ~_t83 | ~_t20 | ~_t19 | ~_t18 [ LRES, 119933, 3081, ~_t17 ] % 18.16/18.33 (177,1) [120020,6]. true => ~_t232 | ~_t231 | ~_t230 | ~_t133 | ~_t83 | ~_t20 | ~_t19 [ LRES, 119952, 3083, ~_t18 ] % 18.16/18.33 (177,1) [120095,6]. true => ~_t232 | ~_t231 | ~_t230 | ~_t228 | ~_t133 | ~_t83 | ~_t20 [ LRES, 120020, 3085, ~_t19 ] % 18.16/18.33 (177,1) [120096,6]. true => ~_t232 | ~_t231 | ~_t230 | ~_t228 | ~_t226 | ~_t133 | ~_t83 [ LRES, 120095, 3087, ~_t20 ] % 18.16/18.33 (219,1) [120133,6]. true => ~_t232 | ~_t231 | ~_t230 | ~_t228 | ~_t226 | ~_t182 | ~_t143 | ~_t133 | ~_t84 [ LRES, 120096, 34897, ~_t83 ] % 18.16/18.33 (219,1) [120164,6]. true => ~_t232 | ~_t231 | ~_t230 | ~_t228 | ~_t226 | ~_t195 | ~_t182 | ~_t143 | ~_t133 [ LRES, 120133, 3115, ~_t84 ] [ Backward Subsumption, 120166 ] % 18.16/18.33 (219,1) [120166,6]. true => ~_t232 | ~_t231 | ~_t230 | ~_t228 | ~_t226 | ~_t195 | ~_t182 | ~_t143 [ LRES, 120164, 13706, ~_t133 ] % 18.16/18.33 (219,1) [120167,6]. true => ~_t232 | ~_t231 | ~_t230 | ~_t228 | ~_t226 | ~_t212 | ~_t195 | ~_t182 [ LRES, 120166, 3149, ~_t143 ] % 18.16/18.33 (1,1) [6,7]. _t8 => box 1 _t9 [ SNF ] [ SNF++, 2892, _t9 ] % 18.16/18.33 (1,1) [244,7]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 2894, _t19 ] % 18.16/18.33 (1,1) [481,7]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 2896, _t20 ] % 18.16/18.33 (1,1) [717,7]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 2898, _t21 ] % 18.16/18.33 (1,1) [731,7]. true => ~_t25 | ~p107 | p106 [ SNF ] % 18.16/18.33 (1,1) [732,7]. true => _t25 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [733,7]. true => ~_t26 | ~p106 | p105 [ SNF ] % 18.16/18.33 (1,1) [734,7]. true => _t26 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [735,7]. true => ~_t27 | ~p105 | p104 [ SNF ] % 18.16/18.33 (1,1) [736,7]. true => _t27 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [806,7]. _t83 => box 1 _t84 [ SNF ] [ SNF++, 2924, _t84 ] % 18.16/18.33 (1,1) [807,7]. true => _t83 | ~_t82 | p4 [ SNF ] % 18.16/18.33 (1,1) [808,7]. true => _t82 | ~_t81 [ SNF ] % 18.16/18.33 (1,1) [813,7]. true => _t81 | ~_t80 | ~p104 [ SNF ] % 18.16/18.33 (1,1) [814,7]. true => _t80 | ~_t21 [ SNF ] % 18.16/18.33 (131,1) [872,7]. _t127 => ~box 1~ _t131 [ SNF ] [ SNF++, 2950, _t131 ] % 18.16/18.33 (1,1) [873,7]. true => _t127 | ~_t126 | p108 | ~p107 [ SNF ] % 18.16/18.33 (1,1) [874,7]. true => _t126 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [1040,7]. true => ~_t84 | ~p4 | ~p104 [ SNF ] % 18.16/18.33 (177,1) [1111,7]. true => ~_t135 | ~p108 [ SNF ] % 18.16/18.33 (177,1) [1112,7]. true => ~_t135 | p107 [ SNF ] % 18.16/18.33 (1,1) [2892,7]. _t8 => box 1 _t227 [ SNF++, 6 ] % 18.16/18.33 (1,1) [2894,7]. _t18 => box 1 _t228 [ SNF++, 244 ] % 18.16/18.33 (1,1) [2896,7]. _t19 => box 1 _t226 [ SNF++, 481 ] % 18.16/18.33 (1,1) [2898,7]. _t20 => box 1 _t182 [ SNF++, 717 ] % 18.16/18.33 (1,1) [2924,7]. _t83 => box 1 _t195 [ SNF++, 806 ] % 18.16/18.33 (131,1) [2950,7]. _t127 => ~box 1~ _t208 [ SNF++, 872 ] % 18.16/18.33 (1,1) [2985,7]. true => ~_t229 | _t8 [ SNF++, 7 ] % 18.16/18.33 (1,1) [2987,7]. true => ~_t230 | _t18 [ SNF++, 245 ] % 18.16/18.33 (1,1) [2989,7]. true => ~_t228 | _t19 [ SNF++, 482 ] % 18.16/18.33 (1,1) [2991,7]. true => ~_t226 | _t20 [ SNF++, 718 ] % 18.16/18.33 (1,1) [2993,7]. true => ~_t182 | _t21 [ SNF++, 953 ] % 18.16/18.33 (1,1) [3019,7]. true => ~_t195 | _t84 [ SNF++, 1041 ] % 18.16/18.33 (177,1) [3047,7]. true => ~_t209 | _t135 [ SNF++, 1113 ] % 18.16/18.33 (1,1) [3790,7]. true => ~_t182 | _t126 [ LRES, 874, 2993, ~_t21 ] % 18.16/18.33 (1,1) [3862,7]. true => ~_t182 | _t80 [ LRES, 814, 2993, ~_t21 ] % 18.16/18.33 (1,1) [3986,7]. true => ~_t182 | _t27 [ LRES, 736, 2993, ~_t21 ] % 18.16/18.33 (1,1) [3997,7]. true => ~_t182 | _t26 [ LRES, 734, 2993, ~_t21 ] % 18.16/18.33 (1,1) [4008,7]. true => ~_t182 | _t25 [ LRES, 732, 2993, ~_t21 ] % 18.16/18.33 (1,1) [6849,7]. true => ~_t84 | ~_t27 | ~p4 | ~p105 [ LRES, 1040, 735, ~p104 ] % 18.16/18.33 (1,1) [6877,7]. true => _t81 | ~_t80 | ~_t27 | ~p105 [ LRES, 813, 735, ~p104 ] % 18.16/18.33 (177,1) [10658,7]. true => ~_t135 | _t127 | ~_t126 | p108 [ LRES, 873, 1112, ~p107 ] [ Backward Subsumption, 13212 ] % 18.16/18.33 (1,1) [10846,7]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~p106 [ LRES, 6877, 733, ~p105 ] % 18.16/18.33 (1,1) [10873,7]. true => ~_t84 | ~_t27 | ~_t26 | ~p4 | ~p106 [ LRES, 6849, 733, ~p105 ] % 18.16/18.33 (177,1) [13212,7]. true => ~_t135 | _t127 | ~_t126 [ LRES, 10658, 1111, p108 ] % 18.16/18.33 (177,1) [13291,7]. true => ~_t182 | ~_t135 | _t127 [ LRES, 13212, 3790, ~_t126 ] % 18.16/18.33 (1,1) [19655,7]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~p4 | ~p107 [ LRES, 10873, 731, ~p106 ] % 18.16/18.33 (1,1) [19679,7]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~p107 [ LRES, 10846, 731, ~p106 ] % 18.16/18.33 (177,1) [36988,7]. true => ~_t135 | _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 [ LRES, 19679, 1112, ~p107 ] % 18.16/18.33 (177,1) [37014,7]. true => ~_t135 | ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~p4 [ LRES, 19655, 1112, ~p107 ] % 18.16/18.33 (177,1) [40938,7]. true => ~_t182 | ~_t135 | _t81 | ~_t80 | ~_t27 | ~_t26 [ LRES, 36988, 4008, ~_t25 ] [ Backward Subsumption, 41005 ] % 18.16/18.33 (177,1) [40971,7]. true => ~_t135 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 | ~_t25 [ LRES, 37014, 807, ~p4 ] % 18.16/18.33 (177,1) [41005,7]. true => ~_t182 | ~_t135 | _t81 | ~_t80 | ~_t27 [ LRES, 40938, 3997, ~_t26 ] [ Backward Subsumption, 41010 ] % 18.16/18.33 (177,1) [41010,7]. true => ~_t182 | ~_t135 | _t81 | ~_t80 [ LRES, 41005, 3986, ~_t27 ] [ Backward Subsumption, 41016 ] % 18.16/18.33 (177,1) [41016,7]. true => ~_t182 | ~_t135 | _t81 [ LRES, 41010, 3862, ~_t80 ] % 18.16/18.33 (177,1) [41021,7]. true => ~_t182 | ~_t135 | _t82 [ LRES, 41016, 808, _t81 ] % 18.16/18.33 (177,1) [54691,7]. true => ~_t182 | ~_t135 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 [ LRES, 40971, 4008, ~_t25 ] [ Backward Subsumption, 54904 ] % 18.16/18.33 (177,1) [54904,7]. true => ~_t182 | ~_t135 | ~_t84 | _t83 | ~_t82 | ~_t27 [ LRES, 54691, 3997, ~_t26 ] [ Backward Subsumption, 54906 ] % 18.16/18.33 (177,1) [54906,7]. true => ~_t182 | ~_t135 | ~_t84 | _t83 | ~_t82 [ LRES, 54904, 3986, ~_t27 ] [ Backward Subsumption, 54912 ] % 18.16/18.33 (177,1) [54912,7]. true => ~_t182 | ~_t135 | ~_t84 | _t83 [ LRES, 54906, 41021, ~_t82 ] % 18.16/18.33 (131,1) [119628,7]. true => ~_t127 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t8 [ GEN1, 2894, 2896, 2898, 2924, 2892, 2950, 119626, _t228, _t226, _t182, _t195, _t227, _t208 ] % 18.16/18.33 (131,1) [119629,7]. true => ~_t229 | ~_t127 | ~_t83 | ~_t20 | ~_t19 | ~_t18 [ LRES, 119628, 2985, ~_t8 ] % 18.16/18.33 (131,1) [119631,7]. true => ~_t230 | ~_t229 | ~_t127 | ~_t83 | ~_t20 | ~_t19 [ LRES, 119629, 2987, ~_t18 ] % 18.16/18.33 (131,1) [119634,7]. true => ~_t230 | ~_t229 | ~_t228 | ~_t127 | ~_t83 | ~_t20 [ LRES, 119631, 2989, ~_t19 ] % 18.16/18.33 (131,1) [119636,7]. true => ~_t230 | ~_t229 | ~_t228 | ~_t226 | ~_t127 | ~_t83 [ LRES, 119634, 2991, ~_t20 ] % 18.16/18.33 (177,1) [119657,7]. true => ~_t230 | ~_t229 | ~_t228 | ~_t226 | ~_t182 | ~_t135 | ~_t127 | ~_t84 [ LRES, 119636, 54912, ~_t83 ] % 18.16/18.33 (177,1) [119671,7]. true => ~_t230 | ~_t229 | ~_t228 | ~_t226 | ~_t195 | ~_t182 | ~_t135 | ~_t127 [ LRES, 119657, 3019, ~_t84 ] [ Backward Subsumption, 119676 ] % 18.16/18.33 (177,1) [119676,7]. true => ~_t230 | ~_t229 | ~_t228 | ~_t226 | ~_t195 | ~_t182 | ~_t135 [ LRES, 119671, 13291, ~_t127 ] % 18.16/18.33 (177,1) [119680,7]. true => ~_t230 | ~_t229 | ~_t228 | ~_t226 | ~_t209 | ~_t195 | ~_t182 [ LRES, 119676, 3047, ~_t135 ] % 18.16/18.33 (1,1) [5,8]. _t9 => box 1 _t10 [ SNF ] [ SNF++, 2802, _t10 ] % 18.16/18.33 (1,1) [243,8]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 2804, _t20 ] % 18.16/18.33 (1,1) [480,8]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 2806, _t21 ] % 18.16/18.33 (1,1) [493,8]. true => ~_t24 | ~p108 | p107 [ SNF ] % 18.16/18.33 (1,1) [494,8]. true => _t24 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [495,8]. true => ~_t25 | ~p107 | p106 [ SNF ] % 18.16/18.33 (1,1) [496,8]. true => _t25 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [497,8]. true => ~_t26 | ~p106 | p105 [ SNF ] % 18.16/18.33 (1,1) [498,8]. true => _t26 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [499,8]. true => ~_t27 | ~p105 | p104 [ SNF ] % 18.16/18.33 (1,1) [500,8]. true => _t27 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [570,8]. _t83 => box 1 _t84 [ SNF ] [ SNF++, 2832, _t84 ] % 18.16/18.33 (1,1) [571,8]. true => _t83 | ~_t82 | p4 [ SNF ] % 18.16/18.33 (1,1) [572,8]. true => _t82 | ~_t81 [ SNF ] % 18.16/18.33 (1,1) [577,8]. true => _t81 | ~_t80 | ~p104 [ SNF ] % 18.16/18.33 (1,1) [578,8]. true => _t80 | ~_t21 [ SNF ] % 18.16/18.33 (87,1) [626,8]. _t121 => ~box 1~ _t125 [ SNF ] [ SNF++, 2854, _t125 ] % 18.16/18.33 (1,1) [627,8]. true => _t121 | ~_t120 | p109 | ~p108 [ SNF ] % 18.16/18.33 (1,1) [628,8]. true => _t120 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [805,8]. true => ~_t84 | ~p4 | ~p104 [ SNF ] % 18.16/18.33 (131,1) [870,8]. true => ~_t131 | ~p109 [ SNF ] % 18.16/18.33 (131,1) [871,8]. true => ~_t131 | p108 [ SNF ] % 18.16/18.33 (1,1) [2802,8]. _t9 => box 1 _t225 [ SNF++, 5 ] % 18.16/18.33 (1,1) [2804,8]. _t19 => box 1 _t226 [ SNF++, 243 ] % 18.16/18.33 (1,1) [2806,8]. _t20 => box 1 _t182 [ SNF++, 480 ] % 18.16/18.33 (1,1) [2832,8]. _t83 => box 1 _t195 [ SNF++, 570 ] % 18.16/18.33 (87,1) [2854,8]. _t121 => ~box 1~ _t206 [ SNF++, 626 ] % 18.16/18.33 (1,1) [2893,8]. true => ~_t227 | _t9 [ SNF++, 6 ] % 18.16/18.33 (1,1) [2895,8]. true => ~_t228 | _t19 [ SNF++, 244 ] % 18.16/18.33 (1,1) [2897,8]. true => ~_t226 | _t20 [ SNF++, 481 ] % 18.16/18.33 (1,1) [2899,8]. true => ~_t182 | _t21 [ SNF++, 717 ] % 18.16/18.33 (1,1) [2925,8]. true => ~_t195 | _t84 [ SNF++, 806 ] % 18.16/18.33 (131,1) [2951,8]. true => ~_t208 | _t131 [ SNF++, 872 ] % 18.16/18.33 (1,1) [3801,8]. true => ~_t182 | _t120 [ LRES, 628, 2899, ~_t21 ] % 18.16/18.33 (1,1) [3861,8]. true => ~_t182 | _t80 [ LRES, 578, 2899, ~_t21 ] % 18.16/18.33 (1,1) [3985,8]. true => ~_t182 | _t27 [ LRES, 500, 2899, ~_t21 ] % 18.16/18.33 (1,1) [3996,8]. true => ~_t182 | _t26 [ LRES, 498, 2899, ~_t21 ] % 18.16/18.33 (1,1) [4007,8]. true => ~_t182 | _t25 [ LRES, 496, 2899, ~_t21 ] % 18.16/18.33 (1,1) [4018,8]. true => ~_t182 | _t24 [ LRES, 494, 2899, ~_t21 ] % 18.16/18.33 (1,1) [6846,8]. true => ~_t84 | ~_t27 | ~p4 | ~p105 [ LRES, 805, 499, ~p104 ] % 18.16/18.33 (1,1) [6874,8]. true => _t81 | ~_t80 | ~_t27 | ~p105 [ LRES, 577, 499, ~p104 ] % 18.16/18.33 (131,1) [10494,8]. true => ~_t131 | _t121 | ~_t120 | p109 [ LRES, 627, 871, ~p108 ] [ Backward Subsumption, 12494 ] % 18.16/18.33 (1,1) [10843,8]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~p106 [ LRES, 6874, 497, ~p105 ] % 18.16/18.33 (1,1) [10870,8]. true => ~_t84 | ~_t27 | ~_t26 | ~p4 | ~p106 [ LRES, 6846, 497, ~p105 ] % 18.16/18.33 (131,1) [12494,8]. true => ~_t131 | _t121 | ~_t120 [ LRES, 10494, 870, p109 ] % 18.16/18.33 (131,1) [12588,8]. true => ~_t182 | ~_t131 | _t121 [ LRES, 12494, 3801, ~_t120 ] % 18.16/18.33 (1,1) [19676,8]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~p4 | ~p107 [ LRES, 10870, 495, ~p106 ] % 18.16/18.33 (1,1) [19701,8]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~p107 [ LRES, 10843, 495, ~p106 ] % 18.16/18.33 (1,1) [36984,8]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~p108 [ LRES, 19701, 493, ~p107 ] % 18.16/18.33 (1,1) [37010,8]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~p4 | ~p108 [ LRES, 19676, 493, ~p107 ] % 18.16/18.33 (131,1) [49231,8]. true => ~_t131 | ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~p4 [ LRES, 37010, 871, ~p108 ] % 18.16/18.33 (131,1) [49241,8]. true => ~_t131 | _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~_t24 [ LRES, 36984, 871, ~p108 ] % 18.16/18.33 (131,1) [52806,8]. true => ~_t182 | ~_t131 | _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 [ LRES, 49241, 4018, ~_t24 ] [ Backward Subsumption, 54277 ] % 18.16/18.33 (131,1) [54277,8]. true => ~_t182 | ~_t131 | _t81 | ~_t80 | ~_t27 | ~_t26 [ LRES, 52806, 4007, ~_t25 ] [ Backward Subsumption, 54287 ] % 18.16/18.33 (131,1) [54287,8]. true => ~_t182 | ~_t131 | _t81 | ~_t80 | ~_t27 [ LRES, 54277, 3996, ~_t26 ] [ Backward Subsumption, 54295 ] % 18.16/18.33 (131,1) [54295,8]. true => ~_t182 | ~_t131 | _t81 | ~_t80 [ LRES, 54287, 3985, ~_t27 ] [ Backward Subsumption, 54302 ] % 18.16/18.33 (131,1) [54302,8]. true => ~_t182 | ~_t131 | _t81 [ LRES, 54295, 3861, ~_t80 ] % 18.16/18.33 (131,1) [54312,8]. true => ~_t182 | ~_t131 | _t82 [ LRES, 54302, 572, _t81 ] % 18.16/18.33 (131,1) [61730,8]. true => ~_t131 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 | ~_t25 | ~_t24 [ LRES, 49231, 571, ~p4 ] % 18.16/18.33 (131,1) [70631,8]. true => ~_t182 | ~_t131 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 | ~_t25 [ LRES, 61730, 4018, ~_t24 ] [ Backward Subsumption, 71188 ] % 18.16/18.33 (131,1) [71188,8]. true => ~_t182 | ~_t131 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 [ LRES, 70631, 4007, ~_t25 ] [ Backward Subsumption, 71192 ] % 18.16/18.33 (131,1) [71192,8]. true => ~_t182 | ~_t131 | ~_t84 | _t83 | ~_t82 | ~_t27 [ LRES, 71188, 3996, ~_t26 ] [ Backward Subsumption, 71194 ] % 18.16/18.33 (131,1) [71194,8]. true => ~_t182 | ~_t131 | ~_t84 | _t83 | ~_t82 [ LRES, 71192, 3985, ~_t27 ] [ Backward Subsumption, 71198 ] % 18.16/18.33 (131,1) [71198,8]. true => ~_t182 | ~_t131 | ~_t84 | _t83 [ LRES, 71194, 54312, ~_t82 ] % 18.16/18.33 (87,1) [118650,8]. true => ~_t121 | ~_t83 | ~_t20 | ~_t19 | ~_t9 [ GEN1, 2804, 2832, 2806, 2802, 2854, 118611, _t226, _t195, _t182, _t225, _t206 ] % 18.16/18.33 (87,1) [118651,8]. true => ~_t227 | ~_t121 | ~_t83 | ~_t20 | ~_t19 [ LRES, 118650, 2893, ~_t9 ] % 18.16/18.33 (87,1) [118654,8]. true => ~_t228 | ~_t227 | ~_t121 | ~_t83 | ~_t20 [ LRES, 118651, 2895, ~_t19 ] % 18.16/18.33 (87,1) [118656,8]. true => ~_t228 | ~_t227 | ~_t226 | ~_t121 | ~_t83 [ LRES, 118654, 2897, ~_t20 ] % 18.16/18.33 (131,1) [118677,8]. true => ~_t228 | ~_t227 | ~_t226 | ~_t182 | ~_t131 | ~_t121 | ~_t84 [ LRES, 118656, 71198, ~_t83 ] % 18.16/18.33 (131,1) [119622,8]. true => ~_t228 | ~_t227 | ~_t226 | ~_t195 | ~_t182 | ~_t131 | ~_t121 [ LRES, 118677, 2925, ~_t84 ] [ Backward Subsumption, 119625 ] % 18.16/18.33 (131,1) [119625,8]. true => ~_t228 | ~_t227 | ~_t226 | ~_t195 | ~_t182 | ~_t131 [ LRES, 119622, 12588, ~_t121 ] % 18.16/18.33 (131,1) [119626,8]. true => ~_t228 | ~_t227 | ~_t226 | ~_t208 | ~_t195 | ~_t182 [ LRES, 119625, 2951, ~_t131 ] % 18.16/18.33 (1,1) [4,9]. _t10 => box 1 p4 [ SNF ] [ SNF++, 2714, p4 ] % 18.16/18.33 (1,1) [242,9]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 2716, _t21 ] % 18.16/18.33 (1,1) [254,9]. true => ~_t23 | ~p109 | p108 [ SNF ] % 18.16/18.33 (1,1) [255,9]. true => _t23 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [256,9]. true => ~_t24 | ~p108 | p107 [ SNF ] % 18.16/18.33 (1,1) [257,9]. true => _t24 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [258,9]. true => ~_t25 | ~p107 | p106 [ SNF ] % 18.16/18.33 (1,1) [259,9]. true => _t25 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [260,9]. true => ~_t26 | ~p106 | p105 [ SNF ] % 18.16/18.33 (1,1) [261,9]. true => _t26 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [262,9]. true => ~_t27 | ~p105 | p104 [ SNF ] % 18.16/18.33 (1,1) [263,9]. true => _t27 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [333,9]. _t83 => box 1 _t84 [ SNF ] [ SNF++, 2742, _t84 ] % 18.16/18.33 (1,1) [334,9]. true => _t83 | ~_t82 | p4 [ SNF ] % 18.16/18.33 (1,1) [335,9]. true => _t82 | ~_t81 [ SNF ] % 18.16/18.33 (1,1) [340,9]. true => _t81 | ~_t80 | ~p104 [ SNF ] % 18.16/18.33 (1,1) [341,9]. true => _t80 | ~_t21 [ SNF ] % 18.16/18.33 (43,1) [477,9]. _t175 => ~box 1~ _t179 [ SNF ] [ SNF++, 2800, _t179 ] % 18.16/18.33 (1,1) [478,9]. true => _t175 | ~_t174 | p110 | ~p109 [ SNF ] % 18.16/18.33 (1,1) [479,9]. true => _t174 | ~_t21 [ SNF ] % 18.16/18.33 (1,1) [569,9]. true => ~_t84 | ~p4 | ~p104 [ SNF ] % 18.16/18.33 (87,1) [624,9]. true => ~_t125 | ~p110 [ SNF ] % 18.16/18.33 (87,1) [625,9]. true => ~_t125 | p109 [ SNF ] % 18.16/18.33 (1,1) [2714,9]. _t10 => box 1 _t181 [ SNF++, 4 ] % 18.16/18.33 (1,1) [2716,9]. _t20 => box 1 _t182 [ SNF++, 242 ] % 18.16/18.33 (1,1) [2742,9]. _t83 => box 1 _t195 [ SNF++, 333 ] % 18.16/18.33 (43,1) [2800,9]. _t175 => ~box 1~ _t224 [ SNF++, 477 ] % 18.16/18.33 (1,1) [2803,9]. true => ~_t225 | _t10 [ SNF++, 5 ] % 18.16/18.33 (1,1) [2805,9]. true => ~_t226 | _t20 [ SNF++, 243 ] % 18.16/18.33 (1,1) [2807,9]. true => ~_t182 | _t21 [ SNF++, 480 ] % 18.16/18.33 (1,1) [2833,9]. true => ~_t195 | _t84 [ SNF++, 570 ] % 18.16/18.33 (87,1) [2855,9]. true => ~_t206 | _t125 [ SNF++, 626 ] % 18.16/18.33 (1,1) [3692,9]. true => ~_t182 | _t174 [ LRES, 479, 2807, ~_t21 ] % 18.16/18.33 (1,1) [3860,9]. true => ~_t182 | _t80 [ LRES, 341, 2807, ~_t21 ] % 18.16/18.33 (1,1) [3984,9]. true => ~_t182 | _t27 [ LRES, 263, 2807, ~_t21 ] % 18.16/18.33 (1,1) [3995,9]. true => ~_t182 | _t26 [ LRES, 261, 2807, ~_t21 ] % 18.16/18.33 (1,1) [4006,9]. true => ~_t182 | _t25 [ LRES, 259, 2807, ~_t21 ] % 18.16/18.33 (1,1) [4017,9]. true => ~_t182 | _t24 [ LRES, 257, 2807, ~_t21 ] % 18.16/18.33 (1,1) [4028,9]. true => ~_t182 | _t23 [ LRES, 255, 2807, ~_t21 ] % 18.16/18.33 (1,1) [6898,9]. true => ~_t84 | ~_t27 | ~p4 | ~p105 [ LRES, 569, 262, ~p104 ] % 18.16/18.33 (1,1) [6919,9]. true => _t81 | ~_t80 | ~_t27 | ~p105 [ LRES, 340, 262, ~p104 ] % 18.16/18.33 (87,1) [10383,9]. true => _t175 | ~_t174 | ~_t125 | p110 [ LRES, 478, 625, ~p109 ] [ Backward Subsumption, 12031 ] % 18.16/18.33 (1,1) [10894,9]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~p106 [ LRES, 6919, 260, ~p105 ] % 18.16/18.33 (1,1) [10921,9]. true => ~_t84 | ~_t27 | ~_t26 | ~p4 | ~p106 [ LRES, 6898, 260, ~p105 ] % 18.16/18.33 (87,1) [12031,9]. true => _t175 | ~_t174 | ~_t125 [ LRES, 10383, 624, p110 ] % 18.16/18.33 (87,1) [12049,9]. true => ~_t206 | _t175 | ~_t174 [ LRES, 12031, 2855, ~_t125 ] % 18.16/18.33 (87,1) [12076,9]. true => ~_t206 | ~_t182 | _t175 [ LRES, 12049, 3692, ~_t174 ] % 18.16/18.33 (1,1) [19698,9]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~p4 | ~p107 [ LRES, 10921, 258, ~p106 ] % 18.16/18.33 (1,1) [19723,9]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~p107 [ LRES, 10894, 258, ~p106 ] % 18.16/18.33 (1,1) [36931,9]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~p108 [ LRES, 19723, 256, ~p107 ] % 18.16/18.33 (1,1) [36956,9]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~p4 | ~p108 [ LRES, 19698, 256, ~p107 ] % 18.16/18.33 (1,1) [49998,9]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 | ~p4 | ~p109 [ LRES, 36956, 254, ~p108 ] % 18.16/18.33 (1,1) [50013,9]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 | ~p109 [ LRES, 36931, 254, ~p108 ] % 18.16/18.33 (43,1) [73980,9]. true => ~_t175 | ~_t83 | ~_t20 | ~_t10 [ GEN1, 2742, 2714, 2716, 2800, 73970, _t195, _t181, _t182, _t224 ] % 18.16/18.33 (43,1) [73981,9]. true => ~_t225 | ~_t175 | ~_t83 | ~_t20 [ LRES, 73980, 2803, ~_t10 ] % 18.16/18.33 (43,1) [73987,9]. true => ~_t226 | ~_t225 | ~_t175 | ~_t83 [ LRES, 73981, 2805, ~_t20 ] % 18.16/18.33 (87,1) [80385,9]. true => ~_t125 | _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 [ LRES, 50013, 625, ~p109 ] % 18.16/18.33 (87,1) [80389,9]. true => ~_t125 | ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 | ~p4 [ LRES, 49998, 625, ~p109 ] % 18.16/18.33 (87,1) [88635,9]. true => ~_t182 | ~_t125 | _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~_t24 [ LRES, 80385, 4028, ~_t23 ] [ Backward Subsumption, 91147 ] % 18.16/18.33 (87,1) [91147,9]. true => ~_t182 | ~_t125 | _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 [ LRES, 88635, 4017, ~_t24 ] [ Backward Subsumption, 91151 ] % 18.16/18.33 (87,1) [91151,9]. true => ~_t182 | ~_t125 | _t81 | ~_t80 | ~_t27 | ~_t26 [ LRES, 91147, 4006, ~_t25 ] [ Backward Subsumption, 91154 ] % 18.16/18.33 (87,1) [91154,9]. true => ~_t182 | ~_t125 | _t81 | ~_t80 | ~_t27 [ LRES, 91151, 3995, ~_t26 ] [ Backward Subsumption, 91157 ] % 18.16/18.33 (87,1) [91157,9]. true => ~_t182 | ~_t125 | _t81 | ~_t80 [ LRES, 91154, 3984, ~_t27 ] [ Backward Subsumption, 91160 ] % 18.16/18.33 (87,1) [91160,9]. true => ~_t182 | ~_t125 | _t81 [ LRES, 91157, 3860, ~_t80 ] % 18.16/18.33 (87,1) [91176,9]. true => ~_t182 | ~_t125 | _t82 [ LRES, 91160, 335, _t81 ] % 18.16/18.33 (87,1) [110483,9]. true => ~_t125 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 [ LRES, 80389, 334, ~p4 ] % 18.16/18.33 (87,1) [118417,9]. true => ~_t182 | ~_t125 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 | ~_t25 | ~_t24 [ LRES, 110483, 4028, ~_t23 ] [ Backward Subsumption, 118419 ] % 18.16/18.33 (87,1) [118419,9]. true => ~_t182 | ~_t125 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 | ~_t25 [ LRES, 118417, 4017, ~_t24 ] [ Backward Subsumption, 118420 ] % 18.16/18.33 (87,1) [118420,9]. true => ~_t182 | ~_t125 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 [ LRES, 118419, 4006, ~_t25 ] [ Backward Subsumption, 118421 ] % 18.16/18.33 (87,1) [118421,9]. true => ~_t182 | ~_t125 | ~_t84 | _t83 | ~_t82 | ~_t27 [ LRES, 118420, 3995, ~_t26 ] [ Backward Subsumption, 118422 ] % 18.16/18.33 (87,1) [118422,9]. true => ~_t182 | ~_t125 | ~_t84 | _t83 | ~_t82 [ LRES, 118421, 3984, ~_t27 ] [ Backward Subsumption, 118425 ] % 18.16/18.33 (87,1) [118425,9]. true => ~_t182 | ~_t125 | ~_t84 | _t83 [ LRES, 118422, 91176, ~_t82 ] % 18.16/18.33 (87,1) [118439,9]. true => ~_t226 | ~_t225 | ~_t182 | ~_t175 | ~_t125 | ~_t84 [ LRES, 118425, 73987, _t83 ] % 18.16/18.33 (87,1) [118546,9]. true => ~_t226 | ~_t225 | ~_t195 | ~_t182 | ~_t175 | ~_t125 [ LRES, 118439, 2833, ~_t84 ] % 18.26/18.41 (87,1) [118548,9]. true => ~_t226 | ~_t225 | ~_t206 | ~_t195 | ~_t182 | ~_t175 [ LRES, 118546, 2855, ~_t125 ] [ Backward Subsumption, 118611 ] % 18.26/18.41 (87,1) [118611,9]. true => ~_t226 | ~_t225 | ~_t206 | ~_t195 | ~_t182 [ LRES, 118548, 12076, ~_t175 ] % 18.26/18.41 (1,1) [14,10]. true => ~_t22 | ~p110 | p109 [ SNF ] % 18.26/18.41 (1,1) [15,10]. true => _t22 | ~_t21 [ SNF ] % 18.26/18.41 (1,1) [16,10]. true => ~_t23 | ~p109 | p108 [ SNF ] % 18.26/18.41 (1,1) [17,10]. true => _t23 | ~_t21 [ SNF ] % 18.26/18.41 (1,1) [18,10]. true => ~_t24 | ~p108 | p107 [ SNF ] % 18.26/18.41 (1,1) [19,10]. true => _t24 | ~_t21 [ SNF ] % 18.26/18.41 (1,1) [20,10]. true => ~_t25 | ~p107 | p106 [ SNF ] % 18.26/18.41 (1,1) [21,10]. true => _t25 | ~_t21 [ SNF ] % 18.26/18.41 (1,1) [22,10]. true => ~_t26 | ~p106 | p105 [ SNF ] % 18.26/18.41 (1,1) [23,10]. true => _t26 | ~_t21 [ SNF ] % 18.26/18.41 (1,1) [24,10]. true => ~_t27 | ~p105 | p104 [ SNF ] % 18.26/18.41 (1,1) [25,10]. true => _t27 | ~_t21 [ SNF ] % 18.26/18.41 (1,1) [332,10]. true => ~_t84 | ~p4 | ~p104 [ SNF ] % 18.26/18.41 (43,1) [476,10]. true => ~_t179 | p110 [ SNF ] % 18.26/18.41 (1,1) [2715,10]. true => ~_t181 | p4 [ SNF++, 4 ] % 18.26/18.41 (1,1) [2717,10]. true => ~_t182 | _t21 [ SNF++, 242 ] % 18.26/18.41 (1,1) [2743,10]. true => ~_t195 | _t84 [ SNF++, 333 ] % 18.26/18.41 (43,1) [2801,10]. true => ~_t224 | _t179 [ SNF++, 477 ] % 18.26/18.41 (1,1) [3971,10]. true => ~_t182 | _t27 [ LRES, 25, 2717, ~_t21 ] % 18.26/18.41 (1,1) [3982,10]. true => ~_t182 | _t26 [ LRES, 23, 2717, ~_t21 ] % 18.26/18.41 (1,1) [3993,10]. true => ~_t182 | _t25 [ LRES, 21, 2717, ~_t21 ] % 18.26/18.41 (1,1) [4004,10]. true => ~_t182 | _t24 [ LRES, 19, 2717, ~_t21 ] % 18.26/18.41 (1,1) [4015,10]. true => ~_t182 | _t23 [ LRES, 17, 2717, ~_t21 ] % 18.26/18.41 (1,1) [4026,10]. true => ~_t182 | _t22 [ LRES, 15, 2717, ~_t21 ] % 18.26/18.41 (1,1) [7275,10]. true => ~_t84 | ~_t27 | ~p4 | ~p105 [ LRES, 332, 24, ~p104 ] % 18.26/18.41 (1,1) [10810,10]. true => ~_t84 | ~_t27 | ~_t26 | ~p4 | ~p106 [ LRES, 7275, 22, ~p105 ] % 18.26/18.41 (1,1) [19119,10]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~p4 | ~p107 [ LRES, 10810, 20, ~p106 ] % 18.26/18.41 (1,1) [35780,10]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~p4 | ~p108 [ LRES, 19119, 18, ~p107 ] % 18.26/18.41 (1,1) [41905,10]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 | ~p4 | ~p109 [ LRES, 35780, 16, ~p108 ] % 18.26/18.41 (1,1) [54370,10]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 | ~_t22 | ~p4 | ~p110 [ LRES, 41905, 14, ~p109 ] % 18.26/18.41 (43,1) [65721,10]. true => ~_t179 | ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 | ~_t22 | ~p4 [ LRES, 54370, 476, ~p110 ] % 18.26/18.41 (43,1) [73525,10]. true => ~_t181 | ~_t179 | ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 | ~_t22 [ LRES, 65721, 2715, ~p4 ] % 18.26/18.41 (43,1) [73917,10]. true => ~_t182 | ~_t181 | ~_t179 | ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 [ LRES, 73525, 4026, ~_t22 ] [ Backward Subsumption, 73939 ] % 18.26/18.41 (43,1) [73939,10]. true => ~_t182 | ~_t181 | ~_t179 | ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 [ LRES, 73917, 4015, ~_t23 ] [ Backward Subsumption, 73942 ] % 18.26/18.41 (43,1) [73942,10]. true => ~_t182 | ~_t181 | ~_t179 | ~_t84 | ~_t27 | ~_t26 | ~_t25 [ LRES, 73939, 4004, ~_t24 ] [ Backward Subsumption, 73945 ] % 18.26/18.41 (43,1) [73945,10]. true => ~_t182 | ~_t181 | ~_t179 | ~_t84 | ~_t27 | ~_t26 [ LRES, 73942, 3993, ~_t25 ] [ Backward Subsumption, 73948 ] % 18.26/18.41 (43,1) [73948,10]. true => ~_t182 | ~_t181 | ~_t179 | ~_t84 | ~_t27 [ LRES, 73945, 3982, ~_t26 ] [ Backward Subsumption, 73962 ] % 18.26/18.41 (43,1) [73962,10]. true => ~_t182 | ~_t181 | ~_t179 | ~_t84 [ LRES, 73948, 3971, ~_t27 ] % 18.26/18.41 (43,1) [73968,10]. true => ~_t195 | ~_t182 | ~_t181 | ~_t179 [ LRES, 73962, 2743, ~_t84 ] % 18.26/18.41 (43,1) [73970,10]. true => ~_t224 | ~_t195 | ~_t182 | ~_t181 [ LRES, 73968, 2801, ~_t179 ] % 18.26/18.41 % SZS output end Refutation % 18.26/18.42 % KSP exiting %------------------------------------------------------------------------------