The bear chases the cow. The bear likes the cow. The bear needs the cat. The bear needs the cow. The cat is big. The cat is blue. The cat likes the cow. The cat needs the bear. The cow chases the bear. The cow is nice. The cow is young. The cow needs the cat. If something is big then it is red. If something is young and it needs the cat then it is big. If something is blue and it chases the cow then it needs the bear. If something likes the cow and the cow is nice then it is red. If the bear is big then the bear likes the cow. If something likes the cow then it is nice.
The bear chases the cow.
("bear" "chases" "cow" "+")
The bear likes the cow.
("bear" "likes" "cow" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
If something is big then it is red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is young and it needs the cat then it is big.
((("something" "is" "young" "+") ("something" "needs" "cat" "+")) -> ("something" "is" "big" "+"))
If something is blue and it chases the cow then it needs the bear.
((("something" "is" "blue" "+") ("something" "chases" "cow" "+")) -> ("something" "needs" "bear" "+"))
If something likes the cow and the cow is nice then it is red.
((("something" "likes" "cow" "+") ("cow" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If the bear is big then the bear likes the cow.
((("bear" "is" "big" "+")) -> ("bear" "likes" "cow" "+"))
If something likes the cow then it is nice.
((("something" "likes" "cow" "+")) -> ("something" "is" "nice" "+"))
The bear likes the cow.
True
1
proof
[(triple2)]
("bear" "likes" "cow" "+")
triple2
The cat does not need the bear.
False
1
inv-proof
[(triple8)]
("cat" "needs" "bear" "-")
triple8
The bear is nice.
True
2
proof
[(((triple2) -> rule6))]
("bear" "is" "nice" "+")
((triple2) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is not red.
False
3
inv-proof
[(((triple2 triple10) -> rule4))]
("bear" "is" "red" "-")
((triple2 triple10) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cow is red.
True
4
proof
[(((((triple11 triple12) -> rule2)) -> rule1))]
("cow" "is" "red" "+")
((((triple11 triple12) -> (rule2 % int2))) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is not red.
False
4
inv-proof
[(((((triple11 triple12) -> rule2)) -> rule1))]
("cow" "is" "red" "-")
((((triple11 triple12) -> (rule2 % int2))) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The bear does not need the bear.
Unknown
inv-rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "needs" "bear" "-")
The bear is big.
Unknown
rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "big" "+")
The cow does not need the bear.
Unknown
inv-rconc
[@1: The cow needs the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "needs" "bear" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
The cow does not chase the cat.
Unknown
inv-random
[@0: The cow chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cat" "-")
The cow likes the bear.
Unknown
random
[@0: The cow likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "bear" "+")
@0: The bear chases the cow.[(triple1)] The bear likes the cow.[(triple2)] The bear needs the cat.[(triple3)] The bear needs the cow.[(triple4)] The cat is big.[(triple5)] The cat is blue.[(triple6)] The cat likes the cow.[(triple7)] The cat needs the bear.[(triple8)] The cow chases the bear.[(triple9)] The cow is nice.[(triple10)] The cow is young.[(triple11)] The cow needs the cat.[(triple12)] @1: The bear is nice.[(((triple2) -> rule6))] The bear is red.[(((triple2 triple10) -> rule4))] The cat is nice.[(((triple7) -> rule6))] The cat is red.[(((triple5) -> rule1) OR ((triple7 triple10) -> rule4))] The cow is big.[(((triple11 triple12) -> rule2))] @2: The cow is red.[(((((triple11 triple12) -> rule2)) -> rule1))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The bear likes the cow.
("bear" "likes" "cow" "+")
triple2
The bear needs the cat.
("bear" "needs" "cat" "+")
triple3
The bear needs the cow.
("bear" "needs" "cow" "+")
triple4
The cat is big.
("cat" "is" "big" "+")
triple5
The cat is blue.
("cat" "is" "blue" "+")
triple6
The cat likes the cow.
("cat" "likes" "cow" "+")
triple7
The cat needs the bear.
("cat" "needs" "bear" "+")
triple8
The cow chases the bear.
("cow" "chases" "bear" "+")
triple9
The cow is nice.
("cow" "is" "nice" "+")
triple10
The cow is young.
("cow" "is" "young" "+")
triple11
The cow needs the cat.
("cow" "needs" "cat" "+")
triple12
The bear is nice.
("bear" "is" "nice" "+")
((triple2) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is red.
("bear" "is" "red" "+")
((triple2 triple10) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
((triple7) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is red.
("cat" "is" "red" "+")
((triple5) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((triple7 triple10) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cow is big.
("cow" "is" "big" "+")
((triple11 triple12) -> (rule2 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is red.
("cow" "is" "red" "+")
((((triple11 triple12) -> (rule2 % int2))) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2