The dog likes the squirrel. The mouse is not kind. The squirrel needs the dog. If something likes the dog and it does not need the dog then the dog needs the squirrel. If something visits the mouse then it likes the mouse. If something visits the dog then it likes the mouse. If something needs the squirrel and the squirrel does not need the dog then the squirrel likes the mouse. If something likes the mouse and it likes the squirrel then the squirrel likes the dog. If something likes the squirrel then it visits the mouse. If something needs the squirrel then the squirrel does not need the mouse. If something visits the squirrel and the squirrel does not visit the mouse then the squirrel needs the mouse.
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The mouse is not kind.
("mouse" "is" "kind" "-")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
If something likes the dog and it does not need the dog then the dog needs the squirrel.
((("something" "likes" "dog" "+") ("something" "needs" "dog" "~")) -> ("dog" "needs" "squirrel" "+"))
If something visits the mouse then it likes the mouse.
((("something" "visits" "mouse" "+")) -> ("something" "likes" "mouse" "+"))
If something visits the dog then it likes the mouse.
((("something" "visits" "dog" "+")) -> ("something" "likes" "mouse" "+"))
If something needs the squirrel and the squirrel does not need the dog then the squirrel likes the mouse.
((("something" "needs" "squirrel" "+") ("squirrel" "needs" "dog" "~")) -> ("squirrel" "likes" "mouse" "+"))
If something likes the mouse and it likes the squirrel then the squirrel likes the dog.
((("something" "likes" "mouse" "+") ("something" "likes" "squirrel" "+")) -> ("squirrel" "likes" "dog" "+"))
If something likes the squirrel then it visits the mouse.
((("something" "likes" "squirrel" "+")) -> ("something" "visits" "mouse" "+"))
If something needs the squirrel then the squirrel does not need the mouse.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "needs" "mouse" "-"))
If something visits the squirrel and the squirrel does not visit the mouse then the squirrel needs the mouse.
((("something" "visits" "squirrel" "+") ("squirrel" "visits" "mouse" "~")) -> ("squirrel" "needs" "mouse" "+"))
The mouse is not kind.
True
1
proof
[(triple2)]
("mouse" "is" "kind" "-")
triple2
The dog does not like the squirrel.
False
1
inv-proof
[(triple1)]
("dog" "likes" "squirrel" "-")
triple1
The dog visits the mouse.
True
2
proof
[(((triple1) -> rule6))]
("dog" "visits" "mouse" "+")
((triple1) -> (rule6 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The dog does not visit the mouse.
False
2
inv-proof
[(((triple1) -> rule6))]
("dog" "visits" "mouse" "-")
((triple1) -> (rule6 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The dog likes the mouse.
True
3
proof
[(((((triple1) -> rule6)) -> rule2))]
("dog" "likes" "mouse" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The dog does not like the mouse.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule2))]
("dog" "likes" "mouse" "-")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The squirrel likes the dog.
True
5
proof
[(((((((triple1) -> rule6)) -> rule2) triple1) -> rule5))]
("squirrel" "likes" "dog" "+")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3
The squirrel does not like the dog.
False
5
inv-proof
[(((((((triple1) -> rule6)) -> rule2) triple1) -> rule5))]
("squirrel" "likes" "dog" "-")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3
The dog does not need the squirrel.
Unknown
inv-rconc
[@1: The dog needs the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "needs" "squirrel" "-")
The squirrel needs the mouse.
Unknown
rconc
[@1: The squirrel needs the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "needs" "mouse" "+")
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The squirrel visits the mouse.
Unknown
rconc
[@1: The squirrel visits the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "visits" "mouse" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The dog likes the squirrel.[(triple1)] The mouse is not kind.[(triple2)] The squirrel needs the dog.[(triple3)] @1: The dog visits the mouse.[(((triple1) -> rule6))] @2: The dog likes the mouse.[(((((triple1) -> rule6)) -> rule2))] @3: The squirrel likes the dog.[(((((((triple1) -> rule6)) -> rule2) triple1) -> rule5))]
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple1
The mouse is not kind.
("mouse" "is" "kind" "-")
triple2
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple3
The dog visits the mouse.
("dog" "visits" "mouse" "+")
((triple1) -> (rule6 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int3