The bear chases the dog. The dog needs the bear. If the dog needs the bear then the dog is big. If something is cold and it sees the dog then it is big. If something needs the bear then the bear sees the dog. If the bear chases the dog then the bear is cold. If the dog is cold then the dog needs the bear. If something is blue then it needs the dog. If something sees the dog and it needs the bear then it chases the dog. If the bear chases the dog then the bear sees the dog.
The bear chases the dog.
("bear" "chases" "dog" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
If the dog needs the bear then the dog is big.
((("dog" "needs" "bear" "+")) -> ("dog" "is" "big" "+"))
If something is cold and it sees the dog then it is big.
((("something" "is" "cold" "+") ("something" "sees" "dog" "+")) -> ("something" "is" "big" "+"))
If something needs the bear then the bear sees the dog.
((("something" "needs" "bear" "+")) -> ("bear" "sees" "dog" "+"))
If the bear chases the dog then the bear is cold.
((("bear" "chases" "dog" "+")) -> ("bear" "is" "cold" "+"))
If the dog is cold then the dog needs the bear.
((("dog" "is" "cold" "+")) -> ("dog" "needs" "bear" "+"))
If something is blue then it needs the dog.
((("something" "is" "blue" "+")) -> ("something" "needs" "dog" "+"))
If something sees the dog and it needs the bear then it chases the dog.
((("something" "sees" "dog" "+") ("something" "needs" "bear" "+")) -> ("something" "chases" "dog" "+"))
If the bear chases the dog then the bear sees the dog.
((("bear" "chases" "dog" "+")) -> ("bear" "sees" "dog" "+"))
The bear chases the dog.
True
1
proof
[(triple1)]
("bear" "chases" "dog" "+")
triple1
The dog does not need the bear.
False
1
inv-proof
[(triple2)]
("dog" "needs" "bear" "-")
triple2
The bear is cold.
True
2
proof
[(((triple1) -> rule4))]
("bear" "is" "cold" "+")
((triple1) -> (rule4 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The dog is not big.
False
2
inv-proof
[(((triple2) -> rule1))]
("dog" "is" "big" "-")
((triple2) -> (rule1 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The bear does not need the dog.
Unknown
inv-rconc
[@1: The bear needs the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "needs" "dog" "-")
The dog needs the dog.
Unknown
rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "needs" "dog" "+")
The dog does not see the bear.
Unknown
inv-random
[@0: The dog sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "bear" "-")
The bear is blue.
Unknown
random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "+")
@0: The bear chases the dog.[(triple1)] The dog needs the bear.[(triple2)] @1: The bear is cold.[(((triple1) -> rule4))] The bear sees the dog.[(((triple1) -> rule8) OR ((triple2) -> rule3))] The dog is big.[(((triple2) -> rule1))] @2: The bear is big.[(((((triple1) -> rule4) ((triple1) -> rule8)) -> rule2) OR ((((triple1) -> rule4) ((triple2) -> rule3)) -> rule2))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The dog needs the bear.
("dog" "needs" "bear" "+")
triple2
The bear is cold.
("bear" "is" "cold" "+")
((triple1) -> (rule4 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear sees the dog.
("bear" "sees" "dog" "+")
((triple1) -> (rule8 % int1))
The bear sees the dog.
("bear" "sees" "dog" "+")
int1
((triple2) -> (rule3 % int1))
The bear sees the dog.
("bear" "sees" "dog" "+")
int1
The dog is big.
("dog" "is" "big" "+")
((triple2) -> (rule1 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The bear is big.
("bear" "is" "big" "+")
((((triple1) -> (rule4 % int3)) ((triple1) -> (rule8 % int2))) -> (rule2 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear sees the dog.
("bear" "sees" "dog" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
((((triple1) -> (rule4 % int3)) ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear sees the dog.
("bear" "sees" "dog" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3