The lion eats the mouse. The lion eats the rabbit. The lion sees the mouse. The lion sees the rabbit. The mouse is kind. The rabbit is kind. The rabbit sees the mouse. If something sees the lion and the lion eats the rabbit then it is round. If the mouse is young and the mouse is red then the mouse eats the lion. If something eats the mouse and it sees the mouse then the mouse sees the lion. If something is red and it eats the lion then it eats the mouse. If something eats the rabbit then the rabbit visits the lion. If something eats the rabbit and it visits the lion then the lion eats the rabbit. If something visits the lion and the lion visits the rabbit then the lion visits the mouse. If the rabbit eats the mouse and the rabbit visits the mouse then the rabbit sees the lion.
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If something sees the lion and the lion eats the rabbit then it is round.
((("something" "sees" "lion" "+") ("lion" "eats" "rabbit" "+")) -> ("something" "is" "round" "+"))
If the mouse is young and the mouse is red then the mouse eats the lion.
((("mouse" "is" "young" "+") ("mouse" "is" "red" "+")) -> ("mouse" "eats" "lion" "+"))
If something eats the mouse and it sees the mouse then the mouse sees the lion.
((("something" "eats" "mouse" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "sees" "lion" "+"))
If something is red and it eats the lion then it eats the mouse.
((("something" "is" "red" "+") ("something" "eats" "lion" "+")) -> ("something" "eats" "mouse" "+"))
If something eats the rabbit then the rabbit visits the lion.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "visits" "lion" "+"))
If something eats the rabbit and it visits the lion then the lion eats the rabbit.
((("something" "eats" "rabbit" "+") ("something" "visits" "lion" "+")) -> ("lion" "eats" "rabbit" "+"))
If something visits the lion and the lion visits the rabbit then the lion visits the mouse.
((("something" "visits" "lion" "+") ("lion" "visits" "rabbit" "+")) -> ("lion" "visits" "mouse" "+"))
If the rabbit eats the mouse and the rabbit visits the mouse then the rabbit sees the lion.
((("rabbit" "eats" "mouse" "+") ("rabbit" "visits" "mouse" "+")) -> ("rabbit" "sees" "lion" "+"))
The lion eats the mouse.
True
1
proof
[(triple1)]
("lion" "eats" "mouse" "+")
triple1
The lion does not eat the rabbit.
False
1
inv-proof
[(triple2)]
("lion" "eats" "rabbit" "-")
triple2
The mouse sees the lion.
True
3
proof
[(((triple1 triple3) -> rule3))]
("mouse" "sees" "lion" "+")
((triple1 triple3) -> (rule3 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The rabbit does not visit the lion.
False
2
inv-proof
[(((triple2) -> rule5))]
("rabbit" "visits" "lion" "-")
((triple2) -> (rule5 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The mouse is round.
True
5
proof
[(((((triple1 triple3) -> rule3) triple2) -> rule1))]
("mouse" "is" "round" "+")
((((triple1 triple3) -> (rule3 % int2)) triple2) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The mouse is not round.
False
5
inv-proof
[(((((triple1 triple3) -> rule3) triple2) -> rule1))]
("mouse" "is" "round" "-")
((((triple1 triple3) -> (rule3 % int2)) triple2) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse eats the lion.
Unknown
rconc
[@1: The mouse eats the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "eats" "lion" "+")
The rabbit does not eat the mouse.
Unknown
inv-rconc
[@1: The rabbit eats the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "eats" "mouse" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
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 mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
@0: The lion eats the mouse.[(triple1)] The lion eats the rabbit.[(triple2)] The lion sees the mouse.[(triple3)] The lion sees the rabbit.[(triple4)] The mouse is kind.[(triple5)] The rabbit is kind.[(triple6)] The rabbit sees the mouse.[(triple7)] @1: The mouse sees the lion.[(((triple1 triple3) -> rule3))] The rabbit visits the lion.[(((triple2) -> rule5))] @2: The mouse is round.[(((((triple1 triple3) -> rule3) triple2) -> rule1))]
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple3
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple4
The mouse is kind.
("mouse" "is" "kind" "+")
triple5
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple6
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple7
The mouse sees the lion.
("mouse" "sees" "lion" "+")
((triple1 triple3) -> (rule3 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
((triple2) -> (rule5 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((((triple1 triple3) -> (rule3 % int2)) triple2) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2