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