The cat eats the lion. The lion likes the mouse. The mouse does not like the lion. If something likes the mouse then the mouse likes the cat. If something eats the cat then the cat likes the mouse. If the cat is green and the cat is not kind then the cat chases the lion. If the cat is rough and the cat chases the mouse then the cat does not eat the mouse. If the cat chases the lion then the cat eats the mouse. If something eats the lion and it likes the cat then the lion is not big. If something likes the cat then it is rough. If something is rough then it chases the lion.
The cat eats the lion.
("cat" "eats" "lion" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse does not like the lion.
("mouse" "likes" "lion" "-")
If something likes the mouse then the mouse likes the cat.
((("something" "likes" "mouse" "+")) -> ("mouse" "likes" "cat" "+"))
If something eats the cat then the cat likes the mouse.
((("something" "eats" "cat" "+")) -> ("cat" "likes" "mouse" "+"))
If the cat is green and the cat is not kind then the cat chases the lion.
((("cat" "is" "green" "+") ("cat" "is" "kind" "~")) -> ("cat" "chases" "lion" "+"))
If the cat is rough and the cat chases the mouse then the cat does not eat the mouse.
((("cat" "is" "rough" "+") ("cat" "chases" "mouse" "+")) -> ("cat" "eats" "mouse" "-"))
If the cat chases the lion then the cat eats the mouse.
((("cat" "chases" "lion" "+")) -> ("cat" "eats" "mouse" "+"))
If something eats the lion and it likes the cat then the lion is not big.
((("something" "eats" "lion" "+") ("something" "likes" "cat" "+")) -> ("lion" "is" "big" "-"))
If something likes the cat then it is rough.
((("something" "likes" "cat" "+")) -> ("something" "is" "rough" "+"))
If something is rough then it chases the lion.
((("something" "is" "rough" "+")) -> ("something" "chases" "lion" "+"))
The mouse does not like the lion.
True
1
proof
[(triple3)]
("mouse" "likes" "lion" "-")
triple3
The lion does not like the mouse.
False
1
inv-proof
[(triple2)]
("lion" "likes" "mouse" "-")
triple2
The mouse likes the cat.
True
2
proof
[(((triple2) -> rule1))]
("mouse" "likes" "cat" "+")
((triple2) -> (rule1 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The mouse does not like the cat.
False
2
inv-proof
[(((triple2) -> rule1))]
("mouse" "likes" "cat" "-")
((triple2) -> (rule1 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The mouse is rough.
True
3
proof
[(((((triple2) -> rule1)) -> rule7))]
("mouse" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The mouse is not rough.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule7))]
("mouse" "is" "rough" "-")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The mouse chases the lion.
True
4
proof
[(((((((triple2) -> rule1)) -> rule7)) -> rule8))]
("mouse" "chases" "lion" "+")
((((((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int3
The mouse does not chase the lion.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule7)) -> rule8))]
("mouse" "chases" "lion" "-")
((((((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int3
The cat is not rough.
Unknown
inv-rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "rough" "-")
The cat chases the lion.
Unknown
rconc
[@2: The cat chases the lion.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("cat" "chases" "lion" "+")
The cat does not like the mouse.
Unknown
inv-rconc
[@1: The cat likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "likes" "mouse" "-")
The lion is rough.
Unknown
rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "is" "rough" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The cat chases the mouse.
Unknown
random
[@0: The cat chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "mouse" "+")
@0: The cat eats the lion.[(triple1)] The lion likes the mouse.[(triple2)] The mouse does not like the lion.[(triple3)] @1: The mouse likes the cat.[(((triple2) -> rule1))] @2: The mouse is rough.[(((((triple2) -> rule1)) -> rule7))] @3: The mouse chases the lion.[(((((((triple2) -> rule1)) -> rule7)) -> rule8))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple2
The mouse does not like the lion.
("mouse" "likes" "lion" "-")
triple3
The mouse likes the cat.
("mouse" "likes" "cat" "+")
((triple2) -> (rule1 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
((((((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int3