The cat chases the dog. The cat chases the tiger. The cat visits the dog. The dog does not chase the cat. The dog does not chase the tiger. The dog visits the cat. The dog visits the tiger. The tiger chases the cat. The tiger likes the cat. The tiger visits the dog. If someone chases the cat then they chase the tiger. If someone likes the cat then the cat visits the tiger. If the cat chases the tiger and the cat likes the tiger then the cat likes the dog. If someone likes the dog then they are not big. If someone visits the dog and the dog visits the cat then they like the dog. If someone chases the cat and they are not big then the cat is not nice.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog does not chase the cat.
("dog" "chases" "cat" "-")
The dog does not chase the tiger.
("dog" "chases" "tiger" "-")
The dog visits the cat.
("dog" "visits" "cat" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If someone chases the cat then they chase the tiger.
((("someone" "chases" "cat" "+")) -> ("someone" "chases" "tiger" "+"))
If someone likes the cat then the cat visits the tiger.
((("someone" "likes" "cat" "+")) -> ("cat" "visits" "tiger" "+"))
If the cat chases the tiger and the cat likes the tiger then the cat likes the dog.
((("cat" "chases" "tiger" "+") ("cat" "likes" "tiger" "+")) -> ("cat" "likes" "dog" "+"))
If someone likes the dog then they are not big.
((("someone" "likes" "dog" "+")) -> ("someone" "is" "big" "-"))
If someone visits the dog and the dog visits the cat then they like the dog.
((("someone" "visits" "dog" "+") ("dog" "visits" "cat" "+")) -> ("someone" "likes" "dog" "+"))
If someone chases the cat and they are not big then the cat is not nice.
((("someone" "chases" "cat" "+") ("someone" "is" "big" "~")) -> ("cat" "is" "nice" "-"))
The dog visits the cat.
True
1
proof
[(triple6)]
("dog" "visits" "cat" "+")
triple6
The dog chases the cat.
False
1
inv-proof
[(triple4)]
("dog" "chases" "cat" "+")
triple4
The tiger likes the dog.
True
3
proof
[(((triple10 triple6) -> rule5))]
("tiger" "likes" "dog" "+")
((triple10 triple6) -> (rule5 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger does not chase the tiger.
False
2
inv-proof
[(((triple8) -> rule1))]
("tiger" "chases" "tiger" "-")
((triple8) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The cat is not big.
True
4
proof
[(((((triple3 triple6) -> rule5)) -> rule4))]
("cat" "is" "big" "-")
((((triple3 triple6) -> (rule5 % int2))) -> (rule4 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
int2
The cat is big.
False
4
inv-proof
[(((((triple3 triple6) -> rule5)) -> rule4))]
("cat" "is" "big" "+")
((((triple3 triple6) -> (rule5 % int2))) -> (rule4 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
int2
The cat is not nice.
True
6
proof
[(((triple8 ((((triple10 triple6) -> rule5)) -> rule4)) -> rule6))]
("cat" "is" "nice" "-")
((triple8 ((((triple10 triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The tiger is not big.
("tiger" "is" "big" "-")
int2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int3
The cat is nice.
False
6
inv-proof
[(((triple8 ((((triple10 triple6) -> rule5)) -> rule4)) -> rule6))]
("cat" "is" "nice" "+")
((triple8 ((((triple10 triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The tiger is not big.
("tiger" "is" "big" "-")
int2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int3
The dog does not like the dog.
Unknown
inv-rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "likes" "dog" "-")
The cat likes the tiger.
Unknown
random
[@0: The cat likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "tiger" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The tiger is not blue.
Unknown
inv-random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "-")
The dog likes the cat.
Unknown
random
[@0: The dog likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cat" "+")
@0: The cat chases the dog.[(triple1)] The cat chases the tiger.[(triple2)] The cat visits the dog.[(triple3)] The dog does not chase the cat.[(triple4)] The dog does not chase the tiger.[(triple5)] The dog visits the cat.[(triple6)] The dog visits the tiger.[(triple7)] The tiger chases the cat.[(triple8)] The tiger likes the cat.[(triple9)] The tiger visits the dog.[(triple10)] @1: The cat likes the dog.[(((triple3 triple6) -> rule5))] The cat visits the tiger.[(((triple9) -> rule2))] The tiger chases the tiger.[(((triple8) -> rule1))] The tiger likes the dog.[(((triple10 triple6) -> rule5))] @2: The cat is not big.[(((((triple3 triple6) -> rule5)) -> rule4))] The tiger is not big.[(((((triple10 triple6) -> rule5)) -> rule4))] @3: The cat is not nice.[(((triple8 ((((triple10 triple6) -> rule5)) -> rule4)) -> rule6))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple2
The cat visits the dog.
("cat" "visits" "dog" "+")
triple3
The dog does not chase the cat.
("dog" "chases" "cat" "-")
triple4
The dog does not chase the tiger.
("dog" "chases" "tiger" "-")
triple5
The dog visits the cat.
("dog" "visits" "cat" "+")
triple6
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple7
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple8
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple9
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple10
The cat likes the dog.
("cat" "likes" "dog" "+")
((triple3 triple6) -> (rule5 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
((triple9) -> (rule2 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple8) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
((triple10 triple6) -> (rule5 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The cat is not big.
("cat" "is" "big" "-")
((((triple3 triple6) -> (rule5 % int2))) -> (rule4 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
int2
The tiger is not big.
("tiger" "is" "big" "-")
((((triple10 triple6) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is not big.
("tiger" "is" "big" "-")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The cat is not nice.
("cat" "is" "nice" "-")
((triple8 ((((triple10 triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The tiger is not big.
("tiger" "is" "big" "-")
int2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int3