The bear chases the rabbit. The bear chases the squirrel. The bear is not nice. The bear does not see the rabbit. The bear sees the squirrel. The rabbit eats the squirrel. The squirrel chases the bear. The squirrel eats the bear. The squirrel is big. The squirrel is cold. The squirrel is kind. The squirrel does not see the bear. If something is kind and cold then it eats the squirrel. If something chases the rabbit and it sees the bear then it sees the squirrel. If something eats the squirrel then it sees the squirrel. If something is big and it sees the squirrel then the squirrel does not see the rabbit. If the rabbit chases the squirrel then the rabbit chases the bear. If the rabbit sees the squirrel and the bear does not eat the rabbit then the bear eats the squirrel. If the rabbit is rough and the rabbit chases the bear then the rabbit does not chase the squirrel. If something is rough and it does not chase the bear then the bear chases the squirrel.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear is not nice.
("bear" "is" "nice" "-")
The bear does not see the rabbit.
("bear" "sees" "rabbit" "-")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel does not see the bear.
("squirrel" "sees" "bear" "-")
If something is kind and cold then it eats the squirrel.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "eats" "squirrel" "+"))
If something chases the rabbit and it sees the bear then it sees the squirrel.
((("something" "chases" "rabbit" "+") ("something" "sees" "bear" "+")) -> ("something" "sees" "squirrel" "+"))
If something eats the squirrel then it sees the squirrel.
((("something" "eats" "squirrel" "+")) -> ("something" "sees" "squirrel" "+"))
If something is big and it sees the squirrel then the squirrel does not see the rabbit.
((("something" "is" "big" "+") ("something" "sees" "squirrel" "+")) -> ("squirrel" "sees" "rabbit" "-"))
If the rabbit chases the squirrel then the rabbit chases the bear.
((("rabbit" "chases" "squirrel" "+")) -> ("rabbit" "chases" "bear" "+"))
If the rabbit sees the squirrel and the bear does not eat the rabbit then the bear eats the squirrel.
((("rabbit" "sees" "squirrel" "+") ("bear" "eats" "rabbit" "~")) -> ("bear" "eats" "squirrel" "+"))
If the rabbit is rough and the rabbit chases the bear then the rabbit does not chase the squirrel.
((("rabbit" "is" "rough" "+") ("rabbit" "chases" "bear" "+")) -> ("rabbit" "chases" "squirrel" "-"))
If something is rough and it does not chase the bear then the bear chases the squirrel.
((("something" "is" "rough" "+") ("something" "chases" "bear" "~")) -> ("bear" "chases" "squirrel" "+"))
The squirrel chases the bear.
True
1
proof
[(triple7)]
("squirrel" "chases" "bear" "+")
triple7
The bear does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("bear" "chases" "rabbit" "-")
triple1
The rabbit sees the squirrel.
True
2
proof
[(((triple6) -> rule3))]
("rabbit" "sees" "squirrel" "+")
((triple6) -> (rule3 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The squirrel does not eat the squirrel.
False
3
inv-proof
[(((triple11 triple10) -> rule1))]
("squirrel" "eats" "squirrel" "-")
((triple11 triple10) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel sees the squirrel.
True
4
proof
[(((((triple11 triple10) -> rule1)) -> rule3))]
("squirrel" "sees" "squirrel" "+")
((((triple11 triple10) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel does not see the squirrel.
False
4
inv-proof
[(((((triple11 triple10) -> rule1)) -> rule3))]
("squirrel" "sees" "squirrel" "-")
((((triple11 triple10) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel does not see the rabbit.
True
6
proof
[(((triple9 ((((triple11 triple10) -> rule1)) -> rule3)) -> rule4))]
("squirrel" "sees" "rabbit" "-")
((triple9 ((((triple11 triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel does not see the rabbit.
("squirrel" "sees" "rabbit" "-")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel sees the rabbit.
False
6
inv-proof
[(((triple9 ((((triple11 triple10) -> rule1)) -> rule3)) -> rule4))]
("squirrel" "sees" "rabbit" "+")
((triple9 ((((triple11 triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel does not see the rabbit.
("squirrel" "sees" "rabbit" "-")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The rabbit does not chase the bear.
Unknown
inv-rconc
[@1: The rabbit chases the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "chases" "bear" "-")
The bear eats the squirrel.
Unknown
rconc
[@1: The bear eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "eats" "squirrel" "+")
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
The rabbit eats the bear.
Unknown
random
[@0: The rabbit eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "bear" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
The rabbit does not see the bear.
Unknown
inv-random
[@0: The rabbit sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "bear" "-")
The squirrel chases the rabbit.
Unknown
random
[@0: The squirrel chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "rabbit" "+")
@0: The bear chases the rabbit.[(triple1)] The bear chases the squirrel.[(triple2)] The bear does not see the rabbit.[(triple4)] The bear is not nice.[(triple3)] The bear sees the squirrel.[(triple5)] The rabbit eats the squirrel.[(triple6)] The squirrel chases the bear.[(triple7)] The squirrel does not see the bear.[(triple12)] The squirrel eats the bear.[(triple8)] The squirrel is big.[(triple9)] The squirrel is cold.[(triple10)] The squirrel is kind.[(triple11)] @1: The rabbit sees the squirrel.[(((triple6) -> rule3))] The squirrel eats the squirrel.[(((triple11 triple10) -> rule1))] @2: The squirrel sees the squirrel.[(((((triple11 triple10) -> rule1)) -> rule3))] @3: The squirrel does not see the rabbit.[(((triple9 ((((triple11 triple10) -> rule1)) -> rule3)) -> rule4))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple2
The bear does not see the rabbit.
("bear" "sees" "rabbit" "-")
triple4
The bear is not nice.
("bear" "is" "nice" "-")
triple3
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple5
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple6
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple7
The squirrel does not see the bear.
("squirrel" "sees" "bear" "-")
triple12
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple8
The squirrel is big.
("squirrel" "is" "big" "+")
triple9
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple10
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple11
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
((triple6) -> (rule3 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((triple11 triple10) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((triple11 triple10) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel does not see the rabbit.
("squirrel" "sees" "rabbit" "-")
((triple9 ((((triple11 triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel does not see the rabbit.
("squirrel" "sees" "rabbit" "-")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3