The bear chases the tiger. The cat likes the bear. The rabbit likes the cat. The tiger is blue. If something likes the cat then it is nice. If something chases the cat then it eats the cat. If something likes the bear then the bear is red. If something chases the cat and the cat likes the tiger then the cat chases the rabbit. If something chases the cat then it is blue. If something likes the tiger and it is kind then the tiger is nice.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If something likes the cat then it is nice.
((("something" "likes" "cat" "+")) -> ("something" "is" "nice" "+"))
If something chases the cat then it eats the cat.
((("something" "chases" "cat" "+")) -> ("something" "eats" "cat" "+"))
If something likes the bear then the bear is red.
((("something" "likes" "bear" "+")) -> ("bear" "is" "red" "+"))
If something chases the cat and the cat likes the tiger then the cat chases the rabbit.
((("something" "chases" "cat" "+") ("cat" "likes" "tiger" "+")) -> ("cat" "chases" "rabbit" "+"))
If something chases the cat then it is blue.
((("something" "chases" "cat" "+")) -> ("something" "is" "blue" "+"))
If something likes the tiger and it is kind then the tiger is nice.
((("something" "likes" "tiger" "+") ("something" "is" "kind" "+")) -> ("tiger" "is" "nice" "+"))
The tiger is blue.
True
1
proof
[(triple4)]
("tiger" "is" "blue" "+")
triple4
The bear does not chase the tiger.
False
1
inv-proof
[(triple1)]
("bear" "chases" "tiger" "-")
triple1
The rabbit is nice.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "is" "nice" "+")
((triple3) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is not nice.
False
2
inv-proof
[(((triple3) -> rule1))]
("rabbit" "is" "nice" "-")
((triple3) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The cat is not nice.
Unknown
inv-rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "nice" "-")
The cat chases the rabbit.
Unknown
rconc
[@1: The cat chases the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "chases" "rabbit" "+")
The rabbit does not eat the bear.
Unknown
inv-random
[@0: The rabbit eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "bear" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
@0: The bear chases the tiger.[(triple1)] The cat likes the bear.[(triple2)] The rabbit likes the cat.[(triple3)] The tiger is blue.[(triple4)] @1: The bear is red.[(((triple2) -> rule3))] The rabbit is nice.[(((triple3) -> rule1))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The cat likes the bear.
("cat" "likes" "bear" "+")
triple2
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple3
The tiger is blue.
("tiger" "is" "blue" "+")
triple4
The bear is red.
("bear" "is" "red" "+")
((triple2) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
((triple3) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1