The cat is cold. The dog needs the mouse. The mouse likes the dog. The squirrel eats the mouse. If something eats the mouse then it likes the squirrel. If something is rough and it eats the squirrel then the squirrel likes the mouse. If something likes the squirrel then the squirrel eats the cat.
The cat is cold.
("cat" "is" "cold" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
If something eats the mouse then it likes the squirrel.
((("something" "eats" "mouse" "+")) -> ("something" "likes" "squirrel" "+"))
If something is rough and it eats the squirrel then the squirrel likes the mouse.
((("something" "is" "rough" "+") ("something" "eats" "squirrel" "+")) -> ("squirrel" "likes" "mouse" "+"))
If something likes the squirrel then the squirrel eats the cat.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "eats" "cat" "+"))
The cat is cold.
True
1
proof
[(triple1)]
("cat" "is" "cold" "+")
triple1
The cat is not cold.
False
1
inv-proof
[(triple1)]
("cat" "is" "cold" "-")
triple1
The squirrel likes the squirrel.
True
2
proof
[(((triple4) -> rule1))]
("squirrel" "likes" "squirrel" "+")
((triple4) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel does not like the squirrel.
False
2
inv-proof
[(((triple4) -> rule1))]
("squirrel" "likes" "squirrel" "-")
((triple4) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel eats the cat.
True
3
proof
[(((((triple4) -> rule1)) -> rule3))]
("squirrel" "eats" "cat" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int2
The squirrel does not eat the cat.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule3))]
("squirrel" "eats" "cat" "-")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int2
The cat does not like the squirrel.
Unknown
inv-rconc
[@1: The cat likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "squirrel" "-")
The mouse likes the squirrel.
Unknown
rconc
[@1: The mouse likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "squirrel" "+")
The dog does not like the squirrel.
Unknown
inv-rconc
[@1: The dog likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "likes" "squirrel" "-")
The dog likes the mouse.
Unknown
random
[@0: The dog likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "mouse" "+")
The dog does not like the cat.
Unknown
inv-random
[@0: The dog likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cat" "-")
The squirrel needs the mouse.
Unknown
random
[@0: The squirrel needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "mouse" "+")
@0: The cat is cold.[(triple1)] The dog needs the mouse.[(triple2)] The mouse likes the dog.[(triple3)] The squirrel eats the mouse.[(triple4)] @1: The squirrel likes the squirrel.[(((triple4) -> rule1))] @2: The squirrel eats the cat.[(((((triple4) -> rule1)) -> rule3))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple3
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple4
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((triple4) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int2