The lion eats the rabbit. The lion is cold. The lion is kind. The lion is not nice. The lion sees the rabbit. The lion visits the rabbit. The rabbit eats the lion. The rabbit is not blue. The rabbit sees the lion. The rabbit visits the lion. If something is nice then it visits the rabbit. If the rabbit is not big then the rabbit does not eat the lion. If the lion is not nice then the lion is blue.
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is not nice.
("lion" "is" "nice" "-")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit is not blue.
("rabbit" "is" "blue" "-")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If something is nice then it visits the rabbit.
((("something" "is" "nice" "+")) -> ("something" "visits" "rabbit" "+"))
If the rabbit is not big then the rabbit does not eat the lion.
((("rabbit" "is" "big" "~")) -> ("rabbit" "eats" "lion" "-"))
If the lion is not nice then the lion is blue.
((("lion" "is" "nice" "~")) -> ("lion" "is" "blue" "+"))
The lion visits the rabbit.
True
1
proof
[(triple6)]
("lion" "visits" "rabbit" "+")
triple6
The lion does not see the rabbit.
False
1
inv-proof
[(triple5)]
("lion" "sees" "rabbit" "-")
triple5
The lion is blue.
True
2
proof
[(((triple4) -> rule3))]
("lion" "is" "blue" "+")
((triple4) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is not blue.
False
2
inv-proof
[(((triple4) -> rule3))]
("lion" "is" "blue" "-")
((triple4) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The rabbit does not visit the rabbit.
Unknown
inv-rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "rabbit" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The lion eats the rabbit.[(triple1)] The lion is cold.[(triple2)] The lion is kind.[(triple3)] The lion is not nice.[(triple4)] The lion sees the rabbit.[(triple5)] The lion visits the rabbit.[(triple6)] The rabbit eats the lion.[(triple7)] The rabbit is not blue.[(triple8)] The rabbit sees the lion.[(triple9)] The rabbit visits the lion.[(triple10)] @1: The lion is blue.[(((triple4) -> rule3))]
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The lion is not nice.
("lion" "is" "nice" "-")
triple4
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple5
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple6
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple7
The rabbit is not blue.
("rabbit" "is" "blue" "-")
triple8
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple9
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple10
The lion is blue.
("lion" "is" "blue" "+")
((triple4) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1