The bear visits the squirrel. The squirrel eats the bear. The squirrel is red. If someone is red and they eat the bear then they are round. If the bear sees the squirrel and the bear visits the squirrel then the squirrel eats the bear. If someone sees the bear then they see the squirrel.
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
If someone is red and they eat the bear then they are round.
((("someone" "is" "red" "+") ("someone" "eats" "bear" "+")) -> ("someone" "is" "round" "+"))
If the bear sees the squirrel and the bear visits the squirrel then the squirrel eats the bear.
((("bear" "sees" "squirrel" "+") ("bear" "visits" "squirrel" "+")) -> ("squirrel" "eats" "bear" "+"))
If someone sees the bear then they see the squirrel.
((("someone" "sees" "bear" "+")) -> ("someone" "sees" "squirrel" "+"))
The squirrel is red.
True
1
proof
[(triple3)]
("squirrel" "is" "red" "+")
triple3
The bear does not visit the squirrel.
False
1
inv-proof
[(triple1)]
("bear" "visits" "squirrel" "-")
triple1
The squirrel is round.
True
3
proof
[(((triple3 triple2) -> rule1))]
("squirrel" "is" "round" "+")
((triple3 triple2) -> (rule1 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is not round.
False
3
inv-proof
[(((triple3 triple2) -> rule1))]
("squirrel" "is" "round" "-")
((triple3 triple2) -> (rule1 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The bear is not round.
Unknown
inv-rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "round" "-")
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 is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The bear visits the squirrel.[(triple1)] The squirrel eats the bear.[(triple2)] The squirrel is red.[(triple3)] @1: The squirrel is round.[(((triple3 triple2) -> rule1))]
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple2
The squirrel is red.
("squirrel" "is" "red" "+")
triple3
The squirrel is round.
("squirrel" "is" "round" "+")
((triple3 triple2) -> (rule1 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1