The cat visits the dog. The dog chases the tiger. The tiger chases the cat. If someone eats the tiger then they chase the dog. Big people are young. If someone visits the dog then the dog does not eat the cat. If someone visits the cat then they chase the tiger. If someone eats the cat then they do not chase the cat. If someone visits the cat and the cat is rough then the cat is nice. If someone is rough and they do not visit the cat then they eat the dog. If someone chases the cat and they do not chase the dog then the cat is not rough.
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
If someone eats the tiger then they chase the dog.
((("someone" "eats" "tiger" "+")) -> ("someone" "chases" "dog" "+"))
Big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone visits the dog then the dog does not eat the cat.
((("someone" "visits" "dog" "+")) -> ("dog" "eats" "cat" "-"))
If someone visits the cat then they chase the tiger.
((("someone" "visits" "cat" "+")) -> ("someone" "chases" "tiger" "+"))
If someone eats the cat then they do not chase the cat.
((("someone" "eats" "cat" "+")) -> ("someone" "chases" "cat" "-"))
If someone visits the cat and the cat is rough then the cat is nice.
((("someone" "visits" "cat" "+") ("cat" "is" "rough" "+")) -> ("cat" "is" "nice" "+"))
If someone is rough and they do not visit the cat then they eat the dog.
((("someone" "is" "rough" "+") ("someone" "visits" "cat" "~")) -> ("someone" "eats" "dog" "+"))
If someone chases the cat and they do not chase the dog then the cat is not rough.
((("someone" "chases" "cat" "+") ("someone" "chases" "dog" "~")) -> ("cat" "is" "rough" "-"))
The tiger chases the cat.
True
1
proof
[(triple3)]
("tiger" "chases" "cat" "+")
triple3
The dog does not chase the tiger.
False
1
inv-proof
[(triple2)]
("dog" "chases" "tiger" "-")
triple2
The dog does not eat the cat.
True
2
proof
[(((triple1) -> rule3))]
("dog" "eats" "cat" "-")
((triple1) -> (rule3 % int1))
The dog does not eat the cat.
("dog" "eats" "cat" "-")
int1
The dog eats the cat.
False
2
inv-proof
[(((triple1) -> rule3))]
("dog" "eats" "cat" "+")
((triple1) -> (rule3 % int1))
The dog does not eat the cat.
("dog" "eats" "cat" "-")
int1
The cat does not chase the dog.
Unknown
inv-rconc
[@1: The cat chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "chases" "dog" "-")
The tiger chases the dog.
Unknown
rconc
[@1: The tiger chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "dog" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The tiger visits the dog.
Unknown
random
[@0: The tiger visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "dog" "+")
@0: The cat visits the dog.[(triple1)] The dog chases the tiger.[(triple2)] The tiger chases the cat.[(triple3)] @1: The dog does not eat the cat.[(((triple1) -> rule3))]
The cat visits the dog.
("cat" "visits" "dog" "+")
triple1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple3
The dog does not eat the cat.
("dog" "eats" "cat" "-")
((triple1) -> (rule3 % int1))
The dog does not eat the cat.
("dog" "eats" "cat" "-")
int1