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