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