The bald eagle is big. The mouse is red. The mouse visits the bald eagle. If the bald eagle chases the mouse and the mouse is big then the bald eagle likes the mouse. If something is cold then it visits the bald eagle. If something is kind then it is cold. If something visits the bald eagle then it is kind. If the mouse likes the bald eagle then the bald eagle is big. If something is cold and kind then it likes the mouse. If something is big then it chases the mouse. If something likes the mouse then the mouse visits the bald eagle.
The bald eagle is big.
("bald eagle" "is" "big" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
If the bald eagle chases the mouse and the mouse is big then the bald eagle likes the mouse.
((("bald eagle" "chases" "mouse" "+") ("mouse" "is" "big" "+")) -> ("bald eagle" "likes" "mouse" "+"))
If something is cold then it visits the bald eagle.
((("something" "is" "cold" "+")) -> ("something" "visits" "bald eagle" "+"))
If something is kind then it is cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something visits the bald eagle then it is kind.
((("something" "visits" "bald eagle" "+")) -> ("something" "is" "kind" "+"))
If the mouse likes the bald eagle then the bald eagle is big.
((("mouse" "likes" "bald eagle" "+")) -> ("bald eagle" "is" "big" "+"))
If something is cold and kind then it likes the mouse.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "likes" "mouse" "+"))
If something is big then it chases the mouse.
((("something" "is" "big" "+")) -> ("something" "chases" "mouse" "+"))
If something likes the mouse then the mouse visits the bald eagle.
((("something" "likes" "mouse" "+")) -> ("mouse" "visits" "bald eagle" "+"))
The mouse is red.
True
1
proof
[(triple2)]
("mouse" "is" "red" "+")
triple2
The bald eagle is not big.
False
1
inv-proof
[(triple1)]
("bald eagle" "is" "big" "-")
triple1
The bald eagle chases the mouse.
True
2
proof
[(((triple1) -> rule7))]
("bald eagle" "chases" "mouse" "+")
((triple1) -> (rule7 % int1))
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int1
The mouse is not kind.
False
2
inv-proof
[(((triple3) -> rule4))]
("mouse" "is" "kind" "-")
((triple3) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is cold.
True
3
proof
[(((((triple3) -> rule4)) -> rule3))]
("mouse" "is" "cold" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is not cold.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule3))]
("mouse" "is" "cold" "-")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse likes the mouse.
True
6
proof
[(((((((triple3) -> rule4)) -> rule3) ((triple3) -> rule4)) -> rule6))]
("mouse" "likes" "mouse" "+")
((((((triple3) -> (rule4 % int3))) -> (rule3 % int2)) ((triple3) -> (rule4 % int3))) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse does not like the mouse.
False
6
inv-proof
[(((((((triple3) -> rule4)) -> rule3) ((triple3) -> rule4)) -> rule6))]
("mouse" "likes" "mouse" "-")
((((((triple3) -> (rule4 % int3))) -> (rule3 % int2)) ((triple3) -> (rule4 % int3))) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The bald eagle is not cold.
Unknown
inv-rconc
[@3: The bald eagle is cold.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule2 <- FAIL)]]
("bald eagle" "is" "cold" "-")
The bald eagle likes the mouse.
Unknown
rconc
[@4: The bald eagle likes the mouse.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule4 <- rule2 <- FAIL)]]
("bald eagle" "likes" "mouse" "+")
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The bald eagle is kind.
Unknown
rconc
[@3: The bald eagle is kind.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule3 <- FAIL)]]
("bald eagle" "is" "kind" "+")
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 mouse chases the bald eagle.
Unknown
random
[@0: The mouse chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "bald eagle" "+")
The bald eagle is not red.
Unknown
inv-random
[@0: The bald eagle is red.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "red" "-")
The bald eagle chases the bald eagle.
Unknown
random
[@0: The bald eagle chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "bald eagle" "+")
@0: The bald eagle is big.[(triple1)] The mouse is red.[(triple2)] The mouse visits the bald eagle.[(triple3)] @1: The bald eagle chases the mouse.[(((triple1) -> rule7))] The mouse is kind.[(((triple3) -> rule4))] @2: The mouse is cold.[(((((triple3) -> rule4)) -> rule3))] @3: The mouse likes the mouse.[(((((((triple3) -> rule4)) -> rule3) ((triple3) -> rule4)) -> rule6))]
The bald eagle is big.
("bald eagle" "is" "big" "+")
triple1
The mouse is red.
("mouse" "is" "red" "+")
triple2
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
triple3
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
((triple1) -> (rule7 % int1))
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
((triple3) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((((triple3) -> (rule4 % int3))) -> (rule3 % int2)) ((triple3) -> (rule4 % int3))) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3