The dog chases the mouse. The dog eats the mouse. The dog is blue. The dog is nice. The dog is red. The dog is rough. The dog is round. The dog needs the mouse. The mouse chases the dog. The mouse eats the dog. The mouse is blue. The mouse is nice. The mouse is red. The mouse is rough. The mouse is round. The mouse needs the dog. If the mouse is round and the mouse needs the dog then the dog eats the mouse. If someone eats the dog and the dog is rough then the dog eats the mouse. If someone eats the mouse then the mouse chases the dog. If someone chases the dog and the dog eats the mouse then the mouse chases the dog. If someone is red and they chase the mouse then the mouse chases the dog. If someone is nice then they need the mouse.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
If the mouse is round and the mouse needs the dog then the dog eats the mouse.
((("mouse" "is" "round" "+") ("mouse" "needs" "dog" "+")) -> ("dog" "eats" "mouse" "+"))
If someone eats the dog and the dog is rough then the dog eats the mouse.
((("someone" "eats" "dog" "+") ("dog" "is" "rough" "+")) -> ("dog" "eats" "mouse" "+"))
If someone eats the mouse then the mouse chases the dog.
((("someone" "eats" "mouse" "+")) -> ("mouse" "chases" "dog" "+"))
If someone chases the dog and the dog eats the mouse then the mouse chases the dog.
((("someone" "chases" "dog" "+") ("dog" "eats" "mouse" "+")) -> ("mouse" "chases" "dog" "+"))
If someone is red and they chase the mouse then the mouse chases the dog.
((("someone" "is" "red" "+") ("someone" "chases" "mouse" "+")) -> ("mouse" "chases" "dog" "+"))
If someone is nice then they need the mouse.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "mouse" "+"))
The mouse needs the dog.
True
1
proof
[(triple16)]
("mouse" "needs" "dog" "+")
triple16
The mouse is not rough.
False
1
inv-proof
[(triple14)]
("mouse" "is" "rough" "-")
triple14
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The dog chases the mouse.[(triple1)] The dog eats the mouse.[(triple2 OR ((triple10 triple6) -> rule2) OR ((triple15 triple16) -> rule1))] The dog is blue.[(triple3)] The dog is nice.[(triple4)] The dog is red.[(triple5)] The dog is rough.[(triple6)] The dog is round.[(triple7)] The dog needs the mouse.[(triple8 OR ((triple4) -> rule6))] The mouse chases the dog.[(triple9 OR ((triple2) -> rule3) OR ((triple5 triple1) -> rule5) OR ((((triple10 triple6) -> rule2)) -> rule3) OR ((((triple15 triple16) -> rule1)) -> rule3))] The mouse eats the dog.[(triple10)] The mouse is blue.[(triple11)] The mouse is nice.[(triple12)] The mouse is red.[(triple13)] The mouse is rough.[(triple14)] The mouse is round.[(triple15)] The mouse needs the dog.[(triple16)] @1: The mouse needs the mouse.[(((triple12) -> rule6))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple2
((triple10 triple6) -> (rule2 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
((triple15 triple16) -> (rule1 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
triple3
The dog is nice.
("dog" "is" "nice" "+")
triple4
The dog is red.
("dog" "is" "red" "+")
triple5
The dog is rough.
("dog" "is" "rough" "+")
triple6
The dog is round.
("dog" "is" "round" "+")
triple7
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple8
((triple4) -> (rule6 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple9
((triple2) -> (rule3 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
((triple5 triple1) -> (rule5 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
((((triple10 triple6) -> (rule2 % int2))) -> (rule3 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
((((triple15 triple16) -> (rule1 % int2))) -> (rule3 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple10
The mouse is blue.
("mouse" "is" "blue" "+")
triple11
The mouse is nice.
("mouse" "is" "nice" "+")
triple12
The mouse is red.
("mouse" "is" "red" "+")
triple13
The mouse is rough.
("mouse" "is" "rough" "+")
triple14
The mouse is round.
("mouse" "is" "round" "+")
triple15
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple16
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple12) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1