The bear needs the squirrel. The squirrel sees the bear. If someone needs the squirrel then the squirrel needs the bear. If the bear visits the squirrel and the squirrel is cold then the bear sees the squirrel. If someone needs the bear then they are rough. If someone visits the bear then the bear visits the squirrel. If someone sees the bear and the bear needs the squirrel then the squirrel is cold. If someone visits the squirrel then they are nice.
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If someone needs the squirrel then the squirrel needs the bear.
((("someone" "needs" "squirrel" "+")) -> ("squirrel" "needs" "bear" "+"))
If the bear visits the squirrel and the squirrel is cold then the bear sees the squirrel.
((("bear" "visits" "squirrel" "+") ("squirrel" "is" "cold" "+")) -> ("bear" "sees" "squirrel" "+"))
If someone needs the bear then they are rough.
((("someone" "needs" "bear" "+")) -> ("someone" "is" "rough" "+"))
If someone visits the bear then the bear visits the squirrel.
((("someone" "visits" "bear" "+")) -> ("bear" "visits" "squirrel" "+"))
If someone sees the bear and the bear needs the squirrel then the squirrel is cold.
((("someone" "sees" "bear" "+") ("bear" "needs" "squirrel" "+")) -> ("squirrel" "is" "cold" "+"))
If someone visits the squirrel then they are nice.
((("someone" "visits" "squirrel" "+")) -> ("someone" "is" "nice" "+"))
The bear needs the squirrel.
True
1
proof
[(triple1)]
("bear" "needs" "squirrel" "+")
triple1
The squirrel does not see the bear.
False
1
inv-proof
[(triple2)]
("squirrel" "sees" "bear" "-")
triple2
The squirrel needs the bear.
True
2
proof
[(((triple1) -> rule1))]
("squirrel" "needs" "bear" "+")
((triple1) -> (rule1 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The squirrel does not need the bear.
False
2
inv-proof
[(((triple1) -> rule1))]
("squirrel" "needs" "bear" "-")
((triple1) -> (rule1 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The squirrel is rough.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("squirrel" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The squirrel is not rough.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("squirrel" "is" "rough" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The bear does not see the squirrel.
Unknown
inv-rconc
[@2: The bear sees the squirrel.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("bear" "sees" "squirrel" "-")
The bear is rough.
Unknown
rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "rough" "+")
The bear is not nice.
Unknown
inv-rconc
[@2: The bear is nice.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("bear" "is" "nice" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
@0: The bear needs the squirrel.[(triple1)] The squirrel sees the bear.[(triple2)] @1: The squirrel is cold.[(((triple2 triple1) -> rule5))] The squirrel needs the bear.[(((triple1) -> rule1))] @2: The squirrel is rough.[(((((triple1) -> rule1)) -> rule3))]
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple2
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple2 triple1) -> (rule5 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
((triple1) -> (rule1 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2