The bald eagle is cold. The bald eagle likes the bear. The bald eagle needs the dog. The bear is big. The bear is nice. The bear likes the cat. The bear sees the bald eagle. The cat sees the bald eagle. The dog is big. The dog is kind. The dog needs the cat. The dog sees the bear. If something is cold and kind then it needs the bald eagle. If something sees the dog and it needs the bald eagle then the bald eagle likes the cat. If something likes the bald eagle and the bald eagle sees the cat then the cat is cold. If something sees the bald eagle then it is kind. If something is cold and it likes the dog then it needs the cat. If something needs the dog then the dog needs the bear. If something needs the bald eagle then it is nice. If something sees the bear then it is cold.
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
The bald eagle likes the bear.
("bald eagle" "likes" "bear" "+")
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
If something is cold and kind then it needs the bald eagle.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "needs" "bald eagle" "+"))
If something sees the dog and it needs the bald eagle then the bald eagle likes the cat.
((("something" "sees" "dog" "+") ("something" "needs" "bald eagle" "+")) -> ("bald eagle" "likes" "cat" "+"))
If something likes the bald eagle and the bald eagle sees the cat then the cat is cold.
((("something" "likes" "bald eagle" "+") ("bald eagle" "sees" "cat" "+")) -> ("cat" "is" "cold" "+"))
If something sees the bald eagle then it is kind.
((("something" "sees" "bald eagle" "+")) -> ("something" "is" "kind" "+"))
If something is cold and it likes the dog then it needs the cat.
((("something" "is" "cold" "+") ("something" "likes" "dog" "+")) -> ("something" "needs" "cat" "+"))
If something needs the dog then the dog needs the bear.
((("something" "needs" "dog" "+")) -> ("dog" "needs" "bear" "+"))
If something needs the bald eagle then it is nice.
((("something" "needs" "bald eagle" "+")) -> ("something" "is" "nice" "+"))
If something sees the bear then it is cold.
((("something" "sees" "bear" "+")) -> ("something" "is" "cold" "+"))
The bear is big.
True
1
proof
[(triple4)]
("bear" "is" "big" "+")
triple4
The bald eagle is not cold.
False
1
inv-proof
[(triple1)]
("bald eagle" "is" "cold" "-")
triple1
The dog needs the bear.
True
2
proof
[(((triple3) -> rule6))]
("dog" "needs" "bear" "+")
((triple3) -> (rule6 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The bear is not kind.
False
2
inv-proof
[(((triple7) -> rule4))]
("bear" "is" "kind" "-")
((triple7) -> (rule4 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The dog needs the bald eagle.
True
4
proof
[(((((triple12) -> rule8) triple10) -> rule1))]
("dog" "needs" "bald eagle" "+")
((((triple12) -> (rule8 % int2)) triple10) -> (rule1 % int1))
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog does not need the bald eagle.
False
4
inv-proof
[(((((triple12) -> rule8) triple10) -> rule1))]
("dog" "needs" "bald eagle" "-")
((((triple12) -> (rule8 % int2)) triple10) -> (rule1 % int1))
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog is nice.
True
5
proof
[(((((((triple12) -> rule8) triple10) -> rule1)) -> rule7))]
("dog" "is" "nice" "+")
((((((triple12) -> (rule8 % int3)) triple10) -> (rule1 % int2))) -> (rule7 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The dog is not nice.
False
5
inv-proof
[(((((((triple12) -> rule8) triple10) -> rule1)) -> rule7))]
("dog" "is" "nice" "-")
((((((triple12) -> (rule8 % int3)) triple10) -> (rule1 % int2))) -> (rule7 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The bald eagle is not nice.
Unknown
inv-rconc
[@3: The bald eagle is nice.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule4 <- FAIL)]]
("bald eagle" "is" "nice" "-")
The cat is nice.
Unknown
rconc
[@3: The cat is nice.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule3 <- FAIL)]]
("cat" "is" "nice" "+")
The cat is not cold.
Unknown
inv-rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "cold" "-")
The cat needs the bald eagle.
Unknown
rconc
[@2: The cat needs the bald eagle.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("cat" "needs" "bald eagle" "+")
The cat does not need the dog.
Unknown
inv-random
[@0: The cat needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "dog" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The bald eagle needs the bear.
Unknown
random
[@0: The bald eagle needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "bear" "+")
@0: The bald eagle is cold.[(triple1)] The bald eagle likes the bear.[(triple2)] The bald eagle needs the dog.[(triple3)] The bear is big.[(triple4)] The bear is nice.[(triple5)] The bear likes the cat.[(triple6)] The bear sees the bald eagle.[(triple7)] The cat sees the bald eagle.[(triple8)] The dog is big.[(triple9)] The dog is kind.[(triple10)] The dog needs the cat.[(triple11)] The dog sees the bear.[(triple12)] @1: The bear is kind.[(((triple7) -> rule4))] The cat is kind.[(((triple8) -> rule4))] The dog is cold.[(((triple12) -> rule8))] The dog needs the bear.[(((triple3) -> rule6))] @2: The dog needs the bald eagle.[(((((triple12) -> rule8) triple10) -> rule1))] @3: The dog is nice.[(((((((triple12) -> rule8) triple10) -> rule1)) -> rule7))]
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
triple1
The bald eagle likes the bear.
("bald eagle" "likes" "bear" "+")
triple2
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
triple3
The bear is big.
("bear" "is" "big" "+")
triple4
The bear is nice.
("bear" "is" "nice" "+")
triple5
The bear likes the cat.
("bear" "likes" "cat" "+")
triple6
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
triple7
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
triple8
The dog is big.
("dog" "is" "big" "+")
triple9
The dog is kind.
("dog" "is" "kind" "+")
triple10
The dog needs the cat.
("dog" "needs" "cat" "+")
triple11
The dog sees the bear.
("dog" "sees" "bear" "+")
triple12
The bear is kind.
("bear" "is" "kind" "+")
((triple7) -> (rule4 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
((triple8) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
((triple12) -> (rule8 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
((triple3) -> (rule6 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
((((triple12) -> (rule8 % int2)) triple10) -> (rule1 % int1))
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
((((((triple12) -> (rule8 % int3)) triple10) -> (rule1 % int2))) -> (rule7 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3