The bear is big. The bear needs the mouse. The bear visits the cat. The cat is blue. The cat is nice. The cat is young. The cat needs the bear. The cat needs the mouse. The cat visits the bear. The cat visits the squirrel. The mouse is not nice. The mouse needs the bear. The mouse needs the squirrel. The mouse sees the bear. The squirrel is blue. The squirrel does not see the cat. If something needs the bear then it is red.
The bear is big.
("bear" "is" "big" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The mouse is not nice.
("mouse" "is" "nice" "-")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel does not see the cat.
("squirrel" "sees" "cat" "-")
If something needs the bear then it is red.
((("something" "needs" "bear" "+")) -> ("something" "is" "red" "+"))
The cat visits the squirrel.
True
1
proof
[(triple10)]
("cat" "visits" "squirrel" "+")
triple10
The cat does not need the mouse.
False
1
inv-proof
[(triple8)]
("cat" "needs" "mouse" "-")
triple8
The mouse is red.
True
2
proof
[(((triple12) -> rule1))]
("mouse" "is" "red" "+")
((triple12) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is not red.
False
2
inv-proof
[(((triple12) -> rule1))]
("mouse" "is" "red" "-")
((triple12) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The squirrel is not red.
Unknown
inv-rconc
[@1: The squirrel is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "red" "-")
The bear is red.
Unknown
rconc
[@1: The bear is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "red" "+")
The bear does not need the squirrel.
Unknown
inv-random
[@0: The bear needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "squirrel" "-")
The squirrel needs the bear.
Unknown
random
[@0: The squirrel needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "bear" "+")
@0: The bear is big.[(triple1)] The bear needs the mouse.[(triple2)] The bear visits the cat.[(triple3)] The cat is blue.[(triple4)] The cat is nice.[(triple5)] The cat is young.[(triple6)] The cat needs the bear.[(triple7)] The cat needs the mouse.[(triple8)] The cat visits the bear.[(triple9)] The cat visits the squirrel.[(triple10)] The mouse is not nice.[(triple11)] The mouse needs the bear.[(triple12)] The mouse needs the squirrel.[(triple13)] The mouse sees the bear.[(triple14)] The squirrel does not see the cat.[(triple16)] The squirrel is blue.[(triple15)] @1: The cat is red.[(((triple7) -> rule1))] The mouse is red.[(((triple12) -> rule1))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple2
The bear visits the cat.
("bear" "visits" "cat" "+")
triple3
The cat is blue.
("cat" "is" "blue" "+")
triple4
The cat is nice.
("cat" "is" "nice" "+")
triple5
The cat is young.
("cat" "is" "young" "+")
triple6
The cat needs the bear.
("cat" "needs" "bear" "+")
triple7
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple8
The cat visits the bear.
("cat" "visits" "bear" "+")
triple9
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple10
The mouse is not nice.
("mouse" "is" "nice" "-")
triple11
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple12
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple13
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple14
The squirrel does not see the cat.
("squirrel" "sees" "cat" "-")
triple16
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple15
The cat is red.
("cat" "is" "red" "+")
((triple7) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
((triple12) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1