The lion is big. The lion is kind. The rabbit likes the lion. The squirrel is cold. The squirrel is nice. The squirrel is red. The squirrel likes the rabbit. The squirrel needs the lion. The tiger eats the lion. The tiger needs the lion. If something needs the tiger then the tiger eats the rabbit. If something eats the tiger and it is cold then it is nice. If the tiger is red and the tiger is cold then the tiger likes the lion. If something likes the lion and the lion is red then the lion likes the rabbit. If something is nice then it likes the tiger. If something eats the lion then it is nice. If the rabbit needs the squirrel and the squirrel is red then the squirrel is kind. If something is nice then it likes the rabbit.
The lion is big.
("lion" "is" "big" "+")
The lion is kind.
("lion" "is" "kind" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If something needs the tiger then the tiger eats the rabbit.
((("something" "needs" "tiger" "+")) -> ("tiger" "eats" "rabbit" "+"))
If something eats the tiger and it is cold then it is nice.
((("something" "eats" "tiger" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If the tiger is red and the tiger is cold then the tiger likes the lion.
((("tiger" "is" "red" "+") ("tiger" "is" "cold" "+")) -> ("tiger" "likes" "lion" "+"))
If something likes the lion and the lion is red then the lion likes the rabbit.
((("something" "likes" "lion" "+") ("lion" "is" "red" "+")) -> ("lion" "likes" "rabbit" "+"))
If something is nice then it likes the tiger.
((("something" "is" "nice" "+")) -> ("something" "likes" "tiger" "+"))
If something eats the lion then it is nice.
((("something" "eats" "lion" "+")) -> ("something" "is" "nice" "+"))
If the rabbit needs the squirrel and the squirrel is red then the squirrel is kind.
((("rabbit" "needs" "squirrel" "+") ("squirrel" "is" "red" "+")) -> ("squirrel" "is" "kind" "+"))
If something is nice then it likes the rabbit.
((("something" "is" "nice" "+")) -> ("something" "likes" "rabbit" "+"))
The lion is kind.
True
1
proof
[(triple2)]
("lion" "is" "kind" "+")
triple2
The lion is not big.
False
1
inv-proof
[(triple1)]
("lion" "is" "big" "-")
triple1
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "nice" "-")
The squirrel eats the lion.
Unknown
random
[@0: The squirrel eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "lion" "+")
@0: The lion is big.[(triple1)] The lion is kind.[(triple2)] The rabbit likes the lion.[(triple3)] The squirrel is cold.[(triple4)] The squirrel is nice.[(triple5)] The squirrel is red.[(triple6)] The squirrel likes the rabbit.[(triple7 OR ((triple5) -> rule8))] The squirrel needs the lion.[(triple8)] The tiger eats the lion.[(triple9)] The tiger needs the lion.[(triple10)] @1: The squirrel likes the tiger.[(((triple5) -> rule5))] The tiger is nice.[(((triple9) -> rule6))] @2: The tiger likes the rabbit.[(((((triple9) -> rule6)) -> rule8))] The tiger likes the tiger.[(((((triple9) -> rule6)) -> rule5))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple3
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple4
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple5
The squirrel is red.
("squirrel" "is" "red" "+")
triple6
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple7
((triple5) -> (rule8 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple8
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple9
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple10
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
((triple5) -> (rule5 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((triple9) -> (rule6 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
((((triple9) -> (rule6 % int2))) -> (rule8 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((triple9) -> (rule6 % int2))) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2