The dog likes the mouse. The lion likes the dog. The mouse sees the lion. The rabbit visits the dog. If something likes the lion and the lion is round then it is rough. If something is rough then it sees the dog. If something visits the lion then it sees the lion. If something likes the lion then it is round. If something likes the rabbit then the rabbit likes the mouse. If something likes the mouse then it likes the rabbit.
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If something likes the lion and the lion is round then it is rough.
((("something" "likes" "lion" "+") ("lion" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something is rough then it sees the dog.
((("something" "is" "rough" "+")) -> ("something" "sees" "dog" "+"))
If something visits the lion then it sees the lion.
((("something" "visits" "lion" "+")) -> ("something" "sees" "lion" "+"))
If something likes the lion then it is round.
((("something" "likes" "lion" "+")) -> ("something" "is" "round" "+"))
If something likes the rabbit then the rabbit likes the mouse.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "likes" "mouse" "+"))
If something likes the mouse then it likes the rabbit.
((("something" "likes" "mouse" "+")) -> ("something" "likes" "rabbit" "+"))
The mouse sees the lion.
True
1
proof
[(triple3)]
("mouse" "sees" "lion" "+")
triple3
The mouse does not see the lion.
False
1
inv-proof
[(triple3)]
("mouse" "sees" "lion" "-")
triple3
The dog likes the rabbit.
True
2
proof
[(((triple1) -> rule6))]
("dog" "likes" "rabbit" "+")
((triple1) -> (rule6 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The dog does not like the rabbit.
False
2
inv-proof
[(((triple1) -> rule6))]
("dog" "likes" "rabbit" "-")
((triple1) -> (rule6 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The rabbit likes the mouse.
True
3
proof
[(((((triple1) -> rule6)) -> rule5))]
("rabbit" "likes" "mouse" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The rabbit does not like the mouse.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule5))]
("rabbit" "likes" "mouse" "-")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The lion is not rough.
Unknown
inv-rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "rough" "-")
The rabbit is rough.
Unknown
rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "rough" "+")
The mouse does not see the dog.
Unknown
inv-rconc
[@2: The mouse sees the dog.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("mouse" "sees" "dog" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The rabbit is not green.
Unknown
inv-random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "-")
The lion visits the rabbit.
Unknown
random
[@0: The lion visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "rabbit" "+")
@0: The dog likes the mouse.[(triple1)] The lion likes the dog.[(triple2)] The mouse sees the lion.[(triple3)] The rabbit visits the dog.[(triple4)] @1: The dog likes the rabbit.[(((triple1) -> rule6))] @2: The rabbit likes the mouse.[(((((triple1) -> rule6)) -> rule5))] @3: The rabbit likes the rabbit.[(((((((triple1) -> rule6)) -> rule5)) -> rule6))]
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple1
The lion likes the dog.
("lion" "likes" "dog" "+")
triple2
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple3
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple4
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
((triple1) -> (rule6 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int3