The bear is nice. The bear is round. The bear is young. The bear likes the mouse. The bear likes the tiger. The bear sees the mouse. The bear sees the tiger. The bear visits the tiger. The mouse sees the bear. The mouse visits the bear. The mouse visits the tiger. The tiger is nice. The tiger likes the bear. The tiger likes the mouse. The tiger visits the mouse. If someone visits the mouse then the mouse is red. If someone visits the bear then they are nice. If someone likes the mouse then they see the mouse. If someone sees the mouse and the mouse sees the tiger then the mouse is nice. If someone is nice and they visit the tiger then the tiger visits the mouse. If someone visits the bear then they see the bear.
The bear is nice.
("bear" "is" "nice" "+")
The bear is round.
("bear" "is" "round" "+")
The bear is young.
("bear" "is" "young" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone visits the mouse then the mouse is red.
((("someone" "visits" "mouse" "+")) -> ("mouse" "is" "red" "+"))
If someone visits the bear then they are nice.
((("someone" "visits" "bear" "+")) -> ("someone" "is" "nice" "+"))
If someone likes the mouse then they see the mouse.
((("someone" "likes" "mouse" "+")) -> ("someone" "sees" "mouse" "+"))
If someone sees the mouse and the mouse sees the tiger then the mouse is nice.
((("someone" "sees" "mouse" "+") ("mouse" "sees" "tiger" "+")) -> ("mouse" "is" "nice" "+"))
If someone is nice and they visit the tiger then the tiger visits the mouse.
((("someone" "is" "nice" "+") ("someone" "visits" "tiger" "+")) -> ("tiger" "visits" "mouse" "+"))
If someone visits the bear then they see the bear.
((("someone" "visits" "bear" "+")) -> ("someone" "sees" "bear" "+"))
The mouse visits the bear.
True
1
proof
[(triple10)]
("mouse" "visits" "bear" "+")
triple10
The mouse does not visit the bear.
False
1
inv-proof
[(triple10)]
("mouse" "visits" "bear" "-")
triple10
The mouse is red.
True
2
proof
[(((triple15) -> rule1) OR ((((triple1 triple8) -> rule5)) -> rule1) OR ((((((triple10) -> rule2) triple11) -> rule5)) -> rule1))]
("mouse" "is" "red" "+")
((triple15) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
((((triple1 triple8) -> (rule5 % int2))) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
((((((triple10) -> (rule2 % int3)) triple11) -> (rule5 % int2))) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The tiger does not see the mouse.
False
2
inv-proof
[(((triple14) -> rule3))]
("tiger" "sees" "mouse" "-")
((triple14) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The tiger sees the bear.
Unknown
rconc
[@1: The tiger sees the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "sees" "bear" "+")
The bear does not visit the mouse.
Unknown
inv-random
[@0: The bear visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "mouse" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
@0: The bear is nice.[(triple1)] The bear is round.[(triple2)] The bear is young.[(triple3)] The bear likes the mouse.[(triple4)] The bear likes the tiger.[(triple5)] The bear sees the mouse.[(triple6 OR ((triple4) -> rule3))] The bear sees the tiger.[(triple7)] The bear visits the tiger.[(triple8)] The mouse sees the bear.[(triple9 OR ((triple10) -> rule6))] The mouse visits the bear.[(triple10)] The mouse visits the tiger.[(triple11)] The tiger is nice.[(triple12)] The tiger likes the bear.[(triple13)] The tiger likes the mouse.[(triple14)] The tiger visits the mouse.[(triple15 OR ((triple1 triple8) -> rule5) OR ((((triple10) -> rule2) triple11) -> rule5))] @1: The mouse is nice.[(((triple10) -> rule2))] The mouse is red.[(((triple15) -> rule1) OR ((((triple1 triple8) -> rule5)) -> rule1) OR ((((((triple10) -> rule2) triple11) -> rule5)) -> rule1))] The tiger sees the mouse.[(((triple14) -> rule3))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The bear is round.
("bear" "is" "round" "+")
triple2
The bear is young.
("bear" "is" "young" "+")
triple3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple4
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple5
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple6
((triple4) -> (rule3 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple7
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple8
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple9
((triple10) -> (rule6 % int1))
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple10
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple11
The tiger is nice.
("tiger" "is" "nice" "+")
triple12
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple13
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple14
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple15
((triple1 triple8) -> (rule5 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
((((triple10) -> (rule2 % int2)) triple11) -> (rule5 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
((triple10) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
((triple15) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
((((triple1 triple8) -> (rule5 % int2))) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
((((((triple10) -> (rule2 % int3)) triple11) -> (rule5 % int2))) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
((triple14) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1