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