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