The bear does not chase the squirrel. The squirrel needs the bear. If something needs the bear then it is young. If something needs the squirrel and it likes the bear then it is blue. If something is big and it needs the bear then it is green. If something needs the squirrel then it is not green. If something chases the squirrel and it is blue then the squirrel needs the bear. If something likes the bear then the bear needs the squirrel. If something is young then it likes the bear. If something needs the bear and the bear does not chase the squirrel then it is not big.
The bear does not chase the squirrel.
("bear" "chases" "squirrel" "-")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
If something needs the bear then it is young.
((("something" "needs" "bear" "+")) -> ("something" "is" "young" "+"))
If something needs the squirrel and it likes the bear then it is blue.
((("something" "needs" "squirrel" "+") ("something" "likes" "bear" "+")) -> ("something" "is" "blue" "+"))
If something is big and it needs the bear then it is green.
((("something" "is" "big" "+") ("something" "needs" "bear" "+")) -> ("something" "is" "green" "+"))
If something needs the squirrel then it is not green.
((("something" "needs" "squirrel" "+")) -> ("something" "is" "green" "-"))
If something chases the squirrel and it is blue then the squirrel needs the bear.
((("something" "chases" "squirrel" "+") ("something" "is" "blue" "+")) -> ("squirrel" "needs" "bear" "+"))
If something likes the bear then the bear needs the squirrel.
((("something" "likes" "bear" "+")) -> ("bear" "needs" "squirrel" "+"))
If something is young then it likes the bear.
((("something" "is" "young" "+")) -> ("something" "likes" "bear" "+"))
If something needs the bear and the bear does not chase the squirrel then it is not big.
((("something" "needs" "bear" "+") ("bear" "chases" "squirrel" "~")) -> ("something" "is" "big" "-"))
The squirrel needs the bear.
True
1
proof
[(triple2)]
("squirrel" "needs" "bear" "+")
triple2
The bear chases the squirrel.
False
1
inv-proof
[(triple1)]
("bear" "chases" "squirrel" "+")
triple1
The squirrel is young.
True
2
proof
[(((triple2) -> rule1))]
("squirrel" "is" "young" "+")
((triple2) -> (rule1 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is not young.
False
2
inv-proof
[(((triple2) -> rule1))]
("squirrel" "is" "young" "-")
((triple2) -> (rule1 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel likes the bear.
True
3
proof
[(((((triple2) -> rule1)) -> rule7))]
("squirrel" "likes" "bear" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel does not like the bear.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule7))]
("squirrel" "likes" "bear" "-")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The bear needs the squirrel.
True
4
proof
[(((((((triple2) -> rule1)) -> rule7)) -> rule6))]
("bear" "needs" "squirrel" "+")
((((((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
int3
The bear does not need the squirrel.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule7)) -> rule6))]
("bear" "needs" "squirrel" "-")
((((((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
int3
The squirrel is not blue.
Unknown
inv-rconc
[@1: The squirrel is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "blue" "-")
The bear likes the bear.
Unknown
rconc
[@2: The bear likes the bear.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("bear" "likes" "bear" "+")
The bear is not blue.
Unknown
inv-rconc
[@3: The bear is blue.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule1 <- FAIL)]]
("bear" "is" "blue" "-")
The bear is young.
Unknown
rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "young" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
@0: The bear does not chase the squirrel.[(triple1)] The squirrel needs the bear.[(triple2)] @1: The squirrel is not big.[(((triple2 triple1) -> rule8))] The squirrel is young.[(((triple2) -> rule1))] @2: The squirrel likes the bear.[(((((triple2) -> rule1)) -> rule7))] @3: The bear needs the squirrel.[(((((((triple2) -> rule1)) -> rule7)) -> rule6))] @4: The bear is not green.[(((((((((triple2) -> rule1)) -> rule7)) -> rule6)) -> rule4))]
The bear does not chase the squirrel.
("bear" "chases" "squirrel" "-")
triple1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple2
The squirrel is not big.
("squirrel" "is" "big" "-")
((triple2 triple1) -> (rule8 % int1))
The squirrel is not big.
("squirrel" "is" "big" "-")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
((triple2) -> (rule1 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
((((((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
int3
The bear is not green.
("bear" "is" "green" "-")
((((((((triple2) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int3
The squirrel is young.
("squirrel" "is" "young" "+")
int4