The cat needs the dog. The cow is big. The dog chases the cow. The dog likes the cat. The dog needs the cat. The tiger chases the cow. The tiger needs the cat. If something needs the cat then the cat is nice. If something needs the cat and the cat is nice then it needs the cow. If something is young then it chases the dog. If something needs the dog then it likes the dog. If something likes the dog and the dog needs the cat then the dog is young. If something likes the cat then it chases the cat. If something needs the dog then it likes the cow. If the cow is blue and the cow likes the tiger then the cow chases the tiger.
The cat needs the dog.
("cat" "needs" "dog" "+")
The cow is big.
("cow" "is" "big" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
If something needs the cat then the cat is nice.
((("something" "needs" "cat" "+")) -> ("cat" "is" "nice" "+"))
If something needs the cat and the cat is nice then it needs the cow.
((("something" "needs" "cat" "+") ("cat" "is" "nice" "+")) -> ("something" "needs" "cow" "+"))
If something is young then it chases the dog.
((("something" "is" "young" "+")) -> ("something" "chases" "dog" "+"))
If something needs the dog then it likes the dog.
((("something" "needs" "dog" "+")) -> ("something" "likes" "dog" "+"))
If something likes the dog and the dog needs the cat then the dog is young.
((("something" "likes" "dog" "+") ("dog" "needs" "cat" "+")) -> ("dog" "is" "young" "+"))
If something likes the cat then it chases the cat.
((("something" "likes" "cat" "+")) -> ("something" "chases" "cat" "+"))
If something needs the dog then it likes the cow.
((("something" "needs" "dog" "+")) -> ("something" "likes" "cow" "+"))
If the cow is blue and the cow likes the tiger then the cow chases the tiger.
((("cow" "is" "blue" "+") ("cow" "likes" "tiger" "+")) -> ("cow" "chases" "tiger" "+"))
The dog likes the cat.
True
1
proof
[(triple4)]
("dog" "likes" "cat" "+")
triple4
The cow is not big.
False
1
inv-proof
[(triple2)]
("cow" "is" "big" "-")
triple2
The cat likes the cow.
True
2
proof
[(((triple1) -> rule7))]
("cat" "likes" "cow" "+")
((triple1) -> (rule7 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat does not like the dog.
False
2
inv-proof
[(((triple1) -> rule4))]
("cat" "likes" "dog" "-")
((triple1) -> (rule4 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The dog needs the cow.
True
4
proof
[(((triple5 ((triple5) -> rule1)) -> rule2) OR ((triple5 ((triple7) -> rule1)) -> rule2))]
("dog" "needs" "cow" "+")
((triple5 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
((triple5 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The tiger does not need the cow.
False
4
inv-proof
[(((triple7 ((triple5) -> rule1)) -> rule2) OR ((triple7 ((triple7) -> rule1)) -> rule2))]
("tiger" "needs" "cow" "-")
((triple7 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
((triple7 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The dog chases the dog.
True
5
proof
[(((((((triple1) -> rule4) triple5) -> rule5)) -> rule3))]
("dog" "chases" "dog" "+")
((((((triple1) -> (rule4 % int3)) triple5) -> (rule5 % int2))) -> (rule3 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The cat likes the dog.
("cat" "likes" "dog" "+")
int3
The dog does not chase the dog.
False
5
inv-proof
[(((((((triple1) -> rule4) triple5) -> rule5)) -> rule3))]
("dog" "chases" "dog" "-")
((((((triple1) -> (rule4 % int3)) triple5) -> (rule5 % int2))) -> (rule3 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The cat likes the dog.
("cat" "likes" "dog" "+")
int3
The dog does not like the cow.
Unknown
inv-rconc
[@1: The dog likes the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "likes" "cow" "-")
The cow likes the dog.
Unknown
rconc
[@1: The cow likes the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "likes" "dog" "+")
The cow does not chase the tiger.
Unknown
inv-rconc
[@1: The cow chases the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "chases" "tiger" "-")
The tiger chases the dog.
Unknown
rconc
[@1: The tiger chases the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "chases" "dog" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The cow likes the cat.
Unknown
random
[@0: The cow likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cat" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The cat needs the tiger.
Unknown
random
[@0: The cat needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "tiger" "+")
@0: The cat needs the dog.[(triple1)] The cow is big.[(triple2)] The dog chases the cow.[(triple3)] The dog likes the cat.[(triple4)] The dog needs the cat.[(triple5)] The tiger chases the cow.[(triple6)] The tiger needs the cat.[(triple7)] @1: The cat is nice.[(((triple5) -> rule1) OR ((triple7) -> rule1))] The cat likes the cow.[(((triple1) -> rule7))] The cat likes the dog.[(((triple1) -> rule4))] The dog chases the cat.[(((triple4) -> rule6))] @2: The dog is young.[(((((triple1) -> rule4) triple5) -> rule5))] The dog needs the cow.[(((triple5 ((triple5) -> rule1)) -> rule2) OR ((triple5 ((triple7) -> rule1)) -> rule2))] The tiger needs the cow.[(((triple7 ((triple5) -> rule1)) -> rule2) OR ((triple7 ((triple7) -> rule1)) -> rule2))] @3: The dog chases the dog.[(((((((triple1) -> rule4) triple5) -> rule5)) -> rule3))]
The cat needs the dog.
("cat" "needs" "dog" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The dog chases the cow.
("dog" "chases" "cow" "+")
triple3
The dog likes the cat.
("dog" "likes" "cat" "+")
triple4
The dog needs the cat.
("dog" "needs" "cat" "+")
triple5
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple6
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple7
The cat is nice.
("cat" "is" "nice" "+")
((triple5) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
((triple7) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
((triple1) -> (rule7 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
((triple1) -> (rule4 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The dog chases the cat.
("dog" "chases" "cat" "+")
((triple4) -> (rule6 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((((triple1) -> (rule4 % int2)) triple5) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
int2
The dog needs the cow.
("dog" "needs" "cow" "+")
((triple5 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
((triple5 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
((triple7 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
((triple7 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The dog chases the dog.
("dog" "chases" "dog" "+")
((((((triple1) -> (rule4 % int3)) triple5) -> (rule5 % int2))) -> (rule3 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The cat likes the dog.
("cat" "likes" "dog" "+")
int3