The bald eagle needs the dog. The bear chases the squirrel. The dog chases the bald eagle. The squirrel needs the bear. If something sees the bald eagle and the bald eagle sees the bear then the bear is red. If the dog chases the bear then the dog chases the squirrel. If something chases the dog then it is kind. If something chases the bald eagle then the bald eagle is young. If something needs the bear and the bear chases the dog then the dog is young. If something is young then it chases the dog.
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
If something sees the bald eagle and the bald eagle sees the bear then the bear is red.
((("something" "sees" "bald eagle" "+") ("bald eagle" "sees" "bear" "+")) -> ("bear" "is" "red" "+"))
If the dog chases the bear then the dog chases the squirrel.
((("dog" "chases" "bear" "+")) -> ("dog" "chases" "squirrel" "+"))
If something chases the dog then it is kind.
((("something" "chases" "dog" "+")) -> ("something" "is" "kind" "+"))
If something chases the bald eagle then the bald eagle is young.
((("something" "chases" "bald eagle" "+")) -> ("bald eagle" "is" "young" "+"))
If something needs the bear and the bear chases the dog then the dog is young.
((("something" "needs" "bear" "+") ("bear" "chases" "dog" "+")) -> ("dog" "is" "young" "+"))
If something is young then it chases the dog.
((("something" "is" "young" "+")) -> ("something" "chases" "dog" "+"))
The dog chases the bald eagle.
True
1
proof
[(triple3)]
("dog" "chases" "bald eagle" "+")
triple3
The squirrel does not need the bear.
False
1
inv-proof
[(triple4)]
("squirrel" "needs" "bear" "-")
triple4
The bald eagle is young.
True
2
proof
[(((triple3) -> rule4))]
("bald eagle" "is" "young" "+")
((triple3) -> (rule4 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle is not young.
False
2
inv-proof
[(((triple3) -> rule4))]
("bald eagle" "is" "young" "-")
((triple3) -> (rule4 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle chases the dog.
True
3
proof
[(((((triple3) -> rule4)) -> rule6))]
("bald eagle" "chases" "dog" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The bald eagle chases the dog.
("bald eagle" "chases" "dog" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle does not chase the dog.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule6))]
("bald eagle" "chases" "dog" "-")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The bald eagle chases the dog.
("bald eagle" "chases" "dog" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle is kind.
True
4
proof
[(((((((triple3) -> rule4)) -> rule6)) -> rule3))]
("bald eagle" "is" "kind" "+")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bald eagle chases the dog.
("bald eagle" "chases" "dog" "+")
int2
The bald eagle is young.
("bald eagle" "is" "young" "+")
int3
The bald eagle is not kind.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule6)) -> rule3))]
("bald eagle" "is" "kind" "-")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bald eagle chases the dog.
("bald eagle" "chases" "dog" "+")
int2
The bald eagle is young.
("bald eagle" "is" "young" "+")
int3
The dog is not kind.
Unknown
inv-rconc
[@3: The dog is kind.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule5 <- FAIL)]]
("dog" "is" "kind" "-")
The dog chases the dog.
Unknown
rconc
[@2: The dog chases the dog.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("dog" "chases" "dog" "+")
The squirrel does not chase the dog.
Unknown
inv-rconc
[@1: The squirrel chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "chases" "dog" "-")
The bear is kind.
Unknown
rconc
[@2: The bear is kind.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("bear" "is" "kind" "+")
The bald eagle does not need the squirrel.
Unknown
inv-random
[@0: The bald eagle needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "squirrel" "-")
The squirrel sees the bald eagle.
Unknown
random
[@0: The squirrel sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "bald eagle" "+")
The bear is not young.
Unknown
inv-random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "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" "+")
@0: The bald eagle needs the dog.[(triple1)] The bear chases the squirrel.[(triple2)] The dog chases the bald eagle.[(triple3)] The squirrel needs the bear.[(triple4)] @1: The bald eagle is young.[(((triple3) -> rule4))] @2: The bald eagle chases the dog.[(((((triple3) -> rule4)) -> rule6))] @3: The bald eagle is kind.[(((((((triple3) -> rule4)) -> rule6)) -> rule3))]
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
triple1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple2
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
triple3
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple4
The bald eagle is young.
("bald eagle" "is" "young" "+")
((triple3) -> (rule4 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle chases the dog.
("bald eagle" "chases" "dog" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The bald eagle chases the dog.
("bald eagle" "chases" "dog" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bald eagle chases the dog.
("bald eagle" "chases" "dog" "+")
int2
The bald eagle is young.
("bald eagle" "is" "young" "+")
int3