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