The lion is young. The lion sees the mouse. The lion visits the rabbit. The mouse is big. The mouse is red. The mouse is rough. The mouse is round. The mouse is young. The mouse needs the rabbit. The mouse visits the lion. The mouse visits the rabbit. The rabbit is big. The rabbit needs the lion. The rabbit needs the mouse. The rabbit sees the mouse. The rabbit does not visit the mouse. If someone is red and big then they visit the rabbit. If someone needs the rabbit then they are big. If someone visits the lion and the lion sees the mouse then the lion does not need the rabbit. If someone is round and they visit the rabbit then the rabbit does not visit the mouse. If the rabbit does not visit the mouse and the rabbit is not rough then the mouse sees the lion. If the mouse is not round then the mouse does not see the lion.
The lion is young.
("lion" "is" "young" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
If someone is red and big then they visit the rabbit.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone needs the rabbit then they are big.
((("someone" "needs" "rabbit" "+")) -> ("someone" "is" "big" "+"))
If someone visits the lion and the lion sees the mouse then the lion does not need the rabbit.
((("someone" "visits" "lion" "+") ("lion" "sees" "mouse" "+")) -> ("lion" "needs" "rabbit" "-"))
If someone is round and they visit the rabbit then the rabbit does not visit the mouse.
((("someone" "is" "round" "+") ("someone" "visits" "rabbit" "+")) -> ("rabbit" "visits" "mouse" "-"))
If the rabbit does not visit the mouse and the rabbit is not rough then the mouse sees the lion.
((("rabbit" "visits" "mouse" "~") ("rabbit" "is" "rough" "~")) -> ("mouse" "sees" "lion" "+"))
If the mouse is not round then the mouse does not see the lion.
((("mouse" "is" "round" "~")) -> ("mouse" "sees" "lion" "-"))
The lion is young.
True
1
proof
[(triple1)]
("lion" "is" "young" "+")
triple1
The mouse is not red.
False
1
inv-proof
[(triple5)]
("mouse" "is" "red" "-")
triple5
The rabbit does not visit the rabbit.
Unknown
inv-rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "rabbit" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The lion is young.[(triple1)] The lion sees the mouse.[(triple2)] The lion visits the rabbit.[(triple3)] The mouse is big.[(triple4 OR ((triple9) -> rule2))] The mouse is red.[(triple5)] The mouse is rough.[(triple6)] The mouse is round.[(triple7)] The mouse is young.[(triple8)] The mouse needs the rabbit.[(triple9)] The mouse visits the lion.[(triple10)] The mouse visits the rabbit.[(triple11 OR ((triple5 triple4) -> rule1) OR ((triple5 ((triple9) -> rule2)) -> rule1))] The rabbit does not visit the mouse.[(triple16 OR ((triple7 triple11) -> rule4) OR ((triple7 ((triple5 triple4) -> rule1)) -> rule4) OR ((triple7 ((triple5 ((triple9) -> rule2)) -> rule1)) -> rule4))] The rabbit is big.[(triple12)] The rabbit needs the lion.[(triple13)] The rabbit needs the mouse.[(triple14)] The rabbit sees the mouse.[(triple15)] @1: The lion does not need the rabbit.[(((triple10 triple2) -> rule3))]
The lion is young.
("lion" "is" "young" "+")
triple1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple2
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple3
The mouse is big.
("mouse" "is" "big" "+")
triple4
((triple9) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
triple5
The mouse is rough.
("mouse" "is" "rough" "+")
triple6
The mouse is round.
("mouse" "is" "round" "+")
triple7
The mouse is young.
("mouse" "is" "young" "+")
triple8
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple9
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple10
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple11
((triple5 triple4) -> (rule1 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
((triple5 ((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
triple16
((triple7 triple11) -> (rule4 % int1))
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
int1
((triple7 ((triple5 triple4) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
((triple7 ((triple5 ((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The rabbit is big.
("rabbit" "is" "big" "+")
triple12
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple13
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple14
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple15
The lion does not need the rabbit.
("lion" "needs" "rabbit" "-")
((triple10 triple2) -> (rule3 % int1))
The lion does not need the rabbit.
("lion" "needs" "rabbit" "-")
int1