%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : HWV095_10 : TPTP v9.2.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n013.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:24:09 AM UTC 2026 % Result : Satisfiable 155.24s 155.54s % Output : Model 155.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : HWV095_10 : TPTP v9.2.1. Released v8.2.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.16/0.34 % Computer : n013.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 03:03:00 EDT 2026 % 0.16/0.34 % CPUTime : % 0.46/0.71 %----Disproving TF0_NAR % 0.46/0.73 --- Run --finite-model-find --sort-inference --uf-ss-fair at 60... % 0.46/0.79 --- Run --mbqi at 45... % 45.72/45.92 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --no-cegqi --no-sygus-inst at 45... % 90.81/91.09 --- Run --full-saturate-quant at 45... % 135.96/136.25 --- Run --finite-model-find --fmf-bound --macros-quant at 60... % 155.24/155.54 % SZS status Satisfiable % 155.24/155.54 % SZS output start Model % 155.34/155.62 ( % 155.34/155.62 ; cardinality of $$unsorted is 1 % 155.34/155.62 ; rep: (as @$$unsorted_0 $$unsorted) % 155.34/155.62 ; cardinality of tptp.state_type is 2 % 155.34/155.62 ; rep: (as @tptp.state_type_0 tptp.state_type) % 155.34/155.62 ; rep: (as @tptp.state_type_1 tptp.state_type) % 155.34/155.62 ; cardinality of tptp.bitindex_type is 5 % 155.34/155.62 ; rep: (as @tptp.bitindex_type_0 tptp.bitindex_type) % 155.34/155.62 ; rep: (as @tptp.bitindex_type_1 tptp.bitindex_type) % 155.34/155.62 ; rep: (as @tptp.bitindex_type_2 tptp.bitindex_type) % 155.34/155.62 ; rep: (as @tptp.bitindex_type_3 tptp.bitindex_type) % 155.34/155.62 ; rep: (as @tptp.bitindex_type_4 tptp.bitindex_type) % 155.34/155.62 (define-fun tptp.bitIndex400 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex399 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex398 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex397 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex396 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex395 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex394 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex393 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex31 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex30 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex29 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex28 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex27 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex26 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex25 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex24 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex23 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex22 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex21 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex8 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex7 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex6 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex2 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex3 () tptp.bitindex_type (as @tptp.bitindex_type_0 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex4 () tptp.bitindex_type (as @tptp.bitindex_type_4 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex5 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex0 () tptp.bitindex_type (as @tptp.bitindex_type_3 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex1 () tptp.bitindex_type (as @tptp.bitindex_type_2 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex20 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex19 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex18 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex17 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex16 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex15 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex14 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex13 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex12 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex11 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex10 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex9 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex116 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex117 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex118 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex119 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex120 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex121 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex122 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex737 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex736 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex735 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex734 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex733 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex732 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex731 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex32 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex33 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex34 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex35 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex36 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex37 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex38 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex39 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex40 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex41 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex42 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex43 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex44 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex45 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex46 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex47 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex48 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex49 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex50 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex51 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex52 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex53 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex54 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex55 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex56 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex57 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex58 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex59 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex60 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex61 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex62 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex63 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex64 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex65 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex66 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex67 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex68 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex69 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex70 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex71 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex72 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex73 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex74 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex75 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex76 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex77 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex78 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex79 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex80 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex81 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex82 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex83 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex84 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex85 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex86 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex87 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex88 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex89 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex90 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex91 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex92 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex93 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex94 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex95 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex96 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex97 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex98 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex99 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex100 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex101 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex102 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex103 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex104 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex105 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex106 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex107 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex108 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex109 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex110 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex111 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex112 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex113 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex114 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex115 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex614 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex613 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex612 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex611 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex610 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex609 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex608 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex607 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex606 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex605 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex604 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex603 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex602 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex601 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex600 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex599 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex598 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex597 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex596 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex595 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex594 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex593 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex592 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex591 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex590 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex589 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex588 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex587 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex586 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex585 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex584 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex583 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex582 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex581 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex580 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex579 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex578 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex577 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex576 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex575 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex574 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex573 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex572 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex571 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex570 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.62 (define-fun tptp.bitIndex569 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex568 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex567 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex566 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex565 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex564 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex563 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex562 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex561 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex560 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex559 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex558 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex557 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex556 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex555 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex554 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex553 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex552 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex551 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex550 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex549 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex548 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex547 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex546 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex545 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex544 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex543 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex542 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex541 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex540 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex539 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex538 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex537 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex536 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex535 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex534 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex533 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex532 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex531 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex530 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex529 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex528 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex527 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex526 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex525 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex524 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex523 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex522 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex521 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex520 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex519 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex518 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex517 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex516 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex515 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex514 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex513 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex512 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex511 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex510 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex509 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex508 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex507 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex506 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex505 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex504 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex503 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex502 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex501 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex500 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex499 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex498 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex497 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex496 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex495 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex494 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex493 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex492 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex730 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex729 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex728 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex727 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex726 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex725 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex724 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex723 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex722 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex721 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex720 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex719 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex718 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex717 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex716 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex715 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex714 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex713 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex712 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex711 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex710 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex709 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex708 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex707 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex706 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex705 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex704 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex703 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex702 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex701 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex700 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex699 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex698 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex697 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex696 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex695 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex694 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex693 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex692 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex691 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex690 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex689 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex688 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex687 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex686 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex685 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex684 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex683 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex682 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex681 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex680 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex679 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex678 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex677 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex676 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex675 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex674 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex673 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex672 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex671 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex670 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex669 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex668 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex667 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex666 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex665 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex664 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex663 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex662 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex661 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex660 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex659 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex658 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex657 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex656 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex655 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex654 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex653 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex652 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex651 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex650 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex649 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex648 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex647 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex646 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex645 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex644 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex643 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex642 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex641 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex640 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex639 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex638 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex637 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex636 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex635 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex634 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex633 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex632 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex631 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex630 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex629 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex628 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex627 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex626 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex625 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex624 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex623 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex622 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex621 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex620 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex619 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex618 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex617 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex616 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.bitIndex615 () tptp.bitindex_type (as @tptp.bitindex_type_1 tptp.bitindex_type)) % 155.34/155.63 (define-fun tptp.constB0 () tptp.state_type (as @tptp.state_type_0 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB1 () tptp.state_type (as @tptp.state_type_1 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB2 () tptp.state_type (as @tptp.state_type_0 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB3 () tptp.state_type (as @tptp.state_type_1 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB4 () tptp.state_type (as @tptp.state_type_0 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB5 () tptp.state_type (as @tptp.state_type_1 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB6 () tptp.state_type (as @tptp.state_type_0 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB7 () tptp.state_type (as @tptp.state_type_1 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB8 () tptp.state_type (as @tptp.state_type_0 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB9 () tptp.state_type (as @tptp.state_type_1 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB10 () tptp.state_type (as @tptp.state_type_0 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB11 () tptp.state_type (as @tptp.state_type_1 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB12 () tptp.state_type (as @tptp.state_type_0 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB13 () tptp.state_type (as @tptp.state_type_1 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB14 () tptp.state_type (as @tptp.state_type_0 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB15 () tptp.state_type (as @tptp.state_type_1 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB16 () tptp.state_type (as @tptp.state_type_0 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB17 () tptp.state_type (as @tptp.state_type_1 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB18 () tptp.state_type (as @tptp.state_type_0 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB19 () tptp.state_type (as @tptp.state_type_1 tptp.state_type)) % 155.34/155.63 (define-fun tptp.constB20 () tptp.state_type (as @tptp.state_type_0 tptp.state_type)) % 155.34/155.63 (define-fun tptp.v18 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v20 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v16 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v14 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v12 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v10 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v39 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v52 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v54 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v50 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v48 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v60 (($x1 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v62 (($x1 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v58 (($x1 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v56 (($x1 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v65 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v64 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v46 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v44 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v93 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v91 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v103 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v121 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v119 ((BOUND_VARIABLE_76664 tptp.state_type)) Bool (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76664))) % 155.34/155.63 (define-fun tptp.v117 ((BOUND_VARIABLE_76664 tptp.state_type)) Bool (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76664))) % 155.34/155.63 (define-fun tptp.v115 ((BOUND_VARIABLE_76664 tptp.state_type)) Bool (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76664))) % 155.34/155.63 (define-fun tptp.v113 ((BOUND_VARIABLE_76664 tptp.state_type)) Bool (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76664))) % 155.34/155.63 (define-fun tptp.v111 ((BOUND_VARIABLE_76664 tptp.state_type)) Bool (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76664))) % 155.34/155.63 (define-fun tptp.v109 ((BOUND_VARIABLE_76664 tptp.state_type)) Bool (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76664))) % 155.34/155.63 (define-fun tptp.v107 ((BOUND_VARIABLE_76664 tptp.state_type)) Bool (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76664))) % 155.34/155.63 (define-fun tptp.v105 ((BOUND_VARIABLE_76664 tptp.state_type)) Bool (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76664))) % 155.34/155.63 (define-fun tptp.v136 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.b11 ((_arg_1 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v157 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v155 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v153 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v151 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v149 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v147 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v145 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v143 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v141 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v206 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v208 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v204 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v202 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v214 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v216 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v212 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v210 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v200 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v198 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v196 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v194 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v192 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v190 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v188 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v186 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v184 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v182 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v232 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v227 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.range_7_0 (($x1 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v225 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v223 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.b0000 ((_arg_1 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v238 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v236 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v234 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v221 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v241 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v242 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v219 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v252 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v250 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v248 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v246 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v254 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v256 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v258 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v259 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v244 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v265 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.b010 ((_arg_1 tptp.bitindex_type)) Bool (= (as @tptp.bitindex_type_2 tptp.bitindex_type) _arg_1)) % 155.34/155.63 (define-fun tptp.v264 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v269 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.b001 ((_arg_1 tptp.bitindex_type)) Bool (= (as @tptp.bitindex_type_3 tptp.bitindex_type) _arg_1)) % 155.34/155.63 (define-fun tptp.v268 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v267 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v266 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v263 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v270 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v180 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v178 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v176 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v174 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.b01 (($x1 tptp.bitindex_type)) Bool (not (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x1))) % 155.34/155.63 (define-fun tptp.v97 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v279 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v99 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v280 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v278 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v281 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v277 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v130 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v284 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v167 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v283 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v282 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v276 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v286 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v285 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v274 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v165 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v272 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v291 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v290 ((BOUND_VARIABLE_15419 tptp.state_type)) Bool (and (not (and (not (= BOUND_VARIABLE_15419 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_15419 (as @tptp.state_type_1 tptp.state_type))))) (not (= BOUND_VARIABLE_15419 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_15419 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v169 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v301 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v300 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v299 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v302 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v298 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v297 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v296 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v295 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v304 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v303 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v294 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v307 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v306 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v308 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v305 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v311 ((BOUND_VARIABLE_78016 tptp.state_type)) Bool (or (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_78016) (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78016))) % 155.34/155.63 (define-fun tptp.v310 ((BOUND_VARIABLE_78016 tptp.state_type)) Bool (or (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_78016) (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78016))) % 155.34/155.63 (define-fun tptp.v312 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v309 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v292 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v314 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.b10 (($x1 tptp.bitindex_type)) Bool (not (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x1))) % 155.34/155.63 (define-fun tptp.v313 ((BOUND_VARIABLE_15137 tptp.state_type)) Bool (and (not (and (not (= BOUND_VARIABLE_15137 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_15137 (as @tptp.state_type_1 tptp.state_type))))) (not (= BOUND_VARIABLE_15137 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_15137 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v321 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v320 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v319 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v318 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v322 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v317 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v325 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v324 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v326 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v323 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v328 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v329 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v327 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v315 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v332 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.b00 ((_arg_1 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v331 ((BOUND_VARIABLE_14915 tptp.state_type)) Bool (not (and (not (= BOUND_VARIABLE_14915 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_14915 (as @tptp.state_type_1 tptp.state_type)))))) % 155.34/155.63 (define-fun tptp.v334 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v333 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v330 ((BOUND_VARIABLE_14877 tptp.state_type)) Bool (or (not (and (not (= BOUND_VARIABLE_14877 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_14877 (as @tptp.state_type_1 tptp.state_type))))) (and (not (= BOUND_VARIABLE_14877 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_14877 (as @tptp.state_type_1 tptp.state_type)))))) % 155.34/155.63 (define-fun tptp.v172 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.range_3_0 (($x1 tptp.bitindex_type)) Bool (or (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x1))) % 155.34/155.63 (define-fun tptp.v340 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v1 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v338 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v336 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v347 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.nextState (($x1 tptp.state_type) ($x2 tptp.state_type)) Bool (or (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.state_type_0 tptp.state_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.state_type_1 tptp.state_type) $x2)))) % 155.34/155.63 (define-fun tptp.v345 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v344 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v343 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v354 ((BOUND_VARIABLE_78406 tptp.state_type)) Bool (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78406))) % 155.34/155.63 (define-fun tptp.b1000 (($x1 tptp.bitindex_type)) Bool (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x1)) % 155.34/155.63 (define-fun tptp.v351 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2))) % 155.34/155.63 (define-fun tptp.v353 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2))) % 155.34/155.63 (define-fun tptp.undeclared () Bool false) % 155.34/155.63 (define-fun tptp.v359 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v363 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v364 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v362 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v361 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v365 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v163 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v161 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v370 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v369 ((BOUND_VARIABLE_14643 tptp.state_type)) Bool (not (and (not (= BOUND_VARIABLE_14643 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_14643 (as @tptp.state_type_1 tptp.state_type)))))) % 155.34/155.63 (define-fun tptp.v372 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v371 ((BOUND_VARIABLE_14615 tptp.state_type)) Bool (and (not (and (not (= BOUND_VARIABLE_14615 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_14615 (as @tptp.state_type_1 tptp.state_type))))) (not (= BOUND_VARIABLE_14615 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_14615 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.b000 ((_arg_1 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v134 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v374 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v382 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.range_2_0 (($x1 tptp.bitindex_type)) Bool (or (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x1))) % 155.34/155.63 (define-fun tptp.v387 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v386 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v385 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v388 ((BOUND_VARIABLE_14538 tptp.state_type)) Bool (not (or (= BOUND_VARIABLE_14538 (as @tptp.state_type_0 tptp.state_type)) (= BOUND_VARIABLE_14538 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v384 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v381 ((BOUND_VARIABLE_78016 tptp.state_type)) Bool (or (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_78016) (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78016))) % 155.34/155.63 (define-fun tptp.v380 ((BOUND_VARIABLE_14505 tptp.state_type)) Bool (not (or (= BOUND_VARIABLE_14505 (as @tptp.state_type_0 tptp.state_type)) (= BOUND_VARIABLE_14505 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v379 ((BOUND_VARIABLE_14475 tptp.state_type)) Bool (not (or (= BOUND_VARIABLE_14475 (as @tptp.state_type_0 tptp.state_type)) (= BOUND_VARIABLE_14475 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v390 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v389 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v378 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v393 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v392 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v394 ((BOUND_VARIABLE_14416 tptp.state_type)) Bool (not (or (= BOUND_VARIABLE_14416 (as @tptp.state_type_0 tptp.state_type)) (= BOUND_VARIABLE_14416 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v391 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v397 ((BOUND_VARIABLE_78016 tptp.state_type)) Bool (or (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_78016) (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78016))) % 155.34/155.63 (define-fun tptp.v396 ((BOUND_VARIABLE_78016 tptp.state_type)) Bool (or (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_78016) (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78016))) % 155.34/155.63 (define-fun tptp.v398 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v395 ((BOUND_VARIABLE_78016 tptp.state_type)) Bool (or (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_78016) (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78016))) % 155.34/155.63 (define-fun tptp.v376 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v375 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.b00000000000000000000000000000000 ((_arg_1 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v373 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.range_31_0 (($x1 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v401 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v400 ((BOUND_VARIABLE_14273 tptp.state_type)) Bool (and (not (and (not (= BOUND_VARIABLE_14273 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_14273 (as @tptp.state_type_1 tptp.state_type))))) (not (= BOUND_VARIABLE_14273 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_14273 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.b100 (($x1 tptp.bitindex_type)) Bool (and (not (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x1)) (not (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x1)))) % 155.34/155.63 (define-fun tptp.v403 ((BOUND_VARIABLE_14258 tptp.state_type)) Bool (not (and (not (= BOUND_VARIABLE_14258 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_14258 (as @tptp.state_type_0 tptp.state_type)))))) % 155.34/155.63 (define-fun tptp.v409 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v408 ((BOUND_VARIABLE_14243 tptp.state_type)) Bool (not (and (not (= BOUND_VARIABLE_14243 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_14243 (as @tptp.state_type_0 tptp.state_type)))))) % 155.34/155.63 (define-fun tptp.v410 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v407 ((BOUND_VARIABLE_14204 tptp.state_type)) Bool (not (and (not (= BOUND_VARIABLE_14204 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_14204 (as @tptp.state_type_0 tptp.state_type)))))) % 155.34/155.63 (define-fun tptp.v411 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v406 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v414 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v415 ((BOUND_VARIABLE_14168 tptp.state_type)) Bool (not (and (not (= BOUND_VARIABLE_14168 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_14168 (as @tptp.state_type_0 tptp.state_type)))))) % 155.34/155.63 (define-fun tptp.v413 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v416 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v412 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v404 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v402 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v418 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v417 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v139 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v420 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v427 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v425 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v424 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v423 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v434 ((BOUND_VARIABLE_78406 tptp.state_type)) Bool (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78406))) % 155.34/155.63 (define-fun tptp.v431 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v433 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v132 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v441 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v444 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v439 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v451 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v450 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v452 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v449 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v448 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v453 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v447 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v454 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v446 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v457 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v458 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v456 (($x1 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v455 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v125 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v123 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v464 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v463 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.range_8_1 (($x1 tptp.bitindex_type)) Bool (or (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x1) (= (as @tptp.bitindex_type_4 tptp.bitindex_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x1))) % 155.34/155.63 (define-fun tptp.v462 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_4 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_4 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v467 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v474 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v472 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v471 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v484 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v460 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v485 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v483 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v486 ((BOUND_VARIABLE_78016 tptp.state_type)) Bool (or (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_78016) (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78016))) % 155.34/155.63 (define-fun tptp.v482 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v481 ((BOUND_VARIABLE_76664 tptp.state_type)) Bool (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76664))) % 155.34/155.63 (define-fun tptp.v487 ((BOUND_VARIABLE_78406 tptp.state_type)) Bool (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78406))) % 155.34/155.63 (define-fun tptp.v478 ((BOUND_VARIABLE_13766 tptp.state_type)) Bool (or (not (= BOUND_VARIABLE_13766 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_13766 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v480 (($x1 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v470 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v491 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v488 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v490 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v101 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v511 ((BOUND_VARIABLE_78406 tptp.state_type)) Bool (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78406))) % 155.34/155.63 (define-fun tptp.v512 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_4 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_4 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v515 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v514 ((BOUND_VARIABLE_13712 tptp.state_type)) Bool (and (= BOUND_VARIABLE_13712 (as @tptp.state_type_1 tptp.state_type)) (not (and (not (= BOUND_VARIABLE_13712 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13712 (as @tptp.state_type_0 tptp.state_type))))))) % 155.34/155.63 (define-fun tptp.v517 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v516 ((BOUND_VARIABLE_13684 tptp.state_type)) Bool (and (= BOUND_VARIABLE_13684 (as @tptp.state_type_1 tptp.state_type)) (not (= BOUND_VARIABLE_13684 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13684 (as @tptp.state_type_0 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v518 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v521 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v520 ((BOUND_VARIABLE_13657 tptp.state_type)) Bool (and (not (= BOUND_VARIABLE_13657 (as @tptp.state_type_1 tptp.state_type))) (not (and (not (= BOUND_VARIABLE_13657 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13657 (as @tptp.state_type_0 tptp.state_type))))))) % 155.34/155.63 (define-fun tptp.v522 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v525 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v524 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v513 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.range_8_0 (($x1 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v510 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_4 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v508 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v506 ((BOUND_VARIABLE_76664 tptp.state_type)) Bool (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76664))) % 155.34/155.63 (define-fun tptp.v541 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v539 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.range_122_116 (($x1 tptp.bitindex_type)) Bool (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x1)) % 155.34/155.63 (define-fun tptp.v537 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v535 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v533 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v531 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v529 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v527 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v501 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v543 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v544 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.range_122_0 (($x1 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v504 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v548 ((BOUND_VARIABLE_76664 tptp.state_type)) Bool (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76664))) % 155.34/155.63 (define-fun tptp.v550 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v551 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v546 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v556 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v555 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v564 ((BOUND_VARIABLE_78406 tptp.state_type)) Bool (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78406))) % 155.34/155.63 (define-fun tptp.v569 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v568 ((BOUND_VARIABLE_13429 tptp.state_type)) Bool (and (= BOUND_VARIABLE_13429 (as @tptp.state_type_1 tptp.state_type)) (not (= BOUND_VARIABLE_13429 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13429 (as @tptp.state_type_0 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v571 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v570 ((BOUND_VARIABLE_13402 tptp.state_type)) Bool (and (not (= BOUND_VARIABLE_13402 (as @tptp.state_type_1 tptp.state_type))) (not (and (not (= BOUND_VARIABLE_13402 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13402 (as @tptp.state_type_0 tptp.state_type))))))) % 155.34/155.63 (define-fun tptp.v567 ((BOUND_VARIABLE_13390 tptp.state_type)) Bool (or (and (= BOUND_VARIABLE_13390 (as @tptp.state_type_1 tptp.state_type)) (not (= BOUND_VARIABLE_13390 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13390 (as @tptp.state_type_0 tptp.state_type)))) (and (not (= BOUND_VARIABLE_13390 (as @tptp.state_type_1 tptp.state_type))) (not (and (not (= BOUND_VARIABLE_13390 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13390 (as @tptp.state_type_0 tptp.state_type)))))))) % 155.34/155.63 (define-fun tptp.v573 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v572 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v566 ((BOUND_VARIABLE_13352 tptp.state_type)) Bool (or (and (not (= BOUND_VARIABLE_13352 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13352 (as @tptp.state_type_0 tptp.state_type)))) (and (= BOUND_VARIABLE_13352 (as @tptp.state_type_1 tptp.state_type)) (not (= BOUND_VARIABLE_13352 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13352 (as @tptp.state_type_0 tptp.state_type)))) (and (not (= BOUND_VARIABLE_13352 (as @tptp.state_type_1 tptp.state_type))) (not (and (not (= BOUND_VARIABLE_13352 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13352 (as @tptp.state_type_0 tptp.state_type)))))))) % 155.34/155.63 (define-fun tptp.v574 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v565 ((BOUND_VARIABLE_13332 tptp.state_type)) Bool (and (or (and (not (= BOUND_VARIABLE_13332 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13332 (as @tptp.state_type_0 tptp.state_type)))) (and (= BOUND_VARIABLE_13332 (as @tptp.state_type_1 tptp.state_type)) (not (= BOUND_VARIABLE_13332 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13332 (as @tptp.state_type_0 tptp.state_type)))) (and (not (= BOUND_VARIABLE_13332 (as @tptp.state_type_1 tptp.state_type))) (not (and (not (= BOUND_VARIABLE_13332 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13332 (as @tptp.state_type_0 tptp.state_type))))))) (= BOUND_VARIABLE_13332 (as @tptp.state_type_0 tptp.state_type)))) % 155.34/155.63 (define-fun tptp.v563 ((BOUND_VARIABLE_13321 tptp.state_type)) Bool (or (not (= BOUND_VARIABLE_13321 (as @tptp.state_type_0 tptp.state_type))) (and (or (and (not (= BOUND_VARIABLE_13321 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13321 (as @tptp.state_type_0 tptp.state_type)))) (and (= BOUND_VARIABLE_13321 (as @tptp.state_type_1 tptp.state_type)) (not (= BOUND_VARIABLE_13321 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13321 (as @tptp.state_type_0 tptp.state_type)))) (and (not (= BOUND_VARIABLE_13321 (as @tptp.state_type_1 tptp.state_type))) (not (and (not (= BOUND_VARIABLE_13321 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13321 (as @tptp.state_type_0 tptp.state_type))))))) (= BOUND_VARIABLE_13321 (as @tptp.state_type_0 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v578 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v577 ((BOUND_VARIABLE_13294 tptp.state_type)) Bool (and (= BOUND_VARIABLE_13294 (as @tptp.state_type_1 tptp.state_type)) (not (and (not (= BOUND_VARIABLE_13294 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13294 (as @tptp.state_type_0 tptp.state_type))))))) % 155.34/155.63 (define-fun tptp.v576 ((BOUND_VARIABLE_13282 tptp.state_type)) Bool (not (and (= BOUND_VARIABLE_13282 (as @tptp.state_type_1 tptp.state_type)) (not (and (not (= BOUND_VARIABLE_13282 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13282 (as @tptp.state_type_0 tptp.state_type)))))))) % 155.34/155.63 (define-fun tptp.v575 ((BOUND_VARIABLE_13271 tptp.state_type)) Bool (or (not (and (= BOUND_VARIABLE_13271 (as @tptp.state_type_1 tptp.state_type)) (not (and (not (= BOUND_VARIABLE_13271 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13271 (as @tptp.state_type_0 tptp.state_type))))))) (not (= BOUND_VARIABLE_13271 (as @tptp.state_type_0 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v560 ((BOUND_VARIABLE_13260 tptp.state_type)) Bool (and (or (not (= BOUND_VARIABLE_13260 (as @tptp.state_type_0 tptp.state_type))) (and (or (and (not (= BOUND_VARIABLE_13260 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13260 (as @tptp.state_type_0 tptp.state_type)))) (and (= BOUND_VARIABLE_13260 (as @tptp.state_type_1 tptp.state_type)) (not (= BOUND_VARIABLE_13260 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13260 (as @tptp.state_type_0 tptp.state_type)))) (and (not (= BOUND_VARIABLE_13260 (as @tptp.state_type_1 tptp.state_type))) (not (and (not (= BOUND_VARIABLE_13260 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13260 (as @tptp.state_type_0 tptp.state_type))))))) (= BOUND_VARIABLE_13260 (as @tptp.state_type_0 tptp.state_type)))) (or (not (and (= BOUND_VARIABLE_13260 (as @tptp.state_type_1 tptp.state_type)) (not (and (not (= BOUND_VARIABLE_13260 (as @tptp.state_type_1 tptp.state_type))) (not (= BOUND_VARIABLE_13260 (as @tptp.state_type_0 tptp.state_type))))))) (not (= BOUND_VARIABLE_13260 (as @tptp.state_type_0 tptp.state_type)))))) % 155.34/155.63 (define-fun tptp.v562 (($x1 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v554 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v582 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 ((_arg_1 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v579 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_4 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v581 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_4 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v553 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v499 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v497 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v495 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v599 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v597 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v596 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v594 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v592 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v621 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v622 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v620 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v623 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v619 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v624 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v618 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v625 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v617 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v626 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v616 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v627 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v614 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v630 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v628 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v613 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v637 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v636 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v635 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v634 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v633 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v631 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v612 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v640 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v638 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v611 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v641 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v610 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v643 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v608 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v651 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v650 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v649 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v648 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v647 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v645 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v652 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.range_1_0 (($x1 tptp.bitindex_type)) Bool (or (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x1))) % 155.34/155.63 (define-fun tptp.v654 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v660 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v659 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v658 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v656 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v653 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v668 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v667 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v666 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v664 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v671 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v669 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v663 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v675 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v674 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v672 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v661 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v607 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v679 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v680 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v678 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v681 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v677 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v682 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v95 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v687 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v686 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v685 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v694 ((BOUND_VARIABLE_78406 tptp.state_type)) Bool (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78406))) % 155.34/155.63 (define-fun tptp.v691 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v693 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v89 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v87 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v85 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v83 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v81 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v79 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v702 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v25 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v701 ((BOUND_VARIABLE_12491 tptp.state_type)) Bool (not (and (not (= BOUND_VARIABLE_12491 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_12491 (as @tptp.state_type_1 tptp.state_type)))))) % 155.34/155.63 (define-fun tptp.b00000 ((_arg_1 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v75 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.range_4_0 (($x1 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v704 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v703 ((BOUND_VARIABLE_12456 tptp.state_type)) Bool (and (not (and (not (= BOUND_VARIABLE_12456 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_12456 (as @tptp.state_type_1 tptp.state_type))))) (not (= BOUND_VARIABLE_12456 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_12456 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v706 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v714 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v723 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v722 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v721 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v724 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v720 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v719 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v725 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v718 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v717 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v726 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v716 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v713 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v712 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v711 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v728 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v727 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v710 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v731 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v730 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v732 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v729 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v735 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v734 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v736 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v733 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v739 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v738 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v740 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v737 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v743 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v742 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v744 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v741 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v708 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v707 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.range_5_0 (($x1 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v705 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v746 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v745 ((BOUND_VARIABLE_11938 tptp.state_type)) Bool (and (not (and (not (= BOUND_VARIABLE_11938 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_11938 (as @tptp.state_type_1 tptp.state_type))))) (not (= BOUND_VARIABLE_11938 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_11938 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.b01111 (($x1 tptp.bitindex_type)) Bool (or (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x1))) % 155.34/155.63 (define-fun tptp.v748 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v756 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v755 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v754 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v753 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v757 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v752 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v758 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v751 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v761 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v762 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v760 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v763 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v759 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v766 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v767 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v765 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v768 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v764 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v771 ((BOUND_VARIABLE_78016 tptp.state_type)) Bool (or (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_78016) (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78016))) % 155.34/155.63 (define-fun tptp.v772 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v770 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v773 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v769 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v749 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v747 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v775 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v774 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v77 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v781 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v779 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v777 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v788 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v786 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v785 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v784 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v795 ((BOUND_VARIABLE_78406 tptp.state_type)) Bool (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78406))) % 155.34/155.63 (define-fun tptp.v792 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v794 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v73 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v71 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v33 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v802 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v29 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v803 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v801 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v806 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v805 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v807 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v804 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v800 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v810 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v809 (($x1 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v808 (($x1 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v31 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v817 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v815 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v814 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v813 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v824 ((BOUND_VARIABLE_78406 tptp.state_type)) Bool (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78406))) % 155.34/155.63 (define-fun tptp.v821 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v823 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v828 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v832 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v831 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v830 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v834 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v833 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v829 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v69 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v67 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v837 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v836 ((BOUND_VARIABLE_11246 tptp.state_type)) Bool (not (and (not (= BOUND_VARIABLE_11246 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_11246 (as @tptp.state_type_1 tptp.state_type)))))) % 155.34/155.63 (define-fun tptp.v37 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v839 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v838 ((BOUND_VARIABLE_11218 tptp.state_type)) Bool (and (not (and (not (= BOUND_VARIABLE_11218 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_11218 (as @tptp.state_type_1 tptp.state_type))))) (not (= BOUND_VARIABLE_11218 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_11218 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v841 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v849 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v857 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v856 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v855 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v858 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v854 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v853 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v859 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v852 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v851 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v860 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v850 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v848 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v847 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v846 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v862 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v861 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v845 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v865 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v864 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v866 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v863 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v869 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v868 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v870 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v867 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v873 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v872 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v874 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v871 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v877 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v876 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v878 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v875 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v843 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v842 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool true) % 155.34/155.63 (define-fun tptp.v840 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v880 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v879 ((BOUND_VARIABLE_10711 tptp.state_type)) Bool (and (not (and (not (= BOUND_VARIABLE_10711 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_10711 (as @tptp.state_type_1 tptp.state_type))))) (not (= BOUND_VARIABLE_10711 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_10711 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v882 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v890 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v889 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v888 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v887 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v891 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v886 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v892 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v885 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v895 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v896 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v894 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v897 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v893 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v900 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v901 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v899 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v902 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v898 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v905 ((BOUND_VARIABLE_78016 tptp.state_type)) Bool (or (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_78016) (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78016))) % 155.34/155.63 (define-fun tptp.v906 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v904 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v907 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v903 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v883 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v881 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v909 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v908 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v42 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v911 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v918 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_0 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v916 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v915 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v914 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v925 ((BOUND_VARIABLE_78406 tptp.state_type)) Bool (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78406))) % 155.34/155.63 (define-fun tptp.v922 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v924 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool false) % 155.34/155.63 (define-fun tptp.v35 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v932 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v931 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v933 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v930 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v935 (($x1 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v934 (($x1 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v941 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v939 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v938 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v944 (($x1 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v946 (($x1 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v950 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v953 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v952 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v955 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v954 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v951 (($x1 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v27 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.b1110 ((_arg_1 tptp.bitindex_type)) Bool (or (= (as @tptp.bitindex_type_0 tptp.bitindex_type) _arg_1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) _arg_1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) _arg_1))) % 155.34/155.63 (define-fun tptp.v8 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v959 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v966 ((BOUND_VARIABLE_78016 tptp.state_type)) Bool (or (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_78016) (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78016))) % 155.34/155.63 (define-fun tptp.v965 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v964 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v967 ((BOUND_VARIABLE_10166 tptp.state_type)) Bool (not (or (= BOUND_VARIABLE_10166 (as @tptp.state_type_0 tptp.state_type)) (= BOUND_VARIABLE_10166 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v963 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v968 ((BOUND_VARIABLE_78016 tptp.state_type)) Bool (or (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_78016) (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78016))) % 155.34/155.63 (define-fun tptp.v962 ((BOUND_VARIABLE_78016 tptp.state_type)) Bool (or (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_78016) (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78016))) % 155.34/155.63 (define-fun tptp.v971 ((BOUND_VARIABLE_10221 tptp.state_type)) Bool (not (or (= BOUND_VARIABLE_10221 (as @tptp.state_type_0 tptp.state_type)) (= BOUND_VARIABLE_10221 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v972 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v970 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v973 ((BOUND_VARIABLE_78016 tptp.state_type)) Bool (or (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_78016) (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78016))) % 155.34/155.63 (define-fun tptp.v969 ((BOUND_VARIABLE_78016 tptp.state_type)) Bool (or (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_78016) (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78016))) % 155.34/155.63 (define-fun tptp.v976 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v977 ((BOUND_VARIABLE_10070 tptp.state_type)) Bool (not (or (= BOUND_VARIABLE_10070 (as @tptp.state_type_0 tptp.state_type)) (= BOUND_VARIABLE_10070 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v975 ((BOUND_VARIABLE_10059 tptp.state_type)) Bool (not (or (= BOUND_VARIABLE_10059 (as @tptp.state_type_0 tptp.state_type)) (= BOUND_VARIABLE_10059 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v978 ((BOUND_VARIABLE_78016 tptp.state_type)) Bool (or (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_78016) (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78016))) % 155.34/155.63 (define-fun tptp.v974 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v960 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v958 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_1 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v23 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v983 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v982 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v981 (($x1 tptp.state_type)) Bool (= (as @tptp.state_type_1 tptp.state_type) $x1)) % 155.34/155.63 (define-fun tptp.v990 ((BOUND_VARIABLE_78406 tptp.state_type)) Bool (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_78406))) % 155.34/155.63 (define-fun tptp.v987 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v989 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v1007 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (or (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_0 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2)) (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_2 tptp.bitindex_type) $x2)))) % 155.34/155.63 (define-fun tptp.v1009 ((BOUND_VARIABLE_9984 tptp.state_type)) Bool (not (or (= BOUND_VARIABLE_9984 (as @tptp.state_type_0 tptp.state_type)) (= BOUND_VARIABLE_9984 (as @tptp.state_type_1 tptp.state_type))))) % 155.34/155.63 (define-fun tptp.v1008 ((BOUND_VARIABLE_9973 tptp.state_type)) Bool (and (or (= BOUND_VARIABLE_9973 (as @tptp.state_type_0 tptp.state_type)) (= BOUND_VARIABLE_9973 (as @tptp.state_type_1 tptp.state_type))) (not (or (= BOUND_VARIABLE_9973 (as @tptp.state_type_0 tptp.state_type)) (= BOUND_VARIABLE_9973 (as @tptp.state_type_1 tptp.state_type)))))) % 155.34/155.63 (define-fun tptp.v1006 ((BOUND_VARIABLE_9962 tptp.state_type)) Bool (or (and (or (= BOUND_VARIABLE_9962 (as @tptp.state_type_0 tptp.state_type)) (= BOUND_VARIABLE_9962 (as @tptp.state_type_1 tptp.state_type))) (not (or (= BOUND_VARIABLE_9962 (as @tptp.state_type_0 tptp.state_type)) (= BOUND_VARIABLE_9962 (as @tptp.state_type_1 tptp.state_type))))) (= BOUND_VARIABLE_9962 (as @tptp.state_type_0 tptp.state_type)) (= BOUND_VARIABLE_9962 (as @tptp.state_type_1 tptp.state_type)))) % 155.34/155.63 (define-fun tptp.v1005 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v1004 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v1003 ((BOUND_VARIABLE_76534 tptp.state_type)) Bool false) % 155.34/155.63 (define-fun tptp.v1001 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v1000 (($x1 tptp.state_type) ($x2 tptp.bitindex_type)) Bool (and (not (and (= (as @tptp.state_type_0 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))) (not (and (= (as @tptp.state_type_1 tptp.state_type) $x1) (= (as @tptp.bitindex_type_3 tptp.bitindex_type) $x2))))) % 155.34/155.63 (define-fun tptp.v999 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v998 ((BOUND_VARIABLE_9893 tptp.state_type)) Bool (not (and (not (= BOUND_VARIABLE_9893 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_9893 (as @tptp.state_type_1 tptp.state_type)))))) % 155.34/155.63 (define-fun tptp.v1010 ((BOUND_VARIABLE_77001 tptp.state_type)) Bool true) % 155.34/155.63 (define-fun tptp.v996 ((BOUND_VARIABLE_9871 tptp.state_type)) Bool (not (and (not (= BOUND_VARIABLE_9871 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_9871 (as @tptp.state_type_1 tptp.state_type)))))) % 155.34/155.63 (define-fun tptp.v995 ((BOUND_VARIABLE_76581 tptp.state_type)) Bool (and (not (= (as @tptp.state_type_1 tptp.state_type) BOUND_VARIABLE_76581)) (not (= (as @tptp.state_type_0 tptp.state_type) BOUND_VARIABLE_76581)))) % 155.34/155.63 (define-fun tptp.v4 ((BOUND_VARIABLE_9851 tptp.state_type)) Bool (not (and (not (= BOUND_VARIABLE_9851 (as @tptp.state_type_0 tptp.state_type))) (not (= BOUND_VARIABLE_9851 (as @tptp.state_type_1 tptp.state_type)))))) % 155.34/155.63 (define-fun tptp.reachableState (($x1 tptp.state_type)) Bool true) % 155.34/155.63 ) % 155.34/155.63 % SZS output end Model % 155.34/155.63 % cvc5 exiting %------------------------------------------------------------------------------