The bear is blue. The bear needs the dog. The cow needs the dog. The cow needs the squirrel. The dog is cold. The dog needs the bear. The dog visits the squirrel. The squirrel is kind. The squirrel needs the cow. The squirrel visits the bear. If the dog likes the squirrel then the dog needs the squirrel. If someone visits the cow then they are blue. If someone needs the cow then they visit the cow. If the dog visits the bear then the bear visits the squirrel. If the squirrel visits the dog and the squirrel is round then the dog likes the squirrel. If the cow needs the squirrel then the squirrel needs the cow. If someone needs the cow then the cow is big. If someone is cold and they visit the squirrel then the squirrel needs the cow.
The bear is blue.
("bear" "is" "blue" "+")
The bear needs the dog.
("bear" "needs" "dog" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
If the dog likes the squirrel then the dog needs the squirrel.
((("dog" "likes" "squirrel" "+")) -> ("dog" "needs" "squirrel" "+"))
If someone visits the cow then they are blue.
((("someone" "visits" "cow" "+")) -> ("someone" "is" "blue" "+"))
If someone needs the cow then they visit the cow.
((("someone" "needs" "cow" "+")) -> ("someone" "visits" "cow" "+"))
If the dog visits the bear then the bear visits the squirrel.
((("dog" "visits" "bear" "+")) -> ("bear" "visits" "squirrel" "+"))
If the squirrel visits the dog and the squirrel is round then the dog likes the squirrel.
((("squirrel" "visits" "dog" "+") ("squirrel" "is" "round" "+")) -> ("dog" "likes" "squirrel" "+"))
If the cow needs the squirrel then the squirrel needs the cow.
((("cow" "needs" "squirrel" "+")) -> ("squirrel" "needs" "cow" "+"))
If someone needs the cow then the cow is big.
((("someone" "needs" "cow" "+")) -> ("cow" "is" "big" "+"))
If someone is cold and they visit the squirrel then the squirrel needs the cow.
((("someone" "is" "cold" "+") ("someone" "visits" "squirrel" "+")) -> ("squirrel" "needs" "cow" "+"))
The dog needs the bear.
True
1
proof
[(triple6)]
("dog" "needs" "bear" "+")
triple6
The dog is not cold.
False
1
inv-proof
[(triple5)]
("dog" "is" "cold" "-")
triple5
The cow is big.
True
2
proof
[(((triple9) -> rule7) OR ((((triple4) -> rule6)) -> rule7) OR ((((triple5 triple7) -> rule8)) -> rule7))]
("cow" "is" "big" "+")
((triple9) -> (rule7 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule7 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int2
((((triple5 triple7) -> (rule8 % int2))) -> (rule7 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int2
The squirrel does not visit the cow.
False
2
inv-proof
[(((triple9) -> rule3) OR ((((triple4) -> rule6)) -> rule3) OR ((((triple5 triple7) -> rule8)) -> rule3))]
("squirrel" "visits" "cow" "-")
((triple9) -> (rule3 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int2
((((triple5 triple7) -> (rule8 % int2))) -> (rule3 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int2
The squirrel is blue.
True
3
proof
[(((((triple9) -> rule3)) -> rule2) OR ((((((triple4) -> rule6)) -> rule3)) -> rule2) OR ((((((triple5 triple7) -> rule8)) -> rule3)) -> rule2))]
("squirrel" "is" "blue" "+")
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
((((((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int3
((((((triple5 triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int3
The squirrel is not blue.
False
3
inv-proof
[(((((triple9) -> rule3)) -> rule2) OR ((((((triple4) -> rule6)) -> rule3)) -> rule2) OR ((((((triple5 triple7) -> rule8)) -> rule3)) -> rule2))]
("squirrel" "is" "blue" "-")
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
((((((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int3
((((((triple5 triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int3
The bear does not visit the squirrel.
Unknown
inv-rconc
[@1: The bear visits the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "visits" "squirrel" "-")
The dog visits the cow.
Unknown
rconc
[@1: The dog visits the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "visits" "cow" "+")
The dog is not blue.
Unknown
inv-rconc
[@2: The dog is blue.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("dog" "is" "blue" "-")
The dog likes the bear.
Unknown
random
[@0: The dog likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "bear" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
@0: The bear is blue.[(triple1)] The bear needs the dog.[(triple2)] The cow needs the dog.[(triple3)] The cow needs the squirrel.[(triple4)] The dog is cold.[(triple5)] The dog needs the bear.[(triple6)] The dog visits the squirrel.[(triple7)] The squirrel is kind.[(triple8)] The squirrel needs the cow.[(triple9 OR ((triple4) -> rule6) OR ((triple5 triple7) -> rule8))] The squirrel visits the bear.[(triple10)] @1: The cow is big.[(((triple9) -> rule7) OR ((((triple4) -> rule6)) -> rule7) OR ((((triple5 triple7) -> rule8)) -> rule7))] The squirrel visits the cow.[(((triple9) -> rule3) OR ((((triple4) -> rule6)) -> rule3) OR ((((triple5 triple7) -> rule8)) -> rule3))] @2: The squirrel is blue.[(((((triple9) -> rule3)) -> rule2) OR ((((((triple4) -> rule6)) -> rule3)) -> rule2) OR ((((((triple5 triple7) -> rule8)) -> rule3)) -> rule2))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear needs the dog.
("bear" "needs" "dog" "+")
triple2
The cow needs the dog.
("cow" "needs" "dog" "+")
triple3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple4
The dog is cold.
("dog" "is" "cold" "+")
triple5
The dog needs the bear.
("dog" "needs" "bear" "+")
triple6
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple7
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple8
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple9
((triple4) -> (rule6 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
((triple5 triple7) -> (rule8 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple10
The cow is big.
("cow" "is" "big" "+")
((triple9) -> (rule7 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule7 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int2
((((triple5 triple7) -> (rule8 % int2))) -> (rule7 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int2
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
((triple9) -> (rule3 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int2
((((triple5 triple7) -> (rule8 % int2))) -> (rule3 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
((((((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int3
((((((triple5 triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int3