The bear chases the tiger. The dog sees the tiger. The rabbit needs the tiger. The tiger chases the rabbit. If the rabbit needs the tiger then the rabbit needs the dog.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
If the rabbit needs the tiger then the rabbit needs the dog.
((("rabbit" "needs" "tiger" "+")) -> ("rabbit" "needs" "dog" "+"))
The rabbit needs the tiger.
True
1
proof
[(triple3)]
("rabbit" "needs" "tiger" "+")
triple3
The tiger does not chase the rabbit.
False
1
inv-proof
[(triple4)]
("tiger" "chases" "rabbit" "-")
triple4
The rabbit needs the dog.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "needs" "dog" "+")
((triple3) -> (rule1 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit does not need the dog.
False
2
inv-proof
[(((triple3) -> rule1))]
("rabbit" "needs" "dog" "-")
((triple3) -> (rule1 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
The bear does not see the rabbit.
Unknown
inv-random
[@0: The bear sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "rabbit" "-")
The bear needs the tiger.
Unknown
random
[@0: The bear needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "tiger" "+")
@0: The bear chases the tiger.[(triple1)] The dog sees the tiger.[(triple2)] The rabbit needs the tiger.[(triple3)] The tiger chases the rabbit.[(triple4)] @1: The rabbit needs the dog.[(((triple3) -> rule1))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple2
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple3
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple4
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
((triple3) -> (rule1 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1