The bear eats the mouse. The bear is big. The bear is cold. The bear is green. The bear is nice. The bear is rough. The bear sees the mouse. The bear visits the mouse. The mouse eats the bear. The mouse is big. The mouse is cold. The mouse is nice. The mouse is rough. The mouse sees the bear. The mouse visits the bear. If something visits the bear and the bear visits the mouse then it visits the mouse. If something is big and cold then it visits the bear. If something eats the mouse and the mouse visits the bear then the bear sees the mouse. If something sees the bear and it eats the bear then it eats the mouse. If something sees the bear then the bear is rough. If the mouse sees the bear and the mouse visits the bear then the bear is big.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If something visits the bear and the bear visits the mouse then it visits the mouse.
((("something" "visits" "bear" "+") ("bear" "visits" "mouse" "+")) -> ("something" "visits" "mouse" "+"))
If something is big and cold then it visits the bear.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "visits" "bear" "+"))
If something eats the mouse and the mouse visits the bear then the bear sees the mouse.
((("something" "eats" "mouse" "+") ("mouse" "visits" "bear" "+")) -> ("bear" "sees" "mouse" "+"))
If something sees the bear and it eats the bear then it eats the mouse.
((("something" "sees" "bear" "+") ("something" "eats" "bear" "+")) -> ("something" "eats" "mouse" "+"))
If something sees the bear then the bear is rough.
((("something" "sees" "bear" "+")) -> ("bear" "is" "rough" "+"))
If the mouse sees the bear and the mouse visits the bear then the bear is big.
((("mouse" "sees" "bear" "+") ("mouse" "visits" "bear" "+")) -> ("bear" "is" "big" "+"))
The mouse visits the bear.
True
1
proof
[(triple15 OR ((triple10 triple11) -> rule2))]
("mouse" "visits" "bear" "+")
triple15
((triple10 triple11) -> (rule2 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The bear does not visit the mouse.
False
1
inv-proof
[(triple8)]
("bear" "visits" "mouse" "-")
triple8
The bear visits the bear.
True
3
proof
[(((triple2 triple3) -> rule2) OR ((((triple14 triple15) -> rule6) triple3) -> rule2) OR ((((triple14 ((triple10 triple11) -> rule2)) -> rule6) triple3) -> rule2))]
("bear" "visits" "bear" "+")
((triple2 triple3) -> (rule2 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
((((triple14 triple15) -> (rule6 % int2)) triple3) -> (rule2 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
((((triple14 ((triple10 triple11) -> (rule2 % int3))) -> (rule6 % int2)) triple3) -> (rule2 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int3
The mouse does not eat the mouse.
False
3
inv-proof
[(((triple14 triple9) -> rule4))]
("mouse" "eats" "mouse" "-")
((triple14 triple9) -> (rule4 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
@0: The bear eats the mouse.[(triple1)] The bear is big.[(triple2 OR ((triple14 triple15) -> rule6) OR ((triple14 ((triple10 triple11) -> rule2)) -> rule6))] The bear is cold.[(triple3)] The bear is green.[(triple4)] The bear is nice.[(triple5)] The bear is rough.[(triple6 OR ((triple14) -> rule5))] The bear sees the mouse.[(triple7 OR ((triple1 triple15) -> rule3) OR ((triple1 ((triple10 triple11) -> rule2)) -> rule3) OR ((((triple14 triple9) -> rule4) triple15) -> rule3) OR ((((triple14 triple9) -> rule4) ((triple10 triple11) -> rule2)) -> rule3))] The bear visits the mouse.[(triple8)] The mouse eats the bear.[(triple9)] The mouse is big.[(triple10)] The mouse is cold.[(triple11)] The mouse is nice.[(triple12)] The mouse is rough.[(triple13)] The mouse sees the bear.[(triple14)] The mouse visits the bear.[(triple15 OR ((triple10 triple11) -> rule2))] @1: The bear visits the bear.[(((triple2 triple3) -> rule2) OR ((((triple14 triple15) -> rule6) triple3) -> rule2) OR ((((triple14 ((triple10 triple11) -> rule2)) -> rule6) triple3) -> rule2))] The mouse eats the mouse.[(((triple14 triple9) -> rule4))] The mouse visits the mouse.[(((triple15 triple8) -> rule1) OR ((((triple10 triple11) -> rule2) triple8) -> rule1))]
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
((triple14 triple15) -> (rule6 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
((triple14 ((triple10 triple11) -> (rule2 % int2))) -> (rule6 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
triple3
The bear is green.
("bear" "is" "green" "+")
triple4
The bear is nice.
("bear" "is" "nice" "+")
triple5
The bear is rough.
("bear" "is" "rough" "+")
triple6
((triple14) -> (rule5 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple7
((triple1 triple15) -> (rule3 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
((triple1 ((triple10 triple11) -> (rule2 % int2))) -> (rule3 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
((((triple14 triple9) -> (rule4 % int2)) triple15) -> (rule3 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
((((triple14 triple9) -> (rule4 % int3)) ((triple10 triple11) -> (rule2 % int2))) -> (rule3 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int3
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple8
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple9
The mouse is big.
("mouse" "is" "big" "+")
triple10
The mouse is cold.
("mouse" "is" "cold" "+")
triple11
The mouse is nice.
("mouse" "is" "nice" "+")
triple12
The mouse is rough.
("mouse" "is" "rough" "+")
triple13
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple14
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple15
((triple10 triple11) -> (rule2 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple2 triple3) -> (rule2 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
((((triple14 triple15) -> (rule6 % int2)) triple3) -> (rule2 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
((((triple14 ((triple10 triple11) -> (rule2 % int3))) -> (rule6 % int2)) triple3) -> (rule2 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int3
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple14 triple9) -> (rule4 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple15 triple8) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
((((triple10 triple11) -> (rule2 % int2)) triple8) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2