The bear is big. The squirrel likes the bear. The squirrel sees the bear. If something sees the squirrel then it is red. If something likes the squirrel and it is cold then the squirrel sees the bear. If something is big then it sees the squirrel.
The bear is big.
("bear" "is" "big" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If something sees the squirrel then it is red.
((("something" "sees" "squirrel" "+")) -> ("something" "is" "red" "+"))
If something likes the squirrel and it is cold then the squirrel sees the bear.
((("something" "likes" "squirrel" "+") ("something" "is" "cold" "+")) -> ("squirrel" "sees" "bear" "+"))
If something is big then it sees the squirrel.
((("something" "is" "big" "+")) -> ("something" "sees" "squirrel" "+"))
The squirrel sees the bear.
True
1
proof
[(triple3)]
("squirrel" "sees" "bear" "+")
triple3
The bear is not big.
False
1
inv-proof
[(triple1)]
("bear" "is" "big" "-")
triple1
The bear sees the squirrel.
True
2
proof
[(((triple1) -> rule3))]
("bear" "sees" "squirrel" "+")
((triple1) -> (rule3 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear does not see the squirrel.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "sees" "squirrel" "-")
((triple1) -> (rule3 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear is red.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("bear" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int2
The bear is not red.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("bear" "is" "red" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int2
The squirrel is not red.
Unknown
inv-rconc
[@2: The squirrel is red.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("squirrel" "is" "red" "-")
The squirrel sees the squirrel.
Unknown
rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "sees" "squirrel" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The squirrel does not chase the bear.
Unknown
inv-random
[@0: The squirrel chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "bear" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The bear is big.[(triple1)] The squirrel likes the bear.[(triple2)] The squirrel sees the bear.[(triple3)] @1: The bear sees the squirrel.[(((triple1) -> rule3))] @2: The bear is red.[(((((triple1) -> rule3)) -> rule1))]
The bear is big.
("bear" "is" "big" "+")
triple1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple2
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple3
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
((triple1) -> (rule3 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear is red.
("bear" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int2