The cat eats the cow. The cow likes the tiger. The lion is blue. The tiger likes the cat. If someone likes the tiger then the tiger is red. If someone needs the lion and the lion likes the tiger then the tiger is not blue. If someone likes the cow then the cow is red. If the cow needs the lion and the lion likes the tiger then the cow does not need the tiger. If someone is young and they like the tiger then they do not eat the cow. If someone needs the cow and they are red then the cow eats the tiger. If the cat is big then the cat likes the lion. If someone needs the cow and they are not red then they eat the tiger.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The lion is blue.
("lion" "is" "blue" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If someone likes the tiger then the tiger is red.
((("someone" "likes" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If someone needs the lion and the lion likes the tiger then the tiger is not blue.
((("someone" "needs" "lion" "+") ("lion" "likes" "tiger" "+")) -> ("tiger" "is" "blue" "-"))
If someone likes the cow then the cow is red.
((("someone" "likes" "cow" "+")) -> ("cow" "is" "red" "+"))
If the cow needs the lion and the lion likes the tiger then the cow does not need the tiger.
((("cow" "needs" "lion" "+") ("lion" "likes" "tiger" "+")) -> ("cow" "needs" "tiger" "-"))
If someone is young and they like the tiger then they do not eat the cow.
((("someone" "is" "young" "+") ("someone" "likes" "tiger" "+")) -> ("someone" "eats" "cow" "-"))
If someone needs the cow and they are red then the cow eats the tiger.
((("someone" "needs" "cow" "+") ("someone" "is" "red" "+")) -> ("cow" "eats" "tiger" "+"))
If the cat is big then the cat likes the lion.
((("cat" "is" "big" "+")) -> ("cat" "likes" "lion" "+"))
If someone needs the cow and they are not red then they eat the tiger.
((("someone" "needs" "cow" "+") ("someone" "is" "red" "~")) -> ("someone" "eats" "tiger" "+"))
The cow likes the tiger.
True
1
proof
[(triple2)]
("cow" "likes" "tiger" "+")
triple2
The cow does not like the tiger.
False
1
inv-proof
[(triple2)]
("cow" "likes" "tiger" "-")
triple2
The tiger is red.
True
2
proof
[(((triple2) -> rule1))]
("tiger" "is" "red" "+")
((triple2) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is not red.
False
2
inv-proof
[(((triple2) -> rule1))]
("tiger" "is" "red" "-")
((triple2) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The cat does not like the lion.
Unknown
inv-rconc
[@1: The cat likes the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "likes" "lion" "-")
The cow is red.
Unknown
rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "red" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
@0: The cat eats the cow.[(triple1)] The cow likes the tiger.[(triple2)] The lion is blue.[(triple3)] The tiger likes the cat.[(triple4)] @1: The tiger is red.[(((triple2) -> rule1))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple2
The lion is blue.
("lion" "is" "blue" "+")
triple3
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple4
The tiger is red.
("tiger" "is" "red" "+")
((triple2) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1