The cat chases the tiger. The cat needs the tiger. The dog is rough. The tiger chases the cat. The tiger chases the dog. The tiger is red. The tiger needs the dog. If someone visits the tiger then they need the tiger. If someone visits the dog then they are rough. If someone visits the dog then the dog is kind. If someone visits the cat and they chase the cat then the cat visits the dog. If the tiger needs the dog and the tiger chases the cat then the dog needs the tiger. If someone is rough and they chase the cat then the cat chases the dog. If someone needs the tiger then the tiger visits the cat. If someone needs the tiger and they are young then the tiger needs the dog.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The dog is rough.
("dog" "is" "rough" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If someone visits the tiger then they need the tiger.
((("someone" "visits" "tiger" "+")) -> ("someone" "needs" "tiger" "+"))
If someone visits the dog then they are rough.
((("someone" "visits" "dog" "+")) -> ("someone" "is" "rough" "+"))
If someone visits the dog then the dog is kind.
((("someone" "visits" "dog" "+")) -> ("dog" "is" "kind" "+"))
If someone visits the cat and they chase the cat then the cat visits the dog.
((("someone" "visits" "cat" "+") ("someone" "chases" "cat" "+")) -> ("cat" "visits" "dog" "+"))
If the tiger needs the dog and the tiger chases the cat then the dog needs the tiger.
((("tiger" "needs" "dog" "+") ("tiger" "chases" "cat" "+")) -> ("dog" "needs" "tiger" "+"))
If someone is rough and they chase the cat then the cat chases the dog.
((("someone" "is" "rough" "+") ("someone" "chases" "cat" "+")) -> ("cat" "chases" "dog" "+"))
If someone needs the tiger then the tiger visits the cat.
((("someone" "needs" "tiger" "+")) -> ("tiger" "visits" "cat" "+"))
If someone needs the tiger and they are young then the tiger needs the dog.
((("someone" "needs" "tiger" "+") ("someone" "is" "young" "+")) -> ("tiger" "needs" "dog" "+"))
The tiger is red.
True
1
proof
[(triple6)]
("tiger" "is" "red" "+")
triple6
The tiger does not need the dog.
False
1
inv-proof
[(triple7)]
("tiger" "needs" "dog" "-")
triple7
The tiger visits the cat.
True
2
proof
[(((triple2) -> rule7) OR ((((triple7 triple4) -> rule5)) -> rule7))]
("tiger" "visits" "cat" "+")
((triple2) -> (rule7 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
((((triple7 triple4) -> (rule5 % int2))) -> (rule7 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int2
The dog does not need the tiger.
False
3
inv-proof
[(((triple7 triple4) -> rule5))]
("dog" "needs" "tiger" "-")
((triple7 triple4) -> (rule5 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The cat visits the dog.
True
4
proof
[(((((triple2) -> rule7) triple4) -> rule4) OR ((((((triple7 triple4) -> rule5)) -> rule7) triple4) -> rule4))]
("cat" "visits" "dog" "+")
((((triple2) -> (rule7 % int2)) triple4) -> (rule4 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
((((((triple7 triple4) -> (rule5 % int3))) -> (rule7 % int2)) triple4) -> (rule4 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int3
The cat does not visit the dog.
False
4
inv-proof
[(((((triple2) -> rule7) triple4) -> rule4) OR ((((((triple7 triple4) -> rule5)) -> rule7) triple4) -> rule4))]
("cat" "visits" "dog" "-")
((((triple2) -> (rule7 % int2)) triple4) -> (rule4 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
((((((triple7 triple4) -> (rule5 % int3))) -> (rule7 % int2)) triple4) -> (rule4 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int3
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger is rough.
Unknown
rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "rough" "+")
The cat does not chase the dog.
Unknown
inv-rconc
[@2: The cat chases the dog.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("cat" "chases" "dog" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
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 cat visits the tiger.
Unknown
random
[@0: The cat visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "tiger" "+")
@0: The cat chases the tiger.[(triple1)] The cat needs the tiger.[(triple2)] The dog is rough.[(triple3)] The tiger chases the cat.[(triple4)] The tiger chases the dog.[(triple5)] The tiger is red.[(triple6)] The tiger needs the dog.[(triple7)] @1: The dog needs the tiger.[(((triple7 triple4) -> rule5))] The tiger visits the cat.[(((triple2) -> rule7) OR ((((triple7 triple4) -> rule5)) -> rule7))] @2: The cat visits the dog.[(((((triple2) -> rule7) triple4) -> rule4) OR ((((((triple7 triple4) -> rule5)) -> rule7) triple4) -> rule4))] @3: The cat is rough.[(((((((triple2) -> rule7) triple4) -> rule4)) -> rule2) OR ((((((((triple7 triple4) -> rule5)) -> rule7) triple4) -> rule4)) -> rule2))] The dog is kind.[(((((((triple2) -> rule7) triple4) -> rule4)) -> rule3) OR ((((((((triple7 triple4) -> rule5)) -> rule7) triple4) -> rule4)) -> rule3))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple2
The dog is rough.
("dog" "is" "rough" "+")
triple3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple4
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple5
The tiger is red.
("tiger" "is" "red" "+")
triple6
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple7
The dog needs the tiger.
("dog" "needs" "tiger" "+")
((triple7 triple4) -> (rule5 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
((triple2) -> (rule7 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
((((triple7 triple4) -> (rule5 % int2))) -> (rule7 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
((((triple2) -> (rule7 % int2)) triple4) -> (rule4 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
((((((triple7 triple4) -> (rule5 % int3))) -> (rule7 % int2)) triple4) -> (rule4 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
((((((triple2) -> (rule7 % int3)) triple4) -> (rule4 % int2))) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int3
((((((((triple7 triple4) -> (rule5 % int4))) -> (rule7 % int3)) triple4) -> (rule4 % int2))) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int3
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int4
The dog is kind.
("dog" "is" "kind" "+")
((((((triple2) -> (rule7 % int3)) triple4) -> (rule4 % int2))) -> (rule3 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int3
((((((((triple7 triple4) -> (rule5 % int4))) -> (rule7 % int3)) triple4) -> (rule4 % int2))) -> (rule3 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int3
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int4