The cat chases the rabbit. The cat is green. The cat is nice. The lion chases the rabbit. The lion is nice. The lion needs the cat. The lion needs the rabbit. The mouse chases the cat. The mouse is kind. The mouse needs the lion. The rabbit is nice. The rabbit likes the lion. The rabbit needs the cat. The rabbit needs the mouse. If something chases the cat and it likes the cat then it is rough. If something is green and it likes the mouse then it chases the mouse. If something needs the mouse and the mouse is green then it chases the mouse. If the rabbit is kind then the rabbit chases the mouse. If the cat is nice then the cat likes the mouse. If something is rough then it is nice. If something chases the mouse then the mouse likes the cat.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is nice.
("cat" "is" "nice" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If something chases the cat and it likes the cat then it is rough.
((("something" "chases" "cat" "+") ("something" "likes" "cat" "+")) -> ("something" "is" "rough" "+"))
If something is green and it likes the mouse then it chases the mouse.
((("something" "is" "green" "+") ("something" "likes" "mouse" "+")) -> ("something" "chases" "mouse" "+"))
If something needs the mouse and the mouse is green then it chases the mouse.
((("something" "needs" "mouse" "+") ("mouse" "is" "green" "+")) -> ("something" "chases" "mouse" "+"))
If the rabbit is kind then the rabbit chases the mouse.
((("rabbit" "is" "kind" "+")) -> ("rabbit" "chases" "mouse" "+"))
If the cat is nice then the cat likes the mouse.
((("cat" "is" "nice" "+")) -> ("cat" "likes" "mouse" "+"))
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something chases the mouse then the mouse likes the cat.
((("something" "chases" "mouse" "+")) -> ("mouse" "likes" "cat" "+"))
The mouse needs the lion.
True
1
proof
[(triple10)]
("mouse" "needs" "lion" "+")
triple10
The lion does not chase the rabbit.
False
1
inv-proof
[(triple4)]
("lion" "chases" "rabbit" "-")
triple4
The cat likes the mouse.
True
2
proof
[(((triple3) -> rule5))]
("cat" "likes" "mouse" "+")
((triple3) -> (rule5 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat does not like the mouse.
False
2
inv-proof
[(((triple3) -> rule5))]
("cat" "likes" "mouse" "-")
((triple3) -> (rule5 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat chases the mouse.
True
4
proof
[(((triple2 ((triple3) -> rule5)) -> rule2))]
("cat" "chases" "mouse" "+")
((triple2 ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int2
The cat does not chase the mouse.
False
4
inv-proof
[(((triple2 ((triple3) -> rule5)) -> rule2))]
("cat" "chases" "mouse" "-")
((triple2 ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int2
The mouse likes the cat.
True
5
proof
[(((((triple2 ((triple3) -> rule5)) -> rule2)) -> rule7))]
("mouse" "likes" "cat" "+")
((((triple2 ((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int3
The mouse does not like the cat.
False
5
inv-proof
[(((((triple2 ((triple3) -> rule5)) -> rule2)) -> rule7))]
("mouse" "likes" "cat" "-")
((((triple2 ((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int3
The mouse is rough.
True
7
proof
[(((triple8 ((((triple2 ((triple3) -> rule5)) -> rule2)) -> rule7)) -> rule1))]
("mouse" "is" "rough" "+")
((triple8 ((((triple2 ((triple3) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int4
The mouse is not rough.
False
7
inv-proof
[(((triple8 ((((triple2 ((triple3) -> rule5)) -> rule2)) -> rule7)) -> rule1))]
("mouse" "is" "rough" "-")
((triple8 ((((triple2 ((triple3) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int4
The mouse is nice.
True
8
proof
[(((((triple8 ((((triple2 ((triple3) -> rule5)) -> rule2)) -> rule7)) -> rule1)) -> rule6))]
("mouse" "is" "nice" "+")
((((triple8 ((((triple2 ((triple3) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int3
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int4
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int5
The mouse is not nice.
False
8
inv-proof
[(((((triple8 ((((triple2 ((triple3) -> rule5)) -> rule2)) -> rule7)) -> rule1)) -> rule6))]
("mouse" "is" "nice" "-")
((((triple8 ((((triple2 ((triple3) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int3
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int4
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int5
The lion does not chase the mouse.
Unknown
inv-rconc
[@1: The lion chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "chases" "mouse" "-")
The mouse chases the mouse.
Unknown
rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "chases" "mouse" "+")
The rabbit does not chase the mouse.
Unknown
inv-rconc
[@1: The rabbit chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "chases" "mouse" "-")
The cat is rough.
Unknown
rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "rough" "+")
The rabbit is not rough.
Unknown
inv-rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "rough" "-")
The lion is rough.
Unknown
rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "rough" "+")
The rabbit does not like the cat.
Unknown
inv-random
[@0: The rabbit likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "cat" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The lion does not need the mouse.
Unknown
inv-random
[@0: The lion needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "mouse" "-")
The lion chases the cat.
Unknown
random
[@0: The lion chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cat" "+")
@0: The cat chases the rabbit.[(triple1)] The cat is green.[(triple2)] The cat is nice.[(triple3)] The lion chases the rabbit.[(triple4)] The lion is nice.[(triple5)] The lion needs the cat.[(triple6)] The lion needs the rabbit.[(triple7)] The mouse chases the cat.[(triple8)] The mouse is kind.[(triple9)] The mouse needs the lion.[(triple10)] The rabbit is nice.[(triple11)] The rabbit likes the lion.[(triple12)] The rabbit needs the cat.[(triple13)] The rabbit needs the mouse.[(triple14)] @1: The cat likes the mouse.[(((triple3) -> rule5))] @2: The cat chases the mouse.[(((triple2 ((triple3) -> rule5)) -> rule2))] @3: The mouse likes the cat.[(((((triple2 ((triple3) -> rule5)) -> rule2)) -> rule7))] @4: The mouse is rough.[(((triple8 ((((triple2 ((triple3) -> rule5)) -> rule2)) -> rule7)) -> rule1))] @5: The mouse is nice.[(((((triple8 ((((triple2 ((triple3) -> rule5)) -> rule2)) -> rule7)) -> rule1)) -> rule6))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple4
The lion is nice.
("lion" "is" "nice" "+")
triple5
The lion needs the cat.
("lion" "needs" "cat" "+")
triple6
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple7
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple8
The mouse is kind.
("mouse" "is" "kind" "+")
triple9
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple10
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple11
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple12
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple13
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple14
The cat likes the mouse.
("cat" "likes" "mouse" "+")
((triple3) -> (rule5 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((triple2 ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
((((triple2 ((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
((triple8 ((((triple2 ((triple3) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int4
The mouse is nice.
("mouse" "is" "nice" "+")
((((triple8 ((((triple2 ((triple3) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int3
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int4
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int5