The bald eagle likes the mouse. The mouse chases the bald eagle. The squirrel is kind. If someone likes the squirrel and they chase the mouse then they do not visit the bald eagle. If someone likes the bald eagle then they are round. If someone likes the squirrel and the squirrel does not like the bald eagle then they visit the mouse. If someone is round then they do not visit the mouse. If the bald eagle likes the squirrel and the bald eagle is big then the squirrel is nice. If someone likes the bald eagle then they like the mouse. If someone likes the mouse then the mouse likes the bald eagle. If someone chases the bald eagle then the bald eagle likes the mouse.
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
If someone likes the squirrel and they chase the mouse then they do not visit the bald eagle.
((("someone" "likes" "squirrel" "+") ("someone" "chases" "mouse" "+")) -> ("someone" "visits" "bald eagle" "-"))
If someone likes the bald eagle then they are round.
((("someone" "likes" "bald eagle" "+")) -> ("someone" "is" "round" "+"))
If someone likes the squirrel and the squirrel does not like the bald eagle then they visit the mouse.
((("someone" "likes" "squirrel" "+") ("squirrel" "likes" "bald eagle" "~")) -> ("someone" "visits" "mouse" "+"))
If someone is round then they do not visit the mouse.
((("someone" "is" "round" "+")) -> ("someone" "visits" "mouse" "-"))
If the bald eagle likes the squirrel and the bald eagle is big then the squirrel is nice.
((("bald eagle" "likes" "squirrel" "+") ("bald eagle" "is" "big" "+")) -> ("squirrel" "is" "nice" "+"))
If someone likes the bald eagle then they like the mouse.
((("someone" "likes" "bald eagle" "+")) -> ("someone" "likes" "mouse" "+"))
If someone likes the mouse then the mouse likes the bald eagle.
((("someone" "likes" "mouse" "+")) -> ("mouse" "likes" "bald eagle" "+"))
If someone chases the bald eagle then the bald eagle likes the mouse.
((("someone" "chases" "bald eagle" "+")) -> ("bald eagle" "likes" "mouse" "+"))
The bald eagle likes the mouse.
True
1
proof
[(triple1 OR ((triple2) -> rule8))]
("bald eagle" "likes" "mouse" "+")
triple1
((triple2) -> (rule8 % int1))
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int1
The mouse does not chase the bald eagle.
False
1
inv-proof
[(triple2)]
("mouse" "chases" "bald eagle" "-")
triple2
The mouse likes the bald eagle.
True
2
proof
[(((triple1) -> rule7) OR ((((triple2) -> rule8)) -> rule7))]
("mouse" "likes" "bald eagle" "+")
((triple1) -> (rule7 % int1))
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int1
((((triple2) -> (rule8 % int2))) -> (rule7 % int1))
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int1
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int2
The mouse does not like the bald eagle.
False
2
inv-proof
[(((triple1) -> rule7) OR ((((triple2) -> rule8)) -> rule7))]
("mouse" "likes" "bald eagle" "-")
((triple1) -> (rule7 % int1))
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int1
((((triple2) -> (rule8 % int2))) -> (rule7 % int1))
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int1
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int2
The mouse likes the mouse.
True
3
proof
[(((((triple1) -> rule7)) -> rule6) OR ((((((triple2) -> rule8)) -> rule7)) -> rule6))]
("mouse" "likes" "mouse" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int2
((((((triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int2
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int3
The mouse does not like the mouse.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule6) OR ((((((triple2) -> rule8)) -> rule7)) -> rule6))]
("mouse" "likes" "mouse" "-")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int2
((((((triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int2
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int3
The mouse does not visit the mouse.
True
4
proof
[(((((((triple1) -> rule7)) -> rule2)) -> rule4) OR ((((((((triple2) -> rule8)) -> rule7)) -> rule2)) -> rule4))]
("mouse" "visits" "mouse" "-")
((((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int3
((((((((triple2) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int3
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int4
The mouse visits the mouse.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule2)) -> rule4) OR ((((((((triple2) -> rule8)) -> rule7)) -> rule2)) -> rule4))]
("mouse" "visits" "mouse" "+")
((((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int3
((((((((triple2) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int3
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int4
The squirrel does not like the mouse.
Unknown
inv-rconc
[@1: The squirrel likes the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "likes" "mouse" "-")
The squirrel visits the mouse.
Unknown
rconc
[@1: The squirrel visits the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "visits" "mouse" "+")
The bald eagle is not round.
Unknown
inv-rconc
[@1: The bald eagle is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "is" "round" "-")
The bald eagle visits the mouse.
Unknown
rconc
[@1: The bald eagle visits the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "visits" "mouse" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
The bald eagle does not chase the bald eagle.
Unknown
inv-random
[@0: The bald eagle chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "bald eagle" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
@0: The bald eagle likes the mouse.[(triple1 OR ((triple2) -> rule8))] The mouse chases the bald eagle.[(triple2)] The squirrel is kind.[(triple3)] @1: The mouse likes the bald eagle.[(((triple1) -> rule7) OR ((((triple2) -> rule8)) -> rule7))] @2: The mouse is round.[(((((triple1) -> rule7)) -> rule2) OR ((((((triple2) -> rule8)) -> rule7)) -> rule2))] The mouse likes the mouse.[(((((triple1) -> rule7)) -> rule6) OR ((((((triple2) -> rule8)) -> rule7)) -> rule6))] @3: The mouse does not visit the mouse.[(((((((triple1) -> rule7)) -> rule2)) -> rule4) OR ((((((((triple2) -> rule8)) -> rule7)) -> rule2)) -> rule4))]
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
triple1
((triple2) -> (rule8 % int1))
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int1
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
triple2
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple3
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
((triple1) -> (rule7 % int1))
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int1
((((triple2) -> (rule8 % int2))) -> (rule7 % int1))
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int1
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int2
((((((triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int2
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int3
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int2
((((((triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int2
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int3
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
((((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int3
((((((((triple2) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int3
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int4