The cat chases the lion. The cat does not chase the mouse. The cat sees the tiger. The lion is nice. The mouse likes the cat. The tiger chases the lion. The tiger likes the mouse. If someone sees the mouse and they are rough then the mouse sees the tiger. If someone sees the lion and the lion likes the tiger then they are nice. If someone likes the tiger then they are nice. If someone is rough then they see the mouse. If someone likes the lion then the lion sees the mouse. If someone chases the tiger and the tiger sees the mouse then the mouse is not big. If someone sees the lion then the lion likes the tiger. If someone likes the lion and they chase the cat then they do not see the lion. If someone sees the tiger and the tiger chases the lion then they are rough.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The lion is nice.
("lion" "is" "nice" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If someone sees the mouse and they are rough then the mouse sees the tiger.
((("someone" "sees" "mouse" "+") ("someone" "is" "rough" "+")) -> ("mouse" "sees" "tiger" "+"))
If someone sees the lion and the lion likes the tiger then they are nice.
((("someone" "sees" "lion" "+") ("lion" "likes" "tiger" "+")) -> ("someone" "is" "nice" "+"))
If someone likes the tiger then they are nice.
((("someone" "likes" "tiger" "+")) -> ("someone" "is" "nice" "+"))
If someone is rough then they see the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "mouse" "+"))
If someone likes the lion then the lion sees the mouse.
((("someone" "likes" "lion" "+")) -> ("lion" "sees" "mouse" "+"))
If someone chases the tiger and the tiger sees the mouse then the mouse is not big.
((("someone" "chases" "tiger" "+") ("tiger" "sees" "mouse" "+")) -> ("mouse" "is" "big" "-"))
If someone sees the lion then the lion likes the tiger.
((("someone" "sees" "lion" "+")) -> ("lion" "likes" "tiger" "+"))
If someone likes the lion and they chase the cat then they do not see the lion.
((("someone" "likes" "lion" "+") ("someone" "chases" "cat" "+")) -> ("someone" "sees" "lion" "-"))
If someone sees the tiger and the tiger chases the lion then they are rough.
((("someone" "sees" "tiger" "+") ("tiger" "chases" "lion" "+")) -> ("someone" "is" "rough" "+"))
The cat chases the lion.
True
1
proof
[(triple1)]
("cat" "chases" "lion" "+")
triple1
The mouse does not like the cat.
False
1
inv-proof
[(triple5)]
("mouse" "likes" "cat" "-")
triple5
The cat is rough.
True
3
proof
[(((triple3 triple6) -> rule9))]
("cat" "is" "rough" "+")
((triple3 triple6) -> (rule9 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is not rough.
False
3
inv-proof
[(((triple3 triple6) -> rule9))]
("cat" "is" "rough" "-")
((triple3 triple6) -> (rule9 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat sees the mouse.
True
4
proof
[(((((triple3 triple6) -> rule9)) -> rule4))]
("cat" "sees" "mouse" "+")
((((triple3 triple6) -> (rule9 % int2))) -> (rule4 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat does not see the mouse.
False
4
inv-proof
[(((((triple3 triple6) -> rule9)) -> rule4))]
("cat" "sees" "mouse" "-")
((((triple3 triple6) -> (rule9 % int2))) -> (rule4 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The mouse sees the tiger.
True
8
proof
[(((((((triple3 triple6) -> rule9)) -> rule4) ((triple3 triple6) -> rule9)) -> rule1))]
("mouse" "sees" "tiger" "+")
((((((triple3 triple6) -> (rule9 % int3))) -> (rule4 % int2)) ((triple3 triple6) -> (rule9 % int3))) -> (rule1 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The mouse does not see the tiger.
False
8
inv-proof
[(((((((triple3 triple6) -> rule9)) -> rule4) ((triple3 triple6) -> rule9)) -> rule1))]
("mouse" "sees" "tiger" "-")
((((((triple3 triple6) -> (rule9 % int3))) -> (rule4 % int2)) ((triple3 triple6) -> (rule9 % int3))) -> (rule1 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The mouse is rough.
True
10
proof
[(((((((((triple3 triple6) -> rule9)) -> rule4) ((triple3 triple6) -> rule9)) -> rule1) triple6) -> rule9))]
("mouse" "is" "rough" "+")
((((((((triple3 triple6) -> (rule9 % int4))) -> (rule4 % int3)) ((triple3 triple6) -> (rule9 % int4))) -> (rule1 % int2)) triple6) -> (rule9 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
The mouse is not rough.
False
10
inv-proof
[(((((((((triple3 triple6) -> rule9)) -> rule4) ((triple3 triple6) -> rule9)) -> rule1) triple6) -> rule9))]
("mouse" "is" "rough" "-")
((((((((triple3 triple6) -> (rule9 % int4))) -> (rule4 % int3)) ((triple3 triple6) -> (rule9 % int4))) -> (rule1 % int2)) triple6) -> (rule9 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
The mouse sees the mouse.
True
11
proof
[(((((((((((triple3 triple6) -> rule9)) -> rule4) ((triple3 triple6) -> rule9)) -> rule1) triple6) -> rule9)) -> rule4))]
("mouse" "sees" "mouse" "+")
((((((((((triple3 triple6) -> (rule9 % int5))) -> (rule4 % int4)) ((triple3 triple6) -> (rule9 % int5))) -> (rule1 % int3)) triple6) -> (rule9 % int2))) -> (rule4 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int4
The cat is rough.
("cat" "is" "rough" "+")
int5
The mouse does not see the mouse.
False
11
inv-proof
[(((((((((((triple3 triple6) -> rule9)) -> rule4) ((triple3 triple6) -> rule9)) -> rule1) triple6) -> rule9)) -> rule4))]
("mouse" "sees" "mouse" "-")
((((((((((triple3 triple6) -> (rule9 % int5))) -> (rule4 % int4)) ((triple3 triple6) -> (rule9 % int5))) -> (rule1 % int3)) triple6) -> (rule9 % int2))) -> (rule4 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int4
The cat is rough.
("cat" "is" "rough" "+")
int5
The mouse is not nice.
Unknown
inv-rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "nice" "-")
The lion sees the mouse.
Unknown
rconc
[@2: The lion sees the mouse.[CWA. Example of deepest failure = (rule4 <- rule9 <- FAIL)]]
("lion" "sees" "mouse" "+")
The tiger is not rough.
Unknown
inv-rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("tiger" "is" "rough" "-")
The lion is rough.
Unknown
rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("lion" "is" "rough" "+")
The tiger is not nice.
Unknown
inv-rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "nice" "-")
The lion likes the tiger.
Unknown
rconc
[@1: The lion likes the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "likes" "tiger" "+")
The mouse does not chase the tiger.
Unknown
inv-random
[@0: The mouse chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "tiger" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The lion chases the tiger.
Unknown
random
[@0: The lion chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "tiger" "+")
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 cat likes the lion.
Unknown
random
[@0: The cat likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "lion" "+")
@0: The cat chases the lion.[(triple1)] The cat does not chase the mouse.[(triple2)] The cat sees the tiger.[(triple3)] The lion is nice.[(triple4)] The mouse likes the cat.[(triple5)] The tiger chases the lion.[(triple6)] The tiger likes the mouse.[(triple7)] @1: The cat is rough.[(((triple3 triple6) -> rule9))] @2: The cat sees the mouse.[(((((triple3 triple6) -> rule9)) -> rule4))] @3: The mouse sees the tiger.[(((((((triple3 triple6) -> rule9)) -> rule4) ((triple3 triple6) -> rule9)) -> rule1))] @4: The mouse is rough.[(((((((((triple3 triple6) -> rule9)) -> rule4) ((triple3 triple6) -> rule9)) -> rule1) triple6) -> rule9))] @5: The mouse sees the mouse.[(((((((((((triple3 triple6) -> rule9)) -> rule4) ((triple3 triple6) -> rule9)) -> rule1) triple6) -> rule9)) -> rule4))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
triple2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple5
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple6
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple7
The cat is rough.
("cat" "is" "rough" "+")
((triple3 triple6) -> (rule9 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
((((triple3 triple6) -> (rule9 % int2))) -> (rule4 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
((((((triple3 triple6) -> (rule9 % int3))) -> (rule4 % int2)) ((triple3 triple6) -> (rule9 % int3))) -> (rule1 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
((((((((triple3 triple6) -> (rule9 % int4))) -> (rule4 % int3)) ((triple3 triple6) -> (rule9 % int4))) -> (rule1 % int2)) triple6) -> (rule9 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((((((((triple3 triple6) -> (rule9 % int5))) -> (rule4 % int4)) ((triple3 triple6) -> (rule9 % int5))) -> (rule1 % int3)) triple6) -> (rule9 % int2))) -> (rule4 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int4
The cat is rough.
("cat" "is" "rough" "+")
int5