From 75392de5453c6992e59943cf6246820a8e8c2d2a Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 20 Sep 2023 23:43:46 +0200 Subject: [PATCH] Add test for prover log regression (#4558) ### Changes Add a test that notifies us when we make changes that change anything about verification, with the caveat that the Dafny input program is not using many Dafny features, so verification changes in specific Dafny features might be missed. By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- .../DafnyPipeline.Test.csproj | 3 + .../DafnyPipeline.Test/ProverLogStability.cs | 149 ++ .../DafnyPipeline.Test/expectedProverLog.smt2 | 1903 +++++++++++++++++ 3 files changed, 2055 insertions(+) create mode 100644 Source/DafnyPipeline.Test/ProverLogStability.cs create mode 100644 Source/DafnyPipeline.Test/expectedProverLog.smt2 diff --git a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj index d22194db572..8cd2a7b82fb 100644 --- a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj +++ b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj @@ -43,5 +43,8 @@ + + PreserveNewest + diff --git a/Source/DafnyPipeline.Test/ProverLogStability.cs b/Source/DafnyPipeline.Test/ProverLogStability.cs new file mode 100644 index 00000000000..a722c76015d --- /dev/null +++ b/Source/DafnyPipeline.Test/ProverLogStability.cs @@ -0,0 +1,149 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Threading.Tasks; +using DafnyCore.Test; +using DafnyTestGeneration; +using Microsoft.Boogie; +using Microsoft.Dafny; +using Xunit; +using Xunit.Abstractions; +using BoogieProgram = Microsoft.Boogie.Program; + +namespace DafnyPipeline.Test { + // Main.Resolve has static shared state (TypeConstraint.ErrorsToBeReported for example) + // so we can't execute tests that use it in parallel. + [Collection("Singleton Test Collection - Resolution")] + public class ProverLogStabilityTest { + + private readonly ITestOutputHelper testOutputHelper; + + // All types of top level declarations. + readonly string originalProgram = @" +module SomeModule { + + module NestedModule { + class C { + var f: int + constructor () + } + } + + method m() ensures false { + var x: NestedModule.C; + x := new NestedModule.C(); + x.f := 4; + } +} + +import opened SomeModule + +type FooSynonym = FooClass + +class FooClass { + var f: int + var c: NestedModule.C + + constructor () +} + +datatype Friends = Agnes | Agatha | Jermaine + +function SomeFunc(funcFormal: int, foo: FooClass): nat + reads foo, foo.c + ensures SomeFunc(funcFormal, foo) == foo.c.f +{ + 3 +} + +method SomeMethod(methodFormal: int) returns (result: bool) + requires methodFormal == 2 + ensures result == (methodFormal == 2) + // ensures forall x :: x == methodFormal +{ + m(); + var lambdaExpr := x => x + 1; + var c := new FooClass(); + result := methodFormal == SomeFunc(42, c); +} + +datatype ImapSimulator_ = ImapSimulator( + input: iset, + apply: A --> B) +{ + ghost predicate Valid() { + forall i <- input :: apply.requires(i) + } +} + +type ImapSimulator = + X: ImapSimulator_ | + X.Valid() witness ImapSimulator(iset{}, (x: A) requires false => match() {}) +"; + + public ProverLogStabilityTest(ITestOutputHelper testOutputHelper) { + this.testOutputHelper = testOutputHelper; + } + + /// + /// This test is meant to detect _any_ changes in Dafny's verification behavior. + /// Dafny's verification is powered by an SMT solver. For difficult inputs, such solvers may change their behavior, + /// both in performance and outcome, even when tiny non-semantic changes such as changes in variable names, + /// are made in the input. + /// + /// To detect whether it is possible that the verification of Dafny proofs has changed, + /// this test compares the input Dafny sends to the SMT solver against what it was sending previously. + /// + /// If this test fails, that means a change was made to Dafny that changes the SMT input it sends. + /// If this was intentional, you should update this test's expect file with the new SMT input. + /// The git history of updates to this test allows us to easily see when Dafny's verification has changed. + /// + /// If you make a change to Dafny verification and this test does not fail, then likely the Dafny code in the test + /// does not sufficiently cover the language to detect your change. In that case, please update the test so it does. + /// + /// Note that this test does not detect changes in DafnyPrelude.bplf + /// + /// + [Fact] + public async Task ProverLogRegression() { + var options = DafnyOptions.Create((TextWriter)new WriterFromOutputHelper(testOutputHelper)); + + var filePath = Path.Combine(Directory.GetCurrentDirectory(), "expectedProverLog.smt2"); + var expectation = await File.ReadAllTextAsync(filePath); + var regularProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, originalProgram)); + Assert.Equal(expectation.Replace("\r", ""), regularProverLog.Replace("\r", "")); + } + + private async Task GetProverLogForProgramAsync(DafnyOptions options, IEnumerable boogiePrograms) { + var logs = await GetProverLogsForProgramAsync(options, boogiePrograms).ToListAsync(); + Assert.Single(logs); + return logs[0]; + } + + private async IAsyncEnumerable GetProverLogsForProgramAsync(DafnyOptions options, + IEnumerable boogiePrograms) { + string directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); + Directory.CreateDirectory(directory); + var temp1 = directory + "/proverLog"; + options.ProverLogFilePath = temp1; + using (var engine = ExecutionEngine.CreateWithoutSharedCache(options)) { + foreach (var boogieProgram in boogiePrograms) { + var (outcome, _) = await DafnyMain.BoogieOnce(options, options.OutputWriter, engine, "", "", boogieProgram, "programId"); + } + } + foreach (var proverFile in Directory.GetFiles(directory)) { + yield return await File.ReadAllTextAsync(proverFile); + } + } + + IEnumerable GetBoogie(DafnyOptions options, string dafnyProgramText) { + var reporter = new BatchErrorReporter(options); + var dafnyProgram = Utils.Parse(reporter, dafnyProgramText, false); + Assert.NotNull(dafnyProgram); + DafnyMain.Resolve(dafnyProgram); + Assert.Equal(0, reporter.ErrorCount); + return Translator.Translate(dafnyProgram, reporter).Select(t => t.Item2).ToList(); + } + } +} diff --git a/Source/DafnyPipeline.Test/expectedProverLog.smt2 b/Source/DafnyPipeline.Test/expectedProverLog.smt2 new file mode 100644 index 00000000000..5fb530ec4e6 --- /dev/null +++ b/Source/DafnyPipeline.Test/expectedProverLog.smt2 @@ -0,0 +1,1903 @@ +(set-option :print-success false) +(set-info :smt-lib-version 2.6) +(set-option :auto_config false) +(set-option :type_check true) +(set-option :smt.qi.eager_threshold 100) +(set-option :smt.delay_units true) +(set-option :smt.case_split 3) +(set-option :smt.arith.solver 2) +(set-option :smt.mbqi false) +(set-option :model.compact false) +(set-option :model.v2 true) +(set-option :pp.bv_literals false) +; done setting options + + +(set-info :category "industrial") +(declare-sort |T@U| 0) +(declare-sort |T@T| 0) +(declare-fun real_pow (Real Real) Real) +(declare-fun UOrdering2 (|T@U| |T@U|) Bool) +(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool) +(declare-fun tickleBool (Bool) Bool) +(assert (and (tickleBool true) (tickleBool false))) +(declare-fun $generated () T@U) +(declare-fun $generated@@0 () T@U) +(declare-fun $generated@@1 () T@U) +(declare-fun $generated@@2 () T@U) +(declare-fun $generated@@3 () T@U) +(declare-fun $generated@@4 () T@U) +(declare-fun $generated@@5 () T@U) +(declare-fun $generated@@6 () T@U) +(declare-fun $generated@@7 () T@U) +(declare-fun $generated@@8 (T@T) Int) +(declare-fun $generated@@9 () T@T) +(declare-fun $generated@@10 () T@T) +(declare-fun $generated@@11 () T@T) +(declare-fun $generated@@12 (Bool) T@U) +(declare-fun $generated@@13 (T@U) Bool) +(declare-fun $generated@@14 (Int) T@U) +(declare-fun $generated@@15 (T@U) Int) +(declare-fun $generated@@16 (Real) T@U) +(declare-fun $generated@@17 (T@U) Real) +(declare-fun $generated@@24 (T@T T@U) Int) +(declare-fun $generated@@25 (T@U) T@U) +(declare-fun $generated@@26 (T@T T@U) T@U) +(declare-fun $generated@@27 (T@U T@U) Bool) +(declare-fun $generated@@28 (T@T T@U) T@U) +(declare-fun $generated@@29 (T@T T@T T@U T@U) T@U) +(declare-fun $generated@@30 () T@T) +(declare-fun $generated@@31 (T@T T@T T@U T@U) T@U) +(declare-fun $generated@@32 () T@T) +(declare-fun $generated@@33 (T@T) T@T) +(declare-fun $generated@@34 (T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@35 (T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@36 (T@T) T@T) +(declare-fun $generated@@72 (T@T T@U T@U T@U) Bool) +(declare-fun $generated@@73 () T@U) +(declare-fun $generated@@74 () T@U) +(declare-fun $generated@@77 (T@T T@U T@U) Bool) +(declare-fun $generated@@78 (T@U) T@U) +(declare-fun $generated@@80 () T@U) +(declare-fun $generated@@83 () T@U) +(declare-fun $generated@@84 (T@T T@U T@U) T@U) +(declare-fun $generated@@85 (T@T T@U) Bool) +(declare-fun $generated@@86 (Int) Int) +(declare-fun $generated@@88 (T@T T@U) T@U) +(declare-fun $generated@@91 (T@U) Bool) +(declare-fun $generated@@103 (T@T T@U) T@U) +(declare-fun $generated@@109 (T@T T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@110 (T@U T@U T@U Bool) T@U) +(declare-fun $generated@@111 (T@T T@T T@T T@U T@U T@U T@U) T@U) +(declare-fun $generated@@156 (T@T T@U) T@U) +(declare-fun $generated@@164 (T@U) T@U) +(assert (and (and (and (and (and (and (and (and (= ($generated@@8 $generated@@9) 0) (= ($generated@@8 $generated@@10) 1)) (= ($generated@@8 $generated@@11) 2)) (forall (($generated@@18 Bool) ) (! (= ($generated@@13 ($generated@@12 $generated@@18)) $generated@@18) + :pattern ( ($generated@@12 $generated@@18)) +))) (forall (($generated@@19 T@U) ) (! (= ($generated@@12 ($generated@@13 $generated@@19)) $generated@@19) + :pattern ( ($generated@@13 $generated@@19)) +))) (forall (($generated@@20 Int) ) (! (= ($generated@@15 ($generated@@14 $generated@@20)) $generated@@20) + :pattern ( ($generated@@14 $generated@@20)) +))) (forall (($generated@@21 T@U) ) (! (= ($generated@@14 ($generated@@15 $generated@@21)) $generated@@21) + :pattern ( ($generated@@15 $generated@@21)) +))) (forall (($generated@@22 Real) ) (! (= ($generated@@17 ($generated@@16 $generated@@22)) $generated@@22) + :pattern ( ($generated@@16 $generated@@22)) +))) (forall (($generated@@23 T@U) ) (! (= ($generated@@16 ($generated@@17 $generated@@23)) $generated@@23) + :pattern ( ($generated@@17 $generated@@23)) +)))) +(assert (distinct $generated $generated@@0 $generated@@1 $generated@@2 $generated@@3 $generated@@4 $generated@@5 $generated@@6 $generated@@7) +) +(assert (= ($generated@@24 $generated@@9 $generated@@1) 0)) +(assert (= ($generated@@25 $generated) $generated@@0)) +(assert (= ($generated@@26 $generated@@9 $generated@@1) $generated@@2)) +(assert (and (and (and (and (and (and (and (forall (($generated@@37 T@T) ($generated@@38 T@T) ($generated@@39 T@U) ($generated@@40 T@U) ($generated@@41 T@U) ) (! (= ($generated@@29 $generated@@37 $generated@@38 ($generated@@34 $generated@@37 $generated@@38 $generated@@40 $generated@@41 $generated@@39) $generated@@41) $generated@@39) + :weight 0 +)) (and (forall (($generated@@42 T@T) ($generated@@43 T@T) ($generated@@44 T@T) ($generated@@45 T@U) ($generated@@46 T@U) ($generated@@47 T@U) ($generated@@48 T@U) ) (! (or (= $generated@@43 $generated@@44) (= ($generated@@29 $generated@@44 $generated@@42 ($generated@@34 $generated@@43 $generated@@42 $generated@@46 $generated@@47 $generated@@45) $generated@@48) ($generated@@29 $generated@@44 $generated@@42 $generated@@46 $generated@@48))) + :weight 0 +)) (forall (($generated@@49 T@T) ($generated@@50 T@T) ($generated@@51 T@T) ($generated@@52 T@U) ($generated@@53 T@U) ($generated@@54 T@U) ($generated@@55 T@U) ) (! (or (= $generated@@54 $generated@@55) (= ($generated@@29 $generated@@51 $generated@@49 ($generated@@34 $generated@@50 $generated@@49 $generated@@53 $generated@@54 $generated@@52) $generated@@55) ($generated@@29 $generated@@51 $generated@@49 $generated@@53 $generated@@55))) + :weight 0 +)))) (= ($generated@@8 $generated@@30) 3)) (forall (($generated@@56 T@T) ($generated@@57 T@T) ($generated@@58 T@U) ($generated@@59 T@U) ($generated@@60 T@U) ) (! (= ($generated@@31 $generated@@56 $generated@@57 ($generated@@35 $generated@@56 $generated@@57 $generated@@59 $generated@@60 $generated@@58) $generated@@60) $generated@@58) + :weight 0 +))) (forall (($generated@@61 T@T) ($generated@@62 T@T) ($generated@@63 T@U) ($generated@@64 T@U) ($generated@@65 T@U) ($generated@@66 T@U) ) (! (or (= $generated@@65 $generated@@66) (= ($generated@@31 $generated@@61 $generated@@62 ($generated@@35 $generated@@61 $generated@@62 $generated@@64 $generated@@65 $generated@@63) $generated@@66) ($generated@@31 $generated@@61 $generated@@62 $generated@@64 $generated@@66))) + :weight 0 +))) (= ($generated@@8 $generated@@32) 4)) (forall (($generated@@67 T@T) ) (= ($generated@@8 ($generated@@33 $generated@@67)) 5))) (forall (($generated@@68 T@T) ) (! (= ($generated@@36 ($generated@@33 $generated@@68)) $generated@@68) + :pattern ( ($generated@@33 $generated@@68)) +)))) +(assert (forall (($generated@@69 T@U) ($generated@@70 T@U) ) (! (=> ($generated@@27 $generated@@69 $generated@@70) (forall (($generated@@71 T@U) ) (! (=> ($generated@@13 ($generated@@28 $generated@@9 ($generated@@29 $generated@@9 $generated@@30 ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@69 $generated@@71) $generated@@1))) ($generated@@13 ($generated@@28 $generated@@9 ($generated@@29 $generated@@9 $generated@@30 ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@70 $generated@@71) $generated@@1)))) + :pattern ( ($generated@@28 $generated@@9 ($generated@@29 $generated@@9 $generated@@30 ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@70 $generated@@71) $generated@@1))) +))) + :pattern ( ($generated@@27 $generated@@69 $generated@@70)) +))) +(assert (forall (($generated@@75 T@U) ($generated@@76 T@U) ) (! (= ($generated@@72 $generated@@32 $generated@@75 $generated@@73 $generated@@76) (or (= $generated@@75 $generated@@74) ($generated@@13 ($generated@@28 $generated@@9 ($generated@@29 $generated@@9 $generated@@30 ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@76 $generated@@75) $generated@@1))))) + :pattern ( ($generated@@72 $generated@@32 $generated@@75 $generated@@73 $generated@@76)) +))) +(assert (forall (($generated@@79 T@U) ) (! (= ($generated@@77 $generated@@32 $generated@@79 $generated@@73) (or (= $generated@@79 $generated@@74) (= ($generated@@78 $generated@@79) $generated@@73))) + :pattern ( ($generated@@77 $generated@@32 $generated@@79 $generated@@73)) +))) +(assert (forall (($generated@@81 T@U) ($generated@@82 T@U) ) (! (= ($generated@@72 $generated@@32 $generated@@81 $generated@@80 $generated@@82) ($generated@@72 $generated@@32 $generated@@81 $generated@@73 $generated@@82)) + :pattern ( ($generated@@72 $generated@@32 $generated@@81 $generated@@80 $generated@@82)) +))) +(assert (= ($generated@@24 $generated@@10 $generated@@83) 0)) +(assert (= ($generated@@84 $generated@@10 $generated@@4 $generated@@7) $generated@@83)) +(assert (not ($generated@@85 $generated@@10 $generated@@83))) +(assert (forall (($generated@@87 Int) ) (! (= ($generated@@86 $generated@@87) $generated@@87) + :pattern ( ($generated@@86 $generated@@87)) +))) +(assert (forall (($generated@@89 T@U) ($generated@@90 T@T) ) (! (= ($generated@@88 $generated@@90 $generated@@89) $generated@@89) + :pattern ( ($generated@@88 $generated@@90 $generated@@89)) +))) +(assert (forall (($generated@@92 T@U) ($generated@@93 T@U) ) (! (=> (and (and ($generated@@91 $generated@@92) (and (or (not (= $generated@@93 $generated@@74)) (not true)) (= ($generated@@78 $generated@@93) $generated@@73))) ($generated@@13 ($generated@@28 $generated@@9 ($generated@@29 $generated@@9 $generated@@30 ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@92 $generated@@93) $generated@@1)))) ($generated@@72 $generated@@10 ($generated@@28 $generated@@10 ($generated@@29 $generated@@10 $generated@@30 ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@92 $generated@@93) $generated@@83)) $generated $generated@@92)) + :pattern ( ($generated@@28 $generated@@10 ($generated@@29 $generated@@10 $generated@@30 ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@92 $generated@@93) $generated@@83))) +))) +(assert ($generated@@85 $generated@@9 $generated@@1)) +(assert (forall (($generated@@94 T@U) ($generated@@95 T@U) ($generated@@96 T@U) ($generated@@97 T@U) ($generated@@98 T@T) ) (! (=> ($generated@@27 $generated@@94 $generated@@95) (=> ($generated@@72 $generated@@98 $generated@@96 $generated@@97 $generated@@94) ($generated@@72 $generated@@98 $generated@@96 $generated@@97 $generated@@95))) + :pattern ( ($generated@@27 $generated@@94 $generated@@95) ($generated@@72 $generated@@98 $generated@@96 $generated@@97 $generated@@94)) +))) +(assert (forall (($generated@@99 T@U) ) (! (= ($generated@@77 $generated@@32 $generated@@99 $generated@@80) (and ($generated@@77 $generated@@32 $generated@@99 $generated@@73) (or (not (= $generated@@99 $generated@@74)) (not true)))) + :pattern ( ($generated@@77 $generated@@32 $generated@@99 $generated@@80)) +))) +(assert (forall (($generated@@100 T@U) ($generated@@101 T@U) ($generated@@102 T@U) ) (! (=> (or (not (= $generated@@100 $generated@@102)) (not true)) (=> (and ($generated@@27 $generated@@100 $generated@@101) ($generated@@27 $generated@@101 $generated@@102)) ($generated@@27 $generated@@100 $generated@@102))) + :pattern ( ($generated@@27 $generated@@100 $generated@@101) ($generated@@27 $generated@@101 $generated@@102)) +))) +(assert (forall (($generated@@104 T@U) ($generated@@105 T@U) ($generated@@106 T@T) ) (! (and (= ($generated@@103 $generated@@106 ($generated@@84 $generated@@106 $generated@@104 $generated@@105)) $generated@@104) (= ($generated@@26 $generated@@106 ($generated@@84 $generated@@106 $generated@@104 $generated@@105)) $generated@@105)) + :pattern ( ($generated@@84 $generated@@106 $generated@@104 $generated@@105)) +))) +(assert (forall (($generated@@107 T@U) ($generated@@108 T@U) ) (! (=> (and ($generated@@91 $generated@@107) (and (or (not (= $generated@@108 $generated@@74)) (not true)) (= ($generated@@78 $generated@@108) $generated@@73))) ($generated@@77 $generated@@10 ($generated@@28 $generated@@10 ($generated@@29 $generated@@10 $generated@@30 ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@107 $generated@@108) $generated@@83)) $generated)) + :pattern ( ($generated@@28 $generated@@10 ($generated@@29 $generated@@10 $generated@@30 ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@107 $generated@@108) $generated@@83))) +))) +(assert (and (forall (($generated@@112 T@T) ($generated@@113 T@T) ($generated@@114 T@T) ($generated@@115 T@U) ($generated@@116 T@U) ($generated@@117 T@U) ($generated@@118 T@U) ) (! (= ($generated@@109 $generated@@112 $generated@@113 $generated@@114 ($generated@@111 $generated@@112 $generated@@113 $generated@@114 $generated@@116 $generated@@117 $generated@@118 $generated@@115) $generated@@117 $generated@@118) $generated@@115) + :weight 0 +)) (and (and (forall (($generated@@119 T@T) ($generated@@120 T@T) ($generated@@121 T@T) ($generated@@122 T@T) ($generated@@123 T@U) ($generated@@124 T@U) ($generated@@125 T@U) ($generated@@126 T@U) ($generated@@127 T@U) ($generated@@128 T@U) ) (! (or (= $generated@@121 $generated@@122) (= ($generated@@109 $generated@@122 $generated@@119 $generated@@120 ($generated@@111 $generated@@121 $generated@@119 $generated@@120 $generated@@124 $generated@@125 $generated@@126 $generated@@123) $generated@@127 $generated@@128) ($generated@@109 $generated@@122 $generated@@119 $generated@@120 $generated@@124 $generated@@127 $generated@@128))) + :weight 0 +)) (forall (($generated@@129 T@T) ($generated@@130 T@T) ($generated@@131 T@T) ($generated@@132 T@T) ($generated@@133 T@U) ($generated@@134 T@U) ($generated@@135 T@U) ($generated@@136 T@U) ($generated@@137 T@U) ($generated@@138 T@U) ) (! (or (= $generated@@135 $generated@@137) (= ($generated@@109 $generated@@132 $generated@@129 $generated@@130 ($generated@@111 $generated@@131 $generated@@129 $generated@@130 $generated@@134 $generated@@135 $generated@@136 $generated@@133) $generated@@137 $generated@@138) ($generated@@109 $generated@@132 $generated@@129 $generated@@130 $generated@@134 $generated@@137 $generated@@138))) + :weight 0 +))) (forall (($generated@@139 T@T) ($generated@@140 T@T) ($generated@@141 T@T) ($generated@@142 T@T) ($generated@@143 T@U) ($generated@@144 T@U) ($generated@@145 T@U) ($generated@@146 T@U) ($generated@@147 T@U) ($generated@@148 T@U) ) (! (or (= $generated@@146 $generated@@148) (= ($generated@@109 $generated@@142 $generated@@139 $generated@@140 ($generated@@111 $generated@@141 $generated@@139 $generated@@140 $generated@@144 $generated@@145 $generated@@146 $generated@@143) $generated@@147 $generated@@148) ($generated@@109 $generated@@142 $generated@@139 $generated@@140 $generated@@144 $generated@@147 $generated@@148))) + :weight 0 +))))) +(assert (forall (($generated@@149 T@U) ($generated@@150 T@U) ($generated@@151 T@U) ($generated@@152 Bool) ($generated@@153 T@U) ($generated@@154 T@U) ($generated@@155 T@T) ) (! (= ($generated@@13 ($generated@@109 $generated@@155 $generated@@32 $generated@@9 ($generated@@110 $generated@@149 $generated@@150 $generated@@151 $generated@@152) $generated@@153 $generated@@154)) (=> (and (or (not (= $generated@@153 $generated@@149)) (not true)) ($generated@@13 ($generated@@28 $generated@@9 ($generated@@29 $generated@@9 $generated@@30 ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@150 $generated@@153) $generated@@151)))) $generated@@152)) + :pattern ( ($generated@@109 $generated@@155 $generated@@32 $generated@@9 ($generated@@110 $generated@@149 $generated@@150 $generated@@151 $generated@@152) $generated@@153 $generated@@154)) +))) +(assert (forall (($generated@@157 T@U) ($generated@@158 T@T) ) (! (= ($generated@@28 $generated@@158 ($generated@@156 $generated@@158 $generated@@157)) $generated@@157) + :pattern ( ($generated@@156 $generated@@158 $generated@@157)) +))) +(assert (forall (($generated@@159 T@U) ($generated@@160 T@U) ($generated@@161 T@U) ($generated@@162 T@U) ($generated@@163 T@T) ) (! (=> ($generated@@91 ($generated@@35 $generated@@32 ($generated@@33 $generated@@30) $generated@@159 $generated@@160 ($generated@@34 $generated@@163 $generated@@30 ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@159 $generated@@160) $generated@@161 ($generated@@156 $generated@@163 $generated@@162)))) ($generated@@27 $generated@@159 ($generated@@35 $generated@@32 ($generated@@33 $generated@@30) $generated@@159 $generated@@160 ($generated@@34 $generated@@163 $generated@@30 ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@159 $generated@@160) $generated@@161 ($generated@@156 $generated@@163 $generated@@162))))) + :pattern ( ($generated@@35 $generated@@32 ($generated@@33 $generated@@30) $generated@@159 $generated@@160 ($generated@@34 $generated@@163 $generated@@30 ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@159 $generated@@160) $generated@@161 ($generated@@156 $generated@@163 $generated@@162)))) +))) +(assert (= ($generated@@25 $generated@@80) $generated@@3)) +(assert (= ($generated@@164 $generated@@80) $generated@@6)) +(assert (= ($generated@@25 $generated@@73) $generated@@5)) +(assert (= ($generated@@164 $generated@@73) $generated@@6)) +(assert (forall (($generated@@165 Int) ) (! (= ($generated@@156 $generated@@10 ($generated@@14 ($generated@@86 $generated@@165))) ($generated@@88 $generated@@30 ($generated@@156 $generated@@10 ($generated@@14 $generated@@165)))) + :pattern ( ($generated@@156 $generated@@10 ($generated@@14 ($generated@@86 $generated@@165)))) +))) +(assert (forall (($generated@@166 T@U) ($generated@@167 T@T) ) (! (= ($generated@@156 $generated@@167 ($generated@@88 $generated@@167 $generated@@166)) ($generated@@88 $generated@@30 ($generated@@156 $generated@@167 $generated@@166))) + :pattern ( ($generated@@156 $generated@@167 ($generated@@88 $generated@@167 $generated@@166))) +))) +(assert (forall (($generated@@168 T@U) ($generated@@169 T@U) ) (! ($generated@@72 $generated@@10 $generated@@169 $generated $generated@@168) + :pattern ( ($generated@@72 $generated@@10 $generated@@169 $generated $generated@@168)) +))) +(assert (forall (($generated@@170 T@U) ) (! ($generated@@77 $generated@@10 $generated@@170 $generated) + :pattern ( ($generated@@77 $generated@@10 $generated@@170 $generated)) +))) +(push 1) +(declare-fun ControlFlow (Int Int) Int) +(declare-fun $generated@@171 () T@U) +(declare-fun $generated@@172 () T@U) +(declare-fun $generated@@173 () Bool) +(declare-fun $generated@@174 () T@U) +(declare-fun $generated@@175 () T@U) +(declare-fun $generated@@176 () T@U) +(declare-fun $generated@@177 (T@U) Bool) +(declare-fun $generated@@178 () T@U) +(declare-fun $generated@@179 () Int) +(declare-fun $generated@@180 () T@U) +(declare-fun $generated@@181 () T@U) +(declare-fun $generated@@182 () Int) +(set-option :timeout 0) +(set-option :rlimit 0) +(assert (not + (=> (= (ControlFlow 0 0) 6) (let (($generated@@183 (=> (and (= $generated@@171 ($generated@@110 $generated@@74 $generated@@172 $generated@@1 false)) (=> $generated@@173 (and ($generated@@77 $generated@@32 $generated@@174 $generated@@80) ($generated@@72 $generated@@32 $generated@@174 $generated@@80 $generated@@172)))) (=> (and (and (or (not (= $generated@@175 $generated@@74)) (not true)) (and ($generated@@77 $generated@@32 $generated@@175 $generated@@80) ($generated@@72 $generated@@32 $generated@@175 $generated@@80 $generated@@172))) (and ($generated@@91 $generated@@176) ($generated@@177 $generated@@176))) (=> (and (and (and (or (not (= $generated@@178 $generated@@74)) (not true)) (and ($generated@@77 $generated@@32 $generated@@178 $generated@@80) ($generated@@72 $generated@@32 $generated@@178 $generated@@80 $generated@@176))) (not ($generated@@13 ($generated@@28 $generated@@9 ($generated@@29 $generated@@9 $generated@@30 ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@172 $generated@@178) $generated@@1))))) (and (forall (($generated@@184 T@U) ) (! (=> (and (or (not (= $generated@@184 $generated@@74)) (not true)) ($generated@@13 ($generated@@28 $generated@@9 ($generated@@29 $generated@@9 $generated@@30 ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@172 $generated@@184) $generated@@1)))) (= ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@176 $generated@@184) ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@172 $generated@@184))) + :pattern ( ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@176 $generated@@184)) +)) ($generated@@27 $generated@@172 $generated@@176))) (and (=> (= (ControlFlow 0 2) (- 0 5)) true) (and (=> (= (ControlFlow 0 2) (- 0 4)) (or (not (= $generated@@178 $generated@@74)) (not true))) (=> (or (not (= $generated@@178 $generated@@74)) (not true)) (and (=> (= (ControlFlow 0 2) (- 0 3)) ($generated@@13 ($generated@@109 $generated@@10 $generated@@32 $generated@@9 $generated@@171 $generated@@178 $generated@@83))) (=> ($generated@@13 ($generated@@109 $generated@@10 $generated@@32 $generated@@9 $generated@@171 $generated@@178 $generated@@83)) (=> (and (and (= $generated@@179 ($generated@@86 4)) (= $generated@@180 ($generated@@35 $generated@@32 ($generated@@33 $generated@@30) $generated@@176 $generated@@178 ($generated@@34 $generated@@10 $generated@@30 ($generated@@31 $generated@@32 ($generated@@33 $generated@@30) $generated@@176 $generated@@178) $generated@@83 ($generated@@156 $generated@@10 ($generated@@14 $generated@@179)))))) (and ($generated@@91 $generated@@180) (= (ControlFlow 0 2) (- 0 1)))) ($generated@@13 ($generated@@88 $generated@@9 ($generated@@12 false)))))))))))))) +(let (($generated@@185 (=> (and ($generated@@91 $generated@@172) ($generated@@177 $generated@@172)) (=> (and (and (=> $generated@@173 (and ($generated@@77 $generated@@32 $generated@@181 $generated@@80) ($generated@@72 $generated@@32 $generated@@181 $generated@@80 $generated@@172))) true) (and (= 0 $generated@@182) (= (ControlFlow 0 6) 2))) $generated@@183)))) +$generated@@185))) +)) +(check-sat) +(get-info :reason-unknown) +(assert (not (= (ControlFlow 0 2) (- 1)))) +(check-sat) +(pop 1) +; Invalid +(get-info :rlimit) +(reset) +(set-option :rlimit 0) +; did a full reset +(reset) +(set-option :print-success false) +(set-info :smt-lib-version 2.6) +(set-option :auto_config false) +(set-option :type_check true) +(set-option :smt.qi.eager_threshold 100) +(set-option :smt.delay_units true) +(set-option :smt.case_split 3) +(set-option :smt.arith.solver 2) +(set-option :smt.mbqi false) +(set-option :model.compact false) +(set-option :model.v2 true) +(set-option :pp.bv_literals false) +; done setting options + + +(set-info :category "industrial") +(declare-sort |T@U| 0) +(declare-sort |T@T| 0) +(declare-fun real_pow (Real Real) Real) +(declare-fun UOrdering2 (|T@U| |T@U|) Bool) +(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool) +(declare-fun tickleBool (Bool) Bool) +(assert (and (tickleBool true) (tickleBool false))) +(declare-fun $generated () T@U) +(declare-fun $generated@@0 () T@U) +(declare-fun $generated@@1 () T@U) +(declare-fun $generated@@2 () T@U) +(declare-fun $generated@@3 () T@U) +(declare-fun $generated@@4 () T@U) +(declare-fun $generated@@5 () T@U) +(declare-fun $generated@@6 () T@U) +(declare-fun $generated@@7 () T@U) +(declare-fun $generated@@8 () T@U) +(declare-fun $generated@@9 () T@U) +(declare-fun $generated@@10 () T@U) +(declare-fun $generated@@11 () T@U) +(declare-fun $generated@@12 () T@U) +(declare-fun $generated@@13 () T@U) +(declare-fun $generated@@14 () T@U) +(declare-fun $generated@@15 (T@T) Int) +(declare-fun $generated@@16 () T@T) +(declare-fun $generated@@17 () T@T) +(declare-fun $generated@@18 () T@T) +(declare-fun $generated@@19 (Bool) T@U) +(declare-fun $generated@@20 (T@U) Bool) +(declare-fun $generated@@21 (Int) T@U) +(declare-fun $generated@@22 (T@U) Int) +(declare-fun $generated@@23 (Real) T@U) +(declare-fun $generated@@24 (T@U) Real) +(declare-fun $generated@@31 (T@T T@U) Int) +(declare-fun $generated@@32 (T@U) T@U) +(declare-fun $generated@@33 (T@T T@U) T@U) +(declare-fun $generated@@34 (T@T T@U T@U T@U) Bool) +(declare-fun $generated@@35 () T@U) +(declare-fun $generated@@38 () T@T) +(declare-fun $generated@@39 () T@U) +(declare-fun $generated@@40 () T@U) +(declare-fun $generated@@41 (T@T T@U) T@U) +(declare-fun $generated@@42 (T@T T@T T@U T@U) T@U) +(declare-fun $generated@@43 () T@T) +(declare-fun $generated@@44 (T@T T@T T@U T@U) T@U) +(declare-fun $generated@@45 (T@T) T@T) +(declare-fun $generated@@46 (T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@47 (T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@48 (T@T) T@T) +(declare-fun $generated@@83 () T@U) +(declare-fun $generated@@86 (T@T T@U T@U) Bool) +(declare-fun $generated@@87 (T@U) T@U) +(declare-fun $generated@@90 () T@U) +(declare-fun $generated@@93 () T@U) +(declare-fun $generated@@96 () T@U) +(declare-fun $generated@@97 (T@T T@U T@U) T@U) +(declare-fun $generated@@98 (T@T T@U) Bool) +(declare-fun $generated@@99 () T@U) +(declare-fun $generated@@100 () Int) +(declare-fun $generated@@101 (T@U Int T@U) Int) +(declare-fun $generated@@102 (T@U Int T@U) Bool) +(declare-fun $generated@@103 (T@U) Bool) +(declare-fun $generated@@104 (Int) Int) +(declare-fun $generated@@109 (T@T T@U) T@U) +(declare-fun $generated@@119 (T@T T@U T@U) Bool) +(declare-fun $generated@@129 (T@T T@U T@U) T@U) +(declare-fun $generated@@138 (T@T T@U) T@U) +(declare-fun $generated@@147 (T@T T@U) T@U) +(declare-fun $generated@@150 (T@T) T@U) +(declare-fun $generated@@153 (T@T T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@154 (T@U T@U T@U T@U T@U) T@U) +(declare-fun $generated@@155 (T@T T@T T@T T@U T@U T@U T@U) T@U) +(declare-fun $generated@@201 (T@T T@U T@U) Bool) +(declare-fun $generated@@206 (T@U) T@U) +(assert (and (and (and (and (and (and (and (and (= ($generated@@15 $generated@@16) 0) (= ($generated@@15 $generated@@17) 1)) (= ($generated@@15 $generated@@18) 2)) (forall (($generated@@25 Bool) ) (! (= ($generated@@20 ($generated@@19 $generated@@25)) $generated@@25) + :pattern ( ($generated@@19 $generated@@25)) +))) (forall (($generated@@26 T@U) ) (! (= ($generated@@19 ($generated@@20 $generated@@26)) $generated@@26) + :pattern ( ($generated@@20 $generated@@26)) +))) (forall (($generated@@27 Int) ) (! (= ($generated@@22 ($generated@@21 $generated@@27)) $generated@@27) + :pattern ( ($generated@@21 $generated@@27)) +))) (forall (($generated@@28 T@U) ) (! (= ($generated@@21 ($generated@@22 $generated@@28)) $generated@@28) + :pattern ( ($generated@@22 $generated@@28)) +))) (forall (($generated@@29 Real) ) (! (= ($generated@@24 ($generated@@23 $generated@@29)) $generated@@29) + :pattern ( ($generated@@23 $generated@@29)) +))) (forall (($generated@@30 T@U) ) (! (= ($generated@@23 ($generated@@24 $generated@@30)) $generated@@30) + :pattern ( ($generated@@24 $generated@@30)) +)))) +(assert (distinct $generated $generated@@0 $generated@@1 $generated@@2 $generated@@3 $generated@@4 $generated@@5 $generated@@6 $generated@@7 $generated@@8 $generated@@9 $generated@@10 $generated@@11 $generated@@12 $generated@@13 $generated@@14) +) +(assert (= ($generated@@31 $generated@@16 $generated@@1) 0)) +(assert (= ($generated@@32 $generated) $generated@@0)) +(assert (= ($generated@@33 $generated@@16 $generated@@1) $generated@@2)) +(assert (forall (($generated@@36 T@U) ($generated@@37 T@U) ) (! ($generated@@34 $generated@@17 $generated@@36 $generated@@35 $generated@@37) + :pattern ( ($generated@@34 $generated@@17 $generated@@36 $generated@@35 $generated@@37)) +))) +(assert (and (and (and (and (and (and (and (= ($generated@@15 $generated@@38) 3) (forall (($generated@@49 T@T) ($generated@@50 T@T) ($generated@@51 T@U) ($generated@@52 T@U) ($generated@@53 T@U) ) (! (= ($generated@@42 $generated@@49 $generated@@50 ($generated@@46 $generated@@49 $generated@@50 $generated@@52 $generated@@53 $generated@@51) $generated@@53) $generated@@51) + :weight 0 +))) (and (forall (($generated@@54 T@T) ($generated@@55 T@T) ($generated@@56 T@T) ($generated@@57 T@U) ($generated@@58 T@U) ($generated@@59 T@U) ($generated@@60 T@U) ) (! (or (= $generated@@55 $generated@@56) (= ($generated@@42 $generated@@56 $generated@@54 ($generated@@46 $generated@@55 $generated@@54 $generated@@58 $generated@@59 $generated@@57) $generated@@60) ($generated@@42 $generated@@56 $generated@@54 $generated@@58 $generated@@60))) + :weight 0 +)) (forall (($generated@@61 T@T) ($generated@@62 T@T) ($generated@@63 T@T) ($generated@@64 T@U) ($generated@@65 T@U) ($generated@@66 T@U) ($generated@@67 T@U) ) (! (or (= $generated@@66 $generated@@67) (= ($generated@@42 $generated@@63 $generated@@61 ($generated@@46 $generated@@62 $generated@@61 $generated@@65 $generated@@66 $generated@@64) $generated@@67) ($generated@@42 $generated@@63 $generated@@61 $generated@@65 $generated@@67))) + :weight 0 +)))) (= ($generated@@15 $generated@@43) 4)) (forall (($generated@@68 T@T) ($generated@@69 T@T) ($generated@@70 T@U) ($generated@@71 T@U) ($generated@@72 T@U) ) (! (= ($generated@@44 $generated@@68 $generated@@69 ($generated@@47 $generated@@68 $generated@@69 $generated@@71 $generated@@72 $generated@@70) $generated@@72) $generated@@70) + :weight 0 +))) (forall (($generated@@73 T@T) ($generated@@74 T@T) ($generated@@75 T@U) ($generated@@76 T@U) ($generated@@77 T@U) ($generated@@78 T@U) ) (! (or (= $generated@@77 $generated@@78) (= ($generated@@44 $generated@@73 $generated@@74 ($generated@@47 $generated@@73 $generated@@74 $generated@@76 $generated@@77 $generated@@75) $generated@@78) ($generated@@44 $generated@@73 $generated@@74 $generated@@76 $generated@@78))) + :weight 0 +))) (forall (($generated@@79 T@T) ) (= ($generated@@15 ($generated@@45 $generated@@79)) 5))) (forall (($generated@@80 T@T) ) (! (= ($generated@@48 ($generated@@45 $generated@@80)) $generated@@80) + :pattern ( ($generated@@45 $generated@@80)) +)))) +(assert (forall (($generated@@81 T@U) ($generated@@82 T@U) ) (! (= ($generated@@34 $generated@@38 $generated@@81 $generated@@39 $generated@@82) (or (= $generated@@81 $generated@@40) ($generated@@20 ($generated@@41 $generated@@16 ($generated@@42 $generated@@16 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@82 $generated@@81) $generated@@1))))) + :pattern ( ($generated@@34 $generated@@38 $generated@@81 $generated@@39 $generated@@82)) +))) +(assert (forall (($generated@@84 T@U) ($generated@@85 T@U) ) (! (= ($generated@@34 $generated@@38 $generated@@84 $generated@@83 $generated@@85) (or (= $generated@@84 $generated@@40) ($generated@@20 ($generated@@41 $generated@@16 ($generated@@42 $generated@@16 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@85 $generated@@84) $generated@@1))))) + :pattern ( ($generated@@34 $generated@@38 $generated@@84 $generated@@83 $generated@@85)) +))) +(assert (forall (($generated@@88 T@U) ) (! (= ($generated@@86 $generated@@38 $generated@@88 $generated@@39) (or (= $generated@@88 $generated@@40) (= ($generated@@87 $generated@@88) $generated@@39))) + :pattern ( ($generated@@86 $generated@@38 $generated@@88 $generated@@39)) +))) +(assert (forall (($generated@@89 T@U) ) (! (= ($generated@@86 $generated@@38 $generated@@89 $generated@@83) (or (= $generated@@89 $generated@@40) (= ($generated@@87 $generated@@89) $generated@@83))) + :pattern ( ($generated@@86 $generated@@38 $generated@@89 $generated@@83)) +))) +(assert (forall (($generated@@91 T@U) ($generated@@92 T@U) ) (! (= ($generated@@34 $generated@@38 $generated@@91 $generated@@90 $generated@@92) ($generated@@34 $generated@@38 $generated@@91 $generated@@39 $generated@@92)) + :pattern ( ($generated@@34 $generated@@38 $generated@@91 $generated@@90 $generated@@92)) +))) +(assert (forall (($generated@@94 T@U) ($generated@@95 T@U) ) (! (= ($generated@@34 $generated@@38 $generated@@94 $generated@@93 $generated@@95) ($generated@@34 $generated@@38 $generated@@94 $generated@@83 $generated@@95)) + :pattern ( ($generated@@34 $generated@@38 $generated@@94 $generated@@93 $generated@@95)) +))) +(assert (= ($generated@@31 $generated@@38 $generated@@96) 0)) +(assert (= ($generated@@97 $generated@@38 $generated@@5 $generated@@13) $generated@@96)) +(assert (not ($generated@@98 $generated@@38 $generated@@96))) +(assert (= ($generated@@31 $generated@@17 $generated@@99) 0)) +(assert (= ($generated@@97 $generated@@17 $generated@@8 $generated@@14) $generated@@99)) +(assert (not ($generated@@98 $generated@@17 $generated@@99))) +(assert (=> (<= 1 $generated@@100) (forall (($generated@@105 T@U) ($generated@@106 Int) ($generated@@107 T@U) ) (! (=> (or ($generated@@102 $generated@@105 $generated@@106 $generated@@107) (and (< 1 $generated@@100) (and ($generated@@103 $generated@@105) ($generated@@86 $generated@@38 $generated@@107 $generated@@90)))) (and (= ($generated@@101 $generated@@105 $generated@@106 $generated@@107) ($generated@@22 ($generated@@41 $generated@@17 ($generated@@42 $generated@@17 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@105 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@105 $generated@@107) $generated@@96))) $generated@@99)))) (<= ($generated@@104 0) ($generated@@101 $generated@@105 $generated@@106 $generated@@107)))) + :pattern ( ($generated@@101 $generated@@105 $generated@@106 $generated@@107)) +)))) +(assert (forall (($generated@@108 Int) ) (! (= ($generated@@104 $generated@@108) $generated@@108) + :pattern ( ($generated@@104 $generated@@108)) +))) +(assert (forall (($generated@@110 T@U) ($generated@@111 T@T) ) (! (= ($generated@@109 $generated@@111 $generated@@110) $generated@@110) + :pattern ( ($generated@@109 $generated@@111 $generated@@110)) +))) +(assert (forall (($generated@@112 T@U) ($generated@@113 T@U) ) (! (=> (and (and ($generated@@103 $generated@@112) (and (or (not (= $generated@@113 $generated@@40)) (not true)) (= ($generated@@87 $generated@@113) $generated@@83))) ($generated@@20 ($generated@@41 $generated@@16 ($generated@@42 $generated@@16 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@112 $generated@@113) $generated@@1)))) ($generated@@34 $generated@@17 ($generated@@41 $generated@@17 ($generated@@42 $generated@@17 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@112 $generated@@113) $generated@@99)) $generated $generated@@112)) + :pattern ( ($generated@@41 $generated@@17 ($generated@@42 $generated@@17 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@112 $generated@@113) $generated@@99))) +))) +(assert (forall (($generated@@114 T@U) ) (! (= ($generated@@86 $generated@@17 $generated@@114 $generated@@35) (<= ($generated@@104 0) ($generated@@22 $generated@@114))) + :pattern ( ($generated@@86 $generated@@17 $generated@@114 $generated@@35)) +))) +(assert (forall (($generated@@115 T@U) ($generated@@116 T@U) ) (! (=> (and (and ($generated@@103 $generated@@115) (and (or (not (= $generated@@116 $generated@@40)) (not true)) (= ($generated@@87 $generated@@116) $generated@@39))) ($generated@@20 ($generated@@41 $generated@@16 ($generated@@42 $generated@@16 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@115 $generated@@116) $generated@@1)))) ($generated@@34 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@115 $generated@@116) $generated@@96)) $generated@@93 $generated@@115)) + :pattern ( ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@115 $generated@@116) $generated@@96))) +))) +(assert ($generated@@98 $generated@@16 $generated@@1)) +(assert (forall (($generated@@117 T@U) ($generated@@118 T@U) ) (! (=> (and ($generated@@103 $generated@@117) (and (or (not (= $generated@@118 $generated@@40)) (not true)) (= ($generated@@87 $generated@@118) $generated@@39))) ($generated@@86 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@117 $generated@@118) $generated@@96)) $generated@@93)) + :pattern ( ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@117 $generated@@118) $generated@@96))) +))) +(assert (forall (($generated@@120 T@U) ($generated@@121 T@U) ($generated@@122 T@T) ) (! (= ($generated@@119 $generated@@122 $generated@@120 $generated@@121) (forall (($generated@@123 T@U) ) (! (= ($generated@@20 ($generated@@44 $generated@@122 $generated@@16 $generated@@120 $generated@@123)) ($generated@@20 ($generated@@44 $generated@@122 $generated@@16 $generated@@121 $generated@@123))) + :pattern ( ($generated@@44 $generated@@122 $generated@@16 $generated@@120 $generated@@123)) + :pattern ( ($generated@@44 $generated@@122 $generated@@16 $generated@@121 $generated@@123)) +))) + :pattern ( ($generated@@119 $generated@@122 $generated@@120 $generated@@121)) +))) +(assert (forall (($generated@@124 T@U) ) (! (= ($generated@@86 $generated@@38 $generated@@124 $generated@@90) (and ($generated@@86 $generated@@38 $generated@@124 $generated@@39) (or (not (= $generated@@124 $generated@@40)) (not true)))) + :pattern ( ($generated@@86 $generated@@38 $generated@@124 $generated@@90)) +))) +(assert (forall (($generated@@125 T@U) ) (! (= ($generated@@86 $generated@@38 $generated@@125 $generated@@93) (and ($generated@@86 $generated@@38 $generated@@125 $generated@@83) (or (not (= $generated@@125 $generated@@40)) (not true)))) + :pattern ( ($generated@@86 $generated@@38 $generated@@125 $generated@@93)) +))) +(assert (forall (($generated@@126 T@U) ($generated@@127 T@U) ($generated@@128 T@T) ) (! (=> ($generated@@119 $generated@@128 $generated@@126 $generated@@127) (= $generated@@126 $generated@@127)) + :pattern ( ($generated@@119 $generated@@128 $generated@@126 $generated@@127)) +))) +(assert (forall (($generated@@130 T@U) ($generated@@131 T@U) ($generated@@132 T@U) ($generated@@133 T@T) ) (! (=> ($generated@@20 ($generated@@44 $generated@@133 $generated@@16 $generated@@130 $generated@@132)) ($generated@@20 ($generated@@44 $generated@@133 $generated@@16 ($generated@@129 $generated@@133 $generated@@130 $generated@@131) $generated@@132))) + :pattern ( ($generated@@129 $generated@@133 $generated@@130 $generated@@131) ($generated@@44 $generated@@133 $generated@@16 $generated@@130 $generated@@132)) +))) +(assert (forall (($generated@@134 T@U) ($generated@@135 T@U) ($generated@@136 T@U) ($generated@@137 T@T) ) (! (= ($generated@@20 ($generated@@44 $generated@@137 $generated@@16 ($generated@@129 $generated@@137 $generated@@134 $generated@@135) $generated@@136)) (or (= $generated@@136 $generated@@135) ($generated@@20 ($generated@@44 $generated@@137 $generated@@16 $generated@@134 $generated@@136)))) + :pattern ( ($generated@@44 $generated@@137 $generated@@16 ($generated@@129 $generated@@137 $generated@@134 $generated@@135) $generated@@136)) +))) +(assert (forall (($generated@@139 T@U) ($generated@@140 T@U) ($generated@@141 T@T) ) (! (and (= ($generated@@138 $generated@@141 ($generated@@97 $generated@@141 $generated@@139 $generated@@140)) $generated@@139) (= ($generated@@33 $generated@@141 ($generated@@97 $generated@@141 $generated@@139 $generated@@140)) $generated@@140)) + :pattern ( ($generated@@97 $generated@@141 $generated@@139 $generated@@140)) +))) +(assert (forall (($generated@@142 T@U) ($generated@@143 T@U) ) (! (=> (and ($generated@@103 $generated@@142) (and (or (not (= $generated@@143 $generated@@40)) (not true)) (= ($generated@@87 $generated@@143) $generated@@83))) ($generated@@86 $generated@@17 ($generated@@41 $generated@@17 ($generated@@42 $generated@@17 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@142 $generated@@143) $generated@@99)) $generated)) + :pattern ( ($generated@@41 $generated@@17 ($generated@@42 $generated@@17 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@142 $generated@@143) $generated@@99))) +))) +(assert (forall (($generated@@144 T@U) ($generated@@145 T@U) ($generated@@146 T@T) ) (! ($generated@@20 ($generated@@44 $generated@@146 $generated@@16 ($generated@@129 $generated@@146 $generated@@144 $generated@@145) $generated@@145)) + :pattern ( ($generated@@129 $generated@@146 $generated@@144 $generated@@145)) +))) +(assert (forall (($generated@@148 T@U) ($generated@@149 T@T) ) (! (= ($generated@@41 $generated@@149 ($generated@@147 $generated@@149 $generated@@148)) $generated@@148) + :pattern ( ($generated@@147 $generated@@149 $generated@@148)) +))) +(assert (forall (($generated@@151 T@U) ($generated@@152 T@T) ) (! (not ($generated@@20 ($generated@@44 $generated@@152 $generated@@16 ($generated@@150 $generated@@152) $generated@@151))) + :pattern ( ($generated@@44 $generated@@152 $generated@@16 ($generated@@150 $generated@@152) $generated@@151)) +))) +(assert (and (forall (($generated@@156 T@T) ($generated@@157 T@T) ($generated@@158 T@T) ($generated@@159 T@U) ($generated@@160 T@U) ($generated@@161 T@U) ($generated@@162 T@U) ) (! (= ($generated@@153 $generated@@156 $generated@@157 $generated@@158 ($generated@@155 $generated@@156 $generated@@157 $generated@@158 $generated@@160 $generated@@161 $generated@@162 $generated@@159) $generated@@161 $generated@@162) $generated@@159) + :weight 0 +)) (and (and (forall (($generated@@163 T@T) ($generated@@164 T@T) ($generated@@165 T@T) ($generated@@166 T@T) ($generated@@167 T@U) ($generated@@168 T@U) ($generated@@169 T@U) ($generated@@170 T@U) ($generated@@171 T@U) ($generated@@172 T@U) ) (! (or (= $generated@@165 $generated@@166) (= ($generated@@153 $generated@@166 $generated@@163 $generated@@164 ($generated@@155 $generated@@165 $generated@@163 $generated@@164 $generated@@168 $generated@@169 $generated@@170 $generated@@167) $generated@@171 $generated@@172) ($generated@@153 $generated@@166 $generated@@163 $generated@@164 $generated@@168 $generated@@171 $generated@@172))) + :weight 0 +)) (forall (($generated@@173 T@T) ($generated@@174 T@T) ($generated@@175 T@T) ($generated@@176 T@T) ($generated@@177 T@U) ($generated@@178 T@U) ($generated@@179 T@U) ($generated@@180 T@U) ($generated@@181 T@U) ($generated@@182 T@U) ) (! (or (= $generated@@179 $generated@@181) (= ($generated@@153 $generated@@176 $generated@@173 $generated@@174 ($generated@@155 $generated@@175 $generated@@173 $generated@@174 $generated@@178 $generated@@179 $generated@@180 $generated@@177) $generated@@181 $generated@@182) ($generated@@153 $generated@@176 $generated@@173 $generated@@174 $generated@@178 $generated@@181 $generated@@182))) + :weight 0 +))) (forall (($generated@@183 T@T) ($generated@@184 T@T) ($generated@@185 T@T) ($generated@@186 T@T) ($generated@@187 T@U) ($generated@@188 T@U) ($generated@@189 T@U) ($generated@@190 T@U) ($generated@@191 T@U) ($generated@@192 T@U) ) (! (or (= $generated@@190 $generated@@192) (= ($generated@@153 $generated@@186 $generated@@183 $generated@@184 ($generated@@155 $generated@@185 $generated@@183 $generated@@184 $generated@@188 $generated@@189 $generated@@190 $generated@@187) $generated@@191 $generated@@192) ($generated@@153 $generated@@186 $generated@@183 $generated@@184 $generated@@188 $generated@@191 $generated@@192))) + :weight 0 +))))) +(assert (forall (($generated@@193 T@U) ($generated@@194 T@U) ($generated@@195 T@U) ($generated@@196 T@U) ($generated@@197 T@U) ($generated@@198 T@U) ($generated@@199 T@U) ($generated@@200 T@T) ) (! (= ($generated@@20 ($generated@@153 $generated@@200 $generated@@38 $generated@@16 ($generated@@154 $generated@@193 $generated@@194 $generated@@195 $generated@@196 $generated@@197) $generated@@198 $generated@@199)) (=> (and (or (not (= $generated@@198 $generated@@193)) (not true)) ($generated@@20 ($generated@@41 $generated@@16 ($generated@@42 $generated@@16 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@194 $generated@@198) $generated@@195)))) (or (= $generated@@198 $generated@@196) (= $generated@@198 $generated@@197)))) + :pattern ( ($generated@@153 $generated@@200 $generated@@38 $generated@@16 ($generated@@154 $generated@@193 $generated@@194 $generated@@195 $generated@@196 $generated@@197) $generated@@198 $generated@@199)) +))) +(assert (forall (($generated@@202 T@U) ($generated@@203 T@U) ($generated@@204 T@T) ) (! (= ($generated@@201 $generated@@204 $generated@@202 $generated@@203) (forall (($generated@@205 T@U) ) (! (=> ($generated@@20 ($generated@@44 $generated@@204 $generated@@16 $generated@@202 $generated@@205)) ($generated@@20 ($generated@@44 $generated@@204 $generated@@16 $generated@@203 $generated@@205))) + :pattern ( ($generated@@44 $generated@@204 $generated@@16 $generated@@202 $generated@@205)) + :pattern ( ($generated@@44 $generated@@204 $generated@@16 $generated@@203 $generated@@205)) +))) + :pattern ( ($generated@@201 $generated@@204 $generated@@202 $generated@@203)) +))) +(assert (= ($generated@@32 $generated@@35) $generated@@3)) +(assert (= ($generated@@206 $generated@@35) $generated@@10)) +(assert (= ($generated@@32 $generated@@90) $generated@@4)) +(assert (= ($generated@@206 $generated@@90) $generated@@11)) +(assert (= ($generated@@32 $generated@@39) $generated@@6)) +(assert (= ($generated@@206 $generated@@39) $generated@@11)) +(assert (= ($generated@@32 $generated@@93) $generated@@7)) +(assert (= ($generated@@206 $generated@@93) $generated@@12)) +(assert (= ($generated@@32 $generated@@83) $generated@@9)) +(assert (= ($generated@@206 $generated@@83) $generated@@12)) +(assert (forall (($generated@@207 Int) ) (! (= ($generated@@147 $generated@@17 ($generated@@21 ($generated@@104 $generated@@207))) ($generated@@109 $generated@@43 ($generated@@147 $generated@@17 ($generated@@21 $generated@@207)))) + :pattern ( ($generated@@147 $generated@@17 ($generated@@21 ($generated@@104 $generated@@207)))) +))) +(assert (forall (($generated@@208 T@U) ($generated@@209 T@T) ) (! (= ($generated@@147 $generated@@209 ($generated@@109 $generated@@209 $generated@@208)) ($generated@@109 $generated@@43 ($generated@@147 $generated@@209 $generated@@208))) + :pattern ( ($generated@@147 $generated@@209 ($generated@@109 $generated@@209 $generated@@208))) +))) +(assert (=> (<= 1 $generated@@100) (forall (($generated@@210 T@U) ($generated@@211 Int) ($generated@@212 T@U) ) (! (=> (or ($generated@@102 $generated@@210 $generated@@211 $generated@@212) (and (< 1 $generated@@100) (and ($generated@@103 $generated@@210) ($generated@@86 $generated@@38 $generated@@212 $generated@@90)))) (= ($generated@@101 $generated@@210 $generated@@211 $generated@@212) ($generated@@104 3))) + :pattern ( ($generated@@101 $generated@@210 $generated@@211 $generated@@212) ($generated@@103 $generated@@210)) +)))) +(assert (forall (($generated@@213 T@U) ($generated@@214 T@U) ) (! ($generated@@34 $generated@@17 $generated@@214 $generated $generated@@213) + :pattern ( ($generated@@34 $generated@@17 $generated@@214 $generated $generated@@213)) +))) +(assert (forall (($generated@@215 T@U) ) (! ($generated@@86 $generated@@17 $generated@@215 $generated) + :pattern ( ($generated@@86 $generated@@17 $generated@@215 $generated)) +))) +(push 1) +(declare-fun ControlFlow (Int Int) Int) +(declare-fun $generated@@216 () T@U) +(declare-fun $generated@@217 () Int) +(declare-fun $generated@@218 () T@U) +(declare-fun $generated@@219 () T@U) +(declare-fun $generated@@220 () Bool) +(declare-fun $generated@@221 (T@U) Bool) +(set-option :timeout 0) +(set-option :rlimit 0) +(assert (not + (=> (= (ControlFlow 0 0) 14) (let (($generated@@222 (=> (= (ControlFlow 0 7) (- 0 6)) (= ($generated@@101 $generated@@216 $generated@@217 $generated@@218) ($generated@@22 ($generated@@41 $generated@@17 ($generated@@42 $generated@@17 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96))) $generated@@99))))))) +(let (($generated@@223 (and (=> (= (ControlFlow 0 8) (- 0 9)) ($generated@@86 $generated@@17 ($generated@@21 ($generated@@104 3)) $generated@@35)) (=> ($generated@@86 $generated@@17 ($generated@@21 ($generated@@104 3)) $generated@@35) (=> (= ($generated@@101 $generated@@216 $generated@@217 $generated@@218) ($generated@@104 3)) (=> (and ($generated@@86 $generated@@17 ($generated@@21 ($generated@@101 $generated@@216 $generated@@217 $generated@@218)) $generated@@35) (= (ControlFlow 0 8) 7)) $generated@@222)))))) +(let (($generated@@224 (=> (<= ($generated@@104 0) ($generated@@101 $generated@@216 $generated@@217 $generated@@218)) (=> (and ($generated@@34 $generated@@17 ($generated@@21 $generated@@217) $generated $generated@@216) ($generated@@34 $generated@@38 $generated@@218 $generated@@90 $generated@@216)) (and (=> (= (ControlFlow 0 2) (- 0 5)) (or (or (<= 0 $generated@@217) (and ($generated@@201 $generated@@43 ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96)))) ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96))))) (not ($generated@@201 $generated@@43 ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96)))) ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96)))))))) (= $generated@@217 $generated@@217))) (=> (or (or (<= 0 $generated@@217) (and ($generated@@201 $generated@@43 ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96)))) ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96))))) (not ($generated@@201 $generated@@43 ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96)))) ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96)))))))) (= $generated@@217 $generated@@217)) (and (=> (= (ControlFlow 0 2) (- 0 4)) (or (and (= $generated@@217 $generated@@217) (= $generated@@218 $generated@@218)) (or (and ($generated@@201 $generated@@43 ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96)))) ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96))))) (not ($generated@@201 $generated@@43 ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96)))) ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96))))))) (and ($generated@@119 $generated@@43 ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96)))) ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96))))) (or (< $generated@@217 $generated@@217) (and (= $generated@@217 $generated@@217) (and (= $generated@@218 $generated@@40) (or (not (= $generated@@218 $generated@@40)) (not true))))))))) (=> (or (and (= $generated@@217 $generated@@217) (= $generated@@218 $generated@@218)) (or (and ($generated@@201 $generated@@43 ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96)))) ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96))))) (not ($generated@@201 $generated@@43 ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96)))) ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96))))))) (and ($generated@@119 $generated@@43 ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96)))) ($generated@@129 $generated@@43 ($generated@@129 $generated@@43 ($generated@@150 $generated@@43) ($generated@@147 $generated@@38 $generated@@218)) ($generated@@147 $generated@@38 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96))))) (or (< $generated@@217 $generated@@217) (and (= $generated@@217 $generated@@217) (and (= $generated@@218 $generated@@40) (or (not (= $generated@@218 $generated@@40)) (not true)))))))) (=> (or (and (= $generated@@217 $generated@@217) (= $generated@@218 $generated@@218)) ($generated@@102 $generated@@216 $generated@@217 $generated@@218)) (and (=> (= (ControlFlow 0 2) (- 0 3)) (or (not (= $generated@@218 $generated@@40)) (not true))) (=> (or (not (= $generated@@218 $generated@@40)) (not true)) (=> (= (ControlFlow 0 2) (- 0 1)) (or (not (= ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96)) $generated@@40)) (not true)))))))))))))) +(let (($generated@@225 (=> (= $generated@@219 ($generated@@154 $generated@@40 $generated@@216 $generated@@1 $generated@@218 ($generated@@41 $generated@@38 ($generated@@42 $generated@@38 $generated@@43 ($generated@@44 $generated@@38 ($generated@@45 $generated@@43) $generated@@216 $generated@@218) $generated@@96)))) (and (=> (= (ControlFlow 0 10) (- 0 13)) (or (not (= $generated@@218 $generated@@40)) (not true))) (=> (or (not (= $generated@@218 $generated@@40)) (not true)) (=> (= $generated@@220 ($generated@@20 ($generated@@153 $generated@@38 $generated@@38 $generated@@16 $generated@@219 $generated@@218 $generated@@96))) (and (=> (= (ControlFlow 0 10) (- 0 12)) $generated@@220) (=> $generated@@220 (and (=> (= (ControlFlow 0 10) (- 0 11)) (or (not (= $generated@@218 $generated@@40)) (not true))) (=> (or (not (= $generated@@218 $generated@@40)) (not true)) (and (=> (= (ControlFlow 0 10) 2) $generated@@224) (=> (= (ControlFlow 0 10) 8) $generated@@223)))))))))))) +(let (($generated@@226 (=> (and (and (and ($generated@@103 $generated@@216) ($generated@@221 $generated@@216)) ($generated@@86 $generated@@38 $generated@@218 $generated@@90)) (and (= 1 $generated@@100) (= (ControlFlow 0 14) 10))) $generated@@225))) +$generated@@226)))))) +)) +(check-sat) +(get-info :reason-unknown) +(assert (not (= (ControlFlow 0 7) (- 6)))) +(check-sat) +(pop 1) +; Invalid +(get-info :rlimit) +(reset) +(set-option :rlimit 0) +; did a full reset +(reset) +(set-option :print-success false) +(set-info :smt-lib-version 2.6) +(set-option :auto_config false) +(set-option :type_check true) +(set-option :smt.qi.eager_threshold 100) +(set-option :smt.delay_units true) +(set-option :smt.case_split 3) +(set-option :smt.arith.solver 2) +(set-option :smt.mbqi false) +(set-option :model.compact false) +(set-option :model.v2 true) +(set-option :pp.bv_literals false) +; done setting options + + +(set-info :category "industrial") +(declare-sort |T@U| 0) +(declare-sort |T@T| 0) +(declare-fun real_pow (Real Real) Real) +(declare-fun UOrdering2 (|T@U| |T@U|) Bool) +(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool) +(declare-fun tickleBool (Bool) Bool) +(assert (and (tickleBool true) (tickleBool false))) +(declare-fun $generated () T@U) +(declare-fun $generated@@0 () T@U) +(declare-fun $generated@@1 () T@U) +(declare-fun $generated@@2 () T@U) +(declare-fun $generated@@3 () T@U) +(declare-fun $generated@@4 () T@U) +(declare-fun $generated@@5 () T@U) +(declare-fun $generated@@6 () T@U) +(declare-fun $generated@@7 () T@U) +(declare-fun $generated@@8 () T@U) +(declare-fun $generated@@9 () T@U) +(declare-fun $generated@@10 () T@U) +(declare-fun $generated@@11 () T@U) +(declare-fun $generated@@12 () T@U) +(declare-fun $generated@@13 () T@U) +(declare-fun $generated@@14 () T@U) +(declare-fun $generated@@15 () T@U) +(declare-fun $generated@@16 () T@U) +(declare-fun $generated@@17 () T@U) +(declare-fun $generated@@18 () T@U) +(declare-fun $generated@@19 () T@U) +(declare-fun $generated@@20 () T@U) +(declare-fun $generated@@21 () T@U) +(declare-fun $generated@@22 (T@T) Int) +(declare-fun $generated@@23 () T@T) +(declare-fun $generated@@24 () T@T) +(declare-fun $generated@@25 () T@T) +(declare-fun $generated@@26 (Bool) T@U) +(declare-fun $generated@@27 (T@U) Bool) +(declare-fun $generated@@28 (Int) T@U) +(declare-fun $generated@@29 (T@U) Int) +(declare-fun $generated@@30 (Real) T@U) +(declare-fun $generated@@31 (T@U) Real) +(declare-fun $generated@@38 (T@T T@U) Int) +(declare-fun $generated@@39 (T@U) T@U) +(declare-fun $generated@@40 (T@T T@U) T@U) +(declare-fun $generated@@41 (T@T T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@42 (T@T T@T) T@T) +(declare-fun $generated@@43 () T@T) +(declare-fun $generated@@44 (T@T) T@T) +(declare-fun $generated@@45 () T@T) +(declare-fun $generated@@46 (T@U) T@U) +(declare-fun $generated@@47 (T@T T@U T@U) Bool) +(declare-fun $generated@@48 (T@T T@T T@T T@U T@U T@U T@U) T@U) +(declare-fun $generated@@49 (T@T T@T T@U T@U) T@U) +(declare-fun $generated@@50 (T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@51 (T@T) T@T) +(declare-fun $generated@@52 (T@T) T@T) +(declare-fun $generated@@53 (T@T T@T T@U T@U) T@U) +(declare-fun $generated@@54 (T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@55 (T@T) T@T) +(declare-fun $generated@@122 (T@U T@U) Bool) +(declare-fun $generated@@123 (T@T T@U) T@U) +(declare-fun $generated@@127 (T@T T@U T@U T@U) Bool) +(declare-fun $generated@@128 () T@U) +(declare-fun $generated@@129 () T@U) +(declare-fun $generated@@132 () T@U) +(declare-fun $generated@@135 () T@U) +(declare-fun $generated@@138 (T@U) Bool) +(declare-fun $generated@@139 (T@U Int T@U) Int) +(declare-fun $generated@@140 (T@U) Bool) +(declare-fun $generated@@141 (T@U Int T@U) Bool) +(declare-fun $generated@@142 (T@T T@U T@U) Bool) +(declare-fun $generated@@143 () T@U) +(declare-fun $generated@@144 () T@U) +(declare-fun $generated@@152 (T@U) T@U) +(declare-fun $generated@@155 () T@T) +(declare-fun $generated@@156 (T@U T@U) T@U) +(declare-fun $generated@@166 () T@U) +(declare-fun $generated@@169 (T@T T@U T@U) T@U) +(declare-fun $generated@@170 (T@T T@U) Bool) +(declare-fun $generated@@171 () T@U) +(declare-fun $generated@@172 () Int) +(declare-fun $generated@@173 (Int) Int) +(declare-fun $generated@@177 (T@U) T@U) +(declare-fun $generated@@182 (T@T T@U) T@U) +(declare-fun $generated@@185 (T@U T@U T@U T@U T@U) T@U) +(declare-fun $generated@@186 () T@U) +(declare-fun $generated@@187 (T@T T@U T@U) Bool) +(declare-fun $generated@@188 (T@T) T@U) +(declare-fun $generated@@196 (Int) T@U) +(declare-fun $generated@@197 (T@T T@U) T@U) +(declare-fun $generated@@201 (T@U) T@U) +(declare-fun $generated@@204 (T@T T@U T@U) T@U) +(declare-fun $generated@@205 () T@T) +(declare-fun $generated@@213 (T@T T@U T@U T@U) Bool) +(declare-fun $generated@@231 (T@U T@U) T@U) +(declare-fun $generated@@236 (T@U T@U) T@U) +(declare-fun $generated@@241 (T@U T@U T@U T@U T@U) T@U) +(declare-fun $generated@@242 (T@U T@U T@U) T@U) +(declare-fun $generated@@257 (T@U T@U T@U T@U T@U) Bool) +(declare-fun $generated@@269 (Bool) T@U) +(declare-fun $generated@@272 (T@U) T@U) +(declare-fun $generated@@298 (T@T T@U) T@U) +(declare-fun $generated@@315 (T@U) T@U) +(declare-fun $generated@@318 (T@U) T@U) +(declare-fun $generated@@321 (T@U) T@U) +(declare-fun $generated@@324 (T@U) T@U) +(declare-fun $generated@@327 (T@U) T@U) +(declare-fun $generated@@330 (T@U) T@U) +(declare-fun $generated@@334 (T@T T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@335 (T@U T@U T@U Bool) T@U) +(declare-fun $generated@@336 (T@T T@T T@T T@U T@U T@U T@U) T@U) +(declare-fun $generated@@381 (T@U T@U T@U Bool) T@U) +(declare-fun $generated@@389 (T@U) T@U) +(declare-fun $generated@@420 (T@U) T@U) +(declare-fun $generated@@435 (T@U) T@U) +(declare-fun $generated@@494 (T@U) T@U) +(assert (and (and (and (and (and (and (and (and (= ($generated@@22 $generated@@23) 0) (= ($generated@@22 $generated@@24) 1)) (= ($generated@@22 $generated@@25) 2)) (forall (($generated@@32 Bool) ) (! (= ($generated@@27 ($generated@@26 $generated@@32)) $generated@@32) + :pattern ( ($generated@@26 $generated@@32)) +))) (forall (($generated@@33 T@U) ) (! (= ($generated@@26 ($generated@@27 $generated@@33)) $generated@@33) + :pattern ( ($generated@@27 $generated@@33)) +))) (forall (($generated@@34 Int) ) (! (= ($generated@@29 ($generated@@28 $generated@@34)) $generated@@34) + :pattern ( ($generated@@28 $generated@@34)) +))) (forall (($generated@@35 T@U) ) (! (= ($generated@@28 ($generated@@29 $generated@@35)) $generated@@35) + :pattern ( ($generated@@29 $generated@@35)) +))) (forall (($generated@@36 Real) ) (! (= ($generated@@31 ($generated@@30 $generated@@36)) $generated@@36) + :pattern ( ($generated@@30 $generated@@36)) +))) (forall (($generated@@37 T@U) ) (! (= ($generated@@30 ($generated@@31 $generated@@37)) $generated@@37) + :pattern ( ($generated@@31 $generated@@37)) +)))) +(assert (distinct $generated $generated@@0 $generated@@1 $generated@@2 $generated@@3 $generated@@4 $generated@@5 $generated@@6 $generated@@7 $generated@@8 $generated@@9 $generated@@10 $generated@@11 $generated@@12 $generated@@13 $generated@@14 $generated@@15 $generated@@16 $generated@@17 $generated@@18 $generated@@19 $generated@@20 $generated@@21) +) +(assert (= ($generated@@38 $generated@@23 $generated@@2) 0)) +(assert (= ($generated@@39 $generated) $generated@@0)) +(assert (= ($generated@@40 $generated@@23 $generated@@2) $generated@@3)) +(assert (and (and (and (and (and (and (and (and (and (and (and (and (forall (($generated@@56 T@T) ($generated@@57 T@T) ($generated@@58 T@T) ($generated@@59 T@U) ($generated@@60 T@U) ($generated@@61 T@U) ($generated@@62 T@U) ) (! (= ($generated@@41 $generated@@56 $generated@@57 $generated@@58 ($generated@@48 $generated@@56 $generated@@57 $generated@@58 $generated@@60 $generated@@61 $generated@@62 $generated@@59) $generated@@61 $generated@@62) $generated@@59) + :weight 0 +)) (and (forall (($generated@@63 T@T) ($generated@@64 T@T) ($generated@@65 T@T) ($generated@@66 T@U) ($generated@@67 T@U) ($generated@@68 T@U) ($generated@@69 T@U) ($generated@@70 T@U) ($generated@@71 T@U) ) (! (or (= $generated@@68 $generated@@70) (= ($generated@@41 $generated@@63 $generated@@64 $generated@@65 ($generated@@48 $generated@@63 $generated@@64 $generated@@65 $generated@@67 $generated@@68 $generated@@69 $generated@@66) $generated@@70 $generated@@71) ($generated@@41 $generated@@63 $generated@@64 $generated@@65 $generated@@67 $generated@@70 $generated@@71))) + :weight 0 +)) (forall (($generated@@72 T@T) ($generated@@73 T@T) ($generated@@74 T@T) ($generated@@75 T@U) ($generated@@76 T@U) ($generated@@77 T@U) ($generated@@78 T@U) ($generated@@79 T@U) ($generated@@80 T@U) ) (! (or (= $generated@@78 $generated@@80) (= ($generated@@41 $generated@@72 $generated@@73 $generated@@74 ($generated@@48 $generated@@72 $generated@@73 $generated@@74 $generated@@76 $generated@@77 $generated@@78 $generated@@75) $generated@@79 $generated@@80) ($generated@@41 $generated@@72 $generated@@73 $generated@@74 $generated@@76 $generated@@79 $generated@@80))) + :weight 0 +)))) (forall (($generated@@81 T@T) ($generated@@82 T@T) ($generated@@83 T@U) ($generated@@84 T@U) ($generated@@85 T@U) ) (! (= ($generated@@49 $generated@@81 $generated@@82 ($generated@@50 $generated@@81 $generated@@82 $generated@@84 $generated@@85 $generated@@83) $generated@@85) $generated@@83) + :weight 0 +))) (forall (($generated@@86 T@T) ($generated@@87 T@T) ($generated@@88 T@U) ($generated@@89 T@U) ($generated@@90 T@U) ($generated@@91 T@U) ) (! (or (= $generated@@90 $generated@@91) (= ($generated@@49 $generated@@86 $generated@@87 ($generated@@50 $generated@@86 $generated@@87 $generated@@89 $generated@@90 $generated@@88) $generated@@91) ($generated@@49 $generated@@86 $generated@@87 $generated@@89 $generated@@91))) + :weight 0 +))) (forall (($generated@@92 T@T) ($generated@@93 T@T) ) (= ($generated@@22 ($generated@@42 $generated@@92 $generated@@93)) 3))) (forall (($generated@@94 T@T) ($generated@@95 T@T) ) (! (= ($generated@@51 ($generated@@42 $generated@@94 $generated@@95)) $generated@@94) + :pattern ( ($generated@@42 $generated@@94 $generated@@95)) +))) (forall (($generated@@96 T@T) ($generated@@97 T@T) ) (! (= ($generated@@52 ($generated@@42 $generated@@96 $generated@@97)) $generated@@97) + :pattern ( ($generated@@42 $generated@@96 $generated@@97)) +))) (= ($generated@@22 $generated@@43) 4)) (forall (($generated@@98 T@T) ($generated@@99 T@T) ($generated@@100 T@U) ($generated@@101 T@U) ($generated@@102 T@U) ) (! (= ($generated@@53 $generated@@98 $generated@@99 ($generated@@54 $generated@@98 $generated@@99 $generated@@101 $generated@@102 $generated@@100) $generated@@102) $generated@@100) + :weight 0 +))) (and (forall (($generated@@103 T@T) ($generated@@104 T@T) ($generated@@105 T@T) ($generated@@106 T@U) ($generated@@107 T@U) ($generated@@108 T@U) ($generated@@109 T@U) ) (! (or (= $generated@@104 $generated@@105) (= ($generated@@53 $generated@@105 $generated@@103 ($generated@@54 $generated@@104 $generated@@103 $generated@@107 $generated@@108 $generated@@106) $generated@@109) ($generated@@53 $generated@@105 $generated@@103 $generated@@107 $generated@@109))) + :weight 0 +)) (forall (($generated@@110 T@T) ($generated@@111 T@T) ($generated@@112 T@T) ($generated@@113 T@U) ($generated@@114 T@U) ($generated@@115 T@U) ($generated@@116 T@U) ) (! (or (= $generated@@115 $generated@@116) (= ($generated@@53 $generated@@112 $generated@@110 ($generated@@54 $generated@@111 $generated@@110 $generated@@114 $generated@@115 $generated@@113) $generated@@116) ($generated@@53 $generated@@112 $generated@@110 $generated@@114 $generated@@116))) + :weight 0 +)))) (forall (($generated@@117 T@T) ) (= ($generated@@22 ($generated@@44 $generated@@117)) 5))) (forall (($generated@@118 T@T) ) (! (= ($generated@@55 ($generated@@44 $generated@@118)) $generated@@118) + :pattern ( ($generated@@44 $generated@@118)) +))) (= ($generated@@22 $generated@@45) 6))) +(assert (forall (($generated@@119 T@U) ($generated@@120 T@U) ($generated@@121 T@U) ) (! (= ($generated@@27 ($generated@@41 ($generated@@42 $generated@@43 ($generated@@44 $generated@@45)) $generated@@45 $generated@@23 ($generated@@46 $generated@@119) $generated@@120 $generated@@121)) ($generated@@47 $generated@@45 $generated@@121 $generated@@119)) + :pattern ( ($generated@@41 ($generated@@42 $generated@@43 ($generated@@44 $generated@@45)) $generated@@45 $generated@@23 ($generated@@46 $generated@@119) $generated@@120 $generated@@121)) +))) +(assert (forall (($generated@@124 T@U) ($generated@@125 T@U) ) (! (=> ($generated@@122 $generated@@124 $generated@@125) (forall (($generated@@126 T@U) ) (! (=> ($generated@@27 ($generated@@123 $generated@@23 ($generated@@53 $generated@@23 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@124 $generated@@126) $generated@@2))) ($generated@@27 ($generated@@123 $generated@@23 ($generated@@53 $generated@@23 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@125 $generated@@126) $generated@@2)))) + :pattern ( ($generated@@123 $generated@@23 ($generated@@53 $generated@@23 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@125 $generated@@126) $generated@@2))) +))) + :pattern ( ($generated@@122 $generated@@124 $generated@@125)) +))) +(assert (forall (($generated@@130 T@U) ($generated@@131 T@U) ) (! (= ($generated@@127 $generated@@43 $generated@@130 $generated@@128 $generated@@131) (or (= $generated@@130 $generated@@129) ($generated@@27 ($generated@@123 $generated@@23 ($generated@@53 $generated@@23 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@131 $generated@@130) $generated@@2))))) + :pattern ( ($generated@@127 $generated@@43 $generated@@130 $generated@@128 $generated@@131)) +))) +(assert (forall (($generated@@133 T@U) ($generated@@134 T@U) ) (! (= ($generated@@127 $generated@@43 $generated@@133 $generated@@132 $generated@@134) (or (= $generated@@133 $generated@@129) ($generated@@27 ($generated@@123 $generated@@23 ($generated@@53 $generated@@23 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@134 $generated@@133) $generated@@2))))) + :pattern ( ($generated@@127 $generated@@43 $generated@@133 $generated@@132 $generated@@134)) +))) +(assert (forall (($generated@@136 T@U) ($generated@@137 T@U) ) (! (= ($generated@@127 $generated@@43 $generated@@136 $generated@@135 $generated@@137) (or (= $generated@@136 $generated@@129) ($generated@@27 ($generated@@123 $generated@@23 ($generated@@53 $generated@@23 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@137 $generated@@136) $generated@@2))))) + :pattern ( ($generated@@127 $generated@@43 $generated@@136 $generated@@135 $generated@@137)) +))) +(assert (forall (($generated@@145 T@U) ($generated@@146 T@U) ($generated@@147 Int) ($generated@@148 T@U) ) (! (=> (and (and (and ($generated@@140 $generated@@145) ($generated@@140 $generated@@146)) (or ($generated@@141 $generated@@145 $generated@@147 $generated@@148) ($generated@@142 $generated@@43 $generated@@148 $generated@@143))) (and ($generated@@138 $generated@@145) ($generated@@122 $generated@@145 $generated@@146))) (=> (forall (($generated@@149 T@U) ($generated@@150 T@U) ($generated@@151 T@T) ) (=> (and (or (not (= $generated@@149 $generated@@129)) (not true)) (or (= $generated@@149 $generated@@148) (= $generated@@149 ($generated@@123 $generated@@43 ($generated@@53 $generated@@43 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@145 $generated@@148) $generated@@144))))) (= ($generated@@123 $generated@@151 ($generated@@53 $generated@@151 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@145 $generated@@149) $generated@@150)) ($generated@@123 $generated@@151 ($generated@@53 $generated@@151 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@146 $generated@@149) $generated@@150))))) (= ($generated@@139 $generated@@145 $generated@@147 $generated@@148) ($generated@@139 $generated@@146 $generated@@147 $generated@@148)))) + :pattern ( ($generated@@138 $generated@@145) ($generated@@122 $generated@@145 $generated@@146) ($generated@@139 $generated@@146 $generated@@147 $generated@@148)) +))) +(assert (forall (($generated@@153 T@U) ) (! (= ($generated@@142 $generated@@43 $generated@@153 $generated@@132) (or (= $generated@@153 $generated@@129) (= ($generated@@152 $generated@@153) $generated@@132))) + :pattern ( ($generated@@142 $generated@@43 $generated@@153 $generated@@132)) +))) +(assert (forall (($generated@@154 T@U) ) (! (= ($generated@@142 $generated@@43 $generated@@154 $generated@@135) (or (= $generated@@154 $generated@@129) (= ($generated@@152 $generated@@154) $generated@@135))) + :pattern ( ($generated@@142 $generated@@43 $generated@@154 $generated@@135)) +))) +(assert (= ($generated@@22 $generated@@155) 7)) +(assert (forall (($generated@@157 T@U) ($generated@@158 T@U) ($generated@@159 T@U) ($generated@@160 T@U) ($generated@@161 T@U) ) (! (=> (and (and ($generated@@142 $generated@@155 $generated@@157 ($generated@@156 $generated@@158 $generated@@159)) (forall (($generated@@162 T@U) ) (! (=> ($generated@@47 $generated@@45 $generated@@162 $generated@@160) ($generated@@47 $generated@@45 $generated@@162 $generated@@158)) + :pattern ( ($generated@@47 $generated@@45 $generated@@162 $generated@@160)) + :pattern ( ($generated@@47 $generated@@45 $generated@@162 $generated@@158)) +))) (forall (($generated@@163 T@U) ) (! (=> ($generated@@47 $generated@@45 $generated@@163 $generated@@159) ($generated@@47 $generated@@45 $generated@@163 $generated@@161)) + :pattern ( ($generated@@47 $generated@@45 $generated@@163 $generated@@159)) + :pattern ( ($generated@@47 $generated@@45 $generated@@163 $generated@@161)) +))) ($generated@@142 $generated@@155 $generated@@157 ($generated@@156 $generated@@160 $generated@@161))) + :pattern ( ($generated@@142 $generated@@155 $generated@@157 ($generated@@156 $generated@@158 $generated@@159)) ($generated@@142 $generated@@155 $generated@@157 ($generated@@156 $generated@@160 $generated@@161))) +))) +(assert (forall (($generated@@164 T@U) ($generated@@165 T@U) ) (! (= ($generated@@127 $generated@@43 $generated@@164 $generated@@143 $generated@@165) ($generated@@127 $generated@@43 $generated@@164 $generated@@132 $generated@@165)) + :pattern ( ($generated@@127 $generated@@43 $generated@@164 $generated@@143 $generated@@165)) +))) +(assert (forall (($generated@@167 T@U) ($generated@@168 T@U) ) (! (= ($generated@@127 $generated@@43 $generated@@167 $generated@@166 $generated@@168) ($generated@@127 $generated@@43 $generated@@167 $generated@@135 $generated@@168)) + :pattern ( ($generated@@127 $generated@@43 $generated@@167 $generated@@166 $generated@@168)) +))) +(assert (= ($generated@@38 $generated@@43 $generated@@144) 0)) +(assert (= ($generated@@169 $generated@@43 $generated@@9 $generated@@20) $generated@@144)) +(assert (not ($generated@@170 $generated@@43 $generated@@144))) +(assert (= ($generated@@38 $generated@@24 $generated@@171) 0)) +(assert (= ($generated@@169 $generated@@24 $generated@@12 $generated@@21) $generated@@171)) +(assert (not ($generated@@170 $generated@@24 $generated@@171))) +(assert (=> (<= 1 $generated@@172) (forall (($generated@@174 T@U) ($generated@@175 Int) ($generated@@176 T@U) ) (! (=> (or ($generated@@141 $generated@@174 $generated@@175 $generated@@176) (and (< 1 $generated@@172) (and ($generated@@140 $generated@@174) ($generated@@142 $generated@@43 $generated@@176 $generated@@143)))) (and (= ($generated@@139 $generated@@174 $generated@@175 $generated@@176) ($generated@@29 ($generated@@123 $generated@@24 ($generated@@53 $generated@@24 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@174 ($generated@@123 $generated@@43 ($generated@@53 $generated@@43 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@174 $generated@@176) $generated@@144))) $generated@@171)))) (<= ($generated@@173 0) ($generated@@139 $generated@@174 $generated@@175 $generated@@176)))) + :pattern ( ($generated@@139 $generated@@174 $generated@@175 $generated@@176)) +)))) +(assert (forall (($generated@@178 T@U) ($generated@@179 T@U) ) (! (= ($generated@@142 ($generated@@42 $generated@@45 $generated@@23) $generated@@178 ($generated@@177 $generated@@179)) (forall (($generated@@180 T@U) ) (! (=> ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 $generated@@178 $generated@@180)) ($generated@@47 $generated@@45 $generated@@180 $generated@@179)) + :pattern ( ($generated@@49 $generated@@45 $generated@@23 $generated@@178 $generated@@180)) +))) + :pattern ( ($generated@@142 ($generated@@42 $generated@@45 $generated@@23) $generated@@178 ($generated@@177 $generated@@179))) +))) +(assert (forall (($generated@@181 Int) ) (! (= ($generated@@173 $generated@@181) $generated@@181) + :pattern ( ($generated@@173 $generated@@181)) +))) +(assert (forall (($generated@@183 T@U) ($generated@@184 T@T) ) (! (= ($generated@@182 $generated@@184 $generated@@183) $generated@@183) + :pattern ( ($generated@@182 $generated@@184 $generated@@183)) +))) +(assert (forall (($generated@@189 T@U) ($generated@@190 T@U) ($generated@@191 T@U) ($generated@@192 T@U) ($generated@@193 T@U) ) (! (=> (and ($generated@@140 $generated@@191) (and ($generated@@47 $generated@@45 $generated@@193 $generated@@189) ($generated@@142 $generated@@155 $generated@@192 ($generated@@156 $generated@@189 $generated@@190)))) (= ($generated@@187 $generated@@45 ($generated@@185 $generated@@189 $generated@@190 $generated@@186 $generated@@192 $generated@@193) ($generated@@188 $generated@@45)) ($generated@@187 $generated@@45 ($generated@@185 $generated@@189 $generated@@190 $generated@@191 $generated@@192 $generated@@193) ($generated@@188 $generated@@45)))) + :pattern ( ($generated@@185 $generated@@189 $generated@@190 $generated@@186 $generated@@192 $generated@@193) ($generated@@140 $generated@@191)) + :pattern ( ($generated@@185 $generated@@189 $generated@@190 $generated@@191 $generated@@192 $generated@@193)) +))) +(assert (forall (($generated@@194 T@U) ($generated@@195 T@U) ) (! (=> (and (and ($generated@@140 $generated@@194) (and (or (not (= $generated@@195 $generated@@129)) (not true)) (= ($generated@@152 $generated@@195) $generated@@135))) ($generated@@27 ($generated@@123 $generated@@23 ($generated@@53 $generated@@23 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@194 $generated@@195) $generated@@2)))) ($generated@@127 $generated@@24 ($generated@@123 $generated@@24 ($generated@@53 $generated@@24 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@194 $generated@@195) $generated@@171)) $generated $generated@@194)) + :pattern ( ($generated@@123 $generated@@24 ($generated@@53 $generated@@24 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@194 $generated@@195) $generated@@171))) +))) +(assert (forall (($generated@@198 Int) ($generated@@199 T@U) ($generated@@200 T@U) ) (! (= ($generated@@41 ($generated@@42 $generated@@43 ($generated@@44 $generated@@45)) $generated@@45 $generated@@45 ($generated@@196 $generated@@198) $generated@@199 $generated@@200) ($generated@@197 $generated@@24 ($generated@@28 (+ ($generated@@29 ($generated@@123 $generated@@24 $generated@@200)) $generated@@198)))) + :pattern ( ($generated@@41 ($generated@@42 $generated@@43 ($generated@@44 $generated@@45)) $generated@@45 $generated@@45 ($generated@@196 $generated@@198) $generated@@199 $generated@@200)) +))) +(assert (forall (($generated@@202 T@U) ($generated@@203 T@U) ) (! (= ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@201 $generated@@202) $generated@@203)) ($generated@@27 ($generated@@49 $generated@@43 $generated@@23 $generated@@202 ($generated@@123 $generated@@43 $generated@@203)))) + :pattern ( ($generated@@49 $generated@@45 $generated@@23 ($generated@@201 $generated@@202) $generated@@203)) +))) +(assert (= ($generated@@22 $generated@@205) 8)) +(assert (forall (($generated@@206 T@U) ($generated@@207 T@U) ($generated@@208 T@T) ) (! (= ($generated@@204 $generated@@208 $generated@@206 $generated@@207) ($generated@@49 $generated@@205 $generated@@208 $generated@@206 $generated@@207)) + :pattern ( ($generated@@204 $generated@@208 $generated@@206 $generated@@207)) +))) +(assert (forall (($generated@@209 T@U) ($generated@@210 T@U) ) (! (=> (and (and ($generated@@140 $generated@@209) (and (or (not (= $generated@@210 $generated@@129)) (not true)) (= ($generated@@152 $generated@@210) $generated@@132))) ($generated@@27 ($generated@@123 $generated@@23 ($generated@@53 $generated@@23 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@209 $generated@@210) $generated@@2)))) ($generated@@127 $generated@@43 ($generated@@123 $generated@@43 ($generated@@53 $generated@@43 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@209 $generated@@210) $generated@@144)) $generated@@166 $generated@@209)) + :pattern ( ($generated@@123 $generated@@43 ($generated@@53 $generated@@43 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@209 $generated@@210) $generated@@144))) +))) +(assert ($generated@@170 $generated@@23 $generated@@2)) +(assert ($generated@@140 $generated@@186)) +(assert (forall (($generated@@211 T@U) ($generated@@212 T@U) ) (! (=> (and ($generated@@140 $generated@@211) (and (or (not (= $generated@@212 $generated@@129)) (not true)) (= ($generated@@152 $generated@@212) $generated@@132))) ($generated@@142 $generated@@43 ($generated@@123 $generated@@43 ($generated@@53 $generated@@43 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@211 $generated@@212) $generated@@144)) $generated@@166)) + :pattern ( ($generated@@123 $generated@@43 ($generated@@53 $generated@@43 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@211 $generated@@212) $generated@@144))) +))) +(assert (forall (($generated@@214 T@U) ($generated@@215 T@U) ($generated@@216 T@U) ($generated@@217 T@T) ) (! (= ($generated@@213 $generated@@45 ($generated@@197 $generated@@217 $generated@@214) $generated@@215 $generated@@216) ($generated@@127 $generated@@217 $generated@@214 $generated@@215 $generated@@216)) + :pattern ( ($generated@@213 $generated@@45 ($generated@@197 $generated@@217 $generated@@214) $generated@@215 $generated@@216)) +))) +(assert (forall (($generated@@218 T@U) ($generated@@219 T@U) ($generated@@220 T@U) ($generated@@221 T@U) ) (! (=> ($generated@@122 $generated@@218 $generated@@219) (=> ($generated@@213 $generated@@45 $generated@@220 $generated@@221 $generated@@218) ($generated@@213 $generated@@45 $generated@@220 $generated@@221 $generated@@219))) + :pattern ( ($generated@@122 $generated@@218 $generated@@219) ($generated@@213 $generated@@45 $generated@@220 $generated@@221 $generated@@218)) +))) +(assert (forall (($generated@@222 T@U) ($generated@@223 T@U) ($generated@@224 T@U) ($generated@@225 T@U) ($generated@@226 T@T) ) (! (=> ($generated@@122 $generated@@222 $generated@@223) (=> ($generated@@127 $generated@@226 $generated@@224 $generated@@225 $generated@@222) ($generated@@127 $generated@@226 $generated@@224 $generated@@225 $generated@@223))) + :pattern ( ($generated@@122 $generated@@222 $generated@@223) ($generated@@127 $generated@@226 $generated@@224 $generated@@225 $generated@@222)) +))) +(assert (forall (($generated@@227 T@U) ($generated@@228 T@U) ($generated@@229 T@T) ) (! (= ($generated@@187 $generated@@229 $generated@@227 $generated@@228) (forall (($generated@@230 T@U) ) (! (= ($generated@@27 ($generated@@49 $generated@@229 $generated@@23 $generated@@227 $generated@@230)) ($generated@@27 ($generated@@49 $generated@@229 $generated@@23 $generated@@228 $generated@@230))) + :pattern ( ($generated@@49 $generated@@229 $generated@@23 $generated@@227 $generated@@230)) + :pattern ( ($generated@@49 $generated@@229 $generated@@23 $generated@@228 $generated@@230)) +))) + :pattern ( ($generated@@187 $generated@@229 $generated@@227 $generated@@228)) +))) +(assert (forall (($generated@@232 T@U) ($generated@@233 T@U) ($generated@@234 T@U) ($generated@@235 T@U) ) (! (= ($generated@@127 $generated@@155 $generated@@234 ($generated@@231 $generated@@232 $generated@@233) $generated@@235) ($generated@@127 $generated@@155 $generated@@234 ($generated@@156 $generated@@232 $generated@@233) $generated@@235)) + :pattern ( ($generated@@127 $generated@@155 $generated@@234 ($generated@@231 $generated@@232 $generated@@233) $generated@@235)) +))) +(assert (forall (($generated@@237 T@U) ($generated@@238 T@U) ($generated@@239 T@U) ($generated@@240 T@U) ) (! (= ($generated@@127 $generated@@155 $generated@@239 ($generated@@236 $generated@@237 $generated@@238) $generated@@240) ($generated@@127 $generated@@155 $generated@@239 ($generated@@231 $generated@@237 $generated@@238) $generated@@240)) + :pattern ( ($generated@@127 $generated@@155 $generated@@239 ($generated@@236 $generated@@237 $generated@@238) $generated@@240)) +))) +(assert (forall (($generated@@243 T@U) ($generated@@244 T@U) ($generated@@245 T@U) ($generated@@246 T@U) ($generated@@247 T@U) ($generated@@248 T@U) ($generated@@249 T@U) ) (! (= ($generated@@241 $generated@@243 $generated@@244 $generated@@245 ($generated@@242 $generated@@246 $generated@@247 $generated@@248) $generated@@249) ($generated@@41 ($generated@@42 $generated@@43 ($generated@@44 $generated@@45)) $generated@@45 $generated@@45 $generated@@246 $generated@@245 $generated@@249)) + :pattern ( ($generated@@241 $generated@@243 $generated@@244 $generated@@245 ($generated@@242 $generated@@246 $generated@@247 $generated@@248) $generated@@249)) +))) +(assert (forall (($generated@@250 T@U) ) (! (=> ($generated@@47 $generated@@45 $generated@@250 $generated@@128) (and (= ($generated@@197 $generated@@43 ($generated@@123 $generated@@43 $generated@@250)) $generated@@250) ($generated@@142 $generated@@43 ($generated@@123 $generated@@43 $generated@@250) $generated@@128))) + :pattern ( ($generated@@47 $generated@@45 $generated@@250 $generated@@128)) +))) +(assert (forall (($generated@@251 T@U) ) (! (=> ($generated@@47 $generated@@45 $generated@@251 $generated@@143) (and (= ($generated@@197 $generated@@43 ($generated@@123 $generated@@43 $generated@@251)) $generated@@251) ($generated@@142 $generated@@43 ($generated@@123 $generated@@43 $generated@@251) $generated@@143))) + :pattern ( ($generated@@47 $generated@@45 $generated@@251 $generated@@143)) +))) +(assert (forall (($generated@@252 T@U) ) (! (=> ($generated@@47 $generated@@45 $generated@@252 $generated@@132) (and (= ($generated@@197 $generated@@43 ($generated@@123 $generated@@43 $generated@@252)) $generated@@252) ($generated@@142 $generated@@43 ($generated@@123 $generated@@43 $generated@@252) $generated@@132))) + :pattern ( ($generated@@47 $generated@@45 $generated@@252 $generated@@132)) +))) +(assert (forall (($generated@@253 T@U) ) (! (=> ($generated@@47 $generated@@45 $generated@@253 $generated@@166) (and (= ($generated@@197 $generated@@43 ($generated@@123 $generated@@43 $generated@@253)) $generated@@253) ($generated@@142 $generated@@43 ($generated@@123 $generated@@43 $generated@@253) $generated@@166))) + :pattern ( ($generated@@47 $generated@@45 $generated@@253 $generated@@166)) +))) +(assert (forall (($generated@@254 T@U) ) (! (=> ($generated@@47 $generated@@45 $generated@@254 $generated@@135) (and (= ($generated@@197 $generated@@43 ($generated@@123 $generated@@43 $generated@@254)) $generated@@254) ($generated@@142 $generated@@43 ($generated@@123 $generated@@43 $generated@@254) $generated@@135))) + :pattern ( ($generated@@47 $generated@@45 $generated@@254 $generated@@135)) +))) +(assert (forall (($generated@@255 T@U) ) (! (= ($generated@@142 $generated@@43 $generated@@255 $generated@@143) (and ($generated@@142 $generated@@43 $generated@@255 $generated@@132) (or (not (= $generated@@255 $generated@@129)) (not true)))) + :pattern ( ($generated@@142 $generated@@43 $generated@@255 $generated@@143)) +))) +(assert (forall (($generated@@256 T@U) ) (! (= ($generated@@142 $generated@@43 $generated@@256 $generated@@166) (and ($generated@@142 $generated@@43 $generated@@256 $generated@@135) (or (not (= $generated@@256 $generated@@129)) (not true)))) + :pattern ( ($generated@@142 $generated@@43 $generated@@256 $generated@@166)) +))) +(assert (forall (($generated@@258 T@U) ($generated@@259 T@U) ($generated@@260 T@U) ($generated@@261 T@U) ) (! (=> (and ($generated@@140 $generated@@261) ($generated@@127 $generated@@155 $generated@@258 ($generated@@156 $generated@@259 $generated@@260) $generated@@261)) (forall (($generated@@262 T@U) ) (! (=> (and ($generated@@213 $generated@@45 $generated@@262 $generated@@259 $generated@@261) ($generated@@257 $generated@@259 $generated@@260 $generated@@261 $generated@@258 $generated@@262)) ($generated@@213 $generated@@45 ($generated@@241 $generated@@259 $generated@@260 $generated@@261 $generated@@258 $generated@@262) $generated@@260 $generated@@261)) + :pattern ( ($generated@@241 $generated@@259 $generated@@260 $generated@@261 $generated@@258 $generated@@262)) +))) + :pattern ( ($generated@@127 $generated@@155 $generated@@258 ($generated@@156 $generated@@259 $generated@@260) $generated@@261)) +))) +(assert (forall (($generated@@263 T@U) ($generated@@264 T@U) ($generated@@265 T@U) ($generated@@266 T@U) ) (! (=> ($generated@@140 $generated@@266) (= ($generated@@127 $generated@@155 $generated@@263 ($generated@@156 $generated@@264 $generated@@265) $generated@@266) (forall (($generated@@267 T@U) ) (! (=> (and (and ($generated@@47 $generated@@45 $generated@@267 $generated@@264) ($generated@@213 $generated@@45 $generated@@267 $generated@@264 $generated@@266)) ($generated@@257 $generated@@264 $generated@@265 $generated@@266 $generated@@263 $generated@@267)) (forall (($generated@@268 T@U) ) (! (=> (and (or (not (= $generated@@268 $generated@@129)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@185 $generated@@264 $generated@@265 $generated@@266 $generated@@263 $generated@@267) ($generated@@197 $generated@@43 $generated@@268)))) ($generated@@27 ($generated@@123 $generated@@23 ($generated@@53 $generated@@23 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@266 $generated@@268) $generated@@2)))) + :pattern ( ($generated@@49 $generated@@45 $generated@@23 ($generated@@185 $generated@@264 $generated@@265 $generated@@266 $generated@@263 $generated@@267) ($generated@@197 $generated@@43 $generated@@268))) +))) + :pattern ( ($generated@@241 $generated@@264 $generated@@265 $generated@@266 $generated@@263 $generated@@267)) + :pattern ( ($generated@@185 $generated@@264 $generated@@265 $generated@@266 $generated@@263 $generated@@267)) +)))) + :pattern ( ($generated@@127 $generated@@155 $generated@@263 ($generated@@156 $generated@@264 $generated@@265) $generated@@266)) +))) +(assert (forall (($generated@@270 Bool) ($generated@@271 T@U) ) (! (= ($generated@@27 ($generated@@49 $generated@@43 $generated@@23 ($generated@@269 $generated@@270) $generated@@271)) $generated@@270) + :pattern ( ($generated@@49 $generated@@43 $generated@@23 ($generated@@269 $generated@@270) $generated@@271)) +))) +(assert (forall (($generated@@273 T@U) ($generated@@274 T@U) ) (! (= ($generated@@49 $generated@@205 $generated@@155 ($generated@@272 $generated@@273) $generated@@274) $generated@@273) + :pattern ( ($generated@@49 $generated@@205 $generated@@155 ($generated@@272 $generated@@273) $generated@@274)) +))) +(assert (forall (($generated@@275 T@U) ($generated@@276 T@U) ($generated@@277 T@U) ) (! (= ($generated@@127 ($generated@@42 $generated@@45 $generated@@23) $generated@@275 ($generated@@177 $generated@@276) $generated@@277) (forall (($generated@@278 T@U) ) (! (=> ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 $generated@@275 $generated@@278)) ($generated@@213 $generated@@45 $generated@@278 $generated@@276 $generated@@277)) + :pattern ( ($generated@@49 $generated@@45 $generated@@23 $generated@@275 $generated@@278)) +))) + :pattern ( ($generated@@127 ($generated@@42 $generated@@45 $generated@@23) $generated@@275 ($generated@@177 $generated@@276) $generated@@277)) +))) +(assert (forall (($generated@@279 T@U) ($generated@@280 T@U) ($generated@@281 T@U) ($generated@@282 T@U) ($generated@@283 T@U) ($generated@@284 T@U) ($generated@@285 T@U) ($generated@@286 T@U) ) (! (= ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@185 $generated@@279 $generated@@280 $generated@@281 ($generated@@242 $generated@@282 $generated@@283 $generated@@284) $generated@@285) $generated@@286)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@41 ($generated@@42 $generated@@43 ($generated@@44 $generated@@45)) $generated@@45 ($generated@@42 $generated@@45 $generated@@23) $generated@@284 $generated@@281 $generated@@285) $generated@@286))) + :pattern ( ($generated@@49 $generated@@45 $generated@@23 ($generated@@185 $generated@@279 $generated@@280 $generated@@281 ($generated@@242 $generated@@282 $generated@@283 $generated@@284) $generated@@285) $generated@@286)) +))) +(assert (forall (($generated@@287 T@U) ($generated@@288 T@U) ($generated@@289 T@T) ) (! (=> ($generated@@187 $generated@@289 $generated@@287 $generated@@288) (= $generated@@287 $generated@@288)) + :pattern ( ($generated@@187 $generated@@289 $generated@@287 $generated@@288)) +))) +(assert (forall (($generated@@290 T@U) ($generated@@291 T@U) ($generated@@292 T@U) ) (! (=> (or (not (= $generated@@290 $generated@@292)) (not true)) (=> (and ($generated@@122 $generated@@290 $generated@@291) ($generated@@122 $generated@@291 $generated@@292)) ($generated@@122 $generated@@290 $generated@@292))) + :pattern ( ($generated@@122 $generated@@290 $generated@@291) ($generated@@122 $generated@@291 $generated@@292)) +))) +(assert (forall (($generated@@293 T@U) ($generated@@294 T@U) ($generated@@295 T@U) ) (! (= ($generated@@142 $generated@@155 $generated@@293 ($generated@@156 $generated@@294 $generated@@295)) (forall (($generated@@296 T@U) ($generated@@297 T@U) ) (! (=> (and (and ($generated@@140 $generated@@296) ($generated@@47 $generated@@45 $generated@@297 $generated@@294)) ($generated@@257 $generated@@294 $generated@@295 $generated@@296 $generated@@293 $generated@@297)) ($generated@@47 $generated@@45 ($generated@@241 $generated@@294 $generated@@295 $generated@@296 $generated@@293 $generated@@297) $generated@@295)) + :pattern ( ($generated@@241 $generated@@294 $generated@@295 $generated@@296 $generated@@293 $generated@@297)) +))) + :pattern ( ($generated@@142 $generated@@155 $generated@@293 ($generated@@156 $generated@@294 $generated@@295))) +))) +(assert (forall (($generated@@299 T@U) ($generated@@300 T@U) ($generated@@301 T@T) ) (! (and (= ($generated@@298 $generated@@301 ($generated@@169 $generated@@301 $generated@@299 $generated@@300)) $generated@@299) (= ($generated@@40 $generated@@301 ($generated@@169 $generated@@301 $generated@@299 $generated@@300)) $generated@@300)) + :pattern ( ($generated@@169 $generated@@301 $generated@@299 $generated@@300)) +))) +(assert (forall (($generated@@302 T@U) ) (! (=> ($generated@@47 $generated@@45 $generated@@302 $generated) (and (= ($generated@@197 $generated@@24 ($generated@@123 $generated@@24 $generated@@302)) $generated@@302) ($generated@@142 $generated@@24 ($generated@@123 $generated@@24 $generated@@302) $generated))) + :pattern ( ($generated@@47 $generated@@45 $generated@@302 $generated)) +))) +(assert (forall (($generated@@303 T@U) ($generated@@304 T@U) ($generated@@305 T@T) ) (! (= ($generated@@47 $generated@@45 ($generated@@197 $generated@@305 $generated@@303) $generated@@304) ($generated@@142 $generated@@305 $generated@@303 $generated@@304)) + :pattern ( ($generated@@47 $generated@@45 ($generated@@197 $generated@@305 $generated@@303) $generated@@304)) +))) +(assert (forall (($generated@@306 T@U) ($generated@@307 T@U) ($generated@@308 T@U) ($generated@@309 T@U) ($generated@@310 T@U) ($generated@@311 T@U) ($generated@@312 T@U) ) (! (=> ($generated@@27 ($generated@@41 ($generated@@42 $generated@@43 ($generated@@44 $generated@@45)) $generated@@45 $generated@@23 $generated@@310 $generated@@308 $generated@@312)) ($generated@@257 $generated@@306 $generated@@307 $generated@@308 ($generated@@242 $generated@@309 $generated@@310 $generated@@311) $generated@@312)) + :pattern ( ($generated@@257 $generated@@306 $generated@@307 $generated@@308 ($generated@@242 $generated@@309 $generated@@310 $generated@@311) $generated@@312)) +))) +(assert (forall (($generated@@313 T@U) ($generated@@314 T@U) ) (! (=> (and ($generated@@140 $generated@@313) (and (or (not (= $generated@@314 $generated@@129)) (not true)) (= ($generated@@152 $generated@@314) $generated@@135))) ($generated@@142 $generated@@24 ($generated@@123 $generated@@24 ($generated@@53 $generated@@24 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@313 $generated@@314) $generated@@171)) $generated)) + :pattern ( ($generated@@123 $generated@@24 ($generated@@53 $generated@@24 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@313 $generated@@314) $generated@@171))) +))) +(assert (forall (($generated@@316 T@U) ($generated@@317 T@U) ) (! (= ($generated@@315 ($generated@@156 $generated@@316 $generated@@317)) $generated@@316) + :pattern ( ($generated@@156 $generated@@316 $generated@@317)) +))) +(assert (forall (($generated@@319 T@U) ($generated@@320 T@U) ) (! (= ($generated@@318 ($generated@@156 $generated@@319 $generated@@320)) $generated@@320) + :pattern ( ($generated@@156 $generated@@319 $generated@@320)) +))) +(assert (forall (($generated@@322 T@U) ($generated@@323 T@U) ) (! (= ($generated@@321 ($generated@@231 $generated@@322 $generated@@323)) $generated@@322) + :pattern ( ($generated@@231 $generated@@322 $generated@@323)) +))) +(assert (forall (($generated@@325 T@U) ($generated@@326 T@U) ) (! (= ($generated@@324 ($generated@@231 $generated@@325 $generated@@326)) $generated@@326) + :pattern ( ($generated@@231 $generated@@325 $generated@@326)) +))) +(assert (forall (($generated@@328 T@U) ($generated@@329 T@U) ) (! (= ($generated@@327 ($generated@@236 $generated@@328 $generated@@329)) $generated@@328) + :pattern ( ($generated@@236 $generated@@328 $generated@@329)) +))) +(assert (forall (($generated@@331 T@U) ($generated@@332 T@U) ) (! (= ($generated@@330 ($generated@@236 $generated@@331 $generated@@332)) $generated@@332) + :pattern ( ($generated@@236 $generated@@331 $generated@@332)) +))) +(assert (forall (($generated@@333 T@U) ) (! ($generated@@142 $generated@@43 $generated@@333 $generated@@128) + :pattern ( ($generated@@142 $generated@@43 $generated@@333 $generated@@128)) +))) +(assert (and (forall (($generated@@337 T@T) ($generated@@338 T@T) ($generated@@339 T@T) ($generated@@340 T@U) ($generated@@341 T@U) ($generated@@342 T@U) ($generated@@343 T@U) ) (! (= ($generated@@334 $generated@@337 $generated@@338 $generated@@339 ($generated@@336 $generated@@337 $generated@@338 $generated@@339 $generated@@341 $generated@@342 $generated@@343 $generated@@340) $generated@@342 $generated@@343) $generated@@340) + :weight 0 +)) (and (and (forall (($generated@@344 T@T) ($generated@@345 T@T) ($generated@@346 T@T) ($generated@@347 T@T) ($generated@@348 T@U) ($generated@@349 T@U) ($generated@@350 T@U) ($generated@@351 T@U) ($generated@@352 T@U) ($generated@@353 T@U) ) (! (or (= $generated@@346 $generated@@347) (= ($generated@@334 $generated@@347 $generated@@344 $generated@@345 ($generated@@336 $generated@@346 $generated@@344 $generated@@345 $generated@@349 $generated@@350 $generated@@351 $generated@@348) $generated@@352 $generated@@353) ($generated@@334 $generated@@347 $generated@@344 $generated@@345 $generated@@349 $generated@@352 $generated@@353))) + :weight 0 +)) (forall (($generated@@354 T@T) ($generated@@355 T@T) ($generated@@356 T@T) ($generated@@357 T@T) ($generated@@358 T@U) ($generated@@359 T@U) ($generated@@360 T@U) ($generated@@361 T@U) ($generated@@362 T@U) ($generated@@363 T@U) ) (! (or (= $generated@@360 $generated@@362) (= ($generated@@334 $generated@@357 $generated@@354 $generated@@355 ($generated@@336 $generated@@356 $generated@@354 $generated@@355 $generated@@359 $generated@@360 $generated@@361 $generated@@358) $generated@@362 $generated@@363) ($generated@@334 $generated@@357 $generated@@354 $generated@@355 $generated@@359 $generated@@362 $generated@@363))) + :weight 0 +))) (forall (($generated@@364 T@T) ($generated@@365 T@T) ($generated@@366 T@T) ($generated@@367 T@T) ($generated@@368 T@U) ($generated@@369 T@U) ($generated@@370 T@U) ($generated@@371 T@U) ($generated@@372 T@U) ($generated@@373 T@U) ) (! (or (= $generated@@371 $generated@@373) (= ($generated@@334 $generated@@367 $generated@@364 $generated@@365 ($generated@@336 $generated@@366 $generated@@364 $generated@@365 $generated@@369 $generated@@370 $generated@@371 $generated@@368) $generated@@372 $generated@@373) ($generated@@334 $generated@@367 $generated@@364 $generated@@365 $generated@@369 $generated@@372 $generated@@373))) + :weight 0 +))))) +(assert (forall (($generated@@374 T@U) ($generated@@375 T@U) ($generated@@376 T@U) ($generated@@377 Bool) ($generated@@378 T@U) ($generated@@379 T@U) ($generated@@380 T@T) ) (! (= ($generated@@27 ($generated@@334 $generated@@380 $generated@@43 $generated@@23 ($generated@@335 $generated@@374 $generated@@375 $generated@@376 $generated@@377) $generated@@378 $generated@@379)) (=> (and (or (not (= $generated@@378 $generated@@374)) (not true)) ($generated@@27 ($generated@@123 $generated@@23 ($generated@@53 $generated@@23 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@375 $generated@@378) $generated@@376)))) $generated@@377)) + :pattern ( ($generated@@334 $generated@@380 $generated@@43 $generated@@23 ($generated@@335 $generated@@374 $generated@@375 $generated@@376 $generated@@377) $generated@@378 $generated@@379)) +))) +(assert (forall (($generated@@382 T@U) ($generated@@383 T@U) ($generated@@384 T@U) ($generated@@385 Bool) ($generated@@386 T@U) ($generated@@387 T@U) ($generated@@388 T@T) ) (! (= ($generated@@27 ($generated@@334 $generated@@388 $generated@@43 $generated@@23 ($generated@@381 $generated@@382 $generated@@383 $generated@@384 $generated@@385) $generated@@386 $generated@@387)) (=> (and (or (not (= $generated@@386 $generated@@382)) (not true)) ($generated@@27 ($generated@@123 $generated@@23 ($generated@@53 $generated@@23 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@383 $generated@@386) $generated@@384)))) $generated@@385)) + :pattern ( ($generated@@334 $generated@@388 $generated@@43 $generated@@23 ($generated@@381 $generated@@382 $generated@@383 $generated@@384 $generated@@385) $generated@@386 $generated@@387)) +))) +(assert (forall (($generated@@390 T@U) ) (! (= ($generated@@389 ($generated@@177 $generated@@390)) $generated@@390) + :pattern ( ($generated@@177 $generated@@390)) +))) +(assert (forall (($generated@@391 T@U) ) (! (= ($generated@@39 ($generated@@177 $generated@@391)) $generated@@1) + :pattern ( ($generated@@177 $generated@@391)) +))) +(assert (forall (($generated@@392 T@U) ($generated@@393 T@T) ) (! (= ($generated@@123 $generated@@393 ($generated@@197 $generated@@393 $generated@@392)) $generated@@392) + :pattern ( ($generated@@197 $generated@@393 $generated@@392)) +))) +(assert (forall (($generated@@394 T@U) ($generated@@395 T@U) ($generated@@396 T@U) ($generated@@397 T@U) ($generated@@398 T@U) ($generated@@399 T@U) ) (! (=> (and (and (and ($generated@@122 $generated@@396 $generated@@397) (and ($generated@@140 $generated@@396) ($generated@@140 $generated@@397))) (and ($generated@@47 $generated@@45 $generated@@399 $generated@@394) ($generated@@142 $generated@@155 $generated@@398 ($generated@@156 $generated@@394 $generated@@395)))) (forall (($generated@@400 T@U) ($generated@@401 T@U) ($generated@@402 T@T) ) (=> (and (or (not (= $generated@@400 $generated@@129)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@185 $generated@@394 $generated@@395 $generated@@396 $generated@@398 $generated@@399) ($generated@@197 $generated@@43 $generated@@400)))) (= ($generated@@123 $generated@@402 ($generated@@53 $generated@@402 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@396 $generated@@400) $generated@@401)) ($generated@@123 $generated@@402 ($generated@@53 $generated@@402 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@397 $generated@@400) $generated@@401)))))) (= ($generated@@257 $generated@@394 $generated@@395 $generated@@396 $generated@@398 $generated@@399) ($generated@@257 $generated@@394 $generated@@395 $generated@@397 $generated@@398 $generated@@399))) + :pattern ( ($generated@@122 $generated@@396 $generated@@397) ($generated@@257 $generated@@394 $generated@@395 $generated@@397 $generated@@398 $generated@@399)) +))) +(assert (forall (($generated@@403 T@U) ($generated@@404 T@U) ($generated@@405 T@U) ($generated@@406 T@U) ($generated@@407 T@U) ($generated@@408 T@U) ) (! (=> (and (and (and ($generated@@122 $generated@@405 $generated@@406) (and ($generated@@140 $generated@@405) ($generated@@140 $generated@@406))) (and ($generated@@47 $generated@@45 $generated@@408 $generated@@403) ($generated@@142 $generated@@155 $generated@@407 ($generated@@156 $generated@@403 $generated@@404)))) (forall (($generated@@409 T@U) ($generated@@410 T@U) ($generated@@411 T@T) ) (=> (and (or (not (= $generated@@409 $generated@@129)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@185 $generated@@403 $generated@@404 $generated@@406 $generated@@407 $generated@@408) ($generated@@197 $generated@@43 $generated@@409)))) (= ($generated@@123 $generated@@411 ($generated@@53 $generated@@411 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@405 $generated@@409) $generated@@410)) ($generated@@123 $generated@@411 ($generated@@53 $generated@@411 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@406 $generated@@409) $generated@@410)))))) (= ($generated@@257 $generated@@403 $generated@@404 $generated@@405 $generated@@407 $generated@@408) ($generated@@257 $generated@@403 $generated@@404 $generated@@406 $generated@@407 $generated@@408))) + :pattern ( ($generated@@122 $generated@@405 $generated@@406) ($generated@@257 $generated@@403 $generated@@404 $generated@@406 $generated@@407 $generated@@408)) +))) +(assert (forall (($generated@@412 T@U) ($generated@@413 T@U) ($generated@@414 T@U) ) (! (= ($generated@@142 $generated@@155 $generated@@414 ($generated@@236 $generated@@412 $generated@@413)) (and ($generated@@142 $generated@@155 $generated@@414 ($generated@@231 $generated@@412 $generated@@413)) (forall (($generated@@415 T@U) ) (=> ($generated@@47 $generated@@45 $generated@@415 $generated@@412) ($generated@@257 $generated@@412 $generated@@413 $generated@@186 $generated@@414 $generated@@415))))) + :pattern ( ($generated@@142 $generated@@155 $generated@@414 ($generated@@236 $generated@@412 $generated@@413))) +))) +(assert (forall (($generated@@416 T@U) ($generated@@417 T@U) ($generated@@418 T@U) ) (! (= ($generated@@142 $generated@@155 $generated@@418 ($generated@@231 $generated@@416 $generated@@417)) (and ($generated@@142 $generated@@155 $generated@@418 ($generated@@156 $generated@@416 $generated@@417)) (forall (($generated@@419 T@U) ) (=> ($generated@@47 $generated@@45 $generated@@419 $generated@@416) ($generated@@187 $generated@@45 ($generated@@185 $generated@@416 $generated@@417 $generated@@186 $generated@@418 $generated@@419) ($generated@@188 $generated@@45)))))) + :pattern ( ($generated@@142 $generated@@155 $generated@@418 ($generated@@231 $generated@@416 $generated@@417))) +))) +(assert (forall (($generated@@421 T@U) ($generated@@422 T@U) ($generated@@423 T@T) ) (! (= ($generated@@204 $generated@@423 $generated@@421 ($generated@@420 $generated@@422)) ($generated@@204 $generated@@423 $generated@@421 $generated@@422)) + :pattern ( ($generated@@204 $generated@@423 $generated@@421 ($generated@@420 $generated@@422))) +))) +(assert (forall (($generated@@424 T@U) ($generated@@425 T@U) ($generated@@426 T@U) ) (! (=> ($generated@@47 $generated@@45 $generated@@426 ($generated@@156 $generated@@424 $generated@@425)) (and (= ($generated@@197 $generated@@155 ($generated@@123 $generated@@155 $generated@@426)) $generated@@426) ($generated@@142 $generated@@155 ($generated@@123 $generated@@155 $generated@@426) ($generated@@156 $generated@@424 $generated@@425)))) + :pattern ( ($generated@@47 $generated@@45 $generated@@426 ($generated@@156 $generated@@424 $generated@@425))) +))) +(assert (forall (($generated@@427 T@U) ($generated@@428 T@U) ($generated@@429 T@U) ) (! (=> ($generated@@47 $generated@@45 $generated@@429 ($generated@@231 $generated@@427 $generated@@428)) (and (= ($generated@@197 $generated@@155 ($generated@@123 $generated@@155 $generated@@429)) $generated@@429) ($generated@@142 $generated@@155 ($generated@@123 $generated@@155 $generated@@429) ($generated@@231 $generated@@427 $generated@@428)))) + :pattern ( ($generated@@47 $generated@@45 $generated@@429 ($generated@@231 $generated@@427 $generated@@428))) +))) +(assert (forall (($generated@@430 T@U) ($generated@@431 T@U) ($generated@@432 T@U) ) (! (=> ($generated@@47 $generated@@45 $generated@@432 ($generated@@236 $generated@@430 $generated@@431)) (and (= ($generated@@197 $generated@@155 ($generated@@123 $generated@@155 $generated@@432)) $generated@@432) ($generated@@142 $generated@@155 ($generated@@123 $generated@@155 $generated@@432) ($generated@@236 $generated@@430 $generated@@431)))) + :pattern ( ($generated@@47 $generated@@45 $generated@@432 ($generated@@236 $generated@@430 $generated@@431))) +))) +(assert (forall (($generated@@433 T@U) ($generated@@434 T@T) ) (! (not ($generated@@27 ($generated@@49 $generated@@434 $generated@@23 ($generated@@188 $generated@@434) $generated@@433))) + :pattern ( ($generated@@49 $generated@@434 $generated@@23 ($generated@@188 $generated@@434) $generated@@433)) +))) +(assert (forall (($generated@@436 T@U) ($generated@@437 T@U) ) (! (and (= ($generated@@39 ($generated@@156 $generated@@436 $generated@@437)) $generated@@5) (= ($generated@@435 ($generated@@156 $generated@@436 $generated@@437)) $generated@@15)) + :pattern ( ($generated@@156 $generated@@436 $generated@@437)) +))) +(assert (forall (($generated@@438 T@U) ($generated@@439 T@U) ) (! (and (= ($generated@@39 ($generated@@231 $generated@@438 $generated@@439)) $generated@@6) (= ($generated@@435 ($generated@@231 $generated@@438 $generated@@439)) $generated@@16)) + :pattern ( ($generated@@231 $generated@@438 $generated@@439)) +))) +(assert (forall (($generated@@440 T@U) ($generated@@441 T@U) ) (! (and (= ($generated@@39 ($generated@@236 $generated@@440 $generated@@441)) $generated@@7) (= ($generated@@435 ($generated@@236 $generated@@440 $generated@@441)) $generated@@17)) + :pattern ( ($generated@@236 $generated@@440 $generated@@441)) +))) +(assert (forall (($generated@@442 T@U) ($generated@@443 T@U) ($generated@@444 T@U) ($generated@@445 T@U) ($generated@@446 T@U) ) (! (=> (and (and ($generated@@140 $generated@@444) (and ($generated@@47 $generated@@45 $generated@@446 $generated@@442) ($generated@@142 $generated@@155 $generated@@445 ($generated@@156 $generated@@442 $generated@@443)))) ($generated@@187 $generated@@45 ($generated@@185 $generated@@442 $generated@@443 $generated@@186 $generated@@445 $generated@@446) ($generated@@188 $generated@@45))) (= ($generated@@257 $generated@@442 $generated@@443 $generated@@186 $generated@@445 $generated@@446) ($generated@@257 $generated@@442 $generated@@443 $generated@@444 $generated@@445 $generated@@446))) + :pattern ( ($generated@@257 $generated@@442 $generated@@443 $generated@@186 $generated@@445 $generated@@446) ($generated@@140 $generated@@444)) + :pattern ( ($generated@@257 $generated@@442 $generated@@443 $generated@@444 $generated@@445 $generated@@446)) +))) +(assert (forall (($generated@@447 T@U) ($generated@@448 T@U) ($generated@@449 T@U) ($generated@@450 T@U) ($generated@@451 T@U) ($generated@@452 T@U) ) (! (=> (and (and (and ($generated@@122 $generated@@449 $generated@@450) (and ($generated@@140 $generated@@449) ($generated@@140 $generated@@450))) (and ($generated@@47 $generated@@45 $generated@@452 $generated@@447) ($generated@@142 $generated@@155 $generated@@451 ($generated@@156 $generated@@447 $generated@@448)))) (forall (($generated@@453 T@U) ($generated@@454 T@U) ($generated@@455 T@T) ) (=> (and (or (not (= $generated@@453 $generated@@129)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@185 $generated@@447 $generated@@448 $generated@@449 $generated@@451 $generated@@452) ($generated@@197 $generated@@43 $generated@@453)))) (= ($generated@@123 $generated@@455 ($generated@@53 $generated@@455 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@449 $generated@@453) $generated@@454)) ($generated@@123 $generated@@455 ($generated@@53 $generated@@455 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@450 $generated@@453) $generated@@454)))))) (= ($generated@@185 $generated@@447 $generated@@448 $generated@@449 $generated@@451 $generated@@452) ($generated@@185 $generated@@447 $generated@@448 $generated@@450 $generated@@451 $generated@@452))) + :pattern ( ($generated@@122 $generated@@449 $generated@@450) ($generated@@185 $generated@@447 $generated@@448 $generated@@450 $generated@@451 $generated@@452)) +))) +(assert (forall (($generated@@456 T@U) ($generated@@457 T@U) ($generated@@458 T@U) ($generated@@459 T@U) ($generated@@460 T@U) ($generated@@461 T@U) ) (! (=> (and (and (and ($generated@@122 $generated@@458 $generated@@459) (and ($generated@@140 $generated@@458) ($generated@@140 $generated@@459))) (and ($generated@@47 $generated@@45 $generated@@461 $generated@@456) ($generated@@142 $generated@@155 $generated@@460 ($generated@@156 $generated@@456 $generated@@457)))) (forall (($generated@@462 T@U) ($generated@@463 T@U) ($generated@@464 T@T) ) (=> (and (or (not (= $generated@@462 $generated@@129)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@185 $generated@@456 $generated@@457 $generated@@459 $generated@@460 $generated@@461) ($generated@@197 $generated@@43 $generated@@462)))) (= ($generated@@123 $generated@@464 ($generated@@53 $generated@@464 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@458 $generated@@462) $generated@@463)) ($generated@@123 $generated@@464 ($generated@@53 $generated@@464 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@459 $generated@@462) $generated@@463)))))) (= ($generated@@185 $generated@@456 $generated@@457 $generated@@458 $generated@@460 $generated@@461) ($generated@@185 $generated@@456 $generated@@457 $generated@@459 $generated@@460 $generated@@461))) + :pattern ( ($generated@@122 $generated@@458 $generated@@459) ($generated@@185 $generated@@456 $generated@@457 $generated@@459 $generated@@460 $generated@@461)) +))) +(assert (forall (($generated@@465 T@U) ($generated@@466 T@U) ($generated@@467 T@U) ($generated@@468 T@U) ($generated@@469 T@U) ($generated@@470 T@U) ) (! (=> (and (and (and ($generated@@122 $generated@@467 $generated@@468) (and ($generated@@140 $generated@@467) ($generated@@140 $generated@@468))) (and ($generated@@47 $generated@@45 $generated@@470 $generated@@465) ($generated@@142 $generated@@155 $generated@@469 ($generated@@156 $generated@@465 $generated@@466)))) (forall (($generated@@471 T@U) ($generated@@472 T@U) ($generated@@473 T@T) ) (=> (and (or (not (= $generated@@471 $generated@@129)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@185 $generated@@465 $generated@@466 $generated@@467 $generated@@469 $generated@@470) ($generated@@197 $generated@@43 $generated@@471)))) (= ($generated@@123 $generated@@473 ($generated@@53 $generated@@473 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@467 $generated@@471) $generated@@472)) ($generated@@123 $generated@@473 ($generated@@53 $generated@@473 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@468 $generated@@471) $generated@@472)))))) (= ($generated@@241 $generated@@465 $generated@@466 $generated@@467 $generated@@469 $generated@@470) ($generated@@241 $generated@@465 $generated@@466 $generated@@468 $generated@@469 $generated@@470))) + :pattern ( ($generated@@122 $generated@@467 $generated@@468) ($generated@@241 $generated@@465 $generated@@466 $generated@@468 $generated@@469 $generated@@470)) +))) +(assert (forall (($generated@@474 T@U) ($generated@@475 T@U) ($generated@@476 T@U) ($generated@@477 T@U) ($generated@@478 T@U) ($generated@@479 T@U) ) (! (=> (and (and (and ($generated@@122 $generated@@476 $generated@@477) (and ($generated@@140 $generated@@476) ($generated@@140 $generated@@477))) (and ($generated@@47 $generated@@45 $generated@@479 $generated@@474) ($generated@@142 $generated@@155 $generated@@478 ($generated@@156 $generated@@474 $generated@@475)))) (forall (($generated@@480 T@U) ($generated@@481 T@U) ($generated@@482 T@T) ) (=> (and (or (not (= $generated@@480 $generated@@129)) (not true)) ($generated@@27 ($generated@@49 $generated@@45 $generated@@23 ($generated@@185 $generated@@474 $generated@@475 $generated@@477 $generated@@478 $generated@@479) ($generated@@197 $generated@@43 $generated@@480)))) (= ($generated@@123 $generated@@482 ($generated@@53 $generated@@482 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@476 $generated@@480) $generated@@481)) ($generated@@123 $generated@@482 ($generated@@53 $generated@@482 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@477 $generated@@480) $generated@@481)))))) (= ($generated@@241 $generated@@474 $generated@@475 $generated@@476 $generated@@478 $generated@@479) ($generated@@241 $generated@@474 $generated@@475 $generated@@477 $generated@@478 $generated@@479))) + :pattern ( ($generated@@122 $generated@@476 $generated@@477) ($generated@@241 $generated@@474 $generated@@475 $generated@@477 $generated@@478 $generated@@479)) +))) +(assert (forall (($generated@@483 T@U) ($generated@@484 T@U) ) (! (=> ($generated@@47 $generated@@45 $generated@@483 ($generated@@177 $generated@@484)) (and (= ($generated@@197 ($generated@@42 $generated@@45 $generated@@23) ($generated@@123 ($generated@@42 $generated@@45 $generated@@23) $generated@@483)) $generated@@483) ($generated@@142 ($generated@@42 $generated@@45 $generated@@23) ($generated@@123 ($generated@@42 $generated@@45 $generated@@23) $generated@@483) ($generated@@177 $generated@@484)))) + :pattern ( ($generated@@47 $generated@@45 $generated@@483 ($generated@@177 $generated@@484))) +))) +(assert (= ($generated@@39 $generated@@128) $generated@@4)) +(assert (= ($generated@@435 $generated@@128) $generated@@14)) +(assert (= ($generated@@39 $generated@@143) $generated@@8)) +(assert (= ($generated@@435 $generated@@143) $generated@@18)) +(assert (= ($generated@@39 $generated@@132) $generated@@10)) +(assert (= ($generated@@435 $generated@@132) $generated@@18)) +(assert (= ($generated@@39 $generated@@166) $generated@@11)) +(assert (= ($generated@@435 $generated@@166) $generated@@19)) +(assert (= ($generated@@39 $generated@@135) $generated@@13)) +(assert (= ($generated@@435 $generated@@135) $generated@@19)) +(assert (forall (($generated@@485 T@U) ) (! ($generated@@142 ($generated@@42 $generated@@45 $generated@@23) ($generated@@201 $generated@@485) ($generated@@177 $generated@@128)) + :pattern ( ($generated@@201 $generated@@485)) +))) +(assert (forall (($generated@@486 Int) ) (! (= ($generated@@197 $generated@@24 ($generated@@28 ($generated@@173 $generated@@486))) ($generated@@182 $generated@@45 ($generated@@197 $generated@@24 ($generated@@28 $generated@@486)))) + :pattern ( ($generated@@197 $generated@@24 ($generated@@28 ($generated@@173 $generated@@486)))) +))) +(assert (forall (($generated@@487 T@U) ($generated@@488 T@T) ) (! (= ($generated@@197 $generated@@488 ($generated@@182 $generated@@488 $generated@@487)) ($generated@@182 $generated@@45 ($generated@@197 $generated@@488 $generated@@487))) + :pattern ( ($generated@@197 $generated@@488 ($generated@@182 $generated@@488 $generated@@487))) +))) +(assert (=> (<= 1 $generated@@172) (forall (($generated@@489 T@U) ($generated@@490 Int) ($generated@@491 T@U) ) (! (=> (or ($generated@@141 $generated@@489 $generated@@490 $generated@@491) (and (< 1 $generated@@172) (and ($generated@@140 $generated@@489) ($generated@@142 $generated@@43 $generated@@491 $generated@@143)))) (= ($generated@@139 $generated@@489 $generated@@490 $generated@@491) ($generated@@173 3))) + :pattern ( ($generated@@139 $generated@@489 $generated@@490 $generated@@491) ($generated@@140 $generated@@489)) +)))) +(assert (forall (($generated@@492 T@U) ($generated@@493 T@U) ) (! ($generated@@127 $generated@@24 $generated@@493 $generated $generated@@492) + :pattern ( ($generated@@127 $generated@@24 $generated@@493 $generated $generated@@492)) +))) +(assert (forall (($generated@@495 T@U) ($generated@@496 T@U) ($generated@@497 T@U) ) (! (= ($generated@@41 ($generated@@42 $generated@@43 ($generated@@44 $generated@@45)) $generated@@45 ($generated@@42 $generated@@45 $generated@@23) ($generated@@494 $generated@@495) $generated@@496 $generated@@497) $generated@@495) + :pattern ( ($generated@@41 ($generated@@42 $generated@@43 ($generated@@44 $generated@@45)) $generated@@45 ($generated@@42 $generated@@45 $generated@@23) ($generated@@494 $generated@@495) $generated@@496 $generated@@497)) +))) +(assert (forall (($generated@@498 T@U) ) (! ($generated@@142 $generated@@24 $generated@@498 $generated) + :pattern ( ($generated@@142 $generated@@24 $generated@@498 $generated)) +))) +(push 1) +(declare-fun ControlFlow (Int Int) Int) +(declare-fun $generated@@499 () T@U) +(declare-fun $generated@@500 () T@U) +(declare-fun $generated@@501 () Bool) +(declare-fun $generated@@502 () Int) +(declare-fun $generated@@503 () T@U) +(declare-fun $generated@@504 () T@U) +(declare-fun $generated@@505 () T@U) +(declare-fun $generated@@506 () T@U) +(declare-fun $generated@@507 () T@U) +(declare-fun $generated@@508 () T@U) +(declare-fun $generated@@509 () Int) +(declare-fun $generated@@510 () Bool) +(declare-fun $generated@@511 () T@U) +(declare-fun $generated@@512 () T@U) +(declare-fun $generated@@513 () Bool) +(declare-fun $generated@@514 () T@U) +(set-option :timeout 0) +(set-option :rlimit 0) +(assert (not + (=> (= (ControlFlow 0 0) 9) (let (($generated@@515 true)) +(let (($generated@@516 true)) +(let (($generated@@517 (=> (and ($generated@@140 $generated@@499) (or (= $generated@@500 $generated@@499) ($generated@@122 $generated@@500 $generated@@499))) (and (=> (= (ControlFlow 0 7) 5) $generated@@516) (=> (= (ControlFlow 0 7) 6) $generated@@515))))) +(let (($generated@@518 (=> (= (ControlFlow 0 2) (- 0 1)) (= $generated@@501 (= $generated@@502 ($generated@@173 2)))))) +(let (($generated@@519 (=> (= $generated@@503 ($generated@@182 $generated@@155 ($generated@@204 $generated@@155 ($generated@@272 ($generated@@242 ($generated@@196 1) ($generated@@46 $generated) ($generated@@494 ($generated@@201 ($generated@@269 false))))) ($generated@@420 $generated@@504)))) (=> (and (and (or (not (= $generated@@505 $generated@@129)) (not true)) (and ($generated@@142 $generated@@43 $generated@@505 $generated@@143) ($generated@@127 $generated@@43 $generated@@505 $generated@@143 $generated@@506))) (and ($generated@@140 $generated@@507) ($generated@@138 $generated@@507))) (=> (and (and (and (or (not (= $generated@@508 $generated@@129)) (not true)) (and ($generated@@142 $generated@@43 $generated@@508 $generated@@143) ($generated@@127 $generated@@43 $generated@@508 $generated@@143 $generated@@507))) (not ($generated@@27 ($generated@@123 $generated@@23 ($generated@@53 $generated@@23 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@500 $generated@@508) $generated@@2))))) (and (forall (($generated@@520 T@U) ) (! (=> (and (or (not (= $generated@@520 $generated@@129)) (not true)) ($generated@@27 ($generated@@123 $generated@@23 ($generated@@53 $generated@@23 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@500 $generated@@520) $generated@@2)))) (= ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@507 $generated@@520) ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@500 $generated@@520))) + :pattern ( ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@507 $generated@@520)) +)) ($generated@@122 $generated@@500 $generated@@507))) (and (=> (= (ControlFlow 0 3) (- 0 4)) true) (=> (and (and (and (= $generated@@509 ($generated@@173 42)) ($generated@@127 $generated@@24 ($generated@@28 $generated@@509) $generated $generated@@507)) (and ($generated@@127 $generated@@43 $generated@@508 $generated@@143 $generated@@507) ($generated@@141 $generated@@507 ($generated@@173 42) $generated@@508))) (and (and ($generated@@141 $generated@@507 ($generated@@173 42) $generated@@508) (= $generated@@510 (= $generated@@502 ($generated@@139 $generated@@507 ($generated@@173 42) $generated@@508)))) (and (= $generated@@501 $generated@@510) (= (ControlFlow 0 3) 2)))) $generated@@518))))))) +(let (($generated@@521 (=> (= $generated@@511 ($generated@@335 $generated@@129 $generated@@506 $generated@@2 false)) (=> (and (and (and ($generated@@140 $generated@@500) ($generated@@138 $generated@@500)) ($generated@@27 ($generated@@182 $generated@@23 ($generated@@26 false)))) (and (forall (($generated@@522 T@U) ) (! (=> (and (or (not (= $generated@@522 $generated@@129)) (not true)) ($generated@@27 ($generated@@123 $generated@@23 ($generated@@53 $generated@@23 $generated@@45 ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@506 $generated@@522) $generated@@2)))) (= ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@500 $generated@@522) ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@506 $generated@@522))) + :pattern ( ($generated@@49 $generated@@43 ($generated@@44 $generated@@45) $generated@@500 $generated@@522)) +)) ($generated@@122 $generated@@506 $generated@@500))) (and (=> (= (ControlFlow 0 8) 7) $generated@@517) (=> (= (ControlFlow 0 8) 3) $generated@@519)))))) +(let (($generated@@523 (=> (and ($generated@@140 $generated@@506) ($generated@@138 $generated@@506)) (=> (and (and ($generated@@142 $generated@@155 $generated@@512 ($generated@@236 $generated $generated)) ($generated@@127 $generated@@155 $generated@@512 ($generated@@236 $generated $generated) $generated@@506)) true) (=> (and (and (and (=> $generated@@513 (and ($generated@@142 $generated@@43 $generated@@514 $generated@@143) ($generated@@127 $generated@@43 $generated@@514 $generated@@143 $generated@@506))) true) (= 2 $generated@@172)) (and (= $generated@@502 ($generated@@173 2)) (= (ControlFlow 0 9) 8))) $generated@@521))))) +$generated@@523)))))))) +)) +(check-sat) +(pop 1) +; Valid +(get-info :rlimit) +(reset) +(set-option :rlimit 0) +; did a full reset +(reset) +(set-option :print-success false) +(set-info :smt-lib-version 2.6) +(set-option :auto_config false) +(set-option :type_check true) +(set-option :smt.qi.eager_threshold 100) +(set-option :smt.delay_units true) +(set-option :smt.case_split 3) +(set-option :smt.arith.solver 2) +(set-option :smt.mbqi false) +(set-option :model.compact false) +(set-option :model.v2 true) +(set-option :pp.bv_literals false) +; done setting options + + +(set-info :category "industrial") +(declare-sort |T@U| 0) +(declare-sort |T@T| 0) +(declare-fun real_pow (Real Real) Real) +(declare-fun UOrdering2 (|T@U| |T@U|) Bool) +(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool) +(declare-fun tickleBool (Bool) Bool) +(assert (and (tickleBool true) (tickleBool false))) +(declare-fun $generated () T@U) +(declare-fun $generated@@0 () T@U) +(declare-fun $generated@@1 () T@U) +(declare-fun $generated@@2 () T@U) +(declare-fun $generated@@3 () T@U) +(declare-fun $generated@@4 () T@U) +(declare-fun $generated@@5 () T@U) +(declare-fun $generated@@6 () T@U) +(declare-fun $generated@@7 () T@U) +(declare-fun $generated@@8 () T@U) +(declare-fun $generated@@9 () T@U) +(declare-fun $generated@@10 (T@T) Int) +(declare-fun $generated@@11 () T@T) +(declare-fun $generated@@12 () T@T) +(declare-fun $generated@@13 () T@T) +(declare-fun $generated@@14 (Bool) T@U) +(declare-fun $generated@@15 (T@U) Bool) +(declare-fun $generated@@16 (Int) T@U) +(declare-fun $generated@@17 (T@U) Int) +(declare-fun $generated@@18 (Real) T@U) +(declare-fun $generated@@19 (T@U) Real) +(declare-fun $generated@@26 () Int) +(declare-fun $generated@@27 (T@U T@U T@U) Bool) +(declare-fun $generated@@28 (T@T T@U) T@U) +(declare-fun $generated@@29 () T@T) +(declare-fun $generated@@30 (T@U) Bool) +(declare-fun $generated@@31 (T@U T@U T@U) Bool) +(declare-fun $generated@@32 (T@T T@U T@U) Bool) +(declare-fun $generated@@33 (T@U T@U) T@U) +(declare-fun $generated@@34 (T@T T@U T@U T@U) Bool) +(declare-fun $generated@@35 (T@U T@U T@U T@U T@U) Bool) +(declare-fun $generated@@36 (T@U) T@U) +(declare-fun $generated@@37 (T@T T@T T@U T@U) T@U) +(declare-fun $generated@@38 () T@T) +(declare-fun $generated@@39 (T@U) T@U) +(declare-fun $generated@@40 (T@T T@U T@U) Bool) +(declare-fun $generated@@41 (T@U) Bool) +(declare-fun $generated@@42 (T@T T@T) T@T) +(declare-fun $generated@@43 () T@T) +(declare-fun $generated@@44 (T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@45 (T@T) T@T) +(declare-fun $generated@@46 (T@T) T@T) +(declare-fun $generated@@70 (T@U) T@U) +(declare-fun $generated@@77 (T@U T@U) T@U) +(declare-fun $generated@@85 (T@U T@U) T@U) +(declare-fun $generated@@90 (T@U) T@U) +(declare-fun $generated@@96 (T@U T@U T@U T@U T@U) T@U) +(declare-fun $generated@@97 () T@U) +(declare-fun $generated@@98 (T@T T@U T@U) Bool) +(declare-fun $generated@@99 (T@T) T@U) +(declare-fun $generated@@105 (T@U T@U) T@U) +(declare-fun $generated@@110 (T@U) T@U) +(declare-fun $generated@@120 (T@T T@U T@U T@U) Bool) +(declare-fun $generated@@121 (T@T T@U) T@U) +(declare-fun $generated@@134 (T@U T@U T@U T@U T@U) T@U) +(declare-fun $generated@@140 () T@T) +(declare-fun $generated@@141 () T@U) +(declare-fun $generated@@142 (T@T T@U) T@U) +(declare-fun $generated@@143 (T@T T@T T@U T@U) T@U) +(declare-fun $generated@@144 (T@T) T@T) +(declare-fun $generated@@145 (T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@146 (T@T) T@T) +(declare-fun $generated@@196 (T@U) T@U) +(declare-fun $generated@@199 (T@U) T@U) +(declare-fun $generated@@202 (T@U) T@U) +(declare-fun $generated@@205 (T@U) T@U) +(declare-fun $generated@@210 (T@U) T@U) +(declare-fun $generated@@213 (T@U) T@U) +(declare-fun $generated@@220 (T@T T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@221 (T@U T@U T@U Bool) T@U) +(declare-fun $generated@@222 (T@T T@T T@T T@U T@U T@U T@U) T@U) +(declare-fun $generated@@267 (T@U) T@U) +(declare-fun $generated@@272 (T@U) Int) +(declare-fun $generated@@291 (T@U) T@U) +(assert (and (and (and (and (and (and (and (and (= ($generated@@10 $generated@@11) 0) (= ($generated@@10 $generated@@12) 1)) (= ($generated@@10 $generated@@13) 2)) (forall (($generated@@20 Bool) ) (! (= ($generated@@15 ($generated@@14 $generated@@20)) $generated@@20) + :pattern ( ($generated@@14 $generated@@20)) +))) (forall (($generated@@21 T@U) ) (! (= ($generated@@14 ($generated@@15 $generated@@21)) $generated@@21) + :pattern ( ($generated@@15 $generated@@21)) +))) (forall (($generated@@22 Int) ) (! (= ($generated@@17 ($generated@@16 $generated@@22)) $generated@@22) + :pattern ( ($generated@@16 $generated@@22)) +))) (forall (($generated@@23 T@U) ) (! (= ($generated@@16 ($generated@@17 $generated@@23)) $generated@@23) + :pattern ( ($generated@@17 $generated@@23)) +))) (forall (($generated@@24 Real) ) (! (= ($generated@@19 ($generated@@18 $generated@@24)) $generated@@24) + :pattern ( ($generated@@18 $generated@@24)) +))) (forall (($generated@@25 T@U) ) (! (= ($generated@@18 ($generated@@19 $generated@@25)) $generated@@25) + :pattern ( ($generated@@19 $generated@@25)) +)))) +(assert (distinct $generated $generated@@0 $generated@@1 $generated@@2 $generated@@3 $generated@@4 $generated@@5 $generated@@6 $generated@@7 $generated@@8 $generated@@9) +) +(assert (and (and (and (and (and (and (and (= ($generated@@10 $generated@@29) 3) (forall (($generated@@47 T@T) ($generated@@48 T@T) ($generated@@49 T@U) ($generated@@50 T@U) ($generated@@51 T@U) ) (! (= ($generated@@37 $generated@@47 $generated@@48 ($generated@@44 $generated@@47 $generated@@48 $generated@@50 $generated@@51 $generated@@49) $generated@@51) $generated@@49) + :weight 0 +))) (forall (($generated@@52 T@T) ($generated@@53 T@T) ($generated@@54 T@U) ($generated@@55 T@U) ($generated@@56 T@U) ($generated@@57 T@U) ) (! (or (= $generated@@56 $generated@@57) (= ($generated@@37 $generated@@52 $generated@@53 ($generated@@44 $generated@@52 $generated@@53 $generated@@55 $generated@@56 $generated@@54) $generated@@57) ($generated@@37 $generated@@52 $generated@@53 $generated@@55 $generated@@57))) + :weight 0 +))) (= ($generated@@10 $generated@@38) 4)) (forall (($generated@@58 T@T) ($generated@@59 T@T) ) (= ($generated@@10 ($generated@@42 $generated@@58 $generated@@59)) 5))) (forall (($generated@@60 T@T) ($generated@@61 T@T) ) (! (= ($generated@@45 ($generated@@42 $generated@@60 $generated@@61)) $generated@@60) + :pattern ( ($generated@@42 $generated@@60 $generated@@61)) +))) (forall (($generated@@62 T@T) ($generated@@63 T@T) ) (! (= ($generated@@46 ($generated@@42 $generated@@62 $generated@@63)) $generated@@63) + :pattern ( ($generated@@42 $generated@@62 $generated@@63)) +))) (= ($generated@@10 $generated@@43) 6))) +(assert (=> (<= 0 $generated@@26) (forall (($generated@@64 T@U) ($generated@@65 T@U) ($generated@@66 T@U) ($generated@@67 T@U) ) (! (=> (or ($generated@@31 $generated@@64 $generated@@65 ($generated@@28 $generated@@29 $generated@@67)) (and (< 0 $generated@@26) (and ($generated@@30 $generated@@66) (and ($generated@@32 $generated@@29 $generated@@67 ($generated@@33 $generated@@64 $generated@@65)) ($generated@@34 $generated@@29 $generated@@67 ($generated@@33 $generated@@64 $generated@@65) $generated@@66))))) (and (forall (($generated@@68 T@U) ) (! (=> ($generated@@40 $generated@@38 $generated@@68 $generated@@64) (and ($generated@@41 ($generated@@28 $generated@@29 $generated@@67)) (=> ($generated@@15 ($generated@@37 $generated@@38 $generated@@11 ($generated@@28 ($generated@@42 $generated@@38 $generated@@11) ($generated@@39 ($generated@@28 $generated@@29 $generated@@67))) $generated@@68)) (and ($generated@@41 ($generated@@28 $generated@@29 $generated@@67)) true)))) + :pattern ( ($generated@@35 $generated@@64 $generated@@65 $generated@@66 ($generated@@36 $generated@@67) $generated@@68)) + :pattern ( ($generated@@37 $generated@@38 $generated@@11 ($generated@@39 $generated@@67) $generated@@68)) +)) (= ($generated@@27 $generated@@64 $generated@@65 ($generated@@28 $generated@@29 $generated@@67)) (forall (($generated@@69 T@U) ) (! (=> (and ($generated@@40 $generated@@38 $generated@@69 $generated@@64) ($generated@@15 ($generated@@37 $generated@@38 $generated@@11 ($generated@@28 ($generated@@42 $generated@@38 $generated@@11) ($generated@@39 ($generated@@28 $generated@@29 $generated@@67))) $generated@@69))) ($generated@@35 $generated@@64 $generated@@65 $generated@@66 ($generated@@28 $generated@@43 ($generated@@36 ($generated@@28 $generated@@29 $generated@@67))) $generated@@69)) + :pattern ( ($generated@@35 $generated@@64 $generated@@65 $generated@@66 ($generated@@36 $generated@@67) $generated@@69)) + :pattern ( ($generated@@37 $generated@@38 $generated@@11 ($generated@@39 $generated@@67) $generated@@69)) +))))) + :weight 3 + :pattern ( ($generated@@27 $generated@@64 $generated@@65 ($generated@@28 $generated@@29 $generated@@67)) ($generated@@30 $generated@@66)) +)))) +(assert (= ($generated@@70 $generated) $generated@@0)) +(assert (=> (<= 0 $generated@@26) (forall (($generated@@71 T@U) ($generated@@72 T@U) ($generated@@73 T@U) ) (! (=> (or ($generated@@31 $generated@@71 $generated@@72 $generated@@73) (and (< 0 $generated@@26) ($generated@@32 $generated@@29 $generated@@73 ($generated@@33 $generated@@71 $generated@@72)))) true) + :pattern ( ($generated@@27 $generated@@71 $generated@@72 $generated@@73)) +)))) +(assert (forall (($generated@@74 T@U) ($generated@@75 T@U) ($generated@@76 T@U) ) (! (=> ($generated@@32 $generated@@29 $generated@@76 ($generated@@33 $generated@@74 $generated@@75)) ($generated@@41 $generated@@76)) + :pattern ( ($generated@@41 $generated@@76) ($generated@@32 $generated@@29 $generated@@76 ($generated@@33 $generated@@74 $generated@@75))) +))) +(assert (forall (($generated@@78 T@U) ($generated@@79 T@U) ($generated@@80 T@U) ($generated@@81 T@U) ($generated@@82 T@U) ) (! (=> (and (and ($generated@@32 $generated@@43 $generated@@78 ($generated@@77 $generated@@79 $generated@@80)) (forall (($generated@@83 T@U) ) (! (=> ($generated@@40 $generated@@38 $generated@@83 $generated@@81) ($generated@@40 $generated@@38 $generated@@83 $generated@@79)) + :pattern ( ($generated@@40 $generated@@38 $generated@@83 $generated@@81)) + :pattern ( ($generated@@40 $generated@@38 $generated@@83 $generated@@79)) +))) (forall (($generated@@84 T@U) ) (! (=> ($generated@@40 $generated@@38 $generated@@84 $generated@@80) ($generated@@40 $generated@@38 $generated@@84 $generated@@82)) + :pattern ( ($generated@@40 $generated@@38 $generated@@84 $generated@@80)) + :pattern ( ($generated@@40 $generated@@38 $generated@@84 $generated@@82)) +))) ($generated@@32 $generated@@43 $generated@@78 ($generated@@77 $generated@@81 $generated@@82))) + :pattern ( ($generated@@32 $generated@@43 $generated@@78 ($generated@@77 $generated@@79 $generated@@80)) ($generated@@32 $generated@@43 $generated@@78 ($generated@@77 $generated@@81 $generated@@82))) +))) +(assert (forall (($generated@@86 T@U) ($generated@@87 T@U) ($generated@@88 T@U) ($generated@@89 T@U) ) (! (=> (and ($generated@@30 $generated@@89) (and ($generated@@41 $generated@@86) ($generated@@34 $generated@@29 $generated@@86 ($generated@@33 $generated@@87 $generated@@88) $generated@@89))) ($generated@@34 $generated@@43 ($generated@@36 $generated@@86) ($generated@@85 $generated@@87 $generated@@88) $generated@@89)) + :pattern ( ($generated@@34 $generated@@43 ($generated@@36 $generated@@86) ($generated@@85 $generated@@87 $generated@@88) $generated@@89)) +))) +(assert (forall (($generated@@91 T@U) ($generated@@92 T@U) ) (! (= ($generated@@32 ($generated@@42 $generated@@38 $generated@@11) $generated@@91 ($generated@@90 $generated@@92)) (forall (($generated@@93 T@U) ) (! (=> ($generated@@15 ($generated@@37 $generated@@38 $generated@@11 $generated@@91 $generated@@93)) ($generated@@40 $generated@@38 $generated@@93 $generated@@92)) + :pattern ( ($generated@@37 $generated@@38 $generated@@11 $generated@@91 $generated@@93)) +))) + :pattern ( ($generated@@32 ($generated@@42 $generated@@38 $generated@@11) $generated@@91 ($generated@@90 $generated@@92))) +))) +(assert (forall (($generated@@94 T@U) ($generated@@95 T@T) ) (! (= ($generated@@28 $generated@@95 $generated@@94) $generated@@94) + :pattern ( ($generated@@28 $generated@@95 $generated@@94)) +))) +(assert (forall (($generated@@100 T@U) ($generated@@101 T@U) ($generated@@102 T@U) ($generated@@103 T@U) ($generated@@104 T@U) ) (! (=> (and ($generated@@30 $generated@@102) (and ($generated@@40 $generated@@38 $generated@@104 $generated@@100) ($generated@@32 $generated@@43 $generated@@103 ($generated@@77 $generated@@100 $generated@@101)))) (= ($generated@@98 $generated@@38 ($generated@@96 $generated@@100 $generated@@101 $generated@@97 $generated@@103 $generated@@104) ($generated@@99 $generated@@38)) ($generated@@98 $generated@@38 ($generated@@96 $generated@@100 $generated@@101 $generated@@102 $generated@@103 $generated@@104) ($generated@@99 $generated@@38)))) + :pattern ( ($generated@@96 $generated@@100 $generated@@101 $generated@@97 $generated@@103 $generated@@104) ($generated@@30 $generated@@102)) + :pattern ( ($generated@@96 $generated@@100 $generated@@101 $generated@@102 $generated@@103 $generated@@104)) +))) +(assert (forall (($generated@@106 T@U) ($generated@@107 T@U) ($generated@@108 T@U) ($generated@@109 T@U) ) (! (= ($generated@@32 $generated@@29 ($generated@@105 $generated@@108 $generated@@109) ($generated@@33 $generated@@106 $generated@@107)) (and ($generated@@32 ($generated@@42 $generated@@38 $generated@@11) $generated@@108 ($generated@@90 $generated@@106)) ($generated@@32 $generated@@43 $generated@@109 ($generated@@85 $generated@@106 $generated@@107)))) + :pattern ( ($generated@@32 $generated@@29 ($generated@@105 $generated@@108 $generated@@109) ($generated@@33 $generated@@106 $generated@@107))) +))) +(assert (forall (($generated@@111 T@U) ) (! (= ($generated@@41 $generated@@111) (= ($generated@@110 $generated@@111) $generated@@5)) + :pattern ( ($generated@@41 $generated@@111)) +))) +(assert (forall (($generated@@112 T@U) ) (! (=> ($generated@@41 $generated@@112) (exists (($generated@@113 T@U) ($generated@@114 T@U) ) (= $generated@@112 ($generated@@105 $generated@@113 $generated@@114)))) + :pattern ( ($generated@@41 $generated@@112)) +))) +(assert (forall (($generated@@115 T@U) ($generated@@116 T@U) ($generated@@117 T@U) ($generated@@118 T@U) ($generated@@119 T@U) ) (! (=> ($generated@@30 $generated@@119) (= ($generated@@34 $generated@@29 ($generated@@105 $generated@@117 $generated@@118) ($generated@@33 $generated@@115 $generated@@116) $generated@@119) (and ($generated@@34 ($generated@@42 $generated@@38 $generated@@11) $generated@@117 ($generated@@90 $generated@@115) $generated@@119) ($generated@@34 $generated@@43 $generated@@118 ($generated@@85 $generated@@115 $generated@@116) $generated@@119)))) + :pattern ( ($generated@@34 $generated@@29 ($generated@@105 $generated@@117 $generated@@118) ($generated@@33 $generated@@115 $generated@@116) $generated@@119)) +))) +(assert ($generated@@30 $generated@@97)) +(assert (forall (($generated@@122 T@U) ($generated@@123 T@U) ($generated@@124 T@U) ($generated@@125 T@T) ) (! (= ($generated@@120 $generated@@38 ($generated@@121 $generated@@125 $generated@@122) $generated@@123 $generated@@124) ($generated@@34 $generated@@125 $generated@@122 $generated@@123 $generated@@124)) + :pattern ( ($generated@@120 $generated@@38 ($generated@@121 $generated@@125 $generated@@122) $generated@@123 $generated@@124)) +))) +(assert (forall (($generated@@126 T@U) ($generated@@127 T@U) ($generated@@128 T@T) ) (! (= ($generated@@98 $generated@@128 $generated@@126 $generated@@127) (forall (($generated@@129 T@U) ) (! (= ($generated@@15 ($generated@@37 $generated@@128 $generated@@11 $generated@@126 $generated@@129)) ($generated@@15 ($generated@@37 $generated@@128 $generated@@11 $generated@@127 $generated@@129))) + :pattern ( ($generated@@37 $generated@@128 $generated@@11 $generated@@126 $generated@@129)) + :pattern ( ($generated@@37 $generated@@128 $generated@@11 $generated@@127 $generated@@129)) +))) + :pattern ( ($generated@@98 $generated@@128 $generated@@126 $generated@@127)) +))) +(assert (forall (($generated@@130 T@U) ($generated@@131 T@U) ($generated@@132 T@U) ($generated@@133 T@U) ) (! (= ($generated@@34 $generated@@43 $generated@@132 ($generated@@85 $generated@@130 $generated@@131) $generated@@133) ($generated@@34 $generated@@43 $generated@@132 ($generated@@77 $generated@@130 $generated@@131) $generated@@133)) + :pattern ( ($generated@@34 $generated@@43 $generated@@132 ($generated@@85 $generated@@130 $generated@@131) $generated@@133)) +))) +(assert (forall (($generated@@135 T@U) ($generated@@136 T@U) ($generated@@137 T@U) ($generated@@138 T@U) ) (! (=> (and ($generated@@30 $generated@@138) ($generated@@34 $generated@@43 $generated@@135 ($generated@@77 $generated@@136 $generated@@137) $generated@@138)) (forall (($generated@@139 T@U) ) (! (=> (and ($generated@@120 $generated@@38 $generated@@139 $generated@@136 $generated@@138) ($generated@@35 $generated@@136 $generated@@137 $generated@@138 $generated@@135 $generated@@139)) ($generated@@120 $generated@@38 ($generated@@134 $generated@@136 $generated@@137 $generated@@138 $generated@@135 $generated@@139) $generated@@137 $generated@@138)) + :pattern ( ($generated@@134 $generated@@136 $generated@@137 $generated@@138 $generated@@135 $generated@@139)) +))) + :pattern ( ($generated@@34 $generated@@43 $generated@@135 ($generated@@77 $generated@@136 $generated@@137) $generated@@138)) +))) +(assert (and (and (and (and (= ($generated@@10 $generated@@140) 7) (forall (($generated@@147 T@T) ($generated@@148 T@T) ($generated@@149 T@U) ($generated@@150 T@U) ($generated@@151 T@U) ) (! (= ($generated@@143 $generated@@147 $generated@@148 ($generated@@145 $generated@@147 $generated@@148 $generated@@150 $generated@@151 $generated@@149) $generated@@151) $generated@@149) + :weight 0 +))) (and (forall (($generated@@152 T@T) ($generated@@153 T@T) ($generated@@154 T@T) ($generated@@155 T@U) ($generated@@156 T@U) ($generated@@157 T@U) ($generated@@158 T@U) ) (! (or (= $generated@@153 $generated@@154) (= ($generated@@143 $generated@@154 $generated@@152 ($generated@@145 $generated@@153 $generated@@152 $generated@@156 $generated@@157 $generated@@155) $generated@@158) ($generated@@143 $generated@@154 $generated@@152 $generated@@156 $generated@@158))) + :weight 0 +)) (forall (($generated@@159 T@T) ($generated@@160 T@T) ($generated@@161 T@T) ($generated@@162 T@U) ($generated@@163 T@U) ($generated@@164 T@U) ($generated@@165 T@U) ) (! (or (= $generated@@164 $generated@@165) (= ($generated@@143 $generated@@161 $generated@@159 ($generated@@145 $generated@@160 $generated@@159 $generated@@163 $generated@@164 $generated@@162) $generated@@165) ($generated@@143 $generated@@161 $generated@@159 $generated@@163 $generated@@165))) + :weight 0 +)))) (forall (($generated@@166 T@T) ) (= ($generated@@10 ($generated@@144 $generated@@166)) 8))) (forall (($generated@@167 T@T) ) (! (= ($generated@@146 ($generated@@144 $generated@@167)) $generated@@167) + :pattern ( ($generated@@144 $generated@@167)) +)))) +(assert (forall (($generated@@168 T@U) ($generated@@169 T@U) ($generated@@170 T@U) ($generated@@171 T@U) ) (! (=> ($generated@@30 $generated@@171) (= ($generated@@34 $generated@@43 $generated@@168 ($generated@@77 $generated@@169 $generated@@170) $generated@@171) (forall (($generated@@172 T@U) ) (! (=> (and (and ($generated@@40 $generated@@38 $generated@@172 $generated@@169) ($generated@@120 $generated@@38 $generated@@172 $generated@@169 $generated@@171)) ($generated@@35 $generated@@169 $generated@@170 $generated@@171 $generated@@168 $generated@@172)) (forall (($generated@@173 T@U) ) (! (=> (and (or (not (= $generated@@173 $generated@@141)) (not true)) ($generated@@15 ($generated@@37 $generated@@38 $generated@@11 ($generated@@96 $generated@@169 $generated@@170 $generated@@171 $generated@@168 $generated@@172) ($generated@@121 $generated@@140 $generated@@173)))) ($generated@@15 ($generated@@142 $generated@@11 ($generated@@143 $generated@@11 $generated@@38 ($generated@@37 $generated@@140 ($generated@@144 $generated@@38) $generated@@171 $generated@@173) $generated@@2)))) + :pattern ( ($generated@@37 $generated@@38 $generated@@11 ($generated@@96 $generated@@169 $generated@@170 $generated@@171 $generated@@168 $generated@@172) ($generated@@121 $generated@@140 $generated@@173))) +))) + :pattern ( ($generated@@134 $generated@@169 $generated@@170 $generated@@171 $generated@@168 $generated@@172)) + :pattern ( ($generated@@96 $generated@@169 $generated@@170 $generated@@171 $generated@@168 $generated@@172)) +)))) + :pattern ( ($generated@@34 $generated@@43 $generated@@168 ($generated@@77 $generated@@169 $generated@@170) $generated@@171)) +))) +(assert (forall (($generated@@174 T@U) ($generated@@175 T@U) ($generated@@176 T@U) ) (! (= ($generated@@34 ($generated@@42 $generated@@38 $generated@@11) $generated@@174 ($generated@@90 $generated@@175) $generated@@176) (forall (($generated@@177 T@U) ) (! (=> ($generated@@15 ($generated@@37 $generated@@38 $generated@@11 $generated@@174 $generated@@177)) ($generated@@120 $generated@@38 $generated@@177 $generated@@175 $generated@@176)) + :pattern ( ($generated@@37 $generated@@38 $generated@@11 $generated@@174 $generated@@177)) +))) + :pattern ( ($generated@@34 ($generated@@42 $generated@@38 $generated@@11) $generated@@174 ($generated@@90 $generated@@175) $generated@@176)) +))) +(assert (forall (($generated@@178 T@U) ($generated@@179 T@U) ($generated@@180 T@T) ) (! (=> ($generated@@98 $generated@@180 $generated@@178 $generated@@179) (= $generated@@178 $generated@@179)) + :pattern ( ($generated@@98 $generated@@180 $generated@@178 $generated@@179)) +))) +(assert (=> (<= 0 $generated@@26) (forall (($generated@@181 T@U) ($generated@@182 T@U) ($generated@@183 T@U) ($generated@@184 T@U) ) (! (=> (or ($generated@@31 $generated@@181 $generated@@182 $generated@@184) (and (< 0 $generated@@26) (and ($generated@@30 $generated@@183) (and ($generated@@32 $generated@@29 $generated@@184 ($generated@@33 $generated@@181 $generated@@182)) ($generated@@34 $generated@@29 $generated@@184 ($generated@@33 $generated@@181 $generated@@182) $generated@@183))))) (and (forall (($generated@@185 T@U) ) (! (=> ($generated@@40 $generated@@38 $generated@@185 $generated@@181) (and ($generated@@41 $generated@@184) (=> ($generated@@15 ($generated@@37 $generated@@38 $generated@@11 ($generated@@39 $generated@@184) $generated@@185)) (and ($generated@@41 $generated@@184) true)))) + :pattern ( ($generated@@35 $generated@@181 $generated@@182 $generated@@183 ($generated@@36 $generated@@184) $generated@@185)) + :pattern ( ($generated@@37 $generated@@38 $generated@@11 ($generated@@39 $generated@@184) $generated@@185)) +)) (= ($generated@@27 $generated@@181 $generated@@182 $generated@@184) (forall (($generated@@186 T@U) ) (! (=> (and ($generated@@40 $generated@@38 $generated@@186 $generated@@181) ($generated@@15 ($generated@@37 $generated@@38 $generated@@11 ($generated@@39 $generated@@184) $generated@@186))) ($generated@@35 $generated@@181 $generated@@182 $generated@@183 ($generated@@36 $generated@@184) $generated@@186)) + :pattern ( ($generated@@35 $generated@@181 $generated@@182 $generated@@183 ($generated@@36 $generated@@184) $generated@@186)) + :pattern ( ($generated@@37 $generated@@38 $generated@@11 ($generated@@39 $generated@@184) $generated@@186)) +))))) + :pattern ( ($generated@@27 $generated@@181 $generated@@182 $generated@@184) ($generated@@30 $generated@@183)) +)))) +(assert (forall (($generated@@187 T@U) ($generated@@188 T@U) ($generated@@189 T@U) ) (! (= ($generated@@32 $generated@@43 $generated@@187 ($generated@@77 $generated@@188 $generated@@189)) (forall (($generated@@190 T@U) ($generated@@191 T@U) ) (! (=> (and (and ($generated@@30 $generated@@190) ($generated@@40 $generated@@38 $generated@@191 $generated@@188)) ($generated@@35 $generated@@188 $generated@@189 $generated@@190 $generated@@187 $generated@@191)) ($generated@@40 $generated@@38 ($generated@@134 $generated@@188 $generated@@189 $generated@@190 $generated@@187 $generated@@191) $generated@@189)) + :pattern ( ($generated@@134 $generated@@188 $generated@@189 $generated@@190 $generated@@187 $generated@@191)) +))) + :pattern ( ($generated@@32 $generated@@43 $generated@@187 ($generated@@77 $generated@@188 $generated@@189))) +))) +(assert (forall (($generated@@192 T@U) ) (! (=> ($generated@@40 $generated@@38 $generated@@192 $generated) (and (= ($generated@@121 $generated@@11 ($generated@@142 $generated@@11 $generated@@192)) $generated@@192) ($generated@@32 $generated@@11 ($generated@@142 $generated@@11 $generated@@192) $generated))) + :pattern ( ($generated@@40 $generated@@38 $generated@@192 $generated)) +))) +(assert (forall (($generated@@193 T@U) ($generated@@194 T@U) ($generated@@195 T@T) ) (! (= ($generated@@40 $generated@@38 ($generated@@121 $generated@@195 $generated@@193) $generated@@194) ($generated@@32 $generated@@195 $generated@@193 $generated@@194)) + :pattern ( ($generated@@40 $generated@@38 ($generated@@121 $generated@@195 $generated@@193) $generated@@194)) +))) +(assert (forall (($generated@@197 T@U) ($generated@@198 T@U) ) (! (= ($generated@@196 ($generated@@77 $generated@@197 $generated@@198)) $generated@@197) + :pattern ( ($generated@@77 $generated@@197 $generated@@198)) +))) +(assert (forall (($generated@@200 T@U) ($generated@@201 T@U) ) (! (= ($generated@@199 ($generated@@77 $generated@@200 $generated@@201)) $generated@@201) + :pattern ( ($generated@@77 $generated@@200 $generated@@201)) +))) +(assert (forall (($generated@@203 T@U) ($generated@@204 T@U) ) (! (= ($generated@@202 ($generated@@85 $generated@@203 $generated@@204)) $generated@@203) + :pattern ( ($generated@@85 $generated@@203 $generated@@204)) +))) +(assert (forall (($generated@@206 T@U) ($generated@@207 T@U) ) (! (= ($generated@@205 ($generated@@85 $generated@@206 $generated@@207)) $generated@@207) + :pattern ( ($generated@@85 $generated@@206 $generated@@207)) +))) +(assert (forall (($generated@@208 T@U) ($generated@@209 T@U) ) (! (= ($generated@@110 ($generated@@105 $generated@@208 $generated@@209)) $generated@@5) + :pattern ( ($generated@@105 $generated@@208 $generated@@209)) +))) +(assert (forall (($generated@@211 T@U) ($generated@@212 T@U) ) (! (= ($generated@@210 ($generated@@33 $generated@@211 $generated@@212)) $generated@@211) + :pattern ( ($generated@@33 $generated@@211 $generated@@212)) +))) +(assert (forall (($generated@@214 T@U) ($generated@@215 T@U) ) (! (= ($generated@@213 ($generated@@33 $generated@@214 $generated@@215)) $generated@@215) + :pattern ( ($generated@@33 $generated@@214 $generated@@215)) +))) +(assert (forall (($generated@@216 T@U) ($generated@@217 T@U) ) (! (= ($generated@@39 ($generated@@105 $generated@@216 $generated@@217)) $generated@@216) + :pattern ( ($generated@@105 $generated@@216 $generated@@217)) +))) +(assert (forall (($generated@@218 T@U) ($generated@@219 T@U) ) (! (= ($generated@@36 ($generated@@105 $generated@@218 $generated@@219)) $generated@@219) + :pattern ( ($generated@@105 $generated@@218 $generated@@219)) +))) +(assert (and (forall (($generated@@223 T@T) ($generated@@224 T@T) ($generated@@225 T@T) ($generated@@226 T@U) ($generated@@227 T@U) ($generated@@228 T@U) ($generated@@229 T@U) ) (! (= ($generated@@220 $generated@@223 $generated@@224 $generated@@225 ($generated@@222 $generated@@223 $generated@@224 $generated@@225 $generated@@227 $generated@@228 $generated@@229 $generated@@226) $generated@@228 $generated@@229) $generated@@226) + :weight 0 +)) (and (and (forall (($generated@@230 T@T) ($generated@@231 T@T) ($generated@@232 T@T) ($generated@@233 T@T) ($generated@@234 T@U) ($generated@@235 T@U) ($generated@@236 T@U) ($generated@@237 T@U) ($generated@@238 T@U) ($generated@@239 T@U) ) (! (or (= $generated@@232 $generated@@233) (= ($generated@@220 $generated@@233 $generated@@230 $generated@@231 ($generated@@222 $generated@@232 $generated@@230 $generated@@231 $generated@@235 $generated@@236 $generated@@237 $generated@@234) $generated@@238 $generated@@239) ($generated@@220 $generated@@233 $generated@@230 $generated@@231 $generated@@235 $generated@@238 $generated@@239))) + :weight 0 +)) (forall (($generated@@240 T@T) ($generated@@241 T@T) ($generated@@242 T@T) ($generated@@243 T@T) ($generated@@244 T@U) ($generated@@245 T@U) ($generated@@246 T@U) ($generated@@247 T@U) ($generated@@248 T@U) ($generated@@249 T@U) ) (! (or (= $generated@@246 $generated@@248) (= ($generated@@220 $generated@@243 $generated@@240 $generated@@241 ($generated@@222 $generated@@242 $generated@@240 $generated@@241 $generated@@245 $generated@@246 $generated@@247 $generated@@244) $generated@@248 $generated@@249) ($generated@@220 $generated@@243 $generated@@240 $generated@@241 $generated@@245 $generated@@248 $generated@@249))) + :weight 0 +))) (forall (($generated@@250 T@T) ($generated@@251 T@T) ($generated@@252 T@T) ($generated@@253 T@T) ($generated@@254 T@U) ($generated@@255 T@U) ($generated@@256 T@U) ($generated@@257 T@U) ($generated@@258 T@U) ($generated@@259 T@U) ) (! (or (= $generated@@257 $generated@@259) (= ($generated@@220 $generated@@253 $generated@@250 $generated@@251 ($generated@@222 $generated@@252 $generated@@250 $generated@@251 $generated@@255 $generated@@256 $generated@@257 $generated@@254) $generated@@258 $generated@@259) ($generated@@220 $generated@@253 $generated@@250 $generated@@251 $generated@@255 $generated@@258 $generated@@259))) + :weight 0 +))))) +(assert (forall (($generated@@260 T@U) ($generated@@261 T@U) ($generated@@262 T@U) ($generated@@263 Bool) ($generated@@264 T@U) ($generated@@265 T@U) ($generated@@266 T@T) ) (! (= ($generated@@15 ($generated@@220 $generated@@266 $generated@@140 $generated@@11 ($generated@@221 $generated@@260 $generated@@261 $generated@@262 $generated@@263) $generated@@264 $generated@@265)) (=> (and (or (not (= $generated@@264 $generated@@260)) (not true)) ($generated@@15 ($generated@@142 $generated@@11 ($generated@@143 $generated@@11 $generated@@38 ($generated@@37 $generated@@140 ($generated@@144 $generated@@38) $generated@@261 $generated@@264) $generated@@262)))) $generated@@263)) + :pattern ( ($generated@@220 $generated@@266 $generated@@140 $generated@@11 ($generated@@221 $generated@@260 $generated@@261 $generated@@262 $generated@@263) $generated@@264 $generated@@265)) +))) +(assert (forall (($generated@@268 T@U) ) (! (= ($generated@@267 ($generated@@90 $generated@@268)) $generated@@268) + :pattern ( ($generated@@90 $generated@@268)) +))) +(assert (forall (($generated@@269 T@U) ) (! (= ($generated@@70 ($generated@@90 $generated@@269)) $generated@@1) + :pattern ( ($generated@@90 $generated@@269)) +))) +(assert (forall (($generated@@270 T@U) ($generated@@271 T@T) ) (! (= ($generated@@142 $generated@@271 ($generated@@121 $generated@@271 $generated@@270)) $generated@@270) + :pattern ( ($generated@@121 $generated@@271 $generated@@270)) +))) +(assert (forall (($generated@@273 T@U) ($generated@@274 T@U) ($generated@@275 T@U) ) (! (=> ($generated@@15 ($generated@@37 $generated@@38 $generated@@11 $generated@@273 ($generated@@121 $generated@@29 $generated@@275))) (< ($generated@@272 $generated@@275) ($generated@@272 ($generated@@105 $generated@@273 $generated@@274)))) + :pattern ( ($generated@@37 $generated@@38 $generated@@11 $generated@@273 ($generated@@121 $generated@@29 $generated@@275)) ($generated@@105 $generated@@273 $generated@@274)) +))) +(assert (forall (($generated@@276 T@U) ($generated@@277 T@U) ($generated@@278 T@U) ) (! (= ($generated@@32 $generated@@43 $generated@@278 ($generated@@85 $generated@@276 $generated@@277)) (and ($generated@@32 $generated@@43 $generated@@278 ($generated@@77 $generated@@276 $generated@@277)) (forall (($generated@@279 T@U) ) (=> ($generated@@40 $generated@@38 $generated@@279 $generated@@276) ($generated@@98 $generated@@38 ($generated@@96 $generated@@276 $generated@@277 $generated@@97 $generated@@278 $generated@@279) ($generated@@99 $generated@@38)))))) + :pattern ( ($generated@@32 $generated@@43 $generated@@278 ($generated@@85 $generated@@276 $generated@@277))) +))) +(assert (forall (($generated@@280 T@U) ($generated@@281 T@U) ($generated@@282 T@U) ) (! (=> ($generated@@40 $generated@@38 $generated@@282 ($generated@@77 $generated@@280 $generated@@281)) (and (= ($generated@@121 $generated@@43 ($generated@@142 $generated@@43 $generated@@282)) $generated@@282) ($generated@@32 $generated@@43 ($generated@@142 $generated@@43 $generated@@282) ($generated@@77 $generated@@280 $generated@@281)))) + :pattern ( ($generated@@40 $generated@@38 $generated@@282 ($generated@@77 $generated@@280 $generated@@281))) +))) +(assert (forall (($generated@@283 T@U) ($generated@@284 T@U) ($generated@@285 T@U) ) (! (=> ($generated@@40 $generated@@38 $generated@@285 ($generated@@85 $generated@@283 $generated@@284)) (and (= ($generated@@121 $generated@@43 ($generated@@142 $generated@@43 $generated@@285)) $generated@@285) ($generated@@32 $generated@@43 ($generated@@142 $generated@@43 $generated@@285) ($generated@@85 $generated@@283 $generated@@284)))) + :pattern ( ($generated@@40 $generated@@38 $generated@@285 ($generated@@85 $generated@@283 $generated@@284))) +))) +(assert (forall (($generated@@286 T@U) ($generated@@287 T@U) ($generated@@288 T@U) ) (! (=> ($generated@@40 $generated@@38 $generated@@288 ($generated@@33 $generated@@286 $generated@@287)) (and (= ($generated@@121 $generated@@29 ($generated@@142 $generated@@29 $generated@@288)) $generated@@288) ($generated@@32 $generated@@29 ($generated@@142 $generated@@29 $generated@@288) ($generated@@33 $generated@@286 $generated@@287)))) + :pattern ( ($generated@@40 $generated@@38 $generated@@288 ($generated@@33 $generated@@286 $generated@@287))) +))) +(assert (forall (($generated@@289 T@U) ($generated@@290 T@T) ) (! (not ($generated@@15 ($generated@@37 $generated@@290 $generated@@11 ($generated@@99 $generated@@290) $generated@@289))) + :pattern ( ($generated@@37 $generated@@290 $generated@@11 ($generated@@99 $generated@@290) $generated@@289)) +))) +(assert (forall (($generated@@292 T@U) ($generated@@293 T@U) ) (! (and (= ($generated@@70 ($generated@@77 $generated@@292 $generated@@293)) $generated@@3) (= ($generated@@291 ($generated@@77 $generated@@292 $generated@@293)) $generated@@7)) + :pattern ( ($generated@@77 $generated@@292 $generated@@293)) +))) +(assert (forall (($generated@@294 T@U) ($generated@@295 T@U) ) (! (and (= ($generated@@70 ($generated@@85 $generated@@294 $generated@@295)) $generated@@4) (= ($generated@@291 ($generated@@85 $generated@@294 $generated@@295)) $generated@@8)) + :pattern ( ($generated@@85 $generated@@294 $generated@@295)) +))) +(assert (forall (($generated@@296 T@U) ($generated@@297 T@U) ) (! (and (= ($generated@@70 ($generated@@33 $generated@@296 $generated@@297)) $generated@@6) (= ($generated@@291 ($generated@@33 $generated@@296 $generated@@297)) $generated@@9)) + :pattern ( ($generated@@33 $generated@@296 $generated@@297)) +))) +(assert (forall (($generated@@298 T@U) ($generated@@299 T@U) ($generated@@300 T@U) ($generated@@301 T@U) ($generated@@302 T@U) ) (! (=> (and (and ($generated@@30 $generated@@300) (and ($generated@@40 $generated@@38 $generated@@302 $generated@@298) ($generated@@32 $generated@@43 $generated@@301 ($generated@@77 $generated@@298 $generated@@299)))) ($generated@@98 $generated@@38 ($generated@@96 $generated@@298 $generated@@299 $generated@@97 $generated@@301 $generated@@302) ($generated@@99 $generated@@38))) (= ($generated@@35 $generated@@298 $generated@@299 $generated@@97 $generated@@301 $generated@@302) ($generated@@35 $generated@@298 $generated@@299 $generated@@300 $generated@@301 $generated@@302))) + :pattern ( ($generated@@35 $generated@@298 $generated@@299 $generated@@97 $generated@@301 $generated@@302) ($generated@@30 $generated@@300)) + :pattern ( ($generated@@35 $generated@@298 $generated@@299 $generated@@300 $generated@@301 $generated@@302)) +))) +(assert (forall (($generated@@303 T@U) ($generated@@304 T@U) ) (! (=> ($generated@@40 $generated@@38 $generated@@303 ($generated@@90 $generated@@304)) (and (= ($generated@@121 ($generated@@42 $generated@@38 $generated@@11) ($generated@@142 ($generated@@42 $generated@@38 $generated@@11) $generated@@303)) $generated@@303) ($generated@@32 ($generated@@42 $generated@@38 $generated@@11) ($generated@@142 ($generated@@42 $generated@@38 $generated@@11) $generated@@303) ($generated@@90 $generated@@304)))) + :pattern ( ($generated@@40 $generated@@38 $generated@@303 ($generated@@90 $generated@@304))) +))) +(assert (forall (($generated@@305 T@U) ($generated@@306 T@U) ) (! (= ($generated@@105 ($generated@@28 ($generated@@42 $generated@@38 $generated@@11) $generated@@305) ($generated@@28 $generated@@43 $generated@@306)) ($generated@@28 $generated@@29 ($generated@@105 $generated@@305 $generated@@306))) + :pattern ( ($generated@@105 ($generated@@28 ($generated@@42 $generated@@38 $generated@@11) $generated@@305) ($generated@@28 $generated@@43 $generated@@306))) +))) +(assert (forall (($generated@@307 T@U) ($generated@@308 T@T) ) (! (= ($generated@@121 $generated@@308 ($generated@@28 $generated@@308 $generated@@307)) ($generated@@28 $generated@@38 ($generated@@121 $generated@@308 $generated@@307))) + :pattern ( ($generated@@121 $generated@@308 ($generated@@28 $generated@@308 $generated@@307))) +))) +(assert (forall (($generated@@309 T@U) ($generated@@310 T@U) ($generated@@311 T@U) ) (! (=> (and ($generated@@30 $generated@@311) (and ($generated@@41 $generated@@309) (exists (($generated@@312 T@U) ) (! ($generated@@34 $generated@@29 $generated@@309 ($generated@@33 $generated@@310 $generated@@312) $generated@@311) + :pattern ( ($generated@@34 $generated@@29 $generated@@309 ($generated@@33 $generated@@310 $generated@@312) $generated@@311)) +)))) ($generated@@34 ($generated@@42 $generated@@38 $generated@@11) ($generated@@39 $generated@@309) ($generated@@90 $generated@@310) $generated@@311)) + :pattern ( ($generated@@34 ($generated@@42 $generated@@38 $generated@@11) ($generated@@39 $generated@@309) ($generated@@90 $generated@@310) $generated@@311)) +))) +(assert (forall (($generated@@313 T@U) ($generated@@314 T@U) ) (! ($generated@@34 $generated@@11 $generated@@314 $generated $generated@@313) + :pattern ( ($generated@@34 $generated@@11 $generated@@314 $generated $generated@@313)) +))) +(assert (forall (($generated@@315 T@U) ) (! ($generated@@32 $generated@@11 $generated@@315 $generated) + :pattern ( ($generated@@32 $generated@@11 $generated@@315 $generated)) +))) +(push 1) +(declare-fun ControlFlow (Int Int) Int) +(declare-fun $generated@@316 () T@U) +(declare-fun $generated@@317 () T@U) +(declare-fun $generated@@318 () T@U) +(declare-fun $generated@@319 () T@U) +(declare-fun $generated@@320 () Bool) +(declare-fun $generated@@321 () T@U) +(declare-fun $generated@@322 () Bool) +(declare-fun $generated@@323 () T@U) +(declare-fun $generated@@324 (T@U) Bool) +(set-option :timeout 0) +(set-option :rlimit 0) +(assert (not + (=> (= (ControlFlow 0 0) 9) (let (($generated@@325 (=> (and (and (= ($generated@@27 $generated@@316 $generated@@317 $generated@@318) (forall (($generated@@326 T@U) ) (! (=> (and ($generated@@40 $generated@@38 $generated@@326 $generated@@316) ($generated@@15 ($generated@@37 $generated@@38 $generated@@11 ($generated@@39 $generated@@318) $generated@@326))) ($generated@@35 $generated@@316 $generated@@317 $generated@@319 ($generated@@36 $generated@@318) $generated@@326)) + :pattern ( ($generated@@35 $generated@@316 $generated@@317 $generated@@319 ($generated@@36 $generated@@318) $generated@@326)) + :pattern ( ($generated@@37 $generated@@38 $generated@@11 ($generated@@39 $generated@@318) $generated@@326)) +))) (forall (($generated@@327 T@U) ) (! (=> ($generated@@40 $generated@@38 $generated@@327 $generated@@316) (and ($generated@@41 $generated@@318) (=> ($generated@@15 ($generated@@37 $generated@@38 $generated@@11 ($generated@@39 $generated@@318) $generated@@327)) (and ($generated@@41 $generated@@318) true)))) + :pattern ( ($generated@@35 $generated@@316 $generated@@317 $generated@@319 ($generated@@36 $generated@@318) $generated@@327)) + :pattern ( ($generated@@37 $generated@@38 $generated@@11 ($generated@@39 $generated@@318) $generated@@327)) +))) (and ($generated@@32 $generated@@11 ($generated@@14 ($generated@@27 $generated@@316 $generated@@317 $generated@@318)) $generated) (= (ControlFlow 0 3) (- 0 2)))) $generated@@320))) +(let (($generated@@328 (=> (not ($generated@@15 ($generated@@37 $generated@@38 $generated@@11 ($generated@@39 $generated@@318) $generated@@321))) (=> (and (= $generated@@320 true) (= (ControlFlow 0 6) 3)) $generated@@325)))) +(let (($generated@@329 (=> ($generated@@15 ($generated@@37 $generated@@38 $generated@@11 ($generated@@39 $generated@@318) $generated@@321)) (=> (and ($generated@@41 $generated@@318) ($generated@@34 $generated@@43 ($generated@@36 $generated@@318) ($generated@@77 $generated@@316 $generated@@317) $generated@@319)) (=> (and (and ($generated@@120 $generated@@38 $generated@@321 $generated@@316 $generated@@319) (= $generated@@322 (forall (($generated@@330 T@U) ($generated@@331 T@U) ($generated@@332 T@T) ) (=> (and (and (or (not (= $generated@@330 $generated@@141)) (not true)) ($generated@@15 ($generated@@142 $generated@@11 ($generated@@143 $generated@@11 $generated@@38 ($generated@@37 $generated@@140 ($generated@@144 $generated@@38) $generated@@319 $generated@@330) $generated@@2)))) ($generated@@15 ($generated@@37 $generated@@38 $generated@@11 ($generated@@96 $generated@@316 $generated@@317 $generated@@319 ($generated@@36 $generated@@318) $generated@@321) ($generated@@121 $generated@@140 $generated@@330)))) ($generated@@15 ($generated@@220 $generated@@332 $generated@@140 $generated@@11 $generated@@323 $generated@@330 $generated@@331)))))) (and (= $generated@@320 $generated@@322) (= (ControlFlow 0 5) 3))) $generated@@325))))) +(let (($generated@@333 (=> (and (and ($generated@@40 $generated@@38 $generated@@321 $generated@@316) ($generated@@120 $generated@@38 $generated@@321 $generated@@316 $generated@@319)) ($generated@@41 $generated@@318)) (and (=> (= (ControlFlow 0 7) 5) $generated@@329) (=> (= (ControlFlow 0 7) 6) $generated@@328))))) +(let (($generated@@334 (=> (not (and ($generated@@40 $generated@@38 $generated@@321 $generated@@316) ($generated@@120 $generated@@38 $generated@@321 $generated@@316 $generated@@319))) (=> (and (= $generated@@320 true) (= (ControlFlow 0 4) 3)) $generated@@325)))) +(let (($generated@@335 true)) +(let (($generated@@336 (=> (= $generated@@323 ($generated@@221 $generated@@141 $generated@@319 $generated@@2 false)) (and (and (=> (= (ControlFlow 0 8) 1) $generated@@335) (=> (= (ControlFlow 0 8) 7) $generated@@333)) (=> (= (ControlFlow 0 8) 4) $generated@@334))))) +(let (($generated@@337 (=> (and ($generated@@30 $generated@@319) ($generated@@324 $generated@@319)) (=> (and (and ($generated@@32 $generated@@29 $generated@@318 ($generated@@33 $generated@@316 $generated@@317)) ($generated@@34 $generated@@29 $generated@@318 ($generated@@33 $generated@@316 $generated@@317) $generated@@319)) (and (= 0 $generated@@26) (= (ControlFlow 0 9) 8))) $generated@@336)))) +$generated@@337))))))))) +)) +(check-sat) +(pop 1) +; Valid +(get-info :rlimit) +(reset) +(set-option :rlimit 0) +; did a full reset +(reset) +(set-option :print-success false) +(set-info :smt-lib-version 2.6) +(set-option :auto_config false) +(set-option :type_check true) +(set-option :smt.qi.eager_threshold 100) +(set-option :smt.delay_units true) +(set-option :smt.case_split 3) +(set-option :smt.arith.solver 2) +(set-option :smt.mbqi false) +(set-option :model.compact false) +(set-option :model.v2 true) +(set-option :pp.bv_literals false) +; done setting options + + +(set-info :category "industrial") +(declare-sort |T@U| 0) +(declare-sort |T@T| 0) +(declare-fun real_pow (Real Real) Real) +(declare-fun UOrdering2 (|T@U| |T@U|) Bool) +(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool) +(declare-fun tickleBool (Bool) Bool) +(assert (and (tickleBool true) (tickleBool false))) +(declare-fun $generated () T@U) +(declare-fun $generated@@0 () T@U) +(declare-fun $generated@@1 () T@U) +(declare-fun $generated@@2 () T@U) +(declare-fun $generated@@3 () T@U) +(declare-fun $generated@@4 () T@U) +(declare-fun $generated@@5 () T@U) +(declare-fun $generated@@6 () T@U) +(declare-fun $generated@@7 () T@U) +(declare-fun $generated@@8 () T@U) +(declare-fun $generated@@9 () T@U) +(declare-fun $generated@@10 () T@U) +(declare-fun $generated@@11 () T@U) +(declare-fun $generated@@12 () T@U) +(declare-fun $generated@@13 () T@U) +(declare-fun $generated@@14 (T@T) Int) +(declare-fun $generated@@15 () T@T) +(declare-fun $generated@@16 () T@T) +(declare-fun $generated@@17 () T@T) +(declare-fun $generated@@18 (Bool) T@U) +(declare-fun $generated@@19 (T@U) Bool) +(declare-fun $generated@@20 (Int) T@U) +(declare-fun $generated@@21 (T@U) Int) +(declare-fun $generated@@22 (Real) T@U) +(declare-fun $generated@@23 (T@U) Real) +(declare-fun $generated@@30 () Int) +(declare-fun $generated@@31 (T@U T@U T@U) Bool) +(declare-fun $generated@@32 (T@T T@U) T@U) +(declare-fun $generated@@33 () T@T) +(declare-fun $generated@@34 (T@U) Bool) +(declare-fun $generated@@35 (T@U T@U T@U) Bool) +(declare-fun $generated@@36 (T@T T@U T@U) Bool) +(declare-fun $generated@@37 (T@U T@U) T@U) +(declare-fun $generated@@38 (T@T T@U T@U T@U) Bool) +(declare-fun $generated@@39 (T@U T@U T@U T@U T@U) Bool) +(declare-fun $generated@@40 (T@U) T@U) +(declare-fun $generated@@41 (T@T T@T T@U T@U) T@U) +(declare-fun $generated@@42 () T@T) +(declare-fun $generated@@43 (T@U) T@U) +(declare-fun $generated@@44 (T@T T@U T@U) Bool) +(declare-fun $generated@@45 (T@U) Bool) +(declare-fun $generated@@46 (T@T T@T) T@T) +(declare-fun $generated@@47 () T@T) +(declare-fun $generated@@48 (T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@49 (T@T) T@T) +(declare-fun $generated@@50 (T@T) T@T) +(declare-fun $generated@@74 (T@U T@U) Bool) +(declare-fun $generated@@75 (T@T T@U) T@U) +(declare-fun $generated@@76 (T@T T@T T@U T@U) T@U) +(declare-fun $generated@@77 () T@T) +(declare-fun $generated@@78 (T@T) T@T) +(declare-fun $generated@@79 (T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@80 (T@T) T@T) +(declare-fun $generated@@108 () T@U) +(declare-fun $generated@@109 () T@U) +(declare-fun $generated@@115 (T@U) T@U) +(declare-fun $generated@@116 () T@U) +(declare-fun $generated@@117 (T@U T@U) T@U) +(declare-fun $generated@@125 () T@U) +(declare-fun $generated@@126 (T@U T@U) T@U) +(declare-fun $generated@@131 (T@U) T@U) +(declare-fun $generated@@135 (T@U) T@U) +(declare-fun $generated@@141 (T@U T@U T@U T@U T@U) T@U) +(declare-fun $generated@@142 () T@U) +(declare-fun $generated@@143 (T@T T@U T@U) Bool) +(declare-fun $generated@@144 (T@T) T@U) +(declare-fun $generated@@150 (T@U T@U) T@U) +(declare-fun $generated@@159 (T@U) T@U) +(declare-fun $generated@@162 (T@T T@U T@U) T@U) +(declare-fun $generated@@163 () T@T) +(declare-fun $generated@@172 (T@T T@U T@U T@U) Bool) +(declare-fun $generated@@173 (T@T T@U) T@U) +(declare-fun $generated@@195 (T@U T@U T@U T@U T@U) T@U) +(declare-fun $generated@@196 (T@U T@U T@U) T@U) +(declare-fun $generated@@197 (T@T T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@198 (T@T T@T T@T T@U T@U T@U T@U) T@U) +(declare-fun $generated@@244 (Bool) T@U) +(declare-fun $generated@@247 (T@U) T@U) +(declare-fun $generated@@293 (T@U) T@U) +(declare-fun $generated@@296 (T@U) T@U) +(declare-fun $generated@@299 (T@U) T@U) +(declare-fun $generated@@302 (T@U) T@U) +(declare-fun $generated@@307 (T@U) T@U) +(declare-fun $generated@@310 (T@U) T@U) +(declare-fun $generated@@318 (T@T T@T T@T T@U T@U T@U) T@U) +(declare-fun $generated@@319 (T@U T@U T@U Bool) T@U) +(declare-fun $generated@@320 (T@T T@T T@T T@U T@U T@U T@U) T@U) +(declare-fun $generated@@365 (T@U T@U T@U Bool) T@U) +(declare-fun $generated@@373 (T@U) T@U) +(declare-fun $generated@@375 (T@U) T@U) +(declare-fun $generated@@377 (T@U) T@U) +(declare-fun $generated@@382 (T@U) Int) +(declare-fun $generated@@408 (T@U) T@U) +(declare-fun $generated@@423 (T@T) T@U) +(declare-fun $generated@@426 (T@U) T@U) +(declare-fun $generated@@489 (T@U) T@U) +(declare-fun $generated@@493 (T@U) T@U) +(declare-fun $generated@@497 (T@U Bool) T@U) +(assert (and (and (and (and (and (and (and (and (= ($generated@@14 $generated@@15) 0) (= ($generated@@14 $generated@@16) 1)) (= ($generated@@14 $generated@@17) 2)) (forall (($generated@@24 Bool) ) (! (= ($generated@@19 ($generated@@18 $generated@@24)) $generated@@24) + :pattern ( ($generated@@18 $generated@@24)) +))) (forall (($generated@@25 T@U) ) (! (= ($generated@@18 ($generated@@19 $generated@@25)) $generated@@25) + :pattern ( ($generated@@19 $generated@@25)) +))) (forall (($generated@@26 Int) ) (! (= ($generated@@21 ($generated@@20 $generated@@26)) $generated@@26) + :pattern ( ($generated@@20 $generated@@26)) +))) (forall (($generated@@27 T@U) ) (! (= ($generated@@20 ($generated@@21 $generated@@27)) $generated@@27) + :pattern ( ($generated@@21 $generated@@27)) +))) (forall (($generated@@28 Real) ) (! (= ($generated@@23 ($generated@@22 $generated@@28)) $generated@@28) + :pattern ( ($generated@@22 $generated@@28)) +))) (forall (($generated@@29 T@U) ) (! (= ($generated@@22 ($generated@@23 $generated@@29)) $generated@@29) + :pattern ( ($generated@@23 $generated@@29)) +)))) +(assert (distinct $generated $generated@@0 $generated@@1 $generated@@2 $generated@@3 $generated@@4 $generated@@5 $generated@@6 $generated@@7 $generated@@8 $generated@@9 $generated@@10 $generated@@11 $generated@@12 $generated@@13) +) +(assert (and (and (and (and (and (and (and (= ($generated@@14 $generated@@33) 3) (forall (($generated@@51 T@T) ($generated@@52 T@T) ($generated@@53 T@U) ($generated@@54 T@U) ($generated@@55 T@U) ) (! (= ($generated@@41 $generated@@51 $generated@@52 ($generated@@48 $generated@@51 $generated@@52 $generated@@54 $generated@@55 $generated@@53) $generated@@55) $generated@@53) + :weight 0 +))) (forall (($generated@@56 T@T) ($generated@@57 T@T) ($generated@@58 T@U) ($generated@@59 T@U) ($generated@@60 T@U) ($generated@@61 T@U) ) (! (or (= $generated@@60 $generated@@61) (= ($generated@@41 $generated@@56 $generated@@57 ($generated@@48 $generated@@56 $generated@@57 $generated@@59 $generated@@60 $generated@@58) $generated@@61) ($generated@@41 $generated@@56 $generated@@57 $generated@@59 $generated@@61))) + :weight 0 +))) (= ($generated@@14 $generated@@42) 4)) (forall (($generated@@62 T@T) ($generated@@63 T@T) ) (= ($generated@@14 ($generated@@46 $generated@@62 $generated@@63)) 5))) (forall (($generated@@64 T@T) ($generated@@65 T@T) ) (! (= ($generated@@49 ($generated@@46 $generated@@64 $generated@@65)) $generated@@64) + :pattern ( ($generated@@46 $generated@@64 $generated@@65)) +))) (forall (($generated@@66 T@T) ($generated@@67 T@T) ) (! (= ($generated@@50 ($generated@@46 $generated@@66 $generated@@67)) $generated@@67) + :pattern ( ($generated@@46 $generated@@66 $generated@@67)) +))) (= ($generated@@14 $generated@@47) 6))) +(assert (=> (<= 0 $generated@@30) (forall (($generated@@68 T@U) ($generated@@69 T@U) ($generated@@70 T@U) ($generated@@71 T@U) ) (! (=> (or ($generated@@35 $generated@@68 $generated@@69 ($generated@@32 $generated@@33 $generated@@71)) (and (< 0 $generated@@30) (and ($generated@@34 $generated@@70) (and ($generated@@36 $generated@@33 $generated@@71 ($generated@@37 $generated@@68 $generated@@69)) ($generated@@38 $generated@@33 $generated@@71 ($generated@@37 $generated@@68 $generated@@69) $generated@@70))))) (and (forall (($generated@@72 T@U) ) (! (=> ($generated@@44 $generated@@42 $generated@@72 $generated@@68) (and ($generated@@45 ($generated@@32 $generated@@33 $generated@@71)) (=> ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 ($generated@@32 ($generated@@46 $generated@@42 $generated@@15) ($generated@@43 ($generated@@32 $generated@@33 $generated@@71))) $generated@@72)) (and ($generated@@45 ($generated@@32 $generated@@33 $generated@@71)) true)))) + :pattern ( ($generated@@39 $generated@@68 $generated@@69 $generated@@70 ($generated@@40 $generated@@71) $generated@@72)) + :pattern ( ($generated@@41 $generated@@42 $generated@@15 ($generated@@43 $generated@@71) $generated@@72)) +)) (= ($generated@@31 $generated@@68 $generated@@69 ($generated@@32 $generated@@33 $generated@@71)) (forall (($generated@@73 T@U) ) (! (=> (and ($generated@@44 $generated@@42 $generated@@73 $generated@@68) ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 ($generated@@32 ($generated@@46 $generated@@42 $generated@@15) ($generated@@43 ($generated@@32 $generated@@33 $generated@@71))) $generated@@73))) ($generated@@39 $generated@@68 $generated@@69 $generated@@70 ($generated@@32 $generated@@47 ($generated@@40 ($generated@@32 $generated@@33 $generated@@71))) $generated@@73)) + :pattern ( ($generated@@39 $generated@@68 $generated@@69 $generated@@70 ($generated@@40 $generated@@71) $generated@@73)) + :pattern ( ($generated@@41 $generated@@42 $generated@@15 ($generated@@43 $generated@@71) $generated@@73)) +))))) + :weight 3 + :pattern ( ($generated@@31 $generated@@68 $generated@@69 ($generated@@32 $generated@@33 $generated@@71)) ($generated@@34 $generated@@70)) +)))) +(assert (and (and (and (and (forall (($generated@@81 T@T) ($generated@@82 T@T) ($generated@@83 T@U) ($generated@@84 T@U) ($generated@@85 T@U) ) (! (= ($generated@@76 $generated@@81 $generated@@82 ($generated@@79 $generated@@81 $generated@@82 $generated@@84 $generated@@85 $generated@@83) $generated@@85) $generated@@83) + :weight 0 +)) (and (forall (($generated@@86 T@T) ($generated@@87 T@T) ($generated@@88 T@T) ($generated@@89 T@U) ($generated@@90 T@U) ($generated@@91 T@U) ($generated@@92 T@U) ) (! (or (= $generated@@87 $generated@@88) (= ($generated@@76 $generated@@88 $generated@@86 ($generated@@79 $generated@@87 $generated@@86 $generated@@90 $generated@@91 $generated@@89) $generated@@92) ($generated@@76 $generated@@88 $generated@@86 $generated@@90 $generated@@92))) + :weight 0 +)) (forall (($generated@@93 T@T) ($generated@@94 T@T) ($generated@@95 T@T) ($generated@@96 T@U) ($generated@@97 T@U) ($generated@@98 T@U) ($generated@@99 T@U) ) (! (or (= $generated@@98 $generated@@99) (= ($generated@@76 $generated@@95 $generated@@93 ($generated@@79 $generated@@94 $generated@@93 $generated@@97 $generated@@98 $generated@@96) $generated@@99) ($generated@@76 $generated@@95 $generated@@93 $generated@@97 $generated@@99))) + :weight 0 +)))) (= ($generated@@14 $generated@@77) 7)) (forall (($generated@@100 T@T) ) (= ($generated@@14 ($generated@@78 $generated@@100)) 8))) (forall (($generated@@101 T@T) ) (! (= ($generated@@80 ($generated@@78 $generated@@101)) $generated@@101) + :pattern ( ($generated@@78 $generated@@101)) +)))) +(assert (forall (($generated@@102 T@U) ($generated@@103 T@U) ) (! (=> ($generated@@74 $generated@@102 $generated@@103) (forall (($generated@@104 T@U) ) (! (=> ($generated@@19 ($generated@@75 $generated@@15 ($generated@@76 $generated@@15 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@102 $generated@@104) $generated@@1))) ($generated@@19 ($generated@@75 $generated@@15 ($generated@@76 $generated@@15 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@103 $generated@@104) $generated@@1)))) + :pattern ( ($generated@@75 $generated@@15 ($generated@@76 $generated@@15 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@103 $generated@@104) $generated@@1))) +))) + :pattern ( ($generated@@74 $generated@@102 $generated@@103)) +))) +(assert (=> (<= 0 $generated@@30) (forall (($generated@@105 T@U) ($generated@@106 T@U) ($generated@@107 T@U) ) (! (=> (or ($generated@@35 $generated@@105 $generated@@106 $generated@@107) (and (< 0 $generated@@30) ($generated@@36 $generated@@33 $generated@@107 ($generated@@37 $generated@@105 $generated@@106)))) true) + :pattern ( ($generated@@31 $generated@@105 $generated@@106 $generated@@107)) +)))) +(assert (forall (($generated@@110 T@U) ($generated@@111 T@U) ) (! (= ($generated@@38 $generated@@77 $generated@@110 $generated@@108 $generated@@111) (or (= $generated@@110 $generated@@109) ($generated@@19 ($generated@@75 $generated@@15 ($generated@@76 $generated@@15 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@111 $generated@@110) $generated@@1))))) + :pattern ( ($generated@@38 $generated@@77 $generated@@110 $generated@@108 $generated@@111)) +))) +(assert (forall (($generated@@112 T@U) ($generated@@113 T@U) ($generated@@114 T@U) ) (! (=> ($generated@@36 $generated@@33 $generated@@114 ($generated@@37 $generated@@112 $generated@@113)) ($generated@@45 $generated@@114)) + :pattern ( ($generated@@45 $generated@@114) ($generated@@36 $generated@@33 $generated@@114 ($generated@@37 $generated@@112 $generated@@113))) +))) +(assert (= ($generated@@115 $generated@@116) $generated@@5)) +(assert (forall (($generated@@118 T@U) ($generated@@119 T@U) ($generated@@120 T@U) ($generated@@121 T@U) ($generated@@122 T@U) ) (! (=> (and (and ($generated@@36 $generated@@47 $generated@@118 ($generated@@117 $generated@@119 $generated@@120)) (forall (($generated@@123 T@U) ) (! (=> ($generated@@44 $generated@@42 $generated@@123 $generated@@121) ($generated@@44 $generated@@42 $generated@@123 $generated@@119)) + :pattern ( ($generated@@44 $generated@@42 $generated@@123 $generated@@121)) + :pattern ( ($generated@@44 $generated@@42 $generated@@123 $generated@@119)) +))) (forall (($generated@@124 T@U) ) (! (=> ($generated@@44 $generated@@42 $generated@@124 $generated@@120) ($generated@@44 $generated@@42 $generated@@124 $generated@@122)) + :pattern ( ($generated@@44 $generated@@42 $generated@@124 $generated@@120)) + :pattern ( ($generated@@44 $generated@@42 $generated@@124 $generated@@122)) +))) ($generated@@36 $generated@@47 $generated@@118 ($generated@@117 $generated@@121 $generated@@122))) + :pattern ( ($generated@@36 $generated@@47 $generated@@118 ($generated@@117 $generated@@119 $generated@@120)) ($generated@@36 $generated@@47 $generated@@118 ($generated@@117 $generated@@121 $generated@@122))) +))) +(assert ($generated@@36 $generated@@33 $generated@@116 $generated@@125)) +(assert (forall (($generated@@127 T@U) ($generated@@128 T@U) ($generated@@129 T@U) ($generated@@130 T@U) ) (! (=> (and ($generated@@34 $generated@@130) (and ($generated@@45 $generated@@127) ($generated@@38 $generated@@33 $generated@@127 ($generated@@37 $generated@@128 $generated@@129) $generated@@130))) ($generated@@38 $generated@@47 ($generated@@40 $generated@@127) ($generated@@126 $generated@@128 $generated@@129) $generated@@130)) + :pattern ( ($generated@@38 $generated@@47 ($generated@@40 $generated@@127) ($generated@@126 $generated@@128 $generated@@129) $generated@@130)) +))) +(assert (forall (($generated@@132 T@U) ($generated@@133 T@U) ) (! (= ($generated@@36 ($generated@@46 $generated@@42 $generated@@15) $generated@@132 ($generated@@131 $generated@@133)) (forall (($generated@@134 T@U) ) (! (=> ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 $generated@@132 $generated@@134)) ($generated@@44 $generated@@42 $generated@@134 $generated@@133)) + :pattern ( ($generated@@41 $generated@@42 $generated@@15 $generated@@132 $generated@@134)) +))) + :pattern ( ($generated@@36 ($generated@@46 $generated@@42 $generated@@15) $generated@@132 ($generated@@131 $generated@@133))) +))) +(assert (forall (($generated@@136 T@U) ($generated@@137 T@U) ) (! (= ($generated@@36 ($generated@@46 $generated@@42 $generated@@15) $generated@@136 ($generated@@135 $generated@@137)) (forall (($generated@@138 T@U) ) (! (=> ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 $generated@@136 $generated@@138)) ($generated@@44 $generated@@42 $generated@@138 $generated@@137)) + :pattern ( ($generated@@41 $generated@@42 $generated@@15 $generated@@136 $generated@@138)) +))) + :pattern ( ($generated@@36 ($generated@@46 $generated@@42 $generated@@15) $generated@@136 ($generated@@135 $generated@@137))) +))) +(assert (forall (($generated@@139 T@U) ($generated@@140 T@T) ) (! (= ($generated@@32 $generated@@140 $generated@@139) $generated@@139) + :pattern ( ($generated@@32 $generated@@140 $generated@@139)) +))) +(assert (forall (($generated@@145 T@U) ($generated@@146 T@U) ($generated@@147 T@U) ($generated@@148 T@U) ($generated@@149 T@U) ) (! (=> (and ($generated@@34 $generated@@147) (and ($generated@@44 $generated@@42 $generated@@149 $generated@@145) ($generated@@36 $generated@@47 $generated@@148 ($generated@@117 $generated@@145 $generated@@146)))) (= ($generated@@143 $generated@@42 ($generated@@141 $generated@@145 $generated@@146 $generated@@142 $generated@@148 $generated@@149) ($generated@@144 $generated@@42)) ($generated@@143 $generated@@42 ($generated@@141 $generated@@145 $generated@@146 $generated@@147 $generated@@148 $generated@@149) ($generated@@144 $generated@@42)))) + :pattern ( ($generated@@141 $generated@@145 $generated@@146 $generated@@142 $generated@@148 $generated@@149) ($generated@@34 $generated@@147)) + :pattern ( ($generated@@141 $generated@@145 $generated@@146 $generated@@147 $generated@@148 $generated@@149)) +))) +(assert (forall (($generated@@151 T@U) ($generated@@152 T@U) ($generated@@153 T@U) ($generated@@154 T@U) ) (! (= ($generated@@36 $generated@@33 ($generated@@150 $generated@@153 $generated@@154) ($generated@@37 $generated@@151 $generated@@152)) (and ($generated@@36 ($generated@@46 $generated@@42 $generated@@15) $generated@@153 ($generated@@135 $generated@@151)) ($generated@@36 $generated@@47 $generated@@154 ($generated@@126 $generated@@151 $generated@@152)))) + :pattern ( ($generated@@36 $generated@@33 ($generated@@150 $generated@@153 $generated@@154) ($generated@@37 $generated@@151 $generated@@152))) +))) +(assert (forall (($generated@@155 T@U) ) (! (= ($generated@@45 $generated@@155) (= ($generated@@115 $generated@@155) $generated@@7)) + :pattern ( ($generated@@45 $generated@@155)) +))) +(assert (forall (($generated@@156 T@U) ) (! (=> ($generated@@45 $generated@@156) (exists (($generated@@157 T@U) ($generated@@158 T@U) ) (= $generated@@156 ($generated@@150 $generated@@157 $generated@@158)))) + :pattern ( ($generated@@45 $generated@@156)) +))) +(assert (forall (($generated@@160 T@U) ($generated@@161 T@U) ) (! (= ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 ($generated@@159 $generated@@160) $generated@@161)) ($generated@@19 ($generated@@41 $generated@@77 $generated@@15 $generated@@160 ($generated@@75 $generated@@77 $generated@@161)))) + :pattern ( ($generated@@41 $generated@@42 $generated@@15 ($generated@@159 $generated@@160) $generated@@161)) +))) +(assert (= ($generated@@14 $generated@@163) 9)) +(assert (forall (($generated@@164 T@U) ($generated@@165 T@U) ($generated@@166 T@T) ) (! (= ($generated@@162 $generated@@166 $generated@@164 $generated@@165) ($generated@@41 $generated@@163 $generated@@166 $generated@@164 $generated@@165)) + :pattern ( ($generated@@162 $generated@@166 $generated@@164 $generated@@165)) +))) +(assert (forall (($generated@@167 T@U) ($generated@@168 T@U) ($generated@@169 T@U) ($generated@@170 T@U) ($generated@@171 T@U) ) (! (=> ($generated@@34 $generated@@171) (= ($generated@@38 $generated@@33 ($generated@@150 $generated@@169 $generated@@170) ($generated@@37 $generated@@167 $generated@@168) $generated@@171) (and ($generated@@38 ($generated@@46 $generated@@42 $generated@@15) $generated@@169 ($generated@@135 $generated@@167) $generated@@171) ($generated@@38 $generated@@47 $generated@@170 ($generated@@126 $generated@@167 $generated@@168) $generated@@171)))) + :pattern ( ($generated@@38 $generated@@33 ($generated@@150 $generated@@169 $generated@@170) ($generated@@37 $generated@@167 $generated@@168) $generated@@171)) +))) +(assert ($generated@@34 $generated@@142)) +(assert (forall (($generated@@174 T@U) ($generated@@175 T@U) ($generated@@176 T@U) ($generated@@177 T@T) ) (! (= ($generated@@172 $generated@@42 ($generated@@173 $generated@@177 $generated@@174) $generated@@175 $generated@@176) ($generated@@38 $generated@@177 $generated@@174 $generated@@175 $generated@@176)) + :pattern ( ($generated@@172 $generated@@42 ($generated@@173 $generated@@177 $generated@@174) $generated@@175 $generated@@176)) +))) +(assert (forall (($generated@@178 T@U) ($generated@@179 T@U) ($generated@@180 T@U) ($generated@@181 T@U) ) (! (=> ($generated@@74 $generated@@178 $generated@@179) (=> ($generated@@172 $generated@@42 $generated@@180 $generated@@181 $generated@@178) ($generated@@172 $generated@@42 $generated@@180 $generated@@181 $generated@@179))) + :pattern ( ($generated@@74 $generated@@178 $generated@@179) ($generated@@172 $generated@@42 $generated@@180 $generated@@181 $generated@@178)) +))) +(assert (forall (($generated@@182 T@U) ($generated@@183 T@U) ($generated@@184 T@U) ($generated@@185 T@U) ($generated@@186 T@T) ) (! (=> ($generated@@74 $generated@@182 $generated@@183) (=> ($generated@@38 $generated@@186 $generated@@184 $generated@@185 $generated@@182) ($generated@@38 $generated@@186 $generated@@184 $generated@@185 $generated@@183))) + :pattern ( ($generated@@74 $generated@@182 $generated@@183) ($generated@@38 $generated@@186 $generated@@184 $generated@@185 $generated@@182)) +))) +(assert (forall (($generated@@187 T@U) ($generated@@188 T@U) ($generated@@189 T@T) ) (! (= ($generated@@143 $generated@@189 $generated@@187 $generated@@188) (forall (($generated@@190 T@U) ) (! (= ($generated@@19 ($generated@@41 $generated@@189 $generated@@15 $generated@@187 $generated@@190)) ($generated@@19 ($generated@@41 $generated@@189 $generated@@15 $generated@@188 $generated@@190))) + :pattern ( ($generated@@41 $generated@@189 $generated@@15 $generated@@187 $generated@@190)) + :pattern ( ($generated@@41 $generated@@189 $generated@@15 $generated@@188 $generated@@190)) +))) + :pattern ( ($generated@@143 $generated@@189 $generated@@187 $generated@@188)) +))) +(assert (forall (($generated@@191 T@U) ($generated@@192 T@U) ($generated@@193 T@U) ($generated@@194 T@U) ) (! (= ($generated@@38 $generated@@47 $generated@@193 ($generated@@126 $generated@@191 $generated@@192) $generated@@194) ($generated@@38 $generated@@47 $generated@@193 ($generated@@117 $generated@@191 $generated@@192) $generated@@194)) + :pattern ( ($generated@@38 $generated@@47 $generated@@193 ($generated@@126 $generated@@191 $generated@@192) $generated@@194)) +))) +(assert (and (forall (($generated@@199 T@T) ($generated@@200 T@T) ($generated@@201 T@T) ($generated@@202 T@U) ($generated@@203 T@U) ($generated@@204 T@U) ($generated@@205 T@U) ) (! (= ($generated@@197 $generated@@199 $generated@@200 $generated@@201 ($generated@@198 $generated@@199 $generated@@200 $generated@@201 $generated@@203 $generated@@204 $generated@@205 $generated@@202) $generated@@204 $generated@@205) $generated@@202) + :weight 0 +)) (and (forall (($generated@@206 T@T) ($generated@@207 T@T) ($generated@@208 T@T) ($generated@@209 T@U) ($generated@@210 T@U) ($generated@@211 T@U) ($generated@@212 T@U) ($generated@@213 T@U) ($generated@@214 T@U) ) (! (or (= $generated@@211 $generated@@213) (= ($generated@@197 $generated@@206 $generated@@207 $generated@@208 ($generated@@198 $generated@@206 $generated@@207 $generated@@208 $generated@@210 $generated@@211 $generated@@212 $generated@@209) $generated@@213 $generated@@214) ($generated@@197 $generated@@206 $generated@@207 $generated@@208 $generated@@210 $generated@@213 $generated@@214))) + :weight 0 +)) (forall (($generated@@215 T@T) ($generated@@216 T@T) ($generated@@217 T@T) ($generated@@218 T@U) ($generated@@219 T@U) ($generated@@220 T@U) ($generated@@221 T@U) ($generated@@222 T@U) ($generated@@223 T@U) ) (! (or (= $generated@@221 $generated@@223) (= ($generated@@197 $generated@@215 $generated@@216 $generated@@217 ($generated@@198 $generated@@215 $generated@@216 $generated@@217 $generated@@219 $generated@@220 $generated@@221 $generated@@218) $generated@@222 $generated@@223) ($generated@@197 $generated@@215 $generated@@216 $generated@@217 $generated@@219 $generated@@222 $generated@@223))) + :weight 0 +))))) +(assert (forall (($generated@@224 T@U) ($generated@@225 T@U) ($generated@@226 T@U) ($generated@@227 T@U) ($generated@@228 T@U) ($generated@@229 T@U) ($generated@@230 T@U) ) (! (= ($generated@@195 $generated@@224 $generated@@225 $generated@@226 ($generated@@196 $generated@@227 $generated@@228 $generated@@229) $generated@@230) ($generated@@197 ($generated@@46 $generated@@77 ($generated@@78 $generated@@42)) $generated@@42 $generated@@42 $generated@@227 $generated@@226 $generated@@230)) + :pattern ( ($generated@@195 $generated@@224 $generated@@225 $generated@@226 ($generated@@196 $generated@@227 $generated@@228 $generated@@229) $generated@@230)) +))) +(assert (forall (($generated@@231 T@U) ) (! (=> ($generated@@44 $generated@@42 $generated@@231 $generated@@108) (and (= ($generated@@173 $generated@@77 ($generated@@75 $generated@@77 $generated@@231)) $generated@@231) ($generated@@36 $generated@@77 ($generated@@75 $generated@@77 $generated@@231) $generated@@108))) + :pattern ( ($generated@@44 $generated@@42 $generated@@231 $generated@@108)) +))) +(assert (forall (($generated@@232 T@U) ) (! (=> ($generated@@44 $generated@@42 $generated@@232 $generated@@125) (and (= ($generated@@173 $generated@@33 ($generated@@75 $generated@@33 $generated@@232)) $generated@@232) ($generated@@36 $generated@@33 ($generated@@75 $generated@@33 $generated@@232) $generated@@125))) + :pattern ( ($generated@@44 $generated@@42 $generated@@232 $generated@@125)) +))) +(assert (forall (($generated@@233 T@U) ($generated@@234 T@U) ($generated@@235 T@U) ($generated@@236 T@U) ) (! (=> (and ($generated@@34 $generated@@236) ($generated@@38 $generated@@47 $generated@@233 ($generated@@117 $generated@@234 $generated@@235) $generated@@236)) (forall (($generated@@237 T@U) ) (! (=> (and ($generated@@172 $generated@@42 $generated@@237 $generated@@234 $generated@@236) ($generated@@39 $generated@@234 $generated@@235 $generated@@236 $generated@@233 $generated@@237)) ($generated@@172 $generated@@42 ($generated@@195 $generated@@234 $generated@@235 $generated@@236 $generated@@233 $generated@@237) $generated@@235 $generated@@236)) + :pattern ( ($generated@@195 $generated@@234 $generated@@235 $generated@@236 $generated@@233 $generated@@237)) +))) + :pattern ( ($generated@@38 $generated@@47 $generated@@233 ($generated@@117 $generated@@234 $generated@@235) $generated@@236)) +))) +(assert (forall (($generated@@238 T@U) ($generated@@239 T@U) ($generated@@240 T@U) ($generated@@241 T@U) ) (! (=> ($generated@@34 $generated@@241) (= ($generated@@38 $generated@@47 $generated@@238 ($generated@@117 $generated@@239 $generated@@240) $generated@@241) (forall (($generated@@242 T@U) ) (! (=> (and (and ($generated@@44 $generated@@42 $generated@@242 $generated@@239) ($generated@@172 $generated@@42 $generated@@242 $generated@@239 $generated@@241)) ($generated@@39 $generated@@239 $generated@@240 $generated@@241 $generated@@238 $generated@@242)) (forall (($generated@@243 T@U) ) (! (=> (and (or (not (= $generated@@243 $generated@@109)) (not true)) ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 ($generated@@141 $generated@@239 $generated@@240 $generated@@241 $generated@@238 $generated@@242) ($generated@@173 $generated@@77 $generated@@243)))) ($generated@@19 ($generated@@75 $generated@@15 ($generated@@76 $generated@@15 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@241 $generated@@243) $generated@@1)))) + :pattern ( ($generated@@41 $generated@@42 $generated@@15 ($generated@@141 $generated@@239 $generated@@240 $generated@@241 $generated@@238 $generated@@242) ($generated@@173 $generated@@77 $generated@@243))) +))) + :pattern ( ($generated@@195 $generated@@239 $generated@@240 $generated@@241 $generated@@238 $generated@@242)) + :pattern ( ($generated@@141 $generated@@239 $generated@@240 $generated@@241 $generated@@238 $generated@@242)) +)))) + :pattern ( ($generated@@38 $generated@@47 $generated@@238 ($generated@@117 $generated@@239 $generated@@240) $generated@@241)) +))) +(assert (forall (($generated@@245 Bool) ($generated@@246 T@U) ) (! (= ($generated@@19 ($generated@@41 $generated@@77 $generated@@15 ($generated@@244 $generated@@245) $generated@@246)) $generated@@245) + :pattern ( ($generated@@41 $generated@@77 $generated@@15 ($generated@@244 $generated@@245) $generated@@246)) +))) +(assert (forall (($generated@@248 T@U) ($generated@@249 T@U) ) (! (= ($generated@@41 $generated@@163 $generated@@47 ($generated@@247 $generated@@248) $generated@@249) $generated@@248) + :pattern ( ($generated@@41 $generated@@163 $generated@@47 ($generated@@247 $generated@@248) $generated@@249)) +))) +(assert (forall (($generated@@250 T@U) ($generated@@251 T@U) ($generated@@252 T@U) ) (! (= ($generated@@38 ($generated@@46 $generated@@42 $generated@@15) $generated@@250 ($generated@@131 $generated@@251) $generated@@252) (forall (($generated@@253 T@U) ) (! (=> ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 $generated@@250 $generated@@253)) ($generated@@172 $generated@@42 $generated@@253 $generated@@251 $generated@@252)) + :pattern ( ($generated@@41 $generated@@42 $generated@@15 $generated@@250 $generated@@253)) +))) + :pattern ( ($generated@@38 ($generated@@46 $generated@@42 $generated@@15) $generated@@250 ($generated@@131 $generated@@251) $generated@@252)) +))) +(assert (forall (($generated@@254 T@U) ($generated@@255 T@U) ($generated@@256 T@U) ) (! (= ($generated@@38 ($generated@@46 $generated@@42 $generated@@15) $generated@@254 ($generated@@135 $generated@@255) $generated@@256) (forall (($generated@@257 T@U) ) (! (=> ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 $generated@@254 $generated@@257)) ($generated@@172 $generated@@42 $generated@@257 $generated@@255 $generated@@256)) + :pattern ( ($generated@@41 $generated@@42 $generated@@15 $generated@@254 $generated@@257)) +))) + :pattern ( ($generated@@38 ($generated@@46 $generated@@42 $generated@@15) $generated@@254 ($generated@@135 $generated@@255) $generated@@256)) +))) +(assert (forall (($generated@@258 T@U) ($generated@@259 T@U) ($generated@@260 T@U) ($generated@@261 T@U) ($generated@@262 T@U) ($generated@@263 T@U) ($generated@@264 T@U) ($generated@@265 T@U) ) (! (= ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 ($generated@@141 $generated@@258 $generated@@259 $generated@@260 ($generated@@196 $generated@@261 $generated@@262 $generated@@263) $generated@@264) $generated@@265)) ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 ($generated@@197 ($generated@@46 $generated@@77 ($generated@@78 $generated@@42)) $generated@@42 ($generated@@46 $generated@@42 $generated@@15) $generated@@263 $generated@@260 $generated@@264) $generated@@265))) + :pattern ( ($generated@@41 $generated@@42 $generated@@15 ($generated@@141 $generated@@258 $generated@@259 $generated@@260 ($generated@@196 $generated@@261 $generated@@262 $generated@@263) $generated@@264) $generated@@265)) +))) +(assert (forall (($generated@@266 T@U) ($generated@@267 T@U) ($generated@@268 T@T) ) (! (=> ($generated@@143 $generated@@268 $generated@@266 $generated@@267) (= $generated@@266 $generated@@267)) + :pattern ( ($generated@@143 $generated@@268 $generated@@266 $generated@@267)) +))) +(assert (=> (<= 0 $generated@@30) (forall (($generated@@269 T@U) ($generated@@270 T@U) ($generated@@271 T@U) ($generated@@272 T@U) ) (! (=> (or ($generated@@35 $generated@@269 $generated@@270 $generated@@272) (and (< 0 $generated@@30) (and ($generated@@34 $generated@@271) (and ($generated@@36 $generated@@33 $generated@@272 ($generated@@37 $generated@@269 $generated@@270)) ($generated@@38 $generated@@33 $generated@@272 ($generated@@37 $generated@@269 $generated@@270) $generated@@271))))) (and (forall (($generated@@273 T@U) ) (! (=> ($generated@@44 $generated@@42 $generated@@273 $generated@@269) (and ($generated@@45 $generated@@272) (=> ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 ($generated@@43 $generated@@272) $generated@@273)) (and ($generated@@45 $generated@@272) true)))) + :pattern ( ($generated@@39 $generated@@269 $generated@@270 $generated@@271 ($generated@@40 $generated@@272) $generated@@273)) + :pattern ( ($generated@@41 $generated@@42 $generated@@15 ($generated@@43 $generated@@272) $generated@@273)) +)) (= ($generated@@31 $generated@@269 $generated@@270 $generated@@272) (forall (($generated@@274 T@U) ) (! (=> (and ($generated@@44 $generated@@42 $generated@@274 $generated@@269) ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 ($generated@@43 $generated@@272) $generated@@274))) ($generated@@39 $generated@@269 $generated@@270 $generated@@271 ($generated@@40 $generated@@272) $generated@@274)) + :pattern ( ($generated@@39 $generated@@269 $generated@@270 $generated@@271 ($generated@@40 $generated@@272) $generated@@274)) + :pattern ( ($generated@@41 $generated@@42 $generated@@15 ($generated@@43 $generated@@272) $generated@@274)) +))))) + :pattern ( ($generated@@31 $generated@@269 $generated@@270 $generated@@272) ($generated@@34 $generated@@271)) +)))) +(assert (forall (($generated@@275 T@U) ($generated@@276 T@U) ($generated@@277 T@U) ) (! (=> (or (not (= $generated@@275 $generated@@277)) (not true)) (=> (and ($generated@@74 $generated@@275 $generated@@276) ($generated@@74 $generated@@276 $generated@@277)) ($generated@@74 $generated@@275 $generated@@277))) + :pattern ( ($generated@@74 $generated@@275 $generated@@276) ($generated@@74 $generated@@276 $generated@@277)) +))) +(assert (forall (($generated@@278 T@U) ($generated@@279 T@U) ($generated@@280 T@U) ) (! (= ($generated@@36 $generated@@47 $generated@@278 ($generated@@117 $generated@@279 $generated@@280)) (forall (($generated@@281 T@U) ($generated@@282 T@U) ) (! (=> (and (and ($generated@@34 $generated@@281) ($generated@@44 $generated@@42 $generated@@282 $generated@@279)) ($generated@@39 $generated@@279 $generated@@280 $generated@@281 $generated@@278 $generated@@282)) ($generated@@44 $generated@@42 ($generated@@195 $generated@@279 $generated@@280 $generated@@281 $generated@@278 $generated@@282) $generated@@280)) + :pattern ( ($generated@@195 $generated@@279 $generated@@280 $generated@@281 $generated@@278 $generated@@282)) +))) + :pattern ( ($generated@@36 $generated@@47 $generated@@278 ($generated@@117 $generated@@279 $generated@@280))) +))) +(assert (forall (($generated@@283 T@U) ($generated@@284 T@U) ($generated@@285 T@T) ) (! (= ($generated@@44 $generated@@42 ($generated@@173 $generated@@285 $generated@@283) $generated@@284) ($generated@@36 $generated@@285 $generated@@283 $generated@@284)) + :pattern ( ($generated@@44 $generated@@42 ($generated@@173 $generated@@285 $generated@@283) $generated@@284)) +))) +(assert (forall (($generated@@286 T@U) ($generated@@287 T@U) ($generated@@288 T@U) ($generated@@289 T@U) ($generated@@290 T@U) ($generated@@291 T@U) ($generated@@292 T@U) ) (! (=> ($generated@@19 ($generated@@197 ($generated@@46 $generated@@77 ($generated@@78 $generated@@42)) $generated@@42 $generated@@15 $generated@@290 $generated@@288 $generated@@292)) ($generated@@39 $generated@@286 $generated@@287 $generated@@288 ($generated@@196 $generated@@289 $generated@@290 $generated@@291) $generated@@292)) + :pattern ( ($generated@@39 $generated@@286 $generated@@287 $generated@@288 ($generated@@196 $generated@@289 $generated@@290 $generated@@291) $generated@@292)) +))) +(assert (forall (($generated@@294 T@U) ($generated@@295 T@U) ) (! (= ($generated@@293 ($generated@@117 $generated@@294 $generated@@295)) $generated@@294) + :pattern ( ($generated@@117 $generated@@294 $generated@@295)) +))) +(assert (forall (($generated@@297 T@U) ($generated@@298 T@U) ) (! (= ($generated@@296 ($generated@@117 $generated@@297 $generated@@298)) $generated@@298) + :pattern ( ($generated@@117 $generated@@297 $generated@@298)) +))) +(assert (forall (($generated@@300 T@U) ($generated@@301 T@U) ) (! (= ($generated@@299 ($generated@@126 $generated@@300 $generated@@301)) $generated@@300) + :pattern ( ($generated@@126 $generated@@300 $generated@@301)) +))) +(assert (forall (($generated@@303 T@U) ($generated@@304 T@U) ) (! (= ($generated@@302 ($generated@@126 $generated@@303 $generated@@304)) $generated@@304) + :pattern ( ($generated@@126 $generated@@303 $generated@@304)) +))) +(assert (forall (($generated@@305 T@U) ($generated@@306 T@U) ) (! (= ($generated@@115 ($generated@@150 $generated@@305 $generated@@306)) $generated@@7) + :pattern ( ($generated@@150 $generated@@305 $generated@@306)) +))) +(assert (forall (($generated@@308 T@U) ($generated@@309 T@U) ) (! (= ($generated@@307 ($generated@@37 $generated@@308 $generated@@309)) $generated@@308) + :pattern ( ($generated@@37 $generated@@308 $generated@@309)) +))) +(assert (forall (($generated@@311 T@U) ($generated@@312 T@U) ) (! (= ($generated@@310 ($generated@@37 $generated@@311 $generated@@312)) $generated@@312) + :pattern ( ($generated@@37 $generated@@311 $generated@@312)) +))) +(assert (forall (($generated@@313 T@U) ($generated@@314 T@U) ) (! (= ($generated@@43 ($generated@@150 $generated@@313 $generated@@314)) $generated@@313) + :pattern ( ($generated@@150 $generated@@313 $generated@@314)) +))) +(assert (forall (($generated@@315 T@U) ($generated@@316 T@U) ) (! (= ($generated@@40 ($generated@@150 $generated@@315 $generated@@316)) $generated@@316) + :pattern ( ($generated@@150 $generated@@315 $generated@@316)) +))) +(assert (forall (($generated@@317 T@U) ) (! ($generated@@36 $generated@@77 $generated@@317 $generated@@108) + :pattern ( ($generated@@36 $generated@@77 $generated@@317 $generated@@108)) +))) +(assert (and (forall (($generated@@321 T@T) ($generated@@322 T@T) ($generated@@323 T@T) ($generated@@324 T@U) ($generated@@325 T@U) ($generated@@326 T@U) ($generated@@327 T@U) ) (! (= ($generated@@318 $generated@@321 $generated@@322 $generated@@323 ($generated@@320 $generated@@321 $generated@@322 $generated@@323 $generated@@325 $generated@@326 $generated@@327 $generated@@324) $generated@@326 $generated@@327) $generated@@324) + :weight 0 +)) (and (and (forall (($generated@@328 T@T) ($generated@@329 T@T) ($generated@@330 T@T) ($generated@@331 T@T) ($generated@@332 T@U) ($generated@@333 T@U) ($generated@@334 T@U) ($generated@@335 T@U) ($generated@@336 T@U) ($generated@@337 T@U) ) (! (or (= $generated@@330 $generated@@331) (= ($generated@@318 $generated@@331 $generated@@328 $generated@@329 ($generated@@320 $generated@@330 $generated@@328 $generated@@329 $generated@@333 $generated@@334 $generated@@335 $generated@@332) $generated@@336 $generated@@337) ($generated@@318 $generated@@331 $generated@@328 $generated@@329 $generated@@333 $generated@@336 $generated@@337))) + :weight 0 +)) (forall (($generated@@338 T@T) ($generated@@339 T@T) ($generated@@340 T@T) ($generated@@341 T@T) ($generated@@342 T@U) ($generated@@343 T@U) ($generated@@344 T@U) ($generated@@345 T@U) ($generated@@346 T@U) ($generated@@347 T@U) ) (! (or (= $generated@@344 $generated@@346) (= ($generated@@318 $generated@@341 $generated@@338 $generated@@339 ($generated@@320 $generated@@340 $generated@@338 $generated@@339 $generated@@343 $generated@@344 $generated@@345 $generated@@342) $generated@@346 $generated@@347) ($generated@@318 $generated@@341 $generated@@338 $generated@@339 $generated@@343 $generated@@346 $generated@@347))) + :weight 0 +))) (forall (($generated@@348 T@T) ($generated@@349 T@T) ($generated@@350 T@T) ($generated@@351 T@T) ($generated@@352 T@U) ($generated@@353 T@U) ($generated@@354 T@U) ($generated@@355 T@U) ($generated@@356 T@U) ($generated@@357 T@U) ) (! (or (= $generated@@355 $generated@@357) (= ($generated@@318 $generated@@351 $generated@@348 $generated@@349 ($generated@@320 $generated@@350 $generated@@348 $generated@@349 $generated@@353 $generated@@354 $generated@@355 $generated@@352) $generated@@356 $generated@@357) ($generated@@318 $generated@@351 $generated@@348 $generated@@349 $generated@@353 $generated@@356 $generated@@357))) + :weight 0 +))))) +(assert (forall (($generated@@358 T@U) ($generated@@359 T@U) ($generated@@360 T@U) ($generated@@361 Bool) ($generated@@362 T@U) ($generated@@363 T@U) ($generated@@364 T@T) ) (! (= ($generated@@19 ($generated@@318 $generated@@364 $generated@@77 $generated@@15 ($generated@@319 $generated@@358 $generated@@359 $generated@@360 $generated@@361) $generated@@362 $generated@@363)) (=> (and (or (not (= $generated@@362 $generated@@358)) (not true)) ($generated@@19 ($generated@@75 $generated@@15 ($generated@@76 $generated@@15 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@359 $generated@@362) $generated@@360)))) $generated@@361)) + :pattern ( ($generated@@318 $generated@@364 $generated@@77 $generated@@15 ($generated@@319 $generated@@358 $generated@@359 $generated@@360 $generated@@361) $generated@@362 $generated@@363)) +))) +(assert (forall (($generated@@366 T@U) ($generated@@367 T@U) ($generated@@368 T@U) ($generated@@369 Bool) ($generated@@370 T@U) ($generated@@371 T@U) ($generated@@372 T@T) ) (! (= ($generated@@19 ($generated@@318 $generated@@372 $generated@@77 $generated@@15 ($generated@@365 $generated@@366 $generated@@367 $generated@@368 $generated@@369) $generated@@370 $generated@@371)) (=> (and (or (not (= $generated@@370 $generated@@366)) (not true)) ($generated@@19 ($generated@@75 $generated@@15 ($generated@@76 $generated@@15 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@367 $generated@@370) $generated@@368)))) $generated@@369)) + :pattern ( ($generated@@318 $generated@@372 $generated@@77 $generated@@15 ($generated@@365 $generated@@366 $generated@@367 $generated@@368 $generated@@369) $generated@@370 $generated@@371)) +))) +(assert (forall (($generated@@374 T@U) ) (! (= ($generated@@373 ($generated@@131 $generated@@374)) $generated@@374) + :pattern ( ($generated@@131 $generated@@374)) +))) +(assert (forall (($generated@@376 T@U) ) (! (= ($generated@@375 ($generated@@131 $generated@@376)) $generated) + :pattern ( ($generated@@131 $generated@@376)) +))) +(assert (forall (($generated@@378 T@U) ) (! (= ($generated@@377 ($generated@@135 $generated@@378)) $generated@@378) + :pattern ( ($generated@@135 $generated@@378)) +))) +(assert (forall (($generated@@379 T@U) ) (! (= ($generated@@375 ($generated@@135 $generated@@379)) $generated@@0) + :pattern ( ($generated@@135 $generated@@379)) +))) +(assert (forall (($generated@@380 T@U) ($generated@@381 T@T) ) (! (= ($generated@@75 $generated@@381 ($generated@@173 $generated@@381 $generated@@380)) $generated@@380) + :pattern ( ($generated@@173 $generated@@381 $generated@@380)) +))) +(assert (forall (($generated@@383 T@U) ($generated@@384 T@U) ($generated@@385 T@U) ) (! (=> ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 $generated@@383 ($generated@@173 $generated@@33 $generated@@385))) (< ($generated@@382 $generated@@385) ($generated@@382 ($generated@@150 $generated@@383 $generated@@384)))) + :pattern ( ($generated@@41 $generated@@42 $generated@@15 $generated@@383 ($generated@@173 $generated@@33 $generated@@385)) ($generated@@150 $generated@@383 $generated@@384)) +))) +(assert (forall (($generated@@386 T@U) ($generated@@387 T@U) ($generated@@388 T@U) ($generated@@389 T@U) ($generated@@390 T@U) ($generated@@391 T@U) ) (! (=> (and (and (and ($generated@@74 $generated@@388 $generated@@389) (and ($generated@@34 $generated@@388) ($generated@@34 $generated@@389))) (and ($generated@@44 $generated@@42 $generated@@391 $generated@@386) ($generated@@36 $generated@@47 $generated@@390 ($generated@@117 $generated@@386 $generated@@387)))) (forall (($generated@@392 T@U) ($generated@@393 T@U) ($generated@@394 T@T) ) (=> (and (or (not (= $generated@@392 $generated@@109)) (not true)) ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 ($generated@@141 $generated@@386 $generated@@387 $generated@@388 $generated@@390 $generated@@391) ($generated@@173 $generated@@77 $generated@@392)))) (= ($generated@@75 $generated@@394 ($generated@@76 $generated@@394 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@388 $generated@@392) $generated@@393)) ($generated@@75 $generated@@394 ($generated@@76 $generated@@394 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@389 $generated@@392) $generated@@393)))))) (= ($generated@@39 $generated@@386 $generated@@387 $generated@@388 $generated@@390 $generated@@391) ($generated@@39 $generated@@386 $generated@@387 $generated@@389 $generated@@390 $generated@@391))) + :pattern ( ($generated@@74 $generated@@388 $generated@@389) ($generated@@39 $generated@@386 $generated@@387 $generated@@389 $generated@@390 $generated@@391)) +))) +(assert (forall (($generated@@395 T@U) ($generated@@396 T@U) ($generated@@397 T@U) ($generated@@398 T@U) ($generated@@399 T@U) ($generated@@400 T@U) ) (! (=> (and (and (and ($generated@@74 $generated@@397 $generated@@398) (and ($generated@@34 $generated@@397) ($generated@@34 $generated@@398))) (and ($generated@@44 $generated@@42 $generated@@400 $generated@@395) ($generated@@36 $generated@@47 $generated@@399 ($generated@@117 $generated@@395 $generated@@396)))) (forall (($generated@@401 T@U) ($generated@@402 T@U) ($generated@@403 T@T) ) (=> (and (or (not (= $generated@@401 $generated@@109)) (not true)) ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 ($generated@@141 $generated@@395 $generated@@396 $generated@@398 $generated@@399 $generated@@400) ($generated@@173 $generated@@77 $generated@@401)))) (= ($generated@@75 $generated@@403 ($generated@@76 $generated@@403 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@397 $generated@@401) $generated@@402)) ($generated@@75 $generated@@403 ($generated@@76 $generated@@403 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@398 $generated@@401) $generated@@402)))))) (= ($generated@@39 $generated@@395 $generated@@396 $generated@@397 $generated@@399 $generated@@400) ($generated@@39 $generated@@395 $generated@@396 $generated@@398 $generated@@399 $generated@@400))) + :pattern ( ($generated@@74 $generated@@397 $generated@@398) ($generated@@39 $generated@@395 $generated@@396 $generated@@398 $generated@@399 $generated@@400)) +))) +(assert (forall (($generated@@404 T@U) ($generated@@405 T@U) ($generated@@406 T@U) ) (! (= ($generated@@36 $generated@@47 $generated@@406 ($generated@@126 $generated@@404 $generated@@405)) (and ($generated@@36 $generated@@47 $generated@@406 ($generated@@117 $generated@@404 $generated@@405)) (forall (($generated@@407 T@U) ) (=> ($generated@@44 $generated@@42 $generated@@407 $generated@@404) ($generated@@143 $generated@@42 ($generated@@141 $generated@@404 $generated@@405 $generated@@142 $generated@@406 $generated@@407) ($generated@@144 $generated@@42)))))) + :pattern ( ($generated@@36 $generated@@47 $generated@@406 ($generated@@126 $generated@@404 $generated@@405))) +))) +(assert (forall (($generated@@409 T@U) ($generated@@410 T@U) ($generated@@411 T@T) ) (! (= ($generated@@162 $generated@@411 $generated@@409 ($generated@@408 $generated@@410)) ($generated@@162 $generated@@411 $generated@@409 $generated@@410)) + :pattern ( ($generated@@162 $generated@@411 $generated@@409 ($generated@@408 $generated@@410))) +))) +(assert (forall (($generated@@412 T@U) ($generated@@413 T@U) ($generated@@414 T@U) ) (! (=> ($generated@@44 $generated@@42 $generated@@414 ($generated@@117 $generated@@412 $generated@@413)) (and (= ($generated@@173 $generated@@47 ($generated@@75 $generated@@47 $generated@@414)) $generated@@414) ($generated@@36 $generated@@47 ($generated@@75 $generated@@47 $generated@@414) ($generated@@117 $generated@@412 $generated@@413)))) + :pattern ( ($generated@@44 $generated@@42 $generated@@414 ($generated@@117 $generated@@412 $generated@@413))) +))) +(assert (forall (($generated@@415 T@U) ($generated@@416 T@U) ($generated@@417 T@U) ) (! (=> ($generated@@44 $generated@@42 $generated@@417 ($generated@@126 $generated@@415 $generated@@416)) (and (= ($generated@@173 $generated@@47 ($generated@@75 $generated@@47 $generated@@417)) $generated@@417) ($generated@@36 $generated@@47 ($generated@@75 $generated@@47 $generated@@417) ($generated@@126 $generated@@415 $generated@@416)))) + :pattern ( ($generated@@44 $generated@@42 $generated@@417 ($generated@@126 $generated@@415 $generated@@416))) +))) +(assert (forall (($generated@@418 T@U) ($generated@@419 T@U) ($generated@@420 T@U) ) (! (=> ($generated@@44 $generated@@42 $generated@@420 ($generated@@37 $generated@@418 $generated@@419)) (and (= ($generated@@173 $generated@@33 ($generated@@75 $generated@@33 $generated@@420)) $generated@@420) ($generated@@36 $generated@@33 ($generated@@75 $generated@@33 $generated@@420) ($generated@@37 $generated@@418 $generated@@419)))) + :pattern ( ($generated@@44 $generated@@42 $generated@@420 ($generated@@37 $generated@@418 $generated@@419))) +))) +(assert (forall (($generated@@421 T@U) ($generated@@422 T@T) ) (! (not ($generated@@19 ($generated@@41 $generated@@422 $generated@@15 ($generated@@144 $generated@@422) $generated@@421))) + :pattern ( ($generated@@41 $generated@@422 $generated@@15 ($generated@@144 $generated@@422) $generated@@421)) +))) +(assert (forall (($generated@@424 T@U) ($generated@@425 T@T) ) (! (not ($generated@@19 ($generated@@41 $generated@@425 $generated@@15 ($generated@@423 $generated@@425) $generated@@424))) + :pattern ( ($generated@@41 $generated@@425 $generated@@15 ($generated@@423 $generated@@425) $generated@@424)) +))) +(assert (forall (($generated@@427 T@U) ($generated@@428 T@U) ) (! (and (= ($generated@@375 ($generated@@117 $generated@@427 $generated@@428)) $generated@@3) (= ($generated@@426 ($generated@@117 $generated@@427 $generated@@428)) $generated@@10)) + :pattern ( ($generated@@117 $generated@@427 $generated@@428)) +))) +(assert (forall (($generated@@429 T@U) ($generated@@430 T@U) ) (! (and (= ($generated@@375 ($generated@@126 $generated@@429 $generated@@430)) $generated@@4) (= ($generated@@426 ($generated@@126 $generated@@429 $generated@@430)) $generated@@11)) + :pattern ( ($generated@@126 $generated@@429 $generated@@430)) +))) +(assert (forall (($generated@@431 T@U) ($generated@@432 T@U) ) (! (and (= ($generated@@375 ($generated@@37 $generated@@431 $generated@@432)) $generated@@8) (= ($generated@@426 ($generated@@37 $generated@@431 $generated@@432)) $generated@@13)) + :pattern ( ($generated@@37 $generated@@431 $generated@@432)) +))) +(assert (forall (($generated@@433 T@U) ($generated@@434 T@U) ($generated@@435 T@U) ($generated@@436 T@U) ($generated@@437 T@U) ) (! (=> (and (and ($generated@@34 $generated@@435) (and ($generated@@44 $generated@@42 $generated@@437 $generated@@433) ($generated@@36 $generated@@47 $generated@@436 ($generated@@117 $generated@@433 $generated@@434)))) ($generated@@143 $generated@@42 ($generated@@141 $generated@@433 $generated@@434 $generated@@142 $generated@@436 $generated@@437) ($generated@@144 $generated@@42))) (= ($generated@@39 $generated@@433 $generated@@434 $generated@@142 $generated@@436 $generated@@437) ($generated@@39 $generated@@433 $generated@@434 $generated@@435 $generated@@436 $generated@@437))) + :pattern ( ($generated@@39 $generated@@433 $generated@@434 $generated@@142 $generated@@436 $generated@@437) ($generated@@34 $generated@@435)) + :pattern ( ($generated@@39 $generated@@433 $generated@@434 $generated@@435 $generated@@436 $generated@@437)) +))) +(assert (forall (($generated@@438 T@U) ($generated@@439 T@U) ($generated@@440 T@U) ($generated@@441 T@U) ($generated@@442 T@U) ($generated@@443 T@U) ) (! (=> (and (and (and ($generated@@74 $generated@@440 $generated@@441) (and ($generated@@34 $generated@@440) ($generated@@34 $generated@@441))) (and ($generated@@44 $generated@@42 $generated@@443 $generated@@438) ($generated@@36 $generated@@47 $generated@@442 ($generated@@117 $generated@@438 $generated@@439)))) (forall (($generated@@444 T@U) ($generated@@445 T@U) ($generated@@446 T@T) ) (=> (and (or (not (= $generated@@444 $generated@@109)) (not true)) ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 ($generated@@141 $generated@@438 $generated@@439 $generated@@440 $generated@@442 $generated@@443) ($generated@@173 $generated@@77 $generated@@444)))) (= ($generated@@75 $generated@@446 ($generated@@76 $generated@@446 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@440 $generated@@444) $generated@@445)) ($generated@@75 $generated@@446 ($generated@@76 $generated@@446 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@441 $generated@@444) $generated@@445)))))) (= ($generated@@141 $generated@@438 $generated@@439 $generated@@440 $generated@@442 $generated@@443) ($generated@@141 $generated@@438 $generated@@439 $generated@@441 $generated@@442 $generated@@443))) + :pattern ( ($generated@@74 $generated@@440 $generated@@441) ($generated@@141 $generated@@438 $generated@@439 $generated@@441 $generated@@442 $generated@@443)) +))) +(assert (forall (($generated@@447 T@U) ($generated@@448 T@U) ($generated@@449 T@U) ($generated@@450 T@U) ($generated@@451 T@U) ($generated@@452 T@U) ) (! (=> (and (and (and ($generated@@74 $generated@@449 $generated@@450) (and ($generated@@34 $generated@@449) ($generated@@34 $generated@@450))) (and ($generated@@44 $generated@@42 $generated@@452 $generated@@447) ($generated@@36 $generated@@47 $generated@@451 ($generated@@117 $generated@@447 $generated@@448)))) (forall (($generated@@453 T@U) ($generated@@454 T@U) ($generated@@455 T@T) ) (=> (and (or (not (= $generated@@453 $generated@@109)) (not true)) ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 ($generated@@141 $generated@@447 $generated@@448 $generated@@450 $generated@@451 $generated@@452) ($generated@@173 $generated@@77 $generated@@453)))) (= ($generated@@75 $generated@@455 ($generated@@76 $generated@@455 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@449 $generated@@453) $generated@@454)) ($generated@@75 $generated@@455 ($generated@@76 $generated@@455 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@450 $generated@@453) $generated@@454)))))) (= ($generated@@141 $generated@@447 $generated@@448 $generated@@449 $generated@@451 $generated@@452) ($generated@@141 $generated@@447 $generated@@448 $generated@@450 $generated@@451 $generated@@452))) + :pattern ( ($generated@@74 $generated@@449 $generated@@450) ($generated@@141 $generated@@447 $generated@@448 $generated@@450 $generated@@451 $generated@@452)) +))) +(assert (forall (($generated@@456 T@U) ($generated@@457 T@U) ($generated@@458 T@U) ($generated@@459 T@U) ($generated@@460 T@U) ($generated@@461 T@U) ) (! (=> (and (and (and ($generated@@74 $generated@@458 $generated@@459) (and ($generated@@34 $generated@@458) ($generated@@34 $generated@@459))) (and ($generated@@44 $generated@@42 $generated@@461 $generated@@456) ($generated@@36 $generated@@47 $generated@@460 ($generated@@117 $generated@@456 $generated@@457)))) (forall (($generated@@462 T@U) ($generated@@463 T@U) ($generated@@464 T@T) ) (=> (and (or (not (= $generated@@462 $generated@@109)) (not true)) ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 ($generated@@141 $generated@@456 $generated@@457 $generated@@458 $generated@@460 $generated@@461) ($generated@@173 $generated@@77 $generated@@462)))) (= ($generated@@75 $generated@@464 ($generated@@76 $generated@@464 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@458 $generated@@462) $generated@@463)) ($generated@@75 $generated@@464 ($generated@@76 $generated@@464 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@459 $generated@@462) $generated@@463)))))) (= ($generated@@195 $generated@@456 $generated@@457 $generated@@458 $generated@@460 $generated@@461) ($generated@@195 $generated@@456 $generated@@457 $generated@@459 $generated@@460 $generated@@461))) + :pattern ( ($generated@@74 $generated@@458 $generated@@459) ($generated@@195 $generated@@456 $generated@@457 $generated@@459 $generated@@460 $generated@@461)) +))) +(assert (forall (($generated@@465 T@U) ($generated@@466 T@U) ($generated@@467 T@U) ($generated@@468 T@U) ($generated@@469 T@U) ($generated@@470 T@U) ) (! (=> (and (and (and ($generated@@74 $generated@@467 $generated@@468) (and ($generated@@34 $generated@@467) ($generated@@34 $generated@@468))) (and ($generated@@44 $generated@@42 $generated@@470 $generated@@465) ($generated@@36 $generated@@47 $generated@@469 ($generated@@117 $generated@@465 $generated@@466)))) (forall (($generated@@471 T@U) ($generated@@472 T@U) ($generated@@473 T@T) ) (=> (and (or (not (= $generated@@471 $generated@@109)) (not true)) ($generated@@19 ($generated@@41 $generated@@42 $generated@@15 ($generated@@141 $generated@@465 $generated@@466 $generated@@468 $generated@@469 $generated@@470) ($generated@@173 $generated@@77 $generated@@471)))) (= ($generated@@75 $generated@@473 ($generated@@76 $generated@@473 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@467 $generated@@471) $generated@@472)) ($generated@@75 $generated@@473 ($generated@@76 $generated@@473 $generated@@42 ($generated@@41 $generated@@77 ($generated@@78 $generated@@42) $generated@@468 $generated@@471) $generated@@472)))))) (= ($generated@@195 $generated@@465 $generated@@466 $generated@@467 $generated@@469 $generated@@470) ($generated@@195 $generated@@465 $generated@@466 $generated@@468 $generated@@469 $generated@@470))) + :pattern ( ($generated@@74 $generated@@467 $generated@@468) ($generated@@195 $generated@@465 $generated@@466 $generated@@468 $generated@@469 $generated@@470)) +))) +(assert (forall (($generated@@474 T@U) ($generated@@475 T@U) ) (! (=> ($generated@@44 $generated@@42 $generated@@474 ($generated@@131 $generated@@475)) (and (= ($generated@@173 ($generated@@46 $generated@@42 $generated@@15) ($generated@@75 ($generated@@46 $generated@@42 $generated@@15) $generated@@474)) $generated@@474) ($generated@@36 ($generated@@46 $generated@@42 $generated@@15) ($generated@@75 ($generated@@46 $generated@@42 $generated@@15) $generated@@474) ($generated@@131 $generated@@475)))) + :pattern ( ($generated@@44 $generated@@42 $generated@@474 ($generated@@131 $generated@@475))) +))) +(assert (forall (($generated@@476 T@U) ($generated@@477 T@U) ) (! (=> ($generated@@44 $generated@@42 $generated@@476 ($generated@@135 $generated@@477)) (and (= ($generated@@173 ($generated@@46 $generated@@42 $generated@@15) ($generated@@75 ($generated@@46 $generated@@42 $generated@@15) $generated@@476)) $generated@@476) ($generated@@36 ($generated@@46 $generated@@42 $generated@@15) ($generated@@75 ($generated@@46 $generated@@42 $generated@@15) $generated@@476) ($generated@@135 $generated@@477)))) + :pattern ( ($generated@@44 $generated@@42 $generated@@476 ($generated@@135 $generated@@477))) +))) +(assert (forall (($generated@@478 T@U) ($generated@@479 T@U) ) (! (=> (and ($generated@@34 $generated@@479) ($generated@@36 $generated@@33 $generated@@478 $generated@@125)) ($generated@@38 $generated@@33 $generated@@478 $generated@@125 $generated@@479)) + :pattern ( ($generated@@38 $generated@@33 $generated@@478 $generated@@125 $generated@@479)) +))) +(assert (= ($generated@@375 $generated@@108) $generated@@2)) +(assert (= ($generated@@426 $generated@@108) $generated@@9)) +(assert (= ($generated@@375 $generated@@125) $generated@@6)) +(assert (= ($generated@@426 $generated@@125) $generated@@12)) +(assert (= $generated@@116 ($generated@@32 $generated@@33 $generated@@116))) +(assert (forall (($generated@@480 T@U) ) (! ($generated@@36 ($generated@@46 $generated@@42 $generated@@15) ($generated@@159 $generated@@480) ($generated@@131 $generated@@108)) + :pattern ( ($generated@@159 $generated@@480)) +))) +(assert (forall (($generated@@481 T@U) ($generated@@482 T@U) ) (! (= ($generated@@150 ($generated@@32 ($generated@@46 $generated@@42 $generated@@15) $generated@@481) ($generated@@32 $generated@@47 $generated@@482)) ($generated@@32 $generated@@33 ($generated@@150 $generated@@481 $generated@@482))) + :pattern ( ($generated@@150 ($generated@@32 ($generated@@46 $generated@@42 $generated@@15) $generated@@481) ($generated@@32 $generated@@47 $generated@@482))) +))) +(assert (forall (($generated@@483 T@U) ($generated@@484 T@T) ) (! (= ($generated@@173 $generated@@484 ($generated@@32 $generated@@484 $generated@@483)) ($generated@@32 $generated@@42 ($generated@@173 $generated@@484 $generated@@483))) + :pattern ( ($generated@@173 $generated@@484 ($generated@@32 $generated@@484 $generated@@483))) +))) +(assert (forall (($generated@@485 T@U) ($generated@@486 T@U) ($generated@@487 T@U) ) (! (=> (and ($generated@@34 $generated@@487) (and ($generated@@45 $generated@@485) (exists (($generated@@488 T@U) ) (! ($generated@@38 $generated@@33 $generated@@485 ($generated@@37 $generated@@486 $generated@@488) $generated@@487) + :pattern ( ($generated@@38 $generated@@33 $generated@@485 ($generated@@37 $generated@@486 $generated@@488) $generated@@487)) +)))) ($generated@@38 ($generated@@46 $generated@@42 $generated@@15) ($generated@@43 $generated@@485) ($generated@@135 $generated@@486) $generated@@487)) + :pattern ( ($generated@@38 ($generated@@46 $generated@@42 $generated@@15) ($generated@@43 $generated@@485) ($generated@@135 $generated@@486) $generated@@487)) +))) +(assert (forall (($generated@@490 T@U) ($generated@@491 T@U) ($generated@@492 T@U) ) (! (= ($generated@@197 ($generated@@46 $generated@@77 ($generated@@78 $generated@@42)) $generated@@42 ($generated@@46 $generated@@42 $generated@@15) ($generated@@489 $generated@@490) $generated@@491 $generated@@492) $generated@@490) + :pattern ( ($generated@@197 ($generated@@46 $generated@@77 ($generated@@78 $generated@@42)) $generated@@42 ($generated@@46 $generated@@42 $generated@@15) ($generated@@489 $generated@@490) $generated@@491 $generated@@492)) +))) +(assert (forall (($generated@@494 T@U) ($generated@@495 T@U) ($generated@@496 T@U) ) (! (= ($generated@@197 ($generated@@46 $generated@@77 ($generated@@78 $generated@@42)) $generated@@42 $generated@@42 ($generated@@493 $generated@@494) $generated@@495 $generated@@496) $generated@@494) + :pattern ( ($generated@@197 ($generated@@46 $generated@@77 ($generated@@78 $generated@@42)) $generated@@42 $generated@@42 ($generated@@493 $generated@@494) $generated@@495 $generated@@496)) +))) +(assert (forall (($generated@@498 T@U) ($generated@@499 Bool) ($generated@@500 T@U) ($generated@@501 T@U) ) (! (= ($generated@@19 ($generated@@197 ($generated@@46 $generated@@77 ($generated@@78 $generated@@42)) $generated@@42 $generated@@15 ($generated@@497 $generated@@498 $generated@@499) $generated@@500 $generated@@501)) (and ($generated@@44 $generated@@42 $generated@@501 $generated@@498) $generated@@499)) + :pattern ( ($generated@@197 ($generated@@46 $generated@@77 ($generated@@78 $generated@@42)) $generated@@42 $generated@@15 ($generated@@497 $generated@@498 $generated@@499) $generated@@500 $generated@@501)) +))) +(push 1) +(declare-fun ControlFlow (Int Int) Int) +(declare-fun $generated@@502 () T@U) +(declare-fun $generated@@503 () T@U) +(declare-fun $generated@@504 () T@U) +(declare-fun $generated@@505 () T@U) +(declare-fun $generated@@506 () T@U) +(declare-fun $generated@@507 () T@U) +(declare-fun $generated@@508 () T@U) +(declare-fun $generated@@509 () T@U) +(declare-fun $generated@@510 () T@U) +(declare-fun $generated@@511 (T@U) Bool) +(declare-fun $generated@@512 () T@U) +(set-option :timeout 0) +(set-option :rlimit 0) +(assert (not + (=> (= (ControlFlow 0 0) 14) (let (($generated@@513 true)) +(let (($generated@@514 (=> (and (= ($generated@@32 $generated@@33 $generated@@116) $generated@@116) (= (ControlFlow 0 8) (- 0 7))) false))) +(let (($generated@@515 (=> ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 false))) (and (=> (= (ControlFlow 0 10) 8) $generated@@514) (=> (= (ControlFlow 0 10) 9) $generated@@513))))) +(let (($generated@@516 true)) +(let (($generated@@517 (=> (and (not ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 false)))) (= (ControlFlow 0 6) 4)) $generated@@516))) +(let (($generated@@518 (=> (and (and ($generated@@44 $generated@@42 $generated@@502 $generated@@503) ($generated@@172 $generated@@42 $generated@@502 $generated@@503 $generated@@504)) (= $generated@@505 ($generated@@365 $generated@@109 $generated@@504 $generated@@1 false))) (and (=> (= (ControlFlow 0 11) 10) $generated@@515) (=> (= (ControlFlow 0 11) 6) $generated@@517))))) +(let (($generated@@519 (=> (and (not (and ($generated@@44 $generated@@42 $generated@@502 $generated@@503) ($generated@@172 $generated@@42 $generated@@502 $generated@@503 $generated@@504))) (= (ControlFlow 0 5) 4)) $generated@@516))) +(let (($generated@@520 (=> (and ($generated@@34 $generated@@504) (or (= $generated@@506 $generated@@504) ($generated@@74 $generated@@506 $generated@@504))) (and (=> (= (ControlFlow 0 12) 11) $generated@@518) (=> (= (ControlFlow 0 12) 5) $generated@@519))))) +(let (($generated@@521 (=> (and (and ($generated@@35 $generated@@503 $generated@@507 ($generated@@32 $generated@@33 ($generated@@150 ($generated@@32 ($generated@@46 $generated@@42 $generated@@15) ($generated@@423 $generated@@42)) ($generated@@32 $generated@@47 ($generated@@162 $generated@@47 ($generated@@247 ($generated@@196 ($generated@@493 $generated@@508) ($generated@@497 $generated@@503 ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 false)))) ($generated@@489 ($generated@@159 ($generated@@244 false))))) ($generated@@408 $generated@@509)))))) (= (ControlFlow 0 3) (- 0 2))) ($generated@@35 $generated@@503 $generated@@507 ($generated@@32 $generated@@33 ($generated@@150 ($generated@@32 ($generated@@46 $generated@@42 $generated@@15) ($generated@@423 $generated@@42)) ($generated@@32 $generated@@47 ($generated@@162 $generated@@47 ($generated@@247 ($generated@@196 ($generated@@493 $generated@@508) ($generated@@497 $generated@@503 ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 false)))) ($generated@@489 ($generated@@159 ($generated@@244 false))))) ($generated@@408 $generated@@509))))))) ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 ($generated@@31 $generated@@503 $generated@@507 ($generated@@32 $generated@@33 ($generated@@150 ($generated@@32 ($generated@@46 $generated@@42 $generated@@15) ($generated@@423 $generated@@42)) ($generated@@32 $generated@@47 ($generated@@162 $generated@@47 ($generated@@247 ($generated@@196 ($generated@@493 $generated@@508) ($generated@@497 $generated@@503 ($generated@@19 ($generated@@32 $generated@@15 ($generated@@18 false)))) ($generated@@489 ($generated@@159 ($generated@@244 false))))) ($generated@@408 $generated@@509)))))))))))) +(let (($generated@@522 true)) +(let (($generated@@523 (=> (= $generated@@510 ($generated@@319 $generated@@109 $generated@@506 $generated@@1 false)) (and (and (=> (= (ControlFlow 0 13) 1) $generated@@522) (=> (= (ControlFlow 0 13) 12) $generated@@520)) (=> (= (ControlFlow 0 13) 3) $generated@@521))))) +(let (($generated@@524 (=> (and (and (and ($generated@@34 $generated@@506) ($generated@@511 $generated@@506)) ($generated@@36 $generated@@33 $generated@@512 ($generated@@37 $generated@@503 $generated@@507))) (and (= 1 $generated@@30) (= (ControlFlow 0 14) 13))) $generated@@523))) +$generated@@524))))))))))))) +)) +(check-sat) +(pop 1) +; Valid +(get-info :rlimit)