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