The bear is blue. The bear is rough. The bear is young. The bear needs the lion. The bear needs the squirrel. The bear sees the tiger. The bear visits the tiger. The lion is young. The lion needs the tiger. The lion visits the squirrel. The squirrel is blue. The squirrel sees the lion. The squirrel visits the lion. The tiger needs the lion. If something sees the squirrel then it sees the tiger. If something sees the bear and it sees the tiger then the bear needs the tiger. If the squirrel visits the bear then the bear sees the lion. If the tiger sees the lion and the lion sees the squirrel then the lion sees the bear. If something is young and it visits the lion then it sees the squirrel. If something needs the squirrel then the squirrel sees the bear. If something needs the tiger then it visits the bear. If something is blue then it needs the bear. If something needs the bear and the bear visits the tiger then it sees the squirrel.
The bear is blue.
("bear" "is" "blue" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the lion.
("bear" "needs" "lion" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If something sees the squirrel then it sees the tiger.
((("something" "sees" "squirrel" "+")) -> ("something" "sees" "tiger" "+"))
If something sees the bear and it sees the tiger then the bear needs the tiger.
((("something" "sees" "bear" "+") ("something" "sees" "tiger" "+")) -> ("bear" "needs" "tiger" "+"))
If the squirrel visits the bear then the bear sees the lion.
((("squirrel" "visits" "bear" "+")) -> ("bear" "sees" "lion" "+"))
If the tiger sees the lion and the lion sees the squirrel then the lion sees the bear.
((("tiger" "sees" "lion" "+") ("lion" "sees" "squirrel" "+")) -> ("lion" "sees" "bear" "+"))
If something is young and it visits the lion then it sees the squirrel.
((("something" "is" "young" "+") ("something" "visits" "lion" "+")) -> ("something" "sees" "squirrel" "+"))
If something needs the squirrel then the squirrel sees the bear.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "sees" "bear" "+"))
If something needs the tiger then it visits the bear.
((("something" "needs" "tiger" "+")) -> ("something" "visits" "bear" "+"))
If something is blue then it needs the bear.
((("something" "is" "blue" "+")) -> ("something" "needs" "bear" "+"))
If something needs the bear and the bear visits the tiger then it sees the squirrel.
((("something" "needs" "bear" "+") ("bear" "visits" "tiger" "+")) -> ("something" "sees" "squirrel" "+"))
The bear is rough.
True
1
proof
[(triple2)]
("bear" "is" "rough" "+")
triple2
The bear is not blue.
False
1
inv-proof
[(triple1)]
("bear" "is" "blue" "-")
triple1
The bear needs the bear.
True
2
proof
[(((triple1) -> rule8))]
("bear" "needs" "bear" "+")
((triple1) -> (rule8 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The squirrel does not see the bear.
False
2
inv-proof
[(((triple5) -> rule6))]
("squirrel" "sees" "bear" "-")
((triple5) -> (rule6 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The squirrel sees the squirrel.
True
4
proof
[(((((triple11) -> rule8) triple7) -> rule9))]
("squirrel" "sees" "squirrel" "+")
((((triple11) -> (rule8 % int2)) triple7) -> (rule9 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The squirrel does not see the squirrel.
False
4
inv-proof
[(((((triple11) -> rule8) triple7) -> rule9))]
("squirrel" "sees" "squirrel" "-")
((((triple11) -> (rule8 % int2)) triple7) -> (rule9 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The squirrel sees the tiger.
True
5
proof
[(((((((triple11) -> rule8) triple7) -> rule9)) -> rule1))]
("squirrel" "sees" "tiger" "+")
((((((triple11) -> (rule8 % int3)) triple7) -> (rule9 % int2))) -> (rule1 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int3
The squirrel does not see the tiger.
False
5
inv-proof
[(((((((triple11) -> rule8) triple7) -> rule9)) -> rule1))]
("squirrel" "sees" "tiger" "-")
((((((triple11) -> (rule8 % int3)) triple7) -> (rule9 % int2))) -> (rule1 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int3
The bear needs the tiger.
True
8
proof
[(((((triple5) -> rule6) ((((((triple11) -> rule8) triple7) -> rule9)) -> rule1)) -> rule2))]
("bear" "needs" "tiger" "+")
((((triple5) -> (rule6 % int5)) ((((((triple11) -> (rule8 % int4)) triple7) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int3
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int4
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int5
The bear does not need the tiger.
False
8
inv-proof
[(((((triple5) -> rule6) ((((((triple11) -> rule8) triple7) -> rule9)) -> rule1)) -> rule2))]
("bear" "needs" "tiger" "-")
((((triple5) -> (rule6 % int5)) ((((((triple11) -> (rule8 % int4)) triple7) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int3
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int4
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int5
The bear visits the bear.
True
9
proof
[(((((((triple5) -> rule6) ((((((triple11) -> rule8) triple7) -> rule9)) -> rule1)) -> rule2)) -> rule7))]
("bear" "visits" "bear" "+")
((((((triple5) -> (rule6 % int6)) ((((((triple11) -> (rule8 % int5)) triple7) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int3
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int4
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int5
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int6
The bear does not visit the bear.
False
9
inv-proof
[(((((((triple5) -> rule6) ((((((triple11) -> rule8) triple7) -> rule9)) -> rule1)) -> rule2)) -> rule7))]
("bear" "visits" "bear" "-")
((((((triple5) -> (rule6 % int6)) ((((((triple11) -> (rule8 % int5)) triple7) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int3
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int4
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int5
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int6
The tiger does not need the bear.
Unknown
inv-rconc
[@1: The tiger needs the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "needs" "bear" "-")
The tiger sees the squirrel.
Unknown
rconc
[@2: The tiger sees the squirrel.[CWA. Example of deepest failure = (rule9 <- rule8 <- FAIL)]]
("tiger" "sees" "squirrel" "+")
The tiger does not visit the bear.
Unknown
inv-rconc
[@1: The tiger visits the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "visits" "bear" "-")
The squirrel visits the bear.
Unknown
rconc
[@1: The squirrel visits the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "visits" "bear" "+")
The lion does not see the bear.
Unknown
inv-rconc
[@1: The lion sees the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "sees" "bear" "-")
The lion sees the tiger.
Unknown
rconc
[@3: The lion sees the tiger.[CWA. Example of deepest failure = (rule1 <- rule9 <- rule8 <- FAIL)]]
("lion" "sees" "tiger" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
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 bear visits the squirrel.
Unknown
random
[@0: The bear visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "squirrel" "+")
The tiger does not visit the squirrel.
Unknown
inv-random
[@0: The tiger visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "squirrel" "-")
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 is blue.[(triple1)] The bear is rough.[(triple2)] The bear is young.[(triple3)] The bear needs the lion.[(triple4)] The bear needs the squirrel.[(triple5)] The bear sees the tiger.[(triple6 OR ((((((triple1) -> rule8) triple7) -> rule9)) -> rule1))] The bear visits the tiger.[(triple7)] The lion is young.[(triple8)] The lion needs the tiger.[(triple9)] The lion visits the squirrel.[(triple10)] The squirrel is blue.[(triple11)] The squirrel sees the lion.[(triple12)] The squirrel visits the lion.[(triple13)] The tiger needs the lion.[(triple14)] @1: The bear needs the bear.[(((triple1) -> rule8))] The lion visits the bear.[(((triple9) -> rule7))] The squirrel needs the bear.[(((triple11) -> rule8))] The squirrel sees the bear.[(((triple5) -> rule6))] @2: The bear sees the squirrel.[(((((triple1) -> rule8) triple7) -> rule9))] The squirrel sees the squirrel.[(((((triple11) -> rule8) triple7) -> rule9))] @3: The squirrel sees the tiger.[(((((((triple11) -> rule8) triple7) -> rule9)) -> rule1))] @4: The bear needs the tiger.[(((((triple5) -> rule6) ((((((triple11) -> rule8) triple7) -> rule9)) -> rule1)) -> rule2))] @5: The bear visits the bear.[(((((((triple5) -> rule6) ((((((triple11) -> rule8) triple7) -> rule9)) -> rule1)) -> rule2)) -> rule7))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The bear is young.
("bear" "is" "young" "+")
triple3
The bear needs the lion.
("bear" "needs" "lion" "+")
triple4
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple5
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple6
((((((triple1) -> (rule8 % int3)) triple7) -> (rule9 % int2))) -> (rule1 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
int3
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple7
The lion is young.
("lion" "is" "young" "+")
triple8
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple9
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple10
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple11
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple12
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple13
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple14
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple1) -> (rule8 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
((triple9) -> (rule7 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
((triple11) -> (rule8 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
((triple5) -> (rule6 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
((((triple1) -> (rule8 % int2)) triple7) -> (rule9 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((triple11) -> (rule8 % int2)) triple7) -> (rule9 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
((((((triple11) -> (rule8 % int3)) triple7) -> (rule9 % int2))) -> (rule1 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int3
The bear needs the tiger.
("bear" "needs" "tiger" "+")
((((triple5) -> (rule6 % int5)) ((((((triple11) -> (rule8 % int4)) triple7) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int3
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int4
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int5
The bear visits the bear.
("bear" "visits" "bear" "+")
((((((triple5) -> (rule6 % int6)) ((((((triple11) -> (rule8 % int5)) triple7) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int3
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int4
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int5
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int6