The bear chases the tiger. The bear likes the rabbit. The rabbit likes the tiger. The tiger chases the rabbit. The tiger is young. The tiger needs the bear. The tiger needs the rabbit. If something likes the rabbit then the rabbit likes the bear. If the bear is young then the bear needs the tiger.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If something likes the rabbit then the rabbit likes the bear.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "likes" "bear" "+"))
If the bear is young then the bear needs the tiger.
((("bear" "is" "young" "+")) -> ("bear" "needs" "tiger" "+"))
The bear likes the rabbit.
True
1
proof
[(triple2)]
("bear" "likes" "rabbit" "+")
triple2
The bear does not chase the tiger.
False
1
inv-proof
[(triple1)]
("bear" "chases" "tiger" "-")
triple1
The rabbit likes the bear.
True
2
proof
[(((triple2) -> rule1))]
("rabbit" "likes" "bear" "+")
((triple2) -> (rule1 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The rabbit does not like the bear.
False
2
inv-proof
[(((triple2) -> rule1))]
("rabbit" "likes" "bear" "-")
((triple2) -> (rule1 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The bear does not need the tiger.
Unknown
inv-rconc
[@1: The bear needs the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "needs" "tiger" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The tiger does not chase the bear.
Unknown
inv-random
[@0: The tiger chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "bear" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
@0: The bear chases the tiger.[(triple1)] The bear likes the rabbit.[(triple2)] The rabbit likes the tiger.[(triple3)] The tiger chases the rabbit.[(triple4)] The tiger is young.[(triple5)] The tiger needs the bear.[(triple6)] The tiger needs the rabbit.[(triple7)] @1: The rabbit likes the bear.[(((triple2) -> rule1))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple2
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple3
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple4
The tiger is young.
("tiger" "is" "young" "+")
triple5
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple6
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple7
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
((triple2) -> (rule1 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1