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