The cat is round. The dog is big. The rabbit visits the cat. If the dog chases the cat then the cat likes the rabbit. If something chases the dog then the dog is round. If something is round then it chases the dog.
The cat is round.
("cat" "is" "round" "+")
The dog is big.
("dog" "is" "big" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If the dog chases the cat then the cat likes the rabbit.
((("dog" "chases" "cat" "+")) -> ("cat" "likes" "rabbit" "+"))
If something chases the dog then the dog is round.
((("something" "chases" "dog" "+")) -> ("dog" "is" "round" "+"))
If something is round then it chases the dog.
((("something" "is" "round" "+")) -> ("something" "chases" "dog" "+"))
The rabbit visits the cat.
True
1
proof
[(triple3)]
("rabbit" "visits" "cat" "+")
triple3
The cat is not round.
False
1
inv-proof
[(triple1)]
("cat" "is" "round" "-")
triple1
The cat chases the dog.
True
2
proof
[(((triple1) -> rule3))]
("cat" "chases" "dog" "+")
((triple1) -> (rule3 % int1))
The cat chases the dog.
("cat" "chases" "dog" "+")
int1
The cat does not chase the dog.
False
2
inv-proof
[(((triple1) -> rule3))]
("cat" "chases" "dog" "-")
((triple1) -> (rule3 % int1))
The cat chases the dog.
("cat" "chases" "dog" "+")
int1
The dog is round.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("dog" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The cat chases the dog.
("cat" "chases" "dog" "+")
int2
The dog is not round.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("dog" "is" "round" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The cat chases the dog.
("cat" "chases" "dog" "+")
int2
The dog chases the dog.
True
4
proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule3))]
("dog" "chases" "dog" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The cat chases the dog.
("cat" "chases" "dog" "+")
int3
The dog does not chase the dog.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule3))]
("dog" "chases" "dog" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The cat chases the dog.
("cat" "chases" "dog" "+")
int3
The rabbit does not chase the dog.
Unknown
inv-rconc
[@1: The rabbit chases the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "chases" "dog" "-")
The cat likes the rabbit.
Unknown
rconc
[@1: The cat likes the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "rabbit" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The dog chases the rabbit.
Unknown
random
[@0: The dog chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "rabbit" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The rabbit likes the cat.
Unknown
random
[@0: The rabbit likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "cat" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The rabbit visits the dog.
Unknown
random
[@0: The rabbit visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "dog" "+")
@0: The cat is round.[(triple1)] The dog is big.[(triple2)] The rabbit visits the cat.[(triple3)] @1: The cat chases the dog.[(((triple1) -> rule3))] @2: The dog is round.[(((((triple1) -> rule3)) -> rule2))] @3: The dog chases the dog.[(((((((triple1) -> rule3)) -> rule2)) -> rule3))]
The cat is round.
("cat" "is" "round" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple3
The cat chases the dog.
("cat" "chases" "dog" "+")
((triple1) -> (rule3 % int1))
The cat chases the dog.
("cat" "chases" "dog" "+")
int1
The dog is round.
("dog" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The cat chases the dog.
("cat" "chases" "dog" "+")
int2
The dog chases the dog.
("dog" "chases" "dog" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The cat chases the dog.
("cat" "chases" "dog" "+")
int3