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