The cat needs the lion. The lion visits the cat. The mouse visits the cat. Rough things are cold. If the cat is cold and the cat visits the mouse then the cat visits the lion. If the lion visits the mouse and the mouse is cold then the mouse likes the lion. If something likes the mouse then it likes the cat. If something visits the cat then the cat is kind. If something is kind then it likes the cat. If something visits the cat then the cat visits the lion. If something likes the lion then it needs the cat.
The cat needs the lion.
("cat" "needs" "lion" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
Rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If the cat is cold and the cat visits the mouse then the cat visits the lion.
((("cat" "is" "cold" "+") ("cat" "visits" "mouse" "+")) -> ("cat" "visits" "lion" "+"))
If the lion visits the mouse and the mouse is cold then the mouse likes the lion.
((("lion" "visits" "mouse" "+") ("mouse" "is" "cold" "+")) -> ("mouse" "likes" "lion" "+"))
If something likes the mouse then it likes the cat.
((("something" "likes" "mouse" "+")) -> ("something" "likes" "cat" "+"))
If something visits the cat then the cat is kind.
((("something" "visits" "cat" "+")) -> ("cat" "is" "kind" "+"))
If something is kind then it likes the cat.
((("something" "is" "kind" "+")) -> ("something" "likes" "cat" "+"))
If something visits the cat then the cat visits the lion.
((("something" "visits" "cat" "+")) -> ("cat" "visits" "lion" "+"))
If something likes the lion then it needs the cat.
((("something" "likes" "lion" "+")) -> ("something" "needs" "cat" "+"))
The cat needs the lion.
True
1
proof
[(triple1)]
("cat" "needs" "lion" "+")
triple1
The mouse does not visit the cat.
False
1
inv-proof
[(triple3)]
("mouse" "visits" "cat" "-")
triple3
The cat is kind.
True
2
proof
[(((triple2) -> rule5) OR ((triple3) -> rule5))]
("cat" "is" "kind" "+")
((triple2) -> (rule5 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((triple3) -> (rule5 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is not kind.
False
2
inv-proof
[(((triple2) -> rule5) OR ((triple3) -> rule5))]
("cat" "is" "kind" "-")
((triple2) -> (rule5 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((triple3) -> (rule5 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat likes the cat.
True
3
proof
[(((((triple2) -> rule5)) -> rule6) OR ((((triple3) -> rule5)) -> rule6))]
("cat" "likes" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat does not like the cat.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule6) OR ((((triple3) -> rule5)) -> rule6))]
("cat" "likes" "cat" "-")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "cold" "-")
The lion is cold.
Unknown
rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "cold" "+")
The mouse does not like the cat.
Unknown
inv-rconc
[@1: The mouse likes the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "likes" "cat" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The cat likes the lion.
Unknown
random
[@0: The cat likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "lion" "+")
@0: The cat needs the lion.[(triple1)] The lion visits the cat.[(triple2)] The mouse visits the cat.[(triple3)] @1: The cat is kind.[(((triple2) -> rule5) OR ((triple3) -> rule5))] The cat visits the lion.[(((triple2) -> rule7) OR ((triple3) -> rule7))] @2: The cat likes the cat.[(((((triple2) -> rule5)) -> rule6) OR ((((triple3) -> rule5)) -> rule6))]
The cat needs the lion.
("cat" "needs" "lion" "+")
triple1
The lion visits the cat.
("lion" "visits" "cat" "+")
triple2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple3
The cat is kind.
("cat" "is" "kind" "+")
((triple2) -> (rule5 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((triple3) -> (rule5 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
((triple2) -> (rule7 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
((triple3) -> (rule7 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2