The bald eagle likes the dog. The cat needs the dog. The dog likes the cat. If something likes the cat then it needs the dog. If something needs the dog then it visits the bald eagle.
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
If something likes the cat then it needs the dog.
((("something" "likes" "cat" "+")) -> ("something" "needs" "dog" "+"))
If something needs the dog then it visits the bald eagle.
((("something" "needs" "dog" "+")) -> ("something" "visits" "bald eagle" "+"))
The dog likes the cat.
True
1
proof
[(triple3)]
("dog" "likes" "cat" "+")
triple3
The dog does not like the cat.
False
1
inv-proof
[(triple3)]
("dog" "likes" "cat" "-")
triple3
The dog needs the dog.
True
2
proof
[(((triple3) -> rule1))]
("dog" "needs" "dog" "+")
((triple3) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog does not need the dog.
False
2
inv-proof
[(((triple3) -> rule1))]
("dog" "needs" "dog" "-")
((triple3) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog visits the bald eagle.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("dog" "visits" "bald eagle" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The dog visits the bald eagle.
("dog" "visits" "bald eagle" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog does not visit the bald eagle.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("dog" "visits" "bald eagle" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The dog visits the bald eagle.
("dog" "visits" "bald eagle" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The bald eagle does not need the dog.
Unknown
inv-rconc
[@1: The bald eagle needs the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "needs" "dog" "-")
The bald eagle visits the bald eagle.
Unknown
rconc
[@2: The bald eagle visits the bald eagle.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("bald eagle" "visits" "bald eagle" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The bald eagle is round.
Unknown
random
[@0: The bald eagle is round.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "round" "+")
@0: The bald eagle likes the dog.[(triple1)] The cat needs the dog.[(triple2)] The dog likes the cat.[(triple3)] @1: The cat visits the bald eagle.[(((triple2) -> rule2))] The dog needs the dog.[(((triple3) -> rule1))] @2: The dog visits the bald eagle.[(((((triple3) -> rule1)) -> rule2))]
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
triple1
The cat needs the dog.
("cat" "needs" "dog" "+")
triple2
The dog likes the cat.
("dog" "likes" "cat" "+")
triple3
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
((triple2) -> (rule2 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple3) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog visits the bald eagle.
("dog" "visits" "bald eagle" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The dog visits the bald eagle.
("dog" "visits" "bald eagle" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2