The bald eagle is not kind. The mouse is red. The rabbit sees the mouse. If the rabbit sees the mouse then the rabbit is kind. If something sees the bald eagle and the bald eagle sees the rabbit then the bald eagle is blue. If something is round and it chases the mouse then it visits the mouse. If something sees the mouse and the mouse sees the rabbit then it sees the bald eagle. If the mouse chases the bald eagle and the bald eagle does not chase the mouse then the bald eagle visits the mouse. If something sees the rabbit and it chases the bald eagle then it is not round.
The bald eagle is not kind.
("bald eagle" "is" "kind" "-")
The mouse is red.
("mouse" "is" "red" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If the rabbit sees the mouse then the rabbit is kind.
((("rabbit" "sees" "mouse" "+")) -> ("rabbit" "is" "kind" "+"))
If something sees the bald eagle and the bald eagle sees the rabbit then the bald eagle is blue.
((("something" "sees" "bald eagle" "+") ("bald eagle" "sees" "rabbit" "+")) -> ("bald eagle" "is" "blue" "+"))
If something is round and it chases the mouse then it visits the mouse.
((("something" "is" "round" "+") ("something" "chases" "mouse" "+")) -> ("something" "visits" "mouse" "+"))
If something sees the mouse and the mouse sees the rabbit then it sees the bald eagle.
((("something" "sees" "mouse" "+") ("mouse" "sees" "rabbit" "+")) -> ("something" "sees" "bald eagle" "+"))
If the mouse chases the bald eagle and the bald eagle does not chase the mouse then the bald eagle visits the mouse.
((("mouse" "chases" "bald eagle" "+") ("bald eagle" "chases" "mouse" "~")) -> ("bald eagle" "visits" "mouse" "+"))
If something sees the rabbit and it chases the bald eagle then it is not round.
((("something" "sees" "rabbit" "+") ("something" "chases" "bald eagle" "+")) -> ("something" "is" "round" "-"))
The mouse is red.
True
1
proof
[(triple2)]
("mouse" "is" "red" "+")
triple2
The bald eagle is kind.
False
1
inv-proof
[(triple1)]
("bald eagle" "is" "kind" "+")
triple1
The rabbit is kind.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "is" "kind" "+")
((triple3) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is not kind.
False
2
inv-proof
[(((triple3) -> rule1))]
("rabbit" "is" "kind" "-")
((triple3) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit does not see the bald eagle.
Unknown
inv-rconc
[@1: The rabbit sees the bald eagle.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "sees" "bald eagle" "-")
The mouse sees the bald eagle.
Unknown
rconc
[@1: The mouse sees the bald eagle.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "bald eagle" "+")
The bald eagle does not chase the rabbit.
Unknown
inv-random
[@0: The bald eagle chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "rabbit" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
@0: The bald eagle is not kind.[(triple1)] The mouse is red.[(triple2)] The rabbit sees the mouse.[(triple3)] @1: The rabbit is kind.[(((triple3) -> rule1))]
The bald eagle is not kind.
("bald eagle" "is" "kind" "-")
triple1
The mouse is red.
("mouse" "is" "red" "+")
triple2
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple3
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple3) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1