The bald eagle sees the dog. The cow needs the dog. The dog sees the bald eagle. The squirrel sees the dog. If someone is young then they see the dog. If someone sees the cow and they are blue then the cow sees the squirrel. If someone is nice and they chase the dog then the dog sees the squirrel. If someone sees the bald eagle then the bald eagle is red. If someone sees the squirrel and they chase the cow then they do not chase the dog. If someone is cold then they need the cow. If someone needs the cow and the cow needs the squirrel then they are cold. If someone needs the cow then they are red.
The bald eagle sees the dog.
("bald eagle" "sees" "dog" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
If someone is young then they see the dog.
((("someone" "is" "young" "+")) -> ("someone" "sees" "dog" "+"))
If someone sees the cow and they are blue then the cow sees the squirrel.
((("someone" "sees" "cow" "+") ("someone" "is" "blue" "+")) -> ("cow" "sees" "squirrel" "+"))
If someone is nice and they chase the dog then the dog sees the squirrel.
((("someone" "is" "nice" "+") ("someone" "chases" "dog" "+")) -> ("dog" "sees" "squirrel" "+"))
If someone sees the bald eagle then the bald eagle is red.
((("someone" "sees" "bald eagle" "+")) -> ("bald eagle" "is" "red" "+"))
If someone sees the squirrel and they chase the cow then they do not chase the dog.
((("someone" "sees" "squirrel" "+") ("someone" "chases" "cow" "+")) -> ("someone" "chases" "dog" "-"))
If someone is cold then they need the cow.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "cow" "+"))
If someone needs the cow and the cow needs the squirrel then they are cold.
((("someone" "needs" "cow" "+") ("cow" "needs" "squirrel" "+")) -> ("someone" "is" "cold" "+"))
If someone needs the cow then they are red.
((("someone" "needs" "cow" "+")) -> ("someone" "is" "red" "+"))
The bald eagle sees the dog.
True
1
proof
[(triple1)]
("bald eagle" "sees" "dog" "+")
triple1
The bald eagle does not see the dog.
False
1
inv-proof
[(triple1)]
("bald eagle" "sees" "dog" "-")
triple1
The bald eagle is red.
True
2
proof
[(((triple3) -> rule4))]
("bald eagle" "is" "red" "+")
((triple3) -> (rule4 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
The bald eagle is not red.
False
2
inv-proof
[(((triple3) -> rule4))]
("bald eagle" "is" "red" "-")
((triple3) -> (rule4 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
The cow does not see the squirrel.
Unknown
inv-rconc
[@1: The cow sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "sees" "squirrel" "-")
The dog sees the dog.
Unknown
rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "dog" "+")
The dog does not chase the bald eagle.
Unknown
inv-random
[@0: The dog chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "bald eagle" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
@0: The bald eagle sees the dog.[(triple1)] The cow needs the dog.[(triple2)] The dog sees the bald eagle.[(triple3)] The squirrel sees the dog.[(triple4)] @1: The bald eagle is red.[(((triple3) -> rule4))]
The bald eagle sees the dog.
("bald eagle" "sees" "dog" "+")
triple1
The cow needs the dog.
("cow" "needs" "dog" "+")
triple2
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
triple3
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple4
The bald eagle is red.
("bald eagle" "is" "red" "+")
((triple3) -> (rule4 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1