The cat chases the rabbit. The mouse is round. The rabbit visits the cat. If the rabbit does not like the cat then the cat chases the rabbit. If someone chases the mouse then the mouse visits the rabbit. If someone visits the cat then the cat chases the mouse.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The mouse is round.
("mouse" "is" "round" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If the rabbit does not like the cat then the cat chases the rabbit.
((("rabbit" "likes" "cat" "~")) -> ("cat" "chases" "rabbit" "+"))
If someone chases the mouse then the mouse visits the rabbit.
((("someone" "chases" "mouse" "+")) -> ("mouse" "visits" "rabbit" "+"))
If someone visits the cat then the cat chases the mouse.
((("someone" "visits" "cat" "+")) -> ("cat" "chases" "mouse" "+"))
The rabbit visits the cat.
True
1
proof
[(triple3)]
("rabbit" "visits" "cat" "+")
triple3
The rabbit does not visit the cat.
False
1
inv-proof
[(triple3)]
("rabbit" "visits" "cat" "-")
triple3
The cat chases the mouse.
True
2
proof
[(((triple3) -> rule3))]
("cat" "chases" "mouse" "+")
((triple3) -> (rule3 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat does not chase the mouse.
False
2
inv-proof
[(((triple3) -> rule3))]
("cat" "chases" "mouse" "-")
((triple3) -> (rule3 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The mouse visits the rabbit.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("mouse" "visits" "rabbit" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The mouse does not visit the rabbit.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("mouse" "visits" "rabbit" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The mouse does not like the cat.
Unknown
inv-random
[@0: The mouse likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "cat" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The cat does not like the mouse.
Unknown
inv-random
[@0: The cat likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "mouse" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The mouse does not chase the rabbit.
Unknown
inv-random
[@0: The mouse chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "rabbit" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The cat chases the rabbit.[(triple1)] The mouse is round.[(triple2)] The rabbit visits the cat.[(triple3)] @1: The cat chases the mouse.[(((triple3) -> rule3))] @2: The mouse visits the rabbit.[(((((triple3) -> rule3)) -> rule2))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The mouse is round.
("mouse" "is" "round" "+")
triple2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple3
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((triple3) -> (rule3 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2