The cat is rough. The mouse likes the cat. If the mouse does not like the cat and the mouse does not see the cat then the mouse is kind. If the mouse is big and the mouse sees the cat then the mouse is kind. If someone likes the cat then the cat is green. If the cat is kind then the cat is rough. If someone likes the cat and they do not eat the mouse then they eat the cat. If someone is green then they see the mouse.
The cat is rough.
("cat" "is" "rough" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
If the mouse does not like the cat and the mouse does not see the cat then the mouse is kind.
((("mouse" "likes" "cat" "~") ("mouse" "sees" "cat" "~")) -> ("mouse" "is" "kind" "+"))
If the mouse is big and the mouse sees the cat then the mouse is kind.
((("mouse" "is" "big" "+") ("mouse" "sees" "cat" "+")) -> ("mouse" "is" "kind" "+"))
If someone likes the cat then the cat is green.
((("someone" "likes" "cat" "+")) -> ("cat" "is" "green" "+"))
If the cat is kind then the cat is rough.
((("cat" "is" "kind" "+")) -> ("cat" "is" "rough" "+"))
If someone likes the cat and they do not eat the mouse then they eat the cat.
((("someone" "likes" "cat" "+") ("someone" "eats" "mouse" "~")) -> ("someone" "eats" "cat" "+"))
If someone is green then they see the mouse.
((("someone" "is" "green" "+")) -> ("someone" "sees" "mouse" "+"))
The mouse likes the cat.
True
1
proof
[(triple2)]
("mouse" "likes" "cat" "+")
triple2
The cat is not rough.
False
1
inv-proof
[(triple1)]
("cat" "is" "rough" "-")
triple1
The cat is green.
True
2
proof
[(((triple2) -> rule3))]
("cat" "is" "green" "+")
((triple2) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is not green.
False
2
inv-proof
[(((triple2) -> rule3))]
("cat" "is" "green" "-")
((triple2) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat sees the mouse.
True
3
proof
[(((((triple2) -> rule3)) -> rule6))]
("cat" "sees" "mouse" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat does not see the mouse.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule6))]
("cat" "sees" "mouse" "-")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse is kind.
Unknown
rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "kind" "+")
The mouse does not eat the cat.
Unknown
inv-rconc
[@1: The mouse eats the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "eats" "cat" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
@0: The cat is rough.[(triple1)] The mouse likes the cat.[(triple2)] @1: The cat is green.[(((triple2) -> rule3))] @2: The cat sees the mouse.[(((((triple2) -> rule3)) -> rule6))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
((triple2) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2