%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP063_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n024.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:56 PM UTC 2026 % Result : Theorem 20.94s 21.19s % Output : Refutation 21.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : SYP063_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.07 % Command : run_ksp %s % 0.07/0.25 % Computer : n024.cluster.edu % 0.07/0.25 % Model : x86_64 x86_64 % 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.25 % Memory : 8042.1875MB % 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.25 % CPULimit : 300 % 0.07/0.25 % WCLimit : 300 % 0.07/0.25 % DateTime : Mon May 4 12:02:41 EDT 2026 % 0.07/0.25 % CPUTime : % 0.23/0.43 ----KSP format--- % 0.23/0.43 set(box,SYM). % 0.23/0.43 usable(formulas). % 0.23/0.43 true. % 0.23/0.43 end_of_list. % 0.23/0.43 sos(formulas). % 0.23/0.43 ~ (~ ( 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.23/0.43 end_of_list. % 0.23/0.43 ----------------- % 0.23/0.43 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.FxOzyMKCzD/theBenchmark.ksp % 20.94/21.19 % 20.94/21.19 % SZS status Theorem % 20.94/21.19 % 20.94/21.19 ***************** % 20.94/21.19 FOUND PROOF 1 % 20.94/21.19 ***************** % 20.94/21.19 % SZS output start Refutation % 20.94/21.19 % 20.94/21.19 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 20.94/21.19 (1,1) [4,0]. true => ~_t0 | ~p101 [ SNF ] [ Backward Subsumption, 3508 ] % 20.94/21.19 (1,1) [5,0]. true => ~_t0 | p100 [ SNF ] [ Backward Subsumption, 3507 ] % 20.94/21.19 (1,1) [85,0]. _t1 => box 1 _t2 [ SNF ] [ Backward Subsumption, 3509 ] % 20.94/21.19 (1,1) [86,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 3506 ] % 20.94/21.19 (41,1) [1816,0]. _t170 => ~box 1~ _t171 [ SNF ] [ Backward Subsumption, 3583 ] % 20.94/21.19 (1,1) [1817,0]. true => _t170 | ~_t169 [ SNF ] [ Backward Subsumption, 3576 ] % 20.94/21.19 (1,1) [1823,0]. true => _t169 | ~_t168 | p101 | ~p100 [ SNF ] [ Backward Subsumption, 3525 ] % 20.94/21.19 (1,1) [1859,0]. _t17 => box 1 _t18 [ SNF ] [ Backward Subsumption, 3529 ] % 20.94/21.19 (1,1) [3396,0]. _t20 => box 1 _t21 [ SNF ] [ Backward Subsumption, 3538 ] % 20.94/21.19 (1,1) [3407,0]. _t18 => box 1 _t19 [ SNF ] [ Backward Subsumption, 3527 ] % 20.94/21.19 (1,1) [3428,0]. true => _t17 | ~_t0 [ SNF ] [ Backward Subsumption, 3499 ] % 20.94/21.19 (1,1) [3429,0]. true => _t18 | ~_t0 [ SNF ] [ Backward Subsumption, 3498 ] % 20.94/21.19 (1,1) [3431,0]. true => _t20 | ~_t0 [ SNF ] [ Backward Subsumption, 3496 ] % 20.94/21.19 (1,1) [3461,0]. true => _t168 | ~_t0 [ SNF ] [ Backward Subsumption, 3466 ] % 20.94/21.19 (1,1) [3466,0]. true => _t168 [ Unit Resolution, 3, 3461, _t0 ] [ Modal Level Pure Literal Elimination, _t168 ] % 20.94/21.19 (1,1) [3496,0]. true => _t20 [ Unit Resolution, 3, 3431, _t0 ] [ Modal Level Pure Literal Elimination, _t20 ] % 20.94/21.19 (1,1) [3498,0]. true => _t18 [ Unit Resolution, 3, 3429, _t0 ] [ Modal Level Pure Literal Elimination, _t18 ] % 20.94/21.19 (1,1) [3499,0]. true => _t17 [ Unit Resolution, 3, 3428, _t0 ] [ Modal Level Pure Literal Elimination, _t17 ] % 20.94/21.19 (1,1) [3506,0]. true => _t1 [ Unit Resolution, 3, 86, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 20.94/21.19 (1,1) [3507,0]. true => p100 [ Unit Resolution, 3, 5, _t0 ] [ Modal Level Pure Literal Elimination, p100 ] % 20.94/21.19 (1,1) [3508,0]. true => ~p101 [ Unit Resolution, 3, 4, _t0 ] [ Modal Level Pure Literal Elimination, ~p101 ] % 20.94/21.19 (1,1) [3509,0]. true => box 1 _t2 [ LHS Unit Resolution, 3506, 85, _t1 ] [ SNF++, 5061, _t2 ] % 20.94/21.19 (1,1) [3525,0]. true => _t169 | p101 | ~p100 [ Unit Resolution, 3466, 1823, _t168 ] [ Backward Subsumption, 3530 ] % 20.94/21.19 (1,1) [3527,0]. true => box 1 _t19 [ LHS Unit Resolution, 3498, 3407, _t18 ] [ SNF++, 5083, _t19 ] % 20.94/21.19 (1,1) [3529,0]. true => box 1 _t18 [ LHS Unit Resolution, 3499, 1859, _t17 ] [ SNF++, 5069, _t18 ] % 20.94/21.19 (1,1) [3530,0]. true => _t169 | p101 [ Unit Resolution, 3507, 3525, p100 ] [ Backward Subsumption, 3534 ] % 20.94/21.19 (1,1) [3534,0]. true => _t169 [ Unit Resolution, 3508, 3530, p101 ] [ Modal Level Pure Literal Elimination, _t169 ] % 20.94/21.19 (1,1) [3538,0]. true => box 1 _t21 [ LHS Unit Resolution, 3496, 3396, _t20 ] [ SNF++, 5081, _t21 ] % 20.94/21.19 (1,1) [3576,0]. true => _t170 [ Unit Resolution, 3534, 1817, _t169 ] [ Modal Level Pure Literal Elimination, _t170 ] % 20.94/21.19 (41,1) [3583,0]. true => ~box 1~ _t171 [ LHS Unit Resolution, 3576, 1816, _t170 ] [ SNF++, 5091, _t171 ] % 20.94/21.19 (1,1) [5061,0]. true => box 1 _t320 [ SNF++, 3509 ] % 20.94/21.19 (1,1) [5069,0]. true => box 1 _t298 [ SNF++, 3529 ] % 20.94/21.19 (1,1) [5081,0]. true => box 1 _t244 [ SNF++, 3538 ] % 20.94/21.19 (1,1) [5083,0]. true => box 1 _t294 [ SNF++, 3527 ] % 20.94/21.19 (41,1) [5091,0]. true => ~box 1~ _t283 [ SNF++, 3583 ] % 20.94/21.19 (41,1) [176424,0]. true => false [ GEN1, 5061, 5083, 5081, 5069, 5091, 176418, _t320, _t294, _t244, _t298, _t283 ] % 20.94/21.19 (1,1) [81,1]. _t2 => box 1 _t3 [ SNF ] [ SNF++, 4881, _t3 ] % 20.94/21.19 (1,1) [1606,1]. _t213 => box 1 ~_t19 [ Axiom SYM ] [ SNF++, 4927, ~_t19 ] % 20.94/21.19 (1,1) [1607,1]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 4929, _t21 ] % 20.94/21.19 (41,1) [1814,1]. true => ~_t171 | ~p102 [ SNF ] % 20.94/21.19 (41,1) [1815,1]. true => ~_t171 | p101 [ SNF ] % 20.94/21.19 (1,1) [1836,1]. true => _t213 | _t20 [ Axiom SYM ] % 20.94/21.19 (1,1) [1846,1]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 4933, _t19 ] % 20.94/21.19 (77,1) [3353,1]. _t164 => ~box 1~ _t165 [ SNF ] [ SNF++, 5033, _t165 ] % 20.94/21.19 (1,1) [3354,1]. true => _t164 | ~_t163 [ SNF ] % 20.94/21.19 (1,1) [3360,1]. true => _t163 | ~_t162 | p102 | ~p101 [ SNF ] % 20.94/21.19 (1,1) [3361,1]. true => _t162 | ~_t21 [ SNF ] % 20.94/21.19 (1,1) [3394,1]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 4993, _t20 ] % 20.94/21.19 (1,1) [4881,1]. _t2 => box 1 _t316 [ SNF++, 81 ] % 20.94/21.19 (1,1) [4927,1]. _t213 => box 1 _t293 [ SNF++, 1606 ] % 20.94/21.19 (1,1) [4929,1]. _t20 => box 1 _t244 [ SNF++, 1607 ] % 20.94/21.19 (1,1) [4933,1]. _t18 => box 1 _t294 [ SNF++, 1846 ] % 20.94/21.19 (1,1) [4993,1]. _t19 => box 1 _t290 [ SNF++, 3394 ] % 20.94/21.19 (77,1) [5033,1]. _t164 => ~box 1~ _t281 [ SNF++, 3353 ] % 20.94/21.19 (1,1) [5062,1]. true => ~_t320 | _t2 [ SNF++, 3509 ] % 20.94/21.19 (1,1) [5070,1]. true => ~_t298 | _t18 [ SNF++, 3529 ] % 20.94/21.19 (1,1) [5082,1]. true => ~_t244 | _t21 [ SNF++, 3538 ] % 20.94/21.19 (1,1) [5084,1]. true => ~_t294 | _t19 [ SNF++, 3527 ] % 20.94/21.19 (41,1) [5092,1]. true => ~_t283 | _t171 [ SNF++, 3583 ] % 20.94/21.19 (1,1) [5313,1]. true => ~_t244 | _t162 [ LRES, 3361, 5082, ~_t21 ] % 20.94/21.19 (41,1) [7648,1]. true => ~_t171 | _t163 | ~_t162 | p102 [ LRES, 3360, 1815, ~p101 ] [ Backward Subsumption, 16011 ] % 20.94/21.19 (1,1) [8509,1]. true => ~_t213 | ~_t164 | ~_t18 [ GEN3, 4933, 4927, 6606, 5033, _t294, _t293, _t281 ] % 20.94/21.19 (1,1) [10518,1]. true => ~_t298 | ~_t213 | ~_t164 [ LRES, 8509, 5070, ~_t18 ] % 20.94/21.19 (41,1) [16011,1]. true => ~_t171 | _t163 | ~_t162 [ LRES, 7648, 1814, p102 ] % 20.94/21.19 (41,1) [16027,1]. true => ~_t244 | ~_t171 | _t163 [ LRES, 16011, 5313, ~_t162 ] % 20.94/21.19 (41,1) [16035,1]. true => ~_t244 | ~_t171 | _t164 [ LRES, 16027, 3354, _t163 ] % 20.94/21.19 (41,1) [16101,1]. true => ~_t298 | ~_t244 | ~_t213 | ~_t171 [ LRES, 16035, 10518, _t164 ] % 20.94/21.19 (41,1) [16775,1]. true => ~_t298 | ~_t283 | ~_t244 | ~_t213 [ LRES, 16101, 5092, ~_t171 ] % 20.94/21.19 (77,1) [141965,1]. true => ~_t164 | ~_t20 | ~_t19 | ~_t2 [ GEN1, 4881, 4929, 4993, 5033, 141882, _t316, _t244, _t290, _t281 ] % 20.94/21.19 (77,1) [142003,1]. true => ~_t320 | ~_t164 | ~_t20 | ~_t19 [ LRES, 141965, 5062, ~_t2 ] % 20.94/21.19 (77,1) [151361,1]. true => ~_t320 | ~_t294 | ~_t164 | ~_t20 [ LRES, 142003, 5084, ~_t19 ] % 20.94/21.19 (77,1) [157401,1]. true => ~_t320 | ~_t294 | _t213 | ~_t164 [ LRES, 151361, 1836, ~_t20 ] % 20.94/21.19 (77,1) [161043,1]. true => ~_t320 | ~_t294 | ~_t244 | _t213 | ~_t171 [ LRES, 157401, 16035, ~_t164 ] % 20.94/21.19 (77,1) [161404,1]. true => ~_t320 | ~_t294 | ~_t283 | ~_t244 | _t213 [ LRES, 161043, 5092, ~_t171 ] % 20.94/21.19 (77,1) [176418,1]. true => ~_t320 | ~_t298 | ~_t294 | ~_t283 | ~_t244 [ LRES, 161404, 16775, _t213 ] % 20.94/21.19 (1,1) [41,2]. _t183 => box 1 ~_t8 [ Axiom SYM ] [ SNF++, 4693, ~_t8 ] % 20.94/21.19 (1,1) [42,2]. _t9 => box 1 _t10 [ SNF ] [ SNF++, 4695, _t10 ] % 20.94/21.19 (1,1) [48,2]. true => _t183 | _t9 [ Axiom SYM ] % 20.94/21.19 (1,1) [54,2]. _t185 => box 1 ~_t6 [ Axiom SYM ] [ SNF++, 4697, ~_t6 ] % 20.94/21.19 (1,1) [55,2]. _t7 => box 1 _t8 [ SNF ] [ SNF++, 4699, _t8 ] % 20.94/21.19 (1,1) [62,2]. true => _t185 | _t7 [ Axiom SYM ] % 20.94/21.19 (1,1) [65,2]. _t187 => box 1 ~_t4 [ Axiom SYM ] [ SNF++, 4701, ~_t4 ] % 20.94/21.19 (1,1) [66,2]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 4703, _t6 ] % 20.94/21.19 (1,1) [73,2]. true => _t187 | _t5 [ Axiom SYM ] % 20.94/21.19 (1,1) [74,2]. _t3 => box 1 _t4 [ SNF ] [ SNF++, 4705, _t4 ] % 20.94/21.19 (33,1) [1552,2]. _t158 => ~box 1~ _t159 [ SNF ] [ SNF++, 4849, _t159 ] % 20.94/21.19 (1,1) [1553,2]. true => _t158 | ~_t157 [ SNF ] % 20.94/21.19 (1,1) [1559,2]. true => _t157 | ~_t156 | p103 | ~p102 [ SNF ] % 20.94/21.19 (1,1) [1560,2]. true => _t156 | ~_t21 [ SNF ] % 20.94/21.19 (1,1) [3090,2]. _t20 => box 1 _t21 [ SNF ] [ SNF++, 4813, _t21 ] % 20.94/21.19 (77,1) [3351,2]. true => ~_t165 | ~p103 [ SNF ] % 20.94/21.19 (77,1) [3352,2]. true => ~_t165 | p102 [ SNF ] % 20.94/21.19 (1,1) [4693,2]. _t183 => box 1 _t295 [ SNF++, 41 ] % 20.94/21.19 (1,1) [4695,2]. _t9 => box 1 _t288 [ SNF++, 42 ] % 20.94/21.19 (1,1) [4697,2]. _t185 => box 1 _t303 [ SNF++, 54 ] % 20.94/21.19 (1,1) [4699,2]. _t7 => box 1 _t296 [ SNF++, 55 ] % 20.94/21.19 (1,1) [4701,2]. _t187 => box 1 _t311 [ SNF++, 65 ] % 20.94/21.19 (1,1) [4703,2]. _t5 => box 1 _t304 [ SNF++, 66 ] % 20.94/21.19 (1,1) [4705,2]. _t3 => box 1 _t312 [ SNF++, 74 ] % 20.94/21.19 (1,1) [4813,2]. _t20 => box 1 _t244 [ SNF++, 3090 ] % 20.94/21.19 (33,1) [4849,2]. _t158 => ~box 1~ _t279 [ SNF++, 1552 ] % 20.94/21.19 (1,1) [4882,2]. true => ~_t316 | _t3 [ SNF++, 81 ] % 20.94/21.19 (1,1) [4928,2]. true => ~_t293 | ~_t19 [ SNF++, 1606 ] % 20.94/21.19 (1,1) [4930,2]. true => ~_t244 | _t21 [ SNF++, 1607 ] % 20.94/21.19 (1,1) [4934,2]. true => ~_t294 | _t19 [ SNF++, 1846 ] % 20.94/21.19 (1,1) [4994,2]. true => ~_t290 | _t20 [ SNF++, 3394 ] % 20.94/21.19 (77,1) [5034,2]. true => ~_t281 | _t165 [ SNF++, 3353 ] % 20.94/21.19 (1,1) [5257,2]. true => ~_t244 | _t156 [ LRES, 1560, 4930, ~_t21 ] % 20.94/21.19 (1,1) [6606,2]. true => ~_t294 | ~_t293 [ LRES, 4928, 4934, ~_t19 ] % 20.94/21.19 (1,1) [8188,2]. true => ~_t183 | ~_t158 | ~_t7 [ GEN3, 4699, 4693, 6551, 4849, _t296, _t295, _t279 ] % 20.94/21.19 (1,1) [8276,2]. true => ~_t185 | ~_t158 | ~_t5 [ GEN3, 4703, 4697, 6561, 4849, _t304, _t303, _t279 ] % 20.94/21.19 (1,1) [8360,2]. true => ~_t187 | ~_t158 | ~_t3 [ GEN3, 4705, 4701, 6567, 4849, _t312, _t311, _t279 ] % 20.94/21.19 (1,1) [11153,2]. true => _t185 | ~_t183 | ~_t158 [ LRES, 8188, 62, ~_t7 ] % 20.94/21.19 (1,1) [11389,2]. true => _t187 | ~_t185 | ~_t158 [ LRES, 8276, 73, ~_t5 ] % 20.94/21.19 (1,1) [11636,2]. true => ~_t316 | ~_t187 | ~_t158 [ LRES, 8360, 4882, ~_t3 ] % 20.94/21.19 (77,1) [27083,2]. true => ~_t165 | _t157 | ~_t156 | p103 [ LRES, 1559, 3352, ~p102 ] [ Backward Subsumption, 39395 ] % 20.94/21.19 (33,1) [36693,2]. true => ~_t158 | ~_t20 | ~_t9 [ GEN1, 4695, 4813, 4849, 36638, _t288, _t244, _t279 ] % 20.94/21.19 (33,1) [36699,2]. true => _t183 | ~_t158 | ~_t20 [ LRES, 36693, 48, ~_t9 ] % 20.94/21.19 (33,1) [36717,2]. true => ~_t290 | _t183 | ~_t158 [ LRES, 36699, 4994, ~_t20 ] % 20.94/21.19 (77,1) [39395,2]. true => ~_t165 | _t157 | ~_t156 [ LRES, 27083, 3351, p103 ] % 20.94/21.19 (77,1) [39414,2]. true => ~_t244 | ~_t165 | _t157 [ LRES, 39395, 5257, ~_t156 ] % 20.94/21.19 (77,1) [39420,2]. true => ~_t244 | ~_t165 | _t158 [ LRES, 39414, 1553, _t157 ] % 20.94/21.19 (77,1) [39492,2]. true => ~_t290 | ~_t244 | _t183 | ~_t165 [ LRES, 39420, 36717, _t158 ] % 20.94/21.19 (77,1) [39499,2]. true => ~_t244 | _t185 | ~_t183 | ~_t165 [ LRES, 39420, 11153, _t158 ] % 20.94/21.19 (77,1) [39501,2]. true => ~_t244 | _t187 | ~_t185 | ~_t165 [ LRES, 39420, 11389, _t158 ] % 20.94/21.19 (77,1) [39503,2]. true => ~_t316 | ~_t244 | ~_t187 | ~_t165 [ LRES, 39420, 11636, _t158 ] % 20.94/21.19 (77,1) [70193,2]. true => ~_t316 | ~_t281 | ~_t244 | ~_t187 [ LRES, 39503, 5034, ~_t165 ] % 20.94/21.19 (77,1) [70247,2]. true => ~_t281 | ~_t244 | _t187 | ~_t185 [ LRES, 39501, 5034, ~_t165 ] % 20.94/21.19 (77,1) [70322,2]. true => ~_t281 | ~_t244 | _t185 | ~_t183 [ LRES, 39499, 5034, ~_t165 ] % 20.94/21.19 (77,1) [70417,2]. true => ~_t290 | ~_t281 | ~_t244 | _t183 [ LRES, 39492, 5034, ~_t165 ] % 20.94/21.19 (77,1) [141508,2]. true => ~_t290 | ~_t281 | ~_t244 | _t185 [ LRES, 70322, 70417, ~_t183 ] % 20.94/21.19 (77,1) [141667,2]. true => ~_t290 | ~_t281 | ~_t244 | _t187 [ LRES, 141508, 70247, _t185 ] % 20.94/21.19 (77,1) [141882,2]. true => ~_t316 | ~_t290 | ~_t281 | ~_t244 [ LRES, 141667, 70193, _t187 ] % 20.94/21.19 (1,1) [30,3]. _t10 => box 1 p4 [ SNF ] [ SNF++, 4525, p4 ] % 20.94/21.19 (33,1) [1550,3]. true => ~_t159 | ~p104 [ SNF ] % 20.94/21.19 (33,1) [1551,3]. true => ~_t159 | p103 [ SNF ] % 20.94/21.19 (69,1) [3026,3]. _t152 => ~box 1~ _t153 [ SNF ] [ SNF++, 4671, _t153 ] % 20.94/21.19 (1,1) [3027,3]. true => _t152 | ~_t151 [ SNF ] % 20.94/21.19 (1,1) [3033,3]. true => _t151 | ~_t150 | p104 | ~p103 [ SNF ] % 20.94/21.19 (1,1) [3034,3]. true => _t150 | ~_t21 [ SNF ] % 20.94/21.19 (1,1) [4525,3]. _t10 => box 1 _t221 [ SNF++, 30 ] % 20.94/21.19 (69,1) [4671,3]. _t152 => ~box 1~ _t277 [ SNF++, 3026 ] % 20.94/21.19 (1,1) [4694,3]. true => ~_t295 | ~_t8 [ SNF++, 41 ] % 20.94/21.19 (1,1) [4696,3]. true => ~_t288 | _t10 [ SNF++, 42 ] % 20.94/21.19 (1,1) [4698,3]. true => ~_t303 | ~_t6 [ SNF++, 54 ] % 20.94/21.19 (1,1) [4700,3]. true => ~_t296 | _t8 [ SNF++, 55 ] % 20.94/21.19 (1,1) [4702,3]. true => ~_t311 | ~_t4 [ SNF++, 65 ] % 20.94/21.19 (1,1) [4704,3]. true => ~_t304 | _t6 [ SNF++, 66 ] % 20.94/21.19 (1,1) [4706,3]. true => ~_t312 | _t4 [ SNF++, 74 ] % 20.94/21.19 (1,1) [4814,3]. true => ~_t244 | _t21 [ SNF++, 3090 ] % 20.94/21.19 (33,1) [4850,3]. true => ~_t279 | _t159 [ SNF++, 1552 ] % 20.94/21.19 (1,1) [5893,3]. true => ~_t244 | _t150 [ LRES, 3034, 4814, ~_t21 ] % 20.94/21.19 (1,1) [6551,3]. true => ~_t296 | ~_t295 [ LRES, 4694, 4700, ~_t8 ] % 20.94/21.19 (1,1) [6561,3]. true => ~_t304 | ~_t303 [ LRES, 4698, 4704, ~_t6 ] % 20.94/21.19 (1,1) [6567,3]. true => ~_t312 | ~_t311 [ LRES, 4702, 4706, ~_t4 ] % 20.94/21.19 (69,1) [9047,3]. true => ~_t152 | ~_t10 [ GEN1, 4525, 4671, 7530, _t221, _t277 ] % 20.94/21.19 (69,1) [9351,3]. true => ~_t288 | ~_t152 [ LRES, 9047, 4696, ~_t10 ] % 20.94/21.19 (33,1) [24482,3]. true => ~_t159 | _t151 | ~_t150 | p104 [ LRES, 3033, 1551, ~p103 ] [ Backward Subsumption, 36452 ] % 20.94/21.19 (33,1) [36452,3]. true => ~_t159 | _t151 | ~_t150 [ LRES, 24482, 1550, p104 ] % 20.94/21.19 (33,1) [36470,3]. true => ~_t244 | ~_t159 | _t151 [ LRES, 36452, 5893, ~_t150 ] % 20.94/21.19 (33,1) [36472,3]. true => ~_t244 | ~_t159 | _t152 [ LRES, 36470, 3027, _t151 ] % 20.94/21.19 (69,1) [36531,3]. true => ~_t288 | ~_t244 | ~_t159 [ LRES, 36472, 9351, _t152 ] % 20.94/21.19 (69,1) [36638,3]. true => ~_t288 | ~_t279 | ~_t244 [ LRES, 36531, 4850, ~_t159 ] % 21.23/21.43 (69,1) [3023,4]. true => ~_t153 | ~p4 [ SNF ] % 21.23/21.43 (1,1) [4526,4]. true => ~_t221 | p4 [ SNF++, 30 ] % 21.23/21.43 (69,1) [4672,4]. true => ~_t277 | _t153 [ SNF++, 3026 ] % 21.23/21.43 (69,1) [6352,4]. true => ~_t221 | ~_t153 [ LRES, 3023, 4526, ~p4 ] % 21.23/21.43 (69,1) [7530,4]. true => ~_t277 | ~_t221 [ LRES, 6352, 4672, ~_t153 ] % 21.23/21.43 % SZS output end Refutation % 21.23/21.44 % KSP exiting %------------------------------------------------------------------------------