The bear visits the mouse. The lion sees the mouse. The mouse is big. If the mouse visits the lion then the lion visits the mouse. If someone is green and cold then they do not see the bear. If someone is green then they need the bear. If someone needs the bear then the bear needs the lion. If someone visits the lion then they do not need the mouse. If someone is young and cold then they visit the lion. If someone is big then they are green. If someone sees the bear then the bear needs the mouse.
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
If the mouse visits the lion then the lion visits the mouse.
((("mouse" "visits" "lion" "+")) -> ("lion" "visits" "mouse" "+"))
If someone is green and cold then they do not see the bear.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "sees" "bear" "-"))
If someone is green then they need the bear.
((("someone" "is" "green" "+")) -> ("someone" "needs" "bear" "+"))
If someone needs the bear then the bear needs the lion.
((("someone" "needs" "bear" "+")) -> ("bear" "needs" "lion" "+"))
If someone visits the lion then they do not need the mouse.
((("someone" "visits" "lion" "+")) -> ("someone" "needs" "mouse" "-"))
If someone is young and cold then they visit the lion.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "visits" "lion" "+"))
If someone is big then they are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If someone sees the bear then the bear needs the mouse.
((("someone" "sees" "bear" "+")) -> ("bear" "needs" "mouse" "+"))
The lion sees the mouse.
True
1
proof
[(triple2)]
("lion" "sees" "mouse" "+")
triple2
The bear does not visit the mouse.
False
1
inv-proof
[(triple1)]
("bear" "visits" "mouse" "-")
triple1
The mouse is green.
True
2
proof
[(((triple3) -> rule7))]
("mouse" "is" "green" "+")
((triple3) -> (rule7 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is not green.
False
2
inv-proof
[(((triple3) -> rule7))]
("mouse" "is" "green" "-")
((triple3) -> (rule7 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse needs the bear.
True
3
proof
[(((((triple3) -> rule7)) -> rule3))]
("mouse" "needs" "bear" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse does not need the bear.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule3))]
("mouse" "needs" "bear" "-")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The bear needs the lion.
True
4
proof
[(((((((triple3) -> rule7)) -> rule3)) -> rule4))]
("bear" "needs" "lion" "+")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The bear does not need the lion.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule3)) -> rule4))]
("bear" "needs" "lion" "-")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The lion does not need the bear.
Unknown
inv-rconc
[@2: The lion needs the bear.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("lion" "needs" "bear" "-")
The lion is green.
Unknown
rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "is" "green" "+")
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "visits" "lion" "-")
The bear needs the bear.
Unknown
rconc
[@2: The bear needs the bear.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("bear" "needs" "bear" "+")
The bear is not blue.
Unknown
inv-random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
The bear is not young.
Unknown
inv-random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "-")
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 visits the mouse.[(triple1)] The lion sees the mouse.[(triple2)] The mouse is big.[(triple3)] @1: The mouse is green.[(((triple3) -> rule7))] @2: The mouse needs the bear.[(((((triple3) -> rule7)) -> rule3))] @3: The bear needs the lion.[(((((((triple3) -> rule7)) -> rule3)) -> rule4))]
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple2
The mouse is big.
("mouse" "is" "big" "+")
triple3
The mouse is green.
("mouse" "is" "green" "+")
((triple3) -> (rule7 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The bear needs the lion.
("bear" "needs" "lion" "+")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3