The bear chases the squirrel. The bear sees the squirrel. The lion is blue. The mouse likes the bear. The mouse sees the lion. The squirrel chases the bear. The squirrel is big. If something chases the mouse then the mouse is rough. If something likes the mouse then the mouse is rough. If something sees the squirrel then it likes the mouse. If something chases the squirrel and it chases the mouse then it likes the mouse. If something is big then it sees the squirrel. If something is red then it sees the bear. Cold things are blue. If something likes the mouse and it chases the bear then the mouse likes the lion.
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The lion is blue.
("lion" "is" "blue" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
If something chases the mouse then the mouse is rough.
((("something" "chases" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If something likes the mouse then the mouse is rough.
((("something" "likes" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If something sees the squirrel then it likes the mouse.
((("something" "sees" "squirrel" "+")) -> ("something" "likes" "mouse" "+"))
If something chases the squirrel and it chases the mouse then it likes the mouse.
((("something" "chases" "squirrel" "+") ("something" "chases" "mouse" "+")) -> ("something" "likes" "mouse" "+"))
If something is big then it sees the squirrel.
((("something" "is" "big" "+")) -> ("something" "sees" "squirrel" "+"))
If something is red then it sees the bear.
((("something" "is" "red" "+")) -> ("something" "sees" "bear" "+"))
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something likes the mouse and it chases the bear then the mouse likes the lion.
((("something" "likes" "mouse" "+") ("something" "chases" "bear" "+")) -> ("mouse" "likes" "lion" "+"))
The bear sees the squirrel.
True
1
proof
[(triple2)]
("bear" "sees" "squirrel" "+")
triple2
The bear does not chase the squirrel.
False
1
inv-proof
[(triple1)]
("bear" "chases" "squirrel" "-")
triple1
The squirrel sees the squirrel.
True
2
proof
[(((triple7) -> rule5))]
("squirrel" "sees" "squirrel" "+")
((triple7) -> (rule5 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The bear does not like the mouse.
False
2
inv-proof
[(((triple2) -> rule3))]
("bear" "likes" "mouse" "-")
((triple2) -> (rule3 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The squirrel likes the mouse.
True
3
proof
[(((((triple7) -> rule5)) -> rule3))]
("squirrel" "likes" "mouse" "+")
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel does not like the mouse.
False
3
inv-proof
[(((((triple7) -> rule5)) -> rule3))]
("squirrel" "likes" "mouse" "-")
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The mouse likes the lion.
True
5
proof
[(((((((triple7) -> rule5)) -> rule3) triple6) -> rule8))]
("mouse" "likes" "lion" "+")
((((((triple7) -> (rule5 % int3))) -> (rule3 % int2)) triple6) -> (rule8 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int3
The mouse does not like the lion.
False
5
inv-proof
[(((((((triple7) -> rule5)) -> rule3) triple6) -> rule8))]
("mouse" "likes" "lion" "-")
((((((triple7) -> (rule5 % int3))) -> (rule3 % int2)) triple6) -> (rule8 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int3
The squirrel does not see the bear.
Unknown
inv-rconc
[@1: The squirrel sees the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "sees" "bear" "-")
The bear sees the bear.
Unknown
rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "sees" "bear" "+")
The lion does not see the bear.
Unknown
inv-rconc
[@1: The lion sees the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "sees" "bear" "-")
The lion sees the squirrel.
Unknown
rconc
[@1: The lion sees the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "sees" "squirrel" "+")
The squirrel does not like the bear.
Unknown
inv-random
[@0: The squirrel likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "bear" "-")
The lion chases the bear.
Unknown
random
[@0: The lion chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "bear" "+")
The squirrel does not see the lion.
Unknown
inv-random
[@0: The squirrel sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "lion" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
@0: The bear chases the squirrel.[(triple1)] The bear sees the squirrel.[(triple2)] The lion is blue.[(triple3)] The mouse likes the bear.[(triple4)] The mouse sees the lion.[(triple5)] The squirrel chases the bear.[(triple6)] The squirrel is big.[(triple7)] @1: The bear likes the mouse.[(((triple2) -> rule3))] The squirrel sees the squirrel.[(((triple7) -> rule5))] @2: The mouse is rough.[(((((triple2) -> rule3)) -> rule2) OR ((((((triple7) -> rule5)) -> rule3)) -> rule2))] The squirrel likes the mouse.[(((((triple7) -> rule5)) -> rule3))] @3: The mouse likes the lion.[(((((((triple7) -> rule5)) -> rule3) triple6) -> rule8))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple2
The lion is blue.
("lion" "is" "blue" "+")
triple3
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple4
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple5
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple6
The squirrel is big.
("squirrel" "is" "big" "+")
triple7
The bear likes the mouse.
("bear" "likes" "mouse" "+")
((triple2) -> (rule3 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple7) -> (rule5 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
((((((triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int3
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The mouse likes the lion.
("mouse" "likes" "lion" "+")
((((((triple7) -> (rule5 % int3))) -> (rule3 % int2)) triple6) -> (rule8 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int3