%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : LCL954_19 : TPTP v9.3.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n027.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:24:15 AM UTC 2026 % Result : Theorem 1.44s 1.77s % Output : Proof 1.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL954_19 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.05 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.37 % Computer : n027.cluster.edu % 0.10/0.37 % Model : x86_64 x86_64 % 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.37 % Memory : 8046.5625MB % 0.10/0.37 % OS : Linux 6.8.0-71-generic % 0.10/0.37 % CPULimit : 300 % 0.10/0.37 % WCLimit : 300 % 0.10/0.37 % DateTime : Sat Sep 5 14:53:58 UTC 2026 % 0.10/0.37 % CPUTime : % 0.32/0.56 %----Proving TF0_NAR, FOF, or CNF % 1.44/1.77 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 1.44/1.77 % SZS status Theorem % 1.44/1.77 % SZS output start Proof % 1.44/1.77 ( % 1.44/1.77 (declare-sort |tptp.'$ki_world'| 0) % 1.44/1.77 (declare-sort $$unsorted 0) % 1.44/1.77 (declare-const tptp.def $$unsorted) % 1.44/1.77 (declare-const tptp.use $$unsorted) % 1.44/1.77 (declare-const tptp.true (-> |tptp.'$ki_world'| Bool)) % 1.44/1.77 (declare-const tptp.n5 $$unsorted) % 1.44/1.77 (declare-const tptp.n4 $$unsorted) % 1.44/1.77 (declare-const tptp.n3 $$unsorted) % 1.44/1.77 (declare-const tptp.n2 $$unsorted) % 1.44/1.77 (declare-const tptp.n1 $$unsorted) % 1.44/1.77 (declare-const tptp.sum (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 1.44/1.77 (declare-const tptp.minus (-> $$unsorted $$unsorted $$unsorted)) % 1.44/1.77 (declare-const tptp.dim (-> $$unsorted $$unsorted $$unsorted)) % 1.44/1.77 (declare-const tptp.a_select3 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 1.44/1.77 (declare-const tptp.tptp_minus_1 $$unsorted) % 1.44/1.77 (declare-const |tptp.'$ki_local_world'| |tptp.'$ki_world'|) % 1.44/1.77 (declare-const tptp.plus (-> $$unsorted $$unsorted $$unsorted)) % 1.44/1.77 (declare-const tptp.a_select2 (-> $$unsorted $$unsorted $$unsorted)) % 1.44/1.77 (declare-const tptp.n0 $$unsorted) % 1.44/1.77 (declare-const tptp.succ (-> $$unsorted $$unsorted)) % 1.44/1.77 (declare-const tptp.customqmltpeq (-> |tptp.'$ki_world'| $$unsorted $$unsorted Bool)) % 1.44/1.77 (declare-const tptp.tptp_update3 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 1.44/1.77 (declare-const tptp.pred (-> $$unsorted $$unsorted)) % 1.44/1.77 (declare-const |tptp.'$ki_exists_in_world_$i'| (-> |tptp.'$ki_world'| $$unsorted Bool)) % 1.44/1.77 (declare-const tptp.inv (-> $$unsorted $$unsorted)) % 1.44/1.77 (declare-const |tptp.'$ki_accessible'| (-> |tptp.'$ki_world'| |tptp.'$ki_world'| Bool)) % 1.44/1.77 (declare-const tptp.tptp_const_array1 (-> $$unsorted $$unsorted $$unsorted)) % 1.44/1.77 (declare-const tptp.tptp_const_array2 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 1.44/1.77 (declare-const tptp.tptp_float_0_0 $$unsorted) % 1.44/1.77 (declare-const tptp.tptp_madd (-> $$unsorted $$unsorted $$unsorted)) % 1.44/1.77 (declare-const tptp.tptp_mmul (-> $$unsorted $$unsorted $$unsorted)) % 1.44/1.77 (declare-const tptp.tptp_msub (-> $$unsorted $$unsorted $$unsorted)) % 1.44/1.77 (declare-const tptp.tptp_update2 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 1.44/1.77 (declare-const tptp.trans (-> $$unsorted $$unsorted)) % 1.44/1.77 (declare-const tptp.uniform_int_rnd (-> $$unsorted $$unsorted $$unsorted)) % 1.44/1.77 (declare-const tptp.geq (-> |tptp.'$ki_world'| $$unsorted $$unsorted Bool)) % 1.44/1.77 (declare-const tptp.gt (-> |tptp.'$ki_world'| $$unsorted $$unsorted Bool)) % 1.44/1.77 (declare-const tptp.leq (-> |tptp.'$ki_world'| $$unsorted $$unsorted Bool)) % 1.44/1.77 (declare-const tptp.lt (-> |tptp.'$ki_world'| $$unsorted $$unsorted Bool)) % 1.44/1.77 (define @t1 () (@var "W" |tptp.'$ki_world'|)) % 1.44/1.77 (define @t2 () (@list @t1)) % 1.44/1.77 (define @t3 () (@var "U" |tptp.'$ki_world'|)) % 1.44/1.77 (define @t4 () (@var "V" |tptp.'$ki_world'|)) % 1.44/1.77 (define @t5 () (@var "X" $$unsorted)) % 1.44/1.77 (define @t6 () (|tptp.'$ki_exists_in_world_$i'| @t1 @t5)) % 1.44/1.77 (define @t7 () (@list @t5)) % 1.44/1.77 (define @t8 () (@var "W0" |tptp.'$ki_world'|)) % 1.44/1.77 (define @t9 () (|tptp.'$ki_accessible'| @t1 @t8)) % 1.44/1.77 (define @t10 () (@list @t8)) % 1.44/1.77 (define @t11 () (|tptp.'$ki_accessible'| |tptp.'$ki_local_world'| @t1)) % 1.44/1.77 (define @t12 () (@var "Y" $$unsorted)) % 1.44/1.77 (define @t13 () (@var "W2" |tptp.'$ki_world'|)) % 1.44/1.77 (define @t14 () (@var "W1" |tptp.'$ki_world'|)) % 1.44/1.77 (define @t15 () (|tptp.'$ki_accessible'| @t14 @t13)) % 1.44/1.77 (define @t16 () (@list @t13)) % 1.44/1.77 (define @t17 () (|tptp.'$ki_accessible'| @t8 @t14)) % 1.44/1.77 (define @t18 () (@list @t14)) % 1.44/1.77 (define @t19 () (|tptp.'$ki_exists_in_world_$i'| @t8 @t12)) % 1.44/1.77 (define @t20 () (@list @t12)) % 1.44/1.77 (define @t21 () (@var "Z" $$unsorted)) % 1.44/1.77 (define @t22 () (@var "W3" |tptp.'$ki_world'|)) % 1.44/1.77 (define @t23 () (|tptp.'$ki_accessible'| @t13 @t22)) % 1.44/1.77 (define @t24 () (@list @t22)) % 1.44/1.77 (define @t25 () (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 @t5 @t12)))) % 1.44/1.77 (define @t26 () (|tptp.'$ki_exists_in_world_$i'| @t14 @t21)) % 1.44/1.77 (define @t27 () (@list @t21)) % 1.44/1.77 (define @t28 () (@var "C" $$unsorted)) % 1.44/1.77 (define @t29 () (@var "B" $$unsorted)) % 1.44/1.77 (define @t30 () (@var "A" $$unsorted)) % 1.44/1.77 (define @t31 () (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 @t30 @t29)))) % 1.44/1.77 (define @t32 () (|tptp.'$ki_exists_in_world_$i'| @t14 @t28)) % 1.44/1.77 (define @t33 () (@list @t28)) % 1.44/1.77 (define @t34 () (|tptp.'$ki_exists_in_world_$i'| @t8 @t29)) % 1.44/1.77 (define @t35 () (@list @t29)) % 1.44/1.77 (define @t36 () (|tptp.'$ki_exists_in_world_$i'| @t1 @t30)) % 1.44/1.77 (define @t37 () (@list @t30)) % 1.44/1.77 (define @t38 () (@var "D" $$unsorted)) % 1.44/1.77 (define @t39 () (@var "W4" |tptp.'$ki_world'|)) % 1.44/1.77 (define @t40 () (|tptp.'$ki_accessible'| @t22 @t39)) % 1.44/1.77 (define @t41 () (@list @t39)) % 1.44/1.77 (define @t42 () (forall @t41 (=> @t40 (tptp.customqmltpeq @t39 @t30 @t29)))) % 1.44/1.77 (define @t43 () (|tptp.'$ki_exists_in_world_$i'| @t13 @t38)) % 1.44/1.77 (define @t44 () (@list @t38)) % 1.44/1.77 (define @t45 () (tptp.inv @t30)) % 1.44/1.77 (define @t46 () (forall @t16 (=> @t15 (tptp.customqmltpeq @t13 @t30 @t29)))) % 1.44/1.77 (define @t47 () (@var "E" $$unsorted)) % 1.44/1.77 (define @t48 () (@var "W5" |tptp.'$ki_world'|)) % 1.44/1.77 (define @t49 () (|tptp.'$ki_accessible'| @t39 @t48)) % 1.44/1.77 (define @t50 () (@list @t48)) % 1.44/1.77 (define @t51 () (forall @t50 (=> @t49 (tptp.customqmltpeq @t48 @t30 @t29)))) % 1.44/1.77 (define @t52 () (|tptp.'$ki_exists_in_world_$i'| @t22 @t47)) % 1.44/1.77 (define @t53 () (@list @t47)) % 1.44/1.77 (define @t54 () (tptp.trans @t29)) % 1.44/1.77 (define @t55 () (tptp.trans @t30)) % 1.44/1.77 (define @t56 () (forall @t16 (=> @t15 (tptp.lt @t13 @t5 @t12)))) % 1.44/1.77 (define @t57 () (forall @t16 (=> @t15 (tptp.gt @t13 @t12 @t5)))) % 1.44/1.77 (define @t58 () (forall @t16 (=> @t15 (tptp.geq @t13 @t5 @t12)))) % 1.44/1.77 (define @t59 () (forall @t16 (=> @t15 (tptp.leq @t13 @t12 @t5)))) % 1.44/1.77 (define @t60 () (forall @t16 (=> @t15 (tptp.leq @t13 @t5 @t12)))) % 1.44/1.77 (define @t61 () (forall @t16 (=> @t15 (tptp.leq @t13 @t5 (tptp.pred @t12))))) % 1.44/1.77 (define @t62 () (tptp.succ @t5)) % 1.44/1.77 (define @t63 () (tptp.succ @t12)) % 1.44/1.77 (define @t64 () (forall @t16 (=> @t15 (tptp.gt @t13 @t63 @t5)))) % 1.44/1.77 (define @t65 () (tptp.uniform_int_rnd @t28 @t5)) % 1.44/1.77 (define @t66 () (forall @t16 (=> @t15 (tptp.leq @t13 tptp.n0 @t5)))) % 1.44/1.77 (define @t67 () (|tptp.'$ki_exists_in_world_$i'| @t8 @t28)) % 1.44/1.77 (define @t68 () (@var "Val" $$unsorted)) % 1.44/1.77 (define @t69 () (@var "I" $$unsorted)) % 1.44/1.77 (define @t70 () (@var "U" $$unsorted)) % 1.44/1.77 (define @t71 () (@var "L" $$unsorted)) % 1.44/1.77 (define @t72 () (forall @t41 (=> @t40 (tptp.leq @t39 @t69 @t70)))) % 1.44/1.77 (define @t73 () (@list @t68)) % 1.44/1.77 (define @t74 () (|tptp.'$ki_exists_in_world_$i'| @t14 @t70)) % 1.44/1.77 (define @t75 () (@list @t70)) % 1.44/1.77 (define @t76 () (|tptp.'$ki_exists_in_world_$i'| @t1 @t69)) % 1.44/1.77 (define @t77 () (@list @t69)) % 1.44/1.77 (define @t78 () (@var "J" $$unsorted)) % 1.44/1.77 (define @t79 () (@var "U2" $$unsorted)) % 1.44/1.77 (define @t80 () (@var "L2" $$unsorted)) % 1.44/1.77 (define @t81 () (@var "U1" $$unsorted)) % 1.44/1.77 (define @t82 () (@var "L1" $$unsorted)) % 1.44/1.77 (define @t83 () (@var "W7" |tptp.'$ki_world'|)) % 1.44/1.77 (define @t84 () (@var "W6" |tptp.'$ki_world'|)) % 1.44/1.77 (define @t85 () (|tptp.'$ki_accessible'| @t84 @t83)) % 1.44/1.77 (define @t86 () (@list @t83)) % 1.44/1.77 (define @t87 () (|tptp.'$ki_accessible'| @t48 @t84)) % 1.44/1.77 (define @t88 () (@list @t84)) % 1.44/1.77 (define @t89 () (@list @t78)) % 1.44/1.77 (define @t90 () (@var "N" $$unsorted)) % 1.44/1.77 (define @t91 () (and (forall @t50 (=> @t49 (tptp.leq @t48 tptp.n0 @t69))) (forall @t50 (=> @t49 (tptp.leq @t48 @t69 @t90))) (forall @t50 (=> @t49 (tptp.leq @t48 tptp.n0 @t78))) (forall @t50 (=> @t49 (tptp.leq @t48 @t78 @t90))))) % 1.44/1.77 (define @t92 () (|tptp.'$ki_exists_in_world_$i'| @t22 @t78)) % 1.44/1.77 (define @t93 () (|tptp.'$ki_exists_in_world_$i'| @t13 @t69)) % 1.44/1.77 (define @t94 () (tptp.a_select3 @t30 @t78 @t69)) % 1.44/1.77 (define @t95 () (tptp.a_select3 @t30 @t69 @t78)) % 1.44/1.77 (define @t96 () (forall @t16 (=> @t15 (forall @t77 (=> @t93 (forall @t24 (=> @t23 (forall @t89 (=> @t92 (forall @t41 (=> @t40 (=> @t91 (forall @t50 (=> @t49 (tptp.customqmltpeq @t48 @t95 @t94))))))))))))))) % 1.44/1.77 (define @t97 () (|tptp.'$ki_exists_in_world_$i'| @t8 @t90)) % 1.44/1.77 (define @t98 () (@list @t90)) % 1.44/1.77 (define @t99 () (@var "VAL" $$unsorted)) % 1.44/1.77 (define @t100 () (@var "K" $$unsorted)) % 1.44/1.77 (define @t101 () (tptp.tptp_update3 @t30 @t100 @t100 @t99)) % 1.44/1.77 (define @t102 () (forall @t86 (=> @t85 (tptp.leq @t83 @t78 @t90)))) % 1.44/1.77 (define @t103 () (forall @t86 (=> @t85 (tptp.leq @t83 tptp.n0 @t78)))) % 1.44/1.77 (define @t104 () (forall @t86 (=> @t85 (tptp.leq @t83 @t69 @t90)))) % 1.44/1.77 (define @t105 () (forall @t86 (=> @t85 (tptp.leq @t83 tptp.n0 @t69)))) % 1.44/1.77 (define @t106 () (@list @t99)) % 1.44/1.77 (define @t107 () (tptp.tptp_madd @t30 @t29)) % 1.44/1.77 (define @t108 () (forall @t88 (=> @t87 (tptp.leq @t84 tptp.n0 @t78)))) % 1.44/1.77 (define @t109 () (forall @t88 (=> @t87 (tptp.leq @t84 tptp.n0 @t69)))) % 1.44/1.77 (define @t110 () (and @t109 (forall @t88 (=> @t87 (tptp.leq @t84 @t69 @t90))) @t108 (forall @t88 (=> @t87 (tptp.leq @t84 @t78 @t90))))) % 1.44/1.77 (define @t111 () (|tptp.'$ki_exists_in_world_$i'| @t39 @t78)) % 1.44/1.77 (define @t112 () (|tptp.'$ki_exists_in_world_$i'| @t22 @t69)) % 1.44/1.77 (define @t113 () (tptp.a_select3 @t29 @t78 @t69)) % 1.44/1.77 (define @t114 () (tptp.a_select3 @t29 @t69 @t78)) % 1.44/1.77 (define @t115 () (forall @t24 (=> @t23 (forall @t77 (=> @t112 (forall @t41 (=> @t40 (forall @t89 (=> @t111 (forall @t50 (=> @t49 (=> @t110 (forall @t88 (=> @t87 (tptp.customqmltpeq @t84 @t114 @t113))))))))))))))) % 1.44/1.77 (define @t116 () (and (forall @t24 (=> @t23 (forall @t77 (=> @t112 (forall @t41 (=> @t40 (forall @t89 (=> @t111 (forall @t50 (=> @t49 (=> @t110 (forall @t88 (=> @t87 (tptp.customqmltpeq @t84 @t95 @t94)))))))))))))) @t115)) % 1.44/1.77 (define @t117 () (|tptp.'$ki_exists_in_world_$i'| @t14 @t90)) % 1.44/1.77 (define @t118 () (tptp.tptp_msub @t30 @t29)) % 1.44/1.77 (define @t119 () (tptp.tptp_mmul @t30 (tptp.tptp_mmul @t29 @t55))) % 1.44/1.77 (define @t120 () (tptp.a_select3 @t119 @t78 @t69)) % 1.44/1.77 (define @t121 () (tptp.a_select3 @t119 @t69 @t78)) % 1.44/1.77 (define @t122 () (|tptp.'$ki_exists_in_world_$i'| @t48 @t78)) % 1.44/1.77 (define @t123 () (|tptp.'$ki_exists_in_world_$i'| @t39 @t69)) % 1.44/1.77 (define @t124 () (@var "M" $$unsorted)) % 1.44/1.77 (define @t125 () (@list @t124)) % 1.44/1.77 (define @t126 () (@var "F" $$unsorted)) % 1.44/1.77 (define @t127 () (tptp.tptp_madd @t30 (tptp.tptp_mmul @t29 (tptp.tptp_mmul (tptp.tptp_madd (tptp.tptp_mmul @t28 (tptp.tptp_mmul @t38 (tptp.trans @t28))) (tptp.tptp_mmul @t47 (tptp.tptp_mmul @t126 (tptp.trans @t47)))) @t54)))) % 1.44/1.77 (define @t128 () (@var "W11" |tptp.'$ki_world'|)) % 1.44/1.77 (define @t129 () (@var "W10" |tptp.'$ki_world'|)) % 1.44/1.77 (define @t130 () (|tptp.'$ki_accessible'| @t129 @t128)) % 1.44/1.77 (define @t131 () (@list @t128)) % 1.44/1.77 (define @t132 () (forall @t131 (=> @t130 (tptp.leq @t128 tptp.n0 @t78)))) % 1.44/1.77 (define @t133 () (forall @t131 (=> @t130 (tptp.leq @t128 tptp.n0 @t69)))) % 1.44/1.77 (define @t134 () (and @t133 (forall @t131 (=> @t130 (tptp.leq @t128 @t69 @t90))) @t132 (forall @t131 (=> @t130 (tptp.leq @t128 @t78 @t90))))) % 1.44/1.77 (define @t135 () (@var "W9" |tptp.'$ki_world'|)) % 1.44/1.77 (define @t136 () (|tptp.'$ki_accessible'| @t135 @t129)) % 1.44/1.77 (define @t137 () (@list @t129)) % 1.44/1.77 (define @t138 () (|tptp.'$ki_exists_in_world_$i'| @t135 @t78)) % 1.44/1.77 (define @t139 () (@var "W8" |tptp.'$ki_world'|)) % 1.44/1.77 (define @t140 () (|tptp.'$ki_accessible'| @t139 @t135)) % 1.44/1.77 (define @t141 () (@list @t135)) % 1.44/1.77 (define @t142 () (|tptp.'$ki_exists_in_world_$i'| @t139 @t69)) % 1.44/1.77 (define @t143 () (|tptp.'$ki_accessible'| @t83 @t139)) % 1.44/1.77 (define @t144 () (@list @t139)) % 1.44/1.77 (define @t145 () (@var "Body" $$unsorted)) % 1.44/1.77 (define @t146 () (tptp.sum tptp.n0 tptp.tptp_minus_1 @t145)) % 1.44/1.77 (define @t147 () (|tptp.'$ki_exists_in_world_$i'| @t1 @t145)) % 1.44/1.77 (define @t148 () (@list @t145)) % 1.44/1.77 (define @t149 () (tptp.succ @t62)) % 1.44/1.77 (define @t150 () (tptp.succ @t149)) % 1.44/1.77 (define @t151 () (tptp.succ @t150)) % 1.44/1.77 (define @t152 () (tptp.succ @t151)) % 1.44/1.77 (define @t153 () (tptp.pred @t5)) % 1.44/1.77 (define @t154 () (forall @t16 (=> @t15 (tptp.leq @t13 @t62 @t63)))) % 1.44/1.77 (define @t155 () (@var "V" $$unsorted)) % 1.44/1.77 (define @t156 () (tptp.tptp_update3 @t5 @t70 @t155 @t99)) % 1.44/1.77 (define @t157 () (|tptp.'$ki_exists_in_world_$i'| @t13 @t99)) % 1.44/1.77 (define @t158 () (@list @t155)) % 1.44/1.77 (define @t159 () (|tptp.'$ki_exists_in_world_$i'| @t8 @t70)) % 1.44/1.77 (define @t160 () (@var "VAL2" $$unsorted)) % 1.44/1.77 (define @t161 () (@list @t160)) % 1.44/1.77 (define @t162 () (|tptp.'$ki_exists_in_world_$i'| @t39 @t99)) % 1.44/1.77 (define @t163 () (|tptp.'$ki_exists_in_world_$i'| @t22 @t5)) % 1.44/1.77 (define @t164 () (|tptp.'$ki_exists_in_world_$i'| @t13 @t155)) % 1.44/1.77 (define @t165 () (|tptp.'$ki_exists_in_world_$i'| @t8 @t78)) % 1.44/1.77 (define @t166 () (@var "J0" $$unsorted)) % 1.44/1.77 (define @t167 () (@var "I0" $$unsorted)) % 1.44/1.77 (define @t168 () (@list @t167)) % 1.44/1.77 (define @t169 () (tptp.tptp_update2 @t5 @t70 @t99)) % 1.44/1.77 (define @t170 () (|tptp.'$ki_exists_in_world_$i'| @t14 @t5)) % 1.44/1.77 (define @t171 () (forall @t18 (=> @t17 (tptp.customqmltpeq @t14 @t5 tptp.n4)))) % 1.44/1.77 (define @t172 () (forall @t18 (=> @t17 (tptp.customqmltpeq @t14 @t5 tptp.n3)))) % 1.44/1.77 (define @t173 () (forall @t18 (=> @t17 (tptp.customqmltpeq @t14 @t5 tptp.n2)))) % 1.44/1.77 (define @t174 () (forall @t18 (=> @t17 (tptp.customqmltpeq @t14 @t5 tptp.n1)))) % 1.44/1.77 (define @t175 () (forall @t18 (=> @t17 (tptp.customqmltpeq @t14 @t5 tptp.n0)))) % 1.44/1.77 (define @t176 () (forall @t18 (=> @t17 (tptp.leq @t14 tptp.n0 @t5)))) % 1.44/1.77 (define @t177 () (tptp.succ tptp.n0)) % 1.44/1.77 (define @t178 () (tptp.succ @t177)) % 1.44/1.77 (define @t179 () (tptp.succ @t178)) % 1.44/1.77 (define @t180 () (tptp.succ @t179)) % 1.44/1.77 (define @t181 () (tptp.true @t8)) % 1.44/1.77 (define @t182 () (forall @t10 (=> @t9 @t181))) % 1.44/1.77 (define @t183 () (=> @t182 @t182)) % 1.44/1.77 (define @t184 () (=> @t11 @t183)) % 1.44/1.77 (define @t185 () (forall @t2 @t184)) % 1.44/1.77 (define @t186 () (not @t185)) % 1.44/1.77 (define @t187 () (not @t11)) % 1.44/1.77 (define @t188 () (or @t187 true)) % 1.44/1.77 (define @t189 () (forall @t10 (or (not @t9) @t181))) % 1.44/1.77 (define @t190 () (=> @t189 @t189)) % 1.44/1.77 (assume @p1 (forall @t2 (|tptp.'$ki_accessible'| @t1 @t1))) % 1.44/1.77 (assume @p2 (forall (@list @t1 @t4 @t3) (=> (and (|tptp.'$ki_accessible'| @t1 @t4) (|tptp.'$ki_accessible'| @t4 @t3)) (|tptp.'$ki_accessible'| @t1 @t3)))) % 1.44/1.77 (assume @p3 (forall @t2 (exists @t7 @t6))) % 1.44/1.77 (assume @p4 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 @t5 @t5)))))))) % 1.44/1.77 (assume @p5 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t20 (=> @t19 (forall @t18 (=> @t17 (=> (forall @t16 (=> @t15 (tptp.customqmltpeq @t13 @t5 @t12))) (forall @t16 (=> @t15 (tptp.customqmltpeq @t13 @t12 @t5))))))))))))))) % 1.44/1.77 (assume @p6 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t20 (=> @t19 (forall @t18 (=> @t17 (forall @t27 (=> @t26 (forall @t16 (=> @t15 (=> (and @t25 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 @t12 @t21)))) (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 @t5 @t21))))))))))))))))))) % 1.44/1.77 (assume @p7 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.a_select2 @t30 @t28) (tptp.a_select2 @t29 @t28)))))))))))))))))))) % 1.44/1.77 (assume @p8 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.a_select2 @t28 @t30) (tptp.a_select2 @t28 @t29)))))))))))))))))))) % 1.44/1.77 (assume @p9 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (=> @t42 (forall @t41 (=> @t40 (tptp.customqmltpeq @t39 (tptp.a_select3 @t30 @t28 @t38) (tptp.a_select3 @t29 @t28 @t38)))))))))))))))))))))))) % 1.44/1.77 (assume @p10 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (=> @t42 (forall @t41 (=> @t40 (tptp.customqmltpeq @t39 (tptp.a_select3 @t28 @t30 @t38) (tptp.a_select3 @t28 @t29 @t38)))))))))))))))))))))))) % 1.44/1.77 (assume @p11 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (=> @t42 (forall @t41 (=> @t40 (tptp.customqmltpeq @t39 (tptp.a_select3 @t28 @t38 @t30) (tptp.a_select3 @t28 @t38 @t29)))))))))))))))))))))))) % 1.44/1.77 (assume @p12 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.dim @t30 @t28) (tptp.dim @t29 @t28)))))))))))))))))))) % 1.44/1.77 (assume @p13 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.dim @t28 @t30) (tptp.dim @t28 @t29)))))))))))))))))))) % 1.44/1.77 (assume @p14 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (=> @t46 (forall @t16 (=> @t15 (tptp.customqmltpeq @t13 @t45 (tptp.inv @t29)))))))))))))))) % 1.44/1.77 (assume @p15 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.minus @t30 @t28) (tptp.minus @t29 @t28)))))))))))))))))))) % 1.44/1.77 (assume @p16 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.minus @t28 @t30) (tptp.minus @t28 @t29)))))))))))))))))))) % 1.44/1.77 (assume @p17 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.plus @t30 @t28) (tptp.plus @t29 @t28)))))))))))))))))))) % 1.44/1.77 (assume @p18 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.plus @t28 @t30) (tptp.plus @t28 @t29)))))))))))))))))))) % 1.44/1.77 (assume @p19 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (=> @t46 (forall @t16 (=> @t15 (tptp.customqmltpeq @t13 (tptp.pred @t30) (tptp.pred @t29)))))))))))))))) % 1.44/1.77 (assume @p20 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (=> @t46 (forall @t16 (=> @t15 (tptp.customqmltpeq @t13 (tptp.succ @t30) (tptp.succ @t29)))))))))))))))) % 1.44/1.77 (assume @p21 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (=> @t42 (forall @t41 (=> @t40 (tptp.customqmltpeq @t39 (tptp.sum @t30 @t28 @t38) (tptp.sum @t29 @t28 @t38)))))))))))))))))))))))) % 1.44/1.77 (assume @p22 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (=> @t42 (forall @t41 (=> @t40 (tptp.customqmltpeq @t39 (tptp.sum @t28 @t30 @t38) (tptp.sum @t28 @t29 @t38)))))))))))))))))))))))) % 1.44/1.77 (assume @p23 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (=> @t42 (forall @t41 (=> @t40 (tptp.customqmltpeq @t39 (tptp.sum @t28 @t38 @t30) (tptp.sum @t28 @t38 @t29)))))))))))))))))))))))) % 1.44/1.77 (assume @p24 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.tptp_const_array1 @t30 @t28) (tptp.tptp_const_array1 @t29 @t28)))))))))))))))))))) % 1.44/1.77 (assume @p25 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.tptp_const_array1 @t28 @t30) (tptp.tptp_const_array1 @t28 @t29)))))))))))))))))))) % 1.44/1.77 (assume @p26 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (=> @t42 (forall @t41 (=> @t40 (tptp.customqmltpeq @t39 (tptp.tptp_const_array2 @t30 @t28 @t38) (tptp.tptp_const_array2 @t29 @t28 @t38)))))))))))))))))))))))) % 1.44/1.77 (assume @p27 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (=> @t42 (forall @t41 (=> @t40 (tptp.customqmltpeq @t39 (tptp.tptp_const_array2 @t28 @t30 @t38) (tptp.tptp_const_array2 @t28 @t29 @t38)))))))))))))))))))))))) % 1.44/1.77 (assume @p28 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (=> @t42 (forall @t41 (=> @t40 (tptp.customqmltpeq @t39 (tptp.tptp_const_array2 @t28 @t38 @t30) (tptp.tptp_const_array2 @t28 @t38 @t29)))))))))))))))))))))))) % 1.44/1.77 (assume @p29 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.tptp_madd @t30 @t28) (tptp.tptp_madd @t29 @t28)))))))))))))))))))) % 1.44/1.77 (assume @p30 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.tptp_madd @t28 @t30) (tptp.tptp_madd @t28 @t29)))))))))))))))))))) % 1.44/1.77 (assume @p31 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.tptp_mmul @t30 @t28) (tptp.tptp_mmul @t29 @t28)))))))))))))))))))) % 1.44/1.77 (assume @p32 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.tptp_mmul @t28 @t30) (tptp.tptp_mmul @t28 @t29)))))))))))))))))))) % 1.44/1.77 (assume @p33 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.tptp_msub @t30 @t28) (tptp.tptp_msub @t29 @t28)))))))))))))))))))) % 1.44/1.77 (assume @p34 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.tptp_msub @t28 @t30) (tptp.tptp_msub @t28 @t29)))))))))))))))))))) % 1.44/1.77 (assume @p35 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (=> @t42 (forall @t41 (=> @t40 (tptp.customqmltpeq @t39 (tptp.tptp_update2 @t30 @t28 @t38) (tptp.tptp_update2 @t29 @t28 @t38)))))))))))))))))))))))) % 1.44/1.77 (assume @p36 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (=> @t42 (forall @t41 (=> @t40 (tptp.customqmltpeq @t39 (tptp.tptp_update2 @t28 @t30 @t38) (tptp.tptp_update2 @t28 @t29 @t38)))))))))))))))))))))))) % 1.44/1.77 (assume @p37 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (=> @t42 (forall @t41 (=> @t40 (tptp.customqmltpeq @t39 (tptp.tptp_update2 @t28 @t38 @t30) (tptp.tptp_update2 @t28 @t38 @t29)))))))))))))))))))))))) % 1.44/1.77 (assume @p38 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (forall @t53 (=> @t52 (forall @t41 (=> @t40 (=> @t51 (forall @t50 (=> @t49 (tptp.customqmltpeq @t48 (tptp.tptp_update3 @t30 @t28 @t38 @t47) (tptp.tptp_update3 @t29 @t28 @t38 @t47)))))))))))))))))))))))))))) % 1.44/1.77 (assume @p39 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (forall @t53 (=> @t52 (forall @t41 (=> @t40 (=> @t51 (forall @t50 (=> @t49 (tptp.customqmltpeq @t48 (tptp.tptp_update3 @t28 @t30 @t38 @t47) (tptp.tptp_update3 @t28 @t29 @t38 @t47)))))))))))))))))))))))))))) % 1.44/1.77 (assume @p40 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (forall @t53 (=> @t52 (forall @t41 (=> @t40 (=> @t51 (forall @t50 (=> @t49 (tptp.customqmltpeq @t48 (tptp.tptp_update3 @t28 @t38 @t30 @t47) (tptp.tptp_update3 @t28 @t38 @t29 @t47)))))))))))))))))))))))))))) % 1.44/1.77 (assume @p41 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (forall @t53 (=> @t52 (forall @t41 (=> @t40 (=> @t51 (forall @t50 (=> @t49 (tptp.customqmltpeq @t48 (tptp.tptp_update3 @t28 @t38 @t47 @t30) (tptp.tptp_update3 @t28 @t38 @t47 @t29)))))))))))))))))))))))))))) % 1.44/1.77 (assume @p42 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (=> @t46 (forall @t16 (=> @t15 (tptp.customqmltpeq @t13 @t55 @t54))))))))))))))) % 1.44/1.77 (assume @p43 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.uniform_int_rnd @t30 @t28) (tptp.uniform_int_rnd @t29 @t28)))))))))))))))))))) % 1.44/1.77 (assume @p44 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> @t31 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.uniform_int_rnd @t28 @t30) (tptp.uniform_int_rnd @t28 @t29)))))))))))))))))))) % 1.44/1.77 (assume @p45 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> (and @t31 (forall @t24 (=> @t23 (tptp.geq @t22 @t30 @t28)))) (forall @t24 (=> @t23 (tptp.geq @t22 @t29 @t28))))))))))))))))))) % 1.44/1.77 (assume @p46 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> (and @t31 (forall @t24 (=> @t23 (tptp.geq @t22 @t28 @t30)))) (forall @t24 (=> @t23 (tptp.geq @t22 @t28 @t29))))))))))))))))))) % 1.44/1.77 (assume @p47 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> (and @t31 (forall @t24 (=> @t23 (tptp.gt @t22 @t30 @t28)))) (forall @t24 (=> @t23 (tptp.gt @t22 @t29 @t28))))))))))))))))))) % 1.44/1.77 (assume @p48 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> (and @t31 (forall @t24 (=> @t23 (tptp.gt @t22 @t28 @t30)))) (forall @t24 (=> @t23 (tptp.gt @t22 @t28 @t29))))))))))))))))))) % 1.44/1.77 (assume @p49 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> (and @t31 (forall @t24 (=> @t23 (tptp.leq @t22 @t30 @t28)))) (forall @t24 (=> @t23 (tptp.leq @t22 @t29 @t28))))))))))))))))))) % 1.44/1.77 (assume @p50 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> (and @t31 (forall @t24 (=> @t23 (tptp.leq @t22 @t28 @t30)))) (forall @t24 (=> @t23 (tptp.leq @t22 @t28 @t29))))))))))))))))))) % 1.44/1.77 (assume @p51 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> (and @t31 (forall @t24 (=> @t23 (tptp.lt @t22 @t30 @t28)))) (forall @t24 (=> @t23 (tptp.lt @t22 @t29 @t28))))))))))))))))))) % 1.44/1.77 (assume @p52 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (=> (and @t31 (forall @t24 (=> @t23 (tptp.lt @t22 @t28 @t30)))) (forall @t24 (=> @t23 (tptp.lt @t22 @t28 @t29))))))))))))))))))) % 1.44/1.77 (assume @p53 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t20 (=> @t19 (or (forall @t18 (=> @t17 (tptp.gt @t14 @t5 @t12))) (forall @t18 (=> @t17 (tptp.gt @t14 @t12 @t5))) (forall @t18 (=> @t17 (tptp.customqmltpeq @t14 @t5 @t12))))))))))))) % 1.44/1.77 (assume @p54 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t20 (=> @t19 (forall @t18 (=> @t17 (forall @t27 (=> @t26 (forall @t16 (=> @t15 (=> (and (forall @t24 (=> @t23 (tptp.gt @t22 @t5 @t12))) (forall @t24 (=> @t23 (tptp.gt @t22 @t12 @t21)))) (forall @t24 (=> @t23 (tptp.gt @t22 @t5 @t21))))))))))))))))))) % 1.44/1.77 (assume @p55 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (not (forall @t18 (=> @t17 (tptp.gt @t14 @t5 @t5))))))))))) % 1.44/1.77 (assume @p56 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (tptp.leq @t8 @t5 @t5)))))))) % 1.44/1.77 (assume @p57 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t20 (=> @t19 (forall @t18 (=> @t17 (forall @t27 (=> @t26 (forall @t16 (=> @t15 (=> (and (forall @t24 (=> @t23 (tptp.leq @t22 @t5 @t12))) (forall @t24 (=> @t23 (tptp.leq @t22 @t12 @t21)))) (forall @t24 (=> @t23 (tptp.leq @t22 @t5 @t21))))))))))))))))))) % 1.44/1.77 (assume @p58 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t20 (=> @t19 (and (forall @t18 (=> @t17 (=> @t56 @t57))) (forall @t18 (=> @t17 (=> @t57 @t56))))))))))))) % 1.44/1.77 (assume @p59 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t20 (=> @t19 (and (forall @t18 (=> @t17 (=> @t58 @t59))) (forall @t18 (=> @t17 (=> @t59 @t58))))))))))))) % 1.44/1.77 (assume @p60 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t20 (=> @t19 (forall @t18 (=> @t17 (=> @t57 @t60)))))))))))) % 1.44/1.77 (assume @p61 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t20 (=> @t19 (forall @t18 (=> @t17 (=> (and @t60 (forall @t16 (=> @t15 (not @t25)))) @t57)))))))))))) % 1.44/1.77 (assume @p62 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t20 (=> @t19 (and (forall @t18 (=> @t17 (=> @t61 @t57))) (forall @t18 (=> @t17 (=> @t57 @t61))))))))))))) % 1.44/1.77 (assume @p63 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (tptp.gt @t8 @t62 @t5)))))))) % 1.44/1.77 (assume @p64 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t20 (=> @t19 (forall @t18 (=> @t17 (=> @t60 (forall @t16 (=> @t15 (tptp.leq @t13 @t5 @t63))))))))))))))) % 1.44/1.77 (assume @p65 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t20 (=> @t19 (and (forall @t18 (=> @t17 (=> @t60 @t64))) (forall @t18 (=> @t17 (=> @t64 @t60))))))))))))) % 1.44/1.77 (assume @p66 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t33 (=> @t67 (forall @t18 (=> @t17 (=> @t66 (forall @t16 (=> @t15 (tptp.leq @t13 @t65 @t5))))))))))))))) % 1.44/1.77 (assume @p67 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t33 (=> @t67 (forall @t18 (=> @t17 (=> @t66 (forall @t16 (=> @t15 (tptp.leq @t13 tptp.n0 @t65))))))))))))))) % 1.44/1.77 (assume @p68 (forall @t2 (=> @t11 (forall @t77 (=> @t76 (forall @t10 (=> @t9 (forall (@list @t71) (=> (|tptp.'$ki_exists_in_world_$i'| @t8 @t71) (forall @t18 (=> @t17 (forall @t75 (=> @t74 (forall @t16 (=> @t15 (forall @t73 (=> (|tptp.'$ki_exists_in_world_$i'| @t13 @t68) (forall @t24 (=> @t23 (=> (and (forall @t41 (=> @t40 (tptp.leq @t39 @t71 @t69))) @t72) (forall @t41 (=> @t40 (tptp.customqmltpeq @t39 (tptp.a_select2 (tptp.tptp_const_array1 (tptp.dim @t71 @t70) @t68) @t69) @t68))))))))))))))))))))))) % 1.44/1.77 (assume @p69 (forall @t2 (=> @t11 (forall @t77 (=> @t76 (forall @t10 (=> @t9 (forall (@list @t82) (=> (|tptp.'$ki_exists_in_world_$i'| @t8 @t82) (forall @t18 (=> @t17 (forall (@list @t81) (=> (|tptp.'$ki_exists_in_world_$i'| @t14 @t81) (forall @t16 (=> @t15 (forall @t89 (=> (|tptp.'$ki_exists_in_world_$i'| @t13 @t78) (forall @t24 (=> @t23 (forall (@list @t80) (=> (|tptp.'$ki_exists_in_world_$i'| @t22 @t80) (forall @t41 (=> @t40 (forall (@list @t79) (=> (|tptp.'$ki_exists_in_world_$i'| @t39 @t79) (forall @t50 (=> @t49 (forall @t73 (=> (|tptp.'$ki_exists_in_world_$i'| @t48 @t68) (forall @t88 (=> @t87 (=> (and (forall @t86 (=> @t85 (tptp.leq @t83 @t82 @t69))) (forall @t86 (=> @t85 (tptp.leq @t83 @t69 @t81))) (forall @t86 (=> @t85 (tptp.leq @t83 @t80 @t78))) (forall @t86 (=> @t85 (tptp.leq @t83 @t78 @t79)))) (forall @t86 (=> @t85 (tptp.customqmltpeq @t83 (tptp.a_select3 (tptp.tptp_const_array2 (tptp.dim @t82 @t81) (tptp.dim @t80 @t79) @t68) @t69 @t78) @t68))))))))))))))))))))))))))))))))))) % 1.44/1.77 (assume @p70 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t98 (=> @t97 (forall @t18 (=> @t17 (=> @t96 (forall @t16 (=> @t15 (forall @t77 (=> @t93 (forall @t24 (=> @t23 (forall @t89 (=> @t92 (forall @t41 (=> @t40 (=> @t91 (forall @t50 (=> @t49 (tptp.customqmltpeq @t48 (tptp.a_select3 @t55 @t69 @t78) (tptp.a_select3 @t55 @t78 @t69))))))))))))))))))))))))))) % 1.44/1.77 (assume @p71 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t98 (=> @t97 (forall @t18 (=> @t17 (=> @t96 (forall @t16 (=> @t15 (forall @t77 (=> @t93 (forall @t24 (=> @t23 (forall @t89 (=> @t92 (forall @t41 (=> @t40 (=> @t91 (forall @t50 (=> @t49 (tptp.customqmltpeq @t48 (tptp.a_select3 @t45 @t69 @t78) (tptp.a_select3 @t45 @t78 @t69))))))))))))))))))))))))))) % 1.44/1.77 (assume @p72 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t98 (=> @t97 (forall @t18 (=> @t17 (=> @t96 (forall @t16 (=> @t15 (forall @t77 (=> @t93 (forall @t24 (=> @t23 (forall @t89 (=> @t92 (forall @t41 (=> @t40 (forall (@list @t100) (=> (|tptp.'$ki_exists_in_world_$i'| @t39 @t100) (forall @t50 (=> @t49 (forall @t106 (=> (|tptp.'$ki_exists_in_world_$i'| @t48 @t99) (forall @t88 (=> @t87 (=> (and @t105 @t104 @t103 @t102 (forall @t86 (=> @t85 (tptp.leq @t83 tptp.n0 @t100))) (forall @t86 (=> @t85 (tptp.leq @t83 @t100 @t90)))) (forall @t86 (=> @t85 (tptp.customqmltpeq @t83 (tptp.a_select3 @t101 @t69 @t78) (tptp.a_select3 @t101 @t78 @t69))))))))))))))))))))))))))))))))))) % 1.44/1.77 (assume @p73 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t98 (=> @t117 (forall @t16 (=> @t15 (=> @t116 (forall @t24 (=> @t23 (forall @t77 (=> @t112 (forall @t41 (=> @t40 (forall @t89 (=> @t111 (forall @t50 (=> @t49 (=> @t110 (forall @t88 (=> @t87 (tptp.customqmltpeq @t84 (tptp.a_select3 @t107 @t69 @t78) (tptp.a_select3 @t107 @t78 @t69))))))))))))))))))))))))))))))) % 1.44/1.77 (assume @p74 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t98 (=> @t117 (forall @t16 (=> @t15 (=> @t116 (forall @t24 (=> @t23 (forall @t77 (=> @t112 (forall @t41 (=> @t40 (forall @t89 (=> @t111 (forall @t50 (=> @t49 (=> @t110 (forall @t88 (=> @t87 (tptp.customqmltpeq @t84 (tptp.a_select3 @t118 @t69 @t78) (tptp.a_select3 @t118 @t78 @t69))))))))))))))))))))))))))))))) % 1.44/1.77 (assume @p75 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t98 (=> @t117 (forall @t16 (=> @t15 (=> @t115 (forall @t24 (=> @t23 (forall @t77 (=> @t112 (forall @t41 (=> @t40 (forall @t89 (=> @t111 (forall @t50 (=> @t49 (=> @t110 (forall @t88 (=> @t87 (tptp.customqmltpeq @t84 @t121 @t120)))))))))))))))))))))))))))))) % 1.44/1.77 (assume @p76 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t98 (=> @t117 (forall @t16 (=> @t15 (forall @t125 (=> (|tptp.'$ki_exists_in_world_$i'| @t13 @t124) (forall @t24 (=> @t23 (=> (forall @t41 (=> @t40 (forall @t77 (=> @t123 (forall @t50 (=> @t49 (forall @t89 (=> @t122 (forall @t88 (=> @t87 (=> (and @t105 (forall @t86 (=> @t85 (tptp.leq @t83 @t69 @t124))) @t103 (forall @t86 (=> @t85 (tptp.leq @t83 @t78 @t124)))) (forall @t86 (=> @t85 (tptp.customqmltpeq @t83 @t114 @t113)))))))))))))) (forall @t41 (=> @t40 (forall @t77 (=> @t123 (forall @t50 (=> @t49 (forall @t89 (=> @t122 (forall @t88 (=> @t87 (=> (and @t105 @t104 @t103 @t102) (forall @t86 (=> @t85 (tptp.customqmltpeq @t83 @t121 @t120)))))))))))))))))))))))))))))))))) % 1.44/1.77 (assume @p77 (forall @t2 (=> @t11 (forall @t37 (=> @t36 (forall @t10 (=> @t9 (forall @t35 (=> @t34 (forall @t18 (=> @t17 (forall @t33 (=> @t32 (forall @t16 (=> @t15 (forall @t44 (=> @t43 (forall @t24 (=> @t23 (forall @t53 (=> @t52 (forall @t41 (=> @t40 (forall (@list @t126) (=> (|tptp.'$ki_exists_in_world_$i'| @t39 @t126) (forall @t50 (=> @t49 (forall @t98 (=> (|tptp.'$ki_exists_in_world_$i'| @t48 @t90) (forall @t88 (=> @t87 (forall @t125 (=> (|tptp.'$ki_exists_in_world_$i'| @t84 @t124) (forall @t86 (=> @t85 (=> (and (forall @t144 (=> @t143 (forall @t77 (=> @t142 (forall @t141 (=> @t140 (forall @t89 (=> @t138 (forall @t137 (=> @t136 (=> (and @t133 (forall @t131 (=> @t130 (tptp.leq @t128 @t69 @t124))) @t132 (forall @t131 (=> @t130 (tptp.leq @t128 @t78 @t124)))) (forall @t131 (=> @t130 (tptp.customqmltpeq @t128 (tptp.a_select3 @t38 @t69 @t78) (tptp.a_select3 @t38 @t78 @t69))))))))))))))) (forall @t144 (=> @t143 (forall @t77 (=> @t142 (forall @t141 (=> @t140 (forall @t89 (=> @t138 (forall @t137 (=> @t136 (=> @t134 (forall @t131 (=> @t130 (tptp.customqmltpeq @t128 @t95 @t94)))))))))))))) (forall @t144 (=> @t143 (forall @t77 (=> @t142 (forall @t141 (=> @t140 (forall @t89 (=> @t138 (forall @t137 (=> @t136 (=> @t134 (forall @t131 (=> @t130 (tptp.customqmltpeq @t128 (tptp.a_select3 @t126 @t69 @t78) (tptp.a_select3 @t126 @t78 @t69)))))))))))))))) (forall @t144 (=> @t143 (forall @t77 (=> @t142 (forall @t141 (=> @t140 (forall @t89 (=> @t138 (forall @t137 (=> @t136 (=> @t134 (forall @t131 (=> @t130 (tptp.customqmltpeq @t128 (tptp.a_select3 @t127 @t69 @t78) (tptp.a_select3 @t127 @t78 @t69))))))))))))))))))))))))))))))))))))))))))))))))))) % 1.44/1.77 (assume @p78 (forall @t2 (=> @t11 (forall @t148 (=> @t147 (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 @t146 tptp.n0)))))))) % 1.44/1.77 (assume @p79 (forall @t2 (=> @t11 (forall @t148 (=> @t147 (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 tptp.tptp_float_0_0 @t146)))))))) % 1.44/1.77 (assume @p80 (forall @t2 (=> @t11 (tptp.customqmltpeq @t1 (tptp.succ tptp.tptp_minus_1) tptp.n0)))) % 1.44/1.77 (assume @p81 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 (tptp.plus @t5 tptp.n1) @t62)))))))) % 1.44/1.77 (assume @p82 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 (tptp.plus tptp.n1 @t5) @t62)))))))) % 1.44/1.77 (assume @p83 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 (tptp.plus @t5 tptp.n2) @t149)))))))) % 1.44/1.77 (assume @p84 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 (tptp.plus tptp.n2 @t5) @t149)))))))) % 1.44/1.77 (assume @p85 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 (tptp.plus @t5 tptp.n3) @t150)))))))) % 1.44/1.77 (assume @p86 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 (tptp.plus tptp.n3 @t5) @t150)))))))) % 1.44/1.77 (assume @p87 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 (tptp.plus @t5 tptp.n4) @t151)))))))) % 1.44/1.77 (assume @p88 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 (tptp.plus tptp.n4 @t5) @t151)))))))) % 1.44/1.77 (assume @p89 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 (tptp.plus @t5 tptp.n5) @t152)))))))) % 1.44/1.77 (assume @p90 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 (tptp.plus tptp.n5 @t5) @t152)))))))) % 1.44/1.77 (assume @p91 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 (tptp.minus @t5 tptp.n1) @t153)))))))) % 1.44/1.77 (assume @p92 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 (tptp.pred @t62) @t5)))))))) % 1.44/1.77 (assume @p93 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 (tptp.succ @t153) @t5)))))))) % 1.44/1.78 (assume @p94 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t20 (=> @t19 (and (forall @t18 (=> @t17 (=> @t154 @t60))) (forall @t18 (=> @t17 (=> @t60 @t154))))))))))))) % 1.44/1.78 (assume @p95 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t20 (=> @t19 (forall @t18 (=> @t17 (=> (forall @t16 (=> @t15 (tptp.leq @t13 @t62 @t12))) @t57)))))))))))) % 1.44/1.78 (assume @p96 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t20 (=> @t19 (forall @t18 (=> @t17 (=> (forall @t16 (=> @t15 (tptp.leq @t13 (tptp.minus @t5 @t12) @t5))) (forall @t16 (=> @t15 (tptp.leq @t13 tptp.n0 @t12))))))))))))))) % 1.44/1.78 (assume @p97 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t75 (=> @t159 (forall @t18 (=> @t17 (forall @t158 (=> (|tptp.'$ki_exists_in_world_$i'| @t14 @t155) (forall @t16 (=> @t15 (forall @t106 (=> @t157 (forall @t24 (=> @t23 (tptp.customqmltpeq @t22 (tptp.a_select3 @t156 @t70 @t155) @t99)))))))))))))))))))) % 1.44/1.78 (assume @p98 (forall @t2 (=> @t11 (forall @t77 (=> @t76 (forall @t10 (=> @t9 (forall @t89 (=> @t165 (forall @t18 (=> @t17 (forall @t75 (=> @t74 (forall @t16 (=> @t15 (forall @t158 (=> @t164 (forall @t24 (=> @t23 (forall @t7 (=> @t163 (forall @t41 (=> @t40 (forall @t106 (=> @t162 (forall @t50 (=> @t49 (forall @t161 (=> (|tptp.'$ki_exists_in_world_$i'| @t48 @t160) (forall @t88 (=> @t87 (=> (and (forall @t86 (=> @t85 (not (forall @t144 (=> @t143 (tptp.customqmltpeq @t139 @t69 @t70)))))) (forall @t86 (=> @t85 (tptp.customqmltpeq @t83 @t78 @t155))) (forall @t86 (=> @t85 (tptp.customqmltpeq @t83 (tptp.a_select3 @t5 @t70 @t155) @t99)))) (forall @t86 (=> @t85 (tptp.customqmltpeq @t83 (tptp.a_select3 (tptp.tptp_update3 @t5 @t69 @t78 @t160) @t70 @t155) @t99))))))))))))))))))))))))))))))))))) % 1.44/1.78 (assume @p99 (forall @t2 (=> @t11 (forall @t77 (=> @t76 (forall @t10 (=> @t9 (forall @t89 (=> @t165 (forall @t18 (=> @t17 (forall @t75 (=> @t74 (forall @t16 (=> @t15 (forall @t158 (=> @t164 (forall @t24 (=> @t23 (forall @t7 (=> @t163 (forall @t41 (=> @t40 (forall @t106 (=> @t162 (forall @t50 (=> @t49 (=> (and (forall @t88 (=> @t87 (forall @t168 (=> (|tptp.'$ki_exists_in_world_$i'| @t84 @t167) (forall @t86 (=> @t85 (forall (@list @t166) (=> (|tptp.'$ki_exists_in_world_$i'| @t83 @t166) (forall @t144 (=> @t143 (=> (and (forall @t141 (=> @t140 (tptp.leq @t135 tptp.n0 @t167))) (forall @t141 (=> @t140 (tptp.leq @t135 tptp.n0 @t166))) (forall @t141 (=> @t140 (tptp.leq @t135 @t167 @t70))) (forall @t141 (=> @t140 (tptp.leq @t135 @t166 @t155)))) (forall @t141 (=> @t140 (tptp.customqmltpeq @t135 (tptp.a_select3 @t5 @t167 @t166) @t99)))))))))))))) @t109 (forall @t88 (=> @t87 (tptp.leq @t84 @t69 @t70))) @t108 (forall @t88 (=> @t87 (tptp.leq @t84 @t78 @t155)))) (forall @t88 (=> @t87 (tptp.customqmltpeq @t84 (tptp.a_select3 @t156 @t69 @t78) @t99))))))))))))))))))))))))))))))) % 1.44/1.78 (assume @p100 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (forall @t75 (=> @t159 (forall @t18 (=> @t17 (forall @t106 (=> (|tptp.'$ki_exists_in_world_$i'| @t14 @t99) (forall @t16 (=> @t15 (tptp.customqmltpeq @t13 (tptp.a_select2 @t169 @t70) @t99)))))))))))))))) % 1.44/1.78 (assume @p101 (forall @t2 (=> @t11 (forall @t77 (=> @t76 (forall @t10 (=> @t9 (forall @t75 (=> @t159 (forall @t18 (=> @t17 (forall @t7 (=> @t170 (forall @t16 (=> @t15 (forall @t106 (=> @t157 (forall @t24 (=> @t23 (forall @t161 (=> (|tptp.'$ki_exists_in_world_$i'| @t22 @t160) (forall @t41 (=> @t40 (=> (and (forall @t50 (=> @t49 (not (forall @t88 (=> @t87 (tptp.customqmltpeq @t84 @t69 @t70)))))) (forall @t50 (=> @t49 (tptp.customqmltpeq @t48 (tptp.a_select2 @t5 @t70) @t99)))) (forall @t50 (=> @t49 (tptp.customqmltpeq @t48 (tptp.a_select2 (tptp.tptp_update2 @t5 @t69 @t160) @t70) @t99))))))))))))))))))))))))))) % 1.44/1.78 (assume @p102 (forall @t2 (=> @t11 (forall @t77 (=> @t76 (forall @t10 (=> @t9 (forall @t75 (=> @t159 (forall @t18 (=> @t17 (forall @t7 (=> @t170 (forall @t16 (=> @t15 (forall @t106 (=> @t157 (forall @t24 (=> @t23 (=> (and (forall @t41 (=> @t40 (forall @t168 (=> (|tptp.'$ki_exists_in_world_$i'| @t39 @t167) (forall @t50 (=> @t49 (=> (and (forall @t88 (=> @t87 (tptp.leq @t84 tptp.n0 @t167))) (forall @t88 (=> @t87 (tptp.leq @t84 @t167 @t70)))) (forall @t88 (=> @t87 (tptp.customqmltpeq @t84 (tptp.a_select2 @t5 @t167) @t99)))))))))) (forall @t41 (=> @t40 (tptp.leq @t39 tptp.n0 @t69))) @t72) (forall @t41 (=> @t40 (tptp.customqmltpeq @t39 (tptp.a_select2 @t169 @t69) @t99))))))))))))))))))))))) % 1.44/1.78 (assume @p103 (forall @t2 (=> @t11 (tptp.true @t1)))) % 1.44/1.78 (assume @p104 (forall @t2 (=> @t11 (not (forall @t10 (=> @t9 (tptp.customqmltpeq @t8 tptp.def tptp.use))))))) % 1.44/1.78 (assume @p105 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n5 tptp.n4)))) % 1.44/1.78 (assume @p106 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n4 tptp.tptp_minus_1)))) % 1.44/1.78 (assume @p107 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n5 tptp.tptp_minus_1)))) % 1.44/1.78 (assume @p108 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n0 tptp.tptp_minus_1)))) % 1.44/1.78 (assume @p109 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n1 tptp.tptp_minus_1)))) % 1.44/1.78 (assume @p110 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n2 tptp.tptp_minus_1)))) % 1.44/1.78 (assume @p111 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n3 tptp.tptp_minus_1)))) % 1.44/1.78 (assume @p112 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n4 tptp.n0)))) % 1.44/1.78 (assume @p113 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n5 tptp.n0)))) % 1.44/1.78 (assume @p114 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n1 tptp.n0)))) % 1.44/1.78 (assume @p115 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n2 tptp.n0)))) % 1.44/1.78 (assume @p116 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n3 tptp.n0)))) % 1.44/1.78 (assume @p117 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n4 tptp.n1)))) % 1.44/1.78 (assume @p118 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n5 tptp.n1)))) % 1.44/1.78 (assume @p119 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n2 tptp.n1)))) % 1.44/1.78 (assume @p120 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n3 tptp.n1)))) % 1.44/1.78 (assume @p121 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n4 tptp.n2)))) % 1.44/1.78 (assume @p122 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n5 tptp.n2)))) % 1.44/1.78 (assume @p123 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n3 tptp.n2)))) % 1.44/1.78 (assume @p124 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n4 tptp.n3)))) % 1.44/1.78 (assume @p125 (forall @t2 (=> @t11 (tptp.gt @t1 tptp.n5 tptp.n3)))) % 1.44/1.78 (assume @p126 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (=> (and @t176 (forall @t18 (=> @t17 (tptp.leq @t14 @t5 tptp.n4)))) (or @t175 @t174 @t173 @t172 @t171))))))))) % 1.44/1.78 (assume @p127 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (=> (and @t176 (forall @t18 (=> @t17 (tptp.leq @t14 @t5 tptp.n5)))) (or @t175 @t174 @t173 @t172 @t171 (forall @t18 (=> @t17 (tptp.customqmltpeq @t14 @t5 tptp.n5)))))))))))) % 1.44/1.78 (assume @p128 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (=> (and @t176 (forall @t18 (=> @t17 (tptp.leq @t14 @t5 tptp.n0)))) @t175)))))))) % 1.44/1.78 (assume @p129 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (=> (and @t176 (forall @t18 (=> @t17 (tptp.leq @t14 @t5 tptp.n1)))) (or @t175 @t174))))))))) % 1.44/1.78 (assume @p130 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (=> (and @t176 (forall @t18 (=> @t17 (tptp.leq @t14 @t5 tptp.n2)))) (or @t175 @t174 @t173))))))))) % 1.44/1.78 (assume @p131 (forall @t2 (=> @t11 (forall @t7 (=> @t6 (forall @t10 (=> @t9 (=> (and @t176 (forall @t18 (=> @t17 (tptp.leq @t14 @t5 tptp.n3)))) (or @t175 @t174 @t173 @t172))))))))) % 1.44/1.78 (assume @p132 (forall @t2 (=> @t11 (tptp.customqmltpeq @t1 @t180 tptp.n4)))) % 1.44/1.78 (assume @p133 (forall @t2 (=> @t11 (tptp.customqmltpeq @t1 (tptp.succ @t180) tptp.n5)))) % 1.44/1.78 (assume @p134 (forall @t2 (=> @t11 (tptp.customqmltpeq @t1 @t177 tptp.n1)))) % 1.44/1.78 (assume @p135 (forall @t2 (=> @t11 (tptp.customqmltpeq @t1 @t178 tptp.n2)))) % 1.44/1.78 (assume @p136 (forall @t2 (=> @t11 (tptp.customqmltpeq @t1 @t179 tptp.n3)))) % 1.44/1.78 (assume @p137 @t186) % 1.44/1.78 (assume @p138 true) % 1.44/1.78 (step @p139 :rule evaluate :args ((not true))) % 1.44/1.78 (step @p140 :rule quant-unused-vars :args ((= (forall @t2 true) true))) % 1.44/1.78 (step @p141 :rule absorb :args ((= @t188 true))) % 1.44/1.78 (step @p142 :rule cong :premises (@p141) :args ((forall @t2 @t188))) % 1.44/1.78 (step @p143 :rule trans :premises (@p142 @p140)) % 1.44/1.78 (step @p144 :rule bool-or-taut2 :args (false @t189 false false)) % 1.44/1.78 (step @p145 :rule bool-impl-elim :args (@t189 @t189)) % 1.44/1.78 (step @p146 :rule trans :premises (@p145 @p144)) % 1.44/1.78 (step @p147 :rule refl :args (@t187)) % 1.44/1.78 (step @p148 :rule nary_cong :premises (@p147 @p146) :args ((or @t187 @t190))) % 1.44/1.78 (step @p149 :rule bool-impl-elim :args (@t11 @t190)) % 1.44/1.78 (step @p150 :rule trans :premises (@p149 @p148)) % 1.44/1.78 (step @p151 :rule cong :premises (@p150) :args ((forall @t2 (=> @t11 @t190)))) % 1.44/1.78 (step @p152 :rule trans :premises (@p151 @p143)) % 1.44/1.78 (step @p153 :rule bool-impl-elim :args (@t9 @t181)) % 1.44/1.78 (step @p154 :rule cong :premises (@p153) :args (@t182)) % 1.44/1.78 (step @p155 :rule cong :premises (@p154 @p154) :args (@t183)) % 1.44/1.78 (step @p156 :rule refl :args (@t11)) % 1.44/1.78 (step @p157 :rule cong :premises (@p156 @p155) :args (@t184)) % 1.44/1.78 (step @p158 :rule cong :premises (@p157) :args (@t185)) % 1.44/1.78 (step @p159 :rule trans :premises (@p158 @p152)) % 1.44/1.78 (step @p160 :rule cong :premises (@p159) :args (@t186)) % 1.44/1.78 (step @p161 :rule trans :premises (@p160 @p139)) % 1.44/1.78 (step @p162 false :rule eq_resolve :premises (@p137 @p161)) % 1.44/1.78 ) % 1.44/1.78 % SZS output end Proof % 1.44/1.78 % cvc5 exiting %------------------------------------------------------------------------------