The bald eagle visits the lion. The cat is kind. The lion does not chase the cat. The mouse chases the bald eagle. The mouse chases the lion. The mouse needs the bald eagle. The mouse does not visit the bald eagle. If someone chases the bald eagle and they visit the lion then the lion visits the bald eagle. If the bald eagle is cold then the bald eagle visits the mouse. If the cat needs the lion then the cat is young. If someone chases the lion then they are kind. If someone needs the bald eagle then they are not rough. If someone is kind then they visit the mouse. If someone visits the bald eagle then they visit the mouse. If someone chases the lion and the lion needs the mouse then the lion is kind.
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
The cat is kind.
("cat" "is" "kind" "+")
The lion does not chase the cat.
("lion" "chases" "cat" "-")
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
The mouse does not visit the bald eagle.
("mouse" "visits" "bald eagle" "-")
If someone chases the bald eagle and they visit the lion then the lion visits the bald eagle.
((("someone" "chases" "bald eagle" "+") ("someone" "visits" "lion" "+")) -> ("lion" "visits" "bald eagle" "+"))
If the bald eagle is cold then the bald eagle visits the mouse.
((("bald eagle" "is" "cold" "+")) -> ("bald eagle" "visits" "mouse" "+"))
If the cat needs the lion then the cat is young.
((("cat" "needs" "lion" "+")) -> ("cat" "is" "young" "+"))
If someone chases the lion then they are kind.
((("someone" "chases" "lion" "+")) -> ("someone" "is" "kind" "+"))
If someone needs the bald eagle then they are not rough.
((("someone" "needs" "bald eagle" "+")) -> ("someone" "is" "rough" "-"))
If someone is kind then they visit the mouse.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "mouse" "+"))
If someone visits the bald eagle then they visit the mouse.
((("someone" "visits" "bald eagle" "+")) -> ("someone" "visits" "mouse" "+"))
If someone chases the lion and the lion needs the mouse then the lion is kind.
((("someone" "chases" "lion" "+") ("lion" "needs" "mouse" "+")) -> ("lion" "is" "kind" "+"))
The bald eagle visits the lion.
True
1
proof
[(triple1)]
("bald eagle" "visits" "lion" "+")
triple1
The cat is not kind.
False
1
inv-proof
[(triple2)]
("cat" "is" "kind" "-")
triple2
The cat visits the mouse.
True
2
proof
[(((triple2) -> rule6))]
("cat" "visits" "mouse" "+")
((triple2) -> (rule6 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The mouse is rough.
False
2
inv-proof
[(((triple6) -> rule5))]
("mouse" "is" "rough" "+")
((triple6) -> (rule5 % int1))
The mouse is not rough.
("mouse" "is" "rough" "-")
int1
The mouse visits the mouse.
True
3
proof
[(((((triple5) -> rule4)) -> rule6))]
("mouse" "visits" "mouse" "+")
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse does not visit the mouse.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule6))]
("mouse" "visits" "mouse" "-")
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "young" "-")
The lion visits the mouse.
Unknown
rconc
[@2: The lion visits the mouse.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("lion" "visits" "mouse" "+")
The bald eagle does not visit the mouse.
Unknown
inv-rconc
[@2: The bald eagle visits the mouse.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("bald eagle" "visits" "mouse" "-")
The cat chases the bald eagle.
Unknown
random
[@0: The cat chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "bald eagle" "+")
The bald eagle does not need the cat.
Unknown
inv-random
[@0: The bald eagle needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "cat" "-")
The mouse needs the cat.
Unknown
random
[@0: The mouse needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cat" "+")
@0: The bald eagle visits the lion.[(triple1)] The cat is kind.[(triple2)] The lion does not chase the cat.[(triple3)] The mouse chases the bald eagle.[(triple4)] The mouse chases the lion.[(triple5)] The mouse does not visit the bald eagle.[(triple7)] The mouse needs the bald eagle.[(triple6)] @1: The cat visits the mouse.[(((triple2) -> rule6))] The mouse is kind.[(((triple5) -> rule4))] The mouse is not rough.[(((triple6) -> rule5))] @2: The mouse visits the mouse.[(((((triple5) -> rule4)) -> rule6))]
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The lion does not chase the cat.
("lion" "chases" "cat" "-")
triple3
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
triple4
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple5
The mouse does not visit the bald eagle.
("mouse" "visits" "bald eagle" "-")
triple7
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
triple6
The cat visits the mouse.
("cat" "visits" "mouse" "+")
((triple2) -> (rule6 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
((triple5) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is not rough.
("mouse" "is" "rough" "-")
((triple6) -> (rule5 % int1))
The mouse is not rough.
("mouse" "is" "rough" "-")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2