The cat likes the mouse. The lion is nice. The mouse is not kind. If something likes the lion and it sees the mouse then the mouse does not chase the lion. If something is kind then it likes the lion. If something likes the mouse then the mouse likes the cat. If something likes the cat then the cat is kind. If something likes the lion and the lion likes the mouse then it does not see the lion. If the cat is red and the lion does not like the cat then the lion is red.
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The lion is nice.
("lion" "is" "nice" "+")
The mouse is not kind.
("mouse" "is" "kind" "-")
If something likes the lion and it sees the mouse then the mouse does not chase the lion.
((("something" "likes" "lion" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "chases" "lion" "-"))
If something is kind then it likes the lion.
((("something" "is" "kind" "+")) -> ("something" "likes" "lion" "+"))
If something likes the mouse then the mouse likes the cat.
((("something" "likes" "mouse" "+")) -> ("mouse" "likes" "cat" "+"))
If something likes the cat then the cat is kind.
((("something" "likes" "cat" "+")) -> ("cat" "is" "kind" "+"))
If something likes the lion and the lion likes the mouse then it does not see the lion.
((("something" "likes" "lion" "+") ("lion" "likes" "mouse" "+")) -> ("something" "sees" "lion" "-"))
If the cat is red and the lion does not like the cat then the lion is red.
((("cat" "is" "red" "+") ("lion" "likes" "cat" "~")) -> ("lion" "is" "red" "+"))
The cat likes the mouse.
True
1
proof
[(triple1)]
("cat" "likes" "mouse" "+")
triple1
The mouse is kind.
False
1
inv-proof
[(triple3)]
("mouse" "is" "kind" "+")
triple3
The mouse likes the cat.
True
2
proof
[(((triple1) -> rule3))]
("mouse" "likes" "cat" "+")
((triple1) -> (rule3 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The mouse does not like the cat.
False
2
inv-proof
[(((triple1) -> rule3))]
("mouse" "likes" "cat" "-")
((triple1) -> (rule3 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The cat is kind.
True
3
proof
[(((((triple1) -> rule3)) -> rule4))]
("cat" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The cat is not kind.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule4))]
("cat" "is" "kind" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The lion does not like the lion.
Unknown
inv-rconc
[@1: The lion likes the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "likes" "lion" "-")
The lion is red.
Unknown
rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "red" "+")
The mouse does not like the lion.
Unknown
inv-rconc
[@1: The mouse likes the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "likes" "lion" "-")
The lion sees the cat.
Unknown
random
[@0: The lion sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cat" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
@0: The cat likes the mouse.[(triple1)] The lion is nice.[(triple2)] The mouse is not kind.[(triple3)] @1: The mouse likes the cat.[(((triple1) -> rule3))] @2: The cat is kind.[(((((triple1) -> rule3)) -> rule4))] @3: The cat likes the lion.[(((((((triple1) -> rule3)) -> rule4)) -> rule2))]
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple1
The lion is nice.
("lion" "is" "nice" "+")
triple2
The mouse is not kind.
("mouse" "is" "kind" "-")
triple3
The mouse likes the cat.
("mouse" "likes" "cat" "+")
((triple1) -> (rule3 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The cat likes the lion.
("cat" "likes" "lion" "+")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int3