The bald eagle chases the bear. The bear needs the tiger. The dog chases the bald eagle. The tiger chases the bear. If something needs the bear then it is blue. If the bear needs the tiger then the tiger is blue. If something needs the bear and the bear does not like the dog then the bear likes the tiger. If the tiger chases the dog then the dog is not rough. If something is blue then it chases the dog. If something is blue then it needs the dog.
The bald eagle chases the bear.
("bald eagle" "chases" "bear" "+")
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
If something needs the bear then it is blue.
((("something" "needs" "bear" "+")) -> ("something" "is" "blue" "+"))
If the bear needs the tiger then the tiger is blue.
((("bear" "needs" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
If something needs the bear and the bear does not like the dog then the bear likes the tiger.
((("something" "needs" "bear" "+") ("bear" "likes" "dog" "~")) -> ("bear" "likes" "tiger" "+"))
If the tiger chases the dog then the dog is not rough.
((("tiger" "chases" "dog" "+")) -> ("dog" "is" "rough" "-"))
If something is blue then it chases the dog.
((("something" "is" "blue" "+")) -> ("something" "chases" "dog" "+"))
If something is blue then it needs the dog.
((("something" "is" "blue" "+")) -> ("something" "needs" "dog" "+"))
The bald eagle chases the bear.
True
1
proof
[(triple1)]
("bald eagle" "chases" "bear" "+")
triple1
The bald eagle does not chase the bear.
False
1
inv-proof
[(triple1)]
("bald eagle" "chases" "bear" "-")
triple1
The tiger is blue.
True
2
proof
[(((triple2) -> rule2))]
("tiger" "is" "blue" "+")
((triple2) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is not blue.
False
2
inv-proof
[(((triple2) -> rule2))]
("tiger" "is" "blue" "-")
((triple2) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger chases the dog.
True
3
proof
[(((((triple2) -> rule2)) -> rule5))]
("tiger" "chases" "dog" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger does not chase the dog.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule5))]
("tiger" "chases" "dog" "-")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The dog is not rough.
True
4
proof
[(((((((triple2) -> rule2)) -> rule5)) -> rule4))]
("dog" "is" "rough" "-")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The dog is not rough.
("dog" "is" "rough" "-")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The dog is rough.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule5)) -> rule4))]
("dog" "is" "rough" "+")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The dog is not rough.
("dog" "is" "rough" "-")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The bear is not blue.
Unknown
inv-rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "blue" "-")
The dog chases the dog.
Unknown
rconc
[@2: The dog chases the dog.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("dog" "chases" "dog" "+")
The bear does not like the tiger.
Unknown
inv-rconc
[@1: The bear likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "likes" "tiger" "-")
The dog needs the dog.
Unknown
rconc
[@2: The dog needs the dog.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("dog" "needs" "dog" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The tiger likes the bear.
Unknown
random
[@0: The tiger likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "bear" "+")
The bear does not chase the tiger.
Unknown
inv-random
[@0: The bear chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "tiger" "-")
The bald eagle needs the bald eagle.
Unknown
random
[@0: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "bald eagle" "+")
@0: The bald eagle chases the bear.[(triple1)] The bear needs the tiger.[(triple2)] The dog chases the bald eagle.[(triple3)] The tiger chases the bear.[(triple4)] @1: The tiger is blue.[(((triple2) -> rule2))] @2: The tiger chases the dog.[(((((triple2) -> rule2)) -> rule5))] The tiger needs the dog.[(((((triple2) -> rule2)) -> rule6))] @3: The dog is not rough.[(((((((triple2) -> rule2)) -> rule5)) -> rule4))]
The bald eagle chases the bear.
("bald eagle" "chases" "bear" "+")
triple1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple2
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
triple3
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple4
The tiger is blue.
("tiger" "is" "blue" "+")
((triple2) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The dog is not rough.
("dog" "is" "rough" "-")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The dog is not rough.
("dog" "is" "rough" "-")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3