The dog likes the mouse. The mouse needs the squirrel. The squirrel chases the mouse. If the mouse likes the dog then the mouse needs the squirrel. If something is cold and it needs the dog then it likes the mouse. If something needs the dog then the dog likes the squirrel. If something chases the mouse and the mouse likes the squirrel then the mouse needs the squirrel. If something chases the squirrel then it is cold. If something needs the squirrel then the squirrel needs the dog. If something needs the dog then the dog is cold. If something chases the squirrel and it likes the mouse then it likes the squirrel.
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
If the mouse likes the dog then the mouse needs the squirrel.
((("mouse" "likes" "dog" "+")) -> ("mouse" "needs" "squirrel" "+"))
If something is cold and it needs the dog then it likes the mouse.
((("something" "is" "cold" "+") ("something" "needs" "dog" "+")) -> ("something" "likes" "mouse" "+"))
If something needs the dog then the dog likes the squirrel.
((("something" "needs" "dog" "+")) -> ("dog" "likes" "squirrel" "+"))
If something chases the mouse and the mouse likes the squirrel then the mouse needs the squirrel.
((("something" "chases" "mouse" "+") ("mouse" "likes" "squirrel" "+")) -> ("mouse" "needs" "squirrel" "+"))
If something chases the squirrel then it is cold.
((("something" "chases" "squirrel" "+")) -> ("something" "is" "cold" "+"))
If something needs the squirrel then the squirrel needs the dog.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "needs" "dog" "+"))
If something needs the dog then the dog is cold.
((("something" "needs" "dog" "+")) -> ("dog" "is" "cold" "+"))
If something chases the squirrel and it likes the mouse then it likes the squirrel.
((("something" "chases" "squirrel" "+") ("something" "likes" "mouse" "+")) -> ("something" "likes" "squirrel" "+"))
The mouse needs the squirrel.
True
1
proof
[(triple2)]
("mouse" "needs" "squirrel" "+")
triple2
The squirrel does not chase the mouse.
False
1
inv-proof
[(triple3)]
("squirrel" "chases" "mouse" "-")
triple3
The squirrel needs the dog.
True
2
proof
[(((triple2) -> rule6))]
("squirrel" "needs" "dog" "+")
((triple2) -> (rule6 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
The squirrel does not need the dog.
False
2
inv-proof
[(((triple2) -> rule6))]
("squirrel" "needs" "dog" "-")
((triple2) -> (rule6 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
The dog likes the squirrel.
True
3
proof
[(((((triple2) -> rule6)) -> rule3))]
("dog" "likes" "squirrel" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int2
The dog does not like the squirrel.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule3))]
("dog" "likes" "squirrel" "-")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int2
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "cold" "-")
The mouse likes the squirrel.
Unknown
rconc
[@1: The mouse likes the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "likes" "squirrel" "+")
The mouse does not like the mouse.
Unknown
inv-rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
The dog does not chase the squirrel.
Unknown
inv-random
[@0: The dog chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "squirrel" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
@0: The dog likes the mouse.[(triple1)] The mouse needs the squirrel.[(triple2)] The squirrel chases the mouse.[(triple3)] @1: The squirrel needs the dog.[(((triple2) -> rule6))] @2: The dog is cold.[(((((triple2) -> rule6)) -> rule7))] The dog likes the squirrel.[(((((triple2) -> rule6)) -> rule3))]
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple2
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple3
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
((triple2) -> (rule6 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
((((triple2) -> (rule6 % int2))) -> (rule7 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int2
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int2