ifThenElse1ToSolution

then ... or ... (if-then-else) request goals over ifThenTheory1 and their expected Solutions, checking that the "then" branch is taken whenever the condition has a solution, and the "else" branch otherwise — again committing to the condition's first solution only.