The bald eagle chases the tiger. The bear eats the tiger. The tiger visits the bear. If the bald eagle visits the tiger and the bald eagle is blue then the tiger visits the bald eagle. If the tiger chases the bald eagle and the tiger is red then the tiger visits the bear. If something visits the tiger and it is green then it is red. If something chases the tiger then it eats the bald eagle. If something is round then it chases the bear. If something eats the tiger then the tiger eats the bald eagle.
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If the bald eagle visits the tiger and the bald eagle is blue then the tiger visits the bald eagle.
((("bald eagle" "visits" "tiger" "+") ("bald eagle" "is" "blue" "+")) -> ("tiger" "visits" "bald eagle" "+"))
If the tiger chases the bald eagle and the tiger is red then the tiger visits the bear.
((("tiger" "chases" "bald eagle" "+") ("tiger" "is" "red" "+")) -> ("tiger" "visits" "bear" "+"))
If something visits the tiger and it is green then it is red.
((("something" "visits" "tiger" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If something chases the tiger then it eats the bald eagle.
((("something" "chases" "tiger" "+")) -> ("something" "eats" "bald eagle" "+"))
If something is round then it chases the bear.
((("something" "is" "round" "+")) -> ("something" "chases" "bear" "+"))
If something eats the tiger then the tiger eats the bald eagle.
((("something" "eats" "tiger" "+")) -> ("tiger" "eats" "bald eagle" "+"))
The tiger visits the bear.
True
1
proof
[(triple3)]
("tiger" "visits" "bear" "+")
triple3
The bald eagle does not chase the tiger.
False
1
inv-proof
[(triple1)]
("bald eagle" "chases" "tiger" "-")
triple1
The tiger eats the bald eagle.
True
2
proof
[(((triple2) -> rule6))]
("tiger" "eats" "bald eagle" "+")
((triple2) -> (rule6 % int1))
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
int1
The bald eagle does not eat the bald eagle.
False
2
inv-proof
[(((triple1) -> rule4))]
("bald eagle" "eats" "bald eagle" "-")
((triple1) -> (rule4 % int1))
The bald eagle eats the bald eagle.
("bald eagle" "eats" "bald eagle" "+")
int1
The bear does not eat the bald eagle.
Unknown
inv-rconc
[@1: The bear eats the bald eagle.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "eats" "bald eagle" "-")
The bear is red.
Unknown
rconc
[@1: The bear is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "red" "+")
The bald eagle does not chase the bald eagle.
Unknown
inv-random
[@0: The bald eagle chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "bald eagle" "-")
The bald eagle visits the tiger.
Unknown
random
[@0: The bald eagle visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "tiger" "+")
@0: The bald eagle chases the tiger.[(triple1)] The bear eats the tiger.[(triple2)] The tiger visits the bear.[(triple3)] @1: The bald eagle eats the bald eagle.[(((triple1) -> rule4))] The tiger eats the bald eagle.[(((triple2) -> rule6))]
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
triple1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple2
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple3
The bald eagle eats the bald eagle.
("bald eagle" "eats" "bald eagle" "+")
((triple1) -> (rule4 % int1))
The bald eagle eats the bald eagle.
("bald eagle" "eats" "bald eagle" "+")
int1
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
((triple2) -> (rule6 % int1))
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
int1