The bald eagle likes the rabbit. The bald eagle needs the dog. The cow is blue. The cow likes the bald eagle. The dog likes the bald eagle. The dog likes the rabbit. The dog sees the bald eagle. The dog sees the rabbit. The rabbit likes the bald eagle. The rabbit likes the cow. If the bald eagle likes the rabbit then the bald eagle sees the cow. If something needs the cow then it sees the rabbit. If something sees the cow then the cow needs the bald eagle. If something is cold then it likes the dog. If something sees the cow and the cow likes the rabbit then it is cold. If something needs the bald eagle and it likes the bald eagle then the bald eagle does not need the rabbit. If something is red and it does not need the dog then the dog sees the bald eagle. If something needs the cow and it does not need the dog then the cow likes the dog.
The bald eagle likes the rabbit.
("bald eagle" "likes" "rabbit" "+")
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
The dog likes the bald eagle.
("dog" "likes" "bald eagle" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
If the bald eagle likes the rabbit then the bald eagle sees the cow.
((("bald eagle" "likes" "rabbit" "+")) -> ("bald eagle" "sees" "cow" "+"))
If something needs the cow then it sees the rabbit.
((("something" "needs" "cow" "+")) -> ("something" "sees" "rabbit" "+"))
If something sees the cow then the cow needs the bald eagle.
((("something" "sees" "cow" "+")) -> ("cow" "needs" "bald eagle" "+"))
If something is cold then it likes the dog.
((("something" "is" "cold" "+")) -> ("something" "likes" "dog" "+"))
If something sees the cow and the cow likes the rabbit then it is cold.
((("something" "sees" "cow" "+") ("cow" "likes" "rabbit" "+")) -> ("something" "is" "cold" "+"))
If something needs the bald eagle and it likes the bald eagle then the bald eagle does not need the rabbit.
((("something" "needs" "bald eagle" "+") ("something" "likes" "bald eagle" "+")) -> ("bald eagle" "needs" "rabbit" "-"))
If something is red and it does not need the dog then the dog sees the bald eagle.
((("something" "is" "red" "+") ("something" "needs" "dog" "~")) -> ("dog" "sees" "bald eagle" "+"))
If something needs the cow and it does not need the dog then the cow likes the dog.
((("something" "needs" "cow" "+") ("something" "needs" "dog" "~")) -> ("cow" "likes" "dog" "+"))
The dog likes the rabbit.
True
1
proof
[(triple6)]
("dog" "likes" "rabbit" "+")
triple6
The dog does not see the bald eagle.
False
1
inv-proof
[(triple7)]
("dog" "sees" "bald eagle" "-")
triple7
The bald eagle sees the cow.
True
2
proof
[(((triple1) -> rule1))]
("bald eagle" "sees" "cow" "+")
((triple1) -> (rule1 % int1))
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int1
The bald eagle does not see the cow.
False
2
inv-proof
[(((triple1) -> rule1))]
("bald eagle" "sees" "cow" "-")
((triple1) -> (rule1 % int1))
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int1
The cow needs the bald eagle.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("cow" "needs" "bald eagle" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
int1
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int2
The cow does not need the bald eagle.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("cow" "needs" "bald eagle" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
int1
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int2
The bald eagle does not need the rabbit.
True
5
proof
[(((((((triple1) -> rule1)) -> rule3) triple4) -> rule6))]
("bald eagle" "needs" "rabbit" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2)) triple4) -> (rule6 % int1))
The bald eagle does not need the rabbit.
("bald eagle" "needs" "rabbit" "-")
int1
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
int2
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int3
The bald eagle needs the rabbit.
False
5
inv-proof
[(((((((triple1) -> rule1)) -> rule3) triple4) -> rule6))]
("bald eagle" "needs" "rabbit" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2)) triple4) -> (rule6 % int1))
The bald eagle does not need the rabbit.
("bald eagle" "needs" "rabbit" "-")
int1
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
int2
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int3
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The cow is cold.
Unknown
rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "cold" "+")
The dog is not cold.
Unknown
inv-rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "cold" "-")
The cow likes the dog.
Unknown
rconc
[@2: The cow likes the dog.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("cow" "likes" "dog" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
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" "+")
The bald eagle is not nice.
Unknown
inv-random
[@0: The bald eagle is nice.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "nice" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The bald eagle likes the rabbit.[(triple1)] The bald eagle needs the dog.[(triple2)] The cow is blue.[(triple3)] The cow likes the bald eagle.[(triple4)] The dog likes the bald eagle.[(triple5)] The dog likes the rabbit.[(triple6)] The dog sees the bald eagle.[(triple7)] The dog sees the rabbit.[(triple8)] The rabbit likes the bald eagle.[(triple9)] The rabbit likes the cow.[(triple10)] @1: The bald eagle sees the cow.[(((triple1) -> rule1))] @2: The cow needs the bald eagle.[(((((triple1) -> rule1)) -> rule3))] @3: The bald eagle does not need the rabbit.[(((((((triple1) -> rule1)) -> rule3) triple4) -> rule6))]
The bald eagle likes the rabbit.
("bald eagle" "likes" "rabbit" "+")
triple1
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
triple2
The cow is blue.
("cow" "is" "blue" "+")
triple3
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
triple4
The dog likes the bald eagle.
("dog" "likes" "bald eagle" "+")
triple5
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple6
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
triple7
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple8
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
triple9
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple10
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
((triple1) -> (rule1 % int1))
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int1
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
int1
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int2
The bald eagle does not need the rabbit.
("bald eagle" "needs" "rabbit" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2)) triple4) -> (rule6 % int1))
The bald eagle does not need the rabbit.
("bald eagle" "needs" "rabbit" "-")
int1
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
int2
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int3