The mouse is blue. The mouse is cold. The mouse is green. The mouse is nice. The mouse is round. If something is blue and nice then it is cold. All round things are green. If the mouse is nice and the mouse is cold then the mouse is green. If the mouse is round then the mouse is green. Cold, green things are blue. Nice, cold things are round.
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is round.
("mouse" "is" "round" "+")
If something is blue and nice then it is cold.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
All round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If the mouse is nice and the mouse is cold then the mouse is green.
((("mouse" "is" "nice" "+") ("mouse" "is" "cold" "+")) -> ("mouse" "is" "green" "+"))
If the mouse is round then the mouse is green.
((("mouse" "is" "round" "+")) -> ("mouse" "is" "green" "+"))
Cold, green things are blue.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Nice, cold things are round.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
The mouse is blue.
True
1
proof
[(triple1 OR ((triple2 triple3) -> rule5) OR ((triple2 ((triple5) -> rule2)) -> rule5) OR ((triple2 ((triple5) -> rule4)) -> rule5) OR ((triple2 ((triple4 triple2) -> rule3)) -> rule5) OR ((triple2 ((((triple4 triple2) -> rule6)) -> rule2)) -> rule5) OR ((triple2 ((((triple4 triple2) -> rule6)) -> rule4)) -> rule5))]
("mouse" "is" "blue" "+")
triple1
((triple2 triple3) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple2 ((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
((triple2 ((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
((triple2 ((triple4 triple2) -> (rule3 % int2))) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
((triple2 ((((triple4 triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
((triple2 ((((triple4 triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
The mouse is not round.
False
1
inv-proof
[(triple5 OR ((triple4 triple2) -> rule6) OR ((triple4 ((triple1 triple4) -> rule1)) -> rule6))]
("mouse" "is" "round" "-")
triple5
((triple4 triple2) -> (rule6 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((triple4 ((triple1 triple4) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The mouse is blue.[(triple1 OR ((triple2 triple3) -> rule5) OR ((triple2 ((triple5) -> rule2)) -> rule5) OR ((triple2 ((triple5) -> rule4)) -> rule5) OR ((triple2 ((triple4 triple2) -> rule3)) -> rule5) OR ((triple2 ((((triple4 triple2) -> rule6)) -> rule2)) -> rule5) OR ((triple2 ((((triple4 triple2) -> rule6)) -> rule4)) -> rule5))] The mouse is cold.[(triple2 OR ((triple1 triple4) -> rule1))] The mouse is green.[(triple3 OR ((triple5) -> rule2) OR ((triple5) -> rule4) OR ((triple4 triple2) -> rule3) OR ((((triple4 triple2) -> rule6)) -> rule2) OR ((((triple4 triple2) -> rule6)) -> rule4) OR ((triple4 ((triple1 triple4) -> rule1)) -> rule3) OR ((((triple4 ((triple1 triple4) -> rule1)) -> rule6)) -> rule2) OR ((((triple4 ((triple1 triple4) -> rule1)) -> rule6)) -> rule4))] The mouse is nice.[(triple4)] The mouse is round.[(triple5 OR ((triple4 triple2) -> rule6) OR ((triple4 ((triple1 triple4) -> rule1)) -> rule6))]
The mouse is blue.
("mouse" "is" "blue" "+")
triple1
((triple2 triple3) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple2 ((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
((triple2 ((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
((triple2 ((triple4 triple2) -> (rule3 % int2))) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
((triple2 ((((triple4 triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
((triple2 ((((triple4 triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
((triple1 triple4) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
triple3
((triple5) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((triple5) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((triple4 triple2) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((((triple4 triple2) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
((((triple4 triple2) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
((triple4 ((triple1 triple4) -> (rule1 % int2))) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
((((triple4 ((triple1 triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
((((triple4 ((triple1 triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The mouse is nice.
("mouse" "is" "nice" "+")
triple4
The mouse is round.
("mouse" "is" "round" "+")
triple5
((triple4 triple2) -> (rule6 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((triple4 ((triple1 triple4) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2