The cat chases the rabbit. The cat is kind. The cat is nice. The cat is rough. The cat is not round. The cat visits the rabbit. The rabbit is nice. The rabbit is rough. The rabbit likes the cat. The rabbit visits the cat. If something chases the rabbit then the rabbit is round. If something likes the rabbit and it visits the rabbit then the rabbit is round. If something likes the rabbit then it is kind. If something is round then it likes the rabbit. If something likes the rabbit then the rabbit does not chase the cat. If something chases the rabbit and it is red then the rabbit visits the cat. If something is kind then it visits the cat. If something is red and not round then it visits the cat.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is not round.
("cat" "is" "round" "-")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If something chases the rabbit then the rabbit is round.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
If something likes the rabbit and it visits the rabbit then the rabbit is round.
((("something" "likes" "rabbit" "+") ("something" "visits" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
If something likes the rabbit then it is kind.
((("something" "likes" "rabbit" "+")) -> ("something" "is" "kind" "+"))
If something is round then it likes the rabbit.
((("something" "is" "round" "+")) -> ("something" "likes" "rabbit" "+"))
If something likes the rabbit then the rabbit does not chase the cat.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "chases" "cat" "-"))
If something chases the rabbit and it is red then the rabbit visits the cat.
((("something" "chases" "rabbit" "+") ("something" "is" "red" "+")) -> ("rabbit" "visits" "cat" "+"))
If something is kind then it visits the cat.
((("something" "is" "kind" "+")) -> ("something" "visits" "cat" "+"))
If something is red and not round then it visits the cat.
((("something" "is" "red" "+") ("something" "is" "round" "~")) -> ("something" "visits" "cat" "+"))
The cat is nice.
True
1
proof
[(triple3)]
("cat" "is" "nice" "+")
triple3
The rabbit is not nice.
False
1
inv-proof
[(triple7)]
("rabbit" "is" "nice" "-")
triple7
The rabbit is round.
True
2
proof
[(((triple1) -> rule1))]
("rabbit" "is" "round" "+")
((triple1) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The cat does not visit the cat.
False
2
inv-proof
[(((triple2) -> rule7))]
("cat" "visits" "cat" "-")
((triple2) -> (rule7 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The rabbit likes the rabbit.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("rabbit" "likes" "rabbit" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit does not like the rabbit.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("rabbit" "likes" "rabbit" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The cat does not like the rabbit.
Unknown
inv-rconc
[@1: The cat likes the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "likes" "rabbit" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat chases the rabbit.[(triple1)] The cat is kind.[(triple2)] The cat is nice.[(triple3)] The cat is not round.[(triple5)] The cat is rough.[(triple4)] The cat visits the rabbit.[(triple6)] The rabbit is nice.[(triple7)] The rabbit is rough.[(triple8)] The rabbit likes the cat.[(triple9)] The rabbit visits the cat.[(triple10 OR ((((((((triple1) -> rule1)) -> rule4)) -> rule3)) -> rule7))] @1: The cat visits the cat.[(((triple2) -> rule7))] The rabbit is round.[(((triple1) -> rule1))] @2: The rabbit likes the rabbit.[(((((triple1) -> rule1)) -> rule4))] @3: The rabbit does not chase the cat.[(((((((triple1) -> rule1)) -> rule4)) -> rule5))] The rabbit is kind.[(((((((triple1) -> rule1)) -> rule4)) -> rule3))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat is not round.
("cat" "is" "round" "-")
triple5
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple6
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple7
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple8
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple9
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple10
((((((((triple1) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int3
The rabbit is round.
("rabbit" "is" "round" "+")
int4
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple2) -> (rule7 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple1) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit is kind.
("rabbit" "is" "kind" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3