The cat eats the lion. The cat likes the lion. The cat visits the mouse. The lion eats the cat. The lion is blue. The mouse eats the cat. The mouse eats the lion. The mouse is kind. The mouse is rough. The mouse visits the lion. If something likes the mouse and it visits the lion then the mouse visits the cat. If something visits the mouse then it likes the mouse. If something likes the mouse and it visits the cat then the mouse is red. If something is red then it visits the cat. If something likes the mouse then it visits the cat. If something is blue and it likes the cat then the cat likes the mouse.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is blue.
("lion" "is" "blue" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If something likes the mouse and it visits the lion then the mouse visits the cat.
((("something" "likes" "mouse" "+") ("something" "visits" "lion" "+")) -> ("mouse" "visits" "cat" "+"))
If something visits the mouse then it likes the mouse.
((("something" "visits" "mouse" "+")) -> ("something" "likes" "mouse" "+"))
If something likes the mouse and it visits the cat then the mouse is red.
((("something" "likes" "mouse" "+") ("something" "visits" "cat" "+")) -> ("mouse" "is" "red" "+"))
If something is red then it visits the cat.
((("something" "is" "red" "+")) -> ("something" "visits" "cat" "+"))
If something likes the mouse then it visits the cat.
((("something" "likes" "mouse" "+")) -> ("something" "visits" "cat" "+"))
If something is blue and it likes the cat then the cat likes the mouse.
((("something" "is" "blue" "+") ("something" "likes" "cat" "+")) -> ("cat" "likes" "mouse" "+"))
The cat eats the lion.
True
1
proof
[(triple1)]
("cat" "eats" "lion" "+")
triple1
The mouse is not kind.
False
1
inv-proof
[(triple8)]
("mouse" "is" "kind" "-")
triple8
The cat likes the mouse.
True
2
proof
[(((triple3) -> rule2))]
("cat" "likes" "mouse" "+")
((triple3) -> (rule2 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat does not like the mouse.
False
2
inv-proof
[(((triple3) -> rule2))]
("cat" "likes" "mouse" "-")
((triple3) -> (rule2 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat visits the cat.
True
3
proof
[(((((triple3) -> rule2)) -> rule5))]
("cat" "visits" "cat" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int2
The cat does not visit the cat.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule5))]
("cat" "visits" "cat" "-")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int2
The mouse is red.
True
6
proof
[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule5)) -> rule3))]
("mouse" "is" "red" "+")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int3
The mouse is not red.
False
6
inv-proof
[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule5)) -> rule3))]
("mouse" "is" "red" "-")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int3
The lion does not like the mouse.
Unknown
inv-rconc
[@1: The lion likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "likes" "mouse" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The lion does not visit the cat.
Unknown
inv-rconc
[@2: The lion visits the cat.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("lion" "visits" "cat" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The cat visits the lion.
Unknown
random
[@0: The cat visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "lion" "+")
@0: The cat eats the lion.[(triple1)] The cat likes the lion.[(triple2)] The cat visits the mouse.[(triple3)] The lion eats the cat.[(triple4)] The lion is blue.[(triple5)] The mouse eats the cat.[(triple6)] The mouse eats the lion.[(triple7)] The mouse is kind.[(triple8)] The mouse is rough.[(triple9)] The mouse visits the lion.[(triple10)] @1: The cat likes the mouse.[(((triple3) -> rule2))] @2: The cat visits the cat.[(((((triple3) -> rule2)) -> rule5))] @3: The mouse is red.[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule5)) -> rule3))] @4: The mouse visits the cat.[(((((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule5)) -> rule3)) -> rule4))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat likes the lion.
("cat" "likes" "lion" "+")
triple2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple3
The lion eats the cat.
("lion" "eats" "cat" "+")
triple4
The lion is blue.
("lion" "is" "blue" "+")
triple5
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple6
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple7
The mouse is kind.
("mouse" "is" "kind" "+")
triple8
The mouse is rough.
("mouse" "is" "rough" "+")
triple9
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple10
The cat likes the mouse.
("cat" "likes" "mouse" "+")
((triple3) -> (rule2 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int3
The mouse visits the cat.
("mouse" "visits" "cat" "+")
((((((triple3) -> (rule2 % int4)) ((((triple3) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The cat visits the cat.
("cat" "visits" "cat" "+")
int3
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int4