The bald eagle is not red. The bear is nice. The mouse needs the bald eagle. If someone is nice and they chase the bear then they do not visit the mouse. If someone is blue then they chase the mouse. If the bald eagle chases the mouse then the bald eagle does not visit the mouse. If someone chases the bald eagle then the bald eagle does not need the mouse. If someone is nice then they need the mouse. If the mouse needs the bald eagle and the mouse does not visit the bald eagle then the mouse needs the bear. If someone needs the bald eagle then the bald eagle is blue. If someone chases the bear then the bear does not need the mouse.
The bald eagle is not red.
("bald eagle" "is" "red" "-")
The bear is nice.
("bear" "is" "nice" "+")
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
If someone is nice and they chase the bear then they do not visit the mouse.
((("someone" "is" "nice" "+") ("someone" "chases" "bear" "+")) -> ("someone" "visits" "mouse" "-"))
If someone is blue then they chase the mouse.
((("someone" "is" "blue" "+")) -> ("someone" "chases" "mouse" "+"))
If the bald eagle chases the mouse then the bald eagle does not visit the mouse.
((("bald eagle" "chases" "mouse" "+")) -> ("bald eagle" "visits" "mouse" "-"))
If someone chases the bald eagle then the bald eagle does not need the mouse.
((("someone" "chases" "bald eagle" "+")) -> ("bald eagle" "needs" "mouse" "-"))
If someone is nice then they need the mouse.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "mouse" "+"))
If the mouse needs the bald eagle and the mouse does not visit the bald eagle then the mouse needs the bear.
((("mouse" "needs" "bald eagle" "+") ("mouse" "visits" "bald eagle" "~")) -> ("mouse" "needs" "bear" "+"))
If someone needs the bald eagle then the bald eagle is blue.
((("someone" "needs" "bald eagle" "+")) -> ("bald eagle" "is" "blue" "+"))
If someone chases the bear then the bear does not need the mouse.
((("someone" "chases" "bear" "+")) -> ("bear" "needs" "mouse" "-"))
The bear is nice.
True
1
proof
[(triple2)]
("bear" "is" "nice" "+")
triple2
The mouse does not need the bald eagle.
False
1
inv-proof
[(triple3)]
("mouse" "needs" "bald eagle" "-")
triple3
The bear needs the mouse.
True
2
proof
[(((triple2) -> rule5))]
("bear" "needs" "mouse" "+")
((triple2) -> (rule5 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bald eagle is not blue.
False
2
inv-proof
[(((triple3) -> rule7))]
("bald eagle" "is" "blue" "-")
((triple3) -> (rule7 % int1))
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int1
The bald eagle chases the mouse.
True
3
proof
[(((((triple3) -> rule7)) -> rule2))]
("bald eagle" "chases" "mouse" "+")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int2
The bald eagle does not chase the mouse.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule2))]
("bald eagle" "chases" "mouse" "-")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int2
The bald eagle does not visit the mouse.
True
4
proof
[(((((((triple3) -> rule7)) -> rule2)) -> rule3))]
("bald eagle" "visits" "mouse" "-")
((((((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle does not visit the mouse.
("bald eagle" "visits" "mouse" "-")
int1
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int2
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int3
The bald eagle visits the mouse.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule2)) -> rule3))]
("bald eagle" "visits" "mouse" "+")
((((((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle does not visit the mouse.
("bald eagle" "visits" "mouse" "-")
int1
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int2
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int3
The bald eagle does not need the mouse.
Unknown
inv-rconc
[@1: The bald eagle needs the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "needs" "mouse" "-")
The mouse chases the mouse.
Unknown
rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "chases" "mouse" "+")
The bear does not chase the mouse.
Unknown
inv-rconc
[@1: The bear chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "chases" "mouse" "-")
The mouse needs the bear.
Unknown
rconc
[@1: The mouse needs the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "needs" "bear" "+")
The mouse does not visit the bear.
Unknown
inv-random
[@0: The mouse visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bear" "-")
The mouse visits the bald eagle.
Unknown
random
[@0: The mouse visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bald eagle" "+")
The bald eagle does not visit the bear.
Unknown
inv-random
[@0: The bald eagle visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "bear" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
@0: The bald eagle is not red.[(triple1)] The bear is nice.[(triple2)] The mouse needs the bald eagle.[(triple3)] @1: The bald eagle is blue.[(((triple3) -> rule7))] The bear needs the mouse.[(((triple2) -> rule5))] @2: The bald eagle chases the mouse.[(((((triple3) -> rule7)) -> rule2))] @3: The bald eagle does not visit the mouse.[(((((((triple3) -> rule7)) -> rule2)) -> rule3))]
The bald eagle is not red.
("bald eagle" "is" "red" "-")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
triple3
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
((triple3) -> (rule7 % int1))
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
((triple2) -> (rule5 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int2
The bald eagle does not visit the mouse.
("bald eagle" "visits" "mouse" "-")
((((((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle does not visit the mouse.
("bald eagle" "visits" "mouse" "-")
int1
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int2
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int3