The bald eagle is round. The bald eagle needs the dog. The dog needs the bald eagle. Red people are young. If someone is young and red then they visit the dog. If someone needs the bald eagle and the bald eagle needs the dog then the dog is red. If someone needs the bald eagle then they need the dog. If the bald eagle is young then the bald eagle is rough. If someone sees the dog then the dog sees the bald eagle.
The bald eagle is round.
("bald eagle" "is" "round" "+")
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
Red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is young and red then they visit the dog.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "visits" "dog" "+"))
If someone needs the bald eagle and the bald eagle needs the dog then the dog is red.
((("someone" "needs" "bald eagle" "+") ("bald eagle" "needs" "dog" "+")) -> ("dog" "is" "red" "+"))
If someone needs the bald eagle then they need the dog.
((("someone" "needs" "bald eagle" "+")) -> ("someone" "needs" "dog" "+"))
If the bald eagle is young then the bald eagle is rough.
((("bald eagle" "is" "young" "+")) -> ("bald eagle" "is" "rough" "+"))
If someone sees the dog then the dog sees the bald eagle.
((("someone" "sees" "dog" "+")) -> ("dog" "sees" "bald eagle" "+"))
The bald eagle needs the dog.
True
1
proof
[(triple2)]
("bald eagle" "needs" "dog" "+")
triple2
The bald eagle does not need the dog.
False
1
inv-proof
[(triple2)]
("bald eagle" "needs" "dog" "-")
triple2
The dog needs the dog.
True
2
proof
[(((triple3) -> rule4))]
("dog" "needs" "dog" "+")
((triple3) -> (rule4 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog does not need the dog.
False
2
inv-proof
[(((triple3) -> rule4))]
("dog" "needs" "dog" "-")
((triple3) -> (rule4 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is young.
True
4
proof
[(((((triple3 triple2) -> rule3)) -> rule1))]
("dog" "is" "young" "+")
((((triple3 triple2) -> (rule3 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is not young.
False
4
inv-proof
[(((((triple3 triple2) -> rule3)) -> rule1))]
("dog" "is" "young" "-")
((((triple3 triple2) -> (rule3 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog visits the dog.
True
8
proof
[(((((((triple3 triple2) -> rule3)) -> rule1) ((triple3 triple2) -> rule3)) -> rule2))]
("dog" "visits" "dog" "+")
((((((triple3 triple2) -> (rule3 % int3))) -> (rule1 % int2)) ((triple3 triple2) -> (rule3 % int3))) -> (rule2 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The dog does not visit the dog.
False
8
inv-proof
[(((((((triple3 triple2) -> rule3)) -> rule1) ((triple3 triple2) -> rule3)) -> rule2))]
("dog" "visits" "dog" "-")
((((((triple3 triple2) -> (rule3 % int3))) -> (rule1 % int2)) ((triple3 triple2) -> (rule3 % int3))) -> (rule2 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The dog does not see the bald eagle.
Unknown
inv-rconc
[@1: The dog sees the bald eagle.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "sees" "bald eagle" "-")
The bald eagle is rough.
Unknown
rconc
[@2: The bald eagle is rough.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("bald eagle" "is" "rough" "+")
The bald eagle does not visit the dog.
Unknown
inv-rconc
[@1: The bald eagle visits the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "visits" "dog" "-")
The bald eagle is young.
Unknown
rconc
[@1: The bald eagle is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "is" "young" "+")
The dog does not visit the bald eagle.
Unknown
inv-random
[@0: The dog visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "bald eagle" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The bald eagle is not red.
Unknown
inv-random
[@0: The bald eagle is red.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "red" "-")
The bald eagle sees the bald eagle.
Unknown
random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "+")
@0: The bald eagle is round.[(triple1)] The bald eagle needs the dog.[(triple2)] The dog needs the bald eagle.[(triple3)] @1: The dog is red.[(((triple3 triple2) -> rule3))] The dog needs the dog.[(((triple3) -> rule4))] @2: The dog is young.[(((((triple3 triple2) -> rule3)) -> rule1))] @3: The dog visits the dog.[(((((((triple3 triple2) -> rule3)) -> rule1) ((triple3 triple2) -> rule3)) -> rule2))]
The bald eagle is round.
("bald eagle" "is" "round" "+")
triple1
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
triple2
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
((triple3 triple2) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple3) -> (rule4 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((((triple3 triple2) -> (rule3 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
((((((triple3 triple2) -> (rule3 % int3))) -> (rule1 % int2)) ((triple3 triple2) -> (rule3 % int3))) -> (rule2 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3