The dog is not rough. The dog sees the tiger. The mouse chases the dog. The mouse needs the dog. The rabbit does not need the dog. The rabbit needs the mouse. The tiger needs the dog. If someone chases the dog then they are not cold. If someone sees the dog and the dog does not need the tiger then they need the rabbit. If someone needs the rabbit then the rabbit is not big. If someone sees the mouse then the mouse is cold. If someone needs the tiger then the tiger does not chase the mouse. All big people are red. If someone chases the mouse and the mouse is kind then they see the dog. If someone is cold and they do not chase the rabbit then the rabbit does not need the mouse.
The dog is not rough.
("dog" "is" "rough" "-")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The rabbit does not need the dog.
("rabbit" "needs" "dog" "-")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If someone chases the dog then they are not cold.
((("someone" "chases" "dog" "+")) -> ("someone" "is" "cold" "-"))
If someone sees the dog and the dog does not need the tiger then they need the rabbit.
((("someone" "sees" "dog" "+") ("dog" "needs" "tiger" "~")) -> ("someone" "needs" "rabbit" "+"))
If someone needs the rabbit then the rabbit is not big.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "is" "big" "-"))
If someone sees the mouse then the mouse is cold.
((("someone" "sees" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
If someone needs the tiger then the tiger does not chase the mouse.
((("someone" "needs" "tiger" "+")) -> ("tiger" "chases" "mouse" "-"))
All big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone chases the mouse and the mouse is kind then they see the dog.
((("someone" "chases" "mouse" "+") ("mouse" "is" "kind" "+")) -> ("someone" "sees" "dog" "+"))
If someone is cold and they do not chase the rabbit then the rabbit does not need the mouse.
((("someone" "is" "cold" "+") ("someone" "chases" "rabbit" "~")) -> ("rabbit" "needs" "mouse" "-"))
The mouse needs the dog.
True
1
proof
[(triple4)]
("mouse" "needs" "dog" "+")
triple4
The dog does not see the tiger.
False
1
inv-proof
[(triple2)]
("dog" "sees" "tiger" "-")
triple2
The dog does not need the rabbit.
Unknown
inv-rconc
[@1: The dog needs the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "rabbit" "-")
The dog sees the rabbit.
Unknown
random
[@0: The dog sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "rabbit" "+")
@0: The dog is not rough.[(triple1)] The dog sees the tiger.[(triple2)] The mouse chases the dog.[(triple3)] The mouse needs the dog.[(triple4)] The rabbit does not need the dog.[(triple5)] The rabbit needs the mouse.[(triple6)] The tiger needs the dog.[(triple7)] @1: The mouse is not cold.[(((triple3) -> rule1))]
The dog is not rough.
("dog" "is" "rough" "-")
triple1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple4
The rabbit does not need the dog.
("rabbit" "needs" "dog" "-")
triple5
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple6
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple7
The mouse is not cold.
("mouse" "is" "cold" "-")
((triple3) -> (rule1 % int1))
The mouse is not cold.
("mouse" "is" "cold" "-")
int1