The bald eagle visits the rabbit. The mouse eats the rabbit. The rabbit chases the mouse. If something visits the rabbit then the rabbit is round. If the rabbit eats the mouse then the mouse is rough. If something chases the mouse then it eats the mouse.
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
If something visits the rabbit then the rabbit is round.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
If the rabbit eats the mouse then the mouse is rough.
((("rabbit" "eats" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If something chases the mouse then it eats the mouse.
((("something" "chases" "mouse" "+")) -> ("something" "eats" "mouse" "+"))
The rabbit chases the mouse.
True
1
proof
[(triple3)]
("rabbit" "chases" "mouse" "+")
triple3
The mouse does not eat the rabbit.
False
1
inv-proof
[(triple2)]
("mouse" "eats" "rabbit" "-")
triple2
The rabbit is round.
True
2
proof
[(((triple1) -> rule1))]
("rabbit" "is" "round" "+")
((triple1) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("rabbit" "is" "round" "-")
((triple1) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The mouse is rough.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("mouse" "is" "rough" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The mouse is not rough.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("mouse" "is" "rough" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The bald eagle eats the mouse.
Unknown
rconc
[@1: The bald eagle eats the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "eats" "mouse" "+")
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The rabbit chases the bald eagle.
Unknown
random
[@0: The rabbit chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "bald eagle" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
@0: The bald eagle visits the rabbit.[(triple1)] The mouse eats the rabbit.[(triple2)] The rabbit chases the mouse.[(triple3)] @1: The rabbit eats the mouse.[(((triple3) -> rule3))] The rabbit is round.[(((triple1) -> rule1))] @2: The mouse is rough.[(((((triple3) -> rule3)) -> rule2))]
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
triple1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple3
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
((triple3) -> (rule3 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple1) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2