The bald eagle likes the squirrel. The bald eagle visits the squirrel. The dog sees the bald eagle. The squirrel likes the tiger. The tiger is kind. The tiger likes the bald eagle. The tiger does not like the squirrel. If someone sees the dog and the dog likes the tiger then the dog sees the squirrel. If the dog is red then the dog visits the tiger. If someone visits the bald eagle then they are rough. If someone sees the bald eagle then the bald eagle likes the dog. If someone likes the dog then they see the squirrel. If someone visits the bald eagle then they are not young.
The bald eagle likes the squirrel.
("bald eagle" "likes" "squirrel" "+")
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger likes the bald eagle.
("tiger" "likes" "bald eagle" "+")
The tiger does not like the squirrel.
("tiger" "likes" "squirrel" "-")
If someone sees the dog and the dog likes the tiger then the dog sees the squirrel.
((("someone" "sees" "dog" "+") ("dog" "likes" "tiger" "+")) -> ("dog" "sees" "squirrel" "+"))
If the dog is red then the dog visits the tiger.
((("dog" "is" "red" "+")) -> ("dog" "visits" "tiger" "+"))
If someone visits the bald eagle then they are rough.
((("someone" "visits" "bald eagle" "+")) -> ("someone" "is" "rough" "+"))
If someone sees the bald eagle then the bald eagle likes the dog.
((("someone" "sees" "bald eagle" "+")) -> ("bald eagle" "likes" "dog" "+"))
If someone likes the dog then they see the squirrel.
((("someone" "likes" "dog" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone visits the bald eagle then they are not young.
((("someone" "visits" "bald eagle" "+")) -> ("someone" "is" "young" "-"))
The dog sees the bald eagle.
True
1
proof
[(triple3)]
("dog" "sees" "bald eagle" "+")
triple3
The tiger likes the squirrel.
False
1
inv-proof
[(triple7)]
("tiger" "likes" "squirrel" "+")
triple7
The bald eagle likes the dog.
True
2
proof
[(((triple3) -> rule4))]
("bald eagle" "likes" "dog" "+")
((triple3) -> (rule4 % int1))
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
int1
The bald eagle does not like the dog.
False
2
inv-proof
[(((triple3) -> rule4))]
("bald eagle" "likes" "dog" "-")
((triple3) -> (rule4 % int1))
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
int1
The bald eagle sees the squirrel.
True
3
proof
[(((((triple3) -> rule4)) -> rule5))]
("bald eagle" "sees" "squirrel" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int1
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
int2
The bald eagle does not see the squirrel.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule5))]
("bald eagle" "sees" "squirrel" "-")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int1
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
int2
The tiger does not see the squirrel.
Unknown
inv-rconc
[@1: The tiger sees the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "sees" "squirrel" "-")
The dog visits the tiger.
Unknown
rconc
[@1: The dog visits the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "visits" "tiger" "+")
The squirrel is not rough.
Unknown
inv-rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "rough" "-")
The dog likes the bald eagle.
Unknown
random
[@0: The dog likes the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "bald eagle" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The bald eagle likes the squirrel.[(triple1)] The bald eagle visits the squirrel.[(triple2)] The dog sees the bald eagle.[(triple3)] The squirrel likes the tiger.[(triple4)] The tiger does not like the squirrel.[(triple7)] The tiger is kind.[(triple5)] The tiger likes the bald eagle.[(triple6)] @1: The bald eagle likes the dog.[(((triple3) -> rule4))] @2: The bald eagle sees the squirrel.[(((((triple3) -> rule4)) -> rule5))]
The bald eagle likes the squirrel.
("bald eagle" "likes" "squirrel" "+")
triple1
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
triple2
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
triple3
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple4
The tiger does not like the squirrel.
("tiger" "likes" "squirrel" "-")
triple7
The tiger is kind.
("tiger" "is" "kind" "+")
triple5
The tiger likes the bald eagle.
("tiger" "likes" "bald eagle" "+")
triple6
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
((triple3) -> (rule4 % int1))
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
int1
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int1
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
int2