The bald eagle is kind. The bald eagle visits the dog. The dog is red. The dog likes the bald eagle. The dog likes the mouse. The dog does not visit the bald eagle. The mouse does not visit the bald eagle. If something needs the mouse and it does not need the dog then the dog visits the bald eagle. If the dog visits the bald eagle and the bald eagle needs the mouse then the bald eagle is nice. If something is red and it does not visit the dog then the dog is kind. If the bald eagle likes the mouse then the mouse is kind. If something is kind then it likes the mouse. If something needs the mouse and it is not nice then it needs the bald eagle.
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
The dog is red.
("dog" "is" "red" "+")
The dog likes the bald eagle.
("dog" "likes" "bald eagle" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog does not visit the bald eagle.
("dog" "visits" "bald eagle" "-")
The mouse does not visit the bald eagle.
("mouse" "visits" "bald eagle" "-")
If something needs the mouse and it does not need the dog then the dog visits the bald eagle.
((("something" "needs" "mouse" "+") ("something" "needs" "dog" "~")) -> ("dog" "visits" "bald eagle" "+"))
If the dog visits the bald eagle and the bald eagle needs the mouse then the bald eagle is nice.
((("dog" "visits" "bald eagle" "+") ("bald eagle" "needs" "mouse" "+")) -> ("bald eagle" "is" "nice" "+"))
If something is red and it does not visit the dog then the dog is kind.
((("something" "is" "red" "+") ("something" "visits" "dog" "~")) -> ("dog" "is" "kind" "+"))
If the bald eagle likes the mouse then the mouse is kind.
((("bald eagle" "likes" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If something is kind then it likes the mouse.
((("something" "is" "kind" "+")) -> ("something" "likes" "mouse" "+"))
If something needs the mouse and it is not nice then it needs the bald eagle.
((("something" "needs" "mouse" "+") ("something" "is" "nice" "~")) -> ("something" "needs" "bald eagle" "+"))
The dog likes the bald eagle.
True
1
proof
[(triple4)]
("dog" "likes" "bald eagle" "+")
triple4
The bald eagle does not visit the dog.
False
1
inv-proof
[(triple2)]
("bald eagle" "visits" "dog" "-")
triple2
The bald eagle likes the mouse.
True
2
proof
[(((triple1) -> rule5))]
("bald eagle" "likes" "mouse" "+")
((triple1) -> (rule5 % int1))
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int1
The bald eagle does not like the mouse.
False
2
inv-proof
[(((triple1) -> rule5))]
("bald eagle" "likes" "mouse" "-")
((triple1) -> (rule5 % int1))
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int1
The mouse is kind.
True
3
proof
[(((((triple1) -> rule5)) -> rule4))]
("mouse" "is" "kind" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int2
The mouse is not kind.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("mouse" "is" "kind" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int2
The mouse likes the mouse.
True
4
proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule5))]
("mouse" "likes" "mouse" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int3
The mouse does not like the mouse.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule5))]
("mouse" "likes" "mouse" "-")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int3
The dog is not kind.
Unknown
inv-rconc
[@1: The dog is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "kind" "-")
The bald eagle is nice.
Unknown
rconc
[@1: The bald eagle is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "is" "nice" "+")
The bald eagle does not need the bald eagle.
Unknown
inv-rconc
[@1: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "needs" "bald eagle" "-")
The dog needs the bald eagle.
Unknown
rconc
[@1: The dog needs the bald eagle.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "needs" "bald eagle" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The dog needs the mouse.
Unknown
random
[@0: The dog needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "mouse" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
@0: The bald eagle is kind.[(triple1)] The bald eagle visits the dog.[(triple2)] The dog does not visit the bald eagle.[(triple6)] The dog is red.[(triple3)] The dog likes the bald eagle.[(triple4)] The dog likes the mouse.[(triple5)] The mouse does not visit the bald eagle.[(triple7)] @1: The bald eagle likes the mouse.[(((triple1) -> rule5))] @2: The mouse is kind.[(((((triple1) -> rule5)) -> rule4))] @3: The mouse likes the mouse.[(((((((triple1) -> rule5)) -> rule4)) -> rule5))]
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
triple1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
triple2
The dog does not visit the bald eagle.
("dog" "visits" "bald eagle" "-")
triple6
The dog is red.
("dog" "is" "red" "+")
triple3
The dog likes the bald eagle.
("dog" "likes" "bald eagle" "+")
triple4
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple5
The mouse does not visit the bald eagle.
("mouse" "visits" "bald eagle" "-")
triple7
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
((triple1) -> (rule5 % int1))
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int3