The bald eagle needs the tiger. The dog visits the tiger. The mouse is cold. The tiger is not green. If something visits the tiger then it chases the bald eagle. If the tiger needs the mouse then the mouse needs the bald eagle. If something chases the mouse then it does not visit the bald eagle. If something visits the dog then it is red. If something needs the bald eagle then the bald eagle chases the dog. If something chases the bald eagle and the bald eagle needs the tiger then the tiger needs the bald eagle.
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The tiger is not green.
("tiger" "is" "green" "-")
If something visits the tiger then it chases the bald eagle.
((("something" "visits" "tiger" "+")) -> ("something" "chases" "bald eagle" "+"))
If the tiger needs the mouse then the mouse needs the bald eagle.
((("tiger" "needs" "mouse" "+")) -> ("mouse" "needs" "bald eagle" "+"))
If something chases the mouse then it does not visit the bald eagle.
((("something" "chases" "mouse" "+")) -> ("something" "visits" "bald eagle" "-"))
If something visits the dog then it is red.
((("something" "visits" "dog" "+")) -> ("something" "is" "red" "+"))
If something needs the bald eagle then the bald eagle chases the dog.
((("something" "needs" "bald eagle" "+")) -> ("bald eagle" "chases" "dog" "+"))
If something chases the bald eagle and the bald eagle needs the tiger then the tiger needs the bald eagle.
((("something" "chases" "bald eagle" "+") ("bald eagle" "needs" "tiger" "+")) -> ("tiger" "needs" "bald eagle" "+"))
The tiger is not green.
True
1
proof
[(triple4)]
("tiger" "is" "green" "-")
triple4
The tiger is green.
False
1
inv-proof
[(triple4)]
("tiger" "is" "green" "+")
triple4
The dog chases the bald eagle.
True
2
proof
[(((triple2) -> rule1))]
("dog" "chases" "bald eagle" "+")
((triple2) -> (rule1 % int1))
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int1
The dog does not chase the bald eagle.
False
2
inv-proof
[(((triple2) -> rule1))]
("dog" "chases" "bald eagle" "-")
((triple2) -> (rule1 % int1))
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int1
The tiger needs the bald eagle.
True
4
proof
[(((((triple2) -> rule1) triple1) -> rule6))]
("tiger" "needs" "bald eagle" "+")
((((triple2) -> (rule1 % int2)) triple1) -> (rule6 % int1))
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int1
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int2
The tiger does not need the bald eagle.
False
4
inv-proof
[(((((triple2) -> rule1) triple1) -> rule6))]
("tiger" "needs" "bald eagle" "-")
((((triple2) -> (rule1 % int2)) triple1) -> (rule6 % int1))
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int1
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int2
The bald eagle chases the dog.
True
5
proof
[(((((((triple2) -> rule1) triple1) -> rule6)) -> rule5))]
("bald eagle" "chases" "dog" "+")
((((((triple2) -> (rule1 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
The bald eagle chases the dog.
("bald eagle" "chases" "dog" "+")
int1
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int2
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int3
The bald eagle does not chase the dog.
False
5
inv-proof
[(((((((triple2) -> rule1) triple1) -> rule6)) -> rule5))]
("bald eagle" "chases" "dog" "-")
((((((triple2) -> (rule1 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
The bald eagle chases the dog.
("bald eagle" "chases" "dog" "+")
int1
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int2
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int3
The bald eagle is not red.
Unknown
inv-rconc
[@1: The bald eagle is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "is" "red" "-")
The mouse chases the bald eagle.
Unknown
rconc
[@1: The mouse chases the bald eagle.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "chases" "bald eagle" "+")
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "red" "-")
The dog is red.
Unknown
rconc
[@1: The dog is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "red" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The dog chases the tiger.
Unknown
random
[@0: The dog chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "tiger" "+")
The tiger does not need the dog.
Unknown
inv-random
[@0: The tiger needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "dog" "-")
The bald eagle is green.
Unknown
random
[@0: The bald eagle is green.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "green" "+")
@0: The bald eagle needs the tiger.[(triple1)] The dog visits the tiger.[(triple2)] The mouse is cold.[(triple3)] The tiger is not green.[(triple4)] @1: The dog chases the bald eagle.[(((triple2) -> rule1))] @2: The tiger needs the bald eagle.[(((((triple2) -> rule1) triple1) -> rule6))] @3: The bald eagle chases the dog.[(((((((triple2) -> rule1) triple1) -> rule6)) -> rule5))]
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
triple1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple2
The mouse is cold.
("mouse" "is" "cold" "+")
triple3
The tiger is not green.
("tiger" "is" "green" "-")
triple4
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
((triple2) -> (rule1 % int1))
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int1
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
((((triple2) -> (rule1 % int2)) triple1) -> (rule6 % int1))
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int1
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int2
The bald eagle chases the dog.
("bald eagle" "chases" "dog" "+")
((((((triple2) -> (rule1 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
The bald eagle chases the dog.
("bald eagle" "chases" "dog" "+")
int1
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int2
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int3