The dog is kind. The dog is red. The dog needs the rabbit. The dog does not see the rabbit. The rabbit is red. The rabbit needs the dog. The rabbit sees the dog. If someone visits the dog and they see the rabbit then the rabbit sees the dog. If someone is young then they need the dog. If the rabbit sees the dog then the rabbit is young.
The dog is kind.
("dog" "is" "kind" "+")
The dog is red.
("dog" "is" "red" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog does not see the rabbit.
("dog" "sees" "rabbit" "-")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If someone visits the dog and they see the rabbit then the rabbit sees the dog.
((("someone" "visits" "dog" "+") ("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "dog" "+"))
If someone is young then they need the dog.
((("someone" "is" "young" "+")) -> ("someone" "needs" "dog" "+"))
If the rabbit sees the dog then the rabbit is young.
((("rabbit" "sees" "dog" "+")) -> ("rabbit" "is" "young" "+"))
The dog does not see the rabbit.
True
1
proof
[(triple4)]
("dog" "sees" "rabbit" "-")
triple4
The dog sees the rabbit.
False
1
inv-proof
[(triple4)]
("dog" "sees" "rabbit" "+")
triple4
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "dog" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
@0: The dog does not see the rabbit.[(triple4)] The dog is kind.[(triple1)] The dog is red.[(triple2)] The dog needs the rabbit.[(triple3)] The rabbit is red.[(triple5)] The rabbit needs the dog.[(triple6 OR ((((triple7) -> rule3)) -> rule2))] The rabbit sees the dog.[(triple7)] @1: The rabbit is young.[(((triple7) -> rule3))]
The dog does not see the rabbit.
("dog" "sees" "rabbit" "-")
triple4
The dog is kind.
("dog" "is" "kind" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple3
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple6
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple7
The rabbit is young.
("rabbit" "is" "young" "+")
((triple7) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1