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