The bear eats the squirrel. The bear is not cold. The bear is nice. The bear is not round. The bear does not see the lion. The lion eats the squirrel. The lion likes the bear. The lion sees the squirrel. The squirrel is kind. The squirrel likes the bear. If someone eats the squirrel then the squirrel is nice. If the bear does not see the squirrel then the squirrel likes the lion. If someone is nice then they see the bear.
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The bear is not cold.
("bear" "is" "cold" "-")
The bear is nice.
("bear" "is" "nice" "+")
The bear is not round.
("bear" "is" "round" "-")
The bear does not see the lion.
("bear" "sees" "lion" "-")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
If someone eats the squirrel then the squirrel is nice.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "is" "nice" "+"))
If the bear does not see the squirrel then the squirrel likes the lion.
((("bear" "sees" "squirrel" "~")) -> ("squirrel" "likes" "lion" "+"))
If someone is nice then they see the bear.
((("someone" "is" "nice" "+")) -> ("someone" "sees" "bear" "+"))
The bear is not round.
True
1
proof
[(triple4)]
("bear" "is" "round" "-")
triple4
The bear does not eat the squirrel.
False
1
inv-proof
[(triple1)]
("bear" "eats" "squirrel" "-")
triple1
The squirrel is nice.
True
2
proof
[(((triple1) -> rule1) OR ((triple6) -> rule1))]
("squirrel" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((triple6) -> (rule1 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is not nice.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple6) -> rule1))]
("squirrel" "is" "nice" "-")
((triple1) -> (rule1 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((triple6) -> (rule1 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel sees the bear.
True
3
proof
[(((((triple1) -> rule1)) -> rule3) OR ((((triple6) -> rule1)) -> rule3))]
("squirrel" "sees" "bear" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel does not see the bear.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3) OR ((((triple6) -> rule1)) -> rule3))]
("squirrel" "sees" "bear" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel does not like the lion.
Unknown
inv-rconc
[@1: The squirrel likes the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "likes" "lion" "-")
The lion sees the bear.
Unknown
rconc
[@1: The lion sees the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "sees" "bear" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The lion does not like the squirrel.
Unknown
inv-random
[@0: The lion likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "squirrel" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
@0: The bear does not see the lion.[(triple5)] The bear eats the squirrel.[(triple1)] The bear is nice.[(triple3)] The bear is not cold.[(triple2)] The bear is not round.[(triple4)] The lion eats the squirrel.[(triple6)] The lion likes the bear.[(triple7)] The lion sees the squirrel.[(triple8)] The squirrel is kind.[(triple9)] The squirrel likes the bear.[(triple10)] @1: The bear sees the bear.[(((triple3) -> rule3))] The squirrel is nice.[(((triple1) -> rule1) OR ((triple6) -> rule1))] @2: The squirrel sees the bear.[(((((triple1) -> rule1)) -> rule3) OR ((((triple6) -> rule1)) -> rule3))]
The bear does not see the lion.
("bear" "sees" "lion" "-")
triple5
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple3
The bear is not cold.
("bear" "is" "cold" "-")
triple2
The bear is not round.
("bear" "is" "round" "-")
triple4
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple6
The lion likes the bear.
("lion" "likes" "bear" "+")
triple7
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple8
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple9
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple10
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple3) -> (rule3 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((triple6) -> (rule1 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2