The bald eagle is cold. The cow needs the bald eagle. The dog is blue. The squirrel is round. If someone needs the bald eagle then they are not blue. If someone likes the squirrel then the squirrel is not green. If someone is green then they do not chase the squirrel. If someone needs the dog then the dog likes the squirrel. If the dog likes the squirrel and the dog is cold then the squirrel likes the cow. If someone needs the squirrel then they are green. If someone is blue then they need the squirrel. If someone is nice and not blue then they chase the dog.
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
The dog is blue.
("dog" "is" "blue" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If someone needs the bald eagle then they are not blue.
((("someone" "needs" "bald eagle" "+")) -> ("someone" "is" "blue" "-"))
If someone likes the squirrel then the squirrel is not green.
((("someone" "likes" "squirrel" "+")) -> ("squirrel" "is" "green" "-"))
If someone is green then they do not chase the squirrel.
((("someone" "is" "green" "+")) -> ("someone" "chases" "squirrel" "-"))
If someone needs the dog then the dog likes the squirrel.
((("someone" "needs" "dog" "+")) -> ("dog" "likes" "squirrel" "+"))
If the dog likes the squirrel and the dog is cold then the squirrel likes the cow.
((("dog" "likes" "squirrel" "+") ("dog" "is" "cold" "+")) -> ("squirrel" "likes" "cow" "+"))
If someone needs the squirrel then they are green.
((("someone" "needs" "squirrel" "+")) -> ("someone" "is" "green" "+"))
If someone is blue then they need the squirrel.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone is nice and not blue then they chase the dog.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "~")) -> ("someone" "chases" "dog" "+"))
The dog is blue.
True
1
proof
[(triple3)]
("dog" "is" "blue" "+")
triple3
The bald eagle is not cold.
False
1
inv-proof
[(triple1)]
("bald eagle" "is" "cold" "-")
triple1
The cow is not blue.
True
2
proof
[(((triple2) -> rule1))]
("cow" "is" "blue" "-")
((triple2) -> (rule1 % int1))
The cow is not blue.
("cow" "is" "blue" "-")
int1
The cow is blue.
False
2
inv-proof
[(((triple2) -> rule1))]
("cow" "is" "blue" "+")
((triple2) -> (rule1 % int1))
The cow is not blue.
("cow" "is" "blue" "-")
int1
The dog is green.
True
3
proof
[(((((triple3) -> rule7)) -> rule6))]
("dog" "is" "green" "+")
((((triple3) -> (rule7 % int2))) -> (rule6 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int2
The dog is not green.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule6))]
("dog" "is" "green" "-")
((((triple3) -> (rule7 % int2))) -> (rule6 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int2
The dog does not chase the squirrel.
True
4
proof
[(((((((triple3) -> rule7)) -> rule6)) -> rule3))]
("dog" "chases" "squirrel" "-")
((((((triple3) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The dog does not chase the squirrel.
("dog" "chases" "squirrel" "-")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int3
The dog chases the squirrel.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule6)) -> rule3))]
("dog" "chases" "squirrel" "+")
((((((triple3) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The dog does not chase the squirrel.
("dog" "chases" "squirrel" "-")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int3
The squirrel does not like the cow.
Unknown
inv-rconc
[@1: The squirrel likes the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "likes" "cow" "-")
The squirrel is green.
Unknown
rconc
[@2: The squirrel is green.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("squirrel" "is" "green" "+")
The cow does not chase the dog.
Unknown
inv-rconc
[@1: The cow chases the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "chases" "dog" "-")
The bald eagle is green.
Unknown
rconc
[@2: The bald eagle is green.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("bald eagle" "is" "green" "+")
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
The bald eagle is not round.
Unknown
inv-random
[@0: The bald eagle is round.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "round" "-")
The bald eagle needs the bald eagle.
Unknown
random
[@0: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "bald eagle" "+")
@0: The bald eagle is cold.[(triple1)] The cow needs the bald eagle.[(triple2)] The dog is blue.[(triple3)] The squirrel is round.[(triple4)] @1: The cow is not blue.[(((triple2) -> rule1))] The dog needs the squirrel.[(((triple3) -> rule7))] @2: The dog is green.[(((((triple3) -> rule7)) -> rule6))] @3: The dog does not chase the squirrel.[(((((((triple3) -> rule7)) -> rule6)) -> rule3))]
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
triple1
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
triple2
The dog is blue.
("dog" "is" "blue" "+")
triple3
The squirrel is round.
("squirrel" "is" "round" "+")
triple4
The cow is not blue.
("cow" "is" "blue" "-")
((triple2) -> (rule1 % int1))
The cow is not blue.
("cow" "is" "blue" "-")
int1
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
((triple3) -> (rule7 % int1))
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int1
The dog is green.
("dog" "is" "green" "+")
((((triple3) -> (rule7 % int2))) -> (rule6 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int2
The dog does not chase the squirrel.
("dog" "chases" "squirrel" "-")
((((((triple3) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The dog does not chase the squirrel.
("dog" "chases" "squirrel" "-")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int3