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