The cow is rough. The mouse likes the cow. If the mouse likes the cow then the mouse is kind. If the mouse is kind then the mouse does not eat the cow. If someone needs the cow and the cow is blue then the cow needs the mouse. If someone is round and they do not like the cow then they are rough. If someone needs the mouse and the mouse eats the cow then they are kind. If someone likes the cow then they need the cow. If someone is rough and they eat the mouse then they are nice. If someone is rough and they do not need the cow then they eat the mouse.
The cow is rough.
("cow" "is" "rough" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
If the mouse likes the cow then the mouse is kind.
((("mouse" "likes" "cow" "+")) -> ("mouse" "is" "kind" "+"))
If the mouse is kind then the mouse does not eat the cow.
((("mouse" "is" "kind" "+")) -> ("mouse" "eats" "cow" "-"))
If someone needs the cow and the cow is blue then the cow needs the mouse.
((("someone" "needs" "cow" "+") ("cow" "is" "blue" "+")) -> ("cow" "needs" "mouse" "+"))
If someone is round and they do not like the cow then they are rough.
((("someone" "is" "round" "+") ("someone" "likes" "cow" "~")) -> ("someone" "is" "rough" "+"))
If someone needs the mouse and the mouse eats the cow then they are kind.
((("someone" "needs" "mouse" "+") ("mouse" "eats" "cow" "+")) -> ("someone" "is" "kind" "+"))
If someone likes the cow then they need the cow.
((("someone" "likes" "cow" "+")) -> ("someone" "needs" "cow" "+"))
If someone is rough and they eat the mouse then they are nice.
((("someone" "is" "rough" "+") ("someone" "eats" "mouse" "+")) -> ("someone" "is" "nice" "+"))
If someone is rough and they do not need the cow then they eat the mouse.
((("someone" "is" "rough" "+") ("someone" "needs" "cow" "~")) -> ("someone" "eats" "mouse" "+"))
The mouse likes the cow.
True
1
proof
[(triple2)]
("mouse" "likes" "cow" "+")
triple2
The mouse does not like the cow.
False
1
inv-proof
[(triple2)]
("mouse" "likes" "cow" "-")
triple2
The mouse is kind.
True
2
proof
[(((triple2) -> rule1))]
("mouse" "is" "kind" "+")
((triple2) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is not kind.
False
2
inv-proof
[(((triple2) -> rule1))]
("mouse" "is" "kind" "-")
((triple2) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse does not eat the cow.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("mouse" "eats" "cow" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The mouse does not eat the cow.
("mouse" "eats" "cow" "-")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse eats the cow.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("mouse" "eats" "cow" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The mouse does not eat the cow.
("mouse" "eats" "cow" "-")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The cow does not need the mouse.
Unknown
inv-rconc
[@1: The cow needs the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "needs" "mouse" "-")
The cow is kind.
Unknown
rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "kind" "+")
The mouse is not nice.
Unknown
inv-rconc
[@2: The mouse is nice.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("mouse" "is" "nice" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The cow likes the mouse.
Unknown
random
[@0: The cow likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "mouse" "+")
@0: The cow is rough.[(triple1)] The mouse likes the cow.[(triple2)] @1: The mouse is kind.[(((triple2) -> rule1))] The mouse needs the cow.[(((triple2) -> rule6))] @2: The mouse does not eat the cow.[(((((triple2) -> rule1)) -> rule2))]
The cow is rough.
("cow" "is" "rough" "+")
triple1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
((triple2) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse needs the cow.
("mouse" "needs" "cow" "+")
((triple2) -> (rule6 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The mouse does not eat the cow.
("mouse" "eats" "cow" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The mouse does not eat the cow.
("mouse" "eats" "cow" "-")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2