The dog sees the rabbit. The rabbit is red. The rabbit sees the dog. If someone sees the rabbit then the rabbit eats the dog. If someone eats the dog then they are red.
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If someone sees the rabbit then the rabbit eats the dog.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "eats" "dog" "+"))
If someone eats the dog then they are red.
((("someone" "eats" "dog" "+")) -> ("someone" "is" "red" "+"))
The rabbit sees the dog.
True
1
proof
[(triple3)]
("rabbit" "sees" "dog" "+")
triple3
The rabbit is not red.
False
1
inv-proof
[(triple2 OR ((((triple1) -> rule1)) -> rule2))]
("rabbit" "is" "red" "-")
triple2
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int2
The dog is not red.
Unknown
inv-rconc
[@1: The dog is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "red" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The dog sees the rabbit.[(triple1)] The rabbit is red.[(triple2 OR ((((triple1) -> rule1)) -> rule2))] The rabbit sees the dog.[(triple3)] @1: The rabbit eats the dog.[(((triple1) -> rule1))]
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple1
The rabbit is red.
("rabbit" "is" "red" "+")
triple2
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple3
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
((triple1) -> (rule1 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1