The dog chases the tiger. The dog is blue. The dog is green. The dog is nice. The dog is rough. The dog is young. The dog likes the tiger. The dog needs the tiger. The tiger chases the dog. The tiger is blue. The tiger is green. The tiger is nice. The tiger is rough. The tiger is young. The tiger likes the dog. The tiger needs the dog. If someone needs the dog then they like the tiger. If someone chases the dog and the dog chases the tiger then the dog needs the tiger. If someone likes the tiger then they chase the tiger. If someone chases the dog and the dog is young then the dog is nice. If someone chases the tiger then they need the tiger. If someone needs the dog then they chase the dog.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If someone needs the dog then they like the tiger.
((("someone" "needs" "dog" "+")) -> ("someone" "likes" "tiger" "+"))
If someone chases the dog and the dog chases the tiger then the dog needs the tiger.
((("someone" "chases" "dog" "+") ("dog" "chases" "tiger" "+")) -> ("dog" "needs" "tiger" "+"))
If someone likes the tiger then they chase the tiger.
((("someone" "likes" "tiger" "+")) -> ("someone" "chases" "tiger" "+"))
If someone chases the dog and the dog is young then the dog is nice.
((("someone" "chases" "dog" "+") ("dog" "is" "young" "+")) -> ("dog" "is" "nice" "+"))
If someone chases the tiger then they need the tiger.
((("someone" "chases" "tiger" "+")) -> ("someone" "needs" "tiger" "+"))
If someone needs the dog then they chase the dog.
((("someone" "needs" "dog" "+")) -> ("someone" "chases" "dog" "+"))
The dog is nice.
True
1
proof
[(triple4 OR ((triple9 triple6) -> rule4) OR ((((triple16) -> rule6) triple6) -> rule4))]
("dog" "is" "nice" "+")
triple4
((triple9 triple6) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
((((triple16) -> (rule6 % int2)) triple6) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The dog is not young.
False
1
inv-proof
[(triple6)]
("dog" "is" "young" "-")
triple6
The tiger likes the tiger.
True
2
proof
[(((triple16) -> rule1))]
("tiger" "likes" "tiger" "+")
((triple16) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger does not like the tiger.
False
2
inv-proof
[(((triple16) -> rule1))]
("tiger" "likes" "tiger" "-")
((triple16) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger chases the tiger.
True
3
proof
[(((((triple16) -> rule1)) -> rule3))]
("tiger" "chases" "tiger" "+")
((((triple16) -> (rule1 % int2))) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger does not chase the tiger.
False
3
inv-proof
[(((((triple16) -> rule1)) -> rule3))]
("tiger" "chases" "tiger" "-")
((((triple16) -> (rule1 % int2))) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger needs the tiger.
True
4
proof
[(((((((triple16) -> rule1)) -> rule3)) -> rule5))]
("tiger" "needs" "tiger" "+")
((((((triple16) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger does not need the tiger.
False
4
inv-proof
[(((((((triple16) -> rule1)) -> rule3)) -> rule5))]
("tiger" "needs" "tiger" "-")
((((((triple16) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "chases" "dog" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The dog chases the tiger.[(triple1 OR ((triple7) -> rule3))] The dog is blue.[(triple2)] The dog is green.[(triple3)] The dog is nice.[(triple4 OR ((triple9 triple6) -> rule4) OR ((((triple16) -> rule6) triple6) -> rule4))] The dog is rough.[(triple5)] The dog is young.[(triple6)] The dog likes the tiger.[(triple7)] The dog needs the tiger.[(triple8 OR ((triple1) -> rule5) OR ((triple9 triple1) -> rule2) OR ((((triple7) -> rule3)) -> rule5) OR ((triple9 ((triple7) -> rule3)) -> rule2) OR ((((triple16) -> rule6) triple1) -> rule2) OR ((((triple16) -> rule6) ((triple7) -> rule3)) -> rule2))] The tiger chases the dog.[(triple9 OR ((triple16) -> rule6))] The tiger is blue.[(triple10)] The tiger is green.[(triple11)] The tiger is nice.[(triple12)] The tiger is rough.[(triple13)] The tiger is young.[(triple14)] The tiger likes the dog.[(triple15)] The tiger needs the dog.[(triple16)] @1: The tiger likes the tiger.[(((triple16) -> rule1))] @2: The tiger chases the tiger.[(((((triple16) -> rule1)) -> rule3))] @3: The tiger needs the tiger.[(((((((triple16) -> rule1)) -> rule3)) -> rule5))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
((triple7) -> (rule3 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog is green.
("dog" "is" "green" "+")
triple3
The dog is nice.
("dog" "is" "nice" "+")
triple4
((triple9 triple6) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
((((triple16) -> (rule6 % int2)) triple6) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
triple5
The dog is young.
("dog" "is" "young" "+")
triple6
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple7
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple8
((triple1) -> (rule5 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
((triple9 triple1) -> (rule2 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule5 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
((triple9 ((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
((((triple16) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
((((triple16) -> (rule6 % int3)) ((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int3
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple9
((triple16) -> (rule6 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The tiger is green.
("tiger" "is" "green" "+")
triple11
The tiger is nice.
("tiger" "is" "nice" "+")
triple12
The tiger is rough.
("tiger" "is" "rough" "+")
triple13
The tiger is young.
("tiger" "is" "young" "+")
triple14
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple15
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple16
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple16) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((((triple16) -> (rule1 % int2))) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((((triple16) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3