The lion is big. The lion is cold. The lion likes the mouse. The lion does not see the mouse. The lion visits the mouse. The mouse is young. The mouse does not like the rabbit. The mouse visits the lion. The rabbit likes the mouse. The rabbit sees the lion. The rabbit does not see the mouse. The rabbit visits the mouse. If something is rough and not cold then it likes the rabbit. If something likes the mouse then it likes the rabbit. If something likes the rabbit then it visits the lion. If something sees the rabbit and it is not cold then the rabbit is rough. If something is big then it is nice. If something likes the lion and it sees the rabbit then the rabbit visits the lion.
The lion is big.
("lion" "is" "big" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion does not see the mouse.
("lion" "sees" "mouse" "-")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse does not like the rabbit.
("mouse" "likes" "rabbit" "-")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit does not see the mouse.
("rabbit" "sees" "mouse" "-")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something is rough and not cold then it likes the rabbit.
((("something" "is" "rough" "+") ("something" "is" "cold" "~")) -> ("something" "likes" "rabbit" "+"))
If something likes the mouse then it likes the rabbit.
((("something" "likes" "mouse" "+")) -> ("something" "likes" "rabbit" "+"))
If something likes the rabbit then it visits the lion.
((("something" "likes" "rabbit" "+")) -> ("something" "visits" "lion" "+"))
If something sees the rabbit and it is not cold then the rabbit is rough.
((("something" "sees" "rabbit" "+") ("something" "is" "cold" "~")) -> ("rabbit" "is" "rough" "+"))
If something is big then it is nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something likes the lion and it sees the rabbit then the rabbit visits the lion.
((("something" "likes" "lion" "+") ("something" "sees" "rabbit" "+")) -> ("rabbit" "visits" "lion" "+"))
The lion visits the mouse.
True
1
proof
[(triple5)]
("lion" "visits" "mouse" "+")
triple5
The mouse likes the rabbit.
False
1
inv-proof
[(triple7)]
("mouse" "likes" "rabbit" "+")
triple7
The lion is nice.
True
2
proof
[(((triple1) -> rule5))]
("lion" "is" "nice" "+")
((triple1) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion does not like the rabbit.
False
2
inv-proof
[(((triple3) -> rule2))]
("lion" "likes" "rabbit" "-")
((triple3) -> (rule2 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The lion visits the lion.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("lion" "visits" "lion" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int2
The lion does not visit the lion.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("lion" "visits" "lion" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int2
The rabbit is not rough.
Unknown
inv-rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "rough" "-")
The mouse is nice.
Unknown
rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "nice" "+")
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "nice" "-")
The lion visits the rabbit.
Unknown
random
[@0: The lion visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "rabbit" "+")
The rabbit is not young.
Unknown
inv-random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "-")
The mouse sees the lion.
Unknown
random
[@0: The mouse sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "lion" "+")
@0: The lion does not see the mouse.[(triple4)] The lion is big.[(triple1)] The lion is cold.[(triple2)] The lion likes the mouse.[(triple3)] The lion visits the mouse.[(triple5)] The mouse does not like the rabbit.[(triple7)] The mouse is young.[(triple6)] The mouse visits the lion.[(triple8)] The rabbit does not see the mouse.[(triple11)] The rabbit likes the mouse.[(triple9)] The rabbit sees the lion.[(triple10)] The rabbit visits the mouse.[(triple12)] @1: The lion is nice.[(((triple1) -> rule5))] The lion likes the rabbit.[(((triple3) -> rule2))] The rabbit likes the rabbit.[(((triple9) -> rule2))] @2: The lion visits the lion.[(((((triple3) -> rule2)) -> rule3))] The rabbit visits the lion.[(((((triple9) -> rule2)) -> rule3))]
The lion does not see the mouse.
("lion" "sees" "mouse" "-")
triple4
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple3
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple5
The mouse does not like the rabbit.
("mouse" "likes" "rabbit" "-")
triple7
The mouse is young.
("mouse" "is" "young" "+")
triple6
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple8
The rabbit does not see the mouse.
("rabbit" "sees" "mouse" "-")
triple11
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple9
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple10
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple12
The lion is nice.
("lion" "is" "nice" "+")
((triple1) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
((triple3) -> (rule2 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((triple9) -> (rule2 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int2
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2