The dog is kind. The dog is young. The mouse needs the rabbit. The mouse sees the rabbit. The rabbit likes the mouse. The rabbit needs the dog. The rabbit sees the dog. If something sees the mouse then it does not need the dog. If the mouse sees the dog and the dog does not need the mouse then the mouse does not need the dog. If the dog needs the rabbit then the rabbit sees the mouse. If something needs the rabbit then the rabbit needs the mouse. If something sees the dog and it sees the rabbit then it is round. If something is round and it does not see the mouse then it is kind.
The dog is kind.
("dog" "is" "kind" "+")
The dog is young.
("dog" "is" "young" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If something sees the mouse then it does not need the dog.
((("something" "sees" "mouse" "+")) -> ("something" "needs" "dog" "-"))
If the mouse sees the dog and the dog does not need the mouse then the mouse does not need the dog.
((("mouse" "sees" "dog" "+") ("dog" "needs" "mouse" "~")) -> ("mouse" "needs" "dog" "-"))
If the dog needs the rabbit then the rabbit sees the mouse.
((("dog" "needs" "rabbit" "+")) -> ("rabbit" "sees" "mouse" "+"))
If something needs the rabbit then the rabbit needs the mouse.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "needs" "mouse" "+"))
If something sees the dog and it sees the rabbit then it is round.
((("something" "sees" "dog" "+") ("something" "sees" "rabbit" "+")) -> ("something" "is" "round" "+"))
If something is round and it does not see the mouse then it is kind.
((("something" "is" "round" "+") ("something" "sees" "mouse" "~")) -> ("something" "is" "kind" "+"))
The dog is kind.
True
1
proof
[(triple1)]
("dog" "is" "kind" "+")
triple1
The dog is not young.
False
1
inv-proof
[(triple2)]
("dog" "is" "young" "-")
triple2
The mouse is not kind.
Unknown
inv-rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "kind" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
@0: The dog is kind.[(triple1)] The dog is young.[(triple2)] The mouse needs the rabbit.[(triple3)] The mouse sees the rabbit.[(triple4)] The rabbit likes the mouse.[(triple5)] The rabbit needs the dog.[(triple6)] The rabbit sees the dog.[(triple7)] @1: The rabbit needs the mouse.[(((triple3) -> rule4))]
The dog is kind.
("dog" "is" "kind" "+")
triple1
The dog is young.
("dog" "is" "young" "+")
triple2
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple3
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple4
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple5
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple6
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple7
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
((triple3) -> (rule4 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1