The bald eagle is big. The cat is big. The cat sees the bald eagle. The cow eats the cat. The cow is blue. The cow sees the bald eagle. The cow sees the cat. If something is big then it is not nice. If the cat sees the cow then the cow needs the bald eagle. If the cat is big and the cat does not need the bald eagle then the cat does not see the cow.
The bald eagle is big.
("bald eagle" "is" "big" "+")
The cat is big.
("cat" "is" "big" "+")
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
If something is big then it is not nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "-"))
If the cat sees the cow then the cow needs the bald eagle.
((("cat" "sees" "cow" "+")) -> ("cow" "needs" "bald eagle" "+"))
If the cat is big and the cat does not need the bald eagle then the cat does not see the cow.
((("cat" "is" "big" "+") ("cat" "needs" "bald eagle" "~")) -> ("cat" "sees" "cow" "-"))
The cow is blue.
True
1
proof
[(triple5)]
("cow" "is" "blue" "+")
triple5
The cow does not see the bald eagle.
False
1
inv-proof
[(triple6)]
("cow" "sees" "bald eagle" "-")
triple6
The bald eagle is not nice.
True
2
proof
[(((triple1) -> rule1))]
("bald eagle" "is" "nice" "-")
((triple1) -> (rule1 % int1))
The bald eagle is not nice.
("bald eagle" "is" "nice" "-")
int1
The bald eagle is nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("bald eagle" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The bald eagle is not nice.
("bald eagle" "is" "nice" "-")
int1
The cow does not need the bald eagle.
Unknown
inv-rconc
[@1: The cow needs the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "needs" "bald eagle" "-")
The cat needs the bald eagle.
Unknown
random
[@0: The cat needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "bald eagle" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The bald eagle needs the cat.
Unknown
random
[@0: The bald eagle needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "cat" "+")
@0: The bald eagle is big.[(triple1)] The cat is big.[(triple2)] The cat sees the bald eagle.[(triple3)] The cow eats the cat.[(triple4)] The cow is blue.[(triple5)] The cow sees the bald eagle.[(triple6)] The cow sees the cat.[(triple7)] @1: The bald eagle is not nice.[(((triple1) -> rule1))] The cat is not nice.[(((triple2) -> rule1))]
The bald eagle is big.
("bald eagle" "is" "big" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
triple3
The cow eats the cat.
("cow" "eats" "cat" "+")
triple4
The cow is blue.
("cow" "is" "blue" "+")
triple5
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
triple6
The cow sees the cat.
("cow" "sees" "cat" "+")
triple7
The bald eagle is not nice.
("bald eagle" "is" "nice" "-")
((triple1) -> (rule1 % int1))
The bald eagle is not nice.
("bald eagle" "is" "nice" "-")
int1
The cat is not nice.
("cat" "is" "nice" "-")
((triple2) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1