The bald eagle likes the dog. The dog is big. If something likes the dog then it is cold. If something likes the dog then the dog sees the bald eagle. If the dog is cold then the dog does not see the bald eagle. If something sees the bald eagle then the bald eagle visits the dog. If something visits the dog then it does not visit the bald eagle. If the dog likes the bald eagle then the bald eagle is not red.
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
The dog is big.
("dog" "is" "big" "+")
If something likes the dog then it is cold.
((("something" "likes" "dog" "+")) -> ("something" "is" "cold" "+"))
If something likes the dog then the dog sees the bald eagle.
((("something" "likes" "dog" "+")) -> ("dog" "sees" "bald eagle" "+"))
If the dog is cold then the dog does not see the bald eagle.
((("dog" "is" "cold" "+")) -> ("dog" "sees" "bald eagle" "-"))
If something sees the bald eagle then the bald eagle visits the dog.
((("something" "sees" "bald eagle" "+")) -> ("bald eagle" "visits" "dog" "+"))
If something visits the dog then it does not visit the bald eagle.
((("something" "visits" "dog" "+")) -> ("something" "visits" "bald eagle" "-"))
If the dog likes the bald eagle then the bald eagle is not red.
((("dog" "likes" "bald eagle" "+")) -> ("bald eagle" "is" "red" "-"))
The dog is big.
True
1
proof
[(triple2)]
("dog" "is" "big" "+")
triple2
The dog is not big.
False
1
inv-proof
[(triple2)]
("dog" "is" "big" "-")
triple2
The bald eagle is cold.
True
2
proof
[(((triple1) -> rule1))]
("bald eagle" "is" "cold" "+")
((triple1) -> (rule1 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The dog does not see the bald eagle.
False
2
inv-proof
[(((triple1) -> rule2))]
("dog" "sees" "bald eagle" "-")
((triple1) -> (rule2 % int1))
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int1
The bald eagle visits the dog.
True
3
proof
[(((((triple1) -> rule2)) -> rule4))]
("bald eagle" "visits" "dog" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int1
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int2
The bald eagle does not visit the dog.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("bald eagle" "visits" "dog" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int1
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int2
The bald eagle does not visit the bald eagle.
True
4
proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule5))]
("bald eagle" "visits" "bald eagle" "-")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The bald eagle does not visit the bald eagle.
("bald eagle" "visits" "bald eagle" "-")
int1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int2
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int3
The bald eagle visits the bald eagle.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule5))]
("bald eagle" "visits" "bald eagle" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The bald eagle does not visit the bald eagle.
("bald eagle" "visits" "bald eagle" "-")
int1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int2
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int3
The dog is not cold.
Unknown
inv-rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "cold" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
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 dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
The bald eagle does not see the bald eagle.
Unknown
inv-random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "-")
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 bald eagle is not big.
Unknown
inv-random
[@0: The bald eagle is big.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "big" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The bald eagle likes the dog.[(triple1)] The dog is big.[(triple2)] @1: The bald eagle is cold.[(((triple1) -> rule1))] The dog sees the bald eagle.[(((triple1) -> rule2))] @2: The bald eagle visits the dog.[(((((triple1) -> rule2)) -> rule4))] @3: The bald eagle does not visit the bald eagle.[(((((((triple1) -> rule2)) -> rule4)) -> rule5))]
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
((triple1) -> (rule1 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
((triple1) -> (rule2 % int1))
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int1
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int2
The bald eagle does not visit the bald eagle.
("bald eagle" "visits" "bald eagle" "-")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The bald eagle does not visit the bald eagle.
("bald eagle" "visits" "bald eagle" "-")
int1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int2
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int3