%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : KRS159+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 : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:29:02 AM UTC 2026 % Result : Theorem 0.40s 0.91s % Output : Proof 0.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : KRS159+1 : TPTP v9.2.1. Released v3.1.0. % 0.08/0.15 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.19/0.36 % Computer : n007.cluster.edu % 0.19/0.36 % Model : x86_64 x86_64 % 0.19/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.19/0.36 % Memory : 8042.1875MB % 0.19/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.19/0.36 % CPULimit : 300 % 0.19/0.36 % WCLimit : 300 % 0.19/0.36 % DateTime : Tue Jun 2 05:27:41 EDT 2026 % 0.19/0.36 % CPUTime : % 0.37/0.56 %----Proving TF0_NAR, FOF, or CNF % 0.40/0.91 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.40/0.91 % SZS status Theorem % 0.40/0.91 % SZS output start Proof % 0.40/0.91 ( % 0.40/0.91 (declare-sort $$unsorted 0) % 0.40/0.91 (declare-const tptp.iV21031 $$unsorted) % 0.40/0.91 (declare-const tptp.iV21034 $$unsorted) % 0.40/0.91 (declare-const tptp.iV21036 $$unsorted) % 0.40/0.91 (declare-const tptp.iV21028 $$unsorted) % 0.40/0.91 (declare-const tptp.iV21027 $$unsorted) % 0.40/0.91 (declare-const tptp.iV21026 $$unsorted) % 0.40/0.91 (declare-const tptp.ra_Px35 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px86 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC96 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC94xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px28 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC88 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC84 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC78 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC76 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC74xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC70xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC70 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC68xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC66xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px21 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC64 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC60 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC56 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC54xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px18 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC54 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC52 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px89 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC50xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC48xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px29 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px17 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC46xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px90 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC44xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC82 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC44 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px13 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC80 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC42 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC40 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC38 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC36 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC34xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC34 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.iV21033 $$unsorted) % 0.40/0.91 (declare-const tptp.ra_Px10 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC32xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC32 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px91 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC172xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC134 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC130 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px26 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC124 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC122xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px43 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC86 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC128 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC110 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC168 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC120xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC120 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC98 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px47 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px84 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px24 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px80 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC176xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC126 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC12xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC30 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC136 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC10 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC50 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC14 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px39 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC118 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC92xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC94 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC48 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC132 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC150xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC106 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px42 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC118xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC4 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px33 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px25 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC158 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px34 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC138 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC8 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC154 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC124xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC58 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px3 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px1 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC174 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC28xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC100xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px85 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.xsd_integer (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC98xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC102 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px83 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC62 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC108 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC126xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC166xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cowlNothing (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC114 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.rR1 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC46 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px44 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC112 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px87 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC122 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC104 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC102xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC18 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC106xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC92 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC128xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC18xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px36 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC166 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC96xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC140 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px16 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px77 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.iV21030 $$unsorted) % 0.40/0.91 (declare-const tptp.cC66 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC24xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.xsd_string (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC68 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC116 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC170xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC52xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC142 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px55 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC142xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC144 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC162xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px51 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC104xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC144xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC6 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC146 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC146xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px81 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cTOP (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC148xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.iV21029 $$unsorted) % 0.40/0.91 (declare-const tptp.cC90 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC150 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC152 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC156 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.iV21035 $$unsorted) % 0.40/0.91 (declare-const tptp.cC12 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC22 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC16 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cowlThing (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px8 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC72xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC160xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px60 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC74 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC162 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC164 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px79 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC76xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC164xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC2 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.iV21032 $$unsorted) % 0.40/0.91 (declare-const tptp.ra_Px56 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px78 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC170 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px58 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC172 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px88 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC26xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC100 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC176 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC140xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC178 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cTEST (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC6xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px82 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC178xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px2 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC180 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px27 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px50 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC2xcomp (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC20 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC148 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px5 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC24 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px92 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px52 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC26 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC28 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.ra_Px9 (-> $$unsorted $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC72 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC160 (-> $$unsorted Bool)) % 0.40/0.91 (declare-const tptp.cC30xcomp (-> $$unsorted Bool)) % 0.40/0.91 (define @t1 () (@var "X" $$unsorted)) % 0.40/0.91 (define @t2 () (not (tptp.cowlNothing @t1))) % 0.40/0.91 (define @t3 () (tptp.cowlThing @t1)) % 0.40/0.91 (define @t4 () (@list @t1)) % 0.40/0.91 (define @t5 () (forall @t4 (and @t3 @t2))) % 0.40/0.91 (define @t6 () (forall @t4 (= (tptp.xsd_string @t1) (not (tptp.xsd_integer @t1))))) % 0.40/0.91 (define @t7 () (tptp.cC4 @t1)) % 0.40/0.91 (define @t8 () (tptp.cC8 @t1)) % 0.40/0.91 (define @t9 () (tptp.cC10 @t1)) % 0.40/0.91 (define @t10 () (@var "Y0" $$unsorted)) % 0.40/0.91 (define @t11 () (@list @t10)) % 0.40/0.91 (define @t12 () (tptp.cC100 @t1)) % 0.40/0.91 (define @t13 () (@var "Y" $$unsorted)) % 0.40/0.91 (define @t14 () (@list @t13)) % 0.40/0.91 (define @t15 () (tptp.cC100xcomp @t1)) % 0.40/0.91 (define @t16 () (tptp.cC102 @t1)) % 0.40/0.91 (define @t17 () (tptp.rR1 @t1 @t13)) % 0.40/0.91 (define @t18 () (exists @t14 (and @t17 (tptp.cC6xcomp @t13)))) % 0.40/0.91 (define @t19 () (tptp.cC102xcomp @t1)) % 0.40/0.91 (define @t20 () (tptp.cC104 @t1)) % 0.40/0.91 (define @t21 () (tptp.cC104xcomp @t1)) % 0.40/0.91 (define @t22 () (tptp.cC106 @t1)) % 0.40/0.91 (define @t23 () (tptp.cC106xcomp @t1)) % 0.40/0.91 (define @t24 () (tptp.cC98xcomp @t1)) % 0.40/0.91 (define @t25 () (tptp.cC108 @t1)) % 0.40/0.91 (define @t26 () (tptp.cTOP @t1)) % 0.40/0.91 (define @t27 () (tptp.cC110 @t1)) % 0.40/0.91 (define @t28 () (tptp.cC90 @t1)) % 0.40/0.91 (define @t29 () (tptp.cC112 @t1)) % 0.40/0.91 (define @t30 () (tptp.cC114 @t1)) % 0.40/0.91 (define @t31 () (forall @t4 (= @t30 @t26))) % 0.40/0.91 (define @t32 () (tptp.cC116 @t1)) % 0.40/0.91 (define @t33 () (exists @t14 (and @t17 (tptp.cC92xcomp @t13)))) % 0.40/0.91 (define @t34 () (tptp.cC118 @t1)) % 0.40/0.91 (define @t35 () (tptp.cC118xcomp @t1)) % 0.40/0.91 (define @t36 () (tptp.cC12xcomp @t1)) % 0.40/0.91 (define @t37 () (tptp.cC120 @t1)) % 0.40/0.91 (define @t38 () (tptp.cC92xcomp @t1)) % 0.40/0.91 (define @t39 () (tptp.cC120xcomp @t1)) % 0.40/0.91 (define @t40 () (tptp.cC122 @t1)) % 0.40/0.91 (define @t41 () (tptp.cC122xcomp @t1)) % 0.40/0.91 (define @t42 () (tptp.cC124 @t1)) % 0.40/0.91 (define @t43 () (tptp.cC124xcomp @t1)) % 0.40/0.91 (define @t44 () (tptp.cC126 @t1)) % 0.40/0.91 (define @t45 () (tptp.cC126xcomp @t1)) % 0.40/0.91 (define @t46 () (tptp.cC128 @t1)) % 0.40/0.91 (define @t47 () (tptp.cC128xcomp @t1)) % 0.40/0.91 (define @t48 () (tptp.cC130 @t1)) % 0.40/0.91 (define @t49 () (tptp.cC132 @t1)) % 0.40/0.91 (define @t50 () (tptp.cC134 @t1)) % 0.40/0.91 (define @t51 () (tptp.cC136 @t1)) % 0.40/0.91 (define @t52 () (forall @t4 (= @t51 @t26))) % 0.40/0.91 (define @t53 () (tptp.cC138 @t1)) % 0.40/0.91 (define @t54 () (tptp.cC12xcomp @t13)) % 0.40/0.91 (define @t55 () (and @t17 @t54)) % 0.40/0.91 (define @t56 () (exists @t14 @t55)) % 0.40/0.91 (define @t57 () (tptp.cC14 @t1)) % 0.40/0.91 (define @t58 () (exists @t14 (and @t17 (tptp.cC100xcomp @t13)))) % 0.40/0.91 (define @t59 () (tptp.cC140 @t1)) % 0.40/0.91 (define @t60 () (tptp.cC140xcomp @t1)) % 0.40/0.91 (define @t61 () (tptp.cC142 @t1)) % 0.40/0.91 (define @t62 () (tptp.cC142xcomp @t1)) % 0.40/0.91 (define @t63 () (tptp.cC144 @t1)) % 0.40/0.91 (define @t64 () (tptp.cC144xcomp @t1)) % 0.40/0.91 (define @t65 () (tptp.cC146 @t1)) % 0.40/0.91 (define @t66 () (tptp.cC146xcomp @t1)) % 0.40/0.91 (define @t67 () (tptp.cC148 @t1)) % 0.40/0.91 (define @t68 () (tptp.cC148xcomp @t1)) % 0.40/0.91 (define @t69 () (tptp.cC150 @t1)) % 0.40/0.91 (define @t70 () (tptp.cC150xcomp @t1)) % 0.40/0.91 (define @t71 () (tptp.cC152 @t1)) % 0.40/0.91 (define @t72 () (tptp.cC154 @t1)) % 0.40/0.91 (define @t73 () (tptp.cC156 @t1)) % 0.40/0.91 (define @t74 () (tptp.cC22 @t1)) % 0.40/0.91 (define @t75 () (tptp.cC158 @t1)) % 0.40/0.91 (define @t76 () (tptp.cC16 @t1)) % 0.40/0.91 (define @t77 () (tptp.cC160 @t1)) % 0.40/0.91 (define @t78 () (tptp.cC160xcomp @t1)) % 0.40/0.91 (define @t79 () (tptp.cC162 @t1)) % 0.40/0.91 (define @t80 () (tptp.cC162xcomp @t1)) % 0.40/0.91 (define @t81 () (tptp.cC164 @t1)) % 0.40/0.91 (define @t82 () (tptp.cC164xcomp @t1)) % 0.40/0.91 (define @t83 () (tptp.cC166 @t1)) % 0.40/0.91 (define @t84 () (tptp.cC166xcomp @t1)) % 0.40/0.91 (define @t85 () (tptp.cC168 @t1)) % 0.40/0.91 (define @t86 () (tptp.cC170 @t1)) % 0.40/0.91 (define @t87 () (exists @t14 (and @t17 (tptp.cC18xcomp @t13)))) % 0.40/0.91 (define @t88 () (tptp.cC170xcomp @t1)) % 0.40/0.91 (define @t89 () (tptp.cC172 @t1)) % 0.40/0.91 (define @t90 () (tptp.cC172xcomp @t1)) % 0.40/0.91 (define @t91 () (tptp.cC174 @t1)) % 0.40/0.91 (define @t92 () (tptp.cC176 @t1)) % 0.40/0.91 (define @t93 () (tptp.cC176xcomp @t1)) % 0.40/0.91 (define @t94 () (tptp.cC178 @t1)) % 0.40/0.91 (define @t95 () (tptp.cC178xcomp @t1)) % 0.40/0.91 (define @t96 () (tptp.cC18 @t1)) % 0.40/0.91 (define @t97 () (tptp.cC18xcomp @t1)) % 0.40/0.91 (define @t98 () (tptp.cC180 @t1)) % 0.40/0.91 (define @t99 () (tptp.cC2xcomp @t1)) % 0.40/0.91 (define @t100 () (tptp.cC20 @t1)) % 0.40/0.91 (define @t101 () (tptp.ra_Px5 @t1 @t10)) % 0.40/0.91 (define @t102 () (exists @t11 @t101)) % 0.40/0.91 (define @t103 () (tptp.cC24 @t1)) % 0.40/0.91 (define @t104 () (= @t103 @t102)) % 0.40/0.91 (define @t105 () (forall @t4 @t104)) % 0.40/0.91 (define @t106 () (tptp.cC2xcomp @t13)) % 0.40/0.91 (define @t107 () (and @t17 @t106)) % 0.40/0.91 (define @t108 () (exists @t14 @t107)) % 0.40/0.91 (define @t109 () (tptp.ra_Px5 @t1 @t13)) % 0.40/0.91 (define @t110 () (exists @t14 @t109)) % 0.40/0.91 (define @t111 () (not @t110)) % 0.40/0.91 (define @t112 () (tptp.cC24xcomp @t1)) % 0.40/0.91 (define @t113 () (= @t112 @t111)) % 0.40/0.91 (define @t114 () (forall @t4 @t113)) % 0.40/0.91 (define @t115 () (tptp.ra_Px92 @t1 @t10)) % 0.40/0.91 (define @t116 () (exists @t11 @t115)) % 0.40/0.91 (define @t117 () (tptp.cC26 @t1)) % 0.40/0.91 (define @t118 () (= @t117 @t116)) % 0.40/0.91 (define @t119 () (forall @t4 @t118)) % 0.40/0.91 (define @t120 () (tptp.ra_Px92 @t1 @t13)) % 0.40/0.91 (define @t121 () (exists @t14 @t120)) % 0.40/0.91 (define @t122 () (not @t121)) % 0.40/0.91 (define @t123 () (tptp.cC26xcomp @t1)) % 0.40/0.91 (define @t124 () (= @t123 @t122)) % 0.40/0.91 (define @t125 () (forall @t4 @t124)) % 0.40/0.91 (define @t126 () (tptp.cC28 @t1)) % 0.40/0.91 (define @t127 () (tptp.cC28xcomp @t1)) % 0.40/0.91 (define @t128 () (tptp.ra_Px8 @t1 @t10)) % 0.40/0.91 (define @t129 () (exists @t11 @t128)) % 0.40/0.91 (define @t130 () (tptp.cC30 @t1)) % 0.40/0.91 (define @t131 () (= @t130 @t129)) % 0.40/0.91 (define @t132 () (forall @t4 @t131)) % 0.40/0.91 (define @t133 () (tptp.ra_Px8 @t1 @t13)) % 0.40/0.91 (define @t134 () (exists @t14 @t133)) % 0.40/0.91 (define @t135 () (not @t134)) % 0.40/0.91 (define @t136 () (tptp.cC30xcomp @t1)) % 0.40/0.91 (define @t137 () (= @t136 @t135)) % 0.40/0.91 (define @t138 () (forall @t4 @t137)) % 0.40/0.91 (define @t139 () (tptp.ra_Px91 @t1 @t13)) % 0.40/0.91 (define @t140 () (exists @t14 @t139)) % 0.40/0.91 (define @t141 () (not @t140)) % 0.40/0.91 (define @t142 () (tptp.cC32 @t1)) % 0.40/0.91 (define @t143 () (= @t142 @t141)) % 0.40/0.91 (define @t144 () (forall @t4 @t143)) % 0.40/0.91 (define @t145 () (tptp.ra_Px91 @t1 @t10)) % 0.40/0.91 (define @t146 () (exists @t11 @t145)) % 0.40/0.91 (define @t147 () (tptp.cC32xcomp @t1)) % 0.40/0.91 (define @t148 () (= @t147 @t146)) % 0.40/0.91 (define @t149 () (forall @t4 @t148)) % 0.40/0.91 (define @t150 () (tptp.cC34 @t1)) % 0.40/0.91 (define @t151 () (tptp.cC34xcomp @t1)) % 0.40/0.91 (define @t152 () (tptp.cC36 @t1)) % 0.40/0.91 (define @t153 () (tptp.cC38 @t1)) % 0.40/0.91 (define @t154 () (= @t7 @t108)) % 0.40/0.91 (define @t155 () (forall @t4 @t154)) % 0.40/0.91 (define @t156 () (tptp.cC40 @t1)) % 0.40/0.91 (define @t157 () (forall @t4 (= @t156 @t26))) % 0.40/0.91 (define @t158 () (tptp.cC42 @t1)) % 0.40/0.91 (define @t159 () (tptp.ra_Px13 @t1 @t13)) % 0.40/0.91 (define @t160 () (exists @t14 @t159)) % 0.40/0.91 (define @t161 () (not @t160)) % 0.40/0.91 (define @t162 () (tptp.cC44 @t1)) % 0.40/0.91 (define @t163 () (= @t162 @t161)) % 0.40/0.91 (define @t164 () (forall @t4 @t163)) % 0.40/0.91 (define @t165 () (tptp.ra_Px13 @t1 @t10)) % 0.40/0.91 (define @t166 () (exists @t11 @t165)) % 0.40/0.91 (define @t167 () (tptp.cC44xcomp @t1)) % 0.40/0.91 (define @t168 () (= @t167 @t166)) % 0.40/0.91 (define @t169 () (forall @t4 @t168)) % 0.40/0.91 (define @t170 () (tptp.ra_Px90 @t1 @t10)) % 0.40/0.91 (define @t171 () (exists @t11 @t170)) % 0.40/0.91 (define @t172 () (tptp.cC46 @t1)) % 0.40/0.91 (define @t173 () (= @t172 @t171)) % 0.40/0.91 (define @t174 () (forall @t4 @t173)) % 0.40/0.91 (define @t175 () (tptp.ra_Px90 @t1 @t13)) % 0.40/0.91 (define @t176 () (exists @t14 @t175)) % 0.40/0.91 (define @t177 () (not @t176)) % 0.40/0.91 (define @t178 () (tptp.cC46xcomp @t1)) % 0.40/0.91 (define @t179 () (= @t178 @t177)) % 0.40/0.91 (define @t180 () (forall @t4 @t179)) % 0.40/0.91 (define @t181 () (tptp.cC48 @t1)) % 0.40/0.91 (define @t182 () (tptp.cC48xcomp @t1)) % 0.40/0.91 (define @t183 () (tptp.cC50 @t1)) % 0.40/0.91 (define @t184 () (forall @t4 (= @t183 @t56))) % 0.40/0.91 (define @t185 () (tptp.cC50xcomp @t1)) % 0.40/0.91 (define @t186 () (tptp.cC52 @t1)) % 0.40/0.91 (define @t187 () (tptp.cC52xcomp @t1)) % 0.40/0.91 (define @t188 () (tptp.cC54 @t1)) % 0.40/0.91 (define @t189 () (tptp.cC54xcomp @t1)) % 0.40/0.91 (define @t190 () (tptp.cC56 @t1)) % 0.40/0.91 (define @t191 () (tptp.cC58 @t1)) % 0.40/0.91 (define @t192 () (tptp.cC6 @t1)) % 0.40/0.91 (define @t193 () (tptp.cC60 @t1)) % 0.40/0.91 (define @t194 () (tptp.cC62 @t1)) % 0.40/0.91 (define @t195 () (forall @t4 (= @t194 @t26))) % 0.40/0.91 (define @t196 () (tptp.cC64 @t1)) % 0.40/0.91 (define @t197 () (tptp.ra_Px21 @t1 @t10)) % 0.40/0.91 (define @t198 () (exists @t11 @t197)) % 0.40/0.91 (define @t199 () (tptp.cC66 @t1)) % 0.40/0.91 (define @t200 () (= @t199 @t198)) % 0.40/0.91 (define @t201 () (forall @t4 @t200)) % 0.40/0.91 (define @t202 () (tptp.ra_Px21 @t1 @t13)) % 0.40/0.91 (define @t203 () (exists @t14 @t202)) % 0.40/0.91 (define @t204 () (not @t203)) % 0.40/0.91 (define @t205 () (tptp.cC66xcomp @t1)) % 0.40/0.91 (define @t206 () (= @t205 @t204)) % 0.40/0.91 (define @t207 () (forall @t4 @t206)) % 0.40/0.91 (define @t208 () (tptp.ra_Px88 @t1 @t13)) % 0.40/0.91 (define @t209 () (exists @t14 @t208)) % 0.40/0.91 (define @t210 () (not @t209)) % 0.40/0.91 (define @t211 () (tptp.cC68 @t1)) % 0.40/0.91 (define @t212 () (= @t211 @t210)) % 0.40/0.91 (define @t213 () (forall @t4 @t212)) % 0.40/0.91 (define @t214 () (tptp.ra_Px88 @t1 @t10)) % 0.40/0.91 (define @t215 () (exists @t11 @t214)) % 0.40/0.91 (define @t216 () (tptp.cC68xcomp @t1)) % 0.40/0.91 (define @t217 () (= @t216 @t215)) % 0.40/0.91 (define @t218 () (forall @t4 @t217)) % 0.40/0.91 (define @t219 () (tptp.cC70 @t1)) % 0.40/0.91 (define @t220 () (tptp.cC70xcomp @t1)) % 0.40/0.91 (define @t221 () (tptp.ra_Px24 @t1 @t10)) % 0.40/0.91 (define @t222 () (exists @t11 @t221)) % 0.40/0.91 (define @t223 () (tptp.cC72 @t1)) % 0.40/0.91 (define @t224 () (= @t223 @t222)) % 0.40/0.91 (define @t225 () (forall @t4 @t224)) % 0.40/0.91 (define @t226 () (tptp.ra_Px24 @t1 @t13)) % 0.40/0.91 (define @t227 () (exists @t14 @t226)) % 0.40/0.91 (define @t228 () (not @t227)) % 0.40/0.91 (define @t229 () (tptp.cC72xcomp @t1)) % 0.40/0.91 (define @t230 () (= @t229 @t228)) % 0.40/0.91 (define @t231 () (forall @t4 @t230)) % 0.40/0.91 (define @t232 () (tptp.cC74 @t1)) % 0.40/0.91 (define @t233 () (tptp.ra_Px87 @t1 @t10)) % 0.40/0.91 (define @t234 () (exists @t11 @t233)) % 0.40/0.91 (define @t235 () (= @t232 @t234)) % 0.40/0.91 (define @t236 () (forall @t4 @t235)) % 0.40/0.91 (define @t237 () (tptp.ra_Px87 @t1 @t13)) % 0.40/0.91 (define @t238 () (exists @t14 @t237)) % 0.40/0.91 (define @t239 () (not @t238)) % 0.40/0.91 (define @t240 () (tptp.cC74xcomp @t1)) % 0.40/0.91 (define @t241 () (= @t240 @t239)) % 0.40/0.91 (define @t242 () (forall @t4 @t241)) % 0.40/0.91 (define @t243 () (tptp.cC76 @t1)) % 0.40/0.91 (define @t244 () (tptp.cC76xcomp @t1)) % 0.40/0.91 (define @t245 () (tptp.cC78 @t1)) % 0.40/0.91 (define @t246 () (tptp.cC80 @t1)) % 0.40/0.91 (define @t247 () (tptp.cC82 @t1)) % 0.40/0.91 (define @t248 () (tptp.cC84 @t1)) % 0.40/0.91 (define @t249 () (forall @t4 (= @t248 @t26))) % 0.40/0.91 (define @t250 () (tptp.cC86 @t1)) % 0.40/0.91 (define @t251 () (tptp.cC88 @t1)) % 0.40/0.91 (define @t252 () (forall @t4 (= @t251 @t26))) % 0.40/0.91 (define @t253 () (tptp.cC92 @t1)) % 0.40/0.91 (define @t254 () (tptp.cC94 @t1)) % 0.40/0.91 (define @t255 () (tptp.cC94xcomp @t1)) % 0.40/0.91 (define @t256 () (tptp.cC96 @t1)) % 0.40/0.91 (define @t257 () (tptp.cC96xcomp @t1)) % 0.40/0.91 (define @t258 () (tptp.cC98 @t1)) % 0.40/0.91 (define @t259 () (tptp.cC150xcomp tptp.iV21026)) % 0.40/0.91 (define @t260 () (tptp.rR1 tptp.iV21026 @t1)) % 0.40/0.91 (define @t261 () (tptp.cTOP tptp.iV21026)) % 0.40/0.91 (define @t262 () (tptp.cC76xcomp tptp.iV21026)) % 0.40/0.91 (define @t263 () (tptp.cC98xcomp tptp.iV21026)) % 0.40/0.91 (define @t264 () (tptp.cC128xcomp tptp.iV21026)) % 0.40/0.91 (define @t265 () (tptp.cC166xcomp tptp.iV21026)) % 0.40/0.91 (define @t266 () (tptp.cC106xcomp tptp.iV21026)) % 0.40/0.91 (define @t267 () (tptp.cC34xcomp tptp.iV21026)) % 0.40/0.91 (define @t268 () (tptp.cC144xcomp tptp.iV21026)) % 0.40/0.91 (define @t269 () (tptp.cC28xcomp tptp.iV21026)) % 0.40/0.91 (define @t270 () (tptp.cC54xcomp tptp.iV21026)) % 0.40/0.91 (define @t271 () (tptp.cC122xcomp tptp.iV21026)) % 0.40/0.91 (define @t272 () (tptp.cC162xcomp tptp.iV21026)) % 0.40/0.91 (define @t273 () (tptp.cC70xcomp tptp.iV21026)) % 0.40/0.91 (define @t274 () (tptp.cC172xcomp tptp.iV21026)) % 0.40/0.91 (define @t275 () (tptp.cC48xcomp tptp.iV21026)) % 0.40/0.91 (define @t276 () (tptp.cowlThing tptp.iV21026)) % 0.40/0.91 (define @t277 () (tptp.cTEST tptp.iV21026)) % 0.40/0.91 (define @t278 () (tptp.rR1 tptp.iV21026 tptp.iV21027)) % 0.40/0.91 (define @t279 () (tptp.rR1 tptp.iV21027 @t1)) % 0.40/0.91 (define @t280 () (tptp.cC2xcomp tptp.iV21027)) % 0.40/0.91 (define @t281 () (tptp.cC26xcomp tptp.iV21027)) % 0.40/0.91 (define @t282 () (tptp.cowlThing tptp.iV21027)) % 0.40/0.91 (define @t283 () (tptp.cC32xcomp tptp.iV21027)) % 0.40/0.91 (define @t284 () (tptp.rR1 tptp.iV21029 @t1)) % 0.40/0.91 (define @t285 () (tptp.cC12xcomp tptp.iV21029)) % 0.40/0.91 (define @t286 () (tptp.cC46xcomp tptp.iV21029)) % 0.40/0.91 (define @t287 () (tptp.cowlThing tptp.iV21029)) % 0.40/0.91 (define @t288 () (tptp.rR1 tptp.iV21029 tptp.iV21033)) % 0.40/0.91 (define @t289 () (tptp.cC68xcomp tptp.iV21030)) % 0.40/0.91 (define @t290 () (tptp.rR1 tptp.iV21030 @t1)) % 0.40/0.91 (define @t291 () (tptp.cC18xcomp tptp.iV21030)) % 0.40/0.91 (define @t292 () (tptp.cowlThing tptp.iV21030)) % 0.40/0.91 (define @t293 () (tptp.cC74xcomp tptp.iV21030)) % 0.40/0.91 (define @t294 () (tptp.cC12xcomp tptp.iV21033)) % 0.40/0.91 (define @t295 () (tptp.cC66 tptp.iV21030)) % 0.40/0.91 (define @t296 () (tptp.cC72 tptp.iV21030)) % 0.40/0.91 (define @t297 () (tptp.cC44 tptp.iV21029)) % 0.40/0.91 (define @t298 () (tptp.cC50 tptp.iV21029)) % 0.40/0.91 (define @t299 () (tptp.cC24 tptp.iV21027)) % 0.40/0.91 (define @t300 () (tptp.cC30 tptp.iV21027)) % 0.40/0.91 (define @t301 () (tptp.cC86 tptp.iV21026)) % 0.40/0.91 (define @t302 () (tptp.cC156 tptp.iV21026)) % 0.40/0.91 (define @t303 () (tptp.cC42 tptp.iV21026)) % 0.40/0.91 (define @t304 () (tptp.cC134 tptp.iV21026)) % 0.40/0.91 (define @t305 () (tptp.cC4 tptp.iV21026)) % 0.40/0.91 (define @t306 () (tptp.cC168 tptp.iV21026)) % 0.40/0.91 (define @t307 () (tptp.cC130 tptp.iV21026)) % 0.40/0.91 (define @t308 () (tptp.cC88 tptp.iV21026)) % 0.40/0.91 (define @t309 () (tptp.cC80 tptp.iV21026)) % 0.40/0.91 (define @t310 () (tptp.cC152 tptp.iV21026)) % 0.40/0.91 (define @t311 () (tptp.cC14 tptp.iV21026)) % 0.40/0.91 (define @t312 () (tptp.cC82 tptp.iV21026)) % 0.40/0.91 (define @t313 () (tptp.cC116 tptp.iV21026)) % 0.40/0.91 (define @t314 () (tptp.cC64 tptp.iV21026)) % 0.40/0.91 (define @t315 () (tptp.cC112 tptp.iV21026)) % 0.40/0.91 (define @t316 () (tptp.cC36 tptp.iV21026)) % 0.40/0.91 (define @t317 () (tptp.cC8 tptp.iV21026)) % 0.40/0.91 (define @t318 () (tptp.cC62 tptp.iV21026)) % 0.40/0.91 (define @t319 () (tptp.cC174 tptp.iV21026)) % 0.40/0.91 (define @t320 () (tptp.cC138 tptp.iV21026)) % 0.40/0.91 (define @t321 () (tptp.cC38 tptp.iV21026)) % 0.40/0.91 (define @t322 () (tptp.cC84 tptp.iV21026)) % 0.40/0.91 (define @t323 () (tptp.cC20 tptp.iV21026)) % 0.40/0.91 (define @t324 () (tptp.cC114 tptp.iV21026)) % 0.40/0.91 (define @t325 () (tptp.cC132 tptp.iV21026)) % 0.40/0.91 (define @t326 () (tptp.cC16 tptp.iV21026)) % 0.40/0.91 (define @t327 () (tptp.cC78 tptp.iV21026)) % 0.40/0.91 (define @t328 () (tptp.cC180 tptp.iV21026)) % 0.40/0.91 (define @t329 () (tptp.cC154 tptp.iV21026)) % 0.40/0.91 (define @t330 () (tptp.cC60 tptp.iV21026)) % 0.40/0.91 (define @t331 () (tptp.cC22 tptp.iV21026)) % 0.40/0.91 (define @t332 () (tptp.cC110 tptp.iV21026)) % 0.40/0.91 (define @t333 () (tptp.cC158 tptp.iV21026)) % 0.40/0.91 (define @t334 () (tptp.cC56 tptp.iV21026)) % 0.40/0.91 (define @t335 () (tptp.cC58 tptp.iV21026)) % 0.40/0.91 (define @t336 () (tptp.cC90 tptp.iV21026)) % 0.40/0.91 (define @t337 () (tptp.cC10 tptp.iV21026)) % 0.40/0.91 (define @t338 () (tptp.cC136 tptp.iV21026)) % 0.40/0.91 (define @t339 () (tptp.cC40 tptp.iV21026)) % 0.40/0.91 (define @t340 () (tptp.cC108 tptp.iV21026)) % 0.40/0.91 (define @t341 () (and @t5 @t6 @t340 @t339 @t338 @t337 @t336 @t276 @t335 @t334 @t333 @t332 @t331 @t330 @t329 @t328 @t327 @t326 @t325 @t324 @t323 @t322 @t321 @t320 @t319 @t318 @t317 @t316 @t315 @t314 @t313 @t312 @t311 @t310 @t309 @t308 @t307 @t306 @t305 @t304 @t303 @t302 @t301 @t300 @t282 @t299 @t298 @t297 @t287 @t296 @t295 @t292)) % 0.40/0.91 (define @t342 () (not @t341)) % 0.40/0.91 (define @t343 () (forall @t4 @t2)) % 0.40/0.91 (define @t344 () (@list @t1)) % 0.40/0.91 (define @t345 () (@var "BOUND_VARIABLE_8745" $$unsorted)) % 0.40/0.91 (define @t346 () (forall @t4 @t3)) % 0.40/0.91 (define @t347 () (@var "BOUND_VARIABLE_8740" $$unsorted)) % 0.40/0.91 (define @t348 () (and @t346 @t343)) % 0.40/0.91 (define @t349 () (@list tptp.iV21030)) % 0.40/0.91 (define @t350 () (forall @t14 (not @t202))) % 0.40/0.91 (define @t351 () (forall @t14 (not @t208))) % 0.40/0.91 (define @t352 () (forall @t11 (not (tptp.ra_Px88 tptp.iV21030 @t10)))) % 0.40/0.91 (define @t353 () (not @t352)) % 0.40/0.91 (define @t354 () (= @t289 @t353)) % 0.40/0.91 (define @t355 () (@list false false)) % 0.40/0.91 (define @t356 () (@list @t10)) % 0.40/0.91 (define @t357 () (@list @t13)) % 0.40/0.91 (define @t358 () (forall @t14 (not (tptp.ra_Px88 tptp.iV21030 @t13)))) % 0.40/0.91 (define @t359 () (@list true)) % 0.40/0.91 (define @t360 () (tptp.cC68 tptp.iV21030)) % 0.40/0.91 (define @t361 () (= @t360 @t358)) % 0.40/0.91 (define @t362 () (not @t360)) % 0.40/0.91 (define @t363 () (@list true false)) % 0.40/0.91 (define @t364 () (tptp.cC66xcomp tptp.iV21030)) % 0.40/0.91 (define @t365 () (and @t291 @t364)) % 0.40/0.91 (define @t366 () (= @t360 @t365)) % 0.40/0.91 (define @t367 () (not @t365)) % 0.40/0.91 (define @t368 () (not @t364)) % 0.40/0.91 (define @t369 () (not @t291)) % 0.40/0.91 (define @t370 () (@list false true)) % 0.40/0.91 (define @t371 () (forall @t14 (not (tptp.ra_Px21 tptp.iV21030 @t13)))) % 0.40/0.91 (define @t372 () (= @t364 @t371)) % 0.40/0.91 (define @t373 () (not @t371)) % 0.40/0.91 (define @t374 () (forall @t11 (not (tptp.ra_Px21 tptp.iV21030 @t10)))) % 0.40/0.91 (define @t375 () (not @t374)) % 0.40/0.91 (define @t376 () (= @t295 @t375)) % 0.40/0.91 (define @t377 () (not @t376)) % 0.40/0.91 (define @t378 () (forall @t14 (not @t226))) % 0.40/0.91 (define @t379 () (forall @t14 (not @t237))) % 0.40/0.91 (define @t380 () (forall @t14 (not (tptp.ra_Px87 tptp.iV21030 @t13)))) % 0.40/0.91 (define @t381 () (= @t293 @t380)) % 0.40/0.91 (define @t382 () (forall @t11 (not (tptp.ra_Px87 tptp.iV21030 @t10)))) % 0.40/0.91 (define @t383 () (@list false)) % 0.40/0.91 (define @t384 () (not @t382)) % 0.40/0.91 (define @t385 () (tptp.cC74 tptp.iV21030)) % 0.40/0.91 (define @t386 () (= @t385 @t384)) % 0.40/0.91 (define @t387 () (not @t385)) % 0.40/0.91 (define @t388 () (tptp.cC72xcomp tptp.iV21030)) % 0.40/0.91 (define @t389 () (and @t388 @t291)) % 0.40/0.91 (define @t390 () (= @t385 @t389)) % 0.40/0.91 (define @t391 () (not @t389)) % 0.40/0.91 (define @t392 () (not @t388)) % 0.40/0.91 (define @t393 () (forall @t14 (not (tptp.ra_Px24 tptp.iV21030 @t13)))) % 0.40/0.91 (define @t394 () (= @t388 @t393)) % 0.40/0.91 (define @t395 () (not @t393)) % 0.40/0.91 (define @t396 () (forall @t11 (not (tptp.ra_Px24 tptp.iV21030 @t10)))) % 0.40/0.91 (define @t397 () (not @t396)) % 0.40/0.91 (define @t398 () (= @t296 @t397)) % 0.40/0.91 (define @t399 () (not @t398)) % 0.40/0.91 (define @t400 () (forall @t14 (not @t159))) % 0.40/0.91 (define @t401 () (@list tptp.iV21029)) % 0.40/0.91 (define @t402 () (forall @t14 (not @t175))) % 0.40/0.91 (define @t403 () (forall @t14 (not (tptp.ra_Px90 tptp.iV21029 @t13)))) % 0.40/0.91 (define @t404 () (= @t286 @t403)) % 0.40/0.91 (define @t405 () (forall @t11 (not (tptp.ra_Px90 tptp.iV21029 @t10)))) % 0.40/0.91 (define @t406 () (not @t405)) % 0.40/0.91 (define @t407 () (tptp.cC46 tptp.iV21029)) % 0.40/0.91 (define @t408 () (= @t407 @t406)) % 0.40/0.91 (define @t409 () (not @t407)) % 0.40/0.91 (define @t410 () (tptp.cC44xcomp tptp.iV21029)) % 0.40/0.91 (define @t411 () (and @t410 @t285)) % 0.40/0.91 (define @t412 () (= @t407 @t411)) % 0.40/0.91 (define @t413 () (not @t411)) % 0.40/0.91 (define @t414 () (not @t410)) % 0.40/0.91 (define @t415 () (forall @t11 (not (tptp.ra_Px13 tptp.iV21029 @t10)))) % 0.40/0.91 (define @t416 () (not @t415)) % 0.40/0.91 (define @t417 () (= @t410 @t416)) % 0.40/0.91 (define @t418 () (not @t417)) % 0.40/0.91 (define @t419 () (forall @t14 (not (tptp.ra_Px13 tptp.iV21029 @t13)))) % 0.40/0.91 (define @t420 () (= @t297 @t419)) % 0.40/0.91 (define @t421 () (not @t54)) % 0.40/0.91 (define @t422 () (forall @t14 (not @t55))) % 0.40/0.91 (define @t423 () (not @t422)) % 0.40/0.91 (define @t424 () (not @t294)) % 0.40/0.91 (define @t425 () (not @t288)) % 0.40/0.91 (define @t426 () (or @t425 @t424)) % 0.40/0.91 (define @t427 () (not @t426)) % 0.40/0.91 (define @t428 () (forall @t14 (or (not (tptp.rR1 tptp.iV21029 @t13)) @t421))) % 0.40/0.91 (define @t429 () (not @t428)) % 0.40/0.91 (define @t430 () (= @t298 @t429)) % 0.40/0.91 (define @t431 () (not @t430)) % 0.40/0.91 (define @t432 () (@list tptp.iV21027)) % 0.40/0.91 (define @t433 () (forall @t14 (not @t109))) % 0.40/0.91 (define @t434 () (forall @t14 (not @t120))) % 0.40/0.91 (define @t435 () (forall @t14 (not (tptp.ra_Px92 tptp.iV21027 @t13)))) % 0.40/0.91 (define @t436 () (= @t281 @t435)) % 0.40/0.91 (define @t437 () (forall @t11 (not (tptp.ra_Px92 tptp.iV21027 @t10)))) % 0.40/0.91 (define @t438 () (not @t437)) % 0.40/0.91 (define @t439 () (tptp.cC26 tptp.iV21027)) % 0.40/0.91 (define @t440 () (= @t439 @t438)) % 0.40/0.91 (define @t441 () (not @t439)) % 0.40/0.91 (define @t442 () (tptp.cC24xcomp tptp.iV21027)) % 0.40/0.91 (define @t443 () (and @t442 @t280)) % 0.40/0.91 (define @t444 () (= @t439 @t443)) % 0.40/0.91 (define @t445 () (not @t443)) % 0.40/0.91 (define @t446 () (not @t442)) % 0.40/0.91 (define @t447 () (not @t280)) % 0.40/0.91 (define @t448 () (forall @t14 (not (tptp.ra_Px5 tptp.iV21027 @t13)))) % 0.40/0.91 (define @t449 () (= @t442 @t448)) % 0.40/0.91 (define @t450 () (not @t448)) % 0.40/0.91 (define @t451 () (forall @t11 (not (tptp.ra_Px5 tptp.iV21027 @t10)))) % 0.40/0.91 (define @t452 () (not @t451)) % 0.40/0.91 (define @t453 () (= @t299 @t452)) % 0.40/0.91 (define @t454 () (not @t453)) % 0.40/0.91 (define @t455 () (forall @t14 (not @t133))) % 0.40/0.91 (define @t456 () (forall @t14 (not @t139))) % 0.40/0.91 (define @t457 () (forall @t11 (not (tptp.ra_Px91 tptp.iV21027 @t10)))) % 0.40/0.91 (define @t458 () (not @t457)) % 0.40/0.91 (define @t459 () (= @t283 @t458)) % 0.40/0.91 (define @t460 () (forall @t14 (not (tptp.ra_Px91 tptp.iV21027 @t13)))) % 0.40/0.91 (define @t461 () (tptp.cC32 tptp.iV21027)) % 0.40/0.91 (define @t462 () (= @t461 @t460)) % 0.40/0.91 (define @t463 () (not @t461)) % 0.40/0.91 (define @t464 () (tptp.cC30xcomp tptp.iV21027)) % 0.40/0.91 (define @t465 () (and @t280 @t464)) % 0.40/0.91 (define @t466 () (= @t461 @t465)) % 0.40/0.91 (define @t467 () (not @t465)) % 0.40/0.91 (define @t468 () (not @t464)) % 0.40/0.91 (define @t469 () (forall @t14 (not (tptp.ra_Px8 tptp.iV21027 @t13)))) % 0.40/0.91 (define @t470 () (= @t464 @t469)) % 0.40/0.91 (define @t471 () (not @t469)) % 0.40/0.91 (define @t472 () (forall @t11 (not (tptp.ra_Px8 tptp.iV21027 @t10)))) % 0.40/0.91 (define @t473 () (not @t472)) % 0.40/0.91 (define @t474 () (= @t300 @t473)) % 0.40/0.91 (define @t475 () (not @t474)) % 0.40/0.91 (define @t476 () (@list tptp.iV21026)) % 0.40/0.91 (define @t477 () (and @t333 @t328)) % 0.40/0.91 (define @t478 () (= @t277 @t477)) % 0.40/0.91 (define @t479 () (not @t477)) % 0.40/0.91 (define @t480 () (@list @t477)) % 0.40/0.91 (define @t481 () (and @t331 @t302)) % 0.40/0.91 (define @t482 () (= @t333 @t481)) % 0.40/0.91 (define @t483 () (not @t333)) % 0.40/0.91 (define @t484 () (not @t481)) % 0.40/0.91 (define @t485 () (@list @t481)) % 0.40/0.91 (define @t486 () (and @t329 @t320)) % 0.40/0.91 (define @t487 () (= @t302 @t486)) % 0.40/0.91 (define @t488 () (not @t302)) % 0.40/0.91 (define @t489 () (and @t338 @t304)) % 0.40/0.91 (define @t490 () (= @t320 @t489)) % 0.40/0.91 (define @t491 () (not @t320)) % 0.40/0.91 (define @t492 () (and @t313 @t325)) % 0.40/0.91 (define @t493 () (= @t304 @t492)) % 0.40/0.91 (define @t494 () (not @t304)) % 0.40/0.91 (define @t495 () (and @t324 @t315)) % 0.40/0.91 (define @t496 () (= @t313 @t495)) % 0.40/0.91 (define @t497 () (not @t313)) % 0.40/0.91 (define @t498 () (and @t267 @t269)) % 0.40/0.91 (define @t499 () (= @t316 @t498)) % 0.40/0.91 (define @t500 () (and @t316 @t261)) % 0.40/0.91 (define @t501 () (not @t316)) % 0.40/0.91 (define @t502 () (not @t261)) % 0.40/0.91 (define @t503 () (= @t321 @t500)) % 0.40/0.91 (define @t504 () (= @t261 @t339)) % 0.40/0.91 (define @t505 () (and @t339 @t321)) % 0.40/0.91 (define @t506 () (not @t321)) % 0.40/0.91 (define @t507 () (not @t339)) % 0.40/0.91 (define @t508 () (= @t303 @t505)) % 0.40/0.91 (define @t509 () (forall @t14 (not @t107))) % 0.40/0.91 (define @t510 () (not @t509)) % 0.40/0.91 (define @t511 () (not @t278)) % 0.40/0.91 (define @t512 () (or @t511 @t447)) % 0.40/0.91 (define @t513 () (not @t512)) % 0.40/0.91 (define @t514 () (forall @t14 (or (not (tptp.rR1 tptp.iV21026 @t13)) (not @t106)))) % 0.40/0.91 (define @t515 () (not @t514)) % 0.40/0.91 (define @t516 () (= @t305 @t515)) % 0.40/0.91 (define @t517 () (not @t516)) % 0.40/0.91 (define @t518 () (and @t272 @t265)) % 0.40/0.91 (define @t519 () (= @t306 @t518)) % 0.40/0.91 (define @t520 () (and @t264 @t271)) % 0.40/0.91 (define @t521 () (= @t307 @t520)) % 0.40/0.91 (define @t522 () (= @t261 @t308)) % 0.40/0.91 (define @t523 () (and @t273 @t262)) % 0.40/0.91 (define @t524 () (= @t327 @t523)) % 0.40/0.91 (define @t525 () (and @t327 @t261)) % 0.40/0.91 (define @t526 () (not @t327)) % 0.40/0.91 (define @t527 () (= @t309 @t525)) % 0.40/0.91 (define @t528 () (and @t268 @t259)) % 0.40/0.91 (define @t529 () (= @t310 @t528)) % 0.40/0.91 (define @t530 () (and @t323 @t326)) % 0.40/0.91 (define @t531 () (= @t331 @t530)) % 0.40/0.91 (define @t532 () (not @t331)) % 0.40/0.91 (define @t533 () (not @t530)) % 0.40/0.91 (define @t534 () (@list @t530)) % 0.40/0.91 (define @t535 () (and @t337 @t311)) % 0.40/0.91 (define @t536 () (= @t326 @t535)) % 0.40/0.91 (define @t537 () (not @t326)) % 0.40/0.91 (define @t538 () (not @t535)) % 0.40/0.91 (define @t539 () (@list @t535)) % 0.40/0.91 (define @t540 () (= @t261 @t318)) % 0.40/0.91 (define @t541 () (and @t275 @t270)) % 0.40/0.91 (define @t542 () (= @t334 @t541)) % 0.40/0.91 (define @t543 () (and @t334 @t261)) % 0.40/0.91 (define @t544 () (not @t334)) % 0.40/0.91 (define @t545 () (= @t335 @t543)) % 0.40/0.91 (define @t546 () (and @t335 @t303)) % 0.40/0.91 (define @t547 () (not @t303)) % 0.40/0.91 (define @t548 () (not @t335)) % 0.40/0.91 (define @t549 () (= @t330 @t546)) % 0.40/0.91 (define @t550 () (and @t330 @t318)) % 0.40/0.91 (define @t551 () (not @t318)) % 0.40/0.91 (define @t552 () (not @t330)) % 0.40/0.91 (define @t553 () (= @t314 @t550)) % 0.40/0.91 (define @t554 () (and @t314 @t309)) % 0.40/0.91 (define @t555 () (not @t309)) % 0.40/0.91 (define @t556 () (not @t314)) % 0.40/0.91 (define @t557 () (= @t312 @t554)) % 0.40/0.91 (define @t558 () (and @t317 @t305)) % 0.40/0.91 (define @t559 () (= @t337 @t558)) % 0.40/0.91 (define @t560 () (not @t337)) % 0.40/0.91 (define @t561 () (and @t274 @t306)) % 0.40/0.91 (define @t562 () (not @t306)) % 0.40/0.91 (define @t563 () (= @t319 @t561)) % 0.40/0.91 (define @t564 () (= @t261 @t322)) % 0.40/0.91 (define @t565 () (= @t261 @t324)) % 0.40/0.91 (define @t566 () (and @t307 @t261)) % 0.40/0.91 (define @t567 () (not @t307)) % 0.40/0.91 (define @t568 () (= @t325 @t566)) % 0.40/0.91 (define @t569 () (and @t310 @t261)) % 0.40/0.91 (define @t570 () (not @t310)) % 0.40/0.91 (define @t571 () (= @t329 @t569)) % 0.40/0.91 (define @t572 () (and @t263 @t266)) % 0.40/0.91 (define @t573 () (= @t340 @t572)) % 0.40/0.91 (define @t574 () (and @t340 @t261)) % 0.40/0.91 (define @t575 () (not @t340)) % 0.40/0.91 (define @t576 () (= @t332 @t574)) % 0.40/0.91 (define @t577 () (= @t261 @t338)) % 0.40/0.91 (define @t578 () (and @t312 @t322)) % 0.40/0.91 (define @t579 () (not @t312)) % 0.40/0.91 (define @t580 () (not @t322)) % 0.40/0.91 (define @t581 () (= @t301 @t578)) % 0.40/0.91 (define @t582 () (and @t332 @t336)) % 0.40/0.91 (define @t583 () (= @t315 @t582)) % 0.40/0.91 (define @t584 () (not @t315)) % 0.40/0.91 (define @t585 () (forall (@list @t345) (not (tptp.cowlNothing @t345)))) % 0.40/0.91 (define @t586 () (forall (@list @t347) (tptp.cowlThing @t347))) % 0.40/0.91 (assume @p1 @t5) % 0.40/0.91 (assume @p2 @t6) % 0.40/0.91 (assume @p3 (forall @t4 (= @t9 (and @t8 @t7)))) % 0.40/0.91 (assume @p4 (forall @t4 (= @t12 (exists @t11 (tptp.ra_Px33 @t1 @t10))))) % 0.40/0.91 (assume @p5 (forall @t4 (= @t15 (not (exists @t14 (tptp.ra_Px33 @t1 @t13)))))) % 0.40/0.91 (assume @p6 (forall @t4 (= @t16 (not (exists @t14 (tptp.ra_Px34 @t1 @t13)))))) % 0.40/0.91 (assume @p7 (forall @t4 (= @t16 @t18))) % 0.40/0.91 (assume @p8 (forall @t4 (= @t19 (exists @t11 (tptp.ra_Px34 @t1 @t10))))) % 0.40/0.91 (assume @p9 (forall @t4 (= @t20 (and @t19 @t15)))) % 0.40/0.91 (assume @p10 (forall @t4 (= @t20 (not (exists @t14 (tptp.ra_Px85 @t1 @t13)))))) % 0.40/0.91 (assume @p11 (forall @t4 (= @t21 (exists @t11 (tptp.ra_Px85 @t1 @t10))))) % 0.40/0.91 (assume @p12 (forall @t4 (= @t22 (exists @t14 (and @t17 (tptp.cC104 @t13)))))) % 0.40/0.91 (assume @p13 (forall @t4 (= @t22 (exists @t11 (tptp.ra_Px36 @t1 @t10))))) % 0.40/0.91 (assume @p14 (forall @t4 (= @t23 (not (exists @t14 (tptp.ra_Px36 @t1 @t13)))))) % 0.40/0.91 (assume @p15 (forall @t4 (= @t25 (and @t24 @t23)))) % 0.40/0.91 (assume @p16 (forall @t4 (= @t27 (and @t25 @t26)))) % 0.40/0.91 (assume @p17 (forall @t4 (= @t29 (and @t27 @t28)))) % 0.40/0.91 (assume @p18 @t31) % 0.40/0.91 (assume @p19 (forall @t4 (= @t32 (and @t30 @t29)))) % 0.40/0.91 (assume @p20 (forall @t4 (= @t34 @t33))) % 0.40/0.91 (assume @p21 (forall @t4 (= @t34 (exists @t11 (tptp.ra_Px39 @t1 @t10))))) % 0.40/0.91 (assume @p22 (forall @t4 (= @t35 (not (exists @t14 (tptp.ra_Px39 @t1 @t13)))))) % 0.40/0.91 (assume @p23 (forall @t4 (= (tptp.cC12 @t1) (not (exists @t14 (tptp.ra_Px1 @t1 @t13)))))) % 0.40/0.91 (assume @p24 (forall @t4 (= @t36 (exists @t11 (tptp.ra_Px1 @t1 @t10))))) % 0.40/0.91 (assume @p25 (forall @t4 (= @t37 (exists @t11 (tptp.ra_Px84 @t1 @t10))))) % 0.40/0.91 (assume @p26 (forall @t4 (= @t37 (and @t38 @t35)))) % 0.40/0.91 (assume @p27 (forall @t4 (= @t39 (not (exists @t14 (tptp.ra_Px84 @t1 @t13)))))) % 0.40/0.91 (assume @p28 (forall @t4 (= @t40 (not (exists @t14 (tptp.ra_Px43 @t1 @t13)))))) % 0.40/0.91 (assume @p29 (forall @t4 (= @t40 (exists @t14 (and @t17 (tptp.cC120 @t13)))))) % 0.40/0.91 (assume @p30 (forall @t4 (= @t41 (exists @t11 (tptp.ra_Px43 @t1 @t10))))) % 0.40/0.91 (assume @p31 (forall @t4 (= @t42 (exists @t11 (tptp.ra_Px42 @t1 @t10))))) % 0.40/0.91 (assume @p32 (forall @t4 (= @t42 @t33))) % 0.40/0.91 (assume @p33 (forall @t4 (= @t43 (not (exists @t14 (tptp.ra_Px42 @t1 @t13)))))) % 0.40/0.91 (assume @p34 (forall @t4 (= @t44 (exists @t11 (tptp.ra_Px83 @t1 @t10))))) % 0.40/0.91 (assume @p35 (forall @t4 (= @t44 (and @t43 @t15)))) % 0.40/0.91 (assume @p36 (forall @t4 (= @t45 (not (exists @t14 (tptp.ra_Px83 @t1 @t13)))))) % 0.40/0.91 (assume @p37 (forall @t4 (= @t46 (exists @t14 (and @t17 (tptp.cC126 @t13)))))) % 0.40/0.91 (assume @p38 (forall @t4 (= @t46 (exists @t11 (tptp.ra_Px44 @t1 @t10))))) % 0.40/0.91 (assume @p39 (forall @t4 (= @t47 (not (exists @t14 (tptp.ra_Px44 @t1 @t13)))))) % 0.40/0.91 (assume @p40 (forall @t4 (= @t48 (and @t47 @t41)))) % 0.40/0.91 (assume @p41 (forall @t4 (= @t49 (and @t48 @t26)))) % 0.40/0.91 (assume @p42 (forall @t4 (= @t50 (and @t32 @t49)))) % 0.40/0.91 (assume @p43 @t52) % 0.40/0.91 (assume @p44 (forall @t4 (= @t53 (and @t51 @t50)))) % 0.40/0.91 (assume @p45 (forall @t4 (= @t57 @t56))) % 0.40/0.91 (assume @p46 (forall @t4 (= @t59 @t58))) % 0.40/0.91 (assume @p47 (forall @t4 (= @t59 (exists @t11 (tptp.ra_Px47 @t1 @t10))))) % 0.40/0.91 (assume @p48 (forall @t4 (= @t60 (not (exists @t14 (tptp.ra_Px47 @t1 @t13)))))) % 0.40/0.91 (assume @p49 (forall @t4 (= @t61 (and @t60 @t38)))) % 0.40/0.91 (assume @p50 (forall @t4 (= @t61 (not (exists @t14 (tptp.ra_Px82 @t1 @t13)))))) % 0.40/0.91 (assume @p51 (forall @t4 (= @t62 (exists @t11 (tptp.ra_Px82 @t1 @t10))))) % 0.40/0.91 (assume @p52 (forall @t4 (= @t63 (exists @t14 (and @t17 (tptp.cC142 @t13)))))) % 0.40/0.91 (assume @p53 (forall @t4 (= @t63 (exists @t11 (tptp.ra_Px51 @t1 @t10))))) % 0.40/0.91 (assume @p54 (forall @t4 (= @t64 (not (exists @t14 (tptp.ra_Px51 @t1 @t13)))))) % 0.40/0.91 (assume @p55 (forall @t4 (= @t65 (exists @t11 (tptp.ra_Px50 @t1 @t10))))) % 0.40/0.91 (assume @p56 (forall @t4 (= @t65 @t58))) % 0.40/0.91 (assume @p57 (forall @t4 (= @t66 (not (exists @t14 (tptp.ra_Px50 @t1 @t13)))))) % 0.40/0.91 (assume @p58 (forall @t4 (= @t67 (exists @t11 (tptp.ra_Px81 @t1 @t10))))) % 0.40/0.91 (assume @p59 (forall @t4 (= @t67 (and @t15 @t66)))) % 0.40/0.91 (assume @p60 (forall @t4 (= @t68 (not (exists @t14 (tptp.ra_Px81 @t1 @t13)))))) % 0.40/0.91 (assume @p61 (forall @t4 (= @t69 (not (exists @t14 (tptp.ra_Px52 @t1 @t13)))))) % 0.40/0.91 (assume @p62 (forall @t4 (= @t69 (exists @t14 (and @t17 (tptp.cC148 @t13)))))) % 0.40/0.91 (assume @p63 (forall @t4 (= @t70 (exists @t11 (tptp.ra_Px52 @t1 @t10))))) % 0.40/0.91 (assume @p64 (forall @t4 (= @t71 (and @t64 @t70)))) % 0.40/0.91 (assume @p65 (forall @t4 (= @t72 (and @t71 @t26)))) % 0.40/0.91 (assume @p66 (forall @t4 (= @t73 (and @t72 @t53)))) % 0.40/0.91 (assume @p67 (forall @t4 (= @t75 (and @t74 @t73)))) % 0.40/0.91 (assume @p68 (forall @t4 (= @t76 (and @t9 @t57)))) % 0.40/0.91 (assume @p69 (forall @t4 (= @t77 (exists @t11 (tptp.ra_Px80 @t1 @t10))))) % 0.40/0.91 (assume @p70 (forall @t4 (= @t77 @t18))) % 0.40/0.91 (assume @p71 (forall @t4 (= @t78 (not (exists @t14 (tptp.ra_Px80 @t1 @t13)))))) % 0.40/0.91 (assume @p72 (forall @t4 (= @t79 (not (exists @t14 (tptp.ra_Px55 @t1 @t13)))))) % 0.40/0.91 (assume @p73 (forall @t4 (= @t79 (exists @t14 (and @t17 (tptp.cC160 @t13)))))) % 0.40/0.91 (assume @p74 (forall @t4 (= @t80 (exists @t11 (tptp.ra_Px55 @t1 @t10))))) % 0.40/0.91 (assume @p75 (forall @t4 (= @t81 @t33))) % 0.40/0.91 (assume @p76 (forall @t4 (= @t81 (not (exists @t14 (tptp.ra_Px79 @t1 @t13)))))) % 0.40/0.91 (assume @p77 (forall @t4 (= @t82 (exists @t11 (tptp.ra_Px79 @t1 @t10))))) % 0.40/0.91 (assume @p78 (forall @t4 (= @t83 (exists @t14 (and @t17 (tptp.cC164 @t13)))))) % 0.40/0.91 (assume @p79 (forall @t4 (= @t83 (exists @t11 (tptp.ra_Px56 @t1 @t10))))) % 0.40/0.91 (assume @p80 (forall @t4 (= @t84 (not (exists @t14 (tptp.ra_Px56 @t1 @t13)))))) % 0.40/0.91 (assume @p81 (forall @t4 (= @t85 (and @t80 @t84)))) % 0.40/0.91 (assume @p82 (forall @t4 (= @t86 (exists @t11 (tptp.ra_Px78 @t1 @t10))))) % 0.40/0.91 (assume @p83 (forall @t4 (= @t86 @t87))) % 0.40/0.91 (assume @p84 (forall @t4 (= @t88 (not (exists @t14 (tptp.ra_Px78 @t1 @t13)))))) % 0.40/0.91 (assume @p85 (forall @t4 (= @t89 (not (exists @t14 (tptp.ra_Px58 @t1 @t13)))))) % 0.40/0.91 (assume @p86 (forall @t4 (= @t89 (exists @t14 (and @t17 (tptp.cC170 @t13)))))) % 0.40/0.91 (assume @p87 (forall @t4 (= @t90 (exists @t11 (tptp.ra_Px58 @t1 @t10))))) % 0.40/0.91 (assume @p88 (forall @t4 (= @t91 (and @t90 @t85)))) % 0.40/0.91 (assume @p89 (forall @t4 (= @t92 (exists @t11 (tptp.ra_Px77 @t1 @t10))))) % 0.40/0.91 (assume @p90 (forall @t4 (= @t92 @t58))) % 0.40/0.91 (assume @p91 (forall @t4 (= @t93 (not (exists @t14 (tptp.ra_Px77 @t1 @t13)))))) % 0.40/0.91 (assume @p92 (forall @t4 (= @t94 (exists @t11 (tptp.ra_Px60 @t1 @t10))))) % 0.40/0.91 (assume @p93 (forall @t4 (= @t94 (exists @t14 (and @t17 (tptp.cC176 @t13)))))) % 0.40/0.91 (assume @p94 (forall @t4 (= @t95 (not (exists @t14 (tptp.ra_Px60 @t1 @t13)))))) % 0.40/0.91 (assume @p95 (forall @t4 (= @t96 (exists @t11 (tptp.ra_Px2 @t1 @t10))))) % 0.40/0.91 (assume @p96 (forall @t4 (= @t97 (not (exists @t14 (tptp.ra_Px2 @t1 @t13)))))) % 0.40/0.91 (assume @p97 (forall @t4 (= @t98 (and @t91 @t95)))) % 0.40/0.91 (assume @p98 (forall @t4 (= (tptp.cC2 @t1) (exists @t11 (tptp.ra_Px3 @t1 @t10))))) % 0.40/0.91 (assume @p99 (forall @t4 (= @t99 (not (exists @t14 (tptp.ra_Px3 @t1 @t13)))))) % 0.40/0.91 (assume @p100 (forall @t4 (= @t100 @t87))) % 0.40/0.91 (assume @p101 (forall @t4 (= @t74 (and @t100 @t76)))) % 0.40/0.91 (assume @p102 @t105) % 0.40/0.91 (assume @p103 (forall @t4 (= @t103 @t108))) % 0.40/0.91 (assume @p104 @t114) % 0.40/0.91 (assume @p105 @t119) % 0.40/0.91 (assume @p106 (forall @t4 (= @t117 (and @t112 @t99)))) % 0.40/0.91 (assume @p107 @t125) % 0.40/0.91 (assume @p108 (forall @t4 (= @t126 (exists @t14 (and @t17 (tptp.cC26 @t13)))))) % 0.40/0.91 (assume @p109 (forall @t4 (= @t126 (exists @t11 (tptp.ra_Px9 @t1 @t10))))) % 0.40/0.91 (assume @p110 (forall @t4 (= @t127 (not (exists @t14 (tptp.ra_Px9 @t1 @t13)))))) % 0.40/0.91 (assume @p111 @t132) % 0.40/0.91 (assume @p112 (forall @t4 (= @t130 @t56))) % 0.40/0.91 (assume @p113 @t138) % 0.40/0.91 (assume @p114 @t144) % 0.40/0.91 (assume @p115 (forall @t4 (= @t142 (and @t99 @t136)))) % 0.40/0.91 (assume @p116 @t149) % 0.40/0.91 (assume @p117 (forall @t4 (= @t150 (not (exists @t14 (tptp.ra_Px10 @t1 @t13)))))) % 0.40/0.91 (assume @p118 (forall @t4 (= @t150 (exists @t14 (and @t17 (tptp.cC32 @t13)))))) % 0.40/0.91 (assume @p119 (forall @t4 (= @t151 (exists @t11 (tptp.ra_Px10 @t1 @t10))))) % 0.40/0.91 (assume @p120 (forall @t4 (= @t152 (and @t151 @t127)))) % 0.40/0.91 (assume @p121 (forall @t4 (= @t153 (and @t152 @t26)))) % 0.40/0.91 (assume @p122 @t155) % 0.40/0.91 (assume @p123 @t157) % 0.40/0.91 (assume @p124 (forall @t4 (= @t158 (and @t156 @t153)))) % 0.40/0.91 (assume @p125 @t164) % 0.40/0.91 (assume @p126 (forall @t4 (= @t162 @t108))) % 0.40/0.91 (assume @p127 @t169) % 0.40/0.91 (assume @p128 @t174) % 0.40/0.91 (assume @p129 (forall @t4 (= @t172 (and @t167 @t36)))) % 0.40/0.91 (assume @p130 @t180) % 0.40/0.91 (assume @p131 (forall @t4 (= @t181 (exists @t11 (tptp.ra_Px17 @t1 @t10))))) % 0.40/0.91 (assume @p132 (forall @t4 (= @t181 (exists @t14 (and @t17 (tptp.cC46 @t13)))))) % 0.40/0.91 (assume @p133 (forall @t4 (= @t182 (not (exists @t14 (tptp.ra_Px17 @t1 @t13)))))) % 0.40/0.91 (assume @p134 @t184) % 0.40/0.91 (assume @p135 (forall @t4 (= @t183 (not (exists @t14 (tptp.ra_Px16 @t1 @t13)))))) % 0.40/0.91 (assume @p136 (forall @t4 (= @t185 (exists @t11 (tptp.ra_Px16 @t1 @t10))))) % 0.40/0.91 (assume @p137 (forall @t4 (= @t186 (exists @t11 (tptp.ra_Px89 @t1 @t10))))) % 0.40/0.91 (assume @p138 (forall @t4 (= @t186 (and @t185 @t36)))) % 0.40/0.91 (assume @p139 (forall @t4 (= @t187 (not (exists @t14 (tptp.ra_Px89 @t1 @t13)))))) % 0.40/0.91 (assume @p140 (forall @t4 (= @t188 (exists @t14 (and @t17 (tptp.cC52 @t13)))))) % 0.40/0.91 (assume @p141 (forall @t4 (= @t188 (exists @t11 (tptp.ra_Px18 @t1 @t10))))) % 0.40/0.91 (assume @p142 (forall @t4 (= @t189 (not (exists @t14 (tptp.ra_Px18 @t1 @t13)))))) % 0.40/0.91 (assume @p143 (forall @t4 (= @t190 (and @t182 @t189)))) % 0.40/0.91 (assume @p144 (forall @t4 (= @t191 (and @t190 @t26)))) % 0.40/0.91 (assume @p145 (forall @t4 (= @t192 (exists @t11 (tptp.ra_Px27 @t1 @t10))))) % 0.40/0.91 (assume @p146 (forall @t4 (= (tptp.cC6xcomp @t1) (not (exists @t14 (tptp.ra_Px27 @t1 @t13)))))) % 0.40/0.91 (assume @p147 (forall @t4 (= @t193 (and @t191 @t158)))) % 0.40/0.91 (assume @p148 @t195) % 0.40/0.91 (assume @p149 (forall @t4 (= @t196 (and @t193 @t194)))) % 0.40/0.91 (assume @p150 @t201) % 0.40/0.91 (assume @p151 (forall @t4 (= @t199 @t108))) % 0.40/0.91 (assume @p152 @t207) % 0.40/0.91 (assume @p153 @t213) % 0.40/0.91 (assume @p154 (forall @t4 (= @t211 (and @t97 @t205)))) % 0.40/0.91 (assume @p155 @t218) % 0.40/0.91 (assume @p156 (forall @t4 (= @t219 (exists @t14 (and @t17 (tptp.cC68 @t13)))))) % 0.40/0.91 (assume @p157 (forall @t4 (= @t219 (not (exists @t14 (tptp.ra_Px25 @t1 @t13)))))) % 0.40/0.91 (assume @p158 (forall @t4 (= @t220 (exists @t11 (tptp.ra_Px25 @t1 @t10))))) % 0.40/0.91 (assume @p159 @t225) % 0.40/0.91 (assume @p160 (forall @t4 (= @t223 @t56))) % 0.40/0.91 (assume @p161 @t231) % 0.40/0.91 (assume @p162 (forall @t4 (= @t232 (and @t229 @t97)))) % 0.40/0.91 (assume @p163 @t236) % 0.40/0.91 (assume @p164 @t242) % 0.40/0.91 (assume @p165 (forall @t4 (= @t243 (exists @t14 (and @t17 (tptp.cC74 @t13)))))) % 0.40/0.91 (assume @p166 (forall @t4 (= @t243 (exists @t11 (tptp.ra_Px26 @t1 @t10))))) % 0.40/0.91 (assume @p167 (forall @t4 (= @t244 (not (exists @t14 (tptp.ra_Px26 @t1 @t13)))))) % 0.40/0.91 (assume @p168 (forall @t4 (= @t245 (and @t220 @t244)))) % 0.40/0.91 (assume @p169 (forall @t4 (= @t8 @t18))) % 0.40/0.91 (assume @p170 (forall @t4 (= @t246 (and @t245 @t26)))) % 0.40/0.91 (assume @p171 (forall @t4 (= @t247 (and @t196 @t246)))) % 0.40/0.91 (assume @p172 @t249) % 0.40/0.91 (assume @p173 (forall @t4 (= @t250 (and @t247 @t248)))) % 0.40/0.91 (assume @p174 @t252) % 0.40/0.91 (assume @p175 (forall @t4 (= @t28 (and @t250 @t251)))) % 0.40/0.91 (assume @p176 (forall @t4 (= @t253 (not (exists @t14 (tptp.ra_Px28 @t1 @t13)))))) % 0.40/0.91 (assume @p177 (forall @t4 (= @t38 (exists @t11 (tptp.ra_Px28 @t1 @t10))))) % 0.40/0.91 (assume @p178 (forall @t4 (= @t254 (exists @t11 (tptp.ra_Px29 @t1 @t10))))) % 0.40/0.91 (assume @p179 (forall @t4 (= @t254 @t18))) % 0.40/0.91 (assume @p180 (forall @t4 (= @t255 (not (exists @t14 (tptp.ra_Px29 @t1 @t13)))))) % 0.40/0.91 (assume @p181 (forall @t4 (= @t256 (and @t255 @t38)))) % 0.40/0.91 (assume @p182 (forall @t4 (= @t256 (exists @t11 (tptp.ra_Px86 @t1 @t10))))) % 0.40/0.91 (assume @p183 (forall @t4 (= @t257 (not (exists @t14 (tptp.ra_Px86 @t1 @t13)))))) % 0.40/0.91 (assume @p184 (forall @t4 (= @t258 (exists @t14 (and @t17 (tptp.cC96 @t13)))))) % 0.40/0.91 (assume @p185 (forall @t4 (= @t258 (exists @t11 (tptp.ra_Px35 @t1 @t10))))) % 0.40/0.91 (assume @p186 (forall @t4 (= @t24 (not (exists @t14 (tptp.ra_Px35 @t1 @t13)))))) % 0.40/0.91 (assume @p187 (forall @t4 (= (tptp.cTEST @t1) (and @t75 @t98)))) % 0.40/0.91 (assume @p188 @t259) % 0.40/0.91 (assume @p189 (forall @t4 (=> @t260 @t88))) % 0.40/0.91 (assume @p190 (forall @t4 (=> @t260 @t178))) % 0.40/0.91 (assume @p191 @t261) % 0.40/0.91 (assume @p192 (forall @t4 (=> @t260 @t78))) % 0.40/0.91 (assume @p193 (forall @t4 (=> @t260 @t93))) % 0.40/0.91 (assume @p194 (forall @t4 (=> @t260 @t82))) % 0.40/0.91 (assume @p195 (forall @t4 (=> @t260 @t68))) % 0.40/0.91 (assume @p196 @t262) % 0.40/0.91 (assume @p197 @t263) % 0.40/0.91 (assume @p198 @t264) % 0.40/0.91 (assume @p199 @t265) % 0.40/0.91 (assume @p200 @t266) % 0.40/0.91 (assume @p201 (forall @t4 (=> @t260 @t39))) % 0.40/0.91 (assume @p202 (forall @t4 (=> @t260 @t216))) % 0.40/0.91 (assume @p203 (forall @t4 (=> @t260 @t123))) % 0.40/0.91 (assume @p204 @t267) % 0.40/0.91 (assume @p205 @t268) % 0.40/0.91 (assume @p206 @t269) % 0.40/0.91 (assume @p207 (forall @t4 (=> @t260 @t21))) % 0.40/0.91 (assume @p208 (forall @t4 (=> @t260 @t45))) % 0.40/0.91 (assume @p209 (forall @t4 (=> @t260 @t257))) % 0.40/0.91 (assume @p210 @t270) % 0.40/0.91 (assume @p211 @t271) % 0.40/0.91 (assume @p212 (forall @t4 (=> @t260 @t187))) % 0.40/0.91 (assume @p213 (forall @t4 (=> @t260 @t62))) % 0.40/0.91 (assume @p214 @t272) % 0.40/0.91 (assume @p215 (forall @t4 (=> @t260 @t147))) % 0.40/0.91 (assume @p216 @t273) % 0.40/0.91 (assume @p217 @t274) % 0.40/0.91 (assume @p218 @t275) % 0.40/0.91 (assume @p219 (forall @t4 (=> @t260 @t240))) % 0.40/0.91 (assume @p220 @t276) % 0.40/0.91 (assume @p221 (tptp.cC178xcomp tptp.iV21026)) % 0.40/0.91 (assume @p222 @t277) % 0.40/0.91 (assume @p223 (tptp.rR1 tptp.iV21026 tptp.iV21030)) % 0.40/0.91 (assume @p224 @t278) % 0.40/0.91 (assume @p225 (tptp.rR1 tptp.iV21026 tptp.iV21028)) % 0.40/0.91 (assume @p226 (tptp.rR1 tptp.iV21026 tptp.iV21029)) % 0.40/0.91 (assume @p227 (tptp.cC12 tptp.iV21027)) % 0.40/0.91 (assume @p228 (forall @t4 (=> @t279 @t96))) % 0.40/0.91 (assume @p229 (tptp.cC176xcomp tptp.iV21027)) % 0.40/0.91 (assume @p230 (tptp.cC96xcomp tptp.iV21027)) % 0.40/0.91 (assume @p231 (tptp.cC170xcomp tptp.iV21027)) % 0.40/0.91 (assume @p232 (tptp.cC120xcomp tptp.iV21027)) % 0.40/0.91 (assume @p233 (tptp.cC92 tptp.iV21027)) % 0.40/0.91 (assume @p234 (forall @t4 (=> @t279 @t192))) % 0.40/0.91 (assume @p235 (tptp.cC148xcomp tptp.iV21027)) % 0.40/0.91 (assume @p236 (tptp.cC142xcomp tptp.iV21027)) % 0.40/0.91 (assume @p237 (tptp.cC68xcomp tptp.iV21027)) % 0.40/0.91 (assume @p238 @t280) % 0.40/0.91 (assume @p239 (tptp.cC18 tptp.iV21027)) % 0.40/0.91 (assume @p240 (tptp.cC52xcomp tptp.iV21027)) % 0.40/0.91 (assume @p241 (forall @t4 (=> @t279 @t12))) % 0.40/0.91 (assume @p242 (tptp.cC104xcomp tptp.iV21027)) % 0.40/0.91 (assume @p243 @t281) % 0.40/0.91 (assume @p244 (tptp.cC46xcomp tptp.iV21027)) % 0.40/0.91 (assume @p245 (tptp.cC126xcomp tptp.iV21027)) % 0.40/0.91 (assume @p246 (tptp.cC164xcomp tptp.iV21027)) % 0.40/0.91 (assume @p247 (tptp.cC100 tptp.iV21027)) % 0.40/0.91 (assume @p248 (tptp.cC160xcomp tptp.iV21027)) % 0.40/0.91 (assume @p249 @t282) % 0.40/0.91 (assume @p250 (tptp.cC74xcomp tptp.iV21027)) % 0.40/0.91 (assume @p251 @t283) % 0.40/0.91 (assume @p252 (forall @t4 (=> @t279 @t253))) % 0.40/0.91 (assume @p253 (tptp.rR1 tptp.iV21027 tptp.iV21036)) % 0.40/0.91 (assume @p254 (tptp.rR1 tptp.iV21027 tptp.iV21035)) % 0.40/0.91 (assume @p255 (tptp.cowlThing tptp.iV21028)) % 0.40/0.91 (assume @p256 (forall @t4 (=> @t284 @t192))) % 0.40/0.91 (assume @p257 (tptp.cC176xcomp tptp.iV21029)) % 0.40/0.91 (assume @p258 (tptp.cC96xcomp tptp.iV21029)) % 0.40/0.91 (assume @p259 (tptp.cC120xcomp tptp.iV21029)) % 0.40/0.91 (assume @p260 (tptp.cC170xcomp tptp.iV21029)) % 0.40/0.91 (assume @p261 (forall @t4 (=> @t284 @t96))) % 0.40/0.91 (assume @p262 (tptp.cC92 tptp.iV21029)) % 0.40/0.91 (assume @p263 (tptp.cC148xcomp tptp.iV21029)) % 0.40/0.91 (assume @p264 (tptp.cC142xcomp tptp.iV21029)) % 0.40/0.91 (assume @p265 (tptp.cC68xcomp tptp.iV21029)) % 0.40/0.91 (assume @p266 @t285) % 0.40/0.91 (assume @p267 (forall @t4 (=> @t284 @t253))) % 0.40/0.91 (assume @p268 (tptp.cC18 tptp.iV21029)) % 0.40/0.91 (assume @p269 (tptp.cC52xcomp tptp.iV21029)) % 0.40/0.91 (assume @p270 (tptp.cC104xcomp tptp.iV21029)) % 0.40/0.91 (assume @p271 (tptp.cC2 tptp.iV21029)) % 0.40/0.91 (assume @p272 (tptp.cC26xcomp tptp.iV21029)) % 0.40/0.91 (assume @p273 @t286) % 0.40/0.91 (assume @p274 (forall @t4 (=> @t284 @t12))) % 0.40/0.91 (assume @p275 (tptp.cC126xcomp tptp.iV21029)) % 0.40/0.91 (assume @p276 (tptp.cC164xcomp tptp.iV21029)) % 0.40/0.91 (assume @p277 (tptp.cC100 tptp.iV21029)) % 0.40/0.91 (assume @p278 (tptp.cC160xcomp tptp.iV21029)) % 0.40/0.91 (assume @p279 @t287) % 0.40/0.91 (assume @p280 (tptp.cC74xcomp tptp.iV21029)) % 0.40/0.91 (assume @p281 (tptp.cC32xcomp tptp.iV21029)) % 0.40/0.91 (assume @p282 (tptp.rR1 tptp.iV21029 tptp.iV21034)) % 0.40/0.91 (assume @p283 @t288) % 0.40/0.91 (assume @p284 (tptp.cC12 tptp.iV21030)) % 0.40/0.91 (assume @p285 (tptp.cC176xcomp tptp.iV21030)) % 0.40/0.91 (assume @p286 (tptp.cC96xcomp tptp.iV21030)) % 0.40/0.91 (assume @p287 (tptp.cC170xcomp tptp.iV21030)) % 0.40/0.91 (assume @p288 (tptp.cC120xcomp tptp.iV21030)) % 0.40/0.91 (assume @p289 (tptp.cC92 tptp.iV21030)) % 0.40/0.91 (assume @p290 (tptp.cC148xcomp tptp.iV21030)) % 0.40/0.91 (assume @p291 (tptp.cC142xcomp tptp.iV21030)) % 0.40/0.91 (assume @p292 @t289) % 0.40/0.91 (assume @p293 (forall @t4 (=> @t290 @t192))) % 0.40/0.91 (assume @p294 @t291) % 0.40/0.91 (assume @p295 (tptp.cC52xcomp tptp.iV21030)) % 0.40/0.91 (assume @p296 (tptp.cC104xcomp tptp.iV21030)) % 0.40/0.91 (assume @p297 (tptp.cC2 tptp.iV21030)) % 0.40/0.91 (assume @p298 (forall @t4 (=> @t290 @t12))) % 0.40/0.91 (assume @p299 (tptp.cC26xcomp tptp.iV21030)) % 0.40/0.91 (assume @p300 (forall @t4 (=> @t290 @t96))) % 0.40/0.91 (assume @p301 (tptp.cC46xcomp tptp.iV21030)) % 0.40/0.91 (assume @p302 (tptp.cC126xcomp tptp.iV21030)) % 0.40/0.91 (assume @p303 (tptp.cC164xcomp tptp.iV21030)) % 0.40/0.91 (assume @p304 (forall @t4 (=> @t290 @t253))) % 0.40/0.91 (assume @p305 (tptp.cC100 tptp.iV21030)) % 0.40/0.91 (assume @p306 (tptp.cC160xcomp tptp.iV21030)) % 0.40/0.91 (assume @p307 @t292) % 0.40/0.91 (assume @p308 @t293) % 0.40/0.91 (assume @p309 (tptp.cC32xcomp tptp.iV21030)) % 0.40/0.91 (assume @p310 (tptp.rR1 tptp.iV21030 tptp.iV21032)) % 0.40/0.91 (assume @p311 (tptp.rR1 tptp.iV21030 tptp.iV21031)) % 0.40/0.91 (assume @p312 (tptp.cowlThing tptp.iV21031)) % 0.40/0.91 (assume @p313 (tptp.cC2xcomp tptp.iV21032)) % 0.40/0.91 (assume @p314 (tptp.cC92 tptp.iV21032)) % 0.40/0.91 (assume @p315 (tptp.cC100 tptp.iV21032)) % 0.40/0.91 (assume @p316 (tptp.cC6 tptp.iV21032)) % 0.40/0.91 (assume @p317 (tptp.cowlThing tptp.iV21032)) % 0.40/0.91 (assume @p318 (tptp.cC18 tptp.iV21032)) % 0.40/0.91 (assume @p319 (tptp.cC92 tptp.iV21033)) % 0.40/0.91 (assume @p320 @t294) % 0.40/0.91 (assume @p321 (tptp.cC100 tptp.iV21033)) % 0.40/0.91 (assume @p322 (tptp.cC6 tptp.iV21033)) % 0.40/0.91 (assume @p323 (tptp.cowlThing tptp.iV21033)) % 0.40/0.91 (assume @p324 (tptp.cC18 tptp.iV21033)) % 0.40/0.91 (assume @p325 (tptp.cC92 tptp.iV21034)) % 0.40/0.91 (assume @p326 (tptp.cC2xcomp tptp.iV21034)) % 0.40/0.91 (assume @p327 (tptp.cC100 tptp.iV21034)) % 0.40/0.91 (assume @p328 (tptp.cC6 tptp.iV21034)) % 0.40/0.91 (assume @p329 (tptp.cowlThing tptp.iV21034)) % 0.40/0.91 (assume @p330 (tptp.cC18 tptp.iV21034)) % 0.40/0.91 (assume @p331 (tptp.cC92 tptp.iV21035)) % 0.40/0.91 (assume @p332 (tptp.cC12xcomp tptp.iV21035)) % 0.40/0.91 (assume @p333 (tptp.cC100 tptp.iV21035)) % 0.40/0.91 (assume @p334 (tptp.cC6 tptp.iV21035)) % 0.40/0.91 (assume @p335 (tptp.cowlThing tptp.iV21035)) % 0.40/0.91 (assume @p336 (tptp.cC18 tptp.iV21035)) % 0.40/0.91 (assume @p337 (tptp.cC92 tptp.iV21036)) % 0.40/0.91 (assume @p338 (tptp.cC2xcomp tptp.iV21036)) % 0.40/0.91 (assume @p339 (tptp.cC100 tptp.iV21036)) % 0.40/0.91 (assume @p340 (tptp.cC6 tptp.iV21036)) % 0.40/0.91 (assume @p341 (tptp.cowlThing tptp.iV21036)) % 0.40/0.91 (assume @p342 (tptp.cC18 tptp.iV21036)) % 0.40/0.91 (assume @p343 @t342) % 0.40/0.91 (assume @p344 true) % 0.40/0.91 (step @p345 :rule alpha_equiv :args (@t343 @t344 (@list @t345))) % 0.40/0.91 (step @p346 :rule alpha_equiv :args (@t346 @t344 (@list @t347))) % 0.40/0.91 (step @p347 :rule nary_cong :premises (@p346 @p345) :args (@t348)) % 0.40/0.91 (step @p348 :rule quant-miniscope-and :args ((= @t5 @t348))) % 0.40/0.91 (step @p349 :rule trans :premises (@p348 @p347)) % 0.40/0.91 (step @p350 :rule eq_resolve :premises (@p1 @p349)) % 0.40/0.91 (step @p351 :rule and_elim :premises (@p350) :args (0)) % 0.40/0.91 (step @p352 :rule and_elim :premises (@p350) :args (1)) % 0.40/0.91 (step @p353 :rule exists-elim :args ((= @t198 (not (forall @t11 (not @t197)))))) % 0.40/0.91 (step @p354 :rule refl :args (@t199)) % 0.40/0.91 (step @p355 :rule cong :premises (@p354 @p353) :args (@t200)) % 0.40/0.91 (step @p356 :rule cong :premises (@p355) :args (@t201)) % 0.40/0.91 (step @p357 :rule eq_resolve :premises (@p150 @p356)) % 0.40/0.91 (step @p358 :rule instantiate :premises (@p357) :args (@t349)) % 0.40/0.91 (step @p359 :rule bool-double-not-elim :args (@t350)) % 0.40/0.91 (step @p360 :rule exists-elim :args ((= @t203 (not @t350)))) % 0.40/0.91 (step @p361 :rule cong :premises (@p360) :args (@t204)) % 0.40/0.91 (step @p362 :rule trans :premises (@p361 @p359)) % 0.40/0.91 (step @p363 :rule refl :args (@t205)) % 0.40/0.91 (step @p364 :rule cong :premises (@p363 @p362) :args (@t206)) % 0.40/0.91 (step @p365 :rule cong :premises (@p364) :args (@t207)) % 0.40/0.91 (step @p366 :rule eq_resolve :premises (@p152 @p365)) % 0.40/0.91 (step @p367 :rule instantiate :premises (@p366) :args (@t349)) % 0.40/0.91 (step @p368 :rule instantiate :premises (@p154) :args (@t349)) % 0.40/0.91 (step @p369 :rule bool-double-not-elim :args (@t351)) % 0.40/0.91 (step @p370 :rule exists-elim :args ((= @t209 (not @t351)))) % 0.40/0.91 (step @p371 :rule cong :premises (@p370) :args (@t210)) % 0.40/0.91 (step @p372 :rule trans :premises (@p371 @p369)) % 0.40/0.91 (step @p373 :rule refl :args (@t211)) % 0.40/0.91 (step @p374 :rule cong :premises (@p373 @p372) :args (@t212)) % 0.40/0.91 (step @p375 :rule cong :premises (@p374) :args (@t213)) % 0.40/0.91 (step @p376 :rule eq_resolve :premises (@p153 @p375)) % 0.40/0.91 (step @p377 :rule instantiate :premises (@p376) :args (@t349)) % 0.40/0.91 (step @p378 :rule exists-elim :args ((= @t215 (not (forall @t11 (not @t214)))))) % 0.40/0.91 (step @p379 :rule refl :args (@t216)) % 0.40/0.91 (step @p380 :rule cong :premises (@p379 @p378) :args (@t217)) % 0.40/0.91 (step @p381 :rule cong :premises (@p380) :args (@t218)) % 0.40/0.91 (step @p382 :rule eq_resolve :premises (@p155 @p381)) % 0.40/0.91 (step @p383 :rule instantiate :premises (@p382) :args (@t349)) % 0.40/0.91 (step @p384 :rule cnf_equiv_pos1 :args (@t354)) % 0.40/0.91 (step @p385 :rule reordering :premises (@p384) :args ((or (not @t289) @t353 (not @t354)))) % 0.40/0.91 (step @p386 :rule chain_m_resolution :premises (@p385 @p292 @p383) :args (@t353 @t355 (@list @t289 @t354))) % 0.40/0.91 (step @p387 :rule alpha_equiv :args (@t352 @t356 @t357)) % 0.40/0.91 (step @p388 :rule equiv_elim2 :premises (@p387)) % 0.40/0.91 (step @p389 :rule chain_m_resolution :premises (@p388 @p386) :args ((not @t358) @t359 (@list @t352))) % 0.40/0.91 (step @p390 :rule cnf_equiv_pos1 :args (@t361)) % 0.40/0.91 (step @p391 :rule reordering :premises (@p390) :args ((or @t362 @t358 (not @t361)))) % 0.40/0.91 (step @p392 :rule chain_m_resolution :premises (@p391 @p389 @p377) :args (@t362 @t363 (@list @t358 @t361))) % 0.40/0.91 (step @p393 :rule cnf_equiv_pos2 :args (@t366)) % 0.40/0.91 (step @p394 :rule reordering :premises (@p393) :args ((or @t360 @t367 (not @t366)))) % 0.40/0.91 (step @p395 :rule chain_m_resolution :premises (@p394 @p392 @p368) :args (@t367 @t363 (@list @t360 @t366))) % 0.40/0.91 (step @p396 :rule cnf_and_neg :args (@t365)) % 0.40/0.91 (step @p397 :rule reordering :premises (@p396) :args ((or @t369 @t365 @t368))) % 0.40/0.91 (step @p398 :rule chain_m_resolution :premises (@p397 @p294 @p395) :args (@t368 @t370 (@list @t291 @t365))) % 0.40/0.91 (step @p399 :rule cnf_equiv_pos2 :args (@t372)) % 0.40/0.91 (step @p400 :rule reordering :premises (@p399) :args ((or @t364 @t373 (not @t372)))) % 0.40/0.91 (step @p401 :rule chain_m_resolution :premises (@p400 @p398 @p367) :args (@t373 @t363 (@list @t364 @t372))) % 0.40/0.91 (step @p402 :rule alpha_equiv :args (@t374 @t356 @t357)) % 0.40/0.91 (step @p403 :rule equiv_elim1 :premises (@p402)) % 0.40/0.91 (step @p404 :rule chain_m_resolution :premises (@p403 @p401) :args (@t375 @t359 (@list @t371))) % 0.40/0.91 (step @p405 :rule bool-double-not-elim :args (@t374)) % 0.40/0.91 (step @p406 :rule refl :args (@t295)) % 0.40/0.91 (step @p407 :rule refl :args (@t377)) % 0.40/0.91 (step @p408 :rule nary_cong :premises (@p407 @p406 @p405) :args ((or @t377 @t295 (not @t375)))) % 0.40/0.91 (step @p409 :rule cnf_equiv_pos2 :args (@t376)) % 0.40/0.91 (step @p410 :rule eq_resolve :premises (@p409 @p408)) % 0.40/0.91 (step @p411 :rule reordering :premises (@p410) :args ((or @t295 @t374 @t377))) % 0.40/0.91 (step @p412 :rule chain_m_resolution :premises (@p411 @p404 @p358) :args (@t295 @t363 (@list @t374 @t376))) % 0.40/0.91 (step @p413 :rule exists-elim :args ((= @t222 (not (forall @t11 (not @t221)))))) % 0.40/0.91 (step @p414 :rule refl :args (@t223)) % 0.40/0.91 (step @p415 :rule cong :premises (@p414 @p413) :args (@t224)) % 0.40/0.91 (step @p416 :rule cong :premises (@p415) :args (@t225)) % 0.40/0.91 (step @p417 :rule eq_resolve :premises (@p159 @p416)) % 0.40/0.91 (step @p418 :rule instantiate :premises (@p417) :args (@t349)) % 0.40/0.91 (step @p419 :rule bool-double-not-elim :args (@t378)) % 0.40/0.91 (step @p420 :rule exists-elim :args ((= @t227 (not @t378)))) % 0.40/0.91 (step @p421 :rule cong :premises (@p420) :args (@t228)) % 0.40/0.91 (step @p422 :rule trans :premises (@p421 @p419)) % 0.40/0.91 (step @p423 :rule refl :args (@t229)) % 0.40/0.91 (step @p424 :rule cong :premises (@p423 @p422) :args (@t230)) % 0.40/0.91 (step @p425 :rule cong :premises (@p424) :args (@t231)) % 0.40/0.91 (step @p426 :rule eq_resolve :premises (@p161 @p425)) % 0.40/0.91 (step @p427 :rule instantiate :premises (@p426) :args (@t349)) % 0.40/0.91 (step @p428 :rule instantiate :premises (@p162) :args (@t349)) % 0.40/0.91 (step @p429 :rule exists-elim :args ((= @t234 (not (forall @t11 (not @t233)))))) % 0.40/0.91 (step @p430 :rule refl :args (@t232)) % 0.40/0.91 (step @p431 :rule cong :premises (@p430 @p429) :args (@t235)) % 0.40/0.91 (step @p432 :rule cong :premises (@p431) :args (@t236)) % 0.40/0.91 (step @p433 :rule eq_resolve :premises (@p163 @p432)) % 0.40/0.91 (step @p434 :rule instantiate :premises (@p433) :args (@t349)) % 0.40/0.91 (step @p435 :rule bool-double-not-elim :args (@t379)) % 0.40/0.91 (step @p436 :rule exists-elim :args ((= @t238 (not @t379)))) % 0.40/0.91 (step @p437 :rule cong :premises (@p436) :args (@t239)) % 0.40/0.91 (step @p438 :rule trans :premises (@p437 @p435)) % 0.40/0.91 (step @p439 :rule refl :args (@t240)) % 0.40/0.91 (step @p440 :rule cong :premises (@p439 @p438) :args (@t241)) % 0.40/0.91 (step @p441 :rule cong :premises (@p440) :args (@t242)) % 0.40/0.91 (step @p442 :rule eq_resolve :premises (@p164 @p441)) % 0.40/0.91 (step @p443 :rule instantiate :premises (@p442) :args (@t349)) % 0.40/0.91 (step @p444 :rule cnf_equiv_pos1 :args (@t381)) % 0.40/0.91 (step @p445 :rule reordering :premises (@p444) :args ((or (not @t293) @t380 (not @t381)))) % 0.40/0.91 (step @p446 :rule chain_m_resolution :premises (@p445 @p308 @p443) :args (@t380 @t355 (@list @t293 @t381))) % 0.40/0.91 (step @p447 :rule alpha_equiv :args (@t380 @t357 @t356)) % 0.40/0.91 (step @p448 :rule equiv_elim1 :premises (@p447)) % 0.40/0.91 (step @p449 :rule chain_m_resolution :premises (@p448 @p446) :args (@t382 @t383 (@list @t380))) % 0.40/0.91 (step @p450 :rule cnf_equiv_pos1 :args (@t386)) % 0.40/0.91 (step @p451 :rule reordering :premises (@p450) :args ((or @t387 @t384 (not @t386)))) % 0.40/0.91 (step @p452 :rule chain_m_resolution :premises (@p451 @p449 @p434) :args (@t387 @t355 (@list @t382 @t386))) % 0.40/0.91 (step @p453 :rule cnf_equiv_pos2 :args (@t390)) % 0.40/0.91 (step @p454 :rule reordering :premises (@p453) :args ((or @t385 @t391 (not @t390)))) % 0.40/0.91 (step @p455 :rule chain_m_resolution :premises (@p454 @p452 @p428) :args (@t391 @t363 (@list @t385 @t390))) % 0.40/0.91 (step @p456 :rule cnf_and_neg :args (@t389)) % 0.40/0.91 (step @p457 :rule reordering :premises (@p456) :args ((or @t369 @t389 @t392))) % 0.40/0.91 (step @p458 :rule chain_m_resolution :premises (@p457 @p294 @p455) :args (@t392 @t370 (@list @t291 @t389))) % 0.40/0.91 (step @p459 :rule cnf_equiv_pos2 :args (@t394)) % 0.40/0.91 (step @p460 :rule reordering :premises (@p459) :args ((or @t388 @t395 (not @t394)))) % 0.40/0.91 (step @p461 :rule chain_m_resolution :premises (@p460 @p458 @p427) :args (@t395 @t363 (@list @t388 @t394))) % 0.40/0.91 (step @p462 :rule alpha_equiv :args (@t396 @t356 @t357)) % 0.40/0.91 (step @p463 :rule equiv_elim1 :premises (@p462)) % 0.40/0.91 (step @p464 :rule chain_m_resolution :premises (@p463 @p461) :args (@t397 @t359 (@list @t393))) % 0.40/0.91 (step @p465 :rule bool-double-not-elim :args (@t396)) % 0.40/0.91 (step @p466 :rule refl :args (@t296)) % 0.40/0.91 (step @p467 :rule refl :args (@t399)) % 0.40/0.91 (step @p468 :rule nary_cong :premises (@p467 @p466 @p465) :args ((or @t399 @t296 (not @t397)))) % 0.40/0.91 (step @p469 :rule cnf_equiv_pos2 :args (@t398)) % 0.40/0.91 (step @p470 :rule eq_resolve :premises (@p469 @p468)) % 0.40/0.91 (step @p471 :rule reordering :premises (@p470) :args ((or @t296 @t396 @t399))) % 0.40/0.91 (step @p472 :rule chain_m_resolution :premises (@p471 @p464 @p418) :args (@t296 @t363 (@list @t396 @t398))) % 0.40/0.91 (step @p473 :rule bool-double-not-elim :args (@t400)) % 0.40/0.91 (step @p474 :rule exists-elim :args ((= @t160 (not @t400)))) % 0.40/0.91 (step @p475 :rule cong :premises (@p474) :args (@t161)) % 0.40/0.91 (step @p476 :rule trans :premises (@p475 @p473)) % 0.40/0.91 (step @p477 :rule refl :args (@t162)) % 0.40/0.91 (step @p478 :rule cong :premises (@p477 @p476) :args (@t163)) % 0.40/0.91 (step @p479 :rule cong :premises (@p478) :args (@t164)) % 0.40/0.91 (step @p480 :rule eq_resolve :premises (@p125 @p479)) % 0.40/0.91 (step @p481 :rule instantiate :premises (@p480) :args (@t401)) % 0.40/0.91 (step @p482 :rule exists-elim :args ((= @t166 (not (forall @t11 (not @t165)))))) % 0.40/0.91 (step @p483 :rule refl :args (@t167)) % 0.40/0.91 (step @p484 :rule cong :premises (@p483 @p482) :args (@t168)) % 0.40/0.91 (step @p485 :rule cong :premises (@p484) :args (@t169)) % 0.40/0.91 (step @p486 :rule eq_resolve :premises (@p127 @p485)) % 0.40/0.91 (step @p487 :rule instantiate :premises (@p486) :args (@t401)) % 0.40/0.91 (step @p488 :rule instantiate :premises (@p129) :args (@t401)) % 0.40/0.91 (step @p489 :rule exists-elim :args ((= @t171 (not (forall @t11 (not @t170)))))) % 0.40/0.91 (step @p490 :rule refl :args (@t172)) % 0.40/0.91 (step @p491 :rule cong :premises (@p490 @p489) :args (@t173)) % 0.40/0.91 (step @p492 :rule cong :premises (@p491) :args (@t174)) % 0.40/0.91 (step @p493 :rule eq_resolve :premises (@p128 @p492)) % 0.40/0.91 (step @p494 :rule instantiate :premises (@p493) :args (@t401)) % 0.40/0.91 (step @p495 :rule bool-double-not-elim :args (@t402)) % 0.40/0.91 (step @p496 :rule exists-elim :args ((= @t176 (not @t402)))) % 0.40/0.91 (step @p497 :rule cong :premises (@p496) :args (@t177)) % 0.40/0.91 (step @p498 :rule trans :premises (@p497 @p495)) % 0.40/0.91 (step @p499 :rule refl :args (@t178)) % 0.40/0.91 (step @p500 :rule cong :premises (@p499 @p498) :args (@t179)) % 0.40/0.91 (step @p501 :rule cong :premises (@p500) :args (@t180)) % 0.40/0.91 (step @p502 :rule eq_resolve :premises (@p130 @p501)) % 0.40/0.91 (step @p503 :rule instantiate :premises (@p502) :args (@t401)) % 0.40/0.91 (step @p504 :rule cnf_equiv_pos1 :args (@t404)) % 0.40/0.91 (step @p505 :rule reordering :premises (@p504) :args ((or (not @t286) @t403 (not @t404)))) % 0.40/0.91 (step @p506 :rule chain_m_resolution :premises (@p505 @p273 @p503) :args (@t403 @t355 (@list @t286 @t404))) % 0.40/0.91 (step @p507 :rule alpha_equiv :args (@t403 @t357 @t356)) % 0.40/0.91 (step @p508 :rule equiv_elim1 :premises (@p507)) % 0.40/0.91 (step @p509 :rule chain_m_resolution :premises (@p508 @p506) :args (@t405 @t383 (@list @t403))) % 0.40/0.91 (step @p510 :rule cnf_equiv_pos1 :args (@t408)) % 0.40/0.91 (step @p511 :rule reordering :premises (@p510) :args ((or @t409 @t406 (not @t408)))) % 0.40/0.91 (step @p512 :rule chain_m_resolution :premises (@p511 @p509 @p494) :args (@t409 @t355 (@list @t405 @t408))) % 0.40/0.91 (step @p513 :rule cnf_equiv_pos2 :args (@t412)) % 0.40/0.91 (step @p514 :rule reordering :premises (@p513) :args ((or @t407 @t413 (not @t412)))) % 0.40/0.91 (step @p515 :rule chain_m_resolution :premises (@p514 @p512 @p488) :args (@t413 @t363 (@list @t407 @t412))) % 0.40/0.91 (step @p516 :rule cnf_and_neg :args (@t411)) % 0.40/0.91 (step @p517 :rule reordering :premises (@p516) :args ((or (not @t285) @t411 @t414))) % 0.40/0.91 (step @p518 :rule chain_m_resolution :premises (@p517 @p266 @p515) :args (@t414 @t370 (@list @t285 @t411))) % 0.40/0.91 (step @p519 :rule bool-double-not-elim :args (@t415)) % 0.40/0.91 (step @p520 :rule refl :args (@t410)) % 0.40/0.91 (step @p521 :rule refl :args (@t418)) % 0.40/0.91 (step @p522 :rule nary_cong :premises (@p521 @p520 @p519) :args ((or @t418 @t410 (not @t416)))) % 0.40/0.91 (step @p523 :rule cnf_equiv_pos2 :args (@t417)) % 0.40/0.91 (step @p524 :rule eq_resolve :premises (@p523 @p522)) % 0.40/0.91 (step @p525 :rule reordering :premises (@p524) :args ((or @t410 @t415 @t418))) % 0.40/0.91 (step @p526 :rule chain_m_resolution :premises (@p525 @p518 @p487) :args (@t415 @t363 (@list @t410 @t417))) % 0.40/0.91 (step @p527 :rule alpha_equiv :args (@t419 @t357 @t356)) % 0.40/0.91 (step @p528 :rule equiv_elim2 :premises (@p527)) % 0.40/0.91 (step @p529 :rule chain_m_resolution :premises (@p528 @p526) :args (@t419 @t383 (@list @t415))) % 0.40/0.91 (step @p530 :rule cnf_equiv_pos2 :args (@t420)) % 0.40/0.91 (step @p531 :rule reordering :premises (@p530) :args ((or @t297 (not @t419) (not @t420)))) % 0.40/0.91 (step @p532 :rule chain_m_resolution :premises (@p531 @p529 @p481) :args (@t297 @t355 (@list @t419 @t420))) % 0.40/0.91 (step @p533 :rule eq-symm :args ((not (forall @t14 (or (not @t17) @t421))) @t183)) % 0.40/0.91 (step @p534 :rule refl :args (@t183)) % 0.40/0.91 (step @p535 :rule bool-and-de-morgan :args (@t17 @t54 true)) % 0.40/0.91 (step @p536 :rule cong :premises (@p535) :args (@t422)) % 0.40/0.91 (step @p537 :rule cong :premises (@p536) :args (@t423)) % 0.40/0.91 (step @p538 :rule exists-elim :args ((= @t56 @t423))) % 0.40/0.91 (step @p539 :rule trans :premises (@p538 @p537)) % 0.40/0.91 (step @p540 :rule cong :premises (@p539 @p534) :args ((= @t56 @t183))) % 0.40/0.91 (step @p541 :rule trans :premises (@p540 @p533)) % 0.40/0.91 (step @p542 :rule eq-symm :args (@t183 @t56)) % 0.40/0.91 (step @p543 :rule trans :premises (@p542 @p541)) % 0.40/0.91 (step @p544 :rule cong :premises (@p543) :args (@t184)) % 0.40/0.91 (step @p545 :rule eq_resolve :premises (@p134 @p544)) % 0.40/0.91 (step @p546 :rule instantiate :premises (@p545) :args (@t401)) % 0.40/0.91 (step @p547 :rule cnf_or_pos :args (@t426)) % 0.40/0.91 (step @p548 :rule reordering :premises (@p547) :args ((or @t425 @t424 @t427))) % 0.40/0.91 (step @p549 :rule chain_m_resolution :premises (@p548 @p283 @p320) :args (@t427 @t355 (@list @t288 @t294))) % 0.40/0.91 (assume-push @p1021 @t428) % 0.40/0.91 (step @p551 :rule instantiate :premises (@p1021) :args ((@list tptp.iV21033))) % 0.40/0.91 (step-pop @p1022 :rule scope :premises (@p551)) % 0.40/0.91 (step @p552 :rule process_scope :premises (@p1022) :args (@t426)) % 0.40/0.91 (step @p554 :rule implies_elim :premises (@p552)) % 0.40/0.91 (step @p555 :rule chain_m_resolution :premises (@p554 @p549) :args (@t429 @t359 (@list @t426))) % 0.40/0.91 (step @p556 :rule bool-double-not-elim :args (@t428)) % 0.40/0.91 (step @p557 :rule refl :args (@t298)) % 0.40/0.91 (step @p558 :rule refl :args (@t431)) % 0.40/0.91 (step @p559 :rule nary_cong :premises (@p558 @p557 @p556) :args ((or @t431 @t298 (not @t429)))) % 0.40/0.91 (step @p560 :rule cnf_equiv_pos2 :args (@t430)) % 0.40/0.91 (step @p561 :rule eq_resolve :premises (@p560 @p559)) % 0.40/0.91 (step @p562 :rule reordering :premises (@p561) :args ((or @t298 @t428 @t431))) % 0.40/0.91 (step @p563 :rule chain_m_resolution :premises (@p562 @p555 @p546) :args (@t298 @t363 (@list @t428 @t430))) % 0.40/0.91 (step @p564 :rule exists-elim :args ((= @t102 (not (forall @t11 (not @t101)))))) % 0.40/0.91 (step @p565 :rule refl :args (@t103)) % 0.40/0.91 (step @p566 :rule cong :premises (@p565 @p564) :args (@t104)) % 0.40/0.91 (step @p567 :rule cong :premises (@p566) :args (@t105)) % 0.40/0.91 (step @p568 :rule eq_resolve :premises (@p102 @p567)) % 0.40/0.91 (step @p569 :rule instantiate :premises (@p568) :args (@t432)) % 0.40/0.91 (step @p570 :rule bool-double-not-elim :args (@t433)) % 0.40/0.91 (step @p571 :rule exists-elim :args ((= @t110 (not @t433)))) % 0.40/0.91 (step @p572 :rule cong :premises (@p571) :args (@t111)) % 0.40/0.91 (step @p573 :rule trans :premises (@p572 @p570)) % 0.40/0.91 (step @p574 :rule refl :args (@t112)) % 0.40/0.91 (step @p575 :rule cong :premises (@p574 @p573) :args (@t113)) % 0.40/0.91 (step @p576 :rule cong :premises (@p575) :args (@t114)) % 0.40/0.91 (step @p577 :rule eq_resolve :premises (@p104 @p576)) % 0.40/0.91 (step @p578 :rule instantiate :premises (@p577) :args (@t432)) % 0.40/0.91 (step @p579 :rule instantiate :premises (@p106) :args (@t432)) % 0.40/0.91 (step @p580 :rule exists-elim :args ((= @t116 (not (forall @t11 (not @t115)))))) % 0.40/0.91 (step @p581 :rule refl :args (@t117)) % 0.40/0.91 (step @p582 :rule cong :premises (@p581 @p580) :args (@t118)) % 0.40/0.91 (step @p583 :rule cong :premises (@p582) :args (@t119)) % 0.40/0.91 (step @p584 :rule eq_resolve :premises (@p105 @p583)) % 0.40/0.91 (step @p585 :rule instantiate :premises (@p584) :args (@t432)) % 0.40/0.91 (step @p586 :rule bool-double-not-elim :args (@t434)) % 0.40/0.91 (step @p587 :rule exists-elim :args ((= @t121 (not @t434)))) % 0.40/0.91 (step @p588 :rule cong :premises (@p587) :args (@t122)) % 0.40/0.91 (step @p589 :rule trans :premises (@p588 @p586)) % 0.40/0.91 (step @p590 :rule refl :args (@t123)) % 0.40/0.91 (step @p591 :rule cong :premises (@p590 @p589) :args (@t124)) % 0.40/0.91 (step @p592 :rule cong :premises (@p591) :args (@t125)) % 0.40/0.91 (step @p593 :rule eq_resolve :premises (@p107 @p592)) % 0.40/0.91 (step @p594 :rule instantiate :premises (@p593) :args (@t432)) % 0.40/0.91 (step @p595 :rule cnf_equiv_pos1 :args (@t436)) % 0.40/0.91 (step @p596 :rule reordering :premises (@p595) :args ((or (not @t281) @t435 (not @t436)))) % 0.40/0.91 (step @p597 :rule chain_m_resolution :premises (@p596 @p243 @p594) :args (@t435 @t355 (@list @t281 @t436))) % 0.40/0.91 (step @p598 :rule alpha_equiv :args (@t435 @t357 @t356)) % 0.40/0.91 (step @p599 :rule equiv_elim1 :premises (@p598)) % 0.40/0.91 (step @p600 :rule chain_m_resolution :premises (@p599 @p597) :args (@t437 @t383 (@list @t435))) % 0.40/0.91 (step @p601 :rule cnf_equiv_pos1 :args (@t440)) % 0.40/0.91 (step @p602 :rule reordering :premises (@p601) :args ((or @t441 @t438 (not @t440)))) % 0.40/0.91 (step @p603 :rule chain_m_resolution :premises (@p602 @p600 @p585) :args (@t441 @t355 (@list @t437 @t440))) % 0.40/0.91 (step @p604 :rule cnf_equiv_pos2 :args (@t444)) % 0.40/0.91 (step @p605 :rule reordering :premises (@p604) :args ((or @t439 @t445 (not @t444)))) % 0.40/0.91 (step @p606 :rule chain_m_resolution :premises (@p605 @p603 @p579) :args (@t445 @t363 (@list @t439 @t444))) % 0.40/0.91 (step @p607 :rule cnf_and_neg :args (@t443)) % 0.40/0.91 (step @p608 :rule reordering :premises (@p607) :args ((or @t447 @t443 @t446))) % 0.40/0.91 (step @p609 :rule chain_m_resolution :premises (@p608 @p238 @p606) :args (@t446 @t370 (@list @t280 @t443))) % 0.40/0.91 (step @p610 :rule cnf_equiv_pos2 :args (@t449)) % 0.40/0.91 (step @p611 :rule reordering :premises (@p610) :args ((or @t442 @t450 (not @t449)))) % 0.40/0.91 (step @p612 :rule chain_m_resolution :premises (@p611 @p609 @p578) :args (@t450 @t363 (@list @t442 @t449))) % 0.40/0.91 (step @p613 :rule alpha_equiv :args (@t451 @t356 @t357)) % 0.40/0.91 (step @p614 :rule equiv_elim1 :premises (@p613)) % 0.40/0.91 (step @p615 :rule chain_m_resolution :premises (@p614 @p612) :args (@t452 @t359 (@list @t448))) % 0.40/0.91 (step @p616 :rule bool-double-not-elim :args (@t451)) % 0.40/0.91 (step @p617 :rule refl :args (@t299)) % 0.40/0.91 (step @p618 :rule refl :args (@t454)) % 0.40/0.91 (step @p619 :rule nary_cong :premises (@p618 @p617 @p616) :args ((or @t454 @t299 (not @t452)))) % 0.40/0.91 (step @p620 :rule cnf_equiv_pos2 :args (@t453)) % 0.40/0.91 (step @p621 :rule eq_resolve :premises (@p620 @p619)) % 0.40/0.91 (step @p622 :rule reordering :premises (@p621) :args ((or @t299 @t451 @t454))) % 0.40/0.91 (step @p623 :rule chain_m_resolution :premises (@p622 @p615 @p569) :args (@t299 @t363 (@list @t451 @t453))) % 0.40/0.91 (step @p624 :rule exists-elim :args ((= @t129 (not (forall @t11 (not @t128)))))) % 0.40/0.91 (step @p625 :rule refl :args (@t130)) % 0.40/0.91 (step @p626 :rule cong :premises (@p625 @p624) :args (@t131)) % 0.40/0.91 (step @p627 :rule cong :premises (@p626) :args (@t132)) % 0.40/0.91 (step @p628 :rule eq_resolve :premises (@p111 @p627)) % 0.40/0.91 (step @p629 :rule instantiate :premises (@p628) :args (@t432)) % 0.40/0.91 (step @p630 :rule bool-double-not-elim :args (@t455)) % 0.40/0.91 (step @p631 :rule exists-elim :args ((= @t134 (not @t455)))) % 0.40/0.91 (step @p632 :rule cong :premises (@p631) :args (@t135)) % 0.40/0.91 (step @p633 :rule trans :premises (@p632 @p630)) % 0.40/0.91 (step @p634 :rule refl :args (@t136)) % 0.40/0.91 (step @p635 :rule cong :premises (@p634 @p633) :args (@t137)) % 0.40/0.91 (step @p636 :rule cong :premises (@p635) :args (@t138)) % 0.40/0.91 (step @p637 :rule eq_resolve :premises (@p113 @p636)) % 0.40/0.91 (step @p638 :rule instantiate :premises (@p637) :args (@t432)) % 0.40/0.91 (step @p639 :rule instantiate :premises (@p115) :args (@t432)) % 0.40/0.91 (step @p640 :rule bool-double-not-elim :args (@t456)) % 0.40/0.91 (step @p641 :rule exists-elim :args ((= @t140 (not @t456)))) % 0.40/0.91 (step @p642 :rule cong :premises (@p641) :args (@t141)) % 0.40/0.91 (step @p643 :rule trans :premises (@p642 @p640)) % 0.40/0.91 (step @p644 :rule refl :args (@t142)) % 0.40/0.91 (step @p645 :rule cong :premises (@p644 @p643) :args (@t143)) % 0.40/0.91 (step @p646 :rule cong :premises (@p645) :args (@t144)) % 0.40/0.91 (step @p647 :rule eq_resolve :premises (@p114 @p646)) % 0.40/0.91 (step @p648 :rule instantiate :premises (@p647) :args (@t432)) % 0.40/0.91 (step @p649 :rule exists-elim :args ((= @t146 (not (forall @t11 (not @t145)))))) % 0.40/0.91 (step @p650 :rule refl :args (@t147)) % 0.40/0.91 (step @p651 :rule cong :premises (@p650 @p649) :args (@t148)) % 0.40/0.91 (step @p652 :rule cong :premises (@p651) :args (@t149)) % 0.40/0.91 (step @p653 :rule eq_resolve :premises (@p116 @p652)) % 0.40/0.91 (step @p654 :rule instantiate :premises (@p653) :args (@t432)) % 0.40/0.91 (step @p655 :rule cnf_equiv_pos1 :args (@t459)) % 0.40/0.91 (step @p656 :rule reordering :premises (@p655) :args ((or (not @t283) @t458 (not @t459)))) % 0.40/0.91 (step @p657 :rule chain_m_resolution :premises (@p656 @p251 @p654) :args (@t458 @t355 (@list @t283 @t459))) % 0.40/0.91 (step @p658 :rule alpha_equiv :args (@t457 @t356 @t357)) % 0.40/0.91 (step @p659 :rule equiv_elim2 :premises (@p658)) % 0.40/0.91 (step @p660 :rule chain_m_resolution :premises (@p659 @p657) :args ((not @t460) @t359 (@list @t457))) % 0.40/0.91 (step @p661 :rule cnf_equiv_pos1 :args (@t462)) % 0.40/0.91 (step @p662 :rule reordering :premises (@p661) :args ((or @t463 @t460 (not @t462)))) % 0.40/0.91 (step @p663 :rule chain_m_resolution :premises (@p662 @p660 @p648) :args (@t463 @t363 (@list @t460 @t462))) % 0.40/0.91 (step @p664 :rule cnf_equiv_pos2 :args (@t466)) % 0.40/0.91 (step @p665 :rule reordering :premises (@p664) :args ((or @t461 @t467 (not @t466)))) % 0.40/0.91 (step @p666 :rule chain_m_resolution :premises (@p665 @p663 @p639) :args (@t467 @t363 (@list @t461 @t466))) % 0.40/0.91 (step @p667 :rule cnf_and_neg :args (@t465)) % 0.40/0.91 (step @p668 :rule reordering :premises (@p667) :args ((or @t447 @t465 @t468))) % 0.40/0.91 (step @p669 :rule chain_m_resolution :premises (@p668 @p238 @p666) :args (@t468 @t370 (@list @t280 @t465))) % 0.40/0.91 (step @p670 :rule cnf_equiv_pos2 :args (@t470)) % 0.40/0.91 (step @p671 :rule reordering :premises (@p670) :args ((or @t464 @t471 (not @t470)))) % 0.40/0.91 (step @p672 :rule chain_m_resolution :premises (@p671 @p669 @p638) :args (@t471 @t363 (@list @t464 @t470))) % 0.40/0.91 (step @p673 :rule alpha_equiv :args (@t472 @t356 @t357)) % 0.40/0.91 (step @p674 :rule equiv_elim1 :premises (@p673)) % 0.40/0.91 (step @p675 :rule chain_m_resolution :premises (@p674 @p672) :args (@t473 @t359 (@list @t469))) % 0.40/0.91 (step @p676 :rule bool-double-not-elim :args (@t472)) % 0.40/0.91 (step @p677 :rule refl :args (@t300)) % 0.40/0.91 (step @p678 :rule refl :args (@t475)) % 0.40/0.91 (step @p679 :rule nary_cong :premises (@p678 @p677 @p676) :args ((or @t475 @t300 (not @t473)))) % 0.40/0.91 (step @p680 :rule cnf_equiv_pos2 :args (@t474)) % 0.40/0.91 (step @p681 :rule eq_resolve :premises (@p680 @p679)) % 0.40/0.91 (step @p682 :rule reordering :premises (@p681) :args ((or @t300 @t472 @t475))) % 0.40/0.91 (step @p683 :rule chain_m_resolution :premises (@p682 @p675 @p629) :args (@t300 @t363 (@list @t472 @t474))) % 0.40/0.91 (step @p684 :rule instantiate :premises (@p19) :args (@t476)) % 0.40/0.91 (step @p685 :rule instantiate :premises (@p42) :args (@t476)) % 0.40/0.91 (step @p686 :rule instantiate :premises (@p44) :args (@t476)) % 0.40/0.91 (step @p687 :rule instantiate :premises (@p66) :args (@t476)) % 0.40/0.91 (step @p688 :rule instantiate :premises (@p67) :args (@t476)) % 0.40/0.91 (step @p689 :rule instantiate :premises (@p187) :args (@t476)) % 0.40/0.91 (step @p690 :rule cnf_equiv_pos1 :args (@t478)) % 0.40/0.91 (step @p691 :rule reordering :premises (@p690) :args ((or (not @t277) @t477 (not @t478)))) % 0.40/0.91 (step @p692 :rule chain_m_resolution :premises (@p691 @p222 @p689) :args (@t477 @t355 (@list @t277 @t478))) % 0.40/0.91 (step @p693 :rule cnf_and_pos :args (@t477 0)) % 0.40/0.91 (step @p694 :rule reordering :premises (@p693) :args ((or @t333 @t479))) % 0.40/0.91 (step @p695 :rule chain_m_resolution :premises (@p694 @p692) :args (@t333 @t383 @t480)) % 0.40/0.91 (step @p696 :rule cnf_equiv_pos1 :args (@t482)) % 0.40/0.91 (step @p697 :rule reordering :premises (@p696) :args ((or @t483 @t481 (not @t482)))) % 0.40/0.91 (step @p698 :rule chain_m_resolution :premises (@p697 @p695 @p688) :args (@t481 @t355 (@list @t333 @t482))) % 0.40/0.91 (step @p699 :rule cnf_and_pos :args (@t481 1)) % 0.40/0.91 (step @p700 :rule reordering :premises (@p699) :args ((or @t302 @t484))) % 0.40/0.91 (step @p701 :rule chain_m_resolution :premises (@p700 @p698) :args (@t302 @t383 @t485)) % 0.40/0.91 (step @p702 :rule cnf_equiv_pos1 :args (@t487)) % 0.40/0.91 (step @p703 :rule reordering :premises (@p702) :args ((or @t488 @t486 (not @t487)))) % 0.40/0.91 (step @p704 :rule chain_m_resolution :premises (@p703 @p701 @p687) :args (@t486 @t355 (@list @t302 @t487))) % 0.40/0.91 (step @p705 :rule cnf_and_pos :args (@t486 1)) % 0.40/0.91 (step @p706 :rule reordering :premises (@p705) :args ((or @t320 (not @t486)))) % 0.40/0.91 (step @p707 :rule chain_m_resolution :premises (@p706 @p704) :args (@t320 @t383 (@list @t486))) % 0.40/0.91 (step @p708 :rule cnf_equiv_pos1 :args (@t490)) % 0.40/0.91 (step @p709 :rule reordering :premises (@p708) :args ((or @t491 @t489 (not @t490)))) % 0.40/0.91 (step @p710 :rule chain_m_resolution :premises (@p709 @p707 @p686) :args (@t489 @t355 (@list @t320 @t490))) % 0.40/0.91 (step @p711 :rule cnf_and_pos :args (@t489 1)) % 0.40/0.91 (step @p712 :rule reordering :premises (@p711) :args ((or @t304 (not @t489)))) % 0.40/0.91 (step @p713 :rule chain_m_resolution :premises (@p712 @p710) :args (@t304 @t383 (@list @t489))) % 0.40/0.91 (step @p714 :rule cnf_equiv_pos1 :args (@t493)) % 0.40/0.91 (step @p715 :rule reordering :premises (@p714) :args ((or @t494 @t492 (not @t493)))) % 0.40/0.91 (step @p716 :rule chain_m_resolution :premises (@p715 @p713 @p685) :args (@t492 @t355 (@list @t304 @t493))) % 0.40/0.91 (step @p717 :rule cnf_and_pos :args (@t492 0)) % 0.40/0.91 (step @p718 :rule reordering :premises (@p717) :args ((or @t313 (not @t492)))) % 0.40/0.91 (step @p719 :rule chain_m_resolution :premises (@p718 @p716) :args (@t313 @t383 (@list @t492))) % 0.40/0.91 (step @p720 :rule cnf_equiv_pos1 :args (@t496)) % 0.40/0.91 (step @p721 :rule reordering :premises (@p720) :args ((or @t497 @t495 (not @t496)))) % 0.40/0.91 (step @p722 :rule chain_m_resolution :premises (@p721 @p719 @p684) :args (@t495 @t355 (@list @t313 @t496))) % 0.40/0.91 (step @p723 :rule cnf_and_pos :args (@t495 1)) % 0.40/0.91 (step @p724 :rule reordering :premises (@p723) :args ((or @t315 (not @t495)))) % 0.40/0.91 (step @p725 :rule chain_m_resolution :premises (@p724 @p722) :args (@t315 @t383 (@list @t495))) % 0.40/0.91 (step @p726 :rule instantiate :premises (@p124) :args (@t476)) % 0.40/0.91 (step @p727 :rule instantiate :premises (@p121) :args (@t476)) % 0.40/0.91 (step @p728 :rule instantiate :premises (@p120) :args (@t476)) % 0.40/0.91 (step @p729 :rule cnf_and_neg :args (@t498)) % 0.40/0.91 (step @p730 :rule reordering :premises (@p729) :args ((or (not @t267) (not @t269) @t498))) % 0.40/0.91 (step @p731 :rule chain_m_resolution :premises (@p730 @p204 @p206) :args (@t498 @t355 (@list @t267 @t269))) % 0.40/0.91 (step @p732 :rule cnf_equiv_pos2 :args (@t499)) % 0.40/0.91 (step @p733 :rule reordering :premises (@p732) :args ((or @t316 (not @t498) (not @t499)))) % 0.40/0.91 (step @p734 :rule chain_m_resolution :premises (@p733 @p731 @p728) :args (@t316 @t355 (@list @t498 @t499))) % 0.40/0.91 (step @p735 :rule cnf_and_neg :args (@t500)) % 0.40/0.91 (step @p736 :rule reordering :premises (@p735) :args ((or @t502 @t501 @t500))) % 0.40/0.91 (step @p737 :rule chain_m_resolution :premises (@p736 @p191 @p734) :args (@t500 @t355 (@list @t261 @t316))) % 0.40/0.91 (step @p738 :rule cnf_equiv_pos2 :args (@t503)) % 0.40/0.91 (step @p739 :rule reordering :premises (@p738) :args ((or @t321 (not @t500) (not @t503)))) % 0.40/0.91 (step @p740 :rule chain_m_resolution :premises (@p739 @p737 @p727) :args (@t321 @t355 (@list @t500 @t503))) % 0.40/0.91 (step @p741 :rule eq-symm :args (@t156 @t26)) % 0.40/0.91 (step @p742 :rule cong :premises (@p741) :args (@t157)) % 0.40/0.91 (step @p743 :rule eq_resolve :premises (@p123 @p742)) % 0.40/0.91 (step @p744 :rule instantiate :premises (@p743) :args (@t476)) % 0.40/0.91 (step @p745 :rule cnf_equiv_pos1 :args (@t504)) % 0.40/0.91 (step @p746 :rule reordering :premises (@p745) :args ((or @t339 @t502 (not @t504)))) % 0.40/0.91 (step @p747 :rule chain_m_resolution :premises (@p746 @p191 @p744) :args (@t339 @t355 (@list @t261 @t504))) % 0.40/0.91 (step @p748 :rule cnf_and_neg :args (@t505)) % 0.40/0.91 (step @p749 :rule reordering :premises (@p748) :args ((or @t507 @t506 @t505))) % 0.40/0.91 (step @p750 :rule chain_m_resolution :premises (@p749 @p747 @p740) :args (@t505 @t355 (@list @t339 @t321))) % 0.40/0.91 (step @p751 :rule cnf_equiv_pos2 :args (@t508)) % 0.40/0.91 (step @p752 :rule reordering :premises (@p751) :args ((or @t303 (not @t505) (not @t508)))) % 0.40/0.91 (step @p753 :rule chain_m_resolution :premises (@p752 @p750 @p726) :args (@t303 @t355 (@list @t505 @t508))) % 0.40/0.91 (step @p754 :rule bool-and-de-morgan :args (@t17 @t106 true)) % 0.40/0.91 (step @p755 :rule cong :premises (@p754) :args (@t509)) % 0.40/0.91 (step @p756 :rule cong :premises (@p755) :args (@t510)) % 0.40/0.91 (step @p757 :rule exists-elim :args ((= @t108 @t510))) % 0.40/0.91 (step @p758 :rule trans :premises (@p757 @p756)) % 0.40/0.91 (step @p759 :rule refl :args (@t7)) % 0.40/0.91 (step @p760 :rule cong :premises (@p759 @p758) :args (@t154)) % 0.40/0.91 (step @p761 :rule cong :premises (@p760) :args (@t155)) % 0.40/0.91 (step @p762 :rule eq_resolve :premises (@p122 @p761)) % 0.40/0.91 (step @p763 :rule instantiate :premises (@p762) :args (@t476)) % 0.40/0.91 (step @p764 :rule cnf_or_pos :args (@t512)) % 0.40/0.91 (step @p765 :rule reordering :premises (@p764) :args ((or @t511 @t447 @t513))) % 0.40/0.91 (step @p766 :rule chain_m_resolution :premises (@p765 @p224 @p238) :args (@t513 @t355 (@list @t278 @t280))) % 0.40/0.91 (assume-push @p1023 @t514) % 0.40/0.91 (step @p768 :rule instantiate :premises (@p1023) :args (@t432)) % 0.40/0.91 (step-pop @p1024 :rule scope :premises (@p768)) % 0.40/0.91 (step @p769 :rule process_scope :premises (@p1024) :args (@t512)) % 0.40/0.91 (step @p771 :rule implies_elim :premises (@p769)) % 0.40/0.91 (step @p772 :rule chain_m_resolution :premises (@p771 @p766) :args (@t515 @t359 (@list @t512))) % 0.40/0.91 (step @p773 :rule bool-double-not-elim :args (@t514)) % 0.40/0.91 (step @p774 :rule refl :args (@t305)) % 0.40/0.91 (step @p775 :rule refl :args (@t517)) % 0.40/0.91 (step @p776 :rule nary_cong :premises (@p775 @p774 @p773) :args ((or @t517 @t305 (not @t515)))) % 0.40/0.91 (step @p777 :rule cnf_equiv_pos2 :args (@t516)) % 0.40/0.91 (step @p778 :rule eq_resolve :premises (@p777 @p776)) % 0.40/0.91 (step @p779 :rule reordering :premises (@p778) :args ((or @t305 @t514 @t517))) % 0.40/0.91 (step @p780 :rule chain_m_resolution :premises (@p779 @p772 @p763) :args (@t305 @t363 (@list @t514 @t516))) % 0.40/0.91 (step @p781 :rule instantiate :premises (@p81) :args (@t476)) % 0.40/0.91 (step @p782 :rule cnf_and_neg :args (@t518)) % 0.40/0.91 (step @p783 :rule reordering :premises (@p782) :args ((or (not @t265) (not @t272) @t518))) % 0.40/0.91 (step @p784 :rule chain_m_resolution :premises (@p783 @p199 @p214) :args (@t518 @t355 (@list @t265 @t272))) % 0.40/0.91 (step @p785 :rule cnf_equiv_pos2 :args (@t519)) % 0.40/0.91 (step @p786 :rule reordering :premises (@p785) :args ((or @t306 (not @t518) (not @t519)))) % 0.40/0.91 (step @p787 :rule chain_m_resolution :premises (@p786 @p784 @p781) :args (@t306 @t355 (@list @t518 @t519))) % 0.40/0.91 (step @p788 :rule instantiate :premises (@p40) :args (@t476)) % 0.40/0.91 (step @p789 :rule cnf_and_neg :args (@t520)) % 0.40/0.91 (step @p790 :rule reordering :premises (@p789) :args ((or (not @t264) (not @t271) @t520))) % 0.40/0.91 (step @p791 :rule chain_m_resolution :premises (@p790 @p198 @p211) :args (@t520 @t355 (@list @t264 @t271))) % 0.40/0.91 (step @p792 :rule cnf_equiv_pos2 :args (@t521)) % 0.40/0.91 (step @p793 :rule reordering :premises (@p792) :args ((or @t307 (not @t520) (not @t521)))) % 0.40/0.91 (step @p794 :rule chain_m_resolution :premises (@p793 @p791 @p788) :args (@t307 @t355 (@list @t520 @t521))) % 0.40/0.91 (step @p795 :rule eq-symm :args (@t251 @t26)) % 0.40/0.91 (step @p796 :rule cong :premises (@p795) :args (@t252)) % 0.40/0.91 (step @p797 :rule eq_resolve :premises (@p174 @p796)) % 0.40/0.91 (step @p798 :rule instantiate :premises (@p797) :args (@t476)) % 0.40/0.91 (step @p799 :rule cnf_equiv_pos1 :args (@t522)) % 0.40/0.91 (step @p800 :rule reordering :premises (@p799) :args ((or @t308 @t502 (not @t522)))) % 0.40/0.91 (step @p801 :rule chain_m_resolution :premises (@p800 @p191 @p798) :args (@t308 @t355 (@list @t261 @t522))) % 0.40/0.91 (step @p802 :rule instantiate :premises (@p170) :args (@t476)) % 0.40/0.91 (step @p803 :rule instantiate :premises (@p168) :args (@t476)) % 0.40/0.91 (step @p804 :rule cnf_and_neg :args (@t523)) % 0.40/0.91 (step @p805 :rule reordering :premises (@p804) :args ((or (not @t262) (not @t273) @t523))) % 0.40/0.91 (step @p806 :rule chain_m_resolution :premises (@p805 @p196 @p216) :args (@t523 @t355 (@list @t262 @t273))) % 0.40/0.91 (step @p807 :rule cnf_equiv_pos2 :args (@t524)) % 0.40/0.91 (step @p808 :rule reordering :premises (@p807) :args ((or @t327 (not @t523) (not @t524)))) % 0.40/0.91 (step @p809 :rule chain_m_resolution :premises (@p808 @p806 @p803) :args (@t327 @t355 (@list @t523 @t524))) % 0.40/0.91 (step @p810 :rule cnf_and_neg :args (@t525)) % 0.40/0.91 (step @p811 :rule reordering :premises (@p810) :args ((or @t502 @t526 @t525))) % 0.40/0.91 (step @p812 :rule chain_m_resolution :premises (@p811 @p191 @p809) :args (@t525 @t355 (@list @t261 @t327))) % 0.40/0.91 (step @p813 :rule cnf_equiv_pos2 :args (@t527)) % 0.40/0.91 (step @p814 :rule reordering :premises (@p813) :args ((or @t309 (not @t525) (not @t527)))) % 0.40/0.91 (step @p815 :rule chain_m_resolution :premises (@p814 @p812 @p802) :args (@t309 @t355 (@list @t525 @t527))) % 0.40/0.91 (step @p816 :rule instantiate :premises (@p64) :args (@t476)) % 0.40/0.91 (step @p817 :rule cnf_and_neg :args (@t528)) % 0.40/0.91 (step @p818 :rule reordering :premises (@p817) :args ((or (not @t259) (not @t268) @t528))) % 0.40/0.91 (step @p819 :rule chain_m_resolution :premises (@p818 @p188 @p205) :args (@t528 @t355 (@list @t259 @t268))) % 0.40/0.91 (step @p820 :rule cnf_equiv_pos2 :args (@t529)) % 0.40/0.91 (step @p821 :rule reordering :premises (@p820) :args ((or @t310 (not @t528) (not @t529)))) % 0.40/0.91 (step @p822 :rule chain_m_resolution :premises (@p821 @p819 @p816) :args (@t310 @t355 (@list @t528 @t529))) % 0.40/0.91 (step @p823 :rule instantiate :premises (@p68) :args (@t476)) % 0.40/0.91 (step @p824 :rule instantiate :premises (@p101) :args (@t476)) % 0.40/0.91 (step @p825 :rule cnf_and_pos :args (@t481 0)) % 0.40/0.91 (step @p826 :rule reordering :premises (@p825) :args ((or @t331 @t484))) % 0.40/0.91 (step @p827 :rule chain_m_resolution :premises (@p826 @p698) :args (@t331 @t383 @t485)) % 0.40/0.91 (step @p828 :rule cnf_equiv_pos1 :args (@t531)) % 0.40/0.91 (step @p829 :rule reordering :premises (@p828) :args ((or @t532 @t530 (not @t531)))) % 0.40/0.91 (step @p830 :rule chain_m_resolution :premises (@p829 @p827 @p824) :args (@t530 @t355 (@list @t331 @t531))) % 0.40/0.91 (step @p831 :rule cnf_and_pos :args (@t530 1)) % 0.40/0.91 (step @p832 :rule reordering :premises (@p831) :args ((or @t326 @t533))) % 0.40/0.91 (step @p833 :rule chain_m_resolution :premises (@p832 @p830) :args (@t326 @t383 @t534)) % 0.40/0.91 (step @p834 :rule cnf_equiv_pos1 :args (@t536)) % 0.40/0.91 (step @p835 :rule reordering :premises (@p834) :args ((or @t537 @t535 (not @t536)))) % 0.40/0.91 (step @p836 :rule chain_m_resolution :premises (@p835 @p833 @p823) :args (@t535 @t355 (@list @t326 @t536))) % 0.40/0.91 (step @p837 :rule cnf_and_pos :args (@t535 1)) % 0.40/0.91 (step @p838 :rule reordering :premises (@p837) :args ((or @t311 @t538))) % 0.40/0.91 (step @p839 :rule chain_m_resolution :premises (@p838 @p836) :args (@t311 @t383 @t539)) % 0.40/0.91 (step @p840 :rule instantiate :premises (@p171) :args (@t476)) % 0.40/0.91 (step @p841 :rule instantiate :premises (@p149) :args (@t476)) % 0.40/0.91 (step @p842 :rule eq-symm :args (@t194 @t26)) % 0.40/0.91 (step @p843 :rule cong :premises (@p842) :args (@t195)) % 0.40/0.91 (step @p844 :rule eq_resolve :premises (@p148 @p843)) % 0.40/0.91 (step @p845 :rule instantiate :premises (@p844) :args (@t476)) % 0.40/0.91 (step @p846 :rule cnf_equiv_pos1 :args (@t540)) % 0.40/0.91 (step @p847 :rule reordering :premises (@p846) :args ((or @t318 @t502 (not @t540)))) % 0.40/0.91 (step @p848 :rule chain_m_resolution :premises (@p847 @p191 @p845) :args (@t318 @t355 (@list @t261 @t540))) % 0.40/0.91 (step @p849 :rule instantiate :premises (@p147) :args (@t476)) % 0.40/0.91 (step @p850 :rule instantiate :premises (@p144) :args (@t476)) % 0.40/0.91 (step @p851 :rule instantiate :premises (@p143) :args (@t476)) % 0.40/0.91 (step @p852 :rule cnf_and_neg :args (@t541)) % 0.40/0.91 (step @p853 :rule reordering :premises (@p852) :args ((or (not @t270) (not @t275) @t541))) % 0.40/0.91 (step @p854 :rule chain_m_resolution :premises (@p853 @p210 @p218) :args (@t541 @t355 (@list @t270 @t275))) % 0.40/0.91 (step @p855 :rule cnf_equiv_pos2 :args (@t542)) % 0.40/0.91 (step @p856 :rule reordering :premises (@p855) :args ((or @t334 (not @t541) (not @t542)))) % 0.40/0.91 (step @p857 :rule chain_m_resolution :premises (@p856 @p854 @p851) :args (@t334 @t355 (@list @t541 @t542))) % 0.40/0.91 (step @p858 :rule cnf_and_neg :args (@t543)) % 0.40/0.91 (step @p859 :rule reordering :premises (@p858) :args ((or @t502 @t544 @t543))) % 0.40/0.91 (step @p860 :rule chain_m_resolution :premises (@p859 @p191 @p857) :args (@t543 @t355 (@list @t261 @t334))) % 0.40/0.91 (step @p861 :rule cnf_equiv_pos2 :args (@t545)) % 0.40/0.91 (step @p862 :rule reordering :premises (@p861) :args ((or @t335 (not @t543) (not @t545)))) % 0.40/0.91 (step @p863 :rule chain_m_resolution :premises (@p862 @p860 @p850) :args (@t335 @t355 (@list @t543 @t545))) % 0.40/0.91 (step @p864 :rule cnf_and_neg :args (@t546)) % 0.40/0.91 (step @p865 :rule reordering :premises (@p864) :args ((or @t548 @t547 @t546))) % 0.40/0.91 (step @p866 :rule chain_m_resolution :premises (@p865 @p863 @p753) :args (@t546 @t355 (@list @t335 @t303))) % 0.40/0.91 (step @p867 :rule cnf_equiv_pos2 :args (@t549)) % 0.40/0.91 (step @p868 :rule reordering :premises (@p867) :args ((or @t330 (not @t546) (not @t549)))) % 0.40/0.91 (step @p869 :rule chain_m_resolution :premises (@p868 @p866 @p849) :args (@t330 @t355 (@list @t546 @t549))) % 0.40/0.91 (step @p870 :rule cnf_and_neg :args (@t550)) % 0.40/0.91 (step @p871 :rule reordering :premises (@p870) :args ((or @t552 @t551 @t550))) % 0.40/0.91 (step @p872 :rule chain_m_resolution :premises (@p871 @p869 @p848) :args (@t550 @t355 (@list @t330 @t318))) % 0.40/0.91 (step @p873 :rule cnf_equiv_pos2 :args (@t553)) % 0.40/0.91 (step @p874 :rule reordering :premises (@p873) :args ((or @t314 (not @t550) (not @t553)))) % 0.40/0.91 (step @p875 :rule chain_m_resolution :premises (@p874 @p872 @p841) :args (@t314 @t355 (@list @t550 @t553))) % 0.40/0.91 (step @p876 :rule cnf_and_neg :args (@t554)) % 0.40/0.91 (step @p877 :rule reordering :premises (@p876) :args ((or @t556 @t555 @t554))) % 0.40/0.91 (step @p878 :rule chain_m_resolution :premises (@p877 @p875 @p815) :args (@t554 @t355 (@list @t314 @t309))) % 0.40/0.91 (step @p879 :rule cnf_equiv_pos2 :args (@t557)) % 0.40/0.91 (step @p880 :rule reordering :premises (@p879) :args ((or @t312 (not @t554) (not @t557)))) % 0.40/0.91 (step @p881 :rule chain_m_resolution :premises (@p880 @p878 @p840) :args (@t312 @t355 (@list @t554 @t557))) % 0.40/0.91 (step @p882 :rule instantiate :premises (@p3) :args (@t476)) % 0.40/0.91 (step @p883 :rule cnf_and_pos :args (@t535 0)) % 0.40/0.91 (step @p884 :rule reordering :premises (@p883) :args ((or @t337 @t538))) % 0.40/0.91 (step @p885 :rule chain_m_resolution :premises (@p884 @p836) :args (@t337 @t383 @t539)) % 0.40/0.91 (step @p886 :rule cnf_equiv_pos1 :args (@t559)) % 0.40/0.91 (step @p887 :rule reordering :premises (@p886) :args ((or @t560 @t558 (not @t559)))) % 0.40/0.91 (step @p888 :rule chain_m_resolution :premises (@p887 @p885 @p882) :args (@t558 @t355 (@list @t337 @t559))) % 0.40/0.91 (step @p889 :rule cnf_and_pos :args (@t558 0)) % 0.40/0.91 (step @p890 :rule reordering :premises (@p889) :args ((or @t317 (not @t558)))) % 0.40/0.91 (step @p891 :rule chain_m_resolution :premises (@p890 @p888) :args (@t317 @t383 (@list @t558))) % 0.40/0.91 (step @p892 :rule instantiate :premises (@p88) :args (@t476)) % 0.40/0.91 (step @p893 :rule cnf_and_neg :args (@t561)) % 0.40/0.91 (step @p894 :rule reordering :premises (@p893) :args ((or (not @t274) @t562 @t561))) % 0.40/0.91 (step @p895 :rule chain_m_resolution :premises (@p894 @p217 @p787) :args (@t561 @t355 (@list @t274 @t306))) % 0.40/0.91 (step @p896 :rule cnf_equiv_pos2 :args (@t563)) % 0.40/0.91 (step @p897 :rule reordering :premises (@p896) :args ((or @t319 (not @t561) (not @t563)))) % 0.40/0.91 (step @p898 :rule chain_m_resolution :premises (@p897 @p895 @p892) :args (@t319 @t355 (@list @t561 @t563))) % 0.40/0.91 (step @p899 :rule eq-symm :args (@t248 @t26)) % 0.40/0.91 (step @p900 :rule cong :premises (@p899) :args (@t249)) % 0.40/0.91 (step @p901 :rule eq_resolve :premises (@p172 @p900)) % 0.40/0.91 (step @p902 :rule instantiate :premises (@p901) :args (@t476)) % 0.40/0.91 (step @p903 :rule cnf_equiv_pos1 :args (@t564)) % 0.40/0.91 (step @p904 :rule reordering :premises (@p903) :args ((or @t322 @t502 (not @t564)))) % 0.40/0.91 (step @p905 :rule chain_m_resolution :premises (@p904 @p191 @p902) :args (@t322 @t355 (@list @t261 @t564))) % 0.40/0.91 (step @p906 :rule cnf_and_pos :args (@t530 0)) % 0.40/0.91 (step @p907 :rule reordering :premises (@p906) :args ((or @t323 @t533))) % 0.40/0.91 (step @p908 :rule chain_m_resolution :premises (@p907 @p830) :args (@t323 @t383 @t534)) % 0.40/0.91 (step @p909 :rule eq-symm :args (@t30 @t26)) % 0.40/0.91 (step @p910 :rule cong :premises (@p909) :args (@t31)) % 0.40/0.91 (step @p911 :rule eq_resolve :premises (@p18 @p910)) % 0.40/0.91 (step @p912 :rule instantiate :premises (@p911) :args (@t476)) % 0.40/0.91 (step @p913 :rule cnf_equiv_pos1 :args (@t565)) % 0.40/0.91 (step @p914 :rule reordering :premises (@p913) :args ((or @t324 @t502 (not @t565)))) % 0.40/0.91 (step @p915 :rule chain_m_resolution :premises (@p914 @p191 @p912) :args (@t324 @t355 (@list @t261 @t565))) % 0.40/0.91 (step @p916 :rule instantiate :premises (@p41) :args (@t476)) % 0.40/0.91 (step @p917 :rule cnf_and_neg :args (@t566)) % 0.40/0.91 (step @p918 :rule reordering :premises (@p917) :args ((or @t502 @t567 @t566))) % 0.40/0.91 (step @p919 :rule chain_m_resolution :premises (@p918 @p191 @p794) :args (@t566 @t355 (@list @t261 @t307))) % 0.40/0.91 (step @p920 :rule cnf_equiv_pos2 :args (@t568)) % 0.40/0.91 (step @p921 :rule reordering :premises (@p920) :args ((or @t325 (not @t566) (not @t568)))) % 0.40/0.91 (step @p922 :rule chain_m_resolution :premises (@p921 @p919 @p916) :args (@t325 @t355 (@list @t566 @t568))) % 0.40/0.91 (step @p923 :rule cnf_and_pos :args (@t477 1)) % 0.40/0.91 (step @p924 :rule reordering :premises (@p923) :args ((or @t328 @t479))) % 0.40/0.91 (step @p925 :rule chain_m_resolution :premises (@p924 @p692) :args (@t328 @t383 @t480)) % 0.40/0.91 (step @p926 :rule instantiate :premises (@p65) :args (@t476)) % 0.40/0.91 (step @p927 :rule cnf_and_neg :args (@t569)) % 0.40/0.91 (step @p928 :rule reordering :premises (@p927) :args ((or @t502 @t570 @t569))) % 0.40/0.91 (step @p929 :rule chain_m_resolution :premises (@p928 @p191 @p822) :args (@t569 @t355 (@list @t261 @t310))) % 0.40/0.91 (step @p930 :rule cnf_equiv_pos2 :args (@t571)) % 0.40/0.91 (step @p931 :rule reordering :premises (@p930) :args ((or @t329 (not @t569) (not @t571)))) % 0.40/0.91 (step @p932 :rule chain_m_resolution :premises (@p931 @p929 @p926) :args (@t329 @t355 (@list @t569 @t571))) % 0.40/0.91 (step @p933 :rule instantiate :premises (@p16) :args (@t476)) % 0.40/0.91 (step @p934 :rule instantiate :premises (@p15) :args (@t476)) % 0.40/0.91 (step @p935 :rule cnf_and_neg :args (@t572)) % 0.40/0.91 (step @p936 :rule reordering :premises (@p935) :args ((or (not @t263) (not @t266) @t572))) % 0.40/0.91 (step @p937 :rule chain_m_resolution :premises (@p936 @p197 @p200) :args (@t572 @t355 (@list @t263 @t266))) % 0.40/0.91 (step @p938 :rule cnf_equiv_pos2 :args (@t573)) % 0.40/0.91 (step @p939 :rule reordering :premises (@p938) :args ((or @t340 (not @t572) (not @t573)))) % 0.40/0.91 (step @p940 :rule chain_m_resolution :premises (@p939 @p937 @p934) :args (@t340 @t355 (@list @t572 @t573))) % 0.40/0.91 (step @p941 :rule cnf_and_neg :args (@t574)) % 0.40/0.91 (step @p942 :rule reordering :premises (@p941) :args ((or @t502 @t575 @t574))) % 0.40/0.91 (step @p943 :rule chain_m_resolution :premises (@p942 @p191 @p940) :args (@t574 @t355 (@list @t261 @t340))) % 0.40/0.91 (step @p944 :rule cnf_equiv_pos2 :args (@t576)) % 0.40/0.91 (step @p945 :rule reordering :premises (@p944) :args ((or @t332 (not @t574) (not @t576)))) % 0.40/0.91 (step @p946 :rule chain_m_resolution :premises (@p945 @p943 @p933) :args (@t332 @t355 (@list @t574 @t576))) % 0.40/0.91 (step @p947 :rule eq-symm :args (@t51 @t26)) % 0.40/0.91 (step @p948 :rule cong :premises (@p947) :args (@t52)) % 0.40/0.91 (step @p949 :rule eq_resolve :premises (@p43 @p948)) % 0.40/0.91 (step @p950 :rule instantiate :premises (@p949) :args (@t476)) % 0.40/0.91 (step @p951 :rule cnf_equiv_pos1 :args (@t577)) % 0.40/0.91 (step @p952 :rule reordering :premises (@p951) :args ((or @t338 @t502 (not @t577)))) % 0.40/0.91 (step @p953 :rule chain_m_resolution :premises (@p952 @p191 @p950) :args (@t338 @t355 (@list @t261 @t577))) % 0.40/0.91 (step @p954 :rule instantiate :premises (@p173) :args (@t476)) % 0.40/0.91 (step @p955 :rule cnf_and_neg :args (@t578)) % 0.40/0.91 (step @p956 :rule reordering :premises (@p955) :args ((or @t580 @t579 @t578))) % 0.40/0.91 (step @p957 :rule chain_m_resolution :premises (@p956 @p905 @p881) :args (@t578 @t355 (@list @t322 @t312))) % 0.40/0.91 (step @p958 :rule cnf_equiv_pos2 :args (@t581)) % 0.40/0.91 (step @p959 :rule reordering :premises (@p958) :args ((or @t301 (not @t578) (not @t581)))) % 0.40/0.91 (step @p960 :rule chain_m_resolution :premises (@p959 @p957 @p954) :args (@t301 @t355 (@list @t578 @t581))) % 0.40/0.91 (step @p961 :rule instantiate :premises (@p17) :args (@t476)) % 0.40/0.91 (step @p962 :rule cnf_equiv_pos1 :args (@t583)) % 0.40/0.91 (step @p963 :rule reordering :premises (@p962) :args ((or @t584 @t582 (not @t583)))) % 0.40/0.91 (step @p964 :rule chain_m_resolution :premises (@p963 @p725 @p961) :args (@t582 @t355 (@list @t315 @t583))) % 0.40/0.91 (step @p965 :rule cnf_and_pos :args (@t582 1)) % 0.40/0.91 (step @p966 :rule reordering :premises (@p965) :args ((or @t336 (not @t582)))) % 0.40/0.91 (step @p967 :rule chain_m_resolution :premises (@p966 @p964) :args (@t336 @t383 (@list @t582))) % 0.40/0.91 (step @p968 :rule aci_norm :args ((= (and (and @t586 @t585) @t6 @t340 @t339 @t338 @t337 @t336 @t276 @t335 @t334 @t333 @t332 @t331 @t330 @t329 @t328 @t327 @t326 @t325 @t324 @t323 @t322 @t321 @t320 @t319 @t318 @t317 @t316 @t315 @t314 @t313 @t312 @t311 @t310 @t309 @t308 @t307 @t306 @t305 @t304 @t303 @t302 @t301 @t300 @t282 @t299 @t298 @t297 @t287 @t296 @t295 @t292) (and @t6 @t340 @t339 @t338 @t337 @t336 @t276 @t335 @t334 @t333 @t332 @t331 @t330 @t329 @t328 @t327 @t326 @t325 @t324 @t323 @t322 @t321 @t320 @t319 @t318 @t317 @t316 @t315 @t314 @t313 @t312 @t311 @t310 @t309 @t308 @t307 @t306 @t305 @t304 @t303 @t302 @t301 @t300 @t282 @t299 @t298 @t297 @t287 @t296 @t295 @t292 @t586 @t585)))) % 0.40/0.91 (step @p969 :rule refl :args (@t292)) % 0.40/0.91 (step @p970 :rule refl :args (@t287)) % 0.40/0.91 (step @p971 :rule refl :args (@t297)) % 0.40/0.91 (step @p972 :rule refl :args (@t282)) % 0.40/0.91 (step @p973 :rule refl :args (@t301)) % 0.40/0.91 (step @p974 :rule refl :args (@t302)) % 0.40/0.91 (step @p975 :rule refl :args (@t303)) % 0.40/0.91 (step @p976 :rule refl :args (@t304)) % 0.40/0.91 (step @p977 :rule refl :args (@t306)) % 0.40/0.91 (step @p978 :rule refl :args (@t307)) % 0.40/0.91 (step @p979 :rule refl :args (@t308)) % 0.40/0.91 (step @p980 :rule refl :args (@t309)) % 0.40/0.91 (step @p981 :rule refl :args (@t310)) % 0.40/0.91 (step @p982 :rule refl :args (@t311)) % 0.40/0.91 (step @p983 :rule refl :args (@t312)) % 0.40/0.91 (step @p984 :rule refl :args (@t313)) % 0.40/0.91 (step @p985 :rule refl :args (@t314)) % 0.40/0.91 (step @p986 :rule refl :args (@t315)) % 0.40/0.91 (step @p987 :rule refl :args (@t316)) % 0.40/0.91 (step @p988 :rule refl :args (@t317)) % 0.40/0.91 (step @p989 :rule refl :args (@t318)) % 0.40/0.91 (step @p990 :rule refl :args (@t319)) % 0.40/0.91 (step @p991 :rule refl :args (@t320)) % 0.40/0.91 (step @p992 :rule refl :args (@t321)) % 0.40/0.91 (step @p993 :rule refl :args (@t322)) % 0.40/0.91 (step @p994 :rule refl :args (@t323)) % 0.40/0.91 (step @p995 :rule refl :args (@t324)) % 0.40/0.91 (step @p996 :rule refl :args (@t325)) % 0.40/0.91 (step @p997 :rule refl :args (@t326)) % 0.40/0.91 (step @p998 :rule refl :args (@t327)) % 0.40/0.91 (step @p999 :rule refl :args (@t328)) % 0.40/0.91 (step @p1000 :rule refl :args (@t329)) % 0.40/0.91 (step @p1001 :rule refl :args (@t330)) % 0.40/0.91 (step @p1002 :rule refl :args (@t331)) % 0.40/0.91 (step @p1003 :rule refl :args (@t332)) % 0.40/0.91 (step @p1004 :rule refl :args (@t333)) % 0.40/0.91 (step @p1005 :rule refl :args (@t334)) % 0.40/0.91 (step @p1006 :rule refl :args (@t335)) % 0.40/0.91 (step @p1007 :rule refl :args (@t276)) % 0.40/0.91 (step @p1008 :rule refl :args (@t336)) % 0.40/0.91 (step @p1009 :rule refl :args (@t337)) % 0.40/0.91 (step @p1010 :rule refl :args (@t338)) % 0.40/0.91 (step @p1011 :rule refl :args (@t339)) % 0.40/0.91 (step @p1012 :rule refl :args (@t340)) % 0.40/0.91 (step @p1013 :rule refl :args (@t6)) % 0.40/0.91 (step @p1014 :rule nary_cong :premises (@p349 @p1013 @p1012 @p1011 @p1010 @p1009 @p1008 @p1007 @p1006 @p1005 @p1004 @p1003 @p1002 @p1001 @p1000 @p999 @p998 @p997 @p996 @p995 @p994 @p993 @p992 @p991 @p990 @p989 @p988 @p987 @p986 @p985 @p984 @p983 @p982 @p981 @p980 @p979 @p978 @p977 @p774 @p976 @p975 @p974 @p973 @p677 @p972 @p617 @p557 @p971 @p970 @p466 @p406 @p969) :args (@t341)) % 0.40/0.91 (step @p1015 :rule trans :premises (@p1014 @p968)) % 0.40/0.91 (step @p1016 :rule cong :premises (@p1015) :args (@t342)) % 0.40/0.91 (step @p1017 :rule eq_resolve :premises (@p343 @p1016)) % 0.40/0.91 (step @p1018 :rule not_and :premises (@p1017)) % 0.40/0.91 (step @p1019 :rule reordering :premises (@p1018) :args ((or (not @t586) (not @t585) (not @t6) (not @t276) (not @t282) (not @t287) (not @t292) @t575 @t507 (not @t338) @t560 (not @t336) @t548 @t544 @t483 (not @t332) @t532 @t552 (not @t329) (not @t328) @t526 @t537 (not @t325) (not @t324) (not @t323) @t580 @t506 @t491 (not @t319) @t551 (not @t317) @t501 @t584 @t556 @t497 @t579 (not @t311) @t570 @t555 (not @t308) @t567 @t562 (not @t305) @t494 @t547 @t488 (not @t301) (not @t300) (not @t299) (not @t298) (not @t297) (not @t296) (not @t295)))) % 0.40/0.91 (step @p1020 false :rule chain_m_resolution :premises (@p1019 @p967 @p960 @p953 @p940 @p747 @p863 @p857 @p695 @p946 @p827 @p869 @p932 @p925 @p809 @p833 @p922 @p915 @p908 @p905 @p740 @p707 @p898 @p848 @p885 @p734 @p891 @p875 @p719 @p881 @p839 @p822 @p815 @p801 @p794 @p787 @p780 @p713 @p753 @p701 @p725 @p683 @p623 @p563 @p532 @p472 @p412 @p307 @p279 @p249 @p220 @p2 @p352 @p351) :args (false (@list 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 @t336 @t301 @t338 @t340 @t339 @t335 @t334 @t333 @t332 @t331 @t330 @t329 @t328 @t327 @t326 @t325 @t324 @t323 @t322 @t321 @t320 @t319 @t318 @t337 @t316 @t317 @t314 @t313 @t312 @t311 @t310 @t309 @t308 @t307 @t306 @t305 @t304 @t303 @t302 @t315 @t300 @t299 @t298 @t297 @t296 @t295 @t292 @t287 @t282 @t276 @t6 @t585 @t586))) % 0.40/0.91 ) % 0.40/0.91 % SZS output end Proof % 0.40/0.91 % cvc5 exiting %------------------------------------------------------------------------------