The bear is green. The mouse needs the tiger. The squirrel is big. The tiger is blue. If something sees the tiger then the tiger is big. If something is green then it needs the mouse. If something is green and big then it chases the mouse. If something needs the bear then the bear sees the mouse. If something needs the squirrel and it chases the tiger then the squirrel sees the mouse. If something needs the mouse and it is green then the mouse sees the tiger.
The bear is green.
("bear" "is" "green" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If something sees the tiger then the tiger is big.
((("something" "sees" "tiger" "+")) -> ("tiger" "is" "big" "+"))
If something is green then it needs the mouse.
((("something" "is" "green" "+")) -> ("something" "needs" "mouse" "+"))
If something is green and big then it chases the mouse.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "chases" "mouse" "+"))
If something needs the bear then the bear sees the mouse.
((("something" "needs" "bear" "+")) -> ("bear" "sees" "mouse" "+"))
If something needs the squirrel and it chases the tiger then the squirrel sees the mouse.
((("something" "needs" "squirrel" "+") ("something" "chases" "tiger" "+")) -> ("squirrel" "sees" "mouse" "+"))
If something needs the mouse and it is green then the mouse sees the tiger.
((("something" "needs" "mouse" "+") ("something" "is" "green" "+")) -> ("mouse" "sees" "tiger" "+"))
The tiger is blue.
True
1
proof
[(triple4)]
("tiger" "is" "blue" "+")
triple4
The tiger is not blue.
False
1
inv-proof
[(triple4)]
("tiger" "is" "blue" "-")
triple4
The bear needs the mouse.
True
2
proof
[(((triple1) -> rule2))]
("bear" "needs" "mouse" "+")
((triple1) -> (rule2 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear does not need the mouse.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "needs" "mouse" "-")
((triple1) -> (rule2 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The mouse sees the tiger.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule6))]
("mouse" "sees" "tiger" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
The mouse does not see the tiger.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule6))]
("mouse" "sees" "tiger" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
The tiger is big.
True
5
proof
[(((((((triple1) -> rule2) triple1) -> rule6)) -> rule1))]
("tiger" "is" "big" "+")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule6 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int3
The tiger is not big.
False
5
inv-proof
[(((((((triple1) -> rule2) triple1) -> rule6)) -> rule1))]
("tiger" "is" "big" "-")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule6 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int3
The tiger does not chase the mouse.
Unknown
inv-rconc
[@1: The tiger chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "chases" "mouse" "-")
The squirrel sees the mouse.
Unknown
rconc
[@1: The squirrel sees the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "sees" "mouse" "+")
The bear does not chase the mouse.
Unknown
inv-rconc
[@1: The bear chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "chases" "mouse" "-")
The squirrel needs the mouse.
Unknown
rconc
[@1: The squirrel needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "needs" "mouse" "+")
The bear does not see the squirrel.
Unknown
inv-random
[@0: The bear sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "squirrel" "-")
The bear needs the squirrel.
Unknown
random
[@0: The bear needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "squirrel" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The squirrel sees the bear.
Unknown
random
[@0: The squirrel sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "bear" "+")
@0: The bear is green.[(triple1)] The mouse needs the tiger.[(triple2)] The squirrel is big.[(triple3)] The tiger is blue.[(triple4)] @1: The bear needs the mouse.[(((triple1) -> rule2))] @2: The mouse sees the tiger.[(((((triple1) -> rule2) triple1) -> rule6))] @3: The tiger is big.[(((((((triple1) -> rule2) triple1) -> rule6)) -> rule1))]
The bear is green.
("bear" "is" "green" "+")
triple1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple2
The squirrel is big.
("squirrel" "is" "big" "+")
triple3
The tiger is blue.
("tiger" "is" "blue" "+")
triple4
The bear needs the mouse.
("bear" "needs" "mouse" "+")
((triple1) -> (rule2 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule6 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int3