The bald eagle visits the mouse. The mouse is big. The rabbit is nice. If something sees the rabbit and it visits the rabbit then the rabbit sees the mouse. If something visits the mouse then the mouse visits the rabbit. If something sees the bald eagle and it is not nice then it eats the rabbit. If something is nice then it visits the rabbit. If something visits the rabbit then the rabbit is young. If something is nice then it eats the bald eagle.
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
If something sees the rabbit and it visits the rabbit then the rabbit sees the mouse.
((("something" "sees" "rabbit" "+") ("something" "visits" "rabbit" "+")) -> ("rabbit" "sees" "mouse" "+"))
If something visits the mouse then the mouse visits the rabbit.
((("something" "visits" "mouse" "+")) -> ("mouse" "visits" "rabbit" "+"))
If something sees the bald eagle and it is not nice then it eats the rabbit.
((("something" "sees" "bald eagle" "+") ("something" "is" "nice" "~")) -> ("something" "eats" "rabbit" "+"))
If something is nice then it visits the rabbit.
((("something" "is" "nice" "+")) -> ("something" "visits" "rabbit" "+"))
If something visits the rabbit then the rabbit is young.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If something is nice then it eats the bald eagle.
((("something" "is" "nice" "+")) -> ("something" "eats" "bald eagle" "+"))
The mouse is big.
True
1
proof
[(triple2)]
("mouse" "is" "big" "+")
triple2
The rabbit is not nice.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "nice" "-")
triple3
The rabbit visits the rabbit.
True
2
proof
[(((triple3) -> rule4))]
("rabbit" "visits" "rabbit" "+")
((triple3) -> (rule4 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit does not eat the bald eagle.
False
2
inv-proof
[(((triple3) -> rule6))]
("rabbit" "eats" "bald eagle" "-")
((triple3) -> (rule6 % int1))
The rabbit eats the bald eagle.
("rabbit" "eats" "bald eagle" "+")
int1
The rabbit is young.
True
3
proof
[(((((triple1) -> rule2)) -> rule5) OR ((((triple3) -> rule4)) -> rule5))]
("rabbit" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit is not young.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule5) OR ((((triple3) -> rule4)) -> rule5))]
("rabbit" "is" "young" "-")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The mouse does not eat the rabbit.
Unknown
inv-rconc
[@1: The mouse eats the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "eats" "rabbit" "-")
The mouse eats the bald eagle.
Unknown
rconc
[@1: The mouse eats the bald eagle.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "eats" "bald eagle" "+")
The bald eagle does not eat the bald eagle.
Unknown
inv-rconc
[@1: The bald eagle eats the bald eagle.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "eats" "bald eagle" "-")
The mouse visits the bald eagle.
Unknown
random
[@0: The mouse visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bald eagle" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
@0: The bald eagle visits the mouse.[(triple1)] The mouse is big.[(triple2)] The rabbit is nice.[(triple3)] @1: The mouse visits the rabbit.[(((triple1) -> rule2))] The rabbit eats the bald eagle.[(((triple3) -> rule6))] The rabbit visits the rabbit.[(((triple3) -> rule4))] @2: The rabbit is young.[(((((triple1) -> rule2)) -> rule5) OR ((((triple3) -> rule4)) -> rule5))]
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
triple1
The mouse is big.
("mouse" "is" "big" "+")
triple2
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple3
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
((triple1) -> (rule2 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The rabbit eats the bald eagle.
("rabbit" "eats" "bald eagle" "+")
((triple3) -> (rule6 % int1))
The rabbit eats the bald eagle.
("rabbit" "eats" "bald eagle" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple3) -> (rule4 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2