The bald eagle sees the dog. The cat is nice. The cow is rough. The dog sees the bald eagle. If something is nice then it does not need the dog. If the bald eagle chases the dog and the bald eagle is not blue then the dog needs the cow.
The bald eagle sees the dog.
("bald eagle" "sees" "dog" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cow is rough.
("cow" "is" "rough" "+")
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
If something is nice then it does not need the dog.
((("something" "is" "nice" "+")) -> ("something" "needs" "dog" "-"))
If the bald eagle chases the dog and the bald eagle is not blue then the dog needs the cow.
((("bald eagle" "chases" "dog" "+") ("bald eagle" "is" "blue" "~")) -> ("dog" "needs" "cow" "+"))
The cow is rough.
True
1
proof
[(triple3)]
("cow" "is" "rough" "+")
triple3
The cat is not nice.
False
1
inv-proof
[(triple2)]
("cat" "is" "nice" "-")
triple2
The cat does not need the dog.
True
2
proof
[(((triple2) -> rule1))]
("cat" "needs" "dog" "-")
((triple2) -> (rule1 % int1))
The cat does not need the dog.
("cat" "needs" "dog" "-")
int1
The cat needs the dog.
False
2
inv-proof
[(((triple2) -> rule1))]
("cat" "needs" "dog" "+")
((triple2) -> (rule1 % int1))
The cat does not need the dog.
("cat" "needs" "dog" "-")
int1
The dog does not need the cow.
Unknown
inv-rconc
[@1: The dog needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "cow" "-")
The cow needs the dog.
Unknown
random
[@0: The cow needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "dog" "+")
The cat does not chase the cow.
Unknown
inv-random
[@0: The cat chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cow" "-")
The cow sees the cat.
Unknown
random
[@0: The cow sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cat" "+")
@0: The bald eagle sees the dog.[(triple1)] The cat is nice.[(triple2)] The cow is rough.[(triple3)] The dog sees the bald eagle.[(triple4)] @1: The cat does not need the dog.[(((triple2) -> rule1))]
The bald eagle sees the dog.
("bald eagle" "sees" "dog" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cow is rough.
("cow" "is" "rough" "+")
triple3
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
triple4
The cat does not need the dog.
("cat" "needs" "dog" "-")
((triple2) -> (rule1 % int1))
The cat does not need the dog.
("cat" "needs" "dog" "-")
int1