The mouse is cold. The mouse is red. The mouse is rough. Rough things are cold. If something is red and nice then it is blue. If the mouse is blue and the mouse is cold then the mouse is red. Red things are blue. If something is rough and blue then it is cold. If the mouse is red then the mouse is cold. If something is nice and blue then it is cold. If the mouse is rough and the mouse is cold then the mouse is nice.
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
Rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is red and nice then it is blue.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If the mouse is blue and the mouse is cold then the mouse is red.
((("mouse" "is" "blue" "+") ("mouse" "is" "cold" "+")) -> ("mouse" "is" "red" "+"))
Red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If something is rough and blue then it is cold.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If the mouse is red then the mouse is cold.
((("mouse" "is" "red" "+")) -> ("mouse" "is" "cold" "+"))
If something is nice and blue then it is cold.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If the mouse is rough and the mouse is cold then the mouse is nice.
((("mouse" "is" "rough" "+") ("mouse" "is" "cold" "+")) -> ("mouse" "is" "nice" "+"))
The mouse is red.
True
1
proof
[(triple2)]
("mouse" "is" "red" "+")
triple2
The mouse is not cold.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule6) OR ((triple3) -> rule1) OR ((triple3 ((triple2) -> rule4)) -> rule5))]
("mouse" "is" "cold" "-")
triple1
((triple2) -> (rule6 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
((triple3) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
((triple3 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is blue.
True
2
proof
[(((triple2) -> rule4) OR ((triple2 ((triple3 triple1) -> rule8)) -> rule2) OR ((triple2 ((triple3 ((triple2) -> rule6)) -> rule8)) -> rule2) OR ((triple2 ((triple3 ((triple3) -> rule1)) -> rule8)) -> rule2))]
("mouse" "is" "blue" "+")
((triple2) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple2 ((triple3 triple1) -> (rule8 % int2))) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
((triple2 ((triple3 ((triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
((triple2 ((triple3 ((triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The mouse is not blue.
False
2
inv-proof
[(((triple2) -> rule4) OR ((triple2 ((triple3 triple1) -> rule8)) -> rule2) OR ((triple2 ((triple3 ((triple2) -> rule6)) -> rule8)) -> rule2) OR ((triple2 ((triple3 ((triple3) -> rule1)) -> rule8)) -> rule2))]
("mouse" "is" "blue" "-")
((triple2) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple2 ((triple3 triple1) -> (rule8 % int2))) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
((triple2 ((triple3 ((triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
((triple2 ((triple3 ((triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
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 eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The mouse is cold.[(triple1 OR ((triple2) -> rule6) OR ((triple3) -> rule1) OR ((triple3 ((triple2) -> rule4)) -> rule5))] The mouse is red.[(triple2)] The mouse is rough.[(triple3)] @1: The mouse is blue.[(((triple2) -> rule4) OR ((triple2 ((triple3 triple1) -> rule8)) -> rule2) OR ((triple2 ((triple3 ((triple2) -> rule6)) -> rule8)) -> rule2) OR ((triple2 ((triple3 ((triple3) -> rule1)) -> rule8)) -> rule2))] The mouse is nice.[(((triple3 triple1) -> rule8) OR ((triple3 ((triple2) -> rule6)) -> rule8) OR ((triple3 ((triple3) -> rule1)) -> rule8) OR ((triple3 ((triple3 ((triple2) -> rule4)) -> rule5)) -> rule8))]
The mouse is cold.
("mouse" "is" "cold" "+")
triple1
((triple2) -> (rule6 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
((triple3) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
((triple3 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
triple2
The mouse is rough.
("mouse" "is" "rough" "+")
triple3
The mouse is blue.
("mouse" "is" "blue" "+")
((triple2) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple2 ((triple3 triple1) -> (rule8 % int2))) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
((triple2 ((triple3 ((triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
((triple2 ((triple3 ((triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The mouse is nice.
("mouse" "is" "nice" "+")
((triple3 triple1) -> (rule8 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
((triple3 ((triple2) -> (rule6 % int2))) -> (rule8 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
((triple3 ((triple3) -> (rule1 % int2))) -> (rule8 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
((triple3 ((triple3 ((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3