The lion eats the rabbit. The lion is cold. The lion is nice. The lion sees the rabbit. The lion visits the rabbit. The rabbit eats the lion. The rabbit is big. The rabbit is cold. The rabbit is kind. The rabbit is nice. The rabbit sees the lion. The rabbit visits the lion. If someone sees the rabbit and the rabbit eats the lion then they visit the lion. If someone is blue then they see the lion. If someone visits the lion then they visit the rabbit.
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is 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 big.
("rabbit" "is" "big" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If someone sees the rabbit and the rabbit eats the lion then they visit the lion.
((("someone" "sees" "rabbit" "+") ("rabbit" "eats" "lion" "+")) -> ("someone" "visits" "lion" "+"))
If someone is blue then they see the lion.
((("someone" "is" "blue" "+")) -> ("someone" "sees" "lion" "+"))
If someone visits the lion then they visit the rabbit.
((("someone" "visits" "lion" "+")) -> ("someone" "visits" "rabbit" "+"))
The lion visits the rabbit.
True
1
proof
[(triple5 OR ((((triple4 triple6) -> rule1)) -> rule3))]
("lion" "visits" "rabbit" "+")
triple5
((((triple4 triple6) -> (rule1 % int2))) -> (rule3 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The rabbit does not eat the lion.
False
1
inv-proof
[(triple6)]
("rabbit" "eats" "lion" "-")
triple6
The lion does not see the lion.
Unknown
inv-rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "sees" "lion" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The lion eats the rabbit.[(triple1)] The lion is cold.[(triple2)] The lion is nice.[(triple3)] The lion sees the rabbit.[(triple4)] The lion visits the rabbit.[(triple5 OR ((((triple4 triple6) -> rule1)) -> rule3))] The rabbit eats the lion.[(triple6)] The rabbit is big.[(triple7)] The rabbit is cold.[(triple8)] The rabbit is kind.[(triple9)] The rabbit is nice.[(triple10)] The rabbit sees the lion.[(triple11)] The rabbit visits the lion.[(triple12)] @1: The lion visits the lion.[(((triple4 triple6) -> rule1))] The rabbit visits the rabbit.[(((triple12) -> rule3))]
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is nice.
("lion" "is" "nice" "+")
triple3
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple4
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple5
((((triple4 triple6) -> (rule1 % int2))) -> (rule3 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple6
The rabbit is big.
("rabbit" "is" "big" "+")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple8
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple9
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple10
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple11
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple12
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple4 triple6) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple12) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1