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