The cat chases the tiger. The cat is big. The cat likes the rabbit. The rabbit is nice. The squirrel likes the rabbit. The squirrel sees the cat. The squirrel sees the tiger. The tiger is nice. The tiger is rough. The tiger likes the cat. If someone likes the tiger then the tiger sees the cat. If someone chases the rabbit then they see the squirrel. If the tiger sees the cat then the cat chases the rabbit. If someone sees the rabbit then the rabbit is big. If someone chases the tiger then the tiger sees the rabbit. If someone is big and they like the cat then the cat chases the rabbit. If someone likes the cat then they are kind. If someone chases the rabbit then the rabbit likes the tiger. If someone is kind then they are big.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is big.
("cat" "is" "big" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If someone likes the tiger then the tiger sees the cat.
((("someone" "likes" "tiger" "+")) -> ("tiger" "sees" "cat" "+"))
If someone chases the rabbit then they see the squirrel.
((("someone" "chases" "rabbit" "+")) -> ("someone" "sees" "squirrel" "+"))
If the tiger sees the cat then the cat chases the rabbit.
((("tiger" "sees" "cat" "+")) -> ("cat" "chases" "rabbit" "+"))
If someone sees the rabbit then the rabbit is big.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
If someone chases the tiger then the tiger sees the rabbit.
((("someone" "chases" "tiger" "+")) -> ("tiger" "sees" "rabbit" "+"))
If someone is big and they like the cat then the cat chases the rabbit.
((("someone" "is" "big" "+") ("someone" "likes" "cat" "+")) -> ("cat" "chases" "rabbit" "+"))
If someone likes the cat then they are kind.
((("someone" "likes" "cat" "+")) -> ("someone" "is" "kind" "+"))
If someone chases the rabbit then the rabbit likes the tiger.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "likes" "tiger" "+"))
If someone is kind then they are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
The cat likes the rabbit.
True
1
proof
[(triple3)]
("cat" "likes" "rabbit" "+")
triple3
The tiger is not nice.
False
1
inv-proof
[(triple8)]
("tiger" "is" "nice" "-")
triple8
The tiger is kind.
True
2
proof
[(((triple10) -> rule7))]
("tiger" "is" "kind" "+")
((triple10) -> (rule7 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is not kind.
False
2
inv-proof
[(((triple10) -> rule7))]
("tiger" "is" "kind" "-")
((triple10) -> (rule7 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is big.
True
3
proof
[(((((triple10) -> rule7)) -> rule9))]
("tiger" "is" "big" "+")
((((triple10) -> (rule7 % int2))) -> (rule9 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The rabbit is not big.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("rabbit" "is" "big" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The cat chases the rabbit.
True
5
proof
[(((((((triple10) -> rule7)) -> rule9) triple10) -> rule6))]
("cat" "chases" "rabbit" "+")
((((((triple10) -> (rule7 % int3))) -> (rule9 % int2)) triple10) -> (rule6 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The cat does not chase the rabbit.
False
5
inv-proof
[(((((((triple10) -> rule7)) -> rule9) triple10) -> rule6))]
("cat" "chases" "rabbit" "-")
((((((triple10) -> (rule7 % int3))) -> (rule9 % int2)) triple10) -> (rule6 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The cat sees the squirrel.
True
6
proof
[(((((((((triple10) -> rule7)) -> rule9) triple10) -> rule6)) -> rule2))]
("cat" "sees" "squirrel" "+")
((((((((triple10) -> (rule7 % int4))) -> (rule9 % int3)) triple10) -> (rule6 % int2))) -> (rule2 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger is kind.
("tiger" "is" "kind" "+")
int4
The rabbit does not like the tiger.
False
6
inv-proof
[(((((((((triple10) -> rule7)) -> rule9) triple10) -> rule6)) -> rule8))]
("rabbit" "likes" "tiger" "-")
((((((((triple10) -> (rule7 % int4))) -> (rule9 % int3)) triple10) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger is kind.
("tiger" "is" "kind" "+")
int4
The tiger sees the cat.
True
7
proof
[(((((((((((triple10) -> rule7)) -> rule9) triple10) -> rule6)) -> rule8)) -> rule1))]
("tiger" "sees" "cat" "+")
((((((((((triple10) -> (rule7 % int5))) -> (rule9 % int4)) triple10) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
The tiger is kind.
("tiger" "is" "kind" "+")
int5
The tiger does not see the cat.
False
7
inv-proof
[(((((((((((triple10) -> rule7)) -> rule9) triple10) -> rule6)) -> rule8)) -> rule1))]
("tiger" "sees" "cat" "-")
((((((((((triple10) -> (rule7 % int5))) -> (rule9 % int4)) triple10) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
The tiger is kind.
("tiger" "is" "kind" "+")
int5
The rabbit does not see the squirrel.
Unknown
inv-rconc
[@1: The rabbit sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "squirrel" "-")
The squirrel is big.
Unknown
rconc
[@2: The squirrel is big.[CWA. Example of deepest failure = (rule9 <- rule7 <- FAIL)]]
("squirrel" "is" "big" "+")
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The rabbit is kind.
Unknown
rconc
[@1: The rabbit is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "kind" "+")
The squirrel is not kind.
Unknown
inv-rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "kind" "-")
The cat is kind.
Unknown
rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "kind" "+")
The cat does not chase the squirrel.
Unknown
inv-random
[@0: The cat chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "squirrel" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The cat does not like the squirrel.
Unknown
inv-random
[@0: The cat likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "squirrel" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The cat does not see the rabbit.
Unknown
inv-random
[@0: The cat sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "rabbit" "-")
The squirrel chases the tiger.
Unknown
random
[@0: The squirrel chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "tiger" "+")
@0: The cat chases the tiger.[(triple1)] The cat is big.[(triple2)] The cat likes the rabbit.[(triple3)] The rabbit is nice.[(triple4)] The squirrel likes the rabbit.[(triple5)] The squirrel sees the cat.[(triple6)] The squirrel sees the tiger.[(triple7)] The tiger is nice.[(triple8)] The tiger is rough.[(triple9)] The tiger likes the cat.[(triple10)] @1: The tiger is kind.[(((triple10) -> rule7))] The tiger sees the rabbit.[(((triple1) -> rule5))] @2: The rabbit is big.[(((((triple1) -> rule5)) -> rule4))] The tiger is big.[(((((triple10) -> rule7)) -> rule9))] @3: The cat chases the rabbit.[(((((((triple10) -> rule7)) -> rule9) triple10) -> rule6))] @4: The cat sees the squirrel.[(((((((((triple10) -> rule7)) -> rule9) triple10) -> rule6)) -> rule2))] The rabbit likes the tiger.[(((((((((triple10) -> rule7)) -> rule9) triple10) -> rule6)) -> rule8))] @5: The tiger sees the cat.[(((((((((((triple10) -> rule7)) -> rule9) triple10) -> rule6)) -> rule8)) -> rule1))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple3
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple4
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple5
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple6
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple7
The tiger is nice.
("tiger" "is" "nice" "+")
triple8
The tiger is rough.
("tiger" "is" "rough" "+")
triple9
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple10
The tiger is kind.
("tiger" "is" "kind" "+")
((triple10) -> (rule7 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
((triple1) -> (rule5 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
((((triple10) -> (rule7 % int2))) -> (rule9 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
((((((triple10) -> (rule7 % int3))) -> (rule9 % int2)) triple10) -> (rule6 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
((((((((triple10) -> (rule7 % int4))) -> (rule9 % int3)) triple10) -> (rule6 % int2))) -> (rule2 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger is kind.
("tiger" "is" "kind" "+")
int4
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
((((((((triple10) -> (rule7 % int4))) -> (rule9 % int3)) triple10) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger is kind.
("tiger" "is" "kind" "+")
int4
The tiger sees the cat.
("tiger" "sees" "cat" "+")
((((((((((triple10) -> (rule7 % int5))) -> (rule9 % int4)) triple10) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
The tiger is kind.
("tiger" "is" "kind" "+")
int5