The cat needs the tiger. The rabbit is red. The tiger is green. If the cat chases the rabbit then the rabbit does not chase the cat. If someone chases the tiger and they need the tiger then the tiger needs the cat. If the tiger is blue then the tiger needs the cat. If someone needs the rabbit then the rabbit is young. If someone is green and they eat the tiger then the tiger does not need the rabbit. If someone needs the tiger then the tiger chases the cat.
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The tiger is green.
("tiger" "is" "green" "+")
If the cat chases the rabbit then the rabbit does not chase the cat.
((("cat" "chases" "rabbit" "+")) -> ("rabbit" "chases" "cat" "-"))
If someone chases the tiger and they need the tiger then the tiger needs the cat.
((("someone" "chases" "tiger" "+") ("someone" "needs" "tiger" "+")) -> ("tiger" "needs" "cat" "+"))
If the tiger is blue then the tiger needs the cat.
((("tiger" "is" "blue" "+")) -> ("tiger" "needs" "cat" "+"))
If someone needs the rabbit then the rabbit is young.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If someone is green and they eat the tiger then the tiger does not need the rabbit.
((("someone" "is" "green" "+") ("someone" "eats" "tiger" "+")) -> ("tiger" "needs" "rabbit" "-"))
If someone needs the tiger then the tiger chases the cat.
((("someone" "needs" "tiger" "+")) -> ("tiger" "chases" "cat" "+"))
The rabbit is red.
True
1
proof
[(triple2)]
("rabbit" "is" "red" "+")
triple2
The cat does not need the tiger.
False
1
inv-proof
[(triple1)]
("cat" "needs" "tiger" "-")
triple1
The tiger chases the cat.
True
2
proof
[(((triple1) -> rule6))]
("tiger" "chases" "cat" "+")
((triple1) -> (rule6 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger does not chase the cat.
False
2
inv-proof
[(((triple1) -> rule6))]
("tiger" "chases" "cat" "-")
((triple1) -> (rule6 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The rabbit is not young.
Unknown
inv-rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "young" "-")
The tiger needs the cat.
Unknown
rconc
[@1: The tiger needs the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "needs" "cat" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat needs the tiger.[(triple1)] The rabbit is red.[(triple2)] The tiger is green.[(triple3)] @1: The tiger chases the cat.[(((triple1) -> rule6))]
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple1
The rabbit is red.
("rabbit" "is" "red" "+")
triple2
The tiger is green.
("tiger" "is" "green" "+")
triple3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
((triple1) -> (rule6 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1