The bear eats the cow. The bear is not nice. The bear is rough. The bear is round. The bear needs the cow. The cow eats the bear. The cow is kind. The cow is nice. The cow is round. The cow is young. The cow likes the bear. The cow does not need the bear. If something eats the cow then it is rough. If the cow likes the bear then the cow is nice. If something is nice then it eats the cow. If something likes the bear then it likes the cow. If something likes the cow then the cow eats the bear. If the bear does not like the cow then the cow eats the bear.
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear is not nice.
("bear" "is" "nice" "-")
The bear is rough.
("bear" "is" "rough" "+")
The bear is round.
("bear" "is" "round" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is round.
("cow" "is" "round" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow does not need the bear.
("cow" "needs" "bear" "-")
If something eats the cow then it is rough.
((("something" "eats" "cow" "+")) -> ("something" "is" "rough" "+"))
If the cow likes the bear then the cow is nice.
((("cow" "likes" "bear" "+")) -> ("cow" "is" "nice" "+"))
If something is nice then it eats the cow.
((("something" "is" "nice" "+")) -> ("something" "eats" "cow" "+"))
If something likes the bear then it likes the cow.
((("something" "likes" "bear" "+")) -> ("something" "likes" "cow" "+"))
If something likes the cow then the cow eats the bear.
((("something" "likes" "cow" "+")) -> ("cow" "eats" "bear" "+"))
If the bear does not like the cow then the cow eats the bear.
((("bear" "likes" "cow" "~")) -> ("cow" "eats" "bear" "+"))
The bear is rough.
True
1
proof
[(triple3 OR ((triple1) -> rule1))]
("bear" "is" "rough" "+")
triple3
((triple1) -> (rule1 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The cow is not young.
False
1
inv-proof
[(triple10)]
("cow" "is" "young" "-")
triple10
The cow likes the cow.
True
2
proof
[(((triple11) -> rule4))]
("cow" "likes" "cow" "+")
((triple11) -> (rule4 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow does not like the cow.
False
2
inv-proof
[(((triple11) -> rule4))]
("cow" "likes" "cow" "-")
((triple11) -> (rule4 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow is rough.
True
3
proof
[(((((triple8) -> rule3)) -> rule1) OR ((((((triple11) -> rule2)) -> rule3)) -> rule1))]
("cow" "is" "rough" "+")
((((triple8) -> (rule3 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
((((((triple11) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The cow is not rough.
False
3
inv-proof
[(((((triple8) -> rule3)) -> rule1) OR ((((((triple11) -> rule2)) -> rule3)) -> rule1))]
("cow" "is" "rough" "-")
((((triple8) -> (rule3 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
((((((triple11) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The bear does not like the cow.
Unknown
inv-rconc
[@1: The bear likes the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "likes" "cow" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
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 bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
@0: The bear eats the cow.[(triple1)] The bear is not nice.[(triple2)] The bear is rough.[(triple3 OR ((triple1) -> rule1))] The bear is round.[(triple4)] The bear needs the cow.[(triple5)] The cow does not need the bear.[(triple12)] The cow eats the bear.[(triple6 OR ((((triple11) -> rule4)) -> rule5))] The cow is kind.[(triple7)] The cow is nice.[(triple8 OR ((triple11) -> rule2))] The cow is round.[(triple9)] The cow is young.[(triple10)] The cow likes the bear.[(triple11)] @1: The cow eats the cow.[(((triple8) -> rule3) OR ((((triple11) -> rule2)) -> rule3))] The cow likes the cow.[(((triple11) -> rule4))] @2: The cow is rough.[(((((triple8) -> rule3)) -> rule1) OR ((((((triple11) -> rule2)) -> rule3)) -> rule1))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The bear is not nice.
("bear" "is" "nice" "-")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
((triple1) -> (rule1 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is round.
("bear" "is" "round" "+")
triple4
The bear needs the cow.
("bear" "needs" "cow" "+")
triple5
The cow does not need the bear.
("cow" "needs" "bear" "-")
triple12
The cow eats the bear.
("cow" "eats" "bear" "+")
triple6
((((triple11) -> (rule4 % int2))) -> (rule5 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
triple7
The cow is nice.
("cow" "is" "nice" "+")
triple8
((triple11) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is round.
("cow" "is" "round" "+")
triple9
The cow is young.
("cow" "is" "young" "+")
triple10
The cow likes the bear.
("cow" "likes" "bear" "+")
triple11
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple8) -> (rule3 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple11) -> (rule4 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((((triple8) -> (rule3 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
((((((triple11) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3