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