The dog eats the mouse. The dog is not big. The dog is blue. The dog is kind. The dog is nice. The dog is rough. The dog does not need the mouse. The dog sees the mouse. The mouse eats the dog. The mouse is big. The mouse is kind. The mouse is nice. The mouse is not rough. The mouse needs the dog. The mouse sees the dog. If something is big and it does not need the dog then it does not see the mouse. If something is rough then it does not see the dog. If something sees the dog then the dog eats the mouse.
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is not big.
("dog" "is" "big" "-")
The dog is blue.
("dog" "is" "blue" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog does not need the mouse.
("dog" "needs" "mouse" "-")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If something is big and it does not need the dog then it does not see the mouse.
((("something" "is" "big" "+") ("something" "needs" "dog" "~")) -> ("something" "sees" "mouse" "-"))
If something is rough then it does not see the dog.
((("something" "is" "rough" "+")) -> ("something" "sees" "dog" "-"))
If something sees the dog then the dog eats the mouse.
((("something" "sees" "dog" "+")) -> ("dog" "eats" "mouse" "+"))
The dog eats the mouse.
True
1
proof
[(triple1 OR ((triple15) -> rule3))]
("dog" "eats" "mouse" "+")
triple1
((triple15) -> (rule3 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog needs the mouse.
False
1
inv-proof
[(triple7)]
("dog" "needs" "mouse" "+")
triple7
The dog does not see the dog.
True
2
proof
[(((triple6) -> rule2))]
("dog" "sees" "dog" "-")
((triple6) -> (rule2 % int1))
The dog does not see the dog.
("dog" "sees" "dog" "-")
int1
The dog sees the dog.
False
2
inv-proof
[(((triple6) -> rule2))]
("dog" "sees" "dog" "+")
((triple6) -> (rule2 % int1))
The dog does not see the dog.
("dog" "sees" "dog" "-")
int1
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
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 does not need the mouse.[(triple7)] The dog eats the mouse.[(triple1 OR ((triple15) -> rule3))] The dog is blue.[(triple3)] The dog is kind.[(triple4)] The dog is nice.[(triple5)] The dog is not big.[(triple2)] The dog is rough.[(triple6)] The dog sees the mouse.[(triple8)] The mouse eats the dog.[(triple9)] The mouse is big.[(triple10)] The mouse is kind.[(triple11)] The mouse is nice.[(triple12)] The mouse is not rough.[(triple13)] The mouse needs the dog.[(triple14)] The mouse sees the dog.[(triple15)] @1: The dog does not see the dog.[(((triple6) -> rule2))]
The dog does not need the mouse.
("dog" "needs" "mouse" "-")
triple7
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple1
((triple15) -> (rule3 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
The dog is nice.
("dog" "is" "nice" "+")
triple5
The dog is not big.
("dog" "is" "big" "-")
triple2
The dog is rough.
("dog" "is" "rough" "+")
triple6
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple8
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple9
The mouse is big.
("mouse" "is" "big" "+")
triple10
The mouse is kind.
("mouse" "is" "kind" "+")
triple11
The mouse is nice.
("mouse" "is" "nice" "+")
triple12
The mouse is not rough.
("mouse" "is" "rough" "-")
triple13
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple14
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple15
The dog does not see the dog.
("dog" "sees" "dog" "-")
((triple6) -> (rule2 % int1))
The dog does not see the dog.
("dog" "sees" "dog" "-")
int1