%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWC193-1 : TPTP v9.2.1. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n011.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:58:25 AM UTC 2026 % Result : Unsatisfiable 60.13s 60.39s % Output : Proof 60.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWC193-1 : TPTP v9.2.1. Released v2.4.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.34 % Computer : n011.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Tue Jun 2 19:22:20 EDT 2026 % 0.17/0.34 % CPUTime : % 0.32/0.52 %----Proving TF0_NAR, FOF, or CNF % 0.32/0.54 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.37/15.81 --- Run --no-e-matching --full-saturate-quant at 6... % 21.63/21.85 --- Run --no-e-matching --enum-inst-sum --full-saturate-quant at 6... % 27.63/27.88 --- Run --finite-model-find --uf-ss=no-minimal at 6... % 33.74/33.99 --- Run --multi-trigger-when-single --full-saturate-quant at 30... % 60.13/60.39 % SZS status Unsatisfiable % 60.13/60.39 % SZS output start Proof % 60.23/60.42 ( % 60.23/60.42 (declare-sort $$unsorted 0) % 60.23/60.42 (declare-const tptp.sk8 $$unsorted) % 60.23/60.42 (declare-const tptp.sk7 $$unsorted) % 60.23/60.42 (declare-const tptp.sk6 $$unsorted) % 60.23/60.42 (declare-const tptp.sk5 $$unsorted) % 60.23/60.42 (declare-const tptp.sk4 $$unsorted) % 60.23/60.42 (declare-const tptp.sk2 $$unsorted) % 60.23/60.42 (declare-const tptp.neq (-> $$unsorted $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.tl (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.app (-> $$unsorted $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.cons (-> $$unsorted $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf68 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf69 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.geq (-> $$unsorted $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.skaf70 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf71 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf79 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf80 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.rearsegP (-> $$unsorted $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.skaf82 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.nil $$unsorted) % 60.23/60.42 (declare-const tptp.skaf51 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.strictorderedP (-> $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.skaf81 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.totalorderedP (-> $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.skaf59 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf76 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf46 (-> $$unsorted $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.sk1 $$unsorted) % 60.23/60.42 (declare-const tptp.skaf78 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.gt (-> $$unsorted $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.skac2 $$unsorted) % 60.23/60.42 (declare-const tptp.duplicatefreeP (-> $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.skaf60 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.sk3 $$unsorted) % 60.23/60.42 (declare-const tptp.skaf77 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf47 (-> $$unsorted $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.strictorderP (-> $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.totalorderP (-> $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.skaf58 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf75 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf45 (-> $$unsorted $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.cyclefreeP (-> $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.equalelemsP (-> $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.skaf72 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.ssList (-> $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.skaf57 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf74 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf43 (-> $$unsorted $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skac3 $$unsorted) % 60.23/60.42 (declare-const tptp.skaf67 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf66 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf65 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.leq (-> $$unsorted $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.skaf64 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.lt (-> $$unsorted $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.skaf63 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf62 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf61 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.memberP (-> $$unsorted $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.skaf56 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf73 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf42 (-> $$unsorted $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf55 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.ssItem (-> $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.skaf54 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.singletonP (-> $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.skaf53 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf83 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf52 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.hd (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf50 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf49 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf44 (-> $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.skaf48 (-> $$unsorted $$unsorted $$unsorted)) % 60.23/60.42 (declare-const tptp.segmentP (-> $$unsorted $$unsorted Bool)) % 60.23/60.42 (declare-const tptp.frontsegP (-> $$unsorted $$unsorted Bool)) % 60.23/60.42 (define @t1 () (tptp.ssList tptp.nil)) % 60.23/60.42 (define @t2 () (@var "U" $$unsorted)) % 60.23/60.42 (define @t3 () (tptp.skaf83 @t2)) % 60.23/60.42 (define @t4 () (@list @t2)) % 60.23/60.42 (define @t5 () (tptp.skaf82 @t2)) % 60.23/60.42 (define @t6 () (tptp.skaf81 @t2)) % 60.23/60.42 (define @t7 () (tptp.skaf80 @t2)) % 60.23/60.42 (define @t8 () (tptp.skaf79 @t2)) % 60.23/60.42 (define @t9 () (tptp.skaf78 @t2)) % 60.23/60.42 (define @t10 () (tptp.skaf77 @t2)) % 60.23/60.42 (define @t11 () (tptp.skaf76 @t2)) % 60.23/60.42 (define @t12 () (tptp.skaf75 @t2)) % 60.23/60.42 (define @t13 () (tptp.skaf74 @t2)) % 60.23/60.42 (define @t14 () (tptp.skaf73 @t2)) % 60.23/60.42 (define @t15 () (tptp.skaf72 @t2)) % 60.23/60.42 (define @t16 () (tptp.skaf71 @t2)) % 60.23/60.42 (define @t17 () (tptp.skaf70 @t2)) % 60.23/60.42 (define @t18 () (tptp.skaf69 @t2)) % 60.23/60.42 (define @t19 () (tptp.skaf68 @t2)) % 60.23/60.42 (define @t20 () (tptp.skaf67 @t2)) % 60.23/60.42 (define @t21 () (tptp.skaf66 @t2)) % 60.23/60.42 (define @t22 () (tptp.skaf65 @t2)) % 60.23/60.42 (define @t23 () (tptp.skaf64 @t2)) % 60.23/60.42 (define @t24 () (tptp.skaf63 @t2)) % 60.23/60.42 (define @t25 () (tptp.skaf62 @t2)) % 60.23/60.42 (define @t26 () (tptp.skaf61 @t2)) % 60.23/60.42 (define @t27 () (tptp.skaf60 @t2)) % 60.23/60.42 (define @t28 () (tptp.skaf59 @t2)) % 60.23/60.42 (define @t29 () (tptp.skaf58 @t2)) % 60.23/60.42 (define @t30 () (tptp.skaf57 @t2)) % 60.23/60.42 (define @t31 () (tptp.skaf56 @t2)) % 60.23/60.42 (define @t32 () (tptp.skaf55 @t2)) % 60.23/60.42 (define @t33 () (tptp.skaf54 @t2)) % 60.23/60.42 (define @t34 () (tptp.skaf53 @t2)) % 60.23/60.42 (define @t35 () (tptp.skaf52 @t2)) % 60.23/60.42 (define @t36 () (tptp.skaf51 @t2)) % 60.23/60.42 (define @t37 () (tptp.skaf50 @t2)) % 60.23/60.42 (define @t38 () (tptp.skaf49 @t2)) % 60.23/60.42 (define @t39 () (tptp.skaf44 @t2)) % 60.23/60.42 (define @t40 () (@var "V" $$unsorted)) % 60.23/60.42 (define @t41 () (@list @t2 @t40)) % 60.23/60.42 (define @t42 () (tptp.skaf47 @t2 @t40)) % 60.23/60.42 (define @t43 () (tptp.skaf46 @t2 @t40)) % 60.23/60.42 (define @t44 () (tptp.skaf45 @t2 @t40)) % 60.23/60.42 (define @t45 () (tptp.skaf42 @t2 @t40)) % 60.23/60.42 (define @t46 () (not (tptp.ssItem @t2))) % 60.23/60.42 (define @t47 () (not (tptp.ssList @t2))) % 60.23/60.42 (define @t48 () (tptp.cons @t2 tptp.nil)) % 60.23/60.42 (define @t49 () (tptp.ssItem @t40)) % 60.23/60.42 (define @t50 () (tptp.duplicatefreeP @t2)) % 60.23/60.42 (define @t51 () (tptp.app @t2 tptp.nil)) % 60.23/60.42 (define @t52 () (or @t47 (= @t51 @t2))) % 60.23/60.42 (define @t53 () (forall @t4 @t52)) % 60.23/60.42 (define @t54 () (tptp.app tptp.nil @t2)) % 60.23/60.42 (define @t55 () (or @t47 (= @t54 @t2))) % 60.23/60.42 (define @t56 () (forall @t4 @t55)) % 60.23/60.42 (define @t57 () (= tptp.nil @t2)) % 60.23/60.42 (define @t58 () (tptp.tl @t2)) % 60.23/60.42 (define @t59 () (tptp.hd @t2)) % 60.23/60.42 (define @t60 () (tptp.segmentP tptp.nil @t2)) % 60.23/60.42 (define @t61 () (not @t57)) % 60.23/60.42 (define @t62 () (tptp.rearsegP tptp.nil @t2)) % 60.23/60.42 (define @t63 () (tptp.frontsegP tptp.nil @t2)) % 60.23/60.42 (define @t64 () (tptp.app @t40 @t2)) % 60.23/60.42 (define @t65 () (not (tptp.ssList @t40))) % 60.23/60.42 (define @t66 () (tptp.cons @t2 @t40)) % 60.23/60.42 (define @t67 () (tptp.cyclefreeP @t2)) % 60.23/60.42 (define @t68 () (tptp.equalelemsP @t2)) % 60.23/60.42 (define @t69 () (tptp.strictorderedP @t2)) % 60.23/60.42 (define @t70 () (tptp.totalorderedP @t2)) % 60.23/60.42 (define @t71 () (tptp.strictorderP @t2)) % 60.23/60.42 (define @t72 () (tptp.totalorderP @t2)) % 60.23/60.42 (define @t73 () (tptp.tl @t66)) % 60.23/60.42 (define @t74 () (or @t46 @t65 (= @t73 @t40))) % 60.23/60.42 (define @t75 () (forall @t41 @t74)) % 60.23/60.42 (define @t76 () (tptp.hd @t66)) % 60.23/60.42 (define @t77 () (or @t46 @t65 (= @t76 @t2))) % 60.23/60.42 (define @t78 () (forall @t41 @t77)) % 60.23/60.42 (define @t79 () (not (= @t66 tptp.nil))) % 60.23/60.42 (define @t80 () (or @t79 @t46 @t65)) % 60.23/60.42 (define @t81 () (forall @t41 @t80)) % 60.23/60.42 (define @t82 () (= @t40 @t2)) % 60.23/60.42 (define @t83 () (tptp.neq @t40 @t2)) % 60.23/60.42 (define @t84 () (or @t47 @t65 @t83 @t82)) % 60.23/60.42 (define @t85 () (forall @t41 @t84)) % 60.23/60.42 (define @t86 () (tptp.cons @t39 tptp.nil)) % 60.23/60.42 (define @t87 () (not (tptp.singletonP @t2))) % 60.23/60.42 (define @t88 () (or @t87 @t47 (= @t86 @t2))) % 60.23/60.42 (define @t89 () (forall @t4 @t88)) % 60.23/60.42 (define @t90 () (not @t49)) % 60.23/60.42 (define @t91 () (tptp.leq @t2 @t40)) % 60.23/60.42 (define @t92 () (tptp.lt @t2 @t40)) % 60.23/60.42 (define @t93 () (not @t92)) % 60.23/60.42 (define @t94 () (tptp.cons @t59 @t58)) % 60.23/60.42 (define @t95 () (or @t47 (= @t94 @t2) @t57)) % 60.23/60.42 (define @t96 () (forall @t4 @t95)) % 60.23/60.42 (define @t97 () (tptp.lt @t40 @t2)) % 60.23/60.42 (define @t98 () (not (tptp.gt @t2 @t40))) % 60.23/60.42 (define @t99 () (tptp.gt @t40 @t2)) % 60.23/60.42 (define @t100 () (tptp.leq @t40 @t2)) % 60.23/60.42 (define @t101 () (not (tptp.geq @t2 @t40))) % 60.23/60.42 (define @t102 () (tptp.geq @t40 @t2)) % 60.23/60.42 (define @t103 () (not @t91)) % 60.23/60.42 (define @t104 () (tptp.cons @t3 @t5)) % 60.23/60.42 (define @t105 () (or @t47 (= @t104 @t2) @t57)) % 60.23/60.42 (define @t106 () (forall @t4 @t105)) % 60.23/60.42 (define @t107 () (= @t2 @t40)) % 60.23/60.42 (define @t108 () (not @t107)) % 60.23/60.42 (define @t109 () (tptp.cons @t40 @t2)) % 60.23/60.42 (define @t110 () (not (tptp.neq @t2 @t40))) % 60.23/60.42 (define @t111 () (tptp.app @t2 @t40)) % 60.23/60.42 (define @t112 () (= @t111 tptp.nil)) % 60.23/60.42 (define @t113 () (not @t112)) % 60.23/60.42 (define @t114 () (or @t113 @t65 @t47 @t57)) % 60.23/60.42 (define @t115 () (forall @t41 @t114)) % 60.23/60.42 (define @t116 () (= tptp.nil @t40)) % 60.23/60.42 (define @t117 () (or @t113 @t65 @t47 @t116)) % 60.23/60.42 (define @t118 () (forall @t41 @t117)) % 60.23/60.42 (define @t119 () (tptp.app @t48 @t40)) % 60.23/60.42 (define @t120 () (or @t46 @t65 (= @t119 @t66))) % 60.23/60.42 (define @t121 () (forall @t41 @t120)) % 60.23/60.42 (define @t122 () (tptp.hd @t40)) % 60.23/60.42 (define @t123 () (forall @t41 (or @t47 @t65 @t116 (= (tptp.hd @t64) @t122)))) % 60.23/60.42 (define @t124 () (tptp.strictorderedP @t40)) % 60.23/60.42 (define @t125 () (tptp.strictorderedP @t66)) % 60.23/60.42 (define @t126 () (not @t125)) % 60.23/60.42 (define @t127 () (tptp.totalorderedP @t40)) % 60.23/60.42 (define @t128 () (tptp.totalorderedP @t66)) % 60.23/60.42 (define @t129 () (not @t128)) % 60.23/60.42 (define @t130 () (not (tptp.segmentP @t2 @t40))) % 60.23/60.42 (define @t131 () (not (tptp.rearsegP @t2 @t40))) % 60.23/60.42 (define @t132 () (not (tptp.frontsegP @t40 @t2))) % 60.23/60.42 (define @t133 () (not (tptp.frontsegP @t2 @t40))) % 60.23/60.42 (define @t134 () (or @t133 @t132 @t47 @t65 @t82)) % 60.23/60.42 (define @t135 () (forall @t41 @t134)) % 60.23/60.42 (define @t136 () (not @t100)) % 60.23/60.42 (define @t137 () (tptp.app @t40 @t44)) % 60.23/60.42 (define @t138 () (or @t133 @t65 @t47 (= @t137 @t2))) % 60.23/60.42 (define @t139 () (forall @t41 @t138)) % 60.23/60.42 (define @t140 () (tptp.tl @t40)) % 60.23/60.42 (define @t141 () (tptp.lt @t2 @t122)) % 60.23/60.42 (define @t142 () (tptp.leq @t2 @t122)) % 60.23/60.42 (define @t143 () (@var "W" $$unsorted)) % 60.23/60.42 (define @t144 () (tptp.app @t143 @t2)) % 60.23/60.42 (define @t145 () (not (tptp.ssList @t143))) % 60.23/60.42 (define @t146 () (@list @t2 @t40 @t143)) % 60.23/60.42 (define @t147 () (tptp.app @t2 @t143)) % 60.23/60.42 (define @t148 () (tptp.cons @t40 @t143)) % 60.23/60.42 (define @t149 () (tptp.cons @t143 @t2)) % 60.23/60.42 (define @t150 () (not (tptp.ssItem @t143))) % 60.23/60.42 (define @t151 () (not (tptp.memberP @t2 @t40))) % 60.23/60.42 (define @t152 () (not (= @t111 @t143))) % 60.23/60.42 (define @t153 () (tptp.frontsegP @t143 @t2)) % 60.23/60.42 (define @t154 () (or @t152 @t65 @t47 @t145 @t153)) % 60.23/60.42 (define @t155 () (forall @t146 @t154)) % 60.23/60.42 (define @t156 () (tptp.lt @t2 @t143)) % 60.23/60.42 (define @t157 () (not (tptp.lt @t40 @t143))) % 60.23/60.42 (define @t158 () (tptp.app @t143 @t40)) % 60.23/60.42 (define @t159 () (= @t40 @t143)) % 60.23/60.42 (define @t160 () (forall @t146 (or (not (= @t111 @t147)) @t65 @t47 @t145 @t159))) % 60.23/60.42 (define @t161 () (= @t2 @t143)) % 60.23/60.42 (define @t162 () (tptp.memberP @t40 @t143)) % 60.23/60.42 (define @t163 () (@var "X" $$unsorted)) % 60.23/60.42 (define @t164 () (not (tptp.ssList @t163))) % 60.23/60.42 (define @t165 () (tptp.cons @t143 @t163)) % 60.23/60.42 (define @t166 () (not (= @t66 @t165))) % 60.23/60.42 (define @t167 () (@list @t2 @t40 @t143 @t163)) % 60.23/60.42 (define @t168 () (tptp.segmentP @t163 @t40)) % 60.23/60.42 (define @t169 () (tptp.app @t111 @t143)) % 60.23/60.42 (define @t170 () (not (= @t169 @t163))) % 60.23/60.42 (define @t171 () (or @t170 @t145 @t47 @t65 @t164 @t168)) % 60.23/60.42 (define @t172 () (forall @t167 @t171)) % 60.23/60.42 (define @t173 () (not (tptp.frontsegP @t66 @t165))) % 60.23/60.42 (define @t174 () (tptp.app @t2 @t148)) % 60.23/60.42 (define @t175 () (not (tptp.ssItem @t163))) % 60.23/60.42 (define @t176 () (@var "Y" $$unsorted)) % 60.23/60.42 (define @t177 () (not (tptp.ssList @t176))) % 60.23/60.42 (define @t178 () (@list @t2 @t40 @t143 @t163 @t176)) % 60.23/60.42 (define @t179 () (not (tptp.equalelemsP @t176))) % 60.23/60.42 (define @t180 () (tptp.app @t2 (tptp.cons @t40 @t165))) % 60.23/60.42 (define @t181 () (not (= @t180 @t176))) % 60.23/60.42 (define @t182 () (or @t181 @t164 @t47 @t150 @t90 @t179 @t177 @t159)) % 60.23/60.42 (define @t183 () (forall @t178 @t182)) % 60.23/60.42 (define @t184 () (tptp.lt @t40 @t163)) % 60.23/60.42 (define @t185 () (@var "Z" $$unsorted)) % 60.23/60.42 (define @t186 () (not (tptp.ssList @t185))) % 60.23/60.42 (define @t187 () (not (tptp.strictorderedP @t185))) % 60.23/60.42 (define @t188 () (tptp.app @t174 (tptp.cons @t163 @t176))) % 60.23/60.42 (define @t189 () (not (= @t188 @t185))) % 60.23/60.42 (define @t190 () (or @t189 @t177 @t145 @t47 @t175 @t90 @t187 @t186 @t184)) % 60.23/60.42 (define @t191 () (@list @t2 @t40 @t143 @t163 @t176 @t185)) % 60.23/60.42 (define @t192 () (forall @t191 @t190)) % 60.23/60.42 (define @t193 () (tptp.leq @t40 @t163)) % 60.23/60.42 (define @t194 () (tptp.ssList tptp.sk1)) % 60.23/60.42 (define @t195 () (tptp.ssList tptp.sk4)) % 60.23/60.42 (define @t196 () (tptp.segmentP tptp.sk4 tptp.sk3)) % 60.23/60.42 (define @t197 () (tptp.ssItem tptp.sk5)) % 60.23/60.42 (define @t198 () (tptp.ssItem tptp.sk6)) % 60.23/60.42 (define @t199 () (tptp.ssList tptp.sk7)) % 60.23/60.42 (define @t200 () (tptp.ssList tptp.sk8)) % 60.23/60.42 (define @t201 () (tptp.cons tptp.sk6 tptp.nil)) % 60.23/60.42 (define @t202 () (tptp.cons tptp.sk5 tptp.nil)) % 60.23/60.42 (define @t203 () (tptp.app tptp.sk7 @t202)) % 60.23/60.42 (define @t204 () (tptp.app @t203 @t201)) % 60.23/60.42 (define @t205 () (tptp.app @t204 tptp.sk8)) % 60.23/60.42 (define @t206 () (tptp.neq tptp.sk4 tptp.nil)) % 60.23/60.42 (define @t207 () (not @t206)) % 60.23/60.42 (define @t208 () (tptp.singletonP tptp.sk3)) % 60.23/60.42 (define @t209 () (or @t208 @t207)) % 60.23/60.42 (define @t210 () (@list tptp.sk6 tptp.nil)) % 60.23/60.42 (define @t211 () (not @t1)) % 60.23/60.42 (define @t212 () (not @t198)) % 60.23/60.42 (define @t213 () (= tptp.nil @t201)) % 60.23/60.42 (define @t214 () (not @t213)) % 60.23/60.42 (define @t215 () (or @t214 @t212 @t211)) % 60.23/60.42 (define @t216 () (@list false false false)) % 60.23/60.42 (define @t217 () (tptp.ssList @t201)) % 60.23/60.42 (define @t218 () (or @t212 @t211 @t217)) % 60.23/60.42 (define @t219 () (not @t217)) % 60.23/60.42 (define @t220 () (tptp.segmentP tptp.nil @t201)) % 60.23/60.42 (define @t221 () (not @t220)) % 60.23/60.42 (define @t222 () (or @t221 @t219 @t213)) % 60.23/60.42 (define @t223 () (@list false true false)) % 60.23/60.42 (define @t224 () (tptp.segmentP @t169 @t40)) % 60.23/60.42 (define @t225 () (not (tptp.ssList @t169))) % 60.23/60.42 (define @t226 () (not (= @t169 @t169))) % 60.23/60.42 (define @t227 () (or @t226 @t145 @t47 @t65 @t225 @t224)) % 60.23/60.42 (define @t228 () (not (= @t163 @t169))) % 60.23/60.42 (define @t229 () (or @t228 @t228 @t145 @t47 @t65 @t164 @t168)) % 60.23/60.42 (define @t230 () (@list @t163)) % 60.23/60.42 (define @t231 () (or @t228 @t145 @t47 @t65 @t164 @t168)) % 60.23/60.42 (define @t232 () (forall @t230 @t231)) % 60.23/60.42 (define @t233 () (forall @t146 @t232)) % 60.23/60.42 (define @t234 () (@list @t202 tptp.sk7)) % 60.23/60.42 (define @t235 () (@list tptp.sk5 tptp.nil)) % 60.23/60.42 (define @t236 () (tptp.ssList @t202)) % 60.23/60.42 (define @t237 () (not @t197)) % 60.23/60.42 (define @t238 () (or @t237 @t211 @t236)) % 60.23/60.42 (define @t239 () (tptp.ssList @t203)) % 60.23/60.42 (define @t240 () (not @t199)) % 60.23/60.42 (define @t241 () (not @t236)) % 60.23/60.42 (define @t242 () (or @t241 @t240 @t239)) % 60.23/60.42 (define @t243 () (tptp.segmentP @t205 @t201)) % 60.23/60.42 (define @t244 () (tptp.ssList @t205)) % 60.23/60.42 (define @t245 () (not @t244)) % 60.23/60.42 (define @t246 () (not @t239)) % 60.23/60.42 (define @t247 () (not @t200)) % 60.23/60.42 (define @t248 () (or @t247 @t246 @t219 @t245 @t243)) % 60.23/60.42 (define @t249 () (@list false false false false false)) % 60.23/60.42 (define @t250 () (tptp.segmentP tptp.sk4 @t201)) % 60.23/60.42 (define @t251 () (not @t195)) % 60.23/60.42 (define @t252 () (not @t243)) % 60.23/60.42 (define @t253 () (tptp.segmentP tptp.sk4 @t205)) % 60.23/60.42 (define @t254 () (not @t253)) % 60.23/60.42 (define @t255 () (or @t254 @t252 @t219 @t245 @t251 @t250)) % 60.23/60.42 (define @t256 () (@list @t205)) % 60.23/60.42 (define @t257 () (tptp.skaf82 tptp.sk8)) % 60.23/60.42 (define @t258 () (tptp.skaf83 tptp.sk8)) % 60.23/60.42 (define @t259 () (tptp.cons @t258 @t257)) % 60.23/60.42 (define @t260 () (= tptp.sk8 @t259)) % 60.23/60.42 (define @t261 () (tptp.app @t204 @t259)) % 60.23/60.42 (define @t262 () (tptp.ssList @t261)) % 60.23/60.42 (define @t263 () (and @t244 @t260)) % 60.23/60.42 (define @t264 () (tptp.app @t205 tptp.nil)) % 60.23/60.42 (define @t265 () (= @t205 @t264)) % 60.23/60.42 (define @t266 () (or @t245 @t265)) % 60.23/60.42 (define @t267 () (@list false false)) % 60.23/60.42 (define @t268 () (@list @t201 @t203)) % 60.23/60.42 (define @t269 () (tptp.ssList @t204)) % 60.23/60.42 (define @t270 () (or @t219 @t246 @t269)) % 60.23/60.42 (define @t271 () (@list @t203 @t201)) % 60.23/60.42 (define @t272 () (= tptp.nil @t204)) % 60.23/60.42 (define @t273 () (not @t272)) % 60.23/60.42 (define @t274 () (or @t273 @t219 @t246 @t213)) % 60.23/60.42 (define @t275 () (@list false false true false)) % 60.23/60.42 (define @t276 () (not @t269)) % 60.23/60.42 (define @t277 () (= tptp.nil @t205)) % 60.23/60.42 (define @t278 () (not @t277)) % 60.23/60.42 (define @t279 () (or @t278 @t247 @t276 @t272)) % 60.23/60.42 (define @t280 () (@list false true false false)) % 60.23/60.42 (define @t281 () (tptp.skaf82 @t205)) % 60.23/60.42 (define @t282 () (tptp.skaf83 @t205)) % 60.23/60.42 (define @t283 () (tptp.cons @t282 @t281)) % 60.23/60.42 (define @t284 () (= @t205 @t283)) % 60.23/60.42 (define @t285 () (or @t245 @t284 @t277)) % 60.23/60.42 (define @t286 () (tptp.hd @t205)) % 60.23/60.42 (define @t287 () (tptp.ssItem @t286)) % 60.23/60.42 (define @t288 () (or @t245 @t287 @t277)) % 60.23/60.42 (define @t289 () (tptp.cons @t286 tptp.nil)) % 60.23/60.42 (define @t290 () (tptp.app @t289 tptp.nil)) % 60.23/60.42 (define @t291 () (= @t289 @t290)) % 60.23/60.42 (define @t292 () (not @t287)) % 60.23/60.42 (define @t293 () (or @t292 @t211 @t291)) % 60.23/60.42 (define @t294 () (@list @t282 @t281)) % 60.23/60.42 (define @t295 () (tptp.cons @t282 tptp.nil)) % 60.23/60.42 (define @t296 () (tptp.app @t295 @t281)) % 60.23/60.42 (define @t297 () (= @t283 @t296)) % 60.23/60.42 (define @t298 () (tptp.ssList @t281)) % 60.23/60.42 (define @t299 () (not @t298)) % 60.23/60.42 (define @t300 () (tptp.ssItem @t282)) % 60.23/60.42 (define @t301 () (not @t300)) % 60.23/60.42 (define @t302 () (or @t301 @t299 @t297)) % 60.23/60.42 (define @t303 () (tptp.tl @t283)) % 60.23/60.42 (define @t304 () (= @t281 @t303)) % 60.23/60.42 (define @t305 () (or @t301 @t299 @t304)) % 60.23/60.42 (define @t306 () (tptp.hd @t283)) % 60.23/60.42 (define @t307 () (= @t282 @t306)) % 60.23/60.42 (define @t308 () (or @t301 @t299 @t307)) % 60.23/60.42 (define @t309 () (@list @t286)) % 60.23/60.42 (define @t310 () (tptp.strictorderedP @t289)) % 60.23/60.42 (define @t311 () (or @t292 @t310)) % 60.23/60.42 (define @t312 () (tptp.skaf44 @t205)) % 60.23/60.42 (define @t313 () (tptp.cons @t312 tptp.nil)) % 60.23/60.42 (define @t314 () (tptp.tl @t313)) % 60.23/60.42 (define @t315 () (= tptp.nil @t314)) % 60.23/60.42 (define @t316 () (tptp.ssItem @t312)) % 60.23/60.42 (define @t317 () (not @t316)) % 60.23/60.42 (define @t318 () (or @t317 @t211 @t315)) % 60.23/60.42 (define @t319 () (= @t205 @t313)) % 60.23/60.42 (define @t320 () (tptp.tl @t264)) % 60.23/60.42 (define @t321 () (tptp.tl @t205)) % 60.23/60.42 (define @t322 () (tptp.app @t289 @t321)) % 60.23/60.42 (define @t323 () (tptp.hd @t264)) % 60.23/60.42 (define @t324 () (tptp.strictorderedP @t261)) % 60.23/60.42 (define @t325 () (and @t265 @t319 @t260 @t284 @t297 @t291 @t310 @t315 @t304 @t307)) % 60.23/60.42 (define @t326 () (not @t307)) % 60.23/60.42 (define @t327 () (not @t304)) % 60.23/60.42 (define @t328 () (not @t315)) % 60.23/60.42 (define @t329 () (not @t291)) % 60.23/60.42 (define @t330 () (not @t297)) % 60.23/60.42 (define @t331 () (not @t284)) % 60.23/60.42 (define @t332 () (not @t260)) % 60.23/60.42 (define @t333 () (not @t319)) % 60.23/60.42 (define @t334 () (not @t265)) % 60.23/60.42 (define @t335 () (tptp.app @t201 tptp.sk8)) % 60.23/60.42 (define @t336 () (= @t205 (tptp.app @t203 @t335))) % 60.23/60.42 (define @t337 () (or @t247 @t219 @t246 @t336)) % 60.23/60.42 (define @t338 () (@list false false false false)) % 60.23/60.42 (define @t339 () (= (tptp.cons tptp.sk6 tptp.sk8) @t335)) % 60.23/60.42 (define @t340 () (or @t212 @t247 @t339)) % 60.23/60.42 (define @t341 () (tptp.equalelemsP @t289)) % 60.23/60.42 (define @t342 () (or @t292 @t341)) % 60.23/60.42 (define @t343 () (tptp.cons tptp.sk6 @t259)) % 60.23/60.42 (define @t344 () (tptp.app @t203 @t343)) % 60.23/60.42 (define @t345 () (tptp.equalelemsP @t344)) % 60.23/60.42 (define @t346 () (and @t265 @t319 @t260 @t284 @t336 @t339 @t297 @t291 @t341 @t315 @t304 @t307)) % 60.23/60.42 (define @t347 () (tptp.ssList @t344)) % 60.23/60.42 (define @t348 () (and @t244 @t260 @t336 @t339)) % 60.23/60.42 (define @t349 () (@list tptp.sk8)) % 60.23/60.42 (define @t350 () (not (tptp.ssList @t188))) % 60.23/60.42 (define @t351 () (not (tptp.strictorderedP @t188))) % 60.23/60.42 (define @t352 () (not (= @t188 @t188))) % 60.23/60.42 (define @t353 () (or @t352 @t177 @t145 @t47 @t175 @t90 @t351 @t350 @t184)) % 60.23/60.42 (define @t354 () (not (= @t185 @t188))) % 60.23/60.42 (define @t355 () (or @t354 @t354 @t177 @t145 @t47 @t175 @t90 @t187 @t186 @t184)) % 60.23/60.42 (define @t356 () (@list @t185)) % 60.23/60.42 (define @t357 () (or @t354 @t177 @t145 @t47 @t175 @t90 @t187 @t186 @t184)) % 60.23/60.42 (define @t358 () (forall @t356 @t357)) % 60.23/60.42 (define @t359 () (forall @t178 @t358)) % 60.23/60.42 (define @t360 () (tptp.lt tptp.sk6 @t258)) % 60.23/60.42 (define @t361 () (not @t262)) % 60.23/60.42 (define @t362 () (not @t324)) % 60.23/60.42 (define @t363 () (tptp.ssItem @t258)) % 60.23/60.42 (define @t364 () (not @t363)) % 60.23/60.42 (define @t365 () (tptp.ssList @t257)) % 60.23/60.42 (define @t366 () (not @t365)) % 60.23/60.42 (define @t367 () (or @t366 @t211 @t246 @t364 @t212 @t362 @t361 @t360)) % 60.23/60.42 (define @t368 () (not (tptp.ssList @t180))) % 60.23/60.42 (define @t369 () (not (tptp.equalelemsP @t180))) % 60.23/60.42 (define @t370 () (not (= @t180 @t180))) % 60.23/60.42 (define @t371 () (or @t370 @t164 @t47 @t150 @t90 @t369 @t368 @t159)) % 60.23/60.42 (define @t372 () (not (= @t176 @t180))) % 60.23/60.42 (define @t373 () (or @t372 @t372 @t164 @t47 @t150 @t90 @t179 @t177 @t159)) % 60.23/60.42 (define @t374 () (@list @t176)) % 60.23/60.42 (define @t375 () (or @t372 @t164 @t47 @t150 @t90 @t179 @t177 @t159)) % 60.23/60.42 (define @t376 () (forall @t374 @t375)) % 60.23/60.42 (define @t377 () (forall @t167 @t376)) % 60.23/60.42 (define @t378 () (= tptp.sk6 @t258)) % 60.23/60.42 (define @t379 () (not @t347)) % 60.23/60.42 (define @t380 () (not @t345)) % 60.23/60.42 (define @t381 () (or @t366 @t246 @t364 @t212 @t380 @t379 @t378)) % 60.23/60.42 (define @t382 () (tptp.lt tptp.sk6 tptp.sk6)) % 60.23/60.42 (define @t383 () (not @t382)) % 60.23/60.42 (define @t384 () (or @t383 @t212)) % 60.23/60.42 (define @t385 () (= @t258 (tptp.hd @t259))) % 60.23/60.42 (define @t386 () (or @t364 @t366 @t385)) % 60.23/60.42 (define @t387 () (not @t360)) % 60.23/60.42 (define @t388 () (not @t378)) % 60.23/60.42 (define @t389 () (not @t385)) % 60.23/60.42 (define @t390 () (= false true)) % 60.23/60.42 (define @t391 () (tptp.hd tptp.sk8)) % 60.23/60.42 (define @t392 () (and @t360 @t385 @t260 @t378 @t383)) % 60.23/60.42 (define @t393 () (= tptp.nil tptp.sk8)) % 60.23/60.42 (define @t394 () (or @t247 @t260 @t393)) % 60.23/60.42 (define @t395 () (forall @t4 (or @t47 (= @t2 @t104) @t57))) % 60.23/60.42 (define @t396 () (@list tptp.sk7)) % 60.23/60.42 (define @t397 () (= tptp.nil tptp.sk7)) % 60.23/60.42 (define @t398 () (tptp.skaf82 tptp.sk7)) % 60.23/60.42 (define @t399 () (tptp.skaf83 tptp.sk7)) % 60.23/60.42 (define @t400 () (tptp.cons @t399 @t398)) % 60.23/60.42 (define @t401 () (= tptp.sk7 @t400)) % 60.23/60.42 (define @t402 () (or @t240 @t401 @t397)) % 60.23/60.42 (define @t403 () (tptp.hd @t203)) % 60.23/60.42 (define @t404 () (tptp.hd tptp.sk7)) % 60.23/60.42 (define @t405 () (or @t241 @t240 @t397 (= @t403 @t404))) % 60.23/60.42 (define @t406 () (= @t404 @t403)) % 60.23/60.42 (define @t407 () (or @t241 @t240 @t397 @t406)) % 60.23/60.42 (define @t408 () (@list false)) % 60.23/60.42 (define @t409 () (@list @t123)) % 60.23/60.42 (define @t410 () (= tptp.sk7 (tptp.app tptp.nil tptp.sk7))) % 60.23/60.42 (define @t411 () (or @t240 @t410)) % 60.23/60.42 (define @t412 () (@list tptp.sk8 tptp.sk8)) % 60.23/60.42 (define @t413 () (tptp.frontsegP tptp.sk8 tptp.sk8)) % 60.23/60.42 (define @t414 () (or @t247 @t413)) % 60.23/60.42 (define @t415 () (tptp.skaf45 tptp.sk8 tptp.sk8)) % 60.23/60.42 (define @t416 () (tptp.app tptp.sk8 @t415)) % 60.23/60.42 (define @t417 () (= tptp.sk8 @t416)) % 60.23/60.42 (define @t418 () (not @t413)) % 60.23/60.42 (define @t419 () (or @t418 @t247 @t247 @t417)) % 60.23/60.42 (define @t420 () (@list @t399 @t398)) % 60.23/60.42 (define @t421 () (= @t398 (tptp.tl @t400))) % 60.23/60.42 (define @t422 () (tptp.ssList @t398)) % 60.23/60.42 (define @t423 () (not @t422)) % 60.23/60.42 (define @t424 () (tptp.ssItem @t399)) % 60.23/60.42 (define @t425 () (not @t424)) % 60.23/60.42 (define @t426 () (or @t425 @t423 @t421)) % 60.23/60.42 (define @t427 () (tptp.app @t415 tptp.sk7)) % 60.23/60.42 (define @t428 () (tptp.app tptp.sk8 @t427)) % 60.23/60.42 (define @t429 () (= (tptp.app @t416 tptp.sk7) @t428)) % 60.23/60.42 (define @t430 () (tptp.ssList @t415)) % 60.23/60.42 (define @t431 () (not @t430)) % 60.23/60.42 (define @t432 () (or @t240 @t431 @t247 @t429)) % 60.23/60.42 (define @t433 () (tptp.app tptp.sk8 tptp.nil)) % 60.23/60.42 (define @t434 () (not (= @t416 @t433))) % 60.23/60.42 (define @t435 () (or @t434 @t431 @t247 @t211 (= @t415 tptp.nil))) % 60.23/60.42 (define @t436 () (= tptp.nil @t415)) % 60.23/60.42 (define @t437 () (= @t433 @t416)) % 60.23/60.42 (define @t438 () (not @t437)) % 60.23/60.42 (define @t439 () (or @t438 @t431 @t247 @t211 @t436)) % 60.23/60.42 (define @t440 () (@list @t160)) % 60.23/60.42 (define @t441 () (= tptp.sk8 @t433)) % 60.23/60.42 (define @t442 () (or @t247 @t441)) % 60.23/60.42 (define @t443 () (tptp.tl tptp.sk7)) % 60.23/60.42 (define @t444 () (tptp.app tptp.sk8 tptp.sk7)) % 60.23/60.42 (define @t445 () (tptp.tl @t444)) % 60.23/60.42 (define @t446 () (tptp.ssList @t445)) % 60.23/60.42 (define @t447 () (and @t410 @t393 @t401 @t417 @t422 @t436 @t421 @t429)) % 60.23/60.42 (define @t448 () (not @t429)) % 60.23/60.42 (define @t449 () (not @t421)) % 60.23/60.42 (define @t450 () (not @t436)) % 60.23/60.42 (define @t451 () (not @t417)) % 60.23/60.42 (define @t452 () (not @t401)) % 60.23/60.42 (define @t453 () (not @t393)) % 60.23/60.42 (define @t454 () (not @t410)) % 60.23/60.42 (define @t455 () (tptp.app @t202 @t201)) % 60.23/60.42 (define @t456 () (tptp.app tptp.sk7 @t455)) % 60.23/60.42 (define @t457 () (= @t204 @t456)) % 60.23/60.42 (define @t458 () (or @t219 @t241 @t240 @t457)) % 60.23/60.42 (define @t459 () (tptp.hd @t204)) % 60.23/60.42 (define @t460 () (= tptp.nil @t203)) % 60.23/60.42 (define @t461 () (or @t219 @t246 @t460 (= @t459 @t403))) % 60.23/60.42 (define @t462 () (= @t403 @t459)) % 60.23/60.42 (define @t463 () (or @t219 @t246 @t460 @t462)) % 60.23/60.42 (define @t464 () (@list tptp.sk7 @t202)) % 60.23/60.42 (define @t465 () (= tptp.nil @t202)) % 60.23/60.42 (define @t466 () (not @t465)) % 60.23/60.42 (define @t467 () (or @t466 @t237 @t211)) % 60.23/60.42 (define @t468 () (not @t460)) % 60.23/60.42 (define @t469 () (or @t468 @t241 @t240 @t465)) % 60.23/60.42 (define @t470 () (= @t286 @t459)) % 60.23/60.42 (define @t471 () (or @t247 @t276 @t272 @t470)) % 60.23/60.42 (define @t472 () (= @t400 (tptp.app (tptp.cons @t399 tptp.nil) @t398))) % 60.23/60.42 (define @t473 () (or @t425 @t423 @t472)) % 60.23/60.42 (define @t474 () (= @t399 (tptp.hd @t400))) % 60.23/60.42 (define @t475 () (or @t425 @t423 @t474)) % 60.23/60.42 (define @t476 () (tptp.app @t204 tptp.nil)) % 60.23/60.42 (define @t477 () (= @t204 @t476)) % 60.23/60.42 (define @t478 () (or @t276 @t477)) % 60.23/60.42 (define @t479 () (tptp.frontsegP tptp.sk7 @t203)) % 60.23/60.42 (define @t480 () (not @t479)) % 60.23/60.42 (define @t481 () (tptp.frontsegP @t203 tptp.sk7)) % 60.23/60.42 (define @t482 () (not @t481)) % 60.23/60.42 (define @t483 () (or @t482 @t480 @t246 @t240 (= @t203 tptp.sk7))) % 60.23/60.42 (define @t484 () (forall @t41 (or @t133 @t132 @t47 @t65 @t107))) % 60.23/60.42 (define @t485 () (= tptp.sk7 @t203)) % 60.23/60.42 (define @t486 () (or @t482 @t480 @t246 @t240 @t485)) % 60.23/60.42 (define @t487 () (tptp.app tptp.sk7 tptp.nil)) % 60.23/60.42 (define @t488 () (not (= @t487 @t203))) % 60.23/60.42 (define @t489 () (or @t488 @t211 @t240 @t241 @t465)) % 60.23/60.42 (define @t490 () (= @t203 @t487)) % 60.23/60.42 (define @t491 () (not @t490)) % 60.23/60.42 (define @t492 () (or @t491 @t211 @t240 @t241 @t465)) % 60.23/60.42 (define @t493 () (@list false false false true false)) % 60.23/60.42 (define @t494 () (= tptp.sk7 @t487)) % 60.23/60.42 (define @t495 () (or @t240 @t494)) % 60.23/60.42 (define @t496 () (not @t485)) % 60.23/60.42 (define @t497 () (not @t494)) % 60.23/60.42 (define @t498 () (and @t494 @t485 @t491)) % 60.23/60.42 (define @t499 () (tptp.frontsegP @t111 @t2)) % 60.23/60.42 (define @t500 () (not (tptp.ssList @t111))) % 60.23/60.42 (define @t501 () (not (= @t111 @t111))) % 60.23/60.42 (define @t502 () (or @t501 @t65 @t47 @t500 @t499)) % 60.23/60.42 (define @t503 () (@list @t143)) % 60.23/60.42 (define @t504 () (or @t152 @t152 @t65 @t47 @t145 @t153)) % 60.23/60.42 (define @t505 () (forall @t503 @t154)) % 60.23/60.42 (define @t506 () (forall @t41 @t505)) % 60.23/60.42 (define @t507 () (or @t241 @t240 @t246 @t481)) % 60.23/60.42 (define @t508 () (tptp.app @t204 @t445)) % 60.23/60.42 (define @t509 () (tptp.frontsegP @t508 @t203)) % 60.23/60.42 (define @t510 () (not @t509)) % 60.23/60.42 (define @t511 () (not @t474)) % 60.23/60.42 (define @t512 () (not @t477)) % 60.23/60.42 (define @t513 () (not @t472)) % 60.23/60.42 (define @t514 () (not @t457)) % 60.23/60.42 (define @t515 () (not @t470)) % 60.23/60.42 (define @t516 () (not @t462)) % 60.23/60.42 (define @t517 () (not @t406)) % 60.23/60.42 (define @t518 () (tptp.app @t456 tptp.sk8)) % 60.23/60.42 (define @t519 () (and @t265 @t410 @t393 @t319 @t401 @t284 @t406 @t462 @t470 @t417 @t457 @t436 @t472 @t297 @t291 @t477 @t315 @t421 @t304 @t474 @t307 @t480 @t429)) % 60.23/60.42 (define @t520 () (tptp.frontsegP @t204 @t203)) % 60.23/60.42 (define @t521 () (or @t219 @t246 @t276 @t520)) % 60.23/60.42 (define @t522 () (not @t446)) % 60.23/60.42 (define @t523 () (not @t520)) % 60.23/60.42 (define @t524 () (or @t523 @t522 @t246 @t276 @t509)) % 60.23/60.42 (define @t525 () (= tptp.nil (tptp.tl @t202))) % 60.23/60.42 (define @t526 () (or @t237 @t211 @t525)) % 60.23/60.42 (define @t527 () (tptp.tl (tptp.cons tptp.sk6 tptp.sk7))) % 60.23/60.42 (define @t528 () (= tptp.sk7 @t527)) % 60.23/60.42 (define @t529 () (or @t212 @t240 @t528)) % 60.23/60.42 (define @t530 () (tptp.app @t202 tptp.nil)) % 60.23/60.42 (define @t531 () (= @t202 @t530)) % 60.23/60.42 (define @t532 () (or @t237 @t211 @t531)) % 60.23/60.42 (define @t533 () (tptp.app @t201 tptp.nil)) % 60.23/60.42 (define @t534 () (= @t201 @t533)) % 60.23/60.42 (define @t535 () (or @t212 @t211 @t534)) % 60.23/60.42 (define @t536 () (= @t530 @t455)) % 60.23/60.42 (define @t537 () (not @t536)) % 60.23/60.42 (define @t538 () (or @t537 @t211 @t241 @t219 @t213)) % 60.23/60.42 (define @t539 () (= @t202 (tptp.app tptp.nil @t202))) % 60.23/60.42 (define @t540 () (or @t241 @t539)) % 60.23/60.42 (define @t541 () (tptp.tl @t203)) % 60.23/60.42 (define @t542 () (tptp.cons @t403 @t541)) % 60.23/60.42 (define @t543 () (= @t203 @t542)) % 60.23/60.42 (define @t544 () (or @t246 @t543 @t460)) % 60.23/60.42 (define @t545 () (and @t265 @t397 @t393 @t525 @t528 @t319 @t284 @t531 @t534 @t462 @t470 @t457 @t297 @t291 @t477 @t539 @t315 @t304 @t307 @t543)) % 60.23/60.42 (define @t546 () (tptp.singletonP @t205)) % 60.23/60.42 (define @t547 () (not @t546)) % 60.23/60.42 (define @t548 () (or @t547 @t245 @t319)) % 60.23/60.42 (define @t549 () (= tptp.nil tptp.sk4)) % 60.23/60.42 (define @t550 () (or @t211 @t251 @t206 @t549)) % 60.23/60.42 (define @t551 () (not @t250)) % 60.23/60.42 (define @t552 () (not @t549)) % 60.23/60.42 (define @t553 () (and @t221 @t549 @t250)) % 60.23/60.42 (assume @p1 (tptp.equalelemsP tptp.nil)) % 60.23/60.42 (assume @p2 (tptp.duplicatefreeP tptp.nil)) % 60.23/60.42 (assume @p3 (tptp.strictorderedP tptp.nil)) % 60.23/60.42 (assume @p4 (tptp.totalorderedP tptp.nil)) % 60.23/60.42 (assume @p5 (tptp.strictorderP tptp.nil)) % 60.23/60.42 (assume @p6 (tptp.totalorderP tptp.nil)) % 60.23/60.42 (assume @p7 (tptp.cyclefreeP tptp.nil)) % 60.23/60.42 (assume @p8 @t1) % 60.23/60.42 (assume @p9 (tptp.ssItem tptp.skac3)) % 60.23/60.42 (assume @p10 (tptp.ssItem tptp.skac2)) % 60.23/60.42 (assume @p11 (not (tptp.singletonP tptp.nil))) % 60.23/60.42 (assume @p12 (forall @t4 (tptp.ssItem @t3))) % 60.23/60.42 (assume @p13 (forall @t4 (tptp.ssList @t5))) % 60.23/60.42 (assume @p14 (forall @t4 (tptp.ssList @t6))) % 60.23/60.42 (assume @p15 (forall @t4 (tptp.ssList @t7))) % 60.23/60.42 (assume @p16 (forall @t4 (tptp.ssItem @t8))) % 60.23/60.42 (assume @p17 (forall @t4 (tptp.ssItem @t9))) % 60.23/60.42 (assume @p18 (forall @t4 (tptp.ssList @t10))) % 60.23/60.42 (assume @p19 (forall @t4 (tptp.ssList @t11))) % 60.23/60.42 (assume @p20 (forall @t4 (tptp.ssList @t12))) % 60.23/60.42 (assume @p21 (forall @t4 (tptp.ssItem @t13))) % 60.23/60.42 (assume @p22 (forall @t4 (tptp.ssList @t14))) % 60.23/60.42 (assume @p23 (forall @t4 (tptp.ssList @t15))) % 60.23/60.42 (assume @p24 (forall @t4 (tptp.ssList @t16))) % 60.23/60.42 (assume @p25 (forall @t4 (tptp.ssItem @t17))) % 60.23/60.42 (assume @p26 (forall @t4 (tptp.ssItem @t18))) % 60.23/60.42 (assume @p27 (forall @t4 (tptp.ssList @t19))) % 60.23/60.42 (assume @p28 (forall @t4 (tptp.ssList @t20))) % 60.23/60.42 (assume @p29 (forall @t4 (tptp.ssList @t21))) % 60.23/60.42 (assume @p30 (forall @t4 (tptp.ssItem @t22))) % 60.23/60.42 (assume @p31 (forall @t4 (tptp.ssItem @t23))) % 60.23/60.42 (assume @p32 (forall @t4 (tptp.ssList @t24))) % 60.23/60.42 (assume @p33 (forall @t4 (tptp.ssList @t25))) % 60.23/60.42 (assume @p34 (forall @t4 (tptp.ssList @t26))) % 60.23/60.42 (assume @p35 (forall @t4 (tptp.ssItem @t27))) % 60.23/60.42 (assume @p36 (forall @t4 (tptp.ssItem @t28))) % 60.23/60.42 (assume @p37 (forall @t4 (tptp.ssList @t29))) % 60.23/60.42 (assume @p38 (forall @t4 (tptp.ssList @t30))) % 60.23/60.42 (assume @p39 (forall @t4 (tptp.ssList @t31))) % 60.23/60.42 (assume @p40 (forall @t4 (tptp.ssItem @t32))) % 60.23/60.42 (assume @p41 (forall @t4 (tptp.ssItem @t33))) % 60.23/60.42 (assume @p42 (forall @t4 (tptp.ssList @t34))) % 60.23/60.42 (assume @p43 (forall @t4 (tptp.ssList @t35))) % 60.23/60.42 (assume @p44 (forall @t4 (tptp.ssList @t36))) % 60.23/60.42 (assume @p45 (forall @t4 (tptp.ssItem @t37))) % 60.23/60.42 (assume @p46 (forall @t4 (tptp.ssItem @t38))) % 60.23/60.42 (assume @p47 (forall @t4 (tptp.ssItem @t39))) % 60.23/60.42 (assume @p48 (forall @t41 (tptp.ssList (tptp.skaf48 @t2 @t40)))) % 60.23/60.42 (assume @p49 (forall @t41 (tptp.ssList @t42))) % 60.23/60.42 (assume @p50 (forall @t41 (tptp.ssList @t43))) % 60.23/60.42 (assume @p51 (forall @t41 (tptp.ssList @t44))) % 60.23/60.42 (assume @p52 (forall @t41 (tptp.ssList (tptp.skaf43 @t2 @t40)))) % 60.23/60.42 (assume @p53 (forall @t41 (tptp.ssList @t45))) % 60.23/60.42 (assume @p54 (not (= tptp.skac3 tptp.skac2))) % 60.23/60.42 (assume @p55 (forall @t4 (or @t46 (tptp.geq @t2 @t2)))) % 60.23/60.42 (assume @p56 (forall @t4 (or @t47 (tptp.segmentP @t2 tptp.nil)))) % 60.23/60.42 (assume @p57 (forall @t4 (or @t47 (tptp.segmentP @t2 @t2)))) % 60.23/60.42 (assume @p58 (forall @t4 (or @t47 (tptp.rearsegP @t2 tptp.nil)))) % 60.23/60.42 (assume @p59 (forall @t4 (or @t47 (tptp.rearsegP @t2 @t2)))) % 60.23/60.42 (assume @p60 (forall @t4 (or @t47 (tptp.frontsegP @t2 tptp.nil)))) % 60.23/60.42 (assume @p61 (forall @t4 (or @t47 (tptp.frontsegP @t2 @t2)))) % 60.23/60.42 (assume @p62 (forall @t4 (or @t46 (tptp.leq @t2 @t2)))) % 60.23/60.42 (assume @p63 (forall @t4 (or (not (tptp.lt @t2 @t2)) @t46))) % 60.23/60.42 (assume @p64 (forall @t4 (or @t46 (tptp.equalelemsP @t48)))) % 60.23/60.42 (assume @p65 (forall @t4 (or @t46 (tptp.duplicatefreeP @t48)))) % 60.23/60.42 (assume @p66 (forall @t4 (or @t46 (tptp.strictorderedP @t48)))) % 60.23/60.42 (assume @p67 (forall @t4 (or @t46 (tptp.totalorderedP @t48)))) % 60.23/60.42 (assume @p68 (forall @t4 (or @t46 (tptp.strictorderP @t48)))) % 60.23/60.42 (assume @p69 (forall @t4 (or @t46 (tptp.totalorderP @t48)))) % 60.23/60.42 (assume @p70 (forall @t4 (or @t46 (tptp.cyclefreeP @t48)))) % 60.23/60.42 (assume @p71 (forall @t4 (or (not (tptp.memberP tptp.nil @t2)) @t46))) % 60.23/60.42 (assume @p72 (forall @t41 (or @t47 @t50 @t49))) % 60.23/60.42 (assume @p73 @t53) % 60.23/60.42 (assume @p74 @t56) % 60.23/60.42 (assume @p75 (forall @t4 (or @t47 (tptp.ssList @t58) @t57))) % 60.23/60.42 (assume @p76 (forall @t4 (or @t47 (tptp.ssItem @t59) @t57))) % 60.23/60.42 (assume @p77 (forall @t4 (or @t61 @t47 @t60))) % 60.23/60.42 (assume @p78 (forall @t4 (or (not @t60) @t47 @t57))) % 60.23/60.42 (assume @p79 (forall @t4 (or @t61 @t47 @t62))) % 60.23/60.42 (assume @p80 (forall @t4 (or (not @t62) @t47 @t57))) % 60.23/60.42 (assume @p81 (forall @t4 (or @t61 @t47 @t63))) % 60.23/60.42 (assume @p82 (forall @t4 (or (not @t63) @t47 @t57))) % 60.23/60.42 (assume @p83 (forall @t41 (or @t47 @t65 (tptp.ssList @t64)))) % 60.23/60.42 (assume @p84 (forall @t41 (or @t46 @t65 (tptp.ssList @t66)))) % 60.23/60.42 (assume @p85 (forall @t4 (or @t47 @t67 (tptp.leq @t37 @t38)))) % 60.23/60.42 (assume @p86 (forall @t4 (or @t47 @t67 (tptp.leq @t38 @t37)))) % 60.23/60.42 (assume @p87 (forall @t4 (or (not (= @t8 @t9)) @t47 @t68))) % 60.23/60.42 (assume @p88 (forall @t4 (or (not (tptp.lt @t18 @t17)) @t47 @t69))) % 60.23/60.42 (assume @p89 (forall @t4 (or (not (tptp.leq @t23 @t22)) @t47 @t70))) % 60.23/60.42 (assume @p90 (forall @t4 (or (not (tptp.lt @t27 @t28)) @t47 @t71))) % 60.23/60.42 (assume @p91 (forall @t4 (or (not (tptp.lt @t28 @t27)) @t47 @t71))) % 60.23/60.42 (assume @p92 (forall @t4 (or (not (tptp.leq @t32 @t33)) @t47 @t72))) % 60.23/60.42 (assume @p93 (forall @t4 (or (not (tptp.leq @t33 @t32)) @t47 @t72))) % 60.23/60.42 (assume @p94 @t75) % 60.23/60.42 (assume @p95 @t78) % 60.23/60.42 (assume @p96 @t81) % 60.23/60.42 (assume @p97 (forall @t41 (or (not (= @t66 @t40)) @t46 @t65))) % 60.23/60.42 (assume @p98 @t85) % 60.23/60.42 (assume @p99 @t89) % 60.23/60.42 (assume @p100 (forall @t41 (or @t46 @t90 @t83 @t82))) % 60.23/60.42 (assume @p101 (forall @t41 (or @t93 @t90 @t46 @t91))) % 60.23/60.42 (assume @p102 @t96) % 60.23/60.42 (assume @p103 (forall @t41 (or @t98 @t90 @t46 @t97))) % 60.23/60.42 (assume @p104 (forall @t41 (or @t93 @t46 @t90 @t99))) % 60.23/60.42 (assume @p105 (forall @t41 (or @t101 @t90 @t46 @t100))) % 60.23/60.42 (assume @p106 (forall @t41 (or @t103 @t46 @t90 @t102))) % 60.23/60.42 (assume @p107 @t106) % 60.23/60.42 (assume @p108 (forall @t41 (or @t98 (not @t99) @t46 @t90))) % 60.23/60.42 (assume @p109 (forall @t41 (or @t108 @t93 @t90 @t46))) % 60.23/60.42 (assume @p110 (forall @t41 (or @t61 @t47 @t90 (tptp.strictorderedP @t109)))) % 60.23/60.42 (assume @p111 (forall @t41 (or @t61 @t47 @t90 (tptp.totalorderedP @t109)))) % 60.23/60.42 (assume @p112 (forall @t41 (or @t93 (not @t97) @t46 @t90))) % 60.23/60.42 (assume @p113 (forall @t41 (or @t108 @t110 @t65 @t47))) % 60.23/60.42 (assume @p114 (forall @t41 (or (not (= @t48 @t40)) @t46 @t65 (tptp.singletonP @t40)))) % 60.23/60.42 (assume @p115 (forall @t41 (or @t108 @t110 @t90 @t46))) % 60.23/60.42 (assume @p116 @t115) % 60.23/60.42 (assume @p117 @t118) % 60.23/60.42 (assume @p118 @t121) % 60.23/60.42 (assume @p119 (forall @t41 (or @t103 @t90 @t46 @t92 @t107))) % 60.23/60.42 (assume @p120 @t123) % 60.23/60.42 (assume @p121 (forall @t41 (or @t126 @t65 @t46 @t124 @t116))) % 60.23/60.42 (assume @p122 (forall @t41 (or @t129 @t65 @t46 @t127 @t116))) % 60.23/60.42 (assume @p123 (forall @t41 (or @t101 (not @t102) @t46 @t90 @t82))) % 60.23/60.42 (assume @p124 (forall @t41 (or @t130 (not (tptp.segmentP @t40 @t2)) @t47 @t65 @t82))) % 60.23/60.42 (assume @p125 (forall @t41 (or @t131 (not (tptp.rearsegP @t40 @t2)) @t47 @t65 @t82))) % 60.23/60.42 (assume @p126 @t135) % 60.23/60.42 (assume @p127 (forall @t41 (or @t103 @t136 @t46 @t90 @t82))) % 60.23/60.42 (assume @p128 (forall @t41 (or @t131 @t65 @t47 (= (tptp.app @t43 @t40) @t2)))) % 60.23/60.42 (assume @p129 @t139) % 60.23/60.42 (assume @p130 (forall @t41 (or @t47 @t65 @t116 (= (tptp.tl @t64) (tptp.app @t140 @t2))))) % 60.23/60.42 (assume @p131 (forall @t41 (or @t126 @t65 @t46 @t141 @t116))) % 60.23/60.42 (assume @p132 (forall @t41 (or @t129 @t65 @t46 @t142 @t116))) % 60.23/60.42 (assume @p133 (forall @t146 (or @t131 @t145 @t65 @t47 (tptp.rearsegP @t144 @t40)))) % 60.23/60.42 (assume @p134 (forall @t146 (or @t133 @t145 @t65 @t47 (tptp.frontsegP @t147 @t40)))) % 60.23/60.42 (assume @p135 (forall @t146 (or @t108 @t145 @t90 @t46 (tptp.memberP @t148 @t2)))) % 60.23/60.42 (assume @p136 (forall @t146 (or @t151 @t47 @t150 @t90 (tptp.memberP @t149 @t40)))) % 60.23/60.42 (assume @p137 (forall @t146 (or @t151 @t145 @t47 @t90 (tptp.memberP @t147 @t40)))) % 60.23/60.42 (assume @p138 (forall @t146 (or @t151 @t47 @t145 @t90 (tptp.memberP @t144 @t40)))) % 60.23/60.42 (assume @p139 (forall @t4 (or @t47 @t68 (= (tptp.app @t7 (tptp.cons @t9 (tptp.cons @t8 @t6))) @t2)))) % 60.23/60.42 (assume @p140 (forall @t146 (or @t152 @t47 @t65 @t145 (tptp.rearsegP @t143 @t40)))) % 60.23/60.42 (assume @p141 @t155) % 60.23/60.42 (assume @p142 (forall @t41 (or @t61 (not @t116) @t65 @t47 @t112))) % 60.23/60.42 (assume @p143 (forall @t146 (or @t98 (not (tptp.gt @t40 @t143)) @t150 @t90 @t46 (tptp.gt @t2 @t143)))) % 60.23/60.42 (assume @p144 (forall @t146 (or @t103 @t157 @t150 @t90 @t46 @t156))) % 60.23/60.42 (assume @p145 (forall @t146 (or @t101 (not (tptp.geq @t40 @t143)) @t150 @t90 @t46 (tptp.geq @t2 @t143)))) % 60.23/60.42 (assume @p146 (forall @t146 (or @t47 @t65 @t145 (= (tptp.app @t158 @t2) (tptp.app @t143 @t64))))) % 60.23/60.42 (assume @p147 @t160) % 60.23/60.42 (assume @p148 (forall @t146 (or (not (= @t111 @t158)) @t47 @t65 @t145 @t161))) % 60.23/60.42 (assume @p149 (forall @t146 (or @t130 (not (tptp.segmentP @t40 @t143)) @t145 @t65 @t47 (tptp.segmentP @t2 @t143)))) % 60.23/60.42 (assume @p150 (forall @t146 (or @t131 (not (tptp.rearsegP @t40 @t143)) @t145 @t65 @t47 (tptp.rearsegP @t2 @t143)))) % 60.23/60.42 (assume @p151 (forall @t146 (or @t133 (not (tptp.frontsegP @t40 @t143)) @t145 @t65 @t47 (tptp.frontsegP @t2 @t143)))) % 60.23/60.42 (assume @p152 (forall @t146 (or @t93 @t157 @t150 @t90 @t46 @t156))) % 60.23/60.42 (assume @p153 (forall @t146 (or @t103 (not (tptp.leq @t40 @t143)) @t150 @t90 @t46 (tptp.leq @t2 @t143)))) % 60.23/60.42 (assume @p154 (forall @t146 (or @t46 @t65 @t145 (= (tptp.cons @t2 (tptp.app @t40 @t143)) (tptp.app @t66 @t143))))) % 60.23/60.42 (assume @p155 (forall @t146 (or (not (tptp.memberP @t111 @t143)) @t65 @t47 @t150 @t162 (tptp.memberP @t2 @t143)))) % 60.23/60.42 (assume @p156 (forall @t41 (or (not @t142) (not @t127) @t65 @t46 @t128 @t116))) % 60.23/60.42 (assume @p157 (forall @t41 (or (not @t141) (not @t124) @t65 @t46 @t125 @t116))) % 60.23/60.42 (assume @p158 (forall @t146 (or (not (tptp.memberP @t66 @t143)) @t65 @t46 @t150 @t162 (= @t143 @t2)))) % 60.23/60.42 (assume @p159 (forall @t4 (or @t47 @t50 (= (tptp.app (tptp.app @t12 (tptp.cons @t13 @t11)) (tptp.cons @t13 @t10)) @t2)))) % 60.23/60.42 (assume @p160 (forall @t4 (or @t47 @t69 (= (tptp.app (tptp.app @t16 (tptp.cons @t18 @t15)) (tptp.cons @t17 @t14)) @t2)))) % 60.23/60.42 (assume @p161 (forall @t4 (or @t47 @t70 (= (tptp.app (tptp.app @t21 (tptp.cons @t23 @t20)) (tptp.cons @t22 @t19)) @t2)))) % 60.23/60.42 (assume @p162 (forall @t4 (or @t47 @t71 (= (tptp.app (tptp.app @t26 (tptp.cons @t28 @t25)) (tptp.cons @t27 @t24)) @t2)))) % 60.23/60.42 (assume @p163 (forall @t4 (or @t47 @t72 (= (tptp.app (tptp.app @t31 (tptp.cons @t33 @t30)) (tptp.cons @t32 @t29)) @t2)))) % 60.23/60.42 (assume @p164 (forall @t4 (or @t47 @t67 (= (tptp.app (tptp.app @t36 (tptp.cons @t38 @t35)) (tptp.cons @t37 @t34)) @t2)))) % 60.23/60.42 (assume @p165 (forall @t41 (or @t130 @t65 @t47 (= (tptp.app (tptp.app @t42 @t40) (tptp.skaf48 @t40 @t2)) @t2)))) % 60.23/60.42 (assume @p166 (forall @t41 (or @t151 @t90 @t47 (= (tptp.app @t45 (tptp.cons @t40 (tptp.skaf43 @t40 @t2))) @t2)))) % 60.23/60.42 (assume @p167 (forall @t167 (or @t166 @t150 @t46 @t164 @t65 @t161))) % 60.23/60.42 (assume @p168 (forall @t167 (or @t166 @t150 @t46 @t164 @t65 (= @t163 @t40)))) % 60.23/60.42 (assume @p169 (forall @t167 (or @t130 @t145 @t164 @t65 @t47 (tptp.segmentP (tptp.app (tptp.app @t163 @t2) @t143) @t40)))) % 60.23/60.42 (assume @p170 @t172) % 60.23/60.42 (assume @p171 (forall @t167 (or @t173 @t164 @t65 @t150 @t46 (tptp.frontsegP @t40 @t163)))) % 60.23/60.42 (assume @p172 (forall @t167 (or (not (= @t174 @t163)) @t145 @t47 @t90 @t164 (tptp.memberP @t163 @t40)))) % 60.23/60.42 (assume @p173 (forall @t167 (or @t173 @t164 @t65 @t150 @t46 @t161))) % 60.23/60.42 (assume @p174 (forall @t41 (or (not (= @t58 @t140)) (not (= @t59 @t122)) @t47 @t65 @t116 @t107 @t57))) % 60.23/60.42 (assume @p175 (forall @t167 (or @t133 (not (= @t143 @t163)) @t65 @t47 @t175 @t150 (tptp.frontsegP @t149 (tptp.cons @t163 @t40))))) % 60.23/60.42 (assume @p176 (forall @t178 (or (not (= (tptp.app @t174 (tptp.cons @t40 @t163)) @t176)) @t164 @t145 @t47 @t90 (not (tptp.duplicatefreeP @t176)) @t177))) % 60.23/60.42 (assume @p177 @t183) % 60.23/60.42 (assume @p178 @t192) % 60.23/60.42 (assume @p179 (forall @t191 (or @t189 @t177 @t145 @t47 @t175 @t90 (not (tptp.totalorderedP @t185)) @t186 @t193))) % 60.23/60.42 (assume @p180 (forall @t191 (or @t189 @t177 @t145 @t47 @t175 @t90 (not (tptp.strictorderP @t185)) @t186 @t184 (tptp.lt @t163 @t40)))) % 60.23/60.42 (assume @p181 (forall @t191 (or @t189 @t177 @t145 @t47 @t175 @t90 (not (tptp.totalorderP @t185)) @t186 @t193 (tptp.leq @t163 @t40)))) % 60.23/60.42 (assume @p182 (forall @t191 (or @t103 @t136 (not (= (tptp.app (tptp.app @t143 (tptp.cons @t2 @t163)) (tptp.cons @t40 @t176)) @t185)) @t177 @t164 @t145 @t90 @t46 (not (tptp.cyclefreeP @t185)) @t186))) % 60.23/60.42 (assume @p183 @t194) % 60.23/60.42 (assume @p184 (tptp.ssList tptp.sk2)) % 60.23/60.42 (assume @p185 (tptp.ssList tptp.sk3)) % 60.23/60.42 (assume @p186 @t195) % 60.23/60.42 (assume @p187 (= tptp.sk2 tptp.sk4)) % 60.23/60.42 (assume @p188 (= tptp.sk1 tptp.sk3)) % 60.23/60.42 (assume @p189 @t196) % 60.23/60.42 (assume @p190 @t197) % 60.23/60.42 (assume @p191 @t198) % 60.23/60.42 (assume @p192 @t199) % 60.23/60.42 (assume @p193 @t200) % 60.23/60.42 (assume @p194 (= @t205 tptp.sk1)) % 60.23/60.42 (assume @p195 (not (= tptp.sk5 tptp.sk6))) % 60.23/60.42 (assume @p196 @t209) % 60.23/60.42 (step @p197 :rule instantiate :premises (@p78) :args ((@list @t201))) % 60.23/60.42 (step @p198 :rule refl :args (@t65)) % 60.23/60.42 (step @p199 :rule refl :args (@t46)) % 60.23/60.42 (step @p200 :rule eq-symm :args (@t66 tptp.nil)) % 60.23/60.42 (step @p201 :rule cong :premises (@p200) :args (@t79)) % 60.23/60.42 (step @p202 :rule nary_cong :premises (@p201 @p199 @p198) :args (@t80)) % 60.23/60.42 (step @p203 :rule cong :premises (@p202) :args (@t81)) % 60.23/60.42 (step @p204 :rule eq_resolve :premises (@p96 @p203)) % 60.23/60.42 (step @p205 :rule instantiate :premises (@p204) :args (@t210)) % 60.23/60.42 (step @p206 :rule cnf_or_pos :args (@t215)) % 60.23/60.42 (step @p207 :rule reordering :premises (@p206) :args ((or @t211 @t212 @t214 (not @t215)))) % 60.23/60.42 (step @p208 :rule chain_m_resolution :premises (@p207 @p8 @p191 @p205) :args (@t214 @t216 (@list @t1 @t198 @t215))) % 60.23/60.42 (step @p209 :rule instantiate :premises (@p84) :args (@t210)) % 60.23/60.42 (step @p210 :rule cnf_or_pos :args (@t218)) % 60.23/60.42 (step @p211 :rule reordering :premises (@p210) :args ((or @t211 @t212 @t217 (not @t218)))) % 60.23/60.42 (step @p212 :rule chain_m_resolution :premises (@p211 @p8 @p191 @p209) :args (@t217 @t216 (@list @t1 @t198 @t218))) % 60.23/60.42 (step @p213 :rule cnf_or_pos :args (@t222)) % 60.23/60.42 (step @p214 :rule reordering :premises (@p213) :args ((or @t219 @t213 @t221 (not @t222)))) % 60.23/60.42 (step @p215 :rule chain_m_resolution :premises (@p214 @p212 @p208 @p197) :args (@t221 @t223 (@list @t217 @t213 @t222))) % 60.23/60.42 (step @p216 :rule instantiate :premises (@p149) :args ((@list tptp.sk4 @t205 @t201))) % 60.23/60.42 (step @p217 :rule aci_norm :args ((= (or false @t145 @t47 @t65 @t225 @t224) (or @t145 @t47 @t65 @t225 @t224)))) % 60.23/60.42 (step @p218 :rule refl :args (@t224)) % 60.23/60.42 (step @p219 :rule refl :args (@t225)) % 60.23/60.42 (step @p220 :rule refl :args (@t47)) % 60.23/60.42 (step @p221 :rule refl :args (@t145)) % 60.23/60.42 (step @p222 :rule evaluate :args ((not true))) % 60.23/60.42 (step @p223 :rule eq-refl :args (@t169)) % 60.23/60.42 (step @p224 :rule cong :premises (@p223) :args (@t226)) % 60.23/60.42 (step @p225 :rule trans :premises (@p224 @p222)) % 60.23/60.42 (step @p226 :rule nary_cong :premises (@p225 @p221 @p220 @p198 @p219 @p218) :args (@t227)) % 60.23/60.42 (step @p227 :rule trans :premises (@p226 @p217)) % 60.23/60.42 (step @p228 :rule cong :premises (@p227) :args ((forall @t146 @t227))) % 60.23/60.42 (step @p229 :rule quant-var-elim-eq :args ((= (forall @t230 @t229) @t227))) % 60.23/60.42 (step @p230 :rule aci_norm :args ((= @t231 @t229))) % 60.23/60.42 (step @p231 :rule cong :premises (@p230) :args (@t232)) % 60.23/60.42 (step @p232 :rule trans :premises (@p231 @p229)) % 60.23/60.42 (step @p233 :rule cong :premises (@p232) :args (@t233)) % 60.23/60.42 (step @p234 :rule quant-merge-prenex :args ((= @t233 (forall @t167 @t231)))) % 60.23/60.42 (step @p235 :rule symm :premises (@p234)) % 60.23/60.42 (step @p236 :rule trans :premises (@p235 @p233)) % 60.23/60.42 (step @p237 :rule trans :premises (@p236 @p228)) % 60.23/60.42 (step @p238 :rule refl :args (@t168)) % 60.23/60.42 (step @p239 :rule refl :args (@t164)) % 60.23/60.42 (step @p240 :rule eq-symm :args (@t169 @t163)) % 60.23/60.42 (step @p241 :rule cong :premises (@p240) :args (@t170)) % 60.23/60.42 (step @p242 :rule nary_cong :premises (@p241 @p221 @p220 @p198 @p239 @p238) :args (@t171)) % 60.23/60.42 (step @p243 :rule cong :premises (@p242) :args (@t172)) % 60.23/60.42 (step @p244 :rule trans :premises (@p243 @p237)) % 60.23/60.42 (step @p245 :rule eq_resolve :premises (@p170 @p244)) % 60.23/60.42 (step @p246 :rule instantiate :premises (@p245) :args ((@list @t203 @t201 tptp.sk8))) % 60.23/60.42 (step @p247 :rule instantiate :premises (@p83) :args (@t234)) % 60.23/60.42 (step @p248 :rule instantiate :premises (@p84) :args (@t235)) % 60.23/60.42 (step @p249 :rule cnf_or_pos :args (@t238)) % 60.23/60.42 (step @p250 :rule reordering :premises (@p249) :args ((or @t211 @t237 @t236 (not @t238)))) % 60.23/60.42 (step @p251 :rule chain_m_resolution :premises (@p250 @p8 @p190 @p248) :args (@t236 @t216 (@list @t1 @t197 @t238))) % 60.23/60.42 (step @p252 :rule cnf_or_pos :args (@t242)) % 60.23/60.42 (step @p253 :rule reordering :premises (@p252) :args ((or @t240 @t241 @t239 (not @t242)))) % 60.23/60.42 (step @p254 :rule chain_m_resolution :premises (@p253 @p192 @p251 @p247) :args (@t239 @t216 (@list @t199 @t236 @t242))) % 60.23/60.42 (step @p255 :rule symm :premises (@p194)) % 60.23/60.42 (step @p256 :rule cong :premises (@p255) :args (@t194)) % 60.23/60.42 (step @p257 :rule eq_resolve :premises (@p183 @p256)) % 60.23/60.42 (step @p258 :rule cnf_or_pos :args (@t248)) % 60.23/60.42 (step @p259 :rule reordering :premises (@p258) :args ((or @t245 @t247 @t219 @t246 @t243 (not @t248)))) % 60.23/60.42 (step @p260 :rule chain_m_resolution :premises (@p259 @p257 @p193 @p212 @p254 @p246) :args (@t243 @t249 (@list @t244 @t200 @t217 @t239 @t248))) % 60.23/60.42 (step @p261 :rule refl :args (@t205)) % 60.23/60.42 (step @p262 :rule cong :premises (@p188 @p261) :args ((= tptp.sk1 @t205))) % 60.23/60.42 (step @p263 :rule eq_resolve :premises (@p255 @p262)) % 60.23/60.42 (step @p264 :rule refl :args (tptp.sk4)) % 60.23/60.42 (step @p265 :rule cong :premises (@p264 @p263) :args (@t196)) % 60.23/60.42 (step @p266 :rule eq_resolve :premises (@p189 @p265)) % 60.23/60.42 (step @p267 :rule cnf_or_pos :args (@t255)) % 60.23/60.42 (step @p268 :rule reordering :premises (@p267) :args ((or @t245 @t251 @t254 @t219 @t252 @t250 (not @t255)))) % 60.23/60.42 (step @p269 :rule chain_m_resolution :premises (@p268 @p257 @p186 @p266 @p212 @p260 @p216) :args (@t250 (@list false false false false false false) (@list @t244 @t195 @t253 @t217 @t243 @t255))) % 60.23/60.42 (step @p270 :rule eq-symm :args (@t40 @t2)) % 60.23/60.42 (step @p271 :rule refl :args (@t83)) % 60.23/60.42 (step @p272 :rule nary_cong :premises (@p220 @p198 @p271 @p270) :args (@t84)) % 60.23/60.42 (step @p273 :rule cong :premises (@p272) :args (@t85)) % 60.23/60.42 (step @p274 :rule eq_resolve :premises (@p98 @p273)) % 60.23/60.42 (step @p275 :rule instantiate :premises (@p274) :args ((@list tptp.nil tptp.sk4))) % 60.23/60.42 (step @p276 :rule eq-symm :args (@t86 @t2)) % 60.23/60.42 (step @p277 :rule refl :args (@t87)) % 60.23/60.42 (step @p278 :rule nary_cong :premises (@p277 @p220 @p276) :args (@t88)) % 60.23/60.42 (step @p279 :rule cong :premises (@p278) :args (@t89)) % 60.23/60.42 (step @p280 :rule eq_resolve :premises (@p99 @p279)) % 60.23/60.42 (step @p281 :rule instantiate :premises (@p280) :args (@t256)) % 60.23/60.42 (assume-push @p1358 @t244) % 60.23/60.42 (assume-push @p1359 @t260) % 60.23/60.42 (assume-push @p1360 @t244) % 60.23/60.42 (assume-push @p1361 @t260) % 60.23/60.42 (step @p286 :rule true_intro :premises (@p257)) % 60.23/60.42 (step @p287 :rule symm :premises (@p1359)) % 60.23/60.42 (step @p288 :rule refl :args (@t204)) % 60.23/60.42 (step @p289 :rule cong :premises (@p288 @p287) :args (@t261)) % 60.23/60.42 (step @p290 :rule cong :premises (@p289) :args (@t262)) % 60.23/60.42 (step @p291 :rule trans :premises (@p290 @p286)) % 60.23/60.42 (step @p292 :rule true_elim :premises (@p291)) % 60.23/60.42 (step-pop @p1362 :rule scope :premises (@p292)) % 60.23/60.42 (step-pop @p1363 :rule scope :premises (@p1362)) % 60.23/60.42 (step @p293 :rule process_scope :premises (@p1363) :args (@t262)) % 60.23/60.42 (step @p296 :rule and_intro :premises (@p257 @p1359)) % 60.23/60.42 (step @p297 :rule modus_ponens :premises (@p296 @p293)) % 60.23/60.42 (step-pop @p1364 :rule scope :premises (@p297)) % 60.23/60.42 (step-pop @p1365 :rule scope :premises (@p1364)) % 60.23/60.42 (step @p298 :rule process_scope :premises (@p1365) :args (@t262)) % 60.23/60.42 (step @p301 :rule implies_elim :premises (@p298)) % 60.23/60.42 (step @p302 :rule cnf_and_neg :args (@t263)) % 60.23/60.42 (step @p303 :rule resolution :premises (@p302 @p301) :args (true @t263)) % 60.23/60.42 (step @p304 :rule eq-symm :args (@t51 @t2)) % 60.23/60.42 (step @p305 :rule nary_cong :premises (@p220 @p304) :args (@t52)) % 60.23/60.42 (step @p306 :rule cong :premises (@p305) :args (@t53)) % 60.23/60.42 (step @p307 :rule eq_resolve :premises (@p73 @p306)) % 60.23/60.42 (step @p308 :rule instantiate :premises (@p307) :args (@t256)) % 60.23/60.42 (step @p309 :rule cnf_or_pos :args (@t266)) % 60.23/60.42 (step @p310 :rule reordering :premises (@p309) :args ((or @t245 @t265 (not @t266)))) % 60.23/60.42 (step @p311 :rule chain_m_resolution :premises (@p310 @p257 @p308) :args (@t265 @t267 (@list @t244 @t266))) % 60.23/60.42 (step @p312 :rule refl :args (@t57)) % 60.23/60.42 (step @p313 :rule eq-symm :args (@t104 @t2)) % 60.23/60.42 (step @p314 :rule nary_cong :premises (@p220 @p313 @p312) :args (@t105)) % 60.23/60.42 (step @p315 :rule cong :premises (@p314) :args (@t106)) % 60.23/60.42 (step @p316 :rule eq_resolve :premises (@p107 @p315)) % 60.23/60.42 (step @p317 :rule instantiate :premises (@p316) :args (@t256)) % 60.23/60.42 (step @p318 :rule eq-symm :args (@t111 tptp.nil)) % 60.23/60.42 (step @p319 :rule cong :premises (@p318) :args (@t113)) % 60.23/60.43 (step @p320 :rule nary_cong :premises (@p319 @p198 @p220 @p312) :args (@t114)) % 60.23/60.43 (step @p321 :rule cong :premises (@p320) :args (@t115)) % 60.23/60.43 (step @p322 :rule eq_resolve :premises (@p116 @p321)) % 60.23/60.43 (step @p323 :rule instantiate :premises (@p322) :args ((@list @t204 tptp.sk8))) % 60.23/60.43 (step @p324 :rule instantiate :premises (@p83) :args (@t268)) % 60.23/60.43 (step @p325 :rule cnf_or_pos :args (@t270)) % 60.23/60.43 (step @p326 :rule reordering :premises (@p325) :args ((or @t219 @t246 @t269 (not @t270)))) % 60.23/60.43 (step @p327 :rule chain_m_resolution :premises (@p326 @p212 @p254 @p324) :args (@t269 @t216 (@list @t217 @t239 @t270))) % 60.23/60.43 (step @p328 :rule refl :args (@t116)) % 60.23/60.43 (step @p329 :rule nary_cong :premises (@p319 @p198 @p220 @p328) :args (@t117)) % 60.23/60.43 (step @p330 :rule cong :premises (@p329) :args (@t118)) % 60.23/60.43 (step @p331 :rule eq_resolve :premises (@p117 @p330)) % 60.23/60.43 (step @p332 :rule instantiate :premises (@p331) :args (@t271)) % 60.23/60.43 (step @p333 :rule cnf_or_pos :args (@t274)) % 60.23/60.43 (step @p334 :rule reordering :premises (@p333) :args ((or @t219 @t246 @t213 @t273 (not @t274)))) % 60.23/60.43 (step @p335 :rule chain_m_resolution :premises (@p334 @p212 @p254 @p208 @p332) :args (@t273 @t275 (@list @t217 @t239 @t213 @t274))) % 60.23/60.43 (step @p336 :rule cnf_or_pos :args (@t279)) % 60.23/60.43 (step @p337 :rule reordering :premises (@p336) :args ((or @t247 @t272 @t278 @t276 (not @t279)))) % 60.23/60.43 (step @p338 :rule chain_m_resolution :premises (@p337 @p193 @p335 @p327 @p323) :args (@t278 @t280 (@list @t200 @t272 @t269 @t279))) % 60.23/60.43 (step @p339 :rule cnf_or_pos :args (@t285)) % 60.23/60.43 (step @p340 :rule reordering :premises (@p339) :args ((or @t245 @t277 @t284 (not @t285)))) % 60.23/60.43 (step @p341 :rule chain_m_resolution :premises (@p340 @p257 @p338 @p317) :args (@t284 @t223 (@list @t244 @t277 @t285))) % 60.23/60.43 (step @p342 :rule eq-symm :args (@t119 @t66)) % 60.23/60.43 (step @p343 :rule nary_cong :premises (@p199 @p198 @p342) :args (@t120)) % 60.23/60.43 (step @p344 :rule cong :premises (@p343) :args (@t121)) % 60.23/60.43 (step @p345 :rule eq_resolve :premises (@p118 @p344)) % 60.23/60.43 (step @p346 :rule instantiate :premises (@p345) :args ((@list @t286 tptp.nil))) % 60.23/60.43 (step @p347 :rule instantiate :premises (@p76) :args (@t256)) % 60.23/60.43 (step @p348 :rule cnf_or_pos :args (@t288)) % 60.23/60.43 (step @p349 :rule reordering :premises (@p348) :args ((or @t245 @t287 @t277 (not @t288)))) % 60.23/60.43 (step @p350 :rule chain_m_resolution :premises (@p349 @p257 @p338 @p347) :args (@t287 @t223 (@list @t244 @t277 @t288))) % 60.23/60.43 (step @p351 :rule cnf_or_pos :args (@t293)) % 60.23/60.43 (step @p352 :rule reordering :premises (@p351) :args ((or @t211 @t292 @t291 (not @t293)))) % 60.23/60.43 (step @p353 :rule chain_m_resolution :premises (@p352 @p8 @p350 @p346) :args (@t291 @t216 (@list @t1 @t287 @t293))) % 60.23/60.43 (step @p354 :rule instantiate :premises (@p345) :args (@t294)) % 60.23/60.43 (step @p355 :rule instantiate :premises (@p12) :args (@t256)) % 60.23/60.43 (step @p356 :rule instantiate :premises (@p13) :args (@t256)) % 60.23/60.43 (step @p357 :rule cnf_or_pos :args (@t302)) % 60.23/60.43 (step @p358 :rule reordering :premises (@p357) :args ((or @t299 @t301 @t297 (not @t302)))) % 60.23/60.43 (step @p359 :rule chain_m_resolution :premises (@p358 @p356 @p355 @p354) :args (@t297 @t216 (@list @t298 @t300 @t302))) % 60.23/60.43 (step @p360 :rule eq-symm :args (@t73 @t40)) % 60.23/60.43 (step @p361 :rule nary_cong :premises (@p199 @p198 @p360) :args (@t74)) % 60.23/60.43 (step @p362 :rule cong :premises (@p361) :args (@t75)) % 60.23/60.43 (step @p363 :rule eq_resolve :premises (@p94 @p362)) % 60.23/60.43 (step @p364 :rule instantiate :premises (@p363) :args (@t294)) % 60.23/60.43 (step @p365 :rule cnf_or_pos :args (@t305)) % 60.23/60.43 (step @p366 :rule reordering :premises (@p365) :args ((or @t299 @t301 @t304 (not @t305)))) % 60.23/60.43 (step @p367 :rule chain_m_resolution :premises (@p366 @p356 @p355 @p364) :args (@t304 @t216 (@list @t298 @t300 @t305))) % 60.23/60.43 (step @p368 :rule eq-symm :args (@t76 @t2)) % 60.23/60.43 (step @p369 :rule nary_cong :premises (@p199 @p198 @p368) :args (@t77)) % 60.23/60.43 (step @p370 :rule cong :premises (@p369) :args (@t78)) % 60.23/60.43 (step @p371 :rule eq_resolve :premises (@p95 @p370)) % 60.23/60.43 (step @p372 :rule instantiate :premises (@p371) :args (@t294)) % 60.23/60.43 (step @p373 :rule cnf_or_pos :args (@t308)) % 60.23/60.43 (step @p374 :rule reordering :premises (@p373) :args ((or @t299 @t301 @t307 (not @t308)))) % 60.23/60.43 (step @p375 :rule chain_m_resolution :premises (@p374 @p356 @p355 @p372) :args (@t307 @t216 (@list @t298 @t300 @t308))) % 60.23/60.43 (step @p376 :rule instantiate :premises (@p66) :args (@t309)) % 60.23/60.43 (step @p377 :rule cnf_or_pos :args (@t311)) % 60.23/60.43 (step @p378 :rule reordering :premises (@p377) :args ((or @t292 @t310 (not @t311)))) % 60.23/60.43 (step @p379 :rule chain_m_resolution :premises (@p378 @p350 @p376) :args (@t310 @t267 (@list @t287 @t311))) % 60.23/60.43 (step @p380 :rule instantiate :premises (@p363) :args ((@list @t312 tptp.nil))) % 60.23/60.43 (step @p381 :rule instantiate :premises (@p47) :args (@t256)) % 60.23/60.43 (step @p382 :rule cnf_or_pos :args (@t318)) % 60.23/60.43 (step @p383 :rule reordering :premises (@p382) :args ((or @t211 @t317 @t315 (not @t318)))) % 60.23/60.43 (step @p384 :rule chain_m_resolution :premises (@p383 @p8 @p381 @p380) :args (@t315 @t216 (@list @t1 @t316 @t318))) % 60.23/60.43 (assume-push @p1366 @t265) % 60.23/60.43 (assume-push @p1367 @t319) % 60.23/60.43 (assume-push @p1368 @t260) % 60.23/60.43 (assume-push @p1369 @t284) % 60.23/60.43 (assume-push @p1370 @t297) % 60.23/60.43 (assume-push @p1371 @t291) % 60.23/60.43 (assume-push @p1372 @t310) % 60.23/60.43 (assume-push @p1373 @t315) % 60.23/60.43 (assume-push @p1374 @t304) % 60.23/60.43 (assume-push @p1375 @t307) % 60.23/60.43 (assume-push @p1376 @t310) % 60.23/60.43 (assume-push @p1377 @t291) % 60.23/60.43 (assume-push @p1378 @t315) % 60.23/60.43 (assume-push @p1379 @t319) % 60.23/60.43 (assume-push @p1380 @t265) % 60.23/60.43 (assume-push @p1381 @t284) % 60.23/60.43 (assume-push @p1382 @t307) % 60.23/60.43 (assume-push @p1383 @t304) % 60.23/60.43 (assume-push @p1384 @t297) % 60.23/60.43 (assume-push @p1385 @t260) % 60.23/60.43 (step @p405 :rule true_intro :premises (@p379)) % 60.23/60.43 (step @p406 :rule symm :premises (@p353)) % 60.23/60.43 (step @p407 :rule symm :premises (@p384)) % 60.23/60.43 (step @p408 :rule symm :premises (@p311)) % 60.23/60.43 (step @p409 :rule trans :premises (@p408 @p1367)) % 60.23/60.43 (step @p410 :rule cong :premises (@p409) :args (@t320)) % 60.23/60.43 (step @p411 :rule cong :premises (@p311) :args (@t321)) % 60.23/60.43 (step @p412 :rule trans :premises (@p411 @p410 @p407)) % 60.23/60.43 (step @p413 :rule refl :args (@t289)) % 60.23/60.43 (step @p414 :rule cong :premises (@p413 @p412) :args (@t322)) % 60.23/60.43 (step @p415 :rule symm :premises (@p411)) % 60.23/60.43 (step @p416 :rule symm :premises (@p341)) % 60.23/60.43 (step @p417 :rule trans :premises (@p416 @p311)) % 60.23/60.43 (step @p418 :rule cong :premises (@p417) :args (@t303)) % 60.23/60.43 (step @p419 :rule trans :premises (@p367 @p418 @p415)) % 60.23/60.43 (step @p420 :rule refl :args (tptp.nil)) % 60.23/60.43 (step @p421 :rule cong :premises (@p408) :args (@t323)) % 60.23/60.43 (step @p422 :rule cong :premises (@p417) :args (@t306)) % 60.23/60.43 (step @p423 :rule trans :premises (@p375 @p422 @p421)) % 60.23/60.43 (step @p424 :rule cong :premises (@p423 @p420) :args (@t295)) % 60.23/60.43 (step @p425 :rule cong :premises (@p424 @p419) :args (@t296)) % 60.23/60.43 (step @p426 :rule trans :premises (@p341 @p359 @p425 @p414 @p406)) % 60.23/60.43 (step @p427 :rule cong :premises (@p426) :args ((tptp.strictorderedP @t205))) % 60.23/60.43 (step @p428 :rule symm :premises (@p1368)) % 60.23/60.43 (step @p288 :rule refl :args (@t204)) % 60.23/60.43 (step @p429 :rule cong :premises (@p288 @p428) :args (@t261)) % 60.23/60.43 (step @p430 :rule cong :premises (@p429) :args (@t324)) % 60.23/60.43 (step @p431 :rule trans :premises (@p430 @p427 @p405)) % 60.23/60.43 (step @p432 :rule true_elim :premises (@p431)) % 60.23/60.43 (step-pop @p1386 :rule scope :premises (@p432)) % 60.23/60.43 (step-pop @p1387 :rule scope :premises (@p1386)) % 60.23/60.43 (step-pop @p1388 :rule scope :premises (@p1387)) % 60.23/60.43 (step-pop @p1389 :rule scope :premises (@p1388)) % 60.23/60.43 (step-pop @p1390 :rule scope :premises (@p1389)) % 60.23/60.43 (step-pop @p1391 :rule scope :premises (@p1390)) % 60.23/60.43 (step-pop @p1392 :rule scope :premises (@p1391)) % 60.23/60.43 (step-pop @p1393 :rule scope :premises (@p1392)) % 60.23/60.43 (step-pop @p1394 :rule scope :premises (@p1393)) % 60.23/60.43 (step-pop @p1395 :rule scope :premises (@p1394)) % 60.23/60.43 (step @p433 :rule process_scope :premises (@p1395) :args (@t324)) % 60.23/60.43 (step @p444 :rule and_intro :premises (@p379 @p353 @p384 @p1367 @p311 @p341 @p375 @p367 @p359 @p1368)) % 60.23/60.43 (step @p445 :rule modus_ponens :premises (@p444 @p433)) % 60.23/60.43 (step-pop @p1396 :rule scope :premises (@p445)) % 60.23/60.43 (step-pop @p1397 :rule scope :premises (@p1396)) % 60.23/60.43 (step-pop @p1398 :rule scope :premises (@p1397)) % 60.23/60.43 (step-pop @p1399 :rule scope :premises (@p1398)) % 60.23/60.43 (step-pop @p1400 :rule scope :premises (@p1399)) % 60.23/60.43 (step-pop @p1401 :rule scope :premises (@p1400)) % 60.23/60.43 (step-pop @p1402 :rule scope :premises (@p1401)) % 60.23/60.43 (step-pop @p1403 :rule scope :premises (@p1402)) % 60.23/60.43 (step-pop @p1404 :rule scope :premises (@p1403)) % 60.23/60.43 (step-pop @p1405 :rule scope :premises (@p1404)) % 60.23/60.43 (step @p446 :rule process_scope :premises (@p1405) :args (@t324)) % 60.23/60.43 (step @p457 :rule implies_elim :premises (@p446)) % 60.23/60.43 (step @p458 :rule cnf_and_neg :args (@t325)) % 60.23/60.43 (step @p459 :rule resolution :premises (@p458 @p457) :args (true @t325)) % 60.23/60.43 (step @p460 :rule reordering :premises (@p459) :args ((or @t334 @t333 @t332 @t331 @t324 @t330 @t329 (not @t310) @t328 @t327 @t326))) % 60.23/60.43 (step @p461 :rule instantiate :premises (@p146) :args ((@list tptp.sk8 @t201 @t203))) % 60.23/60.43 (step @p462 :rule cnf_or_pos :args (@t337)) % 60.23/60.43 (step @p463 :rule reordering :premises (@p462) :args ((or @t247 @t219 @t246 @t336 (not @t337)))) % 60.23/60.43 (step @p464 :rule chain_m_resolution :premises (@p463 @p193 @p212 @p254 @p461) :args (@t336 @t338 (@list @t200 @t217 @t239 @t337))) % 60.23/60.43 (step @p465 :rule instantiate :premises (@p345) :args ((@list tptp.sk6 tptp.sk8))) % 60.23/60.43 (step @p466 :rule cnf_or_pos :args (@t340)) % 60.23/60.43 (step @p467 :rule reordering :premises (@p466) :args ((or @t212 @t247 @t339 (not @t340)))) % 60.23/60.43 (step @p468 :rule chain_m_resolution :premises (@p467 @p191 @p193 @p465) :args (@t339 @t216 (@list @t198 @t200 @t340))) % 60.23/60.43 (step @p469 :rule instantiate :premises (@p64) :args (@t309)) % 60.23/60.43 (step @p470 :rule cnf_or_pos :args (@t342)) % 60.23/60.43 (step @p471 :rule reordering :premises (@p470) :args ((or @t292 @t341 (not @t342)))) % 60.23/60.43 (step @p472 :rule chain_m_resolution :premises (@p471 @p350 @p469) :args (@t341 @t267 (@list @t287 @t342))) % 60.23/60.43 (assume-push @p1406 @t265) % 60.23/60.43 (assume-push @p1407 @t319) % 60.23/60.43 (assume-push @p1408 @t260) % 60.23/60.43 (assume-push @p1409 @t284) % 60.23/60.43 (assume-push @p1410 @t336) % 60.23/60.43 (assume-push @p1411 @t339) % 60.23/60.43 (assume-push @p1412 @t297) % 60.23/60.43 (assume-push @p1413 @t291) % 60.23/60.43 (assume-push @p1414 @t341) % 60.23/60.43 (assume-push @p1415 @t315) % 60.23/60.43 (assume-push @p1416 @t304) % 60.23/60.43 (assume-push @p1417 @t307) % 60.23/60.43 (assume-push @p1418 @t341) % 60.23/60.43 (assume-push @p1419 @t291) % 60.23/60.43 (assume-push @p1420 @t315) % 60.23/60.43 (assume-push @p1421 @t319) % 60.23/60.43 (assume-push @p1422 @t265) % 60.23/60.43 (assume-push @p1423 @t284) % 60.23/60.43 (assume-push @p1424 @t307) % 60.23/60.43 (assume-push @p1425 @t304) % 60.23/60.43 (assume-push @p1426 @t297) % 60.23/60.43 (assume-push @p1427 @t336) % 60.23/60.43 (assume-push @p1428 @t339) % 60.23/60.43 (assume-push @p1429 @t260) % 60.23/60.43 (step @p497 :rule true_intro :premises (@p472)) % 60.23/60.43 (step @p406 :rule symm :premises (@p353)) % 60.23/60.43 (step @p407 :rule symm :premises (@p384)) % 60.23/60.43 (step @p408 :rule symm :premises (@p311)) % 60.23/60.43 (step @p498 :rule trans :premises (@p408 @p1407)) % 60.23/60.43 (step @p499 :rule cong :premises (@p498) :args (@t320)) % 60.23/60.43 (step @p411 :rule cong :premises (@p311) :args (@t321)) % 60.23/60.43 (step @p500 :rule trans :premises (@p411 @p499 @p407)) % 60.23/60.43 (step @p413 :rule refl :args (@t289)) % 60.23/60.43 (step @p501 :rule cong :premises (@p413 @p500) :args (@t322)) % 60.23/60.43 (step @p415 :rule symm :premises (@p411)) % 60.23/60.43 (step @p416 :rule symm :premises (@p341)) % 60.23/60.43 (step @p417 :rule trans :premises (@p416 @p311)) % 60.23/60.43 (step @p418 :rule cong :premises (@p417) :args (@t303)) % 60.23/60.43 (step @p419 :rule trans :premises (@p367 @p418 @p415)) % 60.23/60.43 (step @p420 :rule refl :args (tptp.nil)) % 60.23/60.43 (step @p421 :rule cong :premises (@p408) :args (@t323)) % 60.23/60.43 (step @p422 :rule cong :premises (@p417) :args (@t306)) % 60.23/60.43 (step @p423 :rule trans :premises (@p375 @p422 @p421)) % 60.23/60.43 (step @p424 :rule cong :premises (@p423 @p420) :args (@t295)) % 60.23/60.43 (step @p425 :rule cong :premises (@p424 @p419) :args (@t296)) % 60.23/60.43 (step @p502 :rule trans :premises (@p341 @p359 @p425 @p501 @p406)) % 60.23/60.43 (step @p503 :rule cong :premises (@p502) :args ((tptp.equalelemsP @t205))) % 60.23/60.43 (step @p504 :rule symm :premises (@p464)) % 60.23/60.43 (step @p505 :rule symm :premises (@p1408)) % 60.23/60.43 (step @p506 :rule refl :args (tptp.sk6)) % 60.23/60.43 (step @p507 :rule cong :premises (@p506 @p505) :args (@t343)) % 60.23/60.43 (step @p508 :rule trans :premises (@p507 @p468)) % 60.23/60.43 (step @p509 :rule refl :args (@t203)) % 60.23/60.43 (step @p510 :rule cong :premises (@p509 @p508) :args (@t344)) % 60.23/60.43 (step @p511 :rule trans :premises (@p510 @p504)) % 60.23/60.43 (step @p512 :rule cong :premises (@p511) :args (@t345)) % 60.23/60.43 (step @p513 :rule trans :premises (@p512 @p503 @p497)) % 60.23/60.43 (step @p514 :rule true_elim :premises (@p513)) % 60.23/60.43 (step-pop @p1430 :rule scope :premises (@p514)) % 60.23/60.43 (step-pop @p1431 :rule scope :premises (@p1430)) % 60.23/60.43 (step-pop @p1432 :rule scope :premises (@p1431)) % 60.23/60.43 (step-pop @p1433 :rule scope :premises (@p1432)) % 60.23/60.43 (step-pop @p1434 :rule scope :premises (@p1433)) % 60.23/60.43 (step-pop @p1435 :rule scope :premises (@p1434)) % 60.23/60.43 (step-pop @p1436 :rule scope :premises (@p1435)) % 60.23/60.43 (step-pop @p1437 :rule scope :premises (@p1436)) % 60.23/60.43 (step-pop @p1438 :rule scope :premises (@p1437)) % 60.23/60.43 (step-pop @p1439 :rule scope :premises (@p1438)) % 60.23/60.43 (step-pop @p1440 :rule scope :premises (@p1439)) % 60.23/60.43 (step-pop @p1441 :rule scope :premises (@p1440)) % 60.23/60.43 (step @p515 :rule process_scope :premises (@p1441) :args (@t345)) % 60.23/60.43 (step @p528 :rule and_intro :premises (@p472 @p353 @p384 @p1407 @p311 @p341 @p375 @p367 @p359 @p464 @p468 @p1408)) % 60.23/60.43 (step @p529 :rule modus_ponens :premises (@p528 @p515)) % 60.23/60.43 (step-pop @p1442 :rule scope :premises (@p529)) % 60.23/60.43 (step-pop @p1443 :rule scope :premises (@p1442)) % 60.23/60.43 (step-pop @p1444 :rule scope :premises (@p1443)) % 60.23/60.43 (step-pop @p1445 :rule scope :premises (@p1444)) % 60.23/60.43 (step-pop @p1446 :rule scope :premises (@p1445)) % 60.23/60.43 (step-pop @p1447 :rule scope :premises (@p1446)) % 60.23/60.43 (step-pop @p1448 :rule scope :premises (@p1447)) % 60.23/60.43 (step-pop @p1449 :rule scope :premises (@p1448)) % 60.23/60.43 (step-pop @p1450 :rule scope :premises (@p1449)) % 60.23/60.43 (step-pop @p1451 :rule scope :premises (@p1450)) % 60.23/60.43 (step-pop @p1452 :rule scope :premises (@p1451)) % 60.23/60.43 (step-pop @p1453 :rule scope :premises (@p1452)) % 60.23/60.43 (step @p530 :rule process_scope :premises (@p1453) :args (@t345)) % 60.23/60.43 (step @p543 :rule implies_elim :premises (@p530)) % 60.23/60.43 (step @p544 :rule cnf_and_neg :args (@t346)) % 60.23/60.43 (step @p545 :rule resolution :premises (@p544 @p543) :args (true @t346)) % 60.23/60.43 (step @p546 :rule reordering :premises (@p545) :args ((or @t334 @t333 @t332 @t331 (not @t336) (not @t339) @t345 @t330 @t329 (not @t341) @t328 @t327 @t326))) % 60.23/60.43 (assume-push @p1454 @t244) % 60.23/60.43 (assume-push @p1455 @t260) % 60.23/60.43 (assume-push @p1456 @t336) % 60.23/60.43 (assume-push @p1457 @t339) % 60.23/60.43 (assume-push @p1458 @t244) % 60.23/60.43 (assume-push @p1459 @t336) % 60.23/60.43 (assume-push @p1460 @t339) % 60.23/60.43 (assume-push @p1461 @t260) % 60.23/60.43 (step @p286 :rule true_intro :premises (@p257)) % 60.23/60.43 (step @p504 :rule symm :premises (@p464)) % 60.23/60.43 (step @p555 :rule symm :premises (@p1455)) % 60.23/60.43 (step @p506 :rule refl :args (tptp.sk6)) % 60.23/60.43 (step @p556 :rule cong :premises (@p506 @p555) :args (@t343)) % 60.23/60.43 (step @p557 :rule trans :premises (@p556 @p468)) % 60.23/60.43 (step @p509 :rule refl :args (@t203)) % 60.23/60.43 (step @p558 :rule cong :premises (@p509 @p557) :args (@t344)) % 60.23/60.43 (step @p559 :rule trans :premises (@p558 @p504)) % 60.23/60.43 (step @p560 :rule cong :premises (@p559) :args (@t347)) % 60.23/60.43 (step @p561 :rule trans :premises (@p560 @p286)) % 60.23/60.43 (step @p562 :rule true_elim :premises (@p561)) % 60.23/60.43 (step-pop @p1462 :rule scope :premises (@p562)) % 60.23/60.43 (step-pop @p1463 :rule scope :premises (@p1462)) % 60.23/60.43 (step-pop @p1464 :rule scope :premises (@p1463)) % 60.23/60.43 (step-pop @p1465 :rule scope :premises (@p1464)) % 60.23/60.43 (step @p563 :rule process_scope :premises (@p1465) :args (@t347)) % 60.23/60.43 (step @p568 :rule and_intro :premises (@p257 @p464 @p468 @p1455)) % 60.23/60.43 (step @p569 :rule modus_ponens :premises (@p568 @p563)) % 60.23/60.43 (step-pop @p1466 :rule scope :premises (@p569)) % 60.23/60.43 (step-pop @p1467 :rule scope :premises (@p1466)) % 60.23/60.43 (step-pop @p1468 :rule scope :premises (@p1467)) % 60.23/60.43 (step-pop @p1469 :rule scope :premises (@p1468)) % 60.23/60.43 (step @p570 :rule process_scope :premises (@p1469) :args (@t347)) % 60.23/60.43 (step @p575 :rule implies_elim :premises (@p570)) % 60.23/60.43 (step @p576 :rule cnf_and_neg :args (@t348)) % 60.23/60.43 (step @p577 :rule resolution :premises (@p576 @p575) :args (true @t348)) % 60.23/60.43 (step @p578 :rule instantiate :premises (@p13) :args (@t349)) % 60.23/60.43 (step @p579 :rule aci_norm :args ((= (or false @t177 @t145 @t47 @t175 @t90 @t351 @t350 @t184) (or @t177 @t145 @t47 @t175 @t90 @t351 @t350 @t184)))) % 60.23/60.43 (step @p580 :rule refl :args (@t184)) % 60.23/60.43 (step @p581 :rule refl :args (@t350)) % 60.23/60.43 (step @p582 :rule refl :args (@t351)) % 60.23/60.43 (step @p583 :rule refl :args (@t90)) % 60.23/60.43 (step @p584 :rule refl :args (@t175)) % 60.23/60.43 (step @p585 :rule refl :args (@t177)) % 60.23/60.43 (step @p586 :rule eq-refl :args (@t188)) % 60.23/60.43 (step @p587 :rule cong :premises (@p586) :args (@t352)) % 60.23/60.43 (step @p588 :rule trans :premises (@p587 @p222)) % 60.23/60.43 (step @p589 :rule nary_cong :premises (@p588 @p585 @p221 @p220 @p584 @p583 @p582 @p581 @p580) :args (@t353)) % 60.23/60.43 (step @p590 :rule trans :premises (@p589 @p579)) % 60.23/60.43 (step @p591 :rule cong :premises (@p590) :args ((forall @t178 @t353))) % 60.23/60.43 (step @p592 :rule quant-var-elim-eq :args ((= (forall @t356 @t355) @t353))) % 60.23/60.43 (step @p593 :rule aci_norm :args ((= @t357 @t355))) % 60.23/60.43 (step @p594 :rule cong :premises (@p593) :args (@t358)) % 60.23/60.43 (step @p595 :rule trans :premises (@p594 @p592)) % 60.23/60.43 (step @p596 :rule cong :premises (@p595) :args (@t359)) % 60.23/60.43 (step @p597 :rule quant-merge-prenex :args ((= @t359 (forall @t191 @t357)))) % 60.23/60.43 (step @p598 :rule symm :premises (@p597)) % 60.23/60.43 (step @p599 :rule trans :premises (@p598 @p596)) % 60.23/60.43 (step @p600 :rule trans :premises (@p599 @p591)) % 60.23/60.43 (step @p601 :rule refl :args (@t186)) % 60.23/60.43 (step @p602 :rule refl :args (@t187)) % 60.23/60.43 (step @p603 :rule eq-symm :args (@t188 @t185)) % 60.23/60.43 (step @p604 :rule cong :premises (@p603) :args (@t189)) % 60.23/60.43 (step @p605 :rule nary_cong :premises (@p604 @p585 @p221 @p220 @p584 @p583 @p602 @p601 @p580) :args (@t190)) % 60.23/60.43 (step @p606 :rule cong :premises (@p605) :args (@t192)) % 60.23/60.43 (step @p607 :rule trans :premises (@p606 @p600)) % 60.23/60.43 (step @p608 :rule eq_resolve :premises (@p178 @p607)) % 60.23/60.43 (step @p609 :rule instantiate :premises (@p608) :args ((@list @t203 tptp.sk6 tptp.nil @t258 @t257))) % 60.23/60.43 (step @p610 :rule instantiate :premises (@p12) :args (@t349)) % 60.23/60.43 (step @p611 :rule cnf_or_pos :args (@t367)) % 60.23/60.43 (step @p612 :rule reordering :premises (@p611) :args ((or @t211 @t212 @t246 @t366 @t364 @t361 @t362 @t360 (not @t367)))) % 60.23/60.43 (step @p613 :rule aci_norm :args ((= (or false @t164 @t47 @t150 @t90 @t369 @t368 @t159) (or @t164 @t47 @t150 @t90 @t369 @t368 @t159)))) % 60.23/60.43 (step @p614 :rule refl :args (@t159)) % 60.23/60.43 (step @p615 :rule refl :args (@t368)) % 60.23/60.43 (step @p616 :rule refl :args (@t369)) % 60.23/60.43 (step @p617 :rule refl :args (@t150)) % 60.23/60.43 (step @p618 :rule eq-refl :args (@t180)) % 60.23/60.43 (step @p619 :rule cong :premises (@p618) :args (@t370)) % 60.23/60.43 (step @p620 :rule trans :premises (@p619 @p222)) % 60.23/60.43 (step @p621 :rule nary_cong :premises (@p620 @p239 @p220 @p617 @p583 @p616 @p615 @p614) :args (@t371)) % 60.23/60.43 (step @p622 :rule trans :premises (@p621 @p613)) % 60.23/60.43 (step @p623 :rule cong :premises (@p622) :args ((forall @t167 @t371))) % 60.23/60.43 (step @p624 :rule quant-var-elim-eq :args ((= (forall @t374 @t373) @t371))) % 60.23/60.43 (step @p625 :rule aci_norm :args ((= @t375 @t373))) % 60.23/60.43 (step @p626 :rule cong :premises (@p625) :args (@t376)) % 60.23/60.43 (step @p627 :rule trans :premises (@p626 @p624)) % 60.23/60.43 (step @p628 :rule cong :premises (@p627) :args (@t377)) % 60.23/60.43 (step @p629 :rule quant-merge-prenex :args ((= @t377 (forall @t178 @t375)))) % 60.23/60.43 (step @p630 :rule symm :premises (@p629)) % 60.23/60.43 (step @p631 :rule trans :premises (@p630 @p628)) % 60.23/60.43 (step @p632 :rule trans :premises (@p631 @p623)) % 60.23/60.43 (step @p633 :rule refl :args (@t179)) % 60.23/60.43 (step @p634 :rule eq-symm :args (@t180 @t176)) % 60.23/60.43 (step @p635 :rule cong :premises (@p634) :args (@t181)) % 60.23/60.43 (step @p636 :rule nary_cong :premises (@p635 @p239 @p220 @p617 @p583 @p633 @p585 @p614) :args (@t182)) % 60.23/60.43 (step @p637 :rule cong :premises (@p636) :args (@t183)) % 60.23/60.43 (step @p638 :rule trans :premises (@p637 @p632)) % 60.23/60.43 (step @p639 :rule eq_resolve :premises (@p177 @p638)) % 60.23/60.43 (step @p640 :rule instantiate :premises (@p639) :args ((@list @t203 tptp.sk6 @t258 @t257))) % 60.23/60.43 (step @p641 :rule cnf_or_pos :args (@t381)) % 60.23/60.43 (step @p642 :rule reordering :premises (@p641) :args ((or @t212 @t246 @t366 @t364 @t380 @t379 @t378 (not @t381)))) % 60.23/60.43 (step @p643 :rule instantiate :premises (@p63) :args ((@list tptp.sk6))) % 60.23/60.43 (step @p644 :rule cnf_or_pos :args (@t384)) % 60.23/60.43 (step @p645 :rule reordering :premises (@p644) :args ((or @t212 @t383 (not @t384)))) % 60.23/60.43 (step @p646 :rule chain_m_resolution :premises (@p645 @p191 @p643) :args (@t383 @t267 (@list @t198 @t384))) % 60.23/60.43 (step @p647 :rule instantiate :premises (@p371) :args ((@list @t258 @t257))) % 60.23/60.43 (step @p648 :rule cnf_or_pos :args (@t386)) % 60.23/60.43 (step @p649 :rule reordering :premises (@p648) :args ((or @t366 @t364 @t385 (not @t386)))) % 60.23/60.43 (step @p650 :rule chain_m_resolution :premises (@p649 @p578 @p610 @p647) :args (@t385 @t216 (@list @t365 @t363 @t386))) % 60.23/60.43 (step @p651 :rule refl :args (@t387)) % 60.23/60.43 (step @p652 :rule refl :args (@t388)) % 60.23/60.43 (step @p653 :rule refl :args (@t389)) % 60.23/60.43 (step @p654 :rule refl :args (@t332)) % 60.23/60.43 (step @p655 :rule bool-double-not-elim :args (@t382)) % 60.23/60.43 (step @p656 :rule nary_cong :premises (@p655 @p654 @p653 @p652 @p651) :args ((or (not @t383) @t332 @t389 @t388 @t387))) % 60.23/60.43 (assume-push @p1470 @t360) % 60.23/60.43 (assume-push @p1471 @t385) % 60.23/60.43 (assume-push @p1472 @t260) % 60.23/60.43 (assume-push @p1473 @t378) % 60.23/60.43 (assume-push @p1474 @t383) % 60.23/60.43 (step @p662 :rule evaluate :args (@t390)) % 60.23/60.43 (step @p663 :rule true_intro :premises (@p1470)) % 60.23/60.43 (step @p664 :rule symm :premises (@p650)) % 60.23/60.43 (step @p665 :rule cong :premises (@p1472) :args (@t391)) % 60.23/60.43 (step @p666 :rule trans :premises (@p665 @p664)) % 60.23/60.43 (step @p506 :rule refl :args (tptp.sk6)) % 60.23/60.43 (step @p667 :rule cong :premises (@p506 @p666) :args ((tptp.lt tptp.sk6 @t391))) % 60.23/60.43 (step @p668 :rule symm :premises (@p665)) % 60.23/60.43 (step @p669 :rule trans :premises (@p1473 @p650 @p668)) % 60.23/60.43 (step @p670 :rule cong :premises (@p506 @p669) :args (@t382)) % 60.23/60.43 (step @p671 :rule false_intro :premises (@p646)) % 60.23/60.43 (step @p672 :rule symm :premises (@p671)) % 60.23/60.43 (step @p673 :rule trans :premises (@p672 @p670 @p667 @p663)) % 60.23/60.43 (step @p674 false :rule eq_resolve :premises (@p673 @p662)) % 60.23/60.43 (step-pop @p1475 :rule scope :premises (@p674)) % 60.23/60.43 (step-pop @p1476 :rule scope :premises (@p1475)) % 60.23/60.43 (step-pop @p1477 :rule scope :premises (@p1476)) % 60.23/60.43 (step-pop @p1478 :rule scope :premises (@p1477)) % 60.23/60.43 (step-pop @p1479 :rule scope :premises (@p1478)) % 60.23/60.43 (step @p675 :rule process_scope :premises (@p1479) :args (false)) % 60.23/60.43 (assume-push @p1480 @t383) % 60.23/60.43 (assume-push @p1481 @t260) % 60.23/60.43 (assume-push @p1482 @t385) % 60.23/60.43 (assume-push @p1483 @t378) % 60.23/60.43 (assume-push @p1484 @t360) % 60.23/60.43 (step @p686 :rule and_intro :premises (@p1484 @p650 @p1481 @p1483 @p646)) % 60.23/60.43 (step-pop @p1485 :rule scope :premises (@p686)) % 60.23/60.43 (step-pop @p1486 :rule scope :premises (@p1485)) % 60.23/60.43 (step-pop @p1487 :rule scope :premises (@p1486)) % 60.23/60.43 (step-pop @p1488 :rule scope :premises (@p1487)) % 60.23/60.43 (step-pop @p1489 :rule scope :premises (@p1488)) % 60.23/60.43 (step @p687 :rule process_scope :premises (@p1489) :args (@t392)) % 60.23/60.43 (step @p693 :rule implies_elim :premises (@p687)) % 60.23/60.43 (step @p694 :rule resolution :premises (@p693 @p675) :args (true @t392)) % 60.23/60.43 (step @p695 :rule not_and :premises (@p694)) % 60.23/60.43 (step @p696 :rule eq_resolve :premises (@p695 @p656)) % 60.23/60.43 (step @p697 :rule chain_m_resolution :premises (@p696 @p650 @p646 @p642 @p610 @p640 @p578 @p254 @p191 @p612 @p610 @p609 @p578 @p254 @p191 @p8 @p577 @p468 @p464 @p257 @p546 @p384 @p472 @p375 @p367 @p359 @p353 @p468 @p341 @p464 @p311 @p460 @p384 @p379 @p375 @p367 @p359 @p353 @p341 @p311 @p303 @p257) :args ((or @t333 @t332) (@list false true false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false) (@list @t385 @t382 @t378 @t363 @t381 @t365 @t239 @t198 @t360 @t363 @t367 @t365 @t239 @t198 @t1 @t347 @t339 @t336 @t244 @t345 @t315 @t341 @t307 @t304 @t297 @t291 @t339 @t284 @t336 @t265 @t324 @t315 @t310 @t307 @t304 @t297 @t291 @t284 @t265 @t262 @t244))) % 60.23/60.43 (step @p698 :rule instantiate :premises (@p316) :args (@t349)) % 60.23/60.43 (step @p699 :rule cnf_or_pos :args (@t394)) % 60.23/60.43 (step @p700 :rule reordering :premises (@p699) :args ((or @t247 @t393 @t260 (not @t394)))) % 60.23/60.43 (assume-push @p1490 @t395) % 60.23/60.43 (step-pop @p1491 :rule scope :premises (@p698)) % 60.23/60.43 (step @p702 :rule process_scope :premises (@p1491) :args (@t394)) % 60.23/60.43 (step @p704 :rule implies_elim :premises (@p702)) % 60.23/60.43 (step @p705 :rule instantiate :premises (@p316) :args (@t396)) % 60.23/60.43 (step @p706 :rule cnf_or_pos :args (@t402)) % 60.23/60.43 (step @p707 :rule reordering :premises (@p706) :args ((or @t240 @t397 @t401 (not @t402)))) % 60.23/60.43 (step @p708 :rule eq-symm :args (@t403 @t404)) % 60.23/60.43 (step @p709 :rule refl :args (@t397)) % 60.23/60.43 (step @p710 :rule refl :args (@t240)) % 60.23/60.43 (step @p711 :rule refl :args (@t241)) % 60.23/60.43 (step @p712 :rule nary_cong :premises (@p711 @p710 @p709 @p708) :args (@t405)) % 60.23/60.43 (step @p713 :rule refl :args (@t123)) % 60.23/60.43 (step @p714 :rule cong :premises (@p713 @p712) :args ((=> @t123 @t405))) % 60.23/60.43 (assume-push @p1492 @t123) % 60.23/60.43 (step @p716 :rule instantiate :premises (@p120) :args (@t234)) % 60.23/60.43 (step-pop @p1493 :rule scope :premises (@p716)) % 60.23/60.43 (step @p717 :rule process_scope :premises (@p1493) :args (@t405)) % 60.23/60.43 (step @p719 :rule eq_resolve :premises (@p717 @p714)) % 60.23/60.43 (step @p720 :rule implies_elim :premises (@p719)) % 60.23/60.43 (step @p721 :rule chain_m_resolution :premises (@p720 @p120) :args (@t407 @t408 @t409)) % 60.23/60.43 (step @p722 :rule cnf_or_pos :args (@t407)) % 60.23/60.43 (step @p723 :rule reordering :premises (@p722) :args ((or @t240 @t397 @t241 @t406 (not @t407)))) % 60.23/60.43 (step @p724 :rule eq-symm :args (@t54 @t2)) % 60.23/60.43 (step @p725 :rule nary_cong :premises (@p220 @p724) :args (@t55)) % 60.23/60.43 (step @p726 :rule cong :premises (@p725) :args (@t56)) % 60.23/60.43 (step @p727 :rule eq_resolve :premises (@p74 @p726)) % 60.23/60.43 (step @p728 :rule instantiate :premises (@p727) :args (@t396)) % 60.23/60.43 (step @p729 :rule cnf_or_pos :args (@t411)) % 60.23/60.43 (step @p730 :rule reordering :premises (@p729) :args ((or @t240 @t410 (not @t411)))) % 60.23/60.43 (step @p731 :rule chain_m_resolution :premises (@p730 @p192 @p728) :args (@t410 @t267 (@list @t199 @t411))) % 60.23/60.43 (step @p732 :rule eq-symm :args (@t137 @t2)) % 60.23/60.43 (step @p733 :rule refl :args (@t133)) % 60.23/60.43 (step @p734 :rule nary_cong :premises (@p733 @p198 @p220 @p732) :args (@t138)) % 60.23/60.43 (step @p735 :rule cong :premises (@p734) :args (@t139)) % 60.23/60.43 (step @p736 :rule eq_resolve :premises (@p129 @p735)) % 60.23/60.43 (step @p737 :rule instantiate :premises (@p736) :args (@t412)) % 60.23/60.43 (step @p738 :rule instantiate :premises (@p61) :args (@t349)) % 60.23/60.43 (step @p739 :rule cnf_or_pos :args (@t414)) % 60.23/60.43 (step @p740 :rule reordering :premises (@p739) :args ((or @t247 @t413 (not @t414)))) % 60.23/60.43 (step @p741 :rule chain_m_resolution :premises (@p740 @p193 @p738) :args (@t413 @t267 (@list @t200 @t414))) % 60.23/60.43 (step @p742 :rule cnf_or_pos :args (@t419)) % 60.23/60.43 (step @p743 :rule factoring :premises (@p742)) % 60.23/60.43 (step @p744 :rule reordering :premises (@p743) :args ((or @t247 @t418 @t417 (not @t419)))) % 60.23/60.43 (step @p745 :rule chain_m_resolution :premises (@p744 @p193 @p741 @p737) :args (@t417 @t216 (@list @t200 @t413 @t419))) % 60.23/60.43 (step @p746 :rule instantiate :premises (@p13) :args (@t396)) % 60.23/60.43 (step @p747 :rule instantiate :premises (@p363) :args (@t420)) % 60.23/60.43 (step @p748 :rule instantiate :premises (@p12) :args (@t396)) % 60.23/60.43 (step @p749 :rule cnf_or_pos :args (@t426)) % 60.23/60.43 (step @p750 :rule reordering :premises (@p749) :args ((or @t423 @t425 @t421 (not @t426)))) % 60.23/60.43 (step @p751 :rule chain_m_resolution :premises (@p750 @p746 @p748 @p747) :args (@t421 @t216 (@list @t422 @t424 @t426))) % 60.23/60.43 (step @p752 :rule instantiate :premises (@p146) :args ((@list tptp.sk7 @t415 tptp.sk8))) % 60.23/60.43 (step @p753 :rule instantiate :premises (@p51) :args (@t412)) % 60.23/60.43 (step @p754 :rule cnf_or_pos :args (@t432)) % 60.23/60.43 (step @p755 :rule reordering :premises (@p754) :args ((or @t240 @t247 @t431 @t429 (not @t432)))) % 60.23/60.43 (step @p756 :rule chain_m_resolution :premises (@p755 @p192 @p193 @p753 @p752) :args (@t429 @t338 (@list @t199 @t200 @t430 @t432))) % 60.23/60.43 (step @p757 :rule eq-symm :args (@t415 tptp.nil)) % 60.23/60.43 (step @p758 :rule refl :args (@t211)) % 60.23/60.43 (step @p759 :rule refl :args (@t247)) % 60.23/60.43 (step @p760 :rule refl :args (@t431)) % 60.23/60.43 (step @p761 :rule eq-symm :args (@t416 @t433)) % 60.23/60.43 (step @p762 :rule cong :premises (@p761) :args (@t434)) % 60.23/60.43 (step @p763 :rule nary_cong :premises (@p762 @p760 @p759 @p758 @p757) :args (@t435)) % 60.23/60.43 (step @p764 :rule refl :args (@t160)) % 60.23/60.43 (step @p765 :rule cong :premises (@p764 @p763) :args ((=> @t160 @t435))) % 60.23/60.43 (assume-push @p1494 @t160) % 60.23/60.43 (step @p767 :rule instantiate :premises (@p147) :args ((@list tptp.sk8 @t415 tptp.nil))) % 60.23/60.43 (step-pop @p1495 :rule scope :premises (@p767)) % 60.23/60.43 (step @p768 :rule process_scope :premises (@p1495) :args (@t435)) % 60.23/60.43 (step @p770 :rule eq_resolve :premises (@p768 @p765)) % 60.23/60.43 (step @p771 :rule implies_elim :premises (@p770)) % 60.23/60.43 (step @p772 :rule chain_m_resolution :premises (@p771 @p147) :args (@t439 @t408 @t440)) % 60.23/60.43 (step @p773 :rule instantiate :premises (@p307) :args (@t349)) % 60.23/60.43 (step @p774 :rule cnf_or_pos :args (@t442)) % 60.23/60.43 (step @p775 :rule reordering :premises (@p774) :args ((or @t247 @t441 (not @t442)))) % 60.23/60.43 (step @p776 :rule chain_m_resolution :premises (@p775 @p193 @p773) :args (@t441 @t267 (@list @t200 @t442))) % 60.23/60.43 (step @p777 :rule symm :premises (@p776)) % 60.23/60.43 (step @p778 :rule trans :premises (@p777 @p745)) % 60.23/60.43 (step @p779 :rule cnf_or_pos :args (@t439)) % 60.23/60.43 (step @p780 :rule reordering :premises (@p779) :args ((or @t211 @t247 @t431 @t438 @t436 (not @t439)))) % 60.23/60.43 (step @p781 :rule chain_m_resolution :premises (@p780 @p8 @p193 @p753 @p778 @p772) :args (@t436 @t249 (@list @t1 @t200 @t430 @t437 @t439))) % 60.23/60.43 (assume-push @p1496 @t410) % 60.23/60.43 (assume-push @p1497 @t393) % 60.23/60.43 (assume-push @p1498 @t401) % 60.23/60.43 (assume-push @p1499 @t417) % 60.23/60.43 (assume-push @p1500 @t422) % 60.23/60.43 (assume-push @p1501 @t436) % 60.23/60.43 (assume-push @p1502 @t421) % 60.23/60.43 (assume-push @p1503 @t429) % 60.23/60.43 (assume-push @p1504 @t422) % 60.23/60.43 (assume-push @p1505 @t421) % 60.23/60.43 (assume-push @p1506 @t401) % 60.23/60.43 (assume-push @p1507 @t410) % 60.23/60.43 (assume-push @p1508 @t393) % 60.23/60.43 (assume-push @p1509 @t436) % 60.23/60.43 (assume-push @p1510 @t429) % 60.23/60.43 (assume-push @p1511 @t417) % 60.23/60.43 (step @p798 :rule true_intro :premises (@p746)) % 60.23/60.43 (step @p799 :rule symm :premises (@p751)) % 60.23/60.43 (step @p800 :rule cong :premises (@p1498) :args (@t443)) % 60.23/60.43 (step @p801 :rule trans :premises (@p800 @p799)) % 60.23/60.43 (step @p802 :rule cong :premises (@p801) :args ((tptp.ssList @t443))) % 60.23/60.43 (step @p803 :rule symm :premises (@p731)) % 60.23/60.43 (step @p804 :rule refl :args (tptp.sk7)) % 60.23/60.43 (step @p805 :rule symm :premises (@p781)) % 60.23/60.43 (step @p806 :rule cong :premises (@p805 @p804) :args (@t427)) % 60.23/60.43 (step @p807 :rule trans :premises (@p806 @p803)) % 60.23/60.43 (step @p808 :rule symm :premises (@p1497)) % 60.23/60.43 (step @p809 :rule cong :premises (@p808 @p807) :args (@t428)) % 60.23/60.43 (step @p810 :rule cong :premises (@p745 @p804) :args (@t444)) % 60.23/60.43 (step @p811 :rule trans :premises (@p810 @p756 @p809 @p803)) % 60.23/60.43 (step @p812 :rule cong :premises (@p811) :args (@t445)) % 60.23/60.43 (step @p813 :rule cong :premises (@p812) :args (@t446)) % 60.23/60.43 (step @p814 :rule trans :premises (@p813 @p802 @p798)) % 60.23/60.43 (step @p815 :rule true_elim :premises (@p814)) % 60.23/60.43 (step-pop @p1512 :rule scope :premises (@p815)) % 60.23/60.43 (step-pop @p1513 :rule scope :premises (@p1512)) % 60.23/60.43 (step-pop @p1514 :rule scope :premises (@p1513)) % 60.23/60.43 (step-pop @p1515 :rule scope :premises (@p1514)) % 60.23/60.43 (step-pop @p1516 :rule scope :premises (@p1515)) % 60.23/60.43 (step-pop @p1517 :rule scope :premises (@p1516)) % 60.23/60.43 (step-pop @p1518 :rule scope :premises (@p1517)) % 60.23/60.43 (step-pop @p1519 :rule scope :premises (@p1518)) % 60.23/60.43 (step @p816 :rule process_scope :premises (@p1519) :args (@t446)) % 60.23/60.43 (step @p825 :rule and_intro :premises (@p746 @p751 @p1498 @p731 @p1497 @p781 @p756 @p745)) % 60.23/60.43 (step @p826 :rule modus_ponens :premises (@p825 @p816)) % 60.23/60.43 (step-pop @p1520 :rule scope :premises (@p826)) % 60.23/60.43 (step-pop @p1521 :rule scope :premises (@p1520)) % 60.23/60.43 (step-pop @p1522 :rule scope :premises (@p1521)) % 60.23/60.43 (step-pop @p1523 :rule scope :premises (@p1522)) % 60.23/60.43 (step-pop @p1524 :rule scope :premises (@p1523)) % 60.23/60.43 (step-pop @p1525 :rule scope :premises (@p1524)) % 60.23/60.43 (step-pop @p1526 :rule scope :premises (@p1525)) % 60.23/60.43 (step-pop @p1527 :rule scope :premises (@p1526)) % 60.23/60.43 (step @p827 :rule process_scope :premises (@p1527) :args (@t446)) % 60.23/60.43 (step @p836 :rule implies_elim :premises (@p827)) % 60.23/60.43 (step @p837 :rule cnf_and_neg :args (@t447)) % 60.23/60.43 (step @p838 :rule resolution :premises (@p837 @p836) :args (true @t447)) % 60.23/60.43 (step @p839 :rule reordering :premises (@p838) :args ((or @t454 @t453 @t452 @t451 @t423 @t446 @t450 @t449 @t448))) % 60.23/60.43 (step @p840 :rule instantiate :premises (@p146) :args ((@list @t201 @t202 tptp.sk7))) % 60.23/60.43 (step @p841 :rule cnf_or_pos :args (@t458)) % 60.23/60.43 (step @p842 :rule reordering :premises (@p841) :args ((or @t240 @t241 @t219 @t457 (not @t458)))) % 60.23/60.43 (step @p843 :rule chain_m_resolution :premises (@p842 @p192 @p251 @p212 @p840) :args (@t457 @t338 (@list @t199 @t236 @t217 @t458))) % 60.23/60.43 (step @p844 :rule eq-symm :args (@t459 @t403)) % 60.23/60.43 (step @p845 :rule refl :args (@t460)) % 60.23/60.43 (step @p846 :rule refl :args (@t246)) % 60.23/60.43 (step @p847 :rule refl :args (@t219)) % 60.23/60.43 (step @p848 :rule nary_cong :premises (@p847 @p846 @p845 @p844) :args (@t461)) % 60.23/60.43 (step @p849 :rule cong :premises (@p713 @p848) :args ((=> @t123 @t461))) % 60.23/60.43 (assume-push @p1528 @t123) % 60.23/60.43 (step @p851 :rule instantiate :premises (@p120) :args (@t268)) % 60.23/60.43 (step-pop @p1529 :rule scope :premises (@p851)) % 60.23/60.43 (step @p852 :rule process_scope :premises (@p1529) :args (@t461)) % 60.23/60.43 (step @p854 :rule eq_resolve :premises (@p852 @p849)) % 60.23/60.43 (step @p855 :rule implies_elim :premises (@p854)) % 60.23/60.43 (step @p856 :rule chain_m_resolution :premises (@p855 @p120) :args (@t463 @t408 @t409)) % 60.23/60.43 (step @p857 :rule instantiate :premises (@p331) :args (@t464)) % 60.23/60.43 (step @p858 :rule instantiate :premises (@p204) :args (@t235)) % 60.23/60.43 (step @p859 :rule cnf_or_pos :args (@t467)) % 60.23/60.43 (step @p860 :rule reordering :premises (@p859) :args ((or @t211 @t237 @t466 (not @t467)))) % 60.23/60.43 (step @p861 :rule chain_m_resolution :premises (@p860 @p8 @p190 @p858) :args (@t466 @t216 (@list @t1 @t197 @t467))) % 60.23/60.43 (step @p862 :rule cnf_or_pos :args (@t469)) % 60.23/60.43 (step @p863 :rule reordering :premises (@p862) :args ((or @t240 @t241 @t465 @t468 (not @t469)))) % 60.23/60.43 (step @p864 :rule chain_m_resolution :premises (@p863 @p192 @p251 @p861 @p857) :args (@t468 @t275 (@list @t199 @t236 @t465 @t469))) % 60.23/60.43 (step @p865 :rule cnf_or_pos :args (@t463)) % 60.23/60.43 (step @p866 :rule reordering :premises (@p865) :args ((or @t219 @t246 @t460 @t462 (not @t463)))) % 60.23/60.43 (step @p867 :rule chain_m_resolution :premises (@p866 @p212 @p254 @p864 @p856) :args (@t462 @t275 (@list @t217 @t239 @t460 @t463))) % 60.23/60.43 (step @p868 :rule instantiate :premises (@p120) :args ((@list tptp.sk8 @t204))) % 60.23/60.43 (step @p869 :rule cnf_or_pos :args (@t471)) % 60.23/60.43 (step @p870 :rule reordering :premises (@p869) :args ((or @t247 @t272 @t276 @t470 (not @t471)))) % 60.23/60.43 (step @p871 :rule chain_m_resolution :premises (@p870 @p193 @p335 @p327 @p868) :args (@t470 @t280 (@list @t200 @t272 @t269 @t471))) % 60.23/60.43 (step @p872 :rule instantiate :premises (@p345) :args (@t420)) % 60.23/60.43 (step @p873 :rule cnf_or_pos :args (@t473)) % 60.23/60.43 (step @p874 :rule reordering :premises (@p873) :args ((or @t423 @t425 @t472 (not @t473)))) % 60.23/60.43 (step @p875 :rule chain_m_resolution :premises (@p874 @p746 @p748 @p872) :args (@t472 @t216 (@list @t422 @t424 @t473))) % 60.23/60.43 (step @p876 :rule instantiate :premises (@p371) :args (@t420)) % 60.23/60.43 (step @p877 :rule cnf_or_pos :args (@t475)) % 60.23/60.43 (step @p878 :rule reordering :premises (@p877) :args ((or @t423 @t425 @t474 (not @t475)))) % 60.23/60.43 (step @p879 :rule chain_m_resolution :premises (@p878 @p746 @p748 @p876) :args (@t474 @t216 (@list @t422 @t424 @t475))) % 60.23/60.43 (step @p880 :rule instantiate :premises (@p307) :args ((@list @t204))) % 60.23/60.43 (step @p881 :rule cnf_or_pos :args (@t478)) % 60.23/60.43 (step @p882 :rule reordering :premises (@p881) :args ((or @t276 @t477 (not @t478)))) % 60.23/60.43 (step @p883 :rule chain_m_resolution :premises (@p882 @p327 @p880) :args (@t477 @t267 (@list @t269 @t478))) % 60.23/60.43 (step @p884 :rule refl :args (@t132)) % 60.23/60.43 (step @p885 :rule nary_cong :premises (@p733 @p884 @p220 @p198 @p270) :args (@t134)) % 60.23/60.43 (step @p886 :rule cong :premises (@p885) :args (@t135)) % 60.23/60.43 (step @p887 :rule eq_resolve :premises (@p126 @p886)) % 60.23/60.43 (step @p888 :rule eq-symm :args (@t203 tptp.sk7)) % 60.23/60.43 (step @p889 :rule refl :args (@t480)) % 60.23/60.43 (step @p890 :rule refl :args (@t482)) % 60.23/60.43 (step @p891 :rule nary_cong :premises (@p890 @p889 @p846 @p710 @p888) :args (@t483)) % 60.23/60.43 (step @p892 :rule refl :args (@t484)) % 60.23/60.43 (step @p893 :rule cong :premises (@p892 @p891) :args ((=> @t484 @t483))) % 60.23/60.43 (assume-push @p1530 @t484) % 60.23/60.43 (step @p895 :rule instantiate :premises (@p887) :args ((@list @t203 tptp.sk7))) % 60.23/60.43 (step-pop @p1531 :rule scope :premises (@p895)) % 60.23/60.43 (step @p896 :rule process_scope :premises (@p1531) :args (@t483)) % 60.23/60.43 (step @p898 :rule eq_resolve :premises (@p896 @p893)) % 60.23/60.43 (step @p899 :rule implies_elim :premises (@p898)) % 60.23/60.43 (step @p900 :rule chain_m_resolution :premises (@p899 @p887) :args (@t486 @t408 (@list @t484))) % 60.23/60.43 (step @p901 :rule refl :args (@t465)) % 60.23/60.43 (step @p902 :rule eq-symm :args (@t487 @t203)) % 60.23/60.43 (step @p903 :rule cong :premises (@p902) :args (@t488)) % 60.23/60.43 (step @p904 :rule nary_cong :premises (@p903 @p758 @p710 @p711 @p901) :args (@t489)) % 60.23/60.43 (step @p905 :rule cong :premises (@p764 @p904) :args ((=> @t160 @t489))) % 60.23/60.43 (assume-push @p1532 @t160) % 60.23/60.43 (step @p907 :rule instantiate :premises (@p147) :args ((@list tptp.sk7 tptp.nil @t202))) % 60.23/60.43 (step-pop @p1533 :rule scope :premises (@p907)) % 60.23/60.43 (step @p908 :rule process_scope :premises (@p1533) :args (@t489)) % 60.23/60.43 (step @p910 :rule eq_resolve :premises (@p908 @p905)) % 60.23/60.43 (step @p911 :rule implies_elim :premises (@p910)) % 60.23/60.43 (step @p912 :rule chain_m_resolution :premises (@p911 @p147) :args (@t492 @t408 @t440)) % 60.23/60.43 (step @p913 :rule cnf_or_pos :args (@t492)) % 60.23/60.43 (step @p914 :rule reordering :premises (@p913) :args ((or @t211 @t240 @t241 @t465 @t491 (not @t492)))) % 60.23/60.43 (step @p915 :rule chain_m_resolution :premises (@p914 @p8 @p192 @p251 @p861 @p912) :args (@t491 @t493 (@list @t1 @t199 @t236 @t465 @t492))) % 60.23/60.43 (step @p916 :rule instantiate :premises (@p307) :args (@t396)) % 60.23/60.43 (step @p917 :rule cnf_or_pos :args (@t495)) % 60.23/60.43 (step @p918 :rule reordering :premises (@p917) :args ((or @t240 @t494 (not @t495)))) % 60.23/60.43 (step @p919 :rule chain_m_resolution :premises (@p918 @p192 @p916) :args (@t494 @t267 (@list @t199 @t495))) % 60.23/60.43 (step @p920 :rule refl :args (@t496)) % 60.23/60.43 (step @p921 :rule bool-double-not-elim :args (@t490)) % 60.23/60.43 (step @p922 :rule refl :args (@t497)) % 60.23/60.43 (step @p923 :rule nary_cong :premises (@p922 @p921 @p920) :args ((or @t497 (not @t491) @t496))) % 60.23/60.43 (assume-push @p1534 @t494) % 60.23/60.43 (assume-push @p1535 @t485) % 60.23/60.43 (assume-push @p1536 @t491) % 60.23/60.43 (step @p662 :rule evaluate :args (@t390)) % 60.23/60.43 (step @p927 :rule symm :premises (@p1535)) % 60.23/60.43 (step @p928 :rule trans :premises (@p927 @p919)) % 60.23/60.43 (step @p929 :rule true_intro :premises (@p928)) % 60.23/60.43 (step @p930 :rule false_intro :premises (@p915)) % 60.23/60.43 (step @p931 :rule symm :premises (@p930)) % 60.23/60.43 (step @p932 :rule trans :premises (@p931 @p929)) % 60.23/60.43 (step @p933 false :rule eq_resolve :premises (@p932 @p662)) % 60.23/60.43 (step-pop @p1537 :rule scope :premises (@p933)) % 60.23/60.43 (step-pop @p1538 :rule scope :premises (@p1537)) % 60.23/60.43 (step-pop @p1539 :rule scope :premises (@p1538)) % 60.23/60.43 (step @p934 :rule process_scope :premises (@p1539) :args (false)) % 60.23/60.43 (assume-push @p1540 @t494) % 60.23/60.43 (assume-push @p1541 @t491) % 60.23/60.43 (assume-push @p1542 @t485) % 60.23/60.43 (step @p941 :rule and_intro :premises (@p919 @p1542 @p915)) % 60.23/60.43 (step-pop @p1543 :rule scope :premises (@p941)) % 60.23/60.43 (step-pop @p1544 :rule scope :premises (@p1543)) % 60.23/60.43 (step-pop @p1545 :rule scope :premises (@p1544)) % 60.23/60.43 (step @p942 :rule process_scope :premises (@p1545) :args (@t498)) % 60.23/60.43 (step @p946 :rule implies_elim :premises (@p942)) % 60.23/60.43 (step @p947 :rule resolution :premises (@p946 @p934) :args (true @t498)) % 60.23/60.43 (step @p948 :rule not_and :premises (@p947)) % 60.23/60.43 (step @p949 :rule eq_resolve :premises (@p948 @p923)) % 60.23/60.43 (step @p950 :rule chain_m_resolution :premises (@p949 @p919 @p915) :args (@t496 (@list false true) (@list @t494 @t490))) % 60.23/60.43 (step @p951 :rule aci_norm :args ((= (or false @t65 @t47 @t500 @t499) (or @t65 @t47 @t500 @t499)))) % 60.23/60.43 (step @p952 :rule refl :args (@t499)) % 60.23/60.43 (step @p953 :rule refl :args (@t500)) % 60.23/60.43 (step @p954 :rule eq-refl :args (@t111)) % 60.23/60.43 (step @p955 :rule cong :premises (@p954) :args (@t501)) % 60.23/60.43 (step @p956 :rule trans :premises (@p955 @p222)) % 60.23/60.43 (step @p957 :rule nary_cong :premises (@p956 @p198 @p220 @p953 @p952) :args (@t502)) % 60.23/60.43 (step @p958 :rule trans :premises (@p957 @p951)) % 60.23/60.43 (step @p959 :rule cong :premises (@p958) :args ((forall @t41 @t502))) % 60.23/60.43 (step @p960 :rule quant-var-elim-eq :args ((= (forall @t503 (or (not (= @t143 @t111)) @t152 @t65 @t47 @t145 @t153)) @t502))) % 60.23/60.43 (step @p961 :rule refl :args (@t153)) % 60.23/60.43 (step @p962 :rule refl :args (@t145)) % 60.23/60.43 (step @p963 :rule refl :args (@t47)) % 60.23/60.43 (step @p964 :rule refl :args (@t65)) % 60.23/60.43 (step @p965 :rule refl :args (@t152)) % 60.23/60.43 (step @p966 :rule eq-symm :args (@t111 @t143)) % 60.23/60.43 (step @p967 :rule cong :premises (@p966) :args (@t152)) % 60.23/60.43 (step @p968 :rule nary_cong :premises (@p967 @p965 @p964 @p963 @p962 @p961) :args (@t504)) % 60.23/60.43 (step @p969 :rule aci_norm :args ((= @t154 @t504))) % 60.23/60.43 (step @p970 :rule trans :premises (@p969 @p968)) % 60.23/60.43 (step @p971 :rule cong :premises (@p970) :args (@t505)) % 60.23/60.43 (step @p972 :rule trans :premises (@p971 @p960)) % 60.23/60.43 (step @p973 :rule cong :premises (@p972) :args (@t506)) % 60.23/60.43 (step @p974 :rule quant-merge-prenex :args ((= @t506 @t155))) % 60.23/60.43 (step @p975 :rule symm :premises (@p974)) % 60.23/60.43 (step @p976 :rule trans :premises (@p975 @p973)) % 60.23/60.43 (step @p977 :rule trans :premises (@p976 @p959)) % 60.23/60.43 (step @p978 :rule eq_resolve :premises (@p141 @p977)) % 60.23/60.43 (step @p979 :rule instantiate :premises (@p978) :args (@t464)) % 60.23/60.43 (step @p980 :rule cnf_or_pos :args (@t507)) % 60.23/60.43 (step @p981 :rule reordering :premises (@p980) :args ((or @t240 @t241 @t246 @t481 (not @t507)))) % 60.23/60.43 (step @p982 :rule chain_m_resolution :premises (@p981 @p192 @p251 @p254 @p979) :args (@t481 @t338 (@list @t199 @t236 @t239 @t507))) % 60.23/60.43 (step @p983 :rule cnf_or_pos :args (@t486)) % 60.23/60.43 (step @p984 :rule reordering :premises (@p983) :args ((or @t240 @t246 @t482 @t485 @t480 (not @t486)))) % 60.23/60.43 (step @p985 :rule chain_m_resolution :premises (@p984 @p192 @p254 @p982 @p950 @p900) :args (@t480 @t493 (@list @t199 @t239 @t481 @t485 @t486))) % 60.23/60.43 (step @p986 :rule refl :args (@t510)) % 60.23/60.43 (step @p987 :rule refl :args (@t448)) % 60.23/60.43 (step @p988 :rule bool-double-not-elim :args (@t479)) % 60.23/60.43 (step @p989 :rule refl :args (@t326)) % 60.23/60.43 (step @p990 :rule refl :args (@t511)) % 60.23/60.43 (step @p991 :rule refl :args (@t327)) % 60.23/60.43 (step @p992 :rule refl :args (@t449)) % 60.23/60.43 (step @p993 :rule refl :args (@t328)) % 60.23/60.43 (step @p994 :rule refl :args (@t512)) % 60.23/60.43 (step @p995 :rule refl :args (@t329)) % 60.23/60.43 (step @p996 :rule refl :args (@t330)) % 60.23/60.43 (step @p997 :rule refl :args (@t513)) % 60.23/60.43 (step @p998 :rule refl :args (@t450)) % 60.23/60.43 (step @p999 :rule refl :args (@t514)) % 60.23/60.43 (step @p1000 :rule refl :args (@t451)) % 60.23/60.43 (step @p1001 :rule refl :args (@t515)) % 60.23/60.43 (step @p1002 :rule refl :args (@t516)) % 60.23/60.43 (step @p1003 :rule refl :args (@t517)) % 60.23/60.43 (step @p1004 :rule refl :args (@t331)) % 60.23/60.43 (step @p1005 :rule refl :args (@t452)) % 60.23/60.43 (step @p1006 :rule refl :args (@t333)) % 60.23/60.43 (step @p1007 :rule refl :args (@t453)) % 60.23/60.43 (step @p1008 :rule refl :args (@t454)) % 60.23/60.43 (step @p1009 :rule refl :args (@t334)) % 60.23/60.43 (step @p1010 :rule nary_cong :premises (@p1009 @p1008 @p1007 @p1006 @p1005 @p1004 @p1003 @p1002 @p1001 @p1000 @p999 @p998 @p997 @p996 @p995 @p994 @p993 @p992 @p991 @p990 @p989 @p988 @p987 @p986) :args ((or @t334 @t454 @t453 @t333 @t452 @t331 @t517 @t516 @t515 @t451 @t514 @t450 @t513 @t330 @t329 @t512 @t328 @t449 @t327 @t511 @t326 (not @t480) @t448 @t510))) % 60.23/60.43 (assume-push @p1546 @t265) % 60.23/60.43 (assume-push @p1547 @t410) % 60.23/60.43 (assume-push @p1548 @t393) % 60.23/60.43 (assume-push @p1549 @t319) % 60.23/60.43 (assume-push @p1550 @t401) % 60.23/60.43 (assume-push @p1551 @t284) % 60.23/60.43 (assume-push @p1552 @t406) % 60.23/60.43 (assume-push @p1553 @t462) % 60.23/60.43 (assume-push @p1554 @t470) % 60.23/60.43 (assume-push @p1555 @t417) % 60.23/60.43 (assume-push @p1556 @t457) % 60.23/60.43 (assume-push @p1557 @t436) % 60.23/60.43 (assume-push @p1558 @t472) % 60.23/60.43 (assume-push @p1559 @t297) % 60.23/60.43 (assume-push @p1560 @t291) % 60.23/60.43 (assume-push @p1561 @t477) % 60.23/60.43 (assume-push @p1562 @t315) % 60.23/60.43 (assume-push @p1563 @t421) % 60.23/60.43 (assume-push @p1564 @t304) % 60.23/60.43 (assume-push @p1565 @t474) % 60.23/60.43 (assume-push @p1566 @t307) % 60.23/60.43 (assume-push @p1567 @t480) % 60.23/60.43 (assume-push @p1568 @t429) % 60.23/60.43 (assume-push @p1569 @t480) % 60.23/60.43 (assume-push @p1570 @t401) % 60.23/60.43 (assume-push @p1571 @t472) % 60.23/60.43 (assume-push @p1572 @t474) % 60.23/60.43 (assume-push @p1573 @t406) % 60.23/60.43 (assume-push @p1574 @t462) % 60.23/60.43 (assume-push @p1575 @t470) % 60.23/60.43 (assume-push @p1576 @t291) % 60.23/60.43 (assume-push @p1577 @t315) % 60.23/60.43 (assume-push @p1578 @t319) % 60.23/60.43 (assume-push @p1579 @t265) % 60.23/60.43 (assume-push @p1580 @t284) % 60.23/60.43 (assume-push @p1581 @t307) % 60.23/60.43 (assume-push @p1582 @t304) % 60.23/60.43 (assume-push @p1583 @t297) % 60.23/60.43 (assume-push @p1584 @t457) % 60.23/60.43 (assume-push @p1585 @t393) % 60.23/60.43 (assume-push @p1586 @t477) % 60.23/60.43 (assume-push @p1587 @t421) % 60.23/60.43 (assume-push @p1588 @t410) % 60.23/60.43 (assume-push @p1589 @t436) % 60.23/60.43 (assume-push @p1590 @t429) % 60.23/60.43 (assume-push @p1591 @t417) % 60.23/60.43 (step @p1057 :rule false_intro :premises (@p1567)) % 60.23/60.43 (step @p509 :rule refl :args (@t203)) % 60.23/60.43 (step @p1058 :rule symm :premises (@p1550)) % 60.23/60.43 (step @p1059 :rule symm :premises (@p875)) % 60.23/60.43 (step @p799 :rule symm :premises (@p751)) % 60.23/60.43 (step @p1060 :rule cong :premises (@p1550) :args (@t443)) % 60.23/60.43 (step @p803 :rule symm :premises (@p731)) % 60.23/60.43 (step @p804 :rule refl :args (tptp.sk7)) % 60.23/60.43 (step @p805 :rule symm :premises (@p781)) % 60.23/60.43 (step @p806 :rule cong :premises (@p805 @p804) :args (@t427)) % 60.23/60.43 (step @p807 :rule trans :premises (@p806 @p803)) % 60.23/60.43 (step @p1061 :rule symm :premises (@p1548)) % 60.23/60.43 (step @p1062 :rule cong :premises (@p1061 @p807) :args (@t428)) % 60.23/60.43 (step @p810 :rule cong :premises (@p745 @p804) :args (@t444)) % 60.23/60.43 (step @p1063 :rule trans :premises (@p810 @p756 @p1062 @p803)) % 60.23/60.43 (step @p1064 :rule cong :premises (@p1063) :args (@t445)) % 60.23/60.43 (step @p1065 :rule trans :premises (@p1064 @p1060 @p799)) % 60.23/60.43 (step @p420 :rule refl :args (tptp.nil)) % 60.23/60.43 (step @p1066 :rule symm :premises (@p879)) % 60.23/60.43 (step @p1067 :rule cong :premises (@p1550) :args (@t404)) % 60.23/60.43 (step @p1068 :rule symm :premises (@p1552)) % 60.23/60.43 (step @p1069 :rule symm :premises (@p867)) % 60.23/60.43 (step @p1070 :rule trans :premises (@p871 @p1069 @p1068 @p1067 @p1066)) % 60.23/60.43 (step @p1071 :rule cong :premises (@p1070 @p420) :args (@t289)) % 60.23/60.43 (step @p406 :rule symm :premises (@p353)) % 60.23/60.43 (step @p407 :rule symm :premises (@p384)) % 60.23/60.43 (step @p408 :rule symm :premises (@p311)) % 60.23/60.43 (step @p1072 :rule trans :premises (@p408 @p1549)) % 60.23/60.43 (step @p1073 :rule cong :premises (@p1072) :args (@t320)) % 60.23/60.43 (step @p411 :rule cong :premises (@p311) :args (@t321)) % 60.23/60.43 (step @p1074 :rule trans :premises (@p411 @p1073 @p407)) % 60.23/60.43 (step @p413 :rule refl :args (@t289)) % 60.23/60.43 (step @p1075 :rule cong :premises (@p413 @p1074) :args (@t322)) % 60.23/60.43 (step @p415 :rule symm :premises (@p411)) % 60.23/60.43 (step @p416 :rule symm :premises (@p341)) % 60.23/60.43 (step @p417 :rule trans :premises (@p416 @p311)) % 60.23/60.43 (step @p418 :rule cong :premises (@p417) :args (@t303)) % 60.23/60.43 (step @p419 :rule trans :premises (@p367 @p418 @p415)) % 60.23/60.43 (step @p421 :rule cong :premises (@p408) :args (@t323)) % 60.23/60.43 (step @p422 :rule cong :premises (@p417) :args (@t306)) % 60.23/60.43 (step @p423 :rule trans :premises (@p375 @p422 @p421)) % 60.23/60.43 (step @p424 :rule cong :premises (@p423 @p420) :args (@t295)) % 60.23/60.43 (step @p425 :rule cong :premises (@p424 @p419) :args (@t296)) % 60.23/60.43 (step @p1076 :rule trans :premises (@p408 @p341 @p359 @p425 @p1075 @p406 @p1071)) % 60.23/60.43 (step @p1077 :rule refl :args (tptp.sk8)) % 60.23/60.43 (step @p1078 :rule symm :premises (@p843)) % 60.23/60.43 (step @p1079 :rule cong :premises (@p1078 @p1077) :args (@t518)) % 60.23/60.43 (step @p1080 :rule cong :premises (@p843 @p1548) :args (@t476)) % 60.23/60.43 (step @p1081 :rule trans :premises (@p883 @p1080 @p1079 @p311)) % 60.23/60.43 (step @p1082 :rule trans :premises (@p1081 @p1076)) % 60.23/60.43 (step @p1083 :rule cong :premises (@p1082 @p1065) :args (@t508)) % 60.23/60.43 (step @p1084 :rule trans :premises (@p1083 @p1059 @p1058)) % 60.23/60.43 (step @p1085 :rule cong :premises (@p1084 @p509) :args (@t509)) % 60.23/60.43 (step @p1086 :rule trans :premises (@p1085 @p1057)) % 60.23/60.43 (step @p1087 :rule false_elim :premises (@p1086)) % 60.23/60.43 (step-pop @p1592 :rule scope :premises (@p1087)) % 60.23/60.43 (step-pop @p1593 :rule scope :premises (@p1592)) % 60.23/60.43 (step-pop @p1594 :rule scope :premises (@p1593)) % 60.23/60.43 (step-pop @p1595 :rule scope :premises (@p1594)) % 60.23/60.43 (step-pop @p1596 :rule scope :premises (@p1595)) % 60.23/60.43 (step-pop @p1597 :rule scope :premises (@p1596)) % 60.23/60.43 (step-pop @p1598 :rule scope :premises (@p1597)) % 60.23/60.43 (step-pop @p1599 :rule scope :premises (@p1598)) % 60.23/60.43 (step-pop @p1600 :rule scope :premises (@p1599)) % 60.23/60.43 (step-pop @p1601 :rule scope :premises (@p1600)) % 60.23/60.43 (step-pop @p1602 :rule scope :premises (@p1601)) % 60.23/60.43 (step-pop @p1603 :rule scope :premises (@p1602)) % 60.23/60.43 (step-pop @p1604 :rule scope :premises (@p1603)) % 60.23/60.43 (step-pop @p1605 :rule scope :premises (@p1604)) % 60.23/60.43 (step-pop @p1606 :rule scope :premises (@p1605)) % 60.23/60.43 (step-pop @p1607 :rule scope :premises (@p1606)) % 60.23/60.43 (step-pop @p1608 :rule scope :premises (@p1607)) % 60.23/60.43 (step-pop @p1609 :rule scope :premises (@p1608)) % 60.23/60.43 (step-pop @p1610 :rule scope :premises (@p1609)) % 60.23/60.43 (step-pop @p1611 :rule scope :premises (@p1610)) % 60.23/60.43 (step-pop @p1612 :rule scope :premises (@p1611)) % 60.23/60.43 (step-pop @p1613 :rule scope :premises (@p1612)) % 60.23/60.43 (step-pop @p1614 :rule scope :premises (@p1613)) % 60.23/60.43 (step @p1088 :rule process_scope :premises (@p1614) :args (@t510)) % 60.23/60.43 (step @p1112 :rule and_intro :premises (@p1567 @p1550 @p875 @p879 @p1552 @p867 @p871 @p353 @p384 @p1549 @p311 @p341 @p375 @p367 @p359 @p843 @p1548 @p883 @p751 @p731 @p781 @p756 @p745)) % 60.23/60.43 (step @p1113 :rule modus_ponens :premises (@p1112 @p1088)) % 60.23/60.43 (step-pop @p1615 :rule scope :premises (@p1113)) % 60.23/60.43 (step-pop @p1616 :rule scope :premises (@p1615)) % 60.23/60.43 (step-pop @p1617 :rule scope :premises (@p1616)) % 60.23/60.43 (step-pop @p1618 :rule scope :premises (@p1617)) % 60.23/60.43 (step-pop @p1619 :rule scope :premises (@p1618)) % 60.23/60.43 (step-pop @p1620 :rule scope :premises (@p1619)) % 60.23/60.43 (step-pop @p1621 :rule scope :premises (@p1620)) % 60.23/60.43 (step-pop @p1622 :rule scope :premises (@p1621)) % 60.23/60.43 (step-pop @p1623 :rule scope :premises (@p1622)) % 60.23/60.43 (step-pop @p1624 :rule scope :premises (@p1623)) % 60.23/60.43 (step-pop @p1625 :rule scope :premises (@p1624)) % 60.23/60.43 (step-pop @p1626 :rule scope :premises (@p1625)) % 60.23/60.43 (step-pop @p1627 :rule scope :premises (@p1626)) % 60.23/60.43 (step-pop @p1628 :rule scope :premises (@p1627)) % 60.23/60.43 (step-pop @p1629 :rule scope :premises (@p1628)) % 60.23/60.43 (step-pop @p1630 :rule scope :premises (@p1629)) % 60.23/60.43 (step-pop @p1631 :rule scope :premises (@p1630)) % 60.23/60.43 (step-pop @p1632 :rule scope :premises (@p1631)) % 60.23/60.43 (step-pop @p1633 :rule scope :premises (@p1632)) % 60.23/60.43 (step-pop @p1634 :rule scope :premises (@p1633)) % 60.23/60.43 (step-pop @p1635 :rule scope :premises (@p1634)) % 60.23/60.43 (step-pop @p1636 :rule scope :premises (@p1635)) % 60.23/60.43 (step-pop @p1637 :rule scope :premises (@p1636)) % 60.23/60.43 (step @p1114 :rule process_scope :premises (@p1637) :args (@t510)) % 60.23/60.43 (step @p1138 :rule implies_elim :premises (@p1114)) % 60.23/60.43 (step @p1139 :rule cnf_and_neg :args (@t519)) % 60.23/60.43 (step @p1140 :rule resolution :premises (@p1139 @p1138) :args (true @t519)) % 60.23/60.43 (step @p1141 :rule eq_resolve :premises (@p1140 @p1010)) % 60.23/60.43 (step @p1142 :rule reordering :premises (@p1141) :args ((or @t334 @t454 @t453 @t333 @t452 @t331 @t517 @t516 @t515 @t451 @t514 @t479 @t450 @t513 @t330 @t329 @t512 @t328 @t449 @t327 @t511 @t326 @t448 @t510))) % 60.23/60.43 (step @p1143 :rule instantiate :premises (@p978) :args (@t271)) % 60.23/60.43 (step @p1144 :rule cnf_or_pos :args (@t521)) % 60.23/60.43 (step @p1145 :rule reordering :premises (@p1144) :args ((or @t219 @t246 @t276 @t520 (not @t521)))) % 60.23/60.43 (step @p1146 :rule chain_m_resolution :premises (@p1145 @p212 @p254 @p327 @p1143) :args (@t520 @t338 (@list @t217 @t239 @t269 @t521))) % 60.23/60.43 (step @p1147 :rule instantiate :premises (@p134) :args ((@list @t204 @t203 @t445))) % 60.23/60.43 (step @p1148 :rule cnf_or_pos :args (@t524)) % 60.23/60.43 (step @p1149 :rule reordering :premises (@p1148) :args ((or @t246 @t276 @t523 @t522 @t509 (not @t524)))) % 60.23/60.43 (step @p1150 :rule chain_m_resolution :premises (@p1149 @p1147 @p1146 @p327 @p254 @p1142 @p985 @p781 @p384 @p883 @p756 @p375 @p367 @p359 @p879 @p751 @p875 @p353 @p341 @p871 @p867 @p843 @p745 @p731 @p311 @p839 @p781 @p756 @p751 @p746 @p745 @p731 @p723 @p251 @p721 @p192 @p707 @p705 @p192 @p700 @p193 @p704 @p316 @p697) :args ((or @t397 @t333) (@list false false false false true true false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false true) (@list @t524 @t520 @t269 @t239 @t509 @t479 @t436 @t315 @t477 @t429 @t307 @t304 @t297 @t474 @t421 @t472 @t291 @t284 @t470 @t462 @t457 @t417 @t410 @t265 @t446 @t436 @t429 @t421 @t422 @t417 @t410 @t406 @t236 @t407 @t199 @t401 @t402 @t199 @t393 @t200 @t394 @t395 @t260))) % 60.23/60.43 (step @p1151 :rule instantiate :premises (@p363) :args (@t235)) % 60.23/60.43 (step @p1152 :rule cnf_or_pos :args (@t526)) % 60.23/60.43 (step @p1153 :rule reordering :premises (@p1152) :args ((or @t211 @t237 @t525 (not @t526)))) % 60.23/60.43 (step @p1154 :rule chain_m_resolution :premises (@p1153 @p8 @p190 @p1151) :args (@t525 @t216 (@list @t1 @t197 @t526))) % 60.23/60.43 (step @p1155 :rule instantiate :premises (@p363) :args ((@list tptp.sk6 tptp.sk7))) % 60.23/60.43 (step @p1156 :rule cnf_or_pos :args (@t529)) % 60.23/60.43 (step @p1157 :rule reordering :premises (@p1156) :args ((or @t212 @t240 @t528 (not @t529)))) % 60.23/60.43 (step @p1158 :rule chain_m_resolution :premises (@p1157 @p191 @p192 @p1155) :args (@t528 @t216 (@list @t198 @t199 @t529))) % 60.23/60.43 (step @p1159 :rule instantiate :premises (@p345) :args (@t235)) % 60.23/60.43 (step @p1160 :rule cnf_or_pos :args (@t532)) % 60.23/60.43 (step @p1161 :rule reordering :premises (@p1160) :args ((or @t211 @t237 @t531 (not @t532)))) % 60.23/60.43 (step @p1162 :rule chain_m_resolution :premises (@p1161 @p8 @p190 @p1159) :args (@t531 @t216 (@list @t1 @t197 @t532))) % 60.23/60.43 (step @p1163 :rule instantiate :premises (@p345) :args (@t210)) % 60.23/60.43 (step @p1164 :rule cnf_or_pos :args (@t535)) % 60.23/60.43 (step @p1165 :rule reordering :premises (@p1164) :args ((or @t211 @t212 @t534 (not @t535)))) % 60.23/60.43 (step @p1166 :rule chain_m_resolution :premises (@p1165 @p8 @p191 @p1163) :args (@t534 @t216 (@list @t1 @t198 @t535))) % 60.23/60.43 (step @p1167 :rule instantiate :premises (@p147) :args ((@list @t202 tptp.nil @t201))) % 60.23/60.43 (step @p1168 :rule cnf_or_pos :args (@t538)) % 60.23/60.43 (step @p1169 :rule reordering :premises (@p1168) :args ((or @t211 @t241 @t219 @t213 @t537 (not @t538)))) % 60.23/60.43 (step @p1170 :rule chain_m_resolution :premises (@p1169 @p8 @p251 @p212 @p208 @p1167) :args (@t537 @t493 (@list @t1 @t236 @t217 @t213 @t538))) % 60.23/60.43 (step @p1171 :rule instantiate :premises (@p727) :args ((@list @t202))) % 60.23/60.43 (step @p1172 :rule cnf_or_pos :args (@t540)) % 60.23/60.43 (step @p1173 :rule reordering :premises (@p1172) :args ((or @t241 @t539 (not @t540)))) % 60.23/60.43 (step @p1174 :rule chain_m_resolution :premises (@p1173 @p251 @p1171) :args (@t539 @t267 (@list @t236 @t540))) % 60.23/60.43 (step @p1175 :rule eq-symm :args (@t94 @t2)) % 60.23/60.43 (step @p1176 :rule nary_cong :premises (@p220 @p1175 @p312) :args (@t95)) % 60.23/60.43 (step @p1177 :rule cong :premises (@p1176) :args (@t96)) % 60.23/60.43 (step @p1178 :rule eq_resolve :premises (@p102 @p1177)) % 60.23/60.43 (step @p1179 :rule instantiate :premises (@p1178) :args ((@list @t203))) % 60.23/60.43 (step @p1180 :rule cnf_or_pos :args (@t544)) % 60.23/60.43 (step @p1181 :rule reordering :premises (@p1180) :args ((or @t246 @t460 @t543 (not @t544)))) % 60.23/60.43 (step @p1182 :rule chain_m_resolution :premises (@p1181 @p254 @p864 @p1179) :args (@t543 @t223 (@list @t239 @t460 @t544))) % 60.23/60.43 (assume-push @p1638 @t265) % 60.23/60.43 (assume-push @p1639 @t397) % 60.23/60.43 (assume-push @p1640 @t393) % 60.23/60.43 (assume-push @p1641 @t525) % 60.23/60.43 (assume-push @p1642 @t528) % 60.23/60.43 (assume-push @p1643 @t319) % 60.23/60.43 (assume-push @p1644 @t284) % 60.23/60.43 (assume-push @p1645 @t531) % 60.23/60.43 (assume-push @p1646 @t534) % 60.23/60.43 (assume-push @p1647 @t462) % 60.23/60.43 (assume-push @p1648 @t470) % 60.23/60.43 (assume-push @p1649 @t457) % 60.23/60.43 (assume-push @p1650 @t297) % 60.23/60.43 (assume-push @p1651 @t291) % 60.23/60.43 (assume-push @p1652 @t477) % 60.23/60.43 (assume-push @p1653 @t539) % 60.23/60.43 (assume-push @p1654 @t315) % 60.23/60.43 (assume-push @p1655 @t304) % 60.23/60.43 (assume-push @p1656 @t307) % 60.23/60.43 (assume-push @p1657 @t543) % 60.23/60.43 (assume-push @p1658 @t539) % 60.23/60.43 (assume-push @p1659 @t397) % 60.23/60.43 (assume-push @p1660 @t528) % 60.23/60.43 (assume-push @p1661 @t534) % 60.23/60.43 (assume-push @p1662 @t477) % 60.23/60.43 (assume-push @p1663 @t457) % 60.23/60.43 (assume-push @p1664 @t393) % 60.23/60.43 (assume-push @p1665 @t284) % 60.23/60.43 (assume-push @p1666 @t297) % 60.23/60.43 (assume-push @p1667 @t307) % 60.23/60.43 (assume-push @p1668 @t265) % 60.23/60.43 (assume-push @p1669 @t304) % 60.23/60.43 (assume-push @p1670 @t319) % 60.23/60.43 (assume-push @p1671 @t315) % 60.23/60.43 (assume-push @p1672 @t291) % 60.23/60.43 (assume-push @p1673 @t470) % 60.23/60.43 (assume-push @p1674 @t462) % 60.23/60.43 (assume-push @p1675 @t525) % 60.23/60.43 (assume-push @p1676 @t543) % 60.23/60.43 (assume-push @p1677 @t531) % 60.23/60.43 (step @p1223 :rule symm :premises (@p1166)) % 60.23/60.43 (step @p1224 :rule symm :premises (@p1174)) % 60.23/60.43 (step @p1225 :rule refl :args (@t202)) % 60.23/60.43 (step @p1226 :rule symm :premises (@p1639)) % 60.23/60.43 (step @p1227 :rule symm :premises (@p1158)) % 60.23/60.43 (step @p1228 :rule trans :premises (@p1227 @p1226)) % 60.23/60.43 (step @p1229 :rule cong :premises (@p1228 @p1225) :args ((tptp.app @t527 @t202))) % 60.23/60.43 (step @p1230 :rule cong :premises (@p1158 @p1225) :args (@t203)) % 60.23/60.43 (step @p1231 :rule trans :premises (@p1230 @p1229 @p1224)) % 60.23/60.43 (step @p1232 :rule cong :premises (@p1231 @p1223) :args ((tptp.app @t203 @t533))) % 60.23/60.43 (step @p509 :rule refl :args (@t203)) % 60.23/60.43 (step @p1233 :rule cong :premises (@p509 @p1166) :args (@t204)) % 60.23/60.43 (step @p1234 :rule symm :premises (@p883)) % 60.23/60.43 (step @p1235 :rule symm :premises (@p1640)) % 60.23/60.43 (step @p1078 :rule symm :premises (@p843)) % 60.23/60.43 (step @p1236 :rule cong :premises (@p1078 @p1235) :args (@t518)) % 60.23/60.43 (step @p1077 :rule refl :args (tptp.sk8)) % 60.23/60.43 (step @p1237 :rule cong :premises (@p843 @p1077) :args (@t205)) % 60.23/60.43 (step @p416 :rule symm :premises (@p341)) % 60.23/60.43 (step @p1238 :rule symm :premises (@p359)) % 60.23/60.43 (step @p1239 :rule symm :premises (@p367)) % 60.23/60.43 (step @p408 :rule symm :premises (@p311)) % 60.23/60.43 (step @p1240 :rule trans :premises (@p408 @p341)) % 60.23/60.43 (step @p1241 :rule cong :premises (@p1240) :args (@t320)) % 60.23/60.43 (step @p411 :rule cong :premises (@p311) :args (@t321)) % 60.23/60.43 (step @p1242 :rule trans :premises (@p411 @p1241 @p1239)) % 60.23/60.43 (step @p420 :rule refl :args (tptp.nil)) % 60.23/60.43 (step @p1243 :rule symm :premises (@p375)) % 60.23/60.43 (step @p1244 :rule cong :premises (@p1240) :args (@t323)) % 60.23/60.43 (step @p1245 :rule cong :premises (@p311) :args (@t286)) % 60.23/60.43 (step @p1246 :rule trans :premises (@p1245 @p1244 @p1243)) % 60.23/60.43 (step @p1247 :rule cong :premises (@p1246 @p420) :args (@t289)) % 60.23/60.43 (step @p1248 :rule cong :premises (@p1247 @p1242) :args (@t322)) % 60.23/60.43 (step @p415 :rule symm :premises (@p411)) % 60.23/60.43 (step @p1249 :rule symm :premises (@p1643)) % 60.23/60.43 (step @p1250 :rule trans :premises (@p1249 @p311)) % 60.23/60.43 (step @p1251 :rule cong :premises (@p1250) :args (@t314)) % 60.23/60.43 (step @p1252 :rule trans :premises (@p384 @p1251 @p415)) % 60.23/60.43 (step @p413 :rule refl :args (@t289)) % 60.23/60.43 (step @p1253 :rule cong :premises (@p413 @p1252) :args (@t290)) % 60.23/60.43 (step @p1254 :rule symm :premises (@p1154)) % 60.23/60.43 (step @p1255 :rule cong :premises (@p1231) :args (@t541)) % 60.23/60.43 (step @p1256 :rule trans :premises (@p1255 @p1254)) % 60.23/60.43 (step @p1257 :rule symm :premises (@p871)) % 60.23/60.43 (step @p1258 :rule trans :premises (@p867 @p1257)) % 60.23/60.43 (step @p1259 :rule cong :premises (@p1258 @p1256) :args (@t542)) % 60.23/60.43 (step @p1260 :rule symm :premises (@p1230)) % 60.23/60.43 (step @p1261 :rule symm :premises (@p1229)) % 60.23/60.43 (step @p1262 :rule symm :premises (@p1162)) % 60.23/60.43 (step @p1263 :rule trans :premises (@p1262 @p1174 @p1261 @p1260 @p1182 @p1259 @p353 @p1253 @p1248 @p1238 @p416 @p1237 @p1236 @p1234 @p1233 @p1232)) % 60.23/60.43 (step-pop @p1678 :rule scope :premises (@p1263)) % 60.23/60.43 (step-pop @p1679 :rule scope :premises (@p1678)) % 60.23/60.43 (step-pop @p1680 :rule scope :premises (@p1679)) % 60.23/60.43 (step-pop @p1681 :rule scope :premises (@p1680)) % 60.23/60.43 (step-pop @p1682 :rule scope :premises (@p1681)) % 60.23/60.43 (step-pop @p1683 :rule scope :premises (@p1682)) % 60.23/60.43 (step-pop @p1684 :rule scope :premises (@p1683)) % 60.23/60.43 (step-pop @p1685 :rule scope :premises (@p1684)) % 60.23/60.43 (step-pop @p1686 :rule scope :premises (@p1685)) % 60.23/60.43 (step-pop @p1687 :rule scope :premises (@p1686)) % 60.23/60.43 (step-pop @p1688 :rule scope :premises (@p1687)) % 60.23/60.43 (step-pop @p1689 :rule scope :premises (@p1688)) % 60.23/60.43 (step-pop @p1690 :rule scope :premises (@p1689)) % 60.23/60.43 (step-pop @p1691 :rule scope :premises (@p1690)) % 60.23/60.43 (step-pop @p1692 :rule scope :premises (@p1691)) % 60.23/60.43 (step-pop @p1693 :rule scope :premises (@p1692)) % 60.23/60.43 (step-pop @p1694 :rule scope :premises (@p1693)) % 60.23/60.43 (step-pop @p1695 :rule scope :premises (@p1694)) % 60.23/60.43 (step-pop @p1696 :rule scope :premises (@p1695)) % 60.23/60.43 (step-pop @p1697 :rule scope :premises (@p1696)) % 60.23/60.43 (step @p1264 :rule process_scope :premises (@p1697) :args (@t536)) % 60.23/60.43 (step @p1285 :rule and_intro :premises (@p1174 @p1639 @p1158 @p1166 @p883 @p843 @p1640 @p341 @p359 @p375 @p311 @p367 @p1643 @p384 @p353 @p871 @p867 @p1154 @p1182 @p1162)) % 60.23/60.43 (step @p1286 :rule modus_ponens :premises (@p1285 @p1264)) % 60.23/60.43 (step-pop @p1698 :rule scope :premises (@p1286)) % 60.23/60.43 (step-pop @p1699 :rule scope :premises (@p1698)) % 60.23/60.43 (step-pop @p1700 :rule scope :premises (@p1699)) % 60.23/60.43 (step-pop @p1701 :rule scope :premises (@p1700)) % 60.23/60.43 (step-pop @p1702 :rule scope :premises (@p1701)) % 60.23/60.43 (step-pop @p1703 :rule scope :premises (@p1702)) % 60.23/60.43 (step-pop @p1704 :rule scope :premises (@p1703)) % 60.23/60.43 (step-pop @p1705 :rule scope :premises (@p1704)) % 60.23/60.43 (step-pop @p1706 :rule scope :premises (@p1705)) % 60.23/60.43 (step-pop @p1707 :rule scope :premises (@p1706)) % 60.23/60.43 (step-pop @p1708 :rule scope :premises (@p1707)) % 60.23/60.43 (step-pop @p1709 :rule scope :premises (@p1708)) % 60.23/60.43 (step-pop @p1710 :rule scope :premises (@p1709)) % 60.23/60.43 (step-pop @p1711 :rule scope :premises (@p1710)) % 60.23/60.43 (step-pop @p1712 :rule scope :premises (@p1711)) % 60.23/60.43 (step-pop @p1713 :rule scope :premises (@p1712)) % 60.23/60.43 (step-pop @p1714 :rule scope :premises (@p1713)) % 60.23/60.43 (step-pop @p1715 :rule scope :premises (@p1714)) % 60.23/60.43 (step-pop @p1716 :rule scope :premises (@p1715)) % 60.23/60.43 (step-pop @p1717 :rule scope :premises (@p1716)) % 60.23/60.43 (step @p1287 :rule process_scope :premises (@p1717) :args (@t536)) % 60.23/60.43 (step @p1308 :rule implies_elim :premises (@p1287)) % 60.23/60.43 (step @p1309 :rule cnf_and_neg :args (@t545)) % 60.23/60.43 (step @p1310 :rule resolution :premises (@p1309 @p1308) :args (true @t545)) % 60.23/60.43 (step @p1311 :rule reordering :premises (@p1310) :args ((or @t334 (not @t397) @t453 (not @t525) (not @t528) @t333 @t331 (not @t531) (not @t534) @t516 @t515 @t514 @t536 @t330 @t329 @t512 (not @t539) @t328 @t327 @t326 (not @t543)))) % 60.23/60.43 (step @p1312 :rule chain_m_resolution :premises (@p1311 @p1182 @p384 @p1174 @p883 @p375 @p367 @p359 @p353 @p1170 @p341 @p871 @p867 @p843 @p1166 @p1162 @p1158 @p1154 @p311 @p1150 @p700 @p698 @p193 @p697) :args (@t333 (@list false false false false false false false false true false false false false false false false false false false false false false true) (@list @t543 @t315 @t539 @t477 @t307 @t304 @t297 @t291 @t536 @t284 @t470 @t462 @t457 @t534 @t531 @t528 @t525 @t265 @t397 @t393 @t394 @t200 @t260))) % 60.23/60.43 (step @p1313 :rule cnf_or_pos :args (@t548)) % 60.23/60.43 (step @p1314 :rule reordering :premises (@p1313) :args ((or @t245 @t547 @t319 (not @t548)))) % 60.23/60.43 (step @p1315 :rule chain_m_resolution :premises (@p1314 @p257 @p1312 @p281) :args (@t547 @t223 (@list @t244 @t319 @t548))) % 60.23/60.43 (step @p1316 :rule refl :args (@t207)) % 60.23/60.43 (step @p1317 :rule cong :premises (@p263) :args (@t208)) % 60.23/60.43 (step @p1318 :rule nary_cong :premises (@p1317 @p1316) :args (@t209)) % 60.23/60.43 (step @p1319 :rule eq_resolve :premises (@p196 @p1318)) % 60.23/60.43 (step @p1320 :rule reordering :premises (@p1319) :args ((or @t207 @t546))) % 60.23/60.43 (step @p1321 :rule chain_m_resolution :premises (@p1320 @p1315) :args (@t207 (@list true) (@list @t546))) % 60.23/60.43 (step @p1322 :rule cnf_or_pos :args (@t550)) % 60.23/60.43 (step @p1323 :rule reordering :premises (@p1322) :args ((or @t206 @t211 @t251 @t549 (not @t550)))) % 60.23/60.43 (step @p1324 :rule chain_m_resolution :premises (@p1323 @p1321 @p8 @p186 @p275) :args (@t549 (@list true false false false) (@list @t206 @t1 @t195 @t550))) % 60.23/60.43 (step @p1325 :rule refl :args (@t551)) % 60.23/60.43 (step @p1326 :rule bool-double-not-elim :args (@t220)) % 60.23/60.43 (step @p1327 :rule refl :args (@t552)) % 60.23/60.43 (step @p1328 :rule nary_cong :premises (@p1327 @p1326 @p1325) :args ((or @t552 (not @t221) @t551))) % 60.23/60.43 (assume-push @p1718 @t221) % 60.23/60.43 (assume-push @p1719 @t549) % 60.23/60.43 (assume-push @p1720 @t250) % 60.23/60.43 (step @p1332 :rule evaluate :args ((= true false))) % 60.23/60.43 (step @p1333 :rule false_intro :premises (@p215)) % 60.23/60.43 (step @p1334 :rule refl :args (@t201)) % 60.23/60.43 (step @p1335 :rule symm :premises (@p1719)) % 60.23/60.43 (step @p1336 :rule cong :premises (@p1335 @p1334) :args (@t250)) % 60.23/60.43 (step @p1337 :rule true_intro :premises (@p269)) % 60.23/60.43 (step @p1338 :rule symm :premises (@p1337)) % 60.23/60.43 (step @p1339 :rule trans :premises (@p1338 @p1336 @p1333)) % 60.23/60.43 (step @p1340 false :rule eq_resolve :premises (@p1339 @p1332)) % 60.23/60.43 (step-pop @p1721 :rule scope :premises (@p1340)) % 60.23/60.43 (step-pop @p1722 :rule scope :premises (@p1721)) % 60.23/60.43 (step-pop @p1723 :rule scope :premises (@p1722)) % 60.23/60.43 (step @p1341 :rule process_scope :premises (@p1723) :args (false)) % 60.23/60.43 (assume-push @p1724 @t549) % 60.23/60.43 (assume-push @p1725 @t221) % 60.23/60.43 (assume-push @p1726 @t250) % 60.23/60.43 (step @p1348 :rule and_intro :premises (@p215 @p1724 @p269)) % 60.23/60.43 (step-pop @p1727 :rule scope :premises (@p1348)) % 60.23/60.43 (step-pop @p1728 :rule scope :premises (@p1727)) % 60.23/60.43 (step-pop @p1729 :rule scope :premises (@p1728)) % 60.23/60.43 (step @p1349 :rule process_scope :premises (@p1729) :args (@t553)) % 60.23/60.43 (step @p1353 :rule implies_elim :premises (@p1349)) % 60.23/60.43 (step @p1354 :rule resolution :premises (@p1353 @p1341) :args (true @t553)) % 60.23/60.43 (step @p1355 :rule not_and :premises (@p1354)) % 60.23/60.43 (step @p1356 :rule eq_resolve :premises (@p1355 @p1328)) % 60.23/60.43 (step @p1357 false :rule chain_m_resolution :premises (@p1356 @p1324 @p269 @p215) :args (false (@list false false true) (@list @t549 @t250 @t220))) % 60.23/60.43 ) % 60.23/60.43 % SZS output end Proof % 60.23/60.43 % cvc5 exiting %------------------------------------------------------------------------------