The mouse is blue. The mouse is cold. The mouse is red. The mouse is rough. The mouse is young. If someone is cold and young then they are rough. Red people are rough. Red people are cold. Cold people are blue. If the mouse is not blue then the mouse is not rough. If the mouse is cold then the mouse is rough.
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is young.
("mouse" "is" "young" "+")
If someone is cold and young then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
Red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If the mouse is not blue then the mouse is not rough.
((("mouse" "is" "blue" "~")) -> ("mouse" "is" "rough" "-"))
If the mouse is cold then the mouse is rough.
((("mouse" "is" "cold" "+")) -> ("mouse" "is" "rough" "+"))
The mouse is red.
True
1
proof
[(triple3)]
("mouse" "is" "red" "+")
triple3
The mouse is not red.
False
1
inv-proof
[(triple3)]
("mouse" "is" "red" "-")
triple3
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The mouse is blue.[(triple1 OR ((triple2) -> rule4) OR ((((triple3) -> rule3)) -> rule4))] The mouse is cold.[(triple2 OR ((triple3) -> rule3))] The mouse is red.[(triple3)] The mouse is rough.[(triple4 OR ((triple2) -> rule6) OR ((triple3) -> rule2) OR ((triple2 triple5) -> rule1) OR ((((triple3) -> rule3)) -> rule6) OR ((((triple3) -> rule3) triple5) -> rule1))] The mouse is young.[(triple5)]
The mouse is blue.
("mouse" "is" "blue" "+")
triple1
((triple2) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
((triple3) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
((triple2) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
((triple3) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
((triple2 triple5) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
((((triple3) -> (rule3 % int2)) triple5) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
triple5