The bald eagle chases the lion. The dog is not big. The dog needs the lion. The lion eats the bald eagle. The lion is not big. The lion is not blue. The mouse chases the bald eagle. The mouse does not chase the lion. The mouse eats the bald eagle. The mouse is blue. The mouse is green. The mouse is round. The mouse does not need the bald eagle. The mouse needs the dog. The mouse needs the lion. If something eats the bald eagle then the bald eagle chases the mouse. If the bald eagle chases the mouse then the bald eagle is green. If something eats the bald eagle then it needs the dog. If something is blue then it eats the dog. If something eats the dog then the dog eats the bald eagle. If something needs the lion and it is green then the lion needs the dog. If something chases the lion and it is not green then it chases the bald eagle. If the dog chases the bald eagle then the bald eagle eats the lion.
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
The dog is not big.
("dog" "is" "big" "-")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
The lion is not big.
("lion" "is" "big" "-")
The lion is not blue.
("lion" "is" "blue" "-")
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse does not need the bald eagle.
("mouse" "needs" "bald eagle" "-")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
If something eats the bald eagle then the bald eagle chases the mouse.
((("something" "eats" "bald eagle" "+")) -> ("bald eagle" "chases" "mouse" "+"))
If the bald eagle chases the mouse then the bald eagle is green.
((("bald eagle" "chases" "mouse" "+")) -> ("bald eagle" "is" "green" "+"))
If something eats the bald eagle then it needs the dog.
((("something" "eats" "bald eagle" "+")) -> ("something" "needs" "dog" "+"))
If something is blue then it eats the dog.
((("something" "is" "blue" "+")) -> ("something" "eats" "dog" "+"))
If something eats the dog then the dog eats the bald eagle.
((("something" "eats" "dog" "+")) -> ("dog" "eats" "bald eagle" "+"))
If something needs the lion and it is green then the lion needs the dog.
((("something" "needs" "lion" "+") ("something" "is" "green" "+")) -> ("lion" "needs" "dog" "+"))
If something chases the lion and it is not green then it chases the bald eagle.
((("something" "chases" "lion" "+") ("something" "is" "green" "~")) -> ("something" "chases" "bald eagle" "+"))
If the dog chases the bald eagle then the bald eagle eats the lion.
((("dog" "chases" "bald eagle" "+")) -> ("bald eagle" "eats" "lion" "+"))
The mouse chases the bald eagle.
True
1
proof
[(triple7)]
("mouse" "chases" "bald eagle" "+")
triple7
The mouse is not round.
False
1
inv-proof
[(triple12)]
("mouse" "is" "round" "-")
triple12
The mouse eats the dog.
True
2
proof
[(((triple10) -> rule4))]
("mouse" "eats" "dog" "+")
((triple10) -> (rule4 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse does not eat the dog.
False
2
inv-proof
[(((triple10) -> rule4))]
("mouse" "eats" "dog" "-")
((triple10) -> (rule4 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The dog eats the bald eagle.
True
3
proof
[(((((triple10) -> rule4)) -> rule5))]
("dog" "eats" "bald eagle" "+")
((((triple10) -> (rule4 % int2))) -> (rule5 % int1))
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int2
The bald eagle is not green.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2) OR ((((triple9) -> rule1)) -> rule2) OR ((((((((triple10) -> rule4)) -> rule5)) -> rule1)) -> rule2))]
("bald eagle" "is" "green" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle is green.
("bald eagle" "is" "green" "+")
int1
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int2
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle is green.
("bald eagle" "is" "green" "+")
int1
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int2
((((((((triple10) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle is green.
("bald eagle" "is" "green" "+")
int1
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int2
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int3
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int4
The dog needs the dog.
True
4
proof
[(((((((triple10) -> rule4)) -> rule5)) -> rule3))]
("dog" "needs" "dog" "+")
((((((triple10) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3
The dog does not need the dog.
False
4
inv-proof
[(((((((triple10) -> rule4)) -> rule5)) -> rule3))]
("dog" "needs" "dog" "-")
((((((triple10) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3
The dog does not eat the dog.
Unknown
inv-rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "eats" "dog" "-")
The dog chases the bald eagle.
Unknown
rconc
[@1: The dog chases the bald eagle.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "chases" "bald eagle" "+")
The lion does not chase the bald eagle.
Unknown
inv-rconc
[@1: The lion chases the bald eagle.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "chases" "bald eagle" "-")
The bald eagle chases the bald eagle.
Unknown
rconc
[@1: The bald eagle chases the bald eagle.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bald eagle" "chases" "bald eagle" "+")
The lion does not chase the mouse.
Unknown
inv-random
[@0: The lion chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "mouse" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
@0: The bald eagle chases the lion.[(triple1)] The dog is not big.[(triple2)] The dog needs the lion.[(triple3)] The lion eats the bald eagle.[(triple4)] The lion is not big.[(triple5)] The lion is not blue.[(triple6)] The mouse chases the bald eagle.[(triple7)] The mouse does not chase the lion.[(triple8)] The mouse does not need the bald eagle.[(triple13)] The mouse eats the bald eagle.[(triple9)] The mouse is blue.[(triple10)] The mouse is green.[(triple11)] The mouse is round.[(triple12)] The mouse needs the dog.[(triple14 OR ((triple9) -> rule3))] The mouse needs the lion.[(triple15)] @1: The bald eagle chases the mouse.[(((triple4) -> rule1) OR ((triple9) -> rule1) OR ((((((triple10) -> rule4)) -> rule5)) -> rule1))] The lion needs the dog.[(((triple4) -> rule3) OR ((triple15 triple11) -> rule6))] The mouse eats the dog.[(((triple10) -> rule4))] @2: The bald eagle is green.[(((((triple4) -> rule1)) -> rule2) OR ((((triple9) -> rule1)) -> rule2) OR ((((((((triple10) -> rule4)) -> rule5)) -> rule1)) -> rule2))] The dog eats the bald eagle.[(((((triple10) -> rule4)) -> rule5))] @3: The dog needs the dog.[(((((((triple10) -> rule4)) -> rule5)) -> rule3))]
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
triple1
The dog is not big.
("dog" "is" "big" "-")
triple2
The dog needs the lion.
("dog" "needs" "lion" "+")
triple3
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
triple4
The lion is not big.
("lion" "is" "big" "-")
triple5
The lion is not blue.
("lion" "is" "blue" "-")
triple6
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
triple7
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
triple8
The mouse does not need the bald eagle.
("mouse" "needs" "bald eagle" "-")
triple13
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
triple9
The mouse is blue.
("mouse" "is" "blue" "+")
triple10
The mouse is green.
("mouse" "is" "green" "+")
triple11
The mouse is round.
("mouse" "is" "round" "+")
triple12
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple14
((triple9) -> (rule3 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple15
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
((triple4) -> (rule1 % int1))
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int1
((triple9) -> (rule1 % int1))
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int1
((((((triple10) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int1
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3
The lion needs the dog.
("lion" "needs" "dog" "+")
((triple4) -> (rule3 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
((triple15 triple11) -> (rule6 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
((triple10) -> (rule4 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The bald eagle is green.
("bald eagle" "is" "green" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle is green.
("bald eagle" "is" "green" "+")
int1
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int2
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle is green.
("bald eagle" "is" "green" "+")
int1
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int2
((((((((triple10) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle is green.
("bald eagle" "is" "green" "+")
int1
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
int2
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int3
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int4
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
((((triple10) -> (rule4 % int2))) -> (rule5 % int1))
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
((((((triple10) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3