The cat chases the lion. The cat is rough. The cat sees the lion. The lion chases the squirrel. The squirrel is green. The squirrel is not nice. The squirrel needs the cat. The squirrel needs the lion. The squirrel sees the cat. The squirrel sees the lion. The tiger chases the squirrel. The tiger is nice. The tiger needs the cat. The tiger needs the lion. The tiger sees the lion. The tiger sees the squirrel. If something needs the lion then it sees the squirrel. If something needs the lion then the lion sees the cat. If something is blue and it needs the cat then it needs the squirrel. If something is green and it sees the squirrel then the squirrel does not see the tiger. If something needs the tiger then it needs the lion. If something sees the tiger and the tiger does not see the squirrel then it is not big.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is not nice.
("squirrel" "is" "nice" "-")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If something needs the lion then it sees the squirrel.
((("something" "needs" "lion" "+")) -> ("something" "sees" "squirrel" "+"))
If something needs the lion then the lion sees the cat.
((("something" "needs" "lion" "+")) -> ("lion" "sees" "cat" "+"))
If something is blue and it needs the cat then it needs the squirrel.
((("something" "is" "blue" "+") ("something" "needs" "cat" "+")) -> ("something" "needs" "squirrel" "+"))
If something is green and it sees the squirrel then the squirrel does not see the tiger.
((("something" "is" "green" "+") ("something" "sees" "squirrel" "+")) -> ("squirrel" "sees" "tiger" "-"))
If something needs the tiger then it needs the lion.
((("something" "needs" "tiger" "+")) -> ("something" "needs" "lion" "+"))
If something sees the tiger and the tiger does not see the squirrel then it is not big.
((("something" "sees" "tiger" "+") ("tiger" "sees" "squirrel" "~")) -> ("something" "is" "big" "-"))
The tiger sees the lion.
True
1
proof
[(triple15)]
("tiger" "sees" "lion" "+")
triple15
The squirrel does not see the lion.
False
1
inv-proof
[(triple10)]
("squirrel" "sees" "lion" "-")
triple10
The lion does not see the squirrel.
Unknown
inv-rconc
[@2: The lion sees the squirrel.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("lion" "sees" "squirrel" "-")
The squirrel chases the lion.
Unknown
random
[@0: The squirrel chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "lion" "+")
@0: The cat chases the lion.[(triple1)] The cat is rough.[(triple2)] The cat sees the lion.[(triple3)] The lion chases the squirrel.[(triple4)] The squirrel is green.[(triple5)] The squirrel is not nice.[(triple6)] The squirrel needs the cat.[(triple7)] The squirrel needs the lion.[(triple8)] The squirrel sees the cat.[(triple9)] The squirrel sees the lion.[(triple10)] The tiger chases the squirrel.[(triple11)] The tiger is nice.[(triple12)] The tiger needs the cat.[(triple13)] The tiger needs the lion.[(triple14)] The tiger sees the lion.[(triple15)] The tiger sees the squirrel.[(triple16 OR ((triple14) -> rule1))] @1: The lion sees the cat.[(((triple14) -> rule2) OR ((triple8) -> rule2))] The squirrel sees the squirrel.[(((triple8) -> rule1))] @2: The squirrel does not see the tiger.[(((triple5 ((triple8) -> rule1)) -> rule4))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat sees the lion.
("cat" "sees" "lion" "+")
triple3
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple4
The squirrel is green.
("squirrel" "is" "green" "+")
triple5
The squirrel is not nice.
("squirrel" "is" "nice" "-")
triple6
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple7
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple8
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple9
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple10
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple11
The tiger is nice.
("tiger" "is" "nice" "+")
triple12
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple13
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple14
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple15
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple16
((triple14) -> (rule1 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
((triple14) -> (rule2 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
((triple8) -> (rule2 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple8) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
((triple5 ((triple8) -> (rule1 % int2))) -> (rule4 % int1))
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2