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