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