The bear is cold. The dog likes the bear. If someone eats the dog then the dog sees the bear. If someone sees the bear then the bear eats the dog. If the bear likes the dog and the bear is blue then the bear sees the dog. If someone sees the dog then they are kind. If the bear sees the dog then the bear is green. If someone is cold then they see the bear. If someone eats the bear and they eat the dog then the bear sees the dog. If the bear eats the dog then the dog is cold.
The bear is cold.
("bear" "is" "cold" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
If someone eats the dog then the dog sees the bear.
((("someone" "eats" "dog" "+")) -> ("dog" "sees" "bear" "+"))
If someone sees the bear then the bear eats the dog.
((("someone" "sees" "bear" "+")) -> ("bear" "eats" "dog" "+"))
If the bear likes the dog and the bear is blue then the bear sees the dog.
((("bear" "likes" "dog" "+") ("bear" "is" "blue" "+")) -> ("bear" "sees" "dog" "+"))
If someone sees the dog then they are kind.
((("someone" "sees" "dog" "+")) -> ("someone" "is" "kind" "+"))
If the bear sees the dog then the bear is green.
((("bear" "sees" "dog" "+")) -> ("bear" "is" "green" "+"))
If someone is cold then they see the bear.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "bear" "+"))
If someone eats the bear and they eat the dog then the bear sees the dog.
((("someone" "eats" "bear" "+") ("someone" "eats" "dog" "+")) -> ("bear" "sees" "dog" "+"))
If the bear eats the dog then the dog is cold.
((("bear" "eats" "dog" "+")) -> ("dog" "is" "cold" "+"))
The bear is cold.
True
1
proof
[(triple1)]
("bear" "is" "cold" "+")
triple1
The bear is not cold.
False
1
inv-proof
[(triple1)]
("bear" "is" "cold" "-")
triple1
The bear sees the bear.
True
2
proof
[(((triple1) -> rule6))]
("bear" "sees" "bear" "+")
((triple1) -> (rule6 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear does not see the bear.
False
2
inv-proof
[(((triple1) -> rule6))]
("bear" "sees" "bear" "-")
((triple1) -> (rule6 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear eats the dog.
True
3
proof
[(((((triple1) -> rule6)) -> rule2))]
("bear" "eats" "dog" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The bear eats the dog.
("bear" "eats" "dog" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear does not eat the dog.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule2))]
("bear" "eats" "dog" "-")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The bear eats the dog.
("bear" "eats" "dog" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The dog sees the bear.
True
4
proof
[(((((((triple1) -> rule6)) -> rule2)) -> rule1) OR ((((((((triple1) -> rule6)) -> rule2)) -> rule8)) -> rule6))]
("dog" "sees" "bear" "+")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The bear eats the dog.
("bear" "eats" "dog" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
((((((((triple1) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The bear eats the dog.
("bear" "eats" "dog" "+")
int3
The bear sees the bear.
("bear" "sees" "bear" "+")
int4
The dog does not see the bear.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule2)) -> rule1) OR ((((((((triple1) -> rule6)) -> rule2)) -> rule8)) -> rule6))]
("dog" "sees" "bear" "-")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The bear eats the dog.
("bear" "eats" "dog" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
((((((((triple1) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The bear eats the dog.
("bear" "eats" "dog" "+")
int3
The bear sees the bear.
("bear" "sees" "bear" "+")
int4
The bear does not see the dog.
Unknown
inv-rconc
[@1: The bear sees the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "sees" "dog" "-")
The bear is green.
Unknown
rconc
[@2: The bear is green.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("bear" "is" "green" "+")
The bear is not kind.
Unknown
inv-rconc
[@2: The bear is kind.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("bear" "is" "kind" "-")
The dog is kind.
Unknown
rconc
[@1: The dog is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "kind" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
The bear is not blue.
Unknown
inv-random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
@0: The bear is cold.[(triple1)] The dog likes the bear.[(triple2)] @1: The bear sees the bear.[(((triple1) -> rule6))] @2: The bear eats the dog.[(((((triple1) -> rule6)) -> rule2))] @3: The dog is cold.[(((((((triple1) -> rule6)) -> rule2)) -> rule8))] The dog sees the bear.[(((((((triple1) -> rule6)) -> rule2)) -> rule1) OR ((((((((triple1) -> rule6)) -> rule2)) -> rule8)) -> rule6))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The dog likes the bear.
("dog" "likes" "bear" "+")
triple2
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple1) -> (rule6 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear eats the dog.
("bear" "eats" "dog" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The bear eats the dog.
("bear" "eats" "dog" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The bear eats the dog.
("bear" "eats" "dog" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
The dog sees the bear.
("dog" "sees" "bear" "+")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The bear eats the dog.
("bear" "eats" "dog" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
((((((((triple1) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The bear eats the dog.
("bear" "eats" "dog" "+")
int3
The bear sees the bear.
("bear" "sees" "bear" "+")
int4