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