The cat visits the dog. The dog is round. The rabbit chases the cat. If someone chases the cat then the cat chases the rabbit. If someone is blue then they visit the cat. If someone is young and they like the cat then the cat visits the rabbit. If someone chases the rabbit then they visit the cat. If the cat chases the rabbit and the cat is kind then the cat chases the dog. If someone visits the cat then the cat is round. If the rabbit chases the dog then the rabbit visits the cat. If someone chases the cat then they chase the rabbit.
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog is round.
("dog" "is" "round" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
If someone chases the cat then the cat chases the rabbit.
((("someone" "chases" "cat" "+")) -> ("cat" "chases" "rabbit" "+"))
If someone is blue then they visit the cat.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "cat" "+"))
If someone is young and they like the cat then the cat visits the rabbit.
((("someone" "is" "young" "+") ("someone" "likes" "cat" "+")) -> ("cat" "visits" "rabbit" "+"))
If someone chases the rabbit then they visit the cat.
((("someone" "chases" "rabbit" "+")) -> ("someone" "visits" "cat" "+"))
If the cat chases the rabbit and the cat is kind then the cat chases the dog.
((("cat" "chases" "rabbit" "+") ("cat" "is" "kind" "+")) -> ("cat" "chases" "dog" "+"))
If someone visits the cat then the cat is round.
((("someone" "visits" "cat" "+")) -> ("cat" "is" "round" "+"))
If the rabbit chases the dog then the rabbit visits the cat.
((("rabbit" "chases" "dog" "+")) -> ("rabbit" "visits" "cat" "+"))
If someone chases the cat then they chase the rabbit.
((("someone" "chases" "cat" "+")) -> ("someone" "chases" "rabbit" "+"))
The rabbit chases the cat.
True
1
proof
[(triple3)]
("rabbit" "chases" "cat" "+")
triple3
The dog is not round.
False
1
inv-proof
[(triple2)]
("dog" "is" "round" "-")
triple2
The cat chases the rabbit.
True
2
proof
[(((triple3) -> rule1))]
("cat" "chases" "rabbit" "+")
((triple3) -> (rule1 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The rabbit does not chase the rabbit.
False
2
inv-proof
[(((triple3) -> rule8))]
("rabbit" "chases" "rabbit" "-")
((triple3) -> (rule8 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit visits the cat.
True
3
proof
[(((((triple3) -> rule8)) -> rule4))]
("rabbit" "visits" "cat" "+")
((((triple3) -> (rule8 % int2))) -> (rule4 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The cat does not visit the cat.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule4))]
("cat" "visits" "cat" "-")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The cat is round.
True
4
proof
[(((((((triple3) -> rule1)) -> rule4)) -> rule6) OR ((((((triple3) -> rule8)) -> rule4)) -> rule6))]
("cat" "is" "round" "+")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int3
((((((triple3) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3
The cat is not round.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule4)) -> rule6) OR ((((((triple3) -> rule8)) -> rule4)) -> rule6))]
("cat" "is" "round" "-")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int3
((((((triple3) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3
The cat does not chase the dog.
Unknown
inv-rconc
[@1: The cat chases the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "chases" "dog" "-")
The cat visits the rabbit.
Unknown
rconc
[@1: The cat visits the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "visits" "rabbit" "+")
The dog does not visit the cat.
Unknown
inv-rconc
[@2: The dog visits the cat.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("dog" "visits" "cat" "-")
The dog chases the rabbit.
Unknown
rconc
[@1: The dog chases the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "chases" "rabbit" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
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 chases the dog.
Unknown
random
[@0: The rabbit chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "dog" "+")
@0: The cat visits the dog.[(triple1)] The dog is round.[(triple2)] The rabbit chases the cat.[(triple3)] @1: The cat chases the rabbit.[(((triple3) -> rule1))] The rabbit chases the rabbit.[(((triple3) -> rule8))] @2: The cat visits the cat.[(((((triple3) -> rule1)) -> rule4))] The rabbit visits the cat.[(((((triple3) -> rule8)) -> rule4))] @3: The cat is round.[(((((((triple3) -> rule1)) -> rule4)) -> rule6) OR ((((((triple3) -> rule8)) -> rule4)) -> rule6))]
The cat visits the dog.
("cat" "visits" "dog" "+")
triple1
The dog is round.
("dog" "is" "round" "+")
triple2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple3
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
((triple3) -> (rule1 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple3) -> (rule8 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
((((triple3) -> (rule8 % int2))) -> (rule4 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The cat is round.
("cat" "is" "round" "+")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int3
((((((triple3) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3