The bald eagle sees the cat. The cat likes the mouse. The mouse visits the bald eagle. The squirrel is cold. If something likes the mouse then it sees the bald eagle. If something is red and it visits the squirrel then it is not kind. If something sees the bald eagle then the bald eagle does not like the mouse. If something is green then it likes the squirrel. If something likes the cat and it sees the cat then the cat visits the bald eagle. If the cat does not see the squirrel and the squirrel does not visit the mouse then the cat does not visit the squirrel. If something sees the bald eagle and it visits the squirrel then the bald eagle sees the cat. If the bald eagle likes the cat and the cat does not see the bald eagle then the bald eagle is kind.
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
If something likes the mouse then it sees the bald eagle.
((("something" "likes" "mouse" "+")) -> ("something" "sees" "bald eagle" "+"))
If something is red and it visits the squirrel then it is not kind.
((("something" "is" "red" "+") ("something" "visits" "squirrel" "+")) -> ("something" "is" "kind" "-"))
If something sees the bald eagle then the bald eagle does not like the mouse.
((("something" "sees" "bald eagle" "+")) -> ("bald eagle" "likes" "mouse" "-"))
If something is green then it likes the squirrel.
((("something" "is" "green" "+")) -> ("something" "likes" "squirrel" "+"))
If something likes the cat and it sees the cat then the cat visits the bald eagle.
((("something" "likes" "cat" "+") ("something" "sees" "cat" "+")) -> ("cat" "visits" "bald eagle" "+"))
If the cat does not see the squirrel and the squirrel does not visit the mouse then the cat does not visit the squirrel.
((("cat" "sees" "squirrel" "~") ("squirrel" "visits" "mouse" "~")) -> ("cat" "visits" "squirrel" "-"))
If something sees the bald eagle and it visits the squirrel then the bald eagle sees the cat.
((("something" "sees" "bald eagle" "+") ("something" "visits" "squirrel" "+")) -> ("bald eagle" "sees" "cat" "+"))
If the bald eagle likes the cat and the cat does not see the bald eagle then the bald eagle is kind.
((("bald eagle" "likes" "cat" "+") ("cat" "sees" "bald eagle" "~")) -> ("bald eagle" "is" "kind" "+"))
The cat likes the mouse.
True
1
proof
[(triple2)]
("cat" "likes" "mouse" "+")
triple2
The mouse does not visit the bald eagle.
False
1
inv-proof
[(triple3)]
("mouse" "visits" "bald eagle" "-")
triple3
The cat sees the bald eagle.
True
2
proof
[(((triple2) -> rule1))]
("cat" "sees" "bald eagle" "+")
((triple2) -> (rule1 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
The cat does not see the bald eagle.
False
2
inv-proof
[(((triple2) -> rule1))]
("cat" "sees" "bald eagle" "-")
((triple2) -> (rule1 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
The bald eagle does not like the mouse.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("bald eagle" "likes" "mouse" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The bald eagle does not like the mouse.
("bald eagle" "likes" "mouse" "-")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The bald eagle likes the mouse.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("bald eagle" "likes" "mouse" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The bald eagle does not like the mouse.
("bald eagle" "likes" "mouse" "-")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The mouse does not like the squirrel.
Unknown
inv-rconc
[@1: The mouse likes the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "likes" "squirrel" "-")
The bald eagle is kind.
Unknown
rconc
[@1: The bald eagle is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bald eagle" "is" "kind" "+")
The squirrel does not see the bald eagle.
Unknown
inv-rconc
[@1: The squirrel sees the bald eagle.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "bald eagle" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
The bald eagle does not see the squirrel.
Unknown
inv-random
[@0: The bald eagle sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "squirrel" "-")
The mouse sees the cat.
Unknown
random
[@0: The mouse sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "cat" "+")
@0: The bald eagle sees the cat.[(triple1)] The cat likes the mouse.[(triple2)] The mouse visits the bald eagle.[(triple3)] The squirrel is cold.[(triple4)] @1: The cat sees the bald eagle.[(((triple2) -> rule1))] @2: The bald eagle does not like the mouse.[(((((triple2) -> rule1)) -> rule3))]
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
triple1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple2
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
triple3
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple4
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
((triple2) -> (rule1 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
The bald eagle does not like the mouse.
("bald eagle" "likes" "mouse" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The bald eagle does not like the mouse.
("bald eagle" "likes" "mouse" "-")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2