The cat likes the squirrel. The mouse chases the squirrel. The squirrel likes the mouse. If something is nice then it likes the cat. If something needs the squirrel then it needs the mouse. If something likes the squirrel then the squirrel is nice. If something needs the mouse then the mouse needs the squirrel. If something likes the cat then the cat chases the mouse. If something likes the cat and it does not need the mouse then it does not chase the cat.
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
If something is nice then it likes the cat.
((("something" "is" "nice" "+")) -> ("something" "likes" "cat" "+"))
If something needs the squirrel then it needs the mouse.
((("something" "needs" "squirrel" "+")) -> ("something" "needs" "mouse" "+"))
If something likes the squirrel then the squirrel is nice.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "is" "nice" "+"))
If something needs the mouse then the mouse needs the squirrel.
((("something" "needs" "mouse" "+")) -> ("mouse" "needs" "squirrel" "+"))
If something likes the cat then the cat chases the mouse.
((("something" "likes" "cat" "+")) -> ("cat" "chases" "mouse" "+"))
If something likes the cat and it does not need the mouse then it does not chase the cat.
((("something" "likes" "cat" "+") ("something" "needs" "mouse" "~")) -> ("something" "chases" "cat" "-"))
The cat likes the squirrel.
True
1
proof
[(triple1)]
("cat" "likes" "squirrel" "+")
triple1
The cat does not like the squirrel.
False
1
inv-proof
[(triple1)]
("cat" "likes" "squirrel" "-")
triple1
The squirrel is nice.
True
2
proof
[(((triple1) -> rule3))]
("squirrel" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("squirrel" "is" "nice" "-")
((triple1) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel likes the cat.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("squirrel" "likes" "cat" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel does not like the cat.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("squirrel" "likes" "cat" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The cat chases the mouse.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule5))]
("cat" "chases" "mouse" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
The cat does not chase the mouse.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule5))]
("cat" "chases" "mouse" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
The cat does not need the mouse.
Unknown
inv-rconc
[@1: The cat needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "needs" "mouse" "-")
The cat likes the cat.
Unknown
rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "cat" "+")
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 mouse needs the squirrel.
Unknown
rconc
[@2: The mouse needs the squirrel.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("mouse" "needs" "squirrel" "+")
The cat does not like the mouse.
Unknown
inv-random
[@0: The cat likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "mouse" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The cat needs the squirrel.
Unknown
random
[@0: The cat needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "squirrel" "+")
@0: The cat likes the squirrel.[(triple1)] The mouse chases the squirrel.[(triple2)] The squirrel likes the mouse.[(triple3)] @1: The squirrel is nice.[(((triple1) -> rule3))] @2: The squirrel likes the cat.[(((((triple1) -> rule3)) -> rule1))] @3: The cat chases the mouse.[(((((((triple1) -> rule3)) -> rule1)) -> rule5))]
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple1
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple2
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple3
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3