The cow chases the dog. The cow chases the rabbit. The cow sees the tiger. The dog is blue. The dog is cold. The rabbit chases the dog. The rabbit chases the tiger. The rabbit is kind. The rabbit needs the tiger. The tiger is round. The tiger needs the rabbit. The tiger sees the dog. If something chases the rabbit and the rabbit chases the dog then it needs the rabbit.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If something chases the rabbit and the rabbit chases the dog then it needs the rabbit.
((("something" "chases" "rabbit" "+") ("rabbit" "chases" "dog" "+")) -> ("something" "needs" "rabbit" "+"))
The cow chases the dog.
True
1
proof
[(triple1)]
("cow" "chases" "dog" "+")
triple1
The cow does not see the tiger.
False
1
inv-proof
[(triple3)]
("cow" "sees" "tiger" "-")
triple3
The cow needs the rabbit.
True
3
proof
[(((triple2 triple6) -> rule1))]
("cow" "needs" "rabbit" "+")
((triple2 triple6) -> (rule1 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow does not need the rabbit.
False
3
inv-proof
[(((triple2 triple6) -> rule1))]
("cow" "needs" "rabbit" "-")
((triple2 triple6) -> (rule1 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The dog does not need the rabbit.
Unknown
inv-rconc
[@1: The dog needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "needs" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "rabbit" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The tiger chases the rabbit.
Unknown
random
[@0: The tiger chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "rabbit" "+")
@0: The cow chases the dog.[(triple1)] The cow chases the rabbit.[(triple2)] The cow sees the tiger.[(triple3)] The dog is blue.[(triple4)] The dog is cold.[(triple5)] The rabbit chases the dog.[(triple6)] The rabbit chases the tiger.[(triple7)] The rabbit is kind.[(triple8)] The rabbit needs the tiger.[(triple9)] The tiger is round.[(triple10)] The tiger needs the rabbit.[(triple11)] The tiger sees the dog.[(triple12)] @1: The cow needs the rabbit.[(((triple2 triple6) -> rule1))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple2
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple3
The dog is blue.
("dog" "is" "blue" "+")
triple4
The dog is cold.
("dog" "is" "cold" "+")
triple5
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple6
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple7
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple8
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple9
The tiger is round.
("tiger" "is" "round" "+")
triple10
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple11
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple12
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
((triple2 triple6) -> (rule1 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1