The cow does not visit the rabbit. The lion chases the rabbit. The mouse visits the rabbit. The rabbit visits the lion. If the rabbit is kind then the rabbit visits the mouse. If the rabbit chases the mouse and the mouse chases the rabbit then the rabbit does not visit the mouse. If someone visits the mouse and they chase the lion then the lion does not see the rabbit. If someone sees the lion and they do not chase the lion then the lion chases the cow. If someone is kind then they see the mouse. If someone is young then they visit the cow. If the mouse visits the rabbit and the mouse does not see the lion then the mouse is nice. If someone visits the lion then they are young.
The cow does not visit the rabbit.
("cow" "visits" "rabbit" "-")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If the rabbit is kind then the rabbit visits the mouse.
((("rabbit" "is" "kind" "+")) -> ("rabbit" "visits" "mouse" "+"))
If the rabbit chases the mouse and the mouse chases the rabbit then the rabbit does not visit the mouse.
((("rabbit" "chases" "mouse" "+") ("mouse" "chases" "rabbit" "+")) -> ("rabbit" "visits" "mouse" "-"))
If someone visits the mouse and they chase the lion then the lion does not see the rabbit.
((("someone" "visits" "mouse" "+") ("someone" "chases" "lion" "+")) -> ("lion" "sees" "rabbit" "-"))
If someone sees the lion and they do not chase the lion then the lion chases the cow.
((("someone" "sees" "lion" "+") ("someone" "chases" "lion" "~")) -> ("lion" "chases" "cow" "+"))
If someone is kind then they see the mouse.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "mouse" "+"))
If someone is young then they visit the cow.
((("someone" "is" "young" "+")) -> ("someone" "visits" "cow" "+"))
If the mouse visits the rabbit and the mouse does not see the lion then the mouse is nice.
((("mouse" "visits" "rabbit" "+") ("mouse" "sees" "lion" "~")) -> ("mouse" "is" "nice" "+"))
If someone visits the lion then they are young.
((("someone" "visits" "lion" "+")) -> ("someone" "is" "young" "+"))
The rabbit visits the lion.
True
1
proof
[(triple4)]
("rabbit" "visits" "lion" "+")
triple4
The lion does not chase the rabbit.
False
1
inv-proof
[(triple2)]
("lion" "chases" "rabbit" "-")
triple2
The rabbit is young.
True
2
proof
[(((triple4) -> rule8))]
("rabbit" "is" "young" "+")
((triple4) -> (rule8 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is not young.
False
2
inv-proof
[(((triple4) -> rule8))]
("rabbit" "is" "young" "-")
((triple4) -> (rule8 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit visits the cow.
True
3
proof
[(((((triple4) -> rule8)) -> rule6))]
("rabbit" "visits" "cow" "+")
((((triple4) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit does not visit the cow.
False
3
inv-proof
[(((((triple4) -> rule8)) -> rule6))]
("rabbit" "visits" "cow" "-")
((((triple4) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The lion does not see the mouse.
Unknown
inv-rconc
[@1: The lion sees the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "sees" "mouse" "-")
The mouse visits the cow.
Unknown
rconc
[@2: The mouse visits the cow.[CWA. Example of deepest failure = (rule6 <- rule8 <- FAIL)]]
("mouse" "visits" "cow" "+")
The rabbit does not visit the mouse.
Unknown
inv-rconc
[@1: The rabbit visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "mouse" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
@0: The cow does not visit the rabbit.[(triple1)] The lion chases the rabbit.[(triple2)] The mouse visits the rabbit.[(triple3)] The rabbit visits the lion.[(triple4)] @1: The rabbit is young.[(((triple4) -> rule8))] @2: The rabbit visits the cow.[(((((triple4) -> rule8)) -> rule6))]
The cow does not visit the rabbit.
("cow" "visits" "rabbit" "-")
triple1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple2
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple3
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple4
The rabbit is young.
("rabbit" "is" "young" "+")
((triple4) -> (rule8 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
((((triple4) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2