The dog likes the mouse. The mouse is cold. If someone likes the dog then the dog chases the mouse. If someone likes the mouse then they like the dog.
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
If someone likes the dog then the dog chases the mouse.
((("someone" "likes" "dog" "+")) -> ("dog" "chases" "mouse" "+"))
If someone likes the mouse then they like the dog.
((("someone" "likes" "mouse" "+")) -> ("someone" "likes" "dog" "+"))
The mouse is cold.
True
1
proof
[(triple2)]
("mouse" "is" "cold" "+")
triple2
The mouse is not cold.
False
1
inv-proof
[(triple2)]
("mouse" "is" "cold" "-")
triple2
The dog likes the dog.
True
2
proof
[(((triple1) -> rule2))]
("dog" "likes" "dog" "+")
((triple1) -> (rule2 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog does not like the dog.
False
2
inv-proof
[(((triple1) -> rule2))]
("dog" "likes" "dog" "-")
((triple1) -> (rule2 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog chases the mouse.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("dog" "chases" "mouse" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog does not chase the mouse.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("dog" "chases" "mouse" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The mouse does not like the dog.
Unknown
inv-rconc
[@1: The mouse likes the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "likes" "dog" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
@0: The dog likes the mouse.[(triple1)] The mouse is cold.[(triple2)] @1: The dog likes the dog.[(((triple1) -> rule2))] @2: The dog chases the mouse.[(((((triple1) -> rule2)) -> rule1))]
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple1
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The dog likes the dog.
("dog" "likes" "dog" "+")
((triple1) -> (rule2 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2