The lion eats the rabbit. The lion needs the rabbit. The lion sees the rabbit. The lion sees the squirrel. The lion sees the tiger. The rabbit eats the lion. The rabbit is blue. The rabbit needs the squirrel. The rabbit sees the lion. The squirrel needs the rabbit. The tiger eats the rabbit. The tiger needs the lion. If something sees the squirrel and it sees the lion then the lion sees the rabbit. If something needs the lion then it eats the rabbit. If the rabbit sees the squirrel and the squirrel needs the lion then the rabbit needs the lion.
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If something sees the squirrel and it sees the lion then the lion sees the rabbit.
((("something" "sees" "squirrel" "+") ("something" "sees" "lion" "+")) -> ("lion" "sees" "rabbit" "+"))
If something needs the lion then it eats the rabbit.
((("something" "needs" "lion" "+")) -> ("something" "eats" "rabbit" "+"))
If the rabbit sees the squirrel and the squirrel needs the lion then the rabbit needs the lion.
((("rabbit" "sees" "squirrel" "+") ("squirrel" "needs" "lion" "+")) -> ("rabbit" "needs" "lion" "+"))
The tiger eats the rabbit.
True
1
proof
[(triple11 OR ((triple12) -> rule2))]
("tiger" "eats" "rabbit" "+")
triple11
((triple12) -> (rule2 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The lion does not see the rabbit.
False
1
inv-proof
[(triple3)]
("lion" "sees" "rabbit" "-")
triple3
The rabbit does not need the lion.
Unknown
inv-rconc
[@1: The rabbit needs the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "needs" "lion" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The lion eats the rabbit.[(triple1)] The lion needs the rabbit.[(triple2)] The lion sees the rabbit.[(triple3)] The lion sees the squirrel.[(triple4)] The lion sees the tiger.[(triple5)] The rabbit eats the lion.[(triple6)] The rabbit is blue.[(triple7)] The rabbit needs the squirrel.[(triple8)] The rabbit sees the lion.[(triple9)] The squirrel needs the rabbit.[(triple10)] The tiger eats the rabbit.[(triple11 OR ((triple12) -> rule2))] The tiger needs the lion.[(triple12)]
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple2
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple3
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple4
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple5
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple6
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple7
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple8
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple9
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple10
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple11
((triple12) -> (rule2 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple12