The bear is big. The bear is cold. The bear likes the cow. The bear needs the dog. The cow is nice. The cow is young. The cow likes the bear. The cow likes the dog. The cow needs the dog. The cow sees the dog. The dog is young. The dog likes the bear. The dog needs the bear. The dog needs the cow. The dog sees the cow. If someone needs the bear and they are cold then they like the cow. If the dog likes the bear then the dog is cold. If someone likes the cow and they like the bear then the cow likes the bear. If someone is cold and they need the cow then the cow is green. If someone needs the bear and they like the bear then they see the dog. If someone is big then they like the cow.
The bear is big.
("bear" "is" "big" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear likes the cow.
("bear" "likes" "cow" "+")
The bear needs the dog.
("bear" "needs" "dog" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
If someone needs the bear and they are cold then they like the cow.
((("someone" "needs" "bear" "+") ("someone" "is" "cold" "+")) -> ("someone" "likes" "cow" "+"))
If the dog likes the bear then the dog is cold.
((("dog" "likes" "bear" "+")) -> ("dog" "is" "cold" "+"))
If someone likes the cow and they like the bear then the cow likes the bear.
((("someone" "likes" "cow" "+") ("someone" "likes" "bear" "+")) -> ("cow" "likes" "bear" "+"))
If someone is cold and they need the cow then the cow is green.
((("someone" "is" "cold" "+") ("someone" "needs" "cow" "+")) -> ("cow" "is" "green" "+"))
If someone needs the bear and they like the bear then they see the dog.
((("someone" "needs" "bear" "+") ("someone" "likes" "bear" "+")) -> ("someone" "sees" "dog" "+"))
If someone is big then they like the cow.
((("someone" "is" "big" "+")) -> ("someone" "likes" "cow" "+"))
The cow likes the bear.
True
1
proof
[(triple7 OR ((((triple13 ((triple12) -> rule2)) -> rule1) triple12) -> rule3))]
("cow" "likes" "bear" "+")
triple7
((((triple13 ((triple12) -> (rule2 % int3))) -> (rule1 % int2)) triple12) -> (rule3 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The dog likes the cow.
("dog" "likes" "cow" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The dog does not need the bear.
False
1
inv-proof
[(triple13)]
("dog" "needs" "bear" "-")
triple13
The dog is cold.
True
2
proof
[(((triple12) -> rule2))]
("dog" "is" "cold" "+")
((triple12) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog does not see the dog.
False
3
inv-proof
[(((triple13 triple12) -> rule5))]
("dog" "sees" "dog" "-")
((triple13 triple12) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The cow is green.
True
4
proof
[(((((triple12) -> rule2) triple14) -> rule4))]
("cow" "is" "green" "+")
((((triple12) -> (rule2 % int2)) triple14) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The cow is not green.
False
4
inv-proof
[(((((triple12) -> rule2) triple14) -> rule4))]
("cow" "is" "green" "-")
((((triple12) -> (rule2 % int2)) triple14) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The bear does not see the dog.
Unknown
inv-rconc
[@1: The bear sees the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "sees" "dog" "-")
The cow likes the cow.
Unknown
rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "cow" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The dog sees the bear.
Unknown
random
[@0: The dog sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "bear" "+")
The bear does not like the dog.
Unknown
inv-random
[@0: The bear likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "dog" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear is big.[(triple1)] The bear is cold.[(triple2)] The bear likes the cow.[(triple3 OR ((triple1) -> rule6))] The bear needs the dog.[(triple4)] The cow is nice.[(triple5)] The cow is young.[(triple6)] The cow likes the bear.[(triple7 OR ((((triple13 ((triple12) -> rule2)) -> rule1) triple12) -> rule3))] The cow likes the dog.[(triple8)] The cow needs the dog.[(triple9)] The cow sees the dog.[(triple10)] The dog is young.[(triple11)] The dog likes the bear.[(triple12)] The dog needs the bear.[(triple13)] The dog needs the cow.[(triple14)] The dog sees the cow.[(triple15)] @1: The dog is cold.[(((triple12) -> rule2))] The dog sees the dog.[(((triple13 triple12) -> rule5))] @2: The cow is green.[(((((triple12) -> rule2) triple14) -> rule4))] The dog likes the cow.[(((triple13 ((triple12) -> rule2)) -> rule1))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear likes the cow.
("bear" "likes" "cow" "+")
triple3
((triple1) -> (rule6 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
triple4
The cow is nice.
("cow" "is" "nice" "+")
triple5
The cow is young.
("cow" "is" "young" "+")
triple6
The cow likes the bear.
("cow" "likes" "bear" "+")
triple7
((((triple13 ((triple12) -> (rule2 % int3))) -> (rule1 % int2)) triple12) -> (rule3 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The dog likes the cow.
("dog" "likes" "cow" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The cow likes the dog.
("cow" "likes" "dog" "+")
triple8
The cow needs the dog.
("cow" "needs" "dog" "+")
triple9
The cow sees the dog.
("cow" "sees" "dog" "+")
triple10
The dog is young.
("dog" "is" "young" "+")
triple11
The dog likes the bear.
("dog" "likes" "bear" "+")
triple12
The dog needs the bear.
("dog" "needs" "bear" "+")
triple13
The dog needs the cow.
("dog" "needs" "cow" "+")
triple14
The dog sees the cow.
("dog" "sees" "cow" "+")
triple15
The dog is cold.
("dog" "is" "cold" "+")
((triple12) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
((triple13 triple12) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The cow is green.
("cow" "is" "green" "+")
((((triple12) -> (rule2 % int2)) triple14) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog likes the cow.
("dog" "likes" "cow" "+")
((triple13 ((triple12) -> (rule2 % int2))) -> (rule1 % int1))
The dog likes the cow.
("dog" "likes" "cow" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2