The bear chases the mouse. The bear chases the tiger. The bear is blue. The bear is green. The bear does not need the mouse. The bear needs the tiger. The bear visits the tiger. The mouse chases the bear. The mouse is not round. The mouse needs the bear. The tiger is blue. The tiger is rough. The tiger needs the bear. The tiger needs the mouse. The tiger visits the bear. The tiger visits the mouse. If someone chases the bear then they chase the mouse. If someone chases the mouse and the mouse is not round then they do not need the mouse.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is green.
("bear" "is" "green" "+")
The bear does not need the mouse.
("bear" "needs" "mouse" "-")
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse is not round.
("mouse" "is" "round" "-")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone chases the bear then they chase the mouse.
((("someone" "chases" "bear" "+")) -> ("someone" "chases" "mouse" "+"))
If someone chases the mouse and the mouse is not round then they do not need the mouse.
((("someone" "chases" "mouse" "+") ("mouse" "is" "round" "~")) -> ("someone" "needs" "mouse" "-"))
The mouse chases the bear.
True
1
proof
[(triple8)]
("mouse" "chases" "bear" "+")
triple8
The tiger does not need the mouse.
False
1
inv-proof
[(triple14)]
("tiger" "needs" "mouse" "-")
triple14
The mouse chases the mouse.
True
2
proof
[(((triple8) -> rule1))]
("mouse" "chases" "mouse" "+")
((triple8) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse does not chase the mouse.
False
2
inv-proof
[(((triple8) -> rule1))]
("mouse" "chases" "mouse" "-")
((triple8) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse does not need the mouse.
True
4
proof
[(((((triple8) -> rule1) triple9) -> rule2))]
("mouse" "needs" "mouse" "-")
((((triple8) -> (rule1 % int2)) triple9) -> (rule2 % int1))
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse needs the mouse.
False
4
inv-proof
[(((((triple8) -> rule1) triple9) -> rule2))]
("mouse" "needs" "mouse" "+")
((((triple8) -> (rule1 % int2)) triple9) -> (rule2 % int1))
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The tiger does not chase the mouse.
Unknown
inv-rconc
[@1: The tiger chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "mouse" "-")
The mouse visits the bear.
Unknown
random
[@0: The mouse visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bear" "+")
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 chases the tiger.
Unknown
random
[@0: The mouse chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "tiger" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
@0: The bear chases the mouse.[(triple1)] The bear chases the tiger.[(triple2)] The bear does not need the mouse.[(triple5 OR ((triple1 triple9) -> rule2))] The bear is blue.[(triple3)] The bear is green.[(triple4)] The bear needs the tiger.[(triple6)] The bear visits the tiger.[(triple7)] The mouse chases the bear.[(triple8)] The mouse is not round.[(triple9)] The mouse needs the bear.[(triple10)] The tiger is blue.[(triple11)] The tiger is rough.[(triple12)] The tiger needs the bear.[(triple13)] The tiger needs the mouse.[(triple14)] The tiger visits the bear.[(triple15)] The tiger visits the mouse.[(triple16)] @1: The mouse chases the mouse.[(((triple8) -> rule1))] @2: The mouse does not need the mouse.[(((((triple8) -> rule1) triple9) -> rule2))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple2
The bear does not need the mouse.
("bear" "needs" "mouse" "-")
triple5
((triple1 triple9) -> (rule2 % int1))
The bear does not need the mouse.
("bear" "needs" "mouse" "-")
int1
The bear is blue.
("bear" "is" "blue" "+")
triple3
The bear is green.
("bear" "is" "green" "+")
triple4
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple6
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple7
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple8
The mouse is not round.
("mouse" "is" "round" "-")
triple9
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple10
The tiger is blue.
("tiger" "is" "blue" "+")
triple11
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple13
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple14
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple15
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple16
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple8) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
((((triple8) -> (rule1 % int2)) triple9) -> (rule2 % int1))
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2