The dog visits the rabbit. The lion is blue. The mouse is green. The rabbit chases the mouse. If someone is blue then they need the mouse.
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The lion is blue.
("lion" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
If someone is blue then they need the mouse.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "mouse" "+"))
The rabbit chases the mouse.
True
1
proof
[(triple4)]
("rabbit" "chases" "mouse" "+")
triple4
The lion is not blue.
False
1
inv-proof
[(triple2)]
("lion" "is" "blue" "-")
triple2
The lion needs the mouse.
True
2
proof
[(((triple2) -> rule1))]
("lion" "needs" "mouse" "+")
((triple2) -> (rule1 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion does not need the mouse.
False
2
inv-proof
[(((triple2) -> rule1))]
("lion" "needs" "mouse" "-")
((triple2) -> (rule1 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The rabbit does not need the mouse.
Unknown
inv-rconc
[@1: The rabbit needs the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "mouse" "-")
The dog needs the mouse.
Unknown
rconc
[@1: The dog needs the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "needs" "mouse" "+")
The rabbit is not red.
Unknown
inv-random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The dog visits the rabbit.[(triple1)] The lion is blue.[(triple2)] The mouse is green.[(triple3)] The rabbit chases the mouse.[(triple4)] @1: The lion needs the mouse.[(((triple2) -> rule1))]
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple1
The lion is blue.
("lion" "is" "blue" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple4
The lion needs the mouse.
("lion" "needs" "mouse" "+")
((triple2) -> (rule1 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1