The bear chases the mouse. The bear sees the lion. The lion sees the squirrel. The mouse is nice. The squirrel chases the bear. The squirrel needs the lion. The squirrel sees the bear. If something is big then it needs the lion. If something sees the mouse then it needs the lion. If something needs the squirrel then the squirrel sees the lion. If something sees the squirrel then the squirrel sees the mouse. If something chases the squirrel and the squirrel sees the lion then the lion chases the squirrel. If something needs the bear then the bear is round. If the bear sees the lion then the lion chases the squirrel. If something sees the lion then it is red. If something is red then it needs the squirrel.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If something is big then it needs the lion.
((("something" "is" "big" "+")) -> ("something" "needs" "lion" "+"))
If something sees the mouse then it needs the lion.
((("something" "sees" "mouse" "+")) -> ("something" "needs" "lion" "+"))
If something needs the squirrel then the squirrel sees the lion.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "sees" "lion" "+"))
If something sees the squirrel then the squirrel sees the mouse.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "sees" "mouse" "+"))
If something chases the squirrel and the squirrel sees the lion then the lion chases the squirrel.
((("something" "chases" "squirrel" "+") ("squirrel" "sees" "lion" "+")) -> ("lion" "chases" "squirrel" "+"))
If something needs the bear then the bear is round.
((("something" "needs" "bear" "+")) -> ("bear" "is" "round" "+"))
If the bear sees the lion then the lion chases the squirrel.
((("bear" "sees" "lion" "+")) -> ("lion" "chases" "squirrel" "+"))
If something sees the lion then it is red.
((("something" "sees" "lion" "+")) -> ("something" "is" "red" "+"))
If something is red then it needs the squirrel.
((("something" "is" "red" "+")) -> ("something" "needs" "squirrel" "+"))
The squirrel sees the bear.
True
1
proof
[(triple7)]
("squirrel" "sees" "bear" "+")
triple7
The squirrel does not chase the bear.
False
1
inv-proof
[(triple5)]
("squirrel" "chases" "bear" "-")
triple5
The lion chases the squirrel.
True
2
proof
[(((triple2) -> rule7))]
("lion" "chases" "squirrel" "+")
((triple2) -> (rule7 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The lion does not chase the squirrel.
False
2
inv-proof
[(((triple2) -> rule7))]
("lion" "chases" "squirrel" "-")
((triple2) -> (rule7 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The bear needs the squirrel.
True
3
proof
[(((((triple2) -> rule8)) -> rule9))]
("bear" "needs" "squirrel" "+")
((((triple2) -> (rule8 % int2))) -> (rule9 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear does not need the squirrel.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule9))]
("bear" "needs" "squirrel" "-")
((((triple2) -> (rule8 % int2))) -> (rule9 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The squirrel sees the lion.
True
4
proof
[(((((((triple2) -> rule8)) -> rule9)) -> rule3))]
("squirrel" "sees" "lion" "+")
((((((triple2) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The squirrel does not see the lion.
False
4
inv-proof
[(((((((triple2) -> rule8)) -> rule9)) -> rule3))]
("squirrel" "sees" "lion" "-")
((((((triple2) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The squirrel is red.
True
5
proof
[(((((((((triple2) -> rule8)) -> rule9)) -> rule3)) -> rule8))]
("squirrel" "is" "red" "+")
((((((((triple2) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
The bear is red.
("bear" "is" "red" "+")
int4
The squirrel is not red.
False
5
inv-proof
[(((((((((triple2) -> rule8)) -> rule9)) -> rule3)) -> rule8))]
("squirrel" "is" "red" "-")
((((((((triple2) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
The bear is red.
("bear" "is" "red" "+")
int4
The squirrel needs the squirrel.
True
6
proof
[(((((((((((triple2) -> rule8)) -> rule9)) -> rule3)) -> rule8)) -> rule9))]
("squirrel" "needs" "squirrel" "+")
((((((((((triple2) -> (rule8 % int5))) -> (rule9 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int4
The bear is red.
("bear" "is" "red" "+")
int5
The squirrel does not need the squirrel.
False
6
inv-proof
[(((((((((((triple2) -> rule8)) -> rule9)) -> rule3)) -> rule8)) -> rule9))]
("squirrel" "needs" "squirrel" "-")
((((((((((triple2) -> (rule8 % int5))) -> (rule9 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int4
The bear is red.
("bear" "is" "red" "+")
int5
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "is" "red" "-")
The lion is red.
Unknown
rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "is" "red" "+")
The mouse does not need the squirrel.
Unknown
inv-rconc
[@2: The mouse needs the squirrel.[CWA. Example of deepest failure = (rule9 <- rule8 <- FAIL)]]
("mouse" "needs" "squirrel" "-")
The lion needs the lion.
Unknown
rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "lion" "+")
The lion does not need the squirrel.
Unknown
inv-rconc
[@2: The lion needs the squirrel.[CWA. Example of deepest failure = (rule9 <- rule8 <- FAIL)]]
("lion" "needs" "squirrel" "-")
The bear is round.
Unknown
rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "round" "+")
The lion does not need the mouse.
Unknown
inv-random
[@0: The lion needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "mouse" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The lion does not chase the bear.
Unknown
inv-random
[@0: The lion chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "bear" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The lion does not see the bear.
Unknown
inv-random
[@0: The lion sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "bear" "-")
The squirrel is nice.
Unknown
random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "+")
@0: The bear chases the mouse.[(triple1)] The bear sees the lion.[(triple2)] The lion sees the squirrel.[(triple3)] The mouse is nice.[(triple4)] The squirrel chases the bear.[(triple5)] The squirrel needs the lion.[(triple6 OR ((((triple3) -> rule4)) -> rule2))] The squirrel sees the bear.[(triple7)] @1: The bear is red.[(((triple2) -> rule8))] The lion chases the squirrel.[(((triple2) -> rule7))] The squirrel sees the mouse.[(((triple3) -> rule4))] @2: The bear needs the squirrel.[(((((triple2) -> rule8)) -> rule9))] @3: The squirrel sees the lion.[(((((((triple2) -> rule8)) -> rule9)) -> rule3))] @4: The squirrel is red.[(((((((((triple2) -> rule8)) -> rule9)) -> rule3)) -> rule8))] @5: The squirrel needs the squirrel.[(((((((((((triple2) -> rule8)) -> rule9)) -> rule3)) -> rule8)) -> rule9))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear sees the lion.
("bear" "sees" "lion" "+")
triple2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple3
The mouse is nice.
("mouse" "is" "nice" "+")
triple4
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple5
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple6
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int2
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple7
The bear is red.
("bear" "is" "red" "+")
((triple2) -> (rule8 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
((triple2) -> (rule7 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
((triple3) -> (rule4 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
((((triple2) -> (rule8 % int2))) -> (rule9 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
((((((triple2) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The squirrel is red.
("squirrel" "is" "red" "+")
((((((((triple2) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
The bear is red.
("bear" "is" "red" "+")
int4
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((((((((((triple2) -> (rule8 % int5))) -> (rule9 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int4
The bear is red.
("bear" "is" "red" "+")
int5