%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP081_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 5 07:12:58 PM UTC 2026 % Result : Theorem 38.51s 38.79s % Output : Refutation 39.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : SYP081_1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.14 % Command : run_ksp %s % 0.15/0.35 % Computer : n020.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Mon May 4 17:19:49 EDT 2026 % 0.15/0.35 % CPUTime : % 0.47/0.65 ----KSP format--- % 0.47/0.65 set(box,SER). % 0.47/0.65 usable(formulas). % 0.47/0.65 true. % 0.47/0.65 end_of_list. % 0.47/0.65 sos(formulas). % 0.47/0.65 ~ (~ ( p100 & ~ ( p101 ) & ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) & [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) & [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) & [] ( [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( [] ( [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) ) ) ) ) ) ) ) & [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( ( p101 -> p100 ) & ( p102 -> p101 ) & ( p103 -> p102 ) & ( p104 -> p103 ) & ( p105 -> p104 ) & ( p106 -> p105 ) & ( p107 -> p106 ) & ( p108 -> p107 ) & ( p109 -> p108 ) & ( p110 -> p109 ) & ( p111 -> p110 ) & ( p100 -> ( ( p0 -> [] ( ( p100 -> p0 ) ) ) & ( ~ ( p0 ) -> [] ( ( p100 -> ~ ( p0 ) ) ) ) ) ) & ( p101 -> ( ( p1 -> [] ( ( p101 -> p1 ) ) ) & ( ~ ( p1 ) -> [] ( ( p101 -> ~ ( p1 ) ) ) ) ) ) & ( p102 -> ( ( p2 -> [] ( ( p102 -> p2 ) ) ) & ( ~ ( p2 ) -> [] ( ( p102 -> ~ ( p2 ) ) ) ) ) ) & ( p103 -> ( ( p3 -> [] ( ( p103 -> p3 ) ) ) & ( ~ ( p3 ) -> [] ( ( p103 -> ~ ( p3 ) ) ) ) ) ) & ( p104 -> ( ( p4 -> [] ( ( p104 -> p4 ) ) ) & ( ~ ( p4 ) -> [] ( ( p104 -> ~ ( p4 ) ) ) ) ) ) & ( p105 -> ( ( p5 -> [] ( ( p105 -> p5 ) ) ) & ( ~ ( p5 ) -> [] ( ( p105 -> ~ ( p5 ) ) ) ) ) ) & ( p106 -> ( ( p6 -> [] ( ( p106 -> p6 ) ) ) & ( ~ ( p6 ) -> [] ( ( p106 -> ~ ( p6 ) ) ) ) ) ) & ( p107 -> ( ( p7 -> [] ( ( p107 -> p7 ) ) ) & ( ~ ( p7 ) -> [] ( ( p107 -> ~ ( p7 ) ) ) ) ) ) & ( p108 -> ( ( p8 -> [] ( ( p108 -> p8 ) ) ) & ( ~ ( p8 ) -> [] ( ( p108 -> ~ ( p8 ) ) ) ) ) ) & ( p109 -> ( ( p9 -> [] ( ( p109 -> p9 ) ) ) & ( ~ ( p9 ) -> [] ( ( p109 -> ~ ( p9 ) ) ) ) ) ) & ( p110 -> ( ( p10 -> [] ( ( p110 -> p10 ) ) ) & ( ~ ( p10 ) -> [] ( ( p110 -> ~ ( p10 ) ) ) ) ) ) & ( ( p100 & ~ ( p101 ) ) -> ( <> ( p101 & ~ ( p102 ) & p1 ) & <> ( p101 & ~ ( p102 ) & ~ ( p1 ) ) ) ) & ( ( p101 & ~ ( p102 ) ) -> ( <> ( p102 & ~ ( p103 ) & p2 ) & <> ( p102 & ~ ( p103 ) & ~ ( p2 ) ) ) ) & ( ( p102 & ~ ( p103 ) ) -> ( <> ( p103 & ~ ( p104 ) & p3 ) & <> ( p103 & ~ ( p104 ) & ~ ( p3 ) ) ) ) & ( ( p103 & ~ ( p104 ) ) -> ( <> ( p104 & ~ ( p105 ) & p4 ) & <> ( p104 & ~ ( p105 ) & ~ ( p4 ) ) ) ) & ( ( p104 & ~ ( p105 ) ) -> ( <> ( p105 & ~ ( p106 ) & p5 ) & <> ( p105 & ~ ( p106 ) & ~ ( p5 ) ) ) ) & ( ( p105 & ~ ( p106 ) ) -> ( <> ( p106 & ~ ( p107 ) & p6 ) & <> ( p106 & ~ ( p107 ) & ~ ( p6 ) ) ) ) & ( ( p106 & ~ ( p107 ) ) -> ( <> ( p107 & ~ ( p108 ) & p7 ) & <> ( p107 & ~ ( p108 ) & ~ ( p7 ) ) ) ) & ( ( p107 & ~ ( p108 ) ) -> ( <> ( p108 & ~ ( p109 ) & p8 ) & <> ( p108 & ~ ( p109 ) & ~ ( p8 ) ) ) ) & ( ( p108 & ~ ( p109 ) ) -> ( <> ( p109 & ~ ( p110 ) & p9 ) & <> ( p109 & ~ ( p110 ) & ~ ( p9 ) ) ) ) & ( ( p109 & ~ ( p110 ) ) -> ( <> ( p110 & ~ ( p111 ) & p10 ) & <> ( p110 & ~ ( p111 ) & ~ ( p10 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( p4 ) ) ) ) ) ) ) ) ) ) ) ). % 0.47/0.65 end_of_list. % 0.47/0.65 ----------------- % 0.47/0.65 ksp -tstp -pproof -early_ple -mlple -ord -snf++ -unit -lhs_unit -fsub -bsub -limited_reuse_renaming -bnfsimp -maxproof 1 -populate_max_lit_positive -short -global2local -i /export/starexec/sandbox2/tmp/tmp.29XClQqSAJ/theBenchmark.ksp % 38.51/38.79 % 38.51/38.79 % SZS status Theorem % 38.51/38.79 % 38.51/38.79 ***************** % 38.51/38.79 FOUND PROOF 1 % 38.51/38.79 ***************** % 38.51/38.79 % SZS output start Refutation % 38.51/38.79 % 38.51/38.79 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 38.51/38.79 (1,1) [4,0]. true => ~_t0 | ~p101 [ SNF ] [ Backward Subsumption, 3164 ] % 38.51/38.79 (1,1) [5,0]. true => ~_t0 | p100 [ SNF ] [ Backward Subsumption, 3163 ] % 38.51/38.79 (1,1) [24,0]. _t1 => box 1 _t2 [ SNF ] [ Backward Subsumption, 3166 ] % 38.51/38.79 (1,1) [26,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 3162 ] % 38.51/38.79 (1,1) [315,0]. _t11 => box 1 _t12 [ SNF ] [ Backward Subsumption, 3221 ] % 38.51/38.79 (1,1) [317,0]. true => _t11 | ~_t0 [ SNF ] [ Backward Subsumption, 3161 ] % 38.51/38.79 (1,1) [604,0]. _t12 => box 1 _t13 [ SNF ] [ Backward Subsumption, 3168 ] % 38.51/38.79 (1,1) [606,0]. true => _t12 | ~_t0 [ SNF ] [ Backward Subsumption, 3160 ] % 38.51/38.79 (1,1) [891,0]. _t13 => box 1 _t14 [ SNF ] [ Backward Subsumption, 3219 ] % 38.51/38.79 (1,1) [893,0]. true => _t13 | ~_t0 [ SNF ] [ Backward Subsumption, 3159 ] % 38.51/38.79 (1,1) [1176,0]. _t14 => box 1 _t15 [ SNF ] [ Backward Subsumption, 3170 ] % 38.51/38.79 (1,1) [1178,0]. true => _t14 | ~_t0 [ SNF ] [ Backward Subsumption, 3158 ] % 38.51/38.79 (1,1) [1459,0]. _t15 => box 1 _t16 [ SNF ] [ Backward Subsumption, 3217 ] % 38.51/38.79 (1,1) [1461,0]. true => _t15 | ~_t0 [ SNF ] [ Backward Subsumption, 3157 ] % 38.51/38.79 (1,1) [1740,0]. _t16 => box 1 _t17 [ SNF ] [ Backward Subsumption, 3172 ] % 38.51/38.79 (1,1) [1742,0]. true => _t16 | ~_t0 [ SNF ] [ Backward Subsumption, 3156 ] % 38.51/38.79 (1,1) [2019,0]. _t17 => box 1 _t18 [ SNF ] [ Backward Subsumption, 3215 ] % 38.51/38.79 (1,1) [2021,0]. true => _t17 | ~_t0 [ SNF ] [ Backward Subsumption, 3155 ] % 38.51/38.79 (1,1) [2296,0]. _t18 => box 1 _t19 [ SNF ] [ Backward Subsumption, 3174 ] % 38.51/38.79 (1,1) [2298,0]. true => _t18 | ~_t0 [ SNF ] [ Backward Subsumption, 3154 ] % 38.51/38.79 (1,1) [2571,0]. _t19 => box 1 _t20 [ SNF ] [ Backward Subsumption, 3213 ] % 38.51/38.79 (1,1) [2573,0]. true => _t19 | ~_t0 [ SNF ] [ Backward Subsumption, 3153 ] % 38.51/38.79 (1,1) [2844,0]. _t20 => box 1 _t21 [ SNF ] [ Backward Subsumption, 3176 ] % 38.51/38.79 (1,1) [2846,0]. true => _t20 | ~_t0 [ SNF ] [ Backward Subsumption, 3152 ] % 38.51/38.79 (439,1) [3103,0]. _t172 => ~box 1~ _t173 [ SNF ] [ Backward Subsumption, 3243 ] % 38.51/38.79 (1,1) [3104,0]. true => _t172 | ~_t169 [ SNF ] [ Backward Subsumption, 3231 ] % 38.51/38.79 (1,1) [3105,0]. true => _t169 | ~_t168 | p101 | ~p100 [ SNF ] [ Backward Subsumption, 3191 ] % 38.51/38.79 (1,1) [3106,0]. true => _t168 | ~_t0 [ SNF ] [ Backward Subsumption, 3122 ] % 38.51/38.79 (1,1) [3122,0]. true => _t168 [ Unit Resolution, 3, 3106, _t0 ] [ Modal Level Pure Literal Elimination, _t168 ] % 38.51/38.79 (1,1) [3152,0]. true => _t20 [ Unit Resolution, 3, 2846, _t0 ] [ Modal Level Pure Literal Elimination, _t20 ] % 38.51/38.79 (1,1) [3153,0]. true => _t19 [ Unit Resolution, 3, 2573, _t0 ] [ Modal Level Pure Literal Elimination, _t19 ] % 38.51/38.79 (1,1) [3154,0]. true => _t18 [ Unit Resolution, 3, 2298, _t0 ] [ Modal Level Pure Literal Elimination, _t18 ] % 38.51/38.79 (1,1) [3155,0]. true => _t17 [ Unit Resolution, 3, 2021, _t0 ] [ Modal Level Pure Literal Elimination, _t17 ] % 38.51/38.79 (1,1) [3156,0]. true => _t16 [ Unit Resolution, 3, 1742, _t0 ] [ Modal Level Pure Literal Elimination, _t16 ] % 38.51/38.79 (1,1) [3157,0]. true => _t15 [ Unit Resolution, 3, 1461, _t0 ] [ Modal Level Pure Literal Elimination, _t15 ] % 38.51/38.79 (1,1) [3158,0]. true => _t14 [ Unit Resolution, 3, 1178, _t0 ] [ Modal Level Pure Literal Elimination, _t14 ] % 38.51/38.79 (1,1) [3159,0]. true => _t13 [ Unit Resolution, 3, 893, _t0 ] [ Modal Level Pure Literal Elimination, _t13 ] % 38.51/38.79 (1,1) [3160,0]. true => _t12 [ Unit Resolution, 3, 606, _t0 ] [ Modal Level Pure Literal Elimination, _t12 ] % 38.51/38.79 (1,1) [3161,0]. true => _t11 [ Unit Resolution, 3, 317, _t0 ] [ Modal Level Pure Literal Elimination, _t11 ] % 38.51/38.79 (1,1) [3162,0]. true => _t1 [ Unit Resolution, 3, 26, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 38.51/38.79 (1,1) [3163,0]. true => p100 [ Unit Resolution, 3, 5, _t0 ] [ Modal Level Pure Literal Elimination, p100 ] % 38.51/38.79 (1,1) [3164,0]. true => ~p101 [ Unit Resolution, 3, 4, _t0 ] [ Modal Level Pure Literal Elimination, ~p101 ] % 38.51/38.79 (1,1) [3166,0]. true => box 1 _t2 [ LHS Unit Resolution, 3162, 24, _t1 ] [ SNF++, 4664, _t2 ] % 38.51/38.79 (1,1) [3168,0]. true => box 1 _t13 [ LHS Unit Resolution, 3160, 604, _t12 ] [ SNF++, 4668, _t13 ] % 38.51/38.79 (1,1) [3170,0]. true => box 1 _t15 [ LHS Unit Resolution, 3158, 1176, _t14 ] [ SNF++, 4672, _t15 ] % 38.51/38.79 (1,1) [3172,0]. true => box 1 _t17 [ LHS Unit Resolution, 3156, 1740, _t16 ] [ SNF++, 4676, _t17 ] % 38.51/38.79 (1,1) [3174,0]. true => box 1 _t19 [ LHS Unit Resolution, 3154, 2296, _t18 ] [ SNF++, 4680, _t19 ] % 38.51/38.79 (1,1) [3176,0]. true => box 1 _t21 [ LHS Unit Resolution, 3152, 2844, _t20 ] [ SNF++, 4684, _t21 ] % 38.51/38.79 (1,1) [3191,0]. true => _t169 | p101 | ~p100 [ Unit Resolution, 3122, 3105, _t168 ] [ Backward Subsumption, 3192 ] % 38.51/38.79 (1,1) [3192,0]. true => _t169 | p101 [ Unit Resolution, 3163, 3191, p100 ] [ Backward Subsumption, 3194 ] % 38.51/38.79 (1,1) [3194,0]. true => _t169 [ Unit Resolution, 3164, 3192, p101 ] [ Modal Level Pure Literal Elimination, _t169 ] % 38.51/38.79 (1,1) [3213,0]. true => box 1 _t20 [ LHS Unit Resolution, 3153, 2571, _t19 ] [ SNF++, 4682, _t20 ] % 38.51/38.79 (1,1) [3215,0]. true => box 1 _t18 [ LHS Unit Resolution, 3155, 2019, _t17 ] [ SNF++, 4678, _t18 ] % 38.51/38.79 (1,1) [3217,0]. true => box 1 _t16 [ LHS Unit Resolution, 3157, 1459, _t15 ] [ SNF++, 4674, _t16 ] % 38.51/38.79 (1,1) [3219,0]. true => box 1 _t14 [ LHS Unit Resolution, 3159, 891, _t13 ] [ SNF++, 4670, _t14 ] % 38.51/38.79 (1,1) [3221,0]. true => box 1 _t12 [ LHS Unit Resolution, 3161, 315, _t11 ] [ SNF++, 4666, _t12 ] % 38.51/38.79 (1,1) [3231,0]. true => _t172 [ Unit Resolution, 3194, 3104, _t169 ] [ Modal Level Pure Literal Elimination, _t172 ] % 38.51/38.79 (439,1) [3243,0]. true => ~box 1~ _t173 [ LHS Unit Resolution, 3231, 3103, _t172 ] [ SNF++, 4718, _t173 ] % 38.51/38.79 (1,1) [4664,0]. true => box 1 _t283 [ SNF++, 3166 ] % 38.51/38.79 (1,1) [4666,0]. true => box 1 _t284 [ SNF++, 3221 ] % 38.51/38.79 (1,1) [4668,0]. true => box 1 _t282 [ SNF++, 3168 ] % 38.51/38.79 (1,1) [4670,0]. true => box 1 _t280 [ SNF++, 3219 ] % 38.51/38.79 (1,1) [4672,0]. true => box 1 _t278 [ SNF++, 3170 ] % 38.51/38.79 (1,1) [4674,0]. true => box 1 _t276 [ SNF++, 3217 ] % 38.51/38.79 (1,1) [4676,0]. true => box 1 _t274 [ SNF++, 3172 ] % 38.51/38.79 (1,1) [4678,0]. true => box 1 _t272 [ SNF++, 3215 ] % 38.51/38.79 (1,1) [4680,0]. true => box 1 _t270 [ SNF++, 3174 ] % 38.51/38.79 (1,1) [4682,0]. true => box 1 _t268 [ SNF++, 3213 ] % 38.51/38.79 (1,1) [4684,0]. true => box 1 _t224 [ SNF++, 3176 ] % 38.51/38.79 (439,1) [4718,0]. true => ~box 1~ _t264 [ SNF++, 3243 ] % 38.51/38.79 (439,1) [376304,0]. true => false [ GEN1, 4666, 4668, 4672, 4676, 4680, 4684, 4682, 4678, 4674, 4670, 4664, 4718, 376300, _t284, _t282, _t278, _t274, _t270, _t224, _t268, _t272, _t276, _t280, _t283, _t264 ] % 38.51/38.79 (1,1) [22,1]. _t2 => box 1 _t3 [ SNF ] [ SNF++, 4496, _t3 ] % 38.51/38.79 (1,1) [313,1]. _t12 => box 1 _t13 [ SNF ] [ SNF++, 4498, _t13 ] % 38.51/38.79 (1,1) [602,1]. _t13 => box 1 _t14 [ SNF ] [ SNF++, 4500, _t14 ] % 38.51/38.79 (1,1) [889,1]. _t14 => box 1 _t15 [ SNF ] [ SNF++, 4502, _t15 ] % 38.51/38.79 (1,1) [1174,1]. _t15 => box 1 _t16 [ SNF ] [ SNF++, 4504, _t16 ] % 38.51/38.79 (1,1) [1457,1]. _t16 => box 1 _t17 [ SNF ] [ SNF++, 4506, _t17 ] % 38.51/38.79 (1,1) [1738,1]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 4508, _t18 ] % 38.51/38.79 (1,1) [2017,1]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 4510, _t19 ] % 38.51/38.79 (1,1) [2294,1]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 4512, _t20 ] % 38.51/38.79 (1,1) [2569,1]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 4514, _t21 ] % 38.51/38.79 (395,1) [2818,1]. _t166 => ~box 1~ _t167 [ SNF ] [ SNF++, 4654, _t167 ] % 38.51/38.79 (1,1) [2819,1]. true => _t166 | ~_t163 [ SNF ] % 38.51/38.79 (1,1) [2820,1]. true => _t163 | ~_t162 | p102 | ~p101 [ SNF ] % 38.51/38.79 (1,1) [2821,1]. true => _t162 | ~_t21 [ SNF ] % 38.51/38.79 (439,1) [3101,1]. true => ~_t173 | ~p102 [ SNF ] % 38.51/38.79 (439,1) [3102,1]. true => ~_t173 | p101 [ SNF ] % 38.51/38.79 (1,1) [4496,1]. _t2 => box 1 _t281 [ SNF++, 22 ] % 38.51/38.79 (1,1) [4498,1]. _t12 => box 1 _t282 [ SNF++, 313 ] % 38.51/38.79 (1,1) [4500,1]. _t13 => box 1 _t280 [ SNF++, 602 ] % 38.51/38.79 (1,1) [4502,1]. _t14 => box 1 _t278 [ SNF++, 889 ] % 38.51/38.79 (1,1) [4504,1]. _t15 => box 1 _t276 [ SNF++, 1174 ] % 38.51/38.79 (1,1) [4506,1]. _t16 => box 1 _t274 [ SNF++, 1457 ] % 38.51/38.79 (1,1) [4508,1]. _t17 => box 1 _t272 [ SNF++, 1738 ] % 38.51/38.79 (1,1) [4510,1]. _t18 => box 1 _t270 [ SNF++, 2017 ] % 38.51/38.79 (1,1) [4512,1]. _t19 => box 1 _t268 [ SNF++, 2294 ] % 38.51/38.79 (1,1) [4514,1]. _t20 => box 1 _t224 [ SNF++, 2569 ] % 38.51/38.79 (395,1) [4654,1]. _t166 => ~box 1~ _t262 [ SNF++, 2818 ] % 38.51/38.79 (1,1) [4665,1]. true => ~_t283 | _t2 [ SNF++, 3166 ] % 38.51/38.79 (1,1) [4667,1]. true => ~_t284 | _t12 [ SNF++, 3221 ] % 38.51/38.79 (1,1) [4669,1]. true => ~_t282 | _t13 [ SNF++, 3168 ] % 38.51/38.79 (1,1) [4671,1]. true => ~_t280 | _t14 [ SNF++, 3219 ] % 38.51/38.79 (1,1) [4673,1]. true => ~_t278 | _t15 [ SNF++, 3170 ] % 38.51/38.79 (1,1) [4675,1]. true => ~_t276 | _t16 [ SNF++, 3217 ] % 38.51/38.79 (1,1) [4677,1]. true => ~_t274 | _t17 [ SNF++, 3172 ] % 38.51/38.79 (1,1) [4679,1]. true => ~_t272 | _t18 [ SNF++, 3215 ] % 38.51/38.79 (1,1) [4681,1]. true => ~_t270 | _t19 [ SNF++, 3174 ] % 38.51/38.79 (1,1) [4683,1]. true => ~_t268 | _t20 [ SNF++, 3213 ] % 38.51/38.79 (1,1) [4685,1]. true => ~_t224 | _t21 [ SNF++, 3176 ] % 38.51/38.79 (439,1) [4719,1]. true => ~_t264 | _t173 [ SNF++, 3243 ] % 38.51/38.79 (1,1) [4876,1]. true => ~_t224 | _t162 [ LRES, 2821, 4685, ~_t21 ] % 38.51/38.79 (439,1) [6361,1]. true => ~_t173 | _t163 | ~_t162 | p102 [ LRES, 2820, 3102, ~p101 ] [ Backward Subsumption, 6610 ] % 38.51/38.79 (439,1) [6610,1]. true => ~_t173 | _t163 | ~_t162 [ LRES, 6361, 3101, p102 ] % 38.51/38.79 (439,1) [6624,1]. true => ~_t224 | ~_t173 | _t163 [ LRES, 6610, 4876, ~_t162 ] % 38.51/38.79 (439,1) [6636,1]. true => ~_t224 | ~_t173 | _t166 [ LRES, 6624, 2819, _t163 ] % 38.51/38.79 (395,1) [375481,1]. true => ~_t166 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 | ~_t13 | ~_t12 | ~_t2 [ GEN1, 4498, 4500, 4504, 4508, 4512, 4514, 4510, 4506, 4502, 4496, 4654, 369109, _t282, _t280, _t276, _t272, _t268, _t224, _t270, _t274, _t278, _t281, _t262 ] % 38.51/38.79 (395,1) [375497,1]. true => ~_t283 | ~_t166 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 | ~_t13 | ~_t12 [ LRES, 375481, 4665, ~_t2 ] % 38.51/38.79 (395,1) [375501,1]. true => ~_t284 | ~_t283 | ~_t166 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 | ~_t13 [ LRES, 375497, 4667, ~_t12 ] % 38.51/38.79 (395,1) [375595,1]. true => ~_t284 | ~_t283 | ~_t282 | ~_t166 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 [ LRES, 375501, 4669, ~_t13 ] % 38.51/38.79 (395,1) [375899,1]. true => ~_t284 | ~_t283 | ~_t282 | ~_t280 | ~_t166 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 [ LRES, 375595, 4671, ~_t14 ] % 38.51/38.79 (395,1) [376173,1]. true => ~_t284 | ~_t283 | ~_t282 | ~_t280 | ~_t278 | ~_t166 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 [ LRES, 375899, 4673, ~_t15 ] % 38.51/38.79 (395,1) [376176,1]. true => ~_t284 | ~_t283 | ~_t282 | ~_t280 | ~_t278 | ~_t276 | ~_t166 | ~_t20 | ~_t19 | ~_t18 | ~_t17 [ LRES, 376173, 4675, ~_t16 ] % 38.51/38.79 (395,1) [376227,1]. true => ~_t284 | ~_t283 | ~_t282 | ~_t280 | ~_t278 | ~_t276 | ~_t274 | ~_t166 | ~_t20 | ~_t19 | ~_t18 [ LRES, 376176, 4677, ~_t17 ] % 38.51/38.79 (395,1) [376260,1]. true => ~_t284 | ~_t283 | ~_t282 | ~_t280 | ~_t278 | ~_t276 | ~_t274 | ~_t272 | ~_t166 | ~_t20 | ~_t19 [ LRES, 376227, 4679, ~_t18 ] % 38.51/38.79 (395,1) [376279,1]. true => ~_t284 | ~_t283 | ~_t282 | ~_t280 | ~_t278 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t166 | ~_t20 [ LRES, 376260, 4681, ~_t19 ] % 38.51/38.79 (395,1) [376281,1]. true => ~_t284 | ~_t283 | ~_t282 | ~_t280 | ~_t278 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t166 [ LRES, 376279, 4683, ~_t20 ] % 38.51/38.79 (439,1) [376290,1]. true => ~_t284 | ~_t283 | ~_t282 | ~_t280 | ~_t278 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t224 | ~_t173 [ LRES, 376281, 6636, ~_t166 ] % 38.51/38.79 (439,1) [376300,1]. true => ~_t284 | ~_t283 | ~_t282 | ~_t280 | ~_t278 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t264 | ~_t224 [ LRES, 376290, 4719, ~_t173 ] % 38.51/38.79 (1,1) [20,2]. _t3 => box 1 _t4 [ SNF ] [ SNF++, 4332, _t4 ] % 38.51/38.79 (1,1) [311,2]. _t13 => box 1 _t14 [ SNF ] [ SNF++, 4334, _t14 ] % 38.51/38.79 (1,1) [600,2]. _t14 => box 1 _t15 [ SNF ] [ SNF++, 4336, _t15 ] % 38.51/38.79 (1,1) [887,2]. _t15 => box 1 _t16 [ SNF ] [ SNF++, 4338, _t16 ] % 38.51/38.79 (1,1) [1172,2]. _t16 => box 1 _t17 [ SNF ] [ SNF++, 4340, _t17 ] % 38.51/38.79 (1,1) [1455,2]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 4342, _t18 ] % 38.51/38.79 (1,1) [1736,2]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 4344, _t19 ] % 38.51/38.79 (1,1) [2015,2]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 4346, _t20 ] % 38.51/38.79 (1,1) [2292,2]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 4348, _t21 ] % 38.51/38.79 (353,1) [2526,2]. _t158 => ~box 1~ _t159 [ SNF ] [ SNF++, 4480, _t159 ] % 38.51/38.79 (1,1) [2527,2]. true => _t158 | ~_t157 [ SNF ] % 38.51/38.79 (1,1) [2533,2]. true => _t157 | ~_t156 | p103 | ~p102 [ SNF ] % 38.51/38.79 (1,1) [2534,2]. true => _t156 | ~_t21 [ SNF ] % 38.51/38.79 (395,1) [2816,2]. true => ~_t167 | ~p103 [ SNF ] % 38.51/38.79 (395,1) [2817,2]. true => ~_t167 | p102 [ SNF ] % 38.51/38.79 (1,1) [4332,2]. _t3 => box 1 _t279 [ SNF++, 20 ] % 38.51/38.79 (1,1) [4334,2]. _t13 => box 1 _t280 [ SNF++, 311 ] % 38.51/38.79 (1,1) [4336,2]. _t14 => box 1 _t278 [ SNF++, 600 ] % 38.51/38.79 (1,1) [4338,2]. _t15 => box 1 _t276 [ SNF++, 887 ] % 38.51/38.79 (1,1) [4340,2]. _t16 => box 1 _t274 [ SNF++, 1172 ] % 38.51/38.79 (1,1) [4342,2]. _t17 => box 1 _t272 [ SNF++, 1455 ] % 38.51/38.79 (1,1) [4344,2]. _t18 => box 1 _t270 [ SNF++, 1736 ] % 38.51/38.79 (1,1) [4346,2]. _t19 => box 1 _t268 [ SNF++, 2015 ] % 38.51/38.79 (1,1) [4348,2]. _t20 => box 1 _t224 [ SNF++, 2292 ] % 38.51/38.79 (353,1) [4480,2]. _t158 => ~box 1~ _t259 [ SNF++, 2526 ] % 38.51/38.79 (1,1) [4497,2]. true => ~_t281 | _t3 [ SNF++, 22 ] % 38.51/38.79 (1,1) [4499,2]. true => ~_t282 | _t13 [ SNF++, 313 ] % 38.51/38.79 (1,1) [4501,2]. true => ~_t280 | _t14 [ SNF++, 602 ] % 38.51/38.79 (1,1) [4503,2]. true => ~_t278 | _t15 [ SNF++, 889 ] % 38.51/38.79 (1,1) [4505,2]. true => ~_t276 | _t16 [ SNF++, 1174 ] % 38.51/38.79 (1,1) [4507,2]. true => ~_t274 | _t17 [ SNF++, 1457 ] % 38.51/38.79 (1,1) [4509,2]. true => ~_t272 | _t18 [ SNF++, 1738 ] % 38.51/38.79 (1,1) [4511,2]. true => ~_t270 | _t19 [ SNF++, 2017 ] % 38.51/38.79 (1,1) [4513,2]. true => ~_t268 | _t20 [ SNF++, 2294 ] % 38.51/38.79 (1,1) [4515,2]. true => ~_t224 | _t21 [ SNF++, 2569 ] % 38.51/38.79 (395,1) [4655,2]. true => ~_t262 | _t167 [ SNF++, 2818 ] % 38.51/38.79 (1,1) [4887,2]. true => ~_t224 | _t156 [ LRES, 2534, 4515, ~_t21 ] % 38.51/38.79 (395,1) [12608,2]. true => ~_t167 | _t157 | ~_t156 | p103 [ LRES, 2533, 2817, ~p102 ] [ Backward Subsumption, 17184 ] % 38.51/38.79 (395,1) [17184,2]. true => ~_t167 | _t157 | ~_t156 [ LRES, 12608, 2816, p103 ] % 38.51/38.79 (395,1) [17201,2]. true => ~_t224 | ~_t167 | _t157 [ LRES, 17184, 4887, ~_t156 ] % 38.51/38.79 (395,1) [17218,2]. true => ~_t224 | ~_t167 | _t158 [ LRES, 17201, 2527, _t157 ] % 38.51/38.79 (353,1) [349887,2]. true => ~_t158 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 | ~_t13 | ~_t3 [ GEN1, 4334, 4336, 4340, 4344, 4348, 4346, 4342, 4338, 4332, 4480, 349881, _t280, _t278, _t274, _t270, _t224, _t268, _t272, _t276, _t279, _t259 ] % 38.51/38.79 (353,1) [351469,2]. true => ~_t281 | ~_t158 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 | ~_t13 [ LRES, 349887, 4497, ~_t3 ] % 38.51/38.79 (353,1) [351472,2]. true => ~_t282 | ~_t281 | ~_t158 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 [ LRES, 351469, 4499, ~_t13 ] % 38.51/38.79 (353,1) [351473,2]. true => ~_t282 | ~_t281 | ~_t280 | ~_t158 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 [ LRES, 351472, 4501, ~_t14 ] % 38.51/38.79 (353,1) [351476,2]. true => ~_t282 | ~_t281 | ~_t280 | ~_t278 | ~_t158 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 [ LRES, 351473, 4503, ~_t15 ] % 38.51/38.79 (353,1) [351478,2]. true => ~_t282 | ~_t281 | ~_t280 | ~_t278 | ~_t276 | ~_t158 | ~_t20 | ~_t19 | ~_t18 | ~_t17 [ LRES, 351476, 4505, ~_t16 ] % 38.51/38.79 (353,1) [351481,2]. true => ~_t282 | ~_t281 | ~_t280 | ~_t278 | ~_t276 | ~_t274 | ~_t158 | ~_t20 | ~_t19 | ~_t18 [ LRES, 351478, 4507, ~_t17 ] % 38.51/38.79 (353,1) [351482,2]. true => ~_t282 | ~_t281 | ~_t280 | ~_t278 | ~_t276 | ~_t274 | ~_t272 | ~_t158 | ~_t20 | ~_t19 [ LRES, 351481, 4509, ~_t18 ] % 38.51/38.79 (353,1) [351485,2]. true => ~_t282 | ~_t281 | ~_t280 | ~_t278 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t158 | ~_t20 [ LRES, 351482, 4511, ~_t19 ] % 38.51/38.79 (353,1) [351486,2]. true => ~_t282 | ~_t281 | ~_t280 | ~_t278 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t158 [ LRES, 351485, 4513, ~_t20 ] % 38.51/38.79 (395,1) [351489,2]. true => ~_t282 | ~_t281 | ~_t280 | ~_t278 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t224 | ~_t167 [ LRES, 351486, 17218, ~_t158 ] % 38.51/38.79 (395,1) [369109,2]. true => ~_t282 | ~_t281 | ~_t280 | ~_t278 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t262 | ~_t224 [ LRES, 351489, 4655, ~_t167 ] % 38.51/38.79 (1,1) [18,3]. _t4 => box 1 _t5 [ SNF ] [ SNF++, 4172, _t5 ] % 38.51/38.79 (1,1) [309,3]. _t14 => box 1 _t15 [ SNF ] [ SNF++, 4174, _t15 ] % 38.51/38.79 (1,1) [598,3]. _t15 => box 1 _t16 [ SNF ] [ SNF++, 4176, _t16 ] % 38.51/38.79 (1,1) [885,3]. _t16 => box 1 _t17 [ SNF ] [ SNF++, 4178, _t17 ] % 38.51/38.79 (1,1) [1170,3]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 4180, _t18 ] % 38.51/38.79 (1,1) [1453,3]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 4182, _t19 ] % 38.51/38.79 (1,1) [1734,3]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 4184, _t20 ] % 38.51/38.79 (1,1) [2013,3]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 4186, _t21 ] % 38.51/38.79 (309,1) [2237,3]. _t152 => ~box 1~ _t153 [ SNF ] [ SNF++, 4312, _t153 ] % 38.51/38.79 (1,1) [2238,3]. true => _t152 | ~_t151 [ SNF ] % 38.51/38.79 (1,1) [2244,3]. true => _t151 | ~_t150 | p104 | ~p103 [ SNF ] % 38.51/38.79 (1,1) [2245,3]. true => _t150 | ~_t21 [ SNF ] % 38.51/38.79 (353,1) [2524,3]. true => ~_t159 | ~p104 [ SNF ] % 38.51/38.79 (353,1) [2525,3]. true => ~_t159 | p103 [ SNF ] % 38.51/38.79 (1,1) [4172,3]. _t4 => box 1 _t277 [ SNF++, 18 ] % 38.51/38.79 (1,1) [4174,3]. _t14 => box 1 _t278 [ SNF++, 309 ] % 38.51/38.79 (1,1) [4176,3]. _t15 => box 1 _t276 [ SNF++, 598 ] % 38.51/38.79 (1,1) [4178,3]. _t16 => box 1 _t274 [ SNF++, 885 ] % 38.51/38.79 (1,1) [4180,3]. _t17 => box 1 _t272 [ SNF++, 1170 ] % 38.51/38.79 (1,1) [4182,3]. _t18 => box 1 _t270 [ SNF++, 1453 ] % 38.51/38.79 (1,1) [4184,3]. _t19 => box 1 _t268 [ SNF++, 1734 ] % 38.51/38.79 (1,1) [4186,3]. _t20 => box 1 _t224 [ SNF++, 2013 ] % 38.51/38.79 (309,1) [4312,3]. _t152 => ~box 1~ _t257 [ SNF++, 2237 ] % 38.51/38.79 (1,1) [4333,3]. true => ~_t279 | _t4 [ SNF++, 20 ] % 38.51/38.79 (1,1) [4335,3]. true => ~_t280 | _t14 [ SNF++, 311 ] % 38.51/38.79 (1,1) [4337,3]. true => ~_t278 | _t15 [ SNF++, 600 ] % 38.51/38.79 (1,1) [4339,3]. true => ~_t276 | _t16 [ SNF++, 887 ] % 38.51/38.79 (1,1) [4341,3]. true => ~_t274 | _t17 [ SNF++, 1172 ] % 38.51/38.79 (1,1) [4343,3]. true => ~_t272 | _t18 [ SNF++, 1455 ] % 38.51/38.79 (1,1) [4345,3]. true => ~_t270 | _t19 [ SNF++, 1736 ] % 38.51/38.79 (1,1) [4347,3]. true => ~_t268 | _t20 [ SNF++, 2015 ] % 38.51/38.79 (1,1) [4349,3]. true => ~_t224 | _t21 [ SNF++, 2292 ] % 38.51/38.79 (353,1) [4481,3]. true => ~_t259 | _t159 [ SNF++, 2526 ] % 38.51/38.79 (1,1) [4898,3]. true => ~_t224 | _t150 [ LRES, 2245, 4349, ~_t21 ] % 38.51/38.79 (353,1) [12496,3]. true => ~_t159 | _t151 | ~_t150 | p104 [ LRES, 2244, 2525, ~p103 ] [ Backward Subsumption, 16930 ] % 38.51/38.79 (353,1) [16930,3]. true => ~_t159 | _t151 | ~_t150 [ LRES, 12496, 2524, p104 ] % 38.51/38.79 (353,1) [16964,3]. true => ~_t224 | ~_t159 | _t151 [ LRES, 16930, 4898, ~_t150 ] % 38.51/38.79 (353,1) [16977,3]. true => ~_t224 | ~_t159 | _t152 [ LRES, 16964, 2238, _t151 ] % 38.51/38.79 (309,1) [349499,3]. true => ~_t152 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 | ~_t4 [ GEN1, 4174, 4176, 4180, 4184, 4186, 4182, 4178, 4172, 4312, 349469, _t278, _t276, _t272, _t268, _t224, _t270, _t274, _t277, _t257 ] % 38.51/38.79 (309,1) [349862,3]. true => ~_t279 | ~_t152 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t14 [ LRES, 349499, 4333, ~_t4 ] % 38.51/38.79 (309,1) [349864,3]. true => ~_t280 | ~_t279 | ~_t152 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 [ LRES, 349862, 4335, ~_t14 ] % 38.51/38.79 (309,1) [349866,3]. true => ~_t280 | ~_t279 | ~_t278 | ~_t152 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 [ LRES, 349864, 4337, ~_t15 ] % 38.51/38.79 (309,1) [349868,3]. true => ~_t280 | ~_t279 | ~_t278 | ~_t276 | ~_t152 | ~_t20 | ~_t19 | ~_t18 | ~_t17 [ LRES, 349866, 4339, ~_t16 ] % 38.51/38.79 (309,1) [349870,3]. true => ~_t280 | ~_t279 | ~_t278 | ~_t276 | ~_t274 | ~_t152 | ~_t20 | ~_t19 | ~_t18 [ LRES, 349868, 4341, ~_t17 ] % 38.51/38.79 (309,1) [349872,3]. true => ~_t280 | ~_t279 | ~_t278 | ~_t276 | ~_t274 | ~_t272 | ~_t152 | ~_t20 | ~_t19 [ LRES, 349870, 4343, ~_t18 ] % 38.51/38.79 (309,1) [349874,3]. true => ~_t280 | ~_t279 | ~_t278 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t152 | ~_t20 [ LRES, 349872, 4345, ~_t19 ] % 38.51/38.79 (309,1) [349876,3]. true => ~_t280 | ~_t279 | ~_t278 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t152 [ LRES, 349874, 4347, ~_t20 ] % 38.51/38.79 (353,1) [349878,3]. true => ~_t280 | ~_t279 | ~_t278 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t224 | ~_t159 [ LRES, 349876, 16977, ~_t152 ] % 38.51/38.79 (353,1) [349881,3]. true => ~_t280 | ~_t279 | ~_t278 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t259 | ~_t224 [ LRES, 349878, 4481, ~_t159 ] % 38.51/38.79 (1,1) [16,4]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 4016, _t6 ] % 38.51/38.79 (1,1) [307,4]. _t15 => box 1 _t16 [ SNF ] [ SNF++, 4018, _t16 ] % 38.51/38.79 (1,1) [596,4]. _t16 => box 1 _t17 [ SNF ] [ SNF++, 4020, _t17 ] % 38.51/38.79 (1,1) [883,4]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 4022, _t18 ] % 38.51/38.79 (1,1) [1168,4]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 4024, _t19 ] % 38.51/38.79 (1,1) [1451,4]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 4026, _t20 ] % 38.51/38.79 (1,1) [1732,4]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 4028, _t21 ] % 38.51/38.79 (1,1) [1836,4]. _t83 => box 1 _t84 [ SNF ] [ SNF++, 4054, _t84 ] % 38.51/38.79 (1,1) [1838,4]. true => _t83 | ~_t82 | p4 [ SNF ] % 38.51/38.79 (1,1) [1839,4]. true => _t82 | ~_t81 [ SNF ] % 38.51/38.79 (1,1) [1845,4]. true => _t81 | ~_t80 | ~p104 [ SNF ] % 38.51/38.79 (1,1) [1846,4]. true => _t80 | ~_t21 [ SNF ] % 38.51/38.79 (263,1) [1951,4]. _t148 => ~box 1~ _t149 [ SNF ] [ SNF++, 4150, _t149 ] % 38.51/38.79 (1,1) [1952,4]. true => _t148 | ~_t145 [ SNF ] % 38.51/38.79 (1,1) [1953,4]. true => _t145 | ~_t144 | p105 | ~p104 [ SNF ] % 38.51/38.79 (1,1) [1954,4]. true => _t144 | ~_t21 [ SNF ] % 38.51/38.79 (309,1) [2234,4]. true => ~_t153 | ~p4 [ SNF ] % 38.51/38.79 (309,1) [2235,4]. true => ~_t153 | ~p105 [ SNF ] % 38.51/38.79 (309,1) [2236,4]. true => ~_t153 | p104 [ SNF ] % 38.51/38.79 (1,1) [4016,4]. _t5 => box 1 _t275 [ SNF++, 16 ] % 38.51/38.79 (1,1) [4018,4]. _t15 => box 1 _t276 [ SNF++, 307 ] % 38.51/38.79 (1,1) [4020,4]. _t16 => box 1 _t274 [ SNF++, 596 ] % 38.51/38.79 (1,1) [4022,4]. _t17 => box 1 _t272 [ SNF++, 883 ] % 38.51/38.79 (1,1) [4024,4]. _t18 => box 1 _t270 [ SNF++, 1168 ] % 38.51/38.79 (1,1) [4026,4]. _t19 => box 1 _t268 [ SNF++, 1451 ] % 38.51/38.79 (1,1) [4028,4]. _t20 => box 1 _t224 [ SNF++, 1732 ] % 38.51/38.79 (1,1) [4054,4]. _t83 => box 1 _t237 [ SNF++, 1836 ] % 38.51/38.79 (263,1) [4150,4]. _t148 => ~box 1~ _t256 [ SNF++, 1951 ] % 38.51/38.79 (1,1) [4173,4]. true => ~_t277 | _t5 [ SNF++, 18 ] % 38.51/38.79 (1,1) [4175,4]. true => ~_t278 | _t15 [ SNF++, 309 ] % 38.51/38.79 (1,1) [4177,4]. true => ~_t276 | _t16 [ SNF++, 598 ] % 38.51/38.79 (1,1) [4179,4]. true => ~_t274 | _t17 [ SNF++, 885 ] % 38.51/38.79 (1,1) [4181,4]. true => ~_t272 | _t18 [ SNF++, 1170 ] % 38.51/38.79 (1,1) [4183,4]. true => ~_t270 | _t19 [ SNF++, 1453 ] % 38.51/38.79 (1,1) [4185,4]. true => ~_t268 | _t20 [ SNF++, 1734 ] % 38.51/38.79 (1,1) [4187,4]. true => ~_t224 | _t21 [ SNF++, 2013 ] % 38.51/38.79 (309,1) [4313,4]. true => ~_t257 | _t153 [ SNF++, 2237 ] % 38.51/38.79 (1,1) [4909,4]. true => ~_t224 | _t144 [ LRES, 1954, 4187, ~_t21 ] % 38.51/38.79 (1,1) [5017,4]. true => ~_t224 | _t80 [ LRES, 1846, 4187, ~_t21 ] % 38.51/38.79 (309,1) [5664,4]. true => ~_t153 | _t83 | ~_t82 [ LRES, 2234, 1838, ~p4 ] % 38.51/38.79 (309,1) [8029,4]. true => ~_t153 | _t81 | ~_t80 [ LRES, 1845, 2236, ~p104 ] % 38.51/38.79 (309,1) [9495,4]. true => ~_t224 | ~_t153 | _t81 [ LRES, 8029, 5017, ~_t80 ] % 38.51/38.79 (309,1) [10488,4]. true => ~_t224 | ~_t153 | _t82 [ LRES, 9495, 1839, _t81 ] % 38.51/38.79 (309,1) [10996,4]. true => ~_t224 | ~_t153 | _t83 [ LRES, 10488, 5664, _t82 ] % 38.51/38.79 (309,1) [12385,4]. true => ~_t153 | _t145 | ~_t144 | p105 [ LRES, 1953, 2236, ~p104 ] [ Backward Subsumption, 16358 ] % 38.51/38.79 (309,1) [16358,4]. true => ~_t153 | _t145 | ~_t144 [ LRES, 12385, 2235, p105 ] % 38.51/38.79 (309,1) [16403,4]. true => ~_t224 | ~_t153 | _t145 [ LRES, 16358, 4909, ~_t144 ] % 38.51/38.79 (309,1) [16429,4]. true => ~_t224 | ~_t153 | _t148 [ LRES, 16403, 1952, _t145 ] % 38.51/38.79 (263,1) [347517,4]. true => ~_t148 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 | ~_t5 [ GEN1, 4018, 4020, 4024, 4054, 4028, 4026, 4022, 4016, 4150, 347515, _t276, _t274, _t270, _t237, _t224, _t268, _t272, _t275, _t256 ] % 38.51/38.79 (263,1) [349362,4]. true => ~_t277 | ~_t148 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t15 [ LRES, 347517, 4173, ~_t5 ] % 38.51/38.79 (263,1) [349363,4]. true => ~_t278 | ~_t277 | ~_t148 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 [ LRES, 349362, 4175, ~_t15 ] % 38.51/38.79 (263,1) [349369,4]. true => ~_t278 | ~_t277 | ~_t276 | ~_t148 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 [ LRES, 349363, 4177, ~_t16 ] % 38.51/38.79 (263,1) [349371,4]. true => ~_t278 | ~_t277 | ~_t276 | ~_t274 | ~_t148 | ~_t83 | ~_t20 | ~_t19 | ~_t18 [ LRES, 349369, 4179, ~_t17 ] % 38.51/38.79 (263,1) [349377,4]. true => ~_t278 | ~_t277 | ~_t276 | ~_t274 | ~_t272 | ~_t148 | ~_t83 | ~_t20 | ~_t19 [ LRES, 349371, 4181, ~_t18 ] % 38.51/38.79 (263,1) [349379,4]. true => ~_t278 | ~_t277 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t148 | ~_t83 | ~_t20 [ LRES, 349377, 4183, ~_t19 ] % 38.51/38.79 (263,1) [349385,4]. true => ~_t278 | ~_t277 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t148 | ~_t83 [ LRES, 349379, 4185, ~_t20 ] % 38.51/38.79 (309,1) [349387,4]. true => ~_t278 | ~_t277 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t224 | ~_t153 | ~_t148 [ LRES, 349385, 10996, ~_t83 ] [ Backward Subsumption, 349438 ] % 38.51/38.79 (309,1) [349438,4]. true => ~_t278 | ~_t277 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t224 | ~_t153 [ LRES, 349387, 16429, ~_t148 ] % 38.51/38.79 (309,1) [349469,4]. true => ~_t278 | ~_t277 | ~_t276 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t257 | ~_t224 [ LRES, 349438, 4313, ~_t153 ] % 38.51/38.79 (1,1) [14,5]. _t6 => box 1 _t7 [ SNF ] [ SNF++, 3864, _t7 ] % 38.51/38.79 (1,1) [305,5]. _t16 => box 1 _t17 [ SNF ] [ SNF++, 3866, _t17 ] % 38.51/38.79 (1,1) [594,5]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 3868, _t18 ] % 38.51/38.79 (1,1) [881,5]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 3870, _t19 ] % 38.51/38.79 (1,1) [1166,5]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 3872, _t20 ] % 38.51/38.79 (1,1) [1449,5]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 3874, _t21 ] % 38.51/38.79 (1,1) [1472,5]. true => ~_t27 | ~p105 | p104 [ SNF ] % 38.51/38.79 (1,1) [1473,5]. true => _t27 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [1555,5]. _t83 => box 1 _t84 [ SNF ] [ SNF++, 3900, _t84 ] % 38.51/38.79 (1,1) [1557,5]. true => _t83 | ~_t82 | p4 [ SNF ] % 38.51/38.79 (1,1) [1558,5]. true => _t82 | ~_t81 [ SNF ] % 38.51/38.79 (1,1) [1564,5]. true => _t81 | ~_t80 | ~p104 [ SNF ] % 38.51/38.79 (1,1) [1565,5]. true => _t80 | ~_t21 [ SNF ] % 38.51/38.79 (219,1) [1658,5]. _t142 => ~box 1~ _t143 [ SNF ] [ SNF++, 3990, _t143 ] % 38.51/38.79 (1,1) [1659,5]. true => _t142 | ~_t139 [ SNF ] % 38.51/38.79 (1,1) [1660,5]. true => _t139 | ~_t138 | p106 | ~p105 [ SNF ] % 38.51/38.79 (1,1) [1661,5]. true => _t138 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [1835,5]. true => ~_t84 | ~p4 | ~p104 [ SNF ] % 38.51/38.79 (263,1) [1949,5]. true => ~_t149 | ~p106 [ SNF ] % 38.51/38.79 (263,1) [1950,5]. true => ~_t149 | p105 [ SNF ] % 38.51/38.79 (1,1) [3864,5]. _t6 => box 1 _t273 [ SNF++, 14 ] % 38.51/38.79 (1,1) [3866,5]. _t16 => box 1 _t274 [ SNF++, 305 ] % 38.51/38.79 (1,1) [3868,5]. _t17 => box 1 _t272 [ SNF++, 594 ] % 38.51/38.79 (1,1) [3870,5]. _t18 => box 1 _t270 [ SNF++, 881 ] % 38.51/38.79 (1,1) [3872,5]. _t19 => box 1 _t268 [ SNF++, 1166 ] % 38.51/38.79 (1,1) [3874,5]. _t20 => box 1 _t224 [ SNF++, 1449 ] % 38.51/38.79 (1,1) [3900,5]. _t83 => box 1 _t237 [ SNF++, 1555 ] % 38.51/38.79 (219,1) [3990,5]. _t142 => ~box 1~ _t254 [ SNF++, 1658 ] % 38.51/38.79 (1,1) [4017,5]. true => ~_t275 | _t6 [ SNF++, 16 ] % 38.51/38.79 (1,1) [4019,5]. true => ~_t276 | _t16 [ SNF++, 307 ] % 38.51/38.79 (1,1) [4021,5]. true => ~_t274 | _t17 [ SNF++, 596 ] % 38.51/38.79 (1,1) [4023,5]. true => ~_t272 | _t18 [ SNF++, 883 ] % 38.51/38.79 (1,1) [4025,5]. true => ~_t270 | _t19 [ SNF++, 1168 ] % 38.51/38.79 (1,1) [4027,5]. true => ~_t268 | _t20 [ SNF++, 1451 ] % 38.51/38.79 (1,1) [4029,5]. true => ~_t224 | _t21 [ SNF++, 1732 ] % 38.51/38.79 (1,1) [4055,5]. true => ~_t237 | _t84 [ SNF++, 1836 ] % 38.51/38.79 (263,1) [4151,5]. true => ~_t256 | _t149 [ SNF++, 1951 ] % 38.51/38.79 (1,1) [4920,5]. true => ~_t224 | _t138 [ LRES, 1661, 4029, ~_t21 ] % 38.51/38.79 (1,1) [5016,5]. true => ~_t224 | _t80 [ LRES, 1565, 4029, ~_t21 ] % 38.51/38.79 (1,1) [5140,5]. true => ~_t224 | _t27 [ LRES, 1473, 4029, ~_t21 ] % 38.51/38.79 (1,1) [7997,5]. true => ~_t84 | ~_t27 | ~p4 | ~p105 [ LRES, 1835, 1472, ~p104 ] % 38.51/38.79 (1,1) [8025,5]. true => _t81 | ~_t80 | ~_t27 | ~p105 [ LRES, 1564, 1472, ~p104 ] % 38.51/38.79 (263,1) [12086,5]. true => ~_t149 | _t81 | ~_t80 | ~_t27 [ LRES, 8025, 1950, ~p105 ] % 38.51/38.79 (263,1) [12113,5]. true => ~_t149 | ~_t84 | ~_t27 | ~p4 [ LRES, 7997, 1950, ~p105 ] % 38.51/38.79 (263,1) [12221,5]. true => ~_t149 | _t139 | ~_t138 | p106 [ LRES, 1660, 1950, ~p105 ] [ Backward Subsumption, 15575 ] % 38.51/38.79 (263,1) [15424,5]. true => ~_t224 | ~_t149 | _t81 | ~_t80 [ LRES, 12086, 5140, ~_t27 ] [ Backward Subsumption, 18738 ] % 38.51/38.79 (263,1) [15444,5]. true => ~_t149 | ~_t84 | _t83 | ~_t82 | ~_t27 [ LRES, 12113, 1557, ~p4 ] % 38.51/38.79 (263,1) [15575,5]. true => ~_t149 | _t139 | ~_t138 [ LRES, 12221, 1949, p106 ] % 38.51/38.79 (263,1) [15634,5]. true => ~_t224 | ~_t149 | _t139 [ LRES, 15575, 4920, ~_t138 ] % 38.51/38.79 (263,1) [15661,5]. true => ~_t224 | ~_t149 | _t142 [ LRES, 15634, 1659, _t139 ] % 38.51/38.79 (263,1) [18738,5]. true => ~_t224 | ~_t149 | _t81 [ LRES, 15424, 5016, ~_t80 ] % 38.51/38.79 (263,1) [18749,5]. true => ~_t224 | ~_t149 | _t82 [ LRES, 18738, 1558, _t81 ] % 38.51/38.79 (263,1) [24828,5]. true => ~_t224 | ~_t149 | ~_t84 | _t83 | ~_t82 [ LRES, 15444, 5140, ~_t27 ] [ Backward Subsumption, 33880 ] % 38.51/38.79 (263,1) [33880,5]. true => ~_t224 | ~_t149 | ~_t84 | _t83 [ LRES, 24828, 18749, ~_t82 ] % 38.51/38.79 (219,1) [335283,5]. true => ~_t142 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 | ~_t6 [ GEN1, 3866, 3868, 3872, 3874, 3900, 3870, 3864, 3990, 335282, _t274, _t272, _t268, _t224, _t237, _t270, _t273, _t254 ] % 38.51/38.79 (219,1) [347312,5]. true => ~_t275 | ~_t142 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t16 [ LRES, 335283, 4017, ~_t6 ] % 38.51/38.79 (219,1) [347313,5]. true => ~_t276 | ~_t275 | ~_t142 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 [ LRES, 347312, 4019, ~_t16 ] % 38.51/38.79 (219,1) [347316,5]. true => ~_t276 | ~_t275 | ~_t274 | ~_t142 | ~_t83 | ~_t20 | ~_t19 | ~_t18 [ LRES, 347313, 4021, ~_t17 ] % 38.51/38.79 (219,1) [347317,5]. true => ~_t276 | ~_t275 | ~_t274 | ~_t272 | ~_t142 | ~_t83 | ~_t20 | ~_t19 [ LRES, 347316, 4023, ~_t18 ] % 38.51/38.79 (219,1) [347320,5]. true => ~_t276 | ~_t275 | ~_t274 | ~_t272 | ~_t270 | ~_t142 | ~_t83 | ~_t20 [ LRES, 347317, 4025, ~_t19 ] % 38.51/38.79 (219,1) [347321,5]. true => ~_t276 | ~_t275 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t142 | ~_t83 [ LRES, 347320, 4027, ~_t20 ] % 38.51/38.79 (263,1) [347372,5]. true => ~_t276 | ~_t275 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t224 | ~_t149 | ~_t142 | ~_t84 [ LRES, 347321, 33880, ~_t83 ] % 38.51/38.79 (263,1) [347375,5]. true => ~_t276 | ~_t275 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t237 | ~_t224 | ~_t149 | ~_t142 [ LRES, 347372, 4055, ~_t84 ] [ Backward Subsumption, 347392 ] % 38.51/38.79 (263,1) [347392,5]. true => ~_t276 | ~_t275 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t237 | ~_t224 | ~_t149 [ LRES, 347375, 15661, ~_t142 ] % 38.51/38.79 (263,1) [347515,5]. true => ~_t276 | ~_t275 | ~_t274 | ~_t272 | ~_t270 | ~_t268 | ~_t256 | ~_t237 | ~_t224 [ LRES, 347392, 4151, ~_t149 ] % 38.51/38.79 (1,1) [12,6]. _t7 => box 1 _t8 [ SNF ] [ SNF++, 3716, _t8 ] % 38.51/38.79 (1,1) [303,6]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 3718, _t18 ] % 38.51/38.79 (1,1) [592,6]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 3720, _t19 ] % 38.51/38.79 (1,1) [879,6]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 3722, _t20 ] % 38.51/38.79 (1,1) [1164,6]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 3724, _t21 ] % 38.51/38.79 (1,1) [1187,6]. true => ~_t26 | ~p106 | p105 [ SNF ] % 38.51/38.79 (1,1) [1188,6]. true => _t26 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [1189,6]. true => ~_t27 | ~p105 | p104 [ SNF ] % 38.51/38.79 (1,1) [1190,6]. true => _t27 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [1272,6]. _t83 => box 1 _t84 [ SNF ] [ SNF++, 3750, _t84 ] % 38.51/38.79 (1,1) [1274,6]. true => _t83 | ~_t82 | p4 [ SNF ] % 38.51/38.79 (1,1) [1275,6]. true => _t82 | ~_t81 [ SNF ] % 38.51/38.79 (1,1) [1281,6]. true => _t81 | ~_t80 | ~p104 [ SNF ] % 38.51/38.79 (1,1) [1282,6]. true => _t80 | ~_t21 [ SNF ] % 38.51/38.79 (177,1) [1358,6]. _t134 => ~box 1~ _t135 [ SNF ] [ SNF++, 3832, _t135 ] % 38.51/38.79 (1,1) [1359,6]. true => _t134 | ~_t133 [ SNF ] % 38.51/38.79 (1,1) [1365,6]. true => _t133 | ~_t132 | p107 | ~p106 [ SNF ] % 38.51/38.79 (1,1) [1366,6]. true => _t132 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [1554,6]. true => ~_t84 | ~p4 | ~p104 [ SNF ] % 38.51/38.79 (219,1) [1656,6]. true => ~_t143 | ~p107 [ SNF ] % 38.51/38.79 (219,1) [1657,6]. true => ~_t143 | p106 [ SNF ] % 38.51/38.79 (1,1) [3716,6]. _t7 => box 1 _t271 [ SNF++, 12 ] % 38.51/38.79 (1,1) [3718,6]. _t17 => box 1 _t272 [ SNF++, 303 ] % 38.51/38.79 (1,1) [3720,6]. _t18 => box 1 _t270 [ SNF++, 592 ] % 38.51/38.79 (1,1) [3722,6]. _t19 => box 1 _t268 [ SNF++, 879 ] % 38.51/38.79 (1,1) [3724,6]. _t20 => box 1 _t224 [ SNF++, 1164 ] % 38.51/38.79 (1,1) [3750,6]. _t83 => box 1 _t237 [ SNF++, 1272 ] % 38.51/38.79 (177,1) [3832,6]. _t134 => ~box 1~ _t251 [ SNF++, 1358 ] % 38.51/38.79 (1,1) [3865,6]. true => ~_t273 | _t7 [ SNF++, 14 ] % 38.51/38.79 (1,1) [3867,6]. true => ~_t274 | _t17 [ SNF++, 305 ] % 38.51/38.79 (1,1) [3869,6]. true => ~_t272 | _t18 [ SNF++, 594 ] % 38.51/38.79 (1,1) [3871,6]. true => ~_t270 | _t19 [ SNF++, 881 ] % 38.51/38.79 (1,1) [3873,6]. true => ~_t268 | _t20 [ SNF++, 1166 ] % 38.51/38.79 (1,1) [3875,6]. true => ~_t224 | _t21 [ SNF++, 1449 ] % 38.51/38.79 (1,1) [3901,6]. true => ~_t237 | _t84 [ SNF++, 1555 ] % 38.51/38.79 (219,1) [3991,6]. true => ~_t254 | _t143 [ SNF++, 1658 ] % 38.51/38.79 (1,1) [4931,6]. true => ~_t224 | _t132 [ LRES, 1366, 3875, ~_t21 ] % 38.51/38.79 (1,1) [5015,6]. true => ~_t224 | _t80 [ LRES, 1282, 3875, ~_t21 ] % 38.51/38.79 (1,1) [5139,6]. true => ~_t224 | _t27 [ LRES, 1190, 3875, ~_t21 ] % 38.51/38.79 (1,1) [5150,6]. true => ~_t224 | _t26 [ LRES, 1188, 3875, ~_t21 ] % 38.51/38.79 (1,1) [7994,6]. true => ~_t84 | ~_t27 | ~p4 | ~p105 [ LRES, 1554, 1189, ~p104 ] % 38.51/38.79 (1,1) [8022,6]. true => _t81 | ~_t80 | ~_t27 | ~p105 [ LRES, 1281, 1189, ~p104 ] % 38.51/38.79 (219,1) [12056,6]. true => ~_t143 | _t133 | ~_t132 | p107 [ LRES, 1365, 1657, ~p106 ] [ Backward Subsumption, 14968 ] % 38.51/38.79 (1,1) [12081,6]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~p106 [ LRES, 8022, 1187, ~p105 ] % 38.51/38.79 (1,1) [12108,6]. true => ~_t84 | ~_t27 | ~_t26 | ~p4 | ~p106 [ LRES, 7994, 1187, ~p105 ] % 38.51/38.79 (219,1) [14968,6]. true => ~_t143 | _t133 | ~_t132 [ LRES, 12056, 1656, p107 ] % 38.51/38.79 (219,1) [15039,6]. true => ~_t224 | ~_t143 | _t133 [ LRES, 14968, 4931, ~_t132 ] % 38.51/38.79 (219,1) [15063,6]. true => ~_t224 | ~_t143 | _t134 [ LRES, 15039, 1359, _t133 ] % 38.51/38.79 (219,1) [21394,6]. true => ~_t143 | ~_t84 | ~_t27 | ~_t26 | ~p4 [ LRES, 12108, 1657, ~p106 ] % 38.51/38.79 (219,1) [21419,6]. true => ~_t143 | _t81 | ~_t80 | ~_t27 | ~_t26 [ LRES, 12081, 1657, ~p106 ] % 38.51/38.79 (219,1) [24006,6]. true => ~_t224 | ~_t143 | _t81 | ~_t80 | ~_t27 [ LRES, 21419, 5150, ~_t26 ] [ Backward Subsumption, 24654 ] % 38.51/38.79 (219,1) [24654,6]. true => ~_t224 | ~_t143 | _t81 | ~_t80 [ LRES, 24006, 5139, ~_t27 ] [ Backward Subsumption, 24663 ] % 38.51/38.79 (219,1) [24663,6]. true => ~_t224 | ~_t143 | _t81 [ LRES, 24654, 5015, ~_t80 ] % 38.51/38.79 (219,1) [24671,6]. true => ~_t224 | ~_t143 | _t82 [ LRES, 24663, 1275, _t81 ] % 38.51/38.79 (219,1) [25577,6]. true => ~_t143 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 [ LRES, 21394, 1274, ~p4 ] % 38.51/38.79 (219,1) [39915,6]. true => ~_t224 | ~_t143 | ~_t84 | _t83 | ~_t82 | ~_t27 [ LRES, 25577, 5150, ~_t26 ] [ Backward Subsumption, 40270 ] % 38.51/38.79 (219,1) [40270,6]. true => ~_t224 | ~_t143 | ~_t84 | _t83 | ~_t82 [ LRES, 39915, 5139, ~_t27 ] [ Backward Subsumption, 40277 ] % 38.51/38.79 (219,1) [40277,6]. true => ~_t224 | ~_t143 | ~_t84 | _t83 [ LRES, 40270, 24671, ~_t82 ] % 38.51/38.79 (177,1) [335075,6]. true => ~_t134 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 | ~_t7 [ GEN1, 3718, 3720, 3750, 3724, 3722, 3716, 3832, 335073, _t272, _t270, _t237, _t224, _t268, _t271, _t251 ] % 38.51/38.79 (177,1) [335101,6]. true => ~_t273 | ~_t134 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t17 [ LRES, 335075, 3865, ~_t7 ] % 38.51/38.79 (177,1) [335102,6]. true => ~_t274 | ~_t273 | ~_t134 | ~_t83 | ~_t20 | ~_t19 | ~_t18 [ LRES, 335101, 3867, ~_t17 ] % 38.51/38.79 (177,1) [335104,6]. true => ~_t274 | ~_t273 | ~_t272 | ~_t134 | ~_t83 | ~_t20 | ~_t19 [ LRES, 335102, 3869, ~_t18 ] % 38.51/38.79 (177,1) [335107,6]. true => ~_t274 | ~_t273 | ~_t272 | ~_t270 | ~_t134 | ~_t83 | ~_t20 [ LRES, 335104, 3871, ~_t19 ] % 38.51/38.79 (177,1) [335108,6]. true => ~_t274 | ~_t273 | ~_t272 | ~_t270 | ~_t268 | ~_t134 | ~_t83 [ LRES, 335107, 3873, ~_t20 ] % 38.51/38.79 (219,1) [335131,6]. true => ~_t274 | ~_t273 | ~_t272 | ~_t270 | ~_t268 | ~_t224 | ~_t143 | ~_t134 | ~_t84 [ LRES, 335108, 40277, ~_t83 ] % 38.51/38.79 (219,1) [335277,6]. true => ~_t274 | ~_t273 | ~_t272 | ~_t270 | ~_t268 | ~_t237 | ~_t224 | ~_t143 | ~_t134 [ LRES, 335131, 3901, ~_t84 ] [ Backward Subsumption, 335281 ] % 38.51/38.79 (219,1) [335281,6]. true => ~_t274 | ~_t273 | ~_t272 | ~_t270 | ~_t268 | ~_t237 | ~_t224 | ~_t143 [ LRES, 335277, 15063, ~_t134 ] % 38.51/38.79 (219,1) [335282,6]. true => ~_t274 | ~_t273 | ~_t272 | ~_t270 | ~_t268 | ~_t254 | ~_t237 | ~_t224 [ LRES, 335281, 3991, ~_t143 ] % 38.51/38.79 (1,1) [10,7]. _t8 => box 1 _t9 [ SNF ] [ SNF++, 3572, _t9 ] % 38.51/38.79 (1,1) [301,7]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 3574, _t19 ] % 38.51/38.79 (1,1) [590,7]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 3576, _t20 ] % 38.51/38.79 (1,1) [877,7]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 3578, _t21 ] % 38.51/38.79 (1,1) [900,7]. true => ~_t25 | ~p107 | p106 [ SNF ] % 38.51/38.79 (1,1) [901,7]. true => _t25 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [902,7]. true => ~_t26 | ~p106 | p105 [ SNF ] % 38.51/38.79 (1,1) [903,7]. true => _t26 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [904,7]. true => ~_t27 | ~p105 | p104 [ SNF ] % 38.51/38.79 (1,1) [905,7]. true => _t27 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [987,7]. _t83 => box 1 _t84 [ SNF ] [ SNF++, 3604, _t84 ] % 38.51/38.79 (1,1) [989,7]. true => _t83 | ~_t82 | p4 [ SNF ] % 38.51/38.79 (1,1) [990,7]. true => _t82 | ~_t81 [ SNF ] % 38.51/38.79 (1,1) [996,7]. true => _t81 | ~_t80 | ~p104 [ SNF ] % 38.51/38.79 (1,1) [997,7]. true => _t80 | ~_t21 [ SNF ] % 38.51/38.79 (133,1) [1061,7]. _t128 => ~box 1~ _t129 [ SNF ] [ SNF++, 3680, _t129 ] % 38.51/38.79 (1,1) [1062,7]. true => _t128 | ~_t127 [ SNF ] % 38.51/38.79 (1,1) [1068,7]. true => _t127 | ~_t126 | p108 | ~p107 [ SNF ] % 38.51/38.79 (1,1) [1069,7]. true => _t126 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [1271,7]. true => ~_t84 | ~p4 | ~p104 [ SNF ] % 38.51/38.79 (177,1) [1356,7]. true => ~_t135 | ~p108 [ SNF ] % 38.51/38.79 (177,1) [1357,7]. true => ~_t135 | p107 [ SNF ] % 38.51/38.79 (1,1) [3572,7]. _t8 => box 1 _t269 [ SNF++, 10 ] % 38.51/38.79 (1,1) [3574,7]. _t18 => box 1 _t270 [ SNF++, 301 ] % 38.51/38.79 (1,1) [3576,7]. _t19 => box 1 _t268 [ SNF++, 590 ] % 38.51/38.79 (1,1) [3578,7]. _t20 => box 1 _t224 [ SNF++, 877 ] % 38.51/38.79 (1,1) [3604,7]. _t83 => box 1 _t237 [ SNF++, 987 ] % 38.51/38.79 (133,1) [3680,7]. _t128 => ~box 1~ _t249 [ SNF++, 1061 ] % 38.51/38.79 (1,1) [3717,7]. true => ~_t271 | _t8 [ SNF++, 12 ] % 38.51/38.79 (1,1) [3719,7]. true => ~_t272 | _t18 [ SNF++, 303 ] % 38.51/38.79 (1,1) [3721,7]. true => ~_t270 | _t19 [ SNF++, 592 ] % 38.51/38.79 (1,1) [3723,7]. true => ~_t268 | _t20 [ SNF++, 879 ] % 38.51/38.79 (1,1) [3725,7]. true => ~_t224 | _t21 [ SNF++, 1164 ] % 38.51/38.79 (1,1) [3751,7]. true => ~_t237 | _t84 [ SNF++, 1272 ] % 38.51/38.79 (177,1) [3833,7]. true => ~_t251 | _t135 [ SNF++, 1358 ] % 38.51/38.79 (1,1) [4942,7]. true => ~_t224 | _t126 [ LRES, 1069, 3725, ~_t21 ] % 38.51/38.79 (1,1) [5014,7]. true => ~_t224 | _t80 [ LRES, 997, 3725, ~_t21 ] % 38.51/38.79 (1,1) [5138,7]. true => ~_t224 | _t27 [ LRES, 905, 3725, ~_t21 ] % 38.51/38.79 (1,1) [5149,7]. true => ~_t224 | _t26 [ LRES, 903, 3725, ~_t21 ] % 38.51/38.79 (1,1) [5160,7]. true => ~_t224 | _t25 [ LRES, 901, 3725, ~_t21 ] % 38.51/38.79 (1,1) [7991,7]. true => ~_t84 | ~_t27 | ~p4 | ~p105 [ LRES, 1271, 904, ~p104 ] % 38.51/38.79 (1,1) [8019,7]. true => _t81 | ~_t80 | ~_t27 | ~p105 [ LRES, 996, 904, ~p104 ] % 38.51/38.79 (177,1) [11890,7]. true => ~_t135 | _t127 | ~_t126 | p108 [ LRES, 1068, 1357, ~p107 ] [ Backward Subsumption, 14535 ] % 38.51/38.79 (1,1) [12078,7]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~p106 [ LRES, 8019, 902, ~p105 ] % 38.51/38.79 (1,1) [12105,7]. true => ~_t84 | ~_t27 | ~_t26 | ~p4 | ~p106 [ LRES, 7991, 902, ~p105 ] % 38.51/38.79 (177,1) [14535,7]. true => ~_t135 | _t127 | ~_t126 [ LRES, 11890, 1356, p108 ] % 38.51/38.79 (177,1) [14616,7]. true => ~_t224 | ~_t135 | _t127 [ LRES, 14535, 4942, ~_t126 ] % 38.51/38.79 (177,1) [14638,7]. true => ~_t224 | ~_t135 | _t128 [ LRES, 14616, 1062, _t127 ] % 38.51/38.79 (1,1) [21588,7]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~p4 | ~p107 [ LRES, 12105, 900, ~p106 ] % 38.51/38.79 (1,1) [21613,7]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~p107 [ LRES, 12078, 900, ~p106 ] % 38.51/38.79 (177,1) [43000,7]. true => ~_t135 | _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 [ LRES, 21613, 1357, ~p107 ] % 38.51/38.79 (177,1) [43013,7]. true => ~_t135 | ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~p4 [ LRES, 21588, 1357, ~p107 ] % 38.51/38.79 (177,1) [48270,7]. true => ~_t224 | ~_t135 | _t81 | ~_t80 | ~_t27 | ~_t26 [ LRES, 43000, 5160, ~_t25 ] [ Backward Subsumption, 48338 ] % 38.51/38.79 (177,1) [48294,7]. true => ~_t135 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 | ~_t25 [ LRES, 43013, 989, ~p4 ] % 38.51/38.79 (177,1) [48338,7]. true => ~_t224 | ~_t135 | _t81 | ~_t80 | ~_t27 [ LRES, 48270, 5149, ~_t26 ] [ Backward Subsumption, 48349 ] % 38.51/38.79 (177,1) [48349,7]. true => ~_t224 | ~_t135 | _t81 | ~_t80 [ LRES, 48338, 5138, ~_t27 ] [ Backward Subsumption, 48370 ] % 38.51/38.79 (177,1) [48370,7]. true => ~_t224 | ~_t135 | _t81 [ LRES, 48349, 5014, ~_t80 ] % 38.51/38.79 (177,1) [48389,7]. true => ~_t224 | ~_t135 | _t82 [ LRES, 48370, 990, _t81 ] % 38.51/38.79 (177,1) [84895,7]. true => ~_t224 | ~_t135 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 [ LRES, 48294, 5160, ~_t25 ] [ Backward Subsumption, 86107 ] % 38.51/38.79 (177,1) [86107,7]. true => ~_t224 | ~_t135 | ~_t84 | _t83 | ~_t82 | ~_t27 [ LRES, 84895, 5149, ~_t26 ] [ Backward Subsumption, 86123 ] % 38.51/38.79 (177,1) [86123,7]. true => ~_t224 | ~_t135 | ~_t84 | _t83 | ~_t82 [ LRES, 86107, 5138, ~_t27 ] [ Backward Subsumption, 86191 ] % 38.51/38.79 (177,1) [86191,7]. true => ~_t224 | ~_t135 | ~_t84 | _t83 [ LRES, 86123, 48389, ~_t82 ] % 38.51/38.79 (133,1) [333691,7]. true => ~_t128 | ~_t83 | ~_t20 | ~_t19 | ~_t18 | ~_t8 [ GEN1, 3574, 3576, 3578, 3604, 3572, 3680, 333689, _t270, _t268, _t224, _t237, _t269, _t249 ] % 38.51/38.79 (133,1) [333718,7]. true => ~_t271 | ~_t128 | ~_t83 | ~_t20 | ~_t19 | ~_t18 [ LRES, 333691, 3717, ~_t8 ] % 38.51/38.79 (133,1) [333721,7]. true => ~_t272 | ~_t271 | ~_t128 | ~_t83 | ~_t20 | ~_t19 [ LRES, 333718, 3719, ~_t18 ] % 38.51/38.79 (133,1) [333722,7]. true => ~_t272 | ~_t271 | ~_t270 | ~_t128 | ~_t83 | ~_t20 [ LRES, 333721, 3721, ~_t19 ] % 38.51/38.79 (133,1) [333724,7]. true => ~_t272 | ~_t271 | ~_t270 | ~_t268 | ~_t128 | ~_t83 [ LRES, 333722, 3723, ~_t20 ] % 38.51/38.79 (177,1) [333746,7]. true => ~_t272 | ~_t271 | ~_t270 | ~_t268 | ~_t224 | ~_t135 | ~_t128 | ~_t84 [ LRES, 333724, 86191, ~_t83 ] % 38.51/38.79 (177,1) [335068,7]. true => ~_t272 | ~_t271 | ~_t270 | ~_t268 | ~_t237 | ~_t224 | ~_t135 | ~_t128 [ LRES, 333746, 3751, ~_t84 ] [ Backward Subsumption, 335070 ] % 38.51/38.79 (177,1) [335070,7]. true => ~_t272 | ~_t271 | ~_t270 | ~_t268 | ~_t237 | ~_t224 | ~_t135 [ LRES, 335068, 14638, ~_t128 ] % 38.51/38.79 (177,1) [335073,7]. true => ~_t272 | ~_t271 | ~_t270 | ~_t268 | ~_t251 | ~_t237 | ~_t224 [ LRES, 335070, 3833, ~_t135 ] % 38.51/38.79 (1,1) [8,8]. _t9 => box 1 _t10 [ SNF ] [ SNF++, 3432, _t10 ] % 38.51/38.79 (1,1) [299,8]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 3434, _t20 ] % 38.51/38.79 (1,1) [588,8]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 3436, _t21 ] % 38.51/38.79 (1,1) [611,8]. true => ~_t24 | ~p108 | p107 [ SNF ] % 38.51/38.79 (1,1) [612,8]. true => _t24 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [613,8]. true => ~_t25 | ~p107 | p106 [ SNF ] % 38.51/38.79 (1,1) [614,8]. true => _t25 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [615,8]. true => ~_t26 | ~p106 | p105 [ SNF ] % 38.51/38.79 (1,1) [616,8]. true => _t26 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [617,8]. true => ~_t27 | ~p105 | p104 [ SNF ] % 38.51/38.79 (1,1) [618,8]. true => _t27 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [700,8]. _t83 => box 1 _t84 [ SNF ] [ SNF++, 3462, _t84 ] % 38.51/38.79 (1,1) [702,8]. true => _t83 | ~_t82 | p4 [ SNF ] % 38.51/38.79 (1,1) [703,8]. true => _t82 | ~_t81 [ SNF ] % 38.51/38.79 (1,1) [709,8]. true => _t81 | ~_t80 | ~p104 [ SNF ] % 38.51/38.79 (1,1) [710,8]. true => _t80 | ~_t21 [ SNF ] % 38.51/38.79 (87,1) [767,8]. _t124 => ~box 1~ _t125 [ SNF ] [ SNF++, 3534, _t125 ] % 38.51/38.79 (1,1) [768,8]. true => _t124 | ~_t121 [ SNF ] % 38.51/38.79 (1,1) [769,8]. true => _t121 | ~_t120 | p109 | ~p108 [ SNF ] % 38.51/38.79 (1,1) [770,8]. true => _t120 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [986,8]. true => ~_t84 | ~p4 | ~p104 [ SNF ] % 38.51/38.79 (133,1) [1059,8]. true => ~_t129 | ~p109 [ SNF ] % 38.51/38.79 (133,1) [1060,8]. true => ~_t129 | p108 [ SNF ] % 38.51/38.79 (1,1) [3432,8]. _t9 => box 1 _t267 [ SNF++, 8 ] % 38.51/38.79 (1,1) [3434,8]. _t19 => box 1 _t268 [ SNF++, 299 ] % 38.51/38.79 (1,1) [3436,8]. _t20 => box 1 _t224 [ SNF++, 588 ] % 38.51/38.79 (1,1) [3462,8]. _t83 => box 1 _t237 [ SNF++, 700 ] % 38.51/38.79 (87,1) [3534,8]. _t124 => ~box 1~ _t248 [ SNF++, 767 ] % 38.51/38.79 (1,1) [3573,8]. true => ~_t269 | _t9 [ SNF++, 10 ] % 38.51/38.79 (1,1) [3575,8]. true => ~_t270 | _t19 [ SNF++, 301 ] % 38.51/38.79 (1,1) [3577,8]. true => ~_t268 | _t20 [ SNF++, 590 ] % 38.51/38.79 (1,1) [3579,8]. true => ~_t224 | _t21 [ SNF++, 877 ] % 38.51/38.79 (1,1) [3605,8]. true => ~_t237 | _t84 [ SNF++, 987 ] % 38.51/38.79 (133,1) [3681,8]. true => ~_t249 | _t129 [ SNF++, 1061 ] % 38.51/38.79 (1,1) [4953,8]. true => ~_t224 | _t120 [ LRES, 770, 3579, ~_t21 ] % 38.51/38.79 (1,1) [5013,8]. true => ~_t224 | _t80 [ LRES, 710, 3579, ~_t21 ] % 38.51/38.79 (1,1) [5137,8]. true => ~_t224 | _t27 [ LRES, 618, 3579, ~_t21 ] % 38.51/38.79 (1,1) [5148,8]. true => ~_t224 | _t26 [ LRES, 616, 3579, ~_t21 ] % 38.51/38.79 (1,1) [5159,8]. true => ~_t224 | _t25 [ LRES, 614, 3579, ~_t21 ] % 38.51/38.79 (1,1) [5170,8]. true => ~_t224 | _t24 [ LRES, 612, 3579, ~_t21 ] % 38.51/38.79 (1,1) [7988,8]. true => ~_t84 | ~_t27 | ~p4 | ~p105 [ LRES, 986, 617, ~p104 ] % 38.51/38.79 (1,1) [8016,8]. true => _t81 | ~_t80 | ~_t27 | ~p105 [ LRES, 709, 617, ~p104 ] % 38.51/38.79 (133,1) [11725,8]. true => ~_t129 | _t121 | ~_t120 | p109 [ LRES, 769, 1060, ~p108 ] [ Backward Subsumption, 13928 ] % 38.51/38.79 (1,1) [12075,8]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~p106 [ LRES, 8016, 615, ~p105 ] % 38.51/38.79 (1,1) [12102,8]. true => ~_t84 | ~_t27 | ~_t26 | ~p4 | ~p106 [ LRES, 7988, 615, ~p105 ] % 38.51/38.79 (133,1) [13928,8]. true => ~_t129 | _t121 | ~_t120 [ LRES, 11725, 1059, p109 ] % 38.51/38.79 (133,1) [14021,8]. true => ~_t224 | ~_t129 | _t121 [ LRES, 13928, 4953, ~_t120 ] % 38.51/38.79 (133,1) [14043,8]. true => ~_t224 | ~_t129 | _t124 [ LRES, 14021, 768, _t121 ] % 38.51/38.79 (1,1) [21635,8]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~p4 | ~p107 [ LRES, 12102, 613, ~p106 ] % 38.51/38.79 (1,1) [21659,8]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~p107 [ LRES, 12075, 613, ~p106 ] % 38.51/38.79 (1,1) [42932,8]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~p108 [ LRES, 21659, 611, ~p107 ] % 38.51/38.79 (1,1) [42957,8]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~p4 | ~p108 [ LRES, 21635, 611, ~p107 ] % 38.51/38.79 (133,1) [63895,8]. true => ~_t129 | ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~p4 [ LRES, 42957, 1060, ~p108 ] % 38.51/38.79 (133,1) [63898,8]. true => ~_t129 | _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~_t24 [ LRES, 42932, 1060, ~p108 ] % 38.51/38.79 (133,1) [80781,8]. true => ~_t224 | ~_t129 | _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 [ LRES, 63898, 5170, ~_t24 ] [ Backward Subsumption, 84262 ] % 38.51/38.79 (133,1) [84262,8]. true => ~_t224 | ~_t129 | _t81 | ~_t80 | ~_t27 | ~_t26 [ LRES, 80781, 5159, ~_t25 ] [ Backward Subsumption, 84300 ] % 38.51/38.79 (133,1) [84300,8]. true => ~_t224 | ~_t129 | _t81 | ~_t80 | ~_t27 [ LRES, 84262, 5148, ~_t26 ] [ Backward Subsumption, 84330 ] % 38.51/38.79 (133,1) [84330,8]. true => ~_t224 | ~_t129 | _t81 | ~_t80 [ LRES, 84300, 5137, ~_t27 ] [ Backward Subsumption, 84336 ] % 38.51/38.79 (133,1) [84336,8]. true => ~_t224 | ~_t129 | _t81 [ LRES, 84330, 5013, ~_t80 ] % 38.51/38.79 (133,1) [84351,8]. true => ~_t224 | ~_t129 | _t82 [ LRES, 84336, 703, _t81 ] % 38.51/38.79 (133,1) [101455,8]. true => ~_t129 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 | ~_t25 | ~_t24 [ LRES, 63895, 702, ~p4 ] % 38.51/38.79 (133,1) [124461,8]. true => ~_t224 | ~_t129 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 | ~_t25 [ LRES, 101455, 5170, ~_t24 ] [ Backward Subsumption, 127482 ] % 38.51/38.79 (133,1) [127482,8]. true => ~_t224 | ~_t129 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 [ LRES, 124461, 5159, ~_t25 ] [ Backward Subsumption, 127486 ] % 38.51/38.79 (133,1) [127486,8]. true => ~_t224 | ~_t129 | ~_t84 | _t83 | ~_t82 | ~_t27 [ LRES, 127482, 5148, ~_t26 ] [ Backward Subsumption, 127490 ] % 38.51/38.79 (133,1) [127490,8]. true => ~_t224 | ~_t129 | ~_t84 | _t83 | ~_t82 [ LRES, 127486, 5137, ~_t27 ] [ Backward Subsumption, 127496 ] % 38.51/38.79 (133,1) [127496,8]. true => ~_t224 | ~_t129 | ~_t84 | _t83 [ LRES, 127490, 84351, ~_t82 ] % 38.51/38.79 (87,1) [333643,8]. true => ~_t124 | ~_t83 | ~_t20 | ~_t19 | ~_t9 [ GEN1, 3434, 3462, 3436, 3432, 3534, 333642, _t268, _t237, _t224, _t267, _t248 ] % 38.51/38.79 (87,1) [333644,8]. true => ~_t269 | ~_t124 | ~_t83 | ~_t20 | ~_t19 [ LRES, 333643, 3573, ~_t9 ] % 38.51/38.79 (87,1) [333645,8]. true => ~_t270 | ~_t269 | ~_t124 | ~_t83 | ~_t20 [ LRES, 333644, 3575, ~_t19 ] % 38.51/38.79 (87,1) [333646,8]. true => ~_t270 | ~_t269 | ~_t268 | ~_t124 | ~_t83 [ LRES, 333645, 3577, ~_t20 ] % 38.51/38.79 (133,1) [333664,8]. true => ~_t270 | ~_t269 | ~_t268 | ~_t224 | ~_t129 | ~_t124 | ~_t84 [ LRES, 333646, 127496, ~_t83 ] % 38.51/38.79 (133,1) [333684,8]. true => ~_t270 | ~_t269 | ~_t268 | ~_t237 | ~_t224 | ~_t129 | ~_t124 [ LRES, 333664, 3605, ~_t84 ] [ Backward Subsumption, 333686 ] % 38.51/38.79 (133,1) [333686,8]. true => ~_t270 | ~_t269 | ~_t268 | ~_t237 | ~_t224 | ~_t129 [ LRES, 333684, 14043, ~_t124 ] % 38.51/38.79 (133,1) [333689,8]. true => ~_t270 | ~_t269 | ~_t268 | ~_t249 | ~_t237 | ~_t224 [ LRES, 333686, 3681, ~_t129 ] % 38.51/38.79 (1,1) [6,9]. _t10 => box 1 p4 [ SNF ] [ SNF++, 3296, p4 ] % 38.51/38.79 (1,1) [297,9]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 3298, _t21 ] % 38.51/38.79 (1,1) [320,9]. true => ~_t23 | ~p109 | p108 [ SNF ] % 38.51/38.79 (1,1) [321,9]. true => _t23 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [322,9]. true => ~_t24 | ~p108 | p107 [ SNF ] % 38.51/38.79 (1,1) [323,9]. true => _t24 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [324,9]. true => ~_t25 | ~p107 | p106 [ SNF ] % 38.51/38.79 (1,1) [325,9]. true => _t25 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [326,9]. true => ~_t26 | ~p106 | p105 [ SNF ] % 38.51/38.79 (1,1) [327,9]. true => _t26 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [328,9]. true => ~_t27 | ~p105 | p104 [ SNF ] % 38.51/38.79 (1,1) [329,9]. true => _t27 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [411,9]. _t83 => box 1 _t84 [ SNF ] [ SNF++, 3324, _t84 ] % 38.51/38.79 (1,1) [413,9]. true => _t83 | ~_t82 | p4 [ SNF ] % 38.51/38.79 (1,1) [414,9]. true => _t82 | ~_t81 [ SNF ] % 38.51/38.79 (1,1) [420,9]. true => _t81 | ~_t80 | ~p104 [ SNF ] % 38.51/38.79 (1,1) [421,9]. true => _t80 | ~_t21 [ SNF ] % 38.51/38.79 (45,1) [580,9]. _t176 => ~box 1~ _t177 [ SNF ] [ SNF++, 3428, _t177 ] % 38.51/38.79 (1,1) [581,9]. true => _t176 | ~_t175 [ SNF ] % 38.51/38.79 (1,1) [586,9]. true => _t175 | ~_t174 | p110 | ~p109 [ SNF ] % 38.51/38.79 (1,1) [587,9]. true => _t174 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [699,9]. true => ~_t84 | ~p4 | ~p104 [ SNF ] % 38.51/38.79 (87,1) [765,9]. true => ~_t125 | ~p110 [ SNF ] % 38.51/38.79 (87,1) [766,9]. true => ~_t125 | p109 [ SNF ] % 38.51/38.79 (1,1) [3296,9]. _t10 => box 1 _t223 [ SNF++, 6 ] % 38.51/38.79 (1,1) [3298,9]. _t20 => box 1 _t224 [ SNF++, 297 ] % 38.51/38.79 (1,1) [3324,9]. _t83 => box 1 _t237 [ SNF++, 411 ] % 38.51/38.79 (45,1) [3428,9]. _t176 => ~box 1~ _t265 [ SNF++, 580 ] % 38.51/38.79 (1,1) [3433,9]. true => ~_t267 | _t10 [ SNF++, 8 ] % 38.51/38.79 (1,1) [3435,9]. true => ~_t268 | _t20 [ SNF++, 299 ] % 38.51/38.79 (1,1) [3437,9]. true => ~_t224 | _t21 [ SNF++, 588 ] % 38.51/38.79 (1,1) [3463,9]. true => ~_t237 | _t84 [ SNF++, 700 ] % 38.51/38.79 (87,1) [3535,9]. true => ~_t248 | _t125 [ SNF++, 767 ] % 38.51/38.79 (1,1) [4844,9]. true => ~_t224 | _t174 [ LRES, 587, 3437, ~_t21 ] % 38.51/38.79 (1,1) [5012,9]. true => ~_t224 | _t80 [ LRES, 421, 3437, ~_t21 ] % 38.51/38.79 (1,1) [5136,9]. true => ~_t224 | _t27 [ LRES, 329, 3437, ~_t21 ] % 38.51/38.79 (1,1) [5147,9]. true => ~_t224 | _t26 [ LRES, 327, 3437, ~_t21 ] % 38.51/38.79 (1,1) [5158,9]. true => ~_t224 | _t25 [ LRES, 325, 3437, ~_t21 ] % 38.51/38.79 (1,1) [5169,9]. true => ~_t224 | _t24 [ LRES, 323, 3437, ~_t21 ] % 38.51/38.79 (1,1) [5180,9]. true => ~_t224 | _t23 [ LRES, 321, 3437, ~_t21 ] % 38.51/38.79 (1,1) [8041,9]. true => ~_t84 | ~_t27 | ~p4 | ~p105 [ LRES, 699, 328, ~p104 ] % 38.51/38.79 (1,1) [8062,9]. true => _t81 | ~_t80 | ~_t27 | ~p105 [ LRES, 420, 328, ~p104 ] % 38.51/38.79 (87,1) [11615,9]. true => _t175 | ~_t174 | ~_t125 | p110 [ LRES, 586, 766, ~p109 ] [ Backward Subsumption, 13258 ] % 38.51/38.79 (1,1) [12126,9]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~p106 [ LRES, 8062, 326, ~p105 ] % 38.51/38.79 (1,1) [12153,9]. true => ~_t84 | ~_t27 | ~_t26 | ~p4 | ~p106 [ LRES, 8041, 326, ~p105 ] % 38.51/38.79 (87,1) [13258,9]. true => _t175 | ~_t174 | ~_t125 [ LRES, 11615, 765, p110 ] % 38.51/38.79 (87,1) [13278,9]. true => ~_t248 | _t175 | ~_t174 [ LRES, 13258, 3535, ~_t125 ] % 38.51/38.79 (87,1) [13297,9]. true => ~_t248 | ~_t224 | _t175 [ LRES, 13278, 4844, ~_t174 ] % 38.51/38.79 (87,1) [13309,9]. true => ~_t248 | ~_t224 | _t176 [ LRES, 13297, 581, _t175 ] % 38.51/38.79 (1,1) [21680,9]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~p4 | ~p107 [ LRES, 12153, 324, ~p106 ] % 38.51/38.79 (1,1) [21704,9]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~p107 [ LRES, 12126, 324, ~p106 ] % 38.51/38.79 (1,1) [42980,9]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~p108 [ LRES, 21704, 322, ~p107 ] % 38.51/38.79 (1,1) [42993,9]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~p4 | ~p108 [ LRES, 21680, 322, ~p107 ] % 38.51/38.79 (1,1) [81183,9]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 | ~p4 | ~p109 [ LRES, 42993, 320, ~p108 ] % 38.51/38.79 (1,1) [81186,9]. true => _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 | ~p109 [ LRES, 42980, 320, ~p108 ] % 38.51/38.79 (45,1) [98164,9]. true => ~_t176 | ~_t83 | ~_t20 | ~_t10 [ GEN1, 3324, 3296, 3298, 3428, 98163, _t237, _t223, _t224, _t265 ] % 38.51/38.79 (45,1) [98165,9]. true => ~_t267 | ~_t176 | ~_t83 | ~_t20 [ LRES, 98164, 3433, ~_t10 ] % 38.51/38.79 (45,1) [98167,9]. true => ~_t268 | ~_t267 | ~_t176 | ~_t83 [ LRES, 98165, 3435, ~_t20 ] % 38.51/38.79 (87,1) [199156,9]. true => ~_t125 | _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 [ LRES, 81186, 766, ~p109 ] % 38.51/38.79 (87,1) [199160,9]. true => ~_t125 | ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 | ~p4 [ LRES, 81183, 766, ~p109 ] % 38.51/38.79 (87,1) [207145,9]. true => ~_t224 | ~_t125 | _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 | ~_t24 [ LRES, 199156, 5180, ~_t23 ] [ Backward Subsumption, 215561 ] % 38.51/38.79 (87,1) [215561,9]. true => ~_t224 | ~_t125 | _t81 | ~_t80 | ~_t27 | ~_t26 | ~_t25 [ LRES, 207145, 5169, ~_t24 ] [ Backward Subsumption, 215563 ] % 38.51/38.79 (87,1) [215563,9]. true => ~_t224 | ~_t125 | _t81 | ~_t80 | ~_t27 | ~_t26 [ LRES, 215561, 5158, ~_t25 ] [ Backward Subsumption, 215566 ] % 38.51/38.79 (87,1) [215566,9]. true => ~_t224 | ~_t125 | _t81 | ~_t80 | ~_t27 [ LRES, 215563, 5147, ~_t26 ] [ Backward Subsumption, 215568 ] % 38.51/38.79 (87,1) [215568,9]. true => ~_t224 | ~_t125 | _t81 | ~_t80 [ LRES, 215566, 5136, ~_t27 ] [ Backward Subsumption, 215570 ] % 38.51/38.79 (87,1) [215570,9]. true => ~_t224 | ~_t125 | _t81 [ LRES, 215568, 5012, ~_t80 ] % 38.51/38.79 (87,1) [215572,9]. true => ~_t224 | ~_t125 | _t82 [ LRES, 215570, 414, _t81 ] % 38.51/38.79 (87,1) [277849,9]. true => ~_t125 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 [ LRES, 199160, 413, ~p4 ] % 38.51/38.79 (87,1) [331168,9]. true => ~_t224 | ~_t125 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 | ~_t25 | ~_t24 [ LRES, 277849, 5180, ~_t23 ] [ Backward Subsumption, 331182 ] % 38.51/38.79 (87,1) [331182,9]. true => ~_t224 | ~_t125 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 | ~_t25 [ LRES, 331168, 5169, ~_t24 ] [ Backward Subsumption, 331196 ] % 38.51/38.79 (87,1) [331196,9]. true => ~_t224 | ~_t125 | ~_t84 | _t83 | ~_t82 | ~_t27 | ~_t26 [ LRES, 331182, 5158, ~_t25 ] [ Backward Subsumption, 331210 ] % 38.51/38.79 (87,1) [331210,9]. true => ~_t224 | ~_t125 | ~_t84 | _t83 | ~_t82 | ~_t27 [ LRES, 331196, 5147, ~_t26 ] [ Backward Subsumption, 331212 ] % 38.51/38.79 (87,1) [331212,9]. true => ~_t224 | ~_t125 | ~_t84 | _t83 | ~_t82 [ LRES, 331210, 5136, ~_t27 ] [ Backward Subsumption, 331216 ] % 38.51/38.79 (87,1) [331216,9]. true => ~_t224 | ~_t125 | ~_t84 | _t83 [ LRES, 331212, 215572, ~_t82 ] % 38.51/38.79 (87,1) [331231,9]. true => ~_t268 | ~_t267 | ~_t224 | ~_t176 | ~_t125 | ~_t84 [ LRES, 331216, 98167, _t83 ] % 38.51/38.79 (87,1) [331863,9]. true => ~_t268 | ~_t267 | ~_t237 | ~_t224 | ~_t176 | ~_t125 [ LRES, 331231, 3463, ~_t84 ] % 38.51/38.79 (87,1) [331865,9]. true => ~_t268 | ~_t267 | ~_t248 | ~_t237 | ~_t224 | ~_t176 [ LRES, 331863, 3535, ~_t125 ] [ Backward Subsumption, 333642 ] % 38.51/38.79 (87,1) [333642,9]. true => ~_t268 | ~_t267 | ~_t248 | ~_t237 | ~_t224 [ LRES, 331865, 13309, ~_t176 ] % 38.51/38.79 (1,1) [27,10]. true => ~_t22 | ~p110 | p109 [ SNF ] % 38.51/38.79 (1,1) [28,10]. true => _t22 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [29,10]. true => ~_t23 | ~p109 | p108 [ SNF ] % 38.51/38.79 (1,1) [30,10]. true => _t23 | ~_t21 [ SNF ] % 38.51/38.79 (1,1) [31,10]. true => ~_t24 | ~p108 | p107 [ SNF ] % 39.02/39.29 (1,1) [32,10]. true => _t24 | ~_t21 [ SNF ] % 39.02/39.29 (1,1) [33,10]. true => ~_t25 | ~p107 | p106 [ SNF ] % 39.02/39.29 (1,1) [34,10]. true => _t25 | ~_t21 [ SNF ] % 39.02/39.29 (1,1) [35,10]. true => ~_t26 | ~p106 | p105 [ SNF ] % 39.02/39.29 (1,1) [36,10]. true => _t26 | ~_t21 [ SNF ] % 39.02/39.29 (1,1) [37,10]. true => ~_t27 | ~p105 | p104 [ SNF ] % 39.02/39.29 (1,1) [38,10]. true => _t27 | ~_t21 [ SNF ] % 39.02/39.29 (1,1) [410,10]. true => ~_t84 | ~p4 | ~p104 [ SNF ] % 39.02/39.29 (45,1) [579,10]. true => ~_t177 | p110 [ SNF ] % 39.02/39.29 (1,1) [3297,10]. true => ~_t223 | p4 [ SNF++, 6 ] % 39.02/39.29 (1,1) [3299,10]. true => ~_t224 | _t21 [ SNF++, 297 ] % 39.02/39.29 (1,1) [3325,10]. true => ~_t237 | _t84 [ SNF++, 411 ] % 39.02/39.29 (45,1) [3429,10]. true => ~_t265 | _t177 [ SNF++, 580 ] % 39.02/39.29 (1,1) [5134,10]. true => ~_t224 | _t27 [ LRES, 38, 3299, ~_t21 ] % 39.02/39.29 (1,1) [5145,10]. true => ~_t224 | _t26 [ LRES, 36, 3299, ~_t21 ] % 39.02/39.29 (1,1) [5156,10]. true => ~_t224 | _t25 [ LRES, 34, 3299, ~_t21 ] % 39.02/39.29 (1,1) [5167,10]. true => ~_t224 | _t24 [ LRES, 32, 3299, ~_t21 ] % 39.02/39.29 (1,1) [5178,10]. true => ~_t224 | _t23 [ LRES, 30, 3299, ~_t21 ] % 39.02/39.29 (1,1) [5189,10]. true => ~_t224 | _t22 [ LRES, 28, 3299, ~_t21 ] % 39.02/39.29 (1,1) [8450,10]. true => ~_t84 | ~_t27 | ~p4 | ~p105 [ LRES, 410, 37, ~p104 ] % 39.02/39.29 (1,1) [12204,10]. true => ~_t84 | ~_t27 | ~_t26 | ~p4 | ~p106 [ LRES, 8450, 35, ~p105 ] % 39.02/39.29 (1,1) [20992,10]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~p4 | ~p107 [ LRES, 12204, 33, ~p106 ] % 39.02/39.29 (1,1) [41653,10]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~p4 | ~p108 [ LRES, 20992, 31, ~p107 ] % 39.02/39.29 (1,1) [47080,10]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 | ~p4 | ~p109 [ LRES, 41653, 29, ~p108 ] % 39.02/39.29 (1,1) [67191,10]. true => ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 | ~_t22 | ~p4 | ~p110 [ LRES, 47080, 27, ~p109 ] % 39.02/39.29 (45,1) [85625,10]. true => ~_t177 | ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 | ~_t22 | ~p4 [ LRES, 67191, 579, ~p110 ] % 39.02/39.29 (45,1) [97774,10]. true => ~_t223 | ~_t177 | ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 | ~_t22 [ LRES, 85625, 3297, ~p4 ] % 39.02/39.29 (45,1) [98056,10]. true => ~_t224 | ~_t223 | ~_t177 | ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 | ~_t23 [ LRES, 97774, 5189, ~_t22 ] [ Backward Subsumption, 98093 ] % 39.02/39.29 (45,1) [98093,10]. true => ~_t224 | ~_t223 | ~_t177 | ~_t84 | ~_t27 | ~_t26 | ~_t25 | ~_t24 [ LRES, 98056, 5178, ~_t23 ] [ Backward Subsumption, 98105 ] % 39.02/39.29 (45,1) [98105,10]. true => ~_t224 | ~_t223 | ~_t177 | ~_t84 | ~_t27 | ~_t26 | ~_t25 [ LRES, 98093, 5167, ~_t24 ] [ Backward Subsumption, 98159 ] % 39.02/39.29 (45,1) [98159,10]. true => ~_t224 | ~_t223 | ~_t177 | ~_t84 | ~_t27 | ~_t26 [ LRES, 98105, 5156, ~_t25 ] [ Backward Subsumption, 98160 ] % 39.02/39.29 (45,1) [98160,10]. true => ~_t224 | ~_t223 | ~_t177 | ~_t84 | ~_t27 [ LRES, 98159, 5145, ~_t26 ] [ Backward Subsumption, 98161 ] % 39.02/39.29 (45,1) [98161,10]. true => ~_t224 | ~_t223 | ~_t177 | ~_t84 [ LRES, 98160, 5134, ~_t27 ] % 39.02/39.29 (45,1) [98162,10]. true => ~_t237 | ~_t224 | ~_t223 | ~_t177 [ LRES, 98161, 3325, ~_t84 ] % 39.02/39.29 (45,1) [98163,10]. true => ~_t265 | ~_t237 | ~_t224 | ~_t223 [ LRES, 98162, 3429, ~_t177 ] % 39.02/39.29 % SZS output end Refutation % 0.50/39.30 % KSP exiting %------------------------------------------------------------------------------