%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWW842_1 : TPTP v9.2.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n008.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 09:05:44 AM UTC 2026 % Result : Unsatisfiable 56.22s 56.40s % Output : Proof 56.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW842_1 : TPTP v9.2.1. Released v7.0.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.34 % Computer : n008.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Tue Jun 2 22:33:48 EDT 2026 % 0.17/0.35 % CPUTime : % 0.41/0.66 %----Proving TF0_ARI % 0.41/0.67 --- Run --finite-model-find --decision=internal at 45... % 45.85/46.12 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 60... % 56.22/56.40 % SZS status Unsatisfiable % 56.22/56.40 % SZS output start Proof % 56.22/56.45 ( % 56.22/56.45 (declare-sort |tptp.'S60'| 0) % 56.22/56.45 (declare-sort |tptp.'S59'| 0) % 56.22/56.45 (declare-sort |tptp.'S58'| 0) % 56.22/56.45 (declare-sort |tptp.'S57'| 0) % 56.22/56.45 (declare-sort |tptp.'S56'| 0) % 56.22/56.45 (declare-sort |tptp.'S28'| 0) % 56.22/56.45 (declare-sort |tptp.'S23'| 0) % 56.22/56.45 (declare-sort |tptp.'S19'| 0) % 56.22/56.45 (declare-sort |tptp.'S17'| 0) % 56.22/56.45 (declare-sort |tptp.'S14'| 0) % 56.22/56.45 (declare-sort |tptp.'S12'| 0) % 56.22/56.45 (declare-sort |tptp.'S13'| 0) % 56.22/56.45 (declare-sort |tptp.'S11'| 0) % 56.22/56.45 (declare-sort |tptp.'S10'| 0) % 56.22/56.45 (declare-sort |tptp.'S42'| 0) % 56.22/56.45 (declare-sort |tptp.'S18'| 0) % 56.22/56.45 (declare-sort |tptp.'S1'| 0) % 56.22/56.45 (declare-sort |tptp.'S20'| 0) % 56.22/56.45 (declare-sort |tptp.'S16'| 0) % 56.22/56.45 (declare-sort |tptp.'S41'| 0) % 56.22/56.45 (declare-sort |tptp.'S7'| 0) % 56.22/56.45 (declare-sort |tptp.'S24'| 0) % 56.22/56.45 (declare-sort |tptp.'S4'| 0) % 56.22/56.45 (declare-sort |tptp.'S9'| 0) % 56.22/56.45 (declare-sort |tptp.'S22'| 0) % 56.22/56.45 (declare-sort |tptp.'S8'| 0) % 56.22/56.45 (declare-sort |tptp.'S21'| 0) % 56.22/56.45 (declare-sort |tptp.'S2'| 0) % 56.22/56.45 (declare-sort |tptp.'S44'| 0) % 56.22/56.45 (declare-sort |tptp.'S15'| 0) % 56.22/56.45 (declare-sort |tptp.'S3'| 0) % 56.22/56.45 (declare-sort |tptp.'S5'| 0) % 56.22/56.45 (declare-sort |tptp.'S6'| 0) % 56.22/56.45 (declare-sort |tptp.'S30'| 0) % 56.22/56.45 (declare-sort |tptp.'S27'| 0) % 56.22/56.45 (declare-sort |tptp.'S29'| 0) % 56.22/56.45 (declare-sort |tptp.'S25'| 0) % 56.22/56.45 (declare-sort |tptp.'S26'| 0) % 56.22/56.45 (declare-sort |tptp.'S33'| 0) % 56.22/56.45 (declare-sort |tptp.'S34'| 0) % 56.22/56.45 (declare-sort |tptp.'S31'| 0) % 56.22/56.45 (declare-sort |tptp.'S32'| 0) % 56.22/56.45 (declare-sort |tptp.'S35'| 0) % 56.22/56.45 (declare-sort |tptp.'S36'| 0) % 56.22/56.45 (declare-sort |tptp.'S37'| 0) % 56.22/56.45 (declare-sort |tptp.'S38'| 0) % 56.22/56.45 (declare-sort |tptp.'S39'| 0) % 56.22/56.45 (declare-sort |tptp.'S40'| 0) % 56.22/56.45 (declare-sort |tptp.'S43'| 0) % 56.22/56.45 (declare-sort |tptp.'S46'| 0) % 56.22/56.45 (declare-sort |tptp.'S45'| 0) % 56.22/56.45 (declare-sort |tptp.'S47'| 0) % 56.22/56.45 (declare-sort |tptp.'S48'| 0) % 56.22/56.45 (declare-sort |tptp.'S49'| 0) % 56.22/56.45 (declare-sort |tptp.'S50'| 0) % 56.22/56.45 (declare-sort |tptp.'S51'| 0) % 56.22/56.45 (declare-sort |tptp.'S52'| 0) % 56.22/56.45 (declare-sort |tptp.'S53'| 0) % 56.22/56.45 (declare-sort |tptp.'S54'| 0) % 56.22/56.45 (declare-sort |tptp.'S55'| 0) % 56.22/56.45 (declare-const tptp.f146 |tptp.'S4'|) % 56.22/56.45 (declare-const tptp.f145 |tptp.'S2'|) % 56.22/56.45 (declare-const tptp.f144 (-> |tptp.'S2'| |tptp.'S28'| |tptp.'S1'|)) % 56.22/56.45 (declare-const tptp.f143 |tptp.'S56'|) % 56.22/56.45 (declare-const tptp.f142 |tptp.'S15'|) % 56.22/56.45 (declare-const tptp.f139 (-> |tptp.'S59'| |tptp.'S28'| Int)) % 56.22/56.45 (declare-const tptp.f140 (-> |tptp.'S60'| |tptp.'S9'| |tptp.'S59'|)) % 56.22/56.45 (declare-const tptp.f141 |tptp.'S60'|) % 56.22/56.45 (declare-const tptp.f136 (-> |tptp.'S57'| |tptp.'S28'| |tptp.'S2'|)) % 56.22/56.45 (declare-const tptp.f137 (-> |tptp.'S58'| |tptp.'S19'| |tptp.'S57'|)) % 56.22/56.45 (declare-const tptp.f138 |tptp.'S58'|) % 56.22/56.45 (declare-const tptp.f134 (-> |tptp.'S56'| |tptp.'S2'| |tptp.'S17'|)) % 56.22/56.45 (declare-const tptp.f135 |tptp.'S56'|) % 56.22/56.45 (declare-const tptp.f133 |tptp.'S10'|) % 56.22/56.45 (declare-const tptp.f131 |tptp.'S3'|) % 56.22/56.45 (declare-const tptp.f132 |tptp.'S4'|) % 56.22/56.45 (declare-const tptp.f130 |tptp.'S47'|) % 56.22/56.45 (declare-const tptp.f127 (-> |tptp.'S54'| |tptp.'S2'| |tptp.'S46'|)) % 56.22/56.45 (declare-const tptp.f128 (-> |tptp.'S55'| Int |tptp.'S54'|)) % 56.22/56.45 (declare-const tptp.f59 |tptp.'S6'|) % 56.22/56.45 (declare-const tptp.f54 |tptp.'S21'|) % 56.22/56.45 (declare-const tptp.f55 |tptp.'S6'|) % 56.22/56.45 (declare-const tptp.f52 (-> |tptp.'S22'| |tptp.'S10'| |tptp.'S12'|)) % 56.22/56.45 (declare-const tptp.f20 |tptp.'S3'|) % 56.22/56.45 (declare-const tptp.f53 |tptp.'S22'|) % 56.22/56.45 (declare-const tptp.f51 |tptp.'S6'|) % 56.22/56.45 (declare-const tptp.f107 |tptp.'S20'|) % 56.22/56.45 (declare-const tptp.f44 (-> |tptp.'S19'| |tptp.'S2'| |tptp.'S2'|)) % 56.22/56.45 (declare-const tptp.f89 (-> |tptp.'S40'| |tptp.'S4'| |tptp.'S25'|)) % 56.22/56.45 (declare-const tptp.f45 (-> |tptp.'S20'| |tptp.'S2'| |tptp.'S19'|)) % 56.22/56.45 (declare-const tptp.f46 |tptp.'S20'|) % 56.22/56.45 (declare-const tptp.f47 |tptp.'S12'|) % 56.22/56.45 (declare-const tptp.f116 |tptp.'S45'|) % 56.22/56.45 (declare-const tptp.f43 |tptp.'S12'|) % 56.22/56.45 (declare-const tptp.f42 |tptp.'S17'|) % 56.22/56.45 (declare-const tptp.f126 |tptp.'S53'|) % 56.22/56.45 (declare-const tptp.f41 |tptp.'S18'|) % 56.22/56.45 (declare-const tptp.f40 |tptp.'S12'|) % 56.22/56.45 (declare-const tptp.f39 |tptp.'S17'|) % 56.22/56.45 (declare-const tptp.f71 (-> |tptp.'S2'| |tptp.'S30'|)) % 56.22/56.45 (declare-const tptp.f49 (-> |tptp.'S21'| |tptp.'S3'| |tptp.'S17'|)) % 56.22/56.45 (declare-const tptp.f37 (-> |tptp.'S18'| |tptp.'S9'| |tptp.'S9'|)) % 56.22/56.45 (declare-const tptp.f38 |tptp.'S18'|) % 56.22/56.45 (declare-const tptp.f90 (-> |tptp.'S41'| |tptp.'S4'| |tptp.'S40'|)) % 56.22/56.45 (declare-const tptp.f36 |tptp.'S12'|) % 56.22/56.45 (declare-const tptp.f73 (-> |tptp.'S32'| |tptp.'S10'| |tptp.'S31'|)) % 56.22/56.45 (declare-const tptp.f34 (-> |tptp.'S17'| |tptp.'S3'| |tptp.'S3'|)) % 56.22/56.45 (declare-const tptp.f101 |tptp.'S47'|) % 56.22/56.45 (declare-const tptp.f35 |tptp.'S17'|) % 56.22/56.45 (declare-const tptp.f32 (-> |tptp.'S16'| Int |tptp.'S15'|)) % 56.22/56.45 (declare-const tptp.f33 |tptp.'S16'|) % 56.22/56.45 (declare-const tptp.f56 |tptp.'S22'|) % 56.22/56.45 (declare-const tptp.f82 |tptp.'S26'|) % 56.22/56.45 (declare-const tptp.f28 (-> |tptp.'S13'| Real Real)) % 56.22/56.45 (declare-const tptp.f16 |tptp.'S2'|) % 56.22/56.45 (declare-const tptp.f3 (-> |tptp.'S3'| |tptp.'S2'| |tptp.'S4'|)) % 56.22/56.45 (declare-const tptp.f12 |tptp.'S8'|) % 56.22/56.45 (declare-const tptp.f8 (-> |tptp.'S7'| |tptp.'S4'| |tptp.'S3'|)) % 56.22/56.45 (declare-const tptp.f13 (-> |tptp.'S9'| |tptp.'S2'| Int)) % 56.22/56.45 (declare-const tptp.f48 |tptp.'S13'|) % 56.22/56.45 (declare-const tptp.f119 |tptp.'S49'|) % 56.22/56.45 (declare-const tptp.f7 |tptp.'S6'|) % 56.22/56.45 (declare-const tptp.f129 |tptp.'S55'|) % 56.22/56.45 (declare-const tptp.f57 (-> |tptp.'S23'| |tptp.'S3'| |tptp.'S7'|)) % 56.22/56.45 (declare-const tptp.f22 (-> |tptp.'S10'| |tptp.'S2'| Real)) % 56.22/56.45 (declare-const tptp.f78 (-> |tptp.'S35'| |tptp.'S4'| |tptp.'S17'|)) % 56.22/56.45 (declare-const tptp.f25 |tptp.'S11'|) % 56.22/56.45 (declare-const tptp.f1 |tptp.'S1'|) % 56.22/56.45 (declare-const tptp.f15 |tptp.'S2'|) % 56.22/56.45 (declare-const tptp.f115 |tptp.'S49'|) % 56.22/56.45 (declare-const tptp.f14 |tptp.'S9'|) % 56.22/56.45 (declare-const tptp.f2 |tptp.'S1'|) % 56.22/56.45 (declare-const tptp.f58 |tptp.'S23'|) % 56.22/56.45 (declare-const tptp.f113 |tptp.'S41'|) % 56.22/56.45 (declare-const tptp.f6 (-> |tptp.'S6'| |tptp.'S4'| |tptp.'S5'|)) % 56.22/56.45 (declare-const tptp.f31 (-> |tptp.'S15'| Int Int)) % 56.22/56.45 (declare-const tptp.f17 |tptp.'S3'|) % 56.22/56.45 (declare-const tptp.f4 |tptp.'S3'|) % 56.22/56.45 (declare-const tptp.f9 |tptp.'S7'|) % 56.22/56.45 (declare-const tptp.f124 (-> |tptp.'S52'| |tptp.'S2'| |tptp.'S11'|)) % 56.22/56.45 (declare-const tptp.f27 |tptp.'S12'|) % 56.22/56.45 (declare-const tptp.f5 (-> |tptp.'S5'| |tptp.'S4'| |tptp.'S4'|)) % 56.22/56.45 (declare-const tptp.f26 (-> |tptp.'S12'| |tptp.'S10'| |tptp.'S10'|)) % 56.22/56.45 (declare-const tptp.f10 |tptp.'S3'|) % 56.22/56.45 (declare-const tptp.f19 |tptp.'S3'|) % 56.22/56.45 (declare-const tptp.f21 |tptp.'S3'|) % 56.22/56.45 (declare-const tptp.f24 (-> |tptp.'S11'| Real |tptp.'S10'|)) % 56.22/56.45 (declare-const tptp.f74 |tptp.'S32'|) % 56.22/56.45 (declare-const tptp.f23 |tptp.'S10'|) % 56.22/56.45 (declare-const tptp.f105 (-> |tptp.'S49'| |tptp.'S2'| |tptp.'S48'|)) % 56.22/56.45 (declare-const tptp.f50 |tptp.'S21'|) % 56.22/56.45 (declare-const tptp.f118 |tptp.'S43'|) % 56.22/56.45 (declare-const tptp.f30 |tptp.'S14'|) % 56.22/56.45 (declare-const tptp.f75 (-> |tptp.'S33'| |tptp.'S28'| Real)) % 56.22/56.45 (declare-const tptp.f18 |tptp.'S3'|) % 56.22/56.45 (declare-const tptp.f61 |tptp.'S24'|) % 56.22/56.45 (declare-const tptp.f11 (-> |tptp.'S8'| Int |tptp.'S2'|)) % 56.22/56.45 (declare-const tptp.f29 (-> |tptp.'S14'| Real |tptp.'S13'|)) % 56.22/56.45 (declare-const tptp.f104 (-> |tptp.'S48'| |tptp.'S2'| |tptp.'S20'|)) % 56.22/56.45 (declare-const tptp.f60 (-> |tptp.'S24'| |tptp.'S10'| |tptp.'S11'|)) % 56.22/56.45 (declare-const tptp.f62 |tptp.'S23'|) % 56.22/56.45 (declare-const tptp.f63 |tptp.'S24'|) % 56.22/56.45 (declare-const tptp.f70 (-> |tptp.'S30'| |tptp.'S2'| |tptp.'S28'|)) % 56.22/56.45 (declare-const tptp.f69 |tptp.'S29'|) % 56.22/56.45 (declare-const tptp.f68 (-> |tptp.'S29'| |tptp.'S3'| |tptp.'S27'|)) % 56.22/56.45 (declare-const tptp.f67 (-> |tptp.'S27'| |tptp.'S28'| |tptp.'S4'|)) % 56.22/56.45 (declare-const tptp.f66 |tptp.'S26'|) % 56.22/56.45 (declare-const tptp.f65 (-> |tptp.'S26'| |tptp.'S3'| |tptp.'S25'|)) % 56.22/56.45 (declare-const tptp.f102 |tptp.'S41'|) % 56.22/56.45 (declare-const tptp.f64 (-> |tptp.'S25'| |tptp.'S2'| |tptp.'S3'|)) % 56.22/56.45 (declare-const tptp.f77 |tptp.'S34'|) % 56.22/56.45 (declare-const tptp.f83 |tptp.'S32'|) % 56.22/56.45 (declare-const tptp.f76 (-> |tptp.'S34'| |tptp.'S10'| |tptp.'S33'|)) % 56.22/56.45 (declare-const tptp.f93 (-> |tptp.'S43'| Real |tptp.'S42'|)) % 56.22/56.45 (declare-const tptp.f72 (-> |tptp.'S31'| |tptp.'S2'| |tptp.'S10'|)) % 56.22/56.45 (declare-const tptp.f79 |tptp.'S35'|) % 56.22/56.45 (declare-const tptp.f81 |tptp.'S36'|) % 56.22/56.45 (declare-const tptp.f80 (-> |tptp.'S36'| Real |tptp.'S12'|)) % 56.22/56.45 (declare-const tptp.f117 |tptp.'S41'|) % 56.22/56.45 (declare-const tptp.f86 |tptp.'S38'|) % 56.22/56.45 (declare-const tptp.f85 (-> |tptp.'S38'| |tptp.'S9'| |tptp.'S37'|)) % 56.22/56.45 (declare-const tptp.f111 |tptp.'S43'|) % 56.22/56.45 (declare-const tptp.f84 (-> |tptp.'S37'| |tptp.'S2'| |tptp.'S9'|)) % 56.22/56.45 (declare-const tptp.f88 |tptp.'S39'|) % 56.22/56.45 (declare-const tptp.f87 (-> |tptp.'S39'| |tptp.'S2'| |tptp.'S12'|)) % 56.22/56.45 (declare-const tptp.f110 |tptp.'S41'|) % 56.22/56.45 (declare-const tptp.f91 |tptp.'S41'|) % 56.22/56.45 (declare-const tptp.f94 |tptp.'S43'|) % 56.22/56.45 (declare-const tptp.f92 (-> |tptp.'S42'| Real |tptp.'S31'|)) % 56.22/56.45 (declare-const tptp.f99 |tptp.'S46'|) % 56.22/56.45 (declare-const tptp.f98 (-> |tptp.'S46'| Int |tptp.'S9'|)) % 56.22/56.45 (declare-const tptp.f97 |tptp.'S45'|) % 56.22/56.45 (declare-const tptp.f96 (-> |tptp.'S45'| Int |tptp.'S44'|)) % 56.22/56.45 (declare-const tptp.f95 (-> |tptp.'S44'| Int |tptp.'S37'|)) % 56.22/56.45 (declare-const tptp.f100 (-> |tptp.'S47'| |tptp.'S2'| |tptp.'S26'|)) % 56.22/56.45 (declare-const tptp.f103 |tptp.'S43'|) % 56.22/56.45 (declare-const tptp.f108 |tptp.'S20'|) % 56.22/56.45 (declare-const tptp.f106 |tptp.'S49'|) % 56.22/56.45 (declare-const tptp.f109 |tptp.'S45'|) % 56.22/56.45 (declare-const tptp.f112 |tptp.'S45'|) % 56.22/56.45 (declare-const tptp.f114 |tptp.'S43'|) % 56.22/56.45 (declare-const tptp.f120 |tptp.'S45'|) % 56.22/56.45 (declare-const tptp.f123 |tptp.'S51'|) % 56.22/56.45 (declare-const tptp.f122 (-> |tptp.'S51'| |tptp.'S4'| |tptp.'S50'|)) % 56.22/56.45 (declare-const tptp.f121 (-> |tptp.'S50'| |tptp.'S2'| |tptp.'S7'|)) % 56.22/56.45 (declare-const tptp.f125 (-> |tptp.'S53'| Real |tptp.'S52'|)) % 56.22/56.45 (define @t1 () (@var "A__questionmark_v0" |tptp.'S2'|)) % 56.22/56.45 (define @t2 () (tptp.f13 tptp.f14 @t1)) % 56.22/56.45 (define @t3 () (* 2 @t2)) % 56.22/56.45 (define @t4 () (+ @t3 1)) % 56.22/56.45 (define @t5 () (tptp.f11 tptp.f12 @t4)) % 56.22/56.45 (define @t6 () (tptp.f3 tptp.f17 @t5)) % 56.22/56.45 (define @t7 () (tptp.f8 tptp.f9 (tptp.f3 (tptp.f8 tptp.f9 (tptp.f3 tptp.f10 tptp.f15)) tptp.f16))) % 56.22/56.45 (define @t8 () (tptp.f3 @t7 @t1)) % 56.22/56.45 (define @t9 () (tptp.f13 tptp.f14 tptp.f15)) % 56.22/56.45 (define @t10 () (tptp.f11 tptp.f12 (* 2 @t9))) % 56.22/56.45 (define @t11 () (tptp.f8 tptp.f9 (tptp.f3 tptp.f10 @t10))) % 56.22/56.45 (define @t12 () (tptp.f3 @t11 tptp.f16)) % 56.22/56.45 (define @t13 () (tptp.f6 tptp.f7 @t12)) % 56.22/56.45 (define @t14 () (tptp.f6 tptp.f7 (tptp.f5 @t13 @t8))) % 56.22/56.45 (define @t15 () (tptp.f5 @t14 @t6)) % 56.22/56.45 (define @t16 () (tptp.f3 tptp.f4 @t1)) % 56.22/56.45 (define @t17 () (= @t16 @t15)) % 56.22/56.45 (define @t18 () (@list @t1)) % 56.22/56.45 (define @t19 () (forall @t18 @t17)) % 56.22/56.45 (define @t20 () (@var "A__questionmark_v_0_1" Int)) % 56.22/56.45 (define @t21 () (tptp.f13 tptp.f14 tptp.f16)) % 56.22/56.45 (define @t22 () (@var "A__questionmark_v_0_2" Int)) % 56.22/56.45 (define @t23 () (tptp.f6 tptp.f7 @t8)) % 56.22/56.45 (define @t24 () (tptp.f5 @t23 @t6)) % 56.22/56.45 (define @t25 () (tptp.f5 @t13 @t24)) % 56.22/56.45 (define @t26 () (tptp.f3 tptp.f21 @t1)) % 56.22/56.45 (define @t27 () (= @t26 @t25)) % 56.22/56.45 (define @t28 () (forall @t18 @t27)) % 56.22/56.45 (define @t29 () (+ @t2 1)) % 56.22/56.45 (define @t30 () (tptp.f11 tptp.f12 @t29)) % 56.22/56.45 (define @t31 () (@var "A__questionmark_v1" |tptp.'S2'|)) % 56.22/56.45 (define @t32 () (@var "A__questionmark_v0" |tptp.'S10'|)) % 56.22/56.45 (define @t33 () (tptp.f22 @t32 @t31)) % 56.22/56.45 (define @t34 () (tptp.f26 tptp.f27 @t32)) % 56.22/56.45 (define @t35 () (@list @t32 @t31)) % 56.22/56.45 (define @t36 () (@var "A__questionmark_v1" Real)) % 56.22/56.45 (define @t37 () (@var "A__questionmark_v0" Real)) % 56.22/56.45 (define @t38 () (* @t37 @t36)) % 56.22/56.45 (define @t39 () (@list @t37 @t36)) % 56.22/56.45 (define @t40 () (@var "A__questionmark_v1" Int)) % 56.22/56.45 (define @t41 () (@var "A__questionmark_v0" Int)) % 56.22/56.45 (define @t42 () (* @t41 @t40)) % 56.22/56.45 (define @t43 () (@list @t41 @t40)) % 56.22/56.45 (define @t44 () (tptp.f13 tptp.f14 @t31)) % 56.22/56.45 (define @t45 () (* 2 @t44)) % 56.22/56.45 (define @t46 () (tptp.f11 tptp.f12 (+ @t45 1))) % 56.22/56.45 (define @t47 () (@var "A__questionmark_v0" |tptp.'S3'|)) % 56.22/56.45 (define @t48 () (tptp.f34 tptp.f35 @t47)) % 56.22/56.45 (define @t49 () (@list @t47 @t31)) % 56.22/56.45 (define @t50 () (tptp.f26 tptp.f36 @t32)) % 56.22/56.45 (define @t51 () (@var "A__questionmark_v0" |tptp.'S9'|)) % 56.22/56.45 (define @t52 () (tptp.f37 tptp.f38 @t51)) % 56.22/56.45 (define @t53 () (@list @t51 @t31)) % 56.22/56.45 (define @t54 () (tptp.f11 tptp.f12 @t45)) % 56.22/56.45 (define @t55 () (tptp.f34 tptp.f39 @t47)) % 56.22/56.45 (define @t56 () (tptp.f26 tptp.f40 @t32)) % 56.22/56.45 (define @t57 () (tptp.f37 tptp.f41 @t51)) % 56.22/56.45 (define @t58 () (tptp.f11 tptp.f12 (+ @t44 1))) % 56.22/56.45 (define @t59 () (tptp.f34 tptp.f42 @t47)) % 56.22/56.45 (define @t60 () (tptp.f26 tptp.f43 @t32)) % 56.22/56.45 (define @t61 () (tptp.f11 tptp.f12 (* @t2 @t44))) % 56.22/56.45 (define @t62 () (@list @t1 @t31)) % 56.22/56.45 (define @t63 () (tptp.f26 tptp.f47 @t32)) % 56.22/56.45 (define @t64 () (@var "A__questionmark_v2" |tptp.'S2'|)) % 56.22/56.45 (define @t65 () (@var "A__questionmark_v1" |tptp.'S3'|)) % 56.22/56.45 (define @t66 () (tptp.f3 @t65 @t64)) % 56.22/56.45 (define @t67 () (tptp.f3 @t47 @t64)) % 56.22/56.45 (define @t68 () (tptp.f34 (tptp.f49 tptp.f50 @t47) @t65)) % 56.22/56.45 (define @t69 () (@list @t47 @t65 @t64)) % 56.22/56.45 (define @t70 () (@var "A__questionmark_v1" |tptp.'S10'|)) % 56.22/56.45 (define @t71 () (tptp.f22 @t70 @t64)) % 56.22/56.45 (define @t72 () (tptp.f22 @t32 @t64)) % 56.22/56.45 (define @t73 () (tptp.f26 (tptp.f52 tptp.f53 @t32) @t70)) % 56.22/56.45 (define @t74 () (@list @t32 @t70 @t64)) % 56.22/56.45 (define @t75 () (tptp.f34 (tptp.f49 tptp.f54 @t47) @t65)) % 56.22/56.45 (define @t76 () (tptp.f26 (tptp.f52 tptp.f56 @t32) @t70)) % 56.22/56.45 (define @t77 () (@var "A__questionmark_v1" |tptp.'S4'|)) % 56.22/56.45 (define @t78 () (tptp.f57 tptp.f58 @t47)) % 56.22/56.45 (define @t79 () (@list @t47 @t77 @t64)) % 56.22/56.45 (define @t80 () (tptp.f60 tptp.f61 @t32)) % 56.22/56.45 (define @t81 () (@list @t32 @t36 @t64)) % 56.22/56.45 (define @t82 () (tptp.f57 tptp.f62 @t47)) % 56.22/56.45 (define @t83 () (tptp.f60 tptp.f63 @t32)) % 56.22/56.45 (define @t84 () (@var "A__questionmark_v_1_3" Int)) % 56.22/56.45 (define @t85 () (@var "A__questionmark_v_0_4" Int)) % 56.22/56.45 (define @t86 () (tptp.f68 tptp.f69 @t47)) % 56.22/56.45 (define @t87 () (tptp.f64 (tptp.f65 tptp.f66 @t47) @t31)) % 56.22/56.45 (define @t88 () (tptp.f13 tptp.f14 @t64)) % 56.22/56.45 (define @t89 () (@list @t47 @t31 @t64)) % 56.22/56.45 (define @t90 () (@var "A__questionmark_v_1_5" Int)) % 56.22/56.45 (define @t91 () (@var "A__questionmark_v_0_6" Int)) % 56.22/56.45 (define @t92 () (tptp.f76 tptp.f77 @t32)) % 56.22/56.45 (define @t93 () (tptp.f72 (tptp.f73 tptp.f74 @t32) @t31)) % 56.22/56.45 (define @t94 () (@list @t32 @t31 @t64)) % 56.22/56.45 (define @t95 () (@var "A__questionmark_v0" |tptp.'S4'|)) % 56.22/56.45 (define @t96 () (tptp.f6 tptp.f7 @t95)) % 56.22/56.45 (define @t97 () (tptp.f34 (tptp.f78 tptp.f79 @t95) @t65)) % 56.22/56.45 (define @t98 () (tptp.f26 (tptp.f80 tptp.f81 @t37) @t70)) % 56.22/56.45 (define @t99 () (tptp.f11 tptp.f12 (+ @t88 @t44))) % 56.22/56.45 (define @t100 () (tptp.f65 tptp.f82 @t47)) % 56.22/56.45 (define @t101 () (tptp.f64 @t100 @t31)) % 56.22/56.45 (define @t102 () (tptp.f73 tptp.f83 @t32)) % 56.22/56.45 (define @t103 () (tptp.f72 @t102 @t31)) % 56.22/56.45 (define @t104 () (tptp.f85 tptp.f86 @t51)) % 56.22/56.45 (define @t105 () (tptp.f84 @t104 @t31)) % 56.22/56.45 (define @t106 () (@list @t51 @t31 @t64)) % 56.22/56.45 (define @t107 () (tptp.f87 tptp.f88 @t1)) % 56.22/56.45 (define @t108 () (@var "A__questionmark_v_0_7" |tptp.'S3'|)) % 56.22/56.45 (define @t109 () (@var "A__questionmark_v3" |tptp.'S2'|)) % 56.22/56.45 (define @t110 () (tptp.f13 tptp.f14 @t109)) % 56.22/56.45 (define @t111 () (tptp.f11 tptp.f12 (- @t88 @t110))) % 56.22/56.45 (define @t112 () (tptp.f6 tptp.f55 @t95)) % 56.22/56.45 (define @t113 () (tptp.f5 @t112 @t77)) % 56.22/56.45 (define @t114 () (tptp.f8 tptp.f9 @t113)) % 56.22/56.45 (define @t115 () (tptp.f64 (tptp.f89 (tptp.f90 tptp.f91 @t95) @t77) @t64)) % 56.22/56.45 (define @t116 () (tptp.f8 tptp.f9 @t95)) % 56.22/56.45 (define @t117 () (@list @t95 @t77 @t64 @t109)) % 56.22/56.45 (define @t118 () (@var "A__questionmark_v_0_8" |tptp.'S10'|)) % 56.22/56.45 (define @t119 () (+ @t37 @t36)) % 56.22/56.45 (define @t120 () (tptp.f24 tptp.f25 @t119)) % 56.22/56.45 (define @t121 () (tptp.f72 (tptp.f92 (tptp.f93 tptp.f94 @t37) @t36) @t64)) % 56.22/56.45 (define @t122 () (tptp.f24 tptp.f25 @t37)) % 56.22/56.45 (define @t123 () (@list @t37 @t36 @t64 @t109)) % 56.22/56.45 (define @t124 () (@var "A__questionmark_v_0_9" |tptp.'S9'|)) % 56.22/56.45 (define @t125 () (+ @t41 @t40)) % 56.22/56.45 (define @t126 () (tptp.f98 tptp.f99 @t125)) % 56.22/56.45 (define @t127 () (tptp.f84 (tptp.f95 (tptp.f96 tptp.f97 @t41) @t40) @t64)) % 56.22/56.45 (define @t128 () (tptp.f98 tptp.f99 @t41)) % 56.22/56.45 (define @t129 () (@list @t41 @t40 @t64 @t109)) % 56.22/56.45 (define @t130 () (tptp.f3 @t65 @t109)) % 56.22/56.45 (define @t131 () (tptp.f3 tptp.f10 @t1)) % 56.22/56.45 (define @t132 () (tptp.f8 tptp.f9 @t131)) % 56.22/56.45 (define @t133 () (tptp.f3 @t132 (tptp.f11 tptp.f12 (* @t88 @t110)))) % 56.22/56.45 (define @t134 () (tptp.f64 (tptp.f65 (tptp.f100 tptp.f101 @t1) @t65) @t64)) % 56.22/56.45 (define @t135 () (@list @t1 @t65 @t64 @t109)) % 56.22/56.45 (define @t136 () (tptp.f8 tptp.f9 @t77)) % 56.22/56.45 (define @t137 () (tptp.f64 (tptp.f89 (tptp.f90 tptp.f102 @t95) @t77) @t64)) % 56.22/56.45 (define @t138 () (tptp.f24 tptp.f25 @t36)) % 56.22/56.45 (define @t139 () (tptp.f72 (tptp.f92 (tptp.f93 tptp.f103 @t37) @t36) @t64)) % 56.22/56.45 (define @t140 () (tptp.f45 tptp.f108 @t31)) % 56.22/56.45 (define @t141 () (tptp.f45 tptp.f108 @t1)) % 56.22/56.45 (define @t142 () (tptp.f45 (tptp.f104 (tptp.f105 tptp.f106 @t1) @t31) @t64)) % 56.22/56.45 (define @t143 () (@list @t1 @t31 @t64 @t109)) % 56.22/56.45 (define @t144 () (tptp.f98 tptp.f99 @t40)) % 56.22/56.45 (define @t145 () (tptp.f84 (tptp.f95 (tptp.f96 tptp.f109 @t41) @t40) @t64)) % 56.22/56.45 (define @t146 () (@var "A__questionmark_v_1_11" |tptp.'S2'|)) % 56.22/56.45 (define @t147 () (@var "A__questionmark_v_0_10" |tptp.'S3'|)) % 56.22/56.45 (define @t148 () (tptp.f64 (tptp.f89 (tptp.f90 tptp.f110 @t95) @t77) @t64)) % 56.22/56.45 (define @t149 () (@var "A__questionmark_v_1_13" |tptp.'S2'|)) % 56.22/56.45 (define @t150 () (@var "A__questionmark_v_0_12" |tptp.'S10'|)) % 56.22/56.45 (define @t151 () (tptp.f72 (tptp.f92 (tptp.f93 tptp.f111 @t37) @t36) @t64)) % 56.22/56.45 (define @t152 () (@var "A__questionmark_v_1_15" |tptp.'S2'|)) % 56.22/56.45 (define @t153 () (@var "A__questionmark_v_0_14" |tptp.'S9'|)) % 56.22/56.45 (define @t154 () (tptp.f84 (tptp.f95 (tptp.f96 tptp.f112 @t41) @t40) @t64)) % 56.22/56.45 (define @t155 () (+ @t88 1)) % 56.22/56.45 (define @t156 () (tptp.f11 tptp.f12 (- @t155 @t110))) % 56.22/56.45 (define @t157 () (tptp.f6 tptp.f7 (tptp.f3 @t116 @t109))) % 56.22/56.45 (define @t158 () (tptp.f64 (tptp.f89 (tptp.f90 tptp.f113 @t95) @t77) @t64)) % 56.22/56.45 (define @t159 () (tptp.f22 @t122 @t109)) % 56.22/56.45 (define @t160 () (tptp.f72 (tptp.f92 (tptp.f93 tptp.f114 @t37) @t36) @t64)) % 56.22/56.45 (define @t161 () (tptp.f45 tptp.f107 (tptp.f44 @t141 @t109))) % 56.22/56.45 (define @t162 () (tptp.f45 (tptp.f104 (tptp.f105 tptp.f115 @t1) @t31) @t64)) % 56.22/56.45 (define @t163 () (tptp.f13 @t128 @t109)) % 56.22/56.45 (define @t164 () (tptp.f84 (tptp.f95 (tptp.f96 tptp.f116 @t41) @t40) @t64)) % 56.22/56.45 (define @t165 () (tptp.f64 (tptp.f89 (tptp.f90 tptp.f117 @t95) @t77) @t64)) % 56.22/56.45 (define @t166 () (tptp.f72 (tptp.f92 (tptp.f93 tptp.f118 @t37) @t36) @t64)) % 56.22/56.45 (define @t167 () (tptp.f45 (tptp.f104 (tptp.f105 tptp.f119 @t1) @t31) @t64)) % 56.22/56.45 (define @t168 () (tptp.f84 (tptp.f95 (tptp.f96 tptp.f120 @t41) @t40) @t64)) % 56.22/56.45 (define @t169 () (tptp.f11 tptp.f12 (- @t44 @t110))) % 56.22/56.45 (define @t170 () (@var "A__questionmark_v2" |tptp.'S4'|)) % 56.22/56.45 (define @t171 () (tptp.f8 tptp.f9 @t170)) % 56.22/56.45 (define @t172 () (tptp.f8 (tptp.f121 (tptp.f122 tptp.f123 @t95) @t31) @t170)) % 56.22/56.45 (define @t173 () (@var "A__questionmark_v2" Real)) % 56.22/56.45 (define @t174 () (tptp.f24 tptp.f25 @t173)) % 56.22/56.45 (define @t175 () (tptp.f24 (tptp.f124 (tptp.f125 tptp.f126 @t37) @t31) @t173)) % 56.22/56.45 (define @t176 () (@var "A__questionmark_v2" Int)) % 56.22/56.45 (define @t177 () (tptp.f98 tptp.f99 @t176)) % 56.22/56.45 (define @t178 () (tptp.f98 (tptp.f127 (tptp.f128 tptp.f129 @t41) @t31) @t176)) % 56.22/56.45 (define @t179 () (tptp.f64 (tptp.f65 (tptp.f100 tptp.f130 @t1) @t65) @t64)) % 56.22/56.45 (define @t180 () (@var "A__questionmark_v_0_16" |tptp.'S28'|)) % 56.22/56.45 (define @t181 () (tptp.f68 tptp.f69 tptp.f21)) % 56.22/56.45 (define @t182 () (tptp.f68 tptp.f69 tptp.f4)) % 56.22/56.45 (define @t183 () (= (tptp.f67 @t182 @t180) (tptp.f67 @t181 @t180))) % 56.22/56.45 (define @t184 () (not @t183)) % 56.22/56.45 (define @t185 () (tptp.f11 tptp.f12 0)) % 56.22/56.45 (define @t186 () (tptp.f71 @t185)) % 56.22/56.45 (define @t187 () (tptp.f70 @t186 tptp.f15)) % 56.22/56.45 (define @t188 () (= @t180 @t187)) % 56.22/56.45 (define @t189 () (and @t188 @t184)) % 56.22/56.45 (define @t190 () (@list @t180)) % 56.22/56.45 (define @t191 () (exists @t190 @t189)) % 56.22/56.45 (define @t192 () (@var "A__questionmark_v_1_18" Int)) % 56.22/56.45 (define @t193 () (@var "A__questionmark_v_0_17" Int)) % 56.22/56.45 (define @t194 () (tptp.f11 tptp.f12 @t3)) % 56.22/56.45 (define @t195 () (@list @t1 @t31 @t64)) % 56.22/56.45 (define @t196 () (tptp.f3 tptp.f10 @t31)) % 56.22/56.45 (define @t197 () (tptp.f8 tptp.f9 @t196)) % 56.22/56.45 (define @t198 () (@var "A__questionmark_v_0_19" Int)) % 56.22/56.45 (define @t199 () (@var "A__questionmark_v_1_21" |tptp.'S28'|)) % 56.22/56.45 (define @t200 () (@var "A__questionmark_v_0_20" |tptp.'S30'|)) % 56.22/56.45 (define @t201 () (tptp.f70 @t186 @t1)) % 56.22/56.45 (define @t202 () (tptp.f134 tptp.f135 @t1)) % 56.22/56.45 (define @t203 () (@list @t1 @t65 @t64)) % 56.22/56.45 (define @t204 () (@var "A__questionmark_v_0_22" |tptp.'S28'|)) % 56.22/56.45 (define @t205 () (tptp.f137 tptp.f138 @t167)) % 56.22/56.45 (define @t206 () (tptp.f11 tptp.f12 @t155)) % 56.22/56.45 (define @t207 () (tptp.f70 @t186 @t206)) % 56.22/56.45 (define @t208 () (@var "A__questionmark_v_0_23" |tptp.'S28'|)) % 56.22/56.45 (define @t209 () (tptp.f76 tptp.f77 @t166)) % 56.22/56.45 (define @t210 () (@list @t37 @t36 @t64)) % 56.22/56.45 (define @t211 () (@var "A__questionmark_v_0_24" |tptp.'S28'|)) % 56.22/56.45 (define @t212 () (tptp.f68 tptp.f69 @t165)) % 56.22/56.45 (define @t213 () (@list @t95 @t77 @t64)) % 56.22/56.45 (define @t214 () (@var "A__questionmark_v_0_25" |tptp.'S28'|)) % 56.22/56.45 (define @t215 () (tptp.f140 tptp.f141 @t168)) % 56.22/56.45 (define @t216 () (@list @t41 @t40 @t64)) % 56.22/56.45 (define @t217 () (@var "A__questionmark_v_0_26" |tptp.'S28'|)) % 56.22/56.45 (define @t218 () (@var "A__questionmark_v_0_27" |tptp.'S28'|)) % 56.22/56.45 (define @t219 () (@var "A__questionmark_v_0_28" |tptp.'S28'|)) % 56.22/56.45 (define @t220 () (tptp.f6 tptp.f7 @t77)) % 56.22/56.45 (define @t221 () (@var "A__questionmark_v_0_29" |tptp.'S28'|)) % 56.22/56.45 (define @t222 () (tptp.f11 tptp.f12 (* @t88 @t44))) % 56.22/56.45 (define @t223 () (@var "A__questionmark_v_0_30" |tptp.'S30'|)) % 56.22/56.45 (define @t224 () (@var "A__questionmark_v_0_31" |tptp.'S30'|)) % 56.22/56.45 (define @t225 () (tptp.f11 tptp.f12 2)) % 56.22/56.45 (define @t226 () (@var "A__questionmark_v_0_32" |tptp.'S19'|)) % 56.22/56.45 (define @t227 () (tptp.f45 tptp.f107 @t1)) % 56.22/56.45 (define @t228 () (@var "A__questionmark_v_0_33" |tptp.'S10'|)) % 56.22/56.45 (define @t229 () (@list @t37 @t31)) % 56.22/56.45 (define @t230 () (@var "A__questionmark_v_0_34" |tptp.'S3'|)) % 56.22/56.45 (define @t231 () (@list @t95 @t31)) % 56.22/56.45 (define @t232 () (@var "A__questionmark_v_0_35" |tptp.'S9'|)) % 56.22/56.45 (define @t233 () (@list @t41 @t31)) % 56.22/56.45 (define @t234 () (@var "A__questionmark_v_1_37" |tptp.'S2'|)) % 56.22/56.45 (define @t235 () (@var "A__questionmark_v_0_36" |tptp.'S19'|)) % 56.22/56.45 (define @t236 () (@var "A__questionmark_v_1_39" Real)) % 56.22/56.45 (define @t237 () (@var "A__questionmark_v_0_38" |tptp.'S10'|)) % 56.22/56.45 (define @t238 () (@var "A__questionmark_v_1_41" |tptp.'S4'|)) % 56.22/56.45 (define @t239 () (@var "A__questionmark_v_0_40" |tptp.'S3'|)) % 56.22/56.45 (define @t240 () (@var "A__questionmark_v_1_43" Int)) % 56.22/56.45 (define @t241 () (@var "A__questionmark_v_0_42" |tptp.'S9'|)) % 56.22/56.45 (define @t242 () (@var "A__questionmark_v_1_45" |tptp.'S2'|)) % 56.22/56.45 (define @t243 () (@var "A__questionmark_v_0_44" |tptp.'S19'|)) % 56.22/56.45 (define @t244 () (@var "A__questionmark_v_1_47" Real)) % 56.22/56.45 (define @t245 () (@var "A__questionmark_v_0_46" |tptp.'S10'|)) % 56.22/56.45 (define @t246 () (@var "A__questionmark_v_1_49" |tptp.'S4'|)) % 56.22/56.45 (define @t247 () (@var "A__questionmark_v_0_48" |tptp.'S3'|)) % 56.22/56.45 (define @t248 () (@var "A__questionmark_v_1_51" Int)) % 56.22/56.45 (define @t249 () (@var "A__questionmark_v_0_50" |tptp.'S9'|)) % 56.22/56.45 (define @t250 () (tptp.f71 @t31)) % 56.22/56.45 (define @t251 () (tptp.f70 @t250 @t64)) % 56.22/56.45 (define @t252 () (tptp.f70 (tptp.f71 @t58) @t206)) % 56.22/56.45 (define @t253 () (tptp.f70 @t250 @t109)) % 56.22/56.45 (define @t254 () (tptp.f76 tptp.f77 (tptp.f72 @t102 @t64))) % 56.22/56.45 (define @t255 () (@var "A__questionmark_v_0_52" Int)) % 56.22/56.45 (define @t256 () (tptp.f68 tptp.f69 (tptp.f64 @t100 @t64))) % 56.22/56.45 (define @t257 () (@var "A__questionmark_v_0_53" Int)) % 56.22/56.45 (define @t258 () (@var "A__questionmark_v2" |tptp.'S28'|)) % 56.22/56.45 (define @t259 () (tptp.f76 tptp.f77 @t70)) % 56.22/56.45 (define @t260 () (tptp.f75 @t259 @t258)) % 56.22/56.45 (define @t261 () (tptp.f68 tptp.f69 @t65)) % 56.22/56.45 (define @t262 () (tptp.f67 @t261 @t258)) % 56.22/56.45 (define @t263 () (tptp.f6 tptp.f55 @t77)) % 56.22/56.45 (define @t264 () (@list @t95 @t77)) % 56.22/56.45 (define @t265 () (+ @t37 @t173)) % 56.22/56.45 (define @t266 () (+ @t36 @t173)) % 56.22/56.45 (define @t267 () (+ @t37 @t266)) % 56.22/56.45 (define @t268 () (@list @t37 @t36 @t173)) % 56.22/56.45 (define @t269 () (@var "A__questionmark_v_1_54" |tptp.'S5'|)) % 56.22/56.45 (define @t270 () (@var "A__questionmark_v_0_55" |tptp.'S5'|)) % 56.22/56.45 (define @t271 () (@list @t95 @t77 @t170)) % 56.22/56.45 (define @t272 () (+ @t41 @t176)) % 56.22/56.45 (define @t273 () (+ @t40 @t176)) % 56.22/56.45 (define @t274 () (+ @t41 @t273)) % 56.22/56.45 (define @t275 () (@list @t41 @t40 @t176)) % 56.22/56.45 (define @t276 () (+ @t119 @t173)) % 56.22/56.45 (define @t277 () (@var "A__questionmark_v_0_56" |tptp.'S5'|)) % 56.22/56.45 (define @t278 () (tptp.f5 @t263 @t170)) % 56.22/56.45 (define @t279 () (+ @t125 @t176)) % 56.22/56.45 (define @t280 () (@var "A__questionmark_v_0_57" |tptp.'S5'|)) % 56.22/56.45 (define @t281 () (@var "A__questionmark_v_0_58" |tptp.'S5'|)) % 56.22/56.45 (define @t282 () (@var "A__questionmark_v3" Real)) % 56.22/56.45 (define @t283 () (+ @t173 @t282)) % 56.22/56.45 (define @t284 () (@list @t37 @t36 @t173 @t282)) % 56.22/56.45 (define @t285 () (@var "A__questionmark_v3" |tptp.'S4'|)) % 56.22/56.45 (define @t286 () (@var "A__questionmark_v_0_59" |tptp.'S5'|)) % 56.22/56.45 (define @t287 () (tptp.f6 tptp.f55 @t170)) % 56.22/56.45 (define @t288 () (tptp.f5 @t287 @t285)) % 56.22/56.45 (define @t289 () (@list @t95 @t77 @t170 @t285)) % 56.22/56.45 (define @t290 () (@var "A__questionmark_v3" Int)) % 56.22/56.45 (define @t291 () (+ @t176 @t290)) % 56.22/56.45 (define @t292 () (@list @t41 @t40 @t176 @t290)) % 56.22/56.45 (define @t293 () (@var "A__questionmark_v_1_60" Real)) % 56.22/56.45 (define @t294 () (@var "A__questionmark_v_0_61" |tptp.'S10'|)) % 56.22/56.45 (define @t295 () (tptp.f70 @t186 @t31)) % 56.22/56.45 (define @t296 () (+ 0 1)) % 56.22/56.45 (define @t297 () (tptp.f11 tptp.f12 @t296)) % 56.22/56.45 (define @t298 () (tptp.f70 (tptp.f71 @t297) @t31)) % 56.22/56.45 (define @t299 () (* @t173 @t36)) % 56.22/56.45 (define @t300 () (* @t37 @t282)) % 56.22/56.45 (define @t301 () (* @t173 @t282)) % 56.22/56.45 (define @t302 () (@var "A__questionmark_v_1_63" |tptp.'S5'|)) % 56.22/56.45 (define @t303 () (@var "A__questionmark_v_0_62" |tptp.'S5'|)) % 56.22/56.45 (define @t304 () (tptp.f6 tptp.f7 @t170)) % 56.22/56.45 (define @t305 () (* @t176 @t40)) % 56.22/56.45 (define @t306 () (* @t41 @t290)) % 56.22/56.45 (define @t307 () (* @t176 @t290)) % 56.22/56.45 (define @t308 () (* @t265 @t36)) % 56.22/56.45 (define @t309 () (tptp.f5 (tptp.f6 tptp.f7 (tptp.f5 @t112 @t170)) @t77)) % 56.22/56.45 (define @t310 () (tptp.f5 @t304 @t77)) % 56.22/56.45 (define @t311 () (tptp.f5 @t96 @t77)) % 56.22/56.45 (define @t312 () (tptp.f6 tptp.f55 @t311)) % 56.22/56.45 (define @t313 () (* @t272 @t40)) % 56.22/56.45 (define @t314 () (* @t36 @t173)) % 56.22/56.45 (define @t315 () (* @t37 @t173)) % 56.22/56.45 (define @t316 () (tptp.f5 @t220 @t170)) % 56.22/56.45 (define @t317 () (tptp.f5 @t96 @t170)) % 56.22/56.45 (define @t318 () (* @t40 @t176)) % 56.22/56.45 (define @t319 () (* @t41 @t176)) % 56.22/56.45 (define @t320 () (* @t36 @t282)) % 56.22/56.45 (define @t321 () (@var "A__questionmark_v_1_65" |tptp.'S5'|)) % 56.22/56.45 (define @t322 () (@var "A__questionmark_v_0_64" |tptp.'S5'|)) % 56.22/56.45 (define @t323 () (* @t40 @t290)) % 56.22/56.45 (define @t324 () (@var "A__questionmark_v_0_66" |tptp.'S5'|)) % 56.22/56.45 (define @t325 () (@var "A__questionmark_v_0_67" |tptp.'S5'|)) % 56.22/56.45 (define @t326 () (@var "A__questionmark_v_0_68" |tptp.'S5'|)) % 56.22/56.45 (define @t327 () (@var "A__questionmark_v_0_69" |tptp.'S19'|)) % 56.22/56.45 (define @t328 () (tptp.f44 @t327 @t31)) % 56.22/56.45 (define @t329 () (= @t31 @t185)) % 56.22/56.45 (define @t330 () (not @t329)) % 56.22/56.45 (define @t331 () (tptp.f11 tptp.f12 1)) % 56.22/56.45 (define @t332 () (@var "A__questionmark_v_0_70" |tptp.'S30'|)) % 56.22/56.45 (define @t333 () (@var "A__questionmark_v_1_71" |tptp.'S33'|)) % 56.22/56.45 (define @t334 () (tptp.f11 tptp.f12 (+ @t44 @t2))) % 56.22/56.45 (define @t335 () (@var "A__questionmark_v2" |tptp.'S10'|)) % 56.22/56.45 (define @t336 () (tptp.f76 tptp.f77 (tptp.f26 @t107 @t335))) % 56.22/56.45 (define @t337 () (tptp.f76 tptp.f77 @t335)) % 56.22/56.45 (define @t338 () (@list @t1 @t31 @t335)) % 56.22/56.45 (define @t339 () (@var "A__questionmark_v_0_72" |tptp.'S30'|)) % 56.22/56.45 (define @t340 () (@var "A__questionmark_v_1_73" |tptp.'S33'|)) % 56.22/56.45 (define @t341 () (tptp.f75 @t92 @t258)) % 56.22/56.45 (define @t342 () (@list @t32 @t70 @t258)) % 56.22/56.45 (define @t343 () (tptp.f67 @t86 @t258)) % 56.22/56.45 (define @t344 () (@list @t47 @t65 @t258)) % 56.22/56.45 (define @t345 () (@var "A__questionmark_v_2_76" |tptp.'S30'|)) % 56.22/56.45 (define @t346 () (@var "A__questionmark_v_1_75" |tptp.'S33'|)) % 56.22/56.45 (define @t347 () (@var "A__questionmark_v_0_74" Int)) % 56.22/56.45 (define @t348 () (tptp.f71 @t1)) % 56.22/56.45 (define @t349 () (@var "A__questionmark_v3" |tptp.'S10'|)) % 56.22/56.45 (define @t350 () (tptp.f76 tptp.f77 @t349)) % 56.22/56.45 (define @t351 () (@list @t1 @t31 @t64 @t349)) % 56.22/56.45 (define @t352 () (@var "A__questionmark_v_2_79" |tptp.'S30'|)) % 56.22/56.45 (define @t353 () (@var "A__questionmark_v_1_78" |tptp.'S27'|)) % 56.22/56.45 (define @t354 () (@var "A__questionmark_v_0_77" Int)) % 56.22/56.45 (define @t355 () (@var "A__questionmark_v3" |tptp.'S3'|)) % 56.22/56.45 (define @t356 () (tptp.f68 tptp.f69 @t355)) % 56.22/56.45 (define @t357 () (@list @t1 @t31 @t64 @t355)) % 56.22/56.45 (define @t358 () (@var "A__questionmark_v_2_82" |tptp.'S30'|)) % 56.22/56.45 (define @t359 () (@var "A__questionmark_v_1_81" |tptp.'S59'|)) % 56.22/56.45 (define @t360 () (@var "A__questionmark_v_0_80" Int)) % 56.22/56.45 (define @t361 () (@var "A__questionmark_v3" |tptp.'S9'|)) % 56.22/56.45 (define @t362 () (tptp.f140 tptp.f141 @t361)) % 56.22/56.45 (define @t363 () (@list @t1 @t31 @t64 @t361)) % 56.22/56.45 (define @t364 () (@var "A__questionmark_v_1_83" Int)) % 56.22/56.45 (define @t365 () (@var "A__questionmark_v_0_84" |tptp.'S33'|)) % 56.22/56.45 (define @t366 () (tptp.f70 @t348 @t31)) % 56.22/56.45 (define @t367 () (@var "A__questionmark_v_1_85" Int)) % 56.22/56.45 (define @t368 () (@var "A__questionmark_v_0_86" |tptp.'S27'|)) % 56.22/56.45 (define @t369 () (@var "A__questionmark_v2" |tptp.'S3'|)) % 56.22/56.45 (define @t370 () (tptp.f68 tptp.f69 @t369)) % 56.22/56.45 (define @t371 () (@var "A__questionmark_v_1_87" Int)) % 56.22/56.45 (define @t372 () (@var "A__questionmark_v_0_88" |tptp.'S59'|)) % 56.22/56.45 (define @t373 () (@var "A__questionmark_v2" |tptp.'S9'|)) % 56.22/56.45 (define @t374 () (@var "A__questionmark_v_0_89" |tptp.'S30'|)) % 56.22/56.45 (define @t375 () (@var "A__questionmark_v_1_90" |tptp.'S33'|)) % 56.22/56.45 (define @t376 () (tptp.f11 tptp.f12 (+ @t44 @t88))) % 56.22/56.45 (define @t377 () (@var "A__questionmark_v_0_91" |tptp.'S30'|)) % 56.22/56.45 (define @t378 () (@var "A__questionmark_v_1_92" |tptp.'S27'|)) % 56.22/56.45 (define @t379 () (@var "A__questionmark_v_0_93" |tptp.'S30'|)) % 56.22/56.45 (define @t380 () (@var "A__questionmark_v_1_94" |tptp.'S59'|)) % 56.22/56.45 (define @t381 () (tptp.f140 tptp.f141 @t51)) % 56.22/56.45 (define @t382 () (tptp.f11 tptp.f12 3)) % 56.22/56.45 (define @t383 () (@var "A__questionmark_v_0_95" |tptp.'S2'|)) % 56.22/56.45 (define @t384 () (tptp.f11 tptp.f12 4)) % 56.22/56.45 (define @t385 () (@var "A__questionmark_v_0_96" |tptp.'S2'|)) % 56.22/56.45 (define @t386 () (@var "A__questionmark_v_0_97" |tptp.'S2'|)) % 56.22/56.45 (define @t387 () (tptp.f5 @t220 @t285)) % 56.22/56.45 (define @t388 () (@var "A__questionmark_v_0_98" |tptp.'S5'|)) % 56.22/56.45 (define @t389 () (tptp.f5 @t304 @t285)) % 56.22/56.45 (define @t390 () (@var "A__questionmark_v_0_99" Real)) % 56.22/56.45 (define @t391 () (@var "A__questionmark_v_0_100" Int)) % 56.22/56.45 (define @t392 () (@var "A__questionmark_v_1_101" |tptp.'S5'|)) % 56.22/56.45 (define @t393 () (@var "A__questionmark_v_0_102" |tptp.'S5'|)) % 56.22/56.45 (define @t394 () (tptp.f6 tptp.f7 @t311)) % 56.22/56.45 (define @t395 () (@var "A__questionmark_v_0_103" Real)) % 56.22/56.45 (define @t396 () (@var "A__questionmark_v_0_104" Int)) % 56.22/56.45 (define @t397 () (@var "A__questionmark_v_1_106" |tptp.'S4'|)) % 56.22/56.45 (define @t398 () (@var "A__questionmark_v_0_105" |tptp.'S5'|)) % 56.22/56.45 (define @t399 () (* @t38 @t173)) % 56.22/56.45 (define @t400 () (* @t42 @t176)) % 56.22/56.45 (define @t401 () (@var "A__questionmark_v_0_107" |tptp.'S5'|)) % 56.22/56.45 (define @t402 () (* @t37 @t314)) % 56.22/56.45 (define @t403 () (* @t41 @t318)) % 56.22/56.45 (define @t404 () (@var "A__questionmark_v_0_108" |tptp.'S5'|)) % 56.22/56.45 (define @t405 () (= (tptp.f5 (tptp.f6 tptp.f7 (tptp.f5 @t404 @t77)) @t170) (tptp.f5 @t404 @t316))) % 56.22/56.45 (define @t406 () (= @t404 @t96)) % 56.22/56.45 (define @t407 () (and @t406 @t405)) % 56.22/56.45 (define @t408 () (@list @t404)) % 56.22/56.45 (define @t409 () (exists @t408 @t407)) % 56.22/56.45 (define @t410 () (forall @t271 @t409)) % 56.22/56.45 (define @t411 () (@var "A__questionmark_v_0_109" |tptp.'S5'|)) % 56.22/56.45 (define @t412 () (@var "A__questionmark_v_1_110" |tptp.'S5'|)) % 56.22/56.45 (define @t413 () (@var "A__questionmark_v_0_111" |tptp.'S5'|)) % 56.22/56.45 (define @t414 () (* @t36 @t37)) % 56.22/56.45 (define @t415 () (tptp.f5 @t220 @t95)) % 56.22/56.45 (define @t416 () (@var "A__questionmark_v_0_112" |tptp.'S2'|)) % 56.22/56.45 (define @t417 () (tptp.f28 tptp.f48 @t37)) % 56.22/56.45 (define @t418 () (tptp.f24 tptp.f25 @t417)) % 56.22/56.45 (define @t419 () (@list @t37)) % 56.22/56.45 (define @t420 () (@list @t95)) % 56.22/56.45 (define @t421 () (@var "A__questionmark_v_0_113" Real)) % 56.22/56.45 (define @t422 () (tptp.f22 @t122 @t225)) % 56.22/56.45 (define @t423 () (@var "A__questionmark_v_0_114" Int)) % 56.22/56.45 (define @t424 () (@var "A__questionmark_v_0_115" Int)) % 56.22/56.45 (define @t425 () (@var "A__questionmark_v_1_118" Int)) % 56.22/56.45 (define @t426 () (@var "A__questionmark_v_2_117" Int)) % 56.22/56.45 (define @t427 () (tptp.f11 tptp.f12 (* @t426 @t425))) % 56.22/56.45 (define @t428 () (@var "A__questionmark_v_0_116" |tptp.'S2'|)) % 56.22/56.45 (define @t429 () (= @t1 @t428)) % 56.22/56.45 (define @t430 () (@var "A__questionmark_v_1_120" |tptp.'S28'|)) % 56.22/56.45 (define @t431 () (@var "A__questionmark_v_0_119" |tptp.'S30'|)) % 56.22/56.45 (define @t432 () (@var "A__questionmark_v_1_122" |tptp.'S28'|)) % 56.22/56.45 (define @t433 () (@var "A__questionmark_v_0_121" |tptp.'S30'|)) % 56.22/56.45 (define @t434 () (@var "A__questionmark_v_1_124" |tptp.'S28'|)) % 56.22/56.45 (define @t435 () (@var "A__questionmark_v_0_123" |tptp.'S30'|)) % 56.22/56.45 (define @t436 () (@var "A__questionmark_v_1_126" |tptp.'S17'|)) % 56.22/56.45 (define @t437 () (@var "A__questionmark_v_0_125" |tptp.'S2'|)) % 56.22/56.45 (define @t438 () (@var "A__questionmark_v_0_127" Real)) % 56.22/56.45 (define @t439 () (@var "A__questionmark_v1" |tptp.'S28'|)) % 56.22/56.45 (define @t440 () (@var "A__questionmark_v_1_129" Int)) % 56.22/56.45 (define @t441 () (@var "A__questionmark_v_0_128" Int)) % 56.22/56.45 (define @t442 () (@var "A__questionmark_v_2_130" |tptp.'S19'|)) % 56.22/56.45 (define @t443 () (@var "A__questionmark_v_1_132" Int)) % 56.22/56.45 (define @t444 () (@var "A__questionmark_v_0_131" Int)) % 56.22/56.45 (define @t445 () (@var "A__questionmark_v_2_133" |tptp.'S10'|)) % 56.22/56.45 (define @t446 () (@var "A__questionmark_v_1_135" Int)) % 56.22/56.45 (define @t447 () (@var "A__questionmark_v_0_134" Int)) % 56.22/56.45 (define @t448 () (@var "A__questionmark_v_2_136" |tptp.'S3'|)) % 56.22/56.45 (define @t449 () (@var "A__questionmark_v_1_138" Int)) % 56.22/56.45 (define @t450 () (@var "A__questionmark_v_0_137" Int)) % 56.22/56.45 (define @t451 () (@var "A__questionmark_v_2_139" |tptp.'S9'|)) % 56.22/56.45 (define @t452 () (@var "A__questionmark_v_0_140" |tptp.'S19'|)) % 56.22/56.45 (define @t453 () (@var "A__questionmark_v_0_141" |tptp.'S10'|)) % 56.22/56.45 (define @t454 () (@list @t37 @t31 @t64)) % 56.22/56.45 (define @t455 () (@var "A__questionmark_v_0_142" |tptp.'S3'|)) % 56.22/56.45 (define @t456 () (@list @t95 @t31 @t64)) % 56.22/56.45 (define @t457 () (@var "A__questionmark_v_0_143" |tptp.'S9'|)) % 56.22/56.45 (define @t458 () (@list @t41 @t31 @t64)) % 56.22/56.45 (define @t459 () (tptp.f22 @t138 @t64)) % 56.22/56.45 (define @t460 () (tptp.f22 @t122 @t64)) % 56.22/56.45 (define @t461 () (tptp.f3 @t136 @t64)) % 56.22/56.45 (define @t462 () (tptp.f3 @t116 @t64)) % 56.22/56.45 (define @t463 () (@var "A__questionmark_v_0_144" |tptp.'S19'|)) % 56.22/56.45 (define @t464 () (@var "A__questionmark_v_0_145" |tptp.'S10'|)) % 56.22/56.45 (define @t465 () (@var "A__questionmark_v_0_146" |tptp.'S3'|)) % 56.22/56.45 (define @t466 () (@var "A__questionmark_v_0_147" |tptp.'S9'|)) % 56.22/56.45 (define @t467 () (@var "A__questionmark_v_0_148" |tptp.'S19'|)) % 56.22/56.45 (define @t468 () (@var "A__questionmark_v_0_149" |tptp.'S10'|)) % 56.22/56.45 (define @t469 () (@var "A__questionmark_v_0_150" |tptp.'S3'|)) % 56.22/56.45 (define @t470 () (@var "A__questionmark_v_0_151" |tptp.'S9'|)) % 56.22/56.45 (define @t471 () (tptp.f44 @t227 @t1)) % 56.22/56.45 (define @t472 () (* @t37 @t37)) % 56.22/56.45 (define @t473 () (tptp.f5 @t96 @t95)) % 56.22/56.45 (define @t474 () (* @t41 @t41)) % 56.22/56.45 (define @t475 () (@list @t41)) % 56.22/56.45 (define @t476 () (tptp.f44 @t141 @t225)) % 56.22/56.45 (define @t477 () (tptp.f3 @t116 @t225)) % 56.22/56.45 (define @t478 () (tptp.f13 @t128 @t225)) % 56.22/56.45 (define @t479 () (@var "A__questionmark_v_0_152" |tptp.'S19'|)) % 56.22/56.45 (define @t480 () (@var "A__questionmark_v_0_153" |tptp.'S10'|)) % 56.22/56.45 (define @t481 () (@var "A__questionmark_v_0_154" |tptp.'S3'|)) % 56.22/56.45 (define @t482 () (@var "A__questionmark_v_0_155" |tptp.'S9'|)) % 56.22/56.45 (define @t483 () (tptp.f11 tptp.f12 (* @t44 @t88))) % 56.22/56.45 (define @t484 () (@var "A__questionmark_v_0_156" |tptp.'S19'|)) % 56.22/56.45 (define @t485 () (@var "A__questionmark_v_0_157" |tptp.'S10'|)) % 56.22/56.45 (define @t486 () (@var "A__questionmark_v_0_158" |tptp.'S3'|)) % 56.22/56.45 (define @t487 () (@var "A__questionmark_v_0_159" |tptp.'S19'|)) % 56.22/56.45 (define @t488 () (@var "A__questionmark_v_0_160" |tptp.'S10'|)) % 56.22/56.45 (define @t489 () (@var "A__questionmark_v_0_161" |tptp.'S3'|)) % 56.22/56.45 (define @t490 () (tptp.f75 @t92 @t439)) % 56.22/56.45 (define @t491 () (@list @t32 @t439 @t173)) % 56.22/56.45 (define @t492 () (tptp.f67 @t86 @t439)) % 56.22/56.45 (define @t493 () (@list @t47 @t439 @t170)) % 56.22/56.45 (define @t494 () (@var "A__questionmark_v_0_162" |tptp.'S19'|)) % 56.22/56.45 (define @t495 () (@var "A__questionmark_v_0_163" |tptp.'S10'|)) % 56.22/56.45 (define @t496 () (@var "A__questionmark_v_0_164" |tptp.'S3'|)) % 56.22/56.45 (define @t497 () (@var "A__questionmark_v_1_166" |tptp.'S19'|)) % 56.22/56.45 (define @t498 () (@var "A__questionmark_v_0_165" Int)) % 56.22/56.45 (define @t499 () (@var "A__questionmark_v_1_168" |tptp.'S10'|)) % 56.22/56.45 (define @t500 () (@var "A__questionmark_v_0_167" Int)) % 56.22/56.45 (define @t501 () (@var "A__questionmark_v_1_170" |tptp.'S3'|)) % 56.22/56.45 (define @t502 () (@var "A__questionmark_v_0_169" Int)) % 56.22/56.45 (define @t503 () (@var "A__questionmark_v_1_172" |tptp.'S9'|)) % 56.22/56.45 (define @t504 () (@var "A__questionmark_v_0_171" Int)) % 56.22/56.45 (define @t505 () (@var "A__questionmark_v_0_173" |tptp.'S2'|)) % 56.22/56.45 (define @t506 () (tptp.f44 @t141 @t31)) % 56.22/56.45 (define @t507 () (@var "A__questionmark_v_0_174" Real)) % 56.22/56.45 (define @t508 () (tptp.f22 @t122 @t31)) % 56.22/56.45 (define @t509 () (@var "A__questionmark_v_0_175" |tptp.'S4'|)) % 56.22/56.45 (define @t510 () (tptp.f3 @t116 @t31)) % 56.22/56.45 (define @t511 () (@var "A__questionmark_v_0_176" Int)) % 56.22/56.45 (define @t512 () (tptp.f13 @t128 @t31)) % 56.22/56.45 (define @t513 () (@var "A__questionmark_v_0_177" |tptp.'S19'|)) % 56.22/56.45 (define @t514 () (@var "A__questionmark_v_0_178" |tptp.'S10'|)) % 56.22/56.45 (define @t515 () (@var "A__questionmark_v_0_179" |tptp.'S3'|)) % 56.22/56.45 (define @t516 () (@var "A__questionmark_v_0_180" |tptp.'S9'|)) % 56.22/56.45 (define @t517 () (@var "A__questionmark_v_0_181" |tptp.'S19'|)) % 56.22/56.45 (define @t518 () (@var "A__questionmark_v_0_182" |tptp.'S10'|)) % 56.22/56.45 (define @t519 () (@var "A__questionmark_v_0_183" |tptp.'S3'|)) % 56.22/56.45 (define @t520 () (@var "A__questionmark_v_0_184" |tptp.'S9'|)) % 56.22/56.45 (define @t521 () (@var "A__questionmark_v_0_185" |tptp.'S19'|)) % 56.22/56.45 (define @t522 () (@var "A__questionmark_v_0_186" |tptp.'S10'|)) % 56.22/56.45 (define @t523 () (@var "A__questionmark_v_0_187" |tptp.'S3'|)) % 56.22/56.45 (define @t524 () (@var "A__questionmark_v_0_188" |tptp.'S9'|)) % 56.22/56.45 (define @t525 () (tptp.f6 tptp.f55 @t310)) % 56.22/56.45 (define @t526 () (@var "A__questionmark_v_1_190" |tptp.'S30'|)) % 56.22/56.45 (define @t527 () (@var "A__questionmark_v4" |tptp.'S10'|)) % 56.22/56.45 (define @t528 () (@var "A__questionmark_v5" |tptp.'S10'|)) % 56.22/56.45 (define @t529 () (@var "A__questionmark_v6" |tptp.'S2'|)) % 56.22/56.45 (define @t530 () (tptp.f22 @t527 @t529)) % 56.22/56.45 (define @t531 () (@var "A__questionmark_v_3_192" Int)) % 56.22/56.45 (define @t532 () (@var "A__questionmark_v_0_189" Int)) % 56.22/56.45 (define @t533 () (tptp.f13 tptp.f14 @t529)) % 56.22/56.45 (define @t534 () (@list @t529)) % 56.22/56.45 (define @t535 () (@var "A__questionmark_v_2_191" Int)) % 56.22/56.45 (define @t536 () (@var "A__questionmark_v_1_194" |tptp.'S30'|)) % 56.22/56.45 (define @t537 () (@var "A__questionmark_v4" |tptp.'S3'|)) % 56.22/56.45 (define @t538 () (@var "A__questionmark_v5" |tptp.'S3'|)) % 56.22/56.45 (define @t539 () (tptp.f3 @t537 @t529)) % 56.22/56.45 (define @t540 () (@var "A__questionmark_v_3_196" Int)) % 56.22/56.45 (define @t541 () (@var "A__questionmark_v_0_193" Int)) % 56.22/56.45 (define @t542 () (@var "A__questionmark_v_2_195" Int)) % 56.22/56.45 (define @t543 () (@var "A__questionmark_v_1_198" |tptp.'S30'|)) % 56.22/56.45 (define @t544 () (@var "A__questionmark_v4" |tptp.'S9'|)) % 56.22/56.45 (define @t545 () (@var "A__questionmark_v5" |tptp.'S9'|)) % 56.22/56.45 (define @t546 () (tptp.f13 @t544 @t529)) % 56.22/56.45 (define @t547 () (@var "A__questionmark_v_3_200" Int)) % 56.22/56.45 (define @t548 () (@var "A__questionmark_v_0_197" Int)) % 56.22/56.45 (define @t549 () (@var "A__questionmark_v_2_199" Int)) % 56.22/56.45 (define @t550 () (@var "A__questionmark_v_0_201" |tptp.'S2'|)) % 56.22/56.45 (define @t551 () (< 0 @t2)) % 56.22/56.45 (define @t552 () (tptp.f13 tptp.f14 @t506)) % 56.22/56.45 (define @t553 () (@var "A__questionmark_v_0_202" |tptp.'S2'|)) % 56.22/56.45 (define @t554 () (@var "A__questionmark_v_0_203" |tptp.'S2'|)) % 56.22/56.45 (define @t555 () (@var "A__questionmark_v_1_204" Real)) % 56.22/56.45 (define @t556 () (@var "A__questionmark_v_0_205" |tptp.'S2'|)) % 56.22/56.45 (define @t557 () (@var "A__questionmark_v_0_206" |tptp.'S19'|)) % 56.22/56.45 (define @t558 () (@var "A__questionmark_v_0_207" Int)) % 56.22/56.45 (define @t559 () (@var "A__questionmark_v_0_208" Real)) % 56.22/56.45 (define @t560 () (< @t37 0/1)) % 56.22/56.45 (define @t561 () (tptp.f28 tptp.f48 @t36)) % 56.22/56.45 (define @t562 () (tptp.f31 tptp.f142 @t41)) % 56.22/56.45 (define @t563 () (@var "A__questionmark_v_0_209" Real)) % 56.22/56.45 (define @t564 () (@var "A__questionmark_v_0_210" Int)) % 56.22/56.45 (define @t565 () (@var "A__questionmark_v_0_211" Int)) % 56.22/56.45 (define @t566 () (@var "A__questionmark_v_0_212" |tptp.'S28'|)) % 56.22/56.45 (define @t567 () (tptp.f70 @t186 @t64)) % 56.22/56.45 (define @t568 () (@var "A__questionmark_v_0_213" |tptp.'S28'|)) % 56.22/56.45 (define @t569 () (@var "A__questionmark_v_0_214" |tptp.'S28'|)) % 56.22/56.45 (define @t570 () (@var "A__questionmark_v0" |tptp.'S28'|)) % 56.22/56.45 (define @t571 () (tptp.f75 @t337 @t570)) % 56.22/56.45 (define @t572 () (tptp.f144 @t109 @t570)) % 56.22/56.45 (define @t573 () (= @t572 tptp.f1)) % 56.22/56.45 (define @t574 () (@list @t109)) % 56.22/56.45 (define @t575 () (tptp.f67 @t370 @t570)) % 56.22/56.45 (define @t576 () (= (tptp.f67 @t261 @t570) @t575)) % 56.22/56.45 (define @t577 () (= @t130 (tptp.f3 @t369 @t109))) % 56.22/56.45 (define @t578 () (=> @t573 @t577)) % 56.22/56.45 (define @t579 () (forall @t574 @t578)) % 56.22/56.45 (define @t580 () (=> @t579 @t576)) % 56.22/56.45 (define @t581 () (@list @t570 @t65 @t369)) % 56.22/56.45 (define @t582 () (forall @t581 @t580)) % 56.22/56.45 (define @t583 () (@var "A__questionmark_v4" |tptp.'S2'|)) % 56.22/56.45 (define @t584 () (= (tptp.f144 @t583 @t439) tptp.f1)) % 56.22/56.45 (define @t585 () (@list @t583)) % 56.22/56.45 (define @t586 () (= @t570 @t439)) % 56.22/56.45 (define @t587 () (= @t415 @t170)) % 56.22/56.45 (define @t588 () (tptp.f6 tptp.f59 @t170)) % 56.22/56.45 (define @t589 () (tptp.f5 @t588 @t95)) % 56.22/56.45 (define @t590 () (= @t77 @t589)) % 56.22/56.45 (define @t591 () (= @t95 tptp.f132)) % 56.22/56.45 (define @t592 () (not @t591)) % 56.22/56.45 (define @t593 () (= @t414 @t173)) % 56.22/56.45 (define @t594 () (/ @t173 @t37)) % 56.22/56.45 (define @t595 () (= @t36 @t594)) % 56.22/56.45 (define @t596 () (not (= @t37 0/1))) % 56.22/56.45 (define @t597 () (tptp.f5 @t304 @t95)) % 56.22/56.45 (define @t598 () (= @t77 @t597)) % 56.22/56.45 (define @t599 () (tptp.f6 tptp.f59 @t77)) % 56.22/56.45 (define @t600 () (tptp.f5 @t599 @t95)) % 56.22/56.45 (define @t601 () (= @t600 @t170)) % 56.22/56.45 (define @t602 () (* @t173 @t37)) % 56.22/56.45 (define @t603 () (= @t36 @t602)) % 56.22/56.45 (define @t604 () (/ @t36 @t37)) % 56.22/56.45 (define @t605 () (= @t604 @t173)) % 56.22/56.45 (define @t606 () (@var "A__questionmark_v_2_217" |tptp.'S3'|)) % 56.22/56.45 (define @t607 () (@var "A__questionmark_v_1_216" Int)) % 56.22/56.45 (define @t608 () (@var "A__questionmark_v_0_215" Int)) % 56.22/56.45 (define @t609 () (@var "A__questionmark_v_2_220" |tptp.'S10'|)) % 56.22/56.45 (define @t610 () (@var "A__questionmark_v_1_219" Int)) % 56.22/56.45 (define @t611 () (@var "A__questionmark_v_0_218" Int)) % 56.22/56.45 (define @t612 () (/ @t36 @t173)) % 56.22/56.45 (define @t613 () (/ @t37 @t173)) % 56.22/56.45 (define @t614 () (- @t37 @t36)) % 56.22/56.45 (define @t615 () (tptp.f5 @t599 @t170)) % 56.22/56.45 (define @t616 () (tptp.f6 tptp.f59 @t95)) % 56.22/56.45 (define @t617 () (tptp.f5 @t616 @t170)) % 56.22/56.45 (define @t618 () (tptp.f6 tptp.f51 @t95)) % 56.22/56.45 (define @t619 () (tptp.f5 @t618 @t77)) % 56.22/56.45 (define @t620 () (@var "A__questionmark_v_0_221" Real)) % 56.22/56.45 (define @t621 () (@var "A__questionmark_v_0_222" Real)) % 56.22/56.45 (define @t622 () (@var "A__questionmark_v_0_223" Real)) % 56.22/56.45 (define @t623 () (@var "A__questionmark_v_0_224" |tptp.'S5'|)) % 56.22/56.45 (define @t624 () (tptp.f6 tptp.f7 @t619)) % 56.22/56.45 (define @t625 () (@var "A__questionmark_v_0_225" |tptp.'S5'|)) % 56.22/56.45 (define @t626 () (tptp.f6 tptp.f51 @t77)) % 56.22/56.45 (define @t627 () (tptp.f5 @t626 @t170)) % 56.22/56.45 (define @t628 () (@var "A__questionmark_v_0_226" |tptp.'S5'|)) % 56.22/56.45 (define @t629 () (/ @t37 @t36)) % 56.22/56.45 (define @t630 () (tptp.f5 @t616 @t77)) % 56.22/56.45 (define @t631 () (@var "A__questionmark_v_0_227" Real)) % 56.22/56.45 (define @t632 () (@var "A__questionmark_v_0_228" Real)) % 56.22/56.45 (define @t633 () (@var "A__questionmark_v_0_229" Real)) % 56.22/56.45 (define @t634 () (@var "A__questionmark_v_0_230" Real)) % 56.22/56.45 (define @t635 () (@var "A__questionmark_v_0_231" Real)) % 56.22/56.45 (define @t636 () (@var "A__questionmark_v_0_232" Real)) % 56.22/56.45 (define @t637 () (= @t77 tptp.f132)) % 56.22/56.45 (define @t638 () (or @t591 @t637)) % 56.22/56.45 (define @t639 () (= @t311 tptp.f132)) % 56.22/56.45 (define @t640 () (@var "A__questionmark_v_0_233" Real)) % 56.22/56.45 (define @t641 () (= @t40 0)) % 56.22/56.45 (define @t642 () (= @t41 0)) % 56.22/56.45 (define @t643 () (or @t642 @t641)) % 56.22/56.45 (define @t644 () (= @t42 0)) % 56.22/56.45 (define @t645 () (not @t637)) % 56.22/56.45 (define @t646 () (@var "A__questionmark_v_0_234" Real)) % 56.22/56.45 (define @t647 () (not @t642)) % 56.22/56.45 (define @t648 () (@var "A__questionmark_v_0_235" Real)) % 56.22/56.45 (define @t649 () (@var "A__questionmark_v_0_236" Real)) % 56.22/56.45 (define @t650 () (@var "A__questionmark_v_0_237" Real)) % 56.22/56.45 (define @t651 () (@var "A__questionmark_v_0_238" Real)) % 56.22/56.45 (define @t652 () (tptp.f8 tptp.f9 tptp.f132)) % 56.22/56.45 (define @t653 () (@var "A__questionmark_v_0_239" Real)) % 56.22/56.45 (define @t654 () (tptp.f98 tptp.f99 0)) % 56.22/56.45 (define @t655 () (tptp.f45 tptp.f108 tptp.f145)) % 56.22/56.45 (define @t656 () (= @t510 tptp.f132)) % 56.22/56.45 (define @t657 () (@var "A__questionmark_v_0_240" Real)) % 56.22/56.45 (define @t658 () (= @t512 0)) % 56.22/56.45 (define @t659 () (@var "A__questionmark_v_0_241" Real)) % 56.22/56.45 (define @t660 () (@var "A__questionmark_v_0_242" Real)) % 56.22/56.45 (define @t661 () (@list @t570)) % 56.22/56.45 (define @t662 () (@var "A__questionmark_v_1_244" Real)) % 56.22/56.45 (define @t663 () (@var "A__questionmark_v_0_243" Real)) % 56.22/56.45 (define @t664 () (- @t38 @t301)) % 56.22/56.45 (define @t665 () (- @t36 @t282)) % 56.22/56.45 (define @t666 () (- @t37 @t173)) % 56.22/56.45 (define @t667 () (@var "A__questionmark_v_2_247" |tptp.'S4'|)) % 56.22/56.45 (define @t668 () (@var "A__questionmark_v_1_245" |tptp.'S5'|)) % 56.22/56.45 (define @t669 () (@var "A__questionmark_v_0_246" |tptp.'S5'|)) % 56.22/56.45 (define @t670 () (tptp.f6 tptp.f51 @t311)) % 56.22/56.45 (define @t671 () (tptp.f5 @t626 @t285)) % 56.22/56.45 (define @t672 () (tptp.f5 @t618 @t170)) % 56.22/56.45 (define @t673 () (tptp.f6 tptp.f7 @t672)) % 56.22/56.45 (define @t674 () (@var "A__questionmark_v_0_248" |tptp.'S5'|)) % 56.22/56.45 (define @t675 () (- @t41 @t176)) % 56.22/56.45 (define @t676 () (- @t40 @t290)) % 56.22/56.45 (define @t677 () (@var "A__questionmark_v4" Real)) % 56.22/56.45 (define @t678 () (= (+ @t38 @t173) (+ (* @t282 @t36) @t677))) % 56.22/56.45 (define @t679 () (@list @t37 @t36 @t173 @t282 @t677)) % 56.22/56.45 (define @t680 () (@var "A__questionmark_v4" |tptp.'S4'|)) % 56.22/56.45 (define @t681 () (tptp.f6 tptp.f7 @t285)) % 56.22/56.45 (define @t682 () (= (tptp.f5 @t312 @t170) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t681 @t77)) @t680))) % 56.22/56.45 (define @t683 () (@list @t95 @t77 @t170 @t285 @t680)) % 56.22/56.45 (define @t684 () (@var "A__questionmark_v4" Int)) % 56.22/56.45 (define @t685 () (= (+ @t42 @t176) (+ (* @t290 @t40) @t684))) % 56.22/56.45 (define @t686 () (@list @t41 @t40 @t176 @t290 @t684)) % 56.22/56.45 (define @t687 () (@var "A__questionmark_v_1_250" |tptp.'S59'|)) % 56.22/56.45 (define @t688 () (@var "A__questionmark_v_2_251" |tptp.'S30'|)) % 56.22/56.45 (define @t689 () (@var "A__questionmark_v_0_249" Int)) % 56.22/56.45 (define @t690 () (@var "A__questionmark_v_1_253" |tptp.'S33'|)) % 56.22/56.45 (define @t691 () (@var "A__questionmark_v_2_254" |tptp.'S30'|)) % 56.22/56.45 (define @t692 () (@var "A__questionmark_v_0_252" Int)) % 56.22/56.45 (define @t693 () (@var "A__questionmark_v_1_256" |tptp.'S27'|)) % 56.22/56.45 (define @t694 () (@var "A__questionmark_v_2_257" |tptp.'S30'|)) % 56.22/56.45 (define @t695 () (@var "A__questionmark_v_0_255" Int)) % 56.22/56.45 (define @t696 () (@var "A__questionmark_v_0_258" Real)) % 56.22/56.45 (define @t697 () (and @t642 @t641)) % 56.22/56.45 (define @t698 () (@var "A__questionmark_v_0_259" |tptp.'S5'|)) % 56.22/56.45 (define @t699 () (@var "A__questionmark_v_1_260" Real)) % 56.22/56.45 (define @t700 () (@var "A__questionmark_v_0_261" |tptp.'S2'|)) % 56.22/56.45 (define @t701 () (@var "A__questionmark_v_0_262" |tptp.'S2'|)) % 56.22/56.45 (define @t702 () (@var "A__questionmark_v_1_263" |tptp.'S2'|)) % 56.22/56.45 (define @t703 () (@var "A__questionmark_v_0_264" |tptp.'S27'|)) % 56.22/56.45 (define @t704 () (@var "A__questionmark_v_1_265" |tptp.'S2'|)) % 56.22/56.45 (define @t705 () (@var "A__questionmark_v_0_266" |tptp.'S33'|)) % 56.22/56.45 (define @t706 () (@var "A__questionmark_v_1_267" |tptp.'S2'|)) % 56.22/56.45 (define @t707 () (@var "A__questionmark_v_0_268" |tptp.'S59'|)) % 56.22/56.45 (define @t708 () (@var "A__questionmark_v_0_269" |tptp.'S30'|)) % 56.22/56.45 (define @t709 () (@var "A__questionmark_v_1_270" |tptp.'S59'|)) % 56.22/56.45 (define @t710 () (@var "A__questionmark_v_0_271" |tptp.'S30'|)) % 56.22/56.45 (define @t711 () (@var "A__questionmark_v_1_272" |tptp.'S33'|)) % 56.22/56.45 (define @t712 () (@var "A__questionmark_v_0_273" |tptp.'S30'|)) % 56.22/56.45 (define @t713 () (@var "A__questionmark_v_1_274" |tptp.'S27'|)) % 56.22/56.45 (define @t714 () (@var "A__questionmark_v_0_275" |tptp.'S2'|)) % 56.22/56.45 (define @t715 () (tptp.f11 tptp.f12 (+ @t296 1))) % 56.22/56.45 (define @t716 () (@var "A__questionmark_v_0_276" |tptp.'S2'|)) % 56.22/56.45 (define @t717 () (@var "A__questionmark_v_0_277" |tptp.'S2'|)) % 56.22/56.45 (define @t718 () (@var "A__questionmark_v_2_279" |tptp.'S30'|)) % 56.22/56.45 (define @t719 () (@var "A__questionmark_v_1_278" |tptp.'S33'|)) % 56.22/56.45 (define @t720 () (@var "A__questionmark_v_0_280" Int)) % 56.22/56.45 (define @t721 () (tptp.f75 @t719 (tptp.f70 @t718 (tptp.f11 tptp.f12 (+ @t720 1))))) % 56.22/56.45 (define @t722 () (< @t720 @t44)) % 56.22/56.45 (define @t723 () (@var "A__questionmark_v_2_282" |tptp.'S30'|)) % 56.22/56.45 (define @t724 () (@var "A__questionmark_v_1_281" |tptp.'S27'|)) % 56.22/56.45 (define @t725 () (@var "A__questionmark_v_0_283" Int)) % 56.22/56.45 (define @t726 () (tptp.f67 @t724 (tptp.f70 @t723 (tptp.f11 tptp.f12 (+ @t725 1))))) % 56.22/56.45 (define @t727 () (< @t725 @t44)) % 56.22/56.45 (define @t728 () (@var "A__questionmark_v_2_285" |tptp.'S30'|)) % 56.22/56.45 (define @t729 () (@var "A__questionmark_v_1_284" |tptp.'S59'|)) % 56.22/56.45 (define @t730 () (@var "A__questionmark_v_0_286" Int)) % 56.22/56.45 (define @t731 () (tptp.f139 @t729 (tptp.f70 @t728 (tptp.f11 tptp.f12 (+ @t730 1))))) % 56.22/56.45 (define @t732 () (< @t730 @t44)) % 56.22/56.45 (define @t733 () (@var "A__questionmark_v_0_287" |tptp.'S2'|)) % 56.22/56.45 (define @t734 () (@var "A__questionmark_v_0_288" |tptp.'S2'|)) % 56.22/56.45 (define @t735 () (@var "A__questionmark_v_0_289" |tptp.'S2'|)) % 56.22/56.45 (define @t736 () (@var "A__questionmark_v_0_290" |tptp.'S5'|)) % 56.22/56.45 (define @t737 () (tptp.f5 @t681 @t95)) % 56.22/56.45 (define @t738 () (tptp.f5 (tptp.f6 tptp.f59 @t285) @t77)) % 56.22/56.45 (define @t739 () (* @t282 @t37)) % 56.22/56.45 (define @t740 () (/ @t282 @t36)) % 56.22/56.45 (define @t741 () (@var "A__questionmark_v_0_291" Real)) % 56.22/56.45 (define @t742 () (@var "A__questionmark_v_0_292" Real)) % 56.22/56.45 (define @t743 () (= @t170 tptp.f132)) % 56.22/56.45 (define @t744 () (not @t743)) % 56.22/56.45 (define @t745 () (@var "A__questionmark_v_0_293" Real)) % 56.22/56.45 (define @t746 () (not (= @t173 @t745))) % 56.22/56.45 (define @t747 () (@var "A__questionmark_v_0_294" Real)) % 56.22/56.45 (define @t748 () (not (= @t36 @t747))) % 56.22/56.45 (define @t749 () (@var "A__questionmark_v_0_295" |tptp.'S5'|)) % 56.22/56.45 (define @t750 () (@var "A__questionmark_v_0_296" Int)) % 56.22/56.45 (define @t751 () (@var "A__questionmark_v_0_297" Int)) % 56.22/56.45 (define @t752 () (@var "A__questionmark_v_0_298" Int)) % 56.22/56.45 (define @t753 () (@var "A__questionmark_v_1_300" Int)) % 56.22/56.45 (define @t754 () (@var "A__questionmark_v_0_299" Int)) % 56.22/56.45 (define @t755 () (@var "A__questionmark_v_0_301" |tptp.'S2'|)) % 56.22/56.45 (define @t756 () (@var "A__questionmark_v_1_302" Int)) % 56.22/56.45 (define @t757 () (@var "A__questionmark_v_0_303" Int)) % 56.22/56.45 (define @t758 () (@var "A__questionmark_v_1_305" Int)) % 56.22/56.45 (define @t759 () (@var "A__questionmark_v_0_304" Int)) % 56.22/56.45 (define @t760 () (@var "A__questionmark_v_2_308" Int)) % 56.22/56.45 (define @t761 () (@var "A__questionmark_v_0_306" Int)) % 56.22/56.45 (define @t762 () (@var "A__questionmark_v_1_307" Int)) % 56.22/56.45 (define @t763 () (@var "A__questionmark_v_2_310" Int)) % 56.22/56.45 (define @t764 () (@var "A__questionmark_v_0_309" Int)) % 56.22/56.45 (define @t765 () (@var "A__questionmark_v_1_311" Int)) % 56.22/56.45 (define @t766 () (@var "A__questionmark_v_2_314" Int)) % 56.22/56.45 (define @t767 () (@var "A__questionmark_v_0_312" Int)) % 56.22/56.45 (define @t768 () (@var "A__questionmark_v_1_313" Int)) % 56.22/56.45 (define @t769 () (@var "A__questionmark_v_0_316" Int)) % 56.22/56.45 (define @t770 () (@var "A__questionmark_v_1_315" Int)) % 56.22/56.45 (define @t771 () (@var "A__questionmark_v_0_317" |tptp.'S2'|)) % 56.22/56.45 (define @t772 () (@var "A__questionmark_v_0_318" |tptp.'S2'|)) % 56.22/56.45 (define @t773 () (@var "A__questionmark_v_2_321" Int)) % 56.22/56.45 (define @t774 () (@var "A__questionmark_v_1_320" Int)) % 56.22/56.45 (define @t775 () (@var "A__questionmark_v_0_319" Int)) % 56.22/56.45 (define @t776 () (@var "A__questionmark_v_1_324" Int)) % 56.22/56.45 (define @t777 () (@var "A__questionmark_v_2_323" Int)) % 56.22/56.45 (define @t778 () (@var "A__questionmark_v_0_322" Int)) % 56.22/56.45 (define @t779 () (@var "A__questionmark_v_1_327" Int)) % 56.22/56.45 (define @t780 () (@var "A__questionmark_v_2_325" Int)) % 56.22/56.45 (define @t781 () (@var "A__questionmark_v_0_326" Int)) % 56.22/56.45 (define @t782 () (@var "A__questionmark_v_0_328" |tptp.'S2'|)) % 56.22/56.45 (define @t783 () (@var "A__questionmark_v_2_330" Int)) % 56.22/56.45 (define @t784 () (@var "A__questionmark_v_1_331" Int)) % 56.22/56.45 (define @t785 () (@var "A__questionmark_v_0_329" Int)) % 56.22/56.45 (define @t786 () (@var "A__questionmark_v_2_332" Int)) % 56.22/56.45 (define @t787 () (@var "A__questionmark_v_1_334" Int)) % 56.22/56.45 (define @t788 () (@var "A__questionmark_v_0_333" Int)) % 56.22/56.45 (define @t789 () (@var "A__questionmark_v_2_336" Int)) % 56.22/56.45 (define @t790 () (@var "A__questionmark_v_1_337" Int)) % 56.22/56.45 (define @t791 () (@var "A__questionmark_v_0_335" Int)) % 56.22/56.45 (define @t792 () (@var "A__questionmark_v_2_338" Int)) % 56.22/56.45 (define @t793 () (@var "A__questionmark_v_1_340" Int)) % 56.22/56.45 (define @t794 () (@var "A__questionmark_v_0_339" Int)) % 56.22/56.45 (define @t795 () (= @t1 @t185)) % 56.22/56.45 (define @t796 () (= @t31 @t64)) % 56.22/56.45 (define @t797 () (@var "A__questionmark_v_0_341" Int)) % 56.22/56.45 (define @t798 () (@var "A__questionmark_v_0_342" Int)) % 56.22/56.45 (define @t799 () (@var "A__questionmark_v_0_343" Int)) % 56.22/56.45 (define @t800 () (@var "A__questionmark_v_2_345" Int)) % 56.22/56.45 (define @t801 () (@var "A__questionmark_v_1_346" Int)) % 56.22/56.45 (define @t802 () (@var "A__questionmark_v_0_344" Int)) % 56.22/56.45 (define @t803 () (@var "A__questionmark_v_2_348" Int)) % 56.22/56.45 (define @t804 () (@var "A__questionmark_v_1_349" Int)) % 56.22/56.45 (define @t805 () (@var "A__questionmark_v_0_347" Int)) % 56.22/56.45 (define @t806 () (@var "A__questionmark_v_2_352" Int)) % 56.22/56.45 (define @t807 () (@var "A__questionmark_v_1_350" Int)) % 56.22/56.45 (define @t808 () (@var "A__questionmark_v_0_351" Int)) % 56.22/56.45 (define @t809 () (@var "A__questionmark_v_2_353" Int)) % 56.22/56.45 (define @t810 () (@var "A__questionmark_v_1_355" Int)) % 56.22/56.45 (define @t811 () (@var "A__questionmark_v_0_354" Int)) % 56.22/56.45 (define @t812 () (@var "A__questionmark_v_1_358" Int)) % 56.22/56.45 (define @t813 () (@var "A__questionmark_v_2_356" Int)) % 56.22/56.45 (define @t814 () (@var "A__questionmark_v_0_357" Int)) % 56.22/56.45 (define @t815 () (@var "A__questionmark_v_2_359" Int)) % 56.22/56.45 (define @t816 () (@var "A__questionmark_v_0_361" Int)) % 56.22/56.45 (define @t817 () (@var "A__questionmark_v_1_360" Int)) % 56.22/56.45 (define @t818 () (@var "A__questionmark_v_3_364" Int)) % 56.22/56.45 (define @t819 () (@var "A__questionmark_v_2_362" Int)) % 56.22/56.45 (define @t820 () (@var "A__questionmark_v_1_365" Int)) % 56.22/56.45 (define @t821 () (@var "A__questionmark_v_0_363" Int)) % 56.22/56.45 (define @t822 () (@var "A__questionmark_v_1_367" Int)) % 56.22/56.45 (define @t823 () (@var "A__questionmark_v_2_368" Int)) % 56.22/56.45 (define @t824 () (@var "A__questionmark_v_0_366" Int)) % 56.22/56.45 (define @t825 () (@var "A__questionmark_v_2_371" Int)) % 56.22/56.45 (define @t826 () (@var "A__questionmark_v_1_370" Int)) % 56.22/56.45 (define @t827 () (@var "A__questionmark_v_0_369" Int)) % 56.22/56.45 (define @t828 () (@var "A__questionmark_v_2_373" Int)) % 56.22/56.45 (define @t829 () (@var "A__questionmark_v_1_374" Int)) % 56.22/56.45 (define @t830 () (@var "A__questionmark_v_0_372" Int)) % 56.22/56.45 (define @t831 () (tptp.f13 tptp.f14 (tptp.f11 tptp.f12 @t41))) % 56.22/56.45 (define @t832 () (forall @t574 (or (not (= tptp.f1 (tptp.f144 @t109 @t187))) (= (tptp.f3 tptp.f21 @t109) (tptp.f3 tptp.f4 @t109))))) % 56.22/56.45 (define @t833 () (@quantifiers_skolemize @t832 0)) % 56.22/56.45 (define @t834 () (@list @t833)) % 56.22/56.45 (define @t835 () (= (tptp.f5 @t394 @t170) (tptp.f5 @t96 @t316))) % 56.22/56.45 (define @t836 () (not @t835)) % 56.22/56.45 (define @t837 () (not (= @t96 @t96))) % 56.22/56.45 (define @t838 () (or @t837 @t836)) % 56.22/56.45 (define @t839 () (not @t405)) % 56.22/56.45 (define @t840 () (= @t96 @t404)) % 56.22/56.45 (define @t841 () (not @t840)) % 56.22/56.45 (define @t842 () (or @t841 @t841 @t839)) % 56.22/56.45 (define @t843 () (or @t841 @t839)) % 56.22/56.45 (define @t844 () (and @t840 @t405)) % 56.22/56.45 (define @t845 () (forall @t408 (not @t844))) % 56.22/56.45 (define @t846 () (not @t845)) % 56.22/56.45 (define @t847 () (= tptp.f1 @t572)) % 56.22/56.45 (define @t848 () (forall @t574 (or (not @t847) @t577))) % 56.22/56.45 (define @t849 () (tptp.f67 @t181 @t187)) % 56.22/56.45 (define @t850 () (tptp.f67 @t182 @t187)) % 56.22/56.45 (define @t851 () (not @t832)) % 56.22/56.45 (define @t852 () (or @t851 (= @t849 @t850))) % 56.22/56.45 (define @t853 () (forall @t581 (or (not @t848) @t576))) % 56.22/56.45 (define @t854 () (= @t850 @t849)) % 56.22/56.45 (define @t855 () (or @t851 @t854)) % 56.22/56.45 (define @t856 () (not (= @t187 @t187))) % 56.22/56.45 (define @t857 () (or @t856 @t854)) % 56.22/56.45 (define @t858 () (not @t188)) % 56.22/56.45 (define @t859 () (or @t858 @t858 @t183)) % 56.22/56.45 (define @t860 () (or @t858 @t183)) % 56.22/56.45 (define @t861 () (forall @t190 (not @t189))) % 56.22/56.45 (define @t862 () (not @t861)) % 56.22/56.45 (define @t863 () (= (tptp.f3 tptp.f21 @t833) (tptp.f3 tptp.f4 @t833))) % 56.22/56.45 (define @t864 () (or (not (= tptp.f1 (tptp.f144 @t833 @t187))) @t863)) % 56.22/56.45 (assume @p1 (not (= tptp.f1 tptp.f2))) % 56.22/56.45 (assume @p2 @t19) % 56.22/56.45 (assume @p3 (forall @t18 (exists (@list @t20) (and (= @t20 @t4) (= (tptp.f3 tptp.f18 @t1) (tptp.f5 (tptp.f6 tptp.f7 (tptp.f3 @t11 (tptp.f11 tptp.f12 (* @t21 @t20)))) (tptp.f3 tptp.f17 (tptp.f11 tptp.f12 @t20)))))))) % 56.22/56.45 (assume @p4 (forall @t18 (exists (@list @t22) (and (= @t22 @t3) (= (tptp.f3 tptp.f19 @t1) (tptp.f5 (tptp.f6 tptp.f7 (tptp.f3 @t11 (tptp.f11 tptp.f12 (* @t21 @t22)))) (tptp.f3 tptp.f17 (tptp.f11 tptp.f12 @t22)))))))) % 56.22/56.45 (assume @p5 (forall @t18 (= (tptp.f3 tptp.f20 @t1) (tptp.f5 (tptp.f6 tptp.f7 (tptp.f3 @t11 (tptp.f11 tptp.f12 (* @t21 @t2)))) (tptp.f3 tptp.f17 @t1))))) % 56.22/56.45 (assume @p6 @t28) % 56.22/56.45 (assume @p7 (forall @t18 (= (tptp.f22 tptp.f23 @t1) (tptp.f22 (tptp.f24 tptp.f25 (- 1/1)) @t30)))) % 56.22/56.45 (assume @p8 (forall @t35 (= (tptp.f22 @t34 @t31) (* @t33 (tptp.f22 (tptp.f24 tptp.f25 0/1) @t31))))) % 56.22/56.45 (assume @p9 (forall @t39 (= (tptp.f28 (tptp.f29 tptp.f30 @t37) @t36) @t38))) % 56.22/56.45 (assume @p10 (forall @t43 (= (tptp.f31 (tptp.f32 tptp.f33 @t41) @t40) @t42))) % 56.22/56.45 (assume @p11 (forall @t49 (= (tptp.f3 @t48 @t31) (tptp.f3 @t47 @t46)))) % 56.22/56.45 (assume @p12 (forall @t35 (= (tptp.f22 @t50 @t31) (tptp.f22 @t32 @t46)))) % 56.22/56.45 (assume @p13 (forall @t53 (= (tptp.f13 @t52 @t31) (tptp.f13 @t51 @t46)))) % 56.22/56.45 (assume @p14 (forall @t49 (= (tptp.f3 @t55 @t31) (tptp.f3 @t47 @t54)))) % 56.22/56.45 (assume @p15 (forall @t35 (= (tptp.f22 @t56 @t31) (tptp.f22 @t32 @t54)))) % 56.22/56.45 (assume @p16 (forall @t53 (= (tptp.f13 @t57 @t31) (tptp.f13 @t51 @t54)))) % 56.22/56.45 (assume @p17 (forall @t49 (= (tptp.f3 @t59 @t31) (tptp.f3 @t47 @t58)))) % 56.22/56.45 (assume @p18 (forall @t35 (= (tptp.f22 @t60 @t31) (tptp.f22 @t32 @t58)))) % 56.22/56.45 (assume @p19 (forall @t62 (= (tptp.f44 (tptp.f45 tptp.f46 @t1) @t31) @t61))) % 56.22/56.45 (assume @p20 (forall @t35 (= (tptp.f22 @t63 @t31) (tptp.f28 tptp.f48 @t33)))) % 56.22/56.45 (assume @p21 (forall @t69 (= (tptp.f3 @t68 @t64) (tptp.f5 (tptp.f6 tptp.f51 @t67) @t66)))) % 56.22/56.45 (assume @p22 (forall @t74 (= (tptp.f22 @t73 @t64) (- @t72 @t71)))) % 56.22/56.45 (assume @p23 (forall @t69 (= (tptp.f3 @t75 @t64) (tptp.f5 (tptp.f6 tptp.f55 @t67) @t66)))) % 56.22/56.45 (assume @p24 (forall @t74 (= (tptp.f22 @t76 @t64) (+ @t72 @t71)))) % 56.22/56.45 (assume @p25 (forall @t79 (= (tptp.f3 (tptp.f8 @t78 @t77) @t64) (tptp.f5 (tptp.f6 tptp.f59 @t67) @t77)))) % 56.22/56.45 (assume @p26 (forall @t81 (= (tptp.f22 (tptp.f24 @t80 @t36) @t64) (/ @t72 @t36)))) % 56.22/56.45 (assume @p27 (forall @t79 (= (tptp.f3 (tptp.f8 @t82 @t77) @t64) (tptp.f5 (tptp.f6 tptp.f7 @t67) @t77)))) % 56.22/56.45 (assume @p28 (forall @t81 (= (tptp.f22 (tptp.f24 @t83 @t36) @t64) (* @t72 @t36)))) % 56.22/56.45 (assume @p29 (forall @t89 (exists (@list @t84) (and (= @t84 @t44) (exists (@list @t85) (and (= @t85 (* @t88 @t84)) (= (tptp.f3 @t87 @t64) (tptp.f67 @t86 (tptp.f70 (tptp.f71 (tptp.f11 tptp.f12 @t85)) (tptp.f11 tptp.f12 (+ @t85 @t84))))))))))) % 56.22/56.45 (assume @p30 (forall @t94 (exists (@list @t90) (and (= @t90 @t44) (exists (@list @t91) (and (= @t91 (* @t88 @t90)) (= (tptp.f22 @t93 @t64) (tptp.f75 @t92 (tptp.f70 (tptp.f71 (tptp.f11 tptp.f12 @t91)) (tptp.f11 tptp.f12 (+ @t91 @t90))))))))))) % 56.22/56.45 (assume @p31 (forall (@list @t95 @t65 @t64) (= (tptp.f3 @t97 @t64) (tptp.f5 @t96 @t66)))) % 56.22/56.45 (assume @p32 (forall (@list @t37 @t70 @t64) (= (tptp.f22 @t98 @t64) (* @t37 @t71)))) % 56.22/56.45 (assume @p33 (forall @t89 (= (tptp.f3 @t101 @t64) (tptp.f3 @t47 @t99)))) % 56.22/56.45 (assume @p34 (forall @t94 (= (tptp.f22 @t103 @t64) (tptp.f22 @t32 @t99)))) % 56.22/56.45 (assume @p35 (forall @t106 (= (tptp.f13 @t105 @t64) (tptp.f13 @t51 @t99)))) % 56.22/56.45 (assume @p36 (forall (@list @t1 @t70 @t64) (= (tptp.f22 (tptp.f26 @t107 @t70) @t64) (tptp.f22 @t70 (tptp.f11 tptp.f12 (+ @t88 @t2)))))) % 56.22/56.45 (assume @p37 (forall @t117 (exists (@list @t108) (and (= @t108 @t116) (= (tptp.f3 @t115 @t109) (tptp.f5 (tptp.f6 tptp.f51 (tptp.f5 (tptp.f6 tptp.f7 (tptp.f3 @t114 @t111)) (tptp.f3 @t108 @t109))) (tptp.f3 @t108 @t64))))))) % 56.22/56.45 (assume @p38 (forall @t123 (exists (@list @t118) (and (= @t118 @t122) (= (tptp.f22 @t121 @t109) (- (* (tptp.f22 @t120 @t111) (tptp.f22 @t118 @t109)) (tptp.f22 @t118 @t64))))))) % 56.22/56.45 (assume @p39 (forall @t129 (exists (@list @t124) (and (= @t124 @t128) (= (tptp.f13 @t127 @t109) (- (* (tptp.f13 @t126 @t111) (tptp.f13 @t124 @t109)) (tptp.f13 @t124 @t64))))))) % 56.22/56.45 (assume @p40 (forall @t135 (= (tptp.f3 @t134 @t109) (tptp.f5 (tptp.f6 tptp.f7 @t133) @t130)))) % 56.22/56.45 (assume @p41 (forall @t117 (= (tptp.f3 @t137 @t109) (tptp.f5 (tptp.f6 tptp.f7 (tptp.f3 @t116 @t111)) (tptp.f3 @t136 @t109))))) % 56.22/56.45 (assume @p42 (forall @t123 (= (tptp.f22 @t139 @t109) (* (tptp.f22 @t122 @t111) (tptp.f22 @t138 @t109))))) % 56.22/56.45 (assume @p43 (forall @t143 (= (tptp.f44 @t142 @t109) (tptp.f44 (tptp.f45 tptp.f107 (tptp.f44 @t141 @t111)) (tptp.f44 @t140 @t109))))) % 56.22/56.45 (assume @p44 (forall @t129 (= (tptp.f13 @t145 @t109) (* (tptp.f13 @t128 @t111) (tptp.f13 @t144 @t109))))) % 56.22/56.45 (assume @p45 (forall @t117 (exists (@list @t147 @t146) (and (= @t147 @t116) (= @t146 @t111) (= (tptp.f3 @t148 @t109) (tptp.f5 (tptp.f6 tptp.f7 (tptp.f3 @t147 @t109)) (tptp.f5 (tptp.f6 tptp.f51 (tptp.f3 @t114 @t146)) (tptp.f3 @t147 @t146)))))))) % 56.22/56.45 (assume @p46 (forall @t123 (exists (@list @t150 @t149) (and (= @t150 @t122) (= @t149 @t111) (= (tptp.f22 @t151 @t109) (* (tptp.f22 @t150 @t109) (- (tptp.f22 @t120 @t149) (tptp.f22 @t150 @t149)))))))) % 56.22/56.45 (assume @p47 (forall @t129 (exists (@list @t153 @t152) (and (= @t153 @t128) (= @t152 @t111) (= (tptp.f13 @t154 @t109) (* (tptp.f13 @t153 @t109) (- (tptp.f13 @t126 @t152) (tptp.f13 @t153 @t152)))))))) % 56.22/56.45 (assume @p48 (forall @t117 (= (tptp.f3 @t158 @t109) (tptp.f5 @t157 (tptp.f3 @t136 @t156))))) % 56.22/56.45 (assume @p49 (forall @t123 (= (tptp.f22 @t160 @t109) (* @t159 (tptp.f22 @t138 @t156))))) % 56.22/56.45 (assume @p50 (forall @t143 (= (tptp.f44 @t162 @t109) (tptp.f44 @t161 (tptp.f44 @t140 @t156))))) % 56.22/56.45 (assume @p51 (forall @t129 (= (tptp.f13 @t164 @t109) (* @t163 (tptp.f13 @t144 @t156))))) % 56.22/56.45 (assume @p52 (forall @t117 (= (tptp.f3 @t165 @t109) (tptp.f5 @t157 (tptp.f3 @t136 @t111))))) % 56.22/56.45 (assume @p53 (forall @t123 (= (tptp.f22 @t166 @t109) (* @t159 (tptp.f22 @t138 @t111))))) % 56.22/56.45 (assume @p54 (forall @t143 (= (tptp.f44 @t167 @t109) (tptp.f44 @t161 (tptp.f44 @t140 @t111))))) % 56.22/56.45 (assume @p55 (forall @t129 (= (tptp.f13 @t168 @t109) (* @t163 (tptp.f13 @t144 @t111))))) % 56.22/56.45 (assume @p56 (forall (@list @t95 @t31 @t170 @t109) (= (tptp.f3 @t172 @t109) (tptp.f5 @t157 (tptp.f3 @t171 @t169))))) % 56.22/56.45 (assume @p57 (forall (@list @t37 @t31 @t173 @t109) (= (tptp.f22 @t175 @t109) (* @t159 (tptp.f22 @t174 @t169))))) % 56.22/56.45 (assume @p58 (forall (@list @t41 @t31 @t176 @t109) (= (tptp.f13 @t178 @t109) (* @t163 (tptp.f13 @t177 @t169))))) % 56.22/56.45 (assume @p59 (forall @t135 (= (tptp.f3 @t179 @t109) (tptp.f5 (tptp.f6 tptp.f59 @t130) @t133)))) % 56.22/56.45 (assume @p60 (forall @t18 (= (tptp.f3 tptp.f131 @t1) tptp.f132))) % 56.22/56.45 (assume @p61 (forall @t18 (= (tptp.f22 tptp.f133 @t1) 0/1))) % 56.22/56.45 (assume @p62 @t191) % 56.22/56.45 (assume @p63 (< 0 @t9)) % 56.22/56.45 (assume @p64 (<= @t9 @t21)) % 56.22/56.45 (assume @p65 (forall @t195 (exists (@list @t193 @t192) (and (= @t193 @t44) (= @t192 @t88) (= (tptp.f3 (tptp.f8 tptp.f9 (tptp.f3 tptp.f10 @t194)) (tptp.f11 tptp.f12 (* @t193 (* 2 @t192)))) (tptp.f3 @t132 (tptp.f11 tptp.f12 (* @t193 @t192)))))))) % 56.22/56.45 (assume @p66 (forall @t195 (exists (@list @t198) (and (= @t198 @t2) (=> (< 0 @t198) (= (tptp.f3 (tptp.f8 tptp.f9 (tptp.f3 tptp.f10 (tptp.f11 tptp.f12 (* @t198 @t44)))) (tptp.f11 tptp.f12 (* @t198 @t88))) (tptp.f3 @t197 @t64))))))) % 56.22/56.45 (assume @p67 (exists (@list @t200) (and (= @t200 @t186) (exists (@list @t199) (and (= @t199 (tptp.f70 @t200 tptp.f15)) (= (tptp.f67 (tptp.f68 tptp.f69 tptp.f20) (tptp.f70 @t200 @t10)) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f67 (tptp.f68 tptp.f69 tptp.f19) @t199)) (tptp.f67 (tptp.f68 tptp.f69 tptp.f18) @t199)))))))) % 56.22/56.45 (assume @p68 (forall @t203 (= (tptp.f3 (tptp.f34 @t202 @t65) @t64) (tptp.f67 (tptp.f68 tptp.f69 @t134) @t201)))) % 56.22/56.45 (assume @p69 (forall @t195 (exists (@list @t204) (and (= @t204 @t207) (= (tptp.f136 @t205 @t204) (tptp.f136 (tptp.f137 tptp.f138 @t142) @t204)))))) % 56.22/56.45 (assume @p70 (forall @t210 (exists (@list @t208) (and (= @t208 @t207) (= (tptp.f75 @t209 @t208) (tptp.f75 (tptp.f76 tptp.f77 @t139) @t208)))))) % 56.22/56.45 (assume @p71 (forall @t213 (exists (@list @t211) (and (= @t211 @t207) (= (tptp.f67 @t212 @t211) (tptp.f67 (tptp.f68 tptp.f69 @t137) @t211)))))) % 56.22/56.45 (assume @p72 (forall @t216 (exists (@list @t214) (and (= @t214 @t207) (= (tptp.f139 @t215 @t214) (tptp.f139 (tptp.f140 tptp.f141 @t145) @t214)))))) % 56.22/56.45 (assume @p73 (forall @t195 (exists (@list @t217) (and (= @t217 @t207) (= (tptp.f136 (tptp.f137 tptp.f138 @t162) @t217) (tptp.f44 (tptp.f45 tptp.f107 @t31) (tptp.f136 @t205 @t217))))))) % 56.22/56.45 (assume @p74 (forall @t210 (exists (@list @t218) (and (= @t218 @t207) (= (tptp.f75 (tptp.f76 tptp.f77 @t160) @t218) (* @t36 (tptp.f75 @t209 @t218))))))) % 56.22/56.45 (assume @p75 (forall @t213 (exists (@list @t219) (and (= @t219 @t207) (= (tptp.f67 (tptp.f68 tptp.f69 @t158) @t219) (tptp.f5 @t220 (tptp.f67 @t212 @t219))))))) % 56.22/56.45 (assume @p76 (forall @t216 (exists (@list @t221) (and (= @t221 @t207) (= (tptp.f139 (tptp.f140 tptp.f141 @t164) @t221) (* @t40 (tptp.f139 @t215 @t221))))))) % 56.22/56.45 (assume @p77 (forall @t94 (exists (@list @t223) (and (= @t223 @t186) (= (tptp.f75 (tptp.f76 tptp.f77 @t93) (tptp.f70 @t223 @t64)) (tptp.f75 @t92 (tptp.f70 @t223 @t222))))))) % 56.22/56.45 (assume @p78 (forall @t89 (exists (@list @t224) (and (= @t224 @t186) (= (tptp.f67 (tptp.f68 tptp.f69 @t87) (tptp.f70 @t224 @t64)) (tptp.f67 @t86 (tptp.f70 @t224 @t222))))))) % 56.22/56.45 (assume @p79 (forall @t62 (exists (@list @t226) (and (= @t226 @t141) (= (tptp.f44 @t226 @t46) (tptp.f44 @t227 (tptp.f44 (tptp.f45 tptp.f108 (tptp.f44 @t226 @t31)) @t225))))))) % 56.22/56.45 (assume @p80 (forall @t229 (exists (@list @t228) (and (= @t228 @t122) (= (tptp.f22 @t228 @t46) (* @t37 (tptp.f22 (tptp.f24 tptp.f25 (tptp.f22 @t228 @t31)) @t225))))))) % 56.22/56.45 (assume @p81 (forall @t231 (exists (@list @t230) (and (= @t230 @t116) (= (tptp.f3 @t230 @t46) (tptp.f5 @t96 (tptp.f3 (tptp.f8 tptp.f9 (tptp.f3 @t230 @t31)) @t225))))))) % 56.22/56.45 (assume @p82 (forall @t233 (exists (@list @t232) (and (= @t232 @t128) (= (tptp.f13 @t232 @t46) (* @t41 (tptp.f13 (tptp.f98 tptp.f99 (tptp.f13 @t232 @t31)) @t225))))))) % 56.22/56.45 (assume @p83 (forall @t62 (exists (@list @t235) (and (= @t235 @t141) (exists (@list @t234) (and (= @t234 (tptp.f44 @t235 @t31)) (= (tptp.f44 @t235 @t46) (tptp.f44 @t227 (tptp.f44 (tptp.f45 tptp.f107 @t234) @t234))))))))) % 56.22/56.45 (assume @p84 (forall @t229 (exists (@list @t237) (and (= @t237 @t122) (exists (@list @t236) (and (= @t236 (tptp.f22 @t237 @t31)) (= (tptp.f22 @t237 @t46) (* @t37 (* @t236 @t236))))))))) % 56.22/56.45 (assume @p85 (forall @t231 (exists (@list @t239) (and (= @t239 @t116) (exists (@list @t238) (and (= @t238 (tptp.f3 @t239 @t31)) (= (tptp.f3 @t239 @t46) (tptp.f5 @t96 (tptp.f5 (tptp.f6 tptp.f7 @t238) @t238))))))))) % 56.22/56.45 (assume @p86 (forall @t233 (exists (@list @t241) (and (= @t241 @t128) (exists (@list @t240) (and (= @t240 (tptp.f13 @t241 @t31)) (= (tptp.f13 @t241 @t46) (* @t41 (* @t240 @t240))))))))) % 56.22/56.45 (assume @p87 (forall @t62 (exists (@list @t243) (and (= @t243 @t141) (exists (@list @t242) (and (= @t242 (tptp.f44 @t243 @t31)) (= (tptp.f44 @t243 @t54) (tptp.f44 (tptp.f45 tptp.f107 @t242) @t242)))))))) % 56.22/56.45 (assume @p88 (forall @t229 (exists (@list @t245) (and (= @t245 @t122) (exists (@list @t244) (and (= @t244 (tptp.f22 @t245 @t31)) (= (tptp.f22 @t245 @t54) (* @t244 @t244)))))))) % 56.22/56.45 (assume @p89 (forall @t231 (exists (@list @t247) (and (= @t247 @t116) (exists (@list @t246) (and (= @t246 (tptp.f3 @t247 @t31)) (= (tptp.f3 @t247 @t54) (tptp.f5 (tptp.f6 tptp.f7 @t246) @t246)))))))) % 56.22/56.45 (assume @p90 (forall @t233 (exists (@list @t249) (and (= @t249 @t128) (exists (@list @t248) (and (= @t248 (tptp.f13 @t249 @t31)) (= (tptp.f13 @t249 @t54) (* @t248 @t248)))))))) % 56.22/56.45 (assume @p91 (forall @t94 (= (tptp.f75 @t92 @t252) (tptp.f75 (tptp.f76 tptp.f77 @t60) @t251)))) % 56.22/56.45 (assume @p92 (forall @t89 (= (tptp.f67 @t86 @t252) (tptp.f67 (tptp.f68 tptp.f69 @t59) @t251)))) % 56.22/56.45 (assume @p93 (forall (@list @t32 @t31 @t64 @t109) (exists (@list @t255) (and (= @t255 @t88) (= (tptp.f75 @t92 (tptp.f70 (tptp.f71 (tptp.f11 tptp.f12 (+ @t44 @t255))) (tptp.f11 tptp.f12 (+ @t110 @t255)))) (tptp.f75 @t254 @t253)))))) % 56.22/56.45 (assume @p94 (forall (@list @t47 @t31 @t64 @t109) (exists (@list @t257) (and (= @t257 @t88) (= (tptp.f67 @t86 (tptp.f70 (tptp.f71 (tptp.f11 tptp.f12 (+ @t44 @t257))) (tptp.f11 tptp.f12 (+ @t110 @t257)))) (tptp.f67 @t256 @t253)))))) % 56.22/56.45 (assume @p95 (forall (@list @t37 @t70 @t258) (= (* @t37 @t260) (tptp.f75 (tptp.f76 tptp.f77 @t98) @t258)))) % 56.22/56.45 (assume @p96 (forall (@list @t95 @t65 @t258) (= (tptp.f5 @t96 @t262) (tptp.f67 (tptp.f68 tptp.f69 @t97) @t258)))) % 56.22/56.45 (assume @p97 (forall @t39 (= @t119 (+ @t36 @t37)))) % 56.22/56.45 (assume @p98 (forall @t264 (= @t113 (tptp.f5 @t263 @t95)))) % 56.22/56.45 (assume @p99 (forall @t43 (= @t125 (+ @t40 @t41)))) % 56.22/56.45 (assume @p100 (forall @t268 (= @t267 (+ @t36 @t265)))) % 56.22/56.45 (assume @p101 (forall @t271 (exists (@list @t269 @t270) (and (= @t269 @t112) (= @t270 @t263) (= (tptp.f5 @t269 (tptp.f5 @t270 @t170)) (tptp.f5 @t270 (tptp.f5 @t269 @t170))))))) % 56.22/56.45 (assume @p102 (forall @t275 (= @t274 (+ @t40 @t272)))) % 56.22/56.45 (assume @p103 (forall @t268 (= @t267 @t276))) % 56.22/56.45 (assume @p104 (forall @t271 (exists (@list @t277) (and (= @t277 @t112) (= (tptp.f5 @t277 @t278) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t277 @t77)) @t170)))))) % 56.22/56.45 (assume @p105 (forall @t275 (= @t274 @t279))) % 56.22/56.45 (assume @p106 (forall @t268 (= @t276 @t267))) % 56.22/56.45 (assume @p107 (forall @t271 (exists (@list @t280) (and (= @t280 @t112) (= (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t280 @t77)) @t170) (tptp.f5 @t280 @t278)))))) % 56.22/56.45 (assume @p108 (forall @t275 (= @t279 @t274))) % 56.22/56.45 (assume @p109 (forall @t268 (= @t276 (+ @t265 @t36)))) % 56.22/56.45 (assume @p110 (forall @t271 (exists (@list @t281) (and (= @t281 @t112) (= (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t281 @t77)) @t170) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t281 @t170)) @t77)))))) % 56.22/56.45 (assume @p111 (forall @t275 (= @t279 (+ @t272 @t40)))) % 56.22/56.45 (assume @p112 (forall @t284 (= (+ @t119 @t283) (+ @t265 (+ @t36 @t282))))) % 56.22/56.45 (assume @p113 (forall @t289 (exists (@list @t286) (and (= @t286 @t112) (= (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t286 @t77)) @t288) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t286 @t170)) (tptp.f5 @t263 @t285))))))) % 56.22/56.45 (assume @p114 (forall @t292 (= (+ @t125 @t291) (+ @t272 (+ @t40 @t290))))) % 56.22/56.45 (assume @p115 (forall @t229 (exists (@list @t293 @t294) (and (= @t293 1/1) (= @t294 @t122) (=> (not (= @t37 @t293)) (= (tptp.f75 (tptp.f76 tptp.f77 @t294) @t295) (/ (- (tptp.f22 @t294 @t31) @t293) (- @t37 @t293)))))))) % 56.22/56.45 (assume @p116 (forall @t35 (= (tptp.f75 (tptp.f76 tptp.f77 @t34) @t298) 0/1))) % 56.22/56.45 (assume @p117 (forall @t284 (= (= (+ @t38 @t301) (+ @t300 @t299)) (or (= @t37 @t173) (= @t36 @t282))))) % 56.22/56.45 (assume @p118 (forall @t289 (exists (@list @t303 @t302) (and (= @t303 @t96) (= @t302 @t304) (= (= (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t303 @t77)) (tptp.f5 @t302 @t285)) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t303 @t285)) (tptp.f5 @t302 @t77))) (or (= @t95 @t170) (= @t77 @t285))))))) % 56.22/56.45 (assume @p119 (forall @t292 (= (= (+ @t42 @t307) (+ @t306 @t305)) (or (= @t41 @t176) (= @t40 @t290))))) % 56.22/56.45 (assume @p120 (forall @t268 (= (+ @t38 @t299) @t308))) % 56.22/56.45 (assume @p121 (forall @t271 (= (tptp.f5 @t312 @t310) @t309))) % 56.22/56.45 (assume @p122 (forall @t275 (= (+ @t42 @t305) @t313))) % 56.22/56.45 (assume @p123 (forall @t268 (= (* @t119 @t173) (+ @t315 @t314)))) % 56.22/56.45 (assume @p124 (forall @t271 (= (tptp.f5 (tptp.f6 tptp.f7 @t113) @t170) (tptp.f5 (tptp.f6 tptp.f55 @t317) @t316)))) % 56.22/56.45 (assume @p125 (forall @t275 (= (* @t125 @t176) (+ @t319 @t318)))) % 56.22/56.45 (assume @p126 (forall @t284 (= (and (not (= @t37 @t36)) (not (= @t173 @t282))) (not (= (+ @t315 @t320) (+ @t300 @t314)))))) % 56.22/56.45 (assume @p127 (forall @t289 (exists (@list @t322 @t321) (and (= @t322 @t96) (= @t321 @t220) (= (and (not (= @t95 @t77)) (not (= @t170 @t285))) (not (= (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t322 @t170)) (tptp.f5 @t321 @t285)) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t322 @t285)) (tptp.f5 @t321 @t170))))))))) % 56.22/56.45 (assume @p128 (forall @t292 (= (and (not (= @t41 @t40)) (not (= @t176 @t290))) (not (= (+ @t319 @t323) (+ @t306 @t318)))))) % 56.22/56.45 (assume @p129 (forall @t268 (= (* @t37 @t266) (+ @t38 @t315)))) % 56.22/56.45 (assume @p130 (forall @t271 (exists (@list @t324) (and (= @t324 @t96) (= (tptp.f5 @t324 @t278) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t324 @t77)) (tptp.f5 @t324 @t170))))))) % 56.22/56.45 (assume @p131 (forall @t271 (exists (@list @t325) (and (= @t325 @t96) (= (tptp.f5 @t325 @t278) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t325 @t77)) (tptp.f5 @t325 @t170))))))) % 56.22/56.45 (assume @p132 (forall @t275 (= (* @t41 @t273) (+ @t42 @t319)))) % 56.22/56.45 (assume @p133 (forall @t271 (exists (@list @t326) (and (= @t326 @t96) (= (tptp.f5 @t326 @t278) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t326 @t77)) (tptp.f5 @t326 @t170))))))) % 56.22/56.45 (assume @p134 (forall @t62 (exists (@list @t327) (and (= @t327 @t141) (=> @t329 (= @t328 @t331)) (=> @t330 (= @t328 (tptp.f11 tptp.f12 (* @t2 (tptp.f13 tptp.f14 (tptp.f44 @t327 (tptp.f11 tptp.f12 (- @t44 1)))))))))))) % 56.22/56.45 (assume @p135 (forall @t18 (= (tptp.f75 (tptp.f76 tptp.f77 tptp.f23) (tptp.f70 @t186 @t194)) 0/1))) % 56.22/56.45 (assume @p136 (forall @t338 (exists (@list @t332 @t333) (and (= @t332 @t186) (= @t333 @t337) (= (tptp.f75 @t336 (tptp.f70 @t332 @t31)) (- (tptp.f75 @t333 (tptp.f70 @t332 @t334)) (tptp.f75 @t333 (tptp.f70 @t332 @t1)))))))) % 56.22/56.45 (assume @p137 (forall @t338 (exists (@list @t339 @t340) (and (= @t339 @t186) (= @t340 @t337) (= (tptp.f75 @t340 (tptp.f70 @t339 @t334)) (+ (tptp.f75 @t336 (tptp.f70 @t339 @t31)) (tptp.f75 @t340 (tptp.f70 @t339 @t1)))))))) % 56.22/56.45 (assume @p138 (forall @t342 (= (tptp.f75 (tptp.f76 tptp.f77 @t76) @t258) (+ @t341 @t260)))) % 56.22/56.45 (assume @p139 (forall @t344 (= (tptp.f67 (tptp.f68 tptp.f69 @t75) @t258) (tptp.f5 (tptp.f6 tptp.f55 @t343) @t262)))) % 56.22/56.45 (assume @p140 (forall @t351 (exists (@list @t347 @t346 @t345) (and (= @t347 @t44) (= @t346 @t350) (= @t345 @t348) (=> (<= @t2 @t347) (=> (<= @t347 @t88) (= (+ (tptp.f75 @t346 (tptp.f70 @t345 @t31)) (tptp.f75 @t346 @t251)) (tptp.f75 @t346 (tptp.f70 @t345 @t64))))))))) % 56.22/56.45 (assume @p141 (forall @t357 (exists (@list @t354 @t353 @t352) (and (= @t354 @t44) (= @t353 @t356) (= @t352 @t348) (=> (<= @t2 @t354) (=> (<= @t354 @t88) (= (tptp.f5 (tptp.f6 tptp.f55 (tptp.f67 @t353 (tptp.f70 @t352 @t31))) (tptp.f67 @t353 @t251)) (tptp.f67 @t353 (tptp.f70 @t352 @t64))))))))) % 56.22/56.45 (assume @p142 (forall @t363 (exists (@list @t360 @t359 @t358) (and (= @t360 @t44) (= @t359 @t362) (= @t358 @t348) (=> (<= @t2 @t360) (=> (<= @t360 @t88) (= (+ (tptp.f139 @t359 (tptp.f70 @t358 @t31)) (tptp.f139 @t359 @t251)) (tptp.f139 @t359 (tptp.f70 @t358 @t64))))))))) % 56.22/56.45 (assume @p143 (forall @t338 (exists (@list @t364 @t365) (and (= @t364 @t2) (= @t365 @t337) (=> (< @t364 @t44) (= (tptp.f75 @t365 @t366) (+ (tptp.f22 @t335 @t1) (tptp.f75 @t365 (tptp.f70 (tptp.f71 (tptp.f11 tptp.f12 (+ @t364 1))) @t31))))))))) % 56.22/56.45 (assume @p144 (forall (@list @t1 @t31 @t369) (exists (@list @t367 @t368) (and (= @t367 @t2) (= @t368 @t370) (=> (< @t367 @t44) (= (tptp.f67 @t368 @t366) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f3 @t369 @t1)) (tptp.f67 @t368 (tptp.f70 (tptp.f71 (tptp.f11 tptp.f12 (+ @t367 1))) @t31))))))))) % 56.22/56.45 (assume @p145 (forall (@list @t1 @t31 @t373) (exists (@list @t371 @t372) (and (= @t371 @t2) (= @t372 (tptp.f140 tptp.f141 @t373)) (=> (< @t371 @t44) (= (tptp.f139 @t372 @t366) (+ (tptp.f13 @t373 @t1) (tptp.f139 @t372 (tptp.f70 (tptp.f71 (tptp.f11 tptp.f12 (+ @t371 1))) @t31))))))))) % 56.22/56.45 (assume @p146 (forall @t94 (exists (@list @t374 @t375) (and (= @t374 @t186) (= @t375 @t92) (= (tptp.f75 @t375 (tptp.f70 @t374 @t376)) (+ (tptp.f75 @t254 (tptp.f70 @t374 @t31)) (tptp.f75 @t375 (tptp.f70 @t374 @t64)))))))) % 56.22/56.45 (assume @p147 (forall @t89 (exists (@list @t377 @t378) (and (= @t377 @t186) (= @t378 @t86) (= (tptp.f67 @t378 (tptp.f70 @t377 @t376)) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f67 @t256 (tptp.f70 @t377 @t31))) (tptp.f67 @t378 (tptp.f70 @t377 @t64)))))))) % 56.22/56.45 (assume @p148 (forall @t106 (exists (@list @t379 @t380) (and (= @t379 @t186) (= @t380 @t381) (= (tptp.f139 @t380 (tptp.f70 @t379 @t376)) (+ (tptp.f139 (tptp.f140 tptp.f141 (tptp.f84 @t104 @t64)) (tptp.f70 @t379 @t31)) (tptp.f139 @t380 (tptp.f70 @t379 @t64)))))))) % 56.22/56.45 (assume @p149 (forall (@list @t32) (exists (@list @t383) (and (= @t383 @t185) (= (tptp.f75 @t92 (tptp.f70 (tptp.f71 @t383) @t384)) (+ (+ (+ (tptp.f22 @t32 @t383) (tptp.f22 @t32 @t331)) (tptp.f22 @t32 @t225)) (tptp.f22 @t32 @t382))))))) % 56.22/56.45 (assume @p150 (forall (@list @t47) (exists (@list @t385) (and (= @t385 @t185) (= (tptp.f67 @t86 (tptp.f70 (tptp.f71 @t385) @t384)) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 (tptp.f6 tptp.f55 (tptp.f3 @t47 @t385)) (tptp.f3 @t47 @t331))) (tptp.f3 @t47 @t225))) (tptp.f3 @t47 @t382))))))) % 56.22/56.45 (assume @p151 (forall (@list @t51) (exists (@list @t386) (and (= @t386 @t185) (= (tptp.f139 @t381 (tptp.f70 (tptp.f71 @t386) @t384)) (+ (+ (+ (tptp.f13 @t51 @t386) (tptp.f13 @t51 @t331)) (tptp.f13 @t51 @t225)) (tptp.f13 @t51 @t382))))))) % 56.22/56.45 (assume @p152 (forall @t284 (= (* @t38 @t301) (* @t315 @t320)))) % 56.22/56.45 (assume @p153 (forall @t292 (= (* @t42 @t307) (* @t319 @t323)))) % 56.22/56.45 (assume @p154 (forall @t289 (exists (@list @t388) (and (= @t388 @t96) (= (tptp.f5 (tptp.f6 tptp.f7 (tptp.f5 @t388 @t77)) @t389) (tptp.f5 (tptp.f6 tptp.f7 (tptp.f5 @t388 @t170)) @t387)))))) % 56.22/56.45 (assume @p155 (forall @t284 (exists (@list @t390) (and (= @t390 @t38) (= (* @t390 @t301) (* @t173 (* @t390 @t282))))))) % 56.22/56.45 (assume @p156 (forall @t292 (exists (@list @t391) (and (= @t391 @t42) (= (* @t391 @t307) (* @t176 (* @t391 @t290))))))) % 56.22/56.45 (assume @p157 (forall @t289 (exists (@list @t392 @t393) (and (= @t392 @t394) (= @t393 @t304) (= (tptp.f5 @t392 (tptp.f5 @t393 @t285)) (tptp.f5 @t393 (tptp.f5 @t392 @t285))))))) % 56.22/56.45 (assume @p158 (forall @t284 (exists (@list @t395) (and (= @t395 @t301) (= (* @t38 @t395) (* @t37 (* @t36 @t395))))))) % 56.22/56.45 (assume @p159 (forall @t292 (exists (@list @t396) (and (= @t396 @t307) (= (* @t42 @t396) (* @t41 (* @t40 @t396))))))) % 56.22/56.45 (assume @p160 (forall @t289 (exists (@list @t398 @t397) (and (= @t398 @t96) (= @t397 @t389) (= (tptp.f5 (tptp.f6 tptp.f7 (tptp.f5 @t398 @t77)) @t397) (tptp.f5 @t398 (tptp.f5 @t220 @t397))))))) % 56.22/56.45 (assume @p161 (forall @t268 (= @t399 (* @t315 @t36)))) % 56.22/56.45 (assume @p162 (forall @t275 (= @t400 (* @t319 @t40)))) % 56.22/56.45 (assume @p163 (forall @t271 (exists (@list @t401) (and (= @t401 @t96) (= (tptp.f5 (tptp.f6 tptp.f7 (tptp.f5 @t401 @t77)) @t170) (tptp.f5 (tptp.f6 tptp.f7 (tptp.f5 @t401 @t170)) @t77)))))) % 56.22/56.45 (assume @p164 (forall @t268 (= @t399 @t402))) % 56.22/56.45 (assume @p165 (forall @t275 (= @t400 @t403))) % 56.22/56.45 (assume @p166 @t410) % 56.22/56.45 (assume @p167 (forall @t268 (= @t402 @t399))) % 56.22/56.45 (assume @p168 (forall @t275 (= @t403 @t400))) % 56.22/56.45 (assume @p169 (forall @t271 (exists (@list @t411) (and (= @t411 @t96) (= (tptp.f5 @t411 @t316) (tptp.f5 (tptp.f6 tptp.f7 (tptp.f5 @t411 @t77)) @t170)))))) % 56.22/56.45 (assume @p170 (forall @t268 (= @t402 (* @t36 @t315)))) % 56.22/56.45 (assume @p171 (forall @t275 (= @t403 (* @t40 @t319)))) % 56.22/56.45 (assume @p172 (forall @t271 (exists (@list @t412 @t413) (and (= @t412 @t96) (= @t413 @t220) (= (tptp.f5 @t412 (tptp.f5 @t413 @t170)) (tptp.f5 @t413 (tptp.f5 @t412 @t170))))))) % 56.22/56.45 (assume @p173 (forall @t39 (= @t38 @t414))) % 56.22/56.45 (assume @p174 (forall @t43 (= @t42 (* @t40 @t41)))) % 56.22/56.45 (assume @p175 (forall @t264 (= @t311 @t415))) % 56.22/56.45 (assume @p176 (forall @t419 (exists (@list @t416) (and (= @t416 @t225) (= (tptp.f22 @t418 @t416) (tptp.f22 @t122 @t416)))))) % 56.22/56.45 (assume @p177 (forall @t18 (= (tptp.f44 @t141 @t331) @t1))) % 56.22/56.45 (assume @p178 (forall @t419 (= (tptp.f22 @t122 @t331) @t37))) % 56.22/56.45 (assume @p179 (forall @t420 (= (tptp.f3 @t116 @t331) @t95))) % 56.22/56.45 (assume @p180 (forall @t419 (exists (@list @t421) (and (= @t421 @t422) (= (tptp.f28 tptp.f48 @t421) @t421))))) % 56.22/56.45 (assume @p181 (forall @t18 (exists (@list @t423) (and (= @t423 @t2) (= (tptp.f11 tptp.f12 (* 2 @t423)) (tptp.f11 tptp.f12 (+ @t423 @t423))))))) % 56.22/56.45 (assume @p182 (forall @t18 (exists (@list @t424) (and (= @t424 @t2) (= (tptp.f11 tptp.f12 (* @t424 2)) (tptp.f11 tptp.f12 (+ @t424 @t424))))))) % 56.22/56.45 (assume @p183 (forall @t62 (exists (@list @t428 @t426 @t425) (and (= @t428 @t185) (= @t426 @t2) (= @t425 @t44) (=> @t429 (= @t427 @t428)) (=> (not @t429) (= @t427 (tptp.f11 tptp.f12 (+ @t425 (* (tptp.f13 tptp.f14 (tptp.f11 tptp.f12 (- @t426 1))) @t425))))))))) % 56.22/56.45 (assume @p184 (forall @t35 (exists (@list @t431) (and (= @t431 @t186) (exists (@list @t430) (and (= @t430 (tptp.f70 @t431 @t31)) (= (tptp.f75 @t92 (tptp.f70 @t431 @t54)) (+ (tptp.f75 (tptp.f76 tptp.f77 @t56) @t430) (tptp.f75 (tptp.f76 tptp.f77 @t50) @t430))))))))) % 56.22/56.45 (assume @p185 (forall @t49 (exists (@list @t433) (and (= @t433 @t186) (exists (@list @t432) (and (= @t432 (tptp.f70 @t433 @t31)) (= (tptp.f67 @t86 (tptp.f70 @t433 @t54)) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f67 (tptp.f68 tptp.f69 @t55) @t432)) (tptp.f67 (tptp.f68 tptp.f69 @t48) @t432))))))))) % 56.22/56.45 (assume @p186 (forall @t53 (exists (@list @t435) (and (= @t435 @t186) (exists (@list @t434) (and (= @t434 (tptp.f70 @t435 @t31)) (= (tptp.f139 @t381 (tptp.f70 @t435 @t54)) (+ (tptp.f139 (tptp.f140 tptp.f141 @t57) @t434) (tptp.f139 (tptp.f140 tptp.f141 @t52) @t434))))))))) % 56.22/56.45 (assume @p187 (forall @t203 (exists (@list @t437 @t436) (and (= @t437 @t194) (= @t436 @t202) (= (tptp.f3 (tptp.f34 (tptp.f134 tptp.f135 @t437) @t65) @t64) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f3 (tptp.f34 @t436 (tptp.f34 tptp.f39 @t65)) @t64)) (tptp.f5 (tptp.f6 tptp.f7 (tptp.f3 (tptp.f8 tptp.f9 (tptp.f3 tptp.f10 @t437)) @t64)) (tptp.f3 (tptp.f34 @t436 (tptp.f34 tptp.f35 @t65)) @t64)))))))) % 56.22/56.45 (assume @p188 (forall (@list @t32 @t439) (exists (@list @t438) (and (= @t438 (tptp.f75 (tptp.f76 tptp.f77 @t63) @t439)) (= (tptp.f28 tptp.f48 @t438) @t438))))) % 56.22/56.45 (assume @p189 (forall @t195 (exists (@list @t441 @t440 @t442) (and (= @t441 @t44) (= @t440 @t2) (= @t442 (tptp.f45 tptp.f108 @t64)) (=> (<= @t440 @t441) (= (tptp.f44 @t442 (tptp.f11 tptp.f12 (- (+ @t441 1) @t440))) (tptp.f44 (tptp.f45 tptp.f107 (tptp.f44 @t442 (tptp.f11 tptp.f12 (- @t441 @t440)))) @t64))))))) % 56.22/56.45 (assume @p190 (forall (@list @t1 @t31 @t173) (exists (@list @t444 @t443 @t445) (and (= @t444 @t44) (= @t443 @t2) (= @t445 @t174) (=> (<= @t443 @t444) (= (tptp.f22 @t445 (tptp.f11 tptp.f12 (- (+ @t444 1) @t443))) (* (tptp.f22 @t445 (tptp.f11 tptp.f12 (- @t444 @t443))) @t173))))))) % 56.22/56.45 (assume @p191 (forall (@list @t1 @t31 @t170) (exists (@list @t447 @t446 @t448) (and (= @t447 @t44) (= @t446 @t2) (= @t448 @t171) (=> (<= @t446 @t447) (= (tptp.f3 @t448 (tptp.f11 tptp.f12 (- (+ @t447 1) @t446))) (tptp.f5 (tptp.f6 tptp.f7 (tptp.f3 @t448 (tptp.f11 tptp.f12 (- @t447 @t446)))) @t170))))))) % 56.22/56.45 (assume @p192 (forall (@list @t1 @t31 @t176) (exists (@list @t450 @t449 @t451) (and (= @t450 @t44) (= @t449 @t2) (= @t451 @t177) (=> (<= @t449 @t450) (= (tptp.f13 @t451 (tptp.f11 tptp.f12 (- (+ @t450 1) @t449))) (* (tptp.f13 @t451 (tptp.f11 tptp.f12 (- @t450 @t449))) @t176))))))) % 56.22/56.45 (assume @p193 (forall @t195 (exists (@list @t452) (and (= @t452 @t141) (= (tptp.f44 (tptp.f45 tptp.f107 (tptp.f44 @t452 @t31)) (tptp.f44 @t452 @t64)) (tptp.f44 @t452 @t376)))))) % 56.22/56.45 (assume @p194 (forall @t454 (exists (@list @t453) (and (= @t453 @t122) (= (* (tptp.f22 @t453 @t31) (tptp.f22 @t453 @t64)) (tptp.f22 @t453 @t376)))))) % 56.22/56.45 (assume @p195 (forall @t456 (exists (@list @t455) (and (= @t455 @t116) (= (tptp.f5 (tptp.f6 tptp.f7 (tptp.f3 @t455 @t31)) (tptp.f3 @t455 @t64)) (tptp.f3 @t455 @t376)))))) % 56.22/56.45 (assume @p196 (forall @t458 (exists (@list @t457) (and (= @t457 @t128) (= (* (tptp.f13 @t457 @t31) (tptp.f13 @t457 @t64)) (tptp.f13 @t457 @t376)))))) % 56.22/56.45 (assume @p197 (forall @t195 (= (tptp.f44 (tptp.f45 tptp.f108 (tptp.f44 @t227 @t31)) @t64) (tptp.f44 (tptp.f45 tptp.f107 (tptp.f44 @t141 @t64)) (tptp.f44 @t140 @t64))))) % 56.22/56.45 (assume @p198 (forall @t210 (= (tptp.f22 (tptp.f24 tptp.f25 @t38) @t64) (* @t460 @t459)))) % 56.22/56.45 (assume @p199 (forall @t213 (= (tptp.f3 (tptp.f8 tptp.f9 @t311) @t64) (tptp.f5 (tptp.f6 tptp.f7 @t462) @t461)))) % 56.22/56.45 (assume @p200 (forall @t216 (= (tptp.f13 (tptp.f98 tptp.f99 @t42) @t64) (* (tptp.f13 @t128 @t64) (tptp.f13 @t144 @t64))))) % 56.22/56.45 (assume @p201 (forall @t62 (exists (@list @t463) (and (= @t463 @t141) (= (tptp.f44 (tptp.f45 tptp.f107 (tptp.f44 @t463 @t31)) @t1) (tptp.f44 @t463 @t58)))))) % 56.22/56.45 (assume @p202 (forall @t229 (exists (@list @t464) (and (= @t464 @t122) (= (* (tptp.f22 @t464 @t31) @t37) (tptp.f22 @t464 @t58)))))) % 56.22/56.45 (assume @p203 (forall @t231 (exists (@list @t465) (and (= @t465 @t116) (= (tptp.f5 (tptp.f6 tptp.f7 (tptp.f3 @t465 @t31)) @t95) (tptp.f3 @t465 @t58)))))) % 56.22/56.45 (assume @p204 (forall @t233 (exists (@list @t466) (and (= @t466 @t128) (= (* (tptp.f13 @t466 @t31) @t41) (tptp.f13 @t466 @t58)))))) % 56.22/56.45 (assume @p205 (forall @t62 (exists (@list @t467) (and (= @t467 @t141) (= (tptp.f44 @t227 (tptp.f44 @t467 @t31)) (tptp.f44 @t467 @t58)))))) % 56.22/56.45 (assume @p206 (forall @t229 (exists (@list @t468) (and (= @t468 @t122) (= (* @t37 (tptp.f22 @t468 @t31)) (tptp.f22 @t468 @t58)))))) % 56.22/56.45 (assume @p207 (forall @t231 (exists (@list @t469) (and (= @t469 @t116) (= (tptp.f5 @t96 (tptp.f3 @t469 @t31)) (tptp.f3 @t469 @t58)))))) % 56.22/56.45 (assume @p208 (forall @t233 (exists (@list @t470) (and (= @t470 @t128) (= (* @t41 (tptp.f13 @t470 @t31)) (tptp.f13 @t470 @t58)))))) % 56.22/56.45 (assume @p209 (forall @t18 (= (tptp.f44 @t141 @t382) (tptp.f44 (tptp.f45 tptp.f107 @t471) @t1)))) % 56.22/56.45 (assume @p210 (forall @t419 (= (tptp.f22 @t122 @t382) (* @t472 @t37)))) % 56.22/56.45 (assume @p211 (forall @t420 (= (tptp.f3 @t116 @t382) (tptp.f5 (tptp.f6 tptp.f7 @t473) @t95)))) % 56.22/56.45 (assume @p212 (forall @t475 (= (tptp.f13 @t128 @t382) (* @t474 @t41)))) % 56.22/56.45 (assume @p213 (forall @t18 (= @t476 @t471))) % 56.22/56.45 (assume @p214 (forall @t419 (= @t422 @t472))) % 56.22/56.45 (assume @p215 (forall @t420 (= @t477 @t473))) % 56.22/56.45 (assume @p216 (forall @t475 (= @t478 @t474))) % 56.22/56.45 (assume @p217 (forall @t62 (exists (@list @t479) (and (= @t479 @t141) (= (tptp.f44 @t479 @t58) (tptp.f44 @t227 (tptp.f44 @t479 @t31))))))) % 56.22/56.45 (assume @p218 (forall @t229 (exists (@list @t480) (and (= @t480 @t122) (= (tptp.f22 @t480 @t58) (* @t37 (tptp.f22 @t480 @t31))))))) % 56.22/56.45 (assume @p219 (forall @t231 (exists (@list @t481) (and (= @t481 @t116) (= (tptp.f3 @t481 @t58) (tptp.f5 @t96 (tptp.f3 @t481 @t31))))))) % 56.22/56.45 (assume @p220 (forall @t233 (exists (@list @t482) (and (= @t482 @t128) (= (tptp.f13 @t482 @t58) (* @t41 (tptp.f13 @t482 @t31))))))) % 56.22/56.45 (assume @p221 (forall @t18 (= @t471 @t476))) % 56.22/56.45 (assume @p222 (forall @t419 (= @t472 @t422))) % 56.22/56.45 (assume @p223 (forall @t420 (= @t473 @t477))) % 56.22/56.45 (assume @p224 (forall @t475 (= @t474 @t478))) % 56.22/56.45 (assume @p225 (forall @t195 (exists (@list @t484) (and (= @t484 @t141) (= (tptp.f44 (tptp.f45 tptp.f108 (tptp.f44 @t484 @t31)) @t64) (tptp.f44 @t484 @t483)))))) % 56.22/56.45 (assume @p226 (forall @t454 (exists (@list @t485) (and (= @t485 @t122) (= (tptp.f22 (tptp.f24 tptp.f25 (tptp.f22 @t485 @t31)) @t64) (tptp.f22 @t485 @t483)))))) % 56.22/56.45 (assume @p227 (forall @t456 (exists (@list @t486) (and (= @t486 @t116) (= (tptp.f3 (tptp.f8 tptp.f9 (tptp.f3 @t486 @t31)) @t64) (tptp.f3 @t486 @t483)))))) % 56.22/56.45 (assume @p228 (forall @t62 (exists (@list @t487) (and (= @t487 @t141) (= (tptp.f44 @t487 @t54) (tptp.f44 (tptp.f45 tptp.f108 (tptp.f44 @t487 @t31)) @t225)))))) % 56.22/56.45 (assume @p229 (forall @t229 (exists (@list @t488) (and (= @t488 @t122) (= (tptp.f22 @t488 @t54) (tptp.f22 (tptp.f24 tptp.f25 (tptp.f22 @t488 @t31)) @t225)))))) % 56.22/56.45 (assume @p230 (forall @t231 (exists (@list @t489) (and (= @t489 @t116) (= (tptp.f3 @t489 @t54) (tptp.f3 (tptp.f8 tptp.f9 (tptp.f3 @t489 @t31)) @t225)))))) % 56.22/56.45 (assume @p231 (forall @t491 (= (* @t490 @t173) (tptp.f75 (tptp.f76 tptp.f77 (tptp.f24 @t83 @t173)) @t439)))) % 56.22/56.45 (assume @p232 (forall @t493 (= (tptp.f5 (tptp.f6 tptp.f7 @t492) @t170) (tptp.f67 (tptp.f68 tptp.f69 (tptp.f8 @t82 @t170)) @t439)))) % 56.22/56.45 (assume @p233 (forall @t195 (exists (@list @t494) (and (= @t494 @t141) (= (tptp.f44 @t494 @t483) (tptp.f44 (tptp.f45 tptp.f108 (tptp.f44 @t494 @t31)) @t64)))))) % 56.22/56.45 (assume @p234 (forall @t454 (exists (@list @t495) (and (= @t495 @t122) (= (tptp.f22 @t495 @t483) (tptp.f22 (tptp.f24 tptp.f25 (tptp.f22 @t495 @t31)) @t64)))))) % 56.22/56.45 (assume @p235 (forall @t456 (exists (@list @t496) (and (= @t496 @t116) (= (tptp.f3 @t496 @t483) (tptp.f3 (tptp.f8 tptp.f9 (tptp.f3 @t496 @t31)) @t64)))))) % 56.22/56.45 (assume @p236 (forall @t62 (exists (@list @t498 @t497) (and (= @t498 @t2) (= @t497 @t140) (=> (< 0 @t498) (= (tptp.f44 (tptp.f45 tptp.f107 (tptp.f44 @t497 (tptp.f11 tptp.f12 (- @t498 1)))) @t31) (tptp.f44 @t497 @t1))))))) % 56.22/56.45 (assume @p237 (forall (@list @t1 @t36) (exists (@list @t500 @t499) (and (= @t500 @t2) (= @t499 @t138) (=> (< 0 @t500) (= (* (tptp.f22 @t499 (tptp.f11 tptp.f12 (- @t500 1))) @t36) (tptp.f22 @t499 @t1))))))) % 56.22/56.45 (assume @p238 (forall (@list @t1 @t77) (exists (@list @t502 @t501) (and (= @t502 @t2) (= @t501 @t136) (=> (< 0 @t502) (= (tptp.f5 (tptp.f6 tptp.f7 (tptp.f3 @t501 (tptp.f11 tptp.f12 (- @t502 1)))) @t77) (tptp.f3 @t501 @t1))))))) % 56.22/56.45 (assume @p239 (forall (@list @t1 @t40) (exists (@list @t504 @t503) (and (= @t504 @t2) (= @t503 @t144) (=> (< 0 @t504) (= (* (tptp.f13 @t503 (tptp.f11 tptp.f12 (- @t504 1))) @t40) (tptp.f13 @t503 @t1))))))) % 56.22/56.45 (assume @p240 (forall @t62 (exists (@list @t505) (and (= @t505 @t506) (= (tptp.f44 (tptp.f45 tptp.f107 @t505) @t1) (tptp.f44 @t227 @t505)))))) % 56.22/56.45 (assume @p241 (forall @t229 (exists (@list @t507) (and (= @t507 @t508) (= (* @t507 @t37) (* @t37 @t507)))))) % 56.22/56.45 (assume @p242 (forall @t231 (exists (@list @t509) (and (= @t509 @t510) (= (tptp.f5 (tptp.f6 tptp.f7 @t509) @t95) (tptp.f5 @t96 @t509)))))) % 56.22/56.45 (assume @p243 (forall @t233 (exists (@list @t511) (and (= @t511 @t512) (= (* @t511 @t41) (* @t41 @t511)))))) % 56.22/56.45 (assume @p244 (forall @t195 (exists (@list @t513) (and (= @t513 @t141) (= (tptp.f44 @t513 @t376) (tptp.f44 (tptp.f45 tptp.f107 (tptp.f44 @t513 @t31)) (tptp.f44 @t513 @t64))))))) % 56.22/56.45 (assume @p245 (forall @t454 (exists (@list @t514) (and (= @t514 @t122) (= (tptp.f22 @t514 @t376) (* (tptp.f22 @t514 @t31) (tptp.f22 @t514 @t64))))))) % 56.22/56.45 (assume @p246 (forall @t456 (exists (@list @t515) (and (= @t515 @t116) (= (tptp.f3 @t515 @t376) (tptp.f5 (tptp.f6 tptp.f7 (tptp.f3 @t515 @t31)) (tptp.f3 @t515 @t64))))))) % 56.22/56.45 (assume @p247 (forall @t458 (exists (@list @t516) (and (= @t516 @t128) (= (tptp.f13 @t516 @t376) (* (tptp.f13 @t516 @t31) (tptp.f13 @t516 @t64))))))) % 56.22/56.45 (assume @p248 (forall @t62 (exists (@list @t517) (and (= @t517 @t141) (= (tptp.f44 @t517 @t58) (tptp.f44 (tptp.f45 tptp.f107 (tptp.f44 @t517 @t31)) @t1)))))) % 56.22/56.45 (assume @p249 (forall @t229 (exists (@list @t518) (and (= @t518 @t122) (= (tptp.f22 @t518 @t58) (* (tptp.f22 @t518 @t31) @t37)))))) % 56.22/56.45 (assume @p250 (forall @t231 (exists (@list @t519) (and (= @t519 @t116) (= (tptp.f3 @t519 @t58) (tptp.f5 (tptp.f6 tptp.f7 (tptp.f3 @t519 @t31)) @t95)))))) % 56.22/56.45 (assume @p251 (forall @t233 (exists (@list @t520) (and (= @t520 @t128) (= (tptp.f13 @t520 @t58) (* (tptp.f13 @t520 @t31) @t41)))))) % 56.22/56.45 (assume @p252 (forall @t62 (exists (@list @t521) (and (= @t521 @t141) (= (tptp.f44 @t521 @t58) (tptp.f44 @t227 (tptp.f44 @t521 @t31))))))) % 56.22/56.45 (assume @p253 (forall @t229 (exists (@list @t522) (and (= @t522 @t122) (= (tptp.f22 @t522 @t58) (* @t37 (tptp.f22 @t522 @t31))))))) % 56.22/56.45 (assume @p254 (forall @t231 (exists (@list @t523) (and (= @t523 @t116) (= (tptp.f3 @t523 @t58) (tptp.f5 @t96 (tptp.f3 @t523 @t31))))))) % 56.22/56.45 (assume @p255 (forall @t233 (exists (@list @t524) (and (= @t524 @t128) (= (tptp.f13 @t524 @t58) (* @t41 (tptp.f13 @t524 @t31))))))) % 56.22/56.45 (assume @p256 (forall @t284 (= (+ @t38 (+ @t299 @t282)) (+ @t308 @t282)))) % 56.22/56.45 (assume @p257 (forall @t289 (= (tptp.f5 @t312 (tptp.f5 @t525 @t285)) (tptp.f5 (tptp.f6 tptp.f55 @t309) @t285)))) % 56.22/56.45 (assume @p258 (forall @t292 (= (+ @t42 (+ @t305 @t290)) (+ @t313 @t290)))) % 56.22/56.45 (assume @p259 (forall (@list @t1 @t31 @t64 @t349 @t527 @t528) (exists (@list @t532 @t526) (and (= @t532 @t44) (= @t526 @t348) (=> (<= @t2 @t532) (=> (<= @t532 @t88) (=> (forall @t534 (exists (@list @t535) (and (= @t535 @t533) (=> (<= @t2 @t535) (=> (< @t535 @t532) (= (tptp.f22 @t349 @t529) @t530)))))) (=> (forall @t534 (exists (@list @t531) (and (= @t531 @t533) (=> (<= @t532 @t531) (=> (< @t531 @t88) (= (tptp.f22 @t528 @t529) @t530)))))) (= (+ (tptp.f75 @t350 (tptp.f70 @t526 @t31)) (tptp.f75 (tptp.f76 tptp.f77 @t528) @t251)) (tptp.f75 (tptp.f76 tptp.f77 @t527) (tptp.f70 @t526 @t64))))))))))) % 56.22/56.45 (assume @p260 (forall (@list @t1 @t31 @t64 @t355 @t537 @t538) (exists (@list @t541 @t536) (and (= @t541 @t44) (= @t536 @t348) (=> (<= @t2 @t541) (=> (<= @t541 @t88) (=> (forall @t534 (exists (@list @t542) (and (= @t542 @t533) (=> (<= @t2 @t542) (=> (< @t542 @t541) (= (tptp.f3 @t355 @t529) @t539)))))) (=> (forall @t534 (exists (@list @t540) (and (= @t540 @t533) (=> (<= @t541 @t540) (=> (< @t540 @t88) (= (tptp.f3 @t538 @t529) @t539)))))) (= (tptp.f5 (tptp.f6 tptp.f55 (tptp.f67 @t356 (tptp.f70 @t536 @t31))) (tptp.f67 (tptp.f68 tptp.f69 @t538) @t251)) (tptp.f67 (tptp.f68 tptp.f69 @t537) (tptp.f70 @t536 @t64))))))))))) % 56.22/56.45 (assume @p261 (forall (@list @t1 @t31 @t64 @t361 @t544 @t545) (exists (@list @t548 @t543) (and (= @t548 @t44) (= @t543 @t348) (=> (<= @t2 @t548) (=> (<= @t548 @t88) (=> (forall @t534 (exists (@list @t549) (and (= @t549 @t533) (=> (<= @t2 @t549) (=> (< @t549 @t548) (= (tptp.f13 @t361 @t529) @t546)))))) (=> (forall @t534 (exists (@list @t547) (and (= @t547 @t533) (=> (<= @t548 @t547) (=> (< @t547 @t88) (= (tptp.f13 @t545 @t529) @t546)))))) (= (+ (tptp.f139 @t362 (tptp.f70 @t543 @t31)) (tptp.f139 (tptp.f140 tptp.f141 @t545) @t251)) (tptp.f139 (tptp.f140 tptp.f141 @t544) (tptp.f70 @t543 @t64))))))))))) % 56.22/56.45 (assume @p262 (forall @t18 (<= 1/1 (tptp.f22 (tptp.f24 tptp.f25 2/1) @t1)))) % 56.22/56.45 (assume @p263 (forall @t39 (exists (@list @t550) (and (= @t550 @t225) (<= (- (tptp.f22 @t122 @t550)) (tptp.f22 @t138 @t550)))))) % 56.22/56.45 (assume @p264 (forall @t62 (= (< 0 @t552) (or @t551 @t329)))) % 56.22/56.45 (assume @p265 (forall @t18 (exists (@list @t553) (and (= @t553 @t297) (= (tptp.f44 (tptp.f45 tptp.f108 @t553) @t1) @t553))))) % 56.22/56.45 (assume @p266 (forall @t62 (exists (@list @t554) (and (= @t554 @t297) (= (= @t506 @t554) (or @t329 (= @t1 @t554))))))) % 56.22/56.45 (assume @p267 (forall @t39 (exists (@list @t555 @t556) (and (= @t555 0/1) (= @t556 @t225) (= (= (+ (tptp.f22 @t122 @t556) (tptp.f22 @t138 @t556)) @t555) (and (= @t37 @t555) (= @t36 @t555))))))) % 56.22/56.45 (assume @p268 (forall @t195 (exists (@list @t557) (and (= @t557 @t141) (=> @t551 (=> (< (tptp.f13 tptp.f14 (tptp.f44 @t557 @t31)) (tptp.f13 tptp.f14 (tptp.f44 @t557 @t64))) (< @t44 @t88))))))) % 56.22/56.45 (assume @p269 (forall @t62 (exists (@list @t558) (and (= @t558 @t296) (=> (<= @t558 @t2) (<= @t558 @t552)))))) % 56.22/56.45 (assume @p270 (forall @t419 (exists (@list @t559) (and (= @t559 1/1) (=> (and (=> @t560 (< (- @t37) @t559)) (=> (not @t560) (< @t37 @t559))) (< @t422 @t559)))))) % 56.22/56.45 (assume @p271 (forall @t39 (= (tptp.f28 tptp.f48 @t38) (* @t417 @t561)))) % 56.22/56.45 (assume @p272 (forall @t43 (= (tptp.f31 tptp.f142 @t42) (* @t562 (tptp.f31 tptp.f142 @t40))))) % 56.22/56.45 (assume @p273 (forall @t419 (exists (@list @t563) (and (= @t563 @t417) (= (* @t563 @t563) @t472))))) % 56.22/56.45 (assume @p274 (forall @t475 (exists (@list @t564) (and (= @t564 @t562) (= (* @t564 @t564) @t474))))) % 56.22/56.45 (assume @p275 (forall @t229 (= (tptp.f28 tptp.f48 @t508) (tptp.f22 @t418 @t31)))) % 56.22/56.45 (assume @p276 (forall @t62 (exists (@list @t565) (and (= @t565 @t2) (=> (< 0 @t565) (=> (< @t565 @t44) (= (tptp.f67 (tptp.f68 tptp.f69 (tptp.f8 tptp.f9 (tptp.f3 @t197 @t1))) @t295) tptp.f132))))))) % 56.22/56.45 (assume @p277 (forall @t203 (= (tptp.f3 (tptp.f34 (tptp.f134 tptp.f143 @t1) @t65) @t64) (tptp.f67 (tptp.f68 tptp.f69 @t179) @t201)))) % 56.22/56.45 (assume @p278 (forall @t210 (exists (@list @t566) (and (= @t566 @t567) (= (tptp.f75 (tptp.f76 tptp.f77 @t121) @t566) (tptp.f75 (tptp.f76 tptp.f77 @t151) @t566)))))) % 56.22/56.45 (assume @p279 (forall @t213 (exists (@list @t568) (and (= @t568 @t567) (= (tptp.f67 (tptp.f68 tptp.f69 @t115) @t568) (tptp.f67 (tptp.f68 tptp.f69 @t148) @t568)))))) % 56.22/56.45 (assume @p280 (forall @t216 (exists (@list @t569) (and (= @t569 @t567) (= (tptp.f139 (tptp.f140 tptp.f141 @t127) @t569) (tptp.f139 (tptp.f140 tptp.f141 @t154) @t569)))))) % 56.22/56.45 (assume @p281 (forall (@list @t570 @t70 @t335) (=> (forall @t574 (=> @t573 (= (tptp.f22 @t70 @t109) (tptp.f22 @t335 @t109)))) (= (tptp.f75 @t259 @t570) @t571)))) % 56.22/56.45 (assume @p282 @t582) % 56.22/56.45 (assume @p283 (forall (@list @t570 @t439 @t335 @t349) (=> @t586 (=> (forall @t585 (=> @t584 (= (tptp.f22 @t335 @t583) (tptp.f22 @t349 @t583)))) (= @t571 (tptp.f75 @t350 @t439)))))) % 56.22/56.45 (assume @p284 (forall (@list @t570 @t439 @t369 @t355) (=> @t586 (=> (forall @t585 (=> @t584 (= (tptp.f3 @t369 @t583) (tptp.f3 @t355 @t583)))) (= @t575 (tptp.f67 @t356 @t439)))))) % 56.22/56.45 (assume @p285 (forall @t271 (=> @t592 (= @t590 @t587)))) % 56.22/56.45 (assume @p286 (forall @t268 (=> @t596 (= @t595 @t593)))) % 56.22/56.45 (assume @p287 (forall @t271 (=> @t592 (= @t601 @t598)))) % 56.22/56.45 (assume @p288 (forall @t268 (=> @t596 (= @t605 @t603)))) % 56.22/56.45 (assume @p289 (forall @t213 (=> @t592 (= (tptp.f3 (tptp.f8 tptp.f9 @t600) @t64) (tptp.f5 (tptp.f6 tptp.f59 @t461) @t462))))) % 56.22/56.45 (assume @p290 (forall @t210 (=> @t596 (= (tptp.f22 (tptp.f24 tptp.f25 @t604) @t64) (/ @t459 @t460))))) % 56.22/56.45 (assume @p291 (forall @t456 (exists (@list @t608 @t607 @t606) (and (= @t608 @t88) (= @t607 @t44) (= @t606 @t116) (=> @t592 (=> (<= @t607 @t608) (= (tptp.f3 @t606 (tptp.f11 tptp.f12 (- @t608 @t607))) (tptp.f5 (tptp.f6 tptp.f59 (tptp.f3 @t606 @t64)) (tptp.f3 @t606 @t31))))))))) % 56.22/56.45 (assume @p292 (forall @t454 (exists (@list @t611 @t610 @t609) (and (= @t611 @t88) (= @t610 @t44) (= @t609 @t122) (=> @t596 (=> (<= @t610 @t611) (= (tptp.f22 @t609 (tptp.f11 tptp.f12 (- @t611 @t610))) (/ (tptp.f22 @t609 @t64) (tptp.f22 @t609 @t31))))))))) % 56.22/56.45 (assume @p293 (forall @t271 (=> @t592 (=> @t598 @t601)))) % 56.22/56.45 (assume @p294 (forall @t268 (=> @t596 (=> @t603 @t605)))) % 56.22/56.45 (assume @p295 (forall @t271 (=> @t592 (=> @t587 @t590)))) % 56.22/56.45 (assume @p296 (forall @t268 (=> @t596 (=> @t593 @t595)))) % 56.22/56.45 (assume @p297 (forall @t268 (= (/ @t614 @t173) (- @t613 @t612)))) % 56.22/56.45 (assume @p298 (forall @t271 (= (tptp.f5 (tptp.f6 tptp.f59 @t619) @t170) (tptp.f5 (tptp.f6 tptp.f51 @t617) @t615)))) % 56.22/56.45 (assume @p299 (forall @t420 (= (tptp.f5 @t616 tptp.f132) tptp.f132))) % 56.22/56.45 (assume @p300 (forall @t419 (exists (@list @t620) (and (= @t620 0/1) (= (/ @t37 @t620) @t620))))) % 56.22/56.45 (assume @p301 (forall @t420 (= (tptp.f5 (tptp.f6 tptp.f59 tptp.f132) @t95) tptp.f132))) % 56.22/56.45 (assume @p302 (forall @t419 (exists (@list @t621) (and (= @t621 0/1) (= (/ @t621 @t37) @t621))))) % 56.22/56.45 (assume @p303 (forall @t419 (exists (@list @t622) (and (= @t622 0/1) (= (/ @t622 @t37) @t622))))) % 56.22/56.45 (assume @p304 (forall @t268 (= (* @t37 @t612) (/ @t38 @t173)))) % 56.22/56.45 (assume @p305 (forall @t271 (exists (@list @t623) (and (= @t623 @t96) (= (tptp.f5 @t623 @t615) (tptp.f5 (tptp.f6 tptp.f59 (tptp.f5 @t623 @t77)) @t170)))))) % 56.22/56.45 (assume @p306 (forall @t268 (= (/ @t119 @t173) (+ @t613 @t612)))) % 56.22/56.45 (assume @p307 (forall @t271 (= (tptp.f5 (tptp.f6 tptp.f59 @t113) @t170) (tptp.f5 (tptp.f6 tptp.f55 @t617) @t615)))) % 56.22/56.45 (assume @p308 (forall @t268 (= (* @t614 @t173) (- @t315 @t314)))) % 56.22/56.45 (assume @p309 (forall @t271 (= (tptp.f5 @t624 @t170) (tptp.f5 (tptp.f6 tptp.f51 @t317) @t316)))) % 56.22/56.45 (assume @p310 (forall @t268 (= (* @t37 (- @t36 @t173)) (- @t38 @t315)))) % 56.22/56.45 (assume @p311 (forall @t271 (exists (@list @t625) (and (= @t625 @t96) (= (tptp.f5 @t625 @t627) (tptp.f5 (tptp.f6 tptp.f51 (tptp.f5 @t625 @t77)) (tptp.f5 @t625 @t170))))))) % 56.22/56.45 (assume @p312 (forall @t271 (exists (@list @t628) (and (= @t628 @t96) (= (tptp.f5 @t628 @t627) (tptp.f5 (tptp.f6 tptp.f51 (tptp.f5 @t628 @t77)) (tptp.f5 @t628 @t170))))))) % 56.22/56.45 (assume @p313 (forall @t210 (= (tptp.f22 (tptp.f24 tptp.f25 @t629) @t64) (/ @t460 @t459)))) % 56.22/56.45 (assume @p314 (forall @t213 (= (tptp.f3 (tptp.f8 tptp.f9 @t630) @t64) (tptp.f5 (tptp.f6 tptp.f59 @t462) @t461)))) % 56.22/56.45 (assume @p315 (forall @t420 (= (tptp.f5 @t96 tptp.f132) tptp.f132))) % 56.22/56.45 (assume @p316 (forall @t419 (exists (@list @t631) (and (= @t631 0/1) (= (* @t37 @t631) @t631))))) % 56.22/56.45 (assume @p317 (forall @t419 (exists (@list @t632) (and (= @t632 0/1) (= (* @t37 @t632) @t632))))) % 56.22/56.45 (assume @p318 (forall @t419 (exists (@list @t633) (and (= @t633 0/1) (= (* @t37 @t633) @t633))))) % 56.22/56.45 (assume @p319 (forall @t475 (= (* @t41 0) 0))) % 56.22/56.45 (assume @p320 (forall @t420 (= (tptp.f5 (tptp.f6 tptp.f7 tptp.f132) @t95) tptp.f132))) % 56.22/56.45 (assume @p321 (forall @t419 (exists (@list @t634) (and (= @t634 0/1) (= (* @t634 @t37) @t634))))) % 56.22/56.45 (assume @p322 (forall @t419 (exists (@list @t635) (and (= @t635 0/1) (= (* @t635 @t37) @t635))))) % 56.22/56.45 (assume @p323 (forall @t419 (exists (@list @t636) (and (= @t636 0/1) (= (* @t636 @t37) @t636))))) % 56.22/56.45 (assume @p324 (forall @t475 (= (* 0 @t41) 0))) % 56.22/56.45 (assume @p325 (forall @t264 (=> @t639 @t638))) % 56.22/56.45 (assume @p326 (forall @t39 (exists (@list @t640) (and (= @t640 0/1) (=> (= @t38 @t640) (or (= @t37 @t640) (= @t36 @t640))))))) % 56.22/56.45 (assume @p327 (forall @t43 (=> @t644 @t643))) % 56.22/56.45 (assume @p328 (forall @t264 (=> @t592 (=> @t645 (not @t639))))) % 56.22/56.45 (assume @p329 (forall @t39 (exists (@list @t646) (and (= @t646 0/1) (=> (not (= @t37 @t646)) (=> (not (= @t36 @t646)) (not (= @t38 @t646)))))))) % 56.22/56.45 (assume @p330 (forall @t43 (=> @t647 (=> (not @t641) (not @t644))))) % 56.22/56.45 (assume @p331 (forall @t264 (= @t639 @t638))) % 56.22/56.45 (assume @p332 (forall @t39 (exists (@list @t648) (and (= @t648 0/1) (= (= @t38 @t648) (or (= @t37 @t648) (= @t36 @t648))))))) % 56.22/56.45 (assume @p333 (forall @t43 (= @t644 @t643))) % 56.22/56.45 (assume @p334 (forall @t419 (exists (@list @t649) (and (= @t649 0/1) (= (* @t37 @t649) @t649))))) % 56.22/56.45 (assume @p335 (forall @t419 (exists (@list @t650) (and (= @t650 0/1) (= (* @t650 @t37) @t650))))) % 56.22/56.45 (assume @p336 (forall @t419 (= (+ 0/1 @t37) @t37))) % 56.22/56.45 (assume @p337 (forall @t420 (= (tptp.f5 (tptp.f6 tptp.f55 tptp.f132) @t95) @t95))) % 56.22/56.45 (assume @p338 (forall @t475 (= (+ 0 @t41) @t41))) % 56.22/56.45 (assume @p339 (forall @t419 (= (+ @t37 0/1) @t37))) % 56.22/56.45 (assume @p340 (forall @t420 (= (tptp.f5 @t112 tptp.f132) @t95))) % 56.22/56.45 (assume @p341 (forall @t475 (= (+ @t41 0) @t41))) % 56.22/56.45 (assume @p342 (forall @t39 (= (= @t37 @t119) (= @t36 0/1)))) % 56.22/56.45 (assume @p343 (forall @t264 (= (= @t95 @t113) @t637))) % 56.22/56.45 (assume @p344 (forall @t43 (= (= @t41 @t125) @t641))) % 56.22/56.45 (assume @p345 (forall @t420 (= (= @t477 tptp.f132) @t591))) % 56.22/56.45 (assume @p346 (forall @t419 (exists (@list @t651) (and (= @t651 0/1) (= (= @t422 @t651) (= @t37 @t651)))))) % 56.22/56.45 (assume @p347 (forall @t475 (= (= @t478 0) @t642))) % 56.22/56.45 (assume @p348 (= (tptp.f3 @t652 @t225) tptp.f132)) % 56.22/56.45 (assume @p349 (exists (@list @t653) (and (= @t653 0/1) (= (tptp.f22 (tptp.f24 tptp.f25 @t653) @t225) @t653)))) % 56.22/56.45 (assume @p350 (= (tptp.f13 @t654 @t225) 0)) % 56.22/56.45 (assume @p351 (= (tptp.f44 @t655 @t225) tptp.f145)) % 56.22/56.45 (assume @p352 (forall @t231 (=> @t592 (not @t656)))) % 56.22/56.45 (assume @p353 (forall @t229 (exists (@list @t657) (and (= @t657 0/1) (=> (not (= @t37 @t657)) (not (= @t508 @t657))))))) % 56.22/56.45 (assume @p354 (forall @t233 (=> @t647 (not @t658)))) % 56.22/56.45 (assume @p355 (forall @t231 (= @t656 (and @t591 @t330)))) % 56.22/56.45 (assume @p356 (forall @t229 (exists (@list @t659) (and (= @t659 0/1) (= (= @t508 @t659) (and (= @t37 @t659) @t330)))))) % 56.22/56.45 (assume @p357 (forall @t233 (= @t658 (and @t642 @t330)))) % 56.22/56.45 (assume @p358 (forall @t62 (= (= @t506 tptp.f145) (and (= @t1 tptp.f145) @t330)))) % 56.22/56.45 (assume @p359 (forall @t18 (= (tptp.f3 @t652 @t30) tptp.f132))) % 56.22/56.45 (assume @p360 (forall @t18 (exists (@list @t660) (and (= @t660 0/1) (= (tptp.f22 (tptp.f24 tptp.f25 @t660) @t30) @t660))))) % 56.22/56.45 (assume @p361 (forall @t18 (= (tptp.f13 @t654 @t30) 0))) % 56.22/56.45 (assume @p362 (forall @t18 (= (tptp.f44 @t655 @t30) tptp.f145))) % 56.22/56.45 (assume @p363 (forall @t491 (= (/ @t490 @t173) (tptp.f75 (tptp.f76 tptp.f77 (tptp.f24 @t80 @t173)) @t439)))) % 56.22/56.45 (assume @p364 (forall @t493 (= (tptp.f5 (tptp.f6 tptp.f59 @t492) @t170) (tptp.f67 (tptp.f68 tptp.f69 (tptp.f8 @t78 @t170)) @t439)))) % 56.22/56.45 (assume @p365 (forall @t342 (= (tptp.f75 (tptp.f76 tptp.f77 @t73) @t258) (- @t341 @t260)))) % 56.22/56.45 (assume @p366 (forall @t344 (= (tptp.f67 (tptp.f68 tptp.f69 @t68) @t258) (tptp.f5 (tptp.f6 tptp.f51 @t343) @t262)))) % 56.22/56.45 (assume @p367 (forall @t18 (not (= @t131 tptp.f132)))) % 56.22/56.45 (assume @p368 (forall @t661 (= (tptp.f75 (tptp.f76 tptp.f77 tptp.f133) @t570) 0/1))) % 56.22/56.45 (assume @p369 (forall @t661 (= (tptp.f67 (tptp.f68 tptp.f69 tptp.f131) @t570) tptp.f132))) % 56.22/56.45 (assume @p370 (forall @t284 (exists (@list @t663 @t662) (and (= @t663 @t666) (= @t662 @t665) (= @t664 (+ (+ (* @t663 @t662) (* @t663 @t282)) (* @t173 @t662))))))) % 56.22/56.45 (assume @p371 (forall @t289 (exists (@list @t668 @t669 @t667) (and (= @t668 @t304) (= @t669 @t673) (= @t667 @t671) (= (tptp.f5 @t670 (tptp.f5 @t668 @t285)) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t669 @t667)) (tptp.f5 @t669 @t285))) (tptp.f5 @t668 @t667))))))) % 56.22/56.45 (assume @p372 (forall @t284 (= @t664 (+ (* @t37 @t665) (* @t666 @t282))))) % 56.22/56.45 (assume @p373 (forall @t289 (exists (@list @t674) (and (= @t674 @t96) (= (tptp.f5 (tptp.f6 tptp.f51 (tptp.f5 @t674 @t77)) @t389) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t674 @t671)) (tptp.f5 @t673 @t285))))))) % 56.22/56.45 (assume @p374 (forall @t292 (= (- @t42 @t307) (+ (* @t41 @t676) (* @t675 @t290))))) % 56.22/56.45 (assume @p375 (forall @t679 (= @t678 (= @t173 (+ (* (- @t282 @t37) @t36) @t677))))) % 56.22/56.45 (assume @p376 (forall @t683 (= @t682 (= @t170 (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 (tptp.f6 tptp.f7 (tptp.f5 (tptp.f6 tptp.f51 @t285) @t95)) @t77)) @t680))))) % 56.22/56.45 (assume @p377 (forall @t686 (= @t685 (= @t176 (+ (* (- @t290 @t41) @t40) @t684))))) % 56.22/56.45 (assume @p378 (forall @t679 (= @t678 (= (+ (* (- @t37 @t282) @t36) @t173) @t677)))) % 56.22/56.45 (assume @p379 (forall @t683 (= @t682 (= (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 (tptp.f6 tptp.f7 (tptp.f5 @t618 @t285)) @t77)) @t170) @t680)))) % 56.22/56.45 (assume @p380 (forall @t686 (= @t685 (= (+ (* (- @t41 @t290) @t40) @t176) @t684)))) % 56.22/56.45 (assume @p381 (forall @t363 (exists (@list @t689 @t687 @t688) (and (= @t689 @t44) (= @t687 @t362) (= @t688 @t348) (=> (<= @t2 @t689) (=> (<= @t689 @t88) (= (- (tptp.f139 @t687 (tptp.f70 @t688 @t64)) (tptp.f139 @t687 (tptp.f70 @t688 @t31))) (tptp.f139 @t687 @t251)))))))) % 56.22/56.45 (assume @p382 (forall @t351 (exists (@list @t692 @t690 @t691) (and (= @t692 @t44) (= @t690 @t350) (= @t691 @t348) (=> (<= @t2 @t692) (=> (<= @t692 @t88) (= (- (tptp.f75 @t690 (tptp.f70 @t691 @t64)) (tptp.f75 @t690 (tptp.f70 @t691 @t31))) (tptp.f75 @t690 @t251)))))))) % 56.22/56.45 (assume @p383 (forall @t357 (exists (@list @t695 @t693 @t694) (and (= @t695 @t44) (= @t693 @t356) (= @t694 @t348) (=> (<= @t2 @t695) (=> (<= @t695 @t88) (= (tptp.f5 (tptp.f6 tptp.f51 (tptp.f67 @t693 (tptp.f70 @t694 @t64))) (tptp.f67 @t693 (tptp.f70 @t694 @t31))) (tptp.f67 @t693 @t251)))))))) % 56.22/56.45 (assume @p384 (forall @t39 (exists (@list @t696) (and (= @t696 0/1) (= (= (+ @t472 (* @t36 @t36)) @t696) (and (= @t37 @t696) (= @t36 @t696))))))) % 56.22/56.45 (assume @p385 (forall @t43 (= (= (+ @t474 (* @t40 @t40)) 0) @t697))) % 56.22/56.45 (assume @p386 (forall @t679 (=> @t596 (=> (and (= @t36 @t173) (not (= @t282 @t677))) (not (= (+ @t36 @t300) (+ @t173 (* @t37 @t677)))))))) % 56.22/56.45 (assume @p387 (forall @t683 (exists (@list @t698) (and (= @t698 @t96) (=> @t592 (=> (and (= @t77 @t170) (not (= @t285 @t680))) (not (= (tptp.f5 @t263 (tptp.f5 @t698 @t285)) (tptp.f5 @t287 (tptp.f5 @t698 @t680)))))))))) % 56.22/56.45 (assume @p388 (forall @t686 (=> @t647 (=> (and (= @t40 @t176) (not (= @t290 @t684))) (not (= (+ @t40 @t306) (+ @t176 (* @t41 @t684)))))))) % 56.22/56.45 (assume @p389 (forall @t39 (exists (@list @t699 @t700) (and (= @t699 0/1) (= @t700 @t225) (= (= (+ (tptp.f22 @t122 @t700) (tptp.f22 @t138 @t700)) @t699) (and (= @t37 @t699) (= @t36 @t699))))))) % 56.22/56.45 (assume @p390 (forall @t43 (exists (@list @t701) (and (= @t701 @t225) (= (= (+ (tptp.f13 @t128 @t701) (tptp.f13 @t144 @t701)) 0) @t697))))) % 56.22/56.45 (assume @p391 (forall @t49 (exists (@list @t702 @t703) (and (= @t702 @t185) (= @t703 @t86) (=> (= (tptp.f3 @t47 @t702) tptp.f132) (= (tptp.f67 @t703 @t298) (tptp.f67 @t703 (tptp.f70 (tptp.f71 @t702) @t31)))))))) % 56.22/56.45 (assume @p392 (forall @t35 (exists (@list @t704 @t705) (and (= @t704 @t185) (= @t705 @t92) (=> (= (tptp.f22 @t32 @t704) 0/1) (= (tptp.f75 @t705 @t298) (tptp.f75 @t705 (tptp.f70 (tptp.f71 @t704) @t31)))))))) % 56.22/56.45 (assume @p393 (forall @t53 (exists (@list @t706 @t707) (and (= @t706 @t185) (= @t707 @t381) (=> (= (tptp.f13 @t51 @t706) 0) (= (tptp.f139 @t707 @t298) (tptp.f139 @t707 (tptp.f70 (tptp.f71 @t706) @t31)))))))) % 56.22/56.45 (assume @p394 (forall @t106 (exists (@list @t708 @t709) (and (= @t708 @t186) (= @t709 @t381) (= (tptp.f139 (tptp.f140 tptp.f141 @t105) (tptp.f70 @t708 @t64)) (- (tptp.f139 @t709 (tptp.f70 @t708 @t99)) (tptp.f139 @t709 (tptp.f70 @t708 @t31)))))))) % 56.22/56.45 (assume @p395 (forall @t94 (exists (@list @t710 @t711) (and (= @t710 @t186) (= @t711 @t92) (= (tptp.f75 (tptp.f76 tptp.f77 @t103) (tptp.f70 @t710 @t64)) (- (tptp.f75 @t711 (tptp.f70 @t710 @t99)) (tptp.f75 @t711 (tptp.f70 @t710 @t31)))))))) % 56.22/56.45 (assume @p396 (forall @t89 (exists (@list @t712 @t713) (and (= @t712 @t186) (= @t713 @t86) (= (tptp.f67 (tptp.f68 tptp.f69 @t101) (tptp.f70 @t712 @t64)) (tptp.f5 (tptp.f6 tptp.f51 (tptp.f67 @t713 (tptp.f70 @t712 @t99))) (tptp.f67 @t713 (tptp.f70 @t712 @t31)))))))) % 56.22/56.45 (assume @p397 (forall @t39 (exists (@list @t714) (and (= @t714 @t715) (= (- (tptp.f22 @t122 @t714) (tptp.f22 @t138 @t714)) (* @t614 @t119)))))) % 56.22/56.45 (assume @p398 (forall @t264 (exists (@list @t716) (and (= @t716 @t715) (= (tptp.f5 (tptp.f6 tptp.f51 (tptp.f3 @t116 @t716)) (tptp.f3 @t136 @t716)) (tptp.f5 @t624 @t113)))))) % 56.22/56.45 (assume @p399 (forall @t43 (exists (@list @t717) (and (= @t717 @t715) (= (- (tptp.f13 @t128 @t717) (tptp.f13 @t144 @t717)) (* (- @t41 @t40) @t125)))))) % 56.22/56.45 (assume @p400 (forall @t94 (exists (@list @t719 @t718 @t720) (and (= @t719 @t92) (= @t718 @t250) (= @t720 @t88) (=> @t722 (= @t721 0/1)) (=> (not @t722) (= @t721 (+ (tptp.f75 @t719 (tptp.f70 @t718 @t64)) @t72))))))) % 56.22/56.45 (assume @p401 (forall @t89 (exists (@list @t724 @t723 @t725) (and (= @t724 @t86) (= @t723 @t250) (= @t725 @t88) (=> @t727 (= @t726 tptp.f132)) (=> (not @t727) (= @t726 (tptp.f5 (tptp.f6 tptp.f55 (tptp.f67 @t724 (tptp.f70 @t723 @t64))) @t67))))))) % 56.22/56.45 (assume @p402 (forall @t106 (exists (@list @t729 @t728 @t730) (and (= @t729 @t381) (= @t728 @t250) (= @t730 @t88) (=> @t732 (= @t731 0)) (=> (not @t732) (= @t731 (+ (tptp.f139 @t729 (tptp.f70 @t728 @t64)) (tptp.f13 @t51 @t64)))))))) % 56.22/56.45 (assume @p403 (forall (@list @t37 @t31 @t173) (exists (@list @t733) (and (= @t733 @t58) (= (- (tptp.f22 @t122 @t733) (tptp.f22 @t174 @t733)) (* @t666 (tptp.f75 (tptp.f76 tptp.f77 @t175) (tptp.f70 @t186 @t733)))))))) % 56.22/56.45 (assume @p404 (forall (@list @t95 @t31 @t170) (exists (@list @t734) (and (= @t734 @t58) (= (tptp.f5 (tptp.f6 tptp.f51 (tptp.f3 @t116 @t734)) (tptp.f3 @t171 @t734)) (tptp.f5 @t673 (tptp.f67 (tptp.f68 tptp.f69 @t172) (tptp.f70 @t186 @t734)))))))) % 56.22/56.45 (assume @p405 (forall (@list @t41 @t31 @t176) (exists (@list @t735) (and (= @t735 @t58) (= (- (tptp.f13 @t128 @t735) (tptp.f13 @t177 @t735)) (* @t675 (tptp.f139 (tptp.f140 tptp.f141 @t178) (tptp.f70 @t186 @t735)))))))) % 56.22/56.45 (assume @p406 (forall @t679 (= (/ @t664 @t677) (+ (* @t37 (/ @t665 @t677)) (* (/ @t666 @t677) @t282))))) % 56.22/56.45 (assume @p407 (forall @t683 (exists (@list @t736) (and (= @t736 @t96) (= (tptp.f5 (tptp.f6 tptp.f59 (tptp.f5 (tptp.f6 tptp.f51 (tptp.f5 @t736 @t77)) @t389)) @t680) (tptp.f5 (tptp.f6 tptp.f55 (tptp.f5 @t736 (tptp.f5 (tptp.f6 tptp.f59 @t671) @t680))) (tptp.f5 (tptp.f6 tptp.f7 (tptp.f5 (tptp.f6 tptp.f59 @t672) @t680)) @t285))))))) % 56.22/56.45 (assume @p408 (forall @t289 (=> @t592 (=> @t645 (= (tptp.f5 (tptp.f6 tptp.f51 @t589) @t738) (tptp.f5 (tptp.f6 tptp.f59 (tptp.f5 (tptp.f6 tptp.f51 @t310) @t737)) @t311)))))) % 56.22/56.45 (assume @p409 (forall @t284 (exists (@list @t741) (and (= @t741 0/1) (=> (not (= @t37 @t741)) (=> (not (= @t36 @t741)) (= (- @t594 @t740) (/ (- @t299 @t739) @t38)))))))) % 56.22/56.45 (assume @p410 (forall @t271 (=> @t592 (= (tptp.f5 (tptp.f6 tptp.f51 @t600) @t170) (tptp.f5 (tptp.f6 tptp.f59 (tptp.f5 @t626 @t317)) @t95))))) % 56.22/56.45 (assume @p411 (forall @t268 (=> @t596 (= (- @t604 @t173) (/ (- @t36 @t315) @t37))))) % 56.22/56.45 (assume @p412 (forall @t271 (=> @t592 (= (tptp.f5 @t626 @t589) (tptp.f5 (tptp.f6 tptp.f59 (tptp.f5 @t670 @t170)) @t95))))) % 56.22/56.45 (assume @p413 (forall @t268 (=> @t596 (= (- @t36 @t594) (/ (- @t38 @t173) @t37))))) % 56.22/56.45 (assume @p414 (forall @t284 (exists (@list @t742) (and (= @t742 0/1) (=> (not (= @t37 @t742)) (=> (not (= @t36 @t742)) (= (+ @t594 @t740) (/ (+ @t299 @t739) @t38)))))))) % 56.22/56.45 (assume @p415 (forall @t289 (=> @t592 (=> @t645 (= (tptp.f5 (tptp.f6 tptp.f55 @t589) @t738) (tptp.f5 (tptp.f6 tptp.f59 (tptp.f5 @t525 @t737)) @t311)))))) % 56.22/56.45 (assume @p416 (forall @t39 (= (tptp.f28 tptp.f48 @t629) (/ @t417 @t561)))) % 56.22/56.45 (assume @p417 (forall @t284 (= (- @t119 @t283) (+ @t666 @t665)))) % 56.22/56.45 (assume @p418 (forall @t289 (= (tptp.f5 (tptp.f6 tptp.f51 @t113) @t288) (tptp.f5 (tptp.f6 tptp.f55 @t672) @t671)))) % 56.22/56.45 (assume @p419 (forall @t292 (= (- @t125 @t291) (+ @t675 @t676)))) % 56.22/56.45 (assume @p420 (forall @t39 (=> @t596 (= (tptp.f28 tptp.f48 @t604) (/ @t561 @t417))))) % 56.22/56.45 (assume @p421 (forall @t284 (= (* @t629 (/ @t173 @t282)) (/ @t315 @t320)))) % 56.22/56.45 (assume @p422 (forall @t289 (= (tptp.f5 (tptp.f6 tptp.f7 @t630) (tptp.f5 @t588 @t285)) (tptp.f5 (tptp.f6 tptp.f59 @t317) @t387)))) % 56.22/56.45 (assume @p423 (forall @t271 (= (= @t95 @t615) (and (=> @t744 (= @t317 @t77)) (=> (not @t744) @t591))))) % 56.22/56.45 (assume @p424 (forall @t268 (exists (@list @t745) (and (= @t745 0/1) (= (= @t37 @t612) (and (=> @t746 (= @t315 @t36)) (=> (not @t746) (= @t37 @t745)))))))) % 56.22/56.45 (assume @p425 (forall @t271 (= (= @t630 @t170) (and (=> @t645 (= @t95 @t310)) (=> (not @t645) @t743))))) % 56.22/56.45 (assume @p426 (forall @t268 (exists (@list @t747) (and (= @t747 0/1) (= (= @t629 @t173) (and (=> @t748 (= @t37 @t299)) (=> (not @t748) (= @t173 @t747)))))))) % 56.22/56.45 (assume @p427 (forall @t271 (=> @t592 (= (tptp.f5 (tptp.f6 tptp.f59 @t415) @t597) @t615)))) % 56.22/56.45 (assume @p428 (forall @t268 (=> @t596 (= (/ @t414 @t602) @t612)))) % 56.22/56.45 (assume @p429 (forall @t271 (exists (@list @t749) (and (= @t749 @t96) (=> @t592 (= (tptp.f5 (tptp.f6 tptp.f59 (tptp.f5 @t749 @t77)) (tptp.f5 @t749 @t170)) @t615)))))) % 56.22/56.45 (assume @p430 (forall @t268 (=> @t596 (= (/ @t38 @t315) @t612)))) % 56.22/56.45 (assume @p431 (forall @t62 (exists (@list @t750) (and (= @t750 @t2) (=> (< 0 @t750) (=> (< @t750 @t44) (= (tptp.f67 (tptp.f68 tptp.f69 (tptp.f8 tptp.f9 (tptp.f3 (tptp.f8 tptp.f9 (tptp.f5 (tptp.f6 tptp.f59 tptp.f146) @t196)) @t1))) @t295) tptp.f132))))))) % 56.22/56.45 (assume @p432 (= (tptp.f3 tptp.f10 @t331) tptp.f146)) % 56.22/56.45 (assume @p433 (= (tptp.f3 tptp.f10 @t185) tptp.f146)) % 56.22/56.45 (assume @p434 (forall @t18 (= (tptp.f3 @t132 @t1) tptp.f146))) % 56.22/56.45 (assume @p435 (forall @t18 (exists (@list @t751) (and (= @t751 @t2) (<= @t751 (* @t751 @t751)))))) % 56.22/56.45 (assume @p436 (forall @t18 (exists (@list @t752) (and (= @t752 @t2) (<= @t752 (* @t752 (* @t752 @t752))))))) % 56.22/56.45 (assume @p437 (forall @t18 (= (tptp.f11 tptp.f12 (* 0 @t2)) @t185))) % 56.22/56.45 (assume @p438 (forall @t18 (= (tptp.f11 tptp.f12 (* 1 @t2)) @t1))) % 56.22/56.45 (assume @p439 (forall @t62 (exists (@list @t754 @t753) (and (= @t754 @t2) (= @t753 @t44) (= (< 0 (* @t754 @t753)) (and (< 0 @t754) (< 0 @t753))))))) % 56.22/56.45 (assume @p440 (forall @t62 (exists (@list @t755) (and (= @t755 @t331) (= (= @t755 @t61) (and (= @t1 @t755) (= @t31 @t755))))))) % 56.22/56.45 (assume @p441 (forall @t18 (= (tptp.f11 tptp.f12 (* @t2 0)) @t185))) % 56.22/56.45 (assume @p442 (forall @t18 (= (tptp.f11 tptp.f12 (* @t2 1)) @t1))) % 56.22/56.45 (assume @p443 (forall @t62 (exists (@list @t756 @t757) (and (= @t756 @t2) (= @t757 @t44) (= (tptp.f11 tptp.f12 (* @t756 @t757)) (tptp.f11 tptp.f12 (* @t757 @t756))))))) % 56.22/56.45 (assume @p444 (forall @t62 (exists (@list @t759 @t758) (and (= @t759 @t2) (= @t758 @t44) (= (tptp.f11 tptp.f12 (* @t759 (+ @t758 1))) (tptp.f11 tptp.f12 (+ @t759 (* @t759 @t758)))))))) % 56.22/56.45 (assume @p445 (forall @t195 (exists (@list @t761 @t762 @t760) (and (= @t761 @t2) (= @t762 @t44) (= @t760 @t88) (= (tptp.f11 tptp.f12 (* @t761 (+ @t762 @t760))) (tptp.f11 tptp.f12 (+ (* @t761 @t762) (* @t761 @t760)))))))) % 56.22/56.45 (assume @p446 (forall @t195 (exists (@list @t764 @t763 @t765) (and (= @t764 @t2) (= @t763 @t88) (= @t765 @t44) (= (tptp.f11 tptp.f12 (* @t764 (tptp.f13 tptp.f14 (tptp.f11 tptp.f12 (- @t765 @t763))))) (tptp.f11 tptp.f12 (- (* @t764 @t765) (* @t764 @t763)))))))) % 56.22/56.45 (assume @p447 (forall @t62 (exists (@list @t767 @t768 @t766) (and (= @t767 @t296) (= @t768 @t2) (= @t766 @t44) (= (<= @t767 (* @t768 @t766)) (and (<= @t767 @t768) (<= @t767 @t766))))))) % 56.22/56.45 (assume @p448 (forall @t62 (exists (@list @t770 @t769) (and (= @t770 @t2) (= @t769 @t44) (= (tptp.f11 tptp.f12 (* (+ @t770 1) @t769)) (tptp.f11 tptp.f12 (+ @t769 (* @t770 @t769)))))))) % 56.22/56.45 (assume @p449 (forall @t62 (exists (@list @t771) (and (= @t771 @t331) (= (= @t61 @t771) (and (= @t1 @t771) (= @t31 @t771))))))) % 56.22/56.45 (assume @p450 (forall @t62 (exists (@list @t772) (and (= @t772 @t185) (= (= @t61 @t772) (or (= @t1 @t772) (= @t31 @t772))))))) % 56.22/56.45 (assume @p451 (forall @t195 (exists (@list @t775 @t774 @t773) (and (= @t775 @t2) (= @t774 @t44) (= @t773 @t88) (= (tptp.f11 tptp.f12 (* (* @t775 @t774) @t773)) (tptp.f11 tptp.f12 (* @t775 (* @t774 @t773)))))))) % 56.22/56.45 (assume @p452 (forall @t195 (exists (@list @t778 @t777 @t776) (and (= @t778 @t2) (= @t777 @t44) (= @t776 @t88) (= (tptp.f11 tptp.f12 (* (+ @t778 @t777) @t776)) (tptp.f11 tptp.f12 (+ (* @t778 @t776) (* @t777 @t776)))))))) % 56.22/56.45 (assume @p453 (forall @t195 (exists (@list @t780 @t781 @t779) (and (= @t780 @t44) (= @t781 @t2) (= @t779 @t88) (= (tptp.f11 tptp.f12 (* (tptp.f13 tptp.f14 (tptp.f11 tptp.f12 (- @t781 @t780))) @t779)) (tptp.f11 tptp.f12 (- (* @t781 @t779) (* @t780 @t779)))))))) % 56.22/56.45 (assume @p454 (forall @t62 (exists (@list @t782) (and (= @t782 @t297) (= (= @t61 @t782) (and (= @t1 @t782) (= @t31 @t782))))))) % 56.22/56.45 (assume @p455 (forall @t195 (exists (@list @t785 @t783 @t784) (and (= @t785 @t2) (= @t783 @t88) (= @t784 @t44) (= (< (* @t785 @t784) (* @t785 @t783)) (and (< 0 @t785) (< @t784 @t783))))))) % 56.22/56.45 (assume @p456 (forall @t195 (exists (@list @t786 @t788 @t787) (and (= @t786 @t88) (= @t788 @t44) (= @t787 @t2) (= (< (* @t787 @t788) (* @t786 @t788)) (and (< 0 @t788) (< @t787 @t786))))))) % 56.22/56.45 (assume @p457 (forall @t195 (exists (@list @t791 @t789 @t790) (and (= @t791 @t2) (= @t789 @t88) (= @t790 @t44) (= (<= (* @t791 @t790) (* @t791 @t789)) (=> (< 0 @t791) (<= @t790 @t789))))))) % 56.22/56.45 (assume @p458 (forall @t195 (exists (@list @t792 @t794 @t793) (and (= @t792 @t88) (= @t794 @t44) (= @t793 @t2) (= (<= (* @t793 @t794) (* @t792 @t794)) (=> (< 0 @t794) (<= @t793 @t792))))))) % 56.22/56.45 (assume @p459 (forall @t195 (exists (@list @t797) (and (= @t797 @t2) (= (= (tptp.f11 tptp.f12 (* @t797 @t44)) (tptp.f11 tptp.f12 (* @t797 @t88))) (or @t796 @t795)))))) % 56.22/56.45 (assume @p460 (forall @t195 (exists (@list @t798) (and (= @t798 @t44) (= (= (tptp.f11 tptp.f12 (* @t2 @t798)) (tptp.f11 tptp.f12 (* @t88 @t798))) (or (= @t1 @t64) @t329)))))) % 56.22/56.45 (assume @p461 (forall @t195 (exists (@list @t799) (and (= @t799 @t29) (= (= (tptp.f11 tptp.f12 (* @t799 @t44)) (tptp.f11 tptp.f12 (* @t799 @t88))) @t796))))) % 56.22/56.45 (assume @p462 (forall @t195 (exists (@list @t802 @t800 @t801) (and (= @t802 @t29) (= @t800 @t88) (= @t801 @t44) (= (< (* @t802 @t801) (* @t802 @t800)) (< @t801 @t800)))))) % 56.22/56.45 (assume @p463 (forall @t195 (exists (@list @t805 @t803 @t804) (and (= @t805 @t29) (= @t803 @t88) (= @t804 @t44) (= (<= (* @t805 @t804) (* @t805 @t803)) (<= @t804 @t803)))))) % 56.22/56.45 (assume @p464 (forall @t195 (exists (@list @t807 @t808 @t806) (and (= @t807 @t44) (= @t808 @t2) (= @t806 @t88) (=> (<= @t808 @t807) (<= (* @t808 @t806) (* @t807 @t806))))))) % 56.22/56.45 (assume @p465 (forall @t195 (exists (@list @t809 @t811 @t810) (and (= @t809 @t44) (= @t811 @t2) (= @t810 @t88) (=> (<= @t811 @t809) (<= (* @t810 @t811) (* @t810 @t809))))))) % 56.22/56.45 (assume @p466 (forall @t195 (exists (@list @t813 @t814 @t812) (and (= @t813 @t44) (= @t814 @t2) (= @t812 @t88) (=> (< @t814 @t813) (=> (< 0 @t812) (< (* @t814 @t812) (* @t813 @t812)))))))) % 56.22/56.45 (assume @p467 (forall @t195 (exists (@list @t815 @t817 @t816) (and (= @t815 @t44) (= @t817 @t2) (= @t816 @t88) (=> (< @t817 @t815) (=> (< 0 @t816) (< (* @t816 @t817) (* @t816 @t815)))))))) % 56.22/56.45 (assume @p468 (forall @t143 (exists (@list @t819 @t821 @t818 @t820) (and (= @t819 @t44) (= @t821 @t2) (= @t818 @t110) (= @t820 @t88) (=> (<= @t821 @t819) (=> (<= @t820 @t818) (<= (* @t821 @t820) (* @t819 @t818)))))))) % 56.22/56.45 (assume @p469 (forall @t62 (=> (= @t1 @t61) (or (= @t31 @t331) @t795)))) % 56.22/56.45 (assume @p470 (forall @t62 (exists (@list @t824 @t822 @t823) (and (= @t824 @t296) (= @t822 @t2) (= @t823 @t44) (=> (< @t824 @t822) (=> (< @t824 @t823) (< @t822 (* @t823 @t822)))))))) % 56.22/56.45 (assume @p471 (forall @t62 (exists (@list @t827 @t826 @t825) (and (= @t827 @t296) (= @t826 @t2) (= @t825 @t44) (=> (< @t827 @t826) (=> (< @t827 @t825) (< @t826 (* @t826 @t825)))))))) % 56.22/56.45 (assume @p472 (forall @t62 (exists (@list @t830 @t828 @t829) (and (= @t830 @t296) (= @t828 @t2) (= @t829 @t44) (=> (< @t830 @t828) (=> (< @t830 @t829) (< @t830 (* @t829 @t828)))))))) % 56.22/56.45 (assume @p473 (forall @t18 (= (tptp.f11 tptp.f12 @t2) @t1))) % 56.22/56.45 (assume @p474 (forall @t475 (=> (<= 0 @t41) (= @t831 @t41)))) % 56.22/56.45 (assume @p475 (forall @t475 (=> (< @t41 0) (= @t831 0)))) % 56.22/56.45 (step @p476 :rule evaluate :args ((= false true))) % 56.22/56.45 (step @p477 :rule arith_poly_norm :args ((= @t4 (+ 1 @t3)))) % 56.22/56.45 (step @p478 :rule refl :args (tptp.f12)) % 56.22/56.45 (step @p479 :rule cong :premises (@p478 @p477) :args (@t5)) % 56.22/56.45 (step @p480 :rule refl :args (tptp.f17)) % 56.22/56.45 (step @p481 :rule cong :premises (@p480 @p479) :args (@t6)) % 56.22/56.45 (step @p482 :rule refl :args (@t14)) % 56.22/56.45 (step @p483 :rule cong :premises (@p482 @p481) :args (@t15)) % 56.22/56.45 (step @p484 :rule refl :args (@t16)) % 56.22/56.45 (step @p485 :rule cong :premises (@p484 @p483) :args (@t17)) % 56.22/56.45 (step @p486 :rule cong :premises (@p485) :args (@t19)) % 56.22/56.45 (step @p487 :rule eq_resolve :premises (@p2 @p486)) % 56.22/56.45 (step @p488 :rule instantiate :premises (@p487) :args (@t834)) % 56.22/56.45 (step @p489 :rule symm :premises (@p488)) % 56.22/56.45 (step @p490 :rule bool-double-not-elim :args (@t835)) % 56.22/56.45 (step @p491 :rule aci_norm :args ((= (or false @t836) @t836))) % 56.22/56.45 (step @p492 :rule refl :args (@t836)) % 56.22/56.45 (step @p493 :rule evaluate :args ((not true))) % 56.22/56.45 (step @p494 :rule eq-refl :args (@t96)) % 56.22/56.45 (step @p495 :rule cong :premises (@p494) :args (@t837)) % 56.22/56.45 (step @p496 :rule trans :premises (@p495 @p493)) % 56.22/56.45 (step @p497 :rule nary_cong :premises (@p496 @p492) :args (@t838)) % 56.22/56.45 (step @p498 :rule trans :premises (@p497 @p491)) % 56.22/56.45 (step @p499 :rule quant-var-elim-eq :args ((= (forall @t408 (or (not @t406) @t841 @t839)) @t838))) % 56.22/56.45 (step @p500 :rule refl :args (@t839)) % 56.22/56.45 (step @p501 :rule refl :args (@t841)) % 56.22/56.45 (step @p502 :rule eq-symm :args (@t96 @t404)) % 56.22/56.45 (step @p503 :rule cong :premises (@p502) :args (@t841)) % 56.22/56.45 (step @p504 :rule nary_cong :premises (@p503 @p501 @p500) :args (@t842)) % 56.22/56.45 (step @p505 :rule aci_norm :args ((= @t843 @t842))) % 56.22/56.45 (step @p506 :rule trans :premises (@p505 @p504)) % 56.22/56.45 (step @p507 :rule cong :premises (@p506) :args ((forall @t408 @t843))) % 56.22/56.45 (step @p508 :rule trans :premises (@p507 @p499)) % 56.22/56.45 (step @p509 :rule trans :premises (@p508 @p498)) % 56.22/56.45 (step @p510 :rule bool-and-de-morgan :args (@t840 @t405 true)) % 56.22/56.45 (step @p511 :rule cong :premises (@p510) :args (@t845)) % 56.22/56.45 (step @p512 :rule trans :premises (@p511 @p509)) % 56.22/56.45 (step @p513 :rule cong :premises (@p512) :args (@t846)) % 56.22/56.45 (step @p514 :rule trans :premises (@p513 @p490)) % 56.22/56.45 (step @p515 :rule exists-elim :args ((= (exists @t408 @t844) @t846))) % 56.22/56.45 (step @p516 :rule trans :premises (@p515 @p514)) % 56.22/56.45 (step @p517 :rule refl :args (@t405)) % 56.22/56.45 (step @p518 :rule eq-symm :args (@t404 @t96)) % 56.22/56.45 (step @p519 :rule nary_cong :premises (@p518 @p517) :args (@t407)) % 56.22/56.45 (step @p520 :rule cong :premises (@p519) :args (@t409)) % 56.22/56.45 (step @p521 :rule trans :premises (@p520 @p516)) % 56.22/56.45 (step @p522 :rule cong :premises (@p521) :args (@t410)) % 56.22/56.45 (step @p523 :rule eq_resolve :premises (@p166 @p522)) % 56.22/56.45 (step @p524 :rule instantiate :premises (@p523) :args ((@list @t12 (tptp.f3 @t7 @t833) (tptp.f3 tptp.f17 (tptp.f11 tptp.f12 (+ 1 (* 2 (tptp.f13 tptp.f14 @t833)))))))) % 56.22/56.45 (step @p525 :rule symm :premises (@p524)) % 56.22/56.45 (step @p526 :rule refl :args (@t23)) % 56.22/56.45 (step @p527 :rule cong :premises (@p526 @p481) :args (@t24)) % 56.22/56.45 (step @p528 :rule refl :args (@t13)) % 56.22/56.45 (step @p529 :rule cong :premises (@p528 @p527) :args (@t25)) % 56.22/56.45 (step @p530 :rule refl :args (@t26)) % 56.22/56.45 (step @p531 :rule cong :premises (@p530 @p529) :args (@t27)) % 56.22/56.45 (step @p532 :rule cong :premises (@p531) :args (@t28)) % 56.22/56.45 (step @p533 :rule eq_resolve :premises (@p6 @p532)) % 56.22/56.45 (step @p534 :rule instantiate :premises (@p533) :args (@t834)) % 56.22/56.45 (step @p535 :rule trans :premises (@p534 @p525 @p489)) % 56.22/56.45 (step @p536 :rule true_intro :premises (@p535)) % 56.22/56.45 (step @p537 :rule bool-impl-elim :args (@t848 @t576)) % 56.22/56.45 (step @p538 :rule cong :premises (@p537) :args ((forall @t581 (=> @t848 @t576)))) % 56.22/56.45 (step @p539 :rule refl :args (@t576)) % 56.22/56.45 (step @p540 :rule bool-impl-elim :args (@t847 @t577)) % 56.22/56.45 (step @p541 :rule cong :premises (@p540) :args ((forall @t574 (=> @t847 @t577)))) % 56.22/56.45 (step @p542 :rule refl :args (@t577)) % 56.22/56.45 (step @p543 :rule eq-symm :args (@t572 tptp.f1)) % 56.22/56.45 (step @p544 :rule cong :premises (@p543 @p542) :args (@t578)) % 56.22/56.45 (step @p545 :rule cong :premises (@p544) :args (@t579)) % 56.22/56.45 (step @p546 :rule trans :premises (@p545 @p541)) % 56.22/56.45 (step @p547 :rule cong :premises (@p546 @p539) :args (@t580)) % 56.22/56.45 (step @p548 :rule cong :premises (@p547) :args (@t582)) % 56.22/56.45 (step @p549 :rule trans :premises (@p548 @p538)) % 56.22/56.45 (step @p550 :rule eq_resolve :premises (@p282 @p549)) % 56.22/56.45 (step @p551 :rule eq-symm :args (@t849 @t850)) % 56.22/56.45 (step @p552 :rule refl :args (@t851)) % 56.22/56.45 (step @p553 :rule nary_cong :premises (@p552 @p551) :args (@t852)) % 56.22/56.45 (step @p554 :rule refl :args (@t853)) % 56.22/56.45 (step @p555 :rule cong :premises (@p554 @p553) :args ((=> @t853 @t852))) % 56.22/56.45 (assume-push @p596 @t853) % 56.22/56.45 (step @p557 :rule instantiate :premises (@p550) :args ((@list @t187 tptp.f21 tptp.f4))) % 56.22/56.45 (step-pop @p597 :rule scope :premises (@p557)) % 56.22/56.45 (step @p558 :rule process_scope :premises (@p597) :args (@t852)) % 56.22/56.45 (step @p560 :rule eq_resolve :premises (@p558 @p555)) % 56.22/56.45 (step @p561 :rule implies_elim :premises (@p560)) % 56.22/56.45 (step @p562 :rule chain_m_resolution :premises (@p561 @p550) :args (@t855 (@list false) (@list @t853))) % 56.22/56.45 (step @p563 :rule aci_norm :args ((= (or false @t854) @t854))) % 56.22/56.45 (step @p564 :rule refl :args (@t854)) % 56.22/56.45 (step @p565 :rule eq-refl :args (@t187)) % 56.22/56.45 (step @p566 :rule cong :premises (@p565) :args (@t856)) % 56.22/56.45 (step @p567 :rule trans :premises (@p566 @p493)) % 56.22/56.45 (step @p568 :rule nary_cong :premises (@p567 @p564) :args (@t857)) % 56.22/56.45 (step @p569 :rule trans :premises (@p568 @p563)) % 56.22/56.45 (step @p570 :rule quant-var-elim-eq :args ((= (forall @t190 @t859) @t857))) % 56.22/56.45 (step @p571 :rule aci_norm :args ((= @t860 @t859))) % 56.22/56.45 (step @p572 :rule cong :premises (@p571) :args ((forall @t190 @t860))) % 56.22/56.45 (step @p573 :rule trans :premises (@p572 @p570)) % 56.22/56.45 (step @p574 :rule trans :premises (@p573 @p569)) % 56.22/56.45 (step @p575 :rule bool-double-not-elim :args (@t183)) % 56.22/56.45 (step @p576 :rule refl :args (@t858)) % 56.22/56.45 (step @p577 :rule nary_cong :premises (@p576 @p575) :args ((or @t858 (not @t184)))) % 56.22/56.45 (step @p578 :rule bool-and-de-morgan :args (@t188 @t184 true)) % 56.22/56.45 (step @p579 :rule trans :premises (@p578 @p577)) % 56.22/56.45 (step @p580 :rule cong :premises (@p579) :args (@t861)) % 56.22/56.45 (step @p581 :rule trans :premises (@p580 @p574)) % 56.22/56.45 (step @p582 :rule cong :premises (@p581) :args (@t862)) % 56.22/56.45 (step @p583 :rule exists-elim :args ((= @t191 @t862))) % 56.22/56.45 (step @p584 :rule trans :premises (@p583 @p582)) % 56.22/56.45 (step @p585 :rule eq_resolve :premises (@p62 @p584)) % 56.22/56.45 (step @p586 :rule cnf_or_pos :args (@t855)) % 56.22/56.45 (step @p587 :rule reordering :premises (@p586) :args ((or @t854 @t851 (not @t855)))) % 56.22/56.45 (step @p588 :rule chain_m_resolution :premises (@p587 @p585 @p562) :args (@t851 (@list true false) (@list @t854 @t855))) % 56.22/56.45 (step @p589 :rule skolemize :premises (@p588)) % 56.22/56.45 (step @p590 :rule cnf_or_neg :args (@t864 1)) % 56.22/56.45 (step @p591 :rule chain_m_resolution :premises (@p590 @p589) :args ((not @t863) (@list true) (@list @t864))) % 56.22/56.45 (step @p592 :rule false_intro :premises (@p591)) % 56.22/56.45 (step @p593 :rule symm :premises (@p592)) % 56.22/56.45 (step @p594 :rule trans :premises (@p593 @p536)) % 56.22/56.45 (step @p595 false :rule eq_resolve :premises (@p594 @p476)) % 56.22/56.45 ) % 56.22/56.47 % SZS output end Proof % 56.22/56.47 % cvc5 exiting %------------------------------------------------------------------------------