The dog is not big. The dog does not see the mouse. The dog does not see the squirrel. The lion is big. The lion is blue. The lion does not like the mouse. The lion sees the dog. The lion does not see the squirrel. The lion visits the mouse. The mouse likes the squirrel. The mouse sees the squirrel. The mouse visits the dog. The mouse visits the squirrel. The squirrel is rough. The squirrel likes the mouse. The squirrel sees the dog. If someone likes the mouse then they like the squirrel. If someone visits the squirrel then the squirrel is big.
The dog is not big.
("dog" "is" "big" "-")
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
The dog does not see the squirrel.
("dog" "sees" "squirrel" "-")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion does not like the mouse.
("lion" "likes" "mouse" "-")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion does not see the squirrel.
("lion" "sees" "squirrel" "-")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
If someone likes the mouse then they like the squirrel.
((("someone" "likes" "mouse" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone visits the squirrel then the squirrel is big.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "is" "big" "+"))
The lion does not see the squirrel.
True
1
proof
[(triple8)]
("lion" "sees" "squirrel" "-")
triple8
The lion is not blue.
False
1
inv-proof
[(triple5)]
("lion" "is" "blue" "-")
triple5
The squirrel likes the squirrel.
True
2
proof
[(((triple15) -> rule1))]
("squirrel" "likes" "squirrel" "+")
((triple15) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel does not like the squirrel.
False
2
inv-proof
[(((triple15) -> rule1))]
("squirrel" "likes" "squirrel" "-")
((triple15) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The lion does not like the squirrel.
Unknown
inv-rconc
[@1: The lion likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "squirrel" "-")
The dog likes the squirrel.
Unknown
rconc
[@1: The dog likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "likes" "squirrel" "+")
The dog is not red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
@0: The dog does not see the mouse.[(triple2)] The dog does not see the squirrel.[(triple3)] The dog is not big.[(triple1)] The lion does not like the mouse.[(triple6)] The lion does not see the squirrel.[(triple8)] The lion is big.[(triple4)] The lion is blue.[(triple5)] The lion sees the dog.[(triple7)] The lion visits the mouse.[(triple9)] The mouse likes the squirrel.[(triple10)] The mouse sees the squirrel.[(triple11)] The mouse visits the dog.[(triple12)] The mouse visits the squirrel.[(triple13)] The squirrel is rough.[(triple14)] The squirrel likes the mouse.[(triple15)] The squirrel sees the dog.[(triple16)] @1: The squirrel is big.[(((triple13) -> rule2))] The squirrel likes the squirrel.[(((triple15) -> rule1))]
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
triple2
The dog does not see the squirrel.
("dog" "sees" "squirrel" "-")
triple3
The dog is not big.
("dog" "is" "big" "-")
triple1
The lion does not like the mouse.
("lion" "likes" "mouse" "-")
triple6
The lion does not see the squirrel.
("lion" "sees" "squirrel" "-")
triple8
The lion is big.
("lion" "is" "big" "+")
triple4
The lion is blue.
("lion" "is" "blue" "+")
triple5
The lion sees the dog.
("lion" "sees" "dog" "+")
triple7
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple9
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple10
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple11
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple12
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple13
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple14
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple15
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple16
The squirrel is big.
("squirrel" "is" "big" "+")
((triple13) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((triple15) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1