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