The mouse is round. The mouse sees the tiger. The mouse visits the tiger. The tiger is red. The tiger likes the mouse. The tiger sees the mouse. The tiger visits the mouse. If someone is kind and they visit the mouse then they like the mouse. If someone visits the tiger and they are round then the tiger visits the mouse. If someone visits the tiger then they like the mouse. If someone is big and they see the tiger then the tiger sees the mouse. If someone is red and they like the tiger then they are rough. If someone visits the tiger and they see the tiger then they are rough. If someone sees the tiger then they are kind. If someone likes the mouse and they see the tiger then the mouse is red.
The mouse is round.
("mouse" "is" "round" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone is kind and they visit the mouse then they like the mouse.
((("someone" "is" "kind" "+") ("someone" "visits" "mouse" "+")) -> ("someone" "likes" "mouse" "+"))
If someone visits the tiger and they are round then the tiger visits the mouse.
((("someone" "visits" "tiger" "+") ("someone" "is" "round" "+")) -> ("tiger" "visits" "mouse" "+"))
If someone visits the tiger then they like the mouse.
((("someone" "visits" "tiger" "+")) -> ("someone" "likes" "mouse" "+"))
If someone is big and they see the tiger then the tiger sees the mouse.
((("someone" "is" "big" "+") ("someone" "sees" "tiger" "+")) -> ("tiger" "sees" "mouse" "+"))
If someone is red and they like the tiger then they are rough.
((("someone" "is" "red" "+") ("someone" "likes" "tiger" "+")) -> ("someone" "is" "rough" "+"))
If someone visits the tiger and they see the tiger then they are rough.
((("someone" "visits" "tiger" "+") ("someone" "sees" "tiger" "+")) -> ("someone" "is" "rough" "+"))
If someone sees the tiger then they are kind.
((("someone" "sees" "tiger" "+")) -> ("someone" "is" "kind" "+"))
If someone likes the mouse and they see the tiger then the mouse is red.
((("someone" "likes" "mouse" "+") ("someone" "sees" "tiger" "+")) -> ("mouse" "is" "red" "+"))
The tiger is red.
True
1
proof
[(triple4)]
("tiger" "is" "red" "+")
triple4
The tiger does not visit the mouse.
False
1
inv-proof
[(triple7 OR ((triple3 triple1) -> rule2))]
("tiger" "visits" "mouse" "-")
triple7
((triple3 triple1) -> (rule2 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse likes the mouse.
True
2
proof
[(((triple3) -> rule3))]
("mouse" "likes" "mouse" "+")
((triple3) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is not kind.
False
2
inv-proof
[(((triple2) -> rule7))]
("mouse" "is" "kind" "-")
((triple2) -> (rule7 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "is" "kind" "-")
The tiger is rough.
Unknown
rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "rough" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The mouse is round.[(triple1)] The mouse sees the tiger.[(triple2)] The mouse visits the tiger.[(triple3)] The tiger is red.[(triple4)] The tiger likes the mouse.[(triple5)] The tiger sees the mouse.[(triple6)] The tiger visits the mouse.[(triple7 OR ((triple3 triple1) -> rule2))] @1: The mouse is kind.[(((triple2) -> rule7))] The mouse is rough.[(((triple3 triple2) -> rule6))] The mouse likes the mouse.[(((triple3) -> rule3))] @2: The mouse is red.[(((((triple3) -> rule3) triple2) -> rule8))]
The mouse is round.
("mouse" "is" "round" "+")
triple1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple3
The tiger is red.
("tiger" "is" "red" "+")
triple4
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple5
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple6
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple7
((triple3 triple1) -> (rule2 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
((triple2) -> (rule7 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((triple3 triple2) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple3) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
((((triple3) -> (rule3 % int2)) triple2) -> (rule8 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2