The cow sees the rabbit. The dog chases the lion. The lion sees the rabbit. The rabbit needs the lion. If someone chases the lion then they need the cow. If someone is kind then they chase the dog. If someone chases the lion and they need the cow then they are cold. If someone needs the rabbit and they are cold then they chase the dog. If someone is blue then they chase the cow. If someone chases the lion then they see the dog.
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The dog chases the lion.
("dog" "chases" "lion" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
If someone chases the lion then they need the cow.
((("someone" "chases" "lion" "+")) -> ("someone" "needs" "cow" "+"))
If someone is kind then they chase the dog.
((("someone" "is" "kind" "+")) -> ("someone" "chases" "dog" "+"))
If someone chases the lion and they need the cow then they are cold.
((("someone" "chases" "lion" "+") ("someone" "needs" "cow" "+")) -> ("someone" "is" "cold" "+"))
If someone needs the rabbit and they are cold then they chase the dog.
((("someone" "needs" "rabbit" "+") ("someone" "is" "cold" "+")) -> ("someone" "chases" "dog" "+"))
If someone is blue then they chase the cow.
((("someone" "is" "blue" "+")) -> ("someone" "chases" "cow" "+"))
If someone chases the lion then they see the dog.
((("someone" "chases" "lion" "+")) -> ("someone" "sees" "dog" "+"))
The rabbit needs the lion.
True
1
proof
[(triple4)]
("rabbit" "needs" "lion" "+")
triple4
The cow does not see the rabbit.
False
1
inv-proof
[(triple1)]
("cow" "sees" "rabbit" "-")
triple1
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "dog" "-")
The cow chases the lion.
Unknown
random
[@0: The cow chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "lion" "+")
@0: The cow sees the rabbit.[(triple1)] The dog chases the lion.[(triple2)] The lion sees the rabbit.[(triple3)] The rabbit needs the lion.[(triple4)] @1: The dog needs the cow.[(((triple2) -> rule1))] The dog sees the dog.[(((triple2) -> rule6))] @2: The dog is cold.[(((triple2 ((triple2) -> rule1)) -> rule3))]
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple1
The dog chases the lion.
("dog" "chases" "lion" "+")
triple2
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple3
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple4
The dog needs the cow.
("dog" "needs" "cow" "+")
((triple2) -> (rule1 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
((triple2) -> (rule6 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2