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