The cat is green. The cat is young. The cat likes the tiger. The cat sees the squirrel. The lion chases the squirrel. The squirrel is young. The tiger is kind. If someone chases the squirrel then the squirrel sees the cat. If someone is young and they chase the squirrel then the squirrel is round.
The cat is green.
("cat" "is" "green" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
If someone chases the squirrel then the squirrel sees the cat.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "sees" "cat" "+"))
If someone is young and they chase the squirrel then the squirrel is round.
((("someone" "is" "young" "+") ("someone" "chases" "squirrel" "+")) -> ("squirrel" "is" "round" "+"))
The squirrel is young.
True
1
proof
[(triple6)]
("squirrel" "is" "young" "+")
triple6
The cat does not like the tiger.
False
1
inv-proof
[(triple3)]
("cat" "likes" "tiger" "-")
triple3
The squirrel sees the cat.
True
2
proof
[(((triple5) -> rule1))]
("squirrel" "sees" "cat" "+")
((triple5) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The squirrel does not see the cat.
False
2
inv-proof
[(((triple5) -> rule1))]
("squirrel" "sees" "cat" "-")
((triple5) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The squirrel is not round.
Unknown
inv-rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "round" "-")
The cat likes the lion.
Unknown
random
[@0: The cat likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "lion" "+")
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
@0: The cat is green.[(triple1)] The cat is young.[(triple2)] The cat likes the tiger.[(triple3)] The cat sees the squirrel.[(triple4)] The lion chases the squirrel.[(triple5)] The squirrel is young.[(triple6)] The tiger is kind.[(triple7)] @1: The squirrel sees the cat.[(((triple5) -> rule1))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat is young.
("cat" "is" "young" "+")
triple2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple3
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple4
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple5
The squirrel is young.
("squirrel" "is" "young" "+")
triple6
The tiger is kind.
("tiger" "is" "kind" "+")
triple7
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
((triple5) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1