The bear visits the lion. The lion is rough. The mouse is red. If something is rough then it visits the mouse. If something visits the lion and it is rough then it likes the bear. If something visits the mouse then it likes the lion.
The bear visits the lion.
("bear" "visits" "lion" "+")
The lion is rough.
("lion" "is" "rough" "+")
The mouse is red.
("mouse" "is" "red" "+")
If something is rough then it visits the mouse.
((("something" "is" "rough" "+")) -> ("something" "visits" "mouse" "+"))
If something visits the lion and it is rough then it likes the bear.
((("something" "visits" "lion" "+") ("something" "is" "rough" "+")) -> ("something" "likes" "bear" "+"))
If something visits the mouse then it likes the lion.
((("something" "visits" "mouse" "+")) -> ("something" "likes" "lion" "+"))
The mouse is red.
True
1
proof
[(triple3)]
("mouse" "is" "red" "+")
triple3
The bear does not visit the lion.
False
1
inv-proof
[(triple1)]
("bear" "visits" "lion" "-")
triple1
The lion visits the mouse.
True
2
proof
[(((triple2) -> rule1))]
("lion" "visits" "mouse" "+")
((triple2) -> (rule1 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion does not visit the mouse.
False
2
inv-proof
[(((triple2) -> rule1))]
("lion" "visits" "mouse" "-")
((triple2) -> (rule1 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion likes the lion.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("lion" "likes" "lion" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int2
The lion does not like the lion.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("lion" "likes" "lion" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int2
The bear does not like the bear.
Unknown
inv-rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "likes" "bear" "-")
The mouse likes the bear.
Unknown
rconc
[@1: The mouse likes the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "likes" "bear" "+")
The bear does not visit the mouse.
Unknown
inv-rconc
[@1: The bear visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "mouse" "-")
The lion visits the bear.
Unknown
random
[@0: The lion visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "bear" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
@0: The bear visits the lion.[(triple1)] The lion is rough.[(triple2)] The mouse is red.[(triple3)] @1: The lion visits the mouse.[(((triple2) -> rule1))] @2: The lion likes the lion.[(((((triple2) -> rule1)) -> rule3))]
The bear visits the lion.
("bear" "visits" "lion" "+")
triple1
The lion is rough.
("lion" "is" "rough" "+")
triple2
The mouse is red.
("mouse" "is" "red" "+")
triple3
The lion visits the mouse.
("lion" "visits" "mouse" "+")
((triple2) -> (rule1 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int2