The cat is rough. The dog visits the rabbit. The rabbit is blue. The rabbit needs the cat. The tiger needs the cat. The tiger needs the rabbit. The tiger sees the cat. If someone needs the cat and the cat needs the tiger then the tiger visits the rabbit. If someone sees the rabbit then they see the tiger. If someone sees the cat then the cat sees the rabbit.
The cat is rough.
("cat" "is" "rough" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If someone needs the cat and the cat needs the tiger then the tiger visits the rabbit.
((("someone" "needs" "cat" "+") ("cat" "needs" "tiger" "+")) -> ("tiger" "visits" "rabbit" "+"))
If someone sees the rabbit then they see the tiger.
((("someone" "sees" "rabbit" "+")) -> ("someone" "sees" "tiger" "+"))
If someone sees the cat then the cat sees the rabbit.
((("someone" "sees" "cat" "+")) -> ("cat" "sees" "rabbit" "+"))
The tiger needs the rabbit.
True
1
proof
[(triple6)]
("tiger" "needs" "rabbit" "+")
triple6
The tiger does not need the rabbit.
False
1
inv-proof
[(triple6)]
("tiger" "needs" "rabbit" "-")
triple6
The cat sees the rabbit.
True
2
proof
[(((triple7) -> rule3))]
("cat" "sees" "rabbit" "+")
((triple7) -> (rule3 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat does not see the rabbit.
False
2
inv-proof
[(((triple7) -> rule3))]
("cat" "sees" "rabbit" "-")
((triple7) -> (rule3 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat sees the tiger.
True
3
proof
[(((((triple7) -> rule3)) -> rule2))]
("cat" "sees" "tiger" "+")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat does not see the tiger.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule2))]
("cat" "sees" "tiger" "-")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger visits the rabbit.
Unknown
rconc
[@1: The tiger visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "rabbit" "+")
The dog does not see the tiger.
Unknown
inv-rconc
[@1: The dog sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "tiger" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
@0: The cat is rough.[(triple1)] The dog visits the rabbit.[(triple2)] The rabbit is blue.[(triple3)] The rabbit needs the cat.[(triple4)] The tiger needs the cat.[(triple5)] The tiger needs the rabbit.[(triple6)] The tiger sees the cat.[(triple7)] @1: The cat sees the rabbit.[(((triple7) -> rule3))] @2: The cat sees the tiger.[(((((triple7) -> rule3)) -> rule2))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple2
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple3
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple4
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple5
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple6
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple7
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
((triple7) -> (rule3 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2