The bald eagle is not blue. The dog is rough. The dog visits the lion. The dog visits the tiger. The lion chases the dog. The lion needs the tiger. The lion visits the dog. The tiger chases the bald eagle. The tiger does not chase the dog. The tiger needs the dog. The tiger visits the bald eagle. The tiger visits the lion. If something visits the dog then it is young. If the bald eagle needs the tiger then the bald eagle visits the dog. If something is round then it needs the tiger. If the bald eagle needs the dog and the bald eagle does not visit the lion then the lion chases the dog. If something needs the dog and the dog is nice then the dog does not need the lion. If something visits the lion and the lion needs the bald eagle then the bald eagle needs the tiger. If something is young and it chases the dog then it needs the bald eagle. If something needs the tiger then the tiger is young.
The bald eagle is not blue.
("bald eagle" "is" "blue" "-")
The dog is rough.
("dog" "is" "rough" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The tiger chases the bald eagle.
("tiger" "chases" "bald eagle" "+")
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If something visits the dog then it is young.
((("something" "visits" "dog" "+")) -> ("something" "is" "young" "+"))
If the bald eagle needs the tiger then the bald eagle visits the dog.
((("bald eagle" "needs" "tiger" "+")) -> ("bald eagle" "visits" "dog" "+"))
If something is round then it needs the tiger.
((("something" "is" "round" "+")) -> ("something" "needs" "tiger" "+"))
If the bald eagle needs the dog and the bald eagle does not visit the lion then the lion chases the dog.
((("bald eagle" "needs" "dog" "+") ("bald eagle" "visits" "lion" "~")) -> ("lion" "chases" "dog" "+"))
If something needs the dog and the dog is nice then the dog does not need the lion.
((("something" "needs" "dog" "+") ("dog" "is" "nice" "+")) -> ("dog" "needs" "lion" "-"))
If something visits the lion and the lion needs the bald eagle then the bald eagle needs the tiger.
((("something" "visits" "lion" "+") ("lion" "needs" "bald eagle" "+")) -> ("bald eagle" "needs" "tiger" "+"))
If something is young and it chases the dog then it needs the bald eagle.
((("something" "is" "young" "+") ("something" "chases" "dog" "+")) -> ("something" "needs" "bald eagle" "+"))
If something needs the tiger then the tiger is young.
((("something" "needs" "tiger" "+")) -> ("tiger" "is" "young" "+"))
The tiger does not chase the dog.
True
1
proof
[(triple9)]
("tiger" "chases" "dog" "-")
triple9
The tiger chases the dog.
False
1
inv-proof
[(triple9)]
("tiger" "chases" "dog" "+")
triple9
The tiger is young.
True
2
proof
[(((triple6) -> rule8) OR ((((triple12 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6)) -> rule8) OR ((((triple3 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6)) -> rule8))]
("tiger" "is" "young" "+")
((triple6) -> (rule8 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
((((triple12 ((((triple7) -> (rule1 % int4)) triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
((((triple3 ((((triple7) -> (rule1 % int4)) triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The lion is not young.
False
2
inv-proof
[(((triple7) -> rule1))]
("lion" "is" "young" "-")
((triple7) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion needs the bald eagle.
True
4
proof
[(((((triple7) -> rule1) triple5) -> rule7))]
("lion" "needs" "bald eagle" "+")
((((triple7) -> (rule1 % int2)) triple5) -> (rule7 % int1))
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion does not need the bald eagle.
False
4
inv-proof
[(((((triple7) -> rule1) triple5) -> rule7))]
("lion" "needs" "bald eagle" "-")
((((triple7) -> (rule1 % int2)) triple5) -> (rule7 % int1))
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The bald eagle needs the tiger.
True
6
proof
[(((triple12 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6) OR ((triple3 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6))]
("bald eagle" "needs" "tiger" "+")
((triple12 ((((triple7) -> (rule1 % int3)) triple5) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int1
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
((triple3 ((((triple7) -> (rule1 % int3)) triple5) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int1
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The bald eagle does not need the tiger.
False
6
inv-proof
[(((triple12 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6) OR ((triple3 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6))]
("bald eagle" "needs" "tiger" "-")
((triple12 ((((triple7) -> (rule1 % int3)) triple5) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int1
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
((triple3 ((((triple7) -> (rule1 % int3)) triple5) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int1
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The bald eagle visits the dog.
True
7
proof
[(((((triple12 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6)) -> rule2) OR ((((triple3 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6)) -> rule2))]
("bald eagle" "visits" "dog" "+")
((((triple12 ((((triple7) -> (rule1 % int4)) triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
((((triple3 ((((triple7) -> (rule1 % int4)) triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The bald eagle does not visit the dog.
False
7
inv-proof
[(((((triple12 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6)) -> rule2) OR ((((triple3 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6)) -> rule2))]
("bald eagle" "visits" "dog" "-")
((((triple12 ((((triple7) -> (rule1 % int4)) triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
((((triple3 ((((triple7) -> (rule1 % int4)) triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The bald eagle is young.
True
8
proof
[(((((((triple12 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6)) -> rule2)) -> rule1) OR ((((((triple3 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6)) -> rule2)) -> rule1))]
("bald eagle" "is" "young" "+")
((((((triple12 ((((triple7) -> (rule1 % int5)) triple5) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int2
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int3
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
((((((triple3 ((((triple7) -> (rule1 % int5)) triple5) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int2
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int3
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
The bald eagle is not young.
False
8
inv-proof
[(((((((triple12 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6)) -> rule2)) -> rule1) OR ((((((triple3 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6)) -> rule2)) -> rule1))]
("bald eagle" "is" "young" "-")
((((((triple12 ((((triple7) -> (rule1 % int5)) triple5) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int2
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int3
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
((((((triple3 ((((triple7) -> (rule1 % int5)) triple5) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int2
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int3
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
The tiger does not need the bald eagle.
Unknown
inv-rconc
[@1: The tiger needs the bald eagle.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "needs" "bald eagle" "-")
The dog needs the bald eagle.
Unknown
rconc
[@1: The dog needs the bald eagle.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "needs" "bald eagle" "+")
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The bald eagle needs the bald eagle.
Unknown
rconc
[@1: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bald eagle" "needs" "bald eagle" "+")
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "young" "-")
The dog needs the tiger.
Unknown
rconc
[@1: The dog needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "needs" "tiger" "+")
The lion is not blue.
Unknown
inv-random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The bald eagle does not chase the bald eagle.
Unknown
inv-random
[@0: The bald eagle chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "bald eagle" "-")
The lion needs the dog.
Unknown
random
[@0: The lion needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "dog" "+")
@0: The bald eagle is not blue.[(triple1)] The dog is rough.[(triple2)] The dog visits the lion.[(triple3)] The dog visits the tiger.[(triple4)] The lion chases the dog.[(triple5)] The lion needs the tiger.[(triple6)] The lion visits the dog.[(triple7)] The tiger chases the bald eagle.[(triple8)] The tiger does not chase the dog.[(triple9)] The tiger needs the dog.[(triple10)] The tiger visits the bald eagle.[(triple11)] The tiger visits the lion.[(triple12)] @1: The lion is young.[(((triple7) -> rule1))] The tiger is young.[(((triple6) -> rule8) OR ((((triple12 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6)) -> rule8) OR ((((triple3 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6)) -> rule8))] @2: The lion needs the bald eagle.[(((((triple7) -> rule1) triple5) -> rule7))] @3: The bald eagle needs the tiger.[(((triple12 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6) OR ((triple3 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6))] @4: The bald eagle visits the dog.[(((((triple12 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6)) -> rule2) OR ((((triple3 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6)) -> rule2))] @5: The bald eagle is young.[(((((((triple12 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6)) -> rule2)) -> rule1) OR ((((((triple3 ((((triple7) -> rule1) triple5) -> rule7)) -> rule6)) -> rule2)) -> rule1))]
The bald eagle is not blue.
("bald eagle" "is" "blue" "-")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The dog visits the lion.
("dog" "visits" "lion" "+")
triple3
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple4
The lion chases the dog.
("lion" "chases" "dog" "+")
triple5
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple6
The lion visits the dog.
("lion" "visits" "dog" "+")
triple7
The tiger chases the bald eagle.
("tiger" "chases" "bald eagle" "+")
triple8
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
triple9
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple10
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
triple11
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple12
The lion is young.
("lion" "is" "young" "+")
((triple7) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
((triple6) -> (rule8 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
((((triple12 ((((triple7) -> (rule1 % int4)) triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
((((triple3 ((((triple7) -> (rule1 % int4)) triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
((((triple7) -> (rule1 % int2)) triple5) -> (rule7 % int1))
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
((triple12 ((((triple7) -> (rule1 % int3)) triple5) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int1
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
((triple3 ((((triple7) -> (rule1 % int3)) triple5) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int1
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
((((triple12 ((((triple7) -> (rule1 % int4)) triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
((((triple3 ((((triple7) -> (rule1 % int4)) triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The bald eagle is young.
("bald eagle" "is" "young" "+")
((((((triple12 ((((triple7) -> (rule1 % int5)) triple5) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int2
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int3
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
((((((triple3 ((((triple7) -> (rule1 % int5)) triple5) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int2
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int3
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5