%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP113_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n010.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 5 07:13:00 PM UTC 2026 % Result : Theorem 4.26s 4.41s % Output : Refutation 4.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SYP113_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.15/0.33 % Computer : n010.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Mon May 4 17:47:21 EDT 2026 % 0.15/0.33 % CPUTime : % 0.37/0.59 ----KSP format--- % 0.37/0.59 set(box,REF). % 0.37/0.59 usable(formulas). % 0.37/0.59 true. % 0.37/0.59 end_of_list. % 0.37/0.59 sos(formulas). % 0.37/0.59 ~ ([] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( p1 & p2 & p3 & p4 & p5 & p6 & p7 & p8 & p9 & p10 & p11 & p12 & p13 & p14 & p15 & p16 & p17 & p18 & p19 & p20 & p21 & p22 & p23 & p24 & p25 & p26 & p27 & p28 & p29 & p30 & p31 & p32 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( $false | <> ( ( p1 <-> p2 ) ) ) | [] ( p3 ) | <> ( <> ( ( p2 <-> p3 ) ) ) ) | [] ( p4 ) | <> ( <> ( <> ( ( p3 <-> p4 ) ) ) ) ) | [] ( p5 ) | <> ( <> ( <> ( <> ( ( p4 <-> p5 ) ) ) ) ) ) | [] ( p6 ) | <> ( <> ( <> ( <> ( <> ( ( p5 <-> p6 ) ) ) ) ) ) ) | [] ( p7 ) | <> ( <> ( <> ( <> ( <> ( <> ( ( p6 <-> p7 ) ) ) ) ) ) ) ) | [] ( p8 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p7 <-> p8 ) ) ) ) ) ) ) ) ) | [] ( p9 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p8 <-> p9 ) ) ) ) ) ) ) ) ) ) | [] ( p10 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p9 <-> p10 ) ) ) ) ) ) ) ) ) ) ) | [] ( p11 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p10 <-> p11 ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p12 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p11 <-> p12 ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p13 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p12 <-> p13 ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p14 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p13 <-> p14 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p15 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p14 <-> p15 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p16 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p15 <-> p16 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p17 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p16 <-> p17 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p18 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p17 <-> p18 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p19 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p18 <-> p19 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p20 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p19 <-> p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p21 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p20 <-> p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p22 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p21 <-> p22 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p23 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p22 <-> p23 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p24 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p23 <-> p24 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p25 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p24 <-> p25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p26 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p25 <-> p26 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p27 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p26 <-> p27 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p28 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p27 <-> p28 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p29 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p28 <-> p29 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p30 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p29 <-> p30 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p31 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p30 <-> p31 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p32 ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ( p31 <-> p1 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | [] ( p33 ) | [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( [] ( ~ ( p2 ) & ~ ( p4 ) & ~ ( p6 ) & ~ ( p8 ) & ~ ( p10 ) & ~ ( p12 ) & ~ ( p14 ) & ~ ( p16 ) & ~ ( p18 ) & ~ ( p20 ) & ~ ( p22 ) & ~ ( p24 ) & ~ ( p26 ) & ~ ( p28 ) & ~ ( p30 ) & ~ ( p32 ) & ~ ( p34 ) & ~ ( p36 ) & ~ ( p38 ) & ~ ( p40 ) & ~ ( p42 ) & ~ ( p44 ) & ~ ( p46 ) & ~ ( p48 ) & ~ ( p50 ) & ~ ( p52 ) & ~ ( p54 ) & ~ ( p56 ) & ~ ( p58 ) & ~ ( p60 ) & ~ ( p62 ) & ~ ( p64 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ). % 0.37/0.59 end_of_list. % 0.37/0.59 ----------------- % 0.37/0.59 ksp -tstp -pproof -early_ple -mlple -ord -snf++ -unit -lhs_unit -fsub -bsub -limited_reuse_renaming -bnfsimp -maxproof 1 -populate_max_lit_positive -short -global2local -i /export/starexec/sandbox/tmp/tmp.dVhg43m1kw/theBenchmark.ksp % 4.26/4.41 % 4.26/4.41 % SZS status Theorem % 4.26/4.41 % 4.26/4.41 ***************** % 4.26/4.41 FOUND PROOF 1 % 4.26/4.41 ***************** % 4.26/4.41 % SZS output start Refutation % 4.26/4.41 % 4.26/4.41 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 4.26/4.41 (1,1) [27595,0]. true => _t2 | ~_t1 [ Axiom T ] [ Backward Subsumption, 28928 ] % 4.26/4.41 (1,1) [27597,0]. true => _t4 | ~_t3 [ Axiom T ] [ Backward Subsumption, 28934 ] % 4.26/4.41 (1,1) [27599,0]. true => _t5 | ~_t4 [ Axiom T ] [ Backward Subsumption, 28942 ] % 4.26/4.41 (1,1) [27601,0]. true => _t6 | ~_t5 [ Axiom T ] [ Backward Subsumption, 28944 ] % 4.26/4.41 (1,1) [27603,0]. true => _t7 | ~_t6 [ Axiom T ] [ Backward Subsumption, 28953 ] % 4.26/4.41 (1,1) [27605,0]. true => _t8 | ~_t7 [ Axiom T ] [ Backward Subsumption, 28963 ] % 4.26/4.41 (1,1) [27607,0]. true => _t9 | ~_t8 [ Axiom T ] [ Backward Subsumption, 28974 ] % 4.26/4.41 (1,1) [27609,0]. true => _t10 | ~_t9 [ Axiom T ] [ Backward Subsumption, 28976 ] % 4.26/4.41 (1,1) [27611,0]. true => _t11 | ~_t10 [ Axiom T ] [ Backward Subsumption, 28992 ] % 4.26/4.41 (1,1) [27613,0]. true => _t12 | ~_t11 [ Axiom T ] [ Backward Subsumption, 29000 ] % 4.26/4.41 (1,1) [27615,0]. true => _t13 | ~_t12 [ Axiom T ] [ Backward Subsumption, 29015 ] % 4.26/4.41 (1,1) [27617,0]. true => _t14 | ~_t13 [ Axiom T ] [ Backward Subsumption, 29034 ] % 4.26/4.41 (1,1) [27619,0]. true => _t15 | ~_t14 [ Axiom T ] [ Backward Subsumption, 29052 ] % 4.26/4.41 (1,1) [27621,0]. true => _t16 | ~_t15 [ Axiom T ] [ Backward Subsumption, 29054 ] % 4.26/4.41 (1,1) [27623,0]. true => _t17 | ~_t16 [ Axiom T ] [ Backward Subsumption, 29079 ] % 4.26/4.41 (1,1) [27625,0]. true => _t18 | ~_t17 [ Axiom T ] [ Backward Subsumption, 29101 ] % 4.26/4.41 (1,1) [27627,0]. true => _t19 | ~_t18 [ Axiom T ] [ Backward Subsumption, 29110 ] % 4.26/4.41 (1,1) [27629,0]. true => _t20 | ~_t19 [ Axiom T ] [ Backward Subsumption, 29139 ] % 4.26/4.41 (1,1) [27631,0]. true => _t21 | ~_t20 [ Axiom T ] [ Backward Subsumption, 29164 ] % 4.26/4.41 (1,1) [27633,0]. true => _t22 | ~_t21 [ Axiom T ] [ Backward Subsumption, 29189 ] % 4.26/4.41 (1,1) [27635,0]. true => _t23 | ~_t22 [ Axiom T ] [ Backward Subsumption, 29191 ] % 4.26/4.41 (1,1) [27637,0]. true => _t24 | ~_t23 [ Axiom T ] [ Backward Subsumption, 29226 ] % 4.26/4.41 (1,1) [27639,0]. true => _t25 | ~_t24 [ Axiom T ] [ Backward Subsumption, 29258 ] % 4.26/4.41 (1,1) [27641,0]. true => _t26 | ~_t25 [ Axiom T ] [ Backward Subsumption, 29266 ] % 4.26/4.41 (1,1) [27643,0]. true => _t27 | ~_t26 [ Axiom T ] [ Backward Subsumption, 29306 ] % 4.26/4.41 (1,1) [27645,0]. true => _t28 | ~_t27 [ Axiom T ] [ Backward Subsumption, 29341 ] % 4.26/4.41 (1,1) [27647,0]. true => _t29 | ~_t28 [ Axiom T ] [ Backward Subsumption, 29349 ] % 4.26/4.41 (1,1) [27649,0]. true => _t30 | ~_t29 [ Axiom T ] [ Backward Subsumption, 29389 ] % 4.26/4.41 (1,1) [27651,0]. true => _t31 | ~_t30 [ Axiom T ] [ Backward Subsumption, 29416 ] % 4.26/4.41 (1,1) [27653,0]. true => _t32 | ~_t31 [ Axiom T ] [ Backward Subsumption, 29448 ] % 4.26/4.41 (1,1) [27655,0]. true => _t33 | ~_t32 [ Axiom T ] [ Backward Subsumption, 29482 ] % 4.26/4.41 (1,1) [27657,0]. true => _t34 | ~_t33 [ Axiom T ] [ Backward Subsumption, 29514 ] % 4.26/4.41 (1,1) [27658,0]. true => ~_t35 | p31 | p1 [ Axiom T ] [ Backward Subsumption, 29606 ] % 4.26/4.41 (1,1) [27659,0]. true => _t35 | ~_t34 [ Axiom T ] [ Backward Subsumption, 29563 ] % 4.26/4.41 (1,1) [27660,0]. true => ~_t36 | ~p31 | ~p1 [ Axiom T ] [ Backward Subsumption, 29580 ] % 4.26/4.41 (1,1) [27661,0]. true => _t36 | ~_t34 [ Axiom T ] [ Backward Subsumption, 29562 ] % 4.26/4.41 (1,1) [27662,0]. true => _t3 | ~_t2 [ Axiom T ] [ Backward Subsumption, 28933 ] % 4.26/4.41 (1,1) [27664,0]. true => _t38 | ~_t37 [ Axiom T ] [ Backward Subsumption, 28937 ] % 4.26/4.41 (1,1) [27666,0]. true => _t40 | ~_t39 [ Axiom T ] [ Backward Subsumption, 28949 ] % 4.26/4.41 (1,1) [27668,0]. true => _t41 | ~_t40 [ Axiom T ] [ Backward Subsumption, 28951 ] % 4.26/4.41 (1,1) [27670,0]. true => _t42 | ~_t41 [ Axiom T ] [ Backward Subsumption, 28961 ] % 4.26/4.41 (1,1) [27672,0]. true => _t43 | ~_t42 [ Axiom T ] [ Backward Subsumption, 28970 ] % 4.26/4.41 (1,1) [27674,0]. true => _t44 | ~_t43 [ Axiom T ] [ Backward Subsumption, 28978 ] % 4.26/4.41 (1,1) [27676,0]. true => _t45 | ~_t44 [ Axiom T ] [ Backward Subsumption, 28994 ] % 4.26/4.41 (1,1) [27678,0]. true => _t46 | ~_t45 [ Axiom T ] [ Backward Subsumption, 29009 ] % 4.26/4.41 (1,1) [27680,0]. true => _t47 | ~_t46 [ Axiom T ] [ Backward Subsumption, 29011 ] % 4.26/4.41 (1,1) [27682,0]. true => _t48 | ~_t47 [ Axiom T ] [ Backward Subsumption, 29032 ] % 4.26/4.41 (1,1) [27684,0]. true => _t49 | ~_t48 [ Axiom T ] [ Backward Subsumption, 29041 ] % 4.26/4.41 (1,1) [27686,0]. true => _t50 | ~_t49 [ Axiom T ] [ Backward Subsumption, 29063 ] % 4.26/4.41 (1,1) [27688,0]. true => _t51 | ~_t50 [ Axiom T ] [ Backward Subsumption, 29083 ] % 4.26/4.41 (1,1) [27690,0]. true => _t52 | ~_t51 [ Axiom T ] [ Backward Subsumption, 29103 ] % 4.26/4.41 (1,1) [27692,0]. true => _t53 | ~_t52 [ Axiom T ] [ Backward Subsumption, 29124 ] % 4.26/4.41 (1,1) [27694,0]. true => _t54 | ~_t53 [ Axiom T ] [ Backward Subsumption, 29126 ] % 4.26/4.41 (1,1) [27696,0]. true => _t55 | ~_t54 [ Axiom T ] [ Backward Subsumption, 29158 ] % 4.26/4.41 (1,1) [27698,0]. true => _t56 | ~_t55 [ Axiom T ] [ Backward Subsumption, 29172 ] % 4.26/4.41 (1,1) [27700,0]. true => _t57 | ~_t56 [ Axiom T ] [ Backward Subsumption, 29200 ] % 4.26/4.41 (1,1) [27702,0]. true => _t58 | ~_t57 [ Axiom T ] [ Backward Subsumption, 29220 ] % 4.26/4.41 (1,1) [27704,0]. true => _t59 | ~_t58 [ Axiom T ] [ Backward Subsumption, 29247 ] % 4.26/4.41 (1,1) [27706,0]. true => _t60 | ~_t59 [ Axiom T ] [ Backward Subsumption, 29282 ] % 4.26/4.41 (1,1) [27708,0]. true => _t61 | ~_t60 [ Axiom T ] [ Backward Subsumption, 29314 ] % 4.26/4.41 (1,1) [27710,0]. true => _t62 | ~_t61 [ Axiom T ] [ Backward Subsumption, 29345 ] % 4.26/4.41 (1,1) [27712,0]. true => _t63 | ~_t62 [ Axiom T ] [ Backward Subsumption, 29347 ] % 4.26/4.41 (1,1) [27714,0]. true => _t64 | ~_t63 [ Axiom T ] [ Backward Subsumption, 29391 ] % 4.26/4.41 (1,1) [27716,0]. true => _t65 | ~_t64 [ Axiom T ] [ Backward Subsumption, 29430 ] % 4.26/4.41 (1,1) [27718,0]. true => _t66 | ~_t65 [ Axiom T ] [ Backward Subsumption, 29467 ] % 4.26/4.41 (1,1) [27720,0]. true => _t67 | ~_t66 [ Axiom T ] [ Backward Subsumption, 29502 ] % 4.26/4.41 (1,1) [27722,0]. true => _t68 | ~_t67 [ Axiom T ] [ Backward Subsumption, 29504 ] % 4.26/4.41 (1,1) [27724,0]. true => _t69 | ~_t68 [ Axiom T ] [ Backward Subsumption, 29556 ] % 4.26/4.41 (1,1) [27725,0]. true => ~_t70 | p31 | p30 [ Axiom T ] [ Backward Subsumption, 29643 ] % 4.26/4.41 (1,1) [27726,0]. true => _t70 | ~_t69 [ Axiom T ] [ Backward Subsumption, 29603 ] % 4.26/4.41 (1,1) [27727,0]. true => ~_t71 | ~p31 | ~p30 [ Axiom T ] [ Backward Subsumption, 29615 ] % 4.26/4.41 (1,1) [27728,0]. true => _t71 | ~_t69 [ Axiom T ] [ Backward Subsumption, 29602 ] % 4.26/4.41 (1,1) [27729,0]. true => _t39 | ~_t38 [ Axiom T ] [ Backward Subsumption, 28941 ] % 4.26/4.41 (1,1) [27731,0]. true => _t73 | ~_t72 [ Axiom T ] [ Backward Subsumption, 28946 ] % 4.26/4.41 (1,1) [27733,0]. true => _t75 | ~_t74 [ Axiom T ] [ Backward Subsumption, 28958 ] % 4.26/4.41 (1,1) [27735,0]. true => _t76 | ~_t75 [ Axiom T ] [ Backward Subsumption, 28972 ] % 4.26/4.41 (1,1) [27737,0]. true => _t77 | ~_t76 [ Axiom T ] [ Backward Subsumption, 28985 ] % 4.26/4.41 (1,1) [27739,0]. true => _t78 | ~_t77 [ Axiom T ] [ Backward Subsumption, 28987 ] % 4.26/4.41 (1,1) [27741,0]. true => _t79 | ~_t78 [ Axiom T ] [ Backward Subsumption, 29004 ] % 4.26/4.41 (1,1) [27743,0]. true => _t80 | ~_t79 [ Axiom T ] [ Backward Subsumption, 29013 ] % 4.26/4.41 (1,1) [27745,0]. true => _t81 | ~_t80 [ Axiom T ] [ Backward Subsumption, 29030 ] % 4.26/4.41 (1,1) [27747,0]. true => _t82 | ~_t81 [ Axiom T ] [ Backward Subsumption, 29050 ] % 4.26/4.41 (1,1) [27749,0]. true => _t83 | ~_t82 [ Axiom T ] [ Backward Subsumption, 29069 ] % 4.26/4.41 (1,1) [27751,0]. true => _t84 | ~_t83 [ Axiom T ] [ Backward Subsumption, 29071 ] % 4.26/4.41 (1,1) [27753,0]. true => _t85 | ~_t84 [ Axiom T ] [ Backward Subsumption, 29097 ] % 4.26/4.41 (1,1) [27755,0]. true => _t86 | ~_t85 [ Axiom T ] [ Backward Subsumption, 29112 ] % 4.26/4.41 (1,1) [27757,0]. true => _t87 | ~_t86 [ Axiom T ] [ Backward Subsumption, 29132 ] % 4.26/4.41 (1,1) [27759,0]. true => _t88 | ~_t87 [ Axiom T ] [ Backward Subsumption, 29154 ] % 4.26/4.41 (1,1) [27761,0]. true => _t89 | ~_t88 [ Axiom T ] [ Backward Subsumption, 29174 ] % 4.26/4.41 (1,1) [27763,0]. true => _t90 | ~_t89 [ Axiom T ] [ Backward Subsumption, 29206 ] % 4.26/4.41 (1,1) [27765,0]. true => _t91 | ~_t90 [ Axiom T ] [ Backward Subsumption, 29235 ] % 4.26/4.41 (1,1) [27767,0]. true => _t92 | ~_t91 [ Axiom T ] [ Backward Subsumption, 29262 ] % 4.26/4.41 (1,1) [27769,0]. true => _t93 | ~_t92 [ Axiom T ] [ Backward Subsumption, 29264 ] % 4.26/4.41 (1,1) [27771,0]. true => _t94 | ~_t93 [ Axiom T ] [ Backward Subsumption, 29304 ] % 4.26/4.41 (1,1) [27773,0]. true => _t95 | ~_t94 [ Axiom T ] [ Backward Subsumption, 29324 ] % 4.26/4.41 (1,1) [27775,0]. true => _t96 | ~_t95 [ Axiom T ] [ Backward Subsumption, 29357 ] % 4.26/4.41 (1,1) [27777,0]. true => _t97 | ~_t96 [ Axiom T ] [ Backward Subsumption, 29385 ] % 4.26/4.41 (1,1) [27779,0]. true => _t98 | ~_t97 [ Axiom T ] [ Backward Subsumption, 29418 ] % 4.26/4.41 (1,1) [27781,0]. true => _t99 | ~_t98 [ Axiom T ] [ Backward Subsumption, 29461 ] % 4.26/4.41 (1,1) [27783,0]. true => _t100 | ~_t99 [ Axiom T ] [ Backward Subsumption, 29475 ] % 4.26/4.41 (1,1) [27785,0]. true => _t101 | ~_t100 [ Axiom T ] [ Backward Subsumption, 29524 ] % 4.26/4.41 (1,1) [27787,0]. true => _t102 | ~_t101 [ Axiom T ] [ Backward Subsumption, 29545 ] % 4.26/4.41 (1,1) [27789,0]. true => _t103 | ~_t102 [ Axiom T ] [ Backward Subsumption, 29588 ] % 4.26/4.41 (1,1) [27790,0]. true => ~_t104 | p30 | p29 [ Axiom T ] [ Backward Subsumption, 29650 ] % 4.26/4.41 (1,1) [27791,0]. true => _t104 | ~_t103 [ Axiom T ] [ Backward Subsumption, 29636 ] % 4.26/4.41 (1,1) [27792,0]. true => ~_t105 | ~p30 | ~p29 [ Axiom T ] [ Backward Subsumption, 29676 ] % 4.26/4.41 (1,1) [27793,0]. true => _t105 | ~_t103 [ Axiom T ] [ Backward Subsumption, 29635 ] % 4.26/4.41 (1,1) [27794,0]. true => _t74 | ~_t73 [ Axiom T ] [ Backward Subsumption, 28957 ] % 4.26/4.41 (1,1) [27796,0]. true => _t107 | ~_t106 [ Axiom T ] [ Backward Subsumption, 28965 ] % 4.26/4.41 (1,1) [27798,0]. true => _t109 | ~_t108 [ Axiom T ] [ Backward Subsumption, 28983 ] % 4.26/4.41 (1,1) [27800,0]. true => _t110 | ~_t109 [ Axiom T ] [ Backward Subsumption, 28996 ] % 4.26/4.41 (1,1) [27802,0]. true => _t111 | ~_t110 [ Axiom T ] [ Backward Subsumption, 28998 ] % 4.26/4.41 (1,1) [27804,0]. true => _t112 | ~_t111 [ Axiom T ] [ Backward Subsumption, 29017 ] % 4.26/4.41 (1,1) [27806,0]. true => _t113 | ~_t112 [ Axiom T ] [ Backward Subsumption, 29028 ] % 4.26/4.41 (1,1) [27808,0]. true => _t114 | ~_t113 [ Axiom T ] [ Backward Subsumption, 29043 ] % 4.26/4.41 (1,1) [27810,0]. true => _t115 | ~_t114 [ Axiom T ] [ Backward Subsumption, 29059 ] % 4.26/4.41 (1,1) [27812,0]. true => _t116 | ~_t115 [ Axiom T ] [ Backward Subsumption, 29081 ] % 4.26/4.41 (1,1) [27814,0]. true => _t117 | ~_t116 [ Axiom T ] [ Backward Subsumption, 29091 ] % 4.26/4.41 (1,1) [27816,0]. true => _t118 | ~_t117 [ Axiom T ] [ Backward Subsumption, 29118 ] % 4.26/4.41 (1,1) [27818,0]. true => _t119 | ~_t118 [ Axiom T ] [ Backward Subsumption, 29143 ] % 4.26/4.41 (1,1) [27820,0]. true => _t120 | ~_t119 [ Axiom T ] [ Backward Subsumption, 29166 ] % 4.26/4.41 (1,1) [27822,0]. true => _t121 | ~_t120 [ Axiom T ] [ Backward Subsumption, 29168 ] % 4.26/4.41 (1,1) [27824,0]. true => _t122 | ~_t121 [ Axiom T ] [ Backward Subsumption, 29202 ] % 4.26/4.41 (1,1) [27826,0]. true => _t123 | ~_t122 [ Axiom T ] [ Backward Subsumption, 29233 ] % 4.26/4.41 (1,1) [27828,0]. true => _t124 | ~_t123 [ Axiom T ] [ Backward Subsumption, 29241 ] % 4.26/4.41 (1,1) [27830,0]. true => _t125 | ~_t124 [ Axiom T ] [ Backward Subsumption, 29276 ] % 4.26/4.41 (1,1) [27832,0]. true => _t126 | ~_t125 [ Axiom T ] [ Backward Subsumption, 29297 ] % 4.26/4.41 (1,1) [27834,0]. true => _t127 | ~_t126 [ Axiom T ] [ Backward Subsumption, 29336 ] % 4.26/4.41 (1,1) [27836,0]. true => _t128 | ~_t127 [ Axiom T ] [ Backward Subsumption, 29351 ] % 4.26/4.41 (1,1) [27838,0]. true => _t129 | ~_t128 [ Axiom T ] [ Backward Subsumption, 29393 ] % 4.26/4.41 (1,1) [27840,0]. true => _t130 | ~_t129 [ Axiom T ] [ Backward Subsumption, 29414 ] % 4.26/4.41 (1,1) [27842,0]. true => _t131 | ~_t130 [ Axiom T ] [ Backward Subsumption, 29459 ] % 4.26/4.41 (1,1) [27844,0]. true => _t132 | ~_t131 [ Axiom T ] [ Backward Subsumption, 29498 ] % 4.26/4.41 (1,1) [27846,0]. true => _t133 | ~_t132 [ Axiom T ] [ Backward Subsumption, 29506 ] % 4.26/4.41 (1,1) [27848,0]. true => _t134 | ~_t133 [ Axiom T ] [ Backward Subsumption, 29558 ] % 4.26/4.41 (1,1) [27850,0]. true => _t135 | ~_t134 [ Axiom T ] [ Backward Subsumption, 29581 ] % 4.26/4.41 (1,1) [27852,0]. true => _t136 | ~_t135 [ Axiom T ] [ Backward Subsumption, 29625 ] % 4.26/4.41 (1,1) [27853,0]. true => ~_t137 | p29 | p28 [ Axiom T ] [ Backward Subsumption, 29703 ] % 4.26/4.41 (1,1) [27854,0]. true => _t137 | ~_t136 [ Axiom T ] [ Backward Subsumption, 29656 ] % 4.26/4.41 (1,1) [27855,0]. true => ~_t138 | ~p29 | ~p28 [ Axiom T ] [ Backward Subsumption, 29694 ] % 4.26/4.41 (1,1) [27856,0]. true => _t138 | ~_t136 [ Axiom T ] [ Backward Subsumption, 29655 ] % 4.26/4.41 (1,1) [27857,0]. true => _t108 | ~_t107 [ Axiom T ] [ Backward Subsumption, 28969 ] % 4.26/4.41 (1,1) [27859,0]. true => _t140 | ~_t139 [ Axiom T ] [ Backward Subsumption, 28980 ] % 4.26/4.41 (1,1) [27861,0]. true => _t142 | ~_t141 [ Axiom T ] [ Backward Subsumption, 29007 ] % 4.26/4.41 (1,1) [27863,0]. true => _t143 | ~_t142 [ Axiom T ] [ Backward Subsumption, 29022 ] % 4.26/4.41 (1,1) [27865,0]. true => _t144 | ~_t143 [ Axiom T ] [ Backward Subsumption, 29024 ] % 4.26/4.41 (1,1) [27867,0]. true => _t145 | ~_t144 [ Axiom T ] [ Backward Subsumption, 29045 ] % 4.26/4.41 (1,1) [27869,0]. true => _t146 | ~_t145 [ Axiom T ] [ Backward Subsumption, 29065 ] % 4.26/4.41 (1,1) [27871,0]. true => _t147 | ~_t146 [ Axiom T ] [ Backward Subsumption, 29073 ] % 4.26/4.41 (1,1) [27873,0]. true => _t148 | ~_t147 [ Axiom T ] [ Backward Subsumption, 29095 ] % 4.26/4.41 (1,1) [27875,0]. true => _t149 | ~_t148 [ Axiom T ] [ Backward Subsumption, 29120 ] % 4.26/4.41 (1,1) [27877,0]. true => _t150 | ~_t149 [ Axiom T ] [ Backward Subsumption, 29128 ] % 4.26/4.41 (1,1) [27879,0]. true => _t151 | ~_t150 [ Axiom T ] [ Backward Subsumption, 29156 ] % 4.26/4.41 (1,1) [27881,0]. true => _t152 | ~_t151 [ Axiom T ] [ Backward Subsumption, 29185 ] % 4.26/4.41 (1,1) [27883,0]. true => _t153 | ~_t152 [ Axiom T ] [ Backward Subsumption, 29193 ] % 4.26/4.41 (1,1) [27885,0]. true => _t154 | ~_t153 [ Axiom T ] [ Backward Subsumption, 29228 ] % 4.26/4.41 (1,1) [27887,0]. true => _t155 | ~_t154 [ Axiom T ] [ Backward Subsumption, 29243 ] % 4.26/4.41 (1,1) [27889,0]. true => _t156 | ~_t155 [ Axiom T ] [ Backward Subsumption, 29280 ] % 4.26/4.41 (1,1) [27891,0]. true => _t157 | ~_t156 [ Axiom T ] [ Backward Subsumption, 29295 ] % 4.26/4.41 (1,1) [27893,0]. true => _t158 | ~_t157 [ Axiom T ] [ Backward Subsumption, 29330 ] % 4.26/4.41 (1,1) [27895,0]. true => _t159 | ~_t158 [ Axiom T ] [ Backward Subsumption, 29368 ] % 4.26/4.41 (1,1) [27897,0]. true => _t160 | ~_t159 [ Axiom T ] [ Backward Subsumption, 29403 ] % 4.26/4.41 (1,1) [27899,0]. true => _t161 | ~_t160 [ Axiom T ] [ Backward Subsumption, 29436 ] % 4.26/4.41 (1,1) [27901,0]. true => _t162 | ~_t161 [ Axiom T ] [ Backward Subsumption, 29438 ] % 4.26/4.41 (1,1) [27903,0]. true => _t163 | ~_t162 [ Axiom T ] [ Backward Subsumption, 29488 ] % 4.26/4.41 (1,1) [27905,0]. true => _t164 | ~_t163 [ Axiom T ] [ Backward Subsumption, 29531 ] % 4.26/4.41 (1,1) [27907,0]. true => _t165 | ~_t164 [ Axiom T ] [ Backward Subsumption, 29570 ] % 4.26/4.41 (1,1) [27909,0]. true => _t166 | ~_t165 [ Axiom T ] [ Backward Subsumption, 29609 ] % 4.26/4.41 (1,1) [27911,0]. true => _t167 | ~_t166 [ Axiom T ] [ Backward Subsumption, 29611 ] % 4.26/4.41 (1,1) [27913,0]. true => _t168 | ~_t167 [ Axiom T ] [ Backward Subsumption, 29662 ] % 4.26/4.41 (1,1) [27914,0]. true => ~_t169 | p28 | p27 [ Axiom T ] [ Backward Subsumption, 29724 ] % 4.26/4.41 (1,1) [27915,0]. true => _t169 | ~_t168 [ Axiom T ] [ Backward Subsumption, 29691 ] % 4.26/4.41 (1,1) [27916,0]. true => ~_t170 | ~p28 | ~p27 [ Axiom T ] [ Backward Subsumption, 29736 ] % 4.26/4.41 (1,1) [27917,0]. true => _t170 | ~_t168 [ Axiom T ] [ Backward Subsumption, 29690 ] % 4.26/4.41 (1,1) [27918,0]. true => _t141 | ~_t140 [ Axiom T ] [ Backward Subsumption, 28991 ] % 4.26/4.41 (1,1) [27920,0]. true => _t172 | ~_t171 [ Axiom T ] [ Backward Subsumption, 29002 ] % 4.26/4.41 (1,1) [27922,0]. true => _t174 | ~_t173 [ Axiom T ] [ Backward Subsumption, 29037 ] % 4.26/4.41 (1,1) [27924,0]. true => _t175 | ~_t174 [ Axiom T ] [ Backward Subsumption, 29039 ] % 4.26/4.41 (1,1) [27926,0]. true => _t176 | ~_t175 [ Axiom T ] [ Backward Subsumption, 29061 ] % 4.26/4.41 (1,1) [27928,0]. true => _t177 | ~_t176 [ Axiom T ] [ Backward Subsumption, 29075 ] % 4.26/4.41 (1,1) [27930,0]. true => _t178 | ~_t177 [ Axiom T ] [ Backward Subsumption, 29099 ] % 4.26/4.41 (1,1) [27932,0]. true => _t179 | ~_t178 [ Axiom T ] [ Backward Subsumption, 29122 ] % 4.26/4.41 (1,1) [27934,0]. true => _t180 | ~_t179 [ Axiom T ] [ Backward Subsumption, 29145 ] % 4.26/4.41 (1,1) [27936,0]. true => _t181 | ~_t180 [ Axiom T ] [ Backward Subsumption, 29147 ] % 4.26/4.41 (1,1) [27938,0]. true => _t182 | ~_t181 [ Axiom T ] [ Backward Subsumption, 29180 ] % 4.26/4.41 (1,1) [27940,0]. true => _t183 | ~_t182 [ Axiom T ] [ Backward Subsumption, 29195 ] % 4.26/4.41 (1,1) [27942,0]. true => _t184 | ~_t183 [ Axiom T ] [ Backward Subsumption, 29224 ] % 4.26/4.41 (1,1) [27944,0]. true => _t185 | ~_t184 [ Axiom T ] [ Backward Subsumption, 29245 ] % 4.26/4.41 (1,1) [27946,0]. true => _t186 | ~_t185 [ Axiom T ] [ Backward Subsumption, 29274 ] % 4.26/4.41 (1,1) [27948,0]. true => _t187 | ~_t186 [ Axiom T ] [ Backward Subsumption, 29310 ] % 4.26/4.41 (1,1) [27950,0]. true => _t188 | ~_t187 [ Axiom T ] [ Backward Subsumption, 29343 ] % 4.26/4.41 (1,1) [27952,0]. true => _t189 | ~_t188 [ Axiom T ] [ Backward Subsumption, 29374 ] % 4.26/4.41 (1,1) [27954,0]. true => _t190 | ~_t189 [ Axiom T ] [ Backward Subsumption, 29376 ] % 4.26/4.41 (1,1) [27956,0]. true => _t191 | ~_t190 [ Axiom T ] [ Backward Subsumption, 29422 ] % 4.26/4.41 (1,1) [27958,0]. true => _t192 | ~_t191 [ Axiom T ] [ Backward Subsumption, 29463 ] % 4.26/4.41 (1,1) [27960,0]. true => _t193 | ~_t192 [ Axiom T ] [ Backward Subsumption, 29500 ] % 4.26/4.41 (1,1) [27962,0]. true => _t194 | ~_t193 [ Axiom T ] [ Backward Subsumption, 29537 ] % 4.26/4.41 (1,1) [27964,0]. true => _t195 | ~_t194 [ Axiom T ] [ Backward Subsumption, 29539 ] % 4.26/4.41 (1,1) [27966,0]. true => _t196 | ~_t195 [ Axiom T ] [ Backward Subsumption, 29592 ] % 4.26/4.41 (1,1) [27968,0]. true => _t197 | ~_t196 [ Axiom T ] [ Backward Subsumption, 29637 ] % 4.26/4.41 (1,1) [27970,0]. true => _t198 | ~_t197 [ Axiom T ] [ Backward Subsumption, 29677 ] % 4.26/4.41 (1,1) [27972,0]. true => _t199 | ~_t198 [ Axiom T ] [ Backward Subsumption, 29712 ] % 4.26/4.41 (1,1) [27973,0]. true => ~_t200 | p27 | p26 [ Axiom T ] [ Backward Subsumption, 29761 ] % 4.26/4.41 (1,1) [27974,0]. true => _t200 | ~_t199 [ Axiom T ] [ Backward Subsumption, 29715 ] % 4.26/4.41 (1,1) [27975,0]. true => ~_t201 | ~p27 | ~p26 [ Axiom T ] [ Backward Subsumption, 29762 ] % 4.26/4.41 (1,1) [27976,0]. true => _t201 | ~_t199 [ Axiom T ] [ Backward Subsumption, 29714 ] % 4.26/4.41 (1,1) [27977,0]. true => _t173 | ~_t172 [ Axiom T ] [ Backward Subsumption, 29021 ] % 4.26/4.41 (1,1) [27979,0]. true => _t203 | ~_t202 [ Axiom T ] [ Backward Subsumption, 29026 ] % 4.26/4.41 (1,1) [27981,0]. true => _t205 | ~_t204 [ Axiom T ] [ Backward Subsumption, 29056 ] % 4.26/4.41 (1,1) [27983,0]. true => _t206 | ~_t205 [ Axiom T ] [ Backward Subsumption, 29077 ] % 4.26/4.41 (1,1) [27985,0]. true => _t207 | ~_t206 [ Axiom T ] [ Backward Subsumption, 29093 ] % 4.26/4.41 (1,1) [27987,0]. true => _t208 | ~_t207 [ Axiom T ] [ Backward Subsumption, 29114 ] % 4.26/4.41 (1,1) [27989,0]. true => _t209 | ~_t208 [ Axiom T ] [ Backward Subsumption, 29141 ] % 4.26/4.41 (1,1) [27991,0]. true => _t210 | ~_t209 [ Axiom T ] [ Backward Subsumption, 29149 ] % 4.26/4.41 (1,1) [27993,0]. true => _t211 | ~_t210 [ Axiom T ] [ Backward Subsumption, 29178 ] % 4.26/4.41 (1,1) [27995,0]. true => _t212 | ~_t211 [ Axiom T ] [ Backward Subsumption, 29208 ] % 4.26/4.41 (1,1) [27997,0]. true => _t213 | ~_t212 [ Axiom T ] [ Backward Subsumption, 29216 ] % 4.26/4.41 (1,1) [27999,0]. true => _t214 | ~_t213 [ Axiom T ] [ Backward Subsumption, 29249 ] % 4.26/4.41 (1,1) [28001,0]. true => _t215 | ~_t214 [ Axiom T ] [ Backward Subsumption, 29272 ] % 4.26/4.41 (1,1) [28003,0]. true => _t216 | ~_t215 [ Axiom T ] [ Backward Subsumption, 29299 ] % 4.26/4.41 (1,1) [28005,0]. true => _t217 | ~_t216 [ Axiom T ] [ Backward Subsumption, 29328 ] % 4.26/4.41 (1,1) [28007,0]. true => _t218 | ~_t217 [ Axiom T ] [ Backward Subsumption, 29355 ] % 4.26/4.41 (1,1) [28009,0]. true => _t219 | ~_t218 [ Axiom T ] [ Backward Subsumption, 29395 ] % 4.26/4.41 (1,1) [28011,0]. true => _t220 | ~_t219 [ Axiom T ] [ Backward Subsumption, 29432 ] % 4.26/4.41 (1,1) [28013,0]. true => _t221 | ~_t220 [ Axiom T ] [ Backward Subsumption, 29440 ] % 4.26/4.41 (1,1) [28015,0]. true => _t222 | ~_t221 [ Axiom T ] [ Backward Subsumption, 29486 ] % 4.26/4.41 (1,1) [28017,0]. true => _t223 | ~_t222 [ Axiom T ] [ Backward Subsumption, 29512 ] % 4.26/4.41 (1,1) [28019,0]. true => _t224 | ~_t223 [ Axiom T ] [ Backward Subsumption, 29552 ] % 4.26/4.41 (1,1) [28021,0]. true => _t225 | ~_t224 [ Axiom T ] [ Backward Subsumption, 29600 ] % 4.26/4.41 (1,1) [28023,0]. true => _t226 | ~_t225 [ Axiom T ] [ Backward Subsumption, 29641 ] % 4.26/4.41 (1,1) [28025,0]. true => _t227 | ~_t226 [ Axiom T ] [ Backward Subsumption, 29679 ] % 4.26/4.41 (1,1) [28027,0]. true => _t228 | ~_t227 [ Axiom T ] [ Backward Subsumption, 29681 ] % 4.26/4.41 (1,1) [28029,0]. true => _t229 | ~_t228 [ Axiom T ] [ Backward Subsumption, 29730 ] % 4.26/4.41 (1,1) [28030,0]. true => ~_t230 | p26 | p25 [ Axiom T ] [ Backward Subsumption, 29804 ] % 4.26/4.41 (1,1) [28031,0]. true => _t230 | ~_t229 [ Axiom T ] [ Backward Subsumption, 29770 ] % 4.26/4.41 (1,1) [28032,0]. true => ~_t231 | ~p26 | ~p25 [ Axiom T ] [ Backward Subsumption, 29783 ] % 4.26/4.41 (1,1) [28033,0]. true => _t231 | ~_t229 [ Axiom T ] [ Backward Subsumption, 29769 ] % 4.26/4.41 (1,1) [28034,0]. true => _t204 | ~_t203 [ Axiom T ] [ Backward Subsumption, 29049 ] % 4.26/4.41 (1,1) [28036,0]. true => _t233 | ~_t232 [ Axiom T ] [ Backward Subsumption, 29067 ] % 4.26/4.41 (1,1) [28038,0]. true => _t235 | ~_t234 [ Axiom T ] [ Backward Subsumption, 29088 ] % 4.26/4.41 (1,1) [28040,0]. true => _t236 | ~_t235 [ Axiom T ] [ Backward Subsumption, 29116 ] % 4.26/4.41 (1,1) [28042,0]. true => _t237 | ~_t236 [ Axiom T ] [ Backward Subsumption, 29130 ] % 4.26/4.41 (1,1) [28044,0]. true => _t238 | ~_t237 [ Axiom T ] [ Backward Subsumption, 29160 ] % 4.26/4.41 (1,1) [28046,0]. true => _t239 | ~_t238 [ Axiom T ] [ Backward Subsumption, 29187 ] % 4.26/4.41 (1,1) [28048,0]. true => _t240 | ~_t239 [ Axiom T ] [ Backward Subsumption, 29212 ] % 4.26/4.41 (1,1) [28050,0]. true => _t241 | ~_t240 [ Axiom T ] [ Backward Subsumption, 29214 ] % 4.26/4.41 (1,1) [28052,0]. true => _t242 | ~_t241 [ Axiom T ] [ Backward Subsumption, 29251 ] % 4.26/4.41 (1,1) [28054,0]. true => _t243 | ~_t242 [ Axiom T ] [ Backward Subsumption, 29284 ] % 4.26/4.41 (1,1) [28056,0]. true => _t244 | ~_t243 [ Axiom T ] [ Backward Subsumption, 29293 ] % 4.26/4.41 (1,1) [28058,0]. true => _t245 | ~_t244 [ Axiom T ] [ Backward Subsumption, 29334 ] % 4.26/4.41 (1,1) [28060,0]. true => _t246 | ~_t245 [ Axiom T ] [ Backward Subsumption, 29370 ] % 4.26/4.41 (1,1) [28062,0]. true => _t247 | ~_t246 [ Axiom T ] [ Backward Subsumption, 29378 ] % 4.26/4.41 (1,1) [28064,0]. true => _t248 | ~_t247 [ Axiom T ] [ Backward Subsumption, 29424 ] % 4.26/4.41 (1,1) [28066,0]. true => _t249 | ~_t248 [ Axiom T ] [ Backward Subsumption, 29444 ] % 4.26/4.41 (1,1) [28068,0]. true => _t250 | ~_t249 [ Axiom T ] [ Backward Subsumption, 29484 ] % 4.26/4.41 (1,1) [28070,0]. true => _t251 | ~_t250 [ Axiom T ] [ Backward Subsumption, 29529 ] % 4.26/4.41 (1,1) [28072,0]. true => _t252 | ~_t251 [ Axiom T ] [ Backward Subsumption, 29543 ] % 4.26/4.41 (1,1) [28074,0]. true => _t253 | ~_t252 [ Axiom T ] [ Backward Subsumption, 29594 ] % 4.26/4.41 (1,1) [28076,0]. true => _t254 | ~_t253 [ Axiom T ] [ Backward Subsumption, 29619 ] % 4.26/4.41 (1,1) [28078,0]. true => _t255 | ~_t254 [ Axiom T ] [ Backward Subsumption, 29668 ] % 4.26/4.41 (1,1) [28080,0]. true => _t256 | ~_t255 [ Axiom T ] [ Backward Subsumption, 29708 ] % 4.26/4.41 (1,1) [28082,0]. true => _t257 | ~_t256 [ Axiom T ] [ Backward Subsumption, 29716 ] % 4.26/4.41 (1,1) [28084,0]. true => _t258 | ~_t257 [ Axiom T ] [ Backward Subsumption, 29763 ] % 4.26/4.41 (1,1) [28085,0]. true => ~_t259 | p25 | p24 [ Axiom T ] [ Backward Subsumption, 29834 ] % 4.26/4.41 (1,1) [28086,0]. true => _t259 | ~_t258 [ Axiom T ] [ Backward Subsumption, 29801 ] % 4.26/4.41 (1,1) [28087,0]. true => ~_t260 | ~p25 | ~p24 [ Axiom T ] [ Backward Subsumption, 29813 ] % 4.26/4.41 (1,1) [28088,0]. true => _t260 | ~_t258 [ Axiom T ] [ Backward Subsumption, 29800 ] % 4.26/4.41 (1,1) [28089,0]. true => _t234 | ~_t233 [ Axiom T ] [ Backward Subsumption, 29087 ] % 4.26/4.41 (1,1) [28091,0]. true => _t262 | ~_t261 [ Axiom T ] [ Backward Subsumption, 29105 ] % 4.26/4.41 (1,1) [28093,0]. true => _t264 | ~_t263 [ Axiom T ] [ Backward Subsumption, 29134 ] % 4.26/4.41 (1,1) [28095,0]. true => _t265 | ~_t264 [ Axiom T ] [ Backward Subsumption, 29162 ] % 4.26/4.41 (1,1) [28097,0]. true => _t266 | ~_t265 [ Axiom T ] [ Backward Subsumption, 29170 ] % 4.26/4.41 (1,1) [28099,0]. true => _t267 | ~_t266 [ Axiom T ] [ Backward Subsumption, 29204 ] % 4.26/4.41 (1,1) [28101,0]. true => _t268 | ~_t267 [ Axiom T ] [ Backward Subsumption, 29218 ] % 4.26/4.41 (1,1) [28103,0]. true => _t269 | ~_t268 [ Axiom T ] [ Backward Subsumption, 29253 ] % 4.26/4.41 (1,1) [28105,0]. true => _t270 | ~_t269 [ Axiom T ] [ Backward Subsumption, 29270 ] % 4.26/4.41 (1,1) [28107,0]. true => _t271 | ~_t270 [ Axiom T ] [ Backward Subsumption, 29308 ] % 4.26/4.41 (1,1) [28109,0]. true => _t272 | ~_t271 [ Axiom T ] [ Backward Subsumption, 29322 ] % 4.26/4.41 (1,1) [28111,0]. true => _t273 | ~_t272 [ Axiom T ] [ Backward Subsumption, 29363 ] % 4.26/4.41 (1,1) [28113,0]. true => _t274 | ~_t273 [ Axiom T ] [ Backward Subsumption, 29399 ] % 4.26/4.41 (1,1) [28115,0]. true => _t275 | ~_t274 [ Axiom T ] [ Backward Subsumption, 29434 ] % 4.26/4.41 (1,1) [28117,0]. true => _t276 | ~_t275 [ Axiom T ] [ Backward Subsumption, 29469 ] % 4.26/4.41 (1,1) [28119,0]. true => _t277 | ~_t276 [ Axiom T ] [ Backward Subsumption, 29471 ] % 4.26/4.41 (1,1) [28121,0]. true => _t278 | ~_t277 [ Axiom T ] [ Backward Subsumption, 29522 ] % 4.26/4.41 (1,1) [28123,0]. true => _t279 | ~_t278 [ Axiom T ] [ Backward Subsumption, 29566 ] % 4.26/4.41 (1,1) [28125,0]. true => _t280 | ~_t279 [ Axiom T ] [ Backward Subsumption, 29607 ] % 4.26/4.41 (1,1) [28127,0]. true => _t281 | ~_t280 [ Axiom T ] [ Backward Subsumption, 29644 ] % 4.26/4.41 (1,1) [28129,0]. true => _t282 | ~_t281 [ Axiom T ] [ Backward Subsumption, 29646 ] % 4.26/4.41 (1,1) [28131,0]. true => _t283 | ~_t282 [ Axiom T ] [ Backward Subsumption, 29697 ] % 4.26/4.41 (1,1) [28133,0]. true => _t284 | ~_t283 [ Axiom T ] [ Backward Subsumption, 29739 ] % 4.26/4.41 (1,1) [28135,0]. true => _t285 | ~_t284 [ Axiom T ] [ Backward Subsumption, 29774 ] % 4.26/4.41 (1,1) [28137,0]. true => _t286 | ~_t285 [ Axiom T ] [ Backward Subsumption, 29807 ] % 4.26/4.41 (1,1) [28138,0]. true => ~_t287 | p24 | p23 [ Axiom T ] [ Backward Subsumption, 29851 ] % 4.26/4.41 (1,1) [28139,0]. true => _t287 | ~_t286 [ Axiom T ] [ Backward Subsumption, 29810 ] % 4.26/4.41 (1,1) [28140,0]. true => ~_t288 | ~p24 | ~p23 [ Axiom T ] [ Backward Subsumption, 29852 ] % 4.26/4.41 (1,1) [28141,0]. true => _t288 | ~_t286 [ Axiom T ] [ Backward Subsumption, 29809 ] % 4.26/4.41 (1,1) [28142,0]. true => _t263 | ~_t262 [ Axiom T ] [ Backward Subsumption, 29109 ] % 4.26/4.41 (1,1) [28144,0]. true => _t290 | ~_t289 [ Axiom T ] [ Backward Subsumption, 29137 ] % 4.26/4.41 (1,1) [28146,0]. true => _t292 | ~_t291 [ Axiom T ] [ Backward Subsumption, 29183 ] % 4.26/4.41 (1,1) [28148,0]. true => _t293 | ~_t292 [ Axiom T ] [ Backward Subsumption, 29210 ] % 4.26/4.41 (1,1) [28150,0]. true => _t294 | ~_t293 [ Axiom T ] [ Backward Subsumption, 29237 ] % 4.26/4.41 (1,1) [28152,0]. true => _t295 | ~_t294 [ Axiom T ] [ Backward Subsumption, 29239 ] % 4.26/4.41 (1,1) [28154,0]. true => _t296 | ~_t295 [ Axiom T ] [ Backward Subsumption, 29278 ] % 4.26/4.41 (1,1) [28156,0]. true => _t297 | ~_t296 [ Axiom T ] [ Backward Subsumption, 29312 ] % 4.26/4.41 (1,1) [28158,0]. true => _t298 | ~_t297 [ Axiom T ] [ Backward Subsumption, 29320 ] % 4.26/4.41 (1,1) [28160,0]. true => _t299 | ~_t298 [ Axiom T ] [ Backward Subsumption, 29359 ] % 4.26/4.41 (1,1) [28162,0]. true => _t300 | ~_t299 [ Axiom T ] [ Backward Subsumption, 29397 ] % 4.26/4.41 (1,1) [28164,0]. true => _t301 | ~_t300 [ Axiom T ] [ Backward Subsumption, 29412 ] % 4.26/4.41 (1,1) [28166,0]. true => _t302 | ~_t301 [ Axiom T ] [ Backward Subsumption, 29450 ] % 4.26/4.41 (1,1) [28168,0]. true => _t303 | ~_t302 [ Axiom T ] [ Backward Subsumption, 29494 ] % 4.26/4.41 (1,1) [28170,0]. true => _t304 | ~_t303 [ Axiom T ] [ Backward Subsumption, 29508 ] % 4.26/4.41 (1,1) [28172,0]. true => _t305 | ~_t304 [ Axiom T ] [ Backward Subsumption, 29554 ] % 4.26/4.41 (1,1) [28174,0]. true => _t306 | ~_t305 [ Axiom T ] [ Backward Subsumption, 29583 ] % 4.26/4.41 (1,1) [28176,0]. true => _t307 | ~_t306 [ Axiom T ] [ Backward Subsumption, 29633 ] % 4.26/4.41 (1,1) [28178,0]. true => _t308 | ~_t307 [ Axiom T ] [ Backward Subsumption, 29651 ] % 4.26/4.41 (1,1) [28180,0]. true => _t309 | ~_t308 [ Axiom T ] [ Backward Subsumption, 29695 ] % 4.26/4.41 (1,1) [28182,0]. true => _t310 | ~_t309 [ Axiom T ] [ Backward Subsumption, 29722 ] % 4.26/4.41 (1,1) [28184,0]. true => _t311 | ~_t310 [ Axiom T ] [ Backward Subsumption, 29757 ] % 4.26/4.41 (1,1) [28186,0]. true => _t312 | ~_t311 [ Axiom T ] [ Backward Subsumption, 29798 ] % 4.26/4.41 (1,1) [28188,0]. true => _t313 | ~_t312 [ Axiom T ] [ Backward Subsumption, 29832 ] % 4.26/4.41 (1,1) [28189,0]. true => ~_t314 | p23 | p22 [ Axiom T ] [ Backward Subsumption, 29893 ] % 4.26/4.41 (1,1) [28190,0]. true => _t314 | ~_t313 [ Axiom T ] [ Backward Subsumption, 29864 ] % 4.26/4.41 (1,1) [28191,0]. true => ~_t315 | ~p23 | ~p22 [ Axiom T ] [ Backward Subsumption, 29870 ] % 4.26/4.41 (1,1) [28192,0]. true => _t315 | ~_t313 [ Axiom T ] [ Backward Subsumption, 29863 ] % 4.26/4.41 (1,1) [28193,0]. true => _t291 | ~_t290 [ Axiom T ] [ Backward Subsumption, 29153 ] % 4.26/4.41 (1,1) [28195,0]. true => _t317 | ~_t316 [ Axiom T ] [ Backward Subsumption, 29176 ] % 4.26/4.41 (1,1) [28197,0]. true => _t319 | ~_t318 [ Axiom T ] [ Backward Subsumption, 29231 ] % 4.26/4.41 (1,1) [28199,0]. true => _t320 | ~_t319 [ Axiom T ] [ Backward Subsumption, 29260 ] % 4.26/4.41 (1,1) [28201,0]. true => _t321 | ~_t320 [ Axiom T ] [ Backward Subsumption, 29289 ] % 4.26/4.41 (1,1) [28203,0]. true => _t322 | ~_t321 [ Axiom T ] [ Backward Subsumption, 29291 ] % 4.26/4.41 (1,1) [28205,0]. true => _t323 | ~_t322 [ Axiom T ] [ Backward Subsumption, 29332 ] % 4.26/4.41 (1,1) [28207,0]. true => _t324 | ~_t323 [ Axiom T ] [ Backward Subsumption, 29353 ] % 4.26/4.41 (1,1) [28209,0]. true => _t325 | ~_t324 [ Axiom T ] [ Backward Subsumption, 29387 ] % 4.26/4.41 (1,1) [28211,0]. true => _t326 | ~_t325 [ Axiom T ] [ Backward Subsumption, 29428 ] % 4.26/4.41 (1,1) [28213,0]. true => _t327 | ~_t326 [ Axiom T ] [ Backward Subsumption, 29442 ] % 4.26/4.41 (1,1) [28215,0]. true => _t328 | ~_t327 [ Axiom T ] [ Backward Subsumption, 29490 ] % 4.26/4.41 (1,1) [28217,0]. true => _t329 | ~_t328 [ Axiom T ] [ Backward Subsumption, 29510 ] % 4.26/4.41 (1,1) [28219,0]. true => _t330 | ~_t329 [ Axiom T ] [ Backward Subsumption, 29560 ] % 4.26/4.41 (1,1) [28221,0]. true => _t331 | ~_t330 [ Axiom T ] [ Backward Subsumption, 29604 ] % 4.26/4.41 (1,1) [28223,0]. true => _t332 | ~_t331 [ Axiom T ] [ Backward Subsumption, 29613 ] % 4.26/4.41 (1,1) [28225,0]. true => _t333 | ~_t332 [ Axiom T ] [ Backward Subsumption, 29664 ] % 4.26/4.41 (1,1) [28227,0]. true => _t334 | ~_t333 [ Axiom T ] [ Backward Subsumption, 29706 ] % 4.26/4.41 (1,1) [28229,0]. true => _t335 | ~_t334 [ Axiom T ] [ Backward Subsumption, 29743 ] % 4.26/4.41 (1,1) [28231,0]. true => _t336 | ~_t335 [ Axiom T ] [ Backward Subsumption, 29776 ] % 4.26/4.41 (1,1) [28233,0]. true => _t337 | ~_t336 [ Axiom T ] [ Backward Subsumption, 29778 ] % 4.26/4.41 (1,1) [28235,0]. true => _t338 | ~_t337 [ Axiom T ] [ Backward Subsumption, 29822 ] % 4.26/4.41 (1,1) [28237,0]. true => _t339 | ~_t338 [ Axiom T ] [ Backward Subsumption, 29845 ] % 4.26/4.41 (1,1) [28238,0]. true => ~_t340 | p22 | p21 [ Axiom T ] [ Backward Subsumption, 29914 ] % 4.26/4.41 (1,1) [28239,0]. true => _t340 | ~_t339 [ Axiom T ] [ Backward Subsumption, 29878 ] % 4.26/4.41 (1,1) [28240,0]. true => ~_t341 | ~p22 | ~p21 [ Axiom T ] [ Backward Subsumption, 29902 ] % 4.26/4.41 (1,1) [28241,0]. true => _t341 | ~_t339 [ Axiom T ] [ Backward Subsumption, 29877 ] % 4.26/4.41 (1,1) [28242,0]. true => _t318 | ~_t317 [ Axiom T ] [ Backward Subsumption, 29199 ] % 4.26/4.41 (1,1) [28244,0]. true => _t343 | ~_t342 [ Axiom T ] [ Backward Subsumption, 29222 ] % 4.26/4.41 (1,1) [28246,0]. true => _t345 | ~_t344 [ Axiom T ] [ Backward Subsumption, 29287 ] % 4.26/4.41 (1,1) [28248,0]. true => _t346 | ~_t345 [ Axiom T ] [ Backward Subsumption, 29316 ] % 4.26/4.41 (1,1) [28250,0]. true => _t347 | ~_t346 [ Axiom T ] [ Backward Subsumption, 29318 ] % 4.26/4.41 (1,1) [28252,0]. true => _t348 | ~_t347 [ Axiom T ] [ Backward Subsumption, 29361 ] % 4.26/4.41 (1,1) [28254,0]. true => _t349 | ~_t348 [ Axiom T ] [ Backward Subsumption, 29383 ] % 4.26/4.41 (1,1) [28256,0]. true => _t350 | ~_t349 [ Axiom T ] [ Backward Subsumption, 29426 ] % 4.26/4.41 (1,1) [28258,0]. true => _t351 | ~_t350 [ Axiom T ] [ Backward Subsumption, 29465 ] % 4.26/4.41 (1,1) [28260,0]. true => _t352 | ~_t351 [ Axiom T ] [ Backward Subsumption, 29473 ] % 4.26/4.41 (1,1) [28262,0]. true => _t353 | ~_t352 [ Axiom T ] [ Backward Subsumption, 29520 ] % 4.26/4.41 (1,1) [28264,0]. true => _t354 | ~_t353 [ Axiom T ] [ Backward Subsumption, 29547 ] % 4.26/4.41 (1,1) [28266,0]. true => _t355 | ~_t354 [ Axiom T ] [ Backward Subsumption, 29596 ] % 4.26/4.41 (1,1) [28268,0]. true => _t356 | ~_t355 [ Axiom T ] [ Backward Subsumption, 29639 ] % 4.26/4.41 (1,1) [28270,0]. true => _t357 | ~_t356 [ Axiom T ] [ Backward Subsumption, 29648 ] % 4.26/4.41 (1,1) [28272,0]. true => _t358 | ~_t357 [ Axiom T ] [ Backward Subsumption, 29699 ] % 4.26/4.41 (1,1) [28274,0]. true => _t359 | ~_t358 [ Axiom T ] [ Backward Subsumption, 29720 ] % 4.26/4.41 (1,1) [28276,0]. true => _t360 | ~_t359 [ Axiom T ] [ Backward Subsumption, 29765 ] % 4.26/4.41 (1,1) [28278,0]. true => _t361 | ~_t360 [ Axiom T ] [ Backward Subsumption, 29784 ] % 4.26/4.41 (1,1) [28280,0]. true => _t362 | ~_t361 [ Axiom T ] [ Backward Subsumption, 29820 ] % 4.26/4.41 (1,1) [28282,0]. true => _t363 | ~_t362 [ Axiom T ] [ Backward Subsumption, 29857 ] % 4.26/4.41 (1,1) [28284,0]. true => _t364 | ~_t363 [ Axiom T ] [ Backward Subsumption, 29889 ] % 4.26/4.41 (1,1) [28285,0]. true => ~_t365 | p21 | p20 [ Axiom T ] [ Backward Subsumption, 29921 ] % 4.26/4.41 (1,1) [28286,0]. true => _t365 | ~_t364 [ Axiom T ] [ Backward Subsumption, 29920 ] % 4.26/4.41 (1,1) [28287,0]. true => ~_t366 | ~p21 | ~p20 [ Axiom T ] [ Backward Subsumption, 29945 ] % 4.26/4.41 (1,1) [28288,0]. true => _t366 | ~_t364 [ Axiom T ] [ Backward Subsumption, 29919 ] % 4.26/4.41 (1,1) [28289,0]. true => _t344 | ~_t343 [ Axiom T ] [ Backward Subsumption, 29257 ] % 4.26/4.41 (1,1) [28291,0]. true => _t368 | ~_t367 [ Axiom T ] [ Backward Subsumption, 29268 ] % 4.26/4.41 (1,1) [28293,0]. true => _t370 | ~_t369 [ Axiom T ] [ Backward Subsumption, 29339 ] % 4.26/4.41 (1,1) [28295,0]. true => _t371 | ~_t370 [ Axiom T ] [ Backward Subsumption, 29372 ] % 4.26/4.41 (1,1) [28297,0]. true => _t372 | ~_t371 [ Axiom T ] [ Backward Subsumption, 29405 ] % 4.26/4.41 (1,1) [28299,0]. true => _t373 | ~_t372 [ Axiom T ] [ Backward Subsumption, 29407 ] % 4.26/4.41 (1,1) [28301,0]. true => _t374 | ~_t373 [ Axiom T ] [ Backward Subsumption, 29454 ] % 4.26/4.41 (1,1) [28303,0]. true => _t375 | ~_t374 [ Axiom T ] [ Backward Subsumption, 29496 ] % 4.26/4.41 (1,1) [28305,0]. true => _t376 | ~_t375 [ Axiom T ] [ Backward Subsumption, 29535 ] % 4.26/4.41 (1,1) [28307,0]. true => _t377 | ~_t376 [ Axiom T ] [ Backward Subsumption, 29572 ] % 4.26/4.41 (1,1) [28309,0]. true => _t378 | ~_t377 [ Axiom T ] [ Backward Subsumption, 29574 ] % 4.26/4.41 (1,1) [28311,0]. true => _t379 | ~_t378 [ Axiom T ] [ Backward Subsumption, 29629 ] % 4.26/4.41 (1,1) [28313,0]. true => _t380 | ~_t379 [ Axiom T ] [ Backward Subsumption, 29653 ] % 4.26/4.41 (1,1) [28315,0]. true => _t381 | ~_t380 [ Axiom T ] [ Backward Subsumption, 29701 ] % 4.26/4.41 (1,1) [28317,0]. true => _t382 | ~_t381 [ Axiom T ] [ Backward Subsumption, 29741 ] % 4.26/4.41 (1,1) [28319,0]. true => _t383 | ~_t382 [ Axiom T ] [ Backward Subsumption, 29749 ] % 4.26/4.41 (1,1) [28321,0]. true => _t384 | ~_t383 [ Axiom T ] [ Backward Subsumption, 29794 ] % 4.26/4.41 (1,1) [28323,0]. true => _t385 | ~_t384 [ Axiom T ] [ Backward Subsumption, 29830 ] % 4.26/4.41 (1,1) [28325,0]. true => _t386 | ~_t385 [ Axiom T ] [ Backward Subsumption, 29841 ] % 4.26/4.41 (1,1) [28327,0]. true => _t387 | ~_t386 [ Axiom T ] [ Backward Subsumption, 29879 ] % 4.26/4.41 (1,1) [28329,0]. true => _t388 | ~_t387 [ Axiom T ] [ Backward Subsumption, 29900 ] % 4.26/4.41 (1,1) [28330,0]. true => ~_t389 | p20 | p19 [ Axiom T ] [ Backward Subsumption, 29968 ] % 4.26/4.41 (1,1) [28331,0]. true => _t389 | ~_t388 [ Axiom T ] [ Backward Subsumption, 29938 ] % 4.26/4.41 (1,1) [28332,0]. true => ~_t390 | ~p20 | ~p19 [ Axiom T ] [ Backward Subsumption, 29950 ] % 4.26/4.41 (1,1) [28333,0]. true => _t390 | ~_t388 [ Axiom T ] [ Backward Subsumption, 29937 ] % 4.26/4.41 (1,1) [28334,0]. true => _t369 | ~_t368 [ Axiom T ] [ Backward Subsumption, 29303 ] % 4.26/4.41 (1,1) [28336,0]. true => _t392 | ~_t391 [ Axiom T ] [ Backward Subsumption, 29326 ] % 4.26/4.41 (1,1) [28338,0]. true => _t394 | ~_t393 [ Axiom T ] [ Backward Subsumption, 29380 ] % 4.26/4.41 (1,1) [28340,0]. true => _t395 | ~_t394 [ Axiom T ] [ Backward Subsumption, 29420 ] % 4.26/4.41 (1,1) [28342,0]. true => _t396 | ~_t395 [ Axiom T ] [ Backward Subsumption, 29446 ] % 4.26/4.41 (1,1) [28344,0]. true => _t397 | ~_t396 [ Axiom T ] [ Backward Subsumption, 29492 ] % 4.26/4.41 (1,1) [28346,0]. true => _t398 | ~_t397 [ Axiom T ] [ Backward Subsumption, 29533 ] % 4.26/4.41 (1,1) [28348,0]. true => _t399 | ~_t398 [ Axiom T ] [ Backward Subsumption, 29541 ] % 4.26/4.41 (1,1) [28350,0]. true => _t400 | ~_t399 [ Axiom T ] [ Backward Subsumption, 29590 ] % 4.26/4.41 (1,1) [28352,0]. true => _t401 | ~_t400 [ Axiom T ] [ Backward Subsumption, 29621 ] % 4.26/4.41 (1,1) [28354,0]. true => _t402 | ~_t401 [ Axiom T ] [ Backward Subsumption, 29657 ] % 4.26/4.41 (1,1) [28356,0]. true => _t403 | ~_t402 [ Axiom T ] [ Backward Subsumption, 29692 ] % 4.26/4.41 (1,1) [28358,0]. true => _t404 | ~_t403 [ Axiom T ] [ Backward Subsumption, 29737 ] % 4.26/4.41 (1,1) [28360,0]. true => _t405 | ~_t404 [ Axiom T ] [ Backward Subsumption, 29751 ] % 4.26/4.41 (1,1) [28362,0]. true => _t406 | ~_t405 [ Axiom T ] [ Backward Subsumption, 29790 ] % 4.26/4.41 (1,1) [28364,0]. true => _t407 | ~_t406 [ Axiom T ] [ Backward Subsumption, 29828 ] % 4.26/4.41 (1,1) [28366,0]. true => _t408 | ~_t407 [ Axiom T ] [ Backward Subsumption, 29861 ] % 4.26/4.41 (1,1) [28368,0]. true => _t409 | ~_t408 [ Axiom T ] [ Backward Subsumption, 29891 ] % 4.26/4.41 (1,1) [28370,0]. true => _t410 | ~_t409 [ Axiom T ] [ Backward Subsumption, 29894 ] % 4.26/4.41 (1,1) [28372,0]. true => _t411 | ~_t410 [ Axiom T ] [ Backward Subsumption, 29933 ] % 4.26/4.41 (1,1) [28373,0]. true => ~_t412 | p19 | p18 [ Axiom T ] [ Backward Subsumption, 29980 ] % 4.26/4.41 (1,1) [28374,0]. true => _t412 | ~_t411 [ Axiom T ] [ Backward Subsumption, 29952 ] % 4.26/4.41 (1,1) [28375,0]. true => ~_t413 | ~p19 | ~p18 [ Axiom T ] [ Backward Subsumption, 29985 ] % 4.26/4.41 (1,1) [28376,0]. true => _t413 | ~_t411 [ Axiom T ] [ Backward Subsumption, 29951 ] % 4.26/4.41 (1,1) [28377,0]. true => _t393 | ~_t392 [ Axiom T ] [ Backward Subsumption, 29367 ] % 4.26/4.41 (1,1) [28379,0]. true => _t415 | ~_t414 [ Axiom T ] [ Backward Subsumption, 29401 ] % 4.26/4.41 (1,1) [28381,0]. true => _t417 | ~_t416 [ Axiom T ] [ Backward Subsumption, 29457 ] % 4.26/4.41 (1,1) [28383,0]. true => _t418 | ~_t417 [ Axiom T ] [ Backward Subsumption, 29477 ] % 4.26/4.41 (1,1) [28385,0]. true => _t419 | ~_t418 [ Axiom T ] [ Backward Subsumption, 29518 ] % 4.26/4.41 (1,1) [28387,0]. true => _t420 | ~_t419 [ Axiom T ] [ Backward Subsumption, 29564 ] % 4.26/4.41 (1,1) [28389,0]. true => _t421 | ~_t420 [ Axiom T ] [ Backward Subsumption, 29578 ] % 4.26/4.41 (1,1) [28391,0]. true => _t422 | ~_t421 [ Axiom T ] [ Backward Subsumption, 29631 ] % 4.26/4.41 (1,1) [28393,0]. true => _t423 | ~_t422 [ Axiom T ] [ Backward Subsumption, 29674 ] % 4.26/4.41 (1,1) [28395,0]. true => _t424 | ~_t423 [ Axiom T ] [ Backward Subsumption, 29683 ] % 4.26/4.41 (1,1) [28397,0]. true => _t425 | ~_t424 [ Axiom T ] [ Backward Subsumption, 29728 ] % 4.26/4.41 (1,1) [28399,0]. true => _t426 | ~_t425 [ Axiom T ] [ Backward Subsumption, 29755 ] % 4.26/4.41 (1,1) [28401,0]. true => _t427 | ~_t426 [ Axiom T ] [ Backward Subsumption, 29788 ] % 4.26/4.41 (1,1) [28403,0]. true => _t428 | ~_t427 [ Axiom T ] [ Backward Subsumption, 29818 ] % 4.26/4.41 (1,1) [28405,0]. true => _t429 | ~_t428 [ Axiom T ] [ Backward Subsumption, 29847 ] % 4.26/4.41 (1,1) [28407,0]. true => _t430 | ~_t429 [ Axiom T ] [ Backward Subsumption, 29885 ] % 4.26/4.41 (1,1) [28409,0]. true => _t431 | ~_t430 [ Axiom T ] [ Backward Subsumption, 29917 ] % 4.26/4.41 (1,1) [28411,0]. true => _t432 | ~_t431 [ Axiom T ] [ Backward Subsumption, 29922 ] % 4.26/4.41 (1,1) [28413,0]. true => _t433 | ~_t432 [ Axiom T ] [ Backward Subsumption, 29959 ] % 4.26/4.41 (1,1) [28414,0]. true => ~_t434 | p18 | p17 [ Axiom T ] [ Backward Subsumption, 30008 ] % 4.26/4.41 (1,1) [28415,0]. true => _t434 | ~_t433 [ Axiom T ] [ Backward Subsumption, 29976 ] % 4.26/4.41 (1,1) [28416,0]. true => ~_t435 | ~p18 | ~p17 [ Axiom T ] [ Backward Subsumption, 30003 ] % 4.26/4.41 (1,1) [28417,0]. true => _t435 | ~_t433 [ Axiom T ] [ Backward Subsumption, 29975 ] % 4.26/4.41 (1,1) [28418,0]. true => _t416 | ~_t415 [ Axiom T ] [ Backward Subsumption, 29411 ] % 4.26/4.41 (1,1) [28420,0]. true => _t437 | ~_t436 [ Axiom T ] [ Backward Subsumption, 29452 ] % 4.26/4.41 (1,1) [28422,0]. true => _t439 | ~_t438 [ Axiom T ] [ Backward Subsumption, 29527 ] % 4.26/4.41 (1,1) [28424,0]. true => _t440 | ~_t439 [ Axiom T ] [ Backward Subsumption, 29568 ] % 4.26/4.41 (1,1) [28426,0]. true => _t441 | ~_t440 [ Axiom T ] [ Backward Subsumption, 29576 ] % 4.26/4.41 (1,1) [28428,0]. true => _t442 | ~_t441 [ Axiom T ] [ Backward Subsumption, 29627 ] % 4.26/4.41 (1,1) [28430,0]. true => _t443 | ~_t442 [ Axiom T ] [ Backward Subsumption, 29672 ] % 4.26/4.41 (1,1) [28432,0]. true => _t444 | ~_t443 [ Axiom T ] [ Backward Subsumption, 29710 ] % 4.26/4.41 (1,1) [28434,0]. true => _t445 | ~_t444 [ Axiom T ] [ Backward Subsumption, 29745 ] % 4.26/4.41 (1,1) [28436,0]. true => _t446 | ~_t445 [ Axiom T ] [ Backward Subsumption, 29747 ] % 4.26/4.41 (1,1) [28438,0]. true => _t447 | ~_t446 [ Axiom T ] [ Backward Subsumption, 29792 ] % 4.26/4.41 (1,1) [28440,0]. true => _t448 | ~_t447 [ Axiom T ] [ Backward Subsumption, 29816 ] % 4.26/4.41 (1,1) [28442,0]. true => _t449 | ~_t448 [ Axiom T ] [ Backward Subsumption, 29855 ] % 4.26/4.41 (1,1) [28444,0]. true => _t450 | ~_t449 [ Axiom T ] [ Backward Subsumption, 29873 ] % 4.26/4.41 (1,1) [28446,0]. true => _t451 | ~_t450 [ Axiom T ] [ Backward Subsumption, 29903 ] % 4.26/4.41 (1,1) [28448,0]. true => _t452 | ~_t451 [ Axiom T ] [ Backward Subsumption, 29929 ] % 4.26/4.41 (1,1) [28450,0]. true => _t453 | ~_t452 [ Axiom T ] [ Backward Subsumption, 29953 ] % 4.26/4.41 (1,1) [28452,0]. true => _t454 | ~_t453 [ Axiom T ] [ Backward Subsumption, 29986 ] % 4.26/4.41 (1,1) [28453,0]. true => ~_t455 | p17 | p16 [ Axiom T ] [ Backward Subsumption, 30037 ] % 4.26/4.41 (1,1) [28454,0]. true => _t455 | ~_t454 [ Axiom T ] [ Backward Subsumption, 30014 ] % 4.26/4.41 (1,1) [28455,0]. true => ~_t456 | ~p17 | ~p16 [ Axiom T ] [ Backward Subsumption, 30019 ] % 4.26/4.41 (1,1) [28456,0]. true => _t456 | ~_t454 [ Axiom T ] [ Backward Subsumption, 30013 ] % 4.26/4.41 (1,1) [28457,0]. true => _t438 | ~_t437 [ Axiom T ] [ Backward Subsumption, 29481 ] % 4.26/4.41 (1,1) [28459,0]. true => _t458 | ~_t457 [ Axiom T ] [ Backward Subsumption, 29516 ] % 4.26/4.41 (1,1) [28461,0]. true => _t460 | ~_t459 [ Axiom T ] [ Backward Subsumption, 29585 ] % 4.26/4.41 (1,1) [28463,0]. true => _t461 | ~_t460 [ Axiom T ] [ Backward Subsumption, 29623 ] % 4.26/4.41 (1,1) [28465,0]. true => _t462 | ~_t461 [ Axiom T ] [ Backward Subsumption, 29670 ] % 4.26/4.41 (1,1) [28467,0]. true => _t463 | ~_t462 [ Axiom T ] [ Backward Subsumption, 29685 ] % 4.26/4.41 (1,1) [28469,0]. true => _t464 | ~_t463 [ Axiom T ] [ Backward Subsumption, 29732 ] % 4.26/4.41 (1,1) [28471,0]. true => _t465 | ~_t464 [ Axiom T ] [ Backward Subsumption, 29753 ] % 4.26/4.41 (1,1) [28473,0]. true => _t466 | ~_t465 [ Axiom T ] [ Backward Subsumption, 29796 ] % 4.26/4.41 (1,1) [28475,0]. true => _t467 | ~_t466 [ Axiom T ] [ Backward Subsumption, 29814 ] % 4.26/4.41 (1,1) [28477,0]. true => _t468 | ~_t467 [ Axiom T ] [ Backward Subsumption, 29849 ] % 4.26/4.41 (1,1) [28479,0]. true => _t469 | ~_t468 [ Axiom T ] [ Backward Subsumption, 29875 ] % 4.26/4.41 (1,1) [28481,0]. true => _t470 | ~_t469 [ Axiom T ] [ Backward Subsumption, 29912 ] % 4.26/4.41 (1,1) [28483,0]. true => _t471 | ~_t470 [ Axiom T ] [ Backward Subsumption, 29924 ] % 4.26/4.41 (1,1) [28485,0]. true => _t472 | ~_t471 [ Axiom T ] [ Backward Subsumption, 29957 ] % 4.26/4.41 (1,1) [28487,0]. true => _t473 | ~_t472 [ Axiom T ] [ Backward Subsumption, 29988 ] % 4.26/4.41 (1,1) [28489,0]. true => _t474 | ~_t473 [ Axiom T ] [ Backward Subsumption, 29996 ] % 4.26/4.41 (1,1) [28490,0]. true => ~_t475 | p16 | p15 [ Axiom T ] [ Backward Subsumption, 30056 ] % 4.26/4.41 (1,1) [28491,0]. true => _t475 | ~_t474 [ Axiom T ] [ Backward Subsumption, 30030 ] % 4.26/4.41 (1,1) [28492,0]. true => ~_t476 | ~p16 | ~p15 [ Axiom T ] [ Backward Subsumption, 30042 ] % 4.26/4.41 (1,1) [28493,0]. true => _t476 | ~_t474 [ Axiom T ] [ Backward Subsumption, 30029 ] % 4.26/4.41 (1,1) [28494,0]. true => _t459 | ~_t458 [ Axiom T ] [ Backward Subsumption, 29551 ] % 4.26/4.41 (1,1) [28496,0]. true => _t478 | ~_t477 [ Axiom T ] [ Backward Subsumption, 29598 ] % 4.26/4.41 (1,1) [28498,0]. true => _t480 | ~_t479 [ Axiom T ] [ Backward Subsumption, 29659 ] % 4.26/4.41 (1,1) [28500,0]. true => _t481 | ~_t480 [ Axiom T ] [ Backward Subsumption, 29704 ] % 4.26/4.41 (1,1) [28502,0]. true => _t482 | ~_t481 [ Axiom T ] [ Backward Subsumption, 29718 ] % 4.26/4.41 (1,1) [28504,0]. true => _t483 | ~_t482 [ Axiom T ] [ Backward Subsumption, 29759 ] % 4.26/4.41 (1,1) [28506,0]. true => _t484 | ~_t483 [ Axiom T ] [ Backward Subsumption, 29786 ] % 4.26/4.41 (1,1) [28508,0]. true => _t485 | ~_t484 [ Axiom T ] [ Backward Subsumption, 29826 ] % 4.26/4.41 (1,1) [28510,0]. true => _t486 | ~_t485 [ Axiom T ] [ Backward Subsumption, 29843 ] % 4.26/4.41 (1,1) [28512,0]. true => _t487 | ~_t486 [ Axiom T ] [ Backward Subsumption, 29883 ] % 4.26/4.41 (1,1) [28514,0]. true => _t488 | ~_t487 [ Axiom T ] [ Backward Subsumption, 29898 ] % 4.26/4.41 (1,1) [28516,0]. true => _t489 | ~_t488 [ Axiom T ] [ Backward Subsumption, 29931 ] % 4.26/4.41 (1,1) [28518,0]. true => _t490 | ~_t489 [ Axiom T ] [ Backward Subsumption, 29964 ] % 4.26/4.41 (1,1) [28520,0]. true => _t491 | ~_t490 [ Axiom T ] [ Backward Subsumption, 29973 ] % 4.26/4.41 (1,1) [28522,0]. true => _t492 | ~_t491 [ Axiom T ] [ Backward Subsumption, 30006 ] % 4.26/4.41 (1,1) [28524,0]. true => _t493 | ~_t492 [ Axiom T ] [ Backward Subsumption, 30033 ] % 4.26/4.41 (1,1) [28525,0]. true => ~_t494 | p15 | p14 [ Axiom T ] [ Backward Subsumption, 30059 ] % 4.26/4.41 (1,1) [28526,0]. true => _t494 | ~_t493 [ Axiom T ] [ Backward Subsumption, 30058 ] % 4.26/4.41 (1,1) [28527,0]. true => ~_t495 | ~p15 | ~p14 [ Axiom T ] [ Backward Subsumption, 30077 ] % 4.26/4.41 (1,1) [28528,0]. true => _t495 | ~_t493 [ Axiom T ] [ Backward Subsumption, 30057 ] % 4.26/4.41 (1,1) [28529,0]. true => _t479 | ~_t478 [ Axiom T ] [ Backward Subsumption, 29618 ] % 4.26/4.41 (1,1) [28531,0]. true => _t497 | ~_t496 [ Axiom T ] [ Backward Subsumption, 29666 ] % 4.26/4.41 (1,1) [28533,0]. true => _t499 | ~_t498 [ Axiom T ] [ Backward Subsumption, 29725 ] % 4.26/4.41 (1,1) [28535,0]. true => _t500 | ~_t499 [ Axiom T ] [ Backward Subsumption, 29767 ] % 4.26/4.41 (1,1) [28537,0]. true => _t501 | ~_t500 [ Axiom T ] [ Backward Subsumption, 29802 ] % 4.26/4.41 (1,1) [28539,0]. true => _t502 | ~_t501 [ Axiom T ] [ Backward Subsumption, 29811 ] % 4.26/4.41 (1,1) [28541,0]. true => _t503 | ~_t502 [ Axiom T ] [ Backward Subsumption, 29853 ] % 4.26/4.41 (1,1) [28543,0]. true => _t504 | ~_t503 [ Axiom T ] [ Backward Subsumption, 29887 ] % 4.26/4.41 (1,1) [28545,0]. true => _t505 | ~_t504 [ Axiom T ] [ Backward Subsumption, 29896 ] % 4.26/4.41 (1,1) [28547,0]. true => _t506 | ~_t505 [ Axiom T ] [ Backward Subsumption, 29935 ] % 4.26/4.41 (1,1) [28549,0]. true => _t507 | ~_t506 [ Axiom T ] [ Backward Subsumption, 29966 ] % 4.26/4.41 (1,1) [28551,0]. true => _t508 | ~_t507 [ Axiom T ] [ Backward Subsumption, 29992 ] % 4.26/4.41 (1,1) [28553,0]. true => _t509 | ~_t508 [ Axiom T ] [ Backward Subsumption, 29994 ] % 4.26/4.41 (1,1) [28555,0]. true => _t510 | ~_t509 [ Axiom T ] [ Backward Subsumption, 30027 ] % 4.26/4.41 (1,1) [28557,0]. true => _t511 | ~_t510 [ Axiom T ] [ Backward Subsumption, 30054 ] % 4.26/4.41 (1,1) [28558,0]. true => ~_t512 | p14 | p13 [ Axiom T ] [ Backward Subsumption, 30088 ] % 4.26/4.41 (1,1) [28559,0]. true => _t512 | ~_t511 [ Axiom T ] [ Backward Subsumption, 30061 ] % 4.26/4.41 (1,1) [28560,0]. true => ~_t513 | ~p14 | ~p13 [ Axiom T ] [ Backward Subsumption, 30087 ] % 4.26/4.41 (1,1) [28561,0]. true => _t513 | ~_t511 [ Axiom T ] [ Backward Subsumption, 30060 ] % 4.26/4.41 (1,1) [28562,0]. true => _t498 | ~_t497 [ Axiom T ] [ Backward Subsumption, 29689 ] % 4.26/4.41 (1,1) [28564,0]. true => _t515 | ~_t514 [ Axiom T ] [ Backward Subsumption, 29734 ] % 4.26/4.41 (1,1) [28566,0]. true => _t517 | ~_t516 [ Axiom T ] [ Backward Subsumption, 29780 ] % 4.26/4.41 (1,1) [28568,0]. true => _t518 | ~_t517 [ Axiom T ] [ Backward Subsumption, 29824 ] % 4.26/4.41 (1,1) [28570,0]. true => _t519 | ~_t518 [ Axiom T ] [ Backward Subsumption, 29859 ] % 4.26/4.41 (1,1) [28572,0]. true => _t520 | ~_t519 [ Axiom T ] [ Backward Subsumption, 29871 ] % 4.26/4.41 (1,1) [28574,0]. true => _t521 | ~_t520 [ Axiom T ] [ Backward Subsumption, 29910 ] % 4.26/4.41 (1,1) [28576,0]. true => _t522 | ~_t521 [ Axiom T ] [ Backward Subsumption, 29941 ] % 4.26/4.41 (1,1) [28578,0]. true => _t523 | ~_t522 [ Axiom T ] [ Backward Subsumption, 29969 ] % 4.26/4.41 (1,1) [28580,0]. true => _t524 | ~_t523 [ Axiom T ] [ Backward Subsumption, 29971 ] % 4.26/4.41 (1,1) [28582,0]. true => _t525 | ~_t524 [ Axiom T ] [ Backward Subsumption, 30004 ] % 4.26/4.41 (1,1) [28584,0]. true => _t526 | ~_t525 [ Axiom T ] [ Backward Subsumption, 30023 ] % 4.26/4.41 (1,1) [28586,0]. true => _t527 | ~_t526 [ Axiom T ] [ Backward Subsumption, 30052 ] % 4.26/4.41 (1,1) [28588,0]. true => _t528 | ~_t527 [ Axiom T ] [ Backward Subsumption, 30075 ] % 4.26/4.41 (1,1) [28589,0]. true => ~_t529 | p13 | p12 [ Axiom T ] [ Backward Subsumption, 30106 ] % 4.26/4.41 (1,1) [28590,0]. true => _t529 | ~_t528 [ Axiom T ] [ Backward Subsumption, 30079 ] % 4.26/4.41 (1,1) [28591,0]. true => ~_t530 | ~p13 | ~p12 [ Axiom T ] [ Backward Subsumption, 30105 ] % 4.26/4.41 (1,1) [28592,0]. true => _t530 | ~_t528 [ Axiom T ] [ Backward Subsumption, 30078 ] % 4.26/4.41 (1,1) [28593,0]. true => _t516 | ~_t515 [ Axiom T ] [ Backward Subsumption, 29773 ] % 4.26/4.41 (1,1) [28595,0]. true => _t532 | ~_t531 [ Axiom T ] [ Backward Subsumption, 29805 ] % 4.26/4.41 (1,1) [28597,0]. true => _t534 | ~_t533 [ Axiom T ] [ Backward Subsumption, 29838 ] % 4.26/4.41 (1,1) [28599,0]. true => _t535 | ~_t534 [ Axiom T ] [ Backward Subsumption, 29881 ] % 4.26/4.41 (1,1) [28601,0]. true => _t536 | ~_t535 [ Axiom T ] [ Backward Subsumption, 29915 ] % 4.26/4.41 (1,1) [28603,0]. true => _t537 | ~_t536 [ Axiom T ] [ Backward Subsumption, 29943 ] % 4.26/4.41 (1,1) [28605,0]. true => _t538 | ~_t537 [ Axiom T ] [ Backward Subsumption, 29946 ] % 4.26/4.41 (1,1) [28607,0]. true => _t539 | ~_t538 [ Axiom T ] [ Backward Subsumption, 29983 ] % 4.26/4.41 (1,1) [28609,0]. true => _t540 | ~_t539 [ Axiom T ] [ Backward Subsumption, 29998 ] % 4.26/4.41 (1,1) [28611,0]. true => _t541 | ~_t540 [ Axiom T ] [ Backward Subsumption, 30025 ] % 4.26/4.41 (1,1) [28613,0]. true => _t542 | ~_t541 [ Axiom T ] [ Backward Subsumption, 30043 ] % 4.26/4.41 (1,1) [28615,0]. true => _t543 | ~_t542 [ Axiom T ] [ Backward Subsumption, 30071 ] % 4.26/4.41 (1,1) [28617,0]. true => _t544 | ~_t543 [ Axiom T ] [ Backward Subsumption, 30080 ] % 4.26/4.41 (1,1) [28618,0]. true => ~_t545 | p12 | p11 [ Axiom T ] [ Backward Subsumption, 30127 ] % 4.26/4.41 (1,1) [28619,0]. true => _t545 | ~_t544 [ Axiom T ] [ Backward Subsumption, 30104 ] % 4.26/4.41 (1,1) [28620,0]. true => ~_t546 | ~p12 | ~p11 [ Axiom T ] [ Backward Subsumption, 30120 ] % 4.26/4.41 (1,1) [28621,0]. true => _t546 | ~_t544 [ Axiom T ] [ Backward Subsumption, 30103 ] % 4.26/4.41 (1,1) [28622,0]. true => _t533 | ~_t532 [ Axiom T ] [ Backward Subsumption, 29837 ] % 4.26/4.41 (1,1) [28624,0]. true => _t548 | ~_t547 [ Axiom T ] [ Backward Subsumption, 29865 ] % 4.26/4.41 (1,1) [28626,0]. true => _t550 | ~_t549 [ Axiom T ] [ Backward Subsumption, 29905 ] % 4.26/4.41 (1,1) [28628,0]. true => _t551 | ~_t550 [ Axiom T ] [ Backward Subsumption, 29939 ] % 4.26/4.41 (1,1) [28630,0]. true => _t552 | ~_t551 [ Axiom T ] [ Backward Subsumption, 29948 ] % 4.26/4.41 (1,1) [28632,0]. true => _t553 | ~_t552 [ Axiom T ] [ Backward Subsumption, 29981 ] % 4.26/4.41 (1,1) [28634,0]. true => _t554 | ~_t553 [ Axiom T ] [ Backward Subsumption, 30011 ] % 4.26/4.41 (1,1) [28636,0]. true => _t555 | ~_t554 [ Axiom T ] [ Backward Subsumption, 30035 ] % 4.26/4.41 (1,1) [28638,0]. true => _t556 | ~_t555 [ Axiom T ] [ Backward Subsumption, 30038 ] % 4.26/4.41 (1,1) [28640,0]. true => _t557 | ~_t556 [ Axiom T ] [ Backward Subsumption, 30069 ] % 4.26/4.41 (1,1) [28642,0]. true => _t558 | ~_t557 [ Axiom T ] [ Backward Subsumption, 30093 ] % 4.26/4.41 (1,1) [28644,0]. true => _t559 | ~_t558 [ Axiom T ] [ Backward Subsumption, 30112 ] % 4.26/4.41 (1,1) [28645,0]. true => ~_t560 | p11 | p10 [ Axiom T ] [ Backward Subsumption, 30137 ] % 4.26/4.41 (1,1) [28646,0]. true => _t560 | ~_t559 [ Axiom T ] [ Backward Subsumption, 30115 ] % 4.26/4.41 (1,1) [28647,0]. true => ~_t561 | ~p11 | ~p10 [ Axiom T ] [ Backward Subsumption, 30138 ] % 4.26/4.41 (1,1) [28648,0]. true => _t561 | ~_t559 [ Axiom T ] [ Backward Subsumption, 30114 ] % 4.26/4.42 (1,1) [28649,0]. true => _t549 | ~_t548 [ Axiom T ] [ Backward Subsumption, 29869 ] % 4.26/4.42 (1,1) [28651,0]. true => _t563 | ~_t562 [ Axiom T ] [ Backward Subsumption, 29908 ] % 4.26/4.42 (1,1) [28653,0]. true => _t565 | ~_t564 [ Axiom T ] [ Backward Subsumption, 29962 ] % 4.26/4.42 (1,1) [28655,0]. true => _t566 | ~_t565 [ Axiom T ] [ Backward Subsumption, 29990 ] % 4.26/4.42 (1,1) [28657,0]. true => _t567 | ~_t566 [ Axiom T ] [ Backward Subsumption, 30015 ] % 4.26/4.42 (1,1) [28659,0]. true => _t568 | ~_t567 [ Axiom T ] [ Backward Subsumption, 30017 ] % 4.26/4.42 (1,1) [28661,0]. true => _t569 | ~_t568 [ Axiom T ] [ Backward Subsumption, 30048 ] % 4.26/4.42 (1,1) [28663,0]. true => _t570 | ~_t569 [ Axiom T ] [ Backward Subsumption, 30073 ] % 4.26/4.42 (1,1) [28665,0]. true => _t571 | ~_t570 [ Axiom T ] [ Backward Subsumption, 30095 ] % 4.26/4.42 (1,1) [28667,0]. true => _t572 | ~_t571 [ Axiom T ] [ Backward Subsumption, 30097 ] % 4.26/4.42 (1,1) [28669,0]. true => _t573 | ~_t572 [ Axiom T ] [ Backward Subsumption, 30123 ] % 4.26/4.42 (1,1) [28670,0]. true => ~_t574 | p10 | p9 [ Axiom T ] [ Backward Subsumption, 30151 ] % 4.26/4.42 (1,1) [28671,0]. true => _t574 | ~_t573 [ Axiom T ] [ Backward Subsumption, 30134 ] % 4.26/4.42 (1,1) [28672,0]. true => ~_t575 | ~p10 | ~p9 [ Axiom T ] [ Backward Subsumption, 30154 ] % 4.26/4.42 (1,1) [28673,0]. true => _t575 | ~_t573 [ Axiom T ] [ Backward Subsumption, 30133 ] % 4.26/4.42 (1,1) [28674,0]. true => _t564 | ~_t563 [ Axiom T ] [ Backward Subsumption, 29928 ] % 4.26/4.42 (1,1) [28676,0]. true => _t577 | ~_t576 [ Axiom T ] [ Backward Subsumption, 29955 ] % 4.26/4.42 (1,1) [28678,0]. true => _t579 | ~_t578 [ Axiom T ] [ Backward Subsumption, 30000 ] % 4.26/4.42 (1,1) [28680,0]. true => _t580 | ~_t579 [ Axiom T ] [ Backward Subsumption, 30031 ] % 4.26/4.42 (1,1) [28682,0]. true => _t581 | ~_t580 [ Axiom T ] [ Backward Subsumption, 30040 ] % 4.26/4.42 (1,1) [28684,0]. true => _t582 | ~_t581 [ Axiom T ] [ Backward Subsumption, 30067 ] % 4.26/4.42 (1,1) [28686,0]. true => _t583 | ~_t582 [ Axiom T ] [ Backward Subsumption, 30082 ] % 4.26/4.42 (1,1) [28688,0]. true => _t584 | ~_t583 [ Axiom T ] [ Backward Subsumption, 30107 ] % 4.26/4.42 (1,1) [28690,0]. true => _t585 | ~_t584 [ Axiom T ] [ Backward Subsumption, 30118 ] % 4.26/4.42 (1,1) [28692,0]. true => _t586 | ~_t585 [ Axiom T ] [ Backward Subsumption, 30135 ] % 4.26/4.42 (1,1) [28693,0]. true => ~_t587 | p9 | p8 [ Axiom T ] [ Backward Subsumption, 30163 ] % 4.26/4.42 (1,1) [28694,0]. true => _t587 | ~_t586 [ Axiom T ] [ Backward Subsumption, 30156 ] % 4.26/4.42 (1,1) [28695,0]. true => ~_t588 | ~p9 | ~p8 [ Axiom T ] [ Backward Subsumption, 30170 ] % 4.26/4.42 (1,1) [28696,0]. true => _t588 | ~_t586 [ Axiom T ] [ Backward Subsumption, 30155 ] % 4.26/4.42 (1,1) [28697,0]. true => _t578 | ~_t577 [ Axiom T ] [ Backward Subsumption, 29979 ] % 4.26/4.42 (1,1) [28699,0]. true => _t590 | ~_t589 [ Axiom T ] [ Backward Subsumption, 30009 ] % 4.26/4.42 (1,1) [28701,0]. true => _t592 | ~_t591 [ Axiom T ] [ Backward Subsumption, 30045 ] % 4.26/4.42 (1,1) [28703,0]. true => _t593 | ~_t592 [ Axiom T ] [ Backward Subsumption, 30065 ] % 4.26/4.42 (1,1) [28705,0]. true => _t594 | ~_t593 [ Axiom T ] [ Backward Subsumption, 30091 ] % 4.26/4.42 (1,1) [28707,0]. true => _t595 | ~_t594 [ Axiom T ] [ Backward Subsumption, 30099 ] % 4.26/4.42 (1,1) [28709,0]. true => _t596 | ~_t595 [ Axiom T ] [ Backward Subsumption, 30121 ] % 4.26/4.42 (1,1) [28711,0]. true => _t597 | ~_t596 [ Axiom T ] [ Backward Subsumption, 30142 ] % 4.26/4.42 (1,1) [28713,0]. true => _t598 | ~_t597 [ Axiom T ] [ Backward Subsumption, 30159 ] % 4.26/4.42 (1,1) [28714,0]. true => ~_t599 | p8 | p7 [ Axiom T ] [ Backward Subsumption, 30179 ] % 4.26/4.42 (1,1) [28715,0]. true => _t599 | ~_t598 [ Axiom T ] [ Backward Subsumption, 30162 ] % 4.26/4.42 (1,1) [28716,0]. true => ~_t600 | ~p8 | ~p7 [ Axiom T ] [ Backward Subsumption, 30180 ] % 4.26/4.42 (1,1) [28717,0]. true => _t600 | ~_t598 [ Axiom T ] [ Backward Subsumption, 30161 ] % 4.26/4.42 (1,1) [28718,0]. true => _t591 | ~_t590 [ Axiom T ] [ Backward Subsumption, 30022 ] % 4.26/4.42 (1,1) [28720,0]. true => _t602 | ~_t601 [ Axiom T ] [ Backward Subsumption, 30050 ] % 4.26/4.42 (1,1) [28722,0]. true => _t604 | ~_t603 [ Axiom T ] [ Backward Subsumption, 30084 ] % 4.26/4.42 (1,1) [28724,0]. true => _t605 | ~_t604 [ Axiom T ] [ Backward Subsumption, 30101 ] % 4.26/4.42 (1,1) [28726,0]. true => _t606 | ~_t605 [ Axiom T ] [ Backward Subsumption, 30125 ] % 4.26/4.42 (1,1) [28728,0]. true => _t607 | ~_t606 [ Axiom T ] [ Backward Subsumption, 30144 ] % 4.26/4.42 (1,1) [28730,0]. true => _t608 | ~_t607 [ Axiom T ] [ Backward Subsumption, 30146 ] % 4.26/4.42 (1,1) [28732,0]. true => _t609 | ~_t608 [ Axiom T ] [ Backward Subsumption, 30166 ] % 4.26/4.42 (1,1) [28733,0]. true => ~_t610 | p7 | p6 [ Axiom T ] [ Backward Subsumption, 30195 ] % 4.26/4.42 (1,1) [28734,0]. true => _t610 | ~_t609 [ Axiom T ] [ Backward Subsumption, 30178 ] % 4.26/4.42 (1,1) [28735,0]. true => ~_t611 | ~p7 | ~p6 [ Axiom T ] [ Backward Subsumption, 30192 ] % 4.26/4.42 (1,1) [28736,0]. true => _t611 | ~_t609 [ Axiom T ] [ Backward Subsumption, 30177 ] % 4.26/4.42 (1,1) [28737,0]. true => _t603 | ~_t602 [ Axiom T ] [ Backward Subsumption, 30064 ] % 4.26/4.42 (1,1) [28739,0]. true => _t613 | ~_t612 [ Axiom T ] [ Backward Subsumption, 30089 ] % 4.26/4.42 (1,1) [28741,0]. true => _t615 | ~_t614 [ Axiom T ] [ Backward Subsumption, 30129 ] % 4.26/4.42 (1,1) [28743,0]. true => _t616 | ~_t615 [ Axiom T ] [ Backward Subsumption, 30131 ] % 4.26/4.42 (1,1) [28745,0]. true => _t617 | ~_t616 [ Axiom T ] [ Backward Subsumption, 30152 ] % 4.26/4.42 (1,1) [28747,0]. true => _t618 | ~_t617 [ Axiom T ] [ Backward Subsumption, 30164 ] % 4.26/4.42 (1,1) [28749,0]. true => _t619 | ~_t618 [ Axiom T ] [ Backward Subsumption, 30181 ] % 4.26/4.42 (1,1) [28750,0]. true => ~_t620 | p6 | p5 [ Axiom T ] [ Backward Subsumption, 30200 ] % 4.26/4.42 (1,1) [28751,0]. true => _t620 | ~_t619 [ Axiom T ] [ Backward Subsumption, 30191 ] % 4.26/4.42 (1,1) [28752,0]. true => ~_t621 | ~p6 | ~p5 [ Axiom T ] [ Backward Subsumption, 30206 ] % 4.26/4.42 (1,1) [28753,0]. true => _t621 | ~_t619 [ Axiom T ] [ Backward Subsumption, 30190 ] % 4.26/4.42 (1,1) [28754,0]. true => _t614 | ~_t613 [ Axiom T ] [ Backward Subsumption, 30111 ] % 4.26/4.42 (1,1) [28756,0]. true => _t623 | ~_t622 [ Axiom T ] [ Backward Subsumption, 30116 ] % 4.26/4.42 (1,1) [28758,0]. true => _t625 | ~_t624 [ Axiom T ] [ Backward Subsumption, 30148 ] % 4.26/4.42 (1,1) [28760,0]. true => _t626 | ~_t625 [ Axiom T ] [ Backward Subsumption, 30168 ] % 4.26/4.42 (1,1) [28762,0]. true => _t627 | ~_t626 [ Axiom T ] [ Backward Subsumption, 30183 ] % 4.26/4.42 (1,1) [28764,0]. true => _t628 | ~_t627 [ Axiom T ] [ Backward Subsumption, 30196 ] % 4.26/4.42 (1,1) [28765,0]. true => ~_t629 | p5 | p4 [ Axiom T ] [ Backward Subsumption, 30214 ] % 4.26/4.42 (1,1) [28766,0]. true => _t629 | ~_t628 [ Axiom T ] [ Backward Subsumption, 30199 ] % 4.26/4.42 (1,1) [28767,0]. true => ~_t630 | ~p5 | ~p4 [ Axiom T ] [ Backward Subsumption, 30213 ] % 4.26/4.42 (1,1) [28768,0]. true => _t630 | ~_t628 [ Axiom T ] [ Backward Subsumption, 30198 ] % 4.26/4.42 (1,1) [28769,0]. true => _t624 | ~_t623 [ Axiom T ] [ Backward Subsumption, 30141 ] % 4.26/4.42 (1,1) [28771,0]. true => _t632 | ~_t631 [ Axiom T ] [ Backward Subsumption, 30157 ] % 4.26/4.42 (1,1) [28773,0]. true => _t634 | ~_t633 [ Axiom T ] [ Backward Subsumption, 30174 ] % 4.26/4.42 (1,1) [28775,0]. true => _t635 | ~_t634 [ Axiom T ] [ Backward Subsumption, 30193 ] % 4.26/4.42 (1,1) [28777,0]. true => _t636 | ~_t635 [ Axiom T ] [ Backward Subsumption, 30207 ] % 4.26/4.42 (1,1) [28778,0]. true => ~_t637 | p4 | p3 [ Axiom T ] [ Backward Subsumption, 30219 ] % 4.26/4.42 (1,1) [28779,0]. true => _t637 | ~_t636 [ Axiom T ] [ Backward Subsumption, 30210 ] % 4.26/4.42 (1,1) [28780,0]. true => ~_t638 | ~p4 | ~p3 [ Axiom T ] [ Backward Subsumption, 30220 ] % 4.26/4.42 (1,1) [28781,0]. true => _t638 | ~_t636 [ Axiom T ] [ Backward Subsumption, 30209 ] % 4.26/4.42 (1,1) [28782,0]. true => _t633 | ~_t632 [ Axiom T ] [ Backward Subsumption, 30173 ] % 4.26/4.42 (1,1) [28784,0]. true => _t640 | ~_t639 [ Axiom T ] [ Backward Subsumption, 30185 ] % 4.26/4.42 (1,1) [28786,0]. true => _t642 | ~_t641 [ Axiom T ] [ Backward Subsumption, 30201 ] % 4.26/4.42 (1,1) [28788,0]. true => _t643 | ~_t642 [ Axiom T ] [ Backward Subsumption, 30211 ] % 4.26/4.42 (1,1) [28789,0]. true => ~_t644 | p3 | p2 [ Axiom T ] [ Backward Subsumption, 30223 ] % 4.26/4.42 (1,1) [28790,0]. true => _t644 | ~_t643 [ Axiom T ] [ Backward Subsumption, 30222 ] % 4.26/4.42 (1,1) [28791,0]. true => ~_t645 | ~p3 | ~p2 [ Axiom T ] [ Backward Subsumption, 30226 ] % 4.26/4.42 (1,1) [28792,0]. true => _t645 | ~_t643 [ Axiom T ] [ Backward Subsumption, 30221 ] % 4.26/4.42 (1,1) [28793,0]. true => _t641 | ~_t640 [ Axiom T ] [ Backward Subsumption, 30189 ] % 4.26/4.42 (1,1) [28795,0]. true => _t647 | ~_t646 [ Axiom T ] [ Backward Subsumption, 30204 ] % 4.26/4.42 (1,1) [28797,0]. true => _t648 | ~_t647 [ Axiom T ] [ Backward Subsumption, 30215 ] % 4.26/4.42 (1,1) [28798,0]. true => ~_t649 | p2 | p1 [ Axiom T ] [ Backward Subsumption, 30224 ] % 4.26/4.42 (1,1) [28799,0]. true => _t649 | ~_t648 [ Axiom T ] [ Backward Subsumption, 30218 ] % 4.26/4.42 (1,1) [28800,0]. true => ~_t650 | ~p2 | ~p1 [ Axiom T ] [ Backward Subsumption, 30225 ] % 4.26/4.42 (1,1) [28801,0]. true => _t650 | ~_t648 [ Axiom T ] [ Backward Subsumption, 30217 ] % 4.26/4.42 (1,1) [28802,0]. true => _t646 | ~_t640 [ Axiom T ] [ Backward Subsumption, 30188 ] % 4.26/4.42 (1,1) [28805,0]. true => _t639 | ~_t632 [ Axiom T ] [ Backward Subsumption, 30172 ] % 4.26/4.42 (1,1) [28808,0]. true => _t631 | ~_t623 [ Axiom T ] [ Backward Subsumption, 30140 ] % 4.26/4.42 (1,1) [28811,0]. true => _t622 | ~_t613 [ Axiom T ] [ Backward Subsumption, 30110 ] % 4.26/4.42 (1,1) [28814,0]. true => _t612 | ~_t602 [ Axiom T ] [ Backward Subsumption, 30063 ] % 4.26/4.42 (1,1) [28817,0]. true => _t601 | ~_t590 [ Axiom T ] [ Backward Subsumption, 30021 ] % 4.26/4.42 (1,1) [28820,0]. true => _t589 | ~_t577 [ Axiom T ] [ Backward Subsumption, 29978 ] % 4.26/4.42 (1,1) [28823,0]. true => _t576 | ~_t563 [ Axiom T ] [ Backward Subsumption, 29927 ] % 4.26/4.42 (1,1) [28826,0]. true => _t562 | ~_t548 [ Axiom T ] [ Backward Subsumption, 29868 ] % 4.26/4.42 (1,1) [28829,0]. true => _t547 | ~_t532 [ Axiom T ] [ Backward Subsumption, 29836 ] % 4.26/4.42 (1,1) [28832,0]. true => _t531 | ~_t515 [ Axiom T ] [ Backward Subsumption, 29772 ] % 4.26/4.42 (1,1) [28835,0]. true => _t514 | ~_t497 [ Axiom T ] [ Backward Subsumption, 29688 ] % 4.26/4.42 (1,1) [28838,0]. true => _t496 | ~_t478 [ Axiom T ] [ Backward Subsumption, 29617 ] % 4.26/4.42 (1,1) [28841,0]. true => _t477 | ~_t458 [ Axiom T ] [ Backward Subsumption, 29550 ] % 4.26/4.42 (1,1) [28844,0]. true => _t457 | ~_t437 [ Axiom T ] [ Backward Subsumption, 29480 ] % 4.26/4.42 (1,1) [28847,0]. true => _t436 | ~_t415 [ Axiom T ] [ Backward Subsumption, 29410 ] % 4.26/4.42 (1,1) [28850,0]. true => _t414 | ~_t392 [ Axiom T ] [ Backward Subsumption, 29366 ] % 4.26/4.42 (1,1) [28853,0]. true => _t391 | ~_t368 [ Axiom T ] [ Backward Subsumption, 29302 ] % 4.26/4.42 (1,1) [28856,0]. true => _t367 | ~_t343 [ Axiom T ] [ Backward Subsumption, 29256 ] % 4.26/4.42 (1,1) [28859,0]. true => _t342 | ~_t317 [ Axiom T ] [ Backward Subsumption, 29198 ] % 4.26/4.42 (1,1) [28862,0]. true => _t316 | ~_t290 [ Axiom T ] [ Backward Subsumption, 29152 ] % 4.26/4.42 (1,1) [28865,0]. true => _t289 | ~_t262 [ Axiom T ] [ Backward Subsumption, 29108 ] % 4.26/4.42 (1,1) [28868,0]. true => _t261 | ~_t233 [ Axiom T ] [ Backward Subsumption, 29086 ] % 4.26/4.42 (1,1) [28871,0]. true => _t232 | ~_t203 [ Axiom T ] [ Backward Subsumption, 29048 ] % 4.26/4.42 (1,1) [28874,0]. true => _t202 | ~_t172 [ Axiom T ] [ Backward Subsumption, 29020 ] % 4.26/4.42 (1,1) [28877,0]. true => _t171 | ~_t140 [ Axiom T ] [ Backward Subsumption, 28990 ] % 4.26/4.42 (1,1) [28880,0]. true => _t139 | ~_t107 [ Axiom T ] [ Backward Subsumption, 28968 ] % 4.26/4.42 (1,1) [28883,0]. true => _t106 | ~_t73 [ Axiom T ] [ Backward Subsumption, 28956 ] % 4.26/4.42 (1,1) [28886,0]. true => _t72 | ~_t38 [ Axiom T ] [ Backward Subsumption, 28940 ] % 4.26/4.42 (1,1) [28889,0]. true => _t37 | ~_t2 [ Axiom T ] [ Backward Subsumption, 28932 ] % 4.26/4.42 (1,1) [28892,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 28927 ] % 4.26/4.42 (1,1) [28927,0]. true => _t1 [ Unit Resolution, 3, 28892, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 4.26/4.42 (1,1) [28928,0]. true => _t2 [ Unit Resolution, 28927, 27595, _t1 ] [ Modal Level Pure Literal Elimination, _t2 ] % 4.26/4.42 (1,1) [28932,0]. true => _t37 [ Unit Resolution, 28928, 28889, _t2 ] [ Modal Level Pure Literal Elimination, _t37 ] % 4.26/4.42 (1,1) [28933,0]. true => _t3 [ Unit Resolution, 28928, 27662, _t2 ] [ Modal Level Pure Literal Elimination, _t3 ] % 4.26/4.42 (1,1) [28934,0]. true => _t4 [ Unit Resolution, 28933, 27597, _t3 ] [ Modal Level Pure Literal Elimination, _t4 ] % 4.26/4.42 (1,1) [28937,0]. true => _t38 [ Unit Resolution, 28932, 27664, _t37 ] [ Modal Level Pure Literal Elimination, _t38 ] % 4.26/4.42 (1,1) [28940,0]. true => _t72 [ Unit Resolution, 28937, 28886, _t38 ] [ Modal Level Pure Literal Elimination, _t72 ] % 4.26/4.42 (1,1) [28941,0]. true => _t39 [ Unit Resolution, 28937, 27729, _t38 ] [ Modal Level Pure Literal Elimination, _t39 ] % 4.26/4.42 (1,1) [28942,0]. true => _t5 [ Unit Resolution, 28934, 27599, _t4 ] [ Modal Level Pure Literal Elimination, _t5 ] % 4.26/4.42 (1,1) [28944,0]. true => _t6 [ Unit Resolution, 28942, 27601, _t5 ] [ Modal Level Pure Literal Elimination, _t6 ] % 4.26/4.42 (1,1) [28946,0]. true => _t73 [ Unit Resolution, 28940, 27731, _t72 ] [ Modal Level Pure Literal Elimination, _t73 ] % 4.26/4.42 (1,1) [28949,0]. true => _t40 [ Unit Resolution, 28941, 27666, _t39 ] [ Modal Level Pure Literal Elimination, _t40 ] % 4.26/4.42 (1,1) [28951,0]. true => _t41 [ Unit Resolution, 28949, 27668, _t40 ] [ Modal Level Pure Literal Elimination, _t41 ] % 4.26/4.42 (1,1) [28953,0]. true => _t7 [ Unit Resolution, 28944, 27603, _t6 ] [ Modal Level Pure Literal Elimination, _t7 ] % 4.26/4.42 (1,1) [28956,0]. true => _t106 [ Unit Resolution, 28946, 28883, _t73 ] [ Modal Level Pure Literal Elimination, _t106 ] % 4.26/4.42 (1,1) [28957,0]. true => _t74 [ Unit Resolution, 28946, 27794, _t73 ] [ Modal Level Pure Literal Elimination, _t74 ] % 4.26/4.42 (1,1) [28958,0]. true => _t75 [ Unit Resolution, 28957, 27733, _t74 ] [ Modal Level Pure Literal Elimination, _t75 ] % 4.26/4.42 (1,1) [28961,0]. true => _t42 [ Unit Resolution, 28951, 27670, _t41 ] [ Modal Level Pure Literal Elimination, _t42 ] % 4.26/4.42 (1,1) [28963,0]. true => _t8 [ Unit Resolution, 28953, 27605, _t7 ] [ Modal Level Pure Literal Elimination, _t8 ] % 4.26/4.42 (1,1) [28965,0]. true => _t107 [ Unit Resolution, 28956, 27796, _t106 ] [ Modal Level Pure Literal Elimination, _t107 ] % 4.26/4.42 (1,1) [28968,0]. true => _t139 [ Unit Resolution, 28965, 28880, _t107 ] [ Modal Level Pure Literal Elimination, _t139 ] % 4.26/4.42 (1,1) [28969,0]. true => _t108 [ Unit Resolution, 28965, 27857, _t107 ] [ Modal Level Pure Literal Elimination, _t108 ] % 4.26/4.42 (1,1) [28970,0]. true => _t43 [ Unit Resolution, 28961, 27672, _t42 ] [ Modal Level Pure Literal Elimination, _t43 ] % 4.26/4.42 (1,1) [28972,0]. true => _t76 [ Unit Resolution, 28958, 27735, _t75 ] [ Modal Level Pure Literal Elimination, _t76 ] % 4.26/4.42 (1,1) [28974,0]. true => _t9 [ Unit Resolution, 28963, 27607, _t8 ] [ Modal Level Pure Literal Elimination, _t9 ] % 4.26/4.42 (1,1) [28976,0]. true => _t10 [ Unit Resolution, 28974, 27609, _t9 ] [ Modal Level Pure Literal Elimination, _t10 ] % 4.26/4.42 (1,1) [28978,0]. true => _t44 [ Unit Resolution, 28970, 27674, _t43 ] [ Modal Level Pure Literal Elimination, _t44 ] % 4.26/4.42 (1,1) [28980,0]. true => _t140 [ Unit Resolution, 28968, 27859, _t139 ] [ Modal Level Pure Literal Elimination, _t140 ] % 4.26/4.42 (1,1) [28983,0]. true => _t109 [ Unit Resolution, 28969, 27798, _t108 ] [ Modal Level Pure Literal Elimination, _t109 ] % 4.26/4.42 (1,1) [28985,0]. true => _t77 [ Unit Resolution, 28972, 27737, _t76 ] [ Modal Level Pure Literal Elimination, _t77 ] % 4.26/4.42 (1,1) [28987,0]. true => _t78 [ Unit Resolution, 28985, 27739, _t77 ] [ Modal Level Pure Literal Elimination, _t78 ] % 4.26/4.42 (1,1) [28990,0]. true => _t171 [ Unit Resolution, 28980, 28877, _t140 ] [ Modal Level Pure Literal Elimination, _t171 ] % 4.26/4.42 (1,1) [28991,0]. true => _t141 [ Unit Resolution, 28980, 27918, _t140 ] [ Modal Level Pure Literal Elimination, _t141 ] % 4.26/4.42 (1,1) [28992,0]. true => _t11 [ Unit Resolution, 28976, 27611, _t10 ] [ Modal Level Pure Literal Elimination, _t11 ] % 4.26/4.42 (1,1) [28994,0]. true => _t45 [ Unit Resolution, 28978, 27676, _t44 ] [ Modal Level Pure Literal Elimination, _t45 ] % 4.26/4.42 (1,1) [28996,0]. true => _t110 [ Unit Resolution, 28983, 27800, _t109 ] [ Modal Level Pure Literal Elimination, _t110 ] % 4.26/4.42 (1,1) [28998,0]. true => _t111 [ Unit Resolution, 28996, 27802, _t110 ] [ Modal Level Pure Literal Elimination, _t111 ] % 4.26/4.42 (1,1) [29000,0]. true => _t12 [ Unit Resolution, 28992, 27613, _t11 ] [ Modal Level Pure Literal Elimination, _t12 ] % 4.26/4.42 (1,1) [29002,0]. true => _t172 [ Unit Resolution, 28990, 27920, _t171 ] [ Modal Level Pure Literal Elimination, _t172 ] % 4.26/4.42 (1,1) [29004,0]. true => _t79 [ Unit Resolution, 28987, 27741, _t78 ] [ Modal Level Pure Literal Elimination, _t79 ] % 4.26/4.42 (1,1) [29007,0]. true => _t142 [ Unit Resolution, 28991, 27861, _t141 ] [ Modal Level Pure Literal Elimination, _t142 ] % 4.26/4.42 (1,1) [29009,0]. true => _t46 [ Unit Resolution, 28994, 27678, _t45 ] [ Modal Level Pure Literal Elimination, _t46 ] % 4.26/4.42 (1,1) [29011,0]. true => _t47 [ Unit Resolution, 29009, 27680, _t46 ] [ Modal Level Pure Literal Elimination, _t47 ] % 4.26/4.42 (1,1) [29013,0]. true => _t80 [ Unit Resolution, 29004, 27743, _t79 ] [ Modal Level Pure Literal Elimination, _t80 ] % 4.26/4.42 (1,1) [29015,0]. true => _t13 [ Unit Resolution, 29000, 27615, _t12 ] [ Modal Level Pure Literal Elimination, _t13 ] % 4.26/4.42 (1,1) [29017,0]. true => _t112 [ Unit Resolution, 28998, 27804, _t111 ] [ Modal Level Pure Literal Elimination, _t112 ] % 4.26/4.42 (1,1) [29020,0]. true => _t202 [ Unit Resolution, 29002, 28874, _t172 ] [ Modal Level Pure Literal Elimination, _t202 ] % 4.26/4.42 (1,1) [29021,0]. true => _t173 [ Unit Resolution, 29002, 27977, _t172 ] [ Modal Level Pure Literal Elimination, _t173 ] % 4.26/4.42 (1,1) [29022,0]. true => _t143 [ Unit Resolution, 29007, 27863, _t142 ] [ Modal Level Pure Literal Elimination, _t143 ] % 4.26/4.42 (1,1) [29024,0]. true => _t144 [ Unit Resolution, 29022, 27865, _t143 ] [ Modal Level Pure Literal Elimination, _t144 ] % 4.26/4.42 (1,1) [29026,0]. true => _t203 [ Unit Resolution, 29020, 27979, _t202 ] [ Modal Level Pure Literal Elimination, _t203 ] % 4.26/4.42 (1,1) [29028,0]. true => _t113 [ Unit Resolution, 29017, 27806, _t112 ] [ Modal Level Pure Literal Elimination, _t113 ] % 4.26/4.42 (1,1) [29030,0]. true => _t81 [ Unit Resolution, 29013, 27745, _t80 ] [ Modal Level Pure Literal Elimination, _t81 ] % 4.26/4.42 (1,1) [29032,0]. true => _t48 [ Unit Resolution, 29011, 27682, _t47 ] [ Modal Level Pure Literal Elimination, _t48 ] % 4.26/4.42 (1,1) [29034,0]. true => _t14 [ Unit Resolution, 29015, 27617, _t13 ] [ Modal Level Pure Literal Elimination, _t14 ] % 4.26/4.42 (1,1) [29037,0]. true => _t174 [ Unit Resolution, 29021, 27922, _t173 ] [ Modal Level Pure Literal Elimination, _t174 ] % 4.26/4.42 (1,1) [29039,0]. true => _t175 [ Unit Resolution, 29037, 27924, _t174 ] [ Modal Level Pure Literal Elimination, _t175 ] % 4.26/4.42 (1,1) [29041,0]. true => _t49 [ Unit Resolution, 29032, 27684, _t48 ] [ Modal Level Pure Literal Elimination, _t49 ] % 4.26/4.42 (1,1) [29043,0]. true => _t114 [ Unit Resolution, 29028, 27808, _t113 ] [ Modal Level Pure Literal Elimination, _t114 ] % 4.26/4.42 (1,1) [29045,0]. true => _t145 [ Unit Resolution, 29024, 27867, _t144 ] [ Modal Level Pure Literal Elimination, _t145 ] % 4.26/4.42 (1,1) [29048,0]. true => _t232 [ Unit Resolution, 29026, 28871, _t203 ] [ Modal Level Pure Literal Elimination, _t232 ] % 4.26/4.42 (1,1) [29049,0]. true => _t204 [ Unit Resolution, 29026, 28034, _t203 ] [ Modal Level Pure Literal Elimination, _t204 ] % 4.26/4.42 (1,1) [29050,0]. true => _t82 [ Unit Resolution, 29030, 27747, _t81 ] [ Modal Level Pure Literal Elimination, _t82 ] % 4.26/4.42 (1,1) [29052,0]. true => _t15 [ Unit Resolution, 29034, 27619, _t14 ] [ Modal Level Pure Literal Elimination, _t15 ] % 4.26/4.42 (1,1) [29054,0]. true => _t16 [ Unit Resolution, 29052, 27621, _t15 ] [ Modal Level Pure Literal Elimination, _t16 ] % 4.26/4.42 (1,1) [29056,0]. true => _t205 [ Unit Resolution, 29049, 27981, _t204 ] [ Modal Level Pure Literal Elimination, _t205 ] % 4.26/4.42 (1,1) [29059,0]. true => _t115 [ Unit Resolution, 29043, 27810, _t114 ] [ Modal Level Pure Literal Elimination, _t115 ] % 4.26/4.42 (1,1) [29061,0]. true => _t176 [ Unit Resolution, 29039, 27926, _t175 ] [ Modal Level Pure Literal Elimination, _t176 ] % 4.26/4.42 (1,1) [29063,0]. true => _t50 [ Unit Resolution, 29041, 27686, _t49 ] [ Modal Level Pure Literal Elimination, _t50 ] % 4.26/4.42 (1,1) [29065,0]. true => _t146 [ Unit Resolution, 29045, 27869, _t145 ] [ Modal Level Pure Literal Elimination, _t146 ] % 4.26/4.42 (1,1) [29067,0]. true => _t233 [ Unit Resolution, 29048, 28036, _t232 ] [ Modal Level Pure Literal Elimination, _t233 ] % 4.26/4.42 (1,1) [29069,0]. true => _t83 [ Unit Resolution, 29050, 27749, _t82 ] [ Modal Level Pure Literal Elimination, _t83 ] % 4.26/4.42 (1,1) [29071,0]. true => _t84 [ Unit Resolution, 29069, 27751, _t83 ] [ Modal Level Pure Literal Elimination, _t84 ] % 4.26/4.42 (1,1) [29073,0]. true => _t147 [ Unit Resolution, 29065, 27871, _t146 ] [ Modal Level Pure Literal Elimination, _t147 ] % 4.26/4.42 (1,1) [29075,0]. true => _t177 [ Unit Resolution, 29061, 27928, _t176 ] [ Modal Level Pure Literal Elimination, _t177 ] % 4.26/4.42 (1,1) [29077,0]. true => _t206 [ Unit Resolution, 29056, 27983, _t205 ] [ Modal Level Pure Literal Elimination, _t206 ] % 4.26/4.42 (1,1) [29079,0]. true => _t17 [ Unit Resolution, 29054, 27623, _t16 ] [ Modal Level Pure Literal Elimination, _t17 ] % 4.26/4.42 (1,1) [29081,0]. true => _t116 [ Unit Resolution, 29059, 27812, _t115 ] [ Modal Level Pure Literal Elimination, _t116 ] % 4.26/4.42 (1,1) [29083,0]. true => _t51 [ Unit Resolution, 29063, 27688, _t50 ] [ Modal Level Pure Literal Elimination, _t51 ] % 4.26/4.42 (1,1) [29086,0]. true => _t261 [ Unit Resolution, 29067, 28868, _t233 ] [ Modal Level Pure Literal Elimination, _t261 ] % 4.26/4.42 (1,1) [29087,0]. true => _t234 [ Unit Resolution, 29067, 28089, _t233 ] [ Modal Level Pure Literal Elimination, _t234 ] % 4.26/4.42 (1,1) [29088,0]. true => _t235 [ Unit Resolution, 29087, 28038, _t234 ] [ Modal Level Pure Literal Elimination, _t235 ] % 4.26/4.42 (1,1) [29091,0]. true => _t117 [ Unit Resolution, 29081, 27814, _t116 ] [ Modal Level Pure Literal Elimination, _t117 ] % 4.26/4.42 (1,1) [29093,0]. true => _t207 [ Unit Resolution, 29077, 27985, _t206 ] [ Modal Level Pure Literal Elimination, _t207 ] % 4.26/4.42 (1,1) [29095,0]. true => _t148 [ Unit Resolution, 29073, 27873, _t147 ] [ Modal Level Pure Literal Elimination, _t148 ] % 4.26/4.42 (1,1) [29097,0]. true => _t85 [ Unit Resolution, 29071, 27753, _t84 ] [ Modal Level Pure Literal Elimination, _t85 ] % 4.26/4.42 (1,1) [29099,0]. true => _t178 [ Unit Resolution, 29075, 27930, _t177 ] [ Modal Level Pure Literal Elimination, _t178 ] % 4.26/4.42 (1,1) [29101,0]. true => _t18 [ Unit Resolution, 29079, 27625, _t17 ] [ Modal Level Pure Literal Elimination, _t18 ] % 4.26/4.42 (1,1) [29103,0]. true => _t52 [ Unit Resolution, 29083, 27690, _t51 ] [ Modal Level Pure Literal Elimination, _t52 ] % 4.26/4.42 (1,1) [29105,0]. true => _t262 [ Unit Resolution, 29086, 28091, _t261 ] [ Modal Level Pure Literal Elimination, _t262 ] % 4.26/4.42 (1,1) [29108,0]. true => _t289 [ Unit Resolution, 29105, 28865, _t262 ] [ Modal Level Pure Literal Elimination, _t289 ] % 4.26/4.42 (1,1) [29109,0]. true => _t263 [ Unit Resolution, 29105, 28142, _t262 ] [ Modal Level Pure Literal Elimination, _t263 ] % 4.26/4.42 (1,1) [29110,0]. true => _t19 [ Unit Resolution, 29101, 27627, _t18 ] [ Modal Level Pure Literal Elimination, _t19 ] % 4.26/4.42 (1,1) [29112,0]. true => _t86 [ Unit Resolution, 29097, 27755, _t85 ] [ Modal Level Pure Literal Elimination, _t86 ] % 4.26/4.42 (1,1) [29114,0]. true => _t208 [ Unit Resolution, 29093, 27987, _t207 ] [ Modal Level Pure Literal Elimination, _t208 ] % 4.26/4.42 (1,1) [29116,0]. true => _t236 [ Unit Resolution, 29088, 28040, _t235 ] [ Modal Level Pure Literal Elimination, _t236 ] % 4.26/4.42 (1,1) [29118,0]. true => _t118 [ Unit Resolution, 29091, 27816, _t117 ] [ Modal Level Pure Literal Elimination, _t118 ] % 4.26/4.42 (1,1) [29120,0]. true => _t149 [ Unit Resolution, 29095, 27875, _t148 ] [ Modal Level Pure Literal Elimination, _t149 ] % 4.26/4.42 (1,1) [29122,0]. true => _t179 [ Unit Resolution, 29099, 27932, _t178 ] [ Modal Level Pure Literal Elimination, _t179 ] % 4.26/4.42 (1,1) [29124,0]. true => _t53 [ Unit Resolution, 29103, 27692, _t52 ] [ Modal Level Pure Literal Elimination, _t53 ] % 4.26/4.42 (1,1) [29126,0]. true => _t54 [ Unit Resolution, 29124, 27694, _t53 ] [ Modal Level Pure Literal Elimination, _t54 ] % 4.26/4.42 (1,1) [29128,0]. true => _t150 [ Unit Resolution, 29120, 27877, _t149 ] [ Modal Level Pure Literal Elimination, _t150 ] % 4.26/4.42 (1,1) [29130,0]. true => _t237 [ Unit Resolution, 29116, 28042, _t236 ] [ Modal Level Pure Literal Elimination, _t237 ] % 4.26/4.42 (1,1) [29132,0]. true => _t87 [ Unit Resolution, 29112, 27757, _t86 ] [ Modal Level Pure Literal Elimination, _t87 ] % 4.26/4.42 (1,1) [29134,0]. true => _t264 [ Unit Resolution, 29109, 28093, _t263 ] [ Modal Level Pure Literal Elimination, _t264 ] % 4.26/4.42 (1,1) [29137,0]. true => _t290 [ Unit Resolution, 29108, 28144, _t289 ] [ Modal Level Pure Literal Elimination, _t290 ] % 4.26/4.42 (1,1) [29139,0]. true => _t20 [ Unit Resolution, 29110, 27629, _t19 ] [ Modal Level Pure Literal Elimination, _t20 ] % 4.26/4.42 (1,1) [29141,0]. true => _t209 [ Unit Resolution, 29114, 27989, _t208 ] [ Modal Level Pure Literal Elimination, _t209 ] % 4.26/4.42 (1,1) [29143,0]. true => _t119 [ Unit Resolution, 29118, 27818, _t118 ] [ Modal Level Pure Literal Elimination, _t119 ] % 4.26/4.42 (1,1) [29145,0]. true => _t180 [ Unit Resolution, 29122, 27934, _t179 ] [ Modal Level Pure Literal Elimination, _t180 ] % 4.26/4.42 (1,1) [29147,0]. true => _t181 [ Unit Resolution, 29145, 27936, _t180 ] [ Modal Level Pure Literal Elimination, _t181 ] % 4.26/4.42 (1,1) [29149,0]. true => _t210 [ Unit Resolution, 29141, 27991, _t209 ] [ Modal Level Pure Literal Elimination, _t210 ] % 4.26/4.42 (1,1) [29152,0]. true => _t316 [ Unit Resolution, 29137, 28862, _t290 ] [ Modal Level Pure Literal Elimination, _t316 ] % 4.26/4.42 (1,1) [29153,0]. true => _t291 [ Unit Resolution, 29137, 28193, _t290 ] [ Modal Level Pure Literal Elimination, _t291 ] % 4.26/4.42 (1,1) [29154,0]. true => _t88 [ Unit Resolution, 29132, 27759, _t87 ] [ Modal Level Pure Literal Elimination, _t88 ] % 4.26/4.42 (1,1) [29156,0]. true => _t151 [ Unit Resolution, 29128, 27879, _t150 ] [ Modal Level Pure Literal Elimination, _t151 ] % 4.26/4.42 (1,1) [29158,0]. true => _t55 [ Unit Resolution, 29126, 27696, _t54 ] [ Modal Level Pure Literal Elimination, _t55 ] % 4.26/4.42 (1,1) [29160,0]. true => _t238 [ Unit Resolution, 29130, 28044, _t237 ] [ Modal Level Pure Literal Elimination, _t238 ] % 4.26/4.42 (1,1) [29162,0]. true => _t265 [ Unit Resolution, 29134, 28095, _t264 ] [ Modal Level Pure Literal Elimination, _t265 ] % 4.26/4.42 (1,1) [29164,0]. true => _t21 [ Unit Resolution, 29139, 27631, _t20 ] [ Modal Level Pure Literal Elimination, _t21 ] % 4.26/4.42 (1,1) [29166,0]. true => _t120 [ Unit Resolution, 29143, 27820, _t119 ] [ Modal Level Pure Literal Elimination, _t120 ] % 4.26/4.42 (1,1) [29168,0]. true => _t121 [ Unit Resolution, 29166, 27822, _t120 ] [ Modal Level Pure Literal Elimination, _t121 ] % 4.26/4.42 (1,1) [29170,0]. true => _t266 [ Unit Resolution, 29162, 28097, _t265 ] [ Modal Level Pure Literal Elimination, _t266 ] % 4.26/4.42 (1,1) [29172,0]. true => _t56 [ Unit Resolution, 29158, 27698, _t55 ] [ Modal Level Pure Literal Elimination, _t56 ] % 4.26/4.42 (1,1) [29174,0]. true => _t89 [ Unit Resolution, 29154, 27761, _t88 ] [ Modal Level Pure Literal Elimination, _t89 ] % 4.26/4.42 (1,1) [29176,0]. true => _t317 [ Unit Resolution, 29152, 28195, _t316 ] [ Modal Level Pure Literal Elimination, _t317 ] % 4.26/4.42 (1,1) [29178,0]. true => _t211 [ Unit Resolution, 29149, 27993, _t210 ] [ Modal Level Pure Literal Elimination, _t211 ] % 4.26/4.42 (1,1) [29180,0]. true => _t182 [ Unit Resolution, 29147, 27938, _t181 ] [ Modal Level Pure Literal Elimination, _t182 ] % 4.26/4.42 (1,1) [29183,0]. true => _t292 [ Unit Resolution, 29153, 28146, _t291 ] [ Modal Level Pure Literal Elimination, _t292 ] % 4.26/4.42 (1,1) [29185,0]. true => _t152 [ Unit Resolution, 29156, 27881, _t151 ] [ Modal Level Pure Literal Elimination, _t152 ] % 4.26/4.42 (1,1) [29187,0]. true => _t239 [ Unit Resolution, 29160, 28046, _t238 ] [ Modal Level Pure Literal Elimination, _t239 ] % 4.26/4.42 (1,1) [29189,0]. true => _t22 [ Unit Resolution, 29164, 27633, _t21 ] [ Modal Level Pure Literal Elimination, _t22 ] % 4.26/4.42 (1,1) [29191,0]. true => _t23 [ Unit Resolution, 29189, 27635, _t22 ] [ Modal Level Pure Literal Elimination, _t23 ] % 4.26/4.42 (1,1) [29193,0]. true => _t153 [ Unit Resolution, 29185, 27883, _t152 ] [ Modal Level Pure Literal Elimination, _t153 ] % 4.26/4.42 (1,1) [29195,0]. true => _t183 [ Unit Resolution, 29180, 27940, _t182 ] [ Modal Level Pure Literal Elimination, _t183 ] % 4.26/4.42 (1,1) [29198,0]. true => _t342 [ Unit Resolution, 29176, 28859, _t317 ] [ Modal Level Pure Literal Elimination, _t342 ] % 4.26/4.42 (1,1) [29199,0]. true => _t318 [ Unit Resolution, 29176, 28242, _t317 ] [ Modal Level Pure Literal Elimination, _t318 ] % 4.26/4.42 (1,1) [29200,0]. true => _t57 [ Unit Resolution, 29172, 27700, _t56 ] [ Modal Level Pure Literal Elimination, _t57 ] % 4.26/4.42 (1,1) [29202,0]. true => _t122 [ Unit Resolution, 29168, 27824, _t121 ] [ Modal Level Pure Literal Elimination, _t122 ] % 4.26/4.42 (1,1) [29204,0]. true => _t267 [ Unit Resolution, 29170, 28099, _t266 ] [ Modal Level Pure Literal Elimination, _t267 ] % 4.26/4.42 (1,1) [29206,0]. true => _t90 [ Unit Resolution, 29174, 27763, _t89 ] [ Modal Level Pure Literal Elimination, _t90 ] % 4.26/4.42 (1,1) [29208,0]. true => _t212 [ Unit Resolution, 29178, 27995, _t211 ] [ Modal Level Pure Literal Elimination, _t212 ] % 4.26/4.42 (1,1) [29210,0]. true => _t293 [ Unit Resolution, 29183, 28148, _t292 ] [ Modal Level Pure Literal Elimination, _t293 ] % 4.26/4.42 (1,1) [29212,0]. true => _t240 [ Unit Resolution, 29187, 28048, _t239 ] [ Modal Level Pure Literal Elimination, _t240 ] % 4.26/4.42 (1,1) [29214,0]. true => _t241 [ Unit Resolution, 29212, 28050, _t240 ] [ Modal Level Pure Literal Elimination, _t241 ] % 4.26/4.42 (1,1) [29216,0]. true => _t213 [ Unit Resolution, 29208, 27997, _t212 ] [ Modal Level Pure Literal Elimination, _t213 ] % 4.26/4.42 (1,1) [29218,0]. true => _t268 [ Unit Resolution, 29204, 28101, _t267 ] [ Modal Level Pure Literal Elimination, _t268 ] % 4.26/4.42 (1,1) [29220,0]. true => _t58 [ Unit Resolution, 29200, 27702, _t57 ] [ Modal Level Pure Literal Elimination, _t58 ] % 4.26/4.42 (1,1) [29222,0]. true => _t343 [ Unit Resolution, 29198, 28244, _t342 ] [ Modal Level Pure Literal Elimination, _t343 ] % 4.26/4.42 (1,1) [29224,0]. true => _t184 [ Unit Resolution, 29195, 27942, _t183 ] [ Modal Level Pure Literal Elimination, _t184 ] % 4.26/4.42 (1,1) [29226,0]. true => _t24 [ Unit Resolution, 29191, 27637, _t23 ] [ Modal Level Pure Literal Elimination, _t24 ] % 4.26/4.42 (1,1) [29228,0]. true => _t154 [ Unit Resolution, 29193, 27885, _t153 ] [ Modal Level Pure Literal Elimination, _t154 ] % 4.26/4.42 (1,1) [29231,0]. true => _t319 [ Unit Resolution, 29199, 28197, _t318 ] [ Modal Level Pure Literal Elimination, _t319 ] % 4.26/4.42 (1,1) [29233,0]. true => _t123 [ Unit Resolution, 29202, 27826, _t122 ] [ Modal Level Pure Literal Elimination, _t123 ] % 4.26/4.42 (1,1) [29235,0]. true => _t91 [ Unit Resolution, 29206, 27765, _t90 ] [ Modal Level Pure Literal Elimination, _t91 ] % 4.26/4.42 (1,1) [29237,0]. true => _t294 [ Unit Resolution, 29210, 28150, _t293 ] [ Modal Level Pure Literal Elimination, _t294 ] % 4.26/4.42 (1,1) [29239,0]. true => _t295 [ Unit Resolution, 29237, 28152, _t294 ] [ Modal Level Pure Literal Elimination, _t295 ] % 4.26/4.42 (1,1) [29241,0]. true => _t124 [ Unit Resolution, 29233, 27828, _t123 ] [ Modal Level Pure Literal Elimination, _t124 ] % 4.26/4.42 (1,1) [29243,0]. true => _t155 [ Unit Resolution, 29228, 27887, _t154 ] [ Modal Level Pure Literal Elimination, _t155 ] % 4.26/4.42 (1,1) [29245,0]. true => _t185 [ Unit Resolution, 29224, 27944, _t184 ] [ Modal Level Pure Literal Elimination, _t185 ] % 4.26/4.42 (1,1) [29247,0]. true => _t59 [ Unit Resolution, 29220, 27704, _t58 ] [ Modal Level Pure Literal Elimination, _t59 ] % 4.26/4.42 (1,1) [29249,0]. true => _t214 [ Unit Resolution, 29216, 27999, _t213 ] [ Modal Level Pure Literal Elimination, _t214 ] % 4.26/4.42 (1,1) [29251,0]. true => _t242 [ Unit Resolution, 29214, 28052, _t241 ] [ Modal Level Pure Literal Elimination, _t242 ] % 4.26/4.42 (1,1) [29253,0]. true => _t269 [ Unit Resolution, 29218, 28103, _t268 ] [ Modal Level Pure Literal Elimination, _t269 ] % 4.26/4.42 (1,1) [29256,0]. true => _t367 [ Unit Resolution, 29222, 28856, _t343 ] [ Modal Level Pure Literal Elimination, _t367 ] % 4.26/4.42 (1,1) [29257,0]. true => _t344 [ Unit Resolution, 29222, 28289, _t343 ] [ Modal Level Pure Literal Elimination, _t344 ] % 4.26/4.42 (1,1) [29258,0]. true => _t25 [ Unit Resolution, 29226, 27639, _t24 ] [ Modal Level Pure Literal Elimination, _t25 ] % 4.26/4.42 (1,1) [29260,0]. true => _t320 [ Unit Resolution, 29231, 28199, _t319 ] [ Modal Level Pure Literal Elimination, _t320 ] % 4.26/4.42 (1,1) [29262,0]. true => _t92 [ Unit Resolution, 29235, 27767, _t91 ] [ Modal Level Pure Literal Elimination, _t92 ] % 4.26/4.42 (1,1) [29264,0]. true => _t93 [ Unit Resolution, 29262, 27769, _t92 ] [ Modal Level Pure Literal Elimination, _t93 ] % 4.26/4.42 (1,1) [29266,0]. true => _t26 [ Unit Resolution, 29258, 27641, _t25 ] [ Modal Level Pure Literal Elimination, _t26 ] % 4.26/4.42 (1,1) [29268,0]. true => _t368 [ Unit Resolution, 29256, 28291, _t367 ] [ Modal Level Pure Literal Elimination, _t368 ] % 4.26/4.42 (1,1) [29270,0]. true => _t270 [ Unit Resolution, 29253, 28105, _t269 ] [ Modal Level Pure Literal Elimination, _t270 ] % 4.26/4.42 (1,1) [29272,0]. true => _t215 [ Unit Resolution, 29249, 28001, _t214 ] [ Modal Level Pure Literal Elimination, _t215 ] % 4.26/4.42 (1,1) [29274,0]. true => _t186 [ Unit Resolution, 29245, 27946, _t185 ] [ Modal Level Pure Literal Elimination, _t186 ] % 4.26/4.42 (1,1) [29276,0]. true => _t125 [ Unit Resolution, 29241, 27830, _t124 ] [ Modal Level Pure Literal Elimination, _t125 ] % 4.26/4.42 (1,1) [29278,0]. true => _t296 [ Unit Resolution, 29239, 28154, _t295 ] [ Modal Level Pure Literal Elimination, _t296 ] % 4.26/4.42 (1,1) [29280,0]. true => _t156 [ Unit Resolution, 29243, 27889, _t155 ] [ Modal Level Pure Literal Elimination, _t156 ] % 4.26/4.42 (1,1) [29282,0]. true => _t60 [ Unit Resolution, 29247, 27706, _t59 ] [ Modal Level Pure Literal Elimination, _t60 ] % 4.26/4.42 (1,1) [29284,0]. true => _t243 [ Unit Resolution, 29251, 28054, _t242 ] [ Modal Level Pure Literal Elimination, _t243 ] % 4.26/4.42 (1,1) [29287,0]. true => _t345 [ Unit Resolution, 29257, 28246, _t344 ] [ Modal Level Pure Literal Elimination, _t345 ] % 4.26/4.42 (1,1) [29289,0]. true => _t321 [ Unit Resolution, 29260, 28201, _t320 ] [ Modal Level Pure Literal Elimination, _t321 ] % 4.26/4.42 (1,1) [29291,0]. true => _t322 [ Unit Resolution, 29289, 28203, _t321 ] [ Modal Level Pure Literal Elimination, _t322 ] % 4.26/4.42 (1,1) [29293,0]. true => _t244 [ Unit Resolution, 29284, 28056, _t243 ] [ Modal Level Pure Literal Elimination, _t244 ] % 4.26/4.42 (1,1) [29295,0]. true => _t157 [ Unit Resolution, 29280, 27891, _t156 ] [ Modal Level Pure Literal Elimination, _t157 ] % 4.26/4.42 (1,1) [29297,0]. true => _t126 [ Unit Resolution, 29276, 27832, _t125 ] [ Modal Level Pure Literal Elimination, _t126 ] % 4.26/4.42 (1,1) [29299,0]. true => _t216 [ Unit Resolution, 29272, 28003, _t215 ] [ Modal Level Pure Literal Elimination, _t216 ] % 4.26/4.42 (1,1) [29302,0]. true => _t391 [ Unit Resolution, 29268, 28853, _t368 ] [ Modal Level Pure Literal Elimination, _t391 ] % 4.26/4.42 (1,1) [29303,0]. true => _t369 [ Unit Resolution, 29268, 28334, _t368 ] [ Modal Level Pure Literal Elimination, _t369 ] % 4.26/4.42 (1,1) [29304,0]. true => _t94 [ Unit Resolution, 29264, 27771, _t93 ] [ Modal Level Pure Literal Elimination, _t94 ] % 4.26/4.42 (1,1) [29306,0]. true => _t27 [ Unit Resolution, 29266, 27643, _t26 ] [ Modal Level Pure Literal Elimination, _t27 ] % 4.26/4.42 (1,1) [29308,0]. true => _t271 [ Unit Resolution, 29270, 28107, _t270 ] [ Modal Level Pure Literal Elimination, _t271 ] % 4.26/4.42 (1,1) [29310,0]. true => _t187 [ Unit Resolution, 29274, 27948, _t186 ] [ Modal Level Pure Literal Elimination, _t187 ] % 4.26/4.42 (1,1) [29312,0]. true => _t297 [ Unit Resolution, 29278, 28156, _t296 ] [ Modal Level Pure Literal Elimination, _t297 ] % 4.26/4.42 (1,1) [29314,0]. true => _t61 [ Unit Resolution, 29282, 27708, _t60 ] [ Modal Level Pure Literal Elimination, _t61 ] % 4.26/4.42 (1,1) [29316,0]. true => _t346 [ Unit Resolution, 29287, 28248, _t345 ] [ Modal Level Pure Literal Elimination, _t346 ] % 4.26/4.42 (1,1) [29318,0]. true => _t347 [ Unit Resolution, 29316, 28250, _t346 ] [ Modal Level Pure Literal Elimination, _t347 ] % 4.26/4.42 (1,1) [29320,0]. true => _t298 [ Unit Resolution, 29312, 28158, _t297 ] [ Modal Level Pure Literal Elimination, _t298 ] % 4.26/4.42 (1,1) [29322,0]. true => _t272 [ Unit Resolution, 29308, 28109, _t271 ] [ Modal Level Pure Literal Elimination, _t272 ] % 4.26/4.42 (1,1) [29324,0]. true => _t95 [ Unit Resolution, 29304, 27773, _t94 ] [ Modal Level Pure Literal Elimination, _t95 ] % 4.26/4.42 (1,1) [29326,0]. true => _t392 [ Unit Resolution, 29302, 28336, _t391 ] [ Modal Level Pure Literal Elimination, _t392 ] % 4.26/4.42 (1,1) [29328,0]. true => _t217 [ Unit Resolution, 29299, 28005, _t216 ] [ Modal Level Pure Literal Elimination, _t217 ] % 4.26/4.42 (1,1) [29330,0]. true => _t158 [ Unit Resolution, 29295, 27893, _t157 ] [ Modal Level Pure Literal Elimination, _t158 ] % 4.26/4.42 (1,1) [29332,0]. true => _t323 [ Unit Resolution, 29291, 28205, _t322 ] [ Modal Level Pure Literal Elimination, _t323 ] % 4.26/4.42 (1,1) [29334,0]. true => _t245 [ Unit Resolution, 29293, 28058, _t244 ] [ Modal Level Pure Literal Elimination, _t245 ] % 4.26/4.42 (1,1) [29336,0]. true => _t127 [ Unit Resolution, 29297, 27834, _t126 ] [ Modal Level Pure Literal Elimination, _t127 ] % 4.26/4.42 (1,1) [29339,0]. true => _t370 [ Unit Resolution, 29303, 28293, _t369 ] [ Modal Level Pure Literal Elimination, _t370 ] % 4.26/4.42 (1,1) [29341,0]. true => _t28 [ Unit Resolution, 29306, 27645, _t27 ] [ Modal Level Pure Literal Elimination, _t28 ] % 4.26/4.42 (1,1) [29343,0]. true => _t188 [ Unit Resolution, 29310, 27950, _t187 ] [ Modal Level Pure Literal Elimination, _t188 ] % 4.26/4.42 (1,1) [29345,0]. true => _t62 [ Unit Resolution, 29314, 27710, _t61 ] [ Modal Level Pure Literal Elimination, _t62 ] % 4.26/4.42 (1,1) [29347,0]. true => _t63 [ Unit Resolution, 29345, 27712, _t62 ] [ Modal Level Pure Literal Elimination, _t63 ] % 4.26/4.42 (1,1) [29349,0]. true => _t29 [ Unit Resolution, 29341, 27647, _t28 ] [ Modal Level Pure Literal Elimination, _t29 ] % 4.26/4.42 (1,1) [29351,0]. true => _t128 [ Unit Resolution, 29336, 27836, _t127 ] [ Modal Level Pure Literal Elimination, _t128 ] % 4.26/4.42 (1,1) [29353,0]. true => _t324 [ Unit Resolution, 29332, 28207, _t323 ] [ Modal Level Pure Literal Elimination, _t324 ] % 4.26/4.42 (1,1) [29355,0]. true => _t218 [ Unit Resolution, 29328, 28007, _t217 ] [ Modal Level Pure Literal Elimination, _t218 ] % 4.26/4.42 (1,1) [29357,0]. true => _t96 [ Unit Resolution, 29324, 27775, _t95 ] [ Modal Level Pure Literal Elimination, _t96 ] % 4.26/4.42 (1,1) [29359,0]. true => _t299 [ Unit Resolution, 29320, 28160, _t298 ] [ Modal Level Pure Literal Elimination, _t299 ] % 4.26/4.42 (1,1) [29361,0]. true => _t348 [ Unit Resolution, 29318, 28252, _t347 ] [ Modal Level Pure Literal Elimination, _t348 ] % 4.26/4.42 (1,1) [29363,0]. true => _t273 [ Unit Resolution, 29322, 28111, _t272 ] [ Modal Level Pure Literal Elimination, _t273 ] % 4.26/4.42 (1,1) [29366,0]. true => _t414 [ Unit Resolution, 29326, 28850, _t392 ] [ Modal Level Pure Literal Elimination, _t414 ] % 4.26/4.42 (1,1) [29367,0]. true => _t393 [ Unit Resolution, 29326, 28377, _t392 ] [ Modal Level Pure Literal Elimination, _t393 ] % 4.26/4.42 (1,1) [29368,0]. true => _t159 [ Unit Resolution, 29330, 27895, _t158 ] [ Modal Level Pure Literal Elimination, _t159 ] % 4.26/4.42 (1,1) [29370,0]. true => _t246 [ Unit Resolution, 29334, 28060, _t245 ] [ Modal Level Pure Literal Elimination, _t246 ] % 4.26/4.42 (1,1) [29372,0]. true => _t371 [ Unit Resolution, 29339, 28295, _t370 ] [ Modal Level Pure Literal Elimination, _t371 ] % 4.26/4.42 (1,1) [29374,0]. true => _t189 [ Unit Resolution, 29343, 27952, _t188 ] [ Modal Level Pure Literal Elimination, _t189 ] % 4.26/4.42 (1,1) [29376,0]. true => _t190 [ Unit Resolution, 29374, 27954, _t189 ] [ Modal Level Pure Literal Elimination, _t190 ] % 4.26/4.42 (1,1) [29378,0]. true => _t247 [ Unit Resolution, 29370, 28062, _t246 ] [ Modal Level Pure Literal Elimination, _t247 ] % 4.26/4.42 (1,1) [29380,0]. true => _t394 [ Unit Resolution, 29367, 28338, _t393 ] [ Modal Level Pure Literal Elimination, _t394 ] % 4.26/4.42 (1,1) [29383,0]. true => _t349 [ Unit Resolution, 29361, 28254, _t348 ] [ Modal Level Pure Literal Elimination, _t349 ] % 4.26/4.42 (1,1) [29385,0]. true => _t97 [ Unit Resolution, 29357, 27777, _t96 ] [ Modal Level Pure Literal Elimination, _t97 ] % 4.26/4.42 (1,1) [29387,0]. true => _t325 [ Unit Resolution, 29353, 28209, _t324 ] [ Modal Level Pure Literal Elimination, _t325 ] % 4.26/4.42 (1,1) [29389,0]. true => _t30 [ Unit Resolution, 29349, 27649, _t29 ] [ Modal Level Pure Literal Elimination, _t30 ] % 4.26/4.42 (1,1) [29391,0]. true => _t64 [ Unit Resolution, 29347, 27714, _t63 ] [ Modal Level Pure Literal Elimination, _t64 ] % 4.26/4.42 (1,1) [29393,0]. true => _t129 [ Unit Resolution, 29351, 27838, _t128 ] [ Modal Level Pure Literal Elimination, _t129 ] % 4.26/4.42 (1,1) [29395,0]. true => _t219 [ Unit Resolution, 29355, 28009, _t218 ] [ Modal Level Pure Literal Elimination, _t219 ] % 4.26/4.42 (1,1) [29397,0]. true => _t300 [ Unit Resolution, 29359, 28162, _t299 ] [ Modal Level Pure Literal Elimination, _t300 ] % 4.26/4.42 (1,1) [29399,0]. true => _t274 [ Unit Resolution, 29363, 28113, _t273 ] [ Modal Level Pure Literal Elimination, _t274 ] % 4.26/4.42 (1,1) [29401,0]. true => _t415 [ Unit Resolution, 29366, 28379, _t414 ] [ Modal Level Pure Literal Elimination, _t415 ] % 4.26/4.42 (1,1) [29403,0]. true => _t160 [ Unit Resolution, 29368, 27897, _t159 ] [ Modal Level Pure Literal Elimination, _t160 ] % 4.26/4.42 (1,1) [29405,0]. true => _t372 [ Unit Resolution, 29372, 28297, _t371 ] [ Modal Level Pure Literal Elimination, _t372 ] % 4.26/4.42 (1,1) [29407,0]. true => _t373 [ Unit Resolution, 29405, 28299, _t372 ] [ Modal Level Pure Literal Elimination, _t373 ] % 4.26/4.42 (1,1) [29410,0]. true => _t436 [ Unit Resolution, 29401, 28847, _t415 ] [ Modal Level Pure Literal Elimination, _t436 ] % 4.26/4.42 (1,1) [29411,0]. true => _t416 [ Unit Resolution, 29401, 28418, _t415 ] [ Modal Level Pure Literal Elimination, _t416 ] % 4.26/4.42 (1,1) [29412,0]. true => _t301 [ Unit Resolution, 29397, 28164, _t300 ] [ Modal Level Pure Literal Elimination, _t301 ] % 4.26/4.42 (1,1) [29414,0]. true => _t130 [ Unit Resolution, 29393, 27840, _t129 ] [ Modal Level Pure Literal Elimination, _t130 ] % 4.26/4.42 (1,1) [29416,0]. true => _t31 [ Unit Resolution, 29389, 27651, _t30 ] [ Modal Level Pure Literal Elimination, _t31 ] % 4.26/4.42 (1,1) [29418,0]. true => _t98 [ Unit Resolution, 29385, 27779, _t97 ] [ Modal Level Pure Literal Elimination, _t98 ] % 4.26/4.42 (1,1) [29420,0]. true => _t395 [ Unit Resolution, 29380, 28340, _t394 ] [ Modal Level Pure Literal Elimination, _t395 ] % 4.26/4.42 (1,1) [29422,0]. true => _t191 [ Unit Resolution, 29376, 27956, _t190 ] [ Modal Level Pure Literal Elimination, _t191 ] % 4.26/4.42 (1,1) [29424,0]. true => _t248 [ Unit Resolution, 29378, 28064, _t247 ] [ Modal Level Pure Literal Elimination, _t248 ] % 4.26/4.42 (1,1) [29426,0]. true => _t350 [ Unit Resolution, 29383, 28256, _t349 ] [ Modal Level Pure Literal Elimination, _t350 ] % 4.26/4.42 (1,1) [29428,0]. true => _t326 [ Unit Resolution, 29387, 28211, _t325 ] [ Modal Level Pure Literal Elimination, _t326 ] % 4.26/4.42 (1,1) [29430,0]. true => _t65 [ Unit Resolution, 29391, 27716, _t64 ] [ Modal Level Pure Literal Elimination, _t65 ] % 4.26/4.42 (1,1) [29432,0]. true => _t220 [ Unit Resolution, 29395, 28011, _t219 ] [ Modal Level Pure Literal Elimination, _t220 ] % 4.26/4.42 (1,1) [29434,0]. true => _t275 [ Unit Resolution, 29399, 28115, _t274 ] [ Modal Level Pure Literal Elimination, _t275 ] % 4.26/4.42 (1,1) [29436,0]. true => _t161 [ Unit Resolution, 29403, 27899, _t160 ] [ Modal Level Pure Literal Elimination, _t161 ] % 4.26/4.42 (1,1) [29438,0]. true => _t162 [ Unit Resolution, 29436, 27901, _t161 ] [ Modal Level Pure Literal Elimination, _t162 ] % 4.26/4.42 (1,1) [29440,0]. true => _t221 [ Unit Resolution, 29432, 28013, _t220 ] [ Modal Level Pure Literal Elimination, _t221 ] % 4.26/4.42 (1,1) [29442,0]. true => _t327 [ Unit Resolution, 29428, 28213, _t326 ] [ Modal Level Pure Literal Elimination, _t327 ] % 4.26/4.42 (1,1) [29444,0]. true => _t249 [ Unit Resolution, 29424, 28066, _t248 ] [ Modal Level Pure Literal Elimination, _t249 ] % 4.26/4.42 (1,1) [29446,0]. true => _t396 [ Unit Resolution, 29420, 28342, _t395 ] [ Modal Level Pure Literal Elimination, _t396 ] % 4.26/4.42 (1,1) [29448,0]. true => _t32 [ Unit Resolution, 29416, 27653, _t31 ] [ Modal Level Pure Literal Elimination, _t32 ] % 4.26/4.42 (1,1) [29450,0]. true => _t302 [ Unit Resolution, 29412, 28166, _t301 ] [ Modal Level Pure Literal Elimination, _t302 ] % 4.26/4.42 (1,1) [29452,0]. true => _t437 [ Unit Resolution, 29410, 28420, _t436 ] [ Modal Level Pure Literal Elimination, _t437 ] % 4.26/4.42 (1,1) [29454,0]. true => _t374 [ Unit Resolution, 29407, 28301, _t373 ] [ Modal Level Pure Literal Elimination, _t374 ] % 4.26/4.42 (1,1) [29457,0]. true => _t417 [ Unit Resolution, 29411, 28381, _t416 ] [ Modal Level Pure Literal Elimination, _t417 ] % 4.26/4.42 (1,1) [29459,0]. true => _t131 [ Unit Resolution, 29414, 27842, _t130 ] [ Modal Level Pure Literal Elimination, _t131 ] % 4.26/4.42 (1,1) [29461,0]. true => _t99 [ Unit Resolution, 29418, 27781, _t98 ] [ Modal Level Pure Literal Elimination, _t99 ] % 4.26/4.42 (1,1) [29463,0]. true => _t192 [ Unit Resolution, 29422, 27958, _t191 ] [ Modal Level Pure Literal Elimination, _t192 ] % 4.26/4.42 (1,1) [29465,0]. true => _t351 [ Unit Resolution, 29426, 28258, _t350 ] [ Modal Level Pure Literal Elimination, _t351 ] % 4.26/4.42 (1,1) [29467,0]. true => _t66 [ Unit Resolution, 29430, 27718, _t65 ] [ Modal Level Pure Literal Elimination, _t66 ] % 4.26/4.42 (1,1) [29469,0]. true => _t276 [ Unit Resolution, 29434, 28117, _t275 ] [ Modal Level Pure Literal Elimination, _t276 ] % 4.26/4.42 (1,1) [29471,0]. true => _t277 [ Unit Resolution, 29469, 28119, _t276 ] [ Modal Level Pure Literal Elimination, _t277 ] % 4.26/4.42 (1,1) [29473,0]. true => _t352 [ Unit Resolution, 29465, 28260, _t351 ] [ Modal Level Pure Literal Elimination, _t352 ] % 4.26/4.42 (1,1) [29475,0]. true => _t100 [ Unit Resolution, 29461, 27783, _t99 ] [ Modal Level Pure Literal Elimination, _t100 ] % 4.26/4.42 (1,1) [29477,0]. true => _t418 [ Unit Resolution, 29457, 28383, _t417 ] [ Modal Level Pure Literal Elimination, _t418 ] % 4.26/4.42 (1,1) [29480,0]. true => _t457 [ Unit Resolution, 29452, 28844, _t437 ] [ Modal Level Pure Literal Elimination, _t457 ] % 4.26/4.42 (1,1) [29481,0]. true => _t438 [ Unit Resolution, 29452, 28457, _t437 ] [ Modal Level Pure Literal Elimination, _t438 ] % 4.26/4.42 (1,1) [29482,0]. true => _t33 [ Unit Resolution, 29448, 27655, _t32 ] [ Modal Level Pure Literal Elimination, _t33 ] % 4.26/4.42 (1,1) [29484,0]. true => _t250 [ Unit Resolution, 29444, 28068, _t249 ] [ Modal Level Pure Literal Elimination, _t250 ] % 4.26/4.42 (1,1) [29486,0]. true => _t222 [ Unit Resolution, 29440, 28015, _t221 ] [ Modal Level Pure Literal Elimination, _t222 ] % 4.26/4.42 (1,1) [29488,0]. true => _t163 [ Unit Resolution, 29438, 27903, _t162 ] [ Modal Level Pure Literal Elimination, _t163 ] % 4.26/4.42 (1,1) [29490,0]. true => _t328 [ Unit Resolution, 29442, 28215, _t327 ] [ Modal Level Pure Literal Elimination, _t328 ] % 4.26/4.42 (1,1) [29492,0]. true => _t397 [ Unit Resolution, 29446, 28344, _t396 ] [ Modal Level Pure Literal Elimination, _t397 ] % 4.26/4.42 (1,1) [29494,0]. true => _t303 [ Unit Resolution, 29450, 28168, _t302 ] [ Modal Level Pure Literal Elimination, _t303 ] % 4.26/4.42 (1,1) [29496,0]. true => _t375 [ Unit Resolution, 29454, 28303, _t374 ] [ Modal Level Pure Literal Elimination, _t375 ] % 4.26/4.42 (1,1) [29498,0]. true => _t132 [ Unit Resolution, 29459, 27844, _t131 ] [ Modal Level Pure Literal Elimination, _t132 ] % 4.26/4.42 (1,1) [29500,0]. true => _t193 [ Unit Resolution, 29463, 27960, _t192 ] [ Modal Level Pure Literal Elimination, _t193 ] % 4.26/4.42 (1,1) [29502,0]. true => _t67 [ Unit Resolution, 29467, 27720, _t66 ] [ Modal Level Pure Literal Elimination, _t67 ] % 4.26/4.42 (1,1) [29504,0]. true => _t68 [ Unit Resolution, 29502, 27722, _t67 ] [ Modal Level Pure Literal Elimination, _t68 ] % 4.26/4.42 (1,1) [29506,0]. true => _t133 [ Unit Resolution, 29498, 27846, _t132 ] [ Modal Level Pure Literal Elimination, _t133 ] % 4.26/4.42 (1,1) [29508,0]. true => _t304 [ Unit Resolution, 29494, 28170, _t303 ] [ Modal Level Pure Literal Elimination, _t304 ] % 4.26/4.42 (1,1) [29510,0]. true => _t329 [ Unit Resolution, 29490, 28217, _t328 ] [ Modal Level Pure Literal Elimination, _t329 ] % 4.26/4.42 (1,1) [29512,0]. true => _t223 [ Unit Resolution, 29486, 28017, _t222 ] [ Modal Level Pure Literal Elimination, _t223 ] % 4.26/4.42 (1,1) [29514,0]. true => _t34 [ Unit Resolution, 29482, 27657, _t33 ] [ Modal Level Pure Literal Elimination, _t34 ] % 4.26/4.42 (1,1) [29516,0]. true => _t458 [ Unit Resolution, 29480, 28459, _t457 ] [ Modal Level Pure Literal Elimination, _t458 ] % 4.26/4.42 (1,1) [29518,0]. true => _t419 [ Unit Resolution, 29477, 28385, _t418 ] [ Modal Level Pure Literal Elimination, _t419 ] % 4.26/4.42 (1,1) [29520,0]. true => _t353 [ Unit Resolution, 29473, 28262, _t352 ] [ Modal Level Pure Literal Elimination, _t353 ] % 4.26/4.42 (1,1) [29522,0]. true => _t278 [ Unit Resolution, 29471, 28121, _t277 ] [ Modal Level Pure Literal Elimination, _t278 ] % 4.26/4.42 (1,1) [29524,0]. true => _t101 [ Unit Resolution, 29475, 27785, _t100 ] [ Modal Level Pure Literal Elimination, _t101 ] % 4.26/4.42 (1,1) [29527,0]. true => _t439 [ Unit Resolution, 29481, 28422, _t438 ] [ Modal Level Pure Literal Elimination, _t439 ] % 4.26/4.42 (1,1) [29529,0]. true => _t251 [ Unit Resolution, 29484, 28070, _t250 ] [ Modal Level Pure Literal Elimination, _t251 ] % 4.26/4.42 (1,1) [29531,0]. true => _t164 [ Unit Resolution, 29488, 27905, _t163 ] [ Modal Level Pure Literal Elimination, _t164 ] % 4.26/4.42 (1,1) [29533,0]. true => _t398 [ Unit Resolution, 29492, 28346, _t397 ] [ Modal Level Pure Literal Elimination, _t398 ] % 4.26/4.42 (1,1) [29535,0]. true => _t376 [ Unit Resolution, 29496, 28305, _t375 ] [ Modal Level Pure Literal Elimination, _t376 ] % 4.26/4.42 (1,1) [29537,0]. true => _t194 [ Unit Resolution, 29500, 27962, _t193 ] [ Modal Level Pure Literal Elimination, _t194 ] % 4.26/4.42 (1,1) [29539,0]. true => _t195 [ Unit Resolution, 29537, 27964, _t194 ] [ Modal Level Pure Literal Elimination, _t195 ] % 4.26/4.42 (1,1) [29541,0]. true => _t399 [ Unit Resolution, 29533, 28348, _t398 ] [ Modal Level Pure Literal Elimination, _t399 ] % 4.26/4.42 (1,1) [29543,0]. true => _t252 [ Unit Resolution, 29529, 28072, _t251 ] [ Modal Level Pure Literal Elimination, _t252 ] % 4.26/4.42 (1,1) [29545,0]. true => _t102 [ Unit Resolution, 29524, 27787, _t101 ] [ Modal Level Pure Literal Elimination, _t102 ] % 4.26/4.42 (1,1) [29547,0]. true => _t354 [ Unit Resolution, 29520, 28264, _t353 ] [ Modal Level Pure Literal Elimination, _t354 ] % 4.26/4.42 (1,1) [29550,0]. true => _t477 [ Unit Resolution, 29516, 28841, _t458 ] [ Modal Level Pure Literal Elimination, _t477 ] % 4.26/4.42 (1,1) [29551,0]. true => _t459 [ Unit Resolution, 29516, 28494, _t458 ] [ Modal Level Pure Literal Elimination, _t459 ] % 4.26/4.42 (1,1) [29552,0]. true => _t224 [ Unit Resolution, 29512, 28019, _t223 ] [ Modal Level Pure Literal Elimination, _t224 ] % 4.26/4.42 (1,1) [29554,0]. true => _t305 [ Unit Resolution, 29508, 28172, _t304 ] [ Modal Level Pure Literal Elimination, _t305 ] % 4.26/4.42 (1,1) [29556,0]. true => _t69 [ Unit Resolution, 29504, 27724, _t68 ] [ Modal Level Pure Literal Elimination, _t69 ] % 4.26/4.42 (1,1) [29558,0]. true => _t134 [ Unit Resolution, 29506, 27848, _t133 ] [ Modal Level Pure Literal Elimination, _t134 ] % 4.26/4.42 (1,1) [29560,0]. true => _t330 [ Unit Resolution, 29510, 28219, _t329 ] [ Modal Level Pure Literal Elimination, _t330 ] % 4.26/4.42 (1,1) [29562,0]. true => _t36 [ Unit Resolution, 29514, 27661, _t34 ] [ Modal Level Pure Literal Elimination, _t36 ] % 4.26/4.42 (1,1) [29563,0]. true => _t35 [ Unit Resolution, 29514, 27659, _t34 ] [ Modal Level Pure Literal Elimination, _t35 ] % 4.26/4.42 (1,1) [29564,0]. true => _t420 [ Unit Resolution, 29518, 28387, _t419 ] [ Modal Level Pure Literal Elimination, _t420 ] % 4.26/4.42 (1,1) [29566,0]. true => _t279 [ Unit Resolution, 29522, 28123, _t278 ] [ Modal Level Pure Literal Elimination, _t279 ] % 4.26/4.42 (1,1) [29568,0]. true => _t440 [ Unit Resolution, 29527, 28424, _t439 ] [ Modal Level Pure Literal Elimination, _t440 ] % 4.26/4.42 (1,1) [29570,0]. true => _t165 [ Unit Resolution, 29531, 27907, _t164 ] [ Modal Level Pure Literal Elimination, _t165 ] % 4.26/4.42 (1,1) [29572,0]. true => _t377 [ Unit Resolution, 29535, 28307, _t376 ] [ Modal Level Pure Literal Elimination, _t377 ] % 4.26/4.42 (1,1) [29574,0]. true => _t378 [ Unit Resolution, 29572, 28309, _t377 ] [ Modal Level Pure Literal Elimination, _t378 ] % 4.26/4.42 (1,1) [29576,0]. true => _t441 [ Unit Resolution, 29568, 28426, _t440 ] [ Modal Level Pure Literal Elimination, _t441 ] % 4.26/4.42 (1,1) [29578,0]. true => _t421 [ Unit Resolution, 29564, 28389, _t420 ] [ Modal Level Pure Literal Elimination, _t421 ] % 4.26/4.42 (1,1) [29580,0]. true => ~p31 | ~p1 [ Unit Resolution, 29562, 27660, _t36 ] [ Backward Subsumption, 57020 ] % 4.26/4.42 (1,1) [29581,0]. true => _t135 [ Unit Resolution, 29558, 27850, _t134 ] [ Modal Level Pure Literal Elimination, _t135 ] % 4.26/4.42 (1,1) [29583,0]. true => _t306 [ Unit Resolution, 29554, 28174, _t305 ] [ Modal Level Pure Literal Elimination, _t306 ] % 4.26/4.42 (1,1) [29585,0]. true => _t460 [ Unit Resolution, 29551, 28461, _t459 ] [ Modal Level Pure Literal Elimination, _t460 ] % 4.26/4.42 (1,1) [29588,0]. true => _t103 [ Unit Resolution, 29545, 27789, _t102 ] [ Modal Level Pure Literal Elimination, _t103 ] % 4.26/4.42 (1,1) [29590,0]. true => _t400 [ Unit Resolution, 29541, 28350, _t399 ] [ Modal Level Pure Literal Elimination, _t400 ] % 4.26/4.42 (1,1) [29592,0]. true => _t196 [ Unit Resolution, 29539, 27966, _t195 ] [ Modal Level Pure Literal Elimination, _t196 ] % 4.26/4.42 (1,1) [29594,0]. true => _t253 [ Unit Resolution, 29543, 28074, _t252 ] [ Modal Level Pure Literal Elimination, _t253 ] % 4.26/4.42 (1,1) [29596,0]. true => _t355 [ Unit Resolution, 29547, 28266, _t354 ] [ Modal Level Pure Literal Elimination, _t355 ] % 4.26/4.42 (1,1) [29598,0]. true => _t478 [ Unit Resolution, 29550, 28496, _t477 ] [ Modal Level Pure Literal Elimination, _t478 ] % 4.26/4.42 (1,1) [29600,0]. true => _t225 [ Unit Resolution, 29552, 28021, _t224 ] [ Modal Level Pure Literal Elimination, _t225 ] % 4.26/4.42 (1,1) [29602,0]. true => _t71 [ Unit Resolution, 29556, 27728, _t69 ] [ Modal Level Pure Literal Elimination, _t71 ] % 4.26/4.42 (1,1) [29603,0]. true => _t70 [ Unit Resolution, 29556, 27726, _t69 ] [ Modal Level Pure Literal Elimination, _t70 ] % 4.26/4.42 (1,1) [29604,0]. true => _t331 [ Unit Resolution, 29560, 28221, _t330 ] [ Modal Level Pure Literal Elimination, _t331 ] % 4.26/4.42 (1,1) [29606,0]. true => p31 | p1 [ Unit Resolution, 29563, 27658, _t35 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [29607,0]. true => _t280 [ Unit Resolution, 29566, 28125, _t279 ] [ Modal Level Pure Literal Elimination, _t280 ] % 4.26/4.42 (1,1) [29609,0]. true => _t166 [ Unit Resolution, 29570, 27909, _t165 ] [ Modal Level Pure Literal Elimination, _t166 ] % 4.26/4.42 (1,1) [29611,0]. true => _t167 [ Unit Resolution, 29609, 27911, _t166 ] [ Modal Level Pure Literal Elimination, _t167 ] % 4.26/4.42 (1,1) [29613,0]. true => _t332 [ Unit Resolution, 29604, 28223, _t331 ] [ Modal Level Pure Literal Elimination, _t332 ] % 4.26/4.42 (1,1) [29615,0]. true => ~p31 | ~p30 [ Unit Resolution, 29602, 27727, _t71 ] [ Backward Subsumption, 57019 ] % 4.26/4.42 (1,1) [29617,0]. true => _t496 [ Unit Resolution, 29598, 28838, _t478 ] [ Modal Level Pure Literal Elimination, _t496 ] % 4.26/4.42 (1,1) [29618,0]. true => _t479 [ Unit Resolution, 29598, 28529, _t478 ] [ Modal Level Pure Literal Elimination, _t479 ] % 4.26/4.42 (1,1) [29619,0]. true => _t254 [ Unit Resolution, 29594, 28076, _t253 ] [ Modal Level Pure Literal Elimination, _t254 ] % 4.26/4.42 (1,1) [29621,0]. true => _t401 [ Unit Resolution, 29590, 28352, _t400 ] [ Modal Level Pure Literal Elimination, _t401 ] % 4.26/4.42 (1,1) [29623,0]. true => _t461 [ Unit Resolution, 29585, 28463, _t460 ] [ Modal Level Pure Literal Elimination, _t461 ] % 4.26/4.42 (1,1) [29625,0]. true => _t136 [ Unit Resolution, 29581, 27852, _t135 ] [ Modal Level Pure Literal Elimination, _t136 ] % 4.26/4.42 (1,1) [29627,0]. true => _t442 [ Unit Resolution, 29576, 28428, _t441 ] [ Modal Level Pure Literal Elimination, _t442 ] % 4.26/4.42 (1,1) [29629,0]. true => _t379 [ Unit Resolution, 29574, 28311, _t378 ] [ Modal Level Pure Literal Elimination, _t379 ] % 4.26/4.42 (1,1) [29631,0]. true => _t422 [ Unit Resolution, 29578, 28391, _t421 ] [ Modal Level Pure Literal Elimination, _t422 ] % 4.26/4.42 (1,1) [29633,0]. true => _t307 [ Unit Resolution, 29583, 28176, _t306 ] [ Modal Level Pure Literal Elimination, _t307 ] % 4.26/4.42 (1,1) [29635,0]. true => _t105 [ Unit Resolution, 29588, 27793, _t103 ] [ Modal Level Pure Literal Elimination, _t105 ] % 4.26/4.42 (1,1) [29636,0]. true => _t104 [ Unit Resolution, 29588, 27791, _t103 ] [ Modal Level Pure Literal Elimination, _t104 ] % 4.26/4.42 (1,1) [29637,0]. true => _t197 [ Unit Resolution, 29592, 27968, _t196 ] [ Modal Level Pure Literal Elimination, _t197 ] % 4.26/4.42 (1,1) [29639,0]. true => _t356 [ Unit Resolution, 29596, 28268, _t355 ] [ Modal Level Pure Literal Elimination, _t356 ] % 4.26/4.42 (1,1) [29641,0]. true => _t226 [ Unit Resolution, 29600, 28023, _t225 ] [ Modal Level Pure Literal Elimination, _t226 ] % 4.26/4.42 (1,1) [29643,0]. true => p31 | p30 [ Unit Resolution, 29603, 27725, _t70 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [29644,0]. true => _t281 [ Unit Resolution, 29607, 28127, _t280 ] [ Modal Level Pure Literal Elimination, _t281 ] % 4.26/4.42 (1,1) [29646,0]. true => _t282 [ Unit Resolution, 29644, 28129, _t281 ] [ Modal Level Pure Literal Elimination, _t282 ] % 4.26/4.42 (1,1) [29648,0]. true => _t357 [ Unit Resolution, 29639, 28270, _t356 ] [ Modal Level Pure Literal Elimination, _t357 ] % 4.26/4.42 (1,1) [29650,0]. true => p30 | p29 [ Unit Resolution, 29636, 27790, _t104 ] % 4.26/4.42 (1,1) [29651,0]. true => _t308 [ Unit Resolution, 29633, 28178, _t307 ] [ Modal Level Pure Literal Elimination, _t308 ] % 4.26/4.42 (1,1) [29653,0]. true => _t380 [ Unit Resolution, 29629, 28313, _t379 ] [ Modal Level Pure Literal Elimination, _t380 ] % 4.26/4.42 (1,1) [29655,0]. true => _t138 [ Unit Resolution, 29625, 27856, _t136 ] [ Modal Level Pure Literal Elimination, _t138 ] % 4.26/4.42 (1,1) [29656,0]. true => _t137 [ Unit Resolution, 29625, 27854, _t136 ] [ Modal Level Pure Literal Elimination, _t137 ] % 4.26/4.42 (1,1) [29657,0]. true => _t402 [ Unit Resolution, 29621, 28354, _t401 ] [ Modal Level Pure Literal Elimination, _t402 ] % 4.26/4.42 (1,1) [29659,0]. true => _t480 [ Unit Resolution, 29618, 28498, _t479 ] [ Modal Level Pure Literal Elimination, _t480 ] % 4.26/4.42 (1,1) [29662,0]. true => _t168 [ Unit Resolution, 29611, 27913, _t167 ] [ Modal Level Pure Literal Elimination, _t168 ] % 4.26/4.42 (1,1) [29664,0]. true => _t333 [ Unit Resolution, 29613, 28225, _t332 ] [ Modal Level Pure Literal Elimination, _t333 ] % 4.26/4.42 (1,1) [29666,0]. true => _t497 [ Unit Resolution, 29617, 28531, _t496 ] [ Modal Level Pure Literal Elimination, _t497 ] % 4.26/4.42 (1,1) [29668,0]. true => _t255 [ Unit Resolution, 29619, 28078, _t254 ] [ Modal Level Pure Literal Elimination, _t255 ] % 4.26/4.42 (1,1) [29670,0]. true => _t462 [ Unit Resolution, 29623, 28465, _t461 ] [ Modal Level Pure Literal Elimination, _t462 ] % 4.26/4.42 (1,1) [29672,0]. true => _t443 [ Unit Resolution, 29627, 28430, _t442 ] [ Modal Level Pure Literal Elimination, _t443 ] % 4.26/4.42 (1,1) [29674,0]. true => _t423 [ Unit Resolution, 29631, 28393, _t422 ] [ Modal Level Pure Literal Elimination, _t423 ] % 4.26/4.42 (1,1) [29676,0]. true => ~p30 | ~p29 [ Unit Resolution, 29635, 27792, _t105 ] % 4.26/4.42 (1,1) [29677,0]. true => _t198 [ Unit Resolution, 29637, 27970, _t197 ] [ Modal Level Pure Literal Elimination, _t198 ] % 4.26/4.42 (1,1) [29679,0]. true => _t227 [ Unit Resolution, 29641, 28025, _t226 ] [ Modal Level Pure Literal Elimination, _t227 ] % 4.26/4.42 (1,1) [29681,0]. true => _t228 [ Unit Resolution, 29679, 28027, _t227 ] [ Modal Level Pure Literal Elimination, _t228 ] % 4.26/4.42 (1,1) [29683,0]. true => _t424 [ Unit Resolution, 29674, 28395, _t423 ] [ Modal Level Pure Literal Elimination, _t424 ] % 4.26/4.42 (1,1) [29685,0]. true => _t463 [ Unit Resolution, 29670, 28467, _t462 ] [ Modal Level Pure Literal Elimination, _t463 ] % 4.26/4.42 (1,1) [29688,0]. true => _t514 [ Unit Resolution, 29666, 28835, _t497 ] [ Modal Level Pure Literal Elimination, _t514 ] % 4.26/4.42 (1,1) [29689,0]. true => _t498 [ Unit Resolution, 29666, 28562, _t497 ] [ Modal Level Pure Literal Elimination, _t498 ] % 4.26/4.42 (1,1) [29690,0]. true => _t170 [ Unit Resolution, 29662, 27917, _t168 ] [ Modal Level Pure Literal Elimination, _t170 ] % 4.26/4.42 (1,1) [29691,0]. true => _t169 [ Unit Resolution, 29662, 27915, _t168 ] [ Modal Level Pure Literal Elimination, _t169 ] % 4.26/4.42 (1,1) [29692,0]. true => _t403 [ Unit Resolution, 29657, 28356, _t402 ] [ Modal Level Pure Literal Elimination, _t403 ] % 4.26/4.42 (1,1) [29694,0]. true => ~p29 | ~p28 [ Unit Resolution, 29655, 27855, _t138 ] [ Backward Subsumption, 57049 ] % 4.26/4.42 (1,1) [29695,0]. true => _t309 [ Unit Resolution, 29651, 28180, _t308 ] [ Modal Level Pure Literal Elimination, _t309 ] % 4.26/4.42 (1,1) [29697,0]. true => _t283 [ Unit Resolution, 29646, 28131, _t282 ] [ Modal Level Pure Literal Elimination, _t283 ] % 4.26/4.42 (1,1) [29699,0]. true => _t358 [ Unit Resolution, 29648, 28272, _t357 ] [ Modal Level Pure Literal Elimination, _t358 ] % 4.26/4.42 (1,1) [29701,0]. true => _t381 [ Unit Resolution, 29653, 28315, _t380 ] [ Modal Level Pure Literal Elimination, _t381 ] % 4.26/4.42 (1,1) [29703,0]. true => p29 | p28 [ Unit Resolution, 29656, 27853, _t137 ] % 4.26/4.42 (1,1) [29704,0]. true => _t481 [ Unit Resolution, 29659, 28500, _t480 ] [ Modal Level Pure Literal Elimination, _t481 ] % 4.26/4.42 (1,1) [29706,0]. true => _t334 [ Unit Resolution, 29664, 28227, _t333 ] [ Modal Level Pure Literal Elimination, _t334 ] % 4.26/4.42 (1,1) [29708,0]. true => _t256 [ Unit Resolution, 29668, 28080, _t255 ] [ Modal Level Pure Literal Elimination, _t256 ] % 4.26/4.42 (1,1) [29710,0]. true => _t444 [ Unit Resolution, 29672, 28432, _t443 ] [ Modal Level Pure Literal Elimination, _t444 ] % 4.26/4.42 (1,1) [29712,0]. true => _t199 [ Unit Resolution, 29677, 27972, _t198 ] [ Modal Level Pure Literal Elimination, _t199 ] % 4.26/4.42 (1,1) [29714,0]. true => _t201 [ Unit Resolution, 29712, 27976, _t199 ] [ Modal Level Pure Literal Elimination, _t201 ] % 4.26/4.42 (1,1) [29715,0]. true => _t200 [ Unit Resolution, 29712, 27974, _t199 ] [ Modal Level Pure Literal Elimination, _t200 ] % 4.26/4.42 (1,1) [29716,0]. true => _t257 [ Unit Resolution, 29708, 28082, _t256 ] [ Modal Level Pure Literal Elimination, _t257 ] % 4.26/4.42 (1,1) [29718,0]. true => _t482 [ Unit Resolution, 29704, 28502, _t481 ] [ Modal Level Pure Literal Elimination, _t482 ] % 4.26/4.42 (1,1) [29720,0]. true => _t359 [ Unit Resolution, 29699, 28274, _t358 ] [ Modal Level Pure Literal Elimination, _t359 ] % 4.26/4.42 (1,1) [29722,0]. true => _t310 [ Unit Resolution, 29695, 28182, _t309 ] [ Modal Level Pure Literal Elimination, _t310 ] % 4.26/4.42 (1,1) [29724,0]. true => p28 | p27 [ Unit Resolution, 29691, 27914, _t169 ] % 4.26/4.42 (1,1) [29725,0]. true => _t499 [ Unit Resolution, 29689, 28533, _t498 ] [ Modal Level Pure Literal Elimination, _t499 ] % 4.26/4.42 (1,1) [29728,0]. true => _t425 [ Unit Resolution, 29683, 28397, _t424 ] [ Modal Level Pure Literal Elimination, _t425 ] % 4.26/4.42 (1,1) [29730,0]. true => _t229 [ Unit Resolution, 29681, 28029, _t228 ] [ Modal Level Pure Literal Elimination, _t229 ] % 4.26/4.42 (1,1) [29732,0]. true => _t464 [ Unit Resolution, 29685, 28469, _t463 ] [ Modal Level Pure Literal Elimination, _t464 ] % 4.26/4.42 (1,1) [29734,0]. true => _t515 [ Unit Resolution, 29688, 28564, _t514 ] [ Modal Level Pure Literal Elimination, _t515 ] % 4.26/4.42 (1,1) [29736,0]. true => ~p28 | ~p27 [ Unit Resolution, 29690, 27916, _t170 ] [ Backward Subsumption, 57048 ] % 4.26/4.42 (1,1) [29737,0]. true => _t404 [ Unit Resolution, 29692, 28358, _t403 ] [ Modal Level Pure Literal Elimination, _t404 ] % 4.26/4.42 (1,1) [29739,0]. true => _t284 [ Unit Resolution, 29697, 28133, _t283 ] [ Modal Level Pure Literal Elimination, _t284 ] % 4.26/4.42 (1,1) [29741,0]. true => _t382 [ Unit Resolution, 29701, 28317, _t381 ] [ Modal Level Pure Literal Elimination, _t382 ] % 4.26/4.42 (1,1) [29743,0]. true => _t335 [ Unit Resolution, 29706, 28229, _t334 ] [ Modal Level Pure Literal Elimination, _t335 ] % 4.26/4.42 (1,1) [29745,0]. true => _t445 [ Unit Resolution, 29710, 28434, _t444 ] [ Modal Level Pure Literal Elimination, _t445 ] % 4.26/4.42 (1,1) [29747,0]. true => _t446 [ Unit Resolution, 29745, 28436, _t445 ] [ Modal Level Pure Literal Elimination, _t446 ] % 4.26/4.42 (1,1) [29749,0]. true => _t383 [ Unit Resolution, 29741, 28319, _t382 ] [ Modal Level Pure Literal Elimination, _t383 ] % 4.26/4.42 (1,1) [29751,0]. true => _t405 [ Unit Resolution, 29737, 28360, _t404 ] [ Modal Level Pure Literal Elimination, _t405 ] % 4.26/4.42 (1,1) [29753,0]. true => _t465 [ Unit Resolution, 29732, 28471, _t464 ] [ Modal Level Pure Literal Elimination, _t465 ] % 4.26/4.42 (1,1) [29755,0]. true => _t426 [ Unit Resolution, 29728, 28399, _t425 ] [ Modal Level Pure Literal Elimination, _t426 ] % 4.26/4.42 (1,1) [29757,0]. true => _t311 [ Unit Resolution, 29722, 28184, _t310 ] [ Modal Level Pure Literal Elimination, _t311 ] % 4.26/4.42 (1,1) [29759,0]. true => _t483 [ Unit Resolution, 29718, 28504, _t482 ] [ Modal Level Pure Literal Elimination, _t483 ] % 4.26/4.42 (1,1) [29761,0]. true => p27 | p26 [ Unit Resolution, 29715, 27973, _t200 ] % 4.26/4.42 (1,1) [29762,0]. true => ~p27 | ~p26 [ Unit Resolution, 29714, 27975, _t201 ] [ Backward Subsumption, 57047 ] % 4.26/4.42 (1,1) [29763,0]. true => _t258 [ Unit Resolution, 29716, 28084, _t257 ] [ Modal Level Pure Literal Elimination, _t258 ] % 4.26/4.42 (1,1) [29765,0]. true => _t360 [ Unit Resolution, 29720, 28276, _t359 ] [ Modal Level Pure Literal Elimination, _t360 ] % 4.26/4.42 (1,1) [29767,0]. true => _t500 [ Unit Resolution, 29725, 28535, _t499 ] [ Modal Level Pure Literal Elimination, _t500 ] % 4.26/4.42 (1,1) [29769,0]. true => _t231 [ Unit Resolution, 29730, 28033, _t229 ] [ Modal Level Pure Literal Elimination, _t231 ] % 4.26/4.42 (1,1) [29770,0]. true => _t230 [ Unit Resolution, 29730, 28031, _t229 ] [ Modal Level Pure Literal Elimination, _t230 ] % 4.26/4.42 (1,1) [29772,0]. true => _t531 [ Unit Resolution, 29734, 28832, _t515 ] [ Modal Level Pure Literal Elimination, _t531 ] % 4.26/4.42 (1,1) [29773,0]. true => _t516 [ Unit Resolution, 29734, 28593, _t515 ] [ Modal Level Pure Literal Elimination, _t516 ] % 4.26/4.42 (1,1) [29774,0]. true => _t285 [ Unit Resolution, 29739, 28135, _t284 ] [ Modal Level Pure Literal Elimination, _t285 ] % 4.26/4.42 (1,1) [29776,0]. true => _t336 [ Unit Resolution, 29743, 28231, _t335 ] [ Modal Level Pure Literal Elimination, _t336 ] % 4.26/4.42 (1,1) [29778,0]. true => _t337 [ Unit Resolution, 29776, 28233, _t336 ] [ Modal Level Pure Literal Elimination, _t337 ] % 4.26/4.42 (1,1) [29780,0]. true => _t517 [ Unit Resolution, 29773, 28566, _t516 ] [ Modal Level Pure Literal Elimination, _t517 ] % 4.26/4.42 (1,1) [29783,0]. true => ~p26 | ~p25 [ Unit Resolution, 29769, 28032, _t231 ] [ Backward Subsumption, 57046 ] % 4.26/4.42 (1,1) [29784,0]. true => _t361 [ Unit Resolution, 29765, 28278, _t360 ] [ Modal Level Pure Literal Elimination, _t361 ] % 4.26/4.42 (1,1) [29786,0]. true => _t484 [ Unit Resolution, 29759, 28506, _t483 ] [ Modal Level Pure Literal Elimination, _t484 ] % 4.26/4.42 (1,1) [29788,0]. true => _t427 [ Unit Resolution, 29755, 28401, _t426 ] [ Modal Level Pure Literal Elimination, _t427 ] % 4.26/4.42 (1,1) [29790,0]. true => _t406 [ Unit Resolution, 29751, 28362, _t405 ] [ Modal Level Pure Literal Elimination, _t406 ] % 4.26/4.42 (1,1) [29792,0]. true => _t447 [ Unit Resolution, 29747, 28438, _t446 ] [ Modal Level Pure Literal Elimination, _t447 ] % 4.26/4.42 (1,1) [29794,0]. true => _t384 [ Unit Resolution, 29749, 28321, _t383 ] [ Modal Level Pure Literal Elimination, _t384 ] % 4.26/4.42 (1,1) [29796,0]. true => _t466 [ Unit Resolution, 29753, 28473, _t465 ] [ Modal Level Pure Literal Elimination, _t466 ] % 4.26/4.42 (1,1) [29798,0]. true => _t312 [ Unit Resolution, 29757, 28186, _t311 ] [ Modal Level Pure Literal Elimination, _t312 ] % 4.26/4.42 (1,1) [29800,0]. true => _t260 [ Unit Resolution, 29763, 28088, _t258 ] [ Modal Level Pure Literal Elimination, _t260 ] % 4.26/4.42 (1,1) [29801,0]. true => _t259 [ Unit Resolution, 29763, 28086, _t258 ] [ Modal Level Pure Literal Elimination, _t259 ] % 4.26/4.42 (1,1) [29802,0]. true => _t501 [ Unit Resolution, 29767, 28537, _t500 ] [ Modal Level Pure Literal Elimination, _t501 ] % 4.26/4.42 (1,1) [29804,0]. true => p26 | p25 [ Unit Resolution, 29770, 28030, _t230 ] % 4.26/4.42 (1,1) [29805,0]. true => _t532 [ Unit Resolution, 29772, 28595, _t531 ] [ Modal Level Pure Literal Elimination, _t532 ] % 4.26/4.42 (1,1) [29807,0]. true => _t286 [ Unit Resolution, 29774, 28137, _t285 ] [ Modal Level Pure Literal Elimination, _t286 ] % 4.26/4.42 (1,1) [29809,0]. true => _t288 [ Unit Resolution, 29807, 28141, _t286 ] [ Modal Level Pure Literal Elimination, _t288 ] % 4.26/4.42 (1,1) [29810,0]. true => _t287 [ Unit Resolution, 29807, 28139, _t286 ] [ Modal Level Pure Literal Elimination, _t287 ] % 4.26/4.42 (1,1) [29811,0]. true => _t502 [ Unit Resolution, 29802, 28539, _t501 ] [ Modal Level Pure Literal Elimination, _t502 ] % 4.26/4.42 (1,1) [29813,0]. true => ~p25 | ~p24 [ Unit Resolution, 29800, 28087, _t260 ] [ Backward Subsumption, 57045 ] % 4.26/4.42 (1,1) [29814,0]. true => _t467 [ Unit Resolution, 29796, 28475, _t466 ] [ Modal Level Pure Literal Elimination, _t467 ] % 4.26/4.42 (1,1) [29816,0]. true => _t448 [ Unit Resolution, 29792, 28440, _t447 ] [ Modal Level Pure Literal Elimination, _t448 ] % 4.26/4.42 (1,1) [29818,0]. true => _t428 [ Unit Resolution, 29788, 28403, _t427 ] [ Modal Level Pure Literal Elimination, _t428 ] % 4.26/4.42 (1,1) [29820,0]. true => _t362 [ Unit Resolution, 29784, 28280, _t361 ] [ Modal Level Pure Literal Elimination, _t362 ] % 4.26/4.42 (1,1) [29822,0]. true => _t338 [ Unit Resolution, 29778, 28235, _t337 ] [ Modal Level Pure Literal Elimination, _t338 ] % 4.26/4.42 (1,1) [29824,0]. true => _t518 [ Unit Resolution, 29780, 28568, _t517 ] [ Modal Level Pure Literal Elimination, _t518 ] % 4.26/4.42 (1,1) [29826,0]. true => _t485 [ Unit Resolution, 29786, 28508, _t484 ] [ Modal Level Pure Literal Elimination, _t485 ] % 4.26/4.42 (1,1) [29828,0]. true => _t407 [ Unit Resolution, 29790, 28364, _t406 ] [ Modal Level Pure Literal Elimination, _t407 ] % 4.26/4.42 (1,1) [29830,0]. true => _t385 [ Unit Resolution, 29794, 28323, _t384 ] [ Modal Level Pure Literal Elimination, _t385 ] % 4.26/4.42 (1,1) [29832,0]. true => _t313 [ Unit Resolution, 29798, 28188, _t312 ] [ Modal Level Pure Literal Elimination, _t313 ] % 4.26/4.42 (1,1) [29834,0]. true => p25 | p24 [ Unit Resolution, 29801, 28085, _t259 ] % 4.26/4.42 (1,1) [29836,0]. true => _t547 [ Unit Resolution, 29805, 28829, _t532 ] [ Modal Level Pure Literal Elimination, _t547 ] % 4.26/4.42 (1,1) [29837,0]. true => _t533 [ Unit Resolution, 29805, 28622, _t532 ] [ Modal Level Pure Literal Elimination, _t533 ] % 4.26/4.42 (1,1) [29838,0]. true => _t534 [ Unit Resolution, 29837, 28597, _t533 ] [ Modal Level Pure Literal Elimination, _t534 ] % 4.26/4.42 (1,1) [29841,0]. true => _t386 [ Unit Resolution, 29830, 28325, _t385 ] [ Modal Level Pure Literal Elimination, _t386 ] % 4.26/4.42 (1,1) [29843,0]. true => _t486 [ Unit Resolution, 29826, 28510, _t485 ] [ Modal Level Pure Literal Elimination, _t486 ] % 4.26/4.42 (1,1) [29845,0]. true => _t339 [ Unit Resolution, 29822, 28237, _t338 ] [ Modal Level Pure Literal Elimination, _t339 ] % 4.26/4.42 (1,1) [29847,0]. true => _t429 [ Unit Resolution, 29818, 28405, _t428 ] [ Modal Level Pure Literal Elimination, _t429 ] % 4.26/4.42 (1,1) [29849,0]. true => _t468 [ Unit Resolution, 29814, 28477, _t467 ] [ Modal Level Pure Literal Elimination, _t468 ] % 4.26/4.42 (1,1) [29851,0]. true => p24 | p23 [ Unit Resolution, 29810, 28138, _t287 ] % 4.26/4.42 (1,1) [29852,0]. true => ~p24 | ~p23 [ Unit Resolution, 29809, 28140, _t288 ] [ Backward Subsumption, 57044 ] % 4.26/4.42 (1,1) [29853,0]. true => _t503 [ Unit Resolution, 29811, 28541, _t502 ] [ Modal Level Pure Literal Elimination, _t503 ] % 4.26/4.42 (1,1) [29855,0]. true => _t449 [ Unit Resolution, 29816, 28442, _t448 ] [ Modal Level Pure Literal Elimination, _t449 ] % 4.26/4.42 (1,1) [29857,0]. true => _t363 [ Unit Resolution, 29820, 28282, _t362 ] [ Modal Level Pure Literal Elimination, _t363 ] % 4.26/4.42 (1,1) [29859,0]. true => _t519 [ Unit Resolution, 29824, 28570, _t518 ] [ Modal Level Pure Literal Elimination, _t519 ] % 4.26/4.42 (1,1) [29861,0]. true => _t408 [ Unit Resolution, 29828, 28366, _t407 ] [ Modal Level Pure Literal Elimination, _t408 ] % 4.26/4.42 (1,1) [29863,0]. true => _t315 [ Unit Resolution, 29832, 28192, _t313 ] [ Modal Level Pure Literal Elimination, _t315 ] % 4.26/4.42 (1,1) [29864,0]. true => _t314 [ Unit Resolution, 29832, 28190, _t313 ] [ Modal Level Pure Literal Elimination, _t314 ] % 4.26/4.42 (1,1) [29865,0]. true => _t548 [ Unit Resolution, 29836, 28624, _t547 ] [ Modal Level Pure Literal Elimination, _t548 ] % 4.26/4.42 (1,1) [29868,0]. true => _t562 [ Unit Resolution, 29865, 28826, _t548 ] [ Modal Level Pure Literal Elimination, _t562 ] % 4.26/4.42 (1,1) [29869,0]. true => _t549 [ Unit Resolution, 29865, 28649, _t548 ] [ Modal Level Pure Literal Elimination, _t549 ] % 4.26/4.42 (1,1) [29870,0]. true => ~p23 | ~p22 [ Unit Resolution, 29863, 28191, _t315 ] [ Backward Subsumption, 57043 ] % 4.26/4.42 (1,1) [29871,0]. true => _t520 [ Unit Resolution, 29859, 28572, _t519 ] [ Modal Level Pure Literal Elimination, _t520 ] % 4.26/4.42 (1,1) [29873,0]. true => _t450 [ Unit Resolution, 29855, 28444, _t449 ] [ Modal Level Pure Literal Elimination, _t450 ] % 4.26/4.42 (1,1) [29875,0]. true => _t469 [ Unit Resolution, 29849, 28479, _t468 ] [ Modal Level Pure Literal Elimination, _t469 ] % 4.26/4.42 (1,1) [29877,0]. true => _t341 [ Unit Resolution, 29845, 28241, _t339 ] [ Modal Level Pure Literal Elimination, _t341 ] % 4.26/4.42 (1,1) [29878,0]. true => _t340 [ Unit Resolution, 29845, 28239, _t339 ] [ Modal Level Pure Literal Elimination, _t340 ] % 4.26/4.42 (1,1) [29879,0]. true => _t387 [ Unit Resolution, 29841, 28327, _t386 ] [ Modal Level Pure Literal Elimination, _t387 ] % 4.26/4.42 (1,1) [29881,0]. true => _t535 [ Unit Resolution, 29838, 28599, _t534 ] [ Modal Level Pure Literal Elimination, _t535 ] % 4.26/4.42 (1,1) [29883,0]. true => _t487 [ Unit Resolution, 29843, 28512, _t486 ] [ Modal Level Pure Literal Elimination, _t487 ] % 4.26/4.42 (1,1) [29885,0]. true => _t430 [ Unit Resolution, 29847, 28407, _t429 ] [ Modal Level Pure Literal Elimination, _t430 ] % 4.26/4.42 (1,1) [29887,0]. true => _t504 [ Unit Resolution, 29853, 28543, _t503 ] [ Modal Level Pure Literal Elimination, _t504 ] % 4.26/4.42 (1,1) [29889,0]. true => _t364 [ Unit Resolution, 29857, 28284, _t363 ] [ Modal Level Pure Literal Elimination, _t364 ] % 4.26/4.42 (1,1) [29891,0]. true => _t409 [ Unit Resolution, 29861, 28368, _t408 ] [ Modal Level Pure Literal Elimination, _t409 ] % 4.26/4.42 (1,1) [29893,0]. true => p23 | p22 [ Unit Resolution, 29864, 28189, _t314 ] % 4.26/4.42 (1,1) [29894,0]. true => _t410 [ Unit Resolution, 29891, 28370, _t409 ] [ Modal Level Pure Literal Elimination, _t410 ] % 4.26/4.42 (1,1) [29896,0]. true => _t505 [ Unit Resolution, 29887, 28545, _t504 ] [ Modal Level Pure Literal Elimination, _t505 ] % 4.26/4.42 (1,1) [29898,0]. true => _t488 [ Unit Resolution, 29883, 28514, _t487 ] [ Modal Level Pure Literal Elimination, _t488 ] % 4.26/4.42 (1,1) [29900,0]. true => _t388 [ Unit Resolution, 29879, 28329, _t387 ] [ Modal Level Pure Literal Elimination, _t388 ] % 4.26/4.42 (1,1) [29902,0]. true => ~p22 | ~p21 [ Unit Resolution, 29877, 28240, _t341 ] [ Backward Subsumption, 57042 ] % 4.26/4.42 (1,1) [29903,0]. true => _t451 [ Unit Resolution, 29873, 28446, _t450 ] [ Modal Level Pure Literal Elimination, _t451 ] % 4.26/4.42 (1,1) [29905,0]. true => _t550 [ Unit Resolution, 29869, 28626, _t549 ] [ Modal Level Pure Literal Elimination, _t550 ] % 4.26/4.42 (1,1) [29908,0]. true => _t563 [ Unit Resolution, 29868, 28651, _t562 ] [ Modal Level Pure Literal Elimination, _t563 ] % 4.26/4.42 (1,1) [29910,0]. true => _t521 [ Unit Resolution, 29871, 28574, _t520 ] [ Modal Level Pure Literal Elimination, _t521 ] % 4.26/4.42 (1,1) [29912,0]. true => _t470 [ Unit Resolution, 29875, 28481, _t469 ] [ Modal Level Pure Literal Elimination, _t470 ] % 4.26/4.42 (1,1) [29914,0]. true => p22 | p21 [ Unit Resolution, 29878, 28238, _t340 ] % 4.26/4.42 (1,1) [29915,0]. true => _t536 [ Unit Resolution, 29881, 28601, _t535 ] [ Modal Level Pure Literal Elimination, _t536 ] % 4.26/4.42 (1,1) [29917,0]. true => _t431 [ Unit Resolution, 29885, 28409, _t430 ] [ Modal Level Pure Literal Elimination, _t431 ] % 4.26/4.42 (1,1) [29919,0]. true => _t366 [ Unit Resolution, 29889, 28288, _t364 ] [ Modal Level Pure Literal Elimination, _t366 ] % 4.26/4.42 (1,1) [29920,0]. true => _t365 [ Unit Resolution, 29889, 28286, _t364 ] [ Modal Level Pure Literal Elimination, _t365 ] % 4.26/4.42 (1,1) [29921,0]. true => p21 | p20 [ Unit Resolution, 29920, 28285, _t365 ] % 4.26/4.42 (1,1) [29922,0]. true => _t432 [ Unit Resolution, 29917, 28411, _t431 ] [ Modal Level Pure Literal Elimination, _t432 ] % 4.26/4.42 (1,1) [29924,0]. true => _t471 [ Unit Resolution, 29912, 28483, _t470 ] [ Modal Level Pure Literal Elimination, _t471 ] % 4.26/4.42 (1,1) [29927,0]. true => _t576 [ Unit Resolution, 29908, 28823, _t563 ] [ Modal Level Pure Literal Elimination, _t576 ] % 4.26/4.42 (1,1) [29928,0]. true => _t564 [ Unit Resolution, 29908, 28674, _t563 ] [ Modal Level Pure Literal Elimination, _t564 ] % 4.26/4.42 (1,1) [29929,0]. true => _t452 [ Unit Resolution, 29903, 28448, _t451 ] [ Modal Level Pure Literal Elimination, _t452 ] % 4.26/4.42 (1,1) [29931,0]. true => _t489 [ Unit Resolution, 29898, 28516, _t488 ] [ Modal Level Pure Literal Elimination, _t489 ] % 4.26/4.42 (1,1) [29933,0]. true => _t411 [ Unit Resolution, 29894, 28372, _t410 ] [ Modal Level Pure Literal Elimination, _t411 ] % 4.26/4.42 (1,1) [29935,0]. true => _t506 [ Unit Resolution, 29896, 28547, _t505 ] [ Modal Level Pure Literal Elimination, _t506 ] % 4.26/4.42 (1,1) [29937,0]. true => _t390 [ Unit Resolution, 29900, 28333, _t388 ] [ Modal Level Pure Literal Elimination, _t390 ] % 4.26/4.42 (1,1) [29938,0]. true => _t389 [ Unit Resolution, 29900, 28331, _t388 ] [ Modal Level Pure Literal Elimination, _t389 ] % 4.26/4.42 (1,1) [29939,0]. true => _t551 [ Unit Resolution, 29905, 28628, _t550 ] [ Modal Level Pure Literal Elimination, _t551 ] % 4.26/4.42 (1,1) [29941,0]. true => _t522 [ Unit Resolution, 29910, 28576, _t521 ] [ Modal Level Pure Literal Elimination, _t522 ] % 4.26/4.42 (1,1) [29943,0]. true => _t537 [ Unit Resolution, 29915, 28603, _t536 ] [ Modal Level Pure Literal Elimination, _t537 ] % 4.26/4.42 (1,1) [29945,0]. true => ~p21 | ~p20 [ Unit Resolution, 29919, 28287, _t366 ] [ Backward Subsumption, 57041 ] % 4.26/4.42 (1,1) [29946,0]. true => _t538 [ Unit Resolution, 29943, 28605, _t537 ] [ Modal Level Pure Literal Elimination, _t538 ] % 4.26/4.42 (1,1) [29948,0]. true => _t552 [ Unit Resolution, 29939, 28630, _t551 ] [ Modal Level Pure Literal Elimination, _t552 ] % 4.26/4.42 (1,1) [29950,0]. true => ~p20 | ~p19 [ Unit Resolution, 29937, 28332, _t390 ] [ Backward Subsumption, 57040 ] % 4.26/4.42 (1,1) [29951,0]. true => _t413 [ Unit Resolution, 29933, 28376, _t411 ] [ Modal Level Pure Literal Elimination, _t413 ] % 4.26/4.42 (1,1) [29952,0]. true => _t412 [ Unit Resolution, 29933, 28374, _t411 ] [ Modal Level Pure Literal Elimination, _t412 ] % 4.26/4.42 (1,1) [29953,0]. true => _t453 [ Unit Resolution, 29929, 28450, _t452 ] [ Modal Level Pure Literal Elimination, _t453 ] % 4.26/4.42 (1,1) [29955,0]. true => _t577 [ Unit Resolution, 29927, 28676, _t576 ] [ Modal Level Pure Literal Elimination, _t577 ] % 4.26/4.42 (1,1) [29957,0]. true => _t472 [ Unit Resolution, 29924, 28485, _t471 ] [ Modal Level Pure Literal Elimination, _t472 ] % 4.26/4.42 (1,1) [29959,0]. true => _t433 [ Unit Resolution, 29922, 28413, _t432 ] [ Modal Level Pure Literal Elimination, _t433 ] % 4.26/4.42 (1,1) [29962,0]. true => _t565 [ Unit Resolution, 29928, 28653, _t564 ] [ Modal Level Pure Literal Elimination, _t565 ] % 4.26/4.42 (1,1) [29964,0]. true => _t490 [ Unit Resolution, 29931, 28518, _t489 ] [ Modal Level Pure Literal Elimination, _t490 ] % 4.26/4.42 (1,1) [29966,0]. true => _t507 [ Unit Resolution, 29935, 28549, _t506 ] [ Modal Level Pure Literal Elimination, _t507 ] % 4.26/4.42 (1,1) [29968,0]. true => p20 | p19 [ Unit Resolution, 29938, 28330, _t389 ] % 4.26/4.42 (1,1) [29969,0]. true => _t523 [ Unit Resolution, 29941, 28578, _t522 ] [ Modal Level Pure Literal Elimination, _t523 ] % 4.26/4.42 (1,1) [29971,0]. true => _t524 [ Unit Resolution, 29969, 28580, _t523 ] [ Modal Level Pure Literal Elimination, _t524 ] % 4.26/4.42 (1,1) [29973,0]. true => _t491 [ Unit Resolution, 29964, 28520, _t490 ] [ Modal Level Pure Literal Elimination, _t491 ] % 4.26/4.42 (1,1) [29975,0]. true => _t435 [ Unit Resolution, 29959, 28417, _t433 ] [ Modal Level Pure Literal Elimination, _t435 ] % 4.26/4.42 (1,1) [29976,0]. true => _t434 [ Unit Resolution, 29959, 28415, _t433 ] [ Modal Level Pure Literal Elimination, _t434 ] % 4.26/4.42 (1,1) [29978,0]. true => _t589 [ Unit Resolution, 29955, 28820, _t577 ] [ Modal Level Pure Literal Elimination, _t589 ] % 4.26/4.42 (1,1) [29979,0]. true => _t578 [ Unit Resolution, 29955, 28697, _t577 ] [ Modal Level Pure Literal Elimination, _t578 ] % 4.26/4.42 (1,1) [29980,0]. true => p19 | p18 [ Unit Resolution, 29952, 28373, _t412 ] % 4.26/4.42 (1,1) [29981,0]. true => _t553 [ Unit Resolution, 29948, 28632, _t552 ] [ Modal Level Pure Literal Elimination, _t553 ] % 4.26/4.42 (1,1) [29983,0]. true => _t539 [ Unit Resolution, 29946, 28607, _t538 ] [ Modal Level Pure Literal Elimination, _t539 ] % 4.26/4.42 (1,1) [29985,0]. true => ~p19 | ~p18 [ Unit Resolution, 29951, 28375, _t413 ] [ Backward Subsumption, 57039 ] % 4.26/4.42 (1,1) [29986,0]. true => _t454 [ Unit Resolution, 29953, 28452, _t453 ] [ Modal Level Pure Literal Elimination, _t454 ] % 4.26/4.42 (1,1) [29988,0]. true => _t473 [ Unit Resolution, 29957, 28487, _t472 ] [ Modal Level Pure Literal Elimination, _t473 ] % 4.26/4.42 (1,1) [29990,0]. true => _t566 [ Unit Resolution, 29962, 28655, _t565 ] [ Modal Level Pure Literal Elimination, _t566 ] % 4.26/4.42 (1,1) [29992,0]. true => _t508 [ Unit Resolution, 29966, 28551, _t507 ] [ Modal Level Pure Literal Elimination, _t508 ] % 4.26/4.42 (1,1) [29994,0]. true => _t509 [ Unit Resolution, 29992, 28553, _t508 ] [ Modal Level Pure Literal Elimination, _t509 ] % 4.26/4.42 (1,1) [29996,0]. true => _t474 [ Unit Resolution, 29988, 28489, _t473 ] [ Modal Level Pure Literal Elimination, _t474 ] % 4.26/4.42 (1,1) [29998,0]. true => _t540 [ Unit Resolution, 29983, 28609, _t539 ] [ Modal Level Pure Literal Elimination, _t540 ] % 4.26/4.42 (1,1) [30000,0]. true => _t579 [ Unit Resolution, 29979, 28678, _t578 ] [ Modal Level Pure Literal Elimination, _t579 ] % 4.26/4.42 (1,1) [30003,0]. true => ~p18 | ~p17 [ Unit Resolution, 29975, 28416, _t435 ] [ Backward Subsumption, 57038 ] % 4.26/4.42 (1,1) [30004,0]. true => _t525 [ Unit Resolution, 29971, 28582, _t524 ] [ Modal Level Pure Literal Elimination, _t525 ] % 4.26/4.42 (1,1) [30006,0]. true => _t492 [ Unit Resolution, 29973, 28522, _t491 ] [ Modal Level Pure Literal Elimination, _t492 ] % 4.26/4.42 (1,1) [30008,0]. true => p18 | p17 [ Unit Resolution, 29976, 28414, _t434 ] % 4.26/4.42 (1,1) [30009,0]. true => _t590 [ Unit Resolution, 29978, 28699, _t589 ] [ Modal Level Pure Literal Elimination, _t590 ] % 4.26/4.42 (1,1) [30011,0]. true => _t554 [ Unit Resolution, 29981, 28634, _t553 ] [ Modal Level Pure Literal Elimination, _t554 ] % 4.26/4.42 (1,1) [30013,0]. true => _t456 [ Unit Resolution, 29986, 28456, _t454 ] [ Modal Level Pure Literal Elimination, _t456 ] % 4.26/4.42 (1,1) [30014,0]. true => _t455 [ Unit Resolution, 29986, 28454, _t454 ] [ Modal Level Pure Literal Elimination, _t455 ] % 4.26/4.42 (1,1) [30015,0]. true => _t567 [ Unit Resolution, 29990, 28657, _t566 ] [ Modal Level Pure Literal Elimination, _t567 ] % 4.26/4.42 (1,1) [30017,0]. true => _t568 [ Unit Resolution, 30015, 28659, _t567 ] [ Modal Level Pure Literal Elimination, _t568 ] % 4.26/4.42 (1,1) [30019,0]. true => ~p17 | ~p16 [ Unit Resolution, 30013, 28455, _t456 ] [ Backward Subsumption, 57037 ] % 4.26/4.42 (1,1) [30021,0]. true => _t601 [ Unit Resolution, 30009, 28817, _t590 ] [ Modal Level Pure Literal Elimination, _t601 ] % 4.26/4.42 (1,1) [30022,0]. true => _t591 [ Unit Resolution, 30009, 28718, _t590 ] [ Modal Level Pure Literal Elimination, _t591 ] % 4.26/4.42 (1,1) [30023,0]. true => _t526 [ Unit Resolution, 30004, 28584, _t525 ] [ Modal Level Pure Literal Elimination, _t526 ] % 4.26/4.42 (1,1) [30025,0]. true => _t541 [ Unit Resolution, 29998, 28611, _t540 ] [ Modal Level Pure Literal Elimination, _t541 ] % 4.26/4.42 (1,1) [30027,0]. true => _t510 [ Unit Resolution, 29994, 28555, _t509 ] [ Modal Level Pure Literal Elimination, _t510 ] % 4.26/4.42 (1,1) [30029,0]. true => _t476 [ Unit Resolution, 29996, 28493, _t474 ] [ Modal Level Pure Literal Elimination, _t476 ] % 4.26/4.42 (1,1) [30030,0]. true => _t475 [ Unit Resolution, 29996, 28491, _t474 ] [ Modal Level Pure Literal Elimination, _t475 ] % 4.26/4.42 (1,1) [30031,0]. true => _t580 [ Unit Resolution, 30000, 28680, _t579 ] [ Modal Level Pure Literal Elimination, _t580 ] % 4.26/4.42 (1,1) [30033,0]. true => _t493 [ Unit Resolution, 30006, 28524, _t492 ] [ Modal Level Pure Literal Elimination, _t493 ] % 4.26/4.42 (1,1) [30035,0]. true => _t555 [ Unit Resolution, 30011, 28636, _t554 ] [ Modal Level Pure Literal Elimination, _t555 ] % 4.26/4.42 (1,1) [30037,0]. true => p17 | p16 [ Unit Resolution, 30014, 28453, _t455 ] % 4.26/4.42 (1,1) [30038,0]. true => _t556 [ Unit Resolution, 30035, 28638, _t555 ] [ Modal Level Pure Literal Elimination, _t556 ] % 4.26/4.42 (1,1) [30040,0]. true => _t581 [ Unit Resolution, 30031, 28682, _t580 ] [ Modal Level Pure Literal Elimination, _t581 ] % 4.26/4.42 (1,1) [30042,0]. true => ~p16 | ~p15 [ Unit Resolution, 30029, 28492, _t476 ] [ Backward Subsumption, 57036 ] % 4.26/4.42 (1,1) [30043,0]. true => _t542 [ Unit Resolution, 30025, 28613, _t541 ] [ Modal Level Pure Literal Elimination, _t542 ] % 4.26/4.42 (1,1) [30045,0]. true => _t592 [ Unit Resolution, 30022, 28701, _t591 ] [ Modal Level Pure Literal Elimination, _t592 ] % 4.26/4.42 (1,1) [30048,0]. true => _t569 [ Unit Resolution, 30017, 28661, _t568 ] [ Modal Level Pure Literal Elimination, _t569 ] % 4.26/4.42 (1,1) [30050,0]. true => _t602 [ Unit Resolution, 30021, 28720, _t601 ] [ Modal Level Pure Literal Elimination, _t602 ] % 4.26/4.42 (1,1) [30052,0]. true => _t527 [ Unit Resolution, 30023, 28586, _t526 ] [ Modal Level Pure Literal Elimination, _t527 ] % 4.26/4.42 (1,1) [30054,0]. true => _t511 [ Unit Resolution, 30027, 28557, _t510 ] [ Modal Level Pure Literal Elimination, _t511 ] % 4.26/4.42 (1,1) [30056,0]. true => p16 | p15 [ Unit Resolution, 30030, 28490, _t475 ] % 4.26/4.42 (1,1) [30057,0]. true => _t495 [ Unit Resolution, 30033, 28528, _t493 ] [ Modal Level Pure Literal Elimination, _t495 ] % 4.26/4.42 (1,1) [30058,0]. true => _t494 [ Unit Resolution, 30033, 28526, _t493 ] [ Modal Level Pure Literal Elimination, _t494 ] % 4.26/4.42 (1,1) [30059,0]. true => p15 | p14 [ Unit Resolution, 30058, 28525, _t494 ] % 4.26/4.42 (1,1) [30060,0]. true => _t513 [ Unit Resolution, 30054, 28561, _t511 ] [ Modal Level Pure Literal Elimination, _t513 ] % 4.26/4.42 (1,1) [30061,0]. true => _t512 [ Unit Resolution, 30054, 28559, _t511 ] [ Modal Level Pure Literal Elimination, _t512 ] % 4.26/4.42 (1,1) [30063,0]. true => _t612 [ Unit Resolution, 30050, 28814, _t602 ] [ Modal Level Pure Literal Elimination, _t612 ] % 4.26/4.42 (1,1) [30064,0]. true => _t603 [ Unit Resolution, 30050, 28737, _t602 ] [ Modal Level Pure Literal Elimination, _t603 ] % 4.26/4.42 (1,1) [30065,0]. true => _t593 [ Unit Resolution, 30045, 28703, _t592 ] [ Modal Level Pure Literal Elimination, _t593 ] % 4.26/4.42 (1,1) [30067,0]. true => _t582 [ Unit Resolution, 30040, 28684, _t581 ] [ Modal Level Pure Literal Elimination, _t582 ] % 4.26/4.42 (1,1) [30069,0]. true => _t557 [ Unit Resolution, 30038, 28640, _t556 ] [ Modal Level Pure Literal Elimination, _t557 ] % 4.26/4.42 (1,1) [30071,0]. true => _t543 [ Unit Resolution, 30043, 28615, _t542 ] [ Modal Level Pure Literal Elimination, _t543 ] % 4.26/4.42 (1,1) [30073,0]. true => _t570 [ Unit Resolution, 30048, 28663, _t569 ] [ Modal Level Pure Literal Elimination, _t570 ] % 4.26/4.42 (1,1) [30075,0]. true => _t528 [ Unit Resolution, 30052, 28588, _t527 ] [ Modal Level Pure Literal Elimination, _t528 ] % 4.26/4.42 (1,1) [30077,0]. true => ~p15 | ~p14 [ Unit Resolution, 30057, 28527, _t495 ] [ Backward Subsumption, 57035 ] % 4.26/4.42 (1,1) [30078,0]. true => _t530 [ Unit Resolution, 30075, 28592, _t528 ] [ Modal Level Pure Literal Elimination, _t530 ] % 4.26/4.42 (1,1) [30079,0]. true => _t529 [ Unit Resolution, 30075, 28590, _t528 ] [ Modal Level Pure Literal Elimination, _t529 ] % 4.26/4.42 (1,1) [30080,0]. true => _t544 [ Unit Resolution, 30071, 28617, _t543 ] [ Modal Level Pure Literal Elimination, _t544 ] % 4.26/4.42 (1,1) [30082,0]. true => _t583 [ Unit Resolution, 30067, 28686, _t582 ] [ Modal Level Pure Literal Elimination, _t583 ] % 4.26/4.42 (1,1) [30084,0]. true => _t604 [ Unit Resolution, 30064, 28722, _t603 ] [ Modal Level Pure Literal Elimination, _t604 ] % 4.26/4.42 (1,1) [30087,0]. true => ~p14 | ~p13 [ Unit Resolution, 30060, 28560, _t513 ] [ Backward Subsumption, 57034 ] % 4.26/4.42 (1,1) [30088,0]. true => p14 | p13 [ Unit Resolution, 30061, 28558, _t512 ] % 4.26/4.42 (1,1) [30089,0]. true => _t613 [ Unit Resolution, 30063, 28739, _t612 ] [ Modal Level Pure Literal Elimination, _t613 ] % 4.26/4.42 (1,1) [30091,0]. true => _t594 [ Unit Resolution, 30065, 28705, _t593 ] [ Modal Level Pure Literal Elimination, _t594 ] % 4.26/4.42 (1,1) [30093,0]. true => _t558 [ Unit Resolution, 30069, 28642, _t557 ] [ Modal Level Pure Literal Elimination, _t558 ] % 4.26/4.42 (1,1) [30095,0]. true => _t571 [ Unit Resolution, 30073, 28665, _t570 ] [ Modal Level Pure Literal Elimination, _t571 ] % 4.26/4.42 (1,1) [30097,0]. true => _t572 [ Unit Resolution, 30095, 28667, _t571 ] [ Modal Level Pure Literal Elimination, _t572 ] % 4.26/4.42 (1,1) [30099,0]. true => _t595 [ Unit Resolution, 30091, 28707, _t594 ] [ Modal Level Pure Literal Elimination, _t595 ] % 4.26/4.42 (1,1) [30101,0]. true => _t605 [ Unit Resolution, 30084, 28724, _t604 ] [ Modal Level Pure Literal Elimination, _t605 ] % 4.26/4.42 (1,1) [30103,0]. true => _t546 [ Unit Resolution, 30080, 28621, _t544 ] [ Modal Level Pure Literal Elimination, _t546 ] % 4.26/4.42 (1,1) [30104,0]. true => _t545 [ Unit Resolution, 30080, 28619, _t544 ] [ Modal Level Pure Literal Elimination, _t545 ] % 4.26/4.42 (1,1) [30105,0]. true => ~p13 | ~p12 [ Unit Resolution, 30078, 28591, _t530 ] [ Backward Subsumption, 57033 ] % 4.26/4.42 (1,1) [30106,0]. true => p13 | p12 [ Unit Resolution, 30079, 28589, _t529 ] % 4.26/4.42 (1,1) [30107,0]. true => _t584 [ Unit Resolution, 30082, 28688, _t583 ] [ Modal Level Pure Literal Elimination, _t584 ] % 4.26/4.42 (1,1) [30110,0]. true => _t622 [ Unit Resolution, 30089, 28811, _t613 ] [ Modal Level Pure Literal Elimination, _t622 ] % 4.26/4.42 (1,1) [30111,0]. true => _t614 [ Unit Resolution, 30089, 28754, _t613 ] [ Modal Level Pure Literal Elimination, _t614 ] % 4.26/4.42 (1,1) [30112,0]. true => _t559 [ Unit Resolution, 30093, 28644, _t558 ] [ Modal Level Pure Literal Elimination, _t559 ] % 4.26/4.42 (1,1) [30114,0]. true => _t561 [ Unit Resolution, 30112, 28648, _t559 ] [ Modal Level Pure Literal Elimination, _t561 ] % 4.26/4.42 (1,1) [30115,0]. true => _t560 [ Unit Resolution, 30112, 28646, _t559 ] [ Modal Level Pure Literal Elimination, _t560 ] % 4.26/4.42 (1,1) [30116,0]. true => _t623 [ Unit Resolution, 30110, 28756, _t622 ] [ Modal Level Pure Literal Elimination, _t623 ] % 4.26/4.42 (1,1) [30118,0]. true => _t585 [ Unit Resolution, 30107, 28690, _t584 ] [ Modal Level Pure Literal Elimination, _t585 ] % 4.26/4.42 (1,1) [30120,0]. true => ~p12 | ~p11 [ Unit Resolution, 30103, 28620, _t546 ] [ Backward Subsumption, 57032 ] % 4.26/4.42 (1,1) [30121,0]. true => _t596 [ Unit Resolution, 30099, 28709, _t595 ] [ Modal Level Pure Literal Elimination, _t596 ] % 4.26/4.42 (1,1) [30123,0]. true => _t573 [ Unit Resolution, 30097, 28669, _t572 ] [ Modal Level Pure Literal Elimination, _t573 ] % 4.26/4.42 (1,1) [30125,0]. true => _t606 [ Unit Resolution, 30101, 28726, _t605 ] [ Modal Level Pure Literal Elimination, _t606 ] % 4.26/4.42 (1,1) [30127,0]. true => p12 | p11 [ Unit Resolution, 30104, 28618, _t545 ] % 4.26/4.42 (1,1) [30129,0]. true => _t615 [ Unit Resolution, 30111, 28741, _t614 ] [ Modal Level Pure Literal Elimination, _t615 ] % 4.26/4.42 (1,1) [30131,0]. true => _t616 [ Unit Resolution, 30129, 28743, _t615 ] [ Modal Level Pure Literal Elimination, _t616 ] % 4.26/4.42 (1,1) [30133,0]. true => _t575 [ Unit Resolution, 30123, 28673, _t573 ] [ Modal Level Pure Literal Elimination, _t575 ] % 4.26/4.42 (1,1) [30134,0]. true => _t574 [ Unit Resolution, 30123, 28671, _t573 ] [ Modal Level Pure Literal Elimination, _t574 ] % 4.26/4.42 (1,1) [30135,0]. true => _t586 [ Unit Resolution, 30118, 28692, _t585 ] [ Modal Level Pure Literal Elimination, _t586 ] % 4.26/4.42 (1,1) [30137,0]. true => p11 | p10 [ Unit Resolution, 30115, 28645, _t560 ] % 4.26/4.42 (1,1) [30138,0]. true => ~p11 | ~p10 [ Unit Resolution, 30114, 28647, _t561 ] [ Backward Subsumption, 57031 ] % 4.26/4.42 (1,1) [30140,0]. true => _t631 [ Unit Resolution, 30116, 28808, _t623 ] [ Modal Level Pure Literal Elimination, _t631 ] % 4.26/4.42 (1,1) [30141,0]. true => _t624 [ Unit Resolution, 30116, 28769, _t623 ] [ Modal Level Pure Literal Elimination, _t624 ] % 4.26/4.42 (1,1) [30142,0]. true => _t597 [ Unit Resolution, 30121, 28711, _t596 ] [ Modal Level Pure Literal Elimination, _t597 ] % 4.26/4.42 (1,1) [30144,0]. true => _t607 [ Unit Resolution, 30125, 28728, _t606 ] [ Modal Level Pure Literal Elimination, _t607 ] % 4.26/4.42 (1,1) [30146,0]. true => _t608 [ Unit Resolution, 30144, 28730, _t607 ] [ Modal Level Pure Literal Elimination, _t608 ] % 4.26/4.42 (1,1) [30148,0]. true => _t625 [ Unit Resolution, 30141, 28758, _t624 ] [ Modal Level Pure Literal Elimination, _t625 ] % 4.26/4.42 (1,1) [30151,0]. true => p10 | p9 [ Unit Resolution, 30134, 28670, _t574 ] % 4.26/4.42 (1,1) [30152,0]. true => _t617 [ Unit Resolution, 30131, 28745, _t616 ] [ Modal Level Pure Literal Elimination, _t617 ] % 4.26/4.42 (1,1) [30154,0]. true => ~p10 | ~p9 [ Unit Resolution, 30133, 28672, _t575 ] [ Backward Subsumption, 57030 ] % 4.26/4.42 (1,1) [30155,0]. true => _t588 [ Unit Resolution, 30135, 28696, _t586 ] [ Modal Level Pure Literal Elimination, _t588 ] % 4.26/4.42 (1,1) [30156,0]. true => _t587 [ Unit Resolution, 30135, 28694, _t586 ] [ Modal Level Pure Literal Elimination, _t587 ] % 4.26/4.42 (1,1) [30157,0]. true => _t632 [ Unit Resolution, 30140, 28771, _t631 ] [ Modal Level Pure Literal Elimination, _t632 ] % 4.26/4.42 (1,1) [30159,0]. true => _t598 [ Unit Resolution, 30142, 28713, _t597 ] [ Modal Level Pure Literal Elimination, _t598 ] % 4.26/4.42 (1,1) [30161,0]. true => _t600 [ Unit Resolution, 30159, 28717, _t598 ] [ Modal Level Pure Literal Elimination, _t600 ] % 4.26/4.42 (1,1) [30162,0]. true => _t599 [ Unit Resolution, 30159, 28715, _t598 ] [ Modal Level Pure Literal Elimination, _t599 ] % 4.26/4.42 (1,1) [30163,0]. true => p9 | p8 [ Unit Resolution, 30156, 28693, _t587 ] % 4.26/4.42 (1,1) [30164,0]. true => _t618 [ Unit Resolution, 30152, 28747, _t617 ] [ Modal Level Pure Literal Elimination, _t618 ] % 4.26/4.42 (1,1) [30166,0]. true => _t609 [ Unit Resolution, 30146, 28732, _t608 ] [ Modal Level Pure Literal Elimination, _t609 ] % 4.26/4.42 (1,1) [30168,0]. true => _t626 [ Unit Resolution, 30148, 28760, _t625 ] [ Modal Level Pure Literal Elimination, _t626 ] % 4.26/4.42 (1,1) [30170,0]. true => ~p9 | ~p8 [ Unit Resolution, 30155, 28695, _t588 ] [ Backward Subsumption, 57029 ] % 4.26/4.42 (1,1) [30172,0]. true => _t639 [ Unit Resolution, 30157, 28805, _t632 ] [ Modal Level Pure Literal Elimination, _t639 ] % 4.26/4.42 (1,1) [30173,0]. true => _t633 [ Unit Resolution, 30157, 28782, _t632 ] [ Modal Level Pure Literal Elimination, _t633 ] % 4.26/4.42 (1,1) [30174,0]. true => _t634 [ Unit Resolution, 30173, 28773, _t633 ] [ Modal Level Pure Literal Elimination, _t634 ] % 4.26/4.42 (1,1) [30177,0]. true => _t611 [ Unit Resolution, 30166, 28736, _t609 ] [ Modal Level Pure Literal Elimination, _t611 ] % 4.26/4.42 (1,1) [30178,0]. true => _t610 [ Unit Resolution, 30166, 28734, _t609 ] [ Modal Level Pure Literal Elimination, _t610 ] % 4.26/4.42 (1,1) [30179,0]. true => p8 | p7 [ Unit Resolution, 30162, 28714, _t599 ] % 4.26/4.42 (1,1) [30180,0]. true => ~p8 | ~p7 [ Unit Resolution, 30161, 28716, _t600 ] [ Backward Subsumption, 57028 ] % 4.26/4.42 (1,1) [30181,0]. true => _t619 [ Unit Resolution, 30164, 28749, _t618 ] [ Modal Level Pure Literal Elimination, _t619 ] % 4.26/4.42 (1,1) [30183,0]. true => _t627 [ Unit Resolution, 30168, 28762, _t626 ] [ Modal Level Pure Literal Elimination, _t627 ] % 4.26/4.42 (1,1) [30185,0]. true => _t640 [ Unit Resolution, 30172, 28784, _t639 ] [ Modal Level Pure Literal Elimination, _t640 ] % 4.26/4.42 (1,1) [30188,0]. true => _t646 [ Unit Resolution, 30185, 28802, _t640 ] [ Modal Level Pure Literal Elimination, _t646 ] % 4.26/4.42 (1,1) [30189,0]. true => _t641 [ Unit Resolution, 30185, 28793, _t640 ] [ Modal Level Pure Literal Elimination, _t641 ] % 4.26/4.42 (1,1) [30190,0]. true => _t621 [ Unit Resolution, 30181, 28753, _t619 ] [ Modal Level Pure Literal Elimination, _t621 ] % 4.26/4.42 (1,1) [30191,0]. true => _t620 [ Unit Resolution, 30181, 28751, _t619 ] [ Modal Level Pure Literal Elimination, _t620 ] % 4.26/4.42 (1,1) [30192,0]. true => ~p7 | ~p6 [ Unit Resolution, 30177, 28735, _t611 ] [ Backward Subsumption, 57027 ] % 4.26/4.42 (1,1) [30193,0]. true => _t635 [ Unit Resolution, 30174, 28775, _t634 ] [ Modal Level Pure Literal Elimination, _t635 ] % 4.26/4.42 (1,1) [30195,0]. true => p7 | p6 [ Unit Resolution, 30178, 28733, _t610 ] % 4.26/4.42 (1,1) [30196,0]. true => _t628 [ Unit Resolution, 30183, 28764, _t627 ] [ Modal Level Pure Literal Elimination, _t628 ] % 4.26/4.42 (1,1) [30198,0]. true => _t630 [ Unit Resolution, 30196, 28768, _t628 ] [ Modal Level Pure Literal Elimination, _t630 ] % 4.26/4.42 (1,1) [30199,0]. true => _t629 [ Unit Resolution, 30196, 28766, _t628 ] [ Modal Level Pure Literal Elimination, _t629 ] % 4.26/4.42 (1,1) [30200,0]. true => p6 | p5 [ Unit Resolution, 30191, 28750, _t620 ] % 4.26/4.42 (1,1) [30201,0]. true => _t642 [ Unit Resolution, 30189, 28786, _t641 ] [ Modal Level Pure Literal Elimination, _t642 ] % 4.26/4.42 (1,1) [30204,0]. true => _t647 [ Unit Resolution, 30188, 28795, _t646 ] [ Modal Level Pure Literal Elimination, _t647 ] % 4.26/4.42 (1,1) [30206,0]. true => ~p6 | ~p5 [ Unit Resolution, 30190, 28752, _t621 ] [ Backward Subsumption, 57026 ] % 4.26/4.42 (1,1) [30207,0]. true => _t636 [ Unit Resolution, 30193, 28777, _t635 ] [ Modal Level Pure Literal Elimination, _t636 ] % 4.26/4.42 (1,1) [30209,0]. true => _t638 [ Unit Resolution, 30207, 28781, _t636 ] [ Modal Level Pure Literal Elimination, _t638 ] % 4.26/4.42 (1,1) [30210,0]. true => _t637 [ Unit Resolution, 30207, 28779, _t636 ] [ Modal Level Pure Literal Elimination, _t637 ] % 4.26/4.42 (1,1) [30211,0]. true => _t643 [ Unit Resolution, 30201, 28788, _t642 ] [ Modal Level Pure Literal Elimination, _t643 ] % 4.26/4.42 (1,1) [30213,0]. true => ~p5 | ~p4 [ Unit Resolution, 30198, 28767, _t630 ] [ Backward Subsumption, 57025 ] % 4.26/4.42 (1,1) [30214,0]. true => p5 | p4 [ Unit Resolution, 30199, 28765, _t629 ] % 4.26/4.42 (1,1) [30215,0]. true => _t648 [ Unit Resolution, 30204, 28797, _t647 ] [ Modal Level Pure Literal Elimination, _t648 ] % 4.26/4.42 (1,1) [30217,0]. true => _t650 [ Unit Resolution, 30215, 28801, _t648 ] [ Modal Level Pure Literal Elimination, _t650 ] % 4.26/4.42 (1,1) [30218,0]. true => _t649 [ Unit Resolution, 30215, 28799, _t648 ] [ Modal Level Pure Literal Elimination, _t649 ] % 4.26/4.42 (1,1) [30219,0]. true => p4 | p3 [ Unit Resolution, 30210, 28778, _t637 ] % 4.26/4.42 (1,1) [30220,0]. true => ~p4 | ~p3 [ Unit Resolution, 30209, 28780, _t638 ] [ Backward Subsumption, 57024 ] % 4.26/4.42 (1,1) [30221,0]. true => _t645 [ Unit Resolution, 30211, 28792, _t643 ] [ Modal Level Pure Literal Elimination, _t645 ] % 4.26/4.42 (1,1) [30222,0]. true => _t644 [ Unit Resolution, 30211, 28790, _t643 ] [ Modal Level Pure Literal Elimination, _t644 ] % 4.26/4.42 (1,1) [30223,0]. true => p3 | p2 [ Unit Resolution, 30222, 28789, _t644 ] % 4.26/4.42 (1,1) [30224,0]. true => p2 | p1 [ Unit Resolution, 30218, 28798, _t649 ] [ Backward Subsumption, 57021 ] % 4.26/4.42 (1,1) [30225,0]. true => ~p2 | ~p1 [ Unit Resolution, 30217, 28800, _t650 ] [ Backward Subsumption, 57023 ] % 4.26/4.42 (1,1) [30226,0]. true => ~p3 | ~p2 [ Unit Resolution, 30221, 28791, _t645 ] [ Backward Subsumption, 57022 ] % 4.26/4.42 (1,1) [54091,0]. true => p31 | ~p2 [ LRES, 30225, 29606, ~p1 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [54125,0]. true => ~p31 | p2 [ LRES, 29580, 30224, ~p1 ] [ Backward Subsumption, 57018 ] % 4.26/4.42 (1,1) [55082,0]. true => p31 | p3 [ LRES, 54091, 30223, ~p2 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [55148,0]. true => ~p31 | ~p3 [ LRES, 54125, 30226, p2 ] [ Backward Subsumption, 57017 ] % 4.26/4.42 (1,1) [55181,0]. true => p31 | ~p4 [ LRES, 55082, 30220, p3 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [55215,0]. true => ~p31 | p4 [ LRES, 55148, 30219, ~p3 ] [ Backward Subsumption, 57016 ] % 4.26/4.42 (1,1) [55248,0]. true => p31 | p5 [ LRES, 55181, 30214, ~p4 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [55282,0]. true => ~p31 | ~p5 [ LRES, 55215, 30213, p4 ] [ Backward Subsumption, 57015 ] % 4.26/4.42 (1,1) [55314,0]. true => p31 | ~p6 [ LRES, 55248, 30206, p5 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [55347,0]. true => ~p31 | p6 [ LRES, 55282, 30200, ~p5 ] [ Backward Subsumption, 57014 ] % 4.26/4.42 (1,1) [55380,0]. true => p31 | p7 [ LRES, 55314, 30195, ~p6 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [55414,0]. true => ~p31 | ~p7 [ LRES, 55347, 30192, p6 ] [ Backward Subsumption, 57013 ] % 4.26/4.42 (1,1) [55447,0]. true => p31 | ~p8 [ LRES, 55380, 30180, p7 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [55481,0]. true => ~p31 | p8 [ LRES, 55414, 30179, ~p7 ] [ Backward Subsumption, 57012 ] % 4.26/4.42 (1,1) [55514,0]. true => p31 | p9 [ LRES, 55447, 30163, ~p8 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [55548,0]. true => ~p31 | ~p9 [ LRES, 55481, 30170, p8 ] [ Backward Subsumption, 57011 ] % 4.26/4.42 (1,1) [55581,0]. true => p31 | ~p10 [ LRES, 55514, 30154, p9 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [55615,0]. true => ~p31 | p10 [ LRES, 55548, 30151, ~p9 ] [ Backward Subsumption, 57010 ] % 4.26/4.42 (1,1) [55648,0]. true => p31 | p11 [ LRES, 55581, 30137, ~p10 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [55682,0]. true => ~p31 | ~p11 [ LRES, 55615, 30138, p10 ] [ Backward Subsumption, 57009 ] % 4.26/4.42 (1,1) [55715,0]. true => p31 | ~p12 [ LRES, 55648, 30120, p11 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [55749,0]. true => ~p31 | p12 [ LRES, 55682, 30127, ~p11 ] [ Backward Subsumption, 57008 ] % 4.26/4.42 (1,1) [55782,0]. true => p31 | p13 [ LRES, 55715, 30106, ~p12 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [55816,0]. true => ~p31 | ~p13 [ LRES, 55749, 30105, p12 ] [ Backward Subsumption, 57007 ] % 4.26/4.42 (1,1) [55849,0]. true => p31 | ~p14 [ LRES, 55782, 30087, p13 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [55883,0]. true => ~p31 | p14 [ LRES, 55816, 30088, ~p13 ] [ Backward Subsumption, 57006 ] % 4.26/4.42 (1,1) [55916,0]. true => p31 | p15 [ LRES, 55849, 30059, ~p14 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [55950,0]. true => ~p31 | ~p15 [ LRES, 55883, 30077, p14 ] [ Backward Subsumption, 57005 ] % 4.26/4.42 (1,1) [55983,0]. true => p31 | ~p16 [ LRES, 55916, 30042, p15 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [56017,0]. true => ~p31 | p16 [ LRES, 55950, 30056, ~p15 ] [ Backward Subsumption, 57004 ] % 4.26/4.42 (1,1) [56050,0]. true => p31 | p17 [ LRES, 55983, 30037, ~p16 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [56084,0]. true => ~p31 | ~p17 [ LRES, 56017, 30019, p16 ] [ Backward Subsumption, 57003 ] % 4.26/4.42 (1,1) [56117,0]. true => p31 | ~p18 [ LRES, 56050, 30003, p17 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [56151,0]. true => ~p31 | p18 [ LRES, 56084, 30008, ~p17 ] [ Backward Subsumption, 57002 ] % 4.26/4.42 (1,1) [56183,0]. true => p31 | p19 [ LRES, 56117, 29980, ~p18 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [56215,0]. true => ~p31 | ~p19 [ LRES, 56151, 29985, p18 ] [ Backward Subsumption, 57001 ] % 4.26/4.42 (1,1) [56247,0]. true => p31 | ~p20 [ LRES, 56183, 29950, p19 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [56280,0]. true => ~p31 | p20 [ LRES, 56215, 29968, ~p19 ] [ Backward Subsumption, 57000 ] % 4.26/4.42 (1,1) [56312,0]. true => p31 | p21 [ LRES, 56247, 29921, ~p20 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [56345,0]. true => ~p31 | ~p21 [ LRES, 56280, 29945, p20 ] [ Backward Subsumption, 56999 ] % 4.26/4.42 (1,1) [56376,0]. true => p31 | ~p22 [ LRES, 56312, 29902, p21 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [56408,0]. true => ~p31 | p22 [ LRES, 56345, 29914, ~p21 ] [ Backward Subsumption, 56998 ] % 4.26/4.42 (1,1) [56440,0]. true => p31 | p23 [ LRES, 56376, 29893, ~p22 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [56473,0]. true => ~p31 | ~p23 [ LRES, 56408, 29870, p22 ] [ Backward Subsumption, 56997 ] % 4.26/4.42 (1,1) [56505,0]. true => p31 | ~p24 [ LRES, 56440, 29852, p23 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [56537,0]. true => ~p31 | p24 [ LRES, 56473, 29851, ~p23 ] [ Backward Subsumption, 56996 ] % 4.26/4.42 (1,1) [56568,0]. true => p31 | p25 [ LRES, 56505, 29834, ~p24 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [56601,0]. true => ~p31 | ~p25 [ LRES, 56537, 29813, p24 ] [ Backward Subsumption, 56995 ] % 4.26/4.42 (1,1) [56633,0]. true => p31 | ~p26 [ LRES, 56568, 29783, p25 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.42 (1,1) [56666,0]. true => ~p31 | p26 [ LRES, 56601, 29804, ~p25 ] [ Backward Subsumption, 56994 ] % 4.26/4.49 (1,1) [56698,0]. true => p31 | p27 [ LRES, 56633, 29761, ~p26 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.49 (1,1) [56731,0]. true => ~p31 | ~p27 [ LRES, 56666, 29762, p26 ] [ Backward Subsumption, 56993 ] % 4.26/4.49 (1,1) [56763,0]. true => p31 | ~p28 [ LRES, 56698, 29736, p27 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.49 (1,1) [56796,0]. true => ~p31 | p28 [ LRES, 56731, 29724, ~p27 ] [ Backward Subsumption, 56992 ] % 4.26/4.49 (1,1) [56828,0]. true => p31 | p29 [ LRES, 56763, 29703, ~p28 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.49 (1,1) [56861,0]. true => ~p31 | ~p29 [ LRES, 56796, 29694, p28 ] [ Backward Subsumption, 56991 ] % 4.26/4.49 (1,1) [56893,0]. true => p31 | ~p30 [ LRES, 56828, 29676, p29 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.49 (1,1) [56926,0]. true => ~p31 | p30 [ LRES, 56861, 29650, ~p29 ] [ Backward Subsumption, 56990 ] % 4.26/4.49 (1,1) [56958,0]. true => p31 [ LRES, 56893, 29643, ~p30 ] [ Modal Level Pure Literal Elimination, p31 ] % 4.26/4.49 (1,1) [56990,0]. true => p30 [ Unit Resolution, 56958, 56926, p31 ] % 4.26/4.49 (1,1) [57019,0]. true => ~p30 [ Unit Resolution, 56958, 29615, p31 ] % 4.26/4.49 (1,1) [57050,0]. true => false [ Unit Resolution, 56990, 57019, p30 ] % 4.26/4.49 % SZS output end Refutation % 4.26/4.49 % KSP exiting %------------------------------------------------------------------------------