The cat chases the dog. The cat does not eat the tiger. The dog chases the cat. The dog does not chase the tiger. The dog does not eat the cat. The dog eats the tiger. The dog is not young. The dog does not need the tiger. The tiger chases the dog. The tiger needs the dog. If something chases the dog and it needs the tiger then the dog eats the tiger. If something chases the tiger and the tiger chases the dog then the dog eats the tiger. If something is kind then it does not chase the cat. If something is rough and it needs the cat then the cat is not green. If something needs the cat and it is not young then it is rough. If something is green then it needs the cat. If something chases the dog then it does not chase the tiger. If something chases the dog then the dog needs the cat.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat does not eat the tiger.
("cat" "eats" "tiger" "-")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog does not chase the tiger.
("dog" "chases" "tiger" "-")
The dog does not eat the cat.
("dog" "eats" "cat" "-")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is not young.
("dog" "is" "young" "-")
The dog does not need the tiger.
("dog" "needs" "tiger" "-")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If something chases the dog and it needs the tiger then the dog eats the tiger.
((("something" "chases" "dog" "+") ("something" "needs" "tiger" "+")) -> ("dog" "eats" "tiger" "+"))
If something chases the tiger and the tiger chases the dog then the dog eats the tiger.
((("something" "chases" "tiger" "+") ("tiger" "chases" "dog" "+")) -> ("dog" "eats" "tiger" "+"))
If something is kind then it does not chase the cat.
((("something" "is" "kind" "+")) -> ("something" "chases" "cat" "-"))
If something is rough and it needs the cat then the cat is not green.
((("something" "is" "rough" "+") ("something" "needs" "cat" "+")) -> ("cat" "is" "green" "-"))
If something needs the cat and it is not young then it is rough.
((("something" "needs" "cat" "+") ("something" "is" "young" "~")) -> ("something" "is" "rough" "+"))
If something is green then it needs the cat.
((("something" "is" "green" "+")) -> ("something" "needs" "cat" "+"))
If something chases the dog then it does not chase the tiger.
((("something" "chases" "dog" "+")) -> ("something" "chases" "tiger" "-"))
If something chases the dog then the dog needs the cat.
((("something" "chases" "dog" "+")) -> ("dog" "needs" "cat" "+"))
The dog does not eat the cat.
True
1
proof
[(triple5)]
("dog" "eats" "cat" "-")
triple5
The dog eats the cat.
False
1
inv-proof
[(triple5)]
("dog" "eats" "cat" "+")
triple5
The cat does not chase the tiger.
True
2
proof
[(((triple1) -> rule7))]
("cat" "chases" "tiger" "-")
((triple1) -> (rule7 % int1))
The cat does not chase the tiger.
("cat" "chases" "tiger" "-")
int1
The tiger chases the tiger.
False
2
inv-proof
[(((triple9) -> rule7))]
("tiger" "chases" "tiger" "+")
((triple9) -> (rule7 % int1))
The tiger does not chase the tiger.
("tiger" "chases" "tiger" "-")
int1
The dog is rough.
True
4
proof
[(((((triple1) -> rule8) triple7) -> rule5) OR ((((triple9) -> rule8) triple7) -> rule5))]
("dog" "is" "rough" "+")
((((triple1) -> (rule8 % int2)) triple7) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
int2
((((triple9) -> (rule8 % int2)) triple7) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
int2
The dog is not rough.
False
4
inv-proof
[(((((triple1) -> rule8) triple7) -> rule5) OR ((((triple9) -> rule8) triple7) -> rule5))]
("dog" "is" "rough" "-")
((((triple1) -> (rule8 % int2)) triple7) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
int2
((((triple9) -> (rule8 % int2)) triple7) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
int2
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "needs" "cat" "-")
The tiger is rough.
Unknown
rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "rough" "+")
The cat is not rough.
Unknown
inv-rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "rough" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
@0: The cat chases the dog.[(triple1)] The cat does not eat the tiger.[(triple2)] The dog chases the cat.[(triple3)] The dog does not chase the tiger.[(triple4)] The dog does not eat the cat.[(triple5)] The dog does not need the tiger.[(triple8)] The dog eats the tiger.[(triple6)] The dog is not young.[(triple7)] The tiger chases the dog.[(triple9)] The tiger needs the dog.[(triple10)] @1: The cat does not chase the tiger.[(((triple1) -> rule7))] The dog needs the cat.[(((triple1) -> rule8) OR ((triple9) -> rule8))] The tiger does not chase the tiger.[(((triple9) -> rule7))] @2: The dog is rough.[(((((triple1) -> rule8) triple7) -> rule5) OR ((((triple9) -> rule8) triple7) -> rule5))] @3: The cat is not green.[(((((((triple1) -> rule8) triple7) -> rule5) ((triple1) -> rule8)) -> rule4) OR ((((((triple1) -> rule8) triple7) -> rule5) ((triple9) -> rule8)) -> rule4) OR ((((((triple9) -> rule8) triple7) -> rule5) ((triple1) -> rule8)) -> rule4) OR ((((((triple9) -> rule8) triple7) -> rule5) ((triple9) -> rule8)) -> rule4))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat does not eat the tiger.
("cat" "eats" "tiger" "-")
triple2
The dog chases the cat.
("dog" "chases" "cat" "+")
triple3
The dog does not chase the tiger.
("dog" "chases" "tiger" "-")
triple4
The dog does not eat the cat.
("dog" "eats" "cat" "-")
triple5
The dog does not need the tiger.
("dog" "needs" "tiger" "-")
triple8
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple6
The dog is not young.
("dog" "is" "young" "-")
triple7
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple9
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple10
The cat does not chase the tiger.
("cat" "chases" "tiger" "-")
((triple1) -> (rule7 % int1))
The cat does not chase the tiger.
("cat" "chases" "tiger" "-")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
((triple1) -> (rule8 % int1))
The dog needs the cat.
("dog" "needs" "cat" "+")
int1
((triple9) -> (rule8 % int1))
The dog needs the cat.
("dog" "needs" "cat" "+")
int1
The tiger does not chase the tiger.
("tiger" "chases" "tiger" "-")
((triple9) -> (rule7 % int1))
The tiger does not chase the tiger.
("tiger" "chases" "tiger" "-")
int1
The dog is rough.
("dog" "is" "rough" "+")
((((triple1) -> (rule8 % int2)) triple7) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
int2
((((triple9) -> (rule8 % int2)) triple7) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
int2
The cat is not green.
("cat" "is" "green" "-")
((((((triple1) -> (rule8 % int3)) triple7) -> (rule5 % int2)) ((triple1) -> (rule8 % int3))) -> (rule4 % int1))
The cat is not green.
("cat" "is" "green" "-")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog needs the cat.
("dog" "needs" "cat" "+")
int3
((((((triple1) -> (rule8 % int3)) triple7) -> (rule5 % int2)) ((triple9) -> (rule8 % int3))) -> (rule4 % int1))
The cat is not green.
("cat" "is" "green" "-")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog needs the cat.
("dog" "needs" "cat" "+")
int3
((((((triple9) -> (rule8 % int3)) triple7) -> (rule5 % int2)) ((triple1) -> (rule8 % int3))) -> (rule4 % int1))
The cat is not green.
("cat" "is" "green" "-")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog needs the cat.
("dog" "needs" "cat" "+")
int3
((((((triple9) -> (rule8 % int3)) triple7) -> (rule5 % int2)) ((triple9) -> (rule8 % int3))) -> (rule4 % int1))
The cat is not green.
("cat" "is" "green" "-")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog needs the cat.
("dog" "needs" "cat" "+")
int3