The bear does not eat the mouse. The bear visits the rabbit. The mouse is kind. The mouse does not like the rabbit. The mouse visits the bear. The mouse visits the rabbit. The rabbit eats the bear. The rabbit eats the mouse. The rabbit likes the bear. The rabbit likes the mouse. The rabbit visits the bear. The rabbit visits the mouse. If something likes the mouse then the mouse is young. If something visits the rabbit and it is young then the rabbit visits the bear. If something eats the bear then it eats the rabbit. If something is nice then it eats the rabbit. If something is red then it is kind. If something is kind then it visits the bear.
The bear does not eat the mouse.
("bear" "eats" "mouse" "-")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse does not like the rabbit.
("mouse" "likes" "rabbit" "-")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something likes the mouse then the mouse is young.
((("something" "likes" "mouse" "+")) -> ("mouse" "is" "young" "+"))
If something visits the rabbit and it is young then the rabbit visits the bear.
((("something" "visits" "rabbit" "+") ("something" "is" "young" "+")) -> ("rabbit" "visits" "bear" "+"))
If something eats the bear then it eats the rabbit.
((("something" "eats" "bear" "+")) -> ("something" "eats" "rabbit" "+"))
If something is nice then it eats the rabbit.
((("something" "is" "nice" "+")) -> ("something" "eats" "rabbit" "+"))
If something is red then it is kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it visits the bear.
((("something" "is" "kind" "+")) -> ("something" "visits" "bear" "+"))
The bear visits the rabbit.
True
1
proof
[(triple2)]
("bear" "visits" "rabbit" "+")
triple2
The rabbit does not visit the bear.
False
1
inv-proof
[(triple11 OR ((triple6 ((triple10) -> rule1)) -> rule2))]
("rabbit" "visits" "bear" "-")
triple11
((triple6 ((triple10) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The bear does not eat the rabbit.
Unknown
inv-rconc
[@1: The bear eats the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "eats" "rabbit" "-")
The mouse likes the bear.
Unknown
random
[@0: The mouse likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "bear" "+")
@0: The bear does not eat the mouse.[(triple1)] The bear visits the rabbit.[(triple2)] The mouse does not like the rabbit.[(triple4)] The mouse is kind.[(triple3)] The mouse visits the bear.[(triple5 OR ((triple3) -> rule6))] The mouse visits the rabbit.[(triple6)] The rabbit eats the bear.[(triple7)] The rabbit eats the mouse.[(triple8)] The rabbit likes the bear.[(triple9)] The rabbit likes the mouse.[(triple10)] The rabbit visits the bear.[(triple11 OR ((triple6 ((triple10) -> rule1)) -> rule2))] The rabbit visits the mouse.[(triple12)] @1: The mouse is young.[(((triple10) -> rule1))] The rabbit eats the rabbit.[(((triple7) -> rule3))]
The bear does not eat the mouse.
("bear" "eats" "mouse" "-")
triple1
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple2
The mouse does not like the rabbit.
("mouse" "likes" "rabbit" "-")
triple4
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple5
((triple3) -> (rule6 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple6
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple7
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple8
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple9
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple10
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple11
((triple6 ((triple10) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple12
The mouse is young.
("mouse" "is" "young" "+")
((triple10) -> (rule1 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple7) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1