The bald eagle is cold. The cow likes the bald eagle. The dog likes the bald eagle. If something likes the bald eagle then it chases the cow. If something likes the dog then the dog is not rough. All young things are cold. If the dog is not red then the dog does not like the bald eagle. If the dog is not rough and the dog does not eat the cow then the dog does not chase the cow. If something chases the cow then the cow is round. If something is round then it eats the dog. If something likes the cow then it eats the dog.
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
The dog likes the bald eagle.
("dog" "likes" "bald eagle" "+")
If something likes the bald eagle then it chases the cow.
((("something" "likes" "bald eagle" "+")) -> ("something" "chases" "cow" "+"))
If something likes the dog then the dog is not rough.
((("something" "likes" "dog" "+")) -> ("dog" "is" "rough" "-"))
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If the dog is not red then the dog does not like the bald eagle.
((("dog" "is" "red" "~")) -> ("dog" "likes" "bald eagle" "-"))
If the dog is not rough and the dog does not eat the cow then the dog does not chase the cow.
((("dog" "is" "rough" "~") ("dog" "eats" "cow" "~")) -> ("dog" "chases" "cow" "-"))
If something chases the cow then the cow is round.
((("something" "chases" "cow" "+")) -> ("cow" "is" "round" "+"))
If something is round then it eats the dog.
((("something" "is" "round" "+")) -> ("something" "eats" "dog" "+"))
If something likes the cow then it eats the dog.
((("something" "likes" "cow" "+")) -> ("something" "eats" "dog" "+"))
The bald eagle is cold.
True
1
proof
[(triple1)]
("bald eagle" "is" "cold" "+")
triple1
The cow does not like the bald eagle.
False
1
inv-proof
[(triple2)]
("cow" "likes" "bald eagle" "-")
triple2
The cow chases the cow.
True
2
proof
[(((triple2) -> rule1))]
("cow" "chases" "cow" "+")
((triple2) -> (rule1 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The dog does not chase the cow.
False
2
inv-proof
[(((triple3) -> rule1))]
("dog" "chases" "cow" "-")
((triple3) -> (rule1 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The cow is round.
True
3
proof
[(((((triple2) -> rule1)) -> rule6) OR ((((triple3) -> rule1)) -> rule6))]
("cow" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The cow is not round.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6) OR ((((triple3) -> rule1)) -> rule6))]
("cow" "is" "round" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The cow eats the dog.
True
4
proof
[(((((((triple2) -> rule1)) -> rule6)) -> rule7) OR ((((((triple3) -> rule1)) -> rule6)) -> rule7))]
("cow" "eats" "dog" "+")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
int3
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The dog chases the cow.
("dog" "chases" "cow" "+")
int3
The cow does not eat the dog.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule6)) -> rule7) OR ((((((triple3) -> rule1)) -> rule6)) -> rule7))]
("cow" "eats" "dog" "-")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
int3
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The dog chases the cow.
("dog" "chases" "cow" "+")
int3
The bald eagle does not eat the dog.
Unknown
inv-rconc
[@1: The bald eagle eats the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bald eagle" "eats" "dog" "-")
The dog is cold.
Unknown
rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "cold" "+")
The dog does not eat the dog.
Unknown
inv-rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "eats" "dog" "-")
The bald eagle chases the cow.
Unknown
rconc
[@1: The bald eagle chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "chases" "cow" "+")
The dog does not eat the cow.
Unknown
inv-random
[@0: The dog eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cow" "-")
The bald eagle eats the bald eagle.
Unknown
random
[@0: The bald eagle eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "bald eagle" "+")
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The bald eagle is cold.[(triple1)] The cow likes the bald eagle.[(triple2)] The dog likes the bald eagle.[(triple3)] @1: The cow chases the cow.[(((triple2) -> rule1))] The dog chases the cow.[(((triple3) -> rule1))] @2: The cow is round.[(((((triple2) -> rule1)) -> rule6) OR ((((triple3) -> rule1)) -> rule6))] @3: The cow eats the dog.[(((((((triple2) -> rule1)) -> rule6)) -> rule7) OR ((((((triple3) -> rule1)) -> rule6)) -> rule7))]
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
triple1
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
triple2
The dog likes the bald eagle.
("dog" "likes" "bald eagle" "+")
triple3
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple2) -> (rule1 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
((triple3) -> (rule1 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The cow is round.
("cow" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The cow eats the dog.
("cow" "eats" "dog" "+")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
int3
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The dog chases the cow.
("dog" "chases" "cow" "+")
int3