The bear eats the dog. The bear is big. The bear is not cold. The dog eats the bear. The dog is blue. The dog is cold. The dog visits the bear. If the bear likes the dog and the bear is big then the bear does not eat the dog. If something likes the bear and it does not eat the bear then it does not like the dog. If something is cold then it likes the dog. If something is blue then it likes the bear. If something is cold and it does not visit the bear then the bear is cold. If something likes the bear then the bear visits the dog. If something likes the bear then it visits the dog. If something visits the dog then the dog is big.
The bear eats the dog.
("bear" "eats" "dog" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is not cold.
("bear" "is" "cold" "-")
The dog eats the bear.
("dog" "eats" "bear" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
If the bear likes the dog and the bear is big then the bear does not eat the dog.
((("bear" "likes" "dog" "+") ("bear" "is" "big" "+")) -> ("bear" "eats" "dog" "-"))
If something likes the bear and it does not eat the bear then it does not like the dog.
((("something" "likes" "bear" "+") ("something" "eats" "bear" "~")) -> ("something" "likes" "dog" "-"))
If something is cold then it likes the dog.
((("something" "is" "cold" "+")) -> ("something" "likes" "dog" "+"))
If something is blue then it likes the bear.
((("something" "is" "blue" "+")) -> ("something" "likes" "bear" "+"))
If something is cold and it does not visit the bear then the bear is cold.
((("something" "is" "cold" "+") ("something" "visits" "bear" "~")) -> ("bear" "is" "cold" "+"))
If something likes the bear then the bear visits the dog.
((("something" "likes" "bear" "+")) -> ("bear" "visits" "dog" "+"))
If something likes the bear then it visits the dog.
((("something" "likes" "bear" "+")) -> ("something" "visits" "dog" "+"))
If something visits the dog then the dog is big.
((("something" "visits" "dog" "+")) -> ("dog" "is" "big" "+"))
The bear is not cold.
True
1
proof
[(triple3)]
("bear" "is" "cold" "-")
triple3
The dog does not visit the bear.
False
1
inv-proof
[(triple7)]
("dog" "visits" "bear" "-")
triple7
The dog likes the dog.
True
2
proof
[(((triple6) -> rule3))]
("dog" "likes" "dog" "+")
((triple6) -> (rule3 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog does not like the bear.
False
2
inv-proof
[(((triple5) -> rule4))]
("dog" "likes" "bear" "-")
((triple5) -> (rule4 % int1))
The dog likes the bear.
("dog" "likes" "bear" "+")
int1
The dog visits the dog.
True
3
proof
[(((((triple5) -> rule4)) -> rule7))]
("dog" "visits" "dog" "+")
((((triple5) -> (rule4 % int2))) -> (rule7 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
int2
The dog does not visit the dog.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule7))]
("dog" "visits" "dog" "-")
((((triple5) -> (rule4 % int2))) -> (rule7 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
int2
The dog is big.
True
4
proof
[(((((((triple5) -> rule4)) -> rule6)) -> rule8) OR ((((((triple5) -> rule4)) -> rule7)) -> rule8))]
("dog" "is" "big" "+")
((((((triple5) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3
((((((triple5) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3
The dog is not big.
False
4
inv-proof
[(((((((triple5) -> rule4)) -> rule6)) -> rule8) OR ((((((triple5) -> rule4)) -> rule7)) -> rule8))]
("dog" "is" "big" "-")
((((((triple5) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3
((((((triple5) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3
The bear does not like the dog.
Unknown
inv-rconc
[@1: The bear likes the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "likes" "dog" "-")
The bear likes the bear.
Unknown
rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "likes" "bear" "+")
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The bear is blue.
Unknown
random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "+")
@0: The bear eats the dog.[(triple1)] The bear is big.[(triple2)] The bear is not cold.[(triple3)] The dog eats the bear.[(triple4)] The dog is blue.[(triple5)] The dog is cold.[(triple6)] The dog visits the bear.[(triple7)] @1: The dog likes the bear.[(((triple5) -> rule4))] The dog likes the dog.[(((triple6) -> rule3))] @2: The bear visits the dog.[(((((triple5) -> rule4)) -> rule6))] The dog visits the dog.[(((((triple5) -> rule4)) -> rule7))] @3: The dog is big.[(((((((triple5) -> rule4)) -> rule6)) -> rule8) OR ((((((triple5) -> rule4)) -> rule7)) -> rule8))]
The bear eats the dog.
("bear" "eats" "dog" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is not cold.
("bear" "is" "cold" "-")
triple3
The dog eats the bear.
("dog" "eats" "bear" "+")
triple4
The dog is blue.
("dog" "is" "blue" "+")
triple5
The dog is cold.
("dog" "is" "cold" "+")
triple6
The dog visits the bear.
("dog" "visits" "bear" "+")
triple7
The dog likes the bear.
("dog" "likes" "bear" "+")
((triple5) -> (rule4 % int1))
The dog likes the bear.
("dog" "likes" "bear" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
((triple6) -> (rule3 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
((((triple5) -> (rule4 % int2))) -> (rule7 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
int2
The dog is big.
("dog" "is" "big" "+")
((((((triple5) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3
((((((triple5) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3