The cat chases the tiger. The dog does not chase the cat. The tiger chases the dog. If someone chases the cat and the cat is not round then the cat is nice. If someone chases the tiger then they see the dog. If someone is red and they see the cat then they chase the dog. If someone sees the dog then they visit the cat. If someone chases the tiger and they do not see the cat then they are red. If the cat is blue and the cat does not chase the tiger then the tiger is not nice. If someone visits the tiger then the tiger is not nice. If the tiger chases the dog then the dog chases the tiger.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The dog does not chase the cat.
("dog" "chases" "cat" "-")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
If someone chases the cat and the cat is not round then the cat is nice.
((("someone" "chases" "cat" "+") ("cat" "is" "round" "~")) -> ("cat" "is" "nice" "+"))
If someone chases the tiger then they see the dog.
((("someone" "chases" "tiger" "+")) -> ("someone" "sees" "dog" "+"))
If someone is red and they see the cat then they chase the dog.
((("someone" "is" "red" "+") ("someone" "sees" "cat" "+")) -> ("someone" "chases" "dog" "+"))
If someone sees the dog then they visit the cat.
((("someone" "sees" "dog" "+")) -> ("someone" "visits" "cat" "+"))
If someone chases the tiger and they do not see the cat then they are red.
((("someone" "chases" "tiger" "+") ("someone" "sees" "cat" "~")) -> ("someone" "is" "red" "+"))
If the cat is blue and the cat does not chase the tiger then the tiger is not nice.
((("cat" "is" "blue" "+") ("cat" "chases" "tiger" "~")) -> ("tiger" "is" "nice" "-"))
If someone visits the tiger then the tiger is not nice.
((("someone" "visits" "tiger" "+")) -> ("tiger" "is" "nice" "-"))
If the tiger chases the dog then the dog chases the tiger.
((("tiger" "chases" "dog" "+")) -> ("dog" "chases" "tiger" "+"))
The cat chases the tiger.
True
1
proof
[(triple1)]
("cat" "chases" "tiger" "+")
triple1
The cat does not chase the tiger.
False
1
inv-proof
[(triple1)]
("cat" "chases" "tiger" "-")
triple1
The cat sees the dog.
True
2
proof
[(((triple1) -> rule2))]
("cat" "sees" "dog" "+")
((triple1) -> (rule2 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The dog does not chase the tiger.
False
2
inv-proof
[(((triple3) -> rule8))]
("dog" "chases" "tiger" "-")
((triple3) -> (rule8 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The cat visits the cat.
True
3
proof
[(((((triple1) -> rule2)) -> rule4))]
("cat" "visits" "cat" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
The cat does not visit the cat.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("cat" "visits" "cat" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
The dog visits the cat.
True
4
proof
[(((((((triple3) -> rule8)) -> rule2)) -> rule4))]
("dog" "visits" "cat" "+")
((((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int3
The dog does not visit the cat.
False
4
inv-proof
[(((((((triple3) -> rule8)) -> rule2)) -> rule4))]
("dog" "visits" "cat" "-")
((((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int3
The cat is not nice.
Unknown
inv-rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "nice" "-")
The cat chases the dog.
Unknown
rconc
[@1: The cat chases the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "chases" "dog" "+")
The cat is not red.
Unknown
inv-rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "red" "-")
The dog chases the dog.
Unknown
rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "chases" "dog" "+")
The cat does not visit the tiger.
Unknown
inv-random
[@0: The cat visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "tiger" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The cat chases the tiger.[(triple1)] The dog does not chase the cat.[(triple2)] The tiger chases the dog.[(triple3)] @1: The cat sees the dog.[(((triple1) -> rule2))] The dog chases the tiger.[(((triple3) -> rule8))] @2: The cat visits the cat.[(((((triple1) -> rule2)) -> rule4))] The dog sees the dog.[(((((triple3) -> rule8)) -> rule2))] @3: The dog visits the cat.[(((((((triple3) -> rule8)) -> rule2)) -> rule4))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The dog does not chase the cat.
("dog" "chases" "cat" "-")
triple2
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple3
The cat sees the dog.
("cat" "sees" "dog" "+")
((triple1) -> (rule2 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
((triple3) -> (rule8 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat sees the dog.
("cat" "sees" "dog" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
((((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int3