The cat chases the rabbit. The cat is round. The cat does not need the rabbit. The rabbit does not chase the cat. The rabbit is cold. The rabbit likes the cat. The rabbit needs the cat. If something chases the rabbit then it needs the cat. If the cat is red then the cat needs the rabbit. If something needs the cat and it is not rough then it chases the rabbit. If the rabbit is cold then the rabbit likes the cat. If something likes the rabbit then the rabbit is round. If something needs the cat and it does not need the rabbit then it likes the rabbit.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is round.
("cat" "is" "round" "+")
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If something chases the rabbit then it needs the cat.
((("something" "chases" "rabbit" "+")) -> ("something" "needs" "cat" "+"))
If the cat is red then the cat needs the rabbit.
((("cat" "is" "red" "+")) -> ("cat" "needs" "rabbit" "+"))
If something needs the cat and it is not rough then it chases the rabbit.
((("something" "needs" "cat" "+") ("something" "is" "rough" "~")) -> ("something" "chases" "rabbit" "+"))
If the rabbit is cold then the rabbit likes the cat.
((("rabbit" "is" "cold" "+")) -> ("rabbit" "likes" "cat" "+"))
If something likes the rabbit then the rabbit is round.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
If something needs the cat and it does not need the rabbit then it likes the rabbit.
((("something" "needs" "cat" "+") ("something" "needs" "rabbit" "~")) -> ("something" "likes" "rabbit" "+"))
The rabbit needs the cat.
True
1
proof
[(triple7)]
("rabbit" "needs" "cat" "+")
triple7
The rabbit chases the cat.
False
1
inv-proof
[(triple4)]
("rabbit" "chases" "cat" "+")
triple4
The cat needs the cat.
True
2
proof
[(((triple1) -> rule1))]
("cat" "needs" "cat" "+")
((triple1) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat does not need the cat.
False
2
inv-proof
[(((triple1) -> rule1))]
("cat" "needs" "cat" "-")
((triple1) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat likes the rabbit.
True
4
proof
[(((((triple1) -> rule1) triple3) -> rule6))]
("cat" "likes" "rabbit" "+")
((((triple1) -> (rule1 % int2)) triple3) -> (rule6 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat does not like the rabbit.
False
4
inv-proof
[(((((triple1) -> rule1) triple3) -> rule6))]
("cat" "likes" "rabbit" "-")
((((triple1) -> (rule1 % int2)) triple3) -> (rule6 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The rabbit is round.
True
5
proof
[(((((((triple1) -> rule1) triple3) -> rule6)) -> rule5))]
("rabbit" "is" "round" "+")
((((((triple1) -> (rule1 % int3)) triple3) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The rabbit is not round.
False
5
inv-proof
[(((((((triple1) -> rule1) triple3) -> rule6)) -> rule5))]
("rabbit" "is" "round" "-")
((((((triple1) -> (rule1 % int3)) triple3) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The rabbit does not like the rabbit.
Unknown
inv-rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "likes" "rabbit" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
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 cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The cat chases the rabbit.[(triple1)] The cat does not need the rabbit.[(triple3)] The cat is round.[(triple2)] The rabbit does not chase the cat.[(triple4)] The rabbit is cold.[(triple5)] The rabbit likes the cat.[(triple6 OR ((triple5) -> rule4))] The rabbit needs the cat.[(triple7)] @1: The cat needs the cat.[(((triple1) -> rule1))] @2: The cat likes the rabbit.[(((((triple1) -> rule1) triple3) -> rule6))] @3: The rabbit is round.[(((((((triple1) -> rule1) triple3) -> rule6)) -> rule5))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
triple3
The cat is round.
("cat" "is" "round" "+")
triple2
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
triple4
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple5
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple6
((triple5) -> (rule4 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple7
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple1) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
((((triple1) -> (rule1 % int2)) triple3) -> (rule6 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
((((((triple1) -> (rule1 % int3)) triple3) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3