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