The bear is big. The bear is cold. The bear is rough. The bear is round. The bear is young. The bear likes the mouse. The bear sees the mouse. The bear visits the mouse. The mouse is big. The mouse is cold. The mouse is rough. The mouse is young. The mouse likes the bear. The mouse sees the bear. The mouse visits the bear. If someone is big and young then they visit the bear. Cold people are round. If someone likes the mouse then the mouse likes the bear. If the mouse sees the bear and the bear visits the mouse then the mouse visits the bear. If someone visits the bear then they are round. If someone sees the mouse then the mouse likes the bear. If someone is rough and round then they like the bear. If someone visits the bear and the bear visits the mouse then the bear likes the mouse.
The bear is big.
("bear" "is" "big" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear is round.
("bear" "is" "round" "+")
The bear is young.
("bear" "is" "young" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If someone is big and young then they visit the bear.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "visits" "bear" "+"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone likes the mouse then the mouse likes the bear.
((("someone" "likes" "mouse" "+")) -> ("mouse" "likes" "bear" "+"))
If the mouse sees the bear and the bear visits the mouse then the mouse visits the bear.
((("mouse" "sees" "bear" "+") ("bear" "visits" "mouse" "+")) -> ("mouse" "visits" "bear" "+"))
If someone visits the bear then they are round.
((("someone" "visits" "bear" "+")) -> ("someone" "is" "round" "+"))
If someone sees the mouse then the mouse likes the bear.
((("someone" "sees" "mouse" "+")) -> ("mouse" "likes" "bear" "+"))
If someone is rough and round then they like the bear.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "likes" "bear" "+"))
If someone visits the bear and the bear visits the mouse then the bear likes the mouse.
((("someone" "visits" "bear" "+") ("bear" "visits" "mouse" "+")) -> ("bear" "likes" "mouse" "+"))
The mouse is rough.
True
1
proof
[(triple11)]
("mouse" "is" "rough" "+")
triple11
The mouse is not rough.
False
1
inv-proof
[(triple11)]
("mouse" "is" "rough" "-")
triple11
The bear likes the bear.
True
3
proof
[(((triple3 triple4) -> rule7) OR ((triple3 ((triple2) -> rule2)) -> rule7) OR ((triple3 ((((triple1 triple5) -> rule1)) -> rule5)) -> rule7))]
("bear" "likes" "bear" "+")
((triple3 triple4) -> (rule7 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
((triple3 ((triple2) -> (rule2 % int2))) -> (rule7 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
((triple3 ((((triple1 triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3
The mouse is not round.
False
2
inv-proof
[(((triple10) -> rule2) OR ((triple15) -> rule5) OR ((((triple14 triple8) -> rule4)) -> rule5) OR ((((triple9 triple12) -> rule1)) -> rule5))]
("mouse" "is" "round" "-")
((triple10) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((triple15) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((((triple14 triple8) -> (rule4 % int2))) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
((((triple9 triple12) -> (rule1 % int2))) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
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 likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The bear is big.[(triple1)] The bear is cold.[(triple2)] The bear is rough.[(triple3)] The bear is round.[(triple4 OR ((triple2) -> rule2) OR ((((triple1 triple5) -> rule1)) -> rule5))] The bear is young.[(triple5)] The bear likes the mouse.[(triple6 OR ((triple15 triple8) -> rule8) OR ((((triple1 triple5) -> rule1) triple8) -> rule8) OR ((((triple14 triple8) -> rule4) triple8) -> rule8) OR ((((triple9 triple12) -> rule1) triple8) -> rule8))] The bear sees the mouse.[(triple7)] The bear visits the mouse.[(triple8)] The mouse is big.[(triple9)] The mouse is cold.[(triple10)] The mouse is rough.[(triple11)] The mouse is young.[(triple12)] The mouse likes the bear.[(triple13 OR ((triple6) -> rule3) OR ((triple7) -> rule6) OR ((((triple15 triple8) -> rule8)) -> rule3) OR ((triple11 ((triple10) -> rule2)) -> rule7) OR ((triple11 ((triple15) -> rule5)) -> rule7) OR ((((((triple1 triple5) -> rule1) triple8) -> rule8)) -> rule3) OR ((((((triple14 triple8) -> rule4) triple8) -> rule8)) -> rule3) OR ((((((triple9 triple12) -> rule1) triple8) -> rule8)) -> rule3) OR ((triple11 ((((triple14 triple8) -> rule4)) -> rule5)) -> rule7) OR ((triple11 ((((triple9 triple12) -> rule1)) -> rule5)) -> rule7))] The mouse sees the bear.[(triple14)] The mouse visits the bear.[(triple15 OR ((triple14 triple8) -> rule4) OR ((triple9 triple12) -> rule1))] @1: The bear likes the bear.[(((triple3 triple4) -> rule7) OR ((triple3 ((triple2) -> rule2)) -> rule7) OR ((triple3 ((((triple1 triple5) -> rule1)) -> rule5)) -> rule7))] The bear visits the bear.[(((triple1 triple5) -> rule1))] The mouse is round.[(((triple10) -> rule2) OR ((triple15) -> rule5) OR ((((triple14 triple8) -> rule4)) -> rule5) OR ((((triple9 triple12) -> rule1)) -> rule5))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The bear is round.
("bear" "is" "round" "+")
triple4
((triple2) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
((((triple1 triple5) -> (rule1 % int2))) -> (rule5 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear is young.
("bear" "is" "young" "+")
triple5
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple6
((triple15 triple8) -> (rule8 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
((((triple1 triple5) -> (rule1 % int2)) triple8) -> (rule8 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
((((triple14 triple8) -> (rule4 % int2)) triple8) -> (rule8 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
((((triple9 triple12) -> (rule1 % int2)) triple8) -> (rule8 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple7
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple8
The mouse is big.
("mouse" "is" "big" "+")
triple9
The mouse is cold.
("mouse" "is" "cold" "+")
triple10
The mouse is rough.
("mouse" "is" "rough" "+")
triple11
The mouse is young.
("mouse" "is" "young" "+")
triple12
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple13
((triple6) -> (rule3 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
((triple7) -> (rule6 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
((((triple15 triple8) -> (rule8 % int2))) -> (rule3 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
((triple11 ((triple10) -> (rule2 % int2))) -> (rule7 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
((triple11 ((triple15) -> (rule5 % int2))) -> (rule7 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
((((((triple1 triple5) -> (rule1 % int3)) triple8) -> (rule8 % int2))) -> (rule3 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3
((((((triple14 triple8) -> (rule4 % int3)) triple8) -> (rule8 % int2))) -> (rule3 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int3
((((((triple9 triple12) -> (rule1 % int3)) triple8) -> (rule8 % int2))) -> (rule3 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int3
((triple11 ((((triple14 triple8) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int3
((triple11 ((((triple9 triple12) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int3
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple14
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple15
((triple14 triple8) -> (rule4 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
((triple9 triple12) -> (rule1 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
((triple3 triple4) -> (rule7 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
((triple3 ((triple2) -> (rule2 % int2))) -> (rule7 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
((triple3 ((((triple1 triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple1 triple5) -> (rule1 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((triple10) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((triple15) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((((triple14 triple8) -> (rule4 % int2))) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
((((triple9 triple12) -> (rule1 % int2))) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2