The bear is not nice. The bear needs the mouse. The bear does not need the tiger. The dog is young. The dog does not like the bear. The dog needs the mouse. The dog does not visit the bear. The dog visits the tiger. The mouse is big. The mouse likes the dog. The mouse likes the tiger. The mouse needs the bear. The mouse visits the dog. The tiger is nice. The tiger likes the mouse. The tiger visits the bear. If something is big and not blue then it visits the bear. If something visits the tiger then the tiger is not big. If the mouse likes the tiger and the tiger is not cold then the tiger needs the mouse. If something likes the tiger and the tiger visits the mouse then the tiger does not like the dog. If something likes the tiger then it visits the tiger. If something is blue and not big then it needs the mouse.
The bear is not nice.
("bear" "is" "nice" "-")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear does not need the tiger.
("bear" "needs" "tiger" "-")
The dog is young.
("dog" "is" "young" "+")
The dog does not like the bear.
("dog" "likes" "bear" "-")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog does not visit the bear.
("dog" "visits" "bear" "-")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If something is big and not blue then it visits the bear.
((("something" "is" "big" "+") ("something" "is" "blue" "~")) -> ("something" "visits" "bear" "+"))
If something visits the tiger then the tiger is not big.
((("something" "visits" "tiger" "+")) -> ("tiger" "is" "big" "-"))
If the mouse likes the tiger and the tiger is not cold then the tiger needs the mouse.
((("mouse" "likes" "tiger" "+") ("tiger" "is" "cold" "~")) -> ("tiger" "needs" "mouse" "+"))
If something likes the tiger and the tiger visits the mouse then the tiger does not like the dog.
((("something" "likes" "tiger" "+") ("tiger" "visits" "mouse" "+")) -> ("tiger" "likes" "dog" "-"))
If something likes the tiger then it visits the tiger.
((("something" "likes" "tiger" "+")) -> ("something" "visits" "tiger" "+"))
If something is blue and not big then it needs the mouse.
((("something" "is" "blue" "+") ("something" "is" "big" "~")) -> ("something" "needs" "mouse" "+"))
The dog does not visit the bear.
True
1
proof
[(triple7)]
("dog" "visits" "bear" "-")
triple7
The bear does not need the mouse.
False
1
inv-proof
[(triple2)]
("bear" "needs" "mouse" "-")
triple2
The mouse does not visit the bear.
Unknown
inv-rconc
[@1: The mouse visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "bear" "-")
The bear visits the dog.
Unknown
random
[@0: The bear visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "dog" "+")
@0: The bear does not need the tiger.[(triple3)] The bear is not nice.[(triple1)] The bear needs the mouse.[(triple2)] The dog does not like the bear.[(triple5)] The dog does not visit the bear.[(triple7)] The dog is young.[(triple4)] The dog needs the mouse.[(triple6)] The dog visits the tiger.[(triple8)] The mouse is big.[(triple9)] The mouse likes the dog.[(triple10)] The mouse likes the tiger.[(triple11)] The mouse needs the bear.[(triple12)] The mouse visits the dog.[(triple13)] The tiger is nice.[(triple14)] The tiger likes the mouse.[(triple15)] The tiger visits the bear.[(triple16)] @1: The mouse visits the tiger.[(((triple11) -> rule5))] The tiger is not big.[(((triple8) -> rule2) OR ((((triple11) -> rule5)) -> rule2))]
The bear does not need the tiger.
("bear" "needs" "tiger" "-")
triple3
The bear is not nice.
("bear" "is" "nice" "-")
triple1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple2
The dog does not like the bear.
("dog" "likes" "bear" "-")
triple5
The dog does not visit the bear.
("dog" "visits" "bear" "-")
triple7
The dog is young.
("dog" "is" "young" "+")
triple4
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple6
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple8
The mouse is big.
("mouse" "is" "big" "+")
triple9
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple10
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple11
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple12
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple13
The tiger is nice.
("tiger" "is" "nice" "+")
triple14
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple15
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple16
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
((triple11) -> (rule5 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The tiger is not big.
("tiger" "is" "big" "-")
((triple8) -> (rule2 % int1))
The tiger is not big.
("tiger" "is" "big" "-")
int1
((((triple11) -> (rule5 % int2))) -> (rule2 % int1))
The tiger is not big.
("tiger" "is" "big" "-")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2