The bear chases the rabbit. The bear visits the mouse. The cat chases the rabbit. The cat likes the bear. The mouse chases the cat. The mouse chases the rabbit. The rabbit chases the bear. If someone chases the cat then the cat likes the mouse. If someone is young then they are rough. If someone likes the mouse then they visit the bear.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
If someone chases the cat then the cat likes the mouse.
((("someone" "chases" "cat" "+")) -> ("cat" "likes" "mouse" "+"))
If someone is young then they are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone likes the mouse then they visit the bear.
((("someone" "likes" "mouse" "+")) -> ("someone" "visits" "bear" "+"))
The rabbit chases the bear.
True
1
proof
[(triple7)]
("rabbit" "chases" "bear" "+")
triple7
The cat does not chase the rabbit.
False
1
inv-proof
[(triple3)]
("cat" "chases" "rabbit" "-")
triple3
The cat likes the mouse.
True
2
proof
[(((triple5) -> rule1))]
("cat" "likes" "mouse" "+")
((triple5) -> (rule1 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat does not like the mouse.
False
2
inv-proof
[(((triple5) -> rule1))]
("cat" "likes" "mouse" "-")
((triple5) -> (rule1 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat visits the bear.
True
3
proof
[(((((triple5) -> rule1)) -> rule3))]
("cat" "visits" "bear" "+")
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The cat visits the bear.
("cat" "visits" "bear" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int2
The cat does not visit the bear.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule3))]
("cat" "visits" "bear" "-")
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The cat visits the bear.
("cat" "visits" "bear" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int2
The rabbit does not visit the bear.
Unknown
inv-rconc
[@1: The rabbit visits the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "visits" "bear" "-")
The cat is rough.
Unknown
rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "rough" "+")
The bear is not rough.
Unknown
inv-rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "rough" "-")
The bear likes the cat.
Unknown
random
[@0: The bear likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "cat" "+")
The cat does not visit the mouse.
Unknown
inv-random
[@0: The cat visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "mouse" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The bear chases the rabbit.[(triple1)] The bear visits the mouse.[(triple2)] The cat chases the rabbit.[(triple3)] The cat likes the bear.[(triple4)] The mouse chases the cat.[(triple5)] The mouse chases the rabbit.[(triple6)] The rabbit chases the bear.[(triple7)] @1: The cat likes the mouse.[(((triple5) -> rule1))] @2: The cat visits the bear.[(((((triple5) -> rule1)) -> rule3))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple3
The cat likes the bear.
("cat" "likes" "bear" "+")
triple4
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple5
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple6
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple7
The cat likes the mouse.
("cat" "likes" "mouse" "+")
((triple5) -> (rule1 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat visits the bear.
("cat" "visits" "bear" "+")
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The cat visits the bear.
("cat" "visits" "bear" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int2