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