The bear is nice. The bear is young. The bear sees the squirrel. The bear visits the tiger. The cow sees the squirrel. The squirrel is not cold. The squirrel does not need the cow. The squirrel sees the cow. The squirrel visits the bear. The tiger visits the squirrel. If the bear is blue and the bear is not round then the bear sees the tiger. If someone visits the squirrel then they see the tiger. If someone is young then they need the squirrel. If someone visits the tiger and the tiger visits the bear then they need the cow. If the bear is not blue then the bear does not need the cow. If someone is young then they see the bear. If someone needs the squirrel then they visit the squirrel. If someone is young and cold then they do not see the squirrel.
The bear is nice.
("bear" "is" "nice" "+")
The bear is young.
("bear" "is" "young" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The squirrel is not cold.
("squirrel" "is" "cold" "-")
The squirrel does not need the cow.
("squirrel" "needs" "cow" "-")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If the bear is blue and the bear is not round then the bear sees the tiger.
((("bear" "is" "blue" "+") ("bear" "is" "round" "~")) -> ("bear" "sees" "tiger" "+"))
If someone visits the squirrel then they see the tiger.
((("someone" "visits" "squirrel" "+")) -> ("someone" "sees" "tiger" "+"))
If someone is young then they need the squirrel.
((("someone" "is" "young" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone visits the tiger and the tiger visits the bear then they need the cow.
((("someone" "visits" "tiger" "+") ("tiger" "visits" "bear" "+")) -> ("someone" "needs" "cow" "+"))
If the bear is not blue then the bear does not need the cow.
((("bear" "is" "blue" "~")) -> ("bear" "needs" "cow" "-"))
If someone is young then they see the bear.
((("someone" "is" "young" "+")) -> ("someone" "sees" "bear" "+"))
If someone needs the squirrel then they visit the squirrel.
((("someone" "needs" "squirrel" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone is young and cold then they do not see the squirrel.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "sees" "squirrel" "-"))
The tiger visits the squirrel.
True
1
proof
[(triple10)]
("tiger" "visits" "squirrel" "+")
triple10
The tiger does not visit the squirrel.
False
1
inv-proof
[(triple10)]
("tiger" "visits" "squirrel" "-")
triple10
The bear sees the bear.
True
2
proof
[(((triple2) -> rule6))]
("bear" "sees" "bear" "+")
((triple2) -> (rule6 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear does not see the bear.
False
2
inv-proof
[(((triple2) -> rule6))]
("bear" "sees" "bear" "-")
((triple2) -> (rule6 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear visits the squirrel.
True
3
proof
[(((((triple2) -> rule3)) -> rule7))]
("bear" "visits" "squirrel" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The bear does not visit the squirrel.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule7))]
("bear" "visits" "squirrel" "-")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The bear sees the tiger.
True
4
proof
[(((((((triple2) -> rule3)) -> rule7)) -> rule2))]
("bear" "sees" "tiger" "+")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
The bear does not see the tiger.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule7)) -> rule2))]
("bear" "sees" "tiger" "-")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
The cow does not visit the squirrel.
Unknown
inv-rconc
[@2: The cow visits the squirrel.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("cow" "visits" "squirrel" "-")
The cow needs the squirrel.
Unknown
rconc
[@1: The cow needs the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "needs" "squirrel" "+")
The squirrel does not see the tiger.
Unknown
inv-rconc
[@3: The squirrel sees the tiger.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule3 <- FAIL)]]
("squirrel" "sees" "tiger" "-")
The bear needs the cow.
Unknown
rconc
[@1: The bear needs the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "needs" "cow" "+")
The squirrel does not visit the tiger.
Unknown
inv-random
[@0: The squirrel visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "tiger" "-")
The squirrel needs the tiger.
Unknown
random
[@0: The squirrel needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "tiger" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The bear visits the cow.
Unknown
random
[@0: The bear visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "cow" "+")
@0: The bear is nice.[(triple1)] The bear is young.[(triple2)] The bear sees the squirrel.[(triple3)] The bear visits the tiger.[(triple4)] The cow sees the squirrel.[(triple5)] The squirrel does not need the cow.[(triple7)] The squirrel is not cold.[(triple6)] The squirrel sees the cow.[(triple8)] The squirrel visits the bear.[(triple9)] The tiger visits the squirrel.[(triple10)] @1: The bear needs the squirrel.[(((triple2) -> rule3))] The bear sees the bear.[(((triple2) -> rule6))] The tiger sees the tiger.[(((triple10) -> rule2))] @2: The bear visits the squirrel.[(((((triple2) -> rule3)) -> rule7))] @3: The bear sees the tiger.[(((((((triple2) -> rule3)) -> rule7)) -> rule2))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple3
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple4
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple5
The squirrel does not need the cow.
("squirrel" "needs" "cow" "-")
triple7
The squirrel is not cold.
("squirrel" "is" "cold" "-")
triple6
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple8
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple9
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple10
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
((triple2) -> (rule3 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple2) -> (rule6 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple10) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The bear sees the tiger.
("bear" "sees" "tiger" "+")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3