The bald eagle likes the cat. The cat is kind. The cat likes the squirrel. The cat sees the tiger. The squirrel is big. The squirrel is nice. The squirrel likes the cat. The squirrel needs the tiger. The squirrel sees the bald eagle. The tiger likes the squirrel. If someone is kind then they see the squirrel.
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
If someone is kind then they see the squirrel.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "squirrel" "+"))
The squirrel likes the cat.
True
1
proof
[(triple7)]
("squirrel" "likes" "cat" "+")
triple7
The squirrel is not big.
False
1
inv-proof
[(triple5)]
("squirrel" "is" "big" "-")
triple5
The cat sees the squirrel.
True
2
proof
[(((triple2) -> rule1))]
("cat" "sees" "squirrel" "+")
((triple2) -> (rule1 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat does not see the squirrel.
False
2
inv-proof
[(((triple2) -> rule1))]
("cat" "sees" "squirrel" "-")
((triple2) -> (rule1 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The tiger sees the squirrel.
Unknown
rconc
[@1: The tiger sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "squirrel" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The bald eagle likes the tiger.
Unknown
random
[@0: The bald eagle likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "likes" "tiger" "+")
@0: The bald eagle likes the cat.[(triple1)] The cat is kind.[(triple2)] The cat likes the squirrel.[(triple3)] The cat sees the tiger.[(triple4)] The squirrel is big.[(triple5)] The squirrel is nice.[(triple6)] The squirrel likes the cat.[(triple7)] The squirrel needs the tiger.[(triple8)] The squirrel sees the bald eagle.[(triple9)] The tiger likes the squirrel.[(triple10)] @1: The cat sees the squirrel.[(((triple2) -> rule1))]
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple4
The squirrel is big.
("squirrel" "is" "big" "+")
triple5
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple6
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple7
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple8
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
triple9
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple10
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
((triple2) -> (rule1 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1