The bald eagle eats the mouse. The bald eagle is not green. The bald eagle likes the lion. The bald eagle needs the lion. The dog eats the mouse. The dog is cold. The dog is round. The dog does not need the lion. The lion eats the dog. The lion does not need the bald eagle. The lion needs the mouse. The mouse eats the dog. The mouse is not cold. The mouse is green. If someone likes the mouse and the mouse eats the dog then the mouse eats the lion. If the dog is round then the dog needs the mouse. If someone likes the lion then they are young. If the bald eagle needs the lion then the bald eagle eats the mouse. If someone likes the dog then the dog likes the mouse. If someone eats the lion then they do not eat the mouse. If someone eats the dog and the dog needs the mouse then the mouse likes the dog.
The bald eagle eats the mouse.
("bald eagle" "eats" "mouse" "+")
The bald eagle is not green.
("bald eagle" "is" "green" "-")
The bald eagle likes the lion.
("bald eagle" "likes" "lion" "+")
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is round.
("dog" "is" "round" "+")
The dog does not need the lion.
("dog" "needs" "lion" "-")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion does not need the bald eagle.
("lion" "needs" "bald eagle" "-")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is not cold.
("mouse" "is" "cold" "-")
The mouse is green.
("mouse" "is" "green" "+")
If someone likes the mouse and the mouse eats the dog then the mouse eats the lion.
((("someone" "likes" "mouse" "+") ("mouse" "eats" "dog" "+")) -> ("mouse" "eats" "lion" "+"))
If the dog is round then the dog needs the mouse.
((("dog" "is" "round" "+")) -> ("dog" "needs" "mouse" "+"))
If someone likes the lion then they are young.
((("someone" "likes" "lion" "+")) -> ("someone" "is" "young" "+"))
If the bald eagle needs the lion then the bald eagle eats the mouse.
((("bald eagle" "needs" "lion" "+")) -> ("bald eagle" "eats" "mouse" "+"))
If someone likes the dog then the dog likes the mouse.
((("someone" "likes" "dog" "+")) -> ("dog" "likes" "mouse" "+"))
If someone eats the lion then they do not eat the mouse.
((("someone" "eats" "lion" "+")) -> ("someone" "eats" "mouse" "-"))
If someone eats the dog and the dog needs the mouse then the mouse likes the dog.
((("someone" "eats" "dog" "+") ("dog" "needs" "mouse" "+")) -> ("mouse" "likes" "dog" "+"))
The lion does not need the bald eagle.
True
1
proof
[(triple10)]
("lion" "needs" "bald eagle" "-")
triple10
The bald eagle does not like the lion.
False
1
inv-proof
[(triple3)]
("bald eagle" "likes" "lion" "-")
triple3
The bald eagle is young.
True
2
proof
[(((triple3) -> rule3))]
("bald eagle" "is" "young" "+")
((triple3) -> (rule3 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The dog does not need the mouse.
False
2
inv-proof
[(((triple7) -> rule2))]
("dog" "needs" "mouse" "-")
((triple7) -> (rule2 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse likes the dog.
True
4
proof
[(((triple12 ((triple7) -> rule2)) -> rule7) OR ((triple9 ((triple7) -> rule2)) -> rule7))]
("mouse" "likes" "dog" "+")
((triple12 ((triple7) -> (rule2 % int2))) -> (rule7 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
((triple9 ((triple7) -> (rule2 % int2))) -> (rule7 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The mouse does not like the dog.
False
4
inv-proof
[(((triple12 ((triple7) -> rule2)) -> rule7) OR ((triple9 ((triple7) -> rule2)) -> rule7))]
("mouse" "likes" "dog" "-")
((triple12 ((triple7) -> (rule2 % int2))) -> (rule7 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
((triple9 ((triple7) -> (rule2 % int2))) -> (rule7 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The dog likes the mouse.
True
5
proof
[(((((triple12 ((triple7) -> rule2)) -> rule7)) -> rule5) OR ((((triple9 ((triple7) -> rule2)) -> rule7)) -> rule5))]
("dog" "likes" "mouse" "+")
((((triple12 ((triple7) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
((((triple9 ((triple7) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
The dog does not like the mouse.
False
5
inv-proof
[(((((triple12 ((triple7) -> rule2)) -> rule7)) -> rule5) OR ((((triple9 ((triple7) -> rule2)) -> rule7)) -> rule5))]
("dog" "likes" "mouse" "-")
((((triple12 ((triple7) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
((((triple9 ((triple7) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
The mouse eats the lion.
True
7
proof
[(((((((triple12 ((triple7) -> rule2)) -> rule7)) -> rule5) triple12) -> rule1) OR ((((((triple9 ((triple7) -> rule2)) -> rule7)) -> rule5) triple12) -> rule1))]
("mouse" "eats" "lion" "+")
((((((triple12 ((triple7) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) triple12) -> (rule1 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int4
((((((triple9 ((triple7) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) triple12) -> (rule1 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int4
The mouse does not eat the lion.
False
7
inv-proof
[(((((((triple12 ((triple7) -> rule2)) -> rule7)) -> rule5) triple12) -> rule1) OR ((((((triple9 ((triple7) -> rule2)) -> rule7)) -> rule5) triple12) -> rule1))]
("mouse" "eats" "lion" "-")
((((((triple12 ((triple7) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) triple12) -> (rule1 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int4
((((((triple9 ((triple7) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) triple12) -> (rule1 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int4
The mouse does not eat the mouse.
True
8
proof
[(((((((((triple12 ((triple7) -> rule2)) -> rule7)) -> rule5) triple12) -> rule1)) -> rule6) OR ((((((((triple9 ((triple7) -> rule2)) -> rule7)) -> rule5) triple12) -> rule1)) -> rule6))]
("mouse" "eats" "mouse" "-")
((((((((triple12 ((triple7) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule5 % int3)) triple12) -> (rule1 % int2))) -> (rule6 % int1))
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int3
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int4
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int5
((((((((triple9 ((triple7) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule5 % int3)) triple12) -> (rule1 % int2))) -> (rule6 % int1))
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int3
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int4
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int5
The mouse eats the mouse.
False
8
inv-proof
[(((((((((triple12 ((triple7) -> rule2)) -> rule7)) -> rule5) triple12) -> rule1)) -> rule6) OR ((((((((triple9 ((triple7) -> rule2)) -> rule7)) -> rule5) triple12) -> rule1)) -> rule6))]
("mouse" "eats" "mouse" "+")
((((((((triple12 ((triple7) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule5 % int3)) triple12) -> (rule1 % int2))) -> (rule6 % int1))
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int3
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int4
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int5
((((((((triple9 ((triple7) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule5 % int3)) triple12) -> (rule1 % int2))) -> (rule6 % int1))
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int3
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int4
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int5
The mouse is not young.
Unknown
inv-rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "young" "-")
The lion is young.
Unknown
rconc
[@1: The lion is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "young" "+")
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "young" "-")
The lion eats the mouse.
Unknown
random
[@0: The lion eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "mouse" "+")
The bald eagle does not need the bald eagle.
Unknown
inv-random
[@0: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "bald eagle" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The lion needs the dog.
Unknown
random
[@0: The lion needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "dog" "+")
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The bald eagle eats the lion.
Unknown
random
[@0: The bald eagle eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "lion" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The bald eagle needs the mouse.
Unknown
random
[@0: The bald eagle needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "mouse" "+")
@0: The bald eagle eats the mouse.[(triple1 OR ((triple4) -> rule4))] The bald eagle is not green.[(triple2)] The bald eagle likes the lion.[(triple3)] The bald eagle needs the lion.[(triple4)] The dog does not need the lion.[(triple8)] The dog eats the mouse.[(triple5)] The dog is cold.[(triple6)] The dog is round.[(triple7)] The lion does not need the bald eagle.[(triple10)] The lion eats the dog.[(triple9)] The lion needs the mouse.[(triple11)] The mouse eats the dog.[(triple12)] The mouse is green.[(triple14)] The mouse is not cold.[(triple13)] @1: The bald eagle is young.[(((triple3) -> rule3))] The dog needs the mouse.[(((triple7) -> rule2))] @2: The mouse likes the dog.[(((triple12 ((triple7) -> rule2)) -> rule7) OR ((triple9 ((triple7) -> rule2)) -> rule7))] @3: The dog likes the mouse.[(((((triple12 ((triple7) -> rule2)) -> rule7)) -> rule5) OR ((((triple9 ((triple7) -> rule2)) -> rule7)) -> rule5))] @4: The mouse eats the lion.[(((((((triple12 ((triple7) -> rule2)) -> rule7)) -> rule5) triple12) -> rule1) OR ((((((triple9 ((triple7) -> rule2)) -> rule7)) -> rule5) triple12) -> rule1))] @5: The mouse does not eat the mouse.[(((((((((triple12 ((triple7) -> rule2)) -> rule7)) -> rule5) triple12) -> rule1)) -> rule6) OR ((((((((triple9 ((triple7) -> rule2)) -> rule7)) -> rule5) triple12) -> rule1)) -> rule6))]
The bald eagle eats the mouse.
("bald eagle" "eats" "mouse" "+")
triple1
((triple4) -> (rule4 % int1))
The bald eagle eats the mouse.
("bald eagle" "eats" "mouse" "+")
int1
The bald eagle is not green.
("bald eagle" "is" "green" "-")
triple2
The bald eagle likes the lion.
("bald eagle" "likes" "lion" "+")
triple3
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
triple4
The dog does not need the lion.
("dog" "needs" "lion" "-")
triple8
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple5
The dog is cold.
("dog" "is" "cold" "+")
triple6
The dog is round.
("dog" "is" "round" "+")
triple7
The lion does not need the bald eagle.
("lion" "needs" "bald eagle" "-")
triple10
The lion eats the dog.
("lion" "eats" "dog" "+")
triple9
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple11
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple12
The mouse is green.
("mouse" "is" "green" "+")
triple14
The mouse is not cold.
("mouse" "is" "cold" "-")
triple13
The bald eagle is young.
("bald eagle" "is" "young" "+")
((triple3) -> (rule3 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
((triple7) -> (rule2 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
((triple12 ((triple7) -> (rule2 % int2))) -> (rule7 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
((triple9 ((triple7) -> (rule2 % int2))) -> (rule7 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The dog likes the mouse.
("dog" "likes" "mouse" "+")
((((triple12 ((triple7) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
((((triple9 ((triple7) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
The mouse eats the lion.
("mouse" "eats" "lion" "+")
((((((triple12 ((triple7) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) triple12) -> (rule1 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int4
((((((triple9 ((triple7) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) triple12) -> (rule1 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int4
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
((((((((triple12 ((triple7) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule5 % int3)) triple12) -> (rule1 % int2))) -> (rule6 % int1))
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int3
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int4
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int5
((((((((triple9 ((triple7) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule5 % int3)) triple12) -> (rule1 % int2))) -> (rule6 % int1))
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int3
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int4
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int5