The bald eagle needs the bear. The bald eagle visits the bear. The bear eats the bald eagle. The bear visits the mouse. The cow is young. The cow needs the bear. The mouse is young. If someone is young then they visit the cow. If someone visits the cow then they eat the bald eagle. If someone visits the mouse and the mouse is young then the mouse needs the cow.
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
The bald eagle visits the bear.
("bald eagle" "visits" "bear" "+")
The bear eats the bald eagle.
("bear" "eats" "bald eagle" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The mouse is young.
("mouse" "is" "young" "+")
If someone is young then they visit the cow.
((("someone" "is" "young" "+")) -> ("someone" "visits" "cow" "+"))
If someone visits the cow then they eat the bald eagle.
((("someone" "visits" "cow" "+")) -> ("someone" "eats" "bald eagle" "+"))
If someone visits the mouse and the mouse is young then the mouse needs the cow.
((("someone" "visits" "mouse" "+") ("mouse" "is" "young" "+")) -> ("mouse" "needs" "cow" "+"))
The mouse is young.
True
1
proof
[(triple7)]
("mouse" "is" "young" "+")
triple7
The bear does not visit the mouse.
False
1
inv-proof
[(triple4)]
("bear" "visits" "mouse" "-")
triple4
The cow visits the cow.
True
2
proof
[(((triple5) -> rule1))]
("cow" "visits" "cow" "+")
((triple5) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The mouse does not need the cow.
False
3
inv-proof
[(((triple4 triple7) -> rule3))]
("mouse" "needs" "cow" "-")
((triple4 triple7) -> (rule3 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The bald eagle does not visit the cow.
Unknown
inv-rconc
[@1: The bald eagle visits the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "visits" "cow" "-")
The bear visits the cow.
Unknown
rconc
[@1: The bear visits the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "cow" "+")
The bald eagle is not rough.
Unknown
inv-random
[@0: The bald eagle is rough.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "rough" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The bald eagle needs the bear.[(triple1)] The bald eagle visits the bear.[(triple2)] The bear eats the bald eagle.[(triple3)] The bear visits the mouse.[(triple4)] The cow is young.[(triple5)] The cow needs the bear.[(triple6)] The mouse is young.[(triple7)] @1: The cow visits the cow.[(((triple5) -> rule1))] The mouse needs the cow.[(((triple4 triple7) -> rule3))] The mouse visits the cow.[(((triple7) -> rule1))] @2: The cow eats the bald eagle.[(((((triple5) -> rule1)) -> rule2))] The mouse eats the bald eagle.[(((((triple7) -> rule1)) -> rule2))]
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
triple1
The bald eagle visits the bear.
("bald eagle" "visits" "bear" "+")
triple2
The bear eats the bald eagle.
("bear" "eats" "bald eagle" "+")
triple3
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5
The cow needs the bear.
("cow" "needs" "bear" "+")
triple6
The mouse is young.
("mouse" "is" "young" "+")
triple7
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple5) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The mouse needs the cow.
("mouse" "needs" "cow" "+")
((triple4 triple7) -> (rule3 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
((triple7) -> (rule1 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2