The lion chases the mouse. The mouse sees the rabbit. The rabbit chases the lion. If something sees the rabbit then the rabbit is young. If something visits the lion and it is young then it sees the lion.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
If something sees the rabbit then the rabbit is young.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If something visits the lion and it is young then it sees the lion.
((("something" "visits" "lion" "+") ("something" "is" "young" "+")) -> ("something" "sees" "lion" "+"))
The mouse sees the rabbit.
True
1
proof
[(triple2)]
("mouse" "sees" "rabbit" "+")
triple2
The mouse does not see the rabbit.
False
1
inv-proof
[(triple2)]
("mouse" "sees" "rabbit" "-")
triple2
The rabbit is young.
True
2
proof
[(((triple2) -> rule1))]
("rabbit" "is" "young" "+")
((triple2) -> (rule1 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is not young.
False
2
inv-proof
[(((triple2) -> rule1))]
("rabbit" "is" "young" "-")
((triple2) -> (rule1 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The mouse does not see the lion.
Unknown
inv-rconc
[@1: The mouse sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "lion" "-")
The rabbit sees the lion.
Unknown
rconc
[@1: The rabbit sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "lion" "+")
The lion does not visit the rabbit.
Unknown
inv-random
[@0: The lion visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "rabbit" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
@0: The lion chases the mouse.[(triple1)] The mouse sees the rabbit.[(triple2)] The rabbit chases the lion.[(triple3)] @1: The rabbit is young.[(((triple2) -> rule1))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple2
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple3
The rabbit is young.
("rabbit" "is" "young" "+")
((triple2) -> (rule1 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1