The bald eagle visits the dog. The dog is nice. The squirrel needs the dog. If something needs the squirrel and the squirrel eats the dog then it needs the bald eagle. If something is young then it visits the squirrel. If something visits the squirrel then the squirrel visits the dog. If something eats the bald eagle and it needs the bald eagle then it visits the bald eagle. If something needs the dog then the dog is young. If something eats the bald eagle then the bald eagle eats the dog.
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
The dog is nice.
("dog" "is" "nice" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
If something needs the squirrel and the squirrel eats the dog then it needs the bald eagle.
((("something" "needs" "squirrel" "+") ("squirrel" "eats" "dog" "+")) -> ("something" "needs" "bald eagle" "+"))
If something is young then it visits the squirrel.
((("something" "is" "young" "+")) -> ("something" "visits" "squirrel" "+"))
If something visits the squirrel then the squirrel visits the dog.
((("something" "visits" "squirrel" "+")) -> ("squirrel" "visits" "dog" "+"))
If something eats the bald eagle and it needs the bald eagle then it visits the bald eagle.
((("something" "eats" "bald eagle" "+") ("something" "needs" "bald eagle" "+")) -> ("something" "visits" "bald eagle" "+"))
If something needs the dog then the dog is young.
((("something" "needs" "dog" "+")) -> ("dog" "is" "young" "+"))
If something eats the bald eagle then the bald eagle eats the dog.
((("something" "eats" "bald eagle" "+")) -> ("bald eagle" "eats" "dog" "+"))
The bald eagle visits the dog.
True
1
proof
[(triple1)]
("bald eagle" "visits" "dog" "+")
triple1
The bald eagle does not visit the dog.
False
1
inv-proof
[(triple1)]
("bald eagle" "visits" "dog" "-")
triple1
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
@0: The bald eagle visits the dog.[(triple1)] The dog is nice.[(triple2)] The squirrel needs the dog.[(triple3)] @1: The dog is young.[(((triple3) -> rule5))] @2: The dog visits the squirrel.[(((((triple3) -> rule5)) -> rule2))] @3: The squirrel visits the dog.[(((((((triple3) -> rule5)) -> rule2)) -> rule3))]
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
triple1
The dog is nice.
("dog" "is" "nice" "+")
triple2
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple3
The dog is young.
("dog" "is" "young" "+")
((triple3) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
((((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3