The dog is big. The dog is rough. The dog needs the mouse. The dog visits the mouse. The mouse eats the dog. The mouse eats the tiger. The mouse is big. The mouse is kind. The mouse is rough. The mouse is round. The mouse needs the tiger. The mouse visits the tiger. The tiger eats the mouse. The tiger is nice. The tiger needs the dog. The tiger visits the dog. If the mouse visits the tiger then the mouse visits the dog.
The dog is big.
("dog" "is" "big" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If the mouse visits the tiger then the mouse visits the dog.
((("mouse" "visits" "tiger" "+")) -> ("mouse" "visits" "dog" "+"))
The mouse eats the dog.
True
1
proof
[(triple5)]
("mouse" "eats" "dog" "+")
triple5
The mouse does not eat the tiger.
False
1
inv-proof
[(triple6)]
("mouse" "eats" "tiger" "-")
triple6
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The dog is big.[(triple1)] The dog is rough.[(triple2)] The dog needs the mouse.[(triple3)] The dog visits the mouse.[(triple4)] The mouse eats the dog.[(triple5)] The mouse eats the tiger.[(triple6)] The mouse is big.[(triple7)] The mouse is kind.[(triple8)] The mouse is rough.[(triple9)] The mouse is round.[(triple10)] The mouse needs the tiger.[(triple11)] The mouse visits the tiger.[(triple12)] The tiger eats the mouse.[(triple13)] The tiger is nice.[(triple14)] The tiger needs the dog.[(triple15)] The tiger visits the dog.[(triple16)] @1: The mouse visits the dog.[(((triple12) -> rule1))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple3
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple4
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple5
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple6
The mouse is big.
("mouse" "is" "big" "+")
triple7
The mouse is kind.
("mouse" "is" "kind" "+")
triple8
The mouse is rough.
("mouse" "is" "rough" "+")
triple9
The mouse is round.
("mouse" "is" "round" "+")
triple10
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple11
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple12
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple13
The tiger is nice.
("tiger" "is" "nice" "+")
triple14
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple15
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple16
The mouse visits the dog.
("mouse" "visits" "dog" "+")
((triple12) -> (rule1 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1