The bear is big. The bear is red. The bear needs the cow. The cow eats the bear. The cow is blue. The cow likes the bear. The cow needs the bear. If someone is red and they need the cow then the cow eats the bear. If someone eats the bear then the bear is red. If someone needs the bear and they are nice then the bear is blue. If someone needs the cow and the cow likes the bear then the bear likes the cow. If the bear likes the cow then the cow is nice. If the cow is big and the cow eats the bear then the cow is red. If someone likes the cow and they eat the cow then they need the bear. If the bear eats the cow then the bear likes the cow.
The bear is big.
("bear" "is" "big" "+")
The bear is red.
("bear" "is" "red" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
If someone is red and they need the cow then the cow eats the bear.
((("someone" "is" "red" "+") ("someone" "needs" "cow" "+")) -> ("cow" "eats" "bear" "+"))
If someone eats the bear then the bear is red.
((("someone" "eats" "bear" "+")) -> ("bear" "is" "red" "+"))
If someone needs the bear and they are nice then the bear is blue.
((("someone" "needs" "bear" "+") ("someone" "is" "nice" "+")) -> ("bear" "is" "blue" "+"))
If someone needs the cow and the cow likes the bear then the bear likes the cow.
((("someone" "needs" "cow" "+") ("cow" "likes" "bear" "+")) -> ("bear" "likes" "cow" "+"))
If the bear likes the cow then the cow is nice.
((("bear" "likes" "cow" "+")) -> ("cow" "is" "nice" "+"))
If the cow is big and the cow eats the bear then the cow is red.
((("cow" "is" "big" "+") ("cow" "eats" "bear" "+")) -> ("cow" "is" "red" "+"))
If someone likes the cow and they eat the cow then they need the bear.
((("someone" "likes" "cow" "+") ("someone" "eats" "cow" "+")) -> ("someone" "needs" "bear" "+"))
If the bear eats the cow then the bear likes the cow.
((("bear" "eats" "cow" "+")) -> ("bear" "likes" "cow" "+"))
The bear needs the cow.
True
1
proof
[(triple3)]
("bear" "needs" "cow" "+")
triple3
The bear does not need the cow.
False
1
inv-proof
[(triple3)]
("bear" "needs" "cow" "-")
triple3
The bear likes the cow.
True
3
proof
[(((triple3 triple6) -> rule4))]
("bear" "likes" "cow" "+")
((triple3 triple6) -> (rule4 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The bear does not like the cow.
False
3
inv-proof
[(((triple3 triple6) -> rule4))]
("bear" "likes" "cow" "-")
((triple3 triple6) -> (rule4 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The cow is nice.
True
4
proof
[(((((triple3 triple6) -> rule4)) -> rule5))]
("cow" "is" "nice" "+")
((((triple3 triple6) -> (rule4 % int2))) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The bear likes the cow.
("bear" "likes" "cow" "+")
int2
The cow is not nice.
False
4
inv-proof
[(((((triple3 triple6) -> rule4)) -> rule5))]
("cow" "is" "nice" "-")
((((triple3 triple6) -> (rule4 % int2))) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The bear likes the cow.
("bear" "likes" "cow" "+")
int2
The bear is blue.
True
6
proof
[(((triple7 ((((triple3 triple6) -> rule4)) -> rule5)) -> rule3))]
("bear" "is" "blue" "+")
((triple7 ((((triple3 triple6) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The bear likes the cow.
("bear" "likes" "cow" "+")
int3
The bear is not blue.
False
6
inv-proof
[(((triple7 ((((triple3 triple6) -> rule4)) -> rule5)) -> rule3))]
("bear" "is" "blue" "-")
((triple7 ((((triple3 triple6) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The bear likes the cow.
("bear" "likes" "cow" "+")
int3
The cow is not red.
Unknown
inv-rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "red" "-")
The bear needs the bear.
Unknown
rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "needs" "bear" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The bear eats the cow.
Unknown
random
[@0: The bear eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "cow" "+")
@0: The bear is big.[(triple1)] The bear is red.[(triple2 OR ((triple4) -> rule2))] The bear needs the cow.[(triple3)] The cow eats the bear.[(triple4 OR ((triple2 triple3) -> rule1))] The cow is blue.[(triple5)] The cow likes the bear.[(triple6)] The cow needs the bear.[(triple7)] @1: The bear likes the cow.[(((triple3 triple6) -> rule4))] @2: The cow is nice.[(((((triple3 triple6) -> rule4)) -> rule5))] @3: The bear is blue.[(((triple7 ((((triple3 triple6) -> rule4)) -> rule5)) -> rule3))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is red.
("bear" "is" "red" "+")
triple2
((triple4) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
triple3
The cow eats the bear.
("cow" "eats" "bear" "+")
triple4
((triple2 triple3) -> (rule1 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
triple5
The cow likes the bear.
("cow" "likes" "bear" "+")
triple6
The cow needs the bear.
("cow" "needs" "bear" "+")
triple7
The bear likes the cow.
("bear" "likes" "cow" "+")
((triple3 triple6) -> (rule4 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
((((triple3 triple6) -> (rule4 % int2))) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The bear likes the cow.
("bear" "likes" "cow" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
((triple7 ((((triple3 triple6) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The bear likes the cow.
("bear" "likes" "cow" "+")
int3