The dog is not big. The dog is blue. The dog is red. The dog likes the mouse. The dog does not see the mouse. The dog visits the mouse. The dog visits the squirrel. The mouse is blue. The mouse sees the dog. The mouse sees the squirrel. The squirrel is big. The squirrel does not like the mouse. If the dog visits the squirrel and the dog is not cold then the squirrel is round. If something likes the mouse and it likes the squirrel then it visits the dog. If the mouse visits the dog then the mouse likes the squirrel. If the squirrel sees the mouse then the mouse likes the squirrel. If something is big then it likes the dog. If something sees the mouse and it is round then it likes the dog. If something is red then it likes the squirrel. If something is round and it does not like the mouse then it visits the mouse.
The dog is not big.
("dog" "is" "big" "-")
The dog is blue.
("dog" "is" "blue" "+")
The dog is red.
("dog" "is" "red" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel does not like the mouse.
("squirrel" "likes" "mouse" "-")
If the dog visits the squirrel and the dog is not cold then the squirrel is round.
((("dog" "visits" "squirrel" "+") ("dog" "is" "cold" "~")) -> ("squirrel" "is" "round" "+"))
If something likes the mouse and it likes the squirrel then it visits the dog.
((("something" "likes" "mouse" "+") ("something" "likes" "squirrel" "+")) -> ("something" "visits" "dog" "+"))
If the mouse visits the dog then the mouse likes the squirrel.
((("mouse" "visits" "dog" "+")) -> ("mouse" "likes" "squirrel" "+"))
If the squirrel sees the mouse then the mouse likes the squirrel.
((("squirrel" "sees" "mouse" "+")) -> ("mouse" "likes" "squirrel" "+"))
If something is big then it likes the dog.
((("something" "is" "big" "+")) -> ("something" "likes" "dog" "+"))
If something sees the mouse and it is round then it likes the dog.
((("something" "sees" "mouse" "+") ("something" "is" "round" "+")) -> ("something" "likes" "dog" "+"))
If something is red then it likes the squirrel.
((("something" "is" "red" "+")) -> ("something" "likes" "squirrel" "+"))
If something is round and it does not like the mouse then it visits the mouse.
((("something" "is" "round" "+") ("something" "likes" "mouse" "~")) -> ("something" "visits" "mouse" "+"))
The mouse sees the squirrel.
True
1
proof
[(triple10)]
("mouse" "sees" "squirrel" "+")
triple10
The dog does not visit the squirrel.
False
1
inv-proof
[(triple7)]
("dog" "visits" "squirrel" "-")
triple7
The squirrel likes the dog.
True
2
proof
[(((triple11) -> rule5))]
("squirrel" "likes" "dog" "+")
((triple11) -> (rule5 % int1))
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int1
The dog does not like the squirrel.
False
2
inv-proof
[(((triple3) -> rule7))]
("dog" "likes" "squirrel" "-")
((triple3) -> (rule7 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog visits the dog.
True
4
proof
[(((triple4 ((triple3) -> rule7)) -> rule2))]
("dog" "visits" "dog" "+")
((triple4 ((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int2
The dog does not visit the dog.
False
4
inv-proof
[(((triple4 ((triple3) -> rule7)) -> rule2))]
("dog" "visits" "dog" "-")
((triple4 ((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int2
The mouse does not like the dog.
Unknown
inv-rconc
[@1: The mouse likes the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "likes" "dog" "-")
The mouse visits the dog.
Unknown
rconc
[@1: The mouse visits the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "visits" "dog" "+")
The squirrel does not visit the mouse.
Unknown
inv-rconc
[@1: The squirrel visits the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "visits" "mouse" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The squirrel sees the mouse.
Unknown
random
[@0: The squirrel sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "mouse" "+")
@0: The dog does not see the mouse.[(triple5)] The dog is blue.[(triple2)] The dog is not big.[(triple1)] The dog is red.[(triple3)] The dog likes the mouse.[(triple4)] The dog visits the mouse.[(triple6)] The dog visits the squirrel.[(triple7)] The mouse is blue.[(triple8)] The mouse sees the dog.[(triple9)] The mouse sees the squirrel.[(triple10)] The squirrel does not like the mouse.[(triple12)] The squirrel is big.[(triple11)] @1: The dog likes the squirrel.[(((triple3) -> rule7))] The squirrel likes the dog.[(((triple11) -> rule5))] @2: The dog visits the dog.[(((triple4 ((triple3) -> rule7)) -> rule2))]
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
triple5
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog is not big.
("dog" "is" "big" "-")
triple1
The dog is red.
("dog" "is" "red" "+")
triple3
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple4
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple6
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple7
The mouse is blue.
("mouse" "is" "blue" "+")
triple8
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple9
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple10
The squirrel does not like the mouse.
("squirrel" "likes" "mouse" "-")
triple12
The squirrel is big.
("squirrel" "is" "big" "+")
triple11
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
((triple3) -> (rule7 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
((triple11) -> (rule5 % int1))
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple4 ((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int2