%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : PUZ015-2.006 : TPTP v9.2.1. Released v1.2.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n007.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 : Wed Jun 3 08:43:57 AM UTC 2026 % Result : Unsatisfiable 0.37s 0.58s % Output : Proof 0.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : PUZ015-2.006 : TPTP v9.2.1. Released v1.2.0. % 0.12/0.14 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.35 % Computer : n007.cluster.edu % 0.17/0.35 % Model : x86_64 x86_64 % 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.35 % Memory : 8042.1875MB % 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.35 % CPULimit : 300 % 0.17/0.35 % WCLimit : 300 % 0.17/0.35 % DateTime : Tue Jun 2 13:11:41 EDT 2026 % 0.17/0.35 % CPUTime : % 0.28/0.52 %----Proving TF0_NAR, FOF, or CNF % 0.28/0.53 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.37/0.58 % SZS status Unsatisfiable % 0.37/0.58 % SZS output start Proof % 0.37/0.60 ( % 0.37/0.60 (declare-const tptp.horizontal_6_4 Bool) % 0.37/0.60 (declare-const tptp.horizontal_3_2 Bool) % 0.37/0.60 (declare-const tptp.horizontal_3_1 Bool) % 0.37/0.60 (declare-const tptp.horizontal_2_5 Bool) % 0.37/0.60 (declare-const tptp.horizontal_6_3 Bool) % 0.37/0.60 (declare-const tptp.vertical_2_4 Bool) % 0.37/0.60 (declare-const tptp.horizontal_6_2 Bool) % 0.37/0.60 (declare-const tptp.horizontal_2_3 Bool) % 0.37/0.60 (declare-const tptp.vertical_2_3 Bool) % 0.37/0.60 (declare-const tptp.horizontal_2_2 Bool) % 0.37/0.60 (declare-const tptp.vertical_2_2 Bool) % 0.37/0.60 (declare-const tptp.horizontal_5_5 Bool) % 0.37/0.60 (declare-const tptp.horizontal_2_1 Bool) % 0.37/0.60 (declare-const tptp.vertical_2_1 Bool) % 0.37/0.60 (declare-const tptp.horizontal_5_4 Bool) % 0.37/0.60 (declare-const tptp.horizontal_1_1 Bool) % 0.37/0.60 (declare-const tptp.vertical_3_1 Bool) % 0.37/0.60 (declare-const tptp.vertical_2_5 Bool) % 0.37/0.60 (declare-const tptp.vertical_5_6 Bool) % 0.37/0.60 (declare-const tptp.horizontal_4_4 Bool) % 0.37/0.60 (declare-const tptp.horizontal_2_4 Bool) % 0.37/0.60 (declare-const tptp.vertical_1_1 Bool) % 0.37/0.60 (declare-const tptp.vertical_1_4 Bool) % 0.37/0.60 (declare-const tptp.vertical_5_1 Bool) % 0.37/0.60 (declare-const tptp.horizontal_6_5 Bool) % 0.37/0.60 (declare-const tptp.vertical_4_3 Bool) % 0.37/0.60 (declare-const tptp.vertical_3_3 Bool) % 0.37/0.60 (declare-const tptp.horizontal_1_5 Bool) % 0.37/0.60 (declare-const tptp.horizontal_5_2 Bool) % 0.37/0.60 (declare-const tptp.vertical_1_2 Bool) % 0.37/0.60 (declare-const tptp.horizontal_4_5 Bool) % 0.37/0.60 (declare-const tptp.vertical_2_6 Bool) % 0.37/0.60 (declare-const tptp.horizontal_1_2 Bool) % 0.37/0.60 (declare-const tptp.vertical_1_3 Bool) % 0.37/0.60 (declare-const tptp.vertical_4_6 Bool) % 0.37/0.60 (declare-const tptp.horizontal_1_3 Bool) % 0.37/0.60 (declare-const tptp.vertical_3_2 Bool) % 0.37/0.60 (declare-const tptp.horizontal_1_4 Bool) % 0.37/0.60 (declare-const tptp.horizontal_5_1 Bool) % 0.37/0.60 (declare-const tptp.vertical_1_5 Bool) % 0.37/0.60 (declare-const tptp.vertical_5_2 Bool) % 0.37/0.60 (declare-const tptp.vertical_1_6 Bool) % 0.37/0.60 (declare-const tptp.horizontal_5_3 Bool) % 0.37/0.60 (declare-const tptp.horizontal_3_3 Bool) % 0.37/0.60 (declare-const tptp.vertical_3_4 Bool) % 0.37/0.60 (declare-const tptp.horizontal_3_4 Bool) % 0.37/0.60 (declare-const tptp.vertical_3_5 Bool) % 0.37/0.60 (declare-const tptp.horizontal_3_5 Bool) % 0.37/0.60 (declare-const tptp.vertical_3_6 Bool) % 0.37/0.60 (declare-const tptp.vertical_4_1 Bool) % 0.37/0.60 (declare-const tptp.horizontal_4_1 Bool) % 0.37/0.60 (declare-const tptp.vertical_4_2 Bool) % 0.37/0.60 (declare-const tptp.horizontal_4_2 Bool) % 0.37/0.60 (declare-const tptp.horizontal_4_3 Bool) % 0.37/0.60 (declare-const tptp.vertical_4_4 Bool) % 0.37/0.60 (declare-const tptp.vertical_4_5 Bool) % 0.37/0.60 (declare-const tptp.vertical_5_3 Bool) % 0.37/0.60 (declare-const tptp.vertical_5_4 Bool) % 0.37/0.60 (declare-const tptp.vertical_5_5 Bool) % 0.37/0.60 (declare-const tptp.horizontal_6_1 Bool) % 0.37/0.60 (define @t1 () (not tptp.horizontal_1_1)) % 0.37/0.60 (define @t2 () (not tptp.vertical_1_1)) % 0.37/0.60 (define @t3 () (not tptp.horizontal_6_5)) % 0.37/0.60 (define @t4 () (not tptp.vertical_5_6)) % 0.37/0.60 (define @t5 () (not tptp.vertical_1_2)) % 0.37/0.60 (define @t6 () (not tptp.horizontal_1_2)) % 0.37/0.60 (define @t7 () (not tptp.vertical_1_3)) % 0.37/0.60 (define @t8 () (not tptp.horizontal_1_3)) % 0.37/0.60 (define @t9 () (not tptp.vertical_1_4)) % 0.37/0.60 (define @t10 () (not tptp.horizontal_1_4)) % 0.37/0.60 (define @t11 () (not tptp.vertical_1_5)) % 0.37/0.60 (define @t12 () (not tptp.horizontal_1_5)) % 0.37/0.60 (define @t13 () (not tptp.vertical_1_6)) % 0.37/0.60 (define @t14 () (not tptp.vertical_2_1)) % 0.37/0.60 (define @t15 () (not tptp.horizontal_2_1)) % 0.37/0.60 (define @t16 () (not tptp.vertical_2_2)) % 0.37/0.60 (define @t17 () (not tptp.horizontal_2_2)) % 0.37/0.60 (define @t18 () (not tptp.vertical_2_3)) % 0.37/0.60 (define @t19 () (not tptp.horizontal_2_3)) % 0.37/0.60 (define @t20 () (not tptp.vertical_2_4)) % 0.37/0.60 (define @t21 () (not tptp.horizontal_2_4)) % 0.37/0.60 (define @t22 () (not tptp.vertical_2_5)) % 0.37/0.60 (define @t23 () (not tptp.horizontal_2_5)) % 0.37/0.60 (define @t24 () (not tptp.vertical_2_6)) % 0.37/0.60 (define @t25 () (not tptp.vertical_3_1)) % 0.37/0.60 (define @t26 () (not tptp.horizontal_3_1)) % 0.37/0.60 (define @t27 () (not tptp.vertical_3_2)) % 0.37/0.60 (define @t28 () (not tptp.horizontal_3_2)) % 0.37/0.60 (define @t29 () (not tptp.vertical_3_3)) % 0.37/0.60 (define @t30 () (not tptp.horizontal_3_3)) % 0.37/0.60 (define @t31 () (not tptp.vertical_3_4)) % 0.37/0.60 (define @t32 () (not tptp.horizontal_3_4)) % 0.37/0.60 (define @t33 () (not tptp.vertical_3_5)) % 0.37/0.60 (define @t34 () (not tptp.horizontal_3_5)) % 0.37/0.60 (define @t35 () (not tptp.vertical_3_6)) % 0.37/0.60 (define @t36 () (not tptp.vertical_4_1)) % 0.37/0.60 (define @t37 () (not tptp.horizontal_4_1)) % 0.37/0.60 (define @t38 () (not tptp.vertical_4_2)) % 0.37/0.60 (define @t39 () (not tptp.horizontal_4_2)) % 0.37/0.60 (define @t40 () (not tptp.vertical_4_3)) % 0.37/0.60 (define @t41 () (not tptp.horizontal_4_3)) % 0.37/0.60 (define @t42 () (not tptp.vertical_4_4)) % 0.37/0.60 (define @t43 () (not tptp.horizontal_4_4)) % 0.37/0.60 (define @t44 () (not tptp.vertical_4_5)) % 0.37/0.60 (define @t45 () (not tptp.horizontal_4_5)) % 0.37/0.60 (define @t46 () (not tptp.vertical_4_6)) % 0.37/0.60 (define @t47 () (not tptp.vertical_5_1)) % 0.37/0.60 (define @t48 () (not tptp.horizontal_5_1)) % 0.37/0.60 (define @t49 () (not tptp.vertical_5_2)) % 0.37/0.60 (define @t50 () (not tptp.horizontal_5_2)) % 0.37/0.60 (define @t51 () (not tptp.vertical_5_3)) % 0.37/0.60 (define @t52 () (not tptp.horizontal_5_3)) % 0.37/0.60 (define @t53 () (not tptp.vertical_5_4)) % 0.37/0.60 (define @t54 () (not tptp.horizontal_5_4)) % 0.37/0.60 (define @t55 () (not tptp.vertical_5_5)) % 0.37/0.60 (define @t56 () (not tptp.horizontal_5_5)) % 0.37/0.60 (define @t57 () (not tptp.horizontal_6_1)) % 0.37/0.60 (define @t58 () (not tptp.horizontal_6_2)) % 0.37/0.60 (define @t59 () (not tptp.horizontal_6_3)) % 0.37/0.60 (define @t60 () (not tptp.horizontal_6_4)) % 0.37/0.60 (define @t61 () (@list true true)) % 0.37/0.60 (define @t62 () (@list false)) % 0.37/0.60 (define @t63 () (@list tptp.horizontal_1_2)) % 0.37/0.60 (define @t64 () (@list false true false true true)) % 0.37/0.60 (define @t65 () (@list tptp.vertical_4_3)) % 0.37/0.60 (define @t66 () (@list tptp.vertical_3_1)) % 0.37/0.60 (define @t67 () (@list tptp.horizontal_2_1)) % 0.37/0.60 (define @t68 () (@list tptp.vertical_3_6)) % 0.37/0.60 (define @t69 () (@list tptp.vertical_4_4)) % 0.37/0.60 (define @t70 () (@list tptp.horizontal_5_5)) % 0.37/0.60 (define @t71 () (@list true true true)) % 0.37/0.60 (define @t72 () (@list tptp.horizontal_3_2)) % 0.37/0.60 (assume @p1 @t1) % 0.37/0.60 (assume @p2 @t2) % 0.37/0.60 (assume @p3 @t3) % 0.37/0.60 (assume @p4 @t4) % 0.37/0.60 (assume @p5 (or tptp.horizontal_1_2 tptp.vertical_1_2 tptp.horizontal_1_1)) % 0.37/0.60 (assume @p6 (or tptp.horizontal_1_3 tptp.vertical_1_3 tptp.horizontal_1_2)) % 0.37/0.60 (assume @p7 (or tptp.horizontal_1_4 tptp.vertical_1_4 tptp.horizontal_1_3)) % 0.37/0.60 (assume @p8 (or tptp.horizontal_1_5 tptp.vertical_1_5 tptp.horizontal_1_4)) % 0.37/0.60 (assume @p9 (or tptp.vertical_1_6 tptp.horizontal_1_5)) % 0.37/0.60 (assume @p10 (or tptp.horizontal_2_1 tptp.vertical_2_1 tptp.vertical_1_1)) % 0.37/0.60 (assume @p11 (or tptp.horizontal_2_2 tptp.vertical_2_2 tptp.horizontal_2_1 tptp.vertical_1_2)) % 0.37/0.60 (assume @p12 (or tptp.horizontal_2_3 tptp.vertical_2_3 tptp.horizontal_2_2 tptp.vertical_1_3)) % 0.37/0.60 (assume @p13 (or tptp.horizontal_2_4 tptp.vertical_2_4 tptp.horizontal_2_3 tptp.vertical_1_4)) % 0.37/0.60 (assume @p14 (or tptp.horizontal_2_5 tptp.vertical_2_5 tptp.horizontal_2_4 tptp.vertical_1_5)) % 0.37/0.60 (assume @p15 (or tptp.vertical_2_6 tptp.horizontal_2_5 tptp.vertical_1_6)) % 0.37/0.60 (assume @p16 (or tptp.horizontal_3_1 tptp.vertical_3_1 tptp.vertical_2_1)) % 0.37/0.60 (assume @p17 (or tptp.horizontal_3_2 tptp.vertical_3_2 tptp.horizontal_3_1 tptp.vertical_2_2)) % 0.37/0.60 (assume @p18 (or tptp.horizontal_3_3 tptp.vertical_3_3 tptp.horizontal_3_2 tptp.vertical_2_3)) % 0.37/0.60 (assume @p19 (or tptp.horizontal_3_4 tptp.vertical_3_4 tptp.horizontal_3_3 tptp.vertical_2_4)) % 0.37/0.60 (assume @p20 (or tptp.horizontal_3_5 tptp.vertical_3_5 tptp.horizontal_3_4 tptp.vertical_2_5)) % 0.37/0.60 (assume @p21 (or tptp.vertical_3_6 tptp.horizontal_3_5 tptp.vertical_2_6)) % 0.37/0.60 (assume @p22 (or tptp.horizontal_4_1 tptp.vertical_4_1 tptp.vertical_3_1)) % 0.37/0.60 (assume @p23 (or tptp.horizontal_4_2 tptp.vertical_4_2 tptp.horizontal_4_1 tptp.vertical_3_2)) % 0.37/0.60 (assume @p24 (or tptp.horizontal_4_3 tptp.vertical_4_3 tptp.horizontal_4_2 tptp.vertical_3_3)) % 0.37/0.60 (assume @p25 (or tptp.horizontal_4_4 tptp.vertical_4_4 tptp.horizontal_4_3 tptp.vertical_3_4)) % 0.37/0.60 (assume @p26 (or tptp.horizontal_4_5 tptp.vertical_4_5 tptp.horizontal_4_4 tptp.vertical_3_5)) % 0.37/0.60 (assume @p27 (or tptp.vertical_4_6 tptp.horizontal_4_5 tptp.vertical_3_6)) % 0.37/0.60 (assume @p28 (or tptp.horizontal_5_1 tptp.vertical_5_1 tptp.vertical_4_1)) % 0.37/0.60 (assume @p29 (or tptp.horizontal_5_2 tptp.vertical_5_2 tptp.horizontal_5_1 tptp.vertical_4_2)) % 0.37/0.60 (assume @p30 (or tptp.horizontal_5_3 tptp.vertical_5_3 tptp.horizontal_5_2 tptp.vertical_4_3)) % 0.37/0.60 (assume @p31 (or tptp.horizontal_5_4 tptp.vertical_5_4 tptp.horizontal_5_3 tptp.vertical_4_4)) % 0.37/0.60 (assume @p32 (or tptp.horizontal_5_5 tptp.vertical_5_5 tptp.horizontal_5_4 tptp.vertical_4_5)) % 0.37/0.60 (assume @p33 (or tptp.vertical_5_6 tptp.horizontal_5_5 tptp.vertical_4_6)) % 0.37/0.60 (assume @p34 (or tptp.horizontal_6_1 tptp.vertical_5_1)) % 0.37/0.60 (assume @p35 (or tptp.horizontal_6_2 tptp.horizontal_6_1 tptp.vertical_5_2)) % 0.37/0.60 (assume @p36 (or tptp.horizontal_6_3 tptp.horizontal_6_2 tptp.vertical_5_3)) % 0.37/0.60 (assume @p37 (or tptp.horizontal_6_4 tptp.horizontal_6_3 tptp.vertical_5_4)) % 0.37/0.60 (assume @p38 (or tptp.horizontal_6_5 tptp.horizontal_6_4 tptp.vertical_5_5)) % 0.37/0.60 (assume @p39 (or @t6 @t5)) % 0.37/0.60 (assume @p40 (or @t6 @t1)) % 0.37/0.60 (assume @p41 (or @t5 @t1)) % 0.37/0.60 (assume @p42 (or @t8 @t7)) % 0.37/0.60 (assume @p43 (or @t8 @t6)) % 0.37/0.60 (assume @p44 (or @t7 @t6)) % 0.37/0.60 (assume @p45 (or @t10 @t9)) % 0.37/0.60 (assume @p46 (or @t10 @t8)) % 0.37/0.60 (assume @p47 (or @t9 @t8)) % 0.37/0.60 (assume @p48 (or @t12 @t11)) % 0.37/0.60 (assume @p49 (or @t12 @t10)) % 0.37/0.60 (assume @p50 (or @t11 @t10)) % 0.37/0.60 (assume @p51 (or @t13 @t12)) % 0.37/0.60 (assume @p52 (or @t15 @t14)) % 0.37/0.60 (assume @p53 (or @t15 @t2)) % 0.37/0.60 (assume @p54 (or @t14 @t2)) % 0.37/0.60 (assume @p55 (or @t17 @t16)) % 0.37/0.60 (assume @p56 (or @t17 @t15)) % 0.37/0.60 (assume @p57 (or @t17 @t5)) % 0.37/0.60 (assume @p58 (or @t16 @t15)) % 0.37/0.60 (assume @p59 (or @t16 @t5)) % 0.37/0.60 (assume @p60 (or @t15 @t5)) % 0.37/0.60 (assume @p61 (or @t19 @t18)) % 0.37/0.60 (assume @p62 (or @t19 @t17)) % 0.37/0.60 (assume @p63 (or @t19 @t7)) % 0.37/0.60 (assume @p64 (or @t18 @t17)) % 0.37/0.60 (assume @p65 (or @t18 @t7)) % 0.37/0.60 (assume @p66 (or @t17 @t7)) % 0.37/0.60 (assume @p67 (or @t21 @t20)) % 0.37/0.60 (assume @p68 (or @t21 @t19)) % 0.37/0.60 (assume @p69 (or @t21 @t9)) % 0.37/0.60 (assume @p70 (or @t20 @t19)) % 0.37/0.60 (assume @p71 (or @t20 @t9)) % 0.37/0.60 (assume @p72 (or @t19 @t9)) % 0.37/0.60 (assume @p73 (or @t23 @t22)) % 0.37/0.60 (assume @p74 (or @t23 @t21)) % 0.37/0.60 (assume @p75 (or @t23 @t11)) % 0.37/0.60 (assume @p76 (or @t22 @t21)) % 0.37/0.60 (assume @p77 (or @t22 @t11)) % 0.37/0.60 (assume @p78 (or @t21 @t11)) % 0.37/0.60 (assume @p79 (or @t24 @t23)) % 0.37/0.60 (assume @p80 (or @t24 @t13)) % 0.37/0.60 (assume @p81 (or @t23 @t13)) % 0.37/0.60 (assume @p82 (or @t26 @t25)) % 0.37/0.60 (assume @p83 (or @t26 @t14)) % 0.37/0.60 (assume @p84 (or @t25 @t14)) % 0.37/0.60 (assume @p85 (or @t28 @t27)) % 0.37/0.60 (assume @p86 (or @t28 @t26)) % 0.37/0.60 (assume @p87 (or @t28 @t16)) % 0.37/0.60 (assume @p88 (or @t27 @t26)) % 0.37/0.60 (assume @p89 (or @t27 @t16)) % 0.37/0.60 (assume @p90 (or @t26 @t16)) % 0.37/0.60 (assume @p91 (or @t30 @t29)) % 0.37/0.60 (assume @p92 (or @t30 @t28)) % 0.37/0.60 (assume @p93 (or @t30 @t18)) % 0.37/0.60 (assume @p94 (or @t29 @t28)) % 0.37/0.60 (assume @p95 (or @t29 @t18)) % 0.37/0.60 (assume @p96 (or @t28 @t18)) % 0.37/0.60 (assume @p97 (or @t32 @t31)) % 0.37/0.60 (assume @p98 (or @t32 @t30)) % 0.37/0.60 (assume @p99 (or @t32 @t20)) % 0.37/0.60 (assume @p100 (or @t31 @t30)) % 0.37/0.60 (assume @p101 (or @t31 @t20)) % 0.37/0.60 (assume @p102 (or @t30 @t20)) % 0.37/0.60 (assume @p103 (or @t34 @t33)) % 0.37/0.60 (assume @p104 (or @t34 @t32)) % 0.37/0.60 (assume @p105 (or @t34 @t22)) % 0.37/0.60 (assume @p106 (or @t33 @t32)) % 0.37/0.60 (assume @p107 (or @t33 @t22)) % 0.37/0.60 (assume @p108 (or @t32 @t22)) % 0.37/0.60 (assume @p109 (or @t35 @t34)) % 0.37/0.60 (assume @p110 (or @t35 @t24)) % 0.37/0.60 (assume @p111 (or @t34 @t24)) % 0.37/0.60 (assume @p112 (or @t37 @t36)) % 0.37/0.60 (assume @p113 (or @t37 @t25)) % 0.37/0.60 (assume @p114 (or @t36 @t25)) % 0.37/0.60 (assume @p115 (or @t39 @t38)) % 0.37/0.60 (assume @p116 (or @t39 @t37)) % 0.37/0.60 (assume @p117 (or @t39 @t27)) % 0.37/0.60 (assume @p118 (or @t38 @t37)) % 0.37/0.60 (assume @p119 (or @t38 @t27)) % 0.37/0.60 (assume @p120 (or @t37 @t27)) % 0.37/0.60 (assume @p121 (or @t41 @t40)) % 0.37/0.60 (assume @p122 (or @t41 @t39)) % 0.37/0.60 (assume @p123 (or @t41 @t29)) % 0.37/0.60 (assume @p124 (or @t40 @t39)) % 0.37/0.60 (assume @p125 (or @t40 @t29)) % 0.37/0.60 (assume @p126 (or @t39 @t29)) % 0.37/0.60 (assume @p127 (or @t43 @t42)) % 0.37/0.60 (assume @p128 (or @t43 @t41)) % 0.37/0.60 (assume @p129 (or @t43 @t31)) % 0.37/0.60 (assume @p130 (or @t42 @t41)) % 0.37/0.60 (assume @p131 (or @t42 @t31)) % 0.37/0.60 (assume @p132 (or @t41 @t31)) % 0.37/0.60 (assume @p133 (or @t45 @t44)) % 0.37/0.60 (assume @p134 (or @t45 @t43)) % 0.37/0.60 (assume @p135 (or @t45 @t33)) % 0.37/0.60 (assume @p136 (or @t44 @t43)) % 0.37/0.60 (assume @p137 (or @t44 @t33)) % 0.37/0.60 (assume @p138 (or @t43 @t33)) % 0.37/0.60 (assume @p139 (or @t46 @t45)) % 0.37/0.60 (assume @p140 (or @t46 @t35)) % 0.37/0.60 (assume @p141 (or @t45 @t35)) % 0.37/0.60 (assume @p142 (or @t48 @t47)) % 0.37/0.60 (assume @p143 (or @t48 @t36)) % 0.37/0.60 (assume @p144 (or @t47 @t36)) % 0.37/0.60 (assume @p145 (or @t50 @t49)) % 0.37/0.60 (assume @p146 (or @t50 @t48)) % 0.37/0.60 (assume @p147 (or @t50 @t38)) % 0.37/0.60 (assume @p148 (or @t49 @t48)) % 0.37/0.60 (assume @p149 (or @t49 @t38)) % 0.37/0.60 (assume @p150 (or @t48 @t38)) % 0.37/0.60 (assume @p151 (or @t52 @t51)) % 0.37/0.60 (assume @p152 (or @t52 @t50)) % 0.37/0.60 (assume @p153 (or @t52 @t40)) % 0.37/0.60 (assume @p154 (or @t51 @t50)) % 0.37/0.60 (assume @p155 (or @t51 @t40)) % 0.37/0.60 (assume @p156 (or @t50 @t40)) % 0.37/0.60 (assume @p157 (or @t54 @t53)) % 0.37/0.60 (assume @p158 (or @t54 @t52)) % 0.37/0.60 (assume @p159 (or @t54 @t42)) % 0.37/0.60 (assume @p160 (or @t53 @t52)) % 0.37/0.60 (assume @p161 (or @t53 @t42)) % 0.37/0.60 (assume @p162 (or @t52 @t42)) % 0.37/0.60 (assume @p163 (or @t56 @t55)) % 0.37/0.60 (assume @p164 (or @t56 @t54)) % 0.37/0.60 (assume @p165 (or @t56 @t44)) % 0.37/0.60 (assume @p166 (or @t55 @t54)) % 0.37/0.60 (assume @p167 (or @t55 @t44)) % 0.37/0.60 (assume @p168 (or @t54 @t44)) % 0.37/0.60 (assume @p169 (or @t4 @t56)) % 0.37/0.60 (assume @p170 (or @t4 @t46)) % 0.37/0.60 (assume @p171 (or @t56 @t46)) % 0.37/0.60 (assume @p172 (or @t57 @t47)) % 0.37/0.60 (assume @p173 (or @t58 @t57)) % 0.37/0.60 (assume @p174 (or @t58 @t49)) % 0.37/0.60 (assume @p175 (or @t57 @t49)) % 0.37/0.60 (assume @p176 (or @t59 @t58)) % 0.37/0.60 (assume @p177 (or @t59 @t51)) % 0.37/0.60 (assume @p178 (or @t58 @t51)) % 0.37/0.60 (assume @p179 (or @t60 @t59)) % 0.37/0.60 (assume @p180 (or @t60 @t53)) % 0.37/0.60 (assume @p181 (or @t59 @t53)) % 0.37/0.60 (assume @p182 (or @t3 @t60)) % 0.37/0.60 (assume @p183 (or @t3 @t55)) % 0.37/0.60 (assume @p184 (or @t60 @t55)) % 0.37/0.60 (step @p185 :rule reordering :premises (@p107) :args ((or @t22 @t33))) % 0.37/0.60 (step @p186 :rule reordering :premises (@p21) :args ((or tptp.vertical_2_6 tptp.horizontal_3_5 tptp.vertical_3_6))) % 0.37/0.60 (step @p187 :rule reordering :premises (@p79) :args ((or @t23 @t24))) % 0.37/0.60 (step @p188 :rule reordering :premises (@p80) :args ((or @t13 @t24))) % 0.37/0.60 (step @p189 :rule reordering :premises (@p9) :args ((or tptp.horizontal_1_5 tptp.vertical_1_6))) % 0.37/0.60 (step @p190 :rule reordering :premises (@p49) :args ((or @t10 @t12))) % 0.37/0.60 (step @p191 :rule reordering :premises (@p14) :args ((or tptp.vertical_1_5 tptp.horizontal_2_4 tptp.horizontal_2_5 tptp.vertical_2_5))) % 0.37/0.60 (step @p192 :rule reordering :premises (@p57) :args ((or @t5 @t17))) % 0.37/0.60 (step @p193 :rule reordering :premises (@p59) :args ((or @t5 @t16))) % 0.37/0.60 (step @p194 :rule reordering :premises (@p60) :args ((or @t5 @t15))) % 0.37/0.60 (step @p195 :rule reordering :premises (@p10) :args ((or tptp.vertical_1_1 tptp.horizontal_2_1 tptp.vertical_2_1))) % 0.37/0.60 (step @p196 :rule reordering :premises (@p83) :args ((or @t14 @t26))) % 0.37/0.60 (step @p197 :rule reordering :premises (@p84) :args ((or @t14 @t25))) % 0.37/0.60 (step @p198 :rule reordering :premises (@p166) :args ((or @t54 @t55))) % 0.37/0.60 (step @p199 :rule reordering :premises (@p167) :args ((or @t44 @t55))) % 0.37/0.60 (step @p200 :rule reordering :premises (@p33) :args ((or tptp.vertical_5_6 tptp.vertical_4_6 tptp.horizontal_5_5))) % 0.37/0.60 (step @p201 :rule reordering :premises (@p139) :args ((or @t45 @t46))) % 0.37/0.60 (step @p202 :rule reordering :premises (@p140) :args ((or @t35 @t46))) % 0.37/0.60 (step @p203 :rule reordering :premises (@p154) :args ((or @t50 @t51))) % 0.37/0.60 (step @p204 :rule reordering :premises (@p155) :args ((or @t40 @t51))) % 0.37/0.60 (step @p205 :rule reordering :premises (@p116) :args ((or @t37 @t39))) % 0.37/0.60 (step @p206 :rule reordering :premises (@p120) :args ((or @t27 @t37))) % 0.37/0.60 (step @p207 :rule reordering :premises (@p17) :args ((or tptp.vertical_2_2 tptp.horizontal_3_1 tptp.horizontal_3_2 tptp.vertical_3_2))) % 0.37/0.60 (step @p208 :rule reordering :premises (@p92) :args ((or @t28 @t30))) % 0.37/0.60 (step @p209 :rule reordering :premises (@p94) :args ((or @t28 @t29))) % 0.37/0.60 (step @p210 :rule reordering :premises (@p24) :args ((or tptp.vertical_3_3 tptp.horizontal_4_2 tptp.horizontal_4_3 tptp.vertical_4_3))) % 0.37/0.60 (step @p211 :rule reordering :premises (@p128) :args ((or @t41 @t43))) % 0.37/0.60 (step @p212 :rule reordering :premises (@p132) :args ((or @t31 @t41))) % 0.37/0.60 (step @p213 :rule reordering :premises (@p26) :args ((or tptp.vertical_3_5 tptp.horizontal_4_4 tptp.horizontal_4_5 tptp.vertical_4_5))) % 0.37/0.60 (step @p214 :rule reordering :premises (@p106) :args ((or @t32 @t33))) % 0.37/0.60 (step @p215 :rule reordering :premises (@p19) :args ((or tptp.vertical_2_4 tptp.horizontal_3_3 tptp.horizontal_3_4 tptp.vertical_3_4))) % 0.37/0.60 (step @p216 :rule chain_m_resolution :premises (@p48 @p191 @p189 @p67 @p188 @p187 @p215 @p186 @p185 @p214 @p103 @p213 @p212 @p211 @p210 @p209 @p208 @p207 @p206 @p205) :args ((or tptp.vertical_2_2 tptp.horizontal_3_1 tptp.vertical_3_6 tptp.vertical_4_3 tptp.horizontal_4_5 tptp.vertical_4_5 @t37) (@list false false true true true false false true true true false true true false true true false true true) (@list tptp.vertical_1_5 tptp.horizontal_1_5 tptp.horizontal_2_4 tptp.vertical_1_6 tptp.horizontal_2_5 tptp.vertical_2_4 tptp.vertical_2_6 tptp.vertical_2_5 tptp.horizontal_3_4 tptp.horizontal_3_5 tptp.vertical_3_5 tptp.vertical_3_4 tptp.horizontal_4_4 tptp.horizontal_4_3 tptp.vertical_3_3 tptp.horizontal_3_3 tptp.horizontal_3_2 tptp.vertical_3_2 tptp.horizontal_4_2))) % 0.37/0.60 (step @p217 :rule reordering :premises (@p22) :args ((or tptp.vertical_3_1 tptp.horizontal_4_1 tptp.vertical_4_1))) % 0.37/0.60 (step @p218 :rule reordering :premises (@p143) :args ((or @t36 @t48))) % 0.37/0.60 (step @p219 :rule reordering :premises (@p144) :args ((or @t36 @t47))) % 0.37/0.60 (step @p220 :rule reordering :premises (@p34) :args ((or tptp.vertical_5_1 tptp.horizontal_6_1))) % 0.37/0.60 (step @p221 :rule reordering :premises (@p175) :args ((or @t49 @t57))) % 0.37/0.60 (step @p222 :rule reordering :premises (@p29) :args ((or tptp.vertical_4_2 tptp.horizontal_5_1 tptp.horizontal_5_2 tptp.vertical_5_2))) % 0.37/0.60 (step @p223 :rule reordering :premises (@p119) :args ((or @t27 @t38))) % 0.37/0.60 (step @p224 :rule chain_m_resolution :premises (@p48 @p191 @p189 @p67 @p188 @p187 @p215 @p186 @p185 @p214 @p103 @p213 @p212 @p211 @p210 @p209 @p208 @p207 @p223 @p115 @p222 @p221 @p220 @p219 @p218 @p217 @p216 @p204 @p203) :args ((or tptp.vertical_2_2 tptp.horizontal_3_1 tptp.vertical_3_1 tptp.vertical_3_6 tptp.horizontal_4_5 tptp.vertical_4_5 @t51) (@list false false true true true false false true true true false true true false true true false true true false true false true true false true true true) (@list tptp.vertical_1_5 tptp.horizontal_1_5 tptp.horizontal_2_4 tptp.vertical_1_6 tptp.horizontal_2_5 tptp.vertical_2_4 tptp.vertical_2_6 tptp.vertical_2_5 tptp.horizontal_3_4 tptp.horizontal_3_5 tptp.vertical_3_5 tptp.vertical_3_4 tptp.horizontal_4_4 tptp.horizontal_4_3 tptp.vertical_3_3 tptp.horizontal_3_3 tptp.horizontal_3_2 tptp.vertical_3_2 tptp.horizontal_4_2 tptp.vertical_4_2 tptp.vertical_5_2 tptp.horizontal_6_1 tptp.vertical_5_1 tptp.horizontal_5_1 tptp.vertical_4_1 tptp.horizontal_4_1 tptp.vertical_4_3 tptp.horizontal_5_2))) % 0.37/0.60 (step @p225 :rule reordering :premises (@p153) :args ((or @t40 @t52))) % 0.37/0.60 (step @p226 :rule reordering :premises (@p156) :args ((or @t40 @t50))) % 0.37/0.60 (step @p227 :rule reordering :premises (@p31) :args ((or tptp.vertical_4_4 tptp.horizontal_5_3 tptp.horizontal_5_4 tptp.vertical_5_4))) % 0.37/0.60 (step @p228 :rule reordering :premises (@p181) :args ((or @t53 @t59))) % 0.37/0.60 (step @p229 :rule reordering :premises (@p36) :args ((or tptp.vertical_5_3 tptp.horizontal_6_2 tptp.horizontal_6_3))) % 0.37/0.60 (step @p230 :rule reordering :premises (@p173) :args ((or @t57 @t58))) % 0.37/0.60 (step @p231 :rule reordering :premises (@p174) :args ((or @t49 @t58))) % 0.37/0.60 (step @p232 :rule reordering :premises (@p118) :args ((or @t37 @t38))) % 0.37/0.60 (step @p233 :rule chain_m_resolution :premises (@p232 @p217 @p222 @p219 @p142 @p220 @p231 @p230 @p229 @p228 @p227 @p226 @p225) :args ((or tptp.vertical_3_1 tptp.vertical_4_4 tptp.vertical_5_3 tptp.horizontal_5_4 @t40) (@list false false true true false true true false true false true true) (@list tptp.horizontal_4_1 tptp.vertical_4_2 tptp.vertical_4_1 tptp.horizontal_5_1 tptp.vertical_5_1 tptp.vertical_5_2 tptp.horizontal_6_1 tptp.horizontal_6_2 tptp.horizontal_6_3 tptp.vertical_5_4 tptp.horizontal_5_2 tptp.horizontal_5_3))) % 0.37/0.60 (step @p234 :rule reordering :premises (@p152) :args ((or @t50 @t52))) % 0.37/0.60 (step @p235 :rule chain_m_resolution :premises (@p209 @p207 @p210 @p223 @p115 @p222 @p234 @p227 @p228 @p229 @p221 @p230 @p220 @p219 @p218 @p217 @p216 @p233 @p211 @p127 @p224) :args ((or tptp.vertical_2_2 tptp.horizontal_3_1 tptp.vertical_3_1 tptp.vertical_3_6 tptp.horizontal_4_5 tptp.vertical_4_5 tptp.horizontal_5_4 @t43) (@list false false true true false true false true false true true false true true false true true true true true) (@list tptp.horizontal_3_2 tptp.vertical_3_3 tptp.vertical_3_2 tptp.horizontal_4_2 tptp.vertical_4_2 tptp.horizontal_5_2 tptp.horizontal_5_3 tptp.vertical_5_4 tptp.horizontal_6_3 tptp.vertical_5_2 tptp.horizontal_6_2 tptp.horizontal_6_1 tptp.vertical_5_1 tptp.horizontal_5_1 tptp.vertical_4_1 tptp.horizontal_4_1 tptp.vertical_4_3 tptp.horizontal_4_3 tptp.vertical_4_4 tptp.vertical_5_3))) % 0.37/0.60 (step @p236 :rule reordering :premises (@p68) :args ((or @t19 @t21))) % 0.37/0.60 (step @p237 :rule reordering :premises (@p69) :args ((or @t9 @t21))) % 0.37/0.60 (step @p238 :rule reordering :premises (@p7) :args ((or tptp.horizontal_1_3 tptp.horizontal_1_4 tptp.vertical_1_4))) % 0.37/0.60 (step @p239 :rule reordering :premises (@p12) :args ((or tptp.vertical_1_3 tptp.horizontal_2_2 tptp.horizontal_2_3 tptp.vertical_2_3))) % 0.37/0.60 (step @p240 :rule reordering :premises (@p93) :args ((or @t18 @t30))) % 0.37/0.60 (step @p241 :rule reordering :premises (@p95) :args ((or @t18 @t29))) % 0.37/0.60 (step @p242 :rule reordering :premises (@p96) :args ((or @t18 @t28))) % 0.37/0.60 (step @p243 :rule reordering :premises (@p117) :args ((or @t27 @t39))) % 0.37/0.60 (step @p244 :rule chain_m_resolution :premises (@p221 @p220 @p222 @p219 @p218 @p226 @p217 @p210 @p206 @p223 @p243 @p207 @p242 @p241) :args ((or tptp.vertical_2_2 tptp.horizontal_3_1 tptp.vertical_3_1 tptp.horizontal_4_3 @t18) (@list false false true true true false false true true true false true true) (@list tptp.horizontal_6_1 tptp.vertical_5_2 tptp.vertical_5_1 tptp.horizontal_5_1 tptp.horizontal_5_2 tptp.vertical_4_1 tptp.vertical_4_3 tptp.horizontal_4_1 tptp.vertical_4_2 tptp.horizontal_4_2 tptp.vertical_3_2 tptp.horizontal_3_2 tptp.vertical_3_3))) % 0.37/0.60 (step @p245 :rule chain_m_resolution :premises (@p212 @p215 @p244 @p240 @p239 @p42 @p238 @p237 @p236 @p67 @p191 @p190 @p48 @p189 @p188 @p187 @p186 @p185 @p214 @p103 @p213 @p235 @p202 @p201 @p200 @p4 @p199 @p198 @p163) :args ((or tptp.horizontal_2_2 tptp.vertical_2_2 tptp.horizontal_3_1 tptp.vertical_3_1 @t55) (@list false false true false true false true true true false true true false true true false true true true false true true true false true true true true) (@list tptp.vertical_3_4 tptp.horizontal_4_3 tptp.horizontal_3_3 tptp.vertical_2_3 tptp.vertical_1_3 tptp.horizontal_1_3 tptp.vertical_1_4 tptp.horizontal_2_3 tptp.vertical_2_4 tptp.horizontal_2_4 tptp.horizontal_1_4 tptp.vertical_1_5 tptp.horizontal_1_5 tptp.vertical_1_6 tptp.horizontal_2_5 tptp.vertical_2_6 tptp.vertical_2_5 tptp.horizontal_3_4 tptp.horizontal_3_5 tptp.vertical_3_5 tptp.horizontal_4_4 tptp.vertical_3_6 tptp.horizontal_4_5 tptp.vertical_4_6 tptp.vertical_5_6 tptp.vertical_4_5 tptp.horizontal_5_4 tptp.horizontal_5_5))) % 0.37/0.60 (step @p246 :rule reordering :premises (@p38) :args ((or tptp.horizontal_6_5 tptp.vertical_5_5 tptp.horizontal_6_4))) % 0.37/0.60 (step @p247 :rule reordering :premises (@p179) :args ((or @t59 @t60))) % 0.37/0.60 (step @p248 :rule reordering :premises (@p180) :args ((or @t53 @t60))) % 0.37/0.60 (step @p249 :rule reordering :premises (@p130) :args ((or @t41 @t42))) % 0.37/0.60 (step @p250 :rule reordering :premises (@p164) :args ((or @t54 @t56))) % 0.37/0.60 (step @p251 :rule reordering :premises (@p168) :args ((or @t44 @t54))) % 0.37/0.60 (step @p252 :rule chain_m_resolution :premises (@p224 @p202 @p201 @p200 @p4 @p251 @p250 @p227 @p151) :args ((or tptp.vertical_2_2 tptp.horizontal_3_1 tptp.vertical_3_1 tptp.vertical_4_4 tptp.vertical_5_4 @t51) (@list true true false true true true false true) (@list tptp.vertical_3_6 tptp.horizontal_4_5 tptp.vertical_4_6 tptp.vertical_5_6 tptp.vertical_4_5 tptp.horizontal_5_5 tptp.horizontal_5_4 tptp.horizontal_5_3))) % 0.37/0.60 (step @p253 :rule chain_m_resolution :premises (@p216 @p202 @p201 @p200 @p4 @p251 @p250 @p227 @p234 @p222 @p232 @p217 @p219 @p142 @p220 @p231 @p230 @p229 @p252 @p249 @p121) :args ((or tptp.vertical_2_2 tptp.horizontal_3_1 tptp.vertical_3_1 tptp.vertical_5_4 tptp.horizontal_6_3 @t41) (@list true true false true true true false true false true false true true false true true false true true true) (@list tptp.vertical_3_6 tptp.horizontal_4_5 tptp.vertical_4_6 tptp.vertical_5_6 tptp.vertical_4_5 tptp.horizontal_5_5 tptp.horizontal_5_4 tptp.horizontal_5_3 tptp.horizontal_5_2 tptp.vertical_4_2 tptp.horizontal_4_1 tptp.vertical_4_1 tptp.horizontal_5_1 tptp.vertical_5_1 tptp.vertical_5_2 tptp.horizontal_6_1 tptp.horizontal_6_2 tptp.vertical_5_3 tptp.vertical_4_4 tptp.vertical_4_3))) % 0.37/0.60 (step @p254 :rule chain_m_resolution :premises (@p232 @p217 @p222 @p219 @p142 @p220 @p231 @p230 @p229 @p226 @p204) :args ((or tptp.vertical_3_1 tptp.horizontal_6_3 @t40) (@list false false true true false true true false true true) (@list tptp.horizontal_4_1 tptp.vertical_4_2 tptp.vertical_4_1 tptp.horizontal_5_1 tptp.vertical_5_1 tptp.vertical_5_2 tptp.horizontal_6_1 tptp.horizontal_6_2 tptp.horizontal_5_2 tptp.vertical_5_3))) % 0.37/0.60 (step @p255 :rule chain_m_resolution :premises (@p209 @p207 @p210 @p206 @p205) :args ((or tptp.vertical_2_2 tptp.horizontal_3_1 tptp.horizontal_4_3 tptp.vertical_4_3 @t37) (@list false false true true) (@list tptp.horizontal_3_2 tptp.vertical_3_3 tptp.vertical_3_2 tptp.horizontal_4_2))) % 0.37/0.60 (step @p256 :rule chain_m_resolution :premises (@p209 @p207 @p210 @p223 @p115 @p222 @p203 @p229 @p221 @p230 @p220 @p219 @p218 @p217 @p255 @p254 @p253 @p248 @p247 @p246 @p3 @p245 @p197 @p196 @p195 @p2 @p194 @p193 @p192) :args (@t5 (@list false false true true false true false true true false true true false true true true true true false true true true true false true true true true) (@list tptp.horizontal_3_2 tptp.vertical_3_3 tptp.vertical_3_2 tptp.horizontal_4_2 tptp.vertical_4_2 tptp.horizontal_5_2 tptp.vertical_5_3 tptp.vertical_5_2 tptp.horizontal_6_2 tptp.horizontal_6_1 tptp.vertical_5_1 tptp.horizontal_5_1 tptp.vertical_4_1 tptp.horizontal_4_1 tptp.vertical_4_3 tptp.horizontal_4_3 tptp.vertical_5_4 tptp.horizontal_6_3 tptp.horizontal_6_4 tptp.horizontal_6_5 tptp.vertical_5_5 tptp.vertical_3_1 tptp.horizontal_3_1 tptp.vertical_2_1 tptp.vertical_1_1 tptp.horizontal_2_1 tptp.vertical_2_2 tptp.horizontal_2_2))) % 0.37/0.60 (step @p257 :rule reordering :premises (@p5) :args ((or tptp.horizontal_1_1 tptp.horizontal_1_2 tptp.vertical_1_2))) % 0.37/0.60 (step @p258 :rule chain_m_resolution :premises (@p257 @p1 @p256) :args (tptp.horizontal_1_2 @t61 (@list tptp.horizontal_1_1 tptp.vertical_1_2))) % 0.37/0.60 (step @p259 :rule reordering :premises (@p43) :args ((or @t6 @t8))) % 0.37/0.60 (step @p260 :rule chain_m_resolution :premises (@p259 @p258) :args (@t8 @t62 @t63)) % 0.37/0.60 (step @p261 :rule chain_m_resolution :premises (@p237 @p238 @p260 @p191 @p190 @p48 @p189 @p188 @p187 @p186 @p185 @p103) :args ((or tptp.vertical_3_6 @t33) (@list false true false true true false true true false true true) (@list tptp.vertical_1_4 tptp.horizontal_1_3 tptp.horizontal_2_4 tptp.horizontal_1_4 tptp.vertical_1_5 tptp.horizontal_1_5 tptp.vertical_1_6 tptp.horizontal_2_5 tptp.vertical_2_6 tptp.vertical_2_5 tptp.horizontal_3_5))) % 0.37/0.60 (step @p262 :rule reordering :premises (@p72) :args ((or @t9 @t19))) % 0.37/0.60 (step @p263 :rule reordering :premises (@p50) :args ((or @t10 @t11))) % 0.37/0.60 (step @p264 :rule reordering :premises (@p81) :args ((or @t13 @t23))) % 0.37/0.60 (step @p265 :rule reordering :premises (@p105) :args ((or @t22 @t34))) % 0.37/0.60 (step @p266 :rule chain_m_resolution :premises (@p265 @p191 @p186 @p264 @p188 @p189 @p263 @p190 @p238 @p260 @p262 @p236) :args ((or tptp.vertical_3_6 @t19) (@list false false true true false true true false true true true) (@list tptp.vertical_2_5 tptp.horizontal_3_5 tptp.horizontal_2_5 tptp.vertical_2_6 tptp.vertical_1_6 tptp.vertical_1_5 tptp.horizontal_1_5 tptp.horizontal_1_4 tptp.horizontal_1_3 tptp.vertical_1_4 tptp.horizontal_2_4))) % 0.37/0.60 (step @p267 :rule reordering :premises (@p165) :args ((or @t44 @t56))) % 0.37/0.60 (step @p268 :rule reordering :premises (@p44) :args ((or @t6 @t7))) % 0.37/0.60 (step @p269 :rule chain_m_resolution :premises (@p268 @p258) :args (@t7 @t62 @t63)) % 0.37/0.60 (step @p270 :rule reordering :premises (@p129) :args ((or @t31 @t43))) % 0.37/0.60 (step @p271 :rule reordering :premises (@p70) :args ((or @t19 @t20))) % 0.37/0.60 (step @p272 :rule reordering :premises (@p104) :args ((or @t32 @t34))) % 0.37/0.60 (step @p273 :rule reordering :premises (@p108) :args ((or @t22 @t32))) % 0.37/0.60 (step @p274 :rule chain_m_resolution :premises (@p187 @p191 @p186 @p263 @p273 @p272 @p238 @p260 @p215 @p262 @p271 @p236 @p239 @p269 @p241 @p91 @p210 @p270 @p211) :args ((or tptp.horizontal_2_2 tptp.vertical_3_6 tptp.horizontal_4_2 tptp.vertical_4_3 @t43) (@list false false true true true false true false true true true false true true true false true true) (@list tptp.horizontal_2_5 tptp.vertical_2_6 tptp.vertical_1_5 tptp.vertical_2_5 tptp.horizontal_3_5 tptp.horizontal_1_4 tptp.horizontal_1_3 tptp.horizontal_3_4 tptp.vertical_1_4 tptp.vertical_2_4 tptp.horizontal_2_4 tptp.horizontal_2_3 tptp.vertical_1_3 tptp.vertical_2_3 tptp.horizontal_3_3 tptp.vertical_3_3 tptp.vertical_3_4 tptp.horizontal_4_3))) % 0.37/0.60 (step @p275 :rule chain_m_resolution :premises (@p248 @p227 @p246 @p3 @p250 @p163) :args ((or tptp.vertical_4_4 tptp.horizontal_5_3 @t56) (@list false false true true true) (@list tptp.vertical_5_4 tptp.horizontal_6_4 tptp.horizontal_6_5 tptp.horizontal_5_4 tptp.vertical_5_5))) % 0.37/0.60 (step @p276 :rule chain_m_resolution :premises (@p248 @p227 @p246 @p3 @p251 @p199 @p213 @p201 @p200 @p4 @p275 @p249 @p210 @p241 @p239 @p269 @p266 @p274 @p261) :args ((or tptp.horizontal_2_2 tptp.vertical_3_6 tptp.horizontal_4_2 tptp.vertical_4_3 tptp.horizontal_5_3) (@list false false true true true false true false true true true false true false true true true true) (@list tptp.vertical_5_4 tptp.horizontal_6_4 tptp.horizontal_6_5 tptp.horizontal_5_4 tptp.vertical_5_5 tptp.vertical_4_5 tptp.horizontal_4_5 tptp.vertical_4_6 tptp.vertical_5_6 tptp.horizontal_5_5 tptp.vertical_4_4 tptp.horizontal_4_3 tptp.vertical_3_3 tptp.vertical_2_3 tptp.vertical_1_3 tptp.horizontal_2_3 tptp.horizontal_4_4 tptp.vertical_3_5))) % 0.37/0.60 (step @p277 :rule chain_m_resolution :premises (@p187 @p191 @p186 @p263 @p273 @p272 @p238 @p260 @p215 @p262 @p271 @p236 @p239 @p269 @p241 @p91 @p210 @p115 @p222 @p234 @p227 @p270 @p211 @p127 @p213 @p261 @p202 @p201 @p200 @p4 @p199 @p198 @p163 @p246 @p3 @p228 @p247) :args ((or tptp.horizontal_2_2 tptp.vertical_4_3 tptp.horizontal_5_1 tptp.vertical_5_2 @t59) (@list false false true true true false true false true true true false true true true false true false true false true true true false true true true false true true true true false true true true) (@list tptp.horizontal_2_5 tptp.vertical_2_6 tptp.vertical_1_5 tptp.vertical_2_5 tptp.horizontal_3_5 tptp.horizontal_1_4 tptp.horizontal_1_3 tptp.horizontal_3_4 tptp.vertical_1_4 tptp.vertical_2_4 tptp.horizontal_2_4 tptp.horizontal_2_3 tptp.vertical_1_3 tptp.vertical_2_3 tptp.horizontal_3_3 tptp.vertical_3_3 tptp.horizontal_4_2 tptp.vertical_4_2 tptp.horizontal_5_2 tptp.horizontal_5_3 tptp.vertical_3_4 tptp.horizontal_4_3 tptp.vertical_4_4 tptp.horizontal_4_4 tptp.vertical_3_5 tptp.vertical_3_6 tptp.horizontal_4_5 tptp.vertical_4_6 tptp.vertical_5_6 tptp.vertical_4_5 tptp.horizontal_5_4 tptp.horizontal_5_5 tptp.vertical_5_5 tptp.horizontal_6_5 tptp.vertical_5_4 tptp.horizontal_6_4))) % 0.37/0.60 (step @p278 :rule reordering :premises (@p141) :args ((or @t35 @t45))) % 0.37/0.60 (step @p279 :rule reordering :premises (@p131) :args ((or @t31 @t42))) % 0.37/0.60 (step @p280 :rule chain_m_resolution :premises (@p271 @p239 @p269 @p215 @p241 @p91 @p214 @p210 @p213 @p279 @p249 @p127 @p275 @p267 @p200 @p4 @p278 @p202 @p276 @p115 @p222 @p203 @p151 @p229 @p277) :args ((or tptp.horizontal_2_2 tptp.vertical_4_3 tptp.horizontal_5_1 tptp.vertical_5_2 tptp.horizontal_6_2) (@list false true false true true true false false true true true false true false true true true false true false true true false true) (@list tptp.horizontal_2_3 tptp.vertical_1_3 tptp.vertical_2_4 tptp.vertical_2_3 tptp.horizontal_3_3 tptp.horizontal_3_4 tptp.vertical_3_3 tptp.vertical_3_5 tptp.vertical_3_4 tptp.horizontal_4_3 tptp.horizontal_4_4 tptp.vertical_4_4 tptp.vertical_4_5 tptp.horizontal_5_5 tptp.vertical_5_6 tptp.horizontal_4_5 tptp.vertical_4_6 tptp.vertical_3_6 tptp.horizontal_4_2 tptp.vertical_4_2 tptp.horizontal_5_2 tptp.horizontal_5_3 tptp.vertical_5_3 tptp.horizontal_6_3))) % 0.37/0.60 (step @p281 :rule reordering :premises (@p56) :args ((or @t15 @t17))) % 0.37/0.60 (step @p282 :rule reordering :premises (@p177) :args ((or @t51 @t59))) % 0.37/0.60 (step @p283 :rule chain_m_resolution :premises (@p226 @p222 @p216 @p232 @p217 @p219 @p142 @p220 @p231 @p230 @p229 @p224) :args ((or tptp.vertical_2_2 tptp.horizontal_3_1 tptp.vertical_3_1 tptp.vertical_3_6 tptp.horizontal_4_5 tptp.vertical_4_5 tptp.horizontal_6_3) (@list false false true false true true false true true false true) (@list tptp.horizontal_5_2 tptp.vertical_4_3 tptp.vertical_4_2 tptp.horizontal_4_1 tptp.vertical_4_1 tptp.horizontal_5_1 tptp.vertical_5_1 tptp.vertical_5_2 tptp.horizontal_6_1 tptp.horizontal_6_2 tptp.vertical_5_3))) % 0.37/0.60 (step @p284 :rule chain_m_resolution :premises (@p283 @p202 @p201 @p200 @p4 @p199 @p163 @p246 @p3 @p248 @p253 @p210 @p209 @p207 @p223 @p115 @p222 @p282 @p203) :args ((or tptp.vertical_2_2 tptp.horizontal_3_1 tptp.vertical_3_1 tptp.vertical_4_3 tptp.horizontal_5_1 tptp.vertical_5_2 @t51) (@list true true false true true true false true true false false true false true true false true true) (@list tptp.vertical_3_6 tptp.horizontal_4_5 tptp.vertical_4_6 tptp.vertical_5_6 tptp.vertical_4_5 tptp.horizontal_5_5 tptp.vertical_5_5 tptp.horizontal_6_5 tptp.horizontal_6_4 tptp.vertical_5_4 tptp.horizontal_4_3 tptp.vertical_3_3 tptp.horizontal_3_2 tptp.vertical_3_2 tptp.horizontal_4_2 tptp.vertical_4_2 tptp.horizontal_6_3 tptp.horizontal_5_2))) % 0.37/0.60 (step @p285 :rule chain_m_resolution :premises (@p237 @p238 @p260 @p191 @p190 @p48 @p189 @p188 @p187 @p186 @p185 @p103 @p213 @p235 @p202 @p201 @p200 @p4 @p199 @p198 @p163 @p246 @p3 @p247 @p229 @p284) :args ((or tptp.vertical_2_2 tptp.horizontal_3_1 tptp.vertical_3_1 tptp.vertical_4_3 tptp.horizontal_5_1 tptp.vertical_5_2 tptp.horizontal_6_2) (@list false true false true true false true true false true true false true true true false true true true true false true true false true) (@list tptp.vertical_1_4 tptp.horizontal_1_3 tptp.horizontal_2_4 tptp.horizontal_1_4 tptp.vertical_1_5 tptp.horizontal_1_5 tptp.vertical_1_6 tptp.horizontal_2_5 tptp.vertical_2_6 tptp.vertical_2_5 tptp.horizontal_3_5 tptp.vertical_3_5 tptp.horizontal_4_4 tptp.vertical_3_6 tptp.horizontal_4_5 tptp.vertical_4_6 tptp.vertical_5_6 tptp.vertical_4_5 tptp.horizontal_5_4 tptp.horizontal_5_5 tptp.vertical_5_5 tptp.horizontal_6_5 tptp.horizontal_6_4 tptp.horizontal_6_3 tptp.vertical_5_3))) % 0.37/0.60 (step @p286 :rule chain_m_resolution :premises (@p196 @p195 @p2 @p285 @p281 @p55 @p280 @p221 @p230 @p220 @p219 @p218 @p217) :args ((or tptp.vertical_3_1 tptp.horizontal_4_1 tptp.vertical_4_3) (@list false true false true true false true true false true true false) (@list tptp.vertical_2_1 tptp.vertical_1_1 tptp.horizontal_3_1 tptp.horizontal_2_1 tptp.vertical_2_2 tptp.horizontal_2_2 tptp.vertical_5_2 tptp.horizontal_6_2 tptp.horizontal_6_1 tptp.vertical_5_1 tptp.horizontal_5_1 tptp.vertical_4_1))) % 0.37/0.60 (step @p287 :rule reordering :premises (@p58) :args ((or @t15 @t16))) % 0.37/0.60 (step @p288 :rule chain_m_resolution :premises (@p287 @p195 @p2 @p207 @p197 @p82 @p286 @p243 @p205 @p242 @p276 @p239 @p269 @p266) :args ((or tptp.horizontal_2_2 tptp.vertical_3_6 tptp.vertical_4_3 tptp.horizontal_5_3) (@list false true false true true false true true true false false true true) (@list tptp.horizontal_2_1 tptp.vertical_1_1 tptp.vertical_2_2 tptp.vertical_2_1 tptp.horizontal_3_1 tptp.vertical_3_1 tptp.vertical_3_2 tptp.horizontal_4_1 tptp.horizontal_3_2 tptp.horizontal_4_2 tptp.vertical_2_3 tptp.vertical_1_3 tptp.horizontal_2_3))) % 0.37/0.60 (step @p289 :rule chain_m_resolution :premises (@p217 @p255 @p197 @p196 @p195 @p2 @p281 @p55 @p288 @p249 @p227 @p151 @p229 @p248 @p247 @p202 @p246 @p3 @p200 @p4 @p251 @p199 @p267) :args ((or tptp.vertical_4_1 tptp.vertical_4_3 tptp.horizontal_6_2 @t44) (@list true true true false true true true false true false true false true true true false true false true true true true) (@list tptp.horizontal_4_1 tptp.vertical_3_1 tptp.horizontal_3_1 tptp.vertical_2_1 tptp.vertical_1_1 tptp.horizontal_2_1 tptp.vertical_2_2 tptp.horizontal_2_2 tptp.horizontal_4_3 tptp.vertical_4_4 tptp.horizontal_5_3 tptp.vertical_5_3 tptp.vertical_5_4 tptp.horizontal_6_3 tptp.vertical_3_6 tptp.horizontal_6_4 tptp.horizontal_6_5 tptp.vertical_4_6 tptp.vertical_5_6 tptp.horizontal_5_4 tptp.vertical_5_5 tptp.horizontal_5_5))) % 0.37/0.60 (step @p290 :rule chain_m_resolution :premises (@p213 @p274 @p261) :args ((or tptp.horizontal_2_2 tptp.vertical_3_6 tptp.horizontal_4_2 tptp.vertical_4_3 tptp.horizontal_4_5 tptp.vertical_4_5) @t61 (@list tptp.horizontal_4_4 tptp.vertical_3_5))) % 0.37/0.60 (step @p291 :rule chain_m_resolution :premises (@p229 @p247 @p151 @p246 @p3 @p275 @p163) :args ((or tptp.vertical_4_4 tptp.horizontal_6_2 @t56) (@list true true false true false true) (@list tptp.horizontal_6_3 tptp.vertical_5_3 tptp.horizontal_6_4 tptp.horizontal_6_5 tptp.horizontal_5_3 tptp.vertical_5_5))) % 0.37/0.60 (step @p292 :rule chain_m_resolution :premises (@p271 @p239 @p269 @p215 @p241 @p91) :args ((or tptp.horizontal_2_2 tptp.horizontal_3_4 tptp.vertical_3_4 @t29) @t64 (@list tptp.horizontal_2_3 tptp.vertical_1_3 tptp.vertical_2_4 tptp.vertical_2_3 tptp.horizontal_3_3))) % 0.37/0.60 (step @p293 :rule chain_m_resolution :premises (@p292 @p214 @p210 @p213 @p279 @p249 @p127 @p291 @p200 @p4 @p202 @p290 @p205 @p217 @p197 @p195 @p2 @p287 @p55) :args ((or tptp.vertical_4_1 tptp.vertical_4_3 tptp.horizontal_4_5 tptp.vertical_4_5 tptp.horizontal_6_2 @t16) (@list true false false true true true false false true true false true false true false true true true) (@list tptp.horizontal_3_4 tptp.vertical_3_3 tptp.vertical_3_5 tptp.vertical_3_4 tptp.horizontal_4_3 tptp.horizontal_4_4 tptp.vertical_4_4 tptp.horizontal_5_5 tptp.vertical_5_6 tptp.vertical_4_6 tptp.vertical_3_6 tptp.horizontal_4_2 tptp.horizontal_4_1 tptp.vertical_3_1 tptp.vertical_2_1 tptp.vertical_1_1 tptp.horizontal_2_1 tptp.horizontal_2_2))) % 0.37/0.60 (step @p294 :rule chain_m_resolution :premises (@p271 @p239 @p269 @p215 @p242 @p208 @p207 @p243 @p210 @p292 @p281 @p195 @p2 @p197 @p286 @p214 @p255 @p213 @p279 @p249 @p127) :args ((or tptp.vertical_2_2 tptp.horizontal_3_1 tptp.vertical_4_3 tptp.horizontal_4_5 tptp.vertical_4_5 @t42) (@list false true false true true false true false true true false true true false true true false true true true) (@list tptp.horizontal_2_3 tptp.vertical_1_3 tptp.vertical_2_4 tptp.vertical_2_3 tptp.horizontal_3_3 tptp.horizontal_3_2 tptp.vertical_3_2 tptp.horizontal_4_2 tptp.vertical_3_3 tptp.horizontal_2_2 tptp.horizontal_2_1 tptp.vertical_1_1 tptp.vertical_2_1 tptp.vertical_3_1 tptp.horizontal_3_4 tptp.horizontal_4_1 tptp.vertical_3_5 tptp.vertical_3_4 tptp.horizontal_4_3 tptp.horizontal_4_4))) % 0.37/0.60 (step @p295 :rule chain_m_resolution :premises (@p207 @p242 @p243 @p239 @p269 @p274 @p281 @p195 @p2 @p197 @p213 @p286 @p266 @p261 @p216 @p202 @p200 @p4 @p291 @p294) :args ((or tptp.vertical_2_2 tptp.horizontal_3_1 tptp.vertical_4_3 tptp.horizontal_4_5 tptp.vertical_4_5 tptp.horizontal_6_2) (@list true true false true false true false true true false false true true true true false true true true) (@list tptp.horizontal_3_2 tptp.vertical_3_2 tptp.vertical_2_3 tptp.vertical_1_3 tptp.horizontal_4_2 tptp.horizontal_2_2 tptp.horizontal_2_1 tptp.vertical_1_1 tptp.vertical_2_1 tptp.horizontal_4_4 tptp.vertical_3_1 tptp.horizontal_2_3 tptp.vertical_3_5 tptp.horizontal_4_1 tptp.vertical_3_6 tptp.vertical_4_6 tptp.vertical_5_6 tptp.horizontal_5_5 tptp.vertical_4_4))) % 0.37/0.60 (step @p296 :rule chain_m_resolution :premises (@p292 @p214 @p210 @p213 @p279 @p249 @p127 @p291 @p200 @p4 @p202 @p290 @p281 @p205 @p195 @p2 @p217 @p196 @p82 @p295 @p293) :args ((or tptp.vertical_4_1 tptp.vertical_4_3 tptp.horizontal_4_5 tptp.vertical_4_5 tptp.horizontal_6_2) (@list true false false true true true false false true true false true true false true false true true false true) (@list tptp.horizontal_3_4 tptp.vertical_3_3 tptp.vertical_3_5 tptp.vertical_3_4 tptp.horizontal_4_3 tptp.horizontal_4_4 tptp.vertical_4_4 tptp.horizontal_5_5 tptp.vertical_5_6 tptp.vertical_4_6 tptp.vertical_3_6 tptp.horizontal_2_2 tptp.horizontal_4_2 tptp.horizontal_2_1 tptp.vertical_1_1 tptp.horizontal_4_1 tptp.vertical_2_1 tptp.vertical_3_1 tptp.horizontal_3_1 tptp.vertical_2_2))) % 0.37/0.60 (step @p297 :rule reordering :premises (@p162) :args ((or @t42 @t52))) % 0.37/0.60 (step @p298 :rule chain_m_resolution :premises (@p217 @p255 @p197 @p196 @p195 @p2 @p281 @p55 @p288 @p297 @p249 @p291 @p200 @p4 @p278 @p201 @p296 @p289 @p230 @p220 @p218 @p142) :args ((or tptp.vertical_4_3 @t48) (@list true true true false true true true false true true false false true true true false true true false true true) (@list tptp.horizontal_4_1 tptp.vertical_3_1 tptp.horizontal_3_1 tptp.vertical_2_1 tptp.vertical_1_1 tptp.horizontal_2_1 tptp.vertical_2_2 tptp.horizontal_2_2 tptp.horizontal_5_3 tptp.horizontal_4_3 tptp.vertical_4_4 tptp.horizontal_5_5 tptp.vertical_5_6 tptp.vertical_3_6 tptp.vertical_4_6 tptp.horizontal_4_5 tptp.vertical_4_5 tptp.horizontal_6_2 tptp.horizontal_6_1 tptp.vertical_4_1 tptp.vertical_5_1))) % 0.37/0.60 (step @p299 :rule chain_m_resolution :premises (@p222 @p234 @p231 @p275 @p291) :args ((or tptp.vertical_4_2 tptp.vertical_4_4 tptp.horizontal_5_1 @t56) (@list true true false false) (@list tptp.horizontal_5_2 tptp.vertical_5_2 tptp.horizontal_5_3 tptp.horizontal_6_2))) % 0.37/0.60 (step @p300 :rule reordering :premises (@p176) :args ((or @t58 @t59))) % 0.37/0.60 (step @p301 :rule chain_m_resolution :premises (@p253 @p248 @p300 @p246 @p3 @p289 @p199 @p216 @p202 @p201 @p200 @p4 @p299 @p249 @p255 @p232 @p112 @p286 @p197 @p196 @p195 @p2 @p281 @p55 @p298) :args ((or tptp.vertical_4_3 @t17) (@list true true false true false true false true true false true true true false true true false true true false true true true true) (@list tptp.vertical_5_4 tptp.horizontal_6_3 tptp.horizontal_6_4 tptp.horizontal_6_5 tptp.horizontal_6_2 tptp.vertical_5_5 tptp.vertical_4_5 tptp.vertical_3_6 tptp.horizontal_4_5 tptp.vertical_4_6 tptp.vertical_5_6 tptp.horizontal_5_5 tptp.vertical_4_4 tptp.horizontal_4_3 tptp.vertical_4_2 tptp.vertical_4_1 tptp.horizontal_4_1 tptp.vertical_3_1 tptp.horizontal_3_1 tptp.vertical_2_1 tptp.vertical_1_1 tptp.horizontal_2_1 tptp.vertical_2_2 tptp.horizontal_5_1))) % 0.37/0.60 (step @p302 :rule chain_m_resolution :premises (@p82 @p207 @p286 @p223 @p232 @p222 @p231 @p229 @p242 @p234 @p151 @p239 @p269 @p288 @p266 @p247 @p202 @p246 @p3 @p200 @p4 @p199 @p267 @p301 @p298) :args ((or tptp.vertical_2_2 tptp.vertical_4_3 @t44) (@list false false true true false true false true true true false true false true true true false true false true true true true true) (@list tptp.horizontal_3_1 tptp.vertical_3_1 tptp.vertical_3_2 tptp.horizontal_4_1 tptp.vertical_4_2 tptp.vertical_5_2 tptp.horizontal_6_2 tptp.horizontal_3_2 tptp.horizontal_5_2 tptp.vertical_5_3 tptp.vertical_2_3 tptp.vertical_1_3 tptp.horizontal_5_3 tptp.horizontal_2_3 tptp.horizontal_6_3 tptp.vertical_3_6 tptp.horizontal_6_4 tptp.horizontal_6_5 tptp.vertical_4_6 tptp.vertical_5_6 tptp.vertical_5_5 tptp.horizontal_5_5 tptp.horizontal_2_2 tptp.horizontal_5_1))) % 0.37/0.60 (step @p303 :rule chain_m_resolution :premises (@p82 @p207 @p286 @p242 @p243 @p205 @p239 @p269 @p290 @p266 @p202 @p201 @p302 @p301) :args ((or tptp.vertical_2_2 tptp.vertical_4_3 @t46) (@list false false true true true false true false true true true true true) (@list tptp.horizontal_3_1 tptp.vertical_3_1 tptp.horizontal_3_2 tptp.vertical_3_2 tptp.horizontal_4_1 tptp.vertical_2_3 tptp.vertical_1_3 tptp.horizontal_4_2 tptp.horizontal_2_3 tptp.vertical_3_6 tptp.horizontal_4_5 tptp.vertical_4_5 tptp.horizontal_2_2))) % 0.37/0.60 (step @p304 :rule chain_m_resolution :premises (@p214 @p215 @p213 @p279 @p127 @p275 @p234 @p222 @p271 @p223 @p239 @p269 @p207 @p241 @p209 @p91 @p267) :args ((or tptp.horizontal_2_2 tptp.vertical_2_2 tptp.horizontal_3_1 tptp.horizontal_4_5 tptp.horizontal_5_1 tptp.vertical_5_2 @t29 @t56) (@list false false true true false true false true true false true false true true true true) (@list tptp.horizontal_3_4 tptp.vertical_3_5 tptp.vertical_3_4 tptp.horizontal_4_4 tptp.vertical_4_4 tptp.horizontal_5_3 tptp.horizontal_5_2 tptp.vertical_2_4 tptp.vertical_4_2 tptp.horizontal_2_3 tptp.vertical_1_3 tptp.vertical_3_2 tptp.vertical_2_3 tptp.horizontal_3_2 tptp.horizontal_3_3 tptp.vertical_4_5))) % 0.37/0.60 (step @p305 :rule chain_m_resolution :premises (@p214 @p215 @p213 @p271 @p279 @p127 @p239 @p269 @p275 @p242 @p208 @p234 @p207 @p222 @p243 @p115 @p267) :args ((or tptp.horizontal_2_2 tptp.vertical_2_2 tptp.horizontal_3_1 tptp.horizontal_4_5 tptp.horizontal_5_1 tptp.vertical_5_2 @t39 @t56) (@list false false true true true false true false true true true false false true true true) (@list tptp.horizontal_3_4 tptp.vertical_3_5 tptp.vertical_2_4 tptp.vertical_3_4 tptp.horizontal_4_4 tptp.horizontal_2_3 tptp.vertical_1_3 tptp.vertical_4_4 tptp.vertical_2_3 tptp.horizontal_3_3 tptp.horizontal_5_3 tptp.horizontal_3_2 tptp.horizontal_5_2 tptp.vertical_3_2 tptp.vertical_4_2 tptp.vertical_4_5))) % 0.37/0.60 (step @p306 :rule chain_m_resolution :premises (@p271 @p239 @p269 @p215 @p242 @p208 @p207 @p223 @p222 @p234 @p214 @p275 @p213 @p212 @p249 @p211 @p210 @p305 @p304 @p267) :args ((or tptp.horizontal_2_2 tptp.vertical_2_2 tptp.horizontal_3_1 tptp.vertical_4_3 tptp.horizontal_4_5 tptp.horizontal_5_1 tptp.vertical_5_2 @t56) (@list false true false true true false true false true true false false true true true false true true true) (@list tptp.horizontal_2_3 tptp.vertical_1_3 tptp.vertical_2_4 tptp.vertical_2_3 tptp.horizontal_3_3 tptp.horizontal_3_2 tptp.vertical_3_2 tptp.vertical_4_2 tptp.horizontal_5_2 tptp.horizontal_3_4 tptp.horizontal_5_3 tptp.vertical_3_5 tptp.vertical_3_4 tptp.vertical_4_4 tptp.horizontal_4_4 tptp.horizontal_4_3 tptp.horizontal_4_2 tptp.vertical_3_3 tptp.vertical_4_5))) % 0.37/0.60 (step @p307 :rule chain_m_resolution :premises (@p239 @p269 @p266 @p242 @p278 @p207 @p306 @p82 @p286 @p223 @p232 @p231 @p299 @p291 @p200 @p4 @p303 @p298 @p301) :args ((or tptp.vertical_2_2 tptp.vertical_4_3 tptp.vertical_4_4) (@list true true true true false false true false true true true false false false true true true true) (@list tptp.vertical_1_3 tptp.horizontal_2_3 tptp.vertical_2_3 tptp.vertical_3_6 tptp.horizontal_3_2 tptp.horizontal_4_5 tptp.horizontal_3_1 tptp.vertical_3_1 tptp.vertical_3_2 tptp.horizontal_4_1 tptp.vertical_5_2 tptp.vertical_4_2 tptp.horizontal_6_2 tptp.horizontal_5_5 tptp.vertical_5_6 tptp.vertical_4_6 tptp.horizontal_5_1 tptp.horizontal_2_2))) % 0.37/0.60 (step @p308 :rule chain_m_resolution :premises (@p231 @p222 @p289 @p234 @p290 @p288 @p202 @p201 @p200 @p4 @p299 @p232 @p205 @p112 @p286 @p197 @p195 @p2 @p287 @p307 @p301 @p298) :args ((or tptp.vertical_4_3 tptp.vertical_4_4) (@list false false true false false true true false true true true true true false true false true true false true true) (@list tptp.vertical_5_2 tptp.horizontal_6_2 tptp.horizontal_5_2 tptp.vertical_4_5 tptp.horizontal_5_3 tptp.vertical_3_6 tptp.horizontal_4_5 tptp.vertical_4_6 tptp.vertical_5_6 tptp.horizontal_5_5 tptp.vertical_4_2 tptp.horizontal_4_2 tptp.vertical_4_1 tptp.horizontal_4_1 tptp.vertical_3_1 tptp.vertical_2_1 tptp.vertical_1_1 tptp.horizontal_2_1 tptp.vertical_2_2 tptp.horizontal_2_2 tptp.horizontal_5_1))) % 0.37/0.60 (step @p309 :rule chain_m_resolution :premises (@p287 @p195 @p2 @p294 @p197 @p82 @p286 @p205 @p210 @p292 @p214 @p213 @p267 @p200 @p4 @p278 @p202 @p288 @p297 @p279 @p249 @p127 @p308 @p301) :args (tptp.vertical_4_3 (@list false true false true true false true false true true false true false true true true false true true true true false true) (@list tptp.horizontal_2_1 tptp.vertical_1_1 tptp.vertical_2_2 tptp.vertical_2_1 tptp.horizontal_3_1 tptp.vertical_3_1 tptp.horizontal_4_1 tptp.horizontal_4_2 tptp.vertical_3_3 tptp.horizontal_3_4 tptp.vertical_3_5 tptp.vertical_4_5 tptp.horizontal_5_5 tptp.vertical_5_6 tptp.horizontal_4_5 tptp.vertical_4_6 tptp.vertical_3_6 tptp.horizontal_5_3 tptp.vertical_3_4 tptp.horizontal_4_3 tptp.horizontal_4_4 tptp.vertical_4_4 tptp.horizontal_2_2))) % 0.37/0.60 (step @p310 :rule chain_m_resolution :premises (@p204 @p309) :args (@t51 @t62 @t65)) % 0.37/0.60 (step @p311 :rule chain_m_resolution :premises (@p261 @p213 @p127 @p202 @p201 @p233 @p310 @p309 @p200 @p4 @p199 @p198 @p163 @p246 @p3 @p247 @p254 @p309) :args (tptp.vertical_3_1 (@list false true true true false true false false true true true true false true true false false) (@list tptp.vertical_3_5 tptp.horizontal_4_4 tptp.vertical_3_6 tptp.horizontal_4_5 tptp.vertical_4_4 tptp.vertical_5_3 tptp.vertical_4_3 tptp.vertical_4_6 tptp.vertical_5_6 tptp.vertical_4_5 tptp.horizontal_5_4 tptp.horizontal_5_5 tptp.vertical_5_5 tptp.horizontal_6_5 tptp.horizontal_6_4 tptp.horizontal_6_3 tptp.vertical_4_3))) % 0.37/0.60 (step @p312 :rule chain_m_resolution :premises (@p197 @p311) :args (@t14 @t62 @t66)) % 0.37/0.60 (step @p313 :rule chain_m_resolution :premises (@p195 @p2 @p312) :args (tptp.horizontal_2_1 @t61 (@list tptp.vertical_1_1 tptp.vertical_2_1))) % 0.37/0.60 (step @p314 :rule chain_m_resolution :premises (@p281 @p313) :args (@t17 @t62 @t67)) % 0.37/0.60 (step @p315 :rule chain_m_resolution :premises (@p287 @p313) :args (@t16 @t62 @t67)) % 0.37/0.60 (step @p316 :rule chain_m_resolution :premises (@p82 @p311) :args (@t26 @t62 @t66)) % 0.37/0.60 (step @p317 :rule chain_m_resolution :premises (@p226 @p309) :args (@t50 @t62 @t65)) % 0.37/0.60 (step @p318 :rule chain_m_resolution :premises (@p142 @p222 @p317 @p220 @p231 @p230) :args ((or tptp.vertical_4_2 @t58) @t64 (@list tptp.horizontal_5_1 tptp.horizontal_5_2 tptp.vertical_5_1 tptp.vertical_5_2 tptp.horizontal_6_1))) % 0.37/0.60 (step @p319 :rule chain_m_resolution :premises (@p225 @p309) :args (@t52 @t62 @t65)) % 0.37/0.60 (step @p320 :rule chain_m_resolution :premises (@p198 @p227 @p319 @p246 @p3 @p228 @p247) :args ((or tptp.vertical_4_4 @t59) (@list false true false true true true) (@list tptp.horizontal_5_4 tptp.horizontal_5_3 tptp.vertical_5_5 tptp.horizontal_6_5 tptp.vertical_5_4 tptp.horizontal_6_4))) % 0.37/0.60 (step @p321 :rule chain_m_resolution :premises (@p201 @p200 @p4 @p213 @p199 @p163 @p127 @p246 @p3 @p320 @p247 @p229 @p310 @p318 @p223 @p207 @p316 @p315 @p242 @p239 @p269 @p314 @p266 @p261) :args (tptp.vertical_3_6 (@list false true false true true true false true false true false true true true false true true true false true true true true) (@list tptp.vertical_4_6 tptp.vertical_5_6 tptp.horizontal_4_5 tptp.vertical_4_5 tptp.horizontal_5_5 tptp.horizontal_4_4 tptp.vertical_5_5 tptp.horizontal_6_5 tptp.vertical_4_4 tptp.horizontal_6_4 tptp.horizontal_6_3 tptp.vertical_5_3 tptp.horizontal_6_2 tptp.vertical_4_2 tptp.vertical_3_2 tptp.horizontal_3_1 tptp.vertical_2_2 tptp.horizontal_3_2 tptp.vertical_2_3 tptp.vertical_1_3 tptp.horizontal_2_2 tptp.horizontal_2_3 tptp.vertical_3_5))) % 0.37/0.60 (step @p322 :rule chain_m_resolution :premises (@p202 @p321) :args (@t46 @t62 @t68)) % 0.37/0.60 (step @p323 :rule chain_m_resolution :premises (@p200 @p4 @p322) :args (tptp.horizontal_5_5 @t61 (@list tptp.vertical_5_6 tptp.vertical_4_6))) % 0.37/0.60 (step @p324 :rule chain_m_resolution :premises (@p275 @p319 @p323) :args (tptp.vertical_4_4 (@list true false) (@list tptp.horizontal_5_3 tptp.horizontal_5_5))) % 0.37/0.60 (step @p325 :rule chain_m_resolution :premises (@p279 @p324) :args (@t31 @t62 @t69)) % 0.37/0.60 (step @p326 :rule chain_m_resolution :premises (@p267 @p323) :args (@t44 @t62 @t70)) % 0.37/0.60 (step @p327 :rule chain_m_resolution :premises (@p278 @p321) :args (@t45 @t62 @t68)) % 0.37/0.60 (step @p328 :rule chain_m_resolution :premises (@p127 @p324) :args (@t43 @t62 @t69)) % 0.37/0.60 (step @p329 :rule chain_m_resolution :premises (@p213 @p328 @p327 @p326) :args (tptp.vertical_3_5 @t71 (@list tptp.horizontal_4_4 tptp.horizontal_4_5 tptp.vertical_4_5))) % 0.37/0.60 (step @p330 :rule chain_m_resolution :premises (@p214 @p329) :args (@t32 @t62 (@list tptp.vertical_3_5))) % 0.37/0.60 (step @p331 :rule chain_m_resolution :premises (@p163 @p323) :args (@t55 @t62 @t70)) % 0.37/0.60 (step @p332 :rule chain_m_resolution :premises (@p246 @p3 @p331) :args (tptp.horizontal_6_4 @t61 (@list tptp.horizontal_6_5 tptp.vertical_5_5))) % 0.37/0.60 (step @p333 :rule chain_m_resolution :premises (@p247 @p332) :args (@t59 @t62 (@list tptp.horizontal_6_4))) % 0.37/0.60 (step @p334 :rule chain_m_resolution :premises (@p229 @p310 @p333) :args (tptp.horizontal_6_2 @t61 (@list tptp.vertical_5_3 tptp.horizontal_6_3))) % 0.37/0.60 (step @p335 :rule chain_m_resolution :premises (@p318 @p334) :args (tptp.vertical_4_2 @t62 (@list tptp.horizontal_6_2))) % 0.37/0.60 (step @p336 :rule chain_m_resolution :premises (@p223 @p335) :args (@t27 @t62 (@list tptp.vertical_4_2))) % 0.37/0.60 (step @p337 :rule chain_m_resolution :premises (@p207 @p315 @p316 @p336) :args (tptp.horizontal_3_2 @t71 (@list tptp.vertical_2_2 tptp.horizontal_3_1 tptp.vertical_3_2))) % 0.37/0.60 (step @p338 :rule chain_m_resolution :premises (@p208 @p337) :args (@t30 @t62 @t72)) % 0.37/0.60 (step @p339 :rule chain_m_resolution :premises (@p215 @p338 @p330 @p325) :args (tptp.vertical_2_4 @t71 (@list tptp.horizontal_3_3 tptp.horizontal_3_4 tptp.vertical_3_4))) % 0.37/0.60 (step @p340 :rule chain_m_resolution :premises (@p242 @p337) :args (@t18 @t62 @t72)) % 0.37/0.60 (step @p341 :rule chain_m_resolution :premises (@p239 @p269 @p314 @p340) :args (tptp.horizontal_2_3 @t71 (@list tptp.vertical_1_3 tptp.horizontal_2_2 tptp.vertical_2_3))) % 0.37/0.60 (step @p342 false :rule chain_m_resolution :premises (@p271 @p341 @p339) :args (false (@list false false) (@list tptp.horizontal_2_3 tptp.vertical_2_4))) % 0.37/0.60 ) % 0.37/0.60 % SZS output end Proof % 0.37/0.60 % cvc5 exiting %------------------------------------------------------------------------------