The dog is blue. The rabbit is young. If something visits the rabbit then it does not chase the rabbit. If something is blue then it sees the rabbit.
The dog is blue.
("dog" "is" "blue" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
If something visits the rabbit then it does not chase the rabbit.
((("something" "visits" "rabbit" "+")) -> ("something" "chases" "rabbit" "-"))
If something is blue then it sees the rabbit.
((("something" "is" "blue" "+")) -> ("something" "sees" "rabbit" "+"))
The rabbit is young.
True
1
proof
[(triple2)]
("rabbit" "is" "young" "+")
triple2
The dog is not blue.
False
1
inv-proof
[(triple1)]
("dog" "is" "blue" "-")
triple1
The dog sees the rabbit.
True
2
proof
[(((triple1) -> rule2))]
("dog" "sees" "rabbit" "+")
((triple1) -> (rule2 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog does not see the rabbit.
False
2
inv-proof
[(((triple1) -> rule2))]
("dog" "sees" "rabbit" "-")
((triple1) -> (rule2 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
The dog is not young.
Unknown
inv-random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog is blue.[(triple1)] The rabbit is young.[(triple2)] @1: The dog sees the rabbit.[(((triple1) -> rule2))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The rabbit is young.
("rabbit" "is" "young" "+")
triple2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
((triple1) -> (rule2 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1