The bald eagle is big. The cow needs the tiger. The dog needs the cow. The tiger needs the bald eagle. If someone is cold then they need the bald eagle. If someone is round and they visit the cow then the cow is red. If the dog needs the cow then the dog chases the bald eagle.
The bald eagle is big.
("bald eagle" "is" "big" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
If someone is cold then they need the bald eagle.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "bald eagle" "+"))
If someone is round and they visit the cow then the cow is red.
((("someone" "is" "round" "+") ("someone" "visits" "cow" "+")) -> ("cow" "is" "red" "+"))
If the dog needs the cow then the dog chases the bald eagle.
((("dog" "needs" "cow" "+")) -> ("dog" "chases" "bald eagle" "+"))
The dog needs the cow.
True
1
proof
[(triple3)]
("dog" "needs" "cow" "+")
triple3
The bald eagle is not big.
False
1
inv-proof
[(triple1)]
("bald eagle" "is" "big" "-")
triple1
The dog chases the bald eagle.
True
2
proof
[(((triple3) -> rule3))]
("dog" "chases" "bald eagle" "+")
((triple3) -> (rule3 % int1))
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int1
The dog does not chase the bald eagle.
False
2
inv-proof
[(((triple3) -> rule3))]
("dog" "chases" "bald eagle" "-")
((triple3) -> (rule3 % int1))
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int1
The bald eagle does not need the bald eagle.
Unknown
inv-rconc
[@1: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "needs" "bald eagle" "-")
The cow is red.
Unknown
rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "red" "+")
The cow does not chase the dog.
Unknown
inv-random
[@0: The cow chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "dog" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The bald eagle is big.[(triple1)] The cow needs the tiger.[(triple2)] The dog needs the cow.[(triple3)] The tiger needs the bald eagle.[(triple4)] @1: The dog chases the bald eagle.[(((triple3) -> rule3))]
The bald eagle is big.
("bald eagle" "is" "big" "+")
triple1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple2
The dog needs the cow.
("dog" "needs" "cow" "+")
triple3
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
triple4
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
((triple3) -> (rule3 % int1))
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int1