The cat chases the rabbit. The cat is cold. The cat is kind. The cat is not nice. The cat is round. The cat needs the rabbit. The cat sees the rabbit. The rabbit does not chase the cat. The rabbit is cold. The rabbit is kind. The rabbit is round. The rabbit needs the cat. If someone needs the rabbit and the rabbit sees the cat then the rabbit is rough. If someone sees the rabbit and the rabbit is rough then they chase the cat. If someone needs the cat and the cat needs the rabbit then they see the cat.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is not nice.
("cat" "is" "nice" "-")
The cat is round.
("cat" "is" "round" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If someone needs the rabbit and the rabbit sees the cat then the rabbit is rough.
((("someone" "needs" "rabbit" "+") ("rabbit" "sees" "cat" "+")) -> ("rabbit" "is" "rough" "+"))
If someone sees the rabbit and the rabbit is rough then they chase the cat.
((("someone" "sees" "rabbit" "+") ("rabbit" "is" "rough" "+")) -> ("someone" "chases" "cat" "+"))
If someone needs the cat and the cat needs the rabbit then they see the cat.
((("someone" "needs" "cat" "+") ("cat" "needs" "rabbit" "+")) -> ("someone" "sees" "cat" "+"))
The cat is not nice.
True
1
proof
[(triple4)]
("cat" "is" "nice" "-")
triple4
The cat is not cold.
False
1
inv-proof
[(triple2)]
("cat" "is" "cold" "-")
triple2
The rabbit sees the cat.
True
3
proof
[(((triple12 triple6) -> rule3))]
("rabbit" "sees" "cat" "+")
((triple12 triple6) -> (rule3 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit does not see the cat.
False
3
inv-proof
[(((triple12 triple6) -> rule3))]
("rabbit" "sees" "cat" "-")
((triple12 triple6) -> (rule3 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit is rough.
True
5
proof
[(((triple6 ((triple12 triple6) -> rule3)) -> rule1))]
("rabbit" "is" "rough" "+")
((triple6 ((triple12 triple6) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit is not rough.
False
5
inv-proof
[(((triple6 ((triple12 triple6) -> rule3)) -> rule1))]
("rabbit" "is" "rough" "-")
((triple6 ((triple12 triple6) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The cat chases the cat.
True
7
proof
[(((triple7 ((triple6 ((triple12 triple6) -> rule3)) -> rule1)) -> rule2))]
("cat" "chases" "cat" "+")
((triple7 ((triple6 ((triple12 triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3
The cat does not chase the cat.
False
7
inv-proof
[(((triple7 ((triple6 ((triple12 triple6) -> rule3)) -> rule1)) -> rule2))]
("cat" "chases" "cat" "-")
((triple7 ((triple6 ((triple12 triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "sees" "cat" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
@0: The cat chases the rabbit.[(triple1)] The cat is cold.[(triple2)] The cat is kind.[(triple3)] The cat is not nice.[(triple4)] The cat is round.[(triple5)] The cat needs the rabbit.[(triple6)] The cat sees the rabbit.[(triple7)] The rabbit does not chase the cat.[(triple8)] The rabbit is cold.[(triple9)] The rabbit is kind.[(triple10)] The rabbit is round.[(triple11)] The rabbit needs the cat.[(triple12)] @1: The rabbit sees the cat.[(((triple12 triple6) -> rule3))] @2: The rabbit is rough.[(((triple6 ((triple12 triple6) -> rule3)) -> rule1))] @3: The cat chases the cat.[(((triple7 ((triple6 ((triple12 triple6) -> rule3)) -> rule1)) -> rule2))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat is not nice.
("cat" "is" "nice" "-")
triple4
The cat is round.
("cat" "is" "round" "+")
triple5
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple6
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple7
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
triple8
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple9
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple10
The rabbit is round.
("rabbit" "is" "round" "+")
triple11
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple12
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
((triple12 triple6) -> (rule3 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple6 ((triple12 triple6) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple7 ((triple6 ((triple12 triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3