The bald eagle needs the dog. The bear sees the dog. The dog is round. The dog sees the bald eagle. The lion is blue. The lion sees the bear. The lion visits the bear. If someone needs the bear then they are round. If someone is round then they need the lion. If someone is nice then they need the dog. If someone needs the bald eagle then the bald eagle visits the bear. If someone needs the bear then the bear is round. If someone needs the lion then they need the bear. If the lion does not visit the bear and the lion does not need the bear then the lion is not blue. If the lion visits the bald eagle and the bald eagle sees the bear then the lion is not blue. If the bear is young and the bear does not need the lion then the bear sees the dog.
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The dog is round.
("dog" "is" "round" "+")
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
If someone needs the bear then they are round.
((("someone" "needs" "bear" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they need the lion.
((("someone" "is" "round" "+")) -> ("someone" "needs" "lion" "+"))
If someone is nice then they need the dog.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "dog" "+"))
If someone needs the bald eagle then the bald eagle visits the bear.
((("someone" "needs" "bald eagle" "+")) -> ("bald eagle" "visits" "bear" "+"))
If someone needs the bear then the bear is round.
((("someone" "needs" "bear" "+")) -> ("bear" "is" "round" "+"))
If someone needs the lion then they need the bear.
((("someone" "needs" "lion" "+")) -> ("someone" "needs" "bear" "+"))
If the lion does not visit the bear and the lion does not need the bear then the lion is not blue.
((("lion" "visits" "bear" "~") ("lion" "needs" "bear" "~")) -> ("lion" "is" "blue" "-"))
If the lion visits the bald eagle and the bald eagle sees the bear then the lion is not blue.
((("lion" "visits" "bald eagle" "+") ("bald eagle" "sees" "bear" "+")) -> ("lion" "is" "blue" "-"))
If the bear is young and the bear does not need the lion then the bear sees the dog.
((("bear" "is" "young" "+") ("bear" "needs" "lion" "~")) -> ("bear" "sees" "dog" "+"))
The bear sees the dog.
True
1
proof
[(triple2)]
("bear" "sees" "dog" "+")
triple2
The lion does not see the bear.
False
1
inv-proof
[(triple6)]
("lion" "sees" "bear" "-")
triple6
The dog needs the lion.
True
2
proof
[(((triple3) -> rule2))]
("dog" "needs" "lion" "+")
((triple3) -> (rule2 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The dog does not need the lion.
False
2
inv-proof
[(((triple3) -> rule2))]
("dog" "needs" "lion" "-")
((triple3) -> (rule2 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The dog needs the bear.
True
3
proof
[(((((triple3) -> rule2)) -> rule6))]
("dog" "needs" "bear" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The dog does not need the bear.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule6))]
("dog" "needs" "bear" "-")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The bear is round.
True
4
proof
[(((((((triple3) -> rule2)) -> rule6)) -> rule5))]
("bear" "is" "round" "+")
((((((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
int2
The dog needs the lion.
("dog" "needs" "lion" "+")
int3
The bear is not round.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule6)) -> rule5))]
("bear" "is" "round" "-")
((((((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
int2
The dog needs the lion.
("dog" "needs" "lion" "+")
int3
The bear needs the lion.
True
5
proof
[(((((((((triple3) -> rule2)) -> rule6)) -> rule5)) -> rule2))]
("bear" "needs" "lion" "+")
((((((((triple3) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The dog needs the bear.
("dog" "needs" "bear" "+")
int3
The dog needs the lion.
("dog" "needs" "lion" "+")
int4
The bear does not need the lion.
False
5
inv-proof
[(((((((((triple3) -> rule2)) -> rule6)) -> rule5)) -> rule2))]
("bear" "needs" "lion" "-")
((((((((triple3) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The dog needs the bear.
("dog" "needs" "bear" "+")
int3
The dog needs the lion.
("dog" "needs" "lion" "+")
int4
The bear needs the bear.
True
6
proof
[(((((((((((triple3) -> rule2)) -> rule6)) -> rule5)) -> rule2)) -> rule6))]
("bear" "needs" "bear" "+")
((((((((((triple3) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The dog needs the bear.
("dog" "needs" "bear" "+")
int4
The dog needs the lion.
("dog" "needs" "lion" "+")
int5
The bear does not need the bear.
False
6
inv-proof
[(((((((((((triple3) -> rule2)) -> rule6)) -> rule5)) -> rule2)) -> rule6))]
("bear" "needs" "bear" "-")
((((((((((triple3) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The dog needs the bear.
("dog" "needs" "bear" "+")
int4
The dog needs the lion.
("dog" "needs" "lion" "+")
int5
The lion does not need the dog.
Unknown
inv-rconc
[@1: The lion needs the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "needs" "dog" "-")
The bald eagle needs the bear.
Unknown
rconc
[@3: The bald eagle needs the bear.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule1 <- FAIL)]]
("bald eagle" "needs" "bear" "+")
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "needs" "dog" "-")
The lion is round.
Unknown
rconc
[@3: The lion is round.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule2 <- FAIL)]]
("lion" "is" "round" "+")
The bald eagle is not round.
Unknown
inv-rconc
[@3: The bald eagle is round.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule2 <- FAIL)]]
("bald eagle" "is" "round" "-")
The bald eagle needs the lion.
Unknown
rconc
[@3: The bald eagle needs the lion.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule6 <- FAIL)]]
("bald eagle" "needs" "lion" "+")
The dog is not young.
Unknown
inv-random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "-")
The bald eagle sees the dog.
Unknown
random
[@0: The bald eagle sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "dog" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion needs the bald eagle.
Unknown
random
[@0: The lion needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "bald eagle" "+")
The dog is not red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The dog sees the bear.
Unknown
random
[@0: The dog sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "bear" "+")
@0: The bald eagle needs the dog.[(triple1)] The bear sees the dog.[(triple2)] The dog is round.[(triple3)] The dog sees the bald eagle.[(triple4)] The lion is blue.[(triple5)] The lion sees the bear.[(triple6)] The lion visits the bear.[(triple7)] @1: The dog needs the lion.[(((triple3) -> rule2))] @2: The dog needs the bear.[(((((triple3) -> rule2)) -> rule6))] @3: The bear is round.[(((((((triple3) -> rule2)) -> rule6)) -> rule5))] @4: The bear needs the lion.[(((((((((triple3) -> rule2)) -> rule6)) -> rule5)) -> rule2))] @5: The bear needs the bear.[(((((((((((triple3) -> rule2)) -> rule6)) -> rule5)) -> rule2)) -> rule6))]
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
triple1
The bear sees the dog.
("bear" "sees" "dog" "+")
triple2
The dog is round.
("dog" "is" "round" "+")
triple3
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
triple4
The lion is blue.
("lion" "is" "blue" "+")
triple5
The lion sees the bear.
("lion" "sees" "bear" "+")
triple6
The lion visits the bear.
("lion" "visits" "bear" "+")
triple7
The dog needs the lion.
("dog" "needs" "lion" "+")
((triple3) -> (rule2 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The bear is round.
("bear" "is" "round" "+")
((((((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
int2
The dog needs the lion.
("dog" "needs" "lion" "+")
int3
The bear needs the lion.
("bear" "needs" "lion" "+")
((((((((triple3) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The dog needs the bear.
("dog" "needs" "bear" "+")
int3
The dog needs the lion.
("dog" "needs" "lion" "+")
int4
The bear needs the bear.
("bear" "needs" "bear" "+")
((((((((((triple3) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The dog needs the bear.
("dog" "needs" "bear" "+")
int4
The dog needs the lion.
("dog" "needs" "lion" "+")
int5