The cow is blue. The cow is green. The cow is nice. The cow is rough. The cow is young. The cow likes the tiger. The cow needs the tiger. The cow visits the tiger. The tiger is blue. The tiger is green. The tiger is nice. The tiger is rough. The tiger is young. The tiger likes the cow. The tiger needs the cow. The tiger visits the cow. If someone is rough then they visit the cow. If someone is blue and nice then they like the cow. If someone needs the cow then they like the tiger. If the cow visits the tiger and the tiger visits the cow then the tiger likes the cow. If someone needs the tiger and they visit the tiger then they are young. If the tiger is young then the tiger visits the cow. If someone likes the cow then they need the tiger. If someone needs the tiger then the tiger needs the cow.
The cow is blue.
("cow" "is" "blue" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If someone is rough then they visit the cow.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "cow" "+"))
If someone is blue and nice then they like the cow.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "likes" "cow" "+"))
If someone needs the cow then they like the tiger.
((("someone" "needs" "cow" "+")) -> ("someone" "likes" "tiger" "+"))
If the cow visits the tiger and the tiger visits the cow then the tiger likes the cow.
((("cow" "visits" "tiger" "+") ("tiger" "visits" "cow" "+")) -> ("tiger" "likes" "cow" "+"))
If someone needs the tiger and they visit the tiger then they are young.
((("someone" "needs" "tiger" "+") ("someone" "visits" "tiger" "+")) -> ("someone" "is" "young" "+"))
If the tiger is young then the tiger visits the cow.
((("tiger" "is" "young" "+")) -> ("tiger" "visits" "cow" "+"))
If someone likes the cow then they need the tiger.
((("someone" "likes" "cow" "+")) -> ("someone" "needs" "tiger" "+"))
If someone needs the tiger then the tiger needs the cow.
((("someone" "needs" "tiger" "+")) -> ("tiger" "needs" "cow" "+"))
The tiger visits the cow.
True
1
proof
[(triple16 OR ((triple12) -> rule1) OR ((triple13) -> rule6))]
("tiger" "visits" "cow" "+")
triple16
((triple12) -> (rule1 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
((triple13) -> (rule6 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger does not visit the cow.
False
1
inv-proof
[(triple16 OR ((triple12) -> rule1) OR ((triple13) -> rule6))]
("tiger" "visits" "cow" "-")
triple16
((triple12) -> (rule1 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
((triple13) -> (rule6 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow is blue.[(triple1)] The cow is green.[(triple2)] The cow is nice.[(triple3)] The cow is rough.[(triple4)] The cow is young.[(triple5 OR ((triple7 triple8) -> rule5) OR ((((((triple1 triple3) -> rule2)) -> rule7) triple8) -> rule5))] The cow likes the tiger.[(triple6)] The cow needs the tiger.[(triple7 OR ((((triple1 triple3) -> rule2)) -> rule7))] The cow visits the tiger.[(triple8)] The tiger is blue.[(triple9)] The tiger is green.[(triple10)] The tiger is nice.[(triple11)] The tiger is rough.[(triple12)] The tiger is young.[(triple13)] The tiger likes the cow.[(triple14 OR ((triple8 triple16) -> rule4) OR ((triple9 triple11) -> rule2) OR ((triple8 ((triple12) -> rule1)) -> rule4) OR ((triple8 ((triple13) -> rule6)) -> rule4))] The tiger needs the cow.[(triple15 OR ((triple7) -> rule8) OR ((((triple14) -> rule7)) -> rule8) OR ((((((triple1 triple3) -> rule2)) -> rule7)) -> rule8) OR ((((((triple8 triple16) -> rule4)) -> rule7)) -> rule8) OR ((((((triple9 triple11) -> rule2)) -> rule7)) -> rule8) OR ((((((triple8 ((triple12) -> rule1)) -> rule4)) -> rule7)) -> rule8) OR ((((((triple8 ((triple13) -> rule6)) -> rule4)) -> rule7)) -> rule8))] The tiger visits the cow.[(triple16 OR ((triple12) -> rule1) OR ((triple13) -> rule6))] @1: The cow likes the cow.[(((triple1 triple3) -> rule2))] The cow visits the cow.[(((triple4) -> rule1))] The tiger likes the tiger.[(((triple15) -> rule3) OR ((((triple7) -> rule8)) -> rule3) OR ((((((triple14) -> rule7)) -> rule8)) -> rule3) OR ((((((((triple1 triple3) -> rule2)) -> rule7)) -> rule8)) -> rule3) OR ((((((((triple8 triple16) -> rule4)) -> rule7)) -> rule8)) -> rule3) OR ((((((((triple9 triple11) -> rule2)) -> rule7)) -> rule8)) -> rule3) OR ((((((((triple8 ((triple12) -> rule1)) -> rule4)) -> rule7)) -> rule8)) -> rule3) OR ((((((((triple8 ((triple13) -> rule6)) -> rule4)) -> rule7)) -> rule8)) -> rule3))] The tiger needs the tiger.[(((triple14) -> rule7) OR ((((triple8 triple16) -> rule4)) -> rule7) OR ((((triple9 triple11) -> rule2)) -> rule7) OR ((((triple8 ((triple12) -> rule1)) -> rule4)) -> rule7) OR ((((triple8 ((triple13) -> rule6)) -> rule4)) -> rule7))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow is rough.
("cow" "is" "rough" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5
((triple7 triple8) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((((((triple1 triple3) -> (rule2 % int3))) -> (rule7 % int2)) triple8) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple6
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple7
((((triple1 triple3) -> (rule2 % int2))) -> (rule7 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple8
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger is green.
("tiger" "is" "green" "+")
triple10
The tiger is nice.
("tiger" "is" "nice" "+")
triple11
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple14
((triple8 triple16) -> (rule4 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
((triple9 triple11) -> (rule2 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
((triple8 ((triple12) -> (rule1 % int2))) -> (rule4 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
((triple8 ((triple13) -> (rule6 % int2))) -> (rule4 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple15
((triple7) -> (rule8 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
((((triple14) -> (rule7 % int2))) -> (rule8 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
((((((triple1 triple3) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
((((((triple8 triple16) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
((((((triple9 triple11) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
((((((triple8 ((triple12) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int4
((((((triple8 ((triple13) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int4
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple16
((triple12) -> (rule1 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
((triple13) -> (rule6 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple1 triple3) -> (rule2 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple4) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple15) -> (rule3 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
((((((triple14) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
((((((((triple1 triple3) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int3
The cow likes the cow.
("cow" "likes" "cow" "+")
int4
((((((((triple8 triple16) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int4
((((((((triple9 triple11) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int4
((((((((triple8 ((triple12) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int4
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int5
((((((((triple8 ((triple13) -> (rule6 % int5))) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int4
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int5
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple14) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
((((triple8 triple16) -> (rule4 % int2))) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
((((triple9 triple11) -> (rule2 % int2))) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
((((triple8 ((triple12) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int3
((((triple8 ((triple13) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int3