The dog eats the mouse. The dog eats the squirrel. The dog sees the mouse. The dog sees the squirrel. The mouse eats the squirrel. The mouse is big. The squirrel eats the dog. The squirrel is young. The squirrel likes the dog. The squirrel sees the dog. If something likes the dog then the dog is big. If something sees the dog then it is rough. If something is green then it eats the squirrel.
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is big.
("mouse" "is" "big" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
If something likes the dog then the dog is big.
((("something" "likes" "dog" "+")) -> ("dog" "is" "big" "+"))
If something sees the dog then it is rough.
((("something" "sees" "dog" "+")) -> ("something" "is" "rough" "+"))
If something is green then it eats the squirrel.
((("something" "is" "green" "+")) -> ("something" "eats" "squirrel" "+"))
The squirrel likes the dog.
True
1
proof
[(triple9)]
("squirrel" "likes" "dog" "+")
triple9
The dog does not see the squirrel.
False
1
inv-proof
[(triple4)]
("dog" "sees" "squirrel" "-")
triple4
The dog is big.
True
2
proof
[(((triple9) -> rule1))]
("dog" "is" "big" "+")
((triple9) -> (rule1 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The squirrel is not rough.
False
2
inv-proof
[(((triple10) -> rule2))]
("squirrel" "is" "rough" "-")
((triple10) -> (rule2 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel does not eat the squirrel.
Unknown
inv-rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "eats" "squirrel" "-")
The mouse is rough.
Unknown
rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "rough" "+")
The dog does not like the mouse.
Unknown
inv-random
[@0: The dog likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "mouse" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
@0: The dog eats the mouse.[(triple1)] The dog eats the squirrel.[(triple2)] The dog sees the mouse.[(triple3)] The dog sees the squirrel.[(triple4)] The mouse eats the squirrel.[(triple5)] The mouse is big.[(triple6)] The squirrel eats the dog.[(triple7)] The squirrel is young.[(triple8)] The squirrel likes the dog.[(triple9)] The squirrel sees the dog.[(triple10)] @1: The dog is big.[(((triple9) -> rule1))] The squirrel is rough.[(((triple10) -> rule2))]
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple1
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple3
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple4
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple5
The mouse is big.
("mouse" "is" "big" "+")
triple6
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple7
The squirrel is young.
("squirrel" "is" "young" "+")
triple8
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple9
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple10
The dog is big.
("dog" "is" "big" "+")
((triple9) -> (rule1 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple10) -> (rule2 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1