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