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