The bear likes the rabbit. The bear needs the rabbit. The bear visits the dog. The bear visits the mouse. The dog is nice. The dog is rough. The dog is young. The dog visits the bear. The dog visits the rabbit. The mouse is cold. The mouse needs the rabbit. The mouse visits the rabbit. The rabbit is cold. The rabbit likes the dog. The rabbit needs the mouse. If something needs the mouse and it visits the bear then the bear needs the mouse. If something visits the rabbit then the rabbit needs the mouse. If something visits the dog then it needs the dog. If the mouse likes the rabbit and the rabbit visits the mouse then the mouse likes the bear. If something needs the mouse and it is kind then the mouse is kind. If something visits the bear then it visits the dog. If something is nice and it visits the bear then the bear visits the dog. If something visits the rabbit then it visits the bear.
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is young.
("dog" "is" "young" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If something needs the mouse and it visits the bear then the bear needs the mouse.
((("something" "needs" "mouse" "+") ("something" "visits" "bear" "+")) -> ("bear" "needs" "mouse" "+"))
If something visits the rabbit then the rabbit needs the mouse.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "needs" "mouse" "+"))
If something visits the dog then it needs the dog.
((("something" "visits" "dog" "+")) -> ("something" "needs" "dog" "+"))
If the mouse likes the rabbit and the rabbit visits the mouse then the mouse likes the bear.
((("mouse" "likes" "rabbit" "+") ("rabbit" "visits" "mouse" "+")) -> ("mouse" "likes" "bear" "+"))
If something needs the mouse and it is kind then the mouse is kind.
((("something" "needs" "mouse" "+") ("something" "is" "kind" "+")) -> ("mouse" "is" "kind" "+"))
If something visits the bear then it visits the dog.
((("something" "visits" "bear" "+")) -> ("something" "visits" "dog" "+"))
If something is nice and it visits the bear then the bear visits the dog.
((("something" "is" "nice" "+") ("something" "visits" "bear" "+")) -> ("bear" "visits" "dog" "+"))
If something visits the rabbit then it visits the bear.
((("something" "visits" "rabbit" "+")) -> ("something" "visits" "bear" "+"))
The bear visits the mouse.
True
1
proof
[(triple4)]
("bear" "visits" "mouse" "+")
triple4
The dog does not visit the bear.
False
1
inv-proof
[(triple8 OR ((triple9) -> rule8))]
("dog" "visits" "bear" "-")
triple8
((triple9) -> (rule8 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog visits the dog.
True
2
proof
[(((triple8) -> rule6) OR ((((triple9) -> rule8)) -> rule6))]
("dog" "visits" "dog" "+")
((triple8) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
((((triple9) -> (rule8 % int2))) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the bear.
("dog" "visits" "bear" "+")
int2
The dog does not visit the dog.
False
2
inv-proof
[(((triple8) -> rule6) OR ((((triple9) -> rule8)) -> rule6))]
("dog" "visits" "dog" "-")
((triple8) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
((((triple9) -> (rule8 % int2))) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the bear.
("dog" "visits" "bear" "+")
int2
The mouse does not like the bear.
Unknown
inv-rconc
[@1: The mouse likes the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "likes" "bear" "-")
The mouse is kind.
Unknown
rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "kind" "+")
The mouse does not like the rabbit.
Unknown
inv-random
[@0: The mouse likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "rabbit" "-")
The dog visits the mouse.
Unknown
random
[@0: The dog visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "mouse" "+")
@0: The bear likes the rabbit.[(triple1)] The bear needs the rabbit.[(triple2)] The bear visits the dog.[(triple3 OR ((triple5 triple8) -> rule7) OR ((triple5 ((triple9) -> rule8)) -> rule7))] The bear visits the mouse.[(triple4)] The dog is nice.[(triple5)] The dog is rough.[(triple6)] The dog is young.[(triple7)] The dog visits the bear.[(triple8 OR ((triple9) -> rule8))] The dog visits the rabbit.[(triple9)] The mouse is cold.[(triple10)] The mouse needs the rabbit.[(triple11)] The mouse visits the rabbit.[(triple12)] The rabbit is cold.[(triple13)] The rabbit likes the dog.[(triple14)] The rabbit needs the mouse.[(triple15 OR ((triple12) -> rule2) OR ((triple9) -> rule2))] @1: The bear needs the dog.[(((triple3) -> rule3) OR ((((triple5 triple8) -> rule7)) -> rule3) OR ((((triple5 ((triple9) -> rule8)) -> rule7)) -> rule3))] The dog visits the dog.[(((triple8) -> rule6) OR ((((triple9) -> rule8)) -> rule6))] The mouse visits the bear.[(((triple12) -> rule8))] @2: The dog needs the dog.[(((((triple8) -> rule6)) -> rule3) OR ((((((triple9) -> rule8)) -> rule6)) -> rule3))] The mouse visits the dog.[(((((triple12) -> rule8)) -> rule6))] @3: The mouse needs the dog.[(((((((triple12) -> rule8)) -> rule6)) -> rule3))]
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple2
The bear visits the dog.
("bear" "visits" "dog" "+")
triple3
((triple5 triple8) -> (rule7 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
((triple5 ((triple9) -> (rule8 % int2))) -> (rule7 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
The dog visits the bear.
("dog" "visits" "bear" "+")
int2
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple4
The dog is nice.
("dog" "is" "nice" "+")
triple5
The dog is rough.
("dog" "is" "rough" "+")
triple6
The dog is young.
("dog" "is" "young" "+")
triple7
The dog visits the bear.
("dog" "visits" "bear" "+")
triple8
((triple9) -> (rule8 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple9
The mouse is cold.
("mouse" "is" "cold" "+")
triple10
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple11
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple12
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple13
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple14
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple15
((triple12) -> (rule2 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
((triple9) -> (rule2 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
((triple3) -> (rule3 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
((((triple5 triple8) -> (rule7 % int2))) -> (rule3 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
((((triple5 ((triple9) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The dog visits the bear.
("dog" "visits" "bear" "+")
int3
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple8) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
((((triple9) -> (rule8 % int2))) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the bear.
("dog" "visits" "bear" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
((triple12) -> (rule8 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
((((triple8) -> (rule6 % int2))) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
((((((triple9) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog visits the bear.
("dog" "visits" "bear" "+")
int3
The mouse visits the dog.
("mouse" "visits" "dog" "+")
((((triple12) -> (rule8 % int2))) -> (rule6 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
((((((triple12) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int3