%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : KRS161+1 : TPTP v9.2.1. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n018.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:29:02 AM UTC 2026 % Result : Theorem 0.37s 0.79s % Output : Proof 0.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : KRS161+1 : TPTP v9.2.1. Released v3.1.0. % 0.00/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.16/0.34 % Computer : n018.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 05:28:20 EDT 2026 % 0.16/0.34 % CPUTime : % 0.25/0.53 %----Proving TF0_NAR, FOF, or CNF % 0.37/0.79 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.37/0.79 % SZS status Theorem % 0.37/0.79 % SZS output start Proof % 0.37/0.79 ( % 0.37/0.79 (declare-sort $$unsorted 0) % 0.37/0.79 (declare-const tptp.iV16464 $$unsorted) % 0.37/0.79 (declare-const tptp.iV16455 $$unsorted) % 0.37/0.79 (declare-const tptp.iV16461 $$unsorted) % 0.37/0.79 (declare-const tptp.iV16463 $$unsorted) % 0.37/0.79 (declare-const tptp.iV16441 $$unsorted) % 0.37/0.79 (declare-const tptp.iV16442 $$unsorted) % 0.37/0.79 (declare-const tptp.iV16440 $$unsorted) % 0.37/0.79 (declare-const tptp.cTEST (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC98 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC96xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC94xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC94 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC92 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px50 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px32 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px31 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC82 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC80 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC78xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px28 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC78 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC76xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC2 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC86 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px2 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC84 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px1 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC88xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC24 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px58 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC16 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px34 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC4xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC22 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC40 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px9 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC14xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC130 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC18 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.iV16449 $$unsorted) % 0.37/0.79 (declare-const tptp.cC122 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.iV16459 $$unsorted) % 0.37/0.79 (declare-const tptp.ra_Px27 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.xsd_string (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px18 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.iV16462 $$unsorted) % 0.37/0.79 (declare-const tptp.ra_Px33 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC6 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC56 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.iV16439 $$unsorted) % 0.37/0.79 (declare-const tptp.ra_Px42 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC20 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC10 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC90 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC26 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC10xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px43 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC42 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px19 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC74 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC102xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cowlThing (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.rR1 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC120xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC8xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC128 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC88 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px17 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC8 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC72 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC12 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px4 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC44 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC126 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC86xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.xsd_integer (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC110 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC96 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC28 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC66 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC98xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC102 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC100xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC104 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC32xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px14 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px73 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC64xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC106 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC34 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px48 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px22 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.iV16457 $$unsorted) % 0.37/0.79 (declare-const tptp.ra_Px74 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC14 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC108 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC50 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC120 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cowlNothing (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC48 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC112 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px37 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px35 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC114 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC90xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC30 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px25 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px57 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC4 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC30xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px26 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px5 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.iV16465 $$unsorted) % 0.37/0.79 (declare-const tptp.cC92xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px36 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC32 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC60 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px6 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC34xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px15 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px7 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC12xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC36 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px23 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px41 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC36xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px24 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cTOP (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC70 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC116 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px8 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC118 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC38xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC70xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC118xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px3 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px10 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC40xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.iV16448 $$unsorted) % 0.37/0.79 (declare-const tptp.cC72xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC124 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px13 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px72 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC46 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.iV16453 $$unsorted) % 0.37/0.79 (declare-const tptp.cC74xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC46xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.iV16460 $$unsorted) % 0.37/0.79 (declare-const tptp.cC48xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC50xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC16xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px49 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC52 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC66xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC52xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC84xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px16 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC18xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC54 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC2xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC54xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC56xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC58 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC100 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC58xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC6xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC76 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC62 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC64 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC68 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC114xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC38 (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.cC68xcomp (-> $$unsorted Bool)) % 0.37/0.79 (declare-const tptp.ra_Px51 (-> $$unsorted $$unsorted Bool)) % 0.37/0.79 (define @t1 () (@var "X" $$unsorted)) % 0.37/0.79 (define @t2 () (not (tptp.cowlNothing @t1))) % 0.37/0.79 (define @t3 () (tptp.cowlThing @t1)) % 0.37/0.79 (define @t4 () (@list @t1)) % 0.37/0.79 (define @t5 () (forall @t4 (and @t3 @t2))) % 0.37/0.79 (define @t6 () (forall @t4 (= (tptp.xsd_string @t1) (not (tptp.xsd_integer @t1))))) % 0.37/0.79 (define @t7 () (tptp.cC6 @t1)) % 0.37/0.79 (define @t8 () (tptp.cC8 @t1)) % 0.37/0.79 (define @t9 () (tptp.cC10 @t1)) % 0.37/0.79 (define @t10 () (@var "Y" $$unsorted)) % 0.37/0.79 (define @t11 () (@list @t10)) % 0.37/0.79 (define @t12 () (@var "Y0" $$unsorted)) % 0.37/0.79 (define @t13 () (@list @t12)) % 0.37/0.79 (define @t14 () (tptp.rR1 @t1 @t10)) % 0.37/0.79 (define @t15 () (tptp.cC100 @t1)) % 0.37/0.79 (define @t16 () (tptp.cC100xcomp @t1)) % 0.37/0.79 (define @t17 () (tptp.cC102xcomp @t1)) % 0.37/0.79 (define @t18 () (tptp.cC102xcomp @t10)) % 0.37/0.79 (define @t19 () (and @t14 @t18)) % 0.37/0.79 (define @t20 () (exists @t11 @t19)) % 0.37/0.79 (define @t21 () (tptp.cC104 @t1)) % 0.37/0.79 (define @t22 () (= @t21 @t20)) % 0.37/0.79 (define @t23 () (forall @t4 @t22)) % 0.37/0.79 (define @t24 () (tptp.cC106 @t1)) % 0.37/0.79 (define @t25 () (tptp.cC28 @t1)) % 0.37/0.79 (define @t26 () (tptp.cC108 @t1)) % 0.37/0.79 (define @t27 () (tptp.cC12xcomp @t1)) % 0.37/0.79 (define @t28 () (tptp.cC4xcomp @t1)) % 0.37/0.79 (define @t29 () (tptp.cC110 @t1)) % 0.37/0.79 (define @t30 () (tptp.cC112 @t1)) % 0.37/0.79 (define @t31 () (tptp.cC114xcomp @t1)) % 0.37/0.79 (define @t32 () (tptp.cC116 @t1)) % 0.37/0.79 (define @t33 () (tptp.cC118xcomp @t1)) % 0.37/0.79 (define @t34 () (tptp.cC12 @t1)) % 0.37/0.79 (define @t35 () (tptp.cC120 @t1)) % 0.37/0.79 (define @t36 () (tptp.cC130 @t1)) % 0.37/0.79 (define @t37 () (tptp.cC14 @t1)) % 0.37/0.79 (define @t38 () (tptp.cC16 @t1)) % 0.37/0.79 (define @t39 () (tptp.cC18 @t1)) % 0.37/0.79 (define @t40 () (tptp.cC2 @t1)) % 0.37/0.79 (define @t41 () (tptp.cC2xcomp @t1)) % 0.37/0.79 (define @t42 () (tptp.cC30 @t1)) % 0.37/0.79 (define @t43 () (tptp.cC4 @t1)) % 0.37/0.79 (define @t44 () (and @t40 @t43)) % 0.37/0.79 (define @t45 () (tptp.cC30xcomp @t1)) % 0.37/0.79 (define @t46 () (tptp.cC32 @t1)) % 0.37/0.79 (define @t47 () (tptp.cC32xcomp @t1)) % 0.37/0.79 (define @t48 () (tptp.cC34 @t1)) % 0.37/0.79 (define @t49 () (tptp.cC36 @t1)) % 0.37/0.79 (define @t50 () (tptp.cC36xcomp @t1)) % 0.37/0.79 (define @t51 () (tptp.cC38 @t1)) % 0.37/0.79 (define @t52 () (tptp.cC40 @t1)) % 0.37/0.79 (define @t53 () (tptp.cC40xcomp @t1)) % 0.37/0.79 (define @t54 () (tptp.cC8xcomp @t10)) % 0.37/0.79 (define @t55 () (and @t14 @t54)) % 0.37/0.79 (define @t56 () (exists @t11 @t55)) % 0.37/0.79 (define @t57 () (tptp.cC42 @t1)) % 0.37/0.79 (define @t58 () (= @t57 @t56)) % 0.37/0.79 (define @t59 () (forall @t4 @t58)) % 0.37/0.79 (define @t60 () (tptp.cC44 @t1)) % 0.37/0.79 (define @t61 () (tptp.cC46 @t1)) % 0.37/0.79 (define @t62 () (tptp.cC46xcomp @t1)) % 0.37/0.79 (define @t63 () (tptp.cC8xcomp @t1)) % 0.37/0.79 (define @t64 () (tptp.cC48 @t1)) % 0.37/0.79 (define @t65 () (tptp.cC48xcomp @t1)) % 0.37/0.79 (define @t66 () (tptp.cC50 @t1)) % 0.37/0.79 (define @t67 () (tptp.cC52 @t1)) % 0.37/0.79 (define @t68 () (tptp.cC52xcomp @t1)) % 0.37/0.79 (define @t69 () (tptp.cC54 @t1)) % 0.37/0.79 (define @t70 () (tptp.cC54xcomp @t1)) % 0.37/0.79 (define @t71 () (tptp.cC56 @t1)) % 0.37/0.79 (define @t72 () (tptp.cC58 @t1)) % 0.37/0.79 (define @t73 () (tptp.cC58xcomp @t1)) % 0.37/0.79 (define @t74 () (tptp.cC12xcomp @t10)) % 0.37/0.79 (define @t75 () (and @t14 @t74)) % 0.37/0.79 (define @t76 () (exists @t11 @t75)) % 0.37/0.79 (define @t77 () (tptp.cC60 @t1)) % 0.37/0.79 (define @t78 () (= @t77 @t76)) % 0.37/0.79 (define @t79 () (forall @t4 @t78)) % 0.37/0.79 (define @t80 () (tptp.cC62 @t1)) % 0.37/0.79 (define @t81 () (forall @t4 (= @t80 (and @t77 @t73)))) % 0.37/0.79 (define @t82 () (tptp.cC64 @t1)) % 0.37/0.79 (define @t83 () (tptp.cC64xcomp @t1)) % 0.37/0.79 (define @t84 () (tptp.cC66 @t1)) % 0.37/0.79 (define @t85 () (tptp.cC66xcomp @t1)) % 0.37/0.79 (define @t86 () (tptp.cC68 @t1)) % 0.37/0.79 (define @t87 () (tptp.cC70 @t1)) % 0.37/0.79 (define @t88 () (tptp.cC70xcomp @t1)) % 0.37/0.79 (define @t89 () (tptp.cC72 @t1)) % 0.37/0.79 (define @t90 () (tptp.cC72xcomp @t1)) % 0.37/0.79 (define @t91 () (tptp.cC74 @t1)) % 0.37/0.79 (define @t92 () (tptp.cC74xcomp @t1)) % 0.37/0.79 (define @t93 () (tptp.cC76 @t1)) % 0.37/0.79 (define @t94 () (forall @t4 (= @t93 (and @t92 @t80)))) % 0.37/0.79 (define @t95 () (tptp.cC78 @t1)) % 0.37/0.79 (define @t96 () (tptp.cC78xcomp @t1)) % 0.37/0.79 (define @t97 () (tptp.cC80 @t1)) % 0.37/0.79 (define @t98 () (tptp.cC82 @t1)) % 0.37/0.79 (define @t99 () (tptp.cC84 @t1)) % 0.37/0.79 (define @t100 () (tptp.cC84xcomp @t1)) % 0.37/0.79 (define @t101 () (tptp.cC86 @t1)) % 0.37/0.79 (define @t102 () (tptp.cC86xcomp @t1)) % 0.37/0.79 (define @t103 () (tptp.cC88 @t1)) % 0.37/0.79 (define @t104 () (tptp.cC90 @t1)) % 0.37/0.79 (define @t105 () (tptp.cC90xcomp @t1)) % 0.37/0.79 (define @t106 () (tptp.cC92 @t1)) % 0.37/0.79 (define @t107 () (tptp.cC92xcomp @t1)) % 0.37/0.79 (define @t108 () (tptp.cC94 @t1)) % 0.37/0.79 (define @t109 () (tptp.cC94xcomp @t1)) % 0.37/0.79 (define @t110 () (tptp.cC96 @t1)) % 0.37/0.79 (define @t111 () (tptp.cC96xcomp @t1)) % 0.37/0.79 (define @t112 () (tptp.cC98 @t1)) % 0.37/0.79 (define @t113 () (tptp.rR1 tptp.iV16439 @t1)) % 0.37/0.79 (define @t114 () (forall @t4 (=> @t113 @t112))) % 0.37/0.79 (define @t115 () (tptp.cowlThing tptp.iV16439)) % 0.37/0.79 (define @t116 () (tptp.cTEST tptp.iV16439)) % 0.37/0.79 (define @t117 () (tptp.rR1 tptp.iV16439 tptp.iV16440)) % 0.37/0.79 (define @t118 () (tptp.cowlThing tptp.iV16440)) % 0.37/0.79 (define @t119 () (tptp.cC96xcomp tptp.iV16440)) % 0.37/0.79 (define @t120 () (tptp.rR1 tptp.iV16440 @t1)) % 0.37/0.79 (define @t121 () (forall @t4 (=> @t120 @t93))) % 0.37/0.79 (define @t122 () (tptp.cC102xcomp tptp.iV16440)) % 0.37/0.79 (define @t123 () (tptp.cC78xcomp tptp.iV16440)) % 0.37/0.79 (define @t124 () (tptp.rR1 tptp.iV16440 tptp.iV16463)) % 0.37/0.79 (define @t125 () (tptp.cowlThing tptp.iV16448)) % 0.37/0.79 (define @t126 () (tptp.cTOP tptp.iV16448)) % 0.37/0.79 (define @t127 () (tptp.rR1 tptp.iV16448 @t1)) % 0.37/0.79 (define @t128 () (tptp.cC36xcomp tptp.iV16448)) % 0.37/0.79 (define @t129 () (tptp.cC74xcomp tptp.iV16453)) % 0.37/0.79 (define @t130 () (tptp.cowlThing tptp.iV16453)) % 0.37/0.79 (define @t131 () (tptp.rR1 tptp.iV16453 @t1)) % 0.37/0.79 (define @t132 () (forall @t4 (=> @t131 @t71))) % 0.37/0.79 (define @t133 () (tptp.cC58xcomp tptp.iV16453)) % 0.37/0.79 (define @t134 () (tptp.rR1 tptp.iV16453 tptp.iV16461)) % 0.37/0.79 (define @t135 () (tptp.rR1 tptp.iV16455 @t1)) % 0.37/0.79 (define @t136 () (tptp.cowlThing tptp.iV16455)) % 0.37/0.79 (define @t137 () (tptp.cC40xcomp tptp.iV16455)) % 0.37/0.79 (define @t138 () (tptp.cC54xcomp tptp.iV16455)) % 0.37/0.79 (define @t139 () (tptp.rR1 tptp.iV16455 tptp.iV16460)) % 0.37/0.79 (define @t140 () (tptp.rR1 tptp.iV16457 @t1)) % 0.37/0.79 (define @t141 () (tptp.cowlThing tptp.iV16457)) % 0.37/0.79 (define @t142 () (tptp.cTOP tptp.iV16457)) % 0.37/0.79 (define @t143 () (tptp.cC36xcomp tptp.iV16457)) % 0.37/0.79 (define @t144 () (tptp.cowlThing tptp.iV16459)) % 0.37/0.79 (define @t145 () (tptp.cC30xcomp tptp.iV16459)) % 0.37/0.79 (define @t146 () (tptp.cC84xcomp tptp.iV16459)) % 0.37/0.79 (define @t147 () (tptp.cC46xcomp tptp.iV16459)) % 0.37/0.79 (define @t148 () (tptp.cC64xcomp tptp.iV16459)) % 0.37/0.79 (define @t149 () (tptp.cC86xcomp tptp.iV16459)) % 0.37/0.79 (define @t150 () (tptp.cC32xcomp tptp.iV16459)) % 0.37/0.79 (define @t151 () (tptp.cC48xcomp tptp.iV16459)) % 0.37/0.79 (define @t152 () (tptp.cC66xcomp tptp.iV16459)) % 0.37/0.79 (define @t153 () (tptp.rR1 tptp.iV16460 @t1)) % 0.37/0.79 (define @t154 () (tptp.cowlThing tptp.iV16460)) % 0.37/0.79 (define @t155 () (tptp.cTOP tptp.iV16460)) % 0.37/0.79 (define @t156 () (tptp.cC8xcomp tptp.iV16460)) % 0.37/0.79 (define @t157 () (tptp.cC36xcomp tptp.iV16460)) % 0.37/0.79 (define @t158 () (tptp.cowlThing tptp.iV16461)) % 0.37/0.79 (define @t159 () (tptp.cC40xcomp tptp.iV16461)) % 0.37/0.79 (define @t160 () (tptp.rR1 tptp.iV16461 @t1)) % 0.37/0.79 (define @t161 () (tptp.cC12xcomp tptp.iV16461)) % 0.37/0.79 (define @t162 () (tptp.cC54xcomp tptp.iV16461)) % 0.37/0.79 (define @t163 () (tptp.rR1 tptp.iV16462 @t1)) % 0.37/0.79 (define @t164 () (tptp.cowlThing tptp.iV16462)) % 0.37/0.79 (define @t165 () (tptp.cTOP tptp.iV16462)) % 0.37/0.79 (define @t166 () (tptp.cC36xcomp tptp.iV16462)) % 0.37/0.79 (define @t167 () (tptp.cC74xcomp tptp.iV16463)) % 0.37/0.79 (define @t168 () (tptp.cowlThing tptp.iV16463)) % 0.37/0.79 (define @t169 () (tptp.rR1 tptp.iV16463 @t1)) % 0.37/0.79 (define @t170 () (forall @t4 (=> @t169 @t71))) % 0.37/0.79 (define @t171 () (tptp.cC58xcomp tptp.iV16463)) % 0.37/0.79 (define @t172 () (tptp.rR1 tptp.iV16463 tptp.iV16464)) % 0.37/0.79 (define @t173 () (tptp.cowlThing tptp.iV16464)) % 0.37/0.79 (define @t174 () (tptp.rR1 tptp.iV16464 @t1)) % 0.37/0.79 (define @t175 () (tptp.cC40xcomp tptp.iV16464)) % 0.37/0.79 (define @t176 () (tptp.cC54xcomp tptp.iV16464)) % 0.37/0.79 (define @t177 () (tptp.rR1 tptp.iV16465 @t1)) % 0.37/0.79 (define @t178 () (tptp.cowlThing tptp.iV16465)) % 0.37/0.79 (define @t179 () (tptp.cTOP tptp.iV16465)) % 0.37/0.79 (define @t180 () (tptp.cC36xcomp tptp.iV16465)) % 0.37/0.79 (define @t181 () (tptp.cC38 tptp.iV16465)) % 0.37/0.79 (define @t182 () (tptp.cC44 tptp.iV16464)) % 0.37/0.79 (define @t183 () (tptp.cC42 tptp.iV16464)) % 0.37/0.79 (define @t184 () (tptp.cC56 tptp.iV16464)) % 0.37/0.79 (define @t185 () (tptp.cC60 tptp.iV16463)) % 0.37/0.79 (define @t186 () (tptp.cC62 tptp.iV16463)) % 0.37/0.79 (define @t187 () (tptp.cC76 tptp.iV16463)) % 0.37/0.79 (define @t188 () (tptp.cC38 tptp.iV16462)) % 0.37/0.79 (define @t189 () (tptp.cC44 tptp.iV16461)) % 0.37/0.79 (define @t190 () (tptp.cC56 tptp.iV16461)) % 0.37/0.79 (define @t191 () (tptp.cC42 tptp.iV16461)) % 0.37/0.79 (define @t192 () (tptp.cC38 tptp.iV16460)) % 0.37/0.79 (define @t193 () (tptp.cC68 tptp.iV16459)) % 0.37/0.79 (define @t194 () (tptp.cC34 tptp.iV16459)) % 0.37/0.79 (define @t195 () (tptp.cC88 tptp.iV16459)) % 0.37/0.79 (define @t196 () (tptp.cC50 tptp.iV16459)) % 0.37/0.79 (define @t197 () (tptp.cC38 tptp.iV16457)) % 0.37/0.79 (define @t198 () (tptp.cC42 tptp.iV16455)) % 0.37/0.79 (define @t199 () (tptp.cC44 tptp.iV16455)) % 0.37/0.79 (define @t200 () (tptp.cC56 tptp.iV16455)) % 0.37/0.79 (define @t201 () (tptp.cC60 tptp.iV16453)) % 0.37/0.79 (define @t202 () (tptp.cC62 tptp.iV16453)) % 0.37/0.79 (define @t203 () (tptp.cC76 tptp.iV16453)) % 0.37/0.79 (define @t204 () (tptp.cC38 tptp.iV16448)) % 0.37/0.79 (define @t205 () (tptp.cC82 tptp.iV16440)) % 0.37/0.80 (define @t206 () (tptp.cC80 tptp.iV16440)) % 0.37/0.80 (define @t207 () (tptp.cC98 tptp.iV16440)) % 0.37/0.80 (define @t208 () (tptp.cC28 tptp.iV16439)) % 0.37/0.80 (define @t209 () (tptp.cC106 tptp.iV16439)) % 0.37/0.80 (define @t210 () (tptp.cC104 tptp.iV16439)) % 0.37/0.80 (define @t211 () (tptp.cC108 tptp.iV16439)) % 0.37/0.80 (define @t212 () (tptp.cC130 tptp.iV16439)) % 0.37/0.80 (define @t213 () (and @t5 @t6 @t212 @t211 @t210 @t209 @t208 @t115 @t207 @t206 @t205 @t118 @t204 @t125 @t203 @t202 @t130 @t201 @t200 @t199 @t198 @t136 @t197 @t141 @t196 @t195 @t194 @t193 @t144 @t192 @t154 @t191 @t190 @t189 @t158 @t188 @t164 @t187 @t186 @t168 @t185 @t184 @t183 @t182 @t173 @t181 @t178)) % 0.37/0.80 (define @t214 () (not @t213)) % 0.37/0.80 (define @t215 () (forall @t11 (not @t75))) % 0.37/0.80 (define @t216 () (not @t215)) % 0.37/0.80 (define @t217 () (@list tptp.iV16453)) % 0.37/0.80 (define @t218 () (@list tptp.iV16455)) % 0.37/0.80 (define @t219 () (forall @t11 (not @t55))) % 0.37/0.80 (define @t220 () (not @t219)) % 0.37/0.80 (define @t221 () (not @t156)) % 0.37/0.80 (define @t222 () (not @t139)) % 0.37/0.80 (define @t223 () (or @t222 @t221)) % 0.37/0.80 (define @t224 () (not @t223)) % 0.37/0.80 (define @t225 () (@list false false)) % 0.37/0.80 (define @t226 () (forall @t11 (or (not (tptp.rR1 tptp.iV16455 @t10)) (not @t54)))) % 0.37/0.80 (define @t227 () (@list tptp.iV16460)) % 0.37/0.80 (define @t228 () (not @t226)) % 0.37/0.80 (define @t229 () (@list true)) % 0.37/0.80 (define @t230 () (= @t198 @t228)) % 0.37/0.80 (define @t231 () (not @t230)) % 0.37/0.80 (define @t232 () (@list true false)) % 0.37/0.80 (define @t233 () (and @t137 @t198)) % 0.37/0.80 (define @t234 () (not @t198)) % 0.37/0.80 (define @t235 () (= @t199 @t233)) % 0.37/0.80 (define @t236 () (not @t235)) % 0.37/0.80 (define @t237 () (not @t233)) % 0.37/0.80 (define @t238 () (and @t138 @t199)) % 0.37/0.80 (define @t239 () (not @t199)) % 0.37/0.80 (define @t240 () (= @t200 @t238)) % 0.37/0.80 (define @t241 () (not @t240)) % 0.37/0.80 (define @t242 () (not @t238)) % 0.37/0.80 (define @t243 () (and @t129 @t202)) % 0.37/0.80 (define @t244 () (= @t203 @t243)) % 0.37/0.80 (define @t245 () (not @t244)) % 0.37/0.80 (define @t246 () (not @t203)) % 0.37/0.80 (define @t247 () (not @t243)) % 0.37/0.80 (define @t248 () (and @t201 @t133)) % 0.37/0.80 (define @t249 () (= @t202 @t248)) % 0.37/0.80 (define @t250 () (not @t249)) % 0.37/0.80 (define @t251 () (not @t202)) % 0.37/0.80 (define @t252 () (not @t248)) % 0.37/0.80 (define @t253 () (not @t200)) % 0.37/0.80 (define @t254 () (forall @t4 @t2)) % 0.37/0.80 (define @t255 () (@list @t1)) % 0.37/0.80 (define @t256 () (@var "BOUND_VARIABLE_8558" $$unsorted)) % 0.37/0.80 (define @t257 () (forall @t4 @t3)) % 0.37/0.80 (define @t258 () (@var "BOUND_VARIABLE_8553" $$unsorted)) % 0.37/0.80 (define @t259 () (and @t257 @t254)) % 0.37/0.80 (define @t260 () (and @t179 @t180)) % 0.37/0.80 (define @t261 () (= @t181 @t260)) % 0.37/0.80 (define @t262 () (@list tptp.iV16464)) % 0.37/0.80 (define @t263 () (not @t172)) % 0.37/0.80 (define @t264 () (or @t263 @t184)) % 0.37/0.80 (define @t265 () (and @t176 @t182)) % 0.37/0.80 (define @t266 () (= @t184 @t265)) % 0.37/0.80 (define @t267 () (not @t184)) % 0.37/0.80 (define @t268 () (@list false)) % 0.37/0.80 (define @t269 () (and @t175 @t183)) % 0.37/0.80 (define @t270 () (= @t182 @t269)) % 0.37/0.80 (define @t271 () (not @t182)) % 0.37/0.80 (define @t272 () (@list tptp.iV16463)) % 0.37/0.80 (define @t273 () (not @t124)) % 0.37/0.80 (define @t274 () (or @t273 @t187)) % 0.37/0.80 (define @t275 () (and @t167 @t186)) % 0.37/0.80 (define @t276 () (= @t187 @t275)) % 0.37/0.80 (define @t277 () (not @t187)) % 0.37/0.80 (define @t278 () (and @t185 @t171)) % 0.37/0.80 (define @t279 () (= @t186 @t278)) % 0.37/0.80 (define @t280 () (not @t186)) % 0.37/0.80 (define @t281 () (and @t165 @t166)) % 0.37/0.80 (define @t282 () (= @t188 @t281)) % 0.37/0.80 (define @t283 () (@list tptp.iV16461)) % 0.37/0.80 (define @t284 () (not @t134)) % 0.37/0.80 (define @t285 () (or @t284 @t190)) % 0.37/0.80 (define @t286 () (and @t162 @t189)) % 0.37/0.80 (define @t287 () (= @t190 @t286)) % 0.37/0.80 (define @t288 () (not @t190)) % 0.37/0.80 (define @t289 () (and @t159 @t191)) % 0.37/0.80 (define @t290 () (= @t189 @t289)) % 0.37/0.80 (define @t291 () (not @t189)) % 0.37/0.80 (define @t292 () (and @t155 @t157)) % 0.37/0.80 (define @t293 () (= @t192 @t292)) % 0.37/0.80 (define @t294 () (@list tptp.iV16459)) % 0.37/0.80 (define @t295 () (and @t148 @t152)) % 0.37/0.80 (define @t296 () (= @t193 @t295)) % 0.37/0.80 (define @t297 () (and @t145 @t150)) % 0.37/0.80 (define @t298 () (= @t194 @t297)) % 0.37/0.80 (define @t299 () (and @t146 @t149)) % 0.37/0.80 (define @t300 () (= @t195 @t299)) % 0.37/0.80 (define @t301 () (and @t147 @t151)) % 0.37/0.80 (define @t302 () (= @t196 @t301)) % 0.37/0.80 (define @t303 () (and @t142 @t143)) % 0.37/0.80 (define @t304 () (= @t197 @t303)) % 0.37/0.80 (define @t305 () (@list tptp.iV16440)) % 0.37/0.80 (define @t306 () (not @t117)) % 0.37/0.80 (define @t307 () (or @t306 @t207)) % 0.37/0.80 (define @t308 () (and @t119 @t205)) % 0.37/0.80 (define @t309 () (= @t207 @t308)) % 0.37/0.80 (define @t310 () (not @t207)) % 0.37/0.80 (define @t311 () (and @t206 @t123)) % 0.37/0.80 (define @t312 () (= @t205 @t311)) % 0.37/0.80 (define @t313 () (not @t205)) % 0.37/0.80 (define @t314 () (forall @t11 (not @t19))) % 0.37/0.80 (define @t315 () (not @t314)) % 0.37/0.80 (define @t316 () (@list tptp.iV16439)) % 0.37/0.80 (define @t317 () (not @t122)) % 0.37/0.80 (define @t318 () (or @t306 @t317)) % 0.37/0.80 (define @t319 () (not @t318)) % 0.37/0.80 (define @t320 () (forall @t11 (or (not (tptp.rR1 tptp.iV16439 @t10)) (not @t18)))) % 0.37/0.80 (define @t321 () (not @t320)) % 0.37/0.80 (define @t322 () (= @t210 @t321)) % 0.37/0.80 (define @t323 () (not @t322)) % 0.37/0.80 (define @t324 () (and @t126 @t128)) % 0.37/0.80 (define @t325 () (= @t204 @t324)) % 0.37/0.80 (define @t326 () (and @t211 @t212)) % 0.37/0.80 (define @t327 () (= @t116 @t326)) % 0.37/0.80 (define @t328 () (not @t326)) % 0.37/0.80 (define @t329 () (@list @t326)) % 0.37/0.80 (define @t330 () (and @t208 @t209)) % 0.37/0.80 (define @t331 () (= @t211 @t330)) % 0.37/0.80 (define @t332 () (not @t211)) % 0.37/0.80 (define @t333 () (not @t330)) % 0.37/0.80 (define @t334 () (@list @t330)) % 0.37/0.80 (define @t335 () (forall (@list @t256) (not (tptp.cowlNothing @t256)))) % 0.37/0.80 (define @t336 () (forall (@list @t258) (tptp.cowlThing @t258))) % 0.37/0.80 (define @t337 () (not @t201)) % 0.37/0.80 (define @t338 () (@list false true)) % 0.37/0.80 (define @t339 () (forall @t11 (or (not (tptp.rR1 tptp.iV16453 @t10)) (not @t74)))) % 0.37/0.80 (define @t340 () (not @t339)) % 0.37/0.80 (define @t341 () (= @t201 @t340)) % 0.37/0.80 (define @t342 () (not @t341)) % 0.37/0.80 (define @t343 () (not @t161)) % 0.37/0.80 (define @t344 () (or @t284 @t343)) % 0.37/0.80 (define @t345 () (not @t344)) % 0.37/0.80 (assume @p1 @t5) % 0.37/0.80 (assume @p2 @t6) % 0.37/0.80 (assume @p3 (forall @t4 (= @t9 (and @t8 @t7)))) % 0.37/0.80 (assume @p4 (forall @t4 (= @t9 (not (exists @t11 (tptp.ra_Px73 @t1 @t10)))))) % 0.37/0.80 (assume @p5 (forall @t4 (= (tptp.cC10xcomp @t1) (exists @t13 (tptp.ra_Px73 @t1 @t12))))) % 0.37/0.80 (assume @p6 (forall @t4 (= @t15 (exists @t11 (and @t14 (tptp.cC98xcomp @t10)))))) % 0.37/0.80 (assume @p7 (forall @t4 (= @t15 (not (exists @t11 (tptp.ra_Px37 @t1 @t10)))))) % 0.37/0.80 (assume @p8 (forall @t4 (= @t16 (exists @t13 (tptp.ra_Px37 @t1 @t12))))) % 0.37/0.80 (assume @p9 (forall @t4 (= (tptp.cC102 @t1) (exists @t13 (tptp.ra_Px36 @t1 @t12))))) % 0.37/0.80 (assume @p10 (forall @t4 (= @t17 (not (exists @t11 (tptp.ra_Px36 @t1 @t10)))))) % 0.37/0.80 (assume @p11 @t23) % 0.37/0.80 (assume @p12 (forall @t4 (= @t24 (and @t21 @t16)))) % 0.37/0.80 (assume @p13 (forall @t4 (= @t26 (and @t25 @t24)))) % 0.37/0.80 (assume @p14 (forall @t4 (= @t29 (and @t28 @t27)))) % 0.37/0.80 (assume @p15 (forall @t4 (= @t30 (and @t29 @t17)))) % 0.37/0.80 (assume @p16 (forall @t4 (= (tptp.cC114 @t1) (exists @t13 (tptp.ra_Px41 @t1 @t12))))) % 0.37/0.80 (assume @p17 (forall @t4 (= @t31 (not (exists @t11 (tptp.ra_Px41 @t1 @t10)))))) % 0.37/0.80 (assume @p18 (forall @t4 (= @t32 (and @t30 @t31)))) % 0.37/0.80 (assume @p19 (forall @t4 (= (tptp.cC118 @t1) (exists @t13 (tptp.ra_Px42 @t1 @t12))))) % 0.37/0.80 (assume @p20 (forall @t4 (= @t33 (not (exists @t11 (tptp.ra_Px42 @t1 @t10)))))) % 0.37/0.80 (assume @p21 (forall @t4 (= @t34 (exists @t13 (tptp.ra_Px18 @t1 @t12))))) % 0.37/0.80 (assume @p22 (forall @t4 (= @t27 (not (exists @t11 (tptp.ra_Px18 @t1 @t10)))))) % 0.37/0.80 (assume @p23 (forall @t4 (= @t35 (and @t32 @t33)))) % 0.37/0.80 (assume @p24 (forall @t4 (= @t35 (not (exists @t11 (tptp.ra_Px43 @t1 @t10)))))) % 0.37/0.80 (assume @p25 (forall @t4 (= (tptp.cC120xcomp @t1) (exists @t13 (tptp.ra_Px43 @t1 @t12))))) % 0.37/0.80 (assume @p26 (forall @t4 (= (tptp.cC122 @t1) (exists @t11 (and @t14 (tptp.cC120xcomp @t10)))))) % 0.37/0.80 (assume @p27 (forall @t4 (= (tptp.cC124 @t1) (exists @t11 (and @t14 (tptp.cC122 @t10)))))) % 0.37/0.80 (assume @p28 (forall @t4 (= (tptp.cC126 @t1) (exists @t11 (and @t14 (tptp.cC124 @t10)))))) % 0.37/0.80 (assume @p29 (forall @t4 (= (tptp.cC128 @t1) (exists @t11 (and @t14 (tptp.cC126 @t10)))))) % 0.37/0.80 (assume @p30 (forall @t4 (= @t36 (exists @t11 (and @t14 (tptp.cC128 @t10)))))) % 0.37/0.80 (assume @p31 (forall @t4 (= @t37 (exists @t13 (tptp.ra_Px74 @t1 @t12))))) % 0.37/0.80 (assume @p32 (forall @t4 (= @t37 (and @t9 @t34)))) % 0.37/0.80 (assume @p33 (forall @t4 (= (tptp.cC14xcomp @t1) (not (exists @t11 (tptp.ra_Px74 @t1 @t10)))))) % 0.37/0.80 (assume @p34 (forall @t4 (= @t38 (exists @t13 (tptp.ra_Px27 @t1 @t12))))) % 0.37/0.80 (assume @p35 (forall @t4 (= (tptp.cC16xcomp @t1) (not (exists @t11 (tptp.ra_Px27 @t1 @t10)))))) % 0.37/0.80 (assume @p36 (forall @t4 (= @t39 (not (exists @t11 (tptp.ra_Px1 @t1 @t10)))))) % 0.37/0.80 (assume @p37 (forall @t4 (= @t39 (and @t37 @t38)))) % 0.37/0.80 (assume @p38 (forall @t4 (= (tptp.cC18xcomp @t1) (exists @t13 (tptp.ra_Px1 @t1 @t12))))) % 0.37/0.80 (assume @p39 (forall @t4 (= @t40 (exists @t13 (tptp.ra_Px2 @t1 @t12))))) % 0.37/0.80 (assume @p40 (forall @t4 (= @t41 (not (exists @t11 (tptp.ra_Px2 @t1 @t10)))))) % 0.37/0.80 (assume @p41 (forall @t4 (= (tptp.cC20 @t1) (exists @t11 (and @t14 (tptp.cC18xcomp @t10)))))) % 0.37/0.80 (assume @p42 (forall @t4 (= (tptp.cC22 @t1) (exists @t11 (and @t14 (tptp.cC20 @t10)))))) % 0.37/0.80 (assume @p43 (forall @t4 (= (tptp.cC24 @t1) (exists @t11 (and @t14 (tptp.cC22 @t10)))))) % 0.37/0.80 (assume @p44 (forall @t4 (= (tptp.cC26 @t1) (exists @t11 (and @t14 (tptp.cC24 @t10)))))) % 0.37/0.80 (assume @p45 (forall @t4 (= @t25 (exists @t11 (and @t14 (tptp.cC26 @t10)))))) % 0.37/0.80 (assume @p46 (forall @t4 (= @t42 (not (exists @t11 (tptp.ra_Px4 @t1 @t10)))))) % 0.37/0.80 (assume @p47 (forall @t4 (= @t42 @t44))) % 0.37/0.80 (assume @p48 (forall @t4 (= @t45 (exists @t13 (tptp.ra_Px4 @t1 @t12))))) % 0.37/0.80 (assume @p49 (forall @t4 (= @t46 (exists @t13 (tptp.ra_Px5 @t1 @t12))))) % 0.37/0.80 (assume @p50 (forall @t4 (= @t46 (and @t28 @t41)))) % 0.37/0.80 (assume @p51 (forall @t4 (= @t47 (not (exists @t11 (tptp.ra_Px5 @t1 @t10)))))) % 0.37/0.80 (assume @p52 (forall @t4 (= @t48 (exists @t13 (tptp.ra_Px6 @t1 @t12))))) % 0.37/0.80 (assume @p53 (forall @t4 (= @t48 (and @t45 @t47)))) % 0.37/0.80 (assume @p54 (forall @t4 (= (tptp.cC34xcomp @t1) (not (exists @t11 (tptp.ra_Px6 @t1 @t10)))))) % 0.37/0.80 (assume @p55 (forall @t4 (= @t49 (not (exists @t11 (tptp.ra_Px7 @t1 @t10)))))) % 0.37/0.80 (assume @p56 (forall @t4 (= @t49 (exists @t11 (and @t14 (tptp.cC34xcomp @t10)))))) % 0.37/0.80 (assume @p57 (forall @t4 (= @t50 (exists @t13 (tptp.ra_Px7 @t1 @t12))))) % 0.37/0.80 (assume @p58 (forall @t4 (= @t51 (and (tptp.cTOP @t1) @t50)))) % 0.37/0.80 (assume @p59 (forall @t4 (= @t51 (exists @t13 (tptp.ra_Px8 @t1 @t12))))) % 0.37/0.80 (assume @p60 (forall @t4 (= (tptp.cC38xcomp @t1) (not (exists @t11 (tptp.ra_Px8 @t1 @t10)))))) % 0.37/0.80 (assume @p61 (forall @t4 (= @t43 (exists @t13 (tptp.ra_Px3 @t1 @t12))))) % 0.37/0.80 (assume @p62 (forall @t4 (= @t28 (not (exists @t11 (tptp.ra_Px3 @t1 @t10)))))) % 0.37/0.80 (assume @p63 (forall @t4 (= @t52 (not (exists @t11 (tptp.ra_Px10 @t1 @t10)))))) % 0.37/0.80 (assume @p64 (forall @t4 (= @t52 (exists @t11 (and @t14 (tptp.cC38xcomp @t10)))))) % 0.37/0.80 (assume @p65 (forall @t4 (= @t53 (exists @t13 (tptp.ra_Px10 @t1 @t12))))) % 0.37/0.80 (assume @p66 @t59) % 0.37/0.80 (assume @p67 (forall @t4 (= @t60 (and @t53 @t57)))) % 0.37/0.80 (assume @p68 (forall @t4 (= @t61 (not (exists @t11 (tptp.ra_Px13 @t1 @t10)))))) % 0.37/0.80 (assume @p69 (forall @t4 (= @t61 (and @t8 @t43)))) % 0.37/0.80 (assume @p70 (forall @t4 (= @t62 (exists @t13 (tptp.ra_Px13 @t1 @t12))))) % 0.37/0.80 (assume @p71 (forall @t4 (= @t64 (and @t28 @t63)))) % 0.37/0.80 (assume @p72 (forall @t4 (= @t64 (exists @t13 (tptp.ra_Px14 @t1 @t12))))) % 0.37/0.80 (assume @p73 (forall @t4 (= @t65 (not (exists @t11 (tptp.ra_Px14 @t1 @t10)))))) % 0.37/0.80 (assume @p74 (forall @t4 (= @t66 (and @t62 @t65)))) % 0.37/0.80 (assume @p75 (forall @t4 (= @t66 (exists @t13 (tptp.ra_Px15 @t1 @t12))))) % 0.37/0.80 (assume @p76 (forall @t4 (= (tptp.cC50xcomp @t1) (not (exists @t11 (tptp.ra_Px15 @t1 @t10)))))) % 0.37/0.80 (assume @p77 (forall @t4 (= @t67 (not (exists @t11 (tptp.ra_Px49 @t1 @t10)))))) % 0.37/0.80 (assume @p78 (forall @t4 (= @t67 (exists @t11 (and @t14 (tptp.cC50xcomp @t10)))))) % 0.37/0.80 (assume @p79 (forall @t4 (= @t68 (exists @t13 (tptp.ra_Px49 @t1 @t12))))) % 0.37/0.80 (assume @p80 (forall @t4 (= @t69 (not (exists @t11 (tptp.ra_Px16 @t1 @t10)))))) % 0.37/0.80 (assume @p81 (forall @t4 (= @t69 (exists @t11 (and @t14 (tptp.cC52 @t10)))))) % 0.37/0.80 (assume @p82 (forall @t4 (= @t70 (exists @t13 (tptp.ra_Px16 @t1 @t12))))) % 0.37/0.80 (assume @p83 (forall @t4 (= @t71 (and @t70 @t60)))) % 0.37/0.80 (assume @p84 (forall @t4 (= @t71 (exists @t13 (tptp.ra_Px17 @t1 @t12))))) % 0.37/0.80 (assume @p85 (forall @t4 (= (tptp.cC56xcomp @t1) (not (exists @t11 (tptp.ra_Px17 @t1 @t10)))))) % 0.37/0.80 (assume @p86 (forall @t4 (= @t72 (exists @t11 (and @t14 (tptp.cC56xcomp @t10)))))) % 0.37/0.80 (assume @p87 (forall @t4 (= @t72 (not (exists @t11 (tptp.ra_Px19 @t1 @t10)))))) % 0.37/0.80 (assume @p88 (forall @t4 (= @t73 (exists @t13 (tptp.ra_Px19 @t1 @t12))))) % 0.37/0.80 (assume @p89 (forall @t4 (= @t7 @t44))) % 0.37/0.80 (assume @p90 (forall @t4 (= @t7 (exists @t13 (tptp.ra_Px72 @t1 @t12))))) % 0.37/0.80 (assume @p91 (forall @t4 (= (tptp.cC6xcomp @t1) (not (exists @t11 (tptp.ra_Px72 @t1 @t10)))))) % 0.37/0.80 (assume @p92 @t79) % 0.37/0.80 (assume @p93 @t81) % 0.37/0.80 (assume @p94 (forall @t4 (= @t82 (and @t8 @t34)))) % 0.37/0.80 (assume @p95 (forall @t4 (= @t82 (not (exists @t11 (tptp.ra_Px22 @t1 @t10)))))) % 0.37/0.80 (assume @p96 (forall @t4 (= @t83 (exists @t13 (tptp.ra_Px22 @t1 @t12))))) % 0.37/0.80 (assume @p97 (forall @t4 (= @t84 (and @t27 @t63)))) % 0.37/0.80 (assume @p98 (forall @t4 (= @t84 (exists @t13 (tptp.ra_Px23 @t1 @t12))))) % 0.37/0.80 (assume @p99 (forall @t4 (= @t85 (not (exists @t11 (tptp.ra_Px23 @t1 @t10)))))) % 0.37/0.80 (assume @p100 (forall @t4 (= @t86 (exists @t13 (tptp.ra_Px24 @t1 @t12))))) % 0.37/0.80 (assume @p101 (forall @t4 (= @t86 (and @t83 @t85)))) % 0.37/0.80 (assume @p102 (forall @t4 (= (tptp.cC68xcomp @t1) (not (exists @t11 (tptp.ra_Px24 @t1 @t10)))))) % 0.37/0.80 (assume @p103 (forall @t4 (= @t87 (exists @t11 (and @t14 (tptp.cC68xcomp @t10)))))) % 0.37/0.80 (assume @p104 (forall @t4 (= @t87 (exists @t13 (tptp.ra_Px51 @t1 @t12))))) % 0.37/0.80 (assume @p105 (forall @t4 (= @t88 (not (exists @t11 (tptp.ra_Px51 @t1 @t10)))))) % 0.37/0.80 (assume @p106 (forall @t4 (= @t89 (exists @t11 (and @t14 (tptp.cC70 @t10)))))) % 0.37/0.80 (assume @p107 (forall @t4 (= @t89 (not (exists @t11 (tptp.ra_Px58 @t1 @t10)))))) % 0.37/0.80 (assume @p108 (forall @t4 (= @t90 (exists @t13 (tptp.ra_Px58 @t1 @t12))))) % 0.37/0.80 (assume @p109 (forall @t4 (= @t91 (exists @t11 (and @t14 (tptp.cC72 @t10)))))) % 0.37/0.80 (assume @p110 (forall @t4 (= @t91 (not (exists @t11 (tptp.ra_Px25 @t1 @t10)))))) % 0.37/0.80 (assume @p111 (forall @t4 (= @t92 (exists @t13 (tptp.ra_Px25 @t1 @t12))))) % 0.37/0.80 (assume @p112 (forall @t4 (= @t93 (exists @t13 (tptp.ra_Px26 @t1 @t12))))) % 0.37/0.80 (assume @p113 @t94) % 0.37/0.80 (assume @p114 (forall @t4 (= (tptp.cC76xcomp @t1) (not (exists @t11 (tptp.ra_Px26 @t1 @t10)))))) % 0.37/0.80 (assume @p115 (forall @t4 (= @t95 (exists @t11 (and @t14 (tptp.cC76xcomp @t10)))))) % 0.37/0.80 (assume @p116 (forall @t4 (= @t95 (not (exists @t11 (tptp.ra_Px28 @t1 @t10)))))) % 0.37/0.80 (assume @p117 (forall @t4 (= @t96 (exists @t13 (tptp.ra_Px28 @t1 @t12))))) % 0.37/0.80 (assume @p118 (forall @t4 (= @t8 (exists @t13 (tptp.ra_Px9 @t1 @t12))))) % 0.37/0.80 (assume @p119 (forall @t4 (= @t63 (not (exists @t11 (tptp.ra_Px9 @t1 @t10)))))) % 0.37/0.80 (assume @p120 (forall @t4 (= @t97 (exists @t11 (and @t14 (tptp.cC16xcomp @t10)))))) % 0.37/0.80 (assume @p121 (forall @t4 (= @t98 (and @t97 @t96)))) % 0.37/0.80 (assume @p122 (forall @t4 (= @t99 (not (exists @t11 (tptp.ra_Px31 @t1 @t10)))))) % 0.37/0.80 (assume @p123 (forall @t4 (= @t99 (and @t40 @t34)))) % 0.37/0.80 (assume @p124 (forall @t4 (= @t100 (exists @t13 (tptp.ra_Px31 @t1 @t12))))) % 0.37/0.80 (assume @p125 (forall @t4 (= @t101 (and @t27 @t41)))) % 0.37/0.80 (assume @p126 (forall @t4 (= @t101 (exists @t13 (tptp.ra_Px32 @t1 @t12))))) % 0.37/0.80 (assume @p127 (forall @t4 (= @t102 (not (exists @t11 (tptp.ra_Px32 @t1 @t10)))))) % 0.37/0.80 (assume @p128 (forall @t4 (= @t103 (exists @t13 (tptp.ra_Px33 @t1 @t12))))) % 0.37/0.80 (assume @p129 (forall @t4 (= @t103 (and @t100 @t102)))) % 0.37/0.80 (assume @p130 (forall @t4 (= (tptp.cC88xcomp @t1) (not (exists @t11 (tptp.ra_Px33 @t1 @t10)))))) % 0.37/0.80 (assume @p131 (forall @t4 (= @t104 (exists @t13 (tptp.ra_Px50 @t1 @t12))))) % 0.37/0.80 (assume @p132 (forall @t4 (= @t104 (exists @t11 (and @t14 (tptp.cC88xcomp @t10)))))) % 0.37/0.80 (assume @p133 (forall @t4 (= @t105 (not (exists @t11 (tptp.ra_Px50 @t1 @t10)))))) % 0.37/0.80 (assume @p134 (forall @t4 (= @t106 (exists @t13 (tptp.ra_Px57 @t1 @t12))))) % 0.37/0.80 (assume @p135 (forall @t4 (= @t106 (exists @t11 (and @t14 (tptp.cC90 @t10)))))) % 0.37/0.80 (assume @p136 (forall @t4 (= @t107 (not (exists @t11 (tptp.ra_Px57 @t1 @t10)))))) % 0.37/0.80 (assume @p137 (forall @t4 (= @t108 (exists @t11 (and @t14 (tptp.cC92 @t10)))))) % 0.37/0.80 (assume @p138 (forall @t4 (= @t108 (exists @t13 (tptp.ra_Px48 @t1 @t12))))) % 0.37/0.80 (assume @p139 (forall @t4 (= @t109 (not (exists @t11 (tptp.ra_Px48 @t1 @t10)))))) % 0.37/0.80 (assume @p140 (forall @t4 (= @t110 (exists @t11 (and @t14 (tptp.cC94 @t10)))))) % 0.37/0.80 (assume @p141 (forall @t4 (= @t110 (not (exists @t11 (tptp.ra_Px34 @t1 @t10)))))) % 0.37/0.80 (assume @p142 (forall @t4 (= @t111 (exists @t13 (tptp.ra_Px34 @t1 @t12))))) % 0.37/0.80 (assume @p143 (forall @t4 (= @t112 (exists @t13 (tptp.ra_Px35 @t1 @t12))))) % 0.37/0.80 (assume @p144 (forall @t4 (= @t112 (and @t111 @t98)))) % 0.37/0.80 (assume @p145 (forall @t4 (= (tptp.cC98xcomp @t1) (not (exists @t11 (tptp.ra_Px35 @t1 @t10)))))) % 0.37/0.80 (assume @p146 (forall @t4 (= (tptp.cTEST @t1) (and @t26 @t36)))) % 0.37/0.80 (assume @p147 @t114) % 0.37/0.80 (assume @p148 @t115) % 0.37/0.80 (assume @p149 (tptp.cC100xcomp tptp.iV16439)) % 0.37/0.80 (assume @p150 @t116) % 0.37/0.80 (assume @p151 @t117) % 0.37/0.80 (assume @p152 (tptp.rR1 tptp.iV16439 tptp.iV16442)) % 0.37/0.80 (assume @p153 (tptp.rR1 tptp.iV16439 tptp.iV16441)) % 0.37/0.80 (assume @p154 @t118) % 0.37/0.80 (assume @p155 @t119) % 0.37/0.80 (assume @p156 (forall @t4 (=> @t120 @t109))) % 0.37/0.80 (assume @p157 @t121) % 0.37/0.80 (assume @p158 @t122) % 0.37/0.80 (assume @p159 @t123) % 0.37/0.80 (assume @p160 @t124) % 0.37/0.80 (assume @p161 (tptp.cowlThing tptp.iV16441)) % 0.37/0.80 (assume @p162 (tptp.cowlThing tptp.iV16442)) % 0.37/0.80 (assume @p163 @t125) % 0.37/0.80 (assume @p164 @t126) % 0.37/0.80 (assume @p165 (tptp.cC52xcomp tptp.iV16448)) % 0.37/0.80 (assume @p166 (forall @t4 (=> @t127 @t66))) % 0.37/0.80 (assume @p167 (forall @t4 (=> @t127 @t86))) % 0.37/0.80 (assume @p168 (forall @t4 (=> @t127 @t48))) % 0.37/0.80 (assume @p169 @t128) % 0.37/0.80 (assume @p170 (tptp.cC90xcomp tptp.iV16448)) % 0.37/0.80 (assume @p171 (forall @t4 (=> @t127 @t103))) % 0.37/0.80 (assume @p172 (tptp.cC70xcomp tptp.iV16448)) % 0.37/0.80 (assume @p173 (tptp.rR1 tptp.iV16448 tptp.iV16449)) % 0.37/0.80 (assume @p174 (tptp.cowlThing tptp.iV16449)) % 0.37/0.80 (assume @p175 @t129) % 0.37/0.80 (assume @p176 @t130) % 0.37/0.80 (assume @p177 (forall @t4 (=> @t131 @t90))) % 0.37/0.80 (assume @p178 (tptp.cC16xcomp tptp.iV16453)) % 0.37/0.80 (assume @p179 @t132) % 0.37/0.80 (assume @p180 (forall @t4 (=> @t131 @t107))) % 0.37/0.80 (assume @p181 (tptp.cC94xcomp tptp.iV16453)) % 0.37/0.80 (assume @p182 @t133) % 0.37/0.80 (assume @p183 @t134) % 0.37/0.80 (assume @p184 (forall @t4 (=> @t135 @t68))) % 0.37/0.80 (assume @p185 @t136) % 0.37/0.80 (assume @p186 @t137) % 0.37/0.80 (assume @p187 (forall @t4 (=> @t135 @t105))) % 0.37/0.80 (assume @p188 (tptp.cC12xcomp tptp.iV16455)) % 0.37/0.80 (assume @p189 (forall @t4 (=> @t135 @t51))) % 0.37/0.80 (assume @p190 (tptp.cC92xcomp tptp.iV16455)) % 0.37/0.80 (assume @p191 @t138) % 0.37/0.80 (assume @p192 (forall @t4 (=> @t135 @t88))) % 0.37/0.80 (assume @p193 (tptp.cC72xcomp tptp.iV16455)) % 0.37/0.80 (assume @p194 @t139) % 0.37/0.80 (assume @p195 (forall @t4 (=> @t140 @t86))) % 0.37/0.80 (assume @p196 @t141) % 0.37/0.80 (assume @p197 (forall @t4 (=> @t140 @t48))) % 0.37/0.80 (assume @p198 @t142) % 0.37/0.80 (assume @p199 (tptp.cC52xcomp tptp.iV16457)) % 0.37/0.80 (assume @p200 (tptp.cC8xcomp tptp.iV16457)) % 0.37/0.80 (assume @p201 (forall @t4 (=> @t140 @t103))) % 0.37/0.80 (assume @p202 @t143) % 0.37/0.80 (assume @p203 (tptp.cC90xcomp tptp.iV16457)) % 0.37/0.80 (assume @p204 (forall @t4 (=> @t140 @t66))) % 0.37/0.80 (assume @p205 (tptp.cC70xcomp tptp.iV16457)) % 0.37/0.80 (assume @p206 @t144) % 0.37/0.80 (assume @p207 (tptp.cC14xcomp tptp.iV16459)) % 0.37/0.80 (assume @p208 (tptp.cC8xcomp tptp.iV16459)) % 0.37/0.80 (assume @p209 (tptp.cC10xcomp tptp.iV16459)) % 0.37/0.80 (assume @p210 @t145) % 0.37/0.80 (assume @p211 @t146) % 0.37/0.80 (assume @p212 (tptp.cC12 tptp.iV16459)) % 0.37/0.80 (assume @p213 @t147) % 0.37/0.80 (assume @p214 @t148) % 0.37/0.80 (assume @p215 (tptp.cC4 tptp.iV16459)) % 0.37/0.80 (assume @p216 @t149) % 0.37/0.80 (assume @p217 @t150) % 0.37/0.80 (assume @p218 @t151) % 0.37/0.80 (assume @p219 (tptp.cC18xcomp tptp.iV16459)) % 0.37/0.80 (assume @p220 (tptp.cC2xcomp tptp.iV16459)) % 0.37/0.80 (assume @p221 (tptp.cC6xcomp tptp.iV16459)) % 0.37/0.80 (assume @p222 @t152) % 0.37/0.80 (assume @p223 (forall @t4 (=> @t153 @t86))) % 0.37/0.80 (assume @p224 @t154) % 0.37/0.80 (assume @p225 (forall @t4 (=> @t153 @t48))) % 0.37/0.80 (assume @p226 @t155) % 0.37/0.80 (assume @p227 (tptp.cC52xcomp tptp.iV16460)) % 0.37/0.80 (assume @p228 @t156) % 0.37/0.80 (assume @p229 @t157) % 0.37/0.80 (assume @p230 (forall @t4 (=> @t153 @t66))) % 0.37/0.80 (assume @p231 (forall @t4 (=> @t153 @t103))) % 0.37/0.80 (assume @p232 (tptp.cC90xcomp tptp.iV16460)) % 0.37/0.80 (assume @p233 (tptp.cC70xcomp tptp.iV16460)) % 0.37/0.80 (assume @p234 @t158) % 0.37/0.80 (assume @p235 @t159) % 0.37/0.80 (assume @p236 (forall @t4 (=> @t160 @t105))) % 0.37/0.80 (assume @p237 (forall @t4 (=> @t160 @t88))) % 0.37/0.80 (assume @p238 @t161) % 0.37/0.80 (assume @p239 (forall @t4 (=> @t160 @t68))) % 0.37/0.80 (assume @p240 (tptp.cC92xcomp tptp.iV16461)) % 0.37/0.80 (assume @p241 @t162) % 0.37/0.80 (assume @p242 (forall @t4 (=> @t160 @t51))) % 0.37/0.80 (assume @p243 (tptp.cC72xcomp tptp.iV16461)) % 0.37/0.80 (assume @p244 (tptp.rR1 tptp.iV16461 tptp.iV16462)) % 0.37/0.80 (assume @p245 (forall @t4 (=> @t163 @t66))) % 0.37/0.80 (assume @p246 (forall @t4 (=> @t163 @t86))) % 0.37/0.80 (assume @p247 @t164) % 0.37/0.80 (assume @p248 @t165) % 0.37/0.80 (assume @p249 (tptp.cC52xcomp tptp.iV16462)) % 0.37/0.80 (assume @p250 (tptp.cC8xcomp tptp.iV16462)) % 0.37/0.80 (assume @p251 (forall @t4 (=> @t163 @t48))) % 0.37/0.80 (assume @p252 (forall @t4 (=> @t163 @t103))) % 0.37/0.80 (assume @p253 @t166) % 0.37/0.80 (assume @p254 (tptp.cC90xcomp tptp.iV16462)) % 0.37/0.80 (assume @p255 (tptp.cC70xcomp tptp.iV16462)) % 0.37/0.80 (assume @p256 @t167) % 0.37/0.80 (assume @p257 @t168) % 0.37/0.80 (assume @p258 (tptp.cC16xcomp tptp.iV16463)) % 0.37/0.80 (assume @p259 (forall @t4 (=> @t169 @t107))) % 0.37/0.80 (assume @p260 (forall @t4 (=> @t169 @t90))) % 0.37/0.80 (assume @p261 (tptp.cC94xcomp tptp.iV16463)) % 0.37/0.80 (assume @p262 @t170) % 0.37/0.80 (assume @p263 @t171) % 0.37/0.80 (assume @p264 @t172) % 0.37/0.80 (assume @p265 @t173) % 0.37/0.80 (assume @p266 (forall @t4 (=> @t174 @t51))) % 0.37/0.80 (assume @p267 @t175) % 0.37/0.80 (assume @p268 (tptp.cC12xcomp tptp.iV16464)) % 0.37/0.80 (assume @p269 (forall @t4 (=> @t174 @t68))) % 0.37/0.80 (assume @p270 (tptp.cC92xcomp tptp.iV16464)) % 0.37/0.80 (assume @p271 @t176) % 0.37/0.80 (assume @p272 (forall @t4 (=> @t174 @t105))) % 0.37/0.80 (assume @p273 (forall @t4 (=> @t174 @t88))) % 0.37/0.80 (assume @p274 (tptp.cC72xcomp tptp.iV16464)) % 0.37/0.80 (assume @p275 (tptp.rR1 tptp.iV16464 tptp.iV16465)) % 0.37/0.80 (assume @p276 (forall @t4 (=> @t177 @t48))) % 0.37/0.80 (assume @p277 @t178) % 0.37/0.80 (assume @p278 @t179) % 0.37/0.80 (assume @p279 (forall @t4 (=> @t177 @t103))) % 0.37/0.80 (assume @p280 (tptp.cC52xcomp tptp.iV16465)) % 0.37/0.80 (assume @p281 (tptp.cC8xcomp tptp.iV16465)) % 0.37/0.80 (assume @p282 (forall @t4 (=> @t177 @t86))) % 0.37/0.80 (assume @p283 @t180) % 0.37/0.80 (assume @p284 (tptp.cC90xcomp tptp.iV16465)) % 0.37/0.80 (assume @p285 (forall @t4 (=> @t177 @t66))) % 0.37/0.80 (assume @p286 (tptp.cC70xcomp tptp.iV16465)) % 0.37/0.80 (assume @p287 @t214) % 0.37/0.80 (assume @p288 true) % 0.37/0.80 (step @p289 :rule bool-and-de-morgan :args (@t14 @t74 true)) % 0.37/0.80 (step @p290 :rule cong :premises (@p289) :args (@t215)) % 0.37/0.80 (step @p291 :rule cong :premises (@p290) :args (@t216)) % 0.37/0.80 (step @p292 :rule exists-elim :args ((= @t76 @t216))) % 0.37/0.80 (step @p293 :rule trans :premises (@p292 @p291)) % 0.37/0.80 (step @p294 :rule refl :args (@t77)) % 0.37/0.80 (step @p295 :rule cong :premises (@p294 @p293) :args (@t78)) % 0.37/0.80 (step @p296 :rule cong :premises (@p295) :args (@t79)) % 0.37/0.80 (step @p297 :rule eq_resolve :premises (@p92 @p296)) % 0.37/0.80 (step @p298 :rule instantiate :premises (@p297) :args (@t217)) % 0.37/0.80 (step @p299 :rule instantiate :premises (@p93) :args (@t217)) % 0.37/0.80 (step @p300 :rule instantiate :premises (@p113) :args (@t217)) % 0.37/0.80 (step @p301 :rule instantiate :premises (@p83) :args (@t218)) % 0.37/0.80 (step @p302 :rule instantiate :premises (@p67) :args (@t218)) % 0.37/0.80 (step @p303 :rule bool-and-de-morgan :args (@t14 @t54 true)) % 0.37/0.80 (step @p304 :rule cong :premises (@p303) :args (@t219)) % 0.37/0.80 (step @p305 :rule cong :premises (@p304) :args (@t220)) % 0.37/0.80 (step @p306 :rule exists-elim :args ((= @t56 @t220))) % 0.37/0.80 (step @p307 :rule trans :premises (@p306 @p305)) % 0.37/0.80 (step @p308 :rule refl :args (@t57)) % 0.37/0.80 (step @p309 :rule cong :premises (@p308 @p307) :args (@t58)) % 0.37/0.80 (step @p310 :rule cong :premises (@p309) :args (@t59)) % 0.37/0.80 (step @p311 :rule eq_resolve :premises (@p66 @p310)) % 0.37/0.80 (step @p312 :rule instantiate :premises (@p311) :args (@t218)) % 0.37/0.80 (step @p313 :rule cnf_or_pos :args (@t223)) % 0.37/0.80 (step @p314 :rule reordering :premises (@p313) :args ((or @t222 @t221 @t224))) % 0.37/0.80 (step @p315 :rule chain_m_resolution :premises (@p314 @p194 @p228) :args (@t224 @t225 (@list @t139 @t156))) % 0.37/0.80 (assume-push @p649 @t226) % 0.37/0.80 (step @p317 :rule instantiate :premises (@p649) :args (@t227)) % 0.37/0.80 (step-pop @p650 :rule scope :premises (@p317)) % 0.37/0.80 (step @p318 :rule process_scope :premises (@p650) :args (@t223)) % 0.37/0.80 (step @p320 :rule implies_elim :premises (@p318)) % 0.37/0.80 (step @p321 :rule chain_m_resolution :premises (@p320 @p315) :args (@t228 @t229 (@list @t223))) % 0.37/0.80 (step @p322 :rule bool-double-not-elim :args (@t226)) % 0.37/0.80 (step @p323 :rule refl :args (@t198)) % 0.37/0.80 (step @p324 :rule refl :args (@t231)) % 0.37/0.80 (step @p325 :rule nary_cong :premises (@p324 @p323 @p322) :args ((or @t231 @t198 (not @t228)))) % 0.37/0.80 (step @p326 :rule cnf_equiv_pos2 :args (@t230)) % 0.37/0.80 (step @p327 :rule eq_resolve :premises (@p326 @p325)) % 0.37/0.80 (step @p328 :rule reordering :premises (@p327) :args ((or @t198 @t226 @t231))) % 0.37/0.80 (step @p329 :rule chain_m_resolution :premises (@p328 @p321 @p312) :args (@t198 @t232 (@list @t226 @t230))) % 0.37/0.80 (step @p330 :rule cnf_and_neg :args (@t233)) % 0.37/0.80 (step @p331 :rule reordering :premises (@p330) :args ((or (not @t137) @t234 @t233))) % 0.37/0.80 (step @p332 :rule chain_m_resolution :premises (@p331 @p186 @p329) :args (@t233 @t225 (@list @t137 @t198))) % 0.37/0.80 (step @p333 :rule cnf_equiv_pos2 :args (@t235)) % 0.37/0.80 (step @p334 :rule reordering :premises (@p333) :args ((or @t199 @t237 @t236))) % 0.37/0.80 (step @p335 :rule chain_m_resolution :premises (@p334 @p332 @p302) :args (@t199 @t225 (@list @t233 @t235))) % 0.37/0.80 (step @p336 :rule cnf_and_neg :args (@t238)) % 0.37/0.80 (step @p337 :rule reordering :premises (@p336) :args ((or (not @t138) @t239 @t238))) % 0.37/0.80 (step @p338 :rule chain_m_resolution :premises (@p337 @p191 @p335) :args (@t238 @t225 (@list @t138 @t199))) % 0.37/0.80 (step @p339 :rule cnf_equiv_pos2 :args (@t240)) % 0.37/0.80 (step @p340 :rule reordering :premises (@p339) :args ((or @t200 @t242 @t241))) % 0.37/0.80 (step @p341 :rule chain_m_resolution :premises (@p340 @p338 @p301) :args (@t200 @t225 (@list @t238 @t240))) % 0.37/0.80 (assume-push @p651 @t94) % 0.37/0.80 (step-pop @p652 :rule scope :premises (@p300)) % 0.37/0.80 (step @p343 :rule process_scope :premises (@p652) :args (@t244)) % 0.37/0.80 (step @p345 :rule implies_elim :premises (@p343)) % 0.37/0.80 (step @p346 :rule cnf_equiv_pos1 :args (@t244)) % 0.37/0.80 (step @p347 :rule reordering :premises (@p346) :args ((or @t246 @t243 @t245))) % 0.37/0.80 (step @p348 :rule cnf_and_pos :args (@t243 1)) % 0.37/0.80 (step @p349 :rule reordering :premises (@p348) :args ((or @t202 @t247))) % 0.37/0.80 (assume-push @p653 @t81) % 0.37/0.80 (step-pop @p654 :rule scope :premises (@p299)) % 0.37/0.80 (step @p351 :rule process_scope :premises (@p654) :args (@t249)) % 0.37/0.80 (step @p353 :rule implies_elim :premises (@p351)) % 0.37/0.80 (step @p354 :rule cnf_equiv_pos1 :args (@t249)) % 0.37/0.80 (step @p355 :rule reordering :premises (@p354) :args ((or @t251 @t248 @t250))) % 0.37/0.80 (step @p356 :rule cnf_and_pos :args (@t248 0)) % 0.37/0.80 (step @p357 :rule reordering :premises (@p356) :args ((or @t201 @t252))) % 0.37/0.80 (step @p358 :rule cnf_equiv_pos1 :args (@t240)) % 0.37/0.80 (step @p359 :rule reordering :premises (@p358) :args ((or @t253 @t238 @t241))) % 0.37/0.80 (step @p360 :rule cnf_and_pos :args (@t238 1)) % 0.37/0.80 (step @p361 :rule reordering :premises (@p360) :args ((or @t199 @t242))) % 0.37/0.80 (step @p362 :rule cnf_equiv_pos1 :args (@t235)) % 0.37/0.80 (step @p363 :rule reordering :premises (@p362) :args ((or @t239 @t233 @t236))) % 0.37/0.80 (step @p364 :rule alpha_equiv :args (@t254 @t255 (@list @t256))) % 0.37/0.80 (step @p365 :rule alpha_equiv :args (@t257 @t255 (@list @t258))) % 0.37/0.80 (step @p366 :rule nary_cong :premises (@p365 @p364) :args (@t259)) % 0.37/0.80 (step @p367 :rule quant-miniscope-and :args ((= @t5 @t259))) % 0.37/0.80 (step @p368 :rule trans :premises (@p367 @p366)) % 0.37/0.80 (step @p369 :rule eq_resolve :premises (@p1 @p368)) % 0.37/0.80 (step @p370 :rule and_elim :premises (@p369) :args (0)) % 0.37/0.80 (step @p371 :rule and_elim :premises (@p369) :args (1)) % 0.37/0.80 (step @p372 :rule instantiate :premises (@p58) :args ((@list tptp.iV16465))) % 0.37/0.80 (step @p373 :rule cnf_and_neg :args (@t260)) % 0.37/0.80 (step @p374 :rule reordering :premises (@p373) :args ((or (not @t179) (not @t180) @t260))) % 0.37/0.80 (step @p375 :rule chain_m_resolution :premises (@p374 @p278 @p283) :args (@t260 @t225 (@list @t179 @t180))) % 0.37/0.80 (step @p376 :rule cnf_equiv_pos2 :args (@t261)) % 0.37/0.80 (step @p377 :rule reordering :premises (@p376) :args ((or @t181 (not @t260) (not @t261)))) % 0.37/0.80 (step @p378 :rule chain_m_resolution :premises (@p377 @p375 @p372) :args (@t181 @t225 (@list @t260 @t261))) % 0.37/0.80 (step @p379 :rule instantiate :premises (@p83) :args (@t262)) % 0.37/0.80 (step @p380 :rule bool-impl-elim :args (@t169 @t71)) % 0.37/0.80 (step @p381 :rule cong :premises (@p380) :args (@t170)) % 0.37/0.80 (step @p382 :rule eq_resolve :premises (@p262 @p381)) % 0.37/0.80 (step @p383 :rule instantiate :premises (@p382) :args (@t262)) % 0.37/0.80 (step @p384 :rule cnf_or_pos :args (@t264)) % 0.37/0.80 (step @p385 :rule reordering :premises (@p384) :args ((or @t184 @t263 (not @t264)))) % 0.37/0.80 (step @p386 :rule chain_m_resolution :premises (@p385 @p264 @p383) :args (@t184 @t225 (@list @t172 @t264))) % 0.37/0.80 (step @p387 :rule cnf_equiv_pos1 :args (@t266)) % 0.37/0.80 (step @p388 :rule reordering :premises (@p387) :args ((or @t267 @t265 (not @t266)))) % 0.37/0.80 (step @p389 :rule chain_m_resolution :premises (@p388 @p386 @p379) :args (@t265 @t225 (@list @t184 @t266))) % 0.37/0.80 (step @p390 :rule cnf_and_pos :args (@t265 1)) % 0.37/0.80 (step @p391 :rule reordering :premises (@p390) :args ((or @t182 (not @t265)))) % 0.37/0.80 (step @p392 :rule chain_m_resolution :premises (@p391 @p389) :args (@t182 @t268 (@list @t265))) % 0.37/0.80 (step @p393 :rule instantiate :premises (@p67) :args (@t262)) % 0.37/0.80 (step @p394 :rule cnf_equiv_pos1 :args (@t270)) % 0.37/0.80 (step @p395 :rule reordering :premises (@p394) :args ((or @t271 @t269 (not @t270)))) % 0.37/0.80 (step @p396 :rule chain_m_resolution :premises (@p395 @p392 @p393) :args (@t269 @t225 (@list @t182 @t270))) % 0.37/0.80 (step @p397 :rule cnf_and_pos :args (@t269 1)) % 0.37/0.80 (step @p398 :rule reordering :premises (@p397) :args ((or @t183 (not @t269)))) % 0.37/0.80 (step @p399 :rule chain_m_resolution :premises (@p398 @p396) :args (@t183 @t268 (@list @t269))) % 0.37/0.80 (step @p400 :rule instantiate :premises (@p93) :args (@t272)) % 0.37/0.80 (step @p401 :rule instantiate :premises (@p113) :args (@t272)) % 0.37/0.80 (step @p402 :rule bool-impl-elim :args (@t120 @t93)) % 0.37/0.80 (step @p403 :rule cong :premises (@p402) :args (@t121)) % 0.37/0.80 (step @p404 :rule eq_resolve :premises (@p157 @p403)) % 0.37/0.80 (step @p405 :rule instantiate :premises (@p404) :args (@t272)) % 0.37/0.80 (step @p406 :rule cnf_or_pos :args (@t274)) % 0.37/0.80 (step @p407 :rule reordering :premises (@p406) :args ((or @t187 @t273 (not @t274)))) % 0.37/0.80 (step @p408 :rule chain_m_resolution :premises (@p407 @p160 @p405) :args (@t187 @t225 (@list @t124 @t274))) % 0.37/0.80 (step @p409 :rule cnf_equiv_pos1 :args (@t276)) % 0.37/0.80 (step @p410 :rule reordering :premises (@p409) :args ((or @t277 @t275 (not @t276)))) % 0.37/0.80 (step @p411 :rule chain_m_resolution :premises (@p410 @p408 @p401) :args (@t275 @t225 (@list @t187 @t276))) % 0.37/0.80 (step @p412 :rule cnf_and_pos :args (@t275 1)) % 0.37/0.80 (step @p413 :rule reordering :premises (@p412) :args ((or @t186 (not @t275)))) % 0.37/0.80 (step @p414 :rule chain_m_resolution :premises (@p413 @p411) :args (@t186 @t268 (@list @t275))) % 0.37/0.80 (step @p415 :rule cnf_equiv_pos1 :args (@t279)) % 0.37/0.80 (step @p416 :rule reordering :premises (@p415) :args ((or @t280 @t278 (not @t279)))) % 0.37/0.80 (step @p417 :rule chain_m_resolution :premises (@p416 @p414 @p400) :args (@t278 @t225 (@list @t186 @t279))) % 0.37/0.80 (step @p418 :rule cnf_and_pos :args (@t278 0)) % 0.37/0.80 (step @p419 :rule reordering :premises (@p418) :args ((or @t185 (not @t278)))) % 0.37/0.80 (step @p420 :rule chain_m_resolution :premises (@p419 @p417) :args (@t185 @t268 (@list @t278))) % 0.37/0.80 (step @p421 :rule instantiate :premises (@p58) :args ((@list tptp.iV16462))) % 0.37/0.80 (step @p422 :rule cnf_and_neg :args (@t281)) % 0.37/0.80 (step @p423 :rule reordering :premises (@p422) :args ((or (not @t165) (not @t166) @t281))) % 0.37/0.80 (step @p424 :rule chain_m_resolution :premises (@p423 @p248 @p253) :args (@t281 @t225 (@list @t165 @t166))) % 0.37/0.80 (step @p425 :rule cnf_equiv_pos2 :args (@t282)) % 0.37/0.80 (step @p426 :rule reordering :premises (@p425) :args ((or @t188 (not @t281) (not @t282)))) % 0.37/0.80 (step @p427 :rule chain_m_resolution :premises (@p426 @p424 @p421) :args (@t188 @t225 (@list @t281 @t282))) % 0.37/0.80 (step @p428 :rule instantiate :premises (@p83) :args (@t283)) % 0.37/0.80 (step @p429 :rule bool-impl-elim :args (@t131 @t71)) % 0.37/0.80 (step @p430 :rule cong :premises (@p429) :args (@t132)) % 0.37/0.80 (step @p431 :rule eq_resolve :premises (@p179 @p430)) % 0.37/0.80 (step @p432 :rule instantiate :premises (@p431) :args (@t283)) % 0.37/0.80 (step @p433 :rule cnf_or_pos :args (@t285)) % 0.37/0.80 (step @p434 :rule reordering :premises (@p433) :args ((or @t190 @t284 (not @t285)))) % 0.37/0.80 (step @p435 :rule chain_m_resolution :premises (@p434 @p183 @p432) :args (@t190 @t225 (@list @t134 @t285))) % 0.37/0.80 (step @p436 :rule cnf_equiv_pos1 :args (@t287)) % 0.37/0.80 (step @p437 :rule reordering :premises (@p436) :args ((or @t288 @t286 (not @t287)))) % 0.37/0.80 (step @p438 :rule chain_m_resolution :premises (@p437 @p435 @p428) :args (@t286 @t225 (@list @t190 @t287))) % 0.37/0.80 (step @p439 :rule cnf_and_pos :args (@t286 1)) % 0.37/0.80 (step @p440 :rule reordering :premises (@p439) :args ((or @t189 (not @t286)))) % 0.37/0.80 (step @p441 :rule chain_m_resolution :premises (@p440 @p438) :args (@t189 @t268 (@list @t286))) % 0.37/0.80 (step @p442 :rule instantiate :premises (@p67) :args (@t283)) % 0.37/0.80 (step @p443 :rule cnf_equiv_pos1 :args (@t290)) % 0.37/0.80 (step @p444 :rule reordering :premises (@p443) :args ((or @t291 @t289 (not @t290)))) % 0.37/0.80 (step @p445 :rule chain_m_resolution :premises (@p444 @p441 @p442) :args (@t289 @t225 (@list @t189 @t290))) % 0.37/0.80 (step @p446 :rule cnf_and_pos :args (@t289 1)) % 0.37/0.80 (step @p447 :rule reordering :premises (@p446) :args ((or @t191 (not @t289)))) % 0.37/0.80 (step @p448 :rule chain_m_resolution :premises (@p447 @p445) :args (@t191 @t268 (@list @t289))) % 0.37/0.80 (step @p449 :rule instantiate :premises (@p58) :args (@t227)) % 0.37/0.80 (step @p450 :rule cnf_and_neg :args (@t292)) % 0.37/0.80 (step @p451 :rule reordering :premises (@p450) :args ((or (not @t155) (not @t157) @t292))) % 0.37/0.80 (step @p452 :rule chain_m_resolution :premises (@p451 @p226 @p229) :args (@t292 @t225 (@list @t155 @t157))) % 0.37/0.80 (step @p453 :rule cnf_equiv_pos2 :args (@t293)) % 0.37/0.80 (step @p454 :rule reordering :premises (@p453) :args ((or @t192 (not @t292) (not @t293)))) % 0.37/0.80 (step @p455 :rule chain_m_resolution :premises (@p454 @p452 @p449) :args (@t192 @t225 (@list @t292 @t293))) % 0.37/0.80 (step @p456 :rule instantiate :premises (@p101) :args (@t294)) % 0.37/0.80 (step @p457 :rule cnf_and_neg :args (@t295)) % 0.37/0.80 (step @p458 :rule reordering :premises (@p457) :args ((or (not @t148) (not @t152) @t295))) % 0.37/0.80 (step @p459 :rule chain_m_resolution :premises (@p458 @p214 @p222) :args (@t295 @t225 (@list @t148 @t152))) % 0.37/0.80 (step @p460 :rule cnf_equiv_pos2 :args (@t296)) % 0.37/0.80 (step @p461 :rule reordering :premises (@p460) :args ((or @t193 (not @t295) (not @t296)))) % 0.37/0.80 (step @p462 :rule chain_m_resolution :premises (@p461 @p459 @p456) :args (@t193 @t225 (@list @t295 @t296))) % 0.37/0.80 (step @p463 :rule instantiate :premises (@p53) :args (@t294)) % 0.37/0.80 (step @p464 :rule cnf_and_neg :args (@t297)) % 0.37/0.80 (step @p465 :rule reordering :premises (@p464) :args ((or (not @t145) (not @t150) @t297))) % 0.37/0.80 (step @p466 :rule chain_m_resolution :premises (@p465 @p210 @p217) :args (@t297 @t225 (@list @t145 @t150))) % 0.37/0.80 (step @p467 :rule cnf_equiv_pos2 :args (@t298)) % 0.37/0.80 (step @p468 :rule reordering :premises (@p467) :args ((or @t194 (not @t297) (not @t298)))) % 0.37/0.80 (step @p469 :rule chain_m_resolution :premises (@p468 @p466 @p463) :args (@t194 @t225 (@list @t297 @t298))) % 0.37/0.80 (step @p470 :rule instantiate :premises (@p129) :args (@t294)) % 0.37/0.80 (step @p471 :rule cnf_and_neg :args (@t299)) % 0.37/0.80 (step @p472 :rule reordering :premises (@p471) :args ((or (not @t146) (not @t149) @t299))) % 0.37/0.80 (step @p473 :rule chain_m_resolution :premises (@p472 @p211 @p216) :args (@t299 @t225 (@list @t146 @t149))) % 0.37/0.80 (step @p474 :rule cnf_equiv_pos2 :args (@t300)) % 0.37/0.80 (step @p475 :rule reordering :premises (@p474) :args ((or @t195 (not @t299) (not @t300)))) % 0.37/0.80 (step @p476 :rule chain_m_resolution :premises (@p475 @p473 @p470) :args (@t195 @t225 (@list @t299 @t300))) % 0.37/0.80 (step @p477 :rule instantiate :premises (@p74) :args (@t294)) % 0.37/0.80 (step @p478 :rule cnf_and_neg :args (@t301)) % 0.37/0.80 (step @p479 :rule reordering :premises (@p478) :args ((or (not @t147) (not @t151) @t301))) % 0.37/0.80 (step @p480 :rule chain_m_resolution :premises (@p479 @p213 @p218) :args (@t301 @t225 (@list @t147 @t151))) % 0.37/0.80 (step @p481 :rule cnf_equiv_pos2 :args (@t302)) % 0.37/0.80 (step @p482 :rule reordering :premises (@p481) :args ((or @t196 (not @t301) (not @t302)))) % 0.37/0.80 (step @p483 :rule chain_m_resolution :premises (@p482 @p480 @p477) :args (@t196 @t225 (@list @t301 @t302))) % 0.37/0.80 (step @p484 :rule instantiate :premises (@p58) :args ((@list tptp.iV16457))) % 0.37/0.80 (step @p485 :rule cnf_and_neg :args (@t303)) % 0.37/0.80 (step @p486 :rule reordering :premises (@p485) :args ((or (not @t142) (not @t143) @t303))) % 0.37/0.80 (step @p487 :rule chain_m_resolution :premises (@p486 @p198 @p202) :args (@t303 @t225 (@list @t142 @t143))) % 0.37/0.80 (step @p488 :rule cnf_equiv_pos2 :args (@t304)) % 0.37/0.80 (step @p489 :rule reordering :premises (@p488) :args ((or @t197 (not @t303) (not @t304)))) % 0.37/0.80 (step @p490 :rule chain_m_resolution :premises (@p489 @p487 @p484) :args (@t197 @t225 (@list @t303 @t304))) % 0.37/0.80 (step @p491 :rule instantiate :premises (@p121) :args (@t305)) % 0.37/0.80 (step @p492 :rule instantiate :premises (@p144) :args (@t305)) % 0.37/0.80 (step @p493 :rule bool-impl-elim :args (@t113 @t112)) % 0.37/0.80 (step @p494 :rule cong :premises (@p493) :args (@t114)) % 0.37/0.80 (step @p495 :rule eq_resolve :premises (@p147 @p494)) % 0.37/0.80 (step @p496 :rule instantiate :premises (@p495) :args (@t305)) % 0.37/0.80 (step @p497 :rule cnf_or_pos :args (@t307)) % 0.37/0.80 (step @p498 :rule reordering :premises (@p497) :args ((or @t207 @t306 (not @t307)))) % 0.37/0.80 (step @p499 :rule chain_m_resolution :premises (@p498 @p151 @p496) :args (@t207 @t225 (@list @t117 @t307))) % 0.37/0.80 (step @p500 :rule cnf_equiv_pos1 :args (@t309)) % 0.37/0.80 (step @p501 :rule reordering :premises (@p500) :args ((or @t310 @t308 (not @t309)))) % 0.37/0.80 (step @p502 :rule chain_m_resolution :premises (@p501 @p499 @p492) :args (@t308 @t225 (@list @t207 @t309))) % 0.37/0.80 (step @p503 :rule cnf_and_pos :args (@t308 1)) % 0.37/0.80 (step @p504 :rule reordering :premises (@p503) :args ((or @t205 (not @t308)))) % 0.37/0.80 (step @p505 :rule chain_m_resolution :premises (@p504 @p502) :args (@t205 @t268 (@list @t308))) % 0.37/0.80 (step @p506 :rule cnf_equiv_pos1 :args (@t312)) % 0.37/0.80 (step @p507 :rule reordering :premises (@p506) :args ((or @t313 @t311 (not @t312)))) % 0.37/0.80 (step @p508 :rule chain_m_resolution :premises (@p507 @p505 @p491) :args (@t311 @t225 (@list @t205 @t312))) % 0.37/0.80 (step @p509 :rule cnf_and_pos :args (@t311 0)) % 0.37/0.80 (step @p510 :rule reordering :premises (@p509) :args ((or @t206 (not @t311)))) % 0.37/0.80 (step @p511 :rule chain_m_resolution :premises (@p510 @p508) :args (@t206 @t268 (@list @t311))) % 0.37/0.80 (step @p512 :rule bool-and-de-morgan :args (@t14 @t18 true)) % 0.37/0.80 (step @p513 :rule cong :premises (@p512) :args (@t314)) % 0.37/0.80 (step @p514 :rule cong :premises (@p513) :args (@t315)) % 0.37/0.80 (step @p515 :rule exists-elim :args ((= @t20 @t315))) % 0.37/0.80 (step @p516 :rule trans :premises (@p515 @p514)) % 0.37/0.80 (step @p517 :rule refl :args (@t21)) % 0.37/0.80 (step @p518 :rule cong :premises (@p517 @p516) :args (@t22)) % 0.37/0.80 (step @p519 :rule cong :premises (@p518) :args (@t23)) % 0.37/0.80 (step @p520 :rule eq_resolve :premises (@p11 @p519)) % 0.37/0.80 (step @p521 :rule instantiate :premises (@p520) :args (@t316)) % 0.37/0.80 (step @p522 :rule cnf_or_pos :args (@t318)) % 0.37/0.80 (step @p523 :rule reordering :premises (@p522) :args ((or @t306 @t317 @t319))) % 0.37/0.80 (step @p524 :rule chain_m_resolution :premises (@p523 @p151 @p158) :args (@t319 @t225 (@list @t117 @t122))) % 0.37/0.80 (assume-push @p655 @t320) % 0.37/0.80 (step @p526 :rule instantiate :premises (@p655) :args (@t305)) % 0.37/0.80 (step-pop @p656 :rule scope :premises (@p526)) % 0.37/0.80 (step @p527 :rule process_scope :premises (@p656) :args (@t318)) % 0.37/0.80 (step @p529 :rule implies_elim :premises (@p527)) % 0.37/0.80 (step @p530 :rule chain_m_resolution :premises (@p529 @p524) :args (@t321 @t229 (@list @t318))) % 0.37/0.80 (step @p531 :rule bool-double-not-elim :args (@t320)) % 0.37/0.80 (step @p532 :rule refl :args (@t210)) % 0.37/0.80 (step @p533 :rule refl :args (@t323)) % 0.37/0.80 (step @p534 :rule nary_cong :premises (@p533 @p532 @p531) :args ((or @t323 @t210 (not @t321)))) % 0.37/0.80 (step @p535 :rule cnf_equiv_pos2 :args (@t322)) % 0.37/0.80 (step @p536 :rule eq_resolve :premises (@p535 @p534)) % 0.37/0.80 (step @p537 :rule reordering :premises (@p536) :args ((or @t210 @t320 @t323))) % 0.37/0.80 (step @p538 :rule chain_m_resolution :premises (@p537 @p530 @p521) :args (@t210 @t232 (@list @t320 @t322))) % 0.37/0.80 (step @p539 :rule instantiate :premises (@p58) :args ((@list tptp.iV16448))) % 0.37/0.80 (step @p540 :rule cnf_and_neg :args (@t324)) % 0.37/0.80 (step @p541 :rule reordering :premises (@p540) :args ((or (not @t126) (not @t128) @t324))) % 0.37/0.80 (step @p542 :rule chain_m_resolution :premises (@p541 @p164 @p169) :args (@t324 @t225 (@list @t126 @t128))) % 0.37/0.80 (step @p543 :rule cnf_equiv_pos2 :args (@t325)) % 0.37/0.80 (step @p544 :rule reordering :premises (@p543) :args ((or @t204 (not @t324) (not @t325)))) % 0.37/0.80 (step @p545 :rule chain_m_resolution :premises (@p544 @p542 @p539) :args (@t204 @t225 (@list @t324 @t325))) % 0.37/0.80 (step @p546 :rule instantiate :premises (@p13) :args (@t316)) % 0.37/0.80 (step @p547 :rule instantiate :premises (@p146) :args (@t316)) % 0.37/0.80 (step @p548 :rule cnf_equiv_pos1 :args (@t327)) % 0.37/0.80 (step @p549 :rule reordering :premises (@p548) :args ((or (not @t116) @t326 (not @t327)))) % 0.37/0.80 (step @p550 :rule chain_m_resolution :premises (@p549 @p150 @p547) :args (@t326 @t225 (@list @t116 @t327))) % 0.37/0.80 (step @p551 :rule cnf_and_pos :args (@t326 0)) % 0.37/0.80 (step @p552 :rule reordering :premises (@p551) :args ((or @t211 @t328))) % 0.37/0.80 (step @p553 :rule chain_m_resolution :premises (@p552 @p550) :args (@t211 @t268 @t329)) % 0.37/0.80 (step @p554 :rule cnf_equiv_pos1 :args (@t331)) % 0.37/0.80 (step @p555 :rule reordering :premises (@p554) :args ((or @t332 @t330 (not @t331)))) % 0.37/0.80 (step @p556 :rule chain_m_resolution :premises (@p555 @p553 @p546) :args (@t330 @t225 (@list @t211 @t331))) % 0.37/0.80 (step @p557 :rule cnf_and_pos :args (@t330 1)) % 0.37/0.80 (step @p558 :rule reordering :premises (@p557) :args ((or @t209 @t333))) % 0.37/0.80 (step @p559 :rule chain_m_resolution :premises (@p558 @p556) :args (@t209 @t268 @t334)) % 0.37/0.80 (step @p560 :rule cnf_and_pos :args (@t330 0)) % 0.37/0.80 (step @p561 :rule reordering :premises (@p560) :args ((or @t208 @t333))) % 0.37/0.80 (step @p562 :rule chain_m_resolution :premises (@p561 @p556) :args (@t208 @t268 @t334)) % 0.37/0.80 (step @p563 :rule cnf_and_pos :args (@t326 1)) % 0.37/0.80 (step @p564 :rule reordering :premises (@p563) :args ((or @t212 @t328))) % 0.37/0.80 (step @p565 :rule chain_m_resolution :premises (@p564 @p550) :args (@t212 @t268 @t329)) % 0.37/0.80 (step @p566 :rule aci_norm :args ((= (and (and @t336 @t335) @t6 @t212 @t211 @t210 @t209 @t208 @t115 @t207 @t206 @t205 @t118 @t204 @t125 @t203 @t202 @t130 @t201 @t200 @t199 @t198 @t136 @t197 @t141 @t196 @t195 @t194 @t193 @t144 @t192 @t154 @t191 @t190 @t189 @t158 @t188 @t164 @t187 @t186 @t168 @t185 @t184 @t183 @t182 @t173 @t181 @t178) (and @t6 @t212 @t211 @t210 @t209 @t208 @t115 @t207 @t206 @t205 @t118 @t204 @t125 @t203 @t202 @t130 @t201 @t200 @t199 @t198 @t136 @t197 @t141 @t196 @t195 @t194 @t193 @t144 @t192 @t154 @t191 @t190 @t189 @t158 @t188 @t164 @t187 @t186 @t168 @t185 @t184 @t183 @t182 @t173 @t181 @t178 @t336 @t335)))) % 0.37/0.80 (step @p567 :rule refl :args (@t178)) % 0.37/0.80 (step @p568 :rule refl :args (@t181)) % 0.37/0.80 (step @p569 :rule refl :args (@t173)) % 0.37/0.80 (step @p570 :rule refl :args (@t182)) % 0.37/0.80 (step @p571 :rule refl :args (@t183)) % 0.37/0.80 (step @p572 :rule refl :args (@t184)) % 0.37/0.80 (step @p573 :rule refl :args (@t185)) % 0.37/0.80 (step @p574 :rule refl :args (@t168)) % 0.37/0.80 (step @p575 :rule refl :args (@t186)) % 0.37/0.80 (step @p576 :rule refl :args (@t187)) % 0.37/0.80 (step @p577 :rule refl :args (@t164)) % 0.37/0.80 (step @p578 :rule refl :args (@t188)) % 0.37/0.80 (step @p579 :rule refl :args (@t158)) % 0.37/0.80 (step @p580 :rule refl :args (@t189)) % 0.37/0.80 (step @p581 :rule refl :args (@t190)) % 0.37/0.80 (step @p582 :rule refl :args (@t191)) % 0.37/0.80 (step @p583 :rule refl :args (@t154)) % 0.37/0.80 (step @p584 :rule refl :args (@t192)) % 0.37/0.80 (step @p585 :rule refl :args (@t144)) % 0.37/0.80 (step @p586 :rule refl :args (@t193)) % 0.37/0.80 (step @p587 :rule refl :args (@t194)) % 0.37/0.80 (step @p588 :rule refl :args (@t195)) % 0.37/0.80 (step @p589 :rule refl :args (@t196)) % 0.37/0.80 (step @p590 :rule refl :args (@t141)) % 0.37/0.80 (step @p591 :rule refl :args (@t197)) % 0.37/0.80 (step @p592 :rule refl :args (@t136)) % 0.37/0.80 (step @p593 :rule refl :args (@t199)) % 0.37/0.80 (step @p594 :rule refl :args (@t200)) % 0.37/0.80 (step @p595 :rule refl :args (@t201)) % 0.37/0.80 (step @p596 :rule refl :args (@t130)) % 0.37/0.80 (step @p597 :rule refl :args (@t202)) % 0.37/0.80 (step @p598 :rule refl :args (@t203)) % 0.37/0.80 (step @p599 :rule refl :args (@t125)) % 0.37/0.80 (step @p600 :rule refl :args (@t204)) % 0.37/0.80 (step @p601 :rule refl :args (@t118)) % 0.37/0.80 (step @p602 :rule refl :args (@t205)) % 0.37/0.80 (step @p603 :rule refl :args (@t206)) % 0.37/0.80 (step @p604 :rule refl :args (@t207)) % 0.37/0.80 (step @p605 :rule refl :args (@t115)) % 0.37/0.80 (step @p606 :rule refl :args (@t208)) % 0.37/0.80 (step @p607 :rule refl :args (@t209)) % 0.37/0.80 (step @p608 :rule refl :args (@t211)) % 0.37/0.80 (step @p609 :rule refl :args (@t212)) % 0.37/0.80 (step @p610 :rule refl :args (@t6)) % 0.37/0.80 (step @p611 :rule nary_cong :premises (@p368 @p610 @p609 @p608 @p532 @p607 @p606 @p605 @p604 @p603 @p602 @p601 @p600 @p599 @p598 @p597 @p596 @p595 @p594 @p593 @p323 @p592 @p591 @p590 @p589 @p588 @p587 @p586 @p585 @p584 @p583 @p582 @p581 @p580 @p579 @p578 @p577 @p576 @p575 @p574 @p573 @p572 @p571 @p570 @p569 @p568 @p567) :args (@t213)) % 0.37/0.80 (step @p612 :rule trans :premises (@p611 @p566)) % 0.37/0.80 (step @p613 :rule cong :premises (@p612) :args (@t214)) % 0.37/0.80 (step @p614 :rule eq_resolve :premises (@p287 @p613)) % 0.37/0.80 (step @p615 :rule not_and :premises (@p614)) % 0.37/0.80 (step @p616 :rule reordering :premises (@p615) :args ((or (not @t336) (not @t335) (not @t6) (not @t115) (not @t118) (not @t125) (not @t130) (not @t136) (not @t141) (not @t144) (not @t154) (not @t158) (not @t164) (not @t168) (not @t173) (not @t178) (not @t212) @t332 (not @t210) (not @t209) (not @t208) @t310 (not @t206) @t313 (not @t204) @t246 @t251 @t337 @t253 @t239 @t234 (not @t197) (not @t196) (not @t195) (not @t194) (not @t193) (not @t192) (not @t191) @t288 @t291 (not @t188) @t277 @t280 (not @t185) @t267 (not @t183) @t271 (not @t181)))) % 0.37/0.80 (step @p617 :rule cnf_and_pos :args (@t233 1)) % 0.37/0.80 (step @p618 :rule reordering :premises (@p617) :args ((or @t198 @t237))) % 0.37/0.80 (step @p619 :rule chain_m_resolution :premises (@p618 @p616 @p553 @p565 @p562 @p499 @p559 @p505 @p545 @p538 @p511 @p490 @p483 @p476 @p469 @p462 @p455 @p448 @p435 @p441 @p427 @p408 @p414 @p420 @p386 @p399 @p392 @p378 @p277 @p265 @p257 @p247 @p234 @p224 @p206 @p196 @p185 @p176 @p163 @p154 @p148 @p2 @p371 @p370 @p363 @p302 @p361 @p359 @p301 @p357 @p355 @p353 @p93 @p349 @p347 @p345 @p113) :args ((or @t246 @t253) (@list 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 false false false false false false false false false false false false false false false false) (@list @t198 @t211 @t212 @t208 @t207 @t209 @t205 @t204 @t210 @t206 @t197 @t196 @t195 @t194 @t193 @t192 @t191 @t190 @t189 @t188 @t187 @t186 @t185 @t184 @t183 @t182 @t181 @t178 @t173 @t168 @t164 @t158 @t154 @t144 @t141 @t136 @t130 @t125 @t118 @t115 @t6 @t335 @t336 @t233 @t235 @t199 @t238 @t240 @t201 @t248 @t249 @t81 @t202 @t243 @t244 @t94))) % 0.37/0.80 (step @p620 :rule chain_m_resolution :premises (@p619 @p341) :args (@t246 @t268 (@list @t200))) % 0.37/0.80 (step @p621 :rule cnf_equiv_pos2 :args (@t244)) % 0.37/0.80 (step @p622 :rule reordering :premises (@p621) :args ((or @t203 @t247 @t245))) % 0.37/0.80 (step @p623 :rule chain_m_resolution :premises (@p622 @p620 @p300) :args (@t247 @t232 (@list @t203 @t244))) % 0.37/0.80 (step @p624 :rule cnf_and_neg :args (@t243)) % 0.37/0.80 (step @p625 :rule reordering :premises (@p624) :args ((or (not @t129) @t251 @t243))) % 0.37/0.80 (step @p626 :rule chain_m_resolution :premises (@p625 @p175 @p623) :args (@t251 @t338 (@list @t129 @t243))) % 0.37/0.80 (step @p627 :rule cnf_equiv_pos2 :args (@t249)) % 0.37/0.80 (step @p628 :rule reordering :premises (@p627) :args ((or @t202 @t252 @t250))) % 0.37/0.80 (step @p629 :rule chain_m_resolution :premises (@p628 @p626 @p299) :args (@t252 @t232 (@list @t202 @t249))) % 0.37/0.80 (step @p630 :rule cnf_and_neg :args (@t248)) % 0.37/0.80 (step @p631 :rule reordering :premises (@p630) :args ((or (not @t133) @t337 @t248))) % 0.37/0.80 (step @p632 :rule chain_m_resolution :premises (@p631 @p182 @p629) :args (@t337 @t338 (@list @t133 @t248))) % 0.37/0.80 (step @p633 :rule bool-double-not-elim :args (@t339)) % 0.37/0.80 (step @p634 :rule refl :args (@t342)) % 0.37/0.80 (step @p635 :rule nary_cong :premises (@p634 @p595 @p633) :args ((or @t342 @t201 (not @t340)))) % 0.37/0.80 (step @p636 :rule cnf_equiv_pos2 :args (@t341)) % 0.37/0.80 (step @p637 :rule eq_resolve :premises (@p636 @p635)) % 0.37/0.80 (step @p638 :rule reordering :premises (@p637) :args ((or @t201 @t339 @t342))) % 0.37/0.80 (step @p639 :rule chain_m_resolution :premises (@p638 @p632 @p298) :args (@t339 @t232 (@list @t201 @t341))) % 0.37/0.80 (step @p640 :rule cnf_or_pos :args (@t344)) % 0.37/0.80 (step @p641 :rule reordering :premises (@p640) :args ((or @t284 @t343 @t345))) % 0.37/0.80 (step @p642 :rule chain_m_resolution :premises (@p641 @p183 @p238) :args (@t345 @t225 (@list @t134 @t161))) % 0.37/0.80 (assume-push @p657 @t339) % 0.37/0.80 (step @p644 :rule instantiate :premises (@p657) :args (@t283)) % 0.37/0.80 (step-pop @p658 :rule scope :premises (@p644)) % 0.37/0.80 (step @p645 :rule process_scope :premises (@p658) :args (@t344)) % 0.37/0.80 (step @p647 :rule implies_elim :premises (@p645)) % 0.37/0.80 (step @p648 false :rule chain_m_resolution :premises (@p647 @p642 @p639) :args (false @t232 (@list @t344 @t339))) % 0.37/0.80 ) % 0.37/0.80 % SZS output end Proof % 0.37/0.80 % cvc5 exiting %------------------------------------------------------------------------------